comprehensive cleanup, replacing sumr by setsum
authornipkow
Mon Feb 21 15:04:10 2005 +0100 (2005-02-21)
changeset 15539333a88244569
parent 15538 d8edf54cc28c
child 15540 fa23e0561426
comprehensive cleanup, replacing sumr by setsum
src/HOL/Complex/CSeries.thy
src/HOL/Equiv_Relations.thy
src/HOL/Finite_Set.thy
src/HOL/Hyperreal/HSeries.thy
src/HOL/Hyperreal/HTranscendental.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/Lim.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Series.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Integ/IntDef.thy
src/HOL/Nat.thy
src/HOL/NatArith.thy
src/HOL/OrderedGroup.thy
src/HOL/Real/RComplete.thy
src/HOL/SetInterval.thy
     1.1 --- a/src/HOL/Complex/CSeries.thy	Sat Feb 19 18:44:34 2005 +0100
     1.2 +++ b/src/HOL/Complex/CSeries.thy	Mon Feb 21 15:04:10 2005 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4  apply (simp add: add_ac)
     1.5  done
     1.6  
     1.7 -lemma sumc_cmod: "cmod(sumc m n f) \<le> sumr m n (%i. cmod(f i))"
     1.8 +lemma sumc_cmod: "cmod(sumc m n f) \<le> (\<Sum>i=m..<n. cmod(f i))"
     1.9  apply (induct "n")
    1.10  apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
    1.11  done
    1.12 @@ -147,11 +147,11 @@
    1.13  qed_spec_mp "sumc_ge_zero2";
    1.14  ***)
    1.15  
    1.16 -lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
    1.17 -by (induct "n", auto simp add: add_increasing) 
    1.18 +lemma sumr_cmod_ge_zero [iff]: "0 \<le> (\<Sum>n=m..<n::nat. cmod (f n))"
    1.19 +by (induct "n", auto simp add: add_increasing)
    1.20  
    1.21  lemma rabs_sumc_cmod_cancel [simp]:
    1.22 -     "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
    1.23 +     "abs (\<Sum>n=m..<n::nat. cmod (f n)) = (\<Sum>n=m..<n. cmod (f n))"
    1.24  by (simp add: abs_if linorder_not_less)
    1.25  
    1.26  lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
     2.1 --- a/src/HOL/Equiv_Relations.thy	Sat Feb 19 18:44:34 2005 +0100
     2.2 +++ b/src/HOL/Equiv_Relations.thy	Mon Feb 21 15:04:10 2005 +0100
     2.3 @@ -327,7 +327,7 @@
     2.4     apply assumption
     2.5    apply simp
     2.6   apply(fastsimp simp add:inj_on_def)
     2.7 -apply (simp add:setsum_constant_nat)
     2.8 +apply (simp add:setsum_constant)
     2.9  done
    2.10  
    2.11  ML
     3.1 --- a/src/HOL/Finite_Set.thy	Sat Feb 19 18:44:34 2005 +0100
     3.2 +++ b/src/HOL/Finite_Set.thy	Mon Feb 21 15:04:10 2005 +0100
     3.3 @@ -1064,17 +1064,6 @@
     3.4      by (simp add: setsum_def)
     3.5  qed
     3.6  
     3.7 -lemma setsum_mono2_nat:
     3.8 -  assumes fin: "finite B" and sub: "A \<subseteq> B"
     3.9 -shows "setsum f A \<le> (setsum f B :: nat)"
    3.10 -proof -
    3.11 -  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
    3.12 -  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
    3.13 -    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
    3.14 -  also have "A \<union> (B-A) = B" using sub by blast
    3.15 -  finally show ?thesis .
    3.16 -qed
    3.17 -
    3.18  lemma setsum_negf:
    3.19   "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
    3.20  proof (cases "finite A")
    3.21 @@ -1118,6 +1107,30 @@
    3.22    case False thus ?thesis by (simp add: setsum_def)
    3.23  qed
    3.24  
    3.25 +lemma setsum_mono2:
    3.26 +fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
    3.27 +assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
    3.28 +shows "setsum f A \<le> setsum f B"
    3.29 +proof -
    3.30 +  have "setsum f A \<le> setsum f A + setsum f (B-A)"
    3.31 +    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
    3.32 +  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
    3.33 +    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
    3.34 +  also have "A \<union> (B-A) = B" using sub by blast
    3.35 +  finally show ?thesis .
    3.36 +qed
    3.37 +(*
    3.38 +lemma setsum_mono2_nat:
    3.39 +  assumes fin: "finite B" and sub: "A \<subseteq> B"
    3.40 +shows "setsum f A \<le> (setsum f B :: nat)"
    3.41 +proof -
    3.42 +  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
    3.43 +  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
    3.44 +    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
    3.45 +  also have "A \<union> (B-A) = B" using sub by blast
    3.46 +  finally show ?thesis .
    3.47 +qed
    3.48 +*)
    3.49  lemma setsum_mult: 
    3.50    fixes f :: "'a => ('b::semiring_0_cancel)"
    3.51    shows "r * setsum f A = setsum (%n. r * f n) A"
    3.52 @@ -1164,6 +1177,26 @@
    3.53    case False thus ?thesis by (simp add: setsum_def)
    3.54  qed
    3.55  
    3.56 +lemma abs_setsum_abs[simp]: 
    3.57 +  fixes f :: "'a => ('b::lordered_ab_group_abs)"
    3.58 +  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
    3.59 +proof (cases "finite A")
    3.60 +  case True
    3.61 +  thus ?thesis
    3.62 +  proof (induct)
    3.63 +    case empty thus ?case by simp
    3.64 +  next
    3.65 +    case (insert a A)
    3.66 +    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
    3.67 +    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
    3.68 +    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
    3.69 +    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
    3.70 +    finally show ?case .
    3.71 +  qed
    3.72 +next
    3.73 +  case False thus ?thesis by (simp add: setsum_def)
    3.74 +qed
    3.75 +
    3.76  
    3.77  subsection {* Generalized product over a set *}
    3.78  
    3.79 @@ -1430,7 +1463,7 @@
    3.80    by (simp add: card_insert_if)
    3.81  
    3.82  lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
    3.83 -by (simp add: card_def setsum_mono2_nat)
    3.84 +by (simp add: card_def setsum_mono2)
    3.85  
    3.86  lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
    3.87    apply (induct set: Finites, simp, clarify)
    3.88 @@ -1497,13 +1530,13 @@
    3.89  done
    3.90  
    3.91  
    3.92 -lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
    3.93 -  -- {* Generalized to any @{text comm_semiring_1_cancel} in
    3.94 -        @{text IntDef} as @{text setsum_constant}. *}
    3.95 -apply (cases "finite A") 
    3.96 -apply (erule finite_induct, auto)
    3.97 +lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
    3.98 +apply (cases "finite A")
    3.99 +apply (erule finite_induct)
   3.100 +apply (auto simp add: ring_distrib add_ac)
   3.101  done
   3.102  
   3.103 +
   3.104  lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
   3.105    apply (erule finite_induct)
   3.106    apply (auto simp add: power_Suc)
   3.107 @@ -1512,15 +1545,18 @@
   3.108  
   3.109  subsubsection {* Cardinality of unions *}
   3.110  
   3.111 +lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
   3.112 +by(induct n, auto)
   3.113 +
   3.114  lemma card_UN_disjoint:
   3.115      "finite I ==> (ALL i:I. finite (A i)) ==>
   3.116          (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
   3.117        card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
   3.118 -  apply (simp add: card_def)
   3.119 +  apply (simp add: card_def del: setsum_constant)
   3.120    apply (subgoal_tac
   3.121             "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
   3.122 -  apply (simp add: setsum_UN_disjoint)
   3.123 -  apply (simp add: setsum_constant_nat cong: setsum_cong)
   3.124 +  apply (simp add: setsum_UN_disjoint del: setsum_constant)
   3.125 +  apply (simp cong: setsum_cong)
   3.126    done
   3.127  
   3.128  lemma card_Union_disjoint:
   3.129 @@ -1546,7 +1582,7 @@
   3.130    done
   3.131  
   3.132  lemma card_image: "inj_on f A ==> card (f ` A) = card A"
   3.133 -by(simp add:card_def setsum_reindex o_def)
   3.134 +by(simp add:card_def setsum_reindex o_def del:setsum_constant)
   3.135  
   3.136  lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   3.137    by (simp add: card_seteq card_image)
   3.138 @@ -1587,18 +1623,17 @@
   3.139  lemma card_SigmaI [simp]:
   3.140    "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
   3.141    \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
   3.142 -by(simp add:card_def setsum_Sigma)
   3.143 +by(simp add:card_def setsum_Sigma del:setsum_constant)
   3.144  
   3.145  lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
   3.146  apply (cases "finite A") 
   3.147  apply (cases "finite B") 
   3.148 -  apply (simp add: setsum_constant_nat) 
   3.149  apply (auto simp add: card_eq_0_iff
   3.150 -            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
   3.151 +            dest: finite_cartesian_productD1 finite_cartesian_productD2)
   3.152  done
   3.153  
   3.154  lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
   3.155 -by (simp add: card_cartesian_product) 
   3.156 +by (simp add: card_cartesian_product)
   3.157  
   3.158  
   3.159  
     4.1 --- a/src/HOL/Hyperreal/HSeries.thy	Sat Feb 19 18:44:34 2005 +0100
     4.2 +++ b/src/HOL/Hyperreal/HSeries.thy	Mon Feb 21 15:04:10 2005 +0100
     4.3 @@ -15,10 +15,10 @@
     4.4    sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
     4.5     "sumhr p == 
     4.6        (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
     4.7 -                             hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"
     4.8 +                             hyprel ``{%n::nat. setsum f {X n..<Y n}})) p"
     4.9  
    4.10    NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
    4.11 -   "f NSsums s  == (%n. sumr 0 n f) ----NS> s"
    4.12 +   "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"
    4.13  
    4.14    NSsummable :: "(nat=>real) => bool"
    4.15     "NSsummable f == (\<exists>s. f NSsums s)"
    4.16 @@ -30,9 +30,9 @@
    4.17  lemma sumhr: 
    4.18       "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),  
    4.19              Abs_hypnat(hypnatrel``{%n. N n}), f) =  
    4.20 -      Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})"
    4.21 +      Abs_hypreal(hyprel `` {%n. setsum f {M n..<N n}})"
    4.22  apply (simp add: sumhr_def)
    4.23 -apply (rule arg_cong [where f = Abs_hypreal]) 
    4.24 +apply (rule arg_cong [where f = Abs_hypreal])
    4.25  apply (auto, ultra)
    4.26  done
    4.27  
    4.28 @@ -84,7 +84,7 @@
    4.29  lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
    4.30  apply (cases n, cases p)
    4.31  apply (auto elim!: FreeUltrafilterNat_subset simp 
    4.32 -            add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
    4.33 +            add: hypnat_zero_def sumhr hypreal_add hypnat_less setsum_add_nat_ivl)
    4.34  done
    4.35  
    4.36  lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
    4.37 @@ -124,7 +124,7 @@
    4.38  lemma sumhr_shift_bounds:
    4.39       "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
    4.40  apply (cases m, cases n)
    4.41 -apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
    4.42 +apply (simp add: sumhr hypnat_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
    4.43  done
    4.44  
    4.45  
    4.46 @@ -147,15 +147,20 @@
    4.47           add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def 
    4.48                hypnat_zero_def hypnat_omega_def)
    4.49  
    4.50 +(* FIXME move *)
    4.51 +lemma setsum_ivl_cong:
    4.52 + "i = m \<Longrightarrow> j = n \<Longrightarrow> (!!x. m <= x \<Longrightarrow> x < n \<Longrightarrow> f x = g x) \<Longrightarrow>
    4.53 + setsum f {i..<j} = setsum g {m..<n}"
    4.54 +by(rule setsum_cong, simp_all)
    4.55 +
    4.56  lemma sumhr_interval_const:
    4.57       "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
    4.58        ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
    4.59            (hypreal_of_nat (na - m) * hypreal_of_real r)"
    4.60 -by (auto dest!: sumr_interval_const 
    4.61 -         simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq 
    4.62 -                   hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
    4.63 +by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq hypreal_of_real_def
    4.64 +             real_of_nat_def hypreal_mult cong: setsum_ivl_cong)
    4.65  
    4.66 -lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
    4.67 +lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
    4.68  apply (cases N)
    4.69  apply (simp add: hypnat_zero_def starfunNat sumhr)
    4.70  done
    4.71 @@ -192,7 +197,8 @@
    4.72  lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
    4.73  by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
    4.74  
    4.75 -lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"
    4.76 +lemma NSseries_zero:
    4.77 +  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
    4.78  by (simp add: sums_NSsums_iff [symmetric] series_zero)
    4.79  
    4.80  lemma NSsummable_NSCauchy:
     5.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Sat Feb 19 18:44:34 2005 +0100
     5.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Feb 21 15:04:10 2005 +0100
     5.3 @@ -56,7 +56,6 @@
     5.4  lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
     5.5  apply (cases x)
     5.6  apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
     5.7 -                      real_sqrt_pow2_iff 
     5.8              simp del: hpowr_Suc realpow_Suc)
     5.9  done
    5.10  
    5.11 @@ -586,7 +585,7 @@
    5.12  apply (frule STAR_sin_Infinitesimal_divide
    5.13                 [OF Infinitesimal_pi_divide_HNatInfinite 
    5.14                     pi_divide_HNatInfinite_not_zero])
    5.15 -apply (auto simp add: inverse_mult_distrib)
    5.16 +apply (auto)
    5.17  apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
    5.18  apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
    5.19  done
     6.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sat Feb 19 18:44:34 2005 +0100
     6.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Feb 21 15:04:10 2005 +0100
     6.3 @@ -167,7 +167,7 @@
     6.4       "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
     6.5  apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]])
     6.6  apply (safe, drule_tac x = X in bspec)
     6.7 -apply (auto simp add: UNIV_diff_Compl)
     6.8 +apply (auto)
     6.9  done
    6.10  
    6.11  lemma FreeUltrafilterNat_Compl_iff1:
    6.12 @@ -183,12 +183,9 @@
    6.13  apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
    6.14  done
    6.15  
    6.16 -lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat"
    6.17 +lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
    6.18  by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
    6.19  
    6.20 -lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat"
    6.21 -by auto
    6.22 -
    6.23  lemma FreeUltrafilterNat_Nat_set_refl [intro]:
    6.24       "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
    6.25  by simp
    6.26 @@ -200,7 +197,7 @@
    6.27  by (rule ccontr, simp)
    6.28  
    6.29  lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat"
    6.30 -by (auto intro: FreeUltrafilterNat_Nat_set)
    6.31 +by (auto)
    6.32  
    6.33  
    6.34  text{*Define and use Ultrafilter tactics*}
    6.35 @@ -335,8 +332,7 @@
    6.36  
    6.37  lemma hypreal_minus: 
    6.38     "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
    6.39 -by (simp add: hypreal_minus_def Abs_hypreal_inject 
    6.40 -              hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
    6.41 +by (simp add: hypreal_minus_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
    6.42                UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
    6.43  
    6.44  lemma hypreal_diff:
    6.45 @@ -348,7 +344,7 @@
    6.46  by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add)
    6.47  
    6.48  lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
    6.49 -by (simp add: hypreal_add_commute hypreal_add_minus)
    6.50 +by (simp add: hypreal_add_commute)
    6.51  
    6.52  
    6.53  subsection{*Hyperreal Multiplication*}
    6.54 @@ -390,8 +386,7 @@
    6.55  lemma hypreal_inverse: 
    6.56        "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
    6.57         Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
    6.58 -by (simp add: hypreal_inverse_def Abs_hypreal_inject 
    6.59 -              hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
    6.60 +by (simp add: hypreal_inverse_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
    6.61                UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
    6.62  
    6.63  lemma hypreal_mult_inverse: 
    6.64 @@ -466,7 +461,7 @@
    6.65    by intro_classes (rule hypreal_le_linear)
    6.66  
    6.67  lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
    6.68 -by (auto simp add: order_less_irrefl)
    6.69 +by (auto)
    6.70  
    6.71  lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
    6.72  apply (cases x, cases y, cases z)
    6.73 @@ -702,7 +697,6 @@
    6.74  val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1";
    6.75  val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2";
    6.76  val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV";
    6.77 -val FreeUltrafilterNat_Nat_set = thm "FreeUltrafilterNat_Nat_set";
    6.78  val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl";
    6.79  val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P";
    6.80  val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
     7.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Sat Feb 19 18:44:34 2005 +0100
     7.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Feb 21 15:04:10 2005 +0100
     7.3 @@ -71,7 +71,7 @@
     7.4  
     7.5  lemma hrabs_hrealpow_two [simp]:
     7.6       "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
     7.7 -by (simp add: abs_mult)
     7.8 +by (simp)
     7.9  
    7.10  lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
    7.11  by (insert power_increasing [of 0 n "2::hypreal"], simp)
     8.1 --- a/src/HOL/Hyperreal/Integration.thy	Sat Feb 19 18:44:34 2005 +0100
     8.2 +++ b/src/HOL/Hyperreal/Integration.thy	Mon Feb 21 15:04:10 2005 +0100
     8.3 @@ -40,7 +40,7 @@
     8.4    --{*Riemann sum*}
     8.5  
     8.6    rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
     8.7 -  "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
     8.8 +  "rsum == %(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n))"
     8.9  
    8.10    --{*Gauge integrability (definite)*}
    8.11  
    8.12 @@ -331,7 +331,7 @@
    8.13  done
    8.14  
    8.15  lemma sumr_partition_eq_diff_bounds [simp]:
    8.16 -     "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
    8.17 +     "(\<Sum>n=0..<m. D (Suc n) - D n::real) = D(m) - D 0"
    8.18  by (induct "m", auto)
    8.19  
    8.20  lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
    8.21 @@ -453,7 +453,7 @@
    8.22  apply (auto simp add: zero_less_divide_iff)
    8.23  apply (rule exI)
    8.24  apply (auto simp add: tpart_def rsum_def)
    8.25 -apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = f b - f a")
    8.26 +apply (subgoal_tac "(\<Sum>n=0..<psize D. f(D(Suc n)) - f(D n)) = f b - f a")
    8.27   prefer 2
    8.28   apply (cut_tac D = "%n. f (D n)" and m = "psize D"
    8.29          in sumr_partition_eq_diff_bounds)
    8.30 @@ -461,10 +461,10 @@
    8.31  apply (drule sym, simp)
    8.32  apply (simp (no_asm) add: setsum_subtractf[symmetric])
    8.33  apply (rule setsum_abs [THEN order_trans])
    8.34 -apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
    8.35 +apply (subgoal_tac "ea = (\<Sum>n=0..<psize D. (ea / (b - a)) * (D (Suc n) - (D n)))")
    8.36  apply (simp add: abs_minus_commute)
    8.37  apply (rule_tac t = ea in ssubst, assumption)
    8.38 -apply (rule sumr_le2)
    8.39 +apply (rule setsum_mono)
    8.40  apply (rule_tac [2] setsum_mult [THEN subst])
    8.41  apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
    8.42            fine_def)
    8.43 @@ -812,7 +812,7 @@
    8.44           tpart(a,b) (D,p)
    8.45        |] ==> rsum(D,p) f \<le> rsum(D,p) g"
    8.46  apply (simp add: rsum_def)
    8.47 -apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2]
    8.48 +apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2]
    8.49                 dest!: lemma_Integral_le)
    8.50  done
    8.51  
     9.1 --- a/src/HOL/Hyperreal/Lim.thy	Sat Feb 19 18:44:34 2005 +0100
     9.2 +++ b/src/HOL/Hyperreal/Lim.thy	Mon Feb 21 15:04:10 2005 +0100
     9.3 @@ -771,7 +771,7 @@
     9.4  apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
     9.5  apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
     9.6  apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
     9.7 -apply (auto simp add: times_divide_eq_left diff_minus
     9.8 +apply (auto simp add: diff_minus
     9.9  	       approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
    9.10  		     Infinitesimal_subset_HFinite [THEN subsetD])
    9.11  done
    9.12 @@ -787,7 +787,7 @@
    9.13  apply (drule_tac x = h in bspec)
    9.14  apply (drule_tac [2] c = h in approx_mult1)
    9.15  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
    9.16 -            simp add: times_divide_eq_left diff_minus)
    9.17 +            simp add: diff_minus)
    9.18  done
    9.19  
    9.20  lemma NSDERIVD3:
    9.21 @@ -799,7 +799,7 @@
    9.22  apply (rule ccontr, drule_tac x = h in bspec)
    9.23  apply (drule_tac [2] c = h in approx_mult1)
    9.24  apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
    9.25 -            simp add: mult_assoc times_divide_eq_left diff_minus)
    9.26 +            simp add: mult_assoc diff_minus)
    9.27  done
    9.28  
    9.29  text{*Now equivalence between NSDERIV and DERIV*}
    9.30 @@ -821,7 +821,7 @@
    9.31  apply (drule_tac x3=D in
    9.32             HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
    9.33               THEN mem_infmal_iff [THEN iffD1]])
    9.34 -apply (auto simp add: times_divide_eq_right mult_commute
    9.35 +apply (auto simp add: mult_commute
    9.36              intro: approx_trans approx_minus_iff [THEN iffD2])
    9.37  done
    9.38  
    9.39 @@ -872,7 +872,7 @@
    9.40  apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
    9.41  apply (erule_tac V = "(x + y) / z = hypreal_of_real D + yb" in thin_rl)
    9.42  apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
    9.43 -            simp add: times_divide_eq_left mult_assoc mem_infmal_iff [symmetric])
    9.44 +            simp add: mult_assoc mem_infmal_iff [symmetric])
    9.45  apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
    9.46  done
    9.47  
    9.48 @@ -983,7 +983,7 @@
    9.49          in hypreal_mult_right_cancel [THEN iffD2])
    9.50  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)
    9.51  apply assumption
    9.52 -apply (simp add: times_divide_eq_left times_divide_eq_right [symmetric])
    9.53 +apply (simp add: times_divide_eq_right [symmetric])
    9.54  apply (auto simp add: left_distrib)
    9.55  done
    9.56  
    9.57 @@ -1188,7 +1188,7 @@
    9.58    show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
    9.59    proof (intro exI conjI)
    9.60      let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
    9.61 -    show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp add: times_divide_eq)
    9.62 +    show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp)
    9.63      show "isCont ?g x" using der
    9.64        by (simp add: isCont_iff DERIV_iff diff_minus
    9.65                 cong: LIM_equal [rule_format])
    9.66 @@ -1327,13 +1327,13 @@
    9.67     \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
    9.68  apply (rule allI)
    9.69  apply (induct_tac "n")
    9.70 -apply (auto simp add: Bolzano_bisect_le Let_def split_def times_divide_eq)
    9.71 +apply (auto simp add: Bolzano_bisect_le Let_def split_def)
    9.72  done
    9.73  
    9.74  lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" 
    9.75 -apply (auto simp add: times_divide_eq) 
    9.76 +apply (auto)
    9.77  apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
    9.78 -apply (simp add: times_divide_eq) 
    9.79 +apply (simp)
    9.80  done
    9.81  
    9.82  lemma Bolzano_bisect_diff:
    9.83 @@ -1798,7 +1798,7 @@
    9.84    hence ba: "b-a \<noteq> 0" by arith
    9.85    show ?thesis
    9.86      by (rule real_mult_left_cancel [OF ba, THEN iffD1],
    9.87 -        simp add: times_divide_eq right_diff_distrib, 
    9.88 +        simp add: right_diff_distrib, 
    9.89          simp add: left_diff_distrib)
    9.90  qed
    9.91  
    9.92 @@ -1834,8 +1834,7 @@
    9.93    proof (intro exI conjI)
    9.94      show "a < z" .
    9.95      show "z < b" .
    9.96 -    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" 
    9.97 -      by (simp add: times_divide_eq)
    9.98 +    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp)
    9.99      show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
   9.100    qed
   9.101  qed
   9.102 @@ -1885,14 +1884,14 @@
   9.103  lemma DERIV_const_ratio_const2:
   9.104       "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
   9.105  apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
   9.106 -apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc times_divide_eq)
   9.107 +apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc)
   9.108  done
   9.109  
   9.110  lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
   9.111 -by (simp add: times_divide_eq) 
   9.112 +by (simp) 
   9.113  
   9.114  lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
   9.115 -by (simp add: times_divide_eq) 
   9.116 +by (simp) 
   9.117  
   9.118  text{*Gallileo's "trick": average velocity = av. of end velocities*}
   9.119  
    10.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Feb 19 18:44:34 2005 +0100
    10.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Feb 21 15:04:10 2005 +0100
    10.3 @@ -9,25 +9,32 @@
    10.4  imports Log
    10.5  begin
    10.6  
    10.7 -lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
    10.8 +(* FIXME generalize? *)
    10.9 +lemma sumr_offset:
   10.10 + "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
   10.11  by (induct "n", auto)
   10.12  
   10.13 -lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
   10.14 +lemma sumr_offset2:
   10.15 + "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
   10.16  by (induct "n", auto)
   10.17  
   10.18 -lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
   10.19 +lemma sumr_offset3:
   10.20 +  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
   10.21  by (simp  add: sumr_offset)
   10.22  
   10.23 -lemma sumr_offset4: "\<forall>n f. sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
   10.24 +lemma sumr_offset4:
   10.25 + "\<forall>n f. setsum f {0::nat..<n+k} =
   10.26 +        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
   10.27  by (simp add: sumr_offset)
   10.28  
   10.29 +(*
   10.30  lemma sumr_from_1_from_0: "0 < n ==>
   10.31 -      sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else
   10.32 -             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) =
   10.33 -      sumr 0 (Suc n) (%n. (if even(n) then 0 else
   10.34 -             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)"
   10.35 +      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
   10.36 +             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
   10.37 +      (\<Sum>n=0..<Suc n. if even(n) then 0 else
   10.38 +             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
   10.39  by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
   10.40 -
   10.41 +*)
   10.42  
   10.43  subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
   10.44  
   10.45 @@ -36,12 +43,12 @@
   10.46  
   10.47  lemma Maclaurin_lemma:
   10.48      "0 < h ==>
   10.49 -     \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
   10.50 +     \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
   10.51                 (B * ((h^n) / real(fact n)))"
   10.52 -apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
   10.53 +apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
   10.54                   real(fact n) / (h^n)"
   10.55         in exI)
   10.56 -apply (simp add: times_divide_eq) 
   10.57 +apply (simp) 
   10.58  done
   10.59  
   10.60  lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
   10.61 @@ -92,9 +99,9 @@
   10.62    prefer 3 apply (simp add: fact_diff_Suc)
   10.63   prefer 2 apply simp
   10.64  apply (frule_tac m = m in less_add_one, clarify)
   10.65 -apply (simp del: sumr_Suc)
   10.66 +apply (simp del: setsum_Suc)
   10.67  apply (insert sumr_offset4 [of 1])
   10.68 -apply (simp del: sumr_Suc fact_Suc realpow_Suc)
   10.69 +apply (simp del: setsum_Suc fact_Suc realpow_Suc)
   10.70  apply (rule lemma_DERIV_subst)
   10.71  apply (rule DERIV_add)
   10.72  apply (rule_tac [2] DERIV_const)
   10.73 @@ -106,7 +113,7 @@
   10.74  apply (best intro: DERIV_chain2 intro!: DERIV_intros)
   10.75  apply (subst fact_Suc)
   10.76  apply (subst real_of_nat_mult)
   10.77 -apply (simp add: inverse_mult_distrib mult_ac)
   10.78 +apply (simp add: mult_ac)
   10.79  done
   10.80  
   10.81  
   10.82 @@ -137,7 +144,7 @@
   10.83      ==> \<exists>t. 0 < t &
   10.84                t < h &
   10.85                f h =
   10.86 -              sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) +
   10.87 +              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
   10.88                (diff n t / real (fact n)) * h ^ n"
   10.89  apply (case_tac "n = 0", force)
   10.90  apply (drule not0_implies_Suc)
   10.91 @@ -145,15 +152,15 @@
   10.92  apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
   10.93  apply (erule exE)
   10.94  apply (subgoal_tac "\<exists>g.
   10.95 -     g = (%t. f t - (sumr 0 n (%m. (diff m 0 / real(fact m)) * t^m) + (B * (t^n / real(fact n)))))")
   10.96 +     g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))")
   10.97   prefer 2 apply blast
   10.98  apply (erule exE)
   10.99  apply (subgoal_tac "g 0 = 0 & g h =0")
  10.100   prefer 2
  10.101 - apply (simp del: sumr_Suc)
  10.102 + apply (simp del: setsum_Suc)
  10.103   apply (cut_tac n = m and k = 1 in sumr_offset2)
  10.104 - apply (simp add: eq_diff_eq' del: sumr_Suc)
  10.105 -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))))))")
  10.106 + apply (simp add: eq_diff_eq' del: setsum_Suc)
  10.107 +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))))))")
  10.108   prefer 2 apply blast
  10.109  apply (erule exE)
  10.110  apply (subgoal_tac "difg 0 = g")
  10.111 @@ -165,15 +172,15 @@
  10.112    apply (simp (no_asm_simp))
  10.113   apply (erule exE)
  10.114   apply (rule_tac x = t in exI)
  10.115 - apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
  10.116 + apply (simp del: realpow_Suc fact_Suc)
  10.117  apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
  10.118   prefer 2
  10.119   apply clarify
  10.120   apply simp
  10.121   apply (frule_tac m = ma in less_add_one, clarify)
  10.122 - apply (simp del: sumr_Suc)
  10.123 + apply (simp del: setsum_Suc)
  10.124  apply (insert sumr_offset4 [of 1])
  10.125 -apply (simp del: sumr_Suc fact_Suc realpow_Suc)
  10.126 +apply (simp del: setsum_Suc fact_Suc realpow_Suc)
  10.127  apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
  10.128  apply (rule allI, rule impI)
  10.129  apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
  10.130 @@ -181,11 +188,11 @@
  10.131  apply (erule exE)
  10.132  apply (rule_tac x = t in exI)
  10.133  (* do some tidying up *)
  10.134 -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)))))"
  10.135 +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)))))"
  10.136         in thin_rl)
  10.137 -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))))"
  10.138 +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))))"
  10.139         in thin_rl)
  10.140 -apply (erule_tac [!] V="f h = sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + B * (h ^ n / real (fact n))"
  10.141 +apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))"
  10.142         in thin_rl)
  10.143  (* back to business *)
  10.144  apply (simp (no_asm_simp))
  10.145 @@ -215,7 +222,7 @@
  10.146      --> (\<exists>t. 0 < t &
  10.147                t < h &
  10.148                f h =
  10.149 -              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
  10.150 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
  10.151                diff n t / real (fact n) * h ^ n)"
  10.152  by (blast intro: Maclaurin)
  10.153  
  10.154 @@ -227,7 +234,7 @@
  10.155      ==> \<exists>t. 0 < t &
  10.156                t \<le> h &
  10.157                f h =
  10.158 -              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
  10.159 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
  10.160                diff n t / real (fact n) * h ^ n"
  10.161  apply (case_tac "n", auto)
  10.162  apply (drule Maclaurin, auto)
  10.163 @@ -240,7 +247,7 @@
  10.164      --> (\<exists>t. 0 < t &
  10.165                t \<le> h &
  10.166                f h =
  10.167 -              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
  10.168 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
  10.169                diff n t / real (fact n) * h ^ n)"
  10.170  by (blast intro: Maclaurin2)
  10.171  
  10.172 @@ -250,12 +257,12 @@
  10.173      ==> \<exists>t. h < t &
  10.174                t < 0 &
  10.175                f h =
  10.176 -              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
  10.177 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
  10.178                diff n t / real (fact n) * h ^ n"
  10.179  apply (cut_tac f = "%x. f (-x)"
  10.180          and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
  10.181          and h = "-h" and n = n in Maclaurin_objl)
  10.182 -apply (simp add: times_divide_eq) 
  10.183 +apply (simp)
  10.184  apply safe
  10.185  apply (subst minus_mult_right)
  10.186  apply (rule DERIV_cmult)
  10.187 @@ -278,7 +285,7 @@
  10.188      --> (\<exists>t. h < t &
  10.189                t < 0 &
  10.190                f h =
  10.191 -              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
  10.192 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
  10.193                diff n t / real (fact n) * h ^ n)"
  10.194  by (blast intro: Maclaurin_minus)
  10.195  
  10.196 @@ -299,12 +306,12 @@
  10.197         \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
  10.198      ==> \<exists>t. abs t \<le> abs x &
  10.199                f x =
  10.200 -              sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) +
  10.201 +              (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
  10.202                diff n t / real (fact n) * x ^ n"
  10.203  apply (case_tac "n = 0", force)
  10.204  apply (case_tac "x = 0")
  10.205  apply (rule_tac x = 0 in exI)
  10.206 -apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
  10.207 +apply (force simp add: Maclaurin_bi_le_lemma)
  10.208  apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
  10.209  txt{*Case 1, where @{term "x < 0"}*}
  10.210  apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
  10.211 @@ -323,7 +330,7 @@
  10.212           \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
  10.213          x ~= 0; 0 < n
  10.214        |] ==> \<exists>t. 0 < abs t & abs t < abs x &
  10.215 -               f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
  10.216 +               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
  10.217                       (diff n t / real (fact n)) * x ^ n"
  10.218  apply (rule_tac x = x and y = 0 in linorder_cases)
  10.219  prefer 2 apply blast
  10.220 @@ -337,21 +344,21 @@
  10.221        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
  10.222        x ~= 0 & 0 < n
  10.223        --> (\<exists>t. 0 < abs t & abs t < abs x &
  10.224 -               f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
  10.225 +               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
  10.226                       (diff n t / real (fact n)) * x ^ n)"
  10.227  by (blast intro: Maclaurin_all_lt)
  10.228  
  10.229  lemma Maclaurin_zero [rule_format]:
  10.230       "x = (0::real)
  10.231        ==> 0 < n -->
  10.232 -          sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) =
  10.233 +          (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
  10.234            diff 0 0"
  10.235  by (induct n, auto)
  10.236  
  10.237  lemma Maclaurin_all_le: "[| diff 0 = f;
  10.238          \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
  10.239        |] ==> \<exists>t. abs t \<le> abs x &
  10.240 -              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
  10.241 +              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
  10.242                      (diff n t / real (fact n)) * x ^ n"
  10.243  apply (insert linorder_le_less_linear [of n 0])
  10.244  apply (erule disjE, force)
  10.245 @@ -366,7 +373,7 @@
  10.246  lemma Maclaurin_all_le_objl: "diff 0 = f &
  10.247        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
  10.248        --> (\<exists>t. abs t \<le> abs x &
  10.249 -              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
  10.250 +              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
  10.251                      (diff n t / real (fact n)) * x ^ n)"
  10.252  by (blast intro: Maclaurin_all_le)
  10.253  
  10.254 @@ -376,14 +383,14 @@
  10.255  lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
  10.256        ==> (\<exists>t. 0 < abs t &
  10.257                  abs t < abs x &
  10.258 -                exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
  10.259 +                exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
  10.260                          (exp t / real (fact n)) * x ^ n)"
  10.261  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
  10.262  
  10.263  
  10.264  lemma Maclaurin_exp_le:
  10.265       "\<exists>t. abs t \<le> abs x &
  10.266 -            exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
  10.267 +            exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
  10.268                         (exp t / real (fact n)) * x ^ n"
  10.269  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
  10.270  
  10.271 @@ -421,29 +428,29 @@
  10.272  lemma Maclaurin_sin_expansion2:
  10.273       "\<exists>t. abs t \<le> abs x &
  10.274         sin x =
  10.275 -       (sumr 0 n (%m. (if even m then 0
  10.276 +       (\<Sum>m=0..<n. (if even m then 0
  10.277                         else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
  10.278 -                       x ^ m))
  10.279 +                       x ^ m)
  10.280        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
  10.281  apply (cut_tac f = sin and n = n and x = x
  10.282          and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
  10.283  apply safe
  10.284  apply (simp (no_asm))
  10.285 -apply (simp (no_asm) add: times_divide_eq)
  10.286 +apply (simp (no_asm))
  10.287  apply (case_tac "n", clarify, simp, simp)
  10.288  apply (rule ccontr, simp)
  10.289  apply (drule_tac x = x in spec, simp)
  10.290  apply (erule ssubst)
  10.291  apply (rule_tac x = t in exI, simp)
  10.292  apply (rule setsum_cong[OF refl])
  10.293 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
  10.294 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
  10.295  done
  10.296  
  10.297  lemma Maclaurin_sin_expansion:
  10.298       "\<exists>t. sin x =
  10.299 -       (sumr 0 n (%m. (if even m then 0
  10.300 +       (\<Sum>m=0..<n. (if even m then 0
  10.301                         else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
  10.302 -                       x ^ m))
  10.303 +                       x ^ m)
  10.304        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
  10.305  apply (insert Maclaurin_sin_expansion2 [of x n]) 
  10.306  apply (blast intro: elim:); 
  10.307 @@ -455,63 +462,60 @@
  10.308       "[| 0 < n; 0 < x |] ==>
  10.309         \<exists>t. 0 < t & t < x &
  10.310         sin x =
  10.311 -       (sumr 0 n (%m. (if even m then 0
  10.312 +       (\<Sum>m=0..<n. (if even m then 0
  10.313                         else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
  10.314 -                       x ^ m))
  10.315 +                       x ^ m)
  10.316        + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
  10.317  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)
  10.318  apply safe
  10.319  apply simp
  10.320 -apply (simp (no_asm) add: times_divide_eq)
  10.321 +apply (simp (no_asm))
  10.322  apply (erule ssubst)
  10.323  apply (rule_tac x = t in exI, simp)
  10.324  apply (rule setsum_cong[OF refl])
  10.325 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
  10.326 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
  10.327  done
  10.328  
  10.329  lemma Maclaurin_sin_expansion4:
  10.330       "0 < x ==>
  10.331         \<exists>t. 0 < t & t \<le> x &
  10.332         sin x =
  10.333 -       (sumr 0 n (%m. (if even m then 0
  10.334 +       (\<Sum>m=0..<n. (if even m then 0
  10.335                         else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
  10.336 -                       x ^ m))
  10.337 +                       x ^ m)
  10.338        + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
  10.339  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)
  10.340  apply safe
  10.341  apply simp
  10.342 -apply (simp (no_asm) add: times_divide_eq)
  10.343 +apply (simp (no_asm))
  10.344  apply (erule ssubst)
  10.345  apply (rule_tac x = t in exI, simp)
  10.346  apply (rule setsum_cong[OF refl])
  10.347 -apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
  10.348 +apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
  10.349  done
  10.350  
  10.351  
  10.352  subsection{*Maclaurin Expansion for Cosine Function*}
  10.353  
  10.354  lemma sumr_cos_zero_one [simp]:
  10.355 -     "sumr 0 (Suc n)
  10.356 -         (%m. (if even m
  10.357 -               then (- 1) ^ (m div 2)/(real  (fact m))
  10.358 -               else 0) *
  10.359 -              0 ^ m) = 1"
  10.360 + "(\<Sum>m=0..<(Suc n).
  10.361 +     (if even m then (- 1) ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
  10.362  by (induct "n", auto)
  10.363  
  10.364  lemma Maclaurin_cos_expansion:
  10.365       "\<exists>t. abs t \<le> abs x &
  10.366         cos x =
  10.367 -       (sumr 0 n (%m. (if even m
  10.368 +       (\<Sum>m=0..<n. (if even m
  10.369                         then (- 1) ^ (m div 2)/(real (fact m))
  10.370                         else 0) *
  10.371 -                       x ^ m))
  10.372 +                       x ^ m)
  10.373        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
  10.374  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)
  10.375  apply safe
  10.376  apply (simp (no_asm))
  10.377 -apply (simp (no_asm) add: times_divide_eq)
  10.378 +apply (simp (no_asm))
  10.379  apply (case_tac "n", simp)
  10.380 -apply (simp del: sumr_Suc)
  10.381 +apply (simp del: setsum_Suc)
  10.382  apply (rule ccontr, simp)
  10.383  apply (drule_tac x = x in spec, simp)
  10.384  apply (erule ssubst)
  10.385 @@ -524,15 +528,15 @@
  10.386       "[| 0 < x; 0 < n |] ==>
  10.387         \<exists>t. 0 < t & t < x &
  10.388         cos x =
  10.389 -       (sumr 0 n (%m. (if even m
  10.390 +       (\<Sum>m=0..<n. (if even m
  10.391                         then (- 1) ^ (m div 2)/(real (fact m))
  10.392                         else 0) *
  10.393 -                       x ^ m))
  10.394 +                       x ^ m)
  10.395        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
  10.396  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)
  10.397  apply safe
  10.398  apply simp
  10.399 -apply (simp (no_asm) add: times_divide_eq)
  10.400 +apply (simp (no_asm))
  10.401  apply (erule ssubst)
  10.402  apply (rule_tac x = t in exI, simp)
  10.403  apply (rule setsum_cong[OF refl])
  10.404 @@ -543,15 +547,15 @@
  10.405       "[| x < 0; 0 < n |] ==>
  10.406         \<exists>t. x < t & t < 0 &
  10.407         cos x =
  10.408 -       (sumr 0 n (%m. (if even m
  10.409 +       (\<Sum>m=0..<n. (if even m
  10.410                         then (- 1) ^ (m div 2)/(real (fact m))
  10.411                         else 0) *
  10.412 -                       x ^ m))
  10.413 +                       x ^ m)
  10.414        + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
  10.415  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)
  10.416  apply safe
  10.417  apply simp
  10.418 -apply (simp (no_asm) add: times_divide_eq)
  10.419 +apply (simp (no_asm))
  10.420  apply (erule ssubst)
  10.421  apply (rule_tac x = t in exI, simp)
  10.422  apply (rule setsum_cong[OF refl])
  10.423 @@ -567,7 +571,7 @@
  10.424  by auto
  10.425  
  10.426  lemma Maclaurin_sin_bound:
  10.427 -  "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
  10.428 +  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
  10.429    x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
  10.430  proof -
  10.431    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
    11.1 --- a/src/HOL/Hyperreal/NSA.thy	Sat Feb 19 18:44:34 2005 +0100
    11.2 +++ b/src/HOL/Hyperreal/NSA.thy	Mon Feb 21 15:04:10 2005 +0100
    11.3 @@ -61,7 +61,7 @@
    11.4  lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"
    11.5  apply (simp add: SReal_def, safe)
    11.6  apply (rule_tac x = "r * ra" in exI)
    11.7 -apply (simp (no_asm) add: hypreal_of_real_mult)
    11.8 +apply (simp (no_asm))
    11.9  done
   11.10  
   11.11  lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals"
   11.12 @@ -301,7 +301,7 @@
   11.13  apply (auto simp add: Infinitesimal_def)
   11.14  apply (rule hypreal_sum_of_halves [THEN subst])
   11.15  apply (drule half_gt_zero)
   11.16 -apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of)
   11.17 +apply (blast intro: hrabs_add_less SReal_divide_number_of)
   11.18  done
   11.19  
   11.20  lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
   11.21 @@ -325,7 +325,7 @@
   11.22  apply (drule_tac x = "r/t" in bspec)
   11.23  apply (blast intro: SReal_divide)
   11.24  apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
   11.25 -apply (auto simp add: times_divide_eq_left zero_less_divide_iff)
   11.26 +apply (auto simp add: zero_less_divide_iff)
   11.27  done
   11.28  
   11.29  lemma Infinitesimal_HFinite_mult2:
   11.30 @@ -693,13 +693,13 @@
   11.31  lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z"
   11.32  apply (rule bex_Infinitesimal_iff [THEN iffD1])
   11.33  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   11.34 -apply (auto simp add: minus_add_distrib hypreal_add_assoc [symmetric])
   11.35 +apply (auto simp add: hypreal_add_assoc [symmetric])
   11.36  done
   11.37  
   11.38  lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y"
   11.39  apply (rule bex_Infinitesimal_iff [THEN iffD1])
   11.40  apply (drule Infinitesimal_minus_iff [THEN iffD2])
   11.41 -apply (auto simp add: minus_add_distrib hypreal_add_assoc [symmetric])
   11.42 +apply (auto simp add: hypreal_add_assoc [symmetric])
   11.43  done
   11.44  
   11.45  lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x"
   11.46 @@ -723,7 +723,7 @@
   11.47  
   11.48  lemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"
   11.49  apply (drule approx_minus_iff [THEN iffD1])
   11.50 -apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac)
   11.51 +apply (simp add: approx_minus_iff [symmetric] add_ac)
   11.52  done
   11.53  
   11.54  lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
   11.55 @@ -733,7 +733,7 @@
   11.56  
   11.57  lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
   11.58  apply (rule approx_minus_iff [THEN iffD2])
   11.59 -apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac)
   11.60 +apply (simp add: approx_minus_iff [symmetric] add_ac)
   11.61  done
   11.62  
   11.63  lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
   11.64 @@ -805,7 +805,7 @@
   11.65  done
   11.66  
   11.67  
   11.68 -subsection{* Zero is the Only Infinitesimal that is Also a Real*}
   11.69 +subsection{* Zero is the Only Infinitesimal that is also a Real*}
   11.70  
   11.71  lemma Infinitesimal_less_SReal:
   11.72       "[| x \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
   11.73 @@ -1077,7 +1077,7 @@
   11.74           isLub Reals {s. s \<in> Reals & s < x} t;
   11.75           r \<in> Reals; 0 < r |]
   11.76        ==> -(x + -t) \<noteq> r"
   11.77 -apply (auto simp add: minus_add_distrib)
   11.78 +apply (auto)
   11.79  apply (frule isLubD1a)
   11.80  apply (drule SReal_add_cancel, assumption)
   11.81  apply (drule_tac x = "-x" in SReal_minus, simp)
   11.82 @@ -1141,7 +1141,7 @@
   11.83  lemma not_HFinite_HInfinite: "x\<notin> HFinite ==> x \<in> HInfinite"
   11.84  apply (simp add: HInfinite_def HFinite_def, auto)
   11.85  apply (drule_tac x = "r + 1" in bspec)
   11.86 -apply (auto simp add: SReal_add)
   11.87 +apply (auto)
   11.88  done
   11.89  
   11.90  lemma HInfinite_HFinite_disj: "x \<in> HInfinite | x \<in> HFinite"
   11.91 @@ -1432,7 +1432,7 @@
   11.92        ==> hypreal_of_real x + u < hypreal_of_real y"
   11.93  apply (simp add: Infinitesimal_def)
   11.94  apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)  
   11.95 -apply (auto simp add: add_commute abs_less_iff SReal_add SReal_minus)
   11.96 +apply (auto simp add: add_commute abs_less_iff SReal_minus)
   11.97  apply (simp add: compare_rls) 
   11.98  done
   11.99  
  11.100 @@ -1646,7 +1646,7 @@
  11.101      by (simp add: ex ey) 
  11.102    also have "... = st ((ex + ey) + (st x + st y))" by (simp add: add_ac)
  11.103    also have "... = st x + st y" 
  11.104 -    by (simp add: prems st_SReal SReal_add Infinitesimal_add 
  11.105 +    by (simp add: prems st_SReal Infinitesimal_add 
  11.106                    st_Infinitesimal_add_SReal2) 
  11.107    finally show ?thesis .
  11.108  qed
  11.109 @@ -1870,7 +1870,7 @@
  11.110  apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp) 
  11.111  apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset])
  11.112  apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int)
  11.113 -apply (auto simp add: lemma_Int_HIa FreeUltrafilterNat_empty)
  11.114 +apply (auto simp add: lemma_Int_HIa)
  11.115  done
  11.116  
  11.117  lemma HInfinite_FreeUltrafilterNat_iff:
  11.118 @@ -1923,7 +1923,7 @@
  11.119  
  11.120  lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
  11.121  apply (induct n)
  11.122 -apply (simp_all add: SReal_add)
  11.123 +apply (simp_all)
  11.124  done 
  11.125   
  11.126  lemma lemma_Infinitesimal2:
  11.127 @@ -2075,7 +2075,7 @@
  11.128  
  11.129  lemma real_of_nat_inverse_eq_iff:
  11.130       "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
  11.131 -by (auto simp add: inverse_inverse_eq real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
  11.132 +by (auto simp add: real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
  11.133  
  11.134  lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
  11.135  apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff)
    12.1 --- a/src/HOL/Hyperreal/Poly.thy	Sat Feb 19 18:44:34 2005 +0100
    12.2 +++ b/src/HOL/Hyperreal/Poly.thy	Mon Feb 21 15:04:10 2005 +0100
    12.3 @@ -1026,7 +1026,7 @@
    12.4  apply (induct "p", auto)
    12.5  apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
    12.6  apply (rule abs_triangle_ineq)
    12.7 -apply (auto intro!: mult_mono simp add: abs_mult, arith)
    12.8 +apply (auto intro!: mult_mono, arith)
    12.9  done
   12.10  
   12.11  ML
    13.1 --- a/src/HOL/Hyperreal/SEQ.thy	Sat Feb 19 18:44:34 2005 +0100
    13.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon Feb 21 15:04:10 2005 +0100
    13.3 @@ -169,7 +169,7 @@
    13.4  apply (drule FreeUltrafilterNat_all)
    13.5  apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
    13.6  apply (drule FreeUltrafilterNat_Int, assumption)
    13.7 -apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty)
    13.8 +apply (simp add: lemmaLIM2)
    13.9  done
   13.10  
   13.11  lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
   13.12 @@ -207,7 +207,7 @@
   13.13  lemma NSLIMSEQ_mult:
   13.14        "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
   13.15  by (auto intro!: approx_mult_HFinite 
   13.16 -        simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric])
   13.17 +        simp add: NSLIMSEQ_def starfunNat_mult [symmetric])
   13.18  
   13.19  lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
   13.20  by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
   13.21 @@ -707,7 +707,7 @@
   13.22  apply (drule_tac M = M in lemmaCauchy1)
   13.23  apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
   13.24  apply (rule FreeUltrafilterNat_Int)
   13.25 -apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set)
   13.26 +apply (auto intro: FreeUltrafilterNat_Int)
   13.27  done
   13.28  
   13.29  subsubsection{*Nonstandard Implies Standard*}
    14.1 --- a/src/HOL/Hyperreal/Series.thy	Sat Feb 19 18:44:34 2005 +0100
    14.2 +++ b/src/HOL/Hyperreal/Series.thy	Mon Feb 21 15:04:10 2005 +0100
    14.3 @@ -3,6 +3,7 @@
    14.4      Copyright   : 1998  University of Cambridge
    14.5  
    14.6  Converted to Isar and polished by lcp
    14.7 +Converted to setsum and polished yet more by TNN
    14.8  *) 
    14.9  
   14.10  header{*Finite Summation and Infinite Series*}
   14.11 @@ -11,11 +12,9 @@
   14.12  imports SEQ Lim
   14.13  begin
   14.14  
   14.15 +(* FIXME why not globally? *)
   14.16  declare atLeastLessThan_empty[simp];
   14.17 -
   14.18 -syntax sumr :: "[nat,nat,(nat=>real)] => real"
   14.19 -translations
   14.20 -  "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
   14.21 +declare atLeastLessThan_iff[iff]
   14.22  
   14.23  constdefs
   14.24     sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
   14.25 @@ -25,10 +24,9 @@
   14.26     "summable f == (\<exists>s. f sums s)"
   14.27  
   14.28     suminf   :: "(nat=>real) => real"
   14.29 -   "suminf f == (@s. f sums s)"
   14.30 +   "suminf f == SOME s. f sums s"
   14.31  
   14.32 -
   14.33 -lemma sumr_Suc [simp]:
   14.34 +lemma setsum_Suc[simp]:
   14.35    "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
   14.36  by (simp add: atLeastLessThanSuc add_commute)
   14.37  
   14.38 @@ -45,7 +43,6 @@
   14.39  apply (rename_tac k) 
   14.40  apply (subgoal_tac "n=k", auto) 
   14.41  done
   14.42 -*)
   14.43  
   14.44  lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   14.45    setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
   14.46 @@ -58,8 +55,10 @@
   14.47  using sumr_split_add [of m n p f,symmetric]
   14.48  apply (simp add: add_ac)
   14.49  done
   14.50 +*)
   14.51  
   14.52 -lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
   14.53 +lemma sumr_diff_mult_const:
   14.54 + "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
   14.55  by (simp add: diff_minus setsum_addf real_of_nat_def)
   14.56  
   14.57  (*
   14.58 @@ -79,32 +78,54 @@
   14.59  
   14.60  lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
   14.61  by (simp add: Finite_Set.setsum_negf)
   14.62 +
   14.63 +lemma sumr_shift_bounds:
   14.64 +  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
   14.65 +by (induct "n", auto)
   14.66  *)
   14.67  
   14.68 -lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
   14.69 +(* Generalize from real to some algebraic structure? *)
   14.70 +lemma sumr_minus_one_realpow_zero [simp]:
   14.71 +  "setsum (%i. (-1) ^ Suc i) {0..<2*n} = (0::real)"
   14.72  by (induct "n", auto)
   14.73  
   14.74 -lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
   14.75 -by (induct "n", auto)
   14.76 -
   14.77 -lemma sumr_interval_const:
   14.78 -     "\<lbrakk>\<forall>n. m \<le> Suc n --> f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(k-m) * r)"
   14.79 -apply (induct "k", auto) 
   14.80 +(*
   14.81 +lemma sumr_interval_const2:
   14.82 +     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
   14.83 +      ==> sumr m k f = (real (k - m) * r)"
   14.84 +apply (induct "k", auto)
   14.85  apply (drule_tac x = k in spec)
   14.86  apply (auto dest!: le_imp_less_or_eq)
   14.87  apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
   14.88  done
   14.89 +*)
   14.90 +(* FIXME split in tow steps
   14.91 +lemma setsum_nat_set_real_const:
   14.92 +  "(\<And>n. n\<in>A \<Longrightarrow> f n = r) \<Longrightarrow> setsum f A = real(card A) * r" (is "PROP ?P")
   14.93 +proof (cases "finite A")
   14.94 +  case True
   14.95 +  thus "PROP ?P"
   14.96 +  proof induct
   14.97 +    case empty thus ?case by simp
   14.98 +  next
   14.99 +    case insert thus ?case by(simp add: left_distrib real_of_nat_Suc)
  14.100 +  qed
  14.101 +next
  14.102 +  case False thus "PROP ?P" by (simp add: setsum_def)
  14.103 +qed
  14.104 + *)
  14.105  
  14.106 -lemma sumr_interval_const2:
  14.107 -     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
  14.108 -      ==> sumr m k f = (real (k - m) * r)"
  14.109 -apply (induct "k", auto) 
  14.110 -apply (drule_tac x = k in spec)
  14.111 -apply (auto dest!: le_imp_less_or_eq)
  14.112 -apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
  14.113 +(*
  14.114 +lemma sumr_le:
  14.115 +     "[|\<forall>n\<ge>m. 0 \<le> (f n::real); m < k|] ==> setsum f {0..<m} \<le> setsum f {0..<k::nat}"
  14.116 +apply (induct "k")
  14.117 +apply (auto simp add: less_Suc_eq_le)
  14.118 +apply (drule_tac x = k in spec, safe)
  14.119 +apply (drule le_imp_less_or_eq, safe)
  14.120 +apply (arith)
  14.121 +apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
  14.122  done
  14.123  
  14.124 -
  14.125  lemma sumr_le:
  14.126       "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
  14.127  apply (induct "k")
  14.128 @@ -120,13 +141,16 @@
  14.129  apply (induct "n")
  14.130  apply (auto intro: add_mono simp add: le_def)
  14.131  done
  14.132 +*)
  14.133  
  14.134 +(*
  14.135  lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f"
  14.136  apply (induct "n", auto)
  14.137  apply (drule_tac x = n in spec, arith)
  14.138  done
  14.139 +*)
  14.140  
  14.141 -(* FIXME generalize *)
  14.142 +(*
  14.143  lemma rabs_sumr_rabs_cancel [simp]:
  14.144       "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
  14.145  by (induct "n", simp_all add: add_increasing)
  14.146 @@ -134,14 +158,19 @@
  14.147  lemma sumr_zero [rule_format]:
  14.148       "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
  14.149  by (induct "n", auto)
  14.150 +*)
  14.151  
  14.152  lemma Suc_le_imp_diff_ge2:
  14.153 -     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
  14.154 -apply (rule sumr_zero) 
  14.155 +     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> setsum f {m..<n} = 0"
  14.156 +apply (rule setsum_0')
  14.157  apply (case_tac "n", auto)
  14.158 +apply(erule_tac x = "a - 1" in allE)
  14.159 +apply (simp split:nat_diff_split)
  14.160  done
  14.161  
  14.162 -lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"
  14.163 +(* FIXME this is an awful lemma! *)
  14.164 +lemma sumr_one_lb_realpow_zero [simp]:
  14.165 +  "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
  14.166  apply (induct "n")
  14.167  apply (case_tac [2] "n", auto)
  14.168  done
  14.169 @@ -149,30 +178,46 @@
  14.170  lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
  14.171  by (simp add: diff_minus setsum_addf setsum_negf)
  14.172  *)
  14.173 +(*
  14.174  lemma sumr_subst [rule_format (no_asm)]:
  14.175       "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
  14.176  by (induct "n", auto)
  14.177 +*)
  14.178  
  14.179 +lemma setsum_bounded:
  14.180 +  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
  14.181 +  shows "setsum f A \<le> of_nat(card A) * K"
  14.182 +proof (cases "finite A")
  14.183 +  case True
  14.184 +  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
  14.185 +next
  14.186 +  case False thus ?thesis by (simp add: setsum_def)
  14.187 +qed
  14.188 +(*
  14.189  lemma sumr_bound [rule_format (no_asm)]:
  14.190       "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))  
  14.191 -      --> (sumr m (m + n) f \<le> (real n * K))"
  14.192 +      --> setsum f {m..<m+n::nat} \<le> (real n * K)"
  14.193  apply (induct "n")
  14.194  apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
  14.195  done
  14.196 -
  14.197 +*)
  14.198 +(* FIXME should be generalized
  14.199  lemma sumr_bound2 [rule_format (no_asm)]:
  14.200       "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
  14.201 -      --> (sumr 0 n f \<le> (real n * K))"
  14.202 +      --> setsum f {0..<n::nat} \<le> (real n * K)"
  14.203  apply (induct "n")
  14.204  apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
  14.205  done
  14.206 -
  14.207 + *)
  14.208 +(* FIXME a bit specialized for [simp]! *)
  14.209  lemma sumr_group [simp]:
  14.210 -     "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"
  14.211 -apply (subgoal_tac "k = 0 | 0 < k", auto)
  14.212 +     "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
  14.213 +apply (subgoal_tac "k = 0 | 0 < k", auto simp:setsum_0')
  14.214  apply (induct "n")
  14.215 -apply (simp_all add: sumr_split_add add_commute)
  14.216 +apply (simp_all add: setsum_add_nat_ivl add_commute)
  14.217  done
  14.218 +(* FIXME setsum_0[simp] *)
  14.219 +
  14.220  
  14.221  subsection{* Infinite Sums, by the Properties of Limits*}
  14.222  
  14.223 @@ -188,7 +233,7 @@
  14.224  done
  14.225  
  14.226  lemma summable_sumr_LIMSEQ_suminf: 
  14.227 -     "summable f ==> (%n. sumr 0 n f) ----> (suminf f)"
  14.228 +     "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
  14.229  apply (simp add: summable_def suminf_def sums_def)
  14.230  apply (blast intro: someI2)
  14.231  done
  14.232 @@ -216,14 +261,31 @@
  14.233  next one was called series_zero2
  14.234  **********************)
  14.235  
  14.236 +lemma ivl_subset[simp]:
  14.237 + "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
  14.238 +apply(auto simp:linorder_not_le)
  14.239 +apply(rule ccontr)
  14.240 +apply(frule subsetCE[where c = n])
  14.241 +apply(auto simp:linorder_not_le)
  14.242 +done
  14.243 +
  14.244 +lemma ivl_diff[simp]:
  14.245 + "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
  14.246 +by(auto)
  14.247 +
  14.248 +
  14.249 +(* FIXME the last step should work w/o Ball_def, ideally just with
  14.250 +   setsum_0 and setsum_cong. Currently the simplifier does not simplify
  14.251 +   the premise x:{i..<j} that ball_cong (or a modified version of setsum_0')
  14.252 +   generates. FIX simplifier??? *)
  14.253  lemma series_zero: 
  14.254 -     "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (sumr 0 n f)"
  14.255 +     "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
  14.256  apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
  14.257  apply (rule_tac x = n in exI)
  14.258 -apply (clarsimp simp:sumr_split_add_minus)
  14.259 -apply (drule sumr_interval_const2, auto)
  14.260 +apply (clarsimp simp add:setsum_diff[symmetric] setsum_0' Ball_def)
  14.261  done
  14.262  
  14.263 +
  14.264  lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
  14.265  by (auto simp add: sums_def setsum_mult [symmetric]
  14.266           intro!: LIMSEQ_mult intro: LIMSEQ_const)
  14.267 @@ -249,7 +311,7 @@
  14.268  by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
  14.269  
  14.270  lemma sums_group:
  14.271 -     "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"
  14.272 +     "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
  14.273  apply (drule summable_sums)
  14.274  apply (auto simp add: sums_def LIMSEQ_def)
  14.275  apply (drule_tac x = r in spec, safe)
  14.276 @@ -260,18 +322,18 @@
  14.277  done
  14.278  
  14.279  lemma sumr_pos_lt_pair_lemma:
  14.280 -     "[|\<forall>d. - f (n + (d + d)) < f (Suc (n + (d + d)))|]
  14.281 -      ==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f"
  14.282 +  "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |]
  14.283 +   ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}"
  14.284  apply (induct "no", auto)
  14.285  apply (drule_tac x = "Suc no" in spec)
  14.286 -apply (simp add: add_ac) 
  14.287 +apply (simp add: add_ac)
  14.288  done
  14.289  
  14.290  
  14.291  lemma sumr_pos_lt_pair:
  14.292       "[|summable f; 
  14.293          \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
  14.294 -      ==> sumr 0 n f < suminf f"
  14.295 +      ==> setsum f {0..<n} < suminf f"
  14.296  apply (drule summable_sums)
  14.297  apply (auto simp add: sums_def LIMSEQ_def)
  14.298  apply (drule_tac x = "f (n) + f (n + 1)" in spec)
  14.299 @@ -282,18 +344,19 @@
  14.300  apply (drule_tac x = 0 in spec, simp)
  14.301  apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
  14.302  apply (safe, simp)
  14.303 -apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
  14.304 -apply (rule_tac [2] y = "sumr 0 (n+ Suc (Suc 0)) f" in order_trans)
  14.305 +apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le>
  14.306 + setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
  14.307 +apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
  14.308  prefer 3 apply assumption
  14.309 -apply (rule_tac [2] y = "sumr 0 n f + (f (n) + f (n + 1))" in order_trans)
  14.310 +apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
  14.311  apply simp_all 
  14.312 -apply (subgoal_tac "suminf f \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
  14.313 +apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
  14.314  apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
  14.315 -prefer 3 apply simp 
  14.316 +prefer 3 apply simp
  14.317  apply (drule_tac [2] x = 0 in spec)
  14.318   prefer 2 apply simp 
  14.319 -apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f")
  14.320 -apply (simp add: abs_if) 
  14.321 +apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
  14.322 +apply (simp add: abs_if)
  14.323  apply (auto simp add: linorder_not_less [symmetric])
  14.324  done
  14.325  
  14.326 @@ -301,29 +364,30 @@
  14.327  great as any partial sum.*}
  14.328  
  14.329  lemma series_pos_le: 
  14.330 -     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
  14.331 +     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f"
  14.332  apply (drule summable_sums)
  14.333  apply (simp add: sums_def)
  14.334 -apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
  14.335 -apply (erule LIMSEQ_le, blast) 
  14.336 -apply (rule_tac x = n in exI, clarify) 
  14.337 -apply (drule le_imp_less_or_eq)
  14.338 -apply (auto intro: sumr_le)
  14.339 +apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
  14.340 +apply (erule LIMSEQ_le, blast)
  14.341 +apply (rule_tac x = n in exI, clarify)
  14.342 +apply (rule setsum_mono2)
  14.343 +apply auto
  14.344  done
  14.345  
  14.346  lemma series_pos_less:
  14.347 -     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> sumr 0 n f < suminf f"
  14.348 -apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
  14.349 +     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
  14.350 +apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
  14.351  apply (rule_tac [2] series_pos_le, auto)
  14.352  apply (drule_tac x = m in spec, auto)
  14.353  done
  14.354  
  14.355  text{*Sum of a geometric progression.*}
  14.356  
  14.357 -lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
  14.358 +lemma sumr_geometric:
  14.359 + "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)"
  14.360  apply (induct "n", auto)
  14.361  apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
  14.362 -apply (auto simp add: mult_assoc left_distrib  times_divide_eq)
  14.363 +apply (auto simp add: mult_assoc left_distrib)
  14.364  apply (simp add: right_distrib diff_minus mult_commute)
  14.365  done
  14.366  
  14.367 @@ -339,25 +403,27 @@
  14.368  
  14.369  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
  14.370  
  14.371 -lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
  14.372 +lemma summable_convergent_sumr_iff:
  14.373 + "summable f = convergent (%n. setsum f {0..<n})"
  14.374  by (simp add: summable_def sums_def convergent_def)
  14.375  
  14.376  lemma summable_Cauchy:
  14.377       "summable f =  
  14.378 -      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
  14.379 +      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
  14.380  apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric])
  14.381 -apply (drule_tac [!] spec, auto) 
  14.382 +apply (drule_tac [!] spec, auto)
  14.383  apply (rule_tac x = M in exI)
  14.384  apply (rule_tac [2] x = N in exI, auto)
  14.385  apply (cut_tac [!] m = m and n = n in less_linear, auto)
  14.386  apply (frule le_less_trans [THEN less_imp_le], assumption)
  14.387  apply (drule_tac x = n in spec, simp)
  14.388  apply (drule_tac x = m in spec)
  14.389 -apply(simp add: sumr_split_add_minus)
  14.390 +apply(simp add: setsum_diff[symmetric])
  14.391  apply(subst abs_minus_commute)
  14.392 -apply(simp add: sumr_split_add_minus)
  14.393 -apply (simp add: sumr_split_add_minus)
  14.394 +apply(simp add: setsum_diff[symmetric])
  14.395 +apply(simp add: setsum_diff[symmetric])
  14.396  done
  14.397 +(* FIXME move ivl_ lemmas out of this theory *)
  14.398  
  14.399  text{*Comparison test*}
  14.400  
  14.401 @@ -369,10 +435,10 @@
  14.402  apply (rotate_tac 2)
  14.403  apply (drule_tac x = m in spec)
  14.404  apply (auto, rotate_tac 2, drule_tac x = n in spec)
  14.405 -apply (rule_tac y = "sumr m n (%k. abs (f k))" in order_le_less_trans)
  14.406 +apply (rule_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans)
  14.407  apply (rule setsum_abs)
  14.408 -apply (rule_tac y = "sumr m n g" in order_le_less_trans)
  14.409 -apply (auto intro: sumr_le2 simp add: abs_interval_iff)
  14.410 +apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
  14.411 +apply (auto intro: setsum_mono simp add: abs_interval_iff)
  14.412  done
  14.413  
  14.414  lemma summable_rabs_comparison_test:
  14.415 @@ -389,7 +455,7 @@
  14.416  apply (drule summable_sums)+
  14.417  apply (auto intro!: LIMSEQ_le simp add: sums_def)
  14.418  apply (rule exI)
  14.419 -apply (auto intro!: sumr_le2)
  14.420 +apply (auto intro!: setsum_mono)
  14.421  done
  14.422  
  14.423  lemma summable_le2:
  14.424 @@ -405,7 +471,7 @@
  14.425  apply (drule spec, auto)
  14.426  apply (rule_tac x = N in exI, auto)
  14.427  apply (drule spec, auto)
  14.428 -apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
  14.429 +apply (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
  14.430  apply (auto)
  14.431  done
  14.432  
  14.433 @@ -452,7 +518,7 @@
  14.434  apply (rule_tac x = N in exI, safe)
  14.435  apply (drule le_Suc_ex_iff [THEN iffD1])
  14.436  apply (auto simp add: power_add realpow_not_zero)
  14.437 -apply (induct_tac "na", auto simp add: times_divide_eq)
  14.438 +apply (induct_tac "na", auto)
  14.439  apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
  14.440  apply (auto intro: mult_right_mono simp add: summable_def)
  14.441  apply (simp add: mult_ac)
  14.442 @@ -467,28 +533,20 @@
  14.443  
  14.444  lemma DERIV_sumr [rule_format (no_asm)]:
  14.445       "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
  14.446 -      --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
  14.447 +      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
  14.448  apply (induct "n")
  14.449  apply (auto intro: DERIV_add)
  14.450  done
  14.451  
  14.452  ML
  14.453  {*
  14.454 -val sumr_Suc = thm"sumr_Suc";
  14.455  val sums_def = thm"sums_def";
  14.456  val summable_def = thm"summable_def";
  14.457  val suminf_def = thm"suminf_def";
  14.458  
  14.459 -val sumr_split_add = thm "sumr_split_add";
  14.460  val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
  14.461 -val sumr_le2 = thm "sumr_le2";
  14.462 -val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
  14.463 -val sumr_zero = thm "sumr_zero";
  14.464  val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
  14.465  val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
  14.466 -val sumr_subst = thm "sumr_subst";
  14.467 -val sumr_bound = thm "sumr_bound";
  14.468 -val sumr_bound2 = thm "sumr_bound2";
  14.469  val sumr_group = thm "sumr_group";
  14.470  val sums_summable = thm "sums_summable";
  14.471  val summable_sums = thm "summable_sums";
    15.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Sat Feb 19 18:44:34 2005 +0100
    15.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Feb 21 15:04:10 2005 +0100
    15.3 @@ -75,7 +75,7 @@
    15.4  apply (rule_tac x = u and y = x in linorder_cases)
    15.5  apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less])
    15.6  apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less])
    15.7 -apply (auto simp add: order_less_irrefl)
    15.8 +apply (auto)
    15.9  done
   15.10  
   15.11  lemma real_root_pos2: "0 \<le> x ==> root(Suc n) (x ^ (Suc n)) = x"
   15.12 @@ -100,7 +100,7 @@
   15.13  apply (rule_tac x = u and y = 1 in linorder_cases)
   15.14  apply (drule_tac n = n in realpow_Suc_less_one)
   15.15  apply (drule_tac [4] n = n in power_gt1_lemma)
   15.16 -apply (auto simp add: order_less_irrefl)
   15.17 +apply (auto)
   15.18  done
   15.19  
   15.20  
   15.21 @@ -117,7 +117,7 @@
   15.22  lemma real_sqrt_one [simp]: "sqrt 1 = 1"
   15.23  by (simp add: sqrt_def)
   15.24  
   15.25 -lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
   15.26 +lemma real_sqrt_pow2_iff [iff]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
   15.27  apply (simp add: sqrt_def)
   15.28  apply (rule iffI) 
   15.29   apply (cut_tac r = "root 2 x" in realpow_two_le)
   15.30 @@ -130,7 +130,7 @@
   15.31  by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]])
   15.32  
   15.33  lemma real_sqrt_pow2 [simp]: "0 \<le> x ==> (sqrt x)\<twosuperior> = x"
   15.34 -by (simp add: real_sqrt_pow2_iff)
   15.35 +by (simp)
   15.36  
   15.37  lemma real_sqrt_abs_abs [simp]: "sqrt\<bar>x\<bar> ^ 2 = \<bar>x\<bar>"
   15.38  by (rule real_sqrt_pow2_iff [THEN iffD2], arith)
   15.39 @@ -209,13 +209,13 @@
   15.40  
   15.41  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
   15.42       "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
   15.43 -by (auto simp add: real_sqrt_pow2_iff zero_le_mult_iff simp del: realpow_Suc)
   15.44 +by (auto simp add: zero_le_mult_iff simp del: realpow_Suc)
   15.45  
   15.46  lemma real_sqrt_abs [simp]: "sqrt(x\<twosuperior>) = \<bar>x\<bar>"
   15.47  apply (rule abs_realpow_two [THEN subst])
   15.48  apply (rule real_sqrt_abs_abs [THEN subst])
   15.49  apply (subst real_pow_sqrt_eq_sqrt_pow)
   15.50 -apply (auto simp add: numeral_2_eq_2 abs_mult)
   15.51 +apply (auto simp add: numeral_2_eq_2)
   15.52  done
   15.53  
   15.54  lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \<bar>x\<bar>"
   15.55 @@ -229,7 +229,7 @@
   15.56  
   15.57  lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 0"
   15.58  apply (frule real_sqrt_pow2_gt_zero)
   15.59 -apply (auto simp add: numeral_2_eq_2 order_less_irrefl)
   15.60 +apply (auto simp add: numeral_2_eq_2)
   15.61  done
   15.62  
   15.63  lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
   15.64 @@ -269,21 +269,20 @@
   15.65  apply (cut_tac x = r in reals_Archimedean3, auto)
   15.66  apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
   15.67  apply (rule_tac N = n and c = r in ratio_test)
   15.68 -apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc)
   15.69 +apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
   15.70  apply (rule mult_right_mono)
   15.71  apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
   15.72  apply (subst fact_Suc)
   15.73  apply (subst real_of_nat_mult)
   15.74 -apply (auto simp add: abs_mult inverse_mult_distrib)
   15.75 +apply (auto)
   15.76  apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
   15.77  apply (rule order_less_imp_le)
   15.78  apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
   15.79 -apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse)
   15.80 +apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc)
   15.81  apply (erule order_less_trans)
   15.82  apply (auto simp add: mult_less_cancel_left mult_ac)
   15.83  done
   15.84  
   15.85 -
   15.86  lemma summable_sin: 
   15.87       "summable (%n.  
   15.88             (if even n then 0  
   15.89 @@ -321,10 +320,8 @@
   15.90  by (induct "n", auto)
   15.91  
   15.92  lemma lemma_STAR_cos2 [simp]:
   15.93 -     "sumr 1 n (%n. if even n  
   15.94 -                    then (- 1) ^ (n div 2)/(real (fact n)) *  
   15.95 -                          0 ^ n  
   15.96 -                    else 0) = 0"
   15.97 +  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
   15.98 +                         else 0) = 0"
   15.99  apply (induct "n")
  15.100  apply (case_tac [2] "n", auto)
  15.101  done
  15.102 @@ -364,34 +361,33 @@
  15.103  subsection{*Properties of Power Series*}
  15.104  
  15.105  lemma lemma_realpow_diff_sumr:
  15.106 -     "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =  
  15.107 -      y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
  15.108 -apply (auto simp add: setsum_mult simp del: sumr_Suc)
  15.109 -apply (rule sumr_subst)
  15.110 -apply (intro strip)
  15.111 +     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
  15.112 +      y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
  15.113 +apply (auto simp add: setsum_mult simp del: setsum_Suc)
  15.114 +apply (rule setsum_cong[OF refl])
  15.115  apply (subst lemma_realpow_diff)
  15.116  apply (auto simp add: mult_ac)
  15.117  done
  15.118  
  15.119  lemma lemma_realpow_diff_sumr2:
  15.120       "x ^ (Suc n) - y ^ (Suc n) =  
  15.121 -      (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
  15.122 +      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
  15.123  apply (induct "n", simp)
  15.124 -apply (auto simp del: sumr_Suc)
  15.125 -apply (subst sumr_Suc)
  15.126 +apply (auto simp del: setsum_Suc)
  15.127 +apply (subst setsum_Suc)
  15.128  apply (drule sym)
  15.129 -apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc)
  15.130 +apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_Suc)
  15.131  done
  15.132  
  15.133  lemma lemma_realpow_rev_sumr:
  15.134 -     "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =  
  15.135 -      sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"
  15.136 +     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
  15.137 +      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
  15.138  apply (case_tac "x = y")
  15.139 -apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc)
  15.140 +apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_Suc)
  15.141  apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
  15.142  apply (rule_tac [2] minus_minus [THEN subst], simp)
  15.143  apply (subst minus_mult_left)
  15.144 -apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: sumr_Suc)
  15.145 +apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_Suc)
  15.146  done
  15.147  
  15.148  text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
  15.149 @@ -412,7 +408,7 @@
  15.150  apply (auto simp add: mult_assoc power_abs)
  15.151   prefer 2
  15.152   apply (drule_tac x = 0 in spec, force)
  15.153 -apply (auto simp add: abs_mult power_abs mult_ac)
  15.154 +apply (auto simp add: power_abs mult_ac)
  15.155  apply (rule_tac a2 = "z ^ n" 
  15.156         in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
  15.157  apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
  15.158 @@ -423,8 +419,7 @@
  15.159  apply (subgoal_tac "x \<noteq> 0")
  15.160  apply (subgoal_tac [3] "x \<noteq> 0")
  15.161  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])
  15.162 -apply (auto intro!: geometric_sums 
  15.163 -            simp add: power_abs inverse_eq_divide times_divide_eq)
  15.164 +apply (auto intro!: geometric_sums  simp add: power_abs inverse_eq_divide)
  15.165  done
  15.166  
  15.167  lemma powser_inside:
  15.168 @@ -443,16 +438,16 @@
  15.169  
  15.170  text{*Show that we can shift the terms down one*}
  15.171  lemma lemma_diffs:
  15.172 -     "sumr 0 n (%n. (diffs c)(n) * (x ^ n)) =  
  15.173 -      sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) +  
  15.174 +     "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) =  
  15.175 +      (\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) +  
  15.176        (real n * c(n) * x ^ (n - Suc 0))"
  15.177  apply (induct "n")
  15.178  apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
  15.179  done
  15.180  
  15.181  lemma lemma_diffs2:
  15.182 -     "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =  
  15.183 -      sumr 0 n (%n. (diffs c)(n) * (x ^ n)) -  
  15.184 +     "(\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) =  
  15.185 +      (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) -  
  15.186        (real n * c(n) * x ^ (n - Suc 0))"
  15.187  by (auto simp add: lemma_diffs)
  15.188  
  15.189 @@ -474,10 +469,9 @@
  15.190  subsection{*Term-by-Term Differentiability of Power Series*}
  15.191  
  15.192  lemma lemma_termdiff1:
  15.193 -     "sumr 0 m (%p. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
  15.194 -        sumr 0 m (%p. (z ^ p) *  
  15.195 -        (((z + h) ^ (m - p)) - (z ^ (m - p))))"
  15.196 -apply (rule sumr_subst)
  15.197 +  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
  15.198 +   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
  15.199 +apply (rule setsum_cong[OF refl])
  15.200  apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac)
  15.201  done
  15.202  
  15.203 @@ -489,54 +483,59 @@
  15.204  
  15.205  
  15.206  lemma lemma_termdiff2:
  15.207 -     " h \<noteq> 0 ==>  
  15.208 -        (((z + h) ^ n) - (z ^ n)) * inverse h -  
  15.209 -            real n * (z ^ (n - Suc 0)) =  
  15.210 -         h * sumr 0 (n - Suc 0) (%p. (z ^ p) *  
  15.211 -               sumr 0 ((n - Suc 0) - p)  
  15.212 -                 (%q. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))"
  15.213 +  "h \<noteq> 0 ==>
  15.214 +   (((z + h) ^ n) - (z ^ n)) * inverse h - real n * (z ^ (n - Suc 0)) =
  15.215 +   h * (\<Sum>p=0..< n - Suc 0. (z ^ p) *
  15.216 +       (\<Sum>q=0..< (n - Suc 0) - p. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))"
  15.217  apply (rule real_mult_left_cancel [THEN iffD1], simp (no_asm_simp))
  15.218  apply (simp add: right_diff_distrib mult_ac)
  15.219  apply (simp add: mult_assoc [symmetric])
  15.220  apply (case_tac "n")
  15.221  apply (auto simp add: lemma_realpow_diff_sumr2 
  15.222                        right_diff_distrib [symmetric] mult_assoc
  15.223 -            simp del: realpow_Suc sumr_Suc)
  15.224 -apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
  15.225 +            simp del: realpow_Suc setsum_Suc)
  15.226 +apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_Suc)
  15.227  apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
  15.228                  sumdiff lemma_termdiff1 setsum_mult)
  15.229 -apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
  15.230 -apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
  15.231 +apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
  15.232 +apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
  15.233  apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
  15.234 -                 del: sumr_Suc realpow_Suc)
  15.235 +                 del: setsum_Suc realpow_Suc)
  15.236  done
  15.237  
  15.238 +(* FIXME move *)
  15.239 +lemma sumr_bound2 [rule_format (no_asm)]:
  15.240 +     "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
  15.241 +      --> setsum f {0..<n::nat} \<le> (real n * K)"
  15.242 +using setsum_bounded[where A = "{0..<n}"]
  15.243 +by (auto simp:real_of_nat_def)
  15.244 +
  15.245  lemma lemma_termdiff3:
  15.246       "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
  15.247        ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
  15.248            \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
  15.249  apply (subst lemma_termdiff2, assumption)
  15.250 -apply (simp add: abs_mult mult_commute) 
  15.251 +apply (simp add: mult_commute) 
  15.252  apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) 
  15.253  apply (rule setsum_abs [THEN real_le_trans])
  15.254  apply (simp add: mult_assoc [symmetric])
  15.255  apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
  15.256 -apply (auto intro!: sumr_bound2 simp add: abs_mult)
  15.257 +apply (auto intro!: sumr_bound2)
  15.258  apply (case_tac "n", auto)
  15.259  apply (drule less_add_one)
  15.260  (*CLAIM_SIMP " (a * b * c = a * (c * (b::real))" mult_ac]*)
  15.261  apply clarify 
  15.262  apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) =
  15.263                      K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") 
  15.264 -apply (simp (no_asm_simp) add: power_add del: sumr_Suc)
  15.265 -apply (auto intro!: mult_mono simp del: sumr_Suc)
  15.266 -apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc)
  15.267 +apply (simp (no_asm_simp) add: power_add del: setsum_Suc)
  15.268 +apply (auto intro!: mult_mono simp del: setsum_Suc)
  15.269 +apply (auto intro!: power_mono simp add: power_abs simp del: setsum_Suc)
  15.270  apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
  15.271  apply (subgoal_tac [2] "0 \<le> K")
  15.272  apply (drule_tac [2] n = d in zero_le_power)
  15.273 -apply (auto simp del: sumr_Suc)
  15.274 +apply (auto simp del: setsum_Suc)
  15.275  apply (rule setsum_abs [THEN real_le_trans])
  15.276 -apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add)
  15.277 +apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
  15.278  apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
  15.279  done
  15.280  
  15.281 @@ -910,7 +909,7 @@
  15.282    hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
  15.283      by (auto simp add: exp_add exp_minus)
  15.284    thus ?thesis
  15.285 -    by (simp add: divide_inverse [symmetric] pos_less_divide_eq times_divide_eq
  15.286 +    by (simp add: divide_inverse [symmetric] pos_less_divide_eq
  15.287               del: divide_self_if)
  15.288  qed
  15.289  
  15.290 @@ -1067,7 +1066,8 @@
  15.291  by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
  15.292           simp add: sin_def sums_def simp del: power_0_left)
  15.293  
  15.294 -lemma lemma_series_zero2: "(\<forall>m. n \<le> m --> f m = 0) --> f sums sumr 0 n f"
  15.295 +lemma lemma_series_zero2:
  15.296 + "(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"
  15.297  by (auto intro: series_zero)
  15.298  
  15.299  lemma cos_zero [simp]: "cos 0 = 1"
  15.300 @@ -1237,7 +1237,6 @@
  15.301                      DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
  15.302                      DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
  15.303                      DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
  15.304 -                    DERIV_Id DERIV_const DERIV_cos
  15.305  
  15.306  (* lemma *)
  15.307  lemma lemma_DERIV_sin_cos_add:
  15.308 @@ -1361,9 +1360,8 @@
  15.309  apply (case_tac "m=0")
  15.310  apply (simp (no_asm_simp))
  15.311  apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x") 
  15.312 -apply (simp only: mult_less_cancel_left, simp add: times_divide_eq)  
  15.313 -apply (simp (no_asm_simp) add: times_divide_eq 
  15.314 -               numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
  15.315 +apply (simp only: mult_less_cancel_left, simp)  
  15.316 +apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
  15.317  apply (subgoal_tac "x*x < 2*3", simp) 
  15.318  apply (rule mult_strict_mono)
  15.319  apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
  15.320 @@ -1375,7 +1373,7 @@
  15.321  apply (subst real_of_nat_mult)
  15.322  apply (subst real_of_nat_mult)
  15.323  apply (subst real_of_nat_mult)
  15.324 -apply (simp (no_asm) add: divide_inverse inverse_mult_distrib del: fact_Suc)
  15.325 +apply (simp (no_asm) add: divide_inverse del: fact_Suc)
  15.326  apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
  15.327  apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
  15.328  apply (auto simp add: mult_assoc simp del: fact_Suc)
  15.329 @@ -1422,12 +1420,12 @@
  15.330  apply (cut_tac x = 2 in cos_paired)
  15.331  apply (drule sums_minus)
  15.332  apply (rule neg_less_iff_less [THEN iffD1]) 
  15.333 -apply (frule sums_unique, auto simp add: times_divide_eq)
  15.334 -apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) 
  15.335 -                      (%n. - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n)))" 
  15.336 +apply (frule sums_unique, auto)
  15.337 +apply (rule_tac y =
  15.338 + "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
  15.339         in order_less_trans)
  15.340  apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
  15.341 -apply (simp (no_asm) add: mult_assoc times_divide_eq del: sumr_Suc)
  15.342 +apply (simp (no_asm) add: mult_assoc del: setsum_Suc)
  15.343  apply (rule sumr_pos_lt_pair)
  15.344  apply (erule sums_summable, safe)
  15.345  apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
  15.346 @@ -1520,10 +1518,10 @@
  15.347  done
  15.348  
  15.349  lemma cos_pi [simp]: "cos pi = -1"
  15.350 -by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp add: times_divide_eq)
  15.351 +by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp)
  15.352  
  15.353  lemma sin_pi [simp]: "sin pi = 0"
  15.354 -by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp add: times_divide_eq)
  15.355 +by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
  15.356  
  15.357  lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
  15.358  by (simp add: diff_minus cos_add)
  15.359 @@ -1706,7 +1704,7 @@
  15.360  apply (cut_tac x="-x" in cos_zero_lemma, simp, simp) 
  15.361  apply (force simp add: minus_equation_iff [of x]) 
  15.362  apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib) 
  15.363 -apply (auto simp add: cos_add times_divide_eq)
  15.364 +apply (auto simp add: cos_add)
  15.365  done
  15.366  
  15.367  (* ditto: but to a lesser extent *)
  15.368 @@ -1719,7 +1717,7 @@
  15.369  apply (drule sin_zero_lemma, assumption+)
  15.370  apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
  15.371  apply (force simp add: minus_equation_iff [of x]) 
  15.372 -apply (auto simp add: even_mult_two_ex times_divide_eq)
  15.373 +apply (auto simp add: even_mult_two_ex)
  15.374  done
  15.375  
  15.376  
  15.377 @@ -1757,7 +1755,7 @@
  15.378  apply (simp add: tan_def)
  15.379  apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
  15.380  apply (auto simp add: mult_assoc left_distrib)
  15.381 -apply (simp add: sin_add times_divide_eq)
  15.382 +apply (simp add: sin_add)
  15.383  done
  15.384  
  15.385  lemma tan_add:
  15.386 @@ -2068,7 +2066,7 @@
  15.387  by (rule DERIV_exp [THEN DERIV_isCont])
  15.388  
  15.389  lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
  15.390 -by (auto simp add: sin_zero_iff even_mult_two_ex times_divide_eq)
  15.391 +by (auto simp add: sin_zero_iff even_mult_two_ex)
  15.392  
  15.393  lemma exp_eq_one_iff [simp]: "(exp x = 1) = (x = 0)"
  15.394  apply auto
  15.395 @@ -2185,7 +2183,7 @@
  15.396  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
  15.397  apply (simp add: divide_inverse)
  15.398  apply (case_tac "r=0")
  15.399 -apply (auto simp add: inverse_mult_distrib mult_ac)
  15.400 +apply (auto simp add: mult_ac)
  15.401  done
  15.402  
  15.403  
  15.404 @@ -2456,7 +2454,7 @@
  15.405  apply (rule order_less_le_trans [of _ "7/5"], simp) 
  15.406  apply (rule_tac n = 1 in realpow_increasing)
  15.407    prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
  15.408 -apply (simp_all add: numeral_2_eq_2 times_divide_eq)
  15.409 +apply (simp_all add: numeral_2_eq_2)
  15.410  done
  15.411  
  15.412  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
    16.1 --- a/src/HOL/Integ/IntDef.thy	Sat Feb 19 18:44:34 2005 +0100
    16.2 +++ b/src/HOL/Integ/IntDef.thy	Mon Feb 21 15:04:10 2005 +0100
    16.3 @@ -559,80 +559,6 @@
    16.4  by (simp add: linorder_not_less neg_def)
    16.5  
    16.6  
    16.7 -subsection{*Embedding of the Naturals into any @{text
    16.8 -comm_semiring_1_cancel}: @{term of_nat}*}
    16.9 -
   16.10 -consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
   16.11 -
   16.12 -primrec
   16.13 -  of_nat_0:   "of_nat 0 = 0"
   16.14 -  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
   16.15 -
   16.16 -lemma of_nat_1 [simp]: "of_nat 1 = 1"
   16.17 -by simp
   16.18 -
   16.19 -lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   16.20 -apply (induct m)
   16.21 -apply (simp_all add: add_ac)
   16.22 -done
   16.23 -
   16.24 -lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
   16.25 -apply (induct m)
   16.26 -apply (simp_all add: mult_ac add_ac right_distrib)
   16.27 -done
   16.28 -
   16.29 -lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   16.30 -apply (induct m, simp_all)
   16.31 -apply (erule order_trans)
   16.32 -apply (rule less_add_one [THEN order_less_imp_le])
   16.33 -done
   16.34 -
   16.35 -lemma less_imp_of_nat_less:
   16.36 -     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   16.37 -apply (induct m n rule: diff_induct, simp_all)
   16.38 -apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
   16.39 -done
   16.40 -
   16.41 -lemma of_nat_less_imp_less:
   16.42 -     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
   16.43 -apply (induct m n rule: diff_induct, simp_all)
   16.44 -apply (insert zero_le_imp_of_nat)
   16.45 -apply (force simp add: linorder_not_less [symmetric])
   16.46 -done
   16.47 -
   16.48 -lemma of_nat_less_iff [simp]:
   16.49 -     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
   16.50 -by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
   16.51 -
   16.52 -text{*Special cases where either operand is zero*}
   16.53 -declare of_nat_less_iff [of 0, simplified, simp]
   16.54 -declare of_nat_less_iff [of _ 0, simplified, simp]
   16.55 -
   16.56 -lemma of_nat_le_iff [simp]:
   16.57 -     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
   16.58 -by (simp add: linorder_not_less [symmetric])
   16.59 -
   16.60 -text{*Special cases where either operand is zero*}
   16.61 -declare of_nat_le_iff [of 0, simplified, simp]
   16.62 -declare of_nat_le_iff [of _ 0, simplified, simp]
   16.63 -
   16.64 -text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
   16.65 -to exclude the possibility of a finite field, which indeed wraps back to
   16.66 -zero.*}
   16.67 -lemma of_nat_eq_iff [simp]:
   16.68 -     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
   16.69 -by (simp add: order_eq_iff)
   16.70 -
   16.71 -text{*Special cases where either operand is zero*}
   16.72 -declare of_nat_eq_iff [of 0, simplified, simp]
   16.73 -declare of_nat_eq_iff [of _ 0, simplified, simp]
   16.74 -
   16.75 -lemma of_nat_diff [simp]:
   16.76 -     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
   16.77 -by (simp del: of_nat_add
   16.78 -	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   16.79 -
   16.80 -
   16.81  subsection{*The Set of Natural Numbers*}
   16.82  
   16.83  constdefs
    17.1 --- a/src/HOL/Nat.thy	Sat Feb 19 18:44:34 2005 +0100
    17.2 +++ b/src/HOL/Nat.thy	Mon Feb 21 15:04:10 2005 +0100
    17.3 @@ -1022,4 +1022,5 @@
    17.4    apply (fastsimp dest: mult_less_mono2)
    17.5    done
    17.6  
    17.7 +
    17.8  end
    18.1 --- a/src/HOL/NatArith.thy	Sat Feb 19 18:44:34 2005 +0100
    18.2 +++ b/src/HOL/NatArith.thy	Mon Feb 21 15:04:10 2005 +0100
    18.3 @@ -162,5 +162,78 @@
    18.4  val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
    18.5  *}
    18.6  
    18.7 +subsection{*Embedding of the Naturals into any @{text
    18.8 +comm_semiring_1_cancel}: @{term of_nat}*}
    18.9 +
   18.10 +consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
   18.11 +
   18.12 +primrec
   18.13 +  of_nat_0:   "of_nat 0 = 0"
   18.14 +  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
   18.15 +
   18.16 +lemma of_nat_1 [simp]: "of_nat 1 = 1"
   18.17 +by simp
   18.18 +
   18.19 +lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
   18.20 +apply (induct m)
   18.21 +apply (simp_all add: add_ac)
   18.22 +done
   18.23 +
   18.24 +lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
   18.25 +apply (induct m)
   18.26 +apply (simp_all add: mult_ac add_ac right_distrib)
   18.27 +done
   18.28 +
   18.29 +lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
   18.30 +apply (induct m, simp_all)
   18.31 +apply (erule order_trans)
   18.32 +apply (rule less_add_one [THEN order_less_imp_le])
   18.33 +done
   18.34 +
   18.35 +lemma less_imp_of_nat_less:
   18.36 +     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
   18.37 +apply (induct m n rule: diff_induct, simp_all)
   18.38 +apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
   18.39 +done
   18.40 +
   18.41 +lemma of_nat_less_imp_less:
   18.42 +     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
   18.43 +apply (induct m n rule: diff_induct, simp_all)
   18.44 +apply (insert zero_le_imp_of_nat)
   18.45 +apply (force simp add: linorder_not_less [symmetric])
   18.46 +done
   18.47 +
   18.48 +lemma of_nat_less_iff [simp]:
   18.49 +     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
   18.50 +by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
   18.51 +
   18.52 +text{*Special cases where either operand is zero*}
   18.53 +declare of_nat_less_iff [of 0, simplified, simp]
   18.54 +declare of_nat_less_iff [of _ 0, simplified, simp]
   18.55 +
   18.56 +lemma of_nat_le_iff [simp]:
   18.57 +     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
   18.58 +by (simp add: linorder_not_less [symmetric])
   18.59 +
   18.60 +text{*Special cases where either operand is zero*}
   18.61 +declare of_nat_le_iff [of 0, simplified, simp]
   18.62 +declare of_nat_le_iff [of _ 0, simplified, simp]
   18.63 +
   18.64 +text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
   18.65 +to exclude the possibility of a finite field, which indeed wraps back to
   18.66 +zero.*}
   18.67 +lemma of_nat_eq_iff [simp]:
   18.68 +     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
   18.69 +by (simp add: order_eq_iff)
   18.70 +
   18.71 +text{*Special cases where either operand is zero*}
   18.72 +declare of_nat_eq_iff [of 0, simplified, simp]
   18.73 +declare of_nat_eq_iff [of _ 0, simplified, simp]
   18.74 +
   18.75 +lemma of_nat_diff [simp]:
   18.76 +     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
   18.77 +by (simp del: of_nat_add
   18.78 +	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
   18.79 +
   18.80  
   18.81  end
    19.1 --- a/src/HOL/OrderedGroup.thy	Sat Feb 19 18:44:34 2005 +0100
    19.2 +++ b/src/HOL/OrderedGroup.thy	Mon Feb 21 15:04:10 2005 +0100
    19.3 @@ -319,6 +319,11 @@
    19.4    shows  "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
    19.5  by (insert add_mono [of 0 a b c], simp)
    19.6  
    19.7 +lemma add_increasing2:
    19.8 +  fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
    19.9 +  shows  "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"
   19.10 +by (simp add:add_increasing add_commute[of a])
   19.11 +
   19.12  lemma add_strict_increasing:
   19.13    fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   19.14    shows "[|0<a; b\<le>c|] ==> b < a + c"
   19.15 @@ -806,7 +811,7 @@
   19.16  lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::lordered_ab_group_abs))"
   19.17  by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
   19.18  
   19.19 -lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::lordered_ab_group_abs)"
   19.20 +lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
   19.21  proof -
   19.22    have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
   19.23      apply (simp add: abs_lattice add_meet_join_distribs join_aci)
   19.24 @@ -829,6 +834,17 @@
   19.25    finally show ?thesis .
   19.26  qed
   19.27  
   19.28 +lemma abs_add_abs[simp]:
   19.29 +fixes a:: "'a::{lordered_ab_group_abs}"
   19.30 +shows "abs(abs a + abs b) = abs a + abs b" (is "?L = ?R")
   19.31 +proof (rule order_antisym)
   19.32 +  show "?L \<ge> ?R" by(rule abs_ge_self)
   19.33 +next
   19.34 +  have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
   19.35 +  also have "\<dots> = ?R" by simp
   19.36 +  finally show "?L \<le> ?R" .
   19.37 +qed
   19.38 +
   19.39  text {* Needed for abelian cancellation simprocs: *}
   19.40  
   19.41  lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
    20.1 --- a/src/HOL/Real/RComplete.thy	Sat Feb 19 18:44:34 2005 +0100
    20.2 +++ b/src/HOL/Real/RComplete.thy	Mon Feb 21 15:04:10 2005 +0100
    20.3 @@ -389,7 +389,7 @@
    20.4  lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
    20.5  apply (rule inj_int [THEN injD])
    20.6  apply (simp add: real_of_nat_Suc)
    20.7 -apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"])
    20.8 +apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
    20.9  done
   20.10  
   20.11  lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
   20.12 @@ -532,7 +532,3 @@
   20.13  
   20.14  
   20.15  end
   20.16 -
   20.17 -
   20.18 -
   20.19 -
    21.1 --- a/src/HOL/SetInterval.thy	Sat Feb 19 18:44:34 2005 +0100
    21.2 +++ b/src/HOL/SetInterval.thy	Mon Feb 21 15:04:10 2005 +0100
    21.3 @@ -589,6 +589,22 @@
    21.4  lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
    21.5  by (simp add:lessThan_Suc)
    21.6  
    21.7 +lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
    21.8 +  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
    21.9 +by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
   21.10 +
   21.11 +lemma setsum_diff_nat_ivl:
   21.12 +fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
   21.13 +shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
   21.14 +  setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
   21.15 +using setsum_add_nat_ivl [of m n p f,symmetric]
   21.16 +apply (simp add: add_ac)
   21.17 +done
   21.18 +
   21.19 +lemma setsum_shift_bounds_nat_ivl:
   21.20 +  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
   21.21 +by (induct "n", auto simp:atLeastLessThanSuc)
   21.22 +
   21.23  
   21.24  ML
   21.25  {*