src/Doc/Implementation/Tactic.thy

   \]
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Goal.init: "cterm -> thm"} \\
-  @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\
-  @{index_ML Goal.protect: "int -> thm -> thm"} \\
-  @{index_ML Goal.conclude: "thm -> thm"} \\
+  @{define_ML Goal.init: "cterm -> thm"} \\
+  @{define_ML Goal.finish: "Proof.context -> thm -> thm"} \\
+  @{define_ML Goal.protect: "int -> thm -> thm"} \\
+  @{define_ML Goal.conclude: "thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Goal.init\<close>~\<open>C\<close> initializes a tactical goal from the well-formed
   proposition \<open>C\<close>.
 

   prevent composition via standard tacticals such as \<^ML>\<open>REPEAT\<close>).
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_type tactic = "thm -> thm Seq.seq"} \\
-  @{index_ML no_tac: tactic} \\
-  @{index_ML all_tac: tactic} \\
-  @{index_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
-  @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
-  @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
-  @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
-  @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
-  @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
+  @{define_ML_type tactic = "thm -> thm Seq.seq"} \\
+  @{define_ML no_tac: tactic} \\
+  @{define_ML all_tac: tactic} \\
+  @{define_ML print_tac: "Proof.context -> string -> tactic"} \\[1ex]
+  @{define_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
+  @{define_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
+  @{define_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
+  @{define_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
+  @{define_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> Type \<^ML_type>\<open>tactic\<close> represents tactics. The well-formedness conditions
   described above need to be observed. See also \<^file>\<open>~~/src/Pure/General/seq.ML\<close>
   for the underlying implementation of lazy sequences.

   enumerated here.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex]
-  @{index_ML assume_tac: "Proof.context -> int -> tactic"} \\
-  @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
-  @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
-  @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
+  @{define_ML resolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML eresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML dresolve_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML forward_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML biresolve_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\[1ex]
+  @{define_ML assume_tac: "Proof.context -> int -> tactic"} \\
+  @{define_ML eq_assume_tac: "int -> tactic"} \\[1ex]
+  @{define_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
+  @{define_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>resolve_tac\<close>~\<open>ctxt thms i\<close> refines the goal state using the given
   theorems, which should normally be introduction rules. The tactic resolves a
   rule's conclusion with subgoal \<open>i\<close>, replacing it by the corresponding

   type instantiations are seldom necessary.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML Rule_Insts.res_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.res_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.eres_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.eres_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.dres_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.dres_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.forw_inst_tac: "Proof.context ->
+  @{define_ML Rule_Insts.forw_inst_tac: "Proof.context ->
     ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list ->
     thm -> int -> tactic"} \\
-  @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string ->
+  @{define_ML Rule_Insts.subgoal_tac: "Proof.context -> string ->
     (binding * string option * mixfix) list -> int -> tactic"} \\
-  @{index_ML Rule_Insts.thin_tac: "Proof.context -> string ->
+  @{define_ML Rule_Insts.thin_tac: "Proof.context -> string ->
     (binding * string option * mixfix) list -> int -> tactic"} \\
-  @{index_ML rename_tac: "string list -> int -> tactic"} \\
+  @{define_ML rename_tac: "string list -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>Rule_Insts.res_inst_tac\<close>~\<open>ctxt insts thm i\<close> instantiates the rule
   \<open>thm\<close> with the instantiations \<open>insts\<close>, as described above, and then performs
   resolution on subgoal \<open>i\<close>.

   conceptual sets of formulae.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML rotate_tac: "int -> int -> tactic"} \\
-  @{index_ML distinct_subgoals_tac: tactic} \\
-  @{index_ML flexflex_tac: "Proof.context -> tactic"} \\
+  @{define_ML rotate_tac: "int -> int -> tactic"} \\
+  @{define_ML distinct_subgoals_tac: tactic} \\
+  @{define_ML flexflex_tac: "Proof.context -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>rotate_tac\<close>~\<open>n i\<close> rotates the premises of subgoal \<open>i\<close> by \<open>n\<close>
   positions: from right to left if \<open>n\<close> is positive, and from left to right if
   \<open>n\<close> is negative.

   Schematic variables are not renamed by default, so beware of clashes!
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
-  @{index_ML Drule.compose: "thm * int * thm -> thm"} \\
-  @{index_ML_infix COMP: "thm * thm -> thm"} \\
+  @{define_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
+  @{define_ML Drule.compose: "thm * int * thm -> thm"} \\
+  @{define_ML_infix COMP: "thm * thm -> thm"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>compose_tac\<close>~\<open>ctxt (flag, rule, m) i\<close> refines subgoal \<open>i\<close> using
   \<open>rule\<close>, without lifting. The \<open>rule\<close> is taken to have the form \<open>\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow>
   \<psi>\<close>, where \<open>\<psi>\<close> need not be atomic; thus \<open>m\<close> determines the number of new

   subgoal addressing.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML_infix "THEN": "tactic * tactic -> tactic"} \\
-  @{index_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\
-  @{index_ML_infix "APPEND": "tactic * tactic -> tactic"} \\
-  @{index_ML "EVERY": "tactic list -> tactic"} \\
-  @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
-
-  @{index_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
-  @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
-  @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
+  @{define_ML_infix "THEN": "tactic * tactic -> tactic"} \\
+  @{define_ML_infix "ORELSE": "tactic * tactic -> tactic"} \\
+  @{define_ML_infix "APPEND": "tactic * tactic -> tactic"} \\
+  @{define_ML "EVERY": "tactic list -> tactic"} \\
+  @{define_ML "FIRST": "tactic list -> tactic"} \\[0.5ex]
+
+  @{define_ML_infix "THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{define_ML_infix "ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{define_ML_infix "APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\
+  @{define_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\
+  @{define_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<open>tac\<^sub>1\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac\<^sub>2\<close> is the sequential composition of \<open>tac\<^sub>1\<close> and
   \<open>tac\<^sub>2\<close>. Applied to a goal state, it returns all states reachable in two
   steps by applying \<open>tac\<^sub>1\<close> followed by \<open>tac\<^sub>2\<close>. First, it applies \<open>tac\<^sub>1\<close> to

   the stylized forms of ``\<^verbatim>\<open>?\<close>'' and ``\<^verbatim>\<open>+\<close>'' in Isar method expressions.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML "TRY": "tactic -> tactic"} \\
-  @{index_ML "REPEAT": "tactic -> tactic"} \\
-  @{index_ML "REPEAT1": "tactic -> tactic"} \\
-  @{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\
-  @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
+  @{define_ML "TRY": "tactic -> tactic"} \\
+  @{define_ML "REPEAT": "tactic -> tactic"} \\
+  @{define_ML "REPEAT1": "tactic -> tactic"} \\
+  @{define_ML "REPEAT_DETERM": "tactic -> tactic"} \\
+  @{define_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>TRY\<close>~\<open>tac\<close> applies \<open>tac\<close> to the goal state and returns the resulting
   sequence, if non-empty; otherwise it returns the original state. Thus, it
   applies \<open>tac\<close> at most once.

   situations where a different order is desired.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
-  @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
-  @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
-  @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
-  @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
-  @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
-  @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
-  @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
+  @{define_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
+  @{define_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
+  @{define_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
+  @{define_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
+  @{define_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
+  @{define_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
+  @{define_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>ALLGOALS\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_op>\<open>THEN\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>THEN\<close>~\<open>tac 1\<close>. It applies the \<open>tac\<close> to all the subgoals, counting downwards.
 
   \<^descr> \<^ML>\<open>SOMEGOAL\<close>~\<open>tac\<close> is equivalent to \<open>tac n\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>\<dots>\<close>~\<^ML_op>\<open>ORELSE\<close>~\<open>tac 1\<close>. It applies \<open>tac\<close> to one subgoal, counting downwards.

 
 subsubsection \<open>Filtering a tactic's results\<close>
 
 text \<open>
   \begin{mldecls}
-  @{index_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
-  @{index_ML CHANGED: "tactic -> tactic"} \\
+  @{define_ML FILTER: "(thm -> bool) -> tactic -> tactic"} \\
+  @{define_ML CHANGED: "tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>FILTER\<close>~\<open>sat tac\<close> applies \<open>tac\<close> to the goal state and returns a
   sequence consisting of those result goal states that are satisfactory in the
   sense of \<open>sat\<close>.

 
 subsubsection \<open>Depth-first search\<close>
 
 text \<open>
   \begin{mldecls}
-  @{index_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
-  @{index_ML DEPTH_SOLVE: "tactic -> tactic"} \\
-  @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
+  @{define_ML DEPTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
+  @{define_ML DEPTH_SOLVE: "tactic -> tactic"} \\
+  @{define_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>DEPTH_FIRST\<close>~\<open>sat tac\<close> returns the goal state if \<open>sat\<close> returns true.
   Otherwise it applies \<open>tac\<close>, then recursively searches from each element of
   the resulting sequence. The code uses a stack for efficiency, in effect

 
 subsubsection \<open>Other search strategies\<close>
 
 text \<open>
   \begin{mldecls}
-  @{index_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
-  @{index_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
-  @{index_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
+  @{define_ML BREADTH_FIRST: "(thm -> bool) -> tactic -> tactic"} \\
+  @{define_ML BEST_FIRST: "(thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
+  @{define_ML THEN_BEST_FIRST: "tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic"} \\
   \end{mldecls}
 
   These search strategies will find a solution if one exists. However, they do
   not enumerate all solutions; they terminate after the first satisfactory
   result from \<open>tac\<close>.

 
 subsubsection \<open>Auxiliary tacticals for searching\<close>
 
 text \<open>
   \begin{mldecls}
-  @{index_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
-  @{index_ML IF_UNSOLVED: "tactic -> tactic"} \\
-  @{index_ML SOLVE: "tactic -> tactic"} \\
-  @{index_ML DETERM: "tactic -> tactic"} \\
+  @{define_ML COND: "(thm -> bool) -> tactic -> tactic -> tactic"} \\
+  @{define_ML IF_UNSOLVED: "tactic -> tactic"} \\
+  @{define_ML SOLVE: "tactic -> tactic"} \\
+  @{define_ML DETERM: "tactic -> tactic"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>COND\<close>~\<open>sat tac\<^sub>1 tac\<^sub>2\<close> applies \<open>tac\<^sub>1\<close> to the goal state if it
   satisfies predicate \<open>sat\<close>, and applies \<open>tac\<^sub>2\<close>. It is a conditional tactical
   in that only one of \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close> is applied to a goal state. However,

 
 subsubsection \<open>Predicates and functions useful for searching\<close>
 
 text \<open>
   \begin{mldecls}
-  @{index_ML has_fewer_prems: "int -> thm -> bool"} \\
-  @{index_ML Thm.eq_thm: "thm * thm -> bool"} \\
-  @{index_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
-  @{index_ML size_of_thm: "thm -> int"} \\
+  @{define_ML has_fewer_prems: "int -> thm -> bool"} \\
+  @{define_ML Thm.eq_thm: "thm * thm -> bool"} \\
+  @{define_ML Thm.eq_thm_prop: "thm * thm -> bool"} \\
+  @{define_ML size_of_thm: "thm -> int"} \\
   \end{mldecls}
 
   \<^descr> \<^ML>\<open>has_fewer_prems\<close>~\<open>n thm\<close> reports whether \<open>thm\<close> has fewer than \<open>n\<close>
   premises.