# HG changeset patch
# User paulson
# Date 975664975 -3600
# Node ID 09a91221ced1a18036c1d635d070ac83fe34e18b
# Parent  dc615fccc1e6e606b595110e01cd01e13a0d8a6f
renamed less_eq_Suc_add to less_imp_Suc_add

diff -r dc615fccc1e6 -r 09a91221ced1 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Thu Nov 30 20:18:00 2000 +0100
+++ b/src/HOL/Integ/IntDef.ML	Fri Dec 01 11:02:55 2000 +0100
@@ -351,7 +351,7 @@
 by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
 by (Clarify_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
-by (safe_tac (claset() addSDs [less_eq_Suc_add]));
+by (safe_tac (claset() addSDs [less_imp_Suc_add]));
 by (res_inst_tac [("x","k")] exI 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
 qed "zless_iff_Suc_zadd";
diff -r dc615fccc1e6 -r 09a91221ced1 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu Nov 30 20:18:00 2000 +0100
+++ b/src/HOL/Nat.ML	Fri Dec 01 11:02:55 2000 +0100
@@ -265,13 +265,13 @@
 
 (**** Additional theorems about "less than" ****)
 
-(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
+(*Deleted less_natE; instead use less_imp_Suc_add RS exE*)
 Goal "m<n --> (EX k. n=Suc(m+k))";
 by (induct_tac "n" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
 by (blast_tac (claset() addSEs [less_SucE]
                         addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
-qed_spec_mp "less_eq_Suc_add";
+qed_spec_mp "less_imp_Suc_add";
 
 Goal "n <= ((m + n)::nat)";
 by (induct_tac "m" 1);
@@ -288,7 +288,7 @@
 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
 
 Goal "(m<n) = (EX k. n=Suc(m+k))";
-by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
+by (blast_tac (claset() addSIs [less_add_Suc1, less_imp_Suc_add]) 1);
 qed "less_iff_Suc_add";
 
 
@@ -634,7 +634,7 @@
 
 (*strict, in 1st argument; proof is by induction on k>0*)
 Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
-by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
+by (eres_inst_tac [("m1","0")] (less_imp_Suc_add RS exE) 1);
 by (Asm_simp_tac 1);
 by (induct_tac "x" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
diff -r dc615fccc1e6 -r 09a91221ced1 src/HOL/Real/Hyperreal/SEQ.ML
--- a/src/HOL/Real/Hyperreal/SEQ.ML	Thu Nov 30 20:18:00 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML	Fri Dec 01 11:02:55 2000 +0100
@@ -120,7 +120,7 @@
 by (induct_tac "u" 1);
 by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2]));
 by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset),
-    finite_nat_le_segment],simpset()));
+    finite_nat_le_segment], simpset()));
 by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1);
 by (ALLGOALS(Asm_simp_tac));
 qed "NSLIMSEQ_finite_set";
@@ -153,7 +153,7 @@
 Goal "{n. abs (X (f n) + - L) < r} Int \
 \         {n. r <= abs (X (f n) + - (L::real))} = {}";
 by (auto_tac (claset() addDs [real_less_le_trans] 
-    addIs [real_less_irrefl],simpset()));
+    addIs [real_less_irrefl], simpset()));
 val lemmaLIM2 = result();
 
 Goal "!!f. [| #0 < r; ALL n. r <= abs (X (f n) + - L); \
@@ -323,7 +323,7 @@
       "!!X. [| X ----NS> a; X ----NS> b |] \
 \           ==> a = b";
 by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
-by (auto_tac (claset() addDs [inf_close_trans3],simpset()));
+by (auto_tac (claset() addDs [inf_close_trans3], simpset()));
 qed "NSLIMSEQ_unique";
 
 Goal "!!X. [| X ----> a; X ----> b |] \
@@ -377,21 +377,21 @@
 
 Goalw [NSconvergent_def,nslim_def] 
       "NSconvergent X = (X ----NS> nslim X)";
-by (auto_tac (claset() addIs [someI],simpset()));
+by (auto_tac (claset() addIs [someI], simpset()));
 qed "NSconvergent_NSLIMSEQ_iff";
 
 Goalw [convergent_def,lim_def] 
       "convergent X = (X ----> lim X)";
-by (auto_tac (claset() addIs [someI],simpset()));
+by (auto_tac (claset() addIs [someI], simpset()));
 qed "convergent_LIMSEQ_iff";
 
 (*-------------------------------------------------------------------
          Subsequence (alternative definition) (e.g. Hoskins)
  ------------------------------------------------------------------*)
 Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))";
-by (auto_tac (claset() addSDs [less_eq_Suc_add],simpset()));
+by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset()));
 by (nat_ind_tac "k" 1);
-by (auto_tac (claset() addIs [less_trans],simpset()));
+by (auto_tac (claset() addIs [less_trans], simpset()));
 qed "subseq_Suc_iff";
 
 (*-------------------------------------------------------------------
@@ -403,13 +403,14 @@
 \                | (ALL n. X (Suc n) <= X n))";
 by (auto_tac (claset () addSDs [le_imp_less_or_eq],
     simpset() addsimps [real_le_refl]));
-by (auto_tac (claset() addSIs [lessI RS less_imp_le] 
-    addSDs [less_eq_Suc_add],simpset()));
+by (auto_tac (claset() addSIs [lessI RS less_imp_le]
+                       addSDs [less_imp_Suc_add], 
+    simpset()));
 by (induct_tac "ka" 1);
-by (auto_tac (claset() addIs [real_le_trans],simpset()));
+by (auto_tac (claset() addIs [real_le_trans], simpset()));
 by (EVERY1[rtac ccontr, rtac swap, Simp_tac]);
 by (induct_tac "k" 1);
-by (auto_tac (claset() addIs [real_le_trans],simpset()));
+by (auto_tac (claset() addIs [real_le_trans], simpset()));
 qed "monoseq_Suc";
 
 Goalw [monoseq_def] 
@@ -568,7 +569,7 @@
           RS finite_subset) 1);
 by (rtac finite_real_of_posnat_less_real 1);
 by (rtac (lemma_finite_NSBseq RS finite_subset) 1);
-by (auto_tac (claset() addIs [finite_real_of_posnat_less_real],simpset()));
+by (auto_tac (claset() addIs [finite_real_of_posnat_less_real], simpset()));
 val lemma_finite_NSBseq2 = result();
 
 Goal "ALL N. real_of_posnat  N < abs (X (f N)) \
@@ -765,7 +766,7 @@
 
 Goalw [convergent_def] 
       "!!X. (convergent X) = (convergent (%n. -(X n)))";
-by (auto_tac (claset() addDs [LIMSEQ_minus],simpset()));
+by (auto_tac (claset() addDs [LIMSEQ_minus], simpset()));
 by (dtac LIMSEQ_minus 1 THEN Auto_tac);
 qed "convergent_minus_iff";
 
@@ -781,7 +782,7 @@
 by (Step_tac 1);
 by (rtac (convergent_minus_iff RS ssubst) 2);
 by (dtac (Bseq_minus_iff RS ssubst) 2);
-by (auto_tac (claset() addSIs [Bseq_mono_convergent],simpset()));
+by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset()));
 qed "Bseq_monoseq_convergent";
 
 (*----------------------------------------------------------------
@@ -815,7 +816,7 @@
 by (res_inst_tac [("j","abs(X n) + abs (X N)")] 
     real_le_trans 1);
 by (auto_tac (claset() addIs [abs_triangle_minus_ineq,
-    real_add_le_mono1],simpset() addsimps [Bseq_iff2]));
+    real_add_le_mono1], simpset() addsimps [Bseq_iff2]));
 qed "Bseq_iff3";
 
 val real_not_leE = CLAIM "~ m <= n ==> n < (m::real)";
@@ -830,7 +831,7 @@
 by (res_inst_tac [("j","abs K")] real_le_trans 1);
 by (res_inst_tac [("j","abs k")] real_le_trans 3);
 by (auto_tac (claset() addSIs [rename_numerals real_le_add_order] addDs 
-    [real_le_trans],simpset() 
+    [real_le_trans], simpset() 
     addsimps [abs_ge_zero,rename_numerals real_zero_less_one,abs_eqI1]));
 by (subgoal_tac "k < 0" 1);
 by (rtac (real_not_leE RSN (2,real_le_less_trans)) 2);
@@ -874,7 +875,7 @@
     (lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1);
 by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2);
 by (auto_tac (claset() addIs [FreeUltrafilterNat_Int,
-        FreeUltrafilterNat_Nat_set],simpset()));
+        FreeUltrafilterNat_Nat_set], simpset()));
 qed "Cauchy_NSCauchy";
 
 (*-----------------------------------------------
@@ -1052,7 +1053,7 @@
     [NSBseq_def,NSCauchy_def]));
 by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
 by (dtac (HNatInfinite_whn RSN (2,bspec)) 1);
-by (auto_tac (claset() addSDs [st_part_Ex],simpset() 
+by (auto_tac (claset() addSDs [st_part_Ex], simpset() 
               addsimps [SReal_iff]));
 by (blast_tac (claset() addIs [inf_close_trans3]) 1);
 qed "NSCauchy_NSconvergent_iff";
@@ -1077,7 +1078,7 @@
 by (dres_inst_tac [("x","whn")] spec 1);
 by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
 by (auto_tac (claset() addIs 
-    [hypreal_of_real_le_add_Infininitesimal_cancel2],simpset()));
+    [hypreal_of_real_le_add_Infininitesimal_cancel2], simpset()));
 qed "NSLIMSEQ_le";
 
 (* standard version *)
@@ -1188,7 +1189,7 @@
  ---------------------------------------*)
 Goalw [NSLIMSEQ_def] 
        "f ----NS> l ==> (%n. abs(f n)) ----NS> abs(l)";
-by (auto_tac (claset() addIs [inf_close_hrabs],simpset() 
+by (auto_tac (claset() addIs [inf_close_hrabs], simpset() 
     addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym]));
 qed "NSLIMSEQ_imp_rabs";
 
@@ -1214,7 +1215,7 @@
 by (forw_inst_tac [("x","f n")] (rename_numerals real_rinv_gt_zero) 1);
 by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1);
 by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1);
-by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1],simpset()));
+by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1], simpset()));
 qed "LIMSEQ_rinv_zero";
 
 Goal "ALL y. EX N. ALL n. N <= n --> y < f(n) \
@@ -1232,7 +1233,7 @@
 by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1);
 by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1);
 by (dtac (real_of_posnat_less_iff RS iffD2) 1);
-by (auto_tac (claset() addEs [real_less_trans],simpset()));
+by (auto_tac (claset() addEs [real_less_trans], simpset()));
 qed "LIMSEQ_rinv_real_of_posnat";
 
 Goal "(%n. rinv(real_of_posnat n)) ----NS> #0";
@@ -1304,7 +1305,7 @@
       "[| #0 <= x; x < #1 |] ==> Bseq (%n. x ^ n)";
 by (res_inst_tac [("x","#1")] exI 1);
 by (auto_tac (claset() addDs [conjI RS realpow_le2] 
-    addIs [real_less_imp_le],simpset() addsimps 
+    addIs [real_less_imp_le], simpset() addsimps 
     [real_zero_less_one,abs_eqI1,realpow_abs RS sym] ));
 qed "Bseq_realpow";
 
@@ -1334,9 +1335,9 @@
 by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1);
 by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1);
 by (dtac inf_close_trans3 1 THEN assume_tac 1);
-by (auto_tac (claset() addSDs [rename_numerals (real_not_refl2 RS 
-    real_mult_eq_self_zero2)],simpset() addsimps 
-    [hypreal_of_real_mult RS sym]));
+by (auto_tac (claset() addSDs [rename_numerals 
+                                (real_not_refl2 RS real_mult_eq_self_zero2)], 
+    simpset() addsimps [hypreal_of_real_mult RS sym]));
 qed "NSLIMSEQ_realpow_zero";
 
 (*---------------  standard version ---------------*)
diff -r dc615fccc1e6 -r 09a91221ced1 src/HOL/Real/Hyperreal/Series.ML
--- a/src/HOL/Real/Hyperreal/Series.ML	Thu Nov 30 20:18:00 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Series.ML	Fri Dec 01 11:02:55 2000 +0100
@@ -43,7 +43,7 @@
 Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f";
 by (induct_tac "p" 1);
 by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",
-    leI] addDs [le_anti_sym],simpset()));
+    leI] addDs [le_anti_sym], simpset()));
 qed_spec_mp "sumr_split_add";
 
 Goal "!!n. n < p ==> sumr 0 p f + \
@@ -55,7 +55,7 @@
 Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))";
 by (induct_tac "n" 1);
 by (auto_tac (claset() addIs [(abs_triangle_ineq 
-    RS real_le_trans),real_add_le_mono1],simpset()));
+    RS real_le_trans),real_add_le_mono1], simpset()));
 qed "sumr_rabs";
 
 Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
@@ -83,7 +83,7 @@
 
 Goal "n < m --> sumr m n f = #0";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addDs [less_imp_le],simpset()));
+by (auto_tac (claset() addDs [less_imp_le], simpset()));
 qed_spec_mp "sumr_less_bounds_zero";
 Addsimps [sumr_less_bounds_zero];
 
@@ -97,7 +97,7 @@
 context NatArith.thy;
 
 Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m";
-by (auto_tac (claset() addSDs [not_leE],simpset()));
+by (auto_tac (claset() addSDs [not_leE], simpset()));
 qed "lemma_not_Suc_add";
 
 context thy;
@@ -120,7 +120,7 @@
 Addsimps [sumr_minus_one_realpow_zero2];
 
 Goal "m < Suc n ==> Suc n - m = Suc (n - m)";
-by (dtac less_eq_Suc_add 1);
+by (dtac less_imp_Suc_add 1);
 by (Auto_tac);
 val Suc_diff_n = result();
 
@@ -185,13 +185,13 @@
 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()));
+    addDs [leI], simpset()));
 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()));
+    abs_ge_zero], simpset()));
 qed "sumr_rabs_ge_zero";
 Addsimps [sumr_rabs_ge_zero];
 AddSIs [sumr_rabs_ge_zero]; 
@@ -350,12 +350,12 @@
 
 Goal "[| summable f; summable g |]  \
 \     ==> suminf f - suminf g  = suminf(%n. f n - g n)";
-by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums],simpset()));
+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";
-by (auto_tac (claset() addSIs [LIMSEQ_minus],simpset() addsimps [sumr_minus]));
+by (auto_tac (claset() addSIs [LIMSEQ_minus], simpset() addsimps [sumr_minus]));
 qed "sums_minus";
 
 Goal "[|summable f; 0 < k |] \
@@ -365,7 +365,7 @@
 by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); 
 by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); 
 by (dres_inst_tac [("x","n*k")] spec 1); 
-by (auto_tac (claset() addSDs [not_leE],simpset()));
+by (auto_tac (claset() addSDs [not_leE], simpset()));
 by (dres_inst_tac [("j","no")] less_le_trans 1);
 by (Auto_tac);
 qed "sums_group";
@@ -416,7 +416,7 @@
 by (etac LIMSEQ_le 1 THEN Step_tac 1);
 by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1);
 by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
-by (auto_tac (claset() addIs [sumr_le],simpset()));
+by (auto_tac (claset() addIs [sumr_le], simpset()));
 qed "series_pos_le";
 
 Goal "!!f. [| summable f; ALL m. n <= m --> #0 < f(m) |] \
@@ -524,15 +524,15 @@
 Goal "[|ALL n. f n <= g n; summable f; summable g |] \
 \     ==> suminf f <= suminf g";
 by (REPEAT(dtac summable_sums 1));
-by (auto_tac (claset() addSIs [LIMSEQ_le],simpset() addsimps [sums_def]));
+by (auto_tac (claset() addSIs [LIMSEQ_le], simpset() addsimps [sums_def]));
 by (rtac exI 1);
-by (auto_tac (claset() addSIs [sumr_le2],simpset()));
+by (auto_tac (claset() addSIs [sumr_le2], simpset()));
 qed "summable_le";
 
 Goal "[|ALL n. abs(f n) <= g n; summable g |] \
 \     ==> summable f & suminf f <= suminf g";
 by (auto_tac (claset() addIs [summable_comparison_test]
-    addSIs [summable_le],simpset()));
+    addSIs [summable_le], simpset()));
 by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff]));
 qed "summable_le2";
 
@@ -545,7 +545,7 @@
 by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac);
 by (dtac spec 1 THEN Auto_tac);
 by (res_inst_tac [("j","sumr m n (%n. abs(f n))")] real_le_less_trans 1);
-by (auto_tac (claset() addIs [sumr_rabs],simpset()));
+by (auto_tac (claset() addIs [sumr_rabs], simpset()));
 qed "summable_rabs_cancel";
 
 (*-------------------------------------------------------------------
@@ -553,7 +553,7 @@
  -------------------------------------------------------------------*)
 Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))";
 by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel,
-    summable_sumr_LIMSEQ_suminf,sumr_rabs],simpset()));
+    summable_sumr_LIMSEQ_suminf,sumr_rabs], simpset()));
 qed "summable_rabs";
 
 (*-------------------------------------------------------------------
@@ -585,7 +585,7 @@
 
 Goal "(k::nat) <= l ==> (EX n. l = k + n)";
 by (dtac le_imp_less_or_eq 1);
-by (auto_tac (claset() addDs [less_eq_Suc_add],simpset()));
+by (auto_tac (claset() addDs [less_imp_Suc_add], simpset()));
 qed "le_Suc_ex";
 
 Goal "((k::nat) <= l) = (EX n. l = k + n)";
@@ -613,7 +613,7 @@
     simpset() addsimps [summable_def, CLAIM_SIMP 
     "a * (b * c) = b * (a * (c::real))" real_mult_ac]));
 by (res_inst_tac [("x","(abs(f N)*rinv(c ^ N))*rinv(#1 - c)")] exI 1);
-by (auto_tac (claset() addSIs [sums_mult,geometric_sums],simpset() addsimps 
+by (auto_tac (claset() addSIs [sums_mult,geometric_sums], simpset() addsimps 
     [abs_eqI2]));
 qed "ratio_test";
 
@@ -625,7 +625,7 @@
 Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \
 \     --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)";
 by (induct_tac "n" 1);
-by (auto_tac (claset() addIs [DERIV_add],simpset()));
+by (auto_tac (claset() addIs [DERIV_add], simpset()));
 qed "DERIV_sumr";
 
 
diff -r dc615fccc1e6 -r 09a91221ced1 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Thu Nov 30 20:18:00 2000 +0100
+++ b/src/HOL/ex/Primrec.ML	Fri Dec 01 11:02:55 2000 +0100
@@ -125,7 +125,7 @@
 val lemma = result();
 
 Goal "i<j ==> ack(i,k) < ack(j,k)";
-by (dtac less_eq_Suc_add 1);
+by (dtac less_imp_Suc_add 1);
 by (blast_tac (claset() addSIs [lemma]) 1);
 qed "ack_less_mono1";