(* Title: Jinja/Compiler/Compiler.thy
ID: $Id: Compiler.html 1910 2004-05-19 04:46:04Z kleing $
Author: Tobias Nipkow
Copyright TUM 2003
*)
header {* \isaheader{Combining Stages 1 and 2} *}
theory Compiler = Correctness1 + Correctness2:
constdefs
J2JVM :: "J_prog => jvm_prog"
"J2JVM ≡ compP2 ˆ 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
theorem
[| wwf_J_prog P; P \<turnstile> C sees M: Ts->T = (pns, body) in C; eval P body (h, [this # pns [|->] vs]) e' (h', l'); length vs = length pns + 1; length rest = max_vars body |] ==> J2JVM P |- (None, h, [([], vs @ rest, C, M, 0)]) -jvm-> (exception e', h', [])