Theory Compiler

(*  Title:      Jinja/Compiler/Compiler.thy

    Author:     Tobias Nipkow
    Copyright   TUM 2003
*)

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]
    by(fastforce simp add:J2JVM_def final_def)
qed
(*>*)


end