36 |
36 |
37 lemma wt_jvm_progD: |
37 lemma wt_jvm_progD: |
38 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)" |
38 "wt_jvm_prog G phi ==> (\<exists>wt. wf_prog wt G)" |
39 by (unfold wt_jvm_prog_def, blast) |
39 by (unfold wt_jvm_prog_def, blast) |
40 |
40 |
41 lemma wt_jvm_prog_impl_wt_instr: |
41 lemma wt_jvm_prog_impl_wt_instr: (* DvO: is_class G C eingefügt *) |
42 "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] |
42 "[| wt_jvm_prog G phi; is_class G C; |
|
43 method (G,C) sig = Some (C,rT,maxs,maxl,ins); pc < length ins |] |
43 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"; |
44 ==> wt_instr (ins!pc) G rT (phi C sig) maxs (length ins) pc"; |
44 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
45 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
45 simp, simp add: wf_mdecl_def wt_method_def) |
46 simp, simp, simp add: wf_mdecl_def wt_method_def) |
46 |
47 |
47 lemma wt_jvm_prog_impl_wt_start: |
48 lemma wt_jvm_prog_impl_wt_start: (* DvO: is_class G C eingefügt *) |
48 "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> |
49 "[| wt_jvm_prog G phi; is_class G C; |
|
50 method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> |
49 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)" |
51 0 < (length ins) \<and> wt_start G C (snd sig) maxl (phi C sig)" |
50 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
52 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
51 simp, simp add: wf_mdecl_def wt_method_def) |
53 simp, simp, simp add: wf_mdecl_def wt_method_def) |
52 |
54 |
53 text {* for most instructions wt\_instr collapses: *} |
55 text {* for most instructions wt\_instr collapses: *} |
54 lemma |
56 lemma |
55 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = |
57 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = |
56 (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))" |
58 (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))" |