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

*To*: pvs-help@csl.sri.com*Subject*: [PVS-Help] singleton lists*From*: "R. Colvin" <robert@itee.uq.edu.au>*Date*: Thu, 06 May 2004 16:09:02 +1000*List-Help*: <mailto:pvs-help-request@csl.sri.com?subject=help>*List-Id*: PVS-Help <pvs-help.csl.sri.com>*List-Post*: <mailto:pvs-help@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-help-bounces+archive=csl.sri.com@csl.sri.com

Hi, I'm having I'm having trouble working with an antecedent: {-10} cons(c0`next(car(c0`list)), null) = (: empty :) I'd like to simplify this to c0`next(car(c0`list)) = empty ('empty' is a data constructor constant) I can't get PVS to recognise that the LHS of -10 can be simplified down. Is there some property I can use? (I can't figure out exactly what list_rep does in the prelude.) If so, would PVS then work out that equality on singleton lists is equivalent to equality on their elements? Now a couple of related questions: In trying to solve the above problem I proved the lemma: cons_null: THEOREM (forall f, x: (: x :) = cons(x, null)) When I tried introducing this using 'lemma', PVS seemed to automatically simplify it to true, ie, I didn't get any addition to the antecedents by using the lemma rule (with appropriate substitutions). You'll note the inclusion of the unused variable 'f' in the definition of 'cons_null'. Theorems apparently need two variables for the 'lemma' command to work. Is this correct, and if so is there a neater work around? Thanks, Rob

- Prev by Date:
**[PVS-Help] Problem in installation in Linux machine** - Next by Date:
**[PVS-Help] symbol manipulation** - Prev by thread:
**Re: [PVS-Help] symbol manipulation** - Next by thread:
**Re: [PVS-Help] singleton lists** - Index(es):