%%%    NAME/LOGIN-ID    Camil Staps / s4498062_
%%%    ACKNOWLEDGMENTS:

%%%
%%% INDUCTION
%%% These examples of induction can be proven using the arithmetic decision procedures
%%% (ASSERT).  You will need to EXPAND definitions selectively: (EXPAND "name" FN ON ...)
%%% expands Occurance N of the function "name" in formula number FN (see the help listing
%%% for more information.
%%%
%%% It is highly recommended that you prove the results by hand before trying to explain
%%% them to PVS.  However, most of the proofs yield to a systematic application of induction.
%%%

th_D: THEORY
 BEGIN

  n: VAR nat
  f: VAR [nat->nat]

%%%
%%% Defining recursive functions.  Here is the form of a recursive function definition
%%% over the natural numbers.  The MEASURE clause is used to prove well-definedness.
%%% We will discuss this later on.
%%%

  sum(n): RECURSIVE nat =
   IF n = 0 THEN 0 ELSE n + sum(n - 1) ENDIF
   MEASURE n

%%%
%%% Use (INDUCT "n") to start the proof of Theorem F_1.
%%%     ~~~~~~~~~~~~

D_1: THEOREM 2 * sum(n) = (n * (n + 1))

%%%
%%% Higher order parameters.  Here is a slightly more general version of "summation"
%%%

  sum(n,f) : RECURSIVE nat =
   IF n = 0 THEN f(0) ELSE f(n) + sum(n - 1,f) ENDIF
   MEASURE n

D_2: THEOREM 2 * sum(n,id) = (n*(n+1))

  pow(a, n: nat) : RECURSIVE nat =
     IF n=0
     THEN 1
     ELSE a * pow(a, n-1)
     ENDIF
  MEASURE n

END th_D

%%%
%%% PVS source files can contain more than one theory.
%%% Theories can include other theories.
%%%

th_Da : THEORY

  BEGIN

  importing th_D   % Use THEORY D

  n : var nat
  i : var nat
  f : var [nat -> nat]

  square(n:nat) : nat = n*n
  cube(n:nat) : nat = n*n*n

%%%
%%% As in Scheme, LAMBDA is used to express functions without giving them names.
%%% WARNING: at least one of these requires insightful thinking.
%%% HINT:    If you get stuck, try EXPAND
%%%

Da_1: PROPOSITION  sum(n, (LAMBDA (n:nat): 2 * n + 1)) = square(n + 1)

Da_2: PROPOSITION  6 * sum(n,square) = (n*(n+1)*(2*n+1))
  
Da_3: PROPOSITION  sum(n,cube) = square(sum(n))

Da_4: PROPOSITION  sum(n,LAMBDA (n:nat) : pow(2,n)) = pow(2,n+1) - 1

Da_5: LEMMA i * sum(n, f) = sum(n, (LAMBDA (n : nat) : i * f(n)))

END th_Da

th_Db : THEORY
BEGIN
  importing th_D

  geom(a: nat, n:nat) : RECURSIVE nat =
    IF n = 0
    THEN 0
    ELSE pow(a, n-1) + geom(a, n-1)
    ENDIF
  MEASURE n

  geom_sum : THEOREM FORALL(a,n:nat): a > 1 IMPLIES (a-1) * geom(a,n) = pow(a, n)-1
END th_Db