(* Title: HOL/ex/Fundefs.thy Author: Alexander Krauss, TU Muenchen *) section {* Examples of function definitions *} theory Fundefs imports Main "~~/src/HOL/Library/Monad_Syntax" begin subsection {* Very basic *} fun fib :: "nat => nat" where "fib 0 = 1" | "fib (Suc 0) = 1" | "fib (Suc (Suc n)) = fib n + fib (Suc n)" text {* partial simp and induction rules: *} thm fib.psimps thm fib.pinduct text {* There is also a cases rule to distinguish cases along the definition *} thm fib.cases text {* total simp and induction rules: *} thm fib.simps thm fib.induct text {* elimination rules *} thm fib.elims subsection {* Currying *} fun add where "add 0 y = y" | "add (Suc x) y = Suc (add x y)" thm add.simps thm add.induct -- {* Note the curried induction predicate *} subsection {* Nested recursion *} function nz where "nz 0 = 0" | "nz (Suc x) = nz (nz x)" by pat_completeness auto lemma nz_is_zero: -- {* A lemma we need to prove termination *} assumes trm: "nz_dom x" shows "nz x = 0" using trm by induct (auto simp: nz.psimps) termination nz by (relation "less_than") (auto simp:nz_is_zero) thm nz.simps thm nz.induct text {* Here comes McCarthy's 91-function *} function f91 :: "nat => nat" where "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))" by pat_completeness auto (* Prove a lemma before attempting a termination proof *) lemma f91_estimate: assumes trm: "f91_dom n" shows "n < f91 n + 11" using trm by induct (auto simp: f91.psimps) termination proof let ?R = "measure (%x. 101 - x)" show "wf ?R" .. fix n::nat assume "~ 100 < n" (* Inner call *) thus "(n + 11, n) : ?R" by simp assume inner_trm: "f91_dom (n + 11)" (* Outer call *) with f91_estimate have "n + 11 < f91 (n + 11) + 11" . with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp qed text{* Now trivial (even though it does not belong here): *} lemma "f91 n = (if 100 < n then n - 10 else 91)" by (induct n rule:f91.induct) auto subsection {* More general patterns *} subsubsection {* Overlapping patterns *} text {* Currently, patterns must always be compatible with each other, since no automatic splitting takes place. But the following definition of gcd is ok, although patterns overlap: *} fun gcd2 :: "nat => nat => nat" where "gcd2 x 0 = x" | "gcd2 0 y = y" | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x) else gcd2 (x - y) (Suc y))" thm gcd2.simps thm gcd2.induct subsubsection {* Guards *} text {* We can reformulate the above example using guarded patterns *} function gcd3 :: "nat => nat => nat" where "gcd3 x 0 = x" | "gcd3 0 y = y" | "x < y ==> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" | "¬ x < y ==> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" apply (case_tac x, case_tac a, auto) apply (case_tac ba, auto) done termination by lexicographic_order thm gcd3.simps thm gcd3.induct text {* General patterns allow even strange definitions: *} function ev :: "nat => bool" where "ev (2 * n) = True" | "ev (2 * n + 1) = False" proof - -- {* completeness is more difficult here \dots *} fix P :: bool and x :: nat assume c1: "!!n. x = 2 * n ==> P" and c2: "!!n. x = 2 * n + 1 ==> P" have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto show "P" proof cases assume "x mod 2 = 0" with divmod have "x = 2 * (x div 2)" by simp with c1 show "P" . next assume "x mod 2 ≠ 0" hence "x mod 2 = 1" by simp with divmod have "x = 2 * (x div 2) + 1" by simp with c2 show "P" . qed qed presburger+ -- {* solve compatibility with presburger *} termination by lexicographic_order thm ev.simps thm ev.induct thm ev.cases subsection {* Mutual Recursion *} fun evn od :: "nat => bool" where "evn 0 = True" | "od 0 = False" | "evn (Suc n) = od n" | "od (Suc n) = evn n" thm evn.simps thm od.simps thm evn_od.induct thm evn_od.termination thm evn.elims thm od.elims subsection {* Definitions in local contexts *} locale my_monoid = fixes opr :: "'a => 'a => 'a" and un :: "'a" assumes assoc: "opr (opr x y) z = opr x (opr y z)" and lunit: "opr un x = x" and runit: "opr x un = x" begin fun foldR :: "'a list => 'a" where "foldR [] = un" | "foldR (x#xs) = opr x (foldR xs)" fun foldL :: "'a list => 'a" where "foldL [] = un" | "foldL [x] = x" | "foldL (x#y#ys) = foldL (opr x y # ys)" thm foldL.simps lemma foldR_foldL: "foldR xs = foldL xs" by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc) thm foldR_foldL end thm my_monoid.foldL.simps thm my_monoid.foldR_foldL subsection {* @{text fun_cases} *} subsubsection {* Predecessor *} fun pred :: "nat => nat" where "pred 0 = 0" | "pred (Suc n) = n" thm pred.elims lemma assumes "pred x = y" obtains "x = 0" "y = 0" | "n" where "x = Suc n" "y = n" by (fact pred.elims[OF assms]) text {* If the predecessor of a number is 0, that number must be 0 or 1. *} fun_cases pred0E[elim]: "pred n = 0" lemma "pred n = 0 ==> n = 0 ∨ n = Suc 0" by (erule pred0E) metis+ text {* Other expressions on the right-hand side also work, but whether the generated rule is useful depends on how well the simplifier can simplify it. This example works well: *} fun_cases pred42E[elim]: "pred n = 42" lemma "pred n = 42 ==> n = 43" by (erule pred42E) subsubsection {* List to option *} fun list_to_option :: "'a list => 'a option" where "list_to_option [x] = Some x" | "list_to_option _ = None" fun_cases list_to_option_NoneE: "list_to_option xs = None" and list_to_option_SomeE: "list_to_option xs = Some x" lemma "list_to_option xs = Some y ==> xs = [y]" by (erule list_to_option_SomeE) subsubsection {* Boolean Functions *} fun xor :: "bool => bool => bool" where "xor False False = False" | "xor True True = False" | "xor _ _ = True" thm xor.elims text {* @{text fun_cases} does not only recognise function equations, but also works with functions that return a boolean, e.g.: *} fun_cases xor_TrueE: "xor a b" and xor_FalseE: "¬xor a b" print_theorems subsubsection {* Many parameters *} fun sum4 :: "nat => nat => nat => nat => nat" where "sum4 a b c d = a + b + c + d" fun_cases sum40E: "sum4 a b c d = 0" lemma "sum4 a b c d = 0 ==> a = 0" by (erule sum40E) subsection {* Partial Function Definitions *} text {* Partial functions in the option monad: *} partial_function (option) collatz :: "nat => nat list option" where "collatz n = (if n ≤ 1 then Some [n] else if even n then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) } else do { ns \<leftarrow> collatz (3 * n + 1); Some (n # ns)})" declare collatz.simps[code] value "collatz 23" text {* Tail-recursive functions: *} partial_function (tailrec) fixpoint :: "('a => 'a) => 'a => 'a" where "fixpoint f x = (if f x = x then x else fixpoint f (f x))" subsection {* Regression tests *} text {* The following examples mainly serve as tests for the function package *} fun listlen :: "'a list => nat" where "listlen [] = 0" | "listlen (x#xs) = Suc (listlen xs)" (* Context recursion *) fun f :: "nat => nat" where zero: "f 0 = 0" | succ: "f (Suc n) = (if f n = 0 then 0 else f n)" (* A combination of context and nested recursion *) function h :: "nat => nat" where "h 0 = 0" | "h (Suc n) = (if h n = 0 then h (h n) else h n)" by pat_completeness auto (* Context, but no recursive call: *) fun i :: "nat => nat" where "i 0 = 0" | "i (Suc n) = (if n = 0 then 0 else i n)" (* Tupled nested recursion *) fun fa :: "nat => nat => nat" where "fa 0 y = 0" | "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)" (* Let *) fun j :: "nat => nat" where "j 0 = 0" | "j (Suc n) = (let u = n in Suc (j u))" (* There were some problems with fresh names… *) function k :: "nat => nat" where "k x = (let a = x; b = x in k x)" by pat_completeness auto function f2 :: "(nat × nat) => (nat × nat)" where "f2 p = (let (x,y) = p in f2 (y,x))" by pat_completeness auto (* abbreviations *) fun f3 :: "'a set => bool" where "f3 x = finite x" (* Simple Higher-Order Recursion *) datatype 'a tree = Leaf 'a | Branch "'a tree list" fun treemap :: "('a => 'a) => 'a tree => 'a tree" where "treemap fn (Leaf n) = (Leaf (fn n))" | "treemap fn (Branch l) = (Branch (map (treemap fn) l))" fun tinc :: "nat tree => nat tree" where "tinc (Leaf n) = Leaf (Suc n)" | "tinc (Branch l) = Branch (map tinc l)" fun testcase :: "'a tree => 'a list" where "testcase (Leaf a) = [a]" | "testcase (Branch x) = (let xs = concat (map testcase x); ys = concat (map testcase x) in xs @ ys)" (* Pattern matching on records *) record point = Xcoord :: int Ycoord :: int function swp :: "point => point" where "swp (| Xcoord = x, Ycoord = y |)), = (| Xcoord = y, Ycoord = x |))," proof - fix P x assume "!!xa y. x = (|Xcoord = xa, Ycoord = y|)), ==> P" thus "P" by (cases x) qed auto termination by rule auto (* The diagonal function *) fun diag :: "bool => bool => bool => nat" where "diag x True False = 1" | "diag False y True = 2" | "diag True False z = 3" | "diag True True True = 4" | "diag False False False = 5" (* Many equations (quadratic blowup) *) datatype DT = A | B | C | D | E | F | G | H | I | J | K | L | M | N | P | Q | R | S | T | U | V fun big :: "DT => nat" where "big A = 0" | "big B = 0" | "big C = 0" | "big D = 0" | "big E = 0" | "big F = 0" | "big G = 0" | "big H = 0" | "big I = 0" | "big J = 0" | "big K = 0" | "big L = 0" | "big M = 0" | "big N = 0" | "big P = 0" | "big Q = 0" | "big R = 0" | "big S = 0" | "big T = 0" | "big U = 0" | "big V = 0" (* automatic pattern splitting *) fun f4 :: "nat => nat => bool" where "f4 0 0 = True" | "f4 _ _ = False" (* polymorphic partial_function *) partial_function (option) f5 :: "'a list => 'a option" where "f5 x = f5 x" end