# HG changeset patch
# User desharna
# Date 1671434210 -3600
# Node ID 87e7ab6aa40b09b561eb72ca52adaec940fa2ef1
# Parent  a84716ca8b978c3e222d49d630b9d39c07a1e720
strengthened lemmas antisym_on_if_asym_on and antisymp_on_if_asymp_on

diff -r a84716ca8b97 -r 87e7ab6aa40b NEWS
--- a/NEWS	Mon Dec 19 08:14:43 2022 +0100
+++ b/NEWS	Mon Dec 19 08:16:50 2022 +0100
@@ -50,11 +50,11 @@
       reflp_equality[simp] ~> reflp_on_equality[simp]
       total_on_singleton
   - Added lemmas.
-      antisym_if_asymp
+      antisym_on_if_asymp_on
       antisym_onD
       antisym_onI
       antisym_on_subset
-      antisymp_if_asymp
+      antisymp_on_if_asymp_on
       antisymp_onD
       antisymp_onI
       antisymp_on_antisym_on_eq[pred_set_conv]
diff -r a84716ca8b97 -r 87e7ab6aa40b src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 19 08:14:43 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 19 08:16:50 2022 +0100
@@ -576,17 +576,17 @@
   "antisym {x}"
   by (blast intro: antisymI)
 
-lemma antisym_if_asym: "asym r \<Longrightarrow> antisym r"
-  by (auto intro: antisymI dest: asymD)
+lemma antisym_on_if_asym_on: "asym_on A r \<Longrightarrow> antisym_on A r"
+  by (auto intro: antisym_onI dest: asym_onD)
 
-lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
-  by (rule antisym_if_asym[to_pred])
+lemma antisymp_on_if_asymp_on: "asymp_on A R \<Longrightarrow> antisymp_on A R"
+  by (rule antisym_on_if_asym_on[to_pred])
 
 lemma (in preorder) antisymp_less[simp]: "antisymp (<)"
-  by (rule antisymp_if_asymp[OF asymp_on_less])
+  by (rule antisymp_on_if_asymp_on[OF asymp_on_less])
 
 lemma (in preorder) antisymp_greater[simp]: "antisymp (>)"
-  by (rule antisymp_if_asymp[OF asymp_on_greater])
+  by (rule antisymp_on_if_asymp_on[OF asymp_on_greater])
 
 lemma (in order) antisymp_on_le[simp]: "antisymp_on A (\<le>)"
   by (simp add: antisymp_onI)