** 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 gcd : 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 gcd
  eq gcd(0,X) = X .                                ** base case
  ** gcd(0,5) = X
  ceq gcd(X,Y) = gcd( Y , X ) if X < Y .           ** recursive case 1
  ** gcd(3,5) = gcd(5,3)
  ceq gcd(X,Y) = gcd( X - Y , Y ) if not X < Y .   ** recursive case 2
  ** gcd(5,3) = gcd(2,3)
}

** End of question 1

** Question 2

module FACT {
  protecting (RAT)

** Define the signatures of the operations of the FACT module
    op _! : Nat -> NzNat

** Define the meanings of the operations
  var N : Nat    ** using this variable

  ** Define !
  eq 0 ! = 1 .                        ** base case
  ceq N ! = N * (N - 1 !) if N > 0 .   ** recursive case
}

** run through CafeOBJ to generate a trace of the reduction
    open FACT .
      set trace whole on
      reduce s(0)! .
      set trace whole off
    close