--- a/doc-src/TutorialI/Types/document/Overloading.tex Thu Jul 26 16:08:16 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,159 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Overloading}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\begin{isamarkuptext}%
-Type classes allow \emph{overloading}; thus a constant may
-have multiple definitions at non-overlapping types.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsubsection{Overloading%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-We can introduce a binary infix addition operator \isa{{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}}
-for arbitrary types by means of a type class:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{class}\isamarkupfalse%
-\ plus\ {\isaliteral{3D}{\isacharequal}}\isanewline
-\ \ \isakeyword{fixes}\ plus\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}%
-\begin{isamarkuptext}%
-\noindent This introduces a new class \isa{plus},
-along with a constant \isa{plus} with nice infix syntax.
-\isa{plus} is also named \emph{class operation}. The type
-of \isa{plus} carries a class constraint \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus{\isaliteral{22}{\isachardoublequote}}} on its type variable, meaning that only types of class
-\isa{plus} can be instantiated for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}}.
-To breathe life into \isa{plus} we need to declare a type
-to be an \bfindex{instance} of \isa{plus}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instantiation}\isamarkupfalse%
-\ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus\isanewline
-\isakeyword{begin}%
-\begin{isamarkuptext}%
-\noindent Command \isacommand{instantiation} opens a local
-theory context. Here we can now instantiate \isa{plus} on
-\isa{nat}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{primrec}\isamarkupfalse%
-\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
-\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}Suc\ m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent Note that the name \isa{plus} carries a
-suffix \isa{{\isaliteral{5F}{\isacharunderscore}}nat}; by default, the local name of a class operation
-\isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is mangled
-as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. In case of uncertainty, these names may be inspected
-using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the corresponding
-ProofGeneral button.
-
-Although class \isa{plus} has no axioms, the instantiation must be
-formally concluded by a (trivial) instantiation proof ``..'':%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent More interesting \isacommand{instance} proofs will
-arise below.
-
-The instantiation is finished by an explicit%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{end}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-\noindent From now on, terms like \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} are
-legal.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instantiation}\isamarkupfalse%
-\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}plus{\isaliteral{2C}{\isacharcomma}}\ plus{\isaliteral{29}{\isacharparenright}}\ plus\isanewline
-\isakeyword{begin}%
-\begin{isamarkuptext}%
-\noindent Here we instantiate the product type \isa{prod} to
-class \isa{plus}, given that its type arguments are of
-class \isa{plus}:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{fun}\isamarkupfalse%
-\ plus{\isaliteral{5F}{\isacharunderscore}}prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isaliteral{28}{\isacharparenleft}}w{\isaliteral{2C}{\isacharcomma}}\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ w{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
-\begin{isamarkuptext}%
-\noindent Obviously, overloaded specifications may include
-recursion over the syntactic structure of types.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{instance}\isamarkupfalse%
-%
-\isadelimproof
-\ %
-\endisadelimproof
-%
-\isatagproof
-\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-\isanewline
-\isanewline
-\isacommand{end}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-\noindent This way we have encoded the canonical lifting of
-binary operations to products by means of type classes.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: