src/Doc/Tutorial/Misc/Option2.thy
author wenzelm
Tue, 18 May 2021 15:57:49 +0200
changeset 73725 cd9afbd0ccb9
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
redundant: copy produced from session document_files;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10561
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
     1
(*<*)
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 15905
diff changeset
     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
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
     5
(*>*)
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
     6
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
     7
text\<open>\indexbold{*option (type)}\indexbold{*None (constant)}%
11428
332347b9b942 tidying the index
paulson
parents: 11310
diff changeset
     8
\indexbold{*Some (constant)}
10561
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
     9
Our final datatype is very simple but still eminently useful:
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    10
\<close>
10561
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    11
58860
fee7cfa69c50 eliminated spurious semicolons;
wenzelm
parents: 48985
diff changeset
    12
datatype 'a option = None | Some 'a
10561
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    13
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    14
text\<open>\noindent
11310
51e70b7bc315 spelling check
paulson
parents: 10561
diff changeset
    15
Frequently one needs to add a distinguished element to some existing type.
69505
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67406
diff changeset
    16
For example, type \<open>t option\<close> can model the result of a computation that
69597
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    17
may either terminate with an error (represented by \<^const>\<open>None\<close>) or return
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    18
some value \<^term>\<open>v\<close> (represented by \<^term>\<open>Some v\<close>).
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    19
Similarly, \<^typ>\<open>nat\<close> extended with $\infty$ can be modeled by type
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    20
\<^typ>\<open>nat option\<close>. In both cases one could define a new datatype with
ff784d5a5bfb isabelle update -u control_cartouches;
wenzelm
parents: 69505
diff changeset
    21
customized constructors like \<^term>\<open>Error\<close> and \<^term>\<open>Infinity\<close>,
69505
cc2d676d5395 isabelle update_cartouches -t;
wenzelm
parents: 67406
diff changeset
    22
but it is often simpler to use \<open>option\<close>. For an application see
10561
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    23
\S\ref{sec:Trie}.
67406
23307fd33906 isabelle update_cartouches -c;
wenzelm
parents: 58860
diff changeset
    24
\<close>
10561
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    25
(*<*)
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    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
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    28
"infplus x y \<equiv> case x of None \<Rightarrow> None
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    29
               | Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))"
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    30
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    31
*)
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    32
end
d960cc4a6afc *** empty log message ***
nipkow
parents:
diff changeset
    33
(*>*)