author | haftmann |
Mon, 01 Mar 2010 13:40:23 +0100 | |
changeset 35416 | d8d7d1b785af |
parent 16417 | 9bc16273c2d4 |
child 36176 | 3fe7e97ccca8 |
permissions | -rw-r--r-- |
10561 | 1 |
(*<*) |
16417 | 2 |
theory Option2 imports Main begin |
10561 | 3 |
hide const None Some |
4 |
hide type option |
|
5 |
(*>*) |
|
6 |
||
11428 | 7 |
text{*\indexbold{*option (type)}\indexbold{*None (constant)}% |
8 |
\indexbold{*Some (constant)} |
|
10561 | 9 |
Our final datatype is very simple but still eminently useful: |
10 |
*} |
|
11 |
||
12 |
datatype 'a option = None | Some 'a; |
|
13 |
||
14 |
text{*\noindent |
|
11310 | 15 |
Frequently one needs to add a distinguished element to some existing type. |
10561 | 16 |
For example, type @{text"t option"} can model the result of a computation that |
15905 | 17 |
may either terminate with an error (represented by @{const None}) or return |
10561 | 18 |
some value @{term v} (represented by @{term"Some v"}). |
19 |
Similarly, @{typ nat} extended with $\infty$ can be modeled by type |
|
20 |
@{typ"nat option"}. In both cases one could define a new datatype with |
|
21 |
customized constructors like @{term Error} and @{term Infinity}, |
|
22 |
but it is often simpler to use @{text option}. For an application see |
|
23 |
\S\ref{sec:Trie}. |
|
24 |
*} |
|
25 |
(*<*) |
|
26 |
(* |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
16417
diff
changeset
|
27 |
definition infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" where |
10561 | 28 |
"infplus x y \<equiv> case x of None \<Rightarrow> None |
29 |
| Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))" |
|
30 |
||
31 |
*) |
|
32 |
end |
|
33 |
(*>*) |