added lemmas irrefl_on_converse[simp] and irreflp_on_converse[simp]

--- 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]

--- 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