441
|
1 |
theory First_Steps
|
25
|
2 |
imports Base
|
2
|
3 |
begin
|
|
4 |
|
346
|
5 |
(*<*)
|
|
6 |
setup{*
|
|
7 |
open_file_with_prelude
|
441
|
8 |
"First_Steps_Code.thy"
|
|
9 |
["theory First_Steps", "imports Main", "begin"]
|
346
|
10 |
*}
|
|
11 |
(*>*)
|
|
12 |
|
421
|
13 |
chapter {* First Steps\label{chp:firststeps} *}
|
2
|
14 |
|
42
|
15 |
text {*
|
323
|
16 |
\begin{flushright}
|
|
17 |
{\em
|
|
18 |
``We will most likely never realize the full importance of painting the Tower,\\
|
|
19 |
that it is the essential element in the conservation of metal works and the\\
|
347
|
20 |
more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
|
476
|
21 |
Gustave Eiffel, in his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been
|
323
|
22 |
re-painted 18 times since its initial construction, an average of once every
|
350
|
23 |
seven years. It takes more than one year for a team of 25 painters to paint the tower
|
324
|
24 |
from top to bottom.}
|
323
|
25 |
\end{flushright}
|
|
26 |
|
324
|
27 |
\medskip
|
311
|
28 |
Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
|
|
29 |
Isabelle must be part of a theory. If you want to follow the code given in
|
54
|
30 |
this chapter, we assume you are working inside the theory starting with
|
2
|
31 |
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
32 |
\begin{quote}
|
5
|
33 |
\begin{tabular}{@ {}l}
|
441
|
34 |
\isacommand{theory} First\_Steps\\
|
5
|
35 |
\isacommand{imports} Main\\
|
|
36 |
\isacommand{begin}\\
|
6
|
37 |
\ldots
|
5
|
38 |
\end{tabular}
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
39 |
\end{quote}
|
157
|
40 |
|
324
|
41 |
We also generally assume you are working with the logic HOL. The examples
|
|
42 |
that will be given might need to be adapted if you work in a different logic.
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
43 |
*}
|
5
|
44 |
|
372
|
45 |
section {* Including ML-Code\label{sec:include} *}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
46 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
47 |
text {*
|
311
|
48 |
The easiest and quickest way to include code in a theory is by using the
|
|
49 |
\isacommand{ML}-command. For example:
|
|
50 |
|
|
51 |
\begin{isabelle}
|
|
52 |
\begin{graybox}
|
|
53 |
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
|
|
54 |
\hspace{5mm}@{ML "3 + 4"}\isanewline
|
|
55 |
@{text "\<verbclose>"}\isanewline
|
|
56 |
@{text "> 7"}\smallskip
|
|
57 |
\end{graybox}
|
|
58 |
\end{isabelle}
|
|
59 |
|
474
|
60 |
If you work with ProofGeneral then like normal Isabelle scripts
|
|
61 |
\isacommand{ML}-commands can be evaluated by using the advance and
|
|
62 |
undo buttons of your Isabelle environment. If you work with the
|
|
63 |
Jedit GUI, then you just have to hover the cursor over the code
|
|
64 |
and you see the evaluated result in the ``Output'' window.
|
193
|
65 |
|
474
|
66 |
As mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
|
311
|
67 |
"\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
|
|
68 |
prefixed with @{text [quotes] ">"} are not part of the code, rather they
|
|
69 |
indicate what the response is when the code is evaluated. There are also
|
|
70 |
the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
|
|
71 |
ML-code. The first evaluates the given code, but any effect on the theory,
|
|
72 |
in which the code is embedded, is suppressed. The second needs to be used if
|
|
73 |
ML-code is defined inside a proof. For example
|
253
|
74 |
|
254
|
75 |
\begin{quote}
|
|
76 |
\begin{isabelle}
|
|
77 |
\isacommand{lemma}~@{text "test:"}\isanewline
|
|
78 |
\isacommand{shows}~@{text [quotes] "True"}\isanewline
|
|
79 |
\isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline
|
|
80 |
\isacommand{oops}
|
|
81 |
\end{isabelle}
|
|
82 |
\end{quote}
|
253
|
83 |
|
311
|
84 |
However, both commands will only play minor roles in this tutorial (we will
|
374
|
85 |
always arrange that the ML-code is defined outside proofs).
|
10
|
86 |
|
375
|
87 |
|
|
88 |
|
|
89 |
|
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
90 |
Once a portion of code is relatively stable, you usually want to export it
|
235
|
91 |
to a separate ML-file. Such files can then be included somewhere inside a
|
|
92 |
theory by using the command \isacommand{use}. For example
|
|
93 |
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
\begin{quote}
|
235
|
95 |
\begin{tabular}{@ {}l}
|
441
|
96 |
\isacommand{theory} First\_Steps\\
|
235
|
97 |
\isacommand{imports} Main\\
|
|
98 |
\isacommand{uses}~@{text "(\"file_to_be_included.ML\")"} @{text "\<dots>"}\\
|
|
99 |
\isacommand{begin}\\
|
|
100 |
\ldots\\
|
|
101 |
\isacommand{use}~@{text "\"file_to_be_included.ML\""}\\
|
|
102 |
\ldots
|
|
103 |
\end{tabular}
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
104 |
\end{quote}
|
235
|
105 |
|
|
106 |
The \isacommand{uses}-command in the header of the theory is needed in order
|
|
107 |
to indicate the dependency of the theory on the ML-file. Alternatively, the
|
|
108 |
file can be included by just writing in the header
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
109 |
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
110 |
\begin{quote}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
111 |
\begin{tabular}{@ {}l}
|
441
|
112 |
\isacommand{theory} First\_Steps\\
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
113 |
\isacommand{imports} Main\\
|
58
|
114 |
\isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
115 |
\isacommand{begin}\\
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
\ldots
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
117 |
\end{tabular}
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
118 |
\end{quote}
|
235
|
119 |
|
440
|
120 |
Note that no parentheses are given in this case. Note also that the included
|
311
|
121 |
ML-file should not contain any \isacommand{use} itself. Otherwise Isabelle
|
|
122 |
is unable to record all file dependencies, which is a nuisance if you have
|
|
123 |
to track down errors.
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
124 |
*}
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
125 |
|
329
|
126 |
section {* Printing and Debugging\label{sec:printing} *}
|
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
127 |
|
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
text {*
|
374
|
129 |
During development you might find it necessary to inspect data in your
|
311
|
130 |
code. This can be done in a ``quick-and-dirty'' fashion using the function
|
369
|
131 |
@{ML_ind writeln in Output}. For example
|
10
|
132 |
|
441
|
133 |
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
|
10
|
134 |
|
474
|
135 |
will print out @{text [quotes] "any string"} inside the response buffer.
|
|
136 |
This function expects a string as argument. If you develop under
|
311
|
137 |
PolyML, then there is a convenient, though again ``quick-and-dirty'', method
|
421
|
138 |
for converting values into strings, namely the antiquotation
|
|
139 |
@{text "@{make_string}"}:
|
10
|
140 |
|
421
|
141 |
@{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""}
|
12
|
142 |
|
421
|
143 |
However, @{text "@{makes_tring}"} only works if the type of what
|
466
|
144 |
is converted is monomorphic and not a function.
|
311
|
145 |
|
466
|
146 |
You can print out error messages with the function @{ML_ind error in Library};
|
|
147 |
for example:
|
75
|
148 |
|
346
|
149 |
@{ML_response_fake [display,gray]
|
483
|
150 |
"if 0 = 1 then true else (error \"foo\")"
|
122
|
151 |
"Exception- ERROR \"foo\" raised
|
|
152 |
At command \"ML\"."}
|
75
|
153 |
|
307
|
154 |
This function raises the exception @{text ERROR}, which will then
|
420
|
155 |
be displayed by the infrastructure. Note that this exception is meant
|
466
|
156 |
for ``user-level'' error messages seen by the ``end-user''.
|
420
|
157 |
For messages where you want to indicate a genuine program error, then
|
474
|
158 |
use the exception @{text Fail}.
|
304
|
159 |
|
414
|
160 |
Most often you want to inspect data of Isabelle's basic data structures,
|
|
161 |
namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
|
440
|
162 |
and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
|
|
163 |
which we will explain in more detail in Section \ref{sec:pretty}. For now
|
|
164 |
we just use the functions @{ML_ind writeln in Pretty} from the structure
|
|
165 |
@{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
|
|
166 |
@{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
167 |
*}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
168 |
|
441
|
169 |
ML{*val pretty_term = Syntax.pretty_term
|
|
170 |
val pwriteln = Pretty.writeln*}
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
172 |
text {*
|
440
|
173 |
They can now be used as follows
|
126
|
174 |
|
|
175 |
@{ML_response_fake [display,gray]
|
440
|
176 |
"pwriteln (pretty_term @{context} @{term \"1::nat\"})"
|
126
|
177 |
"\"1\""}
|
|
178 |
|
440
|
179 |
If there is more than one term to be printed, you can use the
|
446
|
180 |
function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty}
|
|
181 |
to separate them.
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
182 |
*}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
183 |
|
467
|
184 |
ML{*fun pretty_terms ctxt trms =
|
|
185 |
Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
186 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
187 |
text {*
|
440
|
188 |
You can also print out terms together with their typing information.
|
451
|
189 |
For this you need to set the configuration value
|
|
190 |
@{ML_ind show_types in Syntax} to @{ML true}.
|
370
|
191 |
*}
|
|
192 |
|
451
|
193 |
ML{*val show_types_ctxt = Config.put show_types true @{context}*}
|
370
|
194 |
|
|
195 |
text {*
|
451
|
196 |
Now by using this context @{ML pretty_term} prints out
|
370
|
197 |
|
|
198 |
@{ML_response_fake [display, gray]
|
451
|
199 |
"pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
|
370
|
200 |
"(1::nat, x::'a)"}
|
|
201 |
|
372
|
202 |
where @{text 1} and @{text x} are displayed with their inferred type.
|
370
|
203 |
Even more type information can be printed by setting
|
374
|
204 |
the reference @{ML_ind show_all_types in Syntax} to @{ML true}.
|
377
|
205 |
In this case we obtain
|
370
|
206 |
*}
|
451
|
207 |
|
370
|
208 |
text {*
|
|
209 |
@{ML_response_fake [display, gray]
|
466
|
210 |
"let
|
|
211 |
val show_all_types_ctxt = Config.put show_all_types true @{context}
|
|
212 |
in
|
|
213 |
pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"})
|
|
214 |
end"
|
370
|
215 |
"(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
|
|
216 |
|
466
|
217 |
where now even @{term Pair} is written with its type (@{term Pair} is the
|
|
218 |
term-constructor for products). Other configuration values that influence
|
468
|
219 |
printing of terms include @{ML_ind show_brackets in Syntax}, @{ML_ind
|
|
220 |
show_sorts in Syntax} and @{ML_ind eta_contract in Syntax}.
|
370
|
221 |
*}
|
451
|
222 |
|
370
|
223 |
text {*
|
440
|
224 |
A @{ML_type cterm} can be printed with the following function.
|
126
|
225 |
*}
|
|
226 |
|
467
|
227 |
ML{*fun pretty_cterm ctxt ctrm =
|
|
228 |
pretty_term ctxt (term_of ctrm)*}
|
126
|
229 |
|
|
230 |
text {*
|
440
|
231 |
Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
|
|
232 |
term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can be
|
446
|
233 |
printed again with @{ML commas in Pretty}.
|
126
|
234 |
*}
|
|
235 |
|
467
|
236 |
ML{*fun pretty_cterms ctxt ctrms =
|
|
237 |
Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*}
|
126
|
238 |
|
|
239 |
text {*
|
|
240 |
The easiest way to get the string of a theorem is to transform it
|
369
|
241 |
into a @{ML_type term} using the function @{ML_ind prop_of in Thm}.
|
190
|
242 |
*}
|
|
243 |
|
440
|
244 |
ML{*fun pretty_thm ctxt thm =
|
|
245 |
pretty_term ctxt (prop_of thm)*}
|
190
|
246 |
|
|
247 |
text {*
|
350
|
248 |
Theorems include schematic variables, such as @{text "?P"},
|
343
|
249 |
@{text "?Q"} and so on. They are needed in Isabelle in order to able to
|
314
|
250 |
instantiate theorems when they are applied. For example the theorem
|
|
251 |
@{thm [source] conjI} shown below can be used for any (typable)
|
328
|
252 |
instantiation of @{text "?P"} and @{text "?Q"}.
|
190
|
253 |
|
|
254 |
@{ML_response_fake [display, gray]
|
440
|
255 |
"pwriteln (pretty_thm @{context} @{thm conjI})"
|
190
|
256 |
"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
|
|
257 |
|
314
|
258 |
However, in order to improve the readability when printing theorems, we
|
466
|
259 |
can switch off the question marks as follows:
|
126
|
260 |
*}
|
|
261 |
|
466
|
262 |
ML{*fun pretty_thm_no_vars ctxt thm =
|
|
263 |
let
|
|
264 |
val ctxt' = Config.put show_question_marks false ctxt
|
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
265 |
in
|
466
|
266 |
pretty_term ctxt' (prop_of thm)
|
|
267 |
end*}
|
126
|
268 |
|
|
269 |
text {*
|
374
|
270 |
With this function, theorem @{thm [source] conjI} is now printed as follows:
|
190
|
271 |
|
|
272 |
@{ML_response_fake [display, gray]
|
440
|
273 |
"pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
|
196
|
274 |
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
|
190
|
275 |
|
467
|
276 |
Again the functions @{ML commas} and @{ML block in Pretty} help
|
|
277 |
with printing more than one theorem.
|
126
|
278 |
*}
|
|
279 |
|
440
|
280 |
ML{*fun pretty_thms ctxt thms =
|
446
|
281 |
Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
|
190
|
282 |
|
440
|
283 |
fun pretty_thms_no_vars ctxt thms =
|
446
|
284 |
Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
|
126
|
285 |
|
305
2ac9dc1a95b4
added a comment for printing out information and tuned some examples accordingly
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
286 |
text {*
|
476
|
287 |
Printing functions for @{ML_type typ} are
|
414
|
288 |
*}
|
|
289 |
|
440
|
290 |
ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
|
446
|
291 |
fun pretty_typs ctxt tys =
|
|
292 |
Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
|
414
|
293 |
|
|
294 |
text {*
|
476
|
295 |
respectively @{ML_type ctyp}
|
414
|
296 |
*}
|
|
297 |
|
440
|
298 |
ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
|
446
|
299 |
fun pretty_ctyps ctxt ctys =
|
|
300 |
Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
|
414
|
301 |
|
|
302 |
text {*
|
370
|
303 |
\begin{readmore}
|
|
304 |
The simple conversion functions from Isabelle's main datatypes to
|
|
305 |
@{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}.
|
467
|
306 |
The configuration values that change the printing information are declared in
|
370
|
307 |
@{ML_file "Pure/Syntax/printer.ML"}.
|
|
308 |
\end{readmore}
|
|
309 |
|
414
|
310 |
Note that for printing out several ``parcels'' of information that belong
|
|
311 |
together, like a warning message consisting of a term and its type, you
|
|
312 |
should try to print these parcels together in a single string. Therefore do
|
|
313 |
\emph{not} print out information as
|
306
|
314 |
|
|
315 |
@{ML_response_fake [display,gray]
|
474
|
316 |
"pwriteln (Pretty.str \"First half,\");
|
|
317 |
pwriteln (Pretty.str \"and second half.\")"
|
306
|
318 |
"First half,
|
|
319 |
and second half."}
|
|
320 |
|
|
321 |
but as a single string with appropriate formatting. For example
|
|
322 |
|
|
323 |
@{ML_response_fake [display,gray]
|
474
|
324 |
"pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"
|
306
|
325 |
"First half,
|
|
326 |
and second half."}
|
|
327 |
|
|
328 |
To ease this kind of string manipulations, there are a number
|
374
|
329 |
of library functions in Isabelle. For example, the function
|
|
330 |
@{ML_ind cat_lines in Library} concatenates a list of strings
|
|
331 |
and inserts newlines in between each element.
|
305
2ac9dc1a95b4
added a comment for printing out information and tuned some examples accordingly
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
332 |
|
414
|
333 |
@{ML_response_fake [display, gray]
|
474
|
334 |
"pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
|
414
|
335 |
"foo
|
|
336 |
bar"}
|
306
|
337 |
|
414
|
338 |
Section \ref{sec:pretty} will explain the infrastructure that Isabelle
|
374
|
339 |
provides for more elaborate pretty printing.
|
350
|
340 |
|
|
341 |
\begin{readmore}
|
|
342 |
Most of the basic string functions of Isabelle are defined in
|
|
343 |
@{ML_file "Pure/library.ML"}.
|
|
344 |
\end{readmore}
|
305
2ac9dc1a95b4
added a comment for printing out information and tuned some examples accordingly
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
345 |
*}
|
2ac9dc1a95b4
added a comment for printing out information and tuned some examples accordingly
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
346 |
|
2ac9dc1a95b4
added a comment for printing out information and tuned some examples accordingly
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
347 |
|
126
|
348 |
section {* Combinators\label{sec:combinators} *}
|
|
349 |
|
|
350 |
text {*
|
413
|
351 |
For beginners perhaps the most puzzling parts in the existing code of
|
|
352 |
Isabelle are the combinators. At first they seem to greatly obstruct the
|
|
353 |
comprehension of code, but after getting familiar with them and handled with
|
|
354 |
care, they actually ease the understanding and also the programming.
|
126
|
355 |
|
373
|
356 |
The simplest combinator is @{ML_ind I in Library}, which is just the
|
344
|
357 |
identity function defined as
|
126
|
358 |
*}
|
|
359 |
|
|
360 |
ML{*fun I x = x*}
|
|
361 |
|
344
|
362 |
text {*
|
|
363 |
Another simple combinator is @{ML_ind K in Library}, defined as
|
|
364 |
*}
|
126
|
365 |
|
|
366 |
ML{*fun K x = fn _ => x*}
|
|
367 |
|
|
368 |
text {*
|
350
|
369 |
@{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a
|
|
370 |
result, @{ML K} defines a constant function always returning @{text x}.
|
126
|
371 |
|
344
|
372 |
The next combinator is reverse application, @{ML_ind "|>" in Basics}, defined as:
|
126
|
373 |
*}
|
|
374 |
|
|
375 |
ML{*fun x |> f = f x*}
|
|
376 |
|
|
377 |
text {* While just syntactic sugar for the usual function application,
|
|
378 |
the purpose of this combinator is to implement functions in a
|
|
379 |
``waterfall fashion''. Consider for example the function *}
|
|
380 |
|
|
381 |
ML %linenosgray{*fun inc_by_five x =
|
|
382 |
x |> (fn x => x + 1)
|
|
383 |
|> (fn x => (x, x))
|
|
384 |
|> fst
|
|
385 |
|> (fn x => x + 4)*}
|
|
386 |
|
|
387 |
text {*
|
414
|
388 |
which increments its argument @{text x} by 5. It does this by first
|
|
389 |
incrementing the argument by 1 (Line 2); then storing the result in a pair
|
|
390 |
(Line 3); taking the first component of the pair (Line 4) and finally
|
|
391 |
incrementing the first component by 4 (Line 5). This kind of cascading
|
|
392 |
manipulations of values is quite common when dealing with theories. The
|
|
393 |
reverse application allows you to read what happens in a top-down
|
|
394 |
manner. This kind of coding should be familiar, if you have been exposed to
|
|
395 |
Haskell's {\it do}-notation. Writing the function @{ML inc_by_five} using
|
|
396 |
the reverse application is much clearer than writing
|
126
|
397 |
*}
|
|
398 |
|
|
399 |
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
|
|
400 |
|
|
401 |
text {* or *}
|
|
402 |
|
|
403 |
ML{*fun inc_by_five x =
|
324
|
404 |
((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
|
126
|
405 |
|
|
406 |
text {* and typographically more economical than *}
|
|
407 |
|
|
408 |
ML{*fun inc_by_five x =
|
257
|
409 |
let val y1 = x + 1
|
|
410 |
val y2 = (y1, y1)
|
|
411 |
val y3 = fst y2
|
|
412 |
val y4 = y3 + 4
|
|
413 |
in y4 end*}
|
126
|
414 |
|
|
415 |
text {*
|
|
416 |
Another reason why the let-bindings in the code above are better to be
|
|
417 |
avoided: it is more than easy to get the intermediate values wrong, not to
|
|
418 |
mention the nightmares the maintenance of this code causes!
|
|
419 |
|
350
|
420 |
In Isabelle a ``real world'' example for a function written in
|
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
421 |
the waterfall fashion might be the following code:
|
177
|
422 |
*}
|
126
|
423 |
|
193
|
424 |
ML %linenosgray{*fun apply_fresh_args f ctxt =
|
|
425 |
f |> fastype_of
|
|
426 |
|> binder_types
|
|
427 |
|> map (pair "z")
|
|
428 |
|> Variable.variant_frees ctxt [f]
|
|
429 |
|> map Free
|
257
|
430 |
|> curry list_comb f *}
|
126
|
431 |
|
177
|
432 |
text {*
|
266
|
433 |
This function takes a term and a context as argument. If the term is of function
|
|
434 |
type, then @{ML "apply_fresh_args"} returns the term with distinct variables
|
343
|
435 |
applied to it. For example below three variables are applied to the term
|
298
|
436 |
@{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
|
183
|
437 |
|
|
438 |
@{ML_response_fake [display,gray]
|
266
|
439 |
"let
|
414
|
440 |
val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
|
266
|
441 |
val ctxt = @{context}
|
|
442 |
in
|
414
|
443 |
apply_fresh_args trm ctxt
|
441
|
444 |
|> pretty_term ctxt
|
|
445 |
|> pwriteln
|
266
|
446 |
end"
|
183
|
447 |
"P z za zb"}
|
177
|
448 |
|
344
|
449 |
You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
|
|
450 |
Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
|
|
451 |
term; @{ML_ind binder_types in Term} in the next line produces the list of
|
|
452 |
argument types (in the case above the list @{text "[nat, int, unit]"}); Line
|
|
453 |
4 pairs up each type with the string @{text "z"}; the function @{ML_ind
|
|
454 |
variant_frees in Variable} generates for each @{text "z"} a unique name
|
|
455 |
avoiding the given @{text f}; the list of name-type pairs is turned into a
|
|
456 |
list of variable terms in Line 6, which in the last line is applied by the
|
414
|
457 |
function @{ML_ind list_comb in Term} to the original term. In this last step we have
|
344
|
458 |
to use the function @{ML_ind curry in Library}, because @{ML list_comb}
|
372
|
459 |
expects the function and the variables list as a pair.
|
374
|
460 |
|
414
|
461 |
Functions like @{ML apply_fresh_args} are often needed when constructing
|
|
462 |
terms involving fresh variables. For this the infrastructure helps
|
|
463 |
tremendously to avoid any name clashes. Consider for example:
|
252
|
464 |
|
|
465 |
@{ML_response_fake [display,gray]
|
266
|
466 |
"let
|
414
|
467 |
val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
|
266
|
468 |
val ctxt = @{context}
|
|
469 |
in
|
414
|
470 |
apply_fresh_args trm ctxt
|
441
|
471 |
|> pretty_term ctxt
|
|
472 |
|> pwriteln
|
266
|
473 |
end"
|
252
|
474 |
"za z zb"}
|
177
|
475 |
|
266
|
476 |
where the @{text "za"} is correctly avoided.
|
|
477 |
|
344
|
478 |
The combinator @{ML_ind "#>" in Basics} is the reverse function composition.
|
|
479 |
It can be used to define the following function
|
126
|
480 |
*}
|
|
481 |
|
|
482 |
ML{*val inc_by_six =
|
374
|
483 |
(fn x => x + 1) #>
|
|
484 |
(fn x => x + 2) #>
|
|
485 |
(fn x => x + 3)*}
|
126
|
486 |
|
|
487 |
text {*
|
414
|
488 |
which is the function composed of first the increment-by-one function and
|
|
489 |
then increment-by-two, followed by increment-by-three. Again, the reverse
|
|
490 |
function composition allows you to read the code top-down. This combinator
|
|
491 |
is often used for setup functions inside the
|
478
|
492 |
\isacommand{setup}- or \isacommand{local\_setup}-command. These functions
|
|
493 |
have to be of type @{ML_type "theory -> theory"}, respectively
|
|
494 |
@{ML_type "local_theory -> local_theory"}. More than one such setup function
|
|
495 |
can be composed with @{ML "#>"}. Consider for example the following code,
|
|
496 |
where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1}
|
|
497 |
and @{thm [source] conjunct2} under alternative names.
|
|
498 |
*}
|
|
499 |
|
|
500 |
local_setup %graylinenos {*
|
|
501 |
let
|
|
502 |
fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd
|
|
503 |
in
|
|
504 |
my_note @{binding "foo_conjI"} @{thm conjI} #>
|
|
505 |
my_note @{binding "bar_conjunct1"} @{thm conjunct1} #>
|
|
506 |
my_note @{binding "bar_conjunct2"} @{thm conjunct2}
|
|
507 |
end *}
|
|
508 |
|
|
509 |
text {*
|
|
510 |
The function @{ML_text "my_note"} in line 3 is just a wrapper for the function
|
482
|
511 |
@{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory};
|
|
512 |
its purpose is to store a theorem under a name.
|
|
513 |
In lines 5 to 6 we call this function to give alternative names for the three
|
|
514 |
theorems. The point of @{ML "#>"} is that you can sequence such function calls.
|
478
|
515 |
|
|
516 |
The remaining combinators we describe in this section add convenience for
|
|
517 |
the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
|
|
518 |
in Basics} allows you to get hold of an intermediate result (to do some
|
|
519 |
side-calculations or print out an intermediate result, for instance). The
|
|
520 |
function
|
126
|
521 |
*}
|
|
522 |
|
|
523 |
ML %linenosgray{*fun inc_by_three x =
|
|
524 |
x |> (fn x => x + 1)
|
474
|
525 |
|> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
|
126
|
526 |
|> (fn x => x + 2)*}
|
|
527 |
|
|
528 |
text {*
|
|
529 |
increments the argument first by @{text "1"} and then by @{text "2"}. In the
|
344
|
530 |
middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
|
350
|
531 |
intermediate result. The function @{ML tap} can only be used for
|
|
532 |
side-calculations, because any value that is computed cannot be merged back
|
|
533 |
into the ``main waterfall''. To do this, you can use the next combinator.
|
126
|
534 |
|
344
|
535 |
The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
|
|
536 |
but applies a function to the value and returns the result together with the
|
350
|
537 |
value (as a pair). It is defined as
|
|
538 |
*}
|
|
539 |
|
|
540 |
ML{*fun `f = fn x => (f x, x)*}
|
|
541 |
|
|
542 |
text {*
|
|
543 |
An example for this combinator is the function
|
126
|
544 |
*}
|
|
545 |
|
|
546 |
ML{*fun inc_as_pair x =
|
|
547 |
x |> `(fn x => x + 1)
|
|
548 |
|> (fn (x, y) => (x, y + 1))*}
|
|
549 |
|
|
550 |
text {*
|
350
|
551 |
which takes @{text x} as argument, and then increments @{text x}, but also keeps
|
126
|
552 |
@{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
|
|
553 |
for x}. After that, the function increments the right-hand component of the
|
|
554 |
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
|
|
555 |
|
344
|
556 |
The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
|
|
557 |
defined for functions manipulating pairs. The first applies the function to
|
126
|
558 |
the first component of the pair, defined as
|
|
559 |
*}
|
|
560 |
|
|
561 |
ML{*fun (x, y) |>> f = (f x, y)*}
|
|
562 |
|
|
563 |
text {*
|
|
564 |
and the second combinator to the second component, defined as
|
|
565 |
*}
|
|
566 |
|
|
567 |
ML{*fun (x, y) ||> f = (x, f y)*}
|
|
568 |
|
|
569 |
text {*
|
314
|
570 |
These two functions can, for example, be used to avoid explicit @{text "lets"} for
|
|
571 |
intermediate values in functions that return pairs. As an example, suppose you
|
308
|
572 |
want to separate a list of integers into two lists according to a
|
417
|
573 |
threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
|
414
|
574 |
should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be
|
311
|
575 |
implemented as
|
308
|
576 |
*}
|
|
577 |
|
|
578 |
ML{*fun separate i [] = ([], [])
|
|
579 |
| separate i (x::xs) =
|
|
580 |
let
|
|
581 |
val (los, grs) = separate i xs
|
|
582 |
in
|
|
583 |
if i <= x then (los, x::grs) else (x::los, grs)
|
|
584 |
end*}
|
|
585 |
|
|
586 |
text {*
|
350
|
587 |
where the return value of the recursive call is bound explicitly to
|
414
|
588 |
the pair @{ML "(los, grs)" for los grs}. However, this function
|
|
589 |
can be implemented more concisely as
|
308
|
590 |
*}
|
|
591 |
|
|
592 |
ML{*fun separate i [] = ([], [])
|
|
593 |
| separate i (x::xs) =
|
|
594 |
if i <= x
|
|
595 |
then separate i xs ||> cons x
|
|
596 |
else separate i xs |>> cons x*}
|
|
597 |
|
|
598 |
text {*
|
314
|
599 |
avoiding the explicit @{text "let"}. While in this example the gain in
|
|
600 |
conciseness is only small, in more complicated situations the benefit of
|
|
601 |
avoiding @{text "lets"} can be substantial.
|
308
|
602 |
|
344
|
603 |
With the combinator @{ML_ind "|->" in Basics} you can re-combine the
|
|
604 |
elements from a pair. This combinator is defined as
|
126
|
605 |
*}
|
|
606 |
|
|
607 |
ML{*fun (x, y) |-> f = f x y*}
|
|
608 |
|
215
|
609 |
text {*
|
|
610 |
and can be used to write the following roundabout version
|
126
|
611 |
of the @{text double} function:
|
|
612 |
*}
|
|
613 |
|
|
614 |
ML{*fun double x =
|
|
615 |
x |> (fn x => (x, x))
|
|
616 |
|-> (fn x => fn y => x + y)*}
|
|
617 |
|
215
|
618 |
text {*
|
344
|
619 |
The combinator @{ML_ind ||>> in Basics} plays a central rôle whenever your
|
|
620 |
task is to update a theory and the update also produces a side-result (for
|
|
621 |
example a theorem). Functions for such tasks return a pair whose second
|
|
622 |
component is the theory and the fist component is the side-result. Using
|
|
623 |
@{ML ||>>}, you can do conveniently the update and also
|
|
624 |
accumulate the side-results. Consider the following simple function.
|
215
|
625 |
*}
|
|
626 |
|
|
627 |
ML %linenosgray{*fun acc_incs x =
|
|
628 |
x |> (fn x => ("", x))
|
|
629 |
||>> (fn x => (x, x + 1))
|
|
630 |
||>> (fn x => (x, x + 1))
|
|
631 |
||>> (fn x => (x, x + 1))*}
|
|
632 |
|
|
633 |
text {*
|
|
634 |
The purpose of Line 2 is to just pair up the argument with a dummy value (since
|
344
|
635 |
@{ML ||>>} operates on pairs). Each of the next three lines just increment
|
280
|
636 |
the value by one, but also nest the intermediate results to the left. For example
|
215
|
637 |
|
|
638 |
@{ML_response [display,gray]
|
|
639 |
"acc_incs 1"
|
|
640 |
"((((\"\", 1), 2), 3), 4)"}
|
|
641 |
|
|
642 |
You can continue this chain with:
|
|
643 |
|
|
644 |
@{ML_response [display,gray]
|
|
645 |
"acc_incs 1 ||>> (fn x => (x, x + 2))"
|
|
646 |
"(((((\"\", 1), 2), 3), 4), 6)"}
|
|
647 |
|
483
|
648 |
An example where this combinator is useful is as follows
|
|
649 |
|
|
650 |
@{ML_response_fake [display, gray]
|
|
651 |
"let
|
|
652 |
val ((names1, names2), _) =
|
|
653 |
@{context}
|
|
654 |
|> Variable.variant_fixes (replicate 4 \"x\")
|
|
655 |
||>> Variable.variant_fixes (replicate 5 \"x\")
|
|
656 |
in
|
|
657 |
(names1, names2)
|
|
658 |
end"
|
|
659 |
"([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"}
|
|
660 |
|
|
661 |
Its purpose is to create nine variants of the string @{ML "\"x\""} so
|
|
662 |
that no variant will clash with another. Suppose for some reason we want
|
|
663 |
to bind four variants to the lists @{ML_text "name1"} and the
|
|
664 |
rest to @{ML_text "name2"}. In order to obtain non-clashing
|
|
665 |
variants we have to thread the context through the function calls
|
|
666 |
(the context records which variants have been previously created).
|
|
667 |
For the first call we can use @{ML "|>"}, but in the
|
|
668 |
second and any further call to @{ML_ind variant_fixes in Variable} we
|
|
669 |
have to use @{ML "||>>"} in order to account for the result(s)
|
|
670 |
obtained by previous calls.
|
|
671 |
|
479
|
672 |
A more realistic example for this combinator is the following code
|
478
|
673 |
*}
|
|
674 |
|
479
|
675 |
ML{*val (((one_def, two_def), three_def), ctxt') =
|
478
|
676 |
@{context}
|
|
677 |
|> Local_Defs.add_def ((@{binding "one"}, NoSyn), @{term "1::nat"})
|
|
678 |
||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
|
479
|
679 |
||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
|
478
|
680 |
|
126
|
681 |
text {*
|
479
|
682 |
where we make three definitions, namely @{term "one \<equiv> 1::nat"}, @{term "two \<equiv> 2::nat"}
|
|
683 |
and @{term "three \<equiv> 3::nat"}. The point of this code is that we augment the initial
|
|
684 |
context with the definitions. The result we are interested in is the
|
|
685 |
augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing
|
|
686 |
information about the definitions---the function @{ML_ind add_def in Local_Defs} returns
|
|
687 |
both as pairs. We can use this information for example to print out the definiens and
|
|
688 |
the theorem corresponding to the definitions. For example for the first definition:
|
|
689 |
|
|
690 |
@{ML_response_fake [display, gray]
|
|
691 |
"let
|
|
692 |
val (one_trm, one_thm) = one_def
|
|
693 |
in
|
|
694 |
pwriteln (pretty_term ctxt' one_trm);
|
|
695 |
pwriteln (pretty_thm ctxt' one_thm)
|
|
696 |
end"
|
|
697 |
"one
|
|
698 |
one \<equiv> 1"}
|
344
|
699 |
Recall that @{ML "|>"} is the reverse function application. Recall also that
|
|
700 |
the related reverse function composition is @{ML "#>"}. In fact all the
|
|
701 |
combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
|
|
702 |
described above have related combinators for function composition, namely
|
|
703 |
@{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
|
|
704 |
Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
|
|
705 |
function @{text double} can also be written as:
|
126
|
706 |
*}
|
|
707 |
|
|
708 |
ML{*val double =
|
|
709 |
(fn x => (x, x))
|
|
710 |
#-> (fn x => fn y => x + y)*}
|
|
711 |
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
712 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
713 |
text {*
|
314
|
714 |
When using combinators for writing functions in waterfall fashion, it is
|
311
|
715 |
sometimes necessary to do some ``plumbing'' in order to fit functions
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
716 |
together. We have already seen such plumbing in the function @{ML
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
717 |
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
|
414
|
718 |
list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such
|
|
719 |
plumbing is also needed in situations where a function operates over lists,
|
325
|
720 |
but one calculates only with a single element. An example is the function
|
350
|
721 |
@{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
|
|
722 |
a list of terms. Consider the code:
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
723 |
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
724 |
@{ML_response_fake [display, gray]
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
725 |
"let
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
726 |
val ctxt = @{context}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
727 |
in
|
324
|
728 |
map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"]
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
729 |
|> Syntax.check_terms ctxt
|
441
|
730 |
|> pretty_terms ctxt
|
|
731 |
|> pwriteln
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
732 |
end"
|
324
|
733 |
"m + n, m * n, m - n"}
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
734 |
*}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
735 |
|
126
|
736 |
text {*
|
372
|
737 |
In this example we obtain three terms (using the function
|
|
738 |
@{ML_ind parse_term in Syntax}) whose variables @{text m} and @{text n}
|
|
739 |
are of type @{typ "nat"}. If you have only a single term, then @{ML
|
324
|
740 |
check_terms in Syntax} needs plumbing. This can be done with the function
|
372
|
741 |
@{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in
|
|
742 |
Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented
|
|
743 |
in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
744 |
|
372
|
745 |
@{ML_response_fake [display, gray, linenos]
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
746 |
"let
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
747 |
val ctxt = @{context}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
748 |
in
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
749 |
Syntax.parse_term ctxt \"m - (n::nat)\"
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
750 |
|> singleton (Syntax.check_terms ctxt)
|
441
|
751 |
|> pretty_term ctxt
|
|
752 |
|> pwriteln
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
753 |
end"
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
754 |
"m - n"}
|
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
755 |
|
372
|
756 |
where in Line 5, the function operating over lists fits with the
|
|
757 |
single term generated in Line 4.
|
|
758 |
|
127
|
759 |
\begin{readmore}
|
196
|
760 |
The most frequently used combinators are defined in the files @{ML_file
|
|
761 |
"Pure/library.ML"}
|
127
|
762 |
and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
|
|
763 |
contains further information about combinators.
|
|
764 |
\end{readmore}
|
310
007922777ff1
added some rudimentary inrastructure for producing the ML-code
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
765 |
|
421
|
766 |
\begin{exercise}
|
|
767 |
Find out what the combinator @{ML "K I"} does.
|
|
768 |
\end{exercise}
|
15
|
769 |
*}
|
|
770 |
|
10
|
771 |
|
377
|
772 |
section {* ML-Antiquotations\label{sec:antiquote} *}
|
2
|
773 |
|
|
774 |
text {*
|
372
|
775 |
Recall from Section \ref{sec:include} that code in Isabelle is always
|
|
776 |
embedded in a theory. The main advantage of this is that the code can
|
|
777 |
contain references to entities defined on the logical level of Isabelle. By
|
|
778 |
this we mean references to definitions, theorems, terms and so on. These
|
|
779 |
reference are realised in Isabelle with ML-antiquotations, often just called
|
|
780 |
antiquotations.\footnote{Note that there are two kinds of antiquotations in
|
|
781 |
Isabelle, which have very different purposes and infrastructures. The first
|
|
782 |
kind, described in this section, are \emph{\index*{ML-antiquotation}}. They
|
|
783 |
are used to refer to entities (like terms, types etc) from Isabelle's logic
|
|
784 |
layer inside ML-code. The other kind of antiquotations are
|
|
785 |
\emph{document}\index{document antiquotation} antiquotations. They are used
|
|
786 |
only in the text parts of Isabelle and their purpose is to print logical
|
|
787 |
entities inside \LaTeX-documents. Document antiquotations are part of the
|
|
788 |
user level and therefore we are not interested in them in this Tutorial,
|
|
789 |
except in Appendix \ref{rec:docantiquotations} where we show how to
|
|
790 |
implement your own document antiquotations.} Syntactically antiquotations
|
|
791 |
are indicated by the @{ML_text @}-sign followed by text wrapped in @{text
|
|
792 |
"{\<dots>}"}. For example, one can print out the name of the current theory with
|
|
793 |
the code
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
794 |
|
441
|
795 |
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""}
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
796 |
|
5
|
797 |
where @{text "@{theory}"} is an antiquotation that is substituted with the
|
49
|
798 |
current theory (remember that we assumed we are inside the theory
|
441
|
799 |
@{text First_Steps}). The name of this theory can be extracted using
|
344
|
800 |
the function @{ML_ind theory_name in Context}.
|
5
|
801 |
|
89
|
802 |
Note, however, that antiquotations are statically linked, that is their value is
|
329
|
803 |
determined at ``compile-time'', not at ``run-time''. For example the function
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
804 |
*}
|
5
|
805 |
|
69
|
806 |
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
807 |
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
808 |
text {*
|
89
|
809 |
does \emph{not} return the name of the current theory, if it is run in a
|
5
|
810 |
different theory. Instead, the code above defines the constant function
|
441
|
811 |
that always returns the string @{text [quotes] "First_Steps"}, no matter where the
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
812 |
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
|
5
|
813 |
\emph{not} replaced with code that will look up the current theory in
|
|
814 |
some data structure and return it. Instead, it is literally
|
414
|
815 |
replaced with the value representing the theory.
|
|
816 |
|
|
817 |
Another important antiquotation is @{text "@{context}"}. (What the
|
|
818 |
difference between a theory and a context is will be described in Chapter
|
|
819 |
\ref{chp:advanced}.) A context is for example needed in order to use the
|
475
|
820 |
function @{ML print_abbrevs in Proof_Context} that list of all currently
|
414
|
821 |
defined abbreviations.
|
2
|
822 |
|
414
|
823 |
@{ML_response_fake [display, gray]
|
475
|
824 |
"Proof_Context.print_abbrevs @{context}"
|
414
|
825 |
"Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
|
|
826 |
INTER \<equiv> INFI
|
|
827 |
Inter \<equiv> Inf
|
|
828 |
\<dots>"}
|
|
829 |
|
|
830 |
You can also use antiquotations to refer to proved theorems:
|
133
|
831 |
@{text "@{thm \<dots>}"} for a single theorem
|
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
832 |
|
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
833 |
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
|
75
|
834 |
|
133
|
835 |
and @{text "@{thms \<dots>}"} for more than one
|
132
|
836 |
|
414
|
837 |
@{ML_response_fake [display,gray]
|
|
838 |
"@{thms conj_ac}"
|
132
|
839 |
"(?P \<and> ?Q) = (?Q \<and> ?P)
|
|
840 |
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
|
|
841 |
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
|
|
842 |
|
414
|
843 |
The thm-antiquotations can also be used for manipulating theorems. For
|
474
|
844 |
example, if you need the version of the theorem @{thm [source] refl} that
|
414
|
845 |
has a meta-equality instead of an equality, you can write
|
|
846 |
|
|
847 |
@{ML_response_fake [display,gray]
|
|
848 |
"@{thm refl[THEN eq_reflection]}"
|
|
849 |
"?x \<equiv> ?x"}
|
|
850 |
|
292
|
851 |
The point of these antiquotations is that referring to theorems in this way
|
|
852 |
makes your code independent from what theorems the user might have stored
|
|
853 |
under this name (this becomes especially important when you deal with
|
329
|
854 |
theorem lists; see Section \ref{sec:storing}).
|
292
|
855 |
|
375
|
856 |
It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
|
400
|
857 |
whose first argument is a statement (possibly many of them separated by @{text "and"})
|
375
|
858 |
and the second is a proof. For example
|
|
859 |
*}
|
|
860 |
|
412
|
861 |
ML{*val foo_thm = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
|
375
|
862 |
|
|
863 |
text {*
|
377
|
864 |
The result can be printed out as follows.
|
375
|
865 |
|
|
866 |
@{ML_response_fake [gray,display]
|
440
|
867 |
"foo_thm |> pretty_thms_no_vars @{context}
|
|
868 |
|> pwriteln"
|
414
|
869 |
"True, False \<Longrightarrow> P"}
|
375
|
870 |
|
292
|
871 |
You can also refer to the current simpset via an antiquotation. To illustrate
|
|
872 |
this we implement the function that extracts the theorem names stored in a
|
|
873 |
simpset.
|
131
|
874 |
*}
|
75
|
875 |
|
149
|
876 |
ML{*fun get_thm_names_from_ss simpset =
|
131
|
877 |
let
|
458
|
878 |
val {simps,...} = Raw_Simplifier.dest_ss simpset
|
70
|
879 |
in
|
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
880 |
map #1 simps
|
131
|
881 |
end*}
|
54
|
882 |
|
131
|
883 |
text {*
|
458
|
884 |
The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all
|
414
|
885 |
information stored in the simpset, but here we are only interested in the names of the
|
250
ab9e09076462
some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
886 |
simp-rules. Now you can feed in the current simpset into this function.
|
193
|
887 |
The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
|
81
|
888 |
|
131
|
889 |
@{ML_response_fake [display,gray]
|
149
|
890 |
"get_thm_names_from_ss @{simpset}"
|
|
891 |
"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
|
10
|
892 |
|
196
|
893 |
Again, this way of referencing simpsets makes you independent from additions
|
350
|
894 |
of lemmas to the simpset by the user, which can potentially cause loops in your
|
292
|
895 |
code.
|
156
|
896 |
|
292
|
897 |
It is also possible to define your own antiquotations. But you should
|
315
|
898 |
exercise care when introducing new ones, as they can also make your code
|
372
|
899 |
also difficult to read. In the next chapter we describe how to construct
|
|
900 |
terms with the (build in) antiquotation @{text "@{term \<dots>}"}. A restriction
|
|
901 |
of this antiquotation is that it does not allow you to use schematic
|
|
902 |
variables in terms. If you want to have an antiquotation that does not have
|
323
|
903 |
this restriction, you can implement your own using the function @{ML_ind
|
372
|
904 |
inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code
|
350
|
905 |
for the antiquotation @{text "term_pat"} is as follows.
|
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
906 |
*}
|
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
907 |
|
471
|
908 |
ML %linenosgray{*val term_pat_setup =
|
|
909 |
let
|
325
|
910 |
val parser = Args.context -- Scan.lift Args.name_source
|
|
911 |
|
|
912 |
fun term_pat (ctxt, str) =
|
475
|
913 |
str |> Proof_Context.read_term_pattern ctxt
|
264
|
914 |
|> ML_Syntax.print_term
|
325
|
915 |
|> ML_Syntax.atomic
|
|
916 |
in
|
471
|
917 |
ML_Antiquote.inline @{binding "term_pat"} (parser >> term_pat)
|
325
|
918 |
end*}
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
919 |
|
474
|
920 |
text {*
|
|
921 |
To use it you also have to install it using \isacommand{setup} like so
|
|
922 |
*}
|
|
923 |
|
479
|
924 |
setup %gray {* term_pat_setup *}
|
471
|
925 |
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
926 |
text {*
|
308
|
927 |
The parser in Line 2 provides us with a context and a string; this string is
|
324
|
928 |
transformed into a term using the function @{ML_ind read_term_pattern in
|
475
|
929 |
Proof_Context} (Line 5); the next two lines transform the term into a string
|
372
|
930 |
so that the ML-system can understand it. (All these functions will be explained
|
|
931 |
in more detail in later sections.) An example for this antiquotation is:
|
292
|
932 |
|
|
933 |
@{ML_response_fake [display,gray]
|
|
934 |
"@{term_pat \"Suc (?x::nat)\"}"
|
|
935 |
"Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
|
|
936 |
|
377
|
937 |
which shows the internal representation of the term @{text "Suc ?x"}. Similarly
|
474
|
938 |
we can write an antiquotation for type patterns. Its code is
|
377
|
939 |
*}
|
|
940 |
|
471
|
941 |
ML{*val type_pat_setup =
|
|
942 |
let
|
377
|
943 |
val parser = Args.context -- Scan.lift Args.name_source
|
298
|
944 |
|
377
|
945 |
fun typ_pat (ctxt, str) =
|
|
946 |
str |> Syntax.parse_typ ctxt
|
|
947 |
|> ML_Syntax.print_typ
|
|
948 |
|> ML_Syntax.atomic
|
|
949 |
in
|
471
|
950 |
ML_Antiquote.inline @{binding "typ_pat"} (parser >> typ_pat)
|
377
|
951 |
end*}
|
|
952 |
|
474
|
953 |
text {*
|
|
954 |
which can be installed with
|
|
955 |
*}
|
|
956 |
|
479
|
957 |
setup %gray {* type_pat_setup *}
|
471
|
958 |
|
377
|
959 |
text {*
|
474
|
960 |
However, a word of warning is in order: Introducing new antiquotations
|
|
961 |
should be done only after careful deliberations. They can make your
|
|
962 |
code harder to read, than making it easier.
|
|
963 |
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
964 |
\begin{readmore}
|
292
|
965 |
The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
|
323
|
966 |
for most antiquotations. Most of the basic operations on ML-syntax are implemented
|
|
967 |
in @{ML_file "Pure/ML/ml_syntax.ML"}.
|
263
195c4444dff7
added section about code maintenance and added an example for antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
968 |
\end{readmore}
|
323
|
969 |
*}
|
|
970 |
|
328
|
971 |
section {* Storing Data in Isabelle\label{sec:storing} *}
|
292
|
972 |
|
323
|
973 |
text {*
|
327
|
974 |
Isabelle provides mechanisms for storing (and retrieving) arbitrary
|
|
975 |
data. Before we delve into the details, let us digress a bit. Conventional
|
350
|
976 |
wisdom has it that the type-system of ML ensures that an
|
|
977 |
@{ML_type "'a list"}, say, can only hold elements of the same type, namely
|
467
|
978 |
@{ML_type "'a"} (or whatever is substitued for it). Despite this common
|
|
979 |
wisdom, however, it is possible to implement a
|
327
|
980 |
universal type in ML, although by some arguably accidental features of ML.
|
|
981 |
This universal type can be used to store data of different type into a single list.
|
350
|
982 |
In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is
|
327
|
983 |
in contrast to datatypes, which only allow injection and projection of data for
|
372
|
984 |
some \emph{fixed} collection of types. In light of the conventional wisdom cited
|
327
|
985 |
above it is important to keep in mind that the universal type does not
|
|
986 |
destroy type-safety of ML: storing and accessing the data can only be done
|
474
|
987 |
in a type-safe manner...though run-time checks are needed for that.
|
323
|
988 |
|
327
|
989 |
\begin{readmore}
|
|
990 |
In Isabelle the universal type is implemented as the type @{ML_type
|
|
991 |
Universal.universal} in the file
|
|
992 |
@{ML_file "Pure/ML-Systems/universal.ML"}.
|
|
993 |
\end{readmore}
|
|
994 |
|
|
995 |
We will show the usage of the universal type by storing an integer and
|
|
996 |
a boolean into a single list. Let us first define injection and projection
|
350
|
997 |
functions for booleans and integers into and from the type @{ML_type Universal.universal}.
|
323
|
998 |
*}
|
|
999 |
|
325
|
1000 |
ML{*local
|
|
1001 |
val fn_int = Universal.tag () : int Universal.tag
|
|
1002 |
val fn_bool = Universal.tag () : bool Universal.tag
|
|
1003 |
in
|
|
1004 |
val inject_int = Universal.tagInject fn_int;
|
|
1005 |
val inject_bool = Universal.tagInject fn_bool;
|
|
1006 |
val project_int = Universal.tagProject fn_int;
|
|
1007 |
val project_bool = Universal.tagProject fn_bool
|
|
1008 |
end*}
|
298
|
1009 |
|
325
|
1010 |
text {*
|
327
|
1011 |
Using the injection functions, we can inject the integer @{ML_text "13"}
|
330
|
1012 |
and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and
|
327
|
1013 |
then store them in a @{ML_type "Universal.universal list"} as follows:
|
325
|
1014 |
*}
|
323
|
1015 |
|
327
|
1016 |
ML{*val foo_list =
|
|
1017 |
let
|
474
|
1018 |
val thirteen = inject_int 13
|
327
|
1019 |
val truth_val = inject_bool true
|
|
1020 |
in
|
|
1021 |
[thirteen, truth_val]
|
|
1022 |
end*}
|
|
1023 |
|
|
1024 |
text {*
|
372
|
1025 |
The data can be retrieved with the projection functions defined above.
|
327
|
1026 |
|
372
|
1027 |
@{ML_response_fake [display, gray]
|
|
1028 |
"project_int (nth foo_list 0);
|
|
1029 |
project_bool (nth foo_list 1)"
|
|
1030 |
"13
|
|
1031 |
true"}
|
327
|
1032 |
|
|
1033 |
Notice that we access the integer as an integer and the boolean as
|
|
1034 |
a boolean. If we attempt to access the integer as a boolean, then we get
|
|
1035 |
a runtime error.
|
|
1036 |
|
|
1037 |
@{ML_response_fake [display, gray]
|
|
1038 |
"project_bool (nth foo_list 0)"
|
|
1039 |
"*** Exception- Match raised"}
|
|
1040 |
|
|
1041 |
This runtime error is the reason why ML is still type-sound despite
|
|
1042 |
containing a universal type.
|
|
1043 |
|
328
|
1044 |
Now, Isabelle heavily uses this mechanism for storing all sorts of
|
|
1045 |
data: theorem lists, simpsets, facts etc. Roughly speaking, there are two
|
350
|
1046 |
places where data can be stored in Isabelle: in \emph{theories} and in \emph{proof
|
372
|
1047 |
contexts}. Data such as simpsets are ``global'' and therefore need to be stored
|
|
1048 |
in a theory (simpsets need to be maintained across proofs and even across
|
|
1049 |
theories). On the other hand, data such as facts change inside a proof and
|
328
|
1050 |
are only relevant to the proof at hand. Therefore such data needs to be
|
372
|
1051 |
maintained inside a proof context, which represents ``local'' data.
|
467
|
1052 |
You can think of a theory as the ``longterm memory'' of Isabelle (nothing will
|
|
1053 |
be deleted from it), and a proof-context as a ``shortterm memory'' (it dynamically
|
|
1054 |
changes according to what is needed at the time).
|
327
|
1055 |
|
328
|
1056 |
For theories and proof contexts there are, respectively, the functors
|
385
|
1057 |
@{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help
|
372
|
1058 |
with the data storage. Below we show how to implement a table in which you
|
328
|
1059 |
can store theorems and look them up according to a string key. The
|
350
|
1060 |
intention in this example is to be able to look up introduction rules for logical
|
327
|
1061 |
connectives. Such a table might be useful in an automatic proof procedure
|
350
|
1062 |
and therefore it makes sense to store this data inside a theory.
|
385
|
1063 |
Consequently we use the functor @{ML_funct Theory_Data}.
|
350
|
1064 |
The code for the table is:
|
325
|
1065 |
*}
|
323
|
1066 |
|
385
|
1067 |
ML %linenosgray{*structure Data = Theory_Data
|
327
|
1068 |
(type T = thm Symtab.table
|
|
1069 |
val empty = Symtab.empty
|
|
1070 |
val extend = I
|
385
|
1071 |
val merge = Symtab.merge (K true))*}
|
327
|
1072 |
|
|
1073 |
text {*
|
|
1074 |
In order to store data in a theory, we have to specify the type of the data
|
350
|
1075 |
(Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},
|
|
1076 |
which stands for a table in which @{ML_type string}s can be looked up
|
|
1077 |
producing an associated @{ML_type thm}. We also have to specify four
|
|
1078 |
functions to use this functor: namely how to initialise the data storage
|
385
|
1079 |
(Line 3), how to extend it (Line 4) and how two
|
|
1080 |
tables should be merged (Line 5). These functions correspond roughly to the
|
350
|
1081 |
operations performed on theories and we just give some sensible
|
372
|
1082 |
defaults.\footnote{\bf FIXME: Say more about the
|
350
|
1083 |
assumptions of these operations.} The result structure @{ML_text Data}
|
327
|
1084 |
contains functions for accessing the table (@{ML Data.get}) and for updating
|
385
|
1085 |
it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is
|
|
1086 |
not relevant here. Below we define two
|
350
|
1087 |
auxiliary functions, which help us with accessing the table.
|
327
|
1088 |
*}
|
|
1089 |
|
|
1090 |
ML{*val lookup = Symtab.lookup o Data.get
|
|
1091 |
fun update k v = Data.map (Symtab.update (k, v))*}
|
|
1092 |
|
|
1093 |
text {*
|
|
1094 |
Since we want to store introduction rules associated with their
|
|
1095 |
logical connective, we can fill the table as follows.
|
|
1096 |
*}
|
|
1097 |
|
|
1098 |
setup %gray {*
|
450
|
1099 |
update "conj" @{thm conjI} #>
|
|
1100 |
update "imp" @{thm impI} #>
|
|
1101 |
update "all" @{thm allI}
|
326
|
1102 |
*}
|
|
1103 |
|
|
1104 |
text {*
|
328
|
1105 |
The use of the command \isacommand{setup} makes sure the table in the
|
350
|
1106 |
\emph{current} theory is updated (this is explained further in
|
|
1107 |
section~\ref{sec:theories}). The lookup can now be performed as follows.
|
327
|
1108 |
|
|
1109 |
@{ML_response_fake [display, gray]
|
450
|
1110 |
"lookup @{theory} \"conj\""
|
327
|
1111 |
"SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
|
|
1112 |
|
|
1113 |
An important point to note is that these tables (and data in general)
|
|
1114 |
need to be treated in a purely functional fashion. Although
|
|
1115 |
we can update the table as follows
|
|
1116 |
*}
|
|
1117 |
|
450
|
1118 |
setup %gray {* update "conj" @{thm TrueI} *}
|
327
|
1119 |
|
|
1120 |
text {*
|
350
|
1121 |
and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
|
327
|
1122 |
|
|
1123 |
@{ML_response_fake [display, gray]
|
450
|
1124 |
"lookup @{theory} \"conj\""
|
327
|
1125 |
"SOME \"True\""}
|
|
1126 |
|
|
1127 |
there are no references involved. This is one of the most fundamental
|
350
|
1128 |
coding conventions for programming in Isabelle. References
|
328
|
1129 |
interfere with the multithreaded execution model of Isabelle and also
|
350
|
1130 |
defeat its undo-mechanism. To see the latter, consider the
|
328
|
1131 |
following data container where we maintain a reference to a list of
|
|
1132 |
integers.
|
327
|
1133 |
*}
|
|
1134 |
|
385
|
1135 |
ML{*structure WrongRefData = Theory_Data
|
328
|
1136 |
(type T = (int list) Unsynchronized.ref
|
|
1137 |
val empty = Unsynchronized.ref []
|
|
1138 |
val extend = I
|
385
|
1139 |
val merge = fst)*}
|
327
|
1140 |
|
|
1141 |
text {*
|
328
|
1142 |
We initialise the reference with the empty list. Consequently a first
|
|
1143 |
lookup produces @{ML "ref []" in Unsynchronized}.
|
|
1144 |
|
|
1145 |
@{ML_response_fake [display,gray]
|
|
1146 |
"WrongRefData.get @{theory}"
|
|
1147 |
"ref []"}
|
|
1148 |
|
329
|
1149 |
For updating the reference we use the following function
|
328
|
1150 |
*}
|
|
1151 |
|
|
1152 |
ML{*fun ref_update n = WrongRefData.map
|
|
1153 |
(fn r => let val _ = r := n::(!r) in r end)*}
|
|
1154 |
|
|
1155 |
text {*
|
329
|
1156 |
which takes an integer and adds it to the content of the reference.
|
350
|
1157 |
As before, we update the reference with the command
|
328
|
1158 |
\isacommand{setup}.
|
327
|
1159 |
*}
|
|
1160 |
|
347
|
1161 |
setup %gray {* ref_update 1 *}
|
327
|
1162 |
|
|
1163 |
text {*
|
328
|
1164 |
A lookup in the current theory gives then the expected list
|
|
1165 |
@{ML "ref [1]" in Unsynchronized}.
|
|
1166 |
|
|
1167 |
@{ML_response_fake [display,gray]
|
|
1168 |
"WrongRefData.get @{theory}"
|
|
1169 |
"ref [1]"}
|
|
1170 |
|
347
|
1171 |
So far everything is as expected. But, the trouble starts if we attempt to
|
350
|
1172 |
backtrack to the ``point'' before the \isacommand{setup}-command. There, we
|
347
|
1173 |
would expect that the list is empty again. But since it is stored in a
|
|
1174 |
reference, Isabelle has no control over it. So it is not empty, but still
|
|
1175 |
@{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
|
|
1176 |
\isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
|
|
1177 |
Unsynchronized}, but
|
327
|
1178 |
|
|
1179 |
@{ML_response_fake [display,gray]
|
328
|
1180 |
"WrongRefData.get @{theory}"
|
|
1181 |
"ref [1, 1]"}
|
|
1182 |
|
474
|
1183 |
Now imagine how often you go backwards and forwards in your proof
|
|
1184 |
scripts.\footnote{The same problem can be triggered in the Jedit GUI by
|
|
1185 |
making the parser to go over and over again over the \isacommand{setup} command.}
|
328
|
1186 |
By using references in Isabelle code, you are bound to cause all
|
329
|
1187 |
hell to break loose. Therefore observe the coding convention:
|
328
|
1188 |
Do not use references for storing data!
|
327
|
1189 |
|
328
|
1190 |
\begin{readmore}
|
|
1191 |
The functors for data storage are defined in @{ML_file "Pure/context.ML"}.
|
|
1192 |
Isabelle contains implementations of several container data structures,
|
|
1193 |
including association lists in @{ML_file "Pure/General/alist.ML"},
|
347
|
1194 |
directed graphs in @{ML_file "Pure/General/graph.ML"}, and
|
328
|
1195 |
tables and symtables in @{ML_file "Pure/General/table.ML"}.
|
|
1196 |
\end{readmore}
|
327
|
1197 |
|
350
|
1198 |
Storing data in a proof context is done in a similar fashion. As mentioned
|
385
|
1199 |
before, the corresponding functor is @{ML_funct_ind Proof_Data}. With the
|
350
|
1200 |
following code we can store a list of terms in a proof context.
|
328
|
1201 |
*}
|
|
1202 |
|
385
|
1203 |
ML{*structure Data = Proof_Data
|
328
|
1204 |
(type T = term list
|
|
1205 |
fun init _ = [])*}
|
|
1206 |
|
|
1207 |
text {*
|
414
|
1208 |
The init-function we have to specify must produce a list for when a context
|
350
|
1209 |
is initialised (possibly taking the theory into account from which the
|
372
|
1210 |
context is derived). We choose here to just return the empty list. Next
|
328
|
1211 |
we define two auxiliary functions for updating the list with a given
|
|
1212 |
term and printing the list.
|
|
1213 |
*}
|
|
1214 |
|
330
|
1215 |
ML{*fun update trm = Data.map (fn trms => trm::trms)
|
328
|
1216 |
|
|
1217 |
fun print ctxt =
|
|
1218 |
case (Data.get ctxt) of
|
474
|
1219 |
[] => pwriteln (Pretty.str "Empty!")
|
441
|
1220 |
| trms => pwriteln (pretty_terms ctxt trms)*}
|
328
|
1221 |
|
|
1222 |
text {*
|
330
|
1223 |
Next we start with the context generated by the antiquotation
|
328
|
1224 |
@{text "@{context}"} and update it in various ways.
|
|
1225 |
|
|
1226 |
@{ML_response_fake [display,gray]
|
|
1227 |
"let
|
347
|
1228 |
val ctxt0 = @{context}
|
|
1229 |
val ctxt1 = ctxt0 |> update @{term \"False\"}
|
|
1230 |
|> update @{term \"True \<and> True\"}
|
|
1231 |
val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
|
|
1232 |
val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
|
328
|
1233 |
in
|
347
|
1234 |
print ctxt0;
|
|
1235 |
print ctxt1;
|
|
1236 |
print ctxt2;
|
|
1237 |
print ctxt3
|
328
|
1238 |
end"
|
|
1239 |
"Empty!
|
|
1240 |
True \<and> True, False
|
|
1241 |
1
|
|
1242 |
2, 1"}
|
|
1243 |
|
|
1244 |
Many functions in Isabelle manage and update data in a similar
|
414
|
1245 |
fashion. Consequently, such calculations with contexts occur frequently in
|
328
|
1246 |
Isabelle code, although the ``context flow'' is usually only linear.
|
|
1247 |
Note also that the calculation above has no effect on the underlying
|
|
1248 |
theory. Once we throw away the contexts, we have no access to their
|
414
|
1249 |
associated data. This is different for theories, where the command
|
328
|
1250 |
\isacommand{setup} registers the data with the current and future
|
330
|
1251 |
theories, and therefore one can access the data potentially
|
347
|
1252 |
indefinitely.
|
329
|
1253 |
|
350
|
1254 |
For convenience there is an abstract layer, namely the type @{ML_type Context.generic},
|
|
1255 |
for treating theories and proof contexts more uniformly. This type is defined as follows
|
330
|
1256 |
*}
|
|
1257 |
|
|
1258 |
ML_val{*datatype generic =
|
|
1259 |
Theory of theory
|
|
1260 |
| Proof of proof*}
|
|
1261 |
|
|
1262 |
text {*
|
350
|
1263 |
\footnote{\bf FIXME: say more about generic contexts.}
|
329
|
1264 |
|
|
1265 |
There are two special instances of the data storage mechanism described
|
350
|
1266 |
above. The first instance implements named theorem lists using the functor
|
|
1267 |
@{ML_funct_ind Named_Thms}. This is because storing theorems in a list
|
|
1268 |
is such a common task. To obtain a named theorem list, you just declare
|
329
|
1269 |
*}
|
|
1270 |
|
|
1271 |
ML{*structure FooRules = Named_Thms
|
481
|
1272 |
(val name = @{binding "foo"}
|
329
|
1273 |
val description = "Theorems for foo") *}
|
|
1274 |
|
|
1275 |
text {*
|
|
1276 |
and set up the @{ML_struct FooRules} with the command
|
|
1277 |
*}
|
|
1278 |
|
|
1279 |
setup %gray {* FooRules.setup *}
|
|
1280 |
|
|
1281 |
text {*
|
|
1282 |
This code declares a data container where the theorems are stored,
|
|
1283 |
an attribute @{text foo} (with the @{text add} and @{text del} options
|
377
|
1284 |
for adding and deleting theorems) and an internal ML-interface for retrieving and
|
|
1285 |
modifying the theorems.
|
350
|
1286 |
Furthermore, the theorems are made available on the user-level under the name
|
|
1287 |
@{text foo}. For example you can declare three lemmas to be a member of the
|
|
1288 |
theorem list @{text foo} by:
|
326
|
1289 |
*}
|
|
1290 |
|
329
|
1291 |
lemma rule1[foo]: "A" sorry
|
|
1292 |
lemma rule2[foo]: "B" sorry
|
|
1293 |
lemma rule3[foo]: "C" sorry
|
|
1294 |
|
|
1295 |
text {* and undeclare the first one by: *}
|
|
1296 |
|
|
1297 |
declare rule1[foo del]
|
|
1298 |
|
350
|
1299 |
text {* You can query the remaining ones with:
|
329
|
1300 |
|
|
1301 |
\begin{isabelle}
|
|
1302 |
\isacommand{thm}~@{text "foo"}\\
|
|
1303 |
@{text "> ?C"}\\
|
|
1304 |
@{text "> ?B"}
|
|
1305 |
\end{isabelle}
|
|
1306 |
|
|
1307 |
On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
|
|
1308 |
*}
|
|
1309 |
|
347
|
1310 |
setup %gray {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *}
|
329
|
1311 |
|
|
1312 |
text {*
|
|
1313 |
The rules in the list can be retrieved using the function
|
|
1314 |
@{ML FooRules.get}:
|
|
1315 |
|
347
|
1316 |
@{ML_response_fake [display,gray]
|
|
1317 |
"FooRules.get @{context}"
|
|
1318 |
"[\"True\", \"?C\",\"?B\"]"}
|
|
1319 |
|
|
1320 |
Note that this function takes a proof context as argument. This might be
|
350
|
1321 |
confusing, since the theorem list is stored as theory data. It becomes clear by knowing
|
|
1322 |
that the proof context contains the information about the current theory and so the function
|
347
|
1323 |
can access the theorem list in the theory via the context.
|
329
|
1324 |
|
|
1325 |
\begin{readmore}
|
347
|
1326 |
For more information about named theorem lists see
|
|
1327 |
@{ML_file "Pure/Tools/named_thms.ML"}.
|
329
|
1328 |
\end{readmore}
|
|
1329 |
|
|
1330 |
The second special instance of the data storage mechanism are configuration
|
|
1331 |
values. They are used to enable users to configure tools without having to
|
|
1332 |
resort to the ML-level (and also to avoid references). Assume you want the
|
|
1333 |
user to control three values, say @{text bval} containing a boolean, @{text
|
|
1334 |
ival} containing an integer and @{text sval} containing a string. These
|
|
1335 |
values can be declared by
|
|
1336 |
*}
|
|
1337 |
|
462
|
1338 |
ML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
|
|
1339 |
val ival = Attrib.setup_config_int @{binding "ival"} (K 0)
|
|
1340 |
val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *}
|
329
|
1341 |
|
|
1342 |
text {*
|
462
|
1343 |
where each value needs to be given a default.
|
329
|
1344 |
The user can now manipulate the values from the user-level of Isabelle
|
|
1345 |
with the command
|
|
1346 |
*}
|
|
1347 |
|
|
1348 |
declare [[bval = true, ival = 3]]
|
|
1349 |
|
|
1350 |
text {*
|
|
1351 |
On the ML-level these values can be retrieved using the
|
346
|
1352 |
function @{ML_ind get in Config} from a proof context
|
|
1353 |
|
|
1354 |
@{ML_response [display,gray]
|
|
1355 |
"Config.get @{context} bval"
|
|
1356 |
"true"}
|
|
1357 |
|
423
|
1358 |
or directly from a theory using the function @{ML_ind get_global in Config}
|
346
|
1359 |
|
|
1360 |
@{ML_response [display,gray]
|
423
|
1361 |
"Config.get_global @{theory} bval"
|
346
|
1362 |
"true"}
|
329
|
1363 |
|
346
|
1364 |
It is also possible to manipulate the configuration values
|
347
|
1365 |
from the ML-level with the functions @{ML_ind put in Config}
|
423
|
1366 |
and @{ML_ind put_global in Config}. For example
|
346
|
1367 |
|
|
1368 |
@{ML_response [display,gray]
|
|
1369 |
"let
|
|
1370 |
val ctxt = @{context}
|
|
1371 |
val ctxt' = Config.put sval \"foo\" ctxt
|
347
|
1372 |
val ctxt'' = Config.put sval \"bar\" ctxt'
|
346
|
1373 |
in
|
350
|
1374 |
(Config.get ctxt sval,
|
|
1375 |
Config.get ctxt' sval,
|
|
1376 |
Config.get ctxt'' sval)
|
346
|
1377 |
end"
|
347
|
1378 |
"(\"some string\", \"foo\", \"bar\")"}
|
329
|
1379 |
|
468
|
1380 |
A concrete example for a configuration value is
|
|
1381 |
@{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
|
474
|
1382 |
in the simplifier. This can be used for example in the following proof
|
468
|
1383 |
*}
|
|
1384 |
|
|
1385 |
lemma
|
|
1386 |
shows "(False \<or> True) \<and> True"
|
|
1387 |
proof (rule conjI)
|
|
1388 |
show "False \<or> True" using [[simp_trace = true]] by simp
|
|
1389 |
next
|
|
1390 |
show "True" by simp
|
|
1391 |
qed
|
|
1392 |
|
|
1393 |
text {*
|
|
1394 |
in order to inspect how the simplifier solves the first subgoal.
|
|
1395 |
|
329
|
1396 |
\begin{readmore}
|
|
1397 |
For more information about configuration values see
|
346
|
1398 |
the files @{ML_file "Pure/Isar/attrib.ML"} and
|
|
1399 |
@{ML_file "Pure/config.ML"}.
|
329
|
1400 |
\end{readmore}
|
343
|
1401 |
*}
|
|
1402 |
|
|
1403 |
section {* Summary *}
|
|
1404 |
|
|
1405 |
text {*
|
|
1406 |
This chapter describes the combinators that are used in Isabelle, as well
|
|
1407 |
as a simple printing infrastructure for @{ML_type term}, @{ML_type cterm}
|
|
1408 |
and @{ML_type thm}. The section on ML-antiquotations shows how to refer
|
|
1409 |
statically to entities from the logic level of Isabelle. Isabelle also
|
|
1410 |
contains mechanisms for storing arbitrary data in theory and proof
|
|
1411 |
contexts.
|
|
1412 |
|
347
|
1413 |
\begin{conventions}
|
|
1414 |
\begin{itemize}
|
370
|
1415 |
\item Print messages that belong together in a single string.
|
350
|
1416 |
\item Do not use references in Isabelle code.
|
347
|
1417 |
\end{itemize}
|
|
1418 |
\end{conventions}
|
|
1419 |
|
329
|
1420 |
*}
|
196
|
1421 |
end
|