1%!TEX root = logics-ZF.tex 2\chapter{First-Order Logic} 3\index{first-order logic|(} 4 5Isabelle implements Gentzen's natural deduction systems {\sc nj} and {\sc 6 nk}. Intuitionistic first-order logic is defined first, as theory 7\thydx{IFOL}. Classical logic, theory \thydx{FOL}, is 8obtained by adding the double negation rule. Basic proof procedures are 9provided. The intuitionistic prover works with derived rules to simplify 10implications in the assumptions. Classical~\texttt{FOL} employs Isabelle's 11classical reasoner, which simulates a sequent calculus. 12 13\section{Syntax and rules of inference} 14The logic is many-sorted, using Isabelle's type classes. The class of 15first-order terms is called \cldx{term} and is a subclass of \isa{logic}. 16No types of individuals are provided, but extensions can define types such 17as \isa{nat::term} and type constructors such as \isa{list::(term)term} 18(see the examples directory, \texttt{FOL/ex}). Below, the type variable 19$\alpha$ ranges over class \isa{term}; the equality symbol and quantifiers 20are polymorphic (many-sorted). The type of formulae is~\tydx{o}, which 21belongs to class~\cldx{logic}. Figure~\ref{fol-syntax} gives the syntax. 22Note that $a$\verb|~=|$b$ is translated to $\neg(a=b)$. 23 24Figure~\ref{fol-rules} shows the inference rules with their names. 25Negation is defined in the usual way for intuitionistic logic; $\neg P$ 26abbreviates $P\imp\bot$. The biconditional~($\bimp$) is defined through 27$\conj$ and~$\imp$; introduction and elimination rules are derived for it. 28 29The unique existence quantifier, $\exists!x.P(x)$, is defined in terms 30of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested 31quantifications. For instance, $\exists!x\;y.P(x,y)$ abbreviates 32$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there 33exists a unique pair $(x,y)$ satisfying~$P(x,y)$. 34 35Some intuitionistic derived rules are shown in 36Fig.\ts\ref{fol-int-derived}, again with their names. These include 37rules for the defined symbols $\neg$, $\bimp$ and $\exists!$. Natural 38deduction typically involves a combination of forward and backward 39reasoning, particularly with the destruction rules $(\conj E)$, 40$({\imp}E)$, and~$(\forall E)$. Isabelle's backward style handles these 41rules badly, so sequent-style rules are derived to eliminate conjunctions, 42implications, and universal quantifiers. Used with elim-resolution, 43\tdx{allE} eliminates a universal quantifier while \tdx{all_dupE} 44re-inserts the quantified formula for later use. The rules 45\isa{conj\_impE}, etc., support the intuitionistic proof procedure 46(see~\S\ref{fol-int-prover}). 47 48See the on-line theory library for complete listings of the rules and 49derived rules. 50 51\begin{figure} 52\begin{center} 53\begin{tabular}{rrr} 54 \it name &\it meta-type & \it description \\ 55 \cdx{Trueprop}& $o\To prop$ & coercion to $prop$\\ 56 \cdx{Not} & $o\To o$ & negation ($\neg$) \\ 57 \cdx{True} & $o$ & tautology ($\top$) \\ 58 \cdx{False} & $o$ & absurdity ($\bot$) 59\end{tabular} 60\end{center} 61\subcaption{Constants} 62 63\begin{center} 64\begin{tabular}{llrrr} 65 \it symbol &\it name &\it meta-type & \it priority & \it description \\ 66 \sdx{ALL} & \cdx{All} & $(\alpha\To o)\To o$ & 10 & 67 universal quantifier ($\forall$) \\ 68 \sdx{EX} & \cdx{Ex} & $(\alpha\To o)\To o$ & 10 & 69 existential quantifier ($\exists$) \\ 70 \isa{EX!} & \cdx{Ex1} & $(\alpha\To o)\To o$ & 10 & 71 unique existence ($\exists!$) 72\end{tabular} 73\index{*"E"X"! symbol} 74\end{center} 75\subcaption{Binders} 76 77\begin{center} 78\index{*"= symbol} 79\index{&@{\tt\&} symbol} 80\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working 81\index{*"-"-"> symbol} 82\index{*"<"-"> symbol} 83\begin{tabular}{rrrr} 84 \it symbol & \it meta-type & \it priority & \it description \\ 85 \tt = & $[\alpha,\alpha]\To o$ & Left 50 & equality ($=$) \\ 86 \tt \& & $[o,o]\To o$ & Right 35 & conjunction ($\conj$) \\ 87 \tt | & $[o,o]\To o$ & Right 30 & disjunction ($\disj$) \\ 88 \tt --> & $[o,o]\To o$ & Right 25 & implication ($\imp$) \\ 89 \tt <-> & $[o,o]\To o$ & Right 25 & biconditional ($\bimp$) 90\end{tabular} 91\end{center} 92\subcaption{Infixes} 93 94\dquotes 95\[\begin{array}{rcl} 96 formula & = & \hbox{expression of type~$o$} \\ 97 & | & term " = " term \quad| \quad term " \ttilde= " term \\ 98 & | & "\ttilde\ " formula \\ 99 & | & formula " \& " formula \\ 100 & | & formula " | " formula \\ 101 & | & formula " --> " formula \\ 102 & | & formula " <-> " formula \\ 103 & | & "ALL~" id~id^* " . " formula \\ 104 & | & "EX~~" id~id^* " . " formula \\ 105 & | & "EX!~" id~id^* " . " formula 106 \end{array} 107\] 108\subcaption{Grammar} 109\caption{Syntax of \texttt{FOL}} \label{fol-syntax} 110\end{figure} 111 112 113\begin{figure} 114\begin{ttbox} 115\tdx{refl} a=a 116\tdx{subst} [| a=b; P(a) |] ==> P(b) 117\subcaption{Equality rules} 118 119\tdx{conjI} [| P; Q |] ==> P&Q 120\tdx{conjunct1} P&Q ==> P 121\tdx{conjunct2} P&Q ==> Q 122 123\tdx{disjI1} P ==> P|Q 124\tdx{disjI2} Q ==> P|Q 125\tdx{disjE} [| P|Q; P ==> R; Q ==> R |] ==> R 126 127\tdx{impI} (P ==> Q) ==> P-->Q 128\tdx{mp} [| P-->Q; P |] ==> Q 129 130\tdx{FalseE} False ==> P 131\subcaption{Propositional rules} 132 133\tdx{allI} (!!x. P(x)) ==> (ALL x.P(x)) 134\tdx{spec} (ALL x.P(x)) ==> P(x) 135 136\tdx{exI} P(x) ==> (EX x.P(x)) 137\tdx{exE} [| EX x.P(x); !!x. P(x) ==> R |] ==> R 138\subcaption{Quantifier rules} 139 140\tdx{True_def} True == False-->False 141\tdx{not_def} ~P == P-->False 142\tdx{iff_def} P<->Q == (P-->Q) & (Q-->P) 143\tdx{ex1_def} EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x) 144\subcaption{Definitions} 145\end{ttbox} 146 147\caption{Rules of intuitionistic logic} \label{fol-rules} 148\end{figure} 149 150 151\begin{figure} 152\begin{ttbox} 153\tdx{sym} a=b ==> b=a 154\tdx{trans} [| a=b; b=c |] ==> a=c 155\tdx{ssubst} [| b=a; P(a) |] ==> P(b) 156\subcaption{Derived equality rules} 157 158\tdx{TrueI} True 159 160\tdx{notI} (P ==> False) ==> ~P 161\tdx{notE} [| ~P; P |] ==> R 162 163\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P<->Q 164\tdx{iffE} [| P <-> Q; [| P-->Q; Q-->P |] ==> R |] ==> R 165\tdx{iffD1} [| P <-> Q; P |] ==> Q 166\tdx{iffD2} [| P <-> Q; Q |] ==> P 167 168\tdx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> EX! x. P(x) 169\tdx{ex1E} [| EX! x.P(x); !!x.[| P(x); ALL y. P(y) --> y=x |] ==> R 170 |] ==> R 171\subcaption{Derived rules for \(\top\), \(\neg\), \(\bimp\) and \(\exists!\)} 172 173\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R 174\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R 175\tdx{allE} [| ALL x.P(x); P(x) ==> R |] ==> R 176\tdx{all_dupE} [| ALL x.P(x); [| P(x); ALL x.P(x) |] ==> R |] ==> R 177\subcaption{Sequent-style elimination rules} 178 179\tdx{conj_impE} [| (P&Q)-->S; P-->(Q-->S) ==> R |] ==> R 180\tdx{disj_impE} [| (P|Q)-->S; [| P-->S; Q-->S |] ==> R |] ==> R 181\tdx{imp_impE} [| (P-->Q)-->S; [| P; Q-->S |] ==> Q; S ==> R |] ==> R 182\tdx{not_impE} [| ~P --> S; P ==> False; S ==> R |] ==> R 183\tdx{iff_impE} [| (P<->Q)-->S; [| P; Q-->S |] ==> Q; [| Q; P-->S |] ==> P; 184 S ==> R |] ==> R 185\tdx{all_impE} [| (ALL x.P(x))-->S; !!x.P(x); S ==> R |] ==> R 186\tdx{ex_impE} [| (EX x.P(x))-->S; P(a)-->S ==> R |] ==> R 187\end{ttbox} 188\subcaption{Intuitionistic simplification of implication} 189\caption{Derived rules for intuitionistic logic} \label{fol-int-derived} 190\end{figure} 191 192 193\section{Generic packages} 194FOL instantiates most of Isabelle's generic packages. 195\begin{itemize} 196\item 197It instantiates the simplifier, which is invoked through the method 198\isa{simp}. Both equality ($=$) and the biconditional 199($\bimp$) may be used for rewriting. 200 201\item 202It instantiates the classical reasoner, which is invoked mainly through the 203methods \isa{blast} and \isa{auto}. See~\S\ref{fol-cla-prover} 204for details. 205% 206%\item FOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for 207% an equality throughout a subgoal and its hypotheses. This tactic uses FOL's 208% general substitution rule. 209\end{itemize} 210 211\begin{warn}\index{simplification!of conjunctions}% 212 Simplifying $a=b\conj P(a)$ to $a=b\conj P(b)$ is often advantageous. The 213 left part of a conjunction helps in simplifying the right part. This effect 214 is not available by default: it can be slow. It can be obtained by 215 including the theorem \isa{conj_cong}\index{*conj_cong (rule)}% 216 as a congruence rule in 217 simplification, \isa{simp cong:\ conj\_cong}. 218\end{warn} 219 220 221\section{Intuitionistic proof procedures} \label{fol-int-prover} 222Implication elimination (the rules~\isa{mp} and~\isa{impE}) pose 223difficulties for automated proof. In intuitionistic logic, the assumption 224$P\imp Q$ cannot be treated like $\neg P\disj Q$. Given $P\imp Q$, we may 225use~$Q$ provided we can prove~$P$; the proof of~$P$ may require repeated 226use of $P\imp Q$. If the proof of~$P$ fails then the whole branch of the 227proof must be abandoned. Thus intuitionistic propositional logic requires 228backtracking. 229 230For an elementary example, consider the intuitionistic proof of $Q$ from 231$P\imp Q$ and $(P\imp Q)\imp P$. The implication $P\imp Q$ is needed 232twice: 233\[ \infer[({\imp}E)]{Q}{P\imp Q & 234 \infer[({\imp}E)]{P}{(P\imp Q)\imp P & P\imp Q}} 235\] 236The theorem prover for intuitionistic logic does not use~\isa{impE}.\@ 237Instead, it simplifies implications using derived rules 238(Fig.\ts\ref{fol-int-derived}). It reduces the antecedents of implications 239to atoms and then uses Modus Ponens: from $P\imp Q$ and~$P$ deduce~$Q$. 240The rules \tdx{conj_impE} and \tdx{disj_impE} are 241straightforward: $(P\conj Q)\imp S$ is equivalent to $P\imp (Q\imp S)$, and 242$(P\disj Q)\imp S$ is equivalent to the conjunction of $P\imp S$ and $Q\imp 243S$. The other \ldots\isa{\_impE} rules are unsafe; the method requires 244backtracking. All the rules are derived in the same simple manner. 245 246Dyckhoff has independently discovered similar rules, and (more importantly) 247has demonstrated their completeness for propositional 248logic~\cite{dyckhoff}. However, the tactics given below are not complete 249for first-order logic because they discard universally quantified 250assumptions after a single use. These are \ML{} functions, and are listed 251below with their \ML{} type: 252\begin{ttbox} 253mp_tac : int -> tactic 254eq_mp_tac : int -> tactic 255IntPr.safe_step_tac : int -> tactic 256IntPr.safe_tac : tactic 257IntPr.inst_step_tac : int -> tactic 258IntPr.step_tac : int -> tactic 259IntPr.fast_tac : int -> tactic 260IntPr.best_tac : int -> tactic 261\end{ttbox} 262Most of these belong to the structure \ML{} structure \texttt{IntPr} and resemble the 263tactics of Isabelle's classical reasoner. There are no corresponding 264Isar methods, but you can use the 265\isa{tactic} method to call \ML{} tactics in an Isar script: 266\begin{isabelle} 267\isacommand{apply}\ (tactic\ {* IntPr.fast\_tac 1*}) 268\end{isabelle} 269Here is a description of each tactic: 270 271\begin{ttdescription} 272\item[\ttindexbold{mp_tac} {\it i}] 273attempts to use \tdx{notE} or \tdx{impE} within the assumptions in 274subgoal $i$. For each assumption of the form $\neg P$ or $P\imp Q$, it 275searches for another assumption unifiable with~$P$. By 276contradiction with $\neg P$ it can solve the subgoal completely; by Modus 277Ponens it can replace the assumption $P\imp Q$ by $Q$. The tactic can 278produce multiple outcomes, enumerating all suitable pairs of assumptions. 279 280\item[\ttindexbold{eq_mp_tac} {\it i}] 281is like \texttt{mp_tac} {\it i}, but may not instantiate unknowns --- thus, it 282is safe. 283 284\item[\ttindexbold{IntPr.safe_step_tac} $i$] performs a safe step on 285subgoal~$i$. This may include proof by assumption or Modus Ponens (taking 286care not to instantiate unknowns), or \texttt{hyp_subst_tac}. 287 288\item[\ttindexbold{IntPr.safe_tac}] repeatedly performs safe steps on all 289subgoals. It is deterministic, with at most one outcome. 290 291\item[\ttindexbold{IntPr.inst_step_tac} $i$] is like \texttt{safe_step_tac}, 292but allows unknowns to be instantiated. 293 294\item[\ttindexbold{IntPr.step_tac} $i$] tries \texttt{safe_tac} or {\tt 295 inst_step_tac}, or applies an unsafe rule. This is the basic step of 296 the intuitionistic proof procedure. 297 298\item[\ttindexbold{IntPr.fast_tac} $i$] applies \texttt{step_tac}, using 299depth-first search, to solve subgoal~$i$. 300 301\item[\ttindexbold{IntPr.best_tac} $i$] applies \texttt{step_tac}, using 302best-first search (guided by the size of the proof state) to solve subgoal~$i$. 303\end{ttdescription} 304Here are some of the theorems that \texttt{IntPr.fast_tac} proves 305automatically. The latter three date from {\it Principia Mathematica} 306(*11.53, *11.55, *11.61)~\cite{principia}. 307\begin{ttbox} 308~~P & ~~(P --> Q) --> ~~Q 309(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y))) 310(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y))) 311(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y))) 312\end{ttbox} 313 314 315 316\begin{figure} 317\begin{ttbox} 318\tdx{excluded_middle} ~P | P 319 320\tdx{disjCI} (~Q ==> P) ==> P|Q 321\tdx{exCI} (ALL x. ~P(x) ==> P(a)) ==> EX x.P(x) 322\tdx{impCE} [| P-->Q; ~P ==> R; Q ==> R |] ==> R 323\tdx{iffCE} [| P<->Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R 324\tdx{notnotD} ~~P ==> P 325\tdx{swap} ~P ==> (~Q ==> P) ==> Q 326\end{ttbox} 327\caption{Derived rules for classical logic} \label{fol-cla-derived} 328\end{figure} 329 330 331\section{Classical proof procedures} \label{fol-cla-prover} 332The classical theory, \thydx{FOL}, consists of intuitionistic logic plus 333the rule 334$$ \vcenter{\infer{P}{\infer*{P}{[\neg P]}}} \eqno(classical) $$ 335\noindent 336Natural deduction in classical logic is not really all that natural. FOL 337derives classical introduction rules for $\disj$ and~$\exists$, as well as 338classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule (see 339Fig.\ts\ref{fol-cla-derived}). 340 341The classical reasoner is installed. The most useful methods are 342\isa{blast} (pure classical reasoning) and \isa{auto} (classical reasoning 343combined with simplification), but the full range of 344methods is available, including \isa{clarify}, 345\isa{fast}, \isa{best} and \isa{force}. 346 See the 347\iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 348 {Chap.\ts\ref{chap:classical}} 349and the \emph{Tutorial}~\cite{isa-tutorial} 350for more discussion of classical proof methods. 351 352 353\section{An intuitionistic example} 354Here is a session similar to one in the book {\em Logic and Computation} 355\cite[pages~222--3]{paulson87}. It illustrates the treatment of 356quantifier reasoning, which is different in Isabelle than it is in 357{\sc lcf}-based theorem provers such as {\sc hol}. 358 359The theory header specifies that we are working in intuitionistic 360logic by designating \isa{IFOL} rather than \isa{FOL} as the parent 361theory: 362\begin{isabelle} 363\isacommand{theory}\ IFOL\_examples\ \isacommand{imports}\ IFOL\isanewline 364\isacommand{begin} 365\end{isabelle} 366The proof begins by entering the goal, then applying the rule $({\imp}I)$. 367\begin{isabelle} 368\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline 369\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\ 370\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y)) 371\isanewline 372\isacommand{apply}\ (rule\ impI)\isanewline 373\ 1.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ 374\isasymLongrightarrow \ \isasymforall x.\ \isasymexists y.\ Q(x,\ y) 375\end{isabelle} 376Isabelle's output is shown as it would appear using Proof General. 377In this example, we shall never have more than one subgoal. Applying 378$({\imp}I)$ replaces~\isa{\isasymlongrightarrow} 379by~\isa{\isasymLongrightarrow}, so that 380\(\ex{y}\all{x}Q(x,y)\) becomes an assumption. We have the choice of 381$({\exists}E)$ and $({\forall}I)$; let us try the latter. 382\begin{isabelle} 383\isacommand{apply}\ (rule\ allI)\isanewline 384\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ 385\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y)\hfill\((*)\) 386\end{isabelle} 387Applying $({\forall}I)$ replaces the \isa{\isasymforall 388x} (in ASCII, \isa{ALL~x}) by \isa{\isasymAnd x} 389(or \isa{!!x}), replacing FOL's universal quantifier by Isabelle's 390meta universal quantifier. The bound variable is a {\bf parameter} of 391the subgoal. We now must choose between $({\exists}I)$ and 392$({\exists}E)$. What happens if the wrong rule is chosen? 393\begin{isabelle} 394\isacommand{apply}\ (rule\ exI)\isanewline 395\ 1.\ \isasymAnd x.\ \isasymexists y.\ \isasymforall x.\ Q(x,\ y)\ 396\isasymLongrightarrow \ Q(x,\ ?y2(x)) 397\end{isabelle} 398The new subgoal~1 contains the function variable \isa{?y2}. Instantiating 399\isa{?y2} can replace~\isa{?y2(x)} by a term containing~\isa{x}, even 400though~\isa{x} is a bound variable. Now we analyse the assumption 401\(\exists y.\forall x. Q(x,y)\) using elimination rules: 402\begin{isabelle} 403\isacommand{apply}\ (erule\ exE)\isanewline 404\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ \isasymLongrightarrow \ Q(x,\ ?y2(x)) 405\end{isabelle} 406Applying $(\exists E)$ has produced the parameter \isa{y} and stripped the 407existential quantifier from the assumption. But the subgoal is unprovable: 408there is no way to unify \isa{?y2(x)} with the bound variable~\isa{y}. 409Using Proof General, we can return to the critical point, marked 410$(*)$ above. This time we apply $({\exists}E)$: 411\begin{isabelle} 412\isacommand{apply}\ (erule\ exE)\isanewline 413\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ 414\isasymLongrightarrow \ \isasymexists y.\ Q(x,\ y) 415\end{isabelle} 416We now have two parameters and no scheme variables. Applying 417$({\exists}I)$ and $({\forall}E)$ produces two scheme variables, which are 418applied to those parameters. Parameters should be produced early, as this 419example demonstrates. 420\begin{isabelle} 421\isacommand{apply}\ (rule\ exI)\isanewline 422\ 1.\ \isasymAnd x\ y.\ \isasymforall x.\ Q(x,\ y)\ 423\isasymLongrightarrow \ Q(x,\ ?y3(x,\ y)) 424\isanewline 425\isacommand{apply}\ (erule\ allE)\isanewline 426\ 1.\ \isasymAnd x\ y.\ Q(?x4(x,\ y),\ y)\ \isasymLongrightarrow \ 427Q(x,\ ?y3(x,\ y)) 428\end{isabelle} 429The subgoal has variables \isa{?y3} and \isa{?x4} applied to both 430parameters. The obvious projection functions unify \isa{?x4(x,y)} with~\isa{ 431x} and \isa{?y3(x,y)} with~\isa{y}. 432\begin{isabelle} 433\isacommand{apply}\ assumption\isanewline 434No\ subgoals!\isanewline 435\isacommand{done} 436\end{isabelle} 437The theorem was proved in six method invocations, not counting the 438abandoned ones. But proof checking is tedious, and the \ML{} tactic 439\ttindex{IntPr.fast_tac} can prove the theorem in one step. 440\begin{isabelle} 441\isacommand{lemma}\ "(EX\ y.\ ALL\ x.\ Q(x,y))\ -->\ \ (ALL\ x.\ EX\ y.\ Q(x,y))"\isanewline 442\ 1.\ (\isasymexists y.\ \isasymforall x.\ Q(x,\ y))\ 443\isasymlongrightarrow \ (\isasymforall x.\ \isasymexists y.\ Q(x,\ y)) 444\isanewline 445\isacommand{by} (tactic \ttlbrace*IntPr.fast_tac 1*\ttrbrace)\isanewline 446No\ subgoals! 447\end{isabelle} 448 449 450\section{An example of intuitionistic negation} 451The following example demonstrates the specialized forms of implication 452elimination. Even propositional formulae can be difficult to prove from 453the basic rules; the specialized rules help considerably. 454 455Propositional examples are easy to invent. As Dummett notes~\cite[page 45628]{dummett}, $\neg P$ is classically provable if and only if it is 457intuitionistically provable; therefore, $P$ is classically provable if and 458only if $\neg\neg P$ is intuitionistically provable.% 459\footnote{This remark holds only for propositional logic, not if $P$ is 460 allowed to contain quantifiers.} 461% 462Proving $\neg\neg P$ intuitionistically is 463much harder than proving~$P$ classically. 464 465Our example is the double negation of the classical tautology $(P\imp 466Q)\disj (Q\imp P)$. The first step is apply the 467\isa{unfold} method, which expands 468negations to implications using the definition $\neg P\equiv P\imp\bot$ 469and allows use of the special implication rules. 470\begin{isabelle} 471\isacommand{lemma}\ "\isachartilde \ \isachartilde \ ((P-->Q)\ |\ (Q-->P))"\isanewline 472\ 1.\ \isasymnot \ \isasymnot \ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)) 473\isanewline 474\isacommand{apply}\ (unfold\ not\_def)\isanewline 475\ 1.\ ((P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False)\ \isasymlongrightarrow \ False% 476\end{isabelle} 477The next step is a trivial use of $(\imp I)$. 478\begin{isabelle} 479\isacommand{apply}\ (rule\ impI)\isanewline 480\ 1.\ (P\ \isasymlongrightarrow \ Q)\ \isasymor \ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\ \isasymLongrightarrow \ False% 481\end{isabelle} 482By $(\imp E)$ it would suffice to prove $(P\imp Q)\disj (Q\imp P)$, but 483that formula is not a theorem of intuitionistic logic. Instead, we 484apply the specialized implication rule \tdx{disj_impE}. It splits the 485assumption into two assumptions, one for each disjunct. 486\begin{isabelle} 487\isacommand{apply}\ (erule\ disj\_impE)\isanewline 488\ 1.\ \isasymlbrakk (P\ \isasymlongrightarrow \ Q)\ \isasymlongrightarrow \ False;\ (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ 489False 490\end{isabelle} 491We cannot hope to prove $P\imp Q$ or $Q\imp P$ separately, but 492their negations are inconsistent. Applying \tdx{imp_impE} breaks down 493the assumption $\neg(P\imp Q)$, asking to show~$Q$ while providing new 494assumptions~$P$ and~$\neg Q$. 495\begin{isabelle} 496\isacommand{apply}\ (erule\ imp\_impE)\isanewline 497\ 1.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ P;\ Q\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 498\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ 499False 500\end{isabelle} 501Subgoal~2 holds trivially; let us ignore it and continue working on 502subgoal~1. Thanks to the assumption~$P$, we could prove $Q\imp P$; 503applying \tdx{imp_impE} is simpler. 504\begin{isabelle} 505\ \isacommand{apply}\ (erule\ imp\_impE)\isanewline 506\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ Q;\ P\ \isasymlongrightarrow \ False\isasymrbrakk \ \isasymLongrightarrow \ P\isanewline 507\ 2.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 508\ 3.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ \isasymlongrightarrow \ False;\ False\isasymrbrakk \ \isasymLongrightarrow \ False% 509\end{isabelle} 510The three subgoals are all trivial. 511\begin{isabelle} 512\isacommand{apply}\ assumption\ \isanewline 513\ 1.\ \isasymlbrakk P;\ Q\ \isasymlongrightarrow \ False;\ 514False\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 515\ 2.\ \isasymlbrakk (Q\ \isasymlongrightarrow \ P)\ 516\isasymlongrightarrow \ False;\ False\isasymrbrakk \ 517\isasymLongrightarrow \ False% 518\isanewline 519\isacommand{apply}\ (erule\ FalseE)+\isanewline 520No\ subgoals!\isanewline 521\isacommand{done} 522\end{isabelle} 523This proof is also trivial for the \ML{} tactic \isa{IntPr.fast_tac}. 524 525 526\section{A classical example} \label{fol-cla-example} 527To illustrate classical logic, we shall prove the theorem 528$\ex{y}\all{x}P(y)\imp P(x)$. Informally, the theorem can be proved as 529follows. Choose~$y$ such that~$\neg P(y)$, if such exists; otherwise 530$\all{x}P(x)$ is true. Either way the theorem holds. First, we must 531work in a theory based on classical logic, the theory \isa{FOL}: 532\begin{isabelle} 533\isacommand{theory}\ FOL\_examples\ \isacommand{imports}\ FOL\isanewline 534\isacommand{begin} 535\end{isabelle} 536 537The formal proof does not conform in any obvious way to the sketch given 538above. Its key step is its first rule, \tdx{exCI}, a classical 539version of~$(\exists I)$ that allows multiple instantiation of the 540quantifier. 541\begin{isabelle} 542\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline 543\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x) 544\isanewline 545\isacommand{apply}\ (rule\ exCI)\isanewline 546\ 1.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ \isasymforall x.\ P(?a)\ \isasymlongrightarrow \ P(x) 547\end{isabelle} 548We can either exhibit a term \isa{?a} to satisfy the conclusion of 549subgoal~1, or produce a contradiction from the assumption. The next 550steps are routine. 551\begin{isabelle} 552\isacommand{apply}\ (rule\ allI)\isanewline 553\ 1.\ \isasymAnd x.\ \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x))\ \isasymLongrightarrow \ P(?a)\ \isasymlongrightarrow \ P(x) 554\isanewline 555\isacommand{apply}\ (rule\ impI)\isanewline 556\ 1.\ \isasymAnd x.\ \isasymlbrakk \isasymforall y.\ \isasymnot \ (\isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x));\ P(?a)\isasymrbrakk \ \isasymLongrightarrow \ P(x) 557\end{isabelle} 558By the duality between $\exists$ and~$\forall$, applying~$(\forall E)$ 559is equivalent to applying~$(\exists I)$ again. 560\begin{isabelle} 561\isacommand{apply}\ (erule\ allE)\isanewline 562\ 1.\ \isasymAnd x.\ \isasymlbrakk P(?a);\ \isasymnot \ (\isasymforall xa.\ P(?y3(x))\ \isasymlongrightarrow \ P(xa))\isasymrbrakk \ \isasymLongrightarrow \ P(x) 563\end{isabelle} 564In classical logic, a negated assumption is equivalent to a conclusion. To 565get this effect, we create a swapped version of $(\forall I)$ and apply it 566using \ttindex{erule}. 567\begin{isabelle} 568\isacommand{apply}\ (erule\ allI\ [THEN\ [2]\ swap])\isanewline 569\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x)\isasymrbrakk \ \isasymLongrightarrow \ P(?y3(x))\ \isasymlongrightarrow \ P(xa) 570\end{isabelle} 571The operand of \isa{erule} above denotes the following theorem: 572\begin{isabelle} 573\ \ \ \ \isasymlbrakk \isasymnot \ (\isasymforall x.\ ?P1(x));\ 574\isasymAnd x.\ \isasymnot \ ?P\ \isasymLongrightarrow \ 575?P1(x)\isasymrbrakk \ 576\isasymLongrightarrow \ ?P% 577\end{isabelle} 578The previous conclusion, \isa{P(x)}, has become a negated assumption. 579\begin{isabelle} 580\isacommand{apply}\ (rule\ impI)\isanewline 581\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ \isasymnot \ P(x);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(xa) 582\end{isabelle} 583The subgoal has three assumptions. We produce a contradiction between the 584\index{assumptions!contradictory} assumptions~\isa{\isasymnot P(x)} 585and~\isa{P(?y3(x))}. The proof never instantiates the 586unknown~\isa{?a}. 587\begin{isabelle} 588\isacommand{apply}\ (erule\ notE)\isanewline 589\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P(?a);\ P(?y3(x))\isasymrbrakk \ \isasymLongrightarrow \ P(x) 590\isanewline 591\isacommand{apply}\ assumption\isanewline 592No\ subgoals!\isanewline 593\isacommand{done} 594\end{isabelle} 595The civilised way to prove this theorem is using the 596\methdx{blast} method, which automatically uses the classical form 597of the rule~$(\exists I)$: 598\begin{isabelle} 599\isacommand{lemma}\ "EX\ y.\ ALL\ x.\ P(y)-->P(x)"\isanewline 600\ 1.\ \isasymexists y.\ \isasymforall x.\ P(y)\ \isasymlongrightarrow \ P(x) 601\isanewline 602\isacommand{by}\ blast\isanewline 603No\ subgoals! 604\end{isabelle} 605If this theorem seems counterintuitive, then perhaps you are an 606intuitionist. In constructive logic, proving $\ex{y}\all{x}P(y)\imp P(x)$ 607requires exhibiting a particular term~$t$ such that $\all{x}P(t)\imp P(x)$, 608which we cannot do without further knowledge about~$P$. 609 610 611\section{Derived rules and the classical tactics} 612Classical first-order logic can be extended with the propositional 613connective $if(P,Q,R)$, where 614$$ if(P,Q,R) \equiv P\conj Q \disj \neg P \conj R. \eqno(if) $$ 615Theorems about $if$ can be proved by treating this as an abbreviation, 616replacing $if(P,Q,R)$ by $P\conj Q \disj \neg P \conj R$ in subgoals. But 617this duplicates~$P$, causing an exponential blowup and an unreadable 618formula. Introducing further abbreviations makes the problem worse. 619 620Natural deduction demands rules that introduce and eliminate $if(P,Q,R)$ 621directly, without reference to its definition. The simple identity 622\[ if(P,Q,R) \,\bimp\, (P\imp Q)\conj (\neg P\imp R) \] 623suggests that the 624$if$-introduction rule should be 625\[ \infer[({if}\,I)]{if(P,Q,R)}{\infer*{Q}{[P]} & \infer*{R}{[\neg P]}} \] 626The $if$-elimination rule reflects the definition of $if(P,Q,R)$ and the 627elimination rules for~$\disj$ and~$\conj$. 628\[ \infer[({if}\,E)]{S}{if(P,Q,R) & \infer*{S}{[P,Q]} 629 & \infer*{S}{[\neg P,R]}} 630\] 631Having made these plans, we get down to work with Isabelle. The theory of 632classical logic, \texttt{FOL}, is extended with the constant 633$if::[o,o,o]\To o$. The axiom \tdx{if_def} asserts the 634equation~$(if)$. 635\begin{isabelle} 636\isacommand{theory}\ If\ \isacommand{imports}\ FOL\isanewline 637\isacommand{begin}\isanewline 638\isacommand{constdefs}\isanewline 639\ \ if\ ::\ "[o,o,o]=>o"\isanewline 640\ \ \ "if(P,Q,R)\ ==\ P\&Q\ |\ \isachartilde P\&R" 641\end{isabelle} 642We create the file \texttt{If.thy} containing these declarations. (This file 643is on directory \texttt{FOL/ex} in the Isabelle distribution.) Typing 644\begin{isabelle} 645use_thy "If"; 646\end{isabelle} 647loads that theory and sets it to be the current context. 648 649 650\subsection{Deriving the introduction rule} 651 652The derivations of the introduction and elimination rules demonstrate the 653methods for rewriting with definitions. Classical reasoning is required, 654so we use \isa{blast}. 655 656The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, 657concludes $if(P,Q,R)$. We propose this lemma and immediately simplify 658using \isa{if\_def} to expand the definition of \isa{if} in the 659subgoal. 660\begin{isabelle} 661\isacommand{lemma}\ ifI: "[|\ P\ ==>\ Q;\ \isachartilde P\ ==>\ R\ 662|]\ ==>\ if(P,Q,R)"\isanewline 663\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ Q,\ R) 664\isanewline 665\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 666\ 1.\ \isasymlbrakk P\ \isasymLongrightarrow \ Q;\ \isasymnot \ P\ \isasymLongrightarrow \ R\isasymrbrakk \ \isasymLongrightarrow \ P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ 667R 668\end{isabelle} 669The rule's premises, although expressed using meta-level implication 670(\isa{\isasymLongrightarrow}) are passed as ordinary implications to 671\methdx{blast}. 672\begin{isabelle} 673\isacommand{apply}\ blast\isanewline 674No\ subgoals!\isanewline 675\isacommand{done} 676\end{isabelle} 677 678 679\subsection{Deriving the elimination rule} 680The elimination rule has three premises, two of which are themselves rules. 681The conclusion is simply $S$. 682\begin{isabelle} 683\isacommand{lemma}\ ifE:\isanewline 684\ \ \ "[|\ if(P,Q,R);\ \ [|P;\ Q|]\ ==>\ S;\ [|\isachartilde P;\ R|]\ ==>\ S\ |]\ ==>\ S"\isanewline 685\ 1.\ \isasymlbrakk if(P,\ Q,\ R);\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S% 686\isanewline 687\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 688\ 1.\ \isasymlbrakk P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R;\ \isasymlbrakk P;\ Q\isasymrbrakk \ \isasymLongrightarrow \ S;\ \isasymlbrakk \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ S\isasymrbrakk \ \isasymLongrightarrow \ S% 689\end{isabelle} 690The proof script is the same as before: \isa{simp} followed by 691\isa{blast}: 692\begin{isabelle} 693\isacommand{apply}\ blast\isanewline 694No\ subgoals!\isanewline 695\isacommand{done} 696\end{isabelle} 697 698 699\subsection{Using the derived rules} 700Our new derived rules, \tdx{ifI} and~\tdx{ifE}, permit natural 701proofs of theorems such as the following: 702\begin{eqnarray*} 703 if(P, if(Q,A,B), if(Q,C,D)) & \bimp & if(Q,if(P,A,C),if(P,B,D)) \\ 704 if(if(P,Q,R), A, B) & \bimp & if(P,if(Q,A,B),if(R,A,B)) 705\end{eqnarray*} 706Proofs also require the classical reasoning rules and the $\bimp$ 707introduction rule (called~\tdx{iffI}: do not confuse with~\isa{ifI}). 708 709To display the $if$-rules in action, let us analyse a proof step by step. 710\begin{isabelle} 711\isacommand{lemma}\ if\_commute:\isanewline 712\ \ \ \ \ "if(P,\ if(Q,A,B),\ 713if(Q,C,D))\ <->\ if(Q,\ if(P,A,C),\ if(P,B,D))"\isanewline 714\isacommand{apply}\ (rule\ iffI)\isanewline 715\ 1.\ if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D))\ \isasymLongrightarrow \isanewline 716\isaindent{\ 1.\ }if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 717\ 2.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 718\isaindent{\ 2.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 719\end{isabelle} 720The $if$-elimination rule can be applied twice in succession. 721\begin{isabelle} 722\isacommand{apply}\ (erule\ ifE)\isanewline 723\ 1.\ \isasymlbrakk P;\ if(Q,\ A,\ B)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 724\ 2.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 725\ 3.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 726\isaindent{\ 3.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 727\isanewline 728\isacommand{apply}\ (erule\ ifE)\isanewline 729\ 1.\ \isasymlbrakk P;\ Q;\ A\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 730\ 2.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 731\ 3.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 732\ 4.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 733\isaindent{\ 4.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 734\end{isabelle} 735% 736In the first two subgoals, all assumptions have been reduced to atoms. Now 737$if$-introduction can be applied. Observe how the $if$-rules break down 738occurrences of $if$ when they become the outermost connective. 739\begin{isabelle} 740\isacommand{apply}\ (rule\ ifI)\isanewline 741\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ A,\ C)\isanewline 742\ 2.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline 743\ 3.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 744\ 4.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 745\ 5.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 746\isaindent{\ 5.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 747\isanewline 748\isacommand{apply}\ (rule\ ifI)\isanewline 749\ 1.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline 750\ 2.\ \isasymlbrakk P;\ Q;\ A;\ Q;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ C\isanewline 751\ 3.\ \isasymlbrakk P;\ Q;\ A;\ \isasymnot \ Q\isasymrbrakk \ \isasymLongrightarrow \ if(P,\ B,\ D)\isanewline 752\ 4.\ \isasymlbrakk P;\ \isasymnot \ Q;\ B\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 753\ 5.\ \isasymlbrakk \isasymnot \ P;\ if(Q,\ C,\ D)\isasymrbrakk \ \isasymLongrightarrow \ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\isanewline 754\ 6.\ if(Q,\ if(P,\ A,\ C),\ if(P,\ B,\ D))\ \isasymLongrightarrow \isanewline 755\isaindent{\ 6.\ }if(P,\ if(Q,\ A,\ B),\ if(Q,\ C,\ D)) 756\end{isabelle} 757Where do we stand? The first subgoal holds by assumption; the second and 758third, by contradiction. This is getting tedious. We could use the classical 759reasoner, but first let us extend the default claset with the derived rules 760for~$if$. 761\begin{isabelle} 762\isacommand{declare}\ ifI\ [intro!]\isanewline 763\isacommand{declare}\ ifE\ [elim!] 764\end{isabelle} 765With these declarations, we could have proved this theorem with a single 766call to \isa{blast}. Here is another example: 767\begin{isabelle} 768\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline 769\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B)) 770\isanewline 771\isacommand{by}\ blast 772\end{isabelle} 773 774 775\subsection{Derived rules versus definitions} 776Dispensing with the derived rules, we can treat $if$ as an 777abbreviation, and let \ttindex{blast_tac} prove the expanded formula. Let 778us redo the previous proof: 779\begin{isabelle} 780\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,A,B))"\isanewline 781\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ A,\ B)) 782\end{isabelle} 783This time, we simply unfold using the definition of $if$: 784\begin{isabelle} 785\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 786\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline 787\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ A\ \isasymor \ \isasymnot \ R\ \isasymand \ B) 788\end{isabelle} 789We are left with a subgoal in pure first-order logic, and it falls to 790\isa{blast}: 791\begin{isabelle} 792\isacommand{apply}\ blast\isanewline 793No\ subgoals! 794\end{isabelle} 795Expanding definitions reduces the extended logic to the base logic. This 796approach has its merits, but it can be slow. In these examples, proofs 797using the derived rules for~\isa{if} run about six 798times faster than proofs using just the rules of first-order logic. 799 800Expanding definitions can also make it harder to diagnose errors. 801Suppose we are having difficulties in proving some goal. If by expanding 802definitions we have made it unreadable, then we have little hope of 803diagnosing the problem. 804 805Attempts at program verification often yield invalid assertions. 806Let us try to prove one: 807\begin{isabelle} 808\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline 809\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\ 810A)) 811\end{isabelle} 812Calling \isa{blast} yields an uninformative failure message. We can 813get a closer look at the situation by applying \methdx{auto}. 814\begin{isabelle} 815\isacommand{apply}\ auto\isanewline 816\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline 817\ 2.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline 818\ 3.\ \isasymlbrakk B;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ A\isanewline 819\ 4.\ \isasymlbrakk \isasymnot \ R;\ A;\ \isasymnot \ B;\ \isasymnot \ P\isasymrbrakk \ \isasymLongrightarrow \ 820False 821\end{isabelle} 822Subgoal~1 is unprovable and yields a countermodel: $P$ and~$B$ are false 823while~$R$ and~$A$ are true. This truth assignment reduces the main goal to 824$true\bimp false$, which is of course invalid. 825 826We can repeat this analysis by expanding definitions, using just the rules of 827first-order logic: 828\begin{isabelle} 829\isacommand{lemma}\ "if(if(P,Q,R),\ A,\ B)\ <->\ if(P,\ if(Q,A,B),\ if(R,B,A))"\isanewline 830\ 1.\ if(if(P,\ Q,\ R),\ A,\ B)\ \isasymlongleftrightarrow \ if(P,\ if(Q,\ A,\ B),\ if(R,\ B,\ 831A)) 832\isanewline 833\isacommand{apply}\ (simp\ add:\ if\_def)\isanewline 834\ 1.\ (P\ \isasymand \ Q\ \isasymor \ \isasymnot \ P\ \isasymand \ R)\ \isasymand \ A\ \isasymor \ (\isasymnot \ P\ \isasymor \ \isasymnot \ Q)\ \isasymand \ (P\ \isasymor \ \isasymnot \ R)\ \isasymand \ B\ \isasymlongleftrightarrow \isanewline 835\isaindent{\ 1.\ }P\ \isasymand \ (Q\ \isasymand \ A\ \isasymor \ \isasymnot \ Q\ \isasymand \ B)\ \isasymor \ \isasymnot \ P\ \isasymand \ (R\ \isasymand \ B\ \isasymor \ \isasymnot \ R\ \isasymand \ A) 836\end{isabelle} 837Again \isa{blast} would fail, so we try \methdx{auto}: 838\begin{isabelle} 839\isacommand{apply}\ (auto)\ \isanewline 840\ 1.\ \isasymlbrakk A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ B\isanewline 841\ 2.\ \isasymlbrakk A;\ \isasymnot \ P;\ R;\ \isasymnot \ B\isasymrbrakk \ \isasymLongrightarrow \ Q\isanewline 842\ 3.\ \isasymlbrakk B;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 843\ 4.\ \isasymlbrakk B;\ \isasymnot \ P;\ \isasymnot \ A;\ \isasymnot \ R;\ Q\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 844\ 5.\ \isasymlbrakk B;\ \isasymnot \ Q;\ \isasymnot \ R;\ \isasymnot \ P;\ \isasymnot \ A\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 845\ 6.\ \isasymlbrakk B;\ \isasymnot \ A;\ \isasymnot \ P;\ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 846\ 7.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ False\isanewline 847\ 8.\ \isasymlbrakk \isasymnot \ P;\ A;\ \isasymnot \ B;\ \isasymnot \ R\isasymrbrakk \ \isasymLongrightarrow \ Q% 848\end{isabelle} 849Subgoal~1 yields the same countermodel as before. But each proof step has 850taken six times as long, and the final result contains twice as many subgoals. 851 852Expanding your definitions usually makes proofs more difficult. This is 853why the classical prover has been designed to accept derived rules. 854 855\index{first-order logic|)} 856