author | wenzelm |
Sat, 27 May 2006 17:42:02 +0200 | |
changeset 19736 | d8d0f8f51d69 |
parent 19583 | c5fa77b03442 |
child 19770 | be5c23ebe1eb |
permissions | -rw-r--r-- |
19568 | 1 |
(* Title: HOL/ex/Fundefs.thy |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
||
5 |
Examples of function definitions using the new "function" package. |
|
6 |
*) |
|
7 |
||
8 |
theory Fundefs |
|
9 |
imports Main |
|
10 |
begin |
|
11 |
||
12 |
||
13 |
section {* Very basic *} |
|
14 |
||
15 |
consts fib :: "nat \<Rightarrow> nat" |
|
19736 | 16 |
function |
19568 | 17 |
"fib 0 = 1" |
18 |
"fib (Suc 0) = 1" |
|
19 |
"fib (Suc (Suc n)) = fib n + fib (Suc n)" |
|
19736 | 20 |
by pat_completeness -- {* shows that the patterns are complete *} |
21 |
auto -- {* shows that the patterns are compatible *} |
|
19568 | 22 |
|
19736 | 23 |
text {* we get partial simp and induction rules: *} |
19568 | 24 |
thm fib.psimps |
25 |
thm fib.pinduct |
|
26 |
||
19736 | 27 |
text {* There is also a cases rule to distinguish cases along the definition *} |
19568 | 28 |
thm fib.cases |
29 |
||
19736 | 30 |
text {* Now termination: *} |
19568 | 31 |
termination fib |
19736 | 32 |
by (auto_term "less_than") |
19568 | 33 |
|
34 |
thm fib.simps |
|
35 |
thm fib.induct |
|
36 |
||
37 |
||
38 |
section {* Currying *} |
|
39 |
||
19736 | 40 |
consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
19568 | 41 |
function |
42 |
"add 0 y = y" |
|
43 |
"add (Suc x) y = Suc (add x y)" |
|
44 |
by pat_completeness auto |
|
19736 | 45 |
termination |
19568 | 46 |
by (auto_term "measure fst") |
47 |
||
19736 | 48 |
thm add.induct -- {* Note the curried induction predicate *} |
19568 | 49 |
|
50 |
||
51 |
section {* Nested recursion *} |
|
52 |
||
53 |
||
54 |
consts nz :: "nat \<Rightarrow> nat" |
|
55 |
function |
|
56 |
"nz 0 = 0" |
|
57 |
"nz (Suc x) = nz (nz x)" |
|
58 |
by pat_completeness auto |
|
59 |
||
19736 | 60 |
lemma nz_is_zero: -- {* A lemma we need to prove termination *} |
19583
c5fa77b03442
function-package: Changed record usage to make sml/nj happy...
krauss
parents:
19568
diff
changeset
|
61 |
assumes trm: "x \<in> nz_dom" |
19568 | 62 |
shows "nz x = 0" |
63 |
using trm |
|
64 |
by induct auto |
|
65 |
||
66 |
termination nz |
|
19736 | 67 |
apply (auto_term "less_than") -- {* Oops, it left us something to prove *} |
19568 | 68 |
by (auto simp:nz_is_zero) |
69 |
||
70 |
thm nz.simps |
|
71 |
thm nz.induct |
|
72 |
||
73 |
||
74 |
section {* More general patterns *} |
|
75 |
||
19736 | 76 |
text {* Currently, patterns must always be compatible with each other, since |
19568 | 77 |
no automatich splitting takes place. But the following definition of |
19736 | 78 |
gcd is ok, although patterns overlap: *} |
19568 | 79 |
|
80 |
consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
19736 | 81 |
function |
19568 | 82 |
"gcd2 x 0 = x" |
83 |
"gcd2 0 y = y" |
|
84 |
"gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) |
|
85 |
else gcd2 (x - y) (Suc y))" |
|
86 |
by pat_completeness auto |
|
87 |
termination by (auto_term "measure (\<lambda>(x,y). x + y)") |
|
88 |
||
89 |
thm gcd2.simps |
|
90 |
thm gcd2.induct |
|
91 |
||
92 |
||
19736 | 93 |
text {* General patterns allow even strange definitions: *} |
19568 | 94 |
consts ev :: "nat \<Rightarrow> bool" |
19736 | 95 |
function |
19568 | 96 |
"ev (2 * n) = True" |
97 |
"ev (2 * n + 1) = False" |
|
19736 | 98 |
proof - -- {* completeness is more difficult here \dots *} |
19568 | 99 |
assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P" |
100 |
and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P" |
|
101 |
have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto |
|
102 |
show "P" |
|
19736 | 103 |
proof cases |
19568 | 104 |
assume "x mod 2 = 0" |
105 |
with divmod have "x = 2 * (x div 2)" by simp |
|
106 |
with c1 show "P" . |
|
107 |
next |
|
108 |
assume "x mod 2 \<noteq> 0" |
|
109 |
hence "x mod 2 = 1" by simp |
|
110 |
with divmod have "x = 2 * (x div 2) + 1" by simp |
|
111 |
with c2 show "P" . |
|
112 |
qed |
|
19736 | 113 |
qed presburger+ -- {* solve compatibility with presburger *} |
19568 | 114 |
termination by (auto_term "{}") |
115 |
||
116 |
thm ev.simps |
|
117 |
thm ev.induct |
|
118 |
thm ev.cases |
|
119 |
||
19736 | 120 |
end |