57   \<open>> theorems: \<dots>\<close>

    57   \<open>> theorems: \<dots>\<close>

    58   \end{isabelle}

    58   \end{isabelle}

    59 

    59 

    60   Functions acting on theories often end with the suffix \<open>_global\<close>,

    60   Functions acting on theories often end with the suffix \<open>_global\<close>,

    61   for example the function @{ML read_term_global in Syntax} in the structure

    61   for example the function @{ML read_term_global in Syntax} in the structure

    63   functions acting on contexts or local theories, which will be discussed in

    63   functions acting on contexts or local theories, which will be discussed in

    64   the next sections. There is a tendency amongst Isabelle developers to prefer

    64   the next sections. There is a tendency amongst Isabelle developers to prefer

    65   ``non-global'' operations, because they have some advantages, as we will also

    65   ``non-global'' operations, because they have some advantages, as we will also

    66   discuss later. However, some basic understanding of theories is still necessary

    66   discuss later. However, some basic understanding of theories is still necessary

    67   for effective Isabelle programming.

    67   for effective Isabelle programming.

    72   scenes is that \isacommand{setup} expects a function of type @{ML_type

    72   scenes is that \isacommand{setup} expects a function of type @{ML_type

    73   "theory -> theory"}: the input theory is the current theory and the output

    73   "theory -> theory"}: the input theory is the current theory and the output

    74   the theory where the attribute has been registered or the theorem has been

    74   the theory where the attribute has been registered or the theorem has been

    75   stored.  This is a fundamental principle in Isabelle. A similar situation

    75   stored.  This is a fundamental principle in Isabelle. A similar situation

    76   arises with declaring a constant, which can be done on the ML-level with 

    76   arises with declaring a constant, which can be done on the ML-level with 

    78   Sign}. To see how \isacommand{setup} works, consider the following code:

    78   Sign}. To see how \isacommand{setup} works, consider the following code:

    79 

    79 

    80 \<close>  

    80 \<close>  

    81 

    81 

    82 ML %grayML\<open>let

    82 ML %grayML\<open>let

   174 text \<open>

   174 text \<open>

   175   The interesting point is that we injected ML-code before and after

   175   The interesting point is that we injected ML-code before and after

   176   the variables are fixed. For this remember that ML-code inside a proof

   176   the variables are fixed. For this remember that ML-code inside a proof

   177   needs to be enclosed inside \isacommand{ML\_prf}~\<open>\<verbopen> \<dots> \<verbclose>\<close>,

   177   needs to be enclosed inside \isacommand{ML\_prf}~\<open>\<verbopen> \<dots> \<verbclose>\<close>,

   178   not \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>. The function 

   178   not \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>. The function 

   180   a context and returns all its currently fixed variable (names). That 

   180   a context and returns all its currently fixed variable (names). That 

   181   means a context has a dataslot containing information about fixed variables.

   181   means a context has a dataslot containing information about fixed variables.

   182   The ML-antiquotation \<open>@{context}\<close> points to the context that is

   182   The ML-antiquotation \<open>@{context}\<close> points to the context that is

   183   active at that point of the theory. Consequently, in the first call to 

   183   active at that point of the theory. Consequently, in the first call to 

   184   @{ML dest_fixes in Variable} this dataslot is  empty; in the second it is 

   184   @{ML dest_fixes in Variable} this dataslot is  empty; in the second it is 

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

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

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

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

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

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

   253   fixing a variable twice

   253   fixing a variable twice

   254 

   254 

   256   "@{context}

   256   "@{context}

   257 |> Variable.add_fixes [\"x\", \"x\"]" 

   257 |> Variable.add_fixes [\"x\", \"x\"]" 

   258   "ERROR: Duplicate fixed variable(s): \"x\""}

   258   "ERROR: Duplicate fixed variable(s): \"x\""}

   259 

   259 

   260   More importantly it also allows us to easily create fresh names for

   260   More importantly it also allows us to easily create fresh names for

   261   fixed variables.  For this you have to use the function @{ML_ind

   261   fixed variables.  For this you have to use the function @{ML_ind

   265   "@{context}

   265   "@{context}

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

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

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

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

   268 

   268 

   269   Now a fresh variant for the second occurence of \<open>y\<close> is created

   269   Now a fresh variant for the second occurence of \<open>y\<close> is created

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

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

   272   the variable \<open>x\<close> in the context \<open>ctxt1\<close>. Next we want to

   272   the variable \<open>x\<close> in the context \<open>ctxt1\<close>. Next we want to

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

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

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

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

   275 

   275 

   277   "let

   277   "let

   278   val ctxt0 = @{context}

   278   val ctxt0 = @{context}

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

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

   280   val frees = replicate 2 (\"x\", @{typ nat})

   280   val frees = replicate 2 (\"x\", @{typ nat})

   281 in

   281 in

   289   then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>

   289   then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>

   290   and \<open>xb\<close> avoiding \<open>x\<close>, which was fixed in this context.

   290   and \<open>xb\<close> avoiding \<open>x\<close>, which was fixed in this context.

   291 

   291 

   292   Often one has the problem that given some terms, create fresh variables

   292   Often one has the problem that given some terms, create fresh variables

   293   avoiding any variable occurring in those terms. For this you can use the

   293   avoiding any variable occurring in those terms. For this you can use the

   297   "let

   297   "let

   298   val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}

   298   val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}

   299   val frees = replicate 2 (\"x\", @{typ nat})

   299   val frees = replicate 2 (\"x\", @{typ nat})

   300 in

   300 in

   301   Variable.variant_frees ctxt1 [] frees

   301   Variable.variant_frees ctxt1 [] frees

   325   \end{isabelle}

   325   \end{isabelle}

   326 

   326 

   327   All variables are highligted, indicating that they are not

   327   All variables are highligted, indicating that they are not

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

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

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

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

   333   "let

   333   "let

   334   val ctxt0 = @{context}

   334   val ctxt0 = @{context}

   335   val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0

   335   val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0

   336 in

   336 in

   337   (Syntax.read_term ctxt0 \"x\", 

   337   (Syntax.read_term ctxt0 \"x\", 

   343   with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a

   343   with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a

   344   free variable of type @{typ nat} as previously declared. Which

   344   free variable of type @{typ nat} as previously declared. Which

   345   type the parsed term receives depends upon the last declaration that

   345   type the parsed term receives depends upon the last declaration that

   346   is made, as the next example illustrates.

   346   is made, as the next example illustrates.

   347 

   347 

   349   "let

   349   "let

   350   val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}

   350   val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}

   351   val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1

   351   val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1

   352 in

   352 in

   353   (Syntax.read_term ctxt1 \"x\", 

   353   (Syntax.read_term ctxt1 \"x\", 

   377   \end{graybox}

   377   \end{graybox}

   378   \end{isabelle}

   378   \end{isabelle}

   379 

   379 

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

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

   381   context \<open>ctxt1\<close>.  The function @{ML_ind export_terms in

   381   context \<open>ctxt1\<close>.  The function @{ML_ind export_terms in

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

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

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

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

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

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

   386   \<open>P x y z\<close> from context \<open>ctxt1\<close> to \<open>ctxt0\<close>,

   386   \<open>P x y z\<close> from context \<open>ctxt1\<close> to \<open>ctxt0\<close>,

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

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

   394 

   394 

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

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

   396   that the generalisation of fixed variables to schematic variables is

   396   that the generalisation of fixed variables to schematic variables is

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

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

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

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

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

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

   401   whether it is actually provable).

   401   whether it is actually provable).

   402 

   402 

   404   "let

   404   "let

   405   val thy = @{theory}

   405   val thy = @{theory}

   406   val ctxt0 = @{context}

   406   val ctxt0 = @{context}

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

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

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

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

   414   Since we fixed all variables in \<open>ctxt1\<close>, in the exported

   414   Since we fixed all variables in \<open>ctxt1\<close>, in the exported

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

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

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

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

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

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

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

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

   422   "let

   422   "let

   423   val ctxt0 = @{context}

   423   val ctxt0 = @{context}

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

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

   425   val eq' = Thm.symmetric eq

   425   val eq' = Thm.symmetric eq

   426 in

   426 in

   427   Assumption.export false ctxt1 ctxt0 eq'

   427   Assumption.export false ctxt1 ctxt0 eq'

   428 end"

   428 end"

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

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

   430   

   430   

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

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

   433   to the context \<open>ctxt1\<close> (Line 3). This function expects a list

   433   to the context \<open>ctxt1\<close> (Line 3). This function expects a list

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

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

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

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

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

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

   438   meta-equality. Now exporting the theorem \<open>eq'\<close> from \<open>ctxt1\<close> to \<open>ctxt0\<close> means @{term "y \<equiv> x"} will be prefixed with

   438   meta-equality. Now exporting the theorem \<open>eq'\<close> from \<open>ctxt1\<close> to \<open>ctxt0\<close> means @{term "y \<equiv> x"} will be prefixed with

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

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

   440   Assumption} indicates whether the assumptions should be marked with

   440   Assumption} indicates whether the assumptions should be marked with

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

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

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

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

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

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

   446   Section~\ref{sec:structured}.

   446   Section~\ref{sec:structured}.

   447 

   447 

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

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

   451   in the following example.

   451   in the following example.

   452 

   452 

   454   "let

   454   "let

   455   val ctxt0 = @{context}

   455   val ctxt0 = @{context}

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

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

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

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

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

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

   587   On the ML-level of Isabelle, you often have to work with qualified names.

   587   On the ML-level of Isabelle, you often have to work with qualified names.

   588   These are strings with some additional information, such as positional

   588   These are strings with some additional information, such as positional

   589   information and qualifiers. Such qualified names can be generated with the

   589   information and qualifiers. Such qualified names can be generated with the

   590   antiquotation \<open>@{binding \<dots>}\<close>. For example

   590   antiquotation \<open>@{binding \<dots>}\<close>. For example

   591 

   591 

   593   "@{binding \"name\"}"

   593   "@{binding \"name\"}"

   594   "name"}

   594   "name"}

   595 

   595 

   596   An example where a qualified name is needed is the function 

   596   An example where a qualified name is needed is the function 

   597   @{ML_ind define in Local_Theory}.  This function is used below to define 

   597   @{ML_ind define in Local_Theory}.  This function is used below to define 

   632   section and link with the comment in the antiquotation section.}

   632   section and link with the comment in the antiquotation section.}

   633 

   633 

   634   Occasionally you have to calculate what the ``base'' name of a given

   634   Occasionally you have to calculate what the ``base'' name of a given

   635   constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:

   635   constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:

   636 

   636 

   638 

   638 

   639   \begin{readmore}

   639   \begin{readmore}

   640   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

   640   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};

   641   functions about signatures in @{ML_file "Pure/sign.ML"}.

   641   functions about signatures in @{ML_file "Pure/sign.ML"}.

   642   \end{readmore}

   642   \end{readmore}