congruence rules for the relator

--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 24 12:28:15 2015 +0200
@@ -1000,6 +1000,15 @@
 The @{text "[relator_mono]"} attribute is set by the @{text lifting} plugin
 (Section~\ref{ssec:lifting}).
 
+\item[@{text "t."}\hthm{rel_mono_strong}\rm:] ~ \\
+@{thm list.rel_mono_strong[no_vars]}
+
+\item[@{text "t."}\hthm{rel_cong} @{text "[fundef_cong]"}\rm:] ~ \\
+@{thm list.rel_cong[no_vars]}
+
+\item[@{text "t."}\hthm{rel_cong_simp}\rm:] ~ \\
+@{thm list.rel_cong_simp[no_vars]}
+
 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
 @{thm list.rel_refl[no_vars]}
 

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Sep 24 12:28:15 2015 +0200
@@ -325,13 +325,12 @@
     fun rel_OO_Grp_tac ctxt =
       let
         val outer_rel_Grp = rel_Grp_of_bnf outer RS sym;
-        val outer_rel_cong = rel_cong_of_bnf outer;
         val thm =
           (trans OF [in_alt_thm RS @{thm OO_Grp_cong},
              trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
                [trans OF [outer_rel_Grp RS @{thm arg_cong[of _ _ conversep]},
                  rel_conversep_of_bnf outer RS sym], outer_rel_Grp],
-               trans OF [rel_OO_of_bnf outer RS sym, outer_rel_cong OF
+               trans OF [rel_OO_of_bnf outer RS sym, rel_cong0_of_bnf outer OF
                  (map (fn bnf => rel_OO_Grp_of_bnf bnf RS sym) inners)]]] RS sym);
       in
         unfold_thms_tac ctxt set'_eq_sets THEN rtac ctxt thm 1
@@ -441,7 +440,7 @@
             trans OF [@{thm arg_cong2[of _ _ _ _ relcompp]} OF
               [trans OF [rel_Grp RS @{thm arg_cong[of _ _ conversep]},
                 rel_conversep_of_bnf bnf RS sym], rel_Grp],
-              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+              trans OF [rel_OO_of_bnf bnf RS sym, rel_cong0_of_bnf bnf OF
                 (replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
                  replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
       in

--- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Thu Sep 24 12:28:15 2015 +0200
@@ -76,7 +76,9 @@
   val rel_Grp_of_bnf: bnf -> thm
   val rel_OO_of_bnf: bnf -> thm
   val rel_OO_Grp_of_bnf: bnf -> thm
+  val rel_cong0_of_bnf: bnf -> thm
   val rel_cong_of_bnf: bnf -> thm
+  val rel_cong_simp_of_bnf: bnf -> thm
   val rel_conversep_of_bnf: bnf -> thm
   val rel_mono_of_bnf: bnf -> thm
   val rel_mono_strong0_of_bnf: bnf -> thm
@@ -248,7 +250,9 @@
   rel_eq: thm lazy,
   rel_flip: thm lazy,
   set_map: thm lazy list,
+  rel_cong0: thm lazy,
   rel_cong: thm lazy,
+  rel_cong_simp: thm lazy,
   rel_map: thm list lazy,
   rel_mono: thm lazy,
   rel_mono_strong0: thm lazy,
@@ -267,9 +271,9 @@
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
     inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0 map_ident map_transfer
-    rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer
-    rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp
-    rel_transfer = {
+    rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono rel_mono_strong0
+    rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong rel_reflp
+    rel_symp rel_transp rel_transfer = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -290,7 +294,9 @@
   rel_eq = rel_eq,
   rel_flip = rel_flip,
   set_map = set_map,
+  rel_cong0 = rel_cong0,
   rel_cong = rel_cong,
+  rel_cong_simp = rel_cong_simp,
   rel_map = rel_map,
   rel_mono = rel_mono,
   rel_mono_strong0 = rel_mono_strong0,
@@ -327,7 +333,9 @@
   rel_eq,
   rel_flip,
   set_map,
+  rel_cong0,
   rel_cong,
+  rel_cong_simp,
   rel_map,
   rel_mono,
   rel_mono_strong0,
@@ -362,7 +370,9 @@
     rel_eq = Lazy.map f rel_eq,
     rel_flip = Lazy.map f rel_flip,
     set_map = map (Lazy.map f) set_map,
+    rel_cong0 = Lazy.map f rel_cong0,
     rel_cong = Lazy.map f rel_cong,
+    rel_cong_simp = Lazy.map f rel_cong_simp,
     rel_map = Lazy.map (map f) rel_map,
     rel_mono = Lazy.map f rel_mono,
     rel_mono_strong0 = Lazy.map f rel_mono_strong0,
@@ -503,7 +513,9 @@
 val set_map0_of_bnf = #set_map0 o #axioms o rep_bnf;
 val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
 val set_transfer_of_bnf = Lazy.force o #set_transfer o #facts o rep_bnf;
+val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
+val rel_cong_simp_of_bnf = Lazy.force o #rel_cong_simp o #facts o rep_bnf;
 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
 val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
 val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
@@ -695,6 +707,8 @@
 val rel_monoN = "rel_mono";
 val rel_mono_strong0N = "rel_mono_strong0";
 val rel_mono_strongN = "rel_mono_strong";
+val rel_congN = "rel_cong";
+val rel_cong_simpN = "rel_cong_simp";
 val rel_reflN = "rel_refl";
 val rel_refl_strongN = "rel_refl_strong";
 val rel_reflpN = "rel_reflp";
@@ -771,6 +785,8 @@
            (rel_mapN, Lazy.force (#rel_map facts), []),
            (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
+           (rel_congN, [Lazy.force (#rel_cong facts)], fundefcong_attrs),
+           (rel_cong_simpN, [Lazy.force (#rel_cong_simp facts)], []),
            (rel_reflN, [Lazy.force (#rel_refl facts)], []),
            (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []),
            (rel_reflpN, [Lazy.force (#rel_reflp facts)], []),
@@ -1066,7 +1082,7 @@
     fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
 
     val pre_names_lthy = lthy;
-    val ((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), zs), zs'), ys), As),
+    val (((((((((((((((((((((((fs, fs'), gs), hs), is), x), x'), y), y'), zs), zs'), ys), As),
       As_copy), bs), Rs), Rs_copy), Ss), S_AsCs), S_CsBs), S_BsEs),
       transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
       |> mk_Frees "f" (map2 (curry op -->) As' Bs')
@@ -1077,6 +1093,7 @@
       ||>> yield_singleton (mk_Frees "x") CA'
       ||>> yield_singleton (mk_Frees "x") CA'
       ||>> yield_singleton (mk_Frees "y") CB'
+      ||>> yield_singleton (mk_Frees "y") CB'
       ||>> mk_Frees "z" As'
       ||>> mk_Frees "z" As'
       ||>> mk_Frees "y" Bs'
@@ -1093,7 +1110,8 @@
       ||>> mk_Frees "S" transfer_ranRTs;
 
     val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs;
-    val x_copy = retype_const_or_free CA' y;
+    val x_copy = retype_const_or_free CA' y';
+    val y_copy = retype_const_or_free CB' x';
 
     val rel = mk_bnf_rel pred2RTs CA' CB';
     val relCsEs = mk_bnf_rel pred2RTsCsEs CC' CE';
@@ -1322,7 +1340,7 @@
 
         val rel_Grp = Lazy.lazy mk_rel_Grp;
 
-        fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy
+        fun mk_rel_prems f = map2 (HOLogic.mk_Trueprop oo f) Rs Rs_copy;
         fun mk_rel_concl f = HOLogic.mk_Trueprop
           (f (Term.list_comb (rel, Rs), Term.list_comb (rel, Rs_copy)));
 
@@ -1338,7 +1356,7 @@
             |> Thm.close_derivation
           end;
 
-        fun mk_rel_cong () =
+        fun mk_rel_cong0 () =
           let
             val cong_prems = mk_rel_prems (curry HOLogic.mk_eq);
             val cong_concl = mk_rel_concl HOLogic.mk_eq;
@@ -1350,14 +1368,14 @@
           end;
 
         val rel_mono = Lazy.lazy mk_rel_mono;
-        val rel_cong = Lazy.lazy mk_rel_cong;
+        val rel_cong0 = Lazy.lazy mk_rel_cong0;
 
         fun mk_rel_eq () =
           Goal.prove_sorry lthy [] []
             (mk_Trueprop_eq (Term.list_comb (relAsAs, map HOLogic.eq_const As'),
               HOLogic.eq_const CA'))
             (fn {context = ctxt, prems = _} =>
-              mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong) (#map_id0 axioms))
+              mk_rel_eq_tac ctxt live (Lazy.force rel_Grp) (Lazy.force rel_cong0) (#map_id0 axioms))
           |> Thm.close_derivation;
 
         val rel_eq = Lazy.lazy mk_rel_eq;
@@ -1433,6 +1451,30 @@
 
         val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
 
+        fun mk_rel_cong_prem mk_implies x x' z z' set set' R R_copy =
+          Logic.all z (Logic.all z'
+            (mk_implies (mk_Trueprop_mem (z, set $ x), mk_implies (mk_Trueprop_mem (z', set' $ x'),
+              mk_Trueprop_eq (R $ z $ z', R_copy $ z $ z')))));
+
+        fun mk_rel_cong mk_implies () =
+          let
+            val prem0 = mk_Trueprop_eq (x, x_copy);
+            val prem1 = mk_Trueprop_eq (y, y_copy);
+            val prems = @{map 6} (mk_rel_cong_prem mk_implies x_copy y_copy)
+              zs ys bnf_sets_As bnf_sets_Bs Rs Rs_copy;
+            val eq = mk_Trueprop_eq (Term.list_comb (rel, Rs) $ x $ y,
+              Term.list_comb (rel, Rs_copy) $ x_copy $ y_copy);
+          in
+            Goal.prove_sorry lthy [] (prem0 :: prem1 :: prems) eq
+              (fn {context = ctxt, prems} =>
+                mk_rel_cong_tac ctxt (chop 2 prems) (Lazy.force rel_mono_strong))
+            |> Thm.close_derivation
+            |> singleton (Proof_Context.export names_lthy lthy)
+          end;
+
+        val rel_cong = Lazy.lazy (mk_rel_cong Logic.mk_implies);
+        val rel_cong_simp = Lazy.lazy (mk_rel_cong (fn (a, b) => @{term simp_implies} $ a $ b));
+
         fun mk_rel_map () =
           let
             fun mk_goal lhs rhs =
@@ -1579,9 +1621,9 @@
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
           in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_id map_ident0
-          map_ident map_transfer rel_eq rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0
-          rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl rel_refl_strong
-          rel_reflp rel_symp rel_transp rel_transfer;
+          map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map
+          rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO
+          rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 

--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 24 12:28:15 2015 +0200
@@ -28,6 +28,7 @@
   val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
   val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
   val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
   val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
 
   val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
@@ -356,4 +357,15 @@
     REPEAT_DETERM o (eresolve_tac ctxt @{thms CollectE case_prodE}) THEN' hyp_subst_tac ctxt THEN'
     rtac ctxt bexI THEN' etac ctxt @{thm subst_Pair[OF _ refl]} THEN' etac ctxt imageI))) set_maps);
 
+fun mk_rel_cong_tac ctxt (eqs, prems) mono =
+  let
+    fun mk_tac thm = etac ctxt thm THEN_ALL_NEW assume_tac ctxt;
+    fun mk_tacs iffD = etac ctxt mono :: 
+      map (fn thm => (unfold_thms ctxt @{thms simp_implies_def} thm RS iffD)
+        |> Drule.rotate_prems ~1 |> mk_tac) prems;
+  in
+    unfold_thms_tac ctxt eqs THEN
+    HEADGOAL (EVERY' (rtac ctxt iffI :: mk_tacs iffD1 @ mk_tacs iffD2))
+  end;
+
 end;

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 24 12:28:15 2015 +0200
@@ -219,7 +219,7 @@
     val map_ids = map map_id_of_bnf bnfs;
     val set_bdss = map set_bd_of_bnf bnfs;
     val set_mapss = map set_map_of_bnf bnfs;
-    val rel_congs = map rel_cong_of_bnf bnfs;
+    val rel_congs = map rel_cong0_of_bnf bnfs;
     val rel_converseps = map rel_conversep_of_bnf bnfs;
     val rel_Grps = map rel_Grp_of_bnf bnfs;
     val le_rel_OOs = map le_rel_OO_of_bnf bnfs;