summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/IsarAdvanced/Functions/Thy/Functions.thy

author | krauss |

Tue Apr 08 18:30:40 2008 +0200 (2008-04-08) | |

changeset 26580 | c3e597a476fd |

parent 25688 | 6c24a82a98f1 |

child 26749 | 397a1aeede7d |

permissions | -rw-r--r-- |

Generic conversion and tactic "atomize_elim" to convert elimination rules

to the object logic

to the object logic

1 (* Title: Doc/IsarAdvanced/Functions/Thy/Fundefs.thy

2 ID: $Id$

3 Author: Alexander Krauss, TU Muenchen

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

6 *)

8 theory Functions

9 imports Main

10 begin

12 section {* Function Definitions for Dummies *}

14 text {*

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

16 *}

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

19 where

20 "fib 0 = 1"

21 | "fib (Suc 0) = 1"

22 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"

24 text {*

25 The syntax is rather self-explanatory: We introduce a function by

26 giving its name, its type,

27 and a set of defining recursive equations.

28 If we leave out the type, the most general type will be

29 inferred, which can sometimes lead to surprises: Since both @{term

30 "1::nat"} and @{text "+"} are overloaded, we would end up

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

32 *}

34 text {*

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

36 every recursive call.

37 Since HOL is a logic of total functions, termination is a

38 fundamental requirement to prevent inconsistencies\footnote{From the

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

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

41 Isabelle tries to prove termination automatically when a definition

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

43 fails and see what to do then.

44 *}

46 subsection {* Pattern matching *}

48 text {* \label{patmatch}

49 Like in functional programming, we can use pattern matching to

50 define functions. At the moment we will only consider \emph{constructor

51 patterns}, which only consist of datatype constructors and

52 variables. Furthermore, patterns must be linear, i.e.\ all variables

53 on the left hand side of an equation must be distinct. In

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

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

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

58 two elements of a list:

59 *}

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

62 where

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

64 | "sep a xs = xs"

66 text {*

67 Overlapping patterns are interpreted as \qt{increments} to what is

68 already there: The second equation is only meant for the cases where

69 the first one does not match. Consequently, Isabelle replaces it

70 internally by the remaining cases, making the patterns disjoint:

71 *}

73 thm sep.simps

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

77 text {*

78 \noindent The equations from function definitions are automatically used in

79 simplification:

80 *}

82 lemma "sep 0 [1, 2, 3] = [1, 0, 2, 0, 3]"

83 by simp

85 subsection {* Induction *}

87 text {*

89 Isabelle provides customized induction rules for recursive

90 functions. These rules follow the recursive structure of the

91 definition. Here is the rule @{text sep.induct} arising from the

92 above definition of @{const sep}:

94 @{thm [display] sep.induct}

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

97 base cases for the zero- and the one-element list. Here is a simple

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

99 *}

101 lemma "map f (sep x ys) = sep (f x) (map f ys)"

102 apply (induct x ys rule: sep.induct)

104 txt {*

105 We get three cases, like in the definition.

107 @{subgoals [display]}

108 *}

110 apply auto

111 done

112 text {*

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

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

116 the remaining 20\%.

117 *}

120 section {* fun vs.\ function *}

122 text {*

123 The \cmd{fun} command provides a

124 convenient shorthand notation for simple function definitions. In

125 this mode, Isabelle tries to solve all the necessary proof obligations

126 automatically. If a proof fails, the definition is

127 rejected. This can either mean that the definition is indeed faulty,

128 or that the default proof procedures are just not smart enough (or

129 rather: not designed) to handle the definition.

131 By expanding the abbreviation to the more verbose \cmd{function} command, these proof obligations become visible and can be analyzed or

132 solved manually. The expansion from \cmd{fun} to \cmd{function} is as follows:

134 \end{isamarkuptext}

137 \[\left[\;\begin{minipage}{0.25\textwidth}\vspace{6pt}

138 \cmd{fun} @{text "f :: \<tau>"}\\%

139 \cmd{where}\\%

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

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

142 \end{minipage}\right]

143 \quad\equiv\quad

144 \left[\;\begin{minipage}{0.45\textwidth}\vspace{6pt}

145 \cmd{function} @{text "("}\cmd{sequential}@{text ") f :: \<tau>"}\\%

146 \cmd{where}\\%

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

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

149 \cmd{by} @{text "pat_completeness auto"}\\%

150 \cmd{termination by} @{text "lexicographic_order"}\vspace{6pt}

151 \end{minipage}

152 \right]\]

154 \begin{isamarkuptext}

155 \vspace*{1em}

156 \noindent Some details have now become explicit:

158 \begin{enumerate}

159 \item The \cmd{sequential} option enables the preprocessing of

160 pattern overlaps which we already saw. Without this option, the equations

161 must already be disjoint and complete. The automatic completion only

162 works with constructor patterns.

164 \item A function definition produces a proof obligation which

165 expresses completeness and compatibility of patterns (we talk about

166 this later). The combination of the methods @{text "pat_completeness"} and

167 @{text "auto"} is used to solve this proof obligation.

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

170 \cmd{termination} command. This will be explained in \S\ref{termination}.

171 \end{enumerate}

172 Whenever a \cmd{fun} command fails, it is usually a good idea to

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

174 what is actually going on.

175 *}

178 section {* Termination *}

180 text {*\label{termination}

181 The method @{text "lexicographic_order"} is the default method for

182 termination proofs. It can prove termination of a

183 certain class of functions by searching for a suitable lexicographic

184 combination of size measures. Of course, not all functions have such

185 a simple termination argument. For them, we can specify the termination

186 relation manually.

187 *}

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

190 text{*

191 Consider the following function, which sums up natural numbers up to

192 @{text "N"}, using a counter @{text "i"}:

193 *}

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

196 where

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

198 by pat_completeness auto

200 text {*

201 \noindent The @{text "lexicographic_order"} method fails on this example, because none of the

202 arguments decreases in the recursive call, with respect to the standard size ordering.

203 To prove termination manually, we must provide a custom wellfounded relation.

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

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

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

208 is greater than @{text "N"}. Phrased differently, the expression

209 @{text "N + 1 - i"} always decreases.

211 We can use this expression as a measure function suitable to prove termination.

212 *}

214 termination

215 apply (relation "measure (\<lambda>(i,N). N + 1 - i)")

217 txt {*

218 The \cmd{termination} command sets up the termination goal for the

219 specified function @{text "sum"}. If the function name is omitted, it

220 implicitly refers to the last function definition.

222 The @{text relation} method takes a relation of

223 type @{typ "('a \<times> 'a) set"}, where @{typ "'a"} is the argument type of

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

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

226 example.

228 The predefined function @{term_type "measure"} constructs a

229 wellfounded relation from a mapping into the natural numbers (a

230 \emph{measure function}).

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

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

234 of recursive calls indeed decrease with respect to the

235 relation:

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

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

240 *}

242 apply auto

243 done

245 text {*

246 Let us complicate the function a little, by adding some more

247 recursive calls:

248 *}

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

251 where

252 "foo i N = (if i > N

253 then (if N = 0 then 0 else foo 0 (N - 1))

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

255 by pat_completeness auto

257 text {*

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

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

260 This corresponds to a nested

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

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

263 the value of @{text "N"} and the above difference. The @{const

264 "measures"} combinator generalizes @{text "measure"} by taking a

265 list of measure functions.

266 *}

268 termination

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

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

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

274 where

275 "fails a [] = a"

276 | "fails a (x#xs) = fails (x + a) (x # xs)"

277 *)

279 text {*

280 To see how the automatic termination proofs work, let's look at an

281 example where it fails\footnote{For a detailed discussion of the

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

284 \end{isamarkuptext}

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

286 \cmd{where}\\%

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

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

289 \begin{isamarkuptext}

291 \noindent Isabelle responds with the following error:

293 \begin{isabelle}

294 *** Unfinished subgoals:\newline

295 *** (a, 1, <):\newline

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

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

298 *** \ 1.~False\newline

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

300 *** \ 1.~False\newline

301 *** Calls:\newline

302 *** a) @{text "(a, x # xs) -->> (x + a, x # xs)"}\newline

303 *** Measures:\newline

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

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

306 *** Result matrix:\newline

307 *** \ \ \ \ 1\ \ 2 \newline

308 *** a: ? <= \newline

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

310 *** At command "fun".\newline

311 \end{isabelle}

312 *}

315 text {*

318 The the key to this error message is the matrix at the bottom. The rows

319 of that matrix correspond to the different recursive calls (In our

320 case, there is just one). The columns are the function's arguments

321 (expressed through different measure functions, which map the

322 argument tuple to a natural number).

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

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

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

327 which is expressed by @{text "?"}. In general, there are the values

328 @{text "<"}, @{text "<="} and @{text "?"}.

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

331 printed. Looking at these will often point to a missing lemma.

333 % As a more real example, here is quicksort:

334 *}

335 (*

336 function qs :: "nat list \<Rightarrow> nat list"

337 where

338 "qs [] = []"

339 | "qs (x#xs) = qs [y\<in>xs. y < x] @ x # qs [y\<in>xs. y \<ge> x]"

340 by pat_completeness auto

342 termination apply lexicographic_order

344 text {* If we try @{text "lexicographic_order"} method, we get the

345 following error *}

346 termination by (lexicographic_order simp:l2)

348 lemma l: "x \<le> y \<Longrightarrow> x < Suc y" by arith

350 function

352 *)

354 section {* Mutual Recursion *}

356 text {*

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

358 in one step. Here are @{text "even"} and @{text "odd"}:

359 *}

361 function even :: "nat \<Rightarrow> bool"

362 and odd :: "nat \<Rightarrow> bool"

363 where

364 "even 0 = True"

365 | "odd 0 = False"

366 | "even (Suc n) = odd n"

367 | "odd (Suc n) = even n"

368 by pat_completeness auto

370 text {*

371 To eliminate the mutual dependencies, Isabelle internally

372 creates a single function operating on the sum

373 type @{typ "nat + nat"}. Then, @{const even} and @{const odd} are

374 defined as projections. Consequently, termination has to be proved

375 simultaneously for both functions, by specifying a measure on the

376 sum type:

377 *}

379 termination

380 by (relation "measure (\<lambda>x. case x of Inl n \<Rightarrow> n | Inr n \<Rightarrow> n)") auto

382 text {*

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

384 supports mutual recursive termination proofs to a certain extent.

385 *}

387 subsection {* Induction for mutual recursion *}

389 text {*

391 When functions are mutually recursive, proving properties about them

392 generally requires simultaneous induction. The induction rule @{text "even_odd.induct"}

393 generated from the above definition reflects this.

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

396 *}

398 lemma even_odd_mod2:

399 "even n = (n mod 2 = 0)"

400 "odd n = (n mod 2 = 1)"

402 txt {*

403 We apply simultaneous induction, specifying the induction variable

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

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

408 txt {*

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

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

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

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

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

414 *}

416 apply simp_all

418 txt {*

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

421 \noindent These can be handled by Isabelle's arithmetic decision procedures.

423 *}

425 apply arith

426 apply arith

427 done

429 text {*

430 In proofs like this, the simultaneous induction is really essential:

431 Even if we are just interested in one of the results, the other

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

433 out the statement about @{const odd} (by substituting it with @{term

434 "True"}), the same proof fails:

435 *}

437 lemma failed_attempt:

438 "even n = (n mod 2 = 0)"

439 "True"

440 apply (induct n rule: even_odd.induct)

442 txt {*

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

444 useful induction hypothesis available:

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

447 *}

449 oops

451 section {* General pattern matching *}

452 text{*\label{genpats} *}

454 subsection {* Avoiding automatic pattern splitting *}

456 text {*

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

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

460 they were made disjoint automatically like in the definition of

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

463 This automatic splitting can significantly increase the number of

464 equations involved, and this is not always desirable. The following

465 example shows the problem:

467 Suppose we are modeling incomplete knowledge about the world by a

468 three-valued datatype, which has values @{term "T"}, @{term "F"}

469 and @{term "X"} for true, false and uncertain propositions, respectively.

470 *}

472 datatype P3 = T | F | X

474 text {* \noindent Then the conjunction of such values can be defined as follows: *}

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

477 where

478 "And T p = p"

479 | "And p T = p"

480 | "And p F = F"

481 | "And F p = F"

482 | "And X X = X"

485 text {*

486 This definition is useful, because the equations can directly be used

487 as simplification rules rules. But the patterns overlap: For example,

488 the expression @{term "And T T"} is matched by both the first and

489 the second equation. By default, Isabelle makes the patterns disjoint by

490 splitting them up, producing instances:

491 *}

493 thm And.simps

495 text {*

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

498 \vspace*{1em}

499 \noindent There are several problems with this:

501 \begin{enumerate}

502 \item If the datatype has many constructors, there can be an

503 explosion of equations. For @{const "And"}, we get seven instead of

504 five equations, which can be tolerated, but this is just a small

505 example.

507 \item Since splitting makes the equations \qt{less general}, they

508 do not always match in rewriting. While the term @{term "And x F"}

509 can be simplified to @{term "F"} with the original equations, a

510 (manual) case split on @{term "x"} is now necessary.

512 \item The splitting also concerns the induction rule @{text

513 "And.induct"}. Instead of five premises it now has seven, which

514 means that our induction proofs will have more cases.

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

517 back which we put in.

518 \end{enumerate}

520 If we do not want the automatic splitting, we can switch it off by

521 leaving out the \cmd{sequential} option. However, we will have to

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

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

524 = False"} simultaneously.}:

525 *}

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

528 where

529 "And2 T p = p"

530 | "And2 p T = p"

531 | "And2 p F = F"

532 | "And2 F p = F"

533 | "And2 X X = X"

535 txt {*

536 \noindent Now let's look at the proof obligations generated by a

537 function definition. In this case, they are:

539 @{subgoals[display,indent=0]}\vspace{-1.2em}\hspace{3cm}\vdots\vspace{1.2em}

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

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

543 the function's input type must match at least one of the patterns\footnote{Completeness could

544 be equivalently stated as a disjunction of existential statements:

545 @{term "(\<exists>p. x = (T, p)) \<or> (\<exists>p. x = (p, T)) \<or> (\<exists>p. x = (p, F)) \<or>

546 (\<exists>p. x = (F, p)) \<or> (x = (X, X))"}.}. If the patterns just involve

547 datatypes, we can solve it with the @{text "pat_completeness"}

548 method:

549 *}

551 apply pat_completeness

553 txt {*

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

555 allow that an input value matches multiple patterns, but in this

556 case, the result (i.e.~the right hand sides of the equations) must

557 also be equal. For each pair of two patterns, there is one such

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

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

560 *}

562 by auto

565 subsection {* Non-constructor patterns *}

567 text {*

568 Most of Isabelle's basic types take the form of inductive datatypes,

569 and usually pattern matching works on the constructors of such types.

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

571 command handles other kind of patterns, too.

573 One well-known instance of non-constructor patterns are

574 so-called \emph{$n+k$-patterns}, which are a little controversial in

575 the functional programming world. Here is the initial fibonacci

576 example with $n+k$-patterns:

577 *}

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

580 where

581 "fib2 0 = 1"

582 | "fib2 1 = 1"

583 | "fib2 (n + 2) = fib2 n + fib2 (Suc n)"

585 (*<*)ML "goals_limit := 1"(*>*)

586 txt {*

587 This kind of matching is again justified by the proof of pattern

588 completeness and compatibility.

589 The proof obligation for pattern completeness states that every natural number is

590 either @{term "0::nat"}, @{term "1::nat"} or @{term "n +

591 (2::nat)"}:

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

595 This is an arithmetic triviality, but unfortunately the

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

597 elimination rule. However, we can use the method @{text

598 "atomize_elim"} to do an ad-hoc conversion to a disjunction of

599 existentials, which can then be soved by the arithmetic decision procedure.

600 Pattern compatibility and termination are automatic as usual.

601 *}

602 (*<*)ML "goals_limit := 10"(*>*)

603 apply atomize_elim

604 apply arith

605 apply auto

606 done

607 termination by lexicographic_order

609 text {*

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

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

612 perfectly valid mathematical definition:

613 *}

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

616 where

617 "ev (2 * n) = True"

618 | "ev (2 * n + 1) = False"

619 apply atomize_elim

620 by arith+

621 termination by (relation "{}") simp

623 text {*

624 This general notion of pattern matching gives you the full freedom

625 of mathematical specifications. However, as always, freedom should

626 be used with care:

628 If we leave the area of constructor

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

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

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

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

633 simplification. Your mileage may vary.

634 *}

637 subsection {* Conditional equations *}

639 text {*

640 The function package also supports conditional equations, which are

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

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

643 patterns are also overlapping in the base case}:

644 *}

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

647 where

648 "gcd x 0 = x"

649 | "gcd 0 y = y"

650 | "x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (Suc x) (y - x)"

651 | "\<not> x < y \<Longrightarrow> gcd (Suc x) (Suc y) = gcd (x - y) (Suc y)"

652 by (atomize_elim, auto, arith)

653 termination by lexicographic_order

655 text {*

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

657 pattern completeness and compatibility look like.

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

660 code generator.

661 *}

664 subsection {* Pattern matching on strings *}

666 text {*

667 As strings (as lists of characters) are normal datatypes, pattern

668 matching on them is possible, but somewhat problematic. Consider the

669 following definition:

671 \end{isamarkuptext}

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

673 \cmd{where}\\%

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

675 @{text "| \"check s = False\""}

676 \begin{isamarkuptext}

678 \noindent An invocation of the above \cmd{fun} command does not

679 terminate. What is the problem? Strings are lists of characters, and

680 characters are a datatype with a lot of constructors. Splitting the

681 catch-all pattern thus leads to an explosion of cases, which cannot

682 be handled by Isabelle.

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

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

686 *}

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

689 where

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

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

692 by auto

695 section {* Partiality *}

697 text {*

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

699 @{term "x"} always has the value @{term "f x"}, and there is no notion

700 of undefinedness.

701 This is why we have to do termination

702 proofs when defining functions: The proof justifies that the

703 function can be defined by wellfounded recursion.

705 However, the \cmd{function} package does support partiality to a

706 certain extent. Let's look at the following function which looks

707 for a zero of a given function f.

708 *}

710 function (*<*)(domintros, tailrec)(*>*)findzero :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat"

711 where

712 "findzero f n = (if f n = 0 then n else findzero f (Suc n))"

713 by pat_completeness auto

714 (*<*)declare findzero.simps[simp del](*>*)

716 text {*

717 \noindent Clearly, any attempt of a termination proof must fail. And without

718 that, we do not get the usual rules @{text "findzero.simp"} and

719 @{text "findzero.induct"}. So what was the definition good for at all?

720 *}

722 subsection {* Domain predicates *}

724 text {*

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

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

727 terminates: the \emph{domain} of the function. If we treat a

728 partial function just as a total function with an additional domain

729 predicate, we can derive simplification and

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

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

732 pinduct}:

733 *}

735 text {*

736 \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.psimps}\end{minipage}

737 \hfill(@{text "findzero.psimps"})

738 \vspace{1em}

740 \noindent\begin{minipage}{0.79\textwidth}@{thm[display,margin=85] findzero.pinduct}\end{minipage}

741 \hfill(@{text "findzero.pinduct"})

742 *}

744 text {*

745 Remember that all we

746 are doing here is use some tricks to make a total function appear

747 as if it was partial. We can still write the term @{term "findzero

748 (\<lambda>x. 1) 0"} and like any other term of type @{typ nat} it is equal

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

750 which one. The function is \emph{underdefined}.

752 But it is defined enough to prove something interesting about it. We

753 can prove that if @{term "findzero f n"}

754 terminates, it indeed returns a zero of @{term f}:

755 *}

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

759 txt {* \noindent We apply induction as usual, but using the partial induction

760 rule: *}

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

764 txt {* \noindent This gives the following subgoals:

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

768 \noindent The hypothesis in our lemma was used to satisfy the first premise in

769 the induction rule. However, we also get @{term

770 "findzero_dom (f, n)"} as a local assumption in the induction step. This

771 allows to unfold @{term "findzero f n"} using the @{text psimps}

772 rule, and the rest is trivial. Since the @{text psimps} rules carry the

773 @{text "[simp]"} attribute by default, we just need a single step:

774 *}

775 apply simp

776 done

778 text {*

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

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

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

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

783 additional domain condition hypothesis. Observe how this condition

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

785 *}

787 text_raw {*

788 \begin{figure}

789 \hrule\vspace{6pt}

790 \begin{minipage}{0.8\textwidth}

791 \isabellestyle{it}

792 \isastyle\isamarkuptrue

793 *}

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

795 proof (induct rule: findzero.pinduct)

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

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

798 and x_range: "x \<in> {n ..< findzero f n}"

799 have "f n \<noteq> 0"

800 proof

801 assume "f n = 0"

802 with dom have "findzero f n = n" by simp

803 with x_range show False by auto

804 qed

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

807 thus "f x \<noteq> 0"

808 proof

809 assume "x = n"

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

811 next

812 assume "x \<in> {Suc n ..< findzero f n}"

813 with dom and `f n \<noteq> 0` have "x \<in> {Suc n ..< findzero f (Suc n)}" by simp

814 with IH and `f n \<noteq> 0`

815 show ?thesis by simp

816 qed

817 qed

818 text_raw {*

819 \isamarkupfalse\isabellestyle{tt}

820 \end{minipage}\vspace{6pt}\hrule

821 \caption{A proof about a partial function}\label{findzero_isar}

822 \end{figure}

823 *}

825 subsection {* Partial termination proofs *}

827 text {*

828 Now that we have proved some interesting properties about our

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

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

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

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

834 findzero_dom}. The function package can prove such domain

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

836 often (they are almost never needed if the function is total), this

837 functionality is disabled by default for efficiency reasons. So we have to go

838 back and ask for them explicitly by passing the @{text

839 "(domintros)"} option to the function package:

841 \vspace{1ex}

842 \noindent\cmd{function} @{text "(domintros) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%

843 \cmd{where}\isanewline%

844 \ \ \ldots\\

846 \noindent Now the package has proved an introduction rule for @{text findzero_dom}:

847 *}

849 thm findzero.domintros

851 text {*

852 @{thm[display] findzero.domintros}

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

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

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

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

858 induction principle.

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

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

862 @{text inc_induct}, which allows to do induction from a fixed number

863 \qt{downwards}:

865 \begin{center}@{thm inc_induct}\hfill(@{text "inc_induct"})\end{center}

867 Figure \ref{findzero_term} gives a detailed Isar proof of the fact

868 that @{text findzero} terminates if there is a zero which is greater

869 or equal to @{term n}. First we derive two useful rules which will

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

871 induction is then straightforward, except for the unusual induction

872 principle.

874 *}

876 text_raw {*

877 \begin{figure}

878 \hrule\vspace{6pt}

879 \begin{minipage}{0.8\textwidth}

880 \isabellestyle{it}

881 \isastyle\isamarkuptrue

882 *}

883 lemma findzero_termination:

884 assumes "x \<ge> n" and "f x = 0"

885 shows "findzero_dom (f, n)"

886 proof -

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

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

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

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

892 by (rule findzero.domintros) simp

894 from `x \<ge> n` show ?thesis

895 proof (induct rule:inc_induct)

896 show "findzero_dom (f, x)" by (rule base)

897 next

898 fix i assume "findzero_dom (f, Suc i)"

899 thus "findzero_dom (f, i)" by (rule step)

900 qed

901 qed

902 text_raw {*

903 \isamarkupfalse\isabellestyle{tt}

904 \end{minipage}\vspace{6pt}\hrule

905 \caption{Termination proof for @{text findzero}}\label{findzero_term}

906 \end{figure}

907 *}

909 text {*

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

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

912 can also have a short proof:

913 *}

915 lemma findzero_termination_short:

916 assumes zero: "x >= n"

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

918 shows "findzero_dom (f, n)"

919 using zero

920 by (induct rule:inc_induct) (auto intro: findzero.domintros)

922 text {*

923 \noindent It is simple to combine the partial correctness result with the

924 termination lemma:

925 *}

927 lemma findzero_total_correctness:

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

929 by (blast intro: findzero_zero findzero_termination)

931 subsection {* Definition of the domain predicate *}

933 text {*

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

935 predicate looks like. Actually, @{text findzero_dom} is just an

936 abbreviation:

938 @{abbrev[display] findzero_dom}

940 The domain predicate is the \emph{accessible part} of a relation @{const

941 findzero_rel}, which was also created internally by the function

942 package. @{const findzero_rel} is just a normal

943 inductive predicate, so we can inspect its definition by

944 looking at the introduction rules @{text findzero_rel.intros}.

945 In our case there is just a single rule:

947 @{thm[display] findzero_rel.intros}

949 The predicate @{const findzero_rel}

950 describes the \emph{recursion relation} of the function

951 definition. The recursion relation is a binary relation on

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

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

954 recursive call.

956 The predicate @{term "accp findzero_rel"} is the accessible part of

957 that relation. An argument belongs to the accessible part, if it can

958 be reached in a finite number of steps (cf.~its definition in @{text

959 "Accessible_Part.thy"}).

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

962 lemmas for @{const accp} and @{const findzero_rel} directly. Some

963 lemmas which are occasionally useful are @{text accpI}, @{text

964 accp_downward}, and of course the introduction and elimination rules

965 for the recursion relation @{text "findzero.intros"} and @{text "findzero.cases"}.

966 *}

968 (*lemma findzero_nicer_domintros:

969 "f x = 0 \<Longrightarrow> findzero_dom (f, x)"

970 "findzero_dom (f, Suc x) \<Longrightarrow> findzero_dom (f, x)"

971 by (rule accpI, erule findzero_rel.cases, auto)+

972 *)

974 subsection {* A Useful Special Case: Tail recursion *}

976 text {*

977 The domain predicate is our trick that allows us to model partiality

978 in a world of total functions. The downside of this is that we have

979 to carry it around all the time. The termination proof above allowed

980 us to replace the abstract @{term "findzero_dom (f, n)"} by the more

981 concrete @{term "(x \<ge> n \<and> f x = (0::nat))"}, but the condition is still

982 there and can only be discharged for special cases.

983 In particular, the domain predicate guards the unfolding of our

984 function, since it is there as a condition in the @{text psimp}

985 rules.

987 Now there is an important special case: We can actually get rid

988 of the condition in the simplification rules, \emph{if the function

989 is tail-recursive}. The reason is that for all tail-recursive

990 equations there is a total function satisfying them, even if they

991 are non-terminating.

993 % A function is tail recursive, if each call to the function is either

994 % equal

995 %

996 % So the outer form of the

997 %

998 %if it can be written in the following

999 % form:

1000 % {term[display] "f x = (if COND x then BASE x else f (LOOP x))"}

1003 The function package internally does the right construction and can

1004 derive the unconditional simp rules, if we ask it to do so. Luckily,

1005 our @{const "findzero"} function is tail-recursive, so we can just go

1006 back and add another option to the \cmd{function} command:

1008 \vspace{1ex}

1009 \noindent\cmd{function} @{text "(domintros, tailrec) findzero :: \"(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat\""}\\%

1010 \cmd{where}\isanewline%

1011 \ \ \ldots\\%

1014 \noindent Now, we actually get unconditional simplification rules, even

1015 though the function is partial:

1016 *}

1018 thm findzero.simps

1020 text {*

1021 @{thm[display] findzero.simps}

1023 \noindent Of course these would make the simplifier loop, so we better remove

1024 them from the simpset:

1025 *}

1027 declare findzero.simps[simp del]

1029 text {*

1030 Getting rid of the domain conditions in the simplification rules is

1031 not only useful because it simplifies proofs. It is also required in

1032 order to use Isabelle's code generator to generate ML code

1033 from a function definition.

1034 Since the code generator only works with equations, it cannot be

1035 used with @{text "psimp"} rules. Thus, in order to generate code for

1036 partial functions, they must be defined as a tail recursion.

1037 Luckily, many functions have a relatively natural tail recursive

1038 definition.

1039 *}

1041 section {* Nested recursion *}

1043 text {*

1044 Recursive calls which are nested in one another frequently cause

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

1046 correctness property of the function itself.

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

1049 *}

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

1052 where

1053 "nz 0 = 0"

1054 | "nz (Suc n) = nz (nz n)"

1055 by pat_completeness auto

1057 text {*

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

1059 naturals, this fails:

1060 *}

1062 termination

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

1064 apply auto

1066 txt {*

1067 We get stuck with the subgoal

1069 @{subgoals[display]}

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

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

1073 property by induction.

1074 *}

1075 (*<*)oops(*>*)

1076 lemma nz_is_zero: "nz_dom n \<Longrightarrow> nz n = 0"

1077 by (induct rule:nz.pinduct) auto

1079 text {*

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

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

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

1083 the termination proof works as expected:

1084 *}

1086 termination

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

1089 text {*

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

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

1092 the termination proof. This also works for less trivial

1093 examples. Figure \ref{f91} defines the 91-function, a well-known

1094 challenge problem due to John McCarthy, and proves its termination.

1095 *}

1097 text_raw {*

1098 \begin{figure}

1099 \hrule\vspace{6pt}

1100 \begin{minipage}{0.8\textwidth}

1101 \isabellestyle{it}

1102 \isastyle\isamarkuptrue

1103 *}

1105 function f91 :: "nat \<Rightarrow> nat"

1106 where

1107 "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"

1108 by pat_completeness auto

1110 lemma f91_estimate:

1111 assumes trm: "f91_dom n"

1112 shows "n < f91 n + 11"

1113 using trm by induct auto

1115 termination

1116 proof

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

1118 show "wf ?R" ..

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

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

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

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

1126 with `\<not> 100 < n` show "(f91 (n + 11), n) \<in> ?R" by simp

1127 qed

1129 text_raw {*

1130 \isamarkupfalse\isabellestyle{tt}

1131 \end{minipage}

1132 \vspace{6pt}\hrule

1133 \caption{McCarthy's 91-function}\label{f91}

1134 \end{figure}

1135 *}

1138 section {* Higher-Order Recursion *}

1140 text {*

1141 Higher-order recursion occurs when recursive calls

1142 are passed as arguments to higher-order combinators such as @{term

1143 map}, @{term filter} etc.

1144 As an example, imagine a datatype of n-ary trees:

1145 *}

1147 datatype 'a tree =

1148 Leaf 'a

1149 | Branch "'a tree list"

1152 text {* \noindent We can define a function which swaps the left and right subtrees recursively, using the

1153 list functions @{const rev} and @{const map}: *}

1155 lemma [simp]: "x \<in> set l \<Longrightarrow> f x < Suc (list_size f l)"

1156 by (induct l) auto

1159 fun mirror :: "'a tree \<Rightarrow> 'a tree"

1160 where

1161 "mirror (Leaf n) = Leaf n"

1162 | "mirror (Branch l) = Branch (rev (map mirror l))"

1165 text {*

1166 \emph{Note: The handling of size functions is currently changing

1167 in the developers version of Isabelle. So this documentation is outdated.}

1168 *}

1170 termination proof

1171 txt {*

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

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

1175 the arguments of the recursive calls? Isabelle gives us the

1176 subgoals

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

1180 So Isabelle seems to know that @{const map} behaves nicely and only

1181 applies the recursive call @{term "mirror"} to elements

1182 of @{term "l"}. Before we discuss where this knowledge comes from,

1183 let us finish the termination proof:

1184 *}

1186 show "wf (measure size)" by simp

1187 next

1188 fix f l and x :: "'a tree"

1189 assume "x \<in> set l"

1190 thus "(x, Branch l) \<in> measure size"

1191 apply simp

1192 txt {*

1193 Simplification returns the following subgoal:

1195 @{text[display] "1. x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"}

1197 We are lacking a property about the function @{term

1198 tree_list_size}, which was generated automatically at the

1199 definition of the @{text tree} type. We should go back and prove

1200 it, by induction.

1201 *}

1202 (*<*)oops(*>*)

1204 text {*

1205 Now the whole termination proof is automatic:

1206 *}

1208 termination

1209 by lexicographic_order

1211 subsection {* Congruence Rules *}

1213 text {*

1214 Let's come back to the question how Isabelle knows about @{const

1215 map}.

1217 The knowledge about map is encoded in so-called congruence rules,

1218 which are special theorems known to the \cmd{function} command. The

1219 rule for map is

1221 @{thm[display] map_cong}

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

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

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

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

1227 @{term l}.

1229 Usually, one such congruence rule is

1230 needed for each higher-order construct that is used when defining

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

1232 If} and @{const Let} are handled by this mechanism. The congruence

1233 rule for @{const If} states that the @{text then} branch is only

1234 relevant if the condition is true, and the @{text else} branch only if it

1235 is false:

1237 @{thm[display] if_cong}

1239 Congruence rules can be added to the

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

1242 The constructs that are predefined in Isabelle, usually

1243 come with the respective congruence rules.

1244 But if you define your own higher-order functions, you will have to

1245 come up with the congruence rules yourself, if you want to use your

1246 functions in recursive definitions.

1247 *}

1249 subsection {* Congruence Rules and Evaluation Order *}

1251 text {*

1252 Higher order logic differs from functional programming languages in

1253 that it has no built-in notion of evaluation order. A program is

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

1255 evaluated.

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

1258 evaluation order implicitly, when we reason about termination.

1259 Congruence rules express that a certain evaluation order is

1260 consistent with the logical definition.

1262 Consider the following function.

1263 *}

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

1266 where

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

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

1270 text {*

1271 As given above, the definition fails. The default configuration

1272 specifies no congruence rule for disjunction. We have to add a

1273 congruence rule that specifies left-to-right evaluation order:

1275 \vspace{1ex}

1276 \noindent @{thm disj_cong}\hfill(@{text "disj_cong"})

1277 \vspace{1ex}

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

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

1281 rule.

1283 However, as evaluation is not a hard-wired concept, we

1284 could just turn everything around by declaring a different

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

1286 *}

1288 lemma disj_cong2[fundef_cong]:

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

1290 by blast

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

1293 where

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

1296 text {*

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

1298 congruence rules.

1300 However, such tweaking should rarely be necessary in

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

1302 works well.

1303 *}

1305 end