doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
changeset 22479 de15ea8fb348
parent 22317 b550d2c6ca90
child 22550 c5039bee2602
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Mar 20 08:27:23 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Mar 20 10:23:31 2007 +0100
     1.3 @@ -5,33 +5,23 @@
     1.4  \isadelimtheory
     1.5  \isanewline
     1.6  \isanewline
     1.7 -\isanewline
     1.8  %
     1.9  \endisadelimtheory
    1.10  %
    1.11  \isatagtheory
    1.12 -\isacommand{theory}\isamarkupfalse%
    1.13 -\ Classes\isanewline
    1.14 -\isakeyword{imports}\ Main\isanewline
    1.15 -\isakeyword{begin}%
    1.16 +%
    1.17  \endisatagtheory
    1.18  {\isafoldtheory}%
    1.19  %
    1.20  \isadelimtheory
    1.21 -\isanewline
    1.22  %
    1.23  \endisadelimtheory
    1.24  %
    1.25  \isadelimML
    1.26 -\isanewline
    1.27  %
    1.28  \endisadelimML
    1.29  %
    1.30  \isatagML
    1.31 -\isacommand{ML}\isamarkupfalse%
    1.32 -\ {\isacharverbatimopen}\isanewline
    1.33 -CodegenSerializer{\isachardot}code{\isacharunderscore}width\ {\isacharcolon}{\isacharequal}\ {\isadigit{7}}{\isadigit{4}}{\isacharsemicolon}\isanewline
    1.34 -{\isacharverbatimclose}\isanewline
    1.35  %
    1.36  \endisatagML
    1.37  {\isafoldML}%
    1.38 @@ -112,7 +102,7 @@
    1.39    \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
    1.40  
    1.41    \medskip From a theoretic point of view, type classes are leightweight
    1.42 -  modules; indeed, Haskell type classes may be emulated by
    1.43 +  modules; Haskell type classes may be emulated by
    1.44    SML functors \cite{classes_modules}. 
    1.45    Isabelle/Isar offers a discipline of type classes which brings
    1.46    all those aspects together:
    1.47 @@ -155,15 +145,15 @@
    1.48  \end{isamarkuptext}%
    1.49  \isamarkuptrue%
    1.50  \ \ \ \ \isacommand{class}\isamarkupfalse%
    1.51 -\ semigroup\ {\isacharequal}\isanewline
    1.52 +\ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
    1.53  \ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
    1.54  \ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
    1.55  \begin{isamarkuptext}%
    1.56  \noindent This \isa{{\isasymCLASS}} specification consists of two
    1.57    parts: the \qn{operational} part names the class operation (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
    1.58    (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
    1.59 -  operation \isa{{\isachardoublequote}mult\ {\isacharcolon}{\isacharcolon}\ {\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
    1.60 -  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
    1.61 +  operation \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
    1.62 +  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.63  \end{isamarkuptext}%
    1.64  \isamarkuptrue%
    1.65  %
    1.66 @@ -179,7 +169,7 @@
    1.67  \isamarkuptrue%
    1.68  \ \ \ \ \isacommand{instance}\isamarkupfalse%
    1.69  \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
    1.70 -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isacharcolon}{\isacharcolon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
    1.71 +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}i\ j\ {\isasymColon}\ int{\isachardot}\ i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline
    1.72  %
    1.73  \isadelimproof
    1.74  \ \ \ \ %
    1.75 @@ -380,7 +370,7 @@
    1.76  \ {\isacharminus}\isanewline
    1.77  \ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
    1.78  \ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
    1.79 -\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isacharprime}a\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
    1.80 +\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
    1.81  \isanewline
    1.82  \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
    1.83  \ \isacommand{from}\isamarkupfalse%
    1.84 @@ -454,7 +444,7 @@
    1.85  \ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse%
    1.86  \ \isacommand{from}\isamarkupfalse%
    1.87  \ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse%
    1.88 -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isacharprime}a\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    1.89 +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
    1.90  \ simp\isanewline
    1.91  \ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse%
    1.92  \ \isacommand{show}\isamarkupfalse%
    1.93 @@ -520,7 +510,88 @@
    1.94  \isamarkuptrue%
    1.95  %
    1.96  \begin{isamarkuptext}%
    1.97 +The example above gives an impression how Isar type classes work
    1.98 +  in practice.  As stated in the introduction, classes also provide
    1.99 +  a link to Isar's locale system.  Indeed, the logical core of a class
   1.100 +  is nothing else than a locale:%
   1.101 +\end{isamarkuptext}%
   1.102 +\isamarkuptrue%
   1.103 +\isacommand{class}\isamarkupfalse%
   1.104 +\ idem\ {\isacharequal}\ type\ {\isacharplus}\isanewline
   1.105 +\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   1.106 +\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
   1.107 +\begin{isamarkuptext}%
   1.108 +\noindent essentially introduces the locale%
   1.109 +\end{isamarkuptext}%
   1.110 +\isamarkuptrue%
   1.111  %
   1.112 +\isadelimML
   1.113 +%
   1.114 +\endisadelimML
   1.115 +%
   1.116 +\isatagML
   1.117 +%
   1.118 +\endisatagML
   1.119 +{\isafoldML}%
   1.120 +%
   1.121 +\isadelimML
   1.122 +%
   1.123 +\endisadelimML
   1.124 +\isanewline
   1.125 +\isacommand{locale}\isamarkupfalse%
   1.126 +\ idem\ {\isacharequal}\isanewline
   1.127 +\ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   1.128 +\ \ \isakeyword{assumes}\ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
   1.129 +\begin{isamarkuptext}%
   1.130 +\noindent together with corresponding constant(s) and axclass%
   1.131 +\end{isamarkuptext}%
   1.132 +\isamarkuptrue%
   1.133 +\isacommand{consts}\isamarkupfalse%
   1.134 +\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   1.135 +\isanewline
   1.136 +\isacommand{axclass}\isamarkupfalse%
   1.137 +\ idem\ {\isacharless}\ type\isanewline
   1.138 +\ \ idem{\isacharcolon}\ {\isachardoublequoteopen}f\ {\isacharparenleft}f\ x{\isacharparenright}\ {\isacharequal}\ f\ x{\isachardoublequoteclose}%
   1.139 +\begin{isamarkuptext}%
   1.140 +This axclass is coupled to the locale by means of an interpretation:%
   1.141 +\end{isamarkuptext}%
   1.142 +\isamarkuptrue%
   1.143 +\isacommand{interpretation}\isamarkupfalse%
   1.144 +\ idem{\isacharunderscore}class{\isacharcolon}\isanewline
   1.145 +\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   1.146 +%
   1.147 +\isadelimproof
   1.148 +%
   1.149 +\endisadelimproof
   1.150 +%
   1.151 +\isatagproof
   1.152 +\isacommand{by}\isamarkupfalse%
   1.153 +\ unfold{\isacharunderscore}locales\ {\isacharparenleft}rule\ idem{\isacharparenright}\isanewline
   1.154 +%
   1.155 +\endisatagproof
   1.156 +{\isafoldproof}%
   1.157 +%
   1.158 +\isadelimproof
   1.159 +%
   1.160 +\endisadelimproof
   1.161 +%
   1.162 +\isadelimML
   1.163 +%
   1.164 +\endisadelimML
   1.165 +%
   1.166 +\isatagML
   1.167 +%
   1.168 +\endisatagML
   1.169 +{\isafoldML}%
   1.170 +%
   1.171 +\isadelimML
   1.172 +%
   1.173 +\endisadelimML
   1.174 +%
   1.175 +\begin{isamarkuptext}%
   1.176 +This give you at hand the full power of the Isabelle module system;
   1.177 +  conclusions in locale \isa{idem} are implicitly propagated
   1.178 +  to class \isa{idem}.%
   1.179  \end{isamarkuptext}%
   1.180  \isamarkuptrue%
   1.181  %
   1.182 @@ -529,7 +600,7 @@
   1.183  \isamarkuptrue%
   1.184  %
   1.185  \begin{isamarkuptext}%
   1.186 -Abstract theories enable reasoning at a general level, while results
   1.187 +Isabelle locales enable reasoning at a general level, while results
   1.188    are implicitly transferred to all instances.  For example, we can
   1.189    now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which
   1.190    states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:%
   1.191 @@ -547,16 +618,16 @@
   1.192  \isanewline
   1.193  \ \ \ \ \isacommand{assume}\isamarkupfalse%
   1.194  \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline
   1.195 -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.196 +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.197  \ \isacommand{have}\isamarkupfalse%
   1.198  \ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   1.199  \ simp\isanewline
   1.200 -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.201 +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.202  \ \isacommand{have}\isamarkupfalse%
   1.203  \ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
   1.204  \ assoc\ \isacommand{by}\isamarkupfalse%
   1.205  \ simp\isanewline
   1.206 -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.207 +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.208  \ \isacommand{show}\isamarkupfalse%
   1.209  \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse%
   1.210  \ neutl\ \isakeyword{and}\ invl\ \isacommand{by}\isamarkupfalse%
   1.211 @@ -565,7 +636,7 @@
   1.212  \isanewline
   1.213  \ \ \ \ \isacommand{assume}\isamarkupfalse%
   1.214  \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline
   1.215 -\ \ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.216 +\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   1.217  \ \isacommand{show}\isamarkupfalse%
   1.218  \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   1.219  \ simp\isanewline
   1.220 @@ -581,8 +652,8 @@
   1.221  \begin{isamarkuptext}%
   1.222  \noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
   1.223    indicates that the result is recorded within that context for later
   1.224 -  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isasymalpha}{\isacharcolon}{\isacharcolon}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.225 -  \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
   1.226 +  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.227 +  \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.228  \end{isamarkuptext}%
   1.229  \isamarkuptrue%
   1.230  %
   1.231 @@ -608,13 +679,13 @@
   1.232  \isamarkuptrue%
   1.233  \ \ \ \ \isacommand{fun}\isamarkupfalse%
   1.234  \isanewline
   1.235 -\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.236 +\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoidl{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.237  \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
   1.238 -\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
   1.239 +\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}\isanewline
   1.240  \isanewline
   1.241  \ \ \ \ \isacommand{definition}\isamarkupfalse%
   1.242  \isanewline
   1.243 -\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group\ {\isasymRightarrow}\ {\isacharprime}a{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.244 +\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   1.245  \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
   1.246  \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   1.247  \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\isanewline