theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map

--- a/src/HOL/BNF/BNF_FP_Basic.thy	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy	Thu Aug 08 16:38:28 2013 +0200
@@ -113,6 +113,36 @@
 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
 by blast
 
+lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
+  unfolding o_def fun_eq_iff by auto
+
+lemma convol_o: "<f, g> o h = <f o h, g o h>"
+  unfolding convol_def by auto
+
+lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
+  unfolding convol_def by auto
+
+lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
+  unfolding map_pair_o_convol id_o o_id ..
+
+lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
+  unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
+  unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
+  unfolding sum_case_o_sum_map id_o o_id ..
+
 lemma fun_rel_def_butlast:
   "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
   unfolding fun_rel_def ..

--- a/src/HOL/BNF/BNF_GFP.thy	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Thu Aug 08 16:38:28 2013 +0200
@@ -13,9 +13,6 @@
   "codatatype" :: thy_decl
 begin
 
-lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
-unfolding o_def by (auto split: sum.splits)
-
 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
 by (auto split: sum.splits)
 

--- a/src/HOL/BNF/BNF_LFP.thy	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Thu Aug 08 16:38:28 2013 +0200
@@ -44,9 +44,6 @@
 lemma snd_convol': "snd (<f, g> x) = g x"
 using snd_convol unfolding convol_def by simp
 
-lemma convol_o: "<f, g> o h = <f o h, g o h>"
-  unfolding convol_def by auto
-
 lemma convol_expand_snd: "fst o f = g \<Longrightarrow>  <g, snd o f> = f"
 unfolding convol_def by auto
 

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 08 16:38:28 2013 +0200
@@ -9,6 +9,7 @@
 signature BNF_FP_UTIL =
 sig
   datatype fp_kind = Least_FP | Greatest_FP
+  val fp_case: fp_kind -> 'a -> 'a -> 'a
 
   type fp_result =
     {Ts: typ list,
@@ -54,11 +55,13 @@
   val ctor_inductN: string
   val ctor_injectN: string
   val ctor_foldN: string
+  val ctor_fold_o_mapN: string
+  val ctor_fold_transferN: string
   val ctor_fold_uniqueN: string
-  val ctor_fold_transferN: string
   val ctor_mapN: string
   val ctor_map_uniqueN: string
   val ctor_recN: string
+  val ctor_rec_o_mapN: string
   val ctor_rec_uniqueN: string
   val ctor_relN: string
   val ctor_set_inclN: string
@@ -70,6 +73,7 @@
   val dtorN: string
   val dtor_coinductN: string
   val dtor_corecN: string
+  val dtor_corec_o_mapN: string
   val dtor_corec_uniqueN: string
   val dtor_ctorN: string
   val dtor_exhaustN: string
@@ -83,8 +87,9 @@
   val dtor_set_set_inclN: string
   val dtor_strong_coinductN: string
   val dtor_unfoldN: string
+  val dtor_unfold_o_mapN: string
+  val dtor_unfold_transferN: string
   val dtor_unfold_uniqueN: string
-  val dtor_unfold_transferN: string
   val exhaustN: string
   val foldN: string
   val hsetN: string
@@ -175,6 +180,8 @@
   val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list ->
     term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
     Proof.context -> thm list
+  val mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list ->
+    thm list -> thm list -> thm list
 
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> 'a) ->
@@ -190,6 +197,8 @@
 open BNF_Util
 
 datatype fp_kind = Least_FP | Greatest_FP;
+fun fp_case Least_FP f1 _ = f1
+  | fp_case Greatest_FP _ f2 = f2;
 
 type fp_result =
   {Ts: typ list,
@@ -256,7 +265,9 @@
 val ctor_foldN = ctorN ^ "_" ^ foldN
 val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
 val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
+val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN
 val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
+val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN
 val ctor_fold_transferN = ctor_foldN ^ transferN
 val dtor_unfold_transferN = dtor_unfoldN ^ transferN
 val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
@@ -287,8 +298,10 @@
 val recN = "rec"
 val corecN = coN ^ recN
 val ctor_recN = ctorN ^ "_" ^ recN
+val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN
 val ctor_rec_uniqueN = ctor_recN ^ uniqueN
 val dtor_corecN = dtorN ^ "_" ^ corecN
+val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
 val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
 val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN
 
@@ -516,6 +529,37 @@
     |> split_conj_thm
   end;
 
+fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps
+    map_cong0s =
+  let
+    val n = length sym_map_comps;
+    val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2};
+    val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp};
+    val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_o} @{thm o_id} RS fun_cong);
+    val map_cong_active_args1 = replicate n (if is_rec
+      then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong
+      else refl);
+    val map_cong_passive_args2 = replicate m (fp_case fp @{thm o_id} @{thm id_o} RS fun_cong);
+    val map_cong_active_args2 = replicate n (if is_rec
+      then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id}
+      else fp_case fp @{thm id_o} @{thm o_id} RS fun_cong);
+    fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s;
+    val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
+    val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
+    
+    fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong =>
+      mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs;
+    val rewrite1s = mk_rewrites map_cong1s;
+    val rewrite2s = mk_rewrites map_cong2s;
+    val unique_prems =
+      map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 =>
+        mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold])
+          (mk_trans rewrite1 (mk_sym rewrite2)))
+      xtor_maps xtor_un_folds rewrite1s rewrite2s;
+  in
+    split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems)
+  end;
+
 fun fp_bnf construct_fp bs resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 08 16:38:28 2013 +0200
@@ -2003,8 +2003,8 @@
           |> Thm.close_derivation
       end;
 
-    val dtor_corec_unique_thms =
-      split_conj_thm (split_conj_prems n
+    val (dtor_corec_unique_thms, dtor_corec_unique_thm) =
+      `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
@@ -2131,10 +2131,11 @@
     val in_rels = map in_rel_of_bnf bnfs;
 
     (*register new codatatypes as BNFs*)
-    val (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms,
-      dtor_Jrel_thms, lthy) =
+    val (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss',
+      dtor_set_induct_thms, dtor_Jrel_thms, lthy) =
       if m = 0 then
-        (timer, replicate n DEADID_bnf, map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's,
+        (timer, replicate n DEADID_bnf,
+        map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's),
         replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -2725,6 +2726,7 @@
         val in_Jrels = map in_rel_of_bnf Jbnfs;
 
         val folded_dtor_map_thms = map fold_maps dtor_map_thms;
+        val folded_dtor_map_o_thms = map fold_maps map_thms;
         val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
         val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss;
 
@@ -2767,10 +2769,18 @@
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-       (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms,
-          dtor_Jrel_thms, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
+       (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss',
+         dtor_set_induct_thms, dtor_Jrel_thms,
+         lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
       end;
 
+      val dtor_unfold_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
+        dtor_unfold_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
+        sym_map_comps map_cong0s;
+      val dtor_corec_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
+        dtor_corec_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
+        sym_map_comps map_cong0s;
+
       val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs;
       val zip_ranTs = passiveABs @ prodTsTs';
       val allJphis = Jphis @ activeJphis;
@@ -2906,7 +2916,9 @@
         (dtor_injectN, dtor_inject_thms),
         (dtor_unfoldN, dtor_unfold_thms),
         (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
-        (dtor_corec_uniqueN, dtor_corec_unique_thms)]
+        (dtor_corec_uniqueN, dtor_corec_unique_thms),
+        (dtor_unfold_o_mapN, dtor_unfold_o_map_thms),
+        (dtor_corec_o_mapN, dtor_corec_o_map_thms)]
         |> map (apsnd (map single))
         |> maps (fn (thmN, thmss) =>
           map2 (fn b => fn thms =>

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 08 16:38:28 2013 +0200
@@ -1294,8 +1294,8 @@
           |> Thm.close_derivation
       end;
 
-    val ctor_rec_unique_thms =
-      split_conj_thm (split_conj_prems n
+    val (ctor_rec_unique_thms, ctor_rec_unique_thm) =
+      `split_conj_thm (split_conj_prems n
         (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm)
         |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @
            map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]});
@@ -1396,9 +1396,11 @@
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
 
     (*register new datatypes as BNFs*)
-    val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
+    val (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss',
+        ctor_Irel_thms, lthy) =
       if m = 0 then
-        (timer, replicate n DEADID_bnf, map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's,
+        (timer, replicate n DEADID_bnf,
+        map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's),
         replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
@@ -1446,7 +1448,7 @@
         val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks;
         val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks;
 
-        val ctor_map_thms =
+        val (ctor_map_thms, ctor_map_o_thms) =
           let
             fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
               (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
@@ -1458,7 +1460,7 @@
                 |> Thm.close_derivation)
               goals ctor_fold_thms map_comp_id_thms map_cong0s;
           in
-            map (fn thm => thm RS @{thm comp_eq_dest}) maps
+            `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
           end;
 
         val (ctor_map_unique_thms, ctor_map_unique_thm) =
@@ -1756,6 +1758,7 @@
         val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
         val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
         val folded_ctor_map_thms = map fold_maps ctor_map_thms;
+        val folded_ctor_map_o_thms = map fold_maps ctor_map_o_thms;
         val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
         val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
 
@@ -1797,10 +1800,15 @@
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
-          lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
+        (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss',
+          ctor_Irel_thms, lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
       end;
 
+      val ctor_fold_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
+        folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
+      val ctor_rec_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
+        folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
+
       val Irels = if m = 0 then map HOLogic.eq_const Ts
         else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
       val Irel_induct_thm =
@@ -1831,6 +1839,8 @@
         (ctor_foldN, ctor_fold_thms),
         (ctor_fold_uniqueN, ctor_fold_unique_thms),
         (ctor_rec_uniqueN, ctor_rec_unique_thms),
+        (ctor_fold_o_mapN, ctor_fold_o_map_thms),
+        (ctor_rec_o_mapN, ctor_rec_o_map_thms),
         (ctor_injectN, ctor_inject_thms),
         (ctor_recN, ctor_rec_thms),
         (dtor_ctorN, dtor_ctor_thms),

--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Thu Aug 08 16:38:28 2013 +0200
@@ -19,6 +19,8 @@
   val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
     int -> tactic
 
+  val mk_pointfree: Proof.context -> thm -> thm
+
   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
   val mk_Abs_inj_thm: thm -> thm
 
@@ -53,6 +55,16 @@
 
 fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x;
 
+(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
+fun mk_pointfree ctxt thm = thm
+  |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
+  |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp)
+  |> mk_Trueprop_eq
+  |> (fn goal => Goal.prove_sorry ctxt [] [] goal
+     (fn {context=ctxt, prems = _} =>
+       unfold_thms_tac ctxt [@{thm o_def}, mk_sym thm] THEN rtac refl 1))
+  |> Thm.close_derivation;
+
 
 (* Theorems for open typedefs with UNIV as representing set *)
 

--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Aug 08 15:30:25 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Aug 08 16:38:28 2013 +0200
@@ -604,7 +604,7 @@
   (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys);
 
 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
-fun mk_sym thm = sym OF [thm];
+fun mk_sym thm = thm RS sym;
 
 (*TODO: antiquote heavily used theorems once*)
 val Pair_eqD = @{thm iffD1[OF Pair_eq]};