# 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 \ (0,s1,stk) \* (isize ?cb + isize ?cc,s2,stk)" - using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce + have "?cw \ (0,s1,stk) \* (isize ?cb,s1,stk)" + using `bval b s1` by fastforce + moreover + have "?cw \ (isize ?cb,s1,stk) \* (isize ?cb + isize ?cc,s2,stk)" + using WhileTrue.IH(1) by fastforce moreover have "?cw \ (isize ?cb + isize ?cc,s2,stk) \* (0,s2,stk)" by fastforce