(* 
ソース言語：算術式
マシン命令セット：Lit, Add
 *)


(*************************)
(* stack machine         *)
(*************************)

val _ = Hol_datatype
    `machine =
    machine_init |
    push of num => machine`;;
val top = Define
    `top (push x m) = x`;;
val pop = Define
    `pop (push x m) = m`;;


val exec_lit = Define
    `exec_lit x s = push x s`;;
val exec_add = Define
    `exec_add s =
    let x1 = top s in
    let s1 = pop s in
    let x2 = top s1 in
    let s2 = pop s1 in 
	push (x1+x2) s2`;;
val _ = Hol_datatype 
    `instr = 
    Lit of num
  | Add`;;
val exec_instr = Define    
    `(exec_instr (Lit x) s = exec_lit x s) /\
      (exec_instr Add s = exec_add s)`;;
val exec = Define 
    `(exec [] s = s) /\
    (exec (x::l) s = exec l (exec_instr x s))`;;



(*************************)
(* source language       *)
(*************************)

val _ = Hol_datatype 
    `exp = 
    Const of num | Sum of exp => exp`;;
val eval = Define
    `(eval (Const x) = x) /\ 
    (eval (Sum y z) = eval(y) + eval(z))`;;


(*************************)
(* compiler              *)
(*************************)

val compile = Define
    `(compile (Const x) = [Lit(x)]) /\
    (compile (Sum y z) =
     APPEND (compile y) (APPEND (compile z) [Add]))`;;



(*************************)
(* proof                 *)
(*************************)

val exec_APPEND = prove
    (``!l1 l2 s. exec (APPEND l1 l2) s = exec l2 (exec l1 s)``,
     Induct_on `l1` THEN
     RW_TAC list_ss [exec]);;
val pop_exec_compile = prove
    (``!e s. pop (exec (compile e) s) = s``,
     Induct_on `e` THENL
     [R_TAC [compile] THEN
      R_TAC [exec,exec_instr,exec_lit] THEN
      R_TAC [pop],
      R_TAC [compile] THEN
      R_TAC [exec_APPEND] THEN
      R_TAC [exec,exec_instr,exec_add] THEN
      LETR_TAC THEN
      R_TAC [pop] THEN
      RW_TAC list_ss []]);;
val compiler_correctness = prove
    (``!e s. top (exec (compile e) s) = eval e``,
     Induct_on `e` THENL
     [R_TAC [compile,eval] THEN
      R_TAC [exec,exec_instr,exec_lit] THEN
      R_TAC [top],
      R_TAC [compile,eval] THEN
      R_TAC [exec_APPEND] THEN
      R_TAC [exec,exec_instr,exec_add] THEN
      LETR_TAC THEN
      R_TAC [top] THEN
      RW_TAC arith_ss [pop_exec_compile]]);;