[STATEMENT]
lemma vec_tensor_prod_2_bis [simp]:
  assumes "v \<in> state_qbit 1" and "w \<in> state_qbit 1"
  shows "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)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 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)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec (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)) \<Longrightarrow> (v \<otimes> w) $ i = 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) $ i
 2. dim_vec (v \<otimes> w) = dim_vec (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))
[PROOF STEP]
define u where "u = 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)"
[PROOF STATE]
proof (state)
this:
u = 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 (2 subgoals):
 1. \<And>i. i < dim_vec (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)) \<Longrightarrow> (v \<otimes> w) $ i = 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) $ i
 2. dim_vec (v \<otimes> w) = dim_vec (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))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
u = 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)
[PROOF STEP]
show f2:"dim_vec (v \<otimes> w) = dim_vec u"
[PROOF STATE]
proof (prove)
using this:
u = 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 (v \<otimes> w) = dim_vec u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
u = 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)
v \<in> state_qbit 1
w \<in> state_qbit 1

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

goal (1 subgoal):
 1. \<And>i. i < dim_vec (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)) \<Longrightarrow> (v \<otimes> w) $ i = 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) $ i
[PROOF STEP]
show "\<And>i. i < dim_vec u \<Longrightarrow> (v \<otimes> w) $ i = u $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < dim_vec u \<Longrightarrow> (v \<otimes> w) $ i = u $ i
[PROOF STEP]
apply (auto simp: u_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. (v \<otimes> w) $ Suc 0 = v $ 0 * w $ Suc 0
 2. (v \<otimes> w) $ 3 = v $ Suc 0 * w $ Suc 0
 3. (v \<otimes> w) $ 0 = v $ 0 * w $ 0
 4. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> state_qbit 1
w \<in> state_qbit 1

goal (4 subgoals):
 1. (v \<otimes> w) $ Suc 0 = v $ 0 * w $ Suc 0
 2. (v \<otimes> w) $ 3 = v $ Suc 0 * w $ Suc 0
 3. (v \<otimes> w) $ 0 = v $ 0 * w $ 0
 4. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
apply auto[3]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a aa A Aa. \<lbrakk>v = module.lincomb (module_cpx_vec 2) a A; w = module.lincomb (module_cpx_vec 2) aa Aa; finite A; finite Aa; A \<subseteq> unit_vectors 2; \<parallel>module.lincomb (module_cpx_vec 2) a A\<parallel> = 1; Aa \<subseteq> unit_vectors 2; \<parallel>module.lincomb (module_cpx_vec 2) aa Aa\<parallel> = 1\<rbrakk> \<Longrightarrow> vCons (module.lincomb (module_cpx_vec 2) a A $ 0 * module.lincomb (module_cpx_vec 2) aa Aa $ 0) (vCons (module.lincomb (module_cpx_vec 2) a A $ 0 * module.lincomb (module_cpx_vec 2) aa Aa $ Suc 0) (vCons (module.lincomb (module_cpx_vec 2) a A $ Suc 0 * module.lincomb (module_cpx_vec 2) aa Aa $ 0) (vCons (module.lincomb (module_cpx_vec 2) a A $ Suc 0 * module.lincomb (module_cpx_vec 2) aa Aa $ Suc 0) vNil))) $ 3 = module.lincomb (module_cpx_vec 2) a A $ Suc 0 * module.lincomb (module_cpx_vec 2) aa Aa $ Suc 0
 2. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
apply (simp add: numeral_3_eq_3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
using u_def vec_of_list_index vec_tensor_prod_2 index_is_2
[PROOF STATE]
proof (prove)
using this:
u = 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)
vec_of_list ?xs $ ?j = ?xs ! ?j
\<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]
\<forall>i. i \<noteq> Suc 0 \<longrightarrow> i \<noteq> 3 \<longrightarrow> 0 < i \<longrightarrow> i < 4 \<longrightarrow> i = 2

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < 4; i \<noteq> Suc 0; i \<noteq> 3; 0 < i\<rbrakk> \<Longrightarrow> (v \<otimes> w) $ i = v $ Suc 0 * w $ 0
[PROOF STEP]
by (metis (no_types, lifting) One_nat_def assms nth_Cons_0 nth_Cons_Suc numeral_2_eq_2)
[PROOF STATE]
proof (state)
this:
?i < dim_vec u \<Longrightarrow> (v \<otimes> w) $ ?i = u $ ?i

goal:
No subgoals!
[PROOF STEP]
qed