src/HOL/Tools/Function/mutual.ML
author krauss
Sun, 08 Sep 2013 23:28:27 +0200
changeset 53605 462151f900ea
parent 53603 59ef06cda7b9
child 53606 c3f7070dd05a
permissions -rw-r--r--
dropped dead code
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
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
     9
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
    10
  val prepare_function_mutual : Function_Common.function_config
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    11
    -> string (* defname *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    12
    -> ((string * typ) * mixfix) list
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    13
    -> term list
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    14
    -> local_theory
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    15
    -> ((thm (* goalstate *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    16
        * (thm -> Function_Common.function_result) (* proof continuation *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    17
       ) * local_theory)
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    18
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    19
end
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    20
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
structure Function_Mutual: FUNCTION_MUTUAL =
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    23
struct
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    24
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
    25
open Function_Lib
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
    26
open Function_Common
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    27
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    28
type qgar = string * (string * typ) list * term list * term list * term
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    29
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    30
datatype mutual_part = MutualPart of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    31
 {i : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    32
  i' : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    33
  fvar : string * typ,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    34
  cargTs: typ list,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    35
  f_def: term,
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
  f: term option,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    38
  f_defthm : thm option}
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    39
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    40
datatype mutual_info = Mutual of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    41
 {n : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    42
  n' : int,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    43
  fsum_var : string * 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
  ST: typ,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    46
  RST: typ,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    47
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    48
  parts: mutual_part list,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    49
  fqgars: qgar list,
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    50
  qglrs: ((string * typ) list * term list * term * term) list,
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    51
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    52
  fsum : term option}
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    53
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
    54
fun mutual_induct_Pnames n =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    55
  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
    56
  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
    57
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    58
fun get_part fname =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    59
  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
    60
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    61
(* FIXME *)
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    62
fun mk_prod_abs e (t1, t2) =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    63
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    64
    val bTs = rev (map snd e)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    65
    val T1 = fastype_of1 (bTs, t1)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    66
    val T2 = fastype_of1 (bTs, t2)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    67
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    68
    HOLogic.pair_const T1 T2 $ t1 $ t2
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    69
  end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
    70
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
    71
fun analyze_eqs ctxt defname fs eqs =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    72
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    73
    val num = length fs
39276
2ad95934521f improved error message for common mistake (fun f where "g x = ...")
krauss
parents: 36945
diff changeset
    74
    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
    75
    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
    76
      |> AList.lookup (op =) #> the
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    77
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    78
    fun curried_types (fname, fT) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    79
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    80
        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
    81
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    82
        (caTs, uaTs ---> body_type fT)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    83
      end
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 (caTss, resultTs) = split_list (map curried_types fs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    86
    val argTs = map (foldr1 HOLogic.mk_prodT) caTss
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    87
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    88
    val dresultTs = distinct (op =) resultTs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    89
    val n' = length dresultTs
23494
f985f9239e0d removed "sum_tools.ML" in favour of BalancedTree
krauss
parents: 23217
diff changeset
    90
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    91
    val RST = Balanced_Tree.make (uncurry SumTree.mk_sumT) dresultTs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    92
    val ST = Balanced_Tree.make (uncurry SumTree.mk_sumT) argTs
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    93
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    94
    val fsum_type = ST --> RST
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
    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
    97
    val fsum_var = (fsum_var_name, fsum_type)
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
    98
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
    99
    fun define (fvar as (n, _)) caTs resultT i =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   100
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   101
        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
   102
        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
   103
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   104
        val f_exp = SumTree.mk_proj RST n' i' (Free fsum_var $ SumTree.mk_inj ST num i (foldr1 HOLogic.mk_prod vars))
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   105
        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
   106
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   107
        val rew = (n, fold_rev lambda vars f_exp)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   108
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   109
        (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
   110
      end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   111
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   112
    val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   113
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   114
    fun convert_eqs (f, qs, gs, args, rhs) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   115
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   116
        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
   117
        val rhs' = rhs
89acb654d8eb inlined Function_Lib.replace_frees, which is used only once
krauss
parents: 42361
diff changeset
   118
          |> 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
   119
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   120
        (qs, gs, SumTree.mk_inj ST num i (foldr1 (mk_prod_abs qs) args),
42497
89acb654d8eb inlined Function_Lib.replace_frees, which is used only once
krauss
parents: 42361
diff changeset
   121
         Envir.beta_norm (SumTree.mk_inj RST n' i' rhs'))
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   122
      end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   123
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   124
    val qglrs = map convert_eqs fqgars
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   125
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   126
    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
   127
      parts=parts, fqgars=fqgars, qglrs=qglrs, fsum=NONE}
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   128
  end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   129
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   130
fun define_projections fixes mutual fsum lthy =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   131
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   132
    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
   133
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   134
        val ((f, (_, f_defthm)), lthy') =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   135
          Local_Theory.define
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   136
            ((Binding.name fname, mixfix),
46909
3c73a121a387 more explicit indication of def names;
wenzelm
parents: 45403
diff changeset
   137
              ((Binding.conceal (Binding.name (Thm.def_name fname)), []),
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   138
              Term.subst_bound (fsum, f_def))) lthy
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   139
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   140
        (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
   141
           f=SOME f, f_defthm=SOME f_defthm },
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   142
         lthy')
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   143
      end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   144
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   145
    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
   146
    val (parts', lthy') = fold_map def (parts ~~ fixes) lthy
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   147
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   148
    (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
   149
       fqgars=fqgars, qglrs=qglrs, fsum=SOME fsum },
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   150
     lthy')
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   151
  end
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   152
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   153
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
   154
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41846
diff changeset
   155
    val thy = Proof_Context.theory_of ctxt
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   156
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   157
    val oqnames = map fst pre_qs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   158
    val (qs, _) = Variable.variant_fixes oqnames ctxt
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   159
      |>> 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
   160
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   161
    fun inst t = subst_bounds (rev qs, t)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   162
    val gs = map inst pre_gs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   163
    val args = map inst pre_args
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   164
    val rhs = inst pre_rhs
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   165
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   166
    val cqs = map (cterm_of thy) qs
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   167
    val ags = map (Thm.assume o cterm_of thy) gs
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   168
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   169
    val import = fold Thm.forall_elim cqs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   170
      #> fold Thm.elim_implies ags
20523
36a59e5d0039 Major update to function package, including new syntax and the (only theoretical)
krauss
parents: 19922
diff changeset
   171
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   172
    val export = fold_rev (Thm.implies_intr o cprop_of) ags
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   173
      #> fold_rev forall_intr_rename (oqnames ~~ cqs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   174
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   175
    F ctxt (f, qs, gs, args, rhs) import export
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   176
  end
22497
1fe951654cee fixed problem with the construction of mutual simp rules
krauss
parents: 22323
diff changeset
   177
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   178
fun recover_mutual_psimp all_orig_fdefs parts ctxt (fname, _, _, args, rhs)
45403
wenzelm
parents: 42497
diff changeset
   179
    import (export : thm -> thm) sum_psimp_eq =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   180
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   181
    val (MutualPart {f=SOME f, ...}) = get_part fname parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   182
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   183
    val psimp = import sum_psimp_eq
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   184
    val (simp, restore_cond) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   185
      case cprems_of psimp of
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   186
        [] => (psimp, I)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   187
      | [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
   188
      | _ => raise General.Fail "Too many conditions"
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   189
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   190
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   191
    Goal.prove ctxt [] []
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   192
      (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
45403
wenzelm
parents: 42497
diff changeset
   193
      (fn _ =>
wenzelm
parents: 42497
diff changeset
   194
        Local_Defs.unfold_tac ctxt all_orig_fdefs
wenzelm
parents: 42497
diff changeset
   195
          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
   196
          THEN (simp_tac ctxt) 1)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   197
    |> restore_cond
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   198
    |> export
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   199
  end
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   200
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   201
fun mk_applied_form ctxt caTs thm =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   202
  let
42361
23f352990944 modernized structure Proof_Context;
wenzelm
parents: 41846
diff changeset
   203
    val thy = Proof_Context.theory_of ctxt
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   204
    val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   205
  in
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   206
    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
   207
    |> Conv.fconv_rule (Thm.beta_conversion true)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   208
    |> fold_rev Thm.forall_intr xs
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   209
    |> Thm.forall_elim_vars 0
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   210
  end
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   211
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   212
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
   213
  let
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   214
    val cert = cterm_of (Proof_Context.theory_of ctxt)
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   215
    val newPs =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   216
      map2 (fn Pname => fn MutualPart {cargTs, ...} =>
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   217
          Free (Pname, cargTs ---> HOLogic.boolT))
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   218
        (mutual_induct_Pnames (length parts)) parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   219
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   220
    fun mk_P (MutualPart {cargTs, ...}) P =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   221
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   222
        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
   223
        val atup = foldr1 HOLogic.mk_prod avars
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   224
      in
39756
6c8e83d94536 consolidated tupled_lambda; moved to structure HOLogic
krauss
parents: 39276
diff changeset
   225
        HOLogic.tupled_lambda atup (list_comb (P, avars))
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   226
      end
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 Ps = map2 mk_P parts newPs
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   229
    val case_exp = SumTree.mk_sumcases HOLogic.boolT Ps
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   230
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   231
    val induct_inst =
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   232
      Thm.forall_elim (cert case_exp) induct
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   233
      |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   234
      |> 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
   235
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   236
    fun project rule (MutualPart {cargTs, i, ...}) k =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   237
      let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   238
        val afs = map_index (fn (j,T) => Free ("a" ^ string_of_int (j + k), T)) cargTs (* FIXME! *)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   239
        val inj = SumTree.mk_inj ST n i (foldr1 HOLogic.mk_prod afs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   240
      in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   241
        (rule
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   242
         |> Thm.forall_elim (cert inj)
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   243
         |> full_simplify (put_simpset SumTree.sumcase_split_ss ctxt)
36945
9bec62c10714 less pervasive names from structure Thm;
wenzelm
parents: 36773
diff changeset
   244
         |> fold_rev (Thm.forall_intr o cert) (afs @ newPs),
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   245
         k + length cargTs)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   246
      end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   247
  in
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   248
    fst (fold_map (project induct_inst) parts 0)
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   249
  end
20878
384c5bb713b2 mk_partial_rules_mutual: expand result terms/thms;
wenzelm
parents: 20851
diff changeset
   250
22623
5fcee5b319a2 proper handling of morphisms
krauss
parents: 22622
diff changeset
   251
fun mk_partial_rules_mutual lthy inner_cont (m as Mutual {parts, fqgars, ...}) proof =
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   252
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   253
    val result = inner_cont proof
41846
b368a7aee46a removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents: 41114
diff changeset
   254
    val FunctionResult {G, R, cases, psimps, simple_pinducts=[simple_pinduct],
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   255
      termination, domintros, dom, pelims, ...} = result
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   256
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   257
    val (all_f_defs, fs) =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   258
      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
   259
        (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
   260
      parts
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   261
      |> split_list
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   262
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   263
    val all_orig_fdefs =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   264
      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
   265
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   266
    fun mk_mpsimp fqgar sum_psimp =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   267
      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
   268
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   269
    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
   270
    val mpsimps = map2 mk_mpsimp fqgars psimps
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   271
    val minducts = mutual_induct_rules lthy simple_pinduct all_f_defs m
51717
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   272
    val mtermination = full_simplify rew_simpset termination
9e7d1c139569 simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents: 46909
diff changeset
   273
    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
   274
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   275
  in
52384
80c00a851de5 export dom predicate in the info record
krauss
parents: 51717
diff changeset
   276
    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
   277
      psimps=mpsimps, simple_pinducts=minducts,
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   278
      cases=cases, pelims=pelims, termination=mtermination,
41846
b368a7aee46a removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents: 41114
diff changeset
   279
      domintros=mdomintros}
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   280
  end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   281
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   282
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   283
fun postprocess_cases_rules ctxt cont proof =
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   284
  let val result = cont proof;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   285
      val FunctionResult {fs, G, R, dom, psimps, simple_pinducts, cases, pelims,
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   286
                        termination, domintros, ...} = result;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   287
      val n_fs = length fs;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   288
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   289
      fun postprocess_cases_rule (idx,f) =
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   290
        let fun dest_funprop (Const ("HOL.eq", _) $ lhs $ rhs) = (strip_comb lhs, rhs)
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   291
              | dest_funprop (Const ("HOL.Not", _) $ trm) = (strip_comb trm, @{term "False"})
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   292
              | dest_funprop trm = (strip_comb trm, @{term "True"});
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   293
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   294
            fun mk_fun_args 0 _ acc_vars = rev acc_vars
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   295
              | mk_fun_args n (Type("fun",[S,T])) acc_vars =
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   296
                let val xn = Free ("x" ^ Int.toString n,S) in
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   297
                  mk_fun_args (n - 1) T (xn :: acc_vars)
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   298
                end
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   299
              | mk_fun_args _ _ _ = raise (TERM ("Not a function.", [f]))
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   300
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   301
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   302
            val f_simps = filter (fn r => (prop_of r |> Logic.strip_assums_concl
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   303
                                           |> HOLogic.dest_Trueprop
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   304
                                           |> dest_funprop |> fst |> fst) = f)
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   305
                                 psimps
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   306
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   307
            val arity = hd f_simps |> prop_of |> Logic.strip_assums_concl
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   308
                                   |> HOLogic.dest_Trueprop
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   309
                                   |> snd o fst o dest_funprop |> length;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   310
            val arg_vars = mk_fun_args arity (fastype_of f) []
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   311
            val argsT = fastype_of (HOLogic.mk_tuple arg_vars);
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   312
            val args = Free ("x", argsT);
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   313
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   314
            val thy = Proof_Context.theory_of ctxt;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   315
            val domT = R |> dest_Free |> snd |> hd o snd o dest_Type
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   316
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   317
            val sumtree_inj = SumTree.mk_inj domT n_fs (idx+1) args;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   318
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   319
            val sum_elims = @{thms HOL.notE[OF Sum_Type.sum.distinct(1)]
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   320
                                   HOL.notE[OF Sum_Type.sum.distinct(2)]};
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   321
            fun prep_subgoal i =
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   322
              REPEAT (eresolve_tac @{thms Pair_inject Inl_inject[elim_format]
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   323
                                          Inr_inject[elim_format]} i)
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   324
              THEN REPEAT (Tactic.eresolve_tac sum_elims i);
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   325
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   326
            val tac = ALLGOALS prep_subgoal;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   327
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   328
        in
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   329
            hd cases
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   330
              |> Thm.forall_elim @{cterm "P::bool"}
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   331
              |> Thm.forall_elim (cterm_of thy sumtree_inj)
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   332
              |> Tactic.rule_by_tactic ctxt tac
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   333
              |> Thm.forall_intr (cterm_of thy args)
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   334
              |> Thm.forall_intr @{cterm "P::bool"}
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   335
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   336
        end;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   337
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   338
  val cases' = map_index postprocess_cases_rule fs;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   339
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   340
in
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   341
  FunctionResult {fs=fs, G=G, R=R, dom=dom, psimps=psimps,
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   342
                  simple_pinducts=simple_pinducts,
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   343
                  cases=cases', pelims=pelims, termination=termination,
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   344
                  domintros=domintros}
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   345
end;
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   346
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   347
33099
b8cdd3d73022 function package: more standard names for structures and files
krauss
parents: 32765
diff changeset
   348
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
   349
  let
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   350
    val mutual as Mutual {fsum_var=(n, T), qglrs, ...} =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   351
      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
   352
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   353
    val ((fsum, goalstate, cont), lthy') =
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   354
      Function_Core.prepare_function config defname [((n, T), NoSyn)] qglrs lthy
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   355
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   356
    val (mutual', lthy'') = define_projections fixes mutual fsum lthy'
22166
0a50d4db234a * Preliminary implementation of tail recursion
krauss
parents: 21436
diff changeset
   357
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   358
    val cont' = mk_partial_rules_mutual lthy'' cont mutual'
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   359
    val cont'' = postprocess_cases_rules lthy'' cont'
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   360
  in
53603
59ef06cda7b9 generate elim rules for elimination of function equalities;
Manuel Eberl
parents: 52384
diff changeset
   361
    ((goalstate, cont''), lthy'')
34232
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   362
  end
36a2a3029fd3 new year's resolution: reindented code in function package
krauss
parents: 33855
diff changeset
   363
19770
be5c23ebe1eb HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
diff changeset
   364
end