# HG changeset patch # User oheimb # Date 906648794 -7200 # Node ID 8375188ae9b0682d1313ad68bfaf29f4fe5ad90c # Parent 7e91d450fd6f0bf352167603111b46b3ab66fb79 introduced addSE2, addSD2, addE2, and addD2 reflected changes to addbefore, addSbefore described setup of clasimp.ML introduced clarsimp_tac and Clarsimp_tac diff -r 7e91d450fd6f -r 8375188ae9b0 doc-src/Ref/classical.tex --- a/doc-src/Ref/classical.tex Thu Sep 24 16:53:00 1998 +0200 +++ b/doc-src/Ref/classical.tex Thu Sep 24 16:53:14 1998 +0200 @@ -34,25 +34,27 @@ by (Blast_tac \(i\)); \end{ttbox} This command quickly proves most simple formulas of the predicate calculus or -set theory. To attempt to prove \emph{all} subgoals using a combination of +set theory. To attempt to prove subgoals using a combination of rewriting and classical reasoning, try \begin{ttbox} -by Auto_tac; +auto(); \emph{\textrm{applies to all subgoals}} +force i; \emph{\textrm{applies to one subgoal}} \end{ttbox} To do all obvious logical steps, even if they do not prove the subgoal, type one of the following: \begin{ttbox} +by Safe_tac; \emph{\textrm{applies to all subgoals}} by (Clarify_tac \(i\)); \emph{\textrm{applies to one subgoal}} -by Safe_tac; \emph{\textrm{applies to all subgoals}} \end{ttbox} + + You need to know how the classical reasoner works in order to use it -effectively. There are many tactics to choose from, including {\tt - Fast_tac} and \texttt{Best_tac}. +effectively. There are many tactics to choose from, including +{\tt Fast_tac} and \texttt{Best_tac}. We shall first discuss the underlying principles, then present the -classical reasoner. Finally, we shall see how to instantiate it for -new logics. The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already -installed. +classical reasoner. Finally, we shall see how to instantiate it for new logics. +The logics \FOL, \ZF, {\HOL} and {\HOLCF} have it already installed. \section{The sequent calculus} @@ -312,6 +314,22 @@ subgoals they will yield; rules that generate the fewest subgoals will be tried first (see \S\ref{biresolve_tac}). +For elimination and destruction rules there are variants of the add operations +adding a rule in a way such that it is applied only if also its second premise +can be unified with an assumption of the current proof state: +\begin{ttbox} +addSE2 : claset * (string * thm) -> claset \hfill{\bf infix 4} +addSD2 : claset * (string * thm) -> claset \hfill{\bf infix 4} +addE2 : claset * (string * thm) -> claset \hfill{\bf infix 4} +addD2 : claset * (string * thm) -> claset \hfill{\bf infix 4} +\end{ttbox} +\begin{warn} + A rule to be added in this special way must be given a name, which is used + to delete it again -- when desired -- using \texttt{delSWrappers} or + \texttt{delWrappers}, respectively. This is because these add operations + are implemented as wrappers (see \ref{sec:modifying-search} below). +\end{warn} + \subsection{Modifying the search step} \label{sec:modifying-search} @@ -328,10 +346,10 @@ {\bf wrapper tacticals} to it. The first wrapper list, which is considered to contain safe wrappers only, affects \ttindex{safe_step_tac} and all the tactics that call it. -The second one, which may contain unsafe wrappers, affects \ttindex{step_tac}, -\ttindex{slow_step_tac}, and the tactics that call them. +The second one, which may contain unsafe wrappers, affects the unsafe parts +of \ttindex{step_tac}, \ttindex{slow_step_tac}, and the tactics that call them. A wrapper transforms each step of the search, for example -by invoking other tactics before or alternatively to the original step tactic. +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 @@ -363,12 +381,12 @@ to modify the existing safe step tactic. \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore} -adds the given tactic as safe wrapper, such that it is -applied {\em before} each safe step of the search. +adds the given tactic as a safe wrapper, such that it is tried +{\em before} each safe step of the search. \item[$cs$ addSaltern $(name,tac)$] \indexbold{*addSaltern} -adds the given tactic as safe wrapper, such that it is -applied when a safe step of the search would fail. +adds the given tactic as a safe wrapper, such that it is tried +when a safe step of the search would fail. \item[$cs$ delSWrapper $name$] \indexbold{*delSWrapper} deletes the safe wrapper with the given name. @@ -377,12 +395,12 @@ adds a new wrapper to modify the existing (unsafe) step tactic. \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore} -adds the given tactic as unsafe wrapper, such that it is -applied {\em before} each step of the search. +adds the given tactic as an unsafe wrapper, such that it its result is +concatenated {\em before} the result of each unsafe step. \item[$cs$ addaltern $(name,tac)$] \indexbold{*addaltern} -adds the given tactic as unsafe wrapper, such that it is -applied when a step of the search would fail. +adds the given tactic as an unsafe wrapper, such that it its result is +concatenated {\em after} the result of each unsafe step. \item[$cs$ delWrapper $name$] \indexbold{*delWrapper} deletes the unsafe wrapper with the given name. @@ -397,18 +415,13 @@ \end{ttdescription} -\index{simplification!from classical reasoner} The wrapper tacticals -underly the operators addss and addSss, which are used as primitives -for the automatic tactics described in \S\ref{sec:automatic-tactics}. -Strictly speaking, both operators are not part of the classical reasoner. -They should be defined when the simplifier is installed: -\begin{ttbox} -infix 4 addSss addss; -fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac", - CHANGED o (safe_asm_full_simp_tac ss)); -fun cs addss ss = cs addbefore ("asm_full_simp_tac", - asm_full_simp_tac ss); -\end{ttbox} +\index{simplification!from classical reasoner} +Strictly speaking, the operators \texttt{addss} and \texttt{addSss} +are not part of the classical reasoner. +, which are used as primitives +for the automatic tactics described in \S\ref{sec:automatic-tactics}, are +implemented as wrapper tacticals. +they \begin{warn} Being defined as wrappers, these operators are inappropriate for adding more than one simpset at a time: the simpset added last overwrites any earlier ones. @@ -426,6 +439,7 @@ \begin{ttbox} clarify_tac : claset -> int -> tactic clarify_step_tac : claset -> int -> tactic +clarsimp_tac : clasimpset -> int -> tactic \end{ttbox} Use these when the automatic tactics fail. They perform all the obvious logical inferences that do not split the subgoal. The result is a @@ -434,13 +448,15 @@ \begin{ttdescription} \item[\ttindexbold{clarify_tac} $cs$ $i$] performs a series of safe steps on subgoal~$i$ by repeatedly calling \texttt{clarify_step_tac}. - \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. +\item[\ttindexbold{clarsimp_tac} $cs$ $i$] acts like \texttt{clarify_tac}, but +also does simplification with the given simpset. Still note that if the simpset +includes a splitter for the premises, the subgoal may be split. \end{ttdescription} @@ -629,6 +645,7 @@ Deepen_tac : int -> int -> tactic Clarify_tac : int -> tactic Clarify_step_tac : int -> tactic +Clarsimp_tac : int -> tactic Safe_tac : tactic Safe_step_tac : int -> tactic Step_tac : int -> tactic @@ -710,12 +727,11 @@ \section{Setting up the classical reasoner}\label{sec:classical-setup} \index{classical reasoner!setting up} -Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, have -the classical reasoner already set up. When defining a new classical logic, -you should set up the reasoner yourself. It consists of the \ML{} functor -\ttindex{ClassicalFun}, which takes the argument -signature \texttt{ - CLASSICAL_DATA}: +Isabelle's classical object-logics, including \texttt{FOL} and \texttt{HOL}, +have the classical reasoner already set up. +When defining a new classical logic, you should set up the reasoner yourself. +It consists of the \ML{} functor \ttindex{ClassicalFun}, which takes the +argument signature \texttt{CLASSICAL_DATA}: \begin{ttbox} signature CLASSICAL_DATA = sig @@ -756,7 +772,20 @@ \index{classical reasoner|)} +\section{Setting up the combination with the simplifier} +\label{sec:clasimp-setup} +To combine the classical reasoner and the simplifier, we simply call the +\ML{} functor \ttindex{ClasimpFun} that assembles the parts as required. +It takes a structure (of signature \texttt{CLASIMP_DATA}) as +argment, which can be contructed on the fly: +\begin{ttbox} +structure Clasimp = ClasimpFun + (structure Simplifier = Simplifier + and Classical = Classical + and Blast = Blast); +\end{ttbox} +% %%% Local Variables: %%% mode: latex %%% TeX-master: "ref"