Theory Normal_Vector
section ‹Normal Vectors›
text ‹We provide a function for the normal vector of a half-space (given as n-1 linearly
independent vectors).
We further provide a function that returns a list of normal vectors that span the
orthogonal complement of some subspace of $R^n$.
Bounds for all normal vectors are provided.›
theory Normal_Vector
imports
Integral_Bounded_Vectors
Basis_Extension
begin
context gram_schmidt
begin
lemma ortho_sum_in_span:
assumes W: "W ⊆ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and ortho: "⋀ w x. w ∈ W ⟹ x ∈ X ⟹ x ∙ w = 0"
and inspan: "lincomb l1 X + lincomb l2 W ∈ span X"
shows "lincomb l2 W = 0⇩v n"
proof (rule ccontr)
let ?v = "lincomb l2 W"
have vcarr: "?v ∈ carrier_vec n" using W by auto
have vspan: "?v ∈ span W" using W by auto
assume "¬?thesis"
from this have vnz: "?v ≠ 0⇩v n" by auto
let ?x = "lincomb l1 X"
have xcarr: "?x ∈ carrier_vec n" using X by auto
have xspan: "?x ∈ span X" using X xcarr by auto
have "0 ≠ sq_norm ?v" using vnz vcarr by simp
also have "sq_norm ?v = 0 + ?v ∙ ?v" by (simp add: sq_norm_vec_as_cscalar_prod)
also have "… = ?x ∙ ?v + ?v ∙ ?v"
by (subst (2) ortho_span_span[OF X W ortho], insert X W, auto)
also have "… = (?x + ?v ) ∙ ?v" using xcarr vcarr
using add_scalar_prod_distrib by force
also have "… = 0"
by (rule ortho_span_span[OF X W ortho inspan vspan])
finally show False by simp
qed
lemma ortho_lin_indpt: assumes W: "W ⊆ carrier_vec n"
and X: "X ⊆ carrier_vec n"
and ortho: "⋀ w x. w ∈ W ⟹ x ∈ X ⟹ x ∙ w = 0"
and linW: "lin_indpt W"
and linX: "lin_indpt X"
shows "lin_indpt (W ∪ X)"
proof (rule ccontr)
assume "¬?thesis"
from this obtain c where zerocomb:"lincomb c (W ∪ X) = 0⇩v n"
and notallz: "∃v ∈ (W ∪ X). c v ≠ 0"
using assms fin_dim fin_dim_li_fin finite_lin_indpt2 infinite_Un le_sup_iff
by metis
have zero_nin_W: "0⇩v n ∉ W" using assms by (metis vs_zero_lin_dep)
have WXinters: "W ∩ X = {}"
proof (rule ccontr)
assume "¬?thesis"
from this obtain v where v: "v∈ W ∩ X" by auto
hence "v∙v=0" using ortho by auto
moreover have "v ∈ carrier_vec n" using assms v by auto
ultimately have "v=0⇩v n" using sq_norm_vec_as_cscalar_prod[of v] by auto
then show False using zero_nin_W v by auto
qed
have finX: "finite X" using X linX by (simp add: fin_dim_li_fin)
have finW: "finite W" using W linW by (simp add: fin_dim_li_fin)
have split: "lincomb c (W ∪ X) = lincomb c X + lincomb c W"
using lincomb_union[OF W X WXinters finW finX]
by (simp add: M.add.m_comm W X)
hence "lincomb c X + lincomb c W ∈ span X" using zerocomb
using local.span_zero by auto
hence z1: "lincomb c W = 0⇩v n"
using ortho_sum_in_span[OF W X ortho] by simp
hence z2: "lincomb c X = 0⇩v n" using split zerocomb X by simp
have or: "(∃v ∈ W. c v ≠ 0) ∨ (∃ v∈ X. c v ≠ 0)" using notallz by auto
have ex1: "∃v ∈ W. c v ≠ 0 ⟹ False" using linW
using finW lin_dep_def z1 by blast
have ex2: "∃ v∈ X. c v ≠ 0 ⟹ False" using linX
using finX lin_dep_def z2 by blast
show False using ex1 ex2 or by auto
qed
definition normal_vector :: "'a vec set ⇒ 'a vec" where
"normal_vector W = (let ws = (SOME ws. set ws = W ∧ distinct ws);
m = length ws;
B = (λ j. mat m m (λ(i, j'). ws ! i $ (if j' < j then j' else Suc j')))
in vec n (λ j. (-1)^(m+j) * det (B j)))"
lemma normal_vector: assumes fin: "finite W"
and card: "Suc (card W) = n"
and lin: "lin_indpt W"
and W: "W ⊆ carrier_vec n"
shows "normal_vector W ∈ carrier_vec n"
"normal_vector W ≠ 0⇩v n"
"w ∈ W ⟹ w ∙ normal_vector W = 0"
"w ∈ W ⟹ normal_vector W ∙ w = 0"
"lin_indpt (insert (normal_vector W) W)"
"normal_vector W ∉ W"
"is_det_bound db ⟹ W ⊆ ℤ⇩v ∩ Bounded_vec (of_int Bnd) ⟹ normal_vector W ∈ ℤ⇩v ∩ Bounded_vec (of_int (db (n-1) Bnd))"
proof -
define ws where "ws = (SOME ws. set ws = W ∧ distinct ws)"
from finite_distinct_list[OF fin]
have "∃ ws. set ws = W ∧ distinct ws" by auto
from someI_ex[OF this, folded ws_def] have id: "set ws = W" and dist: "distinct ws" by auto
have len: "length ws = card W" using distinct_card[OF dist] id by auto
let ?n = "length ws"
define B where "B = (λ j. mat ?n ?n (λ(i, j'). ws ! i $ (if j' < j then j' else Suc j')))"
define nv where "nv = vec n (λ j. (-1)^(?n+j) * det (B j))"
have nv2: "normal_vector W = nv" unfolding normal_vector_def Let_def
ws_def[symmetric] B_def nv_def ..
define A where "A = (λ w. mat_of_rows n (ws @ [w]))"
from len id card have len: "Suc ?n = n" by auto
have A: "A w ∈ carrier_mat n n" for w using id W len unfolding A_def by auto
{
fix w :: "'a vec"
assume w: "w ∈ carrier_vec n"
from len have n1[simp]: "n - Suc 0 = ?n" by auto
{
fix j
assume j: "j < n"
have "mat_delete (A w) ?n j = B j"
unfolding mat_delete_def A_def mat_of_rows_def B_def
by (rule eq_matI, insert j len, auto simp: nth_append)
} note B = this
have "det (A w) = (∑j<n. (A w) $$ (length ws, j) * cofactor (A w) ?n j)"
by (subst laplace_expansion_row[OF A, of ?n], insert len, auto)
also have "… = (∑j<n. w $ j * (-1)^(?n+j) * det (mat_delete (A w) ?n j))"
by (rule sum.cong, auto simp: A_def mat_of_rows_def cofactor_def)
also have "… = (∑j<n. w $ j * (-1)^(?n+j) * det (B j))"
by (rule sum.cong[OF refl], subst B, auto)
also have "… = (∑j<n. w $ j * nv $ j)"
by (rule sum.cong[OF refl], auto simp: nv_def)
also have "… = w ∙ nv" unfolding scalar_prod_def unfolding nv_def
by (rule sum.cong, auto)
finally have "det (A w) = w ∙ nv" .
} note det_scalar = this
have nv: "nv ∈ carrier_vec n" unfolding nv_def by auto
{
fix w
assume wW: "w ∈ W"
with W have w: "w ∈ carrier_vec n" by auto
from wW id obtain i where i: "i < ?n" and ws: "ws ! i = w" unfolding set_conv_nth by auto
from det_scalar[OF w] have "det (A w) = w ∙ nv" .
also have "det (A w) = 0"
by (subst det_identical_rows[OF A, of i ?n], insert i ws len, auto simp: A_def mat_of_rows_def nth_append)
finally have "w ∙ nv = 0" ..
note this this[unfolded comm_scalar_prod[OF w nv]]
} note ortho = this
have nv0: "nv ≠ 0⇩v n"
proof
assume nv: "nv = 0⇩v n"
define bs where "bs = basis_extension ws"
define w where "w = hd bs"
have "lin_indpt_list ws" using dist lin W unfolding lin_indpt_list_def id by auto
from basis_extension[OF this, folded bs_def] len
have lin: "lin_indpt_list (ws @ bs)" and "length bs = 1" and bsc: "set bs ⊆ carrier_vec n"
by (auto simp: unit_vecs_def)
hence bs: "bs = [w]" unfolding w_def by (cases bs, auto)
with bsc have w: "w ∈ carrier_vec n" by auto
note lin = lin[unfolded bs]
from lin_indpt_list_length_eq_n[OF lin] len
have basis: "basis (set (ws @ [w]))" by auto
from w det_scalar nv have det0: "det (A w) = 0" by auto
with basis_det_nonzero[OF basis] len show False
unfolding A_def by auto
qed
let ?nv = "normal_vector W"
from ortho nv nv0
show nv: "?nv ∈ carrier_vec n"
and ortho: "⋀ w. w ∈ W ⟹ w ∙ ?nv = 0"
"⋀ w. w ∈ W ⟹ ?nv ∙ w = 0"
and n0: "?nv ≠ 0⇩v n" unfolding nv2 by auto
from n0 nv have "sq_norm ?nv ≠ 0" by auto
hence nvnv: "?nv ∙ ?nv ≠ 0" by (auto simp: sq_norm_vec_as_cscalar_prod)
show nvW: "?nv ∉ W" using nvnv ortho by blast
have "?nv ∉ span W" using W ortho nvnv nv
using orthocompl_span by blast
with lin_dep_iff_in_span[OF W lin nv nvW]
show "lin_indpt (insert ?nv W)" by auto
{
assume db: "is_det_bound db"
assume "W ⊆ ℤ⇩v ∩ Bounded_vec (of_int Bnd)"
hence wsI: "set ws ⊆ ℤ⇩v ∩ Bounded_vec (of_int Bnd)" unfolding id by auto
have ws: "set ws ⊆ carrier_vec n" using W unfolding id by auto
from wsI ws have wsI: "i < ?n ⟹ ws ! i ∈ ℤ⇩v ∩ Bounded_vec (of_int Bnd) ∩ carrier_vec n" for i
using len wsI unfolding set_conv_nth by auto
have ints: "i < ?n ⟹ j < n ⟹ ws ! i $ j ∈ ℤ" for i j
using wsI[of i, unfolded Ints_vec_def] by force
have bnd: "i < ?n ⟹ j < n ⟹ abs (ws ! i $ j) ≤ of_int Bnd" for i j
using wsI[unfolded Bounded_vec_def, of i] by auto
{
fix i
assume i: "i < n"
have ints_nv: "nv $ i ∈ ℤ" unfolding nv_def using wsI len ws
by (auto simp: i B_def set_conv_nth intro!: Ints_mult Ints_det ints)
have "B i ∈ ℤ⇩m ∩ Bounded_mat (of_int Bnd)"
unfolding B_def using len ws i bnd ints_nv
apply (simp add: Ints_mat_def Ints_vec_def Bounded_mat_def, intro allI impI)
subgoal for ii j using ints[of ii j] ints[of ii "Suc j"]
by auto
done
from is_det_bound_of_int[OF db _ this, of ?n]
have "¦nv $ i¦ ≤ of_int (db (n - 1) Bnd)"
unfolding nv_def using wsI len ws i
by (auto simp: B_def abs_mult bnd)
note ints_nv this
}
with nv nv2 show "?nv ∈ ℤ⇩v ∩ Bounded_vec (of_int (db (n - 1) Bnd))"
unfolding Ints_vec_def Bounded_vec_def by auto
}
qed
lemma normal_vector_span:
assumes card: "Suc (card D) = n"
and D: "D ⊆ carrier_vec n" and fin: "finite D" and lin: "lin_indpt D"
shows "span D = { x. x ∈ carrier_vec n ∧ x ∙ normal_vector D = 0}"
proof -
note nv = normal_vector[OF fin card lin D]
{
fix x
assume xspan: "x ∈ span D"
from finite_in_span[OF fin D xspan] obtain c where
"x ∙ normal_vector D = lincomb c D ∙ normal_vector D" by auto
also have "… = (∑w∈D. c w * (w ∙ normal_vector D))"
by (rule lincomb_scalar_prod_left, insert D nv, auto)
also have "… = 0"
apply (rule sum.neutral) using nv(1,2,3) D comm_scalar_prod[of "normal_vector D"] by fastforce
finally have "x ∈ carrier_vec n" "x ∙ normal_vector D = 0" using xspan D by auto
}
moreover
{
let ?n = "normal_vector D"
fix x
assume x: "x ∈ carrier_vec n" and xscal: "x ∙ normal_vector D = 0"
let ?B = "(insert (normal_vector D) D)"
have "card ?B = n" using card card_insert_disjoint[OF fin nv(6)] by auto
moreover have B: "?B ⊆ carrier_vec n" using D nv by auto
ultimately have "span ?B = carrier_vec n"
by (intro span_carrier_lin_indpt_card_n, insert nv(5), auto)
hence xspan: "x ∈ span ?B" using x by auto
obtain c where "x = lincomb c ?B" using finite_in_span[OF _ B xspan] fin by auto
hence "0 = lincomb c ?B ∙ normal_vector D" using xscal by auto
also have "… = (∑w∈ ?B. c w * (w ∙ normal_vector D))"
by (subst lincomb_scalar_prod_left, insert B, auto)
also have "… = (∑w∈ D. c w * (w ∙ normal_vector D)) + c ?n * (?n ∙ ?n)"
by (subst sum.insert[OF fin nv(6)], auto)
also have "(∑w∈ D. c w * (w ∙ normal_vector D)) = 0"
apply(rule sum.neutral) using nv(1,3) comm_scalar_prod[OF nv(1)] D by fastforce
also have "?n ∙ ?n = sq_norm ?n" using sq_norm_vec_as_cscalar_prod[of ?n] by simp
finally have "c ?n * sq_norm ?n = 0" by simp
hence ncoord: "c ?n = 0" using nv(1-5) by auto
have "x = lincomb c ?B" by fact
also have "… = lincomb c D"
apply (subst lincomb_insert2[OF fin D _ nv(6,1)]) using ncoord nv(1) D by auto
finally have "x ∈ span D" using fin by auto
}
ultimately show ?thesis by auto
qed
definition normal_vectors :: "'a vec list ⇒ 'a vec list" where
"normal_vectors ws = (let us = basis_extension ws
in map (λ i. normal_vector (set (ws @ us) - {us ! i})) [0..<length us])"
lemma normal_vectors:
assumes lin: "lin_indpt_list ws"
shows "set (normal_vectors ws) ⊆ carrier_vec n"
"w ∈ set ws ⟹ nv ∈ set (normal_vectors ws) ⟹ nv ∙ w = 0"
"w ∈ set ws ⟹ nv ∈ set (normal_vectors ws) ⟹ w ∙ nv = 0"
"lin_indpt_list (ws @ normal_vectors ws)"
"length ws + length (normal_vectors ws) = n"
"set ws ∩ set (normal_vectors ws) = {}"
"is_det_bound db ⟹ set ws ⊆ ℤ⇩v ∩ Bounded_vec (of_int Bnd) ⟹
set (normal_vectors ws) ⊆ ℤ⇩v ∩ Bounded_vec (of_int (db (n-1) (max 1 Bnd)))"
proof -
define us where "us = basis_extension ws"
from basis_extension[OF assms, folded us_def]
have units: "set us ⊆ set (unit_vecs n)"
and lin: "lin_indpt_list (ws @ us)"
and len: "length (ws @ us) = n"
by auto
from lin_indpt_list_length_eq_n[OF lin len]
have span: "span (set (ws @ us)) = carrier_vec n" by auto
from lin[unfolded lin_indpt_list_def]
have wsus: "set (ws @ us) ⊆ carrier_vec n"
and dist: "distinct (ws @ us)"
and lin': "lin_indpt (set (ws @ us))" by auto
let ?nv = "normal_vectors ws"
note nv_def = normal_vectors_def[of ws, unfolded Let_def, folded us_def]
let ?m = "length ws"
let ?n = "length us"
have lnv[simp]: "length ?nv = length us" unfolding nv_def by auto
{
fix i
let ?V = "set (ws @ us) - {us ! i}"
assume i: "i < ?n"
hence nvi: "?nv ! i = normal_vector ?V" unfolding nv_def by auto
from i have "us ! i ∈ set us" by auto
with wsus have u: "us ! i ∈ carrier_vec n" by auto
have id: "?V ∪ {us ! i} = set (ws @ us)" using i by auto
have V: "?V ⊆ carrier_vec n" using wsus by auto
have finV: "finite ?V" by auto
have "Suc (card ?V) = card (insert (us ! i) ?V)"
by (subst card_insert_disjoint[OF finV], auto)
also have "insert (us ! i) ?V = set (ws @ us)" using i by auto
finally have cardV: "Suc (card ?V) = n"
using len distinct_card[OF dist] by auto
from subset_li_is_li[OF lin'] have linV: "lin_indpt ?V" by auto
from lin_dep_iff_in_span[OF _ linV u, unfolded id] wsus lin'
have usV: "us ! i ∉ span ?V" by auto
note nv = normal_vector[OF finV cardV linV V, folded nvi]
from normal_vector_span[OF cardV V _ linV, folded nvi] comm_scalar_prod[OF _ nv(1)]
have span: "span ?V = {x ∈ carrier_vec n. ?nv ! i ∙ x = 0}"
by auto
from nv(1,2) have "sq_norm (?nv ! i) ≠ 0" by auto
hence nvi: "?nv ! i ∙ ?nv ! i ≠ 0"
by (auto simp: sq_norm_vec_as_cscalar_prod)
from span nvi have nvspan: "?nv ! i ∉ span ?V" by auto
from u usV[unfolded span] have "?nv ! i ∙ us ! i ≠ 0" by blast
note nv nvi this span usV nvspan
} note nvi = this
show nv: "set ?nv ⊆ carrier_vec n"
unfolding set_conv_nth using nvi(1) by auto
{
fix w nv
assume w: "w ∈ set ws"
with dist have wus: "w ∉ set us" by auto
assume n: "nv ∈ set ?nv"
with w wus show "nv ∙ w = 0"
unfolding set_conv_nth[of "normal_vectors _"] by (auto intro!: nvi(4)[of _ w])
thus "w ∙ nv = 0" using comm_scalar_prod[of w n nv] w nv n wsus by auto
} note scalar_0 = this
show "length ws + length ?nv = n" using len by simp
{
let ?oi = "of_int :: int ⇒ 'a"
assume wsI: "set ws ⊆ ℤ⇩v ∩ Bounded_vec (?oi Bnd)" and db: "is_det_bound db"
{
fix nv
assume "nv ∈ set ?nv"
then obtain i where nv: "nv = ?nv ! i" and i: "i < ?n" unfolding set_conv_nth by auto
from order.trans[OF units unit_vec_int_bounds]
wsI have "set (ws @ us) - {us ! i} ⊆ ℤ⇩v ∩ Bounded_vec (?oi (max 1 Bnd))" using
Bounded_vec_mono[of "?oi Bnd" "?oi (max 1 Bnd)", unfolded of_int_le_iff]
by auto
from nvi(7)[OF i db this] nv
have "nv ∈ ℤ⇩v ∩ Bounded_vec (?oi (db (n - 1) (max 1 Bnd)))"
by auto
}
thus "set ?nv ⊆ ℤ⇩v ∩ Bounded_vec (?oi (db (n - 1) (max 1 Bnd)))" by auto
}
have dist_nv: "distinct ?nv" unfolding distinct_conv_nth lnv
proof (intro allI impI)
fix i j
assume i: "i < ?n" and j: "j < ?n" and ij: "i ≠ j"
with dist have usj: "us ! j ∈ set (ws @ us) - {us ! i}"
by (simp, auto simp: distinct_conv_nth set_conv_nth)
from nvi(4)[OF i this] nvi(9)[OF j]
show "?nv ! i ≠ ?nv ! j" by auto
qed
show disj: "set ws ∩ set ?nv = {}"
proof (rule ccontr)
assume "¬ ?thesis"
then obtain w where w: "w ∈ set ws" "w ∈ set ?nv" by auto
from scalar_0[OF this] this(1) have "sq_norm w = 0"
by (auto simp: sq_norm_vec_as_cscalar_prod)
with w wsus have "w = 0⇩v n" by auto
with vs_zero_lin_dep[OF wsus lin'] w(1) show False by auto
qed
have dist': "distinct (ws @ ?nv)" using dist disj dist_nv by auto
show "lin_indpt_list (ws @ ?nv)" unfolding lin_indpt_list_def
proof (intro conjI dist')
show set: "set (ws @ ?nv) ⊆ carrier_vec n" using nv wsus by auto
hence ws: "set ws ⊆ carrier_vec n" by auto
have lin_nv: "lin_indpt (set ?nv)"
proof
assume "lin_dep (set ?nv)"
from finite_lin_dep[OF finite_set this nv]
obtain a v where comb: "lincomb a (set ?nv) = 0⇩v n" and vnv: "v ∈ set ?nv" and av0: "a v ≠ 0" by auto
from vnv[unfolded set_conv_nth] obtain i where i: "i < ?n" and vi: "v = ?nv ! i" by auto
define b where "b = (λ w. a w / a v)"
define c where "c = (λ w. -1 * b w)"
define x where "x = lincomb b (set ?nv - {v})"
define w where "w = lincomb c (set ?nv - {v})"
have w: "w ∈ carrier_vec n" unfolding w_def using nv by auto
have x: "x ∈ carrier_vec n" unfolding x_def using nv by auto
from arg_cong[OF comb, of "λ x. (1/ a v) ⋅⇩v x"]
have "0⇩v n = 1 / a v ⋅⇩v lincomb a (set ?nv)" by auto
also have "… = lincomb b (set ?nv)"
by (subst lincomb_smult[symmetric, OF nv], auto simp: b_def)
also have "… = b v ⋅⇩v v + lincomb b (set ?nv - {v})"
by (subst lincomb_del2[OF _ nv _ vnv], auto)
also have "b v ⋅⇩v v = v" using av0 unfolding b_def by auto
finally have "v + lincomb b (set ?nv - {v}) - lincomb b (set ?nv - {v}) =
0⇩v n - lincomb b (set ?nv - {v})" (is "?l = ?r") by simp
also have "?l = v"
by (rule add_diff_cancel_right_vec, insert vnv nv, auto)
also have "?r = w" unfolding w_def c_def
by (subst lincomb_smult, unfold x_def[symmetric], insert nv x, auto)
finally have vw: "v = w" .
have u: "us ! i ∈ carrier_vec n" using i wsus by auto
have nv': "set ?nv - {?nv ! i} ⊆ carrier_vec n" using nv by auto
have "?nv ! i ∙ us ! i = 0"
unfolding vi[symmetric] vw unfolding w_def vi
unfolding lincomb_scalar_prod_left[OF nv' u]
proof (rule sum.neutral, intro ballI)
fix x
assume "x ∈ set ?nv - {?nv ! i}"
then obtain j where j: "j < ?n" and x: "x = ?nv ! j" and ij: "i ≠ j" unfolding set_conv_nth by auto
from dist[simplified] ij i j have "us ! i ≠ us ! j" unfolding distinct_conv_nth by auto
with i have "us ! i ∈ set (ws @ us) - {us ! j}" by auto
from nvi(3-4)[OF j this]
show "c x * (x ∙ us ! i) = 0" unfolding x by auto
qed
with nvi(9)[OF i] show False ..
qed
from subset_li_is_li[OF lin'] have "lin_indpt (set ws)" by auto
from ortho_lin_indpt[OF nv ws scalar_0 lin_nv this]
have "lin_indpt (set ?nv ∪ set ws)" .
also have "set ?nv ∪ set ws = set (ws @ ?nv)" by auto
finally show "lin_indpt (set (ws @ ?nv))" .
qed
qed
definition pos_norm_vec :: "'a vec set ⇒ 'a vec ⇒ 'a vec" where
"pos_norm_vec D x = (let c' = normal_vector D;
c = (if c' ∙ x > 0 then c' else -c') in c)"
lemma pos_norm_vec:
assumes D: "D ⊆ 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 ∈ carrier_vec n" "span D = { x. x ∈ carrier_vec n ∧ x ∙ c = 0}"
"x ∉ span D ⟹ x ∈ carrier_vec n ⟹ c ∙ x > 0"
"c ∈ {normal_vector D, -normal_vector D}"
proof -
have n: "normal_vector D ∈ carrier_vec n" using normal_vector assms by auto
show cnorm: "c ∈ {normal_vector D, -normal_vector D}" unfolding c_def pos_norm_vec_def Let_def by auto
then show c: "c ∈ carrier_vec n" using assms normal_vector by auto
have "span D = { x. x ∈ carrier_vec n ∧ x ∙ normal_vector D = 0}"
using normal_vector_span[OF card D fin lin] by auto
also have "… = { x. x ∈ carrier_vec n ∧ x ∙ c = 0}" using cnorm c by auto
finally show span_char: "span D = { x. x ∈ carrier_vec n ∧ x ∙ c = 0}" by auto
{
assume x: "x ∉ span D" "x ∈ carrier_vec n"
hence "c ∙ x ≠ 0" using comm_scalar_prod[OF c] unfolding span_char by auto
hence "normal_vector D ∙ x ≠ 0" using cnorm n x by auto
with x have b: "¬ (normal_vector D ∙ x > 0) ⟹ (-normal_vector D) ∙ x > 0"
using assms n by auto
then show "c ∙ x > 0" unfolding c_def pos_norm_vec_def Let_def
by (auto split: if_splits)
}
qed
end
end