# HG changeset patch
# User desharna
# Date 1671435423 -3600
# Node ID 98880b2430ea800488a8cf17a11eea825e1862d9
# Parent  0c6aa6c27ba4c2b1e8a10088e75775de23681dc8
strengthened and renamed lemma antisym_converse and added lemma antisymp_on_conversep

diff -r 0c6aa6c27ba4 -r 98880b2430ea NEWS
--- a/NEWS	Mon Dec 19 08:34:32 2022 +0100
+++ b/NEWS	Mon Dec 19 08:37:03 2022 +0100
@@ -50,6 +50,7 @@
       reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
       sym_converse[simp] ~> sym_on_converse[simp]
+      antisym_converse[simp] ~> antisym_on_converse[simp]
   - Added lemmas.
       antisym_onD
       antisym_onI
@@ -58,6 +59,7 @@
       antisymp_onD
       antisymp_onI
       antisymp_on_antisym_on_eq[pred_set_conv]
+      antisymp_on_conversep[simp]
       antisymp_on_if_asymp_on
       antisymp_on_subset
       asym_if_irrefl_and_trans
diff -r 0c6aa6c27ba4 -r 98880b2430ea src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:34:32 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:37:03 2022 +0100
@@ -1122,8 +1122,11 @@
 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
+lemma antisym_on_converse [simp]: "antisym_on A (r\<inverse>) = antisym_on A r"
+  by (auto intro: antisym_onI dest: antisym_onD)
+
+lemma antisymp_on_conversep [simp]: "antisymp_on A R\<inverse>\<inverse> = antisymp_on A R"
+  by (rule antisym_on_converse[to_pred])
 
 lemma trans_converse [simp]: "trans (converse r) = trans r"
   unfolding trans_def by blast