# HG changeset patch # User paulson # Date 1426868300 0 # Node ID 9c99e5f9fb5e7050d0c22322ea33f40292fd4530 # Parent 26d1c71784f12075a66a913f529768d4eed3acb8# Parent 4ebf2276f58aab757ec22dc1aea57e62070ae7d9 Merge diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/CCL/CCL.thy --- a/src/CCL/CCL.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/CCL/CCL.thy Fri Mar 20 16:18:20 2015 +0000 @@ -475,7 +475,8 @@ method_setup eq_coinduct3 = {* Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => - SIMPLE_METHOD' (res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) + SIMPLE_METHOD' + (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3})) *} diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/CCL/Wfd.thy Fri Mar 20 16:18:20 2015 +0000 @@ -49,7 +49,7 @@ method_setup wfd_strengthen = {* Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt => SIMPLE_METHOD' (fn i => - res_inst_tac ctxt [((("Q", 0), Position.none), s)] @{thm wfd_strengthen_lemma} i + Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] @{thm wfd_strengthen_lemma} i THEN assume_tac ctxt (i + 1))) *} @@ -448,7 +448,7 @@ in fun rcall_tac ctxt i = - let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i + let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps rl i THEN atac i in IHinst tac @{thms rcallTs} i end THEN eresolve_tac ctxt @{thms rcall_lemmas} i @@ -468,7 +468,7 @@ (*** Clean up Correctness Condictions ***) fun clean_ccs_tac ctxt = - let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in + let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps rl i THEN atac i in TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' hyp_subst_tac ctxt)) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/CTT/CTT.thy --- a/src/CTT/CTT.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/CTT/CTT.thy Fri Mar 20 16:18:20 2015 +0000 @@ -421,13 +421,16 @@ The (rtac EqE i) lets them apply to equality judgements. **) fun NE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i + TRY (rtac @{thm EqE} i) THEN + Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i fun SumE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i + TRY (rtac @{thm EqE} i) THEN + Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i fun PlusE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i + TRY (rtac @{thm EqE} i) THEN + Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Doc/Implementation/Tactic.thy Fri Mar 20 16:18:20 2015 +0000 @@ -394,39 +394,39 @@ text %mlref \ \begin{mldecls} - @{index_ML res_inst_tac: "Proof.context -> + @{index_ML Rule_Insts.res_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ - @{index_ML eres_inst_tac: "Proof.context -> + @{index_ML Rule_Insts.eres_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ - @{index_ML dres_inst_tac: "Proof.context -> + @{index_ML Rule_Insts.dres_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ - @{index_ML forw_inst_tac: "Proof.context -> + @{index_ML Rule_Insts.forw_inst_tac: "Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ - @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ - @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\ + @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ + @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> int -> tactic"} \\ @{index_ML rename_tac: "string list -> int -> tactic"} \\ \end{mldecls} \begin{description} - \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the + \item @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the rule @{text thm} with the instantiations @{text insts}, as described above, and then performs resolution on subgoal @{text i}. - \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs - elim-resolution. + \item @{ML Rule_Insts.eres_inst_tac} is like @{ML Rule_Insts.res_inst_tac}, + but performs elim-resolution. - \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs - destruct-resolution. + \item @{ML Rule_Insts.dres_inst_tac} is like @{ML Rule_Insts.res_inst_tac}, + but performs destruct-resolution. - \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that - the selected assumption is not deleted. + \item @{ML Rule_Insts.forw_inst_tac} is like @{ML Rule_Insts.dres_inst_tac} + except that the selected assumption is not deleted. - \item @{ML subgoal_tac}~@{text "ctxt \ i"} adds the proposition + \item @{ML Rule_Insts.subgoal_tac}~@{text "ctxt \ i"} adds the proposition @{text "\"} as local premise to subgoal @{text "i"}, and poses the same as a new subgoal @{text "i + 1"} (in the original context). - \item @{ML thin_tac}~@{text "ctxt \ i"} deletes the specified + \item @{ML Rule_Insts.thin_tac}~@{text "ctxt \ i"} deletes the specified premise from subgoal @{text i}. Note that @{text \} may contain schematic variables, to abbreviate the intended proposition; the first matching subgoal premise will be deleted. Removing useless @@ -476,9 +476,9 @@ facts resulting from goals, and rarely needs to be invoked manually. Flex-flex constraints arise from difficult cases of higher-order - unification. To prevent this, use @{ML res_inst_tac} to instantiate - some variables in a rule. Normally flex-flex constraints can be - ignored; they often disappear as unknowns get instantiated. + unification. To prevent this, use @{ML Rule_Insts.res_inst_tac} to + instantiate some variables in a rule. Normally flex-flex constraints + can be ignored; they often disappear as unknowns get instantiated. \end{description} \ diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Doc/Isar_Ref/Generic.thy --- a/src/Doc/Isar_Ref/Generic.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Doc/Isar_Ref/Generic.thy Fri Mar 20 16:18:20 2015 +0000 @@ -319,7 +319,7 @@ \item @{method rule_tac} etc. do resolution of rules with explicit instantiation. This works the same way as the ML tactics @{ML - res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}). + Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}). 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 diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Doc/Isar_Ref/ML_Tactic.thy --- a/src/Doc/Isar_Ref/ML_Tactic.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Doc/Isar_Ref/ML_Tactic.thy Fri Mar 20 16:18:20 2015 +0000 @@ -39,7 +39,7 @@ @{ML forward_tac}). \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\ - @{ML res_inst_tac}). + @{ML Rule_Insts.res_inst_tac}). \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac} vs.\ @{ML rtac}). @@ -63,11 +63,11 @@ \begin{tabular}{lll} @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\ @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \] 1"} & & @{text "rule a\<^sub>1 \"} \\ - @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a 1"} & & + @{ML Rule_Insts.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 "ctxt [a\<^sub>1, \] i"} & & @{text "rule_tac [i] a\<^sub>1 \"} \\ - @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \] a i"} & & + @{ML Rule_Insts.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 26d1c71784f1 -r 9c99e5f9fb5e src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 16:18:20 2015 +0000 @@ -856,7 +856,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), + (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/FOL/FOL.thy --- a/src/FOL/FOL.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/FOL/FOL.thy Fri Mar 20 16:18:20 2015 +0000 @@ -67,7 +67,7 @@ ML {* fun case_tac ctxt a = - res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split} + Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split} *} method_setup case_tac = {* diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/Auth/Message.thy Fri Mar 20 16:18:20 2015 +0000 @@ -866,7 +866,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), + (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/Bali/AxExample.thy Fri Mar 20 16:18:20 2015 +0000 @@ -43,13 +43,13 @@ ML {* fun inst1_tac ctxt s t xs st = (case AList.lookup (op =) (rev (Term.add_var_names (Thm.prop_of st) [])) s of - SOME i => Rule_Insts.instantiate_tac ctxt [(((s, i), Position.none), t)] xs st + SOME i => PRIMITIVE (Rule_Insts.read_instantiate ctxt [(((s, i), Position.none), t)] xs) st | NONE => Seq.empty); fun ax_tac ctxt = REPEAT o rtac allI THEN' - resolve_tac ctxt (@{thm ax_Skip} :: @{thm ax_StatRef} :: @{thm ax_MethdN} :: @{thm ax_Alloc} :: - @{thm ax_Alloc_Arr} :: @{thm ax_SXAlloc_Normal} :: @{thms ax_derivs.intros(8-)}); + resolve_tac ctxt + @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)}; *} diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/Bali/WellType.thy --- a/src/HOL/Bali/WellType.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/Bali/WellType.thy Fri Mar 20 16:18:20 2015 +0000 @@ -660,10 +660,10 @@ (* 17 subgoals *) apply (tactic {* ALLGOALS (fn 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) *}) + [Rule_Insts.thin_tac @{context} "?E,dt\e0\-PrimT Boolean", + Rule_Insts.thin_tac @{context} "?E,dt\e1\-?T1", + Rule_Insts.thin_tac @{context} "?E,dt\e2\-?T2"] i + else Rule_Insts.thin_tac @{context} "All ?P" i) *}) (*apply (safe del: disjE elim!: wt_elim_cases)*) apply (tactic {*ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})*}) apply (simp_all (no_asm_use) split del: split_if_asm) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 16:18:20 2015 +0000 @@ -1081,7 +1081,7 @@ ML {* fun Seq_case_tac ctxt s i = - res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i + Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2); (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) @@ -1093,7 +1093,7 @@ (* rws are definitions to be unfolded for admissibility check *) fun Seq_induct_tac ctxt s rws i = - res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i + Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1)))) THEN simp_tac (ctxt addsimps rws) i; @@ -1102,12 +1102,12 @@ THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i))); fun pair_tac ctxt s = - res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE} + Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE} THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt; (* induction on a sequence of pairs with pairsplitting and simplification *) fun pair_induct_tac ctxt s rws i = - res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i + Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i THEN pair_tac ctxt "a" (i+3) THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1)))) THEN simp_tac (ctxt addsimps rws) i; diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 16:18:20 2015 +0000 @@ -135,7 +135,7 @@ val take_ss = simpset_of (put_simpset HOL_ss @{context} addsimps (@{thm Rep_cfun_strict1} :: take_rews)) fun quant_tac ctxt i = EVERY - (map (fn name => res_inst_tac ctxt [((("x", 0), Position.none), name)] spec i) x_names) + (map (fn name => Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), name)] spec i) x_names) (* FIXME: move this message to domain_take_proofs.ML *) val is_finite = #is_finite take_info @@ -182,7 +182,7 @@ asm_simp_tac (put_simpset take_ss ctxt) 1 THEN (resolve_tac ctxt prems' THEN_ALL_NEW etac spec) 1 fun cases_tacs (cons, exhaust) = - res_inst_tac ctxt [((("y", 0), Position.none), "x")] exhaust 1 :: + Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] exhaust 1 :: asm_simp_tac (put_simpset take_ss ctxt addsimps prems) 1 :: map con_tac cons val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/IMPP/Hoare.thy Fri Mar 20 16:18:20 2015 +0000 @@ -286,7 +286,7 @@ apply (blast) (* cut *) apply (blast) (* weaken *) apply (tactic {* ALLGOALS (EVERY' - [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y", + [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y", simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) apply (simp_all (no_asm_use) add: triple_valid_def2) apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/NanoJava/Equivalence.thy --- a/src/HOL/NanoJava/Equivalence.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/NanoJava/Equivalence.thy Fri Mar 20 16:18:20 2015 +0000 @@ -105,8 +105,8 @@ apply (rule hoare_ehoare.induct) (*18*) apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *}) -apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *}) -apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *}) +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y") *}) +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y") *}) apply (simp_all only: cnvalid1_eq cenvalid_def2) apply fast apply fast diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/SET_Protocol/Message_SET.thy --- a/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 16:18:20 2015 +0000 @@ -871,7 +871,7 @@ (EVERY [ (*push in occurrences of X...*) (REPEAT o CHANGED) - (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), + (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1), (*...allowing further simplifications*) simp_tac ctxt 1, REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])), diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/TLA/TLA.thy Fri Mar 20 16:18:20 2015 +0000 @@ -300,15 +300,15 @@ fun merge_temp_box_tac ctxt i = REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, - eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i]) + Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i]) fun merge_stp_box_tac ctxt i = REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, - eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i]) + Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i]) fun merge_act_box_tac ctxt i = REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, - eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i]) + Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i]) *} method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 16:18:20 2015 +0000 @@ -185,7 +185,7 @@ else let fun instantiate param = - (map (eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms + (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms |> FIRST') val attempts = map instantiate parameters in @@ -221,7 +221,7 @@ else let fun instantiates param = - eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm + Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm val quantified_var = head_quantified_variable ctxt i st in @@ -673,7 +673,7 @@ else let fun instantiate const_name = - dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] + Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)] @{thm leo2_skolemise} val attempts = map instantiate candidate_consts in @@ -944,16 +944,15 @@ end fun instantiate_tac from to = - Thm.instantiate ([], [(from, to)]) - |> PRIMITIVE + PRIMITIVE (Thm.instantiate ([], [(from, to)])) - val tectic = + val tactic = if is_none var_opt then no_tac else fold (curry (op APPEND)) (map (instantiate_tac (the var_opt)) skolem_cts) no_tac in - tectic st + tactic st end *} @@ -1556,8 +1555,8 @@ ["% _ . True", "% _ . False", "% x . x", "Not"] val tecs = - map (fn t_s => - eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE} + map (fn t_s => (* FIXME proper context!? *) + Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE} THEN' atac) in (TRY o etac @{thm forall_pos_lift}) @@ -1736,7 +1735,7 @@ member (op =) (Term.add_frees hyp_body []) (hd hyp_prefix) then no_tac st else - eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] + Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")] @{thm allE} i st end end diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 16:11:28 2015 +0000 +++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 16:18:20 2015 +0000 @@ -43,9 +43,9 @@ @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2, - res_inst_tac ctxt + Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm totalize_transientI} 2 - ORELSE res_inst_tac ctxt + ORELSE Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ctxt addsimps @{thms Domain_unfold}) 3, diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/LCF/LCF.thy --- a/src/LCF/LCF.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/LCF/LCF.thy Fri Mar 20 16:18:20 2015 +0000 @@ -321,7 +321,7 @@ method_setup induct = {* Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt => SIMPLE_METHOD' (fn i => - res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN + Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN REPEAT (resolve_tac ctxt @{thms adm_lemmas} i))) *} @@ -380,7 +380,7 @@ ML {* fun induct2_tac ctxt (f, g) i = - res_inst_tac ctxt + Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN REPEAT(resolve_tac ctxt @{thms adm_lemmas} i) *} diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 16:18:20 2015 +0000 @@ -4,8 +4,15 @@ Rule instantiations -- operations within implicit rule / subgoal context. *) -signature BASIC_RULE_INSTS = +signature RULE_INSTS = sig + val where_rule: Proof.context -> + ((indexname * Position.T) * string) list -> + (binding * string option * mixfix) list -> thm -> thm + val of_rule: Proof.context -> string option list * string option list -> + (binding * string option * mixfix) list -> thm -> thm + val read_instantiate: Proof.context -> + ((indexname * Position.T) * string) list -> string list -> thm -> thm val res_inst_tac: Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic val eres_inst_tac: Proof.context -> @@ -18,20 +25,6 @@ ((indexname * Position.T) * string) list -> thm -> int -> tactic val thin_tac: Proof.context -> string -> int -> tactic val subgoal_tac: Proof.context -> string -> int -> tactic -end; - -signature RULE_INSTS = -sig - include BASIC_RULE_INSTS - val where_rule: Proof.context -> - ((indexname * Position.T) * string) list -> - (binding * string option * mixfix) list -> thm -> thm - val of_rule: Proof.context -> string option list * string option list -> - (binding * string option * mixfix) list -> thm -> thm - val read_instantiate: Proof.context -> - ((indexname * Position.T) * string) list -> string list -> thm -> thm - val instantiate_tac: Proof.context -> - ((indexname * Position.T) * string) list -> string list -> tactic val make_elim_preserve: Proof.context -> thm -> thm val method: (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) -> @@ -48,8 +41,6 @@ fun error_var msg (xi, pos) = error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); -local - fun the_sort tvars (xi, pos) : sort = (case AList.lookup (op =) tvars xi of SOME S => S @@ -60,6 +51,8 @@ SOME T => T | NONE => error_var "No such variable in theorem: " (xi, pos)); +local + fun instantiate inst = Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #> Envir.beta_norm; @@ -78,6 +71,15 @@ in +fun readT ctxt tvars ((xi, pos), s) = + let + val S = the_sort tvars (xi, pos); + val T = Syntax.read_typ ctxt s; + in + if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T) + else error_var "Incompatible sort for typ instantiation of " (xi, pos) + end; + fun read_termTs ctxt ss Ts = let fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; @@ -88,27 +90,17 @@ |> Variable.polymorphic ctxt; val Ts' = map Term.fastype_of ts'; val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty; - in (ts', map (apsnd snd) (Vartab.dest tyenv)) end; + val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; + in (ts', tyenv') end; -fun read_insts ctxt mixed_insts (tvars, vars) = +fun read_insts ctxt (tvars, vars) mixed_insts = let - val thy = Proof_Context.theory_of ctxt; - val (type_insts, term_insts) = partition_insts mixed_insts; (* type instantiations *) - fun readT ((xi, pos), s) = - let - val S = the_sort tvars (xi, pos); - val T = Syntax.read_typ ctxt s; - in - if Sign.of_sort thy (T, S) then ((xi, S), T) - else error_var "Incompatible sort for typ instantiation of " (xi, pos) - end; - - val instT1 = Term_Subst.instantiateT (map readT type_insts); + val instT1 = Term_Subst.instantiateT (map (readT ctxt tvars) type_insts); val vars1 = map (apsnd instT1) vars; @@ -118,7 +110,7 @@ val Ts = map (the_type vars1) xs; val (ts, inferred) = read_termTs ctxt ss Ts; - val instT2 = Term.typ_subst_TVars inferred; + val instT2 = Term_Subst.instantiateT inferred; val vars2 = map (apsnd instT2) vars1; val inst2 = instantiate (map #1 xs ~~ ts); @@ -139,7 +131,7 @@ |> Variable.declare_thm thm; val tvars = Thm.fold_terms Term.add_tvars thm []; val vars = Thm.fold_terms Term.add_vars thm []; - val insts = read_insts ctxt' mixed_insts (tvars, vars); + val insts = read_insts ctxt' (tvars, vars) mixed_insts; in Drule.instantiate_normalize insts thm |> singleton (Proof_Context.export ctxt' ctxt) @@ -159,15 +151,9 @@ end; - -(* instantiation of rule or goal state *) - fun read_instantiate ctxt insts xs = where_rule ctxt insts (map (fn x => (Binding.name x, NONE, NoSyn)) xs); -fun instantiate_tac ctxt insts fixes = - PRIMITIVE (read_instantiate ctxt insts fixes); - (** attributes **) @@ -212,11 +198,12 @@ fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) => let - val thy = Proof_Context.theory_of ctxt; + val (Tinsts, tinsts) = partition_insts mixed_insts; + - val (Tinsts, tinsts) = partition_insts mixed_insts; + (* goal context *) + val goal = Thm.term_of cgoal; - val params = Logic.strip_params goal (*as they are printed: bound variables with the same name are renamed*) @@ -228,37 +215,18 @@ |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); - (* process type insts: Tinsts_env *) + (* preprocess rule *) - val (rtypes, rsorts) = Drule.types_sorts thm; - fun readT ((xi, pos), s) = - let - val S = - (case rsorts xi of - SOME S => S - | NONE => error_var "No such type variable in theorem: " (xi, pos)); - val T = Syntax.read_typ ctxt' s; - val U = TVar (xi, S); - in - if Sign.typ_instance thy (T, U) then (U, T) - else error_var "Cannot instantiate: " (xi, pos) - end; - val Tinsts_env = map readT Tinsts; + val tvars = Thm.fold_terms Term.add_tvars thm []; + val vars = Thm.fold_terms Term.add_vars thm []; - - (* preprocess rule: extract vars and their types, apply Tinsts *) - - fun get_typ (xi, pos) = - (case rtypes xi of - SOME T => typ_subst_atomic Tinsts_env T - | NONE => error_var "No such variable in theorem: " (xi, pos) xi); + val Tinsts_env = map (readT ctxt' tvars) Tinsts; val (xis, ss) = split_list tinsts; - val Ts = map get_typ xis; + val Ts = map (Term_Subst.instantiateT Tinsts_env o the_type vars) xis; val (ts, envT) = read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts; - val envT' = - map (fn (xi, T) => (TVar (xi, the (rsorts xi)), T)) envT @ Tinsts_env; + val envT' = map (fn (v, T) => (TVar v, T)) (envT @ Tinsts_env); val cenv = map (fn ((xi, _), t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) (distinct @@ -373,6 +341,3 @@ "remove premise (dynamic instantiation)"); end; - -structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts; -open Basic_Rule_Insts; diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Pure/drule.ML --- a/src/Pure/drule.ML Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Pure/drule.ML Fri Mar 20 16:18:20 2015 +0000 @@ -58,7 +58,6 @@ val strip_comb: cterm -> cterm * cterm list val strip_type: ctyp -> ctyp list * ctyp val beta_conv: cterm -> cterm -> cterm - val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) val flexflex_unique: Proof.context option -> thm -> thm val export_without_context: thm -> thm val export_without_context_open: thm -> thm @@ -172,27 +171,6 @@ -(*** Find the type (sort) associated with a (T)Var or (T)Free in a term - Used for establishing default types (of variables) and sorts (of - type variables) when reading another term. - Index -1 indicates that a (T)Free rather than a (T)Var is wanted. -***) - -fun types_sorts thm = - let - val vars = Thm.fold_terms Term.add_vars thm []; - val frees = Thm.fold_terms Term.add_frees thm []; - val tvars = Thm.fold_terms Term.add_tvars thm []; - val tfrees = Thm.fold_terms Term.add_tfrees thm []; - fun types (a, i) = - if i < 0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a, i); - fun sorts (a, i) = - if i < 0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a, i); - in (types, sorts) end; - - - - (** Standardization of rules **) (*Generalization over a list of variables*) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Sequents/LK0.thy Fri Mar 20 16:18:20 2015 +0000 @@ -153,11 +153,13 @@ ML {* (*Cut and thin, replacing the right-side formula*) fun cutR_tac ctxt s i = - res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN rtac @{thm thinR} i + Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN + rtac @{thm thinR} i (*Cut and thin, replacing the left-side formula*) fun cutL_tac ctxt s i = - res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1) + Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN + rtac @{thm thinL} (i + 1) *} diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/Tools/induct_tacs.ML --- a/src/Tools/induct_tacs.ML Fri Mar 20 16:11:28 2015 +0000 +++ b/src/Tools/induct_tacs.ML Fri Mar 20 16:18:20 2015 +0000 @@ -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 res_inst_tac ctxt [((xi, Position.none), s)] rule i st end + in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] rule i st end handle THM _ => Seq.empty; fun case_tac ctxt s = gen_case_tac ctxt s NONE; @@ -104,7 +104,7 @@ val concls = Logic.dest_conjunctions (Thm.concl_of rule); val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths => error "Induction rule has different numbers of variables"; - in res_inst_tac ctxt insts rule' i st end + in Rule_Insts.res_inst_tac ctxt insts rule' i st end handle THM _ => Seq.empty; end; diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Fri Mar 20 16:11:28 2015 +0000 +++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 20 16:18:20 2015 +0000 @@ -101,7 +101,7 @@ [] => error "induction is not available for this datatype" | major::_ => FOLogic.dest_Trueprop major) in - eres_inst_tac ctxt [((ixn, Position.none), var)] rule i + Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] rule i end handle Find_tname msg => if exh then (*try boolean case analysis instead*) diff -r 26d1c71784f1 -r 9c99e5f9fb5e src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Fri Mar 20 16:11:28 2015 +0000 +++ b/src/ZF/UNITY/SubstAx.thy Fri Mar 20 16:18:20 2015 +0000 @@ -359,7 +359,7 @@ @{thm EnsuresI}, @{thm ensuresI}] 1), (*now there are two subgoals: co & transient*) simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2, - res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2, + Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2, (*simplify the command's domain*) simp_tac (ctxt addsimps [@{thm domain_def}]) 3, (* proving the domain part *)