diff -r 3e21699bb83b -r 987533262fc2 src/Doc/Implementation/Tactic.thy --- a/src/Doc/Implementation/Tactic.thy Fri Oct 16 10:11:20 2015 +0200 +++ b/src/Doc/Implementation/Tactic.thy Fri Oct 16 14:53:26 2015 +0200 @@ -70,8 +70,6 @@ @{index_ML Goal.conclude: "thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML "Goal.init"}~@{text C} initializes a tactical goal from the well-formed proposition @{text C}. @@ -86,8 +84,6 @@ \<^descr> @{ML "Goal.conclude"}~@{text "thm"} removes the goal protection, even if there are pending subgoals. - - \end{description} \ @@ -150,8 +146,6 @@ The main well-formedness conditions for proper tactics are summarized as follows. - \begin{itemize} - \<^item> General tactic failure is indicated by an empty result, only serious faults may produce an exception. @@ -164,7 +158,6 @@ \<^item> Range errors in subgoal addressing produce an empty result. - \end{itemize} Some of these conditions are checked by higher-level goal infrastructure (\secref{sec:struct-goals}); others are not checked @@ -187,8 +180,6 @@ @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> Type @{ML_type tactic} represents tactics. The well-formedness conditions described above need to be observed. See also @{file "~~/src/Pure/General/seq.ML"} for the underlying @@ -233,8 +224,6 @@ \<^descr> @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put @{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but without changing the main goal protection. - - \end{description} \ @@ -264,8 +253,6 @@ sequence enumerates all possibilities of the following choices (if applicable): - \begin{enumerate} - \<^enum> selecting one of the rules given as argument to the tactic; \<^enum> selecting a subgoal premise to eliminate, unifying it against @@ -274,7 +261,6 @@ \<^enum> unifying the conclusion of the subgoal to the conclusion of the rule. - \end{enumerate} Recall that higher-order unification may produce multiple results that are enumerated here. @@ -295,8 +281,6 @@ @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state using the given theorems, which should normally be introduction rules. The tactic resolves a rule's conclusion with subgoal @{text @@ -350,7 +334,6 @@ These tactics were written for a specific application within the classical reasoner. Flexible subgoals are not updated at will, but are left alone. - \end{description} \ @@ -419,8 +402,6 @@ @{index_ML rename_tac: "string list -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML Rule_Insts.res_inst_tac}~@{text "ctxt insts thm i"} instantiates the rule @{text thm} with the instantiations @{text insts}, as described above, and then performs resolution on subgoal @{text i}. @@ -449,7 +430,6 @@ parameters of subgoal @{text i} according to the provided @{text names} (which need to be distinct identifiers). - \end{description} For historical reasons, the above instantiation tactics take unparsed string arguments, which makes them hard to use in general @@ -473,8 +453,6 @@ @{index_ML flexflex_tac: "Proof.context -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML rotate_tac}~@{text "n i"} rotates the premises of subgoal @{text i} by @{text n} positions: from right to left if @{text n} is positive, and from left to right if @{text n} is negative. @@ -491,8 +469,6 @@ unification. To prevent this, use @{ML Rule_Insts.res_inst_tac} to instantiate some variables in a rule. Normally flex-flex constraints can be ignored; they often disappear as unknowns get instantiated. - - \end{description} \ @@ -513,8 +489,6 @@ @{index_ML_op COMP: "thm * thm -> thm"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal @{text "i"} using @{text "rule"}, without lifting. The @{text "rule"} is taken to have the form @{text "\\<^sub>1 \ \ \\<^sub>m \ \"}, where @@ -534,7 +508,6 @@ \<^descr> @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose (thm\<^sub>1, 1, thm\<^sub>2)"}. - \end{description} \begin{warn} These low-level operations are stepping outside the structure @@ -581,8 +554,6 @@ @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{text "tac\<^sub>1"}~@{ML_op THEN}~@{text "tac\<^sub>2"} is the sequential composition of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a goal state, it returns all states reachable in two steps by applying @@ -621,8 +592,6 @@ "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}. The other primed tacticals work analogously. - - \end{description} \ @@ -641,8 +610,6 @@ @{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal state and returns the resulting sequence, if non-empty; otherwise it returns the original state. Thus, it applies @{text "tac"} at most @@ -672,15 +639,11 @@ \<^descr> @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound by @{text "n"} (where @{ML "~1"} means @{text "\"}). - - \end{description} \ text %mlex \The basic tactics and tacticals considered above follow some algebraic laws: - \begin{itemize} - \<^item> @{ML all_tac} is the identity element of the tactical @{ML_op "THEN"}. @@ -692,8 +655,6 @@ \<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive) functions over more basic combinators (ignoring some internal implementation tricks): - - \end{itemize} \ ML \ @@ -747,8 +708,6 @@ @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac n"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{text "tac 1"}. It applies the @{text tac} to all the subgoals, counting downwards. @@ -774,8 +733,6 @@ @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the corresponding range of subgoals, counting downwards. - - \end{description} \ @@ -800,8 +757,6 @@ @{index_ML CHANGED: "tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the goal state and returns a sequence consisting of those result goal states that are satisfactory in the sense of @{text "sat"}. @@ -810,8 +765,6 @@ state and returns precisely those states that differ from the original state (according to @{ML Thm.eq_thm}). Thus @{ML CHANGED}~@{text "tac"} always has some effect on the state. - - \end{description} \ @@ -824,8 +777,6 @@ @{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if @{text "sat"} returns true. Otherwise it applies @{text "tac"}, then recursively searches from each element of the resulting @@ -839,8 +790,6 @@ \<^descr> @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to search for states having fewer subgoals than the given state. Thus, it insists upon solving at least one subgoal. - - \end{description} \ @@ -857,8 +806,6 @@ However, they do not enumerate all solutions; they terminate after the first satisfactory result from @{text "tac"}. - \begin{description} - \<^descr> @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first search to find states for which @{text "sat"} is true. For most applications, it is too slow. @@ -880,8 +827,6 @@ the result of applying @{text "tac\<^sub>0"} to the goal state. This tactical permits separate tactics for starting the search and continuing the search. - - \end{description} \ @@ -895,8 +840,6 @@ @{index_ML DETERM: "tactic -> tactic"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML COND}~@{text "sat tac\<^sub>1 tac\<^sub>2"} applies @{text "tac\<^sub>1"} to the goal state if it satisfies predicate @{text "sat"}, and applies @{text "tac\<^sub>2"}. It is a conditional tactical in that only one of @@ -915,8 +858,6 @@ \<^descr> @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal state and returns the head of the resulting sequence. @{ML DETERM} limits the search space by making its argument deterministic. - - \end{description} \ @@ -930,8 +871,6 @@ @{index_ML size_of_thm: "thm -> int"} \\ \end{mldecls} - \begin{description} - \<^descr> @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text "thm"} has fewer than @{text "n"} premises. @@ -948,8 +887,6 @@ "thm"}, namely the number of variables, constants and abstractions in its conclusion. It may serve as a distance function for @{ML BEST_FIRST}. - - \end{description} \ end