equal
deleted
inserted
replaced
48 "[| wt_jvm_prog G phi; method (G,C) sig = Some (C,rT,maxs,maxl,ins) |] ==> |
48 "[| wt_jvm_prog G phi; 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)" |
49 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, |
50 by (unfold wt_jvm_prog_def, drule method_wf_mdecl, |
51 simp, simp add: wf_mdecl_def wt_method_def) |
51 simp, simp add: wf_mdecl_def wt_method_def) |
52 |
52 |
53 text "for most instructions wt_instr collapses:" |
53 text {* for most instructions wt\_instr collapses: *} |
54 lemma |
54 lemma |
55 "succs i pc = [pc+1] ==> wt_instr i G rT phi mxs max_pc pc = |
55 "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)))" |
56 (app i G mxs rT (phi!pc) \<and> pc+1 < max_pc \<and> (G \<turnstile> step i G (phi!pc) <=' phi!(pc+1)))" |
57 by (simp add: wt_instr_def) |
57 by (simp add: wt_instr_def) |
58 |
58 |