2
+ − 1
theory FirstSteps
25
+ − 2
imports Base
2
+ − 3
begin
+ − 4
+ − 5
chapter {* First Steps *}
+ − 6
42
+ − 7
text {*
+ − 8
54
+ − 9
Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
89
+ − 10
in Isabelle is part of a theory. If you want to follow the code given in
54
+ − 11
this chapter, we assume you are working inside the theory starting with
2
+ − 12
6
+ − 13
\begin{center}
5
+ − 14
\begin{tabular}{@ {}l}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 15
\isacommand{theory} FirstSteps\\
5
+ − 16
\isacommand{imports} Main\\
+ − 17
\isacommand{begin}\\
6
+ − 18
\ldots
5
+ − 19
\end{tabular}
6
+ − 20
\end{center}
157
+ − 21
+ − 22
We also generally assume you are working with HOL. The given examples might
193
+ − 23
need to be adapted if you work in a different logic.
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 24
*}
5
+ − 25
20
+ − 26
section {* Including ML-Code *}
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 27
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 28
text {*
5
+ − 29
The easiest and quickest way to include code in a theory is
89
+ − 30
by using the \isacommand{ML}-command. For example:
2
+ − 31
75
+ − 32
\begin{isabelle}
+ − 33
\begin{graybox}
85
+ − 34
\isacommand{ML}~@{text "\<verbopen>"}\isanewline
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 35
\hspace{5mm}@{ML "3 + 4"}\isanewline
85
+ − 36
@{text "\<verbclose>"}\isanewline
+ − 37
@{text "> 7"}\smallskip
75
+ − 38
\end{graybox}
+ − 39
\end{isabelle}
2
+ − 40
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 41
Like normal Isabelle proof scripts, \isacommand{ML}-commands can be
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 42
evaluated by using the advance and undo buttons of your Isabelle
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 43
environment. The code inside the \isacommand{ML}-command can also contain
193
+ − 44
value and function bindings, for example
+ − 45
*}
+ − 46
+ − 47
ML %gray {*
+ − 48
val r = ref 0
+ − 49
fun f n = n + 1
+ − 50
*}
+ − 51
+ − 52
text {*
+ − 53
and even those can be undone when the proof
+ − 54
script is retracted. As mentioned in the Introduction, we will drop the
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 55
\isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
107
+ − 56
show code. The lines prefixed with @{text [quotes] ">"} are not part of the
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 57
code, rather they indicate what the response is when the code is evaluated.
10
+ − 58
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 59
Once a portion of code is relatively stable, you usually want to export it
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 60
to a separate ML-file. Such files can then be included in a theory by using
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 61
the \isacommand{uses}-command in the header of the theory, like:
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 62
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 63
\begin{center}
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 64
\begin{tabular}{@ {}l}
54
+ − 65
\isacommand{theory} FirstSteps\\
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 66
\isacommand{imports} Main\\
58
+ − 67
\isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 68
\isacommand{begin}\\
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 69
\ldots
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 70
\end{tabular}
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 71
\end{center}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 72
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 73
*}
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 74
126
+ − 75
section {* Debugging and Printing\label{sec:printing} *}
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 76
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 77
text {*
13
+ − 78
50
+ − 79
During development you might find it necessary to inspect some data
10
+ − 80
in your code. This can be done in a ``quick-and-dirty'' fashion using
12
+ − 81
the function @{ML "warning"}. For example
10
+ − 82
161
+ − 83
@{ML_response_fake [display,gray] "warning \"any string\"" "\"any string\""}
10
+ − 84
58
+ − 85
will print out @{text [quotes] "any string"} inside the response buffer
+ − 86
of Isabelle. This function expects a string as argument. If you develop under PolyML,
50
+ − 87
then there is a convenient, though again ``quick-and-dirty'', method for
107
+ − 88
converting values into strings, namely the function @{ML makestring}:
10
+ − 89
161
+ − 90
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
12
+ − 91
65
+ − 92
However @{ML makestring} only works if the type of what is converted is monomorphic
78
+ − 93
and not a function.
12
+ − 94
52
+ − 95
The function @{ML "warning"} should only be used for testing purposes, because any
+ − 96
output this function generates will be overwritten as soon as an error is
50
+ − 97
raised. For printing anything more serious and elaborate, the
54
+ − 98
function @{ML tracing} is more appropriate. This function writes all output into
89
+ − 99
a separate tracing buffer. For example:
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 100
161
+ − 101
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 102
58
+ − 103
It is also possible to redirect the ``channel'' where the string @{text "foo"} is
78
+ − 104
printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
107
+ − 105
amounts of trace output. This redirection can be achieved with the code:
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 106
*}
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 107
69
+ − 108
ML{*val strip_specials =
42
+ − 109
let
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 110
fun strip ("\^A" :: _ :: cs) = strip cs
42
+ − 111
| strip (c :: cs) = c :: strip cs
+ − 112
| strip [] = [];
+ − 113
in implode o strip o explode end;
+ − 114
+ − 115
fun redirect_tracing stream =
+ − 116
Output.tracing_fn := (fn s =>
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 117
(TextIO.output (stream, (strip_specials s));
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 118
TextIO.output (stream, "\n");
69
+ − 119
TextIO.flushOut stream)) *}
14
1c17e99f6f66
added a paragraph about "uses" and started a paragraph about tracing
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 120
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 121
text {*
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 122
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
58
+ − 123
will cause that all tracing information is printed into the file @{text "foo.bar"}.
75
+ − 124
107
+ − 125
You can print out error messages with the function @{ML error}; for example:
75
+ − 126
122
+ − 127
@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
+ − 128
"Exception- ERROR \"foo\" raised
+ − 129
At command \"ML\"."}
75
+ − 130
192
+ − 131
(FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling})
+ − 132
*}
+ − 133
+ − 134
(*
193
+ − 135
ML {* set Toplevel.debug *}
+ − 136
192
+ − 137
ML {*
+ − 138
fun dodgy_fun () = (raise (ERROR "bar"); 1)
+ − 139
*}
+ − 140
+ − 141
ML {* fun f1 () = dodgy_fun () *}
+ − 142
+ − 143
ML {* f1 () *}
+ − 144
*)
+ − 145
+ − 146
text {*
126
+ − 147
Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm}
+ − 148
or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing them,
+ − 149
but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
+ − 150
a term into a string is to use the function @{ML Syntax.string_of_term}.
+ − 151
+ − 152
@{ML_response_fake [display,gray]
+ − 153
"Syntax.string_of_term @{context} @{term \"1::nat\"}"
+ − 154
"\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+ − 155
+ − 156
This produces a string with some additional information encoded in it. The string
+ − 157
can be properly printed by using the function @{ML warning}.
+ − 158
+ − 159
@{ML_response_fake [display,gray]
+ − 160
"warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+ − 161
"\"1\""}
+ − 162
+ − 163
A @{ML_type cterm} can be transformed into a string by the following function.
+ − 164
*}
+ − 165
+ − 166
ML{*fun str_of_cterm ctxt t =
+ − 167
Syntax.string_of_term ctxt (term_of t)*}
+ − 168
+ − 169
text {*
149
+ − 170
In this example the function @{ML term_of} extracts the @{ML_type term} from
+ − 171
a @{ML_type cterm}. If there are more than one @{ML_type cterm}s to be
+ − 172
printed, you can use the function @{ML commas} to separate them.
126
+ − 173
*}
+ − 174
+ − 175
ML{*fun str_of_cterms ctxt ts =
+ − 176
commas (map (str_of_cterm ctxt) ts)*}
+ − 177
+ − 178
text {*
+ − 179
The easiest way to get the string of a theorem is to transform it
190
+ − 180
into a @{ML_type cterm} using the function @{ML crep_thm}.
+ − 181
*}
+ − 182
194
+ − 183
ML{*fun str_of_thm ctxt thm =
190
+ − 184
str_of_cterm ctxt (#prop (crep_thm thm))*}
+ − 185
+ − 186
text {*
+ − 187
Theorems also include schematic variables, such as @{text "?P"},
+ − 188
@{text "?Q"} and so on.
+ − 189
+ − 190
@{ML_response_fake [display, gray]
194
+ − 191
"warning (str_of_thm @{context} @{thm conjI})"
190
+ − 192
"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+ − 193
+ − 194
In order to improve the readability of theorems we convert
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 195
these schematic variables into free variables using the
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 196
function @{ML Variable.import_thms}.
126
+ − 197
*}
+ − 198
158
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 199
ML{*fun no_vars ctxt thm =
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 200
let
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 201
val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 202
in
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 203
thm'
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 204
end
d7944bdf7b3f
removed infix_conv and moved function no_vars into the FirstSteps chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 205
194
+ − 206
fun str_of_thm_no_vars ctxt thm =
171
+ − 207
str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
126
+ − 208
+ − 209
text {*
194
+ − 210
Theorem @{thm [source] conjI} looks now as follows:
190
+ − 211
+ − 212
@{ML_response_fake [display, gray]
194
+ − 213
"warning (str_of_thm_no_vars @{context} @{thm conjI})"
+ − 214
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
190
+ − 215
126
+ − 216
Again the function @{ML commas} helps with printing more than one theorem.
+ − 217
*}
+ − 218
+ − 219
ML{*fun str_of_thms ctxt thms =
190
+ − 220
commas (map (str_of_thm ctxt) thms)
+ − 221
194
+ − 222
fun str_of_thms_no_vars ctxt thms =
+ − 223
commas (map (str_of_thm_no_vars ctxt) thms) *}
126
+ − 224
+ − 225
section {* Combinators\label{sec:combinators} *}
+ − 226
+ − 227
text {*
131
+ − 228
For beginners perhaps the most puzzling parts in the existing code of Isabelle are
126
+ − 229
the combinators. At first they seem to greatly obstruct the
+ − 230
comprehension of the code, but after getting familiar with them, they
+ − 231
actually ease the understanding and also the programming.
+ − 232
+ − 233
The simplest combinator is @{ML I}, which is just the identity function defined as
+ − 234
*}
+ − 235
+ − 236
ML{*fun I x = x*}
+ − 237
+ − 238
text {* Another simple combinator is @{ML K}, defined as *}
+ − 239
+ − 240
ML{*fun K x = fn _ => x*}
+ − 241
+ − 242
text {*
+ − 243
@{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
+ − 244
function ignores its argument. As a result, @{ML K} defines a constant function
+ − 245
always returning @{text x}.
+ − 246
+ − 247
The next combinator is reverse application, @{ML "|>"}, defined as:
+ − 248
*}
+ − 249
+ − 250
ML{*fun x |> f = f x*}
+ − 251
+ − 252
text {* While just syntactic sugar for the usual function application,
+ − 253
the purpose of this combinator is to implement functions in a
+ − 254
``waterfall fashion''. Consider for example the function *}
+ − 255
+ − 256
ML %linenosgray{*fun inc_by_five x =
+ − 257
x |> (fn x => x + 1)
+ − 258
|> (fn x => (x, x))
+ − 259
|> fst
+ − 260
|> (fn x => x + 4)*}
+ − 261
+ − 262
text {*
+ − 263
which increments its argument @{text x} by 5. It does this by first incrementing
+ − 264
the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
+ − 265
the first component of the pair (Line 4) and finally incrementing the first
+ − 266
component by 4 (Line 5). This kind of cascading manipulations of values is quite
+ − 267
common when dealing with theories (for example by adding a definition, followed by
+ − 268
lemmas and so on). The reverse application allows you to read what happens in
+ − 269
a top-down manner. This kind of coding should also be familiar,
149
+ − 270
if you have been exposed to Haskell's do-notation. Writing the function @{ML inc_by_five} using
126
+ − 271
the reverse application is much clearer than writing
+ − 272
*}
+ − 273
+ − 274
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
+ − 275
+ − 276
text {* or *}
+ − 277
+ − 278
ML{*fun inc_by_five x =
+ − 279
((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
+ − 280
+ − 281
text {* and typographically more economical than *}
+ − 282
+ − 283
ML{*fun inc_by_five x =
+ − 284
let val y1 = x + 1
+ − 285
val y2 = (y1, y1)
+ − 286
val y3 = fst y2
+ − 287
val y4 = y3 + 4
+ − 288
in y4 end*}
+ − 289
+ − 290
text {*
+ − 291
Another reason why the let-bindings in the code above are better to be
+ − 292
avoided: it is more than easy to get the intermediate values wrong, not to
+ − 293
mention the nightmares the maintenance of this code causes!
+ − 294
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 295
In the context of Isabelle, a ``real world'' example for a function written in
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 296
the waterfall fashion might be the following code:
177
+ − 297
*}
126
+ − 298
193
+ − 299
ML %linenosgray{*fun apply_fresh_args f ctxt =
+ − 300
f |> fastype_of
+ − 301
|> binder_types
+ − 302
|> map (pair "z")
+ − 303
|> Variable.variant_frees ctxt [f]
+ − 304
|> map Free
+ − 305
|> (curry list_comb) f *}
126
+ − 306
177
+ − 307
text {*
194
+ − 308
This code extracts the argument types of a given function @{text "f"} and then generates
193
+ − 309
for each argument type a distinct variable; finally it applies the generated
194
+ − 310
variables to the function. For example:
183
+ − 311
+ − 312
@{ML_response_fake [display,gray]
+ − 313
"apply_fresh_args @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"} @{context}
+ − 314
|> Syntax.string_of_term @{context}
+ − 315
|> warning"
+ − 316
"P z za zb"}
177
+ − 317
184
+ − 318
You can read off this behaviour from how @{ML apply_fresh_args} is
183
+ − 319
coded: in Line 2, the function @{ML fastype_of} calculates the type of the
193
+ − 320
function; @{ML binder_types} in the next line produces the list of argument
184
+ − 321
types (in the case above the list @{text "[nat, int, unit]"}); Line 4
+ − 322
pairs up each type with the string @{text "z"}; the
183
+ − 323
function @{ML variant_frees in Variable} generates for each @{text "z"} a
193
+ − 324
unique name avoiding the given @{text f}; the list of name-type pairs is turned
184
+ − 325
into a list of variable terms in Line 6, which in the last line is applied
194
+ − 326
by the function @{ML list_comb} to the function. In this last step we have to
+ − 327
use the function @{ML curry}, because @{ML list_comb} expects the function and the
184
+ − 328
variables list as a pair.
177
+ − 329
+ − 330
The combinator @{ML "#>"} is the reverse function composition. It can be
+ − 331
used to define the following function
126
+ − 332
*}
+ − 333
+ − 334
ML{*val inc_by_six =
+ − 335
(fn x => x + 1)
+ − 336
#> (fn x => x + 2)
+ − 337
#> (fn x => x + 3)*}
+ − 338
+ − 339
text {*
+ − 340
which is the function composed of first the increment-by-one function and then
+ − 341
increment-by-two, followed by increment-by-three. Again, the reverse function
+ − 342
composition allows you to read the code top-down.
+ − 343
+ − 344
The remaining combinators described in this section add convenience for the
+ − 345
``waterfall method'' of writing functions. The combinator @{ML tap} allows
+ − 346
you to get hold of an intermediate result (to do some side-calculations for
+ − 347
instance). The function
+ − 348
+ − 349
*}
+ − 350
+ − 351
ML %linenosgray{*fun inc_by_three x =
+ − 352
x |> (fn x => x + 1)
+ − 353
|> tap (fn x => tracing (makestring x))
+ − 354
|> (fn x => x + 2)*}
+ − 355
+ − 356
text {*
+ − 357
increments the argument first by @{text "1"} and then by @{text "2"}. In the
+ − 358
middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
+ − 359
intermediate result inside the tracing buffer. The function @{ML tap} can
+ − 360
only be used for side-calculations, because any value that is computed
+ − 361
cannot be merged back into the ``main waterfall''. To do this, you can use
+ − 362
the next combinator.
+ − 363
+ − 364
The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
+ − 365
and returns the result together with the value (as a pair). For example
+ − 366
the function
+ − 367
*}
+ − 368
+ − 369
ML{*fun inc_as_pair x =
+ − 370
x |> `(fn x => x + 1)
+ − 371
|> (fn (x, y) => (x, y + 1))*}
+ − 372
+ − 373
text {*
+ − 374
takes @{text x} as argument, and then increments @{text x}, but also keeps
+ − 375
@{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+ − 376
for x}. After that, the function increments the right-hand component of the
+ − 377
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+ − 378
+ − 379
The combinators @{ML "|>>"} and @{ML "||>"} are defined for
+ − 380
functions manipulating pairs. The first applies the function to
+ − 381
the first component of the pair, defined as
+ − 382
*}
+ − 383
+ − 384
ML{*fun (x, y) |>> f = (f x, y)*}
+ − 385
+ − 386
text {*
+ − 387
and the second combinator to the second component, defined as
+ − 388
*}
+ − 389
+ − 390
ML{*fun (x, y) ||> f = (x, f y)*}
+ − 391
+ − 392
text {*
+ − 393
With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+ − 394
This combinator is defined as
+ − 395
*}
+ − 396
+ − 397
ML{*fun (x, y) |-> f = f x y*}
+ − 398
+ − 399
text {* and can be used to write the following roundabout version
+ − 400
of the @{text double} function:
+ − 401
*}
+ − 402
+ − 403
ML{*fun double x =
+ − 404
x |> (fn x => (x, x))
+ − 405
|-> (fn x => fn y => x + y)*}
+ − 406
+ − 407
text {*
+ − 408
Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
+ − 409
reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
+ − 410
@{ML "|>>"} and @{ML "||>"} described above have related combinators for function
+ − 411
composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
+ − 412
for example, the function @{text double} can also be written as:
+ − 413
*}
+ − 414
+ − 415
ML{*val double =
+ − 416
(fn x => (x, x))
+ − 417
#-> (fn x => fn y => x + y)*}
+ − 418
+ − 419
text {*
+ − 420
+ − 421
(FIXME: find a good exercise for combinators)
127
+ − 422
+ − 423
\begin{readmore}
+ − 424
The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+ − 425
and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
+ − 426
contains further information about combinators.
+ − 427
\end{readmore}
126
+ − 428
15
+ − 429
*}
+ − 430
10
+ − 431
2
+ − 432
section {* Antiquotations *}
+ − 433
+ − 434
text {*
49
+ − 435
The main advantage of embedding all code in a theory is that the code can
58
+ − 436
contain references to entities defined on the logical level of Isabelle. By
+ − 437
this we mean definitions, theorems, terms and so on. This kind of reference is
+ − 438
realised with antiquotations. For example, one can print out the name of the current
49
+ − 439
theory by typing
+ − 440
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 441
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 442
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 443
5
+ − 444
where @{text "@{theory}"} is an antiquotation that is substituted with the
49
+ − 445
current theory (remember that we assumed we are inside the theory
89
+ − 446
@{text FirstSteps}). The name of this theory can be extracted using
49
+ − 447
the function @{ML "Context.theory_name"}.
5
+ − 448
89
+ − 449
Note, however, that antiquotations are statically linked, that is their value is
12
+ − 450
determined at ``compile-time'', not ``run-time''. For example the function
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 451
*}
5
+ − 452
69
+ − 453
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 454
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 455
text {*
2
+ − 456
89
+ − 457
does \emph{not} return the name of the current theory, if it is run in a
5
+ − 458
different theory. Instead, the code above defines the constant function
58
+ − 459
that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 460
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
5
+ − 461
\emph{not} replaced with code that will look up the current theory in
+ − 462
some data structure and return it. Instead, it is literally
+ − 463
replaced with the value representing the theory name.
2
+ − 464
132
+ − 465
In a similar way you can use antiquotations to refer to proved theorems:
133
+ − 466
@{text "@{thm \<dots>}"} for a single theorem
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 467
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 468
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
75
+ − 469
133
+ − 470
and @{text "@{thms \<dots>}"} for more than one
132
+ − 471
+ − 472
@{ML_response_fake [display,gray] "@{thms conj_ac}"
+ − 473
"(?P \<and> ?Q) = (?Q \<and> ?P)
+ − 474
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
+ − 475
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
+ − 476
149
+ − 477
You can also refer to the current simpset. To illustrate this we implement the
132
+ − 478
function that extracts the theorem names stored in a simpset.
131
+ − 479
*}
75
+ − 480
149
+ − 481
ML{*fun get_thm_names_from_ss simpset =
131
+ − 482
let
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 483
val {simps,...} = MetaSimplifier.dest_ss simpset
70
+ − 484
in
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 485
map #1 simps
131
+ − 486
end*}
54
+ − 487
131
+ − 488
text {*
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 489
The function @{ML dest_ss in MetaSimplifier} returns a record containing all
193
+ − 490
information stored in the simpset, but we are only interested in the names of the
184
+ − 491
simp-rules. So now you can feed in the current simpset into this function.
193
+ − 492
The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
81
+ − 493
131
+ − 494
@{ML_response_fake [display,gray]
149
+ − 495
"get_thm_names_from_ss @{simpset}"
+ − 496
"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
10
+ − 497
156
+ − 498
Again, this way or referencing simpsets makes you independent from additions
+ − 499
of lemmas to the simpset by the user that potentially cause loops.
+ − 500
192
+ − 501
On the ML-level of Isabelle, you often have to work with qualified names;
+ − 502
these are strings with some additional information, such positional information
+ − 503
and qualifiers. Such bindings can be generated with the antiquotation
193
+ − 504
@{text "@{binding \<dots>}"}.
192
+ − 505
+ − 506
@{ML_response [display,gray]
+ − 507
"@{binding \"name\"}"
+ − 508
"name"}
+ − 509
+ − 510
An example where a binding is needed is the function @{ML define in LocalTheory}.
+ − 511
Below this function defines the constant @{term "TrueConj"} as the conjunction
+ − 512
@{term "True \<and> True"}.
+ − 513
*}
+ − 514
+ − 515
local_setup %gray {*
+ − 516
snd o LocalTheory.define Thm.internalK
+ − 517
((@{binding "TrueConj"}, NoSyn),
+ − 518
(Attrib.empty_binding, @{term "True \<and> True"})) *}
+ − 519
193
+ − 520
text {*
+ − 521
Now querying the definition you obtain:
+ − 522
+ − 523
\begin{isabelle}
+ − 524
\isacommand{thm}~@{text "TrueConj_def"}\\
+ − 525
@{text "> "}@{thm TrueConj_def}
+ − 526
\end{isabelle}
+ − 527
194
+ − 528
(FIXME give a better example why bindings are important; maybe
+ − 529
give a pointer to \isacommand{local\_setup})
193
+ − 530
75
+ − 531
While antiquotations have many applications, they were originally introduced in order
89
+ − 532
to avoid explicit bindings for theorems such as:
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 533
*}
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 534
69
+ − 535
ML{*val allI = thm "allI" *}
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 536
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 537
text {*
78
+ − 538
These bindings are difficult to maintain and also can be accidentally
156
+ − 539
overwritten by the user. This often broke Isabelle
49
+ − 540
packages. Antiquotations solve this problem, since they are ``linked''
89
+ − 541
statically at compile-time. However, this static linkage also limits their
+ − 542
usefulness in cases where data needs to be build up dynamically. In the
149
+ − 543
course of this chapter you will learn more about these antiquotations:
122
+ − 544
they can simplify Isabelle programming since one can directly access all
89
+ − 545
kinds of logical elements from th ML-level.
2
+ − 546
*}
+ − 547
15
+ − 548
section {* Terms and Types *}
2
+ − 549
+ − 550
text {*
122
+ − 551
One way to construct terms of Isabelle is by using the antiquotation
89
+ − 552
\mbox{@{text "@{term \<dots>}"}}. For example:
2
+ − 553
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 554
@{ML_response [display,gray]
75
+ − 555
"@{term \"(a::nat) + b = c\"}"
+ − 556
"Const (\"op =\", \<dots>) $
149
+ − 557
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
2
+ − 558
50
+ − 559
This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
13
+ − 560
representation of this term. This internal representation corresponds to the
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 561
datatype @{ML_type "term"}.
2
+ − 562
34
+ − 563
The internal representation of terms uses the usual de Bruijn index mechanism where bound
11
+ − 564
variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
10
+ − 565
the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
12
+ − 566
binds the corresponding variable. However, in Isabelle the names of bound variables are
149
+ − 567
kept at abstractions for printing purposes, and so should be treated only as ``comments''.
123
+ − 568
Application in Isabelle is realised with the term-constructor @{ML $}.
10
+ − 569
2
+ − 570
\begin{readmore}
13
+ − 571
Terms are described in detail in \isccite{sec:terms}. Their
78
+ − 572
definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
2
+ − 573
\end{readmore}
193
+ − 574
+ − 575
Constructing terms via antiquotations has the advantage that only typable
+ − 576
terms can be constructed. For example
2
+ − 577
193
+ − 578
@{ML_response_fake_both [display,gray]
+ − 579
"@{term \"(x::nat) x\"}"
+ − 580
"Type unification failed \<dots>"}
+ − 581
194
+ − 582
raises a typing error, while it perfectly ok to construct the term
193
+ − 583
+ − 584
@{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"}
+ − 585
+ − 586
with the raw ML-constructors.
13
+ − 587
Sometimes the internal representation of terms can be surprisingly different
157
+ − 588
from what you see at the user-level, because the layers of
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 589
parsing/type-checking/pretty printing can be quite elaborate.
2
+ − 590
10
+ − 591
\begin{exercise}
2
+ − 592
Look at the internal term representation of the following terms, and
89
+ − 593
find out why they are represented like this:
2
+ − 594
+ − 595
\begin{itemize}
+ − 596
\item @{term "case x of 0 \<Rightarrow> 0 | Suc y \<Rightarrow> y"}
+ − 597
\item @{term "\<lambda>(x,y). P y x"}
+ − 598
\item @{term "{ [x::int] | x. x \<le> -2 }"}
+ − 599
\end{itemize}
+ − 600
+ − 601
Hint: The third term is already quite big, and the pretty printer
+ − 602
may omit parts of it by default. If you want to see all of it, you
122
+ − 603
can use the following ML-function to set the printing depth to a higher
+ − 604
value:
12
+ − 605
75
+ − 606
@{ML [display,gray] "print_depth 50"}
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 607
\end{exercise}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 608
13
+ − 609
The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type,
50
+ − 610
inserting the invisible @{text "Trueprop"}-coercions whenever necessary.
68
+ − 611
Consider for example the pairs
12
+ − 612
126
+ − 613
@{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
+ − 614
"(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
149
+ − 615
Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
65
+ − 616
108
8bea3f74889d
added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 617
where a coercion is inserted in the second component and
12
+ − 618
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 619
@{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
65
+ − 620
"(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>, Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
12
+ − 621
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 622
where it is not (since it is already constructed by a meta-implication).
19
+ − 623
193
+ − 624
As already seen above, types can be constructed using the antiquotation
+ − 625
@{text "@{typ \<dots>}"}. For example:
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 626
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 627
@{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
39
631d12c25bde
substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 628
19
+ − 629
\begin{readmore}
+ − 630
Types are described in detail in \isccite{sec:types}. Their
78
+ − 631
definition and many useful operations are implemented
+ − 632
in @{ML_file "Pure/type.ML"}.
19
+ − 633
\end{readmore}
47
4daf913fdbe1
hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 634
*}
19
+ − 635
+ − 636
156
+ − 637
section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
12
+ − 638
+ − 639
text {*
81
+ − 640
While antiquotations are very convenient for constructing terms, they can
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 641
only construct fixed terms (remember they are ``linked'' at compile-time).
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 642
However, you often need to construct terms dynamically. For example, a
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 643
function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 644
@{term P} and @{term Q} as arguments can only be written as:
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 645
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 646
*}
12
+ − 647
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 648
ML{*fun make_imp P Q =
131
+ − 649
let
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 650
val x = Free ("x", @{typ nat})
131
+ − 651
in
+ − 652
Logic.all x (Logic.mk_implies (P $ x, Q $ x))
+ − 653
end *}
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 654
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 655
text {*
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 656
The reason is that you cannot pass the arguments @{term P} and @{term Q}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 657
into an antiquotation. For example the following does \emph{not} work.
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 658
*}
13
+ − 659
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 660
ML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
12
+ − 661
43
02f76f1b6e7b
added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 662
text {*
194
+ − 663
To see this, apply @{text "@{term S}"} and @{text "@{term T}"}
193
+ − 664
to both functions. With @{ML make_imp} you obtain the intended term involving
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 665
the given arguments
65
+ − 666
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 667
@{ML_response [display,gray] "make_imp @{term S} @{term T}"
162
+ − 668
"Const \<dots> $
+ − 669
Abs (\"x\", Type (\"nat\",[]),
+ − 670
Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
68
+ − 671
193
+ − 672
whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"}
68
+ − 673
and @{text "Q"} from the antiquotation.
+ − 674
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 675
@{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}"
162
+ − 676
"Const \<dots> $
+ − 677
Abs (\"x\", \<dots>,
+ − 678
Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
192
+ − 679
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
65
+ − 680
192
+ − 681
There are a number of handy functions that are frequently used for
193
+ − 682
constructing terms. One is the function @{ML list_comb}, which takes
194
+ − 683
a term and a list of terms as arguments, and produces as output the term
192
+ − 684
list applied to the term. For example
+ − 685
+ − 686
@{ML_response_fake [display,gray]
+ − 687
"list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
+ − 688
"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
+ − 689
193
+ − 690
Another handy function is @{ML lambda}, which abstracts a variable
+ − 691
in a term. For example
+ − 692
+ − 693
@{ML_response_fake [display,gray]
+ − 694
"lambda @{term \"x::nat\"} @{term \"(P::nat\<Rightarrow>bool) x\"}"
+ − 695
"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
+ − 696
194
+ − 697
In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}),
193
+ − 698
and an abstraction. It also records the type of the abstracted
+ − 699
variable and for printing purposes also its name. Note that because of the
+ − 700
typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
+ − 701
is of the same type as the abstracted variable. If it is of different type,
+ − 702
as in
+ − 703
+ − 704
@{ML_response_fake [display,gray]
+ − 705
"lambda @{term \"x::nat\"} @{term \"(P::bool\<Rightarrow>bool) x\"}"
+ − 706
"Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Free (\"x\", \"bool\"))"}
49
+ − 707
193
+ − 708
then the variable @{text "Free (\"x\", \"bool\")"} is \emph{not} abstracted.
+ − 709
This is a fundamental principle
+ − 710
of Church-style typing, where variables with the same name still differ, if they
+ − 711
have different type.
192
+ − 712
193
+ − 713
There is also the function @{ML subst_free} with which terms can
194
+ − 714
be replaced by other terms. For example below, we will replace in
+ − 715
@{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0 x"}
+ − 716
the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
49
+ − 717
193
+ − 718
@{ML_response_fake [display,gray]
+ − 719
"subst_free [(@{term \"(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0\"}, @{term \"y::nat\<Rightarrow>nat\"}),
+ − 720
(@{term \"x::nat\"}, @{term \"True\"})]
+ − 721
@{term \"((f::nat\<Rightarrow>nat\<Rightarrow>nat) 0) x\"}"
+ − 722
"Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
+ − 723
+ − 724
As can be seen, @{ML subst_free} does not take typability into account.
+ − 725
However it takes alpha-equivalence into account:
+ − 726
+ − 727
@{ML_response_fake [display, gray]
+ − 728
"subst_free [(@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})]
+ − 729
@{term \"(\<lambda>x::nat. x)\"}"
+ − 730
"Free (\"x\", \"nat\")"}
192
+ − 731
13
+ − 732
\begin{readmore}
89
+ − 733
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 734
@{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
49
+ − 735
and types easier.\end{readmore}
13
+ − 736
+ − 737
Have a look at these files and try to solve the following two exercises:
11
+ − 738
13
+ − 739
\begin{exercise}\label{fun:revsum}
58
+ − 740
Write a function @{text "rev_sum : term -> term"} that takes a
122
+ − 741
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "n"} might be zero)
11
+ − 742
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
+ − 743
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
13
+ − 744
associates to the left. Try your function on some examples.
11
+ − 745
\end{exercise}
+ − 746
15
+ − 747
\begin{exercise}\label{fun:makesum}
11
+ − 748
Write a function which takes two terms representing natural numbers
75
+ − 749
in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
11
+ − 750
number representing their sum.
+ − 751
\end{exercise}
+ − 752
122
+ − 753
There are a few subtle issues with constants. They usually crop up when
149
+ − 754
pattern matching terms or types, or when constructing them. While it is perfectly ok
122
+ − 755
to write the function @{text is_true} as follows
+ − 756
*}
+ − 757
+ − 758
ML{*fun is_true @{term True} = true
+ − 759
| is_true _ = false*}
+ − 760
+ − 761
text {*
+ − 762
this does not work for picking out @{text "\<forall>"}-quantified terms. Because
+ − 763
the function
+ − 764
*}
+ − 765
+ − 766
ML{*fun is_all (@{term All} $ _) = true
+ − 767
| is_all _ = false*}
+ − 768
+ − 769
text {*
123
+ − 770
will not correctly match the formula @{prop "\<forall>x::nat. P x"}:
122
+ − 771
+ − 772
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+ − 773
+ − 774
The problem is that the @{text "@term"}-antiquotation in the pattern
123
+ − 775
fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for
122
+ − 776
an arbitrary, but fixed type @{typ "'a"}. A properly working alternative
+ − 777
for this function is
+ − 778
*}
+ − 779
+ − 780
ML{*fun is_all (Const ("All", _) $ _) = true
+ − 781
| is_all _ = false*}
+ − 782
+ − 783
text {*
+ − 784
because now
+ − 785
+ − 786
@{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+ − 787
149
+ − 788
matches correctly (the first wildcard in the pattern matches any type and the
+ − 789
second any term).
122
+ − 790
123
+ − 791
However there is still a problem: consider the similar function that
131
+ − 792
attempts to pick out @{text "Nil"}-terms:
122
+ − 793
*}
+ − 794
+ − 795
ML{*fun is_nil (Const ("Nil", _)) = true
+ − 796
| is_nil _ = false *}
+ − 797
+ − 798
text {*
123
+ − 799
Unfortunately, also this function does \emph{not} work as expected, since
122
+ − 800
+ − 801
@{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
+ − 802
123
+ − 803
The problem is that on the ML-level the name of a constant is more
149
+ − 804
subtle than you might expect. The function @{ML is_all} worked correctly,
123
+ − 805
because @{term "All"} is such a fundamental constant, which can be referenced
+ − 806
by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
122
+ − 807
+ − 808
@{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
+ − 809
131
+ − 810
the name of the constant @{text "Nil"} depends on the theory in which the
128
+ − 811
term constructor is defined (@{text "List"}) and also in which datatype
+ − 812
(@{text "list"}). Even worse, some constants have a name involving
+ − 813
type-classes. Consider for example the constants for @{term "zero"} and
131
+ − 814
\mbox{@{text "(op *)"}}:
122
+ − 815
+ − 816
@{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
126
+ − 817
"(Const (\"HOL.zero_class.zero\", \<dots>),
122
+ − 818
Const (\"HOL.times_class.times\", \<dots>))"}
+ − 819
123
+ − 820
While you could use the complete name, for example
+ − 821
@{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
122
+ − 822
matching against @{text "Nil"}, this would make the code rather brittle.
+ − 823
The reason is that the theory and the name of the datatype can easily change.
123
+ − 824
To make the code more robust, it is better to use the antiquotation
122
+ − 825
@{text "@{const_name \<dots>}"}. With this antiquotation you can harness the
123
+ − 826
variable parts of the constant's name. Therefore a functions for
+ − 827
matching against constants that have a polymorphic type should
+ − 828
be written as follows.
122
+ − 829
*}
+ − 830
+ − 831
ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+ − 832
| is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
+ − 833
| is_nil_or_all _ = false *}
+ − 834
+ − 835
text {*
131
+ − 836
Occasional you have to calculate what the ``base'' name of a given
124
+ − 837
constant is. For this you can use the function @{ML Sign.extern_const} or
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 838
@{ML Long_Name.base_name}. For example:
124
+ − 839
+ − 840
@{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
122
+ − 841
124
+ − 842
The difference between both functions is that @{ML extern_const in Sign} returns
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 843
the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
124
+ − 844
strips off all qualifiers.
122
+ − 845
+ − 846
\begin{readmore}
162
+ − 847
Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
+ − 848
functions about signatures in @{ML_file "Pure/sign.ML"}.
122
+ − 849
\end{readmore}
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 850
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 851
Although types of terms can often be inferred, there are many
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 852
situations where you need to construct types manually, especially
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 853
when defining constants. For example the function returning a function
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 854
type is as follows:
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 855
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 856
*}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 857
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 858
ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 859
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 860
text {* This can be equally written with the combinator @{ML "-->"} as: *}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 861
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 862
ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 863
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 864
text {*
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 865
A handy function for manipulating terms is @{ML map_types}: it takes a
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 866
function and applies it to every type in a term. You can, for example,
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 867
change every @{typ nat} in a term into an @{typ int} using the function:
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 868
*}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 869
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 870
ML{*fun nat_to_int t =
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 871
(case t of
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 872
@{typ nat} => @{typ int}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 873
| Type (s, ts) => Type (s, map nat_to_int ts)
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 874
| _ => t)*}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 875
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 876
text {*
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 877
An example as follows:
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 878
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 879
@{ML_response_fake [display,gray]
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 880
"map_types nat_to_int @{term \"a = (1::nat)\"}"
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 881
"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 882
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 883
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 884
(FIXME: readmore about types)
122
+ − 885
*}
162
+ − 886
122
+ − 887
124
+ − 888
section {* Type-Checking *}
+ − 889
+ − 890
text {*
+ − 891
131
+ − 892
You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
+ − 893
typ}es, since they are just arbitrary unchecked trees. However, you
+ − 894
eventually want to see if a term is well-formed, or type-checks, relative to
+ − 895
a theory. Type-checking is done via the function @{ML cterm_of}, which
+ − 896
converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
+ − 897
term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
+ − 898
abstract objects that are guaranteed to be type-correct, and they can only
+ − 899
be constructed via ``official interfaces''.
+ − 900
124
+ − 901
+ − 902
Type-checking is always relative to a theory context. For now we use
+ − 903
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
+ − 904
For example you can write:
+ − 905
149
+ − 906
@{ML_response_fake [display,gray] "cterm_of @{theory} @{term \"(a::nat) + b = c\"}" "a + b = c"}
124
+ − 907
+ − 908
This can also be written with an antiquotation:
+ − 909
+ − 910
@{ML_response_fake [display,gray] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
+ − 911
+ − 912
Attempting to obtain the certified term for
+ − 913
+ − 914
@{ML_response_fake_both [display,gray] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+ − 915
+ − 916
yields an error (since the term is not typable). A slightly more elaborate
+ − 917
example that type-checks is:
+ − 918
+ − 919
@{ML_response_fake [display,gray]
+ − 920
"let
+ − 921
val natT = @{typ \"nat\"}
+ − 922
val zero = @{term \"0::nat\"}
+ − 923
in
+ − 924
cterm_of @{theory}
+ − 925
(Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+ − 926
end" "0 + 0"}
+ − 927
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 928
In Isabelle not just terms need to be certified, but also types. For example,
193
+ − 929
you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 930
the ML-level as follows:
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 931
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 932
@{ML_response_fake [display,gray]
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 933
"ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 934
"nat \<Rightarrow> bool"}
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 935
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 936
\begin{readmore}
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 937
For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 938
the file @{ML_file "Pure/thm.ML"}.
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 939
\end{readmore}
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 940
124
+ − 941
\begin{exercise}
+ − 942
Check that the function defined in Exercise~\ref{fun:revsum} returns a
+ − 943
result that type-checks.
+ − 944
\end{exercise}
+ − 945
193
+ − 946
Remember Isabelle follows the Church-style typing for terms, i.e.~a term contains
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 947
enough typing information (constants, free variables and abstractions all have typing
124
+ − 948
information) so that it is always clear what the type of a term is.
+ − 949
Given a well-typed term, the function @{ML type_of} returns the
+ − 950
type of a term. Consider for example:
+ − 951
+ − 952
@{ML_response [display,gray]
+ − 953
"type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+ − 954
+ − 955
To calculate the type, this function traverses the whole term and will
193
+ − 956
detect any typing inconsistency. For example changing the type of the variable
149
+ − 957
@{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message:
124
+ − 958
+ − 959
@{ML_response_fake [display,gray]
+ − 960
"type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})"
+ − 961
"*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
+ − 962
+ − 963
Since the complete traversal might sometimes be too costly and
149
+ − 964
not necessary, there is the function @{ML fastype_of}, which
+ − 965
also returns the type of a term.
124
+ − 966
+ − 967
@{ML_response [display,gray]
+ − 968
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+ − 969
177
+ − 970
However, efficiency is gained on the expense of skipping some tests. You
124
+ − 971
can see this in the following example
+ − 972
+ − 973
@{ML_response [display,gray]
+ − 974
"fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
+ − 975
149
+ − 976
where no error is detected.
124
+ − 977
+ − 978
Sometimes it is a bit inconvenient to construct a term with
+ − 979
complete typing annotations, especially in cases where the typing
+ − 980
information is redundant. A short-cut is to use the ``place-holder''
+ − 981
type @{ML "dummyT"} and then let type-inference figure out the
+ − 982
complete type. An example is as follows:
+ − 983
+ − 984
@{ML_response_fake [display,gray]
+ − 985
"let
126
+ − 986
val c = Const (@{const_name \"plus\"}, dummyT)
+ − 987
val o = @{term \"1::nat\"}
+ − 988
val v = Free (\"x\", dummyT)
124
+ − 989
in
126
+ − 990
Syntax.check_term @{context} (c $ o $ v)
124
+ − 991
end"
126
+ − 992
"Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
+ − 993
Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
124
+ − 994
+ − 995
Instead of giving explicitly the type for the constant @{text "plus"} and the free
193
+ − 996
variable @{text "x"}, the type-inference fills in the missing information.
124
+ − 997
+ − 998
\begin{readmore}
+ − 999
See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
193
+ − 1000
checking and pretty-printing of terms are defined. Functions related to the
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1001
type inference are implemented in @{ML_file "Pure/type.ML"} and
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1002
@{ML_file "Pure/type_infer.ML"}.
124
+ − 1003
\end{readmore}
162
+ − 1004
+ − 1005
(FIXME: say something about sorts)
124
+ − 1006
*}
+ − 1007
+ − 1008
2
+ − 1009
section {* Theorems *}
+ − 1010
+ − 1011
text {*
50
+ − 1012
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
122
+ − 1013
that can only be build by going through interfaces. As a consequence, every proof
124
+ − 1014
in Isabelle is correct by construction. This follows the tradition of the LCF approach
+ − 1015
\cite{GordonMilnerWadsworth79}.
107
+ − 1016
2
+ − 1017
78
+ − 1018
To see theorems in ``action'', let us give a proof on the ML-level for the following
+ − 1019
statement:
10
+ − 1020
*}
+ − 1021
+ − 1022
lemma
+ − 1023
assumes assm\<^isub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x"
+ − 1024
and assm\<^isub>2: "P t"
13
+ − 1025
shows "Q t" (*<*)oops(*>*)
10
+ − 1026
+ − 1027
text {*
185
+ − 1028
The corresponding ML-code is as follows:
10
+ − 1029
72
7b8c4fe235aa
added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1030
@{ML_response_fake [display,gray]
42
+ − 1031
"let
138
+ − 1032
val assm1 = @{cprop \"\<And>(x::nat). P x \<Longrightarrow> Q x\"}
+ − 1033
val assm2 = @{cprop \"(P::nat\<Rightarrow>bool) t\"}
10
+ − 1034
+ − 1035
val Pt_implies_Qt =
+ − 1036
assume assm1
138
+ − 1037
|> forall_elim @{cterm \"t::nat\"};
10
+ − 1038
+ − 1039
val Qt = implies_elim Pt_implies_Qt (assume assm2);
+ − 1040
in
+ − 1041
Qt
+ − 1042
|> implies_intr assm2
+ − 1043
|> implies_intr assm1
48
+ − 1044
end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
12
+ − 1045
21
+ − 1046
This code-snippet constructs the following proof:
+ − 1047
+ − 1048
\[
+ − 1049
\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
+ − 1050
{\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+ − 1051
{\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
+ − 1052
{\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+ − 1053
{\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
+ − 1054
&
+ − 1055
\infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
+ − 1056
}
+ − 1057
}
+ − 1058
}
+ − 1059
\]
+ − 1060
102
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1061
However, while we obtained a theorem as result, this theorem is not
5e309df58557
general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1062
yet stored in Isabelle's theorem database. So it cannot be referenced later
128
+ − 1063
on. How to store theorems will be explained in Section~\ref{sec:storing}.
21
+ − 1064
13
+ − 1065
\begin{readmore}
50
+ − 1066
For the functions @{text "assume"}, @{text "forall_elim"} etc
13
+ − 1067
see \isccite{sec:thms}. The basic functions for theorems are defined in
+ − 1068
@{ML_file "Pure/thm.ML"}.
+ − 1069
\end{readmore}
12
+ − 1070
194
+ − 1071
(FIXME: handy functions working on theorems; how to add case-names to goal
+ − 1072
states - maybe in the next section)
10
+ − 1073
*}
+ − 1074
123
+ − 1075
section {* Theorem Attributes *}
+ − 1076
127
+ − 1077
text {*
193
+ − 1078
Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
+ − 1079
"[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
136
+ − 1080
annotated to theorems, but functions that do further processing once a
193
+ − 1081
theorem is proved. In particular, it is not possible to find out
136
+ − 1082
what are all theorems that have a given attribute in common, unless of course
193
+ − 1083
the function behind the attribute stores the theorems in a retrievable
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1084
datastructure.
127
+ − 1085
193
+ − 1086
If you want to print out all currently known attributes a theorem can have,
+ − 1087
you can use the Isabelle command
127
+ − 1088
193
+ − 1089
\begin{isabelle}
+ − 1090
\isacommand{print\_attributes}\\
+ − 1091
@{text "> COMP: direct composition with rules (no lifting)"}\\
+ − 1092
@{text "> HOL.dest: declaration of Classical destruction rule"}\\
+ − 1093
@{text "> HOL.elim: declaration of Classical elimination rule"}\\
+ − 1094
@{text "> \<dots>"}
+ − 1095
\end{isabelle}
+ − 1096
+ − 1097
The theorem attributes fall roughly into two categories: the first category manipulates
+ − 1098
the proved theorem (like @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+ − 1099
stores the proved theorem somewhere as data (like @{text "[simp]"}, which adds
+ − 1100
the theorem to the current simpset).
127
+ − 1101
136
+ − 1102
To explain how to write your own attribute, let us start with an extremely simple
+ − 1103
version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
+ − 1104
to produce the ``symmetric'' version of an equation. The main function behind
+ − 1105
this attribute is
127
+ − 1106
*}
+ − 1107
133
+ − 1108
ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
+ − 1109
+ − 1110
text {*
136
+ − 1111
where the function @{ML "Thm.rule_attribute"} expects a function taking a
149
+ − 1112
context (which we ignore in the code above) and a theorem (@{text thm}), and
+ − 1113
returns another theorem (namely @{text thm} resolved with the lemma
+ − 1114
@{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns
156
+ − 1115
an attribute.
136
+ − 1116
+ − 1117
Before we can use the attribute, we need to set it up. This can be done
193
+ − 1118
using the Isabelle command \isacommand{attribute\_setup} as follows:
133
+ − 1119
*}
+ − 1120
193
+ − 1121
attribute_setup %gray my_sym = {* Scan.succeed my_symmetric *}
+ − 1122
"applying the sym rule"
133
+ − 1123
136
+ − 1124
text {*
193
+ − 1125
The attribute does not expect any further arguments (unlike @{text "[THEN
+ − 1126
\<dots>]"}, for example). Therefore
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1127
we use the parser @{ML Scan.succeed}. Later on we will also consider
149
+ − 1128
attributes taking further arguments. An example for the attribute @{text
+ − 1129
"[my_sym]"} is the proof
136
+ − 1130
*}
+ − 1131
+ − 1132
lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
133
+ − 1133
+ − 1134
text {*
193
+ − 1135
which stores the theorem @{thm test} under the name @{thm [source] test}. You
+ − 1136
can see this, if you query the lemma:
+ − 1137
+ − 1138
\begin{isabelle}
+ − 1139
\isacommand{thm}~@{text "test"}\\
+ − 1140
@{text "> "}~@{thm test}
+ − 1141
\end{isabelle}
+ − 1142
+ − 1143
We can also use the attribute when referring to this theorem:
136
+ − 1144
+ − 1145
\begin{isabelle}
+ − 1146
\isacommand{thm}~@{text "test[my_sym]"}\\
+ − 1147
@{text "> "}~@{thm test[my_sym]}
+ − 1148
\end{isabelle}
+ − 1149
193
+ − 1150
As an example of a slightly more complicated theorem attribute, we implement
194
+ − 1151
our version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
+ − 1152
as argument and resolve the proved theorem with this list (one theorem
+ − 1153
after another). The code for this attribute is
193
+ − 1154
*}
+ − 1155
+ − 1156
ML{*fun MY_THEN thms =
+ − 1157
Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
+ − 1158
+ − 1159
text {*
194
+ − 1160
where @{ML swap} swaps the components of a pair (@{ML RS} is explained
+ − 1161
later on in Section~\ref{sec:simpletacs}). The setup of this theorem
193
+ − 1162
attribute uses the parser @{ML Attrib.thms}, which parses a list of
+ − 1163
theorems.
+ − 1164
*}
+ − 1165
+ − 1166
attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
+ − 1167
"resolving the list of theorems with the proved theorem"
+ − 1168
+ − 1169
text {*
+ − 1170
You can, for example, use this theorem attribute to turn an equation into a
+ − 1171
meta-equation:
+ − 1172
+ − 1173
\begin{isabelle}
+ − 1174
\isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\
+ − 1175
@{text "> "}~@{thm test[MY_THEN eq_reflection]}
+ − 1176
\end{isabelle}
+ − 1177
+ − 1178
If you need the symmetric version as a meta-equation, you can write
+ − 1179
+ − 1180
\begin{isabelle}
+ − 1181
\isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
+ − 1182
@{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
+ − 1183
\end{isabelle}
+ − 1184
194
+ − 1185
It is also possible to combine different theorem attributes, as in:
193
+ − 1186
+ − 1187
\begin{isabelle}
+ − 1188
\isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
+ − 1189
@{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
+ − 1190
\end{isabelle}
+ − 1191
+ − 1192
However, here also a weakness of the concept
194
+ − 1193
of theorem attributes shows through: since theorem attributes can be
193
+ − 1194
arbitrary functions, they do not in general commute. If you try
+ − 1195
+ − 1196
\begin{isabelle}
+ − 1197
\isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
+ − 1198
@{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
+ − 1199
\end{isabelle}
+ − 1200
+ − 1201
you get an exception indicating that the theorem @{thm [source] sym}
+ − 1202
does not resolve with meta-equations.
+ − 1203
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1204
The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
194
+ − 1205
Another usage of theorem attributes is to add and delete theorems from stored data.
+ − 1206
For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1207
current simpset. For these applications, you can use @{ML Thm.declaration_attribute}.
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1208
To illustrate this function, let us introduce a reference containing a list
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1209
of theorems.
133
+ − 1210
*}
+ − 1211
193
+ − 1212
ML{*val my_thms = ref ([] : thm list)*}
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1213
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1214
text {*
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1215
A word of warning: such references must not be used in any code that
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1216
is meant to be more than just for testing purposes! Here it is only used
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1217
to illustrate matters. We will show later how to store data properly without
193
+ − 1218
using references.
+ − 1219
+ − 1220
The function @{ML Thm.declaration_attribute} expects us to
153
+ − 1221
provide two functions that add and delete theorems from this list.
+ − 1222
For this we use the two functions:
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1223
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1224
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1225
ML{*fun my_thms_add thm ctxt =
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1226
(my_thms := Thm.add_thm thm (!my_thms); ctxt)
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1227
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1228
fun my_thms_del thm ctxt =
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1229
(my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1230
133
+ − 1231
text {*
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1232
These functions take a theorem and a context and, for what we are explaining
156
+ − 1233
here it is sufficient that they just return the context unchanged. They change
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1234
however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1235
adds a theorem if it is not already included in the list, and @{ML
194
+ − 1236
Thm.del_thm} deletes one (both functions use the predicate @{ML
+ − 1237
Thm.eq_thm_prop}, which compares theorems according to their proved
+ − 1238
propositions modulo alpha-equivalence).
133
+ − 1239
+ − 1240
194
+ − 1241
You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into
+ − 1242
attributes with the code
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1243
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1244
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1245
ML{*val my_add = Thm.declaration_attribute my_thms_add
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1246
val my_del = Thm.declaration_attribute my_thms_del *}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1247
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1248
text {*
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1249
and set up the attributes as follows
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1250
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1251
193
+ − 1252
attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
+ − 1253
"maintaining a list of my_thms"
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1254
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1255
text {*
194
+ − 1256
The parser @{ML Attrib.add_del} is a predefined parser for
+ − 1257
adding and deleting lemmas. Now if you prove the next lemma
+ − 1258
and attach the attribute
+ − 1259
@{text "[my_thms]"}
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1260
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1261
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1262
lemma trueI_2[my_thms]: "True" by simp
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1263
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1264
text {*
194
+ − 1265
then you can see it is added to the initially empty list.
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1266
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1267
@{ML_response_fake [display,gray]
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1268
"!my_thms" "[\"True\"]"}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1269
160
cc9359bfacf4
redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1270
You can also add theorems using the command \isacommand{declare}.
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1271
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1272
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1273
declare test[my_thms] trueI_2[my_thms add]
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1274
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1275
text {*
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1276
The @{text "add"} is the default operation and does not need
194
+ − 1277
to be explicitly given. These two declarations will cause the
+ − 1278
theorem list to be updated as:
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1279
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1280
@{ML_response_fake [display,gray]
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1281
"!my_thms"
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1282
"[\"True\", \"Suc (Suc 0) = 2\"]"}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1283
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1284
The theorem @{thm [source] trueI_2} only appears once, since the
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1285
function @{ML Thm.add_thm} tests for duplicates, before extending
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1286
the list. Deletion from the list works as follows:
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1287
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1288
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1289
declare test[my_thms del]
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1290
156
+ − 1291
text {* After this, the theorem list is again:
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1292
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1293
@{ML_response_fake [display,gray]
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1294
"!my_thms"
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1295
"[\"True\"]"}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1296
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1297
We used in this example two functions declared as @{ML Thm.declaration_attribute},
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1298
but there can be any number of them. We just have to change the parser for reading
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1299
the arguments accordingly.
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1300
156
+ − 1301
However, as said at the beginning of this example, using references for storing theorems is
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1302
\emph{not} the received way of doing such things. The received way is to
194
+ − 1303
start a ``data slot'', below called @{text MyThmsData}, by using the functor
+ − 1304
@{text GenericDataFun}:
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1305
*}
133
+ − 1306
193
+ − 1307
ML {*structure MyThmsData = GenericDataFun
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1308
(type T = thm list
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1309
val empty = []
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1310
val extend = I
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1311
fun merge _ = Thm.merge_thms) *}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1312
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1313
text {*
156
+ − 1314
To use this data slot, you only have to change @{ML my_thms_add} and
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1315
@{ML my_thms_del} to:
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1316
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1317
193
+ − 1318
ML{*val thm_add = MyThmsData.map o Thm.add_thm
+ − 1319
val thm_del = MyThmsData.map o Thm.del_thm*}
+ − 1320
+ − 1321
text {*
194
+ − 1322
where @{ML MyThmsData.map} updates the data appropriately. The
+ − 1323
corresponding theorem addtributes are
193
+ − 1324
*}
+ − 1325
+ − 1326
ML{*val add = Thm.declaration_attribute thm_add
+ − 1327
val del = Thm.declaration_attribute thm_del *}
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1328
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1329
text {*
194
+ − 1330
and the setup is as follows
193
+ − 1331
*}
+ − 1332
+ − 1333
attribute_setup %gray my_thms2 = {* Attrib.add_del add del *}
+ − 1334
"properly maintaining a list of my_thms"
+ − 1335
194
+ − 1336
text {*
+ − 1337
Initially, the data slot is empty
193
+ − 1338
194
+ − 1339
@{ML_response_fake [display,gray]
+ − 1340
"MyThmsData.get (Context.Proof @{context})"
+ − 1341
"[]"}
193
+ − 1342
194
+ − 1343
but if you prove
+ − 1344
*}
+ − 1345
+ − 1346
lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
193
+ − 1347
+ − 1348
text {*
194
+ − 1349
the lemma is now included
+ − 1350
+ − 1351
@{ML_response_fake [display,gray]
+ − 1352
"MyThmsData.get (Context.Proof @{context})"
+ − 1353
"[\"3 = Suc (Suc (Suc 0))\"]"}
+ − 1354
+ − 1355
With @{text my_thms2} you can also nicely see why it is important to
+ − 1356
store data in a ``data slot'' and \emph{not} in a reference. Backtrack
+ − 1357
to the point just before the lemma @{thm [source] three} is proved and
+ − 1358
check the the content of @{ML_struct "MyThmsData"}: it is now again
+ − 1359
empty. The addition has been properly retracted. Now consider the proof:
+ − 1360
*}
+ − 1361
+ − 1362
lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
193
+ − 1363
194
+ − 1364
text {*
+ − 1365
Checking the content of @{ML my_thms} gives
+ − 1366
+ − 1367
@{ML_response_fake [display,gray]
+ − 1368
"!my_thms"
+ − 1369
"[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
+ − 1370
+ − 1371
as expected, but if we backtrack before the lemma @{thm [source] four}, the
+ − 1372
content of @{ML my_thms} is unchanged. The backtracking mechanism
+ − 1373
of Isabelle is completely oblivious about what to do with references!
+ − 1374
+ − 1375
Since storing theorems in a special list is such a common task, there is the
+ − 1376
functor @{text NamedThmsFun}, which does most of the work for you. To obtain
+ − 1377
such a named theorem lists, you just declare
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1378
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1379
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1380
ML{*structure FooRules = NamedThmsFun
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1381
(val name = "foo"
194
+ − 1382
val description = "Rules for foo") *}
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1383
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1384
text {*
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1385
and set up the @{ML_struct FooRules} with the command
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1386
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1387
177
+ − 1388
setup %gray {* FooRules.setup *}
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1389
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1390
text {*
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1391
This code declares a data slot where the theorems are stored,
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1392
an attribute @{text foo} (with the @{text add} and @{text del} options
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1393
for adding and deleting theorems) and an internal ML interface to retrieve and
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1394
modify the theorems.
133
+ − 1395
157
+ − 1396
Furthermore, the facts are made available on the user-level under the dynamic
156
+ − 1397
fact name @{text foo}. For example you can declare three lemmas to be of the kind
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1398
@{text foo} by:
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1399
*}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1400
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1401
lemma rule1[foo]: "A" sorry
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1402
lemma rule2[foo]: "B" sorry
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1403
lemma rule3[foo]: "C" sorry
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1404
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1405
text {* and undeclare the first one by: *}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1406
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1407
declare rule1[foo del]
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1408
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1409
text {* and query the remaining ones with:
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1410
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1411
\begin{isabelle}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1412
\isacommand{thm}~@{text "foo"}\\
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1413
@{text "> ?C"}\\
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1414
@{text "> ?B"}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1415
\end{isabelle}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1416
156
+ − 1417
On the ML-level the rules marked with @{text "foo"} can be retrieved
151
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1418
using the function @{ML FooRules.get}:
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1419
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1420
@{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1421
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1422
\begin{readmore}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1423
For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1424
the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1425
data.
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1426
\end{readmore}
7e0bf13bf743
added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1427
156
+ − 1428
(FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
133
+ − 1429
+ − 1430
+ − 1431
\begin{readmore}
+ − 1432
FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
+ − 1433
\end{readmore}
+ − 1434
*}
+ − 1435
127
+ − 1436
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1437
section {* Setups (TBD) *}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1438
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1439
text {*
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1440
In the previous section we used \isacommand{setup} in order to make
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1441
a theorem attribute known to Isabelle. What happens behind the scenes
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1442
is that \isacommand{setup} expects a functions of type
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1443
@{ML_type "theory -> theory"}: the input theory is the current theory and the
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1444
output the theory where the theory attribute has been stored.
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1445
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1446
This is a fundamental principle in Isabelle. A similar situation occurs
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1447
for example with declaring constants. The function that declares a
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1448
constant on the ML-level is @{ML Sign.add_consts_i}.
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1449
If you write\footnote{Recall that ML-code needs to be
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1450
enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1451
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1452
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1453
ML{*Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] @{theory} *}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1454
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1455
text {*
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1456
for declaring the constant @{text "BAR"} with type @{typ nat} and
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1457
run the code, then you indeed obtain a theory as result. But if you
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1458
query the constant on the Isabelle level using the command \isacommand{term}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1459
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1460
\begin{isabelle}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1461
\isacommand{term}~@{text [quotes] "BAR"}\\
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1462
@{text "> \"BAR\" :: \"'a\""}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1463
\end{isabelle}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1464
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1465
you do not obtain a constant of type @{typ nat}, but a free variable (printed in
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1466
blue) of polymorphic type. The problem is that the ML-expression above did
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1467
not register the declaration with the current theory. This is what the command
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1468
\isacommand{setup} is for. The constant is properly declared with
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1469
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1470
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1471
setup %gray {* Sign.add_consts_i [(@{binding "BAR"}, @{typ "nat"}, NoSyn)] *}
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1472
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1473
text {*
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1474
Now
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1475
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1476
\begin{isabelle}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1477
\isacommand{term}~@{text [quotes] "BAR"}\\
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1478
@{text "> \"BAR\" :: \"nat\""}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1479
\end{isabelle}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1480
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1481
returns a (black) constant with the type @{typ nat}.
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1482
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1483
A similar command is \isacommand{local\_setup}, which expects a function
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1484
of type @{ML_type "local_theory -> local_theory"}. Later on we will also
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1485
use the commands \isacommand{method\_setup} for installing methods in the
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1486
current theory and \isacommand{simproc\_setup} for adding new simprocs to
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1487
the current simpset.
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1488
*}
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1489
153
+ − 1490
section {* Theories, Contexts and Local Theories (TBD) *}
123
+ − 1491
126
+ − 1492
text {*
+ − 1493
There are theories, proof contexts and local theories (in this order, if you
+ − 1494
want to order them).
+ − 1495
+ − 1496
In contrast to an ordinary theory, which simply consists of a type
+ − 1497
signature, as well as tables for constants, axioms and theorems, a local
+ − 1498
theory also contains additional context information, such as locally fixed
+ − 1499
variables and local assumptions that may be used by the package. The type
+ − 1500
@{ML_type local_theory} is identical to the type of \emph{proof contexts}
+ − 1501
@{ML_type "Proof.context"}, although not every proof context constitutes a
+ − 1502
valid local theory.
178
fb8f22dd8ad0
adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1503
*}
126
+ − 1504
153
+ − 1505
section {* Storing Theorems\label{sec:storing} (TBD) *}
123
+ − 1506
+ − 1507
text {* @{ML PureThy.add_thms_dynamic} *}
+ − 1508
100
+ − 1509
75
+ − 1510
126
+ − 1511
(* FIXME: some code below *)
89
+ − 1512
+ − 1513
(*<*)
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1514
(*
89
+ − 1515
setup {*
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1516
Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)]
89
+ − 1517
*}
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1518
*)
89
+ − 1519
lemma "bar = (1::nat)"
+ − 1520
oops
+ − 1521
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1522
(*
89
+ − 1523
setup {*
+ − 1524
Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)]
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1525
#> PureThy.add_defs false [((@{binding "foo_def"},
89
+ − 1526
Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])]
+ − 1527
#> snd
+ − 1528
*}
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1529
*)
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1530
(*
89
+ − 1531
lemma "foo = (1::nat)"
+ − 1532
apply(simp add: foo_def)
+ − 1533
done
+ − 1534
+ − 1535
thm foo_def
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1536
*)
89
+ − 1537
(*>*)
+ − 1538
153
+ − 1539
section {* Pretty-Printing (TBD) *}
+ − 1540
+ − 1541
text {*
163
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1542
@{ML Pretty.big_list},
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1543
@{ML Pretty.brk},
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1544
@{ML Pretty.block},
2319cff107f0
removed rep_ss, and used dest_ss instead; some very slight changes to simple_inductive
Christian Urban <urbanc@in.tum.de>
diff
changeset
+ − 1545
@{ML Pretty.chunks}
153
+ − 1546
*}
+ − 1547
+ − 1548
section {* Misc (TBD) *}
92
+ − 1549
+ − 1550
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
+ − 1551
2
+ − 1552
end