# HG changeset patch
# User desharna
# Date 1671434063 -3600
# Node ID 10c4aa9eecf88db834d38139ec60f534edce8737
# Parent  806d0b3aebafaf605498f61a93113262fa1aa17e
added lemma asymp_on_asym_on_eq[pred_set_conv]

diff -r 806d0b3aebaf -r 10c4aa9eecf8 NEWS
--- a/NEWS	Mon Dec 19 08:07:36 2022 +0100
+++ b/NEWS	Mon Dec 19 08:14:23 2022 +0100
@@ -65,6 +65,7 @@
       asymp_if_irreflp_and_transp
       asymp_onD
       asymp_onI
+      asymp_on_asym_on_eq[pred_set_conv]
       irreflD
       irrefl_onD
       irrefl_onI
diff -r 806d0b3aebaf -r 10c4aa9eecf8 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:07:36 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:14:23 2022 +0100
@@ -347,9 +347,11 @@
 abbreviation asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
   "asymp \<equiv> asymp_on UNIV"
 
-lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R"
+lemma asymp_on_asym_on_eq[pred_set_conv]: "asymp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> asym_on A r"
   by (simp add: asymp_on_def asym_on_def)
 
+lemmas asymp_asym_eq = asymp_on_asym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
+
 lemma asym_onI[intro]:
   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r) \<Longrightarrow> asym_on A r"
   by (simp add: asym_on_def)
@@ -359,10 +361,10 @@
 
 lemma asymp_onI[intro]:
   "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x) \<Longrightarrow> asymp_on A R"
-  by (simp add: asymp_on_def)
+  by (rule asym_onI[to_pred])
 
 lemma asympI[intro]: "(\<And>x y. R x y \<Longrightarrow> \<not> R y x) \<Longrightarrow> asymp R"
-  by (simp add: asymp_onI)
+  by (rule asymI[to_pred])
 
 lemma asym_onD: "asym_on A r \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r"
   by (simp add: asym_on_def)
@@ -371,7 +373,7 @@
   by (simp add: asym_onD)
 
 lemma asymp_onD: "asymp_on A R \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
-  by (simp add: asymp_on_def)
+  by (rule asym_onD[to_pred])
 
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])