Re: [PVS-Help] Min value in a set

[Jerome <jerome@xxxxxxxxxxxxxx>]

I'm having trouble expanding 'min' (over a set) within my proof. To
illustrate, take the following theory:

  local: THEORY BEGIN
    natarray: TYPE = [posnat -> nat]
    indices:  TYPE = finite_set[posnat]

    min_constant: LEMMA FORALL (J, K: indices): min(J) = min(K)
  END local

When trying to prove 'min_constant', after skolemizing, I'd like to
expand 'min', but I can't:

  {1}   min(J!1) = min(K!1)

  Rule? (expand "min")
  No change on: (EXPAND "min")
  min_constant :

    |-------
  {1}   min(J!1) = min(K!1)


Why can't I perform the expansion? Even if I explicitly import
'finite_sets@finite_sets_minmax' in my theory, I get the same results.

jerome

On Wed, Mar 12, 2008 at 07:09:32AM -0500, Butler, Ricky W. (LARC-D320) wrote:
>Jerome,
>   It distinguishes between them on the basis of the number of
>arguments.  Since both are in prelude, no IMPORTING statements are
>needed.
>
>Note. See theory "finite_sets_minmax" in the "finite_sets" library for 
>a more general min/max over sets.
>      This can be located in the lib subdirectory of your installation
>directory.  It is imported as follows
>
>       IMPORTING finite_sets@finite_sets_minmax
>
>The NASA libraries provide min and max over sets over a bounded domain.
>
>       IMPORTING reals@bounded_reals
>
>See http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
>for information about how to install these.
>
>Rick
>
>> -----Original Message-----
>> From: pvs-help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx
>[mailto:pvs-
>> help-bounces+r.w.butler=larc.nasa.gov@xxxxxxxxxxx] On Behalf Of Jerome
>> Sent: Tuesday, March 11, 2008 8:03 PM
>> To: pvs-help@xxxxxxxxxxx
>> Subject: [PVS-Help] Min value in a set
>> 
>> I would like to use both 'min' operations in the prelude: min over a
>> set and min of two values - how do I do it? In the former, I think the
>> min found in 'min_nat' would do the trick, but I'm not sure how to
>> access it. PVS always seems to think I want the min within 'real_defs'
>> (which I do, for the latter).
>> 
>> jerome
>