(***********************************************************************)
load "intLib";
load "stringLib";
type_abbrev("ID", Type`:string`);
Hol_datatype `operand = Num of int | VarName of ID | Empty`;
Hol_datatype `opcode = opPush of operand | opAdd | opSub | opMul | opDiv | opGt | opGtEq
    | opLt | opLtEq | opEq | opNEq | opNeg | opAnd | opOr | opNot | opXor
    | opBrT of int| opBrF of int| opJmp of int| opPop of ID | Label of int`;

Hol_datatype `arith_exp =
     Term     of operand
    |Add      of arith_exp => arith_exp
    |Subtract of arith_exp => arith_exp
    |Multiply of arith_exp => arith_exp
    |Divide   of arith_exp => arith_exp
    |Negate   of arith_exp`;

Hol_datatype `bool_exp =
     Gt  of arith_exp => arith_exp
    |Lt  of arith_exp => arith_exp
    |Eq  of arith_exp => arith_exp
    |LtE of arith_exp => arith_exp
    |GtE of arith_exp => arith_exp
    |NEq of arith_exp => arith_exp
    |And of  bool_exp => bool_exp
    |Or  of  bool_exp => bool_exp
    |Xor of  bool_exp => bool_exp
    |Not of  bool_exp`;

Hol_datatype `statement =
     Assign        of ID => arith_exp
    |Loop_PreTest  of bool_exp => statement list
    |Loop_PostTest of statement list => bool_exp
    |Iterate       of ID => arith_exp => arith_exp => arith_exp => statement list
    |If_Then       of bool_exp => statement list
    |If_Then_Else  of bool_exp => statement list => statement list`;

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([], 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 evalexp_def = Define `
   (evalexp(Term(Empty), VarTable) = 0) /\
   (evalexp(Term(Num(r)), VarTable) = r) /\
   (evalexp(Add A B, VarTable) = evalexp(A, VarTable) + evalexp(B, VarTable)) /\
   (evalexp(Subtract A B, VarTable) = evalexp(A, VarTable) - evalexp(B, VarTable)) /\
   (evalexp(Multiply A B, VarTable) = evalexp(A, VarTable) * evalexp(B, VarTable)) /\
   (evalexp(Divide A B, VarTable) = evalexp(A, VarTable) / evalexp(B, VarTable)) /\
   (evalexp(Negate A, VarTable) = ~(evalexp(A, VarTable))) /\
   (evalexp(Term(VarName(v)), VarTable) = getnum(getvar(VarTable, v)))`;

val evalbool_def = Define `
   (evalbool((Gt A1 A2), VarTable) = evalexp(A1, VarTable) > evalexp(A2, VarTable)) /\
   (evalbool((Lt A1 A2), VarTable) = evalexp(A1, VarTable) < evalexp(A2, VarTable)) /\
   (evalbool((Eq A1 A2), VarTable) = (evalexp(A1, VarTable) = evalexp(A2, VarTable))) /\
   (evalbool((LtE A1 A2), VarTable) = evalexp(A1, VarTable) <= evalexp(A2, VarTable)) /\
   (evalbool((GtE A1 A2), VarTable) = evalexp(A1, VarTable) >= evalexp(A2, VarTable)) /\
   (evalbool((NEq A1 A2), VarTable) = ~((evalexp(A1, VarTable)) = (evalexp(A2, VarTable)))) /\
   (evalbool((And B1 B2), VarTable) = evalbool(B1, VarTable) /\ evalbool(B2, VarTable)) /\
   (evalbool((Or B1 B2), VarTable) = evalbool(B1, VarTable) \/ evalbool(B2, VarTable)) /\
   (evalbool((Xor B1 B2), VarTable) = ~(evalbool(B1, VarTable) = evalbool(B2, VarTable))) /\
   (evalbool((Not B), VarTable) = ~(evalbool(B, VarTable)))`;

val defn = Hol_defn "evaluate1" `
   (evaluate1(0n, _, VarTable) = VarTable) /\
   (evaluate1(_, [], VarTable) = VarTable) /\
   (evaluate1(N, ((Assign Var Exp)::Program), VarTable) = 
      evaluate1(N-1, Program, setvar(VarTable, Var, Num(evalexp(Exp, VarTable))))) /\ 
   (evaluate1(N, ((If_Then B_exp St)::Program), VarTable) = 
      if evalbool(B_exp, VarTable) 
         then evaluate1(N-1, Program, evaluate1(N-1, St, VarTable)) 
         else evaluate1(N-1, Program, VarTable)) /\
   (evaluate1(N, ((If_Then_Else B_exp St Sf)::Program), VarTable) = 
      if evalbool(B_exp, VarTable) 
         then evaluate1(N-1, Program, evaluate1(N-1, St, VarTable)) 
         else evaluate1(N-1, Program, evaluate1(N-1, Sf, VarTable))) /\
   (evaluate1(N, ((Loop_PreTest B_exp St)::Program), VarTable) = 
      if evalbool(B_exp, VarTable) 
         then evaluate1(N-1, ((Loop_PreTest B_exp St)::Program), evaluate1(N-1, St, VarTable))
         else evaluate1(N-1, Program, VarTable)) /\
   (evaluate1(N, ((Loop_PostTest St B_exp)::Program), VarTable) =
      let VarTable = evaluate1(N-1, St, VarTable) in
         if evalbool(B_exp, VarTable)
            then evaluate1(N-1, ((Loop_PostTest St B_exp)::Program), evaluate1(N-1, St, VarTable))
            else evaluate1(N-1, Program, VarTable)
      ) /\
   (evaluate1(N, ((Iterate Var Low High Inc St)::Program), VarTable) = 
      let VarTable = setvar(VarTable, Var, Num(evalexp(Low, VarTable))) in
      let NewLow = Term(Num(evalexp(Add Low Inc, VarTable))) in
         if evalbool(GtE Low High, VarTable)
            then evaluate1(N-1, ((Iterate Var NewLow High Inc St)::Program), evaluate1(N-1, St, VarTable))
            else evaluate1(N-1, Program, VarTable))`;
val (evaluate1_def, evaluate1_ind) = Defn.tprove(defn, WF_REL_TAC `measure FST`);

val evaluate_def = Define `
   (evaluate(Program, State) = ?n. evaluate1(n, Program, []) = State)`;

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]) /\
   (compexp(Subtract A B) = compexp(A) ++ compexp(B) ++ [opSub]) /\
   (compexp(Multiply A B) = compexp(A) ++ compexp(B) ++ [opMul]) /\
   (compexp(Divide A B) = compexp(A) ++ compexp(B) ++ [opDiv]) /\
   (compexp(Negate A) = compexp(A) ++ [opNeg])`;

val compbool_def = Define `
   (compbool(Gt A1 A2) = compexp(A1) ++ compexp(A2) ++ [opGt]) /\
   (compbool(Lt A1 A2) = compexp(A1) ++ compexp(A2) ++ [opLt]) /\
   (compbool(Eq A1 A2) = compexp(A1) ++ compexp(A2) ++ [opEq]) /\
   (compbool(LtE A1 A2) = compexp(A1) ++ compexp(A2) ++ [opLtEq]) /\
   (compbool(GtE A1 A2) = compexp(A1) ++ compexp(A2) ++ [opGtEq]) /\
   (compbool(NEq A1 A2) = compexp(A1) ++ compexp(A2) ++ [opNEq]) /\
   (compbool(And B1 B2) = compbool(B1) ++ compbool(B2) ++ [opAnd]) /\
   (compbool(Or B1 B2) = compbool(B1) ++ compbool(B2) ++ [opOr]) /\
   (compbool(Xor B1 B2) = compbool(B1) ++ compbool(B2) ++ [opXor]) /\
   (compbool(Not B) = compbool(B) ++ [opNot])`;

val defn = Hol_defn "compile1" `
   (compile1([], label) = ([], label)) /\
   (compile1(((Assign Var Exp)::Program), label) = 
	   let (prog_ops, label) = compile1(Program, label) in
          ( compexp(Exp) ++
           [opPop Var] ++
           prog_ops, label )) /\
   (compile1(((If_Then B_exp St)::Program), label) = 
       let DoneLabel = label in
       let (stmt_ops, label) = compile1(St, label+1) in
       let (prog_ops, label) = compile1(Program, label) in
          ( compbool(B_exp) ++
           [opBrF DoneLabel] ++
           stmt_ops ++
           [Label DoneLabel] ++
           prog_ops, label )) /\
   (compile1(((If_Then_Else B_exp St Sf)::Program), label) = 
       let ElseLabel = label in
       let DoneLabel = label+1 in
       let (stmtT_ops, label) = compile1(St, label+2) in
       let (stmtF_ops, label) = compile1(Sf, label) in
       let (prog_ops, label) = compile1(Program, label) in
          ( compbool(B_exp) ++
           [opBrF ElseLabel] ++
           stmtT_ops ++
           [opJmp DoneLabel] ++
           [Label ElseLabel] ++
           stmtF_ops ++
           [Label DoneLabel] ++
           prog_ops, label)) /\
   (compile1(((Loop_PreTest B_exp St)::Program), label) =
       let TestLabel = label in
       let DoneLabel = label+1 in
       let (stmt_ops, label) = compile1(St, label+2) in
       let (prog_ops, label) = compile1(Program, label) in
          ( [Label TestLabel] ++
           compbool(B_exp) ++
           [opBrF DoneLabel] ++
           stmt_ops ++
           [opJmp TestLabel] ++
           [Label DoneLabel] ++
           prog_ops, label )) /\
   (compile1(((Loop_PostTest St B_exp)::Program), label) =
       let TestLabel = label in
       let (stmt_ops, label) = compile1(St, label+1) in
       let (prog_ops, label) = compile1(Program, label) in
          ( [Label TestLabel] ++
           stmt_ops ++
           compbool(B_exp) ++
           [opBrT TestLabel] ++
           prog_ops, label )) /\
   (compile1(((Iterate Var El Eh Ei St)::Program), label) = 
       let AssignLabel = label in
       let DoneLabel = label+1 in
       let (stmt_ops, label) = compile1(St, label+2) in
       let (prog_ops, label) = compile1(Program, label) in
          (  compexp(El) ++
           [Label AssignLabel] ++
           [opPop(Var)] ++
           compexp(Eh) ++
           [opPush (VarName Var)] ++
           [opGt] ++
           [opBrT DoneLabel] ++
           stmt_ops ++
           compexp(Ei) ++
           [opPush (VarName Var)] ++
           [opAdd] ++
           [opJmp AssignLabel] ++
           [Label DoneLabel] ++
           prog_ops, label ))`;

val statement_size_def = fetch "-" "statement_size_def";
val list_size_def = listTheory.list_size_def;
val list_size_eq_statement1_size = 
   Q.prove (`!sl. list_size statement_size sl = statement1_size sl`, Induct 
      THEN RW_TAC list_ss [statement_size_def,list_size_def]);
val (compile1_def, compile1_ind) = 
   Defn.tprove (defn, WF_REL_TAC `measure (list_size statement_size o FST)` 
      THEN RW_TAC arith_ss [list_size_eq_statement1_size]); 

val compile_def = Define `
   (compile(Program) = 
       let (oplist, lbl) = compile1(Program, 1) in
          oplist)`;

val findlabel_def = Define `
   (findlabel([], L) = []) /\
   (findlabel((Label(l)::P), L) = if l = L then P else findlabel(P, L)) /\
   (findlabel((_::P), L) = findlabel(P, L))`;

val defn = Hol_defn "interpret1" `
   (interpret1(0n, _, _, VarTable, _) = VarTable) /\
   (interpret1(_, _, [], VarTable, _) = VarTable) /\
   (interpret1(N, WOpcodes, (opPush(Empty)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, Q)) /\
   (interpret1(N, WOpcodes, (opPush(Num Val)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [(Num Val)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opPush(VarName Var)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [getvar(VarTable, Var)] ++ Q)) /\ 
   (interpret1(N, WOpcodes, ((opPop Var)::Opcodes), VarTable, (op1::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, setvar(VarTable, Var, op1), Q)) /\ 
   (interpret1(N, WOpcodes, (opAdd::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1+val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opSub::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1-val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opDiv::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1/val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opMul::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(val1*val2)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opGt::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1<val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opGtEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1<=val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opLt::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1>val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opLtEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1<=val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if val1=val2 then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opNEq::Opcodes), VarTable, ((Num val1)::(Num val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=val2) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opNeg::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(~val1)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opNot::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=0) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opAnd::Opcodes), VarTable, (Num(val1)::Num(val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=0) /\ ~(val2=0) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opOr::Opcodes), VarTable, (Num(val1)::Num(val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=0) \/ ~(val2=0) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, (opXor::Opcodes), VarTable, (Num(val1)::Num(val2)::Q)) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, [Num(if ~(val1=val2) then 1 else 0)] ++ Q)) /\
   (interpret1(N, WOpcodes, ((opBrT L)::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, (if ~(val1=0) then findlabel(WOpcodes,L) else Opcodes), VarTable, Q)) /\
   (interpret1(N, WOpcodes, ((opBrF L)::Opcodes), VarTable, (Num(val1)::Q)) = 
               interpret1(N-1, WOpcodes, (if val1=0 then findlabel(WOpcodes,L) else Opcodes), VarTable, Q)) /\
   (interpret1(N, WOpcodes, ((opJmp L)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, findlabel(WOpcodes,L), VarTable, Q)) /\
   (interpret1(N, WOpcodes, ((Label _)::Opcodes), VarTable, Q) = 
               interpret1(N-1, WOpcodes, Opcodes, VarTable, Q))`;
val (interpret1_def, interpret1_ind) = Defn.tprove(defn, WF_REL_TAC `measure FST`);

val interpret_def = Define `
   (interpret(Opcodes, State) = ?n. interpret1(n, Opcodes, Opcodes, [], []) = State)`;

val statesEqual_def = Define `
   (statesEqual([], []) = T) /\
   (statesEqual([], _) = F) /\
   (statesEqual(_, []) = F) /\
   (statesEqual(((N1:ID,V1:operand)::L1),((N2:ID,V2:operand)::L2)) = 
      (N1=N2) /\ (V1=V2) /\ statesEqual(L1,L2))`;

(*-----------------------------------------PROOF------------------------------------------*)
g `!n p1 p2 st stk prog m state1 state2.
       (p1 = compile prog) /\ (p1=p2) /\ (st=[]) /\ (stk=[]) /\
       (interpret1(n,p1,p2,st,stk) = state1) /\
       (evaluate1(m,prog,st) = state2)
        ==>
       (state1 = state2)`;

e (recInduct interpret1_ind);
e (REPEAT CONJ_TAC THEN REPEAT GEN_TAC);
e (SIMP_TAC std_ss [interpret1_def]);