1%!TEX root = root.tex 2\chapter{The Rules of the Game} 3\label{chap:rules} 4 5This chapter outlines the concepts and techniques that underlie reasoning 6in Isabelle. Until now, we have proved everything using only induction and 7simplification, but any serious verification project requires more elaborate 8forms of inference. The chapter also introduces the fundamentals of 9predicate logic. The first examples in this chapter will consist of 10detailed, low-level proof steps. Later, we shall see how to automate such 11reasoning using the methods 12\isa{blast}, 13\isa{auto} and others. Backward or goal-directed proof is our usual style, 14but the chapter also introduces forward reasoning, where one theorem is 15transformed to yield another. 16 17\section{Natural Deduction} 18 19\index{natural deduction|(}% 20In Isabelle, proofs are constructed using inference rules. The 21most familiar inference rule is probably \emph{modus ponens}:% 22\index{modus ponens@\emph{modus ponens}} 23\[ \infer{Q}{P\imp Q & P} \] 24This rule says that from $P\imp Q$ and $P$ we may infer~$Q$. 25 26\textbf{Natural deduction} is an attempt to formalize logic in a way 27that mirrors human reasoning patterns. 28For each logical symbol (say, $\conj$), there 29are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules. 30The introduction rules allow us to infer this symbol (say, to 31infer conjunctions). The elimination rules allow us to deduce 32consequences from this symbol. Ideally each rule should mention 33one symbol only. For predicate logic this can be 34done, but when users define their own concepts they typically 35have to refer to other symbols as well. It is best not to be dogmatic. 36Our system is not based on pure natural deduction, but includes elements from the sequent calculus 37and free-variable tableaux. 38 39Natural deduction generally deserves its name. It is easy to use. Each 40proof step consists of identifying the outermost symbol of a formula and 41applying the corresponding rule. It creates new subgoals in 42an obvious way from parts of the chosen formula. Expanding the 43definitions of constants can blow up the goal enormously. Deriving natural 44deduction rules for such constants lets us reason in terms of their key 45properties, which might otherwise be obscured by the technicalities of its 46definition. Natural deduction rules also lend themselves to automation. 47Isabelle's 48\textbf{classical reasoner} accepts any suitable collection of natural deduction 49rules and uses them to search for proofs automatically. Isabelle is designed around 50natural deduction and many of its tools use the terminology of introduction 51and elimination rules.% 52\index{natural deduction|)} 53 54 55\section{Introduction Rules} 56 57\index{introduction rules|(}% 58An introduction rule tells us when we can infer a formula 59containing a specific logical symbol. For example, the conjunction 60introduction rule says that if we have $P$ and if we have $Q$ then 61we have $P\conj Q$. In a mathematics text, it is typically shown 62like this: 63\[ \infer{P\conj Q}{P & Q} \] 64The rule introduces the conjunction 65symbol~($\conj$) in its conclusion. In Isabelle proofs we 66mainly reason backwards. When we apply this rule, the subgoal already has 67the form of a conjunction; the proof step makes this conjunction symbol 68disappear. 69 70In Isabelle notation, the rule looks like this: 71\begin{isabelle} 72\isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulenamedx{conjI} 73\end{isabelle} 74Carefully examine the syntax. The premises appear to the 75left of the arrow and the conclusion to the right. The premises (if 76more than one) are grouped using the fat brackets. The question marks 77indicate \textbf{schematic variables} (also called 78\textbf{unknowns}):\index{unknowns|bold} they may 79be replaced by arbitrary formulas. If we use the rule backwards, Isabelle 80tries to unify the current subgoal with the conclusion of the rule, which 81has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, 82{\S}\ref{sec:unification}.) If successful, 83it yields new subgoals given by the formulas assigned to 84\isa{?P} and \isa{?Q}. 85 86The following trivial proof illustrates how rules work. It also introduces a 87style of indentation. If a command adds a new subgoal, then the next 88command's indentation is increased by one space; if it proves a subgoal, then 89the indentation is reduced. This provides the reader with hints about the 90subgoal structure. 91\begin{isabelle} 92\isacommand{lemma}\ conj_rule:\ "\isasymlbrakk P;\ 93Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ 94(Q\ \isasymand\ P)"\isanewline 95\isacommand{apply}\ (rule\ conjI)\isanewline 96\ \isacommand{apply}\ assumption\isanewline 97\isacommand{apply}\ (rule\ conjI)\isanewline 98\ \isacommand{apply}\ assumption\isanewline 99\isacommand{apply}\ assumption 100\end{isabelle} 101At the start, Isabelle presents 102us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved, 103\isa{P\ \isasymand\ 104(Q\ \isasymand\ P)}. We are working backwards, so when we 105apply conjunction introduction, the rule removes the outermost occurrence 106of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply 107the proof method \isa{rule} --- here with \isa{conjI}, the conjunction 108introduction rule. 109\begin{isabelle} 110%\isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\ 111%\isasymand\ P\isanewline 112\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline 113\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P 114\end{isabelle} 115Isabelle leaves two new subgoals: the two halves of the original conjunction. 116The first is simply \isa{P}, which is trivial, since \isa{P} is among 117the assumptions. We can apply the \methdx{assumption} 118method, which proves a subgoal by finding a matching assumption. 119\begin{isabelle} 120\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ 121Q\ \isasymand\ P 122\end{isabelle} 123We are left with the subgoal of proving 124\isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply 125\isa{rule conjI} again. 126\begin{isabelle} 127\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline 128\ 2.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P 129\end{isabelle} 130We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved 131using the \isa{assumption} method.% 132\index{introduction rules|)} 133 134 135\section{Elimination Rules} 136 137\index{elimination rules|(}% 138Elimination rules work in the opposite direction from introduction 139rules. In the case of conjunction, there are two such rules. 140From $P\conj Q$ we infer $P$. also, from $P\conj Q$ 141we infer $Q$: 142\[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \] 143 144Now consider disjunction. There are two introduction rules, which resemble inverted forms of the 145conjunction elimination rules: 146\[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \] 147 148What is the disjunction elimination rule? The situation is rather different from 149conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we 150cannot conclude that $Q$ is true; there are no direct 151elimination rules of the sort that we have seen for conjunction. Instead, 152there is an elimination rule that works indirectly. If we are trying to prove 153something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider 154two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is 155true and prove $R$ a second time. Here we see a fundamental concept used in natural 156deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under 157different assumptions. The assumptions are local to these subproofs and are visible 158nowhere else. 159 160In a logic text, the disjunction elimination rule might be shown 161like this: 162\[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \] 163The assumptions $[P]$ and $[Q]$ are bracketed 164to emphasize that they are local to their subproofs. In Isabelle 165notation, the already-familiar \isa{\isasymLongrightarrow} syntax serves the 166same purpose: 167\begin{isabelle} 168\isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{disjE} 169\end{isabelle} 170When we use this sort of elimination rule backwards, it produces 171a case split. (We have seen this before, in proofs by induction.) The following proof 172illustrates the use of disjunction elimination. 173\begin{isabelle} 174\isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ 175\isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline 176\isacommand{apply}\ (erule\ disjE)\isanewline 177\ \isacommand{apply}\ (rule\ disjI2)\isanewline 178\ \isacommand{apply}\ assumption\isanewline 179\isacommand{apply}\ (rule\ disjI1)\isanewline 180\isacommand{apply}\ assumption 181\end{isabelle} 182We assume \isa{P\ \isasymor\ Q} and 183must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction 184elimination rule, \isa{disjE}\@. We invoke it using \methdx{erule}, a 185method designed to work with elimination rules. It looks for an assumption that 186matches the rule's first premise. It deletes the matching assumption, 187regards the first premise as proved and returns subgoals corresponding to 188the remaining premises. When we apply \isa{erule} to \isa{disjE}, only two 189subgoals result. This is better than applying it using \isa{rule} 190to get three subgoals, then proving the first by assumption: the other 191subgoals would have the redundant assumption 192\hbox{\isa{P\ \isasymor\ Q}}. 193Most of the time, \isa{erule} is the best way to use elimination rules, since it 194replaces an assumption by its subformulas; only rarely does the original 195assumption remain useful. 196 197\begin{isabelle} 198%P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline 199\ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline 200\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 201\end{isabelle} 202These are the two subgoals returned by \isa{erule}. The first assumes 203\isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we 204need to show \isa{Q\ \isasymor\ P}\@. The second introduction rule 205(\isa{disjI2}) can reduce this to \isa{P}, which matches the assumption. 206So, we apply the 207\isa{rule} method with \isa{disjI2} \ldots 208\begin{isabelle} 209\ 1.\ P\ \isasymLongrightarrow\ P\isanewline 210\ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 211\end{isabelle} 212\ldots and finish off with the \isa{assumption} 213method. We are left with the other subgoal, which 214assumes \isa{Q}. 215\begin{isabelle} 216\ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P 217\end{isabelle} 218Its proof is similar, using the introduction 219rule \isa{disjI1}. 220 221The result of this proof is a new inference rule \isa{disj_swap}, which is neither 222an introduction nor an elimination rule, but which might 223be useful. We can use it to replace any goal of the form $Q\disj P$ 224by one of the form $P\disj Q$.% 225\index{elimination rules|)} 226 227 228\section{Destruction Rules: Some Examples} 229 230\index{destruction rules|(}% 231Now let us examine the analogous proof for conjunction. 232\begin{isabelle} 233\isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline 234\isacommand{apply}\ (rule\ conjI)\isanewline 235\ \isacommand{apply}\ (drule\ conjunct2)\isanewline 236\ \isacommand{apply}\ assumption\isanewline 237\isacommand{apply}\ (drule\ conjunct1)\isanewline 238\isacommand{apply}\ assumption 239\end{isabelle} 240Recall that the conjunction elimination rules --- whose Isabelle names are 241\isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half 242of a conjunction. Rules of this sort (where the conclusion is a subformula of a 243premise) are called \textbf{destruction} rules because they take apart and destroy 244a premise.% 245\footnote{This Isabelle terminology is not used in standard logic texts, 246although the distinction between the two forms of elimination rule is well known. 247Girard \cite[page 74]{girard89},\index{Girard, Jean-Yves|fnote} 248for example, writes ``The elimination rules 249[for $\disj$ and $\exists$] are very 250bad. What is catastrophic about them is the parasitic presence of a formula [$R$] 251which has no structural link with the formula which is eliminated.'' 252These Isabelle rules are inspired by the sequent calculus.} 253 254The first proof step applies conjunction introduction, leaving 255two subgoals: 256\begin{isabelle} 257%P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline 258\ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline 259\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P 260\end{isabelle} 261 262To invoke the elimination rule, we apply a new method, \isa{drule}. 263Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if 264you prefer). Applying the 265second conjunction rule using \isa{drule} replaces the assumption 266\isa{P\ \isasymand\ Q} by \isa{Q}. 267\begin{isabelle} 268\ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline 269\ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P 270\end{isabelle} 271The resulting subgoal can be proved by applying \isa{assumption}. 272The other subgoal is similarly proved, using the \isa{conjunct1} rule and the 273\isa{assumption} method. 274 275Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to 276you. Isabelle does not attempt to work out whether a rule 277is an introduction rule or an elimination rule. The 278method determines how the rule will be interpreted. Many rules 279can be used in more than one way. For example, \isa{disj_swap} can 280be applied to assumptions as well as to goals; it replaces any 281assumption of the form 282$P\disj Q$ by a one of the form $Q\disj P$. 283 284Destruction rules are simpler in form than indirect rules such as \isa{disjE}, 285but they can be inconvenient. Each of the conjunction rules discards half 286of the formula, when usually we want to take both parts of the conjunction as new 287assumptions. The easiest way to do so is by using an 288alternative conjunction elimination rule that resembles \isa{disjE}\@. It is 289seldom, if ever, seen in logic books. In Isabelle syntax it looks like this: 290\begin{isabelle} 291\isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulenamedx{conjE} 292\end{isabelle} 293\index{destruction rules|)} 294 295\begin{exercise} 296Use the rule \isa{conjE} to shorten the proof above. 297\end{exercise} 298 299 300\section{Implication} 301 302\index{implication|(}% 303At the start of this chapter, we saw the rule \emph{modus ponens}. It is, in fact, 304a destruction rule. The matching introduction rule looks like this 305in Isabelle: 306\begin{isabelle} 307(?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\ 308\isasymlongrightarrow\ ?Q\rulenamedx{impI} 309\end{isabelle} 310And this is \emph{modus ponens}\index{modus ponens@\emph{modus ponens}}: 311\begin{isabelle} 312\isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\ 313\isasymLongrightarrow\ ?Q 314\rulenamedx{mp} 315\end{isabelle} 316 317Here is a proof using the implication rules. This 318lemma performs a sort of uncurrying, replacing the two antecedents 319of a nested implication by a conjunction. The proof illustrates 320how assumptions work. At each proof step, the subgoals inherit the previous 321assumptions, perhaps with additions or deletions. Rules such as 322\isa{impI} and \isa{disjE} add assumptions, while applying \isa{erule} or 323\isa{drule} deletes the matching assumption. 324\begin{isabelle} 325\isacommand{lemma}\ imp_uncurry:\ 326"P\ \isasymlongrightarrow\ (Q\ 327\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ 328\isasymand\ Q\ \isasymlongrightarrow\ 329R"\isanewline 330\isacommand{apply}\ (rule\ impI)\isanewline 331\isacommand{apply}\ (erule\ conjE)\isanewline 332\isacommand{apply}\ (drule\ mp)\isanewline 333\ \isacommand{apply}\ assumption\isanewline 334\isacommand{apply}\ (drule\ mp)\isanewline 335\ \ \isacommand{apply}\ assumption\isanewline 336\ \isacommand{apply}\ assumption 337\end{isabelle} 338First, we state the lemma and apply implication introduction (\isa{rule impI}), 339which moves the conjunction to the assumptions. 340\begin{isabelle} 341%P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\ 342%\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline 343\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R 344\end{isabelle} 345Next, we apply conjunction elimination (\isa{erule conjE}), which splits this 346conjunction into two parts. 347\begin{isabelle} 348\ 1.\ \isasymlbrakk P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\ 349Q\isasymrbrakk\ \isasymLongrightarrow\ R 350\end{isabelle} 351Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\ 352\isasymlongrightarrow\ R)}, where the parentheses have been inserted for 353clarity. The nested implication requires two applications of 354\textit{modus ponens}: \isa{drule mp}. The first use yields the 355implication \isa{Q\ 356\isasymlongrightarrow\ R}, but first we must prove the extra subgoal 357\isa{P}, which we do by assumption. 358\begin{isabelle} 359\ 1.\ \isasymlbrakk P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline 360\ 2.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R 361\end{isabelle} 362Repeating these steps for \isa{Q\ 363\isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}. 364\begin{isabelle} 365\ 1.\ \isasymlbrakk P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ 366\isasymLongrightarrow\ R 367\end{isabelle} 368 369The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow} 370both stand for implication, but they differ in many respects. Isabelle 371uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is 372built-in and Isabelle's inference mechanisms treat it specially. On the 373other hand, \isa{\isasymlongrightarrow} is just one of the many connectives 374available in higher-order logic. We reason about it using inference rules 375such as \isa{impI} and \isa{mp}, just as we reason about the other 376connectives. You will have to use \isa{\isasymlongrightarrow} in any 377context that requires a formula of higher-order logic. Use 378\isa{\isasymLongrightarrow} to separate a theorem's preconditions from its 379conclusion.% 380\index{implication|)} 381 382\medskip 383\index{by@\isacommand{by} (command)|(}% 384The \isacommand{by} command is useful for proofs like these that use 385\isa{assumption} heavily. It executes an 386\isacommand{apply} command, then tries to prove all remaining subgoals using 387\isa{assumption}. Since (if successful) it ends the proof, it also replaces the 388\isacommand{done} symbol. For example, the proof above can be shortened: 389\begin{isabelle} 390\isacommand{lemma}\ imp_uncurry:\ 391"P\ \isasymlongrightarrow\ (Q\ 392\isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ 393\isasymand\ Q\ \isasymlongrightarrow\ 394R"\isanewline 395\isacommand{apply}\ (rule\ impI)\isanewline 396\isacommand{apply}\ (erule\ conjE)\isanewline 397\isacommand{apply}\ (drule\ mp)\isanewline 398\ \isacommand{apply}\ assumption\isanewline 399\isacommand{by}\ (drule\ mp) 400\end{isabelle} 401We could use \isacommand{by} to replace the final \isacommand{apply} and 402\isacommand{done} in any proof, but typically we use it 403to eliminate calls to \isa{assumption}. It is also a nice way of expressing a 404one-line proof.% 405\index{by@\isacommand{by} (command)|)} 406 407 408 409\section{Negation} 410 411\index{negation|(}% 412Negation causes surprising complexity in proofs. Its natural 413deduction rules are straightforward, but additional rules seem 414necessary in order to handle negated assumptions gracefully. This section 415also illustrates the \isa{intro} method: a convenient way of 416applying introduction rules. 417 418Negation introduction deduces $\lnot P$ if assuming $P$ leads to a 419contradiction. Negation elimination deduces any formula in the 420presence of $\lnot P$ together with~$P$: 421\begin{isabelle} 422(?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% 423\rulenamedx{notI}\isanewline 424\isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% 425\rulenamedx{notE} 426\end{isabelle} 427% 428Classical logic allows us to assume $\lnot P$ 429when attempting to prove~$P$: 430\begin{isabelle} 431(\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% 432\rulenamedx{classical} 433\end{isabelle} 434 435\index{contrapositives|(}% 436The implications $P\imp Q$ and $\lnot Q\imp\lnot P$ are logically 437equivalent, and each is called the 438\textbf{contrapositive} of the other. Four further rules support 439reasoning about contrapositives. They differ in the placement of the 440negation symbols: 441\begin{isabelle} 442\isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 443\rulename{contrapos_pp}\isanewline 444\isasymlbrakk?Q;\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ 445\isasymnot\ ?P% 446\rulename{contrapos_pn}\isanewline 447\isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 448\rulename{contrapos_np}\isanewline 449\isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P% 450\rulename{contrapos_nn} 451\end{isabelle} 452% 453These rules are typically applied using the \isa{erule} method, where 454their effect is to form a contrapositive from an 455assumption and the goal's conclusion.% 456\index{contrapositives|)} 457 458The most important of these is \isa{contrapos_np}. It is useful 459for applying introduction rules to negated assumptions. For instance, 460the assumption $\lnot(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we 461might want to use conjunction introduction on it. 462Before we can do so, we must move that assumption so that it 463becomes the conclusion. The following proof demonstrates this 464technique: 465\begin{isabelle} 466\isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\ 467\isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\ 468R"\isanewline 469\isacommand{apply}\ (erule_tac\ Q = "R{\isasymlongrightarrow}Q"\ \isakeyword{in}\ 470contrapos_np)\isanewline 471\isacommand{apply}\ (intro\ impI)\isanewline 472\isacommand{by}\ (erule\ notE) 473\end{isabelle} 474% 475There are two negated assumptions and we need to exchange the conclusion with the 476second one. The method \isa{erule contrapos_np} would select the first assumption, 477which we do not want. So we specify the desired assumption explicitly 478using a new method, \isa{erule_tac}. This is the resulting subgoal: 479\begin{isabelle} 480\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ 481R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q% 482\end{isabelle} 483The former conclusion, namely \isa{R}, now appears negated among the assumptions, 484while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new 485conclusion. 486 487We can now apply introduction rules. We use the \methdx{intro} method, which 488repeatedly applies the given introduction rules. Here its effect is equivalent 489to \isa{rule impI}. 490\begin{isabelle} 491\ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\ 492R\isasymrbrakk\ \isasymLongrightarrow\ Q% 493\end{isabelle} 494We can see a contradiction in the form of assumptions \isa{\isasymnot\ R} 495and~\isa{R}, which suggests using negation elimination. If applied on its own, 496\isa{notE} will select the first negated assumption, which is useless. 497Instead, we invoke the rule using the 498\isa{by} command. 499Now when Isabelle selects the first assumption, it tries to prove \isa{P\ 500\isasymlongrightarrow\ Q} and fails; it then backtracks, finds the 501assumption \isa{\isasymnot~R} and finally proves \isa{R} by assumption. That 502concludes the proof. 503 504\medskip 505 506The following example may be skipped on a first reading. It involves a 507peculiar but important rule, a form of disjunction introduction: 508\begin{isabelle} 509(\isasymnot \ ?Q\ \isasymLongrightarrow \ ?P)\ \isasymLongrightarrow \ ?P\ \isasymor \ ?Q% 510\rulenamedx{disjCI} 511\end{isabelle} 512This rule combines the effects of \isa{disjI1} and \isa{disjI2}. Its great 513advantage is that we can remove the disjunction symbol without deciding 514which disjunction to prove. This treatment of disjunction is standard in sequent 515and tableau calculi. 516 517\begin{isabelle} 518\isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\ 519\isasymLongrightarrow\ P\ \isasymor\ (Q\ \isasymand\ R)"\isanewline 520\isacommand{apply}\ (rule\ disjCI)\isanewline 521\isacommand{apply}\ (elim\ conjE\ disjE)\isanewline 522\ \isacommand{apply}\ assumption 523\isanewline 524\isacommand{by}\ (erule\ contrapos_np,\ rule\ conjI) 525\end{isabelle} 526% 527The first proof step to applies the introduction rules \isa{disjCI}. 528The resulting subgoal has the negative assumption 529\hbox{\isa{\isasymnot(Q\ \isasymand\ R)}}. 530 531\begin{isabelle} 532\ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\ 533R)\isasymrbrakk\ \isasymLongrightarrow\ P% 534\end{isabelle} 535Next we apply the \isa{elim} method, which repeatedly applies 536elimination rules; here, the elimination rules given 537in the command. One of the subgoals is trivial (\isa{\isacommand{apply} assumption}), 538leaving us with one other: 539\begin{isabelle} 540\ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P% 541\end{isabelle} 542% 543Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The 544combination 545\begin{isabelle} 546\ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI) 547\end{isabelle} 548is robust: the \isa{conjI} forces the \isa{erule} to select a 549conjunction. The two subgoals are the ones we would expect from applying 550conjunction introduction to 551\isa{Q~\isasymand~R}: 552\begin{isabelle} 553\ 1.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ 554Q\isanewline 555\ 2.\ \isasymlbrakk R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R% 556\end{isabelle} 557They are proved by assumption, which is implicit in the \isacommand{by} 558command.% 559\index{negation|)} 560 561 562\section{Interlude: the Basic Methods for Rules} 563 564We have seen examples of many tactics that operate on individual rules. It 565may be helpful to review how they work given an arbitrary rule such as this: 566\[ \infer{Q}{P@1 & \ldots & P@n} \] 567Below, we refer to $P@1$ as the \bfindex{major premise}. This concept 568applies only to elimination and destruction rules. These rules act upon an 569instance of their major premise, typically to replace it by subformulas of itself. 570 571Suppose that the rule above is called~\isa{R}\@. Here are the basic rule 572methods, most of which we have already seen: 573\begin{itemize} 574\item 575Method \isa{rule\ R} unifies~$Q$ with the current subgoal, replacing it 576by $n$ new subgoals: instances of $P@1$, \ldots,~$P@n$. 577This is backward reasoning and is appropriate for introduction rules. 578\item 579Method \isa{erule\ R} unifies~$Q$ with the current subgoal and 580simultaneously unifies $P@1$ with some assumption. The subgoal is 581replaced by the $n-1$ new subgoals of proving 582instances of $P@2$, 583\ldots,~$P@n$, with the matching assumption deleted. It is appropriate for 584elimination rules. The method 585\isa{(rule\ R,\ assumption)} is similar, but it does not delete an 586assumption. 587\item 588Method \isa{drule\ R} unifies $P@1$ with some assumption, which it 589then deletes. The subgoal is 590replaced by the $n-1$ new subgoals of proving $P@2$, \ldots,~$P@n$; an 591$n$th subgoal is like the original one but has an additional assumption: an 592instance of~$Q$. It is appropriate for destruction rules. 593\item 594Method \isa{frule\ R} is like \isa{drule\ R} except that the matching 595assumption is not deleted. (See {\S}\ref{sec:frule} below.) 596\end{itemize} 597 598Other methods apply a rule while constraining some of its 599variables. The typical form is 600\begin{isabelle} 601\ \ \ \ \ \methdx{rule_tac}\ $v@1$ = $t@1$ \isakeyword{and} \ldots \isakeyword{and} 602$v@k$ = 603$t@k$ \isakeyword{in} R 604\end{isabelle} 605This method behaves like \isa{rule R}, while instantiating the variables 606$v@1$, \ldots, 607$v@k$ as specified. We similarly have \methdx{erule_tac}, \methdx{drule_tac} and 608\methdx{frule_tac}. These methods also let us specify which subgoal to 609operate on. By default it is the first subgoal, as with nearly all 610methods, but we can specify that rule \isa{R} should be applied to subgoal 611number~$i$: 612\begin{isabelle} 613\ \ \ \ \ rule_tac\ [$i$] R 614\end{isabelle} 615 616 617 618\section{Unification and Substitution}\label{sec:unification} 619 620\index{unification|(}% 621As we have seen, Isabelle rules involve schematic variables, which begin with 622a question mark and act as 623placeholders for terms. \textbf{Unification} --- well known to Prolog programmers --- is the act of 624making two terms identical, possibly replacing their schematic variables by 625terms. The simplest case is when the two terms are already the same. Next 626simplest is \textbf{pattern-matching}, which replaces variables in only one of the 627terms. The 628\isa{rule} method typically matches the rule's conclusion 629against the current subgoal. The 630\isa{assumption} method matches the current subgoal's conclusion 631against each of its assumptions. Unification can instantiate variables in both terms; the \isa{rule} method can do this if the goal 632itself contains schematic variables. Other occurrences of the variables in 633the rule or proof state are updated at the same time. 634 635Schematic variables in goals represent unknown terms. Given a goal such 636as $\exists x.\,P$, they let us proceed with a proof. They can be 637filled in later, sometimes in stages and often automatically. 638 639\begin{pgnote} 640If unification fails when you think it should succeed, try setting the Proof General flag \pgmenu{Isabelle} $>$ \pgmenu{Settings} $>$ 641\pgmenu{Trace Unification}, 642which makes Isabelle show the cause of unification failures (in Proof 643General's \pgmenu{Trace} buffer). 644\end{pgnote} 645\noindent 646For example, suppose we are trying to prove this subgoal by assumption: 647\begin{isabelle} 648\ 1.\ P\ (a,\ f\ (b,\ g\ (e,\ a),\ b),\ a)\ \isasymLongrightarrow \ P\ (a,\ f\ (b,\ g\ (c,\ a),\ b),\ a) 649\end{isabelle} 650The \isa{assumption} method having failed, we try again with the flag set: 651\begin{isabelle} 652\isacommand{apply} assumption 653\end{isabelle} 654In this trivial case, the output clearly shows that \isa{e} clashes with \isa{c}: 655\begin{isabelle} 656Clash: e =/= c 657\end{isabelle} 658 659Isabelle uses 660\textbf{higher-order} unification, which works in the 661typed $\lambda$-calculus. The procedure requires search and is potentially 662undecidable. For our purposes, however, the differences from ordinary 663unification are straightforward. It handles bound variables 664correctly, avoiding capture. The two terms 665\isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are 666trivially unifiable because they differ only by a bound variable renaming. The two terms \isa{{\isasymlambda}x.\ ?P} and 667\isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by 668\isa{t x} is forbidden because the free occurrence of~\isa{x} would become 669bound. Unfortunately, even if \isa{trace_unify_fail} is set, Isabelle displays no information about this type of failure. 670 671\begin{warn} 672Higher-order unification sometimes must invent 673$\lambda$-terms to replace function variables, 674which can lead to a combinatorial explosion. However, Isabelle proofs tend 675to involve easy cases where there are few possibilities for the 676$\lambda$-term being constructed. In the easiest case, the 677function variable is applied only to bound variables, 678as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and 679\isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace 680\isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most 681one unifier, like ordinary unification. A harder case is 682unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h}, 683namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}. 684Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is 685exponential in the number of occurrences of~\isa{a} in the second term. 686\end{warn} 687 688 689 690\subsection{Substitution and the {\tt\slshape subst} Method} 691\label{sec:subst} 692 693\index{substitution|(}% 694Isabelle also uses function variables to express \textbf{substitution}. 695A typical substitution rule allows us to replace one term by 696another if we know that two terms are equal. 697\[ \infer{P[t/x]}{s=t & P[s/x]} \] 698The rule uses a notation for substitution: $P[t/x]$ is the result of 699replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions 700designated by~$x$. For example, it can 701derive symmetry of equality from reflexivity. Using $x=s$ for~$P$ 702replaces just the first $s$ in $s=s$ by~$t$: 703\[ \infer{t=s}{s=t & \infer{s=s}{}} \] 704 705The Isabelle version of the substitution rule looks like this: 706\begin{isabelle} 707\isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\ 708?t 709\rulenamedx{ssubst} 710\end{isabelle} 711Crucially, \isa{?P} is a function 712variable. It can be replaced by a $\lambda$-term 713with one bound variable, whose occurrences identify the places 714in which $s$ will be replaced by~$t$. The proof above requires \isa{?P} 715to be replaced by \isa{{\isasymlambda}x.~x=s}; the second premise will then 716be \isa{s=s} and the conclusion will be \isa{t=s}. 717 718The \isa{simp} method also replaces equals by equals, but the substitution 719rule gives us more control. Consider this proof: 720\begin{isabelle} 721\isacommand{lemma}\ 722"\isasymlbrakk x\ =\ f\ x;\ odd(f\ x)\isasymrbrakk\ \isasymLongrightarrow\ 723odd\ x"\isanewline 724\isacommand{by}\ (erule\ ssubst) 725\end{isabelle} 726% 727The assumption \isa{x\ =\ f\ x}, if used for rewriting, would loop, 728replacing \isa{x} by \isa{f x} and then by 729\isa{f(f x)} and so forth. (Here \isa{simp} 730would see the danger and would re-orient the equality, but in more complicated 731cases it can be fooled.) When we apply the substitution rule, 732Isabelle replaces every 733\isa{x} in the subgoal by \isa{f x} just once. It cannot loop. The 734resulting subgoal is trivial by assumption, so the \isacommand{by} command 735proves it implicitly. 736 737We are using the \isa{erule} method in a novel way. Hitherto, 738the conclusion of the rule was just a variable such as~\isa{?R}, but it may 739be any term. The conclusion is unified with the subgoal just as 740it would be with the \isa{rule} method. At the same time \isa{erule} looks 741for an assumption that matches the rule's first premise, as usual. With 742\isa{ssubst} the effect is to find, use and delete an equality 743assumption. 744 745The \methdx{subst} method performs individual substitutions. In simple cases, 746it closely resembles a use of the substitution rule. Suppose a 747proof has reached this point: 748\begin{isabelle} 749\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ \isasymLongrightarrow \ f\ z\ =\ x\ *\ y% 750\end{isabelle} 751Now we wish to apply a commutative law: 752\begin{isabelle} 753?m\ *\ ?n\ =\ ?n\ *\ ?m% 754\rulename{mult.commute} 755\end{isabelle} 756Isabelle rejects our first attempt: 757\begin{isabelle} 758apply (simp add: mult.commute) 759\end{isabelle} 760The simplifier notices the danger of looping and refuses to apply the 761rule.% 762\footnote{More precisely, it only applies such a rule if the new term is 763smaller under a specified ordering; here, \isa{x\ *\ y} 764is already smaller than 765\isa{y\ *\ x}.} 766% 767The \isa{subst} method applies \isa{mult.commute} exactly once. 768\begin{isabelle} 769\isacommand{apply}\ (subst\ mult.commute)\isanewline 770\ 1.\ \isasymlbrakk P\ x\ y\ z;\ Suc\ x\ <\ y\isasymrbrakk \ 771\isasymLongrightarrow \ f\ z\ =\ y\ *\ x% 772\end{isabelle} 773As we wanted, \isa{x\ *\ y} has become \isa{y\ *\ x}. 774 775\medskip 776This use of the \methdx{subst} method has the same effect as the command 777\begin{isabelle} 778\isacommand{apply}\ (rule\ mult.commute [THEN ssubst]) 779\end{isabelle} 780The attribute \isa{THEN}, which combines two rules, is described in 781{\S}\ref{sec:THEN} below. The \methdx{subst} method is more powerful than 782applying the substitution rule. It can perform substitutions in a subgoal's 783assumptions. Moreover, if the subgoal contains more than one occurrence of 784the left-hand side of the equality, the \methdx{subst} method lets us specify which occurrence should be replaced. 785 786 787\subsection{Unification and Its Pitfalls} 788 789Higher-order unification can be tricky. Here is an example, which you may 790want to skip on your first reading: 791\begin{isabelle} 792\isacommand{lemma}\ "\isasymlbrakk x\ =\ 793f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ 794\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 795\isacommand{apply}\ (erule\ ssubst)\isanewline 796\isacommand{back}\isanewline 797\isacommand{back}\isanewline 798\isacommand{back}\isanewline 799\isacommand{back}\isanewline 800\isacommand{apply}\ assumption\isanewline 801\isacommand{done} 802\end{isabelle} 803% 804By default, Isabelle tries to substitute for all the 805occurrences. Applying \isa{erule\ ssubst} yields this subgoal: 806\begin{isabelle} 807\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x) 808\end{isabelle} 809The substitution should have been done in the first two occurrences 810of~\isa{x} only. Isabelle has gone too far. The \commdx{back} 811command allows us to reject this possibility and demand a new one: 812\begin{isabelle} 813\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x) 814\end{isabelle} 815% 816Now Isabelle has left the first occurrence of~\isa{x} alone. That is 817promising but it is not the desired combination. So we use \isacommand{back} 818again: 819\begin{isabelle} 820\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x) 821\end{isabelle} 822% 823This also is wrong, so we use \isacommand{back} again: 824\begin{isabelle} 825\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x) 826\end{isabelle} 827% 828And this one is wrong too. Looking carefully at the series 829of alternatives, we see a binary countdown with reversed bits: 111, 830011, 101, 001. Invoke \isacommand{back} again: 831\begin{isabelle} 832\ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x% 833\end{isabelle} 834At last, we have the right combination! This goal follows by assumption.% 835\index{unification|)} 836 837\medskip 838This example shows that unification can do strange things with 839function variables. We were forced to select the right unifier using the 840\isacommand{back} command. That is all right during exploration, but \isacommand{back} 841should never appear in the final version of a proof. You can eliminate the 842need for \isacommand{back} by giving Isabelle less freedom when you apply a rule. 843 844One way to constrain the inference is by joining two methods in a 845\isacommand{apply} command. Isabelle applies the first method and then the 846second. If the second method fails then Isabelle automatically backtracks. 847This process continues until the first method produces an output that the 848second method can use. We get a one-line proof of our example: 849\begin{isabelle} 850\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ 851\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 852\isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline 853\isacommand{done} 854\end{isabelle} 855 856\noindent 857The \isacommand{by} command works too, since it backtracks when 858proving subgoals by assumption: 859\begin{isabelle} 860\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ 861\isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 862\isacommand{by}\ (erule\ ssubst) 863\end{isabelle} 864 865 866The most general way to constrain unification is 867by instantiating variables in the rule. The method \isa{rule_tac} is 868similar to \isa{rule}, but it 869makes some of the rule's variables denote specified terms. 870Also available are {\isa{drule_tac}} and \isa{erule_tac}. Here we need 871\isa{erule_tac} since above we used \isa{erule}. 872\begin{isabelle} 873\isacommand{lemma}\ "\isasymlbrakk x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline 874\isacommand{by}\ (erule_tac\ P = "\isasymlambda u.\ triple\ u\ u\ x"\ 875\isakeyword{in}\ ssubst) 876\end{isabelle} 877% 878To specify a desired substitution 879requires instantiating the variable \isa{?P} with a $\lambda$-expression. 880The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\ 881u\ x} indicate that the first two arguments have to be substituted, leaving 882the third unchanged. With this instantiation, backtracking is neither necessary 883nor possible. 884 885An alternative to \isa{rule_tac} is to use \isa{rule} with a theorem 886modified using~\isa{of}, described in 887{\S}\ref{sec:forward} below. But \isa{rule_tac}, unlike \isa{of}, can 888express instantiations that refer to 889\isasymAnd-bound variables in the current subgoal.% 890\index{substitution|)} 891 892 893\section{Quantifiers} 894 895\index{quantifiers!universal|(}% 896Quantifiers require formalizing syntactic substitution and the notion of 897arbitrary value. Consider the universal quantifier. In a logic 898book, its introduction rule looks like this: 899\[ \infer{\forall x.\,P}{P} \] 900Typically, a proviso written in English says that $x$ must not 901occur in the assumptions. This proviso guarantees that $x$ can be regarded as 902arbitrary, since it has not been assumed to satisfy any special conditions. 903Isabelle's underlying formalism, called the 904\bfindex{meta-logic}, eliminates the need for English. It provides its own 905universal quantifier (\isasymAnd) to express the notion of an arbitrary value. 906We have already seen another operator of the meta-logic, namely 907\isa\isasymLongrightarrow, which expresses inference rules and the treatment 908of assumptions. The only other operator in the meta-logic is \isa\isasymequiv, 909which can be used to define constants. 910 911\subsection{The Universal Introduction Rule} 912 913Returning to the universal quantifier, we find that having a similar quantifier 914as part of the meta-logic makes the introduction rule trivial to express: 915\begin{isabelle} 916(\isasymAnd x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulenamedx{allI} 917\end{isabelle} 918 919 920The following trivial proof demonstrates how the universal introduction 921rule works. 922\begin{isabelle} 923\isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline 924\isacommand{apply}\ (rule\ allI)\isanewline 925\isacommand{by}\ (rule\ impI) 926\end{isabelle} 927The first step invokes the rule by applying the method \isa{rule allI}. 928\begin{isabelle} 929\ 1.\ \isasymAnd x.\ P\ x\ \isasymlongrightarrow\ P\ x 930\end{isabelle} 931Note that the resulting proof state has a bound variable, 932namely~\isa{x}. The rule has replaced the universal quantifier of 933higher-order logic by Isabelle's meta-level quantifier. Our goal is to 934prove 935\isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is 936an implication, so we apply the corresponding introduction rule (\isa{impI}). 937\begin{isabelle} 938\ 1.\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow\ P\ x 939\end{isabelle} 940This last subgoal is implicitly proved by assumption. 941 942\subsection{The Universal Elimination Rule} 943 944Now consider universal elimination. In a logic text, 945the rule looks like this: 946\[ \infer{P[t/x]}{\forall x.\,P} \] 947The conclusion is $P$ with $t$ substituted for the variable~$x$. 948Isabelle expresses substitution using a function variable: 949\begin{isabelle} 950{\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulenamedx{spec} 951\end{isabelle} 952This destruction rule takes a 953universally quantified formula and removes the quantifier, replacing 954the bound variable \isa{x} by the schematic variable \isa{?x}. Recall that a 955schematic variable starts with a question mark and acts as a 956placeholder: it can be replaced by any term. 957 958The universal elimination rule is also 959available in the standard elimination format. Like \isa{conjE}, it never 960appears in logic books: 961\begin{isabelle} 962\isasymlbrakk \isasymforall x.\ ?P\ x;\ ?P\ ?x\ \isasymLongrightarrow \ ?R\isasymrbrakk \ \isasymLongrightarrow \ ?R% 963\rulenamedx{allE} 964\end{isabelle} 965The methods \isa{drule~spec} and \isa{erule~allE} do precisely the 966same inference. 967 968To see how $\forall$-elimination works, let us derive a rule about reducing 969the scope of a universal quantifier. In mathematical notation we write 970\[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] 971with the proviso ``$x$ not free in~$P$.'' Isabelle's treatment of 972substitution makes the proviso unnecessary. The conclusion is expressed as 973\isa{P\ 974\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the 975variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a 976bound variable capture. Let us walk through the proof. 977\begin{isabelle} 978\isacommand{lemma}\ "(\isasymforall x.\ P\ \isasymlongrightarrow \ Q\ x)\ 979\isasymLongrightarrow \ P\ \isasymlongrightarrow \ (\isasymforall x.\ Q\ 980x)" 981\end{isabelle} 982First we apply implies introduction (\isa{impI}), 983which moves the \isa{P} from the conclusion to the assumptions. Then 984we apply universal introduction (\isa{allI}). 985\begin{isabelle} 986\isacommand{apply}\ (rule\ impI,\ rule\ allI)\isanewline 987\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ 988x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x 989\end{isabelle} 990As before, it replaces the HOL 991quantifier by a meta-level quantifier, producing a subgoal that 992binds the variable~\isa{x}. The leading bound variables 993(here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\ 994\isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the 995conclusion, here \isa{Q\ x}. Subgoals inherit the context, 996although assumptions can be added or deleted (as we saw 997earlier), while rules such as \isa{allI} add bound variables. 998 999Now, to reason from the universally quantified 1000assumption, we apply the elimination rule using the \isa{drule} 1001method. This rule is called \isa{spec} because it specializes a universal formula 1002to a particular term. 1003\begin{isabelle} 1004\isacommand{apply}\ (drule\ spec)\isanewline 1005\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ P\ \isasymlongrightarrow\ Q\ (?x2\ 1006x)\isasymrbrakk\ \isasymLongrightarrow\ Q\ x 1007\end{isabelle} 1008Observe how the context has changed. The quantified formula is gone, 1009replaced by a new assumption derived from its body. We have 1010removed the quantifier and replaced the bound variable 1011by the curious term 1012\isa{?x2~x}. This term is a placeholder: it may become any term that can be 1013built from~\isa{x}. (Formally, \isa{?x2} is an unknown of function type, applied 1014to the argument~\isa{x}.) This new assumption is an implication, so we can use 1015\emph{modus ponens} on it, which concludes the proof. 1016\begin{isabelle} 1017\isacommand{by}\ (drule\ mp) 1018\end{isabelle} 1019Let us take a closer look at this last step. \emph{Modus ponens} yields 1020two subgoals: one where we prove the antecedent (in this case \isa{P}) and 1021one where we may assume the consequent. Both of these subgoals are proved 1022by the 1023\isa{assumption} method, which is implicit in the 1024\isacommand{by} command. Replacing the \isacommand{by} command by 1025\isa{\isacommand{apply} (drule\ mp, assumption)} would have left one last 1026subgoal: 1027\begin{isabelle} 1028\ 1.\ \isasymAnd x.\ \isasymlbrakk P;\ Q\ (?x2\ x)\isasymrbrakk\ 1029\isasymLongrightarrow\ Q\ x 1030\end{isabelle} 1031The consequent is \isa{Q} applied to that placeholder. It may be replaced by any 1032term built from~\isa{x}, and here 1033it should simply be~\isa{x}. The assumption need not 1034be identical to the conclusion, provided the two formulas are unifiable.% 1035\index{quantifiers!universal|)} 1036 1037 1038\subsection{The Existential Quantifier} 1039 1040\index{quantifiers!existential|(}% 1041The concepts just presented also apply 1042to the existential quantifier, whose introduction rule looks like this in 1043Isabelle: 1044\begin{isabelle} 1045?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulenamedx{exI} 1046\end{isabelle} 1047If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x. 1048P(x)$ is also true. It is a dual of the universal elimination rule, and 1049logic texts present it using the same notation for substitution. 1050 1051The existential 1052elimination rule looks like this 1053in a logic text: 1054\[ \infer{Q}{\exists x.\,P & \infer*{Q}{[P]}} \] 1055% 1056It looks like this in Isabelle: 1057\begin{isabelle} 1058\isasymlbrakk{\isasymexists}x.\ ?P\ x;\ \isasymAnd x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulenamedx{exE} 1059\end{isabelle} 1060% 1061Given an existentially quantified theorem and some 1062formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with 1063the universal introduction rule, the textbook version imposes a proviso on the 1064quantified variable, which Isabelle expresses using its meta-logic. It is 1065enough to have a universal quantifier in the meta-logic; we do not need an existential 1066quantifier to be built in as well. 1067 1068 1069\begin{exercise} 1070Prove the lemma 1071\[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \] 1072\emph{Hint}: the proof is similar 1073to the one just above for the universal quantifier. 1074\end{exercise} 1075\index{quantifiers!existential|)} 1076 1077 1078\subsection{Renaming a Bound Variable: {\tt\slshape rename_tac}} 1079 1080\index{assumptions!renaming|(}\index{*rename_tac (method)|(}% 1081When you apply a rule such as \isa{allI}, the quantified variable 1082becomes a new bound variable of the new subgoal. Isabelle tries to avoid 1083changing its name, but sometimes it has to choose a new name in order to 1084avoid a clash. The result may not be ideal: 1085\begin{isabelle} 1086\isacommand{lemma}\ "x\ <\ y\ \isasymLongrightarrow \ \isasymforall x\ y.\ P\ x\ 1087(f\ y)"\isanewline 1088\isacommand{apply}\ (intro allI)\isanewline 1089\ 1.\ \isasymAnd xa\ ya.\ x\ <\ y\ \isasymLongrightarrow \ P\ xa\ (f\ ya) 1090\end{isabelle} 1091% 1092The names \isa{x} and \isa{y} were already in use, so the new bound variables are 1093called \isa{xa} and~\isa{ya}. You can rename them by invoking \isa{rename_tac}: 1094 1095\begin{isabelle} 1096\isacommand{apply}\ (rename_tac\ v\ w)\isanewline 1097\ 1.\ \isasymAnd v\ w.\ x\ <\ y\ \isasymLongrightarrow \ P\ v\ (f\ w) 1098\end{isabelle} 1099Recall that \isa{rule_tac}\index{*rule_tac (method)!and renaming} 1100instantiates a 1101theorem with specified terms. These terms may involve the goal's bound 1102variables, but beware of referring to variables 1103like~\isa{xa}. A future change to your theories could change the set of names 1104produced at top level, so that \isa{xa} changes to~\isa{xb} or reverts to~\isa{x}. 1105It is safer to rename automatically-generated variables before mentioning them. 1106 1107If the subgoal has more bound variables than there are names given to 1108\isa{rename_tac}, the rightmost ones are renamed.% 1109\index{assumptions!renaming|)}\index{*rename_tac (method)|)} 1110 1111 1112\subsection{Reusing an Assumption: {\tt\slshape frule}} 1113\label{sec:frule} 1114 1115\index{assumptions!reusing|(}\index{*frule (method)|(}% 1116Note that \isa{drule spec} removes the universal quantifier and --- as 1117usual with elimination rules --- discards the original formula. Sometimes, a 1118universal formula has to be kept so that it can be used again. Then we use a new 1119method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces 1120the selected assumption. The \isa{f} is for \emph{forward}. 1121 1122In this example, going from \isa{P\ a} to \isa{P(h(h~a))} 1123requires two uses of the quantified assumption, one for each~\isa{h} 1124in~\isa{h(h~a)}. 1125\begin{isabelle} 1126\isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x); 1127\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(h\ (h\ a))" 1128\end{isabelle} 1129% 1130Examine the subgoal left by \isa{frule}: 1131\begin{isabelle} 1132\isacommand{apply}\ (frule\ spec)\isanewline 1133\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (h\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 1134\end{isabelle} 1135It is what \isa{drule} would have left except that the quantified 1136assumption is still present. Next we apply \isa{mp} to the 1137implication and the assumption~\isa{P\ a}: 1138\begin{isabelle} 1139\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline 1140\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 1141\end{isabelle} 1142% 1143We have created the assumption \isa{P(h\ a)}, which is progress. To 1144continue the proof, we apply \isa{spec} again. We shall not need it 1145again, so we can use 1146\isa{drule}. 1147\begin{isabelle} 1148\isacommand{apply}\ (drule\ spec)\isanewline 1149\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ ?x2\ 1150\isasymlongrightarrow \ P\ (h\ ?x2)\isasymrbrakk \ \isasymLongrightarrow \ 1151P\ (h\ (h\ a)) 1152\end{isabelle} 1153% 1154The new assumption bridges the gap between \isa{P(h\ a)} and \isa{P(h(h\ a))}. 1155\begin{isabelle} 1156\isacommand{by}\ (drule\ mp) 1157\end{isabelle} 1158 1159\medskip 1160\emph{A final remark}. Replacing this \isacommand{by} command with 1161\begin{isabelle} 1162\isacommand{apply}\ (drule\ mp,\ assumption) 1163\end{isabelle} 1164would not work: it would add a second copy of \isa{P(h~a)} instead 1165of the desired assumption, \isa{P(h(h~a))}. The \isacommand{by} 1166command forces Isabelle to backtrack until it finds the correct one. 1167Alternatively, we could have used the \isacommand{apply} command and bundled the 1168\isa{drule mp} with \emph{two} calls of \isa{assumption}. Or, of course, 1169we could have given the entire proof to \isa{auto}.% 1170\index{assumptions!reusing|)}\index{*frule (method)|)} 1171 1172 1173 1174\subsection{Instantiating a Quantifier Explicitly} 1175\index{quantifiers!instantiating} 1176 1177We can prove a theorem of the form $\exists x.\,P\, x$ by exhibiting a 1178suitable term~$t$ such that $P\,t$ is true. Dually, we can use an 1179assumption of the form $\forall x.\,P\, x$ to generate a new assumption $P\,t$ for 1180a suitable term~$t$. In many cases, 1181Isabelle makes the correct choice automatically, constructing the term by 1182unification. In other cases, the required term is not obvious and we must 1183specify it ourselves. Suitable methods are \isa{rule_tac}, \isa{drule_tac} 1184and \isa{erule_tac}. 1185 1186We have seen (just above, {\S}\ref{sec:frule}) a proof of this lemma: 1187\begin{isabelle} 1188\isacommand{lemma}\ "\isasymlbrakk \isasymforall x.\ P\ x\ 1189\isasymlongrightarrow \ P\ (h\ x);\ P\ a\isasymrbrakk \ 1190\isasymLongrightarrow \ P(h\ (h\ a))" 1191\end{isabelle} 1192We had reached this subgoal: 1193\begin{isabelle} 1194\ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (h\ 1195x);\ P\ a;\ P\ (h\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (h\ (h\ a)) 1196\end{isabelle} 1197% 1198The proof requires instantiating the quantified assumption with the 1199term~\isa{h~a}. 1200\begin{isabelle} 1201\isacommand{apply}\ (drule_tac\ x\ =\ "h\ a"\ \isakeyword{in}\ 1202spec)\isanewline 1203\ 1.\ \isasymlbrakk P\ a;\ P\ (h\ a);\ P\ (h\ a)\ \isasymlongrightarrow \ 1204P\ (h\ (h\ a))\isasymrbrakk \ \isasymLongrightarrow \ P\ (h\ (h\ a)) 1205\end{isabelle} 1206We have forced the desired instantiation. 1207 1208\medskip 1209Existential formulas can be instantiated too. The next example uses the 1210\textbf{divides} relation\index{divides relation} 1211of number theory: 1212\begin{isabelle} 1213?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k 1214\rulename{dvd_def} 1215\end{isabelle} 1216 1217Let us prove that multiplication of natural numbers is monotone with 1218respect to the divides relation: 1219\begin{isabelle} 1220\isacommand{lemma}\ mult_dvd_mono:\ "{\isasymlbrakk}i\ dvd\ m;\ j\ dvd\ 1221n\isasymrbrakk\ \isasymLongrightarrow\ i*j\ dvd\ (m*n\ ::\ nat)"\isanewline 1222\isacommand{apply}\ (simp\ add:\ dvd_def) 1223\end{isabelle} 1224% 1225Unfolding the definition of divides has left this subgoal: 1226\begin{isabelle} 1227\ 1.\ \isasymlbrakk \isasymexists k.\ m\ =\ i\ *\ k;\ \isasymexists k.\ n\ 1228=\ j\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ 1229n\ =\ i\ *\ j\ *\ k 1230\end{isabelle} 1231% 1232Next, we eliminate the two existential quantifiers in the assumptions: 1233\begin{isabelle} 1234\isacommand{apply}\ (erule\ exE)\isanewline 1235\ 1.\ \isasymAnd k.\ \isasymlbrakk \isasymexists k.\ n\ =\ j\ *\ k;\ m\ =\ 1236i\ *\ k\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ 1237=\ i\ *\ j\ *\ k% 1238\isanewline 1239\isacommand{apply}\ (erule\ exE) 1240\isanewline 1241\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ 1242ka\isasymrbrakk \ \isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\ 1243*\ j\ *\ k 1244\end{isabelle} 1245% 1246The term needed to instantiate the remaining quantifier is~\isa{k*ka}. But 1247\isa{ka} is an automatically-generated name. As noted above, references to 1248such variable names makes a proof less resilient to future changes. So, 1249first we rename the most recent variable to~\isa{l}: 1250\begin{isabelle} 1251\isacommand{apply}\ (rename_tac\ l)\isanewline 1252\ 1.\ \isasymAnd k\ l.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ l\isasymrbrakk \ 1253\isasymLongrightarrow \ \isasymexists k.\ m\ *\ n\ =\ i\ *\ j\ *\ k% 1254\end{isabelle} 1255 1256We instantiate the quantifier with~\isa{k*l}: 1257\begin{isabelle} 1258\isacommand{apply}\ (rule_tac\ x="k*l"\ \isakeyword{in}\ exI)\ \isanewline 1259\ 1.\ \isasymAnd k\ ka.\ \isasymlbrakk m\ =\ i\ *\ k;\ n\ =\ j\ *\ 1260ka\isasymrbrakk \ \isasymLongrightarrow \ m\ *\ n\ =\ i\ 1261*\ j\ *\ (k\ *\ ka) 1262\end{isabelle} 1263% 1264The rest is automatic, by arithmetic. 1265\begin{isabelle} 1266\isacommand{apply}\ simp\isanewline 1267\isacommand{done}\isanewline 1268\end{isabelle} 1269 1270 1271 1272\section{Description Operators} 1273\label{sec:SOME} 1274 1275\index{description operators|(}% 1276HOL provides two description operators. 1277A \textbf{definite description} formalizes the word ``the,'' as in 1278``the greatest divisior of~$n$.'' 1279It returns an arbitrary value unless the formula has a unique solution. 1280An \textbf{indefinite description} formalizes the word ``some,'' as in 1281``some member of~$S$.'' It differs from a definite description in not 1282requiring the solution to be unique: it uses the axiom of choice to pick any 1283solution. 1284 1285\begin{warn} 1286Description operators can be hard to reason about. Novices 1287should try to avoid them. Fortunately, descriptions are seldom required. 1288\end{warn} 1289 1290\subsection{Definite Descriptions} 1291 1292\index{descriptions!definite}% 1293A definite description is traditionally written $\iota x. P(x)$. It denotes 1294the $x$ such that $P(x)$ is true, provided there exists a unique such~$x$; 1295otherwise, it returns an arbitrary value of the expected type. 1296Isabelle uses \sdx{THE} for the Greek letter~$\iota$. 1297 1298%(The traditional notation could be provided, but it is not legible on screen.) 1299 1300We reason using this rule, where \isa{a} is the unique solution: 1301\begin{isabelle} 1302\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 1303\isasymLongrightarrow \ (THE\ x.\ P\ x)\ =\ a% 1304\rulenamedx{the_equality} 1305\end{isabelle} 1306For instance, we can define the 1307cardinality of a finite set~$A$ to be that 1308$n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$. We can then 1309prove that the cardinality of the empty set is zero (since $n=0$ satisfies the 1310description) and proceed to prove other facts. 1311 1312A more challenging example illustrates how Isabelle/HOL defines the least number 1313operator, which denotes the least \isa{x} satisfying~\isa{P}:% 1314\index{least number operator|see{\protect\isa{LEAST}}} 1315\begin{isabelle} 1316(LEAST\ x.\ P\ x)\ = (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ 1317P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)) 1318\end{isabelle} 1319% 1320Let us prove the analogue of \isa{the_equality} for \sdx{LEAST}\@. 1321\begin{isabelle} 1322\isacommand{theorem}\ Least_equality:\isanewline 1323\ \ \ \ \ "\isasymlbrakk P\ (k::nat);\ \ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ (LEAST\ x.\ P\ x)\ =\ k"\isanewline 1324\isacommand{apply}\ (simp\ add:\ Least_def)\isanewline 1325\isanewline 1326\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x\isasymrbrakk \isanewline 1327\isaindent{\ 1.\ }\isasymLongrightarrow \ (THE\ x.\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y))\ =\ k% 1328\end{isabelle} 1329The first step has merely unfolded the definition. 1330\begin{isabelle} 1331\isacommand{apply}\ (rule\ the_equality)\isanewline 1332\isanewline 1333\ 1.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ 1334\isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ P\ k\ \isasymand \ 1335(\isasymforall y.\ P\ y\ \isasymlongrightarrow \ k\ \isasymle \ y)\isanewline 1336\ 2.\ \isasymAnd x.\ \isasymlbrakk P\ k;\ \isasymforall x.\ P\ x\ \isasymlongrightarrow \ k\ \isasymle \ x;\ P\ x\ \isasymand \ (\isasymforall y.\ P\ y\ \isasymlongrightarrow \ x\ \isasymle \ y)\isasymrbrakk \isanewline 1337\ \ \ \ \ \ \ \ \isasymLongrightarrow \ x\ =\ k% 1338\end{isabelle} 1339As always with \isa{the_equality}, we must show existence and 1340uniqueness of the claimed solution,~\isa{k}. Existence, the first 1341subgoal, is trivial. Uniqueness, the second subgoal, follows by antisymmetry: 1342\begin{isabelle} 1343\isasymlbrakk x\ \isasymle \ y;\ y\ \isasymle \ x\isasymrbrakk \ \isasymLongrightarrow \ x\ =\ y% 1344\rulename{order_antisym} 1345\end{isabelle} 1346The assumptions imply both \isa{k~\isasymle~x} and \isa{x~\isasymle~k}. One 1347call to \isa{auto} does it all: 1348\begin{isabelle} 1349\isacommand{by}\ (auto\ intro:\ order_antisym) 1350\end{isabelle} 1351 1352 1353\subsection{Indefinite Descriptions} 1354 1355\index{Hilbert's $\varepsilon$-operator}% 1356\index{descriptions!indefinite}% 1357An indefinite description is traditionally written $\varepsilon x. P(x)$ and is 1358known as Hilbert's $\varepsilon$-operator. It denotes 1359some $x$ such that $P(x)$ is true, provided one exists. 1360Isabelle uses \sdx{SOME} for the Greek letter~$\varepsilon$. 1361 1362Here is the definition of~\cdx{inv},\footnote{In fact, \isa{inv} is defined via a second constant \isa{inv_into}, which we ignore here.} which expresses inverses of 1363functions: 1364\begin{isabelle} 1365inv\ f\ \isasymequiv \ \isasymlambda y.\ SOME\ x.\ f\ x\ =\ y% 1366\rulename{inv_def} 1367\end{isabelle} 1368Using \isa{SOME} rather than \isa{THE} makes \isa{inv~f} behave well 1369even if \isa{f} is not injective. As it happens, most useful theorems about 1370\isa{inv} do assume the function to be injective. 1371 1372The inverse of \isa{f}, when applied to \isa{y}, returns some~\isa{x} such that 1373\isa{f~x~=~y}. For example, we can prove \isa{inv~Suc} really is the inverse 1374of the \isa{Suc} function 1375\begin{isabelle} 1376\isacommand{lemma}\ "inv\ Suc\ (Suc\ n)\ =\ n"\isanewline 1377\isacommand{by}\ (simp\ add:\ inv_def) 1378\end{isabelle} 1379 1380\noindent 1381The proof is a one-liner: the subgoal simplifies to a degenerate application of 1382\isa{SOME}, which is then erased. In detail, the left-hand side simplifies 1383to \isa{SOME\ x.\ Suc\ x\ =\ Suc\ n}, then to \isa{SOME\ x.\ x\ =\ n} and 1384finally to~\isa{n}. 1385 1386We know nothing about what 1387\isa{inv~Suc} returns when applied to zero. The proof above still treats 1388\isa{SOME} as a definite description, since it only reasons about 1389situations in which the value is described uniquely. Indeed, \isa{SOME} 1390satisfies this rule: 1391\begin{isabelle} 1392\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ x\ =\ a\isasymrbrakk \ 1393\isasymLongrightarrow \ (SOME\ x.\ P\ x)\ =\ a% 1394\rulenamedx{some_equality} 1395\end{isabelle} 1396To go further is 1397tricky and requires rules such as these: 1398\begin{isabelle} 1399P\ x\ \isasymLongrightarrow \ P\ (SOME\ x.\ P\ x) 1400\rulenamedx{someI}\isanewline 1401\isasymlbrakk P\ a;\ \isasymAnd x.\ P\ x\ \isasymLongrightarrow \ Q\ 1402x\isasymrbrakk \ \isasymLongrightarrow \ Q\ (SOME\ x.\ P\ x) 1403\rulenamedx{someI2} 1404\end{isabelle} 1405Rule \isa{someI} is basic: if anything satisfies \isa{P} then so does 1406\hbox{\isa{SOME\ x.\ P\ x}}. The repetition of~\isa{P} in the conclusion makes it 1407difficult to apply in a backward proof, so the derived rule \isa{someI2} is 1408also provided. 1409 1410\medskip 1411For example, let us prove the \rmindex{axiom of choice}: 1412\begin{isabelle} 1413\isacommand{theorem}\ axiom_of_choice: 1414\ "(\isasymforall x.\ \isasymexists y.\ P\ x\ y)\ \isasymLongrightarrow \ 1415\isasymexists f.\ \isasymforall x.\ P\ x\ (f\ x)"\isanewline 1416\isacommand{apply}\ (rule\ exI,\ rule\ allI)\isanewline 1417 1418\ 1.\ \isasymAnd x.\ \isasymforall x.\ \isasymexists y.\ P\ x\ y\ 1419\isasymLongrightarrow \ P\ x\ (?f\ x) 1420\end{isabelle} 1421% 1422We have applied the introduction rules; now it is time to apply the elimination 1423rules. 1424 1425\begin{isabelle} 1426\isacommand{apply}\ (drule\ spec,\ erule\ exE)\isanewline 1427 1428\ 1.\ \isasymAnd x\ y.\ P\ (?x2\ x)\ y\ \isasymLongrightarrow \ P\ x\ (?f\ x) 1429\end{isabelle} 1430 1431\noindent 1432The rule \isa{someI} automatically instantiates 1433\isa{f} to \hbox{\isa{\isasymlambda x.\ SOME y.\ P\ x\ y}}, which is the choice 1434function. It also instantiates \isa{?x2\ x} to \isa{x}. 1435\begin{isabelle} 1436\isacommand{by}\ (rule\ someI)\isanewline 1437\end{isabelle} 1438 1439\subsubsection{Historical Note} 1440The original purpose of Hilbert's $\varepsilon$-operator was to express an 1441existential destruction rule: 1442\[ \infer{P[(\varepsilon x. P) / \, x]}{\exists x.\,P} \] 1443This rule is seldom used for that purpose --- it can cause exponential 1444blow-up --- but it is occasionally used as an introduction rule 1445for the~$\varepsilon$-operator. Its name in HOL is \tdxbold{someI_ex}.%% 1446\index{description operators|)} 1447 1448 1449\section{Some Proofs That Fail} 1450 1451\index{proofs!examples of failing|(}% 1452Most of the examples in this tutorial involve proving theorems. But not every 1453conjecture is true, and it can be instructive to see how 1454proofs fail. Here we attempt to prove a distributive law involving 1455the existential quantifier and conjunction. 1456\begin{isabelle} 1457\isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ 1458({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ 1459\isasymand\ Q\ x" 1460\end{isabelle} 1461The first steps are routine. We apply conjunction elimination to break 1462the assumption into two existentially quantified assumptions. 1463Applying existential elimination removes one of the quantifiers. 1464\begin{isabelle} 1465\isacommand{apply}\ (erule\ conjE)\isanewline 1466\isacommand{apply}\ (erule\ exE)\isanewline 1467\ 1.\ \isasymAnd x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x 1468\end{isabelle} 1469% 1470When we remove the other quantifier, we get a different bound 1471variable in the subgoal. (The name \isa{xa} is generated automatically.) 1472\begin{isabelle} 1473\isacommand{apply}\ (erule\ exE)\isanewline 1474\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ 1475\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x 1476\end{isabelle} 1477The proviso of the existential elimination rule has forced the variables to 1478differ: we can hardly expect two arbitrary values to be equal! There is 1479no way to prove this subgoal. Removing the 1480conclusion's existential quantifier yields two 1481identical placeholders, which can become any term involving the variables \isa{x} 1482and~\isa{xa}. We need one to become \isa{x} 1483and the other to become~\isa{xa}, but Isabelle requires all instances of a 1484placeholder to be identical. 1485\begin{isabelle} 1486\isacommand{apply}\ (rule\ exI)\isanewline 1487\isacommand{apply}\ (rule\ conjI)\isanewline 1488\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ 1489\isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline 1490\ 2.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa) 1491\end{isabelle} 1492We can prove either subgoal 1493using the \isa{assumption} method. If we prove the first one, the placeholder 1494changes into~\isa{x}. 1495\begin{isabelle} 1496\ \isacommand{apply}\ assumption\isanewline 1497\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk P\ x;\ Q\ xa\isasymrbrakk\ 1498\isasymLongrightarrow\ Q\ x 1499\end{isabelle} 1500We are left with a subgoal that cannot be proved. Applying the \isa{assumption} 1501method results in an error message: 1502\begin{isabelle} 1503*** empty result sequence -- proof command failed 1504\end{isabelle} 1505When interacting with Isabelle via the shell interface, 1506you can abandon a proof using the \isacommand{oops} command. 1507 1508\medskip 1509 1510Here is another abortive proof, illustrating the interaction between 1511bound variables and unknowns. 1512If $R$ is a reflexive relation, 1513is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when 1514we attempt to prove it. 1515\begin{isabelle} 1516\isacommand{lemma}\ "\isasymforall y.\ R\ y\ y\ \isasymLongrightarrow 1517\ \isasymexists x.\ \isasymforall y.\ R\ x\ y" 1518\end{isabelle} 1519First, we remove the existential quantifier. The new proof state has an 1520unknown, namely~\isa{?x}. 1521\begin{isabelle} 1522\isacommand{apply}\ (rule\ exI)\isanewline 1523\ 1.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ \isasymforall y.\ R\ ?x\ y% 1524\end{isabelle} 1525It looks like we can just apply \isa{assumption}, but it fails. Isabelle 1526refuses to substitute \isa{y}, a bound variable, for~\isa{?x}; that would be 1527a bound variable capture. We can still try to finish the proof in some 1528other way. We remove the universal quantifier from the conclusion, moving 1529the bound variable~\isa{y} into the subgoal. But note that it is still 1530bound! 1531\begin{isabelle} 1532\isacommand{apply}\ (rule\ allI)\isanewline 1533\ 1.\ \isasymAnd y.\ \isasymforall y.\ R\ y\ y\ \isasymLongrightarrow \ R\ ?x\ y% 1534\end{isabelle} 1535Finally, we try to apply our reflexivity assumption. We obtain a 1536new assumption whose identical placeholders may be replaced by 1537any term involving~\isa{y}. 1538\begin{isabelle} 1539\isacommand{apply}\ (drule\ spec)\isanewline 1540\ 1.\ \isasymAnd y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y 1541\end{isabelle} 1542This subgoal can only be proved by putting \isa{y} for all the placeholders, 1543making the assumption and conclusion become \isa{R\ y\ y}. Isabelle can 1544replace \isa{?z2~y} by \isa{y}; this involves instantiating 1545\isa{?z2} to the identity function. But, just as two steps earlier, 1546Isabelle refuses to substitute~\isa{y} for~\isa{?x}. 1547This example is typical of how Isabelle enforces sound quantifier reasoning. 1548\index{proofs!examples of failing|)} 1549 1550\section{Proving Theorems Using the {\tt\slshape blast} Method} 1551 1552\index{*blast (method)|(}% 1553It is hard to prove many theorems using the methods 1554described above. A proof may be hundreds of steps long. You 1555may need to search among different ways of proving certain 1556subgoals. Often a choice that proves one subgoal renders another 1557impossible to prove. There are further complications that we have not 1558discussed, concerning negation and disjunction. Isabelle's 1559\textbf{classical reasoner} is a family of tools that perform such 1560proofs automatically. The most important of these is the 1561\isa{blast} method. 1562 1563In this section, we shall first see how to use the classical 1564reasoner in its default mode and then how to insert additional 1565rules, enabling it to work in new problem domains. 1566 1567 We begin with examples from pure predicate logic. The following 1568example is known as Andrew's challenge. Peter Andrews designed 1569it to be hard to prove by automatic means. 1570It is particularly hard for a resolution prover, where 1571converting the nested biconditionals to 1572clause form produces a combinatorial 1573explosion~\cite{pelletier86}. However, the 1574\isa{blast} method proves it in a fraction of a second. 1575\begin{isabelle} 1576\isacommand{lemma}\ 1577"(({\isasymexists}x.\ 1578{\isasymforall}y.\ 1579p(x){=}p(y))\ 1580=\ 1581(({\isasymexists}x.\ 1582q(x))=({\isasymforall}y.\ 1583p(y))))\ 1584\ \ =\ \ \ \ \isanewline 1585\ \ \ \ \ \ \ \ 1586(({\isasymexists}x.\ 1587{\isasymforall}y.\ 1588q(x){=}q(y))\ =\ (({\isasymexists}x.\ p(x))=({\isasymforall}y.\ q(y))))"\isanewline 1589\isacommand{by}\ blast 1590\end{isabelle} 1591The next example is a logic problem composed by Lewis Carroll. 1592The \isa{blast} method finds it trivial. Moreover, it turns out 1593that not all of the assumptions are necessary. We can 1594experiment with variations of this formula and see which ones 1595can be proved. 1596\begin{isabelle} 1597\isacommand{lemma}\ 1598"({\isasymforall}x.\ 1599honest(x)\ \isasymand\ 1600industrious(x)\ \isasymlongrightarrow\ 1601healthy(x))\ 1602\isasymand\ \ \isanewline 1603\ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\ 1604grocer(x)\ \isasymand\ 1605healthy(x))\ 1606\isasymand\ \isanewline 1607\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 1608industrious(x)\ \isasymand\ 1609grocer(x)\ \isasymlongrightarrow\ 1610honest(x))\ 1611\isasymand\ \isanewline 1612\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 1613cyclist(x)\ \isasymlongrightarrow\ 1614industrious(x))\ 1615\isasymand\ \isanewline 1616\ \ \ \ \ \ \ \ ({\isasymforall}x.\ 1617{\isasymnot}healthy(x)\ \isasymand\ 1618cyclist(x)\ \isasymlongrightarrow\ 1619{\isasymnot}honest(x))\ 1620\ \isanewline 1621\ \ \ \ \ \ \ \ \isasymlongrightarrow\ 1622({\isasymforall}x.\ 1623grocer(x)\ \isasymlongrightarrow\ 1624{\isasymnot}cyclist(x))"\isanewline 1625\isacommand{by}\ blast 1626\end{isabelle} 1627The \isa{blast} method is also effective for set theory, which is 1628described in the next chapter. The formula below may look horrible, but 1629the \isa{blast} method proves it in milliseconds. 1630\begin{isabelle} 1631\isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline 1632\ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline 1633\isacommand{by}\ blast 1634\end{isabelle} 1635 1636Few subgoals are couched purely in predicate logic and set theory. 1637We can extend the scope of the classical reasoner by giving it new rules. 1638Extending it effectively requires understanding the notions of 1639introduction, elimination and destruction rules. Moreover, there is a 1640distinction between safe and unsafe rules. A 1641\textbf{safe}\indexbold{safe rules} rule is one that can be applied 1642backwards without losing information; an 1643\textbf{unsafe}\indexbold{unsafe rules} rule loses information, perhaps 1644transforming the subgoal into one that cannot be proved. The safe/unsafe 1645distinction affects the proof search: if a proof attempt fails, the 1646classical reasoner backtracks to the most recent unsafe rule application 1647and makes another choice. 1648 1649An important special case avoids all these complications. A logical 1650equivalence, which in higher-order logic is an equality between 1651formulas, can be given to the classical 1652reasoner and simplifier by using the attribute \attrdx{iff}. You 1653should do so if the right hand side of the equivalence is 1654simpler than the left-hand side. 1655 1656For example, here is a simple fact about list concatenation. 1657The result of appending two lists is empty if and only if both 1658of the lists are themselves empty. Obviously, applying this equivalence 1659will result in a simpler goal. When stating this lemma, we include 1660the \attrdx{iff} attribute. Once we have proved the lemma, Isabelle 1661will make it known to the classical reasoner (and to the simplifier). 1662\begin{isabelle} 1663\isacommand{lemma}\ 1664[iff]:\ "(xs{\isacharat}ys\ =\ [])\ =\ 1665(xs=[]\ \isasymand\ ys=[])"\isanewline 1666\isacommand{apply}\ (induct_tac\ xs)\isanewline 1667\isacommand{apply}\ (simp_all)\isanewline 1668\isacommand{done} 1669\end{isabelle} 1670% 1671This fact about multiplication is also appropriate for 1672the \attrdx{iff} attribute: 1673\begin{isabelle} 1674(\mbox{?m}\ *\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) 1675\end{isabelle} 1676A product is zero if and only if one of the factors is zero. The 1677reasoning involves a disjunction. Proving new rules for 1678disjunctive reasoning is hard, but translating to an actual disjunction 1679works: the classical reasoner handles disjunction properly. 1680 1681In more detail, this is how the \attrdx{iff} attribute works. It converts 1682the equivalence $P=Q$ to a pair of rules: the introduction 1683rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the 1684classical reasoner as safe rules, ensuring that all occurrences of $P$ in 1685a subgoal are replaced by~$Q$. The simplifier performs the same 1686replacement, since \isa{iff} gives $P=Q$ to the 1687simplifier. 1688 1689Classical reasoning is different from 1690simplification. Simplification is deterministic. It applies rewrite rules 1691repeatedly, as long as possible, transforming a goal into another goal. Classical 1692reasoning uses search and backtracking in order to prove a goal outright.% 1693\index{*blast (method)|)}% 1694 1695 1696\section{Other Classical Reasoning Methods} 1697 1698The \isa{blast} method is our main workhorse for proving theorems 1699automatically. Other components of the classical reasoner interact 1700with the simplifier. Still others perform classical reasoning 1701to a limited extent, giving the user fine control over the proof. 1702 1703Of the latter methods, the most useful is 1704\methdx{clarify}. 1705It performs 1706all obvious reasoning steps without splitting the goal into multiple 1707parts. It does not apply unsafe rules that could render the 1708goal unprovable. By performing the obvious 1709steps, \isa{clarify} lays bare the difficult parts of the problem, 1710where human intervention is necessary. 1711 1712For example, the following conjecture is false: 1713\begin{isabelle} 1714\isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\ 1715({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\ 1716\isasymand\ Q\ x)"\isanewline 1717\isacommand{apply}\ clarify 1718\end{isabelle} 1719The \isa{blast} method would simply fail, but \isa{clarify} presents 1720a subgoal that helps us see why we cannot continue the proof. 1721\begin{isabelle} 1722\ 1.\ \isasymAnd x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\ 1723xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x 1724\end{isabelle} 1725The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x} 1726refer to distinct bound variables. To reach this state, \isa{clarify} applied 1727the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall} 1728and the elimination rule for \isa{\isasymand}. It did not apply the introduction 1729rule for \isa{\isasymand} because of its policy never to split goals. 1730 1731Also available is \methdx{clarsimp}, a method 1732that interleaves \isa{clarify} and \isa{simp}. Also there is \methdx{safe}, 1733which like \isa{clarify} performs obvious steps but even applies those that 1734split goals. 1735 1736The \methdx{force} method applies the classical 1737reasoner and simplifier to one goal. 1738Unless it can prove the goal, it fails. Contrast 1739that with the \isa{auto} method, which also combines classical reasoning 1740with simplification. The latter's purpose is to prove all the 1741easy subgoals and parts of subgoals. Unfortunately, it can produce 1742large numbers of new subgoals; also, since it proves some subgoals 1743and splits others, it obscures the structure of the proof tree. 1744The \isa{force} method does not have these drawbacks. Another 1745difference: \isa{force} tries harder than {\isa{auto}} to prove 1746its goal, so it can take much longer to terminate. 1747 1748Older components of the classical reasoner have largely been 1749superseded by \isa{blast}, but they still have niche applications. 1750Most important among these are \isa{fast} and \isa{best}. While \isa{blast} 1751searches for proofs using a built-in first-order reasoner, these 1752earlier methods search for proofs using standard Isabelle inference. 1753That makes them slower but enables them to work in the 1754presence of the more unusual features of Isabelle rules, such 1755as type classes and function unknowns. For example, recall the introduction rule 1756for Hilbert's $\varepsilon$-operator: 1757\begin{isabelle} 1758?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x) 1759\rulename{someI} 1760\end{isabelle} 1761% 1762The repeated occurrence of the variable \isa{?P} makes this rule tricky 1763to apply. Consider this contrived example: 1764\begin{isabelle} 1765\isacommand{lemma}\ "\isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\isanewline 1766\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\ 1767\isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline 1768\isacommand{apply}\ (rule\ someI) 1769\end{isabelle} 1770% 1771We can apply rule \isa{someI} explicitly. It yields the 1772following subgoal: 1773\begin{isabelle} 1774\ 1.\ \isasymlbrakk Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\ 1775\isasymand\ Q\ ?x% 1776\end{isabelle} 1777The proof from this point is trivial. Could we have 1778proved the theorem with a single command? Not using \isa{blast}: it 1779cannot perform the higher-order unification needed here. The 1780\methdx{fast} method succeeds: 1781\begin{isabelle} 1782\isacommand{apply}\ (fast\ intro!:\ someI) 1783\end{isabelle} 1784 1785The \methdx{best} method is similar to 1786\isa{fast} but it uses a best-first search instead of depth-first search. 1787Accordingly, it is slower but is less susceptible to divergence. 1788Transitivity rules usually cause \isa{fast} to loop where \isa{best} 1789can often manage. 1790 1791Here is a summary of the classical reasoning methods: 1792\begin{itemize} 1793\item \methdx{blast} works automatically and is the fastest 1794 1795\item \methdx{clarify} and \methdx{clarsimp} perform obvious steps without 1796splitting the goal; \methdx{safe} even splits goals 1797 1798\item \methdx{force} uses classical reasoning and simplification to prove a goal; 1799 \methdx{auto} is similar but leaves what it cannot prove 1800 1801\item \methdx{fast} and \methdx{best} are legacy methods that work well with rules 1802involving unusual features 1803\end{itemize} 1804A table illustrates the relationships among four of these methods. 1805\begin{center} 1806\begin{tabular}{r|l|l|} 1807 & no split & split \\ \hline 1808 no simp & \methdx{clarify} & \methdx{safe} \\ \hline 1809 simp & \methdx{clarsimp} & \methdx{auto} \\ \hline 1810\end{tabular} 1811\end{center} 1812 1813\section{Finding More Theorems} 1814\label{sec:find2} 1815\input{find2.tex} 1816 1817 1818\section{Forward Proof: Transforming Theorems}\label{sec:forward} 1819 1820\index{forward proof|(}% 1821Forward proof means deriving new facts from old ones. It is the 1822most fundamental type of proof. Backward proof, by working from goals to 1823subgoals, can help us find a difficult proof. But it is 1824not always the best way of presenting the proof thus found. Forward 1825proof is particularly good for reasoning from the general 1826to the specific. For example, consider this distributive law for 1827the greatest common divisor: 1828\[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\] 1829 1830Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$) 1831\[ k = \gcd(k,k\times n)\] 1832We have derived a new fact; if re-oriented, it might be 1833useful for simplification. After re-orienting it and putting $n=1$, we 1834derive another useful law: 1835\[ \gcd(k,k)=k \] 1836Substituting values for variables --- instantiation --- is a forward step. 1837Re-orientation works by applying the symmetry of equality to 1838an equation, so it too is a forward step. 1839 1840\subsection{Modifying a Theorem using {\tt\slshape of}, {\tt\slshape where} 1841 and {\tt\slshape THEN}} 1842 1843\label{sec:THEN} 1844 1845Let us reproduce our examples in Isabelle. Recall that in 1846{\S}\ref{sec:fun-simplification} we declared the recursive function 1847\isa{gcd}:\index{*gcd (constant)|(} 1848\begin{isabelle} 1849\isacommand{fun}\ gcd\ ::\ "nat\ \isasymRightarrow \ nat\ \isasymRightarrow \ nat"\ \isakeyword{where}\isanewline 1850\ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))" 1851\end{isabelle} 1852% 1853From this definition, it is possible to prove the distributive law. 1854That takes us to the starting point for our example. 1855\begin{isabelle} 1856?k\ *\ gcd\ ?m\ ?n\ =\ gcd\ (?k\ *\ ?m)\ (?k\ *\ ?n) 1857\rulename{gcd_mult_distrib2} 1858\end{isabelle} 1859% 1860The first step in our derivation is to replace \isa{?m} by~1. We instantiate the 1861theorem using~\attrdx{of}, which identifies variables in order of their 1862appearance from left to right. In this case, the variables are \isa{?k}, \isa{?m} 1863and~\isa{?n}. So, the expression 1864\hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m} 1865by~\isa{1}. 1866\begin{isabelle} 1867\isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1] 1868\end{isabelle} 1869% 1870The keyword \commdx{lemmas} declares a new theorem, which can be derived 1871from an existing one using attributes such as \isa{[of~k~1]}. 1872The command 1873\isa{thm gcd_mult_0} 1874displays the result: 1875\begin{isabelle} 1876\ \ \ \ \ k\ *\ gcd\ 1\ ?n\ =\ gcd\ (k\ *\ 1)\ (k\ *\ ?n) 1877\end{isabelle} 1878Something is odd: \isa{k} is an ordinary variable, while \isa{?n} 1879is schematic. We did not specify an instantiation 1880for \isa{?n}. In its present form, the theorem does not allow 1881substitution for \isa{k}. One solution is to avoid giving an instantiation for 1882\isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example, 1883\begin{isabelle} 1884\ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1] 1885\end{isabelle} 1886replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged. 1887 1888An equivalent solution is to use the attribute \isa{where}. 1889\begin{isabelle} 1890\ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1] 1891\end{isabelle} 1892While \isa{of} refers to 1893variables by their position, \isa{where} refers to variables by name. Multiple 1894instantiations are separated by~\isa{and}, as in this example: 1895\begin{isabelle} 1896\ \ \ \ \ gcd\_mult\_distrib2\ [where\ m=1\ and\ k=1] 1897\end{isabelle} 1898 1899We now continue the present example with the version of \isa{gcd_mult_0} 1900shown above, which has \isa{k} instead of \isa{?k}. 1901Once we have replaced \isa{?m} by~1, we must next simplify 1902the theorem \isa{gcd_mult_0}, performing the steps 1903$\gcd(1,n)=1$ and $k\times1=k$. The \attrdx{simplified} 1904attribute takes a theorem 1905and returns the result of simplifying it, with respect to the default 1906simplification rules: 1907\begin{isabelle} 1908\isacommand{lemmas}\ gcd_mult_1\ =\ gcd_mult_0\ 1909[simplified]% 1910\end{isabelle} 1911% 1912Again, we display the resulting theorem: 1913\begin{isabelle} 1914\ \ \ \ \ k\ =\ gcd\ k\ (k\ *\ ?n) 1915\end{isabelle} 1916% 1917To re-orient the equation requires the symmetry rule: 1918\begin{isabelle} 1919?s\ =\ ?t\ 1920\isasymLongrightarrow\ ?t\ =\ 1921?s% 1922\rulenamedx{sym} 1923\end{isabelle} 1924The following declaration gives our equation to \isa{sym}: 1925\begin{isabelle} 1926\ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ [THEN\ sym] 1927\end{isabelle} 1928% 1929Here is the result: 1930\begin{isabelle} 1931\ \ \ \ \ gcd\ k\ (k\ *\ ?n)\ =\ k% 1932\end{isabelle} 1933\isa{THEN~sym}\indexbold{*THEN (attribute)} gives the current theorem to the 1934rule \isa{sym} and returns the resulting conclusion. The effect is to 1935exchange the two operands of the equality. Typically \isa{THEN} is used 1936with destruction rules. Also useful is \isa{THEN~spec}, which removes the 1937quantifier from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, 1938which converts the implication $P\imp Q$ into the rule 1939$\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules, 1940which extract the two directions of reasoning about a boolean equivalence: 1941\begin{isabelle} 1942\isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 1943\rulenamedx{iffD1}% 1944\isanewline 1945\isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% 1946\rulenamedx{iffD2} 1947\end{isabelle} 1948% 1949Normally we would never name the intermediate theorems 1950such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine 1951the three forward steps: 1952\begin{isabelle} 1953\isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]% 1954\end{isabelle} 1955The directives, or attributes, are processed from left to right. This 1956declaration of \isa{gcd_mult} is equivalent to the 1957previous one. 1958 1959Such declarations can make the proof script hard to read. Better 1960is to state the new lemma explicitly and to prove it using a single 1961\isa{rule} method whose operand is expressed using forward reasoning: 1962\begin{isabelle} 1963\isacommand{lemma}\ gcd\_mult\ [simp]:\ "gcd\ k\ (k*n)\ =\ k"\isanewline 1964\isacommand{by}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]) 1965\end{isabelle} 1966Compared with the previous proof of \isa{gcd_mult}, this 1967version shows the reader what has been proved. Also, the result will be processed 1968in the normal way. In particular, Isabelle generalizes over all variables: the 1969resulting theorem will have {\isa{?k}} instead of {\isa{k}}. 1970 1971At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here 1972is the Isabelle version:\index{*gcd (constant)|)} 1973\begin{isabelle} 1974\isacommand{lemma}\ gcd\_self\ [simp]:\ "gcd\ k\ k\ =\ k"\isanewline 1975\isacommand{by}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified]) 1976\end{isabelle} 1977 1978\begin{warn} 1979To give~\isa{of} a nonatomic term, enclose it in quotation marks, as in 1980\isa{[of "k*m"]}. The term must not contain unknowns: an 1981attribute such as 1982\isa{[of "?k*m"]} will be rejected. 1983\end{warn} 1984 1985%Answer is now included in that section! Is a modified version of this 1986% exercise worth including? E.g. find a difference between the two ways 1987% of substituting. 1988%\begin{exercise} 1989%In {\S}\ref{sec:subst} the method \isa{subst\ mult.commute} was applied. How 1990%can we achieve the same effect using \isa{THEN} with the rule \isa{ssubst}? 1991%% answer rule (mult.commute [THEN ssubst]) 1992%\end{exercise} 1993 1994\subsection{Modifying a Theorem using {\tt\slshape OF}} 1995 1996\index{*OF (attribute)|(}% 1997Recall that \isa{of} generates an instance of a 1998rule by specifying values for its variables. Analogous is \isa{OF}, which 1999generates an instance of a rule by specifying facts for its premises. 2000 2001We again need the divides relation\index{divides relation} of number theory, which 2002as we recall is defined by 2003\begin{isabelle} 2004?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ *\ k 2005\rulename{dvd_def} 2006\end{isabelle} 2007% 2008Suppose, for example, that we have proved the following rule. 2009It states that if $k$ and $n$ are relatively prime 2010and if $k$ divides $m\times n$ then $k$ divides $m$. 2011\begin{isabelle} 2012\isasymlbrakk gcd ?k ?n {=} 1;\ ?k\ dvd\ ?m * ?n\isasymrbrakk\ 2013\isasymLongrightarrow\ ?k\ dvd\ ?m 2014\rulename{relprime_dvd_mult} 2015\end{isabelle} 2016We can use \isa{OF} to create an instance of this rule. 2017First, we 2018prove an instance of its first premise: 2019\begin{isabelle} 2020\isacommand{lemma}\ relprime\_20\_81:\ "gcd\ 20\ 81\ =\ 1"\isanewline 2021\isacommand{by}\ (simp\ add:\ gcd.simps) 2022\end{isabelle} 2023We have evaluated an application of the \isa{gcd} function by 2024simplification. Expression evaluation involving recursive functions is not 2025guaranteed to terminate, and it can be slow; Isabelle 2026performs arithmetic by rewriting symbolic bit strings. Here, 2027however, the simplification takes less than one second. We can 2028give this new lemma to \isa{OF}. The expression 2029\begin{isabelle} 2030\ \ \ \ \ relprime_dvd_mult [OF relprime_20_81] 2031\end{isabelle} 2032yields the theorem 2033\begin{isabelle} 2034\ \ \ \ \ 20\ dvd\ (?m\ *\ 81)\ \isasymLongrightarrow\ 20\ dvd\ ?m% 2035\end{isabelle} 2036% 2037\isa{OF} takes any number of operands. Consider 2038the following facts about the divides relation: 2039\begin{isabelle} 2040\isasymlbrakk?k\ dvd\ ?m;\ 2041?k\ dvd\ ?n\isasymrbrakk\ 2042\isasymLongrightarrow\ ?k\ dvd\ 2043?m\ +\ ?n 2044\rulename{dvd_add}\isanewline 2045?m\ dvd\ ?m% 2046\rulename{dvd_refl} 2047\end{isabelle} 2048Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}: 2049\begin{isabelle} 2050\ \ \ \ \ dvd_add [OF dvd_refl dvd_refl] 2051\end{isabelle} 2052Here is the theorem that we have expressed: 2053\begin{isabelle} 2054\ \ \ \ \ ?k\ dvd\ (?k\ +\ ?k) 2055\end{isabelle} 2056As with \isa{of}, we can use the \isa{_} symbol to leave some positions 2057unspecified: 2058\begin{isabelle} 2059\ \ \ \ \ dvd_add [OF _ dvd_refl] 2060\end{isabelle} 2061The result is 2062\begin{isabelle} 2063\ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ ?m\ +\ ?k 2064\end{isabelle} 2065 2066You may have noticed that \isa{THEN} and \isa{OF} are based on 2067the same idea, namely to combine two rules. They differ in the 2068order of the combination and thus in their effect. We use \isa{THEN} 2069typically with a destruction rule to extract a subformula of the current 2070theorem. We use \isa{OF} with a list of facts to generate an instance of 2071the current theorem.% 2072\index{*OF (attribute)|)} 2073 2074Here is a summary of some primitives for forward reasoning: 2075\begin{itemize} 2076\item \attrdx{of} instantiates the variables of a rule to a list of terms 2077\item \attrdx{OF} applies a rule to a list of theorems 2078\item \attrdx{THEN} gives a theorem to a named rule and returns the 2079conclusion 2080%\item \attrdx{rule_format} puts a theorem into standard form 2081% by removing \isa{\isasymlongrightarrow} and~\isa{\isasymforall} 2082\item \attrdx{simplified} applies the simplifier to a theorem 2083\item \isacommand{lemmas} assigns a name to the theorem produced by the 2084attributes above 2085\end{itemize} 2086 2087 2088\section{Forward Reasoning in a Backward Proof} 2089 2090We have seen that the forward proof directives work well within a backward 2091proof. There are many ways to achieve a forward style using our existing 2092proof methods. We shall also meet some new methods that perform forward 2093reasoning. 2094 2095The methods \isa{drule}, \isa{frule}, \isa{drule_tac}, etc., 2096reason forward from a subgoal. We have seen them already, using rules such as 2097\isa{mp} and 2098\isa{spec} to operate on formulae. They can also operate on terms, using rules 2099such as these: 2100\begin{isabelle} 2101x\ =\ y\ \isasymLongrightarrow \ f\ x\ =\ f\ y% 2102\rulenamedx{arg_cong}\isanewline 2103i\ \isasymle \ j\ \isasymLongrightarrow \ i\ *\ k\ \isasymle \ j\ *\ k% 2104\rulename{mult_le_mono1} 2105\end{isabelle} 2106 2107For example, let us prove a fact about divisibility in the natural numbers: 2108\begin{isabelle} 2109\isacommand{lemma}\ "2\ \isasymle \ u\ \isasymLongrightarrow \ u*m\ \isasymnoteq 2110\ Suc(u*n)"\isanewline 2111\isacommand{apply}\ (intro\ notI)\isanewline 2112\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ =\ Suc\ (u\ *\ n)\isasymrbrakk \ \isasymLongrightarrow \ False% 2113\end{isabelle} 2114% 2115The key step is to apply the function \ldots\isa{mod\ u} to both sides of the 2116equation 2117\isa{u*m\ =\ Suc(u*n)}:\index{*drule_tac (method)} 2118\begin{isabelle} 2119\isacommand{apply}\ (drule_tac\ f="\isasymlambda x.\ x\ mod\ u"\ \isakeyword{in}\ 2120arg_cong)\isanewline 2121\ 1.\ \isasymlbrakk 2\ \isasymle \ u;\ u\ *\ m\ mod\ u\ =\ Suc\ (u\ *\ n)\ mod\ 2122u\isasymrbrakk \ \isasymLongrightarrow \ False 2123\end{isabelle} 2124% 2125Simplification reduces the left side to 0 and the right side to~1, yielding the 2126required contradiction. 2127\begin{isabelle} 2128\isacommand{apply}\ (simp\ add:\ mod_Suc)\isanewline 2129\isacommand{done} 2130\end{isabelle} 2131 2132Our proof has used a fact about remainder: 2133\begin{isabelle} 2134Suc\ m\ mod\ n\ =\isanewline 2135(if\ Suc\ (m\ mod\ n)\ =\ n\ then\ 0\ else\ Suc\ (m\ mod\ n)) 2136\rulename{mod_Suc} 2137\end{isabelle} 2138 2139\subsection{The Method {\tt\slshape insert}} 2140 2141\index{*insert (method)|(}% 2142The \isa{insert} method 2143inserts a given theorem as a new assumption of all subgoals. This 2144already is a forward step; moreover, we may (as always when using a 2145theorem) apply 2146\isa{of}, \isa{THEN} and other directives. The new assumption can then 2147be used to help prove the subgoals. 2148 2149For example, consider this theorem about the divides relation. The first 2150proof step inserts the distributive law for 2151\isa{gcd}. We specify its variables as shown. 2152\begin{isabelle} 2153\isacommand{lemma}\ relprime\_dvd\_mult:\ \isanewline 2154\ \ \ \ \ \ "\isasymlbrakk \ gcd\ k\ n\ =\ 1;\ k\ dvd\ m*n\ \isasymrbrakk \ \isasymLongrightarrow \ k\ dvd\ m"\isanewline 2155\isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ n]) 2156\end{isabelle} 2157In the resulting subgoal, note how the equation has been 2158inserted: 2159\begin{isabelle} 2160\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ 1;\ k\ dvd\ m\ *\ n;\ m\ *\ gcd\ k\ n\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline 2161\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m% 2162\end{isabelle} 2163The next proof step utilizes the assumption \isa{gcd\ k\ n\ =\ 1} 2164(note that \isa{Suc\ 0} is another expression for 1): 2165\begin{isabelle} 2166\isacommand{apply}(simp)\isanewline 2167\ 1.\ \isasymlbrakk gcd\ k\ n\ =\ Suc\ 0;\ k\ dvd\ m\ *\ n;\ m\ =\ gcd\ (m\ *\ k)\ (m\ *\ n)\isasymrbrakk \isanewline 2168\isaindent{\ 1.\ }\isasymLongrightarrow \ k\ dvd\ m% 2169\end{isabelle} 2170Simplification has yielded an equation for~\isa{m}. The rest of the proof 2171is omitted. 2172 2173\medskip 2174Here is another demonstration of \isa{insert}. Division and 2175remainder obey a well-known law: 2176\begin{isabelle} 2177(?m\ div\ ?n)\ *\ ?n\ +\ ?m\ mod\ ?n\ =\ ?m 2178\rulename{div_mult_mod_eq} 2179\end{isabelle} 2180 2181We refer to this law explicitly in the following proof: 2182\begin{isabelle} 2183\isacommand{lemma}\ div_mult_self_is_m:\ \isanewline 2184\ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m*n)\ div\ n\ =\ 2185(m::nat)"\isanewline 2186\isacommand{apply}\ (insert\ div_mult_mod_eq\ [of\ "m*n"\ n])\isanewline 2187\isacommand{apply}\ (simp)\isanewline 2188\isacommand{done} 2189\end{isabelle} 2190The first step inserts the law, specifying \isa{m*n} and 2191\isa{n} for its variables. Notice that non-trivial expressions must be 2192enclosed in quotation marks. Here is the resulting 2193subgoal, with its new assumption: 2194\begin{isabelle} 2195%0\ \isacharless\ n\ \isasymLongrightarrow\ (m\ 2196%*\ n)\ div\ n\ =\ m\isanewline 2197\ 1.\ \isasymlbrakk0\ \isacharless\ 2198n;\ \ (m\ *\ n)\ div\ n\ *\ n\ +\ (m\ *\ n)\ mod\ n\ 2199=\ m\ *\ n\isasymrbrakk\isanewline 2200\ \ \ \ \isasymLongrightarrow\ (m\ *\ n)\ div\ n\ 2201=\ m 2202\end{isabelle} 2203Simplification reduces \isa{(m\ *\ n)\ mod\ n} to zero. 2204Then it cancels the factor~\isa{n} on both 2205sides of the equation \isa{(m\ *\ n)\ div\ n\ *\ n\ =\ m\ *\ n}, proving the 2206theorem. 2207 2208\begin{warn} 2209Any unknowns in the theorem given to \methdx{insert} will be universally 2210quantified in the new assumption. 2211\end{warn}% 2212\index{*insert (method)|)} 2213 2214\subsection{The Method {\tt\slshape subgoal_tac}} 2215 2216\index{*subgoal_tac (method)}% 2217A related method is \isa{subgoal_tac}, but instead 2218of inserting a theorem as an assumption, it inserts an arbitrary formula. 2219This formula must be proved later as a separate subgoal. The 2220idea is to claim that the formula holds on the basis of the current 2221assumptions, to use this claim to complete the proof, and finally 2222to justify the claim. It gives the proof 2223some structure. If you find yourself generating a complex assumption by a 2224long series of forward steps, consider using \isa{subgoal_tac} instead: you can 2225state the formula you are aiming for, and perhaps prove it automatically. 2226 2227Look at the following example. 2228\begin{isabelle} 2229\isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ 37;\ 66\ <\ 2*z;\ z*z\ 2230\isasymnoteq\ 1225;\ Q(34);\ Q(36)\isasymrbrakk\isanewline 2231\ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline 2232\isacommand{apply}\ (subgoal_tac\ "z\ =\ 34\ \isasymor\ z\ =\ 223336")\isanewline 2234\isacommand{apply}\ blast\isanewline 2235\isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ 35")\isanewline 2236\isacommand{apply}\ arith\isanewline 2237\isacommand{apply}\ force\isanewline 2238\isacommand{done} 2239\end{isabelle} 2240The first assumption tells us 2241that \isa{z} is no greater than~36. The second tells us that \isa{z} 2242is at least~34. The third assumption tells us that \isa{z} cannot be 35, since 2243$35\times35=1225$. So \isa{z} is either 34 or~36, and since \isa{Q} holds for 2244both of those values, we have the conclusion. 2245 2246The Isabelle proof closely follows this reasoning. The first 2247step is to claim that \isa{z} is either 34 or 36. The resulting proof 2248state gives us two subgoals: 2249\begin{isabelle} 2250%\isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ 2251%Q\ 34;\ Q\ 36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline 2252\ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36;\isanewline 2253\ \ \ \ \ z\ =\ 34\ \isasymor\ z\ =\ 36\isasymrbrakk\isanewline 2254\ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline 2255\ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline 2256\ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36 2257\end{isabelle} 2258The first subgoal is trivial (\isa{blast}), but for the second Isabelle needs help to eliminate 2259the case 2260\isa{z}=35. The second invocation of {\isa{subgoal_tac}} leaves two 2261subgoals: 2262\begin{isabelle} 2263\ 1.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 22641225;\ Q\ 34;\ Q\ 36;\isanewline 2265\ \ \ \ \ z\ \isasymnoteq\ 35\isasymrbrakk\isanewline 2266\ \ \ \ \isasymLongrightarrow\ z\ =\ 34\ \isasymor\ z\ =\ 36\isanewline 2267\ 2.\ \isasymlbrakk z\ <\ 37;\ 66\ <\ 2\ *\ z;\ z\ *\ z\ \isasymnoteq\ 1225;\ Q\ 34;\ Q\ 36\isasymrbrakk\isanewline 2268\ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ 35 2269\end{isabelle} 2270 2271Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic 2272(\isa{arith}). For the second subgoal we apply the method \isa{force}, 2273which proceeds by assuming that \isa{z}=35 and arriving at a contradiction. 2274 2275 2276\medskip 2277Summary of these methods: 2278\begin{itemize} 2279\item \methdx{insert} adds a theorem as a new assumption 2280\item \methdx{subgoal_tac} adds a formula as a new assumption and leaves the 2281subgoal of proving that formula 2282\end{itemize} 2283\index{forward proof|)} 2284 2285 2286\section{Managing Large Proofs} 2287 2288Naturally you should try to divide proofs into manageable parts. Look for lemmas 2289that can be proved separately. Sometimes you will observe that they are 2290instances of much simpler facts. On other occasions, no lemmas suggest themselves 2291and you are forced to cope with a long proof involving many subgoals. 2292 2293\subsection{Tacticals, or Control Structures} 2294 2295\index{tacticals|(}% 2296If the proof is long, perhaps it at least has some regularity. Then you can 2297express it more concisely using \textbf{tacticals}, which provide control 2298structures. Here is a proof (it would be a one-liner using 2299\isa{blast}, but forget that) that contains a series of repeated 2300commands: 2301% 2302\begin{isabelle} 2303\isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\ 2304Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \ 2305\isasymLongrightarrow \ S"\isanewline 2306\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline 2307\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline 2308\isacommand{apply}\ (drule\ mp,\ assumption)\isanewline 2309\isacommand{apply}\ (assumption)\isanewline 2310\isacommand{done} 2311\end{isabelle} 2312% 2313Each of the three identical commands finds an implication and proves its 2314antecedent by assumption. The first one finds \isa{P\isasymlongrightarrow Q} and 2315\isa{P}, concluding~\isa{Q}; the second one concludes~\isa{R} and the third one 2316concludes~\isa{S}. The final step matches the assumption \isa{S} with the goal to 2317be proved. 2318 2319Suffixing a method with a plus sign~(\isa+)\index{*"+ (tactical)} 2320expresses one or more repetitions: 2321\begin{isabelle} 2322\isacommand{lemma}\ "\isasymlbrakk P\isasymlongrightarrow Q;\ Q\isasymlongrightarrow R;\ R\isasymlongrightarrow S;\ P\isasymrbrakk \ \isasymLongrightarrow \ S"\isanewline 2323\isacommand{by}\ (drule\ mp,\ assumption)+ 2324\end{isabelle} 2325% 2326Using \isacommand{by} takes care of the final use of \isa{assumption}. The new 2327proof is more concise. It is also more general: the repetitive method works 2328for a chain of implications having any length, not just three. 2329 2330Choice is another control structure. Separating two methods by a vertical 2331% we must use ?? rather than "| as the sorting item because somehow the presence 2332% of | (even quoted) stops hyperref from putting |hyperpage at the end of the index 2333% entry. 2334bar~(\isa|)\index{??@\texttt{"|} (tactical)} gives the effect of applying the 2335first method, and if that fails, trying the second. It can be combined with 2336repetition, when the choice must be made over and over again. Here is a chain of 2337implications in which most of the antecedents are proved by assumption, but one is 2338proved by arithmetic: 2339\begin{isabelle} 2340\isacommand{lemma}\ "\isasymlbrakk Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ x<5\isasymlongrightarrow P;\ 2341Suc\ x\ <\ 5\isasymrbrakk \ \isasymLongrightarrow \ R"\ \isanewline 2342\isacommand{by}\ (drule\ mp,\ (assumption|arith))+ 2343\end{isabelle} 2344The \isa{arith} 2345method can prove $x<5$ from $x+1<5$, but it cannot duplicate the effect of 2346\isa{assumption}. Therefore, we combine these methods using the choice 2347operator. 2348 2349A postfixed question mark~(\isa?)\index{*"? (tactical)} expresses zero or one 2350repetitions of a method. It can also be viewed as the choice between executing a 2351method and doing nothing. It is useless at top level but can be valuable 2352within other control structures; for example, 2353\isa{($m$+)?} performs zero or more repetitions of method~$m$.% 2354\index{tacticals|)} 2355 2356 2357\subsection{Subgoal Numbering} 2358 2359Another problem in large proofs is contending with huge 2360subgoals or many subgoals. Induction can produce a proof state that looks 2361like this: 2362\begin{isabelle} 2363\ 1.\ bigsubgoal1\isanewline 2364\ 2.\ bigsubgoal2\isanewline 2365\ 3.\ bigsubgoal3\isanewline 2366\ 4.\ bigsubgoal4\isanewline 2367\ 5.\ bigsubgoal5\isanewline 2368\ 6.\ bigsubgoal6 2369\end{isabelle} 2370If each \isa{bigsubgoal} is 15 lines or so, the proof state will be too big to 2371scroll through. By default, Isabelle displays at most 10 subgoals. The 2372\commdx{pr} command lets you change this limit: 2373\begin{isabelle} 2374\isacommand{pr}\ 2\isanewline 2375\ 1.\ bigsubgoal1\isanewline 2376\ 2.\ bigsubgoal2\isanewline 2377A total of 6 subgoals... 2378\end{isabelle} 2379 2380\medskip 2381All methods apply to the first subgoal. 2382Sometimes, not only in a large proof, you may want to focus on some other 2383subgoal. Then you should try the commands \isacommand{defer} or \isacommand{prefer}. 2384 2385In the following example, the first subgoal looks hard, while the others 2386look as if \isa{blast} alone could prove them: 2387\begin{isabelle} 2388\ 1.\ hard\isanewline 2389\ 2.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline 2390\ 3.\ Q\ \isasymLongrightarrow \ Q% 2391\end{isabelle} 2392% 2393The \commdx{defer} command moves the first subgoal into the last position. 2394\begin{isabelle} 2395\isacommand{defer}\ 1\isanewline 2396\ 1.\ \isasymnot \ \isasymnot \ P\ \isasymLongrightarrow \ P\isanewline 2397\ 2.\ Q\ \isasymLongrightarrow \ Q\isanewline 2398\ 3.\ hard% 2399\end{isabelle} 2400% 2401Now we apply \isa{blast} repeatedly to the easy subgoals: 2402\begin{isabelle} 2403\isacommand{apply}\ blast+\isanewline 2404\ 1.\ hard% 2405\end{isabelle} 2406Using \isacommand{defer}, we have cleared away the trivial parts of the proof so 2407that we can devote attention to the difficult part. 2408 2409\medskip 2410The \commdx{prefer} command moves the specified subgoal into the 2411first position. For example, if you suspect that one of your subgoals is 2412invalid (not a theorem), then you should investigate that subgoal first. If it 2413cannot be proved, then there is no point in proving the other subgoals. 2414\begin{isabelle} 2415\ 1.\ ok1\isanewline 2416\ 2.\ ok2\isanewline 2417\ 3.\ doubtful% 2418\end{isabelle} 2419% 2420We decide to work on the third subgoal. 2421\begin{isabelle} 2422\isacommand{prefer}\ 3\isanewline 2423\ 1.\ doubtful\isanewline 2424\ 2.\ ok1\isanewline 2425\ 3.\ ok2 2426\end{isabelle} 2427If we manage to prove \isa{doubtful}, then we can work on the other 2428subgoals, confident that we are not wasting our time. Finally we revise the 2429proof script to remove the \isacommand{prefer} command, since we needed it only to 2430focus our exploration. The previous example is different: its use of 2431\isacommand{defer} stops trivial subgoals from cluttering the rest of the 2432proof. Even there, we should consider proving \isa{hard} as a preliminary 2433lemma. Always seek ways to streamline your proofs. 2434 2435 2436\medskip 2437Summary: 2438\begin{itemize} 2439\item the control structures \isa+, \isa? and \isa| help express complicated proofs 2440\item the \isacommand{pr} command can limit the number of subgoals to display 2441\item the \isacommand{defer} and \isacommand{prefer} commands move a 2442subgoal to the last or first position 2443\end{itemize} 2444 2445\begin{exercise} 2446Explain the use of \isa? and \isa+ in this proof. 2447\begin{isabelle} 2448\isacommand{lemma}\ "\isasymlbrakk P\isasymand Q\isasymlongrightarrow R;\ P\isasymlongrightarrow Q;\ P\isasymrbrakk \ \isasymLongrightarrow \ R"\isanewline 2449\isacommand{by}\ (drule\ mp,\ (intro conjI)?,\ assumption+)+ 2450\end{isabelle} 2451\end{exercise} 2452 2453 2454 2455\section{Proving the Correctness of Euclid's Algorithm} 2456\label{sec:proving-euclid} 2457 2458\index{Euclid's algorithm|(}\index{*gcd (constant)|(}\index{divides relation|(}% 2459A brief development will demonstrate the techniques of this chapter, 2460including \isa{blast} applied with additional rules. We shall also see 2461\isa{case_tac} used to perform a Boolean case split. 2462 2463Let us prove that \isa{gcd} computes the greatest common 2464divisor of its two arguments. 2465% 2466We use induction: \isa{gcd.induct} is the 2467induction rule returned by \isa{fun}. We simplify using 2468rules proved in {\S}\ref{sec:fun-simplification}, since rewriting by the 2469definition of \isa{gcd} can loop. 2470\begin{isabelle} 2471\isacommand{lemma}\ gcd\_dvd\_both:\ "(gcd\ m\ n\ dvd\ m)\ \isasymand \ (gcd\ m\ n\ dvd\ n)" 2472\end{isabelle} 2473The induction formula must be a conjunction. In the 2474inductive step, each conjunct establishes the other. 2475\begin{isabelle} 2476\ 1.\ \isasymAnd m\ n.\ (n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline 2477\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \isanewline 2478\isaindent{\ 1.\ \isasymAnd m\ n.\ (}gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n)\ \isasymLongrightarrow \isanewline 2479\isaindent{\ 1.\ \isasymAnd m\ n.\ }gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n% 2480\end{isabelle} 2481 2482The conditional induction hypothesis suggests doing a case 2483analysis on \isa{n=0}. We apply \methdx{case_tac} with type 2484\isa{bool} --- and not with a datatype, as we have done until now. Since 2485\isa{nat} is a datatype, we could have written 2486\isa{case_tac~n} instead of \isa{case_tac~"n=0"}. However, the definition 2487of \isa{gcd} makes a Boolean decision: 2488\begin{isabelle} 2489\ \ \ \ "gcd\ m\ n\ =\ (if\ n=0\ then\ m\ else\ gcd\ n\ (m\ mod\ n))" 2490\end{isabelle} 2491Proofs about a function frequently follow the function's definition, so we perform 2492case analysis over the same formula. 2493\begin{isabelle} 2494\isacommand{apply}\ (case_tac\ "n=0")\isanewline 2495\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline 2496\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline 2497\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline 2498\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n\isanewline 2499\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline 2500\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline 2501\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline 2502\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ m\ n\ dvd\ m\ \isasymand \ gcd\ m\ n\ dvd\ n% 2503\end{isabelle} 2504% 2505Simplification leaves one subgoal: 2506\begin{isabelle} 2507\isacommand{apply}\ (simp_all)\isanewline 2508\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk gcd\ n\ (m\ mod\ n)\ dvd\ n\ \isasymand \ gcd\ n\ (m\ mod\ n)\ dvd\ m\ mod\ n;\isanewline 2509\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }0\ <\ n\isasymrbrakk \isanewline 2510\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ gcd\ n\ (m\ mod\ n)\ dvd\ m% 2511\end{isabelle} 2512% 2513Here, we can use \isa{blast}. 2514One of the assumptions, the induction hypothesis, is a conjunction. 2515The two divides relationships it asserts are enough to prove 2516the conclusion, for we have the following theorem at our disposal: 2517\begin{isabelle} 2518\isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% 2519\rulename{dvd_mod_imp_dvd} 2520\end{isabelle} 2521% 2522This theorem can be applied in various ways. As an introduction rule, it 2523would cause backward chaining from the conclusion (namely 2524\isa{?k~dvd~?m}) to the two premises, which 2525also involve the divides relation. This process does not look promising 2526and could easily loop. More sensible is to apply the rule in the forward 2527direction; each step would eliminate an occurrence of the \isa{mod} symbol, so the 2528process must terminate. 2529\begin{isabelle} 2530\isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline 2531\isacommand{done} 2532\end{isabelle} 2533Attaching the \attrdx{dest} attribute to \isa{dvd_mod_imp_dvd} tells 2534\isa{blast} to use it as destruction rule; that is, in the forward direction. 2535 2536\medskip 2537We have proved a conjunction. Now, let us give names to each of the 2538two halves: 2539\begin{isabelle} 2540\isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline 2541\isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]% 2542\end{isabelle} 2543Here we see \commdx{lemmas} 2544used with the \attrdx{iff} attribute, which supplies the new theorems to the 2545classical reasoner and the simplifier. Recall that \attrdx{THEN} is 2546frequently used with destruction rules; \isa{THEN conjunct1} extracts the 2547first half of a conjunctive theorem. Given \isa{gcd_dvd_both} it yields 2548\begin{isabelle} 2549\ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?m1 2550\end{isabelle} 2551The variable names \isa{?m1} and \isa{?n1} arise because 2552Isabelle renames schematic variables to prevent 2553clashes. The second \isacommand{lemmas} declaration yields 2554\begin{isabelle} 2555\ \ \ \ \ gcd\ ?m1\ ?n1\ dvd\ ?n1 2556\end{isabelle} 2557 2558\medskip 2559To complete the verification of the \isa{gcd} function, we must 2560prove that it returns the greatest of all the common divisors 2561of its arguments. The proof is by induction, case analysis and simplification. 2562\begin{isabelle} 2563\isacommand{lemma}\ gcd\_greatest\ [rule\_format]:\isanewline 2564\ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n" 2565\end{isabelle} 2566% 2567The goal is expressed using HOL implication, 2568\isa{\isasymlongrightarrow}, because the induction affects the two 2569preconditions. The directive \isa{rule_format} tells Isabelle to replace 2570each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before 2571storing the eventual theorem. This directive can also remove outer 2572universal quantifiers, converting the theorem into the usual format for 2573inference rules. It can replace any series of applications of 2574\isa{THEN} to the rules \isa{mp} and \isa{spec}. We did not have to 2575write this: 2576\begin{isabelle} 2577\isacommand{lemma}\ gcd_greatest\ 2578[THEN mp, THEN mp]:\isanewline 2579\ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n" 2580\end{isabelle} 2581 2582Because we are again reasoning about \isa{gcd}, we perform the same 2583induction and case analysis as in the previous proof: 2584\begingroup\samepage 2585\begin{isabelle} 2586\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline 2587\isaindent{\ 1.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline 2588\isaindent{\ 1.\ \isasymAnd m\ n.\ \ }n\ =\ 0\isasymrbrakk \isanewline 2589\isaindent{\ 1.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n\isanewline 2590\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk n\ \isasymnoteq \ 0\ \isasymLongrightarrow \isanewline 2591\isaindent{\ 2.\ \isasymAnd m\ n.\ \isasymlbrakk }k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ m\ mod\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ n\ (m\ mod\ n);\isanewline 2592\isaindent{\ 2.\ \isasymAnd m\ n.\ \ }n\ \isasymnoteq \ 0\isasymrbrakk \isanewline 2593\isaindent{\ 2.\ \isasymAnd m\ n.\ }\isasymLongrightarrow \ k\ dvd\ m\ \isasymlongrightarrow \ k\ dvd\ n\ \isasymlongrightarrow \ k\ dvd\ gcd\ m\ n% 2594\end{isabelle} 2595\endgroup 2596 2597\noindent Simplification proves both subgoals. 2598\begin{isabelle} 2599\isacommand{apply}\ (simp_all\ add:\ dvd_mod)\isanewline 2600\isacommand{done} 2601\end{isabelle} 2602In the first, where \isa{n=0}, the implication becomes trivial: \isa{k\ dvd\ 2603gcd\ m\ n} goes to~\isa{k\ dvd\ m}. The second subgoal is proved by 2604an unfolding of \isa{gcd}, using this rule about divides: 2605\begin{isabelle} 2606\isasymlbrakk ?f\ dvd\ ?m;\ ?f\ dvd\ ?n\isasymrbrakk \ 2607\isasymLongrightarrow \ ?f\ dvd\ ?m\ mod\ ?n% 2608\rulename{dvd_mod} 2609\end{isabelle} 2610 2611 2612\medskip 2613The facts proved above can be summarized as a single logical 2614equivalence. This step gives us a chance to see another application 2615of \isa{blast}. 2616\begin{isabelle} 2617\isacommand{theorem}\ gcd\_greatest\_iff\ [iff]:\ \isanewline 2618\ \ \ \ \ \ \ \ "(k\ dvd\ gcd\ m\ n)\ =\ (k\ dvd\ m\ \isasymand \ k\ dvd\ n)"\isanewline 2619\isacommand{by}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans) 2620\end{isabelle} 2621This theorem concisely expresses the correctness of the \isa{gcd} 2622function. 2623We state it with the \isa{iff} attribute so that 2624Isabelle can use it to remove some occurrences of \isa{gcd}. 2625The theorem has a one-line 2626proof using \isa{blast} supplied with two additional introduction 2627rules. The exclamation mark 2628({\isa{intro}}{\isa{!}})\ signifies safe rules, which are 2629applied aggressively. Rules given without the exclamation mark 2630are applied reluctantly and their uses can be undone if 2631the search backtracks. Here the unsafe rule expresses transitivity 2632of the divides relation: 2633\begin{isabelle} 2634\isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p% 2635\rulename{dvd_trans} 2636\end{isabelle} 2637Applying \isa{dvd_trans} as 2638an introduction rule entails a risk of looping, for it multiplies 2639occurrences of the divides symbol. However, this proof relies 2640on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply 2641aggressively because it yields simpler subgoals. The proof implicitly 2642uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were 2643declared using \isa{iff}.% 2644\index{Euclid's algorithm|)}\index{*gcd (constant)|)}\index{divides relation|)} 2645