summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Doc/IsarRef/Generic.thy

changeset 50071 | 959548c3b947 |

parent 50070 | e447ad4d6edd |

child 50075 | ceb877c315a1 |

--- a/src/Doc/IsarRef/Generic.thy Sun Nov 04 20:23:26 2012 +0100 +++ b/src/Doc/IsarRef/Generic.thy Wed Nov 07 12:14:38 2012 +0100 @@ -1362,13 +1362,13 @@ subsection {* Single-step tactics *} text {* - \begin{matharray}{rcl} + \begin{mldecls} @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\ @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\ @{index_ML step_tac: "Proof.context -> int -> tactic"} \\ @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\ @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\ - \end{matharray} + \end{mldecls} These are the primitive tactics behind the automated proof methods of the Classical Reasoner. By calling them yourself, you can @@ -1405,6 +1405,94 @@ *} +subsection {* Modifying the search step *} + +text {* + \begin{mldecls} + @{index_ML_type wrapper: "(int -> tactic) -> (int -> tactic)"} \\[0.5ex] + @{index_ML_op addSWrapper: "claset * (string * (Proof.context -> wrapper)) + -> claset"} \\ + @{index_ML_op addSbefore: "claset * (string * (int -> tactic)) -> claset"} \\ + @{index_ML_op addSafter: "claset * (string * (int -> tactic)) -> claset"} \\ + @{index_ML_op delSWrapper: "claset * string -> claset"} \\[0.5ex] + @{index_ML_op addWrapper: "claset * (string * (Proof.context -> wrapper)) + -> claset"} \\ + @{index_ML_op addbefore: "claset * (string * (int -> tactic)) -> claset"} \\ + @{index_ML_op addafter: "claset * (string * (int -> tactic)) -> claset"} \\ + @{index_ML_op delWrapper: "claset * string -> claset"} \\[0.5ex] + @{index_ML addSss: "Proof.context -> Proof.context"} \\ + @{index_ML addss: "Proof.context -> Proof.context"} \\ + \end{mldecls} + + The proof strategy of the Classical Reasoner is simple. Perform as + many safe inferences as possible; or else, apply certain safe rules, + allowing instantiation of unknowns; or else, apply an unsafe rule. + The tactics also eliminate assumptions of the form @{text "x = t"} + by substitution if they have been set up to do so. They may perform + a form of Modus Ponens: if there are assumptions @{text "P \<longrightarrow> Q"} and + @{text "P"}, then replace @{text "P \<longrightarrow> Q"} by @{text "Q"}. + + The classical reasoning tools --- except @{method blast} --- allow + to modify this basic proof strategy by applying two lists of + arbitrary \emph{wrapper tacticals} to it. The first wrapper list, + which is considered to contain safe wrappers only, affects @{ML + safe_step_tac} and all the tactics that call it. The second one, + which may contain unsafe wrappers, affects the unsafe parts of @{ML + step_tac}, @{ML slow_step_tac}, and the tactics that call them. A + wrapper transforms each step of the search, for example by + attempting other tactics before or after the original step tactic. + All members of a wrapper list are applied in turn to the respective + step tactic. + + Initially the two wrapper lists are empty, which means no + modification of the step tactics. Safe and unsafe wrappers are added + to a claset with the functions given below, supplying them with + wrapper names. These names may be used to selectively delete + wrappers. + + \begin{description} + + \item @{text "cs addSWrapper (name, wrapper)"} adds a new wrapper, + which should yield a safe tactic, to modify the existing safe step + tactic. + + \item @{text "cs addSbefore (name, tac)"} adds the given tactic as a + safe wrapper, such that it is tried \emph{before} each safe step of + the search. + + \item @{text "cs addSafter (name, tac)"} adds the given tactic as a + safe wrapper, such that it is tried when a safe step of the search + would fail. + + \item @{text "cs delSWrapper name"} deletes the safe wrapper with + the given name. + + \item @{text "cs addWrapper (name, wrapper)"} adds a new wrapper to + modify the existing (unsafe) step tactic. + + \item @{text "cs addbefore (name, tac)"} adds the given tactic as an + unsafe wrapper, such that it its result is concatenated + \emph{before} the result of each unsafe step. + + \item @{text "cs addafter (name, tac)"} adds the given tactic as an + unsafe wrapper, such that it its result is concatenated \emph{after} + the result of each unsafe step. + + \item @{text "cs delWrapper name"} deletes the unsafe wrapper with + the given name. + + \item @{text "addSss"} adds the simpset of the context to its + classical set. The assumptions and goal will be simplified, in a + rather safe way, after each safe step of the search. + + \item @{text "addss"} adds the simpset of the context to its + classical set. The assumptions and goal will be simplified, before + the each unsafe step of the search. + + \end{description} +*} + + section {* Object-logic setup \label{sec:object-logic} *} text {*