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