# HG changeset patch # User wenzelm # Date 1008185851 -3600 # Node ID 7ad150f5fc1099d3c4e3e63680f0555974c8cdb9 # Parent 0a01efff43e99e72a4fc96a5b96f56a31dac6535 isatool expandshort; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/Cfun2.ML --- a/src/HOLCF/Cfun2.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/HOLCF/Cfun2.ML Wed Dec 12 20:37:31 2001 +0100 @@ -94,9 +94,9 @@ (* ?x2 << ?x1 ==> ?fo5$?x2 << ?fo5$?x1 *) Goal "chain Y ==> chain (%i. f\\(Y i))"; -br chainI 1; -br monofun_cfun_arg 1; -be chainE 1; +by (rtac chainI 1); +by (rtac monofun_cfun_arg 1); +by (etac chainE 1); qed "chain_monofun"; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/FOCUS/Buffer_adm.ML --- a/src/HOLCF/FOCUS/Buffer_adm.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML Wed Dec 12 20:37:31 2001 +0100 @@ -86,7 +86,7 @@ (K [ rtac (BufAC_Cmt_unfold RS iffD2) 1, strip_tac 1, - forward_tac [Buf_f_d_req] 1, + ftac Buf_f_d_req 1, auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]); (*adm_BufAC_Asm*) @@ -118,7 +118,7 @@ by (strip_tac 1); by (stac BufAC_Cmt_F_def3 1); by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1); -by (Safe_tac); +by Safe_tac; by ( etac Buf_f_empty 1); by ( etac Buf_f_d 1); by ( dtac Buf_f_d_req 1); @@ -215,8 +215,8 @@ (**** new approach for admissibility, reduces itself to absurdity *************) Goal "adm (\\x. x\\BufAC_Asm)"; -by(rtac def_gfp_admI 1); -by(rtac BufAC_Asm_def 1); +by (rtac def_gfp_admI 1); +by (rtac BufAC_Asm_def 1); b y Safe_tac; b y rewtac BufAC_Asm_F_def; b y Safe_tac; @@ -238,7 +238,7 @@ b y Clarsimp_tac 1; b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1; b y res_inst_tac [("x","Xa")] exI 1; -br allI 1; +by (rtac allI 1); b y rotate_tac ~1 1; b y eres_inst_tac [("x","i")] allE 1; b y Clarsimp_tac 1; @@ -271,8 +271,8 @@ qed "adm_non_BufAC_Asm"; Goal "f \\ BufEq \\ adm (\\u. u \\ BufAC_Asm \\ (u, f\\u) \\ BufAC_Cmt)"; -by(rtac triv_admI 1); -by(Clarify_tac 1); -by(eatac Buf_Eq_imp_AC_lemma 1 1); +by (rtac triv_admI 1); +by (Clarify_tac 1); +by (eatac Buf_Eq_imp_AC_lemma 1 1); (* this is what we originally aimed to show, using admissibilty :-( *) qed "adm_BufAC"; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/Pcpo.ML --- a/src/HOLCF/Pcpo.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/HOLCF/Pcpo.ML Wed Dec 12 20:37:31 2001 +0100 @@ -52,18 +52,18 @@ Goal "chain (Y::nat=>'a::cpo) ==> lub(range (%i. Y(i + j))) = lub(range Y)"; by (rtac antisym_less 1); -br lub_range_mono 1; +by (rtac lub_range_mono 1); by (Fast_tac 1); by (atac 1); -be chain_shift 1; -br is_lub_thelub 1; -ba 1; -br ub_rangeI 1; -br trans_less 1; -br is_ub_thelub 2; -be chain_shift 2; -be chain_mono3 1; -br le_add1 1; +by (etac chain_shift 1); +by (rtac is_lub_thelub 1); +by (assume_tac 1); +by (rtac ub_rangeI 1); +by (rtac trans_less 1); +by (rtac is_ub_thelub 2); +by (etac chain_shift 2); +by (etac chain_mono3 1); +by (rtac le_add1 1); qed "lub_range_shift"; Goal "chain Y ==> max_in_chain i Y = (lub(range(Y)) = ((Y i)::'a::cpo))"; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/Porder.ML --- a/src/HOLCF/Porder.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/HOLCF/Porder.ML Wed Dec 12 20:37:31 2001 +0100 @@ -38,7 +38,7 @@ (* ------------------------------------------------------------------------ *) Goalw [tord_def] "chain(F) ==> tord(range(F))"; -by (Safe_tac); +by Safe_tac; by (rtac nat_less_cases 1); by (ALLGOALS (fast_tac (claset() addIs [chain_mono]))); qed "chain_tord"; @@ -92,9 +92,9 @@ qed "chainI"; Goal "chain Y ==> chain (%i. Y (i + j))"; -br chainI 1; +by (rtac chainI 1); by (Clarsimp_tac 1); -be chainE 1; +by (etac chainE 1); qed "chain_shift"; (* ------------------------------------------------------------------------ *) diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/ex/Stream.ML --- a/src/HOLCF/ex/Stream.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/HOLCF/ex/Stream.ML Wed Dec 12 20:37:31 2001 +0100 @@ -28,7 +28,7 @@ qed "scons_eq_UU"; Goal "[| a && x = UU; a ~= UU |] ==> R"; -by (dresolve_tac [stream_con_rew2] 1); +by (dtac stream_con_rew2 1); by (contr_tac 1); qed "scons_not_empty"; @@ -534,7 +534,7 @@ \!s. #(s::'a::flat stream) = #t & s << t --> s = t"; by (etac stream_finite_ind 1); by (fast_tac (claset() addDs [eq_UU_iff RS iffD2]) 1); -by (Safe_tac); +by Safe_tac; by (stream_case_tac "sa" 1); by (dtac sym 1); by (Asm_full_simp_tac 1); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/Induct/FoldSet.ML --- a/src/ZF/Induct/FoldSet.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/Induct/FoldSet.ML Wed Dec 12 20:37:31 2001 +0100 @@ -37,7 +37,7 @@ Goal "[| : fold_set(A, B, f,e); x:C; x:A |] \ \ ==> : fold_set(A, B, f, e)"; -by (forward_tac [fold_set_rhs] 1); +by (ftac fold_set_rhs 1); by (etac (cons_Diff RS subst) 1 THEN resolve_tac fold_set.intrs 1); by (auto_tac (claset() addIs [f_type], simpset())); qed "Diff1_fold_set"; @@ -45,7 +45,7 @@ Goal "[| C:Fin(A); e:B |] ==> EX x. : fold_set(A, B, f,e)"; by (etac Fin_induct 1); by (ALLGOALS(Clarify_tac)); -by (forward_tac [fold_set_rhs] 2); +by (ftac fold_set_rhs 2); by (cut_inst_tac [("x", "x"), ("y", "xa")] f_type 2); by (REPEAT(blast_tac (claset() addIs fold_set.intrs) 1)); qed_spec_mp "Fin_imp_fold_set"; @@ -104,7 +104,7 @@ Goal "[| : fold_set(A, B, f, e); \ \ : fold_set(A, B, f, e); e:B |] ==> y=x"; by (forward_tac [fold_set_lhs RS Fin_into_Finite] 1); -by (rewrite_goals_tac [Finite_def]); +by (rewtac Finite_def); by (Clarify_tac 1); by (res_inst_tac [("n", "succ(n)")] lemma 1); by (auto_tac (claset() addIs @@ -171,7 +171,7 @@ by Auto_tac; by (resolve_tac [fold_set_mono RS subsetD] 1); by (Blast_tac 2); -by (dresolve_tac [fold_set_mono2] 3); +by (dtac fold_set_mono2 3); by (auto_tac (claset() addIs [Fin_imp_fold_set], simpset() addsimps [symmetric fold_def, fold_equality])); qed "fold_cons"; @@ -328,10 +328,10 @@ by (Blast_tac 1); by (asm_full_simp_tac (simpset() addsimps [major,subset_cons_iff]@prems) 1); by Safe_tac; -by (forward_tac [subset_Finite] 1); +by (ftac subset_Finite 1); by (assume_tac 1); by (Blast_tac 1); -by (forward_tac [subset_Finite] 1); +by (ftac subset_Finite 1); by (assume_tac 1); by (subgoal_tac "C = cons(x, C - {x})" 1); by (Blast_tac 2); @@ -377,7 +377,7 @@ by (case_tac "Finite(A)" 1); by (blast_tac (claset() addIs [setsum_succD_lemma RS bspec RS mp]) 1); -by (rewrite_goals_tac [setsum_def]); +by (rewtac setsum_def); by (auto_tac (claset(), simpset() delsimps [int_of_0, int_of_succ] addsimps [int_succ_int_1 RS sym, int_of_0 RS sym])); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/Induct/Multiset.ML --- a/src/ZF/Induct/Multiset.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/Induct/Multiset.ML Wed Dec 12 20:37:31 2001 +0100 @@ -106,7 +106,7 @@ Goalw [mdiff_def, multiset_def] "[| multiset(M); mset_of(M)<=A |] ==> mset_of(M -# N) <= A"; by (auto_tac (claset(), simpset() addsimps [normalize_def])); -by (rewrite_goals_tac [mset_of_def]); +by (rewtac mset_of_def); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [multiset_fun_iff]))); by (ALLGOALS(Clarify_tac)); by (ALLGOALS(rotate_simp_tac "M:?u")); @@ -242,7 +242,7 @@ by (rewrite_goals_tac [munion_def, mdiff_def, msingle_def, normalize_def, mset_of_def]); by (auto_tac (claset(), simpset() addsimps [multiset_fun_iff])); -by (resolve_tac [fun_extension] 1); +by (rtac fun_extension 1); by Auto_tac; by (res_inst_tac [("P", "%x. ?u : Pi(x, ?v)")] subst 1); by (rtac restrict_type 2); @@ -546,7 +546,7 @@ \ (setsum(%x. $# mcount(M, x), {x:mset_of(M). 0 < M`x}) = $# n) --> P(M))"; by (rtac (major RS nat_induct) 1); by (ALLGOALS(Clarify_tac)); -by (forward_tac [msize_eq_0_iff] 1); +by (ftac msize_eq_0_iff 1); by (auto_tac (claset(), simpset() addsimps [mset_of_def, multiset_def, multiset_fun_iff, msize_def]@prems)); @@ -632,7 +632,7 @@ \ ==> P(M)"; by (subgoal_tac "EX n:nat. setsum(\\x. $# mcount(M, x), \ \ {x : mset_of(M) . 0 < M ` x}) = $# n" 1); -by (resolve_tac [not_zneg_int_of] 2); +by (rtac not_zneg_int_of 2); by (ALLGOALS(asm_simp_tac (simpset() addsimps [znegative_iff_zless_0, not_zless_iff_zle]))); by (rtac g_zpos_imp_setsum_zpos 2); @@ -649,7 +649,7 @@ Goalw [multiset_def, msingle_def] "[| multiset(M); a ~:mset_of(M) |] ==> M +# {#a#} = cons(, M)"; by (auto_tac (claset(), simpset() addsimps [munion_def])); -by (rewrite_goals_tac [mset_of_def]); +by (rewtac mset_of_def); by (rotate_simp_tac "M:?u" 1); by (rtac fun_extension 1 THEN rtac lam_type 1); by (ALLGOALS(Asm_full_simp_tac)); @@ -666,7 +666,7 @@ "[| multiset(M); a:mset_of(M) |] ==> M +# {#a#} = M(a:=M`a #+ 1)"; by (auto_tac (claset(), simpset() addsimps [munion_def, multiset_fun_iff, msingle_def])); -by (rewrite_goals_tac [mset_of_def]); +by (rewtac mset_of_def); by (rotate_simp_tac "M:?u" 1); by (subgoal_tac "A Un {a} = A" 1); by (rtac fun_extension 1); @@ -776,9 +776,9 @@ Goalw [multiset_on_def, multiset_def, mset_of_def] "M:A-||>nat-{0} ==> multiset[A](M)"; -by (forward_tac [FiniteFun_is_fun] 1); +by (ftac FiniteFun_is_fun 1); by (dtac FiniteFun_domain_Fin 1); -by (forward_tac [FinD] 1); +by (ftac FinD 1); by (Clarify_tac 1); by (res_inst_tac [("x", "domain(M)")] exI 1); by (blast_tac (claset() addIs [Fin_into_Finite]) 1); @@ -861,19 +861,19 @@ Goal "[| :multirel1(A, r); multiset[A](M0) |] ==> \ \ (EX M. :multirel1(A, r) & N = M +# {#a#}) | \ \ (EX K. multiset[A](K) & (ALL b:mset_of(K). :r) & N = M0 +# K)"; -by (forward_tac [multirel1D] 1); +by (ftac multirel1D 1); by (asm_full_simp_tac (simpset() addsimps [multirel1_iff]) 1); by (auto_tac (claset(), simpset() addsimps [munion_eq_conv_exist])); by (ALLGOALS(res_inst_tac [("x", "Ka +# K")] exI)); by Auto_tac; -by (rewrite_goals_tac [multiset_on_def]); +by (rewtac multiset_on_def); by (asm_simp_tac (simpset() addsimps [munion_left_cancel, munion_assoc]) 1); by (auto_tac (claset(), simpset() addsimps [munion_commute])); qed "less_munion"; Goal "[| multiset[A](M); a:A |] ==> : multirel1(A, r)"; by (auto_tac (claset(), simpset() addsimps [multirel1_iff])); -by (rewrite_goals_tac [multiset_on_def]); +by (rewtac multiset_on_def); by (res_inst_tac [("x", "a")] exI 1); by (Clarify_tac 1); by (res_inst_tac [("x", "M")] exI 1); @@ -1112,7 +1112,7 @@ by Auto_tac; by (res_inst_tac [("x", "a")] exI 1); by (res_inst_tac [("x", "M -# {#a#}")] exI 1); -by (forward_tac [multiset_on_imp_multiset] 1); +by (ftac multiset_on_imp_multiset 1); by (Asm_simp_tac 1); by (auto_tac (claset(), simpset() addsimps [multiset_on_def])); qed "msize_eq_succ_imp_eq_union"; @@ -1133,7 +1133,7 @@ by (subgoal_tac "msize(J)=$# succ(x)" 1); by (Asm_simp_tac 2); by (forw_inst_tac [("A", "A")] msize_eq_succ_imp_eq_union 1); -by (rewrite_goals_tac [multiset_on_def]); +by (rewtac multiset_on_def); by (Clarify_tac 3 THEN rotate_tac ~1 3); by (ALLGOALS(Asm_full_simp_tac)); by (rename_tac "J'" 1); @@ -1245,7 +1245,7 @@ Goal "[|:multirel1(A, r); multiset[A](K)|] ==> : multirel1(A, r)"; -by (forward_tac [multirel1D] 1); +by (ftac multirel1D 1); by (auto_tac (claset(), simpset() addsimps [multirel1_iff, multiset_on_def])); by (res_inst_tac [("x", "a")] exI 1); by (Asm_simp_tac 1); @@ -1258,7 +1258,7 @@ Goal "[| :multirel(A, r); multiset[A](K) |]==>:multirel(A, r)"; -by (forward_tac [multirelD] 1); +by (ftac multirelD 1); by (full_simp_tac (simpset() addsimps [multirel_def]) 1); by (Clarify_tac 1); by (dres_inst_tac [("psi", ":multirel1(A, r)^+")] asm_rl 1); @@ -1278,11 +1278,11 @@ Goal "[|:multirel(A, r); multiset[A](K)|] ==> :multirel(A, r)"; -by (forward_tac [multirelD] 1); +by (ftac multirelD 1); by (res_inst_tac [("P", "%x. :multirel(A, r)")] (munion_commute RS subst) 1); by (stac (munion_commute RS sym) 3); by (rtac munion_multirel_mono2 5); -by (rewrite_goals_tac [multiset_on_def]); +by (rewtac multiset_on_def); by Auto_tac; qed "munion_multirel_mono1"; @@ -1468,7 +1468,7 @@ "[| M <#= K; N <#= L |] ==> M +# N <#= K +# L"; by (forw_inst_tac [("M", "M")] mle_imp_omultiset 1); by (forw_inst_tac [("M", "N")] mle_imp_omultiset 1); -by (rewrite_goals_tac [mle_def]); +by (rewtac mle_def); by (ALLGOALS(Asm_full_simp_tac)); by (REPEAT(etac disjE 1)); by (etac disjE 3); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/Comp.ML --- a/src/ZF/UNITY/Comp.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/Comp.ML Wed Dec 12 20:37:31 2001 +0100 @@ -96,7 +96,7 @@ qed "Join_component_iff"; Goal "[| F component G; G:A co B; F:program |] ==> F : A co B"; -by (forward_tac [constrainsD2] 1); +by (ftac constrainsD2 1); by (rotate_tac ~1 1); by (auto_tac (claset(), simpset() addsimps [constrains_def, component_eq_subset])); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/Constrains.ML --- a/src/ZF/UNITY/Constrains.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/Constrains.ML Wed Dec 12 20:37:31 2001 +0100 @@ -18,7 +18,7 @@ qed "reachable_type"; Goalw [st_set_def] "st_set(reachable(F))"; -by (resolve_tac [reachable_type] 1); +by (rtac reachable_type 1); qed "st_set_reachable"; AddIffs [st_set_reachable]; @@ -168,7 +168,7 @@ by (asm_simp_tac (simpset() delsimps INT_simps addsimps [Constrains_def]@INT_extend_simps) 1); by (rtac constrains_INT 1); -by (dresolve_tac [major] 1); +by (dtac major 1); by (auto_tac (claset(), simpset() addsimps [Constrains_def])); qed "Constrains_INT"; @@ -325,7 +325,7 @@ (*the RHS is the traditional definition of the "always" operator*) Goal "Always(A) = {F:program. reachable(F) <= A}"; -br equalityI 1; +by (rtac equalityI 1); by (ALLGOALS(Clarify_tac)); by (auto_tac (claset() addDs [invariant_includes_reachable], simpset() addsimps [subset_Int_iff, invariant_reachable, @@ -337,7 +337,7 @@ qed "Always_type"; Goal "Always(state) = program"; -br equalityI 1; +by (rtac equalityI 1); by (auto_tac (claset() addDs [Always_type RS subsetD, reachable_type RS subsetD], simpset() addsimps [Always_eq_includes_reachable])); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/FP.ML --- a/src/ZF/UNITY/FP.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/FP.ML Wed Dec 12 20:37:31 2001 +0100 @@ -67,7 +67,7 @@ by (Clarify_tac 1); by (dres_inst_tac [("x", "{x}")] spec 1); by (asm_full_simp_tac (simpset() addsimps [Int_cons_right]) 1); -by (forward_tac [stableD2] 1); +by (ftac stableD2 1); by (auto_tac (claset(), simpset() addsimps [cons_absorb, st_set_def])); qed "FP_Orig_subset_FP"; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/GenPrefix.ML --- a/src/ZF/UNITY/GenPrefix.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/GenPrefix.ML Wed Dec 12 20:37:31 2001 +0100 @@ -330,7 +330,7 @@ \ (ALL i:nat. i < length(xs) --> : r))"; by (rtac iffI 1); by (forward_tac [gen_prefix.dom_subset RS subsetD] 1); -by (forward_tac [gen_prefix_length_le] 1); +by (ftac gen_prefix_length_le 1); by (ALLGOALS(Clarify_tac)); by (rtac nth_imp_gen_prefix 2); by (dtac (rotate_prems 4 gen_prefix_imp_nth) 1); @@ -485,7 +485,7 @@ by Safe_tac; by (Blast_tac 1); by (subgoal_tac "length(xs) #+ (x #- length(xs)) = x" 1); -by (rtac (nth_drop RS ssubst) 1); +by (stac nth_drop 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI]))); by (rtac (nat_diff_split RS iffD2) 1); by Auto_tac; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/Guar.ML --- a/src/ZF/UNITY/Guar.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/Guar.ML Wed Dec 12 20:37:31 2001 +0100 @@ -529,7 +529,7 @@ (* To be moved to WFair.ML *) Goal "[| F:A co A Un B; F:transient(A); st_set(B) |] ==> F:A leadsTo B"; -by (forward_tac [constrainsD2] 1); +by (ftac constrainsD2 1); by (dres_inst_tac [("B", "A-B")] constrains_weaken_L 1); by (dres_inst_tac [("B", "A-B")] transient_strengthen 2); by (rtac (ensuresI RS leadsTo_Basis) 3); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/SubstAx.ML --- a/src/ZF/UNITY/SubstAx.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/SubstAx.ML Wed Dec 12 20:37:31 2001 +0100 @@ -70,7 +70,7 @@ (*** Derived rules ***) Goal "F : A leadsTo B ==> F : A LeadsTo B"; -by (forward_tac [leadsToD2] 1); +by (ftac leadsToD2 1); by (Clarify_tac 1); by (asm_simp_tac (simpset() addsimps [LeadsTo_eq]) 1); by (blast_tac (claset() addIs [leadsTo_weaken_L]) 1); @@ -106,7 +106,7 @@ "[|(!!s. s:A ==> F:{s} LeadsTo B); F:program|]==>F:A LeadsTo B"; by (cut_facts_tac [program] 1); by (stac (UN_singleton RS sym) 1 THEN rtac LeadsTo_UN 1); -by (forward_tac [major] 1); +by (ftac major 1); by Auto_tac; qed "single_LeadsTo_I"; @@ -209,7 +209,7 @@ by (cut_facts_tac [minor] 1); by (rtac LeadsTo_Union 1); by (ALLGOALS(Clarify_tac)); -by (forward_tac [major] 1); +by (ftac major 1); by (blast_tac (claset() addIs [LeadsTo_weaken_R]) 1); qed "LeadsTo_UN_UN"; @@ -285,7 +285,7 @@ Goal "[| F : A LeadsTo A'; F : B Unless B'|]==> F:(A Int B) LeadsTo ((A' Int B) Un B')"; -by (rewrite_goals_tac [Unless_def]); +by (rewtac Unless_def); by (dtac PSP 1); by (assume_tac 1); by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, subset_imp_LeadsTo]) 1); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/UNITY.ML --- a/src/ZF/UNITY/UNITY.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/UNITY.ML Wed Dec 12 20:37:31 2001 +0100 @@ -117,7 +117,7 @@ qed "Init_type"; Goalw [st_set_def] "st_set(Init(F))"; -by (resolve_tac [Init_type] 1); +by (rtac Init_type 1); qed "st_set_Init"; AddIffs [st_set_Init]; @@ -439,7 +439,7 @@ "[|(!!i. i:I ==> F:A(i) co A'(i)); F:program |]==> F:(UN i:I. A(i)) co (UN i:I. A'(i))"; by (cut_facts_tac [minor] 1); by Safe_tac; -by (ALLGOALS(forward_tac [major])); +by (ALLGOALS(ftac major )); by (ALLGOALS(Asm_full_simp_tac)); by (REPEAT(Blast_tac 1)); qed "constrains_UN"; @@ -486,8 +486,8 @@ by (etac not_emptyE 1); by Safe_tac; by (forw_inst_tac [("i", "xd")] major 1); -by (forward_tac [major] 2); -by (forward_tac [major] 3); +by (ftac major 2); +by (ftac major 3); by (REPEAT(Force_tac 1)); qed "constrains_INT"; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/Union.ML --- a/src/ZF/UNITY/Union.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/Union.ML Wed Dec 12 20:37:31 2001 +0100 @@ -289,7 +289,7 @@ by (asm_simp_tac (simpset() addsimps [JN_constrains]) 1); by (Clarify_tac 1); by (forw_inst_tac [("i", "x")] major 1); -by (forward_tac [constrainsD2] 1); +by (ftac constrainsD2 1); by (Asm_full_simp_tac 1); by (blast_tac (claset() addIs [constrains_weaken]) 1); qed "JN_constrains_weaken"; @@ -319,10 +319,10 @@ by (auto_tac (claset() addSIs [initially_JN_I] addDs [major], simpset() addsimps [invariant_def, JN_stable])); by (thin_tac "i:I" 1); -by (forward_tac [major] 1); +by (ftac major 1); by (dtac major 2); by (auto_tac (claset(), simpset() addsimps [invariant_def])); -by (ALLGOALS(forward_tac [stableD2])); +by (ALLGOALS(ftac stableD2 )); by Auto_tac; qed "invariant_JN_I"; @@ -355,7 +355,7 @@ by (rotate_tac ~1 3); by (rotate_tac ~1 1); by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [JN_stable]))); -by (rewrite_goals_tac [st_set_def]); +by (rewtac st_set_def); by (REPEAT(Blast_tac 1)); qed "FP_JN"; @@ -365,7 +365,7 @@ \ (EX i:I. programify(F(i)) : transient(A))"; by (auto_tac (claset(), simpset() addsimps [transient_def, JOIN_def])); -by (rewrite_goals_tac [st_set_def]); +by (rewtac st_set_def); by (dres_inst_tac [("x", "xb")] bspec 2); by (auto_tac (claset() addDs [Acts_type RS subsetD], simpset())); qed "JN_transient"; @@ -566,7 +566,7 @@ by (auto_tac (claset(), simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS iff_sym])); -by (rewrite_goals_tac [safety_prop_def]); +by (rewtac safety_prop_def); by Auto_tac; qed "safety_prop_AllowedActs_iff_Allowed"; @@ -579,7 +579,7 @@ simpset() addsimps [safety_prop_def]) 2)); by (asm_full_simp_tac (simpset() delsimps UN_simps addsimps [Allowed_def, safety_prop_Acts_iff]) 1); -by (rewrite_goals_tac [safety_prop_def]); +by (rewtac safety_prop_def); by Auto_tac; qed "Allowed_eq"; @@ -628,7 +628,7 @@ by Safe_tac; by (full_simp_tac (simpset() addsimps [Inter_iff]) 1); by (Clarify_tac 1); -by (forward_tac [major] 1); +by (ftac major 1); by (dres_inst_tac [("i", "xa")] major 2); by (forw_inst_tac [("i", "xa")] major 4); by (ALLGOALS(Asm_full_simp_tac)); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/UNITY/WFair.ML --- a/src/ZF/UNITY/WFair.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/UNITY/WFair.ML Wed Dec 12 20:37:31 2001 +0100 @@ -243,19 +243,19 @@ qed "leadsTo_weaken_R"; Goal "[| F:A leadsTo A'; B<=A |] ==> F : B leadsTo A'"; -by (forward_tac [leadsToD2] 1); +by (ftac leadsToD2 1); by (blast_tac (claset() addIs [leadsTo_Trans,subset_imp_leadsTo, st_set_subset]) 1); qed_spec_mp "leadsTo_weaken_L"; Goal "[| F:A leadsTo A'; B<=A; A'<=B'; st_set(B')|]==> F:B leadsTo B'"; -by (forward_tac [leadsToD2] 1); +by (ftac leadsToD2 1); by (blast_tac (claset() addIs [leadsTo_weaken_R, leadsTo_weaken_L, leadsTo_Trans, leadsTo_refl]) 1); qed "leadsTo_weaken"; (* This rule has a nicer conclusion *) Goal "[| F:transient(A); state-A<=B; st_set(B)|] ==> F:A leadsTo B"; -by (forward_tac [transientD2] 1); +by (ftac transientD2 1); by (rtac leadsTo_weaken_R 1); by (auto_tac (claset(), simpset() addsimps [transient_imp_leadsTo])); qed "transient_imp_leadsTo2"; @@ -359,7 +359,7 @@ by (auto_tac (claset() addIs [trans_prem,union_prem], simpset())); by (rewrite_goal_tac [ensures_def] 1); by (Clarify_tac 1); -by (forward_tac [constrainsD2] 1); +by (ftac constrainsD2 1); by (dres_inst_tac [("B'", "(A-B) Un B")] constrains_weaken_R 1); by (Blast_tac 1); by (forward_tac [ensuresI2 RS leadsTo_Basis] 1); @@ -563,7 +563,7 @@ qed "wlt_type"; Goalw [st_set_def] "st_set(wlt(F, B))"; -by (resolve_tac [wlt_type] 1); +by (rtac wlt_type 1); qed "wlt_st_set"; AddIffs [wlt_st_set]; @@ -575,7 +575,7 @@ bind_thm("wlt_leadsTo", conjI RS (wlt_leadsTo_iff RS iffD2)); Goalw [wlt_def] "F : A leadsTo B ==> A <= wlt(F, B)"; -by (forward_tac [leadsToD2] 1); +by (ftac leadsToD2 1); by (auto_tac (claset(), simpset() addsimps [st_set_def])); qed "leadsTo_subset"; @@ -608,7 +608,7 @@ (* slightly different from the HOL one: B here is bounded *) Goal "F : A leadsTo A' \ \ ==> EX B:Pow(state). A<=B & F:B leadsTo A' & F : (B-A') co (B Un A')"; -by (forward_tac [leadsToD2] 1); +by (ftac leadsToD2 1); by (etac leadsTo_induct 1); (*Basis*) by (blast_tac (claset() addDs [ensuresD, constrainsD2, st_setD]) 1); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/ex/Commutation.ML --- a/src/ZF/ex/Commutation.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/ex/Commutation.ML Wed Dec 12 20:37:31 2001 +0100 @@ -28,7 +28,7 @@ (* A special case of square_rtrancl_on *) Goalw [diamond_def, commute_def, strip_def] "diamond(r) ==> strip(r)"; -by (resolve_tac [square_rtrancl] 1); +by (rtac square_rtrancl 1); by (ALLGOALS(Asm_simp_tac)); qed "diamond_strip"; @@ -116,7 +116,7 @@ Goalw [confluent_def, Church_Rosser_def, square_def,commute_def,diamond_def] "confluent(r) ==> Church_Rosser(r)"; by Auto_tac; -by (forward_tac [fieldI1] 1); +by (ftac fieldI1 1); by (full_simp_tac (simpset() addsimps [rtrancl_field]) 1); by (etac rtrancl_induct 1); by (ALLGOALS(Clarify_tac)); diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/ex/Limit.ML --- a/src/ZF/ex/Limit.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/ex/Limit.ML Wed Dec 12 20:37:31 2001 +0100 @@ -2317,7 +2317,7 @@ val prems = Goalw [mediating_def] "[|emb(E,G,t); !!n. n \\ nat ==> f(n) = t O r(n) |]==>mediating(E,G,r,f,t)"; -by (Safe_tac); +by Safe_tac; by (REPEAT (ares_tac prems 1)); qed "mediatingI"; diff -r 0a01efff43e9 -r 7ad150f5fc10 src/ZF/simpdata.ML --- a/src/ZF/simpdata.ML Wed Dec 12 19:22:21 2001 +0100 +++ b/src/ZF/simpdata.ML Wed Dec 12 20:37:31 2001 +0100 @@ -199,7 +199,7 @@ qed "bex_one_point1"; Goal "(EX x:A. a=x & P(x)) <-> (a:A & P(a))"; -by(Blast_tac 1); +by (Blast_tac 1); qed "bex_one_point2"; Goal "(ALL x:A. x=a --> P(x)) <-> (a:A --> P(a))"; @@ -219,7 +219,7 @@ val ex_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ("EX x:A. P(x) & Q(x)",FOLogic.oT) -val prove_bex_tac = rewrite_goals_tac [Bex_def] THEN +val prove_bex_tac = rewtac Bex_def THEN Quantifier1.prove_one_point_ex_tac; val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; @@ -227,7 +227,7 @@ val all_pattern = Thm.read_cterm (Theory.sign_of (the_context ())) ("ALL x:A. P(x) --> Q(x)",FOLogic.oT) -val prove_ball_tac = rewrite_goals_tac [Ball_def] THEN +val prove_ball_tac = rewtac Ball_def THEN Quantifier1.prove_one_point_all_tac; val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;