395
|
1 |
theory Essential
|
441
|
2 |
imports Base First_Steps
|
318
|
3 |
begin
|
|
4 |
|
358
|
5 |
chapter {* Isabelle Essentials *}
|
318
|
6 |
|
319
|
7 |
text {*
|
410
|
8 |
\begin{flushright}
|
|
9 |
{\em One man's obfuscation is another man's abstraction.} \\[1ex]
|
|
10 |
Frank Ch.~Eigler on the Linux Kernel Mailing List,\\
|
|
11 |
24~Nov.~2009
|
|
12 |
\end{flushright}
|
|
13 |
|
|
14 |
\medskip
|
534
|
15 |
Isabelle is built around a few central ideas. One central idea is the
|
414
|
16 |
LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there
|
|
17 |
is a small trusted core and everything else is built on top of this trusted
|
|
18 |
core. The fundamental data structures involved in this core are certified
|
|
19 |
terms and certified types, as well as theorems.
|
319
|
20 |
*}
|
|
21 |
|
|
22 |
|
318
|
23 |
section {* Terms and Types *}
|
|
24 |
|
|
25 |
text {*
|
350
|
26 |
In Isabelle, there are certified terms and uncertified terms (respectively types).
|
|
27 |
Uncertified terms are often just called terms. One way to construct them is by
|
329
|
28 |
using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
|
318
|
29 |
|
|
30 |
@{ML_response [display,gray]
|
|
31 |
"@{term \"(a::nat) + b = c\"}"
|
451
|
32 |
"Const (\"HOL.eq\", \<dots>) $
|
418
|
33 |
(Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
|
318
|
34 |
|
350
|
35 |
constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
|
|
36 |
the internal representation corresponding to the datatype @{ML_type_ind "term"},
|
|
37 |
which is defined as follows:
|
318
|
38 |
*}
|
|
39 |
|
|
40 |
ML_val %linenosgray{*datatype term =
|
|
41 |
Const of string * typ
|
|
42 |
| Free of string * typ
|
|
43 |
| Var of indexname * typ
|
|
44 |
| Bound of int
|
|
45 |
| Abs of string * typ * term
|
|
46 |
| $ of term * term *}
|
|
47 |
|
|
48 |
text {*
|
345
|
49 |
This datatype implements Church-style lambda-terms, where types are
|
534
|
50 |
explicitly recorded in variables, constants and abstractions. The
|
|
51 |
important point of having terms is that you can pattern-match against them;
|
|
52 |
this cannot be done with certified terms. As can be seen in Line 5,
|
|
53 |
terms use the usual de Bruijn index mechanism for representing bound
|
|
54 |
variables. For example in
|
318
|
55 |
|
|
56 |
@{ML_response_fake [display, gray]
|
|
57 |
"@{term \"\<lambda>x y. x y\"}"
|
|
58 |
"Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
|
|
59 |
|
|
60 |
the indices refer to the number of Abstractions (@{ML Abs}) that we need to
|
|
61 |
skip until we hit the @{ML Abs} that binds the corresponding
|
|
62 |
variable. Constructing a term with dangling de Bruijn indices is possible,
|
|
63 |
but will be flagged as ill-formed when you try to typecheck or certify it
|
|
64 |
(see Section~\ref{sec:typechecking}). Note that the names of bound variables
|
|
65 |
are kept at abstractions for printing purposes, and so should be treated
|
|
66 |
only as ``comments''. Application in Isabelle is realised with the
|
|
67 |
term-constructor @{ML $}.
|
|
68 |
|
469
|
69 |
Be careful if you pretty-print terms. Consider pretty-printing the abstraction
|
|
70 |
term shown above:
|
|
71 |
|
|
72 |
@{ML_response_fake [display, gray]
|
|
73 |
"@{term \"\<lambda>x y. x y\"}
|
|
74 |
|> pretty_term @{context}
|
|
75 |
|> pwriteln"
|
|
76 |
"\<lambda>x. x"}
|
|
77 |
|
|
78 |
This is one common source for puzzlement in Isabelle, which has
|
|
79 |
tacitly eta-contracted the output. You obtain a similar result
|
|
80 |
with beta-redexes
|
|
81 |
|
|
82 |
@{ML_response_fake [display, gray]
|
534
|
83 |
"let
|
|
84 |
val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"}
|
|
85 |
val arg1 = @{term \"1::int\"}
|
|
86 |
val arg2 = @{term \"2::int\"}
|
|
87 |
in
|
|
88 |
pretty_term @{context} (redex $ arg1 $ arg2)
|
|
89 |
|> pwriteln
|
|
90 |
end"
|
469
|
91 |
"1"}
|
|
92 |
|
534
|
93 |
There is a dedicated configuration value for switching off tacit
|
|
94 |
eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section
|
507
|
95 |
\ref{sec:printing}), but none for beta-contractions. However you can avoid
|
534
|
96 |
the beta-contractions by switching off abbreviations using the configuration
|
507
|
97 |
value @{ML_ind show_abbrevs in Syntax}. For example
|
|
98 |
|
|
99 |
|
|
100 |
@{ML_response_fake [display, gray]
|
534
|
101 |
"let
|
|
102 |
val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"}
|
|
103 |
val arg1 = @{term \"1::int\"}
|
|
104 |
val arg2 = @{term \"2::int\"}
|
|
105 |
val ctxt = Config.put show_abbrevs false @{context}
|
|
106 |
in
|
|
107 |
pretty_term ctxt (redex $ arg1 $ arg2)
|
|
108 |
|> pwriteln
|
|
109 |
end"
|
507
|
110 |
"(\<lambda>x y. x) 1 2"}
|
469
|
111 |
|
318
|
112 |
Isabelle makes a distinction between \emph{free} variables (term-constructor
|
|
113 |
@{ML Free} and written on the user level in blue colour) and
|
|
114 |
\emph{schematic} variables (term-constructor @{ML Var} and written with a
|
|
115 |
leading question mark). Consider the following two examples
|
|
116 |
|
|
117 |
@{ML_response_fake [display, gray]
|
|
118 |
"let
|
|
119 |
val v1 = Var ((\"x\", 3), @{typ bool})
|
|
120 |
val v2 = Var ((\"x1\", 3), @{typ bool})
|
|
121 |
val v3 = Free (\"x\", @{typ bool})
|
|
122 |
in
|
441
|
123 |
pretty_terms @{context} [v1, v2, v3]
|
|
124 |
|> pwriteln
|
318
|
125 |
end"
|
|
126 |
"?x3, ?x1.3, x"}
|
|
127 |
|
502
|
128 |
When constructing terms, you are usually concerned with free
|
|
129 |
variables (as mentioned earlier, you cannot construct schematic
|
|
130 |
variables using the built in antiquotation \mbox{@{text "@{term
|
|
131 |
\<dots>}"}}). If you deal with theorems, you have to, however, observe the
|
|
132 |
distinction. The reason is that only schematic variables can be
|
|
133 |
instantiated with terms when a theorem is applied. A similar
|
|
134 |
distinction between free and schematic variables holds for types
|
318
|
135 |
(see below).
|
|
136 |
|
|
137 |
\begin{readmore}
|
|
138 |
Terms and types are described in detail in \isccite{sec:terms}. Their
|
|
139 |
definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
|
|
140 |
For constructing terms involving HOL constants, many helper functions are defined
|
|
141 |
in @{ML_file "HOL/Tools/hologic.ML"}.
|
|
142 |
\end{readmore}
|
|
143 |
|
|
144 |
Constructing terms via antiquotations has the advantage that only typable
|
|
145 |
terms can be constructed. For example
|
|
146 |
|
|
147 |
@{ML_response_fake_both [display,gray]
|
|
148 |
"@{term \"x x\"}"
|
|
149 |
"Type unification failed: Occurs check!"}
|
|
150 |
|
|
151 |
raises a typing error, while it perfectly ok to construct the term
|
414
|
152 |
with the raw ML-constructors:
|
318
|
153 |
|
|
154 |
@{ML_response_fake [display,gray]
|
|
155 |
"let
|
345
|
156 |
val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
|
318
|
157 |
in
|
441
|
158 |
pwriteln (pretty_term @{context} omega)
|
318
|
159 |
end"
|
|
160 |
"x x"}
|
|
161 |
|
|
162 |
Sometimes the internal representation of terms can be surprisingly different
|
|
163 |
from what you see at the user-level, because the layers of
|
|
164 |
parsing/type-checking/pretty printing can be quite elaborate.
|
|
165 |
|
|
166 |
\begin{exercise}
|
|
167 |
Look at the internal term representation of the following terms, and
|
|
168 |
find out why they are represented like this:
|
|
169 |
|
|
170 |
\begin{itemize}
|
|
171 |
\item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}
|
|
172 |
\item @{term "\<lambda>(x,y). P y x"}
|
|
173 |
\item @{term "{ [x::int] | x. x \<le> -2 }"}
|
|
174 |
\end{itemize}
|
|
175 |
|
|
176 |
Hint: The third term is already quite big, and the pretty printer
|
|
177 |
may omit parts of it by default. If you want to see all of it, you
|
|
178 |
can use the following ML-function to set the printing depth to a higher
|
|
179 |
value:
|
|
180 |
|
|
181 |
@{ML [display,gray] "print_depth 50"}
|
|
182 |
\end{exercise}
|
|
183 |
|
|
184 |
The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the
|
|
185 |
usually invisible @{text "Trueprop"}-coercions whenever necessary.
|
|
186 |
Consider for example the pairs
|
|
187 |
|
|
188 |
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
|
|
189 |
"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
|
448
|
190 |
Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
|
|
191 |
|
318
|
192 |
where a coercion is inserted in the second component and
|
|
193 |
|
|
194 |
@{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
|
|
195 |
"(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>,
|
|
196 |
Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
|
|
197 |
|
|
198 |
where it is not (since it is already constructed by a meta-implication).
|
|
199 |
The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
|
350
|
200 |
an object logic, for example HOL, into the meta-logic of Isabelle. The coercion
|
318
|
201 |
is needed whenever a term is constructed that will be proved as a theorem.
|
|
202 |
|
|
203 |
As already seen above, types can be constructed using the antiquotation
|
|
204 |
@{text "@{typ \<dots>}"}. For example:
|
|
205 |
|
|
206 |
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
|
|
207 |
|
|
208 |
The corresponding datatype is
|
|
209 |
*}
|
|
210 |
|
534
|
211 |
ML_val %grayML{*datatype typ =
|
318
|
212 |
Type of string * typ list
|
|
213 |
| TFree of string * sort
|
|
214 |
| TVar of indexname * sort *}
|
|
215 |
|
|
216 |
text {*
|
|
217 |
Like with terms, there is the distinction between free type
|
350
|
218 |
variables (term-constructor @{ML "TFree"}) and schematic
|
375
|
219 |
type variables (term-constructor @{ML "TVar"} and printed with
|
|
220 |
a leading question mark). A type constant,
|
318
|
221 |
like @{typ "int"} or @{typ bool}, are types with an empty list
|
375
|
222 |
of argument types. However, it needs a bit of effort to show an
|
|
223 |
example, because Isabelle always pretty prints types (unlike terms).
|
|
224 |
Using just the antiquotation @{text "@{typ \"bool\"}"} we only see
|
318
|
225 |
|
|
226 |
@{ML_response [display, gray]
|
375
|
227 |
"@{typ \"bool\"}"
|
|
228 |
"bool"}
|
414
|
229 |
which is the pretty printed version of @{text "bool"}. However, in PolyML
|
|
230 |
(version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the
|
393
|
231 |
function below we mimic the behaviour of the usual pretty printer for
|
|
232 |
datatypes (it uses pretty-printing functions which will be explained in more
|
|
233 |
detail in Section~\ref{sec:pretty}).
|
375
|
234 |
*}
|
|
235 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
236 |
ML %grayML{*local
|
393
|
237 |
fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
|
392
|
238 |
fun pp_list xs = Pretty.list "[" "]" xs
|
|
239 |
fun pp_str s = Pretty.str s
|
|
240 |
fun pp_qstr s = Pretty.quote (pp_str s)
|
|
241 |
fun pp_int i = pp_str (string_of_int i)
|
|
242 |
fun pp_sort S = pp_list (map pp_qstr S)
|
393
|
243 |
fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
|
392
|
244 |
in
|
393
|
245 |
fun raw_pp_typ (TVar ((a, i), S)) =
|
392
|
246 |
pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
|
393
|
247 |
| raw_pp_typ (TFree (a, S)) =
|
392
|
248 |
pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
|
393
|
249 |
| raw_pp_typ (Type (a, tys)) =
|
392
|
250 |
pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
|
375
|
251 |
end*}
|
|
252 |
|
|
253 |
text {*
|
|
254 |
We can install this pretty printer with the function
|
|
255 |
@{ML_ind addPrettyPrinter in PolyML} as follows.
|
|
256 |
*}
|
|
257 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
258 |
ML %grayML{*PolyML.addPrettyPrinter
|
393
|
259 |
(fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
|
388
|
260 |
|
375
|
261 |
text {*
|
377
|
262 |
Now the type bool is printed out in full detail.
|
375
|
263 |
|
|
264 |
@{ML_response [display,gray]
|
|
265 |
"@{typ \"bool\"}"
|
448
|
266 |
"Type (\"HOL.bool\", [])"}
|
375
|
267 |
|
|
268 |
When printing out a list-type
|
|
269 |
|
|
270 |
@{ML_response [display,gray]
|
|
271 |
"@{typ \"'a list\"}"
|
|
272 |
"Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
|
|
273 |
|
|
274 |
we can see the full name of the type is actually @{text "List.list"}, indicating
|
|
275 |
that it is defined in the theory @{text "List"}. However, one has to be
|
377
|
276 |
careful with names of types, because even if
|
482
|
277 |
@{text "fun"} is defined in the theory @{text "HOL"}, it is
|
375
|
278 |
still represented by their simple name.
|
|
279 |
|
|
280 |
@{ML_response [display,gray]
|
|
281 |
"@{typ \"bool \<Rightarrow> nat\"}"
|
448
|
282 |
"Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
|
375
|
283 |
|
|
284 |
We can restore the usual behaviour of Isabelle's pretty printer
|
|
285 |
with the code
|
|
286 |
*}
|
|
287 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
288 |
ML %grayML{*PolyML.addPrettyPrinter
|
393
|
289 |
(fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
|
375
|
290 |
|
|
291 |
text {*
|
|
292 |
After that the types for booleans, lists and so on are printed out again
|
|
293 |
the standard Isabelle way.
|
|
294 |
|
|
295 |
@{ML_response_fake [display, gray]
|
|
296 |
"@{typ \"bool\"};
|
|
297 |
@{typ \"'a list\"}"
|
|
298 |
"\"bool\"
|
|
299 |
\"'a List.list\""}
|
318
|
300 |
|
|
301 |
\begin{readmore}
|
|
302 |
Types are described in detail in \isccite{sec:types}. Their
|
|
303 |
definition and many useful operations are implemented
|
|
304 |
in @{ML_file "Pure/type.ML"}.
|
|
305 |
\end{readmore}
|
|
306 |
*}
|
|
307 |
|
|
308 |
section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
|
|
309 |
|
|
310 |
text {*
|
|
311 |
While antiquotations are very convenient for constructing terms, they can
|
|
312 |
only construct fixed terms (remember they are ``linked'' at compile-time).
|
335
|
313 |
However, you often need to construct terms manually. For example, a
|
318
|
314 |
function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
|
|
315 |
@{term P} and @{term Q} as arguments can only be written as:
|
|
316 |
|
|
317 |
*}
|
|
318 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
319 |
ML %grayML{*fun make_imp P Q =
|
318
|
320 |
let
|
|
321 |
val x = Free ("x", @{typ nat})
|
|
322 |
in
|
|
323 |
Logic.all x (Logic.mk_implies (P $ x, Q $ x))
|
|
324 |
end *}
|
|
325 |
|
|
326 |
text {*
|
|
327 |
The reason is that you cannot pass the arguments @{term P} and @{term Q}
|
|
328 |
into an antiquotation.\footnote{At least not at the moment.} For example
|
|
329 |
the following does \emph{not} work.
|
|
330 |
*}
|
|
331 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
332 |
ML %grayML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
|
318
|
333 |
|
|
334 |
text {*
|
|
335 |
To see this, apply @{text "@{term S}"} and @{text "@{term T}"}
|
|
336 |
to both functions. With @{ML make_imp} you obtain the intended term involving
|
|
337 |
the given arguments
|
|
338 |
|
|
339 |
@{ML_response [display,gray] "make_imp @{term S} @{term T}"
|
|
340 |
"Const \<dots> $
|
439
|
341 |
Abs (\"x\", Type (\"Nat.nat\",[]),
|
318
|
342 |
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
|
|
343 |
|
|
344 |
whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"}
|
|
345 |
and @{text "Q"} from the antiquotation.
|
|
346 |
|
|
347 |
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}"
|
|
348 |
"Const \<dots> $
|
|
349 |
Abs (\"x\", \<dots>,
|
|
350 |
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
|
|
351 |
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
|
|
352 |
|
345
|
353 |
There are a number of handy functions that are frequently used for
|
|
354 |
constructing terms. One is the function @{ML_ind list_comb in Term}, which
|
350
|
355 |
takes as argument a term and a list of terms, and produces as output the
|
345
|
356 |
term list applied to the term. For example
|
|
357 |
|
318
|
358 |
|
|
359 |
@{ML_response_fake [display,gray]
|
|
360 |
"let
|
414
|
361 |
val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}
|
318
|
362 |
val args = [@{term \"True\"}, @{term \"False\"}]
|
|
363 |
in
|
|
364 |
list_comb (trm, args)
|
|
365 |
end"
|
414
|
366 |
"Free (\"P\", \"bool \<Rightarrow> bool \<Rightarrow> bool\")
|
|
367 |
$ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
|
318
|
368 |
|
345
|
369 |
Another handy function is @{ML_ind lambda in Term}, which abstracts a variable
|
318
|
370 |
in a term. For example
|
|
371 |
|
|
372 |
@{ML_response_fake [display,gray]
|
|
373 |
"let
|
|
374 |
val x_nat = @{term \"x::nat\"}
|
|
375 |
val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
|
|
376 |
in
|
|
377 |
lambda x_nat trm
|
|
378 |
end"
|
439
|
379 |
"Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
|
318
|
380 |
|
|
381 |
In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}),
|
350
|
382 |
and an abstraction, where it also records the type of the abstracted
|
318
|
383 |
variable and for printing purposes also its name. Note that because of the
|
|
384 |
typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
|
|
385 |
is of the same type as the abstracted variable. If it is of different type,
|
|
386 |
as in
|
|
387 |
|
|
388 |
@{ML_response_fake [display,gray]
|
|
389 |
"let
|
|
390 |
val x_int = @{term \"x::int\"}
|
|
391 |
val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
|
|
392 |
in
|
|
393 |
lambda x_int trm
|
|
394 |
end"
|
|
395 |
"Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
|
|
396 |
|
482
|
397 |
then the variable @{text "Free (\"x\", \"nat\")"} is \emph{not} abstracted.
|
318
|
398 |
This is a fundamental principle
|
|
399 |
of Church-style typing, where variables with the same name still differ, if they
|
|
400 |
have different type.
|
|
401 |
|
345
|
402 |
There is also the function @{ML_ind subst_free in Term} with which terms can be
|
318
|
403 |
replaced by other terms. For example below, we will replace in @{term
|
|
404 |
"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
|
|
405 |
@{term y}, and @{term x} by @{term True}.
|
|
406 |
|
|
407 |
@{ML_response_fake [display,gray]
|
|
408 |
"let
|
|
409 |
val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
|
|
410 |
val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
|
|
411 |
val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
|
|
412 |
in
|
|
413 |
subst_free [sub1, sub2] trm
|
|
414 |
end"
|
|
415 |
"Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
|
|
416 |
|
|
417 |
As can be seen, @{ML subst_free} does not take typability into account.
|
|
418 |
However it takes alpha-equivalence into account:
|
|
419 |
|
|
420 |
@{ML_response_fake [display, gray]
|
|
421 |
"let
|
|
422 |
val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
|
|
423 |
val trm = @{term \"(\<lambda>x::nat. x)\"}
|
|
424 |
in
|
|
425 |
subst_free [sub] trm
|
|
426 |
end"
|
|
427 |
"Free (\"x\", \"nat\")"}
|
|
428 |
|
345
|
429 |
Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound
|
318
|
430 |
variables with terms. To see how this function works, let us implement a
|
469
|
431 |
function that strips off the outermost forall quantifiers in a term.
|
318
|
432 |
*}
|
|
433 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
434 |
ML %grayML{*fun strip_alls t =
|
352
|
435 |
let
|
|
436 |
fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
|
|
437 |
in
|
|
438 |
case t of
|
469
|
439 |
Const (@{const_name All}, _) $ Abs body => aux body
|
352
|
440 |
| _ => ([], t)
|
|
441 |
end*}
|
318
|
442 |
|
|
443 |
text {*
|
|
444 |
The function returns a pair consisting of the stripped off variables and
|
350
|
445 |
the body of the universal quantification. For example
|
318
|
446 |
|
|
447 |
@{ML_response_fake [display, gray]
|
|
448 |
"strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
|
|
449 |
"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
|
|
450 |
Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
|
|
451 |
|
469
|
452 |
Note that we produced in the body two dangling de Bruijn indices.
|
|
453 |
Later on we will also use the inverse function that
|
|
454 |
builds the quantification from a body and a list of (free) variables.
|
|
455 |
*}
|
|
456 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
457 |
ML %grayML{*fun build_alls ([], t) = t
|
469
|
458 |
| build_alls (Free (x, T) :: vs, t) =
|
|
459 |
Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool})
|
|
460 |
$ Abs (x, T, build_alls (vs, t))*}
|
|
461 |
|
|
462 |
text {*
|
|
463 |
As said above, after calling @{ML strip_alls}, you obtain a term with loose
|
|
464 |
bound variables. With the function @{ML subst_bounds}, you can replace these
|
|
465 |
loose @{ML_ind Bound in Term}s with the stripped off variables.
|
318
|
466 |
|
|
467 |
@{ML_response_fake [display, gray, linenos]
|
|
468 |
"let
|
|
469 |
val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
|
|
470 |
in
|
|
471 |
subst_bounds (rev vrs, trm)
|
441
|
472 |
|> pretty_term @{context}
|
|
473 |
|> pwriteln
|
318
|
474 |
end"
|
|
475 |
"x = y"}
|
|
476 |
|
352
|
477 |
Note that in Line 4 we had to reverse the list of variables that @{ML
|
|
478 |
strip_alls} returned. The reason is that the head of the list the function
|
|
479 |
@{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next
|
|
480 |
element for @{ML "Bound 1"} and so on.
|
|
481 |
|
|
482 |
Notice also that this function might introduce name clashes, since we
|
|
483 |
substitute just a variable with the name recorded in an abstraction. This
|
|
484 |
name is by no means unique. If clashes need to be avoided, then we should
|
|
485 |
use the function @{ML_ind dest_abs in Term}, which returns the body where
|
469
|
486 |
the loose de Bruijn index is replaced by a unique free variable. For example
|
352
|
487 |
|
|
488 |
|
|
489 |
@{ML_response_fake [display,gray]
|
|
490 |
"let
|
374
|
491 |
val body = Bound 0 $ Free (\"x\", @{typ nat})
|
352
|
492 |
in
|
374
|
493 |
Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
|
352
|
494 |
end"
|
439
|
495 |
"(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"}
|
318
|
496 |
|
469
|
497 |
Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
|
|
498 |
There are many functions to do this. We describe only two. The first,
|
|
499 |
@{ML_ind incr_boundvars in Term}, increases by an integer the indices
|
|
500 |
of the loose bound variables in a term. In the code below
|
|
501 |
|
|
502 |
@{ML_response_fake [display,gray]
|
|
503 |
"@{term \"\<forall>x y z u. z = u\"}
|
|
504 |
|> strip_alls
|
|
505 |
||> incr_boundvars 2
|
|
506 |
|> build_alls
|
|
507 |
|> pretty_term @{context}
|
|
508 |
|> pwriteln"
|
|
509 |
"\<forall>x y z u. x = y"}
|
|
510 |
|
|
511 |
we first strip off the forall-quantified variables (thus creating two loose
|
|
512 |
bound variables in the body); then we increase the indices of the loose
|
|
513 |
bound variables by @{ML 2} and finally re-quantify the variables. As a
|
|
514 |
result of @{ML incr_boundvars}, we obtain now a term that has the equation
|
|
515 |
between the first two quantified variables.
|
|
516 |
|
|
517 |
The second function, @{ML_ind loose_bvar1 in Text}, tests whether a term
|
|
518 |
contains a loose bound of a certain index. For example
|
|
519 |
|
|
520 |
@{ML_response_fake [gray,display]
|
|
521 |
"let
|
|
522 |
val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"})
|
|
523 |
in
|
|
524 |
[loose_bvar1 (body, 0),
|
|
525 |
loose_bvar1 (body, 1),
|
|
526 |
loose_bvar1 (body, 2)]
|
|
527 |
end"
|
|
528 |
"[true, true, false]"}
|
|
529 |
|
350
|
530 |
There are also many convenient functions that construct specific HOL-terms
|
414
|
531 |
in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in
|
|
532 |
HOLogic} constructs an equality out of two terms. The types needed in this
|
|
533 |
equality are calculated from the type of the arguments. For example
|
318
|
534 |
|
|
535 |
@{ML_response_fake [gray,display]
|
|
536 |
"let
|
|
537 |
val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
|
|
538 |
in
|
441
|
539 |
eq |> pretty_term @{context}
|
|
540 |
|> pwriteln
|
318
|
541 |
end"
|
|
542 |
"True = False"}
|
414
|
543 |
|
318
|
544 |
\begin{readmore}
|
|
545 |
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
|
374
|
546 |
"Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make manual
|
318
|
547 |
constructions of terms and types easier.
|
|
548 |
\end{readmore}
|
|
549 |
|
|
550 |
When constructing terms manually, there are a few subtle issues with
|
|
551 |
constants. They usually crop up when pattern matching terms or types, or
|
|
552 |
when constructing them. While it is perfectly ok to write the function
|
|
553 |
@{text is_true} as follows
|
|
554 |
*}
|
|
555 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
556 |
ML %grayML{*fun is_true @{term True} = true
|
318
|
557 |
| is_true _ = false*}
|
|
558 |
|
|
559 |
text {*
|
|
560 |
this does not work for picking out @{text "\<forall>"}-quantified terms. Because
|
|
561 |
the function
|
|
562 |
*}
|
|
563 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
564 |
ML %grayML{*fun is_all (@{term All} $ _) = true
|
318
|
565 |
| is_all _ = false*}
|
|
566 |
|
|
567 |
text {*
|
|
568 |
will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}:
|
|
569 |
|
|
570 |
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
|
|
571 |
|
|
572 |
The problem is that the @{text "@term"}-antiquotation in the pattern
|
|
573 |
fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
|
|
574 |
an arbitrary, but fixed type @{typ "'a"}. A properly working alternative
|
|
575 |
for this function is
|
|
576 |
*}
|
|
577 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
578 |
ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true
|
318
|
579 |
| is_all _ = false*}
|
|
580 |
|
|
581 |
text {*
|
|
582 |
because now
|
|
583 |
|
448
|
584 |
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
|
318
|
585 |
|
|
586 |
matches correctly (the first wildcard in the pattern matches any type and the
|
|
587 |
second any term).
|
|
588 |
|
|
589 |
However there is still a problem: consider the similar function that
|
|
590 |
attempts to pick out @{text "Nil"}-terms:
|
|
591 |
*}
|
|
592 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
593 |
ML %grayML{*fun is_nil (Const ("Nil", _)) = true
|
318
|
594 |
| is_nil _ = false *}
|
|
595 |
|
|
596 |
text {*
|
|
597 |
Unfortunately, also this function does \emph{not} work as expected, since
|
|
598 |
|
|
599 |
@{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
|
|
600 |
|
|
601 |
The problem is that on the ML-level the name of a constant is more
|
|
602 |
subtle than you might expect. The function @{ML is_all} worked correctly,
|
|
603 |
because @{term "All"} is such a fundamental constant, which can be referenced
|
|
604 |
by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
|
|
605 |
|
|
606 |
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
|
|
607 |
|
|
608 |
the name of the constant @{text "Nil"} depends on the theory in which the
|
|
609 |
term constructor is defined (@{text "List"}) and also in which datatype
|
|
610 |
(@{text "list"}). Even worse, some constants have a name involving
|
|
611 |
type-classes. Consider for example the constants for @{term "zero"} and
|
|
612 |
\mbox{@{text "(op *)"}}:
|
|
613 |
|
|
614 |
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"(op *)\"})"
|
418
|
615 |
"(Const (\"Groups.zero_class.zero\", \<dots>),
|
|
616 |
Const (\"Groups.times_class.times\", \<dots>))"}
|
318
|
617 |
|
|
618 |
While you could use the complete name, for example
|
|
619 |
@{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
|
|
620 |
matching against @{text "Nil"}, this would make the code rather brittle.
|
|
621 |
The reason is that the theory and the name of the datatype can easily change.
|
|
622 |
To make the code more robust, it is better to use the antiquotation
|
|
623 |
@{text "@{const_name \<dots>}"}. With this antiquotation you can harness the
|
|
624 |
variable parts of the constant's name. Therefore a function for
|
|
625 |
matching against constants that have a polymorphic type should
|
|
626 |
be written as follows.
|
|
627 |
*}
|
|
628 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
629 |
ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
|
318
|
630 |
| is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
|
|
631 |
| is_nil_or_all _ = false *}
|
|
632 |
|
|
633 |
text {*
|
|
634 |
The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
|
|
635 |
For example
|
|
636 |
|
|
637 |
@{ML_response [display,gray]
|
|
638 |
"@{type_name \"list\"}" "\"List.list\""}
|
|
639 |
|
|
640 |
Although types of terms can often be inferred, there are many
|
|
641 |
situations where you need to construct types manually, especially
|
|
642 |
when defining constants. For example the function returning a function
|
|
643 |
type is as follows:
|
|
644 |
|
|
645 |
*}
|
|
646 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
647 |
ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
|
318
|
648 |
|
345
|
649 |
text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
|
318
|
650 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
651 |
ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
|
318
|
652 |
|
|
653 |
text {*
|
|
654 |
If you want to construct a function type with more than one argument
|
345
|
655 |
type, then you can use @{ML_ind "--->" in Term}.
|
318
|
656 |
*}
|
|
657 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
658 |
ML %grayML{*fun make_fun_types tys ty = tys ---> ty *}
|
318
|
659 |
|
|
660 |
text {*
|
369
|
661 |
A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a
|
318
|
662 |
function and applies it to every type in a term. You can, for example,
|
|
663 |
change every @{typ nat} in a term into an @{typ int} using the function:
|
|
664 |
*}
|
|
665 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
666 |
ML %grayML{*fun nat_to_int ty =
|
318
|
667 |
(case ty of
|
|
668 |
@{typ nat} => @{typ int}
|
|
669 |
| Type (s, tys) => Type (s, map nat_to_int tys)
|
|
670 |
| _ => ty)*}
|
|
671 |
|
|
672 |
text {*
|
|
673 |
Here is an example:
|
|
674 |
|
|
675 |
@{ML_response_fake [display,gray]
|
|
676 |
"map_types nat_to_int @{term \"a = (1::nat)\"}"
|
|
677 |
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
|
|
678 |
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
|
|
679 |
|
|
680 |
If you want to obtain the list of free type-variables of a term, you
|
|
681 |
can use the function @{ML_ind add_tfrees in Term}
|
|
682 |
(similarly @{ML_ind add_tvars in Term} for the schematic type-variables).
|
|
683 |
One would expect that such functions
|
|
684 |
take a term as input and return a list of types. But their type is actually
|
|
685 |
|
|
686 |
@{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}
|
|
687 |
|
|
688 |
that is they take, besides a term, also a list of type-variables as input.
|
|
689 |
So in order to obtain the list of type-variables of a term you have to
|
|
690 |
call them as follows
|
|
691 |
|
|
692 |
@{ML_response [gray,display]
|
|
693 |
"Term.add_tfrees @{term \"(a, b)\"} []"
|
|
694 |
"[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
|
|
695 |
|
|
696 |
The reason for this definition is that @{ML add_tfrees in Term} can
|
|
697 |
be easily folded over a list of terms. Similarly for all functions
|
|
698 |
named @{text "add_*"} in @{ML_file "Pure/term.ML"}.
|
|
699 |
|
|
700 |
\begin{exercise}\label{fun:revsum}
|
|
701 |
Write a function @{text "rev_sum : term -> term"} that takes a
|
|
702 |
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be one)
|
|
703 |
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
|
|
704 |
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
|
|
705 |
associates to the left. Try your function on some examples.
|
|
706 |
\end{exercise}
|
|
707 |
|
|
708 |
\begin{exercise}\label{fun:makesum}
|
350
|
709 |
Write a function that takes two terms representing natural numbers
|
318
|
710 |
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
|
|
711 |
number representing their sum.
|
|
712 |
\end{exercise}
|
|
713 |
|
469
|
714 |
\begin{exercise}\label{fun:killqnt}
|
|
715 |
Write a function that removes trivial forall and exists quantifiers that do not
|
|
716 |
quantify over any variables. For example the term @{term "\<forall>x y z. P x = P
|
|
717 |
z"} should be transformed to @{term "\<forall>x z. P x = P z"}, deleting the
|
|
718 |
quantification @{term "y"}. Hint: use the functions @{ML incr_boundvars}
|
|
719 |
and @{ML loose_bvar1}.
|
|
720 |
\end{exercise}
|
|
721 |
|
446
|
722 |
\begin{exercise}\label{fun:makelist}
|
|
723 |
Write a function that takes an integer @{text i} and
|
|
724 |
produces an Isabelle integer list from @{text 1} upto @{text i},
|
|
725 |
and then builds the reverse of this list using @{const rev}.
|
|
726 |
The relevant helper functions are @{ML upto},
|
|
727 |
@{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}.
|
|
728 |
\end{exercise}
|
|
729 |
|
329
|
730 |
\begin{exercise}\label{ex:debruijn}
|
350
|
731 |
Implement the function, which we below name deBruijn, that depends on a natural
|
318
|
732 |
number n$>$0 and constructs terms of the form:
|
|
733 |
|
|
734 |
\begin{center}
|
|
735 |
\begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
|
|
736 |
{\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i}\\
|
|
737 |
{\it lhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n. P\,i = P (i + 1 mod n)}
|
|
738 |
$\longrightarrow$ {\it rhs n}\\
|
|
739 |
{\it deBruijn n} & $\dn$ & {\it lhs n} $\longrightarrow$ {\it rhs n}\\
|
|
740 |
\end{tabular}
|
|
741 |
\end{center}
|
|
742 |
|
329
|
743 |
This function returns for n=3 the term
|
318
|
744 |
|
|
745 |
\begin{center}
|
|
746 |
\begin{tabular}{l}
|
|
747 |
(P 1 = P 2 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\
|
|
748 |
(P 2 = P 3 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\wedge$\\
|
|
749 |
(P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3
|
|
750 |
\end{tabular}
|
|
751 |
\end{center}
|
|
752 |
|
|
753 |
Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
|
350
|
754 |
for constructing the terms for the logical connectives.\footnote{Thanks to Roy
|
353
|
755 |
Dyckhoff for suggesting this exercise and working out the details.}
|
318
|
756 |
\end{exercise}
|
|
757 |
*}
|
|
758 |
|
412
|
759 |
section {* Unification and Matching\label{sec:univ} *}
|
377
|
760 |
|
|
761 |
text {*
|
386
|
762 |
As seen earlier, Isabelle's terms and types may contain schematic term variables
|
378
|
763 |
(term-constructor @{ML Var}) and schematic type variables (term-constructor
|
381
|
764 |
@{ML TVar}). These variables stand for unknown entities, which can be made
|
|
765 |
more concrete by instantiations. Such instantiations might be a result of
|
|
766 |
unification or matching. While in case of types, unification and matching is
|
|
767 |
relatively straightforward, in case of terms the algorithms are
|
|
768 |
substantially more complicated, because terms need higher-order versions of
|
|
769 |
the unification and matching algorithms. Below we shall use the
|
|
770 |
antiquotations @{text "@{typ_pat \<dots>}"} and @{text "@{term_pat \<dots>}"} from
|
|
771 |
Section~\ref{sec:antiquote} in order to construct examples involving
|
|
772 |
schematic variables.
|
|
773 |
|
403
|
774 |
Let us begin with describing the unification and matching functions for
|
383
|
775 |
types. Both return type environments (ML-type @{ML_type "Type.tyenv"})
|
|
776 |
which map schematic type variables to types and sorts. Below we use the
|
381
|
777 |
function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
|
|
778 |
for unifying the types @{text "?'a * ?'b"} and @{text "?'b list *
|
|
779 |
nat"}. This will produce the mapping, or type environment, @{text "[?'a :=
|
|
780 |
?'b list, ?'b := nat]"}.
|
378
|
781 |
*}
|
|
782 |
|
382
|
783 |
ML %linenosgray{*val (tyenv_unif, _) = let
|
379
|
784 |
val ty1 = @{typ_pat "?'a * ?'b"}
|
|
785 |
val ty2 = @{typ_pat "?'b list * nat"}
|
378
|
786 |
in
|
|
787 |
Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
|
|
788 |
end*}
|
|
789 |
|
|
790 |
text {*
|
383
|
791 |
The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
|
|
792 |
environment, which is needed for starting the unification without any
|
386
|
793 |
(pre)instantiations. The @{text 0} is an integer index that will be explained
|
414
|
794 |
below. In case of failure, @{ML typ_unify in Sign} will throw the exception
|
386
|
795 |
@{text TUNIFY}. We can print out the resulting type environment bound to
|
|
796 |
@{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
|
383
|
797 |
structure @{ML_struct Vartab}.
|
378
|
798 |
|
|
799 |
@{ML_response_fake [display,gray]
|
|
800 |
"Vartab.dest tyenv_unif"
|
|
801 |
"[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
|
381
|
802 |
((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
|
377
|
803 |
*}
|
|
804 |
|
381
|
805 |
text_raw {*
|
|
806 |
\begin{figure}[t]
|
|
807 |
\begin{minipage}{\textwidth}
|
|
808 |
\begin{isabelle}*}
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
809 |
ML %grayML{*fun pretty_helper aux env =
|
381
|
810 |
env |> Vartab.dest
|
448
|
811 |
|> map aux
|
|
812 |
|> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
|
|
813 |
|> Pretty.enum "," "[" "]"
|
441
|
814 |
|> pwriteln
|
381
|
815 |
|
|
816 |
fun pretty_tyenv ctxt tyenv =
|
378
|
817 |
let
|
389
|
818 |
fun get_typs (v, (s, T)) = (TVar (v, s), T)
|
441
|
819 |
val print = pairself (pretty_typ ctxt)
|
381
|
820 |
in
|
389
|
821 |
pretty_helper (print o get_typs) tyenv
|
378
|
822 |
end*}
|
381
|
823 |
text_raw {*
|
|
824 |
\end{isabelle}
|
|
825 |
\end{minipage}
|
|
826 |
\caption{A pretty printing function for type environments, which are
|
|
827 |
produced by unification and matching.\label{fig:prettyenv}}
|
|
828 |
\end{figure}
|
|
829 |
*}
|
377
|
830 |
|
378
|
831 |
text {*
|
381
|
832 |
The first components in this list stand for the schematic type variables and
|
383
|
833 |
the second are the associated sorts and types. In this example the sort is
|
386
|
834 |
the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will
|
|
835 |
use in what follows our own pretty-printing function from
|
|
836 |
Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
|
|
837 |
environment in the example this function prints out the more legible:
|
|
838 |
|
378
|
839 |
|
|
840 |
@{ML_response_fake [display, gray]
|
|
841 |
"pretty_tyenv @{context} tyenv_unif"
|
|
842 |
"[?'a := ?'b list, ?'b := nat]"}
|
377
|
843 |
|
383
|
844 |
The way the unification function @{ML typ_unify in Sign} is implemented
|
|
845 |
using an initial type environment and initial index makes it easy to
|
|
846 |
unify more than two terms. For example
|
|
847 |
*}
|
|
848 |
|
|
849 |
ML %linenosgray{*val (tyenvs, _) = let
|
|
850 |
val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
|
|
851 |
val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
|
|
852 |
in
|
|
853 |
fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0)
|
|
854 |
end*}
|
|
855 |
|
|
856 |
text {*
|
|
857 |
The index @{text 0} in Line 5 is the maximal index of the schematic type
|
387
|
858 |
variables occurring in @{text tys1} and @{text tys2}. This index will be
|
383
|
859 |
increased whenever a new schematic type variable is introduced during
|
|
860 |
unification. This is for example the case when two schematic type variables
|
|
861 |
have different, incomparable sorts. Then a new schematic type variable is
|
|
862 |
introduced with the combined sorts. To show this let us assume two sorts,
|
|
863 |
say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
|
|
864 |
variables @{text "?'a"} and @{text "?'b"}. Since we do not make any
|
|
865 |
assumption about the sorts, they are incomparable.
|
381
|
866 |
*}
|
|
867 |
|
418
|
868 |
class s1
|
|
869 |
class s2
|
|
870 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
871 |
ML %grayML{*val (tyenv, index) = let
|
383
|
872 |
val ty1 = @{typ_pat "?'a::s1"}
|
|
873 |
val ty2 = @{typ_pat "?'b::s2"}
|
381
|
874 |
in
|
|
875 |
Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
|
|
876 |
end*}
|
|
877 |
|
|
878 |
text {*
|
383
|
879 |
To print out the result type environment we switch on the printing
|
|
880 |
of sort information by setting @{ML_ind show_sorts in Syntax} to
|
|
881 |
true. This allows us to inspect the typing environment.
|
381
|
882 |
|
|
883 |
@{ML_response_fake [display,gray]
|
|
884 |
"pretty_tyenv @{context} tyenv"
|
387
|
885 |
"[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
|
381
|
886 |
|
383
|
887 |
As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated
|
387
|
888 |
with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new
|
381
|
889 |
type variable has been introduced the @{ML index}, originally being @{text 0},
|
387
|
890 |
has been increased to @{text 1}.
|
381
|
891 |
|
|
892 |
@{ML_response [display,gray]
|
|
893 |
"index"
|
|
894 |
"1"}
|
383
|
895 |
|
386
|
896 |
Let us now return to the unification problem @{text "?'a * ?'b"} and
|
|
897 |
@{text "?'b list * nat"} from the beginning of this section, and the
|
383
|
898 |
calculated type environment @{ML tyenv_unif}:
|
381
|
899 |
|
|
900 |
@{ML_response_fake [display, gray]
|
|
901 |
"pretty_tyenv @{context} tyenv_unif"
|
|
902 |
"[?'a := ?'b list, ?'b := nat]"}
|
|
903 |
|
|
904 |
Observe that the type environment which the function @{ML typ_unify in
|
399
|
905 |
Sign} returns is \emph{not} an instantiation in fully solved form: while @{text
|
378
|
906 |
"?'b"} is instantiated to @{typ nat}, this is not propagated to the
|
|
907 |
instantiation for @{text "?'a"}. In unification theory, this is often
|
386
|
908 |
called an instantiation in \emph{triangular form}. These triangular
|
|
909 |
instantiations, or triangular type environments, are used because of
|
|
910 |
performance reasons. To apply such a type environment to a type, say @{text "?'a *
|
378
|
911 |
?'b"}, you should use the function @{ML_ind norm_type in Envir}:
|
377
|
912 |
|
378
|
913 |
@{ML_response_fake [display, gray]
|
|
914 |
"Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
|
|
915 |
"nat list * nat"}
|
381
|
916 |
|
378
|
917 |
Matching of types can be done with the function @{ML_ind typ_match in Sign}
|
383
|
918 |
also from the structure @{ML_struct Sign}. This function returns a @{ML_type
|
|
919 |
Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
|
381
|
920 |
of failure. For example
|
378
|
921 |
*}
|
|
922 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
923 |
ML %grayML{*val tyenv_match = let
|
378
|
924 |
val pat = @{typ_pat "?'a * ?'b"}
|
|
925 |
and ty = @{typ_pat "bool list * nat"}
|
|
926 |
in
|
|
927 |
Sign.typ_match @{theory} (pat, ty) Vartab.empty
|
|
928 |
end*}
|
377
|
929 |
|
|
930 |
text {*
|
381
|
931 |
Printing out the calculated matcher gives
|
378
|
932 |
|
|
933 |
@{ML_response_fake [display,gray]
|
|
934 |
"pretty_tyenv @{context} tyenv_match"
|
|
935 |
"[?'a := bool list, ?'b := nat]"}
|
|
936 |
|
383
|
937 |
Unlike unification, which uses the function @{ML norm_type in Envir},
|
381
|
938 |
applying the matcher to a type needs to be done with the function
|
386
|
939 |
@{ML_ind subst_type in Envir}. For example
|
378
|
940 |
|
|
941 |
@{ML_response_fake [display, gray]
|
|
942 |
"Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
|
|
943 |
"bool list * nat"}
|
|
944 |
|
399
|
945 |
Be careful to observe the difference: always use
|
381
|
946 |
@{ML subst_type in Envir} for matchers and @{ML norm_type in Envir}
|
386
|
947 |
for unifiers. To show the difference, let us calculate the
|
381
|
948 |
following matcher:
|
378
|
949 |
*}
|
|
950 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
951 |
ML %grayML{*val tyenv_match' = let
|
378
|
952 |
val pat = @{typ_pat "?'a * ?'b"}
|
|
953 |
and ty = @{typ_pat "?'b list * nat"}
|
|
954 |
in
|
|
955 |
Sign.typ_match @{theory} (pat, ty) Vartab.empty
|
|
956 |
end*}
|
|
957 |
|
|
958 |
text {*
|
381
|
959 |
Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply
|
383
|
960 |
@{ML norm_type in Envir} to the type @{text "?'a * ?'b"} we obtain
|
378
|
961 |
|
|
962 |
@{ML_response_fake [display, gray]
|
|
963 |
"Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
|
|
964 |
"nat list * nat"}
|
|
965 |
|
383
|
966 |
which does not solve the matching problem, and if
|
|
967 |
we apply @{ML subst_type in Envir} to the same type we obtain
|
378
|
968 |
|
|
969 |
@{ML_response_fake [display, gray]
|
|
970 |
"Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
|
|
971 |
"?'b list * nat"}
|
|
972 |
|
383
|
973 |
which does not solve the unification problem.
|
378
|
974 |
|
|
975 |
\begin{readmore}
|
383
|
976 |
Unification and matching for types is implemented
|
378
|
977 |
in @{ML_file "Pure/type.ML"}. The ``interface'' functions for them
|
|
978 |
are in @{ML_file "Pure/sign.ML"}. Matching and unification produce type environments
|
|
979 |
as results. These are implemented in @{ML_file "Pure/envir.ML"}.
|
379
|
980 |
This file also includes the substitution and normalisation functions,
|
386
|
981 |
which apply a type environment to a type. Type environments are lookup
|
379
|
982 |
tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
|
378
|
983 |
\end{readmore}
|
|
984 |
*}
|
|
985 |
|
|
986 |
text {*
|
381
|
987 |
Unification and matching of terms is substantially more complicated than the
|
383
|
988 |
type-case. The reason is that terms have abstractions and, in this context,
|
|
989 |
unification or matching modulo plain equality is often not meaningful.
|
|
990 |
Nevertheless, Isabelle implements the function @{ML_ind
|
381
|
991 |
first_order_match in Pattern} for terms. This matching function returns a
|
|
992 |
type environment and a term environment. To pretty print the latter we use
|
|
993 |
the function @{text "pretty_env"}:
|
|
994 |
*}
|
|
995 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
996 |
ML %grayML{*fun pretty_env ctxt env =
|
381
|
997 |
let
|
389
|
998 |
fun get_trms (v, (T, t)) = (Var (v, T), t)
|
441
|
999 |
val print = pairself (pretty_term ctxt)
|
381
|
1000 |
in
|
389
|
1001 |
pretty_helper (print o get_trms) env
|
381
|
1002 |
end*}
|
|
1003 |
|
|
1004 |
text {*
|
389
|
1005 |
As can be seen from the @{text "get_trms"}-function, a term environment associates
|
381
|
1006 |
a schematic term variable with a type and a term. An example of a first-order
|
|
1007 |
matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern
|
|
1008 |
@{text "?X ?Y"}.
|
|
1009 |
*}
|
|
1010 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1011 |
ML %grayML{*val (_, fo_env) = let
|
381
|
1012 |
val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
|
387
|
1013 |
val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"}
|
|
1014 |
val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
|
381
|
1015 |
val init = (Vartab.empty, Vartab.empty)
|
|
1016 |
in
|
387
|
1017 |
Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init
|
381
|
1018 |
end *}
|
|
1019 |
|
|
1020 |
text {*
|
399
|
1021 |
In this example we annotated types explicitly because then
|
381
|
1022 |
the type environment is empty and can be ignored. The
|
383
|
1023 |
resulting term environment is
|
381
|
1024 |
|
|
1025 |
@{ML_response_fake [display, gray]
|
|
1026 |
"pretty_env @{context} fo_env"
|
|
1027 |
"[?X := P, ?Y := \<lambda>a b. Q b a]"}
|
|
1028 |
|
|
1029 |
The matcher can be applied to a term using the function @{ML_ind subst_term
|
|
1030 |
in Envir} (remember the same convention for types applies to terms: @{ML
|
383
|
1031 |
subst_term in Envir} is for matchers and @{ML norm_term in Envir} for
|
|
1032 |
unifiers). The function @{ML subst_term in Envir} expects a type environment,
|
381
|
1033 |
which is set to empty in the example below, and a term environment.
|
|
1034 |
|
|
1035 |
@{ML_response_fake [display, gray]
|
|
1036 |
"let
|
|
1037 |
val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
|
|
1038 |
in
|
|
1039 |
Envir.subst_term (Vartab.empty, fo_env) trm
|
441
|
1040 |
|> pretty_term @{context}
|
|
1041 |
|> pwriteln
|
381
|
1042 |
end"
|
|
1043 |
"P (\<lambda>a b. Q b a)"}
|
|
1044 |
|
|
1045 |
First-order matching is useful for matching against applications and
|
399
|
1046 |
variables. It can also deal with abstractions and a limited form of
|
381
|
1047 |
alpha-equivalence, but this kind of matching should be used with care, since
|
383
|
1048 |
it is not clear whether the result is meaningful. A meaningful example is
|
381
|
1049 |
matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this
|
387
|
1050 |
case, first-order matching produces @{text "[?X := P]"}.
|
381
|
1051 |
|
|
1052 |
@{ML_response_fake [display, gray]
|
|
1053 |
"let
|
|
1054 |
val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}
|
|
1055 |
val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"}
|
|
1056 |
val init = (Vartab.empty, Vartab.empty)
|
|
1057 |
in
|
|
1058 |
Pattern.first_order_match @{theory} (fo_pat, trm) init
|
|
1059 |
|> snd
|
|
1060 |
|> pretty_env @{context}
|
|
1061 |
end"
|
|
1062 |
"[?X := P]"}
|
|
1063 |
*}
|
|
1064 |
|
|
1065 |
text {*
|
414
|
1066 |
Unification of abstractions is more thoroughly studied in the context of
|
|
1067 |
higher-order pattern unification and higher-order pattern matching. A
|
448
|
1068 |
\emph{\index*{pattern}} is a well-formed term in which the arguments to
|
429
|
1069 |
every schematic variable are distinct bounds.
|
|
1070 |
In particular this excludes terms where a
|
414
|
1071 |
schematic variable is an argument of another one and where a schematic
|
|
1072 |
variable is applied twice with the same bound variable. The function
|
|
1073 |
@{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
|
429
|
1074 |
whether a term satisfies these restrictions under the assumptions
|
|
1075 |
that it is beta-normal, well-typed and has no loose bound variables.
|
381
|
1076 |
|
|
1077 |
@{ML_response [display, gray]
|
|
1078 |
"let
|
|
1079 |
val trm_list =
|
431
17f70e2834f5
added some further ho-pat-unif examples but commented out (missing response check)
schropp <schropp@in.tum.de>
diff
changeset
|
1080 |
[@{term_pat \"?X\"}, @{term_pat \"a\"},
|
430
|
1081 |
@{term_pat \"f (\<lambda>a b. ?X a b) c\"},
|
|
1082 |
@{term_pat \"\<lambda>a b. (op +) a b\"},
|
381
|
1083 |
@{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
|
430
|
1084 |
@{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
|
|
1085 |
@{term_pat \"?X a\"}]
|
381
|
1086 |
in
|
|
1087 |
map Pattern.pattern trm_list
|
|
1088 |
end"
|
430
|
1089 |
"[true, true, true, true, true, false, false, false, false]"}
|
381
|
1090 |
|
383
|
1091 |
The point of the restriction to patterns is that unification and matching
|
|
1092 |
are decidable and produce most general unifiers, respectively matchers.
|
429
|
1093 |
Note that \emph{both} terms to be unified have to be higher-order patterns
|
|
1094 |
for this to work. The exception @{ML_ind Pattern in Pattern} indicates failure
|
|
1095 |
in this regard.
|
383
|
1096 |
In this way, matching and unification can be implemented as functions that
|
|
1097 |
produce a type and term environment (unification actually returns a
|
414
|
1098 |
record of type @{ML_type Envir.env} containing a max-index, a type environment
|
|
1099 |
and a term environment). The corresponding functions are @{ML_ind match in Pattern}
|
|
1100 |
and @{ML_ind unify in Pattern}, both implemented in the structure
|
383
|
1101 |
@{ML_struct Pattern}. An example for higher-order pattern unification is
|
|
1102 |
|
384
|
1103 |
@{ML_response_fake [display, gray]
|
|
1104 |
"let
|
|
1105 |
val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
|
|
1106 |
val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
|
|
1107 |
val init = Envir.empty 0
|
|
1108 |
val env = Pattern.unify @{theory} (trm1, trm2) init
|
383
|
1109 |
in
|
384
|
1110 |
pretty_env @{context} (Envir.term_env env)
|
|
1111 |
end"
|
|
1112 |
"[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
|
|
1113 |
|
387
|
1114 |
The function @{ML_ind "Envir.empty"} generates a record with a specified
|
|
1115 |
max-index for the schematic variables (in the example the index is @{text
|
|
1116 |
0}) and empty type and term environments. The function @{ML_ind
|
|
1117 |
"Envir.term_env"} pulls out the term environment from the result record. The
|
414
|
1118 |
corresponding function for type environment is @{ML_ind
|
|
1119 |
"Envir.type_env"}. An assumption of this function is that the terms to be
|
|
1120 |
unified have already the same type. In case of failure, the exceptions that
|
|
1121 |
are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
|
387
|
1122 |
|
|
1123 |
As mentioned before, unrestricted higher-order unification, respectively
|
414
|
1124 |
unrestricted higher-order matching, is in general undecidable and might also
|
|
1125 |
not posses a single most general solution. Therefore Isabelle implements the
|
|
1126 |
unification function @{ML_ind unifiers in Unify} so that it returns a lazy
|
|
1127 |
list of potentially infinite unifiers. An example is as follows
|
387
|
1128 |
*}
|
|
1129 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1130 |
ML %grayML{*val uni_seq =
|
387
|
1131 |
let
|
|
1132 |
val trm1 = @{term_pat "?X ?Y"}
|
|
1133 |
val trm2 = @{term "f a"}
|
|
1134 |
val init = Envir.empty 0
|
|
1135 |
in
|
|
1136 |
Unify.unifiers (@{theory}, init, [(trm1, trm2)])
|
|
1137 |
end *}
|
|
1138 |
|
|
1139 |
text {*
|
|
1140 |
The unifiers can be extracted from the lazy sequence using the
|
|
1141 |
function @{ML_ind "Seq.pull"}. In the example we obtain three
|
|
1142 |
unifiers @{text "un1\<dots>un3"}.
|
|
1143 |
*}
|
|
1144 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1145 |
ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
|
387
|
1146 |
val SOME ((un2, _), next2) = Seq.pull next1;
|
|
1147 |
val SOME ((un3, _), next3) = Seq.pull next2;
|
|
1148 |
val NONE = Seq.pull next3 *}
|
|
1149 |
|
|
1150 |
text {*
|
|
1151 |
\footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}
|
|
1152 |
|
|
1153 |
We can print them out as follows.
|
|
1154 |
|
|
1155 |
@{ML_response_fake [display, gray]
|
|
1156 |
"pretty_env @{context} (Envir.term_env un1);
|
|
1157 |
pretty_env @{context} (Envir.term_env un2);
|
|
1158 |
pretty_env @{context} (Envir.term_env un3)"
|
|
1159 |
"[?X := \<lambda>a. a, ?Y := f a]
|
|
1160 |
[?X := f, ?Y := a]
|
|
1161 |
[?X := \<lambda>b. f a]"}
|
|
1162 |
|
|
1163 |
|
|
1164 |
In case of failure the function @{ML_ind unifiers in Unify} does not raise
|
|
1165 |
an exception, rather returns the empty sequence. For example
|
|
1166 |
|
|
1167 |
@{ML_response [display, gray]
|
|
1168 |
"let
|
|
1169 |
val trm1 = @{term \"a\"}
|
|
1170 |
val trm2 = @{term \"b\"}
|
|
1171 |
val init = Envir.empty 0
|
|
1172 |
in
|
|
1173 |
Unify.unifiers (@{theory}, init, [(trm1, trm2)])
|
|
1174 |
|> Seq.pull
|
|
1175 |
end"
|
|
1176 |
"NONE"}
|
|
1177 |
|
408
|
1178 |
In order to find a reasonable solution for a unification problem, Isabelle
|
|
1179 |
also tries first to solve the problem by higher-order pattern
|
|
1180 |
unification. Only in case of failure full higher-order unification is
|
|
1181 |
called. This function has a built-in bound, which can be accessed and
|
451
|
1182 |
manipulated as a configuration value. For example
|
408
|
1183 |
|
|
1184 |
@{ML_response_fake [display,gray]
|
451
|
1185 |
"Config.get_global @{theory} (Unify.search_bound)"
|
408
|
1186 |
"Int 60"}
|
|
1187 |
|
|
1188 |
If this bound is reached during unification, Isabelle prints out the
|
|
1189 |
warning message @{text [quotes] "Unification bound exceeded"} and
|
409
|
1190 |
plenty of diagnostic information (sometimes annoyingly plenty of
|
|
1191 |
information).
|
408
|
1192 |
|
387
|
1193 |
|
403
|
1194 |
For higher-order matching the function is called @{ML_ind matchers in Unify}
|
|
1195 |
implemented in the structure @{ML_struct Unify}. Also this function returns
|
|
1196 |
sequences with possibly more than one matcher. Like @{ML unifiers in
|
|
1197 |
Unify}, this function does not raise an exception in case of failure, but
|
|
1198 |
returns an empty sequence. It also first tries out whether the matching
|
|
1199 |
problem can be solved by first-order matching.
|
|
1200 |
|
|
1201 |
Higher-order matching might be necessary for instantiating a theorem
|
414
|
1202 |
appropriately. More on this will be given in Sections~\ref{sec:theorems}.
|
|
1203 |
Here we only have a look at a simple case, namely the theorem
|
|
1204 |
@{thm [source] spec}:
|
403
|
1205 |
|
|
1206 |
\begin{isabelle}
|
|
1207 |
\isacommand{thm}~@{thm [source] spec}\\
|
|
1208 |
@{text "> "}~@{thm spec}
|
|
1209 |
\end{isabelle}
|
|
1210 |
|
414
|
1211 |
as an introduction rule. Applying it directly can lead to unexpected
|
|
1212 |
behaviour since the unification has more than one solution. One way round
|
|
1213 |
this problem is to instantiate the schematic variables @{text "?P"} and
|
465
|
1214 |
@{text "?x"}. instantiation function for theorems is
|
|
1215 |
@{ML_ind instantiate_normalize in Drule} from the structure
|
|
1216 |
@{ML_struct Drule}. One problem, however, is
|
414
|
1217 |
that this function expects the instantiations as lists of @{ML_type ctyp}
|
|
1218 |
and @{ML_type cterm} pairs:
|
403
|
1219 |
|
|
1220 |
\begin{isabelle}
|
465
|
1221 |
@{ML instantiate_normalize in Drule}@{text ":"}
|
403
|
1222 |
@{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
|
|
1223 |
\end{isabelle}
|
|
1224 |
|
|
1225 |
This means we have to transform the environment the higher-order matching
|
|
1226 |
function returns into such an instantiation. For this we use the functions
|
|
1227 |
@{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract
|
|
1228 |
from an environment the corresponding variable mappings for schematic type
|
|
1229 |
and term variables. These mappings can be turned into proper
|
|
1230 |
@{ML_type ctyp}-pairs with the function
|
|
1231 |
*}
|
|
1232 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1233 |
ML %grayML{*fun prep_trm thy (x, (T, t)) =
|
403
|
1234 |
(cterm_of thy (Var (x, T)), cterm_of thy t)*}
|
|
1235 |
|
|
1236 |
text {*
|
|
1237 |
and into proper @{ML_type cterm}-pairs with
|
|
1238 |
*}
|
|
1239 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1240 |
ML %grayML{*fun prep_ty thy (x, (S, ty)) =
|
403
|
1241 |
(ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
|
|
1242 |
|
|
1243 |
text {*
|
|
1244 |
We can now calculate the instantiations from the matching function.
|
|
1245 |
*}
|
|
1246 |
|
|
1247 |
ML %linenosgray{*fun matcher_inst thy pat trm i =
|
|
1248 |
let
|
|
1249 |
val univ = Unify.matchers thy [(pat, trm)]
|
|
1250 |
val env = nth (Seq.list_of univ) i
|
|
1251 |
val tenv = Vartab.dest (Envir.term_env env)
|
|
1252 |
val tyenv = Vartab.dest (Envir.type_env env)
|
|
1253 |
in
|
|
1254 |
(map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
|
|
1255 |
end*}
|
|
1256 |
|
|
1257 |
text {*
|
|
1258 |
In Line 3 we obtain the higher-order matcher. We assume there is a finite
|
|
1259 |
number of them and select the one we are interested in via the parameter
|
|
1260 |
@{text i} in the next line. In Lines 5 and 6 we destruct the resulting
|
|
1261 |
environments using the function @{ML_ind dest in Vartab}. Finally, we need
|
|
1262 |
to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective
|
415
|
1263 |
environments (Line 8). As a simple example we instantiate the
|
|
1264 |
@{thm [source] spec} rule so that its conclusion is of the form
|
|
1265 |
@{term "Q True"}.
|
|
1266 |
|
|
1267 |
|
|
1268 |
@{ML_response_fake [gray,display,linenos]
|
403
|
1269 |
"let
|
|
1270 |
val pat = Logic.strip_imp_concl (prop_of @{thm spec})
|
415
|
1271 |
val trm = @{term \"Trueprop (Q True)\"}
|
403
|
1272 |
val inst = matcher_inst @{theory} pat trm 1
|
|
1273 |
in
|
465
|
1274 |
Drule.instantiate_normalize inst @{thm spec}
|
403
|
1275 |
end"
|
415
|
1276 |
"\<forall>x. Q x \<Longrightarrow> Q True"}
|
|
1277 |
|
|
1278 |
Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the
|
|
1279 |
conclusion of @{thm [source] spec} contains one.
|
|
1280 |
|
378
|
1281 |
\begin{readmore}
|
383
|
1282 |
Unification and matching of higher-order patterns is implemented in
|
381
|
1283 |
@{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
|
|
1284 |
for terms. Full higher-order unification is implemented
|
383
|
1285 |
in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
|
|
1286 |
in @{ML_file "Pure/General/seq.ML"}.
|
378
|
1287 |
\end{readmore}
|
377
|
1288 |
*}
|
318
|
1289 |
|
435
|
1290 |
section {* Sorts (TBD)\label{sec:sorts} *}
|
381
|
1291 |
|
398
|
1292 |
text {*
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1293 |
Type classes are formal names in the type system which are linked to
|
433
|
1294 |
predicates of one type variable (via the axclass mechanism) and thereby
|
|
1295 |
express extra properties on types, to be propagated by the type system.
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1296 |
The type-in-class judgement is defined
|
433
|
1297 |
via a simple logic over types, with inferences solely based on
|
|
1298 |
modus ponens, instantiation and axiom use.
|
|
1299 |
The declared axioms of this logic are called an order-sorted algebra (see Schmidt-Schauss).
|
|
1300 |
It consists of an acyclic subclass relation and a set of image containment
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1301 |
declarations for type constructors, called arities.
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1302 |
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1303 |
A well-behaved high-level view on type classes has long been established
|
433
|
1304 |
(cite Haftmann-Wenzel): the predicate behind a type class is the foundation
|
|
1305 |
of a locale (for context-management reasons)
|
|
1306 |
and may use so-called type class parameters. These are type-indexed constants
|
|
1307 |
dependent on the sole type variable and are implemented via overloading.
|
|
1308 |
Overloading a constant means specifying its value on a type based on
|
|
1309 |
a well-founded reduction towards other values of constants on types.
|
|
1310 |
When instantiating type classes
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1311 |
(i.e. proving arities) you are specifying overloading via primitive recursion.
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1312 |
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1313 |
Sorts are finite intersections of type classes and are implemented as lists
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1314 |
of type class names. The empty intersection, i.e. the empty list, is therefore
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1315 |
inhabited by all types and is called the topsort.
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1316 |
|
433
|
1317 |
Free and schematic type variables are always annotated with sorts, thereby restricting
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1318 |
the domain of types they quantify over and corresponding to an implicit hypothesis
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1319 |
about the type variable.
|
398
|
1320 |
*}
|
|
1321 |
|
|
1322 |
|
|
1323 |
ML {* Sign.classes_of @{theory} *}
|
|
1324 |
|
535
|
1325 |
ML {* Sign.of_sort @{theory} *}
|
|
1326 |
|
398
|
1327 |
text {*
|
|
1328 |
\begin{readmore}
|
|
1329 |
Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
|
|
1330 |
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1331 |
@{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts,
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1332 |
manages the order sorted algebra and offers an interface for reinterpreting
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1333 |
derivations of type in class judgements
|
433
|
1334 |
@{ML_file "Pure/defs.ML"} manages the constant dependency graph and keeps it well-founded
|
432
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1335 |
(its define function doesn't terminate for complex non-well-founded dependencies)
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1336 |
@{ML_file "Pure/axclass.ML"} manages the theorems that back up subclass and arity relations
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1337 |
and provides basic infrastructure for establishing the high-level view on type classes
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1338 |
@{ML_file "Pure/sign.ML"} is a common interface to all the type-theory-like declarations
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1339 |
(especially names, constants, paths, type classes) a
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1340 |
theory acquires by theory extension mechanisms and manages associated certification
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1341 |
functionality.
|
087dc1726a99
some blabla about type classes, sorts, overloading, high level view on type classes
schropp <schropp@in.tum.de>
diff
changeset
|
1342 |
It also provides the most needed functionality from individual underlying modules.
|
398
|
1343 |
\end{readmore}
|
|
1344 |
*}
|
|
1345 |
|
381
|
1346 |
|
318
|
1347 |
section {* Type-Checking\label{sec:typechecking} *}
|
|
1348 |
|
|
1349 |
text {*
|
|
1350 |
Remember Isabelle follows the Church-style typing for terms, i.e., a term contains
|
|
1351 |
enough typing information (constants, free variables and abstractions all have typing
|
|
1352 |
information) so that it is always clear what the type of a term is.
|
369
|
1353 |
Given a well-typed term, the function @{ML_ind type_of in Term} returns the
|
318
|
1354 |
type of a term. Consider for example:
|
|
1355 |
|
|
1356 |
@{ML_response [display,gray]
|
|
1357 |
"type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
|
|
1358 |
|
|
1359 |
To calculate the type, this function traverses the whole term and will
|
|
1360 |
detect any typing inconsistency. For example changing the type of the variable
|
|
1361 |
@{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message:
|
|
1362 |
|
|
1363 |
@{ML_response_fake [display,gray]
|
|
1364 |
"type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
|
|
1365 |
"*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
|
|
1366 |
|
|
1367 |
Since the complete traversal might sometimes be too costly and
|
369
|
1368 |
not necessary, there is the function @{ML_ind fastype_of in Term}, which
|
318
|
1369 |
also returns the type of a term.
|
|
1370 |
|
|
1371 |
@{ML_response [display,gray]
|
|
1372 |
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
|
|
1373 |
|
|
1374 |
However, efficiency is gained on the expense of skipping some tests. You
|
|
1375 |
can see this in the following example
|
|
1376 |
|
|
1377 |
@{ML_response [display,gray]
|
|
1378 |
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
|
|
1379 |
|
|
1380 |
where no error is detected.
|
|
1381 |
|
|
1382 |
Sometimes it is a bit inconvenient to construct a term with
|
|
1383 |
complete typing annotations, especially in cases where the typing
|
|
1384 |
information is redundant. A short-cut is to use the ``place-holder''
|
345
|
1385 |
type @{ML_ind dummyT in Term} and then let type-inference figure out the
|
400
|
1386 |
complete type. The type inference can be invoked with the function
|
|
1387 |
@{ML_ind check_term in Syntax}. An example is as follows:
|
318
|
1388 |
|
|
1389 |
@{ML_response_fake [display,gray]
|
|
1390 |
"let
|
|
1391 |
val c = Const (@{const_name \"plus\"}, dummyT)
|
|
1392 |
val o = @{term \"1::nat\"}
|
|
1393 |
val v = Free (\"x\", dummyT)
|
|
1394 |
in
|
|
1395 |
Syntax.check_term @{context} (c $ o $ v)
|
|
1396 |
end"
|
|
1397 |
"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
|
|
1398 |
Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
|
|
1399 |
|
|
1400 |
Instead of giving explicitly the type for the constant @{text "plus"} and the free
|
|
1401 |
variable @{text "x"}, type-inference fills in the missing information.
|
|
1402 |
|
|
1403 |
\begin{readmore}
|
|
1404 |
See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
|
|
1405 |
checking and pretty-printing of terms are defined. Functions related to
|
|
1406 |
type-inference are implemented in @{ML_file "Pure/type.ML"} and
|
|
1407 |
@{ML_file "Pure/type_infer.ML"}.
|
|
1408 |
\end{readmore}
|
|
1409 |
|
|
1410 |
|
|
1411 |
\begin{exercise}
|
|
1412 |
Check that the function defined in Exercise~\ref{fun:revsum} returns a
|
|
1413 |
result that type-checks. See what happens to the solutions of this
|
329
|
1414 |
exercise given in Appendix \ref{ch:solutions} when they receive an
|
|
1415 |
ill-typed term as input.
|
318
|
1416 |
\end{exercise}
|
|
1417 |
*}
|
|
1418 |
|
335
|
1419 |
section {* Certified Terms and Certified Types *}
|
|
1420 |
|
|
1421 |
text {*
|
|
1422 |
You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
|
|
1423 |
typ}es, since they are just arbitrary unchecked trees. However, you
|
|
1424 |
eventually want to see if a term is well-formed, or type-checks, relative to
|
369
|
1425 |
a theory. Type-checking is done via the function @{ML_ind cterm_of in Thm}, which
|
335
|
1426 |
converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
|
|
1427 |
term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
|
|
1428 |
abstract objects that are guaranteed to be type-correct, and they can only
|
|
1429 |
be constructed via ``official interfaces''.
|
|
1430 |
|
|
1431 |
Certification is always relative to a theory context. For example you can
|
|
1432 |
write:
|
|
1433 |
|
|
1434 |
@{ML_response_fake [display,gray]
|
|
1435 |
"cterm_of @{theory} @{term \"(a::nat) + b = c\"}"
|
|
1436 |
"a + b = c"}
|
|
1437 |
|
|
1438 |
This can also be written with an antiquotation:
|
|
1439 |
|
|
1440 |
@{ML_response_fake [display,gray]
|
|
1441 |
"@{cterm \"(a::nat) + b = c\"}"
|
|
1442 |
"a + b = c"}
|
|
1443 |
|
|
1444 |
Attempting to obtain the certified term for
|
|
1445 |
|
|
1446 |
@{ML_response_fake_both [display,gray]
|
|
1447 |
"@{cterm \"1 + True\"}"
|
|
1448 |
"Type unification failed \<dots>"}
|
|
1449 |
|
|
1450 |
yields an error (since the term is not typable). A slightly more elaborate
|
|
1451 |
example that type-checks is:
|
|
1452 |
|
|
1453 |
@{ML_response_fake [display,gray]
|
|
1454 |
"let
|
|
1455 |
val natT = @{typ \"nat\"}
|
|
1456 |
val zero = @{term \"0::nat\"}
|
356
|
1457 |
val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
|
335
|
1458 |
in
|
356
|
1459 |
cterm_of @{theory} (plus $ zero $ zero)
|
|
1460 |
end"
|
|
1461 |
"0 + 0"}
|
335
|
1462 |
|
|
1463 |
In Isabelle not just terms need to be certified, but also types. For example,
|
|
1464 |
you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
|
|
1465 |
the ML-level as follows:
|
|
1466 |
|
|
1467 |
@{ML_response_fake [display,gray]
|
|
1468 |
"ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
|
|
1469 |
"nat \<Rightarrow> bool"}
|
|
1470 |
|
|
1471 |
or with the antiquotation:
|
|
1472 |
|
|
1473 |
@{ML_response_fake [display,gray]
|
|
1474 |
"@{ctyp \"nat \<Rightarrow> bool\"}"
|
|
1475 |
"nat \<Rightarrow> bool"}
|
|
1476 |
|
|
1477 |
Since certified terms are, unlike terms, abstract objects, we cannot
|
|
1478 |
pattern-match against them. However, we can construct them. For example
|
513
|
1479 |
the function @{ML_ind apply in Thm} produces a certified application.
|
335
|
1480 |
|
|
1481 |
@{ML_response_fake [display,gray]
|
513
|
1482 |
"Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
|
335
|
1483 |
"P 3"}
|
|
1484 |
|
351
|
1485 |
Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_struct Drule}
|
|
1486 |
applies a list of @{ML_type cterm}s.
|
335
|
1487 |
|
|
1488 |
@{ML_response_fake [display,gray]
|
|
1489 |
"let
|
|
1490 |
val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}
|
|
1491 |
val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]
|
|
1492 |
in
|
|
1493 |
Drule.list_comb (chead, cargs)
|
|
1494 |
end"
|
|
1495 |
"P () 3"}
|
|
1496 |
|
|
1497 |
\begin{readmore}
|
|
1498 |
For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see
|
|
1499 |
the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and
|
|
1500 |
@{ML_file "Pure/drule.ML"}.
|
|
1501 |
\end{readmore}
|
|
1502 |
*}
|
318
|
1503 |
|
403
|
1504 |
section {* Theorems\label{sec:theorems} *}
|
318
|
1505 |
|
|
1506 |
text {*
|
|
1507 |
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
|
|
1508 |
that can only be built by going through interfaces. As a consequence, every proof
|
388
|
1509 |
in Isabelle is correct by construction. This follows the tradition of the LCF-approach.
|
318
|
1510 |
|
|
1511 |
|
|
1512 |
To see theorems in ``action'', let us give a proof on the ML-level for the following
|
|
1513 |
statement:
|
|
1514 |
*}
|
|
1515 |
|
|
1516 |
lemma
|
351
|
1517 |
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
|
|
1518 |
and assm\<^isub>2: "P t"
|
|
1519 |
shows "Q t"(*<*)oops(*>*)
|
318
|
1520 |
|
|
1521 |
text {*
|
|
1522 |
The corresponding ML-code is as follows:
|
337
|
1523 |
*}
|
318
|
1524 |
|
415
|
1525 |
ML %linenosgray{*val my_thm =
|
338
|
1526 |
let
|
337
|
1527 |
val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
|
|
1528 |
val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
|
318
|
1529 |
|
|
1530 |
val Pt_implies_Qt =
|
529
|
1531 |
Thm.assume assm1
|
|
1532 |
|> Thm.forall_elim @{cterm "t::nat"}
|
318
|
1533 |
|
449
|
1534 |
val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
|
318
|
1535 |
in
|
|
1536 |
Qt
|
449
|
1537 |
|> Thm.implies_intr assm2
|
|
1538 |
|> Thm.implies_intr assm1
|
337
|
1539 |
end*}
|
|
1540 |
|
400
|
1541 |
text {*
|
415
|
1542 |
Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which
|
|
1543 |
inserts necessary @{text "Trueprop"}s.
|
|
1544 |
|
337
|
1545 |
If we print out the value of @{ML my_thm} then we see only the
|
|
1546 |
final statement of the theorem.
|
318
|
1547 |
|
337
|
1548 |
@{ML_response_fake [display, gray]
|
440
|
1549 |
"pwriteln (pretty_thm @{context} my_thm)"
|
337
|
1550 |
"\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
|
|
1551 |
|
|
1552 |
However, internally the code-snippet constructs the following
|
|
1553 |
proof.
|
318
|
1554 |
|
|
1555 |
\[
|
|
1556 |
\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
|
|
1557 |
{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
1558 |
{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
|
|
1559 |
{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
|
|
1560 |
{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
|
|
1561 |
&
|
|
1562 |
\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
|
|
1563 |
}
|
|
1564 |
}
|
|
1565 |
}
|
|
1566 |
\]
|
|
1567 |
|
339
c588e8422737
used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1568 |
While we obtained a theorem as result, this theorem is not
|
338
|
1569 |
yet stored in Isabelle's theorem database. Consequently, it cannot be
|
348
|
1570 |
referenced on the user level. One way to store it in the theorem database is
|
502
|
1571 |
by using the function @{ML_ind note in Local_Theory} from the structure
|
|
1572 |
@{ML_struct Local_Theory} (the Isabelle command
|
|
1573 |
\isacommand{local\_setup} will be explained in more detail in
|
|
1574 |
Section~\ref{sec:local}).
|
337
|
1575 |
*}
|
|
1576 |
|
338
|
1577 |
local_setup %gray {*
|
394
|
1578 |
Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
|
337
|
1579 |
|
|
1580 |
text {*
|
396
|
1581 |
The third argument of @{ML note in Local_Theory} is the list of theorems we
|
355
|
1582 |
want to store under a name. We can store more than one under a single name.
|
396
|
1583 |
The first argument of @{ML note in Local_Theory} is the name under
|
|
1584 |
which we store the theorem or theorems. The second argument can contain a
|
353
|
1585 |
list of theorem attributes, which we will explain in detail in
|
529
|
1586 |
Section~\ref{sec:attributes}. Below we just use one such attribute,
|
|
1587 |
@{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset:
|
339
c588e8422737
used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1588 |
*}
|
c588e8422737
used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1589 |
|
c588e8422737
used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1590 |
local_setup %gray {*
|
394
|
1591 |
Local_Theory.note ((@{binding "my_thm_simp"},
|
347
|
1592 |
[Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
|
339
c588e8422737
used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1593 |
|
c588e8422737
used a better implementation of \index in Latex; added more to the theorem section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1594 |
text {*
|
348
|
1595 |
Note that we have to use another name under which the theorem is stored,
|
394
|
1596 |
since Isabelle does not allow us to call @{ML_ind note in Local_Theory} twice
|
353
|
1597 |
with the same name. The attribute needs to be wrapped inside the function @{ML_ind
|
|
1598 |
internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function
|
|
1599 |
@{ML get_thm_names_from_ss} from
|
348
|
1600 |
the previous chapter, we can check whether the theorem has actually been
|
|
1601 |
added.
|
|
1602 |
|
340
|
1603 |
|
|
1604 |
@{ML_response [display,gray]
|
|
1605 |
"let
|
|
1606 |
fun pred s = match_string \"my_thm_simp\" s
|
|
1607 |
in
|
|
1608 |
exists pred (get_thm_names_from_ss @{simpset})
|
|
1609 |
end"
|
|
1610 |
"true"}
|
|
1611 |
|
347
|
1612 |
The main point of storing the theorems @{thm [source] my_thm} and @{thm
|
|
1613 |
[source] my_thm_simp} is that they can now also be referenced with the
|
|
1614 |
\isacommand{thm}-command on the user-level of Isabelle
|
|
1615 |
|
502
|
1616 |
|
337
|
1617 |
\begin{isabelle}
|
415
|
1618 |
\isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
|
|
1619 |
@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
|
|
1620 |
@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
|
337
|
1621 |
\end{isabelle}
|
|
1622 |
|
355
|
1623 |
or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the
|
|
1624 |
user has no access to these theorems.
|
|
1625 |
|
394
|
1626 |
Recall that Isabelle does not let you call @{ML note in Local_Theory} twice
|
355
|
1627 |
with the same theorem name. In effect, once a theorem is stored under a name,
|
358
|
1628 |
this association is fixed. While this is a ``safety-net'' to make sure a
|
355
|
1629 |
theorem name refers to a particular theorem or collection of theorems, it is
|
|
1630 |
also a bit too restrictive in cases where a theorem name should refer to a
|
|
1631 |
dynamically expanding list of theorems (like a simpset). Therefore Isabelle
|
|
1632 |
also implements a mechanism where a theorem name can refer to a custom theorem
|
451
|
1633 |
list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}.
|
358
|
1634 |
To see how it works let us assume we defined our own theorem list @{text MyThmList}.
|
355
|
1635 |
*}
|
349
|
1636 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1637 |
ML %grayML{*structure MyThmList = Generic_Data
|
355
|
1638 |
(type T = thm list
|
|
1639 |
val empty = []
|
|
1640 |
val extend = I
|
394
|
1641 |
val merge = merge Thm.eq_thm_prop)
|
|
1642 |
|
|
1643 |
fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
|
355
|
1644 |
|
|
1645 |
text {*
|
|
1646 |
The function @{ML update} allows us to update the theorem list, for example
|
|
1647 |
by adding the theorem @{thm [source] TrueI}.
|
|
1648 |
*}
|
|
1649 |
|
|
1650 |
setup %gray {* update @{thm TrueI} *}
|
|
1651 |
|
|
1652 |
text {*
|
|
1653 |
We can now install the theorem list so that it is visible to the user and
|
|
1654 |
can be refered to by a theorem name. For this need to call
|
451
|
1655 |
@{ML_ind add_thms_dynamic in Global_Theory}
|
355
|
1656 |
*}
|
|
1657 |
|
|
1658 |
setup %gray {*
|
451
|
1659 |
Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get)
|
347
|
1660 |
*}
|
338
|
1661 |
|
347
|
1662 |
text {*
|
355
|
1663 |
with a name and a function that accesses the theorem list. Now if the
|
|
1664 |
user issues the command
|
|
1665 |
|
|
1666 |
\begin{isabelle}
|
|
1667 |
\isacommand{thm}~@{text "mythmlist"}\\
|
|
1668 |
@{text "> True"}
|
|
1669 |
\end{isabelle}
|
|
1670 |
|
|
1671 |
the current content of the theorem list is displayed. If more theorems are stored in
|
|
1672 |
the list, say
|
|
1673 |
*}
|
|
1674 |
|
|
1675 |
setup %gray {* update @{thm FalseE} *}
|
|
1676 |
|
|
1677 |
text {*
|
|
1678 |
then the same command produces
|
|
1679 |
|
|
1680 |
\begin{isabelle}
|
|
1681 |
\isacommand{thm}~@{text "mythmlist"}\\
|
|
1682 |
@{text "> False \<Longrightarrow> ?P"}\\
|
|
1683 |
@{text "> True"}
|
|
1684 |
\end{isabelle}
|
|
1685 |
|
400
|
1686 |
Note that if we add the theorem @{thm [source] FalseE} again to the list
|
|
1687 |
*}
|
|
1688 |
|
|
1689 |
setup %gray {* update @{thm FalseE} *}
|
|
1690 |
|
|
1691 |
text {*
|
|
1692 |
we still obtain the same list. The reason is that we used the function @{ML_ind
|
|
1693 |
add_thm in Thm} in our update function. This is a dedicated function which
|
|
1694 |
tests whether the theorem is already in the list. This test is done
|
415
|
1695 |
according to alpha-equivalence of the proposition of the theorem. The
|
400
|
1696 |
corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
|
|
1697 |
Suppose you proved the following three theorems.
|
338
|
1698 |
*}
|
|
1699 |
|
|
1700 |
lemma
|
|
1701 |
shows thm1: "\<forall>x. P x"
|
|
1702 |
and thm2: "\<forall>y. P y"
|
|
1703 |
and thm3: "\<forall>y. Q y" sorry
|
|
1704 |
|
|
1705 |
text {*
|
400
|
1706 |
Testing them for alpha equality produces:
|
338
|
1707 |
|
|
1708 |
@{ML_response [display,gray]
|
400
|
1709 |
"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
|
|
1710 |
Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
|
338
|
1711 |
"(true, false)"}
|
|
1712 |
|
340
|
1713 |
Many functions destruct theorems into @{ML_type cterm}s. For example
|
|
1714 |
the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return
|
|
1715 |
the left and right-hand side, respectively, of a meta-equality.
|
337
|
1716 |
|
338
|
1717 |
@{ML_response_fake [display,gray]
|
|
1718 |
"let
|
|
1719 |
val eq = @{thm True_def}
|
|
1720 |
in
|
|
1721 |
(Thm.lhs_of eq, Thm.rhs_of eq)
|
441
|
1722 |
|> pairself (Pretty.string_of o (pretty_cterm @{context}))
|
338
|
1723 |
end"
|
348
|
1724 |
"(True, (\<lambda>x. x) = (\<lambda>x. x))"}
|
338
|
1725 |
|
340
|
1726 |
Other function produce terms that can be pattern-matched.
|
341
|
1727 |
Suppose the following two theorems.
|
338
|
1728 |
*}
|
|
1729 |
|
341
|
1730 |
lemma
|
|
1731 |
shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C"
|
|
1732 |
and foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
|
338
|
1733 |
|
|
1734 |
text {*
|
348
|
1735 |
We can destruct them into premises and conclusions as follows.
|
340
|
1736 |
|
338
|
1737 |
@{ML_response_fake [display,gray]
|
|
1738 |
"let
|
341
|
1739 |
val ctxt = @{context}
|
|
1740 |
fun prems_and_concl thm =
|
441
|
1741 |
[[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)],
|
|
1742 |
[Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
|
|
1743 |
|> map Pretty.block
|
|
1744 |
|> Pretty.chunks
|
|
1745 |
|> pwriteln
|
338
|
1746 |
in
|
341
|
1747 |
prems_and_concl @{thm foo_test1};
|
|
1748 |
prems_and_concl @{thm foo_test2}
|
338
|
1749 |
end"
|
341
|
1750 |
"Premises: ?A, ?B
|
|
1751 |
Conclusion: ?C
|
|
1752 |
Premises:
|
|
1753 |
Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
|
|
1754 |
|
415
|
1755 |
Note that in the second case, there is no premise. The reason is that @{text "\<Longrightarrow>"}
|
|
1756 |
separates premises and conclusion, while @{text "\<longrightarrow>"} is the object implication
|
|
1757 |
from HOL, which just constructs a formula.
|
318
|
1758 |
|
|
1759 |
\begin{readmore}
|
358
|
1760 |
The basic functions for theorems are defined in
|
337
|
1761 |
@{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
|
318
|
1762 |
\end{readmore}
|
|
1763 |
|
388
|
1764 |
Although we will explain the simplifier in more detail as tactic in
|
|
1765 |
Section~\ref{sec:simplifier}, the simplifier
|
|
1766 |
can be used to work directly over theorems, for example to unfold definitions. To show
|
382
|
1767 |
this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then
|
352
|
1768 |
unfold the constant @{term "True"} according to its definition (Line 2).
|
347
|
1769 |
|
|
1770 |
@{ML_response_fake [display,gray,linenos]
|
|
1771 |
"Thm.reflexive @{cterm \"True\"}
|
|
1772 |
|> Simplifier.rewrite_rule [@{thm True_def}]
|
440
|
1773 |
|> pretty_thm @{context}
|
|
1774 |
|> pwriteln"
|
347
|
1775 |
"(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
|
341
|
1776 |
|
|
1777 |
Often it is necessary to transform theorems to and from the object
|
353
|
1778 |
logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"}
|
|
1779 |
and @{text "\<And>"}, or the other way around. A reason for such a transformation
|
|
1780 |
might be stating a definition. The reason is that definitions can only be
|
|
1781 |
stated using object logic connectives, while theorems using the connectives
|
|
1782 |
from the meta logic are more convenient for reasoning. Therefore there are
|
|
1783 |
some build in functions which help with these transformations. The function
|
418
|
1784 |
@{ML_ind rulify in Object_Logic}
|
353
|
1785 |
replaces all object connectives by equivalents in the meta logic. For example
|
341
|
1786 |
|
|
1787 |
@{ML_response_fake [display, gray]
|
418
|
1788 |
"Object_Logic.rulify @{thm foo_test2}"
|
341
|
1789 |
"\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
|
|
1790 |
|
|
1791 |
The transformation in the other direction can be achieved with function
|
418
|
1792 |
@{ML_ind atomize in Object_Logic} and the following code.
|
341
|
1793 |
|
|
1794 |
@{ML_response_fake [display,gray]
|
|
1795 |
"let
|
|
1796 |
val thm = @{thm foo_test1}
|
418
|
1797 |
val meta_eq = Object_Logic.atomize (cprop_of thm)
|
341
|
1798 |
in
|
458
|
1799 |
Raw_Simplifier.rewrite_rule [meta_eq] thm
|
341
|
1800 |
end"
|
|
1801 |
"?A \<longrightarrow> ?B \<longrightarrow> ?C"}
|
|
1802 |
|
418
|
1803 |
In this code the function @{ML atomize in Object_Logic} produces
|
341
|
1804 |
a meta-equation between the given theorem and the theorem transformed
|
347
|
1805 |
into the object logic. The result is the theorem with object logic
|
|
1806 |
connectives. However, in order to completely transform a theorem
|
353
|
1807 |
involving meta variables, such as @{thm [source] list.induct}, which
|
|
1808 |
is of the form
|
347
|
1809 |
|
|
1810 |
@{thm [display] list.induct}
|
|
1811 |
|
349
|
1812 |
we have to first abstract over the meta variables @{text "?P"} and
|
353
|
1813 |
@{text "?list"}. For this we can use the function
|
352
|
1814 |
@{ML_ind forall_intr_vars in Drule}. This allows us to implement the
|
|
1815 |
following function for atomizing a theorem.
|
347
|
1816 |
*}
|
|
1817 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1818 |
ML %grayML{*fun atomize_thm thm =
|
347
|
1819 |
let
|
|
1820 |
val thm' = forall_intr_vars thm
|
418
|
1821 |
val thm'' = Object_Logic.atomize (cprop_of thm')
|
347
|
1822 |
in
|
458
|
1823 |
Raw_Simplifier.rewrite_rule [thm''] thm'
|
347
|
1824 |
end*}
|
|
1825 |
|
|
1826 |
text {*
|
352
|
1827 |
This function produces for the theorem @{thm [source] list.induct}
|
347
|
1828 |
|
|
1829 |
@{ML_response_fake [display, gray]
|
|
1830 |
"atomize_thm @{thm list.induct}"
|
|
1831 |
"\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
|
|
1832 |
|
341
|
1833 |
Theorems can also be produced from terms by giving an explicit proof.
|
353
|
1834 |
One way to achieve this is by using the function @{ML_ind prove in Goal}
|
|
1835 |
in the structure @{ML_struct Goal}. For example below we use this function
|
448
|
1836 |
to prove the term @{term "P \<Longrightarrow> P"}.
|
341
|
1837 |
|
|
1838 |
@{ML_response_fake [display,gray]
|
|
1839 |
"let
|
|
1840 |
val trm = @{term \"P \<Longrightarrow> P::bool\"}
|
|
1841 |
val tac = K (atac 1)
|
|
1842 |
in
|
|
1843 |
Goal.prove @{context} [\"P\"] [] trm tac
|
|
1844 |
end"
|
|
1845 |
"?P \<Longrightarrow> ?P"}
|
|
1846 |
|
352
|
1847 |
This function takes first a context and second a list of strings. This list
|
359
|
1848 |
specifies which variables should be turned into schematic variables once the term
|
448
|
1849 |
is proved (in this case only @{text "\"P\""}). The fourth argument is the term to be
|
|
1850 |
proved. The fifth is a corresponding proof given in form of a tactic (we explain
|
|
1851 |
tactics in Chapter~\ref{chp:tactical}). In the code above, the tactic proves the
|
|
1852 |
theorem by assumption.
|
|
1853 |
|
|
1854 |
There is also the possibility of proving multiple goals at the same time
|
|
1855 |
using the function @{ML_ind prove_multi in Goal}. For this let us define the
|
|
1856 |
following three helper functions.
|
|
1857 |
*}
|
|
1858 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1859 |
ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
|
448
|
1860 |
fun rep_tacs i = replicate i (rtac @{thm refl})
|
|
1861 |
|
|
1862 |
fun multi_test ctxt i =
|
|
1863 |
Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i)
|
|
1864 |
(K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
|
|
1865 |
|
|
1866 |
text {*
|
|
1867 |
With them we can now produce three theorem instances of the
|
|
1868 |
proposition.
|
|
1869 |
|
|
1870 |
@{ML_response_fake [display, gray]
|
|
1871 |
"multi_test @{context} 3"
|
|
1872 |
"[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
|
|
1873 |
|
|
1874 |
However you should be careful with @{ML prove_multi in Goal} and very
|
|
1875 |
large goals. If you increase the counter in the code above to @{text 3000},
|
|
1876 |
you will notice that takes approximately ten(!) times longer than
|
|
1877 |
using @{ML map} and @{ML prove in Goal}.
|
|
1878 |
*}
|
|
1879 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
1880 |
ML %grayML{*let
|
448
|
1881 |
fun test_prove ctxt thm =
|
|
1882 |
Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
|
|
1883 |
in
|
|
1884 |
map (test_prove @{context}) (rep_goals 3000)
|
|
1885 |
end*}
|
|
1886 |
|
|
1887 |
text {*
|
388
|
1888 |
While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
|
|
1889 |
is the function @{ML_ind make_thm in Skip_Proof} in the structure
|
|
1890 |
@{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.
|
|
1891 |
Potentially making the system unsound. This is sometimes useful for developing
|
|
1892 |
purposes, or when explicit proof construction should be omitted due to performace
|
|
1893 |
reasons. An example of this function is as follows:
|
|
1894 |
|
|
1895 |
@{ML_response_fake [display, gray]
|
|
1896 |
"Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
|
|
1897 |
"True = False"}
|
|
1898 |
|
415
|
1899 |
\begin{readmore}
|
|
1900 |
Functions that setup goal states and prove theorems are implemented in
|
|
1901 |
@{ML_file "Pure/goal.ML"}. A function and a tactic that allow one to
|
|
1902 |
skip proofs of theorems are implemented in @{ML_file "Pure/Isar/skip_proof.ML"}.
|
|
1903 |
\end{readmore}
|
|
1904 |
|
352
|
1905 |
Theorems also contain auxiliary data, such as the name of the theorem, its
|
|
1906 |
kind, the names for cases and so on. This data is stored in a string-string
|
|
1907 |
list and can be retrieved with the function @{ML_ind get_tags in
|
353
|
1908 |
Thm}. Assume you prove the following lemma.
|
341
|
1909 |
*}
|
|
1910 |
|
353
|
1911 |
lemma foo_data:
|
|
1912 |
shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
|
341
|
1913 |
|
|
1914 |
text {*
|
353
|
1915 |
The auxiliary data of this lemma can be retrieved using the function
|
|
1916 |
@{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is
|
341
|
1917 |
|
|
1918 |
@{ML_response_fake [display,gray]
|
|
1919 |
"Thm.get_tags @{thm foo_data}"
|
342
|
1920 |
"[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
|
|
1921 |
|
353
|
1922 |
consisting of a name and a kind. When we store lemmas in the theorem database,
|
|
1923 |
we might want to explicitly extend this data by attaching case names to the
|
375
|
1924 |
two premises of the lemma. This can be done with the function @{ML_ind name in Rule_Cases}
|
|
1925 |
from the structure @{ML_struct Rule_Cases}.
|
341
|
1926 |
*}
|
|
1927 |
|
342
|
1928 |
local_setup %gray {*
|
394
|
1929 |
Local_Theory.note ((@{binding "foo_data'"}, []),
|
|
1930 |
[(Rule_Cases.name ["foo_case_one", "foo_case_two"]
|
|
1931 |
@{thm foo_data})]) #> snd *}
|
341
|
1932 |
|
342
|
1933 |
text {*
|
349
|
1934 |
The data of the theorem @{thm [source] foo_data'} is then as follows:
|
341
|
1935 |
|
342
|
1936 |
@{ML_response_fake [display,gray]
|
|
1937 |
"Thm.get_tags @{thm foo_data'}"
|
|
1938 |
"[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
|
352
|
1939 |
(\"case_names\", \"foo_case_one;foo_case_two\")]"}
|
349
|
1940 |
|
353
|
1941 |
You can observe the case names of this lemma on the user level when using
|
355
|
1942 |
the proof methods @{text cases} and @{text induct}. In the proof below
|
342
|
1943 |
*}
|
341
|
1944 |
|
|
1945 |
lemma
|
529
|
1946 |
shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
|
349
|
1947 |
proof (cases rule: foo_data')
|
352
|
1948 |
|
349
|
1949 |
(*<*)oops(*>*)
|
352
|
1950 |
text_raw{*
|
|
1951 |
\begin{tabular}{@ {}l}
|
|
1952 |
\isacommand{print\_cases}\\
|
|
1953 |
@{text "> cases:"}\\
|
|
1954 |
@{text "> foo_case_one:"}\\
|
|
1955 |
@{text "> let \"?case\" = \"?P\""}\\
|
|
1956 |
@{text "> foo_case_two:"}\\
|
|
1957 |
@{text "> let \"?case\" = \"?P\""}
|
|
1958 |
\end{tabular}*}
|
349
|
1959 |
|
|
1960 |
text {*
|
353
|
1961 |
we can proceed by analysing the cases @{text "foo_case_one"} and
|
|
1962 |
@{text "foo_case_two"}. While if the theorem has no names, then
|
352
|
1963 |
the cases have standard names @{text 1}, @{text 2} and so
|
349
|
1964 |
on. This can be seen in the proof below.
|
|
1965 |
*}
|
|
1966 |
|
|
1967 |
lemma
|
529
|
1968 |
shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
|
349
|
1969 |
proof (cases rule: foo_data)
|
352
|
1970 |
|
342
|
1971 |
(*<*)oops(*>*)
|
352
|
1972 |
text_raw{*
|
|
1973 |
\begin{tabular}{@ {}l}
|
|
1974 |
\isacommand{print\_cases}\\
|
|
1975 |
@{text "> cases:"}\\
|
|
1976 |
@{text "> 1:"}\\
|
|
1977 |
@{text "> let \"?case\" = \"?P\""}\\
|
|
1978 |
@{text "> 2:"}\\
|
|
1979 |
@{text "> let \"?case\" = \"?P\""}
|
|
1980 |
\end{tabular}*}
|
|
1981 |
|
529
|
1982 |
|
|
1983 |
text {*
|
533
|
1984 |
Sometimes one wants to know the theorems that are involved in
|
|
1985 |
proving a theorem, especially when the proof is by @{text
|
|
1986 |
auto}. These theorems can be obtained by introspecting the proved theorem.
|
|
1987 |
To introspect a theorem, let us define the following three functions
|
|
1988 |
that analyse the @{ML_type_ind proof_body} data-structure from the
|
|
1989 |
structure @{ML_struct Proofterm}.
|
529
|
1990 |
*}
|
|
1991 |
|
|
1992 |
ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
|
|
1993 |
val get_names = map #1 o pthms_of
|
|
1994 |
val get_pbodies = map (Future.join o #3) o pthms_of *}
|
|
1995 |
|
|
1996 |
text {*
|
|
1997 |
To see what their purpose is, consider the following three short proofs.
|
|
1998 |
*}
|
|
1999 |
|
|
2000 |
lemma my_conjIa:
|
|
2001 |
shows "A \<and> B \<Longrightarrow> A \<and> B"
|
|
2002 |
apply(rule conjI)
|
|
2003 |
apply(drule conjunct1)
|
|
2004 |
apply(assumption)
|
|
2005 |
apply(drule conjunct2)
|
|
2006 |
apply(assumption)
|
|
2007 |
done
|
|
2008 |
|
|
2009 |
lemma my_conjIb:
|
|
2010 |
shows "A \<and> B \<Longrightarrow> A \<and> B"
|
|
2011 |
apply(assumption)
|
|
2012 |
done
|
|
2013 |
|
|
2014 |
lemma my_conjIc:
|
|
2015 |
shows "A \<and> B \<Longrightarrow> A \<and> B"
|
|
2016 |
apply(auto)
|
|
2017 |
done
|
341
|
2018 |
|
535
|
2019 |
|
341
|
2020 |
text {*
|
529
|
2021 |
While the information about which theorems are used is obvious in
|
|
2022 |
the first two proofs, it is not obvious in the third, because of the
|
|
2023 |
@{text auto}-step. Fortunately, ``behind'' every proved theorem is
|
|
2024 |
a proof-tree that records all theorems that are employed for
|
|
2025 |
establishing this theorem. We can traverse this proof-tree
|
|
2026 |
extracting this information. Let us first extract the name of the
|
|
2027 |
established theorem. This can be done with
|
|
2028 |
|
535
|
2029 |
@{ML_response_fake [display,gray]
|
529
|
2030 |
"@{thm my_conjIa}
|
|
2031 |
|> Thm.proof_body_of
|
|
2032 |
|> get_names"
|
|
2033 |
"[\"Essential.my_conjIa\"]"}
|
|
2034 |
|
|
2035 |
whereby @{text "Essential"} refers to the theory name in which
|
|
2036 |
we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
|
|
2037 |
proof_body_of in Thm} returns a part of the data that is stored in a
|
|
2038 |
theorem. Notice that the first proof above references
|
|
2039 |
three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1}
|
|
2040 |
and @{thm [source] conjunct2}. We can obtain them by descending into the
|
|
2041 |
first level of the proof-tree, as follows.
|
|
2042 |
|
535
|
2043 |
@{ML_response_fake [display,gray]
|
529
|
2044 |
"@{thm my_conjIa}
|
|
2045 |
|> Thm.proof_body_of
|
|
2046 |
|> get_pbodies
|
|
2047 |
|> map get_names
|
|
2048 |
|> List.concat"
|
|
2049 |
"[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
|
|
2050 |
\"Pure.protectI\"]"}
|
|
2051 |
|
533
|
2052 |
The theorems @{thm [source] Pure.protectD} and @{thm [source]
|
|
2053 |
Pure.protectI} that are internal theorems are always part of a
|
529
|
2054 |
proof in Isabelle. Note also that applications of @{text assumption} do not
|
|
2055 |
count as a separate theorem, as you can see in the following code.
|
|
2056 |
|
535
|
2057 |
@{ML_response_fake [display,gray]
|
529
|
2058 |
"@{thm my_conjIb}
|
|
2059 |
|> Thm.proof_body_of
|
|
2060 |
|> get_pbodies
|
|
2061 |
|> map get_names
|
|
2062 |
|> List.concat"
|
|
2063 |
"[\"Pure.protectD\", \"Pure.protectI\"]"}
|
|
2064 |
|
|
2065 |
Interestingly, but not surprisingly, the proof of @{thm [source]
|
|
2066 |
my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
|
|
2067 |
and @{thm [source] my_conjIb}, as can be seen by the theorems that
|
|
2068 |
are returned for @{thm [source] my_conjIc}.
|
|
2069 |
|
535
|
2070 |
@{ML_response_fake [display,gray]
|
529
|
2071 |
"@{thm my_conjIc}
|
|
2072 |
|> Thm.proof_body_of
|
|
2073 |
|> get_pbodies
|
|
2074 |
|> map get_names
|
|
2075 |
|> List.concat"
|
|
2076 |
"[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
|
|
2077 |
\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
|
|
2078 |
\"Pure.protectI\"]"}
|
|
2079 |
|
|
2080 |
Of course we can also descend into the second level of the tree
|
|
2081 |
``behind'' @{thm [source] my_conjIa} say, which
|
|
2082 |
means we obtain the theorems that are used in order to prove
|
|
2083 |
@{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
|
|
2084 |
|
535
|
2085 |
@{ML_response_fake [display, gray]
|
529
|
2086 |
"@{thm my_conjIa}
|
|
2087 |
|> Thm.proof_body_of
|
|
2088 |
|> get_pbodies
|
|
2089 |
|> map get_pbodies
|
|
2090 |
|> (map o map) get_names
|
|
2091 |
|> List.concat
|
|
2092 |
|> List.concat
|
|
2093 |
|> duplicates (op=)"
|
|
2094 |
"[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
|
|
2095 |
\"Pure.protectI\"]"}
|
|
2096 |
|
533
|
2097 |
\begin{exercise}
|
|
2098 |
Have a look at the theorems that are used when a lemma is ``proved''
|
|
2099 |
by \isacommand{sorry}?
|
|
2100 |
\end{exercise}
|
|
2101 |
|
529
|
2102 |
\begin{readmore}
|
|
2103 |
The data-structure @{ML_type proof_body} is implemented
|
|
2104 |
in the file @{ML_file "Pure/proofterm.ML"}. The implementation
|
|
2105 |
of theorems and related functions are in @{ML_file "Pure/thm.ML"}.
|
|
2106 |
\end{readmore}
|
|
2107 |
|
352
|
2108 |
One great feature of Isabelle is its document preparation system, where
|
353
|
2109 |
proved theorems can be quoted in documents referencing directly their
|
|
2110 |
formalisation. This helps tremendously to minimise cut-and-paste errors. However,
|
|
2111 |
sometimes the verbatim quoting is not what is wanted or what can be shown to
|
354
|
2112 |
readers. For such situations Isabelle allows the installation of \emph{\index*{theorem
|
|
2113 |
styles}}. These are, roughly speaking, functions from terms to terms. The input
|
353
|
2114 |
term stands for the theorem to be presented; the output can be constructed to
|
|
2115 |
ones wishes. Let us, for example, assume we want to quote theorems without
|
|
2116 |
leading @{text \<forall>}-quantifiers. For this we can implement the following function
|
358
|
2117 |
that strips off @{text "\<forall>"}s.
|
318
|
2118 |
*}
|
|
2119 |
|
358
|
2120 |
ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) =
|
354
|
2121 |
Term.dest_abs body |> snd |> strip_allq
|
|
2122 |
| strip_allq (Const (@{const_name "Trueprop"}, _) $ t) =
|
|
2123 |
strip_allq t
|
|
2124 |
| strip_allq t = t*}
|
318
|
2125 |
|
352
|
2126 |
text {*
|
353
|
2127 |
We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,
|
|
2128 |
since this function deals correctly with potential name clashes. This function produces
|
|
2129 |
a pair consisting of the variable and the body of the abstraction. We are only interested
|
|
2130 |
in the body, which we feed into the recursive call. In Line 3 and 4, we also
|
|
2131 |
have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can
|
354
|
2132 |
install this function as the theorem style named @{text "my_strip_allq"}.
|
352
|
2133 |
*}
|
|
2134 |
|
400
|
2135 |
setup %gray{*
|
354
|
2136 |
Term_Style.setup "my_strip_allq" (Scan.succeed (K strip_allq))
|
352
|
2137 |
*}
|
|
2138 |
|
|
2139 |
text {*
|
353
|
2140 |
We can test this theorem style with the following theorem
|
318
|
2141 |
*}
|
|
2142 |
|
352
|
2143 |
theorem style_test:
|
529
|
2144 |
shows "\<forall>x y z. (x, x) = (y, z)" sorry
|
352
|
2145 |
|
|
2146 |
text {*
|
353
|
2147 |
Now printing out in a document the theorem @{thm [source] style_test} normally
|
|
2148 |
using @{text "@{thm \<dots>}"} produces
|
352
|
2149 |
|
353
|
2150 |
\begin{isabelle}
|
502
|
2151 |
\begin{graybox}
|
353
|
2152 |
@{text "@{thm style_test}"}\\
|
|
2153 |
@{text ">"}~@{thm style_test}
|
502
|
2154 |
\end{graybox}
|
353
|
2155 |
\end{isabelle}
|
318
|
2156 |
|
354
|
2157 |
as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"}
|
352
|
2158 |
we obtain
|
|
2159 |
|
353
|
2160 |
\begin{isabelle}
|
502
|
2161 |
\begin{graybox}
|
354
|
2162 |
@{text "@{thm (my_strip_allq) style_test}"}\\
|
400
|
2163 |
@{text ">"}~@{thm (my_strip_allq) style_test}
|
502
|
2164 |
\end{graybox}
|
353
|
2165 |
\end{isabelle}
|
352
|
2166 |
|
353
|
2167 |
without the leading quantifiers. We can improve this theorem style by explicitly
|
|
2168 |
giving a list of strings that should be used for the replacement of the
|
|
2169 |
variables. For this we implement the function which takes a list of strings
|
|
2170 |
and uses them as name in the outermost abstractions.
|
|
2171 |
*}
|
|
2172 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2173 |
ML %grayML{*fun rename_allq [] t = t
|
354
|
2174 |
| rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) =
|
|
2175 |
Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
|
|
2176 |
| rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
|
|
2177 |
rename_allq xs t
|
|
2178 |
| rename_allq _ t = t*}
|
353
|
2179 |
|
|
2180 |
text {*
|
|
2181 |
We can now install a the modified theorem style as follows
|
318
|
2182 |
*}
|
|
2183 |
|
356
|
2184 |
setup %gray {* let
|
353
|
2185 |
val parser = Scan.repeat Args.name
|
354
|
2186 |
fun action xs = K (rename_allq xs #> strip_allq)
|
353
|
2187 |
in
|
354
|
2188 |
Term_Style.setup "my_strip_allq2" (parser >> action)
|
353
|
2189 |
end *}
|
|
2190 |
|
|
2191 |
text {*
|
355
|
2192 |
The parser reads a list of names. In the function @{text action} we first
|
354
|
2193 |
call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}
|
|
2194 |
on the resulting term. We can now suggest, for example, two variables for
|
|
2195 |
stripping off the first two @{text \<forall>}-quantifiers.
|
|
2196 |
|
353
|
2197 |
\begin{isabelle}
|
502
|
2198 |
\begin{graybox}
|
354
|
2199 |
@{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\
|
|
2200 |
@{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
|
502
|
2201 |
\end{graybox}
|
353
|
2202 |
\end{isabelle}
|
|
2203 |
|
404
|
2204 |
Such styles allow one to print out theorems in documents formatted to
|
|
2205 |
ones heart content. The styles can also be used in the document
|
|
2206 |
antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"}
|
|
2207 |
and @{text "@{typeof ...}"}.
|
|
2208 |
|
|
2209 |
Next we explain theorem attributes, which is another
|
353
|
2210 |
mechanism for dealing with theorems.
|
|
2211 |
|
|
2212 |
\begin{readmore}
|
|
2213 |
Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.
|
|
2214 |
\end{readmore}
|
|
2215 |
*}
|
318
|
2216 |
|
|
2217 |
section {* Theorem Attributes\label{sec:attributes} *}
|
|
2218 |
|
|
2219 |
text {*
|
|
2220 |
Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
|
|
2221 |
"[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
|
356
|
2222 |
annotated to theorems, but functions that do further processing of
|
|
2223 |
theorems. In particular, it is not possible to find out
|
318
|
2224 |
what are all theorems that have a given attribute in common, unless of course
|
|
2225 |
the function behind the attribute stores the theorems in a retrievable
|
|
2226 |
data structure.
|
|
2227 |
|
|
2228 |
If you want to print out all currently known attributes a theorem can have,
|
|
2229 |
you can use the Isabelle command
|
|
2230 |
|
|
2231 |
\begin{isabelle}
|
|
2232 |
\isacommand{print\_attributes}\\
|
|
2233 |
@{text "> COMP: direct composition with rules (no lifting)"}\\
|
|
2234 |
@{text "> HOL.dest: declaration of Classical destruction rule"}\\
|
|
2235 |
@{text "> HOL.elim: declaration of Classical elimination rule"}\\
|
|
2236 |
@{text "> \<dots>"}
|
|
2237 |
\end{isabelle}
|
|
2238 |
|
|
2239 |
The theorem attributes fall roughly into two categories: the first category manipulates
|
356
|
2240 |
theorems (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
|
|
2241 |
stores theorems somewhere as data (for example @{text "[simp]"}, which adds
|
|
2242 |
theorems to the current simpset).
|
318
|
2243 |
|
|
2244 |
To explain how to write your own attribute, let us start with an extremely simple
|
|
2245 |
version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
|
|
2246 |
to produce the ``symmetric'' version of an equation. The main function behind
|
|
2247 |
this attribute is
|
|
2248 |
*}
|
|
2249 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2250 |
ML %grayML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
|
318
|
2251 |
|
|
2252 |
text {*
|
|
2253 |
where the function @{ML_ind rule_attribute in Thm} expects a function taking a
|
|
2254 |
context (which we ignore in the code above) and a theorem (@{text thm}), and
|
|
2255 |
returns another theorem (namely @{text thm} resolved with the theorem
|
363
|
2256 |
@{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind RS in Drule}
|
318
|
2257 |
is explained in Section~\ref{sec:simpletacs}). The function
|
|
2258 |
@{ML rule_attribute in Thm} then returns an attribute.
|
|
2259 |
|
|
2260 |
Before we can use the attribute, we need to set it up. This can be done
|
|
2261 |
using the Isabelle command \isacommand{attribute\_setup} as follows:
|
|
2262 |
*}
|
|
2263 |
|
356
|
2264 |
attribute_setup %gray my_sym =
|
|
2265 |
{* Scan.succeed my_symmetric *} "applying the sym rule"
|
318
|
2266 |
|
|
2267 |
text {*
|
|
2268 |
Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
|
|
2269 |
for the theorem attribute. Since the attribute does not expect any further
|
356
|
2270 |
arguments (unlike @{text "[THEN \<dots>]"}, for instance), we use the parser @{ML
|
|
2271 |
Scan.succeed}. An example for the attribute @{text "[my_sym]"} is the proof
|
318
|
2272 |
*}
|
|
2273 |
|
|
2274 |
lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
|
|
2275 |
|
|
2276 |
text {*
|
|
2277 |
which stores the theorem @{thm test} under the name @{thm [source] test}. You
|
|
2278 |
can see this, if you query the lemma:
|
|
2279 |
|
|
2280 |
\begin{isabelle}
|
|
2281 |
\isacommand{thm}~@{text "test"}\\
|
|
2282 |
@{text "> "}~@{thm test}
|
|
2283 |
\end{isabelle}
|
|
2284 |
|
|
2285 |
We can also use the attribute when referring to this theorem:
|
|
2286 |
|
|
2287 |
\begin{isabelle}
|
|
2288 |
\isacommand{thm}~@{text "test[my_sym]"}\\
|
|
2289 |
@{text "> "}~@{thm test[my_sym]}
|
|
2290 |
\end{isabelle}
|
|
2291 |
|
|
2292 |
An alternative for setting up an attribute is the function @{ML_ind setup in Attrib}.
|
|
2293 |
So instead of using \isacommand{attribute\_setup}, you can also set up the
|
|
2294 |
attribute as follows:
|
|
2295 |
*}
|
|
2296 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2297 |
ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
|
318
|
2298 |
"applying the sym rule" *}
|
|
2299 |
|
|
2300 |
text {*
|
356
|
2301 |
This gives a function from @{ML_type "theory -> theory"}, which
|
361
|
2302 |
can be used for example with \isacommand{setup} or with
|
368
|
2303 |
@{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.}
|
318
|
2304 |
|
|
2305 |
As an example of a slightly more complicated theorem attribute, we implement
|
|
2306 |
our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
|
356
|
2307 |
as argument and resolve the theorem with this list (one theorem
|
318
|
2308 |
after another). The code for this attribute is
|
|
2309 |
*}
|
|
2310 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2311 |
ML %grayML{*fun MY_THEN thms =
|
396
|
2312 |
let
|
|
2313 |
fun RS_rev thm1 thm2 = thm2 RS thm1
|
|
2314 |
in
|
|
2315 |
Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
|
|
2316 |
end*}
|
318
|
2317 |
|
|
2318 |
text {*
|
396
|
2319 |
where for convenience we define the reverse and curried version of @{ML RS}.
|
|
2320 |
The setup of this theorem attribute uses the parser @{ML thms in Attrib},
|
|
2321 |
which parses a list of theorems.
|
318
|
2322 |
*}
|
|
2323 |
|
|
2324 |
attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
|
356
|
2325 |
"resolving the list of theorems with the theorem"
|
318
|
2326 |
|
|
2327 |
text {*
|
|
2328 |
You can, for example, use this theorem attribute to turn an equation into a
|
|
2329 |
meta-equation:
|
|
2330 |
|
|
2331 |
\begin{isabelle}
|
|
2332 |
\isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\
|
|
2333 |
@{text "> "}~@{thm test[MY_THEN eq_reflection]}
|
|
2334 |
\end{isabelle}
|
|
2335 |
|
|
2336 |
If you need the symmetric version as a meta-equation, you can write
|
|
2337 |
|
|
2338 |
\begin{isabelle}
|
|
2339 |
\isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
|
|
2340 |
@{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
|
|
2341 |
\end{isabelle}
|
|
2342 |
|
|
2343 |
It is also possible to combine different theorem attributes, as in:
|
|
2344 |
|
|
2345 |
\begin{isabelle}
|
|
2346 |
\isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
|
|
2347 |
@{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
|
|
2348 |
\end{isabelle}
|
|
2349 |
|
|
2350 |
However, here also a weakness of the concept
|
|
2351 |
of theorem attributes shows through: since theorem attributes can be
|
329
|
2352 |
arbitrary functions, they do not commute in general. If you try
|
318
|
2353 |
|
|
2354 |
\begin{isabelle}
|
|
2355 |
\isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
|
|
2356 |
@{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
|
|
2357 |
\end{isabelle}
|
|
2358 |
|
|
2359 |
you get an exception indicating that the theorem @{thm [source] sym}
|
|
2360 |
does not resolve with meta-equations.
|
|
2361 |
|
329
|
2362 |
The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate
|
|
2363 |
theorems. Another usage of theorem attributes is to add and delete theorems
|
|
2364 |
from stored data. For example the theorem attribute @{text "[simp]"} adds
|
|
2365 |
or deletes a theorem from the current simpset. For these applications, you
|
|
2366 |
can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,
|
|
2367 |
let us introduce a theorem list.
|
318
|
2368 |
*}
|
|
2369 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2370 |
ML %grayML{*structure MyThms = Named_Thms
|
481
|
2371 |
(val name = @{binding "attr_thms"}
|
329
|
2372 |
val description = "Theorems for an Attribute") *}
|
318
|
2373 |
|
329
|
2374 |
text {*
|
|
2375 |
We are going to modify this list by adding and deleting theorems.
|
|
2376 |
For this we use the two functions @{ML MyThms.add_thm} and
|
|
2377 |
@{ML MyThms.del_thm}. You can turn them into attributes
|
|
2378 |
with the code
|
318
|
2379 |
*}
|
|
2380 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2381 |
ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm
|
329
|
2382 |
val my_del = Thm.declaration_attribute MyThms.del_thm *}
|
318
|
2383 |
|
|
2384 |
text {*
|
|
2385 |
and set up the attributes as follows
|
|
2386 |
*}
|
|
2387 |
|
|
2388 |
attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
|
329
|
2389 |
"maintaining a list of my_thms"
|
318
|
2390 |
|
|
2391 |
text {*
|
|
2392 |
The parser @{ML_ind add_del in Attrib} is a predefined parser for
|
|
2393 |
adding and deleting lemmas. Now if you prove the next lemma
|
|
2394 |
and attach to it the attribute @{text "[my_thms]"}
|
|
2395 |
*}
|
|
2396 |
|
|
2397 |
lemma trueI_2[my_thms]: "True" by simp
|
|
2398 |
|
|
2399 |
text {*
|
|
2400 |
then you can see it is added to the initially empty list.
|
|
2401 |
|
|
2402 |
@{ML_response_fake [display,gray]
|
329
|
2403 |
"MyThms.get @{context}"
|
|
2404 |
"[\"True\"]"}
|
318
|
2405 |
|
|
2406 |
You can also add theorems using the command \isacommand{declare}.
|
|
2407 |
*}
|
|
2408 |
|
329
|
2409 |
declare test[my_thms] trueI_2[my_thms add]
|
318
|
2410 |
|
|
2411 |
text {*
|
|
2412 |
With this attribute, the @{text "add"} operation is the default and does
|
|
2413 |
not need to be explicitly given. These three declarations will cause the
|
|
2414 |
theorem list to be updated as:
|
|
2415 |
|
|
2416 |
@{ML_response_fake [display,gray]
|
329
|
2417 |
"MyThms.get @{context}"
|
318
|
2418 |
"[\"True\", \"Suc (Suc 0) = 2\"]"}
|
|
2419 |
|
|
2420 |
The theorem @{thm [source] trueI_2} only appears once, since the
|
|
2421 |
function @{ML_ind add_thm in Thm} tests for duplicates, before extending
|
|
2422 |
the list. Deletion from the list works as follows:
|
|
2423 |
*}
|
|
2424 |
|
|
2425 |
declare test[my_thms del]
|
|
2426 |
|
|
2427 |
text {* After this, the theorem list is again:
|
|
2428 |
|
|
2429 |
@{ML_response_fake [display,gray]
|
329
|
2430 |
"MyThms.get @{context}"
|
318
|
2431 |
"[\"True\"]"}
|
|
2432 |
|
329
|
2433 |
We used in this example two functions declared as @{ML_ind
|
|
2434 |
declaration_attribute in Thm}, but there can be any number of them. We just
|
|
2435 |
have to change the parser for reading the arguments accordingly.
|
318
|
2436 |
|
329
|
2437 |
\footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
|
396
|
2438 |
\footnote{\bf FIXME readmore}
|
318
|
2439 |
|
|
2440 |
\begin{readmore}
|
|
2441 |
FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in
|
|
2442 |
@{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
|
|
2443 |
parsing.
|
|
2444 |
\end{readmore}
|
|
2445 |
*}
|
|
2446 |
|
|
2447 |
section {* Pretty-Printing\label{sec:pretty} *}
|
|
2448 |
|
|
2449 |
text {*
|
|
2450 |
So far we printed out only plain strings without any formatting except for
|
|
2451 |
occasional explicit line breaks using @{text [quotes] "\\n"}. This is
|
|
2452 |
sufficient for ``quick-and-dirty'' printouts. For something more
|
336
|
2453 |
sophisticated, Isabelle includes an infrastructure for properly formatting
|
|
2454 |
text. Most of its functions do not operate on @{ML_type string}s, but on
|
|
2455 |
instances of the pretty type:
|
318
|
2456 |
|
|
2457 |
@{ML_type_ind [display, gray] "Pretty.T"}
|
|
2458 |
|
|
2459 |
The function @{ML str in Pretty} transforms a (plain) string into such a pretty
|
|
2460 |
type. For example
|
|
2461 |
|
|
2462 |
@{ML_response_fake [display,gray]
|
|
2463 |
"Pretty.str \"test\"" "String (\"test\", 4)"}
|
|
2464 |
|
|
2465 |
where the result indicates that we transformed a string with length 4. Once
|
|
2466 |
you have a pretty type, you can, for example, control where linebreaks may
|
|
2467 |
occur in case the text wraps over a line, or with how much indentation a
|
|
2468 |
text should be printed. However, if you want to actually output the
|
|
2469 |
formatted text, you have to transform the pretty type back into a @{ML_type
|
|
2470 |
string}. This can be done with the function @{ML_ind string_of in Pretty}. In what
|
|
2471 |
follows we will use the following wrapper function for printing a pretty
|
|
2472 |
type:
|
|
2473 |
*}
|
|
2474 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2475 |
ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*}
|
318
|
2476 |
|
|
2477 |
text {*
|
|
2478 |
The point of the pretty-printing infrastructure is to give hints about how to
|
|
2479 |
layout text and let Isabelle do the actual layout. Let us first explain
|
|
2480 |
how you can insert places where a line break can occur. For this assume the
|
|
2481 |
following function that replicates a string n times:
|
|
2482 |
*}
|
|
2483 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2484 |
ML %grayML{*fun rep n str = implode (replicate n str) *}
|
318
|
2485 |
|
|
2486 |
text {*
|
|
2487 |
and suppose we want to print out the string:
|
|
2488 |
*}
|
|
2489 |
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
2490 |
ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
|
318
|
2491 |
|
|
2492 |
text {*
|
|
2493 |
We deliberately chose a large string so that it spans over more than one line.
|
|
2494 |
If we print out the string using the usual ``quick-and-dirty'' method, then
|
|
2495 |
we obtain the ugly output:
|
|
2496 |
|
|
2497 |
@{ML_response_fake [display,gray]
|
|
2498 |
"tracing test_str"
|
|
2499 |
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
|
|
2500 |
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
|
|
2501 |
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
|
|
2502 |
oooooooooooooobaaaaaaaaaaaar"}
|
|
2503 |
|
336
|
2504 |
We obtain the same if we just use the function @{ML pprint}.
|
318
|
2505 |
|
|
2506 |
@{ML_response_fake [display,gray]
|
|
2507 |
"pprint (Pretty.str test_str)"
|
|
2508 |
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
|
|
2509 |
ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
|
|
2510 |
aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
|
|
2511 |
oooooooooooooobaaaaaaaaaaaar"}
|
|
2512 |
|
336
|
2513 |
However by using pretty types you have the ability to indicate possible
|
|
2514 |
linebreaks for example at each whitespace. You can achieve this with the
|
|
2515 |
function @{ML_ind breaks in Pretty}, which expects a list of pretty types
|
|
2516 |
and inserts a possible line break in between every two elements in this
|
|
2517 |
list. To print this list of pretty types as a single string, we concatenate
|
|
2518 |
them with the function @{ML_ind blk in Pretty} as follows:
|
318
|
2519 |
|
|
2520 |
@{ML_response_fake [display,gray]
|
|
2521 |
"let
|
|
2522 |
val ptrs = map Pretty.str (space_explode \" \" test_str)
|
|
2523 |
in
|
|
2524 |
pprint (Pretty.blk (0, Pretty.breaks ptrs))
|
|
2525 |
end"
|
|
2526 |
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2527 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2528 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2529 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
|
|
2530 |
|
|
2531 |
Here the layout of @{ML test_str} is much more pleasing to the
|
360
|
2532 |
eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no hanging
|
|
2533 |
indentation of the printed string. You can increase the indentation
|
|
2534 |
and obtain
|
318
|
2535 |
|
|
2536 |
@{ML_response_fake [display,gray]
|
|
2537 |
"let
|
|
2538 |
val ptrs = map Pretty.str (space_explode \" \" test_str)
|
|
2539 |
in
|
|
2540 |
pprint (Pretty.blk (3, Pretty.breaks ptrs))
|
|
2541 |
end"
|
|
2542 |
"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2543 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2544 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2545 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
|
|
2546 |
|
|
2547 |
where starting from the second line the indent is 3. If you want
|
|
2548 |
that every line starts with the same indent, you can use the
|
|
2549 |
function @{ML_ind indent in Pretty} as follows:
|
|
2550 |
|
|
2551 |
@{ML_response_fake [display,gray]
|
|
2552 |
"let
|
|
2553 |
val ptrs = map Pretty.str (space_explode \" \" test_str)
|
|
2554 |
in
|
|
2555 |
pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
|
|
2556 |
end"
|
|
2557 |
" fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2558 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2559 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
|
|
2560 |
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
|
|
2561 |
|
|
2562 |
If you want to print out a list of items separated by commas and
|
|
2563 |
have the linebreaks handled properly, you can use the function
|
|
2564 |
@{ML_ind commas in Pretty}. For example
|
|
2565 |
|
|
2566 |
@{ML_response_fake [display,gray]
|
|
2567 |
"let
|
|
2568 |
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
|
|
2569 |
in
|
|
2570 |
pprint (Pretty.blk (0, Pretty.commas ptrs))
|
|
2571 |
end"
|
|
2572 |
"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
|
|
2573 |
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
|
|
2574 |
100016, 100017, 100018, 100019, 100020"}
|
|
2575 |
|
|
2576 |
where @{ML upto} generates a list of integers. You can print out this
|
|
2577 |
list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
|
|
2578 |
@{text [quotes] "}"}, and separated by commas using the function
|
|
2579 |
@{ML_ind enum in Pretty}. For example
|
|
2580 |
*}
|
|
2581 |
|
|
2582 |
text {*
|
|
2583 |
|
|
2584 |
@{ML_response_fake [display,gray]
|
|
2585 |
"let
|
|
2586 |
val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
|
|
2587 |
in
|
|
2588 |
pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)
|
|
2589 |
end"
|
|
2590 |
"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006,
|
|
2591 |
100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015,
|
|
2592 |
100016, 100017, 100018, 100019, 100020}"}
|
|
2593 |
|
|
2594 |
As can be seen, this function prints out the ``set'' so that starting
|
336
|
2595 |
from the second, each new line has an indentation of 2.
|
318
|
2596 |
|
|
2597 |
If you print out something that goes beyond the capabilities of the
|
|
2598 |
standard functions, you can do relatively easily the formatting
|
|
2599 |
yourself. Assume you want to print out a list of items where like in ``English''
|
|
2600 |
the last two items are separated by @{text [quotes] "and"}. For this you can
|
|
2601 |
write the function
|
|
2602 |
|
|
2603 |
*}
|
|
2604 |
|
|
2605 |
ML %linenosgray{*fun and_list [] = []
|
|
2606 |
| and_list [x] = [x]
|
|
2607 |
| and_list xs =
|
|
2608 |
let
|
|
2609 |
val (front, last) = split_last xs
|
|
2610 |
in
|
|
2611 |
(Pretty.commas front) @
|
|
2612 |
[Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]
|
|
2613 |
end *}
|
|
2614 |
|
|
2615 |
text {*
|
|
2616 |
where Line 7 prints the beginning of the list and Line
|
|
2617 |
8 the last item. We have to use @{ML "Pretty.brk 1"} in order
|
|
2618 |
to insert a space (of length 1) before the
|
|
2619 |
@{text [quotes] "and"}. This space is also a place where a line break
|
|
2620 |
can occur. We do the same after the @{text [quotes] "and"}. This gives you
|
|
2621 |
for example
|
|
2622 |
|
|
2623 |
@{ML_response_fake [display,gray]
|
|
2624 |
"let
|
336
|
2625 |
val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
|
|
2626 |
val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
|
318
|
2627 |
in
|
336
|
2628 |
pprint (Pretty.blk (0, and_list ptrs1));
|
|
2629 |
pprint (Pretty.blk (0, and_list ptrs2))
|
318
|
2630 |
end"
|
|
2631 |
"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21
|
336
|
2632 |
and 22
|
|
2633 |
10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
|
|
2634 |
28"}
|
318
|
2635 |
|
396
|
2636 |
Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out
|
|
2637 |
a list of items, but automatically inserts forced breaks between each item.
|
|
2638 |
Compare
|
318
|
2639 |
|
|
2640 |
@{ML_response_fake [display,gray]
|
396
|
2641 |
"let
|
|
2642 |
val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
|
|
2643 |
in
|
|
2644 |
pprint (Pretty.blk (0, a_and_b));
|
|
2645 |
pprint (Pretty.chunks a_and_b)
|
|
2646 |
end"
|
|
2647 |
"ab
|
|
2648 |
a
|
|
2649 |
b"}
|
318
|
2650 |
|
336
|
2651 |
The function @{ML_ind big_list in Pretty} helps with printing long lists.
|
|
2652 |
It is used for example in the command \isacommand{print\_theorems}. An
|
|
2653 |
example is as follows.
|
318
|
2654 |
|
336
|
2655 |
@{ML_response_fake [display,gray]
|
|
2656 |
"let
|
|
2657 |
val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
|
|
2658 |
in
|
|
2659 |
pprint (Pretty.big_list \"header\" pstrs)
|
|
2660 |
end"
|
|
2661 |
"header
|
|
2662 |
4
|
|
2663 |
5
|
|
2664 |
6
|
|
2665 |
7
|
|
2666 |
8
|
|
2667 |
9
|
|
2668 |
10"}
|
|
2669 |
|
396
|
2670 |
The point of the pretty-printing functions is to conveninetly obtain
|
|
2671 |
a lay-out of terms and types that is pleasing to the eye. If we print
|
|
2672 |
out the the terms produced by the the function @{ML de_bruijn} from
|
|
2673 |
exercise~\ref{ex:debruijn} we obtain the following:
|
336
|
2674 |
|
|
2675 |
@{ML_response_fake [display,gray]
|
396
|
2676 |
"pprint (Syntax.pretty_term @{context} (de_bruijn 4))"
|
|
2677 |
"(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
|
|
2678 |
(P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
|
|
2679 |
(P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
|
|
2680 |
(P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
|
|
2681 |
P 4 \<and> P 3 \<and> P 2 \<and> P 1"}
|
|
2682 |
|
|
2683 |
We use the function @{ML_ind pretty_term in Syntax} for pretty-printing
|
|
2684 |
terms. Next we like to pretty-print a term and its type. For this we use the
|
|
2685 |
function @{text "tell_type"}.
|
|
2686 |
*}
|
|
2687 |
|
|
2688 |
ML %linenosgray{*fun tell_type ctxt trm =
|
|
2689 |
let
|
|
2690 |
fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
|
|
2691 |
val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm)
|
|
2692 |
val pty = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of trm))
|
336
|
2693 |
in
|
396
|
2694 |
pprint (Pretty.blk (0,
|
|
2695 |
(pstr "The term " @ [ptrm] @ pstr " has type "
|
|
2696 |
@ [pty, Pretty.str "."])))
|
|
2697 |
end*}
|
|
2698 |
|
|
2699 |
text {*
|
|
2700 |
In Line 3 we define a function that inserts possible linebreaks in places
|
|
2701 |
where a space is. In Lines 4 and 5 we pretty-print the term and its type
|
|
2702 |
using the functions @{ML pretty_term in Syntax} and @{ML_ind
|
|
2703 |
pretty_typ in Syntax}. We also use the function @{ML_ind quote in
|
|
2704 |
Pretty} in order to enclose the term and type inside quotation marks. In
|
|
2705 |
Line 9 we add a period right after the type without the possibility of a
|
|
2706 |
line break, because we do not want that a line break occurs there.
|
|
2707 |
Now you can write
|
|
2708 |
|
|
2709 |
@{ML_response_fake [display,gray]
|
|
2710 |
"tell_type @{context} @{term \"min (Suc 0)\"}"
|
|
2711 |
"The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
|
336
|
2712 |
|
396
|
2713 |
To see the proper line breaking, you can try out the function on a bigger term
|
|
2714 |
and type. For example:
|
336
|
2715 |
|
396
|
2716 |
@{ML_response_fake [display,gray]
|
|
2717 |
"tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
|
|
2718 |
"The term \"op = (op = (op = (op = (op = op =))))\" has type
|
|
2719 |
\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
|
336
|
2720 |
|
|
2721 |
\begin{readmore}
|
|
2722 |
The general infrastructure for pretty-printing is implemented in the file
|
|
2723 |
@{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
|
|
2724 |
contains pretty-printing functions for terms, types, theorems and so on.
|
|
2725 |
|
505
|
2726 |
@{ML_file "Pure/PIDE/markup.ML"}
|
336
|
2727 |
\end{readmore}
|
318
|
2728 |
*}
|
|
2729 |
|
349
|
2730 |
section {* Summary *}
|
|
2731 |
|
|
2732 |
text {*
|
|
2733 |
\begin{conventions}
|
|
2734 |
\begin{itemize}
|
|
2735 |
\item Start with a proper context and then pass it around
|
|
2736 |
through all your functions.
|
|
2737 |
\end{itemize}
|
|
2738 |
\end{conventions}
|
|
2739 |
*}
|
318
|
2740 |
|
|
2741 |
end
|