mod! PNAT {
  [Zero NzNat < Nat < ErrorNat]
  op 0 : -> Zero
  op s : Nat -> NzNat
  -- For verification
  op errorNat : -> ErrorNat 
  op _=_ : ErrorNat ErrorNat -> Bool {comm}
  op _<_ : ErrorNat ErrorNat -> Bool
  op _+_ : Nat Nat -> Nat
  op _+_ : ErrorNat ErrorNat -> ErrorNat
  op _*_ : Nat Nat -> Nat
  op _*_ : ErrorNat ErrorNat -> ErrorNat
  op sd : Nat Nat -> Nat
  op sd : ErrorNat ErrorNat -> ErrorNat
  op _quo_ : Nat Zero -> ErrorNat
  op _quo_ : Nat NzNat -> Nat
  op _quo_ : ErrorNat ErrorNat -> ErrorNat
  --
  vars M N : Nat
  -- _=_
  eq (N = N) = true .
  eq (0 = s(N)) = false .
  eq (s(M) = s(N)) = (M = N) .
  --
  eq (errorNat = N) = false .
  eq (N = errorNat) = false .
  eq (errorNat = errorNat) = true .
  -- _<_
  eq 0 < 0 = false .
  eq 0 < s(N) = true .
  eq s(M) < 0 = false .
  eq s(M) < s(N) = M < N .
  --
  eq M < errorNat = false .
  eq errorNat < N = false .
  eq errorNat < errorNat = false .
  -- _+_
  eq 0 + N = N .
  eq s(M) + N = s(M + N) .
  --
  eq M + errorNat = errorNat .
  eq errorNat + N = errorNat .
  eq errorNat + errorNat = errorNat .
  -- _*_
  eq 0 * N = 0 .
  eq s(M) * N = N + (M * N) .
  --
  eq M * errorNat = errorNat .
  eq errorNat * N = errorNat .
  eq errorNat * errorNat = errorNat .
  -- sd
  eq sd(0,N) = N .
  eq sd(s(M),0) = s(M) .
  eq sd(s(M),s(N)) = sd(M,N) .
  --
  eq sd(M,errorNat) = errorNat .
  eq sd(errorNat,N) = errorNat .
  eq sd(errorNat,errorNat) = errorNat .
  -- quo
  eq M quo 0 = errorNat .
  eq M quo s(N) = (if M < s(N) then 0 else s(sd(M,s(N)) quo s(N)) fi) .
  --
  eq M quo errorNat = errorNat .
  eq errorNat quo N = errorNat .
  eq errorNat quo errorNat = errorNat .
}

mod! EXP {
  pr(PNAT)
  [Nat < Exp]
  op _++_ : Exp Exp -> Exp {l-assoc prec: 30}
  op _--_ : Exp Exp -> Exp {l-assoc prec: 30}
  op _**_ : Exp Exp -> Exp {l-assoc prec: 29}
  op _//_ : Exp Exp -> Exp {l-assoc prec: 29}
}

mod! INTERPRETER {
  pr(EXP)
  op interpret : Exp -> ErrorNat
  var N : Nat
  vars E E1 E2 : Exp
  eq interpret(N) = N .
  eq interpret(E1 ++ E2) = interpret(E1) + interpret(E2) .
  eq interpret(E1 -- E2) = sd(interpret(E1),interpret(E2)) .
  eq interpret(E1 ** E2) = interpret(E1) * interpret(E2) .
  eq interpret(E1 // E2) = interpret(E1) quo interpret(E2) .
}

--
-- red in INTERPRETER : interpret(s(s(0)) ++ s(s(0)) ** s(s(0))) .
-- red in INTERPRETER : interpret(0 // 0) .
-- red in INTERPRETER : interpret(0 // 0 ++ 0) .
--

mod! COMMAND {
  pr(PNAT)
  [Command]
  op push : Nat -> Command
  op multiply : -> Command
  op divide : -> Command
  op add : -> Command
  op minus : -> Command
}

mod! LIST (M :: TRIV) {
  [List]
  op nil : -> List
  op _|_ : Elt.M List -> List
  op _@_ : List List -> List {assoc}
  var E : Elt.M
  vars L1 L2 : List
  eq nil @ L2 = L2 .
  eq (E | L1) @ L2 = E | (L1 @ L2) .
  eq L1 @ nil = L1 .
}

view TRIV2COMMAND from TRIV to COMMAND {
  sort Elt -> Command
}

mod! CLIST {
  pr(LIST(TRIV2COMMAND) * {sort List -> CList})
}

view TRIV2PNAT from TRIV to PNAT {
  sort Elt -> ErrorNat
}

mod! VM {
  pr(CLIST)
  pr(LIST(TRIV2PNAT) * {sort List -> Stack, op nil -> empstk})
  op vm : CList -> ErrorNat
  op exec : CList Stack -> ErrorNat
  var CL : CList
  var PC : Nat
  var Stk : Stack
  vars N N1 N2 : Nat
  vars EN EN1 EN2 : ErrorNat
  eq vm(CL) = exec(CL,empstk) .
  eq exec(nil,empstk) = errorNat .
  eq exec(nil,N | empstk) = N .
  eq exec(nil,N | N1 | Stk) = errorNat .
  eq exec(push(N) | CL,Stk) = exec(CL,N | Stk) .
  eq exec(add | CL,empstk) = errorNat .
  eq exec(add | CL,N | empstk) = errorNat .
  eq exec(add | CL,N2 | N1 | Stk) = exec(CL,N1 + N2 | Stk) .
  eq exec(multiply | CL,empstk) = errorNat .
  eq exec(multiply | CL,N | empstk) = errorNat .
  eq exec(multiply | CL,N2 | N1 | Stk) = exec(CL,N1 * N2 | Stk) .
  eq exec(divide | CL,empstk) = errorNat .
  eq exec(divide | CL,N | empstk) = errorNat .
  eq exec(divide | CL,N2 | N1 | Stk) = exec(CL,N1 quo N2 | Stk) .
  eq exec(minus | CL,empstk) = errorNat .
  eq exec(minus | CL,N | empstk) = errorNat .
  eq exec(minus | CL,N2 | N1 | Stk) = exec(CL,sd(N1,N2) | Stk) .
  eq exec(CL,errorNat | Stk) = errorNat .
  eq exec(CL,N | errorNat | Stk) = errorNat .
}

mod! COMPILER {
  pr(EXP)
  pr(CLIST)
  op compile : Exp -> CList
  var N : Nat
  vars E E1 E2 : Exp
  eq compile(N) = push(N) | nil .
  eq compile(E1 ++ E2) = compile(E1) @ compile(E2) @ (add | nil) .
  eq compile(E1 -- E2) = compile(E1) @ compile(E2) @ (minus | nil) .
  eq compile(E1 ** E2) = compile(E1) @ compile(E2) @ (multiply | nil) .
  eq compile(E1 // E2) = compile(E1) @ compile(E2) @ (divide | nil) .
}

--
-- open COMPILER + VM
--   red compile(s(s(0)) ++ s(s(0)) ** s(s(0))) .
--   red compile(0 // 0) .
--   red compile(0 // 0 ++ 0) .
--   red vm(compile(s(s(0)) ++ s(s(0)) ** s(s(0)))) .
--   red vm(compile(0 // 0)) .
--   red vm(compile(0 // 0 ++ 0)) .
-- close
--

mod THEOREM-COMPILER {
  pr(INTERPRETER)
  pr(VM)
  pr(COMPILER)
-- arbitrary values  
  ops e e1 e2 : -> Exp
  ops n n1 m : -> Nat
  op nz : -> NzNat
  op l : -> CList
  ops s s1 : -> Stack
-- names of theorems
  op th1 : Exp Nat -> Bool
  op th2 : Exp CList Stack Nat -> Bool
-- CafeOBJ variables
  var E : Exp
  var N : Nat
  var L : CList 
  var S : Stack 
-- theorems
  eq th1(E,N) = (interpret(E) = N implies vm(compile(E)) = N) .
  eq th2(E,L,S,N) = (exec(L,interpret(E) | S) = N
                     implies exec(compile(E) @ L,S) = N) .
}

--
-- Theorem \forall E:Exp,N:Nat.(interpret(E) = N implies vm(compile(E)) = N)
-- Proof. By induction on E.
-- Let e be an arbitrary expression.
-- I. Base case
open THEOREM-COMPILER
-- check
  red th1(m,n) .
close
-- II. Induction case
-- 1. e1 ++ e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 ++ e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 ++ e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th1(e1 ++ e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (k1 + k2 = n) = false .
-- check
  red th1(e1 ++ e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq k1 + k2 = n .
  eq exec((compile(e2) @ (add | nil)),(k1 | empstk)) = n .
-- check
  red th2(e1,compile(e2) @ (add | nil),empstk,n) implies th1(e1 ++ e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq k1 + k2 = n .
  eq (exec((compile(e2) @ (add | nil)),(k1 | empstk)) = n) = false .
-- check
  red th2(e2,add | nil,k1 | empstk,n) implies th1(e1 ++ e2,n) .
close
-- 2. e1 -- e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 -- e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 -- e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th1(e1 -- e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (sd(k1,k2) = n) = false .
-- check
  red th1(e1 -- e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq sd(k1,k2) = n .
  eq exec((compile(e2) @ (minus | nil)),(k1 | empstk)) = n .
-- check
  red th2(e1,compile(e2) @ (minus | nil),empstk,n) implies th1(e1 -- e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq sd(k1,k2) = n .
  eq (exec((compile(e2) @ (minus | nil)),(k1 | empstk)) = n) = false .
-- check
  red th2(e2,minus | nil,k1 | empstk,n) implies th1(e1 -- e2,n) .
close
-- 3. e1 ** e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 ** e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 ** e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th1(e1 ** e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (k1 * k2 = n) = false .
-- check
  red th1(e1 ** e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq k1 * k2 = n .
  eq exec((compile(e2) @ (multiply | nil)),(k1 | empstk)) = n .
-- check
  red th2(e1,compile(e2) @ (multiply | nil),empstk,n) implies th1(e1 ** e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq k1 * k2 = n .
  eq (exec((compile(e2) @ (multiply | nil)),(k1 | empstk)) = n) = false .
-- check
  red th2(e2,multiply | nil,k1 | empstk,n) implies th1(e1 ** e2,n) .
close
-- 4. e1 // e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 // e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th1(e1 // e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th1(e1 // e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (k1 quo k2 = n) = false .
-- check
  red th1(e1 // e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq k1 quo k2 = n .
  eq exec((compile(e2) @ (divide | nil)),(k1 | empstk)) = n .
-- check
  red th2(e1,compile(e2) @ (divide | nil),empstk,n) implies th1(e1 // e2,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq k1 quo k2 = n .
  eq (exec((compile(e2) @ (divide | nil)),(k1 | empstk)) = n) = false .
-- check
  red th2(e2,divide | nil,k1 | empstk,n) implies th1(e1 // e2,n) .
close
--
-- QED
--


--
-- Theorem \forall E:Exp,L:CList,S:Stack,N:Nat.
--         (exec(L,interpret(E) | S) = N implies exec(compile(E) @ L,S) = N) .
-- Proof. By induction on E.
-- Let e be an arbitrary expression.
-- I. Base case
open THEOREM-COMPILER
-- check
  red th2(m,l,s,n) .
close
-- II. Induction case
-- 1. e1 ++ e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 ++ e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 ++ e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th2(e1 ++ e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (exec(l,(k1 + k2) | s) = n) = false .
-- check
  red th2(e1 ++ e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,(k1 + k2) | s) = n .
  eq exec(compile(e2) @ (add | l),k1 | s) = n .
-- check
  red th2(e1,compile(e2) @ (add | l),s,n) implies th2(e1 ++ e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,(k1 + k2) | s) = n .
  eq (exec(compile(e2) @ (add | l),k1 | s) = n) = false .
-- check
  red th2(e2,add | l,k1 | s,n) implies th2(e1 ++ e2,l,s,n) .
close
-- 2. e1 -- e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 -- e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 -- e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th2(e1 -- e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (exec(l,sd(k1,k2) | s) = n) = false .
-- check
  red th2(e1 -- e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,sd(k1,k2) | s) = n .
  eq exec(compile(e2) @ (minus | l),k1 | s) = n .
-- check
  red th2(e1,compile(e2) @ (minus | l),s,n) implies th2(e1 -- e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,sd(k1,k2) | s) = n .
  eq (exec(compile(e2) @ (minus | l),k1 | s) = n) = false .
-- check
  red th2(e2,minus | l,k1 | s,n) implies th2(e1 -- e2,l,s,n) .
close
-- 3. e1 ** e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 ** e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 ** e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th2(e1 ** e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (exec(l,(k1 * k2) | s) = n) = false .
-- check
  red th2(e1 ** e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,(k1 * k2) | s) = n .
  eq exec(compile(e2) @ (multiply | l),k1 | s) = n .
-- check
  red th2(e1,compile(e2) @ (multiply | l),s,n) implies th2(e1 ** e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,(k1 * k2) | s) = n .
  eq (exec(compile(e2) @ (multiply | l),k1 | s) = n) = false .
-- check
  red th2(e2,multiply | l,k1 | s,n) implies th2(e1 ** e2,l,s,n) .
close
-- 4. e1 // e2
open THEOREM-COMPILER
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 // e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = errorNat .
-- check
  red th2(e1 // e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = errorNat .
  eq interpret(e2) = k2 .
-- check
  red th2(e1 // e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq (exec(l,(k1 quo k2) | s) = n) = false .
-- check
  red th2(e1 // e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,(k1 quo k2) | s) = n .
  eq exec(compile(e2) @ (divide | l),k1 | s) = n .
-- check
  red th2(e1,compile(e2) @ (divide | l),s,n) implies th2(e1 // e2,l,s,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  ops k1 k2 : -> Nat .
-- assumptions
  eq interpret(e1) = k1 .
  eq interpret(e2) = k2 .
  eq exec(l,(k1 quo k2) | s) = n .
  eq (exec(compile(e2) @ (divide | l),k1 | s) = n) = false .
-- check
  red th2(e2,divide | l,k1 | s,n) implies th2(e1 // e2,l,s,n) .
close
--
-- QED
--

--
-- Theorem \forall E:Exp,N:Nat.(interpret(E) = N implies vm(compile(E)) = N)
-- (Another) Proof. By case analysis.
open THEOREM-COMPILER
-- assumptions
  eq interpret(e) = errorNat .
-- check
  red th2(e,nil,empstk,n) implies th1(e,n) .
close
open THEOREM-COMPILER
-- arbitrary values
  op k : -> Nat .
-- assumptions
  eq interpret(e) = k .
-- check
  red th2(e,nil,empstk,n) implies th1(e,n) .
close
--
-- QED
--