src/HOL/ex/Fundefs.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 25680 909bfa21acc2
child 28584 58ac551ce1ce
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
krauss@19568
     1
(*  Title:      HOL/ex/Fundefs.thy
krauss@19568
     2
    ID:         $Id$
krauss@19568
     3
    Author:     Alexander Krauss, TU Muenchen
krauss@22726
     4
*)
krauss@19568
     5
krauss@22726
     6
header {* Examples of function definitions *}
krauss@19568
     7
krauss@19770
     8
theory Fundefs 
krauss@20528
     9
imports Main
krauss@19568
    10
begin
krauss@19568
    11
krauss@22726
    12
subsection {* Very basic *}
krauss@19568
    13
krauss@20523
    14
fun fib :: "nat \<Rightarrow> nat"
krauss@20523
    15
where
krauss@19568
    16
  "fib 0 = 1"
krauss@20523
    17
| "fib (Suc 0) = 1"
krauss@20523
    18
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
krauss@20523
    19
krauss@21319
    20
text {* partial simp and induction rules: *}
krauss@19568
    21
thm fib.psimps
krauss@20523
    22
thm fib.pinduct
krauss@19568
    23
wenzelm@19736
    24
text {* There is also a cases rule to distinguish cases along the definition *}
krauss@19568
    25
thm fib.cases
krauss@19568
    26
krauss@20523
    27
krauss@21319
    28
text {* total simp and induction rules: *}
krauss@19568
    29
thm fib.simps
krauss@19568
    30
thm fib.induct
krauss@19568
    31
krauss@22726
    32
subsection {* Currying *}
krauss@19568
    33
krauss@25170
    34
fun add
krauss@20523
    35
where
krauss@19568
    36
  "add 0 y = y"
krauss@20523
    37
| "add (Suc x) y = Suc (add x y)"
krauss@19568
    38
krauss@20523
    39
thm add.simps
wenzelm@19736
    40
thm add.induct -- {* Note the curried induction predicate *}
krauss@19568
    41
krauss@19568
    42
krauss@22726
    43
subsection {* Nested recursion *}
krauss@19568
    44
krauss@25170
    45
function nz 
krauss@20523
    46
where
krauss@19568
    47
  "nz 0 = 0"
krauss@20523
    48
| "nz (Suc x) = nz (nz x)"
krauss@21240
    49
by pat_completeness auto
krauss@20523
    50
wenzelm@19736
    51
lemma nz_is_zero: -- {* A lemma we need to prove termination *}
krauss@21051
    52
  assumes trm: "nz_dom x"
krauss@19568
    53
  shows "nz x = 0"
krauss@19568
    54
using trm
krauss@20523
    55
by induct auto
krauss@19568
    56
krauss@19568
    57
termination nz
krauss@21319
    58
  by (relation "less_than") (auto simp:nz_is_zero)
krauss@19568
    59
krauss@19568
    60
thm nz.simps
krauss@19568
    61
thm nz.induct
krauss@19568
    62
krauss@19770
    63
text {* Here comes McCarthy's 91-function *}
krauss@19770
    64
krauss@21051
    65
krauss@21240
    66
function f91 :: "nat => nat"
krauss@20523
    67
where
krauss@19770
    68
  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
krauss@21240
    69
by pat_completeness auto
krauss@20523
    70
krauss@19770
    71
(* Prove a lemma before attempting a termination proof *)
krauss@19770
    72
lemma f91_estimate: 
haftmann@24585
    73
  assumes trm: "f91_dom n"
krauss@19770
    74
  shows "n < f91 n + 11"
krauss@19770
    75
using trm by induct auto
krauss@19770
    76
krauss@19770
    77
termination
krauss@19770
    78
proof
krauss@19770
    79
  let ?R = "measure (%x. 101 - x)"
krauss@19770
    80
  show "wf ?R" ..
krauss@19770
    81
krauss@19770
    82
  fix n::nat assume "~ 100 < n" (* Inner call *)
haftmann@24585
    83
  thus "(n + 11, n) : ?R" by simp
krauss@19770
    84
krauss@21051
    85
  assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
krauss@19770
    86
  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
krauss@20270
    87
  with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
krauss@19770
    88
qed
krauss@19770
    89
krauss@19770
    90
krauss@19568
    91
haftmann@24585
    92
krauss@22726
    93
subsection {* More general patterns *}
krauss@19568
    94
krauss@22726
    95
subsubsection {* Overlapping patterns *}
krauss@19782
    96
wenzelm@19736
    97
text {* Currently, patterns must always be compatible with each other, since
krauss@20270
    98
no automatic splitting takes place. But the following definition of
wenzelm@19736
    99
gcd is ok, although patterns overlap: *}
krauss@19568
   100
krauss@20523
   101
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@20523
   102
where
krauss@19568
   103
  "gcd2 x 0 = x"
krauss@20523
   104
| "gcd2 0 y = y"
krauss@20523
   105
| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
krauss@20523
   106
                                    else gcd2 (x - y) (Suc y))"
krauss@20523
   107
krauss@19568
   108
thm gcd2.simps
krauss@19568
   109
thm gcd2.induct
krauss@19568
   110
krauss@22726
   111
subsubsection {* Guards *}
krauss@19782
   112
krauss@19782
   113
text {* We can reformulate the above example using guarded patterns *}
krauss@19782
   114
krauss@20523
   115
function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@20523
   116
where
krauss@19782
   117
  "gcd3 x 0 = x"
krauss@22492
   118
| "gcd3 0 y = y"
krauss@22492
   119
| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
krauss@22492
   120
| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
krauss@19922
   121
  apply (case_tac x, case_tac a, auto)
krauss@19922
   122
  apply (case_tac ba, auto)
krauss@19782
   123
  done
krauss@21240
   124
termination by lexicographic_order
krauss@19782
   125
krauss@19782
   126
thm gcd3.simps
krauss@19782
   127
thm gcd3.induct
krauss@19782
   128
krauss@19782
   129
krauss@20523
   130
text {* General patterns allow even strange definitions: *}
krauss@19782
   131
krauss@20523
   132
function ev :: "nat \<Rightarrow> bool"
krauss@20523
   133
where
krauss@19568
   134
  "ev (2 * n) = True"
krauss@22492
   135
| "ev (2 * n + 1) = False"
wenzelm@19736
   136
proof -  -- {* completeness is more difficult here \dots *}
krauss@19922
   137
  fix P :: bool
krauss@19922
   138
    and x :: nat
krauss@19568
   139
  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
krauss@19568
   140
    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
krauss@19568
   141
  have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
krauss@19568
   142
  show "P"
wenzelm@19736
   143
  proof cases
krauss@19568
   144
    assume "x mod 2 = 0"
krauss@19568
   145
    with divmod have "x = 2 * (x div 2)" by simp
krauss@19568
   146
    with c1 show "P" .
krauss@19568
   147
  next
krauss@19568
   148
    assume "x mod 2 \<noteq> 0"
krauss@19568
   149
    hence "x mod 2 = 1" by simp
krauss@19568
   150
    with divmod have "x = 2 * (x div 2) + 1" by simp
krauss@19568
   151
    with c2 show "P" .
krauss@19568
   152
  qed
chaieb@23315
   153
qed presburger+ -- {* solve compatibility with presburger *} 
krauss@21240
   154
termination by lexicographic_order
krauss@19568
   155
krauss@19568
   156
thm ev.simps
krauss@19568
   157
thm ev.induct
krauss@19568
   158
thm ev.cases
krauss@19568
   159
krauss@19770
   160
krauss@22726
   161
subsection {* Mutual Recursion *}
krauss@19770
   162
krauss@20523
   163
fun evn od :: "nat \<Rightarrow> bool"
krauss@20523
   164
where
krauss@19770
   165
  "evn 0 = True"
krauss@20523
   166
| "od 0 = False"
krauss@20523
   167
| "evn (Suc n) = od n"
krauss@20523
   168
| "od (Suc n) = evn n"
krauss@19770
   169
krauss@21240
   170
thm evn.simps
krauss@21240
   171
thm od.simps
krauss@19770
   172
krauss@23817
   173
thm evn_od.induct
krauss@19770
   174
thm evn_od.termination
krauss@19770
   175
krauss@21240
   176
krauss@22726
   177
subsection {* Definitions in local contexts *}
krauss@22618
   178
krauss@22618
   179
locale my_monoid = 
krauss@22618
   180
fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
krauss@22618
   181
  and un :: "'a"
krauss@22618
   182
assumes assoc: "opr (opr x y) z = opr x (opr y z)"
krauss@22618
   183
  and lunit: "opr un x = x"
krauss@22618
   184
  and runit: "opr x un = x"
krauss@22618
   185
begin
krauss@22618
   186
krauss@22618
   187
fun foldR :: "'a list \<Rightarrow> 'a"
krauss@22618
   188
where
krauss@22618
   189
  "foldR [] = un"
krauss@22618
   190
| "foldR (x#xs) = opr x (foldR xs)"
krauss@22618
   191
krauss@22618
   192
fun foldL :: "'a list \<Rightarrow> 'a"
krauss@22618
   193
where
krauss@22618
   194
  "foldL [] = un"
krauss@22618
   195
| "foldL [x] = x"
krauss@22618
   196
| "foldL (x#y#ys) = foldL (opr x y # ys)" 
krauss@22618
   197
krauss@22618
   198
thm foldL.simps
krauss@22618
   199
krauss@22618
   200
lemma foldR_foldL: "foldR xs = foldL xs"
krauss@22618
   201
by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
krauss@22618
   202
krauss@22618
   203
thm foldR_foldL
krauss@22618
   204
krauss@22618
   205
end
krauss@22618
   206
krauss@22618
   207
thm my_monoid.foldL.simps
krauss@22618
   208
thm my_monoid.foldR_foldL
krauss@19770
   209
krauss@22726
   210
subsection {* Regression tests *}
krauss@22726
   211
krauss@22726
   212
text {* The following examples mainly serve as tests for the 
krauss@22726
   213
  function package *}
krauss@22726
   214
krauss@22726
   215
fun listlen :: "'a list \<Rightarrow> nat"
krauss@22726
   216
where
krauss@22726
   217
  "listlen [] = 0"
krauss@22726
   218
| "listlen (x#xs) = Suc (listlen xs)"
krauss@22726
   219
krauss@22726
   220
(* Context recursion *)
krauss@22726
   221
krauss@22726
   222
fun f :: "nat \<Rightarrow> nat" 
krauss@22726
   223
where
krauss@22726
   224
  zero: "f 0 = 0"
krauss@22726
   225
| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
krauss@22726
   226
krauss@22726
   227
krauss@22726
   228
(* A combination of context and nested recursion *)
krauss@22726
   229
function h :: "nat \<Rightarrow> nat"
krauss@22726
   230
where
krauss@22726
   231
  "h 0 = 0"
krauss@22726
   232
| "h (Suc n) = (if h n = 0 then h (h n) else h n)"
krauss@22726
   233
  by pat_completeness auto
krauss@22726
   234
krauss@22726
   235
krauss@22726
   236
(* Context, but no recursive call: *)
krauss@22726
   237
fun i :: "nat \<Rightarrow> nat"
krauss@22726
   238
where
krauss@22726
   239
  "i 0 = 0"
krauss@22726
   240
| "i (Suc n) = (if n = 0 then 0 else i n)"
krauss@22726
   241
krauss@22726
   242
krauss@22726
   243
(* Tupled nested recursion *)
krauss@22726
   244
fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
krauss@22726
   245
where
krauss@22726
   246
  "fa 0 y = 0"
krauss@22726
   247
| "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
krauss@22726
   248
krauss@22726
   249
(* Let *)
krauss@22726
   250
fun j :: "nat \<Rightarrow> nat"
krauss@22726
   251
where
krauss@22726
   252
  "j 0 = 0"
krauss@22726
   253
| "j (Suc n) = (let u = n  in Suc (j u))"
krauss@22726
   254
krauss@22726
   255
krauss@22726
   256
(* There were some problems with fresh names\<dots> *)
krauss@22726
   257
(* FIXME: tailrec? *)
krauss@22726
   258
function  k :: "nat \<Rightarrow> nat"
krauss@22726
   259
where
krauss@22726
   260
  "k x = (let a = x; b = x in k x)"
krauss@22726
   261
  by pat_completeness auto
krauss@22726
   262
krauss@22726
   263
krauss@22726
   264
(* FIXME: tailrec? *)
krauss@22726
   265
function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
krauss@22726
   266
where
krauss@22726
   267
  "f2 p = (let (x,y) = p in f2 (y,x))"
krauss@22726
   268
  by pat_completeness auto
krauss@22726
   269
krauss@22726
   270
krauss@22726
   271
(* abbreviations *)
krauss@22726
   272
fun f3 :: "'a set \<Rightarrow> bool"
krauss@22726
   273
where
krauss@22726
   274
  "f3 x = finite x"
krauss@22726
   275
krauss@22726
   276
krauss@22726
   277
(* Simple Higher-Order Recursion *)
krauss@22726
   278
datatype 'a tree = 
krauss@22726
   279
  Leaf 'a 
krauss@22726
   280
  | Branch "'a tree list"
krauss@23117
   281
berghofe@25680
   282
lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"
krauss@22726
   283
by (induct l, auto)
krauss@22726
   284
krauss@23117
   285
function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
krauss@22726
   286
where
krauss@22726
   287
  "treemap fn (Leaf n) = (Leaf (fn n))"
krauss@22726
   288
| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
krauss@23117
   289
by pat_completeness auto
krauss@23117
   290
termination by (lexicographic_order simp:lem)
krauss@23117
   291
krauss@23117
   292
declare lem[simp]
krauss@22726
   293
krauss@22726
   294
fun tinc :: "nat tree \<Rightarrow> nat tree"
krauss@22726
   295
where
krauss@22726
   296
  "tinc (Leaf n) = Leaf (Suc n)"
krauss@22726
   297
| "tinc (Branch l) = Branch (map tinc l)"
krauss@22726
   298
krauss@22726
   299
krauss@22726
   300
(* Pattern matching on records *)
krauss@22726
   301
record point =
krauss@22726
   302
  Xcoord :: int
krauss@22726
   303
  Ycoord :: int
krauss@22726
   304
krauss@22726
   305
function swp :: "point \<Rightarrow> point"
krauss@22726
   306
where
krauss@22726
   307
  "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
krauss@22726
   308
proof -
krauss@22726
   309
  fix P x
krauss@22726
   310
  assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
krauss@22726
   311
  thus "P"
krauss@22726
   312
    by (cases x)
krauss@22726
   313
qed auto
krauss@22726
   314
termination by rule auto
krauss@22726
   315
krauss@22726
   316
krauss@22726
   317
(* The diagonal function *)
krauss@22726
   318
fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
krauss@22726
   319
where
krauss@22726
   320
  "diag x True False = 1"
krauss@22726
   321
| "diag False y True = 2"
krauss@22726
   322
| "diag True False z = 3"
krauss@22726
   323
| "diag True True True = 4"
krauss@22726
   324
| "diag False False False = 5"
krauss@22726
   325
krauss@22726
   326
krauss@22726
   327
(* Many equations (quadratic blowup) *)
krauss@22726
   328
datatype DT = 
krauss@22726
   329
  A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
krauss@22726
   330
| Q | R | S | T | U | V
krauss@22726
   331
krauss@22726
   332
fun big :: "DT \<Rightarrow> nat"
krauss@22726
   333
where
krauss@22726
   334
  "big A = 0" 
krauss@22726
   335
| "big B = 0" 
krauss@22726
   336
| "big C = 0" 
krauss@22726
   337
| "big D = 0" 
krauss@22726
   338
| "big E = 0" 
krauss@22726
   339
| "big F = 0" 
krauss@22726
   340
| "big G = 0" 
krauss@22726
   341
| "big H = 0" 
krauss@22726
   342
| "big I = 0" 
krauss@22726
   343
| "big J = 0" 
krauss@22726
   344
| "big K = 0" 
krauss@22726
   345
| "big L = 0" 
krauss@22726
   346
| "big M = 0" 
krauss@22726
   347
| "big N = 0" 
krauss@22726
   348
| "big P = 0" 
krauss@22726
   349
| "big Q = 0" 
krauss@22726
   350
| "big R = 0" 
krauss@22726
   351
| "big S = 0" 
krauss@22726
   352
| "big T = 0" 
krauss@22726
   353
| "big U = 0" 
krauss@22726
   354
| "big V = 0"
krauss@22726
   355
krauss@22726
   356
krauss@22726
   357
(* automatic pattern splitting *)
krauss@22726
   358
fun
krauss@22726
   359
  f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool" 
krauss@22726
   360
where
krauss@22726
   361
  "f4 0 0 = True"
krauss@25170
   362
| "f4 _ _ = False"
krauss@22726
   363
krauss@19770
   364
wenzelm@19736
   365
end