# HG changeset patch
# User desharna
# Date 1654360350 -7200
# Node ID 02719bd7b4e6c18e8e1c04d19d92a60af4720904
# Parent  f0dfcd8329d042793526122dbdf3e2286012fdd6
added lemma reflp_on_empty[simp] and totalp_on_empty[simp]

diff -r f0dfcd8329d0 -r 02719bd7b4e6 NEWS
--- a/NEWS	Sat Jun 04 17:58:08 2022 +0200
+++ b/NEWS	Sat Jun 04 18:32:30 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,6 +64,7 @@
       totalpI
       totalp_onD
       totalp_onI
+      totalp_on_empty[simp]
       totalp_on_subset
 
 * Theory "HOL-Library.Multiset":
diff -r f0dfcd8329d0 -r 02719bd7b4e6 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Jun 04 17:58:08 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 18:32:30 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)
 
@@ -548,6 +551,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