# HG changeset patch
# User desharna
# Date 1669195398 -3600
# Node ID d8542bc5a3fa6370e665b16f7cc2ab6866bd64cc
# Parent  5a13f1519f5d19058826cb4bef05a82a8a3eb3ee
added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]

diff -r 5a13f1519f5d -r d8542bc5a3fa NEWS
--- a/NEWS	Wed Nov 23 10:02:04 2022 +0100
+++ b/NEWS	Wed Nov 23 10:23:18 2022 +0100
@@ -40,9 +40,11 @@
       antisymp_if_asymp
       irrefl_onD
       irrefl_onI
+      irrefl_on_converse[simp]
       irrefl_on_subset
       irreflp_onD
       irreflp_onI
+      irreflp_on_converse[simp]
       irreflp_on_irrefl_on_eq[pred_set_conv]
       irreflp_on_subset
       linorder.totalp_on_ge[simp]
diff -r 5a13f1519f5d -r d8542bc5a3fa src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Nov 23 10:02:04 2022 +0100
+++ b/src/HOL/Relation.thy	Wed Nov 23 10:23:18 2022 +0100
@@ -988,12 +988,18 @@
 lemma converse_Id_on [simp]: "(Id_on A)\<inverse> = Id_on A"
   by blast
 
-lemma refl_on_converse [simp]: "refl_on A (converse r) = refl_on A r"
+lemma refl_on_converse [simp]: "refl_on A (r\<inverse>) = 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 irrefl_on_converse [simp]: "irrefl_on A (r\<inverse>) = irrefl_on A r"
+  by (simp add: irrefl_on_def)
+
+lemma irreflp_on_converse [simp]: "irreflp_on A (r\<inverse>\<inverse>) = irreflp_on A r"
+  by (rule irrefl_on_converse[to_pred])
+
 lemma sym_converse [simp]: "sym (converse r) = sym r"
   unfolding sym_def by blast