# HG changeset patch
# User nipkow
# Date 1353430166 -3600
# Node ID 5b43abaf84157a9de678444804a01cc6b551dd7c
# Parent  180d086c30ddbd736048c8ca68912d431cbaac7f
tuned proof

diff -r 180d086c30dd -r 5b43abaf8415 src/HOL/IMP/Compiler.thy
--- a/src/HOL/IMP/Compiler.thy	Tue Nov 20 15:18:11 2012 +0100
+++ b/src/HOL/IMP/Compiler.thy	Tue Nov 20 17:49:26 2012 +0100
@@ -79,7 +79,7 @@
 
 lemmas exec_induct = exec.induct[split_format(complete)]
 
-code_pred exec by force
+code_pred exec by fastforce
 
 values
   "{(i,map t [''x'',''y''],stk) | i t stk.
@@ -232,8 +232,11 @@
   let ?cc = "ccomp c"
   let ?cb = "bcomp b False (isize ?cc + 1)"
   let ?cw = "ccomp(WHILE b DO c)"
-  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
-    using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
+  have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb,s1,stk)"
+    using `bval b s1` by fastforce
+  moreover
+  have "?cw \<turnstile> (isize ?cb,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
+    using WhileTrue.IH(1) by fastforce
   moreover
   have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
     by fastforce