--- a/src/CCL/CCL.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/CCL/CCL.thy Mon Mar 23 13:30:59 2015 +0100
@@ -476,7 +476,7 @@
method_setup eq_coinduct3 = {*
Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD'
- (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3}))
+ (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
*}
--- a/src/CCL/Wfd.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/CCL/Wfd.thy Mon Mar 23 13:30:59 2015 +0100
@@ -49,7 +49,7 @@
method_setup wfd_strengthen = {*
Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
SIMPLE_METHOD' (fn i =>
- Rule_Insts.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 = Rule_Insts.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 = Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/CTT/CTT.thy Mon Mar 23 13:30:59 2015 +0100
@@ -422,15 +422,15 @@
fun NE_tac ctxt sp i =
TRY (rtac @{thm EqE} i) THEN
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i
+ 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
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i
+ 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
- Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i
+ 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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Doc/Implementation/Tactic.thy Mon Mar 23 13:30:59 2015 +0100
@@ -395,15 +395,21 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML Rule_Insts.res_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
@{index_ML Rule_Insts.eres_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
@{index_ML Rule_Insts.dres_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
@{index_ML Rule_Insts.forw_inst_tac: "Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
- @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
- @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> int -> tactic"} \\
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
+ thm -> int -> tactic"} \\
+ @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string ->
+ (binding * string option * mixfix) list -> int -> tactic"} \\
+ @{index_ML Rule_Insts.thin_tac: "Proof.context -> string ->
+ (binding * string option * mixfix) list -> int -> tactic"} \\
@{index_ML rename_tac: "string list -> int -> tactic"} \\
\end{mldecls}
--- a/src/Doc/Isar_Ref/Generic.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Mar 23 13:30:59 2015 +0100
@@ -300,10 +300,14 @@
@{rail \<open>
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
- @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \<newline>
+ @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
( dynamic_insts @'in' @{syntax thmref} | @{syntax thmrefs} )
;
+ @@{method thin_tac} @{syntax goal_spec}? @{syntax prop}
+ (@'for' (@{syntax vars} + @'and'))?
+ ;
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +)
+ (@'for' (@{syntax vars} + @'and'))?
;
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
;
@@ -313,6 +317,7 @@
;
dynamic_insts: ((@{syntax name} '=' @{syntax term}) + @'and')
+ (@'for' (@{syntax vars} + @'and'))?
\<close>}
\begin{description}
--- a/src/Doc/Tutorial/Protocol/Message.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Doc/Tutorial/Protocol/Message.thy Mon Mar 23 13:30:59 2015 +0100
@@ -856,7 +856,8 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/FOL/FOL.thy Mon Mar 23 13:30:59 2015 +0100
@@ -66,13 +66,13 @@
done
ML {*
- fun case_tac ctxt a =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
+ fun case_tac ctxt a fixes =
+ Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] fixes @{thm case_split}
*}
method_setup case_tac = {*
- Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
- (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
+ Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ (fn (quant, (s, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s fixes))
*} "case_tac emulation (dynamic instantiation!)"
--- a/src/HOL/Auth/Message.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Auth/Message.thy Mon Mar 23 13:30:59 2015 +0100
@@ -866,7 +866,8 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/Bali/WellType.thy Mon Mar 23 13:30:59 2015 +0100
@@ -660,10 +660,10 @@
(* 17 subgoals *)
apply (tactic {* ALLGOALS (fn i =>
if i = 11 then EVERY'
- [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) *})
+ [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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Mon Mar 23 13:30:59 2015 +0100
@@ -1081,7 +1081,7 @@
ML {*
fun Seq_case_tac ctxt s i =
- Rule_Insts.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 =
- Rule_Insts.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 =
- Rule_Insts.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 =
- Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Mon Mar 23 13:30:59 2015 +0100
@@ -135,7 +135,8 @@
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 => Rule_Insts.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 +183,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) =
- Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/IMPP/Hoare.thy Mon Mar 23 13:30:59 2015 +0100
@@ -286,7 +286,7 @@
apply (blast) (* cut *)
apply (blast) (* weaken *)
apply (tactic {* ALLGOALS (EVERY'
- [REPEAT o Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/NanoJava/Equivalence.thy Mon Mar 23 13:30:59 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 Rule_Insts.thin_tac @{context} "hoare ?x ?y") *})
-apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Mon Mar 23 13:30:59 2015 +0100
@@ -871,7 +871,8 @@
(EVERY
[ (*push in occurrences of X...*)
(REPEAT o CHANGED)
- (Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/TLA/TLA.thy Mon Mar 23 13:30:59 2015 +0100
@@ -300,15 +300,15 @@
fun merge_temp_box_tac ctxt i =
REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
- Rule_Insts.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,
- Rule_Insts.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,
- Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Mar 23 13:30:59 2015 +0100
@@ -185,7 +185,7 @@
else
let
fun instantiate param =
- (map (Rule_Insts.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 =
- Rule_Insts.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
@@ -427,7 +427,7 @@
fun instantiate_vars ctxt vars : tactic =
map (fn var =>
Rule_Insts.eres_inst_tac ctxt
- [((("x", 0), Position.none), var)] @{thm allE} 1)
+ [((("x", 0), Position.none), var)] [] @{thm allE} 1)
vars
|> EVERY
@@ -673,7 +673,7 @@
else
let
fun instantiate const_name =
- Rule_Insts.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
@@ -1556,7 +1556,7 @@
val tecs =
map (fn t_s => (* FIXME proper context!? *)
- Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
+ 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
- Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/HOL/UNITY/UNITY_tactics.ML Mon Mar 23 13:30:59 2015 +0100
@@ -44,9 +44,9 @@
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
Rule_Insts.res_inst_tac ctxt
- [((("act", 0), Position.none), sact)] @{thm totalize_transientI} 2
+ [((("act", 0), Position.none), sact)] [] @{thm totalize_transientI} 2
ORELSE Rule_Insts.res_inst_tac ctxt
- [((("act", 0), Position.none), sact)] @{thm transientI} 2,
+ [((("act", 0), Position.none), sact)] [] @{thm transientI} 2,
(*simplify the command's domain*)
simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
constrains_tac ctxt 1,
--- a/src/LCF/LCF.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/LCF/LCF.thy Mon Mar 23 13:30:59 2015 +0100
@@ -321,7 +321,7 @@
method_setup induct = {*
Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
SIMPLE_METHOD' (fn i =>
- Rule_Insts.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)))
*}
@@ -381,7 +381,7 @@
ML {*
fun induct2_tac ctxt (f, g) i =
Rule_Insts.res_inst_tac ctxt
- [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN
+ [((("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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Mon Mar 23 13:30:59 2015 +0100
@@ -14,20 +14,28 @@
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
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val eres_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val cut_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val forw_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
val dres_inst_tac: Proof.context ->
- ((indexname * Position.T) * string) list -> thm -> int -> tactic
- val thin_tac: Proof.context -> string -> int -> tactic
- val subgoal_tac: Proof.context -> string -> int -> tactic
+ ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> thm ->
+ int -> tactic
+ val thin_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
+ val subgoal_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
+ int -> tactic
val make_elim_preserve: Proof.context -> thm -> thm
val method:
- (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) ->
+ (Proof.context -> ((indexname * Position.T) * string) list ->
+ (binding * string option * mixfix) list -> thm -> int -> tactic) ->
(Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
end;
@@ -124,15 +132,15 @@
fun where_rule ctxt mixed_insts fixes thm =
let
val ctxt' = ctxt
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
- |> Variable.declare_thm thm;
+ |> Variable.declare_thm thm
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
val (inst_tvars, inst_vars) = read_insts ctxt' mixed_insts thm;
in
thm
|> Drule.instantiate_normalize
(map (apply2 (Thm.ctyp_of ctxt) o apfst TVar) inst_tvars,
map (apply2 (Thm.cterm_of ctxt) o apfst Var) inst_vars)
- |> singleton (Proof_Context.export ctxt' ctxt)
+ |> singleton (Variable.export ctxt' ctxt)
|> Rule_Cases.save thm
end;
@@ -192,7 +200,7 @@
(* resolution after lifting and instantiation; may refer to parameters of the subgoal *)
-fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) =>
+fun bires_inst_tac bires_flag ctxt mixed_insts fixes thm i st = CSUBGOAL (fn (cgoal, _) =>
let
(* goal parameters *)
@@ -210,9 +218,15 @@
val paramTs = map #2 params;
- (* lift and instantiate rule *)
+ (* local fixes *)
+
+ val fixes_ctxt = param_ctxt
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
- val (inst_tvars, inst_vars) = read_insts param_ctxt mixed_insts thm;
+ val (inst_tvars, inst_vars) = read_insts fixes_ctxt mixed_insts thm;
+
+
+ (* lift and instantiate rule *)
val inc = Thm.maxidx_of st + 1;
fun lift_var ((a, j), T) =
@@ -222,13 +236,14 @@
(Logic.incr_indexes (paramTs, inc) t);
val inst_tvars' = inst_tvars
- |> map (apply2 (Thm.ctyp_of param_ctxt o Logic.incr_tvar inc) o apfst TVar);
+ |> map (apply2 (Thm.ctyp_of fixes_ctxt o Logic.incr_tvar inc) o apfst TVar);
val inst_vars' = inst_vars
- |> map (fn (v, t) => apply2 (Thm.cterm_of param_ctxt) (lift_var v, lift_term t));
+ |> map (fn (v, t) => apply2 (Thm.cterm_of fixes_ctxt) (lift_var v, lift_term t));
val thm' =
Drule.instantiate_normalize (inst_tvars', inst_vars')
- (Thm.lift_rule cgoal thm);
+ (Thm.lift_rule cgoal thm)
+ |> singleton (Variable.export fixes_ctxt param_ctxt);
in
compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
end) i st;
@@ -256,25 +271,27 @@
end;
(*instantiate and cut -- for atomic fact*)
-fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
+fun cut_inst_tac ctxt insts fixes rule =
+ res_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule);
(*forward tactic applies a rule to an assumption without deleting it*)
-fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac ctxt;
+fun forw_inst_tac ctxt insts fixes rule =
+ cut_inst_tac ctxt insts fixes rule THEN' assume_tac ctxt;
(*dresolve tactic applies a rule to replace an assumption*)
-fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
+fun dres_inst_tac ctxt insts fixes rule =
+ eres_inst_tac ctxt insts fixes (make_elim_preserve ctxt rule);
(* derived tactics *)
(*deletion of an assumption*)
-fun thin_tac ctxt s =
- eres_inst_tac ctxt [((("V", 0), Position.none), s)] Drule.thin_rl;
+fun thin_tac ctxt s fixes =
+ eres_inst_tac ctxt [((("V", 0), Position.none), s)] fixes Drule.thin_rl;
(*Introduce the given proposition as lemma and subgoal*)
-fun subgoal_tac ctxt A =
- DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] cut_rl;
-
+fun subgoal_tac ctxt A fixes =
+ DETERM o res_inst_tac ctxt [((("psi", 0), Position.none), A)] fixes cut_rl;
(* method wrapper *)
@@ -282,14 +299,16 @@
fun method inst_tac tac =
Args.goal_spec --
Scan.optional (Scan.lift
- (Parse.and_list1 (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax))
- --| Args.$$$ "in")) [] --
+ (Parse.and_list1
+ (Parse.position Args.var -- (Args.$$$ "=" |-- Parse.!!! Args.name_inner_syntax)) --
+ Parse.for_fixes --| Args.$$$ "in")) ([], []) --
Attrib.thms >>
- (fn ((quant, insts), thms) => fn ctxt => METHOD (fn facts =>
- if null insts then quant (Method.insert_tac facts THEN' tac ctxt thms)
+ (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
+ if null insts andalso null fixes
+ then quant (Method.insert_tac facts THEN' tac ctxt thms)
else
(case thms of
- [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts thm)
+ [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts fixes thm)
| _ => error "Cannot have instantiations with multiple rules")));
@@ -309,13 +328,13 @@
Method.setup @{binding cut_tac} (method cut_inst_tac (K cut_rules_tac))
"cut rule (dynamic instantiation)" #>
Method.setup @{binding subgoal_tac}
- (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax) >>
- (fn (quant, props) => fn ctxt =>
- SIMPLE_METHOD'' quant (EVERY' (map (subgoal_tac ctxt) props))))
+ (Args.goal_spec -- Scan.lift (Scan.repeat1 Args.name_inner_syntax -- Parse.for_fixes) >>
+ (fn (quant, (props, fixes)) => fn ctxt =>
+ SIMPLE_METHOD'' quant (EVERY' (map (fn prop => subgoal_tac ctxt prop fixes) props))))
"insert subgoal (dynamic instantiation)" #>
Method.setup @{binding thin_tac}
- (Args.goal_spec -- Scan.lift Args.name_inner_syntax >>
- (fn (quant, prop) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop)))
- "remove premise (dynamic instantiation)");
+ (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) >>
+ (fn (quant, (prop, fixes)) => fn ctxt => SIMPLE_METHOD'' quant (thin_tac ctxt prop fixes)))
+ "remove premise (dynamic instantiation)");
end;
--- a/src/Sequents/LK0.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Sequents/LK0.thy Mon Mar 23 13:30:59 2015 +0100
@@ -153,12 +153,12 @@
ML {*
(*Cut and thin, replacing the right-side formula*)
fun cutR_tac ctxt s i =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN
+ 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 =
- Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN
+ 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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/Tools/induct_tacs.ML Mon Mar 23 13:30:59 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 Rule_Insts.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 Rule_Insts.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 Mon Mar 23 10:16:20 2015 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Mon Mar 23 13:30:59 2015 +0100
@@ -101,11 +101,11 @@
[] => error "induction is not available for this datatype"
| major::_ => FOLogic.dest_Trueprop major)
in
- Rule_Insts.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*)
- case_tac ctxt var i
+ case_tac ctxt var [] i
else error msg) i state;
val exhaust_tac = exhaust_induct_tac true;
--- a/src/ZF/UNITY/SubstAx.thy Mon Mar 23 10:16:20 2015 +0100
+++ b/src/ZF/UNITY/SubstAx.thy Mon Mar 23 13:30:59 2015 +0100
@@ -359,7 +359,8 @@
@{thm EnsuresI}, @{thm ensuresI}] 1),
(*now there are two subgoals: co & transient*)
simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
- Rule_Insts.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 *)