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