164   val foo_const = ((@{binding "FOO"}, @{typ "nat => nat"}), NoSyn)

   164   val foo_const = ((@{binding "FOO"}, @{typ "nat \<Rightarrow> nat"}), NoSyn)

   168   val _ = writeln (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2)

   168   val _ = pwriteln 

   169     (Pretty.str (@{make_string} trm1 ^ "\n" ^ @{make_string} trm2))

   262   of the term changes with which context is used.

   268   of the term changes according to which context is used.

   298   free variables as being alien or faulty.  While this seems like a minor

   304   free variables as being alien or faulty.  Therefore the highlighting. 

   299   detail, the concept of making the context aware of fixed variables is

   305   While this seems like a minor detail, the concept of making the context aware 

   300   actually quite useful. For example it prevents us from fixing a variable

   306   of fixed variables is actually quite useful. For example it prevents us from 

   301   twice

   307   fixing a variable twice

   308   More importantly it also allows us to easily create fresh free variables avoiding any 

   314   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

   315   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}

   316   variant_fixes in Variable} from the structure @{ML_struct Variable}.

   311   as variants of the string @{text [quotes] "x"}.

   317 

   318   @{ML_response_fake [gray, display]

   319   "@{context}

   320 |> Variable.variant_fixes [\"y\", \"y\", \"z\"]" 

   321   "([\"y\", \"ya\", \"z\"], ...)"}

   322 

   323   Now a fresh variant for the second occurence of @{text y} is created

   324   avoiding any clash. In this way we can also create fresh free variables

   325   that avoid any clashes with fixed variables. In Line~3 below we fix

   326   the variable @{text x} in the context @{text ctxt1}. Next we want to

   327   create two fresh variables of type @{typ nat} as variants of the

   328   string @{text [quotes] "x"} (Lines 6 and 7).

   343   variables. Note that @{ML_ind declare_term in Variable} does not fix the

   360   variables, since @{text x} and @{text xa} occur in the term we declared. 

   344   variables; it just makes them ``known'' to the context. This is helpful when

   361   Note that @{ML_ind declare_term in Variable} does not fix the

   345   parsing terms using the function @{ML_ind read_term in Syntax} from the

   362   variables; it just makes them ``known'' to the context. You can see

   346   structure @{ML_struct Syntax}. Consider the following code:

   363   that if you print out a declared term.

   364 

   365   \begin{isabelle}

   366   \begin{graybox}

   367   @{ML "let

   368   val trm = @{term \"P x y z\"}

   369   val ctxt1 = Variable.declare_term trm @{context}

   370 in

   371   pwriteln (pretty_term ctxt1 trm)

   372 end"}\\

   373   \setlength{\fboxsep}{0mm}

   374   @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%

   375   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text x}}}~%

   376   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text y}}}~%

   377   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text z}}}

   378   \end{graybox}

   379   \end{isabelle}

   380 

   381   All variables are highligted, indicating that they are not

   382   fixed. However, declaring a term is helpful when parsing terms using

   383   the function @{ML_ind read_term in Syntax} from the structure

   384   @{ML_struct Syntax}. Consider the following code:

   374   The most useful feature of contexts is that one can export, for example,

   412   The most useful feature of contexts is that one can export, or transfer, 

   375   terms between contexts.

   413   terms and theorems between them. We show this first for terms. 

   376 *}

   414 

   377 

   415   \begin{isabelle}

   378 ML {*

   416   \begin{graybox}

   379 let

   417   \begin{linenos}

   418   @{ML "let

   381   val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 

   420   val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 

   382   val foo_trm = @{term "P x y z"}

   421   val foo_trm = @{term \"P x y z\"}

   385   |> pretty_term ctxt1

   424   |> pretty_term ctxt0

   387 end

   426 end"}

   388 *}

   427   \end{linenos}

   389 

   428   \setlength{\fboxsep}{0mm}

   390 ML {*

   429   @{text ">"}~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{@{text P}}}~%

   391 let

   430   @{text "?x ?y ?z"}

   431   \end{graybox}

   432   \end{isabelle}

   433 

   434   In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in

   435   context @{text ctxt1}.  The function @{ML_ind export_terms in

   436   Variable} from the structure @{ML_struct Variable} can be used to transfer

   437   terms between contexts. Transferring means to turn all (free)

   438   variables that are fixed in one context, but not in the other, into

   439   schematic variables. In our example, we are transferring the term

   440   @{text "P x y z"} from context @{text "ctxt1"} to @{text "ctxt0"},

   441   which means @{term x}, @{term y} and @{term z} become schematic

   442   variables (as can be seen by the leading question marks in the result). 

   443   Note that the variable @{text P} stays a free variable, since it not fixed in

   444   @{text ctxt1}; it is even highlighed, because @{text "ctxt0"} does

   445   not know about it. Note also that in Line 6 we had to use the

   446   function @{ML_ind singleton}, because the function @{ML_ind

   447   export_terms in Variable} normally works over lists of terms.

   448 

   449   The case of transferring theorems is even more useful. The reason is

   450   that the generalisation of fixed variables to schematic variables is

   451   not trivial if done manually. For illustration purposes we use in the 

   452   following code the function @{ML_ind make_thm in Skip_Proof} from the 

   453   structure @{ML_struct Skip_Proof}. This function will turn an arbitray 

   454   term, in our case @{term "P x y z x y z"}, into a theorem (disregarding 

   455   whether it is actually provable).

   456 

   457   @{ML_response_fake [display, gray]

   458   "let

   394   val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 

   461   val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0 

   395   val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}

   462   val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}

   398 end

   465 end"

   399 *}

   466   "?P ?x ?y ?z ?x ?y ?z"}

   400 

   467 

   401 ML {*

   468   Since we fixed all variables in @{text ctxt1}, in the exported

   402 let

   469   result all of them are schematic. The great point of contexts is

   403   val thy = @{theory}

   470   that exporting from one to another is not just restricted to

   471   variables, but also works with assumptions. For this we can use the

   472   function @{ML_ind export in Assumption} from the structure

   473   @{ML_struct Assumption}. Consider the following code.

   474 

   475   @{ML_response_fake [display, gray, linenos]

   476   "let

   405   val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 

   478   val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0

   406   val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z"}

   479   val eq' = Thm.symmetric eq

   407 in

   480 in

   408   singleton (Proof_Context.export ctxt1 ctxt0) foo_thm

   481   Assumption.export false ctxt1 ctxt0 eq'

   409 end

   482 end"

   410 *}

   483   "x \<equiv> y \<Longrightarrow> y \<equiv> x"}

   484   

   485   The function @{ML_ind add_assumes in Assumption} from the structure

   486   @{ML_struct Assumption} adds the assumption \mbox{@{text "x \<equiv> y"}}

   487   to the context @{text ctxt1} (Line 3). This function expects a list

   488   of @{ML_type cterm}s and returns them as theorems, together with the

   489   new context in which they are ``assumed''. In Line 4 we use the

   490   function @{ML_ind symmetric in Thm} from the structure @{ML_struct

   491   Thm} in order to obtain the symmetric version of the assumed

   492   meta-equality. Now exporting the theorem @{text "eq'"} from @{text

   493   ctxt1} to @{text ctxt0} means @{term "y \<equiv> x"} will be prefixed with

   494   the assumed theorem. The boolean flag in @{ML_ind export in

   495   Assumption} indicates whether the assumptions should be marked with

   496   the goal marker (see Section~\ref{sec:basictactics}). In normal

   497   circumstances this is not necessary and so should be set to @{ML

   498   false}.  The result of the export is then the theorem \mbox{@{term

   499   "x \<equiv> y \<Longrightarrow> y \<equiv> x"}}.  As can be seen this is an easy way for obtaing

   500   simple theorems. We will explain this in more detail in

   501   Section~\ref{sec:structured}.

   502 

   503   The function @{ML_ind export in Proof_Context} from the structure 

   504   @{ML_struct Proof_Context} combines both export functions from 

   505   @{ML_struct Variable} and @{ML_struct Assumption}. This can be seen

   506   in the following example.

   507 

   508   @{ML_response_fake [display, gray]

   509   "let

   510   val ctxt0 = @{context}

   511   val ((fvs, [eq]), ctxt1) = ctxt0

   512     |> Variable.add_fixes [\"x\", \"y\"]

   513     ||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]

   514   val eq' = Thm.symmetric eq

   515 in

   516   Proof_Context.export ctxt1 ctxt0 [eq']

   517 end"

   518   "[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}

   519 *}

   520 

   521 

   451 section {* Local Theories (TBD) *}

   562 section {* Local Theories and Local Setups\label{sec:local} (TBD) *}