Thanks Sam. That works.
(then (expand* formula1 formula2 ...) (alltypepreds) (grind))
One has to first expand formulas until the relevant expressions to which typepred is applied appear, and then one can apply alltypepreds.
Jonathan
Hi Jonathan, Look into alltypepreds  it should do what you want. Regards, Sam Owre Jonathan Ostroff < jonathan@xxxxxxxx> wrote: 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
