# HG changeset patch
# User krauss
# Date 1247153602 -7200
# Node ID 09524788a6b994f27cef0da22e5a2c7e2cb30562
# Parent  0314441a53a6eff9ef4ece0d6ebcbe19301fdd07
drop unused lemmas

diff -r 0314441a53a6 -r 09524788a6b9 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Thu Jul 09 10:34:51 2009 +0200
+++ b/src/HOL/IMP/Compiler.thy	Thu Jul 09 17:33:22 2009 +0200
@@ -58,7 +58,7 @@
 
 lemma [simp]: "(\<langle>[],q,s\<rangle> -n\<rightarrow> \<langle>p',q',t\<rangle>) = (n=0 \<and> p' = [] \<and> q' = q \<and> t = s)"
 apply(rule iffI)
- apply(erule converse_rel_powE, simp, fast)
+ apply(erule rel_pow_E2, simp, fast)
 apply simp
 done
 
@@ -143,7 +143,7 @@
     from H C2 obtain p' q' r'
       where 1: "\<langle>instr # tlC2 @ p1 @ p2, C1 @ q,r\<rangle> -1\<rightarrow> \<langle>p',q',r'\<rangle>"
       and n: "\<langle>p',q',r'\<rangle> -n\<rightarrow> \<langle>p2,rev p1 @ rev C2 @ C1 @ q,t\<rangle>"
-      by(fastsimp simp add:R_O_Rn_commute)
+      by(fastsimp simp add:rel_pow_commute)
     from CL closed_exec1[OF _ 1] C2
     obtain C2' C1' where pq': "p' = C2' @ p1 @ p2 \<and> q' = C1' @ q"
       and same: "rev C1' @ C2' = rev C1 @ C2"
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: *}