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