# HG changeset patch # User wenzelm # Date 1213647219 -7200 # Node ID f2f42f9fa09dd6d0be23911077c5dc10ac684bc9 # Parent d2bf12727c8ac6e6ff738b1f8b77af7351b86585 pervasive RuleInsts; diff -r d2bf12727c8a -r f2f42f9fa09d doc-src/IsarRef/Thy/Generic.thy --- a/doc-src/IsarRef/Thy/Generic.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/doc-src/IsarRef/Thy/Generic.thy Mon Jun 16 22:13:39 2008 +0200 @@ -308,7 +308,7 @@ \item [@{method rule_tac} etc.] do resolution of rules with explicit instantiation. This works the same way as the ML tactics @{ML - Tactic.res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}) + res_inst_tac} etc. (see \cite[\S3]{isabelle-ref}) Multiple rules may be only given if there is no instantiation; then @{method rule_tac} is the same as @{ML resolve_tac} in ML (see @@ -323,12 +323,12 @@ \item [@{method thin_tac}~@{text \}] deletes the specified assumption from a subgoal; note that @{text \} may contain schematic - variables. See also @{ML Tactic.thin_tac} in + variables. See also @{ML thin_tac} in \cite[\S3]{isabelle-ref}. \item [@{method subgoal_tac}~@{text \}] adds @{text \} as an - assumption to a subgoal. See also @{ML Tactic.subgoal_tac} and @{ML - Tactic.subgoals_tac} in \cite[\S3]{isabelle-ref}. + assumption to a subgoal. See also @{ML subgoal_tac} and @{ML + subgoals_tac} in \cite[\S3]{isabelle-ref}. \item [@{method rename_tac}~@{text "x\<^sub>1 \ x\<^sub>n"}] renames parameters of a goal according to the list @{text "x\<^sub>1, \, diff -r d2bf12727c8a -r f2f42f9fa09d doc-src/IsarRef/Thy/ML_Tactic.thy --- a/doc-src/IsarRef/Thy/ML_Tactic.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/doc-src/IsarRef/Thy/ML_Tactic.thy Mon Jun 16 22:13:39 2008 +0200 @@ -41,7 +41,7 @@ @{ML forward_tac}). \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ - @{ML RuleInsts.res_inst_tac}). + @{ML res_inst_tac}). \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} vs.\ @{ML rtac}). @@ -66,11 +66,11 @@ \begin{tabular}{lll} @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ @{ML resolve_tac}~@{text "[a\<^sub>1, \] 1"} & & @{text "rule a\<^sub>1 \"} \\ - @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a 1"} & & + @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a 1"} & & @{text "rule_tac x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\[0.5ex] @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\ @{ML resolve_tac}~@{text "[a\<^sub>1, \] i"} & & @{text "rule_tac [i] a\<^sub>1 \"} \\ - @{ML RuleInsts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a i"} & & + @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a i"} & & @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \ \ \ a"} \\ \end{tabular} \medskip diff -r d2bf12727c8a -r f2f42f9fa09d doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Mon Jun 16 22:13:39 2008 +0200 @@ -864,7 +864,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (RuleInsts.res_inst_tac (Simplifier.the_context ss) + (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ss 1, diff -r d2bf12727c8a -r f2f42f9fa09d src/CCL/CCL.thy --- a/src/CCL/CCL.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/CCL/CCL.thy Mon Jun 16 22:13:39 2008 +0200 @@ -415,7 +415,7 @@ ML {* fun po_coinduct_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i + res_inst_tac ctxt [(("R", 0), s)] @{thm po_coinduct} i *} @@ -460,11 +460,8 @@ done ML {* - fun eq_coinduct_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i - - fun eq_coinduct3_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i + fun eq_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct} i + fun eq_coinduct3_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm eq_coinduct3} i *} diff -r d2bf12727c8a -r f2f42f9fa09d src/CCL/Hered.thy --- a/src/CCL/Hered.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/CCL/Hered.thy Mon Jun 16 22:13:39 2008 +0200 @@ -97,8 +97,7 @@ done ML {* - fun HTT_coinduct_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i + fun HTT_coinduct_tac ctxt s i = res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct} i *} lemma HTT_coinduct3: @@ -111,7 +110,7 @@ val HTT_coinduct3_raw = rewrite_rule [@{thm HTTgen_def}] @{thm HTT_coinduct3} fun HTT_coinduct3_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i + res_inst_tac ctxt [(("R", 0), s)] @{thm HTT_coinduct3} i val HTTgenIs = map (mk_genIs @{theory} @{thms data_defs} @{thm HTTgenXH} @{thm HTTgen_mono}) diff -r d2bf12727c8a -r f2f42f9fa09d src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/CCL/Wfd.thy Mon Jun 16 22:13:39 2008 +0200 @@ -55,7 +55,7 @@ ML {* fun wfd_strengthen_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) + res_inst_tac ctxt [(("Q", 0), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac (i+1) *} lemma wf_anti_sym: "[| Wfd(r); :r; :r |] ==> P" @@ -456,7 +456,7 @@ in fun rcall_tac ctxt i = - let fun tac ps rl i = RuleInsts.res_inst_tac ctxt ps rl i THEN atac i + let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i in IHinst tac @{thms rcallTs} i end THEN eresolve_tac @{thms rcall_lemmas} i @@ -478,7 +478,7 @@ hyp_subst_tac) fun clean_ccs_tac ctxt = - let fun tac ps rl i = RuleInsts.eres_inst_tac ctxt ps rl i THEN atac i in + let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' eresolve_tac ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' hyp_subst_tac)) diff -r d2bf12727c8a -r f2f42f9fa09d src/CTT/CTT.thy --- a/src/CTT/CTT.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/CTT/CTT.thy Mon Jun 16 22:13:39 2008 +0200 @@ -417,13 +417,13 @@ The (rtac EqE i) lets them apply to equality judgements. **) fun NE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm NE} i fun SumE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm SumE} i fun PlusE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN RuleInsts.res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i + TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [(("p", 0), sp)] @{thm PlusE} i (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) diff -r d2bf12727c8a -r f2f42f9fa09d src/FOL/FOL.thy --- a/src/FOL/FOL.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/FOL/FOL.thy Mon Jun 16 22:13:39 2008 +0200 @@ -70,8 +70,7 @@ done ML {* - fun case_tac ctxt a = - RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} + fun case_tac ctxt a = res_inst_tac ctxt [(("P", 0), a)] @{thm case_split} *} method_setup case_tac = diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Auth/Message.thy Mon Jun 16 22:13:39 2008 +0200 @@ -884,8 +884,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (RuleInsts.res_inst_tac (Simplifier.the_context ss) - [(("x", 1), "X")] (insert_commute RS ssubst) 1), + (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ss 1, REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Bali/Basis.thy Mon Jun 16 22:13:39 2008 +0200 @@ -230,7 +230,7 @@ ML {* fun sum3_instantiate ctxt thm = map (fn s => simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}]) - (RuleInsts.read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] + (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Bali/WellType.thy Mon Jun 16 22:13:39 2008 +0200 @@ -653,10 +653,11 @@ apply (safe del: disjE) (* 17 subgoals *) apply (tactic {* ALLGOALS (fn i => - if i = 11 then EVERY'[RuleInsts.thin_tac @{context} "?E,dt\e0\-PrimT Boolean", - RuleInsts.thin_tac @{context} "?E,dt\e1\-?T1", - RuleInsts.thin_tac @{context} "?E,dt\e2\-?T2"] i - else RuleInsts.thin_tac @{context} "All ?P" i) *}) + if i = 11 then EVERY' + [thin_tac @{context} "?E,dt\e0\-PrimT Boolean", + thin_tac @{context} "?E,dt\e1\-?T1", + thin_tac @{context} "?E,dt\e2\-?T2"] i + else thin_tac @{context} "All ?P" i) *}) (*apply (safe del: disjE elim!: wt_elim_cases)*) apply (tactic {*ALLGOALS (eresolve_tac @{thms wt_elim_cases})*}) apply (simp_all (no_asm_use) split del: split_if_asm) diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Hyperreal/MacLaurin.thy --- a/src/HOL/Hyperreal/MacLaurin.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Hyperreal/MacLaurin.thy Mon Jun 16 22:13:39 2008 +0200 @@ -50,7 +50,7 @@ fun deriv_tac ctxt = SUBGOAL (fn (prem, i) => resolve_tac @{thms deriv_rulesI} i ORELSE - ((rtac (RuleInsts.read_instantiate ctxt [(("f", 0), get_fun_name prem)] + ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)] @{thm DERIV_chain2}) i) handle DERIV_name => no_tac)); fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i)); diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/IMPP/Hoare.thy Mon Jun 16 22:13:39 2008 +0200 @@ -283,7 +283,7 @@ apply (blast) (* cut *) apply (blast) (* weaken *) apply (tactic {* ALLGOALS (EVERY' - [REPEAT o RuleInsts.thin_tac @{context} "hoare_derivs ?x ?y", + [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y", simp_tac @{simpset}, clarify_tac @{claset}, REPEAT o smp_tac 1]) *}) apply (simp_all (no_asm_use) add: triple_valid_def2) apply (intro strip, tactic "smp_tac 2 1", blast) (* conseq *) diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/NanoJava/Equivalence.thy Mon Jun 16 22:13:39 2008 +0200 @@ -108,8 +108,8 @@ apply (rule hoare_ehoare.induct) (*18*) apply (tactic {* ALLGOALS (REPEAT o dresolve_tac [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *}) -apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "hoare ?x ?y") *}) -apply (tactic {* ALLGOALS (REPEAT o RuleInsts.thin_tac @{context} "ehoare ?x ?y") *}) +apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *}) +apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *}) apply (simp_all only: cnvalid1_eq cenvalid_def2) apply fast apply fast diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Mon Jun 16 22:13:39 2008 +0200 @@ -54,7 +54,7 @@ gen_res_inst_tac_term (K Drule.cterm_instantiate) []; fun cut_inst_tac_term' tinst th = - res_inst_tac_term' tinst false (Tactic.make_elim_preserve th); + res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th); fun get_dyn_thm thy name atom_name = PureThy.get_thm thy name handle ERROR _ => diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Prolog/prolog.ML Mon Jun 16 22:13:39 2008 +0200 @@ -53,7 +53,7 @@ fun atomizeD ctxt thm = let fun at thm = case concl_of thm of _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS - (RuleInsts.read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec)) + (read_instantiate ctxt [(("x", 0), "?" ^ (if s="P" then "PP" else s))] spec)) | _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) | _$(Const("op -->",_)$_$_) => at(thm RS mp) | _ => [thm] diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Real/rat_arith.ML --- a/src/HOL/Real/rat_arith.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Real/rat_arith.ML Mon Jun 16 22:13:39 2008 +0200 @@ -14,7 +14,7 @@ val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, - RuleInsts.read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, + read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, @{thm divide_1}, @{thm divide_zero_left}, @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Mon Jun 16 22:13:39 2008 +0200 @@ -880,7 +880,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (RuleInsts.res_inst_tac (Simplifier.the_context ss) + (res_inst_tac (Simplifier.the_context ss) [(("x", 1), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ss 1, diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/TLA/TLA.thy Mon Jun 16 22:13:39 2008 +0200 @@ -307,15 +307,15 @@ fun merge_temp_box_tac ctxt i = REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, - RuleInsts.eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i]) + eres_inst_tac ctxt [(("'a", 0), "behavior")] @{thm box_thin} i]) fun merge_stp_box_tac ctxt i = REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, - RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i]) + eres_inst_tac ctxt [(("'a", 0), "state")] @{thm box_thin} i]) fun merge_act_box_tac ctxt i = REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, - RuleInsts.eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i]) + eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i]) *} (* rewrite rule to push universal quantification through box: diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/TFL/post.ML Mon Jun 16 22:13:39 2008 +0200 @@ -152,7 +152,7 @@ rule_by_tactic (REPEAT (FIRSTGOAL (resolve_tac [allI, impI, conjI] ORELSE' etac conjE))); (*Strip off the outer !P*) -val spec'= RuleInsts.read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; +val spec'= read_instantiate @{context} [(("x", 0), "P::?'b=>bool")] spec; fun tracing true _ = () | tracing false msg = writeln msg; diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/induct_tacs.ML --- a/src/HOL/Tools/induct_tacs.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/induct_tacs.ML Mon Jun 16 22:13:39 2008 +0200 @@ -44,7 +44,7 @@ (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of Var (xi, _) :: _ => xi | _ => raise THM ("Malformed cases rule", 0, [rule])); - in RuleInsts.res_inst_tac ctxt [(xi, s)] rule i st end + in res_inst_tac ctxt [(xi, s)] rule i st end handle THM _ => Seq.empty; fun case_tac ctxt s = gen_case_tac ctxt (s, NONE); @@ -100,7 +100,7 @@ val concls = HOLogic.dest_concls (Thm.concl_of rule); val insts = maps prep_inst (concls ~~ varss) handle Library.UnequalLengths => error "Induction rule has different numbers of variables"; - in RuleInsts.res_inst_tac ctxt insts rule i st end + in res_inst_tac ctxt insts rule i st end handle THM _ => Seq.empty; end; diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/meson.ML Mon Jun 16 22:13:39 2008 +0200 @@ -646,7 +646,7 @@ (*Rules to convert the head literal into a negated assumption. If the head literal is already negated, then using notEfalse instead of notEfalse' prevents a double negation.*) -val notEfalse = RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE; +val notEfalse = read_instantiate @{context} [(("R", 0), "False")] notE; val notEfalse' = rotate_prems 1 notEfalse; fun negated_asm_of_head th = diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/metis_tools.ML --- a/src/HOL/Tools/metis_tools.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/metis_tools.ML Mon Jun 16 22:13:39 2008 +0200 @@ -24,10 +24,10 @@ (* ------------------------------------------------------------------------- *) (* Useful Theorems *) (* ------------------------------------------------------------------------- *) - val EXCLUDED_MIDDLE = rotate_prems 1 (RuleInsts.read_instantiate @{context} [(("R", 0), "False")] notE); + val EXCLUDED_MIDDLE = rotate_prems 1 (read_instantiate @{context} [(("R", 0), "False")] notE); val REFL_THM = incr_indexes 2 (Meson.make_meta_clause refl); (*Rename from 0,1*) val subst_em = zero_var_indexes (subst RS EXCLUDED_MIDDLE); - val ssubst_em = RuleInsts.read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em); + val ssubst_em = read_instantiate @{context} [(("t", 0), "?s"), (("s", 0), "?t")] (sym RS subst_em); (* ------------------------------------------------------------------------- *) (* Useful Functions *) diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/record_package.ML Mon Jun 16 22:13:39 2008 +0200 @@ -2155,8 +2155,8 @@ fun equality_prf () = prove_standard [] equality_prop (fn {context, ...} => fn st => let val [s, s'] = map #1 (rev (Tactic.innermost_params 1 st)) in - st |> (RuleInsts.res_inst_tac context [((rN, 0), s)] cases_scheme 1 - THEN RuleInsts.res_inst_tac context [((rN, 0), s')] cases_scheme 1 + st |> (res_inst_tac context [((rN, 0), s)] cases_scheme 1 + THEN res_inst_tac context [((rN, 0), s')] cases_scheme 1 THEN (METAHYPS equality_tac 1)) (* simp_all_tac ss (sel_convs) would also work but is less efficient *) end); diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/split_rule.ML Mon Jun 16 22:13:39 2008 +0200 @@ -124,7 +124,7 @@ fun pair_tac ctxt s = - RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} + res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} THEN' hyp_subst_tac THEN' K prune_params_tac; diff -r d2bf12727c8a -r f2f42f9fa09d src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Jun 16 22:13:39 2008 +0200 @@ -41,9 +41,9 @@ @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ss addsimps [@{thm mk_total_program_def}]) 2, - RuleInsts.res_inst_tac (Simplifier.the_context ss) + res_inst_tac (Simplifier.the_context ss) [(("act", 0), sact)] @{thm totalize_transientI} 2 - ORELSE RuleInsts.res_inst_tac (Simplifier.the_context ss) + ORELSE res_inst_tac (Simplifier.the_context ss) [(("act", 0), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ss addsimps [@{thm Domain_def}]) 3, diff -r d2bf12727c8a -r f2f42f9fa09d src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Mon Jun 16 22:13:39 2008 +0200 @@ -1089,7 +1089,7 @@ ML {* fun Seq_case_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i + res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2); (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) @@ -1104,7 +1104,7 @@ (* rws are definitions to be unfolded for admissibility check *) fun Seq_induct_tac ctxt s rws i = let val ss = Simplifier.local_simpset_of ctxt in - RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i + res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1)))) THEN simp_tac (ss addsimps rws) i end; @@ -1114,13 +1114,13 @@ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i))); fun pair_tac ctxt s = - RuleInsts.res_inst_tac ctxt [(("p", 0), s)] PairE + res_inst_tac ctxt [(("p", 0), s)] PairE THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt); (* induction on a sequence of pairs with pairsplitting and simplification *) fun pair_induct_tac ctxt s rws i = let val ss = Simplifier.local_simpset_of ctxt in - RuleInsts.res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i + res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i THEN pair_tac ctxt "a" (i+3) THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1)))) THEN simp_tac (ss addsimps rws) i diff -r d2bf12727c8a -r f2f42f9fa09d src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOLCF/Tools/domain/domain_library.ML Mon Jun 16 22:13:39 2008 +0200 @@ -24,7 +24,7 @@ fun upd_second f (x,y,z) = ( x, f y, z); fun upd_third f (x,y,z) = ( x, y, f z); -fun atomize ctxt thm = let val r_inst = RuleInsts.read_instantiate ctxt; +fun atomize ctxt thm = let val r_inst = read_instantiate ctxt; fun at thm = case concl_of thm of _$(Const("op &",_)$_$_) => at(thm RS conjunct1)@at(thm RS conjunct2) | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [(("x", 0), "?" ^ s)] spec)) diff -r d2bf12727c8a -r f2f42f9fa09d src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Mon Jun 16 22:13:39 2008 +0200 @@ -376,7 +376,7 @@ val goal = lift_defined %: (nonlazy args, concl); fun tacs ctxt = [ rtac @{thm rev_contrapos} 1, - RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1, + eres_inst_tac ctxt [(("f", 0), dis_name con)] cfun_arg_cong 1, asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; in pg [] goal tacs end; in @@ -477,7 +477,7 @@ mk_trp (con_app con1 args1 ~<< con_app con2 args2)); fun tacs ctxt = [ rtac @{thm rev_contrapos} 1, - RuleInsts.eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] + eres_inst_tac ctxt [(("f", 0), dis_name con1)] monofun_cfun_arg 1] @ map (case_UU_tac ctxt (con_stricts @ dis_rews) 1) (nonlazy args2) @ [asm_simp_tac (HOLCF_ss addsimps dis_rews) 1]; in pg [] goal tacs end; @@ -709,7 +709,7 @@ mk_trp (foldr1 mk_conj (mapn concf 1 dnames))); val take_ss = HOL_ss addsimps take_rews; fun quant_tac ctxt i = EVERY - (mapn (fn n => fn _ => RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); + (mapn (fn n => fn _ => res_inst_tac ctxt [(("x", 0), x_name n)] spec i) 1 dnames); fun ind_prems_tac prems = EVERY (maps (fn cons => @@ -766,7 +766,7 @@ map (K (atac 1)) (nonlazy args) @ map (K (etac spec 1)) (List.filter is_rec args); fun cases_tacs (cons, cases) = - RuleInsts.res_inst_tac context [(("x", 0), "x")] cases 1 :: + res_inst_tac context [(("x", 0), "x")] cases 1 :: asm_simp_tac (take_ss addsimps prems) 1 :: maps con_tacs cons; in @@ -783,8 +783,8 @@ val concl = mk_trp (%:(x_name n) === %:(x_name n^"'")); val goal = mk_All ("n", mk_trp (lhs === rhs)) ===> concl; fun tacf {prems, context} = [ - RuleInsts.res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, - RuleInsts.res_inst_tac context [(("t", 0), x_name n^"'")] (ax_reach RS subst) 1, + res_inst_tac context [(("t", 0), x_name n )] (ax_reach RS subst) 1, + res_inst_tac context [(("t", 0), 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)), @@ -833,7 +833,7 @@ val goal = mk_trp (mk_all ("n", foldr1 mk_conj (mapn mk_eqn 1 eqs))); fun arg_tacs ctxt vn = [ - RuleInsts.eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1, + eres_inst_tac ctxt [(("x", 0), vn)] all_dupE 1, etac disjE 1, asm_simp_tac (HOL_ss addsimps con_rews) 1, asm_simp_tac take_ss 1]; @@ -843,7 +843,7 @@ fun foo_tacs ctxt n (cons, cases) = simp_tac take_ss 1 :: rtac allI 1 :: - RuleInsts.res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 :: + res_inst_tac ctxt [(("x", 0), x_name n)] cases 1 :: asm_simp_tac take_ss 1 :: maps (con_tacs ctxt) cons; fun tacs ctxt = @@ -887,8 +887,7 @@ else (* infinite case *) let fun one_finite n dn = - RuleInsts.read_instantiate global_ctxt - [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; + read_instantiate global_ctxt [(("P", 0), dn ^ "_finite " ^ x_name n)] excluded_middle; val finites = mapn one_finite 1 dnames; val goal = @@ -936,7 +935,7 @@ fun x_tacs ctxt n x = [ rotate_tac (n+1) 1, etac all2E 1, - RuleInsts.eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, + eres_inst_tac ctxt [(("P", 1), sproj "R" eqs n^" "^x^" "^x^"'")] (mp RS disjE) 1, TRY (safe_tac HOL_cs), REPEAT (CHANGED (asm_simp_tac take_ss 1))]; fun tacs ctxt = [ diff -r d2bf12727c8a -r f2f42f9fa09d src/LCF/LCF.thy --- a/src/LCF/LCF.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/LCF/LCF.thy Mon Jun 16 22:13:39 2008 +0200 @@ -317,7 +317,7 @@ ML {* fun induct_tac ctxt v i = - RuleInsts.res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN + res_inst_tac ctxt [(("f", 0), v)] @{thm induct} i THEN REPEAT (resolve_tac @{thms adm_lemmas} i) *} @@ -376,7 +376,7 @@ ML {* fun induct2_tac ctxt (f, g) i = - RuleInsts.res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN + res_inst_tac ctxt [(("f", 0), f), (("g", 0), g)] @{thm induct2} i THEN REPEAT(resolve_tac @{thms adm_lemmas} i) *} diff -r d2bf12727c8a -r f2f42f9fa09d src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/Sequents/LK0.thy Mon Jun 16 22:13:39 2008 +0200 @@ -157,11 +157,11 @@ ML {* (*Cut and thin, replacing the right-side formula*) fun cutR_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i + res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i (*Cut and thin, replacing the left-side formula*) fun cutL_tac ctxt s i = - RuleInsts.res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1) + res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1) *} diff -r d2bf12727c8a -r f2f42f9fa09d src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/ZF/Tools/induct_tacs.ML Mon Jun 16 22:13:39 2008 +0200 @@ -102,7 +102,7 @@ [] => error "induction is not available for this datatype" | major::_ => FOLogic.dest_Trueprop major) in - RuleInsts.eres_inst_tac ctxt [(ixn, var)] rule i state + eres_inst_tac ctxt [(ixn, var)] rule i state end handle Find_tname msg => if exh then (*try boolean case analysis instead*) diff -r d2bf12727c8a -r f2f42f9fa09d src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Mon Jun 16 17:56:08 2008 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Mon Jun 16 22:13:39 2008 +0200 @@ -360,7 +360,7 @@ @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ss addsimps (ProgramDefs.get ctxt)) 2, - RuleInsts.res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, + res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ss addsimps [@{thm domain_def}]) 3, (* proving the domain part *) diff -r d2bf12727c8a -r f2f42f9fa09d src/ZF/ind_syntax.ML --- a/src/ZF/ind_syntax.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/ZF/ind_syntax.ML Mon Jun 16 22:13:39 2008 +0200 @@ -51,7 +51,7 @@ (*For deriving cases rules. CollectD2 discards the domain, which is redundant; read_instantiate replaces a propositional variable by a formula variable*) val equals_CollectD = - RuleInsts.read_instantiate @{context} [(("W", 0), "?Q")] + read_instantiate @{context} [(("W", 0), "?Q")] (make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));