doc-src/ZF/FOL.tex
 changeset 6121 5fe77b9b5185 child 8249 3fc32155372c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/ZF/FOL.tex	Wed Jan 13 16:36:36 1999 +0100
1.3 @@ -0,0 +1,936 @@
1.4 +%% $Id$
1.5 +\chapter{First-Order Logic}
1.6 +\index{first-order logic|(}
1.7 +
1.8 +Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc
1.9 +  nk}.  Intuitionistic first-order logic is defined first, as theory
1.10 +\thydx{IFOL}.  Classical logic, theory \thydx{FOL}, is
1.11 +obtained by adding the double negation rule.  Basic proof procedures are
1.12 +provided.  The intuitionistic prover works with derived rules to simplify
1.13 +implications in the assumptions.  Classical~\texttt{FOL} employs Isabelle's
1.14 +classical reasoner, which simulates a sequent calculus.
1.15 +
1.16 +\section{Syntax and rules of inference}
1.17 +The logic is many-sorted, using Isabelle's type classes.  The class of
1.18 +first-order terms is called \cldx{term} and is a subclass of \texttt{logic}.
1.19 +No types of individuals are provided, but extensions can define types such
1.20 +as \texttt{nat::term} and type constructors such as \texttt{list::(term)term}
1.21 +(see the examples directory, \texttt{FOL/ex}).  Below, the type variable
1.22 +$\alpha$ ranges over class \texttt{term}; the equality symbol and quantifiers
1.23 +are polymorphic (many-sorted).  The type of formulae is~\tydx{o}, which
1.24 +belongs to class~\cldx{logic}.  Figure~\ref{fol-syntax} gives the syntax.
1.25 +Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$.
1.26 +
1.27 +Figure~\ref{fol-rules} shows the inference rules with their~\ML\ names.
1.28 +Negation is defined in the usual way for intuitionistic logic; $\neg P$
1.29 +abbreviates $P\imp\bot$.  The biconditional~($\bimp$) is defined through
1.30 +$\conj$ and~$\imp$; introduction and elimination rules are derived for it.
1.31 +
1.32 +The unique existence quantifier, $\exists!x.P(x)$, is defined in terms
1.33 +of~$\exists$ and~$\forall$.  An Isabelle binder, it admits nested
1.34 +quantifications.  For instance, $\exists!x\;y.P(x,y)$ abbreviates
1.35 +$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
1.36 +exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
1.37 +
1.38 +Some intuitionistic derived rules are shown in
1.39 +Fig.\ts\ref{fol-int-derived}, again with their \ML\ names.  These include
1.40 +rules for the defined symbols $\neg$, $\bimp$ and $\exists!$.  Natural
1.41 +deduction typically involves a combination of forward and backward
1.42 +reasoning, particularly with the destruction rules $(\conj E)$,
1.43 +$({\imp}E)$, and~$(\forall E)$.  Isabelle's backward style handles these
1.44 +rules badly, so sequent-style rules are derived to eliminate conjunctions,
1.45 +implications, and universal quantifiers.  Used with elim-resolution,
1.46 +\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE}
1.47 +re-inserts the quantified formula for later use.  The rules {\tt
1.48 +conj_impE}, etc., support the intuitionistic proof procedure
1.49 +(see~\S\ref{fol-int-prover}).
1.50 +
1.51 +See the files \texttt{FOL/IFOL.thy}, \texttt{FOL/IFOL.ML} and
1.52 +\texttt{FOL/intprover.ML} for complete listings of the rules and
1.53 +derived rules.
1.54 +
1.55 +\begin{figure}
1.56 +\begin{center}
1.57 +\begin{tabular}{rrr}
1.58 +  \it name      &\it meta-type  & \it description \\
1.59 +  \cdx{Trueprop}& $o\To prop$           & coercion to $prop$\\
1.60 +  \cdx{Not}     & $o\To o$              & negation ($\neg$) \\
1.61 +  \cdx{True}    & $o$                   & tautology ($\top$) \\
1.62 +  \cdx{False}   & $o$                   & absurdity ($\bot$)
1.63 +\end{tabular}
1.64 +\end{center}
1.65 +\subcaption{Constants}
1.66 +
1.67 +\begin{center}
1.68 +\begin{tabular}{llrrr}
1.69 +  \it symbol &\it name     &\it meta-type & \it priority & \it description \\
1.70 +  \sdx{ALL}  & \cdx{All}  & $(\alpha\To o)\To o$ & 10 &
1.71 +        universal quantifier ($\forall$) \\
1.72 +  \sdx{EX}   & \cdx{Ex}   & $(\alpha\To o)\To o$ & 10 &
1.73 +        existential quantifier ($\exists$) \\
1.74 +  \texttt{EX!}  & \cdx{Ex1}  & $(\alpha\To o)\To o$ & 10 &
1.75 +        unique existence ($\exists!$)
1.76 +\end{tabular}
1.77 +\index{*"E"X"! symbol}
1.78 +\end{center}
1.79 +\subcaption{Binders}
1.80 +
1.81 +\begin{center}
1.82 +\index{*"= symbol}
1.83 +\index{&@{\tt\&} symbol}
1.84 +\index{*"| symbol}
1.85 +\index{*"-"-"> symbol}
1.86 +\index{*"<"-"> symbol}
1.87 +\begin{tabular}{rrrr}
1.88 +  \it symbol    & \it meta-type         & \it priority & \it description \\
1.89 +  \tt =         & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\
1.90 +  \tt \&        & $[o,o]\To o$          & Right 35 & conjunction ($\conj$) \\
1.91 +  \tt |         & $[o,o]\To o$          & Right 30 & disjunction ($\disj$) \\
1.92 +  \tt -->       & $[o,o]\To o$          & Right 25 & implication ($\imp$) \\
1.93 +  \tt <->       & $[o,o]\To o$          & Right 25 & biconditional ($\bimp$)
1.94 +\end{tabular}
1.95 +\end{center}
1.96 +\subcaption{Infixes}
1.97 +
1.98 +\dquotes
1.99 +$\begin{array}{rcl} 1.100 + formula & = & \hbox{expression of type~o} \\ 1.101 + & | & term " = " term \quad| \quad term " \ttilde= " term \\ 1.102 + & | & "\ttilde\ " formula \\ 1.103 + & | & formula " \& " formula \\ 1.104 + & | & formula " | " formula \\ 1.105 + & | & formula " --> " formula \\ 1.106 + & | & formula " <-> " formula \\ 1.107 + & | & "ALL~" id~id^* " . " formula \\ 1.108 + & | & "EX~~" id~id^* " . " formula \\ 1.109 + & | & "EX!~" id~id^* " . " formula 1.110 + \end{array} 1.111 +$
1.112 +\subcaption{Grammar}
1.113 +\caption{Syntax of \texttt{FOL}} \label{fol-syntax}
1.114 +\end{figure}
1.115 +
1.116 +
1.117 +\begin{figure}
1.118 +\begin{ttbox}
1.119 +\tdx{refl}        a=a
1.120 +\tdx{subst}       [| a=b;  P(a) |] ==> P(b)
1.121 +\subcaption{Equality rules}
1.122 +
1.123 +\tdx{conjI}       [| P;  Q |] ==> P&Q
1.124 +\tdx{conjunct1}   P&Q ==> P
1.125 +\tdx{conjunct2}   P&Q ==> Q
1.126 +
1.127 +\tdx{disjI1}      P ==> P|Q
1.128 +\tdx{disjI2}      Q ==> P|Q
1.129 +\tdx{disjE}       [| P|Q;  P ==> R;  Q ==> R |] ==> R
1.130 +
1.131 +\tdx{impI}        (P ==> Q) ==> P-->Q
1.132 +\tdx{mp}          [| P-->Q;  P |] ==> Q
1.133 +
1.134 +\tdx{FalseE}      False ==> P
1.135 +\subcaption{Propositional rules}
1.136 +
1.137 +\tdx{allI}        (!!x. P(x))  ==> (ALL x.P(x))
1.138 +\tdx{spec}        (ALL x.P(x)) ==> P(x)
1.139 +
1.140 +\tdx{exI}         P(x) ==> (EX x.P(x))
1.141 +\tdx{exE}         [| EX x.P(x);  !!x. P(x) ==> R |] ==> R
1.142 +\subcaption{Quantifier rules}
1.143 +
1.144 +\tdx{True_def}    True        == False-->False
1.145 +\tdx{not_def}     ~P          == P-->False
1.146 +\tdx{iff_def}     P<->Q       == (P-->Q) & (Q-->P)
1.147 +\tdx{ex1_def}     EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)
1.148 +\subcaption{Definitions}
1.149 +\end{ttbox}
1.150 +
1.151 +\caption{Rules of intuitionistic logic} \label{fol-rules}
1.152 +\end{figure}
1.153 +
1.154 +
1.155 +\begin{figure}
1.156 +\begin{ttbox}
1.157 +\tdx{sym}       a=b ==> b=a
1.158 +\tdx{trans}     [| a=b;  b=c |] ==> a=c
1.159 +\tdx{ssubst}    [| b=a;  P(a) |] ==> P(b)
1.160 +\subcaption{Derived equality rules}
1.161 +
1.162 +\tdx{TrueI}     True
1.163 +
1.164 +\tdx{notI}      (P ==> False) ==> ~P
1.165 +\tdx{notE}      [| ~P;  P |] ==> R
1.166 +
1.167 +\tdx{iffI}      [| P ==> Q;  Q ==> P |] ==> P<->Q
1.168 +\tdx{iffE}      [| P <-> Q;  [| P-->Q; Q-->P |] ==> R |] ==> R
1.169 +\tdx{iffD1}     [| P <-> Q;  P |] ==> Q
1.170 +\tdx{iffD2}     [| P <-> Q;  Q |] ==> P
1.171 +
1.172 +\tdx{ex1I}      [| P(a);  !!x. P(x) ==> x=a |]  ==>  EX! x. P(x)
1.173 +\tdx{ex1E}      [| EX! x.P(x);  !!x.[| P(x);  ALL y. P(y) --> y=x |] ==> R
1.174 +          |] ==> R
1.175 +\subcaption{Derived rules for $$\top$$, $$\neg$$, $$\bimp$$ and $$\exists!$$}
1.176 +
1.177 +\tdx{conjE}     [| P&Q;  [| P; Q |] ==> R |] ==> R
1.178 +\tdx{impE}      [| P-->Q;  P;  Q ==> R |] ==> R
1.179 +\tdx{allE}      [| ALL x.P(x);  P(x) ==> R |] ==> R
1.180 +\tdx{all_dupE}  [| ALL x.P(x);  [| P(x); ALL x.P(x) |] ==> R |] ==> R
1.181 +\subcaption{Sequent-style elimination rules}
1.182 +
1.183 +\tdx{conj_impE} [| (P&Q)-->S;  P-->(Q-->S) ==> R |] ==> R
1.184 +\tdx{disj_impE} [| (P|Q)-->S;  [| P-->S; Q-->S |] ==> R |] ==> R
1.185 +\tdx{imp_impE}  [| (P-->Q)-->S;  [| P; Q-->S |] ==> Q;  S ==> R |] ==> R
1.186 +\tdx{not_impE}  [| ~P --> S;  P ==> False;  S ==> R |] ==> R
1.187 +\tdx{iff_impE}  [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P;
1.188 +             S ==> R |] ==> R
1.189 +\tdx{all_impE}  [| (ALL x.P(x))-->S;  !!x.P(x);  S ==> R |] ==> R
1.190 +\tdx{ex_impE}   [| (EX x.P(x))-->S;  P(a)-->S ==> R |] ==> R
1.191 +\end{ttbox}
1.192 +\subcaption{Intuitionistic simplification of implication}
1.193 +\caption{Derived rules for intuitionistic logic} \label{fol-int-derived}
1.194 +\end{figure}
1.195 +
1.196 +
1.197 +\section{Generic packages}
1.198 +\FOL{} instantiates most of Isabelle's generic packages.
1.199 +\begin{itemize}
1.200 +\item
1.201 +It instantiates the simplifier.  Both equality ($=$) and the biconditional
1.202 +($\bimp$) may be used for rewriting.  Tactics such as \texttt{Asm_simp_tac} and
1.203 +\texttt{Full_simp_tac} refer to the default simpset (\texttt{simpset()}), which works for
1.204 +most purposes.  Named simplification sets include \ttindexbold{IFOL_ss},
1.205 +for intuitionistic first-order logic, and \ttindexbold{FOL_ss},
1.206 +for classical logic.  See the file
1.207 +\texttt{FOL/simpdata.ML} for a complete listing of the simplification
1.208 +rules%
1.209 +\iflabelundefined{sec:setting-up-simp}{}%
1.210 +        {, and \S\ref{sec:setting-up-simp} for discussion}.
1.211 +
1.212 +\item
1.213 +It instantiates the classical reasoner.  See~\S\ref{fol-cla-prover}
1.214 +for details.
1.215 +
1.216 +\item \FOL{} provides the tactic \ttindex{hyp_subst_tac}, which substitutes
1.217 +  for an equality throughout a subgoal and its hypotheses.  This tactic uses
1.218 +  \FOL's general substitution rule.
1.219 +\end{itemize}
1.220 +
1.221 +\begin{warn}\index{simplification!of conjunctions}%
1.222 +  Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The
1.223 +  left part of a conjunction helps in simplifying the right part.  This effect
1.224 +  is not available by default: it can be slow.  It can be obtained by
1.225 +  including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
1.226 +\end{warn}
1.227 +
1.228 +
1.229 +\section{Intuitionistic proof procedures} \label{fol-int-prover}
1.230 +Implication elimination (the rules~\texttt{mp} and~\texttt{impE}) pose
1.231 +difficulties for automated proof.  In intuitionistic logic, the assumption
1.232 +$P\imp Q$ cannot be treated like $\neg P\disj Q$.  Given $P\imp Q$, we may
1.233 +use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated
1.234 +use of $P\imp Q$.  If the proof of~$P$ fails then the whole branch of the
1.235 +proof must be abandoned.  Thus intuitionistic propositional logic requires
1.236 +backtracking.
1.237 +
1.238 +For an elementary example, consider the intuitionistic proof of $Q$ from
1.239 +$P\imp Q$ and $(P\imp Q)\imp P$.  The implication $P\imp Q$ is needed
1.240 +twice:
1.241 +$\infer[({\imp}E)]{Q}{P\imp Q & 1.242 + \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} 1.243 +$
1.244 +The theorem prover for intuitionistic logic does not use~\texttt{impE}.\@
1.245 +Instead, it simplifies implications using derived rules
1.246 +(Fig.\ts\ref{fol-int-derived}).  It reduces the antecedents of implications
1.247 +to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$.
1.248 +The rules \tdx{conj_impE} and \tdx{disj_impE} are
1.249 +straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and
1.250 +$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp 1.251 +S$.  The other \ldots{\tt_impE} rules are unsafe; the method requires
1.252 +backtracking.  All the rules are derived in the same simple manner.
1.253 +
1.254 +Dyckhoff has independently discovered similar rules, and (more importantly)
1.255 +has demonstrated their completeness for propositional
1.256 +logic~\cite{dyckhoff}.  However, the tactics given below are not complete
1.257 +for first-order logic because they discard universally quantified
1.258 +assumptions after a single use.
1.259 +\begin{ttbox}
1.260 +mp_tac              : int -> tactic
1.261 +eq_mp_tac           : int -> tactic
1.262 +IntPr.safe_step_tac : int -> tactic
1.263 +IntPr.safe_tac      :        tactic
1.264 +IntPr.inst_step_tac : int -> tactic
1.265 +IntPr.step_tac      : int -> tactic
1.266 +IntPr.fast_tac      : int -> tactic
1.267 +IntPr.best_tac      : int -> tactic
1.268 +\end{ttbox}
1.269 +Most of these belong to the structure \texttt{IntPr} and resemble the
1.270 +tactics of Isabelle's classical reasoner.
1.271 +
1.272 +\begin{ttdescription}
1.273 +\item[\ttindexbold{mp_tac} {\it i}]
1.274 +attempts to use \tdx{notE} or \tdx{impE} within the assumptions in
1.275 +subgoal $i$.  For each assumption of the form $\neg P$ or $P\imp Q$, it
1.276 +searches for another assumption unifiable with~$P$.  By
1.277 +contradiction with $\neg P$ it can solve the subgoal completely; by Modus
1.278 +Ponens it can replace the assumption $P\imp Q$ by $Q$.  The tactic can
1.279 +produce multiple outcomes, enumerating all suitable pairs of assumptions.
1.280 +
1.281 +\item[\ttindexbold{eq_mp_tac} {\it i}]
1.282 +is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it
1.283 +is safe.
1.284 +
1.285 +\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on
1.286 +subgoal~$i$.  This may include proof by assumption or Modus Ponens (taking
1.287 +care not to instantiate unknowns), or \texttt{hyp_subst_tac}.
1.288 +
1.289 +\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all
1.290 +subgoals.  It is deterministic, with at most one outcome.
1.291 +
1.292 +\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac},
1.293 +but allows unknowns to be instantiated.
1.294 +
1.295 +\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt
1.296 +    inst_step_tac}, or applies an unsafe rule.  This is the basic step of
1.297 +  the intuitionistic proof procedure.
1.298 +
1.299 +\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using
1.300 +depth-first search, to solve subgoal~$i$.
1.301 +
1.302 +\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using
1.303 +best-first search (guided by the size of the proof state) to solve subgoal~$i$.
1.304 +\end{ttdescription}
1.305 +Here are some of the theorems that \texttt{IntPr.fast_tac} proves
1.306 +automatically.  The latter three date from {\it Principia Mathematica}
1.307 +(*11.53, *11.55, *11.61)~\cite{principia}.
1.308 +\begin{ttbox}
1.309 +~~P & ~~(P --> Q) --> ~~Q
1.310 +(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))
1.311 +(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))
1.312 +(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))
1.313 +\end{ttbox}
1.314 +
1.315 +
1.316 +
1.317 +\begin{figure}
1.318 +\begin{ttbox}
1.319 +\tdx{excluded_middle}    ~P | P
1.320 +
1.321 +\tdx{disjCI}    (~Q ==> P) ==> P|Q
1.322 +\tdx{exCI}      (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x)
1.323 +\tdx{impCE}     [| P-->Q; ~P ==> R; Q ==> R |] ==> R
1.324 +\tdx{iffCE}     [| P<->Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R
1.325 +\tdx{notnotD}   ~~P ==> P
1.326 +\tdx{swap}      ~P ==> (~Q ==> P) ==> Q
1.327 +\end{ttbox}
1.328 +\caption{Derived rules for classical logic} \label{fol-cla-derived}
1.329 +\end{figure}
1.330 +
1.331 +
1.332 +\section{Classical proof procedures} \label{fol-cla-prover}
1.333 +The classical theory, \thydx{FOL}, consists of intuitionistic logic plus
1.334 +the rule
1.335 +$$\vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical)$$
1.336 +\noindent
1.337 +Natural deduction in classical logic is not really all that natural.
1.338 +{\FOL} derives classical introduction rules for $\disj$ and~$\exists$, as
1.339 +well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
1.340 +rule (see Fig.\ts\ref{fol-cla-derived}).
1.341 +
1.342 +The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and {\tt
1.343 +Best_tac} refer to the default claset (\texttt{claset()}), which works for most
1.344 +purposes.  Named clasets include \ttindexbold{prop_cs}, which includes the
1.345 +propositional rules, and \ttindexbold{FOL_cs}, which also includes quantifier
1.346 +rules.  See the file \texttt{FOL/cladata.ML} for lists of the
1.347 +classical rules, and
1.348 +\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
1.349 +        {Chap.\ts\ref{chap:classical}}
1.350 +for more discussion of classical proof methods.
1.351 +
1.352 +
1.353 +\section{An intuitionistic example}
1.354 +Here is a session similar to one in {\em Logic and Computation}
1.355 +\cite[pages~222--3]{paulson87}.  Isabelle treats quantifiers differently
1.356 +from {\sc lcf}-based theorem provers such as {\sc hol}.
1.357 +
1.358 +First, we specify that we are working in intuitionistic logic:
1.359 +\begin{ttbox}
1.360 +context IFOL.thy;
1.361 +\end{ttbox}
1.362 +The proof begins by entering the goal, then applying the rule $({\imp}I)$.
1.363 +\begin{ttbox}
1.364 +Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
1.365 +{\out Level 0}
1.366 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.367 +{\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.368 +\ttbreak
1.369 +by (resolve_tac [impI] 1);
1.370 +{\out Level 1}
1.371 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.372 +{\out  1. EX y. ALL x. Q(x,y) ==> ALL x. EX y. Q(x,y)}
1.373 +\end{ttbox}
1.374 +In this example, we shall never have more than one subgoal.  Applying
1.375 +$({\imp}I)$ replaces~\verb|-->| by~\verb|==>|, making
1.376 +$$\ex{y}\all{x}Q(x,y)$$ an assumption.  We have the choice of
1.377 +$({\exists}E)$ and $({\forall}I)$; let us try the latter.
1.378 +\begin{ttbox}
1.379 +by (resolve_tac [allI] 1);
1.380 +{\out Level 2}
1.381 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.382 +{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
1.383 +\end{ttbox}
1.384 +Applying $({\forall}I)$ replaces the \texttt{ALL~x} by \hbox{\tt!!x},
1.385 +changing the universal quantifier from object~($\forall$) to
1.386 +meta~($\Forall$).  The bound variable is a {\bf parameter} of the
1.387 +subgoal.  We now must choose between $({\exists}I)$ and $({\exists}E)$.  What
1.388 +happens if the wrong rule is chosen?
1.389 +\begin{ttbox}
1.390 +by (resolve_tac [exI] 1);
1.391 +{\out Level 3}
1.392 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.393 +{\out  1. !!x. EX y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
1.394 +\end{ttbox}
1.395 +The new subgoal~1 contains the function variable {\tt?y2}.  Instantiating
1.396 +{\tt?y2} can replace~{\tt?y2(x)} by a term containing~\texttt{x}, even
1.397 +though~\texttt{x} is a bound variable.  Now we analyse the assumption
1.398 +$$\exists y.\forall x. Q(x,y)$$ using elimination rules:
1.399 +\begin{ttbox}
1.400 +by (eresolve_tac [exE] 1);
1.401 +{\out Level 4}
1.402 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.403 +{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y2(x))}
1.404 +\end{ttbox}
1.405 +Applying $(\exists E)$ has produced the parameter \texttt{y} and stripped the
1.406 +existential quantifier from the assumption.  But the subgoal is unprovable:
1.407 +there is no way to unify \texttt{?y2(x)} with the bound variable~\texttt{y}.
1.408 +Using \texttt{choplev} we can return to the critical point.  This time we
1.409 +apply $({\exists}E)$:
1.410 +\begin{ttbox}
1.411 +choplev 2;
1.412 +{\out Level 2}
1.413 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.414 +{\out  1. !!x. EX y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
1.415 +\ttbreak
1.416 +by (eresolve_tac [exE] 1);
1.417 +{\out Level 3}
1.418 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.419 +{\out  1. !!x y. ALL x. Q(x,y) ==> EX y. Q(x,y)}
1.420 +\end{ttbox}
1.421 +We now have two parameters and no scheme variables.  Applying
1.422 +$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are
1.423 +applied to those parameters.  Parameters should be produced early, as this
1.424 +example demonstrates.
1.425 +\begin{ttbox}
1.426 +by (resolve_tac [exI] 1);
1.427 +{\out Level 4}
1.428 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.429 +{\out  1. !!x y. ALL x. Q(x,y) ==> Q(x,?y3(x,y))}
1.430 +\ttbreak
1.431 +by (eresolve_tac [allE] 1);
1.432 +{\out Level 5}
1.433 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.434 +{\out  1. !!x y. Q(?x4(x,y),y) ==> Q(x,?y3(x,y))}
1.435 +\end{ttbox}
1.436 +The subgoal has variables \texttt{?y3} and \texttt{?x4} applied to both
1.437 +parameters.  The obvious projection functions unify {\tt?x4(x,y)} with~{\tt
1.438 +x} and \verb|?y3(x,y)| with~\texttt{y}.
1.439 +\begin{ttbox}
1.440 +by (assume_tac 1);
1.441 +{\out Level 6}
1.442 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.443 +{\out No subgoals!}
1.444 +\end{ttbox}
1.445 +The theorem was proved in six tactic steps, not counting the abandoned
1.446 +ones.  But proof checking is tedious; \ttindex{IntPr.fast_tac} proves the
1.447 +theorem in one step.
1.448 +\begin{ttbox}
1.449 +Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
1.450 +{\out Level 0}
1.451 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.452 +{\out  1. (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.453 +by (IntPr.fast_tac 1);
1.454 +{\out Level 1}
1.455 +{\out (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))}
1.456 +{\out No subgoals!}
1.457 +\end{ttbox}
1.458 +
1.459 +
1.460 +\section{An example of intuitionistic negation}
1.461 +The following example demonstrates the specialized forms of implication
1.462 +elimination.  Even propositional formulae can be difficult to prove from
1.463 +the basic rules; the specialized rules help considerably.
1.464 +
1.465 +Propositional examples are easy to invent.  As Dummett notes~\cite[page
1.466 +28]{dummett}, $\neg P$ is classically provable if and only if it is
1.467 +intuitionistically provable;  therefore, $P$ is classically provable if and
1.468 +only if $\neg\neg P$ is intuitionistically provable.%
1.469 +\footnote{Of course this holds only for propositional logic, not if $P$ is
1.470 +  allowed to contain quantifiers.} Proving $\neg\neg P$ intuitionistically is
1.471 +much harder than proving~$P$ classically.
1.472 +
1.473 +Our example is the double negation of the classical tautology $(P\imp 1.474 +Q)\disj (Q\imp P)$.  When stating the goal, we command Isabelle to expand
1.475 +negations to implications using the definition $\neg P\equiv P\imp\bot$.
1.476 +This allows use of the special implication rules.
1.477 +\begin{ttbox}
1.478 +Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
1.479 +{\out Level 0}
1.480 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.481 +{\out  1. ((P --> Q) | (Q --> P) --> False) --> False}
1.482 +\end{ttbox}
1.483 +The first step is trivial.
1.484 +\begin{ttbox}
1.485 +by (resolve_tac [impI] 1);
1.486 +{\out Level 1}
1.487 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.488 +{\out  1. (P --> Q) | (Q --> P) --> False ==> False}
1.489 +\end{ttbox}
1.490 +By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but
1.491 +that formula is not a theorem of intuitionistic logic.  Instead we apply
1.492 +the specialized implication rule \tdx{disj_impE}.  It splits the
1.493 +assumption into two assumptions, one for each disjunct.
1.494 +\begin{ttbox}
1.495 +by (eresolve_tac [disj_impE] 1);
1.496 +{\out Level 2}
1.497 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.498 +{\out  1. [| (P --> Q) --> False; (Q --> P) --> False |] ==> False}
1.499 +\end{ttbox}
1.500 +We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but
1.501 +their negations are inconsistent.  Applying \tdx{imp_impE} breaks down
1.502 +the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new
1.503 +assumptions~$P$ and~$\neg Q$.
1.504 +\begin{ttbox}
1.505 +by (eresolve_tac [imp_impE] 1);
1.506 +{\out Level 3}
1.507 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.508 +{\out  1. [| (Q --> P) --> False; P; Q --> False |] ==> Q}
1.509 +{\out  2. [| (Q --> P) --> False; False |] ==> False}
1.510 +\end{ttbox}
1.511 +Subgoal~2 holds trivially; let us ignore it and continue working on
1.512 +subgoal~1.  Thanks to the assumption~$P$, we could prove $Q\imp P$;
1.513 +applying \tdx{imp_impE} is simpler.
1.514 +\begin{ttbox}
1.515 +by (eresolve_tac [imp_impE] 1);
1.516 +{\out Level 4}
1.517 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.518 +{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
1.519 +{\out  2. [| P; Q --> False; False |] ==> Q}
1.520 +{\out  3. [| (Q --> P) --> False; False |] ==> False}
1.521 +\end{ttbox}
1.522 +The three subgoals are all trivial.
1.523 +\begin{ttbox}
1.524 +by (REPEAT (eresolve_tac [FalseE] 2));
1.525 +{\out Level 5}
1.526 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.527 +{\out  1. [| P; Q --> False; Q; P --> False |] ==> P}
1.528 +\ttbreak
1.529 +by (assume_tac 1);
1.530 +{\out Level 6}
1.531 +{\out ~ ~ ((P --> Q) | (Q --> P))}
1.532 +{\out No subgoals!}
1.533 +\end{ttbox}
1.534 +This proof is also trivial for \texttt{IntPr.fast_tac}.
1.535 +
1.536 +
1.537 +\section{A classical example} \label{fol-cla-example}
1.538 +To illustrate classical logic, we shall prove the theorem
1.539 +$\ex{y}\all{x}P(y)\imp P(x)$.  Informally, the theorem can be proved as
1.540 +follows.  Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise
1.541 +$\all{x}P(x)$ is true.  Either way the theorem holds.  First, we switch to
1.542 +classical logic:
1.543 +\begin{ttbox}
1.544 +context FOL.thy;
1.545 +\end{ttbox}
1.546 +
1.547 +The formal proof does not conform in any obvious way to the sketch given
1.548 +above.  The key inference is the first one, \tdx{exCI}; this classical
1.549 +version of~$(\exists I)$ allows multiple instantiation of the quantifier.
1.550 +\begin{ttbox}
1.551 +Goal "EX y. ALL x. P(y)-->P(x)";
1.552 +{\out Level 0}
1.553 +{\out EX y. ALL x. P(y) --> P(x)}
1.554 +{\out  1. EX y. ALL x. P(y) --> P(x)}
1.555 +\ttbreak
1.556 +by (resolve_tac [exCI] 1);
1.557 +{\out Level 1}
1.558 +{\out EX y. ALL x. P(y) --> P(x)}
1.559 +{\out  1. ALL y. ~ (ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)}
1.560 +\end{ttbox}
1.561 +We can either exhibit a term {\tt?a} to satisfy the conclusion of
1.562 +subgoal~1, or produce a contradiction from the assumption.  The next
1.563 +steps are routine.
1.564 +\begin{ttbox}
1.565 +by (resolve_tac [allI] 1);
1.566 +{\out Level 2}
1.567 +{\out EX y. ALL x. P(y) --> P(x)}
1.568 +{\out  1. !!x. ALL y. ~ (ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)}
1.569 +\ttbreak
1.570 +by (resolve_tac [impI] 1);
1.571 +{\out Level 3}
1.572 +{\out EX y. ALL x. P(y) --> P(x)}
1.573 +{\out  1. !!x. [| ALL y. ~ (ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)}
1.574 +\end{ttbox}
1.575 +By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$
1.576 +in effect applies~$(\exists I)$ again.
1.577 +\begin{ttbox}
1.578 +by (eresolve_tac [allE] 1);
1.579 +{\out Level 4}
1.580 +{\out EX y. ALL x. P(y) --> P(x)}
1.581 +{\out  1. !!x. [| P(?a); ~ (ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)}
1.582 +\end{ttbox}
1.583 +In classical logic, a negated assumption is equivalent to a conclusion.  To
1.584 +get this effect, we create a swapped version of~$(\forall I)$ and apply it
1.585 +using \ttindex{eresolve_tac}; we could equivalently have applied~$(\forall 1.586 +I)$ using \ttindex{swap_res_tac}.
1.587 +\begin{ttbox}
1.588 +allI RSN (2,swap);
1.589 +{\out val it = "[| ~ (ALL x. ?P1(x)); !!x. ~ ?Q ==> ?P1(x) |] ==> ?Q" : thm}
1.590 +by (eresolve_tac [it] 1);
1.591 +{\out Level 5}
1.592 +{\out EX y. ALL x. P(y) --> P(x)}
1.593 +{\out  1. !!x xa. [| P(?a); ~ P(x) |] ==> P(?y3(x)) --> P(xa)}
1.594 +\end{ttbox}
1.595 +The previous conclusion, \texttt{P(x)}, has become a negated assumption.
1.596 +\begin{ttbox}
1.597 +by (resolve_tac [impI] 1);
1.598 +{\out Level 6}
1.599 +{\out EX y. ALL x. P(y) --> P(x)}
1.600 +{\out  1. !!x xa. [| P(?a); ~ P(x); P(?y3(x)) |] ==> P(xa)}
1.601 +\end{ttbox}
1.602 +The subgoal has three assumptions.  We produce a contradiction between the
1.604 +  P(?y3(x))}.  The proof never instantiates the unknown~{\tt?a}.
1.605 +\begin{ttbox}
1.606 +by (eresolve_tac [notE] 1);
1.607 +{\out Level 7}
1.608 +{\out EX y. ALL x. P(y) --> P(x)}
1.609 +{\out  1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)}
1.610 +\ttbreak
1.611 +by (assume_tac 1);
1.612 +{\out Level 8}
1.613 +{\out EX y. ALL x. P(y) --> P(x)}
1.614 +{\out No subgoals!}
1.615 +\end{ttbox}
1.616 +The civilised way to prove this theorem is through \ttindex{Blast_tac},
1.617 +which automatically uses the classical version of~$(\exists I)$:
1.618 +\begin{ttbox}
1.619 +Goal "EX y. ALL x. P(y)-->P(x)";
1.620 +{\out Level 0}
1.621 +{\out EX y. ALL x. P(y) --> P(x)}
1.622 +{\out  1. EX y. ALL x. P(y) --> P(x)}
1.623 +by (Blast_tac 1);
1.624 +{\out Depth = 0}
1.625 +{\out Depth = 1}
1.626 +{\out Depth = 2}
1.627 +{\out Level 1}
1.628 +{\out EX y. ALL x. P(y) --> P(x)}
1.629 +{\out No subgoals!}
1.630 +\end{ttbox}
1.631 +If this theorem seems counterintuitive, then perhaps you are an
1.632 +intuitionist.  In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$
1.633 +requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$,
1.634 +which we cannot do without further knowledge about~$P$.
1.635 +
1.636 +
1.637 +\section{Derived rules and the classical tactics}
1.638 +Classical first-order logic can be extended with the propositional
1.639 +connective $if(P,Q,R)$, where
1.640 +$$if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if)$$
1.641 +Theorems about $if$ can be proved by treating this as an abbreviation,
1.642 +replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals.  But
1.643 +this duplicates~$P$, causing an exponential blowup and an unreadable
1.644 +formula.  Introducing further abbreviations makes the problem worse.
1.645 +
1.646 +Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$
1.647 +directly, without reference to its definition.  The simple identity
1.648 +$if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R)$
1.649 +suggests that the
1.650 +$if$-introduction rule should be
1.651 +$\infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}}$
1.652 +The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the
1.653 +elimination rules for~$\disj$ and~$\conj$.
1.654 +$\infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]} 1.655 + & \infer*{S}{[\neg P,R]}} 1.656 +$
1.657 +Having made these plans, we get down to work with Isabelle.  The theory of
1.658 +classical logic, \texttt{FOL}, is extended with the constant
1.659 +$if::[o,o,o]\To o$.  The axiom \tdx{if_def} asserts the
1.660 +equation~$(if)$.
1.661 +\begin{ttbox}
1.662 +If = FOL +
1.663 +consts  if     :: [o,o,o]=>o
1.664 +rules   if_def "if(P,Q,R) == P&Q | ~P&R"
1.665 +end
1.666 +\end{ttbox}
1.667 +We create the file \texttt{If.thy} containing these declarations.  (This file
1.668 +is on directory \texttt{FOL/ex} in the Isabelle distribution.)  Typing
1.669 +\begin{ttbox}
1.670 +use_thy "If";
1.671 +\end{ttbox}
1.672 +loads that theory and sets it to be the current context.
1.673 +
1.674 +
1.675 +\subsection{Deriving the introduction rule}
1.676 +
1.677 +The derivations of the introduction and elimination rules demonstrate the
1.678 +methods for rewriting with definitions.  Classical reasoning is required,
1.679 +so we use \texttt{blast_tac}.
1.680 +
1.681 +The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$,
1.682 +concludes $if(P,Q,R)$.  We propose the conclusion as the main goal
1.683 +using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences
1.684 +of $if$ in the subgoal.
1.685 +\begin{ttbox}
1.686 +val prems = Goalw [if_def]
1.687 +    "[| P ==> Q; ~ P ==> R |] ==> if(P,Q,R)";
1.688 +{\out Level 0}
1.689 +{\out if(P,Q,R)}
1.690 +{\out  1. P & Q | ~ P & R}
1.691 +\end{ttbox}
1.692 +The premises (bound to the {\ML} variable \texttt{prems}) are passed as
1.693 +introduction rules to \ttindex{blast_tac}.  Remember that \texttt{claset()} refers
1.694 +to the default classical set.
1.695 +\begin{ttbox}
1.696 +by (blast_tac (claset() addIs prems) 1);
1.697 +{\out Level 1}
1.698 +{\out if(P,Q,R)}
1.699 +{\out No subgoals!}
1.700 +qed "ifI";
1.701 +\end{ttbox}
1.702 +
1.703 +
1.704 +\subsection{Deriving the elimination rule}
1.705 +The elimination rule has three premises, two of which are themselves rules.
1.706 +The conclusion is simply $S$.
1.707 +\begin{ttbox}
1.708 +val major::prems = Goalw [if_def]
1.709 +   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~ P; R |] ==> S |] ==> S";
1.710 +{\out Level 0}
1.711 +{\out S}
1.712 +{\out  1. S}
1.713 +\end{ttbox}
1.714 +The major premise contains an occurrence of~$if$, but the version returned
1.715 +by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the
1.716 +definition expanded.  Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an
1.717 +assumption in the subgoal, so that \ttindex{blast_tac} can break it down.
1.718 +\begin{ttbox}
1.719 +by (cut_facts_tac [major] 1);
1.720 +{\out Level 1}
1.721 +{\out S}
1.722 +{\out  1. P & Q | ~ P & R ==> S}
1.723 +\ttbreak
1.724 +by (blast_tac (claset() addIs prems) 1);
1.725 +{\out Level 2}
1.726 +{\out S}
1.727 +{\out No subgoals!}
1.728 +qed "ifE";
1.729 +\end{ttbox}
1.730 +As you may recall from
1.731 +\iflabelundefined{definitions}{{\em Introduction to Isabelle}}%
1.732 +        {\S\ref{definitions}}, there are other
1.733 +ways of treating definitions when deriving a rule.  We can start the
1.734 +proof using \texttt{Goal}, which does not expand definitions, instead of
1.735 +\texttt{Goalw}.  We can use \ttindex{rew_tac}
1.736 +to expand definitions in the subgoals---perhaps after calling
1.737 +\ttindex{cut_facts_tac} to insert the rule's premises.  We can use
1.738 +\ttindex{rewrite_rule}, which is a meta-inference rule, to expand
1.739 +definitions in the premises directly.
1.740 +
1.741 +
1.742 +\subsection{Using the derived rules}
1.743 +The rules just derived have been saved with the {\ML} names \tdx{ifI}
1.744 +and~\tdx{ifE}.  They permit natural proofs of theorems such as the
1.745 +following:
1.746 +\begin{eqnarray*}
1.747 +    if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\
1.748 +    if(if(P,Q,R), A, B)         & \bimp & if(P,if(Q,A,B),if(R,A,B))
1.749 +\end{eqnarray*}
1.750 +Proofs also require the classical reasoning rules and the $\bimp$
1.751 +introduction rule (called~\tdx{iffI}: do not confuse with~\texttt{ifI}).
1.752 +
1.753 +To display the $if$-rules in action, let us analyse a proof step by step.
1.754 +\begin{ttbox}
1.755 +Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
1.756 +{\out Level 0}
1.757 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.758 +{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.759 +\ttbreak
1.760 +by (resolve_tac [iffI] 1);
1.761 +{\out Level 1}
1.762 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.763 +{\out  1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))}
1.764 +{\out  2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.765 +\end{ttbox}
1.766 +The $if$-elimination rule can be applied twice in succession.
1.767 +\begin{ttbox}
1.768 +by (eresolve_tac [ifE] 1);
1.769 +{\out Level 2}
1.770 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.771 +{\out  1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.772 +{\out  2. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.773 +{\out  3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.774 +\ttbreak
1.775 +by (eresolve_tac [ifE] 1);
1.776 +{\out Level 3}
1.777 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.778 +{\out  1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.779 +{\out  2. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.780 +{\out  3. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.781 +{\out  4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.782 +\end{ttbox}
1.783 +%
1.784 +In the first two subgoals, all assumptions have been reduced to atoms.  Now
1.785 +$if$-introduction can be applied.  Observe how the $if$-rules break down
1.786 +occurrences of $if$ when they become the outermost connective.
1.787 +\begin{ttbox}
1.788 +by (resolve_tac [ifI] 1);
1.789 +{\out Level 4}
1.790 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.791 +{\out  1. [| P; Q; A; Q |] ==> if(P,A,C)}
1.792 +{\out  2. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
1.793 +{\out  3. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.794 +{\out  4. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.795 +{\out  5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.796 +\ttbreak
1.797 +by (resolve_tac [ifI] 1);
1.798 +{\out Level 5}
1.799 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.800 +{\out  1. [| P; Q; A; Q; P |] ==> A}
1.801 +{\out  2. [| P; Q; A; Q; ~ P |] ==> C}
1.802 +{\out  3. [| P; Q; A; ~ Q |] ==> if(P,B,D)}
1.803 +{\out  4. [| P; ~ Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.804 +{\out  5. [| ~ P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))}
1.805 +{\out  6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))}
1.806 +\end{ttbox}
1.807 +Where do we stand?  The first subgoal holds by assumption; the second and
1.808 +third, by contradiction.  This is getting tedious.  We could use the classical
1.809 +reasoner, but first let us extend the default claset with the derived rules
1.810 +for~$if$.
1.811 +\begin{ttbox}
1.814 +\end{ttbox}
1.815 +Now we can revert to the
1.816 +initial proof state and let \ttindex{blast_tac} solve it.
1.817 +\begin{ttbox}
1.818 +choplev 0;
1.819 +{\out Level 0}
1.820 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.821 +{\out  1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.822 +by (Blast_tac 1);
1.823 +{\out Level 1}
1.824 +{\out if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))}
1.825 +{\out No subgoals!}
1.826 +\end{ttbox}
1.827 +This tactic also solves the other example.
1.828 +\begin{ttbox}
1.829 +Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
1.830 +{\out Level 0}
1.831 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.832 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.833 +\ttbreak
1.834 +by (Blast_tac 1);
1.835 +{\out Level 1}
1.836 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.837 +{\out No subgoals!}
1.838 +\end{ttbox}
1.839 +
1.840 +
1.841 +\subsection{Derived rules versus definitions}
1.842 +Dispensing with the derived rules, we can treat $if$ as an
1.843 +abbreviation, and let \ttindex{blast_tac} prove the expanded formula.  Let
1.844 +us redo the previous proof:
1.845 +\begin{ttbox}
1.846 +choplev 0;
1.847 +{\out Level 0}
1.848 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.849 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.850 +\end{ttbox}
1.851 +This time, simply unfold using the definition of $if$:
1.852 +\begin{ttbox}
1.853 +by (rewtac if_def);
1.854 +{\out Level 1}
1.855 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.856 +{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
1.857 +{\out     P & (Q & A | ~ Q & B) | ~ P & (R & A | ~ R & B)}
1.858 +\end{ttbox}
1.859 +We are left with a subgoal in pure first-order logic, which is why the
1.860 +classical reasoner can prove it given \texttt{FOL_cs} alone.  (We could, of
1.861 +course, have used \texttt{Blast_tac}.)
1.862 +\begin{ttbox}
1.863 +by (blast_tac FOL_cs 1);
1.864 +{\out Level 2}
1.865 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))}
1.866 +{\out No subgoals!}
1.867 +\end{ttbox}
1.868 +Expanding definitions reduces the extended logic to the base logic.  This
1.869 +approach has its merits --- especially if the prover for the base logic is
1.870 +good --- but can be slow.  In these examples, proofs using the default
1.871 +claset (which includes the derived rules) run about six times faster
1.872 +than proofs using \texttt{FOL_cs}.
1.873 +
1.874 +Expanding definitions also complicates error diagnosis.  Suppose we are having
1.875 +difficulties in proving some goal.  If by expanding definitions we have
1.876 +made it unreadable, then we have little hope of diagnosing the problem.
1.877 +
1.878 +Attempts at program verification often yield invalid assertions.
1.879 +Let us try to prove one:
1.880 +\begin{ttbox}
1.881 +Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
1.882 +{\out Level 0}
1.883 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.884 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.885 +by (Blast_tac 1);
1.886 +{\out by: tactic failed}
1.887 +\end{ttbox}
1.888 +This failure message is uninformative, but we can get a closer look at the
1.889 +situation by applying \ttindex{Step_tac}.
1.890 +\begin{ttbox}
1.891 +by (REPEAT (Step_tac 1));
1.892 +{\out Level 1}
1.893 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.894 +{\out  1. [| A; ~ P; R; ~ P; R |] ==> B}
1.895 +{\out  2. [| B; ~ P; ~ R; ~ P; ~ R |] ==> A}
1.896 +{\out  3. [| ~ P; R; B; ~ P; R |] ==> A}
1.897 +{\out  4. [| ~ P; ~ R; A; ~ B; ~ P |] ==> R}
1.898 +\end{ttbox}
1.899 +Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false
1.900 +while~$R$ and~$A$ are true.  This truth assignment reduces the main goal to
1.901 +$true\bimp false$, which is of course invalid.
1.902 +
1.903 +We can repeat this analysis by expanding definitions, using just
1.904 +the rules of {\FOL}:
1.905 +\begin{ttbox}
1.906 +choplev 0;
1.907 +{\out Level 0}
1.908 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.909 +{\out  1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.910 +\ttbreak
1.911 +by (rewtac if_def);
1.912 +{\out Level 1}
1.913 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.914 +{\out  1. (P & Q | ~ P & R) & A | ~ (P & Q | ~ P & R) & B <->}
1.915 +{\out     P & (Q & A | ~ Q & B) | ~ P & (R & B | ~ R & A)}
1.916 +by (blast_tac FOL_cs 1);
1.917 +{\out by: tactic failed}
1.918 +\end{ttbox}
1.919 +Again we apply \ttindex{step_tac}:
1.920 +\begin{ttbox}
1.921 +by (REPEAT (step_tac FOL_cs 1));
1.922 +{\out Level 2}
1.923 +{\out if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))}
1.924 +{\out  1. [| A; ~ P; R; ~ P; R; ~ False |] ==> B}
1.925 +{\out  2. [| A; ~ P; R; R; ~ False; ~ B; ~ B |] ==> Q}
1.926 +{\out  3. [| B; ~ P; ~ R; ~ P; ~ A |] ==> R}
1.927 +{\out  4. [| B; ~ P; ~ R; ~ Q; ~ A |] ==> R}
1.928 +{\out  5. [| B; ~ R; ~ P; ~ A; ~ R; Q; ~ False |] ==> A}
1.929 +{\out  6. [| ~ P; R; B; ~ P; R; ~ False |] ==> A}
1.930 +{\out  7. [| ~ P; ~ R; A; ~ B; ~ R |] ==> P}
1.931 +{\out  8. [| ~ P; ~ R; A; ~ B; ~ R |] ==> Q}
1.932 +\end{ttbox}
1.933 +Subgoal~1 yields the same countermodel as before.  But each proof step has
1.934 +taken six times as long, and the final result contains twice as many subgoals.
1.935 +
1.936 +Expanding definitions causes a great increase in complexity.  This is why
1.937 +the classical prover has been designed to accept derived rules.
1.938 +
1.939 +\index{first-order logic|)}