1.1 --- a/doc-src/Ref/classical.tex Fri Sep 25 15:54:29 1998 +0200
1.2 +++ b/doc-src/Ref/classical.tex Fri Sep 25 15:57:23 1998 +0200
1.3 @@ -44,7 +44,7 @@
1.4 subgoal, type one of the following:
1.5 \begin{ttbox}
1.6 by Safe_tac; \emph{\textrm{applies to all subgoals}}
1.7 -by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}}
1.8 +by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}}
1.9 \end{ttbox}
1.10
1.11
1.12 @@ -317,6 +317,7 @@
1.13 For elimination and destruction rules there are variants of the add operations
1.14 adding a rule in a way such that it is applied only if also its second premise
1.15 can be unified with an assumption of the current proof state:
1.16 +\indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2}
1.17 \begin{ttbox}
1.18 addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
1.19 addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
1.20 @@ -435,30 +436,6 @@
1.21 powerful theorem-proving tactics. Most of them have capitalized analogues
1.22 that use the default claset; see \S\ref{sec:current-claset}.
1.23
1.24 -\subsection{Semi-automatic tactics}
1.25 -\begin{ttbox}
1.26 -clarify_tac : claset -> int -> tactic
1.27 -clarify_step_tac : claset -> int -> tactic
1.28 -clarsimp_tac : clasimpset -> int -> tactic
1.29 -\end{ttbox}
1.30 -Use these when the automatic tactics fail. They perform all the obvious
1.31 -logical inferences that do not split the subgoal. The result is a
1.32 -simpler subgoal that can be tackled by other means, such as by
1.33 -instantiating quantifiers yourself.
1.34 -\begin{ttdescription}
1.35 -\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
1.36 -subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
1.37 -\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
1.38 - subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
1.39 - B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
1.40 - performed provided they do not instantiate unknowns. Assumptions of the
1.41 - form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
1.42 - applied.
1.43 -\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
1.44 -also does simplification with the given simpset. Still note that if the simpset
1.45 -includes a splitter for the premises, the subgoal may be split.
1.46 -\end{ttdescription}
1.47 -
1.48
1.49 \subsection{The tableau prover}
1.50 The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover,
1.51 @@ -532,6 +509,32 @@
1.52 the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;}
1.53 while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);}
1.54
1.55 +
1.56 +\subsection{Semi-automatic tactics}
1.57 +\begin{ttbox}
1.58 +clarify_tac : claset -> int -> tactic
1.59 +clarify_step_tac : claset -> int -> tactic
1.60 +clarsimp_tac : clasimpset -> int -> tactic
1.61 +\end{ttbox}
1.62 +Use these when the automatic tactics fail. They perform all the obvious
1.63 +logical inferences that do not split the subgoal. The result is a
1.64 +simpler subgoal that can be tackled by other means, such as by
1.65 +instantiating quantifiers yourself.
1.66 +\begin{ttdescription}
1.67 +\item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
1.68 +subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
1.69 +\item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
1.70 + subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
1.71 + B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
1.72 + performed provided they do not instantiate unknowns. Assumptions of the
1.73 + form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
1.74 + applied.
1.75 +\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
1.76 +also does simplification with the given simpset. Still note that if the simpset
1.77 +includes a splitter for the premises, the subgoal may be split.
1.78 +\end{ttdescription}
1.79 +
1.80 +
1.81 \subsection{Other classical tactics}
1.82 \begin{ttbox}
1.83 fast_tac : claset -> int -> tactic
1.84 @@ -619,21 +622,14 @@
1.85 The resulting search space is larger.
1.86 \end{ttdescription}
1.87
1.88 +
1.89 \subsection{The current claset}\label{sec:current-claset}
1.90
1.91 -Each theory is equipped with an implicit \emph{current
1.92 - claset}\index{claset!current}. This is a default set of classical
1.93 +Each theory is equipped with an implicit \emph{current claset}
1.94 +\index{claset!current}. This is a default set of classical
1.95 rules. The underlying idea is quite similar to that of a current
1.96 simpset described in \S\ref{sec:simp-for-dummies}; please read that
1.97 -section, including its warnings. The implicit claset can be accessed
1.98 -as follows:
1.99 -\begin{ttbox}
1.100 -claset : unit -> claset
1.101 -claset_ref : unit -> claset ref
1.102 -claset_of : theory -> claset
1.103 -claset_ref_of : theory -> claset ref
1.104 -print_claset : theory -> unit
1.105 -\end{ttbox}
1.106 +section, including its warnings.
1.107
1.108 The tactics
1.109 \begin{ttbox}
1.110 @@ -653,15 +649,15 @@
1.111 \indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac}
1.112 \indexbold{*Best_tac}\indexbold{*Fast_tac}%
1.113 \indexbold{*Deepen_tac}
1.114 -\indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}
1.115 +\indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac}
1.116 \indexbold{*Safe_tac}\indexbold{*Safe_step_tac}
1.117 \indexbold{*Step_tac}
1.118 make use of the current claset. For example, \texttt{Blast_tac} is defined as
1.119 \begin{ttbox}
1.120 fun Blast_tac i st = blast_tac (claset()) i st;
1.121 \end{ttbox}
1.122 -and gets the current claset, only after it is applied to a proof
1.123 -state. The functions
1.124 +and gets the current claset, only after it is applied to a proof state.
1.125 +The functions
1.126 \begin{ttbox}
1.127 AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
1.128 \end{ttbox}
1.129 @@ -674,6 +670,27 @@
1.130 \end{ttbox}
1.131 deletes rules from the current claset.
1.132
1.133 +
1.134 +\subsection{Accessing the current claset}
1.135 +\label{sec:access-current-claset}
1.136 +
1.137 +the functions to access the current claset are analogous to the functions
1.138 +for the current simpset, so please see \label{sec:access-current-simpset}
1.139 +for a description.
1.140 +\begin{ttbox}
1.141 +claset : unit -> claset
1.142 +claset_ref : unit -> claset ref
1.143 +claset_of : theory -> claset
1.144 +claset_ref_of : theory -> claset ref
1.145 +print_claset : theory -> unit
1.146 +CLASET :(claset -> tactic) -> tactic
1.147 +CLASET' :(claset -> 'a -> tactic) -> 'a -> tactic
1.148 +
1.149 +CLASIMPSET :(clasimpset -> tactic) -> tactic
1.150 +CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic
1.151 +\end{ttbox}
1.152 +
1.153 +
1.154 \subsection{Other useful tactics}
1.155 \index{tactics!for contradiction}
1.156 \index{tactics!for Modus Ponens}