--- a/src/HOLCF/Cfun1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cfun1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -15,7 +15,7 @@
qed_goalw "CfunI" Cfun1.thy [Cfun_def] "(% x.x):Cfun"
(fn prems =>
[
- (rtac (mem_Collect_eq RS ssubst) 1),
+ (stac mem_Collect_eq 1),
(rtac cont_id 1)
]);
--- a/src/HOLCF/Cfun2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cfun2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -15,7 +15,7 @@
qed_goal "less_cfun" Cfun2.thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))"
(fn prems =>
[
- (rtac (inst_cfun_po RS ssubst) 1),
+ (stac inst_cfun_po 1),
(fold_goals_tac [less_cfun_def]),
(rtac refl 1)
]);
@@ -27,8 +27,8 @@
qed_goalw "minimal_cfun" Cfun2.thy [UU_cfun_def] "UU_cfun << f"
(fn prems =>
[
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac Abs_Cfun_inverse2 1),
(rtac cont_const 1),
(fold_goals_tac [UU_fun_def]),
(rtac minimal_fun 1)
@@ -112,10 +112,10 @@
qed_goal "strictI" Cfun2.thy "f`x = UU ==> f`UU = UU" (fn prems => [
- cut_facts_tac prems 1,
- rtac (eq_UU_iff RS iffD2) 1,
- etac subst 1,
- rtac (minimal RS monofun_cfun_arg) 1]);
+ cut_facts_tac prems 1,
+ rtac (eq_UU_iff RS iffD2) 1,
+ etac subst 1,
+ rtac (minimal RS monofun_cfun_arg) 1]);
(* ------------------------------------------------------------------------ *)
@@ -184,7 +184,7 @@
(etac lub_cfun_mono 1),
(rtac contlubI 1),
(strip_tac 1),
- (rtac (contlub_cfun_arg RS ext RS ssubst) 1),
+ (stac (contlub_cfun_arg RS ext) 1),
(atac 1),
(etac ex_lubcfun 1),
(atac 1)
@@ -203,14 +203,14 @@
(rtac conjI 1),
(rtac ub_rangeI 1),
(rtac allI 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac Abs_Cfun_inverse2 1),
(etac cont_lubcfun 1),
(rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
(strip_tac 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac Abs_Cfun_inverse2 1),
(etac cont_lubcfun 1),
(rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
@@ -255,9 +255,9 @@
(fn prems =>
[
(rtac (less_cfun RS iffD2) 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac Abs_Cfun_inverse2 1),
(resolve_tac prems 1),
- (rtac (Abs_Cfun_inverse2 RS ssubst) 1),
+ (stac Abs_Cfun_inverse2 1),
(resolve_tac prems 1),
(resolve_tac prems 1)
]);
--- a/src/HOLCF/Cfun3.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cfun3.ML Thu Sep 26 15:14:23 1996 +0200
@@ -17,11 +17,11 @@
(strip_tac 1),
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
- (rtac (thelub_cfun RS ssubst) 1),
+ (stac thelub_cfun 1),
(atac 1),
- (rtac (Cfunapp2 RS ssubst) 1),
+ (stac Cfunapp2 1),
(etac cont_lubcfun 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
(rtac refl 1)
]);
@@ -52,7 +52,7 @@
(cut_facts_tac prems 1),
(rtac trans 1),
(etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(etac (monofun_fapp1 RS ch2ch_monofun) 1),
(rtac refl 1)
]);
@@ -137,12 +137,12 @@
(cut_facts_tac prems 1),
(rtac monofunI 1),
(strip_tac 1),
- (rtac (less_cfun RS ssubst) 1),
- (rtac (less_fun RS ssubst) 1),
+ (stac less_cfun 1),
+ (stac less_fun 1),
(rtac allI 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(etac spec 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(etac spec 1),
(etac ((hd (tl prems)) RS spec RS monofunE RS spec RS spec RS mp) 1)
]);
@@ -162,7 +162,7 @@
(etac spec 1),
(rtac contlubI 1),
(strip_tac 1),
- (rtac (thelub_cfun RS ssubst) 1),
+ (stac thelub_cfun 1),
(rtac (cont2mono_LAM RS ch2ch_monofun) 1),
(atac 1),
(rtac (cont2mono RS allI) 1),
@@ -170,7 +170,7 @@
(atac 1),
(res_inst_tac [("f","fabs")] arg_cong 1),
(rtac ext 1),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac (beta_cfun RS ext) 1),
(etac spec 1),
(rtac (cont2contlub RS contlubE
RS spec RS mp ) 1),
@@ -208,9 +208,9 @@
qed_goal "strict_fapp1" Cfun3.thy "(UU::'a->'b)`x = (UU::'b)"
(fn prems =>
[
- (rtac (inst_cfun_pcpo RS ssubst) 1),
+ (stac inst_cfun_pcpo 1),
(rewtac UU_cfun_def),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tac 1),
(rtac refl 1)
]);
@@ -243,15 +243,15 @@
(rtac (less_fun RS iffD2) 1),
(strip_tac 1),
(res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
- (rtac (Istrictify2 RS ssubst) 1),
+ (stac Istrictify2 1),
(atac 1),
- (rtac (Istrictify2 RS ssubst) 1),
+ (stac Istrictify2 1),
(atac 1),
(rtac monofun_cfun_fun 1),
(atac 1),
(hyp_subst_tac 1),
- (rtac (Istrictify1 RS ssubst) 1),
- (rtac (Istrictify1 RS ssubst) 1),
+ (stac Istrictify1 1),
+ (stac Istrictify1 1),
(rtac refl_less 1)
]);
@@ -261,15 +261,15 @@
(rtac monofunI 1),
(strip_tac 1),
(res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
- (rtac (Istrictify2 RS ssubst) 1),
+ (stac Istrictify2 1),
(etac notUU_I 1),
(atac 1),
- (rtac (Istrictify2 RS ssubst) 1),
+ (stac Istrictify2 1),
(atac 1),
(rtac monofun_cfun_arg 1),
(atac 1),
(hyp_subst_tac 1),
- (rtac (Istrictify1 RS ssubst) 1),
+ (stac Istrictify1 1),
(rtac minimal 1)
]);
@@ -281,22 +281,22 @@
(strip_tac 1),
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(etac (monofun_Istrictify1 RS ch2ch_monofun) 1),
(res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
- (rtac (Istrictify2 RS ssubst) 1),
+ (stac Istrictify2 1),
(atac 1),
- (rtac (Istrictify2 RS ext RS ssubst) 1),
+ (stac (Istrictify2 RS ext) 1),
(atac 1),
- (rtac (thelub_cfun RS ssubst) 1),
+ (stac thelub_cfun 1),
(atac 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_lubcfun 1),
(atac 1),
(rtac refl 1),
(hyp_subst_tac 1),
- (rtac (Istrictify1 RS ssubst) 1),
- (rtac (Istrictify1 RS ext RS ssubst) 1),
+ (stac Istrictify1 1),
+ (stac (Istrictify1 RS ext) 1),
(rtac (chain_UU_I_inverse RS sym) 1),
(rtac (refl RS allI) 1)
]);
@@ -310,7 +310,7 @@
(res_inst_tac [("t","lub(range(Y))")] subst 1),
(rtac sym 1),
(atac 1),
- (rtac (Istrictify1 RS ssubst) 1),
+ (stac Istrictify1 1),
(rtac sym 1),
(rtac chain_UU_I_inverse 1),
(strip_tac 1),
@@ -320,7 +320,7 @@
(atac 1),
(atac 1),
(rtac Istrictify1 1),
- (rtac (Istrictify2 RS ssubst) 1),
+ (stac Istrictify2 1),
(atac 1),
(res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1),
(rtac contlub_cfun_arg 1),
@@ -354,12 +354,12 @@
"strictify`f`UU=UU"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tac 1),
(rtac cont_Istrictify2 1),
(rtac cont2cont_CF1L 1),
(rtac cont_Istrictify1 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Istrictify2 1),
(rtac Istrictify1 1)
]);
@@ -368,12 +368,12 @@
"~x=UU ==> strictify`f`x=f`x"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tac 1),
(rtac cont_Istrictify2 1),
(rtac cont2cont_CF1L 1),
(rtac cont_Istrictify1 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Istrictify2 1),
(rtac Istrictify2 1),
(resolve_tac prems 1)
--- a/src/HOLCF/Cont.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cont.ML Thu Sep 26 15:14:23 1996 +0200
@@ -379,9 +379,9 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
+ (stac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp) 1),
(atac 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1),
(atac 1),
(rtac trans 1),
@@ -456,7 +456,7 @@
(rtac ((hd prems) RS cont2contlub RS
contlubE RS spec RS mp RS ssubst) 1),
(atac 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(rtac ch2ch_monofun 1),
(etac cont2mono 1),
(atac 1),
@@ -489,7 +489,7 @@
(rtac contlubI 1),
(strip_tac 1),
(rtac ext 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1),
(etac spec 1),
(atac 1),
--- a/src/HOLCF/Cprod1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cprod1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -80,7 +80,7 @@
(dtac less_cprod2c 1),
(etac conjE 1),
(etac conjE 1),
- (rtac (Pair_eq RS ssubst) 1),
+ (stac Pair_eq 1),
(fast_tac (HOL_cs addSIs [antisym_less]) 1)
]);
@@ -98,7 +98,7 @@
(hyp_subst_tac 1),
(dtac less_cprod2c 1),
(dtac less_cprod2c 1),
- (rtac (less_cprod1b RS ssubst) 1),
+ (stac less_cprod1b 1),
(Simp_tac 1),
(etac conjE 1),
(etac conjE 1),
--- a/src/HOLCF/Cprod2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cprod2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -13,8 +13,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (inst_cprod_po RS ssubst) 1),
- (rtac (less_cprod1b RS ssubst) 1),
+ (stac inst_cprod_po 1),
+ (stac less_cprod1b 1),
(hyp_subst_tac 1),
(Asm_simp_tac 1)
]);
@@ -23,7 +23,7 @@
"(p1 << p2) = (fst(p1)<<fst(p2) & snd(p1)<<snd(p2))"
(fn prems =>
[
- (rtac (inst_cprod_po RS ssubst) 1),
+ (stac inst_cprod_po 1),
(rtac less_cprod1b 1)
]);
--- a/src/HOLCF/Cprod3.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Cprod3.ML Thu Sep 26 15:14:23 1996 +0200
@@ -40,7 +40,7 @@
(strip_tac 1),
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
- (rtac (lub_fun RS thelubI RS ssubst) 1),
+ (stac (lub_fun RS thelubI) 1),
(etac (monofun_pair1 RS ch2ch_monofun) 1),
(rtac trans 1),
(rtac (thelub_cprod RS sym) 2),
@@ -101,7 +101,7 @@
[
(rtac contlubI 1),
(strip_tac 1),
- (rtac (lub_cprod RS thelubI RS ssubst) 1),
+ (stac (lub_cprod RS thelubI) 1),
(atac 1),
(Simp_tac 1)
]);
@@ -111,7 +111,7 @@
[
(rtac contlubI 1),
(strip_tac 1),
- (rtac (lub_cprod RS thelubI RS ssubst) 1),
+ (stac (lub_cprod RS thelubI) 1),
(atac 1),
(Simp_tac 1)
]);
@@ -147,12 +147,12 @@
"(LAM x y.(x,y))`a`b = (a,b)"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tac 1),
(rtac cont_pair2 1),
(rtac cont2cont_CF1L 1),
(rtac cont_pair1 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_pair2 1),
(rtac refl 1)
]);
@@ -211,8 +211,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_cprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_cprod 1),
+ (stac beta_cfun 1),
(rtac cont_fst 1),
(Simp_tac 1)
]);
@@ -222,8 +222,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_cprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_cprod 1),
+ (stac beta_cfun 1),
(rtac cont_snd 1),
(Simp_tac 1)
]);
@@ -232,10 +232,10 @@
[cfst_def,csnd_def,cpair_def] "<cfst`p , csnd`p> = p"
(fn prems =>
[
- (rtac (beta_cfun_cprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_cprod 1),
+ (stac beta_cfun 1),
(rtac cont_snd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_fst 1),
(rtac (surjective_pairing RS sym) 1)
]);
@@ -245,13 +245,13 @@
" (p1 << p2) = (cfst`p1 << cfst`p2 & csnd`p1 << csnd`p2)"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_snd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_snd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_fst 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_fst 1),
(rtac less_cprod3b 1)
]);
@@ -274,10 +274,10 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_cprod RS ssubst) 1),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac beta_cfun_cprod 1),
+ (stac (beta_cfun RS ext) 1),
(rtac cont_snd 1),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac (beta_cfun RS ext) 1),
(rtac cont_fst 1),
(rtac lub_cprod 1),
(atac 1)
@@ -293,7 +293,7 @@
"csplit`f`<x,y> = f`x`y"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
(Simp_tac 1),
(simp_tac (!simpset addsimps [cfst2,csnd2]) 1)
@@ -303,7 +303,7 @@
"csplit`cpair`z=z"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
(simp_tac (!simpset addsimps [surjective_pairing_Cprod2]) 1)
]);
--- a/src/HOLCF/Fix.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Fix.ML Thu Sep 26 15:14:23 1996 +0200
@@ -31,10 +31,10 @@
[
(nat_ind_tac "n" 1),
(Simp_tac 1),
- (rtac (iterate_Suc RS ssubst) 1),
- (rtac (iterate_Suc RS ssubst) 1),
- (etac ssubst 1),
- (rtac refl 1)
+ (stac iterate_Suc 1),
+ (stac iterate_Suc 1),
+ (etac ssubst 1),
+ (rtac refl 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -74,7 +74,7 @@
qed_goalw "Ifix_eq" Fix.thy [Ifix_def] "Ifix F =F`(Ifix F)"
(fn prems =>
[
- (rtac (contlub_cfun_arg RS ssubst) 1),
+ (stac contlub_cfun_arg 1),
(rtac is_chain_iterate 1),
(rtac antisym_less 1),
(rtac lub_mono 1),
@@ -146,7 +146,7 @@
(rtac (lub_const RS thelubI RS sym) 1),
(Asm_simp_tac 1),
(rtac ext 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(rtac is_chainI 1),
(rtac allI 1),
(rtac (less_fun RS iffD2) 1),
@@ -159,7 +159,7 @@
(rtac ch2ch_fun 1),
(rtac (monofun_iterate RS ch2ch_monofun) 1),
(atac 1),
- (rtac (thelub_fun RS ssubst) 1),
+ (stac thelub_fun 1),
(rtac (monofun_iterate RS ch2ch_monofun) 1),
(atac 1),
(rtac contlub_cfun 1),
@@ -266,7 +266,7 @@
(rtac (monofun_iterate RS ch2ch_monofun) 1),
(atac 1),
(rtac fun_cong 1),
- (rtac (contlub_iterate RS contlubE RS spec RS mp RS ssubst) 1),
+ (stac (contlub_iterate RS contlubE RS spec RS mp) 1),
(atac 1),
(rtac refl 1)
]);
@@ -310,7 +310,7 @@
(fn prems =>
[
(strip_tac 1),
- (rtac (contlub_Ifix_lemma1 RS ext RS ssubst) 1),
+ (stac (contlub_Ifix_lemma1 RS ext) 1),
(atac 1),
(etac ex_lub_iterate 1)
]);
@@ -488,15 +488,15 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (fix_def2 RS ssubst) 1),
+ (stac fix_def2 1),
(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
(atac 1),
(rtac is_chain_iterate 1),
(rtac allI 1),
(nat_ind_tac "i" 1),
- (rtac (iterate_0 RS ssubst) 1),
+ (stac iterate_0 1),
(atac 1),
- (rtac (iterate_Suc RS ssubst) 1),
+ (stac iterate_Suc 1),
(resolve_tac prems 1),
(atac 1)
]);
@@ -510,7 +510,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (fix_def2 RS ssubst) 1),
+ (stac fix_def2 1),
(rtac (admw_def2 RS iffD1 RS spec RS mp) 1),
(atac 1),
(rtac allI 1),
@@ -531,7 +531,7 @@
(rtac mp 1),
(etac spec 1),
(atac 1),
- (rtac (lub_finch1 RS thelubI RS ssubst) 1),
+ (stac (lub_finch1 RS thelubI) 1),
(atac 1),
(atac 1),
(etac spec 1)
@@ -598,9 +598,9 @@
]);
qed_goalw "flat_eq" Fix.thy [is_flat_def]
- "[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
- (cut_facts_tac prems 1),
- (fast_tac (HOL_cs addIs [refl_less]) 1)]);
+ "[| is_flat (x::'a); (a::'a) ~= UU |] ==> a << b = (a = b)" (fn prems=>[
+ (cut_facts_tac prems 1),
+ (fast_tac (HOL_cs addIs [refl_less]) 1)]);
(* ------------------------------------------------------------------------ *)
(* lemmata for improved admissibility introdution rule *)
@@ -611,35 +611,35 @@
\ (!!Y. [| is_chain Y; !i. P (Y i); ~ finite_chain Y |] ==> P (lub (range Y)))\
\ |] ==> P (lub (range Y))"
(fn prems => [
- cut_facts_tac prems 1,
- case_tac "finite_chain Y" 1,
- eresolve_tac prems 2, atac 2, atac 2,
- rewtac finite_chain_def,
- safe_tac HOL_cs,
- etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
+ cut_facts_tac prems 1,
+ case_tac "finite_chain Y" 1,
+ eresolve_tac prems 2, atac 2, atac 2,
+ rewtac finite_chain_def,
+ safe_tac HOL_cs,
+ etac (lub_finch1 RS thelubI RS ssubst) 1, atac 1, etac spec 1]);
qed_goal "increasing_chain_adm_lemma" Porder.thy
"[|is_chain Y; !i. P (Y i); \
\ (!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j|]\
\ ==> P (lub (range Y))) |] ==> P (lub (range Y))"
(fn prems => [
- cut_facts_tac prems 1,
- etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
- rewtac finite_chain_def,
- safe_tac HOL_cs,
- etac swap 1,
- rewtac max_in_chain_def,
- resolve_tac prems 1, atac 1, atac 1,
- fast_tac (HOL_cs addDs [le_imp_less_or_eq]
- addEs [chain_mono RS mp]) 1]);
+ cut_facts_tac prems 1,
+ etac infinite_chain_adm_lemma 1, atac 1, etac thin_rl 1,
+ rewtac finite_chain_def,
+ safe_tac HOL_cs,
+ etac swap 1,
+ rewtac max_in_chain_def,
+ resolve_tac prems 1, atac 1, atac 1,
+ fast_tac (HOL_cs addDs [le_imp_less_or_eq]
+ addEs [chain_mono RS mp]) 1]);
qed_goalw "admI" Fix.thy [adm_def]
"(!!Y. [| is_chain Y; !i. P (Y i); !i. ? j. i < j & Y i ~= Y j & Y i << Y j |]\
\ ==> P(lub (range Y))) ==> adm P"
(fn prems => [
- strip_tac 1,
- etac increasing_chain_adm_lemma 1, atac 1,
- eresolve_tac prems 1, atac 1, atac 1]);
+ strip_tac 1,
+ etac increasing_chain_adm_lemma 1, atac 1,
+ eresolve_tac prems 1, atac 1, atac 1]);
(* ------------------------------------------------------------------------ *)
@@ -881,7 +881,7 @@
(cut_facts_tac prems 1),
(rtac (adm_def2 RS iffD2) 1),
(strip_tac 1),
- (rtac (cont2contlub RS contlubE RS spec RS mp RS ssubst) 1),
+ (stac (cont2contlub RS contlubE RS spec RS mp) 1),
(atac 1),
(atac 1),
(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
@@ -1000,7 +1000,7 @@
(hyp_subst_tac 1),
(Asm_simp_tac 1),
(Asm_simp_tac 1),
- (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
+ (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1)
]);
val adm_disj_lemma4 = prove_goal Fix.thy
@@ -1012,14 +1012,14 @@
(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),
+ ("t","if n<Suc(i) then Y(Suc(i)) else Y n")] ssubst 1),
(Asm_simp_tac 1),
(etac allE 1),
(rtac mp 1),
(atac 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),
+ ("t","if n<Suc(i) then Y(Suc(i)) else Y(n)")] ssubst 1),
(Asm_simp_tac 1),
(hyp_subst_tac 1),
(dtac spec 1),
@@ -1027,7 +1027,7 @@
(atac 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),
+ ("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),
(etac FalseE 2),
@@ -1061,7 +1061,7 @@
(rtac (not_less_eq RS iffD2) 1),
(atac 1),
(atac 1),
- (rtac (if_False RS ssubst) 1),
+ (stac if_False 1),
(rtac refl 1)
]);
@@ -1230,14 +1230,14 @@
qed_goal "adm_not_conj" Fix.thy
"[| adm (%x. ~ P x); adm (%x. ~ Q x) |] ==> adm (%x. ~ (P x & Q x))"(fn prems=>[
- cut_facts_tac prems 1,
- subgoal_tac
- "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
- rtac ext 2,
- fast_tac HOL_cs 2,
- etac ssubst 1,
- etac adm_disj 1,
- atac 1]);
+ cut_facts_tac prems 1,
+ subgoal_tac
+ "(%x. ~ (P x & Q x)) = (%x. ~ P x | ~ Q x)" 1,
+ rtac ext 2,
+ fast_tac HOL_cs 2,
+ etac ssubst 1,
+ etac adm_disj 1,
+ atac 1]);
val adm_thms = [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];
--- a/src/HOLCF/Fun1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Fun1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -23,7 +23,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (expand_fun_eq RS ssubst) 1),
+ (stac expand_fun_eq 1),
(fast_tac (HOL_cs addSIs [antisym_less]) 1)
]);
--- a/src/HOLCF/Fun2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Fun2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -15,7 +15,7 @@
qed_goalw "minimal_fun" Fun2.thy [UU_fun_def] "UU_fun << f"
(fn prems =>
[
- (rtac (inst_fun_po RS ssubst) 1),
+ (stac inst_fun_po 1),
(rewtac less_fun_def),
(fast_tac (HOL_cs addSIs [minimal]) 1)
]);
@@ -27,7 +27,7 @@
qed_goal "less_fun" Fun2.thy "(f1 << f2) = (! x. f1(x) << f2(x))"
(fn prems =>
[
- (rtac (inst_fun_po RS ssubst) 1),
+ (stac inst_fun_po 1),
(fold_goals_tac [less_fun_def]),
(rtac refl 1)
]);
@@ -80,12 +80,12 @@
(rtac conjI 1),
(rtac ub_rangeI 1),
(rtac allI 1),
- (rtac (less_fun RS ssubst) 1),
+ (stac less_fun 1),
(rtac allI 1),
(rtac is_ub_thelub 1),
(etac ch2ch_fun 1),
(strip_tac 1),
- (rtac (less_fun RS ssubst) 1),
+ (stac less_fun 1),
(rtac allI 1),
(rtac is_lub_thelub 1),
(etac ch2ch_fun 1),
--- a/src/HOLCF/Holcfb.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Holcfb.ML Thu Sep 26 15:14:23 1996 +0200
@@ -18,9 +18,9 @@
(* val de_morgan2 = de_Morgan_conj RS sym; "(~a | ~b)=(~(a & b))" *)
-(* val notall2ex = not_all "(~ (!x.P(x))) = (? x.~P(x))" *)
+(* val notall2ex = not_all "(~ (!x.P(x))) = (? x.~P(x))" *)
-(* val notex2all = not_ex "(~ (? x.P(x))) = (!x.~P(x))" *)
+(* val notex2all = not_ex "(~ (? x.P(x))) = (!x.~P(x))" *)
(* val selectI3 = select_eq_Ex RS iffD2 "(? x. P(x)) ==> P(@ x.P(x))" *)
--- a/src/HOLCF/Lift1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Lift1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -70,8 +70,8 @@
"Ilift(f)(UU_lift)=UU"
(fn prems =>
[
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (sum_case_Inl RS ssubst) 1),
+ (stac Abs_Lift_inverse 1),
+ (stac sum_case_Inl 1),
(rtac refl 1)
]);
@@ -79,8 +79,8 @@
"Ilift(f)(Iup(x))=f`x"
(fn prems =>
[
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (sum_case_Inr RS ssubst) 1),
+ (stac Abs_Lift_inverse 1),
+ (stac sum_case_Inr 1),
(rtac refl 1)
]);
@@ -90,8 +90,8 @@
"less_lift(UU_lift)(z)"
(fn prems =>
[
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (sum_case_Inl RS ssubst) 1),
+ (stac Abs_Lift_inverse 1),
+ (stac sum_case_Inl 1),
(rtac TrueI 1)
]);
@@ -102,10 +102,10 @@
(rtac notI 1),
(rtac iffD1 1),
(atac 2),
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (sum_case_Inr RS ssubst) 1),
- (rtac (sum_case_Inl RS ssubst) 1),
+ (stac Abs_Lift_inverse 1),
+ (stac Abs_Lift_inverse 1),
+ (stac sum_case_Inr 1),
+ (stac sum_case_Inl 1),
(rtac refl 1)
]);
@@ -113,10 +113,10 @@
"less_lift (Iup x) (Iup y)=(x<<y)"
(fn prems =>
[
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (Abs_Lift_inverse RS ssubst) 1),
- (rtac (sum_case_Inr RS ssubst) 1),
- (rtac (sum_case_Inr RS ssubst) 1),
+ (stac Abs_Lift_inverse 1),
+ (stac Abs_Lift_inverse 1),
+ (stac sum_case_Inr 1),
+ (stac sum_case_Inr 1),
(rtac refl 1)
]);
--- a/src/HOLCF/Lift2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Lift2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -15,7 +15,7 @@
qed_goal "minimal_lift" Lift2.thy "UU_lift << z"
(fn prems =>
[
- (rtac (inst_lift_po RS ssubst) 1),
+ (stac inst_lift_po 1),
(rtac less_lift1a 1)
]);
@@ -26,14 +26,14 @@
qed_goal "less_lift2b" Lift2.thy "~ Iup(x) << UU_lift"
(fn prems =>
[
- (rtac (inst_lift_po RS ssubst) 1),
+ (stac inst_lift_po 1),
(rtac less_lift1b 1)
]);
qed_goal "less_lift2c" Lift2.thy "(Iup(x)<<Iup(y)) = (x<<y)"
(fn prems =>
[
- (rtac (inst_lift_po RS ssubst) 1),
+ (stac inst_lift_po 1),
(rtac less_lift1c 1)
]);
--- a/src/HOLCF/Lift3.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Lift3.ML Thu Sep 26 15:14:23 1996 +0200
@@ -15,14 +15,14 @@
qed_goal "less_lift3b" Lift3.thy "~ Iup(x) << UU"
(fn prems =>
[
- (rtac (inst_lift_pcpo RS ssubst) 1),
+ (stac inst_lift_pcpo 1),
(rtac less_lift2b 1)
]);
qed_goal "defined_Iup2" Lift3.thy "Iup(x) ~= UU"
(fn prems =>
[
- (rtac (inst_lift_pcpo RS ssubst) 1),
+ (stac inst_lift_pcpo 1),
(rtac defined_Iup 1)
]);
@@ -83,11 +83,11 @@
(rtac contlubI 1),
(strip_tac 1),
(rtac disjE 1),
- (rtac (thelub_lift1a RS ssubst) 2),
+ (stac thelub_lift1a 2),
(atac 2),
(atac 2),
(asm_simp_tac Lift0_ss 2),
- (rtac (thelub_lift1b RS ssubst) 3),
+ (stac thelub_lift1b 3),
(atac 3),
(atac 3),
(fast_tac HOL_cs 1),
@@ -100,7 +100,7 @@
(dtac spec 2),
(etac spec 2),
(atac 2),
- (rtac (contlub_cfun_arg RS ssubst) 1),
+ (stac contlub_cfun_arg 1),
(etac (monofun_Ilift2 RS ch2ch_monofun) 1),
(rtac lub_equal2 1),
(rtac (monofun_fapp2 RS ch2ch_monofun) 2),
@@ -120,7 +120,7 @@
(asm_simp_tac Lift0_ss 2),
(res_inst_tac [("P","Y(i) = UU")] notE 1),
(fast_tac HOL_cs 1),
- (rtac (inst_lift_pcpo RS ssubst) 1),
+ (stac inst_lift_pcpo 1),
(atac 1)
]);
@@ -149,7 +149,7 @@
(fn prems =>
[
(simp_tac (Lift0_ss addsimps [cont_Iup]) 1),
- (rtac (inst_lift_pcpo RS ssubst) 1),
+ (stac inst_lift_pcpo 1),
(rtac Exh_Lift 1)
]);
@@ -185,11 +185,11 @@
qed_goalw "lift1" Lift3.thy [up_def,lift_def] "lift`f`UU=UU"
(fn prems =>
[
- (rtac (inst_lift_pcpo RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac inst_lift_pcpo 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
(simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
@@ -198,12 +198,12 @@
qed_goalw "lift2" Lift3.thy [up_def,lift_def] "lift`f`(up`x)=f`x"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Iup 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Ilift2 1),
(simp_tac (Lift0_ss addsimps [cont_Iup,cont_Ilift1,cont_Ilift2]) 1)
]);
@@ -229,14 +229,14 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac (beta_cfun RS ext) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iup,cont_Ilift1,
cont_Ilift2,cont2cont_CF1L]) 1)),
(rtac thelub_lift1a 1),
@@ -257,7 +257,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (inst_lift_pcpo RS ssubst) 1),
+ (stac inst_lift_pcpo 1),
(rtac thelub_lift1b 1),
(atac 1),
(strip_tac 1),
--- a/src/HOLCF/Pcpo.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Pcpo.ML Thu Sep 26 15:14:23 1996 +0200
@@ -162,7 +162,7 @@
qed_goal "UU_I" Pcpo.thy "x << UU ==> x = UU"
(fn prems =>
[
- (rtac (eq_UU_iff RS ssubst) 1),
+ (stac eq_UU_iff 1),
(resolve_tac prems 1)
]);
@@ -251,7 +251,7 @@
qed_goal "unique_void2" Pcpo.thy "(x::void)=UU"
(fn prems =>
[
- (rtac (inst_void_pcpo RS ssubst) 1),
+ (stac inst_void_pcpo 1),
(rtac (Rep_Void_inverse RS subst) 1),
(rtac (Rep_Void_inverse RS subst) 1),
(rtac arg_cong 1),
--- a/src/HOLCF/Porder.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Porder.ML Thu Sep 26 15:14:23 1996 +0200
@@ -62,7 +62,7 @@
(nat_ind_tac "y" 1),
(rtac impI 1),
(etac less_zeroE 1),
- (rtac (less_Suc_eq RS ssubst) 1),
+ (stac less_Suc_eq 1),
(strip_tac 1),
(etac disjE 1),
(rtac trans_less 1),
@@ -108,7 +108,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (lub RS ssubst) 1),
+ (stac lub 1),
(etac (select_eq_Ex RS iffD2) 1)
]);
@@ -123,7 +123,7 @@
"(? x. M <<| x) = M <<| lub(M)"
(fn prems =>
[
- (rtac (lub RS ssubst) 1),
+ (stac lub 1),
(rtac (select_eq_Ex RS subst) 1),
(rtac refl 1)
]);
@@ -134,7 +134,7 @@
[
(cut_facts_tac prems 1),
(rtac unique_lub 1),
- (rtac (lub RS ssubst) 1),
+ (stac lub 1),
(etac selectI 1),
(atac 1)
]);
@@ -217,7 +217,7 @@
qed_goal "less_void" Porder.thy "((u1::void) << u2) = (u1 = u2)"
(fn prems =>
[
- (rtac (inst_void_po RS ssubst) 1),
+ (stac inst_void_po 1),
(rewtac less_void_def),
(rtac iffI 1),
(rtac injD 1),
@@ -234,7 +234,7 @@
qed_goal "minimal_void" Porder.thy "UU_void << x"
(fn prems =>
[
- (rtac (inst_void_po RS ssubst) 1),
+ (stac inst_void_po 1),
(rewtac less_void_def),
(simp_tac (!simpset addsimps [unique_void]) 1)
]);
@@ -249,7 +249,7 @@
(rtac conjI 1),
(rewtac is_ub),
(strip_tac 1),
- (rtac (inst_void_po RS ssubst) 1),
+ (stac inst_void_po 1),
(rewtac less_void_def),
(simp_tac (!simpset addsimps [unique_void]) 1),
(strip_tac 1),
--- a/src/HOLCF/ROOT.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/ROOT.ML Thu Sep 26 15:14:23 1996 +0200
@@ -12,7 +12,7 @@
(* start 8bit 1 *)
val banner =
- "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
+ "HOLCF with sections axioms,ops,domain,generated and 8bit characters";
(* end 8bit 1 *)
writeln banner;
--- a/src/HOLCF/Sprod0.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Sprod0.ML Thu Sep 26 15:14:23 1996 +0200
@@ -225,7 +225,7 @@
"Isfst(Ispair UU y) = UU"
(fn prems =>
[
- (rtac (strict_Ispair1 RS ssubst) 1),
+ (stac strict_Ispair1 1),
(rtac strict_Isfst 1),
(rtac refl 1)
]);
@@ -234,7 +234,7 @@
"Isfst(Ispair x UU) = UU"
(fn prems =>
[
- (rtac (strict_Ispair2 RS ssubst) 1),
+ (stac strict_Ispair2 1),
(rtac strict_Isfst 1),
(rtac refl 1)
]);
@@ -259,7 +259,7 @@
"Issnd(Ispair UU y) = UU"
(fn prems =>
[
- (rtac (strict_Ispair1 RS ssubst) 1),
+ (stac strict_Ispair1 1),
(rtac strict_Issnd 1),
(rtac refl 1)
]);
@@ -268,7 +268,7 @@
"Issnd(Ispair x UU) = UU"
(fn prems =>
[
- (rtac (strict_Ispair2 RS ssubst) 1),
+ (stac strict_Ispair2 1),
(rtac strict_Issnd 1),
(rtac refl 1)
]);
--- a/src/HOLCF/Sprod1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Sprod1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -96,7 +96,7 @@
(res_inst_tac [("p","p")] IsprodE 1),
(etac less_sprod1a 1),
(hyp_subst_tac 1),
- (rtac (less_sprod1b RS ssubst) 1),
+ (stac less_sprod1b 1),
(rtac defined_Ispair 1),
(REPEAT (fast_tac (HOL_cs addIs [refl_less]) 1))
]);
@@ -146,7 +146,7 @@
(hyp_subst_tac 1),
(res_inst_tac [("Q","p2=Ispair(UU::'a)(UU::'b)")]
(excluded_middle RS disjE) 1),
- (rtac (defined_Ispair RS less_sprod1b RS ssubst) 1),
+ (stac (defined_Ispair RS less_sprod1b) 1),
(REPEAT (atac 1)),
(rtac conjI 1),
(res_inst_tac [("y","Isfst(p2)")] trans_less 1),
--- a/src/HOLCF/Sprod2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Sprod2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -18,7 +18,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (inst_sprod_po RS ssubst) 1),
+ (stac inst_sprod_po 1),
(etac less_sprod1a 1)
]);
@@ -29,7 +29,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (inst_sprod_po RS ssubst) 1),
+ (stac inst_sprod_po 1),
(etac less_sprod1b 1)
]);
@@ -84,17 +84,17 @@
(rtac (less_sprod3b RS iffD2) 1),
(atac 1),
(rtac conjI 1),
- (rtac (Isfst RS ssubst) 1),
+ (stac Isfst 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
- (rtac (Isfst RS ssubst) 1),
+ (stac Isfst 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
(atac 1),
- (rtac (Issnd RS ssubst) 1),
+ (stac Issnd 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
- (rtac (Issnd RS ssubst) 1),
+ (stac Issnd 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
(rtac refl_less 1),
@@ -122,17 +122,17 @@
(rtac (less_sprod3b RS iffD2) 1),
(atac 1),
(rtac conjI 1),
- (rtac (Isfst RS ssubst) 1),
+ (stac Isfst 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
- (rtac (Isfst RS ssubst) 1),
+ (stac Isfst 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
(rtac refl_less 1),
- (rtac (Issnd RS ssubst) 1),
+ (stac Issnd 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
- (rtac (Issnd RS ssubst) 1),
+ (stac Issnd 1),
(etac (strict_Ispair_rev RS conjunct1) 1),
(etac (strict_Ispair_rev RS conjunct2) 1),
(atac 1),
@@ -174,7 +174,7 @@
(hyp_subst_tac 1),
(rtac trans_less 1),
(rtac minimal 2),
- (rtac (strict_Isfst1 RS ssubst) 1),
+ (stac strict_Isfst1 1),
(rtac refl_less 1),
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] IsprodE 1),
@@ -183,10 +183,10 @@
(rtac refl_less 2),
(etac (less_sprod4b RS sym RS arg_cong) 1),
(hyp_subst_tac 1),
- (rtac (Isfst RS ssubst) 1),
+ (stac Isfst 1),
(atac 1),
(atac 1),
- (rtac (Isfst RS ssubst) 1),
+ (stac Isfst 1),
(atac 1),
(atac 1),
(etac (less_sprod4c RS conjunct1) 1),
@@ -201,7 +201,7 @@
(hyp_subst_tac 1),
(rtac trans_less 1),
(rtac minimal 2),
- (rtac (strict_Issnd1 RS ssubst) 1),
+ (stac strict_Issnd1 1),
(rtac refl_less 1),
(hyp_subst_tac 1),
(res_inst_tac [("p","y")] IsprodE 1),
@@ -210,10 +210,10 @@
(rtac refl_less 2),
(etac (less_sprod4b RS sym RS arg_cong) 1),
(hyp_subst_tac 1),
- (rtac (Issnd RS ssubst) 1),
+ (stac Issnd 1),
(atac 1),
(atac 1),
- (rtac (Issnd RS ssubst) 1),
+ (stac Issnd 1),
(atac 1),
(atac 1),
(etac (less_sprod4c RS conjunct2) 1),
--- a/src/HOLCF/Sprod3.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Sprod3.ML Thu Sep 26 15:14:23 1996 +0200
@@ -98,7 +98,7 @@
(strip_tac 1),
(rtac (expand_fun_eq RS iffD2) 1),
(strip_tac 1),
- (rtac (lub_fun RS thelubI RS ssubst) 1),
+ (stac (lub_fun RS thelubI) 1),
(etac (monofun_Ispair1 RS ch2ch_monofun) 1),
(rtac trans 1),
(rtac (thelub_sprod RS sym) 2),
@@ -237,7 +237,7 @@
[
(rtac contlubI 1),
(strip_tac 1),
- (rtac (lub_sprod RS thelubI RS ssubst) 1),
+ (stac (lub_sprod RS thelubI) 1),
(atac 1),
(res_inst_tac [("Q","lub(range(%i. Issnd(Y(i))))=UU")]
(excluded_middle RS disjE) 1),
@@ -253,16 +253,16 @@
(rtac strict_Isfst 1),
(rtac swap 1),
(etac (defined_IsfstIssnd RS conjunct2) 2),
- (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS
- chain_UU_I RS spec]) 1)
- ]);
+ (fast_tac (HOL_cs addSDs [monofun_Issnd RS ch2ch_monofun RS
+ chain_UU_I RS spec]) 1)
+ ]);
qed_goal "contlub_Issnd" Sprod3.thy "contlub(Issnd)"
(fn prems =>
[
(rtac contlubI 1),
(strip_tac 1),
- (rtac (lub_sprod RS thelubI RS ssubst) 1),
+ (stac (lub_sprod RS thelubI) 1),
(atac 1),
(res_inst_tac [("Q","lub(range(%i. Isfst(Y(i))))=UU")]
(excluded_middle RS disjE) 1),
@@ -278,8 +278,8 @@
(rtac swap 1),
(etac (defined_IsfstIssnd RS conjunct1) 2),
(fast_tac (HOL_cs addSDs [monofun_Isfst RS ch2ch_monofun RS
- chain_UU_I RS spec]) 1)
- ]);
+ chain_UU_I RS spec]) 1)
+ ]);
qed_goal "cont_Isfst" Sprod3.thy "cont(Isfst)"
(fn prems =>
@@ -319,12 +319,12 @@
"(LAM x y.Ispair x y)`a`b = Ispair a b"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tac 1),
(rtac cont_Ispair2 1),
(rtac cont2cont_CF1L 1),
(rtac cont_Ispair1 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Ispair2 1),
(rtac refl 1)
]);
@@ -366,7 +366,7 @@
qed_goalw "strict_spair1" Sprod3.thy [spair_def] "(|UU,b|) = UU"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
(rtac trans 1),
(rtac (inst_sprod_pcpo RS sym) 2),
(rtac strict_Ispair1 1)
@@ -375,7 +375,7 @@
qed_goalw "strict_spair2" Sprod3.thy [spair_def] "(|a,UU|) = UU"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
(rtac trans 1),
(rtac (inst_sprod_pcpo RS sym) 2),
(rtac strict_Ispair2 1)
@@ -408,8 +408,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (inst_sprod_pcpo RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac inst_sprod_pcpo 1),
(etac defined_Ispair 1),
(atac 1)
]);
@@ -420,7 +420,7 @@
[
(rtac (Exh_Sprod RS disjE) 1),
(rtac disjI1 1),
- (rtac (inst_sprod_pcpo RS ssubst) 1),
+ (stac inst_sprod_pcpo 1),
(atac 1),
(rtac disjI2 1),
(etac exE 1),
@@ -428,7 +428,7 @@
(rtac exI 1),
(rtac exI 1),
(rtac conjI 1),
- (rtac (beta_cfun_sprod RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
(fast_tac HOL_cs 1),
(fast_tac HOL_cs 1)
]);
@@ -440,12 +440,12 @@
[
(rtac IsprodE 1),
(resolve_tac prems 1),
- (rtac (inst_sprod_pcpo RS ssubst) 1),
+ (stac inst_sprod_pcpo 1),
(atac 1),
(resolve_tac prems 1),
(atac 2),
(atac 2),
- (rtac (beta_cfun_sprod RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
(atac 1)
]);
@@ -455,7 +455,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(rtac strict_Isfst 1),
(rtac (inst_sprod_pcpo RS subst) 1),
@@ -466,8 +466,8 @@
"sfst`(|UU,y|) = UU"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(rtac strict_Isfst1 1)
]);
@@ -476,8 +476,8 @@
"sfst`(|x,UU|) = UU"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(rtac strict_Isfst2 1)
]);
@@ -487,7 +487,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
(rtac strict_Issnd 1),
(rtac (inst_sprod_pcpo RS subst) 1),
@@ -498,8 +498,8 @@
"ssnd`(|UU,y|) = UU"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
(rtac strict_Issnd1 1)
]);
@@ -508,8 +508,8 @@
"ssnd`(|x,UU|) = UU"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
(rtac strict_Issnd2 1)
]);
@@ -519,8 +519,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(etac Isfst2 1)
]);
@@ -530,8 +530,8 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
(etac Issnd2 1)
]);
@@ -542,9 +542,9 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(rtac defined_IsfstIssnd 1),
(rtac (inst_sprod_pcpo RS subst) 1),
@@ -556,10 +556,10 @@
[sfst_def,ssnd_def,spair_def] "(|sfst`p , ssnd`p|) = p"
(fn prems =>
[
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(rtac (surjective_pairing_Sprod RS sym) 1)
]);
@@ -570,13 +570,13 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Issnd 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isfst 1),
(rtac less_sprod3b 1),
(rtac (inst_sprod_pcpo RS subst) 1),
@@ -602,10 +602,10 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun_sprod RS ssubst) 1),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac beta_cfun_sprod 1),
+ (stac (beta_cfun RS ext) 1),
(rtac cont_Issnd 1),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac (beta_cfun RS ext) 1),
(rtac cont_Isfst 1),
(rtac lub_sprod 1),
(resolve_tac prems 1)
@@ -623,9 +623,9 @@
"ssplit`f`UU=UU"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
- (rtac (strictify1 RS ssubst) 1),
+ (stac strictify1 1),
(rtac refl 1)
]);
@@ -633,17 +633,17 @@
"[|x~=UU;y~=UU|] ==> ssplit`f`(|x,y|)= f`x`y"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
- (rtac (strictify2 RS ssubst) 1),
+ (stac strictify2 1),
(rtac defined_spair 1),
(resolve_tac prems 1),
(resolve_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
- (rtac (sfst2 RS ssubst) 1),
+ (stac sfst2 1),
(resolve_tac prems 1),
- (rtac (ssnd2 RS ssubst) 1),
+ (stac ssnd2 1),
(resolve_tac prems 1),
(rtac refl 1)
]);
@@ -653,7 +653,7 @@
"ssplit`spair`z=z"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
(case_tac "z=UU" 1),
(hyp_subst_tac 1),
@@ -661,7 +661,7 @@
(rtac trans 1),
(rtac strictify2 1),
(atac 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
(rtac surjective_pairing_Sprod2 1)
]);
--- a/src/HOLCF/Ssum2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Ssum2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -16,7 +16,7 @@
"(Isinl(x) << Isinl(y)) = (x << y)"
(fn prems =>
[
- (rtac (inst_ssum_po RS ssubst) 1),
+ (stac inst_ssum_po 1),
(rtac less_ssum2a 1)
]);
@@ -24,7 +24,7 @@
"(Isinr(x) << Isinr(y)) = (x << y)"
(fn prems =>
[
- (rtac (inst_ssum_po RS ssubst) 1),
+ (stac inst_ssum_po 1),
(rtac less_ssum2b 1)
]);
@@ -32,7 +32,7 @@
"(Isinl(x) << Isinr(y)) = (x = UU)"
(fn prems =>
[
- (rtac (inst_ssum_po RS ssubst) 1),
+ (stac inst_ssum_po 1),
(rtac less_ssum2c 1)
]);
@@ -40,7 +40,7 @@
"(Isinr(x) << Isinl(y)) = (x = UU)"
(fn prems =>
[
- (rtac (inst_ssum_po RS ssubst) 1),
+ (stac inst_ssum_po 1),
(rtac less_ssum2d 1)
]);
@@ -57,7 +57,7 @@
(rtac (less_ssum3a RS iffD2) 1),
(rtac minimal 1),
(hyp_subst_tac 1),
- (rtac (strict_IsinlIsinr RS ssubst) 1),
+ (stac strict_IsinlIsinr 1),
(rtac (less_ssum3b RS iffD2) 1),
(rtac minimal 1)
]);
--- a/src/HOLCF/Ssum3.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Ssum3.ML Thu Sep 26 15:14:23 1996 +0200
@@ -226,7 +226,7 @@
(rtac (chain_mono2 RS exE) 1),
(atac 2),
(rtac chain_UU_I_inverse2 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
(etac swap 1),
(rtac inject_Isinl 1),
(rtac trans 1),
@@ -244,14 +244,14 @@
(rtac Iwhen2 1),
(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
(fast_tac HOL_cs 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
- (rtac (Iwhen2 RS ssubst) 1),
+ (stac Iwhen2 1),
(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
(fast_tac HOL_cs 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
@@ -285,7 +285,7 @@
(rtac (chain_mono2 RS exE) 1),
(atac 2),
(rtac chain_UU_I_inverse2 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
(etac swap 1),
(rtac inject_Isinr 1),
(rtac trans 1),
@@ -305,17 +305,17 @@
(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
(fast_tac HOL_cs 1),
(dtac notnotD 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
- (rtac (strict_IsinlIsinr RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
+ (stac strict_IsinlIsinr 1),
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
- (rtac (Iwhen3 RS ssubst) 1),
+ (stac Iwhen3 1),
(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
(fast_tac HOL_cs 1),
(dtac notnotD 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
- (rtac (strict_IsinlIsinr RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
+ (stac strict_IsinlIsinr 1),
(res_inst_tac [("t","Y(i)")] ssubst 1),
(atac 1),
(fast_tac HOL_cs 1),
@@ -425,7 +425,7 @@
(cut_facts_tac prems 1),
(etac swap 1),
(rtac inject_sinl 1),
- (rtac (strict_sinl RS ssubst) 1),
+ (stac strict_sinl 1),
(etac notnotD 1)
]);
@@ -436,7 +436,7 @@
(cut_facts_tac prems 1),
(etac swap 1),
(rtac inject_sinr 1),
- (rtac (strict_sinr RS ssubst) 1),
+ (stac strict_sinr 1),
(etac notnotD 1)
]);
@@ -445,7 +445,7 @@
(fn prems =>
[
(asm_simp_tac (Ssum0_ss addsimps [cont_Isinr,cont_Isinl]) 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
(rtac Exh_Ssum 1)
]);
@@ -458,7 +458,7 @@
[
(rtac IssumE 1),
(resolve_tac prems 1),
- (rtac (inst_ssum_pcpo RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
(atac 1),
(resolve_tac prems 1),
(atac 2),
@@ -476,11 +476,11 @@
[
(rtac IssumE2 1),
(resolve_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isinl 1),
(atac 1),
(resolve_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_Isinr 1),
(atac 1)
]);
@@ -489,14 +489,14 @@
"sswhen`f`g`UU = UU"
(fn prems =>
[
- (rtac (inst_ssum_pcpo RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac inst_ssum_pcpo 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont2cont_CF1L]) 1)),
(simp_tac Ssum0_ss 1)
@@ -507,16 +507,16 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(asm_simp_tac Ssum0_ss 1)
@@ -529,16 +529,16 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(asm_simp_tac Ssum0_ss 1)
@@ -549,10 +549,10 @@
"(sinl`x << sinl`y) = (x << y)"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(rtac less_ssum3a 1)
@@ -562,10 +562,10 @@
"(sinr`x << sinr`y) = (x << y)"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(rtac less_ssum3b 1)
@@ -575,10 +575,10 @@
"(sinl`x << sinr`y) = (x = UU)"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(rtac less_ssum3c 1)
@@ -588,10 +588,10 @@
"(sinr`x << sinl`y) = (x = UU)"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(rtac less_ssum3d 1)
@@ -613,13 +613,13 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac (beta_cfun RS ext) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2, cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(rtac thelub_ssum1a 1),
(atac 1),
@@ -638,16 +638,16 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
- (rtac (beta_cfun RS ext RS ssubst) 1),
+ (stac (beta_cfun RS ext) 1),
(REPEAT (resolve_tac (cont_lemmas @ [cont_Iwhen1,cont_Iwhen2,
cont_Iwhen3,cont_Isinl,cont_Isinr,cont2cont_CF1L]) 1)),
(rtac thelub_ssum1b 1),
--- a/src/HOLCF/Tr1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Tr1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -23,7 +23,7 @@
(rtac (rep_tr_iso RS subst) 1),
(rtac (rep_tr_iso RS subst) 1),
(rtac cfun_arg_cong 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
+ (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
(etac (eq_UU_iff RS ssubst) 1)
]),
prove_goalw Tr1.thy [FF_def] "~FF << UU"
@@ -36,7 +36,7 @@
(rtac (rep_tr_iso RS subst) 1),
(rtac (rep_tr_iso RS subst) 1),
(rtac cfun_arg_cong 1),
- (rtac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2 RS ssubst) 1),
+ (stac ((abs_tr_iso RS allI) RS ((rep_tr_iso RS allI) RS iso_strict ) RS conjunct2) 1),
(etac (eq_UU_iff RS ssubst) 1)
]),
prove_goalw Tr1.thy [FF_def,TT_def] "~TT << FF"
--- a/src/HOLCF/Void.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/Void.ML Thu Sep 26 15:14:23 1996 +0200
@@ -19,7 +19,7 @@
" UU_void_Rep : Void"
(fn prems =>
[
- (rtac (mem_Collect_eq RS ssubst) 1),
+ (stac mem_Collect_eq 1),
(rtac refl 1)
]);
--- a/src/HOLCF/ccc1.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/ccc1.ML Thu Sep 26 15:14:23 1996 +0200
@@ -17,7 +17,7 @@
qed_goalw "ID1" ccc1.thy [ID_def] "ID`x=x"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(rtac cont_id 1),
(rtac refl 1)
]);
@@ -25,9 +25,9 @@
qed_goalw "cfcomp1" ccc1.thy [oo_def] "(f oo g)=(LAM x.f`(g`x))"
(fn prems =>
[
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
(rtac refl 1)
]);
@@ -35,8 +35,8 @@
qed_goal "cfcomp2" ccc1.thy "(f oo g)`x=f`(g`x)"
(fn prems =>
[
- (rtac (cfcomp1 RS ssubst) 1),
- (rtac (beta_cfun RS ssubst) 1),
+ (stac cfcomp1 1),
+ (stac beta_cfun 1),
(cont_tacR 1),
(rtac refl 1)
]);
@@ -55,8 +55,8 @@
(fn prems =>
[
(rtac ext_cfun 1),
- (rtac (cfcomp2 RS ssubst) 1),
- (rtac (ID1 RS ssubst) 1),
+ (stac cfcomp2 1),
+ (stac ID1 1),
(rtac refl 1)
]);
@@ -64,8 +64,8 @@
(fn prems =>
[
(rtac ext_cfun 1),
- (rtac (cfcomp2 RS ssubst) 1),
- (rtac (ID1 RS ssubst) 1),
+ (stac cfcomp2 1),
+ (stac ID1 1),
(rtac refl 1)
]);
@@ -75,11 +75,11 @@
[
(rtac ext_cfun 1),
(res_inst_tac [("s","f`(g`(h`x))")] trans 1),
- (rtac (cfcomp2 RS ssubst) 1),
- (rtac (cfcomp2 RS ssubst) 1),
+ (stac cfcomp2 1),
+ (stac cfcomp2 1),
(rtac refl 1),
- (rtac (cfcomp2 RS ssubst) 1),
- (rtac (cfcomp2 RS ssubst) 1),
+ (stac cfcomp2 1),
+ (stac cfcomp2 1),
(rtac refl 1)
]);
--- a/src/HOLCF/domain/theorems.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/domain/theorems.ML Thu Sep 26 15:14:23 1996 +0200
@@ -29,56 +29,56 @@
(* ----- general proof facilities ------------------------------------------- *)
fun inferT sg pre_tm = #2 (Sign.infer_types sg (K None) (K None) [] true
- ([pre_tm],propT));
+ ([pre_tm],propT));
fun pg'' thy defs t = let val sg = sign_of thy;
- val ct = Thm.cterm_of sg (inferT sg t);
- in prove_goalw_cterm defs ct end;
+ val ct = Thm.cterm_of sg (inferT sg t);
+ in prove_goalw_cterm defs ct end;
fun pg' thy defs t tacsf=pg'' thy defs t (fn [] => tacsf
- | prems=> (cut_facts_tac prems 1)::tacsf);
+ | prems=> (cut_facts_tac prems 1)::tacsf);
fun REPEAT_DETERM_UNTIL p tac =
let fun drep st = if p st then Sequence.single st
- else (case Sequence.pull(tac st) of
- None => Sequence.null
- | Some(st',_) => drep st')
+ else (case Sequence.pull(tac st) of
+ None => Sequence.null
+ | Some(st',_) => drep st')
in drep end;
val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn _ => [rtac TrueI 1]) in
val kill_neq_tac = dtac trueI2 end;
-fun case_UU_tac rews i v = case_tac (v^"=UU") i THEN
- asm_simp_tac (HOLCF_ss addsimps rews) i;
+fun case_UU_tac rews i v = case_tac (v^"=UU") i THEN
+ asm_simp_tac (HOLCF_ss addsimps rews) i;
val chain_tac = REPEAT_DETERM o resolve_tac
- [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
+ [is_chain_iterate, ch2ch_fappR, ch2ch_fappL];
(* ----- general proofs ----------------------------------------------------- *)
val quant_ss = HOL_ss addsimps (map (fn s => prove_goal HOL.thy s (fn _ =>[
- fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
- "(!x. P & Q x) = (P & (!x. Q x))"]);
+ fast_tac HOL_cs 1]))["(!x. P x & Q)=((!x. P x) & Q)",
+ "(!x. P & Q x) = (P & (!x. Q x))"]);
val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
(fn prems =>[
- resolve_tac prems 1,
- cut_facts_tac prems 1,
- fast_tac HOL_cs 1]);
+ resolve_tac prems 1,
+ cut_facts_tac prems 1,
+ fast_tac HOL_cs 1]);
val swap3 = prove_goal HOL.thy "[| Q ==> P; ~P |] ==> ~Q" (fn prems => [
cut_facts_tac prems 1,
etac swap 1,
dtac notnotD 1,
- etac (hd prems) 1]);
+ etac (hd prems) 1]);
val dist_eqI = prove_goal Porder.thy "~ x << y ==> x ~= y" (fn prems => [
rtac swap3 1,
- etac (antisym_less_inverse RS conjunct1) 1,
- resolve_tac prems 1]);
+ etac (antisym_less_inverse RS conjunct1) 1,
+ resolve_tac prems 1]);
val cfst_strict = prove_goal Cprod3.thy "cfst`UU = UU" (fn _ => [
- (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
+ (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
val csnd_strict = prove_goal Cprod3.thy "csnd`UU = UU" (fn _ => [
- (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
+ (simp_tac (HOLCF_ss addsimps [inst_cprod_pcpo2]) 1)]);
in
@@ -93,8 +93,8 @@
val b = 0;
fun _ y t = by t;
fun g defs t = let val sg = sign_of thy;
- val ct = Thm.cterm_of sg (inferT sg t);
- in goalw_cterm defs ct end;
+ val ct = Thm.cterm_of sg (inferT sg t);
+ in goalw_cterm defs ct end;
*)
@@ -107,7 +107,7 @@
val axs_con_def = map (fn (con,_) => ga (extern_name con ^"_def")) cons;
val axs_dis_def = map (fn (con,_) => ga ( dis_name con ^"_def")) cons;
val axs_sel_def = flat(map (fn (_,args) =>
- map (fn arg => ga (sel_of arg ^"_def")) args)cons);
+ map (fn arg => ga (sel_of arg ^"_def")) args)cons);
val ax_copy_def = ga (dname^"_copy_def" );
end; (* local *)
@@ -119,71 +119,71 @@
val x_name = "x";
val (rep_strict, abs_strict) = let
- val r = ax_rep_iso RS (ax_abs_iso RS (allI RSN(2,allI RS iso_strict)))
- in (r RS conjunct1, r RS conjunct2) end;
+ val r = ax_rep_iso RS (ax_abs_iso RS (allI RSN(2,allI RS iso_strict)))
+ in (r RS conjunct1, r RS conjunct2) end;
val abs_defin' = pg [] ((dc_abs`%x_name === UU) ==> (%x_name === UU)) [
- res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
- etac ssubst 1, rtac rep_strict 1];
+ res_inst_tac [("t",x_name)] (ax_abs_iso RS subst) 1,
+ etac ssubst 1, rtac rep_strict 1];
val rep_defin' = pg [] ((dc_rep`%x_name === UU) ==> (%x_name === UU)) [
- res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
- etac ssubst 1, rtac abs_strict 1];
+ res_inst_tac [("t",x_name)] (ax_rep_iso RS subst) 1,
+ etac ssubst 1, rtac abs_strict 1];
val iso_rews = [ax_abs_iso,ax_rep_iso,abs_strict,rep_strict];
local
val iso_swap = pg [] (dc_rep`%"x" === %"y" ==> %"x" === dc_abs`%"y") [
- dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
- etac (ax_rep_iso RS subst) 1];
+ dres_inst_tac [("f",dname^"_abs")] cfun_arg_cong 1,
+ etac (ax_rep_iso RS subst) 1];
fun exh foldr1 cn quant foldr2 var = let
fun one_con (con,args) = let val vns = map vname args in
foldr quant (vns, foldr2 ((%x_name === con_app2 con (var vns) vns)::
- map (defined o (var vns)) (nonlazy args))) end
+ map (defined o (var vns)) (nonlazy args))) end
in foldr1 ((cn(%x_name===UU))::map one_con cons) end;
in
val cases = let
- fun common_tac thm = rtac thm 1 THEN contr_tac 1;
- fun unit_tac true = common_tac liftE1
- | unit_tac _ = all_tac;
- fun prod_tac [] = common_tac oneE
- | prod_tac [arg] = unit_tac (is_lazy arg)
- | prod_tac (arg::args) =
- common_tac sprodE THEN
- kill_neq_tac 1 THEN
- unit_tac (is_lazy arg) THEN
- prod_tac args;
- fun sum_rest_tac p = SELECT_GOAL(EVERY[
- rtac p 1,
- rewrite_goals_tac axs_con_def,
- dtac iso_swap 1,
- simp_tac HOLCF_ss 1,
- UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
- fun sum_tac [(_,args)] [p] =
- prod_tac args THEN sum_rest_tac p
- | sum_tac ((_,args)::cons') (p::prems) = DETERM(
- common_tac ssumE THEN
- kill_neq_tac 1 THEN kill_neq_tac 2 THEN
- prod_tac args THEN sum_rest_tac p) THEN
- sum_tac cons' prems
- | sum_tac _ _ = Imposs "theorems:sum_tac";
- in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
- (fn T => T ==> %"P") mk_All
- (fn l => foldr (op ===>) (map mk_trp l,
- mk_trp(%"P")))
- bound_arg)
- (fn prems => [
- cut_facts_tac [excluded_middle] 1,
- etac disjE 1,
- rtac (hd prems) 2,
- etac rep_defin' 2,
- if length cons = 1 andalso
- length (snd(hd cons)) = 1 andalso
- not(is_lazy(hd(snd(hd cons))))
- then rtac (hd (tl prems)) 1 THEN atac 2 THEN
- rewrite_goals_tac axs_con_def THEN
- simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
- else sum_tac cons (tl prems)])end;
+ fun common_tac thm = rtac thm 1 THEN contr_tac 1;
+ fun unit_tac true = common_tac liftE1
+ | unit_tac _ = all_tac;
+ fun prod_tac [] = common_tac oneE
+ | prod_tac [arg] = unit_tac (is_lazy arg)
+ | prod_tac (arg::args) =
+ common_tac sprodE THEN
+ kill_neq_tac 1 THEN
+ unit_tac (is_lazy arg) THEN
+ prod_tac args;
+ fun sum_rest_tac p = SELECT_GOAL(EVERY[
+ rtac p 1,
+ rewrite_goals_tac axs_con_def,
+ dtac iso_swap 1,
+ simp_tac HOLCF_ss 1,
+ UNTIL_SOLVED(fast_tac HOL_cs 1)]) 1;
+ fun sum_tac [(_,args)] [p] =
+ prod_tac args THEN sum_rest_tac p
+ | sum_tac ((_,args)::cons') (p::prems) = DETERM(
+ common_tac ssumE THEN
+ kill_neq_tac 1 THEN kill_neq_tac 2 THEN
+ prod_tac args THEN sum_rest_tac p) THEN
+ sum_tac cons' prems
+ | sum_tac _ _ = Imposs "theorems:sum_tac";
+ in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%"P")))
+ (fn T => T ==> %"P") mk_All
+ (fn l => foldr (op ===>) (map mk_trp l,
+ mk_trp(%"P")))
+ bound_arg)
+ (fn prems => [
+ cut_facts_tac [excluded_middle] 1,
+ etac disjE 1,
+ rtac (hd prems) 2,
+ etac rep_defin' 2,
+ if length cons = 1 andalso
+ length (snd(hd cons)) = 1 andalso
+ not(is_lazy(hd(snd(hd cons))))
+ then rtac (hd (tl prems)) 1 THEN atac 2 THEN
+ rewrite_goals_tac axs_con_def THEN
+ simp_tac (HOLCF_ss addsimps [ax_rep_iso]) 1
+ else sum_tac cons (tl prems)])end;
val exhaust= pg[](mk_trp(exh (foldr' mk_disj) Id mk_ex (foldr' mk_conj) (K %)))[
- rtac cases 1,
- UNTIL_SOLVED(fast_tac HOL_cs 1)];
+ rtac cases 1,
+ UNTIL_SOLVED(fast_tac HOL_cs 1)];
end;
local
@@ -191,17 +191,17 @@
fun bound_fun i _ = Bound (length cons - i);
val when_app = foldl (op `) (%%(dname^"_when"), mapn bound_fun 1 cons);
val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name ===
- when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
- simp_tac HOLCF_ss 1];
+ when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
+ simp_tac HOLCF_ss 1];
in
val when_strict = pg [] (bind_fun(mk_trp(strict when_app))) [
- simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
+ simp_tac(HOLCF_ss addsimps [when_appl,rep_strict]) 1];
val when_apps = let fun one_when n (con,args) = pg axs_con_def
- (bind_fun (lift_defined % (nonlazy args,
- mk_trp(when_app`(con_app con args) ===
+ (bind_fun (lift_defined % (nonlazy args,
+ mk_trp(when_app`(con_app con args) ===
mk_cfapp(bound_fun n 0,map %# args)))))[
- asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
- in mapn one_when 1 cons end;
+ asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1];
+ in mapn one_when 1 cons end;
end;
val when_rews = when_strict::when_apps;
@@ -209,143 +209,143 @@
val dis_rews = let
val dis_stricts = map (fn (con,_) => pg axs_dis_def (mk_trp(
- strict(%%(dis_name con)))) [
- simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
+ strict(%%(dis_name con)))) [
+ simp_tac (HOLCF_ss addsimps when_rews) 1]) cons;
val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
- (lift_defined % (nonlazy args,
- (mk_trp((%%(dis_name c))`(con_app con args) ===
- %%(if con=c then "TT" else "FF"))))) [
- asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
- in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
+ (lift_defined % (nonlazy args,
+ (mk_trp((%%(dis_name c))`(con_app con args) ===
+ %%(if con=c then "TT" else "FF"))))) [
+ asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
+ in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
val dis_defins = map (fn (con,args) => pg [] (defined(%x_name) ==>
- defined(%%(dis_name con)`%x_name)) [
- rtac cases 1,
- contr_tac 1,
- UNTIL_SOLVED (CHANGED(asm_simp_tac
- (HOLCF_ss addsimps dis_apps) 1))]) cons;
+ defined(%%(dis_name con)`%x_name)) [
+ rtac cases 1,
+ contr_tac 1,
+ UNTIL_SOLVED (CHANGED(asm_simp_tac
+ (HOLCF_ss addsimps dis_apps) 1))]) cons;
in dis_stricts @ dis_defins @ dis_apps end;
val con_stricts = flat(map (fn (con,args) => map (fn vn =>
- pg (axs_con_def)
- (mk_trp(con_app2 con (fn arg => if vname arg = vn
- then UU else %# arg) args === UU))[
- asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
- ) (nonlazy args)) cons);
+ pg (axs_con_def)
+ (mk_trp(con_app2 con (fn arg => if vname arg = vn
+ then UU else %# arg) args === UU))[
+ asm_simp_tac (HOLCF_ss addsimps [abs_strict]) 1]
+ ) (nonlazy args)) cons);
val con_defins = map (fn (con,args) => pg []
- (lift_defined % (nonlazy args,
- mk_trp(defined(con_app con args)))) ([
- rtac swap3 1,
- eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
- asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
+ (lift_defined % (nonlazy args,
+ mk_trp(defined(con_app con args)))) ([
+ rtac swap3 1,
+ eres_inst_tac [("f",dis_name con)] cfun_arg_cong 1,
+ asm_simp_tac (HOLCF_ss addsimps dis_rews) 1] )) cons;
val con_rews = con_stricts @ con_defins;
val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%sel))) [
- simp_tac (HOLCF_ss addsimps when_rews) 1];
+ simp_tac (HOLCF_ss addsimps when_rews) 1];
in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
val sel_apps = let fun one_sel c n sel = map (fn (con,args) =>
- let val nlas = nonlazy args;
- val vns = map vname args;
- in pg axs_sel_def (lift_defined %
- (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
- mk_trp((%%sel)`(con_app con args) ===
- (if con=c then %(nth_elem(n,vns)) else UU))))
- ( (if con=c then []
- else map(case_UU_tac(when_rews@con_stricts)1) nlas)
- @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
- then[case_UU_tac (when_rews @ con_stricts) 1
- (nth_elem(n,vns))] else [])
- @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
+ let val nlas = nonlazy args;
+ val vns = map vname args;
+ in pg axs_sel_def (lift_defined %
+ (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
+ mk_trp((%%sel)`(con_app con args) ===
+ (if con=c then %(nth_elem(n,vns)) else UU))))
+ ( (if con=c then []
+ else map(case_UU_tac(when_rews@con_stricts)1) nlas)
+ @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
+ then[case_UU_tac (when_rews @ con_stricts) 1
+ (nth_elem(n,vns))] else [])
+ @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
in flat(map (fn (c,args) =>
flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%x_name)==>
- defined(%%(sel_of arg)`%x_name)) [
- rtac cases 1,
- contr_tac 1,
- UNTIL_SOLVED (CHANGED(asm_simp_tac
- (HOLCF_ss addsimps sel_apps) 1))])
- (filter_out is_lazy (snd(hd cons))) else [];
+ defined(%%(sel_of arg)`%x_name)) [
+ rtac cases 1,
+ contr_tac 1,
+ UNTIL_SOLVED (CHANGED(asm_simp_tac
+ (HOLCF_ss addsimps sel_apps) 1))])
+ (filter_out is_lazy (snd(hd cons))) else [];
val sel_rews = sel_stricts @ sel_defins @ sel_apps;
val distincts_le = let
fun dist (con1, args1) (con2, args2) = pg []
- (lift_defined % ((nonlazy args1),
- (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
- rtac swap3 1,
- eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
- @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
- @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
+ (lift_defined % ((nonlazy args1),
+ (mk_trp (con_app con1 args1 ~<< con_app con2 args2))))([
+ rtac swap3 1,
+ eres_inst_tac[("fo",dis_name con1)] monofun_cfun_arg 1]
+ @map(case_UU_tac (con_stricts @ dis_rews)1)(nonlazy args2)
+ @[asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]);
fun distinct (con1,args1) (con2,args2) =
- let val arg1 = (con1, args1);
- val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
- (args2~~variantlist(map vname args2,map vname args1))));
- in [dist arg1 arg2, dist arg2 arg1] end;
+ let val arg1 = (con1, args1);
+ val arg2 = (con2, (map (fn (arg,vn) => upd_vname (K vn) arg)
+ (args2~~variantlist(map vname args2,map vname args1))));
+ in [dist arg1 arg2, dist arg2 arg1] end;
fun distincts [] = []
| distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
in distincts cons end;
val dists_le = flat (flat distincts_le);
val dists_eq = let
fun distinct (_,args1) ((_,args2),leqs) = let
- val (le1,le2) = (hd leqs, hd(tl leqs));
- val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
- if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
- if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
- [eq1, eq2] end;
+ val (le1,le2) = (hd leqs, hd(tl leqs));
+ val (eq1,eq2) = (le1 RS dist_eqI, le2 RS dist_eqI) in
+ if nonlazy args1 = [] then [eq1, eq1 RS not_sym] else
+ if nonlazy args2 = [] then [eq2, eq2 RS not_sym] else
+ [eq1, eq2] end;
fun distincts [] = []
| distincts ((c,leqs)::cs) = flat(map (distinct c) ((map fst cs)~~leqs)) @
- distincts cs;
+ distincts cs;
in distincts (cons~~distincts_le) end;
local
fun pgterm rel con args = let
- fun append s = upd_vname(fn v => v^s);
- val (largs,rargs) = (args, map (append "'") args);
- in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
- lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
- mk_trp (foldr' mk_conj
- (map rel (map %# largs ~~ map %# rargs)))))) end;
+ fun append s = upd_vname(fn v => v^s);
+ val (largs,rargs) = (args, map (append "'") args);
+ in pg [] (mk_trp (rel(con_app con largs,con_app con rargs)) ===>
+ lift_defined % ((nonlazy largs),lift_defined % ((nonlazy rargs),
+ mk_trp (foldr' mk_conj
+ (map rel (map %# largs ~~ map %# rargs)))))) end;
val cons' = filter (fn (_,args) => args<>[]) cons;
in
val inverts = map (fn (con,args) =>
- pgterm (op <<) con args (flat(map (fn arg => [
- TRY(rtac conjI 1),
- dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
- asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
- ) args))) cons';
+ pgterm (op <<) con args (flat(map (fn arg => [
+ TRY(rtac conjI 1),
+ dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
+ asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
+ ) args))) cons';
val injects = map (fn ((con,args),inv_thm) =>
- pgterm (op ===) con args [
- etac (antisym_less_inverse RS conjE) 1,
- dtac inv_thm 1, REPEAT(atac 1),
- dtac inv_thm 1, REPEAT(atac 1),
- TRY(safe_tac HOL_cs),
- REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
- (cons'~~inverts);
+ pgterm (op ===) con args [
+ etac (antisym_less_inverse RS conjE) 1,
+ dtac inv_thm 1, REPEAT(atac 1),
+ dtac inv_thm 1, REPEAT(atac 1),
+ TRY(safe_tac HOL_cs),
+ REPEAT(rtac antisym_less 1 ORELSE atac 1)] )
+ (cons'~~inverts);
end;
(* ----- theorems concerning one induction step ----------------------------- *)
val copy_strict = pg[ax_copy_def](mk_trp(strict(dc_copy`%"f"))) [
- asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
- cfst_strict,csnd_strict]) 1];
+ asm_simp_tac(HOLCF_ss addsimps [abs_strict, when_strict,
+ cfst_strict,csnd_strict]) 1];
val copy_apps = map (fn (con,args) => pg [ax_copy_def]
- (lift_defined % (nonlazy_rec args,
- mk_trp(dc_copy`%"f"`(con_app con args) ===
- (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
- (map (case_UU_tac (abs_strict::when_strict::con_stricts)
- 1 o vname)
- (filter (fn a => not (is_rec a orelse is_lazy a)) args)
- @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
- simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
+ (lift_defined % (nonlazy_rec args,
+ mk_trp(dc_copy`%"f"`(con_app con args) ===
+ (con_app2 con (app_rec_arg (cproj (%"f") (length eqs))) args))))
+ (map (case_UU_tac (abs_strict::when_strict::con_stricts)
+ 1 o vname)
+ (filter (fn a => not (is_rec a orelse is_lazy a)) args)
+ @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
+ simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
- (con_app con args) ===UU))
+ (con_app con args) ===UU))
(let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
- in map (case_UU_tac rews 1) (nonlazy args) @ [
- asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
- (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
+ in map (case_UU_tac rews 1) (nonlazy args) @ [
+ asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
+ (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
val copy_rews = copy_strict::copy_apps @ copy_stricts;
in (iso_rews, exhaust, cases, when_rews,
- con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
- copy_rews)
+ con_rews, sel_rews, dis_rews, dists_le, dists_eq, inverts, injects,
+ copy_rews)
end; (* let *)
@@ -377,68 +377,68 @@
local
val iterate_Cprod_ss = simpset_of "Fix"
- addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
+ addsimps [cfst_strict, csnd_strict]addsimps Cprod_rews;
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
- (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
- nat_ind_tac "n" 1,
- simp_tac iterate_Cprod_ss 1,
- asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
+ (dc_take dn $ %"n")`UU === mk_constrain(Type(dn,args),UU)) eqs)))([
+ nat_ind_tac "n" 1,
+ simp_tac iterate_Cprod_ss 1,
+ asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]);
val take_stricts' = rewrite_rule copy_take_defs take_stricts;
val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%"0")
- `%x_name n === UU))[
- simp_tac iterate_Cprod_ss 1]) 1 dnames;
+ `%x_name n === UU))[
+ simp_tac iterate_Cprod_ss 1]) 1 dnames;
val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj
- (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all
- (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
- con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
- args)) cons) eqs)))) ([
- simp_tac iterate_Cprod_ss 1,
- nat_ind_tac "n" 1,
- simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
- asm_full_simp_tac (HOLCF_ss addsimps
- (filter (has_fewer_prems 1) copy_rews)) 1,
- TRY(safe_tac HOL_cs)] @
- (flat(map (fn ((dn,_),cons) => map (fn (con,args) =>
- if nonlazy_rec args = [] then all_tac else
- EVERY(map c_UU_tac (nonlazy_rec args)) THEN
- asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
- ) cons) eqs)));
+ (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all
+ (map vname args,(dc_take dn $ (%%"Suc" $ %"n"))`(con_app con args) ===
+ con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))$ %"n"))
+ args)) cons) eqs)))) ([
+ simp_tac iterate_Cprod_ss 1,
+ nat_ind_tac "n" 1,
+ simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
+ asm_full_simp_tac (HOLCF_ss addsimps
+ (filter (has_fewer_prems 1) copy_rews)) 1,
+ TRY(safe_tac HOL_cs)] @
+ (flat(map (fn ((dn,_),cons) => map (fn (con,args) =>
+ if nonlazy_rec args = [] then all_tac else
+ EVERY(map c_UU_tac (nonlazy_rec args)) THEN
+ asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
+ ) cons) eqs)));
in
val take_rews = atomize take_stricts @ take_0s @ atomize take_apps;
end; (* local *)
local
fun one_con p (con,args) = foldr mk_All (map vname args,
- lift_defined (bound_arg (map vname args)) (nonlazy args,
- lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
+ lift_defined (bound_arg (map vname args)) (nonlazy args,
+ lift (fn arg => %(P_name (1+rec_of arg)) $ bound_arg args arg)
(filter is_rec args,mk_trp(%p $ con_app2 con (bound_arg args) args))));
fun one_eq ((p,cons),concl) = (mk_trp(%p $ UU) ===>
- foldr (op ===>) (map (one_con p) cons,concl));
+ foldr (op ===>) (map (one_con p) cons,concl));
fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
- mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
+ mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
val take_ss = HOL_ss addsimps take_rews;
fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i)
- 1 dnames);
+ 1 dnames);
fun ind_prems_tac prems = EVERY(flat (map (fn cons => (
- resolve_tac prems 1 ::
- flat (map (fn (_,args) =>
- resolve_tac prems 1 ::
- map (K(atac 1)) (nonlazy args) @
- map (K(atac 1)) (filter is_rec args))
- cons))) conss));
+ resolve_tac prems 1 ::
+ flat (map (fn (_,args) =>
+ resolve_tac prems 1 ::
+ map (K(atac 1)) (nonlazy args) @
+ map (K(atac 1)) (filter is_rec args))
+ cons))) conss));
local
(* check whether every/exists constructor of the n-th part of the equation:
it has a possibly indirectly recursive argument that isn't/is possibly
indirectly lazy *)
fun rec_to quant nfn rfn ns lazy_rec (n,cons) = quant (exists (fn arg =>
- is_rec arg andalso not(rec_of arg mem ns) andalso
- ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
- rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
- (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
- ) o snd) cons;
+ is_rec arg andalso not(rec_of arg mem ns) andalso
+ ((rec_of arg = n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
+ rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
+ (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
+ ) o snd) cons;
fun all_rec_to ns = rec_to forall not all_rec_to ns;
fun warn (n,cons) = if all_rec_to [] false (n,cons) then (writeln
("WARNING: domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
@@ -450,42 +450,42 @@
end;
in (* local *)
val finite_ind = pg'' thy [] (ind_term (fn n => fn dn => %(P_name n)$
- (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
- quant_tac 1,
- simp_tac quant_ss 1,
- nat_ind_tac "n" 1,
- simp_tac (take_ss addsimps prems) 1,
- TRY(safe_tac HOL_cs)]
- @ flat(map (fn (cons,cases) => [
- res_inst_tac [("x","x")] cases 1,
- asm_simp_tac (take_ss addsimps prems) 1]
- @ flat(map (fn (con,args) =>
- asm_simp_tac take_ss 1 ::
- map (fn arg =>
- case_UU_tac (prems@con_rews) 1 (
- nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
- (filter is_nonlazy_rec args) @ [
- resolve_tac prems 1] @
- map (K (atac 1)) (nonlazy args) @
- map (K (etac spec 1)) (filter is_rec args))
- cons))
- (conss~~casess)));
+ (dc_take dn $ %"n" `%(x_name n)))) (fn prems => [
+ quant_tac 1,
+ simp_tac quant_ss 1,
+ nat_ind_tac "n" 1,
+ simp_tac (take_ss addsimps prems) 1,
+ TRY(safe_tac HOL_cs)]
+ @ flat(map (fn (cons,cases) => [
+ res_inst_tac [("x","x")] cases 1,
+ asm_simp_tac (take_ss addsimps prems) 1]
+ @ flat(map (fn (con,args) =>
+ asm_simp_tac take_ss 1 ::
+ map (fn arg =>
+ case_UU_tac (prems@con_rews) 1 (
+ nth_elem(rec_of arg,dnames)^"_take n1`"^vname arg))
+ (filter is_nonlazy_rec args) @ [
+ resolve_tac prems 1] @
+ map (K (atac 1)) (nonlazy args) @
+ map (K (etac spec 1)) (filter is_rec args))
+ cons))
+ (conss~~casess)));
val take_lemmas =mapn(fn n=> fn(dn,ax_reach)=> pg'' thy axs_take_def(mk_All("n",
- mk_trp(dc_take dn $ Bound 0 `%(x_name n) ===
- dc_take dn $ Bound 0 `%(x_name n^"'")))
- ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
- res_inst_tac[("t",x_name n )](ax_reach RS subst) 1,
- res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
- rtac (fix_def2 RS ssubst) 1,
- REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1
- THEN chain_tac 1)),
- rtac (contlub_cfun_fun RS ssubst) 1,
- rtac (contlub_cfun_fun RS ssubst) 2,
- rtac lub_equal 3,
- chain_tac 1,
- rtac allI 1,
- resolve_tac prems 1])) 1 (dnames~~axs_reach);
+ mk_trp(dc_take dn $ Bound 0 `%(x_name n) ===
+ dc_take dn $ Bound 0 `%(x_name n^"'")))
+ ===> mk_trp(%(x_name n) === %(x_name n^"'"))) (fn prems => [
+ res_inst_tac[("t",x_name n )](ax_reach RS subst) 1,
+ res_inst_tac[("t",x_name n^"'")](ax_reach RS subst) 1,
+ stac fix_def2 1,
+ REPEAT(CHANGED(rtac(contlub_cfun_arg RS ssubst)1
+ THEN chain_tac 1)),
+ stac contlub_cfun_fun 1,
+ stac contlub_cfun_fun 2,
+ rtac lub_equal 3,
+ chain_tac 1,
+ rtac allI 1,
+ resolve_tac prems 1])) 1 (dnames~~axs_reach);
(* ----- theorems concerning finiteness and induction ----------------------- *)
@@ -493,70 +493,70 @@
let
fun take_enough dn = mk_ex ("n",dc_take dn $ Bound 0 ` %"x" === %"x");
val finite_lemmas1a = map (fn dn => pg [] (mk_trp(defined (%"x")) ===>
- mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
- take_enough dn)) ===> mk_trp(take_enough dn)) [
- etac disjE 1,
- etac notE 1,
- resolve_tac take_lemmas 1,
- asm_simp_tac take_ss 1,
- atac 1]) dnames;
+ mk_trp(mk_disj(mk_all("n",dc_take dn $ Bound 0 ` %"x" === UU),
+ take_enough dn)) ===> mk_trp(take_enough dn)) [
+ etac disjE 1,
+ etac notE 1,
+ resolve_tac take_lemmas 1,
+ asm_simp_tac take_ss 1,
+ atac 1]) dnames;
val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn
- (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
- mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
- dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
- rtac allI 1,
- nat_ind_tac "n" 1,
- simp_tac take_ss 1,
- TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
- flat(mapn (fn n => fn (cons,cases) => [
- simp_tac take_ss 1,
- rtac allI 1,
- res_inst_tac [("x",x_name n)] cases 1,
- asm_simp_tac take_ss 1] @
- flat(map (fn (con,args) =>
- asm_simp_tac take_ss 1 ::
- flat(map (fn vn => [
- eres_inst_tac [("x",vn)] all_dupE 1,
- etac disjE 1,
- asm_simp_tac (HOL_ss addsimps con_rews) 1,
- asm_simp_tac take_ss 1])
- (nonlazy_rec args)))
- cons))
- 1 (conss~~casess))) handle ERROR => raise ERROR;
+ (fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
+ mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
+ dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
+ rtac allI 1,
+ nat_ind_tac "n" 1,
+ simp_tac take_ss 1,
+ TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
+ flat(mapn (fn n => fn (cons,cases) => [
+ simp_tac take_ss 1,
+ rtac allI 1,
+ res_inst_tac [("x",x_name n)] cases 1,
+ asm_simp_tac take_ss 1] @
+ flat(map (fn (con,args) =>
+ asm_simp_tac take_ss 1 ::
+ flat(map (fn vn => [
+ eres_inst_tac [("x",vn)] all_dupE 1,
+ etac disjE 1,
+ asm_simp_tac (HOL_ss addsimps con_rews) 1,
+ asm_simp_tac take_ss 1])
+ (nonlazy_rec args)))
+ cons))
+ 1 (conss~~casess))) handle ERROR => raise ERROR;
val finites = map (fn (dn,l1b) => pg axs_finite_def (mk_trp(
- %%(dn^"_finite") $ %"x"))[
- case_UU_tac take_rews 1 "x",
- eresolve_tac finite_lemmas1a 1,
- step_tac HOL_cs 1,
- step_tac HOL_cs 1,
- cut_facts_tac [l1b] 1,
- fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
+ %%(dn^"_finite") $ %"x"))[
+ case_UU_tac take_rews 1 "x",
+ eresolve_tac finite_lemmas1a 1,
+ step_tac HOL_cs 1,
+ step_tac HOL_cs 1,
+ cut_facts_tac [l1b] 1,
+ fast_tac HOL_cs 1]) (dnames~~atomize finite_lemma1b);
in
(finites,
pg'' thy[](ind_term (fn n => fn dn => %(P_name n) $ %(x_name n)))(fn prems =>
- TRY(safe_tac HOL_cs) ::
- flat (map (fn (finite,fin_ind) => [
- rtac(rewrite_rule axs_finite_def finite RS exE)1,
- etac subst 1,
- rtac fin_ind 1,
- ind_prems_tac prems])
- (finites~~(atomize finite_ind)) ))
+ TRY(safe_tac HOL_cs) ::
+ flat (map (fn (finite,fin_ind) => [
+ rtac(rewrite_rule axs_finite_def finite RS exE)1,
+ etac subst 1,
+ rtac fin_ind 1,
+ ind_prems_tac prems])
+ (finites~~(atomize finite_ind)) ))
) end (* let *) else
(mapn (fn n => fn dn => read_instantiate_sg (sign_of thy)
- [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
+ [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%"adm" $ %(P_name n))))
- 1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
- (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1)
- axs_reach @ [
- quant_tac 1,
- rtac (adm_impl_admw RS wfix_ind) 1,
- REPEAT_DETERM(rtac adm_all2 1),
- REPEAT_DETERM(TRY(rtac adm_conj 1) THEN
- rtac adm_subst 1 THEN
- cont_tacR 1 THEN resolve_tac prems 1),
- strip_tac 1,
- rtac (rewrite_rule axs_take_def finite_ind) 1,
- ind_prems_tac prems])
+ 1 dnames, ind_term (fn n => fn dn => %(P_name n) $ %(x_name n))))
+ (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1)
+ axs_reach @ [
+ quant_tac 1,
+ rtac (adm_impl_admw RS wfix_ind) 1,
+ REPEAT_DETERM(rtac adm_all2 1),
+ REPEAT_DETERM(TRY(rtac adm_conj 1) THEN
+ rtac adm_subst 1 THEN
+ cont_tacR 1 THEN resolve_tac prems 1),
+ strip_tac 1,
+ rtac (rewrite_rule axs_take_def finite_ind) 1,
+ ind_prems_tac prems])
)
end; (* local *)
@@ -568,35 +568,35 @@
val take_ss = HOL_ss addsimps take_rews;
val sproj = prj (fn s => "fst("^s^")") (fn s => "snd("^s^")");
val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%(comp_dname^"_bisim") $ %"R",
- foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
- foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $
- bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
- foldr' mk_conj (mapn (fn n => fn dn =>
- (dc_take dn $ %"n" `bnd_arg n 0 ===
- (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
- ([ rtac impI 1,
- nat_ind_tac "n" 1,
- simp_tac take_ss 1,
- safe_tac HOL_cs] @
- flat(mapn (fn n => fn x => [
- rotate_tac (n+1) 1,
- etac all2E 1,
- eres_inst_tac [("P1", sproj "R" n_eqs n^
- " "^x^" "^x^"'")](mp RS disjE) 1,
- TRY(safe_tac HOL_cs),
- REPEAT(CHANGED(asm_simp_tac take_ss 1))])
- 0 xs));
+ foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
+ foldr mk_imp (mapn (fn n => K(proj (%"R") n_eqs n $
+ bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
+ foldr' mk_conj (mapn (fn n => fn dn =>
+ (dc_take dn $ %"n" `bnd_arg n 0 ===
+ (dc_take dn $ %"n" `bnd_arg n 1)))0 dnames))))))
+ ([ rtac impI 1,
+ nat_ind_tac "n" 1,
+ simp_tac take_ss 1,
+ safe_tac HOL_cs] @
+ flat(mapn (fn n => fn x => [
+ rotate_tac (n+1) 1,
+ etac all2E 1,
+ eres_inst_tac [("P1", sproj "R" n_eqs n^
+ " "^x^" "^x^"'")](mp RS disjE) 1,
+ TRY(safe_tac HOL_cs),
+ REPEAT(CHANGED(asm_simp_tac take_ss 1))])
+ 0 xs));
in
val coind = pg [] (mk_trp(%%(comp_dname^"_bisim") $ %"R") ===>
- foldr (op ===>) (mapn (fn n => fn x =>
- mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
- mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
- TRY(safe_tac HOL_cs)] @
- flat(map (fn take_lemma => [
- rtac take_lemma 1,
- cut_facts_tac [coind_lemma] 1,
- fast_tac HOL_cs 1])
- take_lemmas));
+ foldr (op ===>) (mapn (fn n => fn x =>
+ mk_trp(proj (%"R") n_eqs n $ %x $ %(x^"'"))) 0 xs,
+ mk_trp(foldr' mk_conj (map (fn x => %x === %(x^"'")) xs)))) ([
+ TRY(safe_tac HOL_cs)] @
+ flat(map (fn take_lemma => [
+ rtac take_lemma 1,
+ cut_facts_tac [coind_lemma] 1,
+ fast_tac HOL_cs 1])
+ take_lemmas));
end; (* local *)
--- a/src/HOLCF/ex/Hoare.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/ex/Hoare.ML Thu Sep 26 15:14:23 1996 +0200
@@ -179,7 +179,7 @@
(simp_tac HOLCF_ss 1),
(etac mp 1),
(strip_tac 1),
- (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
+ (fast_tac (HOL_cs addSDs [less_Suc_eq RS iffD1]) 1)]);
(* -------- results about p for case (? k. b1`(iterate k g x)~=TT) ------- *)
@@ -275,14 +275,14 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (p_def2 RS ssubst) 1),
+ (stac p_def2 1),
(rtac fix_ind 1),
(rtac adm_all 1),
(rtac allI 1),
(rtac adm_eq 1),
(cont_tacR 1),
(rtac allI 1),
- (rtac (strict_fapp1 RS ssubst) 1),
+ (stac strict_fapp1 1),
(rtac refl 1),
(Simp_tac 1),
(rtac allI 1),
@@ -309,14 +309,14 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (q_def2 RS ssubst) 1),
+ (stac q_def2 1),
(rtac fix_ind 1),
(rtac adm_all 1),
(rtac allI 1),
(rtac adm_eq 1),
(cont_tacR 1),
(rtac allI 1),
- (rtac (strict_fapp1 RS ssubst) 1),
+ (stac strict_fapp1 1),
(rtac refl 1),
(rtac allI 1),
(Simp_tac 1),
@@ -351,14 +351,14 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (q_def2 RS ssubst) 1),
+ (stac q_def2 1),
(rtac fix_ind 1),
(rtac adm_all 1),
(rtac allI 1),
(rtac adm_eq 1),
(cont_tacR 1),
(rtac allI 1),
- (rtac (strict_fapp1 RS ssubst) 1),
+ (stac strict_fapp1 1),
(rtac refl 1),
(rtac allI 1),
(Simp_tac 1),
@@ -383,7 +383,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (q_def3 RS ssubst) 1),
+ (stac q_def3 1),
(asm_simp_tac HOLCF_ss 1)
]);
@@ -437,7 +437,7 @@
(Simp_tac 1),
(strip_tac 1),
(etac conjE 1),
- (rtac (q_def3 RS ssubst) 1),
+ (stac q_def3 1),
(asm_simp_tac HOLCF_ss 1),
(hyp_subst_tac 1),
(Simp_tac 1),
@@ -467,18 +467,18 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (hoare_lemma16 RS ssubst) 1),
+ (stac hoare_lemma16 1),
(atac 1),
(rtac (hoare_lemma19 RS disjE) 1),
(atac 1),
- (rtac (hoare_lemma18 RS ssubst) 1),
+ (stac hoare_lemma18 1),
(atac 1),
- (rtac (hoare_lemma22 RS ssubst) 1),
+ (stac hoare_lemma22 1),
(atac 1),
(rtac refl 1),
- (rtac (hoare_lemma21 RS ssubst) 1),
+ (stac hoare_lemma21 1),
(atac 1),
- (rtac (hoare_lemma21 RS ssubst) 1),
+ (stac hoare_lemma21 1),
(atac 1),
(rtac refl 1)
]);
@@ -493,7 +493,7 @@
(rtac (hoare_lemma5 RS disjE) 1),
(atac 1),
(rtac refl 1),
- (rtac (hoare_lemma11 RS mp RS ssubst) 1),
+ (stac (hoare_lemma11 RS mp) 1),
(atac 1),
(rtac conjI 1),
(rtac refl 1),
@@ -504,17 +504,17 @@
(rtac refl 1),
(atac 1),
(rtac refl 1),
- (rtac (hoare_lemma12 RS mp RS ssubst) 1),
+ (stac (hoare_lemma12 RS mp) 1),
(atac 1),
(rtac conjI 1),
(rtac refl 1),
(atac 1),
- (rtac (hoare_lemma22 RS ssubst) 1),
- (rtac (hoare_lemma28 RS ssubst) 1),
+ (stac hoare_lemma22 1),
+ (stac hoare_lemma28 1),
(atac 1),
(rtac refl 1),
(rtac sym 1),
- (rtac (hoare_lemma27 RS mp RS ssubst) 1),
+ (stac (hoare_lemma27 RS mp) 1),
(atac 1),
(rtac conjI 1),
(rtac refl 1),
@@ -528,7 +528,7 @@
(fn prems =>
[
(rtac ext_cfun 1),
- (rtac (cfcomp2 RS ssubst) 1),
+ (stac cfcomp2 1),
(rtac (hoare_lemma3 RS disjE) 1),
(etac hoare_lemma23 1),
(etac hoare_lemma29 1)
--- a/src/HOLCF/ex/Loop.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/ex/Loop.ML Thu Sep 26 15:14:23 1996 +0200
@@ -47,15 +47,15 @@
(simp_tac HOLCF_ss 1),
(rtac allI 1),
(rtac trans 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(rtac refl 2),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(rtac trans 1),
(etac spec 2),
- (rtac (step_def2 RS ssubst) 1),
+ (stac step_def2 1),
(res_inst_tac [("p","b`x")] trE 1),
(asm_simp_tac HOLCF_ss 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(res_inst_tac [("s","UU"),("t","b`UU")]ssubst 1),
(etac (flat_tr RS flat_codom RS disjE) 1),
(atac 1),
@@ -63,7 +63,7 @@
(simp_tac HOLCF_ss 1),
(asm_simp_tac HOLCF_ss 1),
(asm_simp_tac HOLCF_ss 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(asm_simp_tac HOLCF_ss 1)
]);
@@ -144,10 +144,10 @@
(nat_ind_tac "k" 1),
(Simp_tac 1),
(strip_tac 1),
- (rtac (while_unfold RS ssubst) 1),
+ (stac while_unfold 1),
(asm_simp_tac HOLCF_ss 1),
(rtac allI 1),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(strip_tac 1),
(rtac trans 1),
(rtac while_unfold3 1),
@@ -160,7 +160,7 @@
(fn prems =>
[
(cut_facts_tac prems 1),
- (rtac (while_def2 RS ssubst) 1),
+ (stac while_def2 1),
(rtac fix_ind 1),
(rtac (allI RS adm_all) 1),
(rtac adm_eq 1),
@@ -224,7 +224,7 @@
(res_inst_tac [("P","%k. b`(iterate k (step`b`g) x)=FF")] exE 1),
(rtac loop_lemma7 1),
(resolve_tac prems 1),
- (rtac ((loop_lemma4 RS spec RS mp) RS ssubst) 1),
+ (stac (loop_lemma4 RS spec RS mp) 1),
(atac 1),
(rtac (nth_elem (1,prems) RS spec RS mp) 1),
(rtac conjI 1),
--- a/src/HOLCF/ex/loeckx.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/ex/loeckx.ML Thu Sep 26 15:14:23 1996 +0200
@@ -4,7 +4,7 @@
val prems = goalw Fix.thy [Ifix_def]
"Ifix F= lub (range (%i.%G.iterate i G UU)) F";
-by (rtac (thelub_fun RS ssubst) 1);
+by (stac thelub_fun 1);
by (rtac ch2ch_fun 1);
back();
by (rtac refl 2);
@@ -59,7 +59,7 @@
"(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)" 1);
by (etac arg_cong 1);
by (rtac ext 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac refl 1);
@@ -67,10 +67,10 @@
by (rtac is_chainI 1);
by (strip_tac 1);
by (rtac less_cfun2 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
@@ -81,7 +81,7 @@
val prems = goal Fix.thy
"(% i.iterate i f UU) = (%j.(LAM f. iterate j f UU)`f)";
by (rtac ext 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac refl 1);
@@ -91,7 +91,7 @@
" Ifix = (%f.lub(range(%j.(LAM f.iterate j f UU)`f)))";
by (rtac ext 1);
by (rewtac Ifix_def );
-by (rtac (fix_lemma1 RS ssubst) 1);
+by (stac fix_lemma1 1);
by (rtac refl 1);
val fix_lemma2 = result();
@@ -102,15 +102,15 @@
*)
val prems = goal Fix.thy "cont Ifix";
-by (rtac ( fix_lemma2 RS ssubst) 1);
+by (stac fix_lemma2 1);
by (rtac cont_lubcfun 1);
by (rtac is_chainI 1);
by (strip_tac 1);
by (rtac less_cfun2 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (rtac cont2cont_CF1L 1);
by (rtac cont_iterate 1);
by (rtac (is_chain_iterate RS is_chainE RS spec) 1);
--- a/src/HOLCF/explicit_domains/Coind.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Coind.ML Thu Sep 26 15:14:23 1996 +0200
@@ -28,7 +28,7 @@
(fn prems =>
[
(rtac trans 1),
- (rtac (from_def2 RS ssubst) 1),
+ (stac from_def2 1),
(Simp_tac 1),
(rtac refl 1)
]);
@@ -38,7 +38,7 @@
(fn prems =>
[
(rtac trans 1),
- (rtac (from RS ssubst) 1),
+ (stac from 1),
(resolve_tac stream_constrdef 1),
(rtac refl 1)
]);
@@ -119,17 +119,17 @@
(etac conjE 1),
(hyp_subst_tac 1),
(rtac conjI 1),
- (rtac (coind_lemma1 RS ssubst) 1),
- (rtac (from RS ssubst) 1),
+ (stac coind_lemma1 1),
+ (stac from 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),
+ (stac coind_lemma1 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac refl 1),
(rtac trans 1),
- (rtac (from RS ssubst) 1),
+ (stac from 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac refl 1),
(res_inst_tac [("x","dzero")] exI 1),
--- a/src/HOLCF/explicit_domains/Dagstuhl.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dagstuhl.ML Thu Sep 26 15:14:23 1996 +0200
@@ -12,7 +12,7 @@
by (resolve_tac adm_thms 1);
by (cont_tacR 1);
by (rtac minimal 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (cont_tacR 1);
by (rtac monofun_cfun_arg 1);
by (rtac monofun_cfun_arg 1);
@@ -20,7 +20,7 @@
val lemma3 = result();
val prems = goal Dagstuhl.thy "scons`y`YYS << YYS";
-by (rtac (YYS_def2 RS ssubst) 1);
+by (stac YYS_def2 1);
back();
by (rtac monofun_cfun_arg 1);
by (rtac lemma3 1);
@@ -38,8 +38,8 @@
by (rtac stream_take_lemma 1);
by (nat_ind_tac "n" 1);
by (simp_tac (!simpset addsimps stream_rews) 1);
-by (rtac (YS_def2 RS ssubst) 1);
-by (rtac (YYS_def2 RS ssubst) 1);
+by (stac YS_def2 1);
+by (stac YYS_def2 1);
by (asm_simp_tac (!simpset addsimps stream_rews) 1);
by (rtac (lemma5 RS sym RS subst) 1);
by (rtac refl 1);
@@ -54,7 +54,7 @@
val prems = goal Dagstuhl.thy "YYS << YS";
by (rewtac YYS_def);
by (rtac fix_least 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (cont_tacR 1);
by (simp_tac (!simpset addsimps [YS_def2 RS sym]) 1);
val lemma6=result();
@@ -65,9 +65,9 @@
by (resolve_tac adm_thms 1);
by (cont_tacR 1);
by (rtac minimal 1);
-by (rtac (beta_cfun RS ssubst) 1);
+by (stac beta_cfun 1);
by (cont_tacR 1);
-by (rtac (lemma5 RS sym RS ssubst) 1);
+by (stac (lemma5 RS sym) 1);
by (etac monofun_cfun_arg 1);
val lemma7 = result();
--- a/src/HOLCF/explicit_domains/Dlist.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dlist.ML Thu Sep 26 15:14:23 1996 +0200
@@ -427,10 +427,10 @@
[
(res_inst_tac [("t","l1")] (reach RS subst) 1),
(res_inst_tac [("t","l2")] (reach RS subst) 1),
- (rtac (fix_def2 RS ssubst) 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac fix_def2 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
(rtac lub_equal 1),
(rtac (is_chain_iterate RS ch2ch_fappL) 1),
--- a/src/HOLCF/explicit_domains/Dnat.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dnat.ML Thu Sep 26 15:14:23 1996 +0200
@@ -339,10 +339,10 @@
[
(res_inst_tac [("t","s1")] (reach RS subst) 1),
(res_inst_tac [("t","s2")] (reach RS subst) 1),
- (rtac (fix_def2 RS ssubst) 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac fix_def2 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
(rtac lub_equal 1),
(rtac (is_chain_iterate RS ch2ch_fappL) 1),
--- a/src/HOLCF/explicit_domains/Dnat2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dnat2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -23,14 +23,14 @@
qed_goal "iterator1" Dnat2.thy "iterator`UU`f`x = UU"
(fn prems =>
[
- (rtac (iterator_def2 RS ssubst) 1),
+ (stac iterator_def2 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),
+ (stac iterator_def2 1),
(simp_tac (!simpset addsimps dnat_when) 1)
]);
@@ -40,7 +40,7 @@
[
(cut_facts_tac prems 1),
(rtac trans 1),
- (rtac (iterator_def2 RS ssubst) 1),
+ (stac iterator_def2 1),
(asm_simp_tac (!simpset addsimps dnat_rews) 1),
(rtac refl 1)
]);
--- a/src/HOLCF/explicit_domains/Stream.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Stream.ML Thu Sep 26 15:14:23 1996 +0200
@@ -311,20 +311,20 @@
fun prover reach defs thm = prove_goalw Stream.thy defs thm
(fn prems =>
- [
- (res_inst_tac [("t","s1")] (reach RS subst) 1),
- (res_inst_tac [("t","s2")] (reach RS subst) 1),
- (rtac (fix_def2 RS ssubst) 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
- (rtac is_chain_iterate 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
- (rtac is_chain_iterate 1),
- (rtac lub_equal 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac (is_chain_iterate RS ch2ch_fappL) 1),
- (rtac allI 1),
- (resolve_tac prems 1),
- ]);
+ [
+ (res_inst_tac [("t","s1")] (reach RS subst) 1),
+ (res_inst_tac [("t","s2")] (reach RS subst) 1),
+ (stac fix_def2 1),
+ (stac contlub_cfun_fun 1),
+ (rtac is_chain_iterate 1),
+ (stac contlub_cfun_fun 1),
+ (rtac is_chain_iterate 1),
+ (rtac lub_equal 1),
+ (rtac (is_chain_iterate RS ch2ch_fappL) 1),
+ (rtac (is_chain_iterate RS ch2ch_fappL) 1),
+ (rtac allI 1),
+ (resolve_tac prems 1),
+ ]);
val stream_take_lemma = prover stream_reach [stream_take_def]
"(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";
@@ -334,9 +334,9 @@
(fn prems =>
[
(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
- (rtac (fix_def2 RS ssubst) 1),
+ (stac fix_def2 1),
(rewtac stream_take_def),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
(rtac refl 1)
]);
@@ -640,9 +640,9 @@
(strip_tac 1),
(res_inst_tac [("s","s")] streamE 1),
(hyp_subst_tac 1),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(etac allE 1),
(etac mp 1),
@@ -664,7 +664,7 @@
(hyp_subst_tac 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(hyp_subst_tac 1),
- (rtac (iterate_Suc2 RS ssubst) 1),
+ (stac iterate_Suc2 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1)
]);
@@ -833,7 +833,7 @@
(REPEAT(resolve_tac adm_thms 1)),
(rtac cont_iterate2 1),
(rtac allI 1),
- (rtac (stream_finite_lemma8 RS ssubst) 1),
+ (stac stream_finite_lemma8 1),
(fast_tac HOL_cs 1)
]);
--- a/src/HOLCF/explicit_domains/Stream2.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Stream2.ML Thu Sep 26 15:14:23 1996 +0200
@@ -24,7 +24,7 @@
qed_goal "smap1" Stream2.thy "smap`f`UU = UU"
(fn prems =>
[
- (rtac (smap_def2 RS ssubst) 1),
+ (stac smap_def2 1),
(simp_tac (!simpset addsimps stream_when) 1)
]);
@@ -34,7 +34,7 @@
[
(cut_facts_tac prems 1),
(rtac trans 1),
- (rtac (smap_def2 RS ssubst) 1),
+ (stac smap_def2 1),
(asm_simp_tac (!simpset addsimps stream_rews) 1),
(rtac refl 1)
]);
--- a/src/ZF/Arith.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Arith.ML Thu Sep 26 15:14:23 1996 +0200
@@ -450,7 +450,7 @@
qed "add_le_self";
goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le n #+ m";
-by (rtac (add_commute RS ssubst) 1);
+by (stac add_commute 1);
by (REPEAT (ares_tac [add_le_self] 1));
qed "add_le_self2";
@@ -468,8 +468,8 @@
goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
by (rtac (add_lt_mono1 RS lt_trans) 1);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
-by (EVERY [rtac (add_commute RS ssubst) 1,
- rtac (add_commute RS ssubst) 3,
+by (EVERY [stac add_commute 1,
+ stac add_commute 3,
rtac add_lt_mono1 5]);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
qed "add_lt_mono";
@@ -496,8 +496,8 @@
"!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
by (rtac (add_le_mono1 RS le_trans) 1);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
-by (EVERY [rtac (add_commute RS ssubst) 1,
- rtac (add_commute RS ssubst) 3,
+by (EVERY [stac add_commute 1,
+ stac add_commute 3,
rtac add_le_mono1 5]);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
qed "add_le_mono";
@@ -516,8 +516,8 @@
"!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
by (rtac (mult_le_mono1 RS le_trans) 1);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
-by (EVERY [rtac (mult_commute RS ssubst) 1,
- rtac (mult_commute RS ssubst) 3,
+by (EVERY [stac mult_commute 1,
+ stac mult_commute 3,
rtac mult_le_mono1 5]);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
qed "mult_le_mono";
--- a/src/ZF/Cardinal.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Cardinal.ML Thu Sep 26 15:14:23 1996 +0200
@@ -200,7 +200,7 @@
by (trans_ind_tac "i" [] 1);
by (rtac impI 1);
by (rtac classical 1);
-by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
+by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
by (assume_tac 2);
by (fast_tac (ZF_cs addSEs [ltE]) 1);
qed "LeastI";
@@ -211,7 +211,7 @@
by (trans_ind_tac "i" [] 1);
by (rtac impI 1);
by (rtac classical 1);
-by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]);
+by (EVERY1 [stac Least_equality, assume_tac, assume_tac]);
by (etac le_refl 2);
by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1);
qed "Least_le";
@@ -299,7 +299,7 @@
(* Could replace the ~(j eqpoll i) by ~(i lepoll j) *)
val prems = goalw Cardinal.thy [Card_def,cardinal_def]
"[| Ord(i); !!j. j<i ==> ~(j eqpoll i) |] ==> Card(i)";
-by (rtac (Least_equality RS ssubst) 1);
+by (stac Least_equality 1);
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1));
qed "CardI";
@@ -481,7 +481,7 @@
(*The object of all this work: every natural number is a (finite) cardinal*)
goalw Cardinal.thy [Card_def,cardinal_def]
"!!n. n: nat ==> Card(n)";
-by (rtac (Least_equality RS ssubst) 1);
+by (stac Least_equality 1);
by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl]));
by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1);
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1);
@@ -549,7 +549,7 @@
qed "Ord_nat_eqpoll_iff";
goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)";
-by (rtac (Least_equality RS ssubst) 1);
+by (stac Least_equality 1);
by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl]));
by (etac ltE 1);
by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1);
--- a/src/ZF/Cardinal_AC.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Cardinal_AC.ML Thu Sep 26 15:14:23 1996 +0200
@@ -34,7 +34,7 @@
"!!A. [| |A|=|B|; |C|=|D|; A Int C = 0; B Int D = 0 |] ==> \
\ |A Un C| = |B Un D|";
by (asm_full_simp_tac (ZF_ss addsimps [cardinal_eqpoll_iff,
- eqpoll_disjoint_Un]) 1);
+ eqpoll_disjoint_Un]) 1);
qed "cardinal_disjoint_Un";
goal Cardinal_AC.thy "!!A B. A lepoll B ==> |A| le |B|";
--- a/src/ZF/Epsilon.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Epsilon.ML Thu Sep 26 15:14:23 1996 +0200
@@ -154,7 +154,7 @@
"[| !!x u. [| x:eclose({a}); u: Pi(x,B) |] ==> H(x,u) : B(x) \
\ |] ==> transrec(a,H) : B(a)";
by (res_inst_tac [("i", "a")] (arg_in_eclose_sing RS eclose_induct) 1);
-by (rtac (transrec RS ssubst) 1);
+by (stac transrec 1);
by (REPEAT (ares_tac (prems @ [lam_type]) 1 ORELSE etac bspec 1));
qed "transrec_type";
@@ -177,13 +177,13 @@
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
goal Epsilon.thy "rank(a) = (UN y:a. succ(rank(y)))";
-by (rtac (rank_def RS def_transrec RS ssubst) 1);
+by (stac (rank_def RS def_transrec) 1);
by (simp_tac ZF_ss 1);
qed "rank";
goal Epsilon.thy "Ord(rank(a))";
by (eps_ind_tac "a" 1);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
by (rtac (Ord_succ RS Ord_UN) 1);
by (etac bspec 1);
by (assume_tac 1);
@@ -191,7 +191,7 @@
val [major] = goal Epsilon.thy "Ord(i) ==> rank(i) = i";
by (rtac (major RS trans_induct) 1);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
by (asm_simp_tac (ZF_ss addsimps [Ord_equality]) 1);
qed "rank_of_Ord";
@@ -211,8 +211,8 @@
goal Epsilon.thy "!!a b. a<=b ==> rank(a) le rank(b)";
by (rtac subset_imp_le 1);
-by (rtac (rank RS ssubst) 1);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
+by (stac rank 1);
by (etac UN_mono 1);
by (REPEAT (resolve_tac [subset_refl, Ord_rank] 1));
qed "rank_mono";
@@ -243,7 +243,7 @@
by (rtac equalityI 1);
by (rtac (rank_mono RS le_imp_subset RS UN_least) 2);
by (etac Union_upper 2);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
by (rtac UN_least 1);
by (etac UnionE 1);
by (rtac subset_trans 1);
--- a/src/ZF/Finite.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Finite.ML Thu Sep 26 15:14:23 1996 +0200
@@ -73,7 +73,7 @@
\ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \
\ |] ==> c<=b --> P(b-c)";
by (rtac (major RS Fin_induct) 1);
-by (rtac (Diff_cons RS ssubst) 2);
+by (stac Diff_cons 2);
by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff,
Diff_subset RS Fin_subset]))));
qed "Fin_0_induct_lemma";
--- a/src/ZF/List.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/List.ML Thu Sep 26 15:14:23 1996 +0200
@@ -110,8 +110,8 @@
"!!i. i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
by (etac nat_induct 1);
by (simp_tac (nat_ss addsimps [tl_Cons]) 1);
-by (rtac (rec_succ RS ssubst) 1);
-by (rtac (rec_succ RS ssubst) 1);
+by (stac rec_succ 1);
+by (stac rec_succ 1);
by (asm_simp_tac ZF_ss 1);
qed "drop_succ_Cons";
@@ -219,7 +219,7 @@
goalw List.thy [set_of_list_def]
"!!l. l: list(A) ==> set_of_list(l) : Pow(A)";
-be list_rec_type 1;
+by (etac list_rec_type 1);
by (ALLGOALS (fast_tac ZF_cs));
qed "set_of_list_type";
@@ -228,7 +228,7 @@
\ set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)";
by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac (ZF_ss addsimps [set_of_list_Nil,set_of_list_Cons,
- app_Nil,app_Cons,Un_cons])));
+ app_Nil,app_Cons,Un_cons])));
qed "set_of_list_append";
--- a/src/ZF/Nat.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Nat.ML Thu Sep 26 15:14:23 1996 +0200
@@ -21,12 +21,12 @@
(** Type checking of 0 and successor **)
goal Nat.thy "0 : nat";
-by (rtac (nat_unfold RS ssubst) 1);
+by (stac nat_unfold 1);
by (rtac (singletonI RS UnI1) 1);
qed "nat_0I";
val prems = goal Nat.thy "n : nat ==> succ(n) : nat";
-by (rtac (nat_unfold RS ssubst) 1);
+by (stac nat_unfold 1);
by (rtac (RepFunI RS UnI2) 1);
by (resolve_tac prems 1);
qed "nat_succI";
--- a/src/ZF/OrderType.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/OrderType.ML Thu Sep 26 15:14:23 1996 +0200
@@ -116,7 +116,7 @@
goalw OrderType.thy [ordertype_def]
"!!r. well_ord(A,r) ==> Ord(ordertype(A,r))";
-by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
+by (stac ([ordermap_type, subset_refl] MRS image_fun) 1);
by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
by (rewrite_goals_tac [Transset_def,well_ord_def]);
--- a/src/ZF/Ordinal.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Ordinal.ML Thu Sep 26 15:14:23 1996 +0200
@@ -532,7 +532,7 @@
(*Replacing k by succ(k') yields the similar rule for le!*)
goal Ordinal.thy "!!i j k. [| i<k; j<k |] ==> i Un j < k";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
-by (rtac (Un_commute RS ssubst) 4);
+by (stac Un_commute 4);
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 3);
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
@@ -555,7 +555,7 @@
(*Replacing k by succ(k') yields the similar rule for le!*)
goal Ordinal.thy "!!i j k. [| i<k; j<k |] ==> i Int j < k";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
-by (rtac (Int_commute RS ssubst) 4);
+by (stac Int_commute 4);
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 4);
by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Int_iff]) 3);
by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
--- a/src/ZF/Perm.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Perm.ML Thu Sep 26 15:14:23 1996 +0200
@@ -157,7 +157,7 @@
goalw Perm.thy [inj_def] "!!f. f: inj(A,B) ==> converse(f) : range(f)->A";
by (asm_simp_tac (ZF_ss addsimps [Pi_iff, function_def]) 1);
-by (eresolve_tac [CollectE] 1);
+by (etac CollectE 1);
by (asm_simp_tac (ZF_ss addsimps [apply_iff]) 1);
by (fast_tac (ZF_cs addDs [fun_is_rel]) 1);
qed "inj_converse_fun";
@@ -192,7 +192,7 @@
goal Perm.thy "!!f. [| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b";
by (fast_tac (ZF_cs addss
- (ZF_ss addsimps [bij_def, right_inverse, surj_range])) 1);
+ (ZF_ss addsimps [bij_def, right_inverse, surj_range])) 1);
qed "right_inverse_bij";
(** Converses of injections, surjections, bijections **)
@@ -207,12 +207,12 @@
goal Perm.thy "!!f A B. f: inj(A,B) ==> converse(f): surj(range(f), A)";
by (ITER_DEEPEN (has_fewer_prems 1)
(ares_tac [f_imp_surjective, inj_converse_fun, left_inverse,
- inj_is_fun, range_of_fun RS apply_type]));
+ inj_is_fun, range_of_fun RS apply_type]));
qed "inj_converse_surj";
goalw Perm.thy [bij_def] "!!f A B. f: bij(A,B) ==> converse(f): bij(B,A)";
by (fast_tac (ZF_cs addEs [surj_range RS subst, inj_converse_inj,
- inj_converse_surj]) 1);
+ inj_converse_surj]) 1);
qed "bij_converse_bij";
@@ -307,7 +307,7 @@
by (asm_full_simp_tac
(ZF_ss addsimps [Pi_def, comp_function, Pow_iff, comp_rel]
setloop etac conjE) 1);
-by (rtac (range_rel_subset RS domain_comp_eq RS ssubst) 1 THEN assume_tac 2);
+by (stac (range_rel_subset RS domain_comp_eq) 1 THEN assume_tac 2);
by (fast_tac ZF_cs 1);
qed "comp_fun";
@@ -470,7 +470,7 @@
"!!f g. [| f: bij(A,B); g: bij(C,D); A Int C = 0; B Int D = 0 |] ==> \
\ (f Un g) : bij(A Un C, B Un D)";
by (rtac invertible_imp_bijective 1);
-by (rtac (converse_Un RS ssubst) 1);
+by (stac converse_Un 1);
by (REPEAT (ares_tac [fun_disjoint_Un, bij_is_fun, bij_converse_bij] 1));
qed "bij_disjoint_Un";
@@ -533,7 +533,7 @@
"!!f. [| f: inj(A,B); a~:A; b~:B |] ==> \
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
by (fast_tac (ZF_cs addIs [apply_type]
- addss (ZF_ss addsimps [fun_extend, fun_extend_apply2,
- fun_extend_apply1]) ) 1);
+ addss (ZF_ss addsimps [fun_extend, fun_extend_apply2,
+ fun_extend_apply1]) ) 1);
qed "inj_extend";
--- a/src/ZF/QUniv.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/QUniv.ML Thu Sep 26 15:14:23 1996 +0200
@@ -19,7 +19,7 @@
val [prem] = goalw QUniv.thy [sum_def]
"Transset(C) ==> (A+B) Int C <= (A Int C) + (B Int C)";
-by (rtac (Int_Un_distrib RS ssubst) 1);
+by (stac Int_Un_distrib 1);
by (fast_tac (ZF_cs addSDs [prem RS Transset_Pair_D]) 1);
qed "Transset_sum_Int_subset";
@@ -201,7 +201,7 @@
goalw QUniv.thy [QPair_def,sum_def]
"!!X. Transset(X) ==> \
\ <a;b> Int Vfrom(X, succ(i)) <= <a Int Vfrom(X,i); b Int Vfrom(X,i)>";
-by (rtac (Int_Un_distrib RS ssubst) 1);
+by (stac Int_Un_distrib 1);
by (rtac Un_mono 1);
by (REPEAT (ares_tac [product_Int_Vfrom_subset RS subset_trans,
[Int_lower1, subset_refl] MRS Sigma_mono] 1));
@@ -226,7 +226,7 @@
\ |] ==> <a;b> Int Vset(i) <= (UN j:i. <a Int Vset(j); b Int Vset(j)>)";
by (etac Ord_cases 1 THEN REPEAT_FIRST hyp_subst_tac);
(*0 case*)
-by (rtac (Vfrom_0 RS ssubst) 1);
+by (stac Vfrom_0 1);
by (fast_tac ZF_cs 1);
(*succ(j) case*)
by (rtac (Transset_0 RS QPair_Int_Vfrom_succ_subset RS subset_trans) 1);
--- a/src/ZF/Univ.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/Univ.ML Thu Sep 26 15:14:23 1996 +0200
@@ -10,7 +10,7 @@
(*NOT SUITABLE FOR REWRITING -- RECURSIVE!*)
goal Univ.thy "Vfrom(A,i) = A Un (UN j:i. Pow(Vfrom(A,j)))";
-by (rtac (Vfrom_def RS def_transrec RS ssubst) 1);
+by (stac (Vfrom_def RS def_transrec) 1);
by (simp_tac ZF_ss 1);
qed "Vfrom";
@@ -19,8 +19,8 @@
goal Univ.thy "!!A B. A<=B ==> ALL j. i<=j --> Vfrom(A,i) <= Vfrom(B,j)";
by (eps_ind_tac "i" 1);
by (rtac (impI RS allI) 1);
-by (rtac (Vfrom RS ssubst) 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
+by (stac Vfrom 1);
by (etac Un_mono 1);
by (rtac UN_mono 1);
by (assume_tac 1);
@@ -38,15 +38,15 @@
goal Univ.thy "Vfrom(A,x) <= Vfrom(A,rank(x))";
by (eps_ind_tac "x" 1);
-by (rtac (Vfrom RS ssubst) 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
+by (stac Vfrom 1);
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
qed "Vfrom_rank_subset1";
goal Univ.thy "Vfrom(A,rank(x)) <= Vfrom(A,x)";
by (eps_ind_tac "x" 1);
-by (rtac (Vfrom RS ssubst) 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
+by (stac Vfrom 1);
by (rtac (subset_refl RS Un_mono) 1);
by (rtac UN_least 1);
(*expand rank(x1) = (UN y:x1. succ(rank(y))) in assumptions*)
@@ -70,25 +70,25 @@
(*** Basic closure properties ***)
goal Univ.thy "!!x y. y:x ==> 0 : Vfrom(A,x)";
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac ZF_cs 1);
qed "zero_in_Vfrom";
goal Univ.thy "i <= Vfrom(A,i)";
by (eps_ind_tac "i" 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac ZF_cs 1);
qed "i_subset_Vfrom";
goal Univ.thy "A <= Vfrom(A,i)";
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (rtac Un_upper1 1);
qed "A_subset_Vfrom";
bind_thm ("A_into_Vfrom", A_subset_Vfrom RS subsetD);
goal Univ.thy "!!A a i. a <= Vfrom(A,i) ==> a: Vfrom(A,succ(i))";
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac ZF_cs 1);
qed "subset_mem_Vfrom";
@@ -121,7 +121,7 @@
(*** 0, successor and limit equations fof Vfrom ***)
goal Univ.thy "Vfrom(A,0) = A";
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac eq_cs 1);
qed "Vfrom_0";
@@ -138,14 +138,14 @@
goal Univ.thy "Vfrom(A,succ(i)) = A Un Pow(Vfrom(A,i))";
by (res_inst_tac [("x1", "succ(i)")] (Vfrom_rank_eq RS subst) 1);
by (res_inst_tac [("x1", "i")] (Vfrom_rank_eq RS subst) 1);
-by (rtac (rank_succ RS ssubst) 1);
+by (stac rank_succ 1);
by (rtac (Ord_rank RS Vfrom_succ_lemma) 1);
qed "Vfrom_succ";
(*The premise distinguishes this from Vfrom(A,0); allowing X=0 forces
the conclusion to be Vfrom(A,Union(X)) = A Un (UN y:X. Vfrom(A,y)) *)
val [prem] = goal Univ.thy "y:X ==> Vfrom(A,Union(X)) = (UN y:X. Vfrom(A,y))";
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (rtac equalityI 1);
(*first inclusion*)
by (rtac Un_least 1);
@@ -155,11 +155,11 @@
by (etac UnionE 1);
by (rtac subset_trans 1);
by (etac UN_upper 2);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (etac ([UN_upper, Un_upper2] MRS subset_trans) 1);
(*opposite inclusion*)
by (rtac UN_least 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac ZF_cs 1);
qed "Vfrom_Union";
@@ -170,7 +170,7 @@
val [limiti] = goal Univ.thy
"Limit(i) ==> Vfrom(A,i) = (UN y:i. Vfrom(A,y))";
by (rtac (limiti RS (Limit_has_0 RS ltD) RS Vfrom_Union RS subst) 1);
-by (rtac (limiti RS Limit_Union_eq RS ssubst) 1);
+by (stac (limiti RS Limit_Union_eq) 1);
by (rtac refl 1);
qed "Limit_Vfrom_eq";
@@ -269,7 +269,7 @@
goal Univ.thy "!!i A. Transset(A) ==> Transset(Vfrom(A,i))";
by (eps_ind_tac "i" 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac (ZF_cs addSIs [Transset_Union_family, Transset_Un,
Transset_Pow]) 1);
qed "Transset_Vfrom";
@@ -365,7 +365,7 @@
by (dtac Transset_Vfrom 1);
by (rtac subset_mem_Vfrom 1);
by (rtac (Collect_subset RS subset_trans) 1);
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (rtac (subset_trans RS subset_trans) 1);
by (rtac Un_upper2 3);
by (rtac (succI1 RS UN_upper) 2);
@@ -386,7 +386,7 @@
(*** The set Vset(i) ***)
goal Univ.thy "Vset(i) = (UN j:i. Pow(Vset(j)))";
-by (rtac (Vfrom RS ssubst) 1);
+by (stac Vfrom 1);
by (fast_tac eq_cs 1);
qed "Vset";
@@ -398,9 +398,9 @@
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. b : Vset(i) --> rank(b) < i";
by (rtac (ordi RS trans_induct) 1);
-by (rtac (Vset RS ssubst) 1);
+by (stac Vset 1);
by (safe_tac ZF_cs);
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
by (rtac UN_succ_least_lt 1);
by (fast_tac ZF_cs 2);
by (REPEAT (ares_tac [ltI] 1));
@@ -412,7 +412,7 @@
val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
by (rtac (ordi RS trans_induct) 1);
by (rtac allI 1);
-by (rtac (Vset RS ssubst) 1);
+by (stac Vset 1);
by (fast_tac (ZF_cs addSIs [rank_lt RS ltD]) 1);
qed "Vset_rank_imp2";
@@ -433,7 +433,7 @@
qed "Vset_rank_iff";
goal Univ.thy "!!i. Ord(i) ==> rank(Vset(i)) = i";
-by (rtac (rank RS ssubst) 1);
+by (stac rank 1);
by (rtac equalityI 1);
by (safe_tac ZF_cs);
by (EVERY' [rtac UN_I,
@@ -471,7 +471,7 @@
(*NOT SUITABLE FOR REWRITING: recursive!*)
goalw Univ.thy [Vrec_def] "Vrec(a,H) = H(a, lam x:Vset(rank(a)). Vrec(x,H))";
-by (rtac (transrec RS ssubst) 1);
+by (stac transrec 1);
by (simp_tac (ZF_ss addsimps [Ord_rank, Ord_succ, VsetD RS ltD RS beta,
VsetI RS beta, le_refl]) 1);
qed "Vrec";
@@ -511,7 +511,7 @@
"[| a <= univ(X); \
\ !!i. i:nat ==> a Int Vfrom(X,i) <= b \
\ |] ==> a <= b";
-by (rtac (aprem RS subset_univ_eq_Int RS ssubst) 1);
+by (stac (aprem RS subset_univ_eq_Int) 1);
by (rtac UN_least 1);
by (etac iprem 1);
qed "univ_Int_Vfrom_subset";
--- a/src/ZF/WF.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/WF.ML Thu Sep 26 15:14:23 1996 +0200
@@ -207,7 +207,7 @@
val [major] = goalw WF.thy [is_recfun_def]
"is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)";
-by (rtac (major RS ssubst) 1);
+by (stac major 1);
by (rtac (lamI RS rangeI RS lam_type) 1);
by (assume_tac 1);
qed "is_recfun_type";
@@ -300,7 +300,7 @@
goalw WF.thy [wftrec_def]
"!!r. [| wf(r); trans(r) |] ==> \
\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))";
-by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1);
+by (stac (rewrite_rule [is_recfun_def] unfold_the_recfun) 1);
by (ALLGOALS (asm_simp_tac
(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut])));
qed "wftrec";
@@ -310,7 +310,7 @@
(*NOT SUITABLE FOR REWRITING since it is recursive!*)
val [wfr] = goalw WF.thy [wfrec_def]
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))";
-by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1);
+by (stac (wfr RS wf_trancl RS wftrec) 1);
by (rtac trans_trancl 1);
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1);
by (etac r_into_trancl 1);
@@ -330,7 +330,7 @@
\ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \
\ |] ==> wfrec(r,a,H) : B(a)";
by (res_inst_tac [("a","a")] wf_induct2 1);
-by (rtac (wfrec RS ssubst) 4);
+by (stac wfrec 4);
by (REPEAT (ares_tac (prems@[lam_type]) 1
ORELSE eresolve_tac [spec RS mp, underD] 1));
qed "wfrec_type";
--- a/src/ZF/add_ind_def.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/add_ind_def.ML Thu Sep 26 15:14:23 1996 +0200
@@ -194,10 +194,10 @@
(*Combine split terms using case; yields the case operator for one part*)
fun call_case case_list =
let fun call_f (free,[]) = Abs("null", iT, free)
- | call_f (free,args) =
+ | call_f (free,args) =
CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
- Ind_Syntax.iT
- free
+ Ind_Syntax.iT
+ free
in fold_bal (app Su.elim) (map call_f case_list) end;
(** Generating function variables for the case definition
--- a/src/ZF/cartprod.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/cartprod.ML Thu Sep 26 15:14:23 1996 +0200
@@ -18,7 +18,7 @@
val fsplitE : thm (*elim rule; apparently never used*)
end;
-signature CARTPROD = (** Derived syntactic functions for produts **)
+signature CARTPROD = (** Derived syntactic functions for produts **)
sig
val ap_split : typ -> typ -> term -> term
val factors : typ -> typ list
@@ -52,8 +52,8 @@
(*Make a well-typed instance of "split"*)
fun split_const T = Const(Pr.split_name,
- [[Ind_Syntax.iT, Ind_Syntax.iT]--->T,
- Ind_Syntax.iT] ---> T);
+ [[Ind_Syntax.iT, Ind_Syntax.iT]--->T,
+ Ind_Syntax.iT] ---> T);
(*In ap_split S T u, term u expects separate arguments for the factors of S,
with result type T. The call creates a new term expecting one argument
@@ -61,9 +61,9 @@
fun ap_split (Type("*", [T1,T2])) T3 u =
split_const T3 $
Abs("v", Ind_Syntax.iT, (*Not T1, as it involves pseudo-product types*)
- ap_split T2 T3
- ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
- Bound 0))
+ ap_split T2 T3
+ ((ap_split T1 (factors T2 ---> T3) (incr_boundvars 1 u)) $
+ Bound 0))
| ap_split T T3 u = u;
(*Makes a nested tuple from a list, following the product type structure*)
@@ -78,11 +78,11 @@
(*Uncurries any Var involving pseudo-product type T1 in the rule*)
fun split_rule_var (t as Var(v, Type("fun",[T1,T2])), rl) =
let val T' = factors T1 ---> T2
- val newt = ap_split T1 T2 (Var(v,T'))
- val cterm = Thm.cterm_of (#sign(rep_thm rl))
+ val newt = ap_split T1 T2 (Var(v,T'))
+ val cterm = Thm.cterm_of (#sign(rep_thm rl))
in
- remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
- cterm newt)]) rl)
+ remove_split (instantiate ([], [(cterm (Var(v, Ind_Syntax.iT-->T2)),
+ cterm newt)]) rl)
end
| split_rule_var (t,rl) = rl;
--- a/src/ZF/domrange.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/domrange.ML Thu Sep 26 15:14:23 1996 +0200
@@ -79,7 +79,7 @@
qed_goalw "range_subset" ZF.thy [range_def] "range(A*B) <= B"
(fn _ =>
- [ (rtac (converse_prod RS ssubst) 1),
+ [ (stac converse_prod 1),
(rtac domain_subset 1) ]);
--- a/src/ZF/func.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/func.ML Thu Sep 26 15:14:23 1996 +0200
@@ -184,7 +184,7 @@
"(!!x. x:A ==> EX! y. Q(x,y)) ==> EX f. ALL x:A. Q(x, f`x)";
by (res_inst_tac [("x", "lam x: A. THE y. Q(x,y)")] exI 1);
by (rtac ballI 1);
-by (rtac (beta RS ssubst) 1);
+by (stac beta 1);
by (assume_tac 1);
by (etac (major RS theI) 1);
qed "lam_theI";
--- a/src/ZF/indrule.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/indrule.ML Thu Sep 26 15:14:23 1996 +0200
@@ -83,8 +83,8 @@
val min_ss = empty_ss
setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
setsolver (fn prems => resolve_tac (triv_rls@prems)
- ORELSE' assume_tac
- ORELSE' etac FalseE);
+ ORELSE' assume_tac
+ ORELSE' etac FalseE);
val quant_induct =
prove_goalw_cterm part_rec_defs
@@ -118,13 +118,13 @@
fun mk_predpair rec_tm =
let val rec_name = (#1 o dest_Const o head_of) rec_tm
val pfree = Free(pred_name ^ "_" ^ rec_name,
- elem_factors ---> Ind_Syntax.oT)
+ elem_factors ---> Ind_Syntax.oT)
val qconcl =
foldr Ind_Syntax.mk_all
- (elem_frees,
- Ind_Syntax.imp $
- (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
- $ (list_comb (pfree, elem_frees)))
+ (elem_frees,
+ Ind_Syntax.imp $
+ (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
+ $ (list_comb (pfree, elem_frees)))
in (CP.ap_split elem_type Ind_Syntax.oT pfree,
qconcl)
end;
@@ -141,15 +141,15 @@
Ind_Syntax.mk_tprop
(Ind_Syntax.mk_all_imp
(big_rec_tm,
- Abs("z", Ind_Syntax.iT,
- fold_bal (app Ind_Syntax.conj)
- (map mk_rec_imp (Inductive.rec_tms~~preds)))))
+ Abs("z", Ind_Syntax.iT,
+ fold_bal (app Ind_Syntax.conj)
+ (map mk_rec_imp (Inductive.rec_tms~~preds)))))
and mutual_induct_concl =
Ind_Syntax.mk_tprop(fold_bal (app Ind_Syntax.conj) qconcls);
val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, PartE, mp],
- resolve_tac [allI, impI, conjI, Part_eqI],
- dresolve_tac [spec, mp, Pr.fsplitD]];
+ resolve_tac [allI, impI, conjI, Part_eqI],
+ dresolve_tac [spec, mp, Pr.fsplitD]];
val lemma = (*makes the link between the two induction rules*)
prove_goalw_cterm part_rec_defs
@@ -157,7 +157,7 @@
(fn prems =>
[cut_facts_tac prems 1,
REPEAT (rewrite_goals_tac [Pr.split_eq] THEN
- lemma_tac 1)]);
+ lemma_tac 1)]);
(*Mutual induction follows by freeness of Inl/Inr.*)
@@ -190,10 +190,10 @@
IF_UNSOLVED (*simp_tac may have finished it off!*)
((*simplify assumptions*)
(*some risk of excessive simplification here -- might have
- to identify the bare minimum set of rewrites*)
+ to identify the bare minimum set of rewrites*)
full_simp_tac
- (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
- THEN
+ (mut_ss addsimps (conj_simps @ imp_simps @ quant_simps)) 1
+ THEN
(*unpackage and use "prem" in the corresponding place*)
REPEAT (rtac impI 1) THEN
rtac (rewrite_rule all_defs prem) 1 THEN
@@ -225,7 +225,7 @@
val inst =
case elem_frees of [_] => I
| _ => instantiate ([], [(cterm_of sign (Var(("x",1), Ind_Syntax.iT)),
- cterm_of sign elem_tuple)]);
+ cterm_of sign elem_tuple)]);
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
@@ -236,8 +236,8 @@
(*strip quantifier*)
val induct = standard
(CP.split_rule_var
- (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
- induct0));
+ (Var((pred_name,2), elem_type --> Ind_Syntax.oT),
+ induct0));
(*Just "True" unless there's true mutual recursion. This saves storage.*)
val mutual_induct =
--- a/src/ZF/intr_elim.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/ZF/intr_elim.ML Thu Sep 26 15:14:23 1996 +0200
@@ -98,7 +98,7 @@
fun intro_tacsf disjIn prems =
[(*insert prems and underlying sets*)
cut_facts_tac prems 1,
- DETERM (rtac (unfold RS ssubst) 1),
+ DETERM (stac unfold 1),
REPEAT (resolve_tac [Part_eqI,CollectI] 1),
(*Now 2-3 subgoals: typechecking, the disjunction, perhaps equality.*)
rtac disjIn 2,