src/HOL/Transitive_Closure.thy
changeset 32235 8f9b8d14fc9f
parent 32215 87806301a813
child 32601 47d0c967c64e
     1.1 --- a/src/HOL/Transitive_Closure.thy	Mon Jul 27 17:36:30 2009 +0200
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jul 27 21:47:41 2009 +0200
     1.3 @@ -159,7 +159,7 @@
     1.4    apply (erule asm_rl exE disjE conjE base step)+
     1.5    done
     1.6  
     1.7 -lemma rtrancl_Int_subset: "[| Id \<subseteq> s; r O (r^* \<inter> s) \<subseteq> s|] ==> r^* \<subseteq> s"
     1.8 +lemma rtrancl_Int_subset: "[| Id \<subseteq> s; (r^* \<inter> s) O r \<subseteq> s|] ==> r^* \<subseteq> s"
     1.9    apply (rule subsetI)
    1.10    apply (rule_tac p="x" in PairE, clarify)
    1.11    apply (erule rtrancl_induct, auto) 
    1.12 @@ -291,7 +291,7 @@
    1.13    by (blast elim: rtranclE converse_rtranclE
    1.14      intro: rtrancl_into_rtrancl converse_rtrancl_into_rtrancl)
    1.15  
    1.16 -lemma rtrancl_unfold: "r^* = Id Un r O r^*"
    1.17 +lemma rtrancl_unfold: "r^* = Id Un r^* O r"
    1.18    by (auto intro: rtrancl_into_rtrancl elim: rtranclE)
    1.19  
    1.20  lemma rtrancl_Un_separatorE:
    1.21 @@ -384,7 +384,7 @@
    1.22    | (step) c where "(a, c) : r^+" and "(c, b) : r"
    1.23    using assms by cases simp_all
    1.24  
    1.25 -lemma trancl_Int_subset: "[| r \<subseteq> s; r O (r^+ \<inter> s) \<subseteq> s|] ==> r^+ \<subseteq> s"
    1.26 +lemma trancl_Int_subset: "[| r \<subseteq> s; (r^+ \<inter> s) O r \<subseteq> s|] ==> r^+ \<subseteq> s"
    1.27    apply (rule subsetI)
    1.28    apply (rule_tac p = x in PairE)
    1.29    apply clarify
    1.30 @@ -392,7 +392,7 @@
    1.31     apply auto
    1.32    done
    1.33  
    1.34 -lemma trancl_unfold: "r^+ = r Un r O r^+"
    1.35 +lemma trancl_unfold: "r^+ = r Un r^+ O r"
    1.36    by (auto intro: trancl_into_trancl elim: tranclE)
    1.37  
    1.38  text {* Transitivity of @{term "r^+"} *}
    1.39 @@ -676,7 +676,7 @@
    1.40  
    1.41  primrec relpow :: "nat \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" where
    1.42      "relpow 0 R = Id"
    1.43 -  | "relpow (Suc n) R = R O (R ^^ n)"
    1.44 +  | "relpow (Suc n) R = (R ^^ n) O R"
    1.45  
    1.46  end
    1.47  
    1.48 @@ -734,11 +734,11 @@
    1.49    apply (cut_tac n=nat and R=R in rel_pow_Suc_D2', simp, blast)
    1.50    done
    1.51  
    1.52 -lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
    1.53 +lemma rel_pow_add: "R ^^ (m+n) = R^^m O R^^n"
    1.54  by(induct n) auto
    1.55  
    1.56  lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
    1.57 -  by (induct n) (simp, simp add: O_assoc [symmetric])
    1.58 +by (induct n) (simp, simp add: O_assoc [symmetric])
    1.59  
    1.60  lemma rtrancl_imp_UN_rel_pow:
    1.61    assumes "p \<in> R^*"