src/HOL/ex/Fundefs.thy
author krauss
Mon, 05 Jun 2006 14:26:07 +0200
changeset 19770 be5c23ebe1eb
parent 19736 d8d0f8f51d69
child 19782 48c4632e2c28
permissions -rw-r--r--
HOL/Tools/function_package: Added support for mutual recursive definitions.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     1
(*  Title:      HOL/ex/Fundefs.thy
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     2
    ID:         $Id$
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     3
    Author:     Alexander Krauss, TU Muenchen
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     4
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     5
Examples of function definitions using the new "function" package.
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     6
*)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     7
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
     8
theory Fundefs 
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
     9
imports Main
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    10
begin
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    11
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    12
section {* Very basic *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    13
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    14
consts fib :: "nat \<Rightarrow> nat"
19736
wenzelm
parents: 19583
diff changeset
    15
function
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    16
  "fib 0 = 1"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    17
  "fib (Suc 0) = 1"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    18
  "fib (Suc (Suc n)) = fib n + fib (Suc n)"
19736
wenzelm
parents: 19583
diff changeset
    19
by pat_completeness  -- {* shows that the patterns are complete *}
wenzelm
parents: 19583
diff changeset
    20
  auto  -- {* shows that the patterns are compatible *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    21
19736
wenzelm
parents: 19583
diff changeset
    22
text {* we get partial simp and induction rules: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    23
thm fib.psimps
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    24
thm pinduct
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    25
19736
wenzelm
parents: 19583
diff changeset
    26
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
    27
thm fib.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    28
19736
wenzelm
parents: 19583
diff changeset
    29
text {* Now termination: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    30
termination fib
19736
wenzelm
parents: 19583
diff changeset
    31
  by (auto_term "less_than")
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    32
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    33
thm fib.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    34
thm fib.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    35
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    36
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    37
section {* Currying *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    38
19736
wenzelm
parents: 19583
diff changeset
    39
consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    40
function
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    41
  "add 0 y = y"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    42
  "add (Suc x) y = Suc (add x y)"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    43
thm add_rel.cases
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    44
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    45
by pat_completeness auto
19736
wenzelm
parents: 19583
diff changeset
    46
termination
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    47
  by (auto_term "measure fst")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    48
19736
wenzelm
parents: 19583
diff changeset
    49
thm add.induct -- {* Note the curried induction predicate *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    50
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    51
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    52
section {* Nested recursion *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    53
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    54
consts nz :: "nat \<Rightarrow> nat"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    55
function
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    56
  "nz 0 = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    57
  "nz (Suc x) = nz (nz x)"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    58
by pat_completeness auto
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    59
19736
wenzelm
parents: 19583
diff changeset
    60
lemma nz_is_zero: -- {* A lemma we need to prove termination *}
19583
c5fa77b03442 function-package: Changed record usage to make sml/nj happy...
krauss
parents: 19568
diff changeset
    61
  assumes trm: "x \<in> nz_dom"
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    62
  shows "nz x = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    63
using trm
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    64
apply induct 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    65
apply auto
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    66
done
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    67
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    68
termination nz
19736
wenzelm
parents: 19583
diff changeset
    69
  apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    70
  by (auto simp:nz_is_zero)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    71
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    72
thm nz.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    73
thm nz.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
    74
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    75
text {* Here comes McCarthy's 91-function *}
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
consts f91 :: "nat => nat"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    78
function 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    79
  "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    80
by pat_completeness auto
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
(* Prove a lemma before attempting a termination proof *)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    83
lemma f91_estimate: 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    84
  assumes trm: "n : f91_dom" 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    85
  shows "n < f91 n + 11"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    86
using trm by induct auto
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    87
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    88
(* Now go for termination *)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    89
termination
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    90
proof
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    91
  let ?R = "measure (%x. 101 - x)"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    92
  show "wf ?R" ..
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    93
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    94
  fix n::nat assume "~ 100 < n" (* Inner call *)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    95
  thus "(n + 11, n) : ?R"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    96
    by simp arith
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    97
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    98
  assume inner_trm: "n + 11 : f91_dom" (* Outer call *)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
    99
  with f91_estimate have "n + 11 < f91 (n + 11) + 11" .
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   100
  with `~ 100 < n` show "(f91 (n + 11), n) : ?R"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   101
    by simp arith
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   102
qed
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   103
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   104
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   105
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   106
section {* More general patterns *}
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   107
19736
wenzelm
parents: 19583
diff changeset
   108
text {* Currently, patterns must always be compatible with each other, since
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   109
no automatich splitting takes place. But the following definition of
19736
wenzelm
parents: 19583
diff changeset
   110
gcd is ok, although patterns overlap: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   111
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   112
consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
19736
wenzelm
parents: 19583
diff changeset
   113
function
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   114
  "gcd2 x 0 = x"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   115
  "gcd2 0 y = y"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   116
  "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   117
                                else gcd2 (x - y) (Suc y))"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   118
by pat_completeness auto
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   119
termination 
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   120
  by (auto_term "measure (\<lambda>(x,y). x + y)")
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   121
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   122
thm gcd2.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   123
thm gcd2.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   124
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   125
19736
wenzelm
parents: 19583
diff changeset
   126
text {* General patterns allow even strange definitions: *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   127
consts ev :: "nat \<Rightarrow> bool"
19736
wenzelm
parents: 19583
diff changeset
   128
function
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   129
  "ev (2 * n) = True"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   130
  "ev (2 * n + 1) = False"
19736
wenzelm
parents: 19583
diff changeset
   131
proof -  -- {* completeness is more difficult here \dots *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   132
  assume c1: "\<And>n. x = 2 * n \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   133
    and c2: "\<And>n. x = 2 * n + 1 \<Longrightarrow> P"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   134
  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
   135
  show "P"
19736
wenzelm
parents: 19583
diff changeset
   136
  proof cases
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   137
    assume "x mod 2 = 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   138
    with divmod have "x = 2 * (x div 2)" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   139
    with c1 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   140
  next
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   141
    assume "x mod 2 \<noteq> 0"
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   142
    hence "x mod 2 = 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   143
    with divmod have "x = 2 * (x div 2) + 1" by simp
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   144
    with c2 show "P" .
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   145
  qed
19736
wenzelm
parents: 19583
diff changeset
   146
qed presburger+   -- {* solve compatibility with presburger *}
19568
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   147
termination by (auto_term "{}")
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   148
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   149
thm ev.simps
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   150
thm ev.induct
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   151
thm ev.cases
6fa47aad35e9 Added small example theory for new function package.
krauss
parents:
diff changeset
   152
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   153
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   154
section {* Mutual Recursion *}
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   155
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   156
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   157
consts
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   158
  evn :: "nat \<Rightarrow> bool"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   159
  od :: "nat \<Rightarrow> bool"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   160
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   161
function
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   162
  "evn 0 = True"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   163
  "evn (Suc n) = od n"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   164
and
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   165
  "od 0 = False"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   166
  "od (Suc n) = evn n"
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   167
  by pat_completeness auto
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   168
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   169
thm evn.psimps
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   170
thm od.psimps
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   171
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   172
thm evn_od.pinduct
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
thm evn_od.domintros
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   175
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   176
termination
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   177
  by (auto_term "measure (sum_case (%n. n) (%n. n))")
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   178
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   179
thm evn.simps
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   180
thm od.simps
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   181
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents: 19736
diff changeset
   182
19736
wenzelm
parents: 19583
diff changeset
   183
end