Re: [PVS-Help] extend

[Jerome White <jerome@xxxxxxxxxxxxxx>]

I was able to get rid of 'extend' by altering the definittion
unchanged?:

   unchanged?(pre, post: S, K: set[A]): bool =
     FORALL (k: A): member(k, K) IMPLIES
       f(pre, singleton(k)) = f(post, singleton(k))

so, aside from wondering what extend means, I don't think I have a
real understanding of what '(K)' means either. I was under the
impression that the following were equivalent:

  FORALL (k: A): member(k, K) IMPLIES B
  FORALL (k: A | member(k, K): B
  FORALL (k: (K)): B

where 'B' is some boolean.

jerome

On Thu, Aug 27, 2009 at 08:54:32PM -0700, Jerome White wrote:
>I have the following definition:
>
>  S, A, T: TYPE
>  f: FUNCTION[S, set[A] -> T]
>  % ...
>  unchanged?(pre, post: S, K: set[A]): bool =
>    FORALL (k: (K)): f(pre, singleton(k)) = f(post, singleton(k))
>
>When 'unchanged?' is opened in a proof, I get the following:
>
>  [1]   unchanged?(pre!1, post!1, complement(add(t!1, B!1)))
>  Rule? (rewrite "unchanged?")
>  {1}   FORALL (j: (complement(add(t!1, B!1)))):
>	f(pre!1,
>	    extend[A, (complement(add(t!1, B!1))), bool, FALSE]
>		(singleton(j)))
>	   =
>	   f(post!1,
>	     extend[A, (complement(add(t!1, B!1))), bool, FALSE]
>		       (singleton(j)))
>
>What exactly is 'extend'? I see it in the prelude, but am unsure of
>what it means in this context and why it's popping up. Any insight
>would be much appreciated. Thanks
>
>jerome
>