src/HOL/Transitive_Closure.thy
changeset 11090 3041d0347d26
parent 11084 32c1deea5bcd
child 11115 285b31e9e026
     1.1 --- a/src/HOL/Transitive_Closure.thy	Fri Feb 09 23:48:33 2001 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Feb 09 23:48:50 2001 +0100
     1.3 @@ -36,13 +36,13 @@
     1.4  use "Transitive_Closure_lemmas.ML"
     1.5  
     1.6  
     1.7 -lemma reflcl_trancl [simp]: "(r\<^sup>+)\<^sup>= = r\<^sup>*"
     1.8 +lemma reflcl_trancl [simp]: "(r^+)^= = r^*"
     1.9    apply safe
    1.10    apply (erule trancl_into_rtrancl)
    1.11    apply (blast elim: rtranclE dest: rtrancl_into_trancl1)
    1.12    done
    1.13  
    1.14 -lemma trancl_reflcl [simp]: "(r\<^sup>=)\<^sup>+ = r\<^sup>*"
    1.15 +lemma trancl_reflcl [simp]: "(r^=)^+ = r^*"
    1.16    apply safe
    1.17     apply (drule trancl_into_rtrancl)
    1.18     apply simp
    1.19 @@ -55,34 +55,34 @@
    1.20    apply fast
    1.21    done
    1.22  
    1.23 -lemma trancl_empty [simp]: "{}\<^sup>+ = {}"
    1.24 +lemma trancl_empty [simp]: "{}^+ = {}"
    1.25    by (auto elim: trancl_induct)
    1.26  
    1.27 -lemma rtrancl_empty [simp]: "{}\<^sup>* = Id"
    1.28 +lemma rtrancl_empty [simp]: "{}^* = Id"
    1.29    by (rule subst [OF reflcl_trancl]) simp
    1.30  
    1.31 -lemma rtranclD: "(a, b) \<in> R\<^sup>* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R\<^sup>+"
    1.32 +lemma rtranclD: "(a, b) \<in> R^* ==> a = b \<or> a \<noteq> b \<and> (a, b) \<in> R^+"
    1.33    by (force simp add: reflcl_trancl [symmetric] simp del: reflcl_trancl)
    1.34  
    1.35  
    1.36  (* should be merged with the main body of lemmas: *)
    1.37  
    1.38 -lemma Domain_rtrancl [simp]: "Domain (R\<^sup>*) = UNIV"
    1.39 +lemma Domain_rtrancl [simp]: "Domain (R^*) = UNIV"
    1.40    by blast
    1.41  
    1.42 -lemma Range_rtrancl [simp]: "Range (R\<^sup>*) = UNIV"
    1.43 +lemma Range_rtrancl [simp]: "Range (R^*) = UNIV"
    1.44    by blast
    1.45  
    1.46 -lemma rtrancl_Un_subset: "(R\<^sup>* \<union> S\<^sup>*) \<subseteq> (R Un S)\<^sup>*"
    1.47 +lemma rtrancl_Un_subset: "(R^* \<union> S^*) \<subseteq> (R Un S)^*"
    1.48    by (rule rtrancl_Un_rtrancl [THEN subst]) fast
    1.49  
    1.50 -lemma in_rtrancl_UnI: "x \<in> R\<^sup>* \<or> x \<in> S\<^sup>* ==> x \<in> (R \<union> S)\<^sup>*"
    1.51 +lemma in_rtrancl_UnI: "x \<in> R^* \<or> x \<in> S^* ==> x \<in> (R \<union> S)^*"
    1.52    by (blast intro: subsetD [OF rtrancl_Un_subset])
    1.53  
    1.54 -lemma trancl_domain [simp]: "Domain (r\<^sup>+) = Domain r"
    1.55 +lemma trancl_domain [simp]: "Domain (r^+) = Domain r"
    1.56    by (unfold Domain_def) (blast dest: tranclD)
    1.57  
    1.58 -lemma trancl_range [simp]: "Range (r\<^sup>+) = Range r"
    1.59 +lemma trancl_range [simp]: "Range (r^+) = Range r"
    1.60    by (simp add: Range_def trancl_converse [symmetric])
    1.61  
    1.62  end