diff -r 3778bddfb824 -r 1d1165432c9f ProgTutorial/Advanced.thy --- a/ProgTutorial/Advanced.thy Thu Nov 24 19:54:01 2011 +0000 +++ b/ProgTutorial/Advanced.thy Fri Nov 25 00:27:05 2011 +0000 @@ -161,11 +161,12 @@ setup %graylinenos {* fn thy => let val tmp_thy = Theory.copy thy - val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn) + val foo_const = ((@{binding "FOO"}, @{typ "nat \ nat"}), NoSyn) val (_, tmp_thy') = Sign.declare_const @{context} foo_const tmp_thy val trm1 = Syntax.read_term_global tmp_thy' "FOO baz" val trm2 = Syntax.read_term_global thy "FOO baz" - val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2) + val _ = pwriteln + (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)) in thy end *} @@ -192,6 +193,11 @@ inference. This is relevant in situations where definitions are made later, but parsing and type inference has to take already proceed as if the definitions were already made. + + \begin{readmore} + Most of the functions about theories are implemented in + @{ML_file "Pure/theory.ML"} and @{ML_file "Pure/global_theory.ML"}. + \end{readmore} *} section {* Contexts *} @@ -259,7 +265,7 @@ specified by strings. Let us come back to the point about printing terms. Consider printing out the term \mbox{@{text "(x, y, z, w)"}} using our function @{ML_ind pretty_term}. This function takes a term and a context as argument. Notice how the printing - of the term changes with which context is used. + of the term changes according to which context is used. \begin{isabelle} \begin{graybox} @@ -295,20 +301,31 @@ variables, but not @{text z} and @{text w}. In the last case all variables are printed as expected. The point of this example is that the context contains the information which variables are fixed, and designates all other - free variables as being alien or faulty. While this seems like a minor - detail, the concept of making the context aware of fixed variables is - actually quite useful. For example it prevents us from fixing a variable - twice + free variables as being alien or faulty. Therefore the highlighting. + While this seems like a minor detail, the concept of making the context aware + of fixed variables is actually quite useful. For example it prevents us from + fixing a variable twice @{ML_response_fake [gray, display] "@{context} |> Variable.add_fixes [\"x\", \"x\"]" "ERROR: Duplicate fixed variable(s): \"x\""} - More importantly it also allows us to easily create fresh free variables avoiding any - clashes with fixed variables. In Line~3 below we fix the variable @{text x} in the context - @{text ctxt1}. Next we want to create two fresh variables of type @{typ nat} - as variants of the string @{text [quotes] "x"}. + More importantly it also allows us to easily create fresh names for + fixed variables. For this you have to use the function @{ML_ind + variant_fixes in Variable} from the structure @{ML_struct Variable}. + + @{ML_response_fake [gray, display] + "@{context} +|> Variable.variant_fixes [\"y\", \"y\", \"z\"]" + "([\"y\", \"ya\", \"z\"], ...)"} + + Now a fresh variant for the second occurence of @{text y} is created + avoiding any clash. In this way we can also create fresh free variables + that avoid any clashes with fixed variables. In Line~3 below we fix + the variable @{text x} in the context @{text ctxt1}. Next we want to + create two fresh variables of type @{typ nat} as variants of the + string @{text [quotes] "x"} (Lines 6 and 7). @{ML_response_fake [display, gray, linenos] "let @@ -340,10 +357,31 @@ "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"} The result is @{text xb} and @{text xc} for the names of the fresh - variables. Note that @{ML_ind declare_term in Variable} does not fix the - variables; it just makes them ``known'' to the context. This is helpful when - parsing terms using the function @{ML_ind read_term in Syntax} from the - structure @{ML_struct Syntax}. Consider the following code: + variables, since @{text x} and @{text xa} occur in the term we declared. + Note that @{ML_ind declare_term in Variable} does not fix the + variables; it just makes them ``known'' to the context. You can see + that if you print out a declared term. + + \begin{isabelle} + \begin{graybox} + @{ML "let + val trm = @{term \"P x y z\"} + val ctxt1 = Variable.declare_term trm @{context} +in + pwriteln (pretty_term ctxt1 trm) +end"}\\ + \setlength{\fboxsep}{0mm} + @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}~% + \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}} + \end{graybox} + \end{isabelle} + + All variables are highligted, indicating that they are not + fixed. However, declaring a term is helpful when parsing terms using + the function @{ML_ind read_term in Syntax} from the structure + @{ML_struct Syntax}. Consider the following code: @{ML_response_fake [gray, display] "let @@ -371,43 +409,116 @@ end" "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"} - The most useful feature of contexts is that one can export, for example, - terms between contexts. -*} + The most useful feature of contexts is that one can export, or transfer, + terms and theorems between them. We show this first for terms. -ML {* -let + \begin{isabelle} + \begin{graybox} + \begin{linenos} + @{ML "let val ctxt0 = @{context} - val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 - val foo_trm = @{term "P x y z"} + val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 + val foo_trm = @{term \"P x y z\"} in singleton (Variable.export_terms ctxt1 ctxt0) foo_trm - |> pretty_term ctxt1 + |> pretty_term ctxt0 |> pwriteln -end +end"} + \end{linenos} + \setlength{\fboxsep}{0mm} + @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~% + @{text "?x ?y ?z"} + \end{graybox} + \end{isabelle} + + In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in + context @{text ctxt1}. The function @{ML_ind export_terms in + Variable} from the structure @{ML_struct Variable} can be used to transfer + terms between contexts. Transferring means to turn all (free) + variables that are fixed in one context, but not in the other, into + schematic variables. In our example, we are transferring the term + @{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"}, + which means @{term x}, @{term y} and @{term z} become schematic + variables (as can be seen by the leading question marks in the result). + Note that the variable @{text P} stays a free variable, since it not fixed in + @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does + not know about it. Note also that in Line 6 we had to use the + function @{ML_ind singleton}, because the function @{ML_ind + export_terms in Variable} normally works over lists of terms. + + The case of transferring theorems is even more useful. The reason is + that the generalisation of fixed variables to schematic variables is + not trivial if done manually. For illustration purposes we use in the + following code the function @{ML_ind make_thm in Skip_Proof} from the + structure @{ML_struct Skip_Proof}. This function will turn an arbitray + term, in our case @{term "P x y z x y z"}, into a theorem (disregarding + whether it is actually provable). + + @{ML_response_fake [display, gray] + "let + val thy = @{theory} + val ctxt0 = @{context} + val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0 + val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"} +in + singleton (Proof_Context.export ctxt1 ctxt0) foo_thm +end" + "?P ?x ?y ?z ?x ?y ?z"} + + Since we fixed all variables in @{text ctxt1}, in the exported + result all of them are schematic. The great point of contexts is + that exporting from one to another is not just restricted to + variables, but also works with assumptions. For this we can use the + function @{ML_ind export in Assumption} from the structure + @{ML_struct Assumption}. Consider the following code. + + @{ML_response_fake [display, gray, linenos] + "let + val ctxt0 = @{context} + val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \ y\"}] ctxt0 + val eq' = Thm.symmetric eq +in + Assumption.export false ctxt1 ctxt0 eq' +end" + "x \ y \ y \ x"} + + The function @{ML_ind add_assumes in Assumption} from the structure + @{ML_struct Assumption} adds the assumption \mbox{@{text "x \ y"}} + to the context @{text ctxt1} (Line 3). This function expects a list + of @{ML_type cterm}s and returns them as theorems, together with the + new context in which they are ``assumed''. In Line 4 we use the + function @{ML_ind symmetric in Thm} from the structure @{ML_struct + Thm} in order to obtain the symmetric version of the assumed + meta-equality. Now exporting the theorem @{text "eq'"} from @{text + ctxt1} to @{text ctxt0} means @{term "y \ x"} will be prefixed with + the assumed theorem. The boolean flag in @{ML_ind export in + Assumption} indicates whether the assumptions should be marked with + the goal marker (see Section~\ref{sec:basictactics}). In normal + circumstances this is not necessary and so should be set to @{ML + false}. The result of the export is then the theorem \mbox{@{term + "x \ y \ y \ x"}}. As can be seen this is an easy way for obtaing + simple theorems. We will explain this in more detail in + Section~\ref{sec:structured}. + + The function @{ML_ind export in Proof_Context} from the structure + @{ML_struct Proof_Context} combines both export functions from + @{ML_struct Variable} and @{ML_struct Assumption}. This can be seen + in the following example. + + @{ML_response_fake [display, gray] + "let + val ctxt0 = @{context} + val ((fvs, [eq]), ctxt1) = ctxt0 + |> Variable.add_fixes [\"x\", \"y\"] + ||>> Assumption.add_assumes [@{cprop \"x \ y\"}] + val eq' = Thm.symmetric eq +in + Proof_Context.export ctxt1 ctxt0 [eq'] +end" + "[?x \ ?y \ ?y \ ?x]"} *} -ML {* -let - val thy = @{theory} - val ctxt0 = @{context} - val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 - val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"} -in - singleton (Proof_Context.export ctxt1 ctxt0) foo_thm -end -*} -ML {* -let - val thy = @{theory} - val ctxt0 = @{context} - val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 - val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"} -in - singleton (Proof_Context.export ctxt1 ctxt0) foo_thm -end -*} text {* @@ -448,7 +559,7 @@ oops *) -section {* Local Theories (TBD) *} +section {* Local Theories and Local Setups\label{sec:local} (TBD) *} text {* In contrast to an ordinary theory, which simply consists of a type