250 ( [], [Class list_name, Class list_name]), |
250 ( [], [Class list_name, Class list_name]), |
251 ( [Class list_name], [Class list_name, Class list_name]), |
251 ( [Class list_name], [Class list_name, Class list_name]), |
252 ( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
252 ( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
253 ( [], [Class list_name, Class list_name]), |
253 ( [], [Class list_name, Class list_name]), |
254 ( [PrimT Void], [Class list_name, Class list_name])]" |
254 ( [PrimT Void], [Class list_name, Class list_name])]" |
|
255 |
|
256 declare nat_number [simp] |
255 |
257 |
256 lemma wt_append [simp]: |
258 lemma wt_append [simp]: |
257 "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins |
259 "wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins |
258 [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a" |
260 [(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a" |
259 apply (simp add: wt_method_def append_ins_def phi_append_def |
261 apply (simp add: wt_method_def append_ins_def phi_append_def |
346 text {* The whole program is welltyped: *} |
348 text {* The whole program is welltyped: *} |
347 constdefs |
349 constdefs |
348 Phi :: prog_type ("\<Phi>") |
350 Phi :: prog_type ("\<Phi>") |
349 "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else |
351 "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else |
350 if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []" |
352 if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []" |
351 |
353 |
|
354 declare nat_number [simp del] |
|
355 |
352 lemma wf_prog: |
356 lemma wf_prog: |
353 "wt_jvm_prog E \<Phi>" |
357 "wt_jvm_prog E \<Phi>" |
354 apply (unfold wt_jvm_prog_def) |
358 apply (unfold wt_jvm_prog_def) |
355 apply (rule wf_mb'E [OF wf_struct]) |
359 apply (rule wf_mb'E [OF wf_struct]) |
356 apply (simp add: E_def) |
360 apply (simp add: E_def) |