move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
authorkrauss
Thu Jul 09 17:34:59 2009 +0200 (2009-07-09)
changeset 31970ccaadfcf6941
parent 31969 09524788a6b9
child 31971 8c1b845ed105
child 31972 02f02097e1e4
child 32036 8a9228872fbd
move rel_pow_commute: "R O R ^^ n = R ^^ n O R" to Transitive_Closure
src/HOL/IMP/Machines.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/src/HOL/IMP/Machines.thy	Thu Jul 09 17:33:22 2009 +0200
     1.2 +++ b/src/HOL/IMP/Machines.thy	Thu Jul 09 17:34:59 2009 +0200
     1.3 @@ -2,9 +2,6 @@
     1.4  imports Natural
     1.5  begin
     1.6  
     1.7 -lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
     1.8 -  by (induct n) (simp, simp add: O_assoc [symmetric])
     1.9 -
    1.10  lemma converse_in_rel_pow_eq:
    1.11    "((x,z) \<in> R ^^ n) = (n=0 \<and> z=x \<or> (\<exists>m y. n = Suc m \<and> (x,y) \<in> R \<and> (y,z) \<in> R ^^ m))"
    1.12  apply(rule iffI)
     2.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jul 09 17:33:22 2009 +0200
     2.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jul 09 17:34:59 2009 +0200
     2.3 @@ -737,6 +737,9 @@
     2.4  lemma rel_pow_add: "R ^^ (m+n) = R^^n O R^^m"
     2.5  by(induct n) auto
     2.6  
     2.7 +lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
     2.8 +  by (induct n) (simp, simp add: O_assoc [symmetric])
     2.9 +
    2.10  lemma rtrancl_imp_UN_rel_pow:
    2.11    assumes "p \<in> R^*"
    2.12    shows "p \<in> (\<Union>n. R ^^ n)"