1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
%%% 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
|
