doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
changeset 28565 519b17118926
parent 28540 541366e3c1b3
child 28566 be2a72b421ae
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:23:33 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:52:45 2008 +0200
     1.3 @@ -3,12 +3,14 @@
     1.4  \def\isabellecontext{Classes}%
     1.5  %
     1.6  \isadelimtheory
     1.7 -\isanewline
     1.8  %
     1.9  \endisadelimtheory
    1.10  %
    1.11  \isatagtheory
    1.12 -%
    1.13 +\isacommand{theory}\isamarkupfalse%
    1.14 +\ Classes\isanewline
    1.15 +\isakeyword{imports}\ Main\ Setup\isanewline
    1.16 +\isakeyword{begin}%
    1.17  \endisatagtheory
    1.18  {\isafoldtheory}%
    1.19  %
    1.20 @@ -16,32 +18,6 @@
    1.21  %
    1.22  \endisadelimtheory
    1.23  %
    1.24 -\isadelimML
    1.25 -%
    1.26 -\endisadelimML
    1.27 -%
    1.28 -\isatagML
    1.29 -%
    1.30 -\endisatagML
    1.31 -{\isafoldML}%
    1.32 -%
    1.33 -\isadelimML
    1.34 -%
    1.35 -\endisadelimML
    1.36 -%
    1.37 -\isadelimML
    1.38 -%
    1.39 -\endisadelimML
    1.40 -%
    1.41 -\isatagML
    1.42 -%
    1.43 -\endisatagML
    1.44 -{\isafoldML}%
    1.45 -%
    1.46 -\isadelimML
    1.47 -%
    1.48 -\endisadelimML
    1.49 -%
    1.50  \isamarkupchapter{Haskell-style classes with Isabelle/Isar%
    1.51  }
    1.52  \isamarkuptrue%
    1.53 @@ -62,23 +38,27 @@
    1.54    of the \isa{eq} function from its overloaded definitions by means
    1.55    of \isa{class} and \isa{instance} declarations:
    1.56  
    1.57 -  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
    1.58 -  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    1.59 +  \begin{quote}
    1.60 +
    1.61 +  \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
    1.62 +  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    1.63  
    1.64 -  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
    1.65 -  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
    1.66 -  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
    1.67 -  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
    1.68 -  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
    1.69 +  \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
    1.70 +  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
    1.71 +  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
    1.72 +  \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
    1.73 +  \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
    1.74  
    1.75 -  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
    1.76 -  \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
    1.77 +  \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
    1.78 +  \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
    1.79  
    1.80 -  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
    1.81 -  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
    1.82 -  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    1.83 +  \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
    1.84 +  \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
    1.85 +  \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    1.86  
    1.87 -  \medskip\noindent Type variables are annotated with (finitely many) classes;
    1.88 +  \end{quote}
    1.89 +
    1.90 +  \noindent Type variables are annotated with (finitely many) classes;
    1.91    these annotations are assertions that a particular polymorphic type
    1.92    provides definitions for overloaded functions.
    1.93  
    1.94 @@ -95,14 +75,18 @@
    1.95    \isa{class\ eq} is an equivalence relation obeying reflexivity,
    1.96    symmetry and transitivity:
    1.97  
    1.98 -  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
    1.99 -  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
   1.100 -  \hspace*{2ex}\isa{satisfying} \\
   1.101 -  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
   1.102 -  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
   1.103 -  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
   1.104 +  \begin{quote}
   1.105  
   1.106 -  \medskip\noindent From a theoretic point of view, type classes are lightweight
   1.107 +  \noindent\isa{class\ eq\ where} \\
   1.108 +  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
   1.109 +  \isa{satisfying} \\
   1.110 +  \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
   1.111 +  \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
   1.112 +  \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
   1.113 +
   1.114 +  \end{quote}
   1.115 +
   1.116 +  \noindent From a theoretic point of view, type classes are lightweight
   1.117    modules; Haskell type classes may be emulated by
   1.118    SML functors \cite{classes_modules}. 
   1.119    Isabelle/Isar offers a discipline of type classes which brings
   1.120 @@ -142,20 +126,36 @@
   1.121  \isamarkuptrue%
   1.122  %
   1.123  \begin{isamarkuptext}%
   1.124 -Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isasymotimes}} that is
   1.125 +Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
   1.126    assumed to be associative:%
   1.127  \end{isamarkuptext}%
   1.128  \isamarkuptrue%
   1.129 -\ \ \ \ \isacommand{class}\isamarkupfalse%
   1.130 +%
   1.131 +\isadelimquote
   1.132 +%
   1.133 +\endisadelimquote
   1.134 +%
   1.135 +\isatagquote
   1.136 +\isacommand{class}\isamarkupfalse%
   1.137  \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
   1.138 -\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
   1.139 -\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
   1.140 +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
   1.141 +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
   1.142 +\endisatagquote
   1.143 +{\isafoldquote}%
   1.144 +%
   1.145 +\isadelimquote
   1.146 +%
   1.147 +\endisadelimquote
   1.148 +%
   1.149  \begin{isamarkuptext}%
   1.150 -\noindent This \isa{{\isasymCLASS}} specification consists of two
   1.151 -  parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
   1.152 -  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
   1.153 +\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
   1.154 +  parts: the \qn{operational} part names the class parameter
   1.155 +  (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
   1.156 +  (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}).  The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
   1.157 +  \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
   1.158 +  yielding the global
   1.159    parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
   1.160 -  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
   1.161 +  global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
   1.162  \end{isamarkuptext}%
   1.163  \isamarkuptrue%
   1.164  %
   1.165 @@ -166,57 +166,57 @@
   1.166  \begin{isamarkuptext}%
   1.167  The concrete type \isa{int} is made a \isa{semigroup}
   1.168    instance by providing a suitable definition for the class parameter
   1.169 -  \isa{mult} and a proof for the specification of \isa{assoc}.
   1.170 -  This is accomplished by the \isa{{\isasymINSTANTIATION}} target:%
   1.171 +  \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
   1.172 +  This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
   1.173  \end{isamarkuptext}%
   1.174  \isamarkuptrue%
   1.175 -\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   1.176 +%
   1.177 +\isadelimquote
   1.178 +%
   1.179 +\endisadelimquote
   1.180 +%
   1.181 +\isatagquote
   1.182 +\isacommand{instantiation}\isamarkupfalse%
   1.183  \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
   1.184 -\ \ \ \ \isakeyword{begin}\isanewline
   1.185 -\isanewline
   1.186 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   1.187 -\isanewline
   1.188 -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.189 +\isakeyword{begin}\isanewline
   1.190  \isanewline
   1.191 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
   1.192 -%
   1.193 -\isadelimproof
   1.194 -\ %
   1.195 -\endisadelimproof
   1.196 -%
   1.197 -\isatagproof
   1.198 -\isacommand{proof}\isamarkupfalse%
   1.199 +\isacommand{definition}\isamarkupfalse%
   1.200 +\isanewline
   1.201 +\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.202  \isanewline
   1.203 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   1.204 +\isacommand{instance}\isamarkupfalse%
   1.205 +\ \isacommand{proof}\isamarkupfalse%
   1.206 +\isanewline
   1.207 +\ \ \isacommand{fix}\isamarkupfalse%
   1.208  \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
   1.209  \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   1.210  \ simp\isanewline
   1.211 -\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.212 +\ \ \isacommand{then}\isamarkupfalse%
   1.213  \ \isacommand{show}\isamarkupfalse%
   1.214  \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.215 -\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   1.216 +\ \ \isacommand{unfolding}\isamarkupfalse%
   1.217  \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
   1.218  \isanewline
   1.219 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
   1.220 -%
   1.221 -\endisatagproof
   1.222 -{\isafoldproof}%
   1.223 -%
   1.224 -\isadelimproof
   1.225 -%
   1.226 -\endisadelimproof
   1.227 +\isacommand{qed}\isamarkupfalse%
   1.228  \isanewline
   1.229  \isanewline
   1.230 -\ \ \ \ \isacommand{end}\isamarkupfalse%
   1.231 +\isacommand{end}\isamarkupfalse%
   1.232 +%
   1.233 +\endisatagquote
   1.234 +{\isafoldquote}%
   1.235 +%
   1.236 +\isadelimquote
   1.237 +%
   1.238 +\endisadelimquote
   1.239  %
   1.240  \begin{isamarkuptext}%
   1.241 -\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters
   1.242 +\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
   1.243    at a particular instance using common specification tools (here,
   1.244 -  \isa{{\isasymDEFINITION}}).  The concluding \isa{{\isasymINSTANCE}}
   1.245 +  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
   1.246    opens a proof that the given parameters actually conform
   1.247    to the class specification.  Note that the first proof step
   1.248 -  is the \isa{default} method,
   1.249 -  which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method.
   1.250 +  is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
   1.251 +  which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
   1.252    This boils down an instance judgement to the relevant primitive
   1.253    proof goals and should conveniently always be the first method applied
   1.254    in an instantiation proof.
   1.255 @@ -224,51 +224,52 @@
   1.256    From now on, the type-checker will consider \isa{int}
   1.257    as a \isa{semigroup} automatically, i.e.\ any general results
   1.258    are immediately available on concrete instances.
   1.259 +
   1.260    \medskip Another instance of \isa{semigroup} are the natural numbers:%
   1.261  \end{isamarkuptext}%
   1.262  \isamarkuptrue%
   1.263 -\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   1.264 -\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
   1.265 -\ \ \ \ \isakeyword{begin}\isanewline
   1.266 -\isanewline
   1.267 -\ \ \ \ \isacommand{primrec}\isamarkupfalse%
   1.268 -\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
   1.269 -\ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
   1.270 -\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.271 -\isanewline
   1.272 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
   1.273  %
   1.274 -\isadelimproof
   1.275 -\ %
   1.276 -\endisadelimproof
   1.277 +\isadelimquote
   1.278 +%
   1.279 +\endisadelimquote
   1.280  %
   1.281 -\isatagproof
   1.282 -\isacommand{proof}\isamarkupfalse%
   1.283 +\isatagquote
   1.284 +\isacommand{instantiation}\isamarkupfalse%
   1.285 +\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
   1.286 +\isakeyword{begin}\isanewline
   1.287  \isanewline
   1.288 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   1.289 +\isacommand{primrec}\isamarkupfalse%
   1.290 +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
   1.291 +\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
   1.292 +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.293 +\isanewline
   1.294 +\isacommand{instance}\isamarkupfalse%
   1.295 +\ \isacommand{proof}\isamarkupfalse%
   1.296 +\isanewline
   1.297 +\ \ \isacommand{fix}\isamarkupfalse%
   1.298  \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
   1.299 -\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   1.300 +\ \ \isacommand{show}\isamarkupfalse%
   1.301  \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.302 -\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   1.303 +\ \ \ \ \isacommand{by}\isamarkupfalse%
   1.304  \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
   1.305 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
   1.306 -%
   1.307 -\endisatagproof
   1.308 -{\isafoldproof}%
   1.309 -%
   1.310 -\isadelimproof
   1.311 -%
   1.312 -\endisadelimproof
   1.313 +\isacommand{qed}\isamarkupfalse%
   1.314  \isanewline
   1.315  \isanewline
   1.316 -\ \ \ \ \isacommand{end}\isamarkupfalse%
   1.317 +\isacommand{end}\isamarkupfalse%
   1.318 +%
   1.319 +\endisatagquote
   1.320 +{\isafoldquote}%
   1.321 +%
   1.322 +\isadelimquote
   1.323 +%
   1.324 +\endisadelimquote
   1.325  %
   1.326  \begin{isamarkuptext}%
   1.327  \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
   1.328    in the primrec declaration;  by default, the local name of
   1.329    a class operation \isa{f} to instantiate on type constructor
   1.330    \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
   1.331 -  these names may be inspected using the \isa{{\isasymPRINTCONTEXT}} command
   1.332 +  these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
   1.333    or the corresponding ProofGeneral button.%
   1.334  \end{isamarkuptext}%
   1.335  \isamarkuptrue%
   1.336 @@ -284,49 +285,49 @@
   1.337    using our simple algebra:%
   1.338  \end{isamarkuptext}%
   1.339  \isamarkuptrue%
   1.340 -\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   1.341 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
   1.342 -\ \ \ \ \isakeyword{begin}\isanewline
   1.343 -\isanewline
   1.344 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   1.345 -\isanewline
   1.346 -\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.347 -\isanewline
   1.348 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
   1.349 +%
   1.350 +\isadelimquote
   1.351 +%
   1.352 +\endisadelimquote
   1.353  %
   1.354 -\isadelimproof
   1.355 -\ %
   1.356 -\endisadelimproof
   1.357 -%
   1.358 -\isatagproof
   1.359 -\isacommand{proof}\isamarkupfalse%
   1.360 +\isatagquote
   1.361 +\isacommand{instantiation}\isamarkupfalse%
   1.362 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
   1.363 +\isakeyword{begin}\isanewline
   1.364 +\isanewline
   1.365 +\isacommand{definition}\isamarkupfalse%
   1.366 +\isanewline
   1.367 +\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.368  \isanewline
   1.369 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   1.370 +\isacommand{instance}\isamarkupfalse%
   1.371 +\ \isacommand{proof}\isamarkupfalse%
   1.372 +\isanewline
   1.373 +\ \ \isacommand{fix}\isamarkupfalse%
   1.374  \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
   1.375 -\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   1.376 +\ \ \isacommand{show}\isamarkupfalse%
   1.377  \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   1.378 -\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   1.379 +\ \ \isacommand{unfolding}\isamarkupfalse%
   1.380  \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   1.381  \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
   1.382 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
   1.383 -%
   1.384 -\endisatagproof
   1.385 -{\isafoldproof}%
   1.386 -%
   1.387 -\isadelimproof
   1.388 -%
   1.389 -\endisadelimproof
   1.390 +\isacommand{qed}\isamarkupfalse%
   1.391  \ \ \ \ \ \ \isanewline
   1.392  \isanewline
   1.393 -\ \ \ \ \isacommand{end}\isamarkupfalse%
   1.394 +\isacommand{end}\isamarkupfalse%
   1.395 +%
   1.396 +\endisatagquote
   1.397 +{\isafoldquote}%
   1.398 +%
   1.399 +\isadelimquote
   1.400 +%
   1.401 +\endisadelimquote
   1.402  %
   1.403  \begin{isamarkuptext}%
   1.404  \noindent Associativity from product semigroups is
   1.405    established using
   1.406 -  the definition of \isa{{\isasymotimes}} on products and the hypothetical
   1.407 +  the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
   1.408    associativity of the type components;  these hypotheses
   1.409    are facts due to the \isa{semigroup} constraints imposed
   1.410 -  on the type components by the \isa{instance} proposition.
   1.411 +  on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
   1.412    Indeed, this pattern often occurs with parametric types
   1.413    and type classes.%
   1.414  \end{isamarkuptext}%
   1.415 @@ -343,10 +344,23 @@
   1.416    with its property:%
   1.417  \end{isamarkuptext}%
   1.418  \isamarkuptrue%
   1.419 -\ \ \ \ \isacommand{class}\isamarkupfalse%
   1.420 +%
   1.421 +\isadelimquote
   1.422 +%
   1.423 +\endisadelimquote
   1.424 +%
   1.425 +\isatagquote
   1.426 +\isacommand{class}\isamarkupfalse%
   1.427  \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
   1.428 -\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.429 -\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
   1.430 +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   1.431 +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
   1.432 +\endisatagquote
   1.433 +{\isafoldquote}%
   1.434 +%
   1.435 +\isadelimquote
   1.436 +%
   1.437 +\endisadelimquote
   1.438 +%
   1.439  \begin{isamarkuptext}%
   1.440  \noindent Again, we prove some instances, by
   1.441    providing suitable parameter definitions and proofs for the
   1.442 @@ -597,18 +611,21 @@
   1.443  \end{isamarkuptext}%
   1.444  \isamarkuptrue%
   1.445  %
   1.446 -\isadelimML
   1.447 +\isadeliminvisible
   1.448  %
   1.449 -\endisadelimML
   1.450 -%
   1.451 -\isatagML
   1.452 +\endisadeliminvisible
   1.453  %
   1.454 -\endisatagML
   1.455 -{\isafoldML}%
   1.456 +\isataginvisible
   1.457 +\isacommand{setup}\isamarkupfalse%
   1.458 +\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
   1.459 +\endisataginvisible
   1.460 +{\isafoldinvisible}%
   1.461  %
   1.462 -\isadelimML
   1.463 +\isadeliminvisible
   1.464  %
   1.465 -\endisadelimML
   1.466 +\endisadeliminvisible
   1.467 +\isanewline
   1.468 +\isanewline
   1.469  \isacommand{locale}\isamarkupfalse%
   1.470  \ idem\ {\isacharequal}\isanewline
   1.471  \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   1.472 @@ -646,21 +663,24 @@
   1.473  {\isafoldproof}%
   1.474  %
   1.475  \isadelimproof
   1.476 +\isanewline
   1.477  %
   1.478  \endisadelimproof
   1.479  %
   1.480 -\isadelimML
   1.481 +\isadeliminvisible
   1.482 +\isanewline
   1.483  %
   1.484 -\endisadelimML
   1.485 -%
   1.486 -\isatagML
   1.487 +\endisadeliminvisible
   1.488  %
   1.489 -\endisatagML
   1.490 -{\isafoldML}%
   1.491 +\isataginvisible
   1.492 +\isacommand{setup}\isamarkupfalse%
   1.493 +\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
   1.494 +\endisataginvisible
   1.495 +{\isafoldinvisible}%
   1.496  %
   1.497 -\isadelimML
   1.498 +\isadeliminvisible
   1.499  %
   1.500 -\endisadelimML
   1.501 +\endisadeliminvisible
   1.502  %
   1.503  \begin{isamarkuptext}%
   1.504  This give you at hand the full power of the Isabelle module system;
   1.505 @@ -724,9 +744,9 @@
   1.506  \endisadelimproof
   1.507  %
   1.508  \begin{isamarkuptext}%
   1.509 -\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
   1.510 +\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
   1.511    indicates that the result is recorded within that context for later
   1.512 -  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
   1.513 +  use.  This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
   1.514    \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
   1.515  \end{isamarkuptext}%
   1.516  \isamarkuptrue%
   1.517 @@ -772,7 +792,7 @@
   1.518    a canonical interpretation as type classes.
   1.519    Anyway, there is also the possibility of other interpretations.
   1.520    For example, also \isa{list}s form a monoid with
   1.521 -  \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   1.522 +  \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   1.523    seems inappropriate to apply to lists
   1.524    the same operations as for genuinely algebraic types.
   1.525    In such a case, we simply can do a particular interpretation
   1.526 @@ -780,7 +800,7 @@
   1.527  \end{isamarkuptext}%
   1.528  \isamarkuptrue%
   1.529  \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
   1.530 -\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   1.531 +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   1.532  %
   1.533  \isadelimproof
   1.534  \ \ \ \ \ \ %
   1.535 @@ -810,8 +830,8 @@
   1.536  \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
   1.537  \isanewline
   1.538  \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
   1.539 -\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
   1.540 -\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   1.541 +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
   1.542 +\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   1.543  %
   1.544  \isadelimproof
   1.545  \ \ \ \ %
   1.546 @@ -821,16 +841,16 @@
   1.547  \isacommand{proof}\isamarkupfalse%
   1.548  \ {\isacharminus}\isanewline
   1.549  \ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
   1.550 -\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   1.551 +\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   1.552  \isanewline
   1.553  \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   1.554 -\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   1.555 +\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   1.556  \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
   1.557  \isanewline
   1.558  \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   1.559  \ n\isanewline
   1.560  \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   1.561 -\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
   1.562 +\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
   1.563  \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   1.564  \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
   1.565  \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
   1.566 @@ -932,12 +952,24 @@
   1.567    in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
   1.568  \end{isamarkuptext}%
   1.569  \isamarkuptrue%
   1.570 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   1.571 -\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline
   1.572 -\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.573 -\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
   1.574 -\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   1.575 -\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
   1.576 +%
   1.577 +\isadelimquote
   1.578 +%
   1.579 +\endisadelimquote
   1.580 +%
   1.581 +\isatagquote
   1.582 +\isacommand{definition}\isamarkupfalse%
   1.583 +\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.584 +\ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
   1.585 +\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   1.586 +\ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
   1.587 +\endisatagquote
   1.588 +{\isafoldquote}%
   1.589 +%
   1.590 +\isadelimquote
   1.591 +%
   1.592 +\endisadelimquote
   1.593 +%
   1.594  \begin{isamarkuptext}%
   1.595  \noindent yields the global definition of
   1.596    \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
   1.597 @@ -955,6 +987,12 @@
   1.598    uniformly;  type inference resolves ambiguities.  For example:%
   1.599  \end{isamarkuptext}%
   1.600  \isamarkuptrue%
   1.601 +%
   1.602 +\isadelimquote
   1.603 +%
   1.604 +\endisadelimquote
   1.605 +%
   1.606 +\isatagquote
   1.607  \isacommand{context}\isamarkupfalse%
   1.608  \ semigroup\isanewline
   1.609  \isakeyword{begin}\isanewline
   1.610 @@ -968,16 +1006,36 @@
   1.611  \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
   1.612  \isamarkupcmt{example 2%
   1.613  }
   1.614 +%
   1.615 +\endisatagquote
   1.616 +{\isafoldquote}%
   1.617 +%
   1.618 +\isadelimquote
   1.619 +%
   1.620 +\endisadelimquote
   1.621  \isanewline
   1.622  \isanewline
   1.623  \isacommand{end}\isamarkupfalse%
   1.624  \isanewline
   1.625 +%
   1.626 +\isadelimquote
   1.627  \isanewline
   1.628 +%
   1.629 +\endisadelimquote
   1.630 +%
   1.631 +\isatagquote
   1.632  \isacommand{term}\isamarkupfalse%
   1.633  \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
   1.634  \isamarkupcmt{example 3%
   1.635  }
   1.636  %
   1.637 +\endisatagquote
   1.638 +{\isafoldquote}%
   1.639 +%
   1.640 +\isadelimquote
   1.641 +%
   1.642 +\endisadelimquote
   1.643 +%
   1.644  \begin{isamarkuptext}%
   1.645  \noindent Here in example 1, the term refers to the local class operation
   1.646    \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
   1.647 @@ -994,30 +1052,42 @@
   1.648  \begin{isamarkuptext}%
   1.649  Turning back to the first motivation for type classes,
   1.650    namely overloading, it is obvious that overloading
   1.651 -  stemming from \isa{{\isasymCLASS}} statements and
   1.652 -  \isa{{\isasymINSTANTIATION}}
   1.653 +  stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
   1.654 +  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
   1.655    targets naturally maps to Haskell type classes.
   1.656    The code generator framework \cite{isabelle-codegen} 
   1.657    takes this into account.  Concerning target languages
   1.658    lacking type classes (e.g.~SML), type classes
   1.659    are implemented by explicit dictionary construction.
   1.660 -  For example, lets go back to the power function:%
   1.661 +  As example, let's go back to the power function:%
   1.662  \end{isamarkuptext}%
   1.663  \isamarkuptrue%
   1.664 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   1.665 -\isanewline
   1.666 -\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
   1.667 -\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   1.668 +%
   1.669 +\isadelimquote
   1.670 +%
   1.671 +\endisadelimquote
   1.672 +%
   1.673 +\isatagquote
   1.674 +\isacommand{definition}\isamarkupfalse%
   1.675 +\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
   1.676 +\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   1.677 +\endisatagquote
   1.678 +{\isafoldquote}%
   1.679 +%
   1.680 +\isadelimquote
   1.681 +%
   1.682 +\endisadelimquote
   1.683 +%
   1.684  \begin{isamarkuptext}%
   1.685  \noindent This maps to Haskell as:%
   1.686  \end{isamarkuptext}%
   1.687  \isamarkuptrue%
   1.688  %
   1.689 -\isadelimquoteme
   1.690 +\isadelimquote
   1.691  %
   1.692 -\endisadelimquoteme
   1.693 +\endisadelimquote
   1.694  %
   1.695 -\isatagquoteme
   1.696 +\isatagquote
   1.697  %
   1.698  \begin{isamarkuptext}%
   1.699  \isaverbatim%
   1.700 @@ -1088,23 +1158,23 @@
   1.701  \end{isamarkuptext}%
   1.702  \isamarkuptrue%
   1.703  %
   1.704 -\endisatagquoteme
   1.705 -{\isafoldquoteme}%
   1.706 +\endisatagquote
   1.707 +{\isafoldquote}%
   1.708  %
   1.709 -\isadelimquoteme
   1.710 +\isadelimquote
   1.711  %
   1.712 -\endisadelimquoteme
   1.713 +\endisadelimquote
   1.714  %
   1.715  \begin{isamarkuptext}%
   1.716  \noindent The whole code in SML with explicit dictionary passing:%
   1.717  \end{isamarkuptext}%
   1.718  \isamarkuptrue%
   1.719  %
   1.720 -\isadelimquoteme
   1.721 +\isadelimquote
   1.722  %
   1.723 -\endisadelimquoteme
   1.724 +\endisadelimquote
   1.725  %
   1.726 -\isatagquoteme
   1.727 +\isatagquote
   1.728  %
   1.729  \begin{isamarkuptext}%
   1.730  \isaverbatim%
   1.731 @@ -1170,12 +1240,12 @@
   1.732  \end{isamarkuptext}%
   1.733  \isamarkuptrue%
   1.734  %
   1.735 -\endisatagquoteme
   1.736 -{\isafoldquoteme}%
   1.737 +\endisatagquote
   1.738 +{\isafoldquote}%
   1.739  %
   1.740 -\isadelimquoteme
   1.741 +\isadelimquote
   1.742  %
   1.743 -\endisadelimquoteme
   1.744 +\endisadelimquote
   1.745  %
   1.746  \isadelimtheory
   1.747  %