[STATEMENT]
lemma (in \<Z>) cat_tiny_linear_order_cat_ordinal[cat_ordinal_cs_intros]:
  assumes "Ord A" and "A \<in>\<^sub>\<circ> \<alpha>"
  shows "cat_tiny_linear_order \<alpha> (cat_ordinal A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_tiny_linear_order \<alpha> (cat_ordinal A)
[PROOF STEP]
proof(intro cat_tiny_linear_orderI' cat_linear_order_cat_ordinal assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. tiny_category \<alpha> (cat_ordinal A)
 2. A \<subseteq>\<^sub>\<circ> \<alpha>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
Ord A
A \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
show "A \<subseteq>\<^sub>\<circ> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
Ord A
A \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. A \<subseteq>\<^sub>\<circ> \<alpha>
[PROOF STEP]
by (meson Ord_\<alpha> Ord_linear_le mem_not_refl vsubsetE)
[PROOF STATE]
proof (state)
this:
A \<subseteq>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
from assms(1) this
[PROOF STATE]
proof (chain)
picking this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>
[PROOF STEP]
interpret A: cat_linear_order \<alpha> \<open>cat_ordinal A\<close>
[PROOF STATE]
proof (prove)
using this:
Ord A
A \<subseteq>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. cat_linear_order \<alpha> (cat_ordinal A)
[PROOF STEP]
by (intro cat_linear_order_cat_ordinal)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
have A_in_Vset: "A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (simp add: Ord_\<alpha> Ord_in_in_VsetI)
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
have "cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
[PROOF STEP]
unfolding ordinal_arrs_def cat_ordinal_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {[a, b]\<^sub>\<circ> |a b. a \<in>\<^sub>\<circ> A \<and> b \<in>\<^sub>\<circ> A \<and> a \<subseteq>\<^sub>\<circ> b} \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
from A_in_Vset
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro Limit_ftimes_in_VsetI) auto
[PROOF STATE]
proof (state)
this:
A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
have "cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
using this:
cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
using vsubset_in_VsetI
[PROOF STATE]
proof (prove)
using this:
cat_ordinal A\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>?a \<subseteq>\<^sub>\<circ> ?A; ?A \<in>\<^sub>\<circ> Vset ?i\<rbrakk> \<Longrightarrow> ?a \<in>\<^sub>\<circ> Vset ?i

goal (1 subgoal):
 1. cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
ordinal_arrs A \<subseteq>\<^sub>\<circ> A \<times>\<^sub>\<bullet> A
A \<times>\<^sub>\<bullet> A \<in>\<^sub>\<circ> Vset \<alpha>
\<lbrakk>?a \<subseteq>\<^sub>\<circ> ?A; ?A \<in>\<^sub>\<circ> Vset ?i\<rbrakk> \<Longrightarrow> ?a \<in>\<^sub>\<circ> Vset ?i

goal (1 subgoal):
 1. ordinal_arrs A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
have "cat_ordinal A\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal A\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by (intro A_in_Vset)
[PROOF STATE]
proof (state)
this:
cat_ordinal A\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
cat_ordinal A\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "tiny_category \<alpha> (cat_ordinal A)"
[PROOF STATE]
proof (prove)
using this:
cat_ordinal A\<lparr>Arr\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>
cat_ordinal A\<lparr>Obj\<rparr> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. tiny_category \<alpha> (cat_ordinal A)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros tiny_categoryI')
[PROOF STATE]
proof (state)
this:
tiny_category \<alpha> (cat_ordinal A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) finite_category_cat_ordinal[cat_ordinal_cs_intros]:
  assumes "a \<in>\<^sub>\<circ> \<omega>"
  shows "finite_category \<alpha> (cat_ordinal a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
have "Ord a" "a \<in>\<^sub>\<circ> \<alpha>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. Ord a &&& a \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
by (auto simp: Ord_\<alpha> Ord_trans)
[PROOF STATE]
proof (state)
this:
Ord a
a \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Ord a
a \<in>\<^sub>\<circ> \<alpha>
[PROOF STEP]
interpret cat_ordinal: cat_tiny_linear_order \<alpha> \<open>cat_ordinal a\<close>
[PROOF STATE]
proof (prove)
using this:
Ord a
a \<in>\<^sub>\<circ> \<alpha>

goal (1 subgoal):
 1. cat_tiny_linear_order \<alpha> (cat_ordinal a)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_ordinal_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_category \<alpha> (cat_ordinal a)
[PROOF STEP]
proof(intro finite_categoryI')
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. category \<alpha> (cat_ordinal a)
 2. vfinite (cat_ordinal a\<lparr>Obj\<rparr>)
 3. vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "category \<alpha> (cat_ordinal a)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. category \<alpha> (cat_ordinal a)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
category \<alpha> (cat_ordinal a)

goal (2 subgoals):
 1. vfinite (cat_ordinal a\<lparr>Obj\<rparr>)
 2. vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "vfinite (cat_ordinal a\<lparr>Obj\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfinite (cat_ordinal a\<lparr>Obj\<rparr>)
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfinite a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfinite (cat_ordinal a\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
show "vfinite (cat_ordinal a\<lparr>Arr\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
have "cat_ordinal a\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_ordinal a\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a
[PROOF STEP]
unfolding cat_ordinal_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ordinal_arrs a \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cat_ordinal a\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cat_ordinal a\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<omega>
[PROOF STEP]
have "vfinite (a \<times>\<^sub>\<bullet> a)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfinite (a \<times>\<^sub>\<bullet> a)
[PROOF STEP]
by (intro vfinite_ftimesI) auto
[PROOF STATE]
proof (state)
this:
vfinite (a \<times>\<^sub>\<bullet> a)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<omega> \<Longrightarrow> vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cat_ordinal a\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a
vfinite (a \<times>\<^sub>\<bullet> a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cat_ordinal a\<lparr>Arr\<rparr> \<subseteq>\<^sub>\<circ> a \<times>\<^sub>\<bullet> a
vfinite (a \<times>\<^sub>\<bullet> a)

goal (1 subgoal):
 1. vfinite (cat_ordinal a\<lparr>Arr\<rparr>)
[PROOF STEP]
by (auto simp: vfinite_vsubset)
[PROOF STATE]
proof (state)
this:
vfinite (cat_ordinal a\<lparr>Arr\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vfinite (cat_ordinal a\<lparr>Arr\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite_category \<alpha> (cat_ordinal a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ortho_sum_in_span:
  assumes W: "W \<subseteq> carrier_vec n"
    and X: "X \<subseteq> carrier_vec n"
    and ortho: "\<And> w x. w \<in> W \<Longrightarrow> x \<in> X \<Longrightarrow> x \<bullet> w = 0"
    and inspan: "lincomb l1 X + lincomb l2 W \<in> span X"
  shows "lincomb l2 W = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb l2 W = 0\<^sub>v n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
let ?v = "lincomb l2 W"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have vcarr: "?v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb l2 W \<in> carrier_vec n
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb l2 W \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb l2 W \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have vspan: "?v \<in> span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb l2 W \<in> local.span W
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb l2 W \<in> local.span W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb l2 W \<in> local.span W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
lincomb l2 W \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
lincomb l2 W \<noteq> 0\<^sub>v n
[PROOF STEP]
have vnz: "?v \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
lincomb l2 W \<noteq> 0\<^sub>v n

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

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
let ?x = "lincomb l1 X"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have xcarr: "?x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb l1 X \<in> carrier_vec n
[PROOF STEP]
using X
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb l1 X \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb l1 X \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have xspan: "?x \<in> span X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb l1 X \<in> local.span X
[PROOF STEP]
using X xcarr
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n
lincomb l1 X \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb l1 X \<in> local.span X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb l1 X \<in> local.span X

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have "0 \<noteq> sq_norm ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<noteq> \<parallel>lincomb l2 W\<parallel>\<^sup>2
[PROOF STEP]
using vnz vcarr
[PROOF STATE]
proof (prove)
using this:
lincomb l2 W \<noteq> 0\<^sub>v n
lincomb l2 W \<in> carrier_vec n

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

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) \<noteq> \<parallel>lincomb l2 W\<parallel>\<^sup>2

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have "sq_norm ?v = 0 + ?v \<bullet> ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<parallel>lincomb l2 W\<parallel>\<^sup>2 = (0::'a) + lincomb l2 W \<bullet> lincomb l2 W
[PROOF STEP]
by (simp add: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
\<parallel>lincomb l2 W\<parallel>\<^sup>2 = (0::'a) + lincomb l2 W \<bullet> lincomb l2 W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<parallel>lincomb l2 W\<parallel>\<^sup>2 = (0::'a) + lincomb l2 W \<bullet> lincomb l2 W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = ?x \<bullet> ?v + ?v \<bullet> ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) + lincomb l2 W \<bullet> lincomb l2 W = lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W
[PROOF STEP]
by (subst (2) ortho_span_span[OF X W ortho], insert X W, auto)
[PROOF STATE]
proof (state)
this:
(0::'a) + lincomb l2 W \<bullet> lincomb l2 W = lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(0::'a) + lincomb l2 W \<bullet> lincomb l2 W = lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = (?x + ?v ) \<bullet> ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W = (lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W
[PROOF STEP]
using xcarr vcarr
[PROOF STATE]
proof (prove)
using this:
lincomb l1 X \<in> carrier_vec n
lincomb l2 W \<in> carrier_vec n

goal (1 subgoal):
 1. lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W = (lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W
[PROOF STEP]
using add_scalar_prod_distrib
[PROOF STATE]
proof (prove)
using this:
lincomb l1 X \<in> carrier_vec n
lincomb l2 W \<in> carrier_vec n
\<lbrakk>?v\<^sub>1 \<in> carrier_vec ?n; ?v\<^sub>2 \<in> carrier_vec ?n; ?v\<^sub>3 \<in> carrier_vec ?n\<rbrakk> \<Longrightarrow> (?v\<^sub>1 + ?v\<^sub>2) \<bullet> ?v\<^sub>3 = ?v\<^sub>1 \<bullet> ?v\<^sub>3 + ?v\<^sub>2 \<bullet> ?v\<^sub>3

goal (1 subgoal):
 1. lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W = (lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W = (lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb l1 X \<bullet> lincomb l2 W + lincomb l2 W \<bullet> lincomb l2 W = (lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W = (0::'a)
[PROOF STEP]
by (rule ortho_span_span[OF X W ortho inspan vspan])
[PROOF STATE]
proof (state)
this:
(lincomb l1 X + lincomb l2 W) \<bullet> lincomb l2 W = (0::'a)

goal (1 subgoal):
 1. lincomb l2 W \<noteq> 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<noteq> (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<noteq> (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ortho_lin_indpt: assumes W: "W \<subseteq> carrier_vec n"
  and X: "X \<subseteq> carrier_vec n"
  and ortho: "\<And> w x. w \<in> W \<Longrightarrow> x \<in> X \<Longrightarrow> x \<bullet> w = 0"
  and linW: "lin_indpt W"
  and linX: "lin_indpt X"
shows "lin_indpt (W \<union> X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (W \<union> X)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
\<not> lin_indpt (W \<union> X)

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<not> lin_indpt (W \<union> X)
[PROOF STEP]
obtain c where zerocomb:"lincomb c (W \<union> X) = 0\<^sub>v n"
    and notallz: "\<exists>v \<in> (W \<union> X). c v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<not> lin_indpt (W \<union> X)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb c (W \<union> X) = 0\<^sub>v n; \<exists>v\<in>W \<union> X. c v \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms fin_dim fin_dim_li_fin finite_lin_indpt2 infinite_Un le_sup_iff
[PROOF STATE]
proof (prove)
using this:
\<not> lin_indpt (W \<union> X)
W \<subseteq> carrier_vec n
X \<subseteq> carrier_vec n
\<lbrakk>?w3 \<in> W; ?x3 \<in> X\<rbrakk> \<Longrightarrow> ?x3 \<bullet> ?w3 = (0::'a)
lin_indpt W
lin_indpt X
fin_dim
\<lbrakk>fin_dim; lin_indpt ?A; ?A \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> finite ?A
\<lbrakk>finite ?A; ?A \<subseteq> carrier_vec n; \<And>a. \<lbrakk>True; lincomb a ?A = 0\<^sub>v n\<rbrakk> \<Longrightarrow> \<forall>v\<in>?A. a v = (0::'a)\<rbrakk> \<Longrightarrow> lin_indpt ?A
infinite (?S \<union> ?T) = (infinite ?S \<or> infinite ?T)
(sup ?x ?y \<le> ?z) = (?x \<le> ?z \<and> ?y \<le> ?z)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>lincomb c (W \<union> X) = 0\<^sub>v n; \<exists>v\<in>W \<union> X. c v \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
lincomb c (W \<union> X) = 0\<^sub>v n
\<exists>v\<in>W \<union> X. c v \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have zero_nin_W: "0\<^sub>v n \<notin> W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n \<notin> W
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
X \<subseteq> carrier_vec n
\<lbrakk>?w3 \<in> W; ?x3 \<in> X\<rbrakk> \<Longrightarrow> ?x3 \<bullet> ?w3 = (0::'a)
lin_indpt W
lin_indpt X

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

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have WXinters: "W \<inter> X = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. W \<inter> X = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "\<not>?thesis"
[PROOF STATE]
proof (state)
this:
W \<inter> X \<noteq> {}

goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
W \<inter> X \<noteq> {}
[PROOF STEP]
obtain v where v: "v\<in> W \<inter> X"
[PROOF STATE]
proof (prove)
using this:
W \<inter> X \<noteq> {}

goal (1 subgoal):
 1. (\<And>v. v \<in> W \<inter> X \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<in> W \<inter> X

goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
hence "v\<bullet>v=0"
[PROOF STATE]
proof (prove)
using this:
v \<in> W \<inter> X

goal (1 subgoal):
 1. v \<bullet> v = (0::'a)
[PROOF STEP]
using ortho
[PROOF STATE]
proof (prove)
using this:
v \<in> W \<inter> X
\<lbrakk>?w3 \<in> W; ?x3 \<in> X\<rbrakk> \<Longrightarrow> ?x3 \<bullet> ?w3 = (0::'a)

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

goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
v \<bullet> v = (0::'a)

goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
have "v \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> carrier_vec n
[PROOF STEP]
using assms v
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
X \<subseteq> carrier_vec n
\<lbrakk>?w3 \<in> W; ?x3 \<in> X\<rbrakk> \<Longrightarrow> ?x3 \<bullet> ?w3 = (0::'a)
lin_indpt W
lin_indpt X
v \<in> W \<inter> X

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

goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
v \<bullet> v = (0::'a)
v \<in> carrier_vec n
[PROOF STEP]
have "v=0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
v \<bullet> v = (0::'a)
v \<in> carrier_vec n

goal (1 subgoal):
 1. v = 0\<^sub>v n
[PROOF STEP]
using sq_norm_vec_as_cscalar_prod[of v]
[PROOF STATE]
proof (prove)
using this:
v \<bullet> v = (0::'a)
v \<in> carrier_vec n
\<parallel>v\<parallel>\<^sup>2 = v \<bullet>c v

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

goal (1 subgoal):
 1. W \<inter> X \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
v = 0\<^sub>v n
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
v = 0\<^sub>v n

goal (1 subgoal):
 1. False
[PROOF STEP]
using zero_nin_W v
[PROOF STATE]
proof (prove)
using this:
v = 0\<^sub>v n
0\<^sub>v n \<notin> W
v \<in> W \<inter> X

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:
W \<inter> X = {}

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have finX: "finite X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite X
[PROOF STEP]
using X linX
[PROOF STATE]
proof (prove)
using this:
X \<subseteq> carrier_vec n
lin_indpt X

goal (1 subgoal):
 1. finite X
[PROOF STEP]
by (simp add: fin_dim_li_fin)
[PROOF STATE]
proof (state)
this:
finite X

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have finW: "finite W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite W
[PROOF STEP]
using W linW
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
lin_indpt W

goal (1 subgoal):
 1. finite W
[PROOF STEP]
by (simp add: fin_dim_li_fin)
[PROOF STATE]
proof (state)
this:
finite W

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have split: "lincomb c (W \<union> X) = lincomb c X + lincomb c W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (W \<union> X) = lincomb c X + lincomb c W
[PROOF STEP]
using lincomb_union[OF W X WXinters finW finX]
[PROOF STATE]
proof (prove)
using this:
?a \<in> W \<union> X \<rightarrow> UNIV \<Longrightarrow> lincomb ?a (W \<union> X) = lincomb ?a W + lincomb ?a X

goal (1 subgoal):
 1. lincomb c (W \<union> X) = lincomb c X + lincomb c W
[PROOF STEP]
by (simp add: M.add.m_comm W X)
[PROOF STATE]
proof (state)
this:
lincomb c (W \<union> X) = lincomb c X + lincomb c W

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
hence "lincomb c X + lincomb c W  \<in> span X"
[PROOF STATE]
proof (prove)
using this:
lincomb c (W \<union> X) = lincomb c X + lincomb c W

goal (1 subgoal):
 1. lincomb c X + lincomb c W \<in> local.span X
[PROOF STEP]
using zerocomb
[PROOF STATE]
proof (prove)
using this:
lincomb c (W \<union> X) = lincomb c X + lincomb c W
lincomb c (W \<union> X) = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb c X + lincomb c W \<in> local.span X
[PROOF STEP]
using local.span_zero
[PROOF STATE]
proof (prove)
using this:
lincomb c (W \<union> X) = lincomb c X + lincomb c W
lincomb c (W \<union> X) = 0\<^sub>v n
0\<^sub>v n \<in> local.span ?U

goal (1 subgoal):
 1. lincomb c X + lincomb c W \<in> local.span X
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb c X + lincomb c W \<in> local.span X

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
hence z1: "lincomb c W = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
lincomb c X + lincomb c W \<in> local.span X

goal (1 subgoal):
 1. lincomb c W = 0\<^sub>v n
[PROOF STEP]
using ortho_sum_in_span[OF W X ortho]
[PROOF STATE]
proof (prove)
using this:
lincomb c X + lincomb c W \<in> local.span X
\<lbrakk>\<And>w x. \<lbrakk>w \<in> W; x \<in> X\<rbrakk> \<Longrightarrow> w \<in> W; \<And>w x. \<lbrakk>w \<in> W; x \<in> X\<rbrakk> \<Longrightarrow> x \<in> X; lincomb ?l1.0 X + lincomb ?l2.0 W \<in> local.span X\<rbrakk> \<Longrightarrow> lincomb ?l2.0 W = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb c W = 0\<^sub>v n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb c W = 0\<^sub>v n

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
hence z2: "lincomb c X = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
lincomb c W = 0\<^sub>v n

goal (1 subgoal):
 1. lincomb c X = 0\<^sub>v n
[PROOF STEP]
using split zerocomb X
[PROOF STATE]
proof (prove)
using this:
lincomb c W = 0\<^sub>v n
lincomb c (W \<union> X) = lincomb c X + lincomb c W
lincomb c (W \<union> X) = 0\<^sub>v n
X \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb c X = 0\<^sub>v n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lincomb c X = 0\<^sub>v n

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have or: "(\<exists>v \<in> W. c v \<noteq> 0) \<or> (\<exists> v\<in> X. c v \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>v\<in>W. c v \<noteq> (0::'a)) \<or> (\<exists>v\<in>X. c v \<noteq> (0::'a))
[PROOF STEP]
using notallz
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<in>W \<union> X. c v \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<exists>v\<in>W. c v \<noteq> (0::'a)) \<or> (\<exists>v\<in>X. c v \<noteq> (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<exists>v\<in>W. c v \<noteq> (0::'a)) \<or> (\<exists>v\<in>X. c v \<noteq> (0::'a))

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have ex1: "\<exists>v \<in> W. c v \<noteq> 0 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v\<in>W. c v \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
using linW
[PROOF STATE]
proof (prove)
using this:
lin_indpt W

goal (1 subgoal):
 1. \<exists>v\<in>W. c v \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
using finW lin_dep_def z1
[PROOF STATE]
proof (prove)
using this:
lin_indpt W
finite W
lin_dep ?S = (\<exists>A a v. finite A \<and> A \<subseteq> ?S \<and> True \<and> lincomb a A = 0\<^sub>v n \<and> v \<in> A \<and> a v \<noteq> (0::'a))
lincomb c W = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>v\<in>W. c v \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>v\<in>W. c v \<noteq> (0::'a) \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
have ex2: "\<exists> v\<in> X. c v \<noteq> 0 \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v\<in>X. c v \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
using linX
[PROOF STATE]
proof (prove)
using this:
lin_indpt X

goal (1 subgoal):
 1. \<exists>v\<in>X. c v \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
using finX lin_dep_def z2
[PROOF STATE]
proof (prove)
using this:
lin_indpt X
finite X
lin_dep ?S = (\<exists>A a v. finite A \<and> A \<subseteq> ?S \<and> True \<and> lincomb a A = 0\<^sub>v n \<and> v \<in> A \<and> a v \<noteq> (0::'a))
lincomb c X = 0\<^sub>v n

goal (1 subgoal):
 1. \<exists>v\<in>X. c v \<noteq> (0::'a) \<Longrightarrow> False
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>v\<in>X. c v \<noteq> (0::'a) \<Longrightarrow> False

goal (1 subgoal):
 1. \<not> lin_indpt (W \<union> X) \<Longrightarrow> False
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using ex1 ex2 or
[PROOF STATE]
proof (prove)
using this:
\<exists>v\<in>W. c v \<noteq> (0::'a) \<Longrightarrow> False
\<exists>v\<in>X. c v \<noteq> (0::'a) \<Longrightarrow> False
(\<exists>v\<in>W. c v \<noteq> (0::'a)) \<or> (\<exists>v\<in>X. c v \<noteq> (0::'a))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma normal_vector: assumes fin: "finite W"
  and card: "Suc (card W) = n"
  and lin: "lin_indpt W"
  and W: "W \<subseteq> carrier_vec n"
shows "normal_vector W \<in> carrier_vec n"
  "normal_vector W \<noteq> 0\<^sub>v n"
  "w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = 0"
  "w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = 0"
  "lin_indpt (insert (normal_vector W) W)"
  "normal_vector W \<notin> W"
  "is_det_bound db \<Longrightarrow> W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n-1) Bnd))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (normal_vector W \<in> carrier_vec n &&& normal_vector W \<noteq> 0\<^sub>v n &&& (w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a))) &&& ((w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)) &&& lin_indpt (insert (normal_vector W) W)) &&& normal_vector W \<notin> W &&& (\<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
define ws where "ws = (SOME ws. set ws = W \<and> distinct ws)"
[PROOF STATE]
proof (state)
this:
ws = (SOME ws. set ws = W \<and> distinct ws)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from finite_distinct_list[OF fin]
[PROOF STATE]
proof (chain)
picking this:
\<exists>xs. set xs = W \<and> distinct xs
[PROOF STEP]
have "\<exists> ws. set ws = W \<and> distinct ws"
[PROOF STATE]
proof (prove)
using this:
\<exists>xs. set xs = W \<and> distinct xs

goal (1 subgoal):
 1. \<exists>ws. set ws = W \<and> distinct ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ws. set ws = W \<and> distinct ws

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from someI_ex[OF this, folded ws_def]
[PROOF STATE]
proof (chain)
picking this:
set ws = W \<and> distinct ws
[PROOF STEP]
have id: "set ws = W" and dist: "distinct ws"
[PROOF STATE]
proof (prove)
using this:
set ws = W \<and> distinct ws

goal (1 subgoal):
 1. set ws = W &&& distinct ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ws = W
distinct ws

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have len: "length ws = card W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ws = card W
[PROOF STEP]
using distinct_card[OF dist] id
[PROOF STATE]
proof (prove)
using this:
card (set ws) = length ws
set ws = W

goal (1 subgoal):
 1. length ws = card W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ws = card W

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
let ?n = "length ws"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
define B where "B = (\<lambda> j. mat ?n ?n (\<lambda>(i, j'). ws ! i $ (if j' < j then j' else Suc j')))"
[PROOF STATE]
proof (state)
this:
B = (\<lambda>j. mat (length ws) (length ws) (\<lambda>(i, j'). ws ! i $ (if j' < j then j' else Suc j')))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
define nv where "nv = vec n (\<lambda> j. (-1)^(?n+j) * det (B j))"
[PROOF STATE]
proof (state)
this:
nv = vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have nv2: "normal_vector W = nv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_vector W = nv
[PROOF STEP]
unfolding normal_vector_def Let_def
      ws_def[symmetric] B_def nv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (mat (length ws) (length ws) (\<lambda>(i, j'). ws ! i $ (if j' < j then j' else Suc j')))) = vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (mat (length ws) (length ws) (\<lambda>(i, j'). ws ! i $ (if j' < j then j' else Suc j'))))
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
normal_vector W = nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
define A where "A = (\<lambda> w. mat_of_rows n (ws @ [w]))"
[PROOF STATE]
proof (state)
this:
A = (\<lambda>w. mat_of_rows n (ws @ [w]))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from len id card
[PROOF STATE]
proof (chain)
picking this:
length ws = card W
set ws = W
Suc (card W) = n
[PROOF STEP]
have len: "Suc ?n = n"
[PROOF STATE]
proof (prove)
using this:
length ws = card W
set ws = W
Suc (card W) = n

goal (1 subgoal):
 1. Suc (length ws) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (length ws) = n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have A: "A w \<in> carrier_mat n n" for w
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A w \<in> carrier_mat n n
[PROOF STEP]
using id W len
[PROOF STATE]
proof (prove)
using this:
set ws = W
W \<subseteq> carrier_vec n
Suc (length ws) = n

goal (1 subgoal):
 1. A w \<in> carrier_mat n n
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
set ws = W
W \<subseteq> carrier_vec n
Suc (length ws) = n

goal (1 subgoal):
 1. mat_of_rows n (ws @ [w]) \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A ?w3 \<in> carrier_mat n n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
A ?w3 \<in> carrier_mat n n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
fix w :: "'a vec"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
assume w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from len
[PROOF STATE]
proof (chain)
picking this:
Suc (length ws) = n
[PROOF STEP]
have n1[simp]: "n - Suc 0 = ?n"
[PROOF STATE]
proof (prove)
using this:
Suc (length ws) = n

goal (1 subgoal):
 1. n - Suc 0 = length ws
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n - Suc 0 = length ws

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n - Suc 0 = length ws

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
assume j: "j < n"
[PROOF STATE]
proof (state)
this:
j < n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "mat_delete (A w) ?n j = B j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_delete (A w) (length ws) j = B j
[PROOF STEP]
unfolding mat_delete_def A_def mat_of_rows_def B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (dim_row (mat (length (ws @ [w])) n (\<lambda>(i, y). (ws @ [w]) ! i $ y)) - 1) (dim_col (mat (length (ws @ [w])) n (\<lambda>(i, y). (ws @ [w]) ! i $ y)) - 1) (\<lambda>(i', j'). mat (length (ws @ [w])) n (\<lambda>(i, y). (ws @ [w]) ! i $ y) $$ (if i' < length ws then i' else Suc i', if j' < j then j' else Suc j')) = mat (length ws) (length ws) (\<lambda>(i, j'). ws ! i $ (if j' < j then j' else Suc j'))
[PROOF STEP]
by (rule eq_matI, insert j len, auto simp: nth_append)
[PROOF STATE]
proof (state)
this:
mat_delete (A w) (length ws) j = B j

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j5 < n \<Longrightarrow> mat_delete (A w) (length ws) ?j5 = B ?j5

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
note B = this
[PROOF STATE]
proof (state)
this:
?j5 < n \<Longrightarrow> mat_delete (A w) (length ws) ?j5 = B ?j5

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "det (A w) = (\<Sum>j<n. (A w) $$ (length ws, j) * cofactor (A w) ?n j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (A w) = (\<Sum>j<n. A w $$ (length ws, j) * cofactor (A w) (length ws) j)
[PROOF STEP]
by (subst laplace_expansion_row[OF A, of ?n], insert len, auto)
[PROOF STATE]
proof (state)
this:
det (A w) = (\<Sum>j<n. A w $$ (length ws, j) * cofactor (A w) (length ws) j)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (A w) = (\<Sum>j<n. A w $$ (length ws, j) * cofactor (A w) (length ws) j)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "\<dots> = (\<Sum>j<n. w $ j * (-1)^(?n+j) * det (mat_delete (A w) ?n j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. A w $$ (length ws, j) * cofactor (A w) (length ws) j) = (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (mat_delete (A w) (length ws) j))
[PROOF STEP]
by (rule sum.cong, auto simp: A_def mat_of_rows_def cofactor_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. A w $$ (length ws, j) * cofactor (A w) (length ws) j) = (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (mat_delete (A w) (length ws) j))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. A w $$ (length ws, j) * cofactor (A w) (length ws) j) = (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (mat_delete (A w) (length ws) j))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "\<dots> = (\<Sum>j<n. w $ j * (-1)^(?n+j) * det (B j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (mat_delete (A w) (length ws) j)) = (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (B j))
[PROOF STEP]
by (rule sum.cong[OF refl], subst B, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (mat_delete (A w) (length ws) j)) = (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (B j))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (mat_delete (A w) (length ws) j)) = (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (B j))

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "\<dots> = (\<Sum>j<n. w $ j * nv $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (B j)) = (\<Sum>j<n. w $ j * nv $ j)
[PROOF STEP]
by (rule sum.cong[OF refl], auto simp: nv_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (B j)) = (\<Sum>j<n. w $ j * nv $ j)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. w $ j * (- (1::'a)) ^ (length ws + j) * det (B j)) = (\<Sum>j<n. w $ j * nv $ j)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "\<dots> = w \<bullet> nv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. w $ j * nv $ j) = w \<bullet> nv
[PROOF STEP]
unfolding scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. w $ j * nv $ j) = (\<Sum>i = 0..<dim_vec nv. w $ i * nv $ i)
[PROOF STEP]
unfolding nv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. w $ j * vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) $ j) = (\<Sum>i = 0..<dim_vec (vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j))). w $ i * vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) $ i)
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. w $ j * nv $ j) = w \<bullet> nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
det (A w) = w \<bullet> nv
[PROOF STEP]
have "det (A w) = w \<bullet> nv"
[PROOF STATE]
proof (prove)
using this:
det (A w) = w \<bullet> nv

goal (1 subgoal):
 1. det (A w) = w \<bullet> nv
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (A w) = w \<bullet> nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?wa5 \<in> carrier_vec n \<Longrightarrow> det (A ?wa5) = ?wa5 \<bullet> nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
note det_scalar = this
[PROOF STATE]
proof (state)
this:
?wa5 \<in> carrier_vec n \<Longrightarrow> det (A ?wa5) = ?wa5 \<bullet> nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have nv: "nv \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nv \<in> carrier_vec n
[PROOF STEP]
unfolding nv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nv \<in> carrier_vec n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
nv \<in> carrier_vec n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
fix w
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
assume wW: "w \<in> W"
[PROOF STATE]
proof (state)
this:
w \<in> W

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
with W
[PROOF STATE]
proof (chain)
picking this:
W \<subseteq> carrier_vec n
w \<in> W
[PROOF STEP]
have w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
w \<in> W

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

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from wW id
[PROOF STATE]
proof (chain)
picking this:
w \<in> W
set ws = W
[PROOF STEP]
obtain i where i: "i < ?n" and ws: "ws ! i = w"
[PROOF STATE]
proof (prove)
using this:
w \<in> W
set ws = W

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length ws; ws ! i = w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
w \<in> W
{ws ! i |i. i < length ws} = W

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length ws; ws ! i = w\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length ws
ws ! i = w

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from det_scalar[OF w]
[PROOF STATE]
proof (chain)
picking this:
det (A w) = w \<bullet> nv
[PROOF STEP]
have "det (A w) = w \<bullet> nv"
[PROOF STATE]
proof (prove)
using this:
det (A w) = w \<bullet> nv

goal (1 subgoal):
 1. det (A w) = w \<bullet> nv
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
det (A w) = w \<bullet> nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (A w) = w \<bullet> nv

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "det (A w) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (A w) = (0::'a)
[PROOF STEP]
by (subst det_identical_rows[OF A, of i ?n], insert i ws len, auto simp: A_def mat_of_rows_def nth_append)
[PROOF STATE]
proof (state)
this:
det (A w) = (0::'a)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(0::'a) = w \<bullet> nv
[PROOF STEP]
have "w \<bullet> nv = 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) = w \<bullet> nv

goal (1 subgoal):
 1. w \<bullet> nv = (0::'a)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
w \<bullet> nv = (0::'a)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
note this this[unfolded comm_scalar_prod[OF w nv]]
[PROOF STATE]
proof (state)
this:
w \<bullet> nv = (0::'a)
nv \<bullet> w = (0::'a)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?wa5 \<in> W \<Longrightarrow> ?wa5 \<bullet> nv = (0::'a)
?wa5 \<in> W \<Longrightarrow> nv \<bullet> ?wa5 = (0::'a)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
note ortho = this
[PROOF STATE]
proof (state)
this:
?wa5 \<in> W \<Longrightarrow> ?wa5 \<bullet> nv = (0::'a)
?wa5 \<in> W \<Longrightarrow> nv \<bullet> ?wa5 = (0::'a)

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have nv0: "nv \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nv \<noteq> 0\<^sub>v n
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
assume nv: "nv = 0\<^sub>v n"
[PROOF STATE]
proof (state)
this:
nv = 0\<^sub>v n

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
define bs where "bs = basis_extension ws"
[PROOF STATE]
proof (state)
this:
bs = basis_extension ws

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
define w where "w = hd bs"
[PROOF STATE]
proof (state)
this:
w = hd bs

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
have "lin_indpt_list ws"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list ws
[PROOF STEP]
using dist lin W
[PROOF STATE]
proof (prove)
using this:
distinct ws
lin_indpt W
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lin_indpt_list ws
[PROOF STEP]
unfolding lin_indpt_list_def id
[PROOF STATE]
proof (prove)
using this:
distinct ws
lin_indpt W
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. W \<subseteq> carrier_vec n \<and> distinct ws \<and> lin_indpt W
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt_list ws

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from basis_extension[OF this, folded bs_def] len
[PROOF STATE]
proof (chain)
picking this:
set bs \<subseteq> set (unit_vecs n)
lin_indpt_list (ws @ bs)
length (ws @ bs) = n
Suc (length ws) = n
[PROOF STEP]
have lin: "lin_indpt_list (ws @ bs)" and "length bs = 1" and bsc: "set bs \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set bs \<subseteq> set (unit_vecs n)
lin_indpt_list (ws @ bs)
length (ws @ bs) = n
Suc (length ws) = n

goal (1 subgoal):
 1. lin_indpt_list (ws @ bs) &&& length bs = 1 &&& set bs \<subseteq> carrier_vec n
[PROOF STEP]
by (auto simp: unit_vecs_def)
[PROOF STATE]
proof (state)
this:
lin_indpt_list (ws @ bs)
length bs = 1
set bs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
hence bs: "bs = [w]"
[PROOF STATE]
proof (prove)
using this:
lin_indpt_list (ws @ bs)
length bs = 1
set bs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. bs = [w]
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
using this:
lin_indpt_list (ws @ bs)
length bs = 1
set bs \<subseteq> carrier_vec n

goal (1 subgoal):
 1. bs = [hd bs]
[PROOF STEP]
by (cases bs, auto)
[PROOF STATE]
proof (state)
this:
bs = [w]

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
with bsc
[PROOF STATE]
proof (chain)
picking this:
set bs \<subseteq> carrier_vec n
bs = [w]
[PROOF STEP]
have w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set bs \<subseteq> carrier_vec n
bs = [w]

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

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
note lin = lin[unfolded bs]
[PROOF STATE]
proof (state)
this:
lin_indpt_list (ws @ [w])

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from lin_indpt_list_length_eq_n[OF lin] len
[PROOF STATE]
proof (chain)
picking this:
length (ws @ [w]) = n \<Longrightarrow> local.span (set (ws @ [w])) = carrier_vec n
length (ws @ [w]) = n \<Longrightarrow> basis (set (ws @ [w]))
Suc (length ws) = n
[PROOF STEP]
have basis: "basis (set (ws @ [w]))"
[PROOF STATE]
proof (prove)
using this:
length (ws @ [w]) = n \<Longrightarrow> local.span (set (ws @ [w])) = carrier_vec n
length (ws @ [w]) = n \<Longrightarrow> basis (set (ws @ [w]))
Suc (length ws) = n

goal (1 subgoal):
 1. basis (set (ws @ [w]))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
basis (set (ws @ [w]))

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
from w det_scalar nv
[PROOF STATE]
proof (chain)
picking this:
w \<in> carrier_vec n
?wa5 \<in> carrier_vec n \<Longrightarrow> det (A ?wa5) = ?wa5 \<bullet> nv
nv = 0\<^sub>v n
[PROOF STEP]
have det0: "det (A w) = 0"
[PROOF STATE]
proof (prove)
using this:
w \<in> carrier_vec n
?wa5 \<in> carrier_vec n \<Longrightarrow> det (A ?wa5) = ?wa5 \<bullet> nv
nv = 0\<^sub>v n

goal (1 subgoal):
 1. det (A w) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
det (A w) = (0::'a)

goal (1 subgoal):
 1. nv = 0\<^sub>v n \<Longrightarrow> False
[PROOF STEP]
with basis_det_nonzero[OF basis] len
[PROOF STATE]
proof (chain)
picking this:
length (ws @ [w]) = n \<Longrightarrow> det (mat_of_rows n (ws @ [w])) \<noteq> (0::'a)
Suc (length ws) = n
det (A w) = (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
length (ws @ [w]) = n \<Longrightarrow> det (mat_of_rows n (ws @ [w])) \<noteq> (0::'a)
Suc (length ws) = n
det (A w) = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding A_def
[PROOF STATE]
proof (prove)
using this:
length (ws @ [w]) = n \<Longrightarrow> det (mat_of_rows n (ws @ [w])) \<noteq> (0::'a)
Suc (length ws) = n
det (mat_of_rows n (ws @ [w])) = (0::'a)

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:
nv \<noteq> 0\<^sub>v n

goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
let ?nv = "normal_vector W"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. normal_vector W \<in> carrier_vec n
 2. normal_vector W \<noteq> 0\<^sub>v n
 3. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)
 4. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a)
 5. lin_indpt (insert (normal_vector W) W)
 6. normal_vector W \<notin> W
 7. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from ortho nv nv0
[PROOF STATE]
proof (chain)
picking this:
?wa5 \<in> W \<Longrightarrow> ?wa5 \<bullet> nv = (0::'a)
?wa5 \<in> W \<Longrightarrow> nv \<bullet> ?wa5 = (0::'a)
nv \<in> carrier_vec n
nv \<noteq> 0\<^sub>v n
[PROOF STEP]
show nv: "?nv \<in> carrier_vec n"
    and ortho: "\<And> w. w \<in> W \<Longrightarrow> w \<bullet> ?nv = 0"
    "\<And> w. w \<in> W \<Longrightarrow> ?nv \<bullet> w = 0"
    and n0: "?nv \<noteq> 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
?wa5 \<in> W \<Longrightarrow> ?wa5 \<bullet> nv = (0::'a)
?wa5 \<in> W \<Longrightarrow> nv \<bullet> ?wa5 = (0::'a)
nv \<in> carrier_vec n
nv \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. normal_vector W \<in> carrier_vec n &&& ((\<And>w. w \<in> W \<Longrightarrow> w \<bullet> normal_vector W = (0::'a)) &&& (\<And>w. w \<in> W \<Longrightarrow> normal_vector W \<bullet> w = (0::'a))) &&& normal_vector W \<noteq> 0\<^sub>v n
[PROOF STEP]
unfolding nv2
[PROOF STATE]
proof (prove)
using this:
?wa5 \<in> W \<Longrightarrow> ?wa5 \<bullet> nv = (0::'a)
?wa5 \<in> W \<Longrightarrow> nv \<bullet> ?wa5 = (0::'a)
nv \<in> carrier_vec n
nv \<noteq> 0\<^sub>v n

goal (1 subgoal):
 1. nv \<in> carrier_vec n &&& ((\<And>w. w \<in> W \<Longrightarrow> w \<bullet> nv = (0::'a)) &&& (\<And>w. w \<in> W \<Longrightarrow> nv \<bullet> w = (0::'a))) &&& nv \<noteq> 0\<^sub>v n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
normal_vector W \<in> carrier_vec n
?w3 \<in> W \<Longrightarrow> ?w3 \<bullet> normal_vector W = (0::'a)
?w3 \<in> W \<Longrightarrow> normal_vector W \<bullet> ?w3 = (0::'a)
normal_vector W \<noteq> 0\<^sub>v n

goal (3 subgoals):
 1. lin_indpt (insert (normal_vector W) W)
 2. normal_vector W \<notin> W
 3. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from n0 nv
[PROOF STATE]
proof (chain)
picking this:
normal_vector W \<noteq> 0\<^sub>v n
normal_vector W \<in> carrier_vec n
[PROOF STEP]
have "sq_norm ?nv \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
normal_vector W \<noteq> 0\<^sub>v n
normal_vector W \<in> carrier_vec n

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

goal (3 subgoals):
 1. lin_indpt (insert (normal_vector W) W)
 2. normal_vector W \<notin> W
 3. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
hence nvnv: "?nv \<bullet> ?nv \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<parallel>normal_vector W\<parallel>\<^sup>2 \<noteq> (0::'a)

goal (1 subgoal):
 1. normal_vector W \<bullet> normal_vector W \<noteq> (0::'a)
[PROOF STEP]
by (auto simp: sq_norm_vec_as_cscalar_prod)
[PROOF STATE]
proof (state)
this:
normal_vector W \<bullet> normal_vector W \<noteq> (0::'a)

goal (3 subgoals):
 1. lin_indpt (insert (normal_vector W) W)
 2. normal_vector W \<notin> W
 3. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
show nvW: "?nv \<notin> W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_vector W \<notin> W
[PROOF STEP]
using nvnv ortho
[PROOF STATE]
proof (prove)
using this:
normal_vector W \<bullet> normal_vector W \<noteq> (0::'a)
?w3 \<in> W \<Longrightarrow> ?w3 \<bullet> normal_vector W = (0::'a)
?w3 \<in> W \<Longrightarrow> normal_vector W \<bullet> ?w3 = (0::'a)

goal (1 subgoal):
 1. normal_vector W \<notin> W
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
normal_vector W \<notin> W

goal (2 subgoals):
 1. lin_indpt (insert (normal_vector W) W)
 2. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "?nv \<notin> span W"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_vector W \<notin> local.span W
[PROOF STEP]
using W ortho nvnv nv
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
?w3 \<in> W \<Longrightarrow> ?w3 \<bullet> normal_vector W = (0::'a)
?w3 \<in> W \<Longrightarrow> normal_vector W \<bullet> ?w3 = (0::'a)
normal_vector W \<bullet> normal_vector W \<noteq> (0::'a)
normal_vector W \<in> carrier_vec n

goal (1 subgoal):
 1. normal_vector W \<notin> local.span W
[PROOF STEP]
using orthocompl_span
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n
?w3 \<in> W \<Longrightarrow> ?w3 \<bullet> normal_vector W = (0::'a)
?w3 \<in> W \<Longrightarrow> normal_vector W \<bullet> ?w3 = (0::'a)
normal_vector W \<bullet> normal_vector W \<noteq> (0::'a)
normal_vector W \<in> carrier_vec n
\<lbrakk>\<And>x. x \<in> ?S \<Longrightarrow> ?v \<bullet> x = (0::'a); ?S \<subseteq> carrier_vec n; ?v \<in> carrier_vec n; ?y \<in> local.span ?S\<rbrakk> \<Longrightarrow> ?v \<bullet> ?y = (0::'a)

goal (1 subgoal):
 1. normal_vector W \<notin> local.span W
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
normal_vector W \<notin> local.span W

goal (2 subgoals):
 1. lin_indpt (insert (normal_vector W) W)
 2. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
with lin_dep_iff_in_span[OF W lin nv nvW]
[PROOF STATE]
proof (chain)
picking this:
(normal_vector W \<in> local.span W) = lin_dep (W \<union> {normal_vector W})
normal_vector W \<notin> local.span W
[PROOF STEP]
show "lin_indpt (insert ?nv W)"
[PROOF STATE]
proof (prove)
using this:
(normal_vector W \<in> local.span W) = lin_dep (W \<union> {normal_vector W})
normal_vector W \<notin> local.span W

goal (1 subgoal):
 1. lin_indpt (insert (normal_vector W) W)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (insert (normal_vector W) W)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
lin_indpt (insert (normal_vector W) W)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
assume db: "is_det_bound db"
[PROOF STATE]
proof (state)
this:
is_det_bound db

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
assume "W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)"
[PROOF STATE]
proof (state)
this:
W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
hence wsI: "set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)"
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have ws: "set ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ws \<subseteq> carrier_vec n
[PROOF STEP]
using W
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n

goal (1 subgoal):
 1. set ws \<subseteq> carrier_vec n
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
W \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from wsI ws
[PROOF STATE]
proof (chain)
picking this:
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
set ws \<subseteq> carrier_vec n
[PROOF STEP]
have wsI: "i < ?n \<Longrightarrow> ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n" for i
[PROOF STATE]
proof (prove)
using this:
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
set ws \<subseteq> carrier_vec n

goal (1 subgoal):
 1. i < length ws \<Longrightarrow> ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n
[PROOF STEP]
using len wsI
[PROOF STATE]
proof (prove)
using this:
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
set ws \<subseteq> carrier_vec n
Suc (length ws) = n
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. i < length ws \<Longrightarrow> ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
using this:
{ws ! i |i. i < length ws} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
{ws ! i |i. i < length ws} \<subseteq> carrier_vec n
Suc (length ws) = n
{ws ! i |i. i < length ws} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. i < length ws \<Longrightarrow> ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i3 < length ws \<Longrightarrow> ws ! ?i3 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have ints: "i < ?n \<Longrightarrow> j < n \<Longrightarrow> ws ! i $ j \<in> \<int>" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> ws ! i $ j \<in> \<int>
[PROOF STEP]
using wsI[of i, unfolded Ints_vec_def]
[PROOF STATE]
proof (prove)
using this:
i < length ws \<Longrightarrow> ws ! i \<in> {x. \<forall>i<dim_vec x. x $ i \<in> \<int>} \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n

goal (1 subgoal):
 1. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> ws ! i $ j \<in> \<int>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i3 < length ws; ?j3 < n\<rbrakk> \<Longrightarrow> ws ! ?i3 $ ?j3 \<in> \<int>

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have bnd: "i < ?n \<Longrightarrow> j < n \<Longrightarrow> abs (ws ! i $ j) \<le> of_int Bnd" for i j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd
[PROOF STEP]
using wsI[unfolded Bounded_vec_def, of i]
[PROOF STATE]
proof (prove)
using this:
i < length ws \<Longrightarrow> ws ! i \<in> \<int>\<^sub>v \<inter> {x. \<forall>i<dim_vec x. \<bar>x $ i\<bar> \<le> of_int Bnd} \<inter> carrier_vec n

goal (1 subgoal):
 1. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i3 < length ws; ?j3 < n\<rbrakk> \<Longrightarrow> \<bar>ws ! ?i3 $ ?j3\<bar> \<le> of_int Bnd

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?i3 < length ws; ?j3 < n\<rbrakk> \<Longrightarrow> \<bar>ws ! ?i3 $ ?j3\<bar> \<le> of_int Bnd

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
assume i: "i < n"
[PROOF STATE]
proof (state)
this:
i < n

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have ints_nv: "nv $ i \<in> \<int>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nv $ i \<in> \<int>
[PROOF STEP]
unfolding nv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) $ i \<in> \<int>
[PROOF STEP]
using wsI len ws
[PROOF STATE]
proof (prove)
using this:
?i3 < length ws \<Longrightarrow> ws ! ?i3 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n
Suc (length ws) = n
set ws \<subseteq> carrier_vec n

goal (1 subgoal):
 1. vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) $ i \<in> \<int>
[PROOF STEP]
by (auto simp: i B_def set_conv_nth intro!: Ints_mult Ints_det ints)
[PROOF STATE]
proof (state)
this:
nv $ i \<in> \<int>

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
have "B i \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B i \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
[PROOF STEP]
unfolding B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat (length ws) (length ws) (\<lambda>(ia, j'). ws ! ia $ (if j' < i then j' else Suc j')) \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
[PROOF STEP]
using len ws i bnd ints_nv
[PROOF STATE]
proof (prove)
using this:
Suc (length ws) = n
set ws \<subseteq> carrier_vec n
i < n
\<lbrakk>?i3 < length ws; ?j3 < n\<rbrakk> \<Longrightarrow> \<bar>ws ! ?i3 $ ?j3\<bar> \<le> of_int Bnd
nv $ i \<in> \<int>

goal (1 subgoal):
 1. mat (length ws) (length ws) (\<lambda>(ia, j'). ws ! ia $ (if j' < i then j' else Suc j')) \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)
[PROOF STEP]
apply (simp add: Ints_mat_def Ints_vec_def Bounded_mat_def, intro allI impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ia j. \<lbrakk>Suc (length ws) = n; set ws \<subseteq> carrier_vec n; i < n; \<And>i j. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd; nv $ i \<in> \<int>; Suc (length ws) = n; set ws \<subseteq> carrier_vec n; i < n; \<And>i j. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd; nv $ i \<in> \<int>; ia < length ws\<rbrakk> \<Longrightarrow> (j < i \<longrightarrow> ws ! ia $ j \<in> \<int>) \<and> (\<not> j < i \<longrightarrow> j < length ws \<longrightarrow> ws ! ia $ Suc j \<in> \<int>)
[PROOF STEP]
subgoal for ii j
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc (length ws) = n; set ws \<subseteq> carrier_vec n; i < n; \<And>i j. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd; nv $ i \<in> \<int>; Suc (length ws) = n; set ws \<subseteq> carrier_vec n; i < n; \<And>i j. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd; nv $ i \<in> \<int>; ii < length ws\<rbrakk> \<Longrightarrow> (j < i \<longrightarrow> ws ! ii $ j \<in> \<int>) \<and> (\<not> j < i \<longrightarrow> j < length ws \<longrightarrow> ws ! ii $ Suc j \<in> \<int>)
[PROOF STEP]
using ints[of ii j] ints[of ii "Suc j"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>ii < length ws; j < n\<rbrakk> \<Longrightarrow> ws ! ii $ j \<in> \<int>
\<lbrakk>ii < length ws; Suc j < n\<rbrakk> \<Longrightarrow> ws ! ii $ Suc j \<in> \<int>

goal (1 subgoal):
 1. \<lbrakk>Suc (length ws) = n; set ws \<subseteq> carrier_vec n; i < n; \<And>i j. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd; nv $ i \<in> \<int>; Suc (length ws) = n; set ws \<subseteq> carrier_vec n; i < n; \<And>i j. \<lbrakk>i < length ws; j < n\<rbrakk> \<Longrightarrow> \<bar>ws ! i $ j\<bar> \<le> of_int Bnd; nv $ i \<in> \<int>; ii < length ws\<rbrakk> \<Longrightarrow> (j < i \<longrightarrow> ws ! ii $ j \<in> \<int>) \<and> (\<not> j < i \<longrightarrow> j < length ws \<longrightarrow> ws ! ii $ Suc j \<in> \<int>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
B i \<in> \<int>\<^sub>m \<inter> Bounded_mat (of_int Bnd)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
from is_det_bound_of_int[OF db _ this, of ?n]
[PROOF STATE]
proof (chain)
picking this:
B i \<in> carrier_mat (length ws) (length ws) \<Longrightarrow> \<bar>det (B i)\<bar> \<le> of_int (db (length ws) Bnd)
[PROOF STEP]
have "\<bar>nv $ i\<bar> \<le> of_int (db (n - 1) Bnd)"
[PROOF STATE]
proof (prove)
using this:
B i \<in> carrier_mat (length ws) (length ws) \<Longrightarrow> \<bar>det (B i)\<bar> \<le> of_int (db (length ws) Bnd)

goal (1 subgoal):
 1. \<bar>nv $ i\<bar> \<le> of_int (db (n - 1) Bnd)
[PROOF STEP]
unfolding nv_def
[PROOF STATE]
proof (prove)
using this:
B i \<in> carrier_mat (length ws) (length ws) \<Longrightarrow> \<bar>det (B i)\<bar> \<le> of_int (db (length ws) Bnd)

goal (1 subgoal):
 1. \<bar>vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) $ i\<bar> \<le> of_int (db (n - 1) Bnd)
[PROOF STEP]
using wsI len ws i
[PROOF STATE]
proof (prove)
using this:
B i \<in> carrier_mat (length ws) (length ws) \<Longrightarrow> \<bar>det (B i)\<bar> \<le> of_int (db (length ws) Bnd)
?i3 < length ws \<Longrightarrow> ws ! ?i3 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<inter> carrier_vec n
Suc (length ws) = n
set ws \<subseteq> carrier_vec n
i < n

goal (1 subgoal):
 1. \<bar>vec n (\<lambda>j. (- (1::'a)) ^ (length ws + j) * det (B j)) $ i\<bar> \<le> of_int (db (n - 1) Bnd)
[PROOF STEP]
by (auto simp: B_def abs_mult bnd)
[PROOF STATE]
proof (state)
this:
\<bar>nv $ i\<bar> \<le> of_int (db (n - 1) Bnd)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
note ints_nv this
[PROOF STATE]
proof (state)
this:
nv $ i \<in> \<int>
\<bar>nv $ i\<bar> \<le> of_int (db (n - 1) Bnd)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i5 < n \<Longrightarrow> nv $ ?i5 \<in> \<int>
?i5 < n \<Longrightarrow> \<bar>nv $ ?i5\<bar> \<le> of_int (db (n - 1) Bnd)

goal (1 subgoal):
 1. \<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
with nv nv2
[PROOF STATE]
proof (chain)
picking this:
normal_vector W \<in> carrier_vec n
normal_vector W = nv
?i5 < n \<Longrightarrow> nv $ ?i5 \<in> \<int>
?i5 < n \<Longrightarrow> \<bar>nv $ ?i5\<bar> \<le> of_int (db (n - 1) Bnd)
[PROOF STEP]
show "?nv \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))"
[PROOF STATE]
proof (prove)
using this:
normal_vector W \<in> carrier_vec n
normal_vector W = nv
?i5 < n \<Longrightarrow> nv $ ?i5 \<in> \<int>
?i5 < n \<Longrightarrow> \<bar>nv $ ?i5\<bar> \<le> of_int (db (n - 1) Bnd)

goal (1 subgoal):
 1. normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))
[PROOF STEP]
unfolding Ints_vec_def Bounded_vec_def
[PROOF STATE]
proof (prove)
using this:
normal_vector W \<in> carrier_vec n
normal_vector W = nv
?i5 < n \<Longrightarrow> nv $ ?i5 \<in> \<int>
?i5 < n \<Longrightarrow> \<bar>nv $ ?i5\<bar> \<le> of_int (db (n - 1) Bnd)

goal (1 subgoal):
 1. normal_vector W \<in> {x. \<forall>i<dim_vec x. x $ i \<in> \<int>} \<inter> {x. \<forall>i<dim_vec x. \<bar>x $ i\<bar> \<le> of_int (db (n - 1) Bnd)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_det_bound db; W \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> normal_vector W \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) Bnd))

goal:
No subgoals!
[PROOF STEP]
qed