src/HOL/ex/Fundefs.thy
author krauss
Mon, 16 Jul 2007 21:16:16 +0200
changeset 23817 ee3ee9ea0d34
parent 23315 df3a7e9ebadb
child 24585 c359896d0f48
permissions -rw-r--r--
updated
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
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
     4
*)
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     5
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
     6
header {* Examples of function definitions *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     7
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
     8
theory Fundefs 
20528
4ade644022dd Removed debugging code imports...
krauss
parents: 20523
diff changeset
     9
imports Main
19568
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
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
    12
subsection {* Very basic *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    13
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    14
fun fib :: "nat \<Rightarrow> nat"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    15
where
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    16
  "fib 0 = 1"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    17
| "fib (Suc 0) = 1"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    18
| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    19
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21240
diff changeset
    20
text {* partial simp and induction rules: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    21
thm fib.psimps
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    22
thm fib.pinduct
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    23
19736
wenzelm
parents: 19583
diff changeset
    24
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
    25
thm fib.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    26
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    27
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21240
diff changeset
    28
text {* total simp and induction rules: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    29
thm fib.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    30
thm fib.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    31
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
    32
subsection {* Currying *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    33
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    34
fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    35
where
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    36
  "add 0 y = y"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    37
| "add (Suc x) y = Suc (add x y)"
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    38
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    39
thm add.simps
19736
wenzelm
parents: 19583
diff changeset
    40
thm add.induct -- {* Note the curried induction predicate *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    41
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    42
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
    43
subsection {* Nested recursion *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    44
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
    45
function nz :: "nat \<Rightarrow> nat"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    46
where
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    47
  "nz 0 = 0"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    48
| "nz (Suc x) = nz (nz x)"
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
    49
by pat_completeness auto
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    50
19736
wenzelm
parents: 19583
diff changeset
    51
lemma nz_is_zero: -- {* A lemma we need to prove termination *}
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20536
diff changeset
    52
  assumes trm: "nz_dom x"
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    53
  shows "nz x = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    54
using trm
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    55
by induct auto
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    56
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    57
termination nz
21319
cf814e36f788 replaced "auto_term" by the simpler method "relation", which does not try
krauss
parents: 21240
diff changeset
    58
  by (relation "less_than") (auto simp:nz_is_zero)
19568
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
thm nz.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    61
thm nz.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    62
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    63
text {* Here comes McCarthy's 91-function *}
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    64
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20536
diff changeset
    65
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
    66
function f91 :: "nat => nat"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    67
where
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    68
  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
    69
by pat_completeness auto
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
    70
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    71
(* Prove a lemma before attempting a termination proof *)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    72
lemma f91_estimate: 
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20536
diff changeset
    73
  assumes trm: "f91_dom n" 
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    74
  shows "n < f91 n + 11"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    75
using trm by induct auto
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    76
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    77
termination
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    78
proof
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    79
  let ?R = "measure (%x. 101 - x)"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    80
  show "wf ?R" ..
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    81
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    82
  fix n::nat assume "~ 100 < n" (* Inner call *)
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19922
diff changeset
    83
  thus "(n + 11, n) : ?R" by simp 
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    84
21051
c49467a9c1e1 Switched function package to use the new package for inductive predicates.
krauss
parents: 20536
diff changeset
    85
  assume inner_trm: "f91_dom (n + 11)" (* Outer call *)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    86
  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19922
diff changeset
    87
  with `~ 100 < n` show "(f91 (n + 11), n) : ?R" by simp 
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    88
qed
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    89
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    90
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    91
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
    92
subsection {* More general patterns *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    93
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
    94
subsubsection {* Overlapping patterns *}
19782
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
    95
19736
wenzelm
parents: 19583
diff changeset
    96
text {* Currently, patterns must always be compatible with each other, since
20270
3abe7dae681e Function package can now do automatic splits of overlapping datatype patterns
krauss
parents: 19922
diff changeset
    97
no automatic splitting takes place. But the following definition of
19736
wenzelm
parents: 19583
diff changeset
    98
gcd is ok, although patterns overlap: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    99
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   100
fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   101
where
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   102
  "gcd2 x 0 = x"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   103
| "gcd2 0 y = y"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   104
| "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   105
                                    else gcd2 (x - y) (Suc y))"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   106
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   107
thm gcd2.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   108
thm gcd2.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   109
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   110
subsubsection {* Guards *}
19782
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   111
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   112
text {* We can reformulate the above example using guarded patterns *}
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   113
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   114
function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   115
where
19782
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   116
  "gcd3 x 0 = x"
22492
43545e640877 Unified function syntax
krauss
parents: 22166
diff changeset
   117
| "gcd3 0 y = y"
43545e640877 Unified function syntax
krauss
parents: 22166
diff changeset
   118
| "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
43545e640877 Unified function syntax
krauss
parents: 22166
diff changeset
   119
| "\<not> x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (x - y) (Suc y)"
19922
984ae977f7aa Fixed name clash.
krauss
parents: 19782
diff changeset
   120
  apply (case_tac x, case_tac a, auto)
984ae977f7aa Fixed name clash.
krauss
parents: 19782
diff changeset
   121
  apply (case_tac ba, auto)
19782
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   122
  done
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
   123
termination by lexicographic_order
19782
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   124
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   125
thm gcd3.simps
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   126
thm gcd3.induct
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   127
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   128
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   129
text {* General patterns allow even strange definitions: *}
19782
48c4632e2c28 HOL/Tools/function_package: imporoved handling of guards, added an example
krauss
parents: 19770
diff changeset
   130
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   131
function ev :: "nat \<Rightarrow> bool"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   132
where
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   133
  "ev (2 * n) = True"
22492
43545e640877 Unified function syntax
krauss
parents: 22166
diff changeset
   134
| "ev (2 * n + 1) = False"
19736
wenzelm
parents: 19583
diff changeset
   135
proof -  -- {* completeness is more difficult here \dots *}
19922
984ae977f7aa Fixed name clash.
krauss
parents: 19782
diff changeset
   136
  fix P :: bool
984ae977f7aa Fixed name clash.
krauss
parents: 19782
diff changeset
   137
    and x :: nat
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   138
  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   139
    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   140
  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
   141
  show "P"
19736
wenzelm
parents: 19583
diff changeset
   142
  proof cases
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   143
    assume "x mod 2 = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   144
    with divmod have "x = 2 * (x div 2)" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   145
    with c1 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   146
  next
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   147
    assume "x mod 2 \<noteq> 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   148
    hence "x mod 2 = 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   149
    with divmod have "x = 2 * (x div 2) + 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   150
    with c2 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   151
  qed
23315
df3a7e9ebadb tuned Proof
chaieb
parents: 23117
diff changeset
   152
qed presburger+ -- {* solve compatibility with presburger *} 
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
   153
termination by lexicographic_order
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   154
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   155
thm ev.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   156
thm ev.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   157
thm ev.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   158
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   159
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   160
subsection {* Mutual Recursion *}
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   161
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   162
fun evn od :: "nat \<Rightarrow> bool"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   163
where
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   164
  "evn 0 = True"
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   165
| "od 0 = False"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   166
| "evn (Suc n) = od n"
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 20270
diff changeset
   167
| "od (Suc n) = evn n"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   168
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
   169
thm evn.simps
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
   170
thm od.simps
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   171
23817
ee3ee9ea0d34 updated
krauss
parents: 23315
diff changeset
   172
thm evn_od.induct
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   173
thm evn_od.termination
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   174
21240
8e75fb38522c Made "termination by lexicographic_order" the default for "fun" definitions.
krauss
parents: 21051
diff changeset
   175
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   176
subsection {* Definitions in local contexts *}
22618
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   177
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   178
locale my_monoid = 
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   179
fixes opr :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   180
  and un :: "'a"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   181
assumes assoc: "opr (opr x y) z = opr x (opr y z)"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   182
  and lunit: "opr un x = x"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   183
  and runit: "opr x un = x"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   184
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   185
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   186
context my_monoid
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   187
begin
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   188
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   189
fun foldR :: "'a list \<Rightarrow> 'a"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   190
where
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   191
  "foldR [] = un"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   192
| "foldR (x#xs) = opr x (foldR xs)"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   193
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   194
fun foldL :: "'a list \<Rightarrow> 'a"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   195
where
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   196
  "foldL [] = un"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   197
| "foldL [x] = x"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   198
| "foldL (x#y#ys) = foldL (opr x y # ys)" 
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   199
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   200
thm foldL.simps
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   201
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   202
lemma foldR_foldL: "foldR xs = foldL xs"
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   203
by (induct xs rule: foldL.induct) (auto simp:lunit runit assoc)
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   204
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   205
thm foldR_foldL
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   206
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   207
end
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   208
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   209
thm my_monoid.foldL.simps
e40957ccf0e9 added example for definitions in local contexts
krauss
parents: 22492
diff changeset
   210
thm my_monoid.foldR_foldL
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   211
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   212
subsection {* Regression tests *}
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   213
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   214
text {* The following examples mainly serve as tests for the 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   215
  function package *}
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   216
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   217
fun listlen :: "'a list \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   218
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   219
  "listlen [] = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   220
| "listlen (x#xs) = Suc (listlen xs)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   221
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   222
(* Context recursion *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   223
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   224
fun f :: "nat \<Rightarrow> nat" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   225
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   226
  zero: "f 0 = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   227
| succ: "f (Suc n) = (if f n = 0 then 0 else f n)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   228
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   229
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   230
(* A combination of context and nested recursion *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   231
function h :: "nat \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   232
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   233
  "h 0 = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   234
| "h (Suc n) = (if h n = 0 then h (h n) else h n)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   235
  by pat_completeness auto
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   236
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   237
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   238
(* Context, but no recursive call: *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   239
fun i :: "nat \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   240
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   241
  "i 0 = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   242
| "i (Suc n) = (if n = 0 then 0 else i n)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   243
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   244
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   245
(* Tupled nested recursion *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   246
fun fa :: "nat \<Rightarrow> nat \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   247
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   248
  "fa 0 y = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   249
| "fa (Suc n) y = (if fa n y = 0 then 0 else fa n y)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   250
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   251
(* Let *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   252
fun j :: "nat \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   253
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   254
  "j 0 = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   255
| "j (Suc n) = (let u = n  in Suc (j u))"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   256
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   257
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   258
(* There were some problems with fresh names\<dots> *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   259
(* FIXME: tailrec? *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   260
function  k :: "nat \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   261
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   262
  "k x = (let a = x; b = x in k x)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   263
  by pat_completeness auto
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   264
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   265
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   266
(* FIXME: tailrec? *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   267
function f2 :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   268
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   269
  "f2 p = (let (x,y) = p in f2 (y,x))"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   270
  by pat_completeness auto
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   271
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   272
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   273
(* abbreviations *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   274
fun f3 :: "'a set \<Rightarrow> bool"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   275
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   276
  "f3 x = finite x"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   277
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   278
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   279
(* Simple Higher-Order Recursion *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   280
datatype 'a tree = 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   281
  Leaf 'a 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   282
  | Branch "'a tree list"
23117
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   283
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   284
lemma lem:"x \<in> set l \<Longrightarrow> size x < Suc (tree_list_size l)"
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   285
by (induct l, auto)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   286
23117
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   287
function treemap :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   288
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   289
  "treemap fn (Leaf n) = (Leaf (fn n))"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   290
| "treemap fn (Branch l) = (Branch (map (treemap fn) l))"
23117
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   291
by pat_completeness auto
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   292
termination by (lexicographic_order simp:lem)
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   293
e2744f32641e updated examples to include an instance of (lexicographic_order simp:...)
krauss
parents: 22726
diff changeset
   294
declare lem[simp]
22726
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   295
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   296
fun tinc :: "nat tree \<Rightarrow> nat tree"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   297
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   298
  "tinc (Leaf n) = Leaf (Suc n)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   299
| "tinc (Branch l) = Branch (map tinc l)"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   300
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   301
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   302
(* Pattern matching on records *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   303
record point =
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   304
  Xcoord :: int
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   305
  Ycoord :: int
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   306
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   307
function swp :: "point \<Rightarrow> point"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   308
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   309
  "swp \<lparr> Xcoord = x, Ycoord = y \<rparr> = \<lparr> Xcoord = y, Ycoord = x \<rparr>"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   310
proof -
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   311
  fix P x
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   312
  assume "\<And>xa y. x = \<lparr>Xcoord = xa, Ycoord = y\<rparr> \<Longrightarrow> P"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   313
  thus "P"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   314
    by (cases x)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   315
qed auto
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   316
termination by rule auto
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   317
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   318
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   319
(* The diagonal function *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   320
fun diag :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   321
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   322
  "diag x True False = 1"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   323
| "diag False y True = 2"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   324
| "diag True False z = 3"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   325
| "diag True True True = 4"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   326
| "diag False False False = 5"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   327
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   328
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   329
(* Many equations (quadratic blowup) *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   330
datatype DT = 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   331
  A | B | C | D | E | F | G | H | I | J | K | L | M | N | P
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   332
| Q | R | S | T | U | V
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   333
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   334
fun big :: "DT \<Rightarrow> nat"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   335
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   336
  "big A = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   337
| "big B = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   338
| "big C = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   339
| "big D = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   340
| "big E = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   341
| "big F = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   342
| "big G = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   343
| "big H = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   344
| "big I = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   345
| "big J = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   346
| "big K = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   347
| "big L = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   348
| "big M = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   349
| "big N = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   350
| "big P = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   351
| "big Q = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   352
| "big R = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   353
| "big S = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   354
| "big T = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   355
| "big U = 0" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   356
| "big V = 0"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   357
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   358
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   359
(* automatic pattern splitting *)
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   360
fun
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   361
  f4 :: "nat \<Rightarrow> nat \<Rightarrow> bool" 
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   362
where
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   363
  "f4 0 0 = True"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   364
| "f4 x y = False"
11e01dc78377 proper header, added regression tests
krauss
parents: 22618
diff changeset
   365
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   366
19736
wenzelm
parents: 19583
diff changeset
   367
end