Parse.hide "o";
load "stringLib";

type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of num | Empty`;
Hol_datatype `opcode = opAdd | opPush of operand`;
Hol_datatype `arith_exp = Term of operand | Add of arith_exp => arith_exp`;

Hol_datatype `statement = Assign of ID => arith_exp`;

val interpAdd_def = Define `
    (interpAdd(Num(x), Num(y)) = Num(x+y)) /\
    (interpAdd(_, _) = Empty)`;
val interpExp_def = Define `
    (interpExp(Term(Empty)) = Empty) /\
    (interpExp(Term(Num(r))) = Num(r)) /\
    (interpExp(Add A B) = interpAdd(interpExp(A), interpExp(B)))`;
val interpExp_ind = fetch "-" "interpExp_ind";

val compExp_def = Define `
    (compExp(Term(Empty)) = [opPush(Empty)]) /\
    (compExp(Term(Num(r))) = [opPush(Num(r))]) /\
    (compExp(Add A B) = compExp(A) ++ compExp(B) ++ [opAdd])`;
    
val evaluate_def = Define `
    (evaluate((opPush(Empty)::Opcodes), Q) = evaluate(Opcodes, Q)) /\
    (evaluate((opPush(Num Val)::Opcodes), Q) = evaluate(Opcodes, [(Num Val)] ++ Q)) /\
    (evaluate((opAdd::Opcodes), val1::val2::Q) = evaluate(Opcodes, [interpAdd(val1, val2)] ++ Q)) /\
(*    (evaluate((opAdd::Opcodes), ((Num val1)::(Num val2)::Q)) = evaluate(Opcodes, [Num(val1+val2)] ++ Q)) /\*)
(*    (evaluate((_::Opcodes), (_::_::Q)) = evaluate(Opcodes, [Empty] ++ Q)) /\*)
    (evaluate((_::Opcodes), [_]) = evaluate(Opcodes, [Empty])) /\
    (evaluate((_::Opcodes), []) = evaluate(Opcodes, [Empty])) /\
    (evaluate([], top::Q) = top) /\
    (evaluate([], []) = Empty)`;
val evaluate_ind = fetch "-" "evaluate_ind";


(*----------------------------------------------------------------------------*)
val comp_ss = list_ss ++ rewrites [interpAdd_def, interpExp_def, compExp_def, evaluate_def];
g `!oplist prog. (oplist = compExp prog) ==> (evaluate(oplist, []) = interpExp(prog))`;
e (FULL_SIMP_TAC comp_ss []);
e Induct;
e (Cases_on `$o` THEN FULL_SIMP_TAC comp_ss []);
e (RW_TAC comp_ss []);
g `evaluate(A ++ [opAdd], []) = evaluate([opAdd] ++ [evaluate(A, [])], [])`;

g `!prog oplist op. (oplist = compExp prog) /\ (op::L = oplist) ==> ~(op = opAdd)`;
e (Induct_on `prog` THEN FULL_SIMP_TAC comp_ss []);
e (Cases_on `$o` THEN RW_TAC comp_ss []);


load "stringLib";
open listTheory;

map hide ["o", "C"];

Hol_datatype `aexp = Var of string | Const of num | Add of aexp => aexp`;

Hol_datatype `atom = V of string | C of num`;

Hol_datatype `opcode = opAdd | opPush of atom`;

val evalExp_def =
 Define 
    `(evalExp env (Var s) = env s :num) /\
     (evalExp env (Const n) = n) /\
     (evalExp env (Add e1 e2) = evalExp env e1 + evalExp env e2)`;

val compExp_def =
 Define 
    `(compExp (Var s) = [opPush (V s)]) /\
     (compExp (Const n) = [opPush (C n)]) /\
     (compExp (Add e1 e2) = compExp e2 ++ compExp e1 ++ [opAdd])`;

val Int_def = 
 Define
  `(Int env [] stk = stk) /\
   (Int env (opPush(V s)::opcodes) stk = Int env opcodes (env s :: stk)) /\
   (Int env (opPush(C n)::opcodes) stk = Int env opcodes (n :: stk)) /\
   (Int env (opAdd::opcodes) (v1::v2::stk) = Int env opcodes (v1+v2::stk))`;

val Int_ind = fetch "-" "Int_ind";
val comp_ss = list_ss ++ rewrites [evalExp_def, compExp_def, Int_def];

(*---------------------------------------------------------------------------*)
(* Lemmas                                                                    *)
(*---------------------------------------------------------------------------*)
 
val compExp_not_empty = Q.prove
(`!e. ~NULL (compExp e)`,
 Induct THEN RW_TAC comp_ss [] THEN 
 Cases_on `compExp e'` THEN FULL_SIMP_TAC comp_ss []);

val NOT_NULL = Q.prove
(`!l. ~NULL l ==> ?h t. l = h::t`,
Cases THEN RW_TAC list_ss []);

val NULL_EMPTY_LEM = Q.prove
(`!l. NULL l = (l=[])`,
Cases THEN RW_TAC list_ss []);

val compExp_hd_not_Add = Q.prove
(`!e. ~(HD (compExp e) = opAdd)`,
 Induct THEN RW_TAC comp_ss [] THEN 
 `?h t. compExp e' = h::t` by METIS_TAC [compExp_not_empty, NOT_NULL] THEN
 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC comp_ss []);

val THE_LEMMA = Q.prove
(`!e env stk rst.
      Int env (compExp e ++ rst) stk = 
      Int env rst (evalExp env e::stk)`,
 Induct THEN RW_TAC comp_ss [] THEN
 ASM_REWRITE_TAC [GSYM APPEND_ASSOC] THEN
 RW_TAC comp_ss []);

val Correctness = Q.prove
(`!e env stk h stk'. 
    (Int env (compExp e) stk = h::stk') ==> (h = evalExp env e)`,
 Induct THEN RW_TAC comp_ss [] 
   THEN RULE_ASSUM_TAC (REWRITE_RULE [GSYM APPEND_ASSOC]) 
   THEN FULL_SIMP_TAC comp_ss [THE_LEMMA]);