# HG changeset patch # User wenzelm # Date 1427113859 -3600 # Node ID 23b67731f4f09592dbed585f6d22816f58849a56 # Parent fe5b796d6b2a9e5be9546bc28a794fb230a735e0 support 'for' fixes in rule_tac etc.; diff -r fe5b796d6b2a -r 23b67731f4f0 src/CCL/CCL.thy --- 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})) *} diff -r fe5b796d6b2a -r 23b67731f4f0 src/CCL/Wfd.thy --- 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)) diff -r fe5b796d6b2a -r 23b67731f4f0 src/CTT/CTT.thy --- 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. **) diff -r fe5b796d6b2a -r 23b67731f4f0 src/Doc/Implementation/Tactic.thy --- 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 \ \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} diff -r fe5b796d6b2a -r 23b67731f4f0 src/Doc/Isar_Ref/Generic.thy --- 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 \ (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} | - @@{method frule_tac} | @@{method cut_tac} | @@{method thin_tac}) @{syntax goal_spec}? \ + @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \ ( 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'))? \} \begin{description} diff -r fe5b796d6b2a -r 23b67731f4f0 src/Doc/Tutorial/Protocol/Message.thy --- 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])), diff -r fe5b796d6b2a -r 23b67731f4f0 src/FOL/FOL.thy --- 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!)" diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/Auth/Message.thy --- 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])), diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/Bali/WellType.thy --- 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\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) *}) + [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 fe5b796d6b2a -r 23b67731f4f0 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- 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; diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- 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) diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/IMPP/Hoare.thy --- 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 *) diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/NanoJava/Equivalence.thy --- 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 diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/SET_Protocol/Message_SET.thy --- 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])), diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/TLA/TLA.thy --- 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)) *} diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- 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 diff -r fe5b796d6b2a -r 23b67731f4f0 src/HOL/UNITY/UNITY_tactics.ML --- 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, diff -r fe5b796d6b2a -r 23b67731f4f0 src/LCF/LCF.thy --- 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) *} diff -r fe5b796d6b2a -r 23b67731f4f0 src/Pure/Tools/rule_insts.ML --- 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; diff -r fe5b796d6b2a -r 23b67731f4f0 src/Sequents/LK0.thy --- 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) *} diff -r fe5b796d6b2a -r 23b67731f4f0 src/Tools/induct_tacs.ML --- 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; diff -r fe5b796d6b2a -r 23b67731f4f0 src/ZF/Tools/induct_tacs.ML --- 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; diff -r fe5b796d6b2a -r 23b67731f4f0 src/ZF/UNITY/SubstAx.thy --- 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 *)