src/HOL/Tools/Function/mutual.ML
author wenzelm
Sun, 31 May 2015 00:16:26 +0200
changeset 60321 42079156c5aa
parent 59859 f9d1442c70f3
child 60643 9173467ec5b6
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31775
2b04504fcb69 uniformly capitialized names for subdirectories
haftmann
parents: 30906
diff changeset
     1
(*  Title:      HOL/Tools/Function/mutual.ML
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     2
    Author:     Alexander Krauss, TU Muenchen
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     3
41114
f9ae7c2abf7e tuned headers
krauss
parents: 40317
diff changeset
     4
Mutual recursive function definitions.
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     5
*)
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     6
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
     7
signature FUNCTION_MUTUAL =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
     8
sig
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
     9
  val prepare_function_mutual : Function_Common.function_config
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    10
    -> string (* defname *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    11
    -> ((string * typ) * mixfix) list
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    12
    -> term list
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    13
    -> local_theory
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    14
    -> ((thm (* goalstate *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    15
        * (thm -> Function_Common.function_result) (* proof continuation *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    16
       ) * local_theory)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    17
end
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    18
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
    19
structure Function_Mutual: FUNCTION_MUTUAL =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    20
struct
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    21
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
    22
open Function_Lib
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
    23
open Function_Common
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    24
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    25
type qgar = string * (string * typ) list * term list * term list * term
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    26
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    27
datatype mutual_part = MutualPart of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    28
 {i : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    29
  i' : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    30
  fvar : string * typ,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    31
  cargTs: typ list,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    32
  f_def: term,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    33
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    34
  f: term option,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    35
  f_defthm : thm option}
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    36
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    37
datatype mutual_info = Mutual of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    38
 {n : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    39
  n' : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    40
  fsum_var : string * typ,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    41
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    42
  ST: typ,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    43
  RST: typ,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    44
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    45
  parts: mutual_part list,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    46
  fqgars: qgar list,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    47
  qglrs: ((string * typ) list * term list * term * term) list,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    48
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    49
  fsum : term option}
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    50
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    51
fun mutual_induct_Pnames n =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    52
  if n < 5 then fst (chop n ["P","Q","R","S"])
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    53
  else map (fn i => "P" ^ string_of_int i) (1 upto n)
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    54
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    55
fun get_part fname =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    56
  the o find_first (fn (MutualPart {fvar=(n,_), ...}) => n = fname)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    57
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    58
(* FIXME *)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    59
fun mk_prod_abs e (t1, t2) =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    60
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    61
    val bTs = rev (map snd e)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    62
    val T1 = fastype_of1 (bTs, t1)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    63
    val T2 = fastype_of1 (bTs, t2)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    64
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    65
    HOLogic.pair_const T1 T2 $ t1 $ t2
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    66
  end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    67
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    68
fun analyze_eqs ctxt defname fs eqs =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    69
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    70
    val num = length fs
39276
2ad95934521f improved error message for common mistake (fun f where "g x = ...")
krauss
parents: 36945
diff changeset
    71
    val fqgars = map (split_def ctxt (K true)) eqs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    72
    val arity_of = map (fn (fname,_,_,args,_) => (fname, length args)) fqgars
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    73
      |> AList.lookup (op =) #> the
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    74
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    75
    fun curried_types (fname, fT) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    76
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    77
        val (caTs, uaTs) = chop (arity_of fname) (binder_types fT)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    78
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    79
        (caTs, uaTs ---> body_type fT)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    80
      end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    81
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    82
    val (caTss, resultTs) = split_list (map curried_types fs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    83
    val argTs = map (foldr1 HOLogic.mk_prodT) caTss
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    84
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    85
    val dresultTs = distinct (op =) resultTs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    86
    val n' = length dresultTs
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    87
55968
blanchet
parents: 54984
diff changeset
    88
    val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs
blanchet
parents: 54984
diff changeset
    89
    val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    90
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    91
    val fsum_type = ST --> RST
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    92
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    93
    val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    94
    val fsum_var = (fsum_var_name, fsum_type)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    95
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    96
    fun define (fvar as (n, _)) caTs resultT i =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    97
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    98
        val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    99
        val i' = find_index (fn Ta => Ta = resultT) dresultTs + 1
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   100
55968
blanchet
parents: 54984
diff changeset
   101
        val f_exp = Sum_Tree.mk_proj RST n' i' (Free fsum_var $ Sum_Tree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   102
        val def = Term.abstract_over (Free fsum_var, fold_rev lambda vars f_exp)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   103
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   104
        val rew = (n, fold_rev lambda vars f_exp)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   105
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   106
        (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   107
      end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   108
58634
9f10d82e8188 added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
wenzelm
parents: 55968
diff changeset
   109
    val (parts, rews) = split_list (@{map 4} define fs caTss resultTs (1 upto num))
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   110
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   111
    fun convert_eqs (f, qs, gs, args, rhs) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   112
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   113
        val MutualPart {i, i', ...} = get_part f parts
42497
89acb654d8eb inlined Function_Lib.replace_frees, which is used only once
krauss
parents: 42361
diff changeset
   114
        val rhs' = rhs
89acb654d8eb inlined Function_Lib.replace_frees, which is used only once
krauss
parents: 42361
diff changeset
   115
          |> map_aterms (fn t as Free (n, _) => the_default t (AList.lookup (op =) rews n) | t => t)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   116
      in
55968
blanchet
parents: 54984
diff changeset
   117
        (qs, gs, Sum_Tree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
blanchet
parents: 54984
diff changeset
   118
         Envir.beta_norm (Sum_Tree.mk_inj RST n' i' rhs'))
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   119
      end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   120
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   121
    val qglrs = map convert_eqs fqgars
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   122
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   123
    Mutual {n=num, n'=n', fsum_var=fsum_var, ST=ST, RST=RST,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   124
      parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   125
  end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   126
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   127
fun define_projections fixes mutual fsum lthy =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   128
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   129
    fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   130
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   131
        val ((f, (_, f_defthm)), lthy') =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   132
          Local_Theory.define
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   133
            ((Binding.name fname, mixfix),
59859
f9d1442c70f3 tuned signature;
wenzelm
parents: 59651
diff changeset
   134
              ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   135
              Term.subst_bound (fsum, f_def))) lthy
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   136
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   137
        (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   138
           f=SOME f, f_defthm=SOME f_defthm },
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   139
         lthy')
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   140
      end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   141
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   142
    val Mutual { n, n', fsum_var, ST, RST, parts, fqgars, qglrs, ... } = mutual
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   143
    val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   144
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   145
    (Mutual { n=n, n'=n', fsum_var=fsum_var, ST=ST, RST=RST, parts=parts',
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   146
       fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   147
     lthy')
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   148
  end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   149
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   150
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   151
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   152
    val oqnames = map fst pre_qs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   153
    val (qs, _) = Variable.variant_fixes oqnames ctxt
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   154
      |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   155
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   156
    fun inst t = subst_bounds (rev qs, t)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   157
    val gs = map inst pre_gs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   158
    val args = map inst pre_args
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   159
    val rhs = inst pre_rhs
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   160
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59618
diff changeset
   161
    val cqs = map (Thm.cterm_of ctxt) qs
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59618
diff changeset
   162
    val ags = map (Thm.assume o Thm.cterm_of ctxt) gs
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   163
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   164
    val import = fold Thm.forall_elim cqs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   165
      #> fold Thm.elim_implies ags
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   166
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59580
diff changeset
   167
    val export = fold_rev (Thm.implies_intr o Thm.cprop_of) ags
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   168
      #> fold_rev forall_intr_rename (oqnames ~~ cqs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   169
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   170
    F ctxt (f, qs, gs, args, rhs) import export
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   171
  end
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   172
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   173
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
45403
wenzelm
parents: 42497
diff changeset
   174
    import (export : thm -> thm) sum_psimp_eq =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   175
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   176
    val (MutualPart {f=SOME f, ...}) = get_part fname parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   177
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   178
    val psimp = import sum_psimp_eq
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   179
    val (simp, restore_cond) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   180
      case cprems_of psimp of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   181
        [] => (psimp, I)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   182
      | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
40317
1eac228c52b3 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
wenzelm
parents: 40076
diff changeset
   183
      | _ => raise General.Fail "Too many conditions"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   184
54984
da70ab8531f4 more elementary management of declared hyps, below structure Assumption;
wenzelm
parents: 54566
diff changeset
   185
    val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   186
  in
54566
5f3e9baa8f13 more accurate goal context;
wenzelm
parents: 53608
diff changeset
   187
    Goal.prove simp_ctxt [] []
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   188
      (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
45403
wenzelm
parents: 42497
diff changeset
   189
      (fn _ =>
wenzelm
parents: 42497
diff changeset
   190
        Local_Defs.unfold_tac ctxt all_orig_fdefs
wenzelm
parents: 42497
diff changeset
   191
          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   192
          THEN (simp_tac ctxt) 1)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   193
    |> restore_cond
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   194
    |> export
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   195
  end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   196
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   197
fun mk_applied_form ctxt caTs thm =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   198
  let
59582
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59580
diff changeset
   199
    val xs =
0fbed69ff081 tuned signature -- prefer qualified names;
wenzelm
parents: 59580
diff changeset
   200
      map_index (fn (i, T) =>
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59618
diff changeset
   201
        Thm.cterm_of ctxt
59618
e6939796717e clarified context;
wenzelm
parents: 59582
diff changeset
   202
          (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   203
  in
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   204
    fold (fn x => fn thm => Thm.combination thm (Thm.reflexive x)) xs thm
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   205
    |> Conv.fconv_rule (Thm.beta_conversion true)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   206
    |> fold_rev Thm.forall_intr xs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   207
    |> Thm.forall_elim_vars 0
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   208
  end
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   209
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   210
fun mutual_induct_rules ctxt induct all_f_defs (Mutual {n, ST, parts, ...}) =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   211
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   212
    val newPs =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   213
      map2 (fn Pname => fn MutualPart {cargTs, ...} =>
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   214
          Free (Pname, cargTs ---> HOLogic.boolT))
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   215
        (mutual_induct_Pnames (length parts)) parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   216
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   217
    fun mk_P (MutualPart {cargTs, ...}) P =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   218
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   219
        val avars = map_index (fn (i,T) => Var (("a", i), T)) cargTs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   220
        val atup = foldr1 HOLogic.mk_prod avars
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   221
      in
39756
6c8e83d94536 consolidated tupled_lambda; moved to structure HOLogic
krauss
parents: 39276
diff changeset
   222
        HOLogic.tupled_lambda atup (list_comb (P, avars))
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   223
      end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   224
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   225
    val Ps = map2 mk_P parts newPs
55968
blanchet
parents: 54984
diff changeset
   226
    val case_exp = Sum_Tree.mk_sumcases HOLogic.boolT Ps
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   227
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   228
    val induct_inst =
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59618
diff changeset
   229
      Thm.forall_elim (Thm.cterm_of ctxt case_exp) induct
55968
blanchet
parents: 54984
diff changeset
   230
      |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   231
      |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps all_f_defs)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   233
    fun project rule (MutualPart {cargTs, i, ...}) k =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   234
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   235
        val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
55968
blanchet
parents: 54984
diff changeset
   236
        val inj = Sum_Tree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   237
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   238
        (rule
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59618
diff changeset
   239
         |> Thm.forall_elim (Thm.cterm_of ctxt inj)
55968
blanchet
parents: 54984
diff changeset
   240
         |> full_simplify (put_simpset Sum_Tree.sumcase_split_ss ctxt)
59621
291934bac95e Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents: 59618
diff changeset
   241
         |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) (afs @ newPs),
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   242
         k + length cargTs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   243
      end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   244
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   245
    fst (fold_map (project induct_inst) parts 0)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   246
  end
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   247
59651
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   248
fun mutual_cases_rule ctxt cases_rule n ST (MutualPart {i, cargTs = Ts, ...}) =
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   249
  let
59651
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   250
    val [P, x] =
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   251
      Variable.variant_frees ctxt [] [("P", @{typ bool}), ("x", HOLogic.mk_tupleT Ts)]
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   252
      |> map (Thm.cterm_of ctxt o Free);
60321
wenzelm
parents: 59859
diff changeset
   253
    val sumtree_inj = Thm.cterm_of ctxt (Sum_Tree.mk_inj ST n i (Thm.term_of x));
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   254
59651
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   255
    fun prep_subgoal_tac i =
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   256
      REPEAT (eresolve_tac ctxt
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   257
        @{thms Pair_inject Inl_inject [elim_format] Inr_inject [elim_format]} i)
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   258
      THEN REPEAT (eresolve_tac ctxt
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   259
        @{thms HOL.notE [OF Sum_Type.sum.distinct(1)] HOL.notE [OF Sum_Type.sum.distinct(2)]} i);
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   260
  in
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   261
    cases_rule
59454
588b81d19823 Fixed variable naming bug in function package
eberlm
parents: 58634
diff changeset
   262
    |> Thm.forall_elim P
59651
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   263
    |> Thm.forall_elim sumtree_inj
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   264
    |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
7f5f0e785a44 misc tuning and simplification;
wenzelm
parents: 59621
diff changeset
   265
    |> Thm.forall_intr x
59454
588b81d19823 Fixed variable naming bug in function package
eberlm
parents: 58634
diff changeset
   266
    |> Thm.forall_intr P
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   267
  end
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   268
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   269
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   270
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, n, ST, ...}) proof =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   271
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   272
    val result = inner_cont proof
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   273
    val FunctionResult {G, R, cases=[cases_rule], psimps, simple_pinducts=[simple_pinduct],
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   274
      termination, domintros, dom, pelims, ...} = result
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   275
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   276
    val (all_f_defs, fs) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   277
      map (fn MutualPart {f_defthm = SOME f_def, f = SOME f, cargTs, ...} =>
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   278
        (mk_applied_form lthy cargTs (Thm.symmetric f_def), f))
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   279
      parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   280
      |> split_list
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   281
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   282
    val all_orig_fdefs =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   283
      map (fn MutualPart {f_defthm = SOME f_def, ...} => f_def) parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   284
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   285
    fun mk_mpsimp fqgar sum_psimp =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   286
      in_context lthy fqgar (recover_mutual_psimp all_orig_fdefs parts) sum_psimp
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   287
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   288
    val rew_simpset = put_simpset HOL_basic_ss lthy addsimps all_f_defs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   289
    val mpsimps = map2 mk_mpsimp fqgars psimps
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   290
    val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   291
    val mcases = map (mutual_cases_rule lthy cases_rule n ST) parts
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   292
    val mtermination = full_simplify rew_simpset termination
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   293
    val mdomintros = Option.map (map (full_simplify rew_simpset)) domintros
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   294
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   295
  in
52384
80c00a851de5 export dom predicate in the info record
krauss
parents: 51717
diff changeset
   296
    FunctionResult { fs=fs, G=G, R=R, dom=dom,
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   297
      psimps=mpsimps, simple_pinducts=minducts,
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   298
      cases=mcases, pelims=pelims, termination=mtermination,
41846
b368a7aee46a removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents: 41114
diff changeset
   299
      domintros=mdomintros}
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   300
  end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   301
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   302
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
   303
fun prepare_function_mutual config defname fixes eqss lthy =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   304
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   305
    val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   306
      analyze_eqs lthy defname (map fst fixes) (map Envir.beta_eta_contract eqss)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   307
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   308
    val ((fsum, goalstate, cont), lthy') =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   309
      Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   310
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   311
    val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   312
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   313
    val cont' = mk_partial_rules_mutual lthy'' cont mutual'
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   314
  in
53608
53bd62921c54 moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
krauss
parents: 53607
diff changeset
   315
    ((goalstate, cont'), lthy'')
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   316
  end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   317
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   318
end