Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Functions.thy Sprache: Isabelle

Original von: Isabelle^©

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

section \<open>Examples of function definitions\<close>

theory Functions
imports Main "HOL-Library.Monad_Syntax"
begin

subsection \<open>Very basic\<close>

fun fib :: "nat \ nat"
where
  "fib 0 = 1"
| "fib (Suc 0) = 1"
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"

text \<open>Partial simp and induction rules:\<close>
thm fib.psimps
thm fib.pinduct

text \<open>There is also a cases rule to distinguish cases along the definition:\<close>
thm fib.cases

text \<open>Total simp and induction rules:\<close>
thm fib.simps
thm fib.induct

text \<open>Elimination rules:\<close>
thm fib.elims

subsection \<open>Currying\<close>

fun add
where
  "add 0 y = y"
| "add (Suc x) y = Suc (add x y)"

thm add.simps
thm add.induct  \<comment> \<open>Note the curried induction predicate\<close>

subsection \<open>Nested recursion\<close>

function nz
where
  "nz 0 = 0"
| "nz (Suc x) = nz (nz x)"
by pat_completeness auto

lemma nz_is_zero:  \<comment> \<open>A lemma we need to prove termination\<close>
  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 \<open>Here comes McCarthy's 91-function\<close>

function f91 :: "nat \ nat"
where
  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
by pat_completeness auto

text \<open>Prove a lemma before attempting a termination proof:\<close>
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)"  \<comment> \<open>Outer call\<close>
  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
  with \<open>\<not> 100 < n\<close> show "(f91 (n + 11), n) \<in> ?R" by simp
qed

text \<open>Now trivial (even though it does not belong here):\<close>
lemma "f91 n = (if 100 < n then n - 10 else 91)"
  by (induct n rule: f91.induct) auto

subsubsection \<open>Here comes Takeuchi's function\<close>

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 \<open>More general patterns\<close>

subsubsection \<open>Overlapping patterns\<close>

text \<open>
  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:
\<close>

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 \<open>Guards\<close>

text \<open>We can reformulate the above example using guarded patterns:\<close>

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 \<open>General patterns allow even strange definitions:\<close>

function ev :: "nat \ bool"
where
  "ev (2 * n) = True"
| "ev (2 * n + 1) = False"
proof -  \<comment> \<open>completeness is more difficult here \dots\<close>
  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+  \<comment> \<open>solve compatibility with presburger\<close>
termination by lexicographic_order

thm ev.simps
thm ev.induct
thm ev.cases

subsection \<open>Mutual Recursion\<close>

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 \<open>Definitions in local contexts\<close>

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 \<open>\<open>fun_cases\<close>\<close>

subsubsection \<open>Predecessor\<close>

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 \<open>If the predecessor of a number is 0, that number must be 0 or 1.\<close>

fun_cases pred0E[elim]: "pred n = 0"

lemma "pred n = 0 \ n = 0 \ n = Suc 0"
  by (erule pred0E) metis+

text \<open>
  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:
\<close>

fun_cases pred42E[elim]: "pred n = 42"

lemma "pred n = 42 \ n = 43"
  by (erule pred42E)

subsubsection \<open>List to option\<close>

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 \<open>Boolean Functions\<close>

fun xor :: "bool \ bool \ bool"
where
  "xor False False = False"
| "xor True True = False"
| "xor _ _ = True"

thm xor.elims

text \<open>
  \<open>fun_cases\<close> does not only recognise function equations, but also works with
  functions that return a boolean, e.g.:
\<close>

fun_cases xor_TrueE: "xor a b" and xor_FalseE: "\xor a b"
print_theorems

subsubsection \<open>Many parameters\<close>

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 \<open>Partial Function Definitions\<close>

text \<open>Partial functions in the option monad:\<close>

partial_function (option)
  collatz :: "nat \ nat list option"
where
  "collatz n =
    (if n \<le> 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 \<open>Tail-recursive functions:\<close>

partial_function (tailrec) fixpoint :: "('a \ 'a) \ 'a \ 'a"
where
  "fixpoint f x = (if f x = x then x else fixpoint f (f x))"

subsection \<open>Regression tests\<close>

text \<open>
  The following examples mainly serve as tests for the
  function package.
\<close>

fun listlen :: "'a list \ nat"
where
  "listlen [] = 0"
| "listlen (x#xs) = Suc (listlen xs)"

subsubsection \<open>Context recursion\<close>

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

subsubsection \<open>A combination of context and nested recursion\<close>

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 \<open>Context, but no recursive call\<close>

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

subsubsection \<open>Tupled nested recursion\<close>

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 \<open>Let\<close>

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

text \<open>There were some problems with fresh names \dots\<close>
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 \<open>Abbreviations\<close>

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

subsubsection \<open>Simple Higher-Order Recursion\<close>

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 \<open>Pattern matching on records\<close>

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 \<open>The diagonal function\<close>

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 \<open>Many equations (quadratic blowup)\<close>

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 \<open>Automatic pattern splitting\<close>

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

subsubsection \<open>Polymorphic partial-function\<close>

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

end

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.