# HG changeset patch
# User desharna
# Date 1710923052 -3600
# Node ID d26c53bc6ce14f18f9ba3fa3f9d72d9ece72e98d
# Parent  7bac6bd83cc31a25ae0fc56e349bf32d9f8e437f
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on

diff -r 7bac6bd83cc3 -r d26c53bc6ce1 NEWS
--- a/NEWS	Tue Mar 19 13:24:22 2024 +0100
+++ b/NEWS	Wed Mar 20 09:24:12 2024 +0100
@@ -77,6 +77,8 @@
 
 * Theory "HOL.Transitive_Closure":
   - Added lemmas.
+      antisym_on_reflcl_if_asym_on
+      antisymp_on_reflclp_if_asymp_on
       reflclp_greater_eq[simp]
       reflclp_less_eq[simp]
       relpow_left_unique
diff -r 7bac6bd83cc3 -r d26c53bc6ce1 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Tue Mar 19 13:24:22 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy	Wed Mar 20 09:24:12 2024 +0100
@@ -88,6 +88,33 @@
 lemma transp_on_reflclp[simp]: "transp_on A R \<Longrightarrow> transp_on A R\<^sup>=\<^sup>="
   by (rule trans_on_reflcl[to_pred])
 
+lemma antisymp_on_reflclp_if_asymp_on:
+  assumes "asymp_on A R"
+  shows "antisymp_on A R\<^sup>=\<^sup>="
+proof (rule antisymp_onI)
+  fix x y
+  assume "x \<in> A" and "y \<in> A" and "R\<^sup>=\<^sup>= x y" and "R\<^sup>=\<^sup>= y x"
+  show "x = y"
+  proof (cases "x = y")
+    case True
+    thus ?thesis .
+  next
+    case False
+    hence "R x y"
+      using \<open>R\<^sup>=\<^sup>= x y\<close> by simp
+    hence "\<not> R y x"
+      using \<open>asymp_on A R\<close>[THEN asymp_onD, OF \<open>x \<in> A\<close> \<open>y \<in> A\<close>] by iprover
+    moreover have "R y x"
+      using \<open>R\<^sup>=\<^sup>= y x\<close> False by simp
+    ultimately have False
+      by contradiction
+    thus ?thesis ..
+  qed
+qed
+
+lemma antisym_on_reflcl_if_asym_on: "asym_on A R \<Longrightarrow> antisym_on A (R\<^sup>=)"
+  using antisymp_on_reflclp_if_asymp_on[to_set] .
+
 lemma reflclp_idemp [simp]: "(P\<^sup>=\<^sup>=)\<^sup>=\<^sup>= = P\<^sup>=\<^sup>="
   by blast