--- a/src/HOLCF/Cfun3.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cfun3.ML Wed Oct 04 14:01:44 1995 +0100
@@ -224,7 +224,7 @@
"Istrictify(f)(UU)= (UU)"
(fn prems =>
[
- (simp_tac HOL_ss 1)
+ (Simp_tac 1)
]);
qed_goalw "Istrictify2" Cfun3.thy [Istrictify_def]
@@ -232,7 +232,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac HOL_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goal "monofun_Istrictify1" Cfun3.thy "monofun(Istrictify)"
@@ -384,16 +384,14 @@
(* Instantiate the simplifier *)
(* ------------------------------------------------------------------------ *)
-val Cfun_rews = [minimal,refl_less,beta_cfun,strict_fapp1,strictify1,
- strictify2];
+Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2];
+
(* ------------------------------------------------------------------------ *)
(* use cont_tac as autotac. *)
(* ------------------------------------------------------------------------ *)
-val Cfun_ss = HOL_ss
- addsimps Cfun_rews
- setsolver
- (fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
- (fn i => DEPTH_SOLVE_1 (cont_tac i))
- );
+simpset := !simpset setsolver
+ (fn thms => (resolve_tac (TrueI::refl::thms)) ORELSE' atac ORELSE'
+ (fn i => DEPTH_SOLVE_1 (cont_tac i))
+ );
--- a/src/HOLCF/Cont.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cont.ML Wed Oct 04 14:01:44 1995 +0100
@@ -147,7 +147,7 @@
(rtac (binchain_cont RS is_ub_lub) 2),
(atac 2),
(atac 2),
- (simp_tac nat_ss 1)
+ (Simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Cprod1.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cprod1.ML Wed Oct 04 14:01:44 1995 +0100
@@ -40,7 +40,7 @@
(res_inst_tac [("p","p")] PairE 1),
(hyp_subst_tac 1),
(dtac less_cprod2a 1),
- (asm_simp_tac HOL_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goalw "less_cprod2c" Cprod1.thy [less_cprod_def]
@@ -65,13 +65,7 @@
(* ------------------------------------------------------------------------ *)
qed_goalw "refl_less_cprod" Cprod1.thy [less_cprod_def] "less_cprod p p"
- (fn prems =>
- [
- (res_inst_tac [("p","p")] PairE 1),
- (hyp_subst_tac 1),
- (simp_tac prod_ss 1),
- (simp_tac Cfun_ss 1)
- ]);
+ (fn prems => [Simp_tac 1]);
qed_goal "antisym_less_cprod" Cprod1.thy
"[|less_cprod p1 p2;less_cprod p2 p1|] ==> p1=p2"
@@ -105,7 +99,7 @@
(dtac less_cprod2c 1),
(dtac less_cprod2c 1),
(rtac (less_cprod1b RS ssubst) 1),
- (simp_tac prod_ss 1),
+ (Simp_tac 1),
(etac conjE 1),
(etac conjE 1),
(rtac conjI 1),
--- a/src/HOLCF/Cprod2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cprod2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -16,10 +16,7 @@
(rtac (inst_cprod_po RS ssubst) 1),
(rtac (less_cprod1b RS ssubst) 1),
(hyp_subst_tac 1),
- (asm_simp_tac prod_ss 1),
- (rtac conjI 1),
- (rtac minimal 1),
- (rtac minimal 1)
+ (Asm_simp_tac 1)
]);
qed_goal "less_cprod3b" Cprod2.thy
@@ -80,8 +77,7 @@
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
(rtac (less_cprod3b RS iffD2) 1),
- (simp_tac prod_ss 1),
- (asm_simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
qed_goalw "monofun_pair2" Cprod2.thy [monofun] "monofun(Pair(x))"
@@ -89,8 +85,7 @@
[
(strip_tac 1),
(rtac (less_cprod3b RS iffD2) 1),
- (simp_tac prod_ss 1),
- (asm_simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
qed_goal "monofun_pair" Cprod2.thy
@@ -118,7 +113,7 @@
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] PairE 1),
(hyp_subst_tac 1),
- (asm_simp_tac prod_ss 1),
+ (Asm_simp_tac 1),
(etac (less_cprod4c RS conjunct1) 1)
]);
@@ -130,7 +125,7 @@
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] PairE 1),
(hyp_subst_tac 1),
- (asm_simp_tac prod_ss 1),
+ (Asm_simp_tac 1),
(etac (less_cprod4c RS conjunct2) 1)
]);
--- a/src/HOLCF/Cprod3.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Cprod3.ML Wed Oct 04 14:01:44 1995 +0100
@@ -27,9 +27,9 @@
(rtac (monofun_pair1 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (simp_tac prod_ss 1),
+ (Simp_tac 1),
(rtac sym 1),
- (simp_tac prod_ss 1),
+ (Simp_tac 1),
(rtac (lub_const RS thelubI) 1)
]);
@@ -58,7 +58,7 @@
(cut_facts_tac prems 1),
(res_inst_tac [("f1","Pair")] (arg_cong RS cong) 1),
(rtac sym 1),
- (simp_tac prod_ss 1),
+ (Simp_tac 1),
(rtac (lub_const RS thelubI) 1),
(rtac lub_equal 1),
(atac 1),
@@ -66,7 +66,7 @@
(rtac (monofun_pair2 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (simp_tac prod_ss 1)
+ (Simp_tac 1)
]);
qed_goal "contlub_pair2" Cprod3.thy "contlub(Pair(x))"
@@ -103,7 +103,7 @@
(strip_tac 1),
(rtac (lub_cprod RS thelubI RS ssubst) 1),
(atac 1),
- (simp_tac prod_ss 1)
+ (Simp_tac 1)
]);
qed_goal "contlub_snd" Cprod3.thy "contlub(snd)"
@@ -113,7 +113,7 @@
(strip_tac 1),
(rtac (lub_cprod RS thelubI RS ssubst) 1),
(atac 1),
- (simp_tac prod_ss 1)
+ (Simp_tac 1)
]);
qed_goal "cont_fst" Cprod3.thy "cont(fst)"
@@ -214,7 +214,7 @@
(rtac (beta_cfun_cprod RS ssubst) 1),
(rtac (beta_cfun RS ssubst) 1),
(rtac cont_fst 1),
- (simp_tac prod_ss 1)
+ (Simp_tac 1)
]);
qed_goalw "csnd2" Cprod3.thy [csnd_def,cpair_def]
@@ -225,7 +225,7 @@
(rtac (beta_cfun_cprod RS ssubst) 1),
(rtac (beta_cfun RS ssubst) 1),
(rtac cont_snd 1),
- (simp_tac prod_ss 1)
+ (Simp_tac 1)
]);
qed_goalw "surjective_pairing_Cprod2" Cprod3.thy
@@ -295,8 +295,8 @@
[
(rtac (beta_cfun RS ssubst) 1),
(cont_tacR 1),
- (simp_tac Cfun_ss 1),
- (simp_tac (Cfun_ss addsimps [cfst2,csnd2]) 1)
+ (Simp_tac 1),
+ (simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
]);
qed_goalw "csplit3" Cprod3.thy [csplit_def]
@@ -305,14 +305,12 @@
[
(rtac (beta_cfun RS ssubst) 1),
(cont_tacR 1),
- (simp_tac (Cfun_ss addsimps [surjective_pairing_Cprod2]) 1)
+ (simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
]);
(* ------------------------------------------------------------------------ *)
(* install simplifier for Cprod *)
(* ------------------------------------------------------------------------ *)
-val Cprod_rews = [cfst2,csnd2,csplit2];
+Addsimps [cfst2,csnd2,csplit2];
-val Cprod_ss = Cfun_ss addsimps Cprod_rews;
-
--- a/src/HOLCF/Dlist.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Dlist.ML Wed Oct 04 14:01:44 1995 +0100
@@ -25,7 +25,7 @@
val temp = prove_goalw Dlist.thy [dlist_copy_def] "dlist_copy`f`UU=UU"
(fn prems =>
[
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
]);
@@ -36,7 +36,7 @@
"dlist_copy`f`dnil=dnil"
(fn prems =>
[
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1)
]);
@@ -48,11 +48,11 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(dlist_rews @ [dlist_abs_iso,dlist_rep_iso])) 1),
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac HOLCF_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps [defined_spair]) 1)
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps [defined_spair]) 1)
]);
val dlist_copy = temp :: dlist_copy;
@@ -67,23 +67,23 @@
"l = UU | l = dnil | (? x xl. x~=UU &xl~=UU & l = dcons`x`xl)"
(fn prems =>
[
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(rtac (dlist_rep_iso RS subst) 1),
(res_inst_tac [("p","dlist_rep`l")] ssumE 1),
(rtac disjI1 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(rtac disjI2 1),
(rtac disjI1 1),
(res_inst_tac [("p","x")] oneE 1),
(contr_tac 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(rtac disjI2 1),
(rtac disjI2 1),
(res_inst_tac [("p","y")] sprodE 1),
(contr_tac 1),
(rtac exI 1),
(rtac exI 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(fast_tac HOL_cs 1)
]);
@@ -111,7 +111,7 @@
val temp = prove_goalw Dlist.thy [dlist_when_def] "dlist_when`f1`f2`UU=UU"
(fn prems =>
[
- (asm_simp_tac (HOLCF_ss addsimps [dlist_iso_strict]) 1)
+ (asm_simp_tac (!simpset addsimps [dlist_iso_strict]) 1)
]);
val dlist_when = [temp];
@@ -120,7 +120,7 @@
"dlist_when`f1`f2`dnil= f1"
(fn prems =>
[
- (asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso]) 1)
+ (asm_simp_tac (!simpset addsimps [dlist_abs_iso]) 1)
]);
val dlist_when = temp::dlist_when;
@@ -130,7 +130,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps [dlist_abs_iso,defined_spair]) 1)
+ (asm_simp_tac (!simpset addsimps [dlist_abs_iso,defined_spair]) 1)
]);
val dlist_when = temp::dlist_when;
@@ -144,7 +144,7 @@
fun prover defs thm = prove_goalw Dlist.thy defs thm
(fn prems =>
[
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_discsel = [
@@ -158,7 +158,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_discsel = [
@@ -189,10 +189,10 @@
(fn prems =>
[
(res_inst_tac [("P1",contr)] classical3 1),
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (simp_tac (!simpset addsimps dlist_rews) 1),
(dtac sym 1),
- (asm_simp_tac HOLCF_ss 1),
- (simp_tac (HOLCF_ss addsimps (prems @ dlist_rews)) 1)
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps (prems @ dlist_rews)) 1)
]);
@@ -206,7 +206,7 @@
fun prover defs thm = prove_goalw Dlist.thy defs thm
(fn prems =>
[
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_constrdef = [
@@ -228,12 +228,12 @@
(resolve_tac dist_less_tr 1),
(dres_inst_tac [("fo5","is_dnil")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("Q","(x::'a)=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("Q","(xl ::'a dlist)=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_dist_less = [temp];
@@ -246,8 +246,8 @@
(resolve_tac dist_less_tr 1),
(dres_inst_tac [("fo5","is_dcons")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_dist_less = temp::dlist_dist_less;
@@ -256,15 +256,15 @@
(fn prems =>
[
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("Q","xl=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("P1","TT = FF")] classical3 1),
(resolve_tac dist_eq_tr 1),
(dres_inst_tac [("f","is_dnil")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_dist_eq = [temp,temp RS not_sym];
@@ -283,12 +283,12 @@
(rtac conjI 1),
(dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.x)")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (!simpset addsimps dlist_when) 1),
+ (asm_simp_tac (!simpset addsimps dlist_when) 1),
(dres_inst_tac [("fo5","dlist_when`UU`(LAM x l.l)")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+ (asm_simp_tac (!simpset addsimps dlist_when) 1),
+ (asm_simp_tac (!simpset addsimps dlist_when) 1)
]);
val dlist_invert =[temp];
@@ -305,12 +305,12 @@
(rtac conjI 1),
(dres_inst_tac [("f","dlist_when`UU`(LAM x l.x)")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
+ (asm_simp_tac (!simpset addsimps dlist_when) 1),
+ (asm_simp_tac (!simpset addsimps dlist_when) 1),
(dres_inst_tac [("f","dlist_when`UU`(LAM x l.l)")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_when) 1)
+ (asm_simp_tac (!simpset addsimps dlist_when) 1),
+ (asm_simp_tac (!simpset addsimps dlist_when) 1)
]);
val dlist_inject = [temp];
@@ -326,7 +326,7 @@
(cut_facts_tac prems 1),
(rtac dlistE 1),
(contr_tac 1),
- (REPEAT (asm_simp_tac (HOLCF_ss addsimps dlist_discsel) 1))
+ (REPEAT (asm_simp_tac (!simpset addsimps dlist_discsel) 1))
]);
val dlist_discsel_def =
@@ -346,8 +346,8 @@
[
(cut_facts_tac prems 1),
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
qed_goal "dtl2" Dlist.thy "x~=UU ==> dtl`(dcons`x`xl)=xl"
@@ -355,8 +355,8 @@
[
(cut_facts_tac prems 1),
(res_inst_tac [("Q","xl=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_rews = dhd2 :: dtl2 :: dlist_rews;
@@ -369,9 +369,9 @@
(fn prems =>
[
(res_inst_tac [("n","n")] natE 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_take = [temp];
@@ -379,7 +379,7 @@
val temp = prove_goalw Dlist.thy [dlist_take_def] "dlist_take 0`xs=UU"
(fn prems =>
[
- (asm_simp_tac iterate_ss 1)
+ (Asm_simp_tac 1)
]);
val dlist_take = temp::dlist_take;
@@ -388,8 +388,8 @@
"dlist_take (Suc n)`dnil=dnil"
(fn prems =>
[
- (asm_simp_tac iterate_ss 1),
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_take = temp::dlist_take;
@@ -399,19 +399,19 @@
(fn prems =>
[
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("Q","xl=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("n","n")] natE 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
val dlist_take = temp::dlist_take;
@@ -453,17 +453,17 @@
[
(cut_facts_tac prems 1),
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (simp_tac (!simpset addsimps dlist_rews) 1),
(strip_tac 1),
((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
(atac 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(etac disjE 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(etac exE 1),
(etac exE 1),
(etac exE 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(REPEAT (etac conjE 1)),
(rtac cfun_arg_cong 1),
(fast_tac HOL_cs 1)
@@ -489,17 +489,17 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (simp_tac (!simpset addsimps dlist_rews) 1),
(resolve_tac prems 1),
(rtac allI 1),
(res_inst_tac [("l","l")] dlistE 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(res_inst_tac [("Q","dlist_take n1`xl=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
(atac 1),
@@ -512,28 +512,28 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (simp_tac (!simpset addsimps dlist_rews) 1),
(rtac allI 1),
(res_inst_tac [("l","l")] dlistE 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(eres_inst_tac [("x","xl")] allE 1),
(etac disjE 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1)
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1)
]);
qed_goal "dlist_all_finite_lemma2" Dlist.thy "? n.dlist_take n`l=l"
(fn prems =>
[
(res_inst_tac [("Q","l=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(subgoal_tac "(!n.dlist_take n`l=UU) |(? n.dlist_take n`l = l)" 1),
(etac disjE 1),
(eres_inst_tac [("P","l=UU")] notE 1),
(rtac dlist_take_lemma 1),
- (asm_simp_tac (HOLCF_ss addsimps dlist_rews) 1),
+ (asm_simp_tac (!simpset addsimps dlist_rews) 1),
(atac 1),
(subgoal_tac "!n.!l.dlist_take n`l=UU |dlist_take n`l=l" 1),
(fast_tac HOL_cs 1),
--- a/src/HOLCF/Dnat.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Dnat.ML Wed Oct 04 14:01:44 1995 +0100
@@ -26,7 +26,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
]);
@@ -48,18 +48,18 @@
"n = UU | n = dzero | (? x . x~=UU & n = dsucc`x)"
(fn prems =>
[
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(rtac (dnat_rep_iso RS subst) 1),
(res_inst_tac [("p","dnat_rep`n")] ssumE 1),
(rtac disjI1 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(rtac (disjI1 RS disjI2) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(res_inst_tac [("p","x")] oneE 1),
(contr_tac 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(rtac (disjI2 RS disjI2) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(fast_tac HOL_cs 1)
]);
@@ -85,7 +85,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(dnat_rews @ [dnat_abs_iso,dnat_rep_iso])) 1)
]);
@@ -106,7 +106,7 @@
fun prover defs thm = prove_goalw Dnat.thy defs thm
(fn prems =>
[
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_discsel = [
@@ -120,7 +120,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_discsel = [
@@ -142,10 +142,10 @@
(fn prems =>
[
(res_inst_tac [("P1",contr)] classical3 1),
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (simp_tac (!simpset addsimps dnat_rews) 1),
(dtac sym 1),
- (asm_simp_tac HOLCF_ss 1),
- (simp_tac (HOLCF_ss addsimps (prems @ dnat_rews)) 1)
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps (prems @ dnat_rews)) 1)
]);
val dnat_constrdef = [
@@ -157,7 +157,7 @@
fun prover defs thm = prove_goalw Dnat.thy defs thm
(fn prems =>
[
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_constrdef = [
@@ -178,10 +178,10 @@
(resolve_tac dist_less_tr 1),
(dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(res_inst_tac [("Q","n=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_dist_less = [temp];
@@ -194,8 +194,8 @@
(resolve_tac dist_less_tr 1),
(dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_dist_less = temp::dnat_dist_less;
@@ -204,13 +204,13 @@
(fn prems =>
[
(res_inst_tac [("Q","n=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(res_inst_tac [("P1","TT = FF")] classical3 1),
(resolve_tac dist_eq_tr 1),
(dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_dist_eq = [temp, temp RS not_sym];
@@ -230,8 +230,8 @@
(cut_facts_tac prems 1),
(dres_inst_tac [("fo5","dnat_when`c`(LAM x.x)")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
])
];
@@ -248,8 +248,8 @@
(cut_facts_tac prems 1),
(dres_inst_tac [("f","dnat_when`c`(LAM x.x)")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
])
];
@@ -264,7 +264,7 @@
(cut_facts_tac prems 1),
(rtac dnatE 1),
(contr_tac 1),
- (REPEAT (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1))
+ (REPEAT (asm_simp_tac (!simpset addsimps dnat_rews) 1))
]);
val dnat_discsel_def =
@@ -283,9 +283,9 @@
(fn prems =>
[
(res_inst_tac [("n","n")] natE 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_take = [temp];
@@ -293,7 +293,7 @@
val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take 0`xs = UU"
(fn prems =>
[
- (asm_simp_tac iterate_ss 1)
+ (Asm_simp_tac 1)
]);
val dnat_take = temp::dnat_take;
@@ -302,8 +302,8 @@
"dnat_take (Suc n)`dzero=dzero"
(fn prems =>
[
- (asm_simp_tac iterate_ss 1),
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_take = temp::dnat_take;
@@ -313,16 +313,16 @@
(fn prems =>
[
(res_inst_tac [("Q","xs=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(res_inst_tac [("n","n")] natE 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
val dnat_take = temp::dnat_take;
@@ -365,16 +365,16 @@
[
(cut_facts_tac prems 1),
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps dnat_take) 1),
+ (simp_tac (!simpset addsimps dnat_take) 1),
(strip_tac 1),
((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
(atac 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
+ (asm_simp_tac (!simpset addsimps dnat_take) 1),
(etac disjE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
+ (asm_simp_tac (!simpset addsimps dnat_take) 1),
(etac exE 1),
(etac exE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_take) 1),
+ (asm_simp_tac (!simpset addsimps dnat_take) 1),
(REPEAT (etac conjE 1)),
(rtac cfun_arg_cong 1),
(fast_tac HOL_cs 1)
@@ -409,17 +409,17 @@
(rtac adm_subst 1),
(cont_tacR 1),
(resolve_tac prems 1),
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(resolve_tac prems 1),
(strip_tac 1),
(res_inst_tac [("n","xa")] dnatE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+ (asm_simp_tac (!simpset addsimps dnat_copy) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+ (asm_simp_tac (!simpset addsimps dnat_copy) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
+ (asm_simp_tac (!simpset addsimps dnat_copy) 1),
(res_inst_tac [("Q","x`xb=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
(eresolve_tac prems 1),
(etac spec 1)
@@ -433,17 +433,17 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
(rtac allI 1),
(res_inst_tac [("n","s")] dnatE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(res_inst_tac [("Q","dnat_take n1`x=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
(atac 1),
@@ -455,28 +455,28 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (simp_tac (!simpset addsimps dnat_rews) 1),
(rtac allI 1),
(res_inst_tac [("n","s")] dnatE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(eres_inst_tac [("x","x")] allE 1),
(etac disjE 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1)
]);
qed_goal "dnat_all_finite_lemma2" Dnat.thy "? n.dnat_take n`s=s"
(fn prems =>
[
(res_inst_tac [("Q","s=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(subgoal_tac "(!n.dnat_take(n)`s=UU) |(? n.dnat_take(n)`s=s)" 1),
(etac disjE 1),
(eres_inst_tac [("P","s=UU")] notE 1),
(rtac dnat_take_lemma 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(atac 1),
(subgoal_tac "!n.!s.dnat_take(n)`s=UU |dnat_take(n)`s=s" 1),
(fast_tac HOL_cs 1),
@@ -508,13 +508,13 @@
(rtac allI 1),
(res_inst_tac [("n","y")] dnatE 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
- (asm_simp_tac HOLCF_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
+ (Asm_simp_tac 1),
+ (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
(rtac allI 1),
(res_inst_tac [("n","y")] dnatE 1),
(fast_tac (HOL_cs addSIs [UU_I]) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_dist_less) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(strip_tac 1),
(subgoal_tac "s1<<xa" 1),
(etac allE 1),
@@ -522,7 +522,7 @@
(atac 1),
(etac disjE 1),
(contr_tac 1),
- (asm_simp_tac HOLCF_ss 1),
+ (Asm_simp_tac 1),
(resolve_tac dnat_invert 1),
(REPEAT (atac 1))
]);
--- a/src/HOLCF/Dnat2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Dnat2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -24,14 +24,14 @@
(fn prems =>
[
(rtac (iterator_def2 RS ssubst) 1),
- (simp_tac (HOLCF_ss addsimps dnat_when) 1)
+ (simp_tac (!simpset addsimps dnat_when) 1)
]);
qed_goal "iterator2" Dnat2.thy "iterator`dzero`f`x = x"
(fn prems =>
[
(rtac (iterator_def2 RS ssubst) 1),
- (simp_tac (HOLCF_ss addsimps dnat_when) 1)
+ (simp_tac (!simpset addsimps dnat_when) 1)
]);
qed_goal "iterator3" Dnat2.thy
@@ -41,7 +41,7 @@
(cut_facts_tac prems 1),
(rtac trans 1),
(rtac (iterator_def2 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
+ (asm_simp_tac (!simpset addsimps dnat_rews) 1),
(rtac refl 1)
]);
--- a/src/HOLCF/Fix.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Fix.ML Wed Oct 04 14:01:44 1995 +0100
@@ -24,14 +24,14 @@
(resolve_tac (nat_recs iterate_def) 1)
]);
-val iterate_ss = Cfun_ss addsimps [iterate_0,iterate_Suc];
+Addsimps [iterate_0, iterate_Suc];
qed_goal "iterate_Suc2" Fix.thy "iterate (Suc n) F x = iterate n F (F`x)"
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1)
+ (Simp_tac 1),
+ (Asm_simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -45,10 +45,10 @@
[
(cut_facts_tac prems 1),
(strip_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(nat_ind_tac "i" 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(etac monofun_cfun_arg 1)
]);
@@ -101,8 +101,8 @@
(rtac ub_rangeI 1),
(strip_tac 1),
(nat_ind_tac "i" 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("t","x")] subst 1),
(atac 1),
(etac monofun_cfun_arg 1)
@@ -118,8 +118,8 @@
[
(strip_tac 1),
(nat_ind_tac "i" 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(rtac (less_fun RS iffD2) 1),
(rtac allI 1),
(rtac monofun_cfun 1),
@@ -139,9 +139,9 @@
[
(strip_tac 1),
(nat_ind_tac "i" 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
(rtac ext 1),
(rtac (thelub_fun RS ssubst) 1),
(rtac is_chainI 1),
@@ -183,8 +183,8 @@
(rtac monofunI 1),
(strip_tac 1),
(nat_ind_tac "n" 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(etac monofun_cfun_arg 1)
]);
@@ -194,8 +194,8 @@
(rtac contlubI 1),
(strip_tac 1),
(nat_ind_tac "n" 1),
- (simp_tac iterate_ss 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
+ (Simp_tac 1),
(res_inst_tac [("t","iterate n1 F (lub(range(%u. Y u)))"),
("s","lub(range(%i. iterate n1 F (Y i)))")] ssubst 1),
(atac 1),
@@ -328,7 +328,7 @@
qed_goalw "fix_eq" Fix.thy [fix_def] "fix`F = F`(fix`F)"
(fn prems =>
[
- (asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
(rtac Ifix_eq 1)
]);
@@ -336,7 +336,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1),
(etac Ifix_least 1)
]);
@@ -421,7 +421,7 @@
(fn prems =>
[
(fold_goals_tac [Ifix_def]),
- (asm_simp_tac (Cfun_ss addsimps [cont_Ifix]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Ifix]) 1)
]);
@@ -567,7 +567,7 @@
(atac 2),
(rtac mp 1),
(etac spec 1),
- (asm_simp_tac nat_ss 1)
+ (Asm_simp_tac 1)
]);
@@ -836,7 +836,7 @@
(fn prems =>
[
(res_inst_tac [("P2","%x.False")] (adm_cong RS iffD1) 1),
- (asm_simp_tac Cfun_ss 1),
+ (Asm_simp_tac 1),
(rtac adm_not_free 1)
]);
@@ -927,19 +927,17 @@
(atac 1),
(atac 1),
(res_inst_tac [("s","False"),("t","Suc(ia) < Suc(i)")] ssubst 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(rtac iffI 1),
(etac FalseE 2),
(rtac notE 1),
(etac less_not_sym 1),
(atac 1),
- (asm_simp_tac Cfun_ss 1),
+ (Asm_simp_tac 1),
(etac (is_chainE RS spec) 1),
(hyp_subst_tac 1),
- (asm_simp_tac nat_ss 1),
- (rtac refl_less 1),
- (asm_simp_tac nat_ss 1),
- (rtac refl_less 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
qed_goal "adm_disj_lemma4" Fix.thy
@@ -951,18 +949,18 @@
(rtac allI 1),
(res_inst_tac [("m","n"),("n","Suc(i)")] nat_less_cases 1),
(res_inst_tac[("s","Y(Suc(i))"),("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(etac allE 1),
(rtac mp 1),
(atac 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac[("s","Y(n)"),("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(hyp_subst_tac 1),
(dtac spec 1),
(rtac mp 1),
(atac 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("s","Y(n)"),("t","if n < Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
(res_inst_tac [("s","False"),("t","n < Suc(i)")] ssubst 1),
(rtac iffI 1),
@@ -970,7 +968,7 @@
(rtac notE 1),
(etac less_not_sym 1),
(atac 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(dtac spec 1),
(rtac mp 1),
(atac 1),
--- a/src/HOLCF/HOLCF.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/HOLCF.ML Wed Oct 04 14:01:44 1995 +0100
@@ -6,16 +6,5 @@
open HOLCF;
-val HOLCF_ss = ccc1_ss
- addsimps one_when
- addsimps dist_less_one
- addsimps dist_eq_one
- addsimps dist_less_tr
- addsimps dist_eq_tr
- addsimps tr_when
- addsimps andalso_thms
- addsimps orelse_thms
- addsimps neg_thms
- addsimps ifte_thms;
-
-
+Addsimps (one_when @ dist_less_one @ dist_eq_one @ dist_less_tr @ dist_eq_tr
+ @ tr_when @ andalso_thms @ orelse_thms @ neg_thms @ ifte_thms);
--- a/src/HOLCF/Lift1.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Lift1.ML Wed Oct 04 14:01:44 1995 +0100
@@ -84,7 +84,7 @@
(rtac refl 1)
]);
-val Lift_ss = Cfun_ss addsimps [Ilift1,Ilift2];
+Addsimps [Ilift1,Ilift2];
qed_goalw "less_lift1a" Lift1.thy [less_lift_def,UU_lift_def]
"less_lift(UU_lift)(z)"
--- a/src/HOLCF/Lift2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Lift2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -55,8 +55,8 @@
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
(res_inst_tac [("p","xa")] liftE 1),
- (asm_simp_tac Lift_ss 1),
- (asm_simp_tac Lift_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(etac monofun_cfun_fun 1)
]);
@@ -65,14 +65,14 @@
[
(strip_tac 1),
(res_inst_tac [("p","x")] liftE 1),
- (asm_simp_tac Lift_ss 1),
- (asm_simp_tac Lift_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("p","y")] liftE 1),
(hyp_subst_tac 1),
(rtac notE 1),
(rtac less_lift2b 1),
(atac 1),
- (asm_simp_tac Lift_ss 1),
+ (Asm_simp_tac 1),
(rtac monofun_cfun_arg 1),
(hyp_subst_tac 1),
(etac (less_lift2c RS iffD1) 1)
@@ -87,7 +87,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac Lift_ss 1)
+ (Asm_simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/Lift3.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Lift3.ML Wed Oct 04 14:01:44 1995 +0100
@@ -44,7 +44,7 @@
(atac 1),
(rtac (monofun_Ilift2 RS ch2ch_monofun) 1),
(etac (monofun_Iup RS ch2ch_monofun) 1),
- (asm_simp_tac Lift_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goal "cont_Iup" Lift3.thy "cont(Iup)"
@@ -70,9 +70,9 @@
(etac (monofun_Ilift1 RS ch2ch_monofun) 2),
(rtac ext 1),
(res_inst_tac [("p","x")] liftE 1),
- (asm_simp_tac Lift_ss 1),
+ (Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Lift_ss 1),
+ (Asm_simp_tac 1),
(etac contlub_cfun_fun 1)
]);
@@ -86,16 +86,16 @@
(rtac (thelub_lift1a RS ssubst) 2),
(atac 2),
(atac 2),
- (asm_simp_tac Lift_ss 2),
+ (Asm_simp_tac 2),
(rtac (thelub_lift1b RS ssubst) 3),
(atac 3),
(atac 3),
(fast_tac HOL_cs 1),
- (asm_simp_tac Lift_ss 2),
+ (Asm_simp_tac 2),
(rtac (chain_UU_I_inverse RS sym) 2),
(rtac allI 2),
(res_inst_tac [("p","Y(i)")] liftE 2),
- (asm_simp_tac Lift_ss 2),
+ (Asm_simp_tac 2),
(rtac notE 2),
(dtac spec 2),
(etac spec 2),
@@ -117,7 +117,7 @@
(rtac exI 1),
(strip_tac 1),
(res_inst_tac [("p","Y(i)")] liftE 1),
- (asm_simp_tac Lift_ss 2),
+ (Asm_simp_tac 2),
(res_inst_tac [("P","Y(i) = UU")] notE 1),
(fast_tac HOL_cs 1),
(rtac (inst_lift_pcpo RS ssubst) 1),
@@ -148,7 +148,7 @@
qed_goalw "Exh_Lift1" Lift3.thy [up_def] "z = UU | (? x. z = up`x)"
(fn prems =>
[
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+ (simp_tac (!simpset addsimps [cont_Iup]) 1),
(rtac (inst_lift_pcpo RS ssubst) 1),
(rtac Exh_Lift 1)
]);
@@ -159,14 +159,14 @@
(cut_facts_tac prems 1),
(rtac inject_Iup 1),
(etac box_equals 1),
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1),
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+ (simp_tac (!simpset addsimps [cont_Iup]) 1),
+ (simp_tac (!simpset addsimps [cont_Iup]) 1)
]);
qed_goalw "defined_up" Lift3.thy [up_def] " up`x ~= UU"
(fn prems =>
[
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+ (simp_tac (!simpset addsimps [cont_Iup]) 1),
(rtac defined_Iup2 1)
]);
@@ -178,7 +178,7 @@
(resolve_tac prems 1),
(etac (inst_lift_pcpo RS ssubst) 1),
(resolve_tac (tl prems) 1),
- (asm_simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Iup]) 1)
]);
@@ -192,7 +192,7 @@
(rtac (beta_cfun RS ssubst) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
- (simp_tac (Lift_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
+ (simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
]);
qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
@@ -205,13 +205,13 @@
cont_Ilift2,cont2cont_CF1L]) 1)),
(rtac (beta_cfun RS ssubst) 1),
(rtac cont_Ilift2 1),
- (simp_tac (Lift_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
+ (simp_tac (!simpset addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
]);
qed_goalw "less_lift4b" Lift3.thy [up_def,lift_def] "~ up`x << UU"
(fn prems =>
[
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+ (simp_tac (!simpset addsimps [cont_Iup]) 1),
(rtac less_lift3b 1)
]);
@@ -219,7 +219,7 @@
"(up`x << up`y) = (x<<y)"
(fn prems =>
[
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1),
+ (simp_tac (!simpset addsimps [cont_Iup]) 1),
(rtac less_lift2c 1)
]);
@@ -247,7 +247,7 @@
(rtac exI 1),
(etac box_equals 1),
(rtac refl 1),
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+ (simp_tac (!simpset addsimps [cont_Iup]) 1)
]);
@@ -268,7 +268,7 @@
(dtac notnotD 1),
(etac box_equals 1),
(rtac refl 1),
- (simp_tac (Lift_ss addsimps [cont_Iup]) 1)
+ (simp_tac (!simpset addsimps [cont_Iup]) 1)
]);
@@ -338,8 +338,8 @@
(fn prems =>
[
(res_inst_tac [("p","x")] liftE1 1),
- (asm_simp_tac (Cfun_ss addsimps [lift1,lift2]) 1),
- (asm_simp_tac (Cfun_ss addsimps [lift1,lift2]) 1)
+ (asm_simp_tac (!simpset addsimps [lift1,lift2]) 1),
+ (asm_simp_tac (!simpset addsimps [lift1,lift2]) 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/One.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/One.ML Wed Oct 04 14:01:44 1995 +0100
@@ -74,10 +74,10 @@
(rtac allI 1),
(rtac allI 1),
(res_inst_tac [("p","x")] oneE 1),
- (asm_simp_tac ccc1_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("p","y")] oneE 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_one) 1),
- (asm_simp_tac ccc1_ss 1)
+ (asm_simp_tac (!simpset addsimps dist_less_one) 1),
+ (Asm_simp_tac 1)
]);
@@ -89,7 +89,7 @@
fun prover s = prove_goalw One.thy [one_when_def,one_def] s
(fn prems =>
[
- (simp_tac (ccc1_ss addsimps [(rep_one_iso ),
+ (simp_tac (!simpset addsimps [(rep_one_iso ),
(abs_one_iso RS allI) RS ((rep_one_iso RS allI)
RS iso_strict) RS conjunct1] )1)
]);
--- a/src/HOLCF/Pcpo.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Pcpo.ML Wed Oct 04 14:01:44 1995 +0100
@@ -105,7 +105,7 @@
(atac 1),
(res_inst_tac [("s","Y(Suc(x))"),("t","X(Suc(x))")] subst 1),
(rtac sym 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
(rtac is_ub_thelub 1),
(resolve_tac prems 1)
]);
--- a/src/HOLCF/Porder.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Porder.ML Wed Oct 04 14:01:44 1995 +0100
@@ -252,7 +252,7 @@
[
(rtac (inst_void_po RS ssubst) 1),
(rewrite_goals_tac [less_void_def]),
- (simp_tac (HOL_ss addsimps [unique_void]) 1)
+ (simp_tac (!simpset addsimps [unique_void]) 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -267,7 +267,7 @@
(strip_tac 1),
(rtac (inst_void_po RS ssubst) 1),
(rewrite_goals_tac [less_void_def]),
- (simp_tac (HOL_ss addsimps [unique_void]) 1),
+ (simp_tac (!simpset addsimps [unique_void]) 1),
(strip_tac 1),
(rtac minimal_void 1)
]);
@@ -341,8 +341,8 @@
(rtac is_chainI 1),
(rtac allI 1),
(nat_ind_tac "i" 1),
- (asm_simp_tac nat_ss 1),
- (asm_simp_tac nat_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(rtac refl_less 1)
]);
@@ -353,8 +353,8 @@
(cut_facts_tac prems 1),
(rtac allI 1),
(nat_ind_tac "j" 1),
- (asm_simp_tac nat_ss 1),
- (asm_simp_tac nat_ss 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
qed_goal "lub_bin_chain" Porder.thy
@@ -365,7 +365,7 @@
(rtac lub_finch1 2),
(etac bin_chain 2),
(etac bin_chainmax 2),
- (simp_tac nat_ss 1)
+ (Simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/ROOT.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/ROOT.ML Wed Oct 04 14:01:44 1995 +0100
@@ -13,58 +13,7 @@
init_thy_reader();
-
-use_thy "Holcfb";
-use_thy "Void";
-
-use_thy "Porder0";
-use_thy "Porder";
-
-use_thy "Pcpo";
-
-use_thy "Fun1";
-use_thy "Fun2";
-use_thy "Fun3";
-
-use_thy "Cont";
-
-use_thy "Cfun1";
-use_thy "Cfun2";
-use_thy "Cfun3";
-
-use_thy "Cprod1";
-use_thy "Cprod2";
-use_thy "Cprod3";
-
-use_thy "Sprod0";
-use_thy "Sprod1";
-use_thy "Sprod2";
-use_thy "Sprod3";
-
-use_thy "Ssum0";
-use_thy "Ssum1";
-use_thy "Ssum2";
-use_thy "Ssum3";
-
-use_thy "Lift1";
-use_thy "Lift2";
-use_thy "Lift3";
-
use_thy "Fix";
-
-use_thy "ccc1";
-use_thy "One";
-use_thy "Tr1";
-use_thy "Tr2";
-
-use_thy "HOLCF";
-
-use_thy "Dnat";
-use_thy "Dnat2";
-
-use_thy "Stream";
-use_thy "Stream2";
-
use_thy "Dlist";
use "../Pure/install_pp.ML";
--- a/src/HOLCF/Sprod0.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Sprod0.ML Wed Oct 04 14:01:44 1995 +0100
@@ -340,10 +340,8 @@
(* instantiate the simplifier *)
(* ------------------------------------------------------------------------ *)
-val Sprod_ss =
- HOL_ss
- addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
- Isfst2,Issnd2];
+Addsimps [strict_Isfst1,strict_Isfst2,strict_Issnd1,strict_Issnd2,
+ Isfst2,Issnd2];
qed_goal "defined_IsfstIssnd" Sprod0.thy
@@ -355,8 +353,8 @@
(contr_tac 1),
(hyp_subst_tac 1),
(rtac conjI 1),
- (asm_simp_tac Sprod_ss 1),
- (asm_simp_tac Sprod_ss 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
@@ -369,10 +367,10 @@
(fn prems =>
[
(res_inst_tac [("z1","z")] (Exh_Sprod RS disjE) 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(etac exE 1),
(etac exE 1),
- (asm_simp_tac Sprod_ss 1)
+ (Asm_simp_tac 1)
]);
--- a/src/HOLCF/Sprod1.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Sprod1.ML Wed Oct 04 14:01:44 1995 +0100
@@ -18,7 +18,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac HOL_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goalw "less_sprod1b" Sprod1.thy [less_sprod_def]
@@ -27,7 +27,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac HOL_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goal "less_sprod2a" Sprod1.thy
@@ -45,7 +45,7 @@
(fast_tac HOL_cs 1),
(fast_tac HOL_cs 1),
(res_inst_tac [("s","Isfst(Ispair UU UU)"),("t","UU")] subst 1),
- (simp_tac Sprod_ss 1),
+ (Simp_tac 1),
(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
(REPEAT (fast_tac HOL_cs 1))
]);
@@ -69,21 +69,21 @@
[
(rtac conjI 1),
(res_inst_tac [("s","Isfst(Ispair xa ya)"),("t","xa")] subst 1),
- (simp_tac (Sprod_ss addsimps prems)1),
+ (simp_tac (!simpset addsimps prems)1),
(res_inst_tac [("s","Isfst(Ispair x y)"),("t","x")] subst 1),
- (simp_tac (Sprod_ss addsimps prems)1),
+ (simp_tac (!simpset addsimps prems)1),
(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct1) 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
- (simp_tac (Sprod_ss addsimps prems)1),
+ (simp_tac (!simpset addsimps prems)1),
(res_inst_tac [("s","Issnd(Ispair xa ya)"),("t","ya")] subst 1),
- (simp_tac (Sprod_ss addsimps prems)1),
+ (simp_tac (!simpset addsimps prems)1),
(res_inst_tac [("s","Issnd(Ispair x y)"),("t","y")] subst 1),
- (simp_tac (Sprod_ss addsimps prems)1),
+ (simp_tac (!simpset addsimps prems)1),
(rtac (defined_Ispair RS less_sprod1b RS iffD1 RS conjunct2) 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
- (simp_tac (Sprod_ss addsimps prems)1)
+ (simp_tac (!simpset addsimps prems)1)
]);
(* ------------------------------------------------------------------------ *)
@@ -123,11 +123,11 @@
(hyp_subst_tac 1),
(res_inst_tac [("x1","x"),("y1","xa"),("x","y"),("y","ya")] (arg_cong RS cong) 1),
(rtac antisym_less 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct1]) 1),
+ (asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct1]) 1),
+ (asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct1]) 1),
(rtac antisym_less 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1),
- (asm_simp_tac (HOL_ss addsimps [less_sprod2c RS conjunct2]) 1)
+ (asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct2]) 1),
+ (asm_simp_tac (!simpset addsimps [less_sprod2c RS conjunct2]) 1)
]);
qed_goal "trans_less_sprod" Sprod1.thy
--- a/src/HOLCF/Sprod3.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Sprod3.ML Wed Oct 04 14:01:44 1995 +0100
@@ -28,7 +28,7 @@
(rtac (monofun_Ispair1 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(rtac sym 1),
(rtac lub_chain_maxelem 1),
(res_inst_tac [("P","%j.~Y(j)=UU")] exE 1),
@@ -41,12 +41,10 @@
(etac Issnd2 1),
(rtac allI 1),
(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
- (asm_simp_tac Sprod_ss 1),
- (rtac refl_less 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
(etac sym 1),
- (asm_simp_tac Sprod_ss 1),
- (rtac minimal 1)
+ (Asm_simp_tac 1)
]);
qed_goal "sprod3_lemma2" Sprod3.thy
@@ -65,7 +63,7 @@
(rtac disjI1 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(etac (chain_UU_I RS spec) 1),
(atac 1)
]);
@@ -87,7 +85,7 @@
(rtac disjI1 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (simp_tac Sprod_ss 1)
+ (Simp_tac 1)
]);
@@ -138,19 +136,17 @@
(etac Isfst2 1),
(rtac allI 1),
(res_inst_tac [("Q","Y(i)=UU")] (excluded_middle RS disjE) 1),
- (asm_simp_tac Sprod_ss 1),
- (rtac refl_less 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("s","UU"),("t","Y(i)")] subst 1),
(etac sym 1),
- (asm_simp_tac Sprod_ss 1),
- (rtac minimal 1),
+ (Asm_simp_tac 1),
(rtac lub_equal 1),
(atac 1),
(rtac (monofun_Issnd RS ch2ch_monofun) 1),
(rtac (monofun_Ispair2 RS ch2ch_monofun) 1),
(atac 1),
(rtac allI 1),
- (asm_simp_tac Sprod_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goal "sprod3_lemma5" Sprod3.thy
@@ -169,7 +165,7 @@
(rtac disjI2 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(etac (chain_UU_I RS spec) 1),
(atac 1)
]);
@@ -190,7 +186,7 @@
(rtac disjI1 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
- (simp_tac Sprod_ss 1)
+ (Simp_tac 1)
]);
qed_goal "contlub_Ispair2" Sprod3.thy "contlub(Ispair(x))"
@@ -241,12 +237,12 @@
(atac 1),
(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]
(excluded_middle RS disjE) 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("s","UU"),("t","lub(range(%i. Issnd(Y(i))))")]
ssubst 1),
(atac 1),
(rtac trans 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(rtac sym 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
@@ -270,11 +266,11 @@
(atac 1),
(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
(excluded_middle RS disjE) 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("s","UU"),("t","lub(range(%i. Isfst(Y(i))))")]
ssubst 1),
(atac 1),
- (asm_simp_tac Sprod_ss 1),
+ (Asm_simp_tac 1),
(rtac sym 1),
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
@@ -679,10 +675,8 @@
(* install simplifier for Sprod *)
(* ------------------------------------------------------------------------ *)
-val Sprod_rews = [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
- strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
- ssplit1,ssplit2];
-
-val Sprod_ss = Cfun_ss addsimps Sprod_rews;
+Addsimps [strict_spair1,strict_spair2,strict_sfst1,strict_sfst2,
+ strict_ssnd1,strict_ssnd2,sfst2,ssnd2,
+ ssplit1,ssplit2];
--- a/src/HOLCF/Ssum0.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Ssum0.ML Wed Oct 04 14:01:44 1995 +0100
@@ -388,7 +388,6 @@
(* instantiate the simplifier *)
(* ------------------------------------------------------------------------ *)
-val Ssum_ss = Cfun_ss addsimps
- [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
+Addsimps [(strict_IsinlIsinr RS sym),Iwhen1,Iwhen2,Iwhen3];
--- a/src/HOLCF/Ssum1.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Ssum1.ML Wed Oct 04 14:01:44 1995 +0100
@@ -62,7 +62,7 @@
(etac conjE 1),
(UU_left "x"),
(UU_right "v"),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(rtac conjI 1),
(strip_tac 1),
(etac conjE 1),
@@ -77,7 +77,7 @@
(etac conjE 1),
(UU_left "x"),
(UU_right "v"),
- (simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
@@ -98,7 +98,7 @@
(etac conjE 1),
(UU_right "x"),
(UU_left "u"),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(rtac conjI 1),
(strip_tac 1),
(etac conjE 1),
@@ -110,7 +110,7 @@
(etac conjE 1),
(UU_right "x"),
(UU_left "u"),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(eq_right "x" "v"),
@@ -144,7 +144,7 @@
(etac conjE 1),
(UU_left "x"),
(UU_right "v"),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(rtac conjI 1),
(strip_tac 1),
(etac conjE 1),
@@ -154,7 +154,7 @@
(etac conjE 1),
(UU_left "x"),
(UU_right "v"),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(dtac conjunct2 1),
(dtac conjunct2 1),
(dtac conjunct1 1),
@@ -183,7 +183,7 @@
(etac conjE 1),
(UU_right "x"),
(UU_left "u"),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(rtac conjI 1),
(strip_tac 1),
(etac conjE 1),
@@ -199,7 +199,7 @@
(etac conjE 1),
(UU_right "x"),
(UU_left "u"),
- (simp_tac HOL_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(eq_right "x" "v"),
--- a/src/HOLCF/Ssum2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Ssum2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -97,10 +97,10 @@
(strip_tac 1),
(res_inst_tac [("p","xb")] IssumE 1),
(hyp_subst_tac 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(etac monofun_cfun_fun 1),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goalw "monofun_Iwhen2" Ssum2.thy [monofun] "monofun(Iwhen(f))"
@@ -111,9 +111,9 @@
(strip_tac 1),
(res_inst_tac [("p","xa")] IssumE 1),
(hyp_subst_tac 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(etac monofun_cfun_fun 1)
]);
@@ -123,36 +123,36 @@
(strip_tac 1),
(res_inst_tac [("p","x")] IssumE 1),
(hyp_subst_tac 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] IssumE 1),
(hyp_subst_tac 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("P","xa=UU")] notE 1),
(atac 1),
(rtac UU_I 1),
(rtac (less_ssum3a RS iffD1) 1),
(atac 1),
(hyp_subst_tac 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac monofun_cfun_arg 1),
(etac (less_ssum3a RS iffD1) 1),
(hyp_subst_tac 1),
(res_inst_tac [("s","UU"),("t","xa")] subst 1),
(etac (less_ssum3c RS iffD1 RS sym) 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] IssumE 1),
(hyp_subst_tac 1),
(res_inst_tac [("s","UU"),("t","ya")] subst 1),
(etac (less_ssum3d RS iffD1 RS sym) 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(hyp_subst_tac 1),
(res_inst_tac [("s","UU"),("t","ya")] subst 1),
(etac (less_ssum3d RS iffD1 RS sym) 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(hyp_subst_tac 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac monofun_cfun_arg 1),
(etac (less_ssum3b RS iffD1) 1)
]);
@@ -247,8 +247,8 @@
(cut_facts_tac prems 1),
(hyp_subst_tac 1),
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -262,8 +262,8 @@
(cut_facts_tac prems 1),
(hyp_subst_tac 1),
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -339,8 +339,8 @@
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
(res_inst_tac [("p","Y(i)")] IssumE 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 2),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 2),
(etac notE 1),
(rtac (less_ssum3c RS iffD1) 1),
(res_inst_tac [("t","Isinl(x)")] subst 1),
@@ -374,8 +374,8 @@
(rtac chain_UU_I_inverse 1),
(rtac allI 1),
(res_inst_tac [("p","Y(i)")] IssumE 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
(etac notE 1),
(rtac (less_ssum3d RS iffD1) 1),
(res_inst_tac [("t","Isinr(y)")] subst 1),
--- a/src/HOLCF/Ssum3.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Ssum3.ML Wed Oct 04 14:01:44 1995 +0100
@@ -41,8 +41,8 @@
(etac (monofun_Isinl RS ch2ch_monofun) 1),
(rtac allI 1),
(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
qed_goal "contlub_Isinr" Ssum3.thy "contlub(Isinr)"
@@ -72,8 +72,8 @@
(etac (monofun_Isinr RS ch2ch_monofun) 1),
(rtac allI 1),
(res_inst_tac [("Q","Y(k)=UU")] classical2 1),
- (asm_simp_tac Ssum_ss 1),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1)
]);
qed_goal "cont_Isinl" Ssum3.thy "cont(Isinl)"
@@ -114,11 +114,11 @@
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
(res_inst_tac [("p","xa")] IssumE 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(etac contlub_cfun_fun 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1)
]);
@@ -133,11 +133,11 @@
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
(res_inst_tac [("p","x")] IssumE 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac (lub_const RS thelubI RS sym) 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(etac contlub_cfun_fun 1)
]);
@@ -192,7 +192,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(rtac (chain_UU_I_inverse RS sym) 1),
(rtac allI 1),
(res_inst_tac [("s","Isinl(UU)"),("t","Y(i)")] subst 1),
@@ -200,7 +200,7 @@
(rtac (chain_UU_I RS spec RS sym) 1),
(atac 1),
(etac (inst_ssum_pcpo RS ssubst) 1),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goal "ssum_lemma12" Ssum3.thy
@@ -209,7 +209,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("t","x")] subst 1),
(rtac inject_Isinl 1),
(rtac trans 1),
@@ -255,7 +255,7 @@
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
@@ -268,7 +268,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac Ssum_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("t","x")] subst 1),
(rtac inject_Isinr 1),
(rtac trans 1),
@@ -319,7 +319,7 @@
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
- (simp_tac Cfun_ss 1),
+ (Simp_tac 1),
(rtac (monofun_fapp2 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1),
(etac (monofun_Iwhen3 RS ch2ch_monofun) 1)
@@ -373,14 +373,14 @@
qed_goalw "strict_sinl" Ssum3.thy [sinl_def] "sinl`UU =UU"
(fn prems =>
[
- (simp_tac (Ssum_ss addsimps [cont_Isinl]) 1),
+ (simp_tac (!simpset addsimps [cont_Isinl]) 1),
(rtac (inst_ssum_pcpo RS sym) 1)
]);
qed_goalw "strict_sinr" Ssum3.thy [sinr_def] "sinr`UU=UU"
(fn prems =>
[
- (simp_tac (Ssum_ss addsimps [cont_Isinr]) 1),
+ (simp_tac (!simpset addsimps [cont_Isinr]) 1),
(rtac (inst_ssum_pcpo RS sym) 1)
]);
@@ -391,8 +391,8 @@
(cut_facts_tac prems 1),
(rtac noteq_IsinlIsinr 1),
(etac box_equals 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
]);
qed_goalw "inject_sinl" Ssum3.thy [sinl_def,sinr_def]
@@ -402,8 +402,8 @@
(cut_facts_tac prems 1),
(rtac inject_Isinl 1),
(etac box_equals 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
]);
qed_goalw "inject_sinr" Ssum3.thy [sinl_def,sinr_def]
@@ -413,8 +413,8 @@
(cut_facts_tac prems 1),
(rtac inject_Isinr 1),
(etac box_equals 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
]);
@@ -444,7 +444,7 @@
"z=UU | (? a. z=sinl`a & a~=UU) | (? b. z=sinr`b & b~=UU)"
(fn prems =>
[
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
(rtac (inst_ssum_pcpo RS ssubst) 1),
(rtac Exh_Ssum 1)
]);
@@ -462,10 +462,10 @@
(atac 1),
(resolve_tac prems 1),
(atac 2),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
(resolve_tac prems 1),
(atac 2),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1)
]);
@@ -499,7 +499,7 @@
(rtac (beta_cfun RS ssubst) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont2cont_CF1L]) 1)),
- (simp_tac Ssum_ss 1)
+ (Simp_tac 1)
]);
qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def]
@@ -519,7 +519,7 @@
(rtac (beta_cfun RS ssubst) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1)
]);
@@ -541,7 +541,7 @@
(rtac (beta_cfun RS ssubst) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (asm_simp_tac Ssum_ss 1)
+ (Asm_simp_tac 1)
]);
@@ -602,7 +602,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinr,cont_Isinl]) 1),
+ (asm_simp_tac (!simpset addsimps [cont_Isinr,cont_Isinl]) 1),
(etac ssum_lemma4 1)
]);
@@ -629,7 +629,7 @@
(rtac exI 1),
(etac box_equals 1),
(rtac refl 1),
- (asm_simp_tac (Ssum_ss addsimps [cont_Isinl]) 1)
+ (asm_simp_tac (!simpset addsimps [cont_Isinl]) 1)
]);
qed_goalw "thelub_ssum2b" Ssum3.thy [sinl_def,sinr_def,sswhen_def]
@@ -658,7 +658,7 @@
(rtac exI 1),
(etac box_equals 1),
(rtac refl 1),
- (asm_simp_tac (Ssum_ss addsimps
+ (asm_simp_tac (!simpset addsimps
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3]) 1)
]);
@@ -668,11 +668,11 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (Ssum_ss addsimps
+ (asm_simp_tac (!simpset addsimps
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3]) 1),
(etac ssum_lemma9 1),
- (asm_simp_tac (Ssum_ss addsimps
+ (asm_simp_tac (!simpset addsimps
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3]) 1)
]);
@@ -682,11 +682,11 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (Ssum_ss addsimps
+ (asm_simp_tac (!simpset addsimps
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3]) 1),
(etac ssum_lemma10 1),
- (asm_simp_tac (Ssum_ss addsimps
+ (asm_simp_tac (!simpset addsimps
[cont_Isinr,cont_Isinl,cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3]) 1)
]);
@@ -714,9 +714,9 @@
(fn prems =>
[
(res_inst_tac [("p","z")] ssumE 1),
- (asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1),
- (asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1),
- (asm_simp_tac (Cfun_ss addsimps [sswhen1,sswhen2,sswhen3]) 1)
+ (asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1),
+ (asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1),
+ (asm_simp_tac (!simpset addsimps [sswhen1,sswhen2,sswhen3]) 1)
]);
@@ -724,5 +724,4 @@
(* install simplifier for Ssum *)
(* ------------------------------------------------------------------------ *)
-val Ssum_rews = [strict_sinl,strict_sinr,sswhen1,sswhen2,sswhen3];
-val Ssum_ss = Cfun_ss addsimps Ssum_rews;
+Addsimps [strict_sinl,strict_sinr,sswhen1,sswhen2,sswhen3];
--- a/src/HOLCF/Stream.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Stream.ML Wed Oct 04 14:01:44 1995 +0100
@@ -26,7 +26,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
]);
@@ -47,18 +47,18 @@
"s = UU | (? x xs. x~=UU & s = scons`x`xs)"
(fn prems =>
[
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(rtac (stream_rep_iso RS subst) 1),
(res_inst_tac [("p","stream_rep`s")] sprodE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("p","y")] liftE1 1),
(contr_tac 1),
(rtac disjI2 1),
(rtac exI 1),
(rtac exI 1),
(etac conjI 1),
- (asm_simp_tac HOLCF_ss 1)
+ (Asm_simp_tac 1)
]);
qed_goal "streamE" Stream.thy
@@ -82,7 +82,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps
+ (asm_simp_tac (!simpset addsimps
(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
]);
@@ -102,7 +102,7 @@
fun prover defs thm = prove_goalw Stream.thy defs thm
(fn prems =>
[
- (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (simp_tac (!simpset addsimps stream_rews) 1)
]);
val stream_discsel = [
@@ -115,7 +115,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
val stream_discsel = [
@@ -134,10 +134,10 @@
(fn prems =>
[
(res_inst_tac [("P1",contr)] classical3 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(dtac sym 1),
- (asm_simp_tac HOLCF_ss 1),
- (simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps (prems @ stream_rews)) 1)
]);
val stream_constrdef = [
@@ -147,7 +147,7 @@
fun prover defs thm = prove_goalw Stream.thy defs thm
(fn prems =>
[
- (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (simp_tac (!simpset addsimps stream_rews) 1)
]);
val stream_constrdef = [
@@ -176,12 +176,12 @@
(rtac conjI 1),
(dres_inst_tac [("fo5","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+ (asm_simp_tac (!simpset addsimps stream_when) 1),
+ (asm_simp_tac (!simpset addsimps stream_when) 1),
(dres_inst_tac [("fo5","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
(etac box_less 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
+ (asm_simp_tac (!simpset addsimps stream_when) 1),
+ (asm_simp_tac (!simpset addsimps stream_when) 1)
])
];
@@ -199,12 +199,12 @@
(rtac conjI 1),
(dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
+ (asm_simp_tac (!simpset addsimps stream_when) 1),
+ (asm_simp_tac (!simpset addsimps stream_when) 1),
(dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
(etac box_equals 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
+ (asm_simp_tac (!simpset addsimps stream_when) 1),
+ (asm_simp_tac (!simpset addsimps stream_when) 1)
])
];
@@ -218,7 +218,7 @@
(cut_facts_tac prems 1),
(rtac streamE 1),
(contr_tac 1),
- (REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
+ (REPEAT (asm_simp_tac (!simpset addsimps stream_discsel) 1))
]);
val stream_discsel_def =
@@ -240,22 +240,22 @@
(fn prems =>
[
(res_inst_tac [("n","n")] natE 1),
- (asm_simp_tac iterate_ss 1),
- (asm_simp_tac iterate_ss 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (Asm_simp_tac 1),
+ (Asm_simp_tac 1),
+ (simp_tac (!simpset addsimps stream_rews) 1)
]),
prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
(fn prems =>
[
- (asm_simp_tac iterate_ss 1)
+ (Asm_simp_tac 1)
])];
fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
(fn prems =>
[
(cut_facts_tac prems 1),
- (simp_tac iterate_ss 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (Simp_tac 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
val stream_take = [
@@ -274,16 +274,16 @@
(fn prems =>
[
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
(fn prems =>
[
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
qed_goal "stream_take2" Stream.thy
@@ -291,8 +291,8 @@
(fn prems =>
[
(res_inst_tac [("Q","x=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
val stream_rews = [stream_iso_strict RS conjunct1,
@@ -351,15 +351,15 @@
[
(cut_facts_tac prems 1),
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1),
((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
(atac 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(etac exE 1),
(etac exE 1),
(etac exE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(REPEAT (etac conjE 1)),
(rtac cfun_arg_cong 1),
(fast_tac HOL_cs 1)
@@ -385,13 +385,13 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(resolve_tac prems 1),
(rtac allI 1),
(res_inst_tac [("s","s")] streamE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(resolve_tac prems 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(resolve_tac prems 1),
(atac 1),
(etac spec 1)
@@ -473,8 +473,8 @@
(fn prems =>
[
(res_inst_tac [("s","s")] streamE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
@@ -500,18 +500,18 @@
(res_inst_tac [("x","stl`s2")] exI 1),
(rtac conjI 1),
(eresolve_tac stream_discsel_def 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
(eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
- (simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
+ (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
(res_inst_tac [("x","shd`s2")] exI 1),
(res_inst_tac [("x","stl`s1")] exI 1),
(res_inst_tac [("x","stl`s2")] exI 1),
(rtac conjI 1),
(eresolve_tac stream_discsel_def 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
(res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
(etac sym 1),
- (simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
+ (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1)
]);
@@ -528,7 +528,7 @@
(fn prems =>
[
(rtac exI 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (simp_tac (!simpset addsimps stream_rews) 1)
]);
qed_goal "inf_stream_not_UU" Stream.thy "~stream_finite(s) ==> s ~= UU"
@@ -549,9 +549,9 @@
(fn prems =>
[
(res_inst_tac [("s","s")] streamE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(hyp_subst_tac 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
@@ -567,7 +567,7 @@
(rtac allI 1),
(rtac allI 1),
(rtac impI 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1),
(rtac ((hd stream_inject) RS conjunct2) 1),
(atac 1),
@@ -581,14 +581,14 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1 ),
(hyp_subst_tac 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(rtac allI 1),
(res_inst_tac [("s","s2")] streamE 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1 ),
(subgoal_tac "stream_take n1`xs = xs" 1),
(rtac ((hd stream_inject) RS conjunct2) 2),
@@ -605,7 +605,7 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1 ),
(res_inst_tac [("P","scons`x`xs=UU")] notE 1),
(eresolve_tac stream_constrdef 1),
@@ -624,8 +624,8 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (simp_tac (!simpset addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1)
]);
(* ---- *)
@@ -635,15 +635,15 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac iterate_ss 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (Simp_tac 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1),
(res_inst_tac [("s","s")] streamE 1),
(hyp_subst_tac 1),
(rtac (iterate_Suc2 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac (iterate_Suc2 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(etac allE 1),
(etac mp 1),
(hyp_subst_tac 1),
@@ -656,16 +656,16 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac allI 1),
(res_inst_tac [("s","s")] streamE 1),
(hyp_subst_tac 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(hyp_subst_tac 1),
(rtac (iterate_Suc2 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
+ (asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
qed_goal "stream_take_lemma7" Stream.thy
@@ -744,7 +744,7 @@
(fn prems =>
[
(nat_ind_tac "n" 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1 ),
(hyp_subst_tac 1),
(dtac UU_I 1),
@@ -761,9 +761,9 @@
(hyp_subst_tac 1),
(strip_tac 1 ),
(dtac UU_I 1),
- (asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
+ (asm_simp_tac(!simpset addsimps (stream_rews @ [stream_finite_UU])) 1),
(hyp_subst_tac 1),
- (simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps stream_rews) 1),
(strip_tac 1 ),
(rtac stream_finite_lemma1 1),
(subgoal_tac "xs << xsa" 1),
@@ -794,7 +794,7 @@
"stream_finite(s) = (? n. iterate n stl s = UU)"
(fn prems =>
[
- (simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
+ (simp_tac (!simpset addsimps [stream_take_lemma7]) 1)
]);
--- a/src/HOLCF/Stream2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Stream2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -25,7 +25,7 @@
(fn prems =>
[
(rtac (smap_def2 RS ssubst) 1),
- (simp_tac (HOLCF_ss addsimps stream_when) 1)
+ (simp_tac (!simpset addsimps stream_when) 1)
]);
qed_goal "smap2" Stream2.thy
@@ -35,7 +35,7 @@
(cut_facts_tac prems 1),
(rtac trans 1),
(rtac (smap_def2 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac refl 1)
]);
--- a/src/HOLCF/Tr1.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Tr1.ML Wed Oct 04 14:01:44 1995 +0100
@@ -129,15 +129,15 @@
(rtac allI 1),
(rtac allI 1),
(res_inst_tac [("p","x")] trE 1),
- (asm_simp_tac ccc1_ss 1),
+ (Asm_simp_tac 1),
(res_inst_tac [("p","y")] trE 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
+ (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
+ (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
+ (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
(res_inst_tac [("p","y")] trE 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1),
- (asm_simp_tac (ccc1_ss addsimps dist_less_tr) 1)
+ (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
+ (asm_simp_tac (!simpset addsimps dist_less_tr) 1),
+ (asm_simp_tac (!simpset addsimps dist_less_tr) 1)
]);
@@ -148,8 +148,8 @@
fun prover s = prove_goalw Tr1.thy [tr_when_def,TT_def,FF_def] s
(fn prems =>
[
- (simp_tac Cfun_ss 1),
- (simp_tac (Ssum_ss addsimps [(rep_tr_iso ),
+ (Simp_tac 1),
+ (simp_tac (!simpset addsimps [(rep_tr_iso ),
(abs_tr_iso RS allI) RS ((rep_tr_iso RS allI)
RS iso_strict) RS conjunct1]@dist_eq_one)1)
]);
--- a/src/HOLCF/Tr2.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/Tr2.ML Wed Oct 04 14:01:44 1995 +0100
@@ -15,7 +15,7 @@
fun prover s = prove_goalw Tr2.thy [andalso_def] s
(fn prems =>
[
- (simp_tac (ccc1_ss addsimps tr_when) 1)
+ (simp_tac (!simpset addsimps tr_when) 1)
]);
val andalso_thms = map prover [
@@ -29,9 +29,9 @@
(fn prems =>
[
(res_inst_tac [("p","x")] trE 1),
- (asm_simp_tac (ccc1_ss addsimps tr_when) 1),
- (asm_simp_tac (ccc1_ss addsimps tr_when) 1),
- (asm_simp_tac (ccc1_ss addsimps tr_when) 1)
+ (asm_simp_tac (!simpset addsimps tr_when) 1),
+ (asm_simp_tac (!simpset addsimps tr_when) 1),
+ (asm_simp_tac (!simpset addsimps tr_when) 1)
])];
(* ------------------------------------------------------------------------ *)
@@ -41,7 +41,7 @@
fun prover s = prove_goalw Tr2.thy [orelse_def] s
(fn prems =>
[
- (simp_tac (ccc1_ss addsimps tr_when) 1)
+ (simp_tac (!simpset addsimps tr_when) 1)
]);
val orelse_thms = map prover [
@@ -55,9 +55,9 @@
(fn prems =>
[
(res_inst_tac [("p","x")] trE 1),
- (asm_simp_tac (ccc1_ss addsimps tr_when) 1),
- (asm_simp_tac (ccc1_ss addsimps tr_when) 1),
- (asm_simp_tac (ccc1_ss addsimps tr_when) 1)
+ (asm_simp_tac (!simpset addsimps tr_when) 1),
+ (asm_simp_tac (!simpset addsimps tr_when) 1),
+ (asm_simp_tac (!simpset addsimps tr_when) 1)
])];
@@ -68,7 +68,7 @@
fun prover s = prove_goalw Tr2.thy [neg_def] s
(fn prems =>
[
- (simp_tac (ccc1_ss addsimps tr_when) 1)
+ (simp_tac (!simpset addsimps tr_when) 1)
]);
val neg_thms = map prover [
@@ -84,7 +84,7 @@
fun prover s = prove_goalw Tr2.thy [ifte_def] s
(fn prems =>
[
- (simp_tac (ccc1_ss addsimps tr_when) 1)
+ (simp_tac (!simpset addsimps tr_when) 1)
]);
val ifte_thms = map prover [
--- a/src/HOLCF/ccc1.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/ccc1.ML Wed Oct 04 14:01:44 1995 +0100
@@ -87,8 +87,7 @@
(* Merge the different rewrite rules for the simplifier *)
(* ------------------------------------------------------------------------ *)
-val ccc1_ss = Cfun_ss addsimps Cprod_rews addsimps Sprod_rews addsimps
- Ssum_rews addsimps lift_rews addsimps [ID1,ID2,ID3,cfcomp2];
+Addsimps (lift_rews @ [ID1,ID2,ID3,cfcomp2]);
--- a/src/HOLCF/ex/Coind.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/ex/Coind.ML Wed Oct 04 14:01:44 1995 +0100
@@ -29,7 +29,7 @@
[
(rtac trans 1),
(rtac (from_def2 RS ssubst) 1),
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(rtac refl 1)
]);
@@ -58,19 +58,19 @@
(fn prems =>
[
(res_inst_tac [("s","n")] dnat_ind 1),
- (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
- (simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
+ (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1),
+ (simp_tac (!simpset addsimps (coind_rews @ stream_rews)) 1),
(rtac trans 1),
(rtac nats_def2 1),
- (simp_tac (HOLCF_ss addsimps (coind_rews @ dnat_rews)) 1),
+ (simp_tac (!simpset addsimps (coind_rews @ dnat_rews)) 1),
(rtac trans 1),
(etac iterator3 1),
(rtac trans 1),
- (asm_simp_tac HOLCF_ss 1),
+ (Asm_simp_tac 1),
(rtac trans 1),
(etac smap2 1),
(rtac cfun_arg_cong 1),
- (asm_simp_tac (HOLCF_ss addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
+ (asm_simp_tac (!simpset addsimps ([iterator3 RS sym] @ dnat_rews)) 1)
]);
@@ -80,13 +80,13 @@
(res_inst_tac [("R",
"% p q.? n. p = iterator`n`(smap`dsucc)`nats & q = from`n")] stream_coind 1),
(res_inst_tac [("x","dzero")] exI 2),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 2),
+ (asm_simp_tac (!simpset addsimps coind_rews) 2),
(rewrite_goals_tac [stream_bisim_def]),
(strip_tac 1),
(etac exE 1),
(res_inst_tac [("Q","n=UU")] classical2 1),
(rtac disjI1 1),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
+ (asm_simp_tac (!simpset addsimps coind_rews) 1),
(rtac disjI2 1),
(etac conjE 1),
(hyp_subst_tac 1),
@@ -113,26 +113,26 @@
(strip_tac 1),
(etac exE 1),
(res_inst_tac [("Q","n=UU")] classical2 1),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1),
+ (asm_simp_tac (!simpset addsimps coind_rews) 1),
(res_inst_tac [("x","UU::dnat")] exI 1),
- (simp_tac (HOLCF_ss addsimps coind_rews addsimps stream_rews) 1),
+ (simp_tac (!simpset addsimps coind_rews addsimps stream_rews) 1),
(etac conjE 1),
(hyp_subst_tac 1),
(rtac conjI 1),
(rtac (coind_lemma1 RS ssubst) 1),
(rtac (from RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(res_inst_tac [("x","dsucc`n")] exI 1),
(rtac conjI 1),
(rtac trans 1),
(rtac (coind_lemma1 RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac refl 1),
(rtac trans 1),
(rtac (from RS ssubst) 1),
- (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
+ (asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac refl 1),
(res_inst_tac [("x","dzero")] exI 1),
- (asm_simp_tac (HOLCF_ss addsimps coind_rews) 1)
+ (asm_simp_tac (!simpset addsimps coind_rews) 1)
]);
--- a/src/HOLCF/ex/Dagstuhl.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/ex/Dagstuhl.ML Wed Oct 04 14:01:44 1995 +0100
@@ -37,10 +37,10 @@
val prems = goal Dagstuhl.thy "YS = YYS";
by (rtac stream_take_lemma 1);
by (nat_ind_tac "n" 1);
-by (simp_tac (HOLCF_ss addsimps stream_rews) 1);
+by (simp_tac (!simpset addsimps stream_rews) 1);
by (rtac (YS_def2 RS ssubst) 1);
by (rtac (YYS_def2 RS ssubst) 1);
-by (asm_simp_tac (HOLCF_ss addsimps stream_rews) 1);
+by (asm_simp_tac (!simpset addsimps stream_rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
val wir_moel=result();
@@ -56,7 +56,7 @@
by (rtac fix_least 1);
by (rtac (beta_cfun RS ssubst) 1);
by (cont_tacR 1);
-by (simp_tac (HOLCF_ss addsimps [YS_def2 RS sym]) 1);
+by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
val lemma6=result();
val prems = goal Dagstuhl.thy "YS << YYS";
--- a/src/HOLCF/ex/Hoare.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/ex/Hoare.ML Wed Oct 04 14:01:44 1995 +0100
@@ -124,7 +124,7 @@
(fn prems =>
[
(fix_tac3 p_def 1),
- (simp_tac HOLCF_ss 1)
+ (Simp_tac 1)
]);
val q_def3 = prove_goal Hoare.thy
@@ -132,19 +132,21 @@
(fn prems =>
[
(fix_tac3 q_def 1),
- (simp_tac HOLCF_ss 1)
+ (Simp_tac 1)
]);
(** --------- proves about iterations of p and q ---------- **)
+val HOLCF_ss = simpset_of "HOLCF";
+
val hoare_lemma9 = prove_goal Hoare.thy
"(! m. m< Suc k --> b1`(iterate m g x)=TT) -->\
\ p`(iterate k g x)=p`x"
(fn prems =>
[
(nat_ind_tac "k" 1),
- (simp_tac iterate_ss 1),
- (simp_tac iterate_ss 1),
+ (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+ (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
(strip_tac 1),
(res_inst_tac [("s","p`(iterate k1 g x)")] trans 1),
(rtac trans 1),
@@ -152,24 +154,24 @@
(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
(rtac mp 1),
(etac spec 1),
- (simp_tac nat_ss 1),
+ (Simp_tac 1),
(simp_tac HOLCF_ss 1),
(etac mp 1),
(strip_tac 1),
(rtac mp 1),
(etac spec 1),
(etac less_trans 1),
- (simp_tac nat_ss 1)
+ (Simp_tac 1)
]);
-
+trace_simp := false;
val hoare_lemma24 = prove_goal Hoare.thy
"(! m. m< Suc k --> b1`(iterate m g x)=TT) --> \
\ q`(iterate k g x)=q`x"
(fn prems =>
[
(nat_ind_tac "k" 1),
- (simp_tac iterate_ss 1),
- (simp_tac iterate_ss 1),
+ (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
+ (simp_tac (!simpset delsimps [less_Suc_eq]) 1),
(strip_tac 1),
(res_inst_tac [("s","q`(iterate k1 g x)")] trans 1),
(rtac trans 1),
@@ -177,14 +179,14 @@
(res_inst_tac [("s","TT"),("t","b1`(iterate k1 g x)")] ssubst 1),
(rtac mp 1),
(etac spec 1),
- (simp_tac nat_ss 1),
+ (Simp_tac 1),
(simp_tac HOLCF_ss 1),
(etac mp 1),
(strip_tac 1),
(rtac mp 1),
(etac spec 1),
(etac less_trans 1),
- (simp_tac nat_ss 1)
+ (Simp_tac 1)
]);
(* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
@@ -207,15 +209,15 @@
(cut_facts_tac prems 1),
(res_inst_tac [("n","k")] natE 1),
(hyp_subst_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(rtac trans 1),
(rtac p_def3 1),
- (asm_simp_tac HOLCF_ss 1),
- (eres_inst_tac [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")]
- subst 1),
- (simp_tac iterate_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
+ (eres_inst_tac
+ [("s","0"),("t","theleast(%n. b1`(iterate n g x) ~= TT)")] subst 1),
+ (Simp_tac 1),
(hyp_subst_tac 1),
(strip_tac 1),
(etac conjE 1),
@@ -228,12 +230,13 @@
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
- (simp_tac nat_ss 1),
+ (Simp_tac 1),
(simp_tac HOLCF_ss 1),
(rtac trans 1),
(rtac p_def3 1),
- (simp_tac (HOLCF_ss addsimps [iterate_Suc RS sym]) 1),
- (eres_inst_tac [("s","FF")] ssubst 1),
+ (simp_tac (!simpset delsimps [iterate_Suc]
+ addsimps [iterate_Suc RS sym]) 1),
+ (eres_inst_tac [("s","FF")] ssubst 1),
(simp_tac HOLCF_ss 1)
]);
@@ -246,14 +249,14 @@
(cut_facts_tac prems 1),
(res_inst_tac [("n","k")] natE 1),
(hyp_subst_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(rtac trans 1),
(rtac p_def3 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
(hyp_subst_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(rtac trans 1),
@@ -266,11 +269,11 @@
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
- (simp_tac nat_ss 1),
- (asm_simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
+ (asm_simp_tac HOLCF_ss 1),
(rtac trans 1),
(rtac p_def3 1),
- (asm_simp_tac HOLCF_ss 1)
+ (asm_simp_tac HOLCF_ss 1)
]);
(* -------- results about p for case (! k. b1`(iterate k g x)=TT) ------- *)
@@ -289,7 +292,7 @@
(rtac allI 1),
(rtac (strict_fapp1 RS ssubst) 1),
(rtac refl 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(rtac allI 1),
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
(etac spec 1),
@@ -324,10 +327,10 @@
(rtac (strict_fapp1 RS ssubst) 1),
(rtac refl 1),
(rtac allI 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(res_inst_tac [("s","TT"),("t","b1`(iterate k g x)")] ssubst 1),
(etac spec 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
(rtac (iterate_Suc RS subst) 1),
(etac spec 1)
]);
@@ -366,10 +369,10 @@
(rtac (strict_fapp1 RS ssubst) 1),
(rtac refl 1),
(rtac allI 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(res_inst_tac [("s","TT"),("t","b1`(iterate k g (x::'a))")] ssubst 1),
(etac spec 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
(rtac (iterate_Suc RS subst) 1),
(etac spec 1)
]);
@@ -389,7 +392,7 @@
[
(cut_facts_tac prems 1),
(rtac (q_def3 RS ssubst) 1),
- (asm_simp_tac HOLCF_ss 1)
+ (asm_simp_tac HOLCF_ss 1)
]);
(* -------- results about q for case (? k. b1`(iterate k g x) ~= TT) ------- *)
@@ -411,7 +414,7 @@
(res_inst_tac [("n","k")] natE 1),
(hyp_subst_tac 1),
(strip_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(hyp_subst_tac 1),
(strip_tac 1),
(etac conjE 1),
@@ -425,8 +428,8 @@
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
- (simp_tac nat_ss 1),
- (simp_tac (HOLCF_ss addsimps [iterate_Suc]) 1)
+ (Simp_tac 1),
+ (simp_tac HOLCF_ss 1)
]);
@@ -439,13 +442,13 @@
(cut_facts_tac prems 1),
(res_inst_tac [("n","k")] natE 1),
(hyp_subst_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(rtac (q_def3 RS ssubst) 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
(hyp_subst_tac 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
(rtac trans 1),
@@ -458,11 +461,11 @@
(rtac (hoare_lemma8 RS spec RS mp) 1),
(atac 1),
(atac 1),
- (simp_tac nat_ss 1),
+ (Simp_tac 1),
(asm_simp_tac HOLCF_ss 1),
(rtac trans 1),
(rtac q_def3 1),
- (asm_simp_tac HOLCF_ss 1)
+ (asm_simp_tac HOLCF_ss 1)
]);
(* ------- (! k. b1`(iterate k g x)=TT) ==> q o p = q ----- *)
--- a/src/HOLCF/ex/Loop.ML Wed Oct 04 13:12:14 1995 +0100
+++ b/src/HOLCF/ex/Loop.ML Wed Oct 04 14:01:44 1995 +0100
@@ -16,14 +16,14 @@
"step`b`g`x = If b`x then g`x else x fi"
(fn prems =>
[
- (simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
val while_def2 = prove_goalw Loop.thy [while_def]
"while`b`g = fix`(LAM f x. If b`x then f`(g`x) else x fi)"
(fn prems =>
[
- (simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
@@ -36,15 +36,17 @@
(fn prems =>
[
(fix_tac5 while_def2 1),
- (simp_tac Cfun_ss 1)
+ (Simp_tac 1)
]);
+val HOLCF_ss = simpset_of "HOLCF";
+
val while_unfold2 = prove_goal Loop.thy
"!x.while`b`g`x = while`b`g`(iterate k (step`b`g) x)"
(fn prems =>
[
(nat_ind_tac "k" 1),
- (simp_tac (HOLCF_ss addsimps [iterate_0,iterate_Suc]) 1),
+ (simp_tac HOLCF_ss 1),
(rtac allI 1),
(rtac trans 1),
(rtac (while_unfold RS ssubst) 1),
@@ -74,7 +76,7 @@
(res_inst_tac [("s",
"while`b`g`(iterate (Suc 0) (step`b`g) x)")] trans 1),
(rtac (while_unfold2 RS spec) 1),
- (simp_tac iterate_ss 1)
+ (Simp_tac 1)
]);
@@ -87,7 +89,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(rtac trans 1),
(rtac step_def2 1),
(asm_simp_tac HOLCF_ss 1),
@@ -117,21 +119,23 @@
[
(cut_facts_tac prems 1),
(nat_ind_tac "k" 1),
- (asm_simp_tac iterate_ss 1),
+ (Asm_simp_tac 1),
(strip_tac 1),
- (simp_tac (iterate_ss addsimps [step_def2]) 1),
+ (simp_tac (!simpset addsimps [step_def2]) 1),
(res_inst_tac [("p","b`(iterate k1 (step`b`g) x)")] trE 1),
(etac notE 1),
- (asm_simp_tac (HOLCF_ss addsimps [step_def2,iterate_Suc] ) 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
+ (asm_simp_tac HOLCF_ss 1),
(rtac mp 1),
- (etac spec 1),
- (asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1),
+ (etac spec 1),
+ (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
+ addsimps [loop_lemma2] ) 1),
(res_inst_tac [("s","iterate (Suc k1) (step`b`g) x"),
("t","g`(iterate k1 (step`b`g) x)")] ssubst 1),
(atac 2),
- (asm_simp_tac (HOLCF_ss addsimps [iterate_Suc,step_def2] ) 1),
- (asm_simp_tac (HOLCF_ss addsimps [loop_lemma2] ) 1)
+ (asm_simp_tac (HOLCF_ss addsimps [step_def2] ) 1),
+ (asm_simp_tac (HOLCF_ss delsimps [iterate_Suc]
+ addsimps [loop_lemma2] ) 1)
]);
@@ -140,16 +144,16 @@
(fn prems =>
[
(nat_ind_tac "k" 1),
- (simp_tac iterate_ss 1),
+ (Simp_tac 1),
(strip_tac 1),
(rtac (while_unfold RS ssubst) 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
(rtac allI 1),
(rtac (iterate_Suc2 RS ssubst) 1),
(strip_tac 1),
(rtac trans 1),
(rtac while_unfold3 1),
- (asm_simp_tac HOLCF_ss 1)
+ (asm_simp_tac HOLCF_ss 1)
]);
val loop_lemma5 = prove_goal Loop.thy
@@ -163,12 +167,12 @@
(rtac (allI RS adm_all) 1),
(rtac adm_eq 1),
(cont_tacR 1),
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(rtac allI 1),
- (simp_tac HOLCF_ss 1),
+ (Simp_tac 1),
(res_inst_tac [("p","b`(iterate m (step`b`g) x)")] trE 1),
- (asm_simp_tac HOLCF_ss 1),
- (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
+ (asm_simp_tac HOLCF_ss 1),
(res_inst_tac [("s","xa`(iterate (Suc m) (step`b`g) x)")] trans 1),
(etac spec 2),
(rtac cfun_arg_cong 1),