1.1 --- a/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:23:26 2012 +0100
1.2 +++ b/src/Doc/IsarRef/Generic.thy Wed Nov 07 12:14:38 2012 +0100
1.3 @@ -1362,13 +1362,13 @@
1.4 subsection {* Single-step tactics *}
1.5
1.6 text {*
1.7 - \begin{matharray}{rcl}
1.8 + \begin{mldecls}
1.9 @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
1.10 @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
1.11 @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
1.12 @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
1.13 @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
1.14 - \end{matharray}
1.15 + \end{mldecls}
1.16
1.17 These are the primitive tactics behind the automated proof methods
1.18 of the Classical Reasoner. By calling them yourself, you can
1.19 @@ -1405,6 +1405,94 @@
1.20 *}
1.21
1.22
1.23 +subsection {* Modifying the search step *}
1.24 +
1.25 +text {*
1.26 + \begin{mldecls}
1.27 + @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex]
1.28 + @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper))
1.29 + -> claset"} \\
1.30 + @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\
1.31 + @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\
1.32 + @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex]
1.33 + @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper))
1.34 + -> claset"} \\
1.35 + @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\
1.36 + @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\
1.37 + @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex]
1.38 + @{index_ML addSss: "Proof.context -> Proof.context"} \\
1.39 + @{index_ML addss: "Proof.context -> Proof.context"} \\
1.40 + \end{mldecls}
1.41 +
1.42 + The proof strategy of the Classical Reasoner is simple. Perform as
1.43 + many safe inferences as possible; or else, apply certain safe rules,
1.44 + allowing instantiation of unknowns; or else, apply an unsafe rule.
1.45 + The tactics also eliminate assumptions of the form @{text "x = t"}
1.46 + by substitution if they have been set up to do so. They may perform
1.47 + a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and
1.48 + @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}.
1.49 +
1.50 + The classical reasoning tools --- except @{method blast} --- allow
1.51 + to modify this basic proof strategy by applying two lists of
1.52 + arbitrary \emph{wrapper tacticals} to it. The first wrapper list,
1.53 + which is considered to contain safe wrappers only, affects @{ML
1.54 + safe_step_tac} and all the tactics that call it. The second one,
1.55 + which may contain unsafe wrappers, affects the unsafe parts of @{ML
1.56 + step_tac}, @{ML slow_step_tac}, and the tactics that call them. A
1.57 + wrapper transforms each step of the search, for example by
1.58 + attempting other tactics before or after the original step tactic.
1.59 + All members of a wrapper list are applied in turn to the respective
1.60 + step tactic.
1.61 +
1.62 + Initially the two wrapper lists are empty, which means no
1.63 + modification of the step tactics. Safe and unsafe wrappers are added
1.64 + to a claset with the functions given below, supplying them with
1.65 + wrapper names. These names may be used to selectively delete
1.66 + wrappers.
1.67 +
1.68 + \begin{description}
1.69 +
1.70 + \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper,
1.71 + which should yield a safe tactic, to modify the existing safe step
1.72 + tactic.
1.73 +
1.74 + \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a
1.75 + safe wrapper, such that it is tried \emph{before} each safe step of
1.76 + the search.
1.77 +
1.78 + \item @{text "cs addSafter (name, tac)"} adds the given tactic as a
1.79 + safe wrapper, such that it is tried when a safe step of the search
1.80 + would fail.
1.81 +
1.82 + \item @{text "cs delSWrapper name"} deletes the safe wrapper with
1.83 + the given name.
1.84 +
1.85 + \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to
1.86 + modify the existing (unsafe) step tactic.
1.87 +
1.88 + \item @{text "cs addbefore (name, tac)"} adds the given tactic as an
1.89 + unsafe wrapper, such that it its result is concatenated
1.90 + \emph{before} the result of each unsafe step.
1.91 +
1.92 + \item @{text "cs addafter (name, tac)"} adds the given tactic as an
1.93 + unsafe wrapper, such that it its result is concatenated \emph{after}
1.94 + the result of each unsafe step.
1.95 +
1.96 + \item @{text "cs delWrapper name"} deletes the unsafe wrapper with
1.97 + the given name.
1.98 +
1.99 + \item @{text "addSss"} adds the simpset of the context to its
1.100 + classical set. The assumptions and goal will be simplified, in a
1.101 + rather safe way, after each safe step of the search.
1.102 +
1.103 + \item @{text "addss"} adds the simpset of the context to its
1.104 + classical set. The assumptions and goal will be simplified, before
1.105 + the each unsafe step of the search.
1.106 +
1.107 + \end{description}
1.108 +*}
1.109 +
1.110 +
1.111 section {* Object-logic setup \label{sec:object-logic} *}
1.112
1.113 text {*