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

```