6 chapter {* First Steps *} |
6 chapter {* First Steps *} |
7 |
7 |
8 text {* |
8 text {* |
9 |
9 |
10 Isabelle programming is done in Standard ML. |
10 Isabelle programming is done in Standard ML. |
11 Just like lemmas and proofs, code in Isabelle is part of a |
11 Just like lemmas and proofs, SML-code in Isabelle is part of a |
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} |
86 ``quick-and-dirty'', method for converting values into strings, |
83 ``quick-and-dirty'', method for converting values into strings, |
87 for example: |
84 for example: |
88 |
85 |
89 @{ML [display] "warning (makestring 1)"} |
86 @{ML [display] "warning (makestring 1)"} |
90 |
87 |
91 However this only works if the type of what is converted is monomorphic and not |
88 However this only works if the type of what is converted is monomorphic and is not |
92 a function. |
89 a function. |
93 |
90 |
94 The funtion warning should only be used for testing purposes, because any |
91 The funtion @{ML "warning"} should only be used for testing purposes, because any |
95 output this funtion generates will be overwritten, as soon as an error is |
92 output this funtion generates will be overwritten, as soon as an error is |
96 raised. Therefore for printing anything more serious and elaborate, the |
93 raised. Therefore for printing anything more serious and elaborate, the |
97 function @{ML tracing} should be used. This function writes all output into |
94 function @{ML tracing} should be used. This function writes all output into |
98 a separate buffer. |
95 a separate tracing buffer. |
99 |
96 |
100 @{ML [display] "tracing \"foo\""} |
97 @{ML [display] "tracing \"foo\""} |
101 |
98 |
102 It is also possible to redirect the channel where the @{ML_text "foo"} is |
99 It is also possible to redirect the channel where the @{ML_text "foo"} is |
103 printed to a separate file, e.g. to prevent Proof General from choking on massive |
100 printed to a separate file, e.g. to prevent Proof General from choking on massive |
104 amounts of trace output. This rediretion can be achieved using the code |
101 amounts of trace output. This rediretion can be achieved using the code |
105 |
102 *} |
106 @{ML_decl [display] |
103 |
107 "val strip_specials = |
104 ML {* |
|
105 val strip_specials = |
108 let |
106 let |
109 fun strip (\"\\^A\" :: _ :: cs) = strip cs |
107 fun strip ("\^A" :: _ :: cs) = strip cs |
110 | strip (c :: cs) = c :: strip cs |
108 | strip (c :: cs) = c :: strip cs |
111 | strip [] = []; |
109 | strip [] = []; |
112 in implode o strip o explode end; |
110 in implode o strip o explode end; |
113 |
111 |
114 fun redirect_tracing stream = |
112 fun redirect_tracing stream = |
115 Output.tracing_fn := (fn s => |
113 Output.tracing_fn := (fn s => |
116 (TextIO.output (stream, (strip_specials s)); |
114 (TextIO.output (stream, (strip_specials s)); |
117 TextIO.output (stream, \"\\n\"); |
115 TextIO.output (stream, "\n"); |
118 TextIO.flushOut stream));"} |
116 TextIO.flushOut stream)); |
119 |
117 *} |
120 Calling @{ML_text "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
118 |
|
119 text {* |
|
120 |
|
121 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
121 will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. |
122 will cause that all tracing information is printed into the file @{ML_text "foo.bar"}. |
122 |
123 |
123 *} |
124 *} |
124 |
125 |
125 |
126 |
139 The name of this theory can be extracted using the function |
140 The name of this theory can be extracted using the function |
140 @{ML "Context.theory_name"}. |
141 @{ML "Context.theory_name"}. |
141 |
142 |
142 Note, however, that antiquotations are statically scoped, that is the value is |
143 Note, however, that antiquotations are statically scoped, that is the value is |
143 determined at ``compile-time'', not ``run-time''. For example the function |
144 determined at ``compile-time'', not ``run-time''. For example the function |
144 |
145 *} |
145 @{ML_decl [display] |
146 |
146 "fun not_current_thyname () = Context.theory_name @{theory}"} |
147 ML {* |
|
148 fun not_current_thyname () = Context.theory_name @{theory} |
|
149 *} |
|
150 |
|
151 text {* |
147 |
152 |
148 does \emph{not} return the name of the current theory, if it is run in a |
153 does \emph{not} return the name of the current theory, if it is run in a |
149 different theory. Instead, the code above defines the constant function |
154 different theory. Instead, the code above defines the constant function |
150 that always returns the string @{ML_text "FirstSteps"}, no matter where the |
155 that always returns the string @{ML_text "FirstSteps"}, no matter where the |
151 function is called. Operationally speaking, @{text "@{theory}"} is |
156 function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is |
152 \emph{not} replaced with code that will look up the current theory in |
157 \emph{not} replaced with code that will look up the current theory in |
153 some data structure and return it. Instead, it is literally |
158 some data structure and return it. Instead, it is literally |
154 replaced with the value representing the theory name. |
159 replaced with the value representing the theory name. |
155 |
160 |
156 In a similar way you can use antiquotations to refer to theorems or simpsets: |
161 In a similar way you can use antiquotations to refer to theorems or simpsets: |
157 |
162 |
158 @{ML [display] "@{thm allI}"} |
163 @{ML [display] "@{thm allI}"} |
159 @{ML [display] "@{simpset}"} |
164 @{ML [display] "@{simpset}"} |
160 |
165 |
161 In the course of this introduction, we will learn more about |
166 While antiquotations have many uses, they were introduced to avoid explicit |
|
167 bindings for theorems such as |
|
168 *} |
|
169 |
|
170 ML {* |
|
171 val allI = thm "allI" |
|
172 *} |
|
173 |
|
174 text {* |
|
175 These bindings were difficult to maintain and also could be overwritten |
|
176 by bindings introduced by the user. This had the potential to break |
|
177 definitional packages. This additional layer of maintenance complexity |
|
178 can be avoided by using antiquotations, since they are ``linked'' statically |
|
179 at compile time. In the course of this introduction, we will learn more about |
162 these antiquotations: they greatly simplify Isabelle programming since one |
180 these antiquotations: they greatly simplify Isabelle programming since one |
163 can directly access all kinds of logical elements from ML. |
181 can directly access all kinds of logical elements from ML. |
164 |
182 |
165 *} |
183 *} |
166 |
184 |
255 While antiquotations are very convenient for constructing terms and types, |
273 While antiquotations are very convenient for constructing terms and types, |
256 they can only construct fixed terms. Unfortunately, one often needs to construct them |
274 they can only construct fixed terms. Unfortunately, one often needs to construct them |
257 dynamically. For example, a function that returns the implication |
275 dynamically. For example, a function that returns the implication |
258 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"} |
276 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"} |
259 as arguments can only be written as |
277 as arguments can only be written as |
260 |
278 *} |
261 @{ML_decl [display] |
279 |
262 "fun make_imp P Q tau = |
280 ML {* |
|
281 fun make_imp P Q tau = |
263 let |
282 let |
264 val x = Free (\"x\",tau) |
283 val x = Free ("x",tau) |
265 in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), |
284 in Logic.all x (Logic.mk_implies (HOLogic.mk_Trueprop (P $ x), |
266 HOLogic.mk_Trueprop (Q $ x))) |
285 HOLogic.mk_Trueprop (Q $ x))) |
267 end"} |
286 end |
|
287 *} |
|
288 |
|
289 text {* |
268 |
290 |
269 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
291 The reason is that one cannot pass the arguments @{term P}, @{term Q} and |
270 @{term "tau"} into an antiquotation. For example the following does not work. |
292 @{term "tau"} into an antiquotation. For example the following does not work. |
271 |
293 *} |
272 @{ML_decl [display] "fun make_wrong_imp P Q tau = @{prop \"\<And>x. P x \<Longrightarrow> Q x\"}"} |
294 |
273 |
295 ML {* |
|
296 fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} |
|
297 *} |
|
298 |
|
299 text {* |
274 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
300 To see this apply @{text "@{term S}"}, @{text "@{term T}"} and @{text "@{typ nat}"} |
275 to both functions. |
301 to both functions. |
276 |
302 |
277 One tricky point in constructing terms by hand is to obtain the |
303 One tricky point in constructing terms by hand is to obtain the |
278 fully qualified name for constants. For example the names for @{text "zero"} or |
304 fully qualified name for constants. For example the names for @{text "zero"} or |