(*  Title:      HOL/ex/Functions.thy
    Author:     Alexander Krauss, TU Muenchen
*)

section ‹Examples of function definitions›

theory Functions
imports Main "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


subsubsection ‹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

text ‹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›
  then show "(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


subsubsection ‹Here comes Takeuchi's function›

definition tak_m1 where "tak_m1 = (λ(x,y,z). if x ≤ y then 0 else 1)"
definition tak_m2 where "tak_m2 = (λ(x,y,z). nat (Max {x, y, z} - Min {x, y, z}))"
definition tak_m3 where "tak_m3 = (λ(x,y,z). nat (x - Min {x, y, z}))"

function tak :: "int → int → int → int" where
  "tak x y z = (if x ≤ y then y else tak (tak (x-1) y z) (tak (y-1) z x) (tak (z-1) x y))"
  by auto

lemma tak_pcorrect:
  "tak_dom (x, y, z) ==> tak x y z = (if x ≤ y then y else if y ≤ z then z else x)"
  by (induction x y z rule: tak.pinduct) (auto simp: tak.psimps)

termination
  by (relation "tak_m1 <*mlex*> tak_m2 <*mlex*> tak_m3 <*mlex*> {}")
     (auto simp: mlex_iff wf_mlex tak_pcorrect tak_m1_def tak_m2_def tak_m3_def min_def max_def)

theorem tak_correct: "tak x y z = (if x ≤ y then y else if y ≤ z then z else x)"
  by (induction x y z rule: tak.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"
| "gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)" if "x < y"
| "gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)" if "¬ x < 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
  fix 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 "x mod 2 = 0")
    case True
    with divmod have "x = 2 * (x div 2)" by simp
    with c1 show "P" .
  next
    case False
    then have "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 ‹‹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 ‹
 ‹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 ← collatz (n div 2); Some (n # ns) }
       else do { ns ← 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)"


subsubsection ‹Context recursion›

fun f :: "nat → nat"
where
  zero: "f 0 = 0"
| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"


subsubsection ‹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


subsubsection ‹Context, but no recursive call›

fun i :: "nat → nat"
where
  "i 0 = 0"
| "i (Suc n) = (if n = 0 then 0 else i n)"


subsubsection ‹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)"


subsubsection ‹Let›

fun j :: "nat → nat"
where
  "j 0 = 0"
| "j (Suc n) = (let u = n in Suc (j u))"


text ‹There were some problems with fresh names \dots›
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


subsubsection ‹Abbreviations›

fun f3 :: "'a set → bool"
where
  "f3 x = finite x"


subsubsection ‹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)"


subsubsection ‹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"
  then show P by (cases x)
qed auto
termination by rule auto


subsubsection ‹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"


subsubsection ‹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"


subsubsection ‹Automatic pattern splitting›

fun f4 :: "nat → nat → bool"
where
  "f4 0 0 = True"
| "f4 _ _ = False"


subsubsection ‹Polymorphic partial-function›

partial_function (option) f5 :: "'a list → 'a option"
where
  "f5 x = f5 x"

end