# HG changeset patch # User chaieb # Date 1236194516 0 # Node ID c88af4619a7324d3945b30f17ed6284f1b97f116 # Parent 5794fee816c31cdc84b33ec372518e215876d503 fixed proofs; added rules as default simp-rules diff -r 5794fee816c3 -r c88af4619a73 src/HOL/Library/Euclidean_Space.thy --- a/src/HOL/Library/Euclidean_Space.thy Wed Mar 04 19:21:56 2009 +0000 +++ b/src/HOL/Library/Euclidean_Space.thy Wed Mar 04 19:21:56 2009 +0000 @@ -626,7 +626,7 @@ ultimately show ?thesis by metis qed -lemma dot_pos_lt: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] +lemma dot_pos_lt[simp]: "(0 < x \ x) \ (x::'a::{ordered_ring_strict,ring_no_zero_divisors} ^ 'n) \ 0" using dot_eq_0[of x] dot_pos_le[of x] by (auto simp add: le_less) subsection{* The collapse of the general concepts to dimension one. *} @@ -759,10 +759,10 @@ text{* Hence derive more interesting properties of the norm. *} -lemma norm_0: "norm (0::real ^ 'n) = 0" +lemma norm_0[simp]: "norm (0::real ^ 'n) = 0" by (rule norm_zero) -lemma norm_mul: "norm(a *s x) = abs(a) * norm x" +lemma norm_mul[simp]: "norm(a *s x) = abs(a) * norm x" by (simp add: vector_norm_def vector_component setL2_right_distrib abs_mult cong: strong_setL2_cong) lemma norm_eq_0_dot: "(norm x = 0) \ (x \ x = (0::real))" @@ -772,11 +772,11 @@ lemma norm_pow_2: "norm x ^ 2 = x \ x" by (simp add: real_vector_norm_def) lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) -lemma vector_mul_eq_0: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" +lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" by vector -lemma vector_mul_lcancel: "a *s x = a *s y \ a = (0::real) \ x = y" +lemma vector_mul_lcancel[simp]: "a *s x = a *s y \ a = (0::real) \ x = y" by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) -lemma vector_mul_rcancel: "a *s x = b *s x \ (a::real) = b \ x = 0" +lemma vector_mul_rcancel[simp]: "a *s x = b *s x \ (a::real) = b \ x = 0" by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) lemma vector_mul_lcancel_imp: "a \ (0::real) ==> a *s x = a *s y ==> (x = y)" by (metis vector_mul_lcancel) @@ -814,28 +814,6 @@ lemma norm_triangle_lt: "norm(x::real ^'n) + norm(y) < e ==> norm(x + y) < e" by (metis basic_trans_rules(21) norm_triangle_ineq) -lemma setsum_delta: - assumes fS: "finite S" - shows "setsum (\k. if k=a then b k else 0) S = (if a \ S then b a else 0)" -proof- - let ?f = "(\k. if k=a then b k else 0)" - {assume a: "a \ S" - hence "\ k\ S. ?f k = 0" by simp - hence ?thesis using a by simp} - moreover - {assume a: "a \ S" - let ?A = "S - {a}" - let ?B = "{a}" - have eq: "S = ?A \ ?B" using a by blast - have dj: "?A \ ?B = {}" by simp - from fS have fAB: "finite ?A" "finite ?B" by auto - have "setsum ?f S = setsum ?f ?A + setsum ?f ?B" - using setsum_Un_disjoint[OF fAB dj, of ?f, unfolded eq[symmetric]] - by simp - then have ?thesis using a by simp} - ultimately show ?thesis by blast -qed - lemma component_le_norm: "i \ {1 .. dimindex(UNIV :: 'n set)} ==> \x$i\ <= norm (x::real ^ 'n)" apply (simp add: vector_norm_def) apply (rule member_le_setL2, simp_all) @@ -852,7 +830,7 @@ lemma norm_le_l1: "norm (x:: real ^'n) <= setsum(\i. \x$i\) {1..dimindex(UNIV::'n set)}" by (simp add: vector_norm_def setL2_le_setsum) -lemma real_abs_norm: "\ norm x\ = norm (x :: real ^'n)" +lemma real_abs_norm[simp]: "\ norm x\ = norm (x :: real ^'n)" by (rule abs_norm_cancel) lemma real_abs_sub_norm: "\norm(x::real ^'n) - norm y\ <= norm(x - y)" by (rule norm_triangle_ineq3) @@ -929,6 +907,7 @@ apply simp_all done + (* FIXME: Move all these theorems into the ML code using lemma antiquotation *) lemma norm_add_rule_thm: "b1 >= norm(x1 :: real ^'n) \ b2 >= norm(x2) ==> b1 + b2 >= norm(x1 + x2)" apply (rule norm_triangle_le) by simp @@ -977,17 +956,17 @@ text{* Hence more metric properties. *} -lemma dist_refl: "dist x x = 0" by norm +lemma dist_refl[simp]: "dist x x = 0" by norm lemma dist_sym: "dist x y = dist y x"by norm -lemma dist_pos_le: "0 <= dist x y" by norm +lemma dist_pos_le[simp]: "0 <= dist x y" by norm lemma dist_triangle: "dist x z <= dist x y + dist y z" by norm lemma dist_triangle_alt: "dist y z <= dist x y + dist x z" by norm -lemma dist_eq_0: "dist x y = 0 \ x = y" by norm +lemma dist_eq_0[simp]: "dist x y = 0 \ x = y" by norm lemma dist_pos_lt: "x \ y ==> 0 < dist x y" by norm lemma dist_nz: "x \ y \ 0 < dist x y" by norm @@ -1003,12 +982,12 @@ lemma dist_triangle_add: "dist (x + y) (x' + y') <= dist x x' + dist y y'" by norm -lemma dist_mul: "dist (c *s x) (c *s y) = \c\ * dist x y" +lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y" unfolding dist_def vector_ssub_ldistrib[symmetric] norm_mul .. lemma dist_triangle_add_half: " dist x x' < e / 2 \ dist y y' < e / 2 ==> dist(x + y) (x' + y') < e" by norm -lemma dist_le_0: "dist x y <= 0 \ x = y" by norm +lemma dist_le_0[simp]: "dist x y <= 0 \ x = y" by norm lemma setsum_eq: "setsum f S = (\ i. setsum (\x. (f x)$i ) S)" apply vector @@ -1035,47 +1014,6 @@ shows "(setsum f S)$i = setsum (\x. (f x)$i) S" using i by (simp add: setsum_eq Cart_lambda_beta) - (* This needs finiteness assumption due to the definition of fold!!! *) - -lemma setsum_superset: - assumes fb: "finite B" and ab: "A \ B" - and f0: "\x \ B - A. f x = 0" - shows "setsum f B = setsum f A" -proof- - from ab fb have fa: "finite A" by (metis finite_subset) - from fb have fba: "finite (B - A)" by (metis finite_Diff) - have d: "A \ (B - A) = {}" by blast - from ab have b: "B = A \ (B - A)" by blast - from setsum_Un_disjoint[OF fa fba d, of f] b - setsum_0'[OF f0] - show "setsum f B = setsum f A" by simp -qed - -lemma setsum_restrict_set: - assumes fA: "finite A" - shows "setsum f (A \ B) = setsum (\x. if x \ B then f x else 0) A" -proof- - from fA have fab: "finite (A \ B)" by auto - have aba: "A \ B \ A" by blast - let ?g = "\x. if x \ A\B then f x else 0" - from setsum_superset[OF fA aba, of ?g] - show ?thesis by simp -qed - -lemma setsum_cases: - assumes fA: "finite A" - shows "setsum (\x. if x \ B then f x else g x) A = - setsum f (A \ B) + setsum g (A \ - B)" -proof- - have a: "A = A \ B \ A \ -B" "(A \ B) \ (A \ -B) = {}" - by blast+ - from fA - have f: "finite (A \ B)" "finite (A \ -B)" by auto - let ?g = "\x. if x \ B then f x else g x" - from setsum_Un_disjoint[OF f a(2), of ?g] a(1) - show ?thesis by simp -qed - lemma setsum_norm: fixes f :: "'a \ 'b::real_normed_vector" assumes fS: "finite S" @@ -1173,41 +1111,6 @@ from setsum_Un_disjoint[of "?A" "?B" f] eq d show ?thesis by auto qed -lemma setsum_reindex_nonzero: - assumes fS: "finite S" - and nz: "\ x y. x \ S \ y \ S \ x \ y \ f x = f y \ h (f x) = 0" - shows "setsum h (f ` S) = setsum (h o f) S" -using nz -proof(induct rule: finite_induct[OF fS]) - case 1 thus ?case by simp -next - case (2 x F) - {assume fxF: "f x \ f ` F" hence "\y \ F . f y = f x" by auto - then obtain y where y: "y \ F" "f x = f y" by auto - from "2.hyps" y have xy: "x \ y" by auto - - from "2.prems"[of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp - have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto - also have "\ = setsum (h o f) (insert x F)" - using "2.hyps" "2.prems" h0 by auto - finally have ?case .} - moreover - {assume fxF: "f x \ f ` F" - have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" - using fxF "2.hyps" by simp - also have "\ = setsum (h o f) (insert x F)" - using "2.hyps" "2.prems" fxF - apply auto apply metis done - finally have ?case .} - ultimately show ?case by blast -qed - -lemma setsum_Un_nonzero: - assumes fS: "finite S" and fF: "finite F" - and f: "\ x\ S \ F . f x = (0::'a::ab_group_add)" - shows "setsum f (S \ F) = setsum f S + setsum f F" - using setsum_Un[OF fS fF, of f] setsum_0'[OF f] by simp - lemma setsum_natinterval_left: assumes mn: "(m::nat) <= n" shows "setsum f {m..n} = f m + setsum f {m + 1..n}" @@ -1249,109 +1152,9 @@ shows "setsum (\y. setsum g {x. x\ S \ f x = y}) T = setsum g S" apply (subst setsum_image_gen[OF fS, of g f]) -apply (rule setsum_superset[OF fT fST]) +apply (rule setsum_mono_zero_right[OF fT fST]) by (auto intro: setsum_0') -(* FIXME: Change the name to fold_image\ *) -lemma (in comm_monoid_mult) fold_1': "finite S \ (\x\S. f x = 1) \ fold_image op * f 1 S = 1" - apply (induct set: finite) - apply simp by (auto simp add: fold_image_insert) - -lemma (in comm_monoid_mult) fold_union_nonzero: - assumes fS: "finite S" and fT: "finite T" - and I0: "\x \ S\T. f x = 1" - shows "fold_image (op *) f 1 (S \ T) = fold_image (op *) f 1 S * fold_image (op *) f 1 T" -proof- - have "fold_image op * f 1 (S \ T) = 1" - apply (rule fold_1') - using fS fT I0 by auto - with fold_image_Un_Int[OF fS fT] show ?thesis by simp -qed - -lemma setsum_union_nonzero: - assumes fS: "finite S" and fT: "finite T" - and I0: "\x \ S\T. f x = 0" - shows "setsum f (S \ T) = setsum f S + setsum f T" - using fS fT - apply (simp add: setsum_def) - apply (rule comm_monoid_add.fold_union_nonzero) - using I0 by auto - -lemma setprod_union_nonzero: - assumes fS: "finite S" and fT: "finite T" - and I0: "\x \ S\T. f x = 1" - shows "setprod f (S \ T) = setprod f S * setprod f T" - using fS fT - apply (simp add: setprod_def) - apply (rule fold_union_nonzero) - using I0 by auto - -lemma setsum_unions_nonzero: - assumes fS: "finite S" and fSS: "\T \ S. finite T" - and f0: "\T1 T2 x. T1\S \ T2\S \ T1 \ T2 \ x \ T1 \ x \ T2 \ f x = 0" - shows "setsum f (\S) = setsum (\T. setsum f T) S" - using fSS f0 -proof(induct rule: finite_induct[OF fS]) - case 1 thus ?case by simp -next - case (2 T F) - then have fTF: "finite T" "\T\F. finite T" "finite F" and TF: "T \ F" - and H: "setsum f (\ F) = setsum (setsum f) F" by (auto simp add: finite_insert) - from fTF have fUF: "finite (\F)" by (auto intro: finite_Union) - from "2.prems" TF fTF - show ?case - by (auto simp add: H[symmetric] intro: setsum_union_nonzero[OF fTF(1) fUF, of f]) -qed - - (* FIXME : Copied from Pocklington --- should be moved to Finite_Set!!!!!!!! *) - - -lemma (in comm_monoid_mult) fold_related: - assumes Re: "R e e" - and Rop: "\x1 y1 x2 y2. R x1 x2 \ R y1 y2 \ R (x1 * y1) (x2 * y2)" - and fS: "finite S" and Rfg: "\x\S. R (h x) (g x)" - shows "R (fold_image (op *) h e S) (fold_image (op *) g e S)" - using fS by (rule finite_subset_induct) (insert assms, auto) - - (* FIXME: I think we can get rid of the finite assumption!! *) -lemma (in comm_monoid_mult) - fold_eq_general: - assumes fS: "finite S" - and h: "\y\S'. \!x. x\ S \ h(x) = y" - and f12: "\x\S. h x \ S' \ f2(h x) = f1 x" - shows "fold_image (op *) f1 e S = fold_image (op *) f2 e S'" -proof- - from h f12 have hS: "h ` S = S'" by auto - {fix x y assume H: "x \ S" "y \ S" "h x = h y" - from f12 h H have "x = y" by auto } - hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast - from f12 have th: "\x. x \ S \ (f2 \ h) x = f1 x" by auto - from hS have "fold_image (op *) f2 e S' = fold_image (op *) f2 e (h ` S)" by simp - also have "\ = fold_image (op *) (f2 o h) e S" - using fold_image_reindex[OF fS hinj, of f2 e] . - also have "\ = fold_image (op *) f1 e S " using th fold_image_cong[OF fS, of "f2 o h" f1 e] - by blast - finally show ?thesis .. -qed - -lemma (in comm_monoid_mult) fold_eq_general_inverses: - assumes fS: "finite S" - and kh: "\y. y \ T \ k y \ S \ h (k y) = y" - and hk: "\x. x \ S \ h x \ T \ k (h x) = x \ g (h x) = f x" - shows "fold_image (op *) f e S = fold_image (op *) g e T" - using fold_eq_general[OF fS, of T h g f e] kh hk by metis - -lemma setsum_eq_general_reverses: - assumes fS: "finite S" and fT: "finite T" - and kh: "\y. y \ T \ k y \ S \ h (k y) = y" - and hk: "\x. x \ S \ h x \ T \ k (h x) = x \ g (h x) = f x" - shows "setsum f S = setsum g T" - apply (simp add: setsum_def fS fT) - apply (rule comm_monoid_add.fold_eq_general_inverses[OF fS]) - apply (erule kh) - apply (erule hk) - done - lemma vsum_norm_allsubsets_bound: fixes f:: "'a \ real ^'n" assumes fP: "finite P" and fPs: "\Q. Q \ P \ norm (setsum f Q) \ e" @@ -1383,7 +1186,7 @@ by (auto simp add: setsum_negf setsum_component vector_component intro: abs_le_D1) have "setsum (\x. \f x $ i\) P = setsum (\x. \f x $ i\) ?Pp + setsum (\x. \f x $ i\) ?Pn" apply (subst thp) - apply (rule setsum_Un_nonzero) + apply (rule setsum_Un_zero) using fP thp0 by auto also have "\ \ 2*e" using Pne Ppe by arith finally show "setsum (\x. \f x $ i\) P \ 2*e" . @@ -1392,7 +1195,7 @@ qed lemma dot_lsum: "finite S \ setsum f S \ (y::'a::{comm_ring}^'n) = setsum (\x. f x \ y) S " - by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd) + by (induct rule: finite_induct, auto simp add: dot_lzero dot_ladd dot_radd) lemma dot_rsum: "finite S \ (y::'a::{comm_ring}^'n) \ setsum f S = setsum (\x. y \ f x) S " by (induct rule: finite_induct, auto simp add: dot_rzero dot_radd) @@ -4137,7 +3940,8 @@ apply (subst Cy) using C(1) fth apply (simp only: setsum_clauses) - apply (auto simp add: dot_ladd dot_lmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth]) + thm dot_ladd + apply (auto simp add: dot_ladd dot_radd dot_lmult dot_rmult dot_eq_0 dot_sym[of y a] dot_lsum[OF fth]) apply (rule setsum_0') apply clarsimp apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format]) @@ -5294,14 +5098,11 @@ have ?lhs unfolding collinear_def c apply (rule exI[where x=x]) apply auto - apply (rule exI[where x=0], simp) apply (rule exI[where x="- 1"], simp only: vector_smult_lneg vector_smult_lid) apply (rule exI[where x= "-c"], simp only: vector_smult_lneg) apply (rule exI[where x=1], simp) - apply (rule exI[where x=0], simp) apply (rule exI[where x="1 - c"], simp add: vector_smult_lneg vector_sub_rdistrib) apply (rule exI[where x="c - 1"], simp add: vector_smult_lneg vector_sub_rdistrib) - apply (rule exI[where x=0], simp) done} ultimately have ?thesis by blast} ultimately show ?thesis by blast