more useful properties of the relators

--- a/src/Doc/Datatypes/Datatypes.thy	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Sep 24 12:21:19 2015 +0200
@@ -1003,6 +1003,18 @@
 \item[@{text "t."}\hthm{rel_refl}\rm:] ~ \\
 @{thm list.rel_refl[no_vars]}
 
+\item[@{text "t."}\hthm{rel_refl_strong}\rm:] ~ \\
+@{thm list.rel_refl_strong[no_vars]}
+
+\item[@{text "t."}\hthm{rel_reflp}\rm:] ~ \\
+@{thm list.rel_reflp[no_vars]}
+
+\item[@{text "t."}\hthm{rel_symp}\rm:] ~ \\
+@{thm list.rel_symp[no_vars]}
+
+\item[@{text "t."}\hthm{rel_transp}\rm:] ~ \\
+@{thm list.rel_transp[no_vars]}
+
 \item[@{text "t."}\hthm{rel_transfer} @{text "[transfer_rule]"}\rm:] ~ \\
 @{thm list.rel_transfer[no_vars]} \\
 The @{text "[transfer_rule]"} attribute is set by the @{text transfer} plugin

--- a/src/HOL/BNF_Def.thy	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/BNF_Def.thy	Thu Sep 24 12:21:19 2015 +0200
@@ -234,6 +234,18 @@
 lemma ge_eq_refl: "op = \<le> R \<Longrightarrow> R x x"
   by auto
 
+lemma reflp_eq: "reflp R = (op = \<le> R)"
+  by (auto simp: reflp_def fun_eq_iff)
+
+lemma transp_relcompp: "transp r \<longleftrightarrow> r OO r \<le> r"
+  by (auto simp: transp_def)
+
+lemma symp_conversep: "symp R = (R\<inverse>\<inverse> \<le> R)"
+  by (auto simp: symp_def fun_eq_iff)
+
+lemma diag_imp_eq_le: "(\<And>x. x \<in> A \<Longrightarrow> R x x) \<Longrightarrow> \<forall>x y. x \<in> A \<longrightarrow> y \<in> A \<longrightarrow> x = y \<longrightarrow> R x y"
+  by blast
+
 ML_file "Tools/BNF/bnf_util.ML"
 ML_file "Tools/BNF/bnf_tactics.ML"
 ML_file "Tools/BNF/bnf_def_tactics.ML"

--- 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:21:19 2015 +0200
@@ -82,6 +82,10 @@
   val rel_mono_strong0_of_bnf: bnf -> thm
   val rel_mono_strong_of_bnf: bnf -> thm
   val rel_refl_of_bnf: bnf -> thm
+  val rel_refl_strong_of_bnf: bnf -> thm
+  val rel_reflp_of_bnf: bnf -> thm
+  val rel_symp_of_bnf: bnf -> thm
+  val rel_transp_of_bnf: bnf -> thm
   val rel_map_of_bnf: bnf -> thm list
   val rel_transfer_of_bnf: bnf -> thm
   val rel_eq_of_bnf: bnf -> thm
@@ -254,13 +258,18 @@
   rel_conversep: thm lazy,
   rel_OO: thm lazy,
   rel_refl: thm lazy,
+  rel_refl_strong: thm lazy,
+  rel_reflp: thm lazy,
+  rel_symp: thm lazy,
+  rel_transp: thm lazy,
   rel_transfer: thm lazy
 };
 
 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_transfer = {
+    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 = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -291,6 +300,10 @@
   rel_conversep = rel_conversep,
   rel_OO = rel_OO,
   rel_refl = rel_refl,
+  rel_refl_strong = rel_refl_strong,
+  rel_reflp = rel_reflp,
+  rel_symp = rel_symp,
+  rel_transp = rel_transp,
   set_transfer = set_transfer};
 
 fun map_facts f {
@@ -324,6 +337,10 @@
   rel_conversep,
   rel_OO,
   rel_refl,
+  rel_refl_strong,
+  rel_reflp,
+  rel_symp,
+  rel_transp,
   set_transfer} =
   {bd_Card_order = f bd_Card_order,
     bd_Cinfinite = f bd_Cinfinite,
@@ -355,6 +372,10 @@
     rel_conversep = Lazy.map f rel_conversep,
     rel_OO = Lazy.map f rel_OO,
     rel_refl = Lazy.map f rel_refl,
+    rel_refl_strong = Lazy.map f rel_refl_strong,
+    rel_reflp = Lazy.map f rel_reflp,
+    rel_symp = Lazy.map f rel_symp,
+    rel_transp = Lazy.map f rel_transp,
     set_transfer = Lazy.map (map f) set_transfer};
 
 val morph_facts = map_facts o Morphism.thm;
@@ -487,6 +508,10 @@
 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;
 val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
+val rel_refl_strong_of_bnf = Lazy.force o #rel_refl_strong o #facts o rep_bnf;
+val rel_reflp_of_bnf = Lazy.force o #rel_reflp o #facts o rep_bnf;
+val rel_symp_of_bnf = Lazy.force o #rel_symp o #facts o rep_bnf;
+val rel_transp_of_bnf = Lazy.force o #rel_transp o #facts o rep_bnf;
 val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
 val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
@@ -671,6 +696,10 @@
 val rel_mono_strong0N = "rel_mono_strong0";
 val rel_mono_strongN = "rel_mono_strong";
 val rel_reflN = "rel_refl";
+val rel_refl_strongN = "rel_refl_strong";
+val rel_reflpN = "rel_reflp";
+val rel_sympN = "rel_symp";
+val rel_transpN = "rel_transp";
 val rel_transferN = "rel_transfer";
 val rel_comppN = "rel_compp";
 val rel_compp_GrpN = "rel_compp_Grp";
@@ -743,6 +772,10 @@
            (rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
            (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
            (rel_reflN, [Lazy.force (#rel_refl facts)], []),
+           (rel_refl_strongN, [Lazy.force (#rel_refl_strong facts)], []),
+           (rel_reflpN, [Lazy.force (#rel_reflp facts)], []),
+           (rel_sympN, [Lazy.force (#rel_symp facts)], []),
+           (rel_transpN, [Lazy.force (#rel_transp facts)], []),
            (rel_transferN, [Lazy.force (#rel_transfer facts)], []),
            (set_mapN, map Lazy.force (#set_map facts), []),
            (set_transferN, Lazy.force (#set_transfer facts), [])]
@@ -1432,6 +1465,33 @@
 
         val rel_refl = Lazy.lazy mk_rel_refl;
 
+        fun mk_rel_refl_strong () =
+          (rule_by_tactic lthy (ALLGOALS (Object_Logic.full_atomize_tac lthy))
+            ((Lazy.force rel_eq RS @{thm predicate2_eqD}) RS @{thm iffD2[OF _ refl]} RS
+              Lazy.force rel_mono_strong)) OF
+            (replicate live @{thm diag_imp_eq_le})
+
+        val rel_refl_strong = Lazy.lazy mk_rel_refl_strong;
+
+        fun mk_rel_preserves mk_prop prop_conv_thm thm () =
+          let
+            val Rs = map2 retype_const_or_free self_pred2RTs Rs;
+            val prems = map (HOLogic.mk_Trueprop o mk_prop) Rs;
+            val goal = HOLogic.mk_Trueprop (mk_prop (Term.list_comb (relAsAs, Rs)));
+          in
+            Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
+              (fn {context = ctxt, prems = _} =>
+                unfold_thms_tac ctxt [prop_conv_thm] THEN
+                HEADGOAL (rtac ctxt (Lazy.force thm RS sym RS @{thm ord_eq_le_trans}) 
+                  THEN' rtac ctxt (Lazy.force rel_mono) THEN_ALL_NEW assume_tac ctxt))
+            |> singleton (Proof_Context.export names_lthy lthy)
+            |> Thm.close_derivation
+          end;
+
+        val rel_reflp = Lazy.lazy (mk_rel_preserves mk_reflp @{thm reflp_eq} rel_eq);
+        val rel_symp = Lazy.lazy (mk_rel_preserves mk_symp @{thm symp_conversep} rel_conversep);
+        val rel_transp = Lazy.lazy (mk_rel_preserves mk_transp @{thm transp_relcompp} rel_OO);
+
         fun mk_map_transfer () =
           let
             val rels = map2 mk_rel_fun transfer_domRs transfer_ranRs;
@@ -1520,7 +1580,8 @@
         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_transfer;
+          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_util.ML	Thu Sep 24 12:21:19 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 24 12:21:19 2015 +0200
@@ -61,6 +61,9 @@
   val mk_rel_comp: term * term -> term
   val mk_rel_compp: term * term -> term
   val mk_vimage2p: term -> term -> term
+  val mk_reflp: term -> term
+  val mk_symp: term -> term
+  val mk_transp: term -> term
 
   (*parameterized terms*)
   val mk_nthN: int -> term -> int -> term
@@ -348,6 +351,12 @@
       (T1 --> T2) --> (U1 --> U2) --> mk_pred2T T2 U2 --> mk_pred2T T1 U1) $ f $ g
   end;
 
+fun mk_pred name R =
+  Const (name, uncurry mk_pred2T (fastype_of R |> dest_pred2T) --> HOLogic.boolT) $ R;
+val mk_reflp = mk_pred @{const_name reflp};
+val mk_symp = mk_pred @{const_name symp};
+val mk_transp =  mk_pred @{const_name transp};
+
 fun mk_trans thm1 thm2 = trans OF [thm1, thm2];
 fun mk_sym thm = thm RS sym;