--- a/src/HOL/Arith.ML Mon Nov 03 12:12:10 1997 +0100
+++ b/src/HOL/Arith.ML Mon Nov 03 12:13:18 1997 +0100
@@ -35,7 +35,7 @@
AddIffs [pred_le];
goalw Arith.thy [pred_def] "m<=n --> pred(m) <= pred(n)";
-by(simp_tac (!simpset addsplits [expand_nat_case]) 1);
+by(simp_tac (simpset() addsplits [expand_nat_case]) 1);
qed_spec_mp "pred_le_mono";
goal Arith.thy "!!n. n ~= 0 ==> pred n < n";
@@ -124,7 +124,7 @@
goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
by (induct_tac "m" 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (ALLGOALS (fast_tac (claset() addss (simpset()))));
qed "pred_add_is_0";
Addsimps [pred_add_is_0];
@@ -140,7 +140,7 @@
goal Arith.thy "i<j --> (EX k. j = Suc(i+k))";
by (induct_tac "j" 1);
by (Simp_tac 1);
-by (blast_tac (!claset addSEs [less_SucE]
+by (blast_tac (claset() addSEs [less_SucE]
addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
val lemma = result();
@@ -149,8 +149,8 @@
goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
by (induct_tac "n" 1);
-by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
-by (blast_tac (!claset addSEs [less_SucE]
+by (ALLGOALS (simp_tac (simpset() addsimps [less_Suc_eq])));
+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";
@@ -162,7 +162,7 @@
qed "le_add2";
goal Arith.thy "n <= ((n + m)::nat)";
-by (simp_tac (!simpset addsimps add_ac) 1);
+by (simp_tac (simpset() addsimps add_ac) 1);
by (rtac le_add2 1);
qed "le_add1";
@@ -185,7 +185,7 @@
by (etac rev_mp 1);
by (induct_tac "j" 1);
by (ALLGOALS Asm_simp_tac);
-by (blast_tac (!claset addDs [Suc_lessD]) 1);
+by (blast_tac (claset() addDs [Suc_lessD]) 1);
qed "add_lessD1";
goal Arith.thy "!!i::nat. ~ (i+j < i)";
@@ -194,7 +194,7 @@
qed "not_add_less1";
goal Arith.thy "!!i::nat. ~ (j+i < i)";
-by (simp_tac (!simpset addsimps [add_commute, not_add_less1]) 1);
+by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
qed "not_add_less2";
AddIffs [not_add_less1, not_add_less2];
@@ -211,25 +211,25 @@
goal Arith.thy "m+k<=n --> m<=(n::nat)";
by (induct_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
-by (blast_tac (!claset addDs [Suc_leD]) 1);
+by (blast_tac (claset() addDs [Suc_leD]) 1);
qed_spec_mp "add_leD1";
goal Arith.thy "!!n::nat. m+k<=n ==> k<=n";
-by (full_simp_tac (!simpset addsimps [add_commute]) 1);
+by (full_simp_tac (simpset() addsimps [add_commute]) 1);
by (etac add_leD1 1);
qed_spec_mp "add_leD2";
goal Arith.thy "!!n::nat. m+k<=n ==> m<=n & k<=n";
-by (blast_tac (!claset addDs [add_leD1, add_leD2]) 1);
+by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
bind_thm ("add_leE", result() RS conjE);
goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
-by (safe_tac (!claset addSDs [less_eq_Suc_add]));
+by (safe_tac (claset() addSDs [less_eq_Suc_add]));
by (asm_full_simp_tac
- (!simpset delsimps [add_Suc_right]
+ (simpset() delsimps [add_Suc_right]
addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
by (etac subst 1);
-by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
+by (simp_tac (simpset() addsimps [less_add_Suc1]) 1);
qed "less_add_eq_less";
@@ -255,8 +255,8 @@
\ i <= j \
\ |] ==> f(i) <= (f(j)::nat)";
by (cut_facts_tac [le] 1);
-by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
-by (blast_tac (!claset addSIs [lt_mono]) 1);
+by (asm_full_simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
+by (blast_tac (claset() addSIs [lt_mono]) 1);
qed "less_mono_imp_le_mono";
(*non-strict, in 1st argument*)
@@ -269,7 +269,7 @@
(*non-strict, in both arguments*)
goal Arith.thy "!!k l::nat. [|i<=j; k<=l |] ==> i + k <= j + l";
by (etac (add_le_mono1 RS le_trans) 1);
-by (simp_tac (!simpset addsimps [add_commute]) 1);
+by (simp_tac (simpset() addsimps [add_commute]) 1);
(*j moves to the end because it is free while k, l are bound*)
by (etac add_le_mono1 1);
qed "add_le_mono";
@@ -284,7 +284,7 @@
(*right successor law for multiplication*)
qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)"
(fn _ => [induct_tac "m" 1,
- ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
+ ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
Addsimps [mult_0_right, mult_Suc_right];
@@ -303,16 +303,16 @@
(*addition distributes over multiplication*)
qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
(fn _ => [induct_tac "m" 1,
- ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
+ ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
(fn _ => [induct_tac "m" 1,
- ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
+ ALLGOALS(asm_simp_tac (simpset() addsimps add_ac))]);
(*Associative law for multiplication*)
qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
(fn _ => [induct_tac "m" 1,
- ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
+ ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib]))]);
qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
(fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
@@ -345,11 +345,11 @@
qed_spec_mp "add_diff_inverse";
goal Arith.thy "!!m. n<=m ==> n+(m-n) = (m::nat)";
-by (asm_simp_tac (!simpset addsimps [add_diff_inverse, not_less_iff_le]) 1);
+by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
qed "le_add_diff_inverse";
goal Arith.thy "!!m. n<=m ==> (m-n)+n = (m::nat)";
-by (asm_simp_tac (!simpset addsimps [le_add_diff_inverse, add_commute]) 1);
+by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
qed "le_add_diff_inverse2";
Addsimps [le_add_diff_inverse, le_add_diff_inverse2];
@@ -367,7 +367,7 @@
goal Arith.thy "m - n < Suc(m)";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (etac less_SucE 3);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
qed "diff_less_Suc";
goal Arith.thy "!!m::nat. m - n <= m";
@@ -383,14 +383,14 @@
(*This and the next few suggested by Florian Kammueller*)
goal Arith.thy "!!i::nat. i-j-k = i-k-j";
-by (simp_tac (!simpset addsimps [diff_diff_left, add_commute]) 1);
+by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
qed "diff_commute";
goal Arith.thy "!!i j k:: nat. k<=j --> j<=i --> i - (j - k) = i - j + k";
by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
by (ALLGOALS Asm_simp_tac);
by (asm_simp_tac
- (!simpset addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
+ (simpset() addsimps [Suc_diff_n, le_imp_less_Suc, le_Suc_eq]) 1);
qed_spec_mp "diff_diff_right";
goal Arith.thy "!!i j k:: nat. k<=j --> (i + j) - k = i + (j - k)";
@@ -405,7 +405,7 @@
Addsimps [diff_add_inverse];
goal Arith.thy "!!n::nat.(m+n) - n = m";
-by (simp_tac (!simpset addsimps [diff_add_assoc]) 1);
+by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
qed "diff_add_inverse2";
Addsimps [diff_add_inverse2];
@@ -417,7 +417,7 @@
val [prem] = goal Arith.thy "m < Suc(n) ==> m-n = 0";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_is_0";
@@ -433,7 +433,7 @@
qed "less_imp_diff_positive";
goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
+by (simp_tac (simpset() addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
addsplits [expand_if]) 1);
qed "if_Suc_diff_n";
@@ -456,7 +456,7 @@
goal Arith.thy "!!m::nat. (m+k) - (n+k) = m - n";
val add_commute_k = read_instantiate [("n","k")] add_commute;
-by (asm_simp_tac (!simpset addsimps ([add_commute_k])) 1);
+by (asm_simp_tac (simpset() addsimps ([add_commute_k])) 1);
qed "diff_cancel2";
Addsimps [diff_cancel2];
@@ -470,9 +470,9 @@
by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \
\ Suc (m - Suc na) - Suc (n - Suc na) = m-n" 1);
by (Asm_full_simp_tac 1);
-by (blast_tac (!claset addIs [le_trans]) 1);
-by (auto_tac (!claset addIs [Suc_leD], !simpset delsimps [diff_Suc_Suc]));
-by (asm_full_simp_tac (!simpset delsimps [Suc_less_eq]
+by (blast_tac (claset() addIs [le_trans]) 1);
+by (auto_tac (claset() addIs [Suc_leD], simpset() delsimps [diff_Suc_Suc]));
+by (asm_full_simp_tac (simpset() delsimps [Suc_less_eq]
addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
qed "diff_right_cancel";
@@ -491,7 +491,7 @@
goal Arith.thy "!!m::nat. k * (m - n) = (k * m) - (k * n)";
val mult_commute_k = read_instantiate [("m","k")] mult_commute;
-by (simp_tac (!simpset addsimps [diff_mult_distrib, mult_commute_k]) 1);
+by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
qed "diff_mult_distrib2" ;
(*NOT added as rewrites, since sometimes they are used from right-to-left*)
@@ -500,7 +500,7 @@
goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k";
by (induct_tac "k" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
qed "mult_le_mono1";
(*<=monotonicity, BOTH arguments*)
@@ -509,7 +509,7 @@
by (rtac le_trans 1);
by (stac mult_commute 2);
by (etac mult_le_mono1 2);
-by (simp_tac (!simpset addsimps [mult_commute]) 1);
+by (simp_tac (simpset() addsimps [mult_commute]) 1);
qed "mult_le_mono";
(*strict, in 1st argument; proof is by induction on k>0*)
@@ -517,12 +517,12 @@
by (eres_inst_tac [("i","0")] less_natE 1);
by (Asm_simp_tac 1);
by (induct_tac "x" 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
qed "mult_less_mono2";
goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
by (dtac mult_less_mono2 1);
-by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute])));
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
qed "mult_less_mono1";
goal Arith.thy "(0 < m*n) = (0<m & 0<n)";
@@ -536,18 +536,18 @@
by (Simp_tac 1);
by (induct_tac "n" 1);
by (Simp_tac 1);
-by (fast_tac (!claset addss !simpset) 1);
+by (fast_tac (claset() addss simpset()) 1);
qed "mult_eq_1_iff";
goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
-by (safe_tac (!claset addSIs [mult_less_mono1]));
+by (safe_tac (claset() addSIs [mult_less_mono1]));
by (cut_facts_tac [less_linear] 1);
-by (blast_tac (!claset addDs [mult_less_mono1] addEs [less_asym]) 1);
+by (blast_tac (claset() addDs [mult_less_mono1] addEs [less_asym]) 1);
qed "mult_less_cancel2";
goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
by (dtac mult_less_cancel2 1);
-by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
qed "mult_less_cancel1";
Addsimps [mult_less_cancel1, mult_less_cancel2];
@@ -561,7 +561,7 @@
goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
by (dtac mult_cancel2 1);
-by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
+by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
qed "mult_cancel1";
Addsimps [mult_cancel1, mult_cancel2];
@@ -572,9 +572,9 @@
by (dtac sym 1);
by (rtac disjCI 1);
by (rtac nat_less_cases 1 THEN assume_tac 2);
-by (fast_tac (!claset addSEs [less_SucE] addss !simpset) 1);
-by (best_tac (!claset addDs [mult_less_mono2]
- addss (!simpset addsimps [zero_less_eq RS sym])) 1);
+by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
+by (best_tac (claset() addDs [mult_less_mono2]
+ addss (simpset() addsimps [zero_less_eq RS sym])) 1);
qed "mult_eq_self_implies_10";
@@ -584,7 +584,7 @@
by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
by (Full_simp_tac 1);
by (subgoal_tac "c <= b" 1);
-by (blast_tac (!claset addIs [less_imp_le, le_trans]) 2);
+by (blast_tac (claset() addIs [less_imp_le, le_trans]) 2);
by (Asm_simp_tac 1);
qed "diff_less_mono";
@@ -596,18 +596,18 @@
goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
by (rtac Suc_diff_n 1);
-by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
+by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc]) 1);
qed "Suc_diff_le";
goal Arith.thy "!! n. Suc i <= n ==> Suc (n - Suc i) = n - i";
by (asm_full_simp_tac
- (!simpset addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
+ (simpset() addsimps [Suc_diff_n RS sym, le_eq_less_Suc]) 1);
qed "Suc_diff_Suc";
goal Arith.thy "!! i::nat. i <= n ==> n - (n - i) = i";
by (etac rev_mp 1);
by (res_inst_tac [("m","n"),("n","i")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsimps [Suc_diff_le])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [Suc_diff_le])));
qed "diff_diff_cancel";
Addsimps [diff_diff_cancel];
@@ -615,7 +615,7 @@
by (etac rev_mp 1);
by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
by (Simp_tac 1);
-by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1);
+by (simp_tac (simpset() addsimps [less_add_Suc2, less_imp_le]) 1);
by (Simp_tac 1);
qed "le_add_diff";
@@ -626,7 +626,7 @@
goal Arith.thy "!!n::nat. m<=n --> (m-l) <= (n-l)";
by (induct_tac "n" 1);
by (Simp_tac 1);
-by (simp_tac (!simpset addsimps [le_Suc_eq]) 1);
+by (simp_tac (simpset() addsimps [le_Suc_eq]) 1);
by (rtac impI 1);
by (etac impE 1);
by (atac 1);
@@ -640,8 +640,8 @@
by (Simp_tac 1);
by (case_tac "n <= l" 1);
by (subgoal_tac "m <= l" 1);
-by (asm_simp_tac (!simpset addsimps [Suc_diff_le]) 1);
-by (fast_tac (!claset addEs [le_trans]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
+by (fast_tac (claset() addEs [le_trans]) 1);
by (dtac not_leE 1);
-by (asm_simp_tac (!simpset addsimps [if_Suc_diff_n]) 1);
+by (asm_simp_tac (simpset() addsimps [if_Suc_diff_n]) 1);
qed_spec_mp "diff_le_mono2";