src/HOL/ex/Fundefs.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 28584 58ac551ce1ce
child 36269 fa30cbb455df
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/ex/Fundefs.thy
     2     ID:         $Id$
     3     Author:     Alexander Krauss, TU Muenchen
     4 *)
     5 
     6 header {* Examples of function definitions *}
     7 
     8 theory Fundefs 
     9 imports Main
    10 begin
    11 
    12 subsection {* Very basic *}
    13 
    14 fun fib :: "nat \<Rightarrow> nat"
    15 where
    16   "fib 0 = 1"
    17 | "fib (Suc 0) = 1"
    18 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
    19 
    20 text {* partial simp and induction rules: *}
    21 thm fib.psimps
    22 thm fib.pinduct
    23 
    24 text {* There is also a cases rule to distinguish cases along the definition *}
    25 thm fib.cases
    26 
    27 
    28 text {* total simp and induction rules: *}
    29 thm fib.simps
    30 thm fib.induct
    31 
    32 subsection {* Currying *}
    33 
    34 fun add
    35 where
    36   "add 0 y = y"
    37 | "add (Suc x) y = Suc (add x y)"
    38 
    39 thm add.simps
    40 thm add.induct -- {* Note the curried induction predicate *}
    41 
    42 
    43 subsection {* Nested recursion *}
    44 
    45 function nz 
    46 where
    47   "nz 0 = 0"
    48 | "nz (Suc x) = nz (nz x)"
    49 by pat_completeness auto
    50 
    51 lemma nz_is_zero: -- {* A lemma we need to prove termination *}
    52   assumes trm: "nz_dom x"
    53   shows "nz x = 0"
    54 using trm
    55 by induct auto
    56 
    57 termination nz
    58   by (relation "less_than") (auto simp:nz_is_zero)
    59 
    60 thm nz.simps
    61 thm nz.induct
    62 
    63 text {* Here comes McCarthy's 91-function *}
    64 
    65 
    66 function f91 :: "nat => nat"
    67 where
    68   "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
    69 by pat_completeness auto
    70 
    71 (* Prove a lemma before attempting a termination proof *)
    72 lemma f91_estimate: 
    73   assumes trm: "f91_dom n"
    74   shows "n < f91 n + 11"
    75 using trm by induct auto
    76 
    77 termination
    78 proof
    79   let ?R = "measure (%x. 101 - x)"
    80   show "wf ?R" ..
    81 
    82   fix n::nat assume "~ 100 < n" (* Inner call *)
    83   thus "(n + 11, n) : ?R" by simp
    84 
    85   assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
    86   with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
    87   with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
    88 qed
    89 
    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
    93 
    94 
    95 subsection {* More general patterns *}
    96 
    97 subsubsection {* Overlapping patterns *}
    98 
    99 text {* Currently, patterns must always be compatible with each other, since
   100 no automatic splitting takes place. But the following definition of
   101 gcd is ok, although patterns overlap: *}
   102 
   103 fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   104 where
   105   "gcd2 x 0 = x"
   106 | "gcd2 0 y = y"
   107 | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
   108                                     else gcd2 (x - y) (Suc y))"
   109 
   110 thm gcd2.simps
   111 thm gcd2.induct
   112 
   113 subsubsection {* Guards *}
   114 
   115 text {* We can reformulate the above example using guarded patterns *}
   116 
   117 function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   118 where
   119   "gcd3 x 0 = x"
   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)"
   123   apply (case_tac x, case_tac a, auto)
   124   apply (case_tac ba, auto)
   125   done
   126 termination by lexicographic_order
   127 
   128 thm gcd3.simps
   129 thm gcd3.induct
   130 
   131 
   132 text {* General patterns allow even strange definitions: *}
   133 
   134 function ev :: "nat \<Rightarrow> bool"
   135 where
   136   "ev (2 * n) = True"
   137 | "ev (2 * n + 1) = False"
   138 proof -  -- {* completeness is more difficult here \dots *}
   139   fix P :: bool
   140     and x :: nat
   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"
   145   proof cases
   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
   155 qed presburger+ -- {* solve compatibility with presburger *} 
   156 termination by lexicographic_order
   157 
   158 thm ev.simps
   159 thm ev.induct
   160 thm ev.cases
   161 
   162 
   163 subsection {* Mutual Recursion *}
   164 
   165 fun evn od :: "nat \<Rightarrow> bool"
   166 where
   167   "evn 0 = True"
   168 | "od 0 = False"
   169 | "evn (Suc n) = od n"
   170 | "od (Suc n) = evn n"
   171 
   172 thm evn.simps
   173 thm od.simps
   174 
   175 thm evn_od.induct
   176 thm evn_od.termination
   177 
   178 
   179 subsection {* Definitions in local contexts *}
   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
   211 
   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 Higher-Order Recursion *)
   280 datatype 'a tree = 
   281   Leaf 'a 
   282   | Branch "'a tree list"
   283 
   284 lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (list_size size l)"
   285 by (induct l, auto)
   286 
   287 function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
   288 where
   289   "treemap fn (Leaf n) = (Leaf (fn n))"
   290 | "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
   291 by pat_completeness auto
   292 termination by (lexicographic_order simp:lem)
   293 
   294 declare lem[simp]
   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"
   364 | "f4 _ _ = False"
   365 
   366 
   367 end