src/HOLCF/Tools/Domain/domain_take_proofs.ML
author huffman
Tue Mar 02 14:33:34 2010 -0800 (2010-03-02)
changeset 35515 d631dc53ede0
parent 35514 a2cfa413eaab
child 35555 ec01c27bf580
permissions -rw-r--r--
move definition of finiteness predicate into domain_take_proofs.ML
huffman@35514
     1
(*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
huffman@35514
     2
    Author:     Brian Huffman
huffman@35514
     3
huffman@35514
     4
Defines take functions for the given domain equation
huffman@35514
     5
and proves related theorems.
huffman@35514
     6
*)
huffman@35514
     7
huffman@35514
     8
signature DOMAIN_TAKE_PROOFS =
huffman@35514
     9
sig
huffman@35514
    10
  type iso_info =
huffman@35514
    11
    {
huffman@35514
    12
      absT : typ,
huffman@35514
    13
      repT : typ,
huffman@35514
    14
      abs_const : term,
huffman@35514
    15
      rep_const : term,
huffman@35514
    16
      abs_inverse : thm,
huffman@35514
    17
      rep_inverse : thm
huffman@35514
    18
    }
huffman@35514
    19
huffman@35514
    20
  val define_take_functions :
huffman@35514
    21
    (binding * iso_info) list -> theory ->
huffman@35514
    22
    { take_consts : term list,
huffman@35514
    23
      take_defs : thm list,
huffman@35514
    24
      chain_take_thms : thm list,
huffman@35514
    25
      take_0_thms : thm list,
huffman@35514
    26
      take_Suc_thms : thm list,
huffman@35515
    27
      deflation_take_thms : thm list,
huffman@35515
    28
      finite_consts : term list,
huffman@35515
    29
      finite_defs : thm list
huffman@35514
    30
    } * theory
huffman@35514
    31
huffman@35514
    32
  val map_of_typ :
huffman@35514
    33
    theory -> (typ * term) list -> typ -> term
huffman@35514
    34
huffman@35514
    35
  val add_map_function :
huffman@35514
    36
    (string * string * thm) -> theory -> theory
huffman@35514
    37
huffman@35514
    38
  val get_map_tab : theory -> string Symtab.table
huffman@35514
    39
  val get_deflation_thms : theory -> thm list
huffman@35514
    40
end;
huffman@35514
    41
huffman@35514
    42
structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
huffman@35514
    43
struct
huffman@35514
    44
huffman@35514
    45
type iso_info =
huffman@35514
    46
  {
huffman@35514
    47
    absT : typ,
huffman@35514
    48
    repT : typ,
huffman@35514
    49
    abs_const : term,
huffman@35514
    50
    rep_const : term,
huffman@35514
    51
    abs_inverse : thm,
huffman@35514
    52
    rep_inverse : thm
huffman@35514
    53
  };
huffman@35514
    54
huffman@35514
    55
val beta_ss =
huffman@35514
    56
  HOL_basic_ss
huffman@35514
    57
    addsimps simp_thms
huffman@35514
    58
    addsimps [@{thm beta_cfun}]
huffman@35514
    59
    addsimprocs [@{simproc cont_proc}];
huffman@35514
    60
huffman@35514
    61
val beta_tac = simp_tac beta_ss;
huffman@35514
    62
huffman@35514
    63
(******************************************************************************)
huffman@35514
    64
(******************************** theory data *********************************)
huffman@35514
    65
(******************************************************************************)
huffman@35514
    66
huffman@35514
    67
structure MapData = Theory_Data
huffman@35514
    68
(
huffman@35514
    69
  (* constant names like "foo_map" *)
huffman@35514
    70
  type T = string Symtab.table;
huffman@35514
    71
  val empty = Symtab.empty;
huffman@35514
    72
  val extend = I;
huffman@35514
    73
  fun merge data = Symtab.merge (K true) data;
huffman@35514
    74
);
huffman@35514
    75
huffman@35514
    76
structure DeflMapData = Theory_Data
huffman@35514
    77
(
huffman@35514
    78
  (* theorems like "deflation a ==> deflation (foo_map$a)" *)
huffman@35514
    79
  type T = thm list;
huffman@35514
    80
  val empty = [];
huffman@35514
    81
  val extend = I;
huffman@35514
    82
  val merge = Thm.merge_thms;
huffman@35514
    83
);
huffman@35514
    84
huffman@35514
    85
fun add_map_function (tname, map_name, deflation_map_thm) =
huffman@35514
    86
    MapData.map (Symtab.insert (K true) (tname, map_name))
huffman@35514
    87
    #> DeflMapData.map (Thm.add_thm deflation_map_thm);
huffman@35514
    88
huffman@35514
    89
val get_map_tab = MapData.get;
huffman@35514
    90
val get_deflation_thms = DeflMapData.get;
huffman@35514
    91
huffman@35514
    92
(******************************************************************************)
huffman@35514
    93
(************************** building types and terms **************************)
huffman@35514
    94
(******************************************************************************)
huffman@35514
    95
huffman@35514
    96
open HOLCF_Library;
huffman@35514
    97
huffman@35514
    98
infixr 6 ->>;
huffman@35514
    99
infix -->>;
huffman@35515
   100
infix 9 `;
huffman@35514
   101
huffman@35514
   102
val deflT = @{typ "udom alg_defl"};
huffman@35514
   103
huffman@35514
   104
fun mapT (T as Type (_, Ts)) =
huffman@35514
   105
    (map (fn T => T ->> T) Ts) -->> (T ->> T)
huffman@35514
   106
  | mapT T = T ->> T;
huffman@35514
   107
huffman@35514
   108
fun mk_Rep_of T =
huffman@35514
   109
  Const (@{const_name Rep_of}, Term.itselfT T --> deflT) $ Logic.mk_type T;
huffman@35514
   110
huffman@35514
   111
fun coerce_const T = Const (@{const_name coerce}, T);
huffman@35514
   112
huffman@35514
   113
fun isodefl_const T =
huffman@35514
   114
  Const (@{const_name isodefl}, (T ->> T) --> deflT --> HOLogic.boolT);
huffman@35514
   115
huffman@35514
   116
fun mk_deflation t =
huffman@35514
   117
  Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
huffman@35514
   118
huffman@35514
   119
fun mk_lub t =
huffman@35514
   120
  let
huffman@35514
   121
    val T = Term.range_type (Term.fastype_of t);
huffman@35514
   122
    val lub_const = Const (@{const_name lub}, (T --> boolT) --> T);
huffman@35514
   123
    val UNIV_const = @{term "UNIV :: nat set"};
huffman@35514
   124
    val image_type = (natT --> T) --> (natT --> boolT) --> T --> boolT;
huffman@35514
   125
    val image_const = Const (@{const_name image}, image_type);
huffman@35514
   126
  in
huffman@35514
   127
    lub_const $ (image_const $ t $ UNIV_const)
huffman@35514
   128
  end;
huffman@35514
   129
huffman@35514
   130
(* splits a cterm into the right and lefthand sides of equality *)
huffman@35514
   131
fun dest_eqs t = HOLogic.dest_eq (HOLogic.dest_Trueprop t);
huffman@35514
   132
huffman@35514
   133
fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
huffman@35514
   134
huffman@35514
   135
(******************************************************************************)
huffman@35514
   136
(****************************** isomorphism info ******************************)
huffman@35514
   137
(******************************************************************************)
huffman@35514
   138
huffman@35514
   139
fun deflation_abs_rep (info : iso_info) : thm =
huffman@35514
   140
  let
huffman@35514
   141
    val abs_iso = #abs_inverse info;
huffman@35514
   142
    val rep_iso = #rep_inverse info;
huffman@35514
   143
    val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
huffman@35514
   144
  in
huffman@35514
   145
    Drule.export_without_context thm
huffman@35514
   146
  end
huffman@35514
   147
huffman@35514
   148
(******************************************************************************)
huffman@35514
   149
(********************* building map functions over types **********************)
huffman@35514
   150
(******************************************************************************)
huffman@35514
   151
huffman@35514
   152
fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
huffman@35514
   153
  let
huffman@35514
   154
    val map_tab = get_map_tab thy;
huffman@35514
   155
    fun auto T = T ->> T;
huffman@35514
   156
    fun map_of T =
huffman@35514
   157
        case AList.lookup (op =) sub T of
huffman@35514
   158
          SOME m => (m, true) | NONE => map_of' T
huffman@35514
   159
    and map_of' (T as (Type (c, Ts))) =
huffman@35514
   160
        (case Symtab.lookup map_tab c of
huffman@35514
   161
          SOME map_name =>
huffman@35514
   162
          let
huffman@35514
   163
            val map_type = map auto Ts -->> auto T;
huffman@35514
   164
            val (ms, bs) = map_split map_of Ts;
huffman@35514
   165
          in
huffman@35514
   166
            if exists I bs
huffman@35514
   167
            then (list_ccomb (Const (map_name, map_type), ms), true)
huffman@35514
   168
            else (mk_ID T, false)
huffman@35514
   169
          end
huffman@35514
   170
        | NONE => (mk_ID T, false))
huffman@35514
   171
      | map_of' T = (mk_ID T, false);
huffman@35514
   172
  in
huffman@35514
   173
    fst (map_of T)
huffman@35514
   174
  end;
huffman@35514
   175
huffman@35514
   176
huffman@35514
   177
(******************************************************************************)
huffman@35514
   178
(********************* declaring definitions and theorems *********************)
huffman@35514
   179
(******************************************************************************)
huffman@35514
   180
huffman@35514
   181
fun define_const
huffman@35514
   182
    (bind : binding, rhs : term)
huffman@35514
   183
    (thy : theory)
huffman@35514
   184
    : (term * thm) * theory =
huffman@35514
   185
  let
huffman@35514
   186
    val typ = Term.fastype_of rhs;
huffman@35514
   187
    val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy;
huffman@35514
   188
    val eqn = Logic.mk_equals (const, rhs);
huffman@35514
   189
    val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn);
huffman@35514
   190
    val (def_thm, thy) = yield_singleton (PureThy.add_defs false) def thy;
huffman@35514
   191
  in
huffman@35514
   192
    ((const, def_thm), thy)
huffman@35514
   193
  end;
huffman@35514
   194
huffman@35514
   195
fun add_qualified_thm name (path, thm) thy =
huffman@35514
   196
    thy
huffman@35514
   197
    |> Sign.add_path path
huffman@35514
   198
    |> yield_singleton PureThy.add_thms
huffman@35514
   199
        (Thm.no_attributes (Binding.name name, thm))
huffman@35514
   200
    ||> Sign.parent_path;
huffman@35514
   201
huffman@35514
   202
(******************************************************************************)
huffman@35514
   203
(************************** defining take functions ***************************)
huffman@35514
   204
(******************************************************************************)
huffman@35514
   205
huffman@35514
   206
fun define_take_functions
huffman@35514
   207
    (spec : (binding * iso_info) list)
huffman@35514
   208
    (thy : theory) =
huffman@35514
   209
  let
huffman@35514
   210
huffman@35514
   211
    (* retrieve components of spec *)
huffman@35514
   212
    val dom_binds = map fst spec;
huffman@35514
   213
    val iso_infos = map snd spec;
huffman@35514
   214
    val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
huffman@35514
   215
    val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
huffman@35514
   216
    val dnames = map Binding.name_of dom_binds;
huffman@35514
   217
huffman@35514
   218
    (* get table of map functions *)
huffman@35514
   219
    val map_tab = MapData.get thy;
huffman@35514
   220
huffman@35514
   221
    fun mk_projs []      t = []
huffman@35514
   222
      | mk_projs (x::[]) t = [(x, t)]
huffman@35514
   223
      | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
huffman@35514
   224
huffman@35514
   225
    fun mk_cfcomp2 ((rep_const, abs_const), f) =
huffman@35514
   226
        mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
huffman@35514
   227
huffman@35514
   228
    (* define take functional *)
huffman@35514
   229
    val newTs : typ list = map fst dom_eqns;
huffman@35514
   230
    val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
huffman@35514
   231
    val copy_arg = Free ("f", copy_arg_type);
huffman@35514
   232
    val copy_args = map snd (mk_projs dom_binds copy_arg);
huffman@35514
   233
    fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
huffman@35514
   234
      let
huffman@35514
   235
        val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
huffman@35514
   236
      in
huffman@35514
   237
        mk_cfcomp2 (rep_abs, body)
huffman@35514
   238
      end;
huffman@35514
   239
    val take_functional =
huffman@35514
   240
        big_lambda copy_arg
huffman@35514
   241
          (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
huffman@35514
   242
    val take_rhss =
huffman@35514
   243
      let
huffman@35514
   244
        val i = Free ("i", HOLogic.natT);
huffman@35514
   245
        val rhs = mk_iterate (i, take_functional)
huffman@35514
   246
      in
huffman@35514
   247
        map (Term.lambda i o snd) (mk_projs dom_binds rhs)
huffman@35514
   248
      end;
huffman@35514
   249
huffman@35514
   250
    (* define take constants *)
huffman@35514
   251
    fun define_take_const ((tbind, take_rhs), (lhsT, rhsT)) thy =
huffman@35514
   252
      let
huffman@35514
   253
        val take_type = HOLogic.natT --> lhsT ->> lhsT;
huffman@35514
   254
        val take_bind = Binding.suffix_name "_take" tbind;
huffman@35514
   255
        val (take_const, thy) =
huffman@35514
   256
          Sign.declare_const ((take_bind, take_type), NoSyn) thy;
huffman@35514
   257
        val take_eqn = Logic.mk_equals (take_const, take_rhs);
huffman@35514
   258
        val (take_def_thm, thy) =
huffman@35514
   259
          thy
huffman@35514
   260
          |> Sign.add_path (Binding.name_of tbind)
huffman@35514
   261
          |> yield_singleton
huffman@35514
   262
              (PureThy.add_defs false o map Thm.no_attributes)
huffman@35514
   263
              (Binding.name "take_def", take_eqn)
huffman@35514
   264
          ||> Sign.parent_path;
huffman@35514
   265
      in ((take_const, take_def_thm), thy) end;
huffman@35514
   266
    val ((take_consts, take_defs), thy) = thy
huffman@35514
   267
      |> fold_map define_take_const (dom_binds ~~ take_rhss ~~ dom_eqns)
huffman@35514
   268
      |>> ListPair.unzip;
huffman@35514
   269
huffman@35514
   270
    (* prove chain_take lemmas *)
huffman@35514
   271
    fun prove_chain_take (take_const, dname) thy =
huffman@35514
   272
      let
huffman@35514
   273
        val goal = mk_trp (mk_chain take_const);
huffman@35514
   274
        val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
huffman@35514
   275
        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
huffman@35514
   276
        val chain_take_thm = Goal.prove_global thy [] [] goal (K tac);
huffman@35514
   277
      in
huffman@35514
   278
        add_qualified_thm "chain_take" (dname, chain_take_thm) thy
huffman@35514
   279
      end;
huffman@35514
   280
    val (chain_take_thms, thy) =
huffman@35514
   281
      fold_map prove_chain_take (take_consts ~~ dnames) thy;
huffman@35514
   282
huffman@35514
   283
    (* prove take_0 lemmas *)
huffman@35514
   284
    fun prove_take_0 ((take_const, dname), (lhsT, rhsT)) thy =
huffman@35514
   285
      let
huffman@35514
   286
        val lhs = take_const $ @{term "0::nat"};
huffman@35514
   287
        val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
huffman@35514
   288
        val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
huffman@35514
   289
        val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
huffman@35514
   290
        val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
huffman@35514
   291
      in
huffman@35514
   292
        add_qualified_thm "take_0" (dname, take_0_thm) thy
huffman@35514
   293
      end;
huffman@35514
   294
    val (take_0_thms, thy) =
huffman@35514
   295
      fold_map prove_take_0 (take_consts ~~ dnames ~~ dom_eqns) thy;
huffman@35514
   296
huffman@35514
   297
    (* prove take_Suc lemmas *)
huffman@35514
   298
    val i = Free ("i", natT);
huffman@35514
   299
    val take_is = map (fn t => t $ i) take_consts;
huffman@35514
   300
    fun prove_take_Suc
huffman@35514
   301
          (((take_const, rep_abs), dname), (lhsT, rhsT)) thy =
huffman@35514
   302
      let
huffman@35514
   303
        val lhs = take_const $ (@{term Suc} $ i);
huffman@35514
   304
        val body = map_of_typ thy (newTs ~~ take_is) rhsT;
huffman@35514
   305
        val rhs = mk_cfcomp2 (rep_abs, body);
huffman@35514
   306
        val goal = mk_eqs (lhs, rhs);
huffman@35514
   307
        val simps = @{thms iterate_Suc fst_conv snd_conv}
huffman@35514
   308
        val rules = take_defs @ simps;
huffman@35514
   309
        val tac = simp_tac (beta_ss addsimps rules) 1;
huffman@35514
   310
        val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
huffman@35514
   311
      in
huffman@35514
   312
        add_qualified_thm "take_Suc" (dname, take_Suc_thm) thy
huffman@35514
   313
      end;
huffman@35514
   314
    val (take_Suc_thms, thy) =
huffman@35514
   315
      fold_map prove_take_Suc
huffman@35514
   316
        (take_consts ~~ rep_abs_consts ~~ dnames ~~ dom_eqns) thy;
huffman@35514
   317
huffman@35514
   318
    (* prove deflation theorems for take functions *)
huffman@35514
   319
    val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
huffman@35514
   320
    val deflation_take_thm =
huffman@35514
   321
      let
huffman@35514
   322
        val i = Free ("i", natT);
huffman@35514
   323
        fun mk_goal take_const = mk_deflation (take_const $ i);
huffman@35514
   324
        val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
huffman@35514
   325
        val adm_rules =
huffman@35514
   326
          @{thms adm_conj adm_subst [OF _ adm_deflation]
huffman@35514
   327
                 cont2cont_fst cont2cont_snd cont_id};
huffman@35514
   328
        val bottom_rules =
huffman@35514
   329
          take_0_thms @ @{thms deflation_UU simp_thms};
huffman@35514
   330
        val deflation_rules =
huffman@35514
   331
          @{thms conjI deflation_ID}
huffman@35514
   332
          @ deflation_abs_rep_thms
huffman@35514
   333
          @ DeflMapData.get thy;
huffman@35514
   334
      in
huffman@35514
   335
        Goal.prove_global thy [] [] goal (fn _ =>
huffman@35514
   336
         EVERY
huffman@35514
   337
          [rtac @{thm nat.induct} 1,
huffman@35514
   338
           simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
huffman@35514
   339
           asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
huffman@35514
   340
           REPEAT (etac @{thm conjE} 1
huffman@35514
   341
                   ORELSE resolve_tac deflation_rules 1
huffman@35514
   342
                   ORELSE atac 1)])
huffman@35514
   343
      end;
huffman@35514
   344
    fun conjuncts [] thm = []
huffman@35514
   345
      | conjuncts (n::[]) thm = [(n, thm)]
huffman@35514
   346
      | conjuncts (n::ns) thm = let
huffman@35514
   347
          val thmL = thm RS @{thm conjunct1};
huffman@35514
   348
          val thmR = thm RS @{thm conjunct2};
huffman@35514
   349
        in (n, thmL):: conjuncts ns thmR end;
huffman@35514
   350
    val (deflation_take_thms, thy) =
huffman@35514
   351
      fold_map (add_qualified_thm "deflation_take")
huffman@35514
   352
        (map (apsnd Drule.export_without_context)
huffman@35514
   353
          (conjuncts dnames deflation_take_thm)) thy;
huffman@35514
   354
huffman@35514
   355
    (* prove strictness of take functions *)
huffman@35514
   356
    fun prove_take_strict (take_const, dname) thy =
huffman@35514
   357
      let
huffman@35514
   358
        val goal = mk_trp (mk_strict (take_const $ Free ("i", natT)));
huffman@35514
   359
        val tac = rtac @{thm deflation_strict} 1
huffman@35514
   360
                  THEN resolve_tac deflation_take_thms 1;
huffman@35514
   361
        val take_strict_thm = Goal.prove_global thy [] [] goal (K tac);
huffman@35514
   362
      in
huffman@35514
   363
        add_qualified_thm "take_strict" (dname, take_strict_thm) thy
huffman@35514
   364
      end;
huffman@35514
   365
    val (take_strict_thms, thy) =
huffman@35514
   366
      fold_map prove_take_strict (take_consts ~~ dnames) thy;
huffman@35514
   367
huffman@35514
   368
    (* prove take/take rules *)
huffman@35514
   369
    fun prove_take_take ((chain_take, deflation_take), dname) thy =
huffman@35514
   370
      let
huffman@35514
   371
        val take_take_thm =
huffman@35514
   372
            @{thm deflation_chain_min} OF [chain_take, deflation_take];
huffman@35514
   373
      in
huffman@35514
   374
        add_qualified_thm "take_take" (dname, take_take_thm) thy
huffman@35514
   375
      end;
huffman@35514
   376
    val (take_take_thms, thy) =
huffman@35514
   377
      fold_map prove_take_take
huffman@35514
   378
        (chain_take_thms ~~ deflation_take_thms ~~ dnames) thy;
huffman@35514
   379
huffman@35515
   380
    (* define finiteness predicates *)
huffman@35515
   381
    fun define_finite_const ((tbind, take_const), (lhsT, rhsT)) thy =
huffman@35515
   382
      let
huffman@35515
   383
        val finite_type = lhsT --> boolT;
huffman@35515
   384
        val finite_bind = Binding.suffix_name "_finite" tbind;
huffman@35515
   385
        val (finite_const, thy) =
huffman@35515
   386
          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
huffman@35515
   387
        val x = Free ("x", lhsT);
huffman@35515
   388
        val i = Free ("i", natT);
huffman@35515
   389
        val finite_rhs =
huffman@35515
   390
          lambda x (HOLogic.exists_const natT $
huffman@35515
   391
            (lambda i (mk_eq (mk_capply (take_const $ i, x), x))));
huffman@35515
   392
        val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
huffman@35515
   393
        val (finite_def_thm, thy) =
huffman@35515
   394
          thy
huffman@35515
   395
          |> Sign.add_path (Binding.name_of tbind)
huffman@35515
   396
          |> yield_singleton
huffman@35515
   397
              (PureThy.add_defs false o map Thm.no_attributes)
huffman@35515
   398
              (Binding.name "finite_def", finite_eqn)
huffman@35515
   399
          ||> Sign.parent_path;
huffman@35515
   400
      in ((finite_const, finite_def_thm), thy) end;
huffman@35515
   401
    val ((finite_consts, finite_defs), thy) = thy
huffman@35515
   402
      |> fold_map define_finite_const (dom_binds ~~ take_consts ~~ dom_eqns)
huffman@35515
   403
      |>> ListPair.unzip;
huffman@35515
   404
huffman@35514
   405
    val result =
huffman@35514
   406
      {
huffman@35514
   407
        take_consts = take_consts,
huffman@35514
   408
        take_defs = take_defs,
huffman@35514
   409
        chain_take_thms = chain_take_thms,
huffman@35514
   410
        take_0_thms = take_0_thms,
huffman@35514
   411
        take_Suc_thms = take_Suc_thms,
huffman@35515
   412
        deflation_take_thms = deflation_take_thms,
huffman@35515
   413
        finite_consts = finite_consts,
huffman@35515
   414
        finite_defs = finite_defs
huffman@35514
   415
      };
huffman@35514
   416
huffman@35514
   417
  in
huffman@35514
   418
    (result, thy)
huffman@35514
   419
  end;
huffman@35514
   420
huffman@35514
   421
end;