Naturels

TYPE nat
  INHERIT number{nat}
  INHERIT total_order{nat}
    -- Generated by {zero, succ}.

  MESSAGE zero -- Literal 0 = zero.
    REPLY(n: nat)

  MESSAGE one -- Literal 1 = one.
    REPLY(n: nat) WHERE n = succ(zero)

  MESSAGE succ(n1: nat)
    -- Literal 2 = succ(1), literal 3 = succ(2), ...
    REPLY(n2: nat)

  MESSAGE pred(n1: nat)
    WHEN n1 > zero REPLY(n2: nat)
      WHERE ALL(n: nat :: pred(succ(n)) = n)
    OTHERWISE REPLY EXCEPTION undefined_pred

  MESSAGE "+"(n1 n2: nat) REPLY(n3: nat)
    WHERE ALL(n m: nat :: n + succ(m) = succ(n + m))

  MESSAGE "-"(n1 n2: nat)
    WHEN n1 >= n2 REPLY(n3: nat)
      WHERE ALL(n: nat :: n - zero = n),
        ALL(n m: nat :: n - succ(m) = pred(n) - m)
    OTHERWISE REPLY EXCEPTION undefined_difference

  MESSAGE "*"(n1 n2: nat) REPLY(n3: nat)
    WHERE ALL(n m: nat :: n * succ(m) = n + (n * m))

  MESSAGE "/"(n1 n2: nat) 
    WHEN n2 ~= zero REPLY(q: nat)
      WHERE SOME(r: nat :: n1 = q * n2 + r & n2 > r)
    OTHERWISE REPLY EXCEPTION divide_by_zero

  MESSAGE "MOD"(n1 n2: nat)
    -- n1 MOD n2 is also written n1 \\ n2.
    WHEN n2 ~= zero REPLY(r: nat)
      WHERE SOME(q: nat :: n1 = q * n2 + r & n2 > r)
    OTHERWISE REPLY EXCEPTION divide_by_zero

  MESSAGE "^"(n1 n2: nat) 
    WHEN n1 ~= 0 | n2 ~= 0 REPLY(n3: nat)
      WHERE ALL(n: nat SUCH THAT n ~= 0 ::
                n ^ 0 = 1 & 0 ^ n = 0 ),
        ALL(n m: nat :: n ^ succ(m) = (n ^ m) * n)
    OTHERWISE REPLY EXCEPTION undefined_expt

  MESSAGE factorial(n1: nat) REPLY(n2: nat)
      WHERE n2 = PRODUCT(k: nat SUCH THAT k <= n1 :: k)

  MESSAGE equal(n1 n2: nat) REPLY(b: boolean)
    -- The properties of equal are determined by
    -- the definition of < and the inherited properties
    -- of equality and total_order.

  MESSAGE "<"(n1 n2: nat) REPLY(b: boolean)
    WHERE ALL(n: nat :: n < succ(n))

  MESSAGE "|"(n1 n2: nat)  -- n1 | n2 means n1 is a factor of n2.
    REPLY(b: boolean)
    WHERE SOME(n: nat :: n * n1 = n2), Partial_ordering("|")

  CONCEPT prime(n: nat)
    VALUE(b: boolean)
    WHERE b <=> n > 1 & ALL(m: nat SUCH THAT m | n ::
                            m = 1 | m = n )
    -- Note overloading: first "|" is "divides",
    -- second "|" is "or".
END