296 are printed as expected. The point of this example is that the context |
296 are printed as expected. The point of this example is that the context |
297 contains the information which variables are fixed, and designates all other |
297 contains the information which variables are fixed, and designates all other |
298 free variables as being alien or faulty. Therefore the highlighting. |
298 free variables as being alien or faulty. Therefore the highlighting. |
299 While this seems like a minor detail, the concept of making the context aware |
299 While this seems like a minor detail, the concept of making the context aware |
300 of fixed variables is actually quite useful. For example it prevents us from |
300 of fixed variables is actually quite useful. For example it prevents us from |
301 fixing a variable twice. |
301 fixing a variable twice |
302 |
302 |
303 @{ML_response_fake [gray, display] |
303 @{ML_response_fake [gray, display] |
304 "@{context} |
304 "@{context} |
305 |> Variable.add_fixes [\"x\", \"x\"]" |
305 |> Variable.add_fixes [\"x\", \"x\"]" |
306 "ERROR: Duplicate fixed variable(s): \"x\""} |
306 "ERROR: Duplicate fixed variable(s): \"x\""} |
307 |
307 |
308 More importantly it also allows us to easily create fresh free variables avoiding any |
308 More importantly it also allows us to easily create fresh names for |
309 clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context |
309 fixed variables. For this you have to use the function @{ML_ind |
310 @{text ctxt1}. Next we want to create two fresh variables of type @{typ nat} |
310 variant_fixes in Variable} from the structure @{ML_struct Variable}. |
311 as variants of the string @{text [quotes] "x"} (Lines 6 and 7). |
311 |
|
312 @{ML_response_fake [gray, display] |
|
313 "@{context} |
|
314 |> Variable.variant_fixes [\"y\", \"y\", \"z\"]" |
|
315 "([\"y\", \"ya\", \"z\"], ...)"} |
|
316 |
|
317 Now a fresh variant for the second occurence of @{text y} is created |
|
318 avoiding any clash. In this way we can also create free variables |
|
319 that avoid any clashes with fixed variables. In Line~3 below we fix |
|
320 the variable @{text x} in the context @{text ctxt1}. Next we want to |
|
321 create two fresh variables of type @{typ nat} as variants of the |
|
322 string @{text [quotes] "x"} (Lines 6 and 7). |
312 |
323 |
313 @{ML_response_fake [display, gray, linenos] |
324 @{ML_response_fake [display, gray, linenos] |
314 "let |
325 "let |
315 val ctxt0 = @{context} |
326 val ctxt0 = @{context} |
316 val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0 |
327 val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0 |
446 in |
457 in |
447 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
458 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
448 end" |
459 end" |
449 "?P ?x ?y ?z ?x ?y ?z"} |
460 "?P ?x ?y ?z ?x ?y ?z"} |
450 |
461 |
451 Since we fixed all variables in @{text ctxt1}, in result all of them |
462 Since we fixed all variables in @{text ctxt1}, in the result all of them |
452 are schematic. The great point is that exporting between contexts is |
463 are schematic. The great point of contexts is that exporting from one to |
453 not just concerned with variables, but also assumptions. For this we |
464 another is not just concerned with variables, but also assumptions. For this we |
454 can use the function @{ML_ind export in Assumption} from the structure |
465 can use the function @{ML_ind export in Assumption} from the structure |
455 @{ML_struct Assumption}. Consider the following code. |
466 @{ML_struct Assumption}. Consider the following code. |
456 |
467 |
457 @{ML_response_fake [display, gray, linenos] |
468 @{ML_response_fake [display, gray, linenos] |
458 "let |
469 "let |