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

Re: Re: [PVS-Help] fixed-point theory



Sam Owre:
    In order to learn fixed-point theory and PVS. I had tried to replay the proving of the theories in http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html in the last year under PVS 5.0. But I encounter some difficulties. For example, I cannot prove the lemmata “continuous_admissible” in theory “continuous” using the pvs scripts provide in “continuous.prf”. I don’t know how to instance the following bounded variable “x”:
[-1]  C!2(x!3)
[-2]  lub?(x!1, C!1)
[-3]  FORALL (d: D): EXISTS (x: R): lub?(x, fset_image(C!1)(d))
[-4]  chain?(C!2)
[-5]  chain?(C!1)
[-6]  FORALL (x: (C!1)):
        FORALL C:
          lub_exists?(set_image(x)(C)) & (x(lub(C)) = lub(set_image(x)(C)))
  |-------
[1]   EXISTS (x:
                ({M: Lub_Exists[R, le_R] |
                    EXISTS (f: (C!1)): M = set_image[D, R](f)(C!2)})):
        lub(fset_image(C!1)(x!3)) = lub[R, le_R](x)
this is an sub-goal of the formula “continuous_admissible: LEMMA admissible?[[D -> R], pointwise.<=](continuous?)” 
can you help me. Thanks in advance.

Cheers
Qingguo XU
------------------  
2012-06-10
-------------------------------------------------------------
发件人:Sam Owre
发送日期:2012-06-05 09:32:17
收件人:stan.rosenberg
抄送:pvs-help
主题:Re: [PVS-Help] fixed-point theory
Hi Stan,
I happen to have a copy of it, I'm including it below.
Cheers,
Sam
Stan Rosenberg <stan.rosenberg@xxxxxxxxx> wrote:
> Hi,
> 
> I came across this formalization of fixed-points:
> http://www.informatik.uni-ulm.de/ki/PVS/fixpoints.html
> Unfortunately, the link to the dump file is broken.  Does anyone
> happen to know of a mirror or an alternative library?
> 
> Thanks,
> 
> stan