# HG changeset patch
# User nipkow
# Date 1384423162 -3600
# Node ID 6ccc6130140ccbb8bd71b5e77c5db17d785ff606
# Parent  783861a66a60194aca6d2c1c888dd8745f47aeba
tuned to improve automation (for REPEAT)

diff -r 783861a66a60 -r 6ccc6130140c src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Wed Nov 13 19:12:15 2013 +0100
+++ b/src/HOL/IMP/Compiler.thy	Thu Nov 14 10:59:22 2013 +0100
@@ -138,11 +138,12 @@
 by (drule exec_appendL[where P'="[instr]"]) simp
 
 lemma exec_appendL_if[intro]:
-  fixes i i' :: int
+  fixes i i' j :: int
   shows
   "size P' <= i
-   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (i',s',stk')
-   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (size P' + i',s',stk')"
+   \<Longrightarrow> P \<turnstile> (i - size P',s,stk) \<rightarrow>* (j,s',stk')
+   \<Longrightarrow> i' = size P' + j
+   \<Longrightarrow> P' @ P \<turnstile> (i,s,stk) \<rightarrow>* (i',s',stk')"
 by (drule exec_appendL[where P'=P']) simp
 
 text{* Split the execution of a compound program up into the excution of its