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

A problem about rule "inst"

Hi all,
   I am a new user of PVS. Recently I met a problem and did not know how to 
solve it, so I put it here, hope someone can help me.

I was trying to prove the following goal:

{-1}    (FORALL (A: Form[dcTV]): |>(([] A) => A))
[-2]    |>([] (Des_1 /\ Des_2 => Triple))
[1]    |>(Des_1 /\ Des_2 => Req)

I wanted to use rule "inst" to instantiate "A" to "(Des_1 /\ Des_2 => 
Triple)", but

Rule? (inst -1 "(Des_1 /\ Des_2 => Req)")
first argument has the wrong type
     Found:  NL_types[dcTV].Form
  Expected: NL_types[dcTV].Term
Restoring the state.

I don't know why PVS expects type "Term" here, since "A" is of type "Form". 
However, if I instantiate "A" to "Des_1" or "Des_2", that is OK! So, to get 
the result I want, I have to write the following line in the .pvs file:

TempVar : VAR FORM = Des_1 /\ Des_2  => Triple ;

and then use 
(then* (inst -1 "TempVar") (expand "TempVar"))

But this is, of course very inconvenient. Can anyone give an alternative 
solution? My PVS version is "PVS Version 2.0 Alpha Plus (patch level 2.376)". 
I will soon update it to 2.1, but I do not think it is a bug of version 2.0.