Theory Compiler

(*  Title:      Jinja/Compiler/Compiler.thy

    Author:     Tobias Nipkow
    Copyright   TUM 2003

section ‹Combining Stages 1 and 2›

theory Compiler
imports Correctness1 Correctness2

definition J2JVM :: "J_prog  jvm_prog"
  "J2JVM    compP2  compP1"

theorem comp_correct:
assumes wwf: "wwf_J_prog P"
and "method": "P  C sees M:TsT = (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 ?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 [↦] vs] m [this#pns [↦] vs@rest]"
    using sizes by simp
  have "?P1  C sees M: TsT = (compE1 (this#pns) body) in C"
    using sees_method_compP[OF "method", of "λ(pns,e). compE1 (this#pns) e"]
  moreover obtain ls' where
    "?P1 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(fastforce simp add:J2JVM_def final_def)