src/HOL/IMP/Compiler.thy
changeset 50133 5b43abaf8415
parent 50061 7110422d4cb3
child 51259 1491459df114
equal deleted inserted replaced
50132:180d086c30dd 50133:5b43abaf8415
    77 
    77 
    78 declare refl[intro] step[intro]
    78 declare refl[intro] step[intro]
    79 
    79 
    80 lemmas exec_induct = exec.induct[split_format(complete)]
    80 lemmas exec_induct = exec.induct[split_format(complete)]
    81 
    81 
    82 code_pred exec by force
    82 code_pred exec by fastforce
    83 
    83 
    84 values
    84 values
    85   "{(i,map t [''x'',''y''],stk) | i t stk.
    85   "{(i,map t [''x'',''y''],stk) | i t stk.
    86     [LOAD ''y'', STORE ''x''] \<turnstile>
    86     [LOAD ''y'', STORE ''x''] \<turnstile>
    87     (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
    87     (0, <''x'' := 3, ''y'' := 4>, []) \<rightarrow>* (i,t,stk)}"
   230 next
   230 next
   231   case (WhileTrue b s1 c s2 s3)
   231   case (WhileTrue b s1 c s2 s3)
   232   let ?cc = "ccomp c"
   232   let ?cc = "ccomp c"
   233   let ?cb = "bcomp b False (isize ?cc + 1)"
   233   let ?cb = "bcomp b False (isize ?cc + 1)"
   234   let ?cw = "ccomp(WHILE b DO c)"
   234   let ?cw = "ccomp(WHILE b DO c)"
   235   have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
   235   have "?cw \<turnstile> (0,s1,stk) \<rightarrow>* (isize ?cb,s1,stk)"
   236     using WhileTrue.IH(1) WhileTrue.hyps(1) by fastforce
   236     using `bval b s1` by fastforce
       
   237   moreover
       
   238   have "?cw \<turnstile> (isize ?cb,s1,stk) \<rightarrow>* (isize ?cb + isize ?cc,s2,stk)"
       
   239     using WhileTrue.IH(1) by fastforce
   237   moreover
   240   moreover
   238   have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
   241   have "?cw \<turnstile> (isize ?cb + isize ?cc,s2,stk) \<rightarrow>* (0,s2,stk)"
   239     by fastforce
   242     by fastforce
   240   moreover
   243   moreover
   241   have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))
   244   have "?cw \<turnstile> (0,s2,stk) \<rightarrow>* (isize ?cw,s3,stk)" by(rule WhileTrue.IH(2))