Assignment 7

1 files changed, 104 insertions, 0 deletions

diff --git a/assignment7/D.pvs b/assignment7/D.pvs
new file mode 100644
index 0000000..19ff64f
--- /dev/null
+++ b/assignment7/D.pvs
@@ -0,0 +1,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