--- a/doc-src/IsarRef/Thy/Generic.thy Sat Jun 11 15:03:31 2011 +0200
+++ b/doc-src/IsarRef/Thy/Generic.thy Sat Jun 11 15:36:46 2011 +0200
@@ -1068,13 +1068,8 @@
\item @{method safe} repeatedly performs safe steps on all subgoals.
It is deterministic, with at most one outcome.
- \item @{method clarify} performs a series of safe steps as follows.
-
- No splitting step is applied; for example, the subgoal @{text "A \<and>
- B"} is left as a conjunction. Proof by assumption, Modus Ponens,
- etc., may be performed provided they do not instantiate unknowns.
- Assumptions of the form @{text "x = t"} may be eliminated. The safe
- wrapper tactical is applied.
+ \item @{method clarify} performs a series of safe steps without
+ splitting subgoals; see also @{ML clarify_step_tac}.
\item @{method clarsimp} acts like @{method clarify}, but also does
simplification. Note that if the Simplifier context includes a
@@ -1084,6 +1079,52 @@
*}
+subsection {* Single-step tactics *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{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}
+
+ These are the primitive tactics behind the (semi)automated proof
+ methods of the Classical Reasoner. By calling them yourself, you
+ can execute these procedures one step at a time.
+
+ \begin{description}
+
+ \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
+ subgoal @{text i}. The safe wrapper tacticals are applied to a
+ tactic that may include proof by assumption or Modus Ponens (taking
+ care not to instantiate unknowns), or substitution.
+
+ \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
+ unknowns to be instantiated.
+
+ \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
+ procedure. The unsafe wrapper tacticals are applied to a tactic
+ that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
+ rule from the context.
+
+ \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
+ backtracking between using safe rules with instantiation (@{ML
+ inst_step_tac}) and using unsafe rules. The resulting search space
+ is larger.
+
+ \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
+ on subgoal @{text i}. No splitting step is applied; for example,
+ the subgoal @{text "A \<and> B"} is left as a conjunction. Proof by
+ assumption, Modus Ponens, etc., may be performed provided they do
+ not instantiate unknowns. Assumptions of the form @{text "x = t"}
+ may be eliminated. The safe wrapper tactical is applied.
+
+ \end{description}
+*}
+
+
section {* Object-logic setup \label{sec:object-logic} *}
text {*
--- a/doc-src/IsarRef/Thy/document/Generic.tex Sat Jun 11 15:03:31 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Sat Jun 11 15:36:46 2011 +0200
@@ -1656,12 +1656,8 @@
\item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
It is deterministic, with at most one outcome.
- \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
-
- No splitting step is applied; for example, the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction. Proof by assumption, Modus Ponens,
- etc., may be performed provided they do not instantiate unknowns.
- Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated. The safe
- wrapper tactical is applied.
+ \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
+ splitting subgoals; see also \verb|clarify_step_tac|.
\item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
simplification. Note that if the Simplifier context includes a
@@ -1671,6 +1667,53 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Single-step tactics%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
+ \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
+ \end{matharray}
+
+ These are the primitive tactics behind the (semi)automated proof
+ methods of the Classical Reasoner. By calling them yourself, you
+ can execute these procedures one step at a time.
+
+ \begin{description}
+
+ \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
+ subgoal \isa{i}. The safe wrapper tacticals are applied to a
+ tactic that may include proof by assumption or Modus Ponens (taking
+ care not to instantiate unknowns), or substitution.
+
+ \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
+ unknowns to be instantiated.
+
+ \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
+ procedure. The unsafe wrapper tacticals are applied to a tactic
+ that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
+ rule from the context.
+
+ \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
+ backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules. The resulting search space
+ is larger.
+
+ \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
+ on subgoal \isa{i}. No splitting step is applied; for example,
+ the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction. Proof by
+ assumption, Modus Ponens, etc., may be performed provided they do
+ not instantiate unknowns. Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
+ may be eliminated. The safe wrapper tactical is applied.
+
+ \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsection{Object-logic setup \label{sec:object-logic}%
}
\isamarkuptrue%
--- a/doc-src/Ref/classical.tex Sat Jun 11 15:03:31 2011 +0200
+++ b/doc-src/Ref/classical.tex Sat Jun 11 15:36:46 2011 +0200
@@ -125,21 +125,6 @@
\section{The classical tactics}
-\subsection{Semi-automatic tactics}
-\begin{ttbox}
-clarify_step_tac : claset -> int -> tactic
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
- subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
- B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
- performed provided they do not instantiate unknowns. Assumptions of the
- form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
- applied.
-\end{ttdescription}
-
-
\subsection{Other classical tactics}
\begin{ttbox}
slow_best_tac : claset -> int -> tactic
@@ -173,36 +158,6 @@
\end{ttdescription}
-\subsection{Single-step tactics}
-\begin{ttbox}
-safe_step_tac : claset -> int -> tactic
-inst_step_tac : claset -> int -> tactic
-step_tac : claset -> int -> tactic
-slow_step_tac : claset -> int -> tactic
-\end{ttbox}
-The automatic proof procedures call these tactics. By calling them
-yourself, you can execute these procedures one step at a time.
-\begin{ttdescription}
-\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
- subgoal~$i$. The safe wrapper tacticals are applied to a tactic that may
- include proof by assumption or Modus Ponens (taking care not to instantiate
- unknowns), or substitution.
-
-\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
-but allows unknowns to be instantiated.
-
-\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
- procedure. The unsafe wrapper tacticals are applied to a tactic that tries
- \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
- from~$cs$.
-
-\item[\ttindexbold{slow_step_tac}]
- resembles \texttt{step_tac}, but allows backtracking between using safe
- rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
- The resulting search space is larger.
-\end{ttdescription}
-
-
\subsection{Other useful tactics}
\index{tactics!for contradiction}
\index{tactics!for Modus Ponens}