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

doc-src/TutorialI/Rules/rules.tex

author | paulson |

Mon, 04 Dec 2000 17:30:15 +0100 | |

changeset 10578 | b32513971481 |

parent 10546 | b0ad1ed24cf6 |

child 10596 | 77951eaeb5b0 |

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

fixed formatting in section heading

\chapter{The Rules of the Game} \label{chap:rules} Until now, we have proved everything using only induction and simplification. Substantial proofs require more elaborate forms of inference. This chapter outlines the concepts and techniques that underlie reasoning in Isabelle. The examples are mainly drawn from predicate logic. The first examples in this chapter will consist of detailed, low-level proof steps. Later, we shall see how to automate such reasoning using the methods \isa{blast}, \isa{auto} and others. \section{Natural deduction} In Isabelle, proofs are constructed using inference rules. The most familiar inference rule is probably \emph{modus ponens}: \[ \infer{Q}{P\imp Q & P} \] This rule says that from $P\imp Q$ and $P$ we may infer~$Q$. %Early logical formalisms had this %rule and at most one or two others, along with many complicated %axioms. Any desired theorem could be obtained by applying \emph{modus %ponens} or other rules to the axioms, but proofs were %hard to find. For example, a standard inference system has %these two axioms (amongst others): %\begin{gather*} % P\imp(Q\imp P) \tag{K}\\ % (P\imp(Q\imp R))\imp ((P\imp Q)\imp(P\imp R)) \tag{S} %\end{gather*} %Try proving the trivial fact $P\imp P$ using these axioms and \emph{modus %ponens}! \textbf{Natural deduction} is an attempt to formalize logic in a way that mirrors human reasoning patterns. % %Instead of having a few %inference rules and many axioms, it has many inference rules %and few axioms. % For each logical symbol (say, $\conj$), there are two kinds of rules: \textbf{introduction} and \textbf{elimination} rules. The introduction rules allow us to infer this symbol (say, to infer conjunctions). The elimination rules allow us to deduce consequences from this symbol. Ideally each rule should mention one symbol only. For predicate logic this can be done, but when users define their own concepts they typically have to refer to other symbols as well. It is best not be dogmatic. Natural deduction generally deserves its name. It is easy to use. Each proof step consists of identifying the outermost symbol of a formula and applying the corresponding rule. It creates new subgoals in an obvious way from parts of the chosen formula. Expanding the definitions of constants can blow up the goal enormously. Deriving natural deduction rules for such constants lets us reason in terms of their key properties, which might otherwise be obscured by the technicalities of its definition. Natural deduction rules also lend themselves to automation. Isabelle's \textbf{classical reasoner} accepts any suitable collection of natural deduction rules and uses them to search for proofs automatically. Isabelle is designed around natural deduction and many of its tools use the terminology of introduction and elimination rules. \section{Introduction rules} An \textbf{introduction} rule tells us when we can infer a formula containing a specific logical symbol. For example, the conjunction introduction rule says that if we have $P$ and if we have $Q$ then we have $P\conj Q$. In a mathematics text, it is typically shown like this: \[ \infer{P\conj Q}{P & Q} \] The rule introduces the conjunction symbol~($\conj$) in its conclusion. Of course, in Isabelle proofs we mainly reason backwards. When we apply this rule, the subgoal already has the form of a conjunction; the proof step makes this conjunction symbol disappear. In Isabelle notation, the rule looks like this: \begin{isabelle} \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P\ \isasymand\ ?Q\rulename{conjI} \end{isabelle} Carefully examine the syntax. The premises appear to the left of the arrow and the conclusion to the right. The premises (if more than one) are grouped using the fat brackets. The question marks indicate \textbf{schematic variables} (also called \textbf{unknowns}): they may be replaced by arbitrary formulas. If we use the rule backwards, Isabelle tries to unify the current subgoal with the conclusion of the rule, which has the form \isa{?P\ \isasymand\ ?Q}. (Unification is discussed below, \S\ref{sec:unification}.) If successful, it yields new subgoals given by the formulas assigned to \isa{?P} and \isa{?Q}. The following trivial proof illustrates this point. \begin{isabelle} \isacommand{lemma}\ conj_rule:\ "{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ (Q\ \isasymand\ P)"\isanewline \isacommand{apply}\ (rule\ conjI)\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{apply}\ (rule\ conjI)\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{apply}\ assumption \end{isabelle} At the start, Isabelle presents us with the assumptions (\isa{P} and~\isa{Q}) and with the goal to be proved, \isa{P\ \isasymand\ (Q\ \isasymand\ P)}. We are working backwards, so when we apply conjunction introduction, the rule removes the outermost occurrence of the \isa{\isasymand} symbol. To apply a rule to a subgoal, we apply the proof method {\isa{rule}} --- here with {\isa{conjI}}, the conjunction introduction rule. \begin{isabelle} %{\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\ \isasymand\ Q\ %\isasymand\ P\isanewline \ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline \ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P \end{isabelle} Isabelle leaves two new subgoals: the two halves of the original conjunction. The first is simply \isa{P}, which is trivial, since \isa{P} is among the assumptions. We can apply the {\isa{assumption}} method, which proves a subgoal by finding a matching assumption. \begin{isabelle} \ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\ \isasymand\ P \end{isabelle} We are left with the subgoal of proving \isa{Q\ \isasymand\ P} from the assumptions \isa{P} and~\isa{Q}. We apply \isa{rule conjI} again. \begin{isabelle} \ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline \ 2.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P \end{isabelle} We are left with two new subgoals, \isa{Q} and~\isa{P}, each of which can be proved using the {\isa{assumption}} method. \section{Elimination rules} \textbf{Elimination} rules work in the opposite direction from introduction rules. In the case of conjunction, there are two such rules. From $P\conj Q$ we infer $P$. also, from $P\conj Q$ we infer $Q$: \[ \infer{P}{P\conj Q} \qquad \infer{Q}{P\conj Q} \] Now consider disjunction. There are two introduction rules, which resemble inverted forms of the conjunction elimination rules: \[ \infer{P\disj Q}{P} \qquad \infer{P\disj Q}{Q} \] What is the disjunction elimination rule? The situation is rather different from conjunction. From $P\disj Q$ we cannot conclude that $P$ is true and we cannot conclude that $Q$ is true; there are no direct elimination rules of the sort that we have seen for conjunction. Instead, there is an elimination rule that works indirectly. If we are trying to prove something else, say $R$, and we know that $P\disj Q$ holds, then we have to consider two cases. We can assume that $P$ is true and prove $R$ and then assume that $Q$ is true and prove $R$ a second time. Here we see a fundamental concept used in natural deduction: that of the \textbf{assumptions}. We have to prove $R$ twice, under different assumptions. The assumptions are local to these subproofs and are visible nowhere else. In a logic text, the disjunction elimination rule might be shown like this: \[ \infer{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}} \] The assumptions $[P]$ and $[Q]$ are bracketed to emphasize that they are local to their subproofs. In Isabelle notation, the already-familiar \isa\isasymLongrightarrow syntax serves the same purpose: \begin{isabelle} \isasymlbrakk?P\ \isasymor\ ?Q;\ ?P\ \isasymLongrightarrow\ ?R;\ ?Q\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{disjE} \end{isabelle} When we use this sort of elimination rule backwards, it produces a case split. (We have this before, in proofs by induction.) The following proof illustrates the use of disjunction elimination. \begin{isabelle} \isacommand{lemma}\ disj_swap:\ "P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P"\isanewline \isacommand{apply}\ (erule\ disjE)\isanewline \ \isacommand{apply}\ (rule\ disjI2)\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{apply}\ (rule\ disjI1)\isanewline \isacommand{apply}\ assumption \end{isabelle} We assume \isa{P\ \isasymor\ Q} and must prove \isa{Q\ \isasymor\ P}\@. Our first step uses the disjunction elimination rule, \isa{disjE}. The method {\isa{erule}} applies an elimination rule to the assumptions, searching for one that matches the rule's first premise. Deleting that assumption, it return the subgoals for the remaining premises. Most of the time, this is the best way to use elimination rules; only rarely is there any point in keeping the assumption. \begin{isabelle} %P\ \isasymor\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline \ 1.\ P\ \isasymLongrightarrow\ Q\ \isasymor\ P\isanewline \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P \end{isabelle} Here it leaves us with two subgoals. The first assumes \isa{P} and the second assumes \isa{Q}. Tackling the first subgoal, we need to show \isa{Q\ \isasymor\ P}\@. The second introduction rule (\isa{disjI2}) can reduce this to \isa{P}, which matches the assumption. So, we apply the {\isa{rule}} method with \isa{disjI2} \ldots \begin{isabelle} \ 1.\ P\ \isasymLongrightarrow\ P\isanewline \ 2.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P \end{isabelle} \ldots and finish off with the {\isa{assumption}} method. We are left with the other subgoal, which assumes \isa{Q}. \begin{isabelle} \ 1.\ Q\ \isasymLongrightarrow\ Q\ \isasymor\ P \end{isabelle} Its proof is similar, using the introduction rule \isa{disjI1}. The result of this proof is a new inference rule \isa{disj_swap}, which is neither an introduction nor an elimination rule, but which might be useful. We can use it to replace any goal of the form $Q\disj P$ by a one of the form $P\disj Q$. \section{Destruction rules: some examples} Now let us examine the analogous proof for conjunction. \begin{isabelle} \isacommand{lemma}\ conj_swap:\ "P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P"\isanewline \isacommand{apply}\ (rule\ conjI)\isanewline \ \isacommand{apply}\ (drule\ conjunct2)\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{apply}\ (drule\ conjunct1)\isanewline \isacommand{apply}\ assumption \end{isabelle} Recall that the conjunction elimination rules --- whose Isabelle names are \isa{conjunct1} and \isa{conjunct2} --- simply return the first or second half of a conjunction. Rules of this sort (where the conclusion is a subformula of a premise) are called \textbf{destruction} rules, by analogy with the destructor functions of functional programming.% \footnote{This Isabelle terminology has no counterpart in standard logic texts, although the distinction between the two forms of elimination rule is well known. Girard \cite[page 74]{girard89}, for example, writes ``The elimination rules are very bad. What is catastrophic about them is the parasitic presence of a formula [$R$] which has no structural link with the formula which is eliminated.''} The first proof step applies conjunction introduction, leaving two subgoals: \begin{isabelle} %P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\ \isasymand\ P\isanewline \ 1.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ Q\isanewline \ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P \end{isabelle} To invoke the elimination rule, we apply a new method, \isa{drule}. Think of the \isa{d} as standing for \textbf{destruction} (or \textbf{direct}, if you prefer). Applying the second conjunction rule using \isa{drule} replaces the assumption \isa{P\ \isasymand\ Q} by \isa{Q}. \begin{isabelle} \ 1.\ Q\ \isasymLongrightarrow\ Q\isanewline \ 2.\ P\ \isasymand\ Q\ \isasymLongrightarrow\ P \end{isabelle} The resulting subgoal can be proved by applying \isa{assumption}. The other subgoal is similarly proved, using the \isa{conjunct1} rule and the \isa{assumption} method. Choosing among the methods \isa{rule}, \isa{erule} and \isa{drule} is up to you. Isabelle does not attempt to work out whether a rule is an introduction rule or an elimination rule. The method determines how the rule will be interpreted. Many rules can be used in more than one way. For example, \isa{disj_swap} can be applied to assumptions as well as to goals; it replaces any assumption of the form $P\disj Q$ by a one of the form $Q\disj P$. Destruction rules are simpler in form than indirect rules such as \isa{disjE}, but they can be inconvenient. Each of the conjunction rules discards half of the formula, when usually we want to take both parts of the conjunction as new assumptions. The easiest way to do so is by using an alternative conjunction elimination rule that resembles \isa{disjE}. It is seldom, if ever, seen in logic books. In Isabelle syntax it looks like this: \begin{isabelle} \isasymlbrakk?P\ \isasymand\ ?Q;\ \isasymlbrakk?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?R\isasymrbrakk\ \isasymLongrightarrow\ ?R\rulename{conjE} \end{isabelle} \begin{exercise} Use the rule {\isa{conjE}} to shorten the proof above. \end{exercise} \section{Implication} At the start of this chapter, we saw the rule \textit{modus ponens}. It is, in fact, a destruction rule. The matching introduction rule looks like this in Isabelle: \begin{isabelle} (?P\ \isasymLongrightarrow\ ?Q)\ \isasymLongrightarrow\ ?P\ \isasymlongrightarrow\ ?Q\rulename{impI} \end{isabelle} And this is \textit{modus ponens}: \begin{isabelle} \isasymlbrakk?P\ \isasymlongrightarrow\ ?Q;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?Q \rulename{mp} \end{isabelle} Here is a proof using the rules for implication. This lemma performs a sort of uncurrying, replacing the two antecedents of a nested implication by a conjunction. \begin{isabelle} \isacommand{lemma}\ imp_uncurry:\ "P\ \isasymlongrightarrow\ (Q\ \isasymlongrightarrow\ R)\ \isasymLongrightarrow\ P\ \isasymand\ Q\ \isasymlongrightarrow\ R"\isanewline \isacommand{apply}\ (rule\ impI)\isanewline \isacommand{apply}\ (erule\ conjE)\isanewline \isacommand{apply}\ (drule\ mp)\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{apply}\ (drule\ mp)\isanewline \ \ \isacommand{apply}\ assumption\isanewline \ \isacommand{apply}\ assumption \end{isabelle} First, we state the lemma and apply implication introduction (\isa{rule impI}), which moves the conjunction to the assumptions. \begin{isabelle} %P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R\ \isasymLongrightarrow\ P\ %\isasymand\ Q\ \isasymlongrightarrow\ R\isanewline \ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P\ \isasymand\ Q\isasymrbrakk\ \isasymLongrightarrow\ R \end{isabelle} Next, we apply conjunction elimination (\isa{erule conjE}), which splits this conjunction into two parts. \begin{isabelle} \ 1.\ {\isasymlbrakk}P\ \isasymlongrightarrow\ Q\ \isasymlongrightarrow\ R;\ P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ R \end{isabelle} Now, we work on the assumption \isa{P\ \isasymlongrightarrow\ (Q\ \isasymlongrightarrow\ R)}, where the parentheses have been inserted for clarity. The nested implication requires two applications of \textit{modus ponens}: \isa{drule mp}. The first use yields the implication \isa{Q\ \isasymlongrightarrow\ R}, but first we must prove the extra subgoal \isa{P}, which we do by assumption. \begin{isabelle} \ 1.\ {\isasymlbrakk}P;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P\isanewline \ 2.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R \end{isabelle} Repeating these steps for \isa{Q\ \isasymlongrightarrow\ R} yields the conclusion we seek, namely~\isa{R}. \begin{isabelle} \ 1.\ {\isasymlbrakk}P;\ Q;\ Q\ \isasymlongrightarrow\ R\isasymrbrakk\ \isasymLongrightarrow\ R \end{isabelle} The symbols \isa{\isasymLongrightarrow} and \isa{\isasymlongrightarrow} both stand for implication, but they differ in many respects. Isabelle uses \isa{\isasymLongrightarrow} to express inference rules; the symbol is built-in and Isabelle's inference mechanisms treat it specially. On the other hand, \isa{\isasymlongrightarrow} is just one of the many connectives available in higher-order logic. We reason about it using inference rules such as \isa{impI} and \isa{mp}, just as we reason about the other connectives. You will have to use \isa{\isasymlongrightarrow} in any context that requires a formula of higher-order logic. Use \isa{\isasymLongrightarrow} to separate a theorem's preconditions from its conclusion. When using induction, often the desired theorem results in an induction hypothesis that is too weak. In such cases you may have to invent a more complicated induction formula, typically involving \isa{\isasymlongrightarrow} and \isa{\isasymforall}. From this lemma you derive the desired theorem , typically involving \isa{\isasymLongrightarrow}. We shall see an example below, \S\ref{sec:proving-euclid}. \section{Unification and substitution}\label{sec:unification} As we have seen, Isabelle rules involve variables that begin with a question mark. These are called \textbf{schematic} variables and act as placeholders for terms. \textbf{Unification} refers to the process of making two terms identical, possibly by replacing their variables by terms. The simplest case is when the two terms are already the same. Next simplest is when the variables in only one of the term are replaced; this is called \textbf{pattern-matching}. The {\isa{rule}} method typically matches the rule's conclusion against the current subgoal. In the most complex case, variables in both terms are replaced; the {\isa{rule}} method can do this the goal itself contains schematic variables. Other occurrences of the variables in the rule or proof state are updated at the same time. Schematic variables in goals are sometimes called \textbf{unknowns}. They are useful because they let us proceed with a proof even when we do not know what certain terms should be --- as when the goal is $\exists x.\,P$. They can be filled in later, often automatically. Unification is well known to Prolog programmers. Isabelle uses \textbf{higher-order} unification, which is unification in the typed $\lambda$-calculus. The general case is undecidable, but for our purposes, the differences from ordinary unification are straightforward. It handles bound variables correctly, avoiding capture. The two terms \isa{{\isasymlambda}x.\ ?P} and \isa{{\isasymlambda}x.\ t x} are not unifiable; replacing \isa{?P} by \isa{t x} is forbidden because the free occurrence of~\isa{x} would become bound. The two terms \isa{{\isasymlambda}x.\ f(x,z)} and \isa{{\isasymlambda}y.\ f(y,z)} are trivially unifiable because they differ only by a bound variable renaming. Higher-order unification sometimes must invent $\lambda$-terms to replace function variables, which can lead to a combinatorial explosion. However, Isabelle proofs tend to involve easy cases where there are few possibilities for the $\lambda$-term being constructed. In the easiest case, the function variable is applied only to bound variables, as when we try to unify \isa{{\isasymlambda}x\ y.\ f(?h x y)} and \isa{{\isasymlambda}x\ y.\ f(x+y+a)}. The only solution is to replace \isa{?h} by \isa{{\isasymlambda}x\ y.\ x+y+a}. Such cases admit at most one unifier, like ordinary unification. A harder case is unifying \isa{?h a} with~\isa{a+b}; it admits two solutions for \isa{?h}, namely \isa{{\isasymlambda}x.~a+b} and \isa{{\isasymlambda}x.~x+b}. Unifying \isa{?h a} with~\isa{a+a+b} admits four solutions; their number is exponential in the number of occurrences of~\isa{a} in the second term. Isabelle also uses function variables to express \textbf{substitution}. A typical substitution rule allows us to replace one term by another if we know that two terms are equal. \[ \infer{P[t/x]}{s=t & P[s/x]} \] The conclusion uses a notation for substitution: $P[t/x]$ is the result of replacing $x$ by~$t$ in~$P$. The rule only substitutes in the positions designated by~$x$, which gives it additional power. For example, it can derive symmetry of equality from reflexivity. Using $x=s$ for~$P$ replaces just the first $s$ in $s=s$ by~$t$. \[ \infer{t=s}{s=t & \infer{s=s}{}} \] The Isabelle version of the substitution rule looks like this: \begin{isabelle} \isasymlbrakk?t\ =\ ?s;\ ?P\ ?s\isasymrbrakk\ \isasymLongrightarrow\ ?P\ ?t \rulename{ssubst} \end{isabelle} Crucially, \isa{?P} is a function variable: it can be replaced by a $\lambda$-expression involving one bound variable whose occurrences identify the places in which $s$ will be replaced by~$t$. The proof above requires \isa{{\isasymlambda}x.~x=s}. The \isa{simp} method replaces equals by equals, but using the substitution rule gives us more control. Consider this proof: \begin{isabelle} \isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ odd(f\ x)\ \isasymrbrakk\ \isasymLongrightarrow\ odd\ x"\isanewline \isacommand{apply}\ (erule\ ssubst)\isanewline \isacommand{apply}\ assumption\isanewline \isacommand{done}\end{isabelle} % The simplifier might loop, replacing \isa{x} by \isa{f x} and then by \isa{f(f x)} and so forth. (Actually, \isa{simp} sees the danger and re-orients this equality, but in more complicated cases it can be fooled.) When we apply substitution, Isabelle replaces every \isa{x} in the subgoal by \isa{f x} just once: it cannot loop. The resulting subgoal is trivial by assumption. We are using the \isa{erule} method it in a novel way. Hitherto, the conclusion of the rule was just a variable such as~\isa{?R}, but it may be any term. The conclusion is unified with the subgoal just as it would be with the \isa{rule} method. At the same time \isa{erule} looks for an assumption that matches the rule's first premise, as usual. With \isa{ssubst} the effect is to find, use and delete an equality assumption. Higher-order unification can be tricky, as this example indicates: \begin{isabelle} \isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline \isacommand{apply}\ (erule\ ssubst)\isanewline \isacommand{back}\isanewline \isacommand{back}\isanewline \isacommand{back}\isanewline \isacommand{back}\isanewline \isacommand{apply}\ assumption\isanewline \isacommand{done} \end{isabelle} % By default, Isabelle tries to substitute for all the occurrences. Applying \isa{erule\ ssubst} yields this subgoal: \begin{isabelle} \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ (f\ x) \end{isabelle} The substitution should have been done in the first two occurrences of~\isa{x} only. Isabelle has gone too far. The \isa{back} method allows us to reject this possibility and get a new one: \begin{isabelle} \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ (f\ x)\ (f\ x) \end{isabelle} % Now Isabelle has left the first occurrence of~\isa{x} alone. That is promising but it is not the desired combination. So we use \isa{back} again: \begin{isabelle} \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ x\ (f\ x) \end{isabelle} % This also is wrong, so we use \isa{back} again: \begin{isabelle} \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ x\ x\ (f\ x) \end{isabelle} % And this one is wrong too. Looking carefully at the series of alternatives, we see a binary countdown with reversed bits: 111, 011, 101, 001. Invoke \isa{back} again: \begin{isabelle} \ 1.\ triple\ (f\ x)\ (f\ x)\ x\ \isasymLongrightarrow\ triple\ (f\ x)\ (f\ x)\ x% \end{isabelle} At last, we have the right combination! This goal follows by assumption. Never use {\isa{back}} in the final version of a proof. It should only be used for exploration. One way to get rid of {\isa{back}} to combine two methods in a single \textbf{apply} command. Isabelle applies the first method and then the second. If the second method fails then Isabelle automatically backtracks. This process continues until the first method produces an output that the second method can use. We get a one-line proof of our example: \begin{isabelle} \isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline \isacommand{apply}\ (erule\ ssubst,\ assumption)\isanewline \isacommand{done} \end{isabelle} The most general way to get rid of the {\isa{back}} command is to instantiate variables in the rule. The method {\isa{rule\_tac}} is similar to \isa{rule}, but it makes some of the rule's variables denote specified terms. Also available are {\isa{drule\_tac}} and \isa{erule\_tac}. Here we need \isa{erule\_tac} since above we used \isa{erule}. \begin{isabelle} \isacommand{lemma}\ "{\isasymlbrakk}\ x\ =\ f\ x;\ triple\ (f\ x)\ (f\ x)\ x\ \isasymrbrakk\ \isasymLongrightarrow\ triple\ x\ x\ x"\isanewline \isacommand{apply}\ (erule_tac\ P="{\isasymlambda}u.\ triple\ u\ u\ x"\ \isakeyword{in}\ ssubst)\isanewline \isacommand{apply}\ assumption\isanewline \isacommand{done} \end{isabelle} % To specify a desired substitution requires instantiating the variable \isa{?P} with a $\lambda$-expression. The bound variable occurrences in \isa{{\isasymlambda}u.\ P\ u\ u\ x} indicate that the first two arguments have to be substituted, leaving the third unchanged. An alternative to {\isa{rule\_tac}} is to use \isa{rule} with the {\isa{of}} directive, described in \S\ref{sec:forward} below. An advantage of {\isa{rule\_tac}} is that the instantiations may refer to variables bound in the current subgoal. \section{Negation} Negation causes surprising complexity in proofs. Its natural deduction rules are straightforward, but additional rules seem necessary in order to handle negated assumptions gracefully. Negation introduction deduces $\neg P$ if assuming $P$ leads to a contradiction. Negation elimination deduces any formula in the presence of $\neg P$ together with~$P$: \begin{isabelle} (?P\ \isasymLongrightarrow\ False)\ \isasymLongrightarrow\ \isasymnot\ ?P% \rulename{notI}\isanewline \isasymlbrakk{\isasymnot}\ ?P;\ ?P\isasymrbrakk\ \isasymLongrightarrow\ ?R% \rulename{notE} \end{isabelle} % Classical logic allows us to assume $\neg P$ when attempting to prove~$P$: \begin{isabelle} (\isasymnot\ ?P\ \isasymLongrightarrow\ ?P)\ \isasymLongrightarrow\ ?P% \rulename{classical} \end{isabelle} % Three further rules are variations on the theme of contrapositive. They differ in the placement of the negation symbols: \begin{isabelle} \isasymlbrakk?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ \isasymnot\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% \rulename{contrapos_pp}\isanewline \isasymlbrakk{\isasymnot}\ ?Q;\ \isasymnot\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% \rulename{contrapos_np}\isanewline \isasymlbrakk{\isasymnot}\ ?Q;\ ?P\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ \isasymnot\ ?P% \rulename{contrapos_nn} \end{isabelle} % These rules are typically applied using the {\isa{erule}} method, where their effect is to form a contrapositive from an assumption and the goal's conclusion. The most important of these is \isa{contrapos_np}. It is useful for applying introduction rules to negated assumptions. For instance, the assumption $\neg(P\imp Q)$ is equivalent to the conclusion $P\imp Q$ and we might want to use conjunction introduction on it. Before we can do so, we must move that assumption so that it becomes the conclusion. The following proof demonstrates this technique: \begin{isabelle} \isacommand{lemma}\ "\isasymlbrakk{\isasymnot}(P{\isasymlongrightarrow}Q);\ \isasymnot(R{\isasymlongrightarrow}Q)\isasymrbrakk\ \isasymLongrightarrow\ R"\isanewline \isacommand{apply}\ (erule_tac\ Q="R{\isasymlongrightarrow}Q"\ \isakeyword{in}\ contrapos_np)\isanewline \isacommand{apply}\ intro\isanewline \isacommand{apply}\ (erule\ notE,\ assumption)\isanewline \isacommand{done} \end{isabelle} % There are two negated assumptions and we need to exchange the conclusion with the second one. The method \isa{erule contrapos_np} would select the first assumption, which we do not want. So we specify the desired assumption explicitly, using \isa{erule_tac}. This is the resulting subgoal: \begin{isabelle} \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R\isasymrbrakk\ \isasymLongrightarrow\ R\ \isasymlongrightarrow\ Q% \end{isabelle} The former conclusion, namely \isa{R}, now appears negated among the assumptions, while the negated formula \isa{R\ \isasymlongrightarrow\ Q} becomes the new conclusion. We can now apply introduction rules. We use the {\isa{intro}} method, which repeatedly applies built-in introduction rules. Here its effect is equivalent to \isa{rule impI}.\begin{isabelle} \ 1.\ \isasymlbrakk{\isasymnot}\ (P\ \isasymlongrightarrow\ Q);\ \isasymnot\ R;\ R\isasymrbrakk\ \isasymLongrightarrow\ Q% \end{isabelle} We can see a contradiction in the form of assumptions \isa{\isasymnot\ R} and~\isa{R}, which suggests using negation elimination. If applied on its own, however, it will select the first negated assumption, which is useless. Instead, we combine the rule with the \isa{assumption} method: \begin{isabelle} \ \ \ \ \ (erule\ notE,\ assumption) \end{isabelle} Now when Isabelle selects the first assumption, it tries to prove \isa{P\ \isasymlongrightarrow\ Q} and fails; it then backtracks, finds the assumption~\isa{\isasymnot\ R} and finally proves \isa{R} by assumption. That concludes the proof. \medskip Here is another example. \begin{isabelle} \isacommand{lemma}\ "(P\ \isasymor\ Q)\ \isasymand\ R\ \isasymLongrightarrow\ P\ \isasymor\ Q\ \isasymand\ R"\isanewline \isacommand{apply}\ intro% \isacommand{apply}\ (elim\ conjE\ disjE)\isanewline \ \isacommand{apply}\ assumption \isanewline \isacommand{apply}\ (erule\ contrapos_np,\ rule\ conjI)\isanewline \ \ \isacommand{apply}\ assumption\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{done} \end{isabelle} % The first proof step applies the {\isa{intro}} method, which repeatedly uses built-in introduction rules. Here it creates the negative assumption \isa{\isasymnot\ (Q\ \isasymand\ R)}. \begin{isabelle} \ 1.\ \isasymlbrakk(P\ \isasymor\ Q)\ \isasymand\ R;\ \isasymnot\ (Q\ \isasymand\ R)\isasymrbrakk\ \isasymLongrightarrow\ P% \end{isabelle} It comes from \isa{disjCI}, a disjunction introduction rule that is more powerful than the separate rules \isa{disjI1} and \isa{disjI2}. Next we apply the {\isa{elim}} method, which repeatedly applies elimination rules; here, the elimination rules given in the command. One of the subgoals is trivial, leaving us with one other: \begin{isabelle} \ 1.\ \isasymlbrakk{\isasymnot}\ (Q\ \isasymand\ R);\ R;\ Q\isasymrbrakk\ \isasymLongrightarrow\ P% \end{isabelle} % Now we must move the formula \isa{Q\ \isasymand\ R} to be the conclusion. The combination \begin{isabelle} \ \ \ \ \ (erule\ contrapos_np,\ rule\ conjI) \end{isabelle} is robust: the \isa{conjI} forces the \isa{erule} to select a conjunction. The two subgoals are the ones we would expect from applying conjunction introduction to \isa{Q\ \isasymand\ R}: \begin{isabelle} \ 1.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\isanewline \ 2.\ {\isasymlbrakk}R;\ Q;\ \isasymnot\ P\isasymrbrakk\ \isasymLongrightarrow\ R% \end{isabelle} The rest of the proof is trivial. \section{The universal quantifier} Quantifiers require formalizing syntactic substitution and the notion of \textbf{arbitrary value}. Consider the universal quantifier. In a logic book, its introduction rule looks like this: \[ \infer{\forall x.\,P}{P} \] Typically, a proviso written in English says that $x$ must not occur in the assumptions. This proviso guarantees that $x$ can be regarded as arbitrary, since it has not been assumed to satisfy any special conditions. Isabelle's underlying formalism, called the \textbf{meta-logic}, eliminates the need for English. It provides its own universal quantifier (\isasymAnd) to express the notion of an arbitrary value. We have already seen another symbol of the meta-logic, namely \isa\isasymLongrightarrow, which expresses inference rules and the treatment of assumptions. The only other symbol in the meta-logic is \isa\isasymequiv, which can be used to define constants. Returning to the universal quantifier, we find that having a similar quantifier as part of the meta-logic makes the introduction rule trivial to express: \begin{isabelle} ({\isasymAnd}x.\ ?P\ x)\ \isasymLongrightarrow\ {\isasymforall}x.\ ?P\ x\rulename{allI} \end{isabelle} The following trivial proof demonstrates how the universal introduction rule works. \begin{isabelle} \isacommand{lemma}\ "{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x"\isanewline \isacommand{apply}\ (rule\ allI)\isanewline \isacommand{apply}\ (rule\ impI)\isanewline \isacommand{apply}\ assumption \end{isabelle} The first step invokes the rule by applying the method \isa{rule allI}. \begin{isabelle} %{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ x\isanewline \ 1.\ {\isasymAnd}x.\ P\ x\ \isasymlongrightarrow\ P\ x \end{isabelle} Note that the resulting proof state has a bound variable, namely~\bigisa{x}. The rule has replaced the universal quantifier of higher-order logic by Isabelle's meta-level quantifier. Our goal is to prove \isa{P\ x\ \isasymlongrightarrow\ P\ x} for arbitrary~\isa{x}; it is an implication, so we apply the corresponding introduction rule (\isa{impI}). \begin{isabelle} \ 1.\ {\isasymAnd}x.\ P\ x\ \isasymLongrightarrow\ P\ x \end{isabelle} The {\isa{assumption}} method proves this last subgoal. \medskip Now consider universal elimination. In a logic text, the rule looks like this: \[ \infer{P[t/x]}{\forall x.\,P} \] The conclusion is $P$ with $t$ substituted for the variable~$x$. Isabelle expresses substitution using a function variable: \begin{isabelle} {\isasymforall}x.\ ?P\ x\ \isasymLongrightarrow\ ?P\ ?x\rulename{spec} \end{isabelle} This destruction rule takes a universally quantified formula and removes the quantifier, replacing the bound variable \bigisa{x} by the schematic variable \bigisa{?x}. Recall that a schematic variable starts with a question mark and acts as a placeholder: it can be replaced by any term. To see how this works, let us derive a rule about reducing the scope of a universal quantifier. In mathematical notation we write \[ \infer{P\imp\forall x.\,Q}{\forall x.\,P\imp Q} \] with the proviso `$x$ not free in~$P$.' Isabelle's treatment of substitution makes the proviso unnecessary. The conclusion is expressed as \isa{P\ \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)}. No substitution for the variable \isa{P} can introduce a dependence upon~\isa{x}: that would be a bound variable capture. Here is the isabelle proof in full: \begin{isabelle} \isacommand{lemma}\ "({\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x)\ \isasymLongrightarrow\ P\ \isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)"\isanewline \isacommand{apply}\ (rule\ impI)\isanewline \isacommand{apply}\ (rule\ allI)\isanewline \isacommand{apply}\ (drule\ spec)\isanewline \isacommand{apply}\ (drule\ mp)\isanewline \ \ \isacommand{apply}\ assumption\isanewline \ \isacommand{apply}\ assumption \end{isabelle} First we apply implies introduction (\isa{rule impI}), which moves the \isa{P} from the conclusion to the assumptions. Then we apply universal introduction (\isa{rule allI}). \begin{isabelle} %{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x\ \isasymLongrightarrow\ P\ %\isasymlongrightarrow\ ({\isasymforall}x.\ Q\ x)\isanewline \ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x;\ P\isasymrbrakk\ \isasymLongrightarrow\ Q\ x \end{isabelle} As before, it replaces the HOL quantifier by a meta-level quantifier, producing a subgoal that binds the variable~\bigisa{x}. The leading bound variables (here \isa{x}) and the assumptions (here \isa{{\isasymforall}x.\ P\ \isasymlongrightarrow\ Q\ x} and \isa{P}) form the \textbf{context} for the conclusion, here \isa{Q\ x}. At each proof step, the subgoals inherit the previous context, though some context elements may be added or deleted. Applying \isa{erule} deletes an assumption, while many natural deduction rules add bound variables or assumptions. Now, to reason from the universally quantified assumption, we apply the elimination rule using the {\isa{drule}} method. This rule is called \isa{spec} because it specializes a universal formula to a particular term. \begin{isabelle} \ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ P\ \isasymlongrightarrow\ Q\ (?x2\ x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x \end{isabelle} Observe how the context has changed. The quantified formula is gone, replaced by a new assumption derived from its body. Informally, we have removed the quantifier. The quantified variable has been replaced by the curious term \bigisa{?x2~x}; it acts as a placeholder that may be replaced by any term that can be built up from~\bigisa{x}. (Formally, \bigisa{?x2} is an unknown of function type, applied to the argument~\bigisa{x}.) This new assumption is an implication, so we can use \emph{modus ponens} on it. As before, it requires proving the antecedent (in this case \isa{P}) and leaves us with the consequent. \begin{isabelle} \ 1.\ {\isasymAnd}x.\ {\isasymlbrakk}P;\ Q\ (?x2\ x){\isasymrbrakk}\ \isasymLongrightarrow\ Q\ x \end{isabelle} The consequent is \isa{Q} applied to that placeholder. It may be replaced by any term built from~\bigisa{x}, and here it should simply be~\bigisa{x}. The \isa{assumption} method will do this. The assumption need not be identical to the conclusion, provided the two formulas are unifiable. \medskip Note that \isa{drule spec} removes the universal quantifier and --- as usual with elimination rules --- discards the original formula. Sometimes, a universal formula has to be kept so that it can be used again. Then we use a new method: \isa{frule}. It acts like \isa{drule} but copies rather than replaces the selected assumption. The \isa{f} is for `forward.' In this example, we intuitively see that to go from \isa{P\ a} to \isa{P(f\ (f\ a))} requires two uses of the quantified assumption, one for each additional~\isa{f}. \begin{isabelle} \isacommand{lemma}\ "\isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x); \ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P(f\ (f\ a))"\isanewline \isacommand{apply}\ (frule\ spec)\isanewline \isacommand{apply}\ (drule\ mp,\ assumption)\isanewline \isacommand{apply}\ (drule\ spec)\isanewline \isacommand{apply}\ (drule\ mp,\ assumption,\ assumption)\isanewline \isacommand{done} \end{isabelle} % Applying \isa{frule\ spec} leaves this subgoal: \begin{isabelle} \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ ?x\ \isasymlongrightarrow\ P\ (f\ ?x)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a)) \end{isabelle} It is just what \isa{drule} would have left except that the quantified assumption is still present. The next step is to apply \isa{mp} to the implication and the assumption \isa{P\ a}, which leaves this subgoal: \begin{isabelle} \ 1.\ \isasymlbrakk{\isasymforall}x.\ P\ x\ \isasymlongrightarrow\ P\ (f\ x);\ P\ a;\ P\ (f\ a)\isasymrbrakk\ \isasymLongrightarrow\ P\ (f\ (f\ a)) \end{isabelle} % We have created the assumption \isa{P(f\ a)}, which is progress. To finish the proof, we apply \isa{spec} one last time, using \isa{drule}. One final trick: if we then apply \begin{isabelle} \ \ \ \ \ (drule\ mp,\ assumption) \end{isabelle} it will add a second copy of \isa{P(f\ a)} instead of the desired \isa{P(f\ (f\ a))}. Bundling both \isa{assumption} calls with \isa{drule mp} causes Isabelle to backtrack and find the correct one. \section{The existential quantifier} The concepts just presented also apply to the existential quantifier, whose introduction rule looks like this in Isabelle: \begin{isabelle} ?P\ ?x\ \isasymLongrightarrow\ {\isasymexists}x.\ ?P\ x\rulename{exI} \end{isabelle} If we can exhibit some $x$ such that $P(x)$ is true, then $\exists x. P(x)$ is also true. It is essentially a dual of the universal elimination rule, and logic texts present it using the same notation for substitution. The existential elimination rule looks like this in a logic text: \[ \infer{R}{\exists x.\,P & \infer*{R}{[P]}} \] % It looks like this in Isabelle: \begin{isabelle} \isasymlbrakk{\isasymexists}x.\ ?P\ x;\ {\isasymAnd}x.\ ?P\ x\ \isasymLongrightarrow\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?Q\rulename{exE} \end{isabelle} % Given an existentially quantified theorem and some formula $Q$ to prove, it creates a new assumption by removing the quantifier. As with the universal introduction rule, the textbook version imposes a proviso on the quantified variable, which Isabelle expresses using its meta-logic. Note that it is enough to have a universal quantifier in the meta-logic; we do not need an existential quantifier to be built in as well.\REMARK{EX example needed?} Isabelle/HOL also provides Hilbert's $\epsilon$-operator. The term $\epsilon x. P(x)$ denotes some $x$ such that $P(x)$ is true, provided such a value exists. Using this operator, we can express an existential destruction rule: \[ \infer{P[(\epsilon x. P) / \, x]}{\exists x.\,P} \] This rule is seldom used, for it can cause exponential blow-up. The main use of $\epsilon x. P(x)$ is in definitions when $P(x)$ characterizes $x$ uniquely. For instance, we can define the cardinality of a finite set~$A$ to be that $n$ such that $A$ is in one-to-one correspondence with $\{1,\ldots,n\}$. We can then prove that the cardinality of the empty set is zero (since $n=0$ satisfies the description) and proceed to prove other facts.\REMARK{SOME theorems and example} \begin{exercise} Prove the lemma \[ \exists x.\, P\conj Q(x)\Imp P\conj(\exists x.\, Q(x)). \] \emph{Hint}: the proof is similar to the one just above for the universal quantifier. \end{exercise} \section{Some proofs that fail} Most of the examples in this tutorial involve proving theorems. But not every conjecture is true, and it can be instructive to see how proofs fail. Here we attempt to prove a distributive law involving the existential quantifier and conjunction. \begin{isabelle} \isacommand{lemma}\ "({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x"\isanewline \isacommand{apply}\ (erule\ conjE)\isanewline \isacommand{apply}\ (erule\ exE)\isanewline \isacommand{apply}\ (erule\ exE)\isanewline \isacommand{apply}\ (rule\ exI)\isanewline \isacommand{apply}\ (rule\ conjI)\isanewline \ \isacommand{apply}\ assumption\isanewline \isacommand{oops} \end{isabelle} The first steps are routine. We apply conjunction elimination (\isa{erule conjE}) to split the assumption in two, leaving two existentially quantified assumptions. Applying existential elimination (\isa{erule exE}) removes one of the quantifiers. \begin{isabelle} %({\isasymexists}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ %\isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x\isanewline \ 1.\ {\isasymAnd}x.\ \isasymlbrakk{\isasymexists}x.\ Q\ x;\ P\ x\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x \end{isabelle} % When we remove the other quantifier, we get a different bound variable in the subgoal. (The name \isa{xa} is generated automatically.) \begin{isabelle} \ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ {\isasymexists}x.\ P\ x\ \isasymand\ Q\ x \end{isabelle} The proviso of the existential elimination rule has forced the variables to differ: we can hardly expect two arbitrary values to be equal! There is no way to prove this subgoal. Removing the conclusion's existential quantifier yields two identical placeholders, which can become any term involving the variables \bigisa{x} and~\bigisa{xa}. We need one to become \bigisa{x} and the other to become~\bigisa{xa}, but Isabelle requires all instances of a placeholder to be identical. \begin{isabelle} \ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ P\ (?x3\ x\ xa)\isanewline \ 2.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ (?x3\ x\ xa) \end{isabelle} We can prove either subgoal using the \isa{assumption} method. If we prove the first one, the placeholder changes into~\bigisa{x}. \begin{isabelle} \ 1.\ {\isasymAnd}x\ xa.\ {\isasymlbrakk}P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ Q\ x \end{isabelle} We are left with a subgoal that cannot be proved, because there is no way to prove that \bigisa{x} equals~\bigisa{xa}. Applying the \isa{assumption} method results in an error message: \begin{isabelle} *** empty result sequence -- proof command failed \end{isabelle} We can tell Isabelle to abandon a failed proof using the \isacommand{oops} command. \medskip Here is another abortive proof, illustrating the interaction between bound variables and unknowns. If $R$ is a reflexive relation, is there an $x$ such that $R\,x\,y$ holds for all $y$? Let us see what happens when we attempt to prove it. \begin{isabelle} \isacommand{lemma}\ "{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\ {\isasymforall}y.\ R\ x\ y"\isanewline \isacommand{apply}\ (rule\ exI)\isanewline \isacommand{apply}\ (rule\ allI)\isanewline \isacommand{apply}\ (drule\ spec)\isanewline \isacommand{oops} \end{isabelle} First, we remove the existential quantifier. The new proof state has an unknown, namely~\bigisa{?x}. \begin{isabelle} %{\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymexists}x.\ %{\isasymforall}y.\ R\ x\ y\isanewline \ 1.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ {\isasymforall}y.\ R\ ?x\ y \end{isabelle} Next, we remove the universal quantifier from the conclusion, putting the bound variable~\isa{y} into the subgoal. \begin{isabelle} \ 1.\ {\isasymAnd}y.\ {\isasymforall}z.\ R\ z\ z\ \isasymLongrightarrow\ R\ ?x\ y \end{isabelle} Finally, we try to apply our reflexivity assumption. We obtain a new assumption whose identical placeholders may be replaced by any term involving~\bigisa{y}. \begin{isabelle} \ 1.\ {\isasymAnd}y.\ R\ (?z2\ y)\ (?z2\ y)\ \isasymLongrightarrow\ R\ ?x\ y \end{isabelle} This subgoal can only be proved by putting \bigisa{y} for all the placeholders, making the assumption and conclusion become \isa{R\ y\ y}. But Isabelle refuses to substitute \bigisa{y}, a bound variable, for \bigisa{?x}; that would be a bound variable capture. The proof fails. Note that Isabelle can replace \bigisa{?z2~y} by \bigisa{y}; this involves instantiating \bigisa{?z2} to the identity function. This example is typical of how Isabelle enforces sound quantifier reasoning. \section{Proving theorems using the {\tt\slshape blast} method} It is hard to prove substantial theorems using the methods described above. A proof may be dozens or hundreds of steps long. You may need to search among different ways of proving certain subgoals. Often a choice that proves one subgoal renders another impossible to prove. There are further complications that we have not discussed, concerning negation and disjunction. Isabelle's \textbf{classical reasoner} is a family of tools that perform such proofs automatically. The most important of these is the {\isa{blast}} method. In this section, we shall first see how to use the classical reasoner in its default mode and then how to insert additional rules, enabling it to work in new problem domains. We begin with examples from pure predicate logic. The following example is known as Andrew's challenge. Peter Andrews designed it to be hard to prove by automatic means.% \footnote{Pelletier~\cite{pelletier86} describes it and many other problems for automatic theorem provers.} The nested biconditionals cause an exponential explosion: the formal proof is enormous. However, the {\isa{blast}} method proves it in a fraction of a second. \begin{isabelle} \isacommand{lemma}\ "(({\isasymexists}x.\ {\isasymforall}y.\ p(x){=}p(y))\ =\ (({\isasymexists}x.\ q(x))=({\isasymforall}y.\ p(y))))\ \ \ =\ \ \ \ \isanewline \ \ \ \ \ \ \ \ (({\isasymexists}x.\ {\isasymforall}y.\ q(x){=}q(y))\ =\ (({\isasymexists}x.\ p(x))=({\isasymforall}y.\ q(y))))"\isanewline \isacommand{apply}\ blast\isanewline \isacommand{done} \end{isabelle} The next example is a logic problem composed by Lewis Carroll. The {\isa{blast}} method finds it trivial. Moreover, it turns out that not all of the assumptions are necessary. We can easily experiment with variations of this formula and see which ones can be proved. \begin{isabelle} \isacommand{lemma}\ "({\isasymforall}x.\ honest(x)\ \isasymand\ industrious(x)\ \isasymlongrightarrow\ healthy(x))\ \isasymand\ \ \isanewline \ \ \ \ \ \ \ \ \isasymnot\ ({\isasymexists}x.\ grocer(x)\ \isasymand\ healthy(x))\ \isasymand\ \isanewline \ \ \ \ \ \ \ \ ({\isasymforall}x.\ industrious(x)\ \isasymand\ grocer(x)\ \isasymlongrightarrow\ honest(x))\ \isasymand\ \isanewline \ \ \ \ \ \ \ \ ({\isasymforall}x.\ cyclist(x)\ \isasymlongrightarrow\ industrious(x))\ \isasymand\ \isanewline \ \ \ \ \ \ \ \ ({\isasymforall}x.\ {\isasymnot}healthy(x)\ \isasymand\ cyclist(x)\ \isasymlongrightarrow\ {\isasymnot}honest(x))\ \ \isanewline \ \ \ \ \ \ \ \ \isasymlongrightarrow\ ({\isasymforall}x.\ grocer(x)\ \isasymlongrightarrow\ {\isasymnot}cyclist(x))"\isanewline \isacommand{apply}\ blast\isanewline \isacommand{done} \end{isabelle} The {\isa{blast}} method is also effective for set theory, which is described in the next chapter. This formula below may look horrible, but the \isa{blast} method proves it easily. \begin{isabelle} \isacommand{lemma}\ "({\isasymUnion}i{\isasymin}I.\ A(i))\ \isasyminter\ ({\isasymUnion}j{\isasymin}J.\ B(j))\ =\isanewline \ \ \ \ \ \ \ \ ({\isasymUnion}i{\isasymin}I.\ {\isasymUnion}j{\isasymin}J.\ A(i)\ \isasyminter\ B(j))"\isanewline \isacommand{apply}\ blast\isanewline \isacommand{done} \end{isabelle} Few subgoals are couched purely in predicate logic and set theory. We can extend the scope of the classical reasoner by giving it new rules. Extending it effectively requires understanding the notions of introduction, elimination and destruction rules. Moreover, there is a distinction between safe and unsafe rules. A \textbf{safe} rule is one that can be applied backwards without losing information; an \textbf{unsafe} rule loses information, perhaps transforming the subgoal into one that cannot be proved. The safe/unsafe distinction affects the proof search: if a proof attempt fails, the classical reasoner backtracks to the most recent unsafe rule application and makes another choice. An important special case avoids all these complications. A logical equivalence, which in higher-order logic is an equality between formulas, can be given to the classical reasoner and simplifier by using the attribute {\isa{iff}}. You should do so if the right hand side of the equivalence is simpler than the left-hand side. For example, here is a simple fact about list concatenation. The result of appending two lists is empty if and only if both of the lists are themselves empty. Obviously, applying this equivalence will result in a simpler goal. When stating this lemma, we include the {\isa{iff}} attribute. Once we have proved the lemma, Isabelle will make it known to the classical reasoner (and to the simplifier). \begin{isabelle} \isacommand{lemma}\ [iff]:\ "(xs{\isacharat}ys\ =\ \isacharbrackleft{]})\ =\ (xs=[]\ \isacharampersand\ ys=[])"\isanewline \isacommand{apply}\ (induct_tac\ xs)\isanewline \isacommand{apply}\ (simp_all) \isanewline \isacommand{done} \end{isabelle} % This fact about multiplication is also appropriate for the {\isa{iff}} attribute:\REMARK{the ?s are ugly here but we need them again when talking about \isa{of}; we need a consistent style} \begin{isabelle} (\mbox{?m}\ \isacharasterisk\ \mbox{?n}\ =\ 0)\ =\ (\mbox{?m}\ =\ 0\ \isasymor\ \mbox{?n}\ =\ 0) \end{isabelle} A product is zero if and only if one of the factors is zero. The reasoning involves a logical \textsc{or}. Proving new rules for disjunctive reasoning is hard, but translating to an actual disjunction works: the classical reasoner handles disjunction properly. In more detail, this is how the {\isa{iff}} attribute works. It converts the equivalence $P=Q$ to a pair of rules: the introduction rule $Q\Imp P$ and the destruction rule $P\Imp Q$. It gives both to the classical reasoner as safe rules, ensuring that all occurrences of $P$ in a subgoal are replaced by~$Q$. The simplifier performs the same replacement, since \isa{iff} gives $P=Q$ to the simplifier. But classical reasoning is different from simplification. Simplification is deterministic: it applies rewrite rules repeatedly, as long as possible, in order to \emph{transform} a goal. Classical reasoning uses search and backtracking in order to \emph{prove} a goal. \section{Proving the correctness of Euclid's algorithm} \label{sec:proving-euclid} A brief development will illustrate advanced use of \isa{blast}. In \S\ref{sec:recdef-simplification}, we declared the recursive function {\isa{gcd}}: \begin{isabelle} \isacommand{consts}\ gcd\ ::\ "nat{\isacharasterisk}nat\ \isasymRightarrow\ nat"\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \isanewline \isacommand{recdef}\ gcd\ "measure\ ((\isasymlambda(m,n).n)\ ::nat{\isacharasterisk}nat\ \isasymRightarrow\ nat)"\isanewline \ \ \ \ "gcd\ (m,n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n))" \end{isabelle} Let us prove that it computes the greatest common divisor of its two arguments. % %The declaration yields a recursion %equation for {\isa{gcd}}. Simplifying with this equation can %cause looping, expanding to ever-larger expressions of if-then-else %and {\isa{gcd}} calls. To prevent this, we prove separate simplification rules %for $n=0$\ldots %\begin{isabelle} %\isacommand{lemma}\ gcd_0\ [simp]:\ "gcd(m,0)\ =\ m"\isanewline %\isacommand{apply}\ (simp)\isanewline %\isacommand{done} %\end{isabelle} %\ldots{} and for $n>0$: %\begin{isabelle} %\isacommand{lemma}\ gcd_non_0:\ "0{\isacharless}n\ \isasymLongrightarrow\ gcd(m,n)\ =\ gcd\ (n,\ m\ mod\ n)"\isanewline %\isacommand{apply}\ (simp)\isanewline %\isacommand{done} %\end{isabelle} %This second rule is similar to the original equation but %does not loop because it is conditional. It can be applied only %when the second argument is known to be non-zero. %Armed with our two new simplification rules, we now delete the %original {\isa{gcd}} recursion equation. %\begin{isabelle} %\isacommand{declare}\ gcd.simps\ [simp\ del] %\end{isabelle} % %Now we can prove some interesting facts about the {\isa{gcd}} function, %for exampe, that it computes a common divisor of its arguments. % The theorem is expressed in terms of the familiar \textbf{divides} relation from number theory: \begin{isabelle} ?m\ dvd\ ?n\ \isasymequiv\ {\isasymexists}k.\ ?n\ =\ ?m\ \isacharasterisk\ k \rulename{dvd_def} \end{isabelle} % A simple induction proves the theorem. Here \isa{gcd.induct} refers to the induction rule returned by \isa{recdef}. The proof relies on the simplification rules proved in \S\ref{sec:recdef-simplification}, since rewriting by the definition of \isa{gcd} can cause looping. \begin{isabelle} \isacommand{lemma}\ gcd_dvd_both:\ "(gcd(m,n)\ dvd\ m)\ \isasymand\ (gcd(m,n)\ dvd\ n)"\isanewline \isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline \isacommand{apply}\ (case_tac\ "n=0")\isanewline \isacommand{apply}\ (simp_all)\isanewline \isacommand{apply}\ (blast\ dest:\ dvd_mod_imp_dvd)\isanewline \isacommand{done}% \end{isabelle} Notice that the induction formula is a conjunction. This is necessary: in the inductive step, each half of the conjunction establishes the other. The first three proof steps are applying induction, performing a case analysis on \isa{n}, and simplifying. Let us pass over these quickly and consider the use of {\isa{blast}}. We have reached the following subgoal: \begin{isabelle} %gcd\ (m,\ n)\ dvd\ m\ \isasymand\ gcd\ (m,\ n)\ dvd\ n\isanewline \ 1.\ {\isasymAnd}m\ n.\ \isasymlbrakk0\ \isacharless\ n;\isanewline \ \ \ \ \ \ \ \ \ \ \ \ gcd\ (n,\ m\ mod\ n)\ dvd\ n\ \isasymand\ gcd\ (n,\ m\ mod\ n)\ dvd\ (m\ mod\ n){\isasymrbrakk}\isanewline \ \ \ \ \ \ \ \ \ \ \ \isasymLongrightarrow\ gcd\ (n,\ m\ mod\ n)\ dvd\ m \end{isabelle} % One of the assumptions, the induction hypothesis, is a conjunction. The two divides relationships it asserts are enough to prove the conclusion, for we have the following theorem at our disposal: \begin{isabelle} \isasymlbrakk?k\ dvd\ (?m\ mod\ ?n){;}\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ ?m% \rulename{dvd_mod_imp_dvd} \end{isabelle} % This theorem can be applied in various ways. As an introduction rule, it would cause backward chaining from the conclusion (namely \isa{?k\ dvd\ ?m}) to the two premises, which also involve the divides relation. This process does not look promising and could easily loop. More sensible is to apply the rule in the forward direction; each step would eliminate the \isa{mod} symbol from an assumption, so the process must terminate. So the final proof step applies the \isa{blast} method. Attaching the {\isa{dest}} attribute to \isa{dvd_mod_imp_dvd} tells \isa{blast} to use it as destruction rule: in the forward direction. \medskip We have proved a conjunction. Now, let us give names to each of the two halves: \begin{isabelle} \isacommand{lemmas}\ gcd_dvd1\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct1]\isanewline \isacommand{lemmas}\ gcd_dvd2\ [iff]\ =\ gcd_dvd_both\ [THEN\ conjunct2]% \end{isabelle} Several things are happening here. The keyword \isacommand{lemmas} tells Isabelle to transform a theorem in some way and to give a name to the resulting theorem. Attributes can be given, here \isa{iff}, which supplies the new theorems to the classical reasoner and the simplifier. The directive {\isa{THEN}}, which will be explained below, supplies the lemma \isa{gcd_dvd_both} to the destruction rule \isa{conjunct1} in order to extract the first part. \begin{isabelle} \ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?m1% \end{isabelle} The variable names \isa{?m1} and \isa{?n1} arise because Isabelle renames schematic variables to prevent clashes. The second \isacommand{lemmas} declaration yields \begin{isabelle} \ \ \ \ \ gcd\ (?m1,\ ?n1)\ dvd\ ?n1% \end{isabelle} Later, we shall explore this type of forward reasoning in detail. To complete the verification of the {\isa{gcd}} function, we must prove that it returns the greatest of all the common divisors of its arguments. The proof is by induction and simplification. \begin{isabelle} \isacommand{lemma}\ gcd_greatest\ [rule_format]:\isanewline \ \ \ \ \ \ \ "(k\ dvd\ m)\ \isasymlongrightarrow\ (k\ dvd\ n)\ \isasymlongrightarrow\ k\ dvd\ gcd(m,n)"\isanewline \isacommand{apply}\ (induct_tac\ m\ n\ rule:\ gcd.induct)\isanewline \isacommand{apply}\ (case_tac\ "n=0")\isanewline \isacommand{apply}\ (simp_all\ add:\ gcd_non_0\ dvd_mod)\isanewline \isacommand{done} \end{isabelle} % Note that the theorem has been expressed using HOL implication, \isa{\isasymlongrightarrow}, because the induction affects the two preconditions. The directive \isa{rule_format} tells Isabelle to replace each \isa{\isasymlongrightarrow} by \isa{\isasymLongrightarrow} before storing the theorem we have proved. This directive also removes outer universal quantifiers, converting a theorem into the usual format for inference rules. The facts proved above can be summarized as a single logical equivalence. This step gives us a chance to see another application of \isa{blast}, and it is worth doing for sound logical reasons. \begin{isabelle} \isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline \ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m,n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline \isacommand{apply}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)\isanewline \isacommand{done} \end{isabelle} This theorem concisely expresses the correctness of the {\isa{gcd}} function. We state it with the {\isa{iff}} attribute so that Isabelle can use it to remove some occurrences of {\isa{gcd}}. The theorem has a one-line proof using {\isa{blast}} supplied with four introduction rules: note the {\isa{intro}} attribute. The exclamation mark ({\isa{intro}}{\isa{!}})\ signifies safe rules, which are applied aggressively. Rules given without the exclamation mark are applied reluctantly and their uses can be undone if the search backtracks. Here the unsafe rule expresses transitivity of the divides relation: \begin{isabelle} \isasymlbrakk?m\ dvd\ ?n;\ ?n\ dvd\ ?p\isasymrbrakk\ \isasymLongrightarrow\ ?m\ dvd\ ?p% \rulename{dvd_trans} \end{isabelle} Applying \isa{dvd_trans} as an introduction rule entails a risk of looping, for it multiplies occurrences of the divides symbol. However, this proof relies on transitivity reasoning. The rule {\isa{gcd\_greatest}} is safe to apply aggressively because it yields simpler subgoals. The proof implicitly uses \isa{gcd_dvd1} and \isa{gcd_dvd2} as safe rules, because they were declared using \isa{iff}. \section{Other classical reasoning methods} The {\isa{blast}} method is our main workhorse for proving theorems automatically. Other components of the classical reasoner interact with the simplifier. Still others perform classical reasoning to a limited extent, giving the user fine control over the proof. Of the latter methods, the most useful is {\isa{clarify}}. It performs all obvious reasoning steps without splitting the goal into multiple parts. It does not apply rules that could render the goal unprovable (so-called unsafe rules). By performing the obvious steps, {\isa{clarify}} lays bare the difficult parts of the problem, where human intervention is necessary. For example, the following conjecture is false: \begin{isabelle} \isacommand{lemma}\ "({\isasymforall}x.\ P\ x)\ \isasymand\ ({\isasymexists}x.\ Q\ x)\ \isasymlongrightarrow\ ({\isasymforall}x.\ P\ x\ \isasymand\ Q\ x)"\isanewline \isacommand{apply}\ clarify \end{isabelle} The {\isa{blast}} method would simply fail, but {\isa{clarify}} presents a subgoal that helps us see why we cannot continue the proof. \begin{isabelle} \ 1.\ {\isasymAnd}x\ xa.\ \isasymlbrakk{\isasymforall}x.\ P\ x;\ Q\ xa\isasymrbrakk\ \isasymLongrightarrow\ P\ x\ \isasymand\ Q\ x \end{isabelle} The proof must fail because the assumption \isa{Q\ xa} and conclusion \isa{Q\ x} refer to distinct bound variables. To reach this state, \isa{clarify} applied the introduction rules for \isa{\isasymlongrightarrow} and \isa{\isasymforall} and the elimination rule for ~\isa{\isasymand}. It did not apply the introduction rule for \isa{\isasymand} because of its policy never to split goals. Also available is {\isa{clarsimp}}, a method that interleaves {\isa{clarify}} and {\isa{simp}}. Also there is \isa{safe}, which like \isa{clarify} performs obvious steps and even applies those that split goals. The \isa{force} method applies the classical reasoner and simplifier to one goal. \REMARK{example needed of \isa{force}?} Unless it can prove the goal, it fails. Contrast that with the \isa{auto} method, which also combines classical reasoning with simplification. The latter's purpose is to prove all the easy subgoals and parts of subgoals. Unfortunately, it can produce large numbers of new subgoals; also, since it proves some subgoals and splits others, it obscures the structure of the proof tree. The \isa{force} method does not have these drawbacks. Another difference: \isa{force} tries harder than {\isa{auto}} to prove its goal, so it can take much longer to terminate. Older components of the classical reasoner have largely been superseded by {\isa{blast}}, but they still have niche applications. Most important among these are {\isa{fast}} and {\isa{best}}. While {\isa{blast}} searches for proofs using a built-in first-order reasoner, these earlier methods search for proofs using standard Isabelle inference. That makes them slower but enables them to work correctly in the presence of the more unusual features of Isabelle rules, such as type classes and function unknowns. For example, the introduction rule for Hilbert's epsilon-operator has the following form: \begin{isabelle} ?P\ ?x\ \isasymLongrightarrow\ ?P\ (SOME\ x.\ ?P x) \rulename{someI} \end{isabelle} The repeated occurrence of the variable \isa{?P} makes this rule tricky to apply. Consider this contrived example: \begin{isabelle} \isacommand{lemma}\ "{\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\isanewline \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ P\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)\ \isasymand\ Q\ (SOME\ x.\ P\ x\ \isasymand\ Q\ x)"\isanewline \isacommand{apply}\ (rule\ someI) \end{isabelle} % We can apply rule \isa{someI} explicitly. It yields the following subgoal: \begin{isabelle} \ 1.\ {\isasymlbrakk}Q\ a;\ P\ a\isasymrbrakk\ \isasymLongrightarrow\ P\ ?x\ \isasymand\ Q\ ?x% \end{isabelle} The proof from this point is trivial. The question now arises, could we have proved the theorem with a single command? Not using {\isa{blast}} method: it cannot perform the higher-order unification that is necessary here. The {\isa{fast}} method succeeds: \begin{isabelle} \isacommand{apply}\ (fast\ intro!:\ someI) \end{isabelle} The {\isa{best}} method is similar to {\isa{fast}} but it uses a best-first search instead of depth-first search. Accordingly, it is slower but is less susceptible to divergence. Transitivity rules usually cause {\isa{fast}} to loop where often {\isa{best}} can manage. Here is a summary of the classical reasoning methods: \begin{itemize} \item \isa{blast} works automatically and is the fastest \item \isa{clarify} and \isa{clarsimp} perform obvious steps without splitting the goal; \isa{safe} even splits goals \item \isa{force} uses classical reasoning and simplification to prove a goal; \isa{auto} is similar but leaves what it cannot prove \item \isa{fast} and \isa{best} are legacy methods that work well with rules involving unusual features \end{itemize} A table illustrates the relationships among four of these methods. \begin{center} \begin{tabular}{r|l|l|} & no split & split \\ \hline no simp & \isa{clarify} & \isa{safe} \\ \hline simp & \isa{clarsimp} & \isa{auto} \\ \hline \end{tabular} \end{center} \section{Forward proof}\label{sec:forward} Forward proof means deriving new facts from old ones. It is the most fundamental type of proof. Backward proof, by working from goals to subgoals, can help us find a difficult proof. But it is not always the best way of presenting the proof so found. Forward proof is particularly good for reasoning from the general to the specific. For example, consider the following distributive law for the \isa{gcd} function: \[ k\times\gcd(m,n) = \gcd(k\times m,k\times n)\] Putting $m=1$ we get (since $\gcd(1,n)=1$ and $k\times1=k$) \[ k = \gcd(k,k\times n)\] We have derived a new fact about \isa{gcd}; if re-oriented, it might be useful for simplification. After re-orienting it and putting $n=1$, we derive another useful law: \[ \gcd(k,k)=k \] Substituting values for variables --- instantiation --- is a forward step. Re-orientation works by applying the symmetry of equality to an equation, so it too is a forward step. Now let us reproduce our examples in Isabelle. Here is the distributive law: \begin{isabelle}% ?k\ \isacharasterisk\ gcd\ (?m,\ ?n)\ =\ gcd\ (?k\ \isacharasterisk\ ?m,\ ?k\ \isacharasterisk\ ?n) \rulename{gcd_mult_distrib2} \end{isabelle}% The first step is to replace \isa{?m} by~1 in this law. We refer to the variables not by name but by their position in the theorem, from left to right. In this case, the variables are \isa{?k}, \isa{?m} and~\isa{?n}. So, the expression \hbox{\texttt{[of k 1]}} replaces \isa{?k} by~\isa{k} and \isa{?m} by~\isa{1}. \begin{isabelle} \isacommand{lemmas}\ gcd_mult_0\ =\ gcd_mult_distrib2\ [of\ k\ 1] \end{isabelle} % The command \isa{thm gcd_mult_0} displays the resulting theorem: \begin{isabelle} \ \ \ \ \ k\ \isacharasterisk\ gcd\ (1,\ ?n)\ =\ gcd\ (k\ \isacharasterisk\ 1,\ k\ \isacharasterisk\ ?n) \end{isabelle} Something is odd: {\isa{k}} is an ordinary variable, while {\isa{?n}} is schematic. We did not specify an instantiation for {\isa{?n}}. In its present form, the theorem does not allow substitution for {\isa{k}}. One solution is to avoid giving an instantiation for \isa{?k}: instead of a term we can put an underscore~(\isa{_}). For example, \begin{isabelle} \ \ \ \ \ gcd_mult_distrib2\ [of\ _\ 1] \end{isabelle} replaces \isa{?m} by~\isa{1} but leaves \isa{?k} unchanged. Anyway, let us put the theorem \isa{gcd_mult_0} into a simplified form: \begin{isabelle} \isacommand{lemmas}\ gcd_mult_1\ =\ gcd_mult_0\ [simplified]% \end{isabelle} % Again, we display the resulting theorem: \begin{isabelle} \ \ \ \ \ k\ =\ gcd\ (k,\ k\ \isacharasterisk\ ?n) \end{isabelle} % To re-orient the equation requires the symmetry rule: \begin{isabelle} ?s\ =\ ?t\ \isasymLongrightarrow\ ?t\ =\ ?s% \rulename{sym} \end{isabelle} The following declaration gives our equation to \isa{sym}: \begin{isabelle} \ \ \ \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_1\ [THEN\ sym] \end{isabelle} % Here is the result: \begin{isabelle} \ \ \ \ \ gcd\ (k,\ k\ \isacharasterisk\ ?n)\ =\ k% \end{isabelle} \isa{THEN~sym} gives the current theorem to the rule \isa{sym} and returns the resulting conclusion.\REMARK{figure necessary?} The effect is to exchange the two operands of the equality. Typically {\isa{THEN}} is used with destruction rules. Above we have used \isa{THEN~conjunct1} to extract the first part of the theorem \isa{gcd_dvd_both}. Also useful is \isa{THEN~spec}, which removes the quantifier from a theorem of the form $\forall x.\,P$, and \isa{THEN~mp}, which converts the implication $P\imp Q$ into the rule $\vcenter{\infer{Q}{P}}$. Similar to \isa{mp} are the following two rules, which extract the two directions of reasoning about a boolean equivalence: \begin{isabelle} \isasymlbrakk?Q\ =\ ?P;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% \rulename{iffD1}% \isanewline \isasymlbrakk?P\ =\ ?Q;\ ?Q\isasymrbrakk\ \isasymLongrightarrow\ ?P% \rulename{iffD2} \end{isabelle} % Normally we would never name the intermediate theorems such as \isa{gcd_mult_0} and \isa{gcd_mult_1} but would combine the three forward steps: \begin{isabelle} \isacommand{lemmas}\ gcd_mult\ =\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym]% \end{isabelle} The directives, or attributes, are processed from left to right. This declaration of \isa{gcd_mult} is equivalent to the previous one. Such declarations can make the proof script hard to read: what is being proved? More legible is to state the new lemma explicitly and to prove it using a single \isa{rule} method whose operand is expressed using forward reasoning: \begin{isabelle} \isacommand{lemma}\ gcd_mult\ [simp]:\ "gcd(k,\ k{\isacharasterisk}n)\ =\ k"\isanewline \isacommand{apply}\ (rule\ gcd_mult_distrib2\ [of\ k\ 1,\ simplified,\ THEN\ sym])\isanewline \isacommand{done} \end{isabelle} Compared with the previous proof of \isa{gcd_mult}, this version shows the reader what has been proved. Also, it receives the usual Isabelle treatment. In particular, Isabelle generalizes over all variables: the resulting theorem will have {\isa{?k}} instead of {\isa{k}}. At the start of this section, we also saw a proof of $\gcd(k,k)=k$. Here is the Isabelle version: \begin{isabelle} \isacommand{lemma}\ gcd_self\ [simp]:\ "gcd(k,k)\ =\ k"\isanewline \isacommand{apply}\ (rule\ gcd_mult\ [of\ k\ 1,\ simplified])\isanewline \isacommand{done} \end{isabelle} Recall that \isa{of} generates an instance of a rule by specifying values for its variables. Analogous is \isa{OF}, which generates an instance of a rule by specifying facts for its premises. Let us try it with this rule: \begin{isabelle} {\isasymlbrakk}gcd(?k,?n){=}1;\ ?k\ dvd\ (?m * ?n){\isasymrbrakk}\ \isasymLongrightarrow\ ?k\ dvd\ ?m \rulename{relprime_dvd_mult} \end{isabelle} First, we prove an instance of its first premise: \begin{isabelle} \isacommand{lemma}\ relprime_20_81:\ "gcd(\#20,\#81)\ =\ 1"\isanewline \isacommand{apply}\ (simp\ add:\ gcd.simps)\isanewline \isacommand{done}% \end{isabelle} We have evaluated an application of the \isa{gcd} function by simplification. Expression evaluation is not guaranteed to terminate, and certainly is not efficient; Isabelle performs arithmetic operations by rewriting symbolic bit strings. Here, however, the simplification takes less than one second. We can specify this new lemma to {\isa{OF}}, generating an instance of \isa{relprime_dvd_mult}. The expression \begin{isabelle} \ \ \ \ \ relprime_dvd_mult [OF relprime_20_81] \end{isabelle} yields the theorem \begin{isabelle} \ \ \ \ \ \isacharhash20\ dvd\ (?m\ \isacharasterisk\ \isacharhash81)\ \isasymLongrightarrow\ \isacharhash20\ dvd\ ?m% \end{isabelle} % {\isa{OF}} takes any number of operands. Consider the following facts about the divides relation: \begin{isabelle} \isasymlbrakk?k\ dvd\ ?m;\ ?k\ dvd\ ?n\isasymrbrakk\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ \isacharplus\ ?n) \rulename{dvd_add}\isanewline ?m\ dvd\ ?m% \rulename{dvd_refl} \end{isabelle} Let us supply \isa{dvd_refl} for each of the premises of \isa{dvd_add}: \begin{isabelle} \ \ \ \ \ dvd_add [OF dvd_refl dvd_refl] \end{isabelle} Here is the theorem that we have expressed: \begin{isabelle} \ \ \ \ \ ?k\ dvd\ (?k\ \isacharplus\ ?k) \end{isabelle} As with \isa{of}, we can use the \isa{_} symbol to leave some positions unspecified: \begin{isabelle} \ \ \ \ \ dvd_add [OF _ dvd_refl] \end{isabelle} The result is \begin{isabelle} \ \ \ \ \ ?k\ dvd\ ?m\ \isasymLongrightarrow\ ?k\ dvd\ (?m\ \isacharplus\ ?k) \end{isabelle} You may have noticed that {\isa{THEN}} and {\isa{OF}} are based on the same idea, namely to combine two rules. They differ in the order of the combination and thus in their effect. We use \isa{THEN} typically with a destruction rule to extract a subformula of the current theorem. We use \isa{OF} with a list of facts to generate an instance of the current theorem. Here is a summary of the primitives for forward reasoning: \begin{itemize} \item {\isa{of}} instantiates the variables of a rule to a list of terms \item {\isa{OF}} applies a rule to a list of theorems \item {\isa{THEN}} gives a theorem to a named rule and returns the conclusion \end{itemize} \section{Methods for forward proof} We have seen that forward proof works well within a backward proof. Also in that spirit is the \isa{insert} method, which inserts a given theorem as a new assumption of the current subgoal. This already is a forward step; moreover, we may (as always when using a theorem) apply {\isa{of}}, {\isa{THEN}} and other directives. The new assumption can then be used to help prove the subgoal. For example, consider this theorem about the divides relation. Only the first proof step is given; it inserts the distributive law for \isa{gcd}. We specify its variables as shown. \begin{isabelle} \isacommand{lemma}\ relprime_dvd_mult:\isanewline \ \ \ \ \ \ \ "{\isasymlbrakk}\ gcd(k,n){=}1;\ k\ dvd\ (m*n)\ {\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\ m"\isanewline \isacommand{apply}\ (insert\ gcd_mult_distrib2\ [of\ m\ k\ n]) \end{isabelle} In the resulting subgoal, note how the equation has been inserted: \begin{isabelle} {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\ m\isanewline \ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline \ \ \ \ \ m\ \isacharasterisk\ gcd\ (k,\ n)\ =\ gcd\ (m\ \isacharasterisk\ k,\ m\ \isacharasterisk\ n){\isasymrbrakk}\isanewline \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m \end{isabelle} The next proof step, \isa{\isacommand{apply}(simp)}, utilizes the assumption \isa{gcd(k,n)\ =\ 1}. Here is the result: \begin{isabelle} {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){\isasymrbrakk}\ \isasymLongrightarrow\ k\ dvd\ m\isanewline \ 1.\ {\isasymlbrakk}gcd\ (k,\ n)\ =\ 1;\ k\ dvd\ (m\ \isacharasterisk\ n){;}\isanewline \ \ \ \ \ m\ =\ gcd\ (m\ \isacharasterisk\ k,\ m\ \isacharasterisk\ n){\isasymrbrakk}\isanewline \ \ \ \ \isasymLongrightarrow\ k\ dvd\ m \end{isabelle} Simplification has yielded an equation for \isa{m} that will be used to complete the proof. \medskip Here is another proof using \isa{insert}. \REMARK{Effect with unknowns?} Division and remainder obey a well-known law: \begin{isabelle} (?m\ div\ ?n)\ \isacharasterisk\ ?n\ \isacharplus\ ?m\ mod\ ?n\ =\ ?m \rulename{mod_div_equality} \end{isabelle} We refer to this law explicitly in the following proof: \begin{isabelle} \isacommand{lemma}\ div_mult_self_is_m:\ \isanewline \ \ \ \ \ \ "0{\isacharless}n\ \isasymLongrightarrow\ (m{\isacharasterisk}n)\ div\ n\ =\ (m::nat)"\isanewline \isacommand{apply}\ (insert\ mod_div_equality\ [of\ "m{\isacharasterisk}n"\ n])\isanewline \isacommand{apply}\ (simp)\isanewline \isacommand{done} \end{isabelle} The first step inserts the law, specifying \isa{m*n} and \isa{n} for its variables. Notice that non-trivial expressions must be enclosed in quotation marks. Here is the resulting subgoal, with its new assumption: \begin{isabelle} %0\ \isacharless\ n\ \isasymLongrightarrow\ (m\ %\isacharasterisk\ n)\ div\ n\ =\ m\isanewline \ 1.\ \isasymlbrakk0\ \isacharless\ n;\ \ (m\ \isacharasterisk\ n)\ div\ n\ \isacharasterisk\ n\ \isacharplus\ (m\ \isacharasterisk\ n)\ mod\ n\ =\ m\ \isacharasterisk\ n\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ (m\ \isacharasterisk\ n)\ div\ n\ =\ m \end{isabelle} Simplification reduces \isa{(m\ \isacharasterisk\ n)\ mod\ n} to zero. Then it cancels the factor~\isa{n} on both sides of the equation, proving the theorem. \medskip A similar method is {\isa{subgoal\_tac}}. Instead of inserting a theorem as an assumption, it inserts an arbitrary formula. This formula must be proved later as a separate subgoal. The idea is to claim that the formula holds on the basis of the current assumptions, to use this claim to complete the proof, and finally to justify the claim. It is a valuable means of giving the proof some structure. The explicit formula will be more readable than proof commands that yield that formula indirectly. Look at the following example. \begin{isabelle} \isacommand{lemma}\ "\isasymlbrakk(z::int)\ <\ \#37;\ \#66\ <\ \#2*z;\ z*z\ \isasymnoteq\ \#1225;\ Q(\#34);\ Q(\#36)\isasymrbrakk\isanewline \ \ \ \ \ \ \ \ \,\isasymLongrightarrow\ Q(z)"\isanewline \isacommand{apply}\ (subgoal_tac\ "z\ =\ \#34\ \isasymor\ z\ =\ \#36")\isanewline \isacommand{apply}\ blast\isanewline \isacommand{apply}\ (subgoal_tac\ "z\ \isasymnoteq\ \#35")\isanewline \isacommand{apply}\ arith\isanewline \isacommand{apply}\ force\isanewline \isacommand{done} \end{isabelle} Let us prove it informally. The first assumption tells us that \isa{z} is no greater than 36. The second tells us that \isa{z} is at least 34. The third assumption tells us that \isa{z} cannot be 35, since $35\times35=1225$. So \isa{z} is either 34 or 36, and since \isa{Q} holds for both of those values, we have the conclusion. The Isabelle proof closely follows this reasoning. The first step is to claim that \isa{z} is either 34 or 36. The resulting proof state gives us two subgoals: \begin{isabelle} %{\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ %Q\ \#34;\ Q\ \#36\isasymrbrakk\ \isasymLongrightarrow\ Q\ z\isanewline \ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline \ \ \ \ \ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ Q\ z\isanewline \ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36 \end{isabelle} The first subgoal is trivial, but for the second Isabelle needs help to eliminate the case \isa{z}=35. The second invocation of {\isa{subgoal\_tac}} leaves two subgoals: \begin{isabelle} \ 1.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline \ \ \ \ \ z\ \isasymnoteq\ \#35\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ z\ =\ \#34\ \isasymor\ z\ =\ \#36\isanewline \ 2.\ {\isasymlbrakk}z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq\ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk\isanewline \ \ \ \ \isasymLongrightarrow\ z\ \isasymnoteq\ \#35 \end{isabelle} Assuming that \isa{z} is not 35, the first subgoal follows by linear arithmetic: the method {\isa{arith}}. For the second subgoal we apply the method \isa{force}, which proceeds by assuming that \isa{z}=35 and arriving at a contradiction. \medskip Summary of these methods: \begin{itemize} \item {\isa{insert}} adds a theorem as a new assumption \item {\isa{subgoal_tac}} adds a formula as a new assumption and leaves the subgoal of proving that formula \end{itemize}