src/HOL/ex/Fundefs.thy
 author bulwahn Fri Oct 21 11:17:14 2011 +0200 (2011-10-21) changeset 45231 d85a2fdc586c parent 45008 8b74cfea913a child 53611 437c0a63bb16 permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
1 (*  Title:      HOL/ex/Fundefs.thy
2     Author:     Alexander Krauss, TU Muenchen
3 *)
5 header {* Examples of function definitions *}
7 theory Fundefs
8 imports Parity "~~/src/HOL/Library/Monad_Syntax"
9 begin
11 subsection {* Very basic *}
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)"
19 text {* partial simp and induction rules: *}
20 thm fib.psimps
21 thm fib.pinduct
23 text {* There is also a cases rule to distinguish cases along the definition *}
24 thm fib.cases
27 text {* total simp and induction rules: *}
28 thm fib.simps
29 thm fib.induct
31 subsection {* Currying *}
34 where
35   "add 0 y = y"
36 | "add (Suc x) y = Suc (add x y)"
39 thm add.induct -- {* Note the curried induction predicate *}
42 subsection {* Nested recursion *}
44 function nz
45 where
46   "nz 0 = 0"
47 | "nz (Suc x) = nz (nz x)"
48 by pat_completeness auto
50 lemma nz_is_zero: -- {* A lemma we need to prove termination *}
51   assumes trm: "nz_dom x"
52   shows "nz x = 0"
53 using trm
54 by induct (auto simp: nz.psimps)
56 termination nz
57   by (relation "less_than") (auto simp:nz_is_zero)
59 thm nz.simps
60 thm nz.induct
62 text {* Here comes McCarthy's 91-function *}
65 function f91 :: "nat => nat"
66 where
67   "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
68 by pat_completeness auto
70 (* Prove a lemma before attempting a termination proof *)
71 lemma f91_estimate:
72   assumes trm: "f91_dom n"
73   shows "n < f91 n + 11"
74 using trm by induct (auto simp: f91.psimps)
76 termination
77 proof
78   let ?R = "measure (%x. 101 - x)"
79   show "wf ?R" ..
81   fix n::nat assume "~ 100 < n" (* Inner call *)
82   thus "(n + 11, n) : ?R" by simp
84   assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
85   with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
86   with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp
87 qed
89 text{* Now trivial (even though it does not belong here): *}
90 lemma "f91 n = (if 100 < n then n - 10 else 91)"
91 by (induct n rule:f91.induct) auto
94 subsection {* More general patterns *}
96 subsubsection {* Overlapping patterns *}
98 text {* Currently, patterns must always be compatible with each other, since
99 no automatic splitting takes place. But the following definition of
100 gcd is ok, although patterns overlap: *}
102 fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
103 where
104   "gcd2 x 0 = x"
105 | "gcd2 0 y = y"
106 | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
107                                     else gcd2 (x - y) (Suc y))"
109 thm gcd2.simps
110 thm gcd2.induct
112 subsubsection {* Guards *}
114 text {* We can reformulate the above example using guarded patterns *}
116 function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
117 where
118   "gcd3 x 0 = x"
119 | "gcd3 0 y = y"
120 | "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
121 | "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
122   apply (case_tac x, case_tac a, auto)
123   apply (case_tac ba, auto)
124   done
125 termination by lexicographic_order
127 thm gcd3.simps
128 thm gcd3.induct
131 text {* General patterns allow even strange definitions: *}
133 function ev :: "nat \<Rightarrow> bool"
134 where
135   "ev (2 * n) = True"
136 | "ev (2 * n + 1) = False"
137 proof -  -- {* completeness is more difficult here \dots *}
138   fix P :: bool
139     and x :: nat
140   assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
141     and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
142   have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
143   show "P"
144   proof cases
145     assume "x mod 2 = 0"
146     with divmod have "x = 2 * (x div 2)" by simp
147     with c1 show "P" .
148   next
149     assume "x mod 2 \<noteq> 0"
150     hence "x mod 2 = 1" by simp
151     with divmod have "x = 2 * (x div 2) + 1" by simp
152     with c2 show "P" .
153   qed
154 qed presburger+ -- {* solve compatibility with presburger *}
155 termination by lexicographic_order
157 thm ev.simps
158 thm ev.induct
159 thm ev.cases
162 subsection {* Mutual Recursion *}
164 fun evn od :: "nat \<Rightarrow> bool"
165 where
166   "evn 0 = True"
167 | "od 0 = False"
168 | "evn (Suc n) = od n"
169 | "od (Suc n) = evn n"
171 thm evn.simps
172 thm od.simps
174 thm evn_od.induct
175 thm evn_od.termination
178 subsection {* Definitions in local contexts *}
180 locale my_monoid =
181 fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
182   and un :: "'a"
183 assumes assoc: "opr (opr x y) z = opr x (opr y z)"
184   and lunit: "opr un x = x"
185   and runit: "opr x un = x"
186 begin
188 fun foldR :: "'a list \<Rightarrow> 'a"
189 where
190   "foldR [] = un"
191 | "foldR (x#xs) = opr x (foldR xs)"
193 fun foldL :: "'a list \<Rightarrow> 'a"
194 where
195   "foldL [] = un"
196 | "foldL [x] = x"
197 | "foldL (x#y#ys) = foldL (opr x y # ys)"
199 thm foldL.simps
201 lemma foldR_foldL: "foldR xs = foldL xs"
202 by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
204 thm foldR_foldL
206 end
208 thm my_monoid.foldL.simps
209 thm my_monoid.foldR_foldL
212 subsection {* Partial Function Definitions *}
214 text {* Partial functions in the option monad: *}
216 partial_function (option)
217   collatz :: "nat \<Rightarrow> nat list option"
218 where
219   "collatz n =
220   (if n \<le> 1 then Some [n]
221    else if even n
222      then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
223      else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
225 declare collatz.simps[code]
226 value "collatz 23"
229 text {* Tail-recursive functions: *}
231 partial_function (tailrec) fixpoint :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"
232 where
233   "fixpoint f x = (if f x = x then x else fixpoint f (f x))"
236 subsection {* Regression tests *}
238 text {* The following examples mainly serve as tests for the
239   function package *}
241 fun listlen :: "'a list \<Rightarrow> nat"
242 where
243   "listlen [] = 0"
244 | "listlen (x#xs) = Suc (listlen xs)"
246 (* Context recursion *)
248 fun f :: "nat \<Rightarrow> nat"
249 where
250   zero: "f 0 = 0"
251 | succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
254 (* A combination of context and nested recursion *)
255 function h :: "nat \<Rightarrow> nat"
256 where
257   "h 0 = 0"
258 | "h (Suc n) = (if h n = 0 then h (h n) else h n)"
259   by pat_completeness auto
262 (* Context, but no recursive call: *)
263 fun i :: "nat \<Rightarrow> nat"
264 where
265   "i 0 = 0"
266 | "i (Suc n) = (if n = 0 then 0 else i n)"
269 (* Tupled nested recursion *)
270 fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
271 where
272   "fa 0 y = 0"
273 | "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
275 (* Let *)
276 fun j :: "nat \<Rightarrow> nat"
277 where
278   "j 0 = 0"
279 | "j (Suc n) = (let u = n  in Suc (j u))"
282 (* There were some problems with fresh names\<dots> *)
283 function  k :: "nat \<Rightarrow> nat"
284 where
285   "k x = (let a = x; b = x in k x)"
286   by pat_completeness auto
289 function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
290 where
291   "f2 p = (let (x,y) = p in f2 (y,x))"
292   by pat_completeness auto
295 (* abbreviations *)
296 fun f3 :: "'a set \<Rightarrow> bool"
297 where
298   "f3 x = finite x"
301 (* Simple Higher-Order Recursion *)
302 datatype 'a tree =
303   Leaf 'a
304   | Branch "'a tree list"
306 fun treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
307 where
308   "treemap fn (Leaf n) = (Leaf (fn n))"
309 | "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
311 fun tinc :: "nat tree \<Rightarrow> nat tree"
312 where
313   "tinc (Leaf n) = Leaf (Suc n)"
314 | "tinc (Branch l) = Branch (map tinc l)"
316 fun testcase :: "'a tree \<Rightarrow> 'a list"
317 where
318   "testcase (Leaf a) = [a]"
319 | "testcase (Branch x) =
320     (let xs = concat (map testcase x);
321          ys = concat (map testcase x) in
322      xs @ ys)"
325 (* Pattern matching on records *)
326 record point =
327   Xcoord :: int
328   Ycoord :: int
330 function swp :: "point \<Rightarrow> point"
331 where
332   "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
333 proof -
334   fix P x
335   assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
336   thus "P"
337     by (cases x)
338 qed auto
339 termination by rule auto
342 (* The diagonal function *)
343 fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
344 where
345   "diag x True False = 1"
346 | "diag False y True = 2"
347 | "diag True False z = 3"
348 | "diag True True True = 4"
349 | "diag False False False = 5"
352 (* Many equations (quadratic blowup) *)
353 datatype DT =
354   A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
355 | Q | R | S | T | U | V
357 fun big :: "DT \<Rightarrow> nat"
358 where
359   "big A = 0"
360 | "big B = 0"
361 | "big C = 0"
362 | "big D = 0"
363 | "big E = 0"
364 | "big F = 0"
365 | "big G = 0"
366 | "big H = 0"
367 | "big I = 0"
368 | "big J = 0"
369 | "big K = 0"
370 | "big L = 0"
371 | "big M = 0"
372 | "big N = 0"
373 | "big P = 0"
374 | "big Q = 0"
375 | "big R = 0"
376 | "big S = 0"
377 | "big T = 0"
378 | "big U = 0"
379 | "big V = 0"
382 (* automatic pattern splitting *)
383 fun
384   f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool"
385 where
386   "f4 0 0 = True"
387 | "f4 _ _ = False"
390 (* polymorphic partial_function *)
391 partial_function (option) f5 :: "'a list \<Rightarrow> 'a option"
392 where
393   "f5 x = f5 x"
395 end