Theory Fundefs

theory Fundefs
imports Monad_Syntax
(*  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 ‹‹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)"

(* 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