--- a/ProgTutorial/Advanced.thy Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Advanced.thy Thu May 16 19:56:12 2019 +0200
@@ -59,7 +59,7 @@
Functions acting on theories often end with the suffix \<open>_global\<close>,
for example the function @{ML read_term_global in Syntax} in the structure
- @{ML_struct Syntax}. The reason is to set them syntactically apart from
+ @{ML_structure Syntax}. The reason is to set them syntactically apart from
functions acting on contexts or local theories, which will be discussed in
the next sections. There is a tendency amongst Isabelle developers to prefer
``non-global'' operations, because they have some advantages, as we will also
@@ -74,7 +74,7 @@
the theory where the attribute has been registered or the theorem has been
stored. This is a fundamental principle in Isabelle. A similar situation
arises with declaring a constant, which can be done on the ML-level with
- function @{ML_ind declare_const in Sign} from the structure @{ML_struct
+ function @{ML_ind declare_const in Sign} from the structure @{ML_structure
Sign}. To see how \isacommand{setup} works, consider the following code:
\<close>
@@ -176,7 +176,7 @@
the variables are fixed. For this remember that ML-code inside a proof
needs to be enclosed inside \isacommand{ML\_prf}~\<open>\<verbopen> \<dots> \<verbclose>\<close>,
not \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close>. The function
- @{ML_ind dest_fixes in Variable} from the structure @{ML_struct Variable} takes
+ @{ML_ind dest_fixes in Variable} from the structure @{ML_structure Variable} takes
a context and returns all its currently fixed variable (names). That
means a context has a dataslot containing information about fixed variables.
The ML-antiquotation \<open>@{context}\<close> points to the context that is
@@ -252,16 +252,16 @@
of fixed variables is actually quite useful. For example it prevents us from
fixing a variable twice
- @{ML_response_fake [gray, display]
+ @{ML_matchresult_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 names for
fixed variables. For this you have to use the function @{ML_ind
- variant_fixes in Variable} from the structure @{ML_struct Variable}.
+ variant_fixes in Variable} from the structure @{ML_structure Variable}.
- @{ML_response_fake [gray, display]
+ @{ML_matchresult_fake [gray, display]
"@{context}
|> Variable.variant_fixes [\"y\", \"y\", \"z\"]"
"([\"y\", \"ya\", \"z\"], ...)"}
@@ -273,7 +273,7 @@
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]
+ @{ML_matchresult_fake [display, gray, linenos]
"let
val ctxt0 = @{context}
val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
@@ -291,9 +291,9 @@
Often one has the problem that given some terms, create fresh variables
avoiding any variable occurring in those terms. For this you can use the
- function @{ML_ind declare_term in Variable} from the structure @{ML_struct Variable}.
+ function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
- @{ML_response_fake [gray, display]
+ @{ML_matchresult_fake [gray, display]
"let
val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
val frees = replicate 2 (\"x\", @{typ nat})
@@ -327,9 +327,9 @@
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_structure Syntax}. Consider the following code:
- @{ML_response_fake [gray, display]
+ @{ML_matchresult_fake [gray, display]
"let
val ctxt0 = @{context}
val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
@@ -345,7 +345,7 @@
type the parsed term receives depends upon the last declaration that
is made, as the next example illustrates.
- @{ML_response_fake [gray, display]
+ @{ML_matchresult_fake [gray, display]
"let
val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
@@ -379,7 +379,7 @@
In Line 3 we fix the variables @{term x}, @{term y} and @{term z} in
context \<open>ctxt1\<close>. The function @{ML_ind export_terms in
- Variable} from the structure @{ML_struct Variable} can be used to transfer
+ Variable} from the structure @{ML_structure 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
@@ -396,11 +396,11 @@
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
+ structure @{ML_structure 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]
+ @{ML_matchresult_fake [display, gray]
"let
val thy = @{theory}
val ctxt0 = @{context}
@@ -416,9 +416,9 @@
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_structure Assumption}. Consider the following code.
- @{ML_response_fake [display, gray, linenos]
+ @{ML_matchresult_fake [display, gray, linenos]
"let
val ctxt0 = @{context}
val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
@@ -429,11 +429,11 @@
"x \<equiv> y \<Longrightarrow> y \<equiv> x"}
The function @{ML_ind add_assumes in Assumption} from the structure
- @{ML_struct Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
+ @{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
to the context \<open>ctxt1\<close> (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
+ function @{ML_ind symmetric in Thm} from the structure @{ML_structure
Thm} in order to obtain the symmetric version of the assumed
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
the assumed theorem. The boolean flag in @{ML_ind export in
@@ -446,11 +446,11 @@
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
+ @{ML_structure Proof_Context} combines both export functions from
+ @{ML_structure Variable} and @{ML_structure Assumption}. This can be seen
in the following example.
- @{ML_response_fake [display, gray]
+ @{ML_matchresult_fake [display, gray]
"let
val ctxt0 = @{context}
val ((fvs, [eq]), ctxt1) = ctxt0
@@ -589,7 +589,7 @@
information and qualifiers. Such qualified names can be generated with the
antiquotation \<open>@{binding \<dots>}\<close>. For example
- @{ML_response [display,gray]
+ @{ML_matchresult [display,gray]
"@{binding \"name\"}"
"name"}
@@ -634,7 +634,7 @@
Occasionally you have to calculate what the ``base'' name of a given
constant is. For this you can use the function @{ML_ind Long_Name.base_name}. For example:
- @{ML_response [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
+ @{ML_matchresult [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
\begin{readmore}
Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};