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