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 {*