header {* \isaheader{Combining Stages 1 and 2} *}
theory Compiler
imports Correctness1 Correctness2
begin
constdefs
J2JVM :: "J_prog => jvm_prog"
"J2JVM ≡ compP2 o compP1"
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 ?P1 = "compP1 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 "?P1 \<turnstile> C sees M: Ts->T = (compE1 (this#pns) body) in C"
using sees_method_compP[OF method, of "λ(pns,e). compE1 (this#pns) e"]
by(simp)
moreover obtain ls' where
"?P1 \<turnstile>1 ⟨compE1 (this#pns) body, (h, vs@rest)⟩ => ⟨fin1 e', (h',ls')⟩"
using eval1_eval[OF wwf eval fv init] sizes by auto
ultimately show ?thesis using comp2_correct eval_final[OF eval]
by(fastsimp simp add:J2JVM_def final_def)
qed
end