%% PVS Version 3.2
%% 6.2 [Linux (x86)] (Nov 3, 2004 23:30)
$$$PVSHOME/.pvs.lisp

$$$PVSHOME/.pvs.lisp

$$$trans1.pvs
transclosure[T: TYPE]: THEORY
% Wim H. Hesselink, 25 april 2002
% latest modification 27 August 2008

 BEGIN

  relation: TYPE = pred[[T, T]] % predicates and subsets are the same!

  R, S: VAR relation
  x, y: VAR T

% Kleene's star operation:
  star(R: relation): relation =
      {(x, y) |
         (EXISTS (f: [nat -> T], n: nat):
            f(0) = x AND
            f(n) = y AND
            (FORALL (i: nat): i < n IMPLIES R(f(i), f(i + 1))))}

% PVS' prelude contains definitions of reflexive?, symmetric? and transitive?.
% As an example, we have proved reflexivity for you.

  star_reflexive: LEMMA 
     reflexive?(star(R))

  star_implied: LEMMA 
     R(x,y) IMPLIES star(R)(x,y)

  star_preserves_symmetry: LEMMA 
     symmetric?(R) IMPLIES symmetric?(star(R))

  star_transitive: LEMMA 
     transitive?(star(R))

% State and prove the assertion that every reflexive and transitive 
% relation S that contains R, also contains star(R).
% Advice: use the definition of "subset?" from the prelude.

 END transclosure

$$$trans1.prf
(transclosure (star_reflexive 0
               (star_reflexive-1 nil 3378551187 3378551289
                ("" (expand "reflexive?")
                 (("" (skosimp*)
                   (("" (expand "star")
                     (("" (inst + "lambda (i:nat): x!1" "0")
                       (("" (skosimp) (("" (assert) nil nil)) nil))
                       nil))
                     nil))
                   nil))
                 nil)
                proved
                ((number nonempty-type-decl nil numbers nil)
                 (boolean nonempty-type-decl nil booleans nil)
                 (number_field_pred const-decl "[number -> boolean]"
                  number_fields nil)
                 (number_field nonempty-type-from-decl nil
                  number_fields nil)
                 (real_pred const-decl "[number_field -> boolean]"
                            reals nil)
                 (real nonempty-type-from-decl nil reals nil)
                 (rational_pred const-decl "[real -> boolean]"
                                rationals nil)
                 (rational nonempty-type-from-decl nil rationals nil)
                 (integer_pred const-decl "[rational -> boolean]"
                               integers nil)
                 (int nonempty-type-eq-decl nil integers nil)
                 (bool nonempty-type-eq-decl nil booleans nil)
                 (>= const-decl "bool" reals nil)
                 (nat nonempty-type-eq-decl nil naturalnumbers nil)
                 (T formal-type-decl nil transclosure nil)
                 (star const-decl "relation" transclosure nil)
                 (reflexive? const-decl "bool" relations nil))
                102079 780 t shostak)))