author krauss Fri Nov 13 14:03:24 2009 +0100 (2009-11-13) changeset 33656 fc1af6753233 parent 33655 c6dde2106128 child 33658 eb8b9c8a3662
a few lemmas for point-free reasoning about transitive closure
```     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"
```