# HG changeset patch
# User traytel
# Date 1377163814 -7200
# Node ID 4ef7d52cc5a0c7afbcd4da462c6345b4ed9193cc
# Parent  a33298b49d9fbab6e73f5455b1f80aca984e35af
store theorem about composition of fold and map in fp_result

diff -r a33298b49d9f -r 4ef7d52cc5a0 src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 22 11:30:14 2013 +0200
@@ -25,6 +25,7 @@
      xtor_set_thmss: thm list list,
      xtor_rel_thms: thm list,
      xtor_co_iter_thmss: thm list list,
+     xtor_co_iter_o_map_thmss: thm list list,
      rel_co_induct_thm: thm}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
@@ -211,11 +212,12 @@
    xtor_set_thmss: thm list list,
    xtor_rel_thms: thm list,
    xtor_co_iter_thmss: thm list list,
+   xtor_co_iter_o_map_thmss: thm list list,
    rel_co_induct_thm: thm};
 
 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_iterss, xtor_co_induct, dtor_ctors,
     ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms, xtor_co_iter_thmss,
-    rel_co_induct_thm} =
+    xtor_co_iter_o_map_thmss, rel_co_induct_thm} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
@@ -229,6 +231,7 @@
    xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss,
    xtor_rel_thms = map (Morphism.thm phi) xtor_rel_thms,
    xtor_co_iter_thmss = map (map (Morphism.thm phi)) xtor_co_iter_thmss,
+   xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
    rel_co_induct_thm = Morphism.thm phi rel_co_induct_thm};
 
 fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
diff -r a33298b49d9f -r 4ef7d52cc5a0 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 22 11:30:14 2013 +0200
@@ -2902,6 +2902,7 @@
       xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
       xtor_rel_thms = dtor_Jrel_thms,
       xtor_co_iter_thmss = transpose [ctor_dtor_unfold_thms, ctor_dtor_corec_thms],
+      xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms],
       rel_co_induct_thm = Jrel_coinduct_thm},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
diff -r a33298b49d9f -r 4ef7d52cc5a0 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 22 08:42:27 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 22 11:30:14 2013 +0200
@@ -1862,6 +1862,7 @@
       ctor_injects = ctor_inject_thms, xtor_map_thms = folded_ctor_map_thms,
       xtor_set_thmss = folded_ctor_set_thmss', xtor_rel_thms = ctor_Irel_thms,
       xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
+      xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms],
       rel_co_induct_thm = Irel_induct_thm},
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;