th_I: THEORY

BEGIN

%%%
%%% Standard development of iterative factorial-with-accumulator.
%%% Start with a "specification" of the factorial function.
%%%

fac(x:nat): RECURSIVE nat = 
  IF x = 0
   THEN 1
   ELSE x * fac(x-1)
  ENDIF
  MEASURE x 

%%%
%%% A few simple facts about the factorial function.
%%%
thm_6_1: THEOREM (FORALL (x:nat): 1 <= fac(x))
thm_6_2: THEOREM (FORALL (x:nat): x <= fac(x))

%%%
%%% In fac1 all recursive calls are in the tail position.
%%% In operational terms, fac1 improves fac because a
%%% no space is needed for a recursion stack.
%%%

tfac(x:nat, y:nat): RECURSIVE nat =
  IF x = 0
   THEN y
   ELSE tfac(x - 1, x * y)
  ENDIF
 MEASURE x


lemma_6_3: LEMMA  (FORALL (m:nat, n:nat): tfac(m, n) = n * tfac(m, 1))

th_6_4: THEOREM  (FORALL (k:nat): fac(k) = tfac(k, 1))

%%%
%%% Standard development ("aha") for iterative fibonacci function
%%%

fib(x:nat): RECURSIVE nat =
  (IF    x = 0 THEN 1
   ELSIF x = 1 THEN 1
               ELSE fib(x - 1) + fib(x - 2)
   ENDIF)
  MEASURE x
%%%
%%% Tail-recursive version of fib.
%%%
tfib(u:nat, v:nat, w:nat): RECURSIVE nat =
  (IF u = 0
    THEN v
    ELSE tfib(u - 1, w, v + w)
    ENDIF)
  MEASURE u

%%%
%%% You will need to discover a nontrivial lemma to prove this.
%%%
thm_6_6: THEOREM
  (FORALL (i:nat):
    tfib(i, 1, 1) = fib(i))

END th_I