--- a/src/CCL/CCL.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/CCL/CCL.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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}))
*}
--- a/src/CCL/Wfd.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/CCL/Wfd.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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))
--- a/src/CTT/CTT.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/CTT/CTT.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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. **)
--- a/src/Doc/Implementation/Tactic.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy Fri Mar 20 14:48:04 2015 +0100
@@ -394,39 +394,39 @@
text %mlref \<open>
\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 \<phi> i"} adds the proposition
+ \item @{ML Rule_Insts.subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
@{text "\<phi>"} 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 \<phi> i"} deletes the specified
+ \item @{ML Rule_Insts.thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
premise from subgoal @{text i}. Note that @{text \<phi>} 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}
\<close>
--- a/src/Doc/Isar_Ref/Generic.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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
--- a/src/Doc/Isar_Ref/ML_Tactic.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Doc/Isar_Ref/ML_Tactic.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
- @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
+ @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
@{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
@{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
@{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
- @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
+ @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
@{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
\end{tabular}
\medskip
--- a/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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])),
--- a/src/FOL/FOL.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/FOL/FOL.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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 = {*
--- a/src/HOL/Auth/Message.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/Auth/Message.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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])),
--- a/src/HOL/Bali/WellType.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/Bali/WellType.thy Fri Mar 20 14:48:04 2015 +0100
@@ -660,10 +660,10 @@
(* 17 subgoals *)
apply (tactic {* ALLGOALS (fn i =>
if i = 11 then EVERY'
- [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
- thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
- thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
- else thin_tac @{context} "All ?P" i) *})
+ [Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
+ Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
+ Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?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)
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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;
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 14:48:04 2015 +0100
@@ -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)
--- a/src/HOL/IMPP/Hoare.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/IMPP/Hoare.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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 *)
--- a/src/HOL/NanoJava/Equivalence.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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
--- a/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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])),
--- a/src/HOL/TLA/TLA.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/TLA/TLA.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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)) *}
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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
@@ -1555,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})
@@ -1735,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
--- a/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 14:48:04 2015 +0100
@@ -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,
--- a/src/LCF/LCF.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/LCF/LCF.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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)
*}
--- a/src/Pure/Tools/rule_insts.ML Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 14:48:04 2015 +0100
@@ -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,18 +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 make_elim_preserve: Proof.context -> thm -> thm
val method:
(Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) ->
@@ -346,6 +341,3 @@
"remove premise (dynamic instantiation)");
end;
-
-structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
-open Basic_Rule_Insts;
--- a/src/Sequents/LK0.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Sequents/LK0.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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)
*}
--- a/src/Tools/induct_tacs.ML Fri Mar 20 11:53:22 2015 +0100
+++ b/src/Tools/induct_tacs.ML Fri Mar 20 14:48:04 2015 +0100
@@ -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;
--- a/src/ZF/Tools/induct_tacs.ML Fri Mar 20 11:53:22 2015 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 20 14:48:04 2015 +0100
@@ -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*)
--- a/src/ZF/UNITY/SubstAx.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Fri Mar 20 14:48:04 2015 +0100
@@ -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 *)