1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/Codegen/Thy/document/Foundations.tex Fri Aug 13 14:41:12 2010 +0200
1.3 @@ -0,0 +1,1013 @@
1.4 +%
1.5 +\begin{isabellebody}%
1.6 +\def\isabellecontext{Foundations}%
1.7 +%
1.8 +\isadelimtheory
1.9 +%
1.10 +\endisadelimtheory
1.11 +%
1.12 +\isatagtheory
1.13 +\isacommand{theory}\isamarkupfalse%
1.14 +\ Foundations\isanewline
1.15 +\isakeyword{imports}\ Introduction\isanewline
1.16 +\isakeyword{begin}%
1.17 +\endisatagtheory
1.18 +{\isafoldtheory}%
1.19 +%
1.20 +\isadelimtheory
1.21 +%
1.22 +\endisadelimtheory
1.23 +%
1.24 +\isamarkupsection{Code generation foundations \label{sec:program}%
1.25 +}
1.26 +\isamarkuptrue%
1.27 +%
1.28 +\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
1.29 +}
1.30 +\isamarkuptrue%
1.31 +%
1.32 +\begin{isamarkuptext}%
1.33 +We have already seen how by default equations stemming from
1.34 + \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
1.35 + statements are used for code generation. This default behaviour
1.36 + can be changed, e.g.\ by providing different code equations.
1.37 + The customisations shown in this section are \emph{safe}
1.38 + as regards correctness: all programs that can be generated are partially
1.39 + correct.%
1.40 +\end{isamarkuptext}%
1.41 +\isamarkuptrue%
1.42 +%
1.43 +\isamarkupsubsection{Selecting code equations%
1.44 +}
1.45 +\isamarkuptrue%
1.46 +%
1.47 +\begin{isamarkuptext}%
1.48 +Coming back to our introductory example, we
1.49 + could provide an alternative code equations for \isa{dequeue}
1.50 + explicitly:%
1.51 +\end{isamarkuptext}%
1.52 +\isamarkuptrue%
1.53 +%
1.54 +\isadelimquote
1.55 +%
1.56 +\endisadelimquote
1.57 +%
1.58 +\isatagquote
1.59 +\isacommand{lemma}\isamarkupfalse%
1.60 +\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.61 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1.62 +\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
1.63 +\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.64 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
1.65 +\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.66 +\ \ \isacommand{by}\isamarkupfalse%
1.67 +\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
1.68 +\endisatagquote
1.69 +{\isafoldquote}%
1.70 +%
1.71 +\isadelimquote
1.72 +%
1.73 +\endisadelimquote
1.74 +%
1.75 +\begin{isamarkuptext}%
1.76 +\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
1.77 + \isa{attribute} which states that the given theorems should be
1.78 + considered as code equations for a \isa{fun} statement --
1.79 + the corresponding constant is determined syntactically. The resulting code:%
1.80 +\end{isamarkuptext}%
1.81 +\isamarkuptrue%
1.82 +%
1.83 +\isadelimquote
1.84 +%
1.85 +\endisadelimquote
1.86 +%
1.87 +\isatagquote
1.88 +%
1.89 +\begin{isamarkuptext}%
1.90 +\isatypewriter%
1.91 +\noindent%
1.92 +\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
1.93 +\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
1.94 +\hspace*{0pt}dequeue (AQueue xs []) =\\
1.95 +\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
1.96 +\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
1.97 +\end{isamarkuptext}%
1.98 +\isamarkuptrue%
1.99 +%
1.100 +\endisatagquote
1.101 +{\isafoldquote}%
1.102 +%
1.103 +\isadelimquote
1.104 +%
1.105 +\endisadelimquote
1.106 +%
1.107 +\begin{isamarkuptext}%
1.108 +\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
1.109 + replaced by the predicate \isa{null\ xs}. This is due to the default
1.110 + setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
1.111 +
1.112 + Changing the default constructor set of datatypes is also
1.113 + possible. See \secref{sec:datatypes} for an example.
1.114 +
1.115 + As told in \secref{sec:concept}, code generation is based
1.116 + on a structured collection of code theorems.
1.117 + This collection
1.118 + may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
1.119 +\end{isamarkuptext}%
1.120 +\isamarkuptrue%
1.121 +%
1.122 +\isadelimquote
1.123 +%
1.124 +\endisadelimquote
1.125 +%
1.126 +\isatagquote
1.127 +\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
1.128 +\ dequeue%
1.129 +\endisatagquote
1.130 +{\isafoldquote}%
1.131 +%
1.132 +\isadelimquote
1.133 +%
1.134 +\endisadelimquote
1.135 +%
1.136 +\begin{isamarkuptext}%
1.137 +\noindent prints a table with \emph{all} code equations
1.138 + for \isa{dequeue}, including
1.139 + \emph{all} code equations those equations depend
1.140 + on recursively.
1.141 +
1.142 + Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
1.143 + visualising dependencies between code equations.%
1.144 +\end{isamarkuptext}%
1.145 +\isamarkuptrue%
1.146 +%
1.147 +\isamarkupsubsection{\isa{class} and \isa{instantiation}%
1.148 +}
1.149 +\isamarkuptrue%
1.150 +%
1.151 +\begin{isamarkuptext}%
1.152 +Concerning type classes and code generation, let us examine an example
1.153 + from abstract algebra:%
1.154 +\end{isamarkuptext}%
1.155 +\isamarkuptrue%
1.156 +%
1.157 +\isadelimquote
1.158 +%
1.159 +\endisadelimquote
1.160 +%
1.161 +\isatagquote
1.162 +\isacommand{class}\isamarkupfalse%
1.163 +\ semigroup\ {\isacharequal}\isanewline
1.164 +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
1.165 +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.166 +\isanewline
1.167 +\isacommand{class}\isamarkupfalse%
1.168 +\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
1.169 +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
1.170 +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
1.171 +\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
1.172 +\isanewline
1.173 +\isacommand{instantiation}\isamarkupfalse%
1.174 +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
1.175 +\isakeyword{begin}\isanewline
1.176 +\isanewline
1.177 +\isacommand{primrec}\isamarkupfalse%
1.178 +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
1.179 +\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.180 +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
1.181 +\isanewline
1.182 +\isacommand{definition}\isamarkupfalse%
1.183 +\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
1.184 +\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
1.185 +\isanewline
1.186 +\isacommand{lemma}\isamarkupfalse%
1.187 +\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
1.188 +\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
1.189 +\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
1.190 +\ \ \isacommand{by}\isamarkupfalse%
1.191 +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
1.192 +\isanewline
1.193 +\isacommand{instance}\isamarkupfalse%
1.194 +\ \isacommand{proof}\isamarkupfalse%
1.195 +\isanewline
1.196 +\ \ \isacommand{fix}\isamarkupfalse%
1.197 +\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
1.198 +\ \ \isacommand{show}\isamarkupfalse%
1.199 +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.200 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.201 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
1.202 +\ \ \isacommand{show}\isamarkupfalse%
1.203 +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
1.204 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.205 +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
1.206 +\ \ \isacommand{show}\isamarkupfalse%
1.207 +\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
1.208 +\ \ \ \ \isacommand{by}\isamarkupfalse%
1.209 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
1.210 +\isacommand{qed}\isamarkupfalse%
1.211 +\isanewline
1.212 +\isanewline
1.213 +\isacommand{end}\isamarkupfalse%
1.214 +%
1.215 +\endisatagquote
1.216 +{\isafoldquote}%
1.217 +%
1.218 +\isadelimquote
1.219 +%
1.220 +\endisadelimquote
1.221 +%
1.222 +\begin{isamarkuptext}%
1.223 +\noindent We define the natural operation of the natural numbers
1.224 + on monoids:%
1.225 +\end{isamarkuptext}%
1.226 +\isamarkuptrue%
1.227 +%
1.228 +\isadelimquote
1.229 +%
1.230 +\endisadelimquote
1.231 +%
1.232 +\isatagquote
1.233 +\isacommand{primrec}\isamarkupfalse%
1.234 +\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.235 +\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
1.236 +\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
1.237 +\endisatagquote
1.238 +{\isafoldquote}%
1.239 +%
1.240 +\isadelimquote
1.241 +%
1.242 +\endisadelimquote
1.243 +%
1.244 +\begin{isamarkuptext}%
1.245 +\noindent This we use to define the discrete exponentiation function:%
1.246 +\end{isamarkuptext}%
1.247 +\isamarkuptrue%
1.248 +%
1.249 +\isadelimquote
1.250 +%
1.251 +\endisadelimquote
1.252 +%
1.253 +\isatagquote
1.254 +\isacommand{definition}\isamarkupfalse%
1.255 +\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.256 +\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
1.257 +\endisatagquote
1.258 +{\isafoldquote}%
1.259 +%
1.260 +\isadelimquote
1.261 +%
1.262 +\endisadelimquote
1.263 +%
1.264 +\begin{isamarkuptext}%
1.265 +\noindent The corresponding code in Haskell uses that language's native classes:%
1.266 +\end{isamarkuptext}%
1.267 +\isamarkuptrue%
1.268 +%
1.269 +\isadelimquote
1.270 +%
1.271 +\endisadelimquote
1.272 +%
1.273 +\isatagquote
1.274 +%
1.275 +\begin{isamarkuptext}%
1.276 +\isatypewriter%
1.277 +\noindent%
1.278 +\hspace*{0pt}module Example where {\char123}\\
1.279 +\hspace*{0pt}\\
1.280 +\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
1.281 +\hspace*{0pt}\\
1.282 +\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
1.283 +\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
1.284 +\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
1.285 +\hspace*{0pt}\\
1.286 +\hspace*{0pt}class Semigroup a where {\char123}\\
1.287 +\hspace*{0pt} ~mult ::~a -> a -> a;\\
1.288 +\hspace*{0pt}{\char125};\\
1.289 +\hspace*{0pt}\\
1.290 +\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
1.291 +\hspace*{0pt} ~neutral ::~a;\\
1.292 +\hspace*{0pt}{\char125};\\
1.293 +\hspace*{0pt}\\
1.294 +\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
1.295 +\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
1.296 +\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
1.297 +\hspace*{0pt}\\
1.298 +\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
1.299 +\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
1.300 +\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
1.301 +\hspace*{0pt}\\
1.302 +\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
1.303 +\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
1.304 +\hspace*{0pt}\\
1.305 +\hspace*{0pt}instance Semigroup Nat where {\char123}\\
1.306 +\hspace*{0pt} ~mult = mult{\char95}nat;\\
1.307 +\hspace*{0pt}{\char125};\\
1.308 +\hspace*{0pt}\\
1.309 +\hspace*{0pt}instance Monoid Nat where {\char123}\\
1.310 +\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
1.311 +\hspace*{0pt}{\char125};\\
1.312 +\hspace*{0pt}\\
1.313 +\hspace*{0pt}bexp ::~Nat -> Nat;\\
1.314 +\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
1.315 +\hspace*{0pt}\\
1.316 +\hspace*{0pt}{\char125}%
1.317 +\end{isamarkuptext}%
1.318 +\isamarkuptrue%
1.319 +%
1.320 +\endisatagquote
1.321 +{\isafoldquote}%
1.322 +%
1.323 +\isadelimquote
1.324 +%
1.325 +\endisadelimquote
1.326 +%
1.327 +\begin{isamarkuptext}%
1.328 +\noindent This is a convenient place to show how explicit dictionary construction
1.329 + manifests in generated code (here, the same example in \isa{SML})
1.330 + \cite{Haftmann-Nipkow:2010:code}:%
1.331 +\end{isamarkuptext}%
1.332 +\isamarkuptrue%
1.333 +%
1.334 +\isadelimquote
1.335 +%
1.336 +\endisadelimquote
1.337 +%
1.338 +\isatagquote
1.339 +%
1.340 +\begin{isamarkuptext}%
1.341 +\isatypewriter%
1.342 +\noindent%
1.343 +\hspace*{0pt}structure Example :~sig\\
1.344 +\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
1.345 +\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
1.346 +\hspace*{0pt} ~type 'a semigroup\\
1.347 +\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
1.348 +\hspace*{0pt} ~type 'a monoid\\
1.349 +\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
1.350 +\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
1.351 +\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
1.352 +\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
1.353 +\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
1.354 +\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
1.355 +\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
1.356 +\hspace*{0pt} ~val bexp :~nat -> nat\\
1.357 +\hspace*{0pt}end = struct\\
1.358 +\hspace*{0pt}\\
1.359 +\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
1.360 +\hspace*{0pt}\\
1.361 +\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
1.362 +\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
1.363 +\hspace*{0pt}\\
1.364 +\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
1.365 +\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
1.366 +\hspace*{0pt}\\
1.367 +\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
1.368 +\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
1.369 +\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
1.370 +\hspace*{0pt}\\
1.371 +\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
1.372 +\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
1.373 +\hspace*{0pt}\\
1.374 +\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
1.375 +\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
1.376 +\hspace*{0pt}\\
1.377 +\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
1.378 +\hspace*{0pt}\\
1.379 +\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
1.380 +\hspace*{0pt}\\
1.381 +\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
1.382 +\hspace*{0pt} ~:~nat monoid;\\
1.383 +\hspace*{0pt}\\
1.384 +\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
1.385 +\hspace*{0pt}\\
1.386 +\hspace*{0pt}end;~(*struct Example*)%
1.387 +\end{isamarkuptext}%
1.388 +\isamarkuptrue%
1.389 +%
1.390 +\endisatagquote
1.391 +{\isafoldquote}%
1.392 +%
1.393 +\isadelimquote
1.394 +%
1.395 +\endisadelimquote
1.396 +%
1.397 +\begin{isamarkuptext}%
1.398 +\noindent Note the parameters with trailing underscore (\verb|A_|),
1.399 + which are the dictionary parameters.%
1.400 +\end{isamarkuptext}%
1.401 +\isamarkuptrue%
1.402 +%
1.403 +\isamarkupsubsection{The preprocessor \label{sec:preproc}%
1.404 +}
1.405 +\isamarkuptrue%
1.406 +%
1.407 +\begin{isamarkuptext}%
1.408 +Before selected function theorems are turned into abstract
1.409 + code, a chain of definitional transformation steps is carried
1.410 + out: \emph{preprocessing}. In essence, the preprocessor
1.411 + consists of two components: a \emph{simpset} and \emph{function transformers}.
1.412 +
1.413 + The \emph{simpset} can apply the full generality of the
1.414 + Isabelle simplifier. Due to the interpretation of theorems as code
1.415 + equations, rewrites are applied to the right hand side and the
1.416 + arguments of the left hand side of an equation, but never to the
1.417 + constant heading the left hand side. An important special case are
1.418 + \emph{unfold theorems}, which may be declared and removed using
1.419 + the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
1.420 + attribute, respectively.
1.421 +
1.422 + Some common applications:%
1.423 +\end{isamarkuptext}%
1.424 +\isamarkuptrue%
1.425 +%
1.426 +\begin{itemize}
1.427 +%
1.428 +\begin{isamarkuptext}%
1.429 +\item replacing non-executable constructs by executable ones:%
1.430 +\end{isamarkuptext}%
1.431 +\isamarkuptrue%
1.432 +%
1.433 +\isadelimquote
1.434 +%
1.435 +\endisadelimquote
1.436 +%
1.437 +\isatagquote
1.438 +\isacommand{lemma}\isamarkupfalse%
1.439 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
1.440 +\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1.441 +\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
1.442 +\endisatagquote
1.443 +{\isafoldquote}%
1.444 +%
1.445 +\isadelimquote
1.446 +%
1.447 +\endisadelimquote
1.448 +%
1.449 +\begin{isamarkuptext}%
1.450 +\item eliminating superfluous constants:%
1.451 +\end{isamarkuptext}%
1.452 +\isamarkuptrue%
1.453 +%
1.454 +\isadelimquote
1.455 +%
1.456 +\endisadelimquote
1.457 +%
1.458 +\isatagquote
1.459 +\isacommand{lemma}\isamarkupfalse%
1.460 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
1.461 +\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1.462 +\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
1.463 +\endisatagquote
1.464 +{\isafoldquote}%
1.465 +%
1.466 +\isadelimquote
1.467 +%
1.468 +\endisadelimquote
1.469 +%
1.470 +\begin{isamarkuptext}%
1.471 +\item replacing executable but inconvenient constructs:%
1.472 +\end{isamarkuptext}%
1.473 +\isamarkuptrue%
1.474 +%
1.475 +\isadelimquote
1.476 +%
1.477 +\endisadelimquote
1.478 +%
1.479 +\isatagquote
1.480 +\isacommand{lemma}\isamarkupfalse%
1.481 +\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
1.482 +\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
1.483 +\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
1.484 +\endisatagquote
1.485 +{\isafoldquote}%
1.486 +%
1.487 +\isadelimquote
1.488 +%
1.489 +\endisadelimquote
1.490 +%
1.491 +\end{itemize}
1.492 +%
1.493 +\begin{isamarkuptext}%
1.494 +\noindent \emph{Function transformers} provide a very general interface,
1.495 + transforming a list of function theorems to another
1.496 + list of function theorems, provided that neither the heading
1.497 + constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
1.498 + pattern elimination implemented in
1.499 + theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
1.500 + interface.
1.501 +
1.502 + \noindent The current setup of the preprocessor may be inspected using
1.503 + the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
1.504 + \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
1.505 + mechanism to inspect the impact of a preprocessor setup
1.506 + on code equations.
1.507 +
1.508 + \begin{warn}
1.509 +
1.510 + Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
1.511 + preprocessor of the ancient \isa{SML\ code\ generator}; in case
1.512 + this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
1.513 + \end{warn}%
1.514 +\end{isamarkuptext}%
1.515 +\isamarkuptrue%
1.516 +%
1.517 +\isamarkupsubsection{Datatypes \label{sec:datatypes}%
1.518 +}
1.519 +\isamarkuptrue%
1.520 +%
1.521 +\begin{isamarkuptext}%
1.522 +Conceptually, any datatype is spanned by a set of
1.523 + \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
1.524 + \isa{{\isasymtau}}. The HOL datatype package by default registers any new
1.525 + datatype in the table of datatypes, which may be inspected using the
1.526 + \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
1.527 +
1.528 + In some cases, it is appropriate to alter or extend this table. As
1.529 + an example, we will develop an alternative representation of the
1.530 + queue example given in \secref{sec:intro}. The amortised
1.531 + representation is convenient for generating code but exposes its
1.532 + \qt{implementation} details, which may be cumbersome when proving
1.533 + theorems about it. Therefore, here is a simple, straightforward
1.534 + representation of queues:%
1.535 +\end{isamarkuptext}%
1.536 +\isamarkuptrue%
1.537 +%
1.538 +\isadelimquote
1.539 +%
1.540 +\endisadelimquote
1.541 +%
1.542 +\isatagquote
1.543 +\isacommand{datatype}\isamarkupfalse%
1.544 +\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
1.545 +\isanewline
1.546 +\isacommand{definition}\isamarkupfalse%
1.547 +\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.548 +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
1.549 +\isanewline
1.550 +\isacommand{primrec}\isamarkupfalse%
1.551 +\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.552 +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.553 +\isanewline
1.554 +\isacommand{fun}\isamarkupfalse%
1.555 +\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.556 +\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.557 +\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
1.558 +\endisatagquote
1.559 +{\isafoldquote}%
1.560 +%
1.561 +\isadelimquote
1.562 +%
1.563 +\endisadelimquote
1.564 +%
1.565 +\begin{isamarkuptext}%
1.566 +\noindent This we can use directly for proving; for executing,
1.567 + we provide an alternative characterisation:%
1.568 +\end{isamarkuptext}%
1.569 +\isamarkuptrue%
1.570 +%
1.571 +\isadelimquote
1.572 +%
1.573 +\endisadelimquote
1.574 +%
1.575 +\isatagquote
1.576 +\isacommand{definition}\isamarkupfalse%
1.577 +\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.578 +\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.579 +\isanewline
1.580 +\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
1.581 +\ AQueue%
1.582 +\endisatagquote
1.583 +{\isafoldquote}%
1.584 +%
1.585 +\isadelimquote
1.586 +%
1.587 +\endisadelimquote
1.588 +%
1.589 +\begin{isamarkuptext}%
1.590 +\noindent Here we define a \qt{constructor} \isa{AQueue} which
1.591 + is defined in terms of \isa{Queue} and interprets its arguments
1.592 + according to what the \emph{content} of an amortised queue is supposed
1.593 + to be. Equipped with this, we are able to prove the following equations
1.594 + for our primitive queue operations which \qt{implement} the simple
1.595 + queues in an amortised fashion:%
1.596 +\end{isamarkuptext}%
1.597 +\isamarkuptrue%
1.598 +%
1.599 +\isadelimquote
1.600 +%
1.601 +\endisadelimquote
1.602 +%
1.603 +\isatagquote
1.604 +\isacommand{lemma}\isamarkupfalse%
1.605 +\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.606 +\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
1.607 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.608 +\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.609 +\ simp\isanewline
1.610 +\isanewline
1.611 +\isacommand{lemma}\isamarkupfalse%
1.612 +\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.613 +\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
1.614 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.615 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.616 +\ simp\isanewline
1.617 +\isanewline
1.618 +\isacommand{lemma}\isamarkupfalse%
1.619 +\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.620 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1.621 +\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
1.622 +\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.623 +\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.624 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.625 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.626 +\ simp{\isacharunderscore}all%
1.627 +\endisatagquote
1.628 +{\isafoldquote}%
1.629 +%
1.630 +\isadelimquote
1.631 +%
1.632 +\endisadelimquote
1.633 +%
1.634 +\begin{isamarkuptext}%
1.635 +\noindent For completeness, we provide a substitute for the
1.636 + \isa{case} combinator on queues:%
1.637 +\end{isamarkuptext}%
1.638 +\isamarkuptrue%
1.639 +%
1.640 +\isadelimquote
1.641 +%
1.642 +\endisadelimquote
1.643 +%
1.644 +\isatagquote
1.645 +\isacommand{lemma}\isamarkupfalse%
1.646 +\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.647 +\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.648 +\ \ \isacommand{unfolding}\isamarkupfalse%
1.649 +\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
1.650 +\ simp%
1.651 +\endisatagquote
1.652 +{\isafoldquote}%
1.653 +%
1.654 +\isadelimquote
1.655 +%
1.656 +\endisadelimquote
1.657 +%
1.658 +\begin{isamarkuptext}%
1.659 +\noindent The resulting code looks as expected:%
1.660 +\end{isamarkuptext}%
1.661 +\isamarkuptrue%
1.662 +%
1.663 +\isadelimquote
1.664 +%
1.665 +\endisadelimquote
1.666 +%
1.667 +\isatagquote
1.668 +%
1.669 +\begin{isamarkuptext}%
1.670 +\isatypewriter%
1.671 +\noindent%
1.672 +\hspace*{0pt}structure Example :~sig\\
1.673 +\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
1.674 +\hspace*{0pt} ~val rev :~'a list -> 'a list\\
1.675 +\hspace*{0pt} ~val null :~'a list -> bool\\
1.676 +\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
1.677 +\hspace*{0pt} ~val empty :~'a queue\\
1.678 +\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
1.679 +\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
1.680 +\hspace*{0pt}end = struct\\
1.681 +\hspace*{0pt}\\
1.682 +\hspace*{0pt}fun foldl f a [] = a\\
1.683 +\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
1.684 +\hspace*{0pt}\\
1.685 +\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
1.686 +\hspace*{0pt}\\
1.687 +\hspace*{0pt}fun null [] = true\\
1.688 +\hspace*{0pt} ~| null (x ::~xs) = false;\\
1.689 +\hspace*{0pt}\\
1.690 +\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
1.691 +\hspace*{0pt}\\
1.692 +\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
1.693 +\hspace*{0pt}\\
1.694 +\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
1.695 +\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
1.696 +\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
1.697 +\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
1.698 +\hspace*{0pt}\\
1.699 +\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
1.700 +\hspace*{0pt}\\
1.701 +\hspace*{0pt}end;~(*struct Example*)%
1.702 +\end{isamarkuptext}%
1.703 +\isamarkuptrue%
1.704 +%
1.705 +\endisatagquote
1.706 +{\isafoldquote}%
1.707 +%
1.708 +\isadelimquote
1.709 +%
1.710 +\endisadelimquote
1.711 +%
1.712 +\begin{isamarkuptext}%
1.713 +\noindent From this example, it can be glimpsed that using own
1.714 + constructor sets is a little delicate since it changes the set of
1.715 + valid patterns for values of that type. Without going into much
1.716 + detail, here some practical hints:
1.717 +
1.718 + \begin{itemize}
1.719 +
1.720 + \item When changing the constructor set for datatypes, take care
1.721 + to provide alternative equations for the \isa{case} combinator.
1.722 +
1.723 + \item Values in the target language need not to be normalised --
1.724 + different values in the target language may represent the same
1.725 + value in the logic.
1.726 +
1.727 + \item Usually, a good methodology to deal with the subtleties of
1.728 + pattern matching is to see the type as an abstract type: provide
1.729 + a set of operations which operate on the concrete representation
1.730 + of the type, and derive further operations by combinations of
1.731 + these primitive ones, without relying on a particular
1.732 + representation.
1.733 +
1.734 + \end{itemize}%
1.735 +\end{isamarkuptext}%
1.736 +\isamarkuptrue%
1.737 +%
1.738 +\isamarkupsubsection{Equality%
1.739 +}
1.740 +\isamarkuptrue%
1.741 +%
1.742 +\begin{isamarkuptext}%
1.743 +Surely you have already noticed how equality is treated
1.744 + by the code generator:%
1.745 +\end{isamarkuptext}%
1.746 +\isamarkuptrue%
1.747 +%
1.748 +\isadelimquote
1.749 +%
1.750 +\endisadelimquote
1.751 +%
1.752 +\isatagquote
1.753 +\isacommand{primrec}\isamarkupfalse%
1.754 +\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.755 +\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
1.756 +\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
1.757 +\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
1.758 +\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
1.759 +\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
1.760 +\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
1.761 +\endisatagquote
1.762 +{\isafoldquote}%
1.763 +%
1.764 +\isadelimquote
1.765 +%
1.766 +\endisadelimquote
1.767 +%
1.768 +\begin{isamarkuptext}%
1.769 +\noindent During preprocessing, the membership test is rewritten,
1.770 + resulting in \isa{List{\isachardot}member}, which itself
1.771 + performs an explicit equality check.%
1.772 +\end{isamarkuptext}%
1.773 +\isamarkuptrue%
1.774 +%
1.775 +\isadelimquote
1.776 +%
1.777 +\endisadelimquote
1.778 +%
1.779 +\isatagquote
1.780 +%
1.781 +\begin{isamarkuptext}%
1.782 +\isatypewriter%
1.783 +\noindent%
1.784 +\hspace*{0pt}structure Example :~sig\\
1.785 +\hspace*{0pt} ~type 'a eq\\
1.786 +\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
1.787 +\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
1.788 +\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
1.789 +\hspace*{0pt} ~val collect{\char95}duplicates :\\
1.790 +\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
1.791 +\hspace*{0pt}end = struct\\
1.792 +\hspace*{0pt}\\
1.793 +\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
1.794 +\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
1.795 +\hspace*{0pt}\\
1.796 +\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
1.797 +\hspace*{0pt}\\
1.798 +\hspace*{0pt}fun member A{\char95}~[] y = false\\
1.799 +\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
1.800 +\hspace*{0pt}\\
1.801 +\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
1.802 +\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
1.803 +\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
1.804 +\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
1.805 +\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
1.806 +\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
1.807 +\hspace*{0pt}\\
1.808 +\hspace*{0pt}end;~(*struct Example*)%
1.809 +\end{isamarkuptext}%
1.810 +\isamarkuptrue%
1.811 +%
1.812 +\endisatagquote
1.813 +{\isafoldquote}%
1.814 +%
1.815 +\isadelimquote
1.816 +%
1.817 +\endisadelimquote
1.818 +%
1.819 +\begin{isamarkuptext}%
1.820 +\noindent Obviously, polymorphic equality is implemented the Haskell
1.821 + way using a type class. How is this achieved? HOL introduces
1.822 + an explicit class \isa{eq} with a corresponding operation
1.823 + \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
1.824 + The preprocessing framework does the rest by propagating the
1.825 + \isa{eq} constraints through all dependent code equations.
1.826 + For datatypes, instances of \isa{eq} are implicitly derived
1.827 + when possible. For other types, you may instantiate \isa{eq}
1.828 + manually like any other type class.%
1.829 +\end{isamarkuptext}%
1.830 +\isamarkuptrue%
1.831 +%
1.832 +\isamarkupsubsection{Explicit partiality%
1.833 +}
1.834 +\isamarkuptrue%
1.835 +%
1.836 +\begin{isamarkuptext}%
1.837 +Partiality usually enters the game by partial patterns, as
1.838 + in the following example, again for amortised queues:%
1.839 +\end{isamarkuptext}%
1.840 +\isamarkuptrue%
1.841 +%
1.842 +\isadelimquote
1.843 +%
1.844 +\endisadelimquote
1.845 +%
1.846 +\isatagquote
1.847 +\isacommand{definition}\isamarkupfalse%
1.848 +\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.849 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
1.850 +\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.851 +\isanewline
1.852 +\isacommand{lemma}\isamarkupfalse%
1.853 +\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.854 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.855 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
1.856 +\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.857 +\ \ \isacommand{by}\isamarkupfalse%
1.858 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
1.859 +\endisatagquote
1.860 +{\isafoldquote}%
1.861 +%
1.862 +\isadelimquote
1.863 +%
1.864 +\endisadelimquote
1.865 +%
1.866 +\begin{isamarkuptext}%
1.867 +\noindent In the corresponding code, there is no equation
1.868 + for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
1.869 +\end{isamarkuptext}%
1.870 +\isamarkuptrue%
1.871 +%
1.872 +\isadelimquote
1.873 +%
1.874 +\endisadelimquote
1.875 +%
1.876 +\isatagquote
1.877 +%
1.878 +\begin{isamarkuptext}%
1.879 +\isatypewriter%
1.880 +\noindent%
1.881 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
1.882 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
1.883 +\hspace*{0pt} ~let {\char123}\\
1.884 +\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
1.885 +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
1.886 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
1.887 +\end{isamarkuptext}%
1.888 +\isamarkuptrue%
1.889 +%
1.890 +\endisatagquote
1.891 +{\isafoldquote}%
1.892 +%
1.893 +\isadelimquote
1.894 +%
1.895 +\endisadelimquote
1.896 +%
1.897 +\begin{isamarkuptext}%
1.898 +\noindent In some cases it is desirable to have this
1.899 + pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
1.900 +\end{isamarkuptext}%
1.901 +\isamarkuptrue%
1.902 +%
1.903 +\isadelimquote
1.904 +%
1.905 +\endisadelimquote
1.906 +%
1.907 +\isatagquote
1.908 +\isacommand{axiomatization}\isamarkupfalse%
1.909 +\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
1.910 +\isanewline
1.911 +\isacommand{definition}\isamarkupfalse%
1.912 +\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
1.913 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.914 +\isanewline
1.915 +\isacommand{lemma}\isamarkupfalse%
1.916 +\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
1.917 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
1.918 +\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.919 +\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
1.920 +\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
1.921 +\ \ \isacommand{by}\isamarkupfalse%
1.922 +\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
1.923 +\endisatagquote
1.924 +{\isafoldquote}%
1.925 +%
1.926 +\isadelimquote
1.927 +%
1.928 +\endisadelimquote
1.929 +%
1.930 +\begin{isamarkuptext}%
1.931 +Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
1.932 +
1.933 + Normally, if constants without any code equations occur in a
1.934 + program, the code generator complains (since in most cases this is
1.935 + indeed an error). But such constants can also be thought
1.936 + of as function definitions which always fail,
1.937 + since there is never a successful pattern match on the left hand
1.938 + side. In order to categorise a constant into that category
1.939 + explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
1.940 +\end{isamarkuptext}%
1.941 +\isamarkuptrue%
1.942 +%
1.943 +\isadelimquote
1.944 +%
1.945 +\endisadelimquote
1.946 +%
1.947 +\isatagquote
1.948 +\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
1.949 +\ empty{\isacharunderscore}queue%
1.950 +\endisatagquote
1.951 +{\isafoldquote}%
1.952 +%
1.953 +\isadelimquote
1.954 +%
1.955 +\endisadelimquote
1.956 +%
1.957 +\begin{isamarkuptext}%
1.958 +\noindent Then the code generator will just insert an error or
1.959 + exception at the appropriate position:%
1.960 +\end{isamarkuptext}%
1.961 +\isamarkuptrue%
1.962 +%
1.963 +\isadelimquote
1.964 +%
1.965 +\endisadelimquote
1.966 +%
1.967 +\isatagquote
1.968 +%
1.969 +\begin{isamarkuptext}%
1.970 +\isatypewriter%
1.971 +\noindent%
1.972 +\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
1.973 +\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
1.974 +\hspace*{0pt}\\
1.975 +\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
1.976 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
1.977 +\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
1.978 +\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
1.979 +\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
1.980 +\end{isamarkuptext}%
1.981 +\isamarkuptrue%
1.982 +%
1.983 +\endisatagquote
1.984 +{\isafoldquote}%
1.985 +%
1.986 +\isadelimquote
1.987 +%
1.988 +\endisadelimquote
1.989 +%
1.990 +\begin{isamarkuptext}%
1.991 +\noindent This feature however is rarely needed in practice.
1.992 + Note also that the \isa{HOL} default setup already declares
1.993 + \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
1.994 + likely to be used in such situations.%
1.995 +\end{isamarkuptext}%
1.996 +\isamarkuptrue%
1.997 +%
1.998 +\isadelimtheory
1.999 +%
1.1000 +\endisadelimtheory
1.1001 +%
1.1002 +\isatagtheory
1.1003 +\isacommand{end}\isamarkupfalse%
1.1004 +%
1.1005 +\endisatagtheory
1.1006 +{\isafoldtheory}%
1.1007 +%
1.1008 +\isadelimtheory
1.1009 +%
1.1010 +\endisadelimtheory
1.1011 +\isanewline
1.1012 +\end{isabellebody}%
1.1013 +%%% Local Variables:
1.1014 +%%% mode: latex
1.1015 +%%% TeX-master: "root"
1.1016 +%%% End:
2.1 --- a/doc-src/Codegen/Thy/document/ML.tex Fri Aug 13 14:40:15 2010 +0200
2.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
2.3 @@ -1,240 +0,0 @@
2.4 -%
2.5 -\begin{isabellebody}%
2.6 -\def\isabellecontext{ML}%
2.7 -%
2.8 -\isadelimtheory
2.9 -%
2.10 -\endisadelimtheory
2.11 -%
2.12 -\isatagtheory
2.13 -\isacommand{theory}\isamarkupfalse%
2.14 -\ {\isachardoublequoteopen}ML{\isachardoublequoteclose}\isanewline
2.15 -\isakeyword{imports}\ Setup\isanewline
2.16 -\isakeyword{begin}%
2.17 -\endisatagtheory
2.18 -{\isafoldtheory}%
2.19 -%
2.20 -\isadelimtheory
2.21 -%
2.22 -\endisadelimtheory
2.23 -%
2.24 -\isamarkupsection{ML system interfaces \label{sec:ml}%
2.25 -}
2.26 -\isamarkuptrue%
2.27 -%
2.28 -\begin{isamarkuptext}%
2.29 -Since the code generator framework not only aims to provide
2.30 - a nice Isar interface but also to form a base for
2.31 - code-generation-based applications, here a short
2.32 - description of the most important ML interfaces.%
2.33 -\end{isamarkuptext}%
2.34 -\isamarkuptrue%
2.35 -%
2.36 -\isamarkupsubsection{Executable theory content: \isa{Code}%
2.37 -}
2.38 -\isamarkuptrue%
2.39 -%
2.40 -\begin{isamarkuptext}%
2.41 -This Pure module implements the core notions of
2.42 - executable content of a theory.%
2.43 -\end{isamarkuptext}%
2.44 -\isamarkuptrue%
2.45 -%
2.46 -\isamarkupsubsubsection{Managing executable content%
2.47 -}
2.48 -\isamarkuptrue%
2.49 -%
2.50 -\isadelimmlref
2.51 -%
2.52 -\endisadelimmlref
2.53 -%
2.54 -\isatagmlref
2.55 -%
2.56 -\begin{isamarkuptext}%
2.57 -\begin{mldecls}
2.58 - \indexdef{}{ML}{Code.add\_eqn}\verb|Code.add_eqn: thm -> theory -> theory| \\
2.59 - \indexdef{}{ML}{Code.del\_eqn}\verb|Code.del_eqn: thm -> theory -> theory| \\
2.60 - \indexdef{}{ML}{Code\_Preproc.map\_pre}\verb|Code_Preproc.map_pre: (simpset -> simpset) -> theory -> theory| \\
2.61 - \indexdef{}{ML}{Code\_Preproc.map\_post}\verb|Code_Preproc.map_post: (simpset -> simpset) -> theory -> theory| \\
2.62 - \indexdef{}{ML}{Code\_Preproc.add\_functrans}\verb|Code_Preproc.add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option)|\isasep\isanewline%
2.63 -\verb| -> theory -> theory| \\
2.64 - \indexdef{}{ML}{Code\_Preproc.del\_functrans}\verb|Code_Preproc.del_functrans: string -> theory -> theory| \\
2.65 - \indexdef{}{ML}{Code.add\_datatype}\verb|Code.add_datatype: (string * typ) list -> theory -> theory| \\
2.66 - \indexdef{}{ML}{Code.get\_type}\verb|Code.get_type: theory -> string|\isasep\isanewline%
2.67 -\verb| -> (string * sort) list * ((string * string list) * typ list) list| \\
2.68 - \indexdef{}{ML}{Code.get\_type\_of\_constr\_or\_abstr}\verb|Code.get_type_of_constr_or_abstr: theory -> string -> (string * bool) option|
2.69 - \end{mldecls}
2.70 -
2.71 - \begin{description}
2.72 -
2.73 - \item \verb|Code.add_eqn|~\isa{thm}~\isa{thy} adds function
2.74 - theorem \isa{thm} to executable content.
2.75 -
2.76 - \item \verb|Code.del_eqn|~\isa{thm}~\isa{thy} removes function
2.77 - theorem \isa{thm} from executable content, if present.
2.78 -
2.79 - \item \verb|Code_Preproc.map_pre|~\isa{f}~\isa{thy} changes
2.80 - the preprocessor simpset.
2.81 -
2.82 - \item \verb|Code_Preproc.add_functrans|~\isa{{\isacharparenleft}name{\isacharcomma}\ f{\isacharparenright}}~\isa{thy} adds
2.83 - function transformer \isa{f} (named \isa{name}) to executable content;
2.84 - \isa{f} is a transformer of the code equations belonging
2.85 - to a certain function definition, depending on the
2.86 - current theory context. Returning \isa{NONE} indicates that no
2.87 - transformation took place; otherwise, the whole process will be iterated
2.88 - with the new code equations.
2.89 -
2.90 - \item \verb|Code_Preproc.del_functrans|~\isa{name}~\isa{thy} removes
2.91 - function transformer named \isa{name} from executable content.
2.92 -
2.93 - \item \verb|Code.add_datatype|~\isa{cs}~\isa{thy} adds
2.94 - a datatype to executable content, with generation
2.95 - set \isa{cs}.
2.96 -
2.97 - \item \verb|Code.get_type_of_constr_or_abstr|~\isa{thy}~\isa{const}
2.98 - returns type constructor corresponding to
2.99 - constructor \isa{const}; returns \isa{NONE}
2.100 - if \isa{const} is no constructor.
2.101 -
2.102 - \end{description}%
2.103 -\end{isamarkuptext}%
2.104 -\isamarkuptrue%
2.105 -%
2.106 -\endisatagmlref
2.107 -{\isafoldmlref}%
2.108 -%
2.109 -\isadelimmlref
2.110 -%
2.111 -\endisadelimmlref
2.112 -%
2.113 -\isamarkupsubsection{Auxiliary%
2.114 -}
2.115 -\isamarkuptrue%
2.116 -%
2.117 -\isadelimmlref
2.118 -%
2.119 -\endisadelimmlref
2.120 -%
2.121 -\isatagmlref
2.122 -%
2.123 -\begin{isamarkuptext}%
2.124 -\begin{mldecls}
2.125 - \indexdef{}{ML}{Code.read\_const}\verb|Code.read_const: theory -> string -> string|
2.126 - \end{mldecls}
2.127 -
2.128 - \begin{description}
2.129 -
2.130 - \item \verb|Code.read_const|~\isa{thy}~\isa{s}
2.131 - reads a constant as a concrete term expression \isa{s}.
2.132 -
2.133 - \end{description}%
2.134 -\end{isamarkuptext}%
2.135 -\isamarkuptrue%
2.136 -%
2.137 -\endisatagmlref
2.138 -{\isafoldmlref}%
2.139 -%
2.140 -\isadelimmlref
2.141 -%
2.142 -\endisadelimmlref
2.143 -%
2.144 -\isamarkupsubsection{Implementing code generator applications%
2.145 -}
2.146 -\isamarkuptrue%
2.147 -%
2.148 -\begin{isamarkuptext}%
2.149 -Implementing code generator applications on top
2.150 - of the framework set out so far usually not only
2.151 - involves using those primitive interfaces
2.152 - but also storing code-dependent data and various
2.153 - other things.%
2.154 -\end{isamarkuptext}%
2.155 -\isamarkuptrue%
2.156 -%
2.157 -\isamarkupsubsubsection{Data depending on the theory's executable content%
2.158 -}
2.159 -\isamarkuptrue%
2.160 -%
2.161 -\begin{isamarkuptext}%
2.162 -Due to incrementality of code generation, changes in the
2.163 - theory's executable content have to be propagated in a
2.164 - certain fashion. Additionally, such changes may occur
2.165 - not only during theory extension but also during theory
2.166 - merge, which is a little bit nasty from an implementation
2.167 - point of view. The framework provides a solution
2.168 - to this technical challenge by providing a functorial
2.169 - data slot \verb|Code_Data|; on instantiation
2.170 - of this functor, the following types and operations
2.171 - are required:
2.172 -
2.173 - \medskip
2.174 - \begin{tabular}{l}
2.175 - \isa{type\ T} \\
2.176 - \isa{val\ empty{\isacharcolon}\ T} \\
2.177 - \isa{val\ purge{\isacharcolon}\ theory\ {\isasymrightarrow}\ string\ list\ option\ {\isasymrightarrow}\ T\ {\isasymrightarrow}\ T}
2.178 - \end{tabular}
2.179 -
2.180 - \begin{description}
2.181 -
2.182 - \item \isa{T} the type of data to store.
2.183 -
2.184 - \item \isa{empty} initial (empty) data.
2.185 -
2.186 - \item \isa{purge}~\isa{thy}~\isa{consts} propagates changes in executable content;
2.187 - \isa{consts} indicates the kind
2.188 - of change: \verb|NONE| stands for a fundamental change
2.189 - which invalidates any existing code, \isa{SOME\ consts}
2.190 - hints that executable content for constants \isa{consts}
2.191 - has changed.
2.192 -
2.193 - \end{description}
2.194 -
2.195 - \noindent An instance of \verb|Code_Data| provides the following
2.196 - interface:
2.197 -
2.198 - \medskip
2.199 - \begin{tabular}{l}
2.200 - \isa{get{\isacharcolon}\ theory\ {\isasymrightarrow}\ T} \\
2.201 - \isa{change{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ T{\isacharparenright}\ {\isasymrightarrow}\ T} \\
2.202 - \isa{change{\isacharunderscore}yield{\isacharcolon}\ theory\ {\isasymrightarrow}\ {\isacharparenleft}T\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T{\isacharparenright}\ {\isasymrightarrow}\ {\isacharprime}a\ {\isacharasterisk}\ T}
2.203 - \end{tabular}
2.204 -
2.205 - \begin{description}
2.206 -
2.207 - \item \isa{get} retrieval of the current data.
2.208 -
2.209 - \item \isa{change} update of current data (cached!)
2.210 - by giving a continuation.
2.211 -
2.212 - \item \isa{change{\isacharunderscore}yield} update with side result.
2.213 -
2.214 - \end{description}%
2.215 -\end{isamarkuptext}%
2.216 -\isamarkuptrue%
2.217 -%
2.218 -\begin{isamarkuptext}%
2.219 -\bigskip
2.220 -
2.221 - \emph{Happy proving, happy hacking!}%
2.222 -\end{isamarkuptext}%
2.223 -\isamarkuptrue%
2.224 -%
2.225 -\isadelimtheory
2.226 -%
2.227 -\endisadelimtheory
2.228 -%
2.229 -\isatagtheory
2.230 -\isacommand{end}\isamarkupfalse%
2.231 -%
2.232 -\endisatagtheory
2.233 -{\isafoldtheory}%
2.234 -%
2.235 -\isadelimtheory
2.236 -%
2.237 -\endisadelimtheory
2.238 -\isanewline
2.239 -\end{isabellebody}%
2.240 -%%% Local Variables:
2.241 -%%% mode: latex
2.242 -%%% TeX-master: "root"
2.243 -%%% End:
3.1 --- a/doc-src/Codegen/Thy/document/Program.tex Fri Aug 13 14:40:15 2010 +0200
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,1013 +0,0 @@
3.4 -%
3.5 -\begin{isabellebody}%
3.6 -\def\isabellecontext{Program}%
3.7 -%
3.8 -\isadelimtheory
3.9 -%
3.10 -\endisadelimtheory
3.11 -%
3.12 -\isatagtheory
3.13 -\isacommand{theory}\isamarkupfalse%
3.14 -\ Program\isanewline
3.15 -\isakeyword{imports}\ Introduction\isanewline
3.16 -\isakeyword{begin}%
3.17 -\endisatagtheory
3.18 -{\isafoldtheory}%
3.19 -%
3.20 -\isadelimtheory
3.21 -%
3.22 -\endisadelimtheory
3.23 -%
3.24 -\isamarkupsection{Turning Theories into Programs \label{sec:program}%
3.25 -}
3.26 -\isamarkuptrue%
3.27 -%
3.28 -\isamarkupsubsection{The \isa{Isabelle{\isacharslash}HOL} default setup%
3.29 -}
3.30 -\isamarkuptrue%
3.31 -%
3.32 -\begin{isamarkuptext}%
3.33 -We have already seen how by default equations stemming from
3.34 - \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}, \hyperlink{command.primrec}{\mbox{\isa{\isacommand{primrec}}}} and \hyperlink{command.fun}{\mbox{\isa{\isacommand{fun}}}}
3.35 - statements are used for code generation. This default behaviour
3.36 - can be changed, e.g.\ by providing different code equations.
3.37 - The customisations shown in this section are \emph{safe}
3.38 - as regards correctness: all programs that can be generated are partially
3.39 - correct.%
3.40 -\end{isamarkuptext}%
3.41 -\isamarkuptrue%
3.42 -%
3.43 -\isamarkupsubsection{Selecting code equations%
3.44 -}
3.45 -\isamarkuptrue%
3.46 -%
3.47 -\begin{isamarkuptext}%
3.48 -Coming back to our introductory example, we
3.49 - could provide an alternative code equations for \isa{dequeue}
3.50 - explicitly:%
3.51 -\end{isamarkuptext}%
3.52 -\isamarkuptrue%
3.53 -%
3.54 -\isadelimquote
3.55 -%
3.56 -\endisadelimquote
3.57 -%
3.58 -\isatagquote
3.59 -\isacommand{lemma}\isamarkupfalse%
3.60 -\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.61 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
3.62 -\ \ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
3.63 -\ \ \ \ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.64 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
3.65 -\ \ \ \ \ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.66 -\ \ \isacommand{by}\isamarkupfalse%
3.67 -\ {\isacharparenleft}cases\ xs{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\ {\isacharparenleft}cases\ {\isachardoublequoteopen}rev\ xs{\isachardoublequoteclose}{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}%
3.68 -\endisatagquote
3.69 -{\isafoldquote}%
3.70 -%
3.71 -\isadelimquote
3.72 -%
3.73 -\endisadelimquote
3.74 -%
3.75 -\begin{isamarkuptext}%
3.76 -\noindent The annotation \isa{{\isacharbrackleft}code{\isacharbrackright}} is an \isa{Isar}
3.77 - \isa{attribute} which states that the given theorems should be
3.78 - considered as code equations for a \isa{fun} statement --
3.79 - the corresponding constant is determined syntactically. The resulting code:%
3.80 -\end{isamarkuptext}%
3.81 -\isamarkuptrue%
3.82 -%
3.83 -\isadelimquote
3.84 -%
3.85 -\endisadelimquote
3.86 -%
3.87 -\isatagquote
3.88 -%
3.89 -\begin{isamarkuptext}%
3.90 -\isatypewriter%
3.91 -\noindent%
3.92 -\hspace*{0pt}dequeue ::~forall a.~Queue a -> (Maybe a,~Queue a);\\
3.93 -\hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
3.94 -\hspace*{0pt}dequeue (AQueue xs []) =\\
3.95 -\hspace*{0pt} ~(if null xs then (Nothing,~AQueue [] [])\\
3.96 -\hspace*{0pt} ~~~else dequeue (AQueue [] (reverse xs)));%
3.97 -\end{isamarkuptext}%
3.98 -\isamarkuptrue%
3.99 -%
3.100 -\endisatagquote
3.101 -{\isafoldquote}%
3.102 -%
3.103 -\isadelimquote
3.104 -%
3.105 -\endisadelimquote
3.106 -%
3.107 -\begin{isamarkuptext}%
3.108 -\noindent You may note that the equality test \isa{xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}} has been
3.109 - replaced by the predicate \isa{null\ xs}. This is due to the default
3.110 - setup in the \qn{preprocessor} to be discussed further below (\secref{sec:preproc}).
3.111 -
3.112 - Changing the default constructor set of datatypes is also
3.113 - possible. See \secref{sec:datatypes} for an example.
3.114 -
3.115 - As told in \secref{sec:concept}, code generation is based
3.116 - on a structured collection of code theorems.
3.117 - This collection
3.118 - may be inspected using the \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} command:%
3.119 -\end{isamarkuptext}%
3.120 -\isamarkuptrue%
3.121 -%
3.122 -\isadelimquote
3.123 -%
3.124 -\endisadelimquote
3.125 -%
3.126 -\isatagquote
3.127 -\isacommand{code{\isacharunderscore}thms}\isamarkupfalse%
3.128 -\ dequeue%
3.129 -\endisatagquote
3.130 -{\isafoldquote}%
3.131 -%
3.132 -\isadelimquote
3.133 -%
3.134 -\endisadelimquote
3.135 -%
3.136 -\begin{isamarkuptext}%
3.137 -\noindent prints a table with \emph{all} code equations
3.138 - for \isa{dequeue}, including
3.139 - \emph{all} code equations those equations depend
3.140 - on recursively.
3.141 -
3.142 - Similarly, the \hyperlink{command.code-deps}{\mbox{\isa{\isacommand{code{\isacharunderscore}deps}}}} command shows a graph
3.143 - visualising dependencies between code equations.%
3.144 -\end{isamarkuptext}%
3.145 -\isamarkuptrue%
3.146 -%
3.147 -\isamarkupsubsection{\isa{class} and \isa{instantiation}%
3.148 -}
3.149 -\isamarkuptrue%
3.150 -%
3.151 -\begin{isamarkuptext}%
3.152 -Concerning type classes and code generation, let us examine an example
3.153 - from abstract algebra:%
3.154 -\end{isamarkuptext}%
3.155 -\isamarkuptrue%
3.156 -%
3.157 -\isadelimquote
3.158 -%
3.159 -\endisadelimquote
3.160 -%
3.161 -\isatagquote
3.162 -\isacommand{class}\isamarkupfalse%
3.163 -\ semigroup\ {\isacharequal}\isanewline
3.164 -\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
3.165 -\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.166 -\isanewline
3.167 -\isacommand{class}\isamarkupfalse%
3.168 -\ monoid\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
3.169 -\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
3.170 -\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
3.171 -\ \ \ \ \isakeyword{and}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline
3.172 -\isanewline
3.173 -\isacommand{instantiation}\isamarkupfalse%
3.174 -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline
3.175 -\isakeyword{begin}\isanewline
3.176 -\isanewline
3.177 -\isacommand{primrec}\isamarkupfalse%
3.178 -\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
3.179 -\ \ \ \ {\isachardoublequoteopen}{\isadigit{0}}\ {\isasymotimes}\ n\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.180 -\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ n\ {\isacharplus}\ m\ {\isasymotimes}\ n{\isachardoublequoteclose}\isanewline
3.181 -\isanewline
3.182 -\isacommand{definition}\isamarkupfalse%
3.183 -\ neutral{\isacharunderscore}nat\ \isakeyword{where}\isanewline
3.184 -\ \ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline
3.185 -\isanewline
3.186 -\isacommand{lemma}\isamarkupfalse%
3.187 -\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharcolon}\isanewline
3.188 -\ \ \isakeyword{fixes}\ n\ m\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
3.189 -\ \ \isakeyword{shows}\ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharplus}\ m{\isacharparenright}\ {\isasymotimes}\ q\ {\isacharequal}\ n\ {\isasymotimes}\ q\ {\isacharplus}\ m\ {\isasymotimes}\ q{\isachardoublequoteclose}\isanewline
3.190 -\ \ \isacommand{by}\isamarkupfalse%
3.191 -\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
3.192 -\isanewline
3.193 -\isacommand{instance}\isamarkupfalse%
3.194 -\ \isacommand{proof}\isamarkupfalse%
3.195 -\isanewline
3.196 -\ \ \isacommand{fix}\isamarkupfalse%
3.197 -\ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
3.198 -\ \ \isacommand{show}\isamarkupfalse%
3.199 -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.200 -\ \ \ \ \isacommand{by}\isamarkupfalse%
3.201 -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ add{\isacharunderscore}mult{\isacharunderscore}distrib{\isacharparenright}\isanewline
3.202 -\ \ \isacommand{show}\isamarkupfalse%
3.203 -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
3.204 -\ \ \ \ \isacommand{by}\isamarkupfalse%
3.205 -\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
3.206 -\ \ \isacommand{show}\isamarkupfalse%
3.207 -\ {\isachardoublequoteopen}m\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ m{\isachardoublequoteclose}\isanewline
3.208 -\ \ \ \ \isacommand{by}\isamarkupfalse%
3.209 -\ {\isacharparenleft}induct\ m{\isacharparenright}\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}\isanewline
3.210 -\isacommand{qed}\isamarkupfalse%
3.211 -\isanewline
3.212 -\isanewline
3.213 -\isacommand{end}\isamarkupfalse%
3.214 -%
3.215 -\endisatagquote
3.216 -{\isafoldquote}%
3.217 -%
3.218 -\isadelimquote
3.219 -%
3.220 -\endisadelimquote
3.221 -%
3.222 -\begin{isamarkuptext}%
3.223 -\noindent We define the natural operation of the natural numbers
3.224 - on monoids:%
3.225 -\end{isamarkuptext}%
3.226 -\isamarkuptrue%
3.227 -%
3.228 -\isadelimquote
3.229 -%
3.230 -\endisadelimquote
3.231 -%
3.232 -\isatagquote
3.233 -\isacommand{primrec}\isamarkupfalse%
3.234 -\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.235 -\ \ \ \ {\isachardoublequoteopen}pow\ {\isadigit{0}}\ a\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
3.236 -\ \ {\isacharbar}\ {\isachardoublequoteopen}pow\ {\isacharparenleft}Suc\ n{\isacharparenright}\ a\ {\isacharequal}\ a\ {\isasymotimes}\ pow\ n\ a{\isachardoublequoteclose}%
3.237 -\endisatagquote
3.238 -{\isafoldquote}%
3.239 -%
3.240 -\isadelimquote
3.241 -%
3.242 -\endisadelimquote
3.243 -%
3.244 -\begin{isamarkuptext}%
3.245 -\noindent This we use to define the discrete exponentiation function:%
3.246 -\end{isamarkuptext}%
3.247 -\isamarkuptrue%
3.248 -%
3.249 -\isadelimquote
3.250 -%
3.251 -\endisadelimquote
3.252 -%
3.253 -\isatagquote
3.254 -\isacommand{definition}\isamarkupfalse%
3.255 -\ bexp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.256 -\ \ {\isachardoublequoteopen}bexp\ n\ {\isacharequal}\ pow\ n\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
3.257 -\endisatagquote
3.258 -{\isafoldquote}%
3.259 -%
3.260 -\isadelimquote
3.261 -%
3.262 -\endisadelimquote
3.263 -%
3.264 -\begin{isamarkuptext}%
3.265 -\noindent The corresponding code in Haskell uses that language's native classes:%
3.266 -\end{isamarkuptext}%
3.267 -\isamarkuptrue%
3.268 -%
3.269 -\isadelimquote
3.270 -%
3.271 -\endisadelimquote
3.272 -%
3.273 -\isatagquote
3.274 -%
3.275 -\begin{isamarkuptext}%
3.276 -\isatypewriter%
3.277 -\noindent%
3.278 -\hspace*{0pt}module Example where {\char123}\\
3.279 -\hspace*{0pt}\\
3.280 -\hspace*{0pt}data Nat = Zero{\char95}nat | Suc Nat;\\
3.281 -\hspace*{0pt}\\
3.282 -\hspace*{0pt}class Semigroup a where {\char123}\\
3.283 -\hspace*{0pt} ~mult ::~a -> a -> a;\\
3.284 -\hspace*{0pt}{\char125};\\
3.285 -\hspace*{0pt}\\
3.286 -\hspace*{0pt}class (Semigroup a) => Monoid a where {\char123}\\
3.287 -\hspace*{0pt} ~neutral ::~a;\\
3.288 -\hspace*{0pt}{\char125};\\
3.289 -\hspace*{0pt}\\
3.290 -\hspace*{0pt}pow ::~forall a.~(Monoid a) => Nat -> a -> a;\\
3.291 -\hspace*{0pt}pow Zero{\char95}nat a = neutral;\\
3.292 -\hspace*{0pt}pow (Suc n) a = mult a (pow n a);\\
3.293 -\hspace*{0pt}\\
3.294 -\hspace*{0pt}plus{\char95}nat ::~Nat -> Nat -> Nat;\\
3.295 -\hspace*{0pt}plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n);\\
3.296 -\hspace*{0pt}plus{\char95}nat Zero{\char95}nat n = n;\\
3.297 -\hspace*{0pt}\\
3.298 -\hspace*{0pt}mult{\char95}nat ::~Nat -> Nat -> Nat;\\
3.299 -\hspace*{0pt}mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat;\\
3.300 -\hspace*{0pt}mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
3.301 -\hspace*{0pt}\\
3.302 -\hspace*{0pt}neutral{\char95}nat ::~Nat;\\
3.303 -\hspace*{0pt}neutral{\char95}nat = Suc Zero{\char95}nat;\\
3.304 -\hspace*{0pt}\\
3.305 -\hspace*{0pt}instance Semigroup Nat where {\char123}\\
3.306 -\hspace*{0pt} ~mult = mult{\char95}nat;\\
3.307 -\hspace*{0pt}{\char125};\\
3.308 -\hspace*{0pt}\\
3.309 -\hspace*{0pt}instance Monoid Nat where {\char123}\\
3.310 -\hspace*{0pt} ~neutral = neutral{\char95}nat;\\
3.311 -\hspace*{0pt}{\char125};\\
3.312 -\hspace*{0pt}\\
3.313 -\hspace*{0pt}bexp ::~Nat -> Nat;\\
3.314 -\hspace*{0pt}bexp n = pow n (Suc (Suc Zero{\char95}nat));\\
3.315 -\hspace*{0pt}\\
3.316 -\hspace*{0pt}{\char125}%
3.317 -\end{isamarkuptext}%
3.318 -\isamarkuptrue%
3.319 -%
3.320 -\endisatagquote
3.321 -{\isafoldquote}%
3.322 -%
3.323 -\isadelimquote
3.324 -%
3.325 -\endisadelimquote
3.326 -%
3.327 -\begin{isamarkuptext}%
3.328 -\noindent This is a convenient place to show how explicit dictionary construction
3.329 - manifests in generated code (here, the same example in \isa{SML})
3.330 - \cite{Haftmann-Nipkow:2010:code}:%
3.331 -\end{isamarkuptext}%
3.332 -\isamarkuptrue%
3.333 -%
3.334 -\isadelimquote
3.335 -%
3.336 -\endisadelimquote
3.337 -%
3.338 -\isatagquote
3.339 -%
3.340 -\begin{isamarkuptext}%
3.341 -\isatypewriter%
3.342 -\noindent%
3.343 -\hspace*{0pt}structure Example :~sig\\
3.344 -\hspace*{0pt} ~datatype nat = Zero{\char95}nat | Suc of nat\\
3.345 -\hspace*{0pt} ~type 'a semigroup\\
3.346 -\hspace*{0pt} ~val mult :~'a semigroup -> 'a -> 'a -> 'a\\
3.347 -\hspace*{0pt} ~type 'a monoid\\
3.348 -\hspace*{0pt} ~val semigroup{\char95}monoid :~'a monoid -> 'a semigroup\\
3.349 -\hspace*{0pt} ~val neutral :~'a monoid -> 'a\\
3.350 -\hspace*{0pt} ~val pow :~'a monoid -> nat -> 'a -> 'a\\
3.351 -\hspace*{0pt} ~val plus{\char95}nat :~nat -> nat -> nat\\
3.352 -\hspace*{0pt} ~val mult{\char95}nat :~nat -> nat -> nat\\
3.353 -\hspace*{0pt} ~val neutral{\char95}nat :~nat\\
3.354 -\hspace*{0pt} ~val semigroup{\char95}nat :~nat semigroup\\
3.355 -\hspace*{0pt} ~val monoid{\char95}nat :~nat monoid\\
3.356 -\hspace*{0pt} ~val bexp :~nat -> nat\\
3.357 -\hspace*{0pt}end = struct\\
3.358 -\hspace*{0pt}\\
3.359 -\hspace*{0pt}datatype nat = Zero{\char95}nat | Suc of nat;\\
3.360 -\hspace*{0pt}\\
3.361 -\hspace*{0pt}type 'a semigroup = {\char123}mult :~'a -> 'a -> 'a{\char125};\\
3.362 -\hspace*{0pt}val mult = {\char35}mult :~'a semigroup -> 'a -> 'a -> 'a;\\
3.363 -\hspace*{0pt}\\
3.364 -\hspace*{0pt}type 'a monoid = {\char123}semigroup{\char95}monoid :~'a semigroup,~neutral :~'a{\char125};\\
3.365 -\hspace*{0pt}val semigroup{\char95}monoid = {\char35}semigroup{\char95}monoid :~'a monoid -> 'a semigroup;\\
3.366 -\hspace*{0pt}val neutral = {\char35}neutral :~'a monoid -> 'a;\\
3.367 -\hspace*{0pt}\\
3.368 -\hspace*{0pt}fun pow A{\char95}~Zero{\char95}nat a = neutral A{\char95}\\
3.369 -\hspace*{0pt} ~| pow A{\char95}~(Suc n) a = mult (semigroup{\char95}monoid A{\char95}) a (pow A{\char95}~n a);\\
3.370 -\hspace*{0pt}\\
3.371 -\hspace*{0pt}fun plus{\char95}nat (Suc m) n = plus{\char95}nat m (Suc n)\\
3.372 -\hspace*{0pt} ~| plus{\char95}nat Zero{\char95}nat n = n;\\
3.373 -\hspace*{0pt}\\
3.374 -\hspace*{0pt}fun mult{\char95}nat Zero{\char95}nat n = Zero{\char95}nat\\
3.375 -\hspace*{0pt} ~| mult{\char95}nat (Suc m) n = plus{\char95}nat n (mult{\char95}nat m n);\\
3.376 -\hspace*{0pt}\\
3.377 -\hspace*{0pt}val neutral{\char95}nat :~nat = Suc Zero{\char95}nat;\\
3.378 -\hspace*{0pt}\\
3.379 -\hspace*{0pt}val semigroup{\char95}nat = {\char123}mult = mult{\char95}nat{\char125}~:~nat semigroup;\\
3.380 -\hspace*{0pt}\\
3.381 -\hspace*{0pt}val monoid{\char95}nat = {\char123}semigroup{\char95}monoid = semigroup{\char95}nat,~neutral = neutral{\char95}nat{\char125}\\
3.382 -\hspace*{0pt} ~:~nat monoid;\\
3.383 -\hspace*{0pt}\\
3.384 -\hspace*{0pt}fun bexp n = pow monoid{\char95}nat n (Suc (Suc Zero{\char95}nat));\\
3.385 -\hspace*{0pt}\\
3.386 -\hspace*{0pt}end;~(*struct Example*)%
3.387 -\end{isamarkuptext}%
3.388 -\isamarkuptrue%
3.389 -%
3.390 -\endisatagquote
3.391 -{\isafoldquote}%
3.392 -%
3.393 -\isadelimquote
3.394 -%
3.395 -\endisadelimquote
3.396 -%
3.397 -\begin{isamarkuptext}%
3.398 -\noindent Note the parameters with trailing underscore (\verb|A_|),
3.399 - which are the dictionary parameters.%
3.400 -\end{isamarkuptext}%
3.401 -\isamarkuptrue%
3.402 -%
3.403 -\isamarkupsubsection{The preprocessor \label{sec:preproc}%
3.404 -}
3.405 -\isamarkuptrue%
3.406 -%
3.407 -\begin{isamarkuptext}%
3.408 -Before selected function theorems are turned into abstract
3.409 - code, a chain of definitional transformation steps is carried
3.410 - out: \emph{preprocessing}. In essence, the preprocessor
3.411 - consists of two components: a \emph{simpset} and \emph{function transformers}.
3.412 -
3.413 - The \emph{simpset} can apply the full generality of the
3.414 - Isabelle simplifier. Due to the interpretation of theorems as code
3.415 - equations, rewrites are applied to the right hand side and the
3.416 - arguments of the left hand side of an equation, but never to the
3.417 - constant heading the left hand side. An important special case are
3.418 - \emph{unfold theorems}, which may be declared and removed using
3.419 - the \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} or \emph{\hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} del}
3.420 - attribute, respectively.
3.421 -
3.422 - Some common applications:%
3.423 -\end{isamarkuptext}%
3.424 -\isamarkuptrue%
3.425 -%
3.426 -\begin{itemize}
3.427 -%
3.428 -\begin{isamarkuptext}%
3.429 -\item replacing non-executable constructs by executable ones:%
3.430 -\end{isamarkuptext}%
3.431 -\isamarkuptrue%
3.432 -%
3.433 -\isadelimquote
3.434 -%
3.435 -\endisadelimquote
3.436 -%
3.437 -\isatagquote
3.438 -\isacommand{lemma}\isamarkupfalse%
3.439 -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
3.440 -\ \ {\isachardoublequoteopen}x\ {\isasymin}\ set\ xs\ {\isasymlongleftrightarrow}\ List{\isachardot}member\ xs\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.441 -\ {\isacharparenleft}fact\ in{\isacharunderscore}set{\isacharunderscore}member{\isacharparenright}%
3.442 -\endisatagquote
3.443 -{\isafoldquote}%
3.444 -%
3.445 -\isadelimquote
3.446 -%
3.447 -\endisadelimquote
3.448 -%
3.449 -\begin{isamarkuptext}%
3.450 -\item eliminating superfluous constants:%
3.451 -\end{isamarkuptext}%
3.452 -\isamarkuptrue%
3.453 -%
3.454 -\isadelimquote
3.455 -%
3.456 -\endisadelimquote
3.457 -%
3.458 -\isatagquote
3.459 -\isacommand{lemma}\isamarkupfalse%
3.460 -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
3.461 -\ \ {\isachardoublequoteopen}{\isadigit{1}}\ {\isacharequal}\ Suc\ {\isadigit{0}}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.462 -\ {\isacharparenleft}fact\ One{\isacharunderscore}nat{\isacharunderscore}def{\isacharparenright}%
3.463 -\endisatagquote
3.464 -{\isafoldquote}%
3.465 -%
3.466 -\isadelimquote
3.467 -%
3.468 -\endisadelimquote
3.469 -%
3.470 -\begin{isamarkuptext}%
3.471 -\item replacing executable but inconvenient constructs:%
3.472 -\end{isamarkuptext}%
3.473 -\isamarkuptrue%
3.474 -%
3.475 -\isadelimquote
3.476 -%
3.477 -\endisadelimquote
3.478 -%
3.479 -\isatagquote
3.480 -\isacommand{lemma}\isamarkupfalse%
3.481 -\ {\isacharbrackleft}code{\isacharunderscore}unfold{\isacharbrackright}{\isacharcolon}\isanewline
3.482 -\ \ {\isachardoublequoteopen}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymlongleftrightarrow}\ List{\isachardot}null\ xs{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
3.483 -\ {\isacharparenleft}fact\ eq{\isacharunderscore}Nil{\isacharunderscore}null{\isacharparenright}%
3.484 -\endisatagquote
3.485 -{\isafoldquote}%
3.486 -%
3.487 -\isadelimquote
3.488 -%
3.489 -\endisadelimquote
3.490 -%
3.491 -\end{itemize}
3.492 -%
3.493 -\begin{isamarkuptext}%
3.494 -\noindent \emph{Function transformers} provide a very general interface,
3.495 - transforming a list of function theorems to another
3.496 - list of function theorems, provided that neither the heading
3.497 - constant nor its type change. The \isa{{\isadigit{0}}} / \isa{Suc}
3.498 - pattern elimination implemented in
3.499 - theory \isa{Efficient{\isacharunderscore}Nat} (see \secref{eff_nat}) uses this
3.500 - interface.
3.501 -
3.502 - \noindent The current setup of the preprocessor may be inspected using
3.503 - the \hyperlink{command.print-codeproc}{\mbox{\isa{\isacommand{print{\isacharunderscore}codeproc}}}} command.
3.504 - \hyperlink{command.code-thms}{\mbox{\isa{\isacommand{code{\isacharunderscore}thms}}}} provides a convenient
3.505 - mechanism to inspect the impact of a preprocessor setup
3.506 - on code equations.
3.507 -
3.508 - \begin{warn}
3.509 -
3.510 - Attribute \hyperlink{attribute.code-unfold}{\mbox{\isa{code{\isacharunderscore}unfold}}} also applies to the
3.511 - preprocessor of the ancient \isa{SML\ code\ generator}; in case
3.512 - this is not what you intend, use \hyperlink{attribute.code-inline}{\mbox{\isa{code{\isacharunderscore}inline}}} instead.
3.513 - \end{warn}%
3.514 -\end{isamarkuptext}%
3.515 -\isamarkuptrue%
3.516 -%
3.517 -\isamarkupsubsection{Datatypes \label{sec:datatypes}%
3.518 -}
3.519 -\isamarkuptrue%
3.520 -%
3.521 -\begin{isamarkuptext}%
3.522 -Conceptually, any datatype is spanned by a set of
3.523 - \emph{constructors} of type \isa{{\isasymtau}\ {\isacharequal}\ {\isasymdots}\ {\isasymRightarrow}\ {\isasymkappa}\ {\isasymalpha}\isactrlisub {\isadigit{1}}\ {\isasymdots}\ {\isasymalpha}\isactrlisub n} where \isa{{\isacharbraceleft}{\isasymalpha}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymalpha}\isactrlisub n{\isacharbraceright}} is exactly the set of \emph{all} type variables in
3.524 - \isa{{\isasymtau}}. The HOL datatype package by default registers any new
3.525 - datatype in the table of datatypes, which may be inspected using the
3.526 - \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isacharunderscore}codesetup}}}} command.
3.527 -
3.528 - In some cases, it is appropriate to alter or extend this table. As
3.529 - an example, we will develop an alternative representation of the
3.530 - queue example given in \secref{sec:intro}. The amortised
3.531 - representation is convenient for generating code but exposes its
3.532 - \qt{implementation} details, which may be cumbersome when proving
3.533 - theorems about it. Therefore, here is a simple, straightforward
3.534 - representation of queues:%
3.535 -\end{isamarkuptext}%
3.536 -\isamarkuptrue%
3.537 -%
3.538 -\isadelimquote
3.539 -%
3.540 -\endisadelimquote
3.541 -%
3.542 -\isatagquote
3.543 -\isacommand{datatype}\isamarkupfalse%
3.544 -\ {\isacharprime}a\ queue\ {\isacharequal}\ Queue\ {\isachardoublequoteopen}{\isacharprime}a\ list{\isachardoublequoteclose}\isanewline
3.545 -\isanewline
3.546 -\isacommand{definition}\isamarkupfalse%
3.547 -\ empty\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.548 -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
3.549 -\isanewline
3.550 -\isacommand{primrec}\isamarkupfalse%
3.551 -\ enqueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.552 -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}Queue\ xs{\isacharparenright}\ {\isacharequal}\ Queue\ {\isacharparenleft}xs\ {\isacharat}\ {\isacharbrackleft}x{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.553 -\isanewline
3.554 -\isacommand{fun}\isamarkupfalse%
3.555 -\ dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.556 -\ \ \ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}None{\isacharcomma}\ Queue\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.557 -\ \ {\isacharbar}\ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}Queue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ x{\isacharcomma}\ Queue\ xs{\isacharparenright}{\isachardoublequoteclose}%
3.558 -\endisatagquote
3.559 -{\isafoldquote}%
3.560 -%
3.561 -\isadelimquote
3.562 -%
3.563 -\endisadelimquote
3.564 -%
3.565 -\begin{isamarkuptext}%
3.566 -\noindent This we can use directly for proving; for executing,
3.567 - we provide an alternative characterisation:%
3.568 -\end{isamarkuptext}%
3.569 -\isamarkuptrue%
3.570 -%
3.571 -\isadelimquote
3.572 -%
3.573 -\endisadelimquote
3.574 -%
3.575 -\isatagquote
3.576 -\isacommand{definition}\isamarkupfalse%
3.577 -\ AQueue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.578 -\ \ {\isachardoublequoteopen}AQueue\ xs\ ys\ {\isacharequal}\ Queue\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.579 -\isanewline
3.580 -\isacommand{code{\isacharunderscore}datatype}\isamarkupfalse%
3.581 -\ AQueue%
3.582 -\endisatagquote
3.583 -{\isafoldquote}%
3.584 -%
3.585 -\isadelimquote
3.586 -%
3.587 -\endisadelimquote
3.588 -%
3.589 -\begin{isamarkuptext}%
3.590 -\noindent Here we define a \qt{constructor} \isa{AQueue} which
3.591 - is defined in terms of \isa{Queue} and interprets its arguments
3.592 - according to what the \emph{content} of an amortised queue is supposed
3.593 - to be. Equipped with this, we are able to prove the following equations
3.594 - for our primitive queue operations which \qt{implement} the simple
3.595 - queues in an amortised fashion:%
3.596 -\end{isamarkuptext}%
3.597 -\isamarkuptrue%
3.598 -%
3.599 -\isadelimquote
3.600 -%
3.601 -\endisadelimquote
3.602 -%
3.603 -\isatagquote
3.604 -\isacommand{lemma}\isamarkupfalse%
3.605 -\ empty{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.606 -\ \ {\isachardoublequoteopen}empty\ {\isacharequal}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
3.607 -\ \ \isacommand{unfolding}\isamarkupfalse%
3.608 -\ AQueue{\isacharunderscore}def\ empty{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
3.609 -\ simp\isanewline
3.610 -\isanewline
3.611 -\isacommand{lemma}\isamarkupfalse%
3.612 -\ enqueue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.613 -\ \ {\isachardoublequoteopen}enqueue\ x\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ AQueue\ {\isacharparenleft}x\ {\isacharhash}\ xs{\isacharparenright}\ ys{\isachardoublequoteclose}\isanewline
3.614 -\ \ \isacommand{unfolding}\isamarkupfalse%
3.615 -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
3.616 -\ simp\isanewline
3.617 -\isanewline
3.618 -\isacommand{lemma}\isamarkupfalse%
3.619 -\ dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.620 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
3.621 -\ \ \ \ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ {\isacharparenleft}None{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\isanewline
3.622 -\ \ \ \ else\ dequeue\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.623 -\ \ {\isachardoublequoteopen}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}Some\ y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.624 -\ \ \isacommand{unfolding}\isamarkupfalse%
3.625 -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
3.626 -\ simp{\isacharunderscore}all%
3.627 -\endisatagquote
3.628 -{\isafoldquote}%
3.629 -%
3.630 -\isadelimquote
3.631 -%
3.632 -\endisadelimquote
3.633 -%
3.634 -\begin{isamarkuptext}%
3.635 -\noindent For completeness, we provide a substitute for the
3.636 - \isa{case} combinator on queues:%
3.637 -\end{isamarkuptext}%
3.638 -\isamarkuptrue%
3.639 -%
3.640 -\isadelimquote
3.641 -%
3.642 -\endisadelimquote
3.643 -%
3.644 -\isatagquote
3.645 -\isacommand{lemma}\isamarkupfalse%
3.646 -\ queue{\isacharunderscore}case{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.647 -\ \ {\isachardoublequoteopen}queue{\isacharunderscore}case\ f\ {\isacharparenleft}AQueue\ xs\ ys{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}ys\ {\isacharat}\ rev\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.648 -\ \ \isacommand{unfolding}\isamarkupfalse%
3.649 -\ AQueue{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
3.650 -\ simp%
3.651 -\endisatagquote
3.652 -{\isafoldquote}%
3.653 -%
3.654 -\isadelimquote
3.655 -%
3.656 -\endisadelimquote
3.657 -%
3.658 -\begin{isamarkuptext}%
3.659 -\noindent The resulting code looks as expected:%
3.660 -\end{isamarkuptext}%
3.661 -\isamarkuptrue%
3.662 -%
3.663 -\isadelimquote
3.664 -%
3.665 -\endisadelimquote
3.666 -%
3.667 -\isatagquote
3.668 -%
3.669 -\begin{isamarkuptext}%
3.670 -\isatypewriter%
3.671 -\noindent%
3.672 -\hspace*{0pt}structure Example :~sig\\
3.673 -\hspace*{0pt} ~val foldl :~('a -> 'b -> 'a) -> 'a -> 'b list -> 'a\\
3.674 -\hspace*{0pt} ~val rev :~'a list -> 'a list\\
3.675 -\hspace*{0pt} ~val null :~'a list -> bool\\
3.676 -\hspace*{0pt} ~datatype 'a queue = AQueue of 'a list * 'a list\\
3.677 -\hspace*{0pt} ~val empty :~'a queue\\
3.678 -\hspace*{0pt} ~val dequeue :~'a queue -> 'a option * 'a queue\\
3.679 -\hspace*{0pt} ~val enqueue :~'a -> 'a queue -> 'a queue\\
3.680 -\hspace*{0pt}end = struct\\
3.681 -\hspace*{0pt}\\
3.682 -\hspace*{0pt}fun foldl f a [] = a\\
3.683 -\hspace*{0pt} ~| foldl f a (x ::~xs) = foldl f (f a x) xs;\\
3.684 -\hspace*{0pt}\\
3.685 -\hspace*{0pt}fun rev xs = foldl (fn xsa => fn x => x ::~xsa) [] xs;\\
3.686 -\hspace*{0pt}\\
3.687 -\hspace*{0pt}fun null [] = true\\
3.688 -\hspace*{0pt} ~| null (x ::~xs) = false;\\
3.689 -\hspace*{0pt}\\
3.690 -\hspace*{0pt}datatype 'a queue = AQueue of 'a list * 'a list;\\
3.691 -\hspace*{0pt}\\
3.692 -\hspace*{0pt}val empty :~'a queue = AQueue ([],~[]);\\
3.693 -\hspace*{0pt}\\
3.694 -\hspace*{0pt}fun dequeue (AQueue (xs,~y ::~ys)) = (SOME y,~AQueue (xs,~ys))\\
3.695 -\hspace*{0pt} ~| dequeue (AQueue (xs,~[])) =\\
3.696 -\hspace*{0pt} ~~~(if null xs then (NONE,~AQueue ([],~[]))\\
3.697 -\hspace*{0pt} ~~~~~else dequeue (AQueue ([],~rev xs)));\\
3.698 -\hspace*{0pt}\\
3.699 -\hspace*{0pt}fun enqueue x (AQueue (xs,~ys)) = AQueue (x ::~xs,~ys);\\
3.700 -\hspace*{0pt}\\
3.701 -\hspace*{0pt}end;~(*struct Example*)%
3.702 -\end{isamarkuptext}%
3.703 -\isamarkuptrue%
3.704 -%
3.705 -\endisatagquote
3.706 -{\isafoldquote}%
3.707 -%
3.708 -\isadelimquote
3.709 -%
3.710 -\endisadelimquote
3.711 -%
3.712 -\begin{isamarkuptext}%
3.713 -\noindent From this example, it can be glimpsed that using own
3.714 - constructor sets is a little delicate since it changes the set of
3.715 - valid patterns for values of that type. Without going into much
3.716 - detail, here some practical hints:
3.717 -
3.718 - \begin{itemize}
3.719 -
3.720 - \item When changing the constructor set for datatypes, take care
3.721 - to provide alternative equations for the \isa{case} combinator.
3.722 -
3.723 - \item Values in the target language need not to be normalised --
3.724 - different values in the target language may represent the same
3.725 - value in the logic.
3.726 -
3.727 - \item Usually, a good methodology to deal with the subtleties of
3.728 - pattern matching is to see the type as an abstract type: provide
3.729 - a set of operations which operate on the concrete representation
3.730 - of the type, and derive further operations by combinations of
3.731 - these primitive ones, without relying on a particular
3.732 - representation.
3.733 -
3.734 - \end{itemize}%
3.735 -\end{isamarkuptext}%
3.736 -\isamarkuptrue%
3.737 -%
3.738 -\isamarkupsubsection{Equality%
3.739 -}
3.740 -\isamarkuptrue%
3.741 -%
3.742 -\begin{isamarkuptext}%
3.743 -Surely you have already noticed how equality is treated
3.744 - by the code generator:%
3.745 -\end{isamarkuptext}%
3.746 -\isamarkuptrue%
3.747 -%
3.748 -\isadelimquote
3.749 -%
3.750 -\endisadelimquote
3.751 -%
3.752 -\isatagquote
3.753 -\isacommand{primrec}\isamarkupfalse%
3.754 -\ collect{\isacharunderscore}duplicates\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.755 -\ \ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline
3.756 -\ \ {\isacharbar}\ {\isachardoublequoteopen}collect{\isacharunderscore}duplicates\ xs\ ys\ {\isacharparenleft}z{\isacharhash}zs{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ z\ {\isasymin}\ set\ xs\isanewline
3.757 -\ \ \ \ \ \ then\ if\ z\ {\isasymin}\ set\ ys\isanewline
3.758 -\ \ \ \ \ \ \ \ then\ collect{\isacharunderscore}duplicates\ xs\ ys\ zs\isanewline
3.759 -\ \ \ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ xs\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs\isanewline
3.760 -\ \ \ \ \ \ else\ collect{\isacharunderscore}duplicates\ {\isacharparenleft}z{\isacharhash}xs{\isacharparenright}\ {\isacharparenleft}z{\isacharhash}ys{\isacharparenright}\ zs{\isacharparenright}{\isachardoublequoteclose}%
3.761 -\endisatagquote
3.762 -{\isafoldquote}%
3.763 -%
3.764 -\isadelimquote
3.765 -%
3.766 -\endisadelimquote
3.767 -%
3.768 -\begin{isamarkuptext}%
3.769 -\noindent During preprocessing, the membership test is rewritten,
3.770 - resulting in \isa{List{\isachardot}member}, which itself
3.771 - performs an explicit equality check.%
3.772 -\end{isamarkuptext}%
3.773 -\isamarkuptrue%
3.774 -%
3.775 -\isadelimquote
3.776 -%
3.777 -\endisadelimquote
3.778 -%
3.779 -\isatagquote
3.780 -%
3.781 -\begin{isamarkuptext}%
3.782 -\isatypewriter%
3.783 -\noindent%
3.784 -\hspace*{0pt}structure Example :~sig\\
3.785 -\hspace*{0pt} ~type 'a eq\\
3.786 -\hspace*{0pt} ~val eq :~'a eq -> 'a -> 'a -> bool\\
3.787 -\hspace*{0pt} ~val eqa :~'a eq -> 'a -> 'a -> bool\\
3.788 -\hspace*{0pt} ~val member :~'a eq -> 'a list -> 'a -> bool\\
3.789 -\hspace*{0pt} ~val collect{\char95}duplicates :\\
3.790 -\hspace*{0pt} ~~~'a eq -> 'a list -> 'a list -> 'a list -> 'a list\\
3.791 -\hspace*{0pt}end = struct\\
3.792 -\hspace*{0pt}\\
3.793 -\hspace*{0pt}type 'a eq = {\char123}eq :~'a -> 'a -> bool{\char125};\\
3.794 -\hspace*{0pt}val eq = {\char35}eq :~'a eq -> 'a -> 'a -> bool;\\
3.795 -\hspace*{0pt}\\
3.796 -\hspace*{0pt}fun eqa A{\char95}~a b = eq A{\char95}~a b;\\
3.797 -\hspace*{0pt}\\
3.798 -\hspace*{0pt}fun member A{\char95}~[] y = false\\
3.799 -\hspace*{0pt} ~| member A{\char95}~(x ::~xs) y = eqa A{\char95}~x y orelse member A{\char95}~xs y;\\
3.800 -\hspace*{0pt}\\
3.801 -\hspace*{0pt}fun collect{\char95}duplicates A{\char95}~xs ys [] = xs\\
3.802 -\hspace*{0pt} ~| collect{\char95}duplicates A{\char95}~xs ys (z ::~zs) =\\
3.803 -\hspace*{0pt} ~~~(if member A{\char95}~xs z\\
3.804 -\hspace*{0pt} ~~~~~then (if member A{\char95}~ys z then collect{\char95}duplicates A{\char95}~xs ys zs\\
3.805 -\hspace*{0pt} ~~~~~~~~~~~~else collect{\char95}duplicates A{\char95}~xs (z ::~ys) zs)\\
3.806 -\hspace*{0pt} ~~~~~else collect{\char95}duplicates A{\char95}~(z ::~xs) (z ::~ys) zs);\\
3.807 -\hspace*{0pt}\\
3.808 -\hspace*{0pt}end;~(*struct Example*)%
3.809 -\end{isamarkuptext}%
3.810 -\isamarkuptrue%
3.811 -%
3.812 -\endisatagquote
3.813 -{\isafoldquote}%
3.814 -%
3.815 -\isadelimquote
3.816 -%
3.817 -\endisadelimquote
3.818 -%
3.819 -\begin{isamarkuptext}%
3.820 -\noindent Obviously, polymorphic equality is implemented the Haskell
3.821 - way using a type class. How is this achieved? HOL introduces
3.822 - an explicit class \isa{eq} with a corresponding operation
3.823 - \isa{eq{\isacharunderscore}class{\isachardot}eq} such that \isa{eq{\isacharunderscore}class{\isachardot}eq\ {\isacharequal}\ op\ {\isacharequal}}.
3.824 - The preprocessing framework does the rest by propagating the
3.825 - \isa{eq} constraints through all dependent code equations.
3.826 - For datatypes, instances of \isa{eq} are implicitly derived
3.827 - when possible. For other types, you may instantiate \isa{eq}
3.828 - manually like any other type class.%
3.829 -\end{isamarkuptext}%
3.830 -\isamarkuptrue%
3.831 -%
3.832 -\isamarkupsubsection{Explicit partiality%
3.833 -}
3.834 -\isamarkuptrue%
3.835 -%
3.836 -\begin{isamarkuptext}%
3.837 -Partiality usually enters the game by partial patterns, as
3.838 - in the following example, again for amortised queues:%
3.839 -\end{isamarkuptext}%
3.840 -\isamarkuptrue%
3.841 -%
3.842 -\isadelimquote
3.843 -%
3.844 -\endisadelimquote
3.845 -%
3.846 -\isatagquote
3.847 -\isacommand{definition}\isamarkupfalse%
3.848 -\ strict{\isacharunderscore}dequeue\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.849 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\isanewline
3.850 -\ \ \ \ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.851 -\isanewline
3.852 -\isacommand{lemma}\isamarkupfalse%
3.853 -\ strict{\isacharunderscore}dequeue{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.854 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.855 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\isanewline
3.856 -\ \ \ \ {\isacharparenleft}case\ rev\ xs\ of\ y\ {\isacharhash}\ ys\ {\isasymRightarrow}\ {\isacharparenleft}y{\isacharcomma}\ AQueue\ {\isacharbrackleft}{\isacharbrackright}\ ys{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.857 -\ \ \isacommand{by}\isamarkupfalse%
3.858 -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
3.859 -\endisatagquote
3.860 -{\isafoldquote}%
3.861 -%
3.862 -\isadelimquote
3.863 -%
3.864 -\endisadelimquote
3.865 -%
3.866 -\begin{isamarkuptext}%
3.867 -\noindent In the corresponding code, there is no equation
3.868 - for the pattern \isa{AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbrackleft}{\isacharbrackright}}:%
3.869 -\end{isamarkuptext}%
3.870 -\isamarkuptrue%
3.871 -%
3.872 -\isadelimquote
3.873 -%
3.874 -\endisadelimquote
3.875 -%
3.876 -\isatagquote
3.877 -%
3.878 -\begin{isamarkuptext}%
3.879 -\isatypewriter%
3.880 -\noindent%
3.881 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
3.882 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
3.883 -\hspace*{0pt} ~let {\char123}\\
3.884 -\hspace*{0pt} ~~~(y :~ys) = reverse xs;\\
3.885 -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
3.886 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
3.887 -\end{isamarkuptext}%
3.888 -\isamarkuptrue%
3.889 -%
3.890 -\endisatagquote
3.891 -{\isafoldquote}%
3.892 -%
3.893 -\isadelimquote
3.894 -%
3.895 -\endisadelimquote
3.896 -%
3.897 -\begin{isamarkuptext}%
3.898 -\noindent In some cases it is desirable to have this
3.899 - pseudo-\qt{partiality} more explicitly, e.g.~as follows:%
3.900 -\end{isamarkuptext}%
3.901 -\isamarkuptrue%
3.902 -%
3.903 -\isadelimquote
3.904 -%
3.905 -\endisadelimquote
3.906 -%
3.907 -\isatagquote
3.908 -\isacommand{axiomatization}\isamarkupfalse%
3.909 -\ empty{\isacharunderscore}queue\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\isanewline
3.910 -\isanewline
3.911 -\isacommand{definition}\isamarkupfalse%
3.912 -\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ queue\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ queue{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
3.913 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ q\ {\isacharequal}\ {\isacharparenleft}case\ dequeue\ q\ of\ {\isacharparenleft}Some\ x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}x{\isacharcomma}\ q{\isacharprime}{\isacharparenright}\ {\isacharbar}\ {\isacharunderscore}\ {\isasymRightarrow}\ empty{\isacharunderscore}queue{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.914 -\isanewline
3.915 -\isacommand{lemma}\isamarkupfalse%
3.916 -\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}AQueue\ {\isacharbrackleft}code{\isacharbrackright}{\isacharcolon}\isanewline
3.917 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}\ then\ empty{\isacharunderscore}queue\isanewline
3.918 -\ \ \ \ \ else\ strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharparenleft}rev\ xs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.919 -\ \ {\isachardoublequoteopen}strict{\isacharunderscore}dequeue{\isacharprime}\ {\isacharparenleft}AQueue\ xs\ {\isacharparenleft}y\ {\isacharhash}\ ys{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
3.920 -\ \ \ \ \ {\isacharparenleft}y{\isacharcomma}\ AQueue\ xs\ ys{\isacharparenright}{\isachardoublequoteclose}\isanewline
3.921 -\ \ \isacommand{by}\isamarkupfalse%
3.922 -\ {\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}\ strict{\isacharunderscore}dequeue{\isacharprime}{\isacharunderscore}def\ dequeue{\isacharunderscore}AQueue\ split{\isacharcolon}\ list{\isachardot}splits{\isacharparenright}%
3.923 -\endisatagquote
3.924 -{\isafoldquote}%
3.925 -%
3.926 -\isadelimquote
3.927 -%
3.928 -\endisadelimquote
3.929 -%
3.930 -\begin{isamarkuptext}%
3.931 -Observe that on the right hand side of the definition of \isa{strict{\isacharunderscore}dequeue{\isacharprime}}, the unspecified constant \isa{empty{\isacharunderscore}queue} occurs.
3.932 -
3.933 - Normally, if constants without any code equations occur in a
3.934 - program, the code generator complains (since in most cases this is
3.935 - indeed an error). But such constants can also be thought
3.936 - of as function definitions which always fail,
3.937 - since there is never a successful pattern match on the left hand
3.938 - side. In order to categorise a constant into that category
3.939 - explicitly, use \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}:%
3.940 -\end{isamarkuptext}%
3.941 -\isamarkuptrue%
3.942 -%
3.943 -\isadelimquote
3.944 -%
3.945 -\endisadelimquote
3.946 -%
3.947 -\isatagquote
3.948 -\isacommand{code{\isacharunderscore}abort}\isamarkupfalse%
3.949 -\ empty{\isacharunderscore}queue%
3.950 -\endisatagquote
3.951 -{\isafoldquote}%
3.952 -%
3.953 -\isadelimquote
3.954 -%
3.955 -\endisadelimquote
3.956 -%
3.957 -\begin{isamarkuptext}%
3.958 -\noindent Then the code generator will just insert an error or
3.959 - exception at the appropriate position:%
3.960 -\end{isamarkuptext}%
3.961 -\isamarkuptrue%
3.962 -%
3.963 -\isadelimquote
3.964 -%
3.965 -\endisadelimquote
3.966 -%
3.967 -\isatagquote
3.968 -%
3.969 -\begin{isamarkuptext}%
3.970 -\isatypewriter%
3.971 -\noindent%
3.972 -\hspace*{0pt}empty{\char95}queue ::~forall a.~a;\\
3.973 -\hspace*{0pt}empty{\char95}queue = error {\char34}empty{\char95}queue{\char34};\\
3.974 -\hspace*{0pt}\\
3.975 -\hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
3.976 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);\\
3.977 -\hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
3.978 -\hspace*{0pt} ~(if null xs then empty{\char95}queue\\
3.979 -\hspace*{0pt} ~~~else strict{\char95}dequeue (AQueue [] (reverse xs)));%
3.980 -\end{isamarkuptext}%
3.981 -\isamarkuptrue%
3.982 -%
3.983 -\endisatagquote
3.984 -{\isafoldquote}%
3.985 -%
3.986 -\isadelimquote
3.987 -%
3.988 -\endisadelimquote
3.989 -%
3.990 -\begin{isamarkuptext}%
3.991 -\noindent This feature however is rarely needed in practice.
3.992 - Note also that the \isa{HOL} default setup already declares
3.993 - \isa{undefined} as \hyperlink{command.code-abort}{\mbox{\isa{\isacommand{code{\isacharunderscore}abort}}}}, which is most
3.994 - likely to be used in such situations.%
3.995 -\end{isamarkuptext}%
3.996 -\isamarkuptrue%
3.997 -%
3.998 -\isadelimtheory
3.999 -%
3.1000 -\endisadelimtheory
3.1001 -%
3.1002 -\isatagtheory
3.1003 -\isacommand{end}\isamarkupfalse%
3.1004 -%
3.1005 -\endisatagtheory
3.1006 -{\isafoldtheory}%
3.1007 -%
3.1008 -\isadelimtheory
3.1009 -%
3.1010 -\endisadelimtheory
3.1011 -\isanewline
3.1012 -\end{isabellebody}%
3.1013 -%%% Local Variables:
3.1014 -%%% mode: latex
3.1015 -%%% TeX-master: "root"
3.1016 -%%% End:
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/doc-src/Codegen/Thy/document/Refinement.tex Fri Aug 13 14:41:12 2010 +0200
4.3 @@ -0,0 +1,43 @@
4.4 +%
4.5 +\begin{isabellebody}%
4.6 +\def\isabellecontext{Refinement}%
4.7 +%
4.8 +\isadelimtheory
4.9 +%
4.10 +\endisadelimtheory
4.11 +%
4.12 +\isatagtheory
4.13 +\isacommand{theory}\isamarkupfalse%
4.14 +\ Refinement\isanewline
4.15 +\isakeyword{imports}\ Setup\isanewline
4.16 +\isakeyword{begin}%
4.17 +\endisatagtheory
4.18 +{\isafoldtheory}%
4.19 +%
4.20 +\isadelimtheory
4.21 +%
4.22 +\endisadelimtheory
4.23 +%
4.24 +\isamarkupsection{Program and datatype refinement \label{sec:refinement}%
4.25 +}
4.26 +\isamarkuptrue%
4.27 +%
4.28 +\isadelimtheory
4.29 +%
4.30 +\endisadelimtheory
4.31 +%
4.32 +\isatagtheory
4.33 +\isacommand{end}\isamarkupfalse%
4.34 +%
4.35 +\endisatagtheory
4.36 +{\isafoldtheory}%
4.37 +%
4.38 +\isadelimtheory
4.39 +%
4.40 +\endisadelimtheory
4.41 +\isanewline
4.42 +\end{isabellebody}%
4.43 +%%% Local Variables:
4.44 +%%% mode: latex
4.45 +%%% TeX-master: "root"
4.46 +%%% End: