diff -r f51d4a302962 -r 5386df44a037 src/Doc/ProgProve/Isar.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Doc/ProgProve/Isar.thy Tue Aug 28 18:57:32 2012 +0200 @@ -0,0 +1,997 @@ +(*<*) +theory Isar +imports LaTeXsugar +begin +ML{* quick_and_dirty := true *} +(*>*) +text{* +Apply-scripts are unreadable and hard to maintain. The language of choice +for larger proofs is \concept{Isar}. The two key features of Isar are: +\begin{itemize} +\item It is structured, not linear. +\item It is readable without running it because +you need to state what you are proving at any given point. +\end{itemize} +Whereas apply-scripts are like assembly language programs, Isar proofs +are like structured programs with comments. A typical Isar proof looks like this: +*}text{* +\begin{tabular}{@ {}l} +\isacom{proof}\\ +\quad\isacom{assume} @{text"\""}$\mathit{formula}_0$@{text"\""}\\ +\quad\isacom{have} @{text"\""}$\mathit{formula}_1$@{text"\""} \quad\isacom{by} @{text simp}\\ +\quad\vdots\\ +\quad\isacom{have} @{text"\""}$\mathit{formula}_n$@{text"\""} \quad\isacom{by} @{text blast}\\ +\quad\isacom{show} @{text"\""}$\mathit{formula}_{n+1}$@{text"\""} \quad\isacom{by} @{text \}\\ +\isacom{qed} +\end{tabular} +*}text{* +It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$ +(provided each proof step succeeds). +The intermediate \isacom{have} statements are merely stepping stones +on the way towards the \isacom{show} statement that proves the actual +goal. In more detail, this is the Isar core syntax: +\medskip + +\begin{tabular}{@ {}lcl@ {}} +\textit{proof} &=& \isacom{by} \textit{method}\\ + &$\mid$& \isacom{proof} [\textit{method}] \ \textit{step}$^*$ \ \isacom{qed} +\end{tabular} +\medskip + +\begin{tabular}{@ {}lcl@ {}} +\textit{step} &=& \isacom{fix} \textit{variables} \\ + &$\mid$& \isacom{assume} \textit{proposition} \\ + &$\mid$& [\isacom{from} \textit{fact}$^+$] (\isacom{have} $\mid$ \isacom{show}) \ \textit{proposition} \ \textit{proof} +\end{tabular} +\medskip + +\begin{tabular}{@ {}lcl@ {}} +\textit{proposition} &=& [\textit{name}:] @{text"\""}\textit{formula}@{text"\""} +\end{tabular} +\medskip + +\begin{tabular}{@ {}lcl@ {}} +\textit{fact} &=& \textit{name} \ $\mid$ \ \dots +\end{tabular} +\medskip + +\noindent A proof can either be an atomic \isacom{by} with a single proof +method which must finish off the statement being proved, for example @{text +auto}. Or it can be a \isacom{proof}--\isacom{qed} block of multiple +steps. Such a block can optionally begin with a proof method that indicates +how to start off the proof, e.g.\ \mbox{@{text"(induction xs)"}}. + +A step either assumes a proposition or states a proposition +together with its proof. The optional \isacom{from} clause +indicates which facts are to be used in the proof. +Intermediate propositions are stated with \isacom{have}, the overall goal +with \isacom{show}. A step can also introduce new local variables with +\isacom{fix}. Logically, \isacom{fix} introduces @{text"\"}-quantified +variables, \isacom{assume} introduces the assumption of an implication +(@{text"\"}) and \isacom{have}/\isacom{show} the conclusion. + +Propositions are optionally named formulas. These names can be referred to in +later \isacom{from} clauses. In the simplest case, a fact is such a name. +But facts can also be composed with @{text OF} and @{text of} as shown in +\S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note +that assumptions, intermediate \isacom{have} statements and global lemmas all +have the same status and are thus collectively referred to as +\concept{facts}. + +Fact names can stand for whole lists of facts. For example, if @{text f} is +defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of +recursion equations defining @{text f}. Individual facts can be selected by +writing @{text"f.simps(2)"}, whole sublists by @{text"f.simps(2-4)"}. + + +\section{Isar by example} + +We show a number of proofs of Cantor's theorem that a function from a set to +its powerset cannot be surjective, illustrating various features of Isar. The +constant @{const surj} is predefined. +*} + +lemma "\ surj(f :: 'a \ 'a set)" +proof + assume 0: "surj f" + from 0 have 1: "\A. \a. A = f a" by(simp add: surj_def) + from 1 have 2: "\a. {x. x \ f x} = f a" by blast + from 2 show "False" by blast +qed + +text{* +The \isacom{proof} command lacks an explicit method how to perform +the proof. In such cases Isabelle tries to use some standard introduction +rule, in the above case for @{text"\"}: +\[ +\inferrule{ +\mbox{@{thm (prem 1) notI}}} +{\mbox{@{thm (concl) notI}}} +\] +In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}. +Thus we may assume @{prop"surj f"}. The proof shows that names of propositions +may be (single!) digits---meaningful names are hard to invent and are often +not necessary. Both \isacom{have} steps are obvious. The second one introduces +the diagonal set @{term"{x. x \ f x}"}, the key idea in the proof. +If you wonder why @{text 2} directly implies @{text False}: from @{text 2} +it follows that @{prop"a \ f a \ a \ f a"}. + +\subsection{@{text this}, @{text then}, @{text hence} and @{text thus}} + +Labels should be avoided. They interrupt the flow of the reader who has to +scan the context for the point where the label was introduced. Ideally, the +proof is a linear flow, where the output of one step becomes the input of the +next step, piping the previously proved fact into the next proof, just like +in a UNIX pipe. In such cases the predefined name @{text this} can be used +to refer to the proposition proved in the previous step. This allows us to +eliminate all labels from our proof (we suppress the \isacom{lemma} statement): +*} +(*<*) +lemma "\ surj(f :: 'a \ 'a set)" +(*>*) +proof + assume "surj f" + from this have "\a. {x. x \ f x} = f a" by(auto simp: surj_def) + from this show "False" by blast +qed + +text{* We have also taken the opportunity to compress the two \isacom{have} +steps into one. + +To compact the text further, Isar has a few convenient abbreviations: +\medskip + +\begin{tabular}{rcl} +\isacom{then} &=& \isacom{from} @{text this}\\ +\isacom{thus} &=& \isacom{then} \isacom{show}\\ +\isacom{hence} &=& \isacom{then} \isacom{have} +\end{tabular} +\medskip + +\noindent +With the help of these abbreviations the proof becomes +*} +(*<*) +lemma "\ surj(f :: 'a \ 'a set)" +(*>*) +proof + assume "surj f" + hence "\a. {x. x \ f x} = f a" by(auto simp: surj_def) + thus "False" by blast +qed +text{* + +There are two further linguistic variations: +\medskip + +\begin{tabular}{rcl} +(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts} +&=& +\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ +\isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this} +\end{tabular} +\medskip + +\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them +behind the proposition. + +\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} + +Lemmas can also be stated in a more structured fashion. To demonstrate this +feature with Cantor's theorem, we rephrase @{prop"\ surj f"} +a little: +*} + +lemma + fixes f :: "'a \ 'a set" + assumes s: "surj f" + shows "False" + +txt{* The optional \isacom{fixes} part allows you to state the types of +variables up front rather than by decorating one of their occurrences in the +formula with a type constraint. The key advantage of the structured format is +the \isacom{assumes} part that allows you to name each assumption; multiple +assumptions can be separated by \isacom{and}. The +\isacom{shows} part gives the goal. The actual theorem that will come out of +the proof is @{prop"surj f \ False"}, but during the proof the assumption +@{prop"surj f"} is available under the name @{text s} like any other fact. +*} + +proof - + have "\ a. {x. x \ f x} = f a" using s + by(auto simp: surj_def) + thus "False" by blast +qed + +text{* In the \isacom{have} step the assumption @{prop"surj f"} is now +referenced by its name @{text s}. The duplication of @{prop"surj f"} in the +above proofs (once in the statement of the lemma, once in its proof) has been +eliminated. + +\begin{warn} +Note the dash after the \isacom{proof} +command. It is the null method that does nothing to the goal. Leaving it out +would ask Isabelle to try some suitable introduction rule on the goal @{const +False}---but there is no suitable introduction rule and \isacom{proof} +would fail. +\end{warn} + +Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the +name @{text assms} that stands for the list of all assumptions. You can refer +to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc, +thus obviating the need to name them individually. + +\section{Proof patterns} + +We show a number of important basic proof patterns. Many of them arise from +the rules of natural deduction that are applied by \isacom{proof} by +default. The patterns are phrased in terms of \isacom{show} but work for +\isacom{have} and \isacom{lemma}, too. + +We start with two forms of \concept{case analysis}: +starting from a formula @{text P} we have the two cases @{text P} and +@{prop"~P"}, and starting from a fact @{prop"P \ Q"} +we have the two cases @{text P} and @{text Q}: +*}text_raw{* +\begin{tabular}{@ {}ll@ {}} +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "R" proof-(*>*) +show "R" +proof cases + assume "P" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +next + assume "\ P" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)oops(*>*) +text_raw {* } +\end{minipage} +& +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "R" proof-(*>*) +have "P \ Q" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +then show "R" +proof + assume "P" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +next + assume "Q" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +\end{tabular} +\medskip +\begin{isamarkuptext}% +How to prove a logical equivalence: +\end{isamarkuptext}% +\isa{% +*} +(*<*)lemma "P\Q" proof-(*>*) +show "P \ Q" +proof + assume "P" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "Q" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +next + assume "Q" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "P" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +qed(*<*)qed(*>*) +text_raw {* } +\medskip +\begin{isamarkuptext}% +Proofs by contradiction: +\end{isamarkuptext}% +\begin{tabular}{@ {}ll@ {}} +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "\ P" proof-(*>*) +show "\ P" +proof + assume "P" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +& +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "P" proof-(*>*) +show "P" +proof (rule ccontr) + assume "\P" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +\end{tabular} +\medskip +\begin{isamarkuptext}% +The name @{thm[source] ccontr} stands for ``classical contradiction''. + +How to prove quantified formulas: +\end{isamarkuptext}% +\begin{tabular}{@ {}ll@ {}} +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "ALL x. P x" proof-(*>*) +show "\x. P(x)" +proof + fix x + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "P(x)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +& +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "EX x. P(x)" proof-(*>*) +show "\x. P(x)" +proof + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "P(witness)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed +(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +\end{tabular} +\medskip +\begin{isamarkuptext}% +In the proof of \noquotes{@{prop[source]"\x. P(x)"}}, +the step \isacom{fix}~@{text x} introduces a locally fixed variable @{text x} +into the subproof, the proverbial ``arbitrary but fixed value''. +Instead of @{text x} we could have chosen any name in the subproof. +In the proof of \noquotes{@{prop[source]"\x. P(x)"}}, +@{text witness} is some arbitrary +term for which we can prove that it satisfies @{text P}. + +How to reason forward from \noquotes{@{prop[source] "\x. P(x)"}}: +\end{isamarkuptext}% +*} +(*<*)lemma True proof- assume 1: "EX x. P x"(*>*) +have "\x. P(x)" (*<*)by(rule 1)(*>*)txt_raw{*\ $\dots$\\*} +then obtain x where p: "P(x)" by blast +(*<*)oops(*>*) +text{* +After the \isacom{obtain} step, @{text x} (we could have chosen any name) +is a fixed local +variable, and @{text p} is the name of the fact +\noquotes{@{prop[source] "P(x)"}}. +This pattern works for one or more @{text x}. +As an example of the \isacom{obtain} command, here is the proof of +Cantor's theorem in more detail: +*} + +lemma "\ surj(f :: 'a \ 'a set)" +proof + assume "surj f" + hence "\a. {x. x \ f x} = f a" by(auto simp: surj_def) + then obtain a where "{x. x \ f x} = f a" by blast + hence "a \ f a \ a \ f a" by blast + thus "False" by blast +qed + +text_raw{* +\begin{isamarkuptext}% + +Finally, how to prove set equality and subset relationship: +\end{isamarkuptext}% +\begin{tabular}{@ {}ll@ {}} +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "A = (B::'a set)" proof-(*>*) +show "A = B" +proof + show "A \ B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +next + show "B \ A" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)qed(*>*) + +text_raw {* } +\end{minipage} +& +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "A <= (B::'a set)" proof-(*>*) +show "A \ B" +proof + fix x + assume "x \ A" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "x \ B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)qed(*>*) + +text_raw {* } +\end{minipage} +\end{tabular} +\begin{isamarkuptext}% +\section{Streamlining proofs} + +\subsection{Pattern matching and quotations} + +In the proof patterns shown above, formulas are often duplicated. +This can make the text harder to read, write and maintain. Pattern matching +is an abbreviation mechanism to avoid such duplication. Writing +\begin{quote} +\isacom{show} \ \textit{formula} @{text"("}\isacom{is} \textit{pattern}@{text")"} +\end{quote} +matches the pattern against the formula, thus instantiating the unknowns in +the pattern for later use. As an example, consider the proof pattern for +@{text"\"}: +\end{isamarkuptext}% +*} +(*<*)lemma "formula\<^isub>1 \ formula\<^isub>2" proof-(*>*) +show "formula\<^isub>1 \ formula\<^isub>2" (is "?L \ ?R") +proof + assume "?L" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "?R" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +next + assume "?R" + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show "?L" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +qed(*<*)qed(*>*) + +text{* Instead of duplicating @{text"formula\<^isub>i"} in the text, we introduce +the two abbreviations @{text"?L"} and @{text"?R"} by pattern matching. +Pattern matching works wherever a formula is stated, in particular +with \isacom{have} and \isacom{lemma}. + +The unknown @{text"?thesis"} is implicitly matched against any goal stated by +\isacom{lemma} or \isacom{show}. Here is a typical example: *} + +lemma "formula" +proof - + txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} + show ?thesis (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +qed + +text{* +Unknowns can also be instantiated with \isacom{let} commands +\begin{quote} +\isacom{let} @{text"?t"} = @{text"\""}\textit{some-big-term}@{text"\""} +\end{quote} +Later proof steps can refer to @{text"?t"}: +\begin{quote} +\isacom{have} @{text"\""}\dots @{text"?t"} \dots@{text"\""} +\end{quote} +\begin{warn} +Names of facts are introduced with @{text"name:"} and refer to proved +theorems. Unknowns @{text"?X"} refer to terms or formulas. +\end{warn} + +Although abbreviations shorten the text, the reader needs to remember what +they stand for. Similarly for names of facts. Names like @{text 1}, @{text 2} +and @{text 3} are not helpful and should only be used in short proofs. For +longer proofs, descriptive names are better. But look at this example: +\begin{quote} +\isacom{have} \ @{text"x_gr_0: \"x > 0\""}\\ +$\vdots$\\ +\isacom{from} @{text "x_gr_0"} \dots +\end{quote} +The name is longer than the fact it stands for! Short facts do not need names, +one can refer to them easily by quoting them: +\begin{quote} +\isacom{have} \ @{text"\"x > 0\""}\\ +$\vdots$\\ +\isacom{from} @{text "`x>0`"} \dots +\end{quote} +Note that the quotes around @{text"x>0"} are \concept{back quotes}. +They refer to the fact not by name but by value. + +\subsection{\isacom{moreover}} + +Sometimes one needs a number of facts to enable some deduction. Of course +one can name these facts individually, as shown on the right, +but one can also combine them with \isacom{moreover}, as shown on the left: +*}text_raw{* +\begin{tabular}{@ {}ll@ {}} +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "P" proof-(*>*) +have "P\<^isub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +moreover have "P\<^isub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +moreover +txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*) +moreover have "P\<^isub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +ultimately have "P" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +& +\qquad +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "P" proof-(*>*) +have lab\<^isub>1: "P\<^isub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +have lab\<^isub>2: "P\<^isub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$*} +txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*} +have lab\<^isub>n: "P\<^isub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +from lab\<^isub>1 lab\<^isub>2 txt_raw{*\ $\dots$\\*} +have "P" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +(*<*)oops(*>*) + +text_raw {* } +\end{minipage} +\end{tabular} +\begin{isamarkuptext}% +The \isacom{moreover} version is no shorter but expresses the structure more +clearly and avoids new names. + +\subsection{Raw proof blocks} + +Sometimes one would like to prove some lemma locally within a proof. +A lemma that shares the current context of assumptions but that +has its own assumptions and is generalized over its locally fixed +variables at the end. This is what a \concept{raw proof block} does: +\begin{quote} +@{text"{"} \isacom{fix} @{text"x\<^isub>1 \ x\<^isub>n"}\\ +\mbox{}\ \ \ \isacom{assume} @{text"A\<^isub>1 \ A\<^isub>m"}\\ +\mbox{}\ \ \ $\vdots$\\ +\mbox{}\ \ \ \isacom{have} @{text"B"}\\ +@{text"}"} +\end{quote} +proves @{text"\ A\<^isub>1; \ ; A\<^isub>m \ \ B"} +where all @{text"x\<^isub>i"} have been replaced by unknowns @{text"?x\<^isub>i"}. +\begin{warn} +The conclusion of a raw proof block is \emph{not} indicated by \isacom{show} +but is simply the final \isacom{have}. +\end{warn} + +As an example we prove a simple fact about divisibility on integers. +The definition of @{text "dvd"} is @{thm dvd_def}. +\end{isamarkuptext}% +*} + +lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a" +proof - + { fix k assume k: "a+b = b*k" + have "\k'. a = b*k'" + proof + show "a = b*(k - 1)" using k by(simp add: algebra_simps) + qed } + then show ?thesis using assms by(auto simp add: dvd_def) +qed + +text{* Note that the result of a raw proof block has no name. In this example +it was directly piped (via \isacom{then}) into the final proof, but it can +also be named for later reference: you simply follow the block directly by a +\isacom{note} command: +\begin{quote} +\isacom{note} \ @{text"name = this"} +\end{quote} +This introduces a new name @{text name} that refers to @{text this}, +the fact just proved, in this case the preceding block. In general, +\isacom{note} introduces a new name for one or more facts. + +\section{Case analysis and induction} + +\subsection{Datatype case analysis} + +We have seen case analysis on formulas. Now we want to distinguish +which form some term takes: is it @{text 0} or of the form @{term"Suc n"}, +is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example +proof by case analysis on the form of @{text xs}: +*} + +lemma "length(tl xs) = length xs - 1" +proof (cases xs) + assume "xs = []" + thus ?thesis by simp +next + fix y ys assume "xs = y#ys" + thus ?thesis by simp +qed + +text{* Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and +@{thm tl.simps(2)}. Note that the result type of @{const length} is @{typ nat} +and @{prop"0 - 1 = (0::nat)"}. + +This proof pattern works for any term @{text t} whose type is a datatype. +The goal has to be proved for each constructor @{text C}: +\begin{quote} +\isacom{fix} \ @{text"x\<^isub>1 \ x\<^isub>n"} \isacom{assume} @{text"\"t = C x\<^isub>1 \ x\<^isub>n\""} +\end{quote} +Each case can be written in a more compact form by means of the \isacom{case} +command: +\begin{quote} +\isacom{case} @{text "(C x\<^isub>1 \ x\<^isub>n)"} +\end{quote} +This is equivalent to the explicit \isacom{fix}-\isacom{assume} line +but also gives the assumption @{text"\"t = C x\<^isub>1 \ x\<^isub>n\""} a name: @{text C}, +like the constructor. +Here is the \isacom{case} version of the proof above: +*} +(*<*)lemma "length(tl xs) = length xs - 1"(*>*) +proof (cases xs) + case Nil + thus ?thesis by simp +next + case (Cons y ys) + thus ?thesis by simp +qed + +text{* Remember that @{text Nil} and @{text Cons} are the alphanumeric names +for @{text"[]"} and @{text"#"}. The names of the assumptions +are not used because they are directly piped (via \isacom{thus}) +into the proof of the claim. + +\subsection{Structural induction} + +We illustrate structural induction with an example based on natural numbers: +the sum (@{text"\"}) of the first @{text n} natural numbers +(@{text"{0..n::nat}"}) is equal to \mbox{@{term"n*(n+1) div 2::nat"}}. +Never mind the details, just focus on the pattern: +*} + +lemma "\{0..n::nat} = n*(n+1) div 2" +proof (induction n) + show "\{0..0::nat} = 0*(0+1) div 2" by simp +next + fix n assume "\{0..n::nat} = n*(n+1) div 2" + thus "\{0..Suc n} = Suc n*(Suc n+1) div 2" by simp +qed + +text{* Except for the rewrite steps, everything is explicitly given. This +makes the proof easily readable, but the duplication means it is tedious to +write and maintain. Here is how pattern +matching can completely avoid any duplication: *} + +lemma "\{0..n::nat} = n*(n+1) div 2" (is "?P n") +proof (induction n) + show "?P 0" by simp +next + fix n assume "?P n" + thus "?P(Suc n)" by simp +qed + +text{* The first line introduces an abbreviation @{text"?P n"} for the goal. +Pattern matching @{text"?P n"} with the goal instantiates @{text"?P"} to the +function @{term"\n. \{0..n::nat} = n*(n+1) div 2"}. Now the proposition to +be proved in the base case can be written as @{text"?P 0"}, the induction +hypothesis as @{text"?P n"}, and the conclusion of the induction step as +@{text"?P(Suc n)"}. + +Induction also provides the \isacom{case} idiom that abbreviates +the \isacom{fix}-\isacom{assume} step. The above proof becomes +*} +(*<*)lemma "\{0..n::nat} = n*(n+1) div 2"(*>*) +proof (induction n) + case 0 + show ?case by simp +next + case (Suc n) + thus ?case by simp +qed + +text{* +The unknown @{text "?case"} is set in each case to the required +claim, i.e.\ @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof, +without requiring the user to define a @{text "?P"}. The general +pattern for induction over @{typ nat} is shown on the left-hand side: +*}text_raw{* +\begin{tabular}{@ {}ll@ {}} +\begin{minipage}[t]{.4\textwidth} +\isa{% +*} +(*<*)lemma "P(n::nat)" proof -(*>*) +show "P(n)" +proof (induction n) + case 0 + txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*} + show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +next + case (Suc n) + txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*} + show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} +qed(*<*)qed(*>*) + +text_raw {* } +\end{minipage} +& +\begin{minipage}[t]{.4\textwidth} +~\\ +~\\ +\isacom{let} @{text"?case = \"P(0)\""}\\ +~\\ +~\\ +~\\[1ex] +\isacom{fix} @{text n} \isacom{assume} @{text"Suc: \"P(n)\""}\\ +\isacom{let} @{text"?case = \"P(Suc n)\""}\\ +\end{minipage} +\end{tabular} +\medskip +*} +text{* +On the right side you can see what the \isacom{case} command +on the left stands for. + +In case the goal is an implication, induction does one more thing: the +proposition to be proved in each case is not the whole implication but only +its conclusion; the premises of the implication are immediately made +assumptions of that case. That is, if in the above proof we replace +\isacom{show}~@{text"P(n)"} by +\mbox{\isacom{show}~@{text"A(n) \ P(n)"}} +then \isacom{case}~@{text 0} stands for +\begin{quote} +\isacom{assume} \ @{text"0: \"A(0)\""}\\ +\isacom{let} @{text"?case = \"P(0)\""} +\end{quote} +and \isacom{case}~@{text"(Suc n)"} stands for +\begin{quote} +\isacom{fix} @{text n}\\ +\isacom{assume} @{text"Suc:"} + \begin{tabular}[t]{l}@{text"\"A(n) \ P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\ +\isacom{let} @{text"?case = \"P(Suc n)\""} +\end{quote} +The list of assumptions @{text Suc} is actually subdivided +into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \ P(n)"}) +and @{text"Suc.prems"}, the premises of the goal being proved +(here @{text"A(Suc n)"}). + +Induction works for any datatype. +Proving a goal @{text"\ A\<^isub>1(x); \; A\<^isub>k(x) \ \ P(x)"} +by induction on @{text x} generates a proof obligation for each constructor +@{text C} of the datatype. The command @{text"case (C x\<^isub>1 \ x\<^isub>n)"} +performs the following steps: +\begin{enumerate} +\item \isacom{fix} @{text"x\<^isub>1 \ x\<^isub>n"} +\item \isacom{assume} the induction hypotheses (calling them @{text C.IH}) + and the premises \mbox{@{text"A\<^isub>i(C x\<^isub>1 \ x\<^isub>n)"}} (calling them @{text"C.prems"}) + and calling the whole list @{text C} +\item \isacom{let} @{text"?case = \"P(C x\<^isub>1 \ x\<^isub>n)\""} +\end{enumerate} + +\subsection{Rule induction} + +Recall the inductive and recursive definitions of even numbers in +\autoref{sec:inductive-defs}: +*} + +inductive ev :: "nat \ bool" where +ev0: "ev 0" | +evSS: "ev n \ ev(Suc(Suc n))" + +fun even :: "nat \ bool" where +"even 0 = True" | +"even (Suc 0) = False" | +"even (Suc(Suc n)) = even n" + +text{* We recast the proof of @{prop"ev n \ even n"} in Isar. The +left column shows the actual proof text, the right column shows +the implicit effect of the two \isacom{case} commands:*}text_raw{* +\begin{tabular}{@ {}l@ {\qquad}l@ {}} +\begin{minipage}[t]{.5\textwidth} +\isa{% +*} + +lemma "ev n \ even n" +proof(induction rule: ev.induct) + case ev0 + show ?case by simp +next + case evSS + + + + thus ?case by simp +qed + +text_raw {* } +\end{minipage} +& +\begin{minipage}[t]{.5\textwidth} +~\\ +~\\ +\isacom{let} @{text"?case = \"even 0\""}\\ +~\\ +~\\ +\isacom{fix} @{text n}\\ +\isacom{assume} @{text"evSS:"} + \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\ +\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\ +\end{minipage} +\end{tabular} +\medskip +*} +text{* +The proof resembles structural induction, but the induction rule is given +explicitly and the names of the cases are the names of the rules in the +inductive definition. +Let us examine the two assumptions named @{thm[source]evSS}: +@{prop "ev n"} is the premise of rule @{thm[source]evSS}, which we may assume +because we are in the case where that rule was used; @{prop"even n"} +is the induction hypothesis. +\begin{warn} +Because each \isacom{case} command introduces a list of assumptions +named like the case name, which is the name of a rule of the inductive +definition, those rules now need to be accessed with a qualified name, here +@{thm[source] ev.ev0} and @{thm[source] ev.evSS} +\end{warn} + +In the case @{thm[source]evSS} of the proof above we have pretended that the +system fixes a variable @{text n}. But unless the user provides the name +@{text n}, the system will just invent its own name that cannot be referred +to. In the above proof, we do not need to refer to it, hence we do not give +it a specific name. In case one needs to refer to it one writes +\begin{quote} +\isacom{case} @{text"(evSS m)"} +\end{quote} +just like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions. +The name @{text m} is an arbitrary choice. As a result, +case @{thm[source] evSS} is derived from a renamed version of +rule @{thm[source] evSS}: @{text"ev m \ ev(Suc(Suc m))"}. +Here is an example with a (contrived) intermediate step that refers to @{text m}: +*} + +lemma "ev n \ even n" +proof(induction rule: ev.induct) + case ev0 show ?case by simp +next + case (evSS m) + have "even(Suc(Suc m)) = even m" by simp + thus ?case using `even m` by blast +qed + +text{* +\indent +In general, let @{text I} be a (for simplicity unary) inductively defined +predicate and let the rules in the definition of @{text I} +be called @{text "rule\<^isub>1"}, \dots, @{text "rule\<^isub>n"}. A proof by rule +induction follows this pattern: +*} + +(*<*) +inductive I where rule\<^isub>1: "I()" | rule\<^isub>2: "I()" | rule\<^isub>n: "I()" +lemma "I x \ P x" proof-(*>*) +show "I x \ P x" +proof(induction rule: I.induct) + case rule\<^isub>1 + txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*} + show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +next + txt_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*} +(*<*) + case rule\<^isub>2 + show ?case sorry +(*>*) +next + case rule\<^isub>n + txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*} + show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} +qed(*<*)qed(*>*) + +text{* +One can provide explicit variable names by writing +\isacom{case}~@{text"(rule\<^isub>i x\<^isub>1 \ x\<^isub>k)"}, thus renaming the first @{text k} +free variables in rule @{text i} to @{text"x\<^isub>1 \ x\<^isub>k"}, +going through rule @{text i} from left to right. + +\subsection{Assumption naming} + +In any induction, \isacom{case}~@{text name} sets up a list of assumptions +also called @{text name}, which is subdivided into three parts: +\begin{description} +\item[@{text name.IH}] contains the induction hypotheses. +\item[@{text name.hyps}] contains all the other hypotheses of this case in the +induction rule. For rule inductions these are the hypotheses of rule +@{text name}, for structural inductions these are empty. +\item[@{text name.prems}] contains the (suitably instantiated) premises +of the statement being proved, i.e. the @{text A\<^isub>i} when +proving @{text"\ A\<^isub>1; \; A\<^isub>n \ \ A"}. +\end{description} +\begin{warn} +Proof method @{text induct} differs from @{text induction} +only in this naming policy: @{text induct} does not distinguish +@{text IH} from @{text hyps} but subsumes @{text IH} under @{text hyps}. +\end{warn} + +More complicated inductive proofs than the ones we have seen so far +often need to refer to specific assumptions---just @{text name} or even +@{text name.prems} and @{text name.IH} can be too unspecific. +This is where the indexing of fact lists comes in handy, e.g.\ +@{text"name.IH(2)"} or @{text"name.prems(1-2)"}. + +\subsection{Rule inversion} + +Rule inversion is case analysis of which rule could have been used to +derive some fact. The name \concept{rule inversion} emphasizes that we are +reasoning backwards: by which rules could some given fact have been proved? +For the inductive definition of @{const ev}, rule inversion can be summarized +like this: +@{prop[display]"ev n \ n = 0 \ (EX k. n = Suc(Suc k) \ ev k)"} +The realisation in Isabelle is a case analysis. +A simple example is the proof that @{prop"ev n \ ev (n - 2)"}. We +already went through the details informally in \autoref{sec:Logic:even}. This +is the Isar proof: +*} +(*<*) +notepad +begin fix n +(*>*) + assume "ev n" + from this have "ev(n - 2)" + proof cases + case ev0 thus "ev(n - 2)" by (simp add: ev.ev0) + next + case (evSS k) thus "ev(n - 2)" by (simp add: ev.evSS) + qed +(*<*) +end +(*>*) + +text{* The key point here is that a case analysis over some inductively +defined predicate is triggered by piping the given fact +(here: \isacom{from}~@{text this}) into a proof by @{text cases}. +Let us examine the assumptions available in each case. In case @{text ev0} +we have @{text"n = 0"} and in case @{text evSS} we have @{prop"n = Suc(Suc k)"} +and @{prop"ev k"}. In each case the assumptions are available under the name +of the case; there is no fine grained naming schema like for induction. + +Sometimes some rules could not have been used to derive the given fact +because constructors clash. As an extreme example consider +rule inversion applied to @{prop"ev(Suc 0)"}: neither rule @{text ev0} nor +rule @{text evSS} can yield @{prop"ev(Suc 0)"} because @{text"Suc 0"} unifies +neither with @{text 0} nor with @{term"Suc(Suc n)"}. Impossible cases do not +have to be proved. Hence we can prove anything from @{prop"ev(Suc 0)"}: +*} +(*<*) +notepad begin fix P +(*>*) + assume "ev(Suc 0)" then have P by cases +(*<*) +end +(*>*) + +text{* That is, @{prop"ev(Suc 0)"} is simply not provable: *} + +lemma "\ ev(Suc 0)" +proof + assume "ev(Suc 0)" then show False by cases +qed + +text{* Normally not all cases will be impossible. As a simple exercise, +prove that \mbox{@{prop"\ ev(Suc(Suc(Suc 0)))"}.} +*} + +(* +lemma "\ ev(Suc(Suc(Suc 0)))" +proof + assume "ev(Suc(Suc(Suc 0)))" + then show False + proof cases + case evSS + from `ev(Suc 0)` show False by cases + qed +qed +*) + +(*<*) +end +(*>*)