# HG changeset patch
# User desharna
# Date 1671096261 -3600
# Node ID e772c8e6edd07e3ac4976a2977e720b71662c7c7
# Parent  833bae85ac2d63866295e683fd1df908fe317f46
added predicates antisym_on and antisymp_on and redefined antisym and antisymp to be abbreviations

diff -r 833bae85ac2d -r e772c8e6edd0 NEWS
--- a/NEWS	Tue Dec 13 11:29:52 2022 +0100
+++ b/NEWS	Thu Dec 15 10:24:21 2022 +0100
@@ -30,6 +30,10 @@
     irreflp to be abbreviations. Lemmas irrefl_def and irreflp_def are
     explicitly provided for backward compatibility but their usage is
     discouraged. Minor INCOMPATIBILITY.
+  - Added predicates antisym_on and antisymp_on and redefined antisym and
+    antisymp to be abbreviations. Lemmas antisym_def and antisymp_def are
+    explicitly provided for backward compatibility but their usage is
+    discouraged. Minor INCOMPATIBILITY.
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       preorder.irreflp_greater[simp] ~> preorder.irreflp_on_greater[simp]
       preorder.irreflp_less[simp] ~> preorder.irreflp_on_less[simp]
diff -r 833bae85ac2d -r e772c8e6edd0 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Dec 13 11:29:52 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Dec 15 10:24:21 2022 +0100
@@ -423,11 +423,25 @@
 
 subsubsection \<open>Antisymmetry\<close>
 
-definition antisym :: "'a rel \<Rightarrow> bool"
-  where "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
+definition antisym_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "antisym_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
+
+abbreviation antisym :: "'a rel \<Rightarrow> bool" where
+  "antisym \<equiv> antisym_on UNIV"
+
+definition antisymp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "antisymp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. R x y \<longrightarrow> R y x \<longrightarrow> x = y)"
 
-definition antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where "antisymp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> r y x \<longrightarrow> x = y)"
+abbreviation antisymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "antisymp \<equiv> antisymp_on UNIV"
+
+lemma antisym_def[no_atp]: "antisym r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (y, x) \<in> r \<longrightarrow> x = y)"
+  by (simp add: antisym_on_def)
+
+lemma antisymp_def[no_atp]: "antisymp R \<longleftrightarrow> (\<forall>x y. R x y \<longrightarrow> R y x \<longrightarrow> x = y)"
+  by (simp add: antisymp_on_def)
+
+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)