390 (Syntax.read_term ctxt1 \"x\", |
390 (Syntax.read_term ctxt1 \"x\", |
391 Syntax.read_term ctxt2 \"x\") |
391 Syntax.read_term ctxt2 \"x\") |
392 end" |
392 end" |
393 "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"} |
393 "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"} |
394 |
394 |
395 The most useful feature of contexts is that one can export terms and theorems |
395 The most useful feature of contexts is that one can export, or transfer, |
396 between them. Let us show this first in the case of terms. |
396 terms and theorems between them. We show this first for terms. |
397 |
397 |
398 \begin{isabelle} |
398 \begin{isabelle} |
399 \begin{graybox} |
399 \begin{graybox} |
400 \begin{linenos} |
400 \begin{linenos} |
401 @{ML "let |
401 @{ML "let |
414 \end{graybox} |
414 \end{graybox} |
415 \end{isabelle} |
415 \end{isabelle} |
416 |
416 |
417 In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in |
417 In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in |
418 context @{text ctxt1}. The function @{ML_ind export_terms in |
418 context @{text ctxt1}. The function @{ML_ind export_terms in |
419 Variable} from the @{ML_struct Variable} can be used to ``transfer'' |
419 Variable} from the @{ML_struct Variable} can be used to transfer |
420 terms between contexts. Transferring means to turn all (free) |
420 terms between contexts. Transferring means to turn all (free) |
421 variables that are fixed in one context, but not in the other, into |
421 variables that are fixed in one context, but not in the other, into |
422 schematic variables. In our example, we are transferring the term |
422 schematic variables. In our example, we are transferring the term |
423 @{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"}, |
423 @{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"}, |
424 which means @{term x}, @{term y} and @{term z} become schematic |
424 which means @{term x}, @{term y} and @{term z} become schematic |
429 function @{ML_ind singleton}, because the function @{ML_ind |
429 function @{ML_ind singleton}, because the function @{ML_ind |
430 export_terms in Variable} normally works over lists of terms. |
430 export_terms in Variable} normally works over lists of terms. |
431 |
431 |
432 The case of transferring theorems is even more useful. The reason is |
432 The case of transferring theorems is even more useful. The reason is |
433 that the generalisation of fixed variables to schematic variables is |
433 that the generalisation of fixed variables to schematic variables is |
434 not trivial. For illustration purposes we use in the following code |
434 not trivial if done manually. For illustration purposes we use in the |
435 the function @{ML_ind make_thm in Skip_Proof} from the structure |
435 following code the function @{ML_ind make_thm in Skip_Proof} from the |
436 @{ML_struct Skip_Proof} in order to turn an arbitray term into a |
436 structure @{ML_struct Skip_Proof} in order to turn an arbitray term, |
437 theorem. |
437 in our case @{term "P x y z x y z"}, into a theorem. |
438 |
438 |
439 @{ML_response_fake [display, gray] |
439 @{ML_response_fake [display, gray] |
440 "let |
440 "let |
441 val thy = @{theory} |
441 val thy = @{theory} |
442 val ctxt0 = @{context} |
442 val ctxt0 = @{context} |
443 val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 |
443 val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0 |
444 val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"} |
444 val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"} |
445 in |
445 in |
446 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
446 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
447 end" |
447 end" |
448 "> P ?x ?y ?z ?x ?y ?z"} |
448 "?P ?x ?y ?z ?x ?y ?z"} |
449 *} |
449 |
450 |
450 The result is that all variables are schematic. The great point about |
451 |
451 contexts is that exporting is not just concerned with variables, but |
452 ML {* |
452 also assumptions. |
453 let |
453 *} |
454 val thy = @{theory} |
454 |
455 val ctxt0 = @{context} |
|
456 val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 |
|
457 val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"} |
|
458 in |
|
459 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm |
|
460 end |
|
461 *} |
|
462 |
455 |
463 |
456 |
464 text {* |
457 text {* |
465 |
458 |
466 *} |
459 *} |