src/HOL/Library/Euclidean_Space.thy
changeset 30263 c88af4619a73
parent 30242 aea5d7fa7ef5
child 30267 171b3bd93c90
     1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Wed Mar 04 19:21:56 2009 +0000
     1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Wed Mar 04 19:21:56 2009 +0000
     1.3 @@ -626,7 +626,7 @@
     1.4    ultimately show ?thesis by metis
     1.5  qed
     1.6  
     1.7 -lemma dot_pos_lt: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x] 
     1.8 +lemma dot_pos_lt[simp]: "(0 < x \<bullet> x) \<longleftrightarrow> (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \<noteq> 0" using dot_eq_0[of x] dot_pos_le[of x] 
     1.9    by (auto simp add: le_less) 
    1.10  
    1.11  subsection{* The collapse of the general concepts to dimension one. *}
    1.12 @@ -759,10 +759,10 @@
    1.13  
    1.14  text{* Hence derive more interesting properties of the norm. *}
    1.15  
    1.16 -lemma norm_0: "norm (0::real ^ 'n) = 0"
    1.17 +lemma norm_0[simp]: "norm (0::real ^ 'n) = 0"
    1.18    by (rule norm_zero)
    1.19  
    1.20 -lemma norm_mul: "norm(a *s x) = abs(a) * norm x"
    1.21 +lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x"
    1.22    by (simp add: vector_norm_def vector_component setL2_right_distrib
    1.23             abs_mult cong: strong_setL2_cong)
    1.24  lemma norm_eq_0_dot: "(norm x = 0) \<longleftrightarrow> (x \<bullet> x = (0::real))"
    1.25 @@ -772,11 +772,11 @@
    1.26  lemma norm_pow_2: "norm x ^ 2 = x \<bullet> x"
    1.27    by (simp add: real_vector_norm_def)
    1.28  lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
    1.29 -lemma vector_mul_eq_0: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
    1.30 +lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
    1.31    by vector
    1.32 -lemma vector_mul_lcancel: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
    1.33 +lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
    1.34    by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
    1.35 -lemma vector_mul_rcancel: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
    1.36 +lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
    1.37    by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
    1.38  lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
    1.39    by (metis vector_mul_lcancel)
    1.40 @@ -814,28 +814,6 @@
    1.41  lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e"
    1.42    by (metis basic_trans_rules(21) norm_triangle_ineq)
    1.43  
    1.44 -lemma setsum_delta: 
    1.45 -  assumes fS: "finite S"
    1.46 -  shows "setsum (\<lambda>k. if k=a then b k else 0) S = (if a \<in> S then b a else 0)"
    1.47 -proof-
    1.48 -  let ?f = "(\<lambda>k. if k=a then b k else 0)"
    1.49 -  {assume a: "a \<notin> S"
    1.50 -    hence "\<forall> k\<in> S. ?f k = 0" by simp
    1.51 -    hence ?thesis  using a by simp}
    1.52 -  moreover 
    1.53 -  {assume a: "a \<in> S"
    1.54 -    let ?A = "S - {a}"
    1.55 -    let ?B = "{a}"
    1.56 -    have eq: "S = ?A \<union> ?B" using a by blast 
    1.57 -    have dj: "?A \<inter> ?B = {}" by simp
    1.58 -    from fS have fAB: "finite ?A" "finite ?B" by auto  
    1.59 -    have "setsum ?f S = setsum ?f ?A + setsum ?f ?B"
    1.60 -      using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]]
    1.61 -      by simp
    1.62 -    then have ?thesis  using a by simp}
    1.63 -  ultimately show ?thesis by blast
    1.64 -qed
    1.65 -  
    1.66  lemma component_le_norm: "i \<in> {1 .. dimindex(UNIV :: 'n set)} ==> \<bar>x$i\<bar> <= norm (x::real ^ 'n)"
    1.67    apply (simp add: vector_norm_def)
    1.68    apply (rule member_le_setL2, simp_all)
    1.69 @@ -852,7 +830,7 @@
    1.70  lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\<lambda>i. \<bar>x$i\<bar>) {1..dimindex(UNIV::'n set)}"
    1.71    by (simp add: vector_norm_def setL2_le_setsum)
    1.72  
    1.73 -lemma real_abs_norm: "\<bar> norm x\<bar> = norm (x :: real ^'n)" 
    1.74 +lemma real_abs_norm[simp]: "\<bar> norm x\<bar> = norm (x :: real ^'n)" 
    1.75    by (rule abs_norm_cancel)
    1.76  lemma real_abs_sub_norm: "\<bar>norm(x::real ^'n) - norm y\<bar> <= norm(x - y)"
    1.77    by (rule norm_triangle_ineq3)
    1.78 @@ -929,6 +907,7 @@
    1.79    apply simp_all
    1.80    done
    1.81  
    1.82 +  (* FIXME: Move all these theorems into the ML code using lemma antiquotation *)
    1.83  lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \<Longrightarrow> b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)"
    1.84    apply (rule norm_triangle_le) by simp
    1.85  
    1.86 @@ -977,17 +956,17 @@
    1.87  
    1.88  text{* Hence more metric properties. *}
    1.89  
    1.90 -lemma dist_refl: "dist x x = 0" by norm
    1.91 +lemma dist_refl[simp]: "dist x x = 0" by norm
    1.92  
    1.93  lemma dist_sym: "dist x y = dist y x"by norm
    1.94  
    1.95 -lemma dist_pos_le: "0 <= dist x y" by norm
    1.96 +lemma dist_pos_le[simp]: "0 <= dist x y" by norm
    1.97  
    1.98  lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm
    1.99  
   1.100  lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm
   1.101  
   1.102 -lemma dist_eq_0: "dist x y = 0 \<longleftrightarrow> x = y" by norm
   1.103 +lemma dist_eq_0[simp]: "dist x y = 0 \<longleftrightarrow> x = y" by norm
   1.104  
   1.105  lemma dist_pos_lt: "x \<noteq> y ==> 0 < dist x y" by norm 
   1.106  lemma dist_nz:  "x \<noteq> y \<longleftrightarrow> 0 < dist x y" by norm 
   1.107 @@ -1003,12 +982,12 @@
   1.108  lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'"
   1.109    by norm 
   1.110  
   1.111 -lemma dist_mul: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y" 
   1.112 +lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y" 
   1.113    unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. 
   1.114  
   1.115  lemma dist_triangle_add_half: " dist x x' < e / 2 \<Longrightarrow> dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm 
   1.116  
   1.117 -lemma dist_le_0: "dist x y <= 0 \<longleftrightarrow> x = y" by norm 
   1.118 +lemma dist_le_0[simp]: "dist x y <= 0 \<longleftrightarrow> x = y" by norm 
   1.119  
   1.120  lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)"
   1.121    apply vector
   1.122 @@ -1035,47 +1014,6 @@
   1.123    shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S"
   1.124    using i by (simp add: setsum_eq Cart_lambda_beta)
   1.125  
   1.126 -  (* This needs finiteness assumption due to the definition of fold!!! *)
   1.127 -
   1.128 -lemma setsum_superset:
   1.129 -  assumes fb: "finite B" and ab: "A \<subseteq> B" 
   1.130 -  and f0: "\<forall>x \<in> B - A. f x = 0"
   1.131 -  shows "setsum f B = setsum f A"
   1.132 -proof-
   1.133 -  from ab fb have fa: "finite A" by (metis finite_subset)
   1.134 -  from fb have fba: "finite (B - A)" by (metis finite_Diff)
   1.135 -  have d: "A \<inter> (B - A) = {}" by blast
   1.136 -  from ab have b: "B = A \<union> (B - A)" by blast
   1.137 -  from setsum_Un_disjoint[OF fa fba d, of f] b
   1.138 -    setsum_0'[OF f0]
   1.139 -  show "setsum f B = setsum f A" by simp
   1.140 -qed
   1.141 -
   1.142 -lemma setsum_restrict_set:
   1.143 -  assumes fA: "finite A"
   1.144 -  shows "setsum f (A \<inter> B) = setsum (\<lambda>x. if x \<in> B then f x else 0) A"
   1.145 -proof-
   1.146 -  from fA have fab: "finite (A \<inter> B)" by auto
   1.147 -  have aba: "A \<inter> B \<subseteq> A" by blast
   1.148 -  let ?g = "\<lambda>x. if x \<in> A\<inter>B then f x else 0"
   1.149 -  from setsum_superset[OF fA aba, of ?g]
   1.150 -  show ?thesis by simp
   1.151 -qed
   1.152 -
   1.153 -lemma setsum_cases:
   1.154 -  assumes fA: "finite A"
   1.155 -  shows "setsum (\<lambda>x. if x \<in> B then f x else g x) A =
   1.156 -         setsum f (A \<inter> B) + setsum g (A \<inter> - B)"
   1.157 -proof-
   1.158 -  have a: "A = A \<inter> B \<union> A \<inter> -B" "(A \<inter> B) \<inter> (A \<inter> -B) = {}" 
   1.159 -    by blast+
   1.160 -  from fA 
   1.161 -  have f: "finite (A \<inter> B)" "finite (A \<inter> -B)" by auto
   1.162 -  let ?g = "\<lambda>x. if x \<in> B then f x else g x"
   1.163 -  from setsum_Un_disjoint[OF f a(2), of ?g] a(1)
   1.164 -  show ?thesis by simp
   1.165 -qed
   1.166 -
   1.167  lemma setsum_norm: 
   1.168    fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   1.169    assumes fS: "finite S"
   1.170 @@ -1173,41 +1111,6 @@
   1.171    from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto
   1.172  qed
   1.173  
   1.174 -lemma setsum_reindex_nonzero: 
   1.175 -  assumes fS: "finite S"
   1.176 -  and nz: "\<And> x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
   1.177 -  shows "setsum h (f ` S) = setsum (h o f) S"
   1.178 -using nz
   1.179 -proof(induct rule: finite_induct[OF fS])
   1.180 -  case 1 thus ?case by simp
   1.181 -next
   1.182 -  case (2 x F) 
   1.183 -  {assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
   1.184 -    then obtain y where y: "y \<in> F" "f x = f y" by auto 
   1.185 -    from "2.hyps" y have xy: "x \<noteq> y" by auto
   1.186 -    
   1.187 -    from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
   1.188 -    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
   1.189 -    also have "\<dots> = setsum (h o f) (insert x F)" 
   1.190 -      using "2.hyps" "2.prems" h0  by auto 
   1.191 -    finally have ?case .}
   1.192 -  moreover
   1.193 -  {assume fxF: "f x \<notin> f ` F"
   1.194 -    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
   1.195 -      using fxF "2.hyps" by simp 
   1.196 -    also have "\<dots> = setsum (h o f) (insert x F)"  
   1.197 -      using "2.hyps" "2.prems" fxF
   1.198 -      apply auto apply metis done
   1.199 -    finally have ?case .}
   1.200 -  ultimately show ?case by blast
   1.201 -qed
   1.202 -
   1.203 -lemma setsum_Un_nonzero:
   1.204 -  assumes fS: "finite S" and fF: "finite F"
   1.205 -  and f: "\<forall> x\<in> S \<inter> F . f x = (0::'a::ab_group_add)"
   1.206 -  shows "setsum f (S \<union> F) = setsum f S + setsum f F"
   1.207 -  using setsum_Un[OF fS fF, of f] setsum_0'[OF f] by simp
   1.208 -
   1.209  lemma setsum_natinterval_left:
   1.210    assumes mn: "(m::nat) <= n" 
   1.211    shows "setsum f {m..n} = f m + setsum f {m + 1..n}"
   1.212 @@ -1249,109 +1152,9 @@
   1.213    shows "setsum (\<lambda>y. setsum g {x. x\<in> S \<and> f x = y}) T = setsum g S"
   1.214    
   1.215  apply (subst setsum_image_gen[OF fS, of g f])
   1.216 -apply (rule setsum_superset[OF fT fST])
   1.217 +apply (rule setsum_mono_zero_right[OF fT fST])
   1.218  by (auto intro: setsum_0')
   1.219  
   1.220 -(* FIXME: Change the name to fold_image\<dots> *)
   1.221 -lemma (in comm_monoid_mult) fold_1': "finite S \<Longrightarrow> (\<forall>x\<in>S. f x = 1) \<Longrightarrow> fold_image op * f 1 S = 1"
   1.222 -  apply (induct set: finite)
   1.223 -  apply simp by (auto simp add: fold_image_insert)
   1.224 -
   1.225 -lemma (in comm_monoid_mult) fold_union_nonzero:
   1.226 -  assumes fS: "finite S" and fT: "finite T"
   1.227 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
   1.228 -  shows "fold_image (op *) f 1 (S \<union> T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T"
   1.229 -proof-
   1.230 -  have "fold_image op * f 1 (S \<inter> T) = 1" 
   1.231 -    apply (rule fold_1')
   1.232 -    using fS fT I0 by auto 
   1.233 -  with fold_image_Un_Int[OF fS fT] show ?thesis by simp
   1.234 -qed
   1.235 -
   1.236 -lemma setsum_union_nonzero:  
   1.237 -  assumes fS: "finite S" and fT: "finite T"
   1.238 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 0"
   1.239 -  shows "setsum f (S \<union> T) = setsum f S  + setsum f T"
   1.240 -  using fS fT
   1.241 -  apply (simp add: setsum_def)
   1.242 -  apply (rule comm_monoid_add.fold_union_nonzero)
   1.243 -  using I0 by auto
   1.244 -
   1.245 -lemma setprod_union_nonzero:  
   1.246 -  assumes fS: "finite S" and fT: "finite T"
   1.247 -  and I0: "\<forall>x \<in> S\<inter>T. f x = 1"
   1.248 -  shows "setprod f (S \<union> T) = setprod f S  * setprod f T"
   1.249 -  using fS fT
   1.250 -  apply (simp add: setprod_def)
   1.251 -  apply (rule fold_union_nonzero)
   1.252 -  using I0 by auto
   1.253 -
   1.254 -lemma setsum_unions_nonzero: 
   1.255 -  assumes fS: "finite S" and fSS: "\<forall>T \<in> S. finite T"
   1.256 -  and f0: "\<And>T1 T2 x. T1\<in>S \<Longrightarrow> T2\<in>S \<Longrightarrow> T1 \<noteq> T2 \<Longrightarrow> x \<in> T1 \<Longrightarrow> x \<in> T2 \<Longrightarrow> f x = 0"
   1.257 -  shows "setsum f (\<Union>S) = setsum (\<lambda>T. setsum f T) S"
   1.258 -  using fSS f0
   1.259 -proof(induct rule: finite_induct[OF fS])
   1.260 -  case 1 thus ?case by simp
   1.261 -next
   1.262 -  case (2 T F)
   1.263 -  then have fTF: "finite T" "\<forall>T\<in>F. finite T" "finite F" and TF: "T \<notin> F" 
   1.264 -    and H: "setsum f (\<Union> F) = setsum (setsum f) F" by (auto simp add: finite_insert)
   1.265 -  from fTF have fUF: "finite (\<Union>F)" by (auto intro: finite_Union)
   1.266 -  from "2.prems" TF fTF
   1.267 -  show ?case 
   1.268 -    by (auto simp add: H[symmetric] intro: setsum_union_nonzero[OF fTF(1) fUF, of f])
   1.269 -qed
   1.270 -
   1.271 -  (* FIXME : Copied from Pocklington --- should be moved to Finite_Set!!!!!!!! *)
   1.272 -
   1.273 -
   1.274 -lemma (in comm_monoid_mult) fold_related: 
   1.275 -  assumes Re: "R e e" 
   1.276 -  and Rop: "\<forall>x1 y1 x2 y2. R x1 x2 \<and> R y1 y2 \<longrightarrow> R (x1 * y1) (x2 * y2)" 
   1.277 -  and fS: "finite S" and Rfg: "\<forall>x\<in>S. R (h x) (g x)"
   1.278 -  shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)"
   1.279 -  using fS by (rule finite_subset_induct) (insert assms, auto)
   1.280 -
   1.281 -  (* FIXME: I think we can get rid of the finite assumption!! *)	
   1.282 -lemma (in comm_monoid_mult) 
   1.283 -  fold_eq_general:
   1.284 -  assumes fS: "finite S"
   1.285 -  and h: "\<forall>y\<in>S'. \<exists>!x. x\<in> S \<and> h(x) = y" 
   1.286 -  and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2(h x) = f1 x"
   1.287 -  shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'"
   1.288 -proof-
   1.289 -  from h f12 have hS: "h ` S = S'" by auto
   1.290 -  {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
   1.291 -    from f12 h H  have "x = y" by auto }
   1.292 -  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
   1.293 -  from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
   1.294 -  from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp
   1.295 -  also have "\<dots> = fold_image (op *) (f2 o h) e S" 
   1.296 -    using fold_image_reindex[OF fS hinj, of f2 e] .
   1.297 -  also have "\<dots> = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e]
   1.298 -    by blast
   1.299 -  finally show ?thesis ..
   1.300 -qed
   1.301 -
   1.302 -lemma (in comm_monoid_mult) fold_eq_general_inverses:
   1.303 -  assumes fS: "finite S" 
   1.304 -  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   1.305 -  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
   1.306 -  shows "fold_image (op *) f e S = fold_image (op *) g e T"
   1.307 -  using fold_eq_general[OF fS, of T h g f e] kh hk by metis
   1.308 -
   1.309 -lemma setsum_eq_general_reverses:
   1.310 -  assumes fS: "finite S" and fT: "finite T"
   1.311 -  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
   1.312 -  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x  \<and> g (h x) = f x"
   1.313 -  shows "setsum f S = setsum g T"
   1.314 -  apply (simp add: setsum_def fS fT)
   1.315 -  apply (rule comm_monoid_add.fold_eq_general_inverses[OF fS])
   1.316 -  apply (erule kh)
   1.317 -  apply (erule hk)
   1.318 -  done
   1.319 -
   1.320  lemma vsum_norm_allsubsets_bound:
   1.321    fixes f:: "'a \<Rightarrow> real ^'n"
   1.322    assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" 
   1.323 @@ -1383,7 +1186,7 @@
   1.324        by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1)
   1.325      have "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P = setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pp + setsum (\<lambda>x. \<bar>f x $ i\<bar>) ?Pn" 
   1.326        apply (subst thp)
   1.327 -      apply (rule setsum_Un_nonzero) 
   1.328 +      apply (rule setsum_Un_zero) 
   1.329        using fP thp0 by auto
   1.330      also have "\<dots> \<le> 2*e" using Pne Ppe by arith
   1.331      finally show "setsum (\<lambda>x. \<bar>f x $ i\<bar>) P \<le> 2*e" .
   1.332 @@ -1392,7 +1195,7 @@
   1.333  qed
   1.334  
   1.335  lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> (y::'a::{comm_ring}^'n) = setsum (\<lambda>x. f x \<bullet> y) S "
   1.336 -  by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd)
   1.337 +  by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd)
   1.338  
   1.339  lemma dot_rsum: "finite S \<Longrightarrow> (y::'a::{comm_ring}^'n) \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
   1.340    by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd)
   1.341 @@ -4137,7 +3940,8 @@
   1.342  	apply (subst Cy)
   1.343  	using C(1) fth
   1.344  	apply (simp only: setsum_clauses)
   1.345 -	apply (auto simp add: dot_ladd dot_lmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth])
   1.346 +	thm dot_ladd
   1.347 +	apply (auto simp add: dot_ladd dot_radd dot_lmult dot_rmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth])
   1.348  	apply (rule setsum_0')
   1.349  	apply clarsimp
   1.350  	apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
   1.351 @@ -5294,14 +5098,11 @@
   1.352        have ?lhs unfolding collinear_def c
   1.353  	apply (rule exI[where x=x])
   1.354  	apply auto
   1.355 -	apply (rule exI[where x=0], simp)
   1.356  	apply (rule exI[where x="- 1"], simp only: vector_smult_lneg vector_smult_lid)
   1.357  	apply (rule exI[where x= "-c"], simp only: vector_smult_lneg)
   1.358  	apply (rule exI[where x=1], simp)
   1.359 -	apply (rule exI[where x=0], simp)
   1.360  	apply (rule exI[where x="1 - c"], simp add: vector_smult_lneg vector_sub_rdistrib)
   1.361  	apply (rule exI[where x="c - 1"], simp add: vector_smult_lneg vector_sub_rdistrib)
   1.362 -	apply (rule exI[where x=0], simp)
   1.363  	done}
   1.364      ultimately have ?thesis by blast}
   1.365    ultimately show ?thesis by blast