src/HOL/Transitive_Closure.thy
changeset 33656 fc1af6753233
parent 32901 5564af2d0588
child 33878 85102f57b4a8
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Nov 13 11:34:05 2009 +0000
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Nov 13 14:03:24 2009 +0100
     1.3 @@ -575,6 +575,25 @@
     1.4    "(x,y) \<in> R\<^sup>* = (x=y \<or> x\<noteq>y \<and> (x,y) \<in> R\<^sup>+)"
     1.5    by (fast elim: trancl_into_rtrancl dest: rtranclD)
     1.6  
     1.7 +lemma trancl_unfold_right: "r^+ = r^* O r"
     1.8 +by (auto dest: tranclD2 intro: rtrancl_into_trancl1)
     1.9 +
    1.10 +lemma trancl_unfold_left: "r^+ = r O r^*"
    1.11 +by (auto dest: tranclD intro: rtrancl_into_trancl2)
    1.12 +
    1.13 +
    1.14 +text {* Simplifying nested closures *}
    1.15 +
    1.16 +lemma rtrancl_trancl_absorb[simp]: "(R^*)^+ = R^*"
    1.17 +by (simp add: trans_rtrancl)
    1.18 +
    1.19 +lemma trancl_rtrancl_absorb[simp]: "(R^+)^* = R^*"
    1.20 +by (subst reflcl_trancl[symmetric]) simp
    1.21 +
    1.22 +lemma rtrancl_reflcl_absorb[simp]: "(R^*)^= = R^*"
    1.23 +by auto
    1.24 +
    1.25 +
    1.26  text {* @{text Domain} and @{text Range} *}
    1.27  
    1.28  lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"