47269

1 
(*<*)


2 
theory Isar


3 
imports LaTeXsugar


4 
begin


5 
ML{* quick_and_dirty := true *}


6 
(*>*)


7 
text{*


8 
Applyscripts are unreadable and hard to maintain. The language of choice


9 
for larger proofs is \concept{Isar}. The two key features of Isar are:


10 
\begin{itemize}


11 
\item It is structured, not linear.


12 
\item It is readable without running it because


13 
you need to state what you are proving at any given point.


14 
\end{itemize}


15 
Whereas applyscripts are like assembly language programs, Isar proofs


16 
are like structured programs with comments. A typical Isar proof looks like this:


17 
*}text{*


18 
\begin{tabular}{@ {}l}


19 
\isacom{proof}\\


20 
\quad\isacom{assume} @{text"\""}$\mathit{formula}_0$@{text"\""}\\


21 
\quad\isacom{have} @{text"\""}$\mathit{formula}_1$@{text"\""} \quad\isacom{by} @{text simp}\\


22 
\quad\vdots\\


23 
\quad\isacom{have} @{text"\""}$\mathit{formula}_n$@{text"\""} \quad\isacom{by} @{text blast}\\


24 
\quad\isacom{show} @{text"\""}$\mathit{formula}_{n+1}$@{text"\""} \quad\isacom{by} @{text \<dots>}\\


25 
\isacom{qed}


26 
\end{tabular}


27 
*}text{*


28 
It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$

47704

29 
(provided each proof step succeeds).

47269

30 
The intermediate \isacom{have} statements are merely stepping stones


31 
on the way towards the \isacom{show} statement that proves the actual


32 
goal. In more detail, this is the Isar core syntax:


33 
\medskip


34 


35 
\begin{tabular}{@ {}lcl@ {}}


36 
\textit{proof} &=& \isacom{by} \textit{method}\\


37 
&$\mid$& \isacom{proof} [\textit{method}] \ \textit{step}$^*$ \ \isacom{qed}


38 
\end{tabular}


39 
\medskip


40 


41 
\begin{tabular}{@ {}lcl@ {}}


42 
\textit{step} &=& \isacom{fix} \textit{variables} \\


43 
&$\mid$& \isacom{assume} \textit{proposition} \\


44 
&$\mid$& [\isacom{from} \textit{fact}$^+$] (\isacom{have} $\mid$ \isacom{show}) \ \textit{proposition} \ \textit{proof}


45 
\end{tabular}


46 
\medskip


47 


48 
\begin{tabular}{@ {}lcl@ {}}


49 
\textit{proposition} &=& [\textit{name}:] @{text"\""}\textit{formula}@{text"\""}


50 
\end{tabular}


51 
\medskip


52 


53 
\begin{tabular}{@ {}lcl@ {}}


54 
\textit{fact} &=& \textit{name} \ $\mid$ \ \dots


55 
\end{tabular}


56 
\medskip


57 


58 
\noindent A proof can either be an atomic \isacom{by} with a single proof


59 
method which must finish off the statement being proved, for example @{text


60 
auto}. Or it can be a \isacom{proof}\isacom{qed} block of multiple


61 
steps. Such a block can optionally begin with a proof method that indicates


62 
how to start off the proof, e.g.\ \mbox{@{text"(induction xs)"}}.


63 


64 
A step either assumes a proposition or states a proposition


65 
together with its proof. The optional \isacom{from} clause


66 
indicates which facts are to be used in the proof.


67 
Intermediate propositions are stated with \isacom{have}, the overall goal


68 
with \isacom{show}. A step can also introduce new local variables with


69 
\isacom{fix}. Logically, \isacom{fix} introduces @{text"\<And>"}quantified


70 
variables, \isacom{assume} introduces the assumption of an implication


71 
(@{text"\<Longrightarrow>"}) and \isacom{have}/\isacom{show} the conclusion.


72 


73 
Propositions are optionally named formulas. These names can be referred to in


74 
later \isacom{from} clauses. In the simplest case, a fact is such a name.


75 
But facts can also be composed with @{text OF} and @{text of} as shown in


76 
\S\ref{sec:forwardproof}hence the \dots\ in the above grammar. Note


77 
that assumptions, intermediate \isacom{have} statements and global lemmas all


78 
have the same status and are thus collectively referred to as


79 
\concept{facts}.


80 


81 
Fact names can stand for whole lists of facts. For example, if @{text f} is


82 
defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of


83 
recursion equations defining @{text f}. Individual facts can be selected by


84 
writing @{text"f.simps(2)"}, whole sublists by @{text"f.simps(24)"}.


85 


86 


87 
\section{Isar by example}


88 

47704

89 
We show a number of proofs of Cantor's theorem that a function from a set to

47269

90 
its powerset cannot be surjective, illustrating various features of Isar. The


91 
constant @{const surj} is predefined.


92 
*}


93 


94 
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"


95 
proof


96 
assume 0: "surj f"


97 
from 0 have 1: "\<forall>A. \<exists>a. A = f a" by(simp add: surj_def)


98 
from 1 have 2: "\<exists>a. {x. x \<notin> f x} = f a" by blast


99 
from 2 show "False" by blast


100 
qed


101 


102 
text{*


103 
The \isacom{proof} command lacks an explicit method how to perform


104 
the proof. In such cases Isabelle tries to use some standard introduction


105 
rule, in the above case for @{text"\<not>"}:


106 
\[


107 
\inferrule{


108 
\mbox{@{thm (prem 1) notI}}}


109 
{\mbox{@{thm (concl) notI}}}


110 
\]


111 
In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}.


112 
Thus we may assume @{prop"surj f"}. The proof shows that names of propositions


113 
may be (single!) digitsmeaningful names are hard to invent and are often


114 
not necessary. Both \isacom{have} steps are obvious. The second one introduces


115 
the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof.


116 
If you wonder why @{text 2} directly implies @{text False}: from @{text 2}


117 
it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}.


118 


119 
\subsection{@{text this}, @{text then}, @{text hence} and @{text thus}}


120 


121 
Labels should be avoided. They interrupt the flow of the reader who has to


122 
scan the context for the point where the label was introduced. Ideally, the


123 
proof is a linear flow, where the output of one step becomes the input of the


124 
next step, piping the previously proved fact into the next proof, just like


125 
in a UNIX pipe. In such cases the predefined name @{text this} can be used


126 
to refer to the proposition proved in the previous step. This allows us to


127 
eliminate all labels from our proof (we suppress the \isacom{lemma} statement):


128 
*}


129 
(*<*)


130 
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"


131 
(*>*)


132 
proof


133 
assume "surj f"


134 
from this have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)


135 
from this show "False" by blast


136 
qed


137 


138 
text{* We have also taken the opportunity to compress the two \isacom{have}


139 
steps into one.


140 


141 
To compact the text further, Isar has a few convenient abbreviations:


142 
\medskip


143 


144 
\begin{tabular}{rcl}


145 
\isacom{then} &=& \isacom{from} @{text this}\\


146 
\isacom{thus} &=& \isacom{then} \isacom{show}\\


147 
\isacom{hence} &=& \isacom{then} \isacom{have}


148 
\end{tabular}


149 
\medskip


150 


151 
\noindent


152 
With the help of these abbreviations the proof becomes


153 
*}


154 
(*<*)


155 
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"


156 
(*>*)


157 
proof


158 
assume "surj f"


159 
hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)


160 
thus "False" by blast


161 
qed


162 
text{*


163 


164 
There are two further linguistic variations:


165 
\medskip


166 


167 
\begin{tabular}{rcl}


168 
(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts}


169 
&=&


170 
\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\


171 
\isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this}


172 
\end{tabular}


173 
\medskip


174 

47711

175 
\noindent The \isacom{using} idiom deemphasizes the used facts by moving them

47269

176 
behind the proposition.


177 


178 
\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}


179 


180 
Lemmas can also be stated in a more structured fashion. To demonstrate this

47306

181 
feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}

47269

182 
a little:


183 
*}


184 


185 
lemma


186 
fixes f :: "'a \<Rightarrow> 'a set"


187 
assumes s: "surj f"


188 
shows "False"


189 


190 
txt{* The optional \isacom{fixes} part allows you to state the types of


191 
variables up front rather than by decorating one of their occurrences in the


192 
formula with a type constraint. The key advantage of the structured format is

47306

193 
the \isacom{assumes} part that allows you to name each assumption; multiple


194 
assumptions can be separated by \isacom{and}. The

47269

195 
\isacom{shows} part gives the goal. The actual theorem that will come out of


196 
the proof is @{prop"surj f \<Longrightarrow> False"}, but during the proof the assumption


197 
@{prop"surj f"} is available under the name @{text s} like any other fact.


198 
*}


199 


200 
proof 


201 
have "\<exists> a. {x. x \<notin> f x} = f a" using s


202 
by(auto simp: surj_def)


203 
thus "False" by blast


204 
qed


205 


206 
text{* In the \isacom{have} step the assumption @{prop"surj f"} is now


207 
referenced by its name @{text s}. The duplication of @{prop"surj f"} in the


208 
above proofs (once in the statement of the lemma, once in its proof) has been


209 
eliminated.


210 


211 
\begin{warn}


212 
Note the dash after the \isacom{proof}


213 
command. It is the null method that does nothing to the goal. Leaving it out


214 
would ask Isabelle to try some suitable introduction rule on the goal @{const


215 
False}but there is no suitable introduction rule and \isacom{proof}


216 
would fail.


217 
\end{warn}


218 

47704

219 
Stating a lemma with \isacom{assumes}\isacom{shows} implicitly introduces the

47269

220 
name @{text assms} that stands for the list of all assumptions. You can refer


221 
to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc,


222 
thus obviating the need to name them individually.


223 


224 
\section{Proof patterns}


225 


226 
We show a number of important basic proof patterns. Many of them arise from


227 
the rules of natural deduction that are applied by \isacom{proof} by


228 
default. The patterns are phrased in terms of \isacom{show} but work for


229 
\isacom{have} and \isacom{lemma}, too.


230 

47711

231 
We start with two forms of \concept{case analysis}:

47269

232 
starting from a formula @{text P} we have the two cases @{text P} and


233 
@{prop"~P"}, and starting from a fact @{prop"P \<or> Q"}


234 
we have the two cases @{text P} and @{text Q}:


235 
*}text_raw{*


236 
\begin{tabular}{@ {}ll@ {}}


237 
\begin{minipage}[t]{.4\textwidth}


238 
\isa{%


239 
*}


240 
(*<*)lemma "R" proof(*>*)


241 
show "R"


242 
proof cases


243 
assume "P"


244 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


245 
show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


246 
next


247 
assume "\<not> P"


248 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


249 
show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


250 
qed(*<*)oops(*>*)


251 
text_raw {* }


252 
\end{minipage}


253 
&


254 
\begin{minipage}[t]{.4\textwidth}


255 
\isa{%


256 
*}


257 
(*<*)lemma "R" proof(*>*)


258 
have "P \<or> Q" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


259 
then show "R"


260 
proof


261 
assume "P"


262 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


263 
show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


264 
next


265 
assume "Q"


266 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


267 
show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


268 
qed(*<*)oops(*>*)


269 


270 
text_raw {* }


271 
\end{minipage}


272 
\end{tabular}


273 
\medskip


274 
\begin{isamarkuptext}%


275 
How to prove a logical equivalence:


276 
\end{isamarkuptext}%


277 
\isa{%


278 
*}


279 
(*<*)lemma "P\<longleftrightarrow>Q" proof(*>*)


280 
show "P \<longleftrightarrow> Q"


281 
proof


282 
assume "P"


283 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


284 
show "Q" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


285 
next


286 
assume "Q"


287 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


288 
show "P" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


289 
qed(*<*)qed(*>*)


290 
text_raw {* }


291 
\medskip


292 
\begin{isamarkuptext}%


293 
Proofs by contradiction:


294 
\end{isamarkuptext}%


295 
\begin{tabular}{@ {}ll@ {}}


296 
\begin{minipage}[t]{.4\textwidth}


297 
\isa{%


298 
*}


299 
(*<*)lemma "\<not> P" proof(*>*)


300 
show "\<not> P"


301 
proof


302 
assume "P"


303 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


304 
show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


305 
qed(*<*)oops(*>*)


306 


307 
text_raw {* }


308 
\end{minipage}


309 
&


310 
\begin{minipage}[t]{.4\textwidth}


311 
\isa{%


312 
*}


313 
(*<*)lemma "P" proof(*>*)


314 
show "P"


315 
proof (rule ccontr)


316 
assume "\<not>P"


317 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


318 
show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


319 
qed(*<*)oops(*>*)


320 


321 
text_raw {* }


322 
\end{minipage}


323 
\end{tabular}


324 
\medskip


325 
\begin{isamarkuptext}%


326 
The name @{thm[source] ccontr} stands for ``classical contradiction''.


327 


328 
How to prove quantified formulas:


329 
\end{isamarkuptext}%


330 
\begin{tabular}{@ {}ll@ {}}


331 
\begin{minipage}[t]{.4\textwidth}


332 
\isa{%


333 
*}


334 
(*<*)lemma "ALL x. P x" proof(*>*)


335 
show "\<forall>x. P(x)"


336 
proof


337 
fix x


338 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


339 
show "P(x)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


340 
qed(*<*)oops(*>*)


341 


342 
text_raw {* }


343 
\end{minipage}


344 
&


345 
\begin{minipage}[t]{.4\textwidth}


346 
\isa{%


347 
*}


348 
(*<*)lemma "EX x. P(x)" proof(*>*)


349 
show "\<exists>x. P(x)"


350 
proof


351 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


352 
show "P(witness)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


353 
qed


354 
(*<*)oops(*>*)


355 


356 
text_raw {* }


357 
\end{minipage}


358 
\end{tabular}


359 
\medskip


360 
\begin{isamarkuptext}%


361 
In the proof of \noquotes{@{prop[source]"\<forall>x. P(x)"}},

47704

362 
the step \isacom{fix}~@{text x} introduces a locally fixed variable @{text x}

47269

363 
into the subproof, the proverbial ``arbitrary but fixed value''.


364 
Instead of @{text x} we could have chosen any name in the subproof.


365 
In the proof of \noquotes{@{prop[source]"\<exists>x. P(x)"}},


366 
@{text witness} is some arbitrary


367 
term for which we can prove that it satisfies @{text P}.


368 


369 
How to reason forward from \noquotes{@{prop[source] "\<exists>x. P(x)"}}:


370 
\end{isamarkuptext}%


371 
*}


372 
(*<*)lemma True proof assume 1: "EX x. P x"(*>*)


373 
have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)txt_raw{*\ $\dots$\\*}


374 
then obtain x where p: "P(x)" by blast


375 
(*<*)oops(*>*)


376 
text{*


377 
After the \isacom{obtain} step, @{text x} (we could have chosen any name)


378 
is a fixed local


379 
variable, and @{text p} is the name of the fact


380 
\noquotes{@{prop[source] "P(x)"}}.


381 
This pattern works for one or more @{text x}.


382 
As an example of the \isacom{obtain} command, here is the proof of


383 
Cantor's theorem in more detail:


384 
*}


385 


386 
lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)"


387 
proof


388 
assume "surj f"


389 
hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def)


390 
then obtain a where "{x. x \<notin> f x} = f a" by blast


391 
hence "a \<notin> f a \<longleftrightarrow> a \<in> f a" by blast


392 
thus "False" by blast


393 
qed


394 


395 
text_raw{*


396 
\begin{isamarkuptext}%

47306

397 


398 
Finally, how to prove set equality and subset relationship:

47269

399 
\end{isamarkuptext}%


400 
\begin{tabular}{@ {}ll@ {}}


401 
\begin{minipage}[t]{.4\textwidth}


402 
\isa{%


403 
*}


404 
(*<*)lemma "A = (B::'a set)" proof(*>*)


405 
show "A = B"


406 
proof


407 
show "A \<subseteq> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


408 
next


409 
show "B \<subseteq> A" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


410 
qed(*<*)qed(*>*)


411 


412 
text_raw {* }


413 
\end{minipage}


414 
&


415 
\begin{minipage}[t]{.4\textwidth}


416 
\isa{%


417 
*}


418 
(*<*)lemma "A <= (B::'a set)" proof(*>*)


419 
show "A \<subseteq> B"


420 
proof


421 
fix x


422 
assume "x \<in> A"


423 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


424 
show "x \<in> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


425 
qed(*<*)qed(*>*)


426 


427 
text_raw {* }


428 
\end{minipage}


429 
\end{tabular}


430 
\begin{isamarkuptext}%


431 
\section{Streamlining proofs}


432 


433 
\subsection{Pattern matching and quotations}


434 


435 
In the proof patterns shown above, formulas are often duplicated.


436 
This can make the text harder to read, write and maintain. Pattern matching


437 
is an abbreviation mechanism to avoid such duplication. Writing


438 
\begin{quote}


439 
\isacom{show} \ \textit{formula} @{text"("}\isacom{is} \textit{pattern}@{text")"}


440 
\end{quote}


441 
matches the pattern against the formula, thus instantiating the unknowns in


442 
the pattern for later use. As an example, consider the proof pattern for


443 
@{text"\<longleftrightarrow>"}:


444 
\end{isamarkuptext}%


445 
*}


446 
(*<*)lemma "formula\<^isub>1 \<longleftrightarrow> formula\<^isub>2" proof(*>*)


447 
show "formula\<^isub>1 \<longleftrightarrow> formula\<^isub>2" (is "?L \<longleftrightarrow> ?R")


448 
proof


449 
assume "?L"


450 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


451 
show "?R" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


452 
next


453 
assume "?R"


454 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


455 
show "?L" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


456 
qed(*<*)qed(*>*)


457 


458 
text{* Instead of duplicating @{text"formula\<^isub>i"} in the text, we introduce


459 
the two abbreviations @{text"?L"} and @{text"?R"} by pattern matching.


460 
Pattern matching works wherever a formula is stated, in particular


461 
with \isacom{have} and \isacom{lemma}.


462 


463 
The unknown @{text"?thesis"} is implicitly matched against any goal stated by


464 
\isacom{lemma} or \isacom{show}. Here is a typical example: *}


465 


466 
lemma "formula"


467 
proof 


468 
txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*}


469 
show ?thesis (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


470 
qed


471 


472 
text{*


473 
Unknowns can also be instantiated with \isacom{let} commands


474 
\begin{quote}


475 
\isacom{let} @{text"?t"} = @{text"\""}\textit{somebigterm}@{text"\""}


476 
\end{quote}


477 
Later proof steps can refer to @{text"?t"}:


478 
\begin{quote}


479 
\isacom{have} @{text"\""}\dots @{text"?t"} \dots@{text"\""}


480 
\end{quote}


481 
\begin{warn}


482 
Names of facts are introduced with @{text"name:"} and refer to proved


483 
theorems. Unknowns @{text"?X"} refer to terms or formulas.


484 
\end{warn}


485 


486 
Although abbreviations shorten the text, the reader needs to remember what


487 
they stand for. Similarly for names of facts. Names like @{text 1}, @{text 2}


488 
and @{text 3} are not helpful and should only be used in short proofs. For

47704

489 
longer proofs, descriptive names are better. But look at this example:

47269

490 
\begin{quote}


491 
\isacom{have} \ @{text"x_gr_0: \"x > 0\""}\\


492 
$\vdots$\\


493 
\isacom{from} @{text "x_gr_0"} \dots


494 
\end{quote}


495 
The name is longer than the fact it stands for! Short facts do not need names,


496 
one can refer to them easily by quoting them:


497 
\begin{quote}


498 
\isacom{have} \ @{text"\"x > 0\""}\\


499 
$\vdots$\\


500 
\isacom{from} @{text "`x>0`"} \dots


501 
\end{quote}


502 
Note that the quotes around @{text"x>0"} are \concept{back quotes}.


503 
They refer to the fact not by name but by value.


504 


505 
\subsection{\isacom{moreover}}


506 


507 
Sometimes one needs a number of facts to enable some deduction. Of course


508 
one can name these facts individually, as shown on the right,


509 
but one can also combine them with \isacom{moreover}, as shown on the left:


510 
*}text_raw{*


511 
\begin{tabular}{@ {}ll@ {}}


512 
\begin{minipage}[t]{.4\textwidth}


513 
\isa{%


514 
*}


515 
(*<*)lemma "P" proof(*>*)


516 
have "P\<^isub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


517 
moreover have "P\<^isub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


518 
moreover


519 
txt_raw{*\\$\vdots$\\\hspace{1.4ex}*}(*<*)have "True" ..(*>*)


520 
moreover have "P\<^isub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


521 
ultimately have "P" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


522 
(*<*)oops(*>*)


523 


524 
text_raw {* }


525 
\end{minipage}


526 
&


527 
\qquad


528 
\begin{minipage}[t]{.4\textwidth}


529 
\isa{%


530 
*}


531 
(*<*)lemma "P" proof(*>*)


532 
have lab\<^isub>1: "P\<^isub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


533 
have lab\<^isub>2: "P\<^isub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$*}


534 
txt_raw{*\\$\vdots$\\\hspace{1.4ex}*}


535 
have lab\<^isub>n: "P\<^isub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


536 
from lab\<^isub>1 lab\<^isub>2 txt_raw{*\ $\dots$\\*}


537 
have "P" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


538 
(*<*)oops(*>*)


539 


540 
text_raw {* }


541 
\end{minipage}


542 
\end{tabular}


543 
\begin{isamarkuptext}%


544 
The \isacom{moreover} version is no shorter but expresses the structure more


545 
clearly and avoids new names.


546 


547 
\subsection{Raw proof blocks}


548 

47306

549 
Sometimes one would like to prove some lemma locally within a proof.

47269

550 
A lemma that shares the current context of assumptions but that

47711

551 
has its own assumptions and is generalized over its locally fixed

47269

552 
variables at the end. This is what a \concept{raw proof block} does:


553 
\begin{quote}


554 
@{text"{"} \isacom{fix} @{text"x\<^isub>1 \<dots> x\<^isub>n"}\\


555 
\mbox{}\ \ \ \isacom{assume} @{text"A\<^isub>1 \<dots> A\<^isub>m"}\\


556 
\mbox{}\ \ \ $\vdots$\\


557 
\mbox{}\ \ \ \isacom{have} @{text"B"}\\


558 
@{text"}"}


559 
\end{quote}


560 
proves @{text"\<lbrakk> A\<^isub>1; \<dots> ; A\<^isub>m \<rbrakk> \<Longrightarrow> B"}


561 
where all @{text"x\<^isub>i"} have been replaced by unknowns @{text"?x\<^isub>i"}.


562 
\begin{warn}


563 
The conclusion of a raw proof block is \emph{not} indicated by \isacom{show}


564 
but is simply the final \isacom{have}.


565 
\end{warn}


566 


567 
As an example we prove a simple fact about divisibility on integers.


568 
The definition of @{text "dvd"} is @{thm dvd_def}.


569 
\end{isamarkuptext}%


570 
*}


571 


572 
lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a"


573 
proof 


574 
{ fix k assume k: "a+b = b*k"


575 
have "\<exists>k'. a = b*k'"


576 
proof


577 
show "a = b*(k  1)" using k by(simp add: algebra_simps)


578 
qed }


579 
then show ?thesis using assms by(auto simp add: dvd_def)


580 
qed


581 


582 
text{* Note that the result of a raw proof block has no name. In this example


583 
it was directly piped (via \isacom{then}) into the final proof, but it can


584 
also be named for later reference: you simply follow the block directly by a


585 
\isacom{note} command:


586 
\begin{quote}


587 
\isacom{note} \ @{text"name = this"}


588 
\end{quote}


589 
This introduces a new name @{text name} that refers to @{text this},


590 
the fact just proved, in this case the preceding block. In general,


591 
\isacom{note} introduces a new name for one or more facts.


592 

47711

593 
\section{Case analysis and induction}

47269

594 

47711

595 
\subsection{Datatype case analysis}

47269

596 

47711

597 
We have seen case analysis on formulas. Now we want to distinguish

47269

598 
which form some term takes: is it @{text 0} or of the form @{term"Suc n"},


599 
is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example

47711

600 
proof by case analysis on the form of @{text xs}:

47269

601 
*}


602 


603 
lemma "length(tl xs) = length xs  1"


604 
proof (cases xs)


605 
assume "xs = []"


606 
thus ?thesis by simp


607 
next


608 
fix y ys assume "xs = y#ys"


609 
thus ?thesis by simp


610 
qed


611 


612 
text{* Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and


613 
@{thm tl.simps(2)}. Note that the result type of @{const length} is @{typ nat}


614 
and @{prop"0  1 = (0::nat)"}.


615 


616 
This proof pattern works for any term @{text t} whose type is a datatype.


617 
The goal has to be proved for each constructor @{text C}:


618 
\begin{quote}


619 
\isacom{fix} \ @{text"x\<^isub>1 \<dots> x\<^isub>n"} \isacom{assume} @{text"\"t = C x\<^isub>1 \<dots> x\<^isub>n\""}


620 
\end{quote}


621 
Each case can be written in a more compact form by means of the \isacom{case}


622 
command:


623 
\begin{quote}


624 
\isacom{case} @{text "(C x\<^isub>1 \<dots> x\<^isub>n)"}


625 
\end{quote}

47704

626 
This is equivalent to the explicit \isacom{fix}\isacom{assume} line

47269

627 
but also gives the assumption @{text"\"t = C x\<^isub>1 \<dots> x\<^isub>n\""} a name: @{text C},


628 
like the constructor.


629 
Here is the \isacom{case} version of the proof above:


630 
*}


631 
(*<*)lemma "length(tl xs) = length xs  1"(*>*)


632 
proof (cases xs)


633 
case Nil


634 
thus ?thesis by simp


635 
next


636 
case (Cons y ys)


637 
thus ?thesis by simp


638 
qed


639 


640 
text{* Remember that @{text Nil} and @{text Cons} are the alphanumeric names


641 
for @{text"[]"} and @{text"#"}. The names of the assumptions


642 
are not used because they are directly piped (via \isacom{thus})


643 
into the proof of the claim.


644 


645 
\subsection{Structural induction}


646 


647 
We illustrate structural induction with an example based on natural numbers:


648 
the sum (@{text"\<Sum>"}) of the first @{text n} natural numbers


649 
(@{text"{0..n::nat}"}) is equal to \mbox{@{term"n*(n+1) div 2::nat"}}.


650 
Never mind the details, just focus on the pattern:


651 
*}


652 

47711

653 
lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"

47269

654 
proof (induction n)


655 
show "\<Sum>{0..0::nat} = 0*(0+1) div 2" by simp


656 
next


657 
fix n assume "\<Sum>{0..n::nat} = n*(n+1) div 2"

47711

658 
thus "\<Sum>{0..Suc n} = Suc n*(Suc n+1) div 2" by simp

47269

659 
qed


660 


661 
text{* Except for the rewrite steps, everything is explicitly given. This


662 
makes the proof easily readable, but the duplication means it is tedious to


663 
write and maintain. Here is how pattern


664 
matching can completely avoid any duplication: *}


665 


666 
lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n")


667 
proof (induction n)


668 
show "?P 0" by simp


669 
next


670 
fix n assume "?P n"


671 
thus "?P(Suc n)" by simp


672 
qed


673 


674 
text{* The first line introduces an abbreviation @{text"?P n"} for the goal.


675 
Pattern matching @{text"?P n"} with the goal instantiates @{text"?P"} to the


676 
function @{term"\<lambda>n. \<Sum>{0..n::nat} = n*(n+1) div 2"}. Now the proposition to


677 
be proved in the base case can be written as @{text"?P 0"}, the induction


678 
hypothesis as @{text"?P n"}, and the conclusion of the induction step as


679 
@{text"?P(Suc n)"}.


680 


681 
Induction also provides the \isacom{case} idiom that abbreviates


682 
the \isacom{fix}\isacom{assume} step. The above proof becomes


683 
*}


684 
(*<*)lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"(*>*)


685 
proof (induction n)


686 
case 0


687 
show ?case by simp


688 
next


689 
case (Suc n)


690 
thus ?case by simp


691 
qed


692 


693 
text{*


694 
The unknown @{text "?case"} is set in each case to the required


695 
claim, i.e.\ @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof,


696 
without requiring the user to define a @{text "?P"}. The general


697 
pattern for induction over @{typ nat} is shown on the lefthand side:


698 
*}text_raw{*


699 
\begin{tabular}{@ {}ll@ {}}


700 
\begin{minipage}[t]{.4\textwidth}


701 
\isa{%


702 
*}


703 
(*<*)lemma "P(n::nat)" proof (*>*)


704 
show "P(n)"


705 
proof (induction n)


706 
case 0


707 
txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{1ex}*}


708 
show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


709 
next


710 
case (Suc n)


711 
txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{1ex}*}


712 
show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*}


713 
qed(*<*)qed(*>*)


714 


715 
text_raw {* }


716 
\end{minipage}


717 
&


718 
\begin{minipage}[t]{.4\textwidth}


719 
~\\


720 
~\\


721 
\isacom{let} @{text"?case = \"P(0)\""}\\


722 
~\\


723 
~\\


724 
~\\[1ex]


725 
\isacom{fix} @{text n} \isacom{assume} @{text"Suc: \"P(n)\""}\\


726 
\isacom{let} @{text"?case = \"P(Suc n)\""}\\


727 
\end{minipage}


728 
\end{tabular}


729 
\medskip


730 
*}


731 
text{*


732 
On the right side you can see what the \isacom{case} command


733 
on the left stands for.


734 


735 
In case the goal is an implication, induction does one more thing: the


736 
proposition to be proved in each case is not the whole implication but only


737 
its conclusion; the premises of the implication are immediately made


738 
assumptions of that case. That is, if in the above proof we replace

49837

739 
\isacom{show}~@{text"\"P(n)\""} by


740 
\mbox{\isacom{show}~@{text"\"A(n) \<Longrightarrow> P(n)\""}}

47269

741 
then \isacom{case}~@{text 0} stands for


742 
\begin{quote}


743 
\isacom{assume} \ @{text"0: \"A(0)\""}\\


744 
\isacom{let} @{text"?case = \"P(0)\""}


745 
\end{quote}


746 
and \isacom{case}~@{text"(Suc n)"} stands for


747 
\begin{quote}


748 
\isacom{fix} @{text n}\\


749 
\isacom{assume} @{text"Suc:"}

47306

750 
\begin{tabular}[t]{l}@{text"\"A(n) \<Longrightarrow> P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\

47269

751 
\isacom{let} @{text"?case = \"P(Suc n)\""}


752 
\end{quote}


753 
The list of assumptions @{text Suc} is actually subdivided


754 
into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \<Longrightarrow> P(n)"})


755 
and @{text"Suc.prems"}, the premises of the goal being proved


756 
(here @{text"A(Suc n)"}).


757 


758 
Induction works for any datatype.


759 
Proving a goal @{text"\<lbrakk> A\<^isub>1(x); \<dots>; A\<^isub>k(x) \<rbrakk> \<Longrightarrow> P(x)"}


760 
by induction on @{text x} generates a proof obligation for each constructor


761 
@{text C} of the datatype. The command @{text"case (C x\<^isub>1 \<dots> x\<^isub>n)"}


762 
performs the following steps:


763 
\begin{enumerate}


764 
\item \isacom{fix} @{text"x\<^isub>1 \<dots> x\<^isub>n"}


765 
\item \isacom{assume} the induction hypotheses (calling them @{text C.IH})


766 
and the premises \mbox{@{text"A\<^isub>i(C x\<^isub>1 \<dots> x\<^isub>n)"}} (calling them @{text"C.prems"})


767 
and calling the whole list @{text C}


768 
\item \isacom{let} @{text"?case = \"P(C x\<^isub>1 \<dots> x\<^isub>n)\""}


769 
\end{enumerate}


770 


771 
\subsection{Rule induction}


772 


773 
Recall the inductive and recursive definitions of even numbers in


774 
\autoref{sec:inductivedefs}:


775 
*}


776 


777 
inductive ev :: "nat \<Rightarrow> bool" where


778 
ev0: "ev 0" 


779 
evSS: "ev n \<Longrightarrow> ev(Suc(Suc n))"


780 


781 
fun even :: "nat \<Rightarrow> bool" where


782 
"even 0 = True" 


783 
"even (Suc 0) = False" 


784 
"even (Suc(Suc n)) = even n"


785 


786 
text{* We recast the proof of @{prop"ev n \<Longrightarrow> even n"} in Isar. The


787 
left column shows the actual proof text, the right column shows


788 
the implicit effect of the two \isacom{case} commands:*}text_raw{*


789 
\begin{tabular}{@ {}l@ {\qquad}l@ {}}


790 
\begin{minipage}[t]{.5\textwidth}


791 
\isa{%


792 
*}


793 


794 
lemma "ev n \<Longrightarrow> even n"


795 
proof(induction rule: ev.induct)


796 
case ev0


797 
show ?case by simp


798 
next


799 
case evSS


800 


801 


802 


803 
thus ?case by simp


804 
qed


805 


806 
text_raw {* }


807 
\end{minipage}


808 
&


809 
\begin{minipage}[t]{.5\textwidth}


810 
~\\


811 
~\\


812 
\isacom{let} @{text"?case = \"even 0\""}\\


813 
~\\


814 
~\\


815 
\isacom{fix} @{text n}\\


816 
\isacom{assume} @{text"evSS:"}

47306

817 
\begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\


818 
\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\

47269

819 
\end{minipage}


820 
\end{tabular}


821 
\medskip


822 
*}


823 
text{*


824 
The proof resembles structural induction, but the induction rule is given


825 
explicitly and the names of the cases are the names of the rules in the


826 
inductive definition.


827 
Let us examine the two assumptions named @{thm[source]evSS}:


828 
@{prop "ev n"} is the premise of rule @{thm[source]evSS}, which we may assume


829 
because we are in the case where that rule was used; @{prop"even n"}


830 
is the induction hypothesis.


831 
\begin{warn}


832 
Because each \isacom{case} command introduces a list of assumptions


833 
named like the case name, which is the name of a rule of the inductive


834 
definition, those rules now need to be accessed with a qualified name, here


835 
@{thm[source] ev.ev0} and @{thm[source] ev.evSS}


836 
\end{warn}


837 


838 
In the case @{thm[source]evSS} of the proof above we have pretended that the


839 
system fixes a variable @{text n}. But unless the user provides the name


840 
@{text n}, the system will just invent its own name that cannot be referred


841 
to. In the above proof, we do not need to refer to it, hence we do not give


842 
it a specific name. In case one needs to refer to it one writes


843 
\begin{quote}


844 
\isacom{case} @{text"(evSS m)"}


845 
\end{quote}


846 
just like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions.


847 
The name @{text m} is an arbitrary choice. As a result,


848 
case @{thm[source] evSS} is derived from a renamed version of


849 
rule @{thm[source] evSS}: @{text"ev m \<Longrightarrow> ev(Suc(Suc m))"}.


850 
Here is an example with a (contrived) intermediate step that refers to @{text m}:


851 
*}


852 


853 
lemma "ev n \<Longrightarrow> even n"


854 
proof(induction rule: ev.induct)


855 
case ev0 show ?case by simp


856 
next


857 
case (evSS m)


858 
have "even(Suc(Suc m)) = even m" by simp


859 
thus ?case using `even m` by blast


860 
qed


861 


862 
text{*


863 
\indent


864 
In general, let @{text I} be a (for simplicity unary) inductively defined


865 
predicate and let the rules in the definition of @{text I}


866 
be called @{text "rule\<^isub>1"}, \dots, @{text "rule\<^isub>n"}. A proof by rule


867 
induction follows this pattern:


868 
*}


869 


870 
(*<*)


871 
inductive I where rule\<^isub>1: "I()"  rule\<^isub>2: "I()"  rule\<^isub>n: "I()"


872 
lemma "I x \<Longrightarrow> P x" proof(*>*)


873 
show "I x \<Longrightarrow> P x"


874 
proof(induction rule: I.induct)


875 
case rule\<^isub>1


876 
txt_raw{*\\[.4ex]\mbox{}\ \ $\vdots$\\[.4ex]\mbox{}\hspace{1ex}*}


877 
show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


878 
next


879 
txt_raw{*\\[.4ex]$\vdots$\\[.4ex]\mbox{}\hspace{1ex}*}


880 
(*<*)


881 
case rule\<^isub>2


882 
show ?case sorry


883 
(*>*)


884 
next


885 
case rule\<^isub>n


886 
txt_raw{*\\[.4ex]\mbox{}\ \ $\vdots$\\[.4ex]\mbox{}\hspace{1ex}*}


887 
show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*}


888 
qed(*<*)qed(*>*)


889 


890 
text{*


891 
One can provide explicit variable names by writing


892 
\isacom{case}~@{text"(rule\<^isub>i x\<^isub>1 \<dots> x\<^isub>k)"}, thus renaming the first @{text k}


893 
free variables in rule @{text i} to @{text"x\<^isub>1 \<dots> x\<^isub>k"},


894 
going through rule @{text i} from left to right.


895 


896 
\subsection{Assumption naming}

51443

897 
\label{sec:assmnaming}

47269

898 


899 
In any induction, \isacom{case}~@{text name} sets up a list of assumptions


900 
also called @{text name}, which is subdivided into three parts:


901 
\begin{description}


902 
\item[@{text name.IH}] contains the induction hypotheses.


903 
\item[@{text name.hyps}] contains all the other hypotheses of this case in the


904 
induction rule. For rule inductions these are the hypotheses of rule


905 
@{text name}, for structural inductions these are empty.


906 
\item[@{text name.prems}] contains the (suitably instantiated) premises


907 
of the statement being proved, i.e. the @{text A\<^isub>i} when


908 
proving @{text"\<lbrakk> A\<^isub>1; \<dots>; A\<^isub>n \<rbrakk> \<Longrightarrow> A"}.


909 
\end{description}


910 
\begin{warn}


911 
Proof method @{text induct} differs from @{text induction}


912 
only in this naming policy: @{text induct} does not distinguish


913 
@{text IH} from @{text hyps} but subsumes @{text IH} under @{text hyps}.


914 
\end{warn}


915 


916 
More complicated inductive proofs than the ones we have seen so far


917 
often need to refer to specific assumptionsjust @{text name} or even


918 
@{text name.prems} and @{text name.IH} can be too unspecific.


919 
This is where the indexing of fact lists comes in handy, e.g.\


920 
@{text"name.IH(2)"} or @{text"name.prems(12)"}.


921 


922 
\subsection{Rule inversion}


923 

47711

924 
Rule inversion is case analysis of which rule could have been used to

47269

925 
derive some fact. The name \concept{rule inversion} emphasizes that we are


926 
reasoning backwards: by which rules could some given fact have been proved?


927 
For the inductive definition of @{const ev}, rule inversion can be summarized


928 
like this:


929 
@{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (EX k. n = Suc(Suc k) \<and> ev k)"}

47711

930 
The realisation in Isabelle is a case analysis.

47269

931 
A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n  2)"}. We


932 
already went through the details informally in \autoref{sec:Logic:even}. This


933 
is the Isar proof:


934 
*}


935 
(*<*)


936 
notepad


937 
begin fix n


938 
(*>*)


939 
assume "ev n"


940 
from this have "ev(n  2)"


941 
proof cases


942 
case ev0 thus "ev(n  2)" by (simp add: ev.ev0)


943 
next


944 
case (evSS k) thus "ev(n  2)" by (simp add: ev.evSS)


945 
qed


946 
(*<*)


947 
end


948 
(*>*)


949 

47711

950 
text{* The key point here is that a case analysis over some inductively

47269

951 
defined predicate is triggered by piping the given fact


952 
(here: \isacom{from}~@{text this}) into a proof by @{text cases}.


953 
Let us examine the assumptions available in each case. In case @{text ev0}


954 
we have @{text"n = 0"} and in case @{text evSS} we have @{prop"n = Suc(Suc k)"}


955 
and @{prop"ev k"}. In each case the assumptions are available under the name


956 
of the case; there is no fine grained naming schema like for induction.


957 

47704

958 
Sometimes some rules could not have been used to derive the given fact

47269

959 
because constructors clash. As an extreme example consider


960 
rule inversion applied to @{prop"ev(Suc 0)"}: neither rule @{text ev0} nor


961 
rule @{text evSS} can yield @{prop"ev(Suc 0)"} because @{text"Suc 0"} unifies


962 
neither with @{text 0} nor with @{term"Suc(Suc n)"}. Impossible cases do not


963 
have to be proved. Hence we can prove anything from @{prop"ev(Suc 0)"}:


964 
*}


965 
(*<*)


966 
notepad begin fix P


967 
(*>*)


968 
assume "ev(Suc 0)" then have P by cases


969 
(*<*)


970 
end


971 
(*>*)


972 


973 
text{* That is, @{prop"ev(Suc 0)"} is simply not provable: *}


974 


975 
lemma "\<not> ev(Suc 0)"


976 
proof


977 
assume "ev(Suc 0)" then show False by cases


978 
qed


979 


980 
text{* Normally not all cases will be impossible. As a simple exercise,


981 
prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}

51443

982 


983 
\subsection{Advanced rule induction}

51445

984 
\label{sec:advancedruleinduction}

51443

985 


986 
So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}


987 
where @{text I} is some inductively defined predicate and @{text x}, @{text y}, @{text z}


988 
are variables. In some rare situations one needs to deal with an assumption where


989 
not all arguments @{text r}, @{text s}, @{text t} are variables:


990 
\begin{isabelle}


991 
\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}


992 
\end{isabelle}


993 
Applying the standard form of


994 
rule induction in such a situation will lead to strange and typically unproveable goals.


995 
We can easily reduce this situation to the standard one by introducing


996 
new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this:


997 
\begin{isabelle}


998 
\isacom{lemma} @{text[source]"I x y z \<Longrightarrow> x = r \<Longrightarrow> y = s \<Longrightarrow> z = t \<Longrightarrow> \<dots>"}


999 
\end{isabelle}


1000 
Standard rule induction will worke fine now, provided the free variables in


1001 
@{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}.


1002 


1003 
However, induction can do the above transformation for us, behind the curtains, so we never


1004 
need to see the expanded version of the lemma. This is what we need to write:


1005 
\begin{isabelle}


1006 
\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}\isanewline


1007 
\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}


1008 
\end{isabelle}


1009 
Just like for rule inversion, cases that are impossible because of constructor clashes


1010 
will not show up at all. Here is a concrete example: *}


1011 


1012 
lemma "ev (Suc m) \<Longrightarrow> \<not> ev m"


1013 
proof(induction "Suc m" arbitrary: m rule: ev.induct)


1014 
fix n assume IH: "\<And>m. n = Suc m \<Longrightarrow> \<not> ev m"


1015 
show "\<not> ev (Suc n)"


1016 
proof "contradition"


1017 
assume "ev(Suc n)"


1018 
thus False


1019 
proof cases "rule inversion"


1020 
fix k assume "n = Suc k" "ev k"


1021 
thus False using IH by auto


1022 
qed


1023 
qed


1024 
qed


1025 


1026 
text{*


1027 
Remarks:


1028 
\begin{itemize}


1029 
\item


1030 
Instead of the \isacom{case} and @{text ?case} magic we have spelled all formulas out.


1031 
This is merely for greater clarity.


1032 
\item


1033 
We only need to deal with one case because the @{thm[source] ev0} case is impossible.


1034 
\item


1035 
The form of the @{text IH} shows us that internally the lemma was expanded as explained


1036 
above: \noquotes{@{prop[source]"ev x \<Longrightarrow> x = Suc m \<Longrightarrow> \<not> ev m"}}.


1037 
\item


1038 
The goal @{prop"\<not> ev (Suc n)"} may suprise. The expanded version of the lemma


1039 
would suggest that we have a \isacom{fix} @{text m} \isacom{assume} @{prop"Suc(Suc n) = Suc m"}


1040 
and need to show @{prop"\<not> ev m"}. What happened is that Isabelle immediately


1041 
simplified @{prop"Suc(Suc n) = Suc m"} to @{prop"Suc n = m"} and could then eliminate


1042 
@{text m}. Beware of such nice surprises with this advanced form of induction.


1043 
\end{itemize}


1044 
\begin{warn}


1045 
This advanced form of induction does not support the @{text IH}


1046 
naming schema explained in \autoref{sec:assmnaming}:


1047 
the induction hypotheses are instead found under the name @{text hyps}, like for the simpler


1048 
@{text induct} method.


1049 
\end{warn}

47269

1050 
*}


1051 
(*


1052 
lemma "\<not> ev(Suc(Suc(Suc 0)))"


1053 
proof


1054 
assume "ev(Suc(Suc(Suc 0)))"


1055 
then show False


1056 
proof cases


1057 
case evSS


1058 
from `ev(Suc 0)` show False by cases


1059 
qed


1060 
qed


1061 
*)


1062 


1063 
(*<*)


1064 
end


1065 
(*>*)
