create data structure for storing (co)datatype information

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Apr 29 17:37:00 2013 +0200
@@ -18,6 +18,8 @@
      discIs: thm list,
      sel_thmss: thm list list};
 
+  val morph_ctr_wrap_result: morphism -> ctr_wrap_result -> ctr_wrap_result
+
   val rep_compat_prefix: string
 
   val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
@@ -54,6 +56,18 @@
    discIs: thm list,
    sel_thmss: thm list list};
 
+fun morph_ctr_wrap_result phi {discs, selss, exhaust, injects, distincts, case_thms, disc_thmss,
+    discIs, sel_thmss} =
+  {discs = map (Morphism.term phi) discs,
+   selss = map (map (Morphism.term phi)) selss,
+   exhaust = Morphism.thm phi exhaust,
+   injects = map (Morphism.thm phi) injects,
+   distincts = map (Morphism.thm phi) distincts,
+   case_thms = map (Morphism.thm phi) case_thms,
+   disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
+   discIs = map (Morphism.thm phi) discIs,
+   sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
+
 val rep_compat_prefix = "new";
 
 val isN = "is_";

--- a/src/HOL/BNF/Tools/bnf_def.ML	Mon Apr 29 16:50:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Mon Apr 29 17:37:00 2013 +0200
@@ -11,6 +11,8 @@
   type BNF
   type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
 
+  val morph_bnf: morphism -> BNF -> BNF
+  val eq_bnf: BNF * BNF -> bool
   val bnf_of: Proof.context -> string -> BNF option
   val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
 

--- a/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 16:50:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Mon Apr 29 17:37:00 2013 +0200
@@ -1,6 +1,7 @@
 (*  Title:      HOL/BNF/Tools/bnf_fp.ML
     Author:     Dmitriy Traytel, TU Muenchen
-    Copyright   2012
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013
 
 Shared library for the datatype and codatatype constructions.
 *)
@@ -24,6 +25,9 @@
      fold_thms: thm list,
      rec_thms: thm list}
 
+  val morph_fp_result: morphism -> fp_result -> fp_result
+  val eq_fp_result: fp_result * fp_result -> bool
+
   val time: Timer.real_timer -> string -> Timer.real_timer
 
   val IITN: string
@@ -184,6 +188,27 @@
    fold_thms: thm list,
    rec_thms: thm list};
 
+fun morph_fp_result phi {bnfs, dtors, ctors, folds, recs, induct, strong_induct, dtor_ctors,
+    ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, fold_thms, rec_thms} =
+  {bnfs = map (morph_bnf phi) bnfs,
+   dtors = map (Morphism.term phi) dtors,
+   ctors = map (Morphism.term phi) ctors,
+   folds = map (Morphism.term phi) folds,
+   recs = map (Morphism.term phi) recs,
+   induct = Morphism.thm phi induct,
+   strong_induct = Morphism.thm phi strong_induct,
+   dtor_ctors = map (Morphism.thm phi) dtor_ctors,
+   ctor_dtors = map (Morphism.thm phi) ctor_dtors,
+   ctor_injects = map (Morphism.thm phi) ctor_injects,
+   map_thms = map (Morphism.thm phi) map_thms,
+   set_thmss = map (map (Morphism.thm phi)) set_thmss,
+   rel_thms = map (Morphism.thm phi) rel_thms,
+   fold_thms = map (Morphism.thm phi) fold_thms,
+   rec_thms = map (Morphism.thm phi) rec_thms};
+
+fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
+  eq_list eq_bnf (bnfs1, bnfs2);
+
 val timing = true;
 fun time timer msg = (if timing
   then warning (msg ^ ": " ^ ATP_Util.string_from_time (Timer.checkRealTimer timer))

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 16:50:01 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 17:37:00 2013 +0200
@@ -7,6 +7,13 @@
 
 signature BNF_FP_DEF_SUGAR =
 sig
+  type fp =
+    {fp_index: int,
+     fp_res: BNF_FP.fp_result,
+     ctr_wrap_res: BNF_Ctr_Sugar.ctr_wrap_result};
+
+  val fp_of: Proof.context -> string -> fp option
+
   val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> thm -> thm list -> thm list ->
     BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list -> typ list list list ->
     int list list -> int list -> term list list -> term list list -> term list list -> term list
@@ -25,6 +32,7 @@
     * (thm list list * thm list list) * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list * Args.src list) *
     (thm list list * thm list list * Args.src list)
+
   val datatypes: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
       binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
@@ -51,6 +59,33 @@
 
 val EqN = "Eq_";
 
+type fp =
+  {fp_index: int,
+   fp_res: fp_result,
+   ctr_wrap_res: ctr_wrap_result};
+
+fun eq_fp ({fp_index = fp_index1, fp_res = fp_res1, ...} : fp,
+    {fp_index = fp_index2, fp_res = fp_res2, ...} : fp) =
+  fp_index1 = fp_index2 andalso eq_fp_result (fp_res1, fp_res2);
+
+fun morph_fp phi {fp_index, fp_res, ctr_wrap_res} =
+  {fp_index = fp_index, fp_res = morph_fp_result phi fp_res,
+   ctr_wrap_res = morph_ctr_wrap_result phi ctr_wrap_res};
+
+structure Data = Generic_Data
+(
+  type T = fp Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  val merge = Symtab.merge eq_fp;
+);
+
+val fp_of = Symtab.lookup o Data.get o Context.Proof;
+
+fun register_fp key fp =
+  Local_Theory.declaration {syntax = false, pervasive = true}
+    (fn phi => Data.map (Symtab.update_new (key, morph_fp phi fp)));
+
 (* This function could produce clashes in contrived examples (e.g., "x.A", "x.x_A", "y.A"). *)
 fun quasi_unambiguous_case_names names =
   let