--- a/src/HOL/Transitive_Closure.thy Mon Mar 04 21:58:53 2024 +0100
+++ b/src/HOL/Transitive_Closure.thy Tue Mar 05 15:02:31 2024 +0100
@@ -321,6 +321,27 @@
then show ?thesis by auto
qed
+lemma rtranclp_ident_if_reflp_and_transp:
+ assumes "reflp R" and "transp R"
+ shows "R\<^sup>*\<^sup>* = R"
+proof (intro ext iffI)
+ fix x y
+ show "R\<^sup>*\<^sup>* x y \<Longrightarrow> R x y"
+ proof (induction y rule: rtranclp_induct)
+ case base
+ show ?case
+ using \<open>reflp R\<close>[THEN reflpD] .
+ next
+ case (step y z)
+ thus ?case
+ using \<open>transp R\<close>[THEN transpD, of x y z] by simp
+ qed
+next
+ fix x y
+ show "R x y \<Longrightarrow> R\<^sup>*\<^sup>* x y"
+ using r_into_rtranclp .
+qed
+
subsection \<open>Transitive closure\<close>
@@ -735,6 +756,28 @@
declare trancl_into_rtrancl [elim]
+lemma tranclp_ident_if_transp:
+ assumes "transp R"
+ shows "R\<^sup>+\<^sup>+ = R"
+proof (intro ext iffI)
+ fix x y
+ show "R\<^sup>+\<^sup>+ x y \<Longrightarrow> R x y"
+ proof (induction y rule: tranclp_induct)
+ case (base y)
+ thus ?case
+ by simp
+ next
+ case (step y z)
+ thus ?case
+ using \<open>transp R\<close>[THEN transpD, of x y z] by simp
+ qed
+next
+ fix x y
+ show "R x y \<Longrightarrow> R\<^sup>+\<^sup>+ x y"
+ using tranclp.r_into_trancl .
+qed
+
+
subsection \<open>Symmetric closure\<close>
definition symclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"