[STATEMENT]
lemma g3ip_upRules:
shows "g3ip \<subseteq> upRules"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
assume "r \<in> g3ip"
[PROOF STATE]
proof (state)
this:
r \<in> g3ip

goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r \<in> g3ip
[PROOF STEP]
have "r \<in> upRules"
[PROOF STATE]
proof (prove)
using this:
r \<in> g3ip

goal (1 subgoal):
 1. r \<in> upRules
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r \<in> g3ip; r = (a, b)\<rbrakk> \<Longrightarrow> r \<in> upRules
[PROOF STEP]
by (rule g3ip.cases) auto
[PROOF STATE]
proof (state)
this:
r \<in> upRules

goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?r2 \<in> g3ip \<Longrightarrow> ?r2 \<in> upRules

goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?r2 \<in> g3ip \<Longrightarrow> ?r2 \<in> upRules
[PROOF STEP]
show "g3ip \<subseteq> upRules"
[PROOF STATE]
proof (prove)
using this:
?r2 \<in> g3ip \<Longrightarrow> ?r2 \<in> upRules

goal (1 subgoal):
 1. g3ip \<subseteq> upRules
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g3ip \<subseteq> upRules

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma impRInvert:
assumes "(\<Gamma> \<Rightarrow>* (A \<supset> B), n) \<in> derivable (Ax \<union> g3ip)*" and "B \<noteq> Em"
shows "\<exists> m\<le>n. (\<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable (Ax \<union> g3ip)*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*
[PROOF STEP]
have "\<forall> r \<in> (Ax \<union> g3ip). rightPrincipal r (A \<supset> B) \<longrightarrow>
                           (\<LM>A\<RM> \<Rightarrow>* B) \<in> set (fst r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
proof-  \<comment> \<open>Showing that $A \Rightarrow B$ is a premiss of every rule with $\implies{A}{B}$ principal\<close>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
fix r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
assume "r \<in> (Ax \<union> g3ip)"
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<union> g3ip

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
r \<in> Ax \<union> g3ip

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
assume "rightPrincipal r (A \<supset> B)"
[PROOF STATE]
proof (state)
this:
rightPrincipal r (A \<supset> B)

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
r \<in> Ax \<union> g3ip
rightPrincipal r (A \<supset> B)
[PROOF STEP]
have "r \<in> g3ip"
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax \<union> g3ip
rightPrincipal r (A \<supset> B)

goal (1 subgoal):
 1. r \<in> g3ip
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
using this:
r \<in> Ax \<union> g3ip
rightPrincipal r (A \<supset> B)

goal (1 subgoal):
 1. r \<in> g3ip
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rightPrincipal r (A \<supset> B); r \<in> Ax\<rbrakk> \<Longrightarrow> r \<in> g3ip
[PROOF STEP]
apply (rule rightPrincipal.cases)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>rightPrincipal r (A \<supset> B); r \<in> Ax\<rbrakk> \<Longrightarrow> rightPrincipal ?a1.3 ?a2.3
 2. \<And>C F Fs Ps. \<lbrakk>rightPrincipal r (A \<supset> B); r \<in> Ax; ?a1.3 = (Ps, C); ?a2.3 = Compound F Fs; C = ( \<Empt> \<Rightarrow>* Compound F Fs)\<rbrakk> \<Longrightarrow> r \<in> g3ip
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps. \<lbrakk>rightPrincipal (Ps,  \<Empt> \<Rightarrow>* A \<supset> B) (A \<supset> B); (Ps,  \<Empt> \<Rightarrow>* A \<supset> B) \<in> Ax; r = (Ps,  \<Empt> \<Rightarrow>* A \<supset> B)\<rbrakk> \<Longrightarrow> (Ps,  \<Empt> \<Rightarrow>* A \<supset> B) \<in> g3ip
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Ps. \<lbrakk>rightPrincipal (Ps,  \<Empt> \<Rightarrow>* A \<supset> B) (A \<supset> B); (Ps,  \<Empt> \<Rightarrow>* A \<supset> B) \<in> Ax; r = (Ps,  \<Empt> \<Rightarrow>* A \<supset> B)\<rbrakk> \<Longrightarrow> (Ps,  \<Empt> \<Rightarrow>* A \<supset> B) \<in> g3ip
[PROOF STEP]
by(*<*) (rule Ax.cases) (*>*) auto  \<comment> \<open>If $\implies{A}{B}$ was principal, then $r \notin Ax$\<close>
[PROOF STATE]
proof (state)
this:
r \<in> g3ip

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
from \<open>rightPrincipal r (A \<supset> B)\<close>
[PROOF STATE]
proof (chain)
picking this:
rightPrincipal r (A \<supset> B)
[PROOF STEP]
have "snd r = (\<Empt> \<Rightarrow>* (A \<supset> B))"
[PROOF STATE]
proof (prove)
using this:
rightPrincipal r (A \<supset> B)

goal (1 subgoal):
 1. snd r = ( \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
by(*<*) (rule rightPrincipal.cases)(*>*) auto
[PROOF STATE]
proof (state)
this:
snd r = ( \<Empt> \<Rightarrow>* A \<supset> B)

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
with \<open>r \<in> g3ip\<close> and \<open>rightPrincipal r (A \<supset> B)\<close>
[PROOF STATE]
proof (chain)
picking this:
r \<in> g3ip
rightPrincipal r (A \<supset> B)
snd r = ( \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
have "r = ([\<LM>A\<RM> \<Rightarrow>* B], \<Empt> \<Rightarrow>* (A\<supset>B))"
[PROOF STATE]
proof (prove)
using this:
r \<in> g3ip
rightPrincipal r (A \<supset> B)
snd r = ( \<Empt> \<Rightarrow>* A \<supset> B)

goal (1 subgoal):
 1. r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
using this:
r \<in> g3ip
rightPrincipal r (A \<supset> B)
snd r = ( \<Empt> \<Rightarrow>* A \<supset> B)

goal (1 subgoal):
 1. r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
apply (cases r)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r \<in> g3ip; rightPrincipal r (A \<supset> B); snd r = ( \<Empt> \<Rightarrow>* A \<supset> B); r = (a, b)\<rbrakk> \<Longrightarrow> r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>r \<in> g3ip; rightPrincipal r (A \<supset> B); snd r = ( \<Empt> \<Rightarrow>* A \<supset> B); r = (a, b)\<rbrakk> \<Longrightarrow> r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
by (rule g3ip.cases) auto
[PROOF STATE]
proof (state)
this:
r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)
[PROOF STEP]
have "(\<LM>A\<RM> \<Rightarrow>* B) \<in> set (fst r)"
[PROOF STATE]
proof (prove)
using this:
r = ([ \<LM> A  \<RM> \<Rightarrow>* B],  \<Empt> \<Rightarrow>* A \<supset> B)

goal (1 subgoal):
 1. ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?r2 \<in> Ax \<union> g3ip; rightPrincipal ?r2 (A \<supset> B)\<rbrakk> \<Longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst ?r2)

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?r2 \<in> Ax \<union> g3ip; rightPrincipal ?r2 (A \<supset> B)\<rbrakk> \<Longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst ?r2)

goal (1 subgoal):
 1. \<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*
[PROOF STEP]
with assms (*<*)and g3ip_upRules
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*
B \<noteq> Em
g3ip \<subseteq> upRules
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (chain)
picking this:
( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*
B \<noteq> Em
g3ip \<subseteq> upRules
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*
B \<noteq> Em
g3ip \<subseteq> upRules
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*
[PROOF STEP]
using rightInvertible(*<*)[where R'="g3ip" and R="Ax \<union> g3ip" and \<Gamma>=\<Gamma> and n=n
                            and \<Gamma>'="\<LM>A\<RM>" and E=B and F="imp" and Fs="[A,B]"]
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*
B \<noteq> Em
g3ip \<subseteq> upRules
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
\<lbrakk>g3ip \<subseteq> upRules \<and> Ax \<union> g3ip = Ax \<union> g3ip; ( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*; \<forall>r'\<in>Ax \<union> g3ip. rightPrincipal r' (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r'); B \<noteq> Em\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*
[PROOF STEP]
(*>*)
[PROOF STATE]
proof (prove)
using this:
( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*
B \<noteq> Em
g3ip \<subseteq> upRules
\<forall>r\<in>Ax \<union> g3ip. rightPrincipal r (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r)
\<lbrakk>g3ip \<subseteq> upRules \<and> Ax \<union> g3ip = Ax \<union> g3ip; ( \<Gamma> \<Rightarrow>* A \<supset> B, n) \<in> derivable Ax \<union> g3ip*; \<forall>r'\<in>Ax \<union> g3ip. rightPrincipal r' (A \<supset> B) \<longrightarrow> ( \<LM> A  \<RM> \<Rightarrow>* B) \<in> set (fst r'); B \<noteq> Em\<rbrakk> \<Longrightarrow> \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*

goal (1 subgoal):
 1. \<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>m\<le>n. ( \<Gamma> \<oplus> A \<Rightarrow>* B, m) \<in> derivable Ax \<union> g3ip*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma removelE:
    assumes I: "invar s" "\<alpha> s \<noteq> []"
    obtains s' where "removel s = (hd (\<alpha> s), s')" "invar s'" "\<alpha> s' = tl (\<alpha> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>removel s = (hd (\<alpha> s), s'); invar s'; \<alpha> s' = tl (\<alpha> s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>removel s = (hd (\<alpha> s), s'); invar s'; \<alpha> s' = tl (\<alpha> s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from removel_correct(1,2,3)[OF I]
[PROOF STATE]
proof (chain)
picking this:
fst (removel s) = hd (\<alpha> s)
\<alpha> (snd (removel s)) = tl (\<alpha> s)
invar (snd (removel s))
[PROOF STEP]
have
      C: "fst (removel s) = hd (\<alpha> s)"
         "\<alpha> (snd (removel s)) = tl (\<alpha> s)"
         "invar (snd (removel s))"
[PROOF STATE]
proof (prove)
using this:
fst (removel s) = hd (\<alpha> s)
\<alpha> (snd (removel s)) = tl (\<alpha> s)
invar (snd (removel s))

goal (1 subgoal):
 1. fst (removel s) = hd (\<alpha> s) &&& \<alpha> (snd (removel s)) = tl (\<alpha> s) &&& invar (snd (removel s))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
fst (removel s) = hd (\<alpha> s)
\<alpha> (snd (removel s)) = tl (\<alpha> s)
invar (snd (removel s))

goal (1 subgoal):
 1. (\<And>s'. \<lbrakk>removel s = (hd (\<alpha> s), s'); invar s'; \<alpha> s' = tl (\<alpha> s)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from that[of "snd (removel s)", OF _ C(3,2), folded C(1)]
[PROOF STATE]
proof (chain)
picking this:
removel s = (fst (removel s), snd (removel s)) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
using this:
removel s = (fst (removel s), snd (removel s)) \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_vec_of_basis_enum'[simp]:
  \<open>dim_vec (vec_of_basis_enum (v::'a)) = length (canonical_basis::'a::basis_enum list)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum v) = length canonical_basis
[PROOF STEP]
unfolding vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_list (map (crepresentation (set canonical_basis) v) canonical_basis)) = length canonical_basis
[PROOF STEP]
by simp


[STATEMENT]
lemma vec_of_basis_enum_inverse[simp]:
  fixes w::"'a::basis_enum"
  shows  "basis_enum_of_vec (vec_of_basis_enum w) = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (vec_of_basis_enum w) = w
[PROOF STEP]
unfolding vec_of_basis_enum_def basis_enum_of_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if dim_vec (vec_of_list (map (crepresentation (set canonical_basis) w) canonical_basis)) = length canonical_basis then sum_list (map2 (*\<^sub>C) (list_of_vec (vec_of_list (map (crepresentation (set canonical_basis) w) canonical_basis))) canonical_basis) else (0::'a)) = w
[PROOF STEP]
unfolding list_vec zip_map1 zip_same_conv_map map_map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if dim_vec (vec_of_list (map (crepresentation (set canonical_basis) w) canonical_basis)) = length canonical_basis then sum_list (map ((\<lambda>(x, y). x *\<^sub>C y) \<circ> ((\<lambda>(x, y). (crepresentation (set canonical_basis) w x, y)) \<circ> (\<lambda>x. (x, x)))) canonical_basis) else (0::'a)) = w
[PROOF STEP]
apply (simp add: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>canonical_basis. crepresentation (set canonical_basis) w x *\<^sub>C x) = w
[PROOF STEP]
apply (subst sum.distinct_set_conv_list[symmetric], simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set canonical_basis. crepresentation (set canonical_basis) w x *\<^sub>C x) = w
[PROOF STEP]
apply (rule complex_vector.sum_representation_eq)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. cindependent (set canonical_basis)
 2. w \<in> cspan (set canonical_basis)
 3. finite (set canonical_basis)
 4. set canonical_basis \<subseteq> set canonical_basis
[PROOF STEP]
using  is_generator_set
[PROOF STATE]
proof (prove)
using this:
cspan (set canonical_basis) = UNIV

goal (4 subgoals):
 1. cindependent (set canonical_basis)
 2. w \<in> cspan (set canonical_basis)
 3. finite (set canonical_basis)
 4. set canonical_basis \<subseteq> set canonical_basis
[PROOF STEP]
by auto


[STATEMENT]
lemma basis_enum_of_vec_inverse[simp]:
  fixes v::"complex vec"
  defines "n \<equiv> length (canonical_basis :: 'a::basis_enum list)"
  assumes f1: "dim_vec v = n"
  shows "vec_of_basis_enum ((basis_enum_of_vec v)::'a) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec v) = v
[PROOF STEP]
proof (rule eq_vecI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
 2. dim_vec (vec_of_basis_enum (basis_enum_of_vec v)) = dim_vec v
[PROOF STEP]
show \<open>dim_vec (vec_of_basis_enum (basis_enum_of_vec v :: 'a)) = dim_vec v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (basis_enum_of_vec v)) = dim_vec v
[PROOF STEP]
by (auto simp: vec_of_basis_enum_def f1 n_def)
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_basis_enum (basis_enum_of_vec v)) = dim_vec v

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
assume j_v: \<open>j < dim_vec v\<close>
[PROOF STATE]
proof (state)
this:
j < dim_vec v

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
define w where "w = list_of_vec v"
[PROOF STATE]
proof (state)
this:
w = list_of_vec v

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
define basis where "basis = (canonical_basis::'a list)"
[PROOF STATE]
proof (state)
this:
basis = canonical_basis

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have [simp]: "length w = n" "length basis = n" \<open>dim_vec v = n\<close> \<open>length (canonical_basis::'a list) = n\<close>
    \<open>j < n\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (length w = n &&& length basis = n) &&& dim_vec v = n &&& length canonical_basis = n &&& j < n
[PROOF STEP]
using j_v
[PROOF STATE]
proof (prove)
using this:
j < dim_vec v

goal (1 subgoal):
 1. (length w = n &&& length basis = n) &&& dim_vec v = n &&& length canonical_basis = n &&& j < n
[PROOF STEP]
by (auto simp: f1 basis_def w_def n_def)
[PROOF STATE]
proof (state)
this:
length w = n
length basis = n
dim_vec v = n
length canonical_basis = n
j < n

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have [simp]: \<open>cindependent (set basis)\<close> \<open>cspan (set basis) = UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent (set basis) &&& cspan (set basis) = UNIV
[PROOF STEP]
by (auto simp: basis_def is_cindependent_set is_generator_set)
[PROOF STATE]
proof (state)
this:
cindependent (set basis)
cspan (set basis) = UNIV

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have \<open>vec_of_basis_enum ((basis_enum_of_vec v)::'a) $ j
       = map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec v) $ j = map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j
[PROOF STEP]
by (auto simp: vec_of_list_index vec_of_basis_enum_def basis_enum_of_vec_def simp flip: w_def basis_def)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (basis_enum_of_vec v) $ j = map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (basis_enum_of_vec v) $ j = map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have \<open>\<dots> = crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis!j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j = crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j = crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis ! j)

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis))) basis ! j = crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis ! j)

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have \<open>\<dots> = crepresentation (set basis) (\<Sum>i<n. (w!i) *\<^sub>C (basis!i)) (basis!j)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis ! j) = crepresentation (set basis) (\<Sum>i<n. w ! i *\<^sub>C basis ! i) (basis ! j)
[PROOF STEP]
by (auto simp: sum_list_sum_nth atLeast0LessThan)
[PROOF STATE]
proof (state)
this:
crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis ! j) = crepresentation (set basis) (\<Sum>i<n. w ! i *\<^sub>C basis ! i) (basis ! j)

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
crepresentation (set basis) (sum_list (map2 (*\<^sub>C) w basis)) (basis ! j) = crepresentation (set basis) (\<Sum>i<n. w ! i *\<^sub>C basis ! i) (basis ! j)

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have \<open>\<dots> = (\<Sum>i<n. (w!i) *\<^sub>C crepresentation (set basis) (basis!i) (basis!j))\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation (set basis) (\<Sum>i<n. w ! i *\<^sub>C basis ! i) (basis ! j) = (\<Sum>i<n. w ! i *\<^sub>C crepresentation (set basis) (basis ! i) (basis ! j))
[PROOF STEP]
by (auto simp: complex_vector.representation_sum complex_vector.representation_scale)
[PROOF STATE]
proof (state)
this:
crepresentation (set basis) (\<Sum>i<n. w ! i *\<^sub>C basis ! i) (basis ! j) = (\<Sum>i<n. w ! i *\<^sub>C crepresentation (set basis) (basis ! i) (basis ! j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
crepresentation (set basis) (\<Sum>i<n. w ! i *\<^sub>C basis ! i) (basis ! j) = (\<Sum>i<n. w ! i *\<^sub>C crepresentation (set basis) (basis ! i) (basis ! j))

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have \<open>\<dots> = w!j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. w ! i *\<^sub>C crepresentation (set basis) (basis ! i) (basis ! j)) = w ! j
[PROOF STEP]
apply (subst sum_single[where i=j])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite {..<n}
 2. \<And>ja. \<lbrakk>ja \<noteq> j; ja \<in> {..<n}\<rbrakk> \<Longrightarrow> w ! ja *\<^sub>C crepresentation (set basis) (basis ! ja) (basis ! j) = 0
 3. (if j \<in> {..<n} then w ! j *\<^sub>C crepresentation (set basis) (basis ! j) (basis ! j) else 0) = w ! j
[PROOF STEP]
apply (auto simp: complex_vector.representation_basis)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ja. \<lbrakk>ja \<noteq> j; ja < n; basis ! j = basis ! ja\<rbrakk> \<Longrightarrow> w ! ja = 0
[PROOF STEP]
using \<open>j < n\<close> \<open>length basis = n\<close> basis_def distinct_canonical_basis nth_eq_iff_index_eq
[PROOF STATE]
proof (prove)
using this:
j < n
length basis = n
basis = canonical_basis
distinct canonical_basis
\<lbrakk>distinct ?xs; ?i < length ?xs; ?j < length ?xs\<rbrakk> \<Longrightarrow> (?xs ! ?i = ?xs ! ?j) = (?i = ?j)

goal (1 subgoal):
 1. \<And>ja. \<lbrakk>ja \<noteq> j; ja < n; basis ! j = basis ! ja\<rbrakk> \<Longrightarrow> w ! ja = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. w ! i *\<^sub>C crepresentation (set basis) (basis ! i) (basis ! j)) = w ! j

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. w ! i *\<^sub>C crepresentation (set basis) (basis ! i) (basis ! j)) = w ! j

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
have \<open>\<dots> = v $ j\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w ! j = v $ j
[PROOF STEP]
by (simp add: w_def)
[PROOF STATE]
proof (state)
this:
w ! j = v $ j

goal (1 subgoal):
 1. \<And>i. i < dim_vec v \<Longrightarrow> vec_of_basis_enum (basis_enum_of_vec v) $ i = v $ i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
vec_of_basis_enum (basis_enum_of_vec v) $ j = v $ j
[PROOF STEP]
show \<open>vec_of_basis_enum (basis_enum_of_vec v :: 'a) $ j = v $ j\<close>
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (basis_enum_of_vec v) $ j = v $ j

goal (1 subgoal):
 1. vec_of_basis_enum (basis_enum_of_vec v) $ j = v $ j
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (basis_enum_of_vec v) $ j = v $ j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_enum_eq_vec_of_basis_enumI:
  fixes a b :: "_::basis_enum"
  assumes "vec_of_basis_enum a = vec_of_basis_enum b"
  shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (metis assms vec_of_basis_enum_inverse)


[STATEMENT]
lemma basis_enum_of_vec_add:
  assumes [simp]: \<open>dim_vec v1 = length (canonical_basis :: 'a::basis_enum list)\<close>
    \<open>dim_vec v2 = length (canonical_basis :: 'a list)\<close>
  shows \<open>((basis_enum_of_vec (v1 + v2)) :: 'a) = basis_enum_of_vec v1 + basis_enum_of_vec v2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2
[PROOF STEP]
have \<open>length (list_of_vec v1) = length (list_of_vec v2)\<close> and \<open>length (list_of_vec v2) = length (canonical_basis :: 'a list)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (list_of_vec v1) = length (list_of_vec v2) &&& length (list_of_vec v2) = length canonical_basis
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
length (list_of_vec v1) = length (list_of_vec v2)
length (list_of_vec v2) = length canonical_basis

goal (1 subgoal):
 1. basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length (list_of_vec v1) = length (list_of_vec v2)
length (list_of_vec v2) = length canonical_basis
[PROOF STEP]
have \<open>sum_list (map2 (*\<^sub>C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) (canonical_basis::'a list))
    = sum_list (map2 (*\<^sub>C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*\<^sub>C) (list_of_vec v2) canonical_basis)\<close>
[PROOF STATE]
proof (prove)
using this:
length (list_of_vec v1) = length (list_of_vec v2)
length (list_of_vec v2) = length canonical_basis

goal (1 subgoal):
 1. sum_list (map2 (*\<^sub>C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) canonical_basis) = sum_list (map2 (*\<^sub>C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*\<^sub>C) (list_of_vec v2) canonical_basis)
[PROOF STEP]
apply (induction rule: list_induct3)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. sum_list (map2 (*\<^sub>C) (map2 (+) [] []) []) = sum_list (map2 (*\<^sub>C) [] []) + sum_list (map2 (*\<^sub>C) [] [])
 2. \<And>x xs y ys z zs. \<lbrakk>length xs = length ys; length ys = length zs; sum_list (map2 (*\<^sub>C) (map2 (+) xs ys) zs) = sum_list (map2 (*\<^sub>C) xs zs) + sum_list (map2 (*\<^sub>C) ys zs)\<rbrakk> \<Longrightarrow> sum_list (map2 (*\<^sub>C) (map2 (+) (x # xs) (y # ys)) (z # zs)) = sum_list (map2 (*\<^sub>C) (x # xs) (z # zs)) + sum_list (map2 (*\<^sub>C) (y # ys) (z # zs))
[PROOF STEP]
by (auto simp: scaleC_add_left)
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) canonical_basis) = sum_list (map2 (*\<^sub>C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*\<^sub>C) (list_of_vec v2) canonical_basis)

goal (1 subgoal):
 1. basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_list (map2 (*\<^sub>C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) canonical_basis) = sum_list (map2 (*\<^sub>C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*\<^sub>C) (list_of_vec v2) canonical_basis)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) canonical_basis) = sum_list (map2 (*\<^sub>C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*\<^sub>C) (list_of_vec v2) canonical_basis)

goal (1 subgoal):
 1. basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) (map2 (+) (list_of_vec v1) (list_of_vec v2)) canonical_basis) = sum_list (map2 (*\<^sub>C) (list_of_vec v1) canonical_basis) + sum_list (map2 (*\<^sub>C) (list_of_vec v2) canonical_basis)
dim_vec v1 = length canonical_basis
dim_vec v2 = length canonical_basis

goal (1 subgoal):
 1. basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2
[PROOF STEP]
by (auto simp: basis_enum_of_vec_def list_of_vec_plus)
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (v1 + v2) = basis_enum_of_vec v1 + basis_enum_of_vec v2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_enum_of_vec_mult:
  assumes [simp]: \<open>dim_vec v = length (canonical_basis :: 'a::basis_enum list)\<close>
  shows \<open>((basis_enum_of_vec (c \<cdot>\<^sub>v v)) :: 'a) =  c *\<^sub>C basis_enum_of_vec v\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (c \<cdot>\<^sub>v v) = c *\<^sub>C basis_enum_of_vec v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec (c \<cdot>\<^sub>v v) = c *\<^sub>C basis_enum_of_vec v
[PROOF STEP]
have *: \<open>monoid_add_hom ((*\<^sub>C) c :: 'a \<Rightarrow> _)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid_add_hom ((*\<^sub>C) c)
[PROOF STEP]
by (simp add: monoid_add_hom_def plus_hom.intro scaleC_add_right semigroup_add_hom.intro zero_hom.intro)
[PROOF STATE]
proof (state)
this:
monoid_add_hom ((*\<^sub>C) c)

goal (1 subgoal):
 1. basis_enum_of_vec (c \<cdot>\<^sub>v v) = c *\<^sub>C basis_enum_of_vec v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (c \<cdot>\<^sub>v v) = c *\<^sub>C basis_enum_of_vec v
[PROOF STEP]
apply (auto simp: basis_enum_of_vec_def list_of_vec_mult map_zip_map
        monoid_add_hom.hom_sum_list[OF *])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map2 (\<lambda>x. (*\<^sub>C) (c * x)) (list_of_vec v) canonical_basis) = sum_list (map ((*\<^sub>C) c \<circ> (\<lambda>(x, y). x *\<^sub>C y)) (zip (list_of_vec v) canonical_basis))
[PROOF STEP]
by (metis case_prod_unfold comp_apply scaleC_scaleC)
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (c \<cdot>\<^sub>v v) = c *\<^sub>C basis_enum_of_vec v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_add:
  "vec_of_basis_enum (b1 + b2) = vec_of_basis_enum b1 + vec_of_basis_enum b2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (b1 + b2) = vec_of_basis_enum b1 + vec_of_basis_enum b2
[PROOF STEP]
by (auto simp: vec_of_basis_enum_def complex_vector.representation_add)


[STATEMENT]
lemma vec_of_basis_enum_scaleC:
  "vec_of_basis_enum (c *\<^sub>C b) = c \<cdot>\<^sub>v (vec_of_basis_enum b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (c *\<^sub>C b) = c \<cdot>\<^sub>v vec_of_basis_enum b
[PROOF STEP]
by (auto simp: vec_of_basis_enum_def complex_vector.representation_scale)


[STATEMENT]
lemma vec_of_basis_enum_scaleR:
  "vec_of_basis_enum (r *\<^sub>R b) = complex_of_real r \<cdot>\<^sub>v (vec_of_basis_enum b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (r *\<^sub>R b) = complex_of_real r \<cdot>\<^sub>v vec_of_basis_enum b
[PROOF STEP]
by (simp add: scaleR_scaleC vec_of_basis_enum_scaleC)


[STATEMENT]
lemma vec_of_basis_enum_uminus:
  "vec_of_basis_enum (- b2) = - vec_of_basis_enum b2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (- b2) = - vec_of_basis_enum b2
[PROOF STEP]
unfolding scaleC_minus1_left[symmetric, of b2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (- 1 *\<^sub>C b2) = - vec_of_basis_enum b2
[PROOF STEP]
unfolding scaleC_minus1_left_vec[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (- 1 *\<^sub>C b2) = - 1 \<cdot>\<^sub>v vec_of_basis_enum b2
[PROOF STEP]
by (rule vec_of_basis_enum_scaleC)


[STATEMENT]
lemma vec_of_basis_enum_minus:
  "vec_of_basis_enum (b1 - b2) = vec_of_basis_enum b1 - vec_of_basis_enum b2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (b1 - b2) = vec_of_basis_enum b1 - vec_of_basis_enum b2
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) carrier_vec_dim_vec diff_conv_add_uminus diff_zero index_add_vec(2) minus_add_uminus_vec vec_of_basis_enum_add vec_of_basis_enum_uminus)


[STATEMENT]
lemma cscalar_prod_vec_of_basis_enum: "cscalar_prod (vec_of_basis_enum \<phi>) (vec_of_basis_enum \<psi>) = cinner \<psi> \<phi>"
  for \<psi> :: "'a::onb_enum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum \<phi> \<bullet>c vec_of_basis_enum \<psi> = \<psi> \<bullet>\<^sub>C \<phi>
[PROOF STEP]
apply (subst cinner_basis_enum_of_vec[symmetric, where 'a='a])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. dim_vec (vec_of_basis_enum \<psi>) = length canonical_basis
 2. dim_vec (vec_of_basis_enum \<phi>) = length canonical_basis
 3. basis_enum_of_vec (vec_of_basis_enum \<psi>) \<bullet>\<^sub>C basis_enum_of_vec (vec_of_basis_enum \<phi>) = \<psi> \<bullet>\<^sub>C \<phi>
[PROOF STEP]
by simp_all


[STATEMENT]
lemma norm_ell2_vec_of_basis_enum: "norm \<psi> =
  (let \<psi>' = vec_of_basis_enum \<psi> in
    sqrt (\<Sum> i \<in> {0 ..< dim_vec \<psi>'}. let z = vec_index \<psi>' i in (Re z)\<^sup>2 + (Im z)\<^sup>2))"
  (is "_ = ?rhs") for \<psi> :: "'a::onb_enum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
have "norm \<psi> = sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>).
            vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. norm \<psi> = sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i))
[PROOF STEP]
unfolding norm_eq_sqrt_cinner[where 'a='a] cscalar_prod_vec_of_basis_enum[symmetric] scalar_prod_def dim_vec_conjugate
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i)) = sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i))
[PROOF STEP]
by rule
[PROOF STATE]
proof (state)
this:
norm \<psi> = sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i))

goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
norm \<psi> = sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i))

goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
have "\<dots> = sqrt (cmod (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>).
                    let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i)) = sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2)))
[PROOF STEP]
apply (subst sum.cong, rule refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0..<dim_vec (vec_of_basis_enum \<psi>)} \<Longrightarrow> vec_of_basis_enum \<psi> $ x * conjugate (vec_of_basis_enum \<psi>) $ x = ?h x
 2. sqrt (cmod (sum ?h {0..<dim_vec (vec_of_basis_enum \<psi>)})) = sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2)))
[PROOF STEP]
apply (subst vec_index_conjugate)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> {0..<dim_vec (vec_of_basis_enum \<psi>)} \<Longrightarrow> x < dim_vec (vec_of_basis_enum \<psi>)
 2. \<And>x. x \<in> {0..<dim_vec (vec_of_basis_enum \<psi>)} \<Longrightarrow> vec_of_basis_enum \<psi> $ x * conjugate (vec_of_basis_enum \<psi> $ x) = ?h3 x x
 3. sqrt (cmod (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). ?h3 x x)) = sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2)))
[PROOF STEP]
by (auto simp: Let_def complex_mult_cnj)
[PROOF STATE]
proof (state)
this:
sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i)) = sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2)))

goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sqrt (cmod (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). vec_of_basis_enum \<psi> $ i * conjugate (vec_of_basis_enum \<psi>) $ i)) = sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2)))

goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
have "\<dots> = ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2))) = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
unfolding Let_def norm_of_real
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt \<bar>\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ x))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ x))\<^sup>2\<bar> = sqrt (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ i))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ i))\<^sup>2)
[PROOF STEP]
apply (subst abs_of_nonneg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ x))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ x))\<^sup>2)
 2. sqrt (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ x))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ x))\<^sup>2) = sqrt (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ i))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ i))\<^sup>2)
[PROOF STEP]
apply (rule sum_nonneg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> {0..<dim_vec (vec_of_basis_enum \<psi>)} \<Longrightarrow> 0 \<le> (Re (vec_of_basis_enum \<psi> $ x))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ x))\<^sup>2
 2. sqrt (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ x))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ x))\<^sup>2) = sqrt (\<Sum>i = 0..<dim_vec (vec_of_basis_enum \<psi>). (Re (vec_of_basis_enum \<psi> $ i))\<^sup>2 + (Im (vec_of_basis_enum \<psi> $ i))\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sqrt (cmod (complex_of_real (\<Sum>x = 0..<dim_vec (vec_of_basis_enum \<psi>). let z = vec_of_basis_enum \<psi> $ x in (Re z)\<^sup>2 + (Im z)\<^sup>2))) = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))

goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))

goal (1 subgoal):
 1. norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))
[PROOF STEP]
by -
[PROOF STATE]
proof (state)
this:
norm \<psi> = (let \<psi>' = vec_of_basis_enum \<psi> in sqrt (\<Sum>i = 0..<dim_vec \<psi>'. let z = \<psi>' $ i in (Re z)\<^sup>2 + (Im z)\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_enum_of_vec_unit_vec:
  defines "basis \<equiv> (canonical_basis::'a::basis_enum list)"
    and "n \<equiv> length (canonical_basis :: 'a list)"
  assumes a3: "i < n"
  shows "basis_enum_of_vec (unit_vec n i) = basis!i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
define L::"complex list" where "L = list_of_vec (unit_vec n i)"
[PROOF STATE]
proof (state)
this:
L = list_of_vec (unit_vec n i)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
define I::"nat list" where "I = [0..<n]"
[PROOF STATE]
proof (state)
this:
I = [0..<n]

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
have "length L = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length L = n
[PROOF STEP]
by (simp add: L_def)
[PROOF STATE]
proof (state)
this:
length L = n

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
length L = n

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
have "length basis = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length basis = n
[PROOF STEP]
by (simp add: basis_def n_def)
[PROOF STATE]
proof (state)
this:
length basis = n

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
length L = n
length basis = n
[PROOF STEP]
have "map2 (*\<^sub>C) L basis = map (\<lambda>j. L!j *\<^sub>C basis!j) I"
[PROOF STATE]
proof (prove)
using this:
length L = n
length basis = n

goal (1 subgoal):
 1. map2 (*\<^sub>C) L basis = map (\<lambda>j. L ! j *\<^sub>C basis ! j) I
[PROOF STEP]
by (simp add: I_def list_eq_iff_nth_eq)
[PROOF STATE]
proof (state)
this:
map2 (*\<^sub>C) L basis = map (\<lambda>j. L ! j *\<^sub>C basis ! j) I

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
hence "sum_list (map2 (*\<^sub>C) L basis) = sum_list (map (\<lambda>j. L!j *\<^sub>C basis!j) I)"
[PROOF STATE]
proof (prove)
using this:
map2 (*\<^sub>C) L basis = map (\<lambda>j. L ! j *\<^sub>C basis ! j) I

goal (1 subgoal):
 1. sum_list (map2 (*\<^sub>C) L basis) = (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) L basis) = (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) L basis) = (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
have "\<dots> = sum (\<lambda>j. L!j *\<^sub>C basis!j) {0..n-1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)
[PROOF STEP]
have "set I = {0..n-1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set I = {0..n - 1}
[PROOF STEP]
using I_def a3
[PROOF STATE]
proof (prove)
using this:
I = [0..<n]
i < n

goal (1 subgoal):
 1. set I = {0..n - 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set I = {0..n - 1}

goal (1 subgoal):
 1. (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set I = {0..n - 1}

goal (1 subgoal):
 1. (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)
[PROOF STEP]
using Groups_List.sum_code[where xs = I and g = "(\<lambda>j. L!j *\<^sub>C basis!j)"]
[PROOF STATE]
proof (prove)
using this:
set I = {0..n - 1}
(\<Sum>j\<in>set I. L ! j *\<^sub>C basis ! j) = (\<Sum>j\<leftarrow>remdups I. L ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. (\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)
[PROOF STEP]
by (simp add: I_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<leftarrow>I. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
have "\<dots> = sum (\<lambda>j. (list_of_vec (unit_vec n i))!j *\<^sub>C basis!j) {0..n-1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
unfolding L_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. L ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_list (map2 (*\<^sub>C) L basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
have "sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis)
       = sum (\<lambda>j. (list_of_vec (unit_vec n i))!j *\<^sub>C basis!j) {0..n-1}"
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) L basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
using L_def
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) L basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
L = list_of_vec (unit_vec n i)

goal (1 subgoal):
 1. sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
have "\<dots> = basis ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
have "(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) =
          (\<Sum>j \<in> {0..n - 1}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
have "\<dots> = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
               + (\<Sum>j \<in> {0..n - 1}-{i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
define a where "a j = list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j" for j
[PROOF STATE]
proof (state)
this:
a ?j = list_of_vec (unit_vec n i) ! ?j *\<^sub>C basis ! ?j

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
define S where "S = {0..n - 1}"
[PROOF STATE]
proof (state)
this:
S = {0..n - 1}

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
have "finite S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S
[PROOF STEP]
by (simp add: S_def)
[PROOF STATE]
proof (state)
this:
finite S

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
hence "(\<Sum>j \<in> insert i S. a j) = a i + (\<Sum>j\<in>S-{i}. a j)"
[PROOF STATE]
proof (prove)
using this:
finite S

goal (1 subgoal):
 1. sum a (insert i S) = a i + sum a (S - {i})
[PROOF STEP]
using Groups_Big.comm_monoid_add_class.sum.insert_remove
[PROOF STATE]
proof (prove)
using this:
finite S
finite ?A \<Longrightarrow> sum ?g (insert ?x ?A) = ?g ?x + sum ?g (?A - {?x})

goal (1 subgoal):
 1. sum a (insert i S) = a i + sum a (S - {i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum a (insert i S) = a i + sum a (S - {i})

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum a (insert i S) = a i + sum a (S - {i})

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
have "S-{i} = {0..n-1}-{i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S - {i} = {0..n - 1} - {i}
[PROOF STEP]
unfolding S_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..n - 1} - {i} = {0..n - 1} - {i}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
S - {i} = {0..n - 1} - {i}

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
S - {i} = {0..n - 1} - {i}

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
have "insert i S = {0..n-1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert i S = {0..n - 1}
[PROOF STEP]
using S_def Suc_diff_1 a3 atLeastAtMost_iff diff_is_0_eq' le_SucE le_numeral_extra(4)
          less_imp_le not_gr_zero
[PROOF STATE]
proof (prove)
using this:
S = {0..n - 1}
0 < ?n \<Longrightarrow> Suc (?n - 1) = ?n
i < n
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
?m \<le> ?n \<Longrightarrow> ?m - ?n = 0
\<lbrakk>?m \<le> Suc ?n; ?m \<le> ?n \<Longrightarrow> ?R; ?m = Suc ?n \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
(1::?'a) \<le> (1::?'a)
?x < ?y \<Longrightarrow> ?x \<le> ?y
(\<not> (0::?'a) < ?n) = (?n = (0::?'a))

goal (1 subgoal):
 1. insert i S = {0..n - 1}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
insert i S = {0..n - 1}

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum a (insert i S) = a i + sum a (S - {i})
S - {i} = {0..n - 1} - {i}
insert i S = {0..n - 1}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum a (insert i S) = a i + sum a (S - {i})
S - {i} = {0..n - 1} - {i}
insert i S = {0..n - 1}

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
using \<open>a \<equiv> \<lambda>j. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j\<close>
[PROOF STATE]
proof (prove)
using this:
sum a (insert i S) = a i + sum a (S - {i})
S - {i} = {0..n - 1} - {i}
insert i S = {0..n - 1}
a \<equiv> \<lambda>j. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
have "\<dots> = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
[PROOF STEP]
have "j \<in> {0..n - 1}-{i} \<Longrightarrow> list_of_vec (unit_vec n i) ! j = 0"
        for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! j = (0::'b)
[PROOF STEP]
using a3 atMost_atLeast0 atMost_iff diff_Suc_less index_unit_vec(1) le_less_trans
          list_of_vec_index member_remove zero_le
[PROOF STATE]
proof (prove)
using this:
i < n
{..?n} = {0..?n}
(?i \<in> {..?k}) = (?i \<le> ?k)
0 < ?n \<Longrightarrow> ?n - Suc ?i < ?n
\<lbrakk>?i < ?n; ?j < ?n\<rbrakk> \<Longrightarrow> unit_vec ?n ?i $ ?j = (if ?j = ?i then 1::?'a else (0::?'a))
\<lbrakk>?x \<le> ?y; ?y < ?z\<rbrakk> \<Longrightarrow> ?x < ?z
list_of_vec ?v ! ?j = ?v $ ?j
(?x \<in> Set.remove ?y ?A) = (?x \<in> ?A \<and> ?x \<noteq> ?y)
(0::?'a) \<le> ?x

goal (1 subgoal):
 1. j \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! j = (0::'b)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?j1 \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! ?j1 = (0::?'b2)

goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
[PROOF STEP]
hence "j \<in> {0..n - 1}-{i} \<Longrightarrow> list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j = 0"
        for j
[PROOF STATE]
proof (prove)
using this:
?j1 \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! ?j1 = (0::?'b2)

goal (1 subgoal):
 1. j \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?j1 \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! ?j1 *\<^sub>C basis ! ?j1 = (0::'a)

goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
[PROOF STEP]
hence "(\<Sum>j \<in> {0..n - 1}-{i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = 0"
[PROOF STATE]
proof (prove)
using this:
?j1 \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! ?j1 *\<^sub>C basis ! ?j1 = (0::'a)

goal (1 subgoal):
 1. (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (0::'a)
[PROOF STEP]
by (simp add: \<open>\<And>j. j \<in> {0..n - 1} - {i} \<Longrightarrow> list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j = 0\<close>)
[PROOF STATE]
proof (state)
this:
(\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (0::'a)

goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = (0::'a)

goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
have "\<dots> = basis ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i = basis ! i
[PROOF STEP]
by (simp add: a3)
[PROOF STATE]
proof (state)
this:
list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i = basis ! i

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
basis ! i = basis ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
basis ! i = basis ! i

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
using \<open>(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
             = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)\<close>
        \<open>list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
           = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i\<close>
        \<open>list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i = basis ! i\<close>
[PROOF STATE]
proof (prove)
using this:
basis ! i = basis ! i
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j)
list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i + (\<Sum>j\<in>{0..n - 1} - {i}. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i
list_of_vec (unit_vec n i) ! i *\<^sub>C basis ! i = basis ! i

goal (1 subgoal):
 1. (\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..n - 1. list_of_vec (unit_vec n i) ! j *\<^sub>C basis ! j) = basis ! i

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = basis ! i
[PROOF STEP]
have "sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis)
      = basis ! i"
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = basis ! i

goal (1 subgoal):
 1. sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = basis ! i
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = basis ! i

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
hence "sum_list (map2 scaleC (list_of_vec (unit_vec n i)) (canonical_basis::'a list))
      = (canonical_basis::'a list) ! i"
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) basis) = basis ! i

goal (1 subgoal):
 1. sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) canonical_basis) = canonical_basis ! i
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) canonical_basis) = canonical_basis ! i

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) canonical_basis) = canonical_basis ! i

goal (1 subgoal):
 1. basis_enum_of_vec (unit_vec n i) = basis ! i
[PROOF STEP]
unfolding basis_enum_of_vec_def
[PROOF STATE]
proof (prove)
using this:
sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) canonical_basis) = canonical_basis ! i

goal (1 subgoal):
 1. (if dim_vec (unit_vec n i) = length canonical_basis then sum_list (map2 (*\<^sub>C) (list_of_vec (unit_vec n i)) canonical_basis) else (0::'a)) = basis ! i
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
basis_enum_of_vec (unit_vec n i) = basis ! i

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_ket:
  "vec_of_basis_enum (ket i) = unit_vec (CARD('a)) (enum_idx i)"
  for i::"'a::enum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
have "dim_vec (vec_of_basis_enum (ket i))
      = dim_vec (unit_vec (CARD('a)) (enum_idx i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
have "dim_vec (unit_vec (CARD('a)) (enum_idx i))
      = CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (unit_vec CARD('a) (enum_idx i)) = CARD('a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (unit_vec CARD('a) (enum_idx i)) = CARD('a)

goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dim_vec (unit_vec CARD('a) (enum_idx i)) = CARD('a)

goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
have "dim_vec (vec_of_basis_enum (ket i)) = CARD('a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = CARD('a)
[PROOF STEP]
unfolding vec_of_basis_enum_def vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (vec_of_list (map (crepresentation (set canonical_basis) (ket i)) canonical_basis)) = CARD('a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_basis_enum (ket i)) = CARD('a)

goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dim_vec (unit_vec CARD('a) (enum_idx i)) = CARD('a)
dim_vec (vec_of_basis_enum (ket i)) = CARD('a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dim_vec (unit_vec CARD('a) (enum_idx i)) = CARD('a)
dim_vec (vec_of_basis_enum (ket i)) = CARD('a)

goal (1 subgoal):
 1. dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
have "vec_of_basis_enum (ket i) $ j =
    (unit_vec (CARD('a)) (enum_idx i)) $ j"
    if "j < dim_vec (vec_of_basis_enum (ket i))"
    for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have j_bound: "j < length (canonical_basis::'a ell2 list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length canonical_basis
[PROOF STEP]
by (metis dim_vec_of_basis_enum' that)
[PROOF STATE]
proof (state)
this:
j < length canonical_basis

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have y1: "cindependent (set (canonical_basis::'a ell2 list))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindependent (set canonical_basis)
[PROOF STEP]
using is_cindependent_set
[PROOF STATE]
proof (prove)
using this:
cindependent (set canonical_basis)

goal (1 subgoal):
 1. cindependent (set canonical_basis)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cindependent (set canonical_basis)

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have y2: "canonical_basis ! j \<in> set (canonical_basis::'a ell2 list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_basis ! j \<in> set canonical_basis
[PROOF STEP]
using j_bound
[PROOF STATE]
proof (prove)
using this:
j < length canonical_basis

goal (1 subgoal):
 1. canonical_basis ! j \<in> set canonical_basis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonical_basis ! j \<in> set canonical_basis

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have p1: "enum_class.enum ! enum_idx i = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_class.enum ! enum_idx i = i
[PROOF STEP]
using enum_idx_correct
[PROOF STATE]
proof (prove)
using this:
enum_class.enum ! enum_idx ?i = ?i

goal (1 subgoal):
 1. enum_class.enum ! enum_idx i = i
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
enum_class.enum ! enum_idx i = i

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enum_class.enum ! enum_idx i = i

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have p2: "(canonical_basis::'a ell2 list) ! t  = ket ((enum_class.enum::'a list) ! t)"
      if "t < length (enum_class.enum::'a list)"
      for t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. canonical_basis ! t = ket (enum_class.enum ! t)
[PROOF STEP]
unfolding canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ket enum_class.enum ! t = ket (enum_class.enum ! t)
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
t < length enum_class.enum

goal (1 subgoal):
 1. map ket enum_class.enum ! t = ket (enum_class.enum ! t)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?t1 < length enum_class.enum \<Longrightarrow> canonical_basis ! ?t1 = ket (enum_class.enum ! ?t1)

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?t1 < length enum_class.enum \<Longrightarrow> canonical_basis ! ?t1 = ket (enum_class.enum ! ?t1)

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have p3: "enum_idx i < length (enum_class.enum::'a list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
have "set (enum_class.enum::'a list) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set enum_class.enum = UNIV
[PROOF STEP]
using UNIV_enum
[PROOF STATE]
proof (prove)
using this:
UNIV = set enum_class.enum

goal (1 subgoal):
 1. set enum_class.enum = UNIV
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set enum_class.enum = UNIV

goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
hence "i \<in> set (enum_class.enum::'a list)"
[PROOF STATE]
proof (prove)
using this:
set enum_class.enum = UNIV

goal (1 subgoal):
 1. i \<in> set enum_class.enum
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
i \<in> set enum_class.enum

goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i \<in> set enum_class.enum

goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
unfolding enum_idx_def
[PROOF STATE]
proof (prove)
using this:
i \<in> set enum_class.enum

goal (1 subgoal):
 1. index_of i enum_class.enum < length enum_class.enum
[PROOF STEP]
by (metis index_of_bound length_greater_0_conv length_pos_if_in_set)
[PROOF STATE]
proof (state)
this:
enum_idx i < length enum_class.enum

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
enum_idx i < length enum_class.enum

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enum_class.enum ! enum_idx i = i
?t1 < length enum_class.enum \<Longrightarrow> canonical_basis ! ?t1 = ket (enum_class.enum ! ?t1)
enum_idx i < length enum_class.enum
[PROOF STEP]
have p4: "(canonical_basis::'a ell2 list) ! (enum_idx i)  = ket i"
[PROOF STATE]
proof (prove)
using this:
enum_class.enum ! enum_idx i = i
?t1 < length enum_class.enum \<Longrightarrow> canonical_basis ! ?t1 = ket (enum_class.enum ! ?t1)
enum_idx i < length enum_class.enum

goal (1 subgoal):
 1. canonical_basis ! enum_idx i = ket i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
canonical_basis ! enum_idx i = ket i

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have "enum_idx i < length (enum_class.enum::'a list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
using p3
[PROOF STATE]
proof (prove)
using this:
enum_idx i < length enum_class.enum

goal (1 subgoal):
 1. enum_idx i < length enum_class.enum
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enum_idx i < length enum_class.enum

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
enum_idx i < length enum_class.enum

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have "length (enum_class.enum::'a list) = dim_vec (vec_of_basis_enum (ket i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length enum_class.enum = dim_vec (vec_of_basis_enum (ket i))
[PROOF STEP]
unfolding vec_of_basis_enum_def canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length enum_class.enum = dim_vec (vec_of_list (map (crepresentation (set (map ket enum_class.enum)) (ket i)) (map ket enum_class.enum)))
[PROOF STEP]
using dim_vec_of_basis_enum'[where v = "ket i"]
[PROOF STATE]
proof (prove)
using this:
dim_vec (vec_of_basis_enum (ket i)) = length canonical_basis

goal (1 subgoal):
 1. length enum_class.enum = dim_vec (vec_of_list (map (crepresentation (set (map ket enum_class.enum)) (ket i)) (map ket enum_class.enum)))
[PROOF STEP]
unfolding canonical_basis_ell2_def
[PROOF STATE]
proof (prove)
using this:
dim_vec (vec_of_basis_enum (ket i)) = length (map ket enum_class.enum)

goal (1 subgoal):
 1. length enum_class.enum = dim_vec (vec_of_list (map (crepresentation (set (map ket enum_class.enum)) (ket i)) (map ket enum_class.enum)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length enum_class.enum = dim_vec (vec_of_basis_enum (ket i))

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
enum_idx i < length enum_class.enum
length enum_class.enum = dim_vec (vec_of_basis_enum (ket i))
[PROOF STEP]
have enum_i_dim_vec: "enum_idx i < dim_vec (unit_vec (CARD('a)) (enum_idx i))"
[PROOF STATE]
proof (prove)
using this:
enum_idx i < length enum_class.enum
length enum_class.enum = dim_vec (vec_of_basis_enum (ket i))

goal (1 subgoal):
 1. enum_idx i < dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
using \<open>dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec (CARD('a)) (enum_idx i))\<close>
[PROOF STATE]
proof (prove)
using this:
enum_idx i < length enum_class.enum
length enum_class.enum = dim_vec (vec_of_basis_enum (ket i))
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))

goal (1 subgoal):
 1. enum_idx i < dim_vec (unit_vec CARD('a) (enum_idx i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
enum_idx i < dim_vec (unit_vec CARD('a) (enum_idx i))

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
hence r1: "(unit_vec (CARD('a)) (enum_idx i)) $ j
        = (if enum_idx i = j then 1 else 0)"
[PROOF STATE]
proof (prove)
using this:
enum_idx i < dim_vec (unit_vec CARD('a) (enum_idx i))

goal (1 subgoal):
 1. unit_vec CARD('a) (enum_idx i) $ j = (if enum_idx i = j then 1::'b else (0::'b))
[PROOF STEP]
using \<open>dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec (CARD('a)) (enum_idx i))\<close> that
[PROOF STATE]
proof (prove)
using this:
enum_idx i < dim_vec (unit_vec CARD('a) (enum_idx i))
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
j < dim_vec (vec_of_basis_enum (ket i))

goal (1 subgoal):
 1. unit_vec CARD('a) (enum_idx i) $ j = (if enum_idx i = j then 1::'b else (0::'b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_vec CARD('a) (enum_idx i) $ j = (if enum_idx i = j then 1::?'b3 else (0::?'b3))

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
unit_vec CARD('a) (enum_idx i) $ j = (if enum_idx i = j then 1::?'b3 else (0::?'b3))

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
have "vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
proof(cases "enum_idx i = j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. enum_idx i = j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
 2. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
enum_idx i = j

goal (2 subgoals):
 1. enum_idx i = j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
 2. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
have "crepresentation (set (canonical_basis::'a ell2 list))
          ((canonical_basis::'a ell2 list) ! j) ((canonical_basis::'a ell2 list) ! j) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation (set canonical_basis) (canonical_basis ! j) (canonical_basis ! j) = 1
[PROOF STEP]
using y1 y2 complex_vector.representation_basis[where
            basis = "set (canonical_basis::'a ell2 list)"
            and b = "(canonical_basis::'a ell2 list) ! j"]
[PROOF STATE]
proof (prove)
using this:
cindependent (set canonical_basis)
canonical_basis ! j \<in> set canonical_basis
\<lbrakk>cindependent (set canonical_basis); canonical_basis ! j \<in> set canonical_basis\<rbrakk> \<Longrightarrow> crepresentation (set canonical_basis) (canonical_basis ! j) = (\<lambda>v. if v = canonical_basis ! j then 1 else 0)

goal (1 subgoal):
 1. crepresentation (set canonical_basis) (canonical_basis ! j) (canonical_basis ! j) = 1
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
crepresentation (set canonical_basis) (canonical_basis ! j) (canonical_basis ! j) = 1

goal (2 subgoals):
 1. enum_idx i = j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
 2. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! j) $ j = 1"
[PROOF STATE]
proof (prove)
using this:
crepresentation (set canonical_basis) (canonical_basis ! j) (canonical_basis ! j) = 1

goal (1 subgoal):
 1. vec_of_basis_enum (canonical_basis ! j) $ j = 1
[PROOF STEP]
unfolding vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
using this:
crepresentation (set canonical_basis) (canonical_basis ! j) (canonical_basis ! j) = 1

goal (1 subgoal):
 1. vec_of_list (map (crepresentation (set canonical_basis) (canonical_basis ! j)) canonical_basis) $ j = 1
[PROOF STEP]
by (metis j_bound nth_map vec_of_list_index)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (canonical_basis ! j) $ j = 1

goal (2 subgoals):
 1. enum_idx i = j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
 2. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! (enum_idx i))
            $ enum_idx i = 1"
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! j) $ j = 1

goal (1 subgoal):
 1. vec_of_basis_enum (canonical_basis ! enum_idx i) $ enum_idx i = 1
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! j) $ j = 1
enum_idx i = j

goal (1 subgoal):
 1. vec_of_basis_enum (canonical_basis ! enum_idx i) $ enum_idx i = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ enum_idx i = 1

goal (2 subgoals):
 1. enum_idx i = j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
 2. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
hence "vec_of_basis_enum (ket i) $ enum_idx i = 1"
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ enum_idx i = 1

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ enum_idx i = 1
[PROOF STEP]
using p4
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ enum_idx i = 1
canonical_basis ! enum_idx i = ket i

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ enum_idx i = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) $ enum_idx i = 1

goal (2 subgoals):
 1. enum_idx i = j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
 2. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (ket i) $ enum_idx i = 1

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (ket i) $ enum_idx i = 1
enum_idx i = j

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
unfolding vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
using this:
vec_of_list (map (crepresentation (set canonical_basis) (ket i)) canonical_basis) $ enum_idx i = 1
enum_idx i = j

goal (1 subgoal):
 1. vec_of_list (map (crepresentation (set canonical_basis) (ket i)) canonical_basis) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)

goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
enum_idx i \<noteq> j

goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
have "crepresentation (set (canonical_basis::'a ell2 list))
          ((canonical_basis::'a ell2 list) ! (enum_idx i)) ((canonical_basis::'a ell2 list) ! j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. crepresentation (set canonical_basis) (canonical_basis ! enum_idx i) (canonical_basis ! j) = 0
[PROOF STEP]
using y1 y2 complex_vector.representation_basis[where
            basis = "set (canonical_basis::'a ell2 list)"
            and b = "(canonical_basis::'a ell2 list) ! j"]
[PROOF STATE]
proof (prove)
using this:
cindependent (set canonical_basis)
canonical_basis ! j \<in> set canonical_basis
\<lbrakk>cindependent (set canonical_basis); canonical_basis ! j \<in> set canonical_basis\<rbrakk> \<Longrightarrow> crepresentation (set canonical_basis) (canonical_basis ! j) = (\<lambda>v. if v = canonical_basis ! j then 1 else 0)

goal (1 subgoal):
 1. crepresentation (set canonical_basis) (canonical_basis ! enum_idx i) (canonical_basis ! j) = 0
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) False enum_i_dim_vec basis_enum_of_vec_inverse
            basis_enum_of_vec_unit_vec canonical_basis_length_ell2 index_unit_vec(3) j_bound
            list_of_vec_index list_vec nth_map r1 vec_of_basis_enum_def)
[PROOF STATE]
proof (state)
this:
crepresentation (set canonical_basis) (canonical_basis ! enum_idx i) (canonical_basis ! j) = 0

goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! (enum_idx i)) $ j = 0"
[PROOF STATE]
proof (prove)
using this:
crepresentation (set canonical_basis) (canonical_basis ! enum_idx i) (canonical_basis ! j) = 0

goal (1 subgoal):
 1. vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0
[PROOF STEP]
unfolding vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
using this:
crepresentation (set canonical_basis) (canonical_basis ! enum_idx i) (canonical_basis ! j) = 0

goal (1 subgoal):
 1. vec_of_list (map (crepresentation (set canonical_basis) (canonical_basis ! enum_idx i)) canonical_basis) $ j = 0
[PROOF STEP]
by (smt j_bound nth_map vec_of_list_index)
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0

goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
hence "vec_of_basis_enum ((canonical_basis::'a ell2 list) ! (enum_idx i)) $ j = 0"
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0

goal (1 subgoal):
 1. vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0

goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
hence "vec_of_basis_enum (ket i) $ j = 0"
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = 0
[PROOF STEP]
using p4
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (canonical_basis ! enum_idx i) $ j = 0
canonical_basis ! enum_idx i = ket i

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) $ j = 0

goal (1 subgoal):
 1. enum_idx i \<noteq> j \<Longrightarrow> vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (ket i) $ j = 0

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
vec_of_basis_enum (ket i) $ j = 0
enum_idx i \<noteq> j

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
unfolding vec_of_basis_enum_def
[PROOF STATE]
proof (prove)
using this:
vec_of_list (map (crepresentation (set canonical_basis) (ket i)) canonical_basis) $ j = 0
enum_idx i \<noteq> j

goal (1 subgoal):
 1. vec_of_list (map (crepresentation (set canonical_basis) (ket i)) canonical_basis) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
unit_vec CARD('a) (enum_idx i) $ j = (if enum_idx i = j then 1::?'b3 else (0::?'b3))
vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
unit_vec CARD('a) (enum_idx i) $ j = (if enum_idx i = j then 1::?'b3 else (0::?'b3))
vec_of_basis_enum (ket i) $ j = (if enum_idx i = j then 1 else 0)

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) $ j = unit_vec CARD('a) (enum_idx i) $ j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?j1 < dim_vec (vec_of_basis_enum (ket i)) \<Longrightarrow> vec_of_basis_enum (ket i) $ ?j1 = unit_vec CARD('a) (enum_idx i) $ ?j1

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
?j1 < dim_vec (vec_of_basis_enum (ket i)) \<Longrightarrow> vec_of_basis_enum (ket i) $ ?j1 = unit_vec CARD('a) (enum_idx i) $ ?j1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
?j1 < dim_vec (vec_of_basis_enum (ket i)) \<Longrightarrow> vec_of_basis_enum (ket i) $ ?j1 = unit_vec CARD('a) (enum_idx i) $ ?j1

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
using Matrix.eq_vecI
[PROOF STATE]
proof (prove)
using this:
dim_vec (vec_of_basis_enum (ket i)) = dim_vec (unit_vec CARD('a) (enum_idx i))
?j1 < dim_vec (vec_of_basis_enum (ket i)) \<Longrightarrow> vec_of_basis_enum (ket i) $ ?j1 = unit_vec CARD('a) (enum_idx i) $ ?j1
\<lbrakk>\<And>i. i < dim_vec ?w \<Longrightarrow> ?v $ i = ?w $ i; dim_vec ?v = dim_vec ?w\<rbrakk> \<Longrightarrow> ?v = ?w

goal (1 subgoal):
 1. vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vec_of_basis_enum (ket i) = unit_vec CARD('a) (enum_idx i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vec_of_basis_enum_zero:
  defines "nA \<equiv> length (canonical_basis :: 'a::basis_enum list)"
  shows "vec_of_basis_enum (0::'a) = 0\<^sub>v nA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec_of_basis_enum (0::'a) = 0\<^sub>v nA
[PROOF STEP]
by (metis assms carrier_vecI dim_vec_of_basis_enum' minus_cancel_vec right_minus_eq vec_of_basis_enum_minus)