next weeks lab is experiment, arrive 10 minutes early *please*
bring calculators

writing re-write rules

recursive defn of nat, needs recursive rewrite rules
recursive: 
	defined in terms of itself (a natural number is a successor of a
natural number)
	plus a base case (zero is a natural number - zero is not a successor of
a natural number)

every rewrite should bring you closer to the base case, until eventually the
base case allows you to take out the operator.

eg Natural _+_

base case X + 0 = X (and 0 + X = X) (gets rid of the operator +)
recursive case (difficult rewriting rule):

X + Y = something more like X + 0, without changing the semantics (meaning)

well, if we subtract 1 from Y and add it to the whole term, the whole term is
still a Nat (recursive defn) and Y is closer to 0. If we apply this rewrite
rule repeatedly (recursively) we'll eventually get to the base case, and be
able to get rid of the + operator

   X + Y = (X + (Y - 1)) + 1
(this statement is true)

You can't use +1 and -1 in CafeOBJ, you can only use the fact that Nats are
defined recursively, we can change the above to 

   X + Y = s(X + (Y - 1))

but we still have to get rid of the Y - 1
change it to 
(write right hand side first)
  
   X + (Z + 1) = s(X + Z)

Then we can say

   X + s(Z) = s(X + Z) 


Let's follow the same steps for the pseudo-minus that's necessary for GCD

pseudo-minus - we can arrange it so that it's never used with a smaller Nat on
the left and a bigger nat on the right (which would give a negative number), so
we only deal with the possibility that the result is zero or positive.

base case (get rid of the - operator) (Pause, and let them answer)
   X - 0 = X

recursive case
what would get us closer to the base case? (pause)

   X - Y = (X - 1) - (Y - 1)

   (long pause here)
   (right hand side first) 

   (P + 1) - (Q + 1) = P - Q
   s(P) - s(Q) = P - Q

what about < ?
	signature
	op _<_ : Nat Nat -> Bool

base case(s)
	0 < M = true
	M < 0 = false

recursive case (get closer to base case)
	M < N = (M - 1) < (N - 1)
	(X + 1) < (Y + 1) = X < Y
	s(X) < s(Y) = X < Y


steps:
	find a base case which gets rid of the operator
	find a recursive case which gets closer to the base case

multiplication - example of confluence

base case: X * 0 = 0
recursive case X * Y = (X * (Y - 1)) + X
	must add + X to preserve *semantics*
	seems to be getting bigger, but we know we can reduce '+' back
	

GCD


GCD(N, M)
    if N < M
        GCD(M, N)
    otherwise
        GCD(N - M, M)

if statements work slightly differently, the condition is checked after the
pattern is matched


module SIMPLE-NAT+ {
	protecting (SIMPLE-NAT)
	op _-_ : Nat Nat -> Nat
	op _<_ : Nat Nat -> Bool
	-- ---------------------
	vars N M : Nat
	eq 0 - M = 0 .
	eq N - 0 = N .

	eq s(N) - s(M) = N - M .
	eq 0 < s(N) = true .
	eq N < 0 = false .
	eq s(N) < s(M) = N < M .
}

module GCD {
	protecting (SIMPLE-NAT+)
	op gcd : Nat Nat -> Nat
	-- --------------------
	vars N M : Nat
	ceq gcd(N, M) = gcd(M, N) if N < M .
	eq gcd(N, 0) = N .
	ceq gcd(s(N), s(M)) = gcd(s(N) - s(M), s(M)) if not (N < M) .
}