# HG changeset patch
# User krauss
# Date 1258117404 -3600
# Node ID fc1af67532334c0e9f10cdd96e9f70baf50a8ee4
# Parent  c6dde2106128d4022fe03a442efc1165910eb74e
a few lemmas for point-free reasoning about transitive closure

diff -r c6dde2106128 -r fc1af6753233 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Nov 13 11:34:05 2009 +0000
+++ b/src/HOL/Transitive_Closure.thy	Fri Nov 13 14:03:24 2009 +0100
@@ -575,6 +575,25 @@
   "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
   by (fast elim: trancl_into_rtrancl dest: rtranclD)
 
+lemma trancl_unfold_right: "r^+ = r^* O r"
+by (auto dest: tranclD2 intro: rtrancl_into_trancl1)
+
+lemma trancl_unfold_left: "r^+ = r O r^*"
+by (auto dest: tranclD intro: rtrancl_into_trancl2)
+
+
+text {* Simplifying nested closures *}
+
+lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*"
+by (simp add: trans_rtrancl)
+
+lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*"
+by (subst reflcl_trancl[symmetric]) simp
+
+lemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*"
+by auto
+
+
 text {* @{text Domain} and @{text Range} *}
 
 lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"