--- a/src/Doc/Implementation/Tactic.thy Tue Oct 20 23:03:46 2015 +0200
+++ b/src/Doc/Implementation/Tactic.thy Tue Oct 20 23:53:40 2015 +0200
@@ -5,40 +5,36 @@
chapter \<open>Tactical reasoning\<close>
text \<open>Tactical reasoning works by refining an initial claim in a
- backwards fashion, until a solved form is reached. A @{text "goal"}
+ backwards fashion, until a solved form is reached. A \<open>goal\<close>
consists of several subgoals that need to be solved in order to
achieve the main statement; zero subgoals means that the proof may
- be finished. A @{text "tactic"} is a refinement operation that maps
- a goal to a lazy sequence of potential successors. A @{text
- "tactical"} is a combinator for composing tactics.\<close>
+ be finished. A \<open>tactic\<close> is a refinement operation that maps
+ a goal to a lazy sequence of potential successors. A \<open>tactical\<close> is a combinator for composing tactics.\<close>
section \<open>Goals \label{sec:tactical-goals}\<close>
text \<open>
Isabelle/Pure represents a goal as a theorem stating that the
- subgoals imply the main goal: @{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
- C"}. The outermost goal structure is that of a Horn Clause: i.e.\
+ subgoals imply the main goal: \<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow>
+ C\<close>. The outermost goal structure is that of a Horn Clause: i.e.\
an iterated implication without any quantifiers\footnote{Recall that
- outermost @{text "\<And>x. \<phi>[x]"} is always represented via schematic
- variables in the body: @{text "\<phi>[?x]"}. These variables may get
- instantiated during the course of reasoning.}. For @{text "n = 0"}
+ outermost \<open>\<And>x. \<phi>[x]\<close> is always represented via schematic
+ variables in the body: \<open>\<phi>[?x]\<close>. These variables may get
+ instantiated during the course of reasoning.}. For \<open>n = 0\<close>
a goal is called ``solved''.
- The structure of each subgoal @{text "A\<^sub>i"} is that of a
- general Hereditary Harrop Formula @{text "\<And>x\<^sub>1 \<dots>
- \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B"}. Here @{text
- "x\<^sub>1, \<dots>, x\<^sub>k"} are goal parameters, i.e.\
- arbitrary-but-fixed entities of certain types, and @{text
- "H\<^sub>1, \<dots>, H\<^sub>m"} are goal hypotheses, i.e.\ facts that may
+ The structure of each subgoal \<open>A\<^sub>i\<close> is that of a
+ general Hereditary Harrop Formula \<open>\<And>x\<^sub>1 \<dots>
+ \<And>x\<^sub>k. H\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> H\<^sub>m \<Longrightarrow> B\<close>. Here \<open>x\<^sub>1, \<dots>, x\<^sub>k\<close> are goal parameters, i.e.\
+ arbitrary-but-fixed entities of certain types, and \<open>H\<^sub>1, \<dots>, H\<^sub>m\<close> are goal hypotheses, i.e.\ facts that may
be assumed locally. Together, this forms the goal context of the
- conclusion @{text B} to be established. The goal hypotheses may be
+ conclusion \<open>B\<close> to be established. The goal hypotheses may be
again arbitrary Hereditary Harrop Formulas, although the level of
nesting rarely exceeds 1--2 in practice.
- The main conclusion @{text C} is internally marked as a protected
- proposition, which is represented explicitly by the notation @{text
- "#C"} here. This ensures that the decomposition into subgoals and
+ The main conclusion \<open>C\<close> is internally marked as a protected
+ proposition, which is represented explicitly by the notation \<open>#C\<close> here. This ensures that the decomposition into subgoals and
main conclusion is well-defined for arbitrarily structured claims.
\<^medskip>
@@ -46,8 +42,8 @@
Isabelle/Pure rules:
\[
- \infer[@{text "(init)"}]{@{text "C \<Longrightarrow> #C"}}{} \qquad
- \infer[@{text "(finish)"}]{@{text "C"}}{@{text "#C"}}
+ \infer[\<open>(init)\<close>]{\<open>C \<Longrightarrow> #C\<close>}{} \qquad
+ \infer[\<open>(finish)\<close>]{\<open>C\<close>}{\<open>#C\<close>}
\]
\<^medskip>
@@ -55,10 +51,10 @@
with protected propositions:
\[
- \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C"}}{@{text "A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C"}}
+ \infer[\<open>(protect n)\<close>]{\<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> #C\<close>}{\<open>A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> C\<close>}
\]
\[
- \infer[@{text "(conclude)"}]{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> C"}}{@{text "A \<Longrightarrow> \<dots> \<Longrightarrow> #C"}}
+ \infer[\<open>(conclude)\<close>]{\<open>A \<Longrightarrow> \<dots> \<Longrightarrow> C\<close>}{\<open>A \<Longrightarrow> \<dots> \<Longrightarrow> #C\<close>}
\]
\<close>
@@ -70,26 +66,26 @@
@{index_ML Goal.conclude: "thm -> thm"} \\
\end{mldecls}
- \<^descr> @{ML "Goal.init"}~@{text C} initializes a tactical goal from
- the well-formed proposition @{text C}.
+ \<^descr> @{ML "Goal.init"}~\<open>C\<close> initializes a tactical goal from
+ the well-formed proposition \<open>C\<close>.
- \<^descr> @{ML "Goal.finish"}~@{text "ctxt thm"} checks whether theorem
- @{text "thm"} is a solved goal (no subgoals), and concludes the
+ \<^descr> @{ML "Goal.finish"}~\<open>ctxt thm\<close> checks whether theorem
+ \<open>thm\<close> is a solved goal (no subgoals), and concludes the
result by removing the goal protection. The context is only
required for printing error messages.
- \<^descr> @{ML "Goal.protect"}~@{text "n thm"} protects the statement
- of theorem @{text "thm"}. The parameter @{text n} indicates the
+ \<^descr> @{ML "Goal.protect"}~\<open>n thm\<close> protects the statement
+ of theorem \<open>thm\<close>. The parameter \<open>n\<close> indicates the
number of premises to be retained.
- \<^descr> @{ML "Goal.conclude"}~@{text "thm"} removes the goal
+ \<^descr> @{ML "Goal.conclude"}~\<open>thm\<close> removes the goal
protection, even if there are pending subgoals.
\<close>
section \<open>Tactics\label{sec:tactics}\<close>
-text \<open>A @{text "tactic"} is a function @{text "goal \<rightarrow> goal\<^sup>*\<^sup>*"} that
+text \<open>A \<open>tactic\<close> is a function \<open>goal \<rightarrow> goal\<^sup>*\<^sup>*\<close> that
maps a given goal state (represented as a theorem, cf.\
\secref{sec:tactical-goals}) to a lazy sequence of potential
successor states. The underlying sequence implementation is lazy
@@ -121,7 +117,7 @@
schematic goal variables).
Tactics with explicit \<^emph>\<open>subgoal addressing\<close> are of the form
- @{text "int \<rightarrow> tactic"} and may be applied to a particular subgoal
+ \<open>int \<rightarrow> tactic\<close> and may be applied to a particular subgoal
(counting from 1). If the subgoal number is out of range, the
tactic should fail with an empty result sequence, but must not raise
an exception!
@@ -139,7 +135,7 @@
very common error when implementing tactics!
Tactics with internal subgoal addressing should expose the subgoal
- index as @{text "int"} argument in full generality; a hardwired
+ index as \<open>int\<close> argument in full generality; a hardwired
subgoal 1 is not acceptable.
\<^medskip>
@@ -195,16 +191,16 @@
\<^descr> @{ML all_tac} is a tactic that always succeeds, returning a
singleton sequence with unchanged goal state.
- \<^descr> @{ML print_tac}~@{text "ctxt message"} is like @{ML all_tac}, but
+ \<^descr> @{ML print_tac}~\<open>ctxt message\<close> is like @{ML all_tac}, but
prints a message together with the goal state on the tracing
channel.
- \<^descr> @{ML PRIMITIVE}~@{text rule} turns a primitive inference rule
+ \<^descr> @{ML PRIMITIVE}~\<open>rule\<close> turns a primitive inference rule
into a tactic with unique result. Exception @{ML THM} is considered
a regular tactic failure and produces an empty result; other
exceptions are passed through.
- \<^descr> @{ML SUBGOAL}~@{text "(fn (subgoal, i) => tactic)"} is the
+ \<^descr> @{ML SUBGOAL}~\<open>(fn (subgoal, i) => tactic)\<close> is the
most basic form to produce a tactic with subgoal addressing. The
given abstraction over the subgoal term and subgoal number allows to
peek at the relevant information of the full goal state. The
@@ -215,14 +211,14 @@
avoids expensive re-certification in situations where the subgoal is
used directly for primitive inferences.
- \<^descr> @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
- specified subgoal @{text "i"}. This rearranges subgoals and the
+ \<^descr> @{ML SELECT_GOAL}~\<open>tac i\<close> confines a tactic to the
+ specified subgoal \<open>i\<close>. This rearranges subgoals and the
main goal protection (\secref{sec:tactical-goals}), while retaining
the syntactic context of the overall goal state (concerning
schematic variables etc.).
- \<^descr> @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
- @{text "i"} in front. This is similar to @{ML SELECT_GOAL}, but
+ \<^descr> @{ML PREFER_GOAL}~\<open>tac i\<close> rearranges subgoals to put
+ \<open>i\<close> in front. This is similar to @{ML SELECT_GOAL}, but
without changing the main goal protection.
\<close>
@@ -237,7 +233,7 @@
\<^emph>\<open>Destruct-resolution\<close> is like elim-resolution, but the given
destruction rules are first turned into canonical elimination
format. \<^emph>\<open>Forward-resolution\<close> is like destruct-resolution, but
- without deleting the selected assumption. The @{text "r/e/d/f"}
+ without deleting the selected assumption. The \<open>r/e/d/f\<close>
naming convention is maintained for several different kinds of
resolution rules and tactics.
@@ -281,20 +277,19 @@
@{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
\end{mldecls}
- \<^descr> @{ML resolve_tac}~@{text "ctxt thms i"} refines the goal state
+ \<^descr> @{ML resolve_tac}~\<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 @{text
- i}, replacing it by the corresponding versions of the rule's
+ rules. The tactic resolves a rule's conclusion with subgoal \<open>i\<close>, replacing it by the corresponding versions of the rule's
premises.
- \<^descr> @{ML eresolve_tac}~@{text "ctxt thms i"} performs elim-resolution
+ \<^descr> @{ML eresolve_tac}~\<open>ctxt thms i\<close> performs elim-resolution
with the given theorems, which are normally be elimination rules.
Note that @{ML_text "eresolve_tac ctxt [asm_rl]"} is equivalent to @{ML_text
"assume_tac ctxt"}, which facilitates mixing of assumption steps with
genuine eliminations.
- \<^descr> @{ML dresolve_tac}~@{text "ctxt thms i"} performs
+ \<^descr> @{ML dresolve_tac}~\<open>ctxt thms i\<close> performs
destruct-resolution with the given theorems, which should normally
be destruction rules. This replaces an assumption by the result of
applying one of the rules.
@@ -303,21 +298,20 @@
selected assumption is not deleted. It applies a rule to an
assumption, adding the result as a new assumption.
- \<^descr> @{ML biresolve_tac}~@{text "ctxt brls i"} refines the proof state
+ \<^descr> @{ML biresolve_tac}~\<open>ctxt brls i\<close> refines the proof state
by resolution or elim-resolution on each rule, as indicated by its
- flag. It affects subgoal @{text "i"} of the proof state.
+ flag. It affects subgoal \<open>i\<close> of the proof state.
- For each pair @{text "(flag, rule)"}, it applies resolution if the
- flag is @{text "false"} and elim-resolution if the flag is @{text
- "true"}. A single tactic call handles a mixture of introduction and
+ For each pair \<open>(flag, rule)\<close>, it applies resolution if the
+ flag is \<open>false\<close> and elim-resolution if the flag is \<open>true\<close>. A single tactic call handles a mixture of introduction and
elimination rules, which is useful to organize the search process
systematically in proof tools.
- \<^descr> @{ML assume_tac}~@{text "ctxt i"} attempts to solve subgoal @{text i}
+ \<^descr> @{ML assume_tac}~\<open>ctxt i\<close> attempts to solve subgoal \<open>i\<close>
by assumption (modulo higher-order unification).
\<^descr> @{ML eq_assume_tac} is similar to @{ML assume_tac}, but checks
- only for immediate @{text "\<alpha>"}-convertibility instead of using
+ only for immediate \<open>\<alpha>\<close>-convertibility instead of using
unification. It succeeds (with a unique next state) if one of the
assumptions is equal to the subgoal's conclusion. Since it does not
instantiate variables, it cannot make other subgoals unprovable.
@@ -346,25 +340,22 @@
higher-order unification is not so useful. This typically involves
rules like universal elimination, existential introduction, or
equational substitution. Here the unification problem involves
- fully flexible @{text "?P ?x"} schemes, which are hard to manage
+ fully flexible \<open>?P ?x\<close> schemes, which are hard to manage
without further hints.
- By providing a (small) rigid term for @{text "?x"} explicitly, the
- remaining unification problem is to assign a (large) term to @{text
- "?P"}, according to the shape of the given subgoal. This is
+ By providing a (small) rigid term for \<open>?x\<close> explicitly, the
+ remaining unification problem is to assign a (large) term to \<open>?P\<close>, according to the shape of the given subgoal. This is
sufficiently well-behaved in most practical situations.
\<^medskip>
- Isabelle provides separate versions of the standard @{text
- "r/e/d/f"} resolution tactics that allow to provide explicit
+ Isabelle provides separate versions of the standard \<open>r/e/d/f\<close> resolution tactics that allow to provide explicit
instantiations of unknowns of the given rule, wrt.\ terms that refer
to the implicit context of the selected subgoal.
- An instantiation consists of a list of pairs of the form @{text
- "(?x, t)"}, where @{text ?x} is a schematic variable occurring in
- the given rule, and @{text t} is a term from the current proof
+ An instantiation consists of a list of pairs of the form \<open>(?x, t)\<close>, where \<open>?x\<close> is a schematic variable occurring in
+ the given rule, and \<open>t\<close> is a term from the current proof
context, augmented by the local goal parameters of the selected
- subgoal; cf.\ the @{text "focus"} operation described in
+ subgoal; cf.\ the \<open>focus\<close> operation described in
\secref{sec:variables}.
Entering the syntactic context of a subgoal is a brittle operation,
@@ -373,8 +364,7 @@
global names. Explicit renaming of subgoal parameters prior to
explicit instantiation might help to achieve a bit more robustness.
- Type instantiations may be given as well, via pairs like @{text
- "(?'a, \<tau>)"}. Type instantiations are distinguished from term
+ Type instantiations may be given as well, via pairs like \<open>(?'a, \<tau>)\<close>. Type instantiations are distinguished from term
instantiations by the syntactic form of the schematic variable.
Types are instantiated before terms are. Since term instantiation
already performs simple type-inference, so explicit type
@@ -402,9 +392,9 @@
@{index_ML rename_tac: "string list -> int -> tactic"} \\
\end{mldecls}
- \<^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}.
+ \<^descr> @{ML Rule_Insts.res_inst_tac}~\<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>.
\<^descr> @{ML Rule_Insts.eres_inst_tac} is like @{ML Rule_Insts.res_inst_tac},
but performs elim-resolution.
@@ -415,20 +405,19 @@
\<^descr> @{ML Rule_Insts.forw_inst_tac} is like @{ML Rule_Insts.dres_inst_tac}
except that the selected assumption is not deleted.
- \<^descr> @{ML Rule_Insts.subgoal_tac}~@{text "ctxt \<phi> i"} adds the proposition
- @{text "\<phi>"} as local premise to subgoal @{text "i"}, and poses the
- same as a new subgoal @{text "i + 1"} (in the original context).
+ \<^descr> @{ML Rule_Insts.subgoal_tac}~\<open>ctxt \<phi> i\<close> adds the proposition
+ \<open>\<phi>\<close> as local premise to subgoal \<open>i\<close>, and poses the
+ same as a new subgoal \<open>i + 1\<close> (in the original context).
- \<^descr> @{ML Rule_Insts.thin_tac}~@{text "ctxt \<phi> i"} deletes the specified
- premise from subgoal @{text i}. Note that @{text \<phi>} may contain
+ \<^descr> @{ML Rule_Insts.thin_tac}~\<open>ctxt \<phi> i\<close> deletes the specified
+ premise from subgoal \<open>i\<close>. Note that \<open>\<phi>\<close> may contain
schematic variables, to abbreviate the intended proposition; the
first matching subgoal premise will be deleted. Removing useless
premises from a subgoal increases its readability and can make
search tactics run faster.
- \<^descr> @{ML rename_tac}~@{text "names i"} renames the innermost
- parameters of subgoal @{text i} according to the provided @{text
- names} (which need to be distinct identifiers).
+ \<^descr> @{ML rename_tac}~\<open>names i\<close> renames the innermost
+ parameters of subgoal \<open>i\<close> according to the provided \<open>names\<close> (which need to be distinct identifiers).
For historical reasons, the above instantiation tactics take
@@ -453,9 +442,9 @@
@{index_ML flexflex_tac: "Proof.context -> tactic"} \\
\end{mldecls}
- \<^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.
+ \<^descr> @{ML rotate_tac}~\<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.
\<^descr> @{ML distinct_subgoals_tac} removes duplicate subgoals from a
proof state. This is potentially inefficient.
@@ -489,24 +478,21 @@
@{index_ML_op COMP: "thm * thm -> thm"} \\
\end{mldecls}
- \<^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 "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
- @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
- number of new subgoals. If @{text "flag"} is @{text "true"} then it
- performs elim-resolution --- it solves the first premise of @{text
- "rule"} by assumption and deletes that assumption.
+ \<^descr> @{ML compose_tac}~\<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 subgoals. If \<open>flag\<close> is \<open>true\<close> then it
+ performs elim-resolution --- it solves the first premise of \<open>rule\<close> by assumption and deletes that assumption.
- \<^descr> @{ML Drule.compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
- regarded as an atomic formula, to solve premise @{text "i"} of
- @{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
- "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. The unique @{text "s"} that
- unifies @{text "\<psi>"} and @{text "\<phi>\<^sub>i"} yields the theorem @{text "(\<phi>\<^sub>1 \<Longrightarrow>
- \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}. Multiple results are considered as
+ \<^descr> @{ML Drule.compose}~\<open>(thm\<^sub>1, i, thm\<^sub>2)\<close> uses \<open>thm\<^sub>1\<close>,
+ regarded as an atomic formula, to solve premise \<open>i\<close> of
+ \<open>thm\<^sub>2\<close>. Let \<open>thm\<^sub>1\<close> and \<open>thm\<^sub>2\<close> be \<open>\<psi>\<close> and \<open>\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>\<close>. The unique \<open>s\<close> that
+ unifies \<open>\<psi>\<close> and \<open>\<phi>\<^sub>i\<close> yields the theorem \<open>(\<phi>\<^sub>1 \<Longrightarrow>
+ \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s\<close>. Multiple results are considered as
error (exception @{ML THM}).
- \<^descr> @{text "thm\<^sub>1 COMP thm\<^sub>2"} is the same as @{text "Drule.compose
- (thm\<^sub>1, 1, thm\<^sub>2)"}.
+ \<^descr> \<open>thm\<^sub>1 COMP thm\<^sub>2\<close> is the same as \<open>Drule.compose
+ (thm\<^sub>1, 1, thm\<^sub>2)\<close>.
\begin{warn}
@@ -554,42 +540,35 @@
@{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\
\end{mldecls}
- \<^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
+ \<^descr> \<open>tac\<^sub>1\<close>~@{ML_op THEN}~\<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
- @{text "tac\<^sub>1"} followed by @{text "tac\<^sub>2"}. First, it applies @{text
- "tac\<^sub>1"} to the goal state, getting a sequence of possible next
- states; then, it applies @{text "tac\<^sub>2"} to each of these and
+ \<open>tac\<^sub>1\<close> followed by \<open>tac\<^sub>2\<close>. First, it applies \<open>tac\<^sub>1\<close> to the goal state, getting a sequence of possible next
+ states; then, it applies \<open>tac\<^sub>2\<close> to each of these and
concatenates the results to produce again one flat sequence of
states.
- \<^descr> @{text "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "tac\<^sub>2"} makes a choice
- between @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it
- tries @{text "tac\<^sub>1"} and returns the result if non-empty; if @{text
- "tac\<^sub>1"} fails then it uses @{text "tac\<^sub>2"}. This is a deterministic
- choice: if @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded
+ \<^descr> \<open>tac\<^sub>1\<close>~@{ML_op ORELSE}~\<open>tac\<^sub>2\<close> makes a choice
+ between \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>. Applied to a state, it
+ tries \<open>tac\<^sub>1\<close> and returns the result if non-empty; if \<open>tac\<^sub>1\<close> fails then it uses \<open>tac\<^sub>2\<close>. This is a deterministic
+ choice: if \<open>tac\<^sub>1\<close> succeeds then \<open>tac\<^sub>2\<close> is excluded
from the result.
- \<^descr> @{text "tac\<^sub>1"}~@{ML_op APPEND}~@{text "tac\<^sub>2"} concatenates the
- possible results of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike
+ \<^descr> \<open>tac\<^sub>1\<close>~@{ML_op APPEND}~\<open>tac\<^sub>2\<close> concatenates the
+ possible results of \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close>. Unlike
@{ML_op "ORELSE"} there is \<^emph>\<open>no commitment\<close> to either tactic, so
@{ML_op "APPEND"} helps to avoid incompleteness during search, at
the cost of potential inefficiencies.
- \<^descr> @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
- "tac\<^sub>1"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac\<^sub>n"}.
+ \<^descr> @{ML EVERY}~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~@{ML_op THEN}~\<open>\<dots>\<close>~@{ML_op THEN}~\<open>tac\<^sub>n\<close>.
Note that @{ML "EVERY []"} is the same as @{ML all_tac}: it always
succeeds.
- \<^descr> @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>n]"} abbreviates @{text
- "tac\<^sub>1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op "ORELSE"}~@{text
- "tac\<^sub>n"}. Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
+ \<^descr> @{ML FIRST}~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>n]\<close> abbreviates \<open>tac\<^sub>1\<close>~@{ML_op ORELSE}~\<open>\<dots>\<close>~@{ML_op "ORELSE"}~\<open>tac\<^sub>n\<close>. Note that @{ML "FIRST []"} is the same as @{ML no_tac}: it
always fails.
\<^descr> @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
- tactics with explicit subgoal addressing. So @{text
- "(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text
- "(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
+ tactics with explicit subgoal addressing. So \<open>(tac\<^sub>1\<close>~@{ML_op THEN'}~\<open>tac\<^sub>2) i\<close> is the same as \<open>(tac\<^sub>1 i\<close>~@{ML_op THEN}~\<open>tac\<^sub>2 i)\<close>.
The other primed tacticals work analogously.
\<close>
@@ -610,35 +589,33 @@
@{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
\end{mldecls}
- \<^descr> @{ML TRY}~@{text "tac"} applies @{text "tac"} to the goal
+ \<^descr> @{ML TRY}~\<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 @{text "tac"} at most
+ returns the original state. Thus, it applies \<open>tac\<close> at most
once.
Note that for tactics with subgoal addressing, the combinator can be
- applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
- "tac"}. There is no need for @{verbatim TRY'}.
+ applied via functional composition: @{ML "TRY"}~@{ML_op o}~\<open>tac\<close>. There is no need for @{verbatim TRY'}.
- \<^descr> @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the goal
+ \<^descr> @{ML REPEAT}~\<open>tac\<close> applies \<open>tac\<close> to the goal
state and, recursively, to each element of the resulting sequence.
- The resulting sequence consists of those states that make @{text
- "tac"} fail. Thus, it applies @{text "tac"} as many times as
+ The resulting sequence consists of those states that make \<open>tac\<close> fail. Thus, it applies \<open>tac\<close> as many times as
possible (including zero times), and allows backtracking over each
- invocation of @{text "tac"}. @{ML REPEAT} is more general than @{ML
+ invocation of \<open>tac\<close>. @{ML REPEAT} is more general than @{ML
REPEAT_DETERM}, but requires more space.
- \<^descr> @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"}
- but it always applies @{text "tac"} at least once, failing if this
+ \<^descr> @{ML REPEAT1}~\<open>tac\<close> is like @{ML REPEAT}~\<open>tac\<close>
+ but it always applies \<open>tac\<close> at least once, failing if this
is impossible.
- \<^descr> @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
+ \<^descr> @{ML REPEAT_DETERM}~\<open>tac\<close> applies \<open>tac\<close> to the
goal state and, recursively, to the head of the resulting sequence.
- It returns the first state to make @{text "tac"} fail. It is
+ It returns the first state to make \<open>tac\<close> fail. It is
deterministic, discarding alternative outcomes.
- \<^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 "\<infinity>"}).
+ \<^descr> @{ML REPEAT_DETERM_N}~\<open>n tac\<close> is like @{ML
+ REPEAT_DETERM}~\<open>tac\<close> but the number of repetitions is bound
+ by \<open>n\<close> (where @{ML "~1"} means \<open>\<infinity>\<close>).
\<close>
text %mlex \<open>The basic tactics and tacticals considered above follow
@@ -649,7 +626,7 @@
\<^item> @{ML no_tac} is the identity element of @{ML_op "ORELSE"} and
@{ML_op "APPEND"}. Also, it is a zero element for @{ML_op "THEN"},
- which means that @{text "tac"}~@{ML_op THEN}~@{ML no_tac} is
+ which means that \<open>tac\<close>~@{ML_op THEN}~@{ML no_tac} is
equivalent to @{ML no_tac}.
\<^item> @{ML TRY} and @{ML REPEAT} can be expressed as (recursive)
@@ -662,9 +639,9 @@
fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st;
\<close>
-text \<open>If @{text "tac"} can return multiple outcomes then so can @{ML
- REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML_op "ORELSE"} and not
- @{ML_op "APPEND"}, it applies @{text "tac"} as many times as
+text \<open>If \<open>tac\<close> can return multiple outcomes then so can @{ML
+ REPEAT}~\<open>tac\<close>. @{ML REPEAT} uses @{ML_op "ORELSE"} and not
+ @{ML_op "APPEND"}, it applies \<open>tac\<close> as many times as
possible in each outcome.
\begin{warn}
@@ -672,7 +649,7 @@
definition of @{ML REPEAT}. Recursive tacticals must be coded in
this awkward fashion to avoid infinite recursion of eager functional
evaluation in Standard ML. The following attempt would make @{ML
- REPEAT}~@{text "tac"} loop:
+ REPEAT}~\<open>tac\<close> loop:
\end{warn}
\<close>
@@ -690,9 +667,9 @@
tactic a certain range of subgoals is covered. Thus the body tactic
is applied to \<^emph>\<open>all\<close> subgoals, \<^emph>\<open>some\<close> subgoal etc.
- Suppose that the goal state has @{text "n \<ge> 0"} subgoals. Many of
+ Suppose that the goal state has \<open>n \<ge> 0\<close> subgoals. Many of
these tacticals address subgoal ranges counting downwards from
- @{text "n"} towards @{text "1"}. This has the fortunate effect that
+ \<open>n\<close> towards \<open>1\<close>. This has the fortunate effect that
newly emerging subgoals are concatenated in the result, without
interfering each other. Nonetheless, there might be situations
where a different order is desired.\<close>
@@ -708,30 +685,30 @@
@{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
\end{mldecls}
- \<^descr> @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac
- n"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op THEN}~@{text "tac 1"}. It
- applies the @{text tac} to all the subgoals, counting downwards.
+ \<^descr> @{ML ALLGOALS}~\<open>tac\<close> is equivalent to \<open>tac
+ n\<close>~@{ML_op THEN}~\<open>\<dots>\<close>~@{ML_op THEN}~\<open>tac 1\<close>. It
+ applies the \<open>tac\<close> to all the subgoals, counting downwards.
- \<^descr> @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac
- n"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}. It
- applies @{text "tac"} to one subgoal, counting downwards.
+ \<^descr> @{ML SOMEGOAL}~\<open>tac\<close> is equivalent to \<open>tac
+ n\<close>~@{ML_op ORELSE}~\<open>\<dots>\<close>~@{ML_op ORELSE}~\<open>tac 1\<close>. It
+ applies \<open>tac\<close> to one subgoal, counting downwards.
- \<^descr> @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac
- 1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}. It
- applies @{text "tac"} to one subgoal, counting upwards.
+ \<^descr> @{ML FIRSTGOAL}~\<open>tac\<close> is equivalent to \<open>tac
+ 1\<close>~@{ML_op ORELSE}~\<open>\<dots>\<close>~@{ML_op ORELSE}~\<open>tac n\<close>. It
+ applies \<open>tac\<close> to one subgoal, counting upwards.
- \<^descr> @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.
- It applies @{text "tac"} unconditionally to the first subgoal.
+ \<^descr> @{ML HEADGOAL}~\<open>tac\<close> is equivalent to \<open>tac 1\<close>.
+ It applies \<open>tac\<close> unconditionally to the first subgoal.
- \<^descr> @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or
+ \<^descr> @{ML REPEAT_SOME}~\<open>tac\<close> applies \<open>tac\<close> once or
more to a subgoal, counting downwards.
- \<^descr> @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or
+ \<^descr> @{ML REPEAT_FIRST}~\<open>tac\<close> applies \<open>tac\<close> once or
more to a subgoal, counting upwards.
- \<^descr> @{ML RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to
- @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op
- THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the
+ \<^descr> @{ML RANGE}~\<open>[tac\<^sub>1, \<dots>, tac\<^sub>k] i\<close> is equivalent to
+ \<open>tac\<^sub>k (i + k - 1)\<close>~@{ML_op THEN}~\<open>\<dots>\<close>~@{ML_op
+ THEN}~\<open>tac\<^sub>1 i\<close>. It applies the given list of tactics to the
corresponding range of subgoals, counting downwards.
\<close>
@@ -757,14 +734,14 @@
@{index_ML CHANGED: "tactic -> tactic"} \\
\end{mldecls}
- \<^descr> @{ML FILTER}~@{text "sat tac"} applies @{text "tac"} to the
+ \<^descr> @{ML FILTER}~\<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 @{text "sat"}.
+ states that are satisfactory in the sense of \<open>sat\<close>.
- \<^descr> @{ML CHANGED}~@{text "tac"} applies @{text "tac"} to the goal
+ \<^descr> @{ML CHANGED}~\<open>tac\<close> applies \<open>tac\<close> to the goal
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.
+ CHANGED}~\<open>tac\<close> always has some effect on the state.
\<close>
@@ -777,17 +754,17 @@
@{index_ML DEPTH_SOLVE_1: "tactic -> tactic"} \\
\end{mldecls}
- \<^descr> @{ML DEPTH_FIRST}~@{text "sat tac"} returns the goal state if
- @{text "sat"} returns true. Otherwise it applies @{text "tac"},
+ \<^descr> @{ML DEPTH_FIRST}~\<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 applying
- @{text "tac"}~@{ML_op THEN}~@{ML DEPTH_FIRST}~@{text "sat tac"} to
+ \<open>tac\<close>~@{ML_op THEN}~@{ML DEPTH_FIRST}~\<open>sat tac\<close> to
the state.
- \<^descr> @{ML DEPTH_SOLVE}@{text "tac"} uses @{ML DEPTH_FIRST} to
+ \<^descr> @{ML DEPTH_SOLVE}\<open>tac\<close> uses @{ML DEPTH_FIRST} to
search for states having no subgoals.
- \<^descr> @{ML DEPTH_SOLVE_1}~@{text "tac"} uses @{ML DEPTH_FIRST} to
+ \<^descr> @{ML DEPTH_SOLVE_1}~\<open>tac\<close> uses @{ML DEPTH_FIRST} to
search for states having fewer subgoals than the given state. Thus,
it insists upon solving at least one subgoal.
\<close>
@@ -804,16 +781,16 @@
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 @{text "tac"}.
+ the first satisfactory result from \<open>tac\<close>.
- \<^descr> @{ML BREADTH_FIRST}~@{text "sat tac"} uses breadth-first
- search to find states for which @{text "sat"} is true. For most
+ \<^descr> @{ML BREADTH_FIRST}~\<open>sat tac\<close> uses breadth-first
+ search to find states for which \<open>sat\<close> is true. For most
applications, it is too slow.
- \<^descr> @{ML BEST_FIRST}~@{text "(sat, dist) tac"} does a heuristic
- search, using @{text "dist"} to estimate the distance from a
- satisfactory state (in the sense of @{text "sat"}). It maintains a
- list of states ordered by distance. It applies @{text "tac"} to the
+ \<^descr> @{ML BEST_FIRST}~\<open>(sat, dist) tac\<close> does a heuristic
+ search, using \<open>dist\<close> to estimate the distance from a
+ satisfactory state (in the sense of \<open>sat\<close>). It maintains a
+ list of states ordered by distance. It applies \<open>tac\<close> to the
head of this list; if the result contains any satisfactory states,
then it returns them. Otherwise, @{ML BEST_FIRST} adds the new
states to the list, and continues.
@@ -822,9 +799,9 @@
the size of the state. The smaller the state, the fewer and simpler
subgoals it has.
- \<^descr> @{ML THEN_BEST_FIRST}~@{text "tac\<^sub>0 (sat, dist) tac"} is like
+ \<^descr> @{ML THEN_BEST_FIRST}~\<open>tac\<^sub>0 (sat, dist) tac\<close> is like
@{ML BEST_FIRST}, except that the priority queue initially contains
- the result of applying @{text "tac\<^sub>0"} to the goal state. This
+ the result of applying \<open>tac\<^sub>0\<close> to the goal state. This
tactical permits separate tactics for starting the search and
continuing the search.
\<close>
@@ -840,22 +817,22 @@
@{index_ML DETERM: "tactic -> tactic"} \\
\end{mldecls}
- \<^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
- @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} is applied to a goal state.
- However, both @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"} are evaluated
+ \<^descr> @{ML COND}~\<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, both \<open>tac\<^sub>1\<close> and \<open>tac\<^sub>2\<close> are evaluated
because ML uses eager evaluation.
- \<^descr> @{ML IF_UNSOLVED}~@{text "tac"} applies @{text "tac"} to the
+ \<^descr> @{ML IF_UNSOLVED}~\<open>tac\<close> applies \<open>tac\<close> to the
goal state if it has any subgoals, and simply returns the goal state
otherwise. Many common tactics, such as @{ML resolve_tac}, fail if
applied to a goal state that has no subgoals.
- \<^descr> @{ML SOLVE}~@{text "tac"} applies @{text "tac"} to the goal
+ \<^descr> @{ML SOLVE}~\<open>tac\<close> applies \<open>tac\<close> to the goal
state and then fails iff there are subgoals left.
- \<^descr> @{ML DETERM}~@{text "tac"} applies @{text "tac"} to the goal
+ \<^descr> @{ML DETERM}~\<open>tac\<close> applies \<open>tac\<close> to the goal
state and returns the head of the resulting sequence. @{ML DETERM}
limits the search space by making its argument deterministic.
\<close>
@@ -871,20 +848,17 @@
@{index_ML size_of_thm: "thm -> int"} \\
\end{mldecls}
- \<^descr> @{ML has_fewer_prems}~@{text "n thm"} reports whether @{text
- "thm"} has fewer than @{text "n"} premises.
+ \<^descr> @{ML has_fewer_prems}~\<open>n thm\<close> reports whether \<open>thm\<close> has fewer than \<open>n\<close> premises.
- \<^descr> @{ML Thm.eq_thm}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether @{text
- "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal. Both theorems must have the
+ \<^descr> @{ML Thm.eq_thm}~\<open>(thm\<^sub>1, thm\<^sub>2)\<close> reports whether \<open>thm\<^sub>1\<close> and \<open>thm\<^sub>2\<close> are equal. Both theorems must have the
same conclusions, the same set of hypotheses, and the same set of sort
hypotheses. Names of bound variables are ignored as usual.
- \<^descr> @{ML Thm.eq_thm_prop}~@{text "(thm\<^sub>1, thm\<^sub>2)"} reports whether
- the propositions of @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} are equal.
+ \<^descr> @{ML Thm.eq_thm_prop}~\<open>(thm\<^sub>1, thm\<^sub>2)\<close> reports whether
+ the propositions of \<open>thm\<^sub>1\<close> and \<open>thm\<^sub>2\<close> are equal.
Names of bound variables are ignored.
- \<^descr> @{ML size_of_thm}~@{text "thm"} computes the size of @{text
- "thm"}, namely the number of variables, constants and abstractions
+ \<^descr> @{ML size_of_thm}~\<open>thm\<close> computes the size of \<open>thm\<close>, namely the number of variables, constants and abstractions
in its conclusion. It may serve as a distance function for
@{ML BEST_FIRST}.
\<close>