--- 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";
--- 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])));
--- 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 ---------------*)
--- 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";
--- 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";