--- a/src/HOL/Arith.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Arith.ML Wed Oct 04 13:10:03 1995 +0100
@@ -21,42 +21,40 @@
qed_goalw "diff_0_eq_0" Arith.thy [diff_def, pred_def]
"0 - n = 0"
- (fn _ => [nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]);
+ (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
(*Must simplify BEFORE the induction!! (Else we get a critical pair)
Suc(m) - Suc(n) rewrites to pred(Suc(m) - n) *)
qed_goalw "diff_Suc_Suc" Arith.thy [diff_def, pred_def]
"Suc(m) - Suc(n) = m - n"
(fn _ =>
- [simp_tac nat_ss 1, nat_ind_tac "n" 1, ALLGOALS(asm_simp_tac nat_ss)]);
+ [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
(*** Simplification over add, mult, diff ***)
-val arith_simps =
- [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc,
- diff_0, diff_0_eq_0, diff_Suc_Suc];
+Addsimps [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc, diff_0,
+ diff_0_eq_0, diff_Suc_Suc];
-val arith_ss = nat_ss addsimps arith_simps;
(**** Inductive properties of the operators ****)
(*** Addition ***)
qed_goal "add_0_right" Arith.thy "m + 0 = m"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
-val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
+Addsimps [add_0_right,add_Suc_right];
(*Associative law for addition*)
qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
(*Commutative law for addition*)
qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)"
(fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
@@ -67,59 +65,59 @@
goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)";
by (nat_ind_tac "k" 1);
-by (simp_tac arith_ss 1);
-by (asm_simp_tac arith_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "add_left_cancel";
goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)";
by (nat_ind_tac "k" 1);
-by (simp_tac arith_ss 1);
-by (asm_simp_tac arith_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "add_right_cancel";
goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)";
by (nat_ind_tac "k" 1);
-by (simp_tac arith_ss 1);
-by (asm_simp_tac (arith_ss addsimps [Suc_le_mono]) 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "add_left_cancel_le";
goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)";
by (nat_ind_tac "k" 1);
-by (simp_tac arith_ss 1);
-by (asm_simp_tac arith_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
qed "add_left_cancel_less";
(*** Multiplication ***)
(*right annihilation in product*)
qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
(*right Sucessor law for multiplication*)
qed_goal "mult_Suc_right" Arith.thy "m * Suc(n) = m + (m * n)"
(fn _ => [nat_ind_tac "m" 1,
- ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+ ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
-val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right];
+Addsimps [mult_0_right,mult_Suc_right];
(*Commutative law for multiplication*)
qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS (asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
(*addition distributes over multiplication*)
qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
(fn _ => [nat_ind_tac "m" 1,
- ALLGOALS(asm_simp_tac (arith_ss 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 _ => [nat_ind_tac "m" 1,
- ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+ ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
-val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
+Addsimps [add_mult_distrib,add_mult_distrib2];
(*Associative law for multiplication*)
qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
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,
@@ -130,13 +128,13 @@
(*** Difference ***)
qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
+ (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = (m::nat)";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS(asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "add_diff_inverse";
@@ -145,24 +143,24 @@
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 arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "diff_less_Suc";
goal Arith.thy "!!m::nat. m - n <= m";
by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
by (etac le_trans 1);
-by (simp_tac (HOL_ss addsimps [le_eq_less_or_eq, lessI]) 1);
+by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
qed "diff_le_self";
goal Arith.thy "!!n::nat. (n+m) - n = m";
by (nat_ind_tac "n" 1);
-by (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "diff_add_inverse";
goal Arith.thy "!!n::nat. n - (n+m) = 0";
by (nat_ind_tac "n" 1);
-by (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "diff_add_0";
(*In ordinary notation: if 0<n and n<=m then m-n < m *)
@@ -170,7 +168,7 @@
by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
by (fast_tac HOL_cs 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS(asm_simp_tac(arith_ss addsimps [diff_less_Suc])));
+by (ALLGOALS(asm_simp_tac(!simpset addsimps [diff_less_Suc])));
qed "div_termination";
val wf_less_trans = wf_pred_nat RS wf_trancl RSN (2, def_wfrec RS trans);
@@ -181,12 +179,12 @@
goal Arith.thy "!!m. m<n ==> m mod n = m";
by (rtac (mod_def RS wf_less_trans) 1);
-by(asm_simp_tac HOL_ss 1);
+by(Asm_simp_tac 1);
qed "mod_less";
goal Arith.thy "!!m. [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n";
by (rtac (mod_def RS wf_less_trans) 1);
-by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1);
+by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1);
qed "mod_geq";
@@ -194,12 +192,12 @@
goal Arith.thy "!!m. m<n ==> m div n = 0";
by (rtac (div_def RS wf_less_trans) 1);
-by(asm_simp_tac nat_ss 1);
+by(Asm_simp_tac 1);
qed "div_less";
goal Arith.thy "!!M. [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)";
by (rtac (div_def RS wf_less_trans) 1);
-by(asm_simp_tac (nat_ss addsimps [div_termination, cut_apply, less_eq]) 1);
+by(asm_simp_tac (!simpset addsimps [div_termination, cut_apply, less_eq]) 1);
qed "div_geq";
(*Main Result about quotient and remainder.*)
@@ -207,7 +205,7 @@
by (res_inst_tac [("n","m")] less_induct 1);
by (rename_tac "k" 1); (*Variable name used in line below*)
by (case_tac "k<n" 1);
-by (ALLGOALS (asm_simp_tac(arith_ss addsimps (add_ac @
+by (ALLGOALS (asm_simp_tac(!simpset addsimps (add_ac @
[mod_less, mod_geq, div_less, div_geq,
add_diff_inverse, div_termination]))));
qed "mod_div_equality";
@@ -218,12 +216,12 @@
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 (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_is_0";
val prems = goal Arith.thy "m-n = 0 --> n-m = 0 --> m=n";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (REPEAT(simp_tac arith_ss 1 THEN TRY(atac 1)));
+by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
qed "diffs0_imp_equal_lemma";
(* [| m-n = 0; n-m = 0 |] ==> m=n *)
@@ -232,23 +230,23 @@
val [prem] = goal Arith.thy "m<n ==> 0<n-m";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS(asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "less_imp_diff_positive";
val [prem] = goal Arith.thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS(asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "Suc_diff_n";
goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc m-n)";
-by(simp_tac (nat_ss 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]
setloop (split_tac [expand_if])) 1);
qed "if_Suc_diff_n";
goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs));
+by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o fast_tac HOL_cs));
qed "zero_induct_lemma";
val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
@@ -263,13 +261,13 @@
goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
by (nat_ind_tac "n" 1);
-by (ALLGOALS(simp_tac arith_ss));
+by (ALLGOALS(Simp_tac));
by (REPEAT_FIRST (ares_tac [conjI, impI]));
by (res_inst_tac [("x","0")] exI 2);
-by (simp_tac arith_ss 2);
+by (Simp_tac 2);
by (safe_tac HOL_cs);
by (res_inst_tac [("x","Suc(k)")] exI 1);
-by (simp_tac arith_ss 1);
+by (Simp_tac 1);
val less_eq_Suc_add_lemma = result();
(*"m<n ==> ? k. n = Suc(m+k)"*)
@@ -278,13 +276,13 @@
goal Arith.thy "n <= ((m + n)::nat)";
by (nat_ind_tac "m" 1);
-by (ALLGOALS(simp_tac arith_ss));
+by (ALLGOALS Simp_tac);
by (etac le_trans 1);
by (rtac (lessI RS less_imp_le) 1);
qed "le_add2";
goal Arith.thy "n <= ((n + m)::nat)";
-by (simp_tac (arith_ss addsimps add_ac) 1);
+by (simp_tac (!simpset addsimps add_ac) 1);
by (rtac le_add2 1);
qed "le_add1";
@@ -306,7 +304,7 @@
goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
be rev_mp 1;
by(nat_ind_tac "j" 1);
-by (ALLGOALS(asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
qed "add_lessD1";
@@ -322,17 +320,18 @@
goal Arith.thy "m+k<=n --> m<=(n::nat)";
by (nat_ind_tac "k" 1);
-by (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
val add_leD1_lemma = result();
-bind_thm ("add_leD1", add_leD1_lemma RS mp);;
+bind_thm ("add_leD1", add_leD1_lemma RS mp);
goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
by (asm_full_simp_tac
- (HOL_ss addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
+ (!simpset delsimps [add_Suc_right]
+ addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
by (eresolve_tac [subst] 1);
-by (simp_tac (arith_ss addsimps [less_add_Suc1]) 1);
+by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
qed "less_add_eq_less";
@@ -343,7 +342,7 @@
(*strict, in 1st argument*)
goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k";
by (nat_ind_tac "k" 1);
-by (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "add_less_mono1";
(*strict, in both arguments*)
@@ -351,7 +350,7 @@
by (rtac (add_less_mono1 RS less_trans) 1);
by (REPEAT (assume_tac 1));
by (nat_ind_tac "j" 1);
-by (ALLGOALS (asm_simp_tac arith_ss));
+by (ALLGOALS Asm_simp_tac);
qed "add_less_mono";
(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
@@ -360,7 +359,7 @@
\ i <= j \
\ |] ==> f(i) <= (f(j)::nat)";
by (cut_facts_tac [le] 1);
-by (asm_full_simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
+by (asm_full_simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
by (fast_tac (HOL_cs addSIs [lt_mono]) 1);
qed "less_mono_imp_le_mono";
@@ -374,7 +373,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 (HOL_ss 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 (eresolve_tac [add_le_mono1] 1);
qed "add_le_mono";
--- a/src/HOL/Finite.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Finite.ML Wed Oct 04 13:10:03 1995 +0100
@@ -33,13 +33,13 @@
(** Simplification for Fin **)
-val Fin_ss = set_ss addsimps Fin.intrs;
+Addsimps Fin.intrs;
(*The union of two finite sets is finite*)
val major::prems = goal Finite.thy
"[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)";
by (rtac (major RS Fin_induct) 1);
-by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_insert_left]))));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left]))));
qed "Fin_UnI";
(*Every subset of a finite set is finite*)
@@ -48,18 +48,19 @@
rtac mp, etac spec,
rtac subs]);
by (rtac (fin RS Fin_induct) 1);
-by (simp_tac (Fin_ss addsimps [subset_Un_eq]) 1);
+by (simp_tac (!simpset addsimps [subset_Un_eq]) 1);
by (safe_tac (set_cs addSDs [subset_insert_iff RS iffD1]));
by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2);
-by (ALLGOALS (asm_simp_tac Fin_ss));
+by (ALLGOALS Asm_simp_tac);
qed "Fin_subset";
(*The image of a finite set is finite*)
val major::_ = goal Finite.thy
"F: Fin(A) ==> h``F : Fin(h``A)";
by (rtac (major RS Fin_induct) 1);
-by (simp_tac Fin_ss 1);
-by (asm_simp_tac (set_ss addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
+by (Simp_tac 1);
+by (asm_simp_tac
+ (!simpset addsimps [image_eqI RS Fin.insertI, image_insert]) 1);
qed "Fin_imageI";
val major::prems = goal Finite.thy
@@ -70,7 +71,7 @@
by (rtac (major RS Fin_induct) 1);
by (rtac (Diff_insert RS ssubst) 2);
by (ALLGOALS (asm_simp_tac
- (Fin_ss addsimps (prems@[Diff_subset RS Fin_subset]))));
+ (!simpset addsimps (prems@[Diff_subset RS Fin_subset]))));
qed "Fin_empty_induct_lemma";
val prems = goal Finite.thy
--- a/src/HOL/Fun.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Fun.ML Wed Oct 04 13:10:03 1995 +0100
@@ -6,10 +6,12 @@
Lemmas about functions.
*)
+simpset := HOL_ss;
+
goal Fun.thy "(f = g) = (!x. f(x)=g(x))";
by (rtac iffI 1);
-by(asm_simp_tac HOL_ss 1);
-by(rtac ext 1 THEN asm_simp_tac HOL_ss 1);
+by (Asm_simp_tac 1);
+by (rtac ext 1 THEN Asm_simp_tac 1);
qed "expand_fun_eq";
val prems = goal Fun.thy
@@ -194,7 +196,6 @@
val mksimps_pairs = ("Ball",[bspec]) :: mksimps_pairs;
-val set_ss =
- HOL_ss addsimps mem_simps
- addcongs [ball_cong,bex_cong]
- setmksimps (mksimps mksimps_pairs);
+simpset := !simpset addsimps mem_simps
+ addcongs [ball_cong,bex_cong]
+ setmksimps (mksimps mksimps_pairs);
--- a/src/HOL/Lfp.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Lfp.ML Wed Oct 04 13:10:03 1995 +0100
@@ -59,7 +59,7 @@
brs prems 1;
by(res_inst_tac[("p","x")]PairE 1);
by(hyp_subst_tac 1);
-by(asm_simp_tac (prod_ss addsimps prems) 1);
+by(asm_simp_tac (!simpset addsimps prems) 1);
qed"induct2";
(*** Fixpoint induction a la David Park ***)
--- a/src/HOL/Lfp.thy Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Lfp.thy Wed Oct 04 13:10:03 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/lfp.thy
+(* Title: HOL/Lfp.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/HOL/List.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/List.ML Wed Oct 04 13:10:03 1995 +0100
@@ -15,53 +15,39 @@
bind_thm("Cons_inject", (hd list.inject) RS iffD1 RS conjE);
-val list_ss = HOL_ss addsimps list.simps;
-
goal List.thy "!x. xs ~= x#xs";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "not_Cons_self";
goal List.thy "(xs ~= []) = (? y ys. xs = y#ys)";
by (list.induct_tac "xs" 1);
-by (simp_tac list_ss 1);
-by (asm_simp_tac list_ss 1);
+by (Simp_tac 1);
+by (Asm_simp_tac 1);
by (REPEAT(resolve_tac [exI,refl,conjI] 1));
qed "neq_Nil_conv";
-val list_ss = arith_ss addsimps list.simps @
- [null_Nil, null_Cons, hd_Cons, tl_Cons, ttl_Nil, ttl_Cons,
- mem_Nil, mem_Cons,
- append_Nil, append_Cons,
- rev_Nil, rev_Cons,
- map_Nil, map_Cons,
- flat_Nil, flat_Cons,
- list_all_Nil, list_all_Cons,
- filter_Nil, filter_Cons,
- foldl_Nil, foldl_Cons,
- length_Nil, length_Cons];
-
(** @ - append **)
goal List.thy "(xs@ys)@zs = xs@(ys@zs)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "append_assoc";
goal List.thy "xs @ [] = xs";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "append_Nil2";
goal List.thy "(xs@ys = []) = (xs=[] & ys=[])";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "append_is_Nil";
goal List.thy "(xs @ ys = xs @ zs) = (ys=zs)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "same_append_eq";
@@ -69,12 +55,12 @@
goal List.thy "rev(xs@ys) = rev(ys) @ rev(xs)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_Nil2,append_assoc])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_Nil2,append_assoc])));
qed "rev_append";
goal List.thy "rev(rev l) = l";
by (list.induct_tac "l" 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps [rev_append])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [rev_append])));
qed "rev_rev_ident";
@@ -82,29 +68,29 @@
goal List.thy "x mem (xs@ys) = (x mem xs | x mem ys)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mem_append";
goal List.thy "x mem [x:xs.P(x)] = (x mem xs & P(x))";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
qed "mem_filter";
(** list_all **)
goal List.thy "(Alls x:xs.True) = True";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "list_all_True";
goal List.thy "list_all p (xs@ys) = (list_all p xs & list_all p ys)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "list_all_conj";
goal List.thy "(Alls x:xs.P(x)) = (!x. x mem xs --> P(x))";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (list_ss setloop (split_tac [expand_if]))));
+by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
by (fast_tac HOL_cs 1);
qed "list_all_mem_conv";
@@ -115,7 +101,7 @@
"P(list_case a f xs) = ((xs=[] --> P(a)) & \
\ (!y ys. xs=y#ys --> P(f y ys)))";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
by (fast_tac HOL_cs 1);
qed "expand_list_case";
@@ -130,19 +116,19 @@
goal List.thy "flat(xs@ys) = flat(xs)@flat(ys)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps [append_assoc])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [append_assoc])));
qed"flat_append";
(** length **)
goal List.thy "length(xs@ys) = length(xs)+length(ys)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed"length_append";
goal List.thy "length(rev xs) = length(xs)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps [length_append])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [length_append])));
qed "length_rev";
(** nth **)
@@ -156,31 +142,31 @@
goal List.thy "map (%x.x) = (%xs.xs)";
by (rtac ext 1);
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "map_ident";
goal List.thy "map f (xs@ys) = map f xs @ map f ys";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "map_append";
goalw List.thy [o_def] "map (f o g) xs = map f (map g xs)";
by (list.induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac list_ss));
+by (ALLGOALS Asm_simp_tac);
qed "map_compose";
goal List.thy "rev(map f l) = map f (rev l)";
by (list.induct_tac "l" 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps [map_append])));
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [map_append])));
qed "rev_map_distrib";
goal List.thy "rev(flat ls) = flat (map rev (rev ls))";
by (list.induct_tac "ls" 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps
+by (ALLGOALS (asm_simp_tac (!simpset addsimps
[map_append, flat_append, rev_append, append_Nil2])));
qed "rev_flat";
-val list_ss = list_ss addsimps
+Addsimps
[not_Cons_self, append_assoc, append_Nil2, append_is_Nil, same_append_eq,
mem_append, mem_filter,
rev_append, rev_rev_ident,
--- a/src/HOL/Makefile Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Makefile Wed Oct 04 13:10:03 1995 +0100
@@ -88,7 +88,7 @@
IOA: $(BIN)/HOL $(IOA_FILES)
echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
- echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
+# echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
##Properties of substitutions
SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
@@ -118,8 +118,8 @@
ex: $(BIN)/HOL $(EX_FILES)
echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
-#Full test.
-test: $(BIN)/HOL IMP Integ IOA Subst Lambda ex
+#Full test. (IOA has been removed temporarily)
+test: $(BIN)/HOL IMP Integ Subst Lambda ex
echo 'Test examples ran successfully' > test
.PRECIOUS: $(BIN)/Pure $(BIN)/HOL
--- a/src/HOL/Nat.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Nat.ML Wed Oct 04 13:10:03 1995 +0100
@@ -110,7 +110,7 @@
by (etac (inj_Rep_Nat RS injD) 1);
qed "inj_Suc";
-val Suc_inject = inj_Suc RS injD;;
+val Suc_inject = inj_Suc RS injD;
goal Nat.thy "(Suc(m)=Suc(n)) = (m=n)";
by (EVERY1 [rtac iffI, etac Suc_inject, etac arg_cong]);
@@ -118,7 +118,7 @@
goal Nat.thy "n ~= Suc(n)";
by (nat_ind_tac "n" 1);
-by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [Zero_not_Suc,Suc_Suc_eq])));
+by (ALLGOALS(asm_simp_tac (!simpset addsimps [Zero_not_Suc,Suc_Suc_eq])));
qed "n_not_Suc_n";
val Suc_n_not_n = n_not_Suc_n RS not_sym;
@@ -164,12 +164,12 @@
goal Nat.thy "nat_rec 0 c h = c";
by (rtac (nat_rec_unfold RS trans) 1);
-by (simp_tac (HOL_ss addsimps [nat_case_0]) 1);
+by (simp_tac (!simpset addsimps [nat_case_0]) 1);
qed "nat_rec_0";
goal Nat.thy "nat_rec (Suc n) c h = h n (nat_rec n c h)";
by (rtac (nat_rec_unfold RS trans) 1);
-by (simp_tac (HOL_ss addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
+by (simp_tac (!simpset addsimps [nat_case_Suc, pred_natI, cut_apply]) 1);
qed "nat_rec_Suc";
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
@@ -328,7 +328,7 @@
(*Can be used with less_Suc_eq to get n=m | n<m *)
goal Nat.thy "(~ m < n) = (n < Suc(m))";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by(ALLGOALS(asm_simp_tac (HOL_ss addsimps
+by(ALLGOALS(asm_simp_tac (!simpset addsimps
[not_less0,zero_less_Suc,Suc_less_eq])));
qed "not_less_eq";
@@ -346,13 +346,11 @@
by (rtac not_less0 1);
qed "le0";
-val nat_simps = [not_less0, less_not_refl, zero_less_Suc, lessI,
- Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
- Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
- n_not_Suc_n, Suc_n_not_n,
- nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
-
-val nat_ss0 = sum_ss addsimps nat_simps;
+Addsimps [not_less0, less_not_refl, zero_less_Suc, lessI,
+ Suc_less_eq, less_Suc_eq, le0, not_Suc_n_less_n,
+ Suc_not_Zero, Zero_not_Suc, Suc_Suc_eq,
+ n_not_Suc_n, Suc_n_not_n,
+ nat_case_0, nat_case_Suc, nat_rec_0, nat_rec_Suc];
(*Prevents simplification of f and g: much faster*)
qed_goal "nat_case_weak_cong" Nat.thy
@@ -378,12 +376,12 @@
qed "not_leE";
goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
-by(simp_tac nat_ss0 1);
+by(Simp_tac 1);
by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
qed "lessD";
goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
-by(asm_full_simp_tac nat_ss0 1);
+by(Asm_full_simp_tac 1);
by(fast_tac HOL_cs 1);
qed "Suc_leD";
@@ -407,7 +405,7 @@
qed "le_eq_less_or_eq";
goal Nat.thy "n <= (n::nat)";
-by(simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
+by(simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
qed "le_refl";
val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
@@ -431,7 +429,7 @@
qed "le_anti_sym";
goal Nat.thy "(Suc(n) <= Suc(m)) = (n <= m)";
-by (simp_tac (nat_ss0 addsimps [le_eq_less_or_eq]) 1);
+by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
qed "Suc_le_mono";
-val nat_ss = nat_ss0 addsimps [le_refl,Suc_le_mono];
+Addsimps [le_refl,Suc_le_mono];
--- a/src/HOL/Prod.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Prod.ML Wed Oct 04 13:10:03 1995 +0100
@@ -58,12 +58,12 @@
by (rtac refl 1);
qed "split";
-val prod_ss = set_ss addsimps [fst_conv, snd_conv, split, Pair_eq];
+Addsimps [fst_conv, snd_conv, split, Pair_eq];
goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))";
by (res_inst_tac[("p","s")] PairE 1);
by (res_inst_tac[("p","t")] PairE 1);
-by (asm_simp_tac prod_ss 1);
+by (Asm_simp_tac 1);
qed "Pair_fst_snd_eq";
(*Prevents simplification of c: much faster*)
@@ -74,12 +74,12 @@
(* Do not add as rewrite rule: invalidates some proofs in IMP *)
goal Prod.thy "p = (fst(p),snd(p))";
by (res_inst_tac [("p","p")] PairE 1);
-by (asm_simp_tac prod_ss 1);
+by (Asm_simp_tac 1);
qed "surjective_pairing";
goal Prod.thy "p = split (%x y.(x,y)) p";
by (res_inst_tac [("p","p")] PairE 1);
-by (asm_simp_tac prod_ss 1);
+by (Asm_simp_tac 1);
qed "surjective_pairing2";
(*For use with split_tac and the simplifier*)
@@ -95,7 +95,7 @@
Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
goal Prod.thy "!!a b c. c a b ==> split c (a,b)";
-by (asm_simp_tac prod_ss 1);
+by (Asm_simp_tac 1);
qed "splitI";
val prems = goalw Prod.thy [split_def]
@@ -108,7 +108,7 @@
qed "splitD";
goal Prod.thy "!!a b c. z: c a b ==> z: split c (a,b)";
-by (asm_simp_tac prod_ss 1);
+by (Asm_simp_tac 1);
qed "mem_splitI";
val prems = goalw Prod.thy [split_def]
@@ -126,13 +126,13 @@
"prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
by (rtac ext 1);
by (res_inst_tac [("p","x")] PairE 1);
-by (asm_simp_tac (prod_ss addsimps [prod_fun,o_def]) 1);
+by (asm_simp_tac (!simpset addsimps [prod_fun,o_def]) 1);
qed "prod_fun_compose";
goal Prod.thy "prod_fun (%x.x) (%y.y) = (%z.z)";
by (rtac ext 1);
by (res_inst_tac [("p","z")] PairE 1);
-by (asm_simp_tac (prod_ss addsimps [prod_fun]) 1);
+by (asm_simp_tac (!simpset addsimps [prod_fun]) 1);
qed "prod_fun_ident";
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
--- a/src/HOL/ROOT.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/ROOT.ML Wed Oct 04 13:10:03 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: CHOL/ROOT.ML
+(* Title: HOL/ROOT.ML
ID: $Id$
Author: Tobias Nipkow
Copyright 1993 University of Cambridge
@@ -18,7 +18,6 @@
use "thy_syntax.ML";
use_thy "HOL";
-use "../Provers/simplifier.ML";
use "../Provers/splitter.ML";
use "../Provers/hypsubst.ML";
use "../Provers/classical.ML";
@@ -64,7 +63,6 @@
use "simpdata.ML";
use_thy "Ord";
use_thy "subset";
-use_thy "equalities";
use "hologic.ML";
use "subtype.ML";
use_thy "Prod";
--- a/src/HOL/Relation.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Relation.ML Wed Oct 04 13:10:03 1995 +0100
@@ -83,7 +83,7 @@
(** Natural deduction for converse(r) **)
goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
-by (simp_tac prod_ss 1);
+by (Simp_tac 1);
by (fast_tac set_cs 1);
qed "converseI";
@@ -170,4 +170,4 @@
val rel_eq_cs = rel_cs addSIs [equalityI];
-val rel_ss = prod_ss addsimps [pair_in_id_conv];
+Addsimps [pair_in_id_conv];
--- a/src/HOL/Sexp.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Sexp.ML Wed Oct 04 13:10:03 1995 +0100
@@ -87,11 +87,8 @@
and pred_sexp_trans2 = pred_sexp_t2 RSN (2, trans_trancl RS transD);
(*Proves goals of the form (M,N):pred_sexp^+ provided M,N:sexp*)
-val pred_sexp_simps =
- sexp.intrs @
- [pred_sexp_t1, pred_sexp_t2,
- pred_sexp_trans1, pred_sexp_trans2, cut_apply];
-val pred_sexp_ss = HOL_ss addsimps pred_sexp_simps;
+Addsimps (sexp.intrs @ [pred_sexp_t1, pred_sexp_t2,
+ pred_sexp_trans1, pred_sexp_trans2, cut_apply]);
val major::prems = goalw Sexp.thy [pred_sexp_def]
"[| p : pred_sexp; \
@@ -130,6 +127,6 @@
goal Sexp.thy "!!M. [| M: sexp; N: sexp |] ==> \
\ sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
by (rtac (sexp_rec_unfold RS trans) 1);
-by (asm_simp_tac(HOL_ss addsimps
- [sexp_case_Scons,pred_sexpI1,pred_sexpI2,cut_apply])1);
+by (asm_simp_tac (!simpset addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
+ 1);
qed "sexp_rec_Scons";
--- a/src/HOL/Sum.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Sum.ML Wed Oct 04 13:10:03 1995 +0100
@@ -44,11 +44,11 @@
val Inr_neq_Inl = sym RS Inl_neq_Inr;
goal Sum.thy "(Inl(a)=Inr(b)) = False";
-by (simp_tac (HOL_ss addsimps [Inl_not_Inr]) 1);
+by (simp_tac (!simpset addsimps [Inl_not_Inr]) 1);
qed "Inl_Inr_eq";
goal Sum.thy "(Inr(b)=Inl(a)) = False";
-by (simp_tac (HOL_ss addsimps [Inl_not_Inr RS not_sym]) 1);
+by (simp_tac (!simpset addsimps [Inl_not_Inr RS not_sym]) 1);
qed "Inr_Inl_eq";
@@ -157,8 +157,7 @@
by (fast_tac (set_cs addSEs [make_elim Inr_inject, Inr_neq_Inl]) 1);
qed "expand_sum_case";
-val sum_ss = prod_ss addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq,
- sum_case_Inl, sum_case_Inr];
+Addsimps [Inl_eq, Inr_eq, Inl_Inr_eq, Inr_Inl_eq, sum_case_Inl, sum_case_Inr];
(*Prevents simplification of f and g: much faster*)
qed_goal "sum_case_weak_cong" Sum.thy
--- a/src/HOL/Univ.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Univ.ML Wed Oct 04 13:10:03 1995 +0100
@@ -242,7 +242,7 @@
(** Leaf vs Numb **)
goalw Univ.thy [Leaf_def,Numb_def] "Leaf(a) ~= Numb(k)";
-by (simp_tac (HOL_ss addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
+by (simp_tac (!simpset addsimps [Atom_Atom_eq,Inl_not_Inr]) 1);
qed "Leaf_not_Numb";
bind_thm ("Numb_not_Leaf", (Leaf_not_Numb RS not_sym));
@@ -252,8 +252,7 @@
(*** ndepth -- the depth of a node ***)
-val univ_simps = [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq];
-val univ_ss = nat_ss addsimps univ_simps;
+Addsimps [apfst_conv,Scons_not_Atom,Atom_not_Scons,Scons_Scons_eq];
goalw Univ.thy [ndepth_def] "ndepth (Abs_Node((%k.0, x))) = 0";
@@ -265,7 +264,7 @@
goal Univ.thy "k < Suc(LEAST x. f(x)=0) --> nat_case (Suc i) f k ~= 0";
by (nat_ind_tac "k" 1);
-by (ALLGOALS (simp_tac nat_ss));
+by (ALLGOALS Simp_tac);
by (rtac impI 1);
by (etac not_less_Least 1);
qed "ndepth_Push_lemma";
@@ -276,7 +275,7 @@
by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
by (safe_tac set_cs);
be ssubst 1; (*instantiates type variables!*)
-by (simp_tac univ_ss 1);
+by (Simp_tac 1);
by (rtac Least_equality 1);
by (rewtac Push_def);
by (rtac (nat_case_Suc RS trans) 1);
@@ -317,25 +316,25 @@
(** Injection nodes **)
goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
-by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_0]) 1);
+by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
by (rewtac Scons_def);
by (safe_tac (set_cs addSIs [equalityI]));
qed "ntrunc_one_In0";
goalw Univ.thy [In0_def]
"ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
-by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
+by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
qed "ntrunc_In0";
goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
-by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_0]) 1);
+by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
by (rewtac Scons_def);
by (safe_tac (set_cs addSIs [equalityI]));
qed "ntrunc_one_In1";
goalw Univ.thy [In1_def]
"ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
-by (simp_tac (univ_ss addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
+by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
qed "ntrunc_In1";
@@ -611,5 +610,4 @@
addSEs [usumE, dsumE]) 1);
qed "fst_image_dsum";
-val fst_image_simps = [fst_image_diag, fst_image_dprod, fst_image_dsum];
-val fst_image_ss = univ_ss addsimps fst_image_simps;
+Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
--- a/src/HOL/WF.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/WF.ML Wed Oct 04 13:10:03 1995 +0100
@@ -69,12 +69,12 @@
H_cong to expose the equality*)
goalw WF.thy [cut_def]
"(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
-by(simp_tac (HOL_ss addsimps [expand_fun_eq]
- setloop (split_tac [expand_if])) 1);
+by(simp_tac (!simpset addsimps [expand_fun_eq]
+ setloop (split_tac [expand_if])) 1);
qed "cut_cut_eq";
goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
-by(asm_simp_tac HOL_ss 1);
+by(Asm_simp_tac 1);
qed "cut_apply";
@@ -83,7 +83,7 @@
goalw WF.thy [is_recfun_def,cut_def]
"!!f. [| is_recfun r a H f; ~(b,a):r |] ==> f(b) = (@z.True)";
by (etac ssubst 1);
-by(asm_simp_tac HOL_ss 1);
+by(Asm_simp_tac 1);
qed "is_recfun_undef";
(*eresolve_tac transD solves (a,b):r using transitivity AT MOST ONCE
@@ -100,7 +100,7 @@
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE'
eresolve_tac [transD, mp, allE]));
-val wf_super_ss = HOL_ss setsolver indhyp_tac;
+val wf_super_ss = !simpset setsolver indhyp_tac;
val prems = goalw WF.thy [is_recfun_def,cut_def]
"[| wf(r); trans(r); is_recfun r a H f; is_recfun r b H g |] ==> \
@@ -168,7 +168,7 @@
\ wftrec r a H = H a (cut (%x.wftrec r x H) r a)";
by (EVERY1 [stac (rewrite_rule [is_recfun_def] unfold_the_recfun),
REPEAT o atac, rtac H_cong1]);
-by (asm_simp_tac (HOL_ss addsimps [cut_cut_eq,the_recfun_cut]) 1);
+by (asm_simp_tac (!simpset addsimps [cut_cut_eq,the_recfun_cut]) 1);
qed "wftrec";
(*Unused but perhaps interesting*)
@@ -186,7 +186,7 @@
by (etac (wf_trancl RS wftrec RS ssubst) 1);
by (rtac trans_trancl 1);
by (rtac (refl RS H_cong) 1); (*expose the equality of cuts*)
-by (simp_tac (HOL_ss addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
+by (simp_tac (!simpset addsimps [cut_cut_eq, cut_apply, r_into_trancl]) 1);
qed "wfrec";
(*This form avoids giant explosions in proofs. NOTE USE OF == *)
--- a/src/HOL/equalities.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/equalities.ML Wed Oct 04 13:10:03 1995 +0100
@@ -337,7 +337,7 @@
by (fast_tac eq_cs 1);
qed "Diff_Int";
-val set_ss = set_ss addsimps
+Addsimps
[in_empty,in_insert,insert_subset,
insert_not_empty,empty_not_insert,
Int_absorb,Int_empty_left,Int_empty_right,
--- a/src/HOL/indrule.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/indrule.ML Wed Oct 04 13:10:03 1995 +0100
@@ -87,7 +87,7 @@
(fn prems =>
[rtac (impI RS allI) 1,
DETERM (etac raw_induct 1),
- asm_full_simp_tac (HOL_ss addsimps [Part_Collect]) 1,
+ asm_full_simp_tac (!simpset addsimps [Part_Collect]) 1,
REPEAT (FIRSTGOAL (eresolve_tac [IntE, CollectE, exE, conjE, disjE]
ORELSE' hyp_subst_tac)),
ind_tac (rev prems) (length prems)])
@@ -141,7 +141,8 @@
(*Simplification largely reduces the mutual induction rule to the
standard rule*)
-val mut_ss = set_ss addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
+val mut_ss = simpset_of "Fun"
+ addsimps [Inl_Inr_eq, Inr_Inl_eq, Inl_eq, Inr_eq];
val all_defs = con_defs@part_rec_defs;
--- a/src/HOL/intr_elim.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/intr_elim.ML Wed Oct 04 13:10:03 1995 +0100
@@ -126,7 +126,7 @@
fun con_elim_tac simps =
let val elim_tac = REPEAT o (eresolve_tac (elim_rls@sumprod_free_SEs))
in ALLGOALS(EVERY'[elim_tac,
- asm_full_simp_tac (nat_ss addsimps simps),
+ asm_full_simp_tac (simpset_of "Nat" addsimps simps),
elim_tac,
REPEAT o bound_hyp_subst_tac])
THEN prune_params_tac
--- a/src/HOL/mono.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/mono.ML Wed Oct 04 13:10:03 1995 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/mono
+(* Title: HOL/mono.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
--- a/src/HOL/mono.thy Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/mono.thy Wed Oct 04 13:10:03 1995 +0100
@@ -1,8 +1,8 @@
-(* Title: HOL/mono
+(* Title: HOL/mono.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
-mono = subset
+mono = equalities
--- a/src/HOL/simpdata.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/simpdata.ML Wed Oct 04 13:10:03 1995 +0100
@@ -98,6 +98,8 @@
infix 4 addcongs;
fun ss addcongs congs = ss addeqcongs (congs RL [eq_reflection]);
+fun Addcongs congs = (simpset := !simpset addcongs congs);
+
(*Add a simpset to a classical set!*)
infix 4 addss;
fun cs addss ss = cs addbefore asm_full_simp_tac ss 1;
--- a/src/HOL/subtype.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/subtype.ML Wed Oct 04 13:10:03 1995 +0100
@@ -45,7 +45,7 @@
fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
let
- val _ = require_thy thy "Set" "subtype definitions";
+ val dummy = require_thy thy "Set" "subtype definitions";
val sign = sign_of thy;
(*rhs*)
--- a/src/HOL/thy_syntax.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/thy_syntax.ML Wed Oct 04 13:10:03 1995 +0100
@@ -134,7 +134,8 @@
\ val recs =" ^ mk_rules tname cons "_rec_" ^ ";\n\
\ val simps = inject @ distinct @ cases @ recs;\n\
\ fun induct_tac a = res_inst_tac [(" ^ quote tname ^ ", a)] induct;\n\
- \end;\n");
+ \end;\n\
+ \val dummy = Addsimps " ^ tname ^ ".simps;\n");
(*parsers*)
val tvars = type_args >> map (cat "dtVar");
@@ -159,11 +160,14 @@
fun mk_primrec_decl ((fname, tname), axms) =
let
fun mk_prove (name, eqn) =
- "val " ^ name ^ " = store_thm (" ^ quote name ^ ", prove_goalw thy [get_def thy "
- ^ fname ^ "] " ^ eqn ^ "\n\
- \ (fn _ => [simp_tac (HOL_ss addsimps " ^ tname ^ ".recs) 1]));";
+ "val " ^ name ^ " = store_thm (" ^ quote name
+ ^ ", prove_goalw thy [get_def thy " ^ fname ^ "] " ^ eqn ^ "\n\
+ \ (fn _ => [Simp_tac 1]));";
+
val axs = mk_list (map (fn (n, a) => mk_pair (quote n, a)) axms);
- in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)) end;
+ in ("|> " ^ tname ^ "_add_primrec " ^ axs, cat_lines (map mk_prove axms)
+ ^ "\nval dummy = Addsimps " ^ mk_list (map fst axms) ^ ";")
+ end;
val primrec_decl =
name -- long_id -- repeat1 (ident -- string) >> mk_primrec_decl;
--- a/src/HOL/typedef.ML Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/typedef.ML Wed Oct 04 13:10:03 1995 +0100
@@ -45,7 +45,7 @@
fun ext_subtype prep_term name (t, vs, mx) raw_set axms thms usr_tac thy =
let
- val _ = require_thy thy "Set" "subtype definitions";
+ val dummy = require_thy thy "Set" "subtype definitions";
val sign = sign_of thy;
(*rhs*)