src/HOL/ex/Fundefs.thy
author krauss
Fri, 05 May 2006 18:39:16 +0200
changeset 19568 6fa47aad35e9
child 19583 c5fa77b03442
permissions -rw-r--r--
Added small example theory for new function package.
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"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    16
function 
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)"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    20
by pat_completeness (* shows that the patterns are complete *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    21
  auto (* shows that the patterns are compatible *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    22
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    23
(* we get partial simp and induction rules: *)
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    27
(* There is also a cases rule to distinguish cases along the definition *)
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    30
(* Now termination: *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    31
termination fib
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    32
  by (auto_term "less_than")    
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    40
consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    45
termination 
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    48
thm add.induct (* Note the curried induction predicate *)
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    60
lemma nz_is_zero: (* A lemma we need to prove termination *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    61
  assumes trm: "x \<in> nz.dom"
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    67
  apply (auto_term "less_than") (* Oops, it left us something to prove *)
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    76
(* Currently, patterns must always be compatible with each other, since
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    77
no automatich splitting takes place. But the following definition of
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    78
gcd is ok, although patterns overlap: *)
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
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    81
consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    82
function 
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    83
  "gcd2 x 0 = x"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    84
  "gcd2 0 y = y"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    85
  "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
    86
                                else gcd2 (x - y) (Suc y))"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    87
by pat_completeness auto
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    88
termination by (auto_term "measure (\<lambda>(x,y). x + y)")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    89
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    90
thm gcd2.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    91
thm gcd2.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    92
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    93
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    94
(* General patterns allow even strange definitions: *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    95
consts ev :: "nat \<Rightarrow> bool"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    96
function 
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    97
  "ev (2 * n) = True"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    98
  "ev (2 * n + 1) = False"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    99
proof - (* completeness is more difficult here. . . *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   100
  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   101
    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   102
  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
   103
  show "P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   104
  proof cases 
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   105
    assume "x mod 2 = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   106
    with divmod have "x = 2 * (x div 2)" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   107
    with c1 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   108
  next
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   109
    assume "x mod 2 \<noteq> 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   110
    hence "x mod 2 = 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   111
    with divmod have "x = 2 * (x div 2) + 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   112
    with c2 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   113
  qed
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   114
qed presburger+ (* solve compatibility with presburger *)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   115
termination by (auto_term "{}")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   116
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   117
thm ev.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   118
thm ev.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   119
thm ev.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   120
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   121
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   122
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   123
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   124
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   125
end