9791
|
1 |
(* Title: HOL/BCV/Opt.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Tobias Nipkow
|
|
4 |
Copyright 2000 TUM
|
|
5 |
|
|
6 |
More about options
|
|
7 |
*)
|
|
8 |
|
|
9 |
Opt = Semilat +
|
|
10 |
|
|
11 |
constdefs
|
|
12 |
le :: 'a ord => 'a option ord
|
|
13 |
"le r o1 o2 == case o2 of None => o1=None |
|
|
14 |
Some y => (case o1 of None => True |
|
|
15 |
Some x => x <=_r y)"
|
|
16 |
|
|
17 |
opt :: 'a set => 'a option set
|
|
18 |
"opt A == insert None {x . ? y:A. x = Some y}"
|
|
19 |
|
|
20 |
sup :: 'a binop => 'a option binop
|
|
21 |
"sup f o1 o2 ==
|
|
22 |
case o1 of None => o2 | Some x => (case o2 of None => o1
|
|
23 |
| Some y => Some(f x y))"
|
|
24 |
|
|
25 |
sl :: "'a sl => 'a option sl"
|
|
26 |
"sl == %(A,r,f). (opt A, le r, sup f)"
|
|
27 |
|
|
28 |
end
|