moved/updated single-step tactics;
authorwenzelm
Sat Jun 11 15:36:46 2011 +0200 (2011-06-11)
changeset 433669cbcab5c780a
parent 43365 f8944cb2468f
child 43367 3f1469de9e47
moved/updated single-step tactics;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/document/Generic.tex
doc-src/Ref/classical.tex
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:03:31 2011 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Sat Jun 11 15:36:46 2011 +0200
     1.3 @@ -1068,13 +1068,8 @@
     1.4    \item @{method safe} repeatedly performs safe steps on all subgoals.
     1.5    It is deterministic, with at most one outcome.
     1.6  
     1.7 -  \item @{method clarify} performs a series of safe steps as follows.
     1.8 -
     1.9 -  No splitting step is applied; for example, the subgoal @{text "A \<and>
    1.10 -  B"} is left as a conjunction.  Proof by assumption, Modus Ponens,
    1.11 -  etc., may be performed provided they do not instantiate unknowns.
    1.12 -  Assumptions of the form @{text "x = t"} may be eliminated.  The safe
    1.13 -  wrapper tactical is applied.
    1.14 +  \item @{method clarify} performs a series of safe steps without
    1.15 +  splitting subgoals; see also @{ML clarify_step_tac}.
    1.16  
    1.17    \item @{method clarsimp} acts like @{method clarify}, but also does
    1.18    simplification.  Note that if the Simplifier context includes a
    1.19 @@ -1084,6 +1079,52 @@
    1.20  *}
    1.21  
    1.22  
    1.23 +subsection {* Single-step tactics *}
    1.24 +
    1.25 +text {*
    1.26 +  \begin{matharray}{rcl}
    1.27 +    @{index_ML safe_step_tac: "Proof.context -> int -> tactic"} \\
    1.28 +    @{index_ML inst_step_tac: "Proof.context -> int -> tactic"} \\
    1.29 +    @{index_ML step_tac: "Proof.context -> int -> tactic"} \\
    1.30 +    @{index_ML slow_step_tac: "Proof.context -> int -> tactic"} \\
    1.31 +    @{index_ML clarify_step_tac: "Proof.context -> int -> tactic"} \\
    1.32 +  \end{matharray}
    1.33 +
    1.34 +  These are the primitive tactics behind the (semi)automated proof
    1.35 +  methods of the Classical Reasoner.  By calling them yourself, you
    1.36 +  can execute these procedures one step at a time.
    1.37 +
    1.38 +  \begin{description}
    1.39 +
    1.40 +  \item @{ML safe_step_tac}~@{text "ctxt i"} performs a safe step on
    1.41 +  subgoal @{text i}.  The safe wrapper tacticals are applied to a
    1.42 +  tactic that may include proof by assumption or Modus Ponens (taking
    1.43 +  care not to instantiate unknowns), or substitution.
    1.44 +
    1.45 +  \item @{ML inst_step_tac} is like @{ML safe_step_tac}, but allows
    1.46 +  unknowns to be instantiated.
    1.47 +
    1.48 +  \item @{ML step_tac}~@{text "ctxt i"} is the basic step of the proof
    1.49 +  procedure.  The unsafe wrapper tacticals are applied to a tactic
    1.50 +  that tries @{ML safe_tac}, @{ML inst_step_tac}, or applies an unsafe
    1.51 +  rule from the context.
    1.52 +
    1.53 +  \item @{ML slow_step_tac} resembles @{ML step_tac}, but allows
    1.54 +  backtracking between using safe rules with instantiation (@{ML
    1.55 +  inst_step_tac}) and using unsafe rules.  The resulting search space
    1.56 +  is larger.
    1.57 +
    1.58 +  \item @{ML clarify_step_tac}~@{text "ctxt i"} performs a safe step
    1.59 +  on subgoal @{text i}.  No splitting step is applied; for example,
    1.60 +  the subgoal @{text "A \<and> B"} is left as a conjunction.  Proof by
    1.61 +  assumption, Modus Ponens, etc., may be performed provided they do
    1.62 +  not instantiate unknowns.  Assumptions of the form @{text "x = t"}
    1.63 +  may be eliminated.  The safe wrapper tactical is applied.
    1.64 +
    1.65 +  \end{description}
    1.66 +*}
    1.67 +
    1.68 +
    1.69  section {* Object-logic setup \label{sec:object-logic} *}
    1.70  
    1.71  text {*
     2.1 --- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:03:31 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 11 15:36:46 2011 +0200
     2.3 @@ -1656,12 +1656,8 @@
     2.4    \item \hyperlink{method.safe}{\mbox{\isa{safe}}} repeatedly performs safe steps on all subgoals.
     2.5    It is deterministic, with at most one outcome.
     2.6  
     2.7 -  \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps as follows.
     2.8 -
     2.9 -  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,
    2.10 -  etc., may be performed provided they do not instantiate unknowns.
    2.11 -  Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}} may be eliminated.  The safe
    2.12 -  wrapper tactical is applied.
    2.13 +  \item \hyperlink{method.clarify}{\mbox{\isa{clarify}}} performs a series of safe steps without
    2.14 +  splitting subgoals; see also \verb|clarify_step_tac|.
    2.15  
    2.16    \item \hyperlink{method.clarsimp}{\mbox{\isa{clarsimp}}} acts like \hyperlink{method.clarify}{\mbox{\isa{clarify}}}, but also does
    2.17    simplification.  Note that if the Simplifier context includes a
    2.18 @@ -1671,6 +1667,53 @@
    2.19  \end{isamarkuptext}%
    2.20  \isamarkuptrue%
    2.21  %
    2.22 +\isamarkupsubsection{Single-step tactics%
    2.23 +}
    2.24 +\isamarkuptrue%
    2.25 +%
    2.26 +\begin{isamarkuptext}%
    2.27 +\begin{matharray}{rcl}
    2.28 +    \indexdef{}{ML}{safe\_step\_tac}\verb|safe_step_tac: Proof.context -> int -> tactic| \\
    2.29 +    \indexdef{}{ML}{inst\_step\_tac}\verb|inst_step_tac: Proof.context -> int -> tactic| \\
    2.30 +    \indexdef{}{ML}{step\_tac}\verb|step_tac: Proof.context -> int -> tactic| \\
    2.31 +    \indexdef{}{ML}{slow\_step\_tac}\verb|slow_step_tac: Proof.context -> int -> tactic| \\
    2.32 +    \indexdef{}{ML}{clarify\_step\_tac}\verb|clarify_step_tac: Proof.context -> int -> tactic| \\
    2.33 +  \end{matharray}
    2.34 +
    2.35 +  These are the primitive tactics behind the (semi)automated proof
    2.36 +  methods of the Classical Reasoner.  By calling them yourself, you
    2.37 +  can execute these procedures one step at a time.
    2.38 +
    2.39 +  \begin{description}
    2.40 +
    2.41 +  \item \verb|safe_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step on
    2.42 +  subgoal \isa{i}.  The safe wrapper tacticals are applied to a
    2.43 +  tactic that may include proof by assumption or Modus Ponens (taking
    2.44 +  care not to instantiate unknowns), or substitution.
    2.45 +
    2.46 +  \item \verb|inst_step_tac| is like \verb|safe_step_tac|, but allows
    2.47 +  unknowns to be instantiated.
    2.48 +
    2.49 +  \item \verb|step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} is the basic step of the proof
    2.50 +  procedure.  The unsafe wrapper tacticals are applied to a tactic
    2.51 +  that tries \verb|safe_tac|, \verb|inst_step_tac|, or applies an unsafe
    2.52 +  rule from the context.
    2.53 +
    2.54 +  \item \verb|slow_step_tac| resembles \verb|step_tac|, but allows
    2.55 +  backtracking between using safe rules with instantiation (\verb|inst_step_tac|) and using unsafe rules.  The resulting search space
    2.56 +  is larger.
    2.57 +
    2.58 +  \item \verb|clarify_step_tac|~\isa{{\isaliteral{22}{\isachardoublequote}}ctxt\ i{\isaliteral{22}{\isachardoublequote}}} performs a safe step
    2.59 +  on subgoal \isa{i}.  No splitting step is applied; for example,
    2.60 +  the subgoal \isa{{\isaliteral{22}{\isachardoublequote}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequote}}} is left as a conjunction.  Proof by
    2.61 +  assumption, Modus Ponens, etc., may be performed provided they do
    2.62 +  not instantiate unknowns.  Assumptions of the form \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequote}}}
    2.63 +  may be eliminated.  The safe wrapper tactical is applied.
    2.64 +
    2.65 +  \end{description}%
    2.66 +\end{isamarkuptext}%
    2.67 +\isamarkuptrue%
    2.68 +%
    2.69  \isamarkupsection{Object-logic setup \label{sec:object-logic}%
    2.70  }
    2.71  \isamarkuptrue%
     3.1 --- a/doc-src/Ref/classical.tex	Sat Jun 11 15:03:31 2011 +0200
     3.2 +++ b/doc-src/Ref/classical.tex	Sat Jun 11 15:36:46 2011 +0200
     3.3 @@ -125,21 +125,6 @@
     3.4  
     3.5  \section{The classical tactics}
     3.6  
     3.7 -\subsection{Semi-automatic tactics}
     3.8 -\begin{ttbox} 
     3.9 -clarify_step_tac : claset -> int -> tactic
    3.10 -\end{ttbox}
    3.11 -
    3.12 -\begin{ttdescription}
    3.13 -\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
    3.14 -  subgoal~$i$.  No splitting step is applied; for example, the subgoal $A\conj
    3.15 -  B$ is left as a conjunction.  Proof by assumption, Modus Ponens, etc., may be
    3.16 -  performed provided they do not instantiate unknowns.  Assumptions of the
    3.17 -  form $x=t$ may be eliminated.  The user-supplied safe wrapper tactical is
    3.18 -  applied.
    3.19 -\end{ttdescription}
    3.20 -
    3.21 -
    3.22  \subsection{Other classical tactics}
    3.23  \begin{ttbox} 
    3.24  slow_best_tac : claset -> int -> tactic
    3.25 @@ -173,36 +158,6 @@
    3.26  \end{ttdescription}
    3.27  
    3.28  
    3.29 -\subsection{Single-step tactics}
    3.30 -\begin{ttbox} 
    3.31 -safe_step_tac : claset -> int -> tactic
    3.32 -inst_step_tac : claset -> int -> tactic
    3.33 -step_tac      : claset -> int -> tactic
    3.34 -slow_step_tac : claset -> int -> tactic
    3.35 -\end{ttbox}
    3.36 -The automatic proof procedures call these tactics.  By calling them
    3.37 -yourself, you can execute these procedures one step at a time.
    3.38 -\begin{ttdescription}
    3.39 -\item[\ttindexbold{safe_step_tac} $cs$ $i$] performs a safe step on
    3.40 -  subgoal~$i$.  The safe wrapper tacticals are applied to a tactic that may
    3.41 -  include proof by assumption or Modus Ponens (taking care not to instantiate
    3.42 -  unknowns), or substitution.
    3.43 -
    3.44 -\item[\ttindexbold{inst_step_tac} $cs$ $i$] is like \texttt{safe_step_tac},
    3.45 -but allows unknowns to be instantiated.
    3.46 -
    3.47 -\item[\ttindexbold{step_tac} $cs$ $i$] is the basic step of the proof
    3.48 -  procedure.  The unsafe wrapper tacticals are applied to a tactic that tries
    3.49 -  \texttt{safe_tac}, \texttt{inst_step_tac}, or applies an unsafe rule
    3.50 -  from~$cs$.
    3.51 -
    3.52 -\item[\ttindexbold{slow_step_tac}] 
    3.53 -  resembles \texttt{step_tac}, but allows backtracking between using safe
    3.54 -  rules with instantiation (\texttt{inst_step_tac}) and using unsafe rules.
    3.55 -  The resulting search space is larger.
    3.56 -\end{ttdescription}
    3.57 -
    3.58 -
    3.59  \subsection{Other useful tactics}
    3.60  \index{tactics!for contradiction}
    3.61  \index{tactics!for Modus Ponens}