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 (* TODO move *) 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 (* TODO move *) 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