[STATEMENT]
lemma A_del_min: assumes "is_root h"
shows "T_del_min h + \<Phi>(del_min h) - \<Phi> h \<le> 2 * log 2 (size h + 1) + 5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
proof (cases h)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
case [simp]: (Node hs1 x hs)
[PROOF STATE]
proof (state)
this:
h = \<langle>hs1, x, hs\<rangle>

goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
have "T_pass\<^sub>2 (pass\<^sub>1 hs1) + real(T_pass\<^sub>1 hs1) \<le> real(len hs1) + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_pass\<^sub>2 (pass\<^sub>1 hs1)) + real (T_pass\<^sub>1 hs1) \<le> real (len hs1) + 2
[PROOF STEP]
by (induct hs1 rule: pass\<^sub>1.induct) simp_all
[PROOF STATE]
proof (state)
this:
real (T_pass\<^sub>2 (pass\<^sub>1 hs1)) + real (T_pass\<^sub>1 hs1) \<le> real (len hs1) + 2

goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
real (T_pass\<^sub>2 (pass\<^sub>1 hs1)) + real (T_pass\<^sub>1 hs1) \<le> real (len hs1) + 2

goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
have "\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (size h + 1) - len hs1 + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
have "\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (size hs1 + 1) - len hs1 + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2
[PROOF STEP]
using  \<Delta>\<Phi>_del_min[of "hs1" "x"] assms
[PROOF STATE]
proof (prove)
using this:
\<Phi> (del_min \<langle>hs1, x, \<langle>\<rangle>\<rangle>) - \<Phi> \<langle>hs1, x, \<langle>\<rangle>\<rangle> \<le> 2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2
is_root h

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
have "\<dots> \<le> 2 * log 2 (size h + 1) - len hs1 + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2 \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
2 * log 2 (real (size hs1 + 1)) - real (len hs1) + 2 \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2

goal (1 subgoal):
 1. \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2

goal (2 subgoals):
 1. h = \<langle>\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
 2. \<And>x21 x22 x23. h = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
real (T_pass\<^sub>2 (pass\<^sub>1 hs1)) + real (T_pass\<^sub>1 hs1) \<le> real (len hs1) + 2
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (T_pass\<^sub>2 (pass\<^sub>1 hs1)) + real (T_pass\<^sub>1 hs1) \<le> real (len hs1) + 2
\<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) - real (len hs1) + 2

goal (1 subgoal):
 1. real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
by(simp)
[PROOF STATE]
proof (state)
this:
real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5

goal (1 subgoal):
 1. h = \<langle>\<rangle> \<Longrightarrow> real (T_del_min h) + \<Phi> (del_min h) - \<Phi> h \<le> 2 * log 2 (real (size h + 1)) + 5
[PROOF STEP]
qed simp


[STATEMENT]
lemma A_insert: "is_root h \<Longrightarrow> T_insert a h + \<Phi>(insert a h) - \<Phi> h \<le> log 2 (size h + 1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_root h \<Longrightarrow> real (T_insert a h) + \<Phi> (Pairing_Heap_Tree.insert a h) - \<Phi> h \<le> log 2 (real (size h + 1)) + 1
[PROOF STEP]
by(drule \<Delta>\<Phi>_insert) simp


[STATEMENT]
lemma A_merge: assumes "is_root h1" "is_root h2"
shows "T_merge h1 h2 + \<Phi>(merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (size h1 + size h2 + 1) + 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
proof (cases h1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. h1 = \<langle>\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
 2. \<And>x21 x22 x23. h1 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
h1 = \<langle>\<rangle>

goal (2 subgoals):
 1. h1 = \<langle>\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
 2. \<And>x21 x22 x23. h1 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
h1 = \<langle>\<rangle>

goal (1 subgoal):
 1. real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
by (cases h2) auto
[PROOF STATE]
proof (state)
this:
real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2

goal (1 subgoal):
 1. \<And>x21 x22 x23. h1 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. h1 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
case h1: Node
[PROOF STATE]
proof (state)
this:
h1 = \<langle>x21_, x22_, x23_\<rangle>

goal (1 subgoal):
 1. \<And>x21 x22 x23. h1 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
proof (cases h2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. h2 = \<langle>\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
 2. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
h2 = \<langle>\<rangle>

goal (2 subgoals):
 1. h2 = \<langle>\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
 2. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
h2 = \<langle>\<rangle>

goal (1 subgoal):
 1. real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
using h1
[PROOF STATE]
proof (prove)
using this:
h2 = \<langle>\<rangle>
h1 = \<langle>x21_, x22_, x23_\<rangle>

goal (1 subgoal):
 1. real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2

goal (1 subgoal):
 1. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
case h2: Node
[PROOF STATE]
proof (state)
this:
h2 = \<langle>x21_, x22_, x23_\<rangle>

goal (1 subgoal):
 1. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
have "\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1
[PROOF STEP]
apply(rule \<Delta>\<Phi>_merge)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. h1 = \<langle>?hs1.0, ?x1.0, \<langle>\<rangle>\<rangle>
 2. h2 = \<langle>?hs2.0, ?x2.0, \<langle>\<rangle>\<rangle>
[PROOF STEP]
using h1 h2 assms
[PROOF STATE]
proof (prove)
using this:
h1 = \<langle>x21___, x22___, x23___\<rangle>
h2 = \<langle>x21_, x22_, x23_\<rangle>
is_root h1
is_root h2

goal (2 subgoals):
 1. h1 = \<langle>?hs1.0, ?x1.0, \<langle>\<rangle>\<rangle>
 2. h2 = \<langle>?hs2.0, ?x2.0, \<langle>\<rangle>\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1

goal (1 subgoal):
 1. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2)) + 1

goal (1 subgoal):
 1. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
have "\<dots> \<le> log 2 (size h1 + size h2 + 1) + 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. log 2 (real (size h1 + size h2)) + 1 \<le> log 2 (real (size h1 + size h2 + 1)) + 1
[PROOF STEP]
by (simp add: h1)
[PROOF STATE]
proof (state)
this:
log 2 (real (size h1 + size h2)) + 1 \<le> log 2 (real (size h1 + size h2 + 1)) + 1

goal (1 subgoal):
 1. \<And>x21 x22 x23. h2 = \<langle>x21, x22, x23\<rangle> \<Longrightarrow> real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 1

goal (1 subgoal):
 1. real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2
[PROOF STEP]
by(simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real (T_merge h1 h2) + \<Phi> (merge h1 h2) - \<Phi> h1 - \<Phi> h2 \<le> log 2 (real (size h1 + size h2 + 1)) + 2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_index_not_in_set: "x \<notin> set xs \<longleftrightarrow> find_index xs x = length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<notin> set xs) = (find_index xs x = length xs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma find_index_in_set: "x \<in> set xs \<Longrightarrow> xs ! (find_index xs x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs \<Longrightarrow> xs ! find_index xs x = x
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma find_index_inj: "inj_on (find_index xs) (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (find_index xs) (set xs)
[PROOF STEP]
by (induction xs) (auto simp add: inj_on_def)


[STATEMENT]
lemma find_index_leq_length: "find_index xs x < length xs \<longleftrightarrow> x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (find_index xs x < length xs) = (x \<in> set xs)
[PROOF STEP]
by (induction xs) (auto)


[STATEMENT]
lemma rev_unsimp: "rev xs @ (r # rs) = rev (r#xs) @ rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev xs @ r # rs = rev (r # xs) @ rs
[PROOF STEP]
by(induct xs,auto)


[STATEMENT]
lemma corthogonal_is_orthogonal[simp]:
  "corthogonal (xs :: 'a :: trivial_conjugatable_ordered_field vec list) = orthogonal xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. corthogonal xs = orthogonal xs
[PROOF STEP]
unfolding corthogonal_def orthogonal_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<length xs. \<forall>j<length xs. (xs ! i \<bullet>c xs ! j = (0::'a)) = (i \<noteq> j)) = (\<forall>i j. i < length xs \<longrightarrow> j < length xs \<longrightarrow> (xs ! i \<bullet> xs ! j = (0::'a)) = (i \<noteq> j))
[PROOF STEP]
by simp


[STATEMENT]
lemma lattice_of_finsum:
  assumes "set fs \<subseteq> carrier_vec n"
  shows "lattice_of fs = range (\<lambda> c. finsum V (\<lambda> i. of_int (c i) \<cdot>\<^sub>v fs ! i) {0 ..< length fs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of fs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of fs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
have "sumlist (map (\<lambda> i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0 ..< length fs])
        = finsum V (\<lambda> i. of_int (c i) \<cdot>\<^sub>v fs ! i) {0 ..< length fs}" for c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
using  assms
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
by (subst sumlist_map_as_finsum) (fastforce)+
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (?c1 i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (?c1 i) \<cdot>\<^sub>v fs ! i)

goal (1 subgoal):
 1. lattice_of fs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (map (\<lambda>i. of_int (?c1 i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (?c1 i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. of_int (?c1 i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (?c1 i) \<cdot>\<^sub>v fs ! i)

goal (1 subgoal):
 1. lattice_of fs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
unfolding lattice_of_def
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. of_int (?c1 i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (?c1 i) \<cdot>\<^sub>v fs ! i)

goal (1 subgoal):
 1. range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs])) = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lattice_of fs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>i\<in>{0..<length fs}. of_int (c i) \<cdot>\<^sub>v fs ! i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma in_latticeE: assumes "f \<in> lattice_of fs" obtains c where
    "f = sumlist (map (\<lambda> i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0 ..< length fs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> lattice_of fs

goal (1 subgoal):
 1. (\<And>c. f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lattice_of_def
[PROOF STATE]
proof (prove)
using this:
f \<in> range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]))

goal (1 subgoal):
 1. (\<And>c. f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma in_latticeI: assumes "f = sumlist (map (\<lambda> i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0 ..< length fs])"
  shows "f \<in> lattice_of fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs])

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
unfolding lattice_of_def
[PROOF STATE]
proof (prove)
using this:
f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs])

goal (1 subgoal):
 1. f \<in> range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs]))
[PROOF STEP]
by auto


[STATEMENT]
lemma finsum_over_indexes_to_vectors:
  assumes "set vs \<subseteq> carrier_vec n" "l = length vs"
  shows "\<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n
l = length vs

goal (1 subgoal):
 1. \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
proof (induction l arbitrary: vs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
case (Suc l)
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
[PROOF STEP]
obtain vs' v where vs'_def: "vs = vs' @ [v]"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs

goal (1 subgoal):
 1. (\<And>vs' v. vs = vs' @ [v] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Zero_not_Suc length_0_conv rev_exhaust)
[PROOF STATE]
proof (state)
this:
vs = vs' @ [v]

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have c: "\<exists>c. (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<l}. of_int (g i) \<cdot>\<^sub>v vs' ! i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<l}. of_int (g i) \<cdot>\<^sub>v vs' ! i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. \<exists>c. (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<l}. of_int (g i) \<cdot>\<^sub>v vs' ! i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
\<exists>c. (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<l}. of_int (g i) \<cdot>\<^sub>v vs' ! i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<l}. of_int (g i) \<cdot>\<^sub>v vs' ! i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
obtain c
    where c_def: "(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. (\<Oplus>\<^bsub>V\<^esub>i\<in>{0..<l}. of_int (g i) \<cdot>\<^sub>v vs' ! i) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. (\<And>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x)
        = of_int (g l) \<cdot>\<^sub>v vs ! l + (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = of_int (g l) \<cdot>\<^sub>v vs ! l + (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = of_int (g l) \<cdot>\<^sub>v vs ! l + (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x)
[PROOF STEP]
by (subst finsum_insert[symmetric]) (fastforce intro!: finsum_cong')+
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = of_int (g l) \<cdot>\<^sub>v vs ! l + (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = of_int (g l) \<cdot>\<^sub>v vs ! l + (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "vs = vs' @ [v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vs = vs' @ [v]
[PROOF STEP]
using vs'_def
[PROOF STATE]
proof (prove)
using this:
vs = vs' @ [v]

goal (1 subgoal):
 1. vs = vs' @ [v]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vs = vs' @ [v]

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
vs = vs' @ [v]

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x)
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x)
[PROOF STEP]
by (intro finsum_cong') (auto simp add: in_mono append_Cons_nth_left)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
note c_def
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs' ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "(vs' @ [v]) ! l = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vs' @ [v]) ! l = v
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. (vs' @ [v]) ! l = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(vs' @ [v]) ! l = v

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(vs' @ [v]) ! l = v

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "\<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
proof (cases "v \<in> set vs'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v \<in> set vs'

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> set vs'
[PROOF STEP]
have I: "set vs' = insert v (set vs' - {v})"
[PROOF STATE]
proof (prove)
using this:
v \<in> set vs'

goal (1 subgoal):
 1. set vs' = insert v (set vs' - {v})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set vs' = insert v (set vs' - {v})

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
define c' where "c' x = (if x = v then c x + g l else c x)" for x
[PROOF STATE]
proof (state)
this:
c' ?x = (if ?x = v then c ?x + g l else c ?x)

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
          = of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v))
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v))
[PROOF STEP]
by (subst I, subst finsum_insert) fastforce+
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v))

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v))

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "\<dots> = of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)) = of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)) = of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (subst a_assoc) (auto intro!: finsum_closed)
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)) = of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + (of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)) = of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v = of_int (c' v)  \<cdot>\<^sub>v v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v = of_int (c' v) \<cdot>\<^sub>v v
[PROOF STEP]
unfolding c'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v = of_int (if v = v then c v + g l else c v) \<cdot>\<^sub>v v
[PROOF STEP]
by (auto simp add: add_smult_distrib_vec)
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v = of_int (c' v) \<cdot>\<^sub>v v

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + of_int (c v) \<cdot>\<^sub>v v = of_int (c' v) \<cdot>\<^sub>v v

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding c'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>va\<in>set vs' - {v}. of_int (if va = v then c va + g l else c va) \<cdot>\<^sub>v va)
[PROOF STEP]
by (intro finsum_cong') (auto)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v)
               = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
using Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (subst finsum_insert[symmetric]) (auto)
[PROOF STATE]
proof (state)
this:
of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs' - {v}. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. v \<in> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
 2. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
using vs'_def
[PROOF STATE]
proof (prove)
using this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
vs = vs' @ [v]

goal (1 subgoal):
 1. \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
v \<notin> set vs'

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
define c' where "c' x = (if x = v then g l else c x)" for x
[PROOF STATE]
proof (state)
this:
c' ?x = (if ?x = v then g l else c ?x)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
          = of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding c'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (if v = v then g l else c v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding c'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>va\<in>set vs'. of_int (if va = v then g l else c va) \<cdot>\<^sub>v va)
[PROOF STEP]
using Suc False vs'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
v \<notin> set vs'
vs = vs' @ [v]

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>va\<in>set vs'. of_int (if va = v then g l else c va) \<cdot>\<^sub>v va)
[PROOF STEP]
by (auto intro!: finsum_cong')
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v)
               = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
using False Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
v \<notin> set vs'
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (subst finsum_insert[symmetric]) (auto)
[PROOF STATE]
proof (state)
this:
of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (c' v) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding c'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>va\<in>set vs'. of_int (if va = v then g l else c va) \<cdot>\<^sub>v va) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
using False Suc vs'_def
[PROOF STATE]
proof (prove)
using this:
v \<notin> set vs'
\<lbrakk>set ?vs1 \<subseteq> carrier_vec n; l = length ?vs1\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v ?vs1 ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs1. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n
Suc l = length vs
vs = vs' @ [v]

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>va\<in>set vs'. of_int (if va = v then g l else c va) \<cdot>\<^sub>v va) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (auto intro!: finsum_cong')
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c' v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<notin> set vs' \<Longrightarrow> \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
using vs'_def
[PROOF STATE]
proof (prove)
using this:
of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>insert v (set vs'). of_int (c' v) \<cdot>\<^sub>v v)
vs = vs' @ [v]

goal (1 subgoal):
 1. \<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>d'. of_int (g l) \<cdot>\<^sub>v v + (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs'. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)

goal (2 subgoals):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
 2. \<And>l vs. \<lbrakk>\<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v); set vs \<subseteq> carrier_vec n; Suc l = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<exists>d'. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<exists>d'. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
unfolding vs'_def
[PROOF STATE]
proof (prove)
using this:
\<exists>d'. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (vs' @ [v]). of_int (d' v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v (vs' @ [v]) ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set (vs' @ [v]). of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<Suc l}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. \<And>vs. \<lbrakk>set vs \<subseteq> carrier_vec n; 0 = length vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<0}. of_int (g x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
qed (auto)


[STATEMENT]
lemma lattice_of_altdef:
  assumes "set vs \<subseteq> carrier_vec n"
  shows "lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "v \<in> lattice_of vs" if "v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
obtain c where v: "v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. (\<And>c. v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
define c' where "c' i = (if find_index vs (vs ! i) = i then c (vs ! i) else 0)" for i
[PROOF STATE]
proof (state)
this:
c' ?i = (if find_index vs (vs ! ?i) = ?i then c (vs ! ?i) else 0)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
have "v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! (find_index vs v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v)
[PROOF STEP]
unfolding v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v)
[PROOF STEP]
by (auto intro!: finsum_cong' simp add: c'_def find_index_in_set in_mono)
[PROOF STATE]
proof (state)
this:
v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
have "\<dots> = (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` (set vs). of_int (c' i) \<cdot>\<^sub>v vs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v) = (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
using assms find_index_in_set find_index_inj
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n
?x \<in> set ?xs \<Longrightarrow> ?xs ! find_index ?xs ?x = ?x
inj_on (find_index ?xs) (set ?xs)

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v) = (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
by (subst finsum_reindex) fastforce+
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v) = (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c' (find_index vs v)) \<cdot>\<^sub>v vs ! find_index vs v) = (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
have "\<dots> = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
have "i \<in> find_index vs ` set vs" if "i < length vs" "find_index vs (vs ! i) = i" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<in> find_index vs ` set vs
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
i < length vs
find_index vs (vs ! i) = i

goal (1 subgoal):
 1. i \<in> find_index vs ` set vs
[PROOF STEP]
by (metis imageI nth_mem)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i1 < length vs; find_index vs (vs ! ?i1) = ?i1\<rbrakk> \<Longrightarrow> ?i1 \<in> find_index vs ` set vs

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?i1 < length vs; find_index vs (vs ! ?i1) = ?i1\<rbrakk> \<Longrightarrow> ?i1 \<in> find_index vs ` set vs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length vs; find_index vs (vs ! ?i1) = ?i1\<rbrakk> \<Longrightarrow> ?i1 \<in> find_index vs ` set vs

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
unfolding c'_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length vs; find_index vs (vs ! ?i1) = ?i1\<rbrakk> \<Longrightarrow> ?i1 \<in> find_index vs ` set vs

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (if find_index vs (vs ! i) = i then c (vs ! i) else 0) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (if find_index vs (vs ! i) = i then c (vs ! i) else 0) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
using find_index_leq_length assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?i1 < length vs; find_index vs (vs ! ?i1) = ?i1\<rbrakk> \<Longrightarrow> ?i1 \<in> find_index vs ` set vs
(find_index ?xs ?x < length ?xs) = (?x \<in> set ?xs)
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (if find_index vs (vs ! i) = i then c (vs ! i) else 0) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (if find_index vs (vs ! i) = i then c (vs ! i) else 0) \<cdot>\<^sub>v vs ! i)
[PROOF STEP]
by (intro add.finprod_mono_neutral_cong_left) (auto simp add: in_mono find_index_leq_length)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>i\<in>find_index vs ` set vs. of_int (c' i) \<cdot>\<^sub>v vs ! i) = (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i)

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
have "\<dots> = sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i) = M.sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i) = M.sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])
[PROOF STEP]
by (subst sumlist_map_as_finsum) (fastforce)+
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>i\<in>set [0..<length vs]. of_int (c' i) \<cdot>\<^sub>v vs ! i) = M.sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
v = M.sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v = M.sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])

goal (1 subgoal):
 1. v \<in> lattice_of vs
[PROOF STEP]
unfolding lattice_of_def
[PROOF STATE]
proof (prove)
using this:
v = M.sumlist (map (\<lambda>i. of_int (c' i) \<cdot>\<^sub>v vs ! i) [0..<length vs])

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> lattice_of vs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> ?v1 \<in> lattice_of vs

goal (1 subgoal):
 1. lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> ?v1 \<in> lattice_of vs

goal (1 subgoal):
 1. lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)" if "v \<in> lattice_of vs" for v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
obtain c where "v = sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. v = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>v \<in> lattice_of vs\<close>
[PROOF STATE]
proof (prove)
using this:
v \<in> lattice_of vs

goal (1 subgoal):
 1. (\<And>c. v = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding lattice_of_def
[PROOF STATE]
proof (prove)
using this:
v \<in> range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]))

goal (1 subgoal):
 1. (\<And>c. v = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
v = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs])

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs])

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
have "\<dots> = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x)
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
v \<in> lattice_of vs
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x)
[PROOF STEP]
by (subst sumlist_map_as_finsum) fastforce+
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x)

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v vs ! i) [0..<length vs]) = (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x)

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
obtain d where  "\<dots> = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>d. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d v) \<cdot>\<^sub>v v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finsum_over_indexes_to_vectors assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set ?vs \<subseteq> carrier_vec n; ?l = length ?vs\<rbrakk> \<Longrightarrow> \<exists>c. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<?l}. of_int (?g x) \<cdot>\<^sub>v ?vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs. of_int (c v) \<cdot>\<^sub>v v)
set vs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (\<And>d. (\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d v) \<cdot>\<^sub>v v) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>x\<in>{0..<length vs}. of_int (c x) \<cdot>\<^sub>v vs ! x) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d v) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
v = (\<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (d v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?v1 \<in> lattice_of vs \<Longrightarrow> ?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> ?v1 \<in> lattice_of vs
?v1 \<in> lattice_of vs \<Longrightarrow> ?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v) \<Longrightarrow> ?v1 \<in> lattice_of vs
?v1 \<in> lattice_of vs \<Longrightarrow> ?v1 \<in> range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
lattice_of vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set vs. of_int (c v) \<cdot>\<^sub>v v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_in_latticeI:
  assumes fs: "set fs \<subseteq> carrier_vec n" and "f \<in> set fs"
  shows "f \<in> lattice_of fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
define c :: "'a vec \<Rightarrow> int" where "c v = (if v = f then 1 else 0)" for v
[PROOF STATE]
proof (state)
this:
c ?v = (if ?v = f then 1 else 0)

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
have "f = (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n
f \<in> set fs

goal (1 subgoal):
 1. f = (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (auto simp add: c_def)
[PROOF STATE]
proof (state)
this:
f = (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f = (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
have "\<dots> = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n
f \<in> set fs

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
by (intro add.finprod_mono_neutral_cong_left) (auto simp add: c_def)
[PROOF STATE]
proof (state)
this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>{f}. of_int (c v) \<cdot>\<^sub>v v) = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
using assms lattice_of_altdef
[PROOF STATE]
proof (prove)
using this:
f = (\<Oplus>\<^bsub>V\<^esub>v\<in>set fs. of_int (c v) \<cdot>\<^sub>v v)
set fs \<subseteq> carrier_vec n
f \<in> set fs
set ?vs \<subseteq> carrier_vec n \<Longrightarrow> lattice_of ?vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. f \<in> lattice_of fs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f \<in> lattice_of fs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lattice_of_eq_set:
  assumes "set fs = set gs" "set fs \<subseteq> carrier_vec n"
  shows "lattice_of fs = lattice_of gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of fs = lattice_of gs
[PROOF STEP]
using assms lattice_of_altdef
[PROOF STATE]
proof (prove)
using this:
set fs = set gs
set fs \<subseteq> carrier_vec n
set ?vs \<subseteq> carrier_vec n \<Longrightarrow> lattice_of ?vs = range (\<lambda>c. \<Oplus>\<^bsub>V\<^esub>v\<in>set ?vs. of_int (c v) \<cdot>\<^sub>v v)

goal (1 subgoal):
 1. lattice_of fs = lattice_of gs
[PROOF STEP]
by simp


[STATEMENT]
lemma lattice_of_swap: assumes fs: "set fs \<subseteq> carrier_vec n"
  and ij: "i < length fs" "j < length fs" "i \<noteq> j"
  and gs: "gs = fs[ i := fs ! j, j := fs ! i]"
shows "lattice_of gs = lattice_of fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
using assms mset_swap
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n
i < length fs
j < length fs
i \<noteq> j
gs = fs[i := fs ! j, j := fs ! i]
\<lbrakk>?i < length ?ls; ?j < length ?ls\<rbrakk> \<Longrightarrow> mset (?ls[?j := ?ls ! ?i, ?i := ?ls ! ?j]) = mset ?ls

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
by (intro lattice_of_eq_set) auto