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.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.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.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.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.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.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
```