# HG changeset patch
# User desharna
# Date 1669280546 -3600
# Node ID 7bc934b99faf7b0259ef3a0ea22646dc2c1b5d1b
# Parent  cbf38b7cb195dc3e3157e1fa1cf4d71b7128e1ae
added lemmas asym_if_irrefl_and_trans and asymp_if_irreflp_and_transp

diff -r cbf38b7cb195 -r 7bc934b99faf NEWS
--- a/NEWS	Wed Nov 23 10:27:24 2022 +0100
+++ b/NEWS	Thu Nov 24 10:02:26 2022 +0100
@@ -38,6 +38,8 @@
   - Added lemmas.
       antisym_if_asymp
       antisymp_if_asymp
+      asym_if_irrefl_and_trans
+      asymp_if_irreflp_and_transp
       irrefl_onD
       irrefl_onI
       irrefl_on_converse[simp]
diff -r cbf38b7cb195 -r 7bc934b99faf src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Wed Nov 23 10:27:24 2022 +0100
+++ b/src/HOL/Relation.thy	Thu Nov 24 10:02:26 2022 +0100
@@ -561,6 +561,12 @@
 lemma transp_singleton [simp]: "transp (\<lambda>x y. x = a \<and> y = a)"
   by (simp add: transp_def)
 
+lemma asym_if_irrefl_and_trans: "irrefl R \<Longrightarrow> trans R \<Longrightarrow> asym R"
+  by (auto intro: asymI dest: transD irreflD)
+
+lemma asymp_if_irreflp_and_transp: "irreflp R \<Longrightarrow> transp R \<Longrightarrow> asymp R"
+  by (rule asym_if_irrefl_and_trans[to_pred])
+
 context preorder
 begin