Theory Compiler

```(*  Title:      Jinja/Compiler/Compiler.thy

Author:     Tobias Nipkow
*)

section ‹Combining Stages 1 and 2›

theory Compiler
imports Correctness1 Correctness2
begin

definition J2JVM :: "J_prog ⇒ jvm_prog"
where
"J2JVM  ≡  compP⇩2 ∘ compP⇩1"

theorem comp_correct:
assumes wwf: "wwf_J_prog P"
and "method": "P ⊢ C sees M:Ts→T = (pns,body) in C"
and eval: "P ⊢ ⟨body,(h,[this#pns [↦] vs])⟩ ⇒ ⟨e',(h',l')⟩"
and sizes: "size vs = size pns + 1"    "size rest = max_vars body"
shows "J2JVM P ⊢ (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 [↦] vs] ⊆⇩m [this#pns [↦] vs@rest]"
using sizes by simp
have "?P⇩1 ⊢ 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 ⊢⇩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]