src/HOL/IMP/Compiler.thy
changeset 50133 5b43abaf8415
parent 50061 7110422d4cb3
child 51259 1491459df114
--- 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