tuned signature;
authorwenzelm
Fri Mar 20 14:48:04 2015 +0100 (2015-03-20)
changeset 5976356d2c357e6b5
parent 59762 df377a6fdd90
child 59764 4ebf2276f58a
tuned signature;
src/CCL/CCL.thy
src/CCL/Wfd.thy
src/CTT/CTT.thy
src/Doc/Implementation/Tactic.thy
src/Doc/Isar_Ref/Generic.thy
src/Doc/Isar_Ref/ML_Tactic.thy
src/Doc/Tutorial/Protocol/Message.thy
src/FOL/FOL.thy
src/HOL/Auth/Message.thy
src/HOL/Bali/WellType.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/IMPP/Hoare.thy
src/HOL/NanoJava/Equivalence.thy
src/HOL/SET_Protocol/Message_SET.thy
src/HOL/TLA/TLA.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
src/HOL/UNITY/UNITY_tactics.ML
src/LCF/LCF.thy
src/Pure/Tools/rule_insts.ML
src/Sequents/LK0.thy
src/Tools/induct_tacs.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/CCL/CCL.thy	Fri Mar 20 11:53:22 2015 +0100
     1.2 +++ b/src/CCL/CCL.thy	Fri Mar 20 14:48:04 2015 +0100
     1.3 @@ -475,7 +475,8 @@
     1.4  
     1.5  method_setup eq_coinduct3 = {*
     1.6    Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
     1.7 -    SIMPLE_METHOD' (res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3}))
     1.8 +    SIMPLE_METHOD'
     1.9 +      (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] @{thm eq_coinduct3}))
    1.10  *}
    1.11  
    1.12  
     2.1 --- a/src/CCL/Wfd.thy	Fri Mar 20 11:53:22 2015 +0100
     2.2 +++ b/src/CCL/Wfd.thy	Fri Mar 20 14:48:04 2015 +0100
     2.3 @@ -49,7 +49,7 @@
     2.4  method_setup wfd_strengthen = {*
     2.5    Scan.lift Args.name_inner_syntax >> (fn s => fn ctxt =>
     2.6      SIMPLE_METHOD' (fn i =>
     2.7 -      res_inst_tac ctxt [((("Q", 0), Position.none), s)] @{thm wfd_strengthen_lemma} i
     2.8 +      Rule_Insts.res_inst_tac ctxt [((("Q", 0), Position.none), s)] @{thm wfd_strengthen_lemma} i
     2.9          THEN assume_tac ctxt (i + 1)))
    2.10  *}
    2.11  
    2.12 @@ -448,7 +448,7 @@
    2.13  in
    2.14  
    2.15  fun rcall_tac ctxt i =
    2.16 -  let fun tac ps rl i = res_inst_tac ctxt ps rl i THEN atac i
    2.17 +  let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps rl i THEN atac i
    2.18    in IHinst tac @{thms rcallTs} i end
    2.19    THEN eresolve_tac ctxt @{thms rcall_lemmas} i
    2.20  
    2.21 @@ -468,7 +468,7 @@
    2.22  (*** Clean up Correctness Condictions ***)
    2.23  
    2.24  fun clean_ccs_tac ctxt =
    2.25 -  let fun tac ps rl i = eres_inst_tac ctxt ps rl i THEN atac i in
    2.26 +  let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps rl i THEN atac i in
    2.27      TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE'
    2.28        eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE'
    2.29        hyp_subst_tac ctxt))
     3.1 --- a/src/CTT/CTT.thy	Fri Mar 20 11:53:22 2015 +0100
     3.2 +++ b/src/CTT/CTT.thy	Fri Mar 20 14:48:04 2015 +0100
     3.3 @@ -421,13 +421,16 @@
     3.4      The (rtac EqE i) lets them apply to equality judgements. **)
     3.5  
     3.6  fun NE_tac ctxt sp i =
     3.7 -  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i
     3.8 +  TRY (rtac @{thm EqE} i) THEN
     3.9 +  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm NE} i
    3.10  
    3.11  fun SumE_tac ctxt sp i =
    3.12 -  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i
    3.13 +  TRY (rtac @{thm EqE} i) THEN
    3.14 +  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm SumE} i
    3.15  
    3.16  fun PlusE_tac ctxt sp i =
    3.17 -  TRY (rtac @{thm EqE} i) THEN res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i
    3.18 +  TRY (rtac @{thm EqE} i) THEN
    3.19 +  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] @{thm PlusE} i
    3.20  
    3.21  (** Predicate logic reasoning, WITH THINNING!!  Procedures adapted from NJ. **)
    3.22  
     4.1 --- a/src/Doc/Implementation/Tactic.thy	Fri Mar 20 11:53:22 2015 +0100
     4.2 +++ b/src/Doc/Implementation/Tactic.thy	Fri Mar 20 14:48:04 2015 +0100
     4.3 @@ -394,39 +394,39 @@
     4.4  
     4.5  text %mlref \<open>
     4.6    \begin{mldecls}
     4.7 -  @{index_ML res_inst_tac: "Proof.context ->
     4.8 +  @{index_ML Rule_Insts.res_inst_tac: "Proof.context ->
     4.9      ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
    4.10 -  @{index_ML eres_inst_tac: "Proof.context ->
    4.11 +  @{index_ML Rule_Insts.eres_inst_tac: "Proof.context ->
    4.12      ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
    4.13 -  @{index_ML dres_inst_tac: "Proof.context ->
    4.14 +  @{index_ML Rule_Insts.dres_inst_tac: "Proof.context ->
    4.15      ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
    4.16 -  @{index_ML forw_inst_tac: "Proof.context ->
    4.17 +  @{index_ML Rule_Insts.forw_inst_tac: "Proof.context ->
    4.18      ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\
    4.19 -  @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
    4.20 -  @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\
    4.21 +  @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> int -> tactic"} \\
    4.22 +  @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> int -> tactic"} \\
    4.23    @{index_ML rename_tac: "string list -> int -> tactic"} \\
    4.24    \end{mldecls}
    4.25  
    4.26    \begin{description}
    4.27  
    4.28 -  \item @{ML res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
    4.29 +  \item @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the
    4.30    rule @{text thm} with the instantiations @{text insts}, as described
    4.31    above, and then performs resolution on subgoal @{text i}.
    4.32    
    4.33 -  \item @{ML eres_inst_tac} is like @{ML res_inst_tac}, but performs
    4.34 -  elim-resolution.
    4.35 +  \item @{ML Rule_Insts.eres_inst_tac} is like @{ML Rule_Insts.res_inst_tac},
    4.36 +  but performs elim-resolution.
    4.37  
    4.38 -  \item @{ML dres_inst_tac} is like @{ML res_inst_tac}, but performs
    4.39 -  destruct-resolution.
    4.40 +  \item @{ML Rule_Insts.dres_inst_tac} is like @{ML Rule_Insts.res_inst_tac},
    4.41 +  but performs destruct-resolution.
    4.42  
    4.43 -  \item @{ML forw_inst_tac} is like @{ML dres_inst_tac} except that
    4.44 -  the selected assumption is not deleted.
    4.45 +  \item @{ML Rule_Insts.forw_inst_tac} is like @{ML Rule_Insts.dres_inst_tac}
    4.46 +  except that the selected assumption is not deleted.
    4.47  
    4.48 -  \item @{ML subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
    4.49 +  \item @{ML Rule_Insts.subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
    4.50    @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the
    4.51    same as a new subgoal @{text "i + 1"} (in the original context).
    4.52  
    4.53 -  \item @{ML thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
    4.54 +  \item @{ML Rule_Insts.thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
    4.55    premise from subgoal @{text i}.  Note that @{text \<phi>} may contain
    4.56    schematic variables, to abbreviate the intended proposition; the
    4.57    first matching subgoal premise will be deleted.  Removing useless
    4.58 @@ -476,9 +476,9 @@
    4.59    facts resulting from goals, and rarely needs to be invoked manually.
    4.60  
    4.61    Flex-flex constraints arise from difficult cases of higher-order
    4.62 -  unification.  To prevent this, use @{ML res_inst_tac} to instantiate
    4.63 -  some variables in a rule.  Normally flex-flex constraints can be
    4.64 -  ignored; they often disappear as unknowns get instantiated.
    4.65 +  unification.  To prevent this, use @{ML Rule_Insts.res_inst_tac} to
    4.66 +  instantiate some variables in a rule.  Normally flex-flex constraints
    4.67 +  can be ignored; they often disappear as unknowns get instantiated.
    4.68  
    4.69    \end{description}
    4.70  \<close>
     5.1 --- a/src/Doc/Isar_Ref/Generic.thy	Fri Mar 20 11:53:22 2015 +0100
     5.2 +++ b/src/Doc/Isar_Ref/Generic.thy	Fri Mar 20 14:48:04 2015 +0100
     5.3 @@ -319,7 +319,7 @@
     5.4  
     5.5    \item @{method rule_tac} etc. do resolution of rules with explicit
     5.6    instantiation.  This works the same way as the ML tactics @{ML
     5.7 -  res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
     5.8 +  Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
     5.9  
    5.10    Multiple rules may be only given if there is no instantiation; then
    5.11    @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
     6.1 --- a/src/Doc/Isar_Ref/ML_Tactic.thy	Fri Mar 20 11:53:22 2015 +0100
     6.2 +++ b/src/Doc/Isar_Ref/ML_Tactic.thy	Fri Mar 20 14:48:04 2015 +0100
     6.3 @@ -39,7 +39,7 @@
     6.4    @{ML forward_tac}).
     6.5  
     6.6    \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
     6.7 -  @{ML res_inst_tac}).
     6.8 +  @{ML Rule_Insts.res_inst_tac}).
     6.9  
    6.10    \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
    6.11    vs.\ @{ML rtac}).
    6.12 @@ -63,11 +63,11 @@
    6.13    \begin{tabular}{lll}
    6.14      @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
    6.15      @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
    6.16 -    @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    6.17 +    @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
    6.18      @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
    6.19      @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
    6.20      @{ML resolve_tac}~@{text "ctxt [a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
    6.21 -    @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    6.22 +    @{ML Rule_Insts.res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
    6.23      @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
    6.24    \end{tabular}
    6.25    \medskip
     7.1 --- a/src/Doc/Tutorial/Protocol/Message.thy	Fri Mar 20 11:53:22 2015 +0100
     7.2 +++ b/src/Doc/Tutorial/Protocol/Message.thy	Fri Mar 20 14:48:04 2015 +0100
     7.3 @@ -856,7 +856,7 @@
     7.4       (EVERY 
     7.5        [  (*push in occurrences of X...*)
     7.6         (REPEAT o CHANGED)
     7.7 -           (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
     7.8 +         (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
     7.9         (*...allowing further simplifications*)
    7.10         simp_tac ctxt 1,
    7.11         REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
     8.1 --- a/src/FOL/FOL.thy	Fri Mar 20 11:53:22 2015 +0100
     8.2 +++ b/src/FOL/FOL.thy	Fri Mar 20 14:48:04 2015 +0100
     8.3 @@ -67,7 +67,7 @@
     8.4  
     8.5  ML {*
     8.6    fun case_tac ctxt a =
     8.7 -    res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
     8.8 +    Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), a)] @{thm case_split}
     8.9  *}
    8.10  
    8.11  method_setup case_tac = {*
     9.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 20 11:53:22 2015 +0100
     9.2 +++ b/src/HOL/Auth/Message.thy	Fri Mar 20 14:48:04 2015 +0100
     9.3 @@ -866,7 +866,7 @@
     9.4       (EVERY 
     9.5        [  (*push in occurrences of X...*)
     9.6         (REPEAT o CHANGED)
     9.7 -           (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
     9.8 +         (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
     9.9         (*...allowing further simplifications*)
    9.10         simp_tac ctxt 1,
    9.11         REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
    10.1 --- a/src/HOL/Bali/WellType.thy	Fri Mar 20 11:53:22 2015 +0100
    10.2 +++ b/src/HOL/Bali/WellType.thy	Fri Mar 20 14:48:04 2015 +0100
    10.3 @@ -660,10 +660,10 @@
    10.4  (* 17 subgoals *)
    10.5  apply (tactic {* ALLGOALS (fn i =>
    10.6    if i = 11 then EVERY'
    10.7 -   [thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
    10.8 -    thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
    10.9 -    thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
   10.10 -  else thin_tac @{context} "All ?P" i) *})
   10.11 +   [Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean",
   10.12 +    Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e1\<Colon>-?T1",
   10.13 +    Rule_Insts.thin_tac @{context} "?E,dt\<Turnstile>e2\<Colon>-?T2"] i
   10.14 +  else Rule_Insts.thin_tac @{context} "All ?P" i) *})
   10.15  (*apply (safe del: disjE elim!: wt_elim_cases)*)
   10.16  apply (tactic {*ALLGOALS (eresolve_tac @{context} @{thms wt_elim_cases})*})
   10.17  apply (simp_all (no_asm_use) split del: split_if_asm)
    11.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Fri Mar 20 11:53:22 2015 +0100
    11.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Fri Mar 20 14:48:04 2015 +0100
    11.3 @@ -1081,7 +1081,7 @@
    11.4  ML {*
    11.5  
    11.6  fun Seq_case_tac ctxt s i =
    11.7 -  res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i
    11.8 +  Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i
    11.9    THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
   11.10  
   11.11  (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
   11.12 @@ -1093,7 +1093,7 @@
   11.13  
   11.14  (* rws are definitions to be unfolded for admissibility check *)
   11.15  fun Seq_induct_tac ctxt s rws i =
   11.16 -  res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
   11.17 +  Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
   11.18    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1))))
   11.19    THEN simp_tac (ctxt addsimps rws) i;
   11.20  
   11.21 @@ -1102,12 +1102,12 @@
   11.22    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
   11.23  
   11.24  fun pair_tac ctxt s =
   11.25 -  res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE}
   11.26 +  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] @{thm PairE}
   11.27    THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
   11.28  
   11.29  (* induction on a sequence of pairs with pairsplitting and simplification *)
   11.30  fun pair_induct_tac ctxt s rws i =
   11.31 -  res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
   11.32 +  Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
   11.33    THEN pair_tac ctxt "a" (i+3)
   11.34    THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
   11.35    THEN simp_tac (ctxt addsimps rws) i;
    12.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri Mar 20 11:53:22 2015 +0100
    12.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri Mar 20 14:48:04 2015 +0100
    12.3 @@ -135,7 +135,7 @@
    12.4    val take_ss =
    12.5      simpset_of (put_simpset HOL_ss @{context} addsimps (@{thm Rep_cfun_strict1} :: take_rews))
    12.6    fun quant_tac ctxt i = EVERY
    12.7 -    (map (fn name => res_inst_tac ctxt [((("x", 0), Position.none), name)] spec i) x_names)
    12.8 +    (map (fn name => Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), name)] spec i) x_names)
    12.9  
   12.10    (* FIXME: move this message to domain_take_proofs.ML *)
   12.11    val is_finite = #is_finite take_info
   12.12 @@ -182,7 +182,7 @@
   12.13              asm_simp_tac (put_simpset take_ss ctxt) 1 THEN
   12.14              (resolve_tac ctxt prems' THEN_ALL_NEW etac spec) 1
   12.15            fun cases_tacs (cons, exhaust) =
   12.16 -            res_inst_tac ctxt [((("y", 0), Position.none), "x")] exhaust 1 ::
   12.17 +            Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] exhaust 1 ::
   12.18              asm_simp_tac (put_simpset take_ss ctxt addsimps prems) 1 ::
   12.19              map con_tac cons
   12.20            val tacs = tacs1 @ maps cases_tacs (conss ~~ exhausts)
    13.1 --- a/src/HOL/IMPP/Hoare.thy	Fri Mar 20 11:53:22 2015 +0100
    13.2 +++ b/src/HOL/IMPP/Hoare.thy	Fri Mar 20 14:48:04 2015 +0100
    13.3 @@ -286,7 +286,7 @@
    13.4  apply         (blast) (* cut *)
    13.5  apply        (blast) (* weaken *)
    13.6  apply       (tactic {* ALLGOALS (EVERY'
    13.7 -  [REPEAT o thin_tac @{context} "hoare_derivs ?x ?y",
    13.8 +  [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y",
    13.9     simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *})
   13.10  apply       (simp_all (no_asm_use) add: triple_valid_def2)
   13.11  apply       (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *)
    14.1 --- a/src/HOL/NanoJava/Equivalence.thy	Fri Mar 20 11:53:22 2015 +0100
    14.2 +++ b/src/HOL/NanoJava/Equivalence.thy	Fri Mar 20 14:48:04 2015 +0100
    14.3 @@ -105,8 +105,8 @@
    14.4  apply (rule hoare_ehoare.induct)
    14.5  (*18*)
    14.6  apply (tactic {* ALLGOALS (REPEAT o dresolve_tac @{context} [@{thm all_conjunct2}, @{thm all3_conjunct2}]) *})
    14.7 -apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "hoare ?x ?y") *})
    14.8 -apply (tactic {* ALLGOALS (REPEAT o thin_tac @{context} "ehoare ?x ?y") *})
    14.9 +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "hoare ?x ?y") *})
   14.10 +apply (tactic {* ALLGOALS (REPEAT o Rule_Insts.thin_tac @{context} "ehoare ?x ?y") *})
   14.11  apply (simp_all only: cnvalid1_eq cenvalid_def2)
   14.12                   apply fast
   14.13                  apply fast
    15.1 --- a/src/HOL/SET_Protocol/Message_SET.thy	Fri Mar 20 11:53:22 2015 +0100
    15.2 +++ b/src/HOL/SET_Protocol/Message_SET.thy	Fri Mar 20 14:48:04 2015 +0100
    15.3 @@ -871,7 +871,7 @@
    15.4       (EVERY
    15.5        [  (*push in occurrences of X...*)
    15.6         (REPEAT o CHANGED)
    15.7 -           (res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
    15.8 +         (Rule_Insts.res_inst_tac ctxt [((("x", 1), Position.none), "X")] (insert_commute RS ssubst) 1),
    15.9         (*...allowing further simplifications*)
   15.10         simp_tac ctxt 1,
   15.11         REPEAT (FIRSTGOAL (resolve_tac ctxt [allI,impI,notI,conjI,iffI])),
    16.1 --- a/src/HOL/TLA/TLA.thy	Fri Mar 20 11:53:22 2015 +0100
    16.2 +++ b/src/HOL/TLA/TLA.thy	Fri Mar 20 14:48:04 2015 +0100
    16.3 @@ -300,15 +300,15 @@
    16.4  
    16.5  fun merge_temp_box_tac ctxt i =
    16.6    REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i,
    16.7 -    eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i])
    16.8 +    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] @{thm box_thin} i])
    16.9  
   16.10  fun merge_stp_box_tac ctxt i =
   16.11    REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i,
   16.12 -    eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i])
   16.13 +    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] @{thm box_thin} i])
   16.14  
   16.15  fun merge_act_box_tac ctxt i =
   16.16    REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
   16.17 -    eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i])
   16.18 +    Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] @{thm box_thin} i])
   16.19  *}
   16.20  
   16.21  method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}
    17.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 20 11:53:22 2015 +0100
    17.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 20 14:48:04 2015 +0100
    17.3 @@ -185,7 +185,7 @@
    17.4      else
    17.5        let
    17.6          fun instantiate param =
    17.7 -           (map (eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms
    17.8 +          (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms
    17.9                     |> FIRST')
   17.10          val attempts = map instantiate parameters
   17.11        in
   17.12 @@ -221,7 +221,7 @@
   17.13      else
   17.14        let
   17.15          fun instantiates param =
   17.16 -           eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm
   17.17 +          Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm
   17.18  
   17.19          val quantified_var = head_quantified_variable ctxt i st
   17.20        in
   17.21 @@ -673,7 +673,7 @@
   17.22      else
   17.23        let
   17.24          fun instantiate const_name =
   17.25 -          dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)]
   17.26 +          Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)]
   17.27              @{thm leo2_skolemise}
   17.28          val attempts = map instantiate candidate_consts
   17.29        in
   17.30 @@ -1555,8 +1555,8 @@
   17.31        ["% _ . True", "% _ . False", "% x . x", "Not"]
   17.32  
   17.33      val tecs =
   17.34 -      map (fn t_s =>
   17.35 -       eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
   17.36 +      map (fn t_s =>  (* FIXME proper context!? *)
   17.37 +       Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
   17.38         THEN' atac)
   17.39    in
   17.40      (TRY o etac @{thm forall_pos_lift})
   17.41 @@ -1735,7 +1735,7 @@
   17.42                member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
   17.43                no_tac st
   17.44              else
   17.45 -              eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
   17.46 +              Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
   17.47                  @{thm allE} i st
   17.48            end
   17.49       end
    18.1 --- a/src/HOL/UNITY/UNITY_tactics.ML	Fri Mar 20 11:53:22 2015 +0100
    18.2 +++ b/src/HOL/UNITY/UNITY_tactics.ML	Fri Mar 20 14:48:04 2015 +0100
    18.3 @@ -43,9 +43,9 @@
    18.4                              @{thm EnsuresI}, @{thm ensuresI}] 1),
    18.5        (*now there are two subgoals: co & transient*)
    18.6        simp_tac (ctxt addsimps [@{thm mk_total_program_def}]) 2,
    18.7 -      res_inst_tac ctxt
    18.8 +      Rule_Insts.res_inst_tac ctxt
    18.9          [((("act", 0), Position.none), sact)] @{thm totalize_transientI} 2
   18.10 -      ORELSE res_inst_tac ctxt
   18.11 +      ORELSE Rule_Insts.res_inst_tac ctxt
   18.12          [((("act", 0), Position.none), sact)] @{thm transientI} 2,
   18.13           (*simplify the command's domain*)
   18.14        simp_tac (ctxt addsimps @{thms Domain_unfold}) 3,
    19.1 --- a/src/LCF/LCF.thy	Fri Mar 20 11:53:22 2015 +0100
    19.2 +++ b/src/LCF/LCF.thy	Fri Mar 20 14:48:04 2015 +0100
    19.3 @@ -321,7 +321,7 @@
    19.4  method_setup induct = {*
    19.5    Scan.lift Args.name_inner_syntax >> (fn v => fn ctxt =>
    19.6      SIMPLE_METHOD' (fn i =>
    19.7 -      res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN
    19.8 +      Rule_Insts.res_inst_tac ctxt [((("f", 0), Position.none), v)] @{thm induct} i THEN
    19.9        REPEAT (resolve_tac ctxt @{thms adm_lemmas} i)))
   19.10  *}
   19.11  
   19.12 @@ -380,7 +380,7 @@
   19.13  
   19.14  ML {*
   19.15  fun induct2_tac ctxt (f, g) i =
   19.16 -  res_inst_tac ctxt
   19.17 +  Rule_Insts.res_inst_tac ctxt
   19.18      [((("f", 0), Position.none), f), ((("g", 0), Position.none), g)] @{thm induct2} i THEN
   19.19    REPEAT(resolve_tac ctxt @{thms adm_lemmas} i)
   19.20  *}
    20.1 --- a/src/Pure/Tools/rule_insts.ML	Fri Mar 20 11:53:22 2015 +0100
    20.2 +++ b/src/Pure/Tools/rule_insts.ML	Fri Mar 20 14:48:04 2015 +0100
    20.3 @@ -4,8 +4,15 @@
    20.4  Rule instantiations -- operations within implicit rule / subgoal context.
    20.5  *)
    20.6  
    20.7 -signature BASIC_RULE_INSTS =
    20.8 +signature RULE_INSTS =
    20.9  sig
   20.10 +  val where_rule: Proof.context ->
   20.11 +    ((indexname * Position.T) * string) list ->
   20.12 +    (binding * string option * mixfix) list -> thm -> thm
   20.13 +  val of_rule: Proof.context -> string option list * string option list ->
   20.14 +    (binding * string option * mixfix) list -> thm -> thm
   20.15 +  val read_instantiate: Proof.context ->
   20.16 +    ((indexname * Position.T) * string) list -> string list -> thm -> thm
   20.17    val res_inst_tac: Proof.context ->
   20.18      ((indexname * Position.T) * string) list -> thm -> int -> tactic
   20.19    val eres_inst_tac: Proof.context ->
   20.20 @@ -18,18 +25,6 @@
   20.21      ((indexname * Position.T) * string) list -> thm -> int -> tactic
   20.22    val thin_tac: Proof.context -> string -> int -> tactic
   20.23    val subgoal_tac: Proof.context -> string -> int -> tactic
   20.24 -end;
   20.25 -
   20.26 -signature RULE_INSTS =
   20.27 -sig
   20.28 -  include BASIC_RULE_INSTS
   20.29 -  val where_rule: Proof.context ->
   20.30 -    ((indexname * Position.T) * string) list ->
   20.31 -    (binding * string option * mixfix) list -> thm -> thm
   20.32 -  val of_rule: Proof.context -> string option list * string option list ->
   20.33 -    (binding * string option * mixfix) list -> thm -> thm
   20.34 -  val read_instantiate: Proof.context ->
   20.35 -    ((indexname * Position.T) * string) list -> string list -> thm -> thm
   20.36    val make_elim_preserve: Proof.context -> thm -> thm
   20.37    val method:
   20.38      (Proof.context -> ((indexname * Position.T) * string) list -> thm -> int -> tactic) ->
   20.39 @@ -346,6 +341,3 @@
   20.40        "remove premise (dynamic instantiation)");
   20.41  
   20.42  end;
   20.43 -
   20.44 -structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
   20.45 -open Basic_Rule_Insts;
    21.1 --- a/src/Sequents/LK0.thy	Fri Mar 20 11:53:22 2015 +0100
    21.2 +++ b/src/Sequents/LK0.thy	Fri Mar 20 14:48:04 2015 +0100
    21.3 @@ -153,11 +153,13 @@
    21.4  ML {*
    21.5  (*Cut and thin, replacing the right-side formula*)
    21.6  fun cutR_tac ctxt s i =
    21.7 -  res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i  THEN  rtac @{thm thinR} i
    21.8 +  Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s) ] @{thm cut} i THEN
    21.9 +  rtac @{thm thinR} i
   21.10  
   21.11  (*Cut and thin, replacing the left-side formula*)
   21.12  fun cutL_tac ctxt s i =
   21.13 -  res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i  THEN  rtac @{thm thinL} (i+1)
   21.14 +  Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] @{thm cut} i THEN
   21.15 +  rtac @{thm thinL} (i + 1)
   21.16  *}
   21.17  
   21.18  
    22.1 --- a/src/Tools/induct_tacs.ML	Fri Mar 20 11:53:22 2015 +0100
    22.2 +++ b/src/Tools/induct_tacs.ML	Fri Mar 20 14:48:04 2015 +0100
    22.3 @@ -44,7 +44,7 @@
    22.4        (case Induct.vars_of (Thm.term_of (Thm.cprem_of rule 1)) of
    22.5          Var (xi, _) :: _ => xi
    22.6        | _ => raise THM ("Malformed cases rule", 0, [rule]));
    22.7 -  in res_inst_tac ctxt [((xi, Position.none), s)] rule i st end
    22.8 +  in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] rule i st end
    22.9    handle THM _ => Seq.empty;
   22.10  
   22.11  fun case_tac ctxt s = gen_case_tac ctxt s NONE;
   22.12 @@ -104,7 +104,7 @@
   22.13      val concls = Logic.dest_conjunctions (Thm.concl_of rule);
   22.14      val insts = maps prep_inst (concls ~~ varss) handle ListPair.UnequalLengths =>
   22.15        error "Induction rule has different numbers of variables";
   22.16 -  in res_inst_tac ctxt insts rule' i st end
   22.17 +  in Rule_Insts.res_inst_tac ctxt insts rule' i st end
   22.18    handle THM _ => Seq.empty;
   22.19  
   22.20  end;
    23.1 --- a/src/ZF/Tools/induct_tacs.ML	Fri Mar 20 11:53:22 2015 +0100
    23.2 +++ b/src/ZF/Tools/induct_tacs.ML	Fri Mar 20 14:48:04 2015 +0100
    23.3 @@ -101,7 +101,7 @@
    23.4               [] => error "induction is not available for this datatype"
    23.5             | major::_ => FOLogic.dest_Trueprop major)
    23.6    in
    23.7 -    eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
    23.8 +    Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] rule i
    23.9    end
   23.10    handle Find_tname msg =>
   23.11              if exh then (*try boolean case analysis instead*)
    24.1 --- a/src/ZF/UNITY/SubstAx.thy	Fri Mar 20 11:53:22 2015 +0100
    24.2 +++ b/src/ZF/UNITY/SubstAx.thy	Fri Mar 20 14:48:04 2015 +0100
    24.3 @@ -359,7 +359,7 @@
    24.4                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
    24.5              (*now there are two subgoals: co & transient*)
    24.6              simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
    24.7 -            res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2,
    24.8 +            Rule_Insts.res_inst_tac ctxt [((("act", 0), Position.none), sact)] @{thm transientI} 2,
    24.9                 (*simplify the command's domain*)
   24.10              simp_tac (ctxt addsimps [@{thm domain_def}]) 3,
   24.11              (* proving the domain part *)