--- a/src/CCL/CCL.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/CCL/CCL.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/CCL/Wfd.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/CTT/CTT.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/Doc/Implementation/Tactic.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/Doc/Isar_Ref/Generic.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/Doc/Isar_Ref/ML_Tactic.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/Doc/Tutorial/Protocol/Message.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/FOL/FOL.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/Auth/Message.thy Fri Mar 20 16:18:28 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/AxExample.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/HOL/Bali/AxExample.thy Fri Mar 20 16:18:28 2015 +0100
@@ -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-)};
*}
--- a/src/HOL/Bali/WellType.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/HOL/Bali/WellType.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/IMPP/Hoare.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/NanoJava/Equivalence.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/SET_Protocol/Message_SET.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/TLA/TLA.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 16:18:28 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
@@ -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
--- a/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 14:06:15 2015 +0000
+++ b/src/HOL/UNITY/UNITY_tactics.ML Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/LCF/LCF.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 16:18:28 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,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;
--- a/src/Pure/drule.ML Fri Mar 20 14:06:15 2015 +0000
+++ b/src/Pure/drule.ML Fri Mar 20 16:18:28 2015 +0100
@@ -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*)
--- a/src/Sequents/LK0.thy Fri Mar 20 14:06:15 2015 +0000
+++ b/src/Sequents/LK0.thy Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/Tools/induct_tacs.ML Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 20 16:18:28 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 14:06:15 2015 +0000
+++ b/src/ZF/UNITY/SubstAx.thy Fri Mar 20 16:18:28 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 *)