author  nipkow 
Tue, 14 Oct 2008 13:24:07 +0200  
changeset 28584  58ac551ce1ce 
parent 25680  909bfa21acc2 
child 36269  fa30cbb455df 
permissions  rwrr 
19568  1 
(* Title: HOL/ex/Fundefs.thy 
2 
ID: $Id$ 

3 
Author: Alexander Krauss, TU Muenchen 

22726  4 
*) 
19568  5 

22726  6 
header {* Examples of function definitions *} 
19568  7 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

8 
theory Fundefs 
20528  9 
imports Main 
19568  10 
begin 
11 

22726  12 
subsection {* Very basic *} 
19568  13 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

14 
fun fib :: "nat \<Rightarrow> nat" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

15 
where 
19568  16 
"fib 0 = 1" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

17 
 "fib (Suc 0) = 1" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

18 
 "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

19 

21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21240
diff
changeset

20 
text {* partial simp and induction rules: *} 
19568  21 
thm fib.psimps 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

22 
thm fib.pinduct 
19568  23 

19736  24 
text {* There is also a cases rule to distinguish cases along the definition *} 
19568  25 
thm fib.cases 
26 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

27 

21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21240
diff
changeset

28 
text {* total simp and induction rules: *} 
19568  29 
thm fib.simps 
30 
thm fib.induct 

31 

22726  32 
subsection {* Currying *} 
19568  33 

25170  34 
fun add 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

35 
where 
19568  36 
"add 0 y = y" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

37 
 "add (Suc x) y = Suc (add x y)" 
19568  38 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

39 
thm add.simps 
19736  40 
thm add.induct  {* Note the curried induction predicate *} 
19568  41 

42 

22726  43 
subsection {* Nested recursion *} 
19568  44 

25170  45 
function nz 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

46 
where 
19568  47 
"nz 0 = 0" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

48 
 "nz (Suc x) = nz (nz x)" 
21240
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

49 
by pat_completeness auto 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

50 

19736  51 
lemma nz_is_zero:  {* A lemma we need to prove termination *} 
21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20536
diff
changeset

52 
assumes trm: "nz_dom x" 
19568  53 
shows "nz x = 0" 
54 
using trm 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

55 
by induct auto 
19568  56 

57 
termination nz 

21319
cf814e36f788
replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents:
21240
diff
changeset

58 
by (relation "less_than") (auto simp:nz_is_zero) 
19568  59 

60 
thm nz.simps 

61 
thm nz.induct 

62 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

63 
text {* Here comes McCarthy's 91function *} 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

64 

21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20536
diff
changeset

65 

21240
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

66 
function f91 :: "nat => nat" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

67 
where 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

68 
"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

69 
by pat_completeness auto 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

70 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

71 
(* Prove a lemma before attempting a termination proof *) 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

72 
lemma f91_estimate: 
24585  73 
assumes trm: "f91_dom n" 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

74 
shows "n < f91 n + 11" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

75 
using trm by induct auto 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

76 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

77 
termination 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

78 
proof 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

79 
let ?R = "measure (%x. 101  x)" 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

80 
show "wf ?R" .. 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

81 

be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

82 
fix n::nat assume "~ 100 < n" (* Inner call *) 
24585  83 
thus "(n + 11, n) : ?R" by simp 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

84 

21051
c49467a9c1e1
Switched function package to use the new package for inductive predicates.
krauss
parents:
20536
diff
changeset

85 
assume inner_trm: "f91_dom (n + 11)" (* Outer call *) 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

86 
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

87 
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

88 
qed 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

89 

28584  90 
text{* Now trivial (even though it does not belong here): *} 
91 
lemma "f91 n = (if 100 < n then n  10 else 91)" 

92 
by (induct n rule:f91.induct) auto 

19568  93 

24585  94 

22726  95 
subsection {* More general patterns *} 
19568  96 

22726  97 
subsubsection {* Overlapping patterns *} 
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

98 

19736  99 
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

100 
no automatic splitting takes place. But the following definition of 
19736  101 
gcd is ok, although patterns overlap: *} 
19568  102 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

103 
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

104 
where 
19568  105 
"gcd2 x 0 = x" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

106 
 "gcd2 0 y = y" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

107 
 "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

108 
else gcd2 (x  y) (Suc y))" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

109 

19568  110 
thm gcd2.simps 
111 
thm gcd2.induct 

112 

22726  113 
subsubsection {* Guards *} 
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

114 

48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

115 
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

116 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

117 
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

118 
where 
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

119 
"gcd3 x 0 = x" 
22492  120 
 "gcd3 0 y = y" 
121 
 "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y  x)" 

122 
 "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x  y) (Suc y)" 

19922  123 
apply (case_tac x, case_tac a, auto) 
124 
apply (case_tac ba, auto) 

19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

125 
done 
21240
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

126 
termination by lexicographic_order 
19782
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

127 

48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

128 
thm gcd3.simps 
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

129 
thm gcd3.induct 
48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

130 

48c4632e2c28
HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents:
19770
diff
changeset

131 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

132 
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

133 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

134 
function ev :: "nat \<Rightarrow> bool" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

135 
where 
19568  136 
"ev (2 * n) = True" 
22492  137 
 "ev (2 * n + 1) = False" 
19736  138 
proof   {* completeness is more difficult here \dots *} 
19922  139 
fix P :: bool 
140 
and x :: nat 

19568  141 
assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P" 
142 
and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P" 

143 
have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto 

144 
show "P" 

19736  145 
proof cases 
19568  146 
assume "x mod 2 = 0" 
147 
with divmod have "x = 2 * (x div 2)" by simp 

148 
with c1 show "P" . 

149 
next 

150 
assume "x mod 2 \<noteq> 0" 

151 
hence "x mod 2 = 1" by simp 

152 
with divmod have "x = 2 * (x div 2) + 1" by simp 

153 
with c2 show "P" . 

154 
qed 

23315  155 
qed presburger+  {* solve compatibility with presburger *} 
21240
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

156 
termination by lexicographic_order 
19568  157 

158 
thm ev.simps 

159 
thm ev.induct 

160 
thm ev.cases 

161 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

162 

22726  163 
subsection {* Mutual Recursion *} 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

164 

20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

165 
fun evn od :: "nat \<Rightarrow> bool" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

166 
where 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

167 
"evn 0 = True" 
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

168 
 "od 0 = False" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

169 
 "evn (Suc n) = od n" 
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20270
diff
changeset

170 
 "od (Suc n) = evn n" 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

171 

21240
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

172 
thm evn.simps 
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

173 
thm od.simps 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

174 

23817  175 
thm evn_od.induct 
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

176 
thm evn_od.termination 
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

177 

21240
8e75fb38522c
Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents:
21051
diff
changeset

178 

22726  179 
subsection {* Definitions in local contexts *} 
22618  180 

181 
locale my_monoid = 

182 
fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" 

183 
and un :: "'a" 

184 
assumes assoc: "opr (opr x y) z = opr x (opr y z)" 

185 
and lunit: "opr un x = x" 

186 
and runit: "opr x un = x" 

187 
begin 

188 

189 
fun foldR :: "'a list \<Rightarrow> 'a" 

190 
where 

191 
"foldR [] = un" 

192 
 "foldR (x#xs) = opr x (foldR xs)" 

193 

194 
fun foldL :: "'a list \<Rightarrow> 'a" 

195 
where 

196 
"foldL [] = un" 

197 
 "foldL [x] = x" 

198 
 "foldL (x#y#ys) = foldL (opr x y # ys)" 

199 

200 
thm foldL.simps 

201 

202 
lemma foldR_foldL: "foldR xs = foldL xs" 

203 
by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc) 

204 

205 
thm foldR_foldL 

206 

207 
end 

208 

209 
thm my_monoid.foldL.simps 

210 
thm my_monoid.foldR_foldL 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

211 

22726  212 
subsection {* Regression tests *} 
213 

214 
text {* The following examples mainly serve as tests for the 

215 
function package *} 

216 

217 
fun listlen :: "'a list \<Rightarrow> nat" 

218 
where 

219 
"listlen [] = 0" 

220 
 "listlen (x#xs) = Suc (listlen xs)" 

221 

222 
(* Context recursion *) 

223 

224 
fun f :: "nat \<Rightarrow> nat" 

225 
where 

226 
zero: "f 0 = 0" 

227 
 succ: "f (Suc n) = (if f n = 0 then 0 else f n)" 

228 

229 

230 
(* A combination of context and nested recursion *) 

231 
function h :: "nat \<Rightarrow> nat" 

232 
where 

233 
"h 0 = 0" 

234 
 "h (Suc n) = (if h n = 0 then h (h n) else h n)" 

235 
by pat_completeness auto 

236 

237 

238 
(* Context, but no recursive call: *) 

239 
fun i :: "nat \<Rightarrow> nat" 

240 
where 

241 
"i 0 = 0" 

242 
 "i (Suc n) = (if n = 0 then 0 else i n)" 

243 

244 

245 
(* Tupled nested recursion *) 

246 
fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat" 

247 
where 

248 
"fa 0 y = 0" 

249 
 "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)" 

250 

251 
(* Let *) 

252 
fun j :: "nat \<Rightarrow> nat" 

253 
where 

254 
"j 0 = 0" 

255 
 "j (Suc n) = (let u = n in Suc (j u))" 

256 

257 

258 
(* There were some problems with fresh names\<dots> *) 

259 
(* FIXME: tailrec? *) 

260 
function k :: "nat \<Rightarrow> nat" 

261 
where 

262 
"k x = (let a = x; b = x in k x)" 

263 
by pat_completeness auto 

264 

265 

266 
(* FIXME: tailrec? *) 

267 
function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)" 

268 
where 

269 
"f2 p = (let (x,y) = p in f2 (y,x))" 

270 
by pat_completeness auto 

271 

272 

273 
(* abbreviations *) 

274 
fun f3 :: "'a set \<Rightarrow> bool" 

275 
where 

276 
"f3 x = finite x" 

277 

278 

279 
(* Simple HigherOrder Recursion *) 

280 
datatype 'a tree = 

281 
Leaf 'a 

282 
 Branch "'a tree list" 

23117
e2744f32641e
updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents:
22726
diff
changeset

283 

25680  284 
lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)" 
22726  285 
by (induct l, auto) 
286 

23117
e2744f32641e
updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents:
22726
diff
changeset

287 
function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree" 
22726  288 
where 
289 
"treemap fn (Leaf n) = (Leaf (fn n))" 

290 
 "treemap fn (Branch l) = (Branch (map (treemap fn) l))" 

23117
e2744f32641e
updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents:
22726
diff
changeset

291 
by pat_completeness auto 
e2744f32641e
updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents:
22726
diff
changeset

292 
termination by (lexicographic_order simp:lem) 
e2744f32641e
updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents:
22726
diff
changeset

293 

e2744f32641e
updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents:
22726
diff
changeset

294 
declare lem[simp] 
22726  295 

296 
fun tinc :: "nat tree \<Rightarrow> nat tree" 

297 
where 

298 
"tinc (Leaf n) = Leaf (Suc n)" 

299 
 "tinc (Branch l) = Branch (map tinc l)" 

300 

301 

302 
(* Pattern matching on records *) 

303 
record point = 

304 
Xcoord :: int 

305 
Ycoord :: int 

306 

307 
function swp :: "point \<Rightarrow> point" 

308 
where 

309 
"swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>" 

310 
proof  

311 
fix P x 

312 
assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P" 

313 
thus "P" 

314 
by (cases x) 

315 
qed auto 

316 
termination by rule auto 

317 

318 

319 
(* The diagonal function *) 

320 
fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat" 

321 
where 

322 
"diag x True False = 1" 

323 
 "diag False y True = 2" 

324 
 "diag True False z = 3" 

325 
 "diag True True True = 4" 

326 
 "diag False False False = 5" 

327 

328 

329 
(* Many equations (quadratic blowup) *) 

330 
datatype DT = 

331 
A  B  C  D  E  F  G  H  I  J  K  L  M  N  P 

332 
 Q  R  S  T  U  V 

333 

334 
fun big :: "DT \<Rightarrow> nat" 

335 
where 

336 
"big A = 0" 

337 
 "big B = 0" 

338 
 "big C = 0" 

339 
 "big D = 0" 

340 
 "big E = 0" 

341 
 "big F = 0" 

342 
 "big G = 0" 

343 
 "big H = 0" 

344 
 "big I = 0" 

345 
 "big J = 0" 

346 
 "big K = 0" 

347 
 "big L = 0" 

348 
 "big M = 0" 

349 
 "big N = 0" 

350 
 "big P = 0" 

351 
 "big Q = 0" 

352 
 "big R = 0" 

353 
 "big S = 0" 

354 
 "big T = 0" 

355 
 "big U = 0" 

356 
 "big V = 0" 

357 

358 

359 
(* automatic pattern splitting *) 

360 
fun 

361 
f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool" 

362 
where 

363 
"f4 0 0 = True" 

25170  364 
 "f4 _ _ = False" 
22726  365 

19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19736
diff
changeset

366 

19736  367 
end 