[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] reduce adt
Hello every one:
I have a smaple theory :
Conj: DATATYPE BEGIN
True : TURE?
Hold(b: bool): a?
AND(a1, a2: Data): and?
f: VAR Conj;
|=(f): RECURSIVE bool =
CASES f OF Hold(b): b,
AND(a1, a2): |= (a1) AND |= (a2)
MEASURE id BY <<
true_free?(f): INDUCTIVE bool =
OF AND(f1, f2): true_free?(f1) AND true_free?(f2), True: FALSE
reduce(f: Conj): recursive (true_free?) = CASES f
OF AND(f1, f2): reduce?(f1) AND reduce?(f2), True: ...,
ENDCASES MEASURE id BY <<
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.