** Sample solution to SE304 Lab 5
** Author: Gareth Carter

module SIMPLE-NAT {

  [Zero NzNat < Nat]

** Define the signatures of the operations of the SIMPLE-NAT module
  op 0 : -> Zero
  op s : Nat -> Nat
  op _+_ : Nat Nat -> Nat
  op _-_ : Nat Nat -> Nat
  op _<_ : Nat Nat -> Bool
  op _*_ : Nat Nat -> Nat {assoc comm} ** id: 1
  op _%_ : Nat Nat -> Nat

** Define the meanings of the operations
  vars X, Y : Nat    ** using these variables

  ** Definition of +
  eq 0 + X = X .                     ** base case
  ** 0 + 6 = 6
  eq s(X) + Y = s(X + Y) .           ** recursive case
  ** s(4) + 5 = s(4 + 5)

  ** Definition of -
  eq 0 - X = X .                     ** base case 1
  ** 0 - 3 = 3 (pseudo minus)
  eq X - 0 = X .                     ** base case 2
  ** 3 - 0 = 3
  eq s(X) - s(Y) = X - Y .           ** recurssive case
  ** s(5) - s(2) = 5 - 2

  ** Definition of <
  eq 0 < s(X) = true .               ** base case 1
  ** 0 < s(0) = true
  eq s(X) < 0 = false .              ** base case 2
  ** s(0) < 0 = false
  eq s(X) < s(Y) = X < Y .           ** recursive case
  ** s(4) < s(2) = 4 < 2 (ultimately false)

  ** Definition of *
  eq 0 * X = 0 .                     ** base case
  ** 0 * 5 = 0
  eq s(X) * Y = Y + (X * Y) .        ** recusive case
  ** s(3) * 5 = 5 + (3 * 5)

  ** Definition of %
  ceq X % Y = 0 if X == Y .             ** base case 1
  ** 5 % 5 = 0
  ceq X % Y = X if X < Y .              ** base case 2
  ** 5 % 8 = 5
  ceq X % Y = ( X - Y ) % Y if Y < X .  ** recursive case
  ** 15 % 6 = 9 % 6

}

open SIMPLE-NAT .
  ops a,b,c : -> Nat .
  set trace whole on .
  --> Base case
  red 0 + 0 == 0 .
  --> Inductive hypothesis
  eq a + 0 = a .
  --> Conclusion - should reduce to true
  red s(a) + 0 == s(a) .
  -->
  -->
  -->
  --> Proof of Associativity
  --> Base case
  red (0 + a) + b == 0 + (a + b) .
  --> Inductive hypothesis
  eq (a + b) + c = a + (b + c) .
  --> Conclusion - should reduce to true
  red (s(a) + b) + c == s(a) + (b + c) .
  set trace whole off .

close

module STACK {

  protecting(SIMPLE-NAT)
  [Stack]

** Define the signatures of the operations in the STACK Module
  op empty : -> Stack
  op top : Stack -> Nat
  op push : Nat Stack -> Stack
  op pop : Stack -> Stack

** Define the meanings of the operations
  var X : Nat    ** using these variables
  var S : Stack

  eq top(push(X,S)) = X .
  ** The element at the top of a stack is the last element pushed on it
  ** top(push(5,(push(4,push(3,empty))))) = 5 .
  eq pop(push(X,S)) = S .
  ** Popping an element off a stack is the stack with the last pushed element removed
  ** pop(push(5,(push(4,push(3,empty))))) = push(4,push(3,empty)) .
}