(* 
ソース言語：代入文, If文, 複文
マシン命令セット：Load, Store, Lit, Add, Ifcmpeq, Goto
 *)


val DROP1 = Define 
      `(DROP1 0 l = l) /\
      (DROP1 (SUC n) l = DROP1 n (TL l))`;;
val DROP = Define 
    `DROP n l = if n <= LENGTH l then DROP1 n l else l`;;
val LENGTH_DROP1 = prove
     (``!n (l:'a list). n <= LENGTH l ==>
	  (LENGTH (DROP1 n l) < SUC (LENGTH l))``,
      Induct_on `n` THENL
      [RW_TAC list_ss [DROP1],
       RW_TAC list_ss [DROP1] THEN
       Induct_on `l` THENL
       [RW_TAC list_ss [DROP1],
	RW_TAC list_ss [] THEN RES_TAC THEN
	RW_TAC list_ss []]]);;
val LENGTH_DROP = prove
    (``!n (l:'a list). LENGTH (DROP n l) < SUC (LENGTH l)``,
     R_TAC [DROP] THEN
     RW_TAC list_ss [LENGTH_DROP1]);;
val DROP_LENGTH = prove
    (``!l. DROP (LENGTH l) l = []``,
     RW_TAC list_ss [DROP] THEN
     Induct_on `l` THEN
     RW_TAC list_ss [DROP1]);;
val LENGTH_APPEND = prove
    (``!l1 l2. LENGTH l1 <= LENGTH (APPEND l1 l2)``,
     Induct_on `l1` THEN
     RW_TAC list_ss []);;
val DROP_LENGTH_APPEND = prove
    (``!l1 l2. DROP (LENGTH l1) (APPEND l1 l2) = l2``,
     R_TAC [DROP] THEN
     Induct_on `l1` THENL
     [RW_TAC list_ss [DROP,DROP1],
      RW_TAC list_ss [DROP,DROP1] THEN
      UNDISCH_ALL_TAC THEN
      RW_TAC list_ss [LENGTH_APPEND]]);;
val APPEND_APPEND = prove
      (``!l1 l2 l3. APPEND (APPEND l1 l2) l3 = APPEND l1 (APPEND l2 l3)``,
       RW_TAC list_ss []);;
val DROP_lemma = prove 
	(``!l1 l2. DROP (SUC (LENGTH l1)) (APPEND l1 (APPEND [x] l2)) = l2``,
	 Induct_on `l1` THENL
	 [RW_TAC list_ss [DROP,DROP1],
	  UNDISCH_ALL_TAC THEN
	  RW_TAC list_ss [DROP,DROP1]]);;



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


val _ = Hol_datatype 
    `value = 
    vInt of num
  | vBool of bool`;;
val is_vInt = Define
    `(is_vInt (vInt x) = T) /\ (is_vInt (vBool y) = F)`;;
val value_eq = Define
    `value_eq (x:value) y = (x = y)`;;
val dest_vInt = Define
    `dest_vInt (vInt x) = x`;;
val dest_vBool = Define
    `dest_vBool (vBool x) = x`;;
val vInt_add = Define
    `vInt_add x y = 
    if is_vInt x /\ is_vInt y then vInt (dest_vInt x + dest_vInt y)
    else vInt 0`;;
val vInt_add_sym = prove
    (``!x y. vInt_add x y = vInt_add y x``,
     R_TAC [vInt_add] THEN
     Induct_on `x` THENL
     [R_TAC [is_vInt] THEN
      Induct_on `y` THENL
      [R_TAC [is_vInt] THEN
       RW_TAC arith_ss [],
       R_TAC [is_vInt]],
      R_TAC [is_vInt]]);;


val _ = Hol_datatype
    `machine =
    machine_init |
    set_locvar of num => value => machine |
    push of value => machine`;;

val _ = Hol_datatype
    `opstack =
    opstack_emp |
    opstack_push of value => opstack`;;
val opstack_pop = Define
    `opstack_pop (opstack_push x s) = s`;;
val opstack_top = Define
    `opstack_top (opstack_push x s) = x`;;
val _ = Hol_datatype
    `locvars =
    locvars_nil |
    locvars_set of num => value => locvars`;;
val locvars_get = Define
    `locvars_get n1 (locvars_set n2 x l) =
    if n1 = n2 then x else locvars_get n1 l`;;
val _ = Hol_datatype
    `machine =
    Machine of opstack => locvars`;;
val machine_get_opstack = Define
    `machine_get_opstack (Machine s l) = s`;;
val machine_set_opstack = Define
    `machine_set_opstack s1 (Machine s l) = Machine s1 l`;;
val machine_get_locvars = Define
    `machine_get_locvars (Machine s l) = l`;;
val machine_set_locvars = Define
    `machine_set_locvars l1 (Machine s l) = Machine s l1`;;
(*** top level functions ***)
val get_locvar = Define
    `get_locvar n m = locvars_get n (machine_get_locvars m)`;;
val set_locvar = Define
    `set_locvar n x m = 
    let l1 = machine_get_locvars m in
    let l2 = locvars_set n x l1 in
	machine_set_locvars l2 m`;;
val pop = Define
    `pop m = 
    let s1 = machine_get_opstack m in
    let s2 = opstack_pop s1 in
	machine_set_opstack s2 m`;;
val top = Define
    `top m = opstack_top (machine_get_opstack m)`;;
val push = Define
    `push x m = 
    let s1 = machine_get_opstack m in
    let s2 = opstack_push x s1 in
	machine_set_opstack s2 m`;;



val machine_get_opstack_machine_set_opstack = prove
    (``!s m. machine_get_opstack (machine_set_opstack s m) = s``,
     Induct_on `m` THEN
     R_TAC [machine_get_opstack,machine_set_opstack]);;
val machine_set_opstack_machine_set_opstack = prove
    (``!s1 s2 m. machine_set_opstack s1 (machine_set_opstack s2 m) = 
     machine_set_opstack s1 m``,
     Induct_on `m` THEN
     R_TAC [machine_set_opstack]);;
val machine_set_opstack_machine_get_opstack = prove
    (``!m. machine_set_opstack (machine_get_opstack m) m = m``,
     Induct_on `m` THEN
     R_TAC [machine_get_opstack,machine_set_opstack]);;
val machine_get_locvars_machine_set_locvars = prove
    (``!l m. machine_get_locvars (machine_set_locvars l m) = l``,
     Induct_on `m` THEN
     R_TAC [machine_get_locvars,machine_set_locvars]);;
val machine_get_locvars_machine_set_opstack = prove
    (``!s m. machine_get_locvars (machine_set_opstack s m) = 
     machine_get_locvars m``,
     Induct_on `m` THEN
     R_TAC [machine_get_locvars,machine_set_opstack]);;
val machine_get_opstack_machine_set_locvars = prove
    (``!m. machine_get_opstack (machine_set_locvars l m) = 
     machine_get_opstack m``,
     Induct_on `m` THEN
     R_TAC [machine_get_opstack,machine_set_locvars]);;


(*** top level theorems ***)
val get_locvar_set_locvar = prove
    (``!n1 n2 x s. 
     get_locvar n1 (set_locvar n2 x s) =
     if n1 = n2 then x else get_locvar n1 s``,
     R_TAC [get_locvar,set_locvar] THEN
     LETR_TAC THEN
     R_TAC [machine_get_locvars_machine_set_locvars] THEN
     R_TAC [locvars_get]);;
val pop_push = prove
    (``!x m. pop (push x m) = m``, 
     R_TAC [pop,push] THEN LETR_TAC THEN
     R_TAC [machine_get_opstack_machine_set_opstack] THEN
     R_TAC [opstack_pop] THEN
     R_TAC [machine_set_opstack_machine_set_opstack] THEN
     R_TAC [machine_set_opstack_machine_get_opstack]);;
val top_push = prove
    (``!x m. top (push x m) = x``,
     R_TAC [top,push] THEN LETR_TAC THEN
     R_TAC [machine_get_opstack_machine_set_opstack] THEN
     R_TAC [opstack_top]);;
val get_locvar_push = prove
    (``!n x m. get_locvar n (push x m) = get_locvar n m``,
     R_TAC [get_locvar,push] THEN LETR_TAC THEN
     R_TAC [machine_get_locvars_machine_set_opstack]);;
val get_locvar_pop = prove
    (``!n m. get_locvar n (pop m) = get_locvar n m``,
     R_TAC [get_locvar,pop] THEN LETR_TAC THEN
     R_TAC [machine_get_locvars_machine_set_opstack]);;
val top_set_locvar = prove
    (``!n x s. top (set_locvar n x s) = top s``,
     R_TAC [top,set_locvar] THEN LETR_TAC THEN
     R_TAC [machine_get_opstack_machine_set_locvars]);;



val exec_load = Define
    `exec_load n s =
    let x = get_locvar n s in
	push x s`;;
val exec_store = Define
    `exec_store n s =
    let x = top s in
    let s1 = pop s in 
	set_locvar n x s1`;;
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 (vInt_add x1 x2) s2`;;
val comp = Define
    `comp s =
    let x = top s in
    let s1 = pop s in
    let y = top s1 in
    let s2 = pop s1 in
	(value_eq x y, s2)`;;
val _ = Hol_datatype 
    `instr = 
    Load of num
  | Store of num
  | Lit of value
  | Add
  | Ifcmpeq of num
  | Goto of num`;;
val exec_defn = Hol_defn "machine_exec"
    `(exec [] s = s) /\ 
     (exec ((Load x)::l) s = exec l (exec_load x s)) /\
     (exec ((Store x)::l) s = exec l (exec_store x s)) /\
     (exec ((Lit y)::l) s = exec l (exec_lit y s)) /\
     (exec (Add::l) s = exec l (exec_add s)) /\
     (exec ((Goto n)::l) s = exec (DROP n l) s) /\
     (exec ((Ifcmpeq n)::l) s = 
      let (b,s1) = comp s in
	  if b then exec (DROP n l) s1
	  else exec l s1)`;;
val exec = 
    #1(Defn.tprove(exec_defn,
		   WF_REL_TAC `measure (LENGTH o FST)` THEN
		   RW_TAC list_ss [LENGTH_DROP]));;



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


val _= Hol_datatype 
    `aexp =
    Int of num
  | Var of num
  | Sum of aexp => aexp`;;
val _= Hol_datatype 
    `bexp = 
    Bool of bool
  | Eq of aexp => aexp`;;
val _ = Hol_datatype
    `stm =
    Assign of aexp => aexp
  | If of bexp => stm => stm 
  | Seq of stm => stm`;;
val is_Var = Define
    `(is_Var (Var x) = T) /\ (is_Var (Int x) = F)
    /\ (is_Var (Sum y z) = F)`;;
val dest_Var = Define
    `dest_Var (Var x) = x`;;


val _ = Hol_datatype
    `env =
    env_init |
    set_var of num => value => env`;;
val get_var = Define
    `(get_var n env_init = vInt 0) /\
    (get_var n1 (set_var n2 x env) = 
     if n1 = n2 then x else get_var n1 env)`;;
val eval_aexp = Define
    `(eval_aexp (Int x) env = vInt x) /\
    (eval_aexp (Var x) env = get_var x env) /\
     (eval_aexp (Sum y z) env = vInt_add (eval_aexp y env) (eval_aexp z env))`;;
val eval_bexp = Define
    `(eval_bexp (Bool x) env = vBool x) /\
    (eval_bexp (Eq s t) env = vBool (value_eq (eval_aexp s env) (eval_aexp t env)))`;;
val eval = Define
    `(eval (Assign e1 e2) env = 
      if is_Var e1 then 
	  let x = dest_Var e1 in
	  let y = eval_aexp e2 env in
	      set_var x y env
      else
	  env) /\
     (eval (If e s1 s2) env = 
      if dest_vBool (eval_bexp e env) then eval s1 env
      else eval s2 env) /\
     (eval (Seq s1 s2) env = eval s2 (eval s1 env))`;;



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


val compile_aexp = Define
    `(compile_aexp (Int x) = [Lit (vInt x)]) /\
    (compile_aexp (Var x) = [Load x]) /\
     (compile_aexp (Sum e1 e2) =
      APPEND (compile_aexp e1) (APPEND (compile_aexp e2) [Add]))`;;
val compile_bexp = Define
    `(compile_bexp (Bool x) = [Lit (vBool x)]) /\
    (compile_bexp (Eq e1 e2) =
     APPEND (compile_aexp e1) 
     (APPEND (compile_aexp e2)
      [Ifcmpeq 2; Lit(vBool F); Goto 1; Lit(vBool T)]))`;;
val compile = Define
    `(compile (Assign e1 e2) = 
      if is_Var(e1) then 
	  APPEND (compile_aexp e2) [Store (dest_Var(e1))]
      else
	  []) /\
     (compile (If e s1 s2) =
      let cnd = compile_bexp e in 
      let thn = compile s1 in
      let els = compile s2 in
	  APPEND cnd 
	  (APPEND [Lit(vBool F); Ifcmpeq(LENGTH thn + 1)]
		   (APPEND thn (APPEND [Goto(LENGTH els)] els)))) /\
     (compile (Seq s1 s2) =
      APPEND (compile s1) (compile s2))`;;




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

val exec_APPEND_compile_aexp = prove
    (``!e l s. 
     exec (APPEND (compile_aexp e) l) s = 
     exec l (exec (compile_aexp e) s)``,
     Induct_on `e` THENL
     [R_TAC [compile_aexp] THEN
      RW_TAC list_ss [exec],
      R_TAC [compile_aexp] THEN
      RW_TAC list_ss [exec],
      R_TAC [compile_aexp] THEN
      R_TAC [APPEND_APPEND] THEN
      RW_TAC list_ss [exec]]);;
val exec_APPEND_compile_bexp = prove
    (``!e l s. 
     exec (APPEND (compile_bexp e) l) s = 
     exec l (exec (compile_bexp e) s)``,
     Induct_on `e` THENL
     [R_TAC [compile_bexp] THEN
      RW_TAC list_ss [exec],
      R_TAC [compile_bexp] THEN
      R_TAC [APPEND_APPEND] THEN
      RW_TAC list_ss [exec_APPEND_compile_aexp] THEN
      RW_TAC list_ss [exec] THEN
      PAIR_TAC ``comp (exec (compile_aexp a0)
		       (exec (compile_aexp a) s))`` THEN
      LETR_TAC THEN
      RW_TAC list_ss [] THENL
      [R_TAC [DECIDE ``2 = SUC (SUC 0)``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       RW_TAC bool_ss [exec],
       R_TAC [DECIDE ``1 = SUC 0``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       RW_TAC bool_ss [exec]]]);;
val exec_APPEND_compile = prove
    (``!s prog l. 
     exec (APPEND (compile prog) l) s =
     exec l (exec (compile prog) s)``,
     Induct_on `prog` THENL
     [R_TAC [compile] THEN 
      RW_TAC list_ss [] THENL
      [R_TAC [APPEND_APPEND] THEN
       RW_TAC list_ss [exec_APPEND_compile_aexp] THEN
       R_TAC [exec],
       R_TAC [exec]],
       R_TAC [compile] THEN LETR_TAC THEN
       R_TAC [APPEND_APPEND] THEN
       RW_TAC list_ss [exec_APPEND_compile_bexp] THEN
       R_TAC [exec] THEN
       PAIR_TAC ``comp (exec_lit (vBool F)
			(exec (compile_bexp b) s))`` THEN
       LETR_TAC THEN
       RW_TAC list_ss [] THENL
       [R_TAC [APPEND_APPEND] THEN
	R_TAC [DECIDE ``!n. n + 1 = SUC n``] THEN
	R_TAC [DROP_lemma] THEN
	RW_TAC bool_ss [],
	R_TAC [APPEND_APPEND] THEN
	RW_TAC list_ss [] THEN
	R_TAC [exec] THEN
	RW_TAC list_ss [DROP_LENGTH_APPEND] THEN
	RW_TAC list_ss [DROP_LENGTH] THEN
	R_TAC [exec]],
       R_TAC [compile] THEN
       R_TAC [APPEND_APPEND] THEN
       RW_TAC list_ss []]);;
val pop_exec_compile_aexp = prove
    (``!e s. pop (exec (compile_aexp e) s) = s``,
     Induct_on `e` THENL
     [R_TAC [compile_aexp] THEN
      R_TAC [exec,exec_lit] THEN
      R_TAC [pop_push],
      R_TAC [compile_aexp] THEN
      R_TAC [exec,exec_load] THEN LETR_TAC THEN
      R_TAC [pop_push],
      R_TAC [compile_aexp] THEN
      R_TAC [exec_APPEND_compile_aexp] THEN
      R_TAC [exec,exec_add] THEN
      LETR_TAC THEN
      R_TAC [pop_push] THEN
      RW_TAC list_ss []]);;
val get_locvar_exec_compile_aexp = prove
    (``!n e s. 
     get_locvar n (exec (compile_aexp e) s) = get_locvar n s``,
     Induct_on `e` THENL
     [R_TAC [exec,compile_aexp] THEN 
      R_TAC [exec_lit] THEN
      R_TAC [get_locvar_push],
      R_TAC [exec,compile_aexp] THEN 
      R_TAC [exec_load] THEN LETR_TAC THEN
      R_TAC [get_locvar_push],
      R_TAC [exec,compile_aexp] THEN
      R_TAC [exec_APPEND_compile_aexp] THEN
      R_TAC [exec,exec_add] THEN
      LETR_TAC THEN
      R_TAC [get_locvar_push] THEN
      R_TAC [pop_exec_compile_aexp]]);;
val compiler_aexp_correctness = prove
    (``!e s env. 
     (!n. get_locvar n s = get_var n env) ==>
	  (top (exec (compile_aexp e) s) = eval_aexp e env)``,
     Induct_on `e` THENL
     [R_TAC [compile_aexp,eval_aexp] THEN
      R_TAC [exec,exec_lit] THEN
      R_TAC [top_push],
      R_TAC [compile_aexp,eval_aexp] THEN
      R_TAC [exec,exec_load] THEN
      LETR_TAC THEN
      RW_TAC bool_ss [top_push],
      R_TAC [compile_aexp,eval_aexp] THEN
      R_TAC [exec_APPEND_compile_aexp] THEN
      R_TAC [exec,exec_add] THEN
      LETR_TAC THEN
      RW_TAC bool_ss [top_push] THEN
      RW_TAC bool_ss [pop_exec_compile_aexp] THEN
      ASSUM_LIST (fn thl => ASSUME_TAC
		  (SPEC ``exec (compile_aexp e) s`` (el 2 thl))) THEN
      ASSUM_LIST (fn thl => ASSUME_TAC
		  (REWRITE_RULE [get_locvar_exec_compile_aexp] (el 1 thl))) THEN
      RES_TAC THEN
      RW_TAC bool_ss [] THEN
      ACCEPT_TAC
      (SPECL [``eval_aexp e' env``,``eval_aexp e env``] vInt_add_sym)]);;
val comp_lemma1 = prove
    (``!s a1 a2 env.
     (!n. get_locvar n s = get_var n env) ==>
	  (FST (comp (exec (compile_aexp a1) (exec (compile_aexp a2) s))) =
	   (eval_aexp a1 env = eval_aexp a2 env))``,
     R_TAC [comp] THEN LETR_TAC THEN
     RW_TAC bool_ss [] THEN
     R_TAC [value_eq] THEN
     R_TAC [pop_exec_compile_aexp] THEN
     ASSUM_LIST (fn thl => ASSUME_TAC (SPEC ``n:num`` (el 1 thl))) THEN
     ASSUME_TAC (SPECL [``n:num``,``a2:aexp``,``s:machine``]
		 get_locvar_exec_compile_aexp) THEN
     IMP_RES_TAC
     (REWRITE_RULE
      [get_locvar_exec_compile_aexp]
      (SPECL [``a1:aexp``,``exec (compile_aexp a2) s``]
       compiler_aexp_correctness)) THEN
     IMP_RES_TAC compiler_aexp_correctness THEN
     RW_TAC bool_ss []);;
val compiler_bexp_correctness = prove
    (``!s e env. 
     (!n. get_locvar n s = get_var n env) ==>
	  (top (exec (compile_bexp e) s) = eval_bexp e env)``,
     LETR_TAC THEN Induct_on `e` THENL
     [R_TAC [compile_bexp,eval_bexp] THEN
      R_TAC [exec,exec_lit] THEN
      R_TAC [top_push],
      REPEAT STRIP_TAC THEN
      R_TAC [compile_bexp,eval_bexp] THEN
      R_TAC [exec_APPEND_compile_aexp] THEN
      R_TAC [exec] THEN
      PAIR_TAC ``comp (exec (compile_aexp a0)
		       (exec (compile_aexp a) s))`` THEN
      LETR_TAC THEN
      RW_TAC bool_ss [] THENL
      [R_TAC [DECIDE ``2 = SUC (SUC 0)``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       R_TAC [exec] THEN
       R_TAC [exec_lit,top_push] THEN
       RW_TAC bool_ss [] THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       IMP_RES_TAC comp_lemma1 THEN
       RW_TAC bool_ss [value_eq],
       R_TAC [DECIDE ``1 = SUC 0``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       R_TAC [exec] THEN
       RW_TAC bool_ss [exec_lit,top_push] THEN
       R_TAC [value_eq] THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       IMP_RES_TAC comp_lemma1 THEN
       RW_TAC bool_ss []]]);;



val get_locvar_exec_compile_bexp = prove
    (``!n b s. get_locvar n (exec (compile_bexp b) s) = get_locvar n s``,
     Induct_on `b` THENL
     [R_TAC [compile_bexp] THEN
      R_TAC [exec,exec_lit] THEN
      R_TAC [get_locvar_push],
      R_TAC [compile_bexp] THEN
      R_TAC [exec_APPEND_compile_aexp] THEN
      RW_TAC list_ss [exec] THEN
      PAIR_TAC 
      ``comp (exec (compile_aexp a0)
	      (exec (compile_aexp a) s))`` THEN
      LETR_TAC THEN
      RW_TAC bool_ss [] THENL
      [R_TAC [DECIDE ``2 = SUC (SUC 0)``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       R_TAC [exec] THEN
       R_TAC [exec_lit,comp] THEN LETR_TAC THEN
       R_TAC [get_locvar_push,get_locvar_pop] THEN
       R_TAC [get_locvar_exec_compile_aexp],
       R_TAC [DECIDE ``1 = SUC 0``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       R_TAC [exec] THEN
       R_TAC [exec_lit,comp] THEN LETR_TAC THEN
       R_TAC [get_locvar_push,get_locvar_pop] THEN
       R_TAC [get_locvar_exec_compile_aexp]]]);;
val get_locvar_lemma = prove
    (``!n b s. 
     get_locvar n  
     (SND (comp (exec_lit (vBool F)
		 (exec (compile_bexp b) s)))) = get_locvar n s``,
     R_TAC [comp] THEN LETR_TAC THEN
     R_TAC [get_locvar_pop] THEN
     R_TAC [exec_lit] THEN
     R_TAC [get_locvar_push] THEN
     R_TAC [get_locvar_exec_compile_bexp]);;



val comp_push_push = prove
    (``!x y s. FST (comp (push x (push y s))) = value_eq x y``,
     R_TAC [comp] THEN LETR_TAC THEN
     R_TAC [top_push,pop_push]);;
val comp_lemma2 = prove
    (``!b s env.
     (!n. get_locvar n s = get_var n env) ==>
	  (FST (comp (exec_lit (vBool F)
		      (exec (compile_bexp b) s))) = 
		       ~dest_vBool (eval_bexp b env))``,
     Induct_on `b` THENL
     [R_TAC [compile_bexp] THEN
      R_TAC [exec,exec_lit] THEN
      R_TAC [comp_push_push] THEN
      R_TAC [eval_bexp,value_eq] THEN
      R_TAC [dest_vBool] THEN
      RW_TAC bool_ss [],
      R_TAC [compile_bexp] THEN
      R_TAC [exec_APPEND_compile_aexp] THEN
      RW_TAC list_ss [exec] THEN
      PAIR_TAC ``comp (exec (compile_aexp a0)
		       (exec (compile_aexp a) s))`` THEN
      LETR_TAC THEN
      RW_TAC list_ss [] THENL
      [R_TAC [DECIDE ``2 = SUC (SUC 0)``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       R_TAC [exec,exec_lit] THEN
       R_TAC [comp_push_push] THEN
       R_TAC [eval_bexp,value_eq] THEN
       RW_TAC bool_ss [dest_vBool] THEN
       IMP_RES_TAC comp_lemma1 THEN
       RW_TAC bool_ss [],
       R_TAC [DECIDE ``1 = SUC 0``] THEN
       RW_TAC list_ss [DROP,DROP1] THEN
       R_TAC [exec,exec_lit] THEN
       R_TAC [comp_push_push] THEN
       R_TAC [eval_bexp,value_eq] THEN
       RW_TAC bool_ss [dest_vBool] THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       IMP_RES_TAC comp_lemma1 THEN
       RW_TAC bool_ss []]]);;



 
val compiler_correctness = prove
    (``!n s prog env.
     (!n. get_locvar n s = get_var n env) ==>
	  (get_locvar n (exec (compile prog) s) =
	   get_var n (eval prog env))``,
     Induct_on `prog` THENL
     [R_TAC [compile,eval] THEN LETR_TAC THEN
      Induct_on `a` THENL
      [SIMP_TAC list_ss [is_Var] THEN
       RW_TAC bool_ss [exec],
       SIMP_TAC list_ss [is_Var] THEN
       RW_TAC list_ss [dest_Var] THEN
       R_TAC [exec_APPEND_compile_aexp] THEN
       R_TAC [exec] THEN
       R_TAC [exec_store] THEN LETR_TAC THEN
       R_TAC [pop_exec_compile_aexp] THEN
       Cases_on `n = n'` THENL
       [RW_TAC bool_ss [get_locvar_set_locvar,get_var] THEN
	ASM_SIMP_TAC bool_ss [compiler_aexp_correctness],
	RW_TAC bool_ss [get_locvar_set_locvar,get_var]],
       SIMP_TAC list_ss [is_Var] THEN
       RW_TAC bool_ss [exec]],
      R_TAC [compile] THEN LETR_TAC THEN
      R_TAC [exec_APPEND_compile_bexp] THEN
      RW_TAC list_ss [exec] THEN
      PAIR_TAC 
      ``comp (exec_lit (vBool F)
	      (exec (compile_bexp b) s))`` THEN
      LETR_TAC THEN
      RW_TAC list_ss [] THENL
      [R_TAC [DECIDE ``!n. n + 1 = SUC n``] THEN
       R_TAC [APPEND_APPEND] THEN
       R_TAC [DROP_lemma] THEN
       ASSUM_LIST (fn thl => ASSUME_TAC
		   (SPECL [``n:num``,
			   ``SND (comp (exec_lit (vBool F) (exec (compile_bexp b) s)))``,``env:env``] (el 3 thl))) THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       R_TAC [get_locvar_lemma] THEN
       RW_TAC bool_ss [] THEN
       R_TAC [eval] THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 2 thl)) THEN
       IMP_RES_TAC comp_lemma2 THEN
       RW_TAC bool_ss [],
       R_TAC [APPEND_APPEND] THEN
       R_TAC [exec_APPEND_compile] THEN
       RW_TAC list_ss [exec] THEN
       R_TAC [DROP_LENGTH] THEN
       R_TAC [exec] THEN
       ASSUM_LIST (fn thl => ASSUME_TAC
		   (SPECL [``n:num``,
			   ``SND (comp (exec_lit (vBool F) (exec (compile_bexp b) s)))``,
			   ``env:env``] (el 4 thl))) THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 1 thl)) THEN
       R_TAC [get_locvar_lemma] THEN
       RW_TAC bool_ss [] THEN
       R_TAC [eval] THEN
       ASSUM_LIST (fn thl => THM_UNDISCH_TAC (el 2 thl)) THEN
       IMP_RES_TAC comp_lemma2 THEN
       RW_TAC bool_ss []],
       R_TAC [compile,eval] THEN
       R_TAC [exec_APPEND_compile] THEN
       RW_TAC bool_ss []]);;