author  Christian Sternagel 
Sat, 17 Aug 2013 14:44:48 +0900  
changeset 53107  57c7294eac0a 
parent 50530  6266e44b3396 
child 54017  2a3c07f49615 
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 

23188  449 
section {* General pattern matching *} 
23805  450 
text{*\label{genpats} *} 
22065  451 

23188  452 
subsection {* Avoiding automatic pattern splitting *} 
22065  453 

454 
text {* 

455 

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

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

458 
they were made disjoint automatically like in the definition of 

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

460 

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

463 
example shows the problem: 

22065  464 

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

22065  468 
*} 
469 

470 
datatype P3 = T  F  X 

471 

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

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

475 
where 

476 
"And T p = p" 

23003  477 
 "And p T = p" 
478 
 "And p F = F" 

479 
 "And F p = F" 

480 
 "And X X = X" 

21212  481 

482 

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

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

22065  488 
splitting them up, producing instances: 
489 
*} 

490 

491 
thm And.simps 

492 

493 
text {* 

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

495 

496 
\vspace*{1em} 

23003  497 
\noindent There are several problems with this: 
22065  498 

499 
\begin{enumerate} 

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

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

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

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

513 

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

515 
back which we put in. 

516 
\end{enumerate} 

517 

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

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

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

522 
= False"} simultaneously.}: 

22065  523 
*} 
524 

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

526 
where 

527 
"And2 T p = p" 

23003  528 
 "And2 p T = p" 
529 
 "And2 p F = F" 

530 
 "And2 F p = F" 

531 
 "And2 X X = X" 

22065  532 

533 
txt {* 

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

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

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

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

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

27026  544 
(\<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  545 
datatypes, we can solve it with the @{text "pat_completeness"} 
546 
method: 

22065  547 
*} 
548 

549 
apply pat_completeness 

550 

551 
txt {* 

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

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

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

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

558 
*} 

559 

560 
by auto 

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

561 
termination by (relation "{}") simp 
21212  562 

563 

22065  564 
subsection {* Nonconstructor patterns *} 
21212  565 

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

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

570 
command handles other kind of patterns, too. 

23188  571 

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

575 
example with $n+k$patterns: 

576 
*} 

577 

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

579 
where 

580 
"fib2 0 = 1" 

581 
 "fib2 1 = 1" 

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

583 

584 
txt {* 

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

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

589 
(2::nat)"}: 

590 

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

591 
@{subgoals[display,indent=0,goals_limit=1]} 
23188  592 

593 
This is an arithmetic triviality, but unfortunately the 

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

23805  595 
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

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

600 
apply atomize_elim 
23805  601 
apply arith 
23188  602 
apply auto 
603 
done 

604 
termination by lexicographic_order 

605 
text {* 

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

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

608 
perfectly valid mathematical definition: 

609 
*} 

610 

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

612 
where 

613 
"ev (2 * n) = True" 

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

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

615 
apply atomize_elim 
23805  616 
by arith+ 
23188  617 
termination by (relation "{}") simp 
618 

619 
text {* 

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

23188  622 
be used with care: 
623 

624 
If we leave the area of constructor 

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

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

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

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

629 
simplification. Your mileage may vary. 

630 
*} 

631 

632 

633 
subsection {* Conditional equations *} 

634 

635 
text {* 

636 
The function package also supports conditional equations, which are 

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

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

639 
patterns are also overlapping in the base case}: 

640 
*} 

641 

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

643 
where 

644 
"gcd x 0 = x" 

645 
 "gcd 0 y = y" 

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

647 
 "\<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

648 
by (atomize_elim, auto, arith) 
23188  649 
termination by lexicographic_order 
650 

651 
text {* 

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

653 
pattern completeness and compatibility look like. 

654 

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

656 
code generator. 

657 
*} 

658 

659 

660 
subsection {* Pattern matching on strings *} 

661 

662 
text {* 

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

666 

667 
\end{isamarkuptext} 

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

669 
\cmd{where}\\% 

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

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

672 
\begin{isamarkuptext} 

673 

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

679 

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

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

682 
*} 

683 

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

685 
where 

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

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

688 
by auto 

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

689 
termination by (relation "{}") simp 
22065  690 

691 

692 
section {* Partiality *} 

693 

694 
text {* 

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

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

700 
function can be defined by wellfounded recursion. 

22065  701 

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

704 
for a zero of a given function f. 

23003  705 
*} 
706 

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

707 
function (*<*)(domintros)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat" 
23003  708 
where 
709 
"findzero f n = (if f n = 0 then n else findzero f (Suc n))" 

710 
by pat_completeness auto 

711 

712 
text {* 

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

717 

718 
subsection {* Domain predicates *} 

719 

720 
text {* 

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

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

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

725 
predicate, we can derive simplification and 

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

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

728 
pinduct}: 

23003  729 
*} 
730 

23805  731 
text {* 
732 
\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

733 
\hfill(@{thm [source] "findzero.psimps"}) 
23805  734 
\vspace{1em} 
23003  735 

23805  736 
\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

737 
\hfill(@{thm [source] "findzero.pinduct"}) 
23003  738 
*} 
739 

740 
text {* 

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

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

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

23188  746 
which one. The function is \emph{underdefined}. 
23003  747 

23805  748 
But it is defined enough to prove something interesting about it. We 
23188  749 
can prove that if @{term "findzero f n"} 
23805  750 
terminates, it indeed returns a zero of @{term f}: 
23003  751 
*} 
752 

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

754 

23805  755 
txt {* \noindent We apply induction as usual, but using the partial induction 
23003  756 
rule: *} 
757 

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

759 

23805  760 
txt {* \noindent This gives the following subgoals: 
23003  761 

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

763 

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

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

23003  769 
*} 
39754  770 
apply (simp add: findzero.psimps) 
23003  771 
done 
772 

773 
text {* 

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

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

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

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

778 
additional domain condition hypothesis. Observe how this condition 

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

780 
*} 

781 

782 
text_raw {* 

783 
\begin{figure} 

23188  784 
\hrule\vspace{6pt} 
23003  785 
\begin{minipage}{0.8\textwidth} 
786 
\isabellestyle{it} 

787 
\isastyle\isamarkuptrue 

788 
*} 

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

790 
proof (induct rule: findzero.pinduct) 

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

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

23003  794 
have "f n \<noteq> 0" 
795 
proof 

796 
assume "f n = 0" 

39754  797 
with dom have "findzero f n = n" by (simp add: findzero.psimps) 
23003  798 
with x_range show False by auto 
799 
qed 

800 

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

802 
thus "f x \<noteq> 0" 

803 
proof 

804 
assume "x = n" 

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

806 
next 

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

811 
qed 

812 
qed 

813 
text_raw {* 

814 
\isamarkupfalse\isabellestyle{tt} 

23188  815 
\end{minipage}\vspace{6pt}\hrule 
23003  816 
\caption{A proof about a partial function}\label{findzero_isar} 
817 
\end{figure} 

818 
*} 

819 

820 
subsection {* Partial termination proofs *} 

821 

822 
text {* 

823 
Now that we have proved some interesting properties about our 

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

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

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

827 

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

829 
findzero_dom}. The function package can prove such domain 

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

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

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

835 

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

839 
\ \ \ldots\\ 

840 

23188  841 
\noindent Now the package has proved an introduction rule for @{text findzero_dom}: 
23003  842 
*} 
843 

844 
thm findzero.domintros 

845 

846 
text {* 

847 
@{thm[display] findzero.domintros} 

848 

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

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

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

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

853 
induction principle. 

854 

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

856 
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

857 
@{thm [source] inc_induct}, which allows to do induction from a fixed number 
23003  858 
\qt{downwards}: 
859 

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

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

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

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

23805  866 
induction is then straightforward, except for the unusual induction 
23003  867 
principle. 
868 

869 
*} 

870 

871 
text_raw {* 

872 
\begin{figure} 

23188  873 
\hrule\vspace{6pt} 
23003  874 
\begin{minipage}{0.8\textwidth} 
875 
\isabellestyle{it} 

876 
\isastyle\isamarkuptrue 

877 
*} 

878 
lemma findzero_termination: 

23188  879 
assumes "x \<ge> n" and "f x = 0" 
23003  880 
shows "findzero_dom (f, n)" 
881 
proof  

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

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

884 

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

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

887 
by (rule findzero.domintros) simp 

888 

23188  889 
from `x \<ge> n` show ?thesis 
23003  890 
proof (induct rule:inc_induct) 
23188  891 
show "findzero_dom (f, x)" by (rule base) 
23003  892 
next 
893 
fix i assume "findzero_dom (f, Suc i)" 

23188  894 
thus "findzero_dom (f, i)" by (rule step) 
23003  895 
qed 
896 
qed 

897 
text_raw {* 

898 
\isamarkupfalse\isabellestyle{tt} 

23188  899 
\end{minipage}\vspace{6pt}\hrule 
23003  900 
\caption{Termination proof for @{text findzero}}\label{findzero_term} 
901 
\end{figure} 

902 
*} 

903 

904 
text {* 

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

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

907 
can also have a short proof: 

908 
*} 

909 

910 
lemma findzero_termination_short: 

911 
assumes zero: "x >= n" 

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

913 
shows "findzero_dom (f, n)" 

23805  914 
using zero 
915 
by (induct rule:inc_induct) (auto intro: findzero.domintros) 

23003  916 

917 
text {* 

23188  918 
\noindent It is simple to combine the partial correctness result with the 
23003  919 
termination lemma: 
920 
*} 

921 

922 
lemma findzero_total_correctness: 

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

924 
by (blast intro: findzero_zero findzero_termination) 

925 

926 
subsection {* Definition of the domain predicate *} 

927 

928 
text {* 

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

23805  930 
predicate looks like. Actually, @{text findzero_dom} is just an 
23003  931 
abbreviation: 
932 

933 
@{abbrev[display] findzero_dom} 

934 

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

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

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

942 
@{thm[display] findzero_rel.intros} 

943 

23188  944 
The predicate @{const findzero_rel} 
23003  945 
describes the \emph{recursion relation} of the function 
946 
definition. The recursion relation is a binary relation on 

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

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

949 
recursive call. 

950 

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

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

23805  957 
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

958 
lemmas which are occasionally useful are @{thm [source] accpI}, @{thm [source] 
23805  959 
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

960 
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

961 
[source] "findzero_rel.cases"}. 
23003  962 
*} 
963 

964 
section {* Nested recursion *} 

965 

966 
text {* 

967 
Recursive calls which are nested in one another frequently cause 

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

969 
correctness property of the function itself. 

970 

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

972 
*} 

973 

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

975 
where 

976 
"nz 0 = 0" 

977 
 "nz (Suc n) = nz (nz n)" 

978 
by pat_completeness auto 

979 

980 
text {* 

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

982 
naturals, this fails: 

983 
*} 

984 

985 
termination 

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

987 
apply auto 

988 

989 
txt {* 

990 
We get stuck with the subgoal 

991 

992 
@{subgoals[display]} 

993 

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

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

996 
property by induction. 

997 
*} 

23805  998 
(*<*)oops(*>*) 
23003  999 
lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0" 
39754  1000 
by (induct rule:nz.pinduct) (auto simp: nz.psimps) 
23003  1001 

1002 
text {* 

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

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

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

1006 
the termination proof works as expected: 

1007 
*} 

1008 

1009 
termination 

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

1011 

1012 
text {* 

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

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

1015 
the termination proof. This also works for less trivial 

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

23003  1018 
*} 
1019 

1020 
text_raw {* 

1021 
\begin{figure} 

23188  1022 
\hrule\vspace{6pt} 
23003  1023 
\begin{minipage}{0.8\textwidth} 
1024 
\isabellestyle{it} 

1025 
\isastyle\isamarkuptrue 

1026 
*} 

1027 

23188  1028 
function f91 :: "nat \<Rightarrow> nat" 
23003  1029 
where 
1030 
"f91 n = (if 100 < n then n  10 else f91 (f91 (n + 11)))" 

1031 
by pat_completeness auto 

1032 

1033 
lemma f91_estimate: 

1034 
assumes trm: "f91_dom n" 

1035 
shows "n < f91 n + 11" 

39754  1036 
using trm by induct (auto simp: f91.psimps) 
23003  1037 

1038 
termination 

1039 
proof 

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

1041 
show "wf ?R" .. 

1042 

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

1044 

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

1046 

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

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

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

1052 
text_raw {* 

1053 
\isamarkupfalse\isabellestyle{tt} 

23188  1054 
\end{minipage} 
1055 
\vspace{6pt}\hrule 

23003  1056 
\caption{McCarthy's 91function}\label{f91} 
1057 
\end{figure} 

22065  1058 
*} 
1059 

1060 

23003  1061 
section {* HigherOrder Recursion *} 
22065  1062 

23003  1063 
text {* 
1064 
Higherorder recursion occurs when recursive calls 

29781  1065 
are passed as arguments to higherorder combinators such as @{const 
23003  1066 
map}, @{term filter} etc. 
23805  1067 
As an example, imagine a datatype of nary trees: 
23003  1068 
*} 
1069 

1070 
datatype 'a tree = 

1071 
Leaf 'a 

1072 
 Branch "'a tree list" 

1073 

1074 

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

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

1077 

27026  1078 
fun mirror :: "'a tree \<Rightarrow> 'a tree" 
23003  1079 
where 
25278  1080 
"mirror (Leaf n) = Leaf n" 
1081 
 "mirror (Branch l) = Branch (rev (map mirror l))" 

22065  1082 

1083 
text {* 

27026  1084 
Although the definition is accepted without problems, let us look at the termination proof: 
23003  1085 
*} 
1086 

1087 
termination proof 

1088 
txt {* 

1089 

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

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

27026  1092 
the arguments of the recursive calls when mirror is given as an 
29781  1093 
argument to @{const map}? Isabelle gives us the 
23003  1094 
subgoals 
1095 

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

1097 

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

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

1106 
@{thm[display] map_cong} 

1107 

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

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

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

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

27026  1112 
the elements of @{term l}. 
23003  1113 

1114 
Usually, one such congruence rule is 

1115 
needed for each higherorder construct that is used when defining 

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

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

1120 
is false: 

1121 

1122 
@{thm[display] if_cong} 

1123 

1124 
Congruence rules can be added to the 

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

1126 

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

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

23805  1131 
functions in recursive definitions. 
1132 
*} 

27026  1133 
(*<*)oops(*>*) 
23805  1134 

1135 
subsection {* Congruence Rules and Evaluation Order *} 

1136 

1137 
text {* 

1138 
Higher order logic differs from functional programming languages in 

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

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

1141 
evaluated. 

1142 

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

1144 
evaluation order implicitly, when we reason about termination. 

1145 
Congruence rules express that a certain evaluation order is 

1146 
consistent with the logical definition. 

1147 

1148 
Consider the following function. 

1149 
*} 

1150 

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

1152 
where 

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

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

1155 

1156 
text {* 

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

1160 

1161 
\vspace{1ex} 

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

1162 
\noindent @{thm disj_cong}\hfill(@{thm [source] "disj_cong"}) 
23805  1163 
\vspace{1ex} 
1164 

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

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

1167 
rule. 

1168 

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

1170 
could just turn everything around by declaring a different 

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

1172 
*} 

1173 

1174 
lemma disj_cong2[fundef_cong]: 

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

1176 
by blast 

1177 

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

1179 
where 

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

1181 

1182 
text {* 

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

1184 
congruence rules. 

1185 

1186 
However, such tweaking should rarely be necessary in 

1187 
practice, as most of the time, the default set of congruence rules 

1188 
works well. 

1189 
*} 

1190 

21212  1191 
end 