src/HOL/Transitive_Closure.thy
changeset 10996 74e970389def
parent 10980 0a45f2efaaec
child 11084 32c1deea5bcd
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Jan 29 22:25:45 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jan 29 23:02:21 2001 +0100
     1.3 @@ -35,4 +35,52 @@
     1.4  
     1.5  use "Transitive_Closure_lemmas.ML"
     1.6  
     1.7 +
     1.8 +lemma reflcl_trancl[simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
     1.9 +apply safe;
    1.10 +apply (erule trancl_into_rtrancl);
    1.11 +by (blast elim:rtranclE dest:rtrancl_into_trancl1)
    1.12 +
    1.13 +lemma trancl_reflcl[simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
    1.14 +apply safe
    1.15 + apply (drule trancl_into_rtrancl)
    1.16 + apply simp;
    1.17 +apply (erule rtranclE)
    1.18 + apply safe
    1.19 + apply(rule r_into_trancl)
    1.20 + apply simp
    1.21 +apply(rule rtrancl_into_trancl1)
    1.22 + apply(erule rtrancl_reflcl[THEN equalityD2, THEN subsetD])
    1.23 +apply fast
    1.24 +done
    1.25 +
    1.26 +lemma trancl_empty[simp]: "{}\<^sup>+ = {}"
    1.27 +by (auto elim:trancl_induct)
    1.28 +
    1.29 +lemma rtrancl_empty[simp]: "{}\<^sup>* = Id"
    1.30 +by(rule subst[OF reflcl_trancl], simp)
    1.31 +
    1.32 +lemma rtranclD: "(a,b) \<in> R\<^sup>* \<Longrightarrow> a=b \<or> a\<noteq>b \<and> (a,b) \<in> R\<^sup>+"
    1.33 +by(force simp add: reflcl_trancl[THEN sym] simp del: reflcl_trancl)
    1.34 +
    1.35 +(* should be merged with the main body of lemmas: *)
    1.36 +
    1.37 +lemma Domain_rtrancl[simp]: "Domain(R\<^sup>*) = UNIV"
    1.38 +by blast
    1.39 +
    1.40 +lemma Range_rtrancl[simp]: "Range(R\<^sup>*) = UNIV"
    1.41 +by blast
    1.42 +
    1.43 +lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
    1.44 +by(rule rtrancl_Un_rtrancl[THEN subst], fast)
    1.45 +
    1.46 +lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*"
    1.47 +by (blast intro: subsetD[OF rtrancl_Un_subset])
    1.48 +
    1.49 +lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
    1.50 +by (unfold Domain_def, blast dest:tranclD)
    1.51 +
    1.52 +lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
    1.53 +by (simp add:Range_def trancl_converse[THEN sym])
    1.54 +
    1.55  end