--- a/src/HOL/Transitive_Closure.thy Wed Mar 20 09:26:25 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Mar 20 09:57:14 2024 +0100
@@ -91,26 +91,8 @@
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
+ unfolding antisymp_on_reflcp
+ using antisymp_on_if_asymp_on[OF \<open>asymp_on A R\<close>] .
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] .