--- 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) \<le> sumr m n (%i. cmod(f i))"
+lemma sumc_cmod: "cmod(sumc m n f) \<le> (\<Sum>i=m..<n. cmod(f i))"
apply (induct "n")
apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
done
@@ -147,11 +147,11 @@
qed_spec_mp "sumc_ge_zero2";
***)
-lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
-by (induct "n", auto simp add: add_increasing)
+lemma sumr_cmod_ge_zero [iff]: "0 \<le> (\<Sum>n=m..<n::nat. cmod (f n))"
+by (induct "n", auto simp add: add_increasing)
lemma rabs_sumc_cmod_cancel [simp]:
- "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
+ "abs (\<Sum>n=m..<n::nat. cmod (f n)) = (\<Sum>n=m..<n. cmod (f n))"
by (simp add: abs_if linorder_not_less)
lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
--- a/src/HOL/Equiv_Relations.thy Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Equiv_Relations.thy Mon Feb 21 15:04:10 2005 +0100
@@ -327,7 +327,7 @@
apply assumption
apply simp
apply(fastsimp simp add:inj_on_def)
-apply (simp add:setsum_constant_nat)
+apply (simp add:setsum_constant)
done
ML
--- a/src/HOL/Finite_Set.thy Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Finite_Set.thy Mon Feb 21 15:04:10 2005 +0100
@@ -1064,17 +1064,6 @@
by (simp add: setsum_def)
qed
-lemma setsum_mono2_nat:
- assumes fin: "finite B" and sub: "A \<subseteq> B"
-shows "setsum f A \<le> (setsum f B :: nat)"
-proof -
- have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
- also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
- by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
- also have "A \<union> (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 \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
+assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
+shows "setsum f A \<le> setsum f B"
+proof -
+ have "setsum f A \<le> setsum f A + setsum f (B-A)"
+ by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
+ also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
+ by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
+ also have "A \<union> (B-A) = B" using sub by blast
+ finally show ?thesis .
+qed
+(*
+lemma setsum_mono2_nat:
+ assumes fin: "finite B" and sub: "A \<subseteq> B"
+shows "setsum f A \<le> (setsum f B :: nat)"
+proof -
+ have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
+ also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
+ by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
+ also have "A \<union> (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 (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>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 "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
+ also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>" using insert by simp
+ also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
+ also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" 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: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> 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: "(\<Sum>x\<in>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]: "(\<Sum>x \<in> 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 ==> (\<Prod>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 \<noteq> j --> A i Int A j = {}) ==>
card (UNION I A) = (\<Sum>i\<in>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 \<subseteq> A ==> inj_on f A ==> f ` A = A"
by (simp add: card_seteq card_image)
@@ -1587,18 +1623,17 @@
lemma card_SigmaI [simp]:
"\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
\<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>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)
--- 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(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).
- hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"
+ hyprel ``{%n::nat. setsum f {X n..<Y n}})) p"
NSsums :: "[nat=>real,real] => bool" (infixr "NSsums" 80)
- "f NSsums s == (%n. sumr 0 n f) ----NS> s"
+ "f NSsums s == (%n. setsum f {0..<n}) ----NS> s"
NSsummable :: "(nat=>real) => bool"
"NSsummable f == (\<exists>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..<N n}})"
apply (simp add: sumhr_def)
-apply (rule arg_cong [where f = Abs_hypreal])
+apply (rule arg_cong [where f = Abs_hypreal])
apply (auto, ultra)
done
@@ -84,7 +84,7 @@
lemma sumhr_split_add: "n < p ==> 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<p ==> 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 \<Longrightarrow> j = n \<Longrightarrow> (!!x. m <= x \<Longrightarrow> x < n \<Longrightarrow> f x = g x) \<Longrightarrow>
+ setsum f {i..<j} = setsum g {m..<n}"
+by(rule setsum_cong, simp_all)
+
lemma sumhr_interval_const:
"(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> 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..<n})) N = sumhr(0,N,f)"
apply (cases N)
apply (simp add: hypnat_zero_def starfunNat sumhr)
done
@@ -192,7 +197,8 @@
lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
-lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"
+lemma NSseries_zero:
+ "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
by (simp add: sums_NSsums_iff [symmetric] series_zero)
lemma NSsummable_NSCauchy:
--- a/src/HOL/Hyperreal/HTranscendental.thy Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy Mon Feb 21 15:04:10 2005 +0100
@@ -56,7 +56,6 @@
lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> 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
--- 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\<notin> FreeUltrafilterNat ==> -X \<in> 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) \<in> FreeUltrafilterNat"
+lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
-lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat"
-by auto
-
lemma FreeUltrafilterNat_Nat_set_refl [intro]:
"{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
by simp
@@ -200,7 +197,7 @@
by (rule ccontr, simp)
lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> 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 \<noteq> y"
-by (auto simp add: order_less_irrefl)
+by (auto)
lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> 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";
--- 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) \<le> 2 ^ n"
by (insert power_increasing [of 0 n "2::hypreal"], simp)
--- 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. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n))"
--{*Gauge integrability (definite)*}
@@ -331,7 +331,7 @@
done
lemma sumr_partition_eq_diff_bounds [simp]:
- "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
+ "(\<Sum>n=0..<m. D (Suc n) - D n::real) = D(m) - D 0"
by (induct "m", auto)
lemma Integral_eq_diff_bounds: "a \<le> 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 "(\<Sum>n=0..<psize D. f(D(Suc n)) - f(D n)) = f b - f a")
prefer 2
apply (cut_tac D = "%n. f (D n)" and m = "psize D"
in sumr_partition_eq_diff_bounds)
@@ -461,10 +461,10 @@
apply (drule sym, simp)
apply (simp (no_asm) add: setsum_subtractf[symmetric])
apply (rule setsum_abs [THEN order_trans])
-apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
+apply (subgoal_tac "ea = (\<Sum>n=0..<psize D. (ea / (b - a)) * (D (Suc n) - (D n)))")
apply (simp add: abs_minus_commute)
apply (rule_tac t = ea in ssubst, assumption)
-apply (rule sumr_le2)
+apply (rule setsum_mono)
apply (rule_tac [2] setsum_mult [THEN subst])
apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
fine_def)
@@ -812,7 +812,7 @@
tpart(a,b) (D,p)
|] ==> rsum(D,p) f \<le> 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
--- 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 \<noteq> (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 "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
proof (intro exI conjI)
let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
- show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp add: times_divide_eq)
+ show "\<forall>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 @@
\<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> 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 \<noteq> 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 \<noteq> b; \<forall>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*}
--- 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:
+ "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
by (induct "n", auto)
-lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
+lemma sumr_offset2:
+ "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
by (induct "n", auto)
-lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
+lemma sumr_offset3:
+ "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
by (simp add: sumr_offset)
-lemma sumr_offset4: "\<forall>n f. sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
+lemma sumr_offset4:
+ "\<forall>n f. setsum f {0::nat..<n+k} =
+ (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
by (simp add: sumr_offset)
+(*
lemma sumr_from_1_from_0: "0 < n ==>
- 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)"
+ (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
+ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
+ (\<Sum>n=0..<Suc n. if even(n) then 0 else
+ ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
-
+*)
subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
@@ -36,12 +43,12 @@
lemma Maclaurin_lemma:
"0 < h ==>
- \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
+ \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
(B * ((h^n) / real(fact n)))"
-apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
+apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
real(fact n) / (h^n)"
in exI)
-apply (simp add: times_divide_eq)
+apply (simp)
done
lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
@@ -92,9 +99,9 @@
prefer 3 apply (simp add: fact_diff_Suc)
prefer 2 apply simp
apply (frule_tac m = m 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 (rule lemma_DERIV_subst)
apply (rule DERIV_add)
apply (rule_tac [2] DERIV_const)
@@ -106,7 +113,7 @@
apply (best intro: DERIV_chain2 intro!: DERIV_intros)
apply (subst fact_Suc)
apply (subst real_of_nat_mult)
-apply (simp add: inverse_mult_distrib mult_ac)
+apply (simp add: mult_ac)
done
@@ -137,7 +144,7 @@
==> \<exists>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..<n} +
(diff n t / real (fact n)) * h ^ n"
apply (case_tac "n = 0", force)
apply (drule not0_implies_Suc)
@@ -145,15 +152,15 @@
apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
apply (erule exE)
apply (subgoal_tac "\<exists>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..<n} + (B * (t^n / real(fact n)))))")
prefer 2 apply blast
apply (erule exE)
apply (subgoal_tac "g 0 = 0 & g h =0")
prefer 2
- apply (simp del: sumr_Suc)
+ apply (simp del: setsum_Suc)
apply (cut_tac n = m and k = 1 in sumr_offset2)
- apply (simp add: eq_diff_eq' del: sumr_Suc)
-apply (subgoal_tac "\<exists>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 "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
prefer 2 apply blast
apply (erule exE)
apply (subgoal_tac "difg 0 = g")
@@ -165,15 +172,15 @@
apply (simp (no_asm_simp))
apply (erule exE)
apply (rule_tac x = t in exI)
- apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
+ apply (simp del: realpow_Suc fact_Suc)
apply (subgoal_tac "\<forall>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 "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
apply (rule allI, rule impI)
apply (drule_tac x = ma and P="%m. m<n --> (\<exists>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..<n-m} + B * (t ^ (n - m) / real (fact (n - m)))))"
in thin_rl)
-apply (erule_tac [!] V="g = (%t. f t - (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + B * (t ^ n / real (fact n))))"
+apply (erule_tac [!] V="g = (%t. f t - (setsum (%m. diff m 0 / real (fact m) * t ^ m) {0..<n} + B * (t ^ n / real (fact n))))"
in thin_rl)
-apply (erule_tac [!] V="f h = sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + B * (h ^ n / real (fact n))"
+apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))"
in thin_rl)
(* back to business *)
apply (simp (no_asm_simp))
@@ -215,7 +222,7 @@
--> (\<exists>t. 0 < t &
t < h &
f h =
- sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n)"
by (blast intro: Maclaurin)
@@ -227,7 +234,7 @@
==> \<exists>t. 0 < t &
t \<le> h &
f h =
- sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n"
apply (case_tac "n", auto)
apply (drule Maclaurin, auto)
@@ -240,7 +247,7 @@
--> (\<exists>t. 0 < t &
t \<le> h &
f h =
- sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n)"
by (blast intro: Maclaurin2)
@@ -250,12 +257,12 @@
==> \<exists>t. h < t &
t < 0 &
f h =
- sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n"
apply (cut_tac f = "%x. f (-x)"
and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
and h = "-h" and n = n in Maclaurin_objl)
-apply (simp add: times_divide_eq)
+apply (simp)
apply safe
apply (subst minus_mult_right)
apply (rule DERIV_cmult)
@@ -278,7 +285,7 @@
--> (\<exists>t. h < t &
t < 0 &
f h =
- sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
diff n t / real (fact n) * h ^ n)"
by (blast intro: Maclaurin_minus)
@@ -299,12 +306,12 @@
\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
==> \<exists>t. abs t \<le> abs x &
f x =
- sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) +
+ (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
diff n t / real (fact n) * x ^ n"
apply (case_tac "n = 0", force)
apply (case_tac "x = 0")
apply (rule_tac x = 0 in exI)
-apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
+apply (force simp add: Maclaurin_bi_le_lemma)
apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
txt{*Case 1, where @{term "x < 0"}*}
apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
@@ -323,7 +330,7 @@
\<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
x ~= 0; 0 < n
|] ==> \<exists>t. 0 < abs t & abs t < abs x &
- f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+ f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n"
apply (rule_tac x = x and y = 0 in linorder_cases)
prefer 2 apply blast
@@ -337,21 +344,21 @@
(\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
x ~= 0 & 0 < n
--> (\<exists>t. 0 < abs t & abs t < abs x &
- f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+ f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n)"
by (blast intro: Maclaurin_all_lt)
lemma Maclaurin_zero [rule_format]:
"x = (0::real)
==> 0 < n -->
- sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) =
+ (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
diff 0 0"
by (induct n, auto)
lemma Maclaurin_all_le: "[| diff 0 = f;
\<forall>m x. DERIV (diff m) x :> diff (Suc m) x
|] ==> \<exists>t. abs t \<le> abs x &
- f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+ f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n"
apply (insert linorder_le_less_linear [of n 0])
apply (erule disjE, force)
@@ -366,7 +373,7 @@
lemma Maclaurin_all_le_objl: "diff 0 = f &
(\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
--> (\<exists>t. abs t \<le> abs x &
- f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+ f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
(diff n t / real (fact n)) * x ^ n)"
by (blast intro: Maclaurin_all_le)
@@ -376,14 +383,14 @@
lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
==> (\<exists>t. 0 < abs t &
abs t < abs x &
- exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
+ exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
(exp t / real (fact n)) * x ^ n)"
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
lemma Maclaurin_exp_le:
"\<exists>t. abs t \<le> abs x &
- exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
+ exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
(exp t / real (fact n)) * x ^ n"
by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
@@ -421,29 +428,29 @@
lemma Maclaurin_sin_expansion2:
"\<exists>t. abs t \<le> abs x &
sin x =
- (sumr 0 n (%m. (if even m then 0
+ (\<Sum>m=0..<n. (if even m then 0
else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
- x ^ m))
+ x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and x = x
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
apply (case_tac "n", clarify, simp, simp)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
done
lemma Maclaurin_sin_expansion:
"\<exists>t. sin x =
- (sumr 0 n (%m. (if even m then 0
+ (\<Sum>m=0..<n. (if even m then 0
else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
- x ^ m))
+ x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (insert Maclaurin_sin_expansion2 [of x n])
apply (blast intro: elim:);
@@ -455,63 +462,60 @@
"[| 0 < n; 0 < x |] ==>
\<exists>t. 0 < t & t < x &
sin x =
- (sumr 0 n (%m. (if even m then 0
+ (\<Sum>m=0..<n. (if even m then 0
else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
- x ^ m))
+ x ^ m)
+ ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
done
lemma Maclaurin_sin_expansion4:
"0 < x ==>
\<exists>t. 0 < t & t \<le> x &
sin x =
- (sumr 0 n (%m. (if even m then 0
+ (\<Sum>m=0..<n. (if even m then 0
else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
- x ^ m))
+ x ^ m)
+ ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
done
subsection{*Maclaurin Expansion for Cosine Function*}
lemma sumr_cos_zero_one [simp]:
- "sumr 0 (Suc n)
- (%m. (if even m
- then (- 1) ^ (m div 2)/(real (fact m))
- else 0) *
- 0 ^ m) = 1"
+ "(\<Sum>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:
"\<exists>t. abs t \<le> abs x &
cos x =
- (sumr 0 n (%m. (if even m
+ (\<Sum>m=0..<n. (if even m
then (- 1) ^ (m div 2)/(real (fact m))
else 0) *
- x ^ m))
+ x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
apply (simp (no_asm))
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
apply (case_tac "n", simp)
-apply (simp del: sumr_Suc)
+apply (simp del: setsum_Suc)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
@@ -524,15 +528,15 @@
"[| 0 < x; 0 < n |] ==>
\<exists>t. 0 < t & t < x &
cos x =
- (sumr 0 n (%m. (if even m
+ (\<Sum>m=0..<n. (if even m
then (- 1) ^ (m div 2)/(real (fact m))
else 0) *
- x ^ m))
+ x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -543,15 +547,15 @@
"[| x < 0; 0 < n |] ==>
\<exists>t. x < t & t < 0 &
cos x =
- (sumr 0 n (%m. (if even m
+ (\<Sum>m=0..<n. (if even m
then (- 1) ^ (m div 2)/(real (fact m))
else 0) *
- x ^ m))
+ x ^ m)
+ ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum_cong[OF refl])
@@ -567,7 +571,7 @@
by auto
lemma Maclaurin_sin_bound:
- "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+ "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
x ^ m)) \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
proof -
have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
--- 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) \<in> Reals; y \<in> Reals |] ==> x * y \<in> 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) \<in> Reals ==> inverse x \<in> 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 \<in> 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 \<in> 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 \<in> 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 \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
@@ -1077,7 +1077,7 @@
isLub Reals {s. s \<in> Reals & s < x} t;
r \<in> Reals; 0 < r |]
==> -(x + -t) \<noteq> 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\<notin> HFinite ==> x \<in> 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 \<in> HInfinite | x \<in> 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) \<in> \<real>"
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)
--- 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
--- 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. \<bar>Y n\<bar> < 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*}
--- 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 == (\<exists>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..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
by (simp add: atLeastLessThanSuc add_commute)
@@ -45,7 +43,6 @@
apply (rename_tac k)
apply (subgoal_tac "n=k", auto)
done
-*)
lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
@@ -58,8 +55,10 @@
using sumr_split_add [of m n p f,symmetric]
apply (simp add: add_ac)
done
+*)
-lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
+lemma sumr_diff_mult_const:
+ "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
by (simp add: diff_minus setsum_addf real_of_nat_def)
(*
@@ -79,32 +78,54 @@
lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
by (simp add: Finite_Set.setsum_negf)
+
+lemma sumr_shift_bounds:
+ "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
+by (induct "n", auto)
*)
-lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
+(* Generalize from real to some algebraic structure? *)
+lemma sumr_minus_one_realpow_zero [simp]:
+ "setsum (%i. (-1) ^ Suc i) {0..<2*n} = (0::real)"
by (induct "n", auto)
-lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
-by (induct "n", auto)
-
-lemma sumr_interval_const:
- "\<lbrakk>\<forall>n. m \<le> Suc n --> f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(k-m) * r)"
-apply (induct "k", auto)
+(*
+lemma sumr_interval_const2:
+ "[|\<forall>n\<ge>m. f n = r; m \<le> 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:
+ "(\<And>n. n\<in>A \<Longrightarrow> f n = r) \<Longrightarrow> 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:
- "[|\<forall>n\<ge>m. f n = r; m \<le> 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:
+ "[|\<forall>n\<ge>m. 0 \<le> (f n::real); m < k|] ==> setsum f {0..<m} \<le> setsum f {0..<k::nat}"
+apply (induct "k")
+apply (auto simp add: less_Suc_eq_le)
+apply (drule_tac x = k in spec, safe)
+apply (drule le_imp_less_or_eq, safe)
+apply (arith)
+apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
done
-
lemma sumr_le:
"[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> 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: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> 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]:
"\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
by (induct "n", auto)
+*)
lemma Suc_le_imp_diff_ge2:
- "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
-apply (rule sumr_zero)
+ "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> setsum f {m..<n} = 0"
+apply (rule setsum_0')
apply (case_tac "n", auto)
+apply(erule_tac x = "a - 1" in allE)
+apply (simp split:nat_diff_split)
done
-lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"
+(* FIXME this is an awful lemma! *)
+lemma sumr_one_lb_realpow_zero [simp]:
+ "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
apply (induct "n")
apply (case_tac [2] "n", auto)
done
@@ -149,30 +178,46 @@
lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
by (simp add: diff_minus setsum_addf setsum_negf)
*)
+(*
lemma sumr_subst [rule_format (no_asm)]:
"(\<forall>p. m \<le> 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: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
+ shows "setsum f A \<le> 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)]:
"(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))
- --> (sumr m (m + n) f \<le> (real n * K))"
+ --> setsum f {m..<m+n::nat} \<le> (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)]:
"(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))
- --> (sumr 0 n f \<le> (real n * K))"
+ --> setsum f {0..<n::nat} \<le> (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)
+ "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
+apply (subgoal_tac "k = 0 | 0 < k", auto simp:setsum_0')
apply (induct "n")
-apply (simp_all add: sumr_split_add add_commute)
+apply (simp_all add: setsum_add_nat_ivl add_commute)
done
+(* FIXME setsum_0[simp] *)
+
subsection{* Infinite Sums, by the Properties of Limits*}
@@ -188,7 +233,7 @@
done
lemma summable_sumr_LIMSEQ_suminf:
- "summable f ==> (%n. sumr 0 n f) ----> (suminf f)"
+ "summable f ==> (%n. setsum f {0..<n}) ----> (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..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (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 \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
+by(auto)
+
+
+(* FIXME the last step should work w/o Ball_def, ideally just with
+ setsum_0 and setsum_cong. Currently the simplifier does not simplify
+ the premise x:{i..<j} that ball_cong (or a modified version of setsum_0')
+ generates. FIX simplifier??? *)
lemma series_zero:
- "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (sumr 0 n f)"
+ "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
apply (rule_tac x = n in exI)
-apply (clarsimp simp:sumr_split_add_minus)
-apply (drule sumr_interval_const2, auto)
+apply (clarsimp simp add:setsum_diff[symmetric] setsum_0' Ball_def)
done
+
lemma sums_mult: "x sums x0 ==> (%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..<n*k+k}) sums (suminf f)"
apply (drule summable_sums)
apply (auto simp add: sums_def LIMSEQ_def)
apply (drule_tac x = r in spec, safe)
@@ -260,18 +322,18 @@
done
lemma sumr_pos_lt_pair_lemma:
- "[|\<forall>d. - f (n + (d + d)) < f (Suc (n + (d + d)))|]
- ==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f"
+ "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |]
+ ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}"
apply (induct "no", auto)
apply (drule_tac x = "Suc no" in spec)
-apply (simp add: add_ac)
+apply (simp add: add_ac)
done
lemma sumr_pos_lt_pair:
"[|summable f;
\<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]
- ==> sumr 0 n f < suminf f"
+ ==> setsum f {0..<n} < suminf f"
apply (drule summable_sums)
apply (auto simp add: sums_def LIMSEQ_def)
apply (drule_tac x = "f (n) + f (n + 1)" in spec)
@@ -282,18 +344,19 @@
apply (drule_tac x = 0 in spec, simp)
apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
apply (safe, simp)
-apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> 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)) \<le>
+ setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
+apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
prefer 3 apply assumption
-apply (rule_tac [2] y = "sumr 0 n f + (f (n) + f (n + 1))" in order_trans)
+apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
apply simp_all
-apply (subgoal_tac "suminf f \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
+apply (subgoal_tac "suminf f \<le> 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 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f")
-apply (simp add: abs_if)
+apply (subgoal_tac "0 \<le> 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; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
+ "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> 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..<n}" in LIMSEQ_const)
+apply (erule LIMSEQ_le, blast)
+apply (rule_tac x = n in exI, clarify)
+apply (rule setsum_mono2)
+apply auto
done
lemma series_pos_less:
- "[| summable f; \<forall>m \<ge> 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; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
+apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
apply (rule_tac [2] series_pos_le, auto)
apply (drule_tac x = m in spec, auto)
done
text{*Sum of a geometric progression.*}
-lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
+lemma sumr_geometric:
+ "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)"
apply (induct "n", auto)
apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
-apply (auto simp add: mult_assoc left_distrib times_divide_eq)
+apply (auto simp add: mult_assoc left_distrib)
apply (simp add: right_distrib diff_minus mult_commute)
done
@@ -339,25 +403,27 @@
text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
-lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
+lemma summable_convergent_sumr_iff:
+ "summable f = convergent (%n. setsum f {0..<n})"
by (simp add: summable_def sums_def convergent_def)
lemma summable_Cauchy:
"summable f =
- (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
+ (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric])
-apply (drule_tac [!] spec, auto)
+apply (drule_tac [!] spec, auto)
apply (rule_tac x = M in exI)
apply (rule_tac [2] x = N in exI, auto)
apply (cut_tac [!] m = m and n = n in less_linear, auto)
apply (frule le_less_trans [THEN less_imp_le], assumption)
apply (drule_tac x = n in spec, simp)
apply (drule_tac x = m in spec)
-apply(simp add: sumr_split_add_minus)
+apply(simp add: setsum_diff[symmetric])
apply(subst abs_minus_commute)
-apply(simp add: sumr_split_add_minus)
-apply (simp add: sumr_split_add_minus)
+apply(simp add: setsum_diff[symmetric])
+apply(simp add: setsum_diff[symmetric])
done
+(* FIXME move ivl_ lemmas out of this theory *)
text{*Comparison test*}
@@ -369,10 +435,10 @@
apply (rotate_tac 2)
apply (drule_tac x = m in spec)
apply (auto, rotate_tac 2, drule_tac x = n in spec)
-apply (rule_tac y = "sumr m n (%k. abs (f k))" in order_le_less_trans)
+apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans)
apply (rule setsum_abs)
-apply (rule_tac y = "sumr m n g" in order_le_less_trans)
-apply (auto intro: sumr_le2 simp add: abs_interval_iff)
+apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
+apply (auto intro: setsum_mono simp add: abs_interval_iff)
done
lemma summable_rabs_comparison_test:
@@ -389,7 +455,7 @@
apply (drule summable_sums)+
apply (auto intro!: LIMSEQ_le simp add: sums_def)
apply (rule exI)
-apply (auto intro!: sumr_le2)
+apply (auto intro!: setsum_mono)
done
lemma summable_le2:
@@ -405,7 +471,7 @@
apply (drule spec, auto)
apply (rule_tac x = N in exI, auto)
apply (drule spec, auto)
-apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
+apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
apply (auto)
done
@@ -452,7 +518,7 @@
apply (rule_tac x = N in exI, safe)
apply (drule le_Suc_ex_iff [THEN iffD1])
apply (auto simp add: power_add realpow_not_zero)
-apply (induct_tac "na", auto simp add: times_divide_eq)
+apply (induct_tac "na", auto)
apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
apply (auto intro: mult_right_mono simp add: summable_def)
apply (simp add: mult_ac)
@@ -467,28 +533,20 @@
lemma DERIV_sumr [rule_format (no_asm)]:
"(\<forall>r. m \<le> 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. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
apply (induct "n")
apply (auto intro: DERIV_add)
done
ML
{*
-val sumr_Suc = thm"sumr_Suc";
val sums_def = thm"sums_def";
val summable_def = thm"summable_def";
val suminf_def = thm"suminf_def";
-val sumr_split_add = thm "sumr_split_add";
val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
-val sumr_le2 = thm "sumr_le2";
-val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
-val sumr_zero = thm "sumr_zero";
val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
-val sumr_subst = thm "sumr_subst";
-val sumr_bound = thm "sumr_bound";
-val sumr_bound2 = thm "sumr_bound2";
val sumr_group = thm "sumr_group";
val sums_summable = thm "sums_summable";
val summable_sums = thm "summable_sums";
--- a/src/HOL/Hyperreal/Transcendental.thy Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy Mon Feb 21 15:04:10 2005 +0100
@@ -75,7 +75,7 @@
apply (rule_tac x = u and y = x in linorder_cases)
apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less])
apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less])
-apply (auto simp add: order_less_irrefl)
+apply (auto)
done
lemma real_root_pos2: "0 \<le> 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)\<twosuperior> = x) = (0 \<le> x)"
+lemma real_sqrt_pow2_iff [iff]: "((sqrt x)\<twosuperior> = x) = (0 \<le> 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 \<le> x ==> (sqrt x)\<twosuperior> = x"
-by (simp add: real_sqrt_pow2_iff)
+by (simp)
lemma real_sqrt_abs_abs [simp]: "sqrt\<bar>x\<bar> ^ 2 = \<bar>x\<bar>"
by (rule real_sqrt_pow2_iff [THEN iffD2], arith)
@@ -209,13 +209,13 @@
lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
"sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
-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\<twosuperior>) = \<bar>x\<bar>"
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) = \<bar>x\<bar>"
@@ -229,7 +229,7 @@
lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 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 = "\<bar>x\<bar>" 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 = "\<bar>x\<bar>" 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"
+ "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) * 0 ^ n
+ else 0) = 0"
apply (induct "n")
apply (case_tac [2] "n", auto)
done
@@ -364,34 +361,33 @@
subsection{*Properties of Power Series*}
lemma lemma_realpow_diff_sumr:
- "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =
- y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
-apply (auto simp add: setsum_mult simp del: sumr_Suc)
-apply (rule sumr_subst)
-apply (intro strip)
+ "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =
+ y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
+apply (auto simp add: setsum_mult simp del: setsum_Suc)
+apply (rule setsum_cong[OF refl])
apply (subst lemma_realpow_diff)
apply (auto simp add: mult_ac)
done
lemma lemma_realpow_diff_sumr2:
"x ^ (Suc n) - y ^ (Suc n) =
- (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
+ (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
apply (induct "n", simp)
-apply (auto simp del: sumr_Suc)
-apply (subst sumr_Suc)
+apply (auto simp del: setsum_Suc)
+apply (subst setsum_Suc)
apply (drule sym)
-apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc)
+apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_Suc)
done
lemma lemma_realpow_rev_sumr:
- "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =
- sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"
+ "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
+ (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
apply (case_tac "x = y")
-apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc)
+apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_Suc)
apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
apply (rule_tac [2] minus_minus [THEN subst], simp)
apply (subst minus_mult_left)
-apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: sumr_Suc)
+apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_Suc)
done
text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
@@ -412,7 +408,7 @@
apply (auto simp add: mult_assoc power_abs)
prefer 2
apply (drule_tac x = 0 in spec, force)
-apply (auto simp add: abs_mult power_abs mult_ac)
+apply (auto simp add: power_abs mult_ac)
apply (rule_tac a2 = "z ^ n"
in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
@@ -423,8 +419,7 @@
apply (subgoal_tac "x \<noteq> 0")
apply (subgoal_tac [3] "x \<noteq> 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))) +
+ "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) =
+ (\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) +
(real n * c(n) * x ^ (n - Suc 0))"
apply (induct "n")
apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
done
lemma lemma_diffs2:
- "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =
- sumr 0 n (%n. (diffs c)(n) * (x ^ n)) -
+ "(\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) =
+ (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) -
(real n * c(n) * x ^ (n - Suc 0))"
by (auto simp add: lemma_diffs)
@@ -474,10 +469,9 @@
subsection{*Term-by-Term Differentiability of Power Series*}
lemma lemma_termdiff1:
- "sumr 0 m (%p. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
- sumr 0 m (%p. (z ^ p) *
- (((z + h) ^ (m - p)) - (z ^ (m - p))))"
-apply (rule sumr_subst)
+ "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =
+ (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
+apply (rule setsum_cong[OF refl])
apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac)
done
@@ -489,54 +483,59 @@
lemma lemma_termdiff2:
- " h \<noteq> 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 \<noteq> 0 ==>
+ (((z + h) ^ n) - (z ^ n)) * inverse h - real n * (z ^ (n - Suc 0)) =
+ h * (\<Sum>p=0..< n - Suc 0. (z ^ p) *
+ (\<Sum>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)]:
+ "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))
+ --> setsum f {0..<n::nat} \<le> (real n * K)"
+using setsum_bounded[where A = "{0..<n}"]
+by (auto simp:real_of_nat_def)
+
lemma lemma_termdiff3:
"[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]
==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))
\<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
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 \<le> 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: "(\<forall>m. n \<le> m --> f m = 0) --> f sums sumr 0 n f"
+lemma lemma_series_zero2:
+ "(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"
by (auto intro: series_zero)
lemma cos_zero [simp]: "cos 0 = 1"
@@ -1237,7 +1237,6 @@
DERIV_add DERIV_diff DERIV_mult DERIV_minus
DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
- DERIV_Id DERIV_const DERIV_cos
(* lemma *)
lemma lemma_DERIV_sin_cos_add:
@@ -1361,9 +1360,8 @@
apply (case_tac "m=0")
apply (simp (no_asm_simp))
apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x")
-apply (simp only: mult_less_cancel_left, simp add: times_divide_eq)
-apply (simp (no_asm_simp) add: times_divide_eq
- numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
+apply (simp only: mult_less_cancel_left, simp)
+apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
apply (subgoal_tac "x*x < 2*3", simp)
apply (rule mult_strict_mono)
apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
@@ -1375,7 +1373,7 @@
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse inverse_mult_distrib del: fact_Suc)
+apply (simp (no_asm) add: divide_inverse del: fact_Suc)
apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right)
apply (auto simp add: mult_assoc simp del: fact_Suc)
@@ -1422,12 +1420,12 @@
apply (cut_tac x = 2 in cos_paired)
apply (drule sums_minus)
apply (rule neg_less_iff_less [THEN iffD1])
-apply (frule sums_unique, auto simp add: times_divide_eq)
-apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0)))
- (%n. - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n)))"
+apply (frule sums_unique, auto)
+apply (rule_tac y =
+ "\<Sum>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 ==> \<bar>cos x\<bar> = 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"
--- 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 \<le> (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<n)"
-by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
-
-text{*Special cases where either operand is zero*}
-declare of_nat_less_iff [of 0, simplified, simp]
-declare of_nat_less_iff [of _ 0, simplified, simp]
-
-lemma of_nat_le_iff [simp]:
- "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> 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 \<le> 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
--- 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
--- 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 \<le> (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<n)"
+by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
+
+text{*Special cases where either operand is zero*}
+declare of_nat_less_iff [of 0, simplified, simp]
+declare of_nat_less_iff [of _ 0, simplified, simp]
+
+lemma of_nat_le_iff [simp]:
+ "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> 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 \<le> 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
--- 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\<le>a; b\<le>c|] ==> b \<le> 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\<le>c; b\<le>a|] ==> b \<le> 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 "[|0<a; b\<le>c|] ==> b < a + c"
@@ -806,7 +811,7 @@
lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (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) \<le> abs a + abs (b::'a::lordered_ab_group_abs)"
+lemma abs_triangle_ineq: "abs(a+b) \<le> 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 \<ge> ?R" by(rule abs_ge_self)
+next
+ have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
+ also have "\<dots> = ?R" by simp
+ finally show "?L \<le> ?R" .
+qed
+
text {* Needed for abelian cancellation simprocs: *}
lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
--- 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 \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
@@ -532,7 +532,3 @@
end
-
-
-
-
--- 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]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
by (simp add:lessThan_Suc)
+lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+ setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
+by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
+
+lemma setsum_diff_nat_ivl:
+fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+ setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
+using setsum_add_nat_ivl [of m n p f,symmetric]
+apply (simp add: add_ac)
+done
+
+lemma setsum_shift_bounds_nat_ivl:
+ "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
+by (induct "n", auto simp:atLeastLessThanSuc)
+
ML
{*