author | nipkow |

Fri May 10 11:56:26 2002 +0200 (2002-05-10) | |

changeset 13130 | 423ce375bf65 |

parent 13129 | bb448fb75191 |

child 13131 | 2d284f0dfd56 |

commented out half converted proof

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