```Regardless of PVS, you cannot define

reduce : [Conj -> (true_free?)]

such that

reduce(True AND True AND True) = True

because, according to your definition, true_free?(True) = FALSE.

idea to overload True and And. Notice, for example, that in your
definition of reduce "reduce?(f1) AND reduce?(f2)" you are using the
constructor "AND" rather than the boolean operator.

Maybe, you want to define something like:

true_free_or_true(f) : bool =
true_free?(f) OR f = True

reduce(f: Conj): recursive (true_free_or_true?)  = CASES f
OF AND(f1, f2): IF reduce?(f1) = True THEN reduce?(f2)
ELSIF reduce?(f2) = True  THEN
reduce?(f1)
ELSE reduce?(f1) AND reduce?(f2)
ENDIF,
ELSE Conj
ENDCASES   MEASURE id BY <<

Cesar

On Wed, 2006-05-24 at 06:00, 许庆国 wrote:
> Hello every one:
>
> I have a smaple theory :
>
> Reduce: THEORY
>
> BEGIN
>   Conj: DATATYPE   BEGIN
>    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)
>    ENDCASES
>   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
>           ENDCASES
>  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?
>
>