# HG changeset patch # User nipkow # Date 1108994650 -3600 # Node ID 333a8824456991b447db46ee075ecffb4872d5b7 # Parent d8edf54cc28c76408b1f206d8add326dede62b7a comprehensive cleanup, replacing sumr by setsum diff -r d8edf54cc28c -r 333a88244569 src/HOL/Complex/CSeries.thy --- a/src/HOL/Complex/CSeries.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Complex/CSeries.thy Mon Feb 21 15:04:10 2005 +0100 @@ -63,7 +63,7 @@ apply (simp add: add_ac) done -lemma sumc_cmod: "cmod(sumc m n f) \ sumr m n (%i. cmod(f i))" +lemma sumc_cmod: "cmod(sumc m n f) \ (\i=m.. sumr m n (%n. cmod (f n))" -by (induct "n", auto simp add: add_increasing) +lemma sumr_cmod_ge_zero [iff]: "0 \ (\n=m..n=m..n=m.. B" -shows "setsum f A \ (setsum f B :: nat)" -proof - - have "setsum f A \ setsum f A + setsum f (B-A)" by arith - also have "\ = setsum f (A \ (B-A))" using fin finite_subset[OF sub fin] - by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) - also have "A \ (B-A) = B" using sub by blast - finally show ?thesis . -qed - lemma setsum_negf: "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A" proof (cases "finite A") @@ -1118,6 +1107,30 @@ case False thus ?thesis by (simp add: setsum_def) qed +lemma setsum_mono2: +fixes f :: "'a \ 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}" +assumes fin: "finite B" and sub: "A \ B" and nn: "\b. b \ B-A \ 0 \ f b" +shows "setsum f A \ setsum f B" +proof - + have "setsum f A \ setsum f A + setsum f (B-A)" + by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def) + also have "\ = setsum f (A \ (B-A))" using fin finite_subset[OF sub fin] + by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) + also have "A \ (B-A) = B" using sub by blast + finally show ?thesis . +qed +(* +lemma setsum_mono2_nat: + assumes fin: "finite B" and sub: "A \ B" +shows "setsum f A \ (setsum f B :: nat)" +proof - + have "setsum f A \ setsum f A + setsum f (B-A)" by arith + also have "\ = setsum f (A \ (B-A))" using fin finite_subset[OF sub fin] + by (simp add:setsum_Un_disjoint del:Un_Diff_cancel) + also have "A \ (B-A) = B" using sub by blast + finally show ?thesis . +qed +*) lemma setsum_mult: fixes f :: "'a => ('b::semiring_0_cancel)" shows "r * setsum f A = setsum (%n. r * f n) A" @@ -1164,6 +1177,26 @@ case False thus ?thesis by (simp add: setsum_def) qed +lemma abs_setsum_abs[simp]: + fixes f :: "'a => ('b::lordered_ab_group_abs)" + shows "abs (\a\A. abs(f a)) = (\a\A. abs(f a))" +proof (cases "finite A") + case True + thus ?thesis + proof (induct) + case empty thus ?case by simp + next + case (insert a A) + hence "\\a\insert a A. \f a\\ = \\f a\ + (\a\A. \f a\)\" by simp + also have "\ = \\f a\ + \\a\A. \f a\\\" using insert by simp + also have "\ = \f a\ + \\a\A. \f a\\" by simp + also have "\ = (\a\insert a A. \f a\)" using insert by simp + finally show ?case . + qed +next + case False thus ?thesis by (simp add: setsum_def) +qed + subsection {* Generalized product over a set *} @@ -1430,7 +1463,7 @@ by (simp add: card_insert_if) lemma card_mono: "\ finite B; A \ B \ \ card A \ card B" -by (simp add: card_def setsum_mono2_nat) +by (simp add: card_def setsum_mono2) lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)" apply (induct set: Finites, simp, clarify) @@ -1497,13 +1530,13 @@ done -lemma setsum_constant_nat: "(\x\A. y) = (card A) * y" - -- {* Generalized to any @{text comm_semiring_1_cancel} in - @{text IntDef} as @{text setsum_constant}. *} -apply (cases "finite A") -apply (erule finite_induct, auto) +lemma setsum_constant [simp]: "(\x \ A. y) = of_nat(card A) * y" +apply (cases "finite A") +apply (erule finite_induct) +apply (auto simp add: ring_distrib add_ac) done + lemma setprod_constant: "finite A ==> (\x: A. (y::'a::recpower)) = y^(card A)" apply (erule finite_induct) apply (auto simp add: power_Suc) @@ -1512,15 +1545,18 @@ subsubsection {* Cardinality of unions *} +lemma of_nat_id[simp]: "(of_nat n :: nat) = n" +by(induct n, auto) + lemma card_UN_disjoint: "finite I ==> (ALL i:I. finite (A i)) ==> (ALL i:I. ALL j:I. i \ j --> A i Int A j = {}) ==> card (UNION I A) = (\i\I. card(A i))" - apply (simp add: card_def) + apply (simp add: card_def del: setsum_constant) apply (subgoal_tac "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I") - apply (simp add: setsum_UN_disjoint) - apply (simp add: setsum_constant_nat cong: setsum_cong) + apply (simp add: setsum_UN_disjoint del: setsum_constant) + apply (simp cong: setsum_cong) done lemma card_Union_disjoint: @@ -1546,7 +1582,7 @@ done lemma card_image: "inj_on f A ==> card (f ` A) = card A" -by(simp add:card_def setsum_reindex o_def) +by(simp add:card_def setsum_reindex o_def del:setsum_constant) lemma endo_inj_surj: "finite A ==> f ` A \ A ==> inj_on f A ==> f ` A = A" by (simp add: card_seteq card_image) @@ -1587,18 +1623,17 @@ lemma card_SigmaI [simp]: "\ finite A; ALL a:A. finite (B a) \ \ card (SIGMA x: A. B x) = (\a\A. card (B a))" -by(simp add:card_def setsum_Sigma) +by(simp add:card_def setsum_Sigma del:setsum_constant) lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)" apply (cases "finite A") apply (cases "finite B") - apply (simp add: setsum_constant_nat) apply (auto simp add: card_eq_0_iff - dest: finite_cartesian_productD1 finite_cartesian_productD2) + dest: finite_cartesian_productD1 finite_cartesian_productD2) done lemma card_cartesian_product_singleton: "card({x} <*> A) = card(A)" -by (simp add: card_cartesian_product) +by (simp add: card_cartesian_product) diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HSeries.thy --- a/src/HOL/Hyperreal/HSeries.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/HSeries.thy Mon Feb 21 15:04:10 2005 +0100 @@ -15,10 +15,10 @@ sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" "sumhr p == (%(M,N,f). Abs_hypreal(\X \ Rep_hypnat(M). \Y \ Rep_hypnat(N). - hyprel ``{%n::nat. sumr (X n) (Y n) f})) p" + hyprel ``{%n::nat. setsum f {X n..real,real] => bool" (infixr "NSsums" 80) - "f NSsums s == (%n. sumr 0 n f) ----NS> s" + "f NSsums s == (%n. setsum f {0.. s" NSsummable :: "(nat=>real) => bool" "NSsummable f == (\s. f NSsums s)" @@ -30,9 +30,9 @@ lemma sumhr: "sumhr(Abs_hypnat(hypnatrel``{%n. M n}), Abs_hypnat(hypnatrel``{%n. N n}), f) = - Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})" + Abs_hypreal(hyprel `` {%n. setsum f {M n.. sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)" apply (cases n, cases p) apply (auto elim!: FreeUltrafilterNat_subset simp - add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add) + add: hypnat_zero_def sumhr hypreal_add hypnat_less setsum_add_nat_ivl) done lemma sumhr_split_diff: "n

sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)" @@ -124,7 +124,7 @@ lemma sumhr_shift_bounds: "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))" apply (cases m, cases n) -apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq) +apply (simp add: sumhr hypnat_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq) done @@ -147,15 +147,20 @@ add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def hypnat_zero_def hypnat_omega_def) +(* FIXME move *) +lemma setsum_ivl_cong: + "i = m \ j = n \ (!!x. m <= x \ x < n \ f x = g x) \ + setsum f {i..n. m \ Suc n --> f n = r) & m \ na ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = (hypreal_of_nat (na - m) * hypreal_of_real r)" -by (auto dest!: sumr_interval_const - simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq - hypnat_of_nat_eq hypreal_of_real_def hypreal_mult) +by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq hypreal_of_real_def + real_of_nat_def hypreal_mult cong: setsum_ivl_cong) -lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)" +lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0.. (s = NSsuminf f)" by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique) -lemma NSseries_zero: "\m. n \ Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)" +lemma NSseries_zero: + "\m. n \ Suc m --> f(m) = 0 ==> f NSsums (setsum f {0.. x)" apply (cases x) apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow - real_sqrt_pow2_iff simp del: hpowr_Suc realpow_Suc) done @@ -586,7 +585,7 @@ apply (frule STAR_sin_Infinitesimal_divide [OF Infinitesimal_pi_divide_HNatInfinite pi_divide_HNatInfinite_not_zero]) -apply (auto simp add: inverse_mult_distrib) +apply (auto) apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"]) apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac) done diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Mon Feb 21 15:04:10 2005 +0100 @@ -167,7 +167,7 @@ "X\ FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) apply (safe, drule_tac x = X in bspec) -apply (auto simp add: UNIV_diff_Compl) +apply (auto) done lemma FreeUltrafilterNat_Compl_iff1: @@ -183,12 +183,9 @@ apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric]) done -lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \ FreeUltrafilterNat" +lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \ FreeUltrafilterNat" by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4]) -lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \ FreeUltrafilterNat" -by auto - lemma FreeUltrafilterNat_Nat_set_refl [intro]: "{n. P(n) = P(n)} \ FreeUltrafilterNat" by simp @@ -200,7 +197,7 @@ by (rule ccontr, simp) lemma FreeUltrafilterNat_all: "\n. P(n) ==> {n. P(n)} \ FreeUltrafilterNat" -by (auto intro: FreeUltrafilterNat_Nat_set) +by (auto) text{*Define and use Ultrafilter tactics*} @@ -335,8 +332,7 @@ lemma hypreal_minus: "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})" -by (simp add: hypreal_minus_def Abs_hypreal_inject - hyprel_in_hypreal [THEN Abs_hypreal_inverse] +by (simp add: hypreal_minus_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent]) lemma hypreal_diff: @@ -348,7 +344,7 @@ by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add) lemma hypreal_add_minus_left: "-z + z = (0::hypreal)" -by (simp add: hypreal_add_commute hypreal_add_minus) +by (simp add: hypreal_add_commute) subsection{*Hyperreal Multiplication*} @@ -390,8 +386,7 @@ lemma hypreal_inverse: "inverse (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})" -by (simp add: hypreal_inverse_def Abs_hypreal_inject - hyprel_in_hypreal [THEN Abs_hypreal_inverse] +by (simp add: hypreal_inverse_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent]) lemma hypreal_mult_inverse: @@ -466,7 +461,7 @@ by intro_classes (rule hypreal_le_linear) lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \ y" -by (auto simp add: order_less_irrefl) +by (auto) lemma hypreal_add_left_mono: "x \ y ==> z + x \ z + (y::hypreal)" apply (cases x, cases y, cases z) @@ -702,7 +697,6 @@ val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1"; val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2"; val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV"; -val FreeUltrafilterNat_Nat_set = thm "FreeUltrafilterNat_Nat_set"; val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl"; val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P"; val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P"; diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/HyperPow.thy Mon Feb 21 15:04:10 2005 +0100 @@ -71,7 +71,7 @@ lemma hrabs_hrealpow_two [simp]: "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)" -by (simp add: abs_mult) +by (simp) lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \ 2 ^ n" by (insert power_increasing [of 0 n "2::hypreal"], simp) diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Integration.thy --- a/src/HOL/Hyperreal/Integration.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/Integration.thy Mon Feb 21 15:04:10 2005 +0100 @@ -40,7 +40,7 @@ --{*Riemann sum*} rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" - "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))" + "rsum == %(D,p) f. \n=0..n=0.. b ==> Integral(a,b) (%x. 1) (b - a)" @@ -453,7 +453,7 @@ apply (auto simp add: zero_less_divide_iff) apply (rule exI) apply (auto simp add: tpart_def rsum_def) -apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = f b - f a") +apply (subgoal_tac "(\n=0..n=0.. rsum(D,p) f \ rsum(D,p) g" apply (simp add: rsum_def) -apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2] +apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2] dest!: lemma_Integral_le) done diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Lim.thy --- a/src/HOL/Hyperreal/Lim.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/Lim.thy Mon Feb 21 15:04:10 2005 +0100 @@ -771,7 +771,7 @@ apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1) apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1]) apply (subgoal_tac [2] "( *f* (%z. z-x)) u \ (0::hypreal) ") -apply (auto simp add: times_divide_eq_left diff_minus +apply (auto simp add: diff_minus approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] Infinitesimal_subset_HFinite [THEN subsetD]) done @@ -787,7 +787,7 @@ apply (drule_tac x = h in bspec) apply (drule_tac [2] c = h in approx_mult1) apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: times_divide_eq_left diff_minus) + simp add: diff_minus) done lemma NSDERIVD3: @@ -799,7 +799,7 @@ apply (rule ccontr, drule_tac x = h in bspec) apply (drule_tac [2] c = h in approx_mult1) apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] - simp add: mult_assoc times_divide_eq_left diff_minus) + simp add: mult_assoc diff_minus) done text{*Now equivalence between NSDERIV and DERIV*} @@ -821,7 +821,7 @@ apply (drule_tac x3=D in HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult, THEN mem_infmal_iff [THEN iffD1]]) -apply (auto simp add: times_divide_eq_right mult_commute +apply (auto simp add: mult_commute intro: approx_trans approx_minus_iff [THEN iffD2]) done @@ -872,7 +872,7 @@ apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption) apply (erule_tac V = "(x + y) / z = hypreal_of_real D + yb" in thin_rl) apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add - simp add: times_divide_eq_left mult_assoc mem_infmal_iff [symmetric]) + simp add: mult_assoc mem_infmal_iff [symmetric]) apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) done @@ -983,7 +983,7 @@ in hypreal_mult_right_cancel [THEN iffD2]) apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) + - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl) apply assumption -apply (simp add: times_divide_eq_left times_divide_eq_right [symmetric]) +apply (simp add: times_divide_eq_right [symmetric]) apply (auto simp add: left_distrib) done @@ -1188,7 +1188,7 @@ show "\g. (\z. f z - f x = g z * (z-x)) \ isCont g x \ g x = l" proof (intro exI conjI) let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" - show "\z. f z - f x = ?g z * (z-x)" by (simp add: times_divide_eq) + show "\z. f z - f x = ?g z * (z-x)" by (simp) show "isCont ?g x" using der by (simp add: isCont_iff DERIV_iff diff_minus cong: LIM_equal [rule_format]) @@ -1327,13 +1327,13 @@ \n. snd(Bolzano_bisect P a b (Suc n)) \ snd (Bolzano_bisect P a b n)" apply (rule allI) apply (induct_tac "n") -apply (auto simp add: Bolzano_bisect_le Let_def split_def times_divide_eq) +apply (auto simp add: Bolzano_bisect_le Let_def split_def) done lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" -apply (auto simp add: times_divide_eq) +apply (auto) apply (drule_tac f = "%u. (1/2) *u" in arg_cong) -apply (simp add: times_divide_eq) +apply (simp) done lemma Bolzano_bisect_diff: @@ -1798,7 +1798,7 @@ hence ba: "b-a \ 0" by arith show ?thesis by (rule real_mult_left_cancel [OF ba, THEN iffD1], - simp add: times_divide_eq right_diff_distrib, + simp add: right_diff_distrib, simp add: left_diff_distrib) qed @@ -1834,8 +1834,7 @@ proof (intro exI conjI) show "a < z" . show "z < b" . - show "f b - f a = (b - a) * ((f b - f a)/(b-a))" - by (simp add: times_divide_eq) + show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp) show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp qed qed @@ -1885,14 +1884,14 @@ lemma DERIV_const_ratio_const2: "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k" apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1]) -apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc times_divide_eq) +apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc) done lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)" -by (simp add: times_divide_eq) +by (simp) lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)" -by (simp add: times_divide_eq) +by (simp) text{*Gallileo's "trick": average velocity = av. of end velocities*} diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/MacLaurin.thy Mon Feb 21 15:04:10 2005 +0100 @@ -9,25 +9,32 @@ imports Log begin -lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" +(* FIXME generalize? *) +lemma sumr_offset: + "(\m=0..f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" +lemma sumr_offset2: + "\f. (\m=0..m=0..n f. sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f" +lemma sumr_offset4: + "\n f. setsum f {0::nat..m=0.. - sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else - ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) = - sumr 0 (Suc n) (%n. (if even(n) then 0 else - ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)" + (\n=Suc 0 ..< Suc n. if even(n) then 0 else + ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n = + (\n=0.. - \B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) + + \B. f h = (\m=0..m=0.. \t. 0 < t & t < h & f h = - sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) + + setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..g. - g = (%t. f t - (sumr 0 n (%m. (diff m 0 / real(fact m)) * t^m) + (B * (t^n / real(fact n)))))") + g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..difg. difg = (%m t. diff m t - (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) + (B * ((t ^ (n - m)) / real (fact (n - m))))))") + apply (simp add: eq_diff_eq' del: setsum_Suc) +apply (subgoal_tac "\difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..m. m < n --> difg m 0 = 0") prefer 2 apply clarify apply simp apply (frule_tac m = ma in less_add_one, clarify) - apply (simp del: sumr_Suc) + apply (simp del: setsum_Suc) apply (insert sumr_offset4 [of 1]) -apply (simp del: sumr_Suc fact_Suc realpow_Suc) +apply (simp del: setsum_Suc fact_Suc realpow_Suc) apply (subgoal_tac "\m. m < n --> (\t. 0 < t & t < h & DERIV (difg m) t :> 0) ") apply (rule allI, rule impI) apply (drule_tac x = ma and P="%m. m (\t. ?QQ m t)" in spec) @@ -181,11 +188,11 @@ apply (erule exE) apply (rule_tac x = t in exI) (* do some tidying up *) -apply (erule_tac [!] V= "difg = (%m t. diff m t - (sumr 0 (n - m) (%p. diff (m + p) 0 / real (fact p) * t ^ p) + B * (t ^ (n - m) / real (fact (n - m)))))" +apply (erule_tac [!] V= "difg = (%m t. diff m t - (setsum (%p. diff (m + p) 0 / real (fact p) * t ^ p) {0.. (\t. 0 < t & t < h & f h = - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + + (\m=0.. \t. 0 < t & t \ h & f h = - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + + (\m=0.. (\t. 0 < t & t \ h & f h = - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + + (\m=0.. \t. h < t & t < 0 & f h = - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + + (\m=0.. (\t. h < t & t < 0 & f h = - sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + + (\m=0..m t. m < n & abs t \ abs x --> DERIV (diff m) t :> diff (Suc m) t |] ==> \t. abs t \ abs x & f x = - sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) + + (\m=0..m x. DERIV (diff m) x :> diff(Suc m) x; x ~= 0; 0 < n |] ==> \t. 0 < abs t & abs t < abs x & - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + + f x = (\m=0..m x. DERIV (diff m) x :> diff(Suc m) x) & x ~= 0 & 0 < n --> (\t. 0 < abs t & abs t < abs x & - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + + f x = (\m=0.. 0 < n --> - sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) = + (\m=0..m x. DERIV (diff m) x :> diff (Suc m) x |] ==> \t. abs t \ abs x & - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + + f x = (\m=0..m x. DERIV (diff m) x :> diff (Suc m) x) --> (\t. abs t \ abs x & - f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) + + f x = (\m=0.. (\t. 0 < abs t & abs t < abs x & - exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + + exp x = (\m=0..t. abs t \ abs x & - exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) + + exp x = (\m=0..t. abs t \ abs x & sin x = - (sumr 0 n (%m. (if even m then 0 + (\m=0..t. sin x = - (sumr 0 n (%m. (if even m then 0 + (\m=0.. \t. 0 < t & t < x & sin x = - (sumr 0 n (%m. (if even m then 0 + (\m=0.. \t. 0 < t & t \ x & sin x = - (sumr 0 n (%m. (if even m then 0 + (\m=0..m=0..<(Suc n). + (if even m then (- 1) ^ (m div 2)/(real (fact m)) else 0) * 0 ^ m) = 1" by (induct "n", auto) lemma Maclaurin_cos_expansion: "\t. abs t \ abs x & cos x = - (sumr 0 n (%m. (if even m + (\m=0.. \t. 0 < t & t < x & cos x = - (sumr 0 n (%m. (if even m + (\m=0.. \t. x < t & t < 0 & cos x = - (sumr 0 n (%m. (if even m + (\m=0..m=0.. inverse(real (fact n)) * \x\ ^ n" proof - have "!! x (y::real). x \ 1 \ 0 \ y \ x * y \ 1 * y" diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/NSA.thy --- a/src/HOL/Hyperreal/NSA.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/NSA.thy Mon Feb 21 15:04:10 2005 +0100 @@ -61,7 +61,7 @@ lemma SReal_mult: "[| (x::hypreal) \ Reals; y \ Reals |] ==> x * y \ Reals" apply (simp add: SReal_def, safe) apply (rule_tac x = "r * ra" in exI) -apply (simp (no_asm) add: hypreal_of_real_mult) +apply (simp (no_asm)) done lemma SReal_inverse: "(x::hypreal) \ Reals ==> inverse x \ Reals" @@ -301,7 +301,7 @@ apply (auto simp add: Infinitesimal_def) apply (rule hypreal_sum_of_halves [THEN subst]) apply (drule half_gt_zero) -apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of) +apply (blast intro: hrabs_add_less SReal_divide_number_of) done lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)" @@ -325,7 +325,7 @@ apply (drule_tac x = "r/t" in bspec) apply (blast intro: SReal_divide) apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono) -apply (auto simp add: times_divide_eq_left zero_less_divide_iff) +apply (auto simp add: zero_less_divide_iff) done lemma Infinitesimal_HFinite_mult2: @@ -693,13 +693,13 @@ lemma Infinitesimal_add_approx: "[| y \ Infinitesimal; x + y = z |] ==> x @= z" apply (rule bex_Infinitesimal_iff [THEN iffD1]) apply (drule Infinitesimal_minus_iff [THEN iffD2]) -apply (auto simp add: minus_add_distrib hypreal_add_assoc [symmetric]) +apply (auto simp add: hypreal_add_assoc [symmetric]) done lemma Infinitesimal_add_approx_self: "y \ Infinitesimal ==> x @= x + y" apply (rule bex_Infinitesimal_iff [THEN iffD1]) apply (drule Infinitesimal_minus_iff [THEN iffD2]) -apply (auto simp add: minus_add_distrib hypreal_add_assoc [symmetric]) +apply (auto simp add: hypreal_add_assoc [symmetric]) done lemma Infinitesimal_add_approx_self2: "y \ Infinitesimal ==> x @= y + x" @@ -723,7 +723,7 @@ lemma approx_add_left_cancel: "d + b @= d + c ==> b @= c" apply (drule approx_minus_iff [THEN iffD1]) -apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac) +apply (simp add: approx_minus_iff [symmetric] add_ac) done lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c" @@ -733,7 +733,7 @@ lemma approx_add_mono1: "b @= c ==> d + b @= d + c" apply (rule approx_minus_iff [THEN iffD2]) -apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac) +apply (simp add: approx_minus_iff [symmetric] add_ac) done lemma approx_add_mono2: "b @= c ==> b + a @= c + a" @@ -805,7 +805,7 @@ done -subsection{* Zero is the Only Infinitesimal that is Also a Real*} +subsection{* Zero is the Only Infinitesimal that is also a Real*} lemma Infinitesimal_less_SReal: "[| x \ Reals; y \ Infinitesimal; 0 < x |] ==> y < x" @@ -1077,7 +1077,7 @@ isLub Reals {s. s \ Reals & s < x} t; r \ Reals; 0 < r |] ==> -(x + -t) \ r" -apply (auto simp add: minus_add_distrib) +apply (auto) apply (frule isLubD1a) apply (drule SReal_add_cancel, assumption) apply (drule_tac x = "-x" in SReal_minus, simp) @@ -1141,7 +1141,7 @@ lemma not_HFinite_HInfinite: "x\ HFinite ==> x \ HInfinite" apply (simp add: HInfinite_def HFinite_def, auto) apply (drule_tac x = "r + 1" in bspec) -apply (auto simp add: SReal_add) +apply (auto) done lemma HInfinite_HFinite_disj: "x \ HInfinite | x \ HFinite" @@ -1432,7 +1432,7 @@ ==> hypreal_of_real x + u < hypreal_of_real y" apply (simp add: Infinitesimal_def) apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp) -apply (auto simp add: add_commute abs_less_iff SReal_add SReal_minus) +apply (auto simp add: add_commute abs_less_iff SReal_minus) apply (simp add: compare_rls) done @@ -1646,7 +1646,7 @@ by (simp add: ex ey) also have "... = st ((ex + ey) + (st x + st y))" by (simp add: add_ac) also have "... = st x + st y" - by (simp add: prems st_SReal SReal_add Infinitesimal_add + by (simp add: prems st_SReal Infinitesimal_add st_Infinitesimal_add_SReal2) finally show ?thesis . qed @@ -1870,7 +1870,7 @@ apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp) apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset]) apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int) -apply (auto simp add: lemma_Int_HIa FreeUltrafilterNat_empty) +apply (auto simp add: lemma_Int_HIa) done lemma HInfinite_FreeUltrafilterNat_iff: @@ -1923,7 +1923,7 @@ lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \ \" apply (induct n) -apply (simp_all add: SReal_add) +apply (simp_all) done lemma lemma_Infinitesimal2: @@ -2075,7 +2075,7 @@ lemma real_of_nat_inverse_eq_iff: "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)" -by (auto simp add: inverse_inverse_eq real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym]) +by (auto simp add: real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym]) lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}" apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff) diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Poly.thy --- a/src/HOL/Hyperreal/Poly.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/Poly.thy Mon Feb 21 15:04:10 2005 +0100 @@ -1026,7 +1026,7 @@ apply (induct "p", auto) apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans) apply (rule abs_triangle_ineq) -apply (auto intro!: mult_mono simp add: abs_mult, arith) +apply (auto intro!: mult_mono, arith) done ML diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/SEQ.thy --- a/src/HOL/Hyperreal/SEQ.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/SEQ.thy Mon Feb 21 15:04:10 2005 +0100 @@ -169,7 +169,7 @@ apply (drule FreeUltrafilterNat_all) apply (erule_tac V = "{n. \Y n\ < r} : FreeUltrafilterNat" in thin_rl) apply (drule FreeUltrafilterNat_Int, assumption) -apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty) +apply (simp add: lemmaLIM2) done lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L" @@ -207,7 +207,7 @@ lemma NSLIMSEQ_mult: "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b" by (auto intro!: approx_mult_HFinite - simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric]) + simp add: NSLIMSEQ_def starfunNat_mult [symmetric]) lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b" by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult) @@ -707,7 +707,7 @@ apply (drule_tac M = M in lemmaCauchy1) apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset]) apply (rule FreeUltrafilterNat_Int) -apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set) +apply (auto intro: FreeUltrafilterNat_Int) done subsubsection{*Nonstandard Implies Standard*} diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Series.thy --- a/src/HOL/Hyperreal/Series.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Hyperreal/Series.thy Mon Feb 21 15:04:10 2005 +0100 @@ -3,6 +3,7 @@ Copyright : 1998 University of Cambridge Converted to Isar and polished by lcp +Converted to setsum and polished yet more by TNN *) header{*Finite Summation and Infinite Series*} @@ -11,11 +12,9 @@ imports SEQ Lim begin +(* FIXME why not globally? *) declare atLeastLessThan_empty[simp]; - -syntax sumr :: "[nat,nat,(nat=>real)] => real" -translations - "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)" +declare atLeastLessThan_iff[iff] constdefs sums :: "[nat=>real,real] => bool" (infixr "sums" 80) @@ -25,10 +24,9 @@ "summable f == (\s. f sums s)" suminf :: "(nat=>real) => real" - "suminf f == (@s. f sums s)" + "suminf f == SOME s. f sums s" - -lemma sumr_Suc [simp]: +lemma setsum_Suc[simp]: "setsum f {m.. m \ n; n \ p \ \ setsum f {m..\n. m \ Suc n --> f n = r; m \ k\ \ sumr m k f = (real(k-m) * r)" -apply (induct "k", auto) +(* +lemma sumr_interval_const2: + "[|\n\m. f n = r; m \ k|] + ==> sumr m k f = (real (k - m) * r)" +apply (induct "k", auto) apply (drule_tac x = k in spec) apply (auto dest!: le_imp_less_or_eq) apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) done +*) +(* FIXME split in tow steps +lemma setsum_nat_set_real_const: + "(\n. n\A \ f n = r) \ setsum f A = real(card A) * r" (is "PROP ?P") +proof (cases "finite A") + case True + thus "PROP ?P" + proof induct + case empty thus ?case by simp + next + case insert thus ?case by(simp add: left_distrib real_of_nat_Suc) + qed +next + case False thus "PROP ?P" by (simp add: setsum_def) +qed + *) -lemma sumr_interval_const2: - "[|\n\m. f n = r; m \ k|] - ==> sumr m k f = (real (k - m) * r)" -apply (induct "k", auto) -apply (drule_tac x = k in spec) -apply (auto dest!: le_imp_less_or_eq) -apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split) +(* +lemma sumr_le: + "[|\n\m. 0 \ (f n::real); m < k|] ==> setsum f {0.. setsum f {0..n\m. 0 \ f n; m < k|] ==> sumr 0 m f \ sumr 0 k f" apply (induct "k") @@ -120,13 +141,16 @@ apply (induct "n") apply (auto intro: add_mono simp add: le_def) done +*) +(* lemma sumr_ge_zero: "(\n\m. 0 \ f n) --> 0 \ sumr m n f" apply (induct "n", auto) apply (drule_tac x = n in spec, arith) done +*) -(* FIXME generalize *) +(* lemma rabs_sumr_rabs_cancel [simp]: "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))" by (induct "n", simp_all add: add_increasing) @@ -134,14 +158,19 @@ lemma sumr_zero [rule_format]: "\n \ N. f n = 0 ==> N \ m --> sumr m n f = 0" by (induct "n", auto) +*) lemma Suc_le_imp_diff_ge2: - "[|\n \ N. f (Suc n) = 0; Suc N \ m|] ==> sumr m n f = 0" -apply (rule sumr_zero) + "[|\n \ N. f (Suc n) = 0; Suc N \ m|] ==> setsum f {m..n=Suc 0..p. m \ p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g" by (induct "n", auto) +*) +lemma setsum_bounded: + assumes le: "\i. i\A \ f i \ (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})" + shows "setsum f A \ of_nat(card A) * K" +proof (cases "finite A") + case True + thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp +next + case False thus ?thesis by (simp add: setsum_def) +qed +(* lemma sumr_bound [rule_format (no_asm)]: "(\p. m \ p & p < m + n --> (f(p) \ K)) - --> (sumr m (m + n) f \ (real n * K))" + --> setsum f {m.. (real n * K)" apply (induct "n") apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc) done - +*) +(* FIXME should be generalized lemma sumr_bound2 [rule_format (no_asm)]: "(\p. 0 \ p & p < n --> (f(p) \ K)) - --> (sumr 0 n f \ (real n * K))" + --> setsum f {0.. (real n * K)" apply (induct "n") apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute) done - + *) +(* FIXME a bit specialized for [simp]! *) lemma sumr_group [simp]: - "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f" -apply (subgoal_tac "k = 0 | 0 < k", auto) + "(\m=0.. (%n. sumr 0 n f) ----> (suminf f)" + "summable f ==> (%n. setsum f {0.. (suminf f)" apply (simp add: summable_def suminf_def sums_def) apply (blast intro: someI2) done @@ -216,14 +261,31 @@ next one was called series_zero2 **********************) +lemma ivl_subset[simp]: + "({i.. {m.. i | m \ i & j \ (n::'a::linorder))" +apply(auto simp:linorder_not_le) +apply(rule ccontr) +apply(frule subsetCE[where c = n]) +apply(auto simp:linorder_not_le) +done + +lemma ivl_diff[simp]: + "i \ n \ {i..m. n \ m --> f(m) = 0) ==> f sums (sumr 0 n f)" + "(\m. n \ m --> f(m) = 0) ==> f sums (setsum f {0.. (%n. c * x(n)) sums (c * x0)" by (auto simp add: sums_def setsum_mult [symmetric] intro!: LIMSEQ_mult intro: LIMSEQ_const) @@ -249,7 +311,7 @@ by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf) lemma sums_group: - "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)" + "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..d. - f (n + (d + d)) < f (Suc (n + (d + d)))|] - ==> sumr 0 (n + Suc (Suc 0)) f \ sumr 0 (Suc (Suc 0) * Suc no + n) f" + "[|\d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |] + ==> setsum f {0.. setsum f {0..d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|] - ==> sumr 0 n f < suminf f" + ==> setsum f {0.. sumr 0 (Suc (Suc 0) * (Suc no) + n) f") -apply (rule_tac [2] y = "sumr 0 (n+ Suc (Suc 0)) f" in order_trans) +apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \ + setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}") +apply (rule_tac [2] y = "setsum f {0.. sumr 0 (Suc (Suc 0) * (Suc no) + n) f") +apply (subgoal_tac "suminf f \ setsum f {0..< Suc (Suc 0) * (Suc no) + n}") apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans) -prefer 3 apply simp +prefer 3 apply simp apply (drule_tac [2] x = 0 in spec) prefer 2 apply simp -apply (subgoal_tac "0 \ sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f") -apply (simp add: abs_if) +apply (subgoal_tac "0 \ setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f") +apply (simp add: abs_if) apply (auto simp add: linorder_not_less [symmetric]) done @@ -301,29 +364,30 @@ great as any partial sum.*} lemma series_pos_le: - "[| summable f; \m \ n. 0 \ f(m) |] ==> sumr 0 n f \ suminf f" + "[| summable f; \m \ n. 0 \ f(m) |] ==> setsum f {0.. suminf f" apply (drule summable_sums) apply (simp add: sums_def) -apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const) -apply (erule LIMSEQ_le, blast) -apply (rule_tac x = n in exI, clarify) -apply (drule le_imp_less_or_eq) -apply (auto intro: sumr_le) +apply (cut_tac k = "setsum f {0..m \ n. 0 < f(m) |] ==> sumr 0 n f < suminf f" -apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans) + "[| summable f; \m \ n. 0 < f(m) |] ==> setsum f {0.. sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)" +lemma sumr_geometric: + "x ~= 1 ==> (\i=0..e > 0. \N. \m \ N. \n. abs(sumr m n f) < e)" + (\e > 0. \N. \m \ N. \n. abs(setsum f {m..r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) - --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)" + --> DERIV (%x. \n=m.. (\r=m.. x ==> root(Suc n) (x ^ (Suc n)) = x" @@ -100,7 +100,7 @@ apply (rule_tac x = u and y = 1 in linorder_cases) apply (drule_tac n = n in realpow_Suc_less_one) apply (drule_tac [4] n = n in power_gt1_lemma) -apply (auto simp add: order_less_irrefl) +apply (auto) done @@ -117,7 +117,7 @@ lemma real_sqrt_one [simp]: "sqrt 1 = 1" by (simp add: sqrt_def) -lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\ = x) = (0 \ x)" +lemma real_sqrt_pow2_iff [iff]: "((sqrt x)\ = x) = (0 \ x)" apply (simp add: sqrt_def) apply (rule iffI) apply (cut_tac r = "root 2 x" in realpow_two_le) @@ -130,7 +130,7 @@ by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]]) lemma real_sqrt_pow2 [simp]: "0 \ x ==> (sqrt x)\ = x" -by (simp add: real_sqrt_pow2_iff) +by (simp) lemma real_sqrt_abs_abs [simp]: "sqrt\x\ ^ 2 = \x\" by (rule real_sqrt_pow2_iff [THEN iffD2], arith) @@ -209,13 +209,13 @@ lemma real_sqrt_sum_squares_mult_squared_eq [simp]: "sqrt ((x\ + y\) * (xa\ + ya\)) ^ 2 = (x\ + y\) * (xa\ + ya\)" -by (auto simp add: real_sqrt_pow2_iff zero_le_mult_iff simp del: realpow_Suc) +by (auto simp add: zero_le_mult_iff simp del: realpow_Suc) lemma real_sqrt_abs [simp]: "sqrt(x\) = \x\" apply (rule abs_realpow_two [THEN subst]) apply (rule real_sqrt_abs_abs [THEN subst]) apply (subst real_pow_sqrt_eq_sqrt_pow) -apply (auto simp add: numeral_2_eq_2 abs_mult) +apply (auto simp add: numeral_2_eq_2) done lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \x\" @@ -229,7 +229,7 @@ lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \ 0" apply (frule real_sqrt_pow2_gt_zero) -apply (auto simp add: numeral_2_eq_2 order_less_irrefl) +apply (auto simp add: numeral_2_eq_2) done lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x" @@ -269,21 +269,20 @@ apply (cut_tac x = r in reals_Archimedean3, auto) apply (drule_tac x = "\x\" in spec, safe) apply (rule_tac N = n and c = r in ratio_test) -apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc) +apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc) apply (rule mult_right_mono) apply (rule_tac b1 = "\x\" in mult_commute [THEN ssubst]) apply (subst fact_Suc) apply (subst real_of_nat_mult) -apply (auto simp add: abs_mult inverse_mult_distrib) +apply (auto) apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive) apply (rule order_less_imp_le) apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1]) -apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse) +apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc) apply (erule order_less_trans) apply (auto simp add: mult_less_cancel_left mult_ac) done - lemma summable_sin: "summable (%n. (if even n then 0 @@ -321,10 +320,8 @@ by (induct "n", auto) lemma lemma_STAR_cos2 [simp]: - "sumr 1 n (%n. if even n - then (- 1) ^ (n div 2)/(real (fact n)) * - 0 ^ n - else 0) = 0" + "(\n=1..p=0..p=0..p=0..p=0..p=0.. 0") apply (subgoal_tac [3] "x \ 0") apply (auto simp del: abs_inverse abs_mult simp add: abs_inverse [symmetric] realpow_not_zero abs_mult [symmetric] power_inverse power_mult_distrib [symmetric]) -apply (auto intro!: geometric_sums - simp add: power_abs inverse_eq_divide times_divide_eq) +apply (auto intro!: geometric_sums simp add: power_abs inverse_eq_divide) done lemma powser_inside: @@ -443,16 +438,16 @@ text{*Show that we can shift the terms down one*} lemma lemma_diffs: - "sumr 0 n (%n. (diffs c)(n) * (x ^ n)) = - sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) + + "(\n=0..n=0..n=0..n=0..p=0..p=0.. 0 ==> - (((z + h) ^ n) - (z ^ n)) * inverse h - - real n * (z ^ (n - Suc 0)) = - h * sumr 0 (n - Suc 0) (%p. (z ^ p) * - sumr 0 ((n - Suc 0) - p) - (%q. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))" + "h \ 0 ==> + (((z + h) ^ n) - (z ^ n)) * inverse h - real n * (z ^ (n - Suc 0)) = + h * (\p=0..< n - Suc 0. (z ^ p) * + (\q=0..< (n - Suc 0) - p. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))" apply (rule real_mult_left_cancel [THEN iffD1], simp (no_asm_simp)) apply (simp add: right_diff_distrib mult_ac) apply (simp add: mult_assoc [symmetric]) apply (case_tac "n") apply (auto simp add: lemma_realpow_diff_sumr2 right_diff_distrib [symmetric] mult_assoc - simp del: realpow_Suc sumr_Suc) -apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc) + simp del: realpow_Suc setsum_Suc) +apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_Suc) apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib sumdiff lemma_termdiff1 setsum_mult) -apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc) -apply (simp add: diff_minus [symmetric] less_iff_Suc_add) +apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc) +apply (simp add: diff_minus [symmetric] less_iff_Suc_add) apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp - del: sumr_Suc realpow_Suc) + del: setsum_Suc realpow_Suc) done +(* FIXME move *) +lemma sumr_bound2 [rule_format (no_asm)]: + "(\p. 0 \ p & p < n --> (f(p) \ K)) + --> setsum f {0.. (real n * K)" +using setsum_bounded[where A = "{0.. 0; \z\ \ K; \z + h\ \ K |] ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0)) \ real n * real (n - Suc 0) * K ^ (n - 2) * \h\" apply (subst lemma_termdiff2, assumption) -apply (simp add: abs_mult mult_commute) +apply (simp add: mult_commute) apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) apply (rule setsum_abs [THEN real_le_trans]) apply (simp add: mult_assoc [symmetric]) apply (simp add: mult_commute [of _ "real (n - Suc 0)"]) -apply (auto intro!: sumr_bound2 simp add: abs_mult) +apply (auto intro!: sumr_bound2) apply (case_tac "n", auto) apply (drule less_add_one) (*CLAIM_SIMP " (a * b * c = a * (c * (b::real))" mult_ac]*) apply clarify apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) = K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") -apply (simp (no_asm_simp) add: power_add del: sumr_Suc) -apply (auto intro!: mult_mono simp del: sumr_Suc) -apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc) +apply (simp (no_asm_simp) add: power_add del: setsum_Suc) +apply (auto intro!: mult_mono simp del: setsum_Suc) +apply (auto intro!: power_mono simp add: power_abs simp del: setsum_Suc) apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans) apply (subgoal_tac [2] "0 \ K") apply (drule_tac [2] n = d in zero_le_power) -apply (auto simp del: sumr_Suc) +apply (auto simp del: setsum_Suc) apply (rule setsum_abs [THEN real_le_trans]) -apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add) +apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: power_add) apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+) done @@ -910,7 +909,7 @@ hence "exp x * inverse (exp x) < exp y * inverse (exp x)" by (auto simp add: exp_add exp_minus) thus ?thesis - by (simp add: divide_inverse [symmetric] pos_less_divide_eq times_divide_eq + by (simp add: divide_inverse [symmetric] pos_less_divide_eq del: divide_self_if) qed @@ -1067,7 +1066,8 @@ by (auto intro!: sums_unique [symmetric] LIMSEQ_const simp add: sin_def sums_def simp del: power_0_left) -lemma lemma_series_zero2: "(\m. n \ m --> f m = 0) --> f sums sumr 0 n f" +lemma lemma_series_zero2: + "(\m. n \ m --> f m = 0) --> f sums setsum f {0..n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))" in order_less_trans) apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc) -apply (simp (no_asm) add: mult_assoc times_divide_eq del: sumr_Suc) +apply (simp (no_asm) add: mult_assoc del: setsum_Suc) apply (rule sumr_pos_lt_pair) apply (erule sums_summable, safe) apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] @@ -1520,10 +1518,10 @@ done lemma cos_pi [simp]: "cos pi = -1" -by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp add: times_divide_eq) +by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp) lemma sin_pi [simp]: "sin pi = 0" -by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp add: times_divide_eq) +by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp) lemma sin_cos_eq: "sin x = cos (pi/2 - x)" by (simp add: diff_minus cos_add) @@ -1706,7 +1704,7 @@ apply (cut_tac x="-x" in cos_zero_lemma, simp, simp) apply (force simp add: minus_equation_iff [of x]) apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib) -apply (auto simp add: cos_add times_divide_eq) +apply (auto simp add: cos_add) done (* ditto: but to a lesser extent *) @@ -1719,7 +1717,7 @@ apply (drule sin_zero_lemma, assumption+) apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe) apply (force simp add: minus_equation_iff [of x]) -apply (auto simp add: even_mult_two_ex times_divide_eq) +apply (auto simp add: even_mult_two_ex) done @@ -1757,7 +1755,7 @@ apply (simp add: tan_def) apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst]) apply (auto simp add: mult_assoc left_distrib) -apply (simp add: sin_add times_divide_eq) +apply (simp add: sin_add) done lemma tan_add: @@ -2068,7 +2066,7 @@ by (rule DERIV_exp [THEN DERIV_isCont]) lemma sin_zero_abs_cos_one: "sin x = 0 ==> \cos x\ = 1" -by (auto simp add: sin_zero_iff even_mult_two_ex times_divide_eq) +by (auto simp add: sin_zero_iff even_mult_two_ex) lemma exp_eq_one_iff [simp]: "(exp x = 1) = (x = 0)" apply auto @@ -2185,7 +2183,7 @@ lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r" apply (simp add: divide_inverse) apply (case_tac "r=0") -apply (auto simp add: inverse_mult_distrib mult_ac) +apply (auto simp add: mult_ac) done @@ -2456,7 +2454,7 @@ apply (rule order_less_le_trans [of _ "7/5"], simp) apply (rule_tac n = 1 in realpow_increasing) prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc) -apply (simp_all add: numeral_2_eq_2 times_divide_eq) +apply (simp_all add: numeral_2_eq_2) done lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u" diff -r d8edf54cc28c -r 333a88244569 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Integ/IntDef.thy Mon Feb 21 15:04:10 2005 +0100 @@ -559,80 +559,6 @@ by (simp add: linorder_not_less neg_def) -subsection{*Embedding of the Naturals into any @{text -comm_semiring_1_cancel}: @{term of_nat}*} - -consts of_nat :: "nat => 'a::comm_semiring_1_cancel" - -primrec - of_nat_0: "of_nat 0 = 0" - of_nat_Suc: "of_nat (Suc m) = of_nat m + 1" - -lemma of_nat_1 [simp]: "of_nat 1 = 1" -by simp - -lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n" -apply (induct m) -apply (simp_all add: add_ac) -done - -lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n" -apply (induct m) -apply (simp_all add: mult_ac add_ac right_distrib) -done - -lemma zero_le_imp_of_nat: "0 \ (of_nat m::'a::ordered_semidom)" -apply (induct m, simp_all) -apply (erule order_trans) -apply (rule less_add_one [THEN order_less_imp_le]) -done - -lemma less_imp_of_nat_less: - "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)" -apply (induct m n rule: diff_induct, simp_all) -apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force) -done - -lemma of_nat_less_imp_less: - "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n" -apply (induct m n rule: diff_induct, simp_all) -apply (insert zero_le_imp_of_nat) -apply (force simp add: linorder_not_less [symmetric]) -done - -lemma of_nat_less_iff [simp]: - "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m (of_nat n::'a::ordered_semidom)) = (m \ n)" -by (simp add: linorder_not_less [symmetric]) - -text{*Special cases where either operand is zero*} -declare of_nat_le_iff [of 0, simplified, simp] -declare of_nat_le_iff [of _ 0, simplified, simp] - -text{*The ordering on the @{text comm_semiring_1_cancel} is necessary -to exclude the possibility of a finite field, which indeed wraps back to -zero.*} -lemma of_nat_eq_iff [simp]: - "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)" -by (simp add: order_eq_iff) - -text{*Special cases where either operand is zero*} -declare of_nat_eq_iff [of 0, simplified, simp] -declare of_nat_eq_iff [of _ 0, simplified, simp] - -lemma of_nat_diff [simp]: - "n \ m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)" -by (simp del: of_nat_add - add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) - - subsection{*The Set of Natural Numbers*} constdefs diff -r d8edf54cc28c -r 333a88244569 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Nat.thy Mon Feb 21 15:04:10 2005 +0100 @@ -1022,4 +1022,5 @@ apply (fastsimp dest: mult_less_mono2) done + end diff -r d8edf54cc28c -r 333a88244569 src/HOL/NatArith.thy --- a/src/HOL/NatArith.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/NatArith.thy Mon Feb 21 15:04:10 2005 +0100 @@ -162,5 +162,78 @@ val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2"; *} +subsection{*Embedding of the Naturals into any @{text +comm_semiring_1_cancel}: @{term of_nat}*} + +consts of_nat :: "nat => 'a::comm_semiring_1_cancel" + +primrec + of_nat_0: "of_nat 0 = 0" + of_nat_Suc: "of_nat (Suc m) = of_nat m + 1" + +lemma of_nat_1 [simp]: "of_nat 1 = 1" +by simp + +lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n" +apply (induct m) +apply (simp_all add: add_ac) +done + +lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n" +apply (induct m) +apply (simp_all add: mult_ac add_ac right_distrib) +done + +lemma zero_le_imp_of_nat: "0 \ (of_nat m::'a::ordered_semidom)" +apply (induct m, simp_all) +apply (erule order_trans) +apply (rule less_add_one [THEN order_less_imp_le]) +done + +lemma less_imp_of_nat_less: + "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)" +apply (induct m n rule: diff_induct, simp_all) +apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force) +done + +lemma of_nat_less_imp_less: + "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n" +apply (induct m n rule: diff_induct, simp_all) +apply (insert zero_le_imp_of_nat) +apply (force simp add: linorder_not_less [symmetric]) +done + +lemma of_nat_less_iff [simp]: + "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m (of_nat n::'a::ordered_semidom)) = (m \ n)" +by (simp add: linorder_not_less [symmetric]) + +text{*Special cases where either operand is zero*} +declare of_nat_le_iff [of 0, simplified, simp] +declare of_nat_le_iff [of _ 0, simplified, simp] + +text{*The ordering on the @{text comm_semiring_1_cancel} is necessary +to exclude the possibility of a finite field, which indeed wraps back to +zero.*} +lemma of_nat_eq_iff [simp]: + "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)" +by (simp add: order_eq_iff) + +text{*Special cases where either operand is zero*} +declare of_nat_eq_iff [of 0, simplified, simp] +declare of_nat_eq_iff [of _ 0, simplified, simp] + +lemma of_nat_diff [simp]: + "n \ m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)" +by (simp del: of_nat_add + add: compare_rls of_nat_add [symmetric] split add: nat_diff_split) + end diff -r d8edf54cc28c -r 333a88244569 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/OrderedGroup.thy Mon Feb 21 15:04:10 2005 +0100 @@ -319,6 +319,11 @@ shows "[|0\a; b\c|] ==> b \ a + c" by (insert add_mono [of 0 a b c], simp) +lemma add_increasing2: + fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" + shows "[|0\c; b\a|] ==> b \ a + c" +by (simp add:add_increasing add_commute[of a]) + lemma add_strict_increasing: fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}" shows "[|0c|] ==> b < a + c" @@ -806,7 +811,7 @@ lemma abs_le_iff: "(abs a \ b) = (a \ b & -a \ (b::'a::lordered_ab_group_abs))" by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2) -lemma abs_triangle_ineq: "abs (a+b) \ abs a + abs (b::'a::lordered_ab_group_abs)" +lemma abs_triangle_ineq: "abs(a+b) \ abs a + abs(b::'a::lordered_ab_group_abs)" proof - have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n") apply (simp add: abs_lattice add_meet_join_distribs join_aci) @@ -829,6 +834,17 @@ finally show ?thesis . qed +lemma abs_add_abs[simp]: +fixes a:: "'a::{lordered_ab_group_abs}" +shows "abs(abs a + abs b) = abs a + abs b" (is "?L = ?R") +proof (rule order_antisym) + show "?L \ ?R" by(rule abs_ge_self) +next + have "?L \ \\a\\ + \\b\\" by(rule abs_triangle_ineq) + also have "\ = ?R" by simp + finally show "?L \ ?R" . +qed + text {* Needed for abelian cancellation simprocs: *} lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)" diff -r d8edf54cc28c -r 333a88244569 src/HOL/Real/RComplete.thy --- a/src/HOL/Real/RComplete.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/Real/RComplete.thy Mon Feb 21 15:04:10 2005 +0100 @@ -389,7 +389,7 @@ lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n" apply (rule inj_int [THEN injD]) apply (simp add: real_of_nat_Suc) -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"]) +apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"]) done lemma floor_eq4: "[| real n \ x; x < real (Suc n) |] ==> nat(floor x) = n" @@ -532,7 +532,3 @@ end - - - - diff -r d8edf54cc28c -r 333a88244569 src/HOL/SetInterval.thy --- a/src/HOL/SetInterval.thy Sat Feb 19 18:44:34 2005 +0100 +++ b/src/HOL/SetInterval.thy Mon Feb 21 15:04:10 2005 +0100 @@ -589,6 +589,22 @@ lemma Summation_Suc[simp]: "(\i < Suc n. b i) = b n + (\i < n. b i)" by (simp add:lessThan_Suc) +lemma setsum_add_nat_ivl: "\ m \ n; n \ p \ \ + setsum f {m.. 'a::ab_group_add" +shows "\ m \ n; n \ p \ \ + setsum f {m..