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

Re: Generalizations



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
> > 
> > 
> 
>