[STATEMENT]
lemma tensor_state [simp]:
  assumes "state m u" and "state n v"
  shows "state (m + n) (u \<Otimes> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state (m + n) (u \<Otimes> v)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dim_col (u \<Otimes> v) = 1
 2. dim_row (u \<Otimes> v) = 2 ^ (m + n)
 3. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
show c1:"dim_col (u \<Otimes> v) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (u \<Otimes> v) = 1
[PROOF STEP]
using assms dim_col_tensor_mat state.is_column
[PROOF STATE]
proof (prove)
using this:
state m u
state n v
dim_col (?A \<Otimes> ?B) = dim_col ?A * dim_col ?B
state ?n ?v \<Longrightarrow> dim_col ?v = 1

goal (1 subgoal):
 1. dim_col (u \<Otimes> v) = 1
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
dim_col (u \<Otimes> v) = 1

goal (2 subgoals):
 1. dim_row (u \<Otimes> v) = 2 ^ (m + n)
 2. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
show c2:"dim_row (u \<Otimes> v) = 2^(m + n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (u \<Otimes> v) = 2 ^ (m + n)
[PROOF STEP]
using assms dim_row_tensor_mat state.dim_row
[PROOF STATE]
proof (prove)
using this:
state m u
state n v
dim_row (?A \<Otimes> ?B) = dim_row ?A * dim_row ?B
state ?n ?v \<Longrightarrow> dim_row ?v = 2 ^ ?n

goal (1 subgoal):
 1. dim_row (u \<Otimes> v) = 2 ^ (m + n)
[PROOF STEP]
by (metis power_add)
[PROOF STATE]
proof (state)
this:
dim_row (u \<Otimes> v) = 2 ^ (m + n)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "(\<Sum>i<2^(m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) =
(\<Sum>i<2^(m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2)
[PROOF STEP]
by (simp add: sqr_of_cmod_of_prod)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "\<dots> = (\<Sum>i<2^m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2^n. (cmod (v $$ (i, 0)))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
have "\<dots> = (\<Sum>i<2^(m + n).complex_of_real((cmod (u $$ (i div 2^n,0)))\<^sup>2) * complex_of_real((cmod (v $$ (i mod 2^n,0)))\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
complex_of_real (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
complex_of_real (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
have "(\<Sum>i<2^m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2^m. complex_of_real ((cmod (u $$ (i,0)))\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
complex_of_real (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
complex_of_real (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
have "(\<Sum>i<2^n. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2^n. complex_of_real ((cmod (v $$ (i, 0)))\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complex_of_real (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ n. complex_of_real ((cmod (v $$ (i, 0)))\<^sup>2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
complex_of_real (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ n. complex_of_real ((cmod (v $$ (i, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
complex_of_real (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2))
complex_of_real (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2))
complex_of_real (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ n. complex_of_real ((cmod (v $$ (i, 0)))\<^sup>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
complex_of_real (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2))
complex_of_real (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2))
complex_of_real (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ n. complex_of_real ((cmod (v $$ (i, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
using sum_prod[of "\<lambda>i. (cmod (u $$ (i , 0)))\<^sup>2" "2^n" "\<lambda>i. (cmod (v $$ (i , 0)))\<^sup>2" "2^m"]
[PROOF STATE]
proof (prove)
using this:
complex_of_real (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ (m + n). complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2))
complex_of_real (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2))
complex_of_real (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2 ^ n. complex_of_real ((cmod (v $$ (i, 0)))\<^sup>2))
(\<Sum>i<2 ^ m * 2 ^ n. complex_of_real ((cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2) * complex_of_real ((cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2)) = (\<Sum>i<2 ^ m. complex_of_real ((cmod (u $$ (i, 0)))\<^sup>2)) * (\<Sum>j<2 ^ n. complex_of_real ((cmod (v $$ (j, 0)))\<^sup>2))

goal (1 subgoal):
 1. (\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
by (smt of_real_eq_iff of_real_mult power_add)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0)))\<^sup>2 * (cmod (v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
have "(\<Sum>i<2^m. (cmod (u $$ (i, 0)))\<^sup>2) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
using assms(1) state_def cpx_vec_length_def
[PROOF STATE]
proof (prove)
using this:
state m u
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1
\<parallel>?v\<parallel> \<equiv> sqrt (\<Sum>i<dim_vec ?v. (cmod (?v $ i))\<^sup>2)

goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = 1

goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = 1

goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
have "(\<Sum>i<2^n. (cmod (v $$ (i, 0)))\<^sup>2) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
using assms(2) state_def cpx_vec_length_def
[PROOF STATE]
proof (prove)
using this:
state n v
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1
\<parallel>?v\<parallel> \<equiv> sqrt (\<Sum>i<dim_vec ?v. (cmod (?v $ i))\<^sup>2)

goal (1 subgoal):
 1. (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1

goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = 1
(\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) = 1
(\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1

goal (1 subgoal):
 1. (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
[PROOF STEP]
show "\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
using c1 c2 assms state_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<2 ^ (m + n). (cmod (u $$ (i div 2 ^ n, 0) * v $$ (i mod 2 ^ n, 0)))\<^sup>2) = (\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2)
(\<Sum>i<2 ^ m. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2 ^ n. (cmod (v $$ (i, 0)))\<^sup>2) = 1
dim_col (u \<Otimes> v) = 1
dim_row (u \<Otimes> v) = 2 ^ (m + n)
state m u
state n v
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
by (auto simp add: cpx_vec_length_def)
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_row_of_tensor_gate:
  assumes "gate m G1" and "gate n G2"
  shows "dim_row (G1 \<Otimes> G2) = 2^(m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (G1 \<Otimes> G2) = 2 ^ (m + n)
[PROOF STEP]
using assms dim_row_tensor_mat gate.dim_row
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
dim_row (?A \<Otimes> ?B) = dim_row ?A * dim_row ?B
gate ?n ?A \<Longrightarrow> dim_row ?A = 2 ^ ?n

goal (1 subgoal):
 1. dim_row (G1 \<Otimes> G2) = 2 ^ (m + n)
[PROOF STEP]
by (simp add: power_add)


[STATEMENT]
lemma tensor_gate_sqr_mat:
  assumes "gate m G1" and "gate n G2"
  shows "square_mat (G1 \<Otimes> G2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_mat (G1 \<Otimes> G2)
[PROOF STEP]
using assms gate.square_mat
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<Longrightarrow> square_mat ?A

goal (1 subgoal):
 1. square_mat (G1 \<Otimes> G2)
[PROOF STEP]
by simp


[STATEMENT]
lemma dim_col_of_one_mat_less_pow:
  assumes "gate m G1" and "gate n G2" and "j < dim_col (1\<^sub>m(dim_col G1 * dim_col G2))"
  shows "j < 2^(m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < 2 ^ (m + n)
[PROOF STEP]
using assms gate_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A

goal (1 subgoal):
 1. j < 2 ^ (m + n)
[PROOF STEP]
by (simp add: power_add)


[STATEMENT]
lemma index_tensor_gate_unitary1:
  assumes "gate m G1" and "gate n G2" and "i < dim_row (1\<^sub>m(dim_col G1 * dim_col G2))" and
"j < dim_col (1\<^sub>m(dim_col G1 * dim_col G2))"
  shows "((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m(dim_col G1 * dim_col G2) $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<And>k. k<2^(m+n) \<Longrightarrow> cnj((G1 \<Otimes> G2) $$ (k,i)) =
cnj(G1 $$ (k div 2^n, i div 2^n)) * cnj(G2 $$ (k mod 2^n, i mod 2^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (k, i)) = cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n))
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (k, i)) = cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n))
[PROOF STEP]
by (simp add: gate_def power_add)
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<And>k. k<2^(m+n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (k,j) =
                                   G1 $$ (k div 2^n, j div 2^n) * G2 $$ (k mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (k, j) = G1 $$ (k div 2 ^ n, j div 2 ^ n) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
using assms(1,2,4)
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (k, j) = G1 $$ (k div 2 ^ n, j div 2 ^ n) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by (simp add: gate_def power_add)
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (?k, j) = G1 $$ (?k div 2 ^ n, j div 2 ^ n) * G2 $$ (?k mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n))
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (?k, j) = G1 $$ (?k div 2 ^ n, j div 2 ^ n) * G2 $$ (?k mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
have "\<And>k. k<2^(m+n) \<Longrightarrow> cnj((G1 \<Otimes> G2) $$ (k,i)) * ((G1 \<Otimes> G2) $$ (k,j)) =
      cnj(G1 $$ (k div 2^n, i div 2^n)) * G1 $$ (k div 2^n, j div 2^n) *
      cnj(G2 $$ (k mod 2^n, i mod 2^n)) * G2 $$ (k mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
using this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n))
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (?k, j) = G1 $$ (?k div 2 ^ n, j div 2 ^ n) * G2 $$ (?k mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j) = cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) * (G1 \<Otimes> G2) $$ (?k, j) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * G1 $$ (?k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (?k mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) * (G1 \<Otimes> G2) $$ (?k, j) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * G1 $$ (?k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (?k mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
have "(\<Sum>k<2^(m+n). cnj((G1 \<Otimes> G2) $$ (k,i)) * ((G1 \<Otimes> G2) $$ (k,j))) =
      (\<Sum>k<2^(m+n). cnj(G1 $$ (k div 2^n, i div 2^n)) * G1 $$ (k div 2^n, j div 2^n) *
                    cnj(G2 $$ (k mod 2^n, i mod 2^n)) * G2 $$ (k mod 2^n, j mod 2^n))"
[PROOF STATE]
proof (prove)
using this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (?k, i)) * (G1 \<Otimes> G2) $$ (?k, j) = cnj (G1 $$ (?k div 2 ^ n, i div 2 ^ n)) * G1 $$ (?k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (?k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (?k mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j)) = (\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j)) = (\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j)) = (\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<dots> =
             (\<Sum>k<2^m. cnj(G1 $$ (k, i div 2^n)) * G1 $$ (k, j div 2^n)) *
             (\<Sum>k<2^n. cnj(G2 $$ (k, i mod 2^n)) * G2 $$ (k, j mod 2^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)) = (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) * (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n))
[PROOF STEP]
using sum_prod[of "\<lambda>x. cnj(G1 $$ (x, i div 2^n)) * G1 $$ (x, j div 2^n)" "2^n"
"\<lambda>x. cnj(G2 $$ (x, i mod 2^n)) * G2 $$ (x, j mod 2^n)" "2^m"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>ia<2 ^ m * 2 ^ n. cnj (G1 $$ (ia div 2 ^ n, i div 2 ^ n)) * G1 $$ (ia div 2 ^ n, j div 2 ^ n) * (cnj (G2 $$ (ia mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (ia mod 2 ^ n, j mod 2 ^ n))) = (\<Sum>ia<2 ^ m. cnj (G1 $$ (ia, i div 2 ^ n)) * G1 $$ (ia, j div 2 ^ n)) * (\<Sum>ja<2 ^ n. cnj (G2 $$ (ja, i mod 2 ^ n)) * G2 $$ (ja, j mod 2 ^ n))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)) = (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) * (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n))
[PROOF STEP]
by (metis (no_types, lifting) power_add semigroup_mult_class.mult.assoc sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)) = (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) * (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). cnj (G1 $$ (k div 2 ^ n, i div 2 ^ n)) * G1 $$ (k div 2 ^ n, j div 2 ^ n) * cnj (G2 $$ (k mod 2 ^ n, i mod 2 ^ n)) * G2 $$ (k mod 2 ^ n, j mod 2 ^ n)) = (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) * (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<2^(m+n).cnj((G1 \<Otimes> G2) $$ (k,i)) * ((G1 \<Otimes> G2) $$ (k,j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j))
[PROOF STEP]
using assms index_matrix_prod[of "i" "(G1 \<Otimes> G2)\<^sup>\<dagger>" "j" "(G1 \<Otimes> G2)"] dagger_def
dim_row_of_tensor_gate tensor_gate_sqr_mat
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
\<lbrakk>i < dim_row G1 \<Otimes> G2\<^sup>\<dagger>; j < dim_col (G1 \<Otimes> G2); dim_col G1 \<Otimes> G2\<^sup>\<dagger> = dim_row (G1 \<Otimes> G2)\<rbrakk> \<Longrightarrow> (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<dim_row (G1 \<Otimes> G2). G1 \<Otimes> G2\<^sup>\<dagger> $$ (i, k) * (G1 \<Otimes> G2) $$ (k, j))
?M\<^sup>\<dagger> \<equiv> Matrix.mat (dim_col ?M) (dim_row ?M) (\<lambda>(i, j). cnj (?M $$ (j, i)))
\<lbrakk>gate ?m ?G1.0; gate ?n ?G2.0\<rbrakk> \<Longrightarrow> dim_row (?G1.0 \<Otimes> ?G2.0) = 2 ^ (?m + ?n)
\<lbrakk>gate ?m ?G1.0; gate ?n ?G2.0\<rbrakk> \<Longrightarrow> square_mat (?G1.0 \<Otimes> ?G2.0)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j)) = (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) * (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n))
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j))
[PROOF STEP]
have "((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i,j) =
              (\<Sum>k1<2^m. cnj(G1 $$ (k1, i div 2^n)) * G1 $$ (k1, j div 2^n)) *
              (\<Sum>k2<2^n. cnj(G2 $$ (k2, i mod 2^n)) * G2 $$ (k2, j mod 2^n))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j)) = (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) * (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n))
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k<2 ^ (m + n). cnj ((G1 \<Otimes> G2) $$ (k, i)) * (G1 \<Otimes> G2) $$ (k, j))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k1<2 ^ m. cnj (G1 $$ (k1, i div 2 ^ n)) * G1 $$ (k1, j div 2 ^ n)) * (\<Sum>k2<2 ^ n. cnj (G2 $$ (k2, i mod 2 ^ n)) * G2 $$ (k2, j mod 2 ^ n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k1<2 ^ m. cnj (G1 $$ (k1, i div 2 ^ n)) * G1 $$ (k1, j div 2 ^ n)) * (\<Sum>k2<2 ^ n. cnj (G2 $$ (k2, i mod 2 ^ n)) * G2 $$ (k2, j mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k1<2 ^ m. cnj (G1 $$ (k1, i div 2 ^ n)) * G1 $$ (k1, j div 2 ^ n)) * (\<Sum>k2<2 ^ n. cnj (G2 $$ (k2, i mod 2 ^ n)) * G2 $$ (k2, j mod 2 ^ n))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "(\<Sum>k<2^m. cnj(G1 $$ (k, i div 2^n))* G1 $$ (k, j div 2^n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2^n, j div 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
using assms gate_def dagger_def index_matrix_prod[of "i div 2^n" "G1\<^sup>\<dagger>" "j div 2^n" "G1"]
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
?M\<^sup>\<dagger> \<equiv> Matrix.mat (dim_col ?M) (dim_row ?M) (\<lambda>(i, j). cnj (?M $$ (j, i)))
\<lbrakk>i div 2 ^ n < dim_row G1\<^sup>\<dagger>; j div 2 ^ n < dim_col G1; dim_col G1\<^sup>\<dagger> = dim_row G1\<rbrakk> \<Longrightarrow> (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = (\<Sum>k<dim_row G1. G1\<^sup>\<dagger> $$ (i div 2 ^ n, k) * G1 $$ (k, j div 2 ^ n))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
by (simp add: less_mult_imp_div_less power_add)
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<dots> = 1\<^sub>m(2^m) $$ (i div 2^n, j div 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
using assms(1,2) gate_def unitary_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
unitary ?M \<equiv> ?M\<^sup>\<dagger> * ?M = 1\<^sub>m (dim_col ?M) \<and> ?M * ?M\<^sup>\<dagger> = 1\<^sub>m (dim_row ?M)

goal (1 subgoal):
 1. (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "(\<Sum>k<2^n. cnj(G2 $$ (k, i mod 2^n))* G2 $$ (k, j mod 2^n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
using assms(1,2) gate_def dagger_def index_matrix_prod[of "i mod 2^n" "G2\<^sup>\<dagger>" "j mod 2^n" "G2"]
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
?M\<^sup>\<dagger> \<equiv> Matrix.mat (dim_col ?M) (dim_row ?M) (\<lambda>(i, j). cnj (?M $$ (j, i)))
\<lbrakk>i mod 2 ^ n < dim_row G2\<^sup>\<dagger>; j mod 2 ^ n < dim_col G2; dim_col G2\<^sup>\<dagger> = dim_row G2\<rbrakk> \<Longrightarrow> (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n) = (\<Sum>k<dim_row G2. G2\<^sup>\<dagger> $$ (i mod 2 ^ n, k) * G2 $$ (k, j mod 2 ^ n))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<dots> = 1\<^sub>m(2^n) $$ (i mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
using assms(1,2) gate_def unitary_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
unitary ?M \<equiv> ?M\<^sup>\<dagger> * ?M = 1\<^sub>m (dim_col ?M) \<and> ?M * ?M\<^sup>\<dagger> = 1\<^sub>m (dim_row ?M)

goal (1 subgoal):
 1. (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k1<2 ^ m. cnj (G1 $$ (k1, i div 2 ^ n)) * G1 $$ (k1, j div 2 ^ n)) * (\<Sum>k2<2 ^ n. cnj (G2 $$ (k2, i mod 2 ^ n)) * G2 $$ (k2, j mod 2 ^ n))
(\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n)
(G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
(\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n)
(G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
have "((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i,j) = 1\<^sub>m (2^m) $$ (i div 2^n, j div 2^n) * 1\<^sub>m (2^n) $$ (i mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
using this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = (\<Sum>k1<2 ^ m. cnj (G1 $$ (k1, i div 2 ^ n)) * G1 $$ (k1, j div 2 ^ n)) * (\<Sum>k2<2 ^ n. cnj (G2 $$ (k2, i mod 2 ^ n)) * G2 $$ (k2, j mod 2 ^ n))
(\<Sum>k<2 ^ m. cnj (G1 $$ (k, i div 2 ^ n)) * G1 $$ (k, j div 2 ^ n)) = (G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n)
(G1\<^sup>\<dagger> * G1) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
(\<Sum>k<2 ^ n. cnj (G2 $$ (k, i mod 2 ^ n)) * G2 $$ (k, j mod 2 ^ n)) = (G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n)
(G2\<^sup>\<dagger> * G2) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
using assms assms(3,4) gate_def index_one_mat_div_mod[of "i" "m" "n" "j"]
[PROOF STATE]
proof (prove)
using this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
\<lbrakk>i < 2 ^ (m + n); j < 2 ^ (m + n)\<rbrakk> \<Longrightarrow> 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ (m + n)) $$ (i, j)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
by(simp add: power_add)
[PROOF STATE]
proof (state)
this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_gate_unitary1 [simp]:
  assumes "gate m G1" and "gate n G2"
  shows "(G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2) = 1\<^sub>m(dim_col G1 * dim_col G2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2) = 1\<^sub>m (dim_col G1 * dim_col G2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
 2. dim_row (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
 3. dim_col (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
show "dim_row ((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_row (1\<^sub>m(dim_col G1 * dim_col G2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
 2. dim_col (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
show "dim_col ((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_col (1\<^sub>m(dim_col G1 * dim_col G2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_col (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
assume "i < dim_row (1\<^sub>m(dim_col G1 * dim_col G2))" and "j < dim_col (1\<^sub>m(dim_col G1 * dim_col G2))"
[PROOF STATE]
proof (state)
this:
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
thus "((G1 \<Otimes> G2)\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m(dim_col G1 * dim_col G2) $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
using assms index_tensor_gate_unitary1
[PROOF STATE]
proof (prove)
using this:
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate m G1
gate n G2
\<lbrakk>gate ?m ?G1.0; gate ?n ?G2.0; ?i < dim_row (1\<^sub>m (dim_col ?G1.0 * dim_col ?G2.0)); ?j < dim_col (1\<^sub>m (dim_col ?G1.0 * dim_col ?G2.0))\<rbrakk> \<Longrightarrow> (?G1.0 \<Otimes> ?G2.0\<^sup>\<dagger> * (?G1.0 \<Otimes> ?G2.0)) $$ (?i, ?j) = 1\<^sub>m (dim_col ?G1.0 * dim_col ?G2.0) $$ (?i, ?j)

goal (1 subgoal):
 1. (G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G1 \<Otimes> G2\<^sup>\<dagger> * (G1 \<Otimes> G2)) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma index_tensor_gate_unitary2 [simp]:
  assumes "gate m G1" and "gate n G2" and "i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))" and
"j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))"
  shows "((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) $$ (i, j) = 1\<^sub>m(dim_col G1 * dim_col G2) $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<And>k. k<2^(m+n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i,k) =
G1 $$ (i div 2^n, k div 2^n) * G2 $$ (i mod 2^n, k mod 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, k) = G1 $$ (i div 2 ^ n, k div 2 ^ n) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n)
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, k) = G1 $$ (i div 2 ^ n, k div 2 ^ n) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n)
[PROOF STEP]
by (simp add: gate_def power_add)
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<And>k. k<2^(m+n) \<Longrightarrow> cnj((G1 \<Otimes> G2) $$ (j,k)) =
cnj(G1 $$ (j div 2^n, k div 2^n)) * cnj(G2 $$ (j mod 2^n, k mod 2^n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (j, k)) = cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))
[PROOF STEP]
using assms(1,2,4)
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>k. k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (j, k)) = cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))
[PROOF STEP]
by (simp add: gate_def power_add)
[PROOF STATE]
proof (state)
this:
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (j, ?k)) = cnj (G1 $$ (j div 2 ^ n, ?k div 2 ^ n)) * cnj (G2 $$ (j mod 2 ^ n, ?k mod 2 ^ n))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n)
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (j, ?k)) = cnj (G1 $$ (j div 2 ^ n, ?k div 2 ^ n)) * cnj (G2 $$ (j mod 2 ^ n, ?k mod 2 ^ n))
[PROOF STEP]
have "\<And>k. k\<in>{..<2^(m+n)} \<Longrightarrow> (G1 \<Otimes> G2) $$ (i,k) * cnj((G1 \<Otimes> G2) $$ (j,k)) =
                         G1 $$ (i div 2^n, k div 2^n) * cnj(G1 $$ (j div 2^n, k div 2^n)) *
                         G2 $$ (i mod 2^n, k mod 2^n) * cnj(G2 $$ (j mod 2^n, k mod 2^n))"
[PROOF STATE]
proof (prove)
using this:
?k < 2 ^ (m + n) \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n)
?k < 2 ^ (m + n) \<Longrightarrow> cnj ((G1 \<Otimes> G2) $$ (j, ?k)) = cnj (G1 $$ (j div 2 ^ n, ?k div 2 ^ n)) * cnj (G2 $$ (j mod 2 ^ n, ?k mod 2 ^ n))

goal (1 subgoal):
 1. \<And>k. k \<in> {..<2 ^ (m + n)} \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k)) = G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?k \<in> {..<2 ^ (m + n)} \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) * cnj ((G1 \<Otimes> G2) $$ (j, ?k)) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, ?k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, ?k mod 2 ^ n))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?k \<in> {..<2 ^ (m + n)} \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) * cnj ((G1 \<Otimes> G2) $$ (j, ?k)) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, ?k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, ?k mod 2 ^ n))
[PROOF STEP]
have "(\<Sum>k<2^(m+n). (G1 \<Otimes> G2) $$ (i,k) * cnj((G1 \<Otimes> G2) $$ (j,k))) =
      (\<Sum>k<2^(m+n). G1 $$ (i div 2^n, k div 2^n) * cnj(G1 $$ (j div 2^n, k div 2^n)) *
      G2 $$ (i mod 2^n, k mod 2^n) * cnj(G2 $$ (j mod 2^n, k mod 2^n)))"
[PROOF STATE]
proof (prove)
using this:
?k \<in> {..<2 ^ (m + n)} \<Longrightarrow> (G1 \<Otimes> G2) $$ (i, ?k) * cnj ((G1 \<Otimes> G2) $$ (j, ?k)) = G1 $$ (i div 2 ^ n, ?k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, ?k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, ?k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, ?k mod 2 ^ n))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k))) = (\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k))) = (\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k))) = (\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<dots> =
             (\<Sum>k<2^m. G1 $$ (i div 2^n, k) * cnj(G1 $$ (j div 2^n, k))) *
             (\<Sum>k<2^n. G2 $$ (i mod 2^n, k) * cnj(G2 $$ (j mod 2^n, k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
[PROOF STEP]
using sum_prod[of "\<lambda>k. G1 $$ (i div 2^n, k) * cnj(G1 $$ (j div 2^n, k))" "2^n"
                        "\<lambda>k. G2 $$ (i mod 2^n, k) * cnj(G2 $$ (j mod 2^n, k))" "2^m"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>ia<2 ^ m * 2 ^ n. G1 $$ (i div 2 ^ n, ia div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, ia div 2 ^ n)) * (G2 $$ (i mod 2 ^ n, ia mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, ia mod 2 ^ n)))) = (\<Sum>ia<2 ^ m. G1 $$ (i div 2 ^ n, ia) * cnj (G1 $$ (j div 2 ^ n, ia))) * (\<Sum>ja<2 ^ n. G2 $$ (i mod 2 ^ n, ja) * cnj (G2 $$ (j mod 2 ^ n, ja)))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
[PROOF STEP]
by (metis (no_types, lifting) power_add semigroup_mult_class.mult.assoc sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ (m + n). G1 $$ (i div 2 ^ n, k div 2 ^ n) * cnj (G1 $$ (j div 2 ^ n, k div 2 ^ n)) * G2 $$ (i mod 2 ^ n, k mod 2 ^ n) * cnj (G2 $$ (j mod 2 ^ n, k mod 2 ^ n))) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) $$ (i, j) = (\<Sum>k<2^(m+n). (G1 \<Otimes> G2) $$ (i,k) * cnj((G1 \<Otimes> G2) $$ (j,k)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k)))
[PROOF STEP]
using assms index_matrix_prod[of "i" "(G1 \<Otimes> G2)" "j" "(G1 \<Otimes> G2)\<^sup>\<dagger>"] dagger_def
dim_row_of_tensor_gate tensor_gate_sqr_mat
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
\<lbrakk>i < dim_row (G1 \<Otimes> G2); j < dim_col G1 \<Otimes> G2\<^sup>\<dagger>; dim_col (G1 \<Otimes> G2) = dim_row G1 \<Otimes> G2\<^sup>\<dagger>\<rbrakk> \<Longrightarrow> ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<dim_row G1 \<Otimes> G2\<^sup>\<dagger>. (G1 \<Otimes> G2) $$ (i, k) * G1 \<Otimes> G2\<^sup>\<dagger> $$ (k, j))
?M\<^sup>\<dagger> \<equiv> Matrix.mat (dim_col ?M) (dim_row ?M) (\<lambda>(i, j). cnj (?M $$ (j, i)))
\<lbrakk>gate ?m ?G1.0; gate ?n ?G2.0\<rbrakk> \<Longrightarrow> dim_row (?G1.0 \<Otimes> ?G2.0) = 2 ^ (?m + ?n)
\<lbrakk>gate ?m ?G1.0; gate ?n ?G2.0\<rbrakk> \<Longrightarrow> square_mat (?G1.0 \<Otimes> ?G2.0)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k))) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k)))
[PROOF STEP]
have "((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) $$ (i,j) =
             (\<Sum>k<2^m. G1 $$ (i div 2^n, k) * cnj(G1 $$ (j div 2^n, k))) *
             (\<Sum>k<2^n. G2 $$ (i mod 2^n, k) * cnj(G2 $$ (j mod 2^n, k)))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k))) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ (m + n). (G1 \<Otimes> G2) $$ (i, k) * cnj ((G1 \<Otimes> G2) $$ (j, k)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "(\<Sum>k<2^m. G1 $$ (i div 2^n, k) * cnj(G1 $$ (j div 2^n, k))) = (G1 * (G1\<^sup>\<dagger>)) $$ (i div 2^n, j div 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) = (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
using assms gate_def dagger_def index_matrix_prod[of "i div 2^n" "G1" "j div 2^n" "G1\<^sup>\<dagger>"]
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
?M\<^sup>\<dagger> \<equiv> Matrix.mat (dim_col ?M) (dim_row ?M) (\<lambda>(i, j). cnj (?M $$ (j, i)))
\<lbrakk>i div 2 ^ n < dim_row G1; j div 2 ^ n < dim_col G1\<^sup>\<dagger>; dim_col G1 = dim_row G1\<^sup>\<dagger>\<rbrakk> \<Longrightarrow> (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = (\<Sum>k<dim_row G1\<^sup>\<dagger>. G1 $$ (i div 2 ^ n, k) * G1\<^sup>\<dagger> $$ (k, j div 2 ^ n))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) = (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
by (simp add: less_mult_imp_div_less power_add)
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) = (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) = (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<dots> = 1\<^sub>m(2^m) $$ (i div 2^n, j div 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
using assms(1,2) gate_def unitary_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
unitary ?M \<equiv> ?M\<^sup>\<dagger> * ?M = 1\<^sub>m (dim_col ?M) \<and> ?M * ?M\<^sup>\<dagger> = 1\<^sub>m (dim_row ?M)

goal (1 subgoal):
 1. (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "(\<Sum>k<2^n. G2 $$ (i mod 2^n, k) * cnj(G2 $$ (j mod 2^n, k))) = (G2 * (G2\<^sup>\<dagger>)) $$ (i mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k))) = (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
using assms(1,2) gate_def dagger_def index_matrix_prod[of "i mod 2^n" "G2" "j mod 2^n" "G2\<^sup>\<dagger>"]
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
?M\<^sup>\<dagger> \<equiv> Matrix.mat (dim_col ?M) (dim_row ?M) (\<lambda>(i, j). cnj (?M $$ (j, i)))
\<lbrakk>i mod 2 ^ n < dim_row G2; j mod 2 ^ n < dim_col G2\<^sup>\<dagger>; dim_col G2 = dim_row G2\<^sup>\<dagger>\<rbrakk> \<Longrightarrow> (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n) = (\<Sum>k<dim_row G2\<^sup>\<dagger>. G2 $$ (i mod 2 ^ n, k) * G2\<^sup>\<dagger> $$ (k, j mod 2 ^ n))

goal (1 subgoal):
 1. (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k))) = (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k))) = (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k))) = (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
have "\<dots> = 1\<^sub>m(2^n) $$ (i mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
using assms(1,2) gate_def unitary_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
unitary ?M \<equiv> ?M\<^sup>\<dagger> * ?M = 1\<^sub>m (dim_col ?M) \<and> ?M * ?M\<^sup>\<dagger> = 1\<^sub>m (dim_row ?M)

goal (1 subgoal):
 1. (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
(\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) = (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n)
(G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
(\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k))) = (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n)
(G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
have "((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) $$ (i,j) = 1\<^sub>m(2^m) $$ (i div 2^n, j div 2^n) * 1\<^sub>m(2^n) $$ (i mod 2^n, j mod 2^n)"
[PROOF STATE]
proof (prove)
using this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = (\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) * (\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k)))
(\<Sum>k<2 ^ m. G1 $$ (i div 2 ^ n, k) * cnj (G1 $$ (j div 2 ^ n, k))) = (G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n)
(G1 * G1\<^sup>\<dagger>) $$ (i div 2 ^ n, j div 2 ^ n) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n)
(\<Sum>k<2 ^ n. G2 $$ (i mod 2 ^ n, k) * cnj (G2 $$ (j mod 2 ^ n, k))) = (G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n)
(G2 * G2\<^sup>\<dagger>) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
using assms gate_def index_one_mat_div_mod[of "i" "m" "n" "j"]
[PROOF STATE]
proof (prove)
using this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n)
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A
\<lbrakk>i < 2 ^ (m + n); j < 2 ^ (m + n)\<rbrakk> \<Longrightarrow> 1\<^sub>m (2 ^ m) $$ (i div 2 ^ n, j div 2 ^ n) * 1\<^sub>m (2 ^ n) $$ (i mod 2 ^ n, j mod 2 ^ n) = 1\<^sub>m (2 ^ (m + n)) $$ (i, j)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
by(simp add: power_add)
[PROOF STATE]
proof (state)
this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_gate_unitary2 [simp]:
  assumes "gate m G1" and "gate n G2"
  shows "(G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>) = 1\<^sub>m(dim_col G1 * dim_col G2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger> = 1\<^sub>m (dim_col G1 * dim_col G2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
 2. dim_row ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
 3. dim_col ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
show "dim_row ((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) = dim_row(1\<^sub>m (dim_col G1 * dim_col G2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
using assms gate_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A

goal (1 subgoal):
 1. dim_row ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_row ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_row (1\<^sub>m (dim_col G1 * dim_col G2))

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
 2. dim_col ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
show "dim_col ((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) = dim_col (1\<^sub>m(dim_col G1 * dim_col G2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
using assms gate_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A

goal (1 subgoal):
 1. dim_col ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_col ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) = dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
assume "i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))" and "j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))"
[PROOF STATE]
proof (state)
this:
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2)); j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))\<rbrakk> \<Longrightarrow> ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
thus "((G1 \<Otimes> G2) * ((G1 \<Otimes> G2)\<^sup>\<dagger>)) $$ (i, j) = 1\<^sub>m(dim_col G1 * dim_col G2) $$ (i, j)"
[PROOF STATE]
proof (prove)
using this:
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
using assms index_tensor_gate_unitary2
[PROOF STATE]
proof (prove)
using this:
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
j < dim_col (1\<^sub>m (dim_col G1 * dim_col G2))
gate m G1
gate n G2
\<lbrakk>gate ?m ?G1.0; gate ?n ?G2.0; ?i < dim_row (1\<^sub>m (dim_col ?G1.0 * dim_col ?G2.0)); ?j < dim_col (1\<^sub>m (dim_col ?G1.0 * dim_col ?G2.0))\<rbrakk> \<Longrightarrow> ((?G1.0 \<Otimes> ?G2.0) * ?G1.0 \<Otimes> ?G2.0\<^sup>\<dagger>) $$ (?i, ?j) = 1\<^sub>m (dim_col ?G1.0 * dim_col ?G2.0) $$ (?i, ?j)

goal (1 subgoal):
 1. ((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
((G1 \<Otimes> G2) * G1 \<Otimes> G2\<^sup>\<dagger>) $$ (i, j) = 1\<^sub>m (dim_col G1 * dim_col G2) $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_gate [simp]:
  assumes "gate m G1" and "gate n G2"
  shows "gate (m + n) (G1 \<Otimes> G2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gate (m + n) (G1 \<Otimes> G2)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dim_row (G1 \<Otimes> G2) = 2 ^ (m + n)
 2. square_mat (G1 \<Otimes> G2)
 3. unitary (G1 \<Otimes> G2)
[PROOF STEP]
show "dim_row (G1 \<Otimes> G2) = 2^(m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (G1 \<Otimes> G2) = 2 ^ (m + n)
[PROOF STEP]
using assms dim_row_tensor_mat gate.dim_row
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
dim_row (?A \<Otimes> ?B) = dim_row ?A * dim_row ?B
gate ?n ?A \<Longrightarrow> dim_row ?A = 2 ^ ?n

goal (1 subgoal):
 1. dim_row (G1 \<Otimes> G2) = 2 ^ (m + n)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
dim_row (G1 \<Otimes> G2) = 2 ^ (m + n)

goal (2 subgoals):
 1. square_mat (G1 \<Otimes> G2)
 2. unitary (G1 \<Otimes> G2)
[PROOF STEP]
show "square_mat (G1 \<Otimes> G2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. square_mat (G1 \<Otimes> G2)
[PROOF STEP]
using assms gate.square_mat
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
gate ?n ?A \<Longrightarrow> square_mat ?A

goal (1 subgoal):
 1. square_mat (G1 \<Otimes> G2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
square_mat (G1 \<Otimes> G2)

goal (1 subgoal):
 1. unitary (G1 \<Otimes> G2)
[PROOF STEP]
thus "unitary (G1 \<Otimes> G2)"
[PROOF STATE]
proof (prove)
using this:
square_mat (G1 \<Otimes> G2)

goal (1 subgoal):
 1. unitary (G1 \<Otimes> G2)
[PROOF STEP]
using assms unitary_def
[PROOF STATE]
proof (prove)
using this:
square_mat (G1 \<Otimes> G2)
gate m G1
gate n G2
unitary ?M \<equiv> ?M\<^sup>\<dagger> * ?M = 1\<^sub>m (dim_col ?M) \<and> ?M * ?M\<^sup>\<dagger> = 1\<^sub>m (dim_row ?M)

goal (1 subgoal):
 1. unitary (G1 \<Otimes> G2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
unitary (G1 \<Otimes> G2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma best_division_abs: "(n::int) > 0 \<Longrightarrow> \<exists> k. 2 * \<bar>a - k*n\<bar> \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
assume a: "n > 0"
[PROOF STATE]
proof (state)
this:
0 < n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
define k where "k = a div n"
[PROOF STATE]
proof (state)
this:
k = a div n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
have h: "a - k * n = a mod n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - k * n = a mod n
[PROOF STEP]
by (simp add: div_mult_mod_eq algebra_simps k_def)
[PROOF STATE]
proof (state)
this:
a - k * n = a mod n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a - k * n = a mod n

goal (1 subgoal):
 1. \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
proof (cases "2 * (a mod n) \<le> n")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>a - k * n = a mod n; 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
 2. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
2 * (a mod n) \<le> n

goal (2 subgoals):
 1. \<lbrakk>a - k * n = a mod n; 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
 2. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence "2 * \<bar>a - k*n\<bar> \<le> n"
[PROOF STATE]
proof (prove)
using this:
2 * (a mod n) \<le> n

goal (1 subgoal):
 1. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
using h pos_mod_sign a
[PROOF STATE]
proof (prove)
using this:
2 * (a mod n) \<le> n
a - k * n = a mod n
(0::?'a) < ?b \<Longrightarrow> (0::?'a) \<le> ?a mod ?b
0 < n

goal (1 subgoal):
 1. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * \<bar>a - k * n\<bar> \<le> n

goal (2 subgoals):
 1. \<lbrakk>a - k * n = a mod n; 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
 2. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * \<bar>a - k * n\<bar> \<le> n

goal (1 subgoal):
 1. \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> 2 * (a mod n) \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence "2 * (n - a mod n) \<le> n"
[PROOF STATE]
proof (prove)
using this:
\<not> 2 * (a mod n) \<le> n

goal (1 subgoal):
 1. 2 * (n - a mod n) \<le> n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * (n - a mod n) \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
have "a - (k+1)*n = a mod n - n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a - (k + 1) * n = a mod n - n
[PROOF STEP]
using h
[PROOF STATE]
proof (prove)
using this:
a - k * n = a mod n

goal (1 subgoal):
 1. a - (k + 1) * n = a mod n - n
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
a - (k + 1) * n = a mod n - n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
hence "2 * \<bar>a - (k+1)*n\<bar> \<le> n"
[PROOF STATE]
proof (prove)
using this:
a - (k + 1) * n = a mod n - n

goal (1 subgoal):
 1. 2 * \<bar>a - (k + 1) * n\<bar> \<le> n
[PROOF STEP]
using h pos_mod_bound[of n a] a False
[PROOF STATE]
proof (prove)
using this:
a - (k + 1) * n = a mod n - n
a - k * n = a mod n
0 < n \<Longrightarrow> a mod n < n
0 < n
\<not> 2 * (a mod n) \<le> n

goal (1 subgoal):
 1. 2 * \<bar>a - (k + 1) * n\<bar> \<le> n
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
2 * \<bar>a - (k + 1) * n\<bar> \<le> n

goal (1 subgoal):
 1. \<lbrakk>a - k * n = a mod n; \<not> 2 * (a mod n) \<le> n\<rbrakk> \<Longrightarrow> \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 * \<bar>a - (k + 1) * n\<bar> \<le> n

goal (1 subgoal):
 1. \<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>k. 2 * \<bar>a - k * n\<bar> \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_sum4sq_int: "sum4sq_int(a,b,c,d) * sum4sq_int(p,q,r,s) =
  sum4sq_int(a*p+b*q+c*r+d*s, a*q-b*p-c*s+d*r,
         a*r+b*s-c*p-d*q, a*s-b*r+c*q-d*p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum4sq_int (a, b, c, d) * sum4sq_int (p, q, r, s) = sum4sq_int (a * p + b * q + c * r + d * s, a * q - b * p - c * s + d * r, a * r + b * s - c * p - d * q, a * s - b * r + c * q - d * p)
[PROOF STEP]
by (unfold sum4sq_int_def, simp add: eval_nat_numeral field_simps)


[STATEMENT]
lemma sum4sq_int_nat_eq: "sum4sq_nat a b c d = sum4sq_int (a, b, c, d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (sum4sq_nat a b c d) = sum4sq_int (int a, int b, int c, int d)
[PROOF STEP]
unfolding sum4sq_nat_def sum4sq_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int (a\<^sup>2 + b\<^sup>2 + c\<^sup>2 + d\<^sup>2) = (case (int a, int b, int c, int d) of (a, b, c, d) \<Rightarrow> a\<^sup>2 + b\<^sup>2 + c\<^sup>2 + d\<^sup>2)
[PROOF STEP]
by simp


[STATEMENT]
lemma is_sum4sq_int_nat_eq: "is_sum4sq_nat n = is_sum4sq_int (int n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_sum4sq_nat n = is_sum4sq_int (int n)
[PROOF STEP]
unfolding is_sum4sq_nat_def is_sum4sq_int_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>a b c d. n = sum4sq_nat a b c d) = (\<exists>a b c d. int n = sum4sq_int (a, b, c, d))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a b c d. n = sum4sq_nat a b c d \<Longrightarrow> \<exists>a b c d. int n = sum4sq_int (a, b, c, d)
 2. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
assume "\<exists>a b c d. n = sum4sq_nat a b c d"
[PROOF STATE]
proof (state)
this:
\<exists>a b c d. n = sum4sq_nat a b c d

goal (2 subgoals):
 1. \<exists>a b c d. n = sum4sq_nat a b c d \<Longrightarrow> \<exists>a b c d. int n = sum4sq_int (a, b, c, d)
 2. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
thus "\<exists>a b c d. int n = sum4sq_int (a, b, c, d)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b c d. n = sum4sq_nat a b c d

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d)
[PROOF STEP]
using sum4sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
\<exists>a b c d. n = sum4sq_nat a b c d
int (sum4sq_nat ?a ?b ?c ?d) = sum4sq_int (int ?a, int ?b, int ?c, int ?d)

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>a b c d. int n = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
assume "\<exists>a b c d. int n = sum4sq_int (a, b, c, d)"
[PROOF STATE]
proof (state)
this:
\<exists>a b c d. int n = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a b c d. int n = sum4sq_int (a, b, c, d)
[PROOF STEP]
obtain a b c d where "int n = sum4sq_int (a, b, c, d)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a b c d. int n = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. (\<And>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
int n = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
hence "int n = sum4sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>), int (nat \<bar>c\<bar>), int (nat \<bar>d\<bar>))"
[PROOF STATE]
proof (prove)
using this:
int n = sum4sq_int (a, b, c, d)

goal (1 subgoal):
 1. int n = sum4sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>), int (nat \<bar>c\<bar>), int (nat \<bar>d\<bar>))
[PROOF STEP]
unfolding sum4sq_int_def
[PROOF STATE]
proof (prove)
using this:
int n = (case (a, b, c, d) of (a, b, c, d) \<Rightarrow> a\<^sup>2 + b\<^sup>2 + c\<^sup>2 + d\<^sup>2)

goal (1 subgoal):
 1. int n = (case (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>), int (nat \<bar>c\<bar>), int (nat \<bar>d\<bar>)) of (a, b, c, d) \<Rightarrow> a\<^sup>2 + b\<^sup>2 + c\<^sup>2 + d\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int n = sum4sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>), int (nat \<bar>c\<bar>), int (nat \<bar>d\<bar>))

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
hence "int n = int (sum4sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>) (nat \<bar>c\<bar>) (nat \<bar>d\<bar>))"
[PROOF STATE]
proof (prove)
using this:
int n = sum4sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>), int (nat \<bar>c\<bar>), int (nat \<bar>d\<bar>))

goal (1 subgoal):
 1. int n = int (sum4sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>) (nat \<bar>c\<bar>) (nat \<bar>d\<bar>))
[PROOF STEP]
using sum4sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
int n = sum4sq_int (int (nat \<bar>a\<bar>), int (nat \<bar>b\<bar>), int (nat \<bar>c\<bar>), int (nat \<bar>d\<bar>))
int (sum4sq_nat ?a ?b ?c ?d) = sum4sq_int (int ?a, int ?b, int ?c, int ?d)

goal (1 subgoal):
 1. int n = int (sum4sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>) (nat \<bar>c\<bar>) (nat \<bar>d\<bar>))
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
int n = int (sum4sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>) (nat \<bar>c\<bar>) (nat \<bar>d\<bar>))

goal (1 subgoal):
 1. \<exists>a b c d. int n = sum4sq_int (a, b, c, d) \<Longrightarrow> \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
thus "\<exists>a b c d. n = sum4sq_nat a b c d"
[PROOF STATE]
proof (prove)
using this:
int n = int (sum4sq_nat (nat \<bar>a\<bar>) (nat \<bar>b\<bar>) (nat \<bar>c\<bar>) (nat \<bar>d\<bar>))

goal (1 subgoal):
 1. \<exists>a b c d. n = sum4sq_nat a b c d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a b c d. n = sum4sq_nat a b c d

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_mult_sum4sq_int: "is_sum4sq_int x \<Longrightarrow> is_sum4sq_int y \<Longrightarrow> is_sum4sq_int (x*y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_sum4sq_int x; is_sum4sq_int y\<rbrakk> \<Longrightarrow> is_sum4sq_int (x * y)
[PROOF STEP]
by (unfold is_sum4sq_int_def, auto simp only: mult_sum4sq_int, blast)


[STATEMENT]
lemma is_mult_sum4sq_nat: "is_sum4sq_nat x \<Longrightarrow> is_sum4sq_nat y \<Longrightarrow> is_sum4sq_nat (x*y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_sum4sq_nat x; is_sum4sq_nat y\<rbrakk> \<Longrightarrow> is_sum4sq_nat (x * y)
[PROOF STEP]
using is_mult_sum4sq_int is_sum4sq_int_nat_eq
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_sum4sq_int ?x; is_sum4sq_int ?y\<rbrakk> \<Longrightarrow> is_sum4sq_int (?x * ?y)
is_sum4sq_nat ?n = is_sum4sq_int (int ?n)

goal (1 subgoal):
 1. \<lbrakk>is_sum4sq_nat x; is_sum4sq_nat y\<rbrakk> \<Longrightarrow> is_sum4sq_nat (x * y)
[PROOF STEP]
by simp