(co)rec is (just as the (un)fold) the unique morphism;

--- a/src/HOL/BNF/BNF_GFP.thy	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Tue Apr 23 11:43:09 2013 +0200
@@ -13,13 +13,18 @@
   "codata" :: thy_decl
 begin
 
-lemma sum_case_comp_Inl:
-"sum_case f g \<circ> Inl = f"
+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_comp_Inl: "sum_case f g \<circ> Inl = f"
 unfolding comp_def by simp
 
 lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
 by (auto split: sum.splits)
 
+lemma sum_case_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> sum_case g h = f"
+by (metis sum_case_comp_Inl sum_case_o_inj(2) surjective_sum)
+
 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
 by auto
 

--- a/src/HOL/BNF/BNF_LFP.thy	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Tue Apr 23 11:43:09 2013 +0200
@@ -44,9 +44,15 @@
 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
 
+lemma convol_expand_snd': "(fst o f = g) \<Longrightarrow> (h = snd o f) \<longleftrightarrow> (<g, h> = f)"
+  by (metis convol_expand_snd snd_convol)
+
 definition inver where
   "inver g f A = (ALL a : A. g (f a) = a)"
 

--- a/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 23 11:43:09 2013 +0200
@@ -36,6 +36,7 @@
   val ctor_mapN: string
   val ctor_map_uniqueN: string
   val ctor_recN: string
+  val ctor_rec_uniqueN: string
   val ctor_relN: string
   val ctor_set_inclN: string
   val ctor_set_set_inclN: string
@@ -47,6 +48,7 @@
   val dtorN: string
   val dtor_coinductN: string
   val dtor_corecN: string
+  val dtor_corec_uniqueN: string
   val dtor_ctorN: string
   val dtor_exhaustN: string
   val dtor_injectN: string
@@ -207,7 +209,9 @@
 val recN = "rec"
 val corecN = coN ^ recN
 val ctor_recN = ctorN ^ "_" ^ recN
+val ctor_rec_uniqueN = ctor_recN ^ uniqueN
 val dtor_corecN = dtorN ^ "_" ^ corecN
+val dtor_corec_uniqueN = dtor_corecN ^ uniqueN
 val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN
 
 val ctor_dtorN = ctorN ^ "_" ^ dtorN

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Apr 23 11:43:09 2013 +0200
@@ -219,8 +219,10 @@
     val in_bds = map in_bd_of_bnf bnfs;
     val in_monos = map in_mono_of_bnf bnfs;
     val map_comps = map map_comp_of_bnf bnfs;
+    val sym_map_comps = map (fn thm => thm RS sym) map_comps;
     val map_comp's = map map_comp'_of_bnf bnfs;
     val map_congs = map map_cong_of_bnf bnfs;
+    val map_ids = map map_id_of_bnf bnfs;
     val map_id's = map map_id'_of_bnf bnfs;
     val map_wpulls = map map_wpull_of_bnf bnfs;
     val set_bdss = map set_bd_of_bnf bnfs;
@@ -1861,6 +1863,7 @@
     val corec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls;
     val corec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_Inls_rev;
     val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
+    val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs;
 
     val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs),
       FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy
@@ -2126,15 +2129,18 @@
     val corec_name = Binding.name_of o corec_bind;
     val corec_def_bind = rpair [] o Thm.def_binding o corec_bind;
 
+    val corec_strs =
+      map3 (fn dtor => fn sum_s => fn mapx =>
+        mk_sum_case
+          (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
+      dtors corec_ss corec_maps;
+
     fun corec_spec i T AT =
       let
         val corecT = Library.foldr (op -->) (corec_sTs, AT --> T);
-        val maps = map3 (fn dtor => fn sum_s => fn mapx => mk_sum_case
-            (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
-          dtors corec_ss corec_maps;
 
         val lhs = Term.list_comb (Free (corec_name i, corecT), corec_ss);
-        val rhs = HOLogic.mk_comp (mk_unfold Ts maps i, Inr_const T AT);
+        val rhs = HOLogic.mk_comp (mk_unfold Ts corec_strs i, Inr_const T AT);
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -2175,6 +2181,26 @@
         goals dtor_unfold_thms map_congs
       end;
 
+    val corec_unique_mor_thm =
+      let
+        val id_fs = map2 (fn T => fn f => mk_sum_case (HOLogic.id_const T, f)) Ts unfold_fs;
+        val prem = HOLogic.mk_Trueprop (mk_mor corec_UNIVs corec_strs UNIVs dtors id_fs);
+        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_corec corec_ss i);
+        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+          (map2 mk_fun_eq unfold_fs ks));
+      in
+        Goal.prove_sorry lthy [] []
+          (fold_rev Logic.all (corec_ss @ unfold_fs) (Logic.mk_implies (prem, unique)))
+          (mk_corec_unique_mor_tac corec_defs corec_Inl_sum_thms unfold_unique_mor_thm)
+          |> Thm.close_derivation
+      end;
+
+    val dtor_corec_unique_thms =
+      split_conj_thm (split_conj_prems n
+        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} RS corec_unique_mor_thm)
+        |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_comp_Inl} @
+           map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]});
+
     val ctor_dtor_corec_thms =
       map3 mk_ctor_dtor_unfold_like_thm dtor_inject_thms dtor_ctor_thms dtor_corec_thms;
 
@@ -2990,7 +3016,8 @@
         (dtor_exhaustN, dtor_exhaust_thms),
         (dtor_injectN, dtor_inject_thms),
         (dtor_unfoldN, dtor_unfold_thms),
-        (dtor_unfold_uniqueN, dtor_unfold_unique_thms)]
+        (dtor_unfold_uniqueN, dtor_unfold_unique_thms),
+        (dtor_corec_uniqueN, dtor_corec_unique_thms)]
         |> map (apsnd (map single))
         |> maps (fn (thmN, thmss) =>
           map2 (fn b => fn thms =>

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Apr 23 11:43:09 2013 +0200
@@ -37,6 +37,8 @@
   val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
   val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
+  val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
+    tactic
   val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
   val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
     thm -> thm -> tactic
@@ -1121,6 +1123,11 @@
     REPEAT_DETERM_N m o rtac refl,
     EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
 
+fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt
+    (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
+  etac unfold_unique_mor 1;
+
 fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel =
   EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
     CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Apr 23 11:43:09 2013 +0200
@@ -141,6 +141,7 @@
     val bd_Cnotzeros = map bd_Cnotzero_of_bnf bnfs;
     val bd_Cnotzero = hd bd_Cnotzeros;
     val in_bds = map in_bd_of_bnf bnfs;
+    val sym_map_comps = map (fn bnf => map_comp_of_bnf bnf RS sym) bnfs;
     val map_comp's = map map_comp'_of_bnf bnfs;
     val map_congs = map map_cong_of_bnf bnfs;
     val map_ids = map map_id_of_bnf bnfs;
@@ -980,6 +981,7 @@
     val rec_maps = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts;
     val rec_maps_rev = map (Term.subst_atomic_types (activeBs ~~ Ts)) map_fsts_rev;
     val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts;
+    val rec_UNIVs = map2 (HOLogic.mk_UNIV oo curry HOLogic.mk_prodT) Ts activeAs;
 
     val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')),
       (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy
@@ -1217,15 +1219,17 @@
     val rec_name = Binding.name_of o rec_bind;
     val rec_def_bind = rpair [] o Thm.def_binding o rec_bind;
 
+    val rec_strs =
+      map3 (fn ctor => fn prod_s => fn mapx =>
+        mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
+      ctors rec_ss rec_maps;
+
     fun rec_spec i T AT =
       let
         val recT = Library.foldr (op -->) (rec_sTs, T --> AT);
-        val maps = map3 (fn ctor => fn prod_s => fn mapx =>
-          mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
-          ctors rec_ss rec_maps;
 
         val lhs = Term.list_comb (Free (rec_name i, recT), rec_ss);
-        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts maps i);
+        val rhs = HOLogic.mk_comp (snd_const (HOLogic.mk_prodT (T, AT)), mk_fold Ts rec_strs i);
       in
         mk_Trueprop_eq (lhs, rhs)
       end;
@@ -1264,6 +1268,25 @@
         goals ctor_fold_thms
       end;
 
+    val rec_unique_mor_thm =
+      let
+        val id_fs = map2 (fn T => fn f => mk_convol (HOLogic.id_const T, f)) Ts fs;
+        val prem = HOLogic.mk_Trueprop (mk_mor UNIVs ctors rec_UNIVs rec_strs id_fs);
+        fun mk_fun_eq f i = HOLogic.mk_eq (f, mk_rec rec_ss i);
+        val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_fun_eq fs ks));
+      in
+        Goal.prove_sorry lthy [] []
+          (fold_rev Logic.all (rec_ss @ fs) (Logic.mk_implies (prem, unique)))
+          (mk_rec_unique_mor_tac rec_defs fst_rec_pair_thms fold_unique_mor_thm)
+          |> Thm.close_derivation
+      end;
+
+    val ctor_rec_unique_thms =
+      split_conj_thm (split_conj_prems n
+        (mor_UNIV_thm RS @{thm ssubst[of _ _ "%x. x"]} 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]});
+
     val timer = time (timer "rec definitions & thms");
 
     val (ctor_induct_thm, induct_params) =
@@ -1817,6 +1840,7 @@
         (ctor_exhaustN, ctor_exhaust_thms),
         (ctor_foldN, ctor_fold_thms),
         (ctor_fold_uniqueN, ctor_fold_unique_thms),
+        (ctor_rec_uniqueN, ctor_rec_unique_thms),
         (ctor_injectN, ctor_inject_thms),
         (ctor_recN, ctor_rec_thms),
         (dtor_ctorN, dtor_ctor_thms),

--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Tue Apr 23 11:14:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Tue Apr 23 11:43:09 2013 +0200
@@ -65,6 +65,8 @@
     thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic
   val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
+    tactic
   val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
     {prems: 'a, context: Proof.context} -> tactic
   val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
@@ -525,6 +527,11 @@
   EVERY' [rtac trans, rtac o_apply, rtac trans, rtac (foldx RS @{thm arg_cong[of _ _ snd]}),
     rtac @{thm snd_convol'}] 1;
 
+fun mk_rec_unique_mor_tac rec_defs fst_recs fold_unique_mor {context = ctxt, prems = _} =
+  unfold_thms_tac ctxt
+    (rec_defs @ map (fn thm => thm RS @{thm convol_expand_snd'}) fst_recs) THEN
+  etac fold_unique_mor 1;
+
 fun mk_ctor_induct_tac m set_natural'ss init_induct morEs mor_Abs Rep_invs Abs_invs Reps =
   let
     val n = length set_natural'ss;