# HG changeset patch
# User paulson
# Date 976708035 -3600
# Node ID fb08faea465d5162abd65ee3c2f629c04a30de1d
# Parent  cf6be18049122577c4be6127014a57942363b8eb
tidying

diff -r cf6be1804912 -r fb08faea465d src/HOL/Real/Hyperreal/Series.ML
--- a/src/HOL/Real/Hyperreal/Series.ML	Wed Dec 13 12:46:47 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML	Wed Dec 13 12:47:15 2000 +0100
@@ -46,7 +46,7 @@
     leI] addDs [le_anti_sym], simpset()));
 qed_spec_mp "sumr_split_add";
 
-Goal "!!n. n < p ==> sumr 0 p f + \
+Goal "n < p ==> sumr 0 p f + \
 \                - sumr 0 n f = sumr n p f";
 by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1);
 by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
@@ -76,7 +76,7 @@
     real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1);
 qed "sumr_add_mult_const";
 
-goalw Series.thy [real_diff_def] 
+Goalw [real_diff_def] 
      "sumr 0 n f - (real_of_nat n*r) = sumr 0 n (%i. f i - r)";
 by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1);
 qed "sumr_diff_mult_const";
@@ -94,14 +94,6 @@
     [real_minus_add_distrib]));
 qed "sumr_minus";
 
-context NatArith.thy;
-
-Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
-by (auto_tac (claset() addSDs [not_leE], simpset()));
-qed "lemma_not_Suc_add";
-
-context thy;
-
 Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))";
 by (induct_tac "n" 1);
 by (Auto_tac);
@@ -178,20 +170,22 @@
 
 Goal "(ALL n. #0 <= f n) --> #0 <= sumr m n f";
 by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps 
-    [rename_numerals real_le_add_order]));
+by Auto_tac;
+by (dres_inst_tac [("x","n")] spec 1);
+by (arith_tac 1);
 qed_spec_mp "sumr_ge_zero";
 
 Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [rename_numerals real_le_add_order] 
-    addDs [leI], simpset()));
+by Auto_tac;
+by (dres_inst_tac [("x","n")] spec 1);
+by (arith_tac 1);
 qed_spec_mp "sumr_ge_zero2";
 
 Goal "#0 <= sumr m n (%n. abs (f n))";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addSIs [rename_numerals real_le_add_order,
-    abs_ge_zero], simpset()));
+by Auto_tac;
+by (arith_tac 1);
 qed "sumr_rabs_ge_zero";
 Addsimps [sumr_rabs_ge_zero];
 AddSIs [sumr_rabs_ge_zero]; 
@@ -279,32 +273,32 @@
    suminf is the sum   
  ---------------------*)
 Goalw [sums_def,summable_def] 
-      "!!f. f sums l ==> summable f";
+      "f sums l ==> summable f";
 by (Blast_tac 1);
 qed "sums_summable";
 
 Goalw [summable_def,suminf_def]
-     "!!f. summable f ==> f sums (suminf f)";
+     "summable f ==> f sums (suminf f)";
 by (blast_tac (claset() addIs [someI2]) 1);
 qed "summable_sums";
 
 Goalw [summable_def,suminf_def,sums_def]
-     "!!f. summable f ==> (%n. sumr 0 n f) ----> (suminf f)";
+     "summable f ==> (%n. sumr 0 n f) ----> (suminf f)";
 by (blast_tac (claset() addIs [someI2]) 1);
 qed "summable_sumr_LIMSEQ_suminf";
 
 (*-------------------
     sum is unique                    
  ------------------*)
-Goal "!!f. f sums s ==> (s = suminf f)";
+Goal "f sums s ==> (s = suminf f)";
 by (forward_tac [sums_summable RS summable_sums] 1);
 by (auto_tac (claset() addSIs [LIMSEQ_unique],
     simpset() addsimps [sums_def]));
 qed "sums_unique";
 
+(*
 Goalw [sums_def,LIMSEQ_def] 
-     "!!f. ALL m. n <= Suc m --> f(m) = #0 \
-\                ==> f sums (sumr 0 n f)";
+     "(ALL m. n <= Suc m --> f(m) = #0) ==> f sums (sumr 0 n f)";
 by (Step_tac 1);
 by (res_inst_tac [("x","n")] exI 1);
 by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1);
@@ -314,10 +308,11 @@
 by (dtac (conjI RS sumr_interval_const) 1);
 by (Auto_tac);
 qed "series_zero";
+next one was called series_zero2
+**********************)
 
-goalw Series.thy [sums_def,LIMSEQ_def] 
-     "!!f. ALL m. n <= m --> f(m) = #0 \
-\                ==> f sums (sumr 0 n f)";
+Goalw [sums_def,LIMSEQ_def] 
+     "(ALL m. n <= m --> f(m) = #0) ==> f sums (sumr 0 n f)";
 by (Step_tac 1);
 by (res_inst_tac [("x","n")] exI 1);
 by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1);
@@ -326,7 +321,7 @@
 by (ALLGOALS (Asm_simp_tac));
 by (dtac (conjI RS sumr_interval_const2) 1);
 by (Auto_tac);
-qed "series_zero2";
+qed "series_zero";
 
 Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)";
 by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], 
@@ -338,12 +333,12 @@
     simpset() addsimps [sumr_diff RS sym]));
 qed "sums_diff";
 
-goal Series.thy "!!f. summable f ==> suminf f * c = suminf(%n. f n * c)";
+Goal "summable f ==> suminf f * c = suminf(%n. f n * c)";
 by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums],
     simpset() addsimps [real_mult_commute]));
 qed "suminf_mult";
 
-goal Series.thy "!!f. summable f ==> c * suminf f  = suminf(%n. c * f n)";
+Goal "summable f ==> c * suminf f  = suminf(%n. c * f n)";
 by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums],
     simpset()));
 qed "suminf_mult2";
@@ -353,8 +348,8 @@
 by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums], simpset()));
 qed "suminf_diff";
 
-goalw Series.thy [sums_def] 
-       "!!x. x sums x0 ==> (%n. - x n) sums - x0";
+Goalw [sums_def] 
+       "x sums x0 ==> (%n. - x n) sums - x0";
 by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus]));
 qed "sums_minus";
 
@@ -408,7 +403,7 @@
    Summable series of positive terms has limit >= any partial sum 
  ----------------------------------------------------------------*)
 Goal 
-     "!!f. [| summable f; ALL m. n <= m --> #0 <= f(m) |] \
+     "[| summable f; ALL m. n <= m --> #0 <= f(m) |] \
 \          ==> sumr 0 n f <= suminf f";
 by (dtac summable_sums 1);
 by (rewtac sums_def);
@@ -419,7 +414,7 @@
 by (auto_tac (claset() addIs [sumr_le], simpset()));
 qed "series_pos_le";
 
-Goal "!!f. [| summable f; ALL m. n <= m --> #0 < f(m) |] \
+Goal "[| summable f; ALL m. n <= m --> #0 < f(m) |] \
 \          ==> sumr 0 n f < suminf f";
 by (res_inst_tac [("j","sumr 0 (Suc n) f")] real_less_le_trans 1);
 by (rtac series_pos_le 2);
@@ -433,19 +428,16 @@
  -------------------------------------------------------------------*)
 (* lemma *)
 
-Goalw [real_diff_def] "x ~= y ==> x - y ~= (#0::real)";
-by (asm_full_simp_tac (simpset() addsimps 
-   [rename_numerals (real_eq_minus_iff2 RS sym)]) 1);
-qed "real_not_eq_diff";
-
 Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * inverse(x - #1)";
 by (induct_tac "n" 1);
 by (Auto_tac);
 by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [real_not_eq_diff,
-    real_eq_minus_iff2 RS sym,real_mult_assoc,real_add_mult_distrib]));
-by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
-    real_diff_def,real_mult_commute]) 1);
+by (auto_tac (claset(),
+       simpset() addsimps [real_eq_minus_iff2 RS sym,
+                           real_mult_assoc, real_add_mult_distrib]));
+by (auto_tac (claset(),
+       simpset() addsimps [real_add_mult_distrib2,
+                           real_diff_def, real_mult_commute]));
 qed "sumr_geometric";
 
 Goal "abs(x) < #1 ==> (%n. x ^ n) sums inverse(#1 - x)";
@@ -456,7 +448,6 @@
 by (rtac (real_add_zero_left RS subst) 1);
 by (rtac (real_mult_0 RS subst) 1);
 by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1);
-by (dtac real_not_eq_diff 3);
 by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps 
     [real_minus_inverse RS sym,real_diff_def,real_add_commute,
      rename_numerals LIMSEQ_rabs_realpow_zero2]));
@@ -592,7 +583,7 @@
 by (auto_tac (claset(),simpset() addsimps [le_Suc_ex]));
 qed "le_Suc_ex_iff";
 
-Goal "!!c. [| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
+Goal "[| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \
 \     ==> summable f";
 by (subgoal_tac "c <= #0 | #0 < c" 1 THEN Auto_tac);
 by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
@@ -627,9 +618,3 @@
 by (induct_tac "n" 1);
 by (auto_tac (claset() addIs [DERIV_add], simpset()));
 qed "DERIV_sumr";
-
-
-
-
-
-