src/HOLCF/Tools/Domain/domain_take_proofs.ML
author haftmann
Wed May 05 18:25:34 2010 +0200 (2010-05-05)
changeset 36692 54b64d4ad524
parent 36241 2a4cec6bcae2
child 37078 a1656804fcad
permissions -rw-r--r--
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
     1 (*  Title:      HOLCF/Tools/domain/domain_take_proofs.ML
     2     Author:     Brian Huffman
     3 
     4 Defines take functions for the given domain equation
     5 and proves related theorems.
     6 *)
     7 
     8 signature DOMAIN_TAKE_PROOFS =
     9 sig
    10   type iso_info =
    11     {
    12       absT : typ,
    13       repT : typ,
    14       abs_const : term,
    15       rep_const : term,
    16       abs_inverse : thm,
    17       rep_inverse : thm
    18     }
    19   type take_info =
    20     {
    21       take_consts : term list,
    22       take_defs : thm list,
    23       chain_take_thms : thm list,
    24       take_0_thms : thm list,
    25       take_Suc_thms : thm list,
    26       deflation_take_thms : thm list,
    27       finite_consts : term list,
    28       finite_defs : thm list
    29     }
    30   type take_induct_info =
    31     {
    32       take_consts         : term list,
    33       take_defs           : thm list,
    34       chain_take_thms     : thm list,
    35       take_0_thms         : thm list,
    36       take_Suc_thms       : thm list,
    37       deflation_take_thms : thm list,
    38       finite_consts       : term list,
    39       finite_defs         : thm list,
    40       lub_take_thms       : thm list,
    41       reach_thms          : thm list,
    42       take_lemma_thms     : thm list,
    43       is_finite           : bool,
    44       take_induct_thms    : thm list
    45     }
    46   val define_take_functions :
    47     (binding * iso_info) list -> theory -> take_info * theory
    48 
    49   val add_lub_take_theorems :
    50     (binding * iso_info) list -> take_info -> thm list ->
    51     theory -> take_induct_info * theory
    52 
    53   val map_of_typ :
    54     theory -> (typ * term) list -> typ -> term
    55 
    56   val add_map_function :
    57     (string * string * thm) -> theory -> theory
    58 
    59   val get_map_tab : theory -> string Symtab.table
    60   val get_deflation_thms : theory -> thm list
    61 end;
    62 
    63 structure Domain_Take_Proofs : DOMAIN_TAKE_PROOFS =
    64 struct
    65 
    66 type iso_info =
    67   {
    68     absT : typ,
    69     repT : typ,
    70     abs_const : term,
    71     rep_const : term,
    72     abs_inverse : thm,
    73     rep_inverse : thm
    74   };
    75 
    76 type take_info =
    77   { take_consts : term list,
    78     take_defs : thm list,
    79     chain_take_thms : thm list,
    80     take_0_thms : thm list,
    81     take_Suc_thms : thm list,
    82     deflation_take_thms : thm list,
    83     finite_consts : term list,
    84     finite_defs : thm list
    85   };
    86 
    87 type take_induct_info =
    88   {
    89     take_consts         : term list,
    90     take_defs           : thm list,
    91     chain_take_thms     : thm list,
    92     take_0_thms         : thm list,
    93     take_Suc_thms       : thm list,
    94     deflation_take_thms : thm list,
    95     finite_consts       : term list,
    96     finite_defs         : thm list,
    97     lub_take_thms       : thm list,
    98     reach_thms          : thm list,
    99     take_lemma_thms     : thm list,
   100     is_finite           : bool,
   101     take_induct_thms    : thm list
   102   };
   103 
   104 val beta_ss =
   105   HOL_basic_ss
   106     addsimps simp_thms
   107     addsimps [@{thm beta_cfun}]
   108     addsimprocs [@{simproc cont_proc}];
   109 
   110 val beta_tac = simp_tac beta_ss;
   111 
   112 (******************************************************************************)
   113 (******************************** theory data *********************************)
   114 (******************************************************************************)
   115 
   116 structure MapData = Theory_Data
   117 (
   118   (* constant names like "foo_map" *)
   119   type T = string Symtab.table;
   120   val empty = Symtab.empty;
   121   val extend = I;
   122   fun merge data = Symtab.merge (K true) data;
   123 );
   124 
   125 structure DeflMapData = Theory_Data
   126 (
   127   (* theorems like "deflation a ==> deflation (foo_map$a)" *)
   128   type T = thm list;
   129   val empty = [];
   130   val extend = I;
   131   val merge = Thm.merge_thms;
   132 );
   133 
   134 fun add_map_function (tname, map_name, deflation_map_thm) =
   135     MapData.map (Symtab.insert (K true) (tname, map_name))
   136     #> DeflMapData.map (Thm.add_thm deflation_map_thm);
   137 
   138 val get_map_tab = MapData.get;
   139 val get_deflation_thms = DeflMapData.get;
   140 
   141 (******************************************************************************)
   142 (************************** building types and terms **************************)
   143 (******************************************************************************)
   144 
   145 open HOLCF_Library;
   146 
   147 infixr 6 ->>;
   148 infix -->>;
   149 infix 9 `;
   150 
   151 fun mapT (T as Type (_, Ts)) =
   152     (map (fn T => T ->> T) Ts) -->> (T ->> T)
   153   | mapT T = T ->> T;
   154 
   155 fun mk_deflation t =
   156   Const (@{const_name deflation}, Term.fastype_of t --> boolT) $ t;
   157 
   158 fun mk_eqs (t, u) = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u));
   159 
   160 (******************************************************************************)
   161 (****************************** isomorphism info ******************************)
   162 (******************************************************************************)
   163 
   164 fun deflation_abs_rep (info : iso_info) : thm =
   165   let
   166     val abs_iso = #abs_inverse info;
   167     val rep_iso = #rep_inverse info;
   168     val thm = @{thm deflation_abs_rep} OF [abs_iso, rep_iso];
   169   in
   170     Drule.zero_var_indexes thm
   171   end
   172 
   173 (******************************************************************************)
   174 (********************* building map functions over types **********************)
   175 (******************************************************************************)
   176 
   177 fun map_of_typ (thy : theory) (sub : (typ * term) list) (T : typ) : term =
   178   let
   179     val map_tab = get_map_tab thy;
   180     fun auto T = T ->> T;
   181     fun map_of T =
   182         case AList.lookup (op =) sub T of
   183           SOME m => (m, true) | NONE => map_of' T
   184     and map_of' (T as (Type (c, Ts))) =
   185         (case Symtab.lookup map_tab c of
   186           SOME map_name =>
   187           let
   188             val map_type = map auto Ts -->> auto T;
   189             val (ms, bs) = map_split map_of Ts;
   190           in
   191             if exists I bs
   192             then (list_ccomb (Const (map_name, map_type), ms), true)
   193             else (mk_ID T, false)
   194           end
   195         | NONE => (mk_ID T, false))
   196       | map_of' T = (mk_ID T, false);
   197   in
   198     fst (map_of T)
   199   end;
   200 
   201 
   202 (******************************************************************************)
   203 (********************* declaring definitions and theorems *********************)
   204 (******************************************************************************)
   205 
   206 fun add_qualified_def name (dbind, eqn) =
   207     yield_singleton (PureThy.add_defs false)
   208      ((Binding.qualified true name dbind, eqn), []);
   209 
   210 fun add_qualified_thm name (dbind, thm) =
   211     yield_singleton PureThy.add_thms
   212       ((Binding.qualified true name dbind, thm), []);
   213 
   214 fun add_qualified_simp_thm name (dbind, thm) =
   215     yield_singleton PureThy.add_thms
   216       ((Binding.qualified true name dbind, thm), [Simplifier.simp_add]);
   217 
   218 (******************************************************************************)
   219 (************************** defining take functions ***************************)
   220 (******************************************************************************)
   221 
   222 fun define_take_functions
   223     (spec : (binding * iso_info) list)
   224     (thy : theory) =
   225   let
   226 
   227     (* retrieve components of spec *)
   228     val dbinds = map fst spec;
   229     val iso_infos = map snd spec;
   230     val dom_eqns = map (fn x => (#absT x, #repT x)) iso_infos;
   231     val rep_abs_consts = map (fn x => (#rep_const x, #abs_const x)) iso_infos;
   232 
   233     (* get table of map functions *)
   234     val map_tab = MapData.get thy;
   235 
   236     fun mk_projs []      t = []
   237       | mk_projs (x::[]) t = [(x, t)]
   238       | mk_projs (x::xs) t = (x, mk_fst t) :: mk_projs xs (mk_snd t);
   239 
   240     fun mk_cfcomp2 ((rep_const, abs_const), f) =
   241         mk_cfcomp (abs_const, mk_cfcomp (f, rep_const));
   242 
   243     (* define take functional *)
   244     val newTs : typ list = map fst dom_eqns;
   245     val copy_arg_type = mk_tupleT (map (fn T => T ->> T) newTs);
   246     val copy_arg = Free ("f", copy_arg_type);
   247     val copy_args = map snd (mk_projs dbinds copy_arg);
   248     fun one_copy_rhs (rep_abs, (lhsT, rhsT)) =
   249       let
   250         val body = map_of_typ thy (newTs ~~ copy_args) rhsT;
   251       in
   252         mk_cfcomp2 (rep_abs, body)
   253       end;
   254     val take_functional =
   255         big_lambda copy_arg
   256           (mk_tuple (map one_copy_rhs (rep_abs_consts ~~ dom_eqns)));
   257     val take_rhss =
   258       let
   259         val n = Free ("n", HOLogic.natT);
   260         val rhs = mk_iterate (n, take_functional);
   261       in
   262         map (lambda n o snd) (mk_projs dbinds rhs)
   263       end;
   264 
   265     (* define take constants *)
   266     fun define_take_const ((dbind, take_rhs), (lhsT, rhsT)) thy =
   267       let
   268         val take_type = HOLogic.natT --> lhsT ->> lhsT;
   269         val take_bind = Binding.suffix_name "_take" dbind;
   270         val (take_const, thy) =
   271           Sign.declare_const ((take_bind, take_type), NoSyn) thy;
   272         val take_eqn = Logic.mk_equals (take_const, take_rhs);
   273         val (take_def_thm, thy) =
   274             add_qualified_def "take_def" (dbind, take_eqn) thy;
   275       in ((take_const, take_def_thm), thy) end;
   276     val ((take_consts, take_defs), thy) = thy
   277       |> fold_map define_take_const (dbinds ~~ take_rhss ~~ dom_eqns)
   278       |>> ListPair.unzip;
   279 
   280     (* prove chain_take lemmas *)
   281     fun prove_chain_take (take_const, dbind) thy =
   282       let
   283         val goal = mk_trp (mk_chain take_const);
   284         val rules = take_defs @ @{thms chain_iterate ch2ch_fst ch2ch_snd};
   285         val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   286         val thm = Goal.prove_global thy [] [] goal (K tac);
   287       in
   288         add_qualified_simp_thm "chain_take" (dbind, thm) thy
   289       end;
   290     val (chain_take_thms, thy) =
   291       fold_map prove_chain_take (take_consts ~~ dbinds) thy;
   292 
   293     (* prove take_0 lemmas *)
   294     fun prove_take_0 ((take_const, dbind), (lhsT, rhsT)) thy =
   295       let
   296         val lhs = take_const $ @{term "0::nat"};
   297         val goal = mk_eqs (lhs, mk_bottom (lhsT ->> lhsT));
   298         val rules = take_defs @ @{thms iterate_0 fst_strict snd_strict};
   299         val tac = simp_tac (HOL_basic_ss addsimps rules) 1;
   300         val take_0_thm = Goal.prove_global thy [] [] goal (K tac);
   301       in
   302         add_qualified_thm "take_0" (dbind, take_0_thm) thy
   303       end;
   304     val (take_0_thms, thy) =
   305       fold_map prove_take_0 (take_consts ~~ dbinds ~~ dom_eqns) thy;
   306 
   307     (* prove take_Suc lemmas *)
   308     val n = Free ("n", natT);
   309     val take_is = map (fn t => t $ n) take_consts;
   310     fun prove_take_Suc
   311           (((take_const, rep_abs), dbind), (lhsT, rhsT)) thy =
   312       let
   313         val lhs = take_const $ (@{term Suc} $ n);
   314         val body = map_of_typ thy (newTs ~~ take_is) rhsT;
   315         val rhs = mk_cfcomp2 (rep_abs, body);
   316         val goal = mk_eqs (lhs, rhs);
   317         val simps = @{thms iterate_Suc fst_conv snd_conv}
   318         val rules = take_defs @ simps;
   319         val tac = simp_tac (beta_ss addsimps rules) 1;
   320         val take_Suc_thm = Goal.prove_global thy [] [] goal (K tac);
   321       in
   322         add_qualified_thm "take_Suc" (dbind, take_Suc_thm) thy
   323       end;
   324     val (take_Suc_thms, thy) =
   325       fold_map prove_take_Suc
   326         (take_consts ~~ rep_abs_consts ~~ dbinds ~~ dom_eqns) thy;
   327 
   328     (* prove deflation theorems for take functions *)
   329     val deflation_abs_rep_thms = map deflation_abs_rep iso_infos;
   330     val deflation_take_thm =
   331       let
   332         val n = Free ("n", natT);
   333         fun mk_goal take_const = mk_deflation (take_const $ n);
   334         val goal = mk_trp (foldr1 mk_conj (map mk_goal take_consts));
   335         val adm_rules =
   336           @{thms adm_conj adm_subst [OF _ adm_deflation]
   337                  cont2cont_fst cont2cont_snd cont_id};
   338         val bottom_rules =
   339           take_0_thms @ @{thms deflation_UU simp_thms};
   340         val deflation_rules =
   341           @{thms conjI deflation_ID}
   342           @ deflation_abs_rep_thms
   343           @ DeflMapData.get thy;
   344       in
   345         Goal.prove_global thy [] [] goal (fn _ =>
   346          EVERY
   347           [rtac @{thm nat.induct} 1,
   348            simp_tac (HOL_basic_ss addsimps bottom_rules) 1,
   349            asm_simp_tac (HOL_basic_ss addsimps take_Suc_thms) 1,
   350            REPEAT (etac @{thm conjE} 1
   351                    ORELSE resolve_tac deflation_rules 1
   352                    ORELSE atac 1)])
   353       end;
   354     fun conjuncts [] thm = []
   355       | conjuncts (n::[]) thm = [(n, thm)]
   356       | conjuncts (n::ns) thm = let
   357           val thmL = thm RS @{thm conjunct1};
   358           val thmR = thm RS @{thm conjunct2};
   359         in (n, thmL):: conjuncts ns thmR end;
   360     val (deflation_take_thms, thy) =
   361       fold_map (add_qualified_thm "deflation_take")
   362         (map (apsnd Drule.zero_var_indexes)
   363           (conjuncts dbinds deflation_take_thm)) thy;
   364 
   365     (* prove strictness of take functions *)
   366     fun prove_take_strict (deflation_take, dbind) thy =
   367       let
   368         val take_strict_thm =
   369             Drule.zero_var_indexes
   370               (@{thm deflation_strict} OF [deflation_take]);
   371       in
   372         add_qualified_thm "take_strict" (dbind, take_strict_thm) thy
   373       end;
   374     val (take_strict_thms, thy) =
   375       fold_map prove_take_strict
   376         (deflation_take_thms ~~ dbinds) thy;
   377 
   378     (* prove take/take rules *)
   379     fun prove_take_take ((chain_take, deflation_take), dbind) thy =
   380       let
   381         val take_take_thm =
   382             Drule.zero_var_indexes
   383               (@{thm deflation_chain_min} OF [chain_take, deflation_take]);
   384       in
   385         add_qualified_thm "take_take" (dbind, take_take_thm) thy
   386       end;
   387     val (take_take_thms, thy) =
   388       fold_map prove_take_take
   389         (chain_take_thms ~~ deflation_take_thms ~~ dbinds) thy;
   390 
   391     (* prove take_below rules *)
   392     fun prove_take_below (deflation_take, dbind) thy =
   393       let
   394         val take_below_thm =
   395             Drule.zero_var_indexes
   396               (@{thm deflation.below} OF [deflation_take]);
   397       in
   398         add_qualified_thm "take_below" (dbind, take_below_thm) thy
   399       end;
   400     val (take_below_thms, thy) =
   401       fold_map prove_take_below
   402         (deflation_take_thms ~~ dbinds) thy;
   403 
   404     (* define finiteness predicates *)
   405     fun define_finite_const ((dbind, take_const), (lhsT, rhsT)) thy =
   406       let
   407         val finite_type = lhsT --> boolT;
   408         val finite_bind = Binding.suffix_name "_finite" dbind;
   409         val (finite_const, thy) =
   410           Sign.declare_const ((finite_bind, finite_type), NoSyn) thy;
   411         val x = Free ("x", lhsT);
   412         val n = Free ("n", natT);
   413         val finite_rhs =
   414           lambda x (HOLogic.exists_const natT $
   415             (lambda n (mk_eq (mk_capply (take_const $ n, x), x))));
   416         val finite_eqn = Logic.mk_equals (finite_const, finite_rhs);
   417         val (finite_def_thm, thy) =
   418             add_qualified_def "finite_def" (dbind, finite_eqn) thy;
   419       in ((finite_const, finite_def_thm), thy) end;
   420     val ((finite_consts, finite_defs), thy) = thy
   421       |> fold_map define_finite_const (dbinds ~~ take_consts ~~ dom_eqns)
   422       |>> ListPair.unzip;
   423 
   424     val result =
   425       {
   426         take_consts = take_consts,
   427         take_defs = take_defs,
   428         chain_take_thms = chain_take_thms,
   429         take_0_thms = take_0_thms,
   430         take_Suc_thms = take_Suc_thms,
   431         deflation_take_thms = deflation_take_thms,
   432         finite_consts = finite_consts,
   433         finite_defs = finite_defs
   434       };
   435 
   436   in
   437     (result, thy)
   438   end;
   439 
   440 fun prove_finite_take_induct
   441     (spec : (binding * iso_info) list)
   442     (take_info : take_info)
   443     (lub_take_thms : thm list)
   444     (thy : theory) =
   445   let
   446     val dbinds = map fst spec;
   447     val iso_infos = map snd spec;
   448     val absTs = map #absT iso_infos;
   449     val {take_consts, ...} = take_info;
   450     val {chain_take_thms, take_0_thms, take_Suc_thms, ...} = take_info;
   451     val {finite_consts, finite_defs, ...} = take_info;
   452 
   453     val decisive_lemma =
   454       let
   455         fun iso_locale info =
   456             @{thm iso.intro} OF [#abs_inverse info, #rep_inverse info];
   457         val iso_locale_thms = map iso_locale iso_infos;
   458         val decisive_abs_rep_thms =
   459             map (fn x => @{thm decisive_abs_rep} OF [x]) iso_locale_thms;
   460         val n = Free ("n", @{typ nat});
   461         fun mk_decisive t =
   462             Const (@{const_name decisive}, fastype_of t --> boolT) $ t;
   463         fun f take_const = mk_decisive (take_const $ n);
   464         val goal = mk_trp (foldr1 mk_conj (map f take_consts));
   465         val rules0 = @{thm decisive_bottom} :: take_0_thms;
   466         val rules1 =
   467             take_Suc_thms @ decisive_abs_rep_thms
   468             @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map};
   469         val tac = EVERY [
   470             rtac @{thm nat.induct} 1,
   471             simp_tac (HOL_ss addsimps rules0) 1,
   472             asm_simp_tac (HOL_ss addsimps rules1) 1];
   473       in Goal.prove_global thy [] [] goal (K tac) end;
   474     fun conjuncts 1 thm = [thm]
   475       | conjuncts n thm = let
   476           val thmL = thm RS @{thm conjunct1};
   477           val thmR = thm RS @{thm conjunct2};
   478         in thmL :: conjuncts (n-1) thmR end;
   479     val decisive_thms = conjuncts (length spec) decisive_lemma;
   480 
   481     fun prove_finite_thm (absT, finite_const) =
   482       let
   483         val goal = mk_trp (finite_const $ Free ("x", absT));
   484         val tac =
   485             EVERY [
   486             rewrite_goals_tac finite_defs,
   487             rtac @{thm lub_ID_finite} 1,
   488             resolve_tac chain_take_thms 1,
   489             resolve_tac lub_take_thms 1,
   490             resolve_tac decisive_thms 1];
   491       in
   492         Goal.prove_global thy [] [] goal (K tac)
   493       end;
   494     val finite_thms =
   495         map prove_finite_thm (absTs ~~ finite_consts);
   496 
   497     fun prove_take_induct ((ch_take, lub_take), decisive) =
   498         Drule.export_without_context
   499           (@{thm lub_ID_finite_take_induct} OF [ch_take, lub_take, decisive]);
   500     val take_induct_thms =
   501         map prove_take_induct
   502           (chain_take_thms ~~ lub_take_thms ~~ decisive_thms);
   503 
   504     val thy = thy
   505         |> fold (snd oo add_qualified_thm "finite")
   506             (dbinds ~~ finite_thms)
   507         |> fold (snd oo add_qualified_thm "take_induct")
   508             (dbinds ~~ take_induct_thms);
   509   in
   510     ((finite_thms, take_induct_thms), thy)
   511   end;
   512 
   513 fun add_lub_take_theorems
   514     (spec : (binding * iso_info) list)
   515     (take_info : take_info)
   516     (lub_take_thms : thm list)
   517     (thy : theory) =
   518   let
   519 
   520     (* retrieve components of spec *)
   521     val dbinds = map fst spec;
   522     val iso_infos = map snd spec;
   523     val absTs = map #absT iso_infos;
   524     val repTs = map #repT iso_infos;
   525     val {take_consts, take_0_thms, take_Suc_thms, ...} = take_info;
   526     val {chain_take_thms, deflation_take_thms, ...} = take_info;
   527 
   528     (* prove take lemmas *)
   529     fun prove_take_lemma ((chain_take, lub_take), dbind) thy =
   530       let
   531         val take_lemma =
   532             Drule.export_without_context
   533               (@{thm lub_ID_take_lemma} OF [chain_take, lub_take]);
   534       in
   535         add_qualified_thm "take_lemma" (dbind, take_lemma) thy
   536       end;
   537     val (take_lemma_thms, thy) =
   538       fold_map prove_take_lemma
   539         (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
   540 
   541     (* prove reach lemmas *)
   542     fun prove_reach_lemma ((chain_take, lub_take), dbind) thy =
   543       let
   544         val thm =
   545             Drule.zero_var_indexes
   546               (@{thm lub_ID_reach} OF [chain_take, lub_take]);
   547       in
   548         add_qualified_thm "reach" (dbind, thm) thy
   549       end;
   550     val (reach_thms, thy) =
   551       fold_map prove_reach_lemma
   552         (chain_take_thms ~~ lub_take_thms ~~ dbinds) thy;
   553 
   554     (* test for finiteness of domain definitions *)
   555     local
   556       val types = [@{type_name ssum}, @{type_name sprod}];
   557       fun finite d T = if member (op =) absTs T then d else finite' d T
   558       and finite' d (Type (c, Ts)) =
   559           let val d' = d andalso member (op =) types c;
   560           in forall (finite d') Ts end
   561         | finite' d _ = true;
   562     in
   563       val is_finite = forall (finite true) repTs;
   564     end;
   565 
   566     val ((finite_thms, take_induct_thms), thy) =
   567       if is_finite
   568       then
   569         let
   570           val ((finites, take_inducts), thy) =
   571               prove_finite_take_induct spec take_info lub_take_thms thy;
   572         in
   573           ((SOME finites, take_inducts), thy)
   574         end
   575       else
   576         let
   577           fun prove_take_induct (chain_take, lub_take) =
   578               Drule.zero_var_indexes
   579                 (@{thm lub_ID_take_induct} OF [chain_take, lub_take]);
   580           val take_inducts =
   581               map prove_take_induct (chain_take_thms ~~ lub_take_thms);
   582           val thy = fold (snd oo add_qualified_thm "take_induct")
   583                          (dbinds ~~ take_inducts) thy;
   584         in
   585           ((NONE, take_inducts), thy)
   586         end;
   587 
   588     val result =
   589       {
   590         take_consts         = #take_consts take_info,
   591         take_defs           = #take_defs take_info,
   592         chain_take_thms     = #chain_take_thms take_info,
   593         take_0_thms         = #take_0_thms take_info,
   594         take_Suc_thms       = #take_Suc_thms take_info,
   595         deflation_take_thms = #deflation_take_thms take_info,
   596         finite_consts       = #finite_consts take_info,
   597         finite_defs         = #finite_defs take_info,
   598         lub_take_thms       = lub_take_thms,
   599         reach_thms          = reach_thms,
   600         take_lemma_thms     = take_lemma_thms,
   601         is_finite           = is_finite,
   602         take_induct_thms    = take_induct_thms
   603       };
   604   in
   605     (result, thy)
   606   end;
   607 
   608 end;