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