# HG changeset patch
# User desharna
# Date 1669195644 -3600
# Node ID cbf38b7cb195dc3e3157e1fa1cf4d71b7128e1ae
# Parent  d8542bc5a3fa6370e665b16f7cc2ab6866bd64cc
added lemma totalp_on_converse[simp]

diff -r d8542bc5a3fa -r cbf38b7cb195 NEWS
--- a/NEWS	Wed Nov 23 10:23:18 2022 +0100
+++ b/NEWS	Wed Nov 23 10:27:24 2022 +0100
@@ -59,6 +59,7 @@
       preorder.reflp_on_le[simp]
       reflp_on_conversp[simp]
       totalI
+      totalp_on_converse[simp]
       totalp_on_singleton[simp]
 
 * Theory "HOL.Transitive_Closure":
diff -r d8542bc5a3fa -r cbf38b7cb195 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Nov 23 10:23:18 2022 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 23 10:27:24 2022 +0100
@@ -1021,6 +1021,9 @@
 lemma total_on_converse [simp]: "total_on A (r\<inverse>) = total_on A r"
   by (auto simp: total_on_def)
 
+lemma totalp_on_converse [simp]: "totalp_on A R\<inverse>\<inverse> = totalp_on A R"
+  by (rule total_on_converse[to_pred])
+
 lemma finite_converse [iff]: "finite (r\<inverse>) = finite r"
 unfolding converse_def conversep_iff using [[simproc add: finite_Collect]]
 by (auto elim: finite_imageD simp: inj_on_def)