# HG changeset patch
# User desharna
# Date 1641816678 -3600
# Node ID 5d3a846bccf83678652cecb42c2322336325845c
# Parent  a565a2889b49f2a15487398bdc96d28a85e6e442
added lemma asympD

diff -r a565a2889b49 -r 5d3a846bccf8 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Jan 09 18:50:06 2022 +0000
+++ b/src/HOL/Relation.thy	Mon Jan 10 13:11:18 2022 +0100
@@ -261,19 +261,18 @@
 lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
   by (simp add: asym.simps)
 
+lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
+  by (rule asymD[to_pred])
+
 lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
   by (blast intro: asymI dest: asymD)
 
-context preorder begin
-
-lemma asymp_less[simp]: "asymp (<)"
+lemma (in preorder) asymp_less[simp]: "asymp (<)"
   by (auto intro: asympI dual_order.asym)
 
-lemma asymp_greater[simp]: "asymp (>)"
+lemma (in preorder) asymp_greater[simp]: "asymp (>)"
   by (auto intro: asympI dual_order.asym)
 
-end
-
 
 subsubsection \<open>Symmetry\<close>