# HG changeset patch
# User desharna
# Date 1672061672 -3600
# Node ID c9e0918672063d7c42036ea027a94ebfc1a091ca
# Parent  2735b11a3de8ec02cf9b9f0b38725ec5433eb131
strengthened and renamed lemmas asym_on_iff_irrefl_on_if_trans and asymp_on_iff_irreflp_on_if_transp

diff -r 2735b11a3de8 -r c9e091867206 NEWS
--- a/NEWS	Mon Dec 26 14:04:06 2022 +0100
+++ b/NEWS	Mon Dec 26 14:34:32 2022 +0100
@@ -74,11 +74,11 @@
       antisymp_on_conversep[simp]
       antisymp_on_if_asymp_on
       antisymp_on_subset
-      asym_on_iff_irrefl_on_if_trans
+      asym_on_iff_irrefl_on_if_trans_on
       asym_onD
       asym_onI
       asym_on_converse[simp]
-      asymp_on_iff_irreflp_on_if_transp
+      asymp_on_iff_irreflp_on_if_transp_on
       asymp_onD
       asymp_onI
       asymp_on_asym_on_eq[pred_set_conv]
diff -r 2735b11a3de8 -r c9e091867206 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Mon Dec 26 14:04:06 2022 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 26 14:34:32 2022 +0100
@@ -718,11 +718,11 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
-lemma asym_on_iff_irrefl_on_if_trans: "trans r \<Longrightarrow> asym_on A r \<longleftrightarrow> irrefl_on A r"
-  by (auto intro: irrefl_onI dest: transD asym_onD irrefl_onD)
+lemma asym_on_iff_irrefl_on_if_trans_on: "trans_on A r \<Longrightarrow> asym_on A r \<longleftrightarrow> irrefl_on A r"
+  by (auto intro: irrefl_on_if_asym_on dest: trans_onD irrefl_onD)
 
-lemma asymp_on_iff_irreflp_on_if_transp: "transp R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
-  by (rule asym_on_iff_irrefl_on_if_trans[to_pred])
+lemma asymp_on_iff_irreflp_on_if_transp_on: "transp_on A R \<Longrightarrow> asymp_on A R \<longleftrightarrow> irreflp_on A R"
+  by (rule asym_on_iff_irrefl_on_if_trans_on[to_pred])
 
 lemma (in preorder) transp_on_le[simp]: "transp_on A (\<le>)"
   by (auto intro: transp_onI order_trans)