197 qed_spec_mp "FB_lemma2"; |
198 qed_spec_mp "FB_lemma2"; |
198 |
199 |
199 Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
200 Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t"; |
200 by (fast_tac (claset() addEs [FB_lemma2]) 1); |
201 by (fast_tac (claset() addEs [FB_lemma2]) 1); |
201 qed "evalc1_impl_evalc"; |
202 qed "evalc1_impl_evalc"; |
|
203 |
|
204 |
|
205 section "The proof in Nielson and Nielson"; |
|
206 |
|
207 (* The more precise n=i1+i2+1 is proved by the same script but complicates |
|
208 life further down, where i1,i2 < n is needed. |
|
209 *) |
|
210 Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \ |
|
211 \ (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)"; |
|
212 by(induct_tac "n" 1); |
|
213 by (fast_tac (claset() addSDs [hlemma]) 1); |
|
214 by(fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2] |
|
215 addSDs [rel_pow_Suc_D2] addss simpset()) 1); |
|
216 qed_spec_mp "comp_decomp_lemma"; |
|
217 |
|
218 Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t"; |
|
219 by(res_inst_tac [("n","n")] less_induct 1); |
|
220 by(Clarify_tac 1); |
|
221 be rel_pow_E2 1; |
|
222 by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1); |
|
223 by(exhaust_tac "c" 1); |
|
224 by (fast_tac (claset() addSDs [hlemma]) 1); |
|
225 by(Blast_tac 1); |
|
226 by(blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1); |
|
227 by(Blast_tac 1); |
|
228 by(Blast_tac 1); |
|
229 qed_spec_mp "evalc1_impl_evalc"; |