[STATEMENT]
lemma lattice_of_add: assumes fs: "set fs \<subseteq> carrier_vec n"
  and ij: "i < length fs" "j < length fs" "i \<noteq> j"
  and gs: "gs = fs[ i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]"
shows "lattice_of gs = lattice_of fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
fix i j l and fs :: "'a vec list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
assume *: "i < j" "j < length fs" and fs: "set fs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (state)
this:
i < j
j < length fs
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
note * = ij(1) *
[PROOF STATE]
proof (state)
this:
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?gs = "fs[ i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?len = "[0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "[0 ..< length fs] = [0 ..< j] @ [j] @ [Suc j ..< length fs]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<length fs] = [0..<j] @ [j] @ [Suc j..<length fs]
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < j
j < length fs

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

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[0..<length fs] = [0..<j] @ [j] @ [Suc j..<length fs]

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "[0 ..< j] = [0 ..< i] @ [i] @ [Suc i ..< j]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<j] = [0..<i] @ [i] @ [Suc i..<j]
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < j
j < length fs

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

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
[0..<length fs] = ([0..<i] @ [i] @ [Suc i..<j]) @ [j] @ [Suc j..<length fs]
[PROOF STEP]
have len: "[0..<length fs] = ?len"
[PROOF STATE]
proof (prove)
using this:
[0..<length fs] = ([0..<i] @ [i] @ [Suc i..<j]) @ [j] @ [Suc j..<length fs]

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

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from fs
[PROOF STATE]
proof (chain)
picking this:
set fs \<subseteq> carrier_vec n
[PROOF STEP]
have fs: "\<And> i. i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n

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

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

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from fs
[PROOF STATE]
proof (chain)
picking this:
?i1 < length fs \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
[PROOF STEP]
have fsd: "\<And> i. i < length fs \<Longrightarrow> dim_vec (fs ! i) = n"
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < length fs \<Longrightarrow> dim_vec (fs ! ?i1) = n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from fsd[of i] fsd[of j] *
[PROOF STATE]
proof (chain)
picking this:
i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
j < length fs \<Longrightarrow> dim_vec (fs ! j) = n
i < length fs
i < j
j < length fs
[PROOF STEP]
have fsd: "dim_vec (fs ! i) = n" "dim_vec (fs ! j) = n"
[PROOF STATE]
proof (prove)
using this:
i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
j < length fs \<Longrightarrow> dim_vec (fs ! j) = n
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. dim_vec (fs ! i) = n &&& dim_vec (fs ! j) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_vec (fs ! i) = n
dim_vec (fs ! j) = n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
dim_vec (fs ! i) = n
dim_vec (fs ! j) = n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
assume "f \<in> lattice_of fs"
[PROOF STATE]
proof (state)
this:
f \<in> lattice_of fs

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from in_latticeE[OF this, unfolded len]
[PROOF STATE]
proof (chain)
picking this:
(\<And>c. f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs])) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain c where
        f: "f = sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) ?len)"
[PROOF STATE]
proof (prove)
using this:
(\<And>c. f = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs])) \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
define sc where "sc = (\<lambda> xs. sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) xs))"
[PROOF STATE]
proof (state)
this:
sc = (\<lambda>xs. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) xs))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
define d where "d = (\<lambda> k. if k = j then c j - c i * l else c k)"
[PROOF STATE]
proof (state)
this:
d = (\<lambda>k. if k = j then c j - c i * l else c k)

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
define sd where "sd = (\<lambda> xs. sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v ?gs ! i) xs))"
[PROOF STATE]
proof (state)
this:
sd = (\<lambda>xs. M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) xs))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have isc: "set is \<subseteq> {0 ..< length fs} \<Longrightarrow> sc is \<in> carrier_vec n" for "is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set is \<subseteq> {0..<length fs} \<Longrightarrow> sc is \<in> carrier_vec n
[PROOF STEP]
unfolding sc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set is \<subseteq> {0..<length fs} \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) is) \<in> carrier_vec n
[PROOF STEP]
by (intro sumlist_carrier, auto simp: fs)
[PROOF STATE]
proof (state)
this:
set ?is1 \<subseteq> {0..<length fs} \<Longrightarrow> sc ?is1 \<in> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have isd: "set is \<subseteq> {0 ..< length fs} \<Longrightarrow> sd is \<in> carrier_vec n" for "is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set is \<subseteq> {0..<length fs} \<Longrightarrow> sd is \<in> carrier_vec n
[PROOF STEP]
unfolding sd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set is \<subseteq> {0..<length fs} \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) is) \<in> carrier_vec n
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. set is \<subseteq> {0..<length fs} \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) is) \<in> carrier_vec n
[PROOF STEP]
by (intro sumlist_carrier, auto, rename_tac k,
        case_tac "k = i", auto simp: fs)
[PROOF STATE]
proof (state)
this:
set ?is1 \<subseteq> {0..<length fs} \<Longrightarrow> sd ?is1 \<in> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?a = "sc [0..<i]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?b = "sc [i]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?c = "sc [Suc i ..< j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?d = "sc [j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?e = "sc [Suc j ..< length fs]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?A = "sd [0..<i]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?B = "sd [i]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?C = "sd [Suc i ..< j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?D = "sd [j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?E = "sd [Suc j ..< length fs]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?CC = "carrier_vec n"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have ae: "?a \<in> ?CC" "?b \<in> ?CC" "?c \<in> ?CC" "?d \<in> ?CC" "?e \<in> ?CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sc [0..<i] \<in> carrier_vec n &&& sc [i] \<in> carrier_vec n) &&& sc [Suc i..<j] \<in> carrier_vec n &&& sc [j] \<in> carrier_vec n &&& sc [Suc j..<length fs] \<in> carrier_vec n
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. (sc [0..<i] \<in> carrier_vec n &&& sc [i] \<in> carrier_vec n) &&& sc [Suc i..<j] \<in> carrier_vec n &&& sc [j] \<in> carrier_vec n &&& sc [Suc j..<length fs] \<in> carrier_vec n
[PROOF STEP]
by (auto intro: isc)
[PROOF STATE]
proof (state)
this:
sc [0..<i] \<in> carrier_vec n
sc [i] \<in> carrier_vec n
sc [Suc i..<j] \<in> carrier_vec n
sc [j] \<in> carrier_vec n
sc [Suc j..<length fs] \<in> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have AE: "?A \<in> ?CC" "?B \<in> ?CC" "?C \<in> ?CC" "?D \<in> ?CC" "?E \<in> ?CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sd [0..<i] \<in> carrier_vec n &&& sd [i] \<in> carrier_vec n) &&& sd [Suc i..<j] \<in> carrier_vec n &&& sd [j] \<in> carrier_vec n &&& sd [Suc j..<length fs] \<in> carrier_vec n
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. (sd [0..<i] \<in> carrier_vec n &&& sd [i] \<in> carrier_vec n) &&& sd [Suc i..<j] \<in> carrier_vec n &&& sd [j] \<in> carrier_vec n &&& sd [Suc j..<length fs] \<in> carrier_vec n
[PROOF STEP]
by (auto intro: isd)
[PROOF STATE]
proof (state)
this:
sd [0..<i] \<in> carrier_vec n
sd [i] \<in> carrier_vec n
sd [Suc i..<j] \<in> carrier_vec n
sd [j] \<in> carrier_vec n
sd [Suc j..<length fs] \<in> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have sc_sd: "{i,j} \<inter> set is \<subseteq> {} \<Longrightarrow> sc is = sd is" for "is"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i, j} \<inter> set is \<subseteq> {} \<Longrightarrow> sc is = sd is
[PROOF STEP]
unfolding sc_def sd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i, j} \<inter> set is \<subseteq> {} \<Longrightarrow> M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) is) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) is)
[PROOF STEP]
by (rule arg_cong[of _ _ sumlist], rule map_cong, auto simp: d_def,
        rename_tac k, case_tac "i = k", auto)
[PROOF STATE]
proof (state)
this:
{i, j} \<inter> set ?is2 \<subseteq> {} \<Longrightarrow> sc ?is2 = sd ?is2

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "f = ?a + (?b + (?c + (?d + ?e)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs])))
[PROOF STEP]
unfolding f map_append sc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<i] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [i] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc i..<j] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [j] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc j..<length fs]) = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<i]) + (M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [i]) + (M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc i..<j]) + (M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [j]) + M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc j..<length fs]))))
[PROOF STEP]
using fs *
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<i] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [i] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc i..<j] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [j] @ map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc j..<length fs]) = M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [0..<i]) + (M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [i]) + (M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc i..<j]) + (M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [j]) + M.sumlist (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [Suc j..<length fs]))))
[PROOF STEP]
by ((subst sumlist_append, force, force)+, simp)
[PROOF STATE]
proof (state)
this:
f = sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs])))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f = sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs])))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "\<dots> = ?a + ((?b + ?d) + (?c + ?e))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs]))) = sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs]))
[PROOF STEP]
using ae
[PROOF STATE]
proof (prove)
using this:
sc [0..<i] \<in> carrier_vec n
sc [i] \<in> carrier_vec n
sc [Suc i..<j] \<in> carrier_vec n
sc [j] \<in> carrier_vec n
sc [Suc j..<length fs] \<in> carrier_vec n

goal (1 subgoal):
 1. sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs]))) = sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs]))) = sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs]))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sc [0..<i] + (sc [i] + (sc [Suc i..<j] + (sc [j] + sc [Suc j..<length fs]))) = sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs]))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "\<dots> = ?A + ((?b + ?d) + (?C + ?E))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs])) = sd [0..<i] + (sc [i] + sc [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs])) = sd [0..<i] + (sc [i] + sc [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))
[PROOF STEP]
by (auto simp: sc_sd)
[PROOF STATE]
proof (state)
this:
sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs])) = sd [0..<i] + (sc [i] + sc [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sc [0..<i] + (sc [i] + sc [j] + (sc [Suc i..<j] + sc [Suc j..<length fs])) = sd [0..<i] + (sc [i] + sc [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "?b + ?d = ?B + ?D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sc [i] + sc [j] = sd [i] + sd [j]
[PROOF STEP]
unfolding sd_def sc_def d_def sumlist_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldr (+) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [i]) (0\<^sub>v n) + foldr (+) (map (\<lambda>i. of_int (c i) \<cdot>\<^sub>v fs ! i) [j]) (0\<^sub>v n) = foldr (+) (map (\<lambda>i. of_int (if i = j then c j - c i * l else c i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [i]) (0\<^sub>v n) + foldr (+) (map (\<lambda>i. of_int (if i = j then c j - c i * l else c i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [j]) (0\<^sub>v n)
[PROOF STEP]
by (rule eq_vecI, insert * fsd, auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
sc [i] + sc [j] = sd [i] + sd [j]

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f = sd [0..<i] + (sd [i] + sd [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))
[PROOF STEP]
have "f = ?A + (?B + (?C + (?D + ?E)))"
[PROOF STATE]
proof (prove)
using this:
f = sd [0..<i] + (sd [i] + sd [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))

goal (1 subgoal):
 1. f = sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs])))
[PROOF STEP]
using AE
[PROOF STATE]
proof (prove)
using this:
f = sd [0..<i] + (sd [i] + sd [j] + (sd [Suc i..<j] + sd [Suc j..<length fs]))
sd [0..<i] \<in> carrier_vec n
sd [i] \<in> carrier_vec n
sd [Suc i..<j] \<in> carrier_vec n
sd [j] \<in> carrier_vec n
sd [Suc j..<length fs] \<in> carrier_vec n

goal (1 subgoal):
 1. f = sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs])))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f = sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs])))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f = sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs])))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "\<dots> = sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v ?gs ! i) ?len)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs]))) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs]))
[PROOF STEP]
unfolding f map_append sd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<i]) + (M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [i]) + (M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc i..<j]) + (M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [j]) + M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc j..<length fs])))) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<i] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [i] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc i..<j] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [j] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc j..<length fs])
[PROOF STEP]
using fs *
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
i < length fs
i < j
j < length fs

goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<i]) + (M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [i]) + (M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc i..<j]) + (M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [j]) + M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc j..<length fs])))) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<i] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [i] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc i..<j] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [j] @ map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [Suc j..<length fs])
[PROOF STEP]
by ((subst sumlist_append, force, force)+, simp)
[PROOF STATE]
proof (state)
this:
sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs]))) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs]))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sd [0..<i] + (sd [i] + (sd [Suc i..<j] + (sd [j] + sd [Suc j..<length fs]))) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs]))

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "\<dots> = sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v ?gs ! i) [0 ..< length ?gs])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs])) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])
[PROOF STEP]
unfolding len[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length fs]) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) ([0..<i] @ [i] @ [Suc i..<j] @ [j] @ [Suc j..<length fs])) = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])
[PROOF STEP]
have "f = sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v ?gs ! i) [0 ..< length ?gs])"
[PROOF STATE]
proof (prove)
using this:
f = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])

goal (1 subgoal):
 1. f = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f = M.sumlist (map (\<lambda>i. of_int (d i) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i) [0..<length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from in_latticeI[OF this]
[PROOF STATE]
proof (chain)
picking this:
f \<in> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
have "f \<in> lattice_of ?gs"
[PROOF STATE]
proof (prove)
using this:
f \<in> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. f \<in> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f \<in> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?f3 \<in> lattice_of fs \<Longrightarrow> ?f3 \<in> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
hence "lattice_of fs \<subseteq> lattice_of ?gs"
[PROOF STATE]
proof (prove)
using this:
?f3 \<in> lattice_of fs \<Longrightarrow> ?f3 \<in> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of fs \<subseteq> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
lattice_of fs \<subseteq> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ia3 < ?ja3; ?ja3 < length ?fsa3; set ?fsa3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lattice_of ?fsa3 \<subseteq> lattice_of (?fsa3[?ia3 := ?fsa3 ! ?ia3 + of_int ?la3 \<cdot>\<^sub>v ?fsa3 ! ?ja3])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ia3 < ?ja3; ?ja3 < length ?fsa3; set ?fsa3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lattice_of ?fsa3 \<subseteq> lattice_of (?fsa3[?ia3 := ?fsa3 ! ?ia3 + of_int ?la3 \<cdot>\<^sub>v ?fsa3 ! ?ja3])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ia3 < ?ja3; ?ja3 < length ?fsa3; set ?fsa3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lattice_of ?fsa3 \<subseteq> lattice_of (?fsa3[?ia3 := ?fsa3 ! ?ia3 + of_int ?la3 \<cdot>\<^sub>v ?fsa3 ! ?ja3])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
fix i j and fs :: "'a vec list"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
assume *: "i < j" "j < length fs" and fs: "set fs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (state)
this:
i < j
j < length fs
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
let ?gs = "fs[ i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
define gs where "gs = ?gs"
[PROOF STATE]
proof (state)
this:
gs = fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from main[OF * fs, of l, folded gs_def]
[PROOF STATE]
proof (chain)
picking this:
lattice_of fs \<subseteq> lattice_of gs
[PROOF STEP]
have one: "lattice_of fs \<subseteq> lattice_of gs"
[PROOF STATE]
proof (prove)
using this:
lattice_of fs \<subseteq> lattice_of gs

goal (1 subgoal):
 1. lattice_of fs \<subseteq> lattice_of gs
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lattice_of fs \<subseteq> lattice_of gs

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have *: "i < j" "j < length gs" "set gs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < j &&& j < length gs &&& set gs \<subseteq> carrier_vec n
[PROOF STEP]
using * fs
[PROOF STATE]
proof (prove)
using this:
i < j
j < length fs
set fs \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. i < j &&& j < length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]) &&& {fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i |i. i < length (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])} \<subseteq> carrier_vec n
[PROOF STEP]
by (auto, rename_tac k, case_tac "k = i", (force intro!: add_carrier_vec)+)
[PROOF STATE]
proof (state)
this:
i < j
j < length gs
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from fs
[PROOF STATE]
proof (chain)
picking this:
set fs \<subseteq> carrier_vec n
[PROOF STEP]
have fs: "\<And> i. i < length fs \<Longrightarrow> fs ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n

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

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

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from fs
[PROOF STATE]
proof (chain)
picking this:
?i1 < length fs \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n
[PROOF STEP]
have fsd: "\<And> i. i < length fs \<Longrightarrow> dim_vec (fs ! i) = n"
[PROOF STATE]
proof (prove)
using this:
?i1 < length fs \<Longrightarrow> fs ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>i. i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i1 < length fs \<Longrightarrow> dim_vec (fs ! ?i1) = n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from fsd[of i] fsd[of j] *
[PROOF STATE]
proof (chain)
picking this:
i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
j < length fs \<Longrightarrow> dim_vec (fs ! j) = n
i < j
j < length gs
set gs \<subseteq> carrier_vec n
[PROOF STEP]
have fsd: "dim_vec (fs ! i) = n" "dim_vec (fs ! j) = n"
[PROOF STATE]
proof (prove)
using this:
i < length fs \<Longrightarrow> dim_vec (fs ! i) = n
j < length fs \<Longrightarrow> dim_vec (fs ! j) = n
i < j
j < length gs
set gs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. dim_vec (fs ! i) = n &&& dim_vec (fs ! j) = n
[PROOF STEP]
by (auto simp: gs_def)
[PROOF STATE]
proof (state)
this:
dim_vec (fs ! i) = n
dim_vec (fs ! j) = n

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
from main[OF *, of "-l"]
[PROOF STATE]
proof (chain)
picking this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])
[PROOF STEP]
have "lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])"
[PROOF STATE]
proof (prove)
using this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])

goal (1 subgoal):
 1. lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
have "gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j] = fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j] = fs
[PROOF STEP]
unfolding gs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j, i := fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i + of_int (- l) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! j] = fs
[PROOF STEP]
by (rule nth_equalityI, auto, insert * fsd, rename_tac k, case_tac "k = i", auto)
[PROOF STATE]
proof (state)
this:
gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j] = fs

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])
gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j] = fs
[PROOF STEP]
have "lattice_of fs = lattice_of ?gs"
[PROOF STATE]
proof (prove)
using this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])
gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j] = fs

goal (1 subgoal):
 1. lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
using one
[PROOF STATE]
proof (prove)
using this:
lattice_of gs \<subseteq> lattice_of (gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j])
gs[i := gs ! i + of_int (- l) \<cdot>\<^sub>v gs ! j] = fs
lattice_of fs \<subseteq> lattice_of gs

goal (1 subgoal):
 1. lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
unfolding gs_def
[PROOF STATE]
proof (prove)
using this:
lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]) \<subseteq> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j, i := fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i + of_int (- l) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! j])
fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j, i := fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! i + of_int (- l) \<cdot>\<^sub>v fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j] ! j] = fs
lattice_of fs \<subseteq> lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ia3 < ?ja3; ?ja3 < length ?fsa3; set ?fsa3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lattice_of ?fsa3 = lattice_of (?fsa3[?ia3 := ?fsa3 ! ?ia3 + of_int l \<cdot>\<^sub>v ?fsa3 ! ?ja3])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
note main = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?ia3 < ?ja3; ?ja3 < length ?fsa3; set ?fsa3 \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lattice_of ?fsa3 = lattice_of (?fsa3[?ia3 := ?fsa3 ! ?ia3 + of_int l \<cdot>\<^sub>v ?fsa3 ! ?ja3])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
proof (cases "i < j")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < j \<Longrightarrow> lattice_of gs = lattice_of fs
 2. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < j

goal (2 subgoals):
 1. i < j \<Longrightarrow> lattice_of gs = lattice_of fs
 2. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
from main[OF this ij(2) fs]
[PROOF STATE]
proof (chain)
picking this:
lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of gs = lattice_of fs
[PROOF STEP]
unfolding gs
[PROOF STATE]
proof (prove)
using this:
lattice_of fs = lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j])

goal (1 subgoal):
 1. lattice_of (fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]) = lattice_of fs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lattice_of gs = lattice_of fs

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
with ij
[PROOF STATE]
proof (chain)
picking this:
i < length fs
j < length fs
i \<noteq> j
\<not> i < j
[PROOF STEP]
have ji: "j < i"
[PROOF STATE]
proof (prove)
using this:
i < length fs
j < length fs
i \<noteq> j
\<not> i < j

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

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
define hs where "hs = fs[i := fs ! j, j := fs ! i]"
[PROOF STATE]
proof (state)
this:
hs = fs[i := fs ! j, j := fs ! i]

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
define ks where "ks = hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i]"
[PROOF STATE]
proof (state)
this:
ks = hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i]

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
from ij fs
[PROOF STATE]
proof (chain)
picking this:
i < length fs
j < length fs
i \<noteq> j
set fs \<subseteq> carrier_vec n
[PROOF STEP]
have ij': "i < length hs" "set hs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
i < length fs
j < length fs
i \<noteq> j
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. i < length hs &&& set hs \<subseteq> carrier_vec n
[PROOF STEP]
unfolding hs_def
[PROOF STATE]
proof (prove)
using this:
i < length fs
j < length fs
i \<noteq> j
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. i < length (fs[i := fs ! j, j := fs ! i]) &&& set (fs[i := fs ! j, j := fs ! i]) \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length hs
set hs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
hence ij'': "set ks \<subseteq> carrier_vec n" "i < length ks" "j < length ks" "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
i < length hs
set hs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. (set ks \<subseteq> carrier_vec n &&& i < length ks) &&& j < length ks &&& i \<noteq> j
[PROOF STEP]
using ji
[PROOF STATE]
proof (prove)
using this:
i < length hs
set hs \<subseteq> carrier_vec n
j < i

goal (1 subgoal):
 1. (set ks \<subseteq> carrier_vec n &&& i < length ks) &&& j < length ks &&& i \<noteq> j
[PROOF STEP]
unfolding ks_def set_conv_nth
[PROOF STATE]
proof (prove)
using this:
i < length hs
{hs ! i |i. i < length hs} \<subseteq> carrier_vec n
j < i

goal (1 subgoal):
 1. ({hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i] ! ia |ia. ia < length (hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i])} \<subseteq> carrier_vec n &&& i < length (hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i])) &&& j < length (hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i]) &&& i \<noteq> j
[PROOF STEP]
by (auto, rename_tac k, case_tac "k = i",
        force, case_tac "k = j", (force intro!: add_carrier_vec)+)
[PROOF STATE]
proof (state)
this:
set ks \<subseteq> carrier_vec n
i < length ks
j < length ks
i \<noteq> j

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
from lattice_of_swap[OF fs ij refl]
[PROOF STATE]
proof (chain)
picking this:
lattice_of (fs[i := fs ! j, j := fs ! i]) = lattice_of fs
[PROOF STEP]
have "lattice_of fs = lattice_of hs"
[PROOF STATE]
proof (prove)
using this:
lattice_of (fs[i := fs ! j, j := fs ! i]) = lattice_of fs

goal (1 subgoal):
 1. lattice_of fs = lattice_of hs
[PROOF STEP]
unfolding hs_def
[PROOF STATE]
proof (prove)
using this:
lattice_of (fs[i := fs ! j, j := fs ! i]) = lattice_of fs

goal (1 subgoal):
 1. lattice_of fs = lattice_of (fs[i := fs ! j, j := fs ! i])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lattice_of fs = lattice_of hs

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lattice_of fs = lattice_of hs

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
have "\<dots> = lattice_of ks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of hs = lattice_of ks
[PROOF STEP]
using main[OF ji ij']
[PROOF STATE]
proof (prove)
using this:
lattice_of hs = lattice_of (hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i])

goal (1 subgoal):
 1. lattice_of hs = lattice_of ks
[PROOF STEP]
unfolding ks_def
[PROOF STATE]
proof (prove)
using this:
lattice_of hs = lattice_of (hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i])

goal (1 subgoal):
 1. lattice_of hs = lattice_of (hs[j := hs ! j + of_int l \<cdot>\<^sub>v hs ! i])
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lattice_of hs = lattice_of ks

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lattice_of hs = lattice_of ks

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
have "\<dots> = lattice_of (ks[i := ks ! j, j := ks ! i])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lattice_of ks = lattice_of (ks[i := ks ! j, j := ks ! i])
[PROOF STEP]
by (rule sym, rule lattice_of_swap[OF ij'' refl])
[PROOF STATE]
proof (state)
this:
lattice_of ks = lattice_of (ks[i := ks ! j, j := ks ! i])

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lattice_of ks = lattice_of (ks[i := ks ! j, j := ks ! i])

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
have "ks[i := ks ! j, j := ks ! i] = gs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ks[i := ks ! j, j := ks ! i] = gs
[PROOF STEP]
unfolding gs ks_def hs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fs[i := fs ! j, j := fs ! i, j := fs[i := fs ! j, j := fs ! i] ! j + of_int l \<cdot>\<^sub>v fs[i := fs ! j, j := fs ! i] ! i, i := fs[i := fs ! j, j := fs ! i, j := fs[i := fs ! j, j := fs ! i] ! j + of_int l \<cdot>\<^sub>v fs[i := fs ! j, j := fs ! i] ! i] ! j, j := fs[i := fs ! j, j := fs ! i, j := fs[i := fs ! j, j := fs ! i] ! j + of_int l \<cdot>\<^sub>v fs[i := fs ! j, j := fs ! i] ! i] ! i] = fs[i := fs ! i + of_int l \<cdot>\<^sub>v fs ! j]
[PROOF STEP]
by (rule nth_equalityI, insert ij, auto,
       rename_tac k, case_tac "k = i", force, case_tac "k = j", auto)
[PROOF STATE]
proof (state)
this:
ks[i := ks ! j, j := ks ! i] = gs

goal (1 subgoal):
 1. \<not> i < j \<Longrightarrow> lattice_of gs = lattice_of fs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lattice_of fs = lattice_of gs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lattice_of fs = lattice_of gs

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lattice_of gs = lattice_of fs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma orthogonal_complement_subset:
  assumes "A \<subseteq> B"
  shows "orthogonal_complement B \<subseteq> orthogonal_complement A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal_complement B \<subseteq> orthogonal_complement A
[PROOF STEP]
unfolding orthogonal_complement_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier_vec n. \<forall>y\<in>B. x \<bullet> y = (0::'b)} \<subseteq> {x \<in> carrier_vec n. \<forall>y\<in>A. x \<bullet> y = (0::'b)}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B

goal (1 subgoal):
 1. {x \<in> carrier_vec n. \<forall>y\<in>B. x \<bullet> y = (0::'b)} \<subseteq> {x \<in> carrier_vec n. \<forall>y\<in>A. x \<bullet> y = (0::'b)}
[PROOF STEP]
by auto


[STATEMENT]
lemma in_orthogonal_complement_span[simp]:
  assumes [intro]:"S \<subseteq> carrier_vec n"
  shows "orthogonal_complement (span S) = orthogonal_complement S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal_complement (local.span S) = orthogonal_complement S
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. orthogonal_complement (local.span S) \<subseteq> orthogonal_complement S
 2. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
show "orthogonal_complement (span S) \<subseteq> orthogonal_complement S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. orthogonal_complement (local.span S) \<subseteq> orthogonal_complement S
[PROOF STEP]
by(fact orthogonal_complement_subset[OF in_own_span[OF assms]])
[PROOF STATE]
proof (state)
this:
orthogonal_complement (local.span S) \<subseteq> orthogonal_complement S

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
orthogonal_complement (local.span S) \<subseteq> orthogonal_complement S

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
fix x :: "'a vec"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
fix A :: "'a vec set"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
assume x [intro]:"x \<in> carrier_vec n" and f: "finite A" and S:"A \<subseteq> S"
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec n
finite A
A \<subseteq> S

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
assume i0:"\<forall>y\<in>S. x \<bullet> y = 0"
[PROOF STATE]
proof (state)
this:
\<forall>y\<in>S. x \<bullet> y = (0::'a)

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
have "x \<bullet> lincomb a A = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<bullet> lincomb a A = (0::'a)
[PROOF STEP]
unfolding comm_scalar_prod[OF x lincomb_closed[OF subset_trans[OF S assms]]]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a A \<bullet> x = (0::'a)
[PROOF STEP]
proof(insert S,atomize(full),rule finite_induct[OF f],goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<subseteq> S \<longrightarrow> lincomb a {} \<bullet> x = (0::'a)
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. {} \<subseteq> S \<longrightarrow> lincomb a {} \<bullet> x = (0::'a)
 2. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {} \<subseteq> S \<longrightarrow> lincomb a {} \<bullet> x = (0::'a)
[PROOF STEP]
using assms x
[PROOF STATE]
proof (prove)
using this:
S \<subseteq> carrier_vec n
x \<in> carrier_vec n

goal (1 subgoal):
 1. {} \<subseteq> S \<longrightarrow> lincomb a {} \<bullet> x = (0::'a)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{} \<subseteq> S \<longrightarrow> lincomb a {} \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
case (2 f F)
[PROOF STATE]
proof (state)
this:
finite F
f \<notin> F
F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
finite F
f \<notin> F
F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
assume i:"insert f F \<subseteq> S"
[PROOF STATE]
proof (state)
this:
insert f F \<subseteq> S

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
hence F:"F \<subseteq> S" and f: "f \<in> S"
[PROOF STATE]
proof (prove)
using this:
insert f F \<subseteq> S

goal (1 subgoal):
 1. F \<subseteq> S &&& f \<in> S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F \<subseteq> S
f \<in> S

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
from F f assms
[PROOF STATE]
proof (chain)
picking this:
F \<subseteq> S
f \<in> S
S \<subseteq> carrier_vec n
[PROOF STEP]
have [intro]:"F \<subseteq> carrier_vec n"
          and fc[intro]:"f \<in> carrier_vec n"
          and [intro]:"x \<in> F \<Longrightarrow> x \<in> carrier_vec n" for x
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> S
f \<in> S
S \<subseteq> carrier_vec n

goal (1 subgoal):
 1. F \<subseteq> carrier_vec n &&& f \<in> carrier_vec n &&& (x \<in> F \<Longrightarrow> x \<in> carrier_vec n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
F \<subseteq> carrier_vec n
f \<in> carrier_vec n
?x1 \<in> F \<Longrightarrow> ?x1 \<in> carrier_vec n

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
have laf:"lincomb a F \<bullet> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb a F \<bullet> x = (0::'a)
[PROOF STEP]
using F 2
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> S
finite F
f \<notin> F
F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)

goal (1 subgoal):
 1. lincomb a F \<bullet> x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a F \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
have [simp]:"(\<Sum>u\<in>F. (a u \<cdot>\<^sub>v u) \<bullet> x) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>u\<in>F. (a u \<cdot>\<^sub>v u) \<bullet> x) = (0::'a)
[PROOF STEP]
by(insert laf[unfolded lincomb_def],atomize(full),subst finsum_scalar_prod_sum) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>u\<in>F. (a u \<cdot>\<^sub>v u) \<bullet> x) = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
from f i0
[PROOF STATE]
proof (chain)
picking this:
f \<in> S
\<forall>y\<in>S. x \<bullet> y = (0::'a)
[PROOF STEP]
have [simp]:"f \<bullet> x = 0"
[PROOF STATE]
proof (prove)
using this:
f \<in> S
\<forall>y\<in>S. x \<bullet> y = (0::'a)

goal (1 subgoal):
 1. f \<bullet> x = (0::'a)
[PROOF STEP]
by (subst comm_scalar_prod) auto
[PROOF STATE]
proof (state)
this:
f \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
from lincomb_closed[OF subset_trans[OF i assms]]
[PROOF STATE]
proof (chain)
picking this:
lincomb ?a (insert f F) \<in> carrier_vec n
[PROOF STEP]
have "lincomb a (insert f F) \<bullet> x = 0"
[PROOF STATE]
proof (prove)
using this:
lincomb ?a (insert f F) \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb a (insert f F) \<bullet> x = (0::'a)
[PROOF STEP]
unfolding lincomb_def
[PROOF STATE]
proof (prove)
using this:
(\<Oplus>\<^bsub>V\<^esub>v\<in>insert f F. ?a v \<cdot>\<^sub>v v) \<in> carrier_vec n

goal (1 subgoal):
 1. (\<Oplus>\<^bsub>V\<^esub>v\<in>insert f F. a v \<cdot>\<^sub>v v) \<bullet> x = (0::'a)
[PROOF STEP]
apply(subst finsum_scalar_prod_sum,force,force)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a. (\<Oplus>\<^bsub>V\<^esub>v\<in>insert f F. a v \<cdot>\<^sub>v v) \<in> carrier_vec n) \<Longrightarrow> (\<Sum>u\<in>insert f F. (a u \<cdot>\<^sub>v u) \<bullet> x) = (0::'a)
[PROOF STEP]
using 2(1,2) smult_scalar_prod_distrib[OF fc x]
[PROOF STATE]
proof (prove)
using this:
finite F
f \<notin> F
(?a \<cdot>\<^sub>v f) \<bullet> x = ?a * (f \<bullet> x)

goal (1 subgoal):
 1. (\<And>a. (\<Oplus>\<^bsub>V\<^esub>v\<in>insert f F. a v \<cdot>\<^sub>v v) \<in> carrier_vec n) \<Longrightarrow> (\<Sum>u\<in>insert f F. (a u \<cdot>\<^sub>v u) \<bullet> x) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a (insert f F) \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
insert f F \<subseteq> S \<Longrightarrow> lincomb a (insert f F) \<bullet> x = (0::'a)

goal (1 subgoal):
 1. \<And>xa F. \<lbrakk>finite F; xa \<notin> F; F \<subseteq> S \<longrightarrow> lincomb a F \<bullet> x = (0::'a)\<rbrakk> \<Longrightarrow> insert xa F \<subseteq> S \<longrightarrow> lincomb a (insert xa F) \<bullet> x = (0::'a)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
insert f F \<subseteq> S \<Longrightarrow> lincomb a (insert f F) \<bullet> x = (0::'a)

goal (1 subgoal):
 1. insert f F \<subseteq> S \<longrightarrow> lincomb a (insert f F) \<bullet> x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert f F \<subseteq> S \<longrightarrow> lincomb a (insert f F) \<bullet> x = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<bullet> lincomb a A = (0::'a)

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> carrier_vec n; finite ?A3; ?A3 \<subseteq> S; \<forall>y\<in>S. ?x3 \<bullet> y = (0::'a)\<rbrakk> \<Longrightarrow> ?x3 \<bullet> lincomb ?a3 ?A3 = (0::'a)

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
thus "orthogonal_complement S \<subseteq> orthogonal_complement (span S)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 \<in> carrier_vec n; finite ?A3; ?A3 \<subseteq> S; \<forall>y\<in>S. ?x3 \<bullet> y = (0::'a)\<rbrakk> \<Longrightarrow> ?x3 \<bullet> lincomb ?a3 ?A3 = (0::'a)

goal (1 subgoal):
 1. orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)
[PROOF STEP]
unfolding orthogonal_complement_def span_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x3 \<in> carrier_vec n; finite ?A3; ?A3 \<subseteq> S; \<forall>y\<in>S. ?x3 \<bullet> y = (0::'a)\<rbrakk> \<Longrightarrow> ?x3 \<bullet> lincomb ?a3 ?A3 = (0::'a)

goal (1 subgoal):
 1. {x \<in> carrier_vec n. \<forall>y\<in>S. x \<bullet> y = (0::'a)} \<subseteq> {x \<in> carrier_vec n. \<forall>y\<in>{lincomb a A |a A. finite A \<and> A \<subseteq> S}. x \<bullet> y = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
orthogonal_complement S \<subseteq> orthogonal_complement (local.span S)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma upper_triangular_imp_lin_indpt_list:
  assumes A: "A \<in> carrier_mat n n"
    and tri: "upper_triangular A"
    and diag: "0 \<notin> set (diag_mat A)"
  shows "lin_indpt_list (rows A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list (rows A)
[PROOF STEP]
using upper_triangular_imp_distinct[OF assms]
[PROOF STATE]
proof (prove)
using this:
distinct (rows A)

goal (1 subgoal):
 1. lin_indpt_list (rows A)
[PROOF STEP]
using upper_triangular_imp_lin_indpt_rows[OF assms] A
[PROOF STATE]
proof (prove)
using this:
distinct (rows A)
lin_indpt (set (rows A))
A \<in> carrier_mat n n

goal (1 subgoal):
 1. lin_indpt_list (rows A)
[PROOF STEP]
unfolding lin_indpt_list_def
[PROOF STATE]
proof (prove)
using this:
distinct (rows A)
lin_indpt (set (rows A))
A \<in> carrier_mat n n

goal (1 subgoal):
 1. set (rows A) \<subseteq> carrier_vec n \<and> distinct (rows A) \<and> lin_indpt (set (rows A))
[PROOF STEP]
by (auto simp: rows_def)


[STATEMENT]
lemma basis_list_basis: assumes "basis_list fs"
  shows "distinct fs" "lin_indpt (set fs)" "basis (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct fs &&& lin_indpt (set fs) &&& basis (set fs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. distinct fs
 2. lin_indpt (set fs)
 3. basis (set fs)
[PROOF STEP]
from assms[unfolded basis_list_def]
[PROOF STATE]
proof (chain)
picking this:
set fs \<subseteq> carrier_vec n \<and> length fs = n \<and> carrier_vec n \<subseteq> local.span (set fs)
[PROOF STEP]
have len: "length fs = n" and C: "set fs \<subseteq> carrier_vec n"
    and span: "carrier_vec n \<subseteq> span (set fs)"
[PROOF STATE]
proof (prove)
using this:
set fs \<subseteq> carrier_vec n \<and> length fs = n \<and> carrier_vec n \<subseteq> local.span (set fs)

goal (1 subgoal):
 1. length fs = n &&& set fs \<subseteq> carrier_vec n &&& carrier_vec n \<subseteq> local.span (set fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length fs = n
set fs \<subseteq> carrier_vec n
carrier_vec n \<subseteq> local.span (set fs)

goal (3 subgoals):
 1. distinct fs
 2. lin_indpt (set fs)
 3. basis (set fs)
[PROOF STEP]
show b: "basis (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. basis (set fs)
[PROOF STEP]
proof (rule dim_gen_is_basis[OF finite_set C])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.span (set fs) = carrier_vec n
 2. card (set fs) \<le> local.dim
[PROOF STEP]
show "card (set fs) \<le> dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set fs) \<le> local.dim
[PROOF STEP]
unfolding dim_is_n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set fs) \<le> n
[PROOF STEP]
unfolding len[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set fs) \<le> length fs
[PROOF STEP]
by (rule card_length)
[PROOF STATE]
proof (state)
this:
card (set fs) \<le> local.dim

goal (1 subgoal):
 1. local.span (set fs) = carrier_vec n
[PROOF STEP]
show "span (set fs) = carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span (set fs) = carrier_vec n
[PROOF STEP]
using span C
[PROOF STATE]
proof (prove)
using this:
carrier_vec n \<subseteq> local.span (set fs)
set fs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. local.span (set fs) = carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span (set fs) = carrier_vec n

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

goal (2 subgoals):
 1. distinct fs
 2. lin_indpt (set fs)
[PROOF STEP]
thus "lin_indpt (set fs)"
[PROOF STATE]
proof (prove)
using this:
basis (set fs)

goal (1 subgoal):
 1. lin_indpt (set fs)
[PROOF STEP]
unfolding basis_def
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set fs) \<and> local.span (set fs) = carrier_vec n \<and> set fs \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. distinct fs
[PROOF STEP]
show "distinct fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct fs
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
assume "\<not> distinct fs"
[PROOF STATE]
proof (state)
this:
\<not> distinct fs

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
hence "card (set fs) < length fs"
[PROOF STATE]
proof (prove)
using this:
\<not> distinct fs

goal (1 subgoal):
 1. card (set fs) < length fs
[PROOF STEP]
using antisym_conv1 card_distinct card_length
[PROOF STATE]
proof (prove)
using this:
\<not> distinct fs
\<not> ?x < ?y \<Longrightarrow> (?x \<le> ?y) = (?x = ?y)
card (set ?xs) = length ?xs \<Longrightarrow> distinct ?xs
card (set ?xs) \<le> length ?xs

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

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (set fs) < length fs

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = dim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length fs = local.dim
[PROOF STEP]
unfolding len dim_is_n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = n
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
length fs = local.dim

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (set fs) < local.dim
[PROOF STEP]
have "card (set fs) < dim"
[PROOF STATE]
proof (prove)
using this:
card (set fs) < local.dim

goal (1 subgoal):
 1. card (set fs) < local.dim
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (set fs) < local.dim

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card (set fs) < local.dim

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> card (set fs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.dim \<le> card (set fs)
[PROOF STEP]
using span finite_set[of fs]
[PROOF STATE]
proof (prove)
using this:
carrier_vec n \<subseteq> local.span (set fs)
finite (set fs)

goal (1 subgoal):
 1. local.dim \<le> card (set fs)
[PROOF STEP]
using b basis_def gen_ge_dim
[PROOF STATE]
proof (prove)
using this:
carrier_vec n \<subseteq> local.span (set fs)
finite (set fs)
basis (set fs)
basis ?A = (lin_indpt ?A \<and> local.span ?A = carrier_vec n \<and> ?A \<subseteq> carrier_vec n)
\<lbrakk>finite ?A; ?A \<subseteq> carrier_vec n; local.span ?A = carrier_vec n\<rbrakk> \<Longrightarrow> local.dim \<le> card ?A

goal (1 subgoal):
 1. local.dim \<le> card (set fs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.dim \<le> card (set fs)

goal (1 subgoal):
 1. \<not> distinct fs \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
card (set fs) < card (set fs)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
card (set fs) < card (set fs)

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma basis_list_imp_lin_indpt_list: assumes "basis_list fs" shows "lin_indpt_list fs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list fs
[PROOF STEP]
using basis_list_basis[OF assms] assms
[PROOF STATE]
proof (prove)
using this:
distinct fs
lin_indpt (set fs)
basis (set fs)
basis_list fs

goal (1 subgoal):
 1. lin_indpt_list fs
[PROOF STEP]
unfolding lin_indpt_list_def basis_list_def
[PROOF STATE]
proof (prove)
using this:
distinct fs
lin_indpt (set fs)
basis (set fs)
set fs \<subseteq> carrier_vec n \<and> length fs = n \<and> carrier_vec n \<subseteq> local.span (set fs)

goal (1 subgoal):
 1. set fs \<subseteq> carrier_vec n \<and> distinct fs \<and> lin_indpt (set fs)
[PROOF STEP]
by auto


[STATEMENT]
lemma basis_det_nonzero:
  assumes db:"basis (set G)" and len:"length G = n"
  shows "det (mat_of_rows n G) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
have M_car1:"mat_of_rows n G \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_rows n G \<in> carrier_mat n n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
basis (set G)
length G = n

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

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
hence M_car:"(mat_of_rows n G)\<^sup>T \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
mat_of_rows n G \<in> carrier_mat n n

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

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
have li:"lin_indpt (set G)"
   and inc_2:"set G \<subseteq> carrier_vec n"
   and issp:"carrier_vec n = span (set G)"
   and RG_in_carr:"\<And>i. i < length G \<Longrightarrow> G ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lin_indpt (set G) &&& set G \<subseteq> carrier_vec n) &&& carrier_vec n = local.span (set G) &&& (\<And>i. i < length G \<Longrightarrow> G ! i \<in> carrier_vec n)
[PROOF STEP]
using assms[unfolded basis_def]
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set G) \<and> local.span (set G) = carrier_vec n \<and> set G \<subseteq> carrier_vec n
length G = n

goal (1 subgoal):
 1. (lin_indpt (set G) &&& set G \<subseteq> carrier_vec n) &&& carrier_vec n = local.span (set G) &&& (\<And>i. i < length G \<Longrightarrow> G ! i \<in> carrier_vec n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (set G)
set G \<subseteq> carrier_vec n
carrier_vec n = local.span (set G)
?i1 < length G \<Longrightarrow> G ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
hence "basis_list G"
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set G)
set G \<subseteq> carrier_vec n
carrier_vec n = local.span (set G)
?i1 < length G \<Longrightarrow> G ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. basis_list G
[PROOF STEP]
unfolding basis_list_def
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set G)
set G \<subseteq> carrier_vec n
carrier_vec n = local.span (set G)
?i1 < length G \<Longrightarrow> G ! ?i1 \<in> carrier_vec n

goal (1 subgoal):
 1. set G \<subseteq> carrier_vec n \<and> length G = n \<and> carrier_vec n \<subseteq> local.span (set G)
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set G)
set G \<subseteq> carrier_vec n
carrier_vec n = local.span (set G)
?i1 < length G \<Longrightarrow> G ! ?i1 \<in> carrier_vec n
length G = n

goal (1 subgoal):
 1. set G \<subseteq> carrier_vec n \<and> length G = n \<and> carrier_vec n \<subseteq> local.span (set G)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis_list G

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
from basis_list_basis[OF this]
[PROOF STATE]
proof (chain)
picking this:
distinct G
lin_indpt (set G)
basis (set G)
[PROOF STEP]
have di:"distinct G"
[PROOF STATE]
proof (prove)
using this:
distinct G
lin_indpt (set G)
basis (set G)

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

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
have "det ((mat_of_rows n G)\<^sup>T) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_of_rows n G)\<^sup>T \<noteq> (0::'a)
[PROOF STEP]
unfolding det_0_iff_vec_prod_zero[OF M_car]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
assume "\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (state)
this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
obtain v where v:"v \<in> span (set G)"
                          "v \<noteq> 0\<^sub>v n" "(mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.span (set G); v \<noteq> 0\<^sub>v n; (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding issp
[PROOF STATE]
proof (prove)
using this:
\<exists>v. v \<in> local.span (set G) \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<in> local.span (set G); v \<noteq> 0\<^sub>v n; (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
v \<in> local.span (set G)
v \<noteq> 0\<^sub>v n
(mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from finite_in_span[OF finite_set inc_2 v(1)]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. True \<and> lincomb a (set G) = v
[PROOF STEP]
obtain a
      where aA: "v = lincomb a (set G)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. True \<and> lincomb a (set G) = v

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

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from v(1,2)[folded issp]
[PROOF STATE]
proof (chain)
picking this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n
[PROOF STEP]
obtain i where i:"v $ i \<noteq> 0" "i < n"
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
v \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>v $ i \<noteq> (0::'a); i < n\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
v $ i \<noteq> (0::'a)
i < n

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
hence inG:"G ! i \<in> set G"
[PROOF STATE]
proof (prove)
using this:
v $ i \<noteq> (0::'a)
i < n

goal (1 subgoal):
 1. G ! i \<in> set G
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
v $ i \<noteq> (0::'a)
i < n
length G = n

goal (1 subgoal):
 1. G ! i \<in> set G
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
G ! i \<in> set G

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have di2: "distinct [0..<length G]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct [0..<length G]
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct [0..<length G]

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
define f where "f = (\<lambda>l. \<Sum>i \<in> set [0..<length G]. if l = G ! i then v $ i else 0)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>l. \<Sum>i\<in>set [0..<length G]. if l = G ! i then v $ i else (0::'a))

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
hence f':"f (G ! i) = (\<Sum>ia\<leftarrow>[0..<n]. if G ! ia = G ! i then v $ ia else 0)"
[PROOF STATE]
proof (prove)
using this:
f = (\<lambda>l. \<Sum>i\<in>set [0..<length G]. if l = G ! i then v $ i else (0::'a))

goal (1 subgoal):
 1. f (G ! i) = (\<Sum>ia\<leftarrow>[0..<n]. if G ! ia = G ! i then v $ ia else (0::'a))
[PROOF STEP]
unfolding f_def sum.distinct_set_conv_list[OF di2]
[PROOF STATE]
proof (prove)
using this:
(\<lambda>l. \<Sum>i\<leftarrow>[0..<length G]. if l = G ! i then v $ i else (0::'a)) = (\<lambda>l. \<Sum>i\<leftarrow>[0..<length G]. if l = G ! i then v $ i else (0::'a))

goal (1 subgoal):
 1. (\<Sum>ia\<leftarrow>[0..<length G]. if G ! i = G ! ia then v $ ia else (0::'a)) = (\<Sum>ia\<leftarrow>[0..<n]. if G ! ia = G ! i then v $ ia else (0::'a))
[PROOF STEP]
unfolding len
[PROOF STATE]
proof (prove)
using this:
(\<lambda>l. \<Sum>i\<leftarrow>[0..<n]. if l = G ! i then v $ i else (0::'a)) = (\<lambda>l. \<Sum>i\<leftarrow>[0..<n]. if l = G ! i then v $ i else (0::'a))

goal (1 subgoal):
 1. (\<Sum>ia\<leftarrow>[0..<n]. if G ! i = G ! ia then v $ ia else (0::'a)) = (\<Sum>ia\<leftarrow>[0..<n]. if G ! ia = G ! i then v $ ia else (0::'a))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
f (G ! i) = (\<Sum>ia\<leftarrow>[0..<n]. if G ! ia = G ! i then v $ ia else (0::'a))

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from v
[PROOF STATE]
proof (chain)
picking this:
v \<in> local.span (set G)
v \<noteq> 0\<^sub>v n
(mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
have "mat_of_cols n G *\<^sub>v v = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
v \<in> local.span (set G)
v \<noteq> 0\<^sub>v n
(mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n

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

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

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
with mat_of_cols_mult_as_finsum[OF v(1)[folded issp len] RG_in_carr]
[PROOF STATE]
proof (chain)
picking this:
(\<And>i. i < length G \<Longrightarrow> i < length G) \<Longrightarrow> mat_of_cols n G *\<^sub>v v = lincomb (\<lambda>l. \<Sum>i = 0..<length G. if l = G ! i then v $ i else (0::'a)) (set G)
mat_of_cols n G *\<^sub>v v = 0\<^sub>v n
[PROOF STEP]
have f:"lincomb f (set G) = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i < length G \<Longrightarrow> i < length G) \<Longrightarrow> mat_of_cols n G *\<^sub>v v = lincomb (\<lambda>l. \<Sum>i = 0..<length G. if l = G ! i then v $ i else (0::'a)) (set G)
mat_of_cols n G *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb f (set G) = 0\<^sub>v n
[PROOF STEP]
unfolding len f_def
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i < n \<Longrightarrow> i < n) \<Longrightarrow> mat_of_cols n G *\<^sub>v v = lincomb (\<lambda>l. \<Sum>i = 0..<n. if l = G ! i then v $ i else (0::'a)) (set G)
mat_of_cols n G *\<^sub>v v = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb (\<lambda>l. \<Sum>i\<in>set [0..<n]. if l = G ! i then v $ i else (0::'a)) (set G) = 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb f (set G) = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
note [simp] = list_trisect[OF i(2)[folded len],unfolded len]
[PROOF STATE]
proof (state)
this:
[0..<n] = [0..<i] @ i # [Suc i..<n]

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
note x = i(2)[folded len]
[PROOF STATE]
proof (state)
this:
i < length G

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have [simp]:"(\<Sum>x\<leftarrow>[0..<i]. if G ! x = G ! i then v $ x else 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[0..<i]. if G ! x = G ! i then v $ x else (0::'a)) = (0::'a)
[PROOF STEP]
by (rule sum_list_0,auto simp: nth_eq_iff_index_eq[OF di less_trans[OF _ x] x])
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>[0..<i]. if G ! x = G ! i then v $ x else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have [simp]:"(\<Sum>x\<leftarrow>[Suc i..<n]. if G ! x = G ! i then v $ x else 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<leftarrow>[Suc i..<n]. if G ! x = G ! i then v $ x else (0::'a)) = (0::'a)
[PROOF STEP]
apply (rule sum_list_0)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>x. if G ! x = G ! i then v $ x else (0::'a)) [Suc i..<n]) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
using nth_eq_iff_index_eq[OF di _ x] len
[PROOF STATE]
proof (prove)
using this:
?i < length G \<Longrightarrow> (G ! ?i = G ! i) = (?i = i)
length G = n

goal (1 subgoal):
 1. \<And>x. x \<in> set (map (\<lambda>x. if G ! x = G ! i then v $ x else (0::'a)) [Suc i..<n]) \<Longrightarrow> x = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>x\<leftarrow>[Suc i..<n]. if G ! x = G ! i then v $ x else (0::'a)) = (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from i(1)
[PROOF STATE]
proof (chain)
picking this:
v $ i \<noteq> (0::'a)
[PROOF STEP]
have "f (G ! i) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. f (G ! i) \<noteq> (0::'a)
[PROOF STEP]
unfolding f'
[PROOF STATE]
proof (prove)
using this:
v $ i \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<Sum>ia\<leftarrow>[0..<n]. if G ! ia = G ! i then v $ ia else (0::'a)) \<noteq> (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f (G ! i) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from lin_dep_crit[OF finite_set subset_refl TrueI inG this f]
[PROOF STATE]
proof (chain)
picking this:
lin_dep (set G)
[PROOF STEP]
have "lin_dep (set G)"
[PROOF STATE]
proof (prove)
using this:
lin_dep (set G)

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

goal (1 subgoal):
 1. \<exists>v. v \<in> carrier_vec n \<and> v \<noteq> 0\<^sub>v n \<and> (mat_of_rows n G)\<^sup>T *\<^sub>v v = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
lin_dep (set G)

goal (1 subgoal):
 1. False
[PROOF STEP]
using li
[PROOF STATE]
proof (prove)
using this:
lin_dep (set G)
lin_indpt (set G)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n G)\<^sup>T \<noteq> (0::'a)

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
thus det0:"det (mat_of_rows n G) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
det (mat_of_rows n G)\<^sup>T \<noteq> (0::'a)

goal (1 subgoal):
 1. det (mat_of_rows n G) \<noteq> (0::'a)
[PROOF STEP]
by (unfold det_transpose[OF M_car1])
[PROOF STATE]
proof (state)
this:
det (mat_of_rows n G) \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed