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
```