summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 10 May 2002 11:56:26 +0200 | |

changeset 13130 | 423ce375bf65 |

parent 13129 | bb448fb75191 |

child 13131 | 2d284f0dfd56 |

commented out half converted proof

--- a/src/HOL/IMP/Compiler0.thy Fri May 10 11:55:45 2002 +0200 +++ b/src/HOL/IMP/Compiler0.thy Fri May 10 11:56:26 2002 +0200 @@ -215,7 +215,7 @@ Second proof; statement is generalized to cater for prefixes and suffixes; needs none of the lifting lemmas, but instantiations of pre/suffix. *} - +(* theorem assumes A: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t" shows "\<And>a z. a@compile c@z \<turnstile> \<langle>s,size a\<rangle> -*\<rightarrow> \<langle>t,size a + size(compile c)\<rangle>" (is "\<And>a z. ?P c s t a z") @@ -269,7 +269,7 @@ apply(force intro!: JMPB) apply(simp) done - +*) text {* Missing: the other direction! I did much of it, and although the main lemma is very similar to the one in the new development, the lemmas surrounding it seemed much more complicated. In the end I gave