equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/BV/BVNoTypeErrors.thy |
1 (* Title: HOL/MicroJava/BV/BVNoTypeErrors.thy |
2 ID: $Id$ |
|
3 Author: Gerwin Klein |
2 Author: Gerwin Klein |
4 *) |
3 *) |
5 |
4 |
6 header {* \isaheader{Welltyped Programs produce no Type Errors} *} |
5 header {* \isaheader{Welltyped Programs produce no Type Errors} *} |
7 |
6 |
292 by (auto dest!: non_np_objD) |
291 by (auto dest!: non_np_objD) |
293 } |
292 } |
294 ultimately show ?thesis using Getfield field "class" stk hconf wf |
293 ultimately show ?thesis using Getfield field "class" stk hconf wf |
295 apply clarsimp |
294 apply clarsimp |
296 apply (fastsimp intro: wf_prog_ws_prog |
295 apply (fastsimp intro: wf_prog_ws_prog |
297 dest!: hconfD widen_cfs_fields oconf_objD) |
296 dest!: hconfD widen_cfs_fields oconf_objD) |
298 done |
297 done |
299 next |
298 next |
300 case (Putfield F C) |
299 case (Putfield F C) |
301 with app stk loc phi obtain v ref vT stk' where |
300 with app stk loc phi obtain v ref vT stk' where |
302 "class": "is_class G C" and |
301 "class": "is_class G C" and |