241 txt_raw {*\mbox{}\\[-7mm]*} |
241 txt_raw {*\mbox{}\\[-7mm]*} |
242 ML_prf {* Variable.dest_fixes @{context} *} |
242 ML_prf {* Variable.dest_fixes @{context} *} |
243 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
243 txt_raw {*\mbox{}\\[-7mm] \ldots*}(*<*)oops(*>*) |
244 |
244 |
245 text {* |
245 text {* |
246 The first time we call @{ML dest_fixes in Variable} we have four fixes variables; |
246 Here the first time we call @{ML dest_fixes in Variable} we have four fixes variables; |
247 the second time we get only the fixes variables @{text x} and @{text y} as answer. |
247 the second time we get only the fixes variables @{text x} and @{text y} as answer, since |
248 This means the curly-braces act as opening and closing statements for a context. |
248 @{text z} and @{text w} are not anymore in the scope of the context. |
249 The above proof corresoponds roughly to the following ML-code. |
249 This means the curly-braces act on the Isabelle level as opening and closing statements |
|
250 for a context. The above proof fragment corresoponds roughly to the following ML-code |
250 *} |
251 *} |
251 |
252 |
252 ML{*val ctxt0 = @{context}; |
253 ML{*val ctxt0 = @{context}; |
253 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
254 val ([x, y], ctxt1) = Variable.add_fixes ["x", "y"] ctxt0; |
254 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
255 val ([z, w], ctxt2) = Variable.add_fixes ["z", "w"] ctxt1*} |
255 |
256 |
256 text {* |
257 text {* |
257 where the function @{ML_ind add_fixes in Variable} fixes a list of variables |
258 where the function @{ML_ind add_fixes in Variable} fixes a list of variables |
258 specified by strings. Let us come back to the point about printing terms. Consider |
259 specified by strings. Let us come back to the point about printing terms. Consider |
259 printing out the term @{text "(x, y, z, w)"} using the function @{ML_ind pretty_term}. |
260 printing out the term \mbox{@{text "(x, y, z, w)"}} using our function @{ML_ind pretty_term}. |
260 This function takes a term and a context as argument. |
261 This function takes a term and a context as argument. |
261 *} |
262 |
262 |
263 \begin{isabelle} |
263 ML {* |
264 \begin{graybox} |
264 let |
265 @{ML "let |
265 val trm = @{term "(x, y, z, w)"} |
266 val trm = @{term \"(x, y, z, w)\"} |
266 in |
267 in |
267 pwriteln (Pretty.chunks |
268 pwriteln (Pretty.chunks |
268 [ pretty_term ctxt0 trm, |
269 [ pretty_term ctxt0 trm, |
269 pretty_term ctxt1 trm, |
270 pretty_term ctxt1 trm, |
270 pretty_term ctxt2 trm ]) |
271 pretty_term ctxt2 trm ]) |
271 end |
272 end"}\\ |
272 *} |
273 \setlength{\fboxsep}{0mm} |
273 |
274 @{text ">"}~@{text "("}\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~% |
274 |
275 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~% |
275 text {* |
276 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~% |
276 The term we are printing is in all three cases the same---a tuple containing four |
277 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}\\ |
277 free variables. As you can see in case of @{ML "ctxt0"}, however, all variables are highlighted |
278 @{text ">"}~@{text "("}\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~% |
278 indicating a problem, while in case of @{ML "ctxt1"} @{text x} and @{text y} are printed |
279 \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~% |
279 as normal (blue) free variables, but not @{text z} and @{text w}. In the last case all |
280 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~% |
280 variables are printed as expected. The point is that the context contains the information |
281 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"}\\ |
281 which variables are fixed, and designates all other free variables as being alien or faulty. |
282 @{text ">"}~@{text "("}\colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text x}}}@{text ","}~% |
282 While this seems like a minor feat, the concept of making the context aware of |
283 \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text y}}}@{text ","}~% |
283 fixed variables is actually quite useful. For example it prevents us from fixing a |
284 \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text z}}}@{text ","}~% |
284 variable twice |
285 \colorbox{gray!20}{\raisebox{0mm}[3mm][1mm]{@{text w}}}@{text ")"} |
|
286 \end{graybox} |
|
287 \end{isabelle} |
|
288 |
|
289 |
|
290 The term we are printing is in all three cases the same---a tuple containing |
|
291 four free variables. As you can see in case of @{ML "ctxt0"}, however, all |
|
292 variables are highlighted indicating a problem, while in case of @{ML |
|
293 "ctxt1"} @{text x} and @{text y} are printed as normal (blue) free |
|
294 variables, but not @{text z} and @{text w}. In the last case all variables |
|
295 are printed as expected. The point of this example is that the context |
|
296 contains the information which variables are fixed, and designates all other |
|
297 free variables as being alien or faulty. While this seems like a minor |
|
298 detail, the concept of making the context aware of fixed variables is |
|
299 actually quite useful. For example it prevents us from fixing a variable |
|
300 twice |
285 |
301 |
286 @{ML_response_fake [gray, display] |
302 @{ML_response_fake [gray, display] |
287 "@{context} |
303 "@{context} |
288 |> Variable.add_fixes [\"x\", \"y\"] |
304 |> Variable.add_fixes [\"x\", \"x\"]" |
289 ||>> Variable.add_fixes [\"x\", \"y\"]" |
305 "ERROR: Duplicate fixed variable(s): \"x\""} |
290 "Duplicate fixed variable(s): \"x\""} |
306 |
|
307 But it also allows us to easily create fresh free variables avoiding any |
|
308 clashes. In Line~3 below we fix the variable @{text x} in the context |
|
309 @{text ctxt1}. Next we want to create two fresh variables of type @{typ nat} |
|
310 as variants of the string @{text [quotes] "x"}. |
|
311 |
|
312 @{ML_response_fake [display, gray, linenos] |
|
313 "let |
|
314 val ctxt0 = @{context} |
|
315 val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0 |
|
316 val frees = replicate 2 (\"x\", @{typ nat}) |
|
317 in |
|
318 (Variable.variant_frees ctxt0 [] frees, |
|
319 Variable.variant_frees ctxt1 [] frees) |
|
320 end" |
|
321 "([(\"x\", \"nat\"), (\"xa\", \"nat\")], |
|
322 [(\"xa\", \"nat\"), (\"xb\", \"nat\")])"} |
|
323 |
|
324 As can be seen, if we create the fresh variables with the context @{text ctxt0}, |
|
325 then we obtain @{text "x"} and @{text "xa"}; but in @{text ctxt1} we obtain @{text "xa"} |
|
326 and @{text "xb"} avoiding @{text x}, which was fixed in this context. |
|
327 |
|
328 Often one has the situation that given some terms, create fresh variables |
|
329 avoiding any variable occuring in those terms. For this you can use the |
|
330 function @{ML_ind declare_term in Variable} from the structure @{ML_struct Variable}. |
|
331 |
|
332 @{ML_response_fake [gray, display] |
|
333 "let |
|
334 val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context} |
|
335 val frees = replicate 2 (\"x\", @{typ nat}) |
|
336 in |
|
337 Variable.variant_frees ctxt1 [] frees |
|
338 end" |
|
339 "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"} |
|
340 |
|
341 The result is @{text xb} and @{text xc} for the names of the freshh variables. This |
|
342 is also important when parsing terms, for example with the function |
|
343 @{ML_ind read_term in Syntax} from the structure @{ML_struct Syntax}. Consider |
|
344 the following code: |
|
345 |
|
346 @{ML_response_fake [gray, display] |
|
347 "let |
|
348 val ctxt0 = @{context} |
|
349 val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0 |
|
350 in |
|
351 (Syntax.read_term ctxt0 \"x\", |
|
352 Syntax.read_term ctxt1 \"x\") |
|
353 end" |
|
354 "(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"} |
|
355 |
|
356 Parsing the string in the first context results in a free variable |
|
357 with a default polymorphic type, but in the second case we obtain a |
|
358 free variable of type @{typ nat} as previously declared. Which |
|
359 type the parsed term receives depends on the last declaration that |
|
360 is made as the next example illustrates. |
|
361 |
|
362 @{ML_response_fake [gray, display] |
|
363 "let |
|
364 val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context} |
|
365 val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1 |
|
366 in |
|
367 (Syntax.read_term ctxt1 \"x\", |
|
368 Syntax.read_term ctxt2 \"x\") |
|
369 end" |
|
370 "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"} |
|
371 |
|
372 *} |
|
373 |
|
374 ML {* |
|
375 let |
|
376 val ctxt0 = @{context} |
|
377 val trm = @{prop "P x y z"} |
|
378 val foo_thm = Skip_Proof.make_thm (Proof_Context.theory_of ctxt0) trm |
|
379 val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 |
|
380 in |
|
381 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
|
382 end |
|
383 *} |
|
384 |
|
385 text {* |
|
386 |
291 *} |
387 *} |
292 |
388 |
293 |
389 |
294 (* |
390 (* |
295 ML{*Proof_Context.debug := true*} |
391 ML{*Proof_Context.debug := true*} |