[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Recursive declarations

    Good evening,

    I am a new user of PVS and I have some questions about the recursive
declarations. First of all, I wonder how the termination TCC is generated
opposite the measure term. For example, at the section 3.7 of your tutorial
with the very simple case of the factorial function, could you explicit the
process of generation? At last, in the same section, you tell that mutual
recursion is not directly possible but we can produce the same effect by means
I don't understand very well in fact. Could you put into practice the two means
you propose with the following example that I give in ML:

    let rec add1 n=
      if n=0 then
    and add2 n=
      if n=0 then

    Many thanks for your answer.

    Best regards.

    David Delahaye.

David Delahaye                                 <Email>: David.Delahaye@inria.fr
<Laboratory>: The Coq Project                                  <Domain>: Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
<Tel>: (33)-(0)1 39 63 57 53
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~delahaye

[If you have time to waste, you can have a look on my proof that all the real
 number are positive. Given x in R:

   x^2>=0                 (well-known result)
   (x^2)^(1/2)>=(0)^(1/2) (use of power on each member)
   x^(2*1/2)>=0           (use of the propertie: (x^n)^m=x^(n*m)
   x^1>=0                 (very easy simplification) 
   x>=0                   (great!)]