Isabelle compiler correctness demo.

Compiler_Demo.thy

theory Compiler_Demo
  imports Main
begin

type_synonym 'a binop = "'a ⇒ 'a ⇒ 'a"

datatype ('a, 'v) expr
  = Const 'v
  | Var 'a
  | BinOp "'v binop" "('a, 'v) expr" "('a, 'v) expr"

primrec "value" :: "('a, 'v) expr ⇒ ('a ⇒ 'v) ⇒ 'v" where
  "value (Const v) _ = v"
| "value (Var r) env = env r"
| "value (BinOp f e1 e2) env = f (value e1 env) (value e2 env)"

datatype ('a, 'v) inst
  = Push 'v
  | Load 'a
  | Call "'v binop"

primrec exec :: "('a, 'v) inst list ⇒ ('a ⇒ 'v) ⇒ 'v list ⇒ 'v list" where
  "exec [] _ stack = stack"
| "exec (i#is) env stack = (case i of
    Push v ⇒ exec is env (v # stack)
  | Load r ⇒ exec is env ((env r) # stack)
  | Call f ⇒ exec is env ( (f (hd stack) (hd (tl stack))) # (tl (tl stack)) ))"

primrec compile :: "('a, 'v) expr ⇒ ('a, 'v) inst list" where
  "compile (Const v) = [Push v]"
| "compile (Var r)   = [Load r]"
| "compile (BinOp f e1 e2) = (compile e2) @ (compile e1) @ [Call f]"

lemma exec_app[simp]: "∀st. exec (xs@ys) env st = exec ys env (exec xs env st)"
  apply (induction xs)
   apply (simp_all)
    by (simp split: inst.split)

theorem gen_corr: "∀stack. exec (compile ex) env stack = (value ex env) # stack"
  apply (induction ex)
    apply (simp_all)
    done

corollary "exec (compile ex) env [] = [value ex env]"
  by (simp add: gen_corr)

lemma "hd [] = hd []"
  by (simp)

end