author  wenzelm 
Tue, 31 Mar 2015 22:31:05 +0200  
changeset 59886  e0dc738eb08c 
parent 58999  ed09ae4ea2d8 
child 61012  40a0a4077126 
permissions  rwrr 
47269  1 
(*<*) 
2 
theory Isar 

3 
imports LaTeXsugar 

4 
begin 

52059  5 
declare [[quick_and_dirty]] 
47269  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. 

56989  12 
\item It is readable without its being run because 
47269  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@ {}} 

55359  36 
\textit{proof} &=& \indexed{\isacom{by}}{by} \textit{method}\\ 
37 
&$\mid$& \indexed{\isacom{proof}}{proof} [\textit{method}] \ \textit{step}$^*$ \ \indexed{\isacom{qed}}{qed} 

47269  38 
\end{tabular} 
39 
\medskip 

40 

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

55359  42 
\textit{step} &=& \indexed{\isacom{fix}}{fix} \textit{variables} \\ 
43 
&$\mid$& \indexed{\isacom{assume}}{assume} \textit{proposition} \\ 

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

47269  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 

56989  60 
auto}, or it can be a \isacom{proof}\isacom{qed} block of multiple 
47269  61 
steps. Such a block can optionally begin with a proof method that indicates 
58504  62 
how to start off the proof, e.g., \mbox{@{text"(induction xs)"}}. 
47269  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 

56989  68 
is stated with \isacom{show}. A step can also introduce new local variables with 
47269  69 
\isacom{fix}. Logically, \isacom{fix} introduces @{text"\<And>"}quantified 
70 
variables, \isacom{assume} introduces the assumption of an implication 

56989  71 
(@{text"\<Longrightarrow>"}) and \isacom{have}/\isacom{show} introduce the conclusion. 
47269  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 

58602  76 
\autoref{sec:forwardproof}  hence the \dots\ in the above grammar. Note 
47269  77 
that assumptions, intermediate \isacom{have} statements and global lemmas all 
78 
have the same status and are thus collectively referred to as 

55317  79 
\conceptidx{facts}{fact}. 
47269  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 

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

86 

52361  87 
\section{Isar by Example} 
47269  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{* 

56989  103 
The \isacom{proof} command lacks an explicit method by which to perform 
47269  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 

58602  113 
may be (single!) digits  meaningful names are hard to invent and are often 
47269  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 

55359  119 
\subsection{\indexed{@{text this}}{this}, \indexed{\isacom{then}}{then}, \indexed{\isacom{hence}}{hence} and \indexed{\isacom{thus}}{thus}} 
47269  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 

58605  124 
next step, piping the previously proved fact into the next proof, like 
47269  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 

54839  144 
\begin{tabular}{r@ {\quad=\quad}l} 
145 
\isacom{then} & \isacom{from} @{text this}\\ 

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

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

47269  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 

54839  167 
\begin{tabular}{r@ {\quad=\quad}l} 
55359  168 
(\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \indexed{\isacom{using}}{using} \ \textit{facts} 
54839  169 
& 
47269  170 
\isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ 
55359  171 
\indexed{\isacom{with}}{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this} 
47269  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 

55359  178 
\subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}} 
179 
\index{lemma@\isacom{lemma}} 

47269  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 

56312  206 
text{* 
207 
\begin{warn} 

208 
Note the hyphen after the \isacom{proof} command. 

56989  209 
It is the null method that does nothing to the goal. Leaving it out would be asking 
58602  210 
Isabelle to try some suitable introduction rule on the goal @{const False}  but 
56312  211 
there is no such rule and \isacom{proof} would fail. 
212 
\end{warn} 

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

47269  214 
referenced by its name @{text s}. The duplication of @{prop"surj f"} in the 
215 
above proofs (once in the statement of the lemma, once in its proof) has been 

216 
eliminated. 

217 

47704  218 
Stating a lemma with \isacom{assumes}\isacom{shows} implicitly introduces the 
55359  219 
name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer 
58521  220 
to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc., 
47269  221 
thus obviating the need to name them individually. 
222 

52361  223 
\section{Proof Patterns} 
47269  224 

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

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

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

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

229 

47711  230 
We start with two forms of \concept{case analysis}: 
47269  231 
starting from a formula @{text P} we have the two cases @{text P} and 
232 
@{prop"~P"}, and starting from a fact @{prop"P \<or> Q"} 

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

234 
*}text_raw{* 

235 
\begin{tabular}{@ {}ll@ {}} 

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

237 
\isa{% 

238 
*} 

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

240 
show "R" 

241 
proof cases 

242 
assume "P" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

243 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

244 
show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  245 
next 
246 
assume "\<not> P" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

247 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

248 
show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  249 
qed(*<*)oops(*>*) 
250 
text_raw {* } 

55361  251 
\end{minipage}\index{cases@@{text cases}} 
47269  252 
& 
253 
\begin{minipage}[t]{.4\textwidth} 

254 
\isa{% 

255 
*} 

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

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

257 
have "P \<or> Q" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  258 
then show "R" 
259 
proof 

260 
assume "P" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

261 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

262 
show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  263 
next 
264 
assume "Q" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

265 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

266 
show "R" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  267 
qed(*<*)oops(*>*) 
268 

269 
text_raw {* } 

270 
\end{minipage} 

271 
\end{tabular} 

272 
\medskip 

273 
\begin{isamarkuptext}% 

274 
How to prove a logical equivalence: 

275 
\end{isamarkuptext}% 

276 
\isa{% 

277 
*} 

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

279 
show "P \<longleftrightarrow> Q" 

280 
proof 

281 
assume "P" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

282 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

283 
show "Q" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  284 
next 
285 
assume "Q" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

286 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

287 
show "P" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  288 
qed(*<*)qed(*>*) 
289 
text_raw {* } 

290 
\medskip 

291 
\begin{isamarkuptext}% 

55361  292 
Proofs by contradiction (@{thm[source] ccontr} stands for ``classical contradiction''): 
47269  293 
\end{isamarkuptext}% 
294 
\begin{tabular}{@ {}ll@ {}} 

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

296 
\isa{% 

297 
*} 

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

299 
show "\<not> P" 

300 
proof 

301 
assume "P" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

302 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

303 
show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  304 
qed(*<*)oops(*>*) 
305 

306 
text_raw {* } 

307 
\end{minipage} 

308 
& 

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

310 
\isa{% 

311 
*} 

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

313 
show "P" 

314 
proof (rule ccontr) 

315 
assume "\<not>P" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

316 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

317 
show "False" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  318 
qed(*<*)oops(*>*) 
319 

320 
text_raw {* } 

321 
\end{minipage} 

322 
\end{tabular} 

323 
\medskip 

324 
\begin{isamarkuptext}% 

325 
How to prove quantified formulas: 

326 
\end{isamarkuptext}% 

327 
\begin{tabular}{@ {}ll@ {}} 

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

329 
\isa{% 

330 
*} 

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

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

333 
proof 

334 
fix x 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

335 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

336 
show "P(x)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  337 
qed(*<*)oops(*>*) 
338 

339 
text_raw {* } 

340 
\end{minipage} 

341 
& 

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

343 
\isa{% 

344 
*} 

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

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

347 
proof 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

348 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

349 
show "P(witness)" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  350 
qed 
351 
(*<*)oops(*>*) 

352 

353 
text_raw {* } 

354 
\end{minipage} 

355 
\end{tabular} 

356 
\medskip 

357 
\begin{isamarkuptext}% 

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

55361  359 
the step \indexed{\isacom{fix}}{fix}~@{text x} introduces a locally fixed variable @{text x} 
47269  360 
into the subproof, the proverbial ``arbitrary but fixed value''. 
361 
Instead of @{text x} we could have chosen any name in the subproof. 

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

363 
@{text witness} is some arbitrary 

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

365 

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

367 
\end{isamarkuptext}% 

368 
*} 

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

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

370 
have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)text_raw{*\ $\dots$\\*} 
47269  371 
then obtain x where p: "P(x)" by blast 
372 
(*<*)oops(*>*) 

373 
text{* 

55389  374 
After the \indexed{\isacom{obtain}}{obtain} step, @{text x} (we could have chosen any name) 
47269  375 
is a fixed local 
376 
variable, and @{text p} is the name of the fact 

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

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

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

380 
Cantor's theorem in more detail: 

381 
*} 

382 

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

384 
proof 

385 
assume "surj f" 

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

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

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

389 
thus "False" by blast 

390 
qed 

391 

392 
text_raw{* 

393 
\begin{isamarkuptext}% 

47306  394 

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

47269  396 
\end{isamarkuptext}% 
397 
\begin{tabular}{@ {}ll@ {}} 

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

399 
\isa{% 

400 
*} 

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

402 
show "A = B" 

403 
proof 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

404 
show "A \<subseteq> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  405 
next 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

406 
show "B \<subseteq> A" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  407 
qed(*<*)qed(*>*) 
408 

409 
text_raw {* } 

410 
\end{minipage} 

411 
& 

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

413 
\isa{% 

414 
*} 

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

416 
show "A \<subseteq> B" 

417 
proof 

418 
fix x 

419 
assume "x \<in> A" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

420 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

421 
show "x \<in> B" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  422 
qed(*<*)qed(*>*) 
423 

424 
text_raw {* } 

425 
\end{minipage} 

426 
\end{tabular} 

427 
\begin{isamarkuptext}% 

52361  428 
\section{Streamlining Proofs} 
47269  429 

52361  430 
\subsection{Pattern Matching and Quotations} 
47269  431 

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

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

434 
is an abbreviation mechanism to avoid such duplication. Writing 

435 
\begin{quote} 

55359  436 
\isacom{show} \ \textit{formula} @{text"("}\indexed{\isacom{is}}{is} \textit{pattern}@{text")"} 
47269  437 
\end{quote} 
438 
matches the pattern against the formula, thus instantiating the unknowns in 

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

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

441 
\end{isamarkuptext}% 

442 
*} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

443 
(*<*)lemma "formula\<^sub>1 \<longleftrightarrow> formula\<^sub>2" proof(*>*) 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

444 
show "formula\<^sub>1 \<longleftrightarrow> formula\<^sub>2" (is "?L \<longleftrightarrow> ?R") 
47269  445 
proof 
446 
assume "?L" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

447 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

448 
show "?R" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  449 
next 
450 
assume "?R" 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

451 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

452 
show "?L" (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  453 
qed(*<*)qed(*>*) 
454 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

455 
text{* Instead of duplicating @{text"formula\<^sub>i"} in the text, we introduce 
47269  456 
the two abbreviations @{text"?L"} and @{text"?R"} by pattern matching. 
457 
Pattern matching works wherever a formula is stated, in particular 

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

459 

55359  460 
The unknown \indexed{@{text"?thesis"}}{thesis} is implicitly matched against any goal stated by 
47269  461 
\isacom{lemma} or \isacom{show}. Here is a typical example: *} 
462 

463 
lemma "formula" 

464 
proof  

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

465 
text_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

466 
show ?thesis (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  467 
qed 
468 

469 
text{* 

55359  470 
Unknowns can also be instantiated with \indexed{\isacom{let}}{let} commands 
47269  471 
\begin{quote} 
472 
\isacom{let} @{text"?t"} = @{text"\""}\textit{somebigterm}@{text"\""} 

473 
\end{quote} 

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

475 
\begin{quote} 

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

477 
\end{quote} 

478 
\begin{warn} 

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

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

481 
\end{warn} 

482 

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

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

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

47704  486 
longer proofs, descriptive names are better. But look at this example: 
47269  487 
\begin{quote} 
488 
\isacom{have} \ @{text"x_gr_0: \"x > 0\""}\\ 

489 
$\vdots$\\ 

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

491 
\end{quote} 

56989  492 
The name is longer than the fact it stands for! Short facts do not need names; 
47269  493 
one can refer to them easily by quoting them: 
494 
\begin{quote} 

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

496 
$\vdots$\\ 

55359  497 
\isacom{from} @{text "`x>0`"} \dots\index{$IMP053@@{text"`...`"}} 
47269  498 
\end{quote} 
55317  499 
Note that the quotes around @{text"x>0"} are \conceptnoidx{back quotes}. 
47269  500 
They refer to the fact not by name but by value. 
501 

55359  502 
\subsection{\indexed{\isacom{moreover}}{moreover}} 
503 
\index{ultimately@\isacom{ultimately}} 

47269  504 

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

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

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

508 
*}text_raw{* 

509 
\begin{tabular}{@ {}ll@ {}} 

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

511 
\isa{% 

512 
*} 

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

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

514 
have "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

515 
moreover have "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  516 
moreover 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

517 
text_raw{*\\$\vdots$\\\hspace{1.4ex}*}(*<*)have "True" ..(*>*) 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

518 
moreover have "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

519 
ultimately have "P" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  520 
(*<*)oops(*>*) 
521 

522 
text_raw {* } 

523 
\end{minipage} 

524 
& 

525 
\qquad 

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

527 
\isa{% 

528 
*} 

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

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

530 
have lab\<^sub>1: "P\<^sub>1" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

531 
have lab\<^sub>2: "P\<^sub>2" (*<*)sorry(*>*)text_raw{*\ $\dots$*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

532 
text_raw{*\\$\vdots$\\\hspace{1.4ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

533 
have lab\<^sub>n: "P\<^sub>n" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

534 
from lab\<^sub>1 lab\<^sub>2 text_raw{*\ $\dots$\\*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

535 
have "P" (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  536 
(*<*)oops(*>*) 
537 

538 
text_raw {* } 

539 
\end{minipage} 

540 
\end{tabular} 

541 
\begin{isamarkuptext}% 

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

543 
clearly and avoids new names. 

544 

52361  545 
\subsection{Raw Proof Blocks} 
47269  546 

56989  547 
Sometimes one would like to prove some lemma locally within a proof, 
548 
a lemma that shares the current context of assumptions but that 

58502  549 
has its own assumptions and is generalized over its locally fixed 
47269  550 
variables at the end. This is what a \concept{raw proof block} does: 
55359  551 
\begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)} 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

552 
@{text"{"} \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\ 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

553 
\mbox{}\ \ \ \isacom{assume} @{text"A\<^sub>1 \<dots> A\<^sub>m"}\\ 
47269  554 
\mbox{}\ \ \ $\vdots$\\ 
555 
\mbox{}\ \ \ \isacom{have} @{text"B"}\\ 

556 
@{text"}"} 

557 
\end{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

558 
proves @{text"\<lbrakk> A\<^sub>1; \<dots> ; A\<^sub>m \<rbrakk> \<Longrightarrow> B"} 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

559 
where all @{text"x\<^sub>i"} have been replaced by unknowns @{text"?x\<^sub>i"}. 
47269  560 
\begin{warn} 
561 
The conclusion of a raw proof block is \emph{not} indicated by \isacom{show} 

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

563 
\end{warn} 

564 

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

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

567 
\end{isamarkuptext}% 

568 
*} 

569 

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

571 
proof  

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

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

574 
proof 

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

576 
qed } 

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

578 
qed 

579 

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

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

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

583 
\isacom{note} command: 

584 
\begin{quote} 

55359  585 
\indexed{\isacom{note}}{note} \ @{text"name = this"} 
47269  586 
\end{quote} 
587 
This introduces a new name @{text name} that refers to @{text this}, 

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

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

590 

54436  591 
\subsection*{Exercises} 
52706  592 

52661  593 
\exercise 
594 
Give a readable, structured proof of the following lemma: 

595 
*} 

54218  596 
lemma assumes T: "\<forall>x y. T x y \<or> T y x" 
597 
and A: "\<forall>x y. A x y \<and> A y x \<longrightarrow> x = y" 

598 
and TA: "\<forall>x y. T x y \<longrightarrow> A x y" and "A x y" 

599 
shows "T x y" 

52661  600 
(*<*)oops(*>*) 
601 
text{* 

602 
\endexercise 

603 

52706  604 
\exercise 
605 
Give a readable, structured proof of the following lemma: 

606 
*} 

607 
lemma "(\<exists>ys zs. xs = ys @ zs \<and> length ys = length zs) 

608 
\<or> (\<exists>ys zs. xs = ys @ zs \<and> length ys = length zs + 1)" 

609 
(*<*)oops(*>*) 

610 
text{* 

611 
Hint: There are predefined functions @{const_typ take} and @{const_typ drop} 

612 
such that @{text"take k [x\<^sub>1,\<dots>] = [x\<^sub>1,\<dots>,x\<^sub>k]"} and 

54218  613 
@{text"drop k [x\<^sub>1,\<dots>] = [x\<^bsub>k+1\<^esub>,\<dots>]"}. Let sledgehammer find and apply 
614 
the relevant @{const take} and @{const drop} lemmas for you. 

52706  615 
\endexercise 
616 

54218  617 

52361  618 
\section{Case Analysis and Induction} 
55361  619 

52361  620 
\subsection{Datatype Case Analysis} 
55361  621 
\index{case analysis(} 
47269  622 

47711  623 
We have seen case analysis on formulas. Now we want to distinguish 
47269  624 
which form some term takes: is it @{text 0} or of the form @{term"Suc n"}, 
625 
is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example 

47711  626 
proof by case analysis on the form of @{text xs}: 
47269  627 
*} 
628 

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

630 
proof (cases xs) 

631 
assume "xs = []" 

632 
thus ?thesis by simp 

633 
next 

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

635 
thus ?thesis by simp 

636 
qed 

637 

55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55389
diff
changeset

638 
text{*\index{cases@@{text"cases"}(}Function @{text tl} (''tail'') is defined by @{thm list.sel(2)} and 
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
55389
diff
changeset

639 
@{thm list.sel(3)}. Note that the result type of @{const length} is @{typ nat} 
47269  640 
and @{prop"0  1 = (0::nat)"}. 
641 

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

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

644 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

645 
\isacom{fix} \ @{text"x\<^sub>1 \<dots> x\<^sub>n"} \isacom{assume} @{text"\"t = C x\<^sub>1 \<dots> x\<^sub>n\""} 
55361  646 
\end{quote}\index{case@\isacom{case}(} 
47269  647 
Each case can be written in a more compact form by means of the \isacom{case} 
648 
command: 

649 
\begin{quote} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

650 
\isacom{case} @{text "(C x\<^sub>1 \<dots> x\<^sub>n)"} 
47269  651 
\end{quote} 
47704  652 
This is equivalent to the explicit \isacom{fix}\isacom{assume} line 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

653 
but also gives the assumption @{text"\"t = C x\<^sub>1 \<dots> x\<^sub>n\""} a name: @{text C}, 
47269  654 
like the constructor. 
655 
Here is the \isacom{case} version of the proof above: 

656 
*} 

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

658 
proof (cases xs) 

659 
case Nil 

660 
thus ?thesis by simp 

661 
next 

662 
case (Cons y ys) 

663 
thus ?thesis by simp 

664 
qed 

665 

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

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

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

669 
into the proof of the claim. 

55361  670 
\index{case analysis)} 
47269  671 

52361  672 
\subsection{Structural Induction} 
55361  673 
\index{induction(} 
674 
\index{structural induction(} 

47269  675 

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

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

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

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

680 
*} 

681 

47711  682 
lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" 
47269  683 
proof (induction n) 
684 
show "\<Sum>{0..0::nat} = 0*(0+1) div 2" by simp 

685 
next 

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

47711  687 
thus "\<Sum>{0..Suc n} = Suc n*(Suc n+1) div 2" by simp 
47269  688 
qed 
689 

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

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

692 
write and maintain. Here is how pattern 

693 
matching can completely avoid any duplication: *} 

694 

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

696 
proof (induction n) 

697 
show "?P 0" by simp 

698 
next 

699 
fix n assume "?P n" 

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

701 
qed 

702 

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

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

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

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

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

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

709 

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

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

712 
*} 

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

714 
proof (induction n) 

715 
case 0 

716 
show ?case by simp 

717 
next 

718 
case (Suc n) 

719 
thus ?case by simp 

720 
qed 

721 

722 
text{* 

55361  723 
The unknown @{text"?case"}\index{case?@@{text"?case"}(} is set in each case to the required 
58504  724 
claim, i.e., @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof, 
47269  725 
without requiring the user to define a @{text "?P"}. The general 
726 
pattern for induction over @{typ nat} is shown on the lefthand side: 

727 
*}text_raw{* 

728 
\begin{tabular}{@ {}ll@ {}} 

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

730 
\isa{% 

731 
*} 

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

733 
show "P(n)" 

734 
proof (induction n) 

735 
case 0 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

736 
text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{1ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

737 
show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  738 
next 
739 
case (Suc n) 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

740 
text_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{1ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

741 
show ?case (*<*)sorry(*>*) text_raw{*\ $\dots$\\*} 
47269  742 
qed(*<*)qed(*>*) 
743 

744 
text_raw {* } 

745 
\end{minipage} 

746 
& 

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

748 
~\\ 

749 
~\\ 

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

751 
~\\ 

752 
~\\ 

753 
~\\[1ex] 

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

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

756 
\end{minipage} 

757 
\end{tabular} 

758 
\medskip 

759 
*} 

760 
text{* 

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

762 
on the left stands for. 

763 

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

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

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

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

49837  768 
\isacom{show}~@{text"\"P(n)\""} by 
769 
\mbox{\isacom{show}~@{text"\"A(n) \<Longrightarrow> P(n)\""}} 

47269  770 
then \isacom{case}~@{text 0} stands for 
771 
\begin{quote} 

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

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

774 
\end{quote} 

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

776 
\begin{quote} 

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

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

47306  779 
\begin{tabular}[t]{l}@{text"\"A(n) \<Longrightarrow> P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\ 
47269  780 
\isacom{let} @{text"?case = \"P(Suc n)\""} 
781 
\end{quote} 

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

56989  783 
into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \<Longrightarrow> P(n)"}), 
47269  784 
and @{text"Suc.prems"}, the premises of the goal being proved 
785 
(here @{text"A(Suc n)"}). 

786 

787 
Induction works for any datatype. 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

788 
Proving a goal @{text"\<lbrakk> A\<^sub>1(x); \<dots>; A\<^sub>k(x) \<rbrakk> \<Longrightarrow> P(x)"} 
47269  789 
by induction on @{text x} generates a proof obligation for each constructor 
55361  790 
@{text C} of the datatype. The command \isacom{case}~@{text"(C x\<^sub>1 \<dots> x\<^sub>n)"} 
47269  791 
performs the following steps: 
792 
\begin{enumerate} 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

793 
\item \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"} 
55361  794 
\item \isacom{assume} the induction hypotheses (calling them @{text C.IH}\index{IH@@{text".IH"}}) 
795 
and the premises \mbox{@{text"A\<^sub>i(C x\<^sub>1 \<dots> x\<^sub>n)"}} (calling them @{text"C.prems"}\index{prems@@{text".prems"}}) 

47269  796 
and calling the whole list @{text C} 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

797 
\item \isacom{let} @{text"?case = \"P(C x\<^sub>1 \<dots> x\<^sub>n)\""} 
47269  798 
\end{enumerate} 
55361  799 
\index{structural induction)} 
47269  800 

52361  801 
\subsection{Rule Induction} 
55361  802 
\index{rule induction(} 
47269  803 

804 
Recall the inductive and recursive definitions of even numbers in 

805 
\autoref{sec:inductivedefs}: 

806 
*} 

807 

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

809 
ev0: "ev 0"  

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

811 

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

813 
"even 0 = True"  

814 
"even (Suc 0) = False"  

815 
"even (Suc(Suc n)) = even n" 

816 

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

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

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

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

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

822 
\isa{% 

823 
*} 

824 

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

826 
proof(induction rule: ev.induct) 

827 
case ev0 

828 
show ?case by simp 

829 
next 

830 
case evSS 

831 

832 

833 

834 
thus ?case by simp 

835 
qed 

836 

837 
text_raw {* } 

838 
\end{minipage} 

839 
& 

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

841 
~\\ 

842 
~\\ 

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

844 
~\\ 

845 
~\\ 

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

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

47306  848 
\begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\ 
849 
\isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\ 

47269  850 
\end{minipage} 
851 
\end{tabular} 

852 
\medskip 

853 
*} 

854 
text{* 

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

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

857 
inductive definition. 

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

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

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

861 
is the induction hypothesis. 

862 
\begin{warn} 

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

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

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

58522  866 
@{thm[source] ev.ev0} and @{thm[source] ev.evSS}. 
47269  867 
\end{warn} 
868 

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

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

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

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

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

874 
\begin{quote} 

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

876 
\end{quote} 

58605  877 
like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions. 
47269  878 
The name @{text m} is an arbitrary choice. As a result, 
879 
case @{thm[source] evSS} is derived from a renamed version of 

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

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

882 
*} 

883 

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

885 
proof(induction rule: ev.induct) 

886 
case ev0 show ?case by simp 

887 
next 

888 
case (evSS m) 

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

890 
thus ?case using `even m` by blast 

891 
qed 

892 

893 
text{* 

894 
\indent 

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

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

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

897 
be called @{text "rule\<^sub>1"}, \dots, @{text "rule\<^sub>n"}. A proof by rule 
55361  898 
induction follows this pattern:\index{inductionrule@@{text"induction ... rule:"}} 
47269  899 
*} 
900 

901 
(*<*) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

902 
inductive I where rule\<^sub>1: "I()"  rule\<^sub>2: "I()"  rule\<^sub>n: "I()" 
47269  903 
lemma "I x \<Longrightarrow> P x" proof(*>*) 
904 
show "I x \<Longrightarrow> P x" 

905 
proof(induction rule: I.induct) 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

906 
case rule\<^sub>1 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

907 
text_raw{*\\[.4ex]\mbox{}\ \ $\vdots$\\[.4ex]\mbox{}\hspace{1ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

908 
show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  909 
next 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

910 
text_raw{*\\[.4ex]$\vdots$\\[.4ex]\mbox{}\hspace{1ex}*} 
47269  911 
(*<*) 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

912 
case rule\<^sub>2 
47269  913 
show ?case sorry 
914 
(*>*) 

915 
next 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

916 
case rule\<^sub>n 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

917 
text_raw{*\\[.4ex]\mbox{}\ \ $\vdots$\\[.4ex]\mbox{}\hspace{1ex}*} 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58605
diff
changeset

918 
show ?case (*<*)sorry(*>*)text_raw{*\ $\dots$\\*} 
47269  919 
qed(*<*)qed(*>*) 
920 

921 
text{* 

922 
One can provide explicit variable names by writing 

53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

923 
\isacom{case}~@{text"(rule\<^sub>i x\<^sub>1 \<dots> x\<^sub>k)"}, thus renaming the first @{text k} 
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

924 
free variables in rule @{text i} to @{text"x\<^sub>1 \<dots> x\<^sub>k"}, 
47269  925 
going through rule @{text i} from left to right. 
926 

52361  927 
\subsection{Assumption Naming} 
51443  928 
\label{sec:assmnaming} 
47269  929 

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

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

932 
\begin{description} 

55361  933 
\item[@{text name.IH}]\index{IH@@{text".IH"}} contains the induction hypotheses. 
934 
\item[@{text name.hyps}]\index{hyps@@{text".hyps"}} contains all the other hypotheses of this case in the 

47269  935 
induction rule. For rule inductions these are the hypotheses of rule 
936 
@{text name}, for structural inductions these are empty. 

55361  937 
\item[@{text name.prems}]\index{prems@@{text".prems"}} contains the (suitably instantiated) premises 
58504  938 
of the statement being proved, i.e., the @{text A\<^sub>i} when 
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52718
diff
changeset

939 
proving @{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}. 
47269  940 
\end{description} 
941 
\begin{warn} 

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

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

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

945 
\end{warn} 

946 

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

58602  948 
often need to refer to specific assumptions  just @{text name} or even 
47269  949 
@{text name.prems} and @{text name.IH} can be too unspecific. 
58504  950 
This is where the indexing of fact lists comes in handy, e.g., 
47269  951 
@{text"name.IH(2)"} or @{text"name.prems(12)"}. 
952 

52361  953 
\subsection{Rule Inversion} 
954 
\label{sec:ruleinversion} 

55361  955 
\index{rule inversion(} 
47269  956 

47711  957 
Rule inversion is case analysis of which rule could have been used to 
55361  958 
derive some fact. The name \conceptnoidx{rule inversion} emphasizes that we are 
47269  959 
reasoning backwards: by which rules could some given fact have been proved? 
960 
For the inductive definition of @{const ev}, rule inversion can be summarized 

961 
like this: 

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

47711  963 
The realisation in Isabelle is a case analysis. 
47269  964 
A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n  2)"}. We 
965 
already went through the details informally in \autoref{sec:Logic:even}. This 

966 
is the Isar proof: 

967 
*} 

968 
(*<*) 

969 
notepad 

970 
begin fix n 

971 
(*>*) 

972 
assume "ev n" 

973 
from this have "ev(n  2)" 

974 
proof cases 

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

976 
next 

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

978 
qed 

979 
(*<*) 

980 
end 

981 
(*>*) 

982 

47711  983 
text{* The key point here is that a case analysis over some inductively 
47269  984 
defined predicate is triggered by piping the given fact 
985 
(here: \isacom{from}~@{text this}) into a proof by @{text cases}. 

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

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

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

56989  989 
of the case; there is no finegrained naming schema like there is for induction. 
47269  990 

47704  991 
Sometimes some rules could not have been used to derive the given fact 
47269  992 
because constructors clash. As an extreme example consider 
993 
rule inversion applied to @{prop"ev(Suc 0)"}: neither rule @{text ev0} nor 

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

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

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

997 
*} 

998 
(*<*) 

999 
notepad begin fix P 

1000 
(*>*) 

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

1002 
(*<*) 

1003 
end 

1004 
(*>*) 

1005 

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

1007 

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

1009 
proof 

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

1011 
qed 

1012 

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

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

51443  1015 

52361  1016 
\subsection{Advanced Rule Induction} 
51445  1017 
\label{sec:advancedruleinduction} 
51443  1018 

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

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

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

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

1023 
\begin{isabelle} 

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

1025 
\end{isabelle} 

1026 
Applying the standard form of 

54577  1027 
rule induction in such a situation will lead to strange and typically unprovable goals. 
51443  1028 
We can easily reduce this situation to the standard one by introducing 
1029 
new variables @{text x}, @{text y}, @{text z} and reformulating the goal like this: 

1030 
\begin{isabelle} 

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

1032 
\end{isabelle} 

56989  1033 
Standard rule induction will work fine now, provided the free variables in 
58502  1034 
@{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}. 
51443  1035 

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

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

1038 
\begin{isabelle} 

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

55361  1040 
\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}\index{inductionrule@@{text"induction ... rule:"}}\index{arbitrary@@{text"arbitrary:"}} 
51443  1041 
\end{isabelle} 
58605  1042 
Like for rule inversion, cases that are impossible because of constructor clashes 
51443  1043 
will not show up at all. Here is a concrete example: *} 
1044 

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

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

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

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

54577  1049 
proof "contradiction" 
51443  1050 
assume "ev(Suc n)" 
1051 
thus False 

1052 
proof cases "rule inversion" 

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

1054 
thus False using IH by auto 

1055 
qed 

1056 
qed 

1057 
qed 

1058 

1059 
text{* 

1060 
Remarks: 

1061 
\begin{itemize} 

1062 
\item 

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

1064 
This is merely for greater clarity. 

1065 
\item 

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

1067 
\item 

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

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

1070 
\item 

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

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

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

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

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

1076 
\end{itemize} 

1077 
\begin{warn} 

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

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

56989  1080 
the induction hypotheses are instead found under the name @{text hyps}, 
1081 
as they are for the simpler 

51443  1082 
@{text induct} method. 
1083 
\end{warn} 

55361  1084 
\index{induction)} 
1085 
\index{cases@@{text"cases"})} 

1086 
\index{case@\isacom{case})} 

1087 
\index{case?@@{text"?case"})} 

1088 
\index{rule induction)} 

1089 
\index{rule inversion)} 

54218  1090 

54436  1091 
\subsection*{Exercises} 
52593  1092 

54232  1093 

1094 
\exercise 

54292  1095 
Give a structured proof by rule inversion: 
54232  1096 
*} 
1097 

1098 
lemma assumes a: "ev(Suc(Suc n))" shows "ev n" 

1099 
(*<*)oops(*>*) 

1100 

1101 
text{* 

1102 
\endexercise 

1103 

52593  1104 
\begin{exercise} 
54232  1105 
Give a structured proof of @{prop "\<not> ev(Suc(Suc(Suc 0)))"} 
1106 
by rule inversions. If there are no cases to be proved you can close 

54218  1107 
a proof immediateley with \isacom{qed}. 
1108 
\end{exercise} 

1109 

1110 
\begin{exercise} 

54292  1111 
Recall predicate @{text star} from \autoref{sec:star} and @{text iter} 
1112 
from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \<Longrightarrow> star r x y"} 

56989  1113 
in a structured style; do not just sledgehammer each case of the 
54292  1114 
required induction. 
1115 
\end{exercise} 

1116 

1117 
\begin{exercise} 

52593  1118 
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"} 
1119 
and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}. 

1120 
\end{exercise} 

47269  1121 
*} 
1122 

1123 
(*<*) 

1124 
end 

1125 
(*>*) 