src/Doc/Tutorial/Misc/Option2.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 48985 5386df44a037
child 67406 23307fd33906
permissions -rw-r--r--
eliminated spurious semicolons;
nipkow@10561
     1
(*<*)
haftmann@16417
     2
theory Option2 imports Main begin
wenzelm@36176
     3
hide_const None Some
wenzelm@36176
     4
hide_type option
nipkow@10561
     5
(*>*)
nipkow@10561
     6
paulson@11428
     7
text{*\indexbold{*option (type)}\indexbold{*None (constant)}%
paulson@11428
     8
\indexbold{*Some (constant)}
nipkow@10561
     9
Our final datatype is very simple but still eminently useful:
nipkow@10561
    10
*}
nipkow@10561
    11
wenzelm@58860
    12
datatype 'a option = None | Some 'a
nipkow@10561
    13
nipkow@10561
    14
text{*\noindent
paulson@11310
    15
Frequently one needs to add a distinguished element to some existing type.
nipkow@10561
    16
For example, type @{text"t option"} can model the result of a computation that
haftmann@15905
    17
may either terminate with an error (represented by @{const None}) or return
nipkow@10561
    18
some value @{term v} (represented by @{term"Some v"}).
nipkow@10561
    19
Similarly, @{typ nat} extended with $\infty$ can be modeled by type
nipkow@10561
    20
@{typ"nat option"}. In both cases one could define a new datatype with
nipkow@10561
    21
customized constructors like @{term Error} and @{term Infinity},
nipkow@10561
    22
but it is often simpler to use @{text option}. For an application see
nipkow@10561
    23
\S\ref{sec:Trie}.
nipkow@10561
    24
*}
nipkow@10561
    25
(*<*)
nipkow@10561
    26
(*
haftmann@35416
    27
definition infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" where
nipkow@10561
    28
"infplus x y \<equiv> case x of None \<Rightarrow> None
nipkow@10561
    29
               | Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))"
nipkow@10561
    30
nipkow@10561
    31
*)
nipkow@10561
    32
end
nipkow@10561
    33
(*>*)