src/HOL/ex/Fundefs.thy
author wenzelm
Sat, 27 May 2006 17:42:02 +0200
changeset 19736 d8d0f8f51d69
parent 19583 c5fa77b03442
child 19770 be5c23ebe1eb
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     1
(*  Title:      HOL/ex/Fundefs.thy
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     2
    ID:         $Id$
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     3
    Author:     Alexander Krauss, TU Muenchen
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     4
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     5
Examples of function definitions using the new "function" package.
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     6
*)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     7
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     8
theory Fundefs
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     9
imports Main
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    10
begin
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    11
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    12
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    13
section {* Very basic *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    14
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    15
consts fib :: "nat \<Rightarrow> nat"
19736
wenzelm
parents: 19583
diff changeset
    16
function
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    17
  "fib 0 = 1"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    18
  "fib (Suc 0) = 1"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    19
  "fib (Suc (Suc n)) = fib n + fib (Suc n)"
19736
wenzelm
parents: 19583
diff changeset
    20
by pat_completeness  -- {* shows that the patterns are complete *}
wenzelm
parents: 19583
diff changeset
    21
  auto  -- {* shows that the patterns are compatible *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    22
19736
wenzelm
parents: 19583
diff changeset
    23
text {* we get partial simp and induction rules: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    24
thm fib.psimps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    25
thm fib.pinduct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    26
19736
wenzelm
parents: 19583
diff changeset
    27
text {* There is also a cases rule to distinguish cases along the definition *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    28
thm fib.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    29
19736
wenzelm
parents: 19583
diff changeset
    30
text {* Now termination: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    31
termination fib
19736
wenzelm
parents: 19583
diff changeset
    32
  by (auto_term "less_than")
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    33
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    34
thm fib.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    35
thm fib.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    36
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    37
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    38
section {* Currying *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    39
19736
wenzelm
parents: 19583
diff changeset
    40
consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    41
function
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    42
  "add 0 y = y"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    43
  "add (Suc x) y = Suc (add x y)"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    44
by pat_completeness auto
19736
wenzelm
parents: 19583
diff changeset
    45
termination
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    46
  by (auto_term "measure fst")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    47
19736
wenzelm
parents: 19583
diff changeset
    48
thm add.induct -- {* Note the curried induction predicate *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    49
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    50
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    51
section {* Nested recursion *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    52
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    53
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    54
consts nz :: "nat \<Rightarrow> nat"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    55
function
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    56
  "nz 0 = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    57
  "nz (Suc x) = nz (nz x)"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    58
by pat_completeness auto
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    59
19736
wenzelm
parents: 19583
diff changeset
    60
lemma nz_is_zero: -- {* A lemma we need to prove termination *}
19583
c5fa77b03442 function-package: Changed record usage to make sml/nj happy...
krauss
parents: 19568
diff changeset
    61
  assumes trm: "x \<in> nz_dom"
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    62
  shows "nz x = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    63
using trm
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    64
by induct auto
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    65
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    66
termination nz
19736
wenzelm
parents: 19583
diff changeset
    67
  apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    68
  by (auto simp:nz_is_zero)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    69
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    70
thm nz.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    71
thm nz.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    72
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    73
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    74
section {* More general patterns *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    75
19736
wenzelm
parents: 19583
diff changeset
    76
text {* Currently, patterns must always be compatible with each other, since
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    77
no automatich splitting takes place. But the following definition of
19736
wenzelm
parents: 19583
diff changeset
    78
gcd is ok, although patterns overlap: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    79
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    80
consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
19736
wenzelm
parents: 19583
diff changeset
    81
function
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    82
  "gcd2 x 0 = x"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    83
  "gcd2 0 y = y"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    84
  "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    85
                                else gcd2 (x - y) (Suc y))"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    86
by pat_completeness auto
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    87
termination by (auto_term "measure (\<lambda>(x,y). x + y)")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    88
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    89
thm gcd2.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    90
thm gcd2.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    91
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    92
19736
wenzelm
parents: 19583
diff changeset
    93
text {* General patterns allow even strange definitions: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    94
consts ev :: "nat \<Rightarrow> bool"
19736
wenzelm
parents: 19583
diff changeset
    95
function
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    96
  "ev (2 * n) = True"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    97
  "ev (2 * n + 1) = False"
19736
wenzelm
parents: 19583
diff changeset
    98
proof -  -- {* completeness is more difficult here \dots *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    99
  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   100
    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   101
  have divmod: "x = 2 * (x div 2) + (x mod 2)" by auto
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   102
  show "P"
19736
wenzelm
parents: 19583
diff changeset
   103
  proof cases
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   104
    assume "x mod 2 = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   105
    with divmod have "x = 2 * (x div 2)" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   106
    with c1 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   107
  next
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   108
    assume "x mod 2 \<noteq> 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   109
    hence "x mod 2 = 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   110
    with divmod have "x = 2 * (x div 2) + 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   111
    with c2 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   112
  qed
19736
wenzelm
parents: 19583
diff changeset
   113
qed presburger+   -- {* solve compatibility with presburger *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   114
termination by (auto_term "{}")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   115
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   116
thm ev.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   117
thm ev.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   118
thm ev.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   119
19736
wenzelm
parents: 19583
diff changeset
   120
end