src/HOL/Transitive_Closure.thy
changeset 11084 32c1deea5bcd
parent 10996 74e970389def
child 11090 3041d0347d26
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Feb 07 20:57:03 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Feb 09 11:40:10 2001 +0100
     1.3 @@ -36,51 +36,53 @@
     1.4  use "Transitive_Closure_lemmas.ML"
     1.5  
     1.6  
     1.7 -lemma reflcl_trancl[simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
     1.8 -apply safe;
     1.9 -apply (erule trancl_into_rtrancl);
    1.10 -by (blast elim:rtranclE dest:rtrancl_into_trancl1)
    1.11 +lemma reflcl_trancl [simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
    1.12 +  apply safe
    1.13 +  apply (erule trancl_into_rtrancl)
    1.14 +  apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    1.15 +  done
    1.16  
    1.17 -lemma trancl_reflcl[simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
    1.18 -apply safe
    1.19 - apply (drule trancl_into_rtrancl)
    1.20 - apply simp;
    1.21 -apply (erule rtranclE)
    1.22 - apply safe
    1.23 - apply(rule r_into_trancl)
    1.24 - apply simp
    1.25 -apply(rule rtrancl_into_trancl1)
    1.26 - apply(erule rtrancl_reflcl[THEN equalityD2, THEN subsetD])
    1.27 -apply fast
    1.28 -done
    1.29 +lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
    1.30 +  apply safe
    1.31 +   apply (drule trancl_into_rtrancl)
    1.32 +   apply simp
    1.33 +  apply (erule rtranclE)
    1.34 +   apply safe
    1.35 +   apply (rule r_into_trancl)
    1.36 +   apply simp
    1.37 +  apply (rule rtrancl_into_trancl1)
    1.38 +   apply (erule rtrancl_reflcl [THEN equalityD2, THEN subsetD])
    1.39 +  apply fast
    1.40 +  done
    1.41  
    1.42 -lemma trancl_empty[simp]: "{}\<^sup>+ = {}"
    1.43 -by (auto elim:trancl_induct)
    1.44 +lemma trancl_empty [simp]: "{}\<^sup>+ = {}"
    1.45 +  by (auto elim: trancl_induct)
    1.46  
    1.47 -lemma rtrancl_empty[simp]: "{}\<^sup>* = Id"
    1.48 -by(rule subst[OF reflcl_trancl], simp)
    1.49 +lemma rtrancl_empty [simp]: "{}\<^sup>* = Id"
    1.50 +  by (rule subst [OF reflcl_trancl]) simp
    1.51  
    1.52 -lemma rtranclD: "(a,b) \<in> R\<^sup>* \<Longrightarrow> a=b \<or> a\<noteq>b \<and> (a,b) \<in> R\<^sup>+"
    1.53 -by(force simp add: reflcl_trancl[THEN sym] simp del: reflcl_trancl)
    1.54 +lemma rtranclD: "(a, b) \<in> R\<^sup>* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R\<^sup>+"
    1.55 +  by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
    1.56 +
    1.57  
    1.58  (* should be merged with the main body of lemmas: *)
    1.59  
    1.60 -lemma Domain_rtrancl[simp]: "Domain(R\<^sup>*) = UNIV"
    1.61 -by blast
    1.62 +lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV"
    1.63 +  by blast
    1.64  
    1.65 -lemma Range_rtrancl[simp]: "Range(R\<^sup>*) = UNIV"
    1.66 -by blast
    1.67 +lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV"
    1.68 +  by blast
    1.69  
    1.70  lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
    1.71 -by(rule rtrancl_Un_rtrancl[THEN subst], fast)
    1.72 +  by (rule rtrancl_Un_rtrancl [THEN subst]) fast
    1.73  
    1.74 -lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* \<Longrightarrow> x \<in> (R \<union> S)\<^sup>*"
    1.75 -by (blast intro: subsetD[OF rtrancl_Un_subset])
    1.76 +lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* ==> x \<in> (R \<union> S)\<^sup>*"
    1.77 +  by (blast intro: subsetD [OF rtrancl_Un_subset])
    1.78  
    1.79  lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
    1.80 -by (unfold Domain_def, blast dest:tranclD)
    1.81 +  by (unfold Domain_def) (blast dest: tranclD)
    1.82  
    1.83  lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
    1.84 -by (simp add:Range_def trancl_converse[THEN sym])
    1.85 +  by (simp add: Range_def trancl_converse [symmetric])
    1.86  
    1.87  end