summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/classical.tex

author | wenzelm |

Fri, 10 Nov 2000 19:02:37 +0100 | |

changeset 10432 | 3dfbc913d184 |

parent 9695 | ec7d7f877712 |

child 11181 | d04f57b91166 |

permissions | -rw-r--r-- |

added axclass inverse and consts inverse, divide (infix "/");
moved axclass power to Nat.thy;

%% $Id$ \chapter{The Classical Reasoner}\label{chap:classical} \index{classical reasoner|(} \newcommand\ainfer[2]{\begin{array}{r@{\,}l}#2\\ \hline#1\end{array}} Although Isabelle is generic, many users will be working in some extension of classical first-order logic. Isabelle's set theory~ZF is built upon theory~FOL, while HOL conceptually contains first-order logic as a fragment. Theorem-proving in predicate logic is undecidable, but many researchers have developed strategies to assist in this task. Isabelle's classical reasoner is an \ML{} functor that accepts certain information about a logic and delivers a suite of automatic tactics. Each tactic takes a collection of rules and executes a simple, non-clausal proof procedure. They are slow and simplistic compared with resolution theorem provers, but they can save considerable time and effort. They can prove theorems such as Pelletier's~\cite{pelletier86} problems~40 and~41 in seconds: \[ (\exists y. \forall x. J(y,x) \bimp \neg J(x,x)) \imp \neg (\forall x. \exists y. \forall z. J(z,y) \bimp \neg J(z,x)) \] \[ (\forall z. \exists y. \forall x. F(x,y) \bimp F(x,z) \conj \neg F(x,x)) \imp \neg (\exists z. \forall x. F(x,z)) \] % The tactics are generic. They are not restricted to first-order logic, and have been heavily used in the development of Isabelle's set theory. Few interactive proof assistants provide this much automation. The tactics can be traced, and their components can be called directly; in this manner, any proof can be viewed interactively. The simplest way to apply the classical reasoner (to subgoal~$i$) is to type \begin{ttbox} by (Blast_tac \(i\)); \end{ttbox} This command quickly proves most simple formulas of the predicate calculus or set theory. To attempt to prove subgoals using a combination of rewriting and classical reasoning, try \begin{ttbox} 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}} \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}. 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. \section{The sequent calculus} \index{sequent calculus} Isabelle supports natural deduction, which is easy to use for interactive proof. But natural deduction does not easily lend itself to automation, and has a bias towards intuitionism. For certain proofs in classical logic, it can not be called natural. The {\bf sequent calculus}, a generalization of natural deduction, is easier to automate. A {\bf sequent} has the form $\Gamma\turn\Delta$, where $\Gamma$ and~$\Delta$ are sets of formulae.% \footnote{For first-order logic, sequents can equivalently be made from lists or multisets of formulae.} The sequent \[ P@1,\ldots,P@m\turn Q@1,\ldots,Q@n \] is {\bf valid} if $P@1\conj\ldots\conj P@m$ implies $Q@1\disj\ldots\disj Q@n$. Thus $P@1,\ldots,P@m$ represent assumptions, each of which is true, while $Q@1,\ldots,Q@n$ represent alternative goals. A sequent is {\bf basic} if its left and right sides have a common formula, as in $P,Q\turn Q,R$; basic sequents are trivially valid. Sequent rules are classified as {\bf right} or {\bf left}, indicating which side of the $\turn$~symbol they operate on. Rules that operate on the right side are analogous to natural deduction's introduction rules, and left rules are analogous to elimination rules. Recall the natural deduction rules for first-order logic, \iflabelundefined{fol-fig}{from {\it Introduction to Isabelle}}% {Fig.\ts\ref{fol-fig}}. The sequent calculus analogue of~$({\imp}I)$ is the rule $$ \ainfer{\Gamma &\turn \Delta, P\imp Q}{P,\Gamma &\turn \Delta,Q} \eqno({\imp}R) $$ This breaks down some implication on the right side of a sequent; $\Gamma$ and $\Delta$ stand for the sets of formulae that are unaffected by the inference. The analogue of the pair~$({\disj}I1)$ and~$({\disj}I2)$ is the single rule $$ \ainfer{\Gamma &\turn \Delta, P\disj Q}{\Gamma &\turn \Delta,P,Q} \eqno({\disj}R) $$ This breaks down some disjunction on the right side, replacing it by both disjuncts. Thus, the sequent calculus is a kind of multiple-conclusion logic. To illustrate the use of multiple formulae on the right, let us prove the classical theorem $(P\imp Q)\disj(Q\imp P)$. Working backwards, we reduce this formula to a basic sequent: \[ \infer[(\disj)R]{\turn(P\imp Q)\disj(Q\imp P)} {\infer[(\imp)R]{\turn(P\imp Q), (Q\imp P)\;} {\infer[(\imp)R]{P \turn Q, (Q\imp P)\qquad} {P, Q \turn Q, P\qquad\qquad}}} \] This example is typical of the sequent calculus: start with the desired theorem and apply rules backwards in a fairly arbitrary manner. This yields a surprisingly effective proof procedure. Quantifiers add few complications, since Isabelle handles parameters and schematic variables. See Chapter~10 of {\em ML for the Working Programmer}~\cite{paulson-ml2} for further discussion. \section{Simulating sequents by natural deduction} Isabelle can represent sequents directly, as in the object-logic~\texttt{LK}\@. But natural deduction is easier to work with, and most object-logics employ it. Fortunately, we can simulate the sequent $P@1,\ldots,P@m\turn Q@1,\ldots,Q@n$ by the Isabelle formula \[ \List{P@1;\ldots;P@m; \neg Q@2;\ldots; \neg Q@n}\Imp Q@1, \] where the order of the assumptions and the choice of~$Q@1$ are arbitrary. Elim-resolution plays a key role in simulating sequent proofs. We can easily handle reasoning on the left. As discussed in \iflabelundefined{destruct}{{\it Introduction to Isabelle}}{\S\ref{destruct}}, elim-resolution with the rules $(\disj E)$, $(\bot E)$ and $(\exists E)$ achieves a similar effect as the corresponding sequent rules. For the other connectives, we use sequent-style elimination rules instead of destruction rules such as $({\conj}E1,2)$ and $(\forall E)$. But note that the rule $(\neg L)$ has no effect under our representation of sequents! $$ \ainfer{\neg P,\Gamma &\turn \Delta}{\Gamma &\turn \Delta,P}\eqno({\neg}L) $$ What about reasoning on the right? Introduction rules can only affect the formula in the conclusion, namely~$Q@1$. The other right-side formulae are represented as negated assumptions, $\neg Q@2$, \ldots,~$\neg Q@n$. \index{assumptions!negated} In order to operate on one of these, it must first be exchanged with~$Q@1$. Elim-resolution with the {\bf swap} rule has this effect: $$ \List{\neg P; \; \neg R\Imp P} \Imp R \eqno(swap) $$ To ensure that swaps occur only when necessary, each introduction rule is converted into a swapped form: it is resolved with the second premise of~$(swap)$. The swapped form of~$({\conj}I)$, which might be called~$({\neg\conj}E)$, is \[ \List{\neg(P\conj Q); \; \neg R\Imp P; \; \neg R\Imp Q} \Imp R. \] Similarly, the swapped form of~$({\imp}I)$ is \[ \List{\neg(P\imp Q); \; \List{\neg R;P}\Imp Q} \Imp R \] Swapped introduction rules are applied using elim-resolution, which deletes the negated formula. Our representation of sequents also requires the use of ordinary introduction rules. If we had no regard for readability, we could treat the right side more uniformly by representing sequents as \[ \List{P@1;\ldots;P@m; \neg Q@1;\ldots; \neg Q@n}\Imp \bot. \] \section{Extra rules for the sequent calculus} As mentioned, destruction rules such as $({\conj}E1,2)$ and $(\forall E)$ must be replaced by sequent-style elimination rules. In addition, we need rules to embody the classical equivalence between $P\imp Q$ and $\neg P\disj Q$. The introduction rules~$({\disj}I1,2)$ are replaced by a rule that simulates $({\disj}R)$: \[ (\neg Q\Imp P) \Imp P\disj Q \] The destruction rule $({\imp}E)$ is replaced by \[ \List{P\imp Q;\; \neg P\Imp R;\; Q\Imp R} \Imp R. \] Quantifier replication also requires special rules. In classical logic, $\exists x{.}P$ is equivalent to $\neg\forall x{.}\neg P$; the rules $(\exists R)$ and $(\forall L)$ are dual: \[ \ainfer{\Gamma &\turn \Delta, \exists x{.}P} {\Gamma &\turn \Delta, \exists x{.}P, P[t/x]} \; (\exists R) \qquad \ainfer{\forall x{.}P, \Gamma &\turn \Delta} {P[t/x], \forall x{.}P, \Gamma &\turn \Delta} \; (\forall L) \] Thus both kinds of quantifier may be replicated. Theorems requiring multiple uses of a universal formula are easy to invent; consider \[ (\forall x.P(x)\imp P(f(x))) \conj P(a) \imp P(f^n(a)), \] for any~$n>1$. Natural examples of the multiple use of an existential formula are rare; a standard one is $\exists x.\forall y. P(x)\imp P(y)$. Forgoing quantifier replication loses completeness, but gains decidability, since the search space becomes finite. Many useful theorems can be proved without replication, and the search generally delivers its verdict in a reasonable time. To adopt this approach, represent the sequent rules $(\exists R)$, $(\exists L)$ and $(\forall R)$ by $(\exists I)$, $(\exists E)$ and $(\forall I)$, respectively, and put $(\forall E)$ into elimination form: $$ \List{\forall x{.}P(x); P(t)\Imp Q} \Imp Q \eqno(\forall E@2) $$ Elim-resolution with this rule will delete the universal formula after a single use. To replicate universal quantifiers, replace the rule by $$ \List{\forall x{.}P(x);\; \List{P(t); \forall x{.}P(x)}\Imp Q} \Imp Q. \eqno(\forall E@3) $$ To replicate existential quantifiers, replace $(\exists I)$ by \[ \List{\neg(\exists x{.}P(x)) \Imp P(t)} \Imp \exists x{.}P(x). \] All introduction rules mentioned above are also useful in swapped form. Replication makes the search space infinite; we must apply the rules with care. The classical reasoner distinguishes between safe and unsafe rules, applying the latter only when there is no alternative. Depth-first search may well go down a blind alley; best-first search is better behaved in an infinite search space. However, quantifier replication is too expensive to prove any but the simplest theorems. \section{Classical rule sets} \index{classical sets} Each automatic tactic takes a {\bf classical set} --- a collection of rules, classified as introduction or elimination and as {\bf safe} or {\bf unsafe}. In general, safe rules can be attempted blindly, while unsafe rules must be used with care. A safe rule must never reduce a provable goal to an unprovable set of subgoals. The rule~$({\disj}I1)$ is unsafe because it reduces $P\disj Q$ to~$P$. Any rule is unsafe whose premises contain new unknowns. The elimination rule~$(\forall E@2)$ is unsafe, since it is applied via elim-resolution, which discards the assumption $\forall x{.}P(x)$ and replaces it by the weaker assumption~$P(\Var{t})$. The rule $({\exists}I)$ is unsafe for similar reasons. The rule~$(\forall E@3)$ is unsafe in a different sense: since it keeps the assumption $\forall x{.}P(x)$, it is prone to looping. In classical first-order logic, all rules are safe except those mentioned above. The safe/unsafe distinction is vague, and may be regarded merely as a way of giving some rules priority over others. One could argue that $({\disj}E)$ is unsafe, because repeated application of it could generate exponentially many subgoals. Induction rules are unsafe because inductive proofs are difficult to set up automatically. Any inference is unsafe that instantiates an unknown in the proof state --- thus \ttindex{match_tac} must be used, rather than \ttindex{resolve_tac}. Even proof by assumption is unsafe if it instantiates unknowns shared with other subgoals --- thus \ttindex{eq_assume_tac} must be used, rather than \ttindex{assume_tac}. \subsection{Adding rules to classical sets} Classical rule sets belong to the abstract type \mltydx{claset}, which supports the following operations (provided the classical reasoner is installed!): \begin{ttbox} empty_cs : claset print_cs : claset -> unit rep_cs : claset -> \{safeEs: thm list, safeIs: thm list, hazEs: thm list, hazIs: thm list, swrappers: (string * wrapper) list, uwrappers: (string * wrapper) list, safe0_netpair: netpair, safep_netpair: netpair, haz_netpair: netpair, dup_netpair: netpair\} addSIs : claset * thm list -> claset \hfill{\bf infix 4} addSEs : claset * thm list -> claset \hfill{\bf infix 4} addSDs : claset * thm list -> claset \hfill{\bf infix 4} addIs : claset * thm list -> claset \hfill{\bf infix 4} addEs : claset * thm list -> claset \hfill{\bf infix 4} addDs : claset * thm list -> claset \hfill{\bf infix 4} delrules : claset * thm list -> claset \hfill{\bf infix 4} \end{ttbox} The add operations ignore any rule already present in the claset with the same classification (such as safe introduction). They print a warning if the rule has already been added with some other classification, but add the rule anyway. Calling \texttt{delrules} deletes all occurrences of a rule from the claset, but see the warning below concerning destruction rules. \begin{ttdescription} \item[\ttindexbold{empty_cs}] is the empty classical set. \item[\ttindexbold{print_cs} $cs$] displays the printable contents of~$cs$, which is the rules. All other parts are non-printable. \item[\ttindexbold{rep_cs} $cs$] decomposes $cs$ as a record of its internal components, namely the safe introduction and elimination rules, the unsafe introduction and elimination rules, the lists of safe and unsafe wrappers (see \ref{sec:modifying-search}), and the internalized forms of the rules. \item[$cs$ addSIs $rules$] \indexbold{*addSIs} adds safe introduction~$rules$ to~$cs$. \item[$cs$ addSEs $rules$] \indexbold{*addSEs} adds safe elimination~$rules$ to~$cs$. \item[$cs$ addSDs $rules$] \indexbold{*addSDs} adds safe destruction~$rules$ to~$cs$. \item[$cs$ addIs $rules$] \indexbold{*addIs} adds unsafe introduction~$rules$ to~$cs$. \item[$cs$ addEs $rules$] \indexbold{*addEs} adds unsafe elimination~$rules$ to~$cs$. \item[$cs$ addDs $rules$] \indexbold{*addDs} adds unsafe destruction~$rules$ to~$cs$. \item[$cs$ delrules $rules$] \indexbold{*delrules} deletes~$rules$ from~$cs$. It prints a warning for those rules that are not in~$cs$. \end{ttdescription} \begin{warn} If you added $rule$ using \texttt{addSDs} or \texttt{addDs}, then you must delete it as follows: \begin{ttbox} \(cs\) delrules [make_elim \(rule\)] \end{ttbox} \par\noindent This is necessary because the operators \texttt{addSDs} and \texttt{addDs} convert the destruction rules to elimination rules by applying \ttindex{make_elim}, and then insert them using \texttt{addSEs} and \texttt{addEs}, respectively. \end{warn} Introduction rules are those that can be applied using ordinary resolution. The classical set automatically generates their swapped forms, which will be applied using elim-resolution. Elimination rules are applied using elim-resolution. In a classical set, rules are sorted by the number of new 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: \indexbold{*addSE2}\indexbold{*addSD2}\indexbold{*addE2}\indexbold{*addD2} \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} For a given classical set, the proof strategy is simple. Perform as many safe inferences as possible; or else, apply certain safe rules, allowing instantiation of unknowns; or else, apply an unsafe rule. The tactics also eliminate assumptions of the form $x=t$ by substitution if they have been set up to do so (see \texttt{hyp_subst_tacs} in~\S\ref{sec:classical-setup} below). They may perform a form of Modus Ponens: if there are assumptions $P\imp Q$ and~$P$, then replace $P\imp Q$ by~$Q$. The classical reasoning tactics --- except \texttt{blast_tac}! --- allow you to modify this basic proof strategy by applying two lists of arbitrary {\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 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 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 step tactics. Safe and unsafe wrappers are added to a claset with the functions given below, supplying them with wrapper names. These names may be used to selectively delete wrappers. \begin{ttbox} type wrapper = (int -> tactic) -> (int -> tactic); addSWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4} addSbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} addSaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} delSWrapper : claset * string -> claset \hfill{\bf infix 4} addWrapper : claset * (string * wrapper ) -> claset \hfill{\bf infix 4} addbefore : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} addaltern : claset * (string * (int -> tactic)) -> claset \hfill{\bf infix 4} delWrapper : claset * string -> claset \hfill{\bf infix 4} addSss : claset * simpset -> claset \hfill{\bf infix 4} addss : claset * simpset -> claset \hfill{\bf infix 4} \end{ttbox} % \begin{ttdescription} \item[$cs$ addSWrapper $(name,wrapper)$] \indexbold{*addSWrapper} adds a new wrapper, which should yield a safe tactic, to modify the existing safe step tactic. \item[$cs$ addSbefore $(name,tac)$] \indexbold{*addSbefore} 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 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. \item[$cs$ addWrapper $(name,wrapper)$] \indexbold{*addWrapper} adds a new wrapper to modify the existing (unsafe) step tactic. \item[$cs$ addbefore $(name,tac)$] \indexbold{*addbefore} 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 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. \item[$cs$ addSss $ss$] \indexbold{*addss} adds the simpset~$ss$ to the classical set. The assumptions and goal will be simplified, in a rather safe way, after each safe step of the search. \item[$cs$ addss $ss$] \indexbold{*addss} adds the simpset~$ss$ to the classical set. The assumptions and goal will be simplified, before the each unsafe step of the search. \end{ttdescription} \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. When a simpset combined with a claset is to be augmented, this should done {\em before} combining it with the claset. \end{warn} \section{The classical tactics} \index{classical reasoner!tactics} If installed, the classical module provides powerful theorem-proving tactics. Most of them have capitalized analogues that use the default claset; see \S\ref{sec:current-claset}. \subsection{The tableau prover} The tactic \texttt{blast_tac} searches for a proof using a fast tableau prover, coded directly in \ML. It then reconstructs the proof using Isabelle tactics. It is faster and more powerful than the other classical reasoning tactics, but has major limitations too. \begin{itemize} \item It does not use the wrapper tacticals described above, such as \ttindex{addss}. \item It ignores types, which can cause problems in HOL. If it applies a rule whose types are inappropriate, then proof reconstruction will fail. \item It does not perform higher-order unification, as needed by the rule {\tt rangeI} in HOL and \texttt{RepFunI} in ZF. There are often alternatives to such rules, for example {\tt range_eqI} and \texttt{RepFun_eqI}. \item Function variables may only be applied to parameters of the subgoal. (This restriction arises because the prover does not use higher-order unification.) If other function variables are present then the prover will fail with the message {\small\tt Function Var's argument not a bound variable}. \item Its proof strategy is more general than \texttt{fast_tac}'s but can be slower. If \texttt{blast_tac} fails or seems to be running forever, try {\tt fast_tac} and the other tactics described below. \end{itemize} % \begin{ttbox} blast_tac : claset -> int -> tactic Blast.depth_tac : claset -> int -> int -> tactic Blast.trace : bool ref \hfill{\bf initially false} \end{ttbox} The two tactics differ on how they bound the number of unsafe steps used in a proof. While \texttt{blast_tac} starts with a bound of zero and increases it successively to~20, \texttt{Blast.depth_tac} applies a user-supplied search bound. \begin{ttdescription} \item[\ttindexbold{blast_tac} $cs$ $i$] tries to prove subgoal~$i$, increasing the search bound using iterative deepening~\cite{korf85}. \item[\ttindexbold{Blast.depth_tac} $cs$ $lim$ $i$] tries to prove subgoal~$i$ using a search bound of $lim$. Sometimes a slow proof using \texttt{blast_tac} can be made much faster by supplying the successful search bound to this tactic instead. \item[set \ttindexbold{Blast.trace};] \index{tracing!of classical prover} causes the tableau prover to print a trace of its search. At each step it displays the formula currently being examined and reports whether the branch has been closed, extended or split. \end{ttdescription} \subsection{Automatic tactics}\label{sec:automatic-tactics} \begin{ttbox} type clasimpset = claset * simpset; auto_tac : clasimpset -> tactic force_tac : clasimpset -> int -> tactic auto : unit -> unit force : int -> unit \end{ttbox} The automatic tactics attempt to prove goals using a combination of simplification and classical reasoning. \begin{ttdescription} \item[\ttindexbold{auto_tac $(cs,ss)$}] is intended for situations where there are a lot of mostly trivial subgoals; it proves all the easy ones, leaving the ones it cannot prove. (Unfortunately, attempting to prove the hard ones may take a long time.) \item[\ttindexbold{force_tac} $(cs,ss)$ $i$] is intended to prove subgoal~$i$ completely. It tries to apply all fancy tactics it knows about, performing a rather exhaustive search. \end{ttdescription} They must be supplied both a simpset and a claset; therefore they are most easily called as \texttt{Auto_tac} and \texttt{Force_tac}, which use the default claset and simpset (see \S\ref{sec:current-claset} below). For interactive use, the shorthand \texttt{auto();} abbreviates \texttt{by Auto_tac;} while \texttt{force 1;} abbreviates \texttt{by (Force_tac 1);} \subsection{Semi-automatic tactics} \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 simpler subgoal that can be tackled by other means, such as by instantiating quantifiers yourself. \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. Note that if the simpset includes a splitter for the premises, the subgoal may still be split. \end{ttdescription} \subsection{Other classical tactics} \begin{ttbox} fast_tac : claset -> int -> tactic best_tac : claset -> int -> tactic slow_tac : claset -> int -> tactic slow_best_tac : claset -> int -> tactic \end{ttbox} These tactics attempt to prove a subgoal using sequent-style reasoning. Unlike \texttt{blast_tac}, they construct proofs directly in Isabelle. Their effect is restricted (by \texttt{SELECT_GOAL}) to one subgoal; they either prove this subgoal or fail. The \texttt{slow_} versions conduct a broader search.% \footnote{They may, when backtracking from a failed proof attempt, undo even the step of proving a subgoal by assumption.} The best-first tactics are guided by a heuristic function: typically, the total size of the proof state. This function is supplied in the functor call that sets up the classical reasoner. \begin{ttdescription} \item[\ttindexbold{fast_tac} $cs$ $i$] applies \texttt{step_tac} using depth-first search to prove subgoal~$i$. \item[\ttindexbold{best_tac} $cs$ $i$] applies \texttt{step_tac} using best-first search to prove subgoal~$i$. \item[\ttindexbold{slow_tac} $cs$ $i$] applies \texttt{slow_step_tac} using depth-first search to prove subgoal~$i$. \item[\ttindexbold{slow_best_tac} $cs$ $i$] applies \texttt{slow_step_tac} with best-first search to prove subgoal~$i$. \end{ttdescription} \subsection{Depth-limited automatic tactics} \begin{ttbox} depth_tac : claset -> int -> int -> tactic deepen_tac : claset -> int -> int -> tactic \end{ttbox} These work by exhaustive search up to a specified depth. Unsafe rules are modified to preserve the formula they act on, so that it be used repeatedly. They can prove more goals than \texttt{fast_tac} can but are much slower, for example if the assumptions have many universal quantifiers. The depth limits the number of unsafe steps. If you can estimate the minimum number of unsafe steps needed, supply this value as~$m$ to save time. \begin{ttdescription} \item[\ttindexbold{depth_tac} $cs$ $m$ $i$] tries to prove subgoal~$i$ by exhaustive search up to depth~$m$. \item[\ttindexbold{deepen_tac} $cs$ $m$ $i$] tries to prove subgoal~$i$ by iterative deepening. It calls \texttt{depth_tac} repeatedly with increasing depths, starting with~$m$. \end{ttdescription} \subsection{Single-step tactics} \begin{ttbox} safe_step_tac : claset -> int -> tactic safe_tac : claset -> 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{safe_tac} $cs$] repeatedly performs safe steps on all subgoals. It is deterministic, with at most one outcome. \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{The current claset}\label{sec:current-claset} Each theory is equipped with an implicit \emph{current claset} \index{claset!current}. This is a default set of classical rules. The underlying idea is quite similar to that of a current simpset described in \S\ref{sec:simp-for-dummies}; please read that section, including its warnings. The tactics \begin{ttbox} Blast_tac : int -> tactic Auto_tac : tactic Force_tac : int -> tactic Fast_tac : int -> tactic Best_tac : int -> tactic 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 \end{ttbox} \indexbold{*Blast_tac}\indexbold{*Auto_tac}\indexbold{*Force_tac} \indexbold{*Best_tac}\indexbold{*Fast_tac}% \indexbold{*Deepen_tac} \indexbold{*Clarify_tac}\indexbold{*Clarify_step_tac}\indexbold{*Clarsimp_tac} \indexbold{*Safe_tac}\indexbold{*Safe_step_tac} \indexbold{*Step_tac} make use of the current claset. For example, \texttt{Blast_tac} is defined as \begin{ttbox} fun Blast_tac i st = blast_tac (claset()) i st; \end{ttbox} and gets the current claset, only after it is applied to a proof state. The functions \begin{ttbox} AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit \end{ttbox} \indexbold{*AddSIs} \indexbold{*AddSEs} \indexbold{*AddSDs} \indexbold{*AddIs} \indexbold{*AddEs} \indexbold{*AddDs} are used to add rules to the current claset. They work exactly like their lower case counterparts, such as \texttt{addSIs}. Calling \begin{ttbox} Delrules : thm list -> unit \end{ttbox} deletes rules from the current claset. \medskip A few further functions are available as uppercase versions only: \begin{ttbox} AddXIs, AddXEs, AddXDs: thm list -> unit \end{ttbox} \indexbold{*AddXIs} \indexbold{*AddXEs} \indexbold{*AddXDs} augment the current claset by \emph{extra} introduction, elimination, or destruct rules. These provide additional hints for the basic non-automated proof methods of Isabelle/Isar \cite{isabelle-isar-ref}. The corresponding Isar attributes are ``$intro?$'', ``$elim?$'', and ``$dest?$''. Note that these extra rules do not have any effect on classic Isabelle tactics. \subsection{Accessing the current claset} \label{sec:access-current-claset} the functions to access the current claset are analogous to the functions for the current simpset, so please see \ref{sec:access-current-simpset} for a description. \begin{ttbox} claset : unit -> claset claset_ref : unit -> claset ref claset_of : theory -> claset claset_ref_of : theory -> claset ref print_claset : theory -> unit CLASET :(claset -> tactic) -> tactic CLASET' :(claset -> 'a -> tactic) -> 'a -> tactic CLASIMPSET :(clasimpset -> tactic) -> tactic CLASIMPSET' :(clasimpset -> 'a -> tactic) -> 'a -> tactic \end{ttbox} \subsection{Other useful tactics} \index{tactics!for contradiction} \index{tactics!for Modus Ponens} \begin{ttbox} contr_tac : int -> tactic mp_tac : int -> tactic eq_mp_tac : int -> tactic swap_res_tac : thm list -> int -> tactic \end{ttbox} These can be used in the body of a specialized search. \begin{ttdescription} \item[\ttindexbold{contr_tac} {\it i}]\index{assumptions!contradictory} solves subgoal~$i$ by detecting a contradiction among two assumptions of the form $P$ and~$\neg P$, or fail. It may instantiate unknowns. The tactic can produce multiple outcomes, enumerating all possible contradictions. \item[\ttindexbold{mp_tac} {\it i}] is like \texttt{contr_tac}, but also attempts to perform Modus Ponens in subgoal~$i$. If there are assumptions $P\imp Q$ and~$P$, then it replaces $P\imp Q$ by~$Q$. It may instantiate unknowns. It fails if it can do nothing. \item[\ttindexbold{eq_mp_tac} {\it i}] is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it is safe. \item[\ttindexbold{swap_res_tac} {\it thms} {\it i}] refines subgoal~$i$ of the proof state using {\it thms}, which should be a list of introduction rules. First, it attempts to prove the goal using \texttt{assume_tac} or \texttt{contr_tac}. It then attempts to apply each rule in turn, attempting resolution and also elim-resolution with the swapped form. \end{ttdescription} \subsection{Creating swapped rules} \begin{ttbox} swapify : thm list -> thm list joinrules : thm list * thm list -> (bool * thm) list \end{ttbox} \begin{ttdescription} \item[\ttindexbold{swapify} {\it thms}] returns a list consisting of the swapped versions of~{\it thms}, regarded as introduction rules. \item[\ttindexbold{joinrules} ({\it intrs}, {\it elims})] joins introduction rules, their swapped versions, and elimination rules for use with \ttindex{biresolve_tac}. Each rule is paired with~\texttt{false} (indicating ordinary resolution) or~\texttt{true} (indicating elim-resolution). \end{ttdescription} \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}: \begin{ttbox} signature CLASSICAL_DATA = sig val mp : thm val not_elim : thm val swap : thm val sizef : thm -> int val hyp_subst_tacs : (int -> tactic) list end; \end{ttbox} Thus, the functor requires the following items: \begin{ttdescription} \item[\tdxbold{mp}] should be the Modus Ponens rule $\List{\Var{P}\imp\Var{Q};\; \Var{P}} \Imp \Var{Q}$. \item[\tdxbold{not_elim}] should be the contradiction rule $\List{\neg\Var{P};\; \Var{P}} \Imp \Var{R}$. \item[\tdxbold{swap}] should be the swap rule $\List{\neg \Var{P}; \; \neg \Var{R}\Imp \Var{P}} \Imp \Var{R}$. \item[\ttindexbold{sizef}] is the heuristic function used for best-first search. It should estimate the size of the remaining subgoals. A good heuristic function is \ttindex{size_of_thm}, which measures the size of the proof state. Another size function might ignore certain subgoals (say, those concerned with type-checking). A heuristic function might simply count the subgoals. \item[\ttindexbold{hyp_subst_tacs}] is a list of tactics for substitution in the hypotheses, typically created by \ttindex{HypsubstFun} (see Chapter~\ref{substitution}). This list can, of course, be empty. The tactics are assumed to be safe! \end{ttdescription} The functor is not at all sensitive to the formalization of the object-logic. It does not even examine the rules, but merely applies them according to its fixed strategy. The functor resides in {\tt Provers/classical.ML} in the Isabelle sources. \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" %%% End: