diff -r 0314441a53a6 -r 09524788a6b9 src/HOL/IMP/Machines.thy
--- a/src/HOL/IMP/Machines.thy	Thu Jul 09 10:34:51 2009 +0200
+++ b/src/HOL/IMP/Machines.thy	Thu Jul 09 17:33:22 2009 +0200
@@ -2,32 +2,16 @@
 imports Natural
 begin
 
-lemma rtrancl_eq: "R^* = Id \<union> (R O R^*)"
-  by (fast intro: rtrancl_into_rtrancl elim: rtranclE)
-
-lemma converse_rtrancl_eq: "R^* = Id \<union> (R^* O R)"
-  by (subst r_comp_rtrancl_eq[symmetric], rule rtrancl_eq)
-
-lemmas converse_rel_powE = rel_pow_E2
-
-lemma R_O_Rn_commute: "R O R ^^ n = R ^^ n O R"
+lemma rel_pow_commute: "R O R ^^ n = R ^^ n O R"
   by (induct n) (simp, simp add: O_assoc [symmetric])
 
 lemma converse_in_rel_pow_eq:
   "((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))"
 apply(rule iffI)
- apply(blast elim:converse_rel_powE)
-apply (fastsimp simp add:gr0_conv_Suc R_O_Rn_commute)
+ apply(blast elim:rel_pow_E2)
+apply (fastsimp simp add:gr0_conv_Suc rel_pow_commute)
 done
 
-lemma rel_pow_plus:
-  "R ^^ (m+n) = R ^^ n O R ^^ m"
-  by (induct n) (simp, simp add: O_assoc)
-
-lemma rel_pow_plusI:
-  "\<lbrakk> (x,y) \<in> R ^^ m; (y,z) \<in> R ^^ n \<rbrakk> \<Longrightarrow> (x,z) \<in> R ^^ (m+n)"
-  by (simp add: rel_pow_plus rel_compI)
-
 subsection "Instructions"
 
 text {* There are only three instructions: *}