# HG changeset patch
# User desharna
# Date 1654357324 -7200
# Node ID 6bd264ff410f973340a15d0f4912bb560ba6aec7
# Parent  a7c6722fbaf1769a379af9ebfdda2a8841a93e48
added lemmas reflp_on_inf, reflp_on_sup, and reflp_on_mono

diff -r a7c6722fbaf1 -r 6bd264ff410f NEWS
--- a/NEWS	Sat Jun 04 15:59:24 2022 +0200
+++ b/NEWS	Sat Jun 04 17:42:04 2022 +0200
@@ -50,7 +50,10 @@
       preorder.asymp_less
       reflp_onD
       reflp_onI
+      reflp_on_inf
+      reflp_on_mono
       reflp_on_subset
+      reflp_on_sup
       total_on_subset
       totalpD
       totalpI
diff -r a7c6722fbaf1 -r 6bd264ff410f src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Jun 04 15:59:24 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 17:42:04 2022 +0200
@@ -206,14 +206,20 @@
 lemma refl_on_Int: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<inter> B) (r \<inter> s)"
   unfolding refl_on_def by blast
 
+lemma reflp_on_inf: "reflp_on A R \<Longrightarrow> reflp_on B S \<Longrightarrow> reflp_on (A \<inter> B) (R \<sqinter> S)"
+  by (auto intro: reflp_onI dest: reflp_onD)
+
 lemma reflp_inf: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<sqinter> s)"
-  by (auto intro: reflpI elim: reflpE)
+  by (rule reflp_on_inf[of UNIV _ UNIV, unfolded Int_absorb])
 
 lemma refl_on_Un: "refl_on A r \<Longrightarrow> refl_on B s \<Longrightarrow> refl_on (A \<union> B) (r \<union> s)"
   unfolding refl_on_def by blast
 
+lemma reflp_on_sup: "reflp_on A R \<Longrightarrow> reflp_on B S \<Longrightarrow> reflp_on (A \<union> B) (R \<squnion> S)"
+  by (auto intro: reflp_onI dest: reflp_onD)
+
 lemma reflp_sup: "reflp r \<Longrightarrow> reflp s \<Longrightarrow> reflp (r \<squnion> s)"
-  by (auto intro: reflpI elim: reflpE)
+  by (rule reflp_on_sup[of UNIV _ UNIV, unfolded Un_absorb])
 
 lemma refl_on_INTER: "\<forall>x\<in>S. refl_on (A x) (r x) \<Longrightarrow> refl_on (\<Inter>(A ` S)) (\<Inter>(r ` S))"
   unfolding refl_on_def by fast
@@ -234,8 +240,12 @@
 lemma reflp_equality [simp]: "reflp (=)"
   by (simp add: reflp_def)
 
+lemma reflp_on_mono:
+  "reflp_on A R \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> Q x y) \<Longrightarrow> reflp_on A Q"
+  by (auto intro: reflp_onI dest: reflp_onD)
+
 lemma reflp_mono: "reflp R \<Longrightarrow> (\<And>x y. R x y \<longrightarrow> Q x y) \<Longrightarrow> reflp Q"
-  by (auto intro: reflpI dest: reflpD)
+  by (rule reflp_on_mono[of UNIV R Q]) simp_all
 
 
 subsubsection \<open>Irreflexivity\<close>