# HG changeset patch
# User desharna
# Date 1671435272 -3600
# Node ID 0c6aa6c27ba4c2b1e8a10088e75775de23681dc8
# Parent  da062f9f2e53adc759003817cd399d5dc041a046
added lemmas asym_on_converse[simp] and asymp_on_conversep[simp]

diff -r da062f9f2e53 -r 0c6aa6c27ba4 NEWS
--- a/NEWS	Mon Dec 19 08:30:44 2022 +0100
+++ b/NEWS	Mon Dec 19 08:34:32 2022 +0100
@@ -51,22 +51,24 @@
       total_on_singleton
       sym_converse[simp] ~> sym_on_converse[simp]
   - Added lemmas.
-      antisym_on_if_asymp_on
       antisym_onD
       antisym_onI
+      antisym_on_if_asymp_on
       antisym_on_subset
-      antisymp_on_if_asymp_on
       antisymp_onD
       antisymp_onI
       antisymp_on_antisym_on_eq[pred_set_conv]
+      antisymp_on_if_asymp_on
       antisymp_on_subset
       asym_if_irrefl_and_trans
       asym_onD
       asym_onI
+      asym_on_converse[simp]
       asymp_if_irreflp_and_transp
       asymp_onD
       asymp_onI
       asymp_on_asym_on_eq[pred_set_conv]
+      asymp_on_conversep[simp]
       irreflD
       irrefl_onD
       irrefl_onI
diff -r da062f9f2e53 -r 0c6aa6c27ba4 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:30:44 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:34:32 2022 +0100
@@ -1116,6 +1116,12 @@
 lemma symp_on_conversep [simp]: "symp_on A R\<inverse>\<inverse> = symp_on A R"
   by (rule sym_on_converse[to_pred])
 
+lemma asym_on_converse [simp]: "asym_on A (r\<inverse>) = asym_on A r"
+  by (auto dest: asym_onD)
+
+lemma asymp_on_conversep [simp]: "asymp_on A R\<inverse>\<inverse> = asymp_on A R"
+  by (rule asym_on_converse[to_pred])
+
 lemma antisym_converse [simp]: "antisym (converse r) = antisym r"
   unfolding antisym_def by blast