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

*To*: pvs-help@csl.sri.com*Subject*: Re: Generalizations*From*: Tamarah Arons <tamarah@wisdom.weizmann.ac.il>*Date*: Mon, 4 Feb 2002 15:22:42 +0200 (IST)*Delivery-Date*: Mon Feb 4 05:24:15 2002*In-Reply-To*: <200202031126.g13BQ91k012814@quarter.csl.sri.com>

Hello Sam, I didn't realize that one can import a theory generically. This doesn't solve my problem entirely as I have strategies that call lemma "g_holds", so if I import g_holds generically this call won't work. Still, it gives me another direction in trying to solve the problem. Thanks a lot, Tamarah On Sun, 3 Feb 2002, Sam Owre wrote: > Hi Tamarah, > > I'm not sure if this is what you're looking for, but you can import > gtheory generically, then prove lem1 with the proper instance of > g_holds: > > general[N : posnat, STATE : NONEMPTY_TYPE]: THEORY > ... > importing gtheory > > lem1: lemma > forall d: g(f(d)) > ... > > The proof then goes through with > (SKOSIMP*) > (LEMMA "g_holds[STATE, f(d!1)]") > > Regards, > Sam Owre > > > From: Tamarah Arons <tamarah@wisdom.weizmann.ac.il> > > Subject: Generalizations > > Date: Sun, 03 Feb 2002 12:34:55 +0200 > > To: pvs-help@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 filewith 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 > > > > > >

**References**:**Re: Generalizations***From:*Sam Owre <owre@csl.sri.com>

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