author | wenzelm |
Tue, 18 May 2021 15:57:49 +0200 | |
changeset 73725 | cd9afbd0ccb9 |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
10561 | 1 |
(*<*) |
16417 | 2 |
theory Option2 imports Main begin |
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35416
diff
changeset
|
3 |
hide_const None Some |
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
35416
diff
changeset
|
4 |
hide_type option |
10561 | 5 |
(*>*) |
6 |
||
67406 | 7 |
text\<open>\indexbold{*option (type)}\indexbold{*None (constant)}% |
11428 | 8 |
\indexbold{*Some (constant)} |
10561 | 9 |
Our final datatype is very simple but still eminently useful: |
67406 | 10 |
\<close> |
10561 | 11 |
|
58860 | 12 |
datatype 'a option = None | Some 'a |
10561 | 13 |
|
67406 | 14 |
text\<open>\noindent |
11310 | 15 |
Frequently one needs to add a distinguished element to some existing type. |
69505 | 16 |
For example, type \<open>t option\<close> can model the result of a computation that |
69597 | 17 |
may either terminate with an error (represented by \<^const>\<open>None\<close>) or return |
18 |
some value \<^term>\<open>v\<close> (represented by \<^term>\<open>Some v\<close>). |
|
19 |
Similarly, \<^typ>\<open>nat\<close> extended with $\infty$ can be modeled by type |
|
20 |
\<^typ>\<open>nat option\<close>. In both cases one could define a new datatype with |
|
21 |
customized constructors like \<^term>\<open>Error\<close> and \<^term>\<open>Infinity\<close>, |
|
69505 | 22 |
but it is often simpler to use \<open>option\<close>. For an application see |
10561 | 23 |
\S\ref{sec:Trie}. |
67406 | 24 |
\<close> |
10561 | 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 |
(*>*) |