(***************************************HOL PROGRAM***************************************)
load "intLib";
load "stringLib";
type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of num | VarName of ID | Empty`;
Hol_datatype `opcode = opPush of operand | opAdd | opPop of ID `;

Hol_datatype `arith_exp =
     Term     of operand
    |Add      of arith_exp => arith_exp`;

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

val getnum_def = Define `
   (getnum(Num(i)) = i)`;

val STRLT_def = Define `
   (STRLT "" s = T) /\
   (STRLT (STRING c s) "" = F) /\
   (STRLT (STRING c1 t1) (STRING c2 t2) = ORD c1 < ORD c2 /\ STRLT t1 t2)`;

val setvar_def = Define `
   (setvar(a, _, VarName(_)) = a) /\
   (setvar([], n:ID, v:operand) = [(n,v)]) /\
   (setvar(((N, V)::List), n, v) =
      if STRLT N n then (N,V)::setvar(List, n, v)
      else if N = n then (N, v)::List
      else (n,v)::(N,V)::List)`;

val getvar_def = Define ` 
   (getvar([], n:ID) = Empty) /\
   (getvar(((N, V)::List), n) =
      if STRLT N n then getvar(List, n)
      else if N = n then V
      else Empty)`;

val evaladd_def = Define `
	(evaladd(Num(x), Num(y)) = Num(x+y)) /\
	(evaladd(_, _) = Empty)`;

val evalexp_def = Define `
   (evalexp(Term(Empty), _) = Empty) /\
   (evalexp(Term(Num(r)), _) = Num(r)) /\
   (evalexp(Add A B, VarTable) = evaladd(evalexp(A, VarTable), evalexp(B, VarTable))) /\
   (evalexp(Term(VarName(v)), VarTable) = getvar(VarTable, v))`;

val evaluate1_def = Define `
   (evaluate1([], VarTable) = VarTable) /\
   (evaluate1(((Assign Var Exp)::Program), VarTable) = 
      evaluate1(Program, setvar(VarTable, Var, evalexp(Exp, VarTable))))`; 
val evaluate1_ind = fetch "-" "evaluate1_ind";

val evaluate_def = Define `
   (evaluate(Program) = evaluate1(Program, []))`;

val compexp_def = Define `
   (compexp(Term(Empty)) = [opPush(Empty)]) /\
   (compexp(Term(Num(r))) = [opPush(Num(r))]) /\
   (compexp(Term(VarName(v))) = [opPush(VarName(v))]) /\
   (compexp(Add A B) = compexp(A) ++ compexp(B) ++ [opAdd])`;

val compile1_def = Define `
   (compile1([]) = ([])) /\
   (compile1(((Assign Var Exp)::Program)) = 
          compexp(Exp) ++
           [opPop Var] ++
           compile1(Program) )`;
val compile1_ind = fetch "-" "compile1_ind";

val compile_def = Define `
   (compile(Program) = compile1(Program))`;

val interpret1_def = Define `
   (interpret1(((opPop Var)::Opcodes), VarTable, []) = 
               interpret1(Opcodes, setvar(VarTable, Var, Empty), [])) /\
   (interpret1([], VarTable, _) = VarTable) /\
   (interpret1((opPush(Empty)::Opcodes), VarTable, Q) = 
               interpret1(Opcodes, VarTable, Q)) /\
   (interpret1((opPush(Num Val)::Opcodes), VarTable, Q) = 
               interpret1(Opcodes, VarTable, [(Num Val)] ++ Q)) /\
   (interpret1((opPush(VarName Var)::Opcodes), VarTable, Q) = 
               interpret1(Opcodes, VarTable, [getvar(VarTable, Var)] ++ Q)) /\ 
   (interpret1(((opPop Var)::Opcodes), VarTable, (op1::Q)) = 
               interpret1(Opcodes, setvar(VarTable, Var, op1), Q)) /\ 
   (interpret1((opAdd::Opcodes), VarTable, []) = 
               interpret1(Opcodes, VarTable, [Empty])) /\
   (interpret1((opAdd::Opcodes), VarTable, [_]) = 
               interpret1(Opcodes, VarTable, [Empty])) /\
   (interpret1((opAdd::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(Opcodes, VarTable, [Num(val1+val2)] ++ Q)) /\
   (interpret1((opAdd::Opcodes), VarTable, (_::_::Q)) = 
               interpret1(Opcodes, VarTable, [Empty] ++ Q))`;
val interpret1_ind = fetch "-" "interpret1_ind";

val interpret_def = Define `
   (interpret(Opcodes) = interpret1(Opcodes, [], []))`;


(*******************************************PROOF*******************************************)
g `!prog p state1 state2.
(p = compile prog) /\ (interpret(p) = state1) /\ (evaluate(prog) = state2) ==> (state1 = state2)`;
e (SIMP_TAC std_ss [compile_def, interpret_def, evaluate_def]);
e (recInduct compile1_ind);
e (FULL_SIMP_TAC std_ss [compile1_def, interpret1_def, evaluate1_def]);
e (GEN_TAC);
e (Induct_on `Program`);
e (RW_TAC std_ss [compile1_def, evaluate1_def, interpret1_def]);
e (Induct_on `Exp`);
e (GEN_TAC);
e (SIMP_TAC list_ss [setvar_def]);
Parse.hide "o";
e (Cases_on `$o` THEN RW_TAC list_ss [evalexp_def, compexp_def, setvar_def, getvar_def, interpret1_def]);
e (RW_TAC list_ss [compexp_def, evalexp_def, evaladd_def]);
e (FULL_SIMP_TAC list_ss []);
e (Induct_on `Exp`);
e GEN_TAC;
e (Induct_on `Exp'`);
e GEN_TAC;
e (RW_TAC list_ss [evalexp_def]);
e (Cases_on `$o`);
e (Cases_on `o'` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (RW_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `$o` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `Exp'`);
e (Cases_on `Exp''`);
e (Cases_on `o'`);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'`);
e (Cases_on `a`);
e (Cases_on `a0`);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'`);
e (Cases_on `a`);
e (Cases_on `a0'`);
e (Cases_on `o'`);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o''` THEN FULL_SIMP_TAC list_ss [evalexp_def, getvar_def, interpret1_def, setvar_def, compexp_def, evaladd_def]);
e (Cases_on `o'`);
e (Cases_on `a`);
e (Cases_on `a0`);






(*--------------------------Lemma: recursive proof of interpret1()--------------------------*)
g `!X Y V Q. interpret1(X ++ Y::Prog, V, Q) = interpret1(Y::Prog,interpret1(X, V, Q), Q)`;
e (RW_TAC list_ss []);
e (Induct_on `X`);
e (RW_TAC list_ss [interpret1_def]);
e (Cases_on `h`);
e (Cases_on `o'` THEN RW_TAC list_ss [interpret1_def, getvar_def, setvar_def]);