[pvs] few old files

pvs/socrates-mortal.pvs

@@ -0,0 +1,13 @@
+socrates: THEORY
+BEGIN
+  man: TYPE
+  socrates: man
+  x: VAR man
+  mortal(x): boolean
+
+  menMortal: AXIOM
+    forall x: mortal(x)
+
+  socratesMortal: LEMMA
+    mortal(socrates)
+END socrates

pvs/sum-n.pvs

@@ -0,0 +1,14 @@
+sumn: THEORY
+BEGIN
+  n: VAR nat
+  sum(n): RECURSIVE nat =
+    (IF n = 0 THEN
+       0
+     ELSE
+       n + sum(n-1)
+     ENDIF)
+     MEASURE (λ n: n)
+
+  nnatsum: THEOREM
+    sum(n) = (n * (n+1)) / 2
+END sumn

pvs/sum-n3.pvs

@@ -0,0 +1,25 @@
+sum: THEORY
+BEGIN
+  n: VAR nat
+  f, g: VAR [nat -> nat]
+
+  sum(f, n): RECURSIVE nat =
+    IF n = 0
+      THEN 0
+      ELSE f(n-1) + sum(f, n - 1)
+    ENDIF
+   MEASURE n
+
+  sum_plus: LEMMA
+   sum((lambda n: f(n) + g(n)), n) = sum(f, n) + sum(g, n)
+
+  square(n): nat = n*n
+
+  sum_of_squares: LEMMA
+    6 * sum(square, n+1) = n * (n + 1) * (2*n + 1)
+
+  cube(n): nat = n*n*n
+
+  sum_of_cubes: LEMMA
+    4 * sum(cube, n+1) = n*n*(n+1)*(n+1)
+END sum

pvs/sum-tut.pvs

@@ -0,0 +1,10 @@
+sumtut: THEORY
+  BEGIN
+    n: VAR nat
+
+    sum(n): RECURSIVE nat =
+      (IF n = 0 THEN 0 ELSE n + sum(n-1) ENDIF)
+      MEASURE (LAMBDA n:n)
+ 
+    closed_form: THEOREM sum(n) = n * (n + 1)/2
+  END sumtut