[STATEMENT]
lemma gram_schmidt_short_vector:
  assumes in_L: "h \<in> lattice_of fs - {0\<^sub>v n}"
  shows "\<exists> i < m. \<parallel>h\<parallel>\<^sup>2 \<ge> \<parallel>gso i\<parallel>\<^sup>2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from in_L
[PROOF STATE]
proof (chain)
picking this:
h \<in> lattice_of fs - {0\<^sub>v n}
[PROOF STEP]
have non_0: "h \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
h \<in> lattice_of fs - {0\<^sub>v n}

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

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from in_L[unfolded lattice_of_def]
[PROOF STATE]
proof (chain)
picking this:
h \<in> range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs])) - {0\<^sub>v n}
[PROOF STEP]
obtain lam where
    h: "h =  sumlist (map (\<lambda> i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0 ..< length fs])"
[PROOF STATE]
proof (prove)
using this:
h \<in> range (\<lambda>c. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<length fs])) - {0\<^sub>v n}

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

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have in_L: "h = sumlist (map (\<lambda> i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0 ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])
[PROOF STEP]
unfolding length_map h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])
[PROOF STEP]
by (rule arg_cong[of _ _ sumlist], rule map_cong, auto)
[PROOF STATE]
proof (state)
this:
h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?n = "[0 ..< m]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?f = "(\<lambda> i. of_int (lam i) \<cdot>\<^sub>v fs ! i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?vs = "map ?f ?n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?P = "\<lambda> k. k < m \<and> lam k \<noteq> 0"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define k where "k = (GREATEST kk. ?P kk)"
[PROOF STATE]
proof (state)
this:
k = (GREATEST kk. kk < length fs \<and> lam kk \<noteq> 0)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
k = (GREATEST kk. kk < length fs \<and> lam kk \<noteq> 0)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
assume *: "\<forall> i < m. lam i = 0"
[PROOF STATE]
proof (state)
this:
\<forall>i<length fs. lam i = 0

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have vs: "?vs = map (\<lambda> i. 0\<^sub>v n) ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs] = map (\<lambda>i. 0\<^sub>v n) [0..<length fs]
[PROOF STEP]
by (rule map_cong, insert f_dim *, auto)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs] = map (\<lambda>i. 0\<^sub>v n) [0..<length fs]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "h = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = 0\<^sub>v n
[PROOF STEP]
unfolding in_L vs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. 0\<^sub>v n) [0..<length fs]) = 0\<^sub>v n
[PROOF STEP]
by (rule sumlist_neutral, auto)
[PROOF STATE]
proof (state)
this:
h = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
with non_0
[PROOF STATE]
proof (chain)
picking this:
h \<noteq> 0\<^sub>v n
h = 0\<^sub>v n
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
h \<noteq> 0\<^sub>v n
h = 0\<^sub>v n

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

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>i<length fs. lam i = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length fs. lam i = 0 \<Longrightarrow> False
[PROOF STEP]
obtain kk where "?P kk"
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length fs. lam i = 0 \<Longrightarrow> False

goal (1 subgoal):
 1. (\<And>kk. kk < length fs \<and> lam kk \<noteq> 0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
kk < length fs \<and> lam kk \<noteq> 0

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from GreatestI_nat[of ?P, OF this, of m]
[PROOF STATE]
proof (chain)
picking this:
(\<And>y. y < length fs \<and> lam y \<noteq> 0 \<Longrightarrow> y \<le> length fs) \<Longrightarrow> (GREATEST k. k < length fs \<and> lam k \<noteq> 0) < length fs \<and> lam (GREATEST k. k < length fs \<and> lam k \<noteq> 0) \<noteq> 0
[PROOF STEP]
have Pk: "?P k"
[PROOF STATE]
proof (prove)
using this:
(\<And>y. y < length fs \<and> lam y \<noteq> 0 \<Longrightarrow> y \<le> length fs) \<Longrightarrow> (GREATEST k. k < length fs \<and> lam k \<noteq> 0) < length fs \<and> lam (GREATEST k. k < length fs \<and> lam k \<noteq> 0) \<noteq> 0

goal (1 subgoal):
 1. k < length fs \<and> lam k \<noteq> 0
[PROOF STEP]
unfolding k_def
[PROOF STATE]
proof (prove)
using this:
(\<And>y. y < length fs \<and> lam y \<noteq> 0 \<Longrightarrow> y \<le> length fs) \<Longrightarrow> (GREATEST k. k < length fs \<and> lam k \<noteq> 0) < length fs \<and> lam (GREATEST k. k < length fs \<and> lam k \<noteq> 0) \<noteq> 0

goal (1 subgoal):
 1. (GREATEST kk. kk < length fs \<and> lam kk \<noteq> 0) < length fs \<and> lam (GREATEST kk. kk < length fs \<and> lam kk \<noteq> 0) \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < length fs \<and> lam k \<noteq> 0

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
hence kn: "k < m"
[PROOF STATE]
proof (prove)
using this:
k < length fs \<and> lam k \<noteq> 0

goal (1 subgoal):
 1. k < length fs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
k < length fs

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?gso = "(\<lambda>i j. \<mu> i j \<cdot>\<^sub>v gso j)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have k: "k < i \<Longrightarrow> i < m \<Longrightarrow> lam i = 0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < i; i < length fs\<rbrakk> \<Longrightarrow> lam i = 0
[PROOF STEP]
using Greatest_le_nat[of ?P i m, folded k_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i < length fs \<and> lam i \<noteq> 0; \<And>y. y < length fs \<and> lam y \<noteq> 0 \<Longrightarrow> y \<le> length fs\<rbrakk> \<Longrightarrow> i \<le> k

goal (1 subgoal):
 1. \<lbrakk>k < i; i < length fs\<rbrakk> \<Longrightarrow> lam i = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>k < ?i1; ?i1 < length fs\<rbrakk> \<Longrightarrow> lam ?i1 = 0

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define l where "l = lam k"
[PROOF STATE]
proof (state)
this:
l = lam k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from Pk
[PROOF STATE]
proof (chain)
picking this:
k < length fs \<and> lam k \<noteq> 0
[PROOF STEP]
have l: "l \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
k < length fs \<and> lam k \<noteq> 0

goal (1 subgoal):
 1. l \<noteq> 0
[PROOF STEP]
unfolding l_def
[PROOF STATE]
proof (prove)
using this:
k < length fs \<and> lam k \<noteq> 0

goal (1 subgoal):
 1. lam k \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l \<noteq> 0

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define idx where "idx = [0 ..< k]"
[PROOF STATE]
proof (state)
this:
idx = [0..<k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have idx: "\<And> i. i \<in> set idx \<Longrightarrow> i < k" "\<And> i. i \<in> set idx \<Longrightarrow> i < m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> set idx \<Longrightarrow> i < k) &&& (\<And>i. i \<in> set idx \<Longrightarrow> i < length fs)
[PROOF STEP]
unfolding idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. i \<in> set [0..<k] \<Longrightarrow> i < k) &&& (\<And>i. i \<in> set [0..<k] \<Longrightarrow> i < length fs)
[PROOF STEP]
using kn
[PROOF STATE]
proof (prove)
using this:
k < length fs

goal (1 subgoal):
 1. (\<And>i. i \<in> set [0..<k] \<Longrightarrow> i < k) &&& (\<And>i. i \<in> set [0..<k] \<Longrightarrow> i < length fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 \<in> set idx \<Longrightarrow> ?i1 < k
?i1 \<in> set idx \<Longrightarrow> ?i1 < length fs

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from Pk
[PROOF STATE]
proof (chain)
picking this:
k < length fs \<and> lam k \<noteq> 0
[PROOF STEP]
have split: "[0 ..< m] = idx @ [k] @ [Suc k ..< m]"
[PROOF STATE]
proof (prove)
using this:
k < length fs \<and> lam k \<noteq> 0

goal (1 subgoal):
 1. [0..<length fs] = idx @ [k] @ [Suc k..<length fs]
[PROOF STEP]
unfolding idx_def
[PROOF STATE]
proof (prove)
using this:
k < length fs \<and> lam k \<noteq> 0

goal (1 subgoal):
 1. [0..<length fs] = [0..<k] @ [k] @ [Suc k..<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] = idx @ [k] @ [Suc k..<length fs]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define gg where "gg = sumlist
    (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int l \<cdot>\<^sub>v sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx)"
[PROOF STATE]
proof (state)
this:
gg = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int l \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "h = sumlist ?vs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])
[PROOF STEP]
unfolding in_L
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sumlist ((map ?f idx @ [?f k]) @ map ?f [Suc k ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])
[PROOF STEP]
unfolding split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (idx @ [k] @ [Suc k..<length fs])) = M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [0..<length fs]) = M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sumlist (map ?f idx @ [?f k]) + sumlist (map ?f [Suc k ..< m])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])
[PROOF STEP]
by (rule sumlist_append, auto intro!: f_carrier, insert Pk idx, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist ((map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "sumlist (map ?f [Suc k ..< m]) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs]) = 0\<^sub>v n
[PROOF STEP]
by (rule sumlist_neutral, auto simp: k)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs]) = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) [Suc k..<length fs]) = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "sumlist (map ?f idx @ [?f k]) = sumlist (map ?f idx) + ?f k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int (lam k) \<cdot>\<^sub>v fs ! k
[PROOF STEP]
by (subst sumlist_append, auto intro!: f_carrier, insert Pk idx, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int (lam k) \<cdot>\<^sub>v fs ! k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx @ [of_int (lam k) \<cdot>\<^sub>v fs ! k]) = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int (lam k) \<cdot>\<^sub>v fs ! k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "fs ! k = sumlist (map (?gso k) [0..<Suc k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs ! k = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<Suc k])
[PROOF STEP]
using fi_is_sum_of_mu_gso[OF kn]
[PROOF STATE]
proof (prove)
using this:
fs ! k = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<Suc k])

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

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
fs ! k = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<Suc k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sumlist (map (?gso k) idx @ [gso k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<Suc k]) = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx @ [gso k])
[PROOF STEP]
by (simp add: \<mu>.simps[of k k] idx_def)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<Suc k]) = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx @ [gso k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<Suc k]) = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx @ [gso k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sumlist (map (?gso k) idx) + gso k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx @ [gso k]) = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + gso k
[PROOF STEP]
by (subst sumlist_append, auto intro!: f_carrier, insert Pk idx, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx @ [gso k]) = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx @ [gso k]) = M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "of_int (lam k) \<cdot>\<^sub>v \<dots> = of_int (lam k) \<cdot>\<^sub>v (sumlist (map (?gso k) idx))
    + of_int (lam k) \<cdot>\<^sub>v gso k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (lam k) \<cdot>\<^sub>v (M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + gso k) = of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k
[PROOF STEP]
unfolding idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (lam k) \<cdot>\<^sub>v (M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<k]) + gso k) = of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) [0..<k]) + of_int (lam k) \<cdot>\<^sub>v gso k
[PROOF STEP]
by (rule smult_add_distrib_vec[OF sumlist_carrier], auto intro!: gso_carrier, insert kn, auto)
[PROOF STATE]
proof (state)
this:
of_int (lam k) \<cdot>\<^sub>v (M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + gso k) = of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + (of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n
[PROOF STEP]
have "h = sumlist (map ?f idx) +
       (of_int (lam k) \<cdot>\<^sub>v sumlist (map (?gso k) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n "
[PROOF STATE]
proof (prove)
using this:
h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + (of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n

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

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
h = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + (of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = gg + of_int l \<cdot>\<^sub>v gso k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + (of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n = gg + of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
unfolding gg_def l_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + (of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n = M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k
[PROOF STEP]
by (rule eq_vecI, insert idx kn, auto simp: sumlist_vec_index,
      subst index_add_vec, auto simp: sumlist_dim kn, subst sumlist_dim, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + (of_int (lam k) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) + of_int (lam k) \<cdot>\<^sub>v gso k) + 0\<^sub>v n = gg + of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
h = gg + of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
have hgg: "h = gg + of_int l \<cdot>\<^sub>v gso k"
[PROOF STATE]
proof (prove)
using this:
h = gg + of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. h = gg + of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
h = gg + of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?k = "[0 ..< k]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define R where "R = {gg. \<exists> nu. gg = sumlist (map (\<lambda> i. nu i \<cdot>\<^sub>v gso i) idx)}"
[PROOF STATE]
proof (state)
this:
R = {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
R = {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
fix nu
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "dim_vec (sumlist (map (\<lambda> i. nu i \<cdot>\<^sub>v gso i) idx)) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)) = n
[PROOF STEP]
by (rule sumlist_dim, insert kn, auto simp: idx_def)
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)) = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>i. ?nu3 i \<cdot>\<^sub>v gso i) idx)) = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
note dim_nu[simp] = this
[PROOF STATE]
proof (state)
this:
dim_vec (M.sumlist (map (\<lambda>i. ?nu3 i \<cdot>\<^sub>v gso i) idx)) = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define kk where "kk = ?k"
[PROOF STATE]
proof (state)
this:
kk = [0..<k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
kk = [0..<k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
assume "v \<in> R"
[PROOF STATE]
proof (state)
this:
v \<in> R

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v \<in> R
[PROOF STEP]
obtain nu where v: "v = sumlist (map (\<lambda> i. nu i \<cdot>\<^sub>v gso i) idx)"
[PROOF STATE]
proof (prove)
using this:
v \<in> R

goal (1 subgoal):
 1. (\<And>nu. v = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
v \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}

goal (1 subgoal):
 1. (\<And>nu. v = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "dim_vec v = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec v = n
[PROOF STEP]
unfolding gg_def v
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)) = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dim_vec v = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?v3 \<in> R \<Longrightarrow> dim_vec ?v3 = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
note dim_R = this
[PROOF STATE]
proof (state)
this:
?v3 \<in> R \<Longrightarrow> dim_vec ?v3 = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?v3 \<in> R \<Longrightarrow> dim_vec ?v3 = n

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
fix v1 v2
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
assume "v1 \<in> R" "v2 \<in> R"
[PROOF STATE]
proof (state)
this:
v1 \<in> R
v2 \<in> R

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v1 \<in> R
v2 \<in> R
[PROOF STEP]
obtain nu1 nu2 where v1: "v1 = sumlist (map (\<lambda> i. nu1 i \<cdot>\<^sub>v gso i) idx)" and
      v2: "v2 = sumlist (map (\<lambda> i. nu2 i \<cdot>\<^sub>v gso i) idx)"
[PROOF STATE]
proof (prove)
using this:
v1 \<in> R
v2 \<in> R

goal (1 subgoal):
 1. (\<And>nu1 nu2. \<lbrakk>v1 = M.sumlist (map (\<lambda>i. nu1 i \<cdot>\<^sub>v gso i) idx); v2 = M.sumlist (map (\<lambda>i. nu2 i \<cdot>\<^sub>v gso i) idx)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
v1 \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}
v2 \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}

goal (1 subgoal):
 1. (\<And>nu1 nu2. \<lbrakk>v1 = M.sumlist (map (\<lambda>i. nu1 i \<cdot>\<^sub>v gso i) idx); v2 = M.sumlist (map (\<lambda>i. nu2 i \<cdot>\<^sub>v gso i) idx)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v1 = M.sumlist (map (\<lambda>i. nu1 i \<cdot>\<^sub>v gso i) idx)
v2 = M.sumlist (map (\<lambda>i. nu2 i \<cdot>\<^sub>v gso i) idx)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "v1 + v2 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 + v2 \<in> R
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v1 + v2 \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}
[PROOF STEP]
by (standard, rule exI[of _ "\<lambda> i. nu1 i + nu2 i"], unfold v1 v2, rule eq_vecI,
        (subst sumlist_vec_index, insert idx, auto intro!: gso_carrier simp: o_def)+,
        unfold sum_list_addf[symmetric], induct idx, auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
v1 + v2 \<in> R

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v1.3 \<in> R; ?v2.3 \<in> R\<rbrakk> \<Longrightarrow> ?v1.3 + ?v2.3 \<in> R

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
note add_R = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v1.3 \<in> R; ?v2.3 \<in> R\<rbrakk> \<Longrightarrow> ?v1.3 + ?v2.3 \<in> R

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "gg \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gg \<in> R
[PROOF STEP]
unfolding gg_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) + of_int l \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) \<in> R
[PROOF STEP]
proof (rule add_R)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R
 2. of_int l \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) \<in> R
[PROOF STEP]
show "of_int l \<cdot>\<^sub>v sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int l \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) \<in> R
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int l \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}
[PROOF STEP]
by (standard, rule exI[of _ "\<lambda>i. of_int l * \<mu> k i"], rule eq_vecI,
       (subst sumlist_vec_index, insert idx, auto intro!: gso_carrier simp: o_def)+,
       induct idx, auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
of_int l \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> k j \<cdot>\<^sub>v gso j) idx) \<in> R

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R
[PROOF STEP]
show "sumlist (map ?f idx) \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R
[PROOF STEP]
using idx
[PROOF STATE]
proof (prove)
using this:
?i1 \<in> set idx \<Longrightarrow> ?i1 < k
?i1 \<in> set idx \<Longrightarrow> ?i1 < length fs

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R
[PROOF STEP]
proof (induct idx)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>i. i \<in> set [] \<Longrightarrow> i < k; \<And>i. i \<in> set [] \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) []) \<in> R
 2. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
?i1 \<in> set [] \<Longrightarrow> ?i1 < k
?i1 \<in> set [] \<Longrightarrow> ?i1 < length fs

goal (2 subgoals):
 1. \<lbrakk>\<And>i. i \<in> set [] \<Longrightarrow> i < k; \<And>i. i \<in> set [] \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) []) \<in> R
 2. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) []) \<in> R
[PROOF STEP]
by (simp add: R_def, intro exI[of _ "\<lambda> i. 0"], rule eq_vecI,
        (subst sumlist_vec_index, insert idx, auto intro!: gso_carrier simp: o_def)+,
        induct idx, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) []) \<in> R

goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
case (Cons i idxs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i. i \<in> set idxs \<Longrightarrow> i < k; \<And>i. i \<in> set idxs \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs) \<in> R
?i1 \<in> set (i # idxs) \<Longrightarrow> ?i1 < k
?i1 \<in> set (i # idxs) \<Longrightarrow> ?i1 < length fs

goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
have "sumlist (map ?f (i # idxs)) = sumlist ([?f i] @ map ?f idxs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = M.sumlist ([of_int (lam i) \<cdot>\<^sub>v fs ! i] @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = M.sumlist ([of_int (lam i) \<cdot>\<^sub>v fs ! i] @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)

goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = M.sumlist ([of_int (lam i) \<cdot>\<^sub>v fs ! i] @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)

goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
have "\<dots> = ?f i + sumlist (map ?f idxs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist ([of_int (lam i) \<cdot>\<^sub>v fs ! i] @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs) = of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)
[PROOF STEP]
by (subst sumlist_append, insert Cons(3), auto intro!: f_carrier)
[PROOF STATE]
proof (state)
this:
M.sumlist ([of_int (lam i) \<cdot>\<^sub>v fs ! i] @ map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs) = of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)

goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)
[PROOF STEP]
have id: "sumlist (map ?f (i # idxs)) = ?f i + sumlist (map ?f idxs)"
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) = of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs)

goal (1 subgoal):
 1. \<And>a idx. \<lbrakk>\<lbrakk>\<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < k; \<And>i. i \<in> set (a # idx) \<Longrightarrow> i < length fs\<rbrakk> \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (a # idx)) \<in> R
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) \<in> R
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i + M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idxs) \<in> R
[PROOF STEP]
proof (rule add_R[OF _ Cons(1)[OF Cons(2-3)]])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
from Cons(2-3)
[PROOF STATE]
proof (chain)
picking this:
?i1 \<in> set (i # idxs) \<Longrightarrow> ?i1 < k
?i1 \<in> set (i # idxs) \<Longrightarrow> ?i1 < length fs
[PROOF STEP]
have i: "i < m" "i < k"
[PROOF STATE]
proof (prove)
using this:
?i1 \<in> set (i # idxs) \<Longrightarrow> ?i1 < k
?i1 \<in> set (i # idxs) \<Longrightarrow> ?i1 < length fs

goal (1 subgoal):
 1. i < length fs &&& i < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length fs
i < k

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
hence idx_split: "idx = [0 ..< Suc i] @ [Suc i ..< k]"
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < k

goal (1 subgoal):
 1. idx = [0..<Suc i] @ [Suc i..<k]
[PROOF STEP]
unfolding idx_def
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < k

goal (1 subgoal):
 1. [0..<k] = [0..<Suc i] @ [Suc i..<k]
[PROOF STEP]
by (metis Suc_lessI append_Nil2 less_imp_add_positive upt_add_eq_append upt_rec zero_le)
[PROOF STATE]
proof (state)
this:
idx = [0..<Suc i] @ [Suc i..<k]

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
idx = [0..<Suc i] @ [Suc i..<k]

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
assume j: "j < n"
[PROOF STATE]
proof (state)
this:
j < n

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
define idxs where "idxs = [0 ..< Suc i]"
[PROOF STATE]
proof (state)
this:
idxs = [0..<Suc i]

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
let ?f = "\<lambda> x. ((if x < Suc i then of_int (lam i) * \<mu> i x else 0) \<cdot>\<^sub>v gso x) $ j"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
have "(\<Sum>x\<leftarrow>idx. ?f x) = (\<Sum>x\<leftarrow>[0 ..< Suc i]. ?f x) + (\<Sum>x\<leftarrow> [Suc i ..< k]. ?f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) + (\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
unfolding idx_split
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[0..<Suc i] @ [Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) + (\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) + (\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) + (\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
have "(\<Sum>x\<leftarrow> [Suc i ..< k]. ?f x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (0::'a)
[PROOF STEP]
by (rule sum_list_neutral, insert j kn, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (0::'a)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>[Suc i..<k]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (0::'a)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
have "(\<Sum>x\<leftarrow>[0 ..< Suc i]. ?f x) = (\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
unfolding idxs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>[0..<Suc i]. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
by (rule arg_cong[of _ _ sum_list], rule map_cong[OF refl],
                subst index_smult_vec, insert j i kn, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>[0..<Suc i]. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = (\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
have "\<dots> = of_int (lam i) * ((\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
unfolding idxs_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>idxs. (\<mu> i x \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
by (induct idxs, auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>idxs. of_int (lam i) * (\<mu> i x \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j) + (0::'a)
[PROOF STEP]
have "(\<Sum>x\<leftarrow>idx. ?f x) = of_int (lam i) * ((\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j))"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j) + (0::'a)

goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ j) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ j)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
 3. \<And>ia. ia \<in> set idxs__ \<Longrightarrow> ia \<in> set (i # idxs__)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j3 < n \<Longrightarrow> (\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ ?j3) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ ?j3)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
?j3 < n \<Longrightarrow> (\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ ?j3) = of_int (lam i) * (\<Sum>x\<leftarrow>[0..<Suc i]. (\<mu> i x \<cdot>\<^sub>v gso x) $ ?j3)

goal (3 subgoals):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 3. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
show "?f i \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R
[PROOF STEP]
unfolding fi_is_sum_of_mu_gso[OF i(1)] R_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (lam i) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i]) \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}
[PROOF STEP]
apply (standard, rule exI[of _ "\<lambda> j. if j < Suc i then of_int (lam i) * \<mu> i j else 0"], rule eq_vecI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ia. ia < dim_vec (M.sumlist (map (\<lambda>ia. (if ia < Suc i then of_int (lam i) * \<mu> i ia else (0::'a)) \<cdot>\<^sub>v gso ia) idx)) \<Longrightarrow> (of_int (lam i) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])) $ ia = M.sumlist (map (\<lambda>ia. (if ia < Suc i then of_int (lam i) * \<mu> i ia else (0::'a)) \<cdot>\<^sub>v gso ia) idx) $ ia
 2. dim_vec (of_int (lam i) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<Suc i])) = dim_vec (M.sumlist (map (\<lambda>ia. (if ia < Suc i then of_int (lam i) * \<mu> i ia else (0::'a)) \<cdot>\<^sub>v gso ia) idx))
[PROOF STEP]
apply (subst sumlist_vec_index, insert idx i, auto intro!: gso_carrier sumlist_dim simp: o_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>ia < n; \<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs; i < length fs; i < k\<rbrakk> \<Longrightarrow> (of_int (lam i) \<cdot>\<^sub>v M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [\<mu> i i \<cdot>\<^sub>v gso i])) $ ia = (\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ ia)
[PROOF STEP]
apply (subst index_smult_vec, subst sumlist_dim, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia. \<lbrakk>ia < n; \<And>i. i \<in> set idx \<Longrightarrow> i < k; \<And>i. i \<in> set idx \<Longrightarrow> i < length fs; i < length fs; i < k\<rbrakk> \<Longrightarrow> of_int (lam i) * M.sumlist (map (\<lambda>j. \<mu> i j \<cdot>\<^sub>v gso j) [0..<i] @ [\<mu> i i \<cdot>\<^sub>v gso i]) $ ia = (\<Sum>x\<leftarrow>idx. ((if x < Suc i then of_int (lam i) * \<mu> i x else (0::'a)) \<cdot>\<^sub>v gso x) $ ia)
[PROOF STEP]
apply (subst sumlist_vec_index, auto, insert idx i main, auto simp: o_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
of_int (lam i) \<cdot>\<^sub>v fs ! i \<in> R

goal (2 subgoals):
 1. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
 2. \<And>ia. ia \<in> set idxs \<Longrightarrow> ia \<in> set (i # idxs)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) (i # idxs)) \<in> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (lam i) \<cdot>\<^sub>v fs ! i) idx) \<in> R

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gg \<in> R

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gg \<in> R
[PROOF STEP]
obtain nu where gg: "gg = sumlist (map (\<lambda> i. nu i \<cdot>\<^sub>v gso i) idx)"
[PROOF STATE]
proof (prove)
using this:
gg \<in> R

goal (1 subgoal):
 1. (\<And>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding R_def
[PROOF STATE]
proof (prove)
using this:
gg \<in> {gg. \<exists>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)}

goal (1 subgoal):
 1. (\<And>nu. gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gg = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?ff = "sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
define hh where "hh = (\<lambda> i. (if i < k then nu i else of_int l))"
[PROOF STATE]
proof (state)
this:
hh = (\<lambda>i. if i < k then nu i else of_int l)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
let ?hh = "sumlist (map (\<lambda> i. hh i \<cdot>\<^sub>v gso i) [0 ..< Suc k])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have ffhh: "?hh = sumlist (map (\<lambda> i. hh i \<cdot>\<^sub>v gso i) [0 ..< k] @ [hh k \<cdot>\<^sub>v gso k])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] @ [hh k \<cdot>\<^sub>v gso k])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] @ [hh k \<cdot>\<^sub>v gso k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] @ [hh k \<cdot>\<^sub>v gso k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = sumlist (map (\<lambda> i. hh i \<cdot>\<^sub>v gso i) [0 ..< k]) + sumlist [hh k \<cdot>\<^sub>v gso k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] @ [hh k \<cdot>\<^sub>v gso k]) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k]) + M.sumlist [hh k \<cdot>\<^sub>v gso k]
[PROOF STEP]
by (rule sumlist_append, insert kn, auto)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] @ [hh k \<cdot>\<^sub>v gso k]) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k]) + M.sumlist [hh k \<cdot>\<^sub>v gso k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] @ [hh k \<cdot>\<^sub>v gso k]) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k]) + M.sumlist [hh k \<cdot>\<^sub>v gso k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "sumlist [hh k \<cdot>\<^sub>v gso k] = hh k \<cdot>\<^sub>v gso k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist [hh k \<cdot>\<^sub>v gso k] = hh k \<cdot>\<^sub>v gso k
[PROOF STEP]
using kn
[PROOF STATE]
proof (prove)
using this:
k < length fs

goal (1 subgoal):
 1. M.sumlist [hh k \<cdot>\<^sub>v gso k] = hh k \<cdot>\<^sub>v gso k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
M.sumlist [hh k \<cdot>\<^sub>v gso k] = hh k \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist [hh k \<cdot>\<^sub>v gso k] = hh k \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = of_int l \<cdot>\<^sub>v gso k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hh k \<cdot>\<^sub>v gso k = of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
unfolding hh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if k < k then nu k else of_int l) \<cdot>\<^sub>v gso k = of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
hh k \<cdot>\<^sub>v gso k = of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
hh k \<cdot>\<^sub>v gso k = of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "map (\<lambda> i. hh i \<cdot>\<^sub>v gso i) [0 ..< k] = map (\<lambda> i. nu i \<cdot>\<^sub>v gso i) [0 ..< k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] = map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) [0..<k]
[PROOF STEP]
by (rule map_cong, auto simp: hh_def)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<k] = map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) [0..<k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) [0..<k]) + of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
have ffhh: "?ff = ?hh"
[PROOF STATE]
proof (prove)
using this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) [0..<k]) + of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k])
[PROOF STEP]
by (simp add: idx_def)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from hgg[unfolded gg]
[PROOF STATE]
proof (chain)
picking this:
h = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
have h: "h = ?ff"
[PROOF STATE]
proof (prove)
using this:
h = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. h = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
h = M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "gso k \<bullet> gso k \<le> 1 * (gso k \<bullet> gso k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gso k \<bullet> gso k \<le> (1::'a) * (gso k \<bullet> gso k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gso k \<bullet> gso k \<le> (1::'a) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gso k \<bullet> gso k \<le> (1::'a) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<le> of_int (l * l) * (gso k \<bullet> gso k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) * (gso k \<bullet> gso k) \<le> of_int (l * l) * (gso k \<bullet> gso k)
[PROOF STEP]
proof (rule mult_right_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (1::'a) \<le> of_int (l * l)
 2. (0::'a) \<le> gso k \<bullet> gso k
[PROOF STEP]
from l
[PROOF STATE]
proof (chain)
picking this:
l \<noteq> 0
[PROOF STEP]
have "l * l \<ge> 1"
[PROOF STATE]
proof (prove)
using this:
l \<noteq> 0

goal (1 subgoal):
 1. 1 \<le> l * l
[PROOF STEP]
by (meson eq_iff int_one_le_iff_zero_less mult_le_0_iff not_le)
[PROOF STATE]
proof (state)
this:
1 \<le> l * l

goal (2 subgoals):
 1. (1::'a) \<le> of_int (l * l)
 2. (0::'a) \<le> gso k \<bullet> gso k
[PROOF STEP]
thus "1 \<le> (of_int (l * l) :: 'a)"
[PROOF STATE]
proof (prove)
using this:
1 \<le> l * l

goal (1 subgoal):
 1. (1::'a) \<le> of_int (l * l)
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> of_int (l * l)

goal (1 subgoal):
 1. (0::'a) \<le> gso k \<bullet> gso k
[PROOF STEP]
show "0 \<le> gso k \<bullet> gso k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> gso k \<bullet> gso k
[PROOF STEP]
by (rule scalar_prod_ge_0)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> gso k \<bullet> gso k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(1::'a) * (gso k \<bullet> gso k) \<le> of_int (l * l) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) * (gso k \<bullet> gso k) \<le> of_int (l * l) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = 0 + of_int (l * l) * (gso k \<bullet> gso k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (l * l) * (gso k \<bullet> gso k) = (0::'a) + of_int (l * l) * (gso k \<bullet> gso k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_int (l * l) * (gso k \<bullet> gso k) = (0::'a) + of_int (l * l) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (l * l) * (gso k \<bullet> gso k) = (0::'a) + of_int (l * l) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<le> sum_list (map (\<lambda> i. (nu i * nu i) * (gso i \<bullet> gso i)) idx) + of_int (l * l) * (gso k \<bullet> gso k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) + of_int (l * l) * (gso k \<bullet> gso k) \<le> (\<Sum>i\<leftarrow>idx. nu i * nu i * (gso i \<bullet> gso i)) + of_int (l * l) * (gso k \<bullet> gso k)
[PROOF STEP]
by (rule add_right_mono, rule sum_list_nonneg, auto, rule mult_nonneg_nonneg, auto simp: scalar_prod_ge_0)
[PROOF STATE]
proof (state)
this:
(0::'a) + of_int (l * l) * (gso k \<bullet> gso k) \<le> (\<Sum>i\<leftarrow>idx. nu i * nu i * (gso i \<bullet> gso i)) + of_int (l * l) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) + of_int (l * l) * (gso k \<bullet> gso k) \<le> (\<Sum>i\<leftarrow>idx. nu i * nu i * (gso i \<bullet> gso i)) + of_int (l * l) * (gso k \<bullet> gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "map (\<lambda> i. (nu i * nu i) * (gso i \<bullet> gso i)) idx = map (\<lambda> i. hh i * hh i * (gso i \<bullet> gso i)) [0..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. nu i * nu i * (gso i \<bullet> gso i)) idx = map (\<lambda>i. hh i * hh i * (gso i \<bullet> gso i)) [0..<k]
[PROOF STEP]
unfolding idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. nu i * nu i * (gso i \<bullet> gso i)) [0..<k] = map (\<lambda>i. hh i * hh i * (gso i \<bullet> gso i)) [0..<k]
[PROOF STEP]
by (rule map_cong, auto simp: hh_def)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. nu i * nu i * (gso i \<bullet> gso i)) idx = map (\<lambda>i. hh i * hh i * (gso i \<bullet> gso i)) [0..<k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. nu i * nu i * (gso i \<bullet> gso i)) idx = map (\<lambda>i. hh i * hh i * (gso i \<bullet> gso i)) [0..<k]

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "of_int (l * l) = hh k * hh k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (l * l) = hh k * hh k
[PROOF STEP]
unfolding hh_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (l * l) = (if k < k then nu k else of_int l) * (if k < k then nu k else of_int l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_int (l * l) = hh k * hh k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_int (l * l) = hh k * hh k

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "(\<Sum>i\<leftarrow>[0..<k]. hh i * hh i * (gso i \<bullet> gso i)) + hh k * hh k * (gso k \<bullet> gso k)
     = (\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<k]. hh i * hh i * (gso i \<bullet> gso i)) + hh k * hh k * (gso k \<bullet> gso k) = (\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<leftarrow>[0..<k]. hh i * hh i * (gso i \<bullet> gso i)) + hh k * hh k * (gso k \<bullet> gso k) = (\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i))

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<leftarrow>[0..<k]. hh i * hh i * (gso i \<bullet> gso i)) + hh k * hh k * (gso k \<bullet> gso k) = (\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i))

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = ?hh \<bullet> ?hh"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i)) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k])
[PROOF STEP]
by (rule sym, rule scalar_prod_lincomb_gso, insert kn assms, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i)) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<leftarrow>[0..<Suc k]. hh i * hh i * (gso i \<bullet> gso i)) = M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k])

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = ?ff \<bullet> ?ff"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k)
[PROOF STEP]
by (simp add: ffhh)
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) \<bullet> M.sumlist (map (\<lambda>i. hh i \<cdot>\<^sub>v gso i) [0..<Suc k]) = (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k)

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> = h \<bullet> h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) = h \<bullet> h
[PROOF STEP]
unfolding h
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) = (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) \<bullet> (M.sumlist (map (\<lambda>i. nu i \<cdot>\<^sub>v gso i) idx) + of_int l \<cdot>\<^sub>v gso k) = h \<bullet> h

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gso k \<bullet> gso k \<le> h \<bullet> h
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gso k \<bullet> gso k \<le> h \<bullet> h

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
using kn
[PROOF STATE]
proof (prove)
using this:
gso k \<bullet> gso k \<le> h \<bullet> h
k < length fs

goal (1 subgoal):
 1. \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
unfolding sq_norm_vec_as_cscalar_prod
[PROOF STATE]
proof (prove)
using this:
gso k \<bullet> gso k \<le> h \<bullet> h
k < length fs

goal (1 subgoal):
 1. \<exists>i<length fs. gso i \<bullet>c gso i \<le> h \<bullet>c h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakly_reduced_imp_short_vector:
  assumes "weakly_reduced \<alpha> m"
    and in_L: "h \<in> lattice_of fs - {0\<^sub>v n}" and \<alpha>_pos:"\<alpha> \<ge> 1"
  shows "fs \<noteq> [] \<and> sq_norm (fs ! 0) \<le> \<alpha>^(m-1) * sq_norm h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
from gram_schmidt_short_vector assms
[PROOF STATE]
proof (chain)
picking this:
?h \<in> lattice_of fs - {0\<^sub>v n} \<Longrightarrow> \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>?h\<parallel>\<^sup>2
weakly_reduced \<alpha> (length fs)
h \<in> lattice_of fs - {0\<^sub>v n}
(1::'a) \<le> \<alpha>
[PROOF STEP]
obtain i where
    i: "i < m" and le: "sq_norm (gso i) \<le> sq_norm h"
[PROOF STATE]
proof (prove)
using this:
?h \<in> lattice_of fs - {0\<^sub>v n} \<Longrightarrow> \<exists>i<length fs. \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>?h\<parallel>\<^sup>2
weakly_reduced \<alpha> (length fs)
h \<in> lattice_of fs - {0\<^sub>v n}
(1::'a) \<le> \<alpha>

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length fs; \<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length fs
\<parallel>gso i\<parallel>\<^sup>2 \<le> \<parallel>h\<parallel>\<^sup>2

goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have small: "sq_norm (fs ! 0) \<le> \<alpha>^i * sq_norm (gso i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length fs

goal (1 subgoal):
 1. \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
proof (induct i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ 0 * \<parallel>gso 0\<parallel>\<^sup>2
 2. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < length fs

goal (2 subgoals):
 1. 0 < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ 0 * \<parallel>gso 0\<parallel>\<^sup>2
 2. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ 0 * \<parallel>gso 0\<parallel>\<^sup>2
[PROOF STEP]
unfolding fs0_gso0[OF 0]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>gso 0\<parallel>\<^sup>2 \<le> \<alpha> ^ 0 * \<parallel>gso 0\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ 0 * \<parallel>gso 0\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
case (Suc i)
[PROOF STATE]
proof (state)
this:
i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2
Suc i < length fs

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
hence "sq_norm (fs ! 0) \<le> \<alpha>^i * sq_norm (gso i)"
[PROOF STATE]
proof (prove)
using this:
i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2
Suc i < length fs

goal (1 subgoal):
 1. \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<le> \<alpha>^i * (\<alpha> * (sq_norm (gso (Suc i))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> ^ i * (\<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2)
[PROOF STEP]
using reduced_gso_E[OF assms(1) le_refl Suc(2)] \<alpha>_pos
[PROOF STATE]
proof (prove)
using this:
\<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2
(1::'a) \<le> \<alpha>

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

goal (1 subgoal):
 1. \<And>i. \<lbrakk>i < length fs \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2; Suc i < length fs\<rbrakk> \<Longrightarrow> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * (\<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * (\<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2)

goal (1 subgoal):
 1. \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
unfolding class_semiring.nat_pow_Suc[of \<alpha> i]
[PROOF STATE]
proof (prove)
using this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * (\<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2)

goal (1 subgoal):
 1. \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<alpha> * \<parallel>gso (Suc i)\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ Suc i * \<parallel>gso (Suc i)\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2

goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
have "\<dots> \<le> \<alpha>^(m-1) * sq_norm h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
by (rule mult_mono[OF power_increasing le], insert i \<alpha>_pos, auto)
[PROOF STATE]
proof (state)
this:
\<alpha> ^ i * \<parallel>gso i\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2

goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2

goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
\<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
i < length fs

goal (1 subgoal):
 1. fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2
[PROOF STEP]
by (cases fs, auto)
[PROOF STATE]
proof (state)
this:
fs \<noteq> [] \<and> \<parallel>fs ! 0\<parallel>\<^sup>2 \<le> \<alpha> ^ (length fs - 1) * \<parallel>h\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sq_norm_pos:
  assumes j: "j < m"
  shows "sq_norm (gso j) > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
from j
[PROOF STATE]
proof (chain)
picking this:
j < length fs
[PROOF STEP]
have jj: "j < m - 0"
[PROOF STATE]
proof (prove)
using this:
j < length fs

goal (1 subgoal):
 1. j < length fs - 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
j < length fs - 0

goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
from orthogonalD[OF orthogonal_gso, unfolded length_map length_upt, OF jj jj] assms
[PROOF STATE]
proof (chain)
picking this:
(map gso [0..<length fs] ! j \<bullet> map gso [0..<length fs] ! j = (0::'a)) = (j \<noteq> j)
j < length fs
[PROOF STEP]
have "sq_norm (gso j) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
(map gso [0..<length fs] ! j \<bullet> map gso [0..<length fs] ! j = (0::'a)) = (j \<noteq> j)
j < length fs

goal (1 subgoal):
 1. \<parallel>gso j\<parallel>\<^sup>2 \<noteq> (0::'a)
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
(map gso [0..<length fs] ! j \<bullet> map gso [0..<length fs] ! j = (0::'a)) = (j \<noteq> j)
j < length fs
j < length fs

goal (1 subgoal):
 1. \<parallel>gso j\<parallel>\<^sup>2 \<noteq> (0::'a)
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
\<parallel>gso j\<parallel>\<^sup>2 \<noteq> (0::'a)

goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<parallel>gso j\<parallel>\<^sup>2 \<noteq> (0::'a)

goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
have "sq_norm (gso j) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> \<parallel>gso j\<parallel>\<^sup>2

goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<parallel>gso j\<parallel>\<^sup>2 \<noteq> (0::'a)
(0::'a) \<le> \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
show "0 < sq_norm (gso j)"
[PROOF STATE]
proof (prove)
using this:
\<parallel>gso j\<parallel>\<^sup>2 \<noteq> (0::'a)
(0::'a) \<le> \<parallel>gso j\<parallel>\<^sup>2

goal (1 subgoal):
 1. (0::'a) < \<parallel>gso j\<parallel>\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) < \<parallel>gso j\<parallel>\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed