# HG changeset patch # User wenzelm # Date 1265143047 -3600 # Node ID 28e231e4144b20a42a4a1d4d26fab070696f9412 # Parent fd90fb0903c019b972d5a47eca7192efdd7c4a78 some examples for basic context operations; diff -r fd90fb0903c0 -r 28e231e4144b doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Tue Feb 02 13:22:36 2010 +0100 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Tue Feb 02 21:37:27 2010 +0100 @@ -145,6 +145,72 @@ \end{description} *} +text %mlex {* The following example (in theory @{theory Pure}) shows + how to work with fixed term and type parameters work with + type-inference. +*} + +typedecl foo -- {* some basic type for testing purposes *} + +ML {* + (*static compile-time context -- for testing only*) + val ctxt0 = @{context}; + + (*locally fixed parameters -- no type assignment yet*) + val ([x, y], ctxt1) = ctxt0 |> Variable.add_fixes ["x", "y"]; + + (*t1: most general fixed type; t1': most general arbitrary type*) + val t1 = Syntax.read_term ctxt1 "x"; + val t1' = singleton (Variable.polymorphic ctxt1) t1; + + (*term u enforces specific type assignment*) + val u = Syntax.read_term ctxt1 "(x::foo) \ y"; + + (*official declaration of u -- propagates constraints etc.*) + val ctxt2 = ctxt1 |> Variable.declare_term u; + val t2 = Syntax.read_term ctxt2 "x"; (*x::foo is enforced*) +*} + +text {* In the above example, the starting context had been derived + from the toplevel theory, which means that fixed variables are + internalized literally: @{verbatim "x"} is mapped again to + @{verbatim "x"}, and attempting to fix it again in the subsequent + context is an error. Alternatively, fixed parameters can be renamed + explicitly as follows: +*} + +ML {* + val ctxt0 = @{context}; + val ([x1, x2, x3], ctxt1) = + ctxt0 |> Variable.variant_fixes ["x", "x", "x"]; +*} + +text {* \noindent Subsequent ML code can now work with the invented + names of @{verbatim x1}, @{verbatim x2}, @{verbatim x3}, without + depending on the details on the system policy for introducing these + variants. Recall that within a proof body the system always invents + fresh ``skolem constants'', e.g.\ as follows: +*} + +lemma "PROP XXX" +proof - + ML_prf %"ML" {* + val ctxt0 = @{context}; + + val ([x1], ctxt1) = ctxt0 |> Variable.add_fixes ["x"]; + val ([x2], ctxt2) = ctxt1 |> Variable.add_fixes ["x"]; + val ([x3], ctxt3) = ctxt2 |> Variable.add_fixes ["x"]; + + val ([y1, y2], ctxt4) = + ctxt3 |> Variable.variant_fixes ["y", "y"]; + *} + oops + +text {* \noindent In this situation @{ML Variable.add_fixes} and @{ML + Variable.variant_fixes} are very similar, but identical name + proposals given in a row are only accepted by the second version. +*} + section {* Assumptions \label{sec:assumptions} *} @@ -246,6 +312,30 @@ \end{description} *} +text %mlex {* The following example demonstrates how rules can be + derived by building up a context of assumptions first, and exporting + some local fact afterwards. We refer to @{theory Pure} equality + here for testing purposes. +*} + +ML {* + (*static compile-time context -- for testing only*) + val ctxt0 = @{context}; + + val ([eq], ctxt1) = + ctxt0 |> Assumption.add_assumes [@{cprop "x \ y"}]; + val eq' = Thm.symmetric eq; + + (*back to original context -- discharges assumption*) + val r = Assumption.export false ctxt1 ctxt0 eq'; +*} + +text {* \noindent Note that the variables of the resulting rule are + not generalized. This would have required to fix them properly in + the context beforehand, and export wrt.\ variables afterwards (cf.\ + @{ML Variable.export} or the combined @{ML "ProofContext.export"}). +*} + section {* Structured goals and results \label{sec:struct-goals} *}