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

[PVS-Help] Typred with grind/ground



I used predicate subtyping to define a type DIGIT.

 DIGIT: TYPE = {i: nat | i = 0 OR i = 1} CONTAINING 0
 a,b,c,z: DIGIT

Then, in the middle of a proof I was given the following sequent, which should have discharged automatically.

[-1]  (a + b + c >= 2)
{-2}  IF a = 1 AND b = 1 THEN 1 = d ELSE 0 = d ENDIF
{-3}  IF b = 1 AND c = 1 THEN 1 = e ELSE 0 = e ENDIF
{-4}  IF c = 1 AND a = 1 THEN 1 = f ELSE 0 = f ENDIF
{-5}  IF d = 1 OR e = 1 THEN 1 = g ELSE 0 = g ENDIF
{-6}  IF g = 1 OR f = 1 THEN 1 = z ELSE 0 = z ENDIF
  |-------
[1]   z = 1

However, without using (typepred a b c), the above would not prove.

In fact, if I had done (typepred a b c) and then (grind) at a higher level, all would have proven automatically. We also could do (typepred a b c)(ground) in the above case. 

Is there some way to say (a) introduce all relevant type predicates whatever they are, and then (2) grind?

(In this case, I knew that I needed a, b and c, but in many cases it is not obvious when ons starts out).

Thanks,

Jonathan