--- a/NEWS Thu Dec 15 10:24:21 2022 +0100
+++ b/NEWS Thu Dec 15 10:25:55 2022 +0100
@@ -42,6 +42,7 @@
- Added lemmas.
antisym_if_asymp
antisymp_if_asymp
+ antisymp_on_antisym_on_eq[pred_set_conv]
asym_if_irrefl_and_trans
asymp_if_irreflp_and_transp
irreflD
--- a/src/HOL/Relation.thy Thu Dec 15 10:24:21 2022 +0100
+++ b/src/HOL/Relation.thy Thu Dec 15 10:25:55 2022 +0100
@@ -443,8 +443,11 @@
text \<open>@{thm [source] antisym_def} and @{thm [source] antisymp_def} are for backward compatibility.\<close>
-lemma antisymp_antisym_eq [pred_set_conv]: "antisymp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym r"
- by (simp add: antisym_def antisymp_def)
+lemma antisymp_on_antisym_on_eq[pred_set_conv]:
+ "antisymp_on A (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> antisym_on A r"
+ by (simp add: antisym_on_def antisymp_on_def)
+
+lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV]
lemma antisymI [intro?]:
"(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<in> r \<Longrightarrow> x = y) \<Longrightarrow> antisym r"