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

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