# Generalizations

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

```