# HG changeset patch # User paulson # Date 843743663 -7200 # Node ID 639de962ded4525b382ba4b1311ccc068e56604b # Parent 1bbf1bdcaf56d0d75bfd1d7fc4b79a42f1cefcdd Ran expandshort; used stac instead of ssubst diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cfun1.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cfun2.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cfun3.ML --- 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) diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cont.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cprod1.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cprod2.ML --- 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)< [ - (rtac (inst_cprod_po RS ssubst) 1), + (stac inst_cprod_po 1), (rtac less_cprod1b 1) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Cprod3.ML --- 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] " = 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` = 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Fix.ML --- 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 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]; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Fun1.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Fun2.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Holcfb.ML --- 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))" *) diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Lift1.ML --- 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< [ - (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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Lift2.ML --- 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)< [ - (rtac (inst_lift_po RS ssubst) 1), + (stac inst_lift_po 1), (rtac less_lift1c 1) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Lift3.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Pcpo.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Porder.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/ROOT.ML --- 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; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Sprod0.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Sprod1.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Sprod2.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Sprod3.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Ssum2.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Ssum3.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Tr1.ML --- 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" diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/Void.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/ccc1.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/domain/theorems.ML --- 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 *) diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/ex/Hoare.ML --- 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) diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/ex/Loop.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/ex/loeckx.ML --- 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); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Coind.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Dagstuhl.ML --- 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(); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Dlist.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Dnat.ML --- 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), diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Dnat2.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Stream.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/HOLCF/explicit_domains/Stream2.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Arith.ML --- 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 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Cardinal.ML --- 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 ~(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); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Cardinal_AC.ML --- 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|"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Epsilon.ML --- 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); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Finite.ML --- 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/List.ML --- 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Nat.ML --- 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/OrderType.ML --- 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]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Ordinal.ML --- 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 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 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)); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Perm.ML --- 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(,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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/QUniv.ML --- 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) ==> \ \ Int Vfrom(X, succ(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 @@ \ |] ==> Int Vset(i) <= (UN j:i. )"; 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); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/Univ.ML --- 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/WF.ML --- 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/add_ind_def.ML --- 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 diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/cartprod.ML --- 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; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/domrange.ML --- 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) ]); diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/func.ML --- 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"; diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/indrule.ML --- 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 = diff -r 1bbf1bdcaf56 -r 639de962ded4 src/ZF/intr_elim.ML --- 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,