# HG changeset patch
# User desharna
# Date 1671433523 -3600
# Node ID cca28679bdbfe57a7978e8646a09a11ce5d54412
# Parent  e260dabc88e65c8e0e7679ec0db971afdfaa7683
added lemmas asym_onI, asymp_onI, asym_onD, and asymp_onD

diff -r e260dabc88e6 -r cca28679bdbf NEWS
--- a/NEWS	Sun Dec 18 14:03:43 2022 +0100
+++ b/NEWS	Mon Dec 19 08:05:23 2022 +0100
@@ -58,7 +58,11 @@
       antisymp_on_antisym_on_eq[pred_set_conv]
       antisymp_on_subset
       asym_if_irrefl_and_trans
+      asym_onD
+      asym_onI
       asymp_if_irreflp_and_transp
+      asymp_onD
+      asymp_onI
       irreflD
       irrefl_onD
       irrefl_onI
diff -r e260dabc88e6 -r cca28679bdbf src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Dec 18 14:03:43 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:05:23 2022 +0100
@@ -347,23 +347,37 @@
 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 (simp add: asymp_on_def asym_on_def)
 
-lemma asymD: "\<lbrakk>asym R; (x,y) \<in> R\<rbrakk> \<Longrightarrow> (y,x) \<notin> R"
+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)
 
+lemma asymI[intro]: "(\<And>x y. (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r) \<Longrightarrow> asym r"
+  by (simp add: asym_onI)
+
+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)
+
+lemma asympI[intro]: "(\<And>x y. R x y \<Longrightarrow> \<not> R y x) \<Longrightarrow> asymp R"
+  by (simp add: asymp_onI)
+
+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)
+
+lemma asymD: "asym r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (y, x) \<notin> r"
+  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)
+
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
 
 lemma asym_iff: "asym R \<longleftrightarrow> (\<forall>x y. (x,y) \<in> R \<longrightarrow> (y,x) \<notin> R)"
-  by (blast intro: asymI dest: asymD)
+  by (blast dest: asymD)
 
 lemma (in preorder) asymp_less[simp]: "asymp (<)"
   by (auto intro: asympI dual_order.asym)