[STATEMENT]
lemma sub2_wit:
  assumes "set us \<subseteq> carrier_vec n" "set ws \<subseteq> carrier_vec n" "length us + length ws = m"
    and "ws = map (\<lambda> i. fs ! i) [i ..< m]"
    and "us = map gso (rev [0 ..< i])"
    and us: "\<And> j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n"
    and mn: "m \<le> n"
  shows "sub2_wit us ws = (wits,vvs) \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs
    \<and> vvs = map gso [i ..< m] \<and> wits = map (\<lambda> i. map (\<mu> i) [0..<i]) [i ..< m]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub2_wit us ws = (wits, vvs) \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
using assms(1-6)
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> carrier_vec n
set ws \<subseteq> carrier_vec n
length us + length ws = m
ws = map ((!) fs) [i..<m]
us = map gso (rev [0..<i])
?j1 < m \<Longrightarrow> fs ! ?j1 \<in> carrier_vec n

goal (1 subgoal):
 1. sub2_wit us ws = (wits, vvs) \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
proof (induct ws arbitrary: us vvs i wits)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
case (Cons w ws us vs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub2_wit ?us1 ws = (?wits1, ?vvs1); set ?us1 \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length ?us1 + length ws = m; ws = map ((!) fs) [?i1..<m]; ?us1 = map gso (rev [0..<?i1]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n ?us1 ws = ?vvs1 \<and> ?vvs1 = map gso [?i1..<m] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [?i1..<m]
sub2_wit us (w # ws) = (wits, vs)
set us \<subseteq> carrier_vec n
set (w # ws) \<subseteq> carrier_vec n
length us + length (w # ws) = m
w # ws = map ((!) fs) [i..<m]
us = map gso (rev [0..<i])
?j1 < m \<Longrightarrow> fs ! ?j1 \<in> carrier_vec n

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
note us = Cons(3)
[PROOF STATE]
proof (state)
this:
set us \<subseteq> carrier_vec n

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
note wws = Cons(4)
[PROOF STATE]
proof (state)
this:
set (w # ws) \<subseteq> carrier_vec n

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
note wsf' = Cons(6)
[PROOF STATE]
proof (state)
this:
w # ws = map ((!) fs) [i..<m]

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
note us_gs = Cons(7)
[PROOF STATE]
proof (state)
this:
us = map gso (rev [0..<i])

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from wsf'
[PROOF STATE]
proof (chain)
picking this:
w # ws = map ((!) fs) [i..<m]
[PROOF STEP]
have "i < m" "i \<le> m"
[PROOF STATE]
proof (prove)
using this:
w # ws = map ((!) fs) [i..<m]

goal (1 subgoal):
 1. i < m &&& i \<le> m
[PROOF STEP]
by (cases "i < m", auto)+
[PROOF STATE]
proof (state)
this:
i < m
i \<le> m

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
hence i_m: "[i ..< m] = i # [Suc i ..< m]"
[PROOF STATE]
proof (prove)
using this:
i < m
i \<le> m

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

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from \<open>i < m\<close> mn
[PROOF STATE]
proof (chain)
picking this:
i < m
m \<le> n
[PROOF STEP]
have "i < n" "i \<le> n" "i \<le> m"
[PROOF STATE]
proof (prove)
using this:
i < m
m \<le> n

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

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
hence i_n: "[i ..< n] = i # [Suc i ..< n]"
[PROOF STATE]
proof (prove)
using this:
i < n
i \<le> n
i \<le> m

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

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from wsf' i_m
[PROOF STATE]
proof (chain)
picking this:
w # ws = map ((!) fs) [i..<m]
[i..<m] = i # [Suc i..<m]
[PROOF STEP]
have wsf: "ws = map (\<lambda> i. fs ! i) [Suc i ..< m]"
    and fiw: "fs !  i = w"
[PROOF STATE]
proof (prove)
using this:
w # ws = map ((!) fs) [i..<m]
[i..<m] = i # [Suc i..<m]

goal (1 subgoal):
 1. ws = map ((!) fs) [Suc i..<m] &&& fs ! i = w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ws = map ((!) fs) [Suc i..<m]
fs ! i = w

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from wws
[PROOF STATE]
proof (chain)
picking this:
set (w # ws) \<subseteq> carrier_vec n
[PROOF STEP]
have w: "w \<in> carrier_vec n" and ws: "set ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set (w # ws) \<subseteq> carrier_vec n

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

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
have list: "map (\<mu> i) [i ..< i] = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<mu> i) [i..<i] = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<mu> i) [i..<i] = []

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
let ?a = "adjuster_wit [] w us"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
obtain wit a where a: "?a = (wit,a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>wit a. adjuster_wit [] w us = (wit, a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
adjuster_wit [] w us = (wit, a)

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
obtain wits' vv where gs: "sub2_wit ((a + w) # us) ws = (wits',vv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>wits' vv. sub2_wit ((a + w) # us) ws = (wits', vv) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub2_wit ((a + w) # us) ws = (wits', vv)

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from adjuster_wit[OF a w Cons(8) us_gs list[symmetric] \<open>i \<le> n\<close> _ fiw[symmetric]] us wws \<open>i < m\<close>
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>i. i \<le> i \<Longrightarrow> i < m; i \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wit = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
set us \<subseteq> carrier_vec n
set (w # ws) \<subseteq> carrier_vec n
i < m
[PROOF STEP]
have awus: "set ((a + w) # us) \<subseteq> carrier_vec n"
     and aa: "adjuster n w us = a" "a \<in> carrier_vec n"
     and aaa: "a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])"
     and wit: "wit = map (\<mu> i) [0..<i]"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>i. i \<le> i \<Longrightarrow> i < m; i \<le> i\<rbrakk> \<Longrightarrow> adjuster n w us = a \<and> a \<in> carrier_vec n \<and> wit = map (\<mu> i) [0..<i] \<and> a = sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i])
set us \<subseteq> carrier_vec n
set (w # ws) \<subseteq> carrier_vec n
i < m

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

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
have aw_gs: "a + w = gso i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + w = gso i
[PROOF STEP]
unfolding gso.simps[of i] fiw aaa[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a + w = w + a
[PROOF STEP]
using aa(2) w
[PROOF STATE]
proof (prove)
using this:
a \<in> carrier_vec n
w \<in> carrier_vec n

goal (1 subgoal):
 1. a + w = w + a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a + w = gso i

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
with us_gs
[PROOF STATE]
proof (chain)
picking this:
us = map gso (rev [0..<i])
a + w = gso i
[PROOF STEP]
have us_gs': "(a + w) # us = map gso (rev [0..<Suc i])"
[PROOF STATE]
proof (prove)
using this:
us = map gso (rev [0..<i])
a + w = gso i

goal (1 subgoal):
 1. (a + w) # us = map gso (rev [0..<Suc i])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a + w) # us = map gso (rev [0..<Suc i])

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from Cons(1)[OF gs awus ws _ wsf us_gs' Cons(8)] Cons(5)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length ((a + w) # us) + length ws = m; \<And>j. j < m \<Longrightarrow> j < m\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n ((a + w) # us) ws = vv \<and> vv = map gso [Suc i..<m] \<and> wits' = map (\<lambda>i. map (\<mu> i) [0..<i]) [Suc i..<m]
length us + length (w # ws) = m
[PROOF STEP]
have IH: "gram_schmidt_sub2 n ((a + w) # us) ws = vv"
    and vv: "vv = map gso [Suc i..<m]"
    and wits': "wits' = map (\<lambda>i. map (\<mu> i) [0..<i]) [Suc i ..< m]"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ((a + w) # us) + length ws = m; \<And>j. j < m \<Longrightarrow> j < m\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n ((a + w) # us) ws = vv \<and> vv = map gso [Suc i..<m] \<and> wits' = map (\<lambda>i. map (\<mu> i) [0..<i]) [Suc i..<m]
length us + length (w # ws) = m

goal (1 subgoal):
 1. gram_schmidt_sub2 n ((a + w) # us) ws = vv &&& vv = map gso [Suc i..<m] &&& wits' = map (\<lambda>i. map (\<mu> i) [0..<i]) [Suc i..<m]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gram_schmidt_sub2 n ((a + w) # us) ws = vv
vv = map gso [Suc i..<m]
wits' = map (\<lambda>i. map (\<mu> i) [0..<i]) [Suc i..<m]

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from gs a aa IH Cons(5)
[PROOF STATE]
proof (chain)
picking this:
sub2_wit ((a + w) # us) ws = (wits', vv)
adjuster_wit [] w us = (wit, a)
adjuster n w us = a
a \<in> carrier_vec n
gram_schmidt_sub2 n ((a + w) # us) ws = vv
length us + length (w # ws) = m
[PROOF STEP]
have gs_vs: "gram_schmidt_sub2 n us (w # ws) = vs" and vs: "vs = (a + w) # vv"
[PROOF STATE]
proof (prove)
using this:
sub2_wit ((a + w) # us) ws = (wits', vv)
adjuster_wit [] w us = (wit, a)
adjuster n w us = a
a \<in> carrier_vec n
gram_schmidt_sub2 n ((a + w) # us) ws = vv
length us + length (w # ws) = m

goal (1 subgoal):
 1. gram_schmidt_sub2 n us (w # ws) = vs &&& vs = (a + w) # vv
[PROOF STEP]
using Cons(2)
[PROOF STATE]
proof (prove)
using this:
sub2_wit ((a + w) # us) ws = (wits', vv)
adjuster_wit [] w us = (wit, a)
adjuster n w us = a
a \<in> carrier_vec n
gram_schmidt_sub2 n ((a + w) # us) ws = vv
length us + length (w # ws) = m
sub2_wit us (w # ws) = (wits, vs)

goal (1 subgoal):
 1. gram_schmidt_sub2 n us (w # ws) = vs &&& vs = (a + w) # vv
[PROOF STEP]
by (auto simp add: Let_def snd_def split:prod.splits)
[PROOF STATE]
proof (state)
this:
gram_schmidt_sub2 n us (w # ws) = vs
vs = (a + w) # vv

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from Cons(2)[unfolded sub2_wit.simps a split Let_def gs]
[PROOF STATE]
proof (chain)
picking this:
(wit # wits', (a + w) # vv) = (wits, vs)
[PROOF STEP]
have wits: "wits = wit # wits'"
[PROOF STATE]
proof (prove)
using this:
(wit # wits', (a + w) # vv) = (wits, vs)

goal (1 subgoal):
 1. wits = wit # wits'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
wits = wit # wits'

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
from vs vv aw_gs
[PROOF STATE]
proof (chain)
picking this:
vs = (a + w) # vv
vv = map gso [Suc i..<m]
a + w = gso i
[PROOF STEP]
have vs: "vs = map gso [i ..< m]"
[PROOF STATE]
proof (prove)
using this:
vs = (a + w) # vv
vv = map gso [Suc i..<m]
a + w = gso i

goal (1 subgoal):
 1. vs = map gso [i..<m]
[PROOF STEP]
unfolding i_m
[PROOF STATE]
proof (prove)
using this:
vs = (a + w) # vv
vv = map gso [Suc i..<m]
a + w = gso i

goal (1 subgoal):
 1. vs = map gso (i # [Suc i..<m])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vs = map gso [i..<m]

goal (2 subgoals):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
 2. \<And>a ws us vvs i wits. \<lbrakk>\<And>us vvs i wits. \<lbrakk>sub2_wit us ws = (wits, vvs); set us \<subseteq> carrier_vec n; set ws \<subseteq> carrier_vec n; length us + length ws = m; ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us ws = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]; sub2_wit us (a # ws) = (wits, vvs); set us \<subseteq> carrier_vec n; set (a # ws) \<subseteq> carrier_vec n; length us + length (a # ws) = m; a # ws = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us (a # ws) = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
with gs_vs
[PROOF STATE]
proof (chain)
picking this:
gram_schmidt_sub2 n us (w # ws) = vs
vs = map gso [i..<m]
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
gram_schmidt_sub2 n us (w # ws) = vs
vs = map gso [i..<m]

goal (1 subgoal):
 1. gram_schmidt_sub2 n us (w # ws) = vs \<and> vs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
unfolding wits wit wits'
[PROOF STATE]
proof (prove)
using this:
gram_schmidt_sub2 n us (w # ws) = vs
vs = map gso [i..<m]

goal (1 subgoal):
 1. gram_schmidt_sub2 n us (w # ws) = vs \<and> vs = map gso [i..<m] \<and> map (\<mu> i) [0..<i] # map (\<lambda>i. map (\<mu> i) [0..<i]) [Suc i..<m] = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
by (auto simp: i_m)
[PROOF STATE]
proof (state)
this:
gram_schmidt_sub2 n us (w # ws) = vs \<and> vs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]

goal (1 subgoal):
 1. \<And>us vvs i wits. \<lbrakk>sub2_wit us [] = (wits, vvs); set us \<subseteq> carrier_vec n; set [] \<subseteq> carrier_vec n; length us + length [] = m; [] = map ((!) fs) [i..<m]; us = map gso (rev [0..<i]); \<And>j. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n us [] = vvs \<and> vvs = map gso [i..<m] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [i..<m]
[PROOF STEP]
qed auto


[STATEMENT]
lemma partial_connect: fixes vs
  assumes "length fs = m" "k \<le> m" "m \<le> n" "set us \<subseteq> carrier_vec n" "snd (main us) = vs"
  "us = take k fs" "set fs \<subseteq> carrier_vec n"
shows "gram_schmidt n us = vs"
    "vs = map gso [0..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt n us = vs &&& vs = map gso [0..<k]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. gram_schmidt n us = vs
 2. vs = map gso [0..<k]
[PROOF STEP]
have [simp]: "map ((!) fs) [0..<k] = take k fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((!) fs) [0..<k] = take k fs
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
length fs = m
k \<le> m

goal (1 subgoal):
 1. map ((!) fs) [0..<k] = take k fs
[PROOF STEP]
by (intro nth_equalityI, auto)
[PROOF STATE]
proof (state)
this:
map ((!) fs) [0..<k] = take k fs

goal (2 subgoals):
 1. gram_schmidt n us = vs
 2. vs = map gso [0..<k]
[PROOF STEP]
have carr: "j < m \<Longrightarrow> fs ! j \<in> carrier_vec n" for j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length fs = m
k \<le> m
m \<le> n
set us \<subseteq> carrier_vec n
snd (main us) = vs
us = take k fs
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. j < m \<Longrightarrow> fs ! j \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?j1 < m \<Longrightarrow> fs ! ?j1 \<in> carrier_vec n

goal (2 subgoals):
 1. gram_schmidt n us = vs
 2. vs = map gso [0..<k]
[PROOF STEP]
note assms(5)[unfolded main_def]
[PROOF STATE]
proof (state)
this:
snd (sub2_wit [] us) = vs

goal (2 subgoals):
 1. gram_schmidt n us = vs
 2. vs = map gso [0..<k]
[PROOF STEP]
have "gram_schmidt_sub2 n [] (take k fs) = vvs \<and> vvs = map gso [0..<k] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]"
    if "vvs = snd (sub2_wit [] (take k fs))" "wits = fst (sub2_wit [] (take k fs))" for vvs wits
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_sub2 n [] (take k fs) = vvs \<and> vvs = map gso [0..<k] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
length fs = m
k \<le> m
m \<le> n
set us \<subseteq> carrier_vec n
snd (main us) = vs
us = take k fs
set fs \<subseteq> carrier_vec n
vvs = snd (sub2_wit [] (take k fs))
wits = fst (sub2_wit [] (take k fs))

goal (1 subgoal):
 1. gram_schmidt_sub2 n [] (take k fs) = vvs \<and> vvs = map gso [0..<k] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]
[PROOF STEP]
by (intro sub2_wit) (auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?vvs1 = snd (sub2_wit [] (take k fs)); ?wits1 = fst (sub2_wit [] (take k fs))\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n [] (take k fs) = ?vvs1 \<and> ?vvs1 = map gso [0..<k] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]

goal (2 subgoals):
 1. gram_schmidt n us = vs
 2. vs = map gso [0..<k]
[PROOF STEP]
with assms main_def
[PROOF STATE]
proof (chain)
picking this:
length fs = m
k \<le> m
m \<le> n
set us \<subseteq> carrier_vec n
snd (main us) = vs
us = take k fs
set fs \<subseteq> carrier_vec n
main ?us = sub2_wit [] ?us
\<lbrakk>?vvs1 = snd (sub2_wit [] (take k fs)); ?wits1 = fst (sub2_wit [] (take k fs))\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n [] (take k fs) = ?vvs1 \<and> ?vvs1 = map gso [0..<k] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]
[PROOF STEP]
show "gram_schmidt n us = vs" "vs = map gso [0..<k]"
[PROOF STATE]
proof (prove)
using this:
length fs = m
k \<le> m
m \<le> n
set us \<subseteq> carrier_vec n
snd (main us) = vs
us = take k fs
set fs \<subseteq> carrier_vec n
main ?us = sub2_wit [] ?us
\<lbrakk>?vvs1 = snd (sub2_wit [] (take k fs)); ?wits1 = fst (sub2_wit [] (take k fs))\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n [] (take k fs) = ?vvs1 \<and> ?vvs1 = map gso [0..<k] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]

goal (1 subgoal):
 1. gram_schmidt n us = vs &&& vs = map gso [0..<k]
[PROOF STEP]
unfolding gram_schmidt_code
[PROOF STATE]
proof (prove)
using this:
length fs = m
k \<le> m
m \<le> n
set us \<subseteq> carrier_vec n
snd (main us) = vs
us = take k fs
set fs \<subseteq> carrier_vec n
main ?us = sub2_wit [] ?us
\<lbrakk>?vvs1 = snd (sub2_wit [] (take k fs)); ?wits1 = fst (sub2_wit [] (take k fs))\<rbrakk> \<Longrightarrow> gram_schmidt_sub2 n [] (take k fs) = ?vvs1 \<and> ?vvs1 = map gso [0..<k] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<k]

goal (1 subgoal):
 1. gram_schmidt_sub2 n [] us = vs &&& vs = map gso [0..<k]
[PROOF STEP]
by (auto simp add: main_def case_prod_beta')
[PROOF STATE]
proof (state)
this:
gram_schmidt n us = vs
vs = map gso [0..<k]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjuster_wit_small:
  "(adjuster_wit v a xs) = (x1,x2)
  \<longleftrightarrow> (fst (adjuster_wit v a xs) = x1 \<and> x2 = adjuster n a xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (adjuster_wit v a xs = (x1, x2)) = (fst (adjuster_wit v a xs) = x1 \<and> x2 = adjuster n a xs)
[PROOF STEP]
proof(induct xs arbitrary: a v x1 x2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a v x1 x2. (adjuster_wit v a [] = (x1, x2)) = (fst (adjuster_wit v a []) = x1 \<and> x2 = adjuster n a [])
 2. \<And>a xs aa v x1 x2. (\<And>a v x1 x2. (adjuster_wit v a xs = (x1, x2)) = (fst (adjuster_wit v a xs) = x1 \<and> x2 = adjuster n a xs)) \<Longrightarrow> (adjuster_wit v aa (a # xs) = (x1, x2)) = (fst (adjuster_wit v aa (a # xs)) = x1 \<and> x2 = adjuster n aa (a # xs))
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
(adjuster_wit ?v1 ?a1 xs = (?x1.1, ?x2.1)) = (fst (adjuster_wit ?v1 ?a1 xs) = ?x1.1 \<and> ?x2.1 = adjuster n ?a1 xs)

goal (2 subgoals):
 1. \<And>a v x1 x2. (adjuster_wit v a [] = (x1, x2)) = (fst (adjuster_wit v a []) = x1 \<and> x2 = adjuster n a [])
 2. \<And>a xs aa v x1 x2. (\<And>a v x1 x2. (adjuster_wit v a xs = (x1, x2)) = (fst (adjuster_wit v a xs) = x1 \<and> x2 = adjuster n a xs)) \<Longrightarrow> (adjuster_wit v aa (a # xs) = (x1, x2)) = (fst (adjuster_wit v aa (a # xs)) = x1 \<and> x2 = adjuster n aa (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(adjuster_wit ?v1 ?a1 xs = (?x1.1, ?x2.1)) = (fst (adjuster_wit ?v1 ?a1 xs) = ?x1.1 \<and> ?x2.1 = adjuster n ?a1 xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(adjuster_wit ?v1 ?a1 xs = (?x1.1, ?x2.1)) = (fst (adjuster_wit ?v1 ?a1 xs) = ?x1.1 \<and> ?x2.1 = adjuster n ?a1 xs)

goal (1 subgoal):
 1. (adjuster_wit v a (aa__ # xs) = (x1, x2)) = (fst (adjuster_wit v a (aa__ # xs)) = x1 \<and> x2 = adjuster n a (aa__ # xs))
[PROOF STEP]
by (auto simp:Let_def sq_norm_vec_as_cscalar_prod split:prod.splits)
[PROOF STATE]
proof (state)
this:
(adjuster_wit v a (aa__ # xs) = (x1, x2)) = (fst (adjuster_wit v a (aa__ # xs)) = x1 \<and> x2 = adjuster n a (aa__ # xs))

goal (1 subgoal):
 1. \<And>a v x1 x2. (adjuster_wit v a [] = (x1, x2)) = (fst (adjuster_wit v a []) = x1 \<and> x2 = adjuster n a [])
[PROOF STEP]
qed auto


[STATEMENT]
lemma sub2: "rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)
[PROOF STEP]
have "sub2_wit xs us = (x1, x2) \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs us)"
    for x1 x2 xs us
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub2_wit xs us = (x1, x2) \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs us)
[PROOF STEP]
apply(induct us arbitrary: xs x1 x2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>xs x1 x2. sub2_wit xs [] = (x1, x2) \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs [])
 2. \<And>a us xs x1 x2. \<lbrakk>\<And>xs x1 x2. sub2_wit xs us = (x1, x2) \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs us); sub2_wit xs (a # us) = (x1, x2)\<rbrakk> \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs (a # us))
[PROOF STEP]
by (auto simp:Let_def rev_unsimp adjuster_wit_small split:prod.splits simp del:rev.simps)
[PROOF STATE]
proof (state)
this:
sub2_wit ?xs1 ?us1 = (?x1.1, ?x2.1) \<Longrightarrow> rev ?xs1 @ ?x2.1 = rev (gram_schmidt_sub n ?xs1 ?us1)

goal (1 subgoal):
 1. rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sub2_wit ?xs1 ?us1 = (?x1.1, ?x2.1) \<Longrightarrow> rev ?xs1 @ ?x2.1 = rev (gram_schmidt_sub n ?xs1 ?us1)

goal (1 subgoal):
 1. rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)
[PROOF STEP]
apply (cases us)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>xs us x1 x2. sub2_wit xs us = (x1, x2) \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs us); us = []\<rbrakk> \<Longrightarrow> rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)
 2. \<And>a list. \<lbrakk>\<And>xs us x1 x2. sub2_wit xs us = (x1, x2) \<Longrightarrow> rev xs @ x2 = rev (gram_schmidt_sub n xs us); us = a # list\<rbrakk> \<Longrightarrow> rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)
[PROOF STEP]
by (auto simp:Let_def rev_unsimp adjuster_wit_small split:prod.splits simp del:rev.simps)
[PROOF STATE]
proof (state)
this:
rev xs @ snd (sub2_wit xs us) = rev (gram_schmidt_sub n xs us)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gso_connect: "snd (main us) = gram_schmidt n us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (main us) = gram_schmidt n us
[PROOF STEP]
unfolding main_def gram_schmidt_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (sub2_wit [] us) = rev (gram_schmidt_sub n [] us)
[PROOF STEP]
using sub2[of Nil us]
[PROOF STATE]
proof (prove)
using this:
rev [] @ snd (sub2_wit [] us) = rev (gram_schmidt_sub n [] us)

goal (1 subgoal):
 1. snd (sub2_wit [] us) = rev (gram_schmidt_sub n [] us)
[PROOF STEP]
by auto


[STATEMENT]
lemma f_carrier[simp]: "i < m \<Longrightarrow> fs ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n
[PROOF STEP]
using fs_carrier
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
{fs ! i |i. i < length fs} \<subseteq> carrier_vec n

goal (1 subgoal):
 1. i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n
[PROOF STEP]
by force


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

goal (1 subgoal):
 1. i < length fs \<Longrightarrow> gso i \<in> carrier_vec n
[PROOF STEP]
by auto


[STATEMENT]
lemma gso_dim[simp]: "i < m \<Longrightarrow> dim_vec (gso i) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length fs \<Longrightarrow> dim_vec (gso i) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma f_dim[simp]: "i < m \<Longrightarrow> dim_vec (fs ! i) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
[PROOF STEP]
by auto


[STATEMENT]
lemma fs0_gso0: "0 < m \<Longrightarrow> fs ! 0 = gso 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length fs \<Longrightarrow> fs ! 0 = gso 0
[PROOF STEP]
unfolding gso.simps[of 0]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < length fs \<Longrightarrow> fs ! 0 = fs ! 0 + M.sumlist (map (\<lambda>j. - \<mu> 0 j \<cdot>\<^sub>v gso j) [0..<0])
[PROOF STEP]
using f_dim[of 0]
[PROOF STATE]
proof (prove)
using this:
0 < length fs \<Longrightarrow> dim_vec (fs ! 0) = n

goal (1 subgoal):
 1. 0 < length fs \<Longrightarrow> fs ! 0 = fs ! 0 + M.sumlist (map (\<lambda>j. - \<mu> 0 j \<cdot>\<^sub>v gso j) [0..<0])
[PROOF STEP]
by (cases fs, auto simp add: upt_rec)


[STATEMENT]
lemma fs_by_gso_def :
assumes i: "i < m"
shows "fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])" (is "_ = _ + ?sum")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
have a: "M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
[PROOF STEP]
using gso_carrier i
[PROOF STATE]
proof (prove)
using this:
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
[PROOF STEP]
by (intro M.sumlist_carrier, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
hence "dim_vec (M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i])) = n"
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i])) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i])) = n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
note a this
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
dim_vec (M.sumlist (map (\<lambda>ja. f ja \<cdot>\<^sub>v gso ja) [0..<i])) = n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
dim_vec (M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i])) = n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
note sum_carrier = this
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
dim_vec (M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i])) = n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
note [simp] = sum_carrier(2)
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i])) = n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
have f: "fs ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i \<in> carrier_vec n
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. fs ! i \<in> carrier_vec n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i \<in> carrier_vec n

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
have "gso i + ?sum = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + ?sum "
    (is "_ = _ + ?minus_sum + _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
unfolding gso.simps[of i]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
have "?minus_sum = - ?sum"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
using gso_carrier i sum_carrier
[PROOF STATE]
proof (prove)
using this:
?i < length fs \<Longrightarrow> gso ?i \<in> carrier_vec n
i < length fs
M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
dim_vec (M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i])) = n

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
by (intro eq_vecI, auto simp: sumlist_nth sum_negf)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) [0..<i]) = - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
have "fs ! i + (-?sum) + ?sum = fs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! i + - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i
[PROOF STEP]
using sum_carrier fs_carrier f
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i]) \<in> carrier_vec n
dim_vec (M.sumlist (map (\<lambda>ja. ?f3 ja \<cdot>\<^sub>v gso ja) [0..<i])) = n
set fs \<subseteq> carrier_vec n
fs ! i \<in> carrier_vec n

goal (1 subgoal):
 1. fs ! i + - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fs ! i + - M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i]) = fs ! i

goal (1 subgoal):
 1. fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fs ! i = gso i + M.sumlist (map (\<lambda>ja. \<mu> i ja \<cdot>\<^sub>v gso ja) [0..<i])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma main_connect:
  assumes "m \<le> n"
  shows "gram_schmidt n fs = map gso [0..<m]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt n fs = map gso [0..<length fs]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gram_schmidt n fs = map gso [0..<length fs]
[PROOF STEP]
obtain vs where snd_main: "snd (main fs) = vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>vs. snd (main fs) = vs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
snd (main fs) = vs

goal (1 subgoal):
 1. gram_schmidt n fs = map gso [0..<length fs]
[PROOF STEP]
have "gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs]
        \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]"
    if "wits = fst (sub2_wit [] fs)" for wits
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
using assms that fs_carrier
[PROOF STATE]
proof (prove)
using this:
length fs \<le> n
wits = fst (sub2_wit [] fs)
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> wits = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
by (intro  sub2_wit) (auto simp add: map_nth)
[PROOF STATE]
proof (state)
this:
?wits1 = fst (sub2_wit [] fs) \<Longrightarrow> gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]

goal (1 subgoal):
 1. gram_schmidt n fs = map gso [0..<length fs]
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?wits1 = fst (sub2_wit [] fs) \<Longrightarrow> gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
[PROOF STEP]
have "gram_schmidt_sub2 n [] fs = vs \<and> vs = map gso [0..<m]"
[PROOF STATE]
proof (prove)
using this:
?wits1 = fst (sub2_wit [] fs) \<Longrightarrow> gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]

goal (1 subgoal):
 1. gram_schmidt_sub2 n [] fs = vs \<and> vs = map gso [0..<length fs]
[PROOF STEP]
using snd_main main_def
[PROOF STATE]
proof (prove)
using this:
?wits1 = fst (sub2_wit [] fs) \<Longrightarrow> gram_schmidt_sub2 n [] fs = snd (sub2_wit [] fs) \<and> snd (sub2_wit [] fs) = map gso [0..<length fs] \<and> ?wits1 = map (\<lambda>i. map (\<mu> i) [0..<i]) [0..<length fs]
snd (main fs) = vs
main ?us = sub2_wit [] ?us

goal (1 subgoal):
 1. gram_schmidt_sub2 n [] fs = vs \<and> vs = map gso [0..<length fs]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gram_schmidt_sub2 n [] fs = vs \<and> vs = map gso [0..<length fs]

goal (1 subgoal):
 1. gram_schmidt n fs = map gso [0..<length fs]
[PROOF STEP]
thus "gram_schmidt n fs = map gso [0..<m]"
[PROOF STATE]
proof (prove)
using this:
gram_schmidt_sub2 n [] fs = vs \<and> vs = map gso [0..<length fs]

goal (1 subgoal):
 1. gram_schmidt n fs = map gso [0..<length fs]
[PROOF STEP]
by (auto simp: gram_schmidt_code)
[PROOF STATE]
proof (state)
this:
gram_schmidt n fs = map gso [0..<length fs]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma reduced_gso_E: "weakly_reduced \<alpha> k \<Longrightarrow> k \<le> m \<Longrightarrow> Suc i < k \<Longrightarrow>
  sq_norm (gso i) \<le> \<alpha> * sq_norm (gso (Suc i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>weakly_reduced \<alpha> k; k \<le> length fs; Suc i < k\<rbrakk> \<Longrightarrow> \<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
unfolding weakly_reduced_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i. Suc i < k \<longrightarrow> \<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2; k \<le> length fs; Suc i < k\<rbrakk> \<Longrightarrow> \<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
by auto


[STATEMENT]
lemma FF_dim[simp]: "dim_row FF = m" "dim_col FF = n" "FF \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_rows n fs) = length fs &&& dim_col (mat_of_rows n fs) = n &&& mat_of_rows n fs \<in> carrier_mat (length fs) n
[PROOF STEP]
unfolding mat_of_rows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat (length fs) n (\<lambda>(i, y). fs ! i $ y)) = length fs &&& dim_col (mat (length fs) n (\<lambda>(i, y). fs ! i $ y)) = n &&& mat (length fs) n (\<lambda>(i, y). fs ! i $ y) \<in> carrier_mat (length fs) n
[PROOF STEP]
by (auto)


[STATEMENT]
lemma Fs_dim[simp]: "dim_row Fs = m" "dim_col Fs = n" "Fs \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat_of_rows n (map gso [0..<length fs])) = length fs &&& dim_col (mat_of_rows n (map gso [0..<length fs])) = n &&& mat_of_rows n (map gso [0..<length fs]) \<in> carrier_mat (length fs) n
[PROOF STEP]
unfolding mat_of_rows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat (length (map gso [0..<length fs])) n (\<lambda>(i, y). map gso [0..<length fs] ! i $ y)) = length fs &&& dim_col (mat (length (map gso [0..<length fs])) n (\<lambda>(i, y). map gso [0..<length fs] ! i $ y)) = n &&& mat (length (map gso [0..<length fs])) n (\<lambda>(i, y). map gso [0..<length fs] ! i $ y) \<in> carrier_mat (length fs) n
[PROOF STEP]
by (auto simp: main_connect)


[STATEMENT]
lemma M_dim[simp]: "dim_row (M m) = m" "dim_col (M m) = m" "(M m) \<in> carrier_mat m m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (M (length fs)) = length fs &&& dim_col (M (length fs)) = length fs &&& M (length fs) \<in> carrier_mat (length fs) (length fs)
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat (length fs) (length fs) (\<lambda>(x, y). \<mu> x y)) = length fs &&& dim_col (mat (length fs) (length fs) (\<lambda>(x, y). \<mu> x y)) = length fs &&& mat (length fs) (length fs) (\<lambda>(x, y). \<mu> x y) \<in> carrier_mat (length fs) (length fs)
[PROOF STEP]
by auto


[STATEMENT]
lemma FF_index[simp]: "i < m \<Longrightarrow> j < n \<Longrightarrow> FF $$ (i,j) = fs ! i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = fs ! i $ j
[PROOF STEP]
unfolding mat_of_rows_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat (length fs) n (\<lambda>(i, y). fs ! i $ y) $$ (i, j) = fs ! i $ j
[PROOF STEP]
by auto


[STATEMENT]
lemma M_index[simp]:"i < m \<Longrightarrow> j < m \<Longrightarrow> (M m) $$ (i,j) = \<mu> i j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length fs; j < length fs\<rbrakk> \<Longrightarrow> M (length fs) $$ (i, j) = \<mu> i j
[PROOF STEP]
unfolding M_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length fs; j < length fs\<rbrakk> \<Longrightarrow> mat (length fs) (length fs) (\<lambda>(x, y). \<mu> x y) $$ (i, j) = \<mu> i j
[PROOF STEP]
by auto


[STATEMENT]
lemma matrix_equality: "FF = (M m) * Fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])
[PROOF STEP]
let ?P = "(M m) * Fs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])
[PROOF STEP]
have dim: "dim_row FF = m" "dim_col FF = n" "dim_row ?P = m" "dim_col ?P = n" "dim_row (M m) = m" "dim_col (M m) = m"
      "dim_row Fs = m" "dim_col Fs = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((dim_row (mat_of_rows n fs) = length fs &&& dim_col (mat_of_rows n fs) = n) &&& dim_row (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = length fs &&& dim_col (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = n) &&& (dim_row (M (length fs)) = length fs &&& dim_col (M (length fs)) = length fs) &&& dim_row (mat_of_rows n (map gso [0..<length fs])) = length fs &&& dim_col (mat_of_rows n (map gso [0..<length fs])) = n
[PROOF STEP]
by (auto simp: mat_of_rows_def mat_of_rows_list_def main_connect)
[PROOF STATE]
proof (state)
this:
dim_row (mat_of_rows n fs) = length fs
dim_col (mat_of_rows n fs) = n
dim_row (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = length fs
dim_col (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = n
dim_row (M (length fs)) = length fs
dim_col (M (length fs)) = length fs
dim_row (mat_of_rows n (map gso [0..<length fs])) = length fs
dim_col (mat_of_rows n (map gso [0..<length fs])) = n

goal (1 subgoal):
 1. mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])
[PROOF STEP]
proof (rule eq_matI; unfold dim)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
assume i: "i < m" and j: "j < n"
[PROOF STATE]
proof (state)
this:
i < length fs
j < n

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < length fs
[PROOF STEP]
have split: "[0 ..< m] = [0 ..< i] @ [i] @ [Suc i ..< m]"
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. [0..<length fs] = [0..<i] @ [i] @ [Suc i..<length fs]
[PROOF STEP]
by (metis append_Cons append_self_conv2 less_Suc_eq_le less_imp_add_positive upt_add_eq_append upt_rec zero_less_Suc)
[PROOF STATE]
proof (state)
this:
[0..<length fs] = [0..<i] @ [i] @ [Suc i..<length fs]

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
let ?prod = "\<lambda> k. \<mu> i k * gso k $ j"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have dim2: "dim_vec (col Fs j) = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (col (mat_of_rows n (map gso [0..<length fs])) j) = length fs
[PROOF STEP]
using j dim
[PROOF STATE]
proof (prove)
using this:
j < n
dim_row (mat_of_rows n fs) = length fs
dim_col (mat_of_rows n fs) = n
dim_row (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = length fs
dim_col (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = n
dim_row (M (length fs)) = length fs
dim_col (M (length fs)) = length fs
dim_row (mat_of_rows n (map gso [0..<length fs])) = length fs
dim_col (mat_of_rows n (map gso [0..<length fs])) = n

goal (1 subgoal):
 1. dim_vec (col (mat_of_rows n (map gso [0..<length fs])) j) = length fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (col (mat_of_rows n (map gso [0..<length fs])) j) = length fs

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
define idx where "idx = [0..<i]"
[PROOF STATE]
proof (state)
this:
idx = [0..<i]

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have idx: "set idx \<subseteq> {0 ..< i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set idx \<subseteq> {0..<i}
[PROOF STEP]
unfolding idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set [0..<i] \<subseteq> {0..<i}
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. set [0..<i] \<subseteq> {0..<i}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set idx \<subseteq> {0..<i}

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
let ?vec = "sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx)"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have vec: "?vec \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx) \<in> carrier_vec n
[PROOF STEP]
by (rule sumlist_carrier, insert idx gso_carrier i, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx) \<in> carrier_vec n

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
hence dimv: "dim_vec ?vec = n"
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx) \<in> carrier_vec n

goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx)) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx)) = n

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "?P $$ (i,j) = row (M m) i \<bullet> col Fs j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j
[PROOF STEP]
using dim i j
[PROOF STATE]
proof (prove)
using this:
dim_row (mat_of_rows n fs) = length fs
dim_col (mat_of_rows n fs) = n
dim_row (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = length fs
dim_col (M (length fs) * mat_of_rows n (map gso [0..<length fs])) = n
dim_row (M (length fs)) = length fs
dim_col (M (length fs)) = length fs
dim_row (mat_of_rows n (map gso [0..<length fs])) = length fs
dim_col (mat_of_rows n (map gso [0..<length fs])) = n
i < length fs
j < n

goal (1 subgoal):
 1. (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "\<dots> = (\<Sum> k = 0..<m. row (M m) i $ k * col Fs j $ k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)
[PROOF STEP]
unfolding scalar_prod_def dim2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>ia = 0..<length fs. row (M (length fs)) i $ ia * col (mat_of_rows n (map gso [0..<length fs])) j $ ia) = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
row (M (length fs)) i \<bullet> col (mat_of_rows n (map gso [0..<length fs])) j = (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "\<dots> = (\<Sum> k = 0..<m. ?prod k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k) = (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j)
[PROOF STEP]
by (rule sum.cong[OF refl], insert i j dim, auto simp: mat_of_rows_list_def mat_of_rows_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k) = (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. row (M (length fs)) i $ k * col (mat_of_rows n (map gso [0..<length fs])) j $ k) = (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "\<dots> = sum_list (map ?prod [0 ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j)
[PROOF STEP]
by (subst sum_list_distinct_conv_sum_set, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k = 0..<length fs. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "\<dots> = sum_list (map ?prod idx) + ?prod i + sum_list (map ?prod [Suc i ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j) + \<mu> i i * gso i $ j + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)
[PROOF STEP]
unfolding split idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[0..<i] @ [i] @ [Suc i..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>[0..<i]. \<mu> i k * gso k $ j) + \<mu> i i * gso i $ j + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j) + \<mu> i i * gso i $ j + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[0..<length fs]. \<mu> i k * gso k $ j) = (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j) + \<mu> i i * gso i $ j + (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "?prod i = gso i $ j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<mu> i i * gso i $ j = gso i $ j
[PROOF STEP]
unfolding \<mu>.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if i < i then fs ! i \<bullet> gso i / \<parallel>gso i\<parallel>\<^sup>2 else if i = i then 1::'a else (0::'a)) * gso i $ j = gso i $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<mu> i i * gso i $ j = gso i $ j

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<mu> i i * gso i $ j = gso i $ j

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "\<dots> = fs ! i $ j + sum_list (map (\<lambda>k. - \<mu> i k * gso k $ j) idx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso i $ j = fs ! i $ j + (\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j)
[PROOF STEP]
unfolding gso.simps[of i] idx_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fs ! i + M.sumlist (map (\<lambda>j. - \<mu> i j \<cdot>\<^sub>v gso j) idx)) $ j = fs ! i $ j + (\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j)
[PROOF STEP]
by (subst index_add_vec, unfold dimv, rule j, subst sumlist_vec_index[OF _ j], insert idx gso_carrier i j,
      auto simp: o_def intro!: arg_cong[OF map_cong])
[PROOF STATE]
proof (state)
this:
gso i $ j = fs ! i $ j + (\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso i $ j = fs ! i $ j + (\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "sum_list (map (\<lambda>k. - \<mu> i k * gso k $ j) idx) = - sum_list (map (\<lambda>k. \<mu> i k * gso k $ j) idx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j) = - (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j)
[PROOF STEP]
by (induct idx, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j) = - (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>idx. - \<mu> i k * gso k $ j) = - (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
have "sum_list (map ?prod [Suc i ..< m]) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j) = (0::'a)
[PROOF STEP]
by (rule sum_list_neutral, auto simp: \<mu>.simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<leftarrow>[Suc i..<length fs]. \<mu> i k * gso k $ j) = (0::'a)

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j) + (fs ! i $ j + - (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j)) + (0::'a)
[PROOF STEP]
have "?P $$ (i,j) = fs ! i $ j"
[PROOF STATE]
proof (prove)
using this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j) + (fs ! i $ j + - (\<Sum>k\<leftarrow>idx. \<mu> i k * gso k $ j)) + (0::'a)

goal (1 subgoal):
 1. (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = fs ! i $ j
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = fs ! i $ j

goal (3 subgoals):
 1. \<And>i j. \<lbrakk>i < length fs; j < n\<rbrakk> \<Longrightarrow> mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
 2. length fs = length fs
 3. n = n
[PROOF STEP]
with FF_index[OF i j]
[PROOF STATE]
proof (chain)
picking this:
mat_of_rows n fs $$ (i, j) = fs ! i $ j
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = fs ! i $ j
[PROOF STEP]
show "FF $$ (i,j) = ?P $$ (i,j)"
[PROOF STATE]
proof (prove)
using this:
mat_of_rows n fs $$ (i, j) = fs ! i $ j
(M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j) = fs ! i $ j

goal (1 subgoal):
 1. mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mat_of_rows n fs $$ (i, j) = (M (length fs) * mat_of_rows n (map gso [0..<length fs])) $$ (i, j)

goal (2 subgoals):
 1. length fs = length fs
 2. n = n
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
mat_of_rows n fs = M (length fs) * mat_of_rows n (map gso [0..<length fs])

goal:
No subgoals!
[PROOF STEP]
qed