--- a/src/Doc/Isar_Ref/Generic.thy Mon Jun 15 13:29:57 2015 +0200
+++ b/src/Doc/Isar_Ref/Generic.thy Mon Jun 15 14:10:41 2015 +0200
@@ -255,120 +255,6 @@
\<close>
-subsection \<open>Further tactic emulations \label{sec:tactics}\<close>
-
-text \<open>
- The following improper proof methods emulate traditional tactics.
- These admit direct access to the goal state, which is normally
- considered harmful! In particular, this may involve both numbered
- goal addressing (default 1), and dynamic instantiation within the
- scope of some subgoal.
-
- \begin{warn}
- Dynamic instantiations refer to universally quantified parameters
- of a subgoal (the dynamic context) rather than fixed variables and
- term abbreviations of a (static) Isar context.
- \end{warn}
-
- Tactic emulation methods, unlike their ML counterparts, admit
- simultaneous instantiation from both dynamic and static contexts.
- If names occur in both contexts goal parameters hide locally fixed
- variables. Likewise, schematic variables refer to term
- abbreviations, if present in the static context. Otherwise the
- schematic variable is interpreted as a schematic variable and left
- to be solved by unification with certain parts of the subgoal.
-
- Note that the tactic emulation proof methods in Isabelle/Isar are
- consistently named @{text foo_tac}. Note also that variable names
- occurring on left hand sides of instantiations must be preceded by a
- question mark if they coincide with a keyword or contain dots. This
- is consistent with the attribute @{attribute "where"} (see
- \secref{sec:pure-meth-att}).
-
- \begin{matharray}{rcl}
- @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
- @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
- \end{matharray}
-
- @{rail \<open>
- (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
- @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
- (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
- ;
- @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
- ;
- @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
- ;
- @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
- ;
- @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
- ;
- (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
- \<close>}
-
-\begin{description}
-
- \item @{method rule_tac} etc. do resolution of rules with explicit
- instantiation. This works the same way as the ML tactics @{ML
- Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
-
- Multiple rules may be only given if there is no instantiation; then
- @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
- @{cite "isabelle-implementation"}).
-
- \item @{method cut_tac} inserts facts into the proof state as
- assumption of a subgoal; instantiations may be given as well. Note
- that the scope of schematic variables is spread over the main goal
- statement and rule premises are turned into new subgoals. This is
- in contrast to the regular method @{method insert} which inserts
- closed rule statements.
-
- \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
- from a subgoal. Note that @{text \<phi>} 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.
-
- \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
- @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
- as new subgoals (in the original context).
-
- \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
- goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
- \emph{suffix} of variables.
-
- \item @{method rotate_tac}~@{text n} rotates the premises of a
- subgoal by @{text n} positions: from right to left if @{text n} is
- positive, and from left to right if @{text n} is negative; the
- default value is 1.
-
- \item @{method tactic}~@{text "text"} produces a proof method from
- any ML text of type @{ML_type tactic}. Apart from the usual ML
- environment and the current proof context, the ML code may refer to
- the locally bound values @{ML_text facts}, which indicates any
- current facts used for forward-chaining.
-
- \item @{method raw_tactic} is similar to @{method tactic}, but
- presents the goal state in its raw internal form, where simultaneous
- subgoals appear as conjunction of the logical framework instead of
- the usual split into several subgoals. While feature this is useful
- for debugging of complex method definitions, it should not never
- appear in production theories.
-
- \end{description}
-\<close>
-
-
section \<open>The Simplifier \label{sec:simplifier}\<close>
text \<open>The Simplifier performs conditional and unconditional