%%%
%%% 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 number ON 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_F: THEORY
 BEGIN

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

%%%
%%% Defining recursive functions
%%%
  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.
%%%     ~~~~~~~~~~~~

F_1: THEOREM sum(n) = (n * (n + 1))/2

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

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

END th_F

%%%
%%% pvs-files can contain more than one theory.
%%% Theories can include other theories.
%%%
th_Fa : THEORY

  BEGIN

  importing th_F

  n : var nat

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

%%%
%%% As in Scheme, LAMBDA is used to express functions without giving them names.
%%%

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

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

Fa_2: PROPOSITION  sum(n,square) = (n*(n+1)*(2*n+1))/6
  
Fa_3: PROPOSITION  sum(n,cube) = square(sum(n))

  exp2(n:nat) : RECURSIVE posnat = 
    IF n = 0 THEN 1 ELSE 2*exp2(n-1) ENDIF
  measure n

Fa_4: PROPOSITION  sum(n,exp2) = exp2(n+1) - 1

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

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

END th_Fa