# HG changeset patch
# User desharna
# Date 1665325490 -7200
# Node ID 7ae89ee919a7ca33287c8f97986c2863eb5e6a89
# Parent  08f555c6f3b5bfa2feeff4b1449706ee23782161
added lemmas antisym_if_asym and antisymp_if_asymp

diff -r 08f555c6f3b5 -r 7ae89ee919a7 NEWS
--- a/NEWS	Sun Oct 09 16:10:52 2022 +0200
+++ b/NEWS	Sun Oct 09 16:24:50 2022 +0200
@@ -11,7 +11,9 @@
 
 * Theory "HOL.Relation":
   - Strengthened total_on_singleton. Minor INCOMPATIBILITY.
-  - Added lemma.
+  - Added lemmas.
+      antisym_if_asymp
+      antisymp_if_asymp
       totalp_on_singleton[simp]
 
 
diff -r 08f555c6f3b5 -r 7ae89ee919a7 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Oct 09 16:10:52 2022 +0200
+++ b/src/HOL/Relation.thy	Sun Oct 09 16:24:50 2022 +0200
@@ -423,6 +423,12 @@
   "antisym {x}"
   by (blast intro: antisymI)
 
+lemma antisym_if_asym: "asym r \<Longrightarrow> antisym r"
+  by (auto intro: antisymI elim: asym.cases)
+
+lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
+  by (rule antisym_if_asym[to_pred])
+
 
 subsubsection \<open>Transitivity\<close>