# HG changeset patch
# User nipkow
# Date 975674857 -3600
# Node ID d960cc4a6afcb678d99bd98dc536bf4f9df6ea5b
# Parent  f4da791d48505743aaf69ffcbdf671a9dd07136c
*** empty log message ***

diff -r f4da791d4850 -r d960cc4a6afc doc-src/TutorialI/Misc/Option2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Option2.thy	Fri Dec 01 13:47:37 2000 +0100
@@ -0,0 +1,33 @@
+(*<*)
+theory Option2 = Main:
+hide const None Some
+hide type option
+(*>*)
+
+text{*\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+Our final datatype is very simple but still eminently useful:
+*}
+
+datatype 'a option = None | Some 'a;
+
+text{*\noindent
+Frequently one needs to add a distiguished element to some existing type.
+For example, type @{text"t option"} can model the result of a computation that
+may either terminate with an error (represented by @{term None}) or return
+some value @{term v} (represented by @{term"Some v"}).
+Similarly, @{typ nat} extended with $\infty$ can be modeled by type
+@{typ"nat option"}. In both cases one could define a new datatype with
+customized constructors like @{term Error} and @{term Infinity},
+but it is often simpler to use @{text option}. For an application see
+\S\ref{sec:Trie}.
+*}
+(*<*)
+(*
+constdefs
+ infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option"
+"infplus x y \<equiv> case x of None \<Rightarrow> None
+               | Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))"
+
+*)
+end
+(*>*)
diff -r f4da791d4850 -r d960cc4a6afc doc-src/TutorialI/Misc/document/Option2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/Option2.tex	Fri Dec 01 13:47:37 2000 +0100
@@ -0,0 +1,26 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Option{\isadigit{2}}}%
+%
+\begin{isamarkuptext}%
+\indexbold{*option}\indexbold{*None}\indexbold{*Some}
+Our final datatype is very simple but still eminently useful:%
+\end{isamarkuptext}%
+\isacommand{datatype}\ {\isacharprime}a\ option\ {\isacharequal}\ None\ {\isacharbar}\ Some\ {\isacharprime}a%
+\begin{isamarkuptext}%
+\noindent
+Frequently one needs to add a distiguished element to some existing type.
+For example, type \isa{t\ option} can model the result of a computation that
+may either terminate with an error (represented by \isa{None}) or return
+some value \isa{v} (represented by \isa{Some\ v}).
+Similarly, \isa{nat} extended with $\infty$ can be modeled by type
+\isa{nat\ option}. In both cases one could define a new datatype with
+customized constructors like \isa{Error} and \isa{Infinity},
+but it is often simpler to use \isa{option}. For an application see
+\S\ref{sec:Trie}.%
+\end{isamarkuptext}%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: