enriched data structure with necessary theorems

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
@@ -23,7 +23,11 @@
      split_asm: thm,
      disc_thmss: thm list list,
      discIs: thm list,
-     sel_thmss: thm list list};
+     sel_thmss: thm list list,
+     disc_exhausts: thm list,
+     collapses: thm list,
+     expands: thm list,
+     case_convs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
 
@@ -68,10 +72,15 @@
    split_asm: thm,
    disc_thmss: thm list list,
    discIs: thm list,
-   sel_thmss: thm list list};
+   sel_thmss: thm list list,
+   disc_exhausts: thm list,
+   collapses: thm list,
+   expands: thm list,
+   case_convs: thm list};
 
 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
-    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss} =
+    case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
+    disc_exhausts, collapses, expands, case_convs} =
   {ctrs = map (Morphism.term phi) ctrs,
    casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
@@ -87,7 +96,11 @@
    split_asm = Morphism.thm phi split_asm,
    disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    discIs = map (Morphism.thm phi) discIs,
-   sel_thmss = map (map (Morphism.thm phi)) sel_thmss};
+   sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
+   disc_exhausts = map (Morphism.thm phi) disc_exhausts,
+   collapses = map (Morphism.thm phi) collapses,
+   expands = map (Morphism.thm phi) expands,
+   case_convs = map (Morphism.thm phi) case_convs};
 
 val rep_compat_prefix = "new";
 
@@ -762,7 +775,8 @@
           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
-          discIs = discI_thms, sel_thmss = sel_thmss},
+          discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+          collapses = collapse_thms, expands = expand_thms, case_convs = case_conv_thms},
          lthy
          |> not rep_compat ?
             (Local_Theory.declaration {syntax = false, pervasive = true}

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
@@ -19,7 +19,9 @@
      ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list,
      co_iterss: term list list,
      co_inducts: thm list,
-     co_iter_thmsss: thm list list list};
+     co_iter_thmsss: thm list list list,
+     disc_co_itersss: thm list list list,
+     sel_co_iterssss: thm list list list list};
 
   val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
   val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
@@ -80,7 +82,7 @@
     * (thm list list * thm list list * Args.src list)
     * (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)
+    * (thm list list list * thm list list list * Args.src list)
 
   val co_datatypes: BNF_FP_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list list -> binding list -> (string * sort) list -> typ list * typ list list ->
@@ -119,7 +121,9 @@
    ctr_sugars: ctr_sugar list,
    co_iterss: term list list,
    co_inducts: thm list,
-   co_iter_thmsss: thm list list list};
+   co_iter_thmsss: thm list list list,
+   disc_co_itersss: thm list list list,
+   sel_co_iterssss: thm list list list list};
 
 fun of_fp_sugar f (fp_sugar as {index, ...}) = nth (f fp_sugar) index;
 
@@ -128,7 +132,7 @@
   T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
 
 fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
-    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss} =
+    ctr_sugars, co_iterss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} =
   {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs,
     nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
    fp_res = morph_fp_result phi fp_res,
@@ -136,7 +140,9 @@
    ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars,
    co_iterss = map (map (Morphism.term phi)) co_iterss,
    co_inducts = map (Morphism.thm phi) co_inducts,
-   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss};
+   co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss,
+   disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss,
+   sel_co_iterssss = map (map (map (map (Morphism.thm phi)))) sel_co_iterssss};
 
 structure Data = Generic_Data
 (
@@ -161,13 +167,14 @@
     (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar)));
 
 fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss
-    ctr_sugars co_iterss co_inducts co_iter_thmsss lthy =
+    ctr_sugars co_iterss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy =
   (0, lthy)
   |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1,
     register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs,
         nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res,
         ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss,
-        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss}
+        co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss,
+        sel_co_iterssss = sel_co_iterssss}
       lthy)) Ts
   |> snd;
 
@@ -999,10 +1006,10 @@
       end;
 
     fun mk_sel_coiter_thms coiter_thmss =
-      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss |> map flat;
+      map3 (map3 (map2 o mk_sel_coiter_thm)) coiter_thmss selsss sel_thmsss;
 
-    val sel_unfold_thmss = mk_sel_coiter_thms unfold_thmss;
-    val sel_corec_thmss = mk_sel_coiter_thms corec_thmss;
+    val sel_unfold_thmsss = mk_sel_coiter_thms unfold_thmss;
+    val sel_corec_thmsss = mk_sel_coiter_thms corec_thmss;
 
     val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
     val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));
@@ -1018,7 +1025,7 @@
      (safe_unfold_thmss, safe_corec_thmss),
      (disc_unfold_thmss, disc_corec_thmss, simp_attrs),
      (disc_unfold_iff_thmss, disc_corec_iff_thmss, simp_attrs),
-     (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
+     (sel_unfold_thmsss, sel_corec_thmsss, simp_attrs))
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
@@ -1435,7 +1442,7 @@
         lthy
         |> Local_Theory.notes (common_notes @ notes) |> snd
         |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars
-          iterss [induct_thm] (transpose [fold_thmss, rec_thmss])
+          iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] []
       end;
 
     fun derive_and_note_coinduct_coiters_thms_for_types
@@ -1448,11 +1455,14 @@
              (safe_unfold_thmss, safe_corec_thmss),
              (disc_unfold_thmss, disc_corec_thmss, disc_coiter_attrs),
              (disc_unfold_iff_thmss, disc_corec_iff_thmss, disc_coiter_iff_attrs),
-             (sel_unfold_thmss, sel_corec_thmss, sel_coiter_attrs)) =
+             (sel_unfold_thmsss, sel_corec_thmsss, sel_coiter_attrs)) =
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars coiterss coiter_defss (Proof_Context.export lthy' no_defs_lthy) lthy;
 
+        val sel_unfold_thmss = map flat sel_unfold_thmsss;
+        val sel_corec_thmss = map flat sel_corec_thmsss;
+
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
 
         fun flat_coiter_thms coiters disc_coiters sel_coiters =
@@ -1495,7 +1505,8 @@
         |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
         |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss
           ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm]
-          (transpose [unfold_thmss, corec_thmss])
+          (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss])
+          (transpose [sel_unfold_thmsss, sel_corec_thmsss])
       end;
 
     val lthy'' = lthy'

--- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Sun Sep 08 19:25:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML	Mon Sep 09 13:47:58 2013 +0200
@@ -145,19 +145,23 @@
 
       val ctr_sugars = map inst_ctr_sugar ctr_sugars0;
 
-      val (co_inducts, un_fold_thmss, co_rec_thmss) =
+      val (co_inducts, un_fold_thmss, co_rec_thmss, disc_unfold_thmss, disc_corec_thmss,
+           sel_unfold_thmsss, sel_corec_thmsss) =
         if fp = Least_FP then
           derive_induct_iters_thms_for_types pre_bnfs (the iters_args_types) xtor_co_induct
             xtor_co_iter_thmss nesting_bnfs nested_bnfs fpTs Cs Xs ctrXs_Tsss ctrss ctr_defss
             co_iterss co_iter_defss lthy
           |> (fn ((_, induct, _), (fold_thmss, _), (rec_thmss, _)) =>
-            ([induct], fold_thmss, rec_thmss))
+            ([induct], fold_thmss, rec_thmss, [], [], [], []))
         else
           derive_coinduct_coiters_thms_for_types pre_bnfs (the coiters_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_iter_thmss nesting_bnfs fpTs Cs kss mss ns ctr_defss
             ctr_sugars co_iterss co_iter_defss (Proof_Context.export lthy no_defs_lthy) lthy
-          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _, _, _) =>
-            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss));
+          |> (fn ((coinduct_thms_pairs, _), (unfold_thmss, corec_thmss, _), _, _,
+                  (disc_unfold_thmss, disc_corec_thmss, _),
+                  (sel_unfold_thmsss, sel_corec_thmsss, _)) =>
+            (map snd coinduct_thms_pairs, unfold_thmss, corec_thmss, disc_unfold_thmss,
+             disc_corec_thmss, sel_unfold_thmsss, sel_corec_thmsss));
 
       val phi = Proof_Context.export_morphism no_defs_lthy no_defs_lthy0;
 
@@ -165,7 +169,9 @@
         {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs,
          nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss,
          ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss,
-         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss]}
+         co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss],
+         disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss],
+         sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]}
         |> morph_fp_sugar phi;
     in
       ((true, map_index mk_target_fp_sugar fpTs), lthy)

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Sun Sep 08 19:25:06 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Sep 09 13:47:58 2013 +0200
@@ -31,7 +31,10 @@
      sels: term list,
      pred: int option,
      calls: corec_call list,
-     corec_thm: thm}
+     collapse: thm,
+     corec_thm: thm,
+     disc_corec: thm,
+     sel_corecs: thm list}
 
   type rec_spec =
     {recx: term,
@@ -41,6 +44,9 @@
 
   type corec_spec =
     {corec: term,
+     nested_maps: thm list,
+     nested_map_idents: thm list,
+     nested_map_comps: thm list,
      ctr_specs: corec_ctr_spec list}
 
   val massage_indirect_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
@@ -90,7 +96,10 @@
    sels: term list,
    pred: int option,
    calls: corec_call list,
-   corec_thm: thm};
+   collapse: thm,
+   corec_thm: thm,
+   disc_corec: thm,
+   sel_corecs: thm list};
 
 type rec_spec =
   {recx: term,
@@ -100,6 +109,9 @@
 
 type corec_spec =
   {corec: term,
+   nested_maps: thm list,
+   nested_map_idents: thm list,
+   nested_map_comps: thm list,
    ctr_specs: corec_ctr_spec list};
 
 val id_def = @{thm id_def};
@@ -348,7 +360,7 @@
     val thy = Proof_Context.theory_of lthy;
 
     val ((nontriv, missing_res_Ts, perm0_kks,
-          fp_sugars as {fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
+          fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...},
           co_inducts = coinduct_thms, ...} :: _), lthy') =
       nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy;
 
@@ -407,27 +419,38 @@
          else No_Corec) g_i
       | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
 
-    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss corec_thm =
+    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
       let val nullary = not (can dest_funT (fastype_of ctr)) in
         {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
-         calls = map3 (call_of nullary) q_iss f_iss f_Tss, corec_thm = corec_thm}
+         calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
+         corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs}
       end;
 
-    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss =
+    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
+        sel_coiterssss =
       let
         val ctrs = #ctrs (nth ctr_sugars index);
         val discs = #discs (nth ctr_sugars index);
         val selss = #selss (nth ctr_sugars index);
         val p_ios = map SOME p_is @ [NONE];
-        val corec_thmss = co_rec_of (nth coiter_thmsss index);
+        val collapses = #collapses (nth ctr_sugars index);
+        val corec_thms = co_rec_of (nth coiter_thmsss index);
+        val disc_corecs = co_rec_of (nth disc_coitersss index);
+        val sel_corecss = co_rec_of (nth sel_coiterssss index);
       in
-        map8 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss corec_thmss
+        map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
+          disc_corecs sel_corecss
       end;
 
-    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, ...}
+    fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
+          disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...}
         p_is q_isss f_isss f_Tsss =
       {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)),
-       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss};
+       nested_maps = [] (*FIXME*),
+       nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs,
+       nested_map_comps = map map_comp_of_bnf nested_bnfs,
+       ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss
+         disc_coitersss sel_coiterssss};
   in
     ((nontriv, map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
       co_induct_of coinduct_thms, strong_co_induct_of coinduct_thms, co_induct_of coinduct_thmss,