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

Re: How can we extend type bool with a "bottom" element?


the DATATYPE mechanism of PVS can be used to define the disjoint union
type of two types A and B (see the recently announced revision of a
technical report by S. Owre and N. Shankar "Datatypes in PVS"; available
via the PVS-Homepage at http://www.csl.sri.com.pvs.html):

  disj_union [A,B : TYPE] : DATATYPE
    inl(left:A)  : inl?
    inr(right:B) : inr?
  END disj_union

There has also been a related discussion on the PVS mailinglist a year
ago. Harald Ruess suggested using conversions in order to hide the
"tags" 'inl' and 'inr':


  f(a: A): disj_union = a;   % instead of inl(a)

In order to solve your problem of defining a boolean type with a bottom
element you might want to define the type 'gen_bool' as follows:

  gen_bool : DATATYPE
      bottom : bottom?
      ordinary_bool(b:bool): isbool?
    END gen_bool

  CONVERSION ordinary_bool

The CONVERSION declaration allows you to also use boolean values
wherever gen_bool's are expected, e.g.:

  g(b:gen_bool) : gen_bool = TRUE

  foo : LEMMA
    FORALL (a,b:bool): g(a) = g(b)

Best regards,

	- Holger

Shtrichman Ofer wrote:
> we have a question concerning extending the predefined boolean type 
> with an additional "bottom" element.
> Extending e.g. integers with a bottom element is not difficult since
> there exist supertypes of the integers (e.g rationals); one can just
> define
> rat_nonint: TYPE = {x: rat | FORALL (y: int): x /= y} CONTAINING 2/3
> bt: rat_nonint
> gen_int: TYPE = {x: rat | x = bt OR integer_pred(x)}.
> Then bt is the designated bottom element. The most important thing in 
> this context is  that we can still use all functions which return 
> integer values in assignments to gen_int variables. Exactly the same 
> we would like to do with the extended boolean type that we are 
> looking for; it is important that we can still use e.g comparison 
> functions on integers (which return a boolean value) in assignments 
> to gen_bool variables. Thus we can not simply use an enumeration 
> type. It seems that there does not exist a union type constructor in 
> PVS so how can we define the gen_bool's?

Holger Pfeifer                               Tel.: (+49) 731 / 502-4124
Abteilung KI                                  Fax: (+49) 731 / 502-4119
Universitaet Ulm
D-89069 Ulm                    e-mail: pfeifer@ki.informatik.uni-ulm.de