[STATEMENT]
lemma perron_frobenius_irreducible: fixes A :: "real Matrix.mat" and cA :: "complex Matrix.mat"
  assumes A: "A \<in> carrier_mat n n" and n: "n \<noteq> 0" and nonneg: "nonneg_mat A"
    and irr: "irreducible_mat A"
    and cA: "cA = map_mat of_real A"
    and sr: "sr = Spectral_Radius.spectral_radius cA"
  shows
    "eigenvalue A sr"
    "order sr (char_poly A) = 1"
    "0 < sr"
    "eigenvalue cA \<alpha> \<Longrightarrow> cmod \<alpha> \<le> sr"
    "eigenvalue cA \<alpha> \<Longrightarrow> cmod \<alpha> = sr \<Longrightarrow> order \<alpha> (char_poly cA) = 1"
    "\<exists> k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and>
        (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eigenvalue A sr &&& order sr (char_poly A) = 1 &&& 0 < sr) &&& (eigenvalue cA \<alpha> \<Longrightarrow> cmod \<alpha> \<le> sr) &&& (\<lbrakk>eigenvalue cA \<alpha>; cmod \<alpha> = sr\<rbrakk> \<Longrightarrow> order \<alpha> (char_poly cA) = 1) &&& \<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)
[PROOF STEP]
proof (atomize (full), goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. (eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))
[PROOF STEP]
from nonneg irr
[PROOF STATE]
proof (chain)
picking this:
nonneg_mat A
irreducible_mat A
[PROOF STEP]
have irr: "nonneg_irreducible_mat A"
[PROOF STATE]
proof (prove)
using this:
nonneg_mat A
irreducible_mat A

goal (1 subgoal):
 1. nonneg_irreducible_mat A
[PROOF STEP]
unfolding nonneg_irreducible_mat_def
[PROOF STATE]
proof (prove)
using this:
nonneg_mat A
irreducible_mat A

goal (1 subgoal):
 1. nonneg_mat A \<and> irreducible_mat A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nonneg_irreducible_mat A

goal (1 subgoal):
 1. (eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))
[PROOF STEP]
note main = perron_frobenius.pf_main_connect[untransferred, cancel_card_constraint, OF A irr,
    folded sr cA]
[PROOF STATE]
proof (state)
this:
n \<noteq> 0 \<Longrightarrow> eigenvalue A sr
\<lbrakk>eigenvalue cA ?\<alpha>; n \<noteq> 0\<rbrakk> \<Longrightarrow> cmod ?\<alpha> \<le> sr
n \<noteq> 0 \<Longrightarrow> order sr (char_poly A) = 1
\<lbrakk>eigenvalue cA ?\<alpha>; cmod ?\<alpha> = sr; n \<noteq> 0\<rbrakk> \<Longrightarrow> order ?\<alpha> (char_poly cA) = 1
\<lbrakk>?M = {ev. eigenvalue cA ev \<and> cmod ev = sr}; ?k = card ?M; n \<noteq> 0\<rbrakk> \<Longrightarrow> ?k \<noteq> 0
\<lbrakk>?M = {ev. eigenvalue cA ev \<and> cmod ev = sr}; ?k = card ?M; n \<noteq> 0\<rbrakk> \<Longrightarrow> ?k \<le> n
\<lbrakk>?M = {ev. eigenvalue cA ev \<and> cmod ev = sr}; ?k = card ?M; n \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>f. char_poly A = (monom 1 ?k - [:sr ^ ?k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)
n \<noteq> 0 \<Longrightarrow> 0 < sr

goal (1 subgoal):
 1. (eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))
[PROOF STEP]
from main(5,6,7)[OF refl refl n]
[PROOF STATE]
proof (chain)
picking this:
card {ev. eigenvalue cA ev \<and> cmod ev = sr} \<noteq> 0
card {ev. eigenvalue cA ev \<and> cmod ev = sr} \<le> n
\<exists>f. char_poly A = (monom 1 (card {ev. eigenvalue cA ev \<and> cmod ev = sr}) - [:sr ^ card {ev. eigenvalue cA ev \<and> cmod ev = sr}:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)
[PROOF STEP]
have "\<exists> k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and>
        (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)"
[PROOF STATE]
proof (prove)
using this:
card {ev. eigenvalue cA ev \<and> cmod ev = sr} \<noteq> 0
card {ev. eigenvalue cA ev \<and> cmod ev = sr} \<le> n
\<exists>f. char_poly A = (monom 1 (card {ev. eigenvalue cA ev \<and> cmod ev = sr}) - [:sr ^ card {ev. eigenvalue cA ev \<and> cmod ev = sr}:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)

goal (1 subgoal):
 1. \<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)

goal (1 subgoal):
 1. (eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))
[PROOF STEP]
with main(1,3,8)[OF n] main(2)[OF _ n] main(4)[OF _ _ n]
[PROOF STATE]
proof (chain)
picking this:
eigenvalue A sr
order sr (char_poly A) = 1
0 < sr
eigenvalue cA ?\<alpha> \<Longrightarrow> cmod ?\<alpha> \<le> sr
\<lbrakk>eigenvalue cA ?\<alpha>; cmod ?\<alpha> = sr\<rbrakk> \<Longrightarrow> order ?\<alpha> (char_poly cA) = 1
\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
eigenvalue A sr
order sr (char_poly A) = 1
0 < sr
eigenvalue cA ?\<alpha> \<Longrightarrow> cmod ?\<alpha> \<le> sr
\<lbrakk>eigenvalue cA ?\<alpha>; cmod ?\<alpha> = sr\<rbrakk> \<Longrightarrow> order ?\<alpha> (char_poly cA) = 1
\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr)

goal (1 subgoal):
 1. (eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(eigenvalue A sr \<and> order sr (char_poly A) = 1 \<and> 0 < sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> \<le> sr) \<and> (eigenvalue cA \<alpha> \<longrightarrow> cmod \<alpha> = sr \<longrightarrow> order \<alpha> (char_poly cA) = 1) \<and> (\<exists>k f. k \<noteq> 0 \<and> k \<le> n \<and> char_poly A = (monom 1 k - [:sr ^ k:]) * f \<and> (\<forall>x. poly (map_poly complex_of_real f) x = 0 \<longrightarrow> cmod x < sr))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dims_matricize:
"dim_row (matricize rmodes T) = prod_list (nths (Tensor.dims T) rmodes)"
"dim_col (matricize rmodes T) = prod_list (nths (Tensor.dims T) (-rmodes))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (matricize rmodes T) = prod_list (nths (dims T) rmodes) &&& dim_col (matricize rmodes T) = prod_list (nths (dims T) (- rmodes))
[PROOF STEP]
unfolding matricize_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row (mat (prod_list (nths (dims T) rmodes)) (prod_list (nths (dims T) (- rmodes))) (\<lambda>(r, c). lookup T (weave rmodes (digit_encode (nths (dims T) rmodes) r) (digit_encode (nths (dims T) (- rmodes)) c)))) = prod_list (nths (dims T) rmodes) &&& dim_col (mat (prod_list (nths (dims T) rmodes)) (prod_list (nths (dims T) (- rmodes))) (\<lambda>(r, c). lookup T (weave rmodes (digit_encode (nths (dims T) rmodes) r) (digit_encode (nths (dims T) (- rmodes)) c)))) = prod_list (nths (dims T) (- rmodes))
[PROOF STEP]
using dim_row_mat
[PROOF STATE]
proof (prove)
using this:
dim_row (mat ?nr ?nc ?f) = ?nr
dim_row (mat\<^sub>r ?nr ?nc ?g) = ?nr

goal (1 subgoal):
 1. dim_row (mat (prod_list (nths (dims T) rmodes)) (prod_list (nths (dims T) (- rmodes))) (\<lambda>(r, c). lookup T (weave rmodes (digit_encode (nths (dims T) rmodes) r) (digit_encode (nths (dims T) (- rmodes)) c)))) = prod_list (nths (dims T) rmodes) &&& dim_col (mat (prod_list (nths (dims T) rmodes)) (prod_list (nths (dims T) (- rmodes))) (\<lambda>(r, c). lookup T (weave rmodes (digit_encode (nths (dims T) rmodes) r) (digit_encode (nths (dims T) (- rmodes)) c)))) = prod_list (nths (dims T) (- rmodes))
[PROOF STEP]
by simp_all


[STATEMENT]
lemma g_bnd_swap:
  assumes i: "i < m" "i \<noteq> 0"
  and Linv: "LLL_invariant_weak fs"
  and mu_F1_i: "\<bar>\<mu> fs i (i-1)\<bar> \<le> 1 / 2"
  and cond: "sq_norm (gso fs (i - 1)) > \<alpha> * sq_norm (gso fs i)"
  and fs'_def: "fs' = fs[i := fs ! (i - 1), i - 1 := fs ! i]"
  and g_bnd: "g_bnd B fs"
shows "g_bnd B fs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
note inv = LLL_inv_wD[OF Linv]
[PROOF STATE]
proof (state)
this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs)
length (map of_int_hom.vec_hom fs) = m
set fs \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?i \<in> Rn
length fs = m
lattice_of fs = L

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have choice: "fs' ! k = fs ! k \<or> fs' ! k = fs ! i \<or> fs' ! k = fs ! (i - 1)" for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs' ! k = fs ! k \<or> fs' ! k = fs ! i \<or> fs' ! k = fs ! (i - 1)
[PROOF STEP]
unfolding fs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs[i := fs ! (i - 1), i - 1 := fs ! i] ! k = fs ! k \<or> fs[i := fs ! (i - 1), i - 1 := fs ! i] ! k = fs ! i \<or> fs[i := fs ! (i - 1), i - 1 := fs ! i] ! k = fs ! (i - 1)
[PROOF STEP]
using i inv(6)
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0
length fs = m

goal (1 subgoal):
 1. fs[i := fs ! (i - 1), i - 1 := fs ! i] ! k = fs ! k \<or> fs[i := fs ! (i - 1), i - 1 := fs ! i] ! k = fs ! i \<or> fs[i := fs ! (i - 1), i - 1 := fs ! i] ! k = fs ! (i - 1)
[PROOF STEP]
by (cases "k = i"; cases "k = i - 1", auto)
[PROOF STATE]
proof (state)
this:
fs' ! ?k1 = fs ! ?k1 \<or> fs' ! ?k1 = fs ! i \<or> fs' ! ?k1 = fs ! (i - 1)

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?g1 = "\<lambda> i. gso fs i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?g2 = "\<lambda> i. gso fs' i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?n1 = "\<lambda> i. sq_norm (?g1 i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?n2 = "\<lambda> i. sq_norm (?g2 i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
from g_bnd[unfolded g_bnd_def]
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<m. \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have short: "\<And> k. k < m \<Longrightarrow> ?n1 k \<le> B"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<m. \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. \<And>k. k < m \<Longrightarrow> \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?k1 < m \<Longrightarrow> \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?k1\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
from short[of "i - 1"] i
[PROOF STATE]
proof (chain)
picking this:
i - 1 < m \<Longrightarrow> \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 \<le> B
i < m
i \<noteq> 0
[PROOF STEP]
have short_im1: "?n1 (i - 1) \<le> B"
[PROOF STATE]
proof (prove)
using this:
i - 1 < m \<Longrightarrow> \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 \<le> B
i < m
i \<noteq> 0

goal (1 subgoal):
 1. \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
note swap = basis_reduction_swap_main[OF Linv disjI2[OF mu_F1_i] i cond fs'_def]
[PROOF STATE]
proof (state)
this:
LLL_invariant_weak fs'
LLL_invariant False i fs \<Longrightarrow> LLL_invariant False (i - 1) fs'
LLL_measure (i - 1) fs' < LLL_measure i fs
?k < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?k = (if ?k = i - 1 then gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i + gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) \<cdot>\<^sub>v gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1) else if ?k = i then gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1) - map of_int_hom.vec_hom fs ! (i - 1) \<bullet> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1) / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 \<cdot>\<^sub>v gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1) else gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?k)
?k < m \<Longrightarrow> \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?k\<parallel>\<^sup>2 = (if ?k = i - 1 then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 + gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) * gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) * \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 else if ?k = i then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 * \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 else \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?k\<parallel>\<^sup>2)
\<lbrakk>?ii < m; ?j < ?ii\<rbrakk> \<Longrightarrow> gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs') ?ii ?j = (if ?ii = i - 1 then gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i ?j else if ?ii = i then if ?j = i - 1 then gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) * \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 else gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) (i - 1) ?j else if i < ?ii \<and> ?j = i then gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) ?ii (i - 1) - gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) * gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) ?ii i else if i < ?ii \<and> ?j = i - 1 then gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) ?ii (i - 1) * gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs') i (i - 1) + gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) ?ii i * \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 else gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) ?ii ?j)
?ii \<le> m \<Longrightarrow> rat_of_int (d fs' ?ii) = (if ?ii = i then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 * rat_of_int (d fs i) else rat_of_int (d fs ?ii))

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
note updates = swap(4,5)
[PROOF STATE]
proof (state)
this:
?k < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?k = (if ?k = i - 1 then gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i + gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) \<cdot>\<^sub>v gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1) else if ?k = i then gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1) - map of_int_hom.vec_hom fs ! (i - 1) \<bullet> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1) / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 \<cdot>\<^sub>v gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1) else gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?k)
?k < m \<Longrightarrow> \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?k\<parallel>\<^sup>2 = (if ?k = i - 1 then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 + gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) * gram_schmidt_fs.\<mu> n (map of_int_hom.vec_hom fs) i (i - 1) * \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 else if ?k = i then \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) i\<parallel>\<^sup>2 * \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) (i - 1)\<parallel>\<^sup>2 / \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') (i - 1)\<parallel>\<^sup>2 else \<parallel>gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?k\<parallel>\<^sup>2)

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
note Linv' = swap(1)
[PROOF STATE]
proof (state)
this:
LLL_invariant_weak fs'

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
note inv' = LLL_inv_wD[OF Linv']
[PROOF STATE]
proof (state)
this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs')
length (map of_int_hom.vec_hom fs') = m
set fs' \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs' ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs') ?i \<in> Rn
length fs' = m
lattice_of fs' = L

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
note inv = LLL_inv_wD[OF Linv]
[PROOF STATE]
proof (state)
this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs)
length (map of_int_hom.vec_hom fs) = m
set fs \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gram_schmidt_fs.gso n (map of_int_hom.vec_hom fs) ?i \<in> Rn
length fs = m
lattice_of fs = L

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
interpret gs1: gram_schmidt_fs_int n "RAT fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_fs_int n (map of_int_hom.vec_hom fs)
[PROOF STEP]
by (standard) (use inv gs.lin_indpt_list_def in \<open>auto simp add: vec_hom_Ints\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
interpret gs2: gram_schmidt_fs_int n "RAT fs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gram_schmidt_fs_int n (map of_int_hom.vec_hom fs')
[PROOF STEP]
by (standard) (use inv' gs.lin_indpt_list_def in \<open>auto simp add: vec_hom_Ints\<close>)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?mu1 = "\<mu> fs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?mu2 = "\<mu> fs'"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
let ?mu = "?mu1 i (i - 1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have mu: "abs ?mu \<le> 1/2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>gs1.\<mu> i (i - 1)\<bar> \<le> 1 / 2
[PROOF STEP]
using mu_F1_i
[PROOF STATE]
proof (prove)
using this:
\<bar>gs1.\<mu> i (i - 1)\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. \<bar>gs1.\<mu> i (i - 1)\<bar> \<le> 1 / 2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<bar>gs1.\<mu> i (i - 1)\<bar> \<le> 1 / 2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "?n2 (i - 1) = ?n1 i + ?mu * ?mu * ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 = \<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by (subst updates(2), insert i, auto)
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 = \<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 = \<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "\<dots> = inverse \<alpha> * (\<alpha> * ?n1 i) + (?mu * ?mu) * ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
using \<alpha>
[PROOF STATE]
proof (prove)
using this:
4 / 3 \<le> \<alpha>

goal (1 subgoal):
 1. \<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso i\<parallel>\<^sup>2 + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "\<dots> \<le> inverse \<alpha> * ?n1 (i - 1) + (abs ?mu * abs ?mu) * ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> inverse \<alpha> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by (rule add_mono[OF mult_left_mono], insert cond \<alpha>, auto)
[PROOF STATE]
proof (state)
this:
inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> inverse \<alpha> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse \<alpha> * (\<alpha> * \<parallel>gs1.gso i\<parallel>\<^sup>2) + gs1.\<mu> i (i - 1) * gs1.\<mu> i (i - 1) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> inverse \<alpha> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "\<dots> = (inverse \<alpha> + abs ?mu * abs ?mu) * ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse \<alpha> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = (inverse \<alpha> + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar>) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
inverse \<alpha> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = (inverse \<alpha> + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar>) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse \<alpha> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar> * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 = (inverse \<alpha> + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar>) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "\<dots> \<le> (inverse \<alpha> + (1/2) * (1/2)) * ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inverse \<alpha> + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar>) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> (inverse \<alpha> + 1 / 2 * (1 / 2)) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by (rule mult_right_mono[OF add_left_mono[OF mult_mono]], insert mu, auto)
[PROOF STATE]
proof (state)
this:
(inverse \<alpha> + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar>) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> (inverse \<alpha> + 1 / 2 * (1 / 2)) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(inverse \<alpha> + \<bar>gs1.\<mu> i (i - 1)\<bar> * \<bar>gs1.\<mu> i (i - 1)\<bar>) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> (inverse \<alpha> + 1 / 2 * (1 / 2)) * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "inverse \<alpha> + (1/2) * (1/2) = reduction"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse \<alpha> + 1 / 2 * (1 / 2) = reduction
[PROOF STEP]
unfolding reduction_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inverse \<alpha> + 1 / 2 * (1 / 2) = (4 + \<alpha>) / (4 * \<alpha>)
[PROOF STEP]
using \<alpha>0
[PROOF STATE]
proof (prove)
using this:
0 < \<alpha>
\<alpha> \<noteq> 0

goal (1 subgoal):
 1. inverse \<alpha> + 1 / 2 * (1 / 2) = (4 + \<alpha>) / (4 * \<alpha>)
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
inverse \<alpha> + 1 / 2 * (1 / 2) = reduction

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inverse \<alpha> + 1 / 2 * (1 / 2) = reduction

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
have "\<dots> * ?n1 (i - 1) \<le> 1 * ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduction * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> 1 * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by (rule mult_right_mono, auto simp: reduction)
[PROOF STATE]
proof (state)
this:
reduction * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> 1 * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> 1 * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have n2im1: "?n2 (i - 1) \<le> ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> 1 * \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
show "g_bnd B fs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_bnd B fs'
[PROOF STEP]
unfolding g_bnd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<m. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < m \<Longrightarrow> \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < m \<Longrightarrow> \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
assume km: "k < m"
[PROOF STATE]
proof (state)
this:
k < m

goal (1 subgoal):
 1. \<And>i. i < m \<Longrightarrow> \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
consider (ki) "k = i" | (im1) "k = i - 1" | (other) "k \<noteq> i" "k \<noteq> i-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k = i \<Longrightarrow> thesis; k = i - 1 \<Longrightarrow> thesis; \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<lbrakk>k = i \<Longrightarrow> ?thesis1; k = i - 1 \<Longrightarrow> ?thesis1; \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. \<And>i. i < m \<Longrightarrow> \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
thus "?n2 k \<le> B"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k = i \<Longrightarrow> ?thesis1; k = i - 1 \<Longrightarrow> ?thesis1; \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> ?thesis1\<rbrakk> \<Longrightarrow> ?thesis1

goal (1 subgoal):
 1. \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 3. \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
case other
[PROOF STATE]
proof (state)
this:
k \<noteq> i
k \<noteq> i - 1

goal (3 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 3. \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
from short[OF km]
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gs1.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "?n1 k \<le> B"
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs1.gso k\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. \<parallel>gs1.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso k\<parallel>\<^sup>2 \<le> B

goal (3 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 3. \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso k\<parallel>\<^sup>2 \<le> B

goal (3 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 3. \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "?n1 k = ?n2 k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs1.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso k\<parallel>\<^sup>2
[PROOF STEP]
using km other
[PROOF STATE]
proof (prove)
using this:
k < m
k \<noteq> i
k \<noteq> i - 1

goal (1 subgoal):
 1. \<parallel>gs1.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso k\<parallel>\<^sup>2
[PROOF STEP]
by (subst updates(2), auto)
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso k\<parallel>\<^sup>2

goal (3 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 3. \<lbrakk>k \<noteq> i; k \<noteq> i - 1\<rbrakk> \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
case im1
[PROOF STATE]
proof (state)
this:
k = i - 1

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "?n2 k = ?n2 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
unfolding im1
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 = \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "\<dots> \<le> ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso (i - 1)\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "\<dots> \<le> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
using short_im1
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> B

goal (2 subgoals):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
 2. k = i - 1 \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
case ki
[PROOF STATE]
proof (state)
this:
k = i

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "?n2 k = ?n2 i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso i\<parallel>\<^sup>2
[PROOF STEP]
unfolding ki
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 = \<parallel>gs2.gso i\<parallel>\<^sup>2
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 = \<parallel>gs2.gso i\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 = \<parallel>gs2.gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "\<dots> \<le> ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
let ?f1 = "\<lambda> i. RAT fs ! i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
let ?f2 = "\<lambda> i. RAT fs' ! i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
define u where "u = gs.sumlist (map (\<lambda>j. ?mu1 (i - 1) j \<cdot>\<^sub>v ?g1 j) [0..<i - 1])"
[PROOF STATE]
proof (state)
this:
u = gs.M.sumlist (map (\<lambda>j. gs1.\<mu> (i - 1) j \<cdot>\<^sub>v gs1.gso j) [0..<i - 1])

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
define U where "U = ?f1 ` {0 ..< i - 1} \<union> {?f1 i}"
[PROOF STATE]
proof (state)
this:
U = (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs ! i}

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have g2i: "?g2 i \<in> Rn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs2.gso i \<in> Rn
[PROOF STEP]
using i inv'
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0
gs.lin_indpt_list (map of_int_hom.vec_hom fs')
length (map of_int_hom.vec_hom fs') = m
set fs' \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs' ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gs2.gso ?i \<in> Rn
length fs' = m
lattice_of fs' = L

goal (1 subgoal):
 1. gs2.gso i \<in> Rn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gs2.gso i \<in> Rn

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have U: "U \<subseteq> Rn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<subseteq> Rn
[PROOF STEP]
unfolding U_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs ! i} \<subseteq> Rn
[PROOF STEP]
using inv i
[PROOF STATE]
proof (prove)
using this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs)
length (map of_int_hom.vec_hom fs) = m
set fs \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gs1.gso ?i \<in> Rn
length fs = m
lattice_of fs = L
i < m
i \<noteq> 0

goal (1 subgoal):
 1. (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs ! i} \<subseteq> Rn
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U \<subseteq> Rn

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have uU: "u \<in> gs.span U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
have im1: "i - 1 \<le> m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i - 1 \<le> m
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0

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

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
have G1: "?g1 ` {0..< i - 1} \<subseteq> Rn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs1.gso ` {0..<i - 1} \<subseteq> Rn
[PROOF STEP]
using inv(5) i
[PROOF STATE]
proof (prove)
using this:
?i < m \<Longrightarrow> gs1.gso ?i \<in> Rn
i < m
i \<noteq> 0

goal (1 subgoal):
 1. gs1.gso ` {0..<i - 1} \<subseteq> Rn
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gs1.gso ` {0..<i - 1} \<subseteq> Rn

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
have "u \<in> gs.span (?g1 ` {0 ..< i - 1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> gs.span (gs1.gso ` {0..<i - 1})
[PROOF STEP]
unfolding u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.M.sumlist (map (\<lambda>j. gs1.\<mu> (i - 1) j \<cdot>\<^sub>v gs1.gso j) [0..<i - 1]) \<in> gs.span (gs1.gso ` {0..<i - 1})
[PROOF STEP]
by (rule gs.sumlist_in_span[OF G1], unfold set_map, insert G1,
              auto intro!: gs.smult_in_span intro: gs.span_mem)
[PROOF STATE]
proof (state)
this:
u \<in> gs.span (gs1.gso ` {0..<i - 1})

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
u \<in> gs.span (gs1.gso ` {0..<i - 1})

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
have "gs.span (?g1 ` {0 ..< i - 1}) = gs.span (?f1 ` {0 ..< i - 1})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.span (gs1.gso ` {0..<i - 1}) = gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1})
[PROOF STEP]
apply(subst gs1.partial_span, insert im1 inv, unfold gs.lin_indpt_list_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i - 1 \<le> m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> i - 1 \<le> length (map of_int_hom.vec_hom fs)
 2. \<lbrakk>i - 1 \<le> m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> gs.span (set (take (i - 1) (map of_int_hom.vec_hom fs))) = gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1})
[PROOF STEP]
apply(blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i - 1 \<le> m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> gs.span (set (take (i - 1) (map of_int_hom.vec_hom fs))) = gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1})
[PROOF STEP]
apply(rule arg_cong[of _ _ gs.span])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i - 1 \<le> m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> set (take (i - 1) (map of_int_hom.vec_hom fs)) = (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1}
[PROOF STEP]
apply(subst nth_image[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i - 1 \<le> m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> i - 1 \<le> length (map of_int_hom.vec_hom fs)
 2. \<lbrakk>i - 1 \<le> m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1} = (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1}
[PROOF STEP]
by (insert i inv, auto)
[PROOF STATE]
proof (state)
this:
gs.span (gs1.gso ` {0..<i - 1}) = gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1})

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gs.span (gs1.gso ` {0..<i - 1}) = gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1})

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
have "\<dots> \<subseteq> gs.span U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1}) \<subseteq> gs.span U
[PROOF STEP]
unfolding U_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1}) \<subseteq> gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs ! i})
[PROOF STEP]
by (rule gs.span_is_monotone, auto)
[PROOF STATE]
proof (state)
this:
gs.span ((!) (map of_int_hom.vec_hom fs) ` {0..<i - 1}) \<subseteq> gs.span U

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
u \<in> gs.span U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<in> gs.span U

goal (1 subgoal):
 1. u \<in> gs.span U
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
u \<in> gs.span U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
u \<in> gs.span U

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < m
i \<noteq> 0
[PROOF STEP]
have im1: "i - 1 < m"
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0

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

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have u: "u \<in> Rn"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> Rn
[PROOF STEP]
using uU U
[PROOF STATE]
proof (prove)
using this:
u \<in> gs.span U
U \<subseteq> Rn

goal (1 subgoal):
 1. u \<in> Rn
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u \<in> Rn

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have id_u: "u + (?g1 (i - 1) - ?g2 i) = u + ?g1 (i - 1) - ?g2 i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u + (gs1.gso (i - 1) - gs2.gso i) = u + gs1.gso (i - 1) - gs2.gso i
[PROOF STEP]
using u g2i inv(5)[OF im1]
[PROOF STATE]
proof (prove)
using this:
u \<in> Rn
gs2.gso i \<in> Rn
gs1.gso (i - 1) \<in> Rn

goal (1 subgoal):
 1. u + (gs1.gso (i - 1) - gs2.gso i) = u + gs1.gso (i - 1) - gs2.gso i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
u + (gs1.gso (i - 1) - gs2.gso i) = u + gs1.gso (i - 1) - gs2.gso i

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have list_id: "[0..<Suc (i - 1)] = [0..< i - 1] @ [i - 1]"
          "map f [x] = [f x]" for f x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<Suc (i - 1)] = [0..<i - 1] @ [i - 1] &&& map f [x] = [f x]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[0..<Suc (i - 1)] = [0..<i - 1] @ [i - 1]
map ?f2 [?x2] = [?f2 ?x2]

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) ((RAT fs') ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs' ! i)
[PROOF STEP]
using i inv'
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0
gs.lin_indpt_list (map of_int_hom.vec_hom fs')
length (map of_int_hom.vec_hom fs') = m
set fs' \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs' ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gs2.gso ?i \<in> Rn
length fs' = m
lattice_of fs' = L

goal (1 subgoal):
 1. gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs' ! i)
[PROOF STEP]
unfolding gs.lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0
set (map of_int_hom.vec_hom fs') \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs') \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs'))
length (map of_int_hom.vec_hom fs') = m
set fs' \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs' ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gs2.gso ?i \<in> Rn
length fs' = m
lattice_of fs' = L

goal (1 subgoal):
 1. gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs' ! i)
[PROOF STEP]
by (intro gs2.gso_oc_projection_span(2)) auto
[PROOF STATE]
proof (state)
this:
gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs' ! i)

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs' ! i)
[PROOF STEP]
have "gs.is_oc_projection (?g2 i) (gs.span (gs2.gso ` {0 ..< i}))  (?f1 (i - 1))"
[PROOF STATE]
proof (prove)
using this:
gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs' ! i)

goal (1 subgoal):
 1. gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs ! (i - 1))
[PROOF STEP]
unfolding fs'_def
[PROOF STATE]
proof (prove)
using this:
gs.is_oc_projection (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) i) (gs.span (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) ` {0..<i})) (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i]) ! i)

goal (1 subgoal):
 1. gs.is_oc_projection (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) i) (gs.span (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) ` {0..<i})) (map of_int_hom.vec_hom fs ! (i - 1))
[PROOF STEP]
using inv(6) i
[PROOF STATE]
proof (prove)
using this:
gs.is_oc_projection (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) i) (gs.span (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) ` {0..<i})) (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i]) ! i)
length fs = m
i < m
i \<noteq> 0

goal (1 subgoal):
 1. gs.is_oc_projection (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) i) (gs.span (gram_schmidt_fs.gso n (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) ` {0..<i})) (map of_int_hom.vec_hom fs ! (i - 1))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs ! (i - 1))

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) (map of_int_hom.vec_hom fs ! (i - 1))

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "?f1 (i - 1) = u + ?g1 (i - 1) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map of_int_hom.vec_hom fs ! (i - 1) = u + gs1.gso (i - 1)
[PROOF STEP]
apply(subst gs1.fi_is_sum_of_mu_gso, insert im1 inv, unfold gs.lin_indpt_list_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i - 1 < m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> i - 1 < length (map of_int_hom.vec_hom fs)
 2. \<lbrakk>i - 1 < m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> gs.M.sumlist (map (\<lambda>j. gs1.\<mu> (i - 1) j \<cdot>\<^sub>v gs1.gso j) [0..<Suc (i - 1)]) = u + gs1.gso (i - 1)
[PROOF STEP]
apply(blast)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i - 1 < m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> gs.M.sumlist (map (\<lambda>j. gs1.\<mu> (i - 1) j \<cdot>\<^sub>v gs1.gso j) [0..<Suc (i - 1)]) = u + gs1.gso (i - 1)
[PROOF STEP]
unfolding list_id map_append u_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i - 1 < m; set (map of_int_hom.vec_hom fs) \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs) \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs)); length (map of_int_hom.vec_hom fs) = m; set fs \<subseteq> carrier_vec n; \<And>i. i < m \<Longrightarrow> fs ! i \<in> carrier_vec n; \<And>i. i < m \<Longrightarrow> gs1.gso i \<in> Rn; length fs = m; lattice_of fs = L\<rbrakk> \<Longrightarrow> gs.M.sumlist (map (\<lambda>j. gs1.\<mu> (i - 1) j \<cdot>\<^sub>v gs1.gso j) [0..<i - 1] @ [gs1.\<mu> (i - 1) (i - 1) \<cdot>\<^sub>v gs1.gso (i - 1)]) = gs.M.sumlist (map (\<lambda>j. gs1.\<mu> (i - 1) j \<cdot>\<^sub>v gs1.gso j) [0..<i - 1]) + gs1.gso (i - 1)
[PROOF STEP]
by (subst gs.M.sumlist_snoc, insert i, auto simp: gs1.\<mu>.simps intro!: inv(5))
[PROOF STATE]
proof (state)
this:
map of_int_hom.vec_hom fs ! (i - 1) = u + gs1.gso (i - 1)

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map of_int_hom.vec_hom fs ! (i - 1) = u + gs1.gso (i - 1)

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "gs.span (gs2.gso ` {0 ..< i}) = gs.span (set (take i (RAT fs')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs.span (gs2.gso ` {0..<i}) = gs.span (set (take i (map of_int_hom.vec_hom fs')))
[PROOF STEP]
using inv' \<open>i < m\<close>
[PROOF STATE]
proof (prove)
using this:
gs.lin_indpt_list (map of_int_hom.vec_hom fs')
length (map of_int_hom.vec_hom fs') = m
set fs' \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs' ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gs2.gso ?i \<in> Rn
length fs' = m
lattice_of fs' = L
i < m

goal (1 subgoal):
 1. gs.span (gs2.gso ` {0..<i}) = gs.span (set (take i (map of_int_hom.vec_hom fs')))
[PROOF STEP]
unfolding gs.lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
set (map of_int_hom.vec_hom fs') \<subseteq> Rn \<and> distinct (map of_int_hom.vec_hom fs') \<and> gs.lin_indpt (set (map of_int_hom.vec_hom fs'))
length (map of_int_hom.vec_hom fs') = m
set fs' \<subseteq> carrier_vec n
?i < m \<Longrightarrow> fs' ! ?i \<in> carrier_vec n
?i < m \<Longrightarrow> gs2.gso ?i \<in> Rn
length fs' = m
lattice_of fs' = L
i < m

goal (1 subgoal):
 1. gs.span (gs2.gso ` {0..<i}) = gs.span (set (take i (map of_int_hom.vec_hom fs')))
[PROOF STEP]
by (subst gs2.partial_span) auto
[PROOF STATE]
proof (state)
this:
gs.span (gs2.gso ` {0..<i}) = gs.span (set (take i (map of_int_hom.vec_hom fs')))

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gs.span (gs2.gso ` {0..<i}) = gs.span (set (take i (map of_int_hom.vec_hom fs')))

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "set (take i (RAT fs')) = ?f2 ` {0 ..< i}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (take i (map of_int_hom.vec_hom fs')) = (!) (map of_int_hom.vec_hom fs') ` {0..<i}
[PROOF STEP]
using inv'(6) i
[PROOF STATE]
proof (prove)
using this:
length fs' = m
i < m
i \<noteq> 0

goal (1 subgoal):
 1. set (take i (map of_int_hom.vec_hom fs')) = (!) (map of_int_hom.vec_hom fs') ` {0..<i}
[PROOF STEP]
by (subst nth_image[symmetric], auto)
[PROOF STATE]
proof (state)
this:
set (take i (map of_int_hom.vec_hom fs')) = (!) (map of_int_hom.vec_hom fs') ` {0..<i}

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
set (take i (map of_int_hom.vec_hom fs')) = (!) (map of_int_hom.vec_hom fs') ` {0..<i}

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "{0 ..< i} = {0 ..< i - 1} \<union> {(i - 1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {0..<i} = {0..<i - 1} \<union> {i - 1}
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < m
i \<noteq> 0

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

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{0..<i} = {0..<i - 1} \<union> {i - 1}

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "?f2 ` \<dots> = ?f2 ` {0 ..< i - 1} \<union> {?f2 (i - 1)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) (map of_int_hom.vec_hom fs') ` ({0..<i - 1} \<union> {i - 1}) = (!) (map of_int_hom.vec_hom fs') ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs' ! (i - 1)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(!) (map of_int_hom.vec_hom fs') ` ({0..<i - 1} \<union> {i - 1}) = (!) (map of_int_hom.vec_hom fs') ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs' ! (i - 1)}

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(!) (map of_int_hom.vec_hom fs') ` ({0..<i - 1} \<union> {i - 1}) = (!) (map of_int_hom.vec_hom fs') ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs' ! (i - 1)}

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) (map of_int_hom.vec_hom fs') ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs' ! (i - 1)} = U
[PROOF STEP]
unfolding U_def fs'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (!) (map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i])) ` {0..<i - 1} \<union> {map of_int_hom.vec_hom (fs[i := fs ! (i - 1), i - 1 := fs ! i]) ! (i - 1)} = (!) (map of_int_hom.vec_hom fs) ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs ! i}
[PROOF STEP]
by (rule arg_cong2[of _ _ _ _ "(\<union>)"], insert i inv(6), force+)
[PROOF STATE]
proof (state)
this:
(!) (map of_int_hom.vec_hom fs') ` {0..<i - 1} \<union> {map of_int_hom.vec_hom fs' ! (i - 1)} = U

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gs.is_oc_projection (gs2.gso i) (gs.span U) (u + gs1.gso (i - 1))
[PROOF STEP]
have "gs.is_oc_projection (?g2 i) (gs.span U) (u + ?g1 (i - 1))"
[PROOF STATE]
proof (prove)
using this:
gs.is_oc_projection (gs2.gso i) (gs.span U) (u + gs1.gso (i - 1))

goal (1 subgoal):
 1. gs.is_oc_projection (gs2.gso i) (gs.span U) (u + gs1.gso (i - 1))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
gs.is_oc_projection (gs2.gso i) (gs.span U) (u + gs1.gso (i - 1))

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
hence proj: "gs.is_oc_projection (?g2 i) (gs.span U) (?g1 (i - 1))"
[PROOF STATE]
proof (prove)
using this:
gs.is_oc_projection (gs2.gso i) (gs.span U) (u + gs1.gso (i - 1))

goal (1 subgoal):
 1. gs.is_oc_projection (gs2.gso i) (gs.span U) (gs1.gso (i - 1))
[PROOF STEP]
unfolding gs.is_oc_projection_def
[PROOF STATE]
proof (prove)
using this:
gs2.gso i \<in> Rn \<and> u + gs1.gso (i - 1) - gs2.gso i \<in> gs.span (gs.span U) \<and> (\<forall>u. u \<in> gs.span U \<longrightarrow> gs2.gso i \<bullet> u = 0)

goal (1 subgoal):
 1. gs2.gso i \<in> Rn \<and> gs1.gso (i - 1) - gs2.gso i \<in> gs.span (gs.span U) \<and> (\<forall>u. u \<in> gs.span U \<longrightarrow> gs2.gso i \<bullet> u = 0)
[PROOF STEP]
using gs.span_add[OF U uU, of "?g1 (i - 1) - ?g2 i"]
          inv(5)[OF im1] g2i u id_u
[PROOF STATE]
proof (prove)
using this:
gs2.gso i \<in> Rn \<and> u + gs1.gso (i - 1) - gs2.gso i \<in> gs.span (gs.span U) \<and> (\<forall>u. u \<in> gs.span U \<longrightarrow> gs2.gso i \<bullet> u = 0)
gs1.gso (i - 1) - gs2.gso i \<in> Rn \<Longrightarrow> (gs1.gso (i - 1) - gs2.gso i \<in> gs.span U) = (u + (gs1.gso (i - 1) - gs2.gso i) \<in> gs.span U)
gs1.gso (i - 1) \<in> Rn
gs2.gso i \<in> Rn
u \<in> Rn
u + (gs1.gso (i - 1) - gs2.gso i) = u + gs1.gso (i - 1) - gs2.gso i

goal (1 subgoal):
 1. gs2.gso i \<in> Rn \<and> gs1.gso (i - 1) - gs2.gso i \<in> gs.span (gs.span U) \<and> (\<forall>u. u \<in> gs.span U \<longrightarrow> gs2.gso i \<bullet> u = 0)
[PROOF STEP]
by (auto simp: U)
[PROOF STATE]
proof (state)
this:
gs.is_oc_projection (gs2.gso i) (gs.span U) (gs1.gso (i - 1))

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
from gs.is_oc_projection_sq_norm[OF this gs.span_is_subset2[OF U]  inv(5)[OF im1]]
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
show "?n2 i \<le> ?n1 (i - 1)"
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso i\<parallel>\<^sup>2 \<le> \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
have "\<dots> \<le> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
\<parallel>gs1.gso (i - 1)\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. k = i \<Longrightarrow> \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal (1 subgoal):
 1. \<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>gs2.gso k\<parallel>\<^sup>2 \<le> B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g_bnd B fs'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma c_snd_le_arg: "c_snd u \<le> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_snd u \<le> u
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. c_snd u \<le> u
[PROOF STEP]
have "c_snd u \<le> c_sum u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_snd u \<le> c_sum u
[PROOF STEP]
by (rule c_snd_le_c_sum)
[PROOF STATE]
proof (state)
this:
c_snd u \<le> c_sum u

goal (1 subgoal):
 1. c_snd u \<le> u
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c_snd u \<le> c_sum u

goal (1 subgoal):
 1. c_snd u \<le> u
[PROOF STEP]
have "c_sum u \<le> u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c_sum u \<le> u
[PROOF STEP]
by (rule c_sum_le_arg)
[PROOF STATE]
proof (state)
this:
c_sum u \<le> u

goal (1 subgoal):
 1. c_snd u \<le> u
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c_snd u \<le> c_sum u
c_sum u \<le> u
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
c_snd u \<le> c_sum u
c_sum u \<le> u

goal (1 subgoal):
 1. c_snd u \<le> u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
c_snd u \<le> u

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma assign_global_A:
     "\<lbrace>\<lambda>\<sigma>. \<triangleright> \<sigma> \<and>  P (\<sigma>\<lparr>A := rhs \<sigma>\<rparr>)\<rbrace>  A_update :==\<^sub>G rhs \<lbrace>\<lambda>r \<sigma>. \<triangleright> \<sigma> \<and> P \<sigma> \<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>\<sigma>. \<triangleright> \<sigma> \<and> P (\<sigma>\<lparr>A := rhs \<sigma>\<rparr>)\<rbrace> A_update :==\<^sub>G rhs \<lbrace>\<lambda>r \<sigma>. \<triangleright> \<sigma> \<and> P \<sigma>\<rbrace>
[PROOF STEP]
apply(rule assign_global)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<sharp> A_update
[PROOF STEP]
apply(rule strong_vs_weak_upd [of global_state_state.A global_state_state.A_update])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<sharp>! (create\<^sub>L A A_update)
 2. (\<lambda>f \<sigma>. \<sigma>\<lparr>A := f (A \<sigma>)\<rparr>) = A_update
[PROOF STEP]
apply (metis A\<^sub>L'_def A\<^sub>L'_strong_indep)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>f \<sigma>. \<sigma>\<lparr>A := f (A \<sigma>)\<rparr>) = A_update
[PROOF STEP]
by(rule ext, rule ext, auto)


[STATEMENT]
lemma apply_outputs_unupdated: assumes "ia \<noteq> r"
      and "ia < length P"
    shows "apply_outputs P j ! ia = apply_outputs (list_update P r v)j ! ia"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_outputs P j ! ia = apply_outputs (P[r := v]) j ! ia
[PROOF STEP]
by (metis apply_outputs_nth assms(1) assms(2) length_list_update nth_list_update_neq)


[STATEMENT]
lemma mat_max_closed[intro]:
  "A \<in> carrier_mat nr nc \<Longrightarrow> B \<in> carrier_mat nr nc \<Longrightarrow> max\<^sub>m A B \<in> carrier_mat nr nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc\<rbrakk> \<Longrightarrow> max\<^sub>m A B \<in> carrier_mat nr nc
[PROOF STEP]
unfolding mat_max_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<in> carrier_mat nr nc; B \<in> carrier_mat nr nc\<rbrakk> \<Longrightarrow> mat (dim_row A) (dim_col A) (\<lambda>ij. max (A $$ ij) (B $$ ij)) \<in> carrier_mat nr nc
[PROOF STEP]
by auto


[STATEMENT]
lemma prime_half:
  assumes "prime (p::int)"
          "p > 2"
  shows "\<lceil>p / 2\<rceil> > \<lfloor>p / 2\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
have "odd p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. odd p
[PROOF STEP]
using prime_odd_int[OF assms]
[PROOF STATE]
proof (prove)
using this:
odd p

goal (1 subgoal):
 1. odd p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
odd p

goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
odd p
[PROOF STEP]
have "\<lceil>p / 2\<rceil> > p/2"
[PROOF STATE]
proof (prove)
using this:
odd p

goal (1 subgoal):
 1. real_of_int p / 2 < real_of_int \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
by (smt (verit, best) cos_npi_int cos_zero_iff_int
    le_of_int_ceiling mult.commute times_divide_eq_right)
[PROOF STATE]
proof (state)
this:
real_of_int p / 2 < real_of_int \<lceil>real_of_int p / 2\<rceil>

goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int p / 2 < real_of_int \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
have "\<lfloor>p / 2\<rfloor> < p/2"
[PROOF STATE]
proof (prove)
using this:
real_of_int p / 2 < real_of_int \<lceil>real_of_int p / 2\<rceil>

goal (1 subgoal):
 1. real_of_int \<lfloor>real_of_int p / 2\<rfloor> < real_of_int p / 2
[PROOF STEP]
by (meson floor_less_iff less_ceiling_iff)
[PROOF STATE]
proof (state)
this:
real_of_int \<lfloor>real_of_int p / 2\<rfloor> < real_of_int p / 2

goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
real_of_int \<lfloor>real_of_int p / 2\<rfloor> < real_of_int p / 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real_of_int \<lfloor>real_of_int p / 2\<rfloor> < real_of_int p / 2

goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
using \<open>\<lceil>p / 2\<rceil> > p/2\<close>
[PROOF STATE]
proof (prove)
using this:
real_of_int \<lfloor>real_of_int p / 2\<rfloor> < real_of_int p / 2
real_of_int p / 2 < real_of_int \<lceil>real_of_int p / 2\<rceil>

goal (1 subgoal):
 1. \<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>real_of_int p / 2\<rfloor> < \<lceil>real_of_int p / 2\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma genempty_substs: "genempty Q \<Longrightarrow> length xs = length ys \<Longrightarrow> genempty (Q[xs \<^bold>\<rightarrow>\<^sup>* ys])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>genempty Q; length xs = length ys\<rbrakk> \<Longrightarrow> genempty (Q[xs \<^bold>\<rightarrow>\<^sup>* ys])
[PROOF STEP]
by (induct Q arbitrary: xs ys rule: genempty.induct) (auto intro: genempty.intros)


[STATEMENT]
lemma set_compP:
 "((C,D,fs,ms') \<in> set(compP f P)) =
  (\<exists>ms. (C,D,fs,ms) \<in> set P \<and> ms' = map (compM f) ms)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((C, D, fs, ms') \<in> set (compP f P)) = (\<exists>ms. (C, D, fs, ms) \<in> set P \<and> ms' = map (compM f) ms)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((C, D, fs, ms') \<in> set (compP f P)) = (\<exists>ms. (C, D, fs, ms) \<in> set P \<and> ms' = map (compM f) ms)
[PROOF STEP]
by(fastforce simp add:compP_def compC_def image_iff Bex_def)


[STATEMENT]
lemma analz_Un_implInsecSet:
  "Enc_keys_clean (G \<union> H) \<Longrightarrow>
   analz (sym.implInsecSet G \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> -payload"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz ({sym.implInsec A B M |A B M. M \<in> G} \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> - payload
[PROOF STEP]
apply (rule subset_trans [of _ "analz (implInsecSet_aux G \<union> H)" _])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz ({sym.implInsec A B M |A B M. M \<in> G} \<union> H) \<subseteq> analz (PairSet Tags (PairSet AgentSet (PairSet AgentSet G)) \<union> H)
 2. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz (PairSet Tags (PairSet AgentSet (PairSet AgentSet G)) \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> - payload
[PROOF STEP]
apply (rule analz_mono, rule Un_mono, blast intro!: implSet_implSet_aux, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz (PairSet Tags (PairSet AgentSet (PairSet AgentSet G)) \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> - payload
[PROOF STEP]
using analz_Un_implInsecSet_aux_3
[PROOF STATE]
proof (prove)
using this:
Enc_keys_clean (?G \<union> ?H) \<Longrightarrow> analz (PairSet Tags (PairSet AgentSet (PairSet AgentSet ?G)) \<union> ?H) \<subseteq> synth (analz (?G \<union> ?H)) \<union> - payload

goal (1 subgoal):
 1. Enc_keys_clean (G \<union> H) \<Longrightarrow> analz (PairSet Tags (PairSet AgentSet (PairSet AgentSet G)) \<union> H) \<subseteq> synth (analz (G \<union> H)) \<union> - payload
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma count_list_length_replicate: "count_list xs y = length xs \<longleftrightarrow> xs = replicate (length xs) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (count_list xs y = length xs) = (xs = replicate (length xs) y)
[PROOF STEP]
by (metis count_list_full_elem count_list_replicate replicate_length_same)


[STATEMENT]
lemma llength_lappend_end'E[elim]:
    assumes "llength w = enat (Suc n)"
    obtains a v
    where "w = v $ " "llength v = enat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v a. \<lbrakk>w = v $ ; llength v = enat n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>v a. \<lbrakk>w = v $ ; llength v = enat n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 1: "llength w \<ge> eSuc (enat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eSuc (enat n) \<le> llength w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
llength w = enat (Suc n)

goal (1 subgoal):
 1. eSuc (enat n) \<le> llength w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eSuc (enat n) \<le> llength w

goal (1 subgoal):
 1. (\<And>v a. \<lbrakk>w = v $ ; llength v = enat n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain a v where 2: "w = v $ "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>v a. w = v $  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
eSuc (enat n) \<le> llength w

goal (1 subgoal):
 1. (\<And>v a. w = v $  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
w = v $

goal (1 subgoal):
 1. (\<And>v a. \<lbrakk>w = v $ ; llength v = enat n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w = ?v $ <?a>
 2. llength ?v = enat n
[PROOF STEP]
show "w = v $ "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w = v $
[PROOF STEP]
using 2(1)
[PROOF STATE]
proof (prove)
using this:
w = v $

goal (1 subgoal):
 1. w = v $
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
w = v $

goal (1 subgoal):
 1. llength v = enat n
[PROOF STEP]
show "llength v = enat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. llength v = enat n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
llength w = enat (Suc n)

goal (1 subgoal):
 1. llength v = enat n
[PROOF STEP]
unfolding 2(1)
[PROOF STATE]
proof (prove)
using this:
llength (v $ ) = enat (Suc n)

goal (1 subgoal):
 1. llength v = enat n
[PROOF STEP]
by (simp, metis eSuc_enat eSuc_inject)
[PROOF STATE]
proof (state)
this:
llength v = enat n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed