diff -r 1fead823c7c6 -r 6e15de7dd871 doc-src/TutorialI/document/Overloading.tex --- a/doc-src/TutorialI/document/Overloading.tex Tue Aug 28 13:15:15 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: