--- a/src/Doc/IsarRef/ML_Tactic.thy Sat Apr 05 17:52:29 2014 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,177 +0,0 @@
-theory ML_Tactic
-imports Base Main
-begin
-
-chapter {* ML tactic expressions *}
-
-text {*
- Isar Proof methods closely resemble traditional tactics, when used
- in unstructured sequences of @{command "apply"} commands.
- Isabelle/Isar provides emulations for all major ML tactics of
- classic Isabelle --- mostly for the sake of easy porting of existing
- developments, as actual Isar proof texts would demand much less
- diversity of proof methods.
-
- Unlike tactic expressions in ML, Isar proof methods provide proper
- concrete syntax for additional arguments, options, modifiers etc.
- Thus a typical method text is usually more concise than the
- corresponding ML tactic. Furthermore, the Isar versions of classic
- Isabelle tactics often cover several variant forms by a single
- method with separate options to tune the behavior. For example,
- method @{method simp} replaces all of @{ML simp_tac}~/ @{ML
- asm_simp_tac}~/ @{ML full_simp_tac}~/ @{ML asm_full_simp_tac}, there
- is also concrete syntax for augmenting the Simplifier context (the
- current ``simpset'') in a convenient way.
-*}
-
-
-section {* Resolution tactics *}
-
-text {*
- Classic Isabelle provides several variant forms of tactics for
- single-step rule applications (based on higher-order resolution).
- The space of resolution tactics has the following main dimensions.
-
- \begin{enumerate}
-
- \item The ``mode'' of resolution: intro, elim, destruct, or forward
- (e.g.\ @{ML resolve_tac}, @{ML eresolve_tac}, @{ML dresolve_tac},
- @{ML forward_tac}).
-
- \item Optional explicit instantiation (e.g.\ @{ML resolve_tac} vs.\
- @{ML res_inst_tac}).
-
- \item Abbreviations for singleton arguments (e.g.\ @{ML resolve_tac}
- vs.\ @{ML rtac}).
-
- \end{enumerate}
-
- Basically, the set of Isar tactic emulations @{method rule_tac},
- @{method erule_tac}, @{method drule_tac}, @{method frule_tac} (see
- \secref{sec:tactics}) would be sufficient to cover the four modes,
- either with or without instantiation, and either with single or
- multiple arguments. Although it is more convenient in most cases to
- use the plain @{method_ref (Pure) rule} method, or any of its
- ``improper'' variants @{method erule}, @{method drule}, @{method
- frule}. Note that explicit goal addressing is only supported by the
- actual @{method rule_tac} version.
-
- With this in mind, plain resolution tactics correspond to Isar
- methods as follows.
-
- \medskip
- \begin{tabular}{lll}
- @{ML rtac}~@{text "a 1"} & & @{text "rule a"} \\
- @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] 1"} & & @{text "rule a\<^sub>1 \<dots>"} \\
- @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a 1"} & &
- @{text "rule_tac x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\[0.5ex]
- @{ML rtac}~@{text "a i"} & & @{text "rule_tac [i] a"} \\
- @{ML resolve_tac}~@{text "[a\<^sub>1, \<dots>] i"} & & @{text "rule_tac [i] a\<^sub>1 \<dots>"} \\
- @{ML res_inst_tac}~@{text "ctxt [(x\<^sub>1, t\<^sub>1), \<dots>] a i"} & &
- @{text "rule_tac [i] x\<^sub>1 = t\<^sub>1 \<AND> \<dots> \<IN> a"} \\
- \end{tabular}
- \medskip
-
- Note that explicit goal addressing may be usually avoided by
- changing the order of subgoals with @{command "defer"} or @{command
- "prefer"} (see \secref{sec:tactic-commands}).
-*}
-
-
-section {* Simplifier tactics *}
-
-text {* The main Simplifier tactics @{ML simp_tac} and variants are
- all covered by the @{method simp} and @{method simp_all} methods
- (see \secref{sec:simplifier}). Note that there is no individual
- goal addressing available, simplification acts either on the first
- goal (@{method simp}) or all goals (@{method simp_all}).
-
- \medskip
- \begin{tabular}{lll}
- @{ML asm_full_simp_tac}~@{text "@{context} 1"} & & @{method simp} \\
- @{ML ALLGOALS}~(@{ML asm_full_simp_tac}~@{text "@{context}"}) & & @{method simp_all} \\[0.5ex]
- @{ML simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm)"} \\
- @{ML asm_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_simp)"} \\
- @{ML full_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(no_asm_use)"} \\
- @{ML asm_lr_simp_tac}~@{text "@{context} 1"} & & @{method simp}~@{text "(asm_lr)"} \\
- \end{tabular}
- \medskip
-*}
-
-
-section {* Classical Reasoner tactics *}
-
-text {* The Classical Reasoner provides a rather large number of
- variations of automated tactics, such as @{ML blast_tac}, @{ML
- fast_tac}, @{ML clarify_tac} etc. The corresponding Isar methods
- usually share the same base name, such as @{method blast}, @{method
- fast}, @{method clarify} etc.\ (see \secref{sec:classical}). *}
-
-
-section {* Miscellaneous tactics *}
-
-text {*
- There are a few additional tactics defined in various theories of
- Isabelle/HOL, some of these also in Isabelle/FOL or Isabelle/ZF.
- The most common ones of these may be ported to Isar as follows.
-
- \medskip
- \begin{tabular}{lll}
- @{ML stac}~@{text "a 1"} & & @{text "subst a"} \\
- @{ML hyp_subst_tac}~@{text 1} & & @{text hypsubst} \\
- @{ML split_all_tac}~@{text 1} & & @{text "simp (no_asm_simp) only: split_tupled_all"} \\
- & @{text "\<approx>"} & @{text "simp only: split_tupled_all"} \\
- & @{text "\<lless>"} & @{text "clarify"} \\
- \end{tabular}
-*}
-
-
-section {* Tacticals *}
-
-text {*
- Classic Isabelle provides a huge amount of tacticals for combination
- and modification of existing tactics. This has been greatly reduced
- in Isar, providing the bare minimum of combinators only: ``@{text
- ","}'' (sequential composition), ``@{text "|"}'' (alternative
- choices), ``@{text "?"}'' (try), ``@{text "+"}'' (repeat at least
- once). These are usually sufficient in practice; if all fails,
- arbitrary ML tactic code may be invoked via the @{method tactic}
- method (see \secref{sec:tactics}).
-
- \medskip Common ML tacticals may be expressed directly in Isar as
- follows:
-
- \medskip
- \begin{tabular}{lll}
- @{text "tac\<^sub>1"}~@{ML_text THEN}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1, meth\<^sub>2"} \\
- @{text "tac\<^sub>1"}~@{ML_text ORELSE}~@{text "tac\<^sub>2"} & & @{text "meth\<^sub>1 | meth\<^sub>2"} \\
- @{ML TRY}~@{text tac} & & @{text "meth?"} \\
- @{ML REPEAT1}~@{text tac} & & @{text "meth+"} \\
- @{ML REPEAT}~@{text tac} & & @{text "(meth+)?"} \\
- @{ML EVERY}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1, \<dots>"} \\
- @{ML FIRST}~@{text "[tac\<^sub>1, \<dots>]"} & & @{text "meth\<^sub>1 | \<dots>"} \\
- \end{tabular}
- \medskip
-
- \medskip @{ML CHANGED} (see \cite{isabelle-implementation}) is
- usually not required in Isar, since most basic proof methods already
- fail unless there is an actual change in the goal state.
- Nevertheless, ``@{text "?"}'' (try) may be used to accept
- \emph{unchanged} results as well.
-
- \medskip @{ML ALLGOALS}, @{ML SOMEGOAL} etc.\ (see
- \cite{isabelle-implementation}) are not available in Isar, since
- there is no direct goal addressing. Nevertheless, some basic
- methods address all goals internally, notably @{method simp_all}
- (see \secref{sec:simplifier}). Also note that @{ML ALLGOALS} can be
- often replaced by ``@{text "+"}'' (repeat at least once), although
- this usually has a different operational behavior: subgoals are
- solved in a different order.
-
- \medskip Iterated resolution, such as
- @{ML_text "REPEAT (FIRSTGOAL (resolve_tac ...))"}, is usually better
- expressed using the @{method intro} and @{method elim} methods of
- Isar (see \secref{sec:classical}).
-*}
-
-end