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

*To*: pvs-help@csl.sri.com*Subject*: Generalizations*From*: Tamarah Arons <tamarah@wisdom.weizmann.ac.il>*Date*: Sun, 3 Feb 2002 12:34:55 +0200 (IST)*Sender*: pvs-help-owner@csl.sri.com

Hello, I would like to prove a property for a non-specified element of a domain and then "generalize" it to all elements of the domain. i.e. if I have f : [domainN -> STATE] z : domainN and I can prove g(f(z)) I would like to generalize to forall (d: domainN): g(f(d)). Since z is totally non-specified, I believe that this is logically sound. However, I have been unable to do this. My motivation is that I have separate theories that prove g(state) but must be given the STATE variable as parameter when they are imported. This makes it impossible to use them to prove forall (d: domainN): g(f(d)). I have included a dump file with a distilled, simplified version of what I would like to do. The dump theories are really futile, but I think that they illustrate what I want to do. Any suggestions? Thanks, Tamarah _________________________________________________________________________ $$$general.pvs general[N : posnat, STATE : NONEMPTY_TYPE]: THEORY BEGIN domainN : TYPE = upto[N] f : [domainN -> STATE] z : domainN d : VAR domainN importing g[STATE] % lem1 cannot be proved lem1 : lemma forall d : g(f(d)) importing gtheory[STATE, f(z)] % lem2 can be proved lem2 : lemma g(f(z)) % I would like to generalize from g(f(z)) to forall d : g(f(d)) END general $$$general.prf (|general| (|lem1| "" (SKOSIMP*) (("" (POSTPONE) NIL NIL)) NIL) (|lem2| "" (LEMMA "g_holds") (("" (PROPAX) NIL NIL)) NIL)) $$$gtheory.pvs gtheory[STATE : NONEMPTY_TYPE, st : STATE] : theory begin importing g[STATE] % In reality, this is a complicated lemma g_holds: axiom g(st) end gtheory $$$g.pvs g[STATE : NONEMPTY_TYPE]: theory begin % In reality, this would be an "interesting", defined function. g : [STATE -> bool] end g

- Prev by Date:
**Re: really basic question** - Next by Date:
**Re: Generalizations** - Prev by thread:
**Re: [LET .. IN ..]** - Next by thread:
**Re: Generalizations** - Index(es):