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 []);

g `!p p'. Add(p p') ==>