(* Title: HOL/ex/Fundefs.thy

Author: Alexander Krauss, TU Muenchen

*)

header {* Examples of function definitions *}

theory Fundefs

imports Parity "~~/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