author | wenzelm |
Mon, 08 Nov 2010 00:00:47 +0100 | |
changeset 40406 | 313a24b66a8d |
parent 40352 | 8fd36f8a5cb7 |
child 40755 | d73659e8ccdd |
permissions | -rw-r--r-- |
38406 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Refinement}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Refinement\isanewline |
|
12 |
\isakeyword{imports}\ Setup\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
21 |
\isamarkupsection{Program and datatype refinement \label{sec:refinement}% |
|
22 |
} |
|
23 |
\isamarkuptrue% |
|
24 |
% |
|
38451 | 25 |
\begin{isamarkuptext}% |
26 |
Code generation by shallow embedding (cf.~\secref{sec:principle}) |
|
27 |
allows to choose code equations and datatype constructors freely, |
|
28 |
given that some very basic syntactic properties are met; this |
|
29 |
flexibility opens up mechanisms for refinement which allow to extend |
|
30 |
the scope and quality of generated code dramatically.% |
|
31 |
\end{isamarkuptext}% |
|
32 |
\isamarkuptrue% |
|
33 |
% |
|
34 |
\isamarkupsubsection{Program refinement% |
|
35 |
} |
|
36 |
\isamarkuptrue% |
|
37 |
% |
|
38 |
\begin{isamarkuptext}% |
|
39 |
Program refinement works by choosing appropriate code equations |
|
40352 | 40 |
explicitly (cf.~\secref{sec:equations}); as example, we use Fibonacci |
38451 | 41 |
numbers:% |
42 |
\end{isamarkuptext}% |
|
43 |
\isamarkuptrue% |
|
44 |
% |
|
45 |
\isadelimquote |
|
46 |
% |
|
47 |
\endisadelimquote |
|
48 |
% |
|
49 |
\isatagquote |
|
50 |
\isacommand{fun}\isamarkupfalse% |
|
40406 | 51 |
\ fib\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
52 |
\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
53 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
54 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fib\ n\ {\isaliteral{2B}{\isacharplus}}\ fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
38451 | 55 |
\endisatagquote |
56 |
{\isafoldquote}% |
|
57 |
% |
|
58 |
\isadelimquote |
|
59 |
% |
|
60 |
\endisadelimquote |
|
61 |
% |
|
62 |
\begin{isamarkuptext}% |
|
63 |
\noindent The runtime of the corresponding code grows exponential due |
|
64 |
to two recursive calls:% |
|
65 |
\end{isamarkuptext}% |
|
66 |
\isamarkuptrue% |
|
67 |
% |
|
39745 | 68 |
\isadelimquotetypewriter |
38451 | 69 |
% |
39745 | 70 |
\endisadelimquotetypewriter |
38451 | 71 |
% |
39745 | 72 |
\isatagquotetypewriter |
38451 | 73 |
% |
74 |
\begin{isamarkuptext}% |
|
40406 | 75 |
fib\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
76 |
fib\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
77 |
fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
78 |
fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ plus{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{28}{\isacharparenleft}}fib\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline% |
|
38451 | 79 |
\end{isamarkuptext}% |
80 |
\isamarkuptrue% |
|
81 |
% |
|
39745 | 82 |
\endisatagquotetypewriter |
83 |
{\isafoldquotetypewriter}% |
|
38451 | 84 |
% |
39745 | 85 |
\isadelimquotetypewriter |
38451 | 86 |
% |
39745 | 87 |
\endisadelimquotetypewriter |
38451 | 88 |
% |
89 |
\begin{isamarkuptext}% |
|
90 |
\noindent A more efficient implementation would use dynamic |
|
91 |
programming, e.g.~sharing of common intermediate results between |
|
92 |
recursive calls. This idea is expressed by an auxiliary operation |
|
93 |
which computes a Fibonacci number and its successor simultaneously:% |
|
94 |
\end{isamarkuptext}% |
|
95 |
\isamarkuptrue% |
|
96 |
% |
|
97 |
\isadelimquote |
|
98 |
% |
|
99 |
\endisadelimquote |
|
100 |
% |
|
101 |
\isatagquote |
|
102 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 103 |
\ fib{\isaliteral{5F}{\isacharunderscore}}step\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
104 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}fib{\isaliteral{5F}{\isacharunderscore}}step\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ fib\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
38451 | 105 |
\endisatagquote |
106 |
{\isafoldquote}% |
|
107 |
% |
|
108 |
\isadelimquote |
|
109 |
% |
|
110 |
\endisadelimquote |
|
111 |
% |
|
112 |
\begin{isamarkuptext}% |
|
113 |
\noindent This operation can be implemented by recursion using |
|
114 |
dynamic programming:% |
|
115 |
\end{isamarkuptext}% |
|
116 |
\isamarkuptrue% |
|
117 |
% |
|
118 |
\isadelimquote |
|
119 |
% |
|
120 |
\endisadelimquote |
|
121 |
% |
|
122 |
\isatagquote |
|
123 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 124 |
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
125 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}fib{\isaliteral{5F}{\isacharunderscore}}step\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isadigit{0}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
126 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}fib{\isaliteral{5F}{\isacharunderscore}}step\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}let\ {\isaliteral{28}{\isacharparenleft}}m{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fib{\isaliteral{5F}{\isacharunderscore}}step\ n\ in\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2B}{\isacharplus}}\ q{\isaliteral{2C}{\isacharcomma}}\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38451 | 127 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 128 |
\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ fib{\isaliteral{5F}{\isacharunderscore}}step{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
38451 | 129 |
\endisatagquote |
130 |
{\isafoldquote}% |
|
131 |
% |
|
132 |
\isadelimquote |
|
133 |
% |
|
134 |
\endisadelimquote |
|
135 |
% |
|
136 |
\begin{isamarkuptext}% |
|
40406 | 137 |
\noindent What remains is to implement \isa{fib} by \isa{fib{\isaliteral{5F}{\isacharunderscore}}step} as follows:% |
38451 | 138 |
\end{isamarkuptext}% |
139 |
\isamarkuptrue% |
|
140 |
% |
|
141 |
\isadelimquote |
|
142 |
% |
|
143 |
\endisadelimquote |
|
144 |
% |
|
145 |
\isatagquote |
|
146 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 147 |
\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
148 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
149 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fst\ {\isaliteral{28}{\isacharparenleft}}fib{\isaliteral{5F}{\isacharunderscore}}step\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38451 | 150 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 151 |
\ {\isaliteral{28}{\isacharparenleft}}simp{\isaliteral{5F}{\isacharunderscore}}all\ add{\isaliteral{3A}{\isacharcolon}}\ fib{\isaliteral{5F}{\isacharunderscore}}step{\isaliteral{5F}{\isacharunderscore}}def{\isaliteral{29}{\isacharparenright}}% |
38451 | 152 |
\endisatagquote |
153 |
{\isafoldquote}% |
|
154 |
% |
|
155 |
\isadelimquote |
|
156 |
% |
|
157 |
\endisadelimquote |
|
158 |
% |
|
159 |
\begin{isamarkuptext}% |
|
160 |
\noindent The resulting code shows only linear growth of runtime:% |
|
161 |
\end{isamarkuptext}% |
|
162 |
\isamarkuptrue% |
|
163 |
% |
|
39745 | 164 |
\isadelimquotetypewriter |
38451 | 165 |
% |
39745 | 166 |
\endisadelimquotetypewriter |
38451 | 167 |
% |
39745 | 168 |
\isatagquotetypewriter |
38451 | 169 |
% |
170 |
\begin{isamarkuptext}% |
|
40406 | 171 |
fib{\isaliteral{5F}{\isacharunderscore}}step\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{28}{\isacharparenleft}}Nat{\isaliteral{2C}{\isacharcomma}}\ Nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
172 |
fib{\isaliteral{5F}{\isacharunderscore}}step\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ let\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
|
173 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}m{\isaliteral{2C}{\isacharcomma}}\ q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fib{\isaliteral{5F}{\isacharunderscore}}step\ n{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
174 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7D}{\isacharbraceright}}\ in\ {\isaliteral{28}{\isacharparenleft}}plus{\isaliteral{5F}{\isacharunderscore}}nat\ m\ q{\isaliteral{2C}{\isacharcomma}}\ m{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
175 |
fib{\isaliteral{5F}{\isacharunderscore}}step\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Suc\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{2C}{\isacharcomma}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
176 |
\isanewline |
40406 | 177 |
fib\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ Nat\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
178 |
fib\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fst\ {\isaliteral{28}{\isacharparenleft}}fib{\isaliteral{5F}{\isacharunderscore}}step\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
179 |
fib\ Zero{\isaliteral{5F}{\isacharunderscore}}nat\ {\isaliteral{3D}{\isacharequal}}\ Zero{\isaliteral{5F}{\isacharunderscore}}nat{\isaliteral{3B}{\isacharsemicolon}}\isanewline% |
|
38451 | 180 |
\end{isamarkuptext}% |
181 |
\isamarkuptrue% |
|
182 |
% |
|
39745 | 183 |
\endisatagquotetypewriter |
184 |
{\isafoldquotetypewriter}% |
|
38451 | 185 |
% |
39745 | 186 |
\isadelimquotetypewriter |
38451 | 187 |
% |
39745 | 188 |
\endisadelimquotetypewriter |
38451 | 189 |
% |
38459 | 190 |
\isamarkupsubsection{Datatype refinement% |
38437 | 191 |
} |
192 |
\isamarkuptrue% |
|
193 |
% |
|
194 |
\begin{isamarkuptext}% |
|
38459 | 195 |
Selecting specific code equations \emph{and} datatype constructors |
196 |
leads to datatype refinement. As an example, we will develop an |
|
197 |
alternative representation of the queue example given in |
|
198 |
\secref{sec:queue_example}. The amortised representation is |
|
199 |
convenient for generating code but exposes its \qt{implementation} |
|
200 |
details, which may be cumbersome when proving theorems about it. |
|
201 |
Therefore, here is a simple, straightforward representation of |
|
202 |
queues:% |
|
38437 | 203 |
\end{isamarkuptext}% |
204 |
\isamarkuptrue% |
|
205 |
% |
|
206 |
\isadelimquote |
|
207 |
% |
|
208 |
\endisadelimquote |
|
209 |
% |
|
210 |
\isatagquote |
|
211 |
\isacommand{datatype}\isamarkupfalse% |
|
40406 | 212 |
\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ Queue\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
38437 | 213 |
\isanewline |
214 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 215 |
\ empty\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
216 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}empty\ {\isaliteral{3D}{\isacharequal}}\ Queue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 217 |
\isanewline |
218 |
\isacommand{primrec}\isamarkupfalse% |
|
40406 | 219 |
\ enqueue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
220 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}enqueue\ x\ {\isaliteral{28}{\isacharparenleft}}Queue\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Queue\ {\isaliteral{28}{\isacharparenleft}}xs\ {\isaliteral{40}{\isacharat}}\ {\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 221 |
\isanewline |
222 |
\isacommand{fun}\isamarkupfalse% |
|
40406 | 223 |
\ dequeue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
224 |
\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}Queue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}None{\isaliteral{2C}{\isacharcomma}}\ Queue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
225 |
\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}Queue\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Some\ x{\isaliteral{2C}{\isacharcomma}}\ Queue\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
38437 | 226 |
\endisatagquote |
227 |
{\isafoldquote}% |
|
228 |
% |
|
229 |
\isadelimquote |
|
230 |
% |
|
231 |
\endisadelimquote |
|
232 |
% |
|
233 |
\begin{isamarkuptext}% |
|
234 |
\noindent This we can use directly for proving; for executing, |
|
235 |
we provide an alternative characterisation:% |
|
236 |
\end{isamarkuptext}% |
|
237 |
\isamarkuptrue% |
|
238 |
% |
|
239 |
\isadelimquote |
|
240 |
% |
|
241 |
\endisadelimquote |
|
242 |
% |
|
243 |
\isatagquote |
|
244 |
\isacommand{definition}\isamarkupfalse% |
|
40406 | 245 |
\ AQueue\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ queue{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
246 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}AQueue\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ Queue\ {\isaliteral{28}{\isacharparenleft}}ys\ {\isaliteral{40}{\isacharat}}\ rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 247 |
\isanewline |
40406 | 248 |
\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}\isamarkupfalse% |
38437 | 249 |
\ AQueue% |
250 |
\endisatagquote |
|
251 |
{\isafoldquote}% |
|
252 |
% |
|
253 |
\isadelimquote |
|
254 |
% |
|
255 |
\endisadelimquote |
|
256 |
% |
|
257 |
\begin{isamarkuptext}% |
|
258 |
\noindent Here we define a \qt{constructor} \isa{AQueue} which |
|
259 |
is defined in terms of \isa{Queue} and interprets its arguments |
|
260 |
according to what the \emph{content} of an amortised queue is supposed |
|
38459 | 261 |
to be. |
262 |
||
263 |
The prerequisite for datatype constructors is only syntactical: a |
|
40406 | 264 |
constructor must be of type \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n} where \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}} is exactly the set of \emph{all} type variables in |
265 |
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}}; then \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} is its corresponding datatype. The |
|
38459 | 266 |
HOL datatype package by default registers any new datatype with its |
40406 | 267 |
constructors, but this may be changed using \indexdef{}{command}{code\_datatype}\hypertarget{command.code-datatype}{\hyperlink{command.code-datatype}{\mbox{\isa{\isacommand{code{\isaliteral{5F}{\isacharunderscore}}datatype}}}}}; the currently chosen constructors can be inspected |
268 |
using the \hyperlink{command.print-codesetup}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}codesetup}}}} command. |
|
38459 | 269 |
|
270 |
Equipped with this, we are able to prove the following equations |
|
38437 | 271 |
for our primitive queue operations which \qt{implement} the simple |
272 |
queues in an amortised fashion:% |
|
273 |
\end{isamarkuptext}% |
|
274 |
\isamarkuptrue% |
|
275 |
% |
|
276 |
\isadelimquote |
|
277 |
% |
|
278 |
\endisadelimquote |
|
279 |
% |
|
280 |
\isatagquote |
|
281 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 282 |
\ empty{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
283 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}empty\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 284 |
\ \ \isacommand{unfolding}\isamarkupfalse% |
40406 | 285 |
\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ empty{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
38437 | 286 |
\ simp\isanewline |
287 |
\isanewline |
|
288 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 289 |
\ enqueue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
290 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}enqueue\ x\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{23}{\isacharhash}}\ xs{\isaliteral{29}{\isacharparenright}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 291 |
\ \ \isacommand{unfolding}\isamarkupfalse% |
40406 | 292 |
\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
38437 | 293 |
\ simp\isanewline |
294 |
\isanewline |
|
295 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 296 |
\ dequeue{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
297 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
298 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ then\ {\isaliteral{28}{\isacharparenleft}}None{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
299 |
\ \ \ \ else\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
300 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}Some\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 301 |
\ \ \isacommand{unfolding}\isamarkupfalse% |
40406 | 302 |
\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
303 |
\ simp{\isaliteral{5F}{\isacharunderscore}}all% |
|
38437 | 304 |
\endisatagquote |
305 |
{\isafoldquote}% |
|
306 |
% |
|
307 |
\isadelimquote |
|
308 |
% |
|
309 |
\endisadelimquote |
|
310 |
% |
|
311 |
\begin{isamarkuptext}% |
|
312 |
\noindent For completeness, we provide a substitute for the |
|
313 |
\isa{case} combinator on queues:% |
|
314 |
\end{isamarkuptext}% |
|
315 |
\isamarkuptrue% |
|
316 |
% |
|
317 |
\isadelimquote |
|
318 |
% |
|
319 |
\endisadelimquote |
|
320 |
% |
|
321 |
\isatagquote |
|
322 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 323 |
\ queue{\isaliteral{5F}{\isacharunderscore}}case{\isaliteral{5F}{\isacharunderscore}}AQueue\ {\isaliteral{5B}{\isacharbrackleft}}code{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
324 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}queue{\isaliteral{5F}{\isacharunderscore}}case\ f\ {\isaliteral{28}{\isacharparenleft}}AQueue\ xs\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}ys\ {\isaliteral{40}{\isacharat}}\ rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38437 | 325 |
\ \ \isacommand{unfolding}\isamarkupfalse% |
40406 | 326 |
\ AQueue{\isaliteral{5F}{\isacharunderscore}}def\ \isacommand{by}\isamarkupfalse% |
38437 | 327 |
\ simp% |
328 |
\endisatagquote |
|
329 |
{\isafoldquote}% |
|
330 |
% |
|
331 |
\isadelimquote |
|
332 |
% |
|
333 |
\endisadelimquote |
|
334 |
% |
|
335 |
\begin{isamarkuptext}% |
|
336 |
\noindent The resulting code looks as expected:% |
|
337 |
\end{isamarkuptext}% |
|
338 |
\isamarkuptrue% |
|
339 |
% |
|
39745 | 340 |
\isadelimquotetypewriter |
38437 | 341 |
% |
39745 | 342 |
\endisadelimquotetypewriter |
38437 | 343 |
% |
39745 | 344 |
\isatagquotetypewriter |
38437 | 345 |
% |
346 |
\begin{isamarkuptext}% |
|
40406 | 347 |
structure\ Example\ {\isaliteral{3A}{\isacharcolon}}\ sig\isanewline |
348 |
\ \ val\ id\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
349 |
\ \ val\ fold\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}b\isanewline |
|
350 |
\ \ val\ rev\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline |
|
351 |
\ \ val\ null\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ bool\isanewline |
|
352 |
\ \ datatype\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ of\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ list\isanewline |
|
353 |
\ \ val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline |
|
354 |
\ \ val\ dequeue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ option\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline |
|
355 |
\ \ val\ enqueue\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{27}{\isacharprime}}a\ queue\isanewline |
|
356 |
end\ {\isaliteral{3D}{\isacharequal}}\ struct\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
357 |
\isanewline |
40406 | 358 |
fun\ id\ x\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}fn\ xa\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ xa{\isaliteral{29}{\isacharparenright}}\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
359 |
\isanewline |
40406 | 360 |
fun\ fold\ f\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ id\isanewline |
361 |
\ \ {\isaliteral{7C}{\isacharbar}}\ fold\ f\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ fold\ f\ xs\ o\ f\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
362 |
\isanewline |
40406 | 363 |
fun\ rev\ xs\ {\isaliteral{3D}{\isacharequal}}\ fold\ {\isaliteral{28}{\isacharparenleft}}fn\ a\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ fn\ b\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ b{\isaliteral{29}{\isacharparenright}}\ xs\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
364 |
\isanewline |
40406 | 365 |
fun\ null\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ true\isanewline |
366 |
\ \ {\isaliteral{7C}{\isacharbar}}\ null\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ false{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
367 |
\isanewline |
40406 | 368 |
datatype\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ of\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
369 |
\isanewline |
40406 | 370 |
val\ empty\ {\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ queue\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
371 |
\isanewline |
40406 | 372 |
fun\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}SOME\ y{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
373 |
\ \ {\isaliteral{7C}{\isacharbar}}\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
374 |
\ \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ null\ xs\ then\ {\isaliteral{28}{\isacharparenleft}}NONE{\isaliteral{2C}{\isacharcomma}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\isanewline |
|
375 |
\ \ \ \ \ \ else\ dequeue\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{2C}{\isacharcomma}}\ rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
376 |
\isanewline |
40406 | 377 |
fun\ enqueue\ x\ {\isaliteral{28}{\isacharparenleft}}AQueue\ {\isaliteral{28}{\isacharparenleft}}xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ AQueue\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{2C}{\isacharcomma}}\ ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
378 |
\isanewline |
40406 | 379 |
end{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}struct\ Example{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline% |
38437 | 380 |
\end{isamarkuptext}% |
381 |
\isamarkuptrue% |
|
382 |
% |
|
39745 | 383 |
\endisatagquotetypewriter |
384 |
{\isafoldquotetypewriter}% |
|
38437 | 385 |
% |
39745 | 386 |
\isadelimquotetypewriter |
38437 | 387 |
% |
39745 | 388 |
\endisadelimquotetypewriter |
38437 | 389 |
% |
390 |
\begin{isamarkuptext}% |
|
38459 | 391 |
The same techniques can also be applied to types which are not |
392 |
specified as datatypes, e.g.~type \isa{int} is originally specified |
|
38511 | 393 |
as quotient type by means of \indexdef{}{command}{typedef}\hypertarget{command.typedef}{\hyperlink{command.typedef}{\mbox{\isa{\isacommand{typedef}}}}}, but for code |
38459 | 394 |
generation constants allowing construction of binary numeral values |
395 |
are used as constructors for \isa{int}. |
|
38437 | 396 |
|
38459 | 397 |
This approach however fails if the representation of a type demands |
398 |
invariants; this issue is discussed in the next section.% |
|
399 |
\end{isamarkuptext}% |
|
400 |
\isamarkuptrue% |
|
401 |
% |
|
39599 | 402 |
\isamarkupsubsection{Datatype refinement involving invariants \label{sec:invariant}% |
38459 | 403 |
} |
404 |
\isamarkuptrue% |
|
405 |
% |
|
406 |
\begin{isamarkuptext}% |
|
38502 | 407 |
Datatype representation involving invariants require a dedicated |
408 |
setup for the type and its primitive operations. As a running |
|
40406 | 409 |
example, we implement a type \isa{{\isaliteral{27}{\isacharprime}}a\ dlist} of list consisting |
38502 | 410 |
of distinct elements. |
411 |
||
412 |
The first step is to decide on which representation the abstract |
|
40406 | 413 |
type (in our example \isa{{\isaliteral{27}{\isacharprime}}a\ dlist}) should be implemented. |
414 |
Here we choose \isa{{\isaliteral{27}{\isacharprime}}a\ list}. Then a conversion from the concrete |
|
38502 | 415 |
type to the abstract type must be specified, here:% |
416 |
\end{isamarkuptext}% |
|
417 |
\isamarkuptrue% |
|
418 |
% |
|
419 |
\isadelimquote |
|
420 |
% |
|
421 |
\endisadelimquote |
|
422 |
% |
|
423 |
\isatagquote |
|
424 |
% |
|
425 |
\begin{isamarkuptext}% |
|
40406 | 426 |
\isa{Dlist\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ dlist}% |
38502 | 427 |
\end{isamarkuptext}% |
428 |
\isamarkuptrue% |
|
429 |
% |
|
430 |
\endisatagquote |
|
431 |
{\isafoldquote}% |
|
432 |
% |
|
433 |
\isadelimquote |
|
434 |
% |
|
435 |
\endisadelimquote |
|
436 |
% |
|
437 |
\begin{isamarkuptext}% |
|
438 |
\noindent Next follows the specification of a suitable \emph{projection}, |
|
439 |
i.e.~a conversion from abstract to concrete type:% |
|
440 |
\end{isamarkuptext}% |
|
441 |
\isamarkuptrue% |
|
442 |
% |
|
443 |
\isadelimquote |
|
444 |
% |
|
445 |
\endisadelimquote |
|
446 |
% |
|
447 |
\isatagquote |
|
448 |
% |
|
449 |
\begin{isamarkuptext}% |
|
40406 | 450 |
\isa{list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a\ dlist\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list}% |
38502 | 451 |
\end{isamarkuptext}% |
452 |
\isamarkuptrue% |
|
453 |
% |
|
454 |
\endisatagquote |
|
455 |
{\isafoldquote}% |
|
456 |
% |
|
457 |
\isadelimquote |
|
458 |
% |
|
459 |
\endisadelimquote |
|
460 |
% |
|
461 |
\begin{isamarkuptext}% |
|
462 |
\noindent This projection must be specified such that the following |
|
463 |
\emph{abstract datatype certificate} can be proven:% |
|
464 |
\end{isamarkuptext}% |
|
465 |
\isamarkuptrue% |
|
466 |
% |
|
467 |
\isadelimquote |
|
468 |
% |
|
469 |
\endisadelimquote |
|
470 |
% |
|
471 |
\isatagquote |
|
472 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 473 |
\ {\isaliteral{5B}{\isacharbrackleft}}code\ abstype{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
474 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}Dlist\ {\isaliteral{28}{\isacharparenleft}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ dxs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ dxs{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38502 | 475 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 476 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ Dlist{\isaliteral{5F}{\isacharunderscore}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist{\isaliteral{29}{\isacharparenright}}% |
38502 | 477 |
\endisatagquote |
478 |
{\isafoldquote}% |
|
479 |
% |
|
480 |
\isadelimquote |
|
481 |
% |
|
482 |
\endisadelimquote |
|
483 |
% |
|
484 |
\begin{isamarkuptext}% |
|
485 |
\noindent Note that so far the invariant on representations |
|
40406 | 486 |
(\isa{distinct\ {\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool}) has never been mentioned explicitly: |
38502 | 487 |
the invariant is only referred to implicitly: all values in |
40406 | 488 |
set \isa{{\isaliteral{7B}{\isacharbraceleft}}xs{\isaliteral{2E}{\isachardot}}\ list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ {\isaliteral{28}{\isacharparenleft}}Dlist\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ xs{\isaliteral{7D}{\isacharbraceright}}} are invariant, |
489 |
and in our example this is exactly \isa{{\isaliteral{7B}{\isacharbraceleft}}xs{\isaliteral{2E}{\isachardot}}\ distinct\ xs{\isaliteral{7D}{\isacharbraceright}}}. |
|
38502 | 490 |
|
40406 | 491 |
The primitive operations on \isa{{\isaliteral{27}{\isacharprime}}a\ dlist} are specified |
492 |
indirectly using the projection \isa{list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist}. For |
|
493 |
the empty \isa{dlist}, \isa{Dlist{\isaliteral{2E}{\isachardot}}empty}, we finally want |
|
38502 | 494 |
the code equation% |
495 |
\end{isamarkuptext}% |
|
496 |
\isamarkuptrue% |
|
497 |
% |
|
498 |
\isadelimquote |
|
499 |
% |
|
500 |
\endisadelimquote |
|
501 |
% |
|
502 |
\isatagquote |
|
503 |
% |
|
504 |
\begin{isamarkuptext}% |
|
40406 | 505 |
\isa{Dlist{\isaliteral{2E}{\isachardot}}empty\ {\isaliteral{3D}{\isacharequal}}\ Dlist\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}% |
38502 | 506 |
\end{isamarkuptext}% |
507 |
\isamarkuptrue% |
|
508 |
% |
|
509 |
\endisatagquote |
|
510 |
{\isafoldquote}% |
|
511 |
% |
|
512 |
\isadelimquote |
|
513 |
% |
|
514 |
\endisadelimquote |
|
515 |
% |
|
516 |
\begin{isamarkuptext}% |
|
517 |
\noindent This we have to prove indirectly as follows:% |
|
518 |
\end{isamarkuptext}% |
|
519 |
\isamarkuptrue% |
|
520 |
% |
|
521 |
\isadelimquote |
|
522 |
% |
|
523 |
\endisadelimquote |
|
524 |
% |
|
525 |
\isatagquote |
|
526 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 527 |
\ {\isaliteral{5B}{\isacharbrackleft}}code\ abstract{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
528 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ Dlist{\isaliteral{2E}{\isachardot}}empty\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38502 | 529 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 530 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist{\isaliteral{5F}{\isacharunderscore}}empty{\isaliteral{29}{\isacharparenright}}% |
38502 | 531 |
\endisatagquote |
532 |
{\isafoldquote}% |
|
533 |
% |
|
534 |
\isadelimquote |
|
535 |
% |
|
536 |
\endisadelimquote |
|
537 |
% |
|
538 |
\begin{isamarkuptext}% |
|
539 |
\noindent This equation logically encodes both the desired code |
|
540 |
equation and that the expression \isa{Dlist} is applied to obeys |
|
541 |
the implicit invariant. Equations for insertion and removal are |
|
542 |
similar:% |
|
543 |
\end{isamarkuptext}% |
|
544 |
\isamarkuptrue% |
|
545 |
% |
|
546 |
\isadelimquote |
|
547 |
% |
|
548 |
\endisadelimquote |
|
549 |
% |
|
550 |
\isatagquote |
|
551 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 552 |
\ {\isaliteral{5B}{\isacharbrackleft}}code\ abstract{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
553 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ {\isaliteral{28}{\isacharparenleft}}Dlist{\isaliteral{2E}{\isachardot}}insert\ x\ dxs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ List{\isaliteral{2E}{\isachardot}}insert\ x\ {\isaliteral{28}{\isacharparenleft}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ dxs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38502 | 554 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 555 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist{\isaliteral{5F}{\isacharunderscore}}insert{\isaliteral{29}{\isacharparenright}}\isanewline |
38502 | 556 |
\isanewline |
557 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 558 |
\ {\isaliteral{5B}{\isacharbrackleft}}code\ abstract{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3A}{\isacharcolon}}\isanewline |
559 |
\ \ {\isaliteral{22}{\isachardoublequoteopen}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ {\isaliteral{28}{\isacharparenleft}}Dlist{\isaliteral{2E}{\isachardot}}remove\ x\ dxs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ remove{\isadigit{1}}\ x\ {\isaliteral{28}{\isacharparenleft}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ dxs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
38502 | 560 |
\ \ \isacommand{by}\isamarkupfalse% |
40406 | 561 |
\ {\isaliteral{28}{\isacharparenleft}}fact\ list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist{\isaliteral{5F}{\isacharunderscore}}remove{\isaliteral{29}{\isacharparenright}}% |
38502 | 562 |
\endisatagquote |
563 |
{\isafoldquote}% |
|
564 |
% |
|
565 |
\isadelimquote |
|
566 |
% |
|
567 |
\endisadelimquote |
|
568 |
% |
|
569 |
\begin{isamarkuptext}% |
|
570 |
\noindent Then the corresponding code is as follows:% |
|
571 |
\end{isamarkuptext}% |
|
572 |
\isamarkuptrue% |
|
573 |
% |
|
39745 | 574 |
\isadelimquotetypewriter |
38502 | 575 |
% |
39745 | 576 |
\endisadelimquotetypewriter |
38502 | 577 |
% |
39745 | 578 |
\isatagquotetypewriter |
38502 | 579 |
% |
580 |
\begin{isamarkuptext}% |
|
40406 | 581 |
module\ Example\ where\ {\isaliteral{7B}{\isacharbraceleft}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
582 |
\isanewline |
40406 | 583 |
newtype\ Dlist\ a\ {\isaliteral{3D}{\isacharequal}}\ Dlist\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
584 |
\isanewline |
40406 | 585 |
empty\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Dlist\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
586 |
empty\ {\isaliteral{3D}{\isacharequal}}\ Dlist\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
587 |
\isanewline |
40406 | 588 |
member\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Eq\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Bool{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
589 |
member\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ False{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
590 |
member\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ y\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{7C}{\isacharbar}}{\isaliteral{7C}{\isacharbar}}\ member\ xs\ y{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
591 |
\isanewline |
40406 | 592 |
insert\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Eq\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
593 |
insert\ x\ xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ member\ xs\ x\ then\ xs\ else\ x\ {\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
594 |
\isanewline |
40406 | 595 |
list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ Dlist\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
596 |
list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ {\isaliteral{28}{\isacharparenleft}}Dlist\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
597 |
\isanewline |
40406 | 598 |
inserta\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Eq\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Dlist\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Dlist\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
599 |
inserta\ x\ dxs\ {\isaliteral{3D}{\isacharequal}}\ Dlist\ {\isaliteral{28}{\isacharparenleft}}insert\ x\ {\isaliteral{28}{\isacharparenleft}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ dxs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
600 |
\isanewline |
40406 | 601 |
remove{\isadigit{1}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Eq\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ {\isaliteral{5B}{\isacharbrackleft}}a{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
602 |
remove{\isadigit{1}}\ x\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
603 |
remove{\isadigit{1}}\ x\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ x\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3D}{\isacharequal}}\ y\ then\ xs\ else\ y\ {\isaliteral{3A}{\isacharcolon}}\ remove{\isadigit{1}}\ x\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
604 |
\isanewline |
40406 | 605 |
remove\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ forall\ a{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}Eq\ a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}{\isaliteral{3E}{\isachargreater}}\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Dlist\ a\ {\isaliteral{2D}{\isacharminus}}{\isaliteral{3E}{\isachargreater}}\ Dlist\ a{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
606 |
remove\ x\ dxs\ {\isaliteral{3D}{\isacharequal}}\ Dlist\ {\isaliteral{28}{\isacharparenleft}}remove{\isadigit{1}}\ x\ {\isaliteral{28}{\isacharparenleft}}list{\isaliteral{5F}{\isacharunderscore}}of{\isaliteral{5F}{\isacharunderscore}}dlist\ dxs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\isanewline |
|
39664
0afaf89ab591
more canonical type setting of type writer code examples
haftmann
parents:
39599
diff
changeset
|
607 |
\isanewline |
40406 | 608 |
{\isaliteral{7D}{\isacharbraceright}}\isanewline% |
38502 | 609 |
\end{isamarkuptext}% |
610 |
\isamarkuptrue% |
|
611 |
% |
|
39745 | 612 |
\endisatagquotetypewriter |
613 |
{\isafoldquotetypewriter}% |
|
38502 | 614 |
% |
39745 | 615 |
\isadelimquotetypewriter |
38502 | 616 |
% |
39745 | 617 |
\endisadelimquotetypewriter |
38502 | 618 |
% |
619 |
\begin{isamarkuptext}% |
|
620 |
Typical data structures implemented by representations involving |
|
40406 | 621 |
invariants are available in the library, e.g.~theories \hyperlink{theory.Fset}{\mbox{\isa{Fset}}} and \hyperlink{theory.Mapping}{\mbox{\isa{Mapping}}} specify sets (type \isa{{\isaliteral{27}{\isacharprime}}a\ fset}) and |
622 |
key-value-mappings (type \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{27}{\isacharprime}}b{\isaliteral{29}{\isacharparenright}}\ mapping}) respectively; |
|
38502 | 623 |
these can be implemented by distinct lists as presented here as |
624 |
example (theory \hyperlink{theory.Dlist}{\mbox{\isa{Dlist}}}) and red-black-trees respectively |
|
625 |
(theory \hyperlink{theory.RBT}{\mbox{\isa{RBT}}}).% |
|
38437 | 626 |
\end{isamarkuptext}% |
627 |
\isamarkuptrue% |
|
628 |
% |
|
38406 | 629 |
\isadelimtheory |
630 |
% |
|
631 |
\endisadelimtheory |
|
632 |
% |
|
633 |
\isatagtheory |
|
634 |
\isacommand{end}\isamarkupfalse% |
|
635 |
% |
|
636 |
\endisatagtheory |
|
637 |
{\isafoldtheory}% |
|
638 |
% |
|
639 |
\isadelimtheory |
|
640 |
% |
|
641 |
\endisadelimtheory |
|
642 |
\isanewline |
|
643 |
\end{isabellebody}% |
|
644 |
%%% Local Variables: |
|
645 |
%%% mode: latex |
|
646 |
%%% TeX-master: "root" |
|
647 |
%%% End: |