--- a/src/HOLCF/Cfun3.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Cfun3.ML Fri Jan 31 13:57:33 1997 +0100
@@ -193,13 +193,15 @@
(* cont2cont tactic *)
(* ------------------------------------------------------------------------ *)
-val cont_lemmas = [cont_const, cont_id, cont_fapp2,
- cont2cont_fapp,cont2cont_LAM2];
+val cont_lemmas1 = [cont_const, cont_id, cont_fapp2,
+ cont2cont_fapp,cont2cont_LAM2];
+
+Addsimps cont_lemmas1;
-val cont_tac = (fn i => (resolve_tac cont_lemmas i));
+(*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
-val cont_tacR = (fn i => (REPEAT (cont_tac i)));
+(*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
(* ------------------------------------------------------------------------ *)
(* function application _[_] is strict in its first arguments *)
@@ -211,7 +213,7 @@
(stac inst_cfun_pcpo 1),
(rewtac UU_cfun_def),
(stac beta_cfun 1),
- (cont_tac 1),
+ (Simp_tac 1),
(rtac refl 1)
]);
@@ -350,29 +352,20 @@
(monofun_Istrictify2 RS monocontlub2cont));
-qed_goalw "strictify1" Cfun3.thy [strictify_def]
- "strictify`f`UU=UU"
- (fn prems =>
- [
+qed_goalw "strictify1" Cfun3.thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
(stac beta_cfun 1),
- (cont_tac 1),
- (rtac cont_Istrictify2 1),
- (rtac cont2cont_CF1L 1),
- (rtac cont_Istrictify1 1),
+ (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
+ cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_Istrictify2 1),
(rtac Istrictify1 1)
]);
qed_goalw "strictify2" Cfun3.thy [strictify_def]
- "~x=UU ==> strictify`f`x=f`x"
- (fn prems =>
- [
+ "~x=UU ==> strictify`f`x=f`x" (fn prems => [
(stac beta_cfun 1),
- (cont_tac 1),
- (rtac cont_Istrictify2 1),
- (rtac cont2cont_CF1L 1),
- (rtac cont_Istrictify1 1),
+ (simp_tac (!simpset addsimps [cont_Istrictify2,cont_Istrictify1,
+ cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_Istrictify2 1),
(rtac Istrictify2 1),
@@ -391,4 +384,4 @@
(* use cont_tac as autotac. *)
(* ------------------------------------------------------------------------ *)
-simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));
+(*simpset := !simpset addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
--- a/src/HOLCF/Cprod3.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Cprod3.ML Fri Jan 31 13:57:33 1997 +0100
@@ -148,10 +148,7 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tac 1),
- (rtac cont_pair2 1),
- (rtac cont2cont_CF1L 1),
- (rtac cont_pair1 1),
+ (simp_tac (!simpset addsimps [cont_pair1,cont_pair2,cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_pair2 1),
(rtac refl 1)
@@ -299,7 +296,6 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tacR 1),
(Simp_tac 1),
(simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
]);
@@ -309,7 +305,7 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
]);
--- a/src/HOLCF/Fix.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Fix.ML Fri Jan 31 13:57:33 1997 +0100
@@ -398,8 +398,7 @@
(rtac (fixdef RS fix_eq4) 1),
(rtac trans 1),
(rtac beta_cfun 1),
- (cont_tacR 1),
- (rtac refl 1)
+ (Simp_tac 1)
]);
(* use this one for definitions! *)
@@ -411,7 +410,7 @@
(rtac (fix_eq2) 1),
(rtac fixdef 1),
(rtac beta_cfun 1),
- (cont_tacR 1)
+ (Simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -1323,6 +1322,8 @@
etac adm_disj 1,
atac 1]);
-val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
+val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less];
+Addsimps adm_lemmas;
+
--- a/src/HOLCF/Lift3.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Lift3.ML Fri Jan 31 13:57:33 1997 +0100
@@ -224,17 +224,18 @@
val cont2cont_CF1L_rev2 = (allI RS cont2cont_CF1L_rev);
-val cont_lemmas = cont_lemmas@
+val cont_lemmas2 = cont_lemmas1@
[cont_flift1_arg,cont_flift2_arg,
cont_flift1_not_arg2,cont2cont_CF1L_rev2,
cont_fapp_app1,cont_fapp_app2,cont_if];
+Addsimps [cont_flift1_arg,cont_flift2_arg,
+ cont_flift1_not_arg2,cont2cont_CF1L_rev2,
+ cont_fapp_app1,cont_fapp_app2,cont_if];
-val cont_tac = (fn i => ((resolve_tac cont_lemmas i)));
-
-val cont_tacR = (fn i => ((simp_tac (!simpset
- addsimps [flift1_def,flift2_def]) i)
- THEN REPEAT (cont_tac i) ));
+fun cont_tac i = resolve_tac cont_lemmas2 i;
+fun cont_tacR i = simp_tac (!simpset addsimps [flift1_def,flift2_def]) i THEN
+ REPEAT (cont_tac i);
(* --------------------------------------------------------- *)
(* Admissibility tactic and tricks *)
@@ -253,10 +254,10 @@
val adm_tricks = [adm_trick_1,adm_trick_2];
-val adm_tac = (fn i => ((resolve_tac adm_thms i)));
-val adm_tacR = (fn i => (REPEAT (adm_tac i)));
-val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));
+(*val adm_tac = (fn i => ((resolve_tac adm_lemmas i)));*)
+(*val adm_tacR = (fn i => (REPEAT (adm_tac i)));*)
+(*val adm_cont_tac = (fn i => ((adm_tacR i) THEN (cont_tacR i)));*)
(* ----------------------------------------------------------------- *)
(* Relations between domains and terms using lift constructs *)
@@ -308,9 +309,6 @@
goal Lift3.thy "plift P`(Def y) = blift (P y)";
by (simp_tac (!simpset addsimps [plift_def,flift1_def]) 1);
-by (stac beta_cfun 1);
-by (cont_tacR 1);
-by (Simp_tac 1);
qed"plift2blift";
goal Lift3.thy
--- a/src/HOLCF/Sprod3.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Sprod3.ML Fri Jan 31 13:57:33 1997 +0100
@@ -320,10 +320,8 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tac 1),
- (rtac cont_Ispair2 1),
- (rtac cont2cont_CF1L 1),
- (rtac cont_Ispair1 1),
+ (simp_tac (!simpset addsimps [cont_Ispair2, cont_Ispair1,
+ cont2cont_CF1L]) 1),
(stac beta_cfun 1),
(rtac cont_Ispair2 1),
(rtac refl 1)
@@ -624,7 +622,7 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(stac strictify1 1),
(rtac refl 1)
]);
@@ -634,13 +632,13 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(stac strictify2 1),
(rtac defined_spair 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(stac sfst2 1),
(resolve_tac prems 1),
(stac ssnd2 1),
@@ -654,7 +652,7 @@
(fn prems =>
[
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(case_tac "z=UU" 1),
(hyp_subst_tac 1),
(rtac strictify1 1),
@@ -662,7 +660,7 @@
(rtac strictify2 1),
(atac 1),
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(rtac surjective_pairing_Sprod2 1)
]);
--- a/src/HOLCF/Ssum3.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Ssum3.ML Fri Jan 31 13:57:33 1997 +0100
@@ -486,101 +486,78 @@
]);
qed_goalw "sswhen1" Ssum3.thy [sswhen_def,sinl_def,sinr_def]
- "sswhen`f`g`UU = UU"
- (fn prems =>
- [
+ "sswhen`f`g`UU = UU" (fn _ => let
+val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2,
+ cont_Iwhen3,cont2cont_CF1L]) 1)) in
+ [
(stac inst_ssum_pcpo 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont2cont_CF1L]) 1)),
+ tac,
+ (stac beta_cfun 1),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont2cont_CF1L]) 1)),
- (stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont2cont_CF1L]) 1)),
+ tac,
(simp_tac Ssum0_ss 1)
- ]);
+ ] end);
+
+
+val tac = (REPEAT (resolve_tac (cont_lemmas1 @ [cont_Iwhen1,cont_Iwhen2,
+ cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1));
qed_goalw "sswhen2" Ssum3.thy [sswhen_def,sinl_def,sinr_def]
- "x~=UU==> sswhen`f`g`(sinl`x) = f`x"
- (fn prems =>
- [
+ "x~=UU==> sswhen`f`g`(sinl`x) = f`x" (fn prems => [
(cut_facts_tac prems 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(asm_simp_tac Ssum0_ss 1)
]);
-
-
qed_goalw "sswhen3" Ssum3.thy [sswhen_def,sinl_def,sinr_def]
- "x~=UU==> sswhen`f`g`(sinr`x) = g`x"
- (fn prems =>
- [
+ "x~=UU==> sswhen`f`g`(sinr`x) = g`x" (fn prems => [
(cut_facts_tac prems 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(asm_simp_tac Ssum0_ss 1)
]);
qed_goalw "less_ssum4a" Ssum3.thy [sinl_def,sinr_def]
- "(sinl`x << sinl`y) = (x << y)"
- (fn prems =>
- [
+ "(sinl`x << sinl`y) = (x << y)" (fn prems => [
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(rtac less_ssum3a 1)
]);
qed_goalw "less_ssum4b" Ssum3.thy [sinl_def,sinr_def]
- "(sinr`x << sinr`y) = (x << y)"
- (fn prems =>
- [
+ "(sinr`x << sinr`y) = (x << y)" (fn prems => [
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(rtac less_ssum3b 1)
]);
qed_goalw "less_ssum4c" Ssum3.thy [sinl_def,sinr_def]
- "(sinl`x << sinr`y) = (x = UU)"
- (fn prems =>
+ "(sinl`x << sinr`y) = (x = UU)" (fn prems =>
[
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(rtac less_ssum3c 1)
]);
@@ -589,11 +566,9 @@
(fn prems =>
[
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(rtac less_ssum3d 1)
]);
@@ -614,13 +589,13 @@
[
(cut_facts_tac prems 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac (beta_cfun RS ext) 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(rtac thelub_ssum1a 1),
(atac 1),
(rtac allI 1),
@@ -639,17 +614,13 @@
[
(cut_facts_tac prems 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(stac (beta_cfun RS ext) 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
- cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
+ tac,
(rtac thelub_ssum1b 1),
(atac 1),
(rtac allI 1),
--- a/src/HOLCF/Up3.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Up3.ML Fri Jan 31 13:57:33 1997 +0100
@@ -181,17 +181,17 @@
(asm_simp_tac (Up0_ss addsimps [cont_Iup]) 1)
]);
+val tac = (simp_tac (!simpset addsimps [cont_Iup,cont_Ifup1,
+ cont_Ifup2,cont2cont_CF1L]) 1);
qed_goalw "fup1" Up3.thy [up_def,fup_def] "fup`f`UU=UU"
(fn prems =>
[
(stac inst_up_pcpo 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
- cont_Ifup2,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
- cont_Ifup2,cont2cont_CF1L]) 1)),
+ tac,
(simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
]);
@@ -201,8 +201,7 @@
(stac beta_cfun 1),
(rtac cont_Iup 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
- cont_Ifup2,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
(rtac cont_Ifup2 1),
(simp_tac (Up0_ss addsimps [cont_Iup,cont_Ifup1,cont_Ifup2]) 1)
@@ -230,15 +229,11 @@
[
(cut_facts_tac prems 1),
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
- cont_Ifup2,cont2cont_CF1L]) 1)),
+ tac,
(stac beta_cfun 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
- cont_Ifup2,cont2cont_CF1L]) 1)),
-
+ tac,
(stac (beta_cfun RS ext) 1),
- (REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ifup1,
- cont_Ifup2,cont2cont_CF1L]) 1)),
+ tac,
(rtac thelub_up1a 1),
(atac 1),
(etac exE 1),
--- a/src/HOLCF/ccc1.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/ccc1.ML Fri Jan 31 13:57:33 1997 +0100
@@ -22,23 +22,19 @@
(rtac refl 1)
]);
-qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))"
- (fn prems =>
- [
+qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))" (fn _ => [
(stac beta_cfun 1),
- (cont_tacR 1),
+ (Simp_tac 1),
(stac beta_cfun 1),
- (cont_tacR 1),
- (rtac refl 1)
+ (Simp_tac 1),
+ (rtac refl 1)
]);
-qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)"
- (fn prems =>
- [
+qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)" (fn _ => [
(stac cfcomp1 1),
(stac beta_cfun 1),
- (cont_tacR 1),
- (rtac refl 1)
+ (Simp_tac 1),
+ (rtac refl 1)
]);