|
1 (* Title: HOL/ex/Functions.thy |
|
2 Author: Alexander Krauss, TU Muenchen |
|
3 *) |
|
4 |
|
5 section \<open>Examples of function definitions\<close> |
|
6 |
|
7 theory Functions |
|
8 imports Main "HOL-Library.Monad_Syntax" |
|
9 begin |
|
10 |
|
11 subsection \<open>Very basic\<close> |
|
12 |
|
13 fun fib :: "nat \<Rightarrow> nat" |
|
14 where |
|
15 "fib 0 = 1" |
|
16 | "fib (Suc 0) = 1" |
|
17 | "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
|
18 |
|
19 text \<open>Partial simp and induction rules:\<close> |
|
20 thm fib.psimps |
|
21 thm fib.pinduct |
|
22 |
|
23 text \<open>There is also a cases rule to distinguish cases along the definition:\<close> |
|
24 thm fib.cases |
|
25 |
|
26 |
|
27 text \<open>Total simp and induction rules:\<close> |
|
28 thm fib.simps |
|
29 thm fib.induct |
|
30 |
|
31 text \<open>Elimination rules:\<close> |
|
32 thm fib.elims |
|
33 |
|
34 |
|
35 subsection \<open>Currying\<close> |
|
36 |
|
37 fun add |
|
38 where |
|
39 "add 0 y = y" |
|
40 | "add (Suc x) y = Suc (add x y)" |
|
41 |
|
42 thm add.simps |
|
43 thm add.induct \<comment> \<open>Note the curried induction predicate\<close> |
|
44 |
|
45 |
|
46 subsection \<open>Nested recursion\<close> |
|
47 |
|
48 function nz |
|
49 where |
|
50 "nz 0 = 0" |
|
51 | "nz (Suc x) = nz (nz x)" |
|
52 by pat_completeness auto |
|
53 |
|
54 lemma nz_is_zero: \<comment> \<open>A lemma we need to prove termination\<close> |
|
55 assumes trm: "nz_dom x" |
|
56 shows "nz x = 0" |
|
57 using trm |
|
58 by induct (auto simp: nz.psimps) |
|
59 |
|
60 termination nz |
|
61 by (relation "less_than") (auto simp:nz_is_zero) |
|
62 |
|
63 thm nz.simps |
|
64 thm nz.induct |
|
65 |
|
66 |
|
67 subsubsection \<open>Here comes McCarthy's 91-function\<close> |
|
68 |
|
69 function f91 :: "nat \<Rightarrow> nat" |
|
70 where |
|
71 "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" |
|
72 by pat_completeness auto |
|
73 |
|
74 text \<open>Prove a lemma before attempting a termination proof:\<close> |
|
75 lemma f91_estimate: |
|
76 assumes trm: "f91_dom n" |
|
77 shows "n < f91 n + 11" |
|
78 using trm by induct (auto simp: f91.psimps) |
|
79 |
|
80 termination |
|
81 proof |
|
82 let ?R = "measure (\<lambda>x. 101 - x)" |
|
83 show "wf ?R" .. |
|
84 |
|
85 fix n :: nat |
|
86 assume "\<not> 100 < n" \<comment> \<open>Inner call\<close> |
|
87 then show "(n + 11, n) \<in> ?R" by simp |
|
88 |
|
89 assume inner_trm: "f91_dom (n + 11)" \<comment> \<open>Outer call\<close> |
|
90 with f91_estimate have "n + 11 < f91 (n + 11) + 11" . |
|
91 with \<open>\<not> 100 < n\<close> show "(f91 (n + 11), n) \<in> ?R" by simp |
|
92 qed |
|
93 |
|
94 text \<open>Now trivial (even though it does not belong here):\<close> |
|
95 lemma "f91 n = (if 100 < n then n - 10 else 91)" |
|
96 by (induct n rule: f91.induct) auto |
|
97 |
|
98 |
|
99 subsubsection \<open>Here comes Takeuchi's function\<close> |
|
100 |
|
101 definition tak_m1 where "tak_m1 = (\<lambda>(x,y,z). if x \<le> y then 0 else 1)" |
|
102 definition tak_m2 where "tak_m2 = (\<lambda>(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))" |
|
103 definition tak_m3 where "tak_m3 = (\<lambda>(x,y,z). nat (x - Min {x, y, z}))" |
|
104 |
|
105 function tak :: "int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int" where |
|
106 "tak x y z = (if x \<le> y then y else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y))" |
|
107 by auto |
|
108 |
|
109 lemma tak_pcorrect: |
|
110 "tak_dom (x, y, z) \<Longrightarrow> tak x y z = (if x \<le> y then y else if y \<le> z then z else x)" |
|
111 by (induction x y z rule: tak.pinduct) (auto simp: tak.psimps) |
|
112 |
|
113 termination |
|
114 by (relation "tak_m1 <*mlex*> tak_m2 <*mlex*> tak_m3 <*mlex*> {}") |
|
115 (auto simp: mlex_iff wf_mlex tak_pcorrect tak_m1_def tak_m2_def tak_m3_def min_def max_def) |
|
116 |
|
117 theorem tak_correct: "tak x y z = (if x \<le> y then y else if y \<le> z then z else x)" |
|
118 by (induction x y z rule: tak.induct) auto |
|
119 |
|
120 |
|
121 subsection \<open>More general patterns\<close> |
|
122 |
|
123 subsubsection \<open>Overlapping patterns\<close> |
|
124 |
|
125 text \<open> |
|
126 Currently, patterns must always be compatible with each other, since |
|
127 no automatic splitting takes place. But the following definition of |
|
128 GCD is OK, although patterns overlap: |
|
129 \<close> |
|
130 |
|
131 fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
132 where |
|
133 "gcd2 x 0 = x" |
|
134 | "gcd2 0 y = y" |
|
135 | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) |
|
136 else gcd2 (x - y) (Suc y))" |
|
137 |
|
138 thm gcd2.simps |
|
139 thm gcd2.induct |
|
140 |
|
141 |
|
142 subsubsection \<open>Guards\<close> |
|
143 |
|
144 text \<open>We can reformulate the above example using guarded patterns:\<close> |
|
145 |
|
146 function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
147 where |
|
148 "gcd3 x 0 = x" |
|
149 | "gcd3 0 y = y" |
|
150 | "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y" |
|
151 | "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "\<not> x < y" |
|
152 apply (case_tac x, case_tac a, auto) |
|
153 apply (case_tac ba, auto) |
|
154 done |
|
155 termination by lexicographic_order |
|
156 |
|
157 thm gcd3.simps |
|
158 thm gcd3.induct |
|
159 |
|
160 |
|
161 text \<open>General patterns allow even strange definitions:\<close> |
|
162 |
|
163 function ev :: "nat \<Rightarrow> bool" |
|
164 where |
|
165 "ev (2 * n) = True" |
|
166 | "ev (2 * n + 1) = False" |
|
167 proof - \<comment> \<open>completeness is more difficult here \dots\<close> |
|
168 fix P :: bool |
|
169 fix x :: nat |
|
170 assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P" |
|
171 and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P" |
|
172 have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto |
|
173 show P |
|
174 proof (cases "x mod 2 = 0") |
|
175 case True |
|
176 with divmod have "x = 2 * (x div 2)" by simp |
|
177 with c1 show "P" . |
|
178 next |
|
179 case False |
|
180 then have "x mod 2 = 1" by simp |
|
181 with divmod have "x = 2 * (x div 2) + 1" by simp |
|
182 with c2 show "P" . |
|
183 qed |
|
184 qed presburger+ \<comment> \<open>solve compatibility with presburger\<close> |
|
185 termination by lexicographic_order |
|
186 |
|
187 thm ev.simps |
|
188 thm ev.induct |
|
189 thm ev.cases |
|
190 |
|
191 |
|
192 subsection \<open>Mutual Recursion\<close> |
|
193 |
|
194 fun evn od :: "nat \<Rightarrow> bool" |
|
195 where |
|
196 "evn 0 = True" |
|
197 | "od 0 = False" |
|
198 | "evn (Suc n) = od n" |
|
199 | "od (Suc n) = evn n" |
|
200 |
|
201 thm evn.simps |
|
202 thm od.simps |
|
203 |
|
204 thm evn_od.induct |
|
205 thm evn_od.termination |
|
206 |
|
207 thm evn.elims |
|
208 thm od.elims |
|
209 |
|
210 |
|
211 subsection \<open>Definitions in local contexts\<close> |
|
212 |
|
213 locale my_monoid = |
|
214 fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
215 and un :: "'a" |
|
216 assumes assoc: "opr (opr x y) z = opr x (opr y z)" |
|
217 and lunit: "opr un x = x" |
|
218 and runit: "opr x un = x" |
|
219 begin |
|
220 |
|
221 fun foldR :: "'a list \<Rightarrow> 'a" |
|
222 where |
|
223 "foldR [] = un" |
|
224 | "foldR (x # xs) = opr x (foldR xs)" |
|
225 |
|
226 fun foldL :: "'a list \<Rightarrow> 'a" |
|
227 where |
|
228 "foldL [] = un" |
|
229 | "foldL [x] = x" |
|
230 | "foldL (x # y # ys) = foldL (opr x y # ys)" |
|
231 |
|
232 thm foldL.simps |
|
233 |
|
234 lemma foldR_foldL: "foldR xs = foldL xs" |
|
235 by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc) |
|
236 |
|
237 thm foldR_foldL |
|
238 |
|
239 end |
|
240 |
|
241 thm my_monoid.foldL.simps |
|
242 thm my_monoid.foldR_foldL |
|
243 |
|
244 |
|
245 subsection \<open>\<open>fun_cases\<close>\<close> |
|
246 |
|
247 subsubsection \<open>Predecessor\<close> |
|
248 |
|
249 fun pred :: "nat \<Rightarrow> nat" |
|
250 where |
|
251 "pred 0 = 0" |
|
252 | "pred (Suc n) = n" |
|
253 |
|
254 thm pred.elims |
|
255 |
|
256 lemma |
|
257 assumes "pred x = y" |
|
258 obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n" |
|
259 by (fact pred.elims[OF assms]) |
|
260 |
|
261 |
|
262 text \<open>If the predecessor of a number is 0, that number must be 0 or 1.\<close> |
|
263 |
|
264 fun_cases pred0E[elim]: "pred n = 0" |
|
265 |
|
266 lemma "pred n = 0 \<Longrightarrow> n = 0 \<or> n = Suc 0" |
|
267 by (erule pred0E) metis+ |
|
268 |
|
269 text \<open> |
|
270 Other expressions on the right-hand side also work, but whether the |
|
271 generated rule is useful depends on how well the simplifier can |
|
272 simplify it. This example works well: |
|
273 \<close> |
|
274 |
|
275 fun_cases pred42E[elim]: "pred n = 42" |
|
276 |
|
277 lemma "pred n = 42 \<Longrightarrow> n = 43" |
|
278 by (erule pred42E) |
|
279 |
|
280 |
|
281 subsubsection \<open>List to option\<close> |
|
282 |
|
283 fun list_to_option :: "'a list \<Rightarrow> 'a option" |
|
284 where |
|
285 "list_to_option [x] = Some x" |
|
286 | "list_to_option _ = None" |
|
287 |
|
288 fun_cases list_to_option_NoneE: "list_to_option xs = None" |
|
289 and list_to_option_SomeE: "list_to_option xs = Some x" |
|
290 |
|
291 lemma "list_to_option xs = Some y \<Longrightarrow> xs = [y]" |
|
292 by (erule list_to_option_SomeE) |
|
293 |
|
294 |
|
295 subsubsection \<open>Boolean Functions\<close> |
|
296 |
|
297 fun xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" |
|
298 where |
|
299 "xor False False = False" |
|
300 | "xor True True = False" |
|
301 | "xor _ _ = True" |
|
302 |
|
303 thm xor.elims |
|
304 |
|
305 text \<open> |
|
306 \<open>fun_cases\<close> does not only recognise function equations, but also works with |
|
307 functions that return a boolean, e.g.: |
|
308 \<close> |
|
309 |
|
310 fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\<not>xor a b" |
|
311 print_theorems |
|
312 |
|
313 |
|
314 subsubsection \<open>Many parameters\<close> |
|
315 |
|
316 fun sum4 :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
|
317 where "sum4 a b c d = a + b + c + d" |
|
318 |
|
319 fun_cases sum40E: "sum4 a b c d = 0" |
|
320 |
|
321 lemma "sum4 a b c d = 0 \<Longrightarrow> a = 0" |
|
322 by (erule sum40E) |
|
323 |
|
324 |
|
325 subsection \<open>Partial Function Definitions\<close> |
|
326 |
|
327 text \<open>Partial functions in the option monad:\<close> |
|
328 |
|
329 partial_function (option) |
|
330 collatz :: "nat \<Rightarrow> nat list option" |
|
331 where |
|
332 "collatz n = |
|
333 (if n \<le> 1 then Some [n] |
|
334 else if even n |
|
335 then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) } |
|
336 else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})" |
|
337 |
|
338 declare collatz.simps[code] |
|
339 value "collatz 23" |
|
340 |
|
341 |
|
342 text \<open>Tail-recursive functions:\<close> |
|
343 |
|
344 partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" |
|
345 where |
|
346 "fixpoint f x = (if f x = x then x else fixpoint f (f x))" |
|
347 |
|
348 |
|
349 subsection \<open>Regression tests\<close> |
|
350 |
|
351 text \<open> |
|
352 The following examples mainly serve as tests for the |
|
353 function package. |
|
354 \<close> |
|
355 |
|
356 fun listlen :: "'a list \<Rightarrow> nat" |
|
357 where |
|
358 "listlen [] = 0" |
|
359 | "listlen (x#xs) = Suc (listlen xs)" |
|
360 |
|
361 |
|
362 subsubsection \<open>Context recursion\<close> |
|
363 |
|
364 fun f :: "nat \<Rightarrow> nat" |
|
365 where |
|
366 zero: "f 0 = 0" |
|
367 | succ: "f (Suc n) = (if f n = 0 then 0 else f n)" |
|
368 |
|
369 |
|
370 subsubsection \<open>A combination of context and nested recursion\<close> |
|
371 |
|
372 function h :: "nat \<Rightarrow> nat" |
|
373 where |
|
374 "h 0 = 0" |
|
375 | "h (Suc n) = (if h n = 0 then h (h n) else h n)" |
|
376 by pat_completeness auto |
|
377 |
|
378 |
|
379 subsubsection \<open>Context, but no recursive call\<close> |
|
380 |
|
381 fun i :: "nat \<Rightarrow> nat" |
|
382 where |
|
383 "i 0 = 0" |
|
384 | "i (Suc n) = (if n = 0 then 0 else i n)" |
|
385 |
|
386 |
|
387 subsubsection \<open>Tupled nested recursion\<close> |
|
388 |
|
389 fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
390 where |
|
391 "fa 0 y = 0" |
|
392 | "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)" |
|
393 |
|
394 |
|
395 subsubsection \<open>Let\<close> |
|
396 |
|
397 fun j :: "nat \<Rightarrow> nat" |
|
398 where |
|
399 "j 0 = 0" |
|
400 | "j (Suc n) = (let u = n in Suc (j u))" |
|
401 |
|
402 |
|
403 text \<open>There were some problems with fresh names \dots\<close> |
|
404 function k :: "nat \<Rightarrow> nat" |
|
405 where |
|
406 "k x = (let a = x; b = x in k x)" |
|
407 by pat_completeness auto |
|
408 |
|
409 |
|
410 function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" |
|
411 where |
|
412 "f2 p = (let (x,y) = p in f2 (y,x))" |
|
413 by pat_completeness auto |
|
414 |
|
415 |
|
416 subsubsection \<open>Abbreviations\<close> |
|
417 |
|
418 fun f3 :: "'a set \<Rightarrow> bool" |
|
419 where |
|
420 "f3 x = finite x" |
|
421 |
|
422 |
|
423 subsubsection \<open>Simple Higher-Order Recursion\<close> |
|
424 |
|
425 datatype 'a tree = Leaf 'a | Branch "'a tree list" |
|
426 |
|
427 fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree" |
|
428 where |
|
429 "treemap fn (Leaf n) = (Leaf (fn n))" |
|
430 | "treemap fn (Branch l) = (Branch (map (treemap fn) l))" |
|
431 |
|
432 fun tinc :: "nat tree \<Rightarrow> nat tree" |
|
433 where |
|
434 "tinc (Leaf n) = Leaf (Suc n)" |
|
435 | "tinc (Branch l) = Branch (map tinc l)" |
|
436 |
|
437 fun testcase :: "'a tree \<Rightarrow> 'a list" |
|
438 where |
|
439 "testcase (Leaf a) = [a]" |
|
440 | "testcase (Branch x) = |
|
441 (let xs = concat (map testcase x); |
|
442 ys = concat (map testcase x) in |
|
443 xs @ ys)" |
|
444 |
|
445 |
|
446 subsubsection \<open>Pattern matching on records\<close> |
|
447 |
|
448 record point = |
|
449 Xcoord :: int |
|
450 Ycoord :: int |
|
451 |
|
452 function swp :: "point \<Rightarrow> point" |
|
453 where |
|
454 "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>" |
|
455 proof - |
|
456 fix P x |
|
457 assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P" |
|
458 then show P by (cases x) |
|
459 qed auto |
|
460 termination by rule auto |
|
461 |
|
462 |
|
463 subsubsection \<open>The diagonal function\<close> |
|
464 |
|
465 fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat" |
|
466 where |
|
467 "diag x True False = 1" |
|
468 | "diag False y True = 2" |
|
469 | "diag True False z = 3" |
|
470 | "diag True True True = 4" |
|
471 | "diag False False False = 5" |
|
472 |
|
473 |
|
474 subsubsection \<open>Many equations (quadratic blowup)\<close> |
|
475 |
|
476 datatype DT = |
|
477 A | B | C | D | E | F | G | H | I | J | K | L | M | N | P |
|
478 | Q | R | S | T | U | V |
|
479 |
|
480 fun big :: "DT \<Rightarrow> nat" |
|
481 where |
|
482 "big A = 0" |
|
483 | "big B = 0" |
|
484 | "big C = 0" |
|
485 | "big D = 0" |
|
486 | "big E = 0" |
|
487 | "big F = 0" |
|
488 | "big G = 0" |
|
489 | "big H = 0" |
|
490 | "big I = 0" |
|
491 | "big J = 0" |
|
492 | "big K = 0" |
|
493 | "big L = 0" |
|
494 | "big M = 0" |
|
495 | "big N = 0" |
|
496 | "big P = 0" |
|
497 | "big Q = 0" |
|
498 | "big R = 0" |
|
499 | "big S = 0" |
|
500 | "big T = 0" |
|
501 | "big U = 0" |
|
502 | "big V = 0" |
|
503 |
|
504 |
|
505 subsubsection \<open>Automatic pattern splitting\<close> |
|
506 |
|
507 fun f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool" |
|
508 where |
|
509 "f4 0 0 = True" |
|
510 | "f4 _ _ = False" |
|
511 |
|
512 |
|
513 subsubsection \<open>Polymorphic partial-function\<close> |
|
514 |
|
515 partial_function (option) f5 :: "'a list \<Rightarrow> 'a option" |
|
516 where |
|
517 "f5 x = f5 x" |
|
518 |
|
519 end |