src/HOL/BCV/Opt.thy

Completely new version of BCV

(*  Title:      HOL/BCV/Opt.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

More about options
*)

Opt = Semilat +

constdefs
 le :: 'a ord => 'a option ord
"le r o1 o2 == case o2 of None => o1=None |
                              Some y => (case o1 of None => True |
                                                    Some x => x <=_r y)"

 opt :: 'a set => 'a option set
"opt A == insert None {x . ? y:A. x = Some y}"

 sup :: 'a binop => 'a option binop
"sup f o1 o2 ==
 case o1 of None => o2 | Some x => (case o2 of None => o1
                                             | Some y => Some(f x y))"

 sl :: "'a sl => 'a option sl"
"sl == %(A,r,f). (opt A, le r, sup f)"

end