1.1 --- a/doc-src/TutorialI/Types/document/Overloading.tex Thu Jul 26 16:08:16 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,159 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{Overloading}%
1.7 -%
1.8 -\isadelimtheory
1.9 -%
1.10 -\endisadelimtheory
1.11 -%
1.12 -\isatagtheory
1.13 -%
1.14 -\endisatagtheory
1.15 -{\isafoldtheory}%
1.16 -%
1.17 -\isadelimtheory
1.18 -%
1.19 -\endisadelimtheory
1.20 -%
1.21 -\begin{isamarkuptext}%
1.22 -Type classes allow \emph{overloading}; thus a constant may
1.23 -have multiple definitions at non-overlapping types.%
1.24 -\end{isamarkuptext}%
1.25 -\isamarkuptrue%
1.26 -%
1.27 -\isamarkupsubsubsection{Overloading%
1.28 -}
1.29 -\isamarkuptrue%
1.30 -%
1.31 -\begin{isamarkuptext}%
1.32 -We can introduce a binary infix addition operator \isa{{\isaliteral{5C3C6F74696D65733E}{\isasymotimes}}}
1.33 -for arbitrary types by means of a type class:%
1.34 -\end{isamarkuptext}%
1.35 -\isamarkuptrue%
1.36 -\isacommand{class}\isamarkupfalse%
1.37 -\ plus\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.38 -\ \ \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}}%
1.39 -\begin{isamarkuptext}%
1.40 -\noindent This introduces a new class \isa{plus},
1.41 -along with a constant \isa{plus} with nice infix syntax.
1.42 -\isa{plus} is also named \emph{class operation}. The type
1.43 -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
1.44 -\isa{plus} can be instantiated for \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequote}}}.
1.45 -To breathe life into \isa{plus} we need to declare a type
1.46 -to be an \bfindex{instance} of \isa{plus}:%
1.47 -\end{isamarkuptext}%
1.48 -\isamarkuptrue%
1.49 -\isacommand{instantiation}\isamarkupfalse%
1.50 -\ nat\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ plus\isanewline
1.51 -\isakeyword{begin}%
1.52 -\begin{isamarkuptext}%
1.53 -\noindent Command \isacommand{instantiation} opens a local
1.54 -theory context. Here we can now instantiate \isa{plus} on
1.55 -\isa{nat}:%
1.56 -\end{isamarkuptext}%
1.57 -\isamarkuptrue%
1.58 -\isacommand{primrec}\isamarkupfalse%
1.59 -\ 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
1.60 -\ \ \ \ {\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
1.61 -\ \ {\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}}%
1.62 -\begin{isamarkuptext}%
1.63 -\noindent Note that the name \isa{plus} carries a
1.64 -suffix \isa{{\isaliteral{5F}{\isacharunderscore}}nat}; by default, the local name of a class operation
1.65 -\isa{f} to be instantiated on type constructor \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is mangled
1.66 -as \isa{f{\isaliteral{5F}{\isacharunderscore}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}}. In case of uncertainty, these names may be inspected
1.67 -using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}context}}}} command or the corresponding
1.68 -ProofGeneral button.
1.69 -
1.70 -Although class \isa{plus} has no axioms, the instantiation must be
1.71 -formally concluded by a (trivial) instantiation proof ``..'':%
1.72 -\end{isamarkuptext}%
1.73 -\isamarkuptrue%
1.74 -\isacommand{instance}\isamarkupfalse%
1.75 -%
1.76 -\isadelimproof
1.77 -\ %
1.78 -\endisadelimproof
1.79 -%
1.80 -\isatagproof
1.81 -\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
1.82 -%
1.83 -\endisatagproof
1.84 -{\isafoldproof}%
1.85 -%
1.86 -\isadelimproof
1.87 -%
1.88 -\endisadelimproof
1.89 -%
1.90 -\begin{isamarkuptext}%
1.91 -\noindent More interesting \isacommand{instance} proofs will
1.92 -arise below.
1.93 -
1.94 -The instantiation is finished by an explicit%
1.95 -\end{isamarkuptext}%
1.96 -\isamarkuptrue%
1.97 -\isacommand{end}\isamarkupfalse%
1.98 -%
1.99 -\begin{isamarkuptext}%
1.100 -\noindent From now on, terms like \isa{Suc\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{5C3C6F706C75733E}{\isasymoplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} are
1.101 -legal.%
1.102 -\end{isamarkuptext}%
1.103 -\isamarkuptrue%
1.104 -\isacommand{instantiation}\isamarkupfalse%
1.105 -\ prod\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}plus{\isaliteral{2C}{\isacharcomma}}\ plus{\isaliteral{29}{\isacharparenright}}\ plus\isanewline
1.106 -\isakeyword{begin}%
1.107 -\begin{isamarkuptext}%
1.108 -\noindent Here we instantiate the product type \isa{prod} to
1.109 -class \isa{plus}, given that its type arguments are of
1.110 -class \isa{plus}:%
1.111 -\end{isamarkuptext}%
1.112 -\isamarkuptrue%
1.113 -\isacommand{fun}\isamarkupfalse%
1.114 -\ 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
1.115 -\ \ {\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}}%
1.116 -\begin{isamarkuptext}%
1.117 -\noindent Obviously, overloaded specifications may include
1.118 -recursion over the syntactic structure of types.%
1.119 -\end{isamarkuptext}%
1.120 -\isamarkuptrue%
1.121 -\isacommand{instance}\isamarkupfalse%
1.122 -%
1.123 -\isadelimproof
1.124 -\ %
1.125 -\endisadelimproof
1.126 -%
1.127 -\isatagproof
1.128 -\isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
1.129 -%
1.130 -\endisatagproof
1.131 -{\isafoldproof}%
1.132 -%
1.133 -\isadelimproof
1.134 -%
1.135 -\endisadelimproof
1.136 -\isanewline
1.137 -\isanewline
1.138 -\isacommand{end}\isamarkupfalse%
1.139 -%
1.140 -\begin{isamarkuptext}%
1.141 -\noindent This way we have encoded the canonical lifting of
1.142 -binary operations to products by means of type classes.%
1.143 -\end{isamarkuptext}%
1.144 -\isamarkuptrue%
1.145 -%
1.146 -\isadelimtheory
1.147 -%
1.148 -\endisadelimtheory
1.149 -%
1.150 -\isatagtheory
1.151 -%
1.152 -\endisatagtheory
1.153 -{\isafoldtheory}%
1.154 -%
1.155 -\isadelimtheory
1.156 -%
1.157 -\endisadelimtheory
1.158 -\end{isabellebody}%
1.159 -%%% Local Variables:
1.160 -%%% mode: latex
1.161 -%%% TeX-master: "root"
1.162 -%%% End: