header {* \isaheader{Combining Stages 1 and 2} *}
theory Compiler
imports Correctness1 Correctness2
begin
definition J2JVM :: "J_prog => jvm_prog"
where
"J2JVM ≡ compP⇣2 o compP⇣1"
theorem comp_correct:
assumes wwf: "wwf_J_prog P"
and method: "P \<turnstile> C sees M:Ts->T = (pns,body) in C"
and eval: "P \<turnstile> ⟨body,(h,[this#pns [\<mapsto>] vs])⟩ => ⟨e',(h',l')⟩"
and sizes: "size vs = size pns + 1" "size rest = max_vars body"
shows "J2JVM P \<turnstile> (None,h,[([],vs@rest,C,M,0)]) -jvm-> (exception e',h',[])"
proof -
let ?P⇣1 = "compP⇣1 P"
have fv: "fv body ⊆ set (this#pns)"
using wwf method by(auto dest!:sees_wf_mdecl simp:wf_mdecl_def)
have init: "[this#pns [\<mapsto>] vs] ⊆⇩m [this#pns [\<mapsto>] vs@rest]"
using sizes by simp
have "?P⇣1 \<turnstile> C sees M: Ts->T = (compE⇣1 (this#pns) body) in C"
using sees_method_compP[OF method, of "λ(pns,e). compE⇣1 (this#pns) e"]
by(simp)
moreover obtain ls' where
"?P⇣1 \<turnstile>⇩1 ⟨compE⇣1 (this#pns) body, (h, vs@rest)⟩ => ⟨fin⇣1 e', (h',ls')⟩"
using eval⇣1_eval[OF wwf eval fv init] sizes by auto
ultimately show ?thesis using comp⇣2_correct eval_final[OF eval]
by(fastforce simp add:J2JVM_def final_def)
qed
end