--- 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
--- 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