1.1 --- a/doc-src/Ref/classical.tex Thu Sep 24 16:53:00 1998 +0200
1.2 +++ b/doc-src/Ref/classical.tex Thu Sep 24 16:53:14 1998 +0200
1.3 @@ -34,25 +34,27 @@
1.4 by (Blast_tac \(i\));
1.5 \end{ttbox}
1.6 This command quickly proves most simple formulas of the predicate calculus or
1.7 -set theory. To attempt to prove \emph{all} subgoals using a combination of
1.8 +set theory. To attempt to prove subgoals using a combination of
1.9 rewriting and classical reasoning, try
1.10 \begin{ttbox}
1.11 -by Auto_tac;
1.12 +auto(); \emph{\textrm{applies to all subgoals}}
1.13 +force i; \emph{\textrm{applies to one subgoal}}
1.14 \end{ttbox}
1.15 To do all obvious logical steps, even if they do not prove the
1.16 subgoal, type one of the following:
1.17 \begin{ttbox}
1.18 +by Safe_tac; \emph{\textrm{applies to all subgoals}}
1.19 by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}}
1.20 -by Safe_tac; \emph{\textrm{applies to all subgoals}}
1.21 \end{ttbox}
1.22 +
1.23 +
1.24 You need to know how the classical reasoner works in order to use it
1.25 -effectively. There are many tactics to choose from, including {\tt
1.26 - Fast_tac} and \texttt{Best_tac}.
1.27 +effectively. There are many tactics to choose from, including
1.28 +{\tt Fast_tac} and \texttt{Best_tac}.
1.29
1.30 We shall first discuss the underlying principles, then present the
1.31 -classical reasoner. Finally, we shall see how to instantiate it for
1.32 -new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already
1.33 -installed.
1.34 +classical reasoner. Finally, we shall see how to instantiate it for new logics.
1.35 +The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed.
1.36
1.37
1.38 \section{The sequent calculus}
1.39 @@ -312,6 +314,22 @@
1.40 subgoals they will yield; rules that generate the fewest subgoals will be
1.41 tried first (see \S\ref{biresolve_tac}).
1.42
1.43 +For elimination and destruction rules there are variants of the add operations
1.44 +adding a rule in a way such that it is applied only if also its second premise
1.45 +can be unified with an assumption of the current proof state:
1.46 +\begin{ttbox}
1.47 +addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
1.48 +addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
1.49 +addE2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
1.50 +addD2 : claset * (string * thm) -> claset \hfill{\bf infix 4}
1.51 +\end{ttbox}
1.52 +\begin{warn}
1.53 + A rule to be added in this special way must be given a name, which is used
1.54 + to delete it again -- when desired -- using \texttt{delSWrappers} or
1.55 + \texttt{delWrappers}, respectively. This is because these add operations
1.56 + are implemented as wrappers (see \ref{sec:modifying-search} below).
1.57 +\end{warn}
1.58 +
1.59
1.60 \subsection{Modifying the search step}
1.61 \label{sec:modifying-search}
1.62 @@ -328,10 +346,10 @@
1.63 {\bf wrapper tacticals} to it.
1.64 The first wrapper list, which is considered to contain safe wrappers only,
1.65 affects \ttindex{safe_step_tac} and all the tactics that call it.
1.66 -The second one, which may contain unsafe wrappers, affects \ttindex{step_tac},
1.67 -\ttindex{slow_step_tac}, and the tactics that call them.
1.68 +The second one, which may contain unsafe wrappers, affects the unsafe parts
1.69 +of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them.
1.70 A wrapper transforms each step of the search, for example
1.71 -by invoking other tactics before or alternatively to the original step tactic.
1.72 +by attempting other tactics before or after the original step tactic.
1.73 All members of a wrapper list are applied in turn to the respective step tactic.
1.74
1.75 Initially the two wrapper lists are empty, which means no modification of the
1.76 @@ -363,12 +381,12 @@
1.77 to modify the existing safe step tactic.
1.78
1.79 \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore}
1.80 -adds the given tactic as safe wrapper, such that it is
1.81 -applied {\em before} each safe step of the search.
1.82 +adds the given tactic as a safe wrapper, such that it is tried
1.83 +{\em before} each safe step of the search.
1.84
1.85 \item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern}
1.86 -adds the given tactic as safe wrapper, such that it is
1.87 -applied when a safe step of the search would fail.
1.88 +adds the given tactic as a safe wrapper, such that it is tried
1.89 +when a safe step of the search would fail.
1.90
1.91 \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper}
1.92 deletes the safe wrapper with the given name.
1.93 @@ -377,12 +395,12 @@
1.94 adds a new wrapper to modify the existing (unsafe) step tactic.
1.95
1.96 \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore}
1.97 -adds the given tactic as unsafe wrapper, such that it is
1.98 -applied {\em before} each step of the search.
1.99 +adds the given tactic as an unsafe wrapper, such that it its result is
1.100 +concatenated {\em before} the result of each unsafe step.
1.101
1.102 \item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern}
1.103 -adds the given tactic as unsafe wrapper, such that it is
1.104 -applied when a step of the search would fail.
1.105 +adds the given tactic as an unsafe wrapper, such that it its result is
1.106 +concatenated {\em after} the result of each unsafe step.
1.107
1.108 \item[$cs$ delWrapper $name$] \indexbold{*delWrapper}
1.109 deletes the unsafe wrapper with the given name.
1.110 @@ -397,18 +415,13 @@
1.111
1.112 \end{ttdescription}
1.113
1.114 -\index{simplification!from classical reasoner} The wrapper tacticals
1.115 -underly the operators addss and addSss, which are used as primitives
1.116 -for the automatic tactics described in \S\ref{sec:automatic-tactics}.
1.117 -Strictly speaking, both operators are not part of the classical reasoner.
1.118 -They should be defined when the simplifier is installed:
1.119 -\begin{ttbox}
1.120 -infix 4 addSss addss;
1.121 -fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
1.122 - CHANGED o (safe_asm_full_simp_tac ss));
1.123 -fun cs addss ss = cs addbefore ("asm_full_simp_tac",
1.124 - asm_full_simp_tac ss);
1.125 -\end{ttbox}
1.126 +\index{simplification!from classical reasoner}
1.127 +Strictly speaking, the operators \texttt{addss} and \texttt{addSss}
1.128 +are not part of the classical reasoner.
1.129 +, which are used as primitives
1.130 +for the automatic tactics described in \S\ref{sec:automatic-tactics}, are
1.131 +implemented as wrapper tacticals.
1.132 +they
1.133 \begin{warn}
1.134 Being defined as wrappers, these operators are inappropriate for adding more
1.135 than one simpset at a time: the simpset added last overwrites any earlier ones.
1.136 @@ -426,6 +439,7 @@
1.137 \begin{ttbox}
1.138 clarify_tac : claset -> int -> tactic
1.139 clarify_step_tac : claset -> int -> tactic
1.140 +clarsimp_tac : clasimpset -> int -> tactic
1.141 \end{ttbox}
1.142 Use these when the automatic tactics fail. They perform all the obvious
1.143 logical inferences that do not split the subgoal. The result is a
1.144 @@ -434,13 +448,15 @@
1.145 \begin{ttdescription}
1.146 \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on
1.147 subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}.
1.148 -
1.149 \item[\ttindexbold{clarify_step_tac} $cs$ $i$] performs a safe step on
1.150 subgoal~$i$. No splitting step is applied; for example, the subgoal $A\conj
1.151 B$ is left as a conjunction. Proof by assumption, Modus Ponens, etc., may be
1.152 performed provided they do not instantiate unknowns. Assumptions of the
1.153 form $x=t$ may be eliminated. The user-supplied safe wrapper tactical is
1.154 applied.
1.155 +\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but
1.156 +also does simplification with the given simpset. Still note that if the simpset
1.157 +includes a splitter for the premises, the subgoal may be split.
1.158 \end{ttdescription}
1.159
1.160
1.161 @@ -629,6 +645,7 @@
1.162 Deepen_tac : int -> int -> tactic
1.163 Clarify_tac : int -> tactic
1.164 Clarify_step_tac : int -> tactic
1.165 +Clarsimp_tac : int -> tactic
1.166 Safe_tac : tactic
1.167 Safe_step_tac : int -> tactic
1.168 Step_tac : int -> tactic
1.169 @@ -710,12 +727,11 @@
1.170
1.171 \section{Setting up the classical reasoner}\label{sec:classical-setup}
1.172 \index{classical reasoner!setting up}
1.173 -Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, have
1.174 -the classical reasoner already set up. When defining a new classical logic,
1.175 -you should set up the reasoner yourself. It consists of the \ML{} functor
1.176 -\ttindex{ClassicalFun}, which takes the argument
1.177 -signature \texttt{
1.178 - CLASSICAL_DATA}:
1.179 +Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL},
1.180 +have the classical reasoner already set up.
1.181 +When defining a new classical logic, you should set up the reasoner yourself.
1.182 +It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the
1.183 +argument signature \texttt{CLASSICAL_DATA}:
1.184 \begin{ttbox}
1.185 signature CLASSICAL_DATA =
1.186 sig
1.187 @@ -756,7 +772,20 @@
1.188
1.189 \index{classical reasoner|)}
1.190
1.191 +\section{Setting up the combination with the simplifier}
1.192 +\label{sec:clasimp-setup}
1.193
1.194 +To combine the classical reasoner and the simplifier, we simply call the
1.195 +\ML{} functor \ttindex{ClasimpFun} that assembles the parts as required.
1.196 +It takes a structure (of signature \texttt{CLASIMP_DATA}) as
1.197 +argment, which can be contructed on the fly:
1.198 +\begin{ttbox}
1.199 +structure Clasimp = ClasimpFun
1.200 + (structure Simplifier = Simplifier
1.201 + and Classical = Classical
1.202 + and Blast = Blast);
1.203 +\end{ttbox}
1.204 +%
1.205 %%% Local Variables:
1.206 %%% mode: latex
1.207 %%% TeX-master: "ref"