[STATEMENT]
lemma mat_tensor_prod_2_prelim [simp]:
  assumes "state 1 v" and "state 1 w"
  shows "v \<Otimes> w = mat_of_cols_list 4
[[v $$ (0,0) * w $$ (0,0), v $$ (0,0) * w $$ (1,0), v $$ (1,0) * w $$ (0,0), v $$ (1,0) * w $$ (1,0)]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<Otimes> w = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]); j < dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]] $$ (i, j)
 2. dim_row (v \<Otimes> w) = dim_row (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])
 3. dim_col (v \<Otimes> w) = dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])
[PROOF STEP]
define u where "u = mat_of_cols_list 4
[[v $$ (0,0) * w $$ (0,0), v $$ (0,0) * w $$ (1,0), v $$ (1,0) * w $$ (0,0), v $$ (1,0) * w $$ (1,0)]]"
[PROOF STATE]
proof (state)
this:
u = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]); j < dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]] $$ (i, j)
 2. dim_row (v \<Otimes> w) = dim_row (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])
 3. dim_col (v \<Otimes> w) = dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]
[PROOF STEP]
show f1:"dim_row (v \<Otimes> w) = dim_row u"
[PROOF STATE]
proof (prove)
using this:
u = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]

goal (1 subgoal):
 1. dim_row (v \<Otimes> w) = dim_row u
[PROOF STEP]
using assms state_def mat_of_cols_list_def tensor_mat_def
[PROOF STATE]
proof (prove)
using this:
u = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]
state 1 v
state 1 w
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1
Tensor.mat_of_cols_list ?nr ?cs = Matrix.mat ?nr (length ?cs) (\<lambda>(i, j). ?cs ! j ! i)
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))

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

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]); j < dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]] $$ (i, j)
 2. dim_col (v \<Otimes> w) = dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])
[PROOF STEP]
show f2:"dim_col (v \<Otimes> w) = dim_col u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (v \<Otimes> w) = dim_col u
[PROOF STEP]
using assms state_def mat_of_cols_list_def tensor_mat_def u_def
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1
Tensor.mat_of_cols_list ?nr ?cs = Matrix.mat ?nr (length ?cs) (\<lambda>(i, j). ?cs ! j ! i)
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))
u = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]); j < dim_col (Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]])\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]] $$ (i, j)
[PROOF STEP]
show "\<And>i j. i < dim_row u \<Longrightarrow> j < dim_col u \<Longrightarrow>  (v \<Otimes> w) $$ (i, j) = u $$ (i, j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
using u_def tensor_mat_def assms state_def
[PROOF STATE]
proof (prove)
using this:
u = Tensor.mat_of_cols_list 4 [[v $$ (0, 0) * w $$ (0, 0), v $$ (0, 0) * w $$ (1, 0), v $$ (1, 0) * w $$ (0, 0), v $$ (1, 0) * w $$ (1, 0)]]
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))
state 1 v
state 1 w
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. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim_row u; ?j < dim_col u\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (?i, ?j) = u $$ (?i, ?j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_tensor_prod_2_col [simp]:
  assumes "state 1 v" and "state 1 w"
  shows "Matrix.col (v \<Otimes> w) 0 = Matrix.col v 0 \<otimes> Matrix.col w 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.col (v \<Otimes> w) 0 = Matrix.col v 0 \<otimes> Matrix.col w 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
 2. dim_vec (Matrix.col (v \<Otimes> w) 0) = dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0)
[PROOF STEP]
show f1:"dim_vec (Matrix.col (v \<Otimes> w) 0) = dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Matrix.col (v \<Otimes> w) 0) = dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0)
[PROOF STEP]
using assms vec_tensor_prod_2_bis
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = Matrix.vec 4 (\<lambda>i. if i = 0 then ?v $ 0 * ?w $ 0 else if i = 3 then ?v $ 1 * ?w $ 1 else if i = 1 then ?v $ 0 * ?w $ 1 else ?v $ 1 * ?w $ 0)

goal (1 subgoal):
 1. dim_vec (Matrix.col (v \<Otimes> w) 0) = dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0)
[PROOF STEP]
by (smt Tensor.mat_of_cols_list_def dim_col dim_row_mat(1) dim_vec mat_tensor_prod_2_prelim state.state_to_state_qbit)
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.col (v \<Otimes> w) 0) = dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
show "\<And>i. i<dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4
[PROOF STEP]
by (metis (no_types, lifting) assms(1) assms(2) dim_vec state.state_to_state_qbit vec_tensor_prod_2_bis)
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0,0) * w $$ (0,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)
[PROOF STEP]
using assms vec_tensor_prod_2 state.state_to_state_qbit col_index_of_mat_col
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = vec_of_list [?v $ 0 * ?w $ 0, ?v $ 0 * ?w $ 1, ?v $ 1 * ?w $ 0, ?v $ 1 * ?w $ 1]
state ?n ?v \<Longrightarrow> Matrix.col ?v 0 \<in> state_qbit ?n
\<lbrakk>dim_col ?v = 1; ?i < dim_row ?v\<rbrakk> \<Longrightarrow> Matrix.col ?v 0 $ ?i = ?v $$ (?i, 0)

goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)
[PROOF STEP]
by (smt nth_Cons_0 power_one_right state_def vec_of_list_index zero_less_numeral)
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "\<dots> = Matrix.col (v \<Otimes> w) 0 $ 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w

goal (1 subgoal):
 1. v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0,0) * w $$ (1,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)
[PROOF STEP]
using assms vec_tensor_prod_2 state.state_to_state_qbit col_index_of_mat_col
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = vec_of_list [?v $ 0 * ?w $ 0, ?v $ 0 * ?w $ 1, ?v $ 1 * ?w $ 0, ?v $ 1 * ?w $ 1]
state ?n ?v \<Longrightarrow> Matrix.col ?v 0 \<in> state_qbit ?n
\<lbrakk>dim_col ?v = 1; ?i < dim_row ?v\<rbrakk> \<Longrightarrow> Matrix.col ?v 0 $ ?i = ?v $$ (?i, 0)

goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)
[PROOF STEP]
by (smt One_nat_def Suc_1 lessI nth_Cons_0 power_one_right state_def vec_index_vCons_Suc
vec_of_list_Cons vec_of_list_index zero_less_numeral)
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "\<dots> = Matrix.col (v \<Otimes> w) 0 $ 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w

goal (1 subgoal):
 1. v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1,0) * w $$ (0,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)
[PROOF STEP]
using assms vec_tensor_prod_2 state.state_to_state_qbit col_index_of_mat_col
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = vec_of_list [?v $ 0 * ?w $ 0, ?v $ 0 * ?w $ 1, ?v $ 1 * ?w $ 0, ?v $ 1 * ?w $ 1]
state ?n ?v \<Longrightarrow> Matrix.col ?v 0 \<in> state_qbit ?n
\<lbrakk>dim_col ?v = 1; ?i < dim_row ?v\<rbrakk> \<Longrightarrow> Matrix.col ?v 0 $ ?i = ?v $$ (?i, 0)

goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)
[PROOF STEP]
by (smt One_nat_def Suc_1 lessI nth_Cons_0 power_one_right state_def vec_index_vCons_Suc
vec_of_list_Cons vec_of_list_index zero_less_numeral)
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "\<dots> = Matrix.col (v \<Otimes> w) 0 $ 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w

goal (1 subgoal):
 1. v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1,0) * w $$ (1,0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)
[PROOF STEP]
using assms vec_tensor_prod_2 state.state_to_state_qbit col_index_of_mat_col numeral_3_eq_3
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = vec_of_list [?v $ 0 * ?w $ 0, ?v $ 0 * ?w $ 1, ?v $ 1 * ?w $ 0, ?v $ 1 * ?w $ 1]
state ?n ?v \<Longrightarrow> Matrix.col ?v 0 \<in> state_qbit ?n
\<lbrakk>dim_col ?v = 1; ?i < dim_row ?v\<rbrakk> \<Longrightarrow> Matrix.col ?v 0 $ ?i = ?v $$ (?i, 0)
3 = Suc (Suc (Suc 0))

goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)
[PROOF STEP]
by (smt One_nat_def Suc_1 lessI nth_Cons_0 power_one_right state_def vec_index_vCons_Suc
vec_of_list_Cons vec_of_list_index zero_less_numeral)
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
have "\<dots> = Matrix.col (v \<Otimes> w) 0 $ 3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v $$ (1, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w

goal (1 subgoal):
 1. v $$ (1, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v $$ (1, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 3

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)
v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)
v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)
v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)
v $$ (1, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 3
[PROOF STEP]
show "\<And>i. i<dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i"
[PROOF STATE]
proof (prove)
using this:
dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)
v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)
v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)
v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)
v $$ (1, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 3

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
using index_sl_four
[PROOF STATE]
proof (prove)
using this:
dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) = 4
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 0 = v $$ (0, 0) * w $$ (0, 0)
v $$ (0, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 0
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 1 = v $$ (0, 0) * w $$ (1, 0)
v $$ (0, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 1
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 2 = v $$ (1, 0) * w $$ (0, 0)
v $$ (1, 0) * w $$ (0, 0) = Matrix.col (v \<Otimes> w) 0 $ 2
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ 3 = v $$ (1, 0) * w $$ (1, 0)
v $$ (1, 0) * w $$ (1, 0) = Matrix.col (v \<Otimes> w) 0 $ 3
\<forall>i<4. i = 0 \<or> i = 1 \<or> i = 2 \<or> i = 3

goal (1 subgoal):
 1. \<And>i. i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ ?i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ ?i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?i < dim_vec (Matrix.col v 0 \<otimes> Matrix.col w 0) \<Longrightarrow> Matrix.col (v \<Otimes> w) 0 $ ?i = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ ?i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_tensor_prod_2 [simp]:
  assumes "state 1 v" and "state 1 w"
  shows "v \<Otimes> w = Matrix.mat 4 1 (\<lambda>(i,j). if i = 0 then v $$ (0,0) * w $$ (0,0) else
                                            if i = 3 then v $$ (1,0) * w $$ (1,0) else
                                              if i = 1 then v $$ (0,0) * w $$ (1,0) else
                                                v $$ (1,0) * w $$ (0,0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<Otimes> w = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
 2. dim_row (v \<Otimes> w) = dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
 3. dim_col (v \<Otimes> w) = dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
[PROOF STEP]
define u where "u = Matrix.mat 4 1 (\<lambda>(i,j). if i = 0 then v $$ (0,0) * w $$ (0,0) else
                                            if i = 3 then v $$ (1,0) * w $$ (1,0) else
                                              if i = 1 then v $$ (0,0) * w $$ (1,0) else
                                                v $$ (1,0) * w $$ (0,0))"
[PROOF STATE]
proof (state)
this:
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
 2. dim_row (v \<Otimes> w) = dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
 3. dim_col (v \<Otimes> w) = dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))
[PROOF STEP]
show "dim_row (v \<Otimes> w) = dim_row u"
[PROOF STATE]
proof (prove)
using this:
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))

goal (1 subgoal):
 1. dim_row (v \<Otimes> w) = dim_row u
[PROOF STEP]
using assms tensor_mat_def state_def
[PROOF STATE]
proof (prove)
using this:
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))
state 1 v
state 1 w
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))
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. dim_row (v \<Otimes> w) = dim_row u
[PROOF STEP]
by(simp add: Tensor.mat_of_cols_list_def)
[PROOF STATE]
proof (state)
this:
dim_row (v \<Otimes> w) = dim_row u

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
 2. dim_col (v \<Otimes> w) = dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dim_row (v \<Otimes> w) = dim_row u

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
 2. dim_col (v \<Otimes> w) = dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
[PROOF STEP]
have "\<dots> = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row u = 4
[PROOF STEP]
by (simp add: u_def)
[PROOF STATE]
proof (state)
this:
dim_row u = 4

goal (2 subgoals):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
 2. dim_col (v \<Otimes> w) = dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))
[PROOF STEP]
show "dim_col (v \<Otimes> w) = dim_col u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col (v \<Otimes> w) = dim_col u
[PROOF STEP]
using u_def assms tensor_mat_def state_def Tensor.mat_of_cols_list_def
[PROOF STATE]
proof (prove)
using this:
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))
state 1 v
state 1 w
?A \<Otimes> ?B \<equiv> Tensor.mat_of_cols_list (dim_row ?A * dim_row ?B) (mult.Tensor (*) (mat_to_cols_list ?A) (mat_to_cols_list ?B))
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1
Tensor.mat_of_cols_list ?nr ?cs = Matrix.mat ?nr (length ?cs) (\<lambda>(i, j). ?cs ! j ! i)

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

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dim_col (v \<Otimes> w) = dim_col u

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
[PROOF STEP]
have "\<dots> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col u = 1
[PROOF STEP]
by(simp add: u_def)
[PROOF STATE]
proof (state)
this:
dim_col u = 1

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))); j < dim_col (Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)))\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $$ (i, j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dim_row (v \<Otimes> w) = dim_row u
dim_col (v \<Otimes> w) = dim_col u
dim_col u = 1
[PROOF STEP]
show "\<And>i j. i < dim_row u \<Longrightarrow> j < dim_col u \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i,j)"
[PROOF STATE]
proof (prove)
using this:
dim_row (v \<Otimes> w) = dim_row u
dim_col (v \<Otimes> w) = dim_col u
dim_col u = 1

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u; dim_row (v \<Otimes> w) = dim_row u; dim_col (v \<Otimes> w) = dim_col u; dim_col u = 1\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
fix i j::nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u; dim_row (v \<Otimes> w) = dim_row u; dim_col (v \<Otimes> w) = dim_col u; dim_col u = 1\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
assume a1:"i < dim_row u" and a2:"j < dim_col u"
[PROOF STATE]
proof (state)
this:
i < dim_row u
j < dim_col u

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u; dim_row (v \<Otimes> w) = dim_row u; dim_col (v \<Otimes> w) = dim_col u; dim_col u = 1\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < dim_row u
j < dim_col u
[PROOF STEP]
have "(v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i"
[PROOF STATE]
proof (prove)
using this:
i < dim_row u
j < dim_col u

goal (1 subgoal):
 1. (v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i
[PROOF STEP]
using Matrix.col_def u_def assms
[PROOF STATE]
proof (prove)
using this:
i < dim_row u
j < dim_col u
Matrix.col ?A ?j = Matrix.vec (dim_row ?A) (\<lambda>i. ?A $$ (i, ?j))
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))
state 1 v
state 1 w

goal (1 subgoal):
 1. (v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u; dim_row (v \<Otimes> w) = dim_row u; dim_col (v \<Otimes> w) = dim_col u; dim_col u = 1\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i
[PROOF STEP]
have f1:"(v \<Otimes> w) $$ (i, j) = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i"
[PROOF STATE]
proof (prove)
using this:
(v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i

goal (1 subgoal):
 1. (v \<Otimes> w) $$ (i, j) = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
using assms mat_tensor_prod_2_col
[PROOF STATE]
proof (prove)
using this:
(v \<Otimes> w) $$ (i, j) = Matrix.col (v \<Otimes> w) 0 $ i
state 1 v
state 1 w
\<lbrakk>state 1 ?v; state 1 ?w\<rbrakk> \<Longrightarrow> Matrix.col (?v \<Otimes> ?w) 0 = Matrix.col ?v 0 \<otimes> Matrix.col ?w 0

goal (1 subgoal):
 1. (v \<Otimes> w) $$ (i, j) = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v \<Otimes> w) $$ (i, j) = (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u; dim_row (v \<Otimes> w) = dim_row u; dim_col (v \<Otimes> w) = dim_col u; dim_col u = 1\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
have "(Matrix.col v 0 \<otimes> Matrix.col w 0) $ i =
 Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else
                                      if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else
                                          if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else
                                            Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i
[PROOF STEP]
using vec_tensor_prod_2_bis assms state.state_to_state_qbit
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = Matrix.vec 4 (\<lambda>i. if i = 0 then ?v $ 0 * ?w $ 0 else if i = 3 then ?v $ 1 * ?w $ 1 else if i = 1 then ?v $ 0 * ?w $ 1 else ?v $ 1 * ?w $ 0)
state 1 v
state 1 w
state ?n ?v \<Longrightarrow> Matrix.col ?v 0 \<in> state_qbit ?n

goal (1 subgoal):
 1. (Matrix.col v 0 \<otimes> Matrix.col w 0) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < dim_row u; j < dim_col u; dim_row (v \<Otimes> w) = dim_row u; dim_col (v \<Otimes> w) = dim_col u; dim_col u = 1\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
thus "(v \<Otimes> w) $$ (i, j) = u $$ (i,j)"
[PROOF STATE]
proof (prove)
using this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i

goal (1 subgoal):
 1. (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
using u_def a1 a2 assms state_def
[PROOF STATE]
proof (prove)
using this:
(Matrix.col v 0 \<otimes> Matrix.col w 0) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i
u = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))
i < dim_row u
j < dim_col u
state 1 v
state 1 w
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. (v \<Otimes> w) $$ (i, j) = u $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v \<Otimes> w) $$ (i, j) = u $$ (i, j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i < dim_row u; ?j < dim_col u\<rbrakk> \<Longrightarrow> (v \<Otimes> w) $$ (?i, ?j) = u $$ (?i, ?j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_tensor_prod_2_bis:
  assumes "state 1 v" and "state 1 w"
  shows "v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0,0) * w $$ (0,0) else
                                          if i = 3 then v $$ (1,0) * w $$ (1,0) else
                                            if i = 1 then v $$ (0,0) * w $$ (1,0) else
                                              v $$ (1,0) * w $$ (0,0))\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle>
[PROOF STEP]
using assms ket_vec_def mat_tensor_prod_2
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
|?v\<rangle> \<equiv> Matrix.mat (dim_vec ?v) 1 (\<lambda>(i, j). ?v $ i)
\<lbrakk>state 1 ?v; state 1 ?w\<rbrakk> \<Longrightarrow> ?v \<Otimes> ?w = Matrix.mat 4 1 (\<lambda>(i, j). if i = 0 then ?v $$ (0, 0) * ?w $$ (0, 0) else if i = 3 then ?v $$ (1, 0) * ?w $$ (1, 0) else if i = 1 then ?v $$ (0, 0) * ?w $$ (1, 0) else ?v $$ (1, 0) * ?w $$ (0, 0))

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle>
[PROOF STEP]
by(simp add: mat_eq_iff)


[STATEMENT]
lemma eq_ket_vec:
  fixes u v:: "complex Matrix.vec"
  assumes "u = v"
  shows "|u\<rangle> = |v\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |u\<rangle> = |v\<rangle>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u = v

goal (1 subgoal):
 1. |u\<rangle> = |v\<rangle>
[PROOF STEP]
by simp


[STATEMENT]
lemma mat_tensor_ket_vec:
  assumes "state 1 v" and "state 1 w"
  shows "v \<Otimes> w = |(Matrix.col v 0) \<otimes> (Matrix.col w 0)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
have "v \<Otimes> w = |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle>
[PROOF STEP]
using assms state_def
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
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. v \<Otimes> w = |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v \<Otimes> w = |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v \<Otimes> w = |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
have "\<dots> =
|Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0,0) * |Matrix.col w 0\<rangle> $$ (0,0) else
                                          if i = 3 then |Matrix.col v 0\<rangle> $$ (1,0) * |Matrix.col w 0\<rangle> $$ (1,0) else
                                            if i = 1 then |Matrix.col v 0\<rangle> $$ (0,0) * |Matrix.col w 0\<rangle> $$ (1,0) else
                                              |Matrix.col v 0\<rangle> $$ (1,0) * |Matrix.col w 0\<rangle> $$ (0,0))\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle>
[PROOF STEP]
using assms mat_tensor_prod_2_bis state_col_ket_vec
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>state 1 ?v; state 1 ?w\<rbrakk> \<Longrightarrow> ?v \<Otimes> ?w = |Matrix.vec 4 (\<lambda>i. if i = 0 then ?v $$ (0, 0) * ?w $$ (0, 0) else if i = 3 then ?v $$ (1, 0) * ?w $$ (1, 0) else if i = 1 then ?v $$ (0, 0) * ?w $$ (1, 0) else ?v $$ (1, 0) * ?w $$ (0, 0))\<rangle>
state 1 ?v \<Longrightarrow> state 1 |Matrix.col ?v 0\<rangle>

goal (1 subgoal):
 1. |Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
|Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|Matrix.col v 0\<rangle> \<Otimes> |Matrix.col w 0\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
have "\<dots> =
|Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0,0) * w $$ (0,0) else
                                          if i = 3 then v $$ (1,0) * w $$ (1,0) else
                                            if i = 1 then v $$ (0,0) * w $$ (1,0) else
                                              v $$ (1,0) * w $$ (0,0))\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle>
[PROOF STEP]
using assms mat_tensor_prod_2_bis calculation
[PROOF STATE]
proof (prove)
using this:
state 1 v
state 1 w
\<lbrakk>state 1 ?v; state 1 ?w\<rbrakk> \<Longrightarrow> ?v \<Otimes> ?w = |Matrix.vec 4 (\<lambda>i. if i = 0 then ?v $$ (0, 0) * ?w $$ (0, 0) else if i = 3 then ?v $$ (1, 0) * ?w $$ (1, 0) else if i = 1 then ?v $$ (0, 0) * ?w $$ (1, 0) else ?v $$ (1, 0) * ?w $$ (0, 0))\<rangle>
v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle>

goal (1 subgoal):
 1. |Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
|Matrix.vec 4 (\<lambda>i. if i = 0 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (0, 0) else if i = 3 then |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else if i = 1 then |Matrix.col v 0\<rangle> $$ (0, 0) * |Matrix.col w 0\<rangle> $$ (1, 0) else |Matrix.col v 0\<rangle> $$ (1, 0) * |Matrix.col w 0\<rangle> $$ (0, 0))\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
have "\<dots> =
|Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else
                                      if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else
                                          if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else
                                            Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)\<rangle>
[PROOF STEP]
apply(rule eq_ket_vec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)
[PROOF STEP]
apply (rule eq_vecI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)) \<Longrightarrow> Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i
 2. dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))) = dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0))
[PROOF STEP]
using col_index_of_mat_col assms state_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>dim_col ?v = 1; ?i < dim_row ?v\<rbrakk> \<Longrightarrow> Matrix.col ?v 0 $ ?i = ?v $$ (?i, 0)
state 1 v
state 1 w
state ?n ?v \<equiv> dim_col ?v = 1 \<and> dim_row ?v = 2 ^ ?n \<and> \<parallel>Matrix.col ?v 0\<parallel> = 1

goal (2 subgoals):
 1. \<And>i. i < dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)) \<Longrightarrow> Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0)) $ i = Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0) $ i
 2. dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))) = dim_vec (Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
|Matrix.vec 4 (\<lambda>i. if i = 0 then v $$ (0, 0) * w $$ (0, 0) else if i = 3 then v $$ (1, 0) * w $$ (1, 0) else if i = 1 then v $$ (0, 0) * w $$ (1, 0) else v $$ (1, 0) * w $$ (0, 0))\<rangle> = |Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)\<rangle>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)\<rangle>

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
using vec_tensor_prod_2_bis assms state.state_to_state_qbit
[PROOF STATE]
proof (prove)
using this:
v \<Otimes> w = |Matrix.vec 4 (\<lambda>i. if i = 0 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 0 else if i = 3 then Matrix.col v 0 $ 1 * Matrix.col w 0 $ 1 else if i = 1 then Matrix.col v 0 $ 0 * Matrix.col w 0 $ 1 else Matrix.col v 0 $ 1 * Matrix.col w 0 $ 0)\<rangle>
\<lbrakk>?v \<in> state_qbit 1; ?w \<in> state_qbit 1\<rbrakk> \<Longrightarrow> ?v \<otimes> ?w = Matrix.vec 4 (\<lambda>i. if i = 0 then ?v $ 0 * ?w $ 0 else if i = 3 then ?v $ 1 * ?w $ 1 else if i = 1 then ?v $ 0 * ?w $ 1 else ?v $ 1 * ?w $ 0)
state 1 v
state 1 w
state ?n ?v \<Longrightarrow> Matrix.col ?v 0 \<in> state_qbit ?n

goal (1 subgoal):
 1. v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
v \<Otimes> w = |Matrix.col v 0 \<otimes> Matrix.col w 0\<rangle>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tensor_state2 [simp]:
  assumes "state 1 u" and "state 1 v"
  shows "state 2 (u \<Otimes> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state 2 (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\<^sup>2
 3. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
show "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 1 u
state 1 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\<^sup>2
 2. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
show "dim_row (u \<Otimes> v) = 2\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (u \<Otimes> v) = 2\<^sup>2
[PROOF STEP]
using assms dim_row_tensor_mat state.dim_row
[PROOF STATE]
proof (prove)
using this:
state 1 u
state 1 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\<^sup>2
[PROOF STEP]
by (metis (mono_tags, lifting) power2_eq_square power_one_right)
[PROOF STATE]
proof (state)
this:
dim_row (u \<Otimes> v) = 2\<^sup>2

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
show "\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
define l where d0:"l = [u $$ (0,0) * v $$ (0,0), u $$ (0,0) * v $$ (1,0), u $$ (1,0) * v $$ (0,0), u $$ (1,0) * v $$ (1,0)]"
[PROOF STATE]
proof (state)
this:
l = [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
l = [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]
[PROOF STEP]
have f4:"length l = 4"
[PROOF STATE]
proof (prove)
using this:
l = [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]

goal (1 subgoal):
 1. length l = 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length l = 4

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
length l = 4

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "u \<Otimes> v = mat_of_cols_list 4
[[u $$ (0,0) * v $$ (0,0), u $$ (0,0) * v $$ (1,0), u $$ (1,0) * v $$ (0,0), u $$ (1,0) * v $$ (1,0)]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<Otimes> v = Tensor.mat_of_cols_list 4 [[u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]]
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
state 1 u
state 1 v

goal (1 subgoal):
 1. u \<Otimes> v = Tensor.mat_of_cols_list 4 [[u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<Otimes> v = Tensor.mat_of_cols_list 4 [[u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]]

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u \<Otimes> v = Tensor.mat_of_cols_list 4 [[u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]]
[PROOF STEP]
have "Matrix.col (u \<Otimes> v) 0 = vec_of_list [u $$ (0,0) * v $$ (0,0), u $$ (0,0) * v $$ (1,0),
u $$ (1,0) * v $$ (0,0), u $$ (1,0) * v $$ (1,0)]"
[PROOF STATE]
proof (prove)
using this:
u \<Otimes> v = Tensor.mat_of_cols_list 4 [[u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]]

goal (1 subgoal):
 1. Matrix.col (u \<Otimes> v) 0 = vec_of_list [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]
[PROOF STEP]
by (metis One_nat_def Suc_eq_plus1 add_Suc col_mat_of_cols_list list.size(3) list.size(4)
nth_Cons_0 numeral_2_eq_2 numeral_Bit0 plus_1_eq_Suc vec_of_list_Cons zero_less_one_class.zero_less_one)
[PROOF STATE]
proof (state)
this:
Matrix.col (u \<Otimes> v) 0 = vec_of_list [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Matrix.col (u \<Otimes> v) 0 = vec_of_list [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]
[PROOF STEP]
have f5:"\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt(\<Sum>i<4. (cmod (l ! i))\<^sup>2)"
[PROOF STATE]
proof (prove)
using this:
Matrix.col (u \<Otimes> v) 0 = vec_of_list [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2)
[PROOF STEP]
by (metis d0 f4 One_nat_def cpx_length_of_vec_of_list d0 vec_of_list_Cons)
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "\<dots> = sqrt ((cmod (u $$ (0,0) * v $$ (0,0)))\<^sup>2 + (cmod(u $$ (0,0) * v $$ (1,0)))\<^sup>2 +
(cmod(u $$ (1,0) * v $$ (0,0)))\<^sup>2 + (cmod(u $$ (1,0) * v $$ (1,0)))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
have "(\<Sum>i<4. (cmod (l ! i))\<^sup>2) = (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 +
(cmod (l ! 3))\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2
[PROOF STEP]
using sum_insert
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<notin> ?F; finite ?F\<rbrakk> \<Longrightarrow> sum ?P (insert ?x ?F) = sum ?P ?F + ?P ?x

goal (1 subgoal):
 1. (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2
[PROOF STEP]
by (smt One_nat_def empty_iff finite.emptyI finite.insertI insertE lessThan_0 lessThan_Suc
numeral_2_eq_2 numeral_3_eq_3 numeral_plus_one one_plus_numeral_commute plus_1_eq_Suc semiring_norm(2)
semiring_norm(8) sum.empty)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<4. (cmod (l ! i))\<^sup>2) = (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2

goal (1 subgoal):
 1. sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<4. (cmod (l ! i))\<^sup>2) = (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2

goal (1 subgoal):
 1. sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
have "\<dots> = (cmod (u $$ (0,0) * v $$ (0,0)))\<^sup>2 + (cmod(u $$ (0,0) * v $$ (1,0)))\<^sup>2 +
(cmod(u $$ (1,0) * v $$ (0,0)))\<^sup>2 + (cmod(u $$ (1,0) * v $$ (1,0)))\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2 = (cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2
[PROOF STEP]
using d0
[PROOF STATE]
proof (prove)
using this:
l = [u $$ (0, 0) * v $$ (0, 0), u $$ (0, 0) * v $$ (1, 0), u $$ (1, 0) * v $$ (0, 0), u $$ (1, 0) * v $$ (1, 0)]

goal (1 subgoal):
 1. (cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2 = (cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(cmod (l ! 0))\<^sup>2 + (cmod (l ! 1))\<^sup>2 + (cmod (l ! 2))\<^sup>2 + (cmod (l ! 3))\<^sup>2 = (cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2

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

goal (1 subgoal):
 1. sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
by(simp add: f5)
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)

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

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "\<dots> =
sqrt ((cmod (u $$ (0,0)))\<^sup>2 * (cmod (v $$ (0,0)))\<^sup>2 + (cmod(u $$ (0,0)))\<^sup>2 * (cmod (v $$ (1,0)))\<^sup>2 +
(cmod(u $$ (1,0)))\<^sup>2 * (cmod (v $$ (0,0)))\<^sup>2 + (cmod(u $$ (1,0)))\<^sup>2 * (cmod(v $$ (1,0)))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2) = sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
by (simp add: norm_mult power_mult_distrib)
[PROOF STATE]
proof (state)
this:
sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2) = sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2) = sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have "\<dots> = sqrt ((((cmod(u $$ (0,0)))\<^sup>2 + (cmod(u $$ (1,0)))\<^sup>2)) *
(((cmod(v $$ (0,0)))\<^sup>2 + (cmod(v $$ (1,0)))\<^sup>2)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2) = sqrt (((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2))
[PROOF STEP]
by (simp add: distrib_left mult.commute)
[PROOF STATE]
proof (state)
this:
sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2) = sqrt (((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2))

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt (\<Sum>i<length l. (cmod (l ! i))\<^sup>2)
sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2) = sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2)
sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2) = sqrt (((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2))
[PROOF STEP]
have f6:"\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = (((cmod(u $$ (0,0)))\<^sup>2 + (cmod(u $$ (1,0)))\<^sup>2)) *
(((cmod(v $$ (0,0)))\<^sup>2 + (cmod(v $$ (1,0)))\<^sup>2))"
[PROOF STATE]
proof (prove)
using this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt (\<Sum>i<length l. (cmod (l ! i))\<^sup>2)
sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)
sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2) = sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2)
sqrt ((cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (0, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2 * (cmod (v $$ (1, 0)))\<^sup>2) = sqrt (((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2))

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = ((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2)
[PROOF STEP]
by (simp add: f4)
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = ((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2)

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

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have f7:"\<dots> = (\<Sum>i< 2. (cmod (u $$ (i,0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i,0)))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2)
[PROOF STEP]
by (simp add: numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (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:
((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have f8:"\<dots> = (\<Sum>i< 2.(cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2.(cmod (Matrix.col v 0 $ i))\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2)
[PROOF STEP]
using assms index_col state_def
[PROOF STATE]
proof (prove)
using this:
state 1 u
state 1 v
\<lbrakk>?i < dim_row ?A; ?j < dim_col ?A\<rbrakk> \<Longrightarrow> Matrix.col ?A ?j $ ?i = ?A $$ (?i, ?j)
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. (\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2)

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

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) \<Longrightarrow> \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have f1:"(\<Sum>i< 2.(cmod (Matrix.col u 0 $ i))\<^sup>2) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) = 1
[PROOF STEP]
using assms(1) state_def cpx_vec_length_def
[PROOF STATE]
proof (prove)
using this:
state 1 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. (cmod (Matrix.col u 0 $ i))\<^sup>2) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) = 1

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) \<Longrightarrow> \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
have f2:"(\<Sum>i< 2.(cmod (Matrix.col v 0 $ i))\<^sup>2) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) = 1
[PROOF STEP]
using assms(2) state_def cpx_vec_length_def
[PROOF STATE]
proof (prove)
using this:
state 1 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. (cmod (Matrix.col v 0 $ i))\<^sup>2) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) = 1

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) \<Longrightarrow> \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) = 1

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
using f1 f8 f5 f6 f7
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2) = 1
(\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) = 1
(\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (Matrix.col u 0 $ i))\<^sup>2) * (\<Sum>i<2. (cmod (Matrix.col v 0 $ i))\<^sup>2)
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2)
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel>\<^sup>2 = ((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2)
((cmod (u $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0)))\<^sup>2) * ((cmod (v $$ (0, 0)))\<^sup>2 + (cmod (v $$ (1, 0)))\<^sup>2) = (\<Sum>i<2. (cmod (u $$ (i, 0)))\<^sup>2) * (\<Sum>i<2. (cmod (v $$ (i, 0)))\<^sup>2)

goal (1 subgoal):
 1. \<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1
[PROOF STEP]
by (simp add: \<open>sqrt (\<Sum>i<4. (cmod (l ! i))\<^sup>2) = sqrt ((cmod (u $$ (0, 0) * v $$ (0, 0)))\<^sup>2 +
(cmod (u $$ (0, 0) * v $$ (1, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (0, 0)))\<^sup>2 + (cmod (u $$ (1, 0) * v $$ (1, 0)))\<^sup>2)\<close>)
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>Matrix.col (u \<Otimes> v) 0\<parallel> = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_prod:
  fixes f::"nat \<Rightarrow> complex" and g::"nat \<Rightarrow> complex"
  shows "(\<Sum>i<a*b. f(i div b) * g(i mod b)) = (\<Sum>i<a. f(i)) * (\<Sum>j<b. g(j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b}
[PROOF STEP]
proof (induction a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>i<0 * b. f (i div b) * g (i mod b)) = sum f {..<0} * sum g {..<b}
 2. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. (\<Sum>i<0 * b. f (i div b) * g (i mod b)) = sum f {..<0} * sum g {..<b}
 2. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<0 * b. f (i div b) * g (i mod b)) = sum f {..<0} * sum g {..<b}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<0 * b. f (i div b) * g (i mod b)) = sum f {..<0} * sum g {..<b}

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
case (Suc a)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b}

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
have "(\<Sum>i<(a+1)*b. f (i div b) * g (i mod b)) = (\<Sum>i<a*b. f (i div b) * g (i mod b)) +
(\<Sum>i\<in>{a*b..<(a+1)*b}. f (i div b) * g (i mod b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<(a + 1) * b. f (i div b) * g (i mod b)) = (\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b))
[PROOF STEP]
apply (auto simp: algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<b + a * b. f (i div b) * g (i mod b)) = (\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<b + a * b. f (i div b) * g (i mod b))
[PROOF STEP]
by (smt add.commute mult_Suc sum.lessThan_Suc sum.nat_group)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<(a + 1) * b. f (i div b) * g (i mod b)) = (\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<(a + 1) * b. f (i div b) * g (i mod b)) = (\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
have "\<dots> = (\<Sum>i<a. f(i)) * (\<Sum>j<b. g(j)) + (\<Sum>i\<in>{a*b..<(a+1)*b}. f (i div b) * g (i mod b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b))
[PROOF STEP]
by (simp add: Suc.IH)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<a * b. f (i div b) * g (i mod b)) + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
have "\<dots> = (\<Sum>i<a. f(i)) * (\<Sum>j<b. g(j)) + (\<Sum>i\<in>{a*b..<(a+1)*b}. f (a) * g(i-a*b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f a * g (i - a * b))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f a * g (i - a * b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f a * g (i - a * b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
have "\<dots> = (\<Sum>i<a. f(i)) * (\<Sum>j<b. g(j)) + f(a) * (\<Sum>i\<in>{a*b..<(a+1)*b}. g(i-a*b))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f a * g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b))
[PROOF STEP]
by(simp add: sum_distrib_left)
[PROOF STATE]
proof (state)
this:
sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f a * g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum f {..<a} * sum g {..<b} + (\<Sum>i = a * b..<(a + 1) * b. f a * g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b))

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
have "\<dots> = (\<Sum>i<a. f(i)) * (\<Sum>j<b. g(j)) + f(a) * (\<Sum>i\<in>{..<b}. g(i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * sum g {..<b}
[PROOF STEP]
using sum_of_index_diff[of "g" "(a*b)" "b"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = a * b..<a * b + b. g (i - a * b)) = sum g {..<b}

goal (1 subgoal):
 1. sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * sum g {..<b}
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * sum g {..<b}

goal (1 subgoal):
 1. \<And>a. (\<Sum>i<a * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} \<Longrightarrow> (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b))
sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * sum g {..<b}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<(a + 1) * b. f (i div b) * g (i mod b)) = sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b))
sum f {..<a} * sum g {..<b} + f a * (\<Sum>i = a * b..<(a + 1) * b. g (i - a * b)) = sum f {..<a} * sum g {..<b} + f a * sum g {..<b}

goal (1 subgoal):
 1. (\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}
[PROOF STEP]
by (simp add: semiring_normalization_rules(1))
[PROOF STATE]
proof (state)
this:
(\<Sum>i<Suc a * b. f (i div b) * g (i mod b)) = sum f {..<Suc a} * sum g {..<b}

goal:
No subgoals!
[PROOF STEP]
qed