291 apply (unfold field_def) |
291 apply (unfold field_def) |
292 apply auto |
292 apply auto |
293 done |
293 done |
294 |
294 |
295 lemma wf_ObjectC: |
295 lemma wf_ObjectC: |
296 "wf_cdecl wf_java_mdecl tprg ObjectC" |
296 "ws_cdecl tprg ObjectC \<and> |
297 apply (unfold wf_cdecl_def wf_fdecl_def ObjectC_def) |
297 wf_cdecl_mdecl wf_java_mdecl tprg ObjectC \<and> wf_mrT tprg ObjectC" |
|
298 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
299 wf_mrT_def wf_fdecl_def ObjectC_def) |
298 apply (simp (no_asm)) |
300 apply (simp (no_asm)) |
299 done |
301 done |
300 |
302 |
301 lemma wf_NP: |
303 lemma wf_NP: |
302 "wf_cdecl wf_java_mdecl tprg NullPointerC" |
304 "ws_cdecl tprg NullPointerC \<and> |
303 apply (unfold wf_cdecl_def wf_fdecl_def NullPointerC_def) |
305 wf_cdecl_mdecl wf_java_mdecl tprg NullPointerC \<and> wf_mrT tprg NullPointerC" |
|
306 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
307 wf_mrT_def wf_fdecl_def NullPointerC_def) |
304 apply (simp add: class_def) |
308 apply (simp add: class_def) |
305 apply (fold NullPointerC_def class_def) |
309 apply (fold NullPointerC_def class_def) |
306 apply auto |
310 apply auto |
307 done |
311 done |
308 |
312 |
309 lemma wf_OM: |
313 lemma wf_OM: |
310 "wf_cdecl wf_java_mdecl tprg OutOfMemoryC" |
314 "ws_cdecl tprg OutOfMemoryC \<and> |
311 apply (unfold wf_cdecl_def wf_fdecl_def OutOfMemoryC_def) |
315 wf_cdecl_mdecl wf_java_mdecl tprg OutOfMemoryC \<and> wf_mrT tprg OutOfMemoryC" |
|
316 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
317 wf_mrT_def wf_fdecl_def OutOfMemoryC_def) |
312 apply (simp add: class_def) |
318 apply (simp add: class_def) |
313 apply (fold OutOfMemoryC_def class_def) |
319 apply (fold OutOfMemoryC_def class_def) |
314 apply auto |
320 apply auto |
315 done |
321 done |
316 |
322 |
317 lemma wf_CC: |
323 lemma wf_CC: |
318 "wf_cdecl wf_java_mdecl tprg ClassCastC" |
324 "ws_cdecl tprg ClassCastC \<and> |
319 apply (unfold wf_cdecl_def wf_fdecl_def ClassCastC_def) |
325 wf_cdecl_mdecl wf_java_mdecl tprg ClassCastC \<and> wf_mrT tprg ClassCastC" |
|
326 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
327 wf_mrT_def wf_fdecl_def ClassCastC_def) |
320 apply (simp add: class_def) |
328 apply (simp add: class_def) |
321 apply (fold ClassCastC_def class_def) |
329 apply (fold ClassCastC_def class_def) |
322 apply auto |
330 apply auto |
323 done |
331 done |
324 |
332 |
325 lemma wf_BaseC: |
333 lemma wf_BaseC: |
326 "wf_cdecl wf_java_mdecl tprg BaseC" |
334 "ws_cdecl tprg BaseC \<and> |
327 apply (unfold wf_cdecl_def wf_fdecl_def BaseC_def) |
335 wf_cdecl_mdecl wf_java_mdecl tprg BaseC \<and> wf_mrT tprg BaseC" |
|
336 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
337 wf_mrT_def wf_fdecl_def BaseC_def) |
328 apply (simp (no_asm)) |
338 apply (simp (no_asm)) |
329 apply (fold BaseC_def) |
339 apply (fold BaseC_def) |
330 apply (rule wf_foo_Base [THEN conjI]) |
340 apply (rule mp) defer apply (rule wf_foo_Base) |
331 apply auto |
341 apply (auto simp add: wf_mdecl_def) |
332 done |
342 done |
|
343 |
333 |
344 |
334 lemma wf_ExtC: |
345 lemma wf_ExtC: |
335 "wf_cdecl wf_java_mdecl tprg ExtC" |
346 "ws_cdecl tprg ExtC \<and> |
336 apply (unfold wf_cdecl_def wf_fdecl_def ExtC_def) |
347 wf_cdecl_mdecl wf_java_mdecl tprg ExtC \<and> wf_mrT tprg ExtC" |
|
348 apply (unfold ws_cdecl_def wf_cdecl_mdecl_def |
|
349 wf_mrT_def wf_fdecl_def ExtC_def) |
337 apply (simp (no_asm)) |
350 apply (simp (no_asm)) |
338 apply (fold ExtC_def) |
351 apply (fold ExtC_def) |
339 apply (rule wf_foo_Ext [THEN conjI]) |
352 apply (rule mp) defer apply (rule wf_foo_Ext) |
340 apply auto |
353 apply (auto simp add: wf_mdecl_def) |
341 apply (drule rtranclD) |
354 apply (drule rtranclD) |
342 apply auto |
355 apply auto |
343 done |
356 done |
|
357 |
344 |
358 |
345 lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) |
359 lemma [simp]: "fst ObjectC = Object" by (simp add: ObjectC_def) |
346 |
360 |
347 lemma wf_tprg: |
361 lemma wf_tprg: |
348 "wf_prog wf_java_mdecl tprg" |
362 "wf_prog wf_java_mdecl tprg" |
349 apply (unfold wf_prog_def Let_def) |
363 apply (unfold wf_prog_def ws_prog_def Let_def) |
350 apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes) |
364 apply (simp add: wf_ObjectC wf_BaseC wf_ExtC wf_NP wf_OM wf_CC unique_classes) |
351 apply (rule wf_syscls) |
365 apply (rule wf_syscls) |
352 apply (simp add: SystemClasses_def) |
366 apply (simp add: SystemClasses_def) |
353 done |
367 done |
354 |
368 |