# HG changeset patch
# User desharna
# Date 1668008182 -3600
# Node ID 0fbfb4293ff714a997a00fded262f0af20d0045c
# Parent  11077c158b37fa6e38a8321c0b50074802d59fb7
added lemma reflp_on_conversp[simp]

diff -r 11077c158b37 -r 0fbfb4293ff7 NEWS
--- a/NEWS	Wed Nov 09 15:38:43 2022 +0100
+++ b/NEWS	Wed Nov 09 16:36:22 2022 +0100
@@ -45,6 +45,7 @@
       preorder.antisymp_less[simp]
       preorder.reflp_ge[simp]
       preorder.reflp_le[simp]
+      reflp_on_conversp[simp]
       totalp_on_singleton[simp]
 
 * Theory "HOL.Transitive_Closure":
diff -r 11077c158b37 -r 0fbfb4293ff7 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Nov 09 15:38:43 2022 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 09 16:36:22 2022 +0100
@@ -951,6 +951,9 @@
 lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
   by (auto simp: refl_on_def)
 
+lemma reflp_on_conversp [simp]: "reflp_on A R\<inverse>\<inverse> \<longleftrightarrow> reflp_on A R"
+  by (auto simp: reflp_on_def)
+
 lemma sym_converse [simp]: "sym (converse r) = sym r"
   unfolding sym_def by blast