[STATEMENT]
lemma normal_vectors:
  assumes lin: "lin_indpt_list ws"
  shows "set (normal_vectors ws) \<subseteq> carrier_vec n"
    "w \<in> set ws \<Longrightarrow> nv \<in> set (normal_vectors ws) \<Longrightarrow> nv \<bullet> w = 0"
    "w \<in> set ws \<Longrightarrow> nv \<in> set (normal_vectors ws) \<Longrightarrow> w \<bullet> nv = 0"
    "lin_indpt_list (ws @ normal_vectors ws)"
    "length ws + length (normal_vectors ws) = n"
    "set ws \<inter> set (normal_vectors ws) = {}"
    "is_det_bound db \<Longrightarrow> set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd) \<Longrightarrow>
       set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n-1) (max 1 Bnd)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set (normal_vectors ws) \<subseteq> carrier_vec n &&& (\<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)) &&& (\<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a))) &&& (lin_indpt_list (ws @ normal_vectors ws) &&& length ws + length (normal_vectors ws) = n) &&& set ws \<inter> set (normal_vectors ws) = {} &&& (\<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
define us where "us = basis_extension ws"
[PROOF STATE]
proof (state)
this:
us = basis_extension ws

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from basis_extension[OF assms, folded us_def]
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> set (unit_vecs n)
lin_indpt_list (ws @ us)
length (ws @ us) = n
[PROOF STEP]
have units: "set us \<subseteq> set (unit_vecs n)"
    and lin: "lin_indpt_list (ws @ us)"
    and len: "length (ws @ us) = n"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> set (unit_vecs n)
lin_indpt_list (ws @ us)
length (ws @ us) = n

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from lin_indpt_list_length_eq_n[OF lin len]
[PROOF STATE]
proof (chain)
picking this:
local.span (set (ws @ us)) = carrier_vec n
basis (set (ws @ us))
[PROOF STEP]
have span: "span (set (ws @ us)) = carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
local.span (set (ws @ us)) = carrier_vec n
basis (set (ws @ us))

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from lin[unfolded lin_indpt_list_def]
[PROOF STATE]
proof (chain)
picking this:
set (ws @ us) \<subseteq> carrier_vec n \<and> distinct (ws @ us) \<and> lin_indpt (set (ws @ us))
[PROOF STEP]
have wsus: "set (ws @ us) \<subseteq> carrier_vec n"
    and dist: "distinct (ws @ us)"
    and lin': "lin_indpt (set (ws @ us))"
[PROOF STATE]
proof (prove)
using this:
set (ws @ us) \<subseteq> carrier_vec n \<and> distinct (ws @ us) \<and> lin_indpt (set (ws @ us))

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
let ?nv = "normal_vectors ws"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
note nv_def = normal_vectors_def[of ws, unfolded Let_def, folded us_def]
[PROOF STATE]
proof (state)
this:
normal_vectors ws = map (\<lambda>i. normal_vector (set (ws @ us) - {us ! i})) [0..<length us]

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
let ?m = "length ws"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
let ?n = "length us"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
have lnv[simp]: "length ?nv = length us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (normal_vectors ws) = length us
[PROOF STEP]
unfolding nv_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. normal_vector (set (ws @ us) - {us ! i})) [0..<length us]) = length us
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (normal_vectors ws) = length us

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length (normal_vectors ws) = length us

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
let ?V = "set (ws @ us) - {us ! i}"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
assume i: "i < ?n"
[PROOF STATE]
proof (state)
this:
i < length us

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
hence nvi: "?nv ! i = normal_vector ?V"
[PROOF STATE]
proof (prove)
using this:
i < length us

goal (1 subgoal):
 1. normal_vectors ws ! i = normal_vector (set (ws @ us) - {us ! i})
[PROOF STEP]
unfolding nv_def
[PROOF STATE]
proof (prove)
using this:
i < length us

goal (1 subgoal):
 1. map (\<lambda>i. normal_vector (set (ws @ us) - {us ! i})) [0..<length us] ! i = normal_vector (set (ws @ us) - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i = normal_vector (set (ws @ us) - {us ! i})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < length us
[PROOF STEP]
have "us ! i \<in> set us"
[PROOF STATE]
proof (prove)
using this:
i < length us

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
with wsus
[PROOF STATE]
proof (chain)
picking this:
set (ws @ us) \<subseteq> carrier_vec n
us ! i \<in> set us
[PROOF STEP]
have u: "us ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set (ws @ us) \<subseteq> carrier_vec n
us ! i \<in> set us

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
have id: "?V \<union> {us ! i} = set (ws @ us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ws @ us) - {us ! i} \<union> {us ! i} = set (ws @ us)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length us

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
have V: "?V \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ws @ us) - {us ! i} \<subseteq> carrier_vec n
[PROOF STEP]
using wsus
[PROOF STATE]
proof (prove)
using this:
set (ws @ us) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. set (ws @ us) - {us ! i} \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (ws @ us) - {us ! i} \<subseteq> carrier_vec n

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
have finV: "finite ?V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (set (ws @ us) - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite (set (ws @ us) - {us ! i})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
have "Suc (card ?V) = card (insert (us ! i) ?V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (card (set (ws @ us) - {us ! i})) = card (insert (us ! i) (set (ws @ us) - {us ! i}))
[PROOF STEP]
by (subst card_insert_disjoint[OF finV], auto)
[PROOF STATE]
proof (state)
this:
Suc (card (set (ws @ us) - {us ! i})) = card (insert (us ! i) (set (ws @ us) - {us ! i}))

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (card (set (ws @ us) - {us ! i})) = card (insert (us ! i) (set (ws @ us) - {us ! i}))

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
have "insert (us ! i) ?V = set (ws @ us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert (us ! i) (set (ws @ us) - {us ! i}) = set (ws @ us)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < length us

goal (1 subgoal):
 1. insert (us ! i) (set (ws @ us) - {us ! i}) = set (ws @ us)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert (us ! i) (set (ws @ us) - {us ! i}) = set (ws @ us)

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Suc (card (set (ws @ us) - {us ! i})) = card (set (ws @ us))
[PROOF STEP]
have cardV: "Suc (card ?V) = n"
[PROOF STATE]
proof (prove)
using this:
Suc (card (set (ws @ us) - {us ! i})) = card (set (ws @ us))

goal (1 subgoal):
 1. Suc (card (set (ws @ us) - {us ! i})) = n
[PROOF STEP]
using len distinct_card[OF dist]
[PROOF STATE]
proof (prove)
using this:
Suc (card (set (ws @ us) - {us ! i})) = card (set (ws @ us))
length (ws @ us) = n
card (set (ws @ us)) = length (ws @ us)

goal (1 subgoal):
 1. Suc (card (set (ws @ us) - {us ! i})) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (card (set (ws @ us) - {us ! i})) = n

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from subset_li_is_li[OF lin']
[PROOF STATE]
proof (chain)
picking this:
?B \<subseteq> set (ws @ us) \<Longrightarrow> lin_indpt ?B
[PROOF STEP]
have linV: "lin_indpt ?V"
[PROOF STATE]
proof (prove)
using this:
?B \<subseteq> set (ws @ us) \<Longrightarrow> lin_indpt ?B

goal (1 subgoal):
 1. lin_indpt (set (ws @ us) - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lin_indpt (set (ws @ us) - {us ! i})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from lin_dep_iff_in_span[OF _ linV u, unfolded id] wsus lin'
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>set (ws @ us) - {us ! i} \<subseteq> carrier_vec n; us ! i \<notin> set (ws @ us) - {us ! i}\<rbrakk> \<Longrightarrow> (us ! i \<in> local.span (set (ws @ us) - {us ! i})) = lin_dep (set (ws @ us))
set (ws @ us) \<subseteq> carrier_vec n
lin_indpt (set (ws @ us))
[PROOF STEP]
have usV: "us ! i \<notin> span ?V"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>set (ws @ us) - {us ! i} \<subseteq> carrier_vec n; us ! i \<notin> set (ws @ us) - {us ! i}\<rbrakk> \<Longrightarrow> (us ! i \<in> local.span (set (ws @ us) - {us ! i})) = lin_dep (set (ws @ us))
set (ws @ us) \<subseteq> carrier_vec n
lin_indpt (set (ws @ us))

goal (1 subgoal):
 1. us ! i \<notin> local.span (set (ws @ us) - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i \<notin> local.span (set (ws @ us) - {us ! i})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
note nv = normal_vector[OF finV cardV linV V, folded nvi]
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i \<in> carrier_vec n
normal_vectors ws ! i \<noteq> 0\<^sub>v n
?w \<in> set (ws @ us) - {us ! i} \<Longrightarrow> ?w \<bullet> normal_vectors ws ! i = (0::'a)
?w \<in> set (ws @ us) - {us ! i} \<Longrightarrow> normal_vectors ws ! i \<bullet> ?w = (0::'a)
lin_indpt (insert (normal_vectors ws ! i) (set (ws @ us) - {us ! i}))
normal_vectors ws ! i \<notin> set (ws @ us) - {us ! i}
\<lbrakk>is_det_bound ?db; set (ws @ us) - {us ! i} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vectors ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from normal_vector_span[OF cardV V _ linV, folded nvi] comm_scalar_prod[OF _ nv(1)]
[PROOF STATE]
proof (chain)
picking this:
finite (set (ws @ us) - {us ! i}) \<Longrightarrow> local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. x \<bullet> normal_vectors ws ! i = (0::'a)}
?v\<^sub>1 \<in> carrier_vec n \<Longrightarrow> ?v\<^sub>1 \<bullet> normal_vectors ws ! i = normal_vectors ws ! i \<bullet> ?v\<^sub>1
[PROOF STEP]
have span: "span ?V = {x \<in> carrier_vec n. ?nv ! i \<bullet> x = 0}"
[PROOF STATE]
proof (prove)
using this:
finite (set (ws @ us) - {us ! i}) \<Longrightarrow> local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. x \<bullet> normal_vectors ws ! i = (0::'a)}
?v\<^sub>1 \<in> carrier_vec n \<Longrightarrow> ?v\<^sub>1 \<bullet> normal_vectors ws ! i = normal_vectors ws ! i \<bullet> ?v\<^sub>1

goal (1 subgoal):
 1. local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from nv(1,2)
[PROOF STATE]
proof (chain)
picking this:
normal_vectors ws ! i \<in> carrier_vec n
normal_vectors ws ! i \<noteq> 0\<^sub>v n
[PROOF STEP]
have "sq_norm (?nv ! i) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
normal_vectors ws ! i \<in> carrier_vec n
normal_vectors ws ! i \<noteq> 0\<^sub>v n

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
hence nvi: "?nv ! i \<bullet> ?nv ! i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<parallel>normal_vectors ws ! i\<parallel>\<^sup>2 \<noteq> (0::'a)

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

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from span nvi
[PROOF STATE]
proof (chain)
picking this:
local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}
normal_vectors ws ! i \<bullet> normal_vectors ws ! i \<noteq> (0::'a)
[PROOF STEP]
have nvspan: "?nv ! i \<notin> span ?V"
[PROOF STATE]
proof (prove)
using this:
local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}
normal_vectors ws ! i \<bullet> normal_vectors ws ! i \<noteq> (0::'a)

goal (1 subgoal):
 1. normal_vectors ws ! i \<notin> local.span (set (ws @ us) - {us ! i})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i \<notin> local.span (set (ws @ us) - {us ! i})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from u usV[unfolded span]
[PROOF STATE]
proof (chain)
picking this:
us ! i \<in> carrier_vec n
us ! i \<notin> {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}
[PROOF STEP]
have "?nv ! i \<bullet> us ! i \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
us ! i \<in> carrier_vec n
us ! i \<notin> {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}

goal (1 subgoal):
 1. normal_vectors ws ! i \<bullet> us ! i \<noteq> (0::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i \<bullet> us ! i \<noteq> (0::'a)

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
note nv nvi this span usV nvspan
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i \<in> carrier_vec n
normal_vectors ws ! i \<noteq> 0\<^sub>v n
?w \<in> set (ws @ us) - {us ! i} \<Longrightarrow> ?w \<bullet> normal_vectors ws ! i = (0::'a)
?w \<in> set (ws @ us) - {us ! i} \<Longrightarrow> normal_vectors ws ! i \<bullet> ?w = (0::'a)
lin_indpt (insert (normal_vectors ws ! i) (set (ws @ us) - {us ! i}))
normal_vectors ws ! i \<notin> set (ws @ us) - {us ! i}
\<lbrakk>is_det_bound ?db; set (ws @ us) - {us ! i} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vectors ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))
normal_vectors ws ! i \<bullet> normal_vectors ws ! i \<noteq> (0::'a)
normal_vectors ws ! i \<bullet> us ! i \<noteq> (0::'a)
local.span (set (ws @ us) - {us ! i}) = {x \<in> carrier_vec n. normal_vectors ws ! i \<bullet> x = (0::'a)}
us ! i \<notin> local.span (set (ws @ us) - {us ! i})
normal_vectors ws ! i \<notin> local.span (set (ws @ us) - {us ! i})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<in> carrier_vec n
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<noteq> 0\<^sub>v n
\<lbrakk>?i5 < length us; ?w \<in> set (ws @ us) - {us ! ?i5}\<rbrakk> \<Longrightarrow> ?w \<bullet> normal_vectors ws ! ?i5 = (0::'a)
\<lbrakk>?i5 < length us; ?w \<in> set (ws @ us) - {us ! ?i5}\<rbrakk> \<Longrightarrow> normal_vectors ws ! ?i5 \<bullet> ?w = (0::'a)
?i5 < length us \<Longrightarrow> lin_indpt (insert (normal_vectors ws ! ?i5) (set (ws @ us) - {us ! ?i5}))
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<notin> set (ws @ us) - {us ! ?i5}
\<lbrakk>?i5 < length us; is_det_bound ?db; set (ws @ us) - {us ! ?i5} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vectors ws ! ?i5 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<bullet> normal_vectors ws ! ?i5 \<noteq> (0::'a)
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<bullet> us ! ?i5 \<noteq> (0::'a)
?i5 < length us \<Longrightarrow> local.span (set (ws @ us) - {us ! ?i5}) = {x \<in> carrier_vec n. normal_vectors ws ! ?i5 \<bullet> x = (0::'a)}
?i5 < length us \<Longrightarrow> us ! ?i5 \<notin> local.span (set (ws @ us) - {us ! ?i5})
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<notin> local.span (set (ws @ us) - {us ! ?i5})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
note nvi = this
[PROOF STATE]
proof (state)
this:
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<in> carrier_vec n
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<noteq> 0\<^sub>v n
\<lbrakk>?i5 < length us; ?w \<in> set (ws @ us) - {us ! ?i5}\<rbrakk> \<Longrightarrow> ?w \<bullet> normal_vectors ws ! ?i5 = (0::'a)
\<lbrakk>?i5 < length us; ?w \<in> set (ws @ us) - {us ! ?i5}\<rbrakk> \<Longrightarrow> normal_vectors ws ! ?i5 \<bullet> ?w = (0::'a)
?i5 < length us \<Longrightarrow> lin_indpt (insert (normal_vectors ws ! ?i5) (set (ws @ us) - {us ! ?i5}))
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<notin> set (ws @ us) - {us ! ?i5}
\<lbrakk>?i5 < length us; is_det_bound ?db; set (ws @ us) - {us ! ?i5} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int ?Bnd)\<rbrakk> \<Longrightarrow> normal_vectors ws ! ?i5 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (?db (n - 1) ?Bnd))
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<bullet> normal_vectors ws ! ?i5 \<noteq> (0::'a)
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<bullet> us ! ?i5 \<noteq> (0::'a)
?i5 < length us \<Longrightarrow> local.span (set (ws @ us) - {us ! ?i5}) = {x \<in> carrier_vec n. normal_vectors ws ! ?i5 \<bullet> x = (0::'a)}
?i5 < length us \<Longrightarrow> us ! ?i5 \<notin> local.span (set (ws @ us) - {us ! ?i5})
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<notin> local.span (set (ws @ us) - {us ! ?i5})

goal (7 subgoals):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 3. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 4. lin_indpt_list (ws @ normal_vectors ws)
 5. length ws + length (normal_vectors ws) = n
 6. set ws \<inter> set (normal_vectors ws) = {}
 7. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
show nv: "set ?nv \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (normal_vectors ws) \<subseteq> carrier_vec n
[PROOF STEP]
unfolding set_conv_nth
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {normal_vectors ws ! i |i. i < length (normal_vectors ws)} \<subseteq> carrier_vec n
[PROOF STEP]
using nvi(1)
[PROOF STATE]
proof (prove)
using this:
?i5 < length us \<Longrightarrow> normal_vectors ws ! ?i5 \<in> carrier_vec n

goal (1 subgoal):
 1. {normal_vectors ws ! i |i. i < length (normal_vectors ws)} \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (normal_vectors ws) \<subseteq> carrier_vec n

goal (6 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 3. lin_indpt_list (ws @ normal_vectors ws)
 4. length ws + length (normal_vectors ws) = n
 5. set ws \<inter> set (normal_vectors ws) = {}
 6. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set (normal_vectors ws) \<subseteq> carrier_vec n

goal (6 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 3. lin_indpt_list (ws @ normal_vectors ws)
 4. length ws + length (normal_vectors ws) = n
 5. set ws \<inter> set (normal_vectors ws) = {}
 6. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
fix w nv
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 3. lin_indpt_list (ws @ normal_vectors ws)
 4. length ws + length (normal_vectors ws) = n
 5. set ws \<inter> set (normal_vectors ws) = {}
 6. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
assume w: "w \<in> set ws"
[PROOF STATE]
proof (state)
this:
w \<in> set ws

goal (6 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 3. lin_indpt_list (ws @ normal_vectors ws)
 4. length ws + length (normal_vectors ws) = n
 5. set ws \<inter> set (normal_vectors ws) = {}
 6. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
with dist
[PROOF STATE]
proof (chain)
picking this:
distinct (ws @ us)
w \<in> set ws
[PROOF STEP]
have wus: "w \<notin> set us"
[PROOF STATE]
proof (prove)
using this:
distinct (ws @ us)
w \<in> set ws

goal (1 subgoal):
 1. w \<notin> set us
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<notin> set us

goal (6 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 3. lin_indpt_list (ws @ normal_vectors ws)
 4. length ws + length (normal_vectors ws) = n
 5. set ws \<inter> set (normal_vectors ws) = {}
 6. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
assume n: "nv \<in> set ?nv"
[PROOF STATE]
proof (state)
this:
nv \<in> set (normal_vectors ws)

goal (6 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> nv \<bullet> w = (0::'a)
 2. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 3. lin_indpt_list (ws @ normal_vectors ws)
 4. length ws + length (normal_vectors ws) = n
 5. set ws \<inter> set (normal_vectors ws) = {}
 6. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
with w wus
[PROOF STATE]
proof (chain)
picking this:
w \<in> set ws
w \<notin> set us
nv \<in> set (normal_vectors ws)
[PROOF STEP]
show "nv \<bullet> w = 0"
[PROOF STATE]
proof (prove)
using this:
w \<in> set ws
w \<notin> set us
nv \<in> set (normal_vectors ws)

goal (1 subgoal):
 1. nv \<bullet> w = (0::'a)
[PROOF STEP]
unfolding set_conv_nth[of "normal_vectors _"]
[PROOF STATE]
proof (prove)
using this:
w \<in> set ws
w \<notin> set us
nv \<in> {normal_vectors ws ! i |i. i < length (normal_vectors ws)}

goal (1 subgoal):
 1. nv \<bullet> w = (0::'a)
[PROOF STEP]
by (auto intro!: nvi(4)[of _ w])
[PROOF STATE]
proof (state)
this:
nv \<bullet> w = (0::'a)

goal (5 subgoals):
 1. \<lbrakk>w \<in> set ws; nv \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> w \<bullet> nv = (0::'a)
 2. lin_indpt_list (ws @ normal_vectors ws)
 3. length ws + length (normal_vectors ws) = n
 4. set ws \<inter> set (normal_vectors ws) = {}
 5. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
thus "w \<bullet> nv = 0"
[PROOF STATE]
proof (prove)
using this:
nv \<bullet> w = (0::'a)

goal (1 subgoal):
 1. w \<bullet> nv = (0::'a)
[PROOF STEP]
using comm_scalar_prod[of w n nv] w nv n wsus
[PROOF STATE]
proof (prove)
using this:
nv \<bullet> w = (0::'a)
\<lbrakk>w \<in> carrier_vec n; nv \<in> carrier_vec n\<rbrakk> \<Longrightarrow> w \<bullet> nv = nv \<bullet> w
w \<in> set ws
set (normal_vectors ws) \<subseteq> carrier_vec n
nv \<in> set (normal_vectors ws)
set (ws @ us) \<subseteq> carrier_vec n

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

goal (4 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. length ws + length (normal_vectors ws) = n
 3. set ws \<inter> set (normal_vectors ws) = {}
 4. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>?wa5 \<in> set ws; ?nva5 \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> ?wa5 \<bullet> ?nva5 = (0::'a)

goal (4 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. length ws + length (normal_vectors ws) = n
 3. set ws \<inter> set (normal_vectors ws) = {}
 4. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
note scalar_0 = this
[PROOF STATE]
proof (state)
this:
\<lbrakk>?wa5 \<in> set ws; ?nva5 \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> ?wa5 \<bullet> ?nva5 = (0::'a)

goal (4 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. length ws + length (normal_vectors ws) = n
 3. set ws \<inter> set (normal_vectors ws) = {}
 4. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
show "length ws + length ?nv = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ws + length (normal_vectors ws) = n
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
length (ws @ us) = n

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

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length ws + length (normal_vectors ws) = n

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
let ?oi = "of_int :: int \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
assume wsI: "set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (?oi Bnd)" and db: "is_det_bound db"
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
is_det_bound db

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
is_det_bound db

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
fix nv
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
assume "nv \<in> set ?nv"
[PROOF STATE]
proof (state)
this:
nv \<in> set (normal_vectors ws)

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
nv \<in> set (normal_vectors ws)
[PROOF STEP]
obtain i where nv: "nv = ?nv ! i" and i: "i < ?n"
[PROOF STATE]
proof (prove)
using this:
nv \<in> set (normal_vectors ws)

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

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

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from order.trans[OF units unit_vec_int_bounds]
        wsI
[PROOF STATE]
proof (chain)
picking this:
set us \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (max 1 ?Bnd1))
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
[PROOF STEP]
have "set (ws @ us) - {us ! i} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (?oi (max 1 Bnd))"
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (max 1 ?Bnd1))
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)

goal (1 subgoal):
 1. set (ws @ us) - {us ! i} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (max 1 Bnd))
[PROOF STEP]
using
          Bounded_vec_mono[of "?oi Bnd" "?oi (max 1 Bnd)", unfolded of_int_le_iff]
[PROOF STATE]
proof (prove)
using this:
set us \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (max 1 ?Bnd1))
set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)
Bnd \<le> max 1 Bnd \<Longrightarrow> Bounded_vec (of_int Bnd) \<subseteq> Bounded_vec (of_int (max 1 Bnd))

goal (1 subgoal):
 1. set (ws @ us) - {us ! i} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (max 1 Bnd))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (ws @ us) - {us ! i} \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (max 1 Bnd))

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
from nvi(7)[OF i db this] nv
[PROOF STATE]
proof (chain)
picking this:
normal_vectors ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
nv = normal_vectors ws ! i
[PROOF STEP]
have "nv \<in> \<int>\<^sub>v \<inter> Bounded_vec (?oi (db (n - 1) (max 1 Bnd)))"
[PROOF STATE]
proof (prove)
using this:
normal_vectors ws ! i \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
nv = normal_vectors ws ! i

goal (1 subgoal):
 1. nv \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nv \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?nva5 \<in> set (normal_vectors ws) \<Longrightarrow> ?nva5 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))

goal (3 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
 3. \<lbrakk>is_det_bound db; set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd)\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))
[PROOF STEP]
thus "set ?nv \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (?oi (db (n - 1) (max 1 Bnd)))"
[PROOF STATE]
proof (prove)
using this:
?nva5 \<in> set (normal_vectors ws) \<Longrightarrow> ?nva5 \<in> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))

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

goal (2 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set ws \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int Bnd); is_det_bound db\<rbrakk> \<Longrightarrow> set (normal_vectors ws) \<subseteq> \<int>\<^sub>v \<inter> Bounded_vec (of_int (db (n - 1) (max 1 Bnd)))

goal (2 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
[PROOF STEP]
have dist_nv: "distinct ?nv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (normal_vectors ws)
[PROOF STEP]
unfolding distinct_conv_nth lnv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length us. \<forall>j<length us. i \<noteq> j \<longrightarrow> normal_vectors ws ! i \<noteq> normal_vectors ws ! j
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < length us; j < length us; i \<noteq> j\<rbrakk> \<Longrightarrow> normal_vectors ws ! i \<noteq> normal_vectors ws ! j
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < length us; j < length us; i \<noteq> j\<rbrakk> \<Longrightarrow> normal_vectors ws ! i \<noteq> normal_vectors ws ! j
[PROOF STEP]
assume i: "i < ?n" and j: "j < ?n" and ij: "i \<noteq> j"
[PROOF STATE]
proof (state)
this:
i < length us
j < length us
i \<noteq> j

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < length us; j < length us; i \<noteq> j\<rbrakk> \<Longrightarrow> normal_vectors ws ! i \<noteq> normal_vectors ws ! j
[PROOF STEP]
with dist
[PROOF STATE]
proof (chain)
picking this:
distinct (ws @ us)
i < length us
j < length us
i \<noteq> j
[PROOF STEP]
have usj: "us ! j \<in> set (ws @ us) - {us ! i}"
[PROOF STATE]
proof (prove)
using this:
distinct (ws @ us)
i < length us
j < length us
i \<noteq> j

goal (1 subgoal):
 1. us ! j \<in> set (ws @ us) - {us ! i}
[PROOF STEP]
by (simp, auto simp: distinct_conv_nth set_conv_nth)
[PROOF STATE]
proof (state)
this:
us ! j \<in> set (ws @ us) - {us ! i}

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>i < length us; j < length us; i \<noteq> j\<rbrakk> \<Longrightarrow> normal_vectors ws ! i \<noteq> normal_vectors ws ! j
[PROOF STEP]
from nvi(4)[OF i this] nvi(9)[OF j]
[PROOF STATE]
proof (chain)
picking this:
normal_vectors ws ! i \<bullet> us ! j = (0::'a)
normal_vectors ws ! j \<bullet> us ! j \<noteq> (0::'a)
[PROOF STEP]
show "?nv ! i \<noteq> ?nv ! j"
[PROOF STATE]
proof (prove)
using this:
normal_vectors ws ! i \<bullet> us ! j = (0::'a)
normal_vectors ws ! j \<bullet> us ! j \<noteq> (0::'a)

goal (1 subgoal):
 1. normal_vectors ws ! i \<noteq> normal_vectors ws ! j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i \<noteq> normal_vectors ws ! j

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

goal (2 subgoals):
 1. lin_indpt_list (ws @ normal_vectors ws)
 2. set ws \<inter> set (normal_vectors ws) = {}
[PROOF STEP]
show disj: "set ws \<inter> set ?nv = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set ws \<inter> set (normal_vectors ws) = {}
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. set ws \<inter> set (normal_vectors ws) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
assume "\<not> ?thesis"
[PROOF STATE]
proof (state)
this:
set ws \<inter> set (normal_vectors ws) \<noteq> {}

goal (1 subgoal):
 1. set ws \<inter> set (normal_vectors ws) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
set ws \<inter> set (normal_vectors ws) \<noteq> {}
[PROOF STEP]
obtain w where w: "w \<in> set ws" "w \<in> set ?nv"
[PROOF STATE]
proof (prove)
using this:
set ws \<inter> set (normal_vectors ws) \<noteq> {}

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

goal (1 subgoal):
 1. set ws \<inter> set (normal_vectors ws) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
from scalar_0[OF this] this(1)
[PROOF STATE]
proof (chain)
picking this:
w \<bullet> w = (0::'a)
w \<in> set ws
[PROOF STEP]
have "sq_norm w = 0"
[PROOF STATE]
proof (prove)
using this:
w \<bullet> w = (0::'a)
w \<in> set ws

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

goal (1 subgoal):
 1. set ws \<inter> set (normal_vectors ws) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with w wsus
[PROOF STATE]
proof (chain)
picking this:
w \<in> set ws
w \<in> set (normal_vectors ws)
set (ws @ us) \<subseteq> carrier_vec n
\<parallel>w\<parallel>\<^sup>2 = (0::'a)
[PROOF STEP]
have "w = 0\<^sub>v n"
[PROOF STATE]
proof (prove)
using this:
w \<in> set ws
w \<in> set (normal_vectors ws)
set (ws @ us) \<subseteq> carrier_vec n
\<parallel>w\<parallel>\<^sup>2 = (0::'a)

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

goal (1 subgoal):
 1. set ws \<inter> set (normal_vectors ws) \<noteq> {} \<Longrightarrow> False
[PROOF STEP]
with vs_zero_lin_dep[OF wsus lin'] w(1)
[PROOF STATE]
proof (chain)
picking this:
0\<^sub>v n \<notin> set (ws @ us)
w \<in> set ws
w = 0\<^sub>v n
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
0\<^sub>v n \<notin> set (ws @ us)
w \<in> set ws
w = 0\<^sub>v n

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:
set ws \<inter> set (normal_vectors ws) = {}

goal (1 subgoal):
 1. lin_indpt_list (ws @ normal_vectors ws)
[PROOF STEP]
have dist': "distinct (ws @ ?nv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (ws @ normal_vectors ws)
[PROOF STEP]
using dist disj dist_nv
[PROOF STATE]
proof (prove)
using this:
distinct (ws @ us)
set ws \<inter> set (normal_vectors ws) = {}
distinct (normal_vectors ws)

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

goal (1 subgoal):
 1. lin_indpt_list (ws @ normal_vectors ws)
[PROOF STEP]
show "lin_indpt_list (ws @ ?nv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt_list (ws @ normal_vectors ws)
[PROOF STEP]
unfolding lin_indpt_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ws @ normal_vectors ws) \<subseteq> carrier_vec n \<and> distinct (ws @ normal_vectors ws) \<and> lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
proof (intro conjI dist')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. set (ws @ normal_vectors ws) \<subseteq> carrier_vec n
 2. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
show set: "set (ws @ ?nv) \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ws @ normal_vectors ws) \<subseteq> carrier_vec n
[PROOF STEP]
using nv wsus
[PROOF STATE]
proof (prove)
using this:
set (normal_vectors ws) \<subseteq> carrier_vec n
set (ws @ us) \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
hence ws: "set ws \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
set (ws @ normal_vectors ws) \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
have lin_nv: "lin_indpt (set ?nv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lin_indpt (set (normal_vectors ws))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
assume "lin_dep (set ?nv)"
[PROOF STATE]
proof (state)
this:
lin_dep (set (normal_vectors ws))

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
from finite_lin_dep[OF finite_set this nv]
[PROOF STATE]
proof (chain)
picking this:
\<exists>a v. True \<and> lincomb a (set (normal_vectors ws)) = 0\<^sub>v n \<and> v \<in> set (normal_vectors ws) \<and> a v \<noteq> (0::'a)
[PROOF STEP]
obtain a v where comb: "lincomb a (set ?nv) = 0\<^sub>v n" and vnv: "v \<in> set ?nv" and av0: "a v \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>a v. True \<and> lincomb a (set (normal_vectors ws)) = 0\<^sub>v n \<and> v \<in> set (normal_vectors ws) \<and> a v \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<And>a v. \<lbrakk>lincomb a (set (normal_vectors ws)) = 0\<^sub>v n; v \<in> set (normal_vectors ws); a v \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lincomb a (set (normal_vectors ws)) = 0\<^sub>v n
v \<in> set (normal_vectors ws)
a v \<noteq> (0::'a)

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
from vnv[unfolded set_conv_nth]
[PROOF STATE]
proof (chain)
picking this:
v \<in> {normal_vectors ws ! i |i. i < length (normal_vectors ws)}
[PROOF STEP]
obtain i where i: "i < ?n" and vi: "v = ?nv ! i"
[PROOF STATE]
proof (prove)
using this:
v \<in> {normal_vectors ws ! i |i. i < length (normal_vectors ws)}

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

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
define b where "b = (\<lambda> w. a w / a v)"
[PROOF STATE]
proof (state)
this:
b = (\<lambda>w. a w / a v)

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
define c where "c = (\<lambda> w. -1 * b w)"
[PROOF STATE]
proof (state)
this:
c = (\<lambda>w. - (1::'a) * b w)

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
define x where "x = lincomb b (set ?nv - {v})"
[PROOF STATE]
proof (state)
this:
x = lincomb b (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
define w where "w = lincomb c (set ?nv - {v})"
[PROOF STATE]
proof (state)
this:
w = lincomb c (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have w: "w \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<in> carrier_vec n
[PROOF STEP]
unfolding w_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (set (normal_vectors ws) - {v}) \<in> carrier_vec n
[PROOF STEP]
using nv
[PROOF STATE]
proof (prove)
using this:
set (normal_vectors ws) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb c (set (normal_vectors ws) - {v}) \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<in> carrier_vec n

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have x: "x \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> carrier_vec n
[PROOF STEP]
unfolding x_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb b (set (normal_vectors ws) - {v}) \<in> carrier_vec n
[PROOF STEP]
using nv
[PROOF STATE]
proof (prove)
using this:
set (normal_vectors ws) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lincomb b (set (normal_vectors ws) - {v}) \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> carrier_vec n

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
from arg_cong[OF comb, of "\<lambda> x. (1/ a v) \<cdot>\<^sub>v x"]
[PROOF STATE]
proof (chain)
picking this:
(1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws)) = (1::'a) / a v \<cdot>\<^sub>v 0\<^sub>v n
[PROOF STEP]
have "0\<^sub>v n = 1 / a v \<cdot>\<^sub>v lincomb a (set ?nv)"
[PROOF STATE]
proof (prove)
using this:
(1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws)) = (1::'a) / a v \<cdot>\<^sub>v 0\<^sub>v n

goal (1 subgoal):
 1. 0\<^sub>v n = (1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>v n = (1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws))

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0\<^sub>v n = (1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws))

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = lincomb b (set ?nv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws)) = lincomb b (set (normal_vectors ws))
[PROOF STEP]
by (subst lincomb_smult[symmetric, OF nv], auto simp: b_def)
[PROOF STATE]
proof (state)
this:
(1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws)) = lincomb b (set (normal_vectors ws))

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(1::'a) / a v \<cdot>\<^sub>v lincomb a (set (normal_vectors ws)) = lincomb b (set (normal_vectors ws))

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> = b v \<cdot>\<^sub>v v + lincomb b (set ?nv - {v})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb b (set (normal_vectors ws)) = b v \<cdot>\<^sub>v v + lincomb b (set (normal_vectors ws) - {v})
[PROOF STEP]
by (subst lincomb_del2[OF _ nv _ vnv], auto)
[PROOF STATE]
proof (state)
this:
lincomb b (set (normal_vectors ws)) = b v \<cdot>\<^sub>v v + lincomb b (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lincomb b (set (normal_vectors ws)) = b v \<cdot>\<^sub>v v + lincomb b (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have "b v \<cdot>\<^sub>v v = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b v \<cdot>\<^sub>v v = v
[PROOF STEP]
using av0
[PROOF STATE]
proof (prove)
using this:
a v \<noteq> (0::'a)

goal (1 subgoal):
 1. b v \<cdot>\<^sub>v v = v
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
using this:
a v \<noteq> (0::'a)

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

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0\<^sub>v n = v + lincomb b (set (normal_vectors ws) - {v})
[PROOF STEP]
have "v + lincomb b (set ?nv - {v}) - lincomb b (set ?nv - {v}) =
         0\<^sub>v n - lincomb b (set ?nv - {v})" (is "?l = ?r")
[PROOF STATE]
proof (prove)
using this:
0\<^sub>v n = v + lincomb b (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. v + lincomb b (set (normal_vectors ws) - {v}) - lincomb b (set (normal_vectors ws) - {v}) = 0\<^sub>v n - lincomb b (set (normal_vectors ws) - {v})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
v + lincomb b (set (normal_vectors ws) - {v}) - lincomb b (set (normal_vectors ws) - {v}) = 0\<^sub>v n - lincomb b (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v + lincomb b (set (normal_vectors ws) - {v}) - lincomb b (set (normal_vectors ws) - {v}) = 0\<^sub>v n - lincomb b (set (normal_vectors ws) - {v})

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have "?l = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v + lincomb b (set (normal_vectors ws) - {v}) - lincomb b (set (normal_vectors ws) - {v}) = v
[PROOF STEP]
by (rule add_diff_cancel_right_vec, insert vnv nv, auto)
[PROOF STATE]
proof (state)
this:
v + lincomb b (set (normal_vectors ws) - {v}) - lincomb b (set (normal_vectors ws) - {v}) = v

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
v + lincomb b (set (normal_vectors ws) - {v}) - lincomb b (set (normal_vectors ws) - {v}) = v

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have "?r = w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n - lincomb b (set (normal_vectors ws) - {v}) = w
[PROOF STEP]
unfolding w_def c_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v n - lincomb b (set (normal_vectors ws) - {v}) = lincomb (\<lambda>w. - (1::'a) * b w) (set (normal_vectors ws) - {v})
[PROOF STEP]
by (subst lincomb_smult, unfold x_def[symmetric], insert nv x, auto)
[PROOF STATE]
proof (state)
this:
0\<^sub>v n - lincomb b (set (normal_vectors ws) - {v}) = w

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
v = w
[PROOF STEP]
have vw: "v = w"
[PROOF STATE]
proof (prove)
using this:
v = w

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

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have u: "us ! i \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. us ! i \<in> carrier_vec n
[PROOF STEP]
using i wsus
[PROOF STATE]
proof (prove)
using this:
i < length us
set (ws @ us) \<subseteq> carrier_vec n

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

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have nv': "set ?nv - {?nv ! i} \<subseteq> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (normal_vectors ws) - {normal_vectors ws ! i} \<subseteq> carrier_vec n
[PROOF STEP]
using nv
[PROOF STATE]
proof (prove)
using this:
set (normal_vectors ws) \<subseteq> carrier_vec n

goal (1 subgoal):
 1. set (normal_vectors ws) - {normal_vectors ws ! i} \<subseteq> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (normal_vectors ws) - {normal_vectors ws ! i} \<subseteq> carrier_vec n

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
have "?nv ! i \<bullet> us ! i = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_vectors ws ! i \<bullet> us ! i = (0::'a)
[PROOF STEP]
unfolding vi[symmetric] vw
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<bullet> us ! i = (0::'a)
[PROOF STEP]
unfolding w_def vi
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lincomb c (set (normal_vectors ws) - {normal_vectors ws ! i}) \<bullet> us ! i = (0::'a)
[PROOF STEP]
unfolding lincomb_scalar_prod_left[OF nv' u]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>w\<in>set (normal_vectors ws) - {normal_vectors ws ! i}. c w * (w \<bullet> us ! i)) = (0::'a)
[PROOF STEP]
proof (rule sum.neutral, intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (normal_vectors ws) - {normal_vectors ws ! i} \<Longrightarrow> c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (normal_vectors ws) - {normal_vectors ws ! i} \<Longrightarrow> c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
assume "x \<in> set ?nv - {?nv ! i}"
[PROOF STATE]
proof (state)
this:
x \<in> set (normal_vectors ws) - {normal_vectors ws ! i}

goal (1 subgoal):
 1. \<And>x. x \<in> set (normal_vectors ws) - {normal_vectors ws ! i} \<Longrightarrow> c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (normal_vectors ws) - {normal_vectors ws ! i}
[PROOF STEP]
obtain j where j: "j < ?n" and x: "x = ?nv ! j" and ij: "i \<noteq> j"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (normal_vectors ws) - {normal_vectors ws ! i}

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

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

goal (1 subgoal):
 1. \<And>x. x \<in> set (normal_vectors ws) - {normal_vectors ws ! i} \<Longrightarrow> c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
from dist[simplified] ij i j
[PROOF STATE]
proof (chain)
picking this:
distinct ws \<and> distinct us \<and> set ws \<inter> set us = {}
i \<noteq> j
i < length us
j < length us
[PROOF STEP]
have "us ! i \<noteq> us ! j"
[PROOF STATE]
proof (prove)
using this:
distinct ws \<and> distinct us \<and> set ws \<inter> set us = {}
i \<noteq> j
i < length us
j < length us

goal (1 subgoal):
 1. us ! i \<noteq> us ! j
[PROOF STEP]
unfolding distinct_conv_nth
[PROOF STATE]
proof (prove)
using this:
(\<forall>i<length ws. \<forall>j<length ws. i \<noteq> j \<longrightarrow> ws ! i \<noteq> ws ! j) \<and> (\<forall>i<length us. \<forall>j<length us. i \<noteq> j \<longrightarrow> us ! i \<noteq> us ! j) \<and> set ws \<inter> set us = {}
i \<noteq> j
i < length us
j < length us

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

goal (1 subgoal):
 1. \<And>x. x \<in> set (normal_vectors ws) - {normal_vectors ws ! i} \<Longrightarrow> c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i < length us
us ! i \<noteq> us ! j
[PROOF STEP]
have "us ! i \<in> set (ws @ us) - {us ! j}"
[PROOF STATE]
proof (prove)
using this:
i < length us
us ! i \<noteq> us ! j

goal (1 subgoal):
 1. us ! i \<in> set (ws @ us) - {us ! j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
us ! i \<in> set (ws @ us) - {us ! j}

goal (1 subgoal):
 1. \<And>x. x \<in> set (normal_vectors ws) - {normal_vectors ws ! i} \<Longrightarrow> c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
from nvi(3-4)[OF j this]
[PROOF STATE]
proof (chain)
picking this:
us ! i \<bullet> normal_vectors ws ! j = (0::'a)
normal_vectors ws ! j \<bullet> us ! i = (0::'a)
[PROOF STEP]
show "c x * (x \<bullet> us ! i) = 0"
[PROOF STATE]
proof (prove)
using this:
us ! i \<bullet> normal_vectors ws ! j = (0::'a)
normal_vectors ws ! j \<bullet> us ! i = (0::'a)

goal (1 subgoal):
 1. c x * (x \<bullet> us ! i) = (0::'a)
[PROOF STEP]
unfolding x
[PROOF STATE]
proof (prove)
using this:
us ! i \<bullet> normal_vectors ws ! j = (0::'a)
normal_vectors ws ! j \<bullet> us ! i = (0::'a)

goal (1 subgoal):
 1. c (normal_vectors ws ! j) * (normal_vectors ws ! j \<bullet> us ! i) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c x * (x \<bullet> us ! i) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
normal_vectors ws ! i \<bullet> us ! i = (0::'a)

goal (1 subgoal):
 1. lin_dep (set (normal_vectors ws)) \<Longrightarrow> False
[PROOF STEP]
with nvi(9)[OF i]
[PROOF STATE]
proof (chain)
picking this:
normal_vectors ws ! i \<bullet> us ! i \<noteq> (0::'a)
normal_vectors ws ! i \<bullet> us ! i = (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
normal_vectors ws ! i \<bullet> us ! i \<noteq> (0::'a)
normal_vectors ws ! i \<bullet> us ! i = (0::'a)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_indpt (set (normal_vectors ws))

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
from subset_li_is_li[OF lin']
[PROOF STATE]
proof (chain)
picking this:
?B \<subseteq> set (ws @ us) \<Longrightarrow> lin_indpt ?B
[PROOF STEP]
have "lin_indpt (set ws)"
[PROOF STATE]
proof (prove)
using this:
?B \<subseteq> set (ws @ us) \<Longrightarrow> lin_indpt ?B

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

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
from ortho_lin_indpt[OF nv ws scalar_0 lin_nv this]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>w x. \<lbrakk>w \<in> set (normal_vectors ws); x \<in> set ws\<rbrakk> \<Longrightarrow> x \<in> set ws; \<And>w x. \<lbrakk>w \<in> set (normal_vectors ws); x \<in> set ws\<rbrakk> \<Longrightarrow> w \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> lin_indpt (set (normal_vectors ws) \<union> set ws)
[PROOF STEP]
have "lin_indpt (set ?nv \<union> set ws)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>w x. \<lbrakk>w \<in> set (normal_vectors ws); x \<in> set ws\<rbrakk> \<Longrightarrow> x \<in> set ws; \<And>w x. \<lbrakk>w \<in> set (normal_vectors ws); x \<in> set ws\<rbrakk> \<Longrightarrow> w \<in> set (normal_vectors ws)\<rbrakk> \<Longrightarrow> lin_indpt (set (normal_vectors ws) \<union> set ws)

goal (1 subgoal):
 1. lin_indpt (set (normal_vectors ws) \<union> set ws)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lin_indpt (set (normal_vectors ws) \<union> set ws)

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lin_indpt (set (normal_vectors ws) \<union> set ws)

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
have "set ?nv \<union> set ws = set (ws @ ?nv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (normal_vectors ws) \<union> set ws = set (ws @ normal_vectors ws)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set (normal_vectors ws) \<union> set ws = set (ws @ normal_vectors ws)

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
show "lin_indpt (set (ws @ ?nv))"
[PROOF STATE]
proof (prove)
using this:
lin_indpt (set (ws @ normal_vectors ws))

goal (1 subgoal):
 1. lin_indpt (set (ws @ normal_vectors ws))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lin_indpt (set (ws @ normal_vectors ws))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
lin_indpt_list (ws @ normal_vectors ws)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pos_norm_vec:
  assumes D: "D \<subseteq> carrier_vec n" and fin: "finite D" and lin: "lin_indpt D"
    and card: "Suc (card D) = n"
    and c_def: "c = pos_norm_vec D x"
  shows "c \<in> carrier_vec n" "span D = { x. x \<in> carrier_vec n \<and> x \<bullet> c = 0}"
    "x \<notin> span D \<Longrightarrow> x \<in> carrier_vec n \<Longrightarrow> c \<bullet> x > 0"
    "c \<in> {normal_vector D, -normal_vector D}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (c \<in> carrier_vec n &&& local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}) &&& (\<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x) &&& c \<in> {normal_vector D, - normal_vector D}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. c \<in> carrier_vec n
 2. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 3. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
 4. c \<in> {normal_vector D, - normal_vector D}
[PROOF STEP]
have n: "normal_vector D \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal_vector D \<in> carrier_vec n
[PROOF STEP]
using normal_vector assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> normal_vector ?W \<in> carrier_vec n
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> normal_vector ?W \<noteq> 0\<^sub>v n
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n; ?w \<in> ?W\<rbrakk> \<Longrightarrow> ?w \<bullet> normal_vector ?W = (0::'a)
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n; ?w \<in> ?W\<rbrakk> \<Longrightarrow> normal_vector ?W \<bullet> ?w = (0::'a)
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lin_indpt (insert (normal_vector ?W) ?W)
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> normal_vector ?W \<notin> ?W
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n; 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))
D \<subseteq> carrier_vec n
finite D
lin_indpt D
Suc (card D) = n
c = pos_norm_vec D x

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

goal (4 subgoals):
 1. c \<in> carrier_vec n
 2. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 3. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
 4. c \<in> {normal_vector D, - normal_vector D}
[PROOF STEP]
show cnorm: "c \<in> {normal_vector D, -normal_vector D}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<in> {normal_vector D, - normal_vector D}
[PROOF STEP]
unfolding c_def pos_norm_vec_def Let_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if (0::'a) < normal_vector D \<bullet> x then normal_vector D else - normal_vector D) \<in> {normal_vector D, - normal_vector D}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> {normal_vector D, - normal_vector D}

goal (3 subgoals):
 1. c \<in> carrier_vec n
 2. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 3. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
c \<in> {normal_vector D, - normal_vector D}
[PROOF STEP]
show c: "c \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
using this:
c \<in> {normal_vector D, - normal_vector D}

goal (1 subgoal):
 1. c \<in> carrier_vec n
[PROOF STEP]
using assms normal_vector
[PROOF STATE]
proof (prove)
using this:
c \<in> {normal_vector D, - normal_vector D}
D \<subseteq> carrier_vec n
finite D
lin_indpt D
Suc (card D) = n
c = pos_norm_vec D x
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> normal_vector ?W \<in> carrier_vec n
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> normal_vector ?W \<noteq> 0\<^sub>v n
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n; ?w \<in> ?W\<rbrakk> \<Longrightarrow> ?w \<bullet> normal_vector ?W = (0::'a)
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n; ?w \<in> ?W\<rbrakk> \<Longrightarrow> normal_vector ?W \<bullet> ?w = (0::'a)
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> lin_indpt (insert (normal_vector ?W) ?W)
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n\<rbrakk> \<Longrightarrow> normal_vector ?W \<notin> ?W
\<lbrakk>finite ?W; Suc (card ?W) = n; lin_indpt ?W; ?W \<subseteq> carrier_vec n; 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 (1 subgoal):
 1. c \<in> carrier_vec n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> carrier_vec n

goal (2 subgoals):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 2. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
have "span D = { x. x \<in> carrier_vec n \<and> x \<bullet> normal_vector D = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
using normal_vector_span[OF card D fin lin]
[PROOF STATE]
proof (prove)
using this:
local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}

goal (2 subgoals):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 2. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
local.span D = {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)}

goal (2 subgoals):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 2. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
have "\<dots> = { x. x \<in> carrier_vec n \<and> x \<bullet> c = 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)} = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
[PROOF STEP]
using cnorm c
[PROOF STATE]
proof (prove)
using this:
c \<in> {normal_vector D, - normal_vector D}
c \<in> carrier_vec n

goal (1 subgoal):
 1. {x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)} = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> carrier_vec n. x \<bullet> normal_vector D = (0::'a)} = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}

goal (2 subgoals):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
 2. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
[PROOF STEP]
show span_char: "span D = { x. x \<in> carrier_vec n \<and> x \<bullet> c = 0}"
[PROOF STATE]
proof (prove)
using this:
local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}

goal (1 subgoal):
 1. local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}

goal (1 subgoal):
 1. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
local.span D = {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}

goal (1 subgoal):
 1. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
assume x: "x \<notin> span D" "x \<in> carrier_vec n"
[PROOF STATE]
proof (state)
this:
x \<notin> local.span D
x \<in> carrier_vec n

goal (1 subgoal):
 1. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
hence "c \<bullet> x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.span D
x \<in> carrier_vec n

goal (1 subgoal):
 1. c \<bullet> x \<noteq> (0::'a)
[PROOF STEP]
using comm_scalar_prod[OF c]
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.span D
x \<in> carrier_vec n
?v\<^sub>2 \<in> carrier_vec n \<Longrightarrow> c \<bullet> ?v\<^sub>2 = ?v\<^sub>2 \<bullet> c

goal (1 subgoal):
 1. c \<bullet> x \<noteq> (0::'a)
[PROOF STEP]
unfolding span_char
[PROOF STATE]
proof (prove)
using this:
x \<notin> {x \<in> carrier_vec n. x \<bullet> c = (0::'a)}
x \<in> carrier_vec n
?v\<^sub>2 \<in> carrier_vec n \<Longrightarrow> c \<bullet> ?v\<^sub>2 = ?v\<^sub>2 \<bullet> c

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

goal (1 subgoal):
 1. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
hence "normal_vector D \<bullet> x \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
c \<bullet> x \<noteq> (0::'a)

goal (1 subgoal):
 1. normal_vector D \<bullet> x \<noteq> (0::'a)
[PROOF STEP]
using cnorm n x
[PROOF STATE]
proof (prove)
using this:
c \<bullet> x \<noteq> (0::'a)
c \<in> {normal_vector D, - normal_vector D}
normal_vector D \<in> carrier_vec n
x \<notin> local.span D
x \<in> carrier_vec n

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

goal (1 subgoal):
 1. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
x \<notin> local.span D
x \<in> carrier_vec n
normal_vector D \<bullet> x \<noteq> (0::'a)
[PROOF STEP]
have b: "\<not> (normal_vector D \<bullet> x > 0) \<Longrightarrow> (-normal_vector D) \<bullet> x > 0"
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.span D
x \<in> carrier_vec n
normal_vector D \<bullet> x \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> (0::'a) < normal_vector D \<bullet> x \<Longrightarrow> (0::'a) < - normal_vector D \<bullet> x
[PROOF STEP]
using assms n
[PROOF STATE]
proof (prove)
using this:
x \<notin> local.span D
x \<in> carrier_vec n
normal_vector D \<bullet> x \<noteq> (0::'a)
D \<subseteq> carrier_vec n
finite D
lin_indpt D
Suc (card D) = n
c = pos_norm_vec D x
normal_vector D \<in> carrier_vec n

goal (1 subgoal):
 1. \<not> (0::'a) < normal_vector D \<bullet> x \<Longrightarrow> (0::'a) < - normal_vector D \<bullet> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> (0::'a) < normal_vector D \<bullet> x \<Longrightarrow> (0::'a) < - normal_vector D \<bullet> x

goal (1 subgoal):
 1. \<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (0::'a) < normal_vector D \<bullet> x \<Longrightarrow> (0::'a) < - normal_vector D \<bullet> x
[PROOF STEP]
show "c \<bullet> x > 0"
[PROOF STATE]
proof (prove)
using this:
\<not> (0::'a) < normal_vector D \<bullet> x \<Longrightarrow> (0::'a) < - normal_vector D \<bullet> x

goal (1 subgoal):
 1. (0::'a) < c \<bullet> x
[PROOF STEP]
unfolding c_def pos_norm_vec_def Let_def
[PROOF STATE]
proof (prove)
using this:
\<not> (0::'a) < normal_vector D \<bullet> x \<Longrightarrow> (0::'a) < - normal_vector D \<bullet> x

goal (1 subgoal):
 1. (0::'a) < (if (0::'a) < normal_vector D \<bullet> x then normal_vector D else - normal_vector D) \<bullet> x
[PROOF STEP]
by (auto split: if_splits)
[PROOF STATE]
proof (state)
this:
(0::'a) < c \<bullet> x

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>x \<notin> local.span D; x \<in> carrier_vec n\<rbrakk> \<Longrightarrow> (0::'a) < c \<bullet> x

goal:
No subgoals!
[PROOF STEP]
qed