[STATEMENT]
lemma lincomb_as_lincomb_list:
  fixes ws f
  assumes s: "set ws \<subseteq> carrier_vec n"
  shows "lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws!i = ws!j then 0 else f (ws ! i)) ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set ws \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws
[PROOF STEP]
proof (induct ws rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
case (snoc a ws)
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws
set (ws @ [a]) \<subseteq> carrier_vec n

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
let ?f = "\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0 else f (ws ! i)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
let ?g = "\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
let ?g2= "(\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0 else f (ws ! i)) \<cdot>\<^sub>v ws ! i)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
have [simp]: "\<And>v. v \<in> set ws \<Longrightarrow> v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. v \<in> set ws \<Longrightarrow> v \<in> carrier_vec n
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (ws @ [a]) \<subseteq> carrier_vec n

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

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?v1 \<in> set ws \<Longrightarrow> ?v1 \<in> carrier_vec n
[PROOF STEP]
have ws: "set ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
?v1 \<in> set ws \<Longrightarrow> ?v1 \<in> carrier_vec n

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

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
have hyp: "lincomb f (set ws) = lincomb_list ?f ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws
[PROOF STEP]
by (intro snoc.hyps ws)
[PROOF STATE]
proof (state)
this:
lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws

goal (2 subgoals):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
 2. \<And>x xs. \<lbrakk>set xs \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set xs) = lincomb_list (\<lambda>i. if \<exists>j<i. xs ! i = xs ! j then 0::'a else f (xs ! i)) xs; set (xs @ [x]) \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lincomb f (set (xs @ [x])) = lincomb_list (\<lambda>i. if \<exists>j<i. (xs @ [x]) ! i = (xs @ [x]) ! j then 0::'a else f ((xs @ [x]) ! i)) (xs @ [x])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
proof (cases "a\<in>set ws")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> set ws

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have g_length: "?g (length ws) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = 0\<^sub>v n
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
a \<in> set ws

goal (1 subgoal):
 1. (if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = 0\<^sub>v n
[PROOF STEP]
by (auto, metis in_set_conv_nth nth_append)
[PROOF STATE]
proof (state)
this:
(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = 0\<^sub>v n

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws]

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws]

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (map ?g [0..<length ws]) @ [0\<^sub>v n]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]
[PROOF STEP]
using g_length
[PROOF STATE]
proof (prove)
using this:
(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = 0\<^sub>v n

goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]
[PROOF STEP]
have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [0\<^sub>v n]"
[PROOF STATE]
proof (prove)
using this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]

goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n]

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws])
[PROOF STEP]
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws])

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws])

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... =  M.sumlist (map ?g [0..<length ws]) + 0\<^sub>v n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) + 0\<^sub>v n
[PROOF STEP]
by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) + 0\<^sub>v n

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) + 0\<^sub>v n

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = M.sumlist (map ?g [0..<length ws] @ [0\<^sub>v n])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) + 0\<^sub>v n = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])
[PROOF STEP]
by (rule M.sumlist_snoc[symmetric], auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) + 0\<^sub>v n = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])
[PROOF STEP]
have summlist_rw: "M.sumlist (map ?g2 [0..<length ws])
      = M.sumlist (map ?g [0..<length ws] @ [0\<^sub>v n])"
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "lincomb f (set (ws @ [a])) = lincomb f (set ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = lincomb f (set ws)
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
a \<in> set ws

goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = lincomb f (set ws)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
using this:
a \<in> set ws

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set (ws @ [a]). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)
[PROOF STEP]
by (simp add: insert_absorb)
[PROOF STATE]
proof (state)
this:
lincomb f (set (ws @ [a])) = lincomb f (set ws)

goal (2 subgoals):
 1. a \<in> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
 2. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (ws @ [a])) = lincomb f (set ws)

goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
unfolding hyp lincomb_list_def map_rw summlist_rw
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (ws @ [a])) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])

goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [0\<^sub>v n])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> set ws

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have g_length: "?g (length ws) = f a \<cdot>\<^sub>v a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = f a \<cdot>\<^sub>v a
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
a \<notin> set ws

goal (1 subgoal):
 1. (if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = f a \<cdot>\<^sub>v a
[PROOF STEP]
by (auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = f a \<cdot>\<^sub>v a

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws]

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws]

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (map ?g [0..<length ws]) @ [(f a \<cdot>\<^sub>v a)]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]
[PROOF STEP]
using g_length
[PROOF STATE]
proof (prove)
using this:
(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws = f a \<cdot>\<^sub>v a

goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [(if \<exists>j<length ws. (ws @ [a]) ! length ws = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! length ws)) \<cdot>\<^sub>v (ws @ [a]) ! length ws] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]
[PROOF STEP]
have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [(f a \<cdot>\<^sub>v a)]"
[PROOF STATE]
proof (prove)
using this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]

goal (1 subgoal):
 1. map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length (ws @ [a])] = map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws] @ [f a \<cdot>\<^sub>v a]

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have summlist_rw: "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws])
[PROOF STEP]
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. (if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) \<cdot>\<^sub>v ws ! i) [0..<length ws]) = M.sumlist (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws])

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f (set (a # ws)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (\<Oplus>\<^bsub>V\<^esub>v\<in> insert a (set ws). f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set (a # ws). f v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (f a \<cdot>\<^sub>v a) + (\<Oplus>\<^bsub>V\<^esub>v\<in> (set ws). f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)
[PROOF STEP]
proof (rule finsum_insert)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. finite (set ws)
 2. a \<notin> set ws
 3. (\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set ws \<rightarrow> carrier_vec n
 4. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
show "finite (set ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set ws)

goal (3 subgoals):
 1. a \<notin> set ws
 2. (\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set ws \<rightarrow> carrier_vec n
 3. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
show "a \<notin> set ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<notin> set ws
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
a \<notin> set ws

goal (1 subgoal):
 1. a \<notin> set ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<notin> set ws

goal (2 subgoals):
 1. (\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set ws \<rightarrow> carrier_vec n
 2. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
show "(\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set ws \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>v. f v \<cdot>\<^sub>v v) \<in> set ws \<rightarrow> carrier_vec n
[PROOF STEP]
using snoc.prems(1)
[PROOF STATE]
proof (prove)
using this:
set (ws @ [a]) \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
show "f a \<cdot>\<^sub>v a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (ws @ [a]) \<subseteq> carrier_vec n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>insert a (set ws). f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (f a \<cdot>\<^sub>v a) + lincomb f (set ws)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb f (set ws)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb f (set ws)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + (\<Oplus>\<^bsub>V\<^esub>v\<in>set ws. f v \<cdot>\<^sub>v v) = f a \<cdot>\<^sub>v a + lincomb f (set ws)

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = (f a \<cdot>\<^sub>v a) + lincomb_list ?f ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + lincomb f (set ws) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws
[PROOF STEP]
using hyp
[PROOF STATE]
proof (prove)
using this:
lincomb f (set ws) = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + lincomb f (set ws) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + lincomb f (set ws) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + lincomb f (set ws) = f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... =  lincomb_list ?f ws  + (f a \<cdot>\<^sub>v a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws + f a \<cdot>\<^sub>v a
[PROOF STEP]
using M.add.m_comm lincomb_list_carrier snoc.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier_vec n; ?y \<in> carrier_vec n\<rbrakk> \<Longrightarrow> ?x + ?y = ?y + ?x
set ?vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list ?c ?vs \<in> carrier_vec n
set (ws @ [a]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws + f a \<cdot>\<^sub>v a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws + f a \<cdot>\<^sub>v a

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f a \<cdot>\<^sub>v a + lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws = lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws + f a \<cdot>\<^sub>v a

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
have "... = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i
      = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) (ws @ [a])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws + f a \<cdot>\<^sub>v a = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
proof (unfold lincomb_list_def map_rw summlist_rw, rule M.sumlist_snoc[symmetric])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) \<subseteq> carrier_vec n
 2. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
show "set (map ?g [0..<length ws]) \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) \<subseteq> carrier_vec n
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (ws @ [a]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. set (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) \<subseteq> carrier_vec n
[PROOF STEP]
by (auto simp add: nth_append)
[PROOF STATE]
proof (state)
this:
set (map (\<lambda>i. (if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) \<cdot>\<^sub>v (ws @ [a]) ! i) [0..<length ws]) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
show "f a \<cdot>\<^sub>v a \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f a \<cdot>\<^sub>v a \<in> carrier_vec n
[PROOF STEP]
using snoc.prems
[PROOF STATE]
proof (prove)
using this:
set (ws @ [a]) \<subseteq> carrier_vec n

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lincomb_list (\<lambda>i. if \<exists>j<i. ws ! i = ws ! j then 0::'a else f (ws ! i)) ws + f a \<cdot>\<^sub>v a = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])

goal (1 subgoal):
 1. a \<notin> set ws \<Longrightarrow> lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])

goal (1 subgoal):
 1. lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lincomb f (set (ws @ [a])) = lincomb_list (\<lambda>i. if \<exists>j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0::'a else f ((ws @ [a]) ! i)) (ws @ [a])

goal (1 subgoal):
 1. set [] \<subseteq> carrier_vec n \<Longrightarrow> lincomb f (set []) = lincomb_list (\<lambda>i. if \<exists>j<i. [] ! i = [] ! j then 0::'a else f ([] ! i)) []
[PROOF STEP]
qed auto


[STATEMENT]
lemma span_list_as_span:
  assumes "set vs \<subseteq> carrier_vec n"
  shows "span_list vs = span (set vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. span_list vs = local.span (set vs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. span_list vs = local.span (set vs)
[PROOF STEP]
proof (auto simp: span_list_def span_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c. set vs \<subseteq> carrier_vec n \<Longrightarrow> \<exists>a A. lincomb_list c vs = lincomb a A \<and> finite A \<and> A \<subseteq> set vs
 2. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>c. set vs \<subseteq> carrier_vec n \<Longrightarrow> \<exists>a A. lincomb_list c vs = lincomb a A \<and> finite A \<and> A \<subseteq> set vs
 2. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
show "\<exists>a A. lincomb_list f vs = lincomb a A \<and> finite A \<and> A \<subseteq> set vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a A. lincomb_list f vs = lincomb a A \<and> finite A \<and> A \<subseteq> set vs
[PROOF STEP]
using assms lincomb_list_as_lincomb
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n
set ?vs \<subseteq> carrier_vec n \<Longrightarrow> lincomb_list ?c ?vs = lincomb (mk_coeff ?vs ?c) (set ?vs)

goal (1 subgoal):
 1. \<exists>a A. lincomb_list f vs = lincomb a A \<and> finite A \<and> A \<subseteq> set vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>a A. lincomb_list f vs = lincomb a A \<and> finite A \<and> A \<subseteq> set vs

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
fix f::"'a vec \<Rightarrow>'a" and A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
assume fA: "finite A" and A: "A \<subseteq> set vs"
[PROOF STATE]
proof (state)
this:
finite A
A \<subseteq> set vs

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have [simp]: "x \<in> carrier_vec n" if x: "x \<in> A" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_vec n
[PROOF STEP]
using A x assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set vs
x \<in> A
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. x \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?x1 \<in> A \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have [simp]:  "v \<in> carrier_vec n" if v: "v \<in> set vs" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
using assms v
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n
v \<in> set vs

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

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have set_vs_Un: "((set vs) - A) \<union> A = set vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set vs - A \<union> A = set vs
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> set vs

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

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
let ?f = "(\<lambda>x. if x\<in>(set vs) - A then 0 else f x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have f0: "(\<Oplus>\<^bsub>V\<^esub>v\<in>(set vs) - A. ?f v \<cdot>\<^sub>v v) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = 0\<^sub>v n
[PROOF STEP]
by (rule M.finsum_all0, auto)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = 0\<^sub>v n

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have "lincomb f A = lincomb ?f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) A
[PROOF STEP]
by (auto simp add: lincomb_def intro!: finsum_cong2)
[PROOF STATE]
proof (state)
this:
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) A

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) A

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have "... = (\<Oplus>\<^bsub>V\<^esub>v\<in>(set vs) - A. ?f v \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. ?f v \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) A = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding f0 lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = 0\<^sub>v n + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) A = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) A = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have "... = lincomb ?f (((set vs) - A) \<union> A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs - A \<union> A)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A \<union> A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (rule M.finsum_Un_disjoint[symmetric], auto simp add: fA)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs - A \<union> A)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs - A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) + (\<Oplus>\<^bsub>V\<^esub>v\<in>A. (if v \<in> set vs - A then 0::'a else f v) \<cdot>\<^sub>v v) = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs - A \<union> A)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
have "... = lincomb ?f (set vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs - A \<union> A) = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)
[PROOF STEP]
using set_vs_Un
[PROOF STATE]
proof (prove)
using this:
set vs - A \<union> A = set vs

goal (1 subgoal):
 1. lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs - A \<union> A) = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs - A \<union> A) = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)
[PROOF STEP]
have "lincomb f A = lincomb ?f (set vs)"
[PROOF STATE]
proof (prove)
using this:
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)

goal (1 subgoal):
 1. lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)

goal (1 subgoal):
 1. \<And>a A. \<lbrakk>set vs \<subseteq> carrier_vec n; finite A; A \<subseteq> set vs\<rbrakk> \<Longrightarrow> \<exists>c. lincomb a A = lincomb_list c vs
[PROOF STEP]
with lincomb_as_lincomb_list[OF assms]
[PROOF STATE]
proof (chain)
picking this:
lincomb ?f (set vs) = lincomb_list (\<lambda>i. if \<exists>j<i. vs ! i = vs ! j then 0::'a else ?f (vs ! i)) vs
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)
[PROOF STEP]
show "\<exists>c. lincomb f A = lincomb_list c vs"
[PROOF STATE]
proof (prove)
using this:
lincomb ?f (set vs) = lincomb_list (\<lambda>i. if \<exists>j<i. vs ! i = vs ! j then 0::'a else ?f (vs ! i)) vs
lincomb f A = lincomb (\<lambda>x. if x \<in> set vs - A then 0::'a else f x) (set vs)

goal (1 subgoal):
 1. \<exists>c. lincomb f A = lincomb_list c vs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>c. lincomb f A = lincomb_list c vs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_spanI[intro]:
  assumes "v = lincomb a A" "finite A" "A \<subseteq> W"
  shows "v \<in> span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> local.span W
[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> W}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v = lincomb a A
finite A
A \<subseteq> W

goal (1 subgoal):
 1. v \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> W}
[PROOF STEP]
by auto


[STATEMENT]
lemma in_spanE:
  assumes "v \<in> span W"
  shows "\<exists> a A. v = lincomb a A \<and> finite A \<and> A \<subseteq> W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a A. v = lincomb a A \<and> finite A \<and> A \<subseteq> W
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> local.span W

goal (1 subgoal):
 1. \<exists>a A. v = lincomb a A \<and> finite A \<and> A \<subseteq> W
[PROOF STEP]
unfolding span_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {lincomb a A |a A. finite A \<and> A \<subseteq> W}

goal (1 subgoal):
 1. \<exists>a A. v = lincomb a A \<and> finite A \<and> A \<subseteq> W
[PROOF STEP]
by auto


[STATEMENT]
lemma smult_in_span:
  assumes "W \<subseteq> carrier_vec n" and insp: "x \<in> span W"
  shows "c \<cdot>\<^sub>v x \<in> span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
from in_spanE[OF insp]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a A. x = lincomb a A \<and> finite A \<and> A \<subseteq> W
[PROOF STEP]
obtain a A where a: "x = lincomb a A" "finite A" "A \<subseteq> W"
[PROOF STATE]
proof (prove)
using this:
\<exists>a A. x = lincomb a A \<and> finite A \<and> A \<subseteq> W

goal (1 subgoal):
 1. (\<And>a A. \<lbrakk>x = lincomb a A; finite A; A \<subseteq> W\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = lincomb a A
finite A
A \<subseteq> W

goal (1 subgoal):
 1. c \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
have "c \<cdot>\<^sub>v x = lincomb (\<lambda> x. c * a x) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<cdot>\<^sub>v x = lincomb (\<lambda>x. c * a x) A
[PROOF STEP]
using a(1)
[PROOF STATE]
proof (prove)
using this:
x = lincomb a A

goal (1 subgoal):
 1. c \<cdot>\<^sub>v x = lincomb (\<lambda>x. c * a x) A
[PROOF STEP]
unfolding lincomb_def a
[PROOF STATE]
proof (prove)
using this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. c \<cdot>\<^sub>v (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. c * a v \<cdot>\<^sub>v v)
[PROOF STEP]
apply(subst finsum_smult)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<Longrightarrow> True
 2. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<Longrightarrow> (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n
 3. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>x\<in>A. c \<cdot>\<^sub>v (a x \<cdot>\<^sub>v x)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. c * a v \<cdot>\<^sub>v v)
[PROOF STEP]
using assms a
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
x \<in> local.span W
x = lincomb a A
finite A
A \<subseteq> W

goal (3 subgoals):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<Longrightarrow> True
 2. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<Longrightarrow> (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n
 3. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>x\<in>A. c \<cdot>\<^sub>v (a x \<cdot>\<^sub>v x)) = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. c * a v \<cdot>\<^sub>v v)
[PROOF STEP]
by (auto simp:smult_smult_assoc)
[PROOF STATE]
proof (state)
this:
c \<cdot>\<^sub>v x = lincomb (\<lambda>x. c * a x) A

goal (1 subgoal):
 1. c \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
thus "c \<cdot>\<^sub>v x \<in> span W"
[PROOF STATE]
proof (prove)
using this:
c \<cdot>\<^sub>v x = lincomb (\<lambda>x. c * a x) A

goal (1 subgoal):
 1. c \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
using a(2,3)
[PROOF STATE]
proof (prove)
using this:
c \<cdot>\<^sub>v x = lincomb (\<lambda>x. c * a x) A
finite A
A \<subseteq> W

goal (1 subgoal):
 1. c \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<cdot>\<^sub>v x \<in> local.span W

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma span_subsetI: assumes ws: "ws \<subseteq> carrier_vec n"
  "us \<subseteq> span ws"
shows "span us \<subseteq> span ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span us \<subseteq> local.span ws
[PROOF STEP]
by (simp add: assms(1) span_is_submodule span_is_subset subsetI ws)


[STATEMENT]
lemma sumlist_in_span: assumes W: "W \<subseteq> carrier_vec n"
  shows "(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> span W) \<Longrightarrow> sumlist xs \<in> span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W
[PROOF STEP]
proof (induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist [] \<in> local.span W
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?x1 \<in> set [] \<Longrightarrow> ?x1 \<in> local.span W

goal (2 subgoals):
 1. (\<And>x. x \<in> set [] \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist [] \<in> local.span W
 2. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> set [] \<Longrightarrow> ?x1 \<in> local.span W

goal (1 subgoal):
 1. M.sumlist [] \<in> local.span W
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
?x1 \<in> set [] \<Longrightarrow> ?x1 \<in> local.span W
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. M.sumlist [] \<in> local.span W
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
M.sumlist [] \<in> local.span W

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W
?x1 \<in> set (x # xs) \<Longrightarrow> ?x1 \<in> local.span W

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
from span_is_subset2[OF W] Cons(2)
[PROOF STATE]
proof (chain)
picking this:
local.span W \<subseteq> carrier_vec n
?x1 \<in> set (x # xs) \<Longrightarrow> ?x1 \<in> local.span W
[PROOF STEP]
have xs: "x \<in> carrier_vec n" "set xs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
local.span W \<subseteq> carrier_vec n
?x1 \<in> set (x # xs) \<Longrightarrow> ?x1 \<in> local.span W

goal (1 subgoal):
 1. x \<in> carrier_vec n &&& set xs \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec n
set xs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
from span_add1[OF W Cons(2)[of x] Cons(1)[OF Cons(2)]]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>x \<in> set (x # xs); \<And>xa. xa \<in> set xs \<Longrightarrow> xa \<in> set (x # xs)\<rbrakk> \<Longrightarrow> x + M.sumlist xs \<in> local.span W
[PROOF STEP]
have "x + sumlist xs \<in> span W"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> set (x # xs); \<And>xa. xa \<in> set xs \<Longrightarrow> xa \<in> set (x # xs)\<rbrakk> \<Longrightarrow> x + M.sumlist xs \<in> local.span W

goal (1 subgoal):
 1. x + M.sumlist xs \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x + M.sumlist xs \<in> local.span W

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x + M.sumlist xs \<in> local.span W

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
have "x + sumlist xs = sumlist ([x] @ xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + M.sumlist xs = M.sumlist ([x] @ xs)
[PROOF STEP]
by (subst sumlist_append, insert xs, auto)
[PROOF STATE]
proof (state)
this:
x + M.sumlist xs = M.sumlist ([x] @ xs)

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. x \<in> set xs \<Longrightarrow> x \<in> local.span W) \<Longrightarrow> M.sumlist xs \<in> local.span W; \<And>x. x \<in> set (a # xs) \<Longrightarrow> x \<in> local.span W\<rbrakk> \<Longrightarrow> M.sumlist (a # xs) \<in> local.span W
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist ([x] @ xs) \<in> local.span W
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
M.sumlist ([x] @ xs) \<in> local.span W

goal (1 subgoal):
 1. M.sumlist (x # xs) \<in> local.span W
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M.sumlist (x # xs) \<in> local.span W

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma span_span[simp]:
  assumes "W \<subseteq> carrier_vec n"
  shows "span (span W) = span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (local.span W) = local.span W
[PROOF STEP]
proof(standard,standard,goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> local.span (local.span W) \<Longrightarrow> x \<in> local.span W
 2. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
case (1 x)
[PROOF STATE]
proof (state)
this:
x \<in> local.span (local.span W)

goal (2 subgoals):
 1. \<And>x. x \<in> local.span (local.span W) \<Longrightarrow> x \<in> local.span W
 2. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
with in_spanE
[PROOF STATE]
proof (chain)
picking this:
?v \<in> local.span ?W \<Longrightarrow> \<exists>a A. ?v = lincomb a A \<and> finite A \<and> A \<subseteq> ?W
x \<in> local.span (local.span W)
[PROOF STEP]
obtain a A where a: "x = lincomb a A" "finite A" "A \<subseteq> span W"
[PROOF STATE]
proof (prove)
using this:
?v \<in> local.span ?W \<Longrightarrow> \<exists>a A. ?v = lincomb a A \<and> finite A \<and> A \<subseteq> ?W
x \<in> local.span (local.span W)

goal (1 subgoal):
 1. (\<And>a A. \<lbrakk>x = lincomb a A; finite A; A \<subseteq> local.span W\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
x = lincomb a A
finite A
A \<subseteq> local.span W

goal (2 subgoals):
 1. \<And>x. x \<in> local.span (local.span W) \<Longrightarrow> x \<in> local.span W
 2. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
from a(3) assms
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq> local.span W
W \<subseteq> carrier_vec n
[PROOF STEP]
have AC:"A \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> local.span W
W \<subseteq> carrier_vec n

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

goal (2 subgoals):
 1. \<And>x. x \<in> local.span (local.span W) \<Longrightarrow> x \<in> local.span W
 2. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> local.span W
[PROOF STEP]
unfolding a(1)[unfolded lincomb_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>A. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
proof(insert a(3),atomize (full),rule finite_induct[OF a(2)],goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>{}. a v \<cdot>\<^sub>v v) \<in> local.span W
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. {} \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>{}. a v \<cdot>\<^sub>v v) \<in> local.span W
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>{}. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
using span_zero
[PROOF STATE]
proof (prove)
using this:
0\<^sub>v n \<in> local.span ?U

goal (1 subgoal):
 1. {} \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>{}. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{} \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>{}. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
case (2 x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
assume F:"insert x F \<subseteq> span W"
[PROOF STATE]
proof (state)
this:
insert x F \<subseteq> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
hence "a x \<cdot>\<^sub>v x \<in> span W"
[PROOF STATE]
proof (prove)
using this:
insert x F \<subseteq> local.span W

goal (1 subgoal):
 1. a x \<cdot>\<^sub>v x \<in> local.span W
[PROOF STEP]
by (intro smult_in_span[OF assms],auto)
[PROOF STATE]
proof (state)
this:
a x \<cdot>\<^sub>v x \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
hence "a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> span W"
[PROOF STATE]
proof (prove)
using this:
a x \<cdot>\<^sub>v x \<in> local.span W

goal (1 subgoal):
 1. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
using span_add1 F 2 assms
[PROOF STATE]
proof (prove)
using this:
a x \<cdot>\<^sub>v x \<in> local.span W
\<lbrakk>?U \<subseteq> carrier_vec n; ?v \<in> local.span ?U; ?w \<in> local.span ?U\<rbrakk> \<Longrightarrow> ?v + ?w \<in> local.span ?U
insert x F \<subseteq> local.span W
finite F
x \<notin> F
F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
hence "(\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> span W"
[PROOF STATE]
proof (prove)
using this:
a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
apply(subst M.finsum_insert[OF 2(1,2)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W \<Longrightarrow> (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> F \<rightarrow> carrier_vec n
 2. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W \<Longrightarrow> a x \<cdot>\<^sub>v x \<in> carrier_vec n
 3. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W \<Longrightarrow> a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
using F assms
[PROOF STATE]
proof (prove)
using this:
insert x F \<subseteq> local.span W
W \<subseteq> carrier_vec n

goal (3 subgoals):
 1. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W \<Longrightarrow> (\<lambda>v. a v \<cdot>\<^sub>v v) \<in> F \<rightarrow> carrier_vec n
 2. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W \<Longrightarrow> a x \<cdot>\<^sub>v x \<in> carrier_vec n
 3. a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W \<Longrightarrow> a x \<cdot>\<^sub>v x + (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
insert x F \<subseteq> local.span W \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>F. a v \<cdot>\<^sub>v v) \<in> local.span W\<rbrakk> \<Longrightarrow> insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
insert x F \<subseteq> local.span W \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
insert x F \<subseteq> local.span W \<Longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal (1 subgoal):
 1. insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x F \<subseteq> local.span W \<longrightarrow> (\<Oplus>\<^bsub>V\<^esub>v\<in>insert x F. a v \<cdot>\<^sub>v v) \<in> local.span W

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<in> local.span W

goal (1 subgoal):
 1. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. local.span W \<subseteq> local.span (local.span W)
[PROOF STEP]
by(intro in_own_span, auto)
[PROOF STATE]
proof (state)
this:
local.span W \<subseteq> local.span (local.span W)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_triangular_imp_basis:
  assumes A: "A \<in> carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0 \<notin> set (diag_mat A)"
  shows "basis (set (rows A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis (set (rows A))
[PROOF STEP]
using upper_triangular_imp_distinct[OF assms]
[PROOF STATE]
proof (prove)
using this:
distinct (rows A)

goal (1 subgoal):
 1. basis (set (rows A))
[PROOF STEP]
using upper_triangular_imp_lin_indpt_rows[OF assms] A
[PROOF STATE]
proof (prove)
using this:
distinct (rows A)
lin_indpt (set (rows A))
A \<in> carrier_mat n n

goal (1 subgoal):
 1. basis (set (rows A))
[PROOF STEP]
by (auto intro: dim_li_is_basis simp: distinct_card dim_is_n set_rows_carrier)


[STATEMENT]
lemma fin_dim_span_rows:
assumes A: "A \<in> carrier_mat nr n"
shows "vectorspace.fin_dim class_ring (vs (span (set (rows A))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vectorspace.fin_dim class_ring (vs (local.span (set (rows A))))
[PROOF STEP]
proof (rule fin_dim_span)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite (set (rows A))
 2. set (rows A) \<subseteq> carrier V
[PROOF STEP]
show "set (rows A) \<subseteq> carrier V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (rows A) \<subseteq> carrier V
[PROOF STEP]
using A rows_carrier[of A]
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr n
set (rows A) \<subseteq> carrier_vec (dim_col A)

goal (1 subgoal):
 1. set (rows A) \<subseteq> carrier V
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
using this:
A \<in> {m. dim_row m = nr \<and> dim_col m = n}
set (rows A) \<subseteq> carrier_vec (dim_col A)

goal (1 subgoal):
 1. set (rows A) \<subseteq> carrier V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (rows A) \<subseteq> carrier V

goal (1 subgoal):
 1. finite (set (rows A))
[PROOF STEP]
show "finite (set (rows A))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (rows A))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set (rows A))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma row_space_eq_col_space_transpose:
  shows "row_space A = col_space A\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row_space A = col_space A\<^sup>T
[PROOF STEP]
unfolding col_space_def row_space_def cols_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set (rows A)) = local.span (set (rows A))
[PROOF STEP]
..


[STATEMENT]
lemma col_space_eq_row_space_transpose:
  shows "col_space A = row_space A\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. col_space A = row_space A\<^sup>T
[PROOF STEP]
unfolding col_space_def row_space_def Matrix.rows_transpose
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set (cols A)) = local.span (set (cols A))
[PROOF STEP]
..