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

Re: Generalizations



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