# HG changeset patch
# User desharna
# Date 1710923185 -3600
# Node ID 890c250feab79494d2006f78de7f664627b8a14d
# Parent  d26c53bc6ce14f18f9ba3fa3f9d72d9ece72e98d
added lemma order_reflclp_if_transp_and_asymp

diff -r d26c53bc6ce1 -r 890c250feab7 NEWS
--- a/NEWS	Wed Mar 20 09:24:12 2024 +0100
+++ b/NEWS	Wed Mar 20 09:26:25 2024 +0100
@@ -79,6 +79,7 @@
   - Added lemmas.
       antisym_on_reflcl_if_asym_on
       antisymp_on_reflclp_if_asymp_on
+      order_reflclp_if_transp_and_asymp
       reflclp_greater_eq[simp]
       reflclp_less_eq[simp]
       relpow_left_unique
diff -r d26c53bc6ce1 -r 890c250feab7 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Wed Mar 20 09:24:12 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Mar 20 09:26:25 2024 +0100
@@ -130,6 +130,23 @@
 lemma (in preorder) reflclp_greater_eq[simp]: "(\<ge>)\<^sup>=\<^sup>= = (\<ge>)"
   using reflp_on_ge by (simp only: reflclp_ident_if_reflp)
 
+lemma order_reflclp_if_transp_and_asymp:
+  assumes "transp R" and "asymp R"
+  shows "class.order R\<^sup>=\<^sup>= R"
+proof unfold_locales
+  show "\<And>x y. R x y = (R\<^sup>=\<^sup>= x y \<and> \<not> R\<^sup>=\<^sup>= y x)"
+    using \<open>asymp R\<close> asympD by fastforce
+next
+  show "\<And>x. R\<^sup>=\<^sup>= x x"
+    by simp
+next
+  show "\<And>x y z. R\<^sup>=\<^sup>= x y \<Longrightarrow> R\<^sup>=\<^sup>= y z \<Longrightarrow> R\<^sup>=\<^sup>= x z"
+    using transp_on_reflclp[OF \<open>transp R\<close>, THEN transpD] .
+next
+  show "\<And>x y. R\<^sup>=\<^sup>= x y \<Longrightarrow> R\<^sup>=\<^sup>= y x \<Longrightarrow> x = y"
+    using antisymp_on_reflclp_if_asymp_on[OF \<open>asymp R\<close>, THEN antisympD] .
+qed
+
 
 subsection \<open>Reflexive-transitive closure\<close>