[STATEMENT]
lemma finsum_index:
  assumes i: "i < n"
    and f: "f \<in> X \<rightarrow> carrier_vec n"
    and X: "X \<subseteq> carrier_vec n"
  shows "finsum V f X $ i = sum (\<lambda>x. f x $ i) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum V f X $ i = (\<Sum>x\<in>X. f x $ i)
[PROOF STEP]
using X f
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n
f \<in> X \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. finsum V f X $ i = (\<Sum>x\<in>X. f x $ i)
[PROOF STEP]
proof (induct X rule: infinite_finite_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<lbrakk>{} \<subseteq> carrier_vec n; f \<in> {} \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f {} $ i = (\<Sum>x\<in>{}. f x $ i)
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<subseteq> carrier_vec n
f \<in> {} \<rightarrow> carrier_vec n

goal (3 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<lbrakk>{} \<subseteq> carrier_vec n; f \<in> {} \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f {} $ i = (\<Sum>x\<in>{}. f x $ i)
 3. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<subseteq> carrier_vec n
f \<in> {} \<rightarrow> carrier_vec n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> carrier_vec n
f \<in> {} \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. finsum V f {} $ i = (\<Sum>x\<in>{}. f x $ i)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> carrier_vec n
f \<in> {} \<rightarrow> carrier_vec n
i < n

goal (1 subgoal):
 1. finsum V f {} $ i = (\<Sum>x\<in>{}. f x $ i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finsum V f {} $ i = (\<Sum>x\<in>{}. f x $ i)

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
case (insert x X)
[PROOF STATE]
proof (state)
this:
finite X
x \<notin> X
\<lbrakk>X \<subseteq> carrier_vec n; f \<in> X \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f X $ i = (\<Sum>x\<in>X. f x $ i)
insert x X \<subseteq> carrier_vec n
f \<in> insert x X \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite X
x \<notin> X
\<lbrakk>X \<subseteq> carrier_vec n; f \<in> X \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f X $ i = (\<Sum>x\<in>X. f x $ i)
insert x X \<subseteq> carrier_vec n
f \<in> insert x X \<rightarrow> carrier_vec n
[PROOF STEP]
have Xf: "finite X"
      and xX: "x \<notin> X"
      and x: "x \<in> carrier_vec n"
      and X: "X \<subseteq> carrier_vec n"
      and fx: "f x \<in> carrier_vec n"
      and f: "f \<in> X \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
\<lbrakk>X \<subseteq> carrier_vec n; f \<in> X \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f X $ i = (\<Sum>x\<in>X. f x $ i)
insert x X \<subseteq> carrier_vec n
f \<in> insert x X \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. (finite X &&& x \<notin> X &&& x \<in> carrier_vec n) &&& X \<subseteq> carrier_vec n &&& f x \<in> carrier_vec n &&& f \<in> X \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite X
x \<notin> X
x \<in> carrier_vec n
X \<subseteq> carrier_vec n
f x \<in> carrier_vec n
f \<in> X \<rightarrow> carrier_vec n

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
have i2: "i < dim_vec (finsum V f X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_vec (finsum V f X)
[PROOF STEP]
using i finsum_closed[OF f]
[PROOF STATE]
proof (prove)
using this:
i < n
finsum V f X \<in> carrier_vec n

goal (1 subgoal):
 1. i < dim_vec (finsum V f X)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_vec (finsum V f X)

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
have ix: "i < dim_vec x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_vec x
[PROOF STEP]
using x i
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier_vec n
i < n

goal (1 subgoal):
 1. i < dim_vec x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_vec x

goal (2 subgoals):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; \<lbrakk>F \<subseteq> carrier_vec n; f \<in> F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f F $ i = (\<Sum>x\<in>F. f x $ i); insert x F \<subseteq> carrier_vec n; f \<in> insert x F \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f (insert x F) $ i = (\<Sum>x\<in>insert x F. f x $ i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finsum V f (insert x X) $ i = (\<Sum>x\<in>insert x X. f x $ i)
[PROOF STEP]
unfolding finsum_insert[OF Xf xX f fx]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x + finsum V f X) $ i = (\<Sum>x\<in>insert x X. f x $ i)
[PROOF STEP]
unfolding sum.insert[OF Xf xX]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x + finsum V f X) $ i = f x $ i + (\<Sum>x\<in>X. f x $ i)
[PROOF STEP]
unfolding index_add_vec(1)[OF i2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f x $ i + finsum V f X $ i = f x $ i + (\<Sum>x\<in>X. f x $ i)
[PROOF STEP]
using insert lincomb_def
[PROOF STATE]
proof (prove)
using this:
finite X
x \<notin> X
\<lbrakk>X \<subseteq> carrier_vec n; f \<in> X \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f X $ i = (\<Sum>x\<in>X. f x $ i)
insert x X \<subseteq> carrier_vec n
f \<in> insert x X \<rightarrow> carrier_vec n
lincomb ?a ?A = (\<Oplus>\<^bsub>V\<^esub>v\<in>?A. ?a v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f x $ i + finsum V f X $ i = f x $ i + (\<Sum>x\<in>X. f x $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finsum V f (insert x X) $ i = (\<Sum>x\<in>insert x X. f x $ i)

goal (1 subgoal):
 1. \<And>A. \<lbrakk>infinite A; A \<subseteq> carrier_vec n; f \<in> A \<rightarrow> carrier_vec n\<rbrakk> \<Longrightarrow> finsum V f A $ i = (\<Sum>x\<in>A. f x $ i)
[PROOF STEP]
qed (insert i, auto)


[STATEMENT]
lemma lincomb_index:
  assumes i: "i < n"
    and X: "X \<subseteq> carrier_vec n"
  shows "lincomb a X $ i = sum (\<lambda>x. a x * x $ i) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
let ?f = "\<lambda>x. a x \<cdot>\<^sub>v x"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
have f: "?f : X \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. a x \<cdot>\<^sub>v x) \<in> X \<rightarrow> carrier_vec n
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (\<lambda>x. a x \<cdot>\<^sub>v x) \<in> X \<rightarrow> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. a x \<cdot>\<^sub>v x) \<in> X \<rightarrow> carrier_vec n

goal (1 subgoal):
 1. lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
have point: "\<And>v. v \<in> X \<Longrightarrow> (a v \<cdot>\<^sub>v v) $ i = a v * v $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. v \<in> X \<Longrightarrow> (a v \<cdot>\<^sub>v v) $ i = a v * v $ i
[PROOF STEP]
using i X
[PROOF STATE]
proof (prove)
using this:
i < n
X \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>v. v \<in> X \<Longrightarrow> (a v \<cdot>\<^sub>v v) $ i = a v * v $ i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?v1 \<in> X \<Longrightarrow> (a ?v1 \<cdot>\<^sub>v ?v1) $ i = a ?v1 * ?v1 $ i

goal (1 subgoal):
 1. lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>X. a v \<cdot>\<^sub>v v) $ i = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
unfolding finsum_index[OF i f X]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>v\<in>X. (a v \<cdot>\<^sub>v v) $ i) = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
using point X
[PROOF STATE]
proof (prove)
using this:
?v1 \<in> X \<Longrightarrow> (a ?v1 \<cdot>\<^sub>v ?v1) $ i = a ?v1 * ?v1 $ i
X \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (\<Sum>v\<in>X. (a v \<cdot>\<^sub>v v) $ i) = (\<Sum>x\<in>X. a x * x $ i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb a X $ i = (\<Sum>x\<in>X. a x * x $ i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma append_insert: "set (xs @ [x]) = insert x (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs @ [x]) = insert x (set xs)
[PROOF STEP]
by simp


[STATEMENT]
lemma lincomb_units:
  assumes i: "i < n"
  shows "lincomb a (set (unit_vecs n)) $ i = a (unit_vec n i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a (set (unit_vecs n)) $ i = a (unit_vec n i)
[PROOF STEP]
unfolding lincomb_index[OF i unit_vecs_carrier]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
unfolding unit_vecs_first
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
let ?f = "\<lambda>m i. \<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
have zero:"\<And>m j. m \<le> j \<Longrightarrow> j < n \<Longrightarrow> ?f m j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>m j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a)
[PROOF STEP]
show "\<And>j. m \<le> j \<Longrightarrow> j < n \<Longrightarrow> ?f m j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a)
[PROOF STEP]
proof (induction m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ j) = (0::'a)
 2. \<And>m j. \<lbrakk>\<And>j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a); Suc m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ j) = (0::'a)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<lbrakk>m \<le> ?j1; ?j1 < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ ?j1) = (0::'a)
Suc m \<le> j
j < n

goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ j) = (0::'a)
 2. \<And>m j. \<lbrakk>\<And>j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a); Suc m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ j) = (0::'a)
[PROOF STEP]
hence mj:"m\<le>j" and mj':"m\<noteq>j" and jn:"j<n" and mn:"m<n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>m \<le> ?j1; ?j1 < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ ?j1) = (0::'a)
Suc m \<le> j
j < n

goal (1 subgoal):
 1. (m \<le> j &&& m \<noteq> j) &&& j < n &&& m < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
m \<le> j
m \<noteq> j
j < n
m < n

goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ j) = (0::'a)
 2. \<And>m j. \<lbrakk>\<And>j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a); Suc m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ j) = (0::'a)
[PROOF STEP]
hence mem: "unit_vec n m \<notin> set (unit_vecs_first n m)"
[PROOF STATE]
proof (prove)
using this:
m \<le> j
m \<noteq> j
j < n
m < n

goal (1 subgoal):
 1. unit_vec n m \<notin> set (unit_vecs_first n m)
[PROOF STEP]
apply(subst unit_vecs_first_distinct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>m \<le> j; m \<noteq> j; j < n; m < n\<rbrakk> \<Longrightarrow> m \<le> m
 2. \<lbrakk>m \<le> j; m \<noteq> j; j < n; m < n\<rbrakk> \<Longrightarrow> m < n
 3. \<lbrakk>m \<le> j; m \<noteq> j; j < n; m < n\<rbrakk> \<Longrightarrow> \<not> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_vec n m \<notin> set (unit_vecs_first n m)

goal (2 subgoals):
 1. \<And>j. \<lbrakk>0 \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ j) = (0::'a)
 2. \<And>m j. \<lbrakk>\<And>j. \<lbrakk>m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a); Suc m \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ j) = (0::'a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ j) = (0::'a)
[PROOF STEP]
unfolding unit_vecs_first.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n m @ [unit_vec n m]). a x * x $ j) = (0::'a)
[PROOF STEP]
unfolding append_insert
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>insert (unit_vec n m) (set (unit_vecs_first n m)). a x * x $ j) = (0::'a)
[PROOF STEP]
unfolding sum.insert[OF finite_set mem]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (unit_vec n m) * unit_vec n m $ j + (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a)
[PROOF STEP]
unfolding index_unit_vec(1)[OF mn jn]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (unit_vec n m) * (if j = m then 1::'a else (0::'a)) + (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ j) = (0::'a)
[PROOF STEP]
unfolding Suc(1)[OF mj jn]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (unit_vec n m) * (if j = m then 1::'a else (0::'a)) + (0::'a) = (0::'a)
[PROOF STEP]
using mj'
[PROOF STATE]
proof (prove)
using this:
m \<noteq> j

goal (1 subgoal):
 1. a (unit_vec n m) * (if j = m then 1::'a else (0::'a)) + (0::'a) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ j) = (0::'a)

goal (1 subgoal):
 1. \<And>j. \<lbrakk>0 \<le> j; j < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ j) = (0::'a)
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>m \<le> ?j1; ?j1 < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ ?j1) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m1 \<le> ?j1; ?j1 < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n ?m1). a x * x $ ?j1) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m1 \<le> ?j1; ?j1 < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n ?m1). a x * x $ ?j1) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
have "i < m \<Longrightarrow> m \<le> n \<Longrightarrow> ?f m i = a (unit_vec n i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
proof (induction m arbitrary: i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < 0; 0 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ i) = a (unit_vec n i)
 2. \<And>m i. \<lbrakk>\<And>i. \<lbrakk>i < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i); i < Suc m; Suc m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
case (Suc m)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ ?i1) = a (unit_vec n ?i1)
i < Suc m
Suc m \<le> n

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < 0; 0 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ i) = a (unit_vec n i)
 2. \<And>m i. \<lbrakk>\<And>i. \<lbrakk>i < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i); i < Suc m; Suc m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
hence iSm: "i < Suc m" and i:"i<n" and mn: "m<n"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ ?i1) = a (unit_vec n ?i1)
i < Suc m
Suc m \<le> n

goal (1 subgoal):
 1. i < Suc m &&& i < n &&& m < n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < Suc m
i < n
m < n

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < 0; 0 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ i) = a (unit_vec n i)
 2. \<And>m i. \<lbrakk>\<And>i. \<lbrakk>i < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i); i < Suc m; Suc m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
hence mem: "unit_vec n m \<notin> set (unit_vecs_first n m)"
[PROOF STATE]
proof (prove)
using this:
i < Suc m
i < n
m < n

goal (1 subgoal):
 1. unit_vec n m \<notin> set (unit_vecs_first n m)
[PROOF STEP]
apply(subst unit_vecs_first_distinct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i < Suc m; i < n; m < n\<rbrakk> \<Longrightarrow> m \<le> m
 2. \<lbrakk>i < Suc m; i < n; m < n\<rbrakk> \<Longrightarrow> m < n
 3. \<lbrakk>i < Suc m; i < n; m < n\<rbrakk> \<Longrightarrow> \<not> False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
unit_vec n m \<notin> set (unit_vecs_first n m)

goal (2 subgoals):
 1. \<And>i. \<lbrakk>i < 0; 0 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ i) = a (unit_vec n i)
 2. \<And>m i. \<lbrakk>\<And>i. \<lbrakk>i < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i); i < Suc m; Suc m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
unfolding unit_vecs_first.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n m @ [unit_vec n m]). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
unfolding append_insert
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>insert (unit_vec n m) (set (unit_vecs_first n m)). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
unfolding sum.insert[OF finite_set mem]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (unit_vec n m) * unit_vec n m $ i + (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
unfolding index_unit_vec(1)[OF mn i]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a (unit_vec n m) * (if i = m then 1::'a else (0::'a)) + (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
using zero Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?m1 \<le> ?j1; ?j1 < n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n ?m1). a x * x $ ?j1) = (0::'a)
\<lbrakk>?i1 < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ ?i1) = a (unit_vec n ?i1)
i < Suc m
Suc m \<le> n

goal (1 subgoal):
 1. a (unit_vec n m) * (if i = m then 1::'a else (0::'a)) + (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
by (cases "i = m",auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (unit_vecs_first n (Suc m)). a x * x $ i) = a (unit_vec n i)

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < 0; 0 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n 0). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < m; m \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n m). a x * x $ i) = a (unit_vec n i)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>i < ?m3; ?m3 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n ?m3). a x * x $ i) = a (unit_vec n i)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
thus "?f n i = a (unit_vec n i)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < ?m3; ?m3 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n ?m3). a x * x $ i) = a (unit_vec n i)

goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < ?m3; ?m3 \<le> n\<rbrakk> \<Longrightarrow> (\<Sum>x\<in>set (unit_vecs_first n ?m3). a x * x $ i) = a (unit_vec n i)
i < n

goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (unit_vecs_first n n). a x * x $ i) = a (unit_vec n i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lincomb_coordinates:
  assumes v: "v : carrier_vec n"
  defines "a \<equiv> (\<lambda>u. v $ (THE i. u = unit_vec n i))"
  shows "lincomb a (set (unit_vecs n)) = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a (set (unit_vecs n)) = v
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb a (set (unit_vecs n)) = v
[PROOF STEP]
have a: "a \<in> set (unit_vecs n) \<rightarrow> UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> set (unit_vecs n) \<rightarrow> UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> set (unit_vecs n) \<rightarrow> UNIV

goal (1 subgoal):
 1. lincomb a (set (unit_vecs n)) = v
[PROOF STEP]
have fvu: "\<And>i. i < n \<Longrightarrow> v $ i = a (unit_vec n i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> v $ i = a (unit_vec n i)
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> v $ i = v $ (THE ia. unit_vec n i = unit_vec n ia)
[PROOF STEP]
using unit_vec_eq
[PROOF STATE]
proof (prove)
using this:
?i < ?n \<Longrightarrow> (unit_vec ?n ?i = unit_vec ?n ?j) = (?i = ?j)

goal (1 subgoal):
 1. \<And>i. i < n \<Longrightarrow> v $ i = v $ (THE ia. unit_vec n i = unit_vec n ia)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < n \<Longrightarrow> v $ ?i1 = a (unit_vec n ?i1)

goal (1 subgoal):
 1. lincomb a (set (unit_vecs n)) = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a (set (unit_vecs n)) = v
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec v \<Longrightarrow> lincomb a (set (unit_vecs n)) $ i = v $ i
 2. dim_vec (lincomb a (set (unit_vecs n))) = dim_vec v
[PROOF STEP]
unfolding lincomb_dim[OF finite_set unit_vecs_carrier]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. i < dim_vec v \<Longrightarrow> lincomb a (set (unit_vecs n)) $ i = v $ i
 2. n = dim_vec v
[PROOF STEP]
using v lincomb_units fvu
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
?i < n \<Longrightarrow> lincomb ?a (set (unit_vecs n)) $ ?i = ?a (unit_vec n ?i)
?i1 < n \<Longrightarrow> v $ ?i1 = a (unit_vec n ?i1)

goal (2 subgoals):
 1. \<And>i. i < dim_vec v \<Longrightarrow> lincomb a (set (unit_vecs n)) $ i = v $ i
 2. n = dim_vec v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a (set (unit_vecs n)) = v

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma span_unit_vecs_is_carrier: "span (set (unit_vecs n)) = carrier_vec n" (is "?L = ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set (unit_vecs n)) = carrier_vec n
[PROOF STEP]
proof (rule;rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> local.span (set (unit_vecs n)) \<Longrightarrow> x \<in> carrier_vec n
 2. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> local.span (set (unit_vecs n)) \<Longrightarrow> x \<in> carrier_vec n
 2. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
assume vsU: "v \<in> ?L"
[PROOF STATE]
proof (state)
this:
v \<in> local.span (set (unit_vecs n))

goal (2 subgoals):
 1. \<And>x. x \<in> local.span (set (unit_vecs n)) \<Longrightarrow> x \<in> carrier_vec n
 2. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
show "v \<in> ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
obtain a
      where v: "v = lincomb a (set (unit_vecs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. v = lincomb a (set (unit_vecs n)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using vsU
[PROOF STATE]
proof (prove)
using this:
v \<in> local.span (set (unit_vecs n))

goal (1 subgoal):
 1. (\<And>a. v = lincomb a (set (unit_vecs n)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding finite_span[OF finite_set unit_vecs_carrier]
[PROOF STATE]
proof (prove)
using this:
v \<in> {uu_. \<exists>a. uu_ = lincomb a (set (unit_vecs n))}

goal (1 subgoal):
 1. (\<And>a. v = lincomb a (set (unit_vecs n)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = lincomb a (set (unit_vecs n))

goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v = lincomb a (set (unit_vecs n))

goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
using lincomb_closed[OF unit_vecs_carrier]
[PROOF STATE]
proof (prove)
using this:
v = lincomb a (set (unit_vecs n))
lincomb ?a (set (unit_vecs n)) \<in> carrier_vec n

goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
fix v::"'a vec"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
assume v: "v \<in> ?R"
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>x. x \<in> carrier_vec n \<Longrightarrow> x \<in> local.span (set (unit_vecs n))
[PROOF STEP]
show "v \<in> ?L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.span (set (unit_vecs n))
[PROOF STEP]
unfolding span_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> set (unit_vecs n)}
[PROOF STEP]
using lincomb_coordinates[OF v,symmetric]
[PROOF STATE]
proof (prove)
using this:
v = lincomb (\<lambda>u. v $ (THE i. u = unit_vec n i)) (set (unit_vecs n))

goal (1 subgoal):
 1. v \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> set (unit_vecs n)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> local.span (set (unit_vecs n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin_dim[simp]: "fin_dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fin_dim
[PROOF STEP]
unfolding fin_dim_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>A. finite A \<and> A \<subseteq> carrier_vec n \<and> local.span A = carrier_vec n
[PROOF STEP]
apply (intro eqTrueI exI conjI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. finite ?A
 2. ?A \<subseteq> carrier_vec n
 3. local.span ?A = carrier_vec n
[PROOF STEP]
using span_unit_vecs_is_carrier unit_vecs_carrier
[PROOF STATE]
proof (prove)
using this:
local.span (set (unit_vecs n)) = carrier_vec n
set (unit_vecs ?n) \<subseteq> carrier_vec ?n

goal (3 subgoals):
 1. finite ?A
 2. ?A \<subseteq> carrier_vec n
 3. local.span ?A = carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma unit_vecs_basis: "basis (set (unit_vecs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis (set (unit_vecs n))
[PROOF STEP]
unfolding basis_def span_unit_vecs_is_carrier
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (set (unit_vecs n)) \<and> carrier_vec n = carrier_vec n \<and> set (unit_vecs n) \<subseteq> carrier_vec n
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lin_indpt (set (unit_vecs n))
 2. carrier_vec n = carrier_vec n
 3. set (unit_vecs n) \<subseteq> carrier_vec n
[PROOF STEP]
show "\<not> lin_dep (set (unit_vecs n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (set (unit_vecs n))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
assume "lin_dep (set (unit_vecs n))"
[PROOF STATE]
proof (state)
this:
lin_dep (set (unit_vecs n))

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
from this[unfolded lin_dep_def]
[PROOF STATE]
proof (chain)
picking this:
\<exists>A a v. finite A \<and> A \<subseteq> set (unit_vecs n) \<and> True \<and> lincomb a A = 0\<^sub>v n \<and> v \<in> A \<and> a v \<noteq> (0::'a)
[PROOF STEP]
obtain A a v where
      fin: "finite A" and A: "A \<subseteq> set (unit_vecs n)"
      and lc: "lincomb a A = 0\<^sub>v n" and v: "v \<in> A" and av: "a v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>A a v. finite A \<and> A \<subseteq> set (unit_vecs n) \<and> True \<and> lincomb a A = 0\<^sub>v n \<and> v \<in> A \<and> a v \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>A a v. \<lbrakk>finite A; A \<subseteq> set (unit_vecs n); lincomb a A = 0\<^sub>v n; v \<in> A; a v \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite A
A \<subseteq> set (unit_vecs n)
lincomb a A = 0\<^sub>v n
v \<in> A
a v \<noteq> (0::'a)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
from v A
[PROOF STATE]
proof (chain)
picking this:
v \<in> A
A \<subseteq> set (unit_vecs n)
[PROOF STEP]
obtain i where i: "i < n" and vu: "v = unit_vec n i"
[PROOF STATE]
proof (prove)
using this:
v \<in> A
A \<subseteq> set (unit_vecs n)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; v = unit_vec n i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding unit_vecs_def
[PROOF STATE]
proof (prove)
using this:
v \<in> A
A \<subseteq> set (map (unit_vec n) [0..<n])

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < n; v = unit_vec n i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < n
v = unit_vec n i

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
define b where "b = (\<lambda> x. if x \<in> A then a x else 0)"
[PROOF STATE]
proof (state)
this:
b = (\<lambda>x. if x \<in> A then a x else (0::'a))

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
have id: "A \<union> (set (unit_vecs n) - A) = set (unit_vecs n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<union> (set (unit_vecs n) - A) = set (unit_vecs n)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set (unit_vecs n)

goal (1 subgoal):
 1. A \<union> (set (unit_vecs n) - A) = set (unit_vecs n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<union> (set (unit_vecs n) - A) = set (unit_vecs n)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
from lincomb_index[OF i unit_vecs_carrier]
[PROOF STATE]
proof (chain)
picking this:
lincomb ?a (set (unit_vecs n)) $ i = (\<Sum>x\<in>set (unit_vecs n). ?a x * x $ i)
[PROOF STEP]
have "lincomb b (set (unit_vecs n)) $ i = (\<Sum>x\<in> (A \<union> (set (unit_vecs n) - A)). b x * x $ i)"
[PROOF STATE]
proof (prove)
using this:
lincomb ?a (set (unit_vecs n)) $ i = (\<Sum>x\<in>set (unit_vecs n). ?a x * x $ i)

goal (1 subgoal):
 1. lincomb b (set (unit_vecs n)) $ i = (\<Sum>x\<in>A \<union> (set (unit_vecs n) - A). b x * x $ i)
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
lincomb ?a (set (unit_vecs n)) $ i = (\<Sum>x\<in>set (unit_vecs n). ?a x * x $ i)

goal (1 subgoal):
 1. lincomb b (set (unit_vecs n)) $ i = (\<Sum>x\<in>set (unit_vecs n). b x * x $ i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb b (set (unit_vecs n)) $ i = (\<Sum>x\<in>A \<union> (set (unit_vecs n) - A). b x * x $ i)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb b (set (unit_vecs n)) $ i = (\<Sum>x\<in>A \<union> (set (unit_vecs n) - A). b x * x $ i)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (\<Sum>x\<in> A. b x * x $ i) + (\<Sum>x\<in> set (unit_vecs n) - A. b x * x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>A \<union> (set (unit_vecs n) - A). b x * x $ i) = (\<Sum>x\<in>A. b x * x $ i) + (\<Sum>x\<in>set (unit_vecs n) - A. b x * x $ i)
[PROOF STEP]
by (rule sum.union_disjoint, insert fin, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>A \<union> (set (unit_vecs n) - A). b x * x $ i) = (\<Sum>x\<in>A. b x * x $ i) + (\<Sum>x\<in>set (unit_vecs n) - A. b x * x $ i)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>A \<union> (set (unit_vecs n) - A). b x * x $ i) = (\<Sum>x\<in>A. b x * x $ i) + (\<Sum>x\<in>set (unit_vecs n) - A. b x * x $ i)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
have "(\<Sum>x\<in> A. b x * x $ i) = (\<Sum>x\<in> A. a x * x $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>A. b x * x $ i) = (\<Sum>x\<in>A. a x * x $ i)
[PROOF STEP]
by (rule sum.cong, auto simp: b_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>A. b x * x $ i) = (\<Sum>x\<in>A. a x * x $ i)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>A. b x * x $ i) = (\<Sum>x\<in>A. a x * x $ i)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = lincomb a A $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>A. a x * x $ i) = lincomb a A $ i
[PROOF STEP]
by (subst lincomb_index[OF i], insert A unit_vecs_carrier, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>A. a x * x $ i) = lincomb a A $ i

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>A. a x * x $ i) = lincomb a A $ i

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a A $ i = (0::'a)
[PROOF STEP]
unfolding lc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n $ i = (0::'a)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < n

goal (1 subgoal):
 1. 0\<^sub>v n $ i = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb a A $ i = (0::'a)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb a A $ i = (0::'a)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
have "(\<Sum>x\<in> set (unit_vecs n) - A. b x * x $ i) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>set (unit_vecs n) - A. b x * x $ i) = (0::'a)
[PROOF STEP]
by (rule sum.neutral, auto simp: b_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<in>set (unit_vecs n) - A. b x * x $ i) = (0::'a)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb b (set (unit_vecs n)) $ i = (0::'a) + (0::'a)
[PROOF STEP]
have "lincomb b (set (unit_vecs n)) $ i = 0"
[PROOF STATE]
proof (prove)
using this:
lincomb b (set (unit_vecs n)) $ i = (0::'a) + (0::'a)

goal (1 subgoal):
 1. lincomb b (set (unit_vecs n)) $ i = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb b (set (unit_vecs n)) $ i = (0::'a)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
from lincomb_units[OF i, of b, unfolded this]
[PROOF STATE]
proof (chain)
picking this:
(0::'a) = b (unit_vec n i)
[PROOF STEP]
have "b v = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) = b (unit_vec n i)

goal (1 subgoal):
 1. b v = (0::'a)
[PROOF STEP]
unfolding vu
[PROOF STATE]
proof (prove)
using this:
(0::'a) = b (unit_vec n i)

goal (1 subgoal):
 1. b (unit_vec n i) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b v = (0::'a)

goal (1 subgoal):
 1. lin_dep (set (unit_vecs n)) \<Longrightarrow> False
[PROOF STEP]
with v av
[PROOF STATE]
proof (chain)
picking this:
v \<in> A
a v \<noteq> (0::'a)
b v = (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v \<in> A
a v \<noteq> (0::'a)
b v = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
using this:
v \<in> A
a v \<noteq> (0::'a)
(if v \<in> A then a v else (0::'a)) = (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_indpt (set (unit_vecs n))

goal (2 subgoals):
 1. carrier_vec n = carrier_vec n
 2. set (unit_vecs n) \<subseteq> carrier_vec n
[PROOF STEP]
qed (insert unit_vecs_carrier, auto)


[STATEMENT]
lemma unit_vecs_length[simp]: "length (unit_vecs n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (unit_vecs n) = n
[PROOF STEP]
unfolding unit_vecs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (unit_vec n) [0..<n]) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma unit_vecs_distinct: "distinct (unit_vecs n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (unit_vecs n)
[PROOF STEP]
unfolding distinct_conv_nth unit_vecs_length
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<n. \<forall>j<n. i \<noteq> j \<longrightarrow> unit_vecs n ! i \<noteq> unit_vecs n ! j
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < n; j < n; i \<noteq> j\<rbrakk> \<Longrightarrow> unit_vecs n ! i \<noteq> unit_vecs n ! j
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < n; j < n; i \<noteq> j\<rbrakk> \<Longrightarrow> unit_vecs n ! i \<noteq> unit_vecs n ! j
[PROOF STEP]
assume *: "i < n" "j < n" "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i < n
j < n
i \<noteq> j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < n; j < n; i \<noteq> j\<rbrakk> \<Longrightarrow> unit_vecs n ! i \<noteq> unit_vecs n ! j
[PROOF STEP]
show "unit_vecs n ! i \<noteq> unit_vecs n ! j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unit_vecs n ! i \<noteq> unit_vecs n ! j
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. unit_vecs n ! i = unit_vecs n ! j \<Longrightarrow> False
[PROOF STEP]
assume "unit_vecs n ! i = unit_vecs n ! j"
[PROOF STATE]
proof (state)
this:
unit_vecs n ! i = unit_vecs n ! j

goal (1 subgoal):
 1. unit_vecs n ! i = unit_vecs n ! j \<Longrightarrow> False
[PROOF STEP]
from arg_cong[OF this, of "\<lambda> v. v $ i"]
[PROOF STATE]
proof (chain)
picking this:
unit_vecs n ! i $ i = unit_vecs n ! j $ i
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
unit_vecs n ! i $ i = unit_vecs n ! j $ i

goal (1 subgoal):
 1. False
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
unit_vecs n ! i $ i = unit_vecs n ! j $ i
i < n
j < n
i \<noteq> j

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding unit_vecs_def
[PROOF STATE]
proof (prove)
using this:
map (unit_vec n) [0..<n] ! i $ i = map (unit_vec n) [0..<n] ! j $ i
i < n
j < n
i \<noteq> j

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
unit_vecs n ! i \<noteq> unit_vecs n ! j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_is_n: "dim = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dim = n
[PROOF STEP]
unfolding dim_basis[OF finite_set unit_vecs_basis]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (unit_vecs n)) = n
[PROOF STEP]
unfolding distinct_card[OF unit_vecs_distinct]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (unit_vecs n) = n
[PROOF STEP]
by simp


[STATEMENT]
lemma fin_dim_span:
assumes "finite A" "A \<subseteq> carrier V"
shows "vectorspace.fin_dim class_ring (vs (span A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
have "vectorspace class_ring (span_vs A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace class_ring (vs (local.span A))
[PROOF STEP]
using assms span_is_subspace subspace_def subspace_is_vs
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> carrier V
?S \<subseteq> carrier_vec n \<Longrightarrow> subspace class_ring (local.span ?S) V
subspace ?K ?W ?V \<equiv> vectorspace ?K ?V \<and> LinearCombinations.submodule ?K ?W ?V
subspace class_ring ?W V \<Longrightarrow> vectorspace class_ring (vs ?W)

goal (1 subgoal):
 1. vectorspace class_ring (vs (local.span A))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vectorspace class_ring (vs (local.span A))

goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
have "A \<subseteq> span A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> local.span A
[PROOF STEP]
using assms in_own_span
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> carrier V
?S \<subseteq> carrier_vec n \<Longrightarrow> ?S \<subseteq> local.span ?S

goal (1 subgoal):
 1. A \<subseteq> local.span A
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<subseteq> local.span A

goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
have "submodule class_ring (span A) V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LinearCombinations.submodule class_ring (local.span A) V
[PROOF STEP]
using assms span_is_submodule
[PROOF STATE]
proof (prove)
using this:
finite A
A \<subseteq> carrier V
?S \<subseteq> carrier_vec n \<Longrightarrow> LinearCombinations.submodule class_ring (local.span ?S) V

goal (1 subgoal):
 1. LinearCombinations.submodule class_ring (local.span A) V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
LinearCombinations.submodule class_ring (local.span A) V

goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
have "LinearCombinations.module.span class_ring (vs (span A)) A = carrier (vs (span A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))
[PROOF STEP]
using  span_li_not_depend(1)[OF \<open>A \<subseteq> span A\<close> \<open>submodule class_ring (span A) V\<close>]
[PROOF STATE]
proof (prove)
using this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = local.span A

goal (1 subgoal):
 1. LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))

goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))

goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span A))
[PROOF STEP]
unfolding vectorspace.fin_dim_def[OF \<open>vectorspace class_ring (span_vs A)\<close>]
[PROOF STATE]
proof (prove)
using this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))

goal (1 subgoal):
 1. \<exists>Aa. finite Aa \<and> Aa \<subseteq> carrier (vs (local.span A)) \<and> LinearCombinations.module.span class_ring (vs (local.span A)) Aa = carrier (vs (local.span A))
[PROOF STEP]
using List.finite_set \<open>A \<subseteq> span A\<close> \<open>vectorspace class_ring (vs (span A))\<close>
    vec_vs vectorspace.carrier_vs_is_self[OF \<open>vectorspace class_ring (span_vs A)\<close>]
[PROOF STATE]
proof (prove)
using this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))
finite (set ?xs)
A \<subseteq> local.span A
vectorspace class_ring (vs (local.span A))
vectorspace class_ring (module_vec TYPE(?'a) ?n)
carrier (vs (local.span A)\<lparr>carrier := ?W\<rparr>) = ?W

goal (1 subgoal):
 1. \<exists>Aa. finite Aa \<and> Aa \<subseteq> carrier (vs (local.span A)) \<and> LinearCombinations.module.span class_ring (vs (local.span A)) Aa = carrier (vs (local.span A))
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
LinearCombinations.module.span class_ring (vs (local.span A)) A = carrier (vs (local.span A))
finite (set ?xs)
A \<subseteq> local.span A
vectorspace class_ring (vs (local.span A))
vectorspace class_ring (module_vec TYPE(?'a) ?n)
carrier (vs (local.span A)\<lparr>carrier := ?W\<rparr>) = ?W
finite A

goal (1 subgoal):
 1. \<exists>Aa. finite Aa \<and> Aa \<subseteq> carrier (vs (local.span A)) \<and> LinearCombinations.module.span class_ring (vs (local.span A)) Aa = carrier (vs (local.span A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vectorspace.fin_dim class_ring (vs (local.span A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fin_dim_span_cols:
assumes "A \<in> carrier_mat n nc"
shows "vectorspace.fin_dim class_ring (vs (span (set (cols A))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span (set (cols A))))
[PROOF STEP]
using fin_dim_span cols_dim List.finite_set assms carrier_matD(1) module_vec_simps(3)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; ?A \<subseteq> carrier V\<rbrakk> \<Longrightarrow> vectorspace.fin_dim class_ring (vs (local.span ?A))
set (cols ?A) \<subseteq> carrier_vec (dim_row ?A)
finite (set ?xs)
A \<in> carrier_mat n nc
?A \<in> carrier_mat ?nr ?nc \<Longrightarrow> dim_row ?A = ?nr
carrier (module_vec ?ty ?n) = carrier_vec ?n

goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span (set (cols A))))
[PROOF STEP]
by force


[STATEMENT]
lemma lincomb_list_as_mat_mult:
  assumes "\<forall>w \<in> set ws. dim_vec w = n"
  shows "lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c" (is "?l ws c = ?r ws c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c
[PROOF STEP]
proof (insert assms, induct ws arbitrary: c)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c. \<forall>w\<in>set []. dim_vec w = n \<Longrightarrow> lincomb_list c [] = mat_of_cols n [] *\<^sub>v vec (length []) c
 2. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set []. dim_vec w = n

goal (2 subgoals):
 1. \<And>c. \<forall>w\<in>set []. dim_vec w = n \<Longrightarrow> lincomb_list c [] = mat_of_cols n [] *\<^sub>v vec (length []) c
 2. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set []. dim_vec w = n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set []. dim_vec w = n

goal (1 subgoal):
 1. lincomb_list c [] = mat_of_cols n [] *\<^sub>v vec (length []) c
[PROOF STEP]
by (auto simp: mult_mat_vec_def scalar_prod_def)
[PROOF STATE]
proof (state)
this:
lincomb_list c [] = mat_of_cols n [] *\<^sub>v vec (length []) c

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
case (Cons w ws)
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list ?c1 ws = mat_of_cols n ws *\<^sub>v vec (length ws) ?c1
\<forall>w\<in>set (w # ws). dim_vec w = n

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list ?c1 ws = mat_of_cols n ws *\<^sub>v vec (length ws) ?c1
\<forall>w\<in>set (w # ws). dim_vec w = n

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
assume i: "i < n"
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
have "?l (w#ws) c = c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list c (w # ws) = c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)
[PROOF STEP]
by (simp add: Cons o_def)
[PROOF STATE]
proof (state)
this:
lincomb_list c (w # ws) = c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb_list c (w # ws) = c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
have "\<dots> $ i = ?r (w#ws) c $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i
[PROOF STEP]
using Cons i index_smult_vec
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list ?c1 ws = mat_of_cols n ws *\<^sub>v vec (length ws) ?c1
\<forall>w\<in>set (w # ws). dim_vec w = n
i < n
?i < dim_vec ?v \<Longrightarrow> (?a \<cdot>\<^sub>v ?v) $ ?i = ?a * ?v $ ?i
dim_vec (?a \<cdot>\<^sub>v ?v) = dim_vec ?v

goal (1 subgoal):
 1. (c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i
[PROOF STEP]
by (simp add: mat_of_cols_Cons_index_0 mat_of_cols_Cons_index_Suc o_def vec_Suc mult_mat_vec_def row_def length_Cons)
[PROOF STATE]
proof (state)
this:
(c 0 \<cdot>\<^sub>v w + mat_of_cols n ws *\<^sub>v vec (length ws) (c \<circ> Suc)) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb_list c (w # ws) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i
[PROOF STEP]
have "?l (w#ws) c $ i = \<dots>"
[PROOF STATE]
proof (prove)
using this:
lincomb_list c (w # ws) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i

goal (1 subgoal):
 1. lincomb_list c (w # ws) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb_list c (w # ws) $ i = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ i

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i3 < n \<Longrightarrow> lincomb_list c (w # ws) $ ?i3 = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ ?i3

goal (1 subgoal):
 1. \<And>a ws c. \<lbrakk>\<And>c. \<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list c ws = mat_of_cols n ws *\<^sub>v vec (length ws) c; \<forall>w\<in>set (a # ws). dim_vec w = n\<rbrakk> \<Longrightarrow> lincomb_list c (a # ws) = mat_of_cols n (a # ws) *\<^sub>v vec (length (a # ws)) c
[PROOF STEP]
with Cons
[PROOF STATE]
proof (chain)
picking this:
\<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list ?c1 ws = mat_of_cols n ws *\<^sub>v vec (length ws) ?c1
\<forall>w\<in>set (w # ws). dim_vec w = n
?i3 < n \<Longrightarrow> lincomb_list c (w # ws) $ ?i3 = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ ?i3
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>w\<in>set ws. dim_vec w = n \<Longrightarrow> lincomb_list ?c1 ws = mat_of_cols n ws *\<^sub>v vec (length ws) ?c1
\<forall>w\<in>set (w # ws). dim_vec w = n
?i3 < n \<Longrightarrow> lincomb_list c (w # ws) $ ?i3 = (mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c) $ ?i3

goal (1 subgoal):
 1. lincomb_list c (w # ws) = mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c
[PROOF STEP]
by (intro eq_vecI, auto)
[PROOF STATE]
proof (state)
this:
lincomb_list c (w # ws) = mat_of_cols n (w # ws) *\<^sub>v vec (length (w # ws)) c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lincomb_vec_diff_add:
    assumes A: "A \<subseteq> carrier_vec n"
    and BA: "B \<subseteq> A" and fin_A: "finite A"
    and f: "f \<in> A \<rightarrow> UNIV" shows "lincomb f A = lincomb f (A-B) + lincomb f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
have "A - B \<union> B = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A - B \<union> B = A
[PROOF STEP]
using BA
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A

goal (1 subgoal):
 1. A - B \<union> B = A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A - B \<union> B = A

goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
hence "lincomb f A = lincomb f (A - B \<union> B)"
[PROOF STATE]
proof (prove)
using this:
A - B \<union> B = A

goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B \<union> B)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb f A = lincomb f (A - B \<union> B)

goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f A = lincomb f (A - B \<union> B)

goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
have "... = lincomb f (A-B) + lincomb f B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (A - B \<union> B) = lincomb f (A - B) + lincomb f B
[PROOF STEP]
by (rule lincomb_union, insert assms, auto intro: finite_subset)
[PROOF STATE]
proof (state)
this:
lincomb f (A - B \<union> B) = lincomb f (A - B) + lincomb f B

goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lincomb f A = lincomb f (A - B) + lincomb f B

goal (1 subgoal):
 1. lincomb f A = lincomb f (A - B) + lincomb f B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb f A = lincomb f (A - B) + lincomb f B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dim_sumlist:
  assumes "\<forall>x\<in>set xs. dim_vec x = n"
  shows "dim_vec (M.sumlist xs) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (M.sumlist xs) = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. dim_vec x = n

goal (1 subgoal):
 1. dim_vec (M.sumlist xs) = n
[PROOF STEP]
by (induct xs, auto)


[STATEMENT]
lemma sumlist_nth:
  assumes "\<forall>x\<in>set xs. dim_vec x = n" and "i<n"
  shows "(M.sumlist xs) $ i= sum (\<lambda>j. (xs ! j) $ i) {0..<length xs}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set xs. dim_vec x = n
i < n

goal (1 subgoal):
 1. M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i)
[PROOF STEP]
proof (induct xs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
case (snoc a xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i)
\<forall>x\<in>set (xs @ [a]). dim_vec x = n
i < n

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have [simp]: "x \<in> carrier_vec n" if x: "x\<in>set xs" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_vec n
[PROOF STEP]
using snoc.prems x
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (xs @ [a]). dim_vec x = n
i < n
x \<in> set xs

goal (1 subgoal):
 1. x \<in> carrier_vec n
[PROOF STEP]
unfolding carrier_vec_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (xs @ [a]). dim_vec x = n
i < n
x \<in> set xs

goal (1 subgoal):
 1. x \<in> {v. dim_vec v = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> set xs \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have [simp]: "a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> carrier_vec n
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (xs @ [a]). dim_vec x = n
i < n

goal (1 subgoal):
 1. a \<in> carrier_vec n
[PROOF STEP]
unfolding carrier_vec_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set (xs @ [a]). dim_vec x = n
i < n

goal (1 subgoal):
 1. a \<in> {v. dim_vec v = n}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> carrier_vec n

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have hyp: "M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i)
[PROOF STEP]
by (rule snoc.hyps, auto simp add: snoc.prems)
[PROOF STATE]
proof (state)
this:
M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have "M.sumlist (xs @ [a]) = M.sumlist xs + M.sumlist [a]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (xs @ [a]) = M.sumlist xs + M.sumlist [a]
[PROOF STEP]
by (rule M.sumlist_append, auto simp add: snoc.prems)
[PROOF STATE]
proof (state)
this:
M.sumlist (xs @ [a]) = M.sumlist xs + M.sumlist [a]

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (xs @ [a]) = M.sumlist xs + M.sumlist [a]

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have "... = M.sumlist xs + a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist xs + M.sumlist [a] = M.sumlist xs + a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist xs + M.sumlist [a] = M.sumlist xs + a

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist xs + M.sumlist [a] = M.sumlist xs + a

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have "... $ i = (M.sumlist xs $ i) + (a $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist xs + a) $ i = M.sumlist xs $ i + a $ i
[PROOF STEP]
by (rule index_add_vec(1), auto simp add: snoc.prems)
[PROOF STATE]
proof (state)
this:
(M.sumlist xs + a) $ i = M.sumlist xs $ i + a $ i

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(M.sumlist xs + a) $ i = M.sumlist xs $ i + a $ i

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have "... =  (\<Sum>j = 0..<length xs. xs ! j $ i) + (a $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist xs $ i + a $ i = (\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i
[PROOF STEP]
unfolding hyp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i = (\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M.sumlist xs $ i + a $ i = (\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist xs $ i + a $ i = (\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
have "... = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)
[PROOF STEP]
by (auto, rule sum.cong, auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
(\<Sum>j = 0..<length xs. xs ! j $ i) + a $ i = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
 2. \<And>x xs. \<lbrakk>\<lbrakk>\<forall>x\<in>set xs. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist xs $ i = (\<Sum>j = 0..<length xs. xs ! j $ i); \<forall>x\<in>set (xs @ [x]). dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist (xs @ [x]) $ i = (\<Sum>j = 0..<length (xs @ [x]). (xs @ [x]) ! j $ i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (xs @ [a]) $ i = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
M.sumlist (xs @ [a]) $ i = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)

goal (1 subgoal):
 1. M.sumlist (xs @ [a]) $ i = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
M.sumlist (xs @ [a]) $ i = (\<Sum>j = 0..<length (xs @ [a]). (xs @ [a]) ! j $ i)

goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set []. dim_vec x = n; i < n\<rbrakk> \<Longrightarrow> M.sumlist [] $ i = (\<Sum>j = 0..<length []. [] ! j $ i)
[PROOF STEP]
qed auto