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