author | krauss |
Wed, 13 Sep 2006 12:05:50 +0200 | |
changeset 20523 | 36a59e5d0039 |
parent 20270 | 3abe7dae681e |
child 20528 | 4ade644022dd |
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 |
||
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
8 |
theory Fundefs |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
9 |
imports Main "../FundefDebug" |
19568 | 10 |
begin |
11 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
12 |
|
19568 | 13 |
section {* Very basic *} |
14 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
15 |
ML "trace_simp := false" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
16 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
17 |
fun fib :: "nat \<Rightarrow> nat" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
18 |
where |
19568 | 19 |
"fib 0 = 1" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
20 |
| "fib (Suc 0) = 1" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
21 |
| "fib (Suc (Suc n)) = fib n + fib (Suc n)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
22 |
|
19568 | 23 |
|
19736 | 24 |
text {* we get partial simp and induction rules: *} |
19568 | 25 |
thm fib.psimps |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
26 |
thm fib.pinduct |
19568 | 27 |
|
19736 | 28 |
text {* There is also a cases rule to distinguish cases along the definition *} |
19568 | 29 |
thm fib.cases |
30 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
31 |
thm fib.domintros |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
32 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
33 |
|
19736 | 34 |
text {* Now termination: *} |
19568 | 35 |
termination fib |
19736 | 36 |
by (auto_term "less_than") |
19568 | 37 |
|
38 |
thm fib.simps |
|
39 |
thm fib.induct |
|
40 |
||
41 |
||
42 |
section {* Currying *} |
|
43 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
44 |
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
45 |
where |
19568 | 46 |
"add 0 y = y" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
47 |
| "add (Suc x) y = Suc (add x y)" |
19736 | 48 |
termination |
19568 | 49 |
by (auto_term "measure fst") |
50 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
51 |
thm add.simps |
19736 | 52 |
thm add.induct -- {* Note the curried induction predicate *} |
19568 | 53 |
|
54 |
||
55 |
section {* Nested recursion *} |
|
56 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
57 |
fun nz :: "nat \<Rightarrow> nat" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
58 |
where |
19568 | 59 |
"nz 0 = 0" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
60 |
| "nz (Suc x) = nz (nz x)" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
61 |
|
19568 | 62 |
|
19736 | 63 |
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
|
64 |
assumes trm: "x \<in> nz_dom" |
19568 | 65 |
shows "nz x = 0" |
66 |
using trm |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
67 |
by induct auto |
19568 | 68 |
|
69 |
termination nz |
|
19736 | 70 |
apply (auto_term "less_than") -- {* Oops, it left us something to prove *} |
19568 | 71 |
by (auto simp:nz_is_zero) |
72 |
||
73 |
thm nz.simps |
|
74 |
thm nz.induct |
|
75 |
||
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
76 |
text {* Here comes McCarthy's 91-function *} |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
77 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
78 |
fun f91 :: "nat => nat" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
79 |
where |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
80 |
"f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
81 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
82 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
83 |
(* Prove a lemma before attempting a termination proof *) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
84 |
lemma f91_estimate: |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
85 |
assumes trm: "n : f91_dom" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
86 |
shows "n < f91 n + 11" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
87 |
using trm by induct auto |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
88 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
89 |
termination |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
90 |
proof |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
91 |
let ?R = "measure (%x. 101 - x)" |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
92 |
show "wf ?R" .. |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
93 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
94 |
fix n::nat assume "~ 100 < n" (* Inner call *) |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19922
diff
changeset
|
95 |
thus "(n + 11, n) : ?R" by simp |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
96 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
97 |
assume inner_trm: "n + 11 : f91_dom" (* Outer call *) |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
98 |
with f91_estimate have "n + 11 < f91 (n + 11) + 11" . |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19922
diff
changeset
|
99 |
with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
100 |
qed |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
101 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
102 |
|
19568 | 103 |
|
104 |
section {* More general patterns *} |
|
105 |
||
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
106 |
subsection {* Overlapping patterns *} |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
107 |
|
19736 | 108 |
text {* Currently, patterns must always be compatible with each other, since |
20270
3abe7dae681e
Function package can now do automatic splits of overlapping datatype patterns
krauss
parents:
19922
diff
changeset
|
109 |
no automatic splitting takes place. But the following definition of |
19736 | 110 |
gcd is ok, although patterns overlap: *} |
19568 | 111 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
112 |
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
113 |
where |
19568 | 114 |
"gcd2 x 0 = x" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
115 |
| "gcd2 0 y = y" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
116 |
| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
117 |
else gcd2 (x - y) (Suc y))" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
118 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
119 |
|
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
120 |
termination |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
121 |
by (auto_term "(measure (%x. x)) <*lex*> (measure (%x. x))") |
19568 | 122 |
|
123 |
thm gcd2.simps |
|
124 |
thm gcd2.induct |
|
125 |
||
126 |
||
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
127 |
subsection {* Guards *} |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
128 |
|
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
129 |
text {* We can reformulate the above example using guarded patterns *} |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
130 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
131 |
function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
132 |
where |
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
133 |
"gcd3 x 0 = x" |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
134 |
"gcd3 0 y = y" |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
135 |
"x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
136 |
"\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" |
19922 | 137 |
apply (case_tac x, case_tac a, auto) |
138 |
apply (case_tac ba, auto) |
|
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
139 |
done |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
140 |
|
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
141 |
termination |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
142 |
by (auto_term "measure (\<lambda>(x,y). x + y)") |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
143 |
|
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
144 |
thm gcd3.simps |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
145 |
thm gcd3.induct |
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
146 |
|
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
147 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
148 |
text {* General patterns allow even strange definitions: *} |
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset
|
149 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
150 |
function ev :: "nat \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
151 |
where |
19568 | 152 |
"ev (2 * n) = True" |
153 |
"ev (2 * n + 1) = False" |
|
19736 | 154 |
proof - -- {* completeness is more difficult here \dots *} |
19922 | 155 |
fix P :: bool |
156 |
and x :: nat |
|
19568 | 157 |
assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P" |
158 |
and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P" |
|
159 |
have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto |
|
160 |
show "P" |
|
19736 | 161 |
proof cases |
19568 | 162 |
assume "x mod 2 = 0" |
163 |
with divmod have "x = 2 * (x div 2)" by simp |
|
164 |
with c1 show "P" . |
|
165 |
next |
|
166 |
assume "x mod 2 \<noteq> 0" |
|
167 |
hence "x mod 2 = 1" by simp |
|
168 |
with divmod have "x = 2 * (x div 2) + 1" by simp |
|
169 |
with c2 show "P" . |
|
170 |
qed |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
171 |
qed presburger+ -- {* solve compatibility with presburger *} |
19568 | 172 |
termination by (auto_term "{}") |
173 |
||
174 |
thm ev.simps |
|
175 |
thm ev.induct |
|
176 |
thm ev.cases |
|
177 |
||
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
178 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
179 |
section {* Mutual Recursion *} |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
180 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
181 |
fun evn od :: "nat \<Rightarrow> bool" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
182 |
where |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
183 |
"evn 0 = True" |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
184 |
| "od 0 = False" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
185 |
| "evn (Suc n) = od n" |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset
|
186 |
| "od (Suc n) = evn n" |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
187 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
188 |
thm evn.psimps |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
189 |
thm od.psimps |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
190 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
191 |
thm evn_od.pinduct |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
192 |
thm evn_od.termination |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
193 |
thm evn_od.domintros |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
194 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
195 |
termination |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
196 |
by (auto_term "measure (sum_case (%n. n) (%n. n))") |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
197 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
198 |
thm evn.simps |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
199 |
thm od.simps |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
200 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset
|
201 |
|
19736 | 202 |
end |