# HG changeset patch
# User desharna
# Date 1654672797 -7200
# Node ID 47abacd97f7b58cd97ebd516723d21840bfc1b15
# Parent  2e8a2dc7a1e6369865389ea721b5f102aec73aa0# Parent  a4fa039a6a60bf7ae39606178da1a9c9ad2ea421
merged

diff -r 2e8a2dc7a1e6 -r 47abacd97f7b NEWS
--- a/NEWS	Wed Jun 08 09:12:51 2022 +0200
+++ b/NEWS	Wed Jun 08 09:19:57 2022 +0200
@@ -54,6 +54,7 @@
       reflp_onI
       reflp_on_Inf
       reflp_on_Sup
+      reflp_on_empty[simp]
       reflp_on_inf
       reflp_on_mono
       reflp_on_subset
@@ -63,7 +64,9 @@
       totalpI
       totalp_onD
       totalp_onI
+      totalp_on_empty[simp]
       totalp_on_subset
+      totalp_on_total_on_eq[pred_set_conv]
 
 * Theory "HOL-Library.Multiset":
   - Consolidated operation and fact names.
diff -r 2e8a2dc7a1e6 -r 47abacd97f7b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Jun 08 09:12:51 2022 +0200
+++ b/src/HOL/Relation.thy	Wed Jun 08 09:19:57 2022 +0200
@@ -236,6 +236,9 @@
 lemma refl_on_empty [simp]: "refl_on {} {}"
   by (simp add: refl_on_def)
 
+lemma reflp_on_empty [simp]: "reflp_on {} R"
+  by (auto intro: reflp_onI)
+
 lemma refl_on_singleton [simp]: "refl_on {x} {(x, x)}"
 by (blast intro: refl_onI)
 
@@ -525,6 +528,9 @@
 abbreviation totalp where
   "totalp \<equiv> totalp_on UNIV"
 
+lemma totalp_on_refl_on_eq[pred_set_conv]: "totalp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> total_on A r"
+  by (simp add: totalp_on_def total_on_def)
+
 lemma totalp_onI:
   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x) \<Longrightarrow> totalp_on A R"
   by (simp add: totalp_on_def)
@@ -548,6 +554,9 @@
 lemma total_on_empty [simp]: "total_on {} r"
   by (simp add: total_on_def)
 
+lemma totalp_on_empty [simp]: "totalp_on {} R"
+  by (auto intro: totalp_onI)
+
 lemma total_on_singleton [simp]: "total_on {x} {(x, x)}"
   unfolding total_on_def by blast