|
2019
|
1 |
(* Title: Option.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1994 TU Muenchen
|
|
|
5 |
|
|
|
6 |
Datatype 'a option
|
|
|
7 |
*)
|
|
|
8 |
|
|
5183
|
9 |
Option = Datatype +
|
|
4133
|
10 |
|
|
2019
|
11 |
datatype 'a option = None | Some 'a
|
|
4133
|
12 |
|
|
|
13 |
constdefs
|
|
|
14 |
|
|
|
15 |
the :: "'a option => 'a"
|
|
4192
|
16 |
"the == %y. case y of None => arbitrary | Some x => x"
|
|
4133
|
17 |
|
|
|
18 |
option_map :: "('a => 'b) => ('a option => 'b option)"
|
|
4192
|
19 |
"option_map == %f y. case y of None => None | Some x => Some (f x)"
|
|
4133
|
20 |
|
|
4752
|
21 |
consts
|
|
|
22 |
|
|
|
23 |
o2s :: "'a option => 'a set"
|
|
|
24 |
|
|
5183
|
25 |
primrec
|
|
4752
|
26 |
"o2s None = {}"
|
|
|
27 |
"o2s (Some x) = {x}"
|
|
|
28 |
|
|
2019
|
29 |
end
|