# HG changeset patch
# User desharna
# Date 1654362712 -7200
# Node ID a4fa039a6a60bf7ae39606178da1a9c9ad2ea421
# Parent  02719bd7b4e6c18e8e1c04d19d92a60af4720904
added lemma totalp_on_total_on_eq[pred_set_conv]

diff -r 02719bd7b4e6 -r a4fa039a6a60 NEWS
--- a/NEWS	Sat Jun 04 18:32:30 2022 +0200
+++ b/NEWS	Sat Jun 04 19:11:52 2022 +0200
@@ -66,6 +66,7 @@
       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 02719bd7b4e6 -r a4fa039a6a60 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Jun 04 18:32:30 2022 +0200
+++ b/src/HOL/Relation.thy	Sat Jun 04 19:11:52 2022 +0200
@@ -528,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)