--- 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
--- 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])