[STATEMENT]
lemma inv_in_span:
  assumes incarr[intro]:"U \<subseteq> carrier_vec n" and insp:"a \<in> span U"
  shows "- a \<in> span U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
from insp[THEN in_spanE]
[PROOF STATE]
proof (chain)
picking this:
\<exists>aa A. a = lincomb aa A \<and> finite A \<and> A \<subseteq> U
[PROOF STEP]
obtain aa A where a:"a = lincomb aa A" "finite A" "A \<subseteq> U"
[PROOF STATE]
proof (prove)
using this:
\<exists>aa A. a = lincomb aa A \<and> finite A \<and> A \<subseteq> U

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

goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
U \<subseteq> carrier_vec n
a \<in> local.span U
a = lincomb aa A
finite A
A \<subseteq> U
[PROOF STEP]
have [intro!]:"(\<lambda>v. aa v \<cdot>\<^sub>v v) \<in> A \<rightarrow> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> carrier_vec n
a \<in> local.span U
a = lincomb aa A
finite A
A \<subseteq> U

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

goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
from a(1)
[PROOF STATE]
proof (chain)
picking this:
a = lincomb aa A
[PROOF STEP]
have e1:"- a = lincomb (\<lambda> x. - 1 * aa x) A"
[PROOF STATE]
proof (prove)
using this:
a = lincomb aa A

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

goal (1 subgoal):
 1. - a = (\<Oplus>\<^bsub>V\<^esub>v\<in>A. - (1::'a) \<cdot>\<^sub>v (aa v \<cdot>\<^sub>v v))
[PROOF STEP]
by(subst finsum_smult[symmetric]) force+
[PROOF STATE]
proof (state)
this:
- a = lincomb (\<lambda>x. - (1::'a) * aa x) A

goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
using e1 a span_def
[PROOF STATE]
proof (prove)
using this:
- a = lincomb (\<lambda>x. - (1::'a) * aa x) A
a = lincomb aa A
finite A
A \<subseteq> U
local.span ?S = {lincomb a A |a A. finite A \<and> A \<subseteq> ?S}

goal (1 subgoal):
 1. - a \<in> local.span U
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
- a \<in> local.span U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma non_span_det_zero:
  assumes len: "length G = n"
  and nonb:"\<not> (carrier_vec n \<subseteq> span (set G))"
  and carr:"set G \<subseteq> carrier_vec n"
  shows "det (mat_of_rows n G) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
unfolding det_0_iff_vec_prod_zero
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
let ?A = "(mat_of_rows n G)\<^sup>T"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
let ?B = "1\<^sub>m n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from carr
[PROOF STATE]
proof (chain)
picking this:
set G \<subseteq> carrier_vec n
[PROOF STEP]
have carr_mat:"?A \<in> carrier_mat n n" "?B \<in> carrier_mat n n" "mat_of_rows n G \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
set G \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T \<in> carrier_mat n n &&& 1\<^sub>m n \<in> carrier_mat n n &&& mat_of_rows n G \<in> carrier_mat n n
[PROOF STEP]
using len mat_of_rows_carrier(1)
[PROOF STATE]
proof (prove)
using this:
set G \<subseteq> carrier_vec n
length G = n
mat_of_rows ?n ?vs \<in> carrier_mat (length ?vs) ?n

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T \<in> carrier_mat n n &&& 1\<^sub>m n \<in> carrier_mat n n &&& mat_of_rows n G \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mat_of_rows n G)\<^sup>T \<in> carrier_mat n n
1\<^sub>m n \<in> carrier_mat n n
mat_of_rows n G \<in> carrier_mat n n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from carr
[PROOF STATE]
proof (chain)
picking this:
set G \<subseteq> carrier_vec n
[PROOF STEP]
have g_len:"\<And> i. i < length G \<Longrightarrow> G ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set G \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < length G \<Longrightarrow> G ! i \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i5 < length G \<Longrightarrow> G ! ?i5 \<in> carrier_vec n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from nonb
[PROOF STATE]
proof (chain)
picking this:
\<not> carrier_vec n \<subseteq> local.span (set G)
[PROOF STEP]
obtain v where v:"v \<in> carrier_vec n" "v \<notin> span (set G)"
[PROOF STATE]
proof (prove)
using this:
\<not> carrier_vec n \<subseteq> local.span (set G)

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> carrier_vec n; v \<notin> local.span (set G)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
v \<in> carrier_vec n
v \<notin> local.span (set G)

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
hence "v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<notin> local.span (set G)

goal (1 subgoal):
 1. v \<noteq> 0\<^sub>v n
[PROOF STEP]
using span_zero
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<notin> local.span (set G)
0\<^sub>v n \<in> local.span ?U

goal (1 subgoal):
 1. v \<noteq> 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
obtain B C where gj:"gauss_jordan ?A ?B = (B,C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B C. gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n) = (B, C) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n) = (B, C)

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
note gj = carr_mat(1,2) gj
[PROOF STATE]
proof (state)
this:
(mat_of_rows n G)\<^sup>T \<in> carrier_mat n n
1\<^sub>m n \<in> carrier_mat n n
gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n) = (B, C)

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
hence B:"B = fst (gauss_jordan ?A ?B)"
[PROOF STATE]
proof (prove)
using this:
(mat_of_rows n G)\<^sup>T \<in> carrier_mat n n
1\<^sub>m n \<in> carrier_mat n n
gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n) = (B, C)

goal (1 subgoal):
 1. B = fst (gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B = fst (gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n))

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from gauss_jordan[OF gj]
[PROOF STATE]
proof (chain)
picking this:
?x \<in> carrier_vec n \<Longrightarrow> ((mat_of_rows n G)\<^sup>T *\<^sub>v ?x = 0\<^sub>v n) = (B *\<^sub>v ?x = 0\<^sub>v n)
?X \<in> carrier_mat n n \<Longrightarrow> ((mat_of_rows n G)\<^sup>T * ?X = 1\<^sub>m n) = (B * ?X = C)
B \<in> carrier_mat n n
C \<in> carrier_mat n n
[PROOF STEP]
have BC:"B \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
?x \<in> carrier_vec n \<Longrightarrow> ((mat_of_rows n G)\<^sup>T *\<^sub>v ?x = 0\<^sub>v n) = (B *\<^sub>v ?x = 0\<^sub>v n)
?X \<in> carrier_mat n n \<Longrightarrow> ((mat_of_rows n G)\<^sup>T * ?X = 1\<^sub>m n) = (B * ?X = C)
B \<in> carrier_mat n n
C \<in> carrier_mat n n

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

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from gauss_jordan_transform[OF gj]
[PROOF STATE]
proof (chain)
picking this:
\<exists>P\<in>Units (ring_mat TYPE('a) n ?b). B = P * (mat_of_rows n G)\<^sup>T \<and> C = P * 1\<^sub>m n
[PROOF STEP]
obtain P where
   P:"P\<in>Units (ring_mat TYPE('a) n ?B)"  "B = P * ?A"
[PROOF STATE]
proof (prove)
using this:
\<exists>P\<in>Units (ring_mat TYPE('a) n ?b). B = P * (mat_of_rows n G)\<^sup>T \<and> C = P * 1\<^sub>m n

goal (1 subgoal):
 1. (\<And>P. \<lbrakk>P \<in> Units (ring_mat TYPE('a) n (1\<^sub>m n)); B = P * (mat_of_rows n G)\<^sup>T\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
P \<in> Units (ring_mat TYPE('a) n (1\<^sub>m n))
B = P * (mat_of_rows n G)\<^sup>T

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
hence PC:"P \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
P \<in> Units (ring_mat TYPE('a) n (1\<^sub>m n))
B = P * (mat_of_rows n G)\<^sup>T

goal (1 subgoal):
 1. P \<in> carrier_mat n n
[PROOF STEP]
unfolding Units_def
[PROOF STATE]
proof (prove)
using this:
P \<in> {y \<in> carrier (ring_mat TYPE('a) n (1\<^sub>m n)). \<exists>x\<in>carrier (ring_mat TYPE('a) n (1\<^sub>m n)). x \<otimes>\<^bsub>ring_mat TYPE('a) n (1\<^sub>m n)\<^esub> y = \<one>\<^bsub>ring_mat TYPE('a) n (1\<^sub>m n)\<^esub> \<and> y \<otimes>\<^bsub>ring_mat TYPE('a) n (1\<^sub>m n)\<^esub> x = \<one>\<^bsub>ring_mat TYPE('a) n (1\<^sub>m n)\<^esub>}
B = P * (mat_of_rows n G)\<^sup>T

goal (1 subgoal):
 1. P \<in> carrier_mat n n
[PROOF STEP]
by (simp add: ring_mat_simps)
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat n n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from mat_inverse[OF PC] P
[PROOF STATE]
proof (chain)
picking this:
mat_inverse P = None \<Longrightarrow> P \<notin> Units (ring_mat TYPE('a) n ?b)
mat_inverse P = Some ?B \<Longrightarrow> P * ?B = 1\<^sub>m n \<and> ?B * P = 1\<^sub>m n \<and> ?B \<in> carrier_mat n n
P \<in> Units (ring_mat TYPE('a) n (1\<^sub>m n))
B = P * (mat_of_rows n G)\<^sup>T
[PROOF STEP]
obtain PI where "mat_inverse P = Some PI"
[PROOF STATE]
proof (prove)
using this:
mat_inverse P = None \<Longrightarrow> P \<notin> Units (ring_mat TYPE('a) n ?b)
mat_inverse P = Some ?B \<Longrightarrow> P * ?B = 1\<^sub>m n \<and> ?B * P = 1\<^sub>m n \<and> ?B \<in> carrier_mat n n
P \<in> Units (ring_mat TYPE('a) n (1\<^sub>m n))
B = P * (mat_of_rows n G)\<^sup>T

goal (1 subgoal):
 1. (\<And>PI. mat_inverse P = Some PI \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
mat_inverse P = Some PI

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
from mat_inverse(2)[OF PC this]
[PROOF STATE]
proof (chain)
picking this:
P * PI = 1\<^sub>m n \<and> PI * P = 1\<^sub>m n \<and> PI \<in> carrier_mat n n
[PROOF STEP]
have PI:"P * PI = 1\<^sub>m n" "PI * P = 1\<^sub>m n" "PI \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
P * PI = 1\<^sub>m n \<and> PI * P = 1\<^sub>m n \<and> PI \<in> carrier_mat n n

goal (1 subgoal):
 1. P * PI = 1\<^sub>m n &&& PI * P = 1\<^sub>m n &&& PI \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P * PI = 1\<^sub>m n
PI * P = 1\<^sub>m n
PI \<in> carrier_mat n n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
have "B \<noteq> 1\<^sub>m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<noteq> 1\<^sub>m n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
assume "B = ?B"
[PROOF STATE]
proof (state)
this:
B = 1\<^sub>m n

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
hence "?A * P = ?B"
[PROOF STATE]
proof (prove)
using this:
B = 1\<^sub>m n

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T * P = 1\<^sub>m n
[PROOF STEP]
unfolding P
[PROOF STATE]
proof (prove)
using this:
P * (mat_of_rows n G)\<^sup>T = 1\<^sub>m n

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T * P = 1\<^sub>m n
[PROOF STEP]
using PC P(2) carr_mat(1) mat_mult_left_right_inverse
[PROOF STATE]
proof (prove)
using this:
P * (mat_of_rows n G)\<^sup>T = 1\<^sub>m n
P \<in> carrier_mat n n
B = P * (mat_of_rows n G)\<^sup>T
(mat_of_rows n G)\<^sup>T \<in> carrier_mat n n
\<lbrakk>?A \<in> carrier_mat ?n ?n; ?B \<in> carrier_mat ?n ?n; ?A * ?B = 1\<^sub>m ?n\<rbrakk> \<Longrightarrow> ?B * ?A = 1\<^sub>m ?n

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T * P = 1\<^sub>m n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(mat_of_rows n G)\<^sup>T * P = 1\<^sub>m n

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
hence "?A * P *\<^sub>v v = v"
[PROOF STATE]
proof (prove)
using this:
(mat_of_rows n G)\<^sup>T * P = 1\<^sub>m n

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T * P *\<^sub>v v = v
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
(mat_of_rows n G)\<^sup>T * P = 1\<^sub>m n
v \<in> carrier_vec n
v \<notin> local.span (set G)

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T * P *\<^sub>v v = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(mat_of_rows n G)\<^sup>T * P *\<^sub>v v = v

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
hence "?A *\<^sub>v (P *\<^sub>v v) = v"
[PROOF STATE]
proof (prove)
using this:
(mat_of_rows n G)\<^sup>T * P *\<^sub>v v = v

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T *\<^sub>v (P *\<^sub>v v) = v
[PROOF STEP]
unfolding assoc_mult_mat_vec[OF carr_mat(1) PC v(1)]
[PROOF STATE]
proof (prove)
using this:
(mat_of_rows n G)\<^sup>T *\<^sub>v (P *\<^sub>v v) = v

goal (1 subgoal):
 1. (mat_of_rows n G)\<^sup>T *\<^sub>v (P *\<^sub>v v) = v
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(mat_of_rows n G)\<^sup>T *\<^sub>v (P *\<^sub>v v) = v

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
hence v_eq:"mat_of_cols n G *\<^sub>v (P *\<^sub>v v) = v"
[PROOF STATE]
proof (prove)
using this:
(mat_of_rows n G)\<^sup>T *\<^sub>v (P *\<^sub>v v) = v

goal (1 subgoal):
 1. mat_of_cols n G *\<^sub>v (P *\<^sub>v v) = v
[PROOF STEP]
unfolding transpose_mat_of_rows
[PROOF STATE]
proof (prove)
using this:
mat_of_cols n G *\<^sub>v (P *\<^sub>v v) = v

goal (1 subgoal):
 1. mat_of_cols n G *\<^sub>v (P *\<^sub>v v) = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_of_cols n G *\<^sub>v (P *\<^sub>v v) = v

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
have pvc:"P *\<^sub>v v \<in> carrier_vec (length G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P *\<^sub>v v \<in> carrier_vec (length G)
[PROOF STEP]
using PC v len
[PROOF STATE]
proof (prove)
using this:
P \<in> carrier_mat n n
v \<in> carrier_vec n
v \<notin> local.span (set G)
length G = n

goal (1 subgoal):
 1. P *\<^sub>v v \<in> carrier_vec (length G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P *\<^sub>v v \<in> carrier_vec (length G)

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
from mat_of_cols_mult_as_finsum[OF pvc g_len,unfolded v_eq]
[PROOF STATE]
proof (chain)
picking this:
(\<And>i. i < length G \<Longrightarrow> i < length G) \<Longrightarrow> v = lincomb (\<lambda>l. \<Sum>i = 0..<length G. if l = G ! i then (P *\<^sub>v v) $ i else (0::'a)) (set G)
[PROOF STEP]
obtain a where
      "v = lincomb a (set G)"
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i < length G \<Longrightarrow> i < length G) \<Longrightarrow> v = lincomb (\<lambda>l. \<Sum>i = 0..<length G. if l = G ! i then (P *\<^sub>v v) $ i else (0::'a)) (set G)

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

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
hence "v \<in> span (set G)"
[PROOF STATE]
proof (prove)
using this:
v = lincomb a (set G)

goal (1 subgoal):
 1. v \<in> local.span (set G)
[PROOF STEP]
by (intro in_spanI[OF _ finite_set subset_refl])
[PROOF STATE]
proof (state)
this:
v \<in> local.span (set G)

goal (1 subgoal):
 1. B = 1\<^sub>m n \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
v \<in> local.span (set G)

goal (1 subgoal):
 1. False
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
v \<in> local.span (set G)
v \<in> carrier_vec n
v \<notin> local.span (set G)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
B \<noteq> 1\<^sub>m n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
with det_non_zero_imp_unit[OF carr_mat(1)]
[PROOF STATE]
proof (chain)
picking this:
det (mat_of_rows n G)\<^sup>T \<noteq> (0::'a) \<Longrightarrow> (mat_of_rows n G)\<^sup>T \<in> Units (ring_mat TYPE('a) n ?b)
B \<noteq> 1\<^sub>m n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
det (mat_of_rows n G)\<^sup>T \<noteq> (0::'a) \<Longrightarrow> (mat_of_rows n G)\<^sup>T \<in> Units (ring_mat TYPE('a) n ?b)
B \<noteq> 1\<^sub>m n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
unfolding gauss_jordan_check_invertable[OF carr_mat(1,2)] B det_transpose[OF carr_mat(3)]
[PROOF STATE]
proof (prove)
using this:
det (mat_of_rows n G) \<noteq> (0::'a) \<Longrightarrow> fst (gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n)) = 1\<^sub>m n
fst (gauss_jordan (mat_of_rows n G)\<^sup>T (1\<^sub>m n)) \<noteq> 1\<^sub>m n

goal (1 subgoal):
 1. det (mat_of_rows n G) = (0::'a)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n G) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma span_basis_det_zero_iff:
assumes "length G = n" "set G \<subseteq> carrier_vec n"
shows "carrier_vec n \<subseteq> span (set G) \<longleftrightarrow> det (mat_of_rows n G) \<noteq> 0" (is ?q1)
      "carrier_vec n \<subseteq> span (set G) \<longleftrightarrow> basis (set G)" (is ?q2)
      "det (mat_of_rows n G) \<noteq> 0 \<longleftrightarrow> basis (set G)" (is ?q3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a)) &&& (carrier_vec n \<subseteq> local.span (set G)) = basis (set G) &&& (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a))
 2. (carrier_vec n \<subseteq> local.span (set G)) = basis (set G)
 3. (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
have dc:"det (mat_of_rows n G) \<noteq> 0 \<Longrightarrow> carrier_vec n \<subseteq> span (set G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a) \<Longrightarrow> carrier_vec n \<subseteq> local.span (set G)
[PROOF STEP]
using assms non_span_det_zero
[PROOF STATE]
proof (prove)
using this:
length G = n
set G \<subseteq> carrier_vec n
\<lbrakk>length ?G = n; \<not> carrier_vec n \<subseteq> local.span (set ?G); set ?G \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> det (mat_of_rows n ?G) = (0::'a)

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a) \<Longrightarrow> carrier_vec n \<subseteq> local.span (set G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n G) \<noteq> (0::'a) \<Longrightarrow> carrier_vec n \<subseteq> local.span (set G)

goal (3 subgoals):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a))
 2. (carrier_vec n \<subseteq> local.span (set G)) = basis (set G)
 3. (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
have cb:"carrier_vec n \<subseteq> span (set G) \<Longrightarrow> basis (set G)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier_vec n \<subseteq> local.span (set G) \<Longrightarrow> basis (set G)
[PROOF STEP]
using assms basis_list_basis
[PROOF STATE]
proof (prove)
using this:
length G = n
set G \<subseteq> carrier_vec n
basis_list ?fs \<Longrightarrow> distinct ?fs
basis_list ?fs \<Longrightarrow> lin_indpt (set ?fs)
basis_list ?fs \<Longrightarrow> basis (set ?fs)

goal (1 subgoal):
 1. carrier_vec n \<subseteq> local.span (set G) \<Longrightarrow> basis (set G)
[PROOF STEP]
by (auto simp: basis_list_def)
[PROOF STATE]
proof (state)
this:
carrier_vec n \<subseteq> local.span (set G) \<Longrightarrow> basis (set G)

goal (3 subgoals):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a))
 2. (carrier_vec n \<subseteq> local.span (set G)) = basis (set G)
 3. (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
have bd:"basis (set G) \<Longrightarrow> det (mat_of_rows n G) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis (set G) \<Longrightarrow> det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
using assms basis_det_nonzero
[PROOF STATE]
proof (prove)
using this:
length G = n
set G \<subseteq> carrier_vec n
\<lbrakk>basis (set ?G); length ?G = n\<rbrakk> \<Longrightarrow> det (mat_of_rows n ?G) \<noteq> (0::'a)

goal (1 subgoal):
 1. basis (set G) \<Longrightarrow> det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis (set G) \<Longrightarrow> det (mat_of_rows n G) \<noteq> (0::'a)

goal (3 subgoals):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a))
 2. (carrier_vec n \<subseteq> local.span (set G)) = basis (set G)
 3. (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
show ?q1 ?q2 ?q3
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a)) &&& (carrier_vec n \<subseteq> local.span (set G)) = basis (set G) &&& (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
using dc cb bd
[PROOF STATE]
proof (prove)
using this:
det (mat_of_rows n G) \<noteq> (0::'a) \<Longrightarrow> carrier_vec n \<subseteq> local.span (set G)
carrier_vec n \<subseteq> local.span (set G) \<Longrightarrow> basis (set G)
basis (set G) \<Longrightarrow> det (mat_of_rows n G) \<noteq> (0::'a)

goal (1 subgoal):
 1. (carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a)) &&& (carrier_vec n \<subseteq> local.span (set G)) = basis (set G) &&& (det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
(carrier_vec n \<subseteq> local.span (set G)) = (det (mat_of_rows n G) \<noteq> (0::'a))
(carrier_vec n \<subseteq> local.span (set G)) = basis (set G)
(det (mat_of_rows n G) \<noteq> (0::'a)) = basis (set G)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lin_indpt_list_nonzero:
  assumes "lin_indpt_list G"
  shows "0\<^sub>v n \<notin> set G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n \<notin> set G
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0\<^sub>v n \<notin> set G
[PROOF STEP]
from assms[unfolded lin_indpt_list_def]
[PROOF STATE]
proof (chain)
picking this:
set G \<subseteq> carrier_vec n \<and> distinct G \<and> lin_indpt (set G)
[PROOF STEP]
have "lin_indpt (set G)"
[PROOF STATE]
proof (prove)
using this:
set G \<subseteq> carrier_vec n \<and> distinct G \<and> lin_indpt (set G)

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

goal (1 subgoal):
 1. 0\<^sub>v n \<notin> set G
[PROOF STEP]
from vs_zero_lin_dep[OF _ this] assms[unfolded lin_indpt_list_def]
[PROOF STATE]
proof (chain)
picking this:
set G \<subseteq> carrier_vec n \<Longrightarrow> 0\<^sub>v n \<notin> set G
set G \<subseteq> carrier_vec n \<and> distinct G \<and> lin_indpt (set G)
[PROOF STEP]
show zero: "0\<^sub>v n \<notin> set G"
[PROOF STATE]
proof (prove)
using this:
set G \<subseteq> carrier_vec n \<Longrightarrow> 0\<^sub>v n \<notin> set G
set G \<subseteq> carrier_vec n \<and> distinct G \<and> lin_indpt (set G)

goal (1 subgoal):
 1. 0\<^sub>v n \<notin> set G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>v n \<notin> set G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_oc_projection_eq:
  assumes ispr:"is_oc_projection a S v" "is_oc_projection b S v"
    and carr: "S \<subseteq> carrier_vec n" "v \<in> carrier_vec n"
  shows "a = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a = b
[PROOF STEP]
from carr
[PROOF STATE]
proof (chain)
picking this:
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
[PROOF STEP]
have c2:"span S \<subseteq> carrier_vec n" "v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier_vec n
v \<in> carrier_vec n

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

goal (1 subgoal):
 1. a = b
[PROOF STEP]
have a:"v - (v - a) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v - (v - a) = a
[PROOF STEP]
using carr ispr
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
is_oc_projection a S v
is_oc_projection b S v

goal (1 subgoal):
 1. v - (v - a) = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v - (v - a) = a

goal (1 subgoal):
 1. a = b
[PROOF STEP]
have b:"v - (v - b) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v - (v - b) = b
[PROOF STEP]
using carr ispr
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier_vec n
v \<in> carrier_vec n
is_oc_projection a S v
is_oc_projection b S v

goal (1 subgoal):
 1. v - (v - b) = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v - (v - b) = b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
have "(v - a) = (v - b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v - a = v - b
[PROOF STEP]
apply(rule oc_projection_alt_def[OF c2])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. v - a \<in> local.span S
 2. v - (v - a) \<in> orthogonal_complement (local.span S)
 3. v - b \<in> local.span S
 4. v - (v - b) \<in> orthogonal_complement (local.span S)
[PROOF STEP]
using ispr a b
[PROOF STATE]
proof (prove)
using this:
is_oc_projection a S v
is_oc_projection b S v
v - (v - a) = a
v - (v - b) = b

goal (4 subgoals):
 1. v - a \<in> local.span S
 2. v - (v - a) \<in> orthogonal_complement (local.span S)
 3. v - b \<in> local.span S
 4. v - (v - b) \<in> orthogonal_complement (local.span S)
[PROOF STEP]
unfolding in_orthogonal_complement_span[OF carr(1)]
[PROOF STATE]
proof (prove)
using this:
is_oc_projection a S v
is_oc_projection b S v
v - (v - a) = a
v - (v - b) = b

goal (4 subgoals):
 1. v - a \<in> local.span S
 2. v - (v - a) \<in> orthogonal_complement S
 3. v - b \<in> local.span S
 4. v - (v - b) \<in> orthogonal_complement S
[PROOF STEP]
unfolding orthogonal_complement_def is_oc_projection_def
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier_vec n \<and> v - a \<in> local.span S \<and> (\<forall>u. u \<in> S \<longrightarrow> a \<bullet> u = (0::'a))
b \<in> carrier_vec n \<and> v - b \<in> local.span S \<and> (\<forall>u. u \<in> S \<longrightarrow> b \<bullet> u = (0::'a))
v - (v - a) = a
v - (v - b) = b

goal (4 subgoals):
 1. v - a \<in> local.span S
 2. v - (v - a) \<in> {x \<in> carrier_vec n. \<forall>y\<in>S. x \<bullet> y = (0::'a)}
 3. v - b \<in> local.span S
 4. v - (v - b) \<in> {x \<in> carrier_vec n. \<forall>y\<in>S. x \<bullet> y = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v - a = v - b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
hence "v - (v - a) = v - (v - b)"
[PROOF STATE]
proof (prove)
using this:
v - a = v - b

goal (1 subgoal):
 1. v - (v - a) = v - (v - b)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
v - (v - a) = v - (v - b)

goal (1 subgoal):
 1. a = b
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
v - (v - a) = v - (v - b)

goal (1 subgoal):
 1. a = b
[PROOF STEP]
unfolding a b
[PROOF STATE]
proof (prove)
using this:
a = b

goal (1 subgoal):
 1. a = b
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_carrier'[intro]:
  assumes "\<And> i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n"
  shows "gso j \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso j \<in> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. gso j \<in> carrier_vec n
[PROOF STEP]
proof(induct j rule:nat_less_induct[rule_format])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>m. \<lbrakk>m < na; \<And>i. i \<le> m \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso m \<in> carrier_vec n; \<And>i. i \<le> na \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso na \<in> carrier_vec n
[PROOF STEP]
case (1 j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m1 < j; \<And>i. i \<le> ?m1 \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso ?m1 \<in> carrier_vec n
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>na. \<lbrakk>\<And>m. \<lbrakk>m < na; \<And>i. i \<le> m \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso m \<in> carrier_vec n; \<And>i. i \<le> na \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso na \<in> carrier_vec n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?m1 < j; \<And>i. i \<le> ?m1 \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso ?m1 \<in> carrier_vec n
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?m1 < j; \<And>i. i \<le> ?m1 \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso ?m1 \<in> carrier_vec n
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. gso j \<in> carrier_vec n
[PROOF STEP]
unfolding gso.simps[of j]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?m1 < j; \<And>i. i \<le> ?m1 \<Longrightarrow> fs ! i \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gso ?m1 \<in> carrier_vec n
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. fs ! j + sumlist (map (\<lambda>j. - \<mu> j j \<cdot>\<^sub>v gso j) [0..<j]) \<in> carrier_vec n
[PROOF STEP]
by (auto intro!:sumlist_carrier add_carrier_vec)
[PROOF STATE]
proof (state)
this:
gso j \<in> carrier_vec n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjuster_wit: assumes res: "adjuster_wit wits w us = (wits',a)"
  and w: "w \<in> carrier_vec n"
    and us: "\<And> i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n"
    and us_gs: "us = map gso (rev [0 ..< j])"
    and wits: "wits = map (\<mu> i) [j ..< i]"
    and j: "j \<le> n" "j \<le> i"
    and wi: "w = fs ! i"
  shows "adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0 ..< i] \<and>
      (a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
using res us us_gs wits j
[PROOF STATE]
proof (prove)
using this:
adjuster_wit wits w us = (wits', a)
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
us = map gso (rev [0..<j])
wits = map (\<mu> i) [j..<i]
j \<le> n
j \<le> i

goal (1 subgoal):
 1. adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
proof (induct us arbitrary: wits wits' a j)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
case (Cons u us wits wits' a j)
[PROOF STATE]
proof (state)
this:
\<lbrakk>adjuster_wit ?wits1 w us = (?wits'1, ?a1); \<And>i. i \<le> ?j1 \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<?j1]); ?wits1 = map (\<mu> i) [?j1..<i]; ?j1 \<le> n; ?j1 \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = ?a1 \<and> ?a1 \<in> carrier_vec n \<and> ?wits'1 = map (\<mu> i) [0..<i] \<and> ?a1 = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<?j1])
adjuster_wit wits w (u # us) = (wits', a)
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
u # us = map gso (rev [0..<j])
wits = map (\<mu> i) [j..<i]
j \<le> n
j \<le> i

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
note us_gs = Cons(4)
[PROOF STATE]
proof (state)
this:
u # us = map gso (rev [0..<j])

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
note wits = Cons(5)
[PROOF STATE]
proof (state)
this:
wits = map (\<mu> i) [j..<i]

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
note jn = Cons(6-7)
[PROOF STATE]
proof (state)
this:
j \<le> n
j \<le> i

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from us_gs
[PROOF STATE]
proof (chain)
picking this:
u # us = map gso (rev [0..<j])
[PROOF STEP]
obtain jj where j: "j = Suc jj"
[PROOF STATE]
proof (prove)
using this:
u # us = map gso (rev [0..<j])

goal (1 subgoal):
 1. (\<And>jj. j = Suc jj \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases j, auto)
[PROOF STATE]
proof (state)
this:
j = Suc jj

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from jn j
[PROOF STATE]
proof (chain)
picking this:
j \<le> n
j \<le> i
j = Suc jj
[PROOF STEP]
have jj: "jj \<le> n" "jj < n" "jj \<le> i" "jj < i"
[PROOF STATE]
proof (prove)
using this:
j \<le> n
j \<le> i
j = Suc jj

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

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
have zj: "[0 ..< j] = [0 ..< jj] @ [jj]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<j] = [0..<jj] @ [jj]
[PROOF STEP]
unfolding j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc jj] = [0..<jj] @ [jj]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[0..<j] = [0..<jj] @ [jj]

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
have jjn: "[jj ..< i] = jj # [j ..< i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [jj..<i] = jj # [j..<i]
[PROOF STEP]
using jj
[PROOF STATE]
proof (prove)
using this:
jj \<le> n
jj < n
jj \<le> i
jj < i

goal (1 subgoal):
 1. [jj..<i] = jj # [j..<i]
[PROOF STEP]
unfolding j
[PROOF STATE]
proof (prove)
using this:
jj \<le> n
jj < n
jj \<le> i
jj < i

goal (1 subgoal):
 1. [jj..<i] = jj # [Suc jj..<i]
[PROOF STEP]
by (metis upt_conv_Cons)
[PROOF STATE]
proof (state)
this:
[jj..<i] = jj # [j..<i]

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from us_gs[unfolded zj]
[PROOF STATE]
proof (chain)
picking this:
u # us = map gso (rev ([0..<jj] @ [jj]))
[PROOF STEP]
have ugs: "u = gso jj" and us: "us = map gso (rev [0..<jj])"
[PROOF STATE]
proof (prove)
using this:
u # us = map gso (rev ([0..<jj] @ [jj]))

goal (1 subgoal):
 1. u = gso jj &&& us = map gso (rev [0..<jj])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u = gso jj
us = map gso (rev [0..<jj])

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
let ?w = "w \<bullet> u / (u \<bullet> u)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
have muij: "?w = \<mu> i jj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<bullet> u / (u \<bullet> u) = \<mu> i jj
[PROOF STEP]
unfolding \<mu>.simps[of i jj] ugs wi sq_norm_vec_as_cscalar_prod
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i \<bullet> gso jj / (gso jj \<bullet> gso jj) = (if jj < i then fs ! i \<bullet> gso jj / (gso jj \<bullet>c gso jj) else if i = jj then 1::'a else (0::'a))
[PROOF STEP]
using jj
[PROOF STATE]
proof (prove)
using this:
jj \<le> n
jj < n
jj \<le> i
jj < i

goal (1 subgoal):
 1. fs ! i \<bullet> gso jj / (gso jj \<bullet> gso jj) = (if jj < i then fs ! i \<bullet> gso jj / (gso jj \<bullet>c gso jj) else if i = jj then 1::'a else (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<bullet> u / (u \<bullet> u) = \<mu> i jj

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
have wwits: "?w # wits = map (\<mu> i) [jj..<i]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<bullet> u / (u \<bullet> u) # wits = map (\<mu> i) [jj..<i]
[PROOF STEP]
unfolding jjn wits muij
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> i jj # map (\<mu> i) [j..<i] = map (\<mu> i) (jj # [j..<i])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w \<bullet> u / (u \<bullet> u) # wits = map (\<mu> i) [jj..<i]

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
obtain wwits b where rec: "adjuster_wit (?w # wits) w us = (wwits,b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>wwits b. adjuster_wit (w \<bullet> u / (u \<bullet> u) # wits) w us = (wwits, b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
adjuster_wit (w \<bullet> u / (u \<bullet> u) # wits) w us = (wwits, b)

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from Cons(1)[OF this Cons(3) us wwits jj(1,3),unfolded j]
[PROOF STATE]
proof (chain)
picking this:
(\<And>i. i \<le> jj \<Longrightarrow> i \<le> Suc jj) \<Longrightarrow> adjuster n w us = b \<and> b \<in> carrier_vec n \<and> wwits = map (\<mu> i) [0..<i] \<and> b = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj])
[PROOF STEP]
have IH:
     "adjuster n w us = b" "wwits = map (\<mu> i) [0..<i]"
     "b = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj])"
      and b: "b \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<le> jj \<Longrightarrow> i \<le> Suc jj) \<Longrightarrow> adjuster n w us = b \<and> b \<in> carrier_vec n \<and> wwits = map (\<mu> i) [0..<i] \<and> b = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj])

goal (1 subgoal):
 1. (adjuster n w us = b &&& wwits = map (\<mu> i) [0..<i] &&& b = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj])) &&& b \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjuster n w us = b
wwits = map (\<mu> i) [0..<i]
b = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj])
b \<in> carrier_vec n

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from Cons(2)[simplified, unfolded Let_def rec split sq_norm_vec_as_cscalar_prod
      cscalar_prod_is_scalar_prod]
[PROOF STATE]
proof (chain)
picking this:
(wwits, - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + b) = (wits', a)
[PROOF STEP]
have id: "wits' = wwits" and a: "a = - ?w \<cdot>\<^sub>v u + b"
[PROOF STATE]
proof (prove)
using this:
(wwits, - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + b) = (wits', a)

goal (1 subgoal):
 1. wits' = wwits &&& a = - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wits' = wwits
a = - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + b

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
have 1: "adjuster n w (u # us) = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster n w (u # us) = a
[PROOF STEP]
unfolding a IH(1)[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster n w (u # us) = - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + adjuster n w us
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjuster n w (u # us) = a

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from id IH(2)
[PROOF STATE]
proof (chain)
picking this:
wits' = wwits
wwits = map (\<mu> i) [0..<i]
[PROOF STEP]
have wits': "wits' =  map (\<mu> i) [0..<i]"
[PROOF STATE]
proof (prove)
using this:
wits' = wwits
wwits = map (\<mu> i) [0..<i]

goal (1 subgoal):
 1. wits' = map (\<mu> i) [0..<i]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
wits' = map (\<mu> i) [0..<i]

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
have carr:"set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]) \<subseteq> carrier_vec n"
            "set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) \<subseteq> carrier_vec n" and u:"u \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]) \<subseteq> carrier_vec n &&& set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) \<subseteq> carrier_vec n) &&& u \<in> carrier_vec n
[PROOF STEP]
using Cons j
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>adjuster_wit ?wits1 w us = (?wits'1, ?a1); \<And>i. i \<le> ?j1 \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<?j1]); ?wits1 = map (\<mu> i) [?j1..<i]; ?j1 \<le> n; ?j1 \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = ?a1 \<and> ?a1 \<in> carrier_vec n \<and> ?wits'1 = map (\<mu> i) [0..<i] \<and> ?a1 = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<?j1])
adjuster_wit wits w (u # us) = (wits', a)
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
u # us = map gso (rev [0..<j])
wits = map (\<mu> i) [j..<i]
j \<le> n
j \<le> i
j = Suc jj

goal (1 subgoal):
 1. (set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]) \<subseteq> carrier_vec n &&& set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) \<subseteq> carrier_vec n) &&& u \<in> carrier_vec n
[PROOF STEP]
by (auto intro!:gso_carrier')
[PROOF STATE]
proof (state)
this:
set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]) \<subseteq> carrier_vec n
set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) \<subseteq> carrier_vec n
u \<in> carrier_vec n

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
from u b a
[PROOF STATE]
proof (chain)
picking this:
u \<in> carrier_vec n
b \<in> carrier_vec n
a = - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + b
[PROOF STEP]
have ac: "a \<in> carrier_vec n" "dim_vec (-?w \<cdot>\<^sub>v u) = n" "dim_vec b = n" "dim_vec u = n"
[PROOF STATE]
proof (prove)
using this:
u \<in> carrier_vec n
b \<in> carrier_vec n
a = - (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u + b

goal (1 subgoal):
 1. (a \<in> carrier_vec n &&& dim_vec (- (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u) = n) &&& dim_vec b = n &&& dim_vec u = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a \<in> carrier_vec n
dim_vec (- (w \<bullet> u / (u \<bullet> u)) \<cdot>\<^sub>v u) = n
dim_vec b = n
dim_vec u = n

goal (2 subgoals):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
 2. \<And>a us wits wits' aa j. \<lbrakk>\<And>wits wits' a j. \<lbrakk>adjuster_wit wits w us = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j]); adjuster_wit wits w (a # us) = (wits', aa); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; a # us = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w (a # us) = aa \<and> aa \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> aa = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjuster n w (u # us) = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
apply (intro conjI[OF 1] ac exI conjI wits')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
unfolding carr a IH zj muij ugs[symmetric] map_append
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - \<mu> i jj \<cdot>\<^sub>v u + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj] @ map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj])
[PROOF STEP]
apply (subst sumlist_append)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) \<subseteq> carrier_vec n
 2. set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj]) \<subseteq> carrier_vec n
 3. - \<mu> i jj \<cdot>\<^sub>v u + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj])
[PROOF STEP]
using Cons.prems j
[PROOF STATE]
proof (prove)
using this:
adjuster_wit wits w (u # us) = (wits', a)
?i1 \<le> j \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
u # us = map gso (rev [0..<j])
wits = map (\<mu> i) [j..<i]
j \<le> n
j \<le> i
j = Suc jj

goal (3 subgoals):
 1. set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) \<subseteq> carrier_vec n
 2. set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj]) \<subseteq> carrier_vec n
 3. - \<mu> i jj \<cdot>\<^sub>v u + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj])
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj]) \<subseteq> carrier_vec n
 2. - \<mu> i jj \<cdot>\<^sub>v u + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj])
[PROOF STEP]
using b u ugs IH(3)
[PROOF STATE]
proof (prove)
using this:
b \<in> carrier_vec n
u \<in> carrier_vec n
u = gso jj
b = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj])

goal (2 subgoals):
 1. set (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj]) \<subseteq> carrier_vec n
 2. - \<mu> i jj \<cdot>\<^sub>v u + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<jj]) + sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [jj])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
adjuster n w (u # us) = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])

goal (1 subgoal):
 1. \<And>wits wits' a j. \<lbrakk>adjuster_wit wits w [] = (wits', a); \<And>i. i \<le> j \<Longrightarrow> fs ! i \<in> carrier_vec n; [] = map gso (rev [0..<j]); wits = map (\<mu> i) [j..<i]; j \<le> n; j \<le> i\<rbrakk> \<Longrightarrow> adjuster n w [] = a \<and> a \<in> carrier_vec n \<and> wits' = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<j])
[PROOF STEP]
qed auto