12 theory. If you want to follow the code written in this chapter, we |
12 theory. If you want to follow the code written in this chapter, we |
13 assume you are working inside the theory defined by |
13 assume you are working inside the theory defined by |
14 |
14 |
15 \begin{center} |
15 \begin{center} |
16 \begin{tabular}{@ {}l} |
16 \begin{tabular}{@ {}l} |
17 \isacommand{theory} CookBook\\ |
17 \isacommand{theory} FirstSteps\\ |
18 \isacommand{imports} Main\\ |
18 \isacommand{imports} Main\\ |
19 \isacommand{begin}\\ |
19 \isacommand{begin}\\ |
20 \ldots |
20 \ldots |
21 \end{tabular} |
21 \end{tabular} |
22 \end{center} |
22 \end{center} |
24 |
24 |
25 section {* Including ML-Code *} |
25 section {* Including ML-Code *} |
26 |
26 |
27 text {* |
27 text {* |
28 The easiest and quickest way to include code in a theory is |
28 The easiest and quickest way to include code in a theory is |
29 by using the \isacommand{ML} command. For example |
29 by using the \isacommand{ML} command. For example\smallskip |
30 *} |
30 |
31 |
31 \isacommand{ML} |
32 ML {* |
32 @{ML_text "{"}@{ML_text "*"}\isanewline |
33 3 + 4 |
33 \hspace{5mm}@{ML "3 + 4"}\isanewline |
34 *} |
34 @{ML_text "*"}@{ML_text "}"}\isanewline |
35 |
35 @{ML_text "> 7"}\smallskip |
36 text {* |
36 |
37 Expressions inside \isacommand{ML} commands are immediately evaluated, |
37 Expressions inside \isacommand{ML} commands are immediately evaluated, |
38 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of |
38 like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of |
39 your Isabelle environment. The code inside the \isacommand{ML} command |
39 your Isabelle environment. The code inside the \isacommand{ML} command |
40 can also contain value and function bindings. However on such \isacommand{ML} |
40 can also contain value and function bindings. However on such \isacommand{ML} |
41 commands the undo operation behaves slightly counter-intuitive, because |
41 commands the undo operation behaves slightly counter-intuitive, because |
42 if you define |
42 if you define\smallskip |
43 *} |
43 |
44 |
44 \isacommand{ML} |
45 ML {* |
45 @{ML_text "{"}@{ML_text "*"}\isanewline |
46 val foo = true |
46 @{ML_text "val foo = true"}\isanewline |
47 *} |
47 @{ML_text "*"}@{ML_text "}"}\isanewline |
48 |
48 @{ML_text "> true"}\smallskip |
49 text {* |
49 |
50 then Isabelle's undo operation has no effect on the definition of |
50 then Isabelle's undo operation has no effect on the definition of |
51 @{ML "foo"}. |
51 @{ML_text "foo"}. Note that from now on we will drop the |
|
52 \isacommand{ML} @{ML_text "{"}@{ML_text "* \<dots> *"}@{ML_text "}"} whenever |
|
53 we show code. |
52 |
54 |
53 Once a portion of code is relatively stable, one usually wants to |
55 Once a portion of code is relatively stable, one usually wants to |
54 export it to a separate ML-file. Such files can then be included in a |
56 export it to a separate ML-file. Such files can then be included in a |
55 theory by using \isacommand{uses} in the header of the theory, like |
57 theory by using \isacommand{uses} in the header of the theory, like |
56 |
58 |
61 \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
63 \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\ |
62 \isacommand{begin}\\ |
64 \isacommand{begin}\\ |
63 \ldots |
65 \ldots |
64 \end{tabular} |
66 \end{tabular} |
65 \end{center} |
67 \end{center} |
|
68 |
|
69 Note that from now on we are going to drop the the |
|
70 |
66 *} |
71 *} |
67 |
72 |
68 section {* Debugging and Printing *} |
73 section {* Debugging and Printing *} |
69 |
74 |
70 text {* |
75 text {* |
71 |
76 |
72 During developments you might find it necessary to quickly inspect some data |
77 During developments you might find it necessary to quickly inspect some data |
73 in your code. This can be done in a ``quick-and-dirty'' fashion using |
78 in your code. This can be done in a ``quick-and-dirty'' fashion using |
74 the function @{ML "warning"}. For example |
79 the function @{ML "warning"}. For example |
75 *} |
80 |
76 |
81 @{ML [display] "warning \"any string\""} |
77 ML {* warning "any string" *} |
82 |
78 |
83 will print out @{ML_text "\"any string\""} inside the response buffer of Isabelle. |
79 text {* |
|
80 will print out @{ML "\"any string\""} inside the response buffer of Isabelle. |
|
81 If you develop under PolyML, then there is a convenient, though again |
84 If you develop under PolyML, then there is a convenient, though again |
82 ``quick-and-dirty'', method for converting values into strings, |
85 ``quick-and-dirty'', method for converting values into strings, |
83 for example: |
86 for example: |
84 *} |
87 |
85 |
88 @{ML [display] "warning (makestring 1)"} |
86 ML {* warning (makestring 1) *} |
89 |
87 |
|
88 text {* |
|
89 However this only works if the type of what is converted is monomorphic and not |
90 However this only works if the type of what is converted is monomorphic and not |
90 a function. |
91 a function. |
91 *} |
92 |
92 |
93 The funtion warning should only be used for testing purposes, because any |
93 text {* |
94 output this funtion generates will be overwritten, as soon as an error is |
94 The funtion warning should only be used for testing purposes, because |
95 raised. Therefore for printing anything more serious and elaborate, the |
95 any output this funtion generates will be overwritten, as soon as an error |
96 function @{ML tracing} should be used. This function writes all output into |
96 is raised. |
97 a separate buffer. |
97 Therefore for printing anything more serious and elaborate, the function @{ML tracing} |
98 |
98 should be used. This function writes all output into a separate buffer. |
99 @{ML [display] "tracing \"foo\""} |
99 *} |
|
100 |
|
101 ML {* tracing "foo" *} |
|
102 |
|
103 text {* |
|
104 |
100 |
105 It is also possible to redirect the channel where the @{ML_text "foo"} is |
101 It is also possible to redirect the channel where the @{ML_text "foo"} is |
106 printed to a separate file, e.g. to prevent Proof General from choking on massive |
102 printed to a separate file, e.g. to prevent Proof General from choking on massive |
107 amounts of trace output. This rediretion can be achieved using the code |
103 amounts of trace output. This rediretion can be achieved using the code |
108 |
|
109 *} |
104 *} |
110 |
105 |
111 ML {* |
106 ML {* |
112 val strip_specials = |
107 val strip_specials = |
113 let |
108 let |
136 The main advantage of embedding all code |
131 The main advantage of embedding all code |
137 in a theory is that the code can contain references to entities defined |
132 in a theory is that the code can contain references to entities defined |
138 on the logical level of Isabelle. This is done using antiquotations. |
133 on the logical level of Isabelle. This is done using antiquotations. |
139 For example, one can print out the name of |
134 For example, one can print out the name of |
140 the current theory by typing |
135 the current theory by typing |
141 *} |
136 |
142 |
137 @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps : string"} |
143 ML {* Context.theory_name @{theory} *} |
138 |
144 |
|
145 text {* |
|
146 where @{text "@{theory}"} is an antiquotation that is substituted with the |
139 where @{text "@{theory}"} is an antiquotation that is substituted with the |
147 current theory (remember that we assumed we are inside the theory CookBook). |
140 current theory (remember that we assumed we are inside the theory CookBook). |
148 The name of this theory can be extracted using the function @{ML "Context.theory_name"}. |
141 The name of this theory can be extracted using the function |
149 So the code above returns the string @{ML "\"CookBook\""}. |
142 @{ML "Context.theory_name"}. |
150 |
143 |
151 Note, however, that antiquotations are statically scoped, that is the value is |
144 Note, however, that antiquotations are statically scoped, that is the value is |
152 determined at ``compile-time'', not ``run-time''. For example the function |
145 determined at ``compile-time'', not ``run-time''. For example the function |
153 |
146 |
154 *} |
147 *} |
158 *} |
151 *} |
159 |
152 |
160 text {* |
153 text {* |
161 does \emph{not} return the name of the current theory, if it is run in a |
154 does \emph{not} return the name of the current theory, if it is run in a |
162 different theory. Instead, the code above defines the constant function |
155 different theory. Instead, the code above defines the constant function |
163 that always returns the string @{ML "\"CookBook\""}, no matter where the |
156 that always returns the string @{ML_text "FirstSteps"}, no matter where the |
164 function is called. Operationally speaking, @{text "@{theory}"} is |
157 function is called. Operationally speaking, @{text "@{theory}"} is |
165 \emph{not} replaced with code that will look up the current theory in |
158 \emph{not} replaced with code that will look up the current theory in |
166 some data structure and return it. Instead, it is literally |
159 some data structure and return it. Instead, it is literally |
167 replaced with the value representing the theory name. |
160 replaced with the value representing the theory name. |
168 |
161 |
169 In a similar way you can use antiquotations to refer to theorems or simpsets: |
162 In a similar way you can use antiquotations to refer to theorems or simpsets: |
170 *} |
163 |
171 |
164 |
172 ML {* @{thm allI} *} |
165 @{ML [display] "@{thm allI}"} |
173 ML {* @{simpset} *} |
166 @{ML [display] "@{simpset}"} |
174 |
167 |
175 text {* |
|
176 In the course of this introduction, we will learn more about |
168 In the course of this introduction, we will learn more about |
177 these antiquotations: they greatly simplify Isabelle programming since one |
169 these antiquotations: they greatly simplify Isabelle programming since one |
178 can directly access all kinds of logical elements from ML. |
170 can directly access all kinds of logical elements from ML. |
179 |
171 |
180 *} |
172 *} |
182 section {* Terms and Types *} |
174 section {* Terms and Types *} |
183 |
175 |
184 text {* |
176 text {* |
185 One way to construct terms of Isabelle on the ML level is by using the antiquotation |
177 One way to construct terms of Isabelle on the ML level is by using the antiquotation |
186 \mbox{@{text "@{term \<dots>}"}}: |
178 \mbox{@{text "@{term \<dots>}"}}: |
187 *} |
179 |
188 |
180 @{ML_response [display] "@{term \"(a::nat) + b = c\"}" |
189 ML {* @{term "(a::nat) + b = c"} *} |
181 "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"} |
190 |
182 |
191 text {* |
|
192 This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal |
183 This will show the term @{term "(a::nat) + b = c"}, but printed out using the internal |
193 representation of this term. This internal representation corresponds to the |
184 representation of this term. This internal representation corresponds to the |
194 datatype @{ML_text "term"}. |
185 datatype @{ML_type "term"}. |
195 |
186 |
196 The internal representation of terms uses the usual de Bruijn index mechanism where bound |
187 The internal representation of terms uses the usual de Bruijn index mechanism where bound |
197 variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to |
188 variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to |
198 the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that |
189 the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that |
199 binds the corresponding variable. However, in Isabelle the names of bound variables are |
190 binds the corresponding variable. However, in Isabelle the names of bound variables are |
223 Hint: The third term is already quite big, and the pretty printer |
214 Hint: The third term is already quite big, and the pretty printer |
224 may omit parts of it by default. If you want to see all of it, you |
215 may omit parts of it by default. If you want to see all of it, you |
225 can use the following ML funtion to set the limit to a value high |
216 can use the following ML funtion to set the limit to a value high |
226 enough: |
217 enough: |
227 \end{exercise} |
218 \end{exercise} |
228 *} |
219 |
229 ML {* print_depth 50 *} |
220 @{ML [display] "print_depth 50"} |
230 |
221 |
231 text {* |
|
232 |
|
233 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, |
222 The antiquotation @{text "@{prop \<dots>}"} constructs terms of propositional type, |
234 inserting the invisible @{text "Trueprop"} coercions whenever necessary. |
223 inserting the invisible @{text "Trueprop"} coercions whenever necessary. |
235 Consider for example |
224 Consider for example |
236 |
225 |
237 *} |
226 @{ML_response [display] "@{term \"P x\"}" "Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)"} |
238 |
227 @{ML_response [display] "@{prop \"P x\"}" |
239 ML {* @{term "P x"} ; @{prop "P x"} *} |
228 "Const (\"Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>))"} |
240 |
229 |
241 text {* which inserts the coercion in the latter case and *} |
230 which inserts the coercion in the latter case and |
242 |
231 |
243 |
232 @{ML_response [display] "@{term \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"} |
244 ML {* @{term "P x \<Longrightarrow> Q x"} ; @{prop "P x \<Longrightarrow> Q x"} *} |
233 @{ML_response [display] "@{prop \"P x \<Longrightarrow> Q x\"}" "Const (\"==>\", \<dots>) $ \<dots> $ \<dots>"} |
245 |
234 |
246 text {* |
|
247 which does not. |
235 which does not. |
248 |
236 |
249 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example |
237 Types can be constructed using the antiquotation @{text "@{typ \<dots>}"}. For example |
250 |
238 |
251 *} |
239 *} |
252 |
240 |
253 ML {* @{typ "bool \<Rightarrow> nat"} *} |
241 |
254 |
242 text {* |
255 text {* |
243 |
|
244 @{ML_response [display] "@{typ \"bool \<Rightarrow> nat\"}" "Type \<dots>"} |
|
245 |
256 (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the |
246 (FIXME: Unlike the term antiquotation, @{text "@{typ \<dots>}"} does not print the |
257 internal representation. Is there a reason for this, that needs to be explained |
247 internal representation. Is there a reason for this, that needs to be explained |
258 here?) |
248 here?) |
259 |
249 |
260 \begin{readmore} |
250 \begin{readmore} |
261 Types are described in detail in \isccite{sec:types}. Their |
251 Types are described in detail in \isccite{sec:types}. Their |
262 definition and many useful operations can be found in @{ML_file "Pure/type.ML"}. |
252 definition and many useful operations can be found in @{ML_file "Pure/type.ML"}. |
263 \end{readmore} |
253 \end{readmore} |
264 |
254 |
265 *} |
255 *} |
266 |
|
267 |
|
268 |
256 |
269 |
257 |
270 section {* Constructing Terms and Types Manually *} |
258 section {* Constructing Terms and Types Manually *} |
271 |
259 |
272 text {* |
260 text {* |
367 interfaces. |
355 interfaces. |
368 |
356 |
369 Type checking is always relative to a theory context. For now we can use |
357 Type checking is always relative to a theory context. For now we can use |
370 the @{ML "@{theory}"} antiquotation to get hold of the current theory. |
358 the @{ML "@{theory}"} antiquotation to get hold of the current theory. |
371 For example we can write: |
359 For example we can write: |
372 *} |
360 |
373 |
361 (FIXME ML-response-unchecked needed) |
374 ML {* cterm_of @{theory} @{term "(a::nat) + b = c"} *} |
362 |
375 |
363 @{ML [display] "@{term \"(a::nat) + b = c\"}"} |
376 text {* and *} |
364 |
377 |
365 and |
378 ML {* |
366 |
379 let |
367 @{ML [display] |
380 val natT = @{typ "nat"} |
368 "let |
381 val zero = @{term "0::nat"} |
369 val natT = @{typ \"nat\"} |
382 in |
370 val zero = @{term \"0::nat\"} |
383 cterm_of @{theory} |
371 in |
384 (Const (@{const_name plus}, natT --> natT --> natT) |
372 cterm_of @{theory} |
385 $ zero $ zero) |
373 (Const (@{const_name plus}, natT --> natT --> natT) |
386 end |
374 $ zero $ zero) |
387 *} |
375 end"} |
388 |
376 |
389 text {* |
|
390 |
|
391 \begin{exercise} |
377 \begin{exercise} |
392 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
378 Check that the function defined in Exercise~\ref{fun:revsum} returns a |
393 result that type checks. |
379 result that type checks. |
394 \end{exercise} |
380 \end{exercise} |
395 |
381 |
572 |
558 |
573 section {* Storing Theorems *} |
559 section {* Storing Theorems *} |
574 |
560 |
575 section {* Theorem Attributes *} |
561 section {* Theorem Attributes *} |
576 |
562 |
|
563 ML {* |
|
564 val str_of_source = space_implode " " o map OuterLex.unparse o #2 o #1 o Args.dest_src; |
|
565 |
|
566 fun ml_val ys txt = "fn " ^ |
|
567 (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ |
|
568 " => (" ^ txt ^ ");"; |
|
569 |
|
570 fun ml_val_open (ys, []) txt = ml_val ys txt |
|
571 | ml_val_open (ys, xs) txt = |
|
572 ml_val ys ("let open " ^ space_implode " " xs ^ " in " ^ txt ^ " end"); |
|
573 |
|
574 fun ml_pat (rhs, pat) = |
|
575 let val pat' = implode (map (fn "\\<dots>" => "_" | s => s) |
|
576 (Symbol.explode pat)) |
|
577 in |
|
578 "val " ^ pat' ^ " = " ^ rhs |
|
579 end; |
|
580 |
|
581 (* modified from original *) |
|
582 fun ml_val txt = "fn _ => (" ^ txt ^ ");"; |
|
583 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"; |
|
584 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;"; |
|
585 |
|
586 *} |
|
587 |
|
588 ML {* ml_pat *} |
|
589 ML {* K ml_pat *} |
|
590 |
|
591 ML {* |
|
592 fun output_verbatim ml src ctxt (txt, pos) = |
|
593 let val txt = ml ctxt (txt, pos) |
|
594 in |
|
595 (if ! ThyOutput.source then str_of_source src else txt) |
|
596 |> (if ! ThyOutput.quotes then quote else I) |
|
597 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt |
|
598 end; |
|
599 *} |
|
600 |
|
601 ML {* |
|
602 fun output_ml ml = output_verbatim |
|
603 (fn ctxt => fn ((txt, p), pos) => |
|
604 (ML_Context.eval_in (SOME ctxt) false pos (ml p txt); |
|
605 txt |> Source.of_string |> ML_Lex.source |> Source.exhaust |> |
|
606 Chunks.transform_cmts |> implode)); |
|
607 *} |
|
608 |
|
609 ML {* |
|
610 fun output_ml_checked ml src ctxt (txt, pos) = |
|
611 (ML_Context.eval_in (SOME ctxt) false pos (ml txt); |
|
612 (if ! ThyOutput.source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos))) |
|
613 |> (if ! ThyOutput.quotes then quote else I) |
|
614 |> ThyOutput.output (fn _ => fn s => Pretty.str s) src ctxt) |
|
615 |
|
616 *} |
|
617 |
|
618 |
577 |
619 |
578 end |
620 end |