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

[PVS-Help] reduce adt

Hello every one:

I have a smaple theory :

Reduce: THEORY

   True : TURE?
    Hold(b: bool): a?
    AND(a1, a2: Data): and?
END Conj

  f: VAR Conj;

  |=(f): RECURSIVE bool =
   CASES f OF Hold(b): b, 
        True: true,
        AND(a1, a2):  |= (a1) AND |= (a2) 
  MEASURE id BY <<

  true_free?(f):  INDUCTIVE bool =
        CASES f
          OF AND(f1, f2): true_free?(f1) AND true_free?(f2), True: FALSE
          ELSE TRUE
 reduce(f: Conj): recursive (true_free?)  = CASES f
          OF AND(f1, f2): reduce?(f1) AND reduce?(f2), True: ...,
             ELSE TRUE
        ENDCASES   MEASURE id BY <<

 END Reduce

   I want to reduce an arbitrary  fomula of datatype "Conj" to compact form:
i.e., for instance,

   "b1 AND True AND (True AND True)"  -->  b1,  %where  b1 is the form of Hold(b) for some b.
    "True AND True AND True"  ---> True

   Is it possible to implement this process using a recursive fucntion in PVS? I cannot know how to deal with True.

Can you give me some hints?

thank you in advance.

Q.G .XU.