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