author  krauss 
Tue, 01 Oct 2013 23:46:46 +0200  
changeset 54017  2a3c07f49615 
parent 53107  57c7294eac0a 
child 54295  45a5523d4a63 
permissions  rwrr 
50530  1 
(* Title: Doc/Functions/Functions.thy 
21212  2 
Author: Alexander Krauss, TU Muenchen 
3 

4 
Tutorial for function definitions with the new "function" package. 

5 
*) 

6 

7 
theory Functions 

8 
imports Main 

9 
begin 

10 

23188  11 
section {* Function Definitions for Dummies *} 
21212  12 

13 
text {* 

14 
In most cases, defining a recursive function is just as simple as other definitions: 

23003  15 
*} 
21212  16 

17 
fun fib :: "nat \<Rightarrow> nat" 

18 
where 

19 
"fib 0 = 1" 

20 
 "fib (Suc 0) = 1" 

21 
 "fib (Suc (Suc n)) = fib n + fib (Suc n)" 

22 

23 
text {* 

23003  24 
The syntax is rather selfexplanatory: We introduce a function by 
25091
a2ae7f71613d
Updated function tutorial: Types can be inferred and need not be given anymore
krauss
parents:
23805
diff
changeset

25 
giving its name, its type, 
a2ae7f71613d
Updated function tutorial: Types can be inferred and need not be given anymore
krauss
parents:
23805
diff
changeset

26 
and a set of defining recursive equations. 
a2ae7f71613d
Updated function tutorial: Types can be inferred and need not be given anymore
krauss
parents:
23805
diff
changeset

27 
If we leave out the type, the most general type will be 
a2ae7f71613d
Updated function tutorial: Types can be inferred and need not be given anymore
krauss
parents:
23805
diff
changeset

28 
inferred, which can sometimes lead to surprises: Since both @{term 
25278  29 
"1::nat"} and @{text "+"} are overloaded, we would end up 
25091
a2ae7f71613d
Updated function tutorial: Types can be inferred and need not be given anymore
krauss
parents:
23805
diff
changeset

30 
with @{text "fib :: nat \<Rightarrow> 'a::{one,plus}"}. 
23003  31 
*} 
32 

33 
text {* 

34 
The function always terminates, since its argument gets smaller in 

23188  35 
every recursive call. 
36 
Since HOL is a logic of total functions, termination is a 

37 
fundamental requirement to prevent inconsistencies\footnote{From the 

38 
\qt{definition} @{text "f(n) = f(n) + 1"} we could prove 

39 
@{text "0 = 1"} by subtracting @{text "f(n)"} on both sides.}. 

40 
Isabelle tries to prove termination automatically when a definition 

41 
is made. In \S\ref{termination}, we will look at cases where this 

42 
fails and see what to do then. 

21212  43 
*} 
44 

45 
subsection {* Pattern matching *} 

46 

22065  47 
text {* \label{patmatch} 
23003  48 
Like in functional programming, we can use pattern matching to 
49 
define functions. At the moment we will only consider \emph{constructor 

21212  50 
patterns}, which only consist of datatype constructors and 
23805  51 
variables. Furthermore, patterns must be linear, i.e.\ all variables 
52 
on the left hand side of an equation must be distinct. In 

53 
\S\ref{genpats} we discuss more general pattern matching. 

21212  54 

55 
If patterns overlap, the order of the equations is taken into 

56 
account. The following function inserts a fixed element between any 

57 
two elements of a list: 

58 
*} 

59 

60 
fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" 

61 
where 

62 
"sep a (x#y#xs) = x # a # sep a (y # xs)" 

63 
 "sep a xs = xs" 

64 

65 
text {* 

23188  66 
Overlapping patterns are interpreted as \qt{increments} to what is 
21212  67 
already there: The second equation is only meant for the cases where 
68 
the first one does not match. Consequently, Isabelle replaces it 

22065  69 
internally by the remaining cases, making the patterns disjoint: 
21212  70 
*} 
71 

22065  72 
thm sep.simps 
21212  73 

22065  74 
text {* @{thm [display] sep.simps[no_vars]} *} 
21212  75 

76 
text {* 

23805  77 
\noindent The equations from function definitions are automatically used in 
21212  78 
simplification: 
79 
*} 

80 

23188  81 
lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]" 
21212  82 
by simp 
83 

84 
subsection {* Induction *} 

85 

22065  86 
text {* 
87 

23805  88 
Isabelle provides customized induction rules for recursive 
89 
functions. These rules follow the recursive structure of the 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

90 
definition. Here is the rule @{thm [source] sep.induct} arising from the 
23805  91 
above definition of @{const sep}: 
92 

93 
@{thm [display] sep.induct} 

94 

95 
We have a step case for list with at least two elements, and two 

96 
base cases for the zero and the oneelement list. Here is a simple 

97 
proof about @{const sep} and @{const map} 

98 
*} 

23188  99 

23805  100 
lemma "map f (sep x ys) = sep (f x) (map f ys)" 
101 
apply (induct x ys rule: sep.induct) 

102 

103 
txt {* 

104 
We get three cases, like in the definition. 

105 

106 
@{subgoals [display]} 

107 
*} 

108 

109 
apply auto 

110 
done 

111 
text {* 

23188  112 

113 
With the \cmd{fun} command, you can define about 80\% of the 

114 
functions that occur in practice. The rest of this tutorial explains 

115 
the remaining 20\%. 

22065  116 
*} 
21212  117 

118 

23188  119 
section {* fun vs.\ function *} 
21212  120 

121 
text {* 

23188  122 
The \cmd{fun} command provides a 
21212  123 
convenient shorthand notation for simple function definitions. In 
124 
this mode, Isabelle tries to solve all the necessary proof obligations 

27026  125 
automatically. If any proof fails, the definition is 
22065  126 
rejected. This can either mean that the definition is indeed faulty, 
127 
or that the default proof procedures are just not smart enough (or 

128 
rather: not designed) to handle the definition. 

129 

23188  130 
By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or 
131 
solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows: 

22065  132 

133 
\end{isamarkuptext} 

134 

135 

23188  136 
\[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt} 
137 
\cmd{fun} @{text "f :: \<tau>"}\\% 

138 
\cmd{where}\\% 

139 
\hspace*{2ex}{\it equations}\\% 

140 
\hspace*{2ex}\vdots\vspace*{6pt} 

141 
\end{minipage}\right] 

142 
\quad\equiv\quad 

27026  143 
\left[\;\begin{minipage}{0.48\textwidth}\vspace{6pt} 
23188  144 
\cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\% 
145 
\cmd{where}\\% 

146 
\hspace*{2ex}{\it equations}\\% 

147 
\hspace*{2ex}\vdots\\% 

22065  148 
\cmd{by} @{text "pat_completeness auto"}\\% 
23188  149 
\cmd{termination by} @{text "lexicographic_order"}\vspace{6pt} 
150 
\end{minipage} 

151 
\right]\] 

21212  152 

22065  153 
\begin{isamarkuptext} 
154 
\vspace*{1em} 

23188  155 
\noindent Some details have now become explicit: 
21212  156 

157 
\begin{enumerate} 

22065  158 
\item The \cmd{sequential} option enables the preprocessing of 
23805  159 
pattern overlaps which we already saw. Without this option, the equations 
21212  160 
must already be disjoint and complete. The automatic completion only 
23188  161 
works with constructor patterns. 
21212  162 

23188  163 
\item A function definition produces a proof obligation which 
164 
expresses completeness and compatibility of patterns (we talk about 

22065  165 
this later). The combination of the methods @{text "pat_completeness"} and 
166 
@{text "auto"} is used to solve this proof obligation. 

21212  167 

168 
\item A termination proof follows the definition, started by the 

23188  169 
\cmd{termination} command. This will be explained in \S\ref{termination}. 
22065  170 
\end{enumerate} 
171 
Whenever a \cmd{fun} command fails, it is usually a good idea to 

172 
expand the syntax to the more verbose \cmd{function} form, to see 

173 
what is actually going on. 

21212  174 
*} 
175 

176 

23188  177 
section {* Termination *} 
21212  178 

23188  179 
text {*\label{termination} 
23805  180 
The method @{text "lexicographic_order"} is the default method for 
181 
termination proofs. It can prove termination of a 

23188  182 
certain class of functions by searching for a suitable lexicographic 
183 
combination of size measures. Of course, not all functions have such 

23805  184 
a simple termination argument. For them, we can specify the termination 
185 
relation manually. 

23188  186 
*} 
187 

188 
subsection {* The {\tt relation} method *} 

189 
text{* 

21212  190 
Consider the following function, which sums up natural numbers up to 
22065  191 
@{text "N"}, using a counter @{text "i"}: 
21212  192 
*} 
193 

194 
function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

195 
where 

196 
"sum i N = (if i > N then 0 else i + sum (Suc i) N)" 

22065  197 
by pat_completeness auto 
21212  198 

199 
text {* 

22065  200 
\noindent The @{text "lexicographic_order"} method fails on this example, because none of the 
23805  201 
arguments decreases in the recursive call, with respect to the standard size ordering. 
202 
To prove termination manually, we must provide a custom wellfounded relation. 

21212  203 

204 
The termination argument for @{text "sum"} is based on the fact that 

205 
the \emph{difference} between @{text "i"} and @{text "N"} gets 

206 
smaller in every step, and that the recursion stops when @{text "i"} 

23805  207 
is greater than @{text "N"}. Phrased differently, the expression 
208 
@{text "N + 1  i"} always decreases. 

21212  209 

22065  210 
We can use this expression as a measure function suitable to prove termination. 
21212  211 
*} 
212 

27026  213 
termination sum 
23188  214 
apply (relation "measure (\<lambda>(i,N). N + 1  i)") 
21212  215 

23188  216 
txt {* 
23003  217 
The \cmd{termination} command sets up the termination goal for the 
23188  218 
specified function @{text "sum"}. If the function name is omitted, it 
23003  219 
implicitly refers to the last function definition. 
220 

22065  221 
The @{text relation} method takes a relation of 
222 
type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of 

223 
the function. If the function has multiple curried arguments, then 

224 
these are packed together into a tuple, as it happened in the above 

225 
example. 

21212  226 

27026  227 
The predefined function @{term[source] "measure :: ('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set"} constructs a 
23188  228 
wellfounded relation from a mapping into the natural numbers (a 
229 
\emph{measure function}). 

22065  230 

231 
After the invocation of @{text "relation"}, we must prove that (a) 

232 
the relation we supplied is wellfounded, and (b) that the arguments 

233 
of recursive calls indeed decrease with respect to the 

23188  234 
relation: 
235 

236 
@{subgoals[display,indent=0]} 

22065  237 

23188  238 
These goals are all solved by @{text "auto"}: 
239 
*} 

240 

241 
apply auto 

242 
done 

243 

244 
text {* 

22065  245 
Let us complicate the function a little, by adding some more 
246 
recursive calls: 

21212  247 
*} 
248 

249 
function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

250 
where 

251 
"foo i N = (if i > N 

252 
then (if N = 0 then 0 else foo 0 (N  1)) 

253 
else i + foo (Suc i) N)" 

254 
by pat_completeness auto 

255 

256 
text {* 

257 
When @{text "i"} has reached @{text "N"}, it starts at zero again 

258 
and @{text "N"} is decremented. 

259 
This corresponds to a nested 

260 
loop where one index counts up and the other down. Termination can 

261 
be proved using a lexicographic combination of two measures, namely 

22065  262 
the value of @{text "N"} and the above difference. The @{const 
263 
"measures"} combinator generalizes @{text "measure"} by taking a 

264 
list of measure functions. 

21212  265 
*} 
266 

267 
termination 

22065  268 
by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1  i]") auto 
21212  269 

23188  270 
subsection {* How @{text "lexicographic_order"} works *} 
271 

272 
(*fun fails :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 

273 
where 

274 
"fails a [] = a" 

275 
 "fails a (x#xs) = fails (x + a) (x # xs)" 

276 
*) 

23003  277 

278 
text {* 

23188  279 
To see how the automatic termination proofs work, let's look at an 
280 
example where it fails\footnote{For a detailed discussion of the 

281 
termination prover, see \cite{bulwahnKN07}}: 

282 

283 
\end{isamarkuptext} 

284 
\cmd{fun} @{text "fails :: \"nat \<Rightarrow> nat list \<Rightarrow> nat\""}\\% 

285 
\cmd{where}\\% 

286 
\hspace*{2ex}@{text "\"fails a [] = a\""}\\% 

287 
\hspace*{1.5ex}@{text "\"fails a (x#xs) = fails (x + a) (x#xs)\""}\\ 

288 
\begin{isamarkuptext} 

289 

290 
\noindent Isabelle responds with the following error: 

291 

292 
\begin{isabelle} 

23805  293 
*** Unfinished subgoals:\newline 
294 
*** (a, 1, <):\newline 

295 
*** \ 1.~@{text "\<And>x. x = 0"}\newline 

296 
*** (a, 1, <=):\newline 

297 
*** \ 1.~False\newline 

298 
*** (a, 2, <):\newline 

299 
*** \ 1.~False\newline 

23188  300 
*** Calls:\newline 
301 
*** a) @{text "(a, x # xs) >> (x + a, x # xs)"}\newline 

302 
*** Measures:\newline 

303 
*** 1) @{text "\<lambda>x. size (fst x)"}\newline 

304 
*** 2) @{text "\<lambda>x. size (snd x)"}\newline 

23805  305 
*** Result matrix:\newline 
306 
*** \ \ \ \ 1\ \ 2 \newline 

307 
*** a: ? <= \newline 

308 
*** Could not find lexicographic termination order.\newline 

23188  309 
*** At command "fun".\newline 
310 
\end{isabelle} 

23003  311 
*} 
23188  312 
text {* 
28040  313 
The key to this error message is the matrix at the bottom. The rows 
23188  314 
of that matrix correspond to the different recursive calls (In our 
315 
case, there is just one). The columns are the function's arguments 

316 
(expressed through different measure functions, which map the 

317 
argument tuple to a natural number). 

318 

319 
The contents of the matrix summarize what is known about argument 

320 
descents: The second argument has a weak descent (@{text "<="}) at the 

321 
recursive call, and for the first argument nothing could be proved, 

23805  322 
which is expressed by @{text "?"}. In general, there are the values 
323 
@{text "<"}, @{text "<="} and @{text "?"}. 

23188  324 

325 
For the failed proof attempts, the unfinished subgoals are also 

23805  326 
printed. Looking at these will often point to a missing lemma. 
33856  327 
*} 
23188  328 

33856  329 
subsection {* The @{text size_change} method *} 
23003  330 

33856  331 
text {* 
332 
Some termination goals that are beyond the powers of 

333 
@{text lexicographic_order} can be solved automatically by the 

334 
more powerful @{text size_change} method, which uses a variant of 

335 
the sizechange principle, together with some other 

336 
techniques. While the details are discussed 

337 
elsewhere\cite{krauss_phd}, 

338 
here are a few typical situations where 

339 
@{text lexicographic_order} has difficulties and @{text size_change} 

340 
may be worth a try: 

341 
\begin{itemize} 

342 
\item Arguments are permuted in a recursive call. 

343 
\item Several mutually recursive functions with multiple arguments. 

344 
\item Unusual control flow (e.g., when some recursive calls cannot 

345 
occur in sequence). 

346 
\end{itemize} 

23003  347 

33856  348 
Loading the theory @{text Multiset} makes the @{text size_change} 
349 
method a bit stronger: it can then use multiset orders internally. 

350 
*} 

21212  351 

352 
section {* Mutual Recursion *} 

353 

354 
text {* 

355 
If two or more functions call one another mutually, they have to be defined 

23188  356 
in one step. Here are @{text "even"} and @{text "odd"}: 
21212  357 
*} 
358 

22065  359 
function even :: "nat \<Rightarrow> bool" 
360 
and odd :: "nat \<Rightarrow> bool" 

21212  361 
where 
362 
"even 0 = True" 

363 
 "odd 0 = False" 

364 
 "even (Suc n) = odd n" 

365 
 "odd (Suc n) = even n" 

22065  366 
by pat_completeness auto 
21212  367 

368 
text {* 

23188  369 
To eliminate the mutual dependencies, Isabelle internally 
21212  370 
creates a single function operating on the sum 
23188  371 
type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are 
372 
defined as projections. Consequently, termination has to be proved 

21212  373 
simultaneously for both functions, by specifying a measure on the 
374 
sum type: 

375 
*} 

376 

377 
termination 

23188  378 
by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n  Inr n \<Rightarrow> n)") auto 
379 

380 
text {* 

381 
We could also have used @{text lexicographic_order}, which 

382 
supports mutual recursive termination proofs to a certain extent. 

383 
*} 

22065  384 

385 
subsection {* Induction for mutual recursion *} 

386 

387 
text {* 

388 

389 
When functions are mutually recursive, proving properties about them 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

390 
generally requires simultaneous induction. The induction rule @{thm [source] "even_odd.induct"} 
23188  391 
generated from the above definition reflects this. 
22065  392 

393 
Let us prove something about @{const even} and @{const odd}: 

394 
*} 

395 

23188  396 
lemma even_odd_mod2: 
22065  397 
"even n = (n mod 2 = 0)" 
398 
"odd n = (n mod 2 = 1)" 

399 

400 
txt {* 

401 
We apply simultaneous induction, specifying the induction variable 

402 
for both goals, separated by \cmd{and}: *} 

403 

404 
apply (induct n and n rule: even_odd.induct) 

405 

406 
txt {* 

407 
We get four subgoals, which correspond to the clauses in the 

408 
definition of @{const even} and @{const odd}: 

409 
@{subgoals[display,indent=0]} 

410 
Simplification solves the first two goals, leaving us with two 

411 
statements about the @{text "mod"} operation to prove: 

412 
*} 

413 

414 
apply simp_all 

415 

416 
txt {* 

417 
@{subgoals[display,indent=0]} 

418 

23805  419 
\noindent These can be handled by Isabelle's arithmetic decision procedures. 
22065  420 

421 
*} 

422 

23805  423 
apply arith 
424 
apply arith 

22065  425 
done 
21212  426 

22065  427 
text {* 
23188  428 
In proofs like this, the simultaneous induction is really essential: 
429 
Even if we are just interested in one of the results, the other 

430 
one is necessary to strengthen the induction hypothesis. If we leave 

27026  431 
out the statement about @{const odd} and just write @{term True} instead, 
432 
the same proof fails: 

22065  433 
*} 
434 

23188  435 
lemma failed_attempt: 
22065  436 
"even n = (n mod 2 = 0)" 
437 
"True" 

438 
apply (induct n rule: even_odd.induct) 

439 

440 
txt {* 

441 
\noindent Now the third subgoal is a dead end, since we have no 

23188  442 
useful induction hypothesis available: 
22065  443 

444 
@{subgoals[display,indent=0]} 

445 
*} 

446 

447 
oops 

448 

54017
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

449 
section {* Elimination *} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

450 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

451 
text {* 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

452 
A definition of function @{text f} gives rise to two kinds of elimination rules. Rule @{text f.cases} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

453 
simply describes case analysis according to the patterns used in the definition: 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

454 
*} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

455 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

456 
fun list_to_option :: "'a list \<Rightarrow> 'a option" 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

457 
where 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

458 
"list_to_option [x] = Some x" 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

459 
 "list_to_option _ = None" 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

460 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

461 
thm list_to_option.cases 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

462 
text {* 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

463 
@{thm[display] list_to_option.cases} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

464 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

465 
Note that this rule does not mention the function at all, but only describes the cases used for 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

466 
defining it. In contrast, the rule @{thm[source] list_to_option.elims} also tell us what the function 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

467 
value will be in each case: 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

468 
*} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

469 
thm list_to_option.elims 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

470 
text {* 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

471 
@{thm[display] list_to_option.elims} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

472 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

473 
\noindent 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

474 
This lets us eliminate an assumption of the form @{prop "list_to_option xs = y"} and replace it 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

475 
with the two cases, e.g.: 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

476 
*} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

477 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

478 
lemma "list_to_option xs = y \<Longrightarrow> P" 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

479 
proof (erule list_to_option.elims) 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

480 
fix x assume "xs = [x]" "y = Some x" thus P sorry 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

481 
next 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

482 
assume "xs = []" "y = None" thus P sorry 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

483 
next 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

484 
fix a b xs' assume "xs = a # b # xs'" "y = None" thus P sorry 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

485 
qed 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

486 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

487 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

488 
text {* 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

489 
Sometimes it is convenient to derive specialized versions of the @{text elim} rules above and 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

490 
keep them around as facts explicitly. For example, it is natural to show that if 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

491 
@{prop "list_to_option xs = Some y"}, then @{term xs} must be a singleton. The command 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

492 
\cmd{fun\_cases} derives such facts automatically, by instantiating and simplifying the general 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

493 
elimination rules given some pattern: 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

494 
*} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

495 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

496 
fun_cases list_to_option_SomeE[elim]: "list_to_option xs = Some y" 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

497 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

498 
thm list_to_option_SomeE 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

499 
text {* 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

500 
@{thm[display] list_to_option_SomeE} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

501 
*} 
2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

502 

2a3c07f49615
basic documentation for function elimination rules and fun_cases
krauss
parents:
53107
diff
changeset

503 

23188  504 
section {* General pattern matching *} 
23805  505 
text{*\label{genpats} *} 
22065  506 

23188  507 
subsection {* Avoiding automatic pattern splitting *} 
22065  508 

509 
text {* 

510 

511 
Up to now, we used pattern matching only on datatypes, and the 

512 
patterns were always disjoint and complete, and if they weren't, 

513 
they were made disjoint automatically like in the definition of 

514 
@{const "sep"} in \S\ref{patmatch}. 

515 

23188  516 
This automatic splitting can significantly increase the number of 
517 
equations involved, and this is not always desirable. The following 

518 
example shows the problem: 

22065  519 

23805  520 
Suppose we are modeling incomplete knowledge about the world by a 
23003  521 
threevalued datatype, which has values @{term "T"}, @{term "F"} 
522 
and @{term "X"} for true, false and uncertain propositions, respectively. 

22065  523 
*} 
524 

525 
datatype P3 = T  F  X 

526 

23188  527 
text {* \noindent Then the conjunction of such values can be defined as follows: *} 
22065  528 

529 
fun And :: "P3 \<Rightarrow> P3 \<Rightarrow> P3" 

530 
where 

531 
"And T p = p" 

23003  532 
 "And p T = p" 
533 
 "And p F = F" 

534 
 "And F p = F" 

535 
 "And X X = X" 

21212  536 

537 

22065  538 
text {* 
539 
This definition is useful, because the equations can directly be used 

28040  540 
as simplification rules. But the patterns overlap: For example, 
23188  541 
the expression @{term "And T T"} is matched by both the first and 
542 
the second equation. By default, Isabelle makes the patterns disjoint by 

22065  543 
splitting them up, producing instances: 
544 
*} 

545 

546 
thm And.simps 

547 

548 
text {* 

549 
@{thm[indent=4] And.simps} 

550 

551 
\vspace*{1em} 

23003  552 
\noindent There are several problems with this: 
22065  553 

554 
\begin{enumerate} 

23188  555 
\item If the datatype has many constructors, there can be an 
22065  556 
explosion of equations. For @{const "And"}, we get seven instead of 
23003  557 
five equations, which can be tolerated, but this is just a small 
22065  558 
example. 
559 

23188  560 
\item Since splitting makes the equations \qt{less general}, they 
22065  561 
do not always match in rewriting. While the term @{term "And x F"} 
23188  562 
can be simplified to @{term "F"} with the original equations, a 
22065  563 
(manual) case split on @{term "x"} is now necessary. 
564 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

565 
\item The splitting also concerns the induction rule @{thm [source] 
22065  566 
"And.induct"}. Instead of five premises it now has seven, which 
567 
means that our induction proofs will have more cases. 

568 

569 
\item In general, it increases clarity if we get the same definition 

570 
back which we put in. 

571 
\end{enumerate} 

572 

23188  573 
If we do not want the automatic splitting, we can switch it off by 
574 
leaving out the \cmd{sequential} option. However, we will have to 

575 
prove that our pattern matching is consistent\footnote{This prevents 

576 
us from defining something like @{term "f x = True"} and @{term "f x 

577 
= False"} simultaneously.}: 

22065  578 
*} 
579 

580 
function And2 :: "P3 \<Rightarrow> P3 \<Rightarrow> P3" 

581 
where 

582 
"And2 T p = p" 

23003  583 
 "And2 p T = p" 
584 
 "And2 p F = F" 

585 
 "And2 F p = F" 

586 
 "And2 X X = X" 

22065  587 

588 
txt {* 

23188  589 
\noindent Now let's look at the proof obligations generated by a 
22065  590 
function definition. In this case, they are: 
591 

23188  592 
@{subgoals[display,indent=0]}\vspace{1.2em}\hspace{3cm}\vdots\vspace{1.2em} 
22065  593 

594 
The first subgoal expresses the completeness of the patterns. It has 

595 
the form of an elimination rule and states that every @{term x} of 

23188  596 
the function's input type must match at least one of the patterns\footnote{Completeness could 
22065  597 
be equivalently stated as a disjunction of existential statements: 
598 
@{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or> 

27026  599 
(\<exists>p. x = (F, p)) \<or> (x = (X, X))"}, and you can use the method @{text atomize_elim} to get that form instead.}. If the patterns just involve 
23188  600 
datatypes, we can solve it with the @{text "pat_completeness"} 
601 
method: 

22065  602 
*} 
603 

604 
apply pat_completeness 

605 

606 
txt {* 

607 
The remaining subgoals express \emph{pattern compatibility}. We do 

23188  608 
allow that an input value matches multiple patterns, but in this 
22065  609 
case, the result (i.e.~the right hand sides of the equations) must 
610 
also be equal. For each pair of two patterns, there is one such 

611 
subgoal. Usually this needs injectivity of the constructors, which 

612 
is used automatically by @{text "auto"}. 

613 
*} 

614 

615 
by auto 

43042
0f9534b7ea75
function tutorial: do not omit termination proof, even when discussing other things
krauss
parents:
41847
diff
changeset

616 
termination by (relation "{}") simp 
21212  617 

618 

22065  619 
subsection {* Nonconstructor patterns *} 
21212  620 

23188  621 
text {* 
23805  622 
Most of Isabelle's basic types take the form of inductive datatypes, 
623 
and usually pattern matching works on the constructors of such types. 

624 
However, this need not be always the case, and the \cmd{function} 

625 
command handles other kind of patterns, too. 

23188  626 

23805  627 
One wellknown instance of nonconstructor patterns are 
23188  628 
socalled \emph{$n+k$patterns}, which are a little controversial in 
629 
the functional programming world. Here is the initial fibonacci 

630 
example with $n+k$patterns: 

631 
*} 

632 

633 
function fib2 :: "nat \<Rightarrow> nat" 

634 
where 

635 
"fib2 0 = 1" 

636 
 "fib2 1 = 1" 

637 
 "fib2 (n + 2) = fib2 n + fib2 (Suc n)" 

638 

639 
txt {* 

23805  640 
This kind of matching is again justified by the proof of pattern 
641 
completeness and compatibility. 

23188  642 
The proof obligation for pattern completeness states that every natural number is 
643 
either @{term "0::nat"}, @{term "1::nat"} or @{term "n + 

644 
(2::nat)"}: 

645 

39752
06fc1a79b4bf
removed unnecessary reference poking (cf. f45d332a90e3)
krauss
parents:
33856
diff
changeset

646 
@{subgoals[display,indent=0,goals_limit=1]} 
23188  647 

648 
This is an arithmetic triviality, but unfortunately the 

649 
@{text arith} method cannot handle this specific form of an 

23805  650 
elimination rule. However, we can use the method @{text 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
25688
diff
changeset

651 
"atomize_elim"} to do an adhoc conversion to a disjunction of 
28040  652 
existentials, which can then be solved by the arithmetic decision procedure. 
23805  653 
Pattern compatibility and termination are automatic as usual. 
23188  654 
*} 
26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
25688
diff
changeset

655 
apply atomize_elim 
23805  656 
apply arith 
23188  657 
apply auto 
658 
done 

659 
termination by lexicographic_order 

660 
text {* 

661 
We can stretch the notion of pattern matching even more. The 

662 
following function is not a sensible functional program, but a 

663 
perfectly valid mathematical definition: 

664 
*} 

665 

666 
function ev :: "nat \<Rightarrow> bool" 

667 
where 

668 
"ev (2 * n) = True" 

669 
 "ev (2 * n + 1) = False" 

26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
25688
diff
changeset

670 
apply atomize_elim 
23805  671 
by arith+ 
23188  672 
termination by (relation "{}") simp 
673 

674 
text {* 

27026  675 
This general notion of pattern matching gives you a certain freedom 
676 
in writing down specifications. However, as always, such freedom should 

23188  677 
be used with care: 
678 

679 
If we leave the area of constructor 

680 
patterns, we have effectively departed from the world of functional 

681 
programming. This means that it is no longer possible to use the 

682 
code generator, and expect it to generate ML code for our 

683 
definitions. Also, such a specification might not work very well together with 

684 
simplification. Your mileage may vary. 

685 
*} 

686 

687 

688 
subsection {* Conditional equations *} 

689 

690 
text {* 

691 
The function package also supports conditional equations, which are 

692 
similar to guards in a language like Haskell. Here is Euclid's 

693 
algorithm written with conditional patterns\footnote{Note that the 

694 
patterns are also overlapping in the base case}: 

695 
*} 

696 

697 
function gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

698 
where 

699 
"gcd x 0 = x" 

700 
 "gcd 0 y = y" 

701 
 "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y  x)" 

702 
 "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x  y) (Suc y)" 

26580
c3e597a476fd
Generic conversion and tactic "atomize_elim" to convert elimination rules
krauss
parents:
25688
diff
changeset

703 
by (atomize_elim, auto, arith) 
23188  704 
termination by lexicographic_order 
705 

706 
text {* 

707 
By now, you can probably guess what the proof obligations for the 

708 
pattern completeness and compatibility look like. 

709 

710 
Again, functions with conditional patterns are not supported by the 

711 
code generator. 

712 
*} 

713 

714 

715 
subsection {* Pattern matching on strings *} 

716 

717 
text {* 

23805  718 
As strings (as lists of characters) are normal datatypes, pattern 
23188  719 
matching on them is possible, but somewhat problematic. Consider the 
720 
following definition: 

721 

722 
\end{isamarkuptext} 

723 
\noindent\cmd{fun} @{text "check :: \"string \<Rightarrow> bool\""}\\% 

724 
\cmd{where}\\% 

725 
\hspace*{2ex}@{text "\"check (''good'') = True\""}\\% 

726 
@{text " \"check s = False\""} 

727 
\begin{isamarkuptext} 

728 

23805  729 
\noindent An invocation of the above \cmd{fun} command does not 
23188  730 
terminate. What is the problem? Strings are lists of characters, and 
23805  731 
characters are a datatype with a lot of constructors. Splitting the 
23188  732 
catchall pattern thus leads to an explosion of cases, which cannot 
733 
be handled by Isabelle. 

734 

735 
There are two things we can do here. Either we write an explicit 

736 
@{text "if"} on the right hand side, or we can use conditional patterns: 

737 
*} 

738 

739 
function check :: "string \<Rightarrow> bool" 

740 
where 

741 
"check (''good'') = True" 

742 
 "s \<noteq> ''good'' \<Longrightarrow> check s = False" 

743 
by auto 

43042
0f9534b7ea75
function tutorial: do not omit termination proof, even when discussing other things
krauss
parents:
41847
diff
changeset

744 
termination by (relation "{}") simp 
22065  745 

746 

747 
section {* Partiality *} 

748 

749 
text {* 

750 
In HOL, all functions are total. A function @{term "f"} applied to 

23188  751 
@{term "x"} always has the value @{term "f x"}, and there is no notion 
22065  752 
of undefinedness. 
23188  753 
This is why we have to do termination 
754 
proofs when defining functions: The proof justifies that the 

755 
function can be defined by wellfounded recursion. 

22065  756 

23188  757 
However, the \cmd{function} package does support partiality to a 
758 
certain extent. Let's look at the following function which looks 

759 
for a zero of a given function f. 

23003  760 
*} 
761 

41846
b368a7aee46a
removed support for tailrecursion from function package (now implemented by partial_function)
krauss
parents:
39754
diff
changeset

762 
function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" 
23003  763 
where 
764 
"findzero f n = (if f n = 0 then n else findzero f (Suc n))" 

765 
by pat_completeness auto 

766 

767 
text {* 

23805  768 
\noindent Clearly, any attempt of a termination proof must fail. And without 
29781  769 
that, we do not get the usual rules @{text "findzero.simps"} and 
23003  770 
@{text "findzero.induct"}. So what was the definition good for at all? 
771 
*} 

772 

773 
subsection {* Domain predicates *} 

774 

775 
text {* 

776 
The trick is that Isabelle has not only defined the function @{const findzero}, but also 

777 
a predicate @{term "findzero_dom"} that characterizes the values where the function 

23188  778 
terminates: the \emph{domain} of the function. If we treat a 
779 
partial function just as a total function with an additional domain 

780 
predicate, we can derive simplification and 

781 
induction rules as we do for total functions. They are guarded 

782 
by domain conditions and are called @{text psimps} and @{text 

783 
pinduct}: 

23003  784 
*} 
785 

23805  786 
text {* 
787 
\noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage} 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

788 
\hfill(@{thm [source] "findzero.psimps"}) 
23805  789 
\vspace{1em} 
23003  790 

23805  791 
\noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage} 
53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

792 
\hfill(@{thm [source] "findzero.pinduct"}) 
23003  793 
*} 
794 

795 
text {* 

23188  796 
Remember that all we 
797 
are doing here is use some tricks to make a total function appear 

23003  798 
as if it was partial. We can still write the term @{term "findzero 
799 
(\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal 

800 
to some natural number, although we might not be able to find out 

23188  801 
which one. The function is \emph{underdefined}. 
23003  802 

23805  803 
But it is defined enough to prove something interesting about it. We 
23188  804 
can prove that if @{term "findzero f n"} 
23805  805 
terminates, it indeed returns a zero of @{term f}: 
23003  806 
*} 
807 

808 
lemma findzero_zero: "findzero_dom (f, n) \<Longrightarrow> f (findzero f n) = 0" 

809 

23805  810 
txt {* \noindent We apply induction as usual, but using the partial induction 
23003  811 
rule: *} 
812 

813 
apply (induct f n rule: findzero.pinduct) 

814 

23805  815 
txt {* \noindent This gives the following subgoals: 
23003  816 

817 
@{subgoals[display,indent=0]} 

818 

23805  819 
\noindent The hypothesis in our lemma was used to satisfy the first premise in 
23188  820 
the induction rule. However, we also get @{term 
821 
"findzero_dom (f, n)"} as a local assumption in the induction step. This 

39754  822 
allows unfolding @{term "findzero f n"} using the @{text psimps} 
823 
rule, and the rest is trivial. 

23003  824 
*} 
39754  825 
apply (simp add: findzero.psimps) 
23003  826 
done 
827 

828 
text {* 

829 
Proofs about partial functions are often not harder than for total 

830 
functions. Fig.~\ref{findzero_isar} shows a slightly more 

831 
complicated proof written in Isar. It is verbose enough to show how 

832 
partiality comes into play: From the partial induction, we get an 

833 
additional domain condition hypothesis. Observe how this condition 

834 
is applied when calls to @{term findzero} are unfolded. 

835 
*} 

836 

837 
text_raw {* 

838 
\begin{figure} 

23188  839 
\hrule\vspace{6pt} 
23003  840 
\begin{minipage}{0.8\textwidth} 
841 
\isabellestyle{it} 

842 
\isastyle\isamarkuptrue 

843 
*} 

844 
lemma "\<lbrakk>findzero_dom (f, n); x \<in> {n ..< findzero f n}\<rbrakk> \<Longrightarrow> f x \<noteq> 0" 

845 
proof (induct rule: findzero.pinduct) 

846 
fix f n assume dom: "findzero_dom (f, n)" 

23188  847 
and IH: "\<lbrakk>f n \<noteq> 0; x \<in> {Suc n ..< findzero f (Suc n)}\<rbrakk> \<Longrightarrow> f x \<noteq> 0" 
848 
and x_range: "x \<in> {n ..< findzero f n}" 

23003  849 
have "f n \<noteq> 0" 
850 
proof 

851 
assume "f n = 0" 

39754  852 
with dom have "findzero f n = n" by (simp add: findzero.psimps) 
23003  853 
with x_range show False by auto 
854 
qed 

855 

856 
from x_range have "x = n \<or> x \<in> {Suc n ..< findzero f n}" by auto 

857 
thus "f x \<noteq> 0" 

858 
proof 

859 
assume "x = n" 

860 
with `f n \<noteq> 0` show ?thesis by simp 

861 
next 

23188  862 
assume "x \<in> {Suc n ..< findzero f n}" 
39754  863 
with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by (simp add: findzero.psimps) 
23003  864 
with IH and `f n \<noteq> 0` 
865 
show ?thesis by simp 

866 
qed 

867 
qed 

868 
text_raw {* 

869 
\isamarkupfalse\isabellestyle{tt} 

23188  870 
\end{minipage}\vspace{6pt}\hrule 
23003  871 
\caption{A proof about a partial function}\label{findzero_isar} 
872 
\end{figure} 

873 
*} 

874 

875 
subsection {* Partial termination proofs *} 

876 

877 
text {* 

878 
Now that we have proved some interesting properties about our 

879 
function, we should turn to the domain predicate and see if it is 

880 
actually true for some values. Otherwise we would have just proved 

881 
lemmas with @{term False} as a premise. 

882 

883 
Essentially, we need some introduction rules for @{text 

884 
findzero_dom}. The function package can prove such domain 

885 
introduction rules automatically. But since they are not used very 

23188  886 
often (they are almost never needed if the function is total), this 
887 
functionality is disabled by default for efficiency reasons. So we have to go 

23003  888 
back and ask for them explicitly by passing the @{text 
889 
"(domintros)"} option to the function package: 

890 

23188  891 
\vspace{1ex} 
23003  892 
\noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\% 
893 
\cmd{where}\isanewline% 

894 
\ \ \ldots\\ 

895 

23188  896 
\noindent Now the package has proved an introduction rule for @{text findzero_dom}: 
23003  897 
*} 
898 

899 
thm findzero.domintros 

900 

901 
text {* 

902 
@{thm[display] findzero.domintros} 

903 

904 
Domain introduction rules allow to show that a given value lies in the 

905 
domain of a function, if the arguments of all recursive calls 

906 
are in the domain as well. They allow to do a \qt{single step} in a 

907 
termination proof. Usually, you want to combine them with a suitable 

908 
induction principle. 

909 

910 
Since our function increases its argument at recursive calls, we 

911 
need an induction principle which works \qt{backwards}. We will use 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

912 
@{thm [source] inc_induct}, which allows to do induction from a fixed number 
23003  913 
\qt{downwards}: 
914 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

915 
\begin{center}@{thm inc_induct}\hfill(@{thm [source] "inc_induct"})\end{center} 
23003  916 

23188  917 
Figure \ref{findzero_term} gives a detailed Isar proof of the fact 
23003  918 
that @{text findzero} terminates if there is a zero which is greater 
919 
or equal to @{term n}. First we derive two useful rules which will 

920 
solve the base case and the step case of the induction. The 

23805  921 
induction is then straightforward, except for the unusual induction 
23003  922 
principle. 
923 

924 
*} 

925 

926 
text_raw {* 

927 
\begin{figure} 

23188  928 
\hrule\vspace{6pt} 
23003  929 
\begin{minipage}{0.8\textwidth} 
930 
\isabellestyle{it} 

931 
\isastyle\isamarkuptrue 

932 
*} 

933 
lemma findzero_termination: 

23188  934 
assumes "x \<ge> n" and "f x = 0" 
23003  935 
shows "findzero_dom (f, n)" 
936 
proof  

937 
have base: "findzero_dom (f, x)" 

938 
by (rule findzero.domintros) (simp add:`f x = 0`) 

939 

940 
have step: "\<And>i. findzero_dom (f, Suc i) 

941 
\<Longrightarrow> findzero_dom (f, i)" 

942 
by (rule findzero.domintros) simp 

943 

23188  944 
from `x \<ge> n` show ?thesis 
23003  945 
proof (induct rule:inc_induct) 
23188  946 
show "findzero_dom (f, x)" by (rule base) 
23003  947 
next 
948 
fix i assume "findzero_dom (f, Suc i)" 

23188  949 
thus "findzero_dom (f, i)" by (rule step) 
23003  950 
qed 
951 
qed 

952 
text_raw {* 

953 
\isamarkupfalse\isabellestyle{tt} 

23188  954 
\end{minipage}\vspace{6pt}\hrule 
23003  955 
\caption{Termination proof for @{text findzero}}\label{findzero_term} 
956 
\end{figure} 

957 
*} 

958 

959 
text {* 

960 
Again, the proof given in Fig.~\ref{findzero_term} has a lot of 

961 
detail in order to explain the principles. Using more automation, we 

962 
can also have a short proof: 

963 
*} 

964 

965 
lemma findzero_termination_short: 

966 
assumes zero: "x >= n" 

967 
assumes [simp]: "f x = 0" 

968 
shows "findzero_dom (f, n)" 

23805  969 
using zero 
970 
by (induct rule:inc_induct) (auto intro: findzero.domintros) 

23003  971 

972 
text {* 

23188  973 
\noindent It is simple to combine the partial correctness result with the 
23003  974 
termination lemma: 
975 
*} 

976 

977 
lemma findzero_total_correctness: 

978 
"f x = 0 \<Longrightarrow> f (findzero f 0) = 0" 

979 
by (blast intro: findzero_zero findzero_termination) 

980 

981 
subsection {* Definition of the domain predicate *} 

982 

983 
text {* 

984 
Sometimes it is useful to know what the definition of the domain 

23805  985 
predicate looks like. Actually, @{text findzero_dom} is just an 
23003  986 
abbreviation: 
987 

988 
@{abbrev[display] findzero_dom} 

989 

23188  990 
The domain predicate is the \emph{accessible part} of a relation @{const 
23003  991 
findzero_rel}, which was also created internally by the function 
992 
package. @{const findzero_rel} is just a normal 

23188  993 
inductive predicate, so we can inspect its definition by 
53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

994 
looking at the introduction rules @{thm [source] findzero_rel.intros}. 
23003  995 
In our case there is just a single rule: 
996 

997 
@{thm[display] findzero_rel.intros} 

998 

23188  999 
The predicate @{const findzero_rel} 
23003  1000 
describes the \emph{recursion relation} of the function 
1001 
definition. The recursion relation is a binary relation on 

1002 
the arguments of the function that relates each argument to its 

1003 
recursive calls. In general, there is one introduction rule for each 

1004 
recursive call. 

1005 

23805  1006 
The predicate @{term "accp findzero_rel"} is the accessible part of 
23003  1007 
that relation. An argument belongs to the accessible part, if it can 
23188  1008 
be reached in a finite number of steps (cf.~its definition in @{text 
29781  1009 
"Wellfounded.thy"}). 
23003  1010 

1011 
Since the domain predicate is just an abbreviation, you can use 

23805  1012 
lemmas for @{const accp} and @{const findzero_rel} directly. Some 
53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

1013 
lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source] 
23805  1014 
accp_downward}, and of course the introduction and elimination rules 
53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

1015 
for the recursion relation @{thm [source] "findzero_rel.intros"} and @{thm 
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

1016 
[source] "findzero_rel.cases"}. 
23003  1017 
*} 
1018 

1019 
section {* Nested recursion *} 

1020 

1021 
text {* 

1022 
Recursive calls which are nested in one another frequently cause 

1023 
complications, since their termination proof can depend on a partial 

1024 
correctness property of the function itself. 

1025 

1026 
As a small example, we define the \qt{nested zero} function: 

1027 
*} 

1028 

1029 
function nz :: "nat \<Rightarrow> nat" 

1030 
where 

1031 
"nz 0 = 0" 

1032 
 "nz (Suc n) = nz (nz n)" 

1033 
by pat_completeness auto 

1034 

1035 
text {* 

1036 
If we attempt to prove termination using the identity measure on 

1037 
naturals, this fails: 

1038 
*} 

1039 

1040 
termination 

1041 
apply (relation "measure (\<lambda>n. n)") 

1042 
apply auto 

1043 

1044 
txt {* 

1045 
We get stuck with the subgoal 

1046 

1047 
@{subgoals[display]} 

1048 

1049 
Of course this statement is true, since we know that @{const nz} is 

1050 
the zero function. And in fact we have no problem proving this 

1051 
property by induction. 

1052 
*} 

23805  1053 
(*<*)oops(*>*) 
23003  1054 
lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0" 
39754  1055 
by (induct rule:nz.pinduct) (auto simp: nz.psimps) 
23003  1056 

1057 
text {* 

1058 
We formulate this as a partial correctness lemma with the condition 

1059 
@{term "nz_dom n"}. This allows us to prove it with the @{text 

1060 
pinduct} rule before we have proved termination. With this lemma, 

1061 
the termination proof works as expected: 

1062 
*} 

1063 

1064 
termination 

1065 
by (relation "measure (\<lambda>n. n)") (auto simp: nz_is_zero) 

1066 

1067 
text {* 

1068 
As a general strategy, one should prove the statements needed for 

1069 
termination as a partial property first. Then they can be used to do 

1070 
the termination proof. This also works for less trivial 

23188  1071 
examples. Figure \ref{f91} defines the 91function, a wellknown 
1072 
challenge problem due to John McCarthy, and proves its termination. 

23003  1073 
*} 
1074 

1075 
text_raw {* 

1076 
\begin{figure} 

23188  1077 
\hrule\vspace{6pt} 
23003  1078 
\begin{minipage}{0.8\textwidth} 
1079 
\isabellestyle{it} 

1080 
\isastyle\isamarkuptrue 

1081 
*} 

1082 

23188  1083 
function f91 :: "nat \<Rightarrow> nat" 
23003  1084 
where 
1085 
"f91 n = (if 100 < n then n  10 else f91 (f91 (n + 11)))" 

1086 
by pat_completeness auto 

1087 

1088 
lemma f91_estimate: 

1089 
assumes trm: "f91_dom n" 

1090 
shows "n < f91 n + 11" 

39754  1091 
using trm by induct (auto simp: f91.psimps) 
23003  1092 

1093 
termination 

1094 
proof 

1095 
let ?R = "measure (\<lambda>x. 101  x)" 

1096 
show "wf ?R" .. 

1097 

1098 
fix n :: nat assume "\<not> 100 < n"  "Assumptions for both calls" 

1099 

1100 
thus "(n + 11, n) \<in> ?R" by simp  "Inner call" 

1101 

1102 
assume inner_trm: "f91_dom (n + 11)"  "Outer call" 

1103 
with f91_estimate have "n + 11 < f91 (n + 11) + 11" . 

23805  1104 
with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp 
23003  1105 
qed 
1106 

1107 
text_raw {* 

1108 
\isamarkupfalse\isabellestyle{tt} 

23188  1109 
\end{minipage} 
1110 
\vspace{6pt}\hrule 

23003  1111 
\caption{McCarthy's 91function}\label{f91} 
1112 
\end{figure} 

22065  1113 
*} 
1114 

1115 

23003  1116 
section {* HigherOrder Recursion *} 
22065  1117 

23003  1118 
text {* 
1119 
Higherorder recursion occurs when recursive calls 

29781  1120 
are passed as arguments to higherorder combinators such as @{const 
23003  1121 
map}, @{term filter} etc. 
23805  1122 
As an example, imagine a datatype of nary trees: 
23003  1123 
*} 
1124 

1125 
datatype 'a tree = 

1126 
Leaf 'a 

1127 
 Branch "'a tree list" 

1128 

1129 

25278  1130 
text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the 
1131 
list functions @{const rev} and @{const map}: *} 

25688
6c24a82a98f1
temporarily fixed documentation due to changed size functions
krauss
parents:
25278
diff
changeset

1132 

27026  1133 
fun mirror :: "'a tree \<Rightarrow> 'a tree" 
23003  1134 
where 
25278  1135 
"mirror (Leaf n) = Leaf n" 
1136 
 "mirror (Branch l) = Branch (rev (map mirror l))" 

22065  1137 

1138 
text {* 

27026  1139 
Although the definition is accepted without problems, let us look at the termination proof: 
23003  1140 
*} 
1141 

1142 
termination proof 

1143 
txt {* 

1144 

1145 
As usual, we have to give a wellfounded relation, such that the 

1146 
arguments of the recursive calls get smaller. But what exactly are 

27026  1147 
the arguments of the recursive calls when mirror is given as an 
29781  1148 
argument to @{const map}? Isabelle gives us the 
23003  1149 
subgoals 
1150 

1151 
@{subgoals[display,indent=0]} 

1152 

27026  1153 
So the system seems to know that @{const map} only 
25278  1154 
applies the recursive call @{term "mirror"} to elements 
27026  1155 
of @{term "l"}, which is essential for the termination proof. 
23003  1156 

29781  1157 
This knowledge about @{const map} is encoded in socalled congruence rules, 
23003  1158 
which are special theorems known to the \cmd{function} command. The 
29781  1159 
rule for @{const map} is 
23003  1160 

1161 
@{thm[display] map_cong} 

1162 

1163 
You can read this in the following way: Two applications of @{const 

1164 
map} are equal, if the list arguments are equal and the functions 

1165 
coincide on the elements of the list. This means that for the value 

1166 
@{term "map f l"} we only have to know how @{term f} behaves on 

27026  1167 
the elements of @{term l}. 
23003  1168 

1169 
Usually, one such congruence rule is 

1170 
needed for each higherorder construct that is used when defining 

1171 
new functions. In fact, even basic functions like @{const 

23805  1172 
If} and @{const Let} are handled by this mechanism. The congruence 
23003  1173 
rule for @{const If} states that the @{text then} branch is only 
1174 
relevant if the condition is true, and the @{text else} branch only if it 

1175 
is false: 

1176 

1177 
@{thm[display] if_cong} 

1178 

1179 
Congruence rules can be added to the 

1180 
function package by giving them the @{term fundef_cong} attribute. 

1181 

23805  1182 
The constructs that are predefined in Isabelle, usually 
1183 
come with the respective congruence rules. 

27026  1184 
But if you define your own higherorder functions, you may have to 
1185 
state and prove the required congruence rules yourself, if you want to use your 

23805  1186 
functions in recursive definitions. 
1187 
*} 

27026  1188 
(*<*)oops(*>*) 
23805  1189 

1190 
subsection {* Congruence Rules and Evaluation Order *} 

1191 

1192 
text {* 

1193 
Higher order logic differs from functional programming languages in 

1194 
that it has no builtin notion of evaluation order. A program is 

1195 
just a set of equations, and it is not specified how they must be 

1196 
evaluated. 

1197 

1198 
However for the purpose of function definition, we must talk about 

1199 
evaluation order implicitly, when we reason about termination. 

1200 
Congruence rules express that a certain evaluation order is 

1201 
consistent with the logical definition. 

1202 

1203 
Consider the following function. 

1204 
*} 

1205 

1206 
function f :: "nat \<Rightarrow> bool" 

1207 
where 

1208 
"f n = (n = 0 \<or> f (n  1))" 

1209 
(*<*)by pat_completeness auto(*>*) 

1210 

1211 
text {* 

27026  1212 
For this definition, the termination proof fails. The default configuration 
23805  1213 
specifies no congruence rule for disjunction. We have to add a 
1214 
congruence rule that specifies lefttoright evaluation order: 

1215 

1216 
\vspace{1ex} 

53107
57c7294eac0a
more document antiquotations (for proper theorem names);
Christian Sternagel
parents:
50530
diff
changeset

1217 
\noindent @{thm disj_cong}\hfill(@{thm [source] "disj_cong"}) 
23805  1218 
\vspace{1ex} 
1219 

1220 
Now the definition works without problems. Note how the termination 

1221 
proof depends on the extra condition that we get from the congruence 

1222 
rule. 

1223 

1224 
However, as evaluation is not a hardwired concept, we 

1225 
could just turn everything around by declaring a different 

1226 
congruence rule. Then we can make the reverse definition: 

1227 
*} 

1228 

1229 
lemma disj_cong2[fundef_cong]: 

1230 
"(\<not> Q' \<Longrightarrow> P = P') \<Longrightarrow> (Q = Q') \<Longrightarrow> (P \<or> Q) = (P' \<or> Q')" 

1231 
by blast 

1232 

1233 
fun f' :: "nat \<Rightarrow> bool" 

1234 
where 

1235 
"f' n = (f' (n  1) \<or> n = 0)" 

1236 

1237 
text {* 

1238 
\noindent These examples show that, in general, there is no \qt{best} set of 
