# HG changeset patch
# User desharna
# Date 1671368623 -3600
# Node ID e260dabc88e65c8e0e7679ec0db971afdfaa7683
# Parent  f572f5525e4bb49194a9a8bcc366c6e913dd187b
added predicates asym_on and asymp_on and redefined asym and asymp to be abbreviations

diff -r f572f5525e4b -r e260dabc88e6 NEWS
--- a/NEWS	Sun Dec 18 13:53:05 2022 +0100
+++ b/NEWS	Sun Dec 18 14:03:43 2022 +0100
@@ -34,6 +34,8 @@
     symp to be abbreviations. Lemmas sym_def and symp_def are explicitly
     provided for backward compatibility but their usage is discouraged.
     Minor INCOMPATIBILITY.
+  - Added predicates asym_on and asymp_on and redefined asym and
+    asymp to be abbreviations. 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
diff -r f572f5525e4b -r e260dabc88e6 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sun Dec 18 13:53:05 2022 +0100
+++ b/src/HOL/Library/Multiset.thy	Sun Dec 18 14:03:43 2022 +0100
@@ -3403,7 +3403,7 @@
   from assms obtain a M0 K where "M = add_mset a M0" "N = M0 + K" and
     *: "b \<in># K \<Longrightarrow> r b a" for b by (blast elim: mult1E)
   moreover from * [of a] have "a \<notin># K"
-    using \<open>asymp r\<close> by (meson asymp.cases)
+    using \<open>asymp r\<close> by (meson asympD)
   ultimately show thesis by (auto intro: that)
 qed
 
diff -r f572f5525e4b -r e260dabc88e6 src/HOL/Library/Multiset_Order.thy
--- a/src/HOL/Library/Multiset_Order.thy	Sun Dec 18 13:53:05 2022 +0100
+++ b/src/HOL/Library/Multiset_Order.thy	Sun Dec 18 14:03:43 2022 +0100
@@ -55,7 +55,7 @@
     using \<open>asymp r\<close> by (auto elim: mult1_lessE)
   from \<open>M \<noteq> N\<close> ** *(1,2,3) have "M \<noteq> P"
     using *(4) \<open>asymp r\<close>
-    by (metis asymp.cases add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
+    by (metis asympD add_cancel_right_right add_diff_cancel_left' add_mset_add_single count_inI
         count_union diff_diff_add_mset diff_single_trivial in_diff_count multi_member_last)
   moreover
   { assume "count P a \<le> count M a"
@@ -65,7 +65,7 @@
         by blast
       with * have "count N z \<le> count P z"
         using \<open>asymp r\<close>
-        by (metis add_diff_cancel_left' add_mset_add_single asymp.cases diff_diff_add_mset
+        by (metis add_diff_cancel_left' add_mset_add_single asympD diff_diff_add_mset
             diff_single_trivial in_diff_count not_le_imp_less)
       with z have "\<exists>z. r a z \<and> count M z < count P z" by auto
   } note count_a = this
diff -r f572f5525e4b -r e260dabc88e6 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Dec 18 13:53:05 2022 +0100
+++ b/src/HOL/List.thy	Sun Dec 18 14:03:43 2022 +0100
@@ -6986,7 +6986,7 @@
   next
     case (Cons x xs)
     then obtain z zs where ys: "ys = z # zs" by (cases ys) auto
-    with assms Cons show ?case by (auto elim: asym.cases)
+    with assms Cons show ?case by (auto dest: asymD)
   qed
 qed
 
@@ -6996,11 +6996,11 @@
   shows "(b, a) \<notin> lexord R"
 proof -
   from \<open>asym R\<close> have "asym (lexord R)" by (rule lexord_asym)
-  then show ?thesis by (rule asym.cases) (auto simp add: hyp)
+  then show ?thesis by (auto simp: hyp dest: asymD)
 qed
 
 lemma asym_lex: "asym R \<Longrightarrow> asym (lex R)"
-  by (meson asym.simps irrefl_lex lexord_asym lexord_lex)
+  by (meson asymI asymD irrefl_lex lexord_asym lexord_lex)
 
 lemma asym_lenlex: "asym R \<Longrightarrow> asym (lenlex R)"
   by (simp add: lenlex_def asym_inv_image asym_less_than asym_lex asym_lex_prod)
diff -r f572f5525e4b -r e260dabc88e6 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Dec 18 13:53:05 2022 +0100
+++ b/src/HOL/Relation.thy	Sun Dec 18 14:03:43 2022 +0100
@@ -332,19 +332,32 @@
 lemma (in preorder) irreflp_on_greater[simp]: "irreflp_on A (>)"
   by (simp add: irreflp_onI)
 
+
 subsubsection \<open>Asymmetry\<close>
 
-inductive asym :: "'a rel \<Rightarrow> bool"
-  where asymI: "(\<And>a b. (a, b) \<in> R \<Longrightarrow> (b, a) \<notin> R) \<Longrightarrow> asym R"
+definition asym_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool" where
+  "asym_on A r \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. (x, y) \<in> r \<longrightarrow> (y, x) \<notin> r)"
+
+abbreviation asym :: "'a rel \<Rightarrow> bool" where
+  "asym \<equiv> asym_on UNIV"
+
+definition asymp_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "asymp_on A R \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> A. R x y \<longrightarrow> \<not> R y x)"
 
-inductive asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
-  where asympI: "(\<And>a b. R a b \<Longrightarrow> \<not> R b a) \<Longrightarrow> asymp R"
+abbreviation asymp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool" where
+  "asymp \<equiv> asymp_on UNIV"
+
+lemma asymI[intro]: "(\<And>x y. (x, y) \<in> R \<Longrightarrow> (y, x) \<notin> R) \<Longrightarrow> asym R"
+  by (simp add: asym_on_def)
+
+lemma asympI[intro]: "(\<And>x y. R x y \<Longrightarrow> \<not> R y x) \<Longrightarrow> asymp R"
+  by (simp add: asymp_on_def)
 
 lemma asymp_asym_eq [pred_set_conv]: "asymp (\<lambda>a b. (a, b) \<in> R) \<longleftrightarrow> asym R"
-  by (auto intro!: asymI asympI elim: asym.cases asymp.cases simp add: irreflp_irrefl_eq)
+  by (simp add: asymp_on_def asym_on_def)
 
 lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
-  by (simp add: asym.simps)
+  by (simp add: asym_on_def)
 
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
@@ -542,7 +555,7 @@
   by (blast intro: antisymI)
 
 lemma antisym_if_asym: "asym r \<Longrightarrow> antisym r"
-  by (auto intro: antisymI elim: asym.cases)
+  by (auto intro: antisymI dest: asymD)
 
 lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
   by (rule antisym_if_asym[to_pred])
diff -r f572f5525e4b -r e260dabc88e6 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sun Dec 18 13:53:05 2022 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Dec 18 14:03:43 2022 +0100
@@ -604,7 +604,7 @@
   using irrefl_def by blast
 
 lemma asym_less_than: "asym less_than"
-  by (simp add: asym.simps irrefl_less_than)
+  by (rule asymI) simp
 
 lemma total_less_than: "total less_than" and total_on_less_than [simp]: "total_on A less_than"
   using total_on_def by force+