Isabelle_little_compiler.md

V2:

theory Isabelle_little_compiler
  imports Main
begin

datatype lang = 
  Lit nat
  | Plus lang lang

datatype op =
  Push nat
  | Add

fun compile :: "lang ⇒ op list" where
"compile (Lit n) = [Push n]" |
"compile (Plus a b) = compile a @ compile b @ [Add]"

fun decompile :: "op list ⇒ lang list ⇒ lang list" where
"decompile [] stack = stack" |
"decompile (Push n # xs) stack = decompile xs (Lit n # stack)" |
"decompile (Add # xs) stack = decompile xs (case stack of
b # a # rest ⇒ Plus a b # rest |
_ ⇒ stack)"

lemma decompile_right_gen: "decompile (compile e @ k) stack = decompile k (e # stack)"
  by (induct e arbitrary: k stack; simp)  

lemma decompile_right: "decompile (compile a) [] = [a]"
  using decompile_right_gen[where k="[]"] by auto

lemma equiv: "compile a = compile b ⟹ a = b"
  using decompile_right
  by (metis list.inject)

end

V1 (horrible termination proof):

(* Should really be in a .thy file, but syntax highlighting ;) *)
theory Isabelle_little_compiler
  imports Main
begin

datatype lang = 
  Lit nat
  | Plus lang lang

datatype op =
  Push nat
  | Add

fun compile :: "lang ⇒ op list" where
"compile (Lit n) = [Push n]" |
"compile (Plus a b) = Add # compile a @ compile b"

(* 
   Writing the function mbones's way would fix the "Isabelle is being a pain around termination" problem,
   but this is how I originally pictured it, so this way it'll stay.
*)

function decompile :: "op list ⇒ lang option × op list" where
"decompile [] = (None, [])" |
"decompile (Push n # xs) = (Some (Lit n), xs)" |
"decompile (Add # a) = (case decompile a of
                          (Some a', xs) ⇒ (case decompile xs of
                              (Some b', ys) ⇒ (Some (Plus a' b'), ys) |
                              _ ⇒ (None, [])) |
                          _ ⇒ (None, []))"
  by pat_completeness auto
termination sorry
 

lemma decompile_right_gen: "decompile ((compile a) @ k) = (Some a, k)"
  by (induct a arbitrary: k; clarsimp)

lemma decompile_right: "decompile (compile a) = (Some a, [])"
  using decompile_right_gen[where k="[]"] by auto

lemma equiv: "compile a = compile b ⟹ a = b"
  using decompile_right
  by (metis option.inject prod.inject)
  
end