395
|
1 |
theory Advanced
|
441
|
2 |
imports Base First_Steps
|
318
|
3 |
begin
|
|
4 |
|
346
|
5 |
(*<*)
|
|
6 |
setup{*
|
|
7 |
open_file_with_prelude
|
395
|
8 |
"Advanced_Code.thy"
|
441
|
9 |
["theory Advanced", "imports Base First_Steps", "begin"]
|
346
|
10 |
*}
|
|
11 |
(*>*)
|
|
12 |
|
|
13 |
|
414
|
14 |
chapter {* Advanced Isabelle\label{chp:advanced} *}
|
381
|
15 |
|
|
16 |
text {*
|
410
|
17 |
\begin{flushright}
|
|
18 |
{\em All things are difficult before they are easy.} \\[1ex]
|
|
19 |
proverb
|
|
20 |
\end{flushright}
|
|
21 |
|
|
22 |
\medskip
|
400
|
23 |
While terms, types and theorems are the most basic data structures in
|
|
24 |
Isabelle, there are a number of layers built on top of them. Most of these
|
408
|
25 |
layers are concerned with storing and manipulating data. Handling them
|
487
|
26 |
properly is an essential skill for programming on the ML-level of Isabelle.
|
|
27 |
The most basic layer are theories. They contain global data and
|
408
|
28 |
can be seen as the ``long-term memory'' of Isabelle. There is usually only
|
|
29 |
one theory active at each moment. Proof contexts and local theories, on the
|
400
|
30 |
other hand, store local data for a task at hand. They act like the
|
408
|
31 |
``short-term memory'' and there can be many of them that are active in
|
|
32 |
parallel.
|
318
|
33 |
*}
|
|
34 |
|
486
|
35 |
section {* Theories and Setups\label{sec:theories} *}
|
358
|
36 |
|
|
37 |
text {*
|
492
|
38 |
Theories, as said above, are the most basic layer of abstraction in
|
|
39 |
Isabelle. They record information about definitions, syntax declarations, axioms,
|
488
|
40 |
theorems and much more. For example, if a definition is made, it
|
|
41 |
must be stored in a theory in order to be usable later on. Similar
|
|
42 |
with proofs: once a proof is finished, the proved theorem needs to
|
|
43 |
be stored in the theorem database of the theory in order to be
|
491
|
44 |
usable. All relevant data of a theory can be queried with the
|
|
45 |
Isabelle command \isacommand{print\_theory}.
|
358
|
46 |
|
|
47 |
\begin{isabelle}
|
|
48 |
\isacommand{print\_theory}\\
|
|
49 |
@{text "> names: Pure Code_Generator HOL \<dots>"}\\
|
|
50 |
@{text "> classes: Inf < type \<dots>"}\\
|
|
51 |
@{text "> default sort: type"}\\
|
|
52 |
@{text "> syntactic types: #prop \<dots>"}\\
|
|
53 |
@{text "> logical types: 'a \<times> 'b \<dots>"}\\
|
|
54 |
@{text "> type arities: * :: (random, random) random \<dots>"}\\
|
|
55 |
@{text "> logical constants: == :: 'a \<Rightarrow> 'a \<Rightarrow> prop \<dots>"}\\
|
|
56 |
@{text "> abbreviations: \<dots>"}\\
|
|
57 |
@{text "> axioms: \<dots>"}\\
|
|
58 |
@{text "> oracles: \<dots>"}\\
|
|
59 |
@{text "> definitions: \<dots>"}\\
|
|
60 |
@{text "> theorems: \<dots>"}
|
|
61 |
\end{isabelle}
|
|
62 |
|
487
|
63 |
Functions acting on theories often end with the suffix @{text "_global"},
|
|
64 |
for example the function @{ML read_term_global in Syntax} in the structure
|
|
65 |
@{ML_struct Syntax}. The reason is to set them syntactically apart from
|
491
|
66 |
functions acting on contexts or local theories, which will be discussed in
|
|
67 |
the next sections. There is a tendency amongst Isabelle developers to prefer
|
487
|
68 |
``non-global'' operations, because they have some advantages, as we will also
|
490
|
69 |
discuss later. However, some basic understanding of theories is still necessary
|
|
70 |
for effective Isabelle programming.
|
487
|
71 |
|
491
|
72 |
An important Isabelle command with theories is \isacommand{setup}. In the
|
492
|
73 |
previous chapters we used it already to make a theorem attribute known
|
|
74 |
to Isabelle and to register a theorem under a name. What happens behind the
|
490
|
75 |
scenes is that \isacommand{setup} expects a function of type @{ML_type
|
|
76 |
"theory -> theory"}: the input theory is the current theory and the output
|
|
77 |
the theory where the attribute has been registered or the theorem has been
|
|
78 |
stored. This is a fundamental principle in Isabelle. A similar situation
|
491
|
79 |
arises with declaring a constant, which can be done on the ML-level with
|
|
80 |
function @{ML_ind declare_const in Sign} from the structure @{ML_struct
|
490
|
81 |
Sign}. To see how \isacommand{setup} works, consider the following code:
|
|
82 |
|
348
|
83 |
*}
|
|
84 |
|
485
|
85 |
ML{*let
|
|
86 |
val thy = @{theory}
|
|
87 |
val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
|
|
88 |
in
|
|
89 |
Sign.declare_const @{context} bar_const thy
|
|
90 |
end*}
|
348
|
91 |
|
|
92 |
text {*
|
488
|
93 |
If you simply run this code\footnote{Recall that ML-code needs to be enclosed in
|
486
|
94 |
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.} with the
|
491
|
95 |
intention of declaring a constant @{text "BAR"} having type @{typ nat}, then
|
488
|
96 |
indeed you obtain a theory as result. But if you query the
|
486
|
97 |
constant on the Isabelle level using the command \isacommand{term}
|
348
|
98 |
|
|
99 |
\begin{isabelle}
|
485
|
100 |
\isacommand{term}~@{text BAR}\\
|
348
|
101 |
@{text "> \"BAR\" :: \"'a\""}
|
|
102 |
\end{isabelle}
|
|
103 |
|
495
|
104 |
you can see that you do \emph{not} obtain the expected constant of type @{typ nat}, but a free
|
484
|
105 |
variable (printed in blue) of polymorphic type. The problem is that the
|
|
106 |
ML-expression above did not ``register'' the declaration with the current theory.
|
|
107 |
This is what the command \isacommand{setup} is for. The constant is properly
|
|
108 |
declared with
|
348
|
109 |
*}
|
|
110 |
|
486
|
111 |
setup %gray {* fn thy =>
|
|
112 |
let
|
485
|
113 |
val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
|
486
|
114 |
val (_, thy') = Sign.declare_const @{context} bar_const thy
|
485
|
115 |
in
|
486
|
116 |
thy'
|
485
|
117 |
end *}
|
348
|
118 |
|
|
119 |
text {*
|
486
|
120 |
where the declaration is actually applied to the current theory and
|
348
|
121 |
|
|
122 |
\begin{isabelle}
|
|
123 |
\isacommand{term}~@{text [quotes] "BAR"}\\
|
|
124 |
@{text "> \"BAR\" :: \"nat\""}
|
|
125 |
\end{isabelle}
|
|
126 |
|
492
|
127 |
now returns a (black) constant with the type @{typ nat}, as expected.
|
348
|
128 |
|
491
|
129 |
In a sense, \isacommand{setup} can be seen as a transaction that
|
|
130 |
takes the current theory @{text thy}, applies an operation, and
|
|
131 |
produces a new current theory @{text thy'}. This means that we have
|
|
132 |
to be careful to apply operations always to the most current theory,
|
|
133 |
not to a \emph{stale} one. Consider again the function inside the
|
486
|
134 |
\isacommand{setup}-command:
|
485
|
135 |
|
486
|
136 |
\begin{isabelle}
|
|
137 |
\begin{graybox}
|
|
138 |
\isacommand{setup}~@{text "\<verbopen>"} @{ML
|
|
139 |
"fn thy =>
|
|
140 |
let
|
|
141 |
val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)
|
|
142 |
val (_, thy') = Sign.declare_const @{context} bar_const thy
|
|
143 |
in
|
|
144 |
thy
|
|
145 |
end"}~@{text "\<verbclose>"}\isanewline
|
495
|
146 |
@{text "> ERROR: \"Stale theory encountered\""}
|
486
|
147 |
\end{graybox}
|
|
148 |
\end{isabelle}
|
|
149 |
|
|
150 |
This time we erroneously return the original theory @{text thy}, instead of
|
488
|
151 |
the modified one @{text thy'}. Such buggy code will always result into
|
|
152 |
a runtime error message about stale theories.
|
486
|
153 |
|
|
154 |
However, sometimes it does make sense to work with two theories at the same
|
|
155 |
time, especially in the context of parsing and typing. In the code below we
|
|
156 |
use in Line 3 the function @{ML_ind copy in Theory} from the structure
|
|
157 |
@{ML_struct Theory} for obtaining a new theory that contains the same
|
|
158 |
data, but is unrelated to the existing theory.
|
|
159 |
*}
|
485
|
160 |
|
486
|
161 |
setup %graylinenos {* fn thy =>
|
|
162 |
let
|
|
163 |
val tmp_thy = Theory.copy thy
|
|
164 |
val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)
|
|
165 |
val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy
|
|
166 |
val trm1 = Syntax.read_term_global tmp_thy' "FOO baz"
|
|
167 |
val trm2 = Syntax.read_term_global thy "FOO baz"
|
|
168 |
val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)
|
|
169 |
in
|
|
170 |
thy
|
|
171 |
end *}
|
|
172 |
|
|
173 |
text {*
|
|
174 |
That means we can make changes to the theory @{text tmp_thy} without
|
|
175 |
affecting the current theory @{text thy}. In this case we declare in @{text
|
|
176 |
"tmp_thy"} the constant @{text FOO} (Lines 4 and 5). The point of this code
|
|
177 |
is that we next, in Lines 6 and 7, parse a string to become a term (both
|
|
178 |
times the string is @{text [quotes] "FOO baz"}). But since we parse the string
|
|
179 |
once in the context of the theory @{text tmp_thy'} in which @{text FOO} is
|
|
180 |
declared to be a constant of type @{typ "nat \<Rightarrow>nat"} and once in the context
|
488
|
181 |
of @{text thy} where it is not, we obtain two different terms, namely
|
486
|
182 |
|
|
183 |
\begin{isabelle}
|
|
184 |
\begin{graybox}
|
|
185 |
@{text "> Const (\"Advanced.FOO\", \"nat \<Rightarrow> nat\") $ Free (\"baz\", \"nat\")"}\isanewline
|
|
186 |
@{text "> Free (\"FOO\", \"'a \<Rightarrow> 'b\") $ Free (\"baz\", \"'a\")"}
|
|
187 |
\end{graybox}
|
|
188 |
\end{isabelle}
|
|
189 |
|
|
190 |
There are two reasons for parsing a term in a temporary theory. One is to
|
488
|
191 |
obtain fully qualified names for constants and the other is appropriate type
|
|
192 |
inference. This is relevant in situations where definitions are made later,
|
|
193 |
but parsing and type inference has to take already proceed as if the definitions
|
|
194 |
were already made.
|
348
|
195 |
*}
|
318
|
196 |
|
495
|
197 |
section {* Contexts *}
|
341
|
198 |
|
486
|
199 |
text {*
|
|
200 |
Contexts are arguably more important than theories, even though they only
|
|
201 |
contain ``short-term memory data''. The reason is that a vast number of
|
490
|
202 |
functions in Isabelle depend in one way or another on contexts. Even such
|
|
203 |
mundane operations like printing out a term make essential use of contexts.
|
494
|
204 |
For this consider the following contrived proof-snippet whose purpose is to
|
490
|
205 |
fix two variables:
|
486
|
206 |
*}
|
|
207 |
|
488
|
208 |
lemma "True"
|
|
209 |
proof -
|
491
|
210 |
txt_raw {*\mbox{}\\[-7mm]*}
|
492
|
211 |
ML_prf {* Variable.dest_fixes @{context} *}
|
491
|
212 |
txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
|
492
|
213 |
fix x y
|
491
|
214 |
txt_raw {*\mbox{}\\[-7mm]*}
|
488
|
215 |
ML_prf {* Variable.dest_fixes @{context} *}
|
491
|
216 |
txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
|
488
|
217 |
|
490
|
218 |
text {*
|
496
|
219 |
The interesting point is that we injected ML-code before and after
|
490
|
220 |
the variables are fixed. For this remember that ML-code inside a proof
|
494
|
221 |
needs to be enclosed inside \isacommand{ML\_prf}~@{text "\<verbopen> \<dots> \<verbclose>"},
|
490
|
222 |
not \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}. The function
|
|
223 |
@{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes
|
|
224 |
a context and returns all its currently fixed variable (names). That
|
|
225 |
means a context has a dataslot containing information about fixed variables.
|
|
226 |
The ML-antiquotation @{text "@{context}"} points to the context that is
|
|
227 |
active at that point of the theory. Consequently, in the first call to
|
|
228 |
@{ML dest_fixes in Variable} this dataslot is empty; in the second it is
|
|
229 |
filled with @{text x} and @{text y}. What is interesting is that contexts
|
494
|
230 |
can be stacked. For this consider the following proof fragment:
|
490
|
231 |
*}
|
|
232 |
|
|
233 |
lemma "True"
|
|
234 |
proof -
|
|
235 |
fix x y
|
|
236 |
{ fix z w
|
491
|
237 |
txt_raw {*\mbox{}\\[-7mm]*}
|
|
238 |
ML_prf {* Variable.dest_fixes @{context} *}
|
492
|
239 |
txt_raw {*\mbox{}\\[-7mm]\mbox{}*}
|
|
240 |
}
|
491
|
241 |
txt_raw {*\mbox{}\\[-7mm]*}
|
490
|
242 |
ML_prf {* Variable.dest_fixes @{context} *}
|
491
|
243 |
txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*)
|
|
244 |
|
|
245 |
text {*
|
495
|
246 |
Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables;
|
|
247 |
the second time we get only the fixes variables @{text x} and @{text y} as answer, since
|
|
248 |
@{text z} and @{text w} are not anymore in the scope of the context.
|
|
249 |
This means the curly-braces act on the Isabelle level as opening and closing statements
|
496
|
250 |
for a context. The above proof fragment corresponds roughly to the following ML-code
|
491
|
251 |
*}
|
488
|
252 |
|
492
|
253 |
ML{*val ctxt0 = @{context};
|
|
254 |
val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0;
|
|
255 |
val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*}
|
|
256 |
|
|
257 |
text {*
|
494
|
258 |
where the function @{ML_ind add_fixes in Variable} fixes a list of variables
|
|
259 |
specified by strings. Let us come back to the point about printing terms. Consider
|
495
|
260 |
printing out the term \mbox{@{text "(x, y, z, w)"}} using our function @{ML_ind pretty_term}.
|
496
|
261 |
This function takes a term and a context as argument. Notice how the printing
|
|
262 |
of the term changes with which context is used.
|
492
|
263 |
|
495
|
264 |
\begin{isabelle}
|
|
265 |
\begin{graybox}
|
|
266 |
@{ML "let
|
|
267 |
val trm = @{term \"(x, y, z, w)\"}
|
493
|
268 |
in
|
|
269 |
pwriteln (Pretty.chunks
|
|
270 |
[ pretty_term ctxt0 trm,
|
|
271 |
pretty_term ctxt1 trm,
|
|
272 |
pretty_term ctxt2 trm ])
|
495
|
273 |
end"}\\
|
|
274 |
\setlength{\fboxsep}{0mm}
|
|
275 |
@{text ">"}~@{text "("}\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~%
|
|
276 |
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~%
|
|
277 |
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~%
|
|
278 |
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}\\
|
|
279 |
@{text ">"}~@{text "("}\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~%
|
|
280 |
\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~%
|
|
281 |
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~%
|
|
282 |
\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}\\
|
|
283 |
@{text ">"}~@{text "("}\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~%
|
|
284 |
\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~%
|
|
285 |
\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~%
|
|
286 |
\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}
|
|
287 |
\end{graybox}
|
|
288 |
\end{isabelle}
|
|
289 |
|
|
290 |
|
|
291 |
The term we are printing is in all three cases the same---a tuple containing
|
496
|
292 |
four free variables. As you can see, however, in case of @{ML "ctxt0"} all
|
495
|
293 |
variables are highlighted indicating a problem, while in case of @{ML
|
|
294 |
"ctxt1"} @{text x} and @{text y} are printed as normal (blue) free
|
|
295 |
variables, but not @{text z} and @{text w}. In the last case all variables
|
|
296 |
are printed as expected. The point of this example is that the context
|
|
297 |
contains the information which variables are fixed, and designates all other
|
497
|
298 |
free variables as being alien or faulty. Therefore the highlighting.
|
|
299 |
While this seems like a minor detail, the concept of making the context aware
|
|
300 |
of fixed variables is actually quite useful. For example it prevents us from
|
|
301 |
fixing a variable twice
|
495
|
302 |
|
|
303 |
@{ML_response_fake [gray, display]
|
|
304 |
"@{context}
|
|
305 |
|> Variable.add_fixes [\"x\", \"x\"]"
|
|
306 |
"ERROR: Duplicate fixed variable(s): \"x\""}
|
|
307 |
|
496
|
308 |
More importantly it also allows us to easily create fresh free variables avoiding any
|
|
309 |
clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context
|
495
|
310 |
@{text ctxt1}. Next we want to create two fresh variables of type @{typ nat}
|
|
311 |
as variants of the string @{text [quotes] "x"}.
|
|
312 |
|
|
313 |
@{ML_response_fake [display, gray, linenos]
|
|
314 |
"let
|
|
315 |
val ctxt0 = @{context}
|
|
316 |
val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
|
|
317 |
val frees = replicate 2 (\"x\", @{typ nat})
|
|
318 |
in
|
|
319 |
(Variable.variant_frees ctxt0 [] frees,
|
|
320 |
Variable.variant_frees ctxt1 [] frees)
|
|
321 |
end"
|
|
322 |
"([(\"x\", \"nat\"), (\"xa\", \"nat\")],
|
|
323 |
[(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
|
|
324 |
|
496
|
325 |
As you can see, if we create the fresh variables with the context @{text ctxt0},
|
495
|
326 |
then we obtain @{text "x"} and @{text "xa"}; but in @{text ctxt1} we obtain @{text "xa"}
|
|
327 |
and @{text "xb"} avoiding @{text x}, which was fixed in this context.
|
|
328 |
|
496
|
329 |
Often one has the problem that given some terms, create fresh variables
|
|
330 |
avoiding any variable occurring in those terms. For this you can use the
|
495
|
331 |
function @{ML_ind declare_term in Variable} from the structure @{ML_struct Variable}.
|
|
332 |
|
|
333 |
@{ML_response_fake [gray, display]
|
|
334 |
"let
|
|
335 |
val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
|
|
336 |
val frees = replicate 2 (\"x\", @{typ nat})
|
|
337 |
in
|
|
338 |
Variable.variant_frees ctxt1 [] frees
|
|
339 |
end"
|
|
340 |
"[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
|
|
341 |
|
496
|
342 |
The result is @{text xb} and @{text xc} for the names of the fresh
|
|
343 |
variables. Note that @{ML_ind declare_term in Variable} does not fix the
|
|
344 |
variables; it just makes them ``known'' to the context. This is helpful when
|
|
345 |
parsing terms using the function @{ML_ind read_term in Syntax} from the
|
|
346 |
structure @{ML_struct Syntax}. Consider the following code:
|
495
|
347 |
|
|
348 |
@{ML_response_fake [gray, display]
|
|
349 |
"let
|
|
350 |
val ctxt0 = @{context}
|
|
351 |
val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
|
|
352 |
in
|
|
353 |
(Syntax.read_term ctxt0 \"x\",
|
|
354 |
Syntax.read_term ctxt1 \"x\")
|
|
355 |
end"
|
|
356 |
"(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
|
|
357 |
|
496
|
358 |
Parsing the string in the context @{text "ctxt0"} results in a free variable
|
|
359 |
with a default polymorphic type, but in case of @{text "ctxt1"} we obtain a
|
495
|
360 |
free variable of type @{typ nat} as previously declared. Which
|
496
|
361 |
type the parsed term receives depends upon the last declaration that
|
|
362 |
is made, as the next example illustrates.
|
495
|
363 |
|
|
364 |
@{ML_response_fake [gray, display]
|
|
365 |
"let
|
|
366 |
val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
|
|
367 |
val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
|
|
368 |
in
|
|
369 |
(Syntax.read_term ctxt1 \"x\",
|
|
370 |
Syntax.read_term ctxt2 \"x\")
|
|
371 |
end"
|
|
372 |
"(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
|
|
373 |
|
497
|
374 |
The most useful feature of contexts is that one can export terms and theorems
|
|
375 |
between contexts. Let us consider first the case of terms.
|
|
376 |
|
|
377 |
\begin{isabelle}
|
|
378 |
\begin{graybox}
|
|
379 |
\begin{linenos}
|
|
380 |
@{ML "let
|
|
381 |
val ctxt0 = @{context}
|
|
382 |
val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0
|
|
383 |
val foo_trm = @{term \"P x y z\"}
|
|
384 |
in
|
|
385 |
singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
|
|
386 |
|> pretty_term ctxt0
|
|
387 |
|> pwriteln
|
|
388 |
end"}
|
|
389 |
\end{linenos}
|
|
390 |
\setlength{\fboxsep}{0mm}
|
|
391 |
@{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%
|
|
392 |
@{text "?x ?y ?z"}
|
|
393 |
\end{graybox}
|
|
394 |
\end{isabelle}
|
|
395 |
|
|
396 |
In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in context @{text ctxt1}.
|
|
397 |
The function @{ML_ind export_terms in Variable} from the @{ML_struct Variable} can be used
|
|
398 |
to ``transfer'' terms between contexts. Transferring means to turn all (free) variables that
|
|
399 |
are fixed in one context, but not in the other, into schematic variables. In our example
|
|
400 |
we are transferring the term @{text "P x y z"} from context @{text "ctxt1"} into @{text "ctxt0"}
|
|
401 |
which means @{term x}, @{term y} and @{term z} become schematic variables (as can be seen
|
|
402 |
by the leading question mark). Note that the variable @{text P} stays a free variable, since
|
|
403 |
it not fixed in @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does not
|
|
404 |
know about it. Note also that in Line 6 we had to use the function @{ML_ind singleton},
|
|
405 |
because the function @{ML_ind export_terms in Variable} normally works over lists of terms.
|
|
406 |
|
|
407 |
|
495
|
408 |
*}
|
|
409 |
|
|
410 |
ML {*
|
|
411 |
let
|
|
412 |
val ctxt0 = @{context}
|
|
413 |
val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
|
496
|
414 |
val foo_trm = @{term "P x y z"}
|
|
415 |
in
|
|
416 |
singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
|
|
417 |
|> pretty_term ctxt1
|
|
418 |
|> pwriteln
|
|
419 |
end
|
|
420 |
*}
|
|
421 |
|
|
422 |
ML {*
|
|
423 |
let
|
|
424 |
val thy = @{theory}
|
|
425 |
val ctxt0 = @{context}
|
|
426 |
val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
|
|
427 |
val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
|
|
428 |
in
|
|
429 |
singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
|
|
430 |
end
|
|
431 |
*}
|
|
432 |
|
|
433 |
ML {*
|
|
434 |
let
|
|
435 |
val thy = @{theory}
|
|
436 |
val ctxt0 = @{context}
|
|
437 |
val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
|
|
438 |
val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}
|
495
|
439 |
in
|
|
440 |
singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
|
493
|
441 |
end
|
|
442 |
*}
|
|
443 |
|
495
|
444 |
text {*
|
493
|
445 |
|
|
446 |
*}
|
|
447 |
|
492
|
448 |
|
486
|
449 |
(*
|
|
450 |
ML{*Proof_Context.debug := true*}
|
|
451 |
ML{*Proof_Context.verbose := true*}
|
|
452 |
*)
|
|
453 |
|
487
|
454 |
(*
|
486
|
455 |
lemma "True"
|
|
456 |
proof -
|
|
457 |
{ -- "\<And>x. _"
|
|
458 |
fix x
|
|
459 |
have "B x" sorry
|
|
460 |
thm this
|
|
461 |
}
|
|
462 |
|
|
463 |
thm this
|
|
464 |
|
|
465 |
{ -- "A \<Longrightarrow> _"
|
|
466 |
assume A
|
|
467 |
have B sorry
|
|
468 |
thm this
|
|
469 |
}
|
|
470 |
|
|
471 |
thm this
|
|
472 |
|
|
473 |
{ -- "\<And>x. x = _ \<Longrightarrow> _"
|
|
474 |
def x \<equiv> a
|
|
475 |
have "B x" sorry
|
|
476 |
}
|
|
477 |
|
|
478 |
thm this
|
|
479 |
|
|
480 |
oops
|
487
|
481 |
*)
|
413
|
482 |
|
341
|
483 |
section {* Local Theories (TBD) *}
|
|
484 |
|
394
|
485 |
text {*
|
400
|
486 |
In contrast to an ordinary theory, which simply consists of a type
|
|
487 |
signature, as well as tables for constants, axioms and theorems, a local
|
|
488 |
theory contains additional context information, such as locally fixed
|
|
489 |
variables and local assumptions that may be used by the package. The type
|
|
490 |
@{ML_type local_theory} is identical to the type of \emph{proof contexts}
|
|
491 |
@{ML_type "Proof.context"}, although not every proof context constitutes a
|
|
492 |
valid local theory.
|
|
493 |
|
|
494 |
@{ML "Context.>> o Context.map_theory"}
|
394
|
495 |
@{ML_ind "Local_Theory.declaration"}
|
486
|
496 |
|
|
497 |
A similar command is \isacommand{local\_setup}, which expects a function
|
|
498 |
of type @{ML_type "local_theory -> local_theory"}. Later on we will also
|
|
499 |
use the commands \isacommand{method\_setup} for installing methods in the
|
|
500 |
current theory and \isacommand{simproc\_setup} for adding new simprocs to
|
|
501 |
the current simpset.
|
394
|
502 |
*}
|
318
|
503 |
|
336
|
504 |
|
394
|
505 |
section {* Morphisms (TBD) *}
|
|
506 |
|
|
507 |
text {*
|
|
508 |
Morphisms are arbitrary transformations over terms, types, theorems and bindings.
|
|
509 |
They can be constructed using the function @{ML_ind morphism in Morphism},
|
|
510 |
which expects a record with functions of type
|
|
511 |
|
|
512 |
\begin{isabelle}
|
|
513 |
\begin{tabular}{rl}
|
|
514 |
@{text "binding:"} & @{text "binding -> binding"}\\
|
|
515 |
@{text "typ:"} & @{text "typ -> typ"}\\
|
|
516 |
@{text "term:"} & @{text "term -> term"}\\
|
|
517 |
@{text "fact:"} & @{text "thm list -> thm list"}
|
|
518 |
\end{tabular}
|
|
519 |
\end{isabelle}
|
|
520 |
|
|
521 |
The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as
|
|
522 |
*}
|
|
523 |
|
481
|
524 |
ML{*val identity = Morphism.morphism {binding = [], typ = [], term = [], fact = []}*}
|
394
|
525 |
|
|
526 |
text {*
|
|
527 |
Morphisms can be composed with the function @{ML_ind "$>" in Morphism}
|
|
528 |
*}
|
|
529 |
|
|
530 |
ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T)
|
|
531 |
| trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)
|
|
532 |
| trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)
|
|
533 |
| trm_phi t = t*}
|
|
534 |
|
|
535 |
ML{*val phi = Morphism.term_morphism trm_phi*}
|
|
536 |
|
|
537 |
ML{*Morphism.term phi @{term "P x y"}*}
|
|
538 |
|
|
539 |
text {*
|
|
540 |
@{ML_ind term_morphism in Morphism}
|
|
541 |
|
|
542 |
@{ML_ind term in Morphism},
|
|
543 |
@{ML_ind thm in Morphism}
|
|
544 |
|
|
545 |
\begin{readmore}
|
|
546 |
Morphisms are implemented in the file @{ML_file "Pure/morphism.ML"}.
|
|
547 |
\end{readmore}
|
|
548 |
*}
|
318
|
549 |
|
|
550 |
section {* Misc (TBD) *}
|
|
551 |
|
|
552 |
ML {*Datatype.get_info @{theory} "List.list"*}
|
|
553 |
|
319
|
554 |
text {*
|
|
555 |
FIXME: association lists:
|
|
556 |
@{ML_file "Pure/General/alist.ML"}
|
|
557 |
|
|
558 |
FIXME: calling the ML-compiler
|
|
559 |
|
|
560 |
*}
|
|
561 |
|
414
|
562 |
section {* What Is In an Isabelle Name? (TBD) *}
|
|
563 |
|
|
564 |
text {*
|
|
565 |
On the ML-level of Isabelle, you often have to work with qualified names.
|
|
566 |
These are strings with some additional information, such as positional
|
|
567 |
information and qualifiers. Such qualified names can be generated with the
|
|
568 |
antiquotation @{text "@{binding \<dots>}"}. For example
|
|
569 |
|
|
570 |
@{ML_response [display,gray]
|
|
571 |
"@{binding \"name\"}"
|
|
572 |
"name"}
|
|
573 |
|
|
574 |
An example where a qualified name is needed is the function
|
|
575 |
@{ML_ind define in Local_Theory}. This function is used below to define
|
|
576 |
the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
|
|
577 |
*}
|
|
578 |
|
|
579 |
local_setup %gray {*
|
|
580 |
Local_Theory.define ((@{binding "TrueConj"}, NoSyn),
|
|
581 |
(Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
|
|
582 |
|
|
583 |
text {*
|
|
584 |
Now querying the definition you obtain:
|
|
585 |
|
|
586 |
\begin{isabelle}
|
|
587 |
\isacommand{thm}~@{text "TrueConj_def"}\\
|
|
588 |
@{text "> "}~@{thm TrueConj_def}
|
|
589 |
\end{isabelle}
|
|
590 |
|
|
591 |
\begin{readmore}
|
|
592 |
The basic operations on bindings are implemented in
|
|
593 |
@{ML_file "Pure/General/binding.ML"}.
|
|
594 |
\end{readmore}
|
|
595 |
|
|
596 |
\footnote{\bf FIXME give a better example why bindings are important}
|
|
597 |
\footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
|
|
598 |
why @{ML snd} is needed.}
|
|
599 |
\footnote{\bf FIXME: There should probably a separate section on binding, long-names
|
|
600 |
and sign.}
|
|
601 |
|
|
602 |
*}
|
|
603 |
|
318
|
604 |
|
360
|
605 |
ML {* Sign.intern_type @{theory} "list" *}
|
|
606 |
ML {* Sign.intern_const @{theory} "prod_fun" *}
|
|
607 |
|
414
|
608 |
text {*
|
|
609 |
\footnote{\bf FIXME: Explain the following better; maybe put in a separate
|
|
610 |
section and link with the comment in the antiquotation section.}
|
|
611 |
|
|
612 |
Occasionally you have to calculate what the ``base'' name of a given
|
462
|
613 |
constant is. For this you can use the function @{ML_ind Long_Name.base_name}. For example:
|
414
|
614 |
|
462
|
615 |
@{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
|
414
|
616 |
|
|
617 |
\begin{readmore}
|
|
618 |
Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
|
|
619 |
functions about signatures in @{ML_file "Pure/sign.ML"}.
|
|
620 |
\end{readmore}
|
|
621 |
*}
|
387
|
622 |
|
|
623 |
text {*
|
|
624 |
@{ML_ind "Binding.name_of"} returns the string without markup
|
394
|
625 |
|
|
626 |
@{ML_ind "Binding.conceal"}
|
387
|
627 |
*}
|
|
628 |
|
388
|
629 |
section {* Concurrency (TBD) *}
|
|
630 |
|
|
631 |
text {*
|
|
632 |
@{ML_ind prove_future in Goal}
|
|
633 |
@{ML_ind future_result in Goal}
|
|
634 |
@{ML_ind fork_pri in Future}
|
|
635 |
*}
|
387
|
636 |
|
396
|
637 |
section {* Parse and Print Translations (TBD) *}
|
|
638 |
|
349
|
639 |
section {* Summary *}
|
|
640 |
|
|
641 |
text {*
|
395
|
642 |
TBD
|
349
|
643 |
*}
|
318
|
644 |
|
|
645 |
end
|