1.1 --- a/src/HOL/IMP/Compiler.thy	Thu Jul 09 10:34:51 2009 +0200
     1.2 +++ b/src/HOL/IMP/Compiler.thy	Thu Jul 09 17:33:22 2009 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  
     1.5  lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
     1.6  apply(rule iffI)
     1.7 - apply(erule converse_rel_powE, simp, fast)
     1.8 + apply(erule rel_pow_E2, simp, fast)
     1.9  apply simp
    1.10  done
    1.11  
    1.12 @@ -143,7 +143,7 @@
    1.13      from H C2 obtain p' q' r'
    1.14        where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
    1.15        and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
    1.16 -      by(fastsimp simp add:R_O_Rn_commute)
    1.17 +      by(fastsimp simp add:rel_pow_commute)
    1.18      from CL closed_exec1[OF _ 1] C2
    1.19      obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
    1.20        and same: "rev C1' @ C2' = rev C1 @ C2"

     2.1 --- a/src/HOL/IMP/Machines.thy	Thu Jul 09 10:34:51 2009 +0200
     2.2 +++ b/src/HOL/IMP/Machines.thy	Thu Jul 09 17:33:22 2009 +0200
     2.3 @@ -2,32 +2,16 @@
     2.4  imports Natural
     2.5  begin
     2.6  
     2.7 -lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
     2.8 -  by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
     2.9 -
    2.10 -lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
    2.11 -  by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
    2.12 -
    2.13 -lemmas converse_rel_powE = rel_pow_E2
    2.14 -
    2.15 -lemma R_O_Rn_commute: "R O R ^^ n = R ^^ n O R"
    2.16 +lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
    2.17    by (induct n) (simp, simp add: O_assoc [symmetric])
    2.18  
    2.19  lemma converse_in_rel_pow_eq:
    2.20    "((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))"
    2.21  apply(rule iffI)
    2.22 - apply(blast elim:converse_rel_powE)
    2.23 -apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
    2.24 + apply(blast elim:rel_pow_E2)
    2.25 +apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute)
    2.26  done
    2.27  
    2.28 -lemma rel_pow_plus:
    2.29 -  "R ^^ (m+n) = R ^^ n O R ^^ m"
    2.30 -  by (induct n) (simp, simp add: O_assoc)
    2.31 -
    2.32 -lemma rel_pow_plusI:
    2.33 -  "\<lbrakk> (x,y) \<in> R ^^ m; (y,z) \<in> R ^^ n \<rbrakk> \<Longrightarrow> (x,z) \<in> R ^^ (m+n)"
    2.34 -  by (simp add: rel_pow_plus rel_compI)
    2.35 -
    2.36  subsection "Instructions"
    2.37  
    2.38  text {* There are only three instructions: *}