--- a/ProgTutorial/Base.thy Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/Base.thy Thu Aug 20 14:19:39 2009 +0200
@@ -39,7 +39,8 @@
ML {*
fun open_file name =
(tracing ("Opened File: " ^ name);
- file_name := SOME name)
+ file_name := SOME name;
+ TextIO.openOut name; ())
fun open_file_prelude name txt =
(open_file name; write_file (txt ^ "\n"))
--- a/ProgTutorial/FirstSteps.thy Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Thu Aug 20 14:19:39 2009 +0200
@@ -115,7 +115,7 @@
text {*
During development you might find it necessary to inspect some data in your
code. This can be done in a ``quick-and-dirty'' fashion using the function
- @{ML [index] "writeln"}. For example
+ @{ML_ind [index] "writeln"}. For example
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
@@ -123,7 +123,7 @@
Isabelle. This function expects a string as argument. If you develop under
PolyML, then there is a convenient, though again ``quick-and-dirty'', method
for converting values into strings, namely the function
- @{ML [index] makestring in PolyML}:
+ @{ML_ind [index] makestring in PolyML}:
@{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""}
@@ -133,7 +133,7 @@
The function @{ML "writeln"} should only be used for testing purposes,
because any output this function generates will be overwritten as soon as an
error is raised. For printing anything more serious and elaborate, the
- function @{ML [index] tracing} is more appropriate. This function writes all
+ function @{ML_ind [index] tracing} is more appropriate. This function writes all
output into a separate tracing buffer. For example:
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
@@ -166,7 +166,7 @@
will cause that all tracing information is printed into the file @{text "foo.bar"}.
- You can print out error messages with the function @{ML [index] error}; for
+ You can print out error messages with the function @{ML_ind [index] error}; for
example:
@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
@@ -177,8 +177,8 @@
be displayed by the infrastructure.
- (FIXME Mention how to work with @{ML [index] debug in Toplevel} and
- @{ML [index] profiling in Toplevel}.)
+ (FIXME Mention how to work with @{ML_ind [index] debug in Toplevel} and
+ @{ML_ind [index] profiling in Toplevel}.)
*}
(*
@@ -201,7 +201,7 @@
thm}. Isabelle contains elaborate pretty-printing functions for printing
them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
are a bit unwieldy. One way to transform a term into a string is to use the
- function @{ML [index] string_of_term in Syntax} in structure @{ML_struct
+ function @{ML_ind [index] string_of_term in Syntax} in structure @{ML_struct
Syntax}, which we bind for more convenience to the toplevel.
*}
@@ -216,7 +216,7 @@
This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
additional information encoded in it. The string can be properly printed by
- using either the function @{ML [index] writeln} or @{ML [index] tracing}:
+ using either the function @{ML_ind [index] writeln} or @{ML_ind [index] tracing}:
@{ML_response_fake [display,gray]
"writeln (string_of_term @{context} @{term \"1::nat\"})"
@@ -229,7 +229,7 @@
"\"1\""}
If there are more than one @{ML_type term}s to be printed, you can use the
- function @{ML [index] commas} to separate them.
+ function @{ML_ind [index] commas} to separate them.
*}
ML{*fun string_of_terms ctxt ts =
@@ -243,9 +243,9 @@
string_of_term ctxt (term_of ct)*}
text {*
- In this example the function @{ML [index] term_of} extracts the @{ML_type
+ In this example the function @{ML_ind [index] term_of} extracts the @{ML_type
term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be
- printed with @{ML [index] commas}.
+ printed with @{ML_ind [index] commas}.
*}
ML{*fun string_of_cterms ctxt cts =
@@ -253,7 +253,7 @@
text {*
The easiest way to get the string of a theorem is to transform it
- into a @{ML_type cterm} using the function @{ML [index] crep_thm}.
+ into a @{ML_type cterm} using the function @{ML_ind [index] crep_thm}.
*}
ML{*fun string_of_thm ctxt thm =
@@ -272,7 +272,7 @@
However, in order to improve the readability when printing theorems, we
convert these schematic variables into free variables using the function
- @{ML [index] import in Variable}. This is similar to statements like @{text
+ @{ML_ind [index] import in Variable}. This is similar to statements like @{text
"conjI[no_vars]"} from Isabelle's user-level.
*}
@@ -322,7 +322,7 @@
and second half."}
To ease this kind of string manipulations, there are a number
- of library functions. For example, the function @{ML [index] cat_lines}
+ of library functions. For example, the function @{ML_ind [index] cat_lines}
concatenates a list of strings and inserts newlines.
@{ML_response [display, gray]
@@ -342,21 +342,21 @@
comprehension of the code, but after getting familiar with them, they
actually ease the understanding and also the programming.
- The simplest combinator is @{ML [index] I}, which is just the identity function defined as
+ The simplest combinator is @{ML_ind [index] I}, which is just the identity function defined as
*}
ML{*fun I x = x*}
-text {* Another simple combinator is @{ML [index] K}, defined as *}
+text {* Another simple combinator is @{ML_ind [index] K}, defined as *}
ML{*fun K x = fn _ => x*}
text {*
- @{ML [index] K} ``wraps'' a function around the argument @{text "x"}. However, this
+ @{ML_ind [index] K} ``wraps'' a function around the argument @{text "x"}. However, this
function ignores its argument. As a result, @{ML K} defines a constant function
always returning @{text x}.
- The next combinator is reverse application, @{ML [index] "|>"}, defined as:
+ The next combinator is reverse application, @{ML_ind [index] "|>"}, defined as:
*}
ML{*fun x |> f = f x*}
@@ -434,15 +434,15 @@
"P z za zb"}
You can read off this behaviour from how @{ML apply_fresh_args} is
- coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the
- term; @{ML [index] binder_types} in the next line produces the list of argument
+ coded: in Line 2, the function @{ML_ind [index] fastype_of} calculates the type of the
+ term; @{ML_ind [index] binder_types} in the next line produces the list of argument
types (in the case above the list @{text "[nat, int, unit]"}); Line 4
pairs up each type with the string @{text "z"}; the
- function @{ML [index] variant_frees in Variable} generates for each @{text "z"} a
+ function @{ML_ind [index] variant_frees in Variable} generates for each @{text "z"} a
unique name avoiding the given @{text f}; the list of name-type pairs is turned
into a list of variable terms in Line 6, which in the last line is applied
- by the function @{ML [index] list_comb} to the term. In this last step we have to
- use the function @{ML [index] curry}, because @{ML [index] list_comb} expects the
+ by the function @{ML_ind [index] list_comb} to the term. In this last step we have to
+ use the function @{ML_ind [index] curry}, because @{ML_ind [index] list_comb} expects the
function and the variables list as a pair. This kind of functions is often needed when
constructing terms with fresh variables. The infrastructure helps tremendously
to avoid any name clashes. Consider for example:
@@ -460,7 +460,7 @@
where the @{text "za"} is correctly avoided.
- The combinator @{ML [index] "#>"} is the reverse function composition. It can be
+ The combinator @{ML_ind [index] "#>"} is the reverse function composition. It can be
used to define the following function
*}
@@ -475,7 +475,7 @@
composition allows you to read the code top-down.
The remaining combinators described in this section add convenience for the
- ``waterfall method'' of writing functions. The combinator @{ML [index] tap} allows
+ ``waterfall method'' of writing functions. The combinator @{ML_ind [index] tap} allows
you to get hold of an intermediate result (to do some side-calculations for
instance). The function
@@ -488,13 +488,13 @@
text {*
increments the argument first by @{text "1"} and then by @{text "2"}. In the
- middle (Line 3), however, it uses @{ML [index] tap} for printing the ``plus-one''
- intermediate result inside the tracing buffer. The function @{ML [index] tap} can
+ middle (Line 3), however, it uses @{ML_ind [index] tap} for printing the ``plus-one''
+ intermediate result inside the tracing buffer. The function @{ML_ind [index] tap} can
only be used for side-calculations, because any value that is computed
cannot be merged back into the ``main waterfall''. To do this, you can use
the next combinator.
- The combinator @{ML [index] "`"} (a backtick) is similar to @{ML tap}, but applies a
+ The combinator @{ML_ind [index] "`"} (a backtick) is similar to @{ML tap}, but applies a
function to the value and returns the result together with the value (as a
pair). For example the function
*}
@@ -509,7 +509,7 @@
for x}. After that, the function increments the right-hand component of the
pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
- The combinators @{ML [index] "|>>"} and @{ML [index] "||>"} are defined for
+ The combinators @{ML_ind [index] "|>>"} and @{ML_ind [index] "||>"} are defined for
functions manipulating pairs. The first applies the function to
the first component of the pair, defined as
*}
@@ -556,7 +556,7 @@
conciseness is only small, in more complicated situations the benefit of
avoiding @{text "lets"} can be substantial.
- With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair.
+ With the combinator @{ML_ind [index] "|->"} you can re-combine the elements from a pair.
This combinator is defined as
*}
@@ -572,10 +572,10 @@
|-> (fn x => fn y => x + y)*}
text {*
- The combinator @{ML [index] ||>>} plays a central rôle whenever your task is to update a
+ The combinator @{ML_ind [index] ||>>} plays a central rôle whenever your task is to update a
theory and the update also produces a side-result (for example a theorem). Functions
for such tasks return a pair whose second component is the theory and the fist
- component is the side-result. Using @{ML [index] ||>>}, you can do conveniently the update
+ component is the side-result. Using @{ML_ind [index] ||>>}, you can do conveniently the update
and also accumulate the side-results. Consider the following simple function.
*}
@@ -587,7 +587,7 @@
text {*
The purpose of Line 2 is to just pair up the argument with a dummy value (since
- @{ML [index] "||>>"} operates on pairs). Each of the next three lines just increment
+ @{ML_ind [index] "||>>"} operates on pairs). Each of the next three lines just increment
the value by one, but also nest the intermediate results to the left. For example
@{ML_response [display,gray]
@@ -604,14 +604,14 @@
*}
text {*
- Recall that @{ML [index] "|>"} is the reverse function application. Recall also that
+ Recall that @{ML_ind [index] "|>"} is the reverse function application. Recall also that
the related
- reverse function composition is @{ML [index] "#>"}. In fact all the combinators
- @{ML [index] "|->"}, @{ML [index] "|>>"} , @{ML [index] "||>"} and @{ML [index]
+ reverse function composition is @{ML_ind [index] "#>"}. In fact all the combinators
+ @{ML_ind [index] "|->"}, @{ML_ind [index] "|>>"} , @{ML_ind [index] "||>"} and @{ML_ind [index]
"||>>"} described above have related combinators for
- function composition, namely @{ML [index] "#->"}, @{ML [index] "#>>"},
- @{ML [index] "##>"} and @{ML [index] "##>>"}.
- Using @{ML [index] "#->"}, for example, the function @{text double} can also be written as:
+ function composition, namely @{ML_ind [index] "#->"}, @{ML_ind [index] "#>>"},
+ @{ML_ind [index] "##>"} and @{ML_ind [index] "##>>"}.
+ Using @{ML_ind [index] "#->"}, for example, the function @{text double} can also be written as:
*}
ML{*val double =
@@ -627,7 +627,7 @@
list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
plumbing is also needed in situations where a functions operate over lists,
but one calculates only with a single entity. An example is the function
- @{ML [index] check_terms in Syntax}, whose purpose is to type-check a list
+ @{ML_ind [index] check_terms in Syntax}, whose purpose is to type-check a list
of terms.
@{ML_response_fake [display, gray]
@@ -690,7 +690,7 @@
where @{text "@{theory}"} is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory
@{text FirstSteps}). The name of this theory can be extracted using
- the function @{ML [index] theory_name in Context}.
+ the function @{ML_ind [index] theory_name in Context}.
Note, however, that antiquotations are statically linked, that is their value is
determined at ``compile-time'', not ``run-time''. For example the function
@@ -738,7 +738,7 @@
end*}
text {*
- The function @{ML [index] dest_ss in MetaSimplifier} returns a record containing all
+ The function @{ML_ind [index] dest_ss in MetaSimplifier} returns a record containing all
information stored in the simpset, but we are only interested in the names of the
simp-rules. Now you can feed in the current simpset into this function.
The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
@@ -752,16 +752,16 @@
code.
On the ML-level of Isabelle, you often have to work with qualified names.
- These are strings with some additional information, such as positional information
- and qualifiers. Such qualified names can be generated with the antiquotation
- @{text "@{binding \<dots>}"}. For example
+ These are strings with some additional information, such as positional
+ information and qualifiers. Such qualified names can be generated with the
+ antiquotation @{text "@{binding \<dots>}"}. For example
@{ML_response [display,gray]
"@{binding \"name\"}"
"name"}
An example where a qualified name is needed is the function
- @{ML [index] define in LocalTheory}. This function is used below to define
+ @{ML_ind [index] define in LocalTheory}. This function is used below to define
the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
@@ -783,13 +783,13 @@
why @{ML snd} is needed)
It is also possible to define your own antiquotations. But you should
- exercise care when introducing new ones, as they can also make your
- code also difficult to read. In the next section we will see how the (build in)
- antiquotation @{text "@{term \<dots>}"} can be used to construct terms.
- A restriction of this antiquotation is that it does not allow you to
- use schematic variables. If you want to have an antiquotation that does not
- have this restriction, you can implement your own using the
- function @{ML [index] ML_Antiquote.inline}. The code is as follows.
+ exercise care when introducing new ones, as they can also make your code
+ also difficult to read. In the next section we will see how the (build in)
+ antiquotation @{text "@{term \<dots>}"} can be used to construct terms. A
+ restriction of this antiquotation is that it does not allow you to use
+ schematic variables. If you want to have an antiquotation that does not have
+ this restriction, you can implement your own using the function @{ML_ind [index]
+ ML_Antiquote.inline}. The code is as follows.
*}
ML %linenosgray{*ML_Antiquote.inline "term_pat"
@@ -801,7 +801,7 @@
text {*
The parser in Line 2 provides us with a context and a string; this string is
- transformed into a term using the function @{ML [index] read_term_pattern in
+ transformed into a term using the function @{ML_ind [index] read_term_pattern in
ProofContext} (Line 4); the next two lines print the term so that the
ML-system can understand them. An example of this antiquotation is as
follows.
@@ -879,8 +879,6 @@
@{ML Free} and written on the user level in blue colour) and
\emph{schematic} variables (term-constructor @{ML Var} and written with a
leading question mark). Consider the following two examples
-
-
@{ML_response_fake [display, gray]
"let
@@ -1047,7 +1045,7 @@
(Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
There are a number of handy functions that are frequently used for
- constructing terms. One is the function @{ML [index] list_comb}, which takes a term
+ constructing terms. One is the function @{ML_ind [index] list_comb}, which takes a term
and a list of terms as arguments, and produces as output the term
list applied to the term. For example
@@ -1060,7 +1058,7 @@
end"
"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
- Another handy function is @{ML [index] lambda}, which abstracts a variable
+ Another handy function is @{ML_ind [index] lambda}, which abstracts a variable
in a term. For example
@{ML_response_fake [display,gray]
@@ -1093,7 +1091,7 @@
of Church-style typing, where variables with the same name still differ, if they
have different type.
- There is also the function @{ML [index] subst_free} with which terms can be
+ There is also the function @{ML_ind [index] subst_free} with which terms can be
replaced by other terms. For example below, we will replace in @{term
"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
@{term y}, and @{term x} by @{term True}.
@@ -1120,7 +1118,7 @@
end"
"Free (\"x\", \"nat\")"}
- Similarly the function @{ML [index] subst_bounds}, replaces lose bound
+ Similarly the function @{ML_ind [index] subst_bounds}, replaces lose bound
variables with terms. To see how this function works, let us implement a
function that strips off the outermost quantifiers in a term.
*}
@@ -1138,8 +1136,9 @@
"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
- With the function @{ML subst_bounds}, you can replace the lose
- @{ML [index] Bound}s with the stripped off variables.
+ After calling @{ML strip_alls}, you obtain a term with lose bound variables. With
+ the function @{ML subst_bounds}, you can replace these lose @{ML_ind [index]
+ Bound}s with the stripped off variables.
@{ML_response_fake [display, gray, linenos]
"let
@@ -1157,7 +1156,7 @@
and so on.
There are many convenient functions that construct specific HOL-terms. For
- example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms.
+ example @{ML_ind [index] mk_eq in HOLogic} constructs an equality out of two terms.
The types needed in this equality are calculated from the type of the
arguments. For example
@@ -1173,8 +1172,9 @@
text {*
\begin{readmore}
- Most of the HOL-specific operations on terms and types are defined
- in @{ML_file "HOL/Tools/hologic.ML"}.
+ There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
+ "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual
+ constructions of terms and types easier.
\end{readmore}
When constructing terms manually, there are a few subtle issues with
@@ -1261,12 +1261,6 @@
| is_nil_or_all _ = false *}
text {*
- \begin{readmore}
- There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file "Pure/logic.ML"} and
- @{ML_file "HOL/Tools/hologic.ML"} that make such manual constructions of terms
- and types easier.
- \end{readmore}
-
The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
For example
@@ -1276,8 +1270,8 @@
(FIXME: Explain the following better.)
Occasionally you have to calculate what the ``base'' name of a given
- constant is. For this you can use the function @{ML [index] "Sign.extern_const"} or
- @{ML [index] Long_Name.base_name}. For example:
+ constant is. For this you can use the function @{ML_ind [index] "Sign.extern_const"} or
+ @{ML_ind [index] Long_Name.base_name}. For example:
@{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
@@ -1299,19 +1293,19 @@
ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-text {* This can be equally written with the combinator @{ML [index] "-->"} as: *}
+text {* This can be equally written with the combinator @{ML_ind [index] "-->"} as: *}
ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
text {*
If you want to construct a function type with more than one argument
- type, then you can use @{ML [index] "--->"}.
+ type, then you can use @{ML_ind [index] "--->"}.
*}
ML{*fun make_fun_types tys ty = tys ---> ty *}
text {*
- A handy function for manipulating terms is @{ML [index] map_types}: it takes a
+ A handy function for manipulating terms is @{ML_ind [index] map_types}: it takes a
function and applies it to every type in a term. You can, for example,
change every @{typ nat} in a term into an @{typ int} using the function:
*}
@@ -1331,8 +1325,8 @@
$ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
If you want to obtain the list of free type-variables of a term, you
- can use the function @{ML [index] add_tfrees in Term}
- (similarly @{ML [index] add_tvars in Term} for the schematic type-variables).
+ can use the function @{ML_ind [index] add_tfrees in Term}
+ (similarly @{ML_ind [index] add_tvars in Term} for the schematic type-variables).
One would expect that such functions
take a term as input and return a list of types. But their type is actually
@@ -1401,7 +1395,7 @@
You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
typ}es, since they are just arbitrary unchecked trees. However, you
eventually want to see if a term is well-formed, or type-checks, relative to
- a theory. Type-checking is done via the function @{ML [index] cterm_of}, which
+ a theory. Type-checking is done via the function @{ML_ind [index] cterm_of}, which
converts a @{ML_type [index] term} into a @{ML_type [index] cterm}, a \emph{certified}
term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
abstract objects that are guaranteed to be type-correct, and they can only
@@ -1453,17 +1447,10 @@
the file @{ML_file "Pure/thm.ML"}.
\end{readmore}
- \begin{exercise}
- Check that the function defined in Exercise~\ref{fun:revsum} returns a
- result that type-checks. See what happens to the solutions of this
- exercise given in \ref{ch:solutions} when they receive an ill-typed term
- as input.
- \end{exercise}
-
Remember Isabelle follows the Church-style typing for terms, i.e., a term contains
enough typing information (constants, free variables and abstractions all have typing
information) so that it is always clear what the type of a term is.
- Given a well-typed term, the function @{ML [index] type_of} returns the
+ Given a well-typed term, the function @{ML_ind [index] type_of} returns the
type of a term. Consider for example:
@{ML_response [display,gray]
@@ -1478,7 +1465,7 @@
"*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
Since the complete traversal might sometimes be too costly and
- not necessary, there is the function @{ML [index] fastype_of}, which
+ not necessary, there is the function @{ML_ind [index] fastype_of}, which
also returns the type of a term.
@{ML_response [display,gray]
@@ -1495,7 +1482,7 @@
Sometimes it is a bit inconvenient to construct a term with
complete typing annotations, especially in cases where the typing
information is redundant. A short-cut is to use the ``place-holder''
- type @{ML [index] dummyT} and then let type-inference figure out the
+ type @{ML_ind [index] dummyT} and then let type-inference figure out the
complete type. An example is as follows:
@{ML_response_fake [display,gray]
@@ -1520,6 +1507,13 @@
\end{readmore}
(FIXME: say something about sorts)
+
+ \begin{exercise}
+ Check that the function defined in Exercise~\ref{fun:revsum} returns a
+ result that type-checks. See what happens to the solutions of this
+ exercise given in \ref{ch:solutions} when they receive an ill-typed term
+ as input.
+ \end{exercise}
*}
@@ -1585,7 +1579,7 @@
@{ML_file "Pure/thm.ML"}.
\end{readmore}
- (FIXME: handy functions working on theorems, like @{ML [index] rulify in ObjectLogic} and so on)
+ (FIXME: handy functions working on theorems, like @{ML_ind [index] rulify in ObjectLogic} and so on)
(FIXME: how to add case-names to goal states - maybe in the
next section)
@@ -1612,7 +1606,7 @@
strip_assums_all ([], @{term "\<And>x y. A x y"})
*}
-setup {*
+setup %gray {*
TermStyle.add_style "no_all_prem1" (style_parm_premise 1) #>
TermStyle.add_style "no_all_prem2" (style_parm_premise 2)
*}
@@ -1629,7 +1623,7 @@
This is a fundamental principle in Isabelle. A similar situation occurs
for example with declaring constants. The function that declares a
- constant on the ML-level is @{ML [index] add_consts_i in Sign}.
+ constant on the ML-level is @{ML_ind [index] add_consts_i in Sign}.
If you write\footnote{Recall that ML-code needs to be
enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
*}
@@ -1707,10 +1701,10 @@
ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
text {*
- where the function @{ML [index] rule_attribute in Thm} expects a function taking a
+ where the function @{ML_ind [index] rule_attribute in Thm} expects a function taking a
context (which we ignore in the code above) and a theorem (@{text thm}), and
returns another theorem (namely @{text thm} resolved with the theorem
- @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML [index] RS}
+ @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML_ind [index] "RS"}
is explained in Section~\ref{sec:simpletacs}.} The function
@{ML rule_attribute in Thm} then returns an attribute.
@@ -1747,7 +1741,7 @@
@{text "> "}~@{thm test[my_sym]}
\end{isabelle}
- An alternative for setting up an attribute is the function @{ML [index] setup in Attrib}.
+ An alternative for setting up an attribute is the function @{ML_ind [index] setup in Attrib}.
So instead of using \isacommand{attribute\_setup}, you can also set up the
attribute as follows:
*}
@@ -1812,10 +1806,10 @@
you get an exception indicating that the theorem @{thm [source] sym}
does not resolve with meta-equations.
- The purpose of @{ML [index] rule_attribute in Thm} is to directly manipulate theorems.
+ The purpose of @{ML_ind [index] rule_attribute in Thm} is to directly manipulate theorems.
Another usage of theorem attributes is to add and delete theorems from stored data.
For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
- current simpset. For these applications, you can use @{ML [index] declaration_attribute in Thm}.
+ current simpset. For these applications, you can use @{ML_ind [index] declaration_attribute in Thm}.
To illustrate this function, let us introduce a reference containing a list
of theorems.
*}
@@ -1844,9 +1838,9 @@
These functions take a theorem and a context and, for what we are explaining
here it is sufficient that they just return the context unchanged. They change
however the reference @{ML my_thms}, whereby the function
- @{ML [index] add_thm in Thm} adds a theorem if it is not already included in
- the list, and @{ML [index] del_thm in Thm} deletes one (both functions use the
- predicate @{ML [index] eq_thm_prop in Thm}, which compares theorems according to
+ @{ML_ind [index] add_thm in Thm} adds a theorem if it is not already included in
+ the list, and @{ML_ind [index] del_thm in Thm} deletes one (both functions use the
+ predicate @{ML_ind [index] eq_thm_prop in Thm}, which compares theorems according to
their proved propositions modulo alpha-equivalence).
You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into
@@ -1864,7 +1858,7 @@
"maintaining a list of my_thms - rough test only!"
text {*
- The parser @{ML [index] add_del in Attrib} is a predefined parser for
+ The parser @{ML_ind [index] add_del in Attrib} is a predefined parser for
adding and deleting lemmas. Now if you prove the next lemma
and attach to it the attribute @{text "[my_thms]"}
*}
@@ -1892,7 +1886,7 @@
"[\"True\", \"Suc (Suc 0) = 2\"]"}
The theorem @{thm [source] trueI_2} only appears once, since the
- function @{ML [index] add_thm in Thm} tests for duplicates, before extending
+ function @{ML_ind [index] add_thm in Thm} tests for duplicates, before extending
the list. Deletion from the list works as follows:
*}
@@ -1904,7 +1898,7 @@
"!my_thms"
"[\"True\"]"}
- We used in this example two functions declared as @{ML [index] declaration_attribute in Thm},
+ We used in this example two functions declared as @{ML_ind [index] declaration_attribute in Thm},
but there can be any number of them. We just have to change the parser for reading
the arguments accordingly.
@@ -2133,9 +2127,9 @@
section {* Storing Theorems\label{sec:storing} (TBD) *}
-text {* @{ML [index] add_thms_dynamic in PureThy} *}
-
-local_setup {*
+text {* @{ML_ind [index] add_thms_dynamic in PureThy} *}
+
+local_setup %gray {*
LocalTheory.note Thm.theoremK
((@{binding "allI_alt"}, []), [@{thm allI}]) #> snd *}
@@ -2192,7 +2186,7 @@
occur in case the text wraps over a line, or with how much indentation a
text should be printed. However, if you want to actually output the
formatted text, you have to transform the pretty type back into a @{ML_type
- string}. This can be done with the function @{ML [index] string_of in Pretty}. In what
+ string}. This can be done with the function @{ML_ind [index] string_of in Pretty}. In what
follows we will use the following wrapper function for printing a pretty
type:
*}
@@ -2237,10 +2231,10 @@
However by using pretty types you have the ability to indicate a possible
line break for example at each space. You can achieve this with the function
- @{ML [index] breaks in Pretty}, which expects a list of pretty types and inserts a
+ @{ML_ind [index] breaks in Pretty}, which expects a list of pretty types and inserts a
possible line break in between every two elements in this list. To print
this list of pretty types as a single string, we concatenate them
- with the function @{ML [index] blk in Pretty} as follows:
+ with the function @{ML_ind [index] blk in Pretty} as follows:
@{ML_response_fake [display,gray]
@@ -2255,7 +2249,7 @@
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
Here the layout of @{ML test_str} is much more pleasing to the
- eye. The @{ML "0"} in @{ML [index] blk in Pretty} stands for no indentation
+ eye. The @{ML "0"} in @{ML_ind [index] blk in Pretty} stands for no indentation
of the printed string. You can increase the indentation and obtain
@{ML_response_fake [display,gray]
@@ -2271,7 +2265,7 @@
where starting from the second line the indent is 3. If you want
that every line starts with the same indent, you can use the
- function @{ML [index] indent in Pretty} as follows:
+ function @{ML_ind [index] indent in Pretty} as follows:
@{ML_response_fake [display,gray]
"let
@@ -2286,7 +2280,7 @@
If you want to print out a list of items separated by commas and
have the linebreaks handled properly, you can use the function
- @{ML [index] commas in Pretty}. For example
+ @{ML_ind [index] commas in Pretty}. For example
@{ML_response_fake [display,gray]
"let
@@ -2301,7 +2295,7 @@
where @{ML upto} generates a list of integers. You can print out this
list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
@{text [quotes] "}"}, and separated by commas using the function
- @{ML [index] enum in Pretty}. For example
+ @{ML_ind [index] enum in Pretty}. For example
*}
text {*
@@ -2372,8 +2366,8 @@
text {*
In Line 3 we define a function that inserts possible linebreaks in places
where a space is. In Lines 4 and 5 we pretty-print the term and its type
- using the functions @{ML [index] pretty_term in Syntax} and @{ML [index]
- pretty_typ in Syntax}. We also use the function @{ML [index] quote in
+ using the functions @{ML_ind [index] pretty_term in Syntax} and @{ML_ind [index]
+ pretty_typ in Syntax}. We also use the function @{ML_ind [index] quote in
Pretty} in order to enclose the term and type inside quotation marks. In
Line 9 we add a period right after the type without the possibility of a
line break, because we do not want that a line break occurs there.
@@ -2460,7 +2454,7 @@
"foo")) state
*}
-setup {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
+setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
lemma "False"
oops
--- a/ProgTutorial/Package/Ind_Code.thy Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy Thu Aug 20 14:19:39 2009 +0200
@@ -21,7 +21,7 @@
and then ``register'' the definition inside a local theory.
To do the latter, we use the following wrapper for the function
- @{ML [index] define in LocalTheory}. The wrapper takes a predicate name, a syntax
+ @{ML_ind [index] define in LocalTheory}. The wrapper takes a predicate name, a syntax
annotation and a term representing the right-hand side of the definition.
*}
@@ -35,12 +35,12 @@
text {*
It returns the definition (as a theorem) and the local theory in which the
- definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
- attached to the theorem (other possibile flags are @{ML [index] definitionK in Thm}
- and @{ML [index] axiomK in Thm}). These flags just classify theorems and have no
+ definition has been made. In Line 4, @{ML_ind [index] internalK in Thm} is a flag
+ attached to the theorem (other possibile flags are @{ML_ind [index] definitionK in Thm}
+ and @{ML_ind [index] axiomK in Thm}). These flags just classify theorems and have no
significant meaning, except for tools that, for example, find theorems in
the theorem database.\footnote{FIXME: put in the section about theorems.} We
- also use @{ML [index] empty_binding in Attrib} in Line 3, since the definitions for
+ also use @{ML_ind [index] empty_binding in Attrib} in Line 3, since the definitions for
our inductive predicates are not meant to be seen by the user and therefore
do not need to have any theorem attributes. A testcase for this function is
*}
@@ -173,9 +173,9 @@
meta-quanti\-fications. In Line 4, we transform these introduction rules
into the object logic (since definitions cannot be stated with
meta-connectives). To do this transformation we have to obtain the theory
- behind the local theory using the function @{ML [index] theory_of in ProofContext}
+ behind the local theory using the function @{ML_ind [index] theory_of in ProofContext}
(Line 3); with this theory we can use the function
- @{ML [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
+ @{ML_ind [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
to @{ML defn_aux} in Line 5 produces all right-hand sides of the
definitions. The actual definitions are then made in Line 7. The result of
the function is a list of theorems and a local theory (the theorems are
@@ -379,7 +379,7 @@
the Isabelle's goal mechanism will fail.\footnote{FIXME: check with
Stefan...is this so?}
- In Line 11 we set up the goal to be proved using the function @{ML [index]
+ In Line 11 we set up the goal to be proved using the function @{ML_ind [index]
prove in Goal}; in the next line we call the tactic for proving the
induction principle. As mentioned before, this tactic expects the
definitions, the premise and the (certified) predicates with which the
@@ -447,7 +447,7 @@
the new predicates. In Line 8, we construct the types of these new predicates
using the given argument types. Next we turn them into terms and subsequently
certify them (Line 9 and 10). We can now produce the substituted introduction rules
- (Line 11) using the function @{ML [index] subst_free}. Line 14 and 15 just iterate
+ (Line 11) using the function @{ML_ind [index] subst_free}. Line 14 and 15 just iterate
the proofs for all predicates.
From this we obtain a list of theorems. Finally we need to export the
fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"}
@@ -593,12 +593,12 @@
differently. In the code below we will therefore separate them into @{text
"params1"} and @{text params2}, respectively @{text "prems1"} and @{text
"prems2"}. To do this separation, it is best to open a subproof with the
- tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as
+ tactic @{ML_ind [index] SUBPROOF}, since this tactic provides us with the parameters (as
list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s).
The problem with @{ML SUBPROOF}, however, is that it always expects us to
completely discharge the goal (see Section~\ref{sec:simpletacs}). This is
a bit inconvenient for our gradual explanation of the proof here. Therefore
- we use first the function @{ML [index] FOCUS in Subgoal}, which does s
+ we use first the function @{ML_ind [index] FOCUS in Subgoal}, which does s
ame as @{ML SUBPROOF}
but does not require us to completely discharge the goal.
*}
@@ -632,7 +632,7 @@
going in our example, we will print out these values using the printing
function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will
supply us the @{text "params"} and @{text "prems"} as lists, we can
- separate them using the function @{ML [index] chop}.
+ separate them using the function @{ML_ind [index] chop}.
*}
ML %linenosgray{*fun chop_test_tac preds rules =
@@ -699,7 +699,7 @@
To use this premise with @{ML rtac}, we need to instantiate its
quantifiers (with @{text params1}) and transform it into rule
- format (using @{ML [index] rulify in ObjectLogic}). So we can modify the
+ format (using @{ML_ind [index] rulify in ObjectLogic}). So we can modify the
code as follows:
*}
@@ -863,7 +863,7 @@
In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve
them with @{text prem}. In the simple cases, that is where the @{text prem}
comes from a non-recursive premise of the rule, @{text prems} will be
- just the empty list and the function @{ML [index] MRS} does nothing. Similarly, in the
+ just the empty list and the function @{ML_ind [index] MRS} does nothing. Similarly, in the
cases where the recursive premises of the rule do not have preconditions.
In case there are preconditions, then Line 4 discharges them. After
that we can proceed as before, i.e., check whether the outermost
@@ -942,7 +942,7 @@
end*}
text {*
- The iteration is done with the function @{ML [index] map_index} since we
+ The iteration is done with the function @{ML_ind [index] map_index} since we
need the introduction rule together with its number (counted from
@{text 0}). This completes the code for the functions deriving the
reasoning infrastructure. It remains to implement some administrative
@@ -955,7 +955,7 @@
We have produced various theorems (definitions, induction principles and
introduction rules), but apart from the definitions, we have not yet
registered them with the theorem database. This is what the functions
- @{ML [index] note in LocalTheory} does.
+ @{ML_ind [index] note in LocalTheory} does.
For convenience, we use the following
@@ -1037,7 +1037,7 @@
Line 20 add further every introduction rule under its own name
(given by the user).\footnote{FIXME: what happens if the user did not give
any name.} Line 21 registers the induction principles. For this we have
- to use some specific attributes. The first @{ML [index] case_names in RuleCases}
+ to use some specific attributes. The first @{ML_ind [index] case_names in RuleCases}
corresponds to the case names that are used by Isar to reference the proof
obligations in the induction. The second @{ML "consumes 1" in RuleCases}
indicates that the first premise of the induction principle (namely
--- a/ProgTutorial/Package/Ind_Interface.thy Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy Thu Aug 20 14:19:39 2009 +0200
@@ -138,8 +138,8 @@
OuterKeyword.thy_decl specification*}
text {*
- We call @{ML [index] local_theory in OuterSyntax} with the kind-indicator
- @{ML [index] thy_decl in OuterKeyword} since the package does not need to open
+ We call @{ML_ind [index] local_theory in OuterSyntax} with the kind-indicator
+ @{ML_ind [index] thy_decl in OuterKeyword} since the package does not need to open
up any proof (see Section~\ref{sec:newcommand}).
The auxiliary function @{text specification} in Lines 1 to 3
gathers the information from the parser to be processed further
@@ -151,7 +151,7 @@
eventually will be). Also the introduction rules are just strings. What we have
to do first is to transform the parser's output into some internal
datastructures that can be processed further. For this we can use the
- function @{ML [index] read_spec in Specification}. This function takes some strings
+ function @{ML_ind [index] read_spec in Specification}. This function takes some strings
(with possible typing annotations) and some rule specifications, and attempts
to find a typing according to the given type constraints given by the
user and the type constraints by the ``ambient'' theory. It returns
--- a/ProgTutorial/Parsing.thy Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/Parsing.thy Thu Aug 20 14:19:39 2009 +0200
@@ -37,7 +37,7 @@
text {*
Let us first have a look at parsing strings using generic parsing
- combinators. The function @{ML [index] "$$"} takes a string as argument and will
+ combinators. The function @{ML_ind [index] "$$"} takes a string as argument and will
``consume'' this string from a given input list of strings. ``Consume'' in
this context means that it will return a pair consisting of this string and
the rest of the input list. For example:
@@ -89,7 +89,7 @@
[\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
Slightly more general than the parser @{ML "$$"} is the function
- @{ML [index] one in Scan}, in that it takes a predicate as argument and
+ @{ML_ind [index] one in Scan}, in that it takes a predicate as argument and
then parses exactly
one item from the input list satisfying this predicate. For example the
following parser either consumes an @{text [quotes] "h"} or a @{text
@@ -105,7 +105,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- Two parsers can be connected in sequence by using the function @{ML [index] "--"}.
+ Two parsers can be connected in sequence by using the function @{ML_ind [index] "--"}.
For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
order) you can achieve by:
@@ -116,14 +116,14 @@
Note how the result of consumed strings builds up on the left as nested pairs.
If, as in the previous example, you want to parse a particular string,
- then you should use the function @{ML [index] this_string in Scan}:
+ then you should use the function @{ML_ind [index] this_string in Scan}:
@{ML_response [display,gray]
"Scan.this_string \"hell\" (Symbol.explode \"hello\")"
"(\"hell\", [\"o\"])"}
Parsers that explore alternatives can be constructed using the function
- @{ML [index] "||"}. The parser @{ML "(p || q)" for p q} returns the
+ @{ML_ind [index] "||"}. The parser @{ML "(p || q)" for p q} returns the
result of @{text "p"}, in case it succeeds, otherwise it returns the
result of @{text "q"}. For example:
@@ -138,7 +138,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- The functions @{ML [index] "|--"} and @{ML [index] "--|"} work like the sequencing function
+ The functions @{ML_ind [index] "|--"} and @{ML_ind [index] "--|"} work like the sequencing function
for parsers, except that they discard the item being parsed by the first (respectively second)
parser. For example:
@@ -167,7 +167,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML [index] option in Scan} works similarly, except no default value can
+ The function @{ML_ind [index] option in Scan} works similarly, except no default value can
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
@{ML_response [display,gray]
@@ -179,7 +179,7 @@
(p input1, p input2)
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML [index] "!!"} helps to produce appropriate error messages
+ The function @{ML_ind [index] "!!"} helps to produce appropriate error messages
for parsing. For example if you want to parse @{text p} immediately
followed by @{text q}, or start a completely different parser @{text r},
you might write:
@@ -215,13 +215,13 @@
then the parsing aborts and the error message @{text "foo"} is printed. In order to
see the error message properly, you need to prefix the parser with the function
- @{ML [index] error in Scan}. For example:
+ @{ML_ind [index] error in Scan}. For example:
@{ML_response_fake [display,gray]
"Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
"Exception Error \"foo\" raised"}
- This ``prefixing'' is usually done by wrappers such as @{ML [index] local_theory in OuterSyntax}
+ This ``prefixing'' is usually done by wrappers such as @{ML_ind [index] local_theory in OuterSyntax}
(see Section~\ref{sec:newcommand} which explains this function in more detail).
Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
@@ -258,14 +258,14 @@
@{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
- Note that @{ML [index] repeat in Scan} stores the parsed items in a list. The function
- @{ML [index] repeat1 in Scan} is similar, but requires that the parser @{text "p"}
+ Note that @{ML_ind [index] repeat in Scan} stores the parsed items in a list. The function
+ @{ML_ind [index] repeat1 in Scan} is similar, but requires that the parser @{text "p"}
succeeds at least once.
Also note that the parser would have aborted with the exception @{text MORE}, if
you had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using
- the wrapper @{ML [index] finite in Scan} and the ``stopper-token''
- @{ML [index] stopper in Symbol}. With them you can write:
+ the wrapper @{ML_ind [index] finite in Scan} and the ``stopper-token''
+ @{ML_ind [index] stopper in Symbol}. With them you can write:
@{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
@@ -274,7 +274,7 @@
other stoppers need to be used when parsing, for example, tokens. However, this kind of
manually wrapping is often already done by the surrounding infrastructure.
- The function @{ML [index] repeat in Scan} can be used with @{ML [index] one in Scan} to read any
+ The function @{ML_ind [index] repeat in Scan} can be used with @{ML_ind [index] one in Scan} to read any
string as in
@{ML_response [display,gray]
@@ -286,10 +286,10 @@
end"
"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
- where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the
+ where the function @{ML_ind [index] not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
- The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can
+ The function @{ML_ind [index] unless in Scan} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
@{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
@@ -302,7 +302,7 @@
succeeds.
- The functions @{ML [index] repeat in Scan} and @{ML [index] unless in Scan} can
+ The functions @{ML_ind [index] repeat in Scan} and @{ML_ind [index] unless in Scan} can
be combined to read any input until a certain marker symbol is reached. In the
example below the marker symbol is a @{text [quotes] "*"}.
@@ -320,7 +320,7 @@
After parsing is done, you almost always want to apply a function to the parsed
- items. One way to do this is the function @{ML [index]">>"} where
+ items. One way to do this is the function @{ML_ind [index]">>"} where
@{ML "(p >> f)" for p f} runs
first the parser @{text p} and upon successful completion applies the
function @{text f} to the result. For example
@@ -349,14 +349,14 @@
(FIXME: move to an earlier place)
- The function @{ML [index] ahead in Scan} parses some input, but leaves the original
+ The function @{ML_ind [index] ahead in Scan} parses some input, but leaves the original
input unchanged. For example:
@{ML_response [display,gray]
"Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
"(\"foo\", [\"f\", \"o\", \"o\"])"}
- The function @{ML [index] lift in Scan} takes a parser and a pair as arguments. This function applies
+ The function @{ML_ind [index] lift in Scan} takes a parser and a pair as arguments. This function applies
the given parser to the second component of the pair and leaves the first component
untouched. For example
@@ -397,11 +397,11 @@
\end{readmore}
The structure @{ML_struct [index] OuterLex} defines several kinds of tokens (for
- example @{ML [index] Ident in OuterLex} for identifiers, @{ML Keyword in
- OuterLex} for keywords and @{ML [index] Command in OuterLex} for commands). Some
+ example @{ML_ind [index] Ident in OuterLex} for identifiers, @{ML Keyword in
+ OuterLex} for keywords and @{ML_ind [index] Command in OuterLex} for commands). Some
token parsers take into account the kind of tokens. The first example shows
how to generate a token list out of a string using the function
- @{ML [index] scan in OuterSyntax}. It is given the argument
+ @{ML_ind [index] scan in OuterSyntax}. It is given the argument
@{ML "Position.none"} since,
at the moment, we are not interested in generating precise error
messages. The following code\footnote{Note that because of a possible bug in
@@ -419,7 +419,7 @@
other syntactic category. The second indicates a space.
We can easily change what is recognised as a keyword with
- @{ML [index] keyword in OuterKeyword}. For example calling this function
+ @{ML_ind [index] keyword in OuterKeyword}. For example calling this function
*}
ML{*val _ = OuterKeyword.keyword "hello"*}
@@ -434,7 +434,7 @@
Many parsing functions later on will require white space, comments and the like
to have already been filtered out. So from now on we are going to use the
- functions @{ML filter} and @{ML [index] is_proper in OuterLex} to do this.
+ functions @{ML filter} and @{ML_ind [index] is_proper in OuterLex} to do this.
For example:
@{ML_response_fake [display,gray]
@@ -472,10 +472,10 @@
end"
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
- You might have to adjust the @{ML [index] print_depth} in order to
+ You might have to adjust the @{ML_ind [index] print_depth} in order to
see the complete list.
- The parser @{ML [index] "$$$" in OuterParse} parses a single keyword. For example:
+ The parser @{ML_ind [index] "$$$" in OuterParse} parses a single keyword. For example:
@{ML_response [display,gray]
"let
@@ -486,7 +486,7 @@
end"
"((\"where\",\<dots>), (\"|\",\<dots>))"}
- Any non-keyword string can be parsed with the function @{ML [index] reserved in OuterParse}.
+ Any non-keyword string can be parsed with the function @{ML_ind [index] reserved in OuterParse}.
For example:
@{ML_response [display,gray]
@@ -498,7 +498,7 @@
end"
"(\"bar\",[])"}
- Like before, you can sequentially connect parsers with @{ML [index] "--"}. For example:
+ Like before, you can sequentially connect parsers with @{ML_ind [index] "--"}. For example:
@{ML_response [display,gray]
"let
@@ -521,7 +521,7 @@
end"
"([\"in\", \"in\", \"in\"], [\<dots>])"}
- @{ML [index] enum1 in OuterParse} works similarly, except that the parsed list must
+ @{ML_ind [index] enum1 in OuterParse} works similarly, except that the parsed list must
be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the
end of the parsed string, otherwise the parser would have consumed all
tokens and then failed with the exception @{text "MORE"}. Like in the
@@ -545,7 +545,7 @@
text {*
- The function @{ML [index] "!!!" in OuterParse} can be used to force termination of the
+ The function @{ML_ind [index] "!!!" in OuterParse} can be used to force termination of the
parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section).
Except that the error message of @{ML "OuterParse.!!!"} is fixed to be
@{text [quotes] "Outer syntax error"}
@@ -564,7 +564,7 @@
\begin{exercise} (FIXME)
A type-identifier, for example @{typ "'a"}, is a token of
- kind @{ML [index] Keyword in OuterLex}. It can be parsed using
+ kind @{ML_ind [index] Keyword in OuterLex}. It can be parsed using
the function @{ML type_ident in OuterParse}.
\end{exercise}
@@ -626,7 +626,7 @@
text {*
There is usually no need to write your own parser for parsing inner syntax, that is
for terms and types: you can just call the predefined parsers. Terms can
- be parsed using the function @{ML [index] term in OuterParse}. For example:
+ be parsed using the function @{ML_ind [index] term in OuterParse}. For example:
@{ML_response [display,gray]
"let
@@ -636,10 +636,10 @@
end"
"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
- The function @{ML [index] prop in OuterParse} is similar, except that it gives a different
+ The function @{ML_ind [index] prop in OuterParse} is similar, except that it gives a different
error message, when parsing fails. As you can see, the parser not just returns
the parsed string, but also some encoded information. You can decode the
- information with the function @{ML [index] parse in YXML}. For example
+ information with the function @{ML_ind [index] parse in YXML}. For example
@{ML_response [display,gray]
"YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
@@ -723,7 +723,7 @@
variables with optional type-annotation and syntax-annotation, and a list of
rules where every rule has optionally a name and an attribute.
- The function @{ML [index] "fixes" in OuterParse} in Line 2 of the parser reads an
+ The function @{ML_ind [index] "fixes" in OuterParse} in Line 2 of the parser reads an
\isacommand{and}-separated
list of variables that can include optional type annotations and syntax translations.
For example:\footnote{Note that in the code we need to write
@@ -747,8 +747,8 @@
not yet used to type the variables: this must be done by type-inference later
on. Since types are part of the inner syntax they are strings with some
encoded information (see previous section). If a mixfix-syntax is
- present for a variable, then it is stored in the @{ML [index] Mixfix} data structure;
- no syntax translation is indicated by @{ML [index] NoSyn}.
+ present for a variable, then it is stored in the @{ML_ind [index] Mixfix} data structure;
+ no syntax translation is indicated by @{ML_ind [index] NoSyn}.
\begin{readmore}
The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
@@ -757,7 +757,7 @@
Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
list of introduction rules, that is propositions with theorem annotations
such as rule names and attributes. The introduction rules are propositions
- parsed by @{ML [index] prop in OuterParse}. However, they can include an optional
+ parsed by @{ML_ind [index] prop in OuterParse}. However, they can include an optional
theorem name plus some attributes. For example
@{ML_response [display,gray] "let
@@ -767,8 +767,8 @@
(name, map Args.dest_src attrib)
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
- The function @{ML [index] opt_thm_name in SpecParse} is the ``optional'' variant of
- @{ML [index] thm_name in SpecParse}. Theorem names can contain attributes. The name
+ The function @{ML_ind [index] opt_thm_name in SpecParse} is the ``optional'' variant of
+ @{ML_ind [index] thm_name in SpecParse}. Theorem names can contain attributes. The name
has to end with @{text [quotes] ":"}---see the argument of
the function @{ML SpecParse.opt_thm_name} in Line 7.
@@ -783,7 +783,7 @@
Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
to the ``where-part'' of the introduction rules given above. Below
- we paraphrase the code of @{ML [index] where_alt_specs in SpecParse} adapted to our
+ we paraphrase the code of @{ML_ind [index] where_alt_specs in SpecParse} adapted to our
purposes.
\begin{isabelle}
*}
@@ -834,7 +834,7 @@
end *}
text {*
- The crucial function @{ML [index] local_theory in OuterSyntax} expects a name for the command, a
+ The crucial function @{ML_ind [index] local_theory in OuterSyntax} expects a name for the command, a
short description, a kind indicator (which we will explain later more thoroughly) and a
parser producing a local theory transition (its purpose will also explained
later).
@@ -974,7 +974,7 @@
The crucial part of a command is the function that determines the behaviour
of the command. In the code above we used a ``do-nothing''-function, which
- because of @{ML [index] succeed in Scan} does not parse any argument, but immediately
+ because of @{ML_ind [index] succeed in Scan} does not parse any argument, but immediately
returns the simple function @{ML "LocalTheory.theory I"}. We can
replace this code by a function that first parses a proposition (using the
parser @{ML OuterParse.prop}), then prints out the tracing
@@ -1004,7 +1004,7 @@
and see the proposition in the tracing buffer.
- Note that so far we used @{ML [index] thy_decl in OuterKeyword} as the kind
+ Note that so far we used @{ML_ind [index] thy_decl in OuterKeyword} as the kind
indicator for the command. This means that the command finishes as soon as
the arguments are processed. Examples of this kind of commands are
\isacommand{definition} and \isacommand{declare}. In other cases, commands
@@ -1012,7 +1012,7 @@
``open up'' a proof in order to prove the proposition (for example
\isacommand{lemma}) or prove some other properties (for example
\isacommand{function}). To achieve this kind of behaviour, you have to use
- the kind indicator @{ML [index] thy_goal in OuterKeyword} and the function @{ML
+ the kind indicator @{ML_ind [index] thy_goal in OuterKeyword} and the function @{ML
"local_theory_to_proof" in OuterSyntax} to set up the command. Note,
however, once you change the ``kind'' of a command from @{ML thy_decl in
OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
@@ -1041,8 +1041,8 @@
text {*
The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
proved) and a context as argument. The context is necessary in order to be able to use
- @{ML [index] read_prop in Syntax}, which converts a string into a proper proposition.
- In Line 6 the function @{ML [index] theorem_i in Proof} starts the proof for the
+ @{ML_ind [index] read_prop in Syntax}, which converts a string into a proper proposition.
+ In Line 6 the function @{ML_ind [index] theorem_i in Proof} starts the proof for the
proposition. Its argument @{ML NONE} stands for a locale (which we chose to
omit); the argument @{ML "(K I)"} stands for a function that determines what
should be done with the theorem once it is proved (we chose to just forget
@@ -1066,7 +1066,7 @@
\isacommand{done}
\end{isabelle}
- (FIXME: read a name and show how to store theorems; see @{ML [index] note in LocalTheory})
+ (FIXME: read a name and show how to store theorems; see @{ML_ind [index] note in LocalTheory})
*}
@@ -1099,7 +1099,7 @@
It defines the method @{text foo}, which takes no arguments (therefore the
parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which
applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
- @{ML [index] SIMPLE_METHOD}
+ @{ML_ind [index] SIMPLE_METHOD}
turns such a tactic into a method. The method @{text "foo"} can be used as follows
*}
--- a/ProgTutorial/Tactical.thy Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/Tactical.thy Thu Aug 20 14:19:39 2009 +0200
@@ -56,12 +56,13 @@
@{text xs} that will be generalised once the goal is proved (in our case
@{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
it can make use of the local assumptions (there are none in this example).
- The tactics @{ML [index] etac}, @{ML [index] rtac} and @{ML [index] atac} in the code above correspond
+ The tactics @{ML_ind [index] etac}, @{ML_ind [index] rtac} and @{ML_ind [index] atac}
+ in the code above correspond
roughly to @{text erule}, @{text rule} and @{text assumption}, respectively.
- The operator @{ML [index] THEN} strings the tactics together.
+ The operator @{ML_ind [index] THEN} strings the tactics together.
\begin{readmore}
- To learn more about the function @{ML [index] prove in Goal} see \isccite{sec:results}
+ To learn more about the function @{ML_ind [index] prove in Goal} see \isccite{sec:results}
and the file @{ML_file "Pure/goal.ML"}. See @{ML_file
"Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
tactics and tactic combinators; see also Chapters 3 and 4 in the old
@@ -119,7 +120,7 @@
THEN' atac)*}text_raw{*\label{tac:footacprime}*}
text {*
- where @{ML [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+ where @{ML_ind [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
the number for the subgoal explicitly when the tactic is
called. So in the next proof you can first discharge the second subgoal, and
subsequently the first.
@@ -160,7 +161,7 @@
willy-nilly; only in very grave failure situations should a tactic raise the
exception @{text THM}.
- The simplest tactics are @{ML [index] no_tac} and @{ML [index] all_tac}. The first returns
+ The simplest tactics are @{ML_ind [index] no_tac} and @{ML_ind [index] all_tac}. The first returns
the empty sequence and is defined as
*}
@@ -335,7 +336,7 @@
section {* Simple Tactics\label{sec:simpletacs} *}
text {*
- Let us start with explaining the simple tactic @{ML [index] print_tac}, which is quite useful
+ Let us start with explaining the simple tactic @{ML_ind [index] print_tac}, which is quite useful
for low-level debugging of tactics. It just prints out a message and the current
goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
as the user would see it. For example, processing the proof
@@ -355,7 +356,7 @@
text {*
A simple tactic for easy discharge of any proof obligations is
- @{ML [index] cheat_tac in SkipProof}. This tactic corresponds to
+ @{ML_ind [index] cheat_tac in SkipProof}. This tactic corresponds to
the Isabelle command \isacommand{sorry} and is sometimes useful
during the development of tactics.
*}
@@ -371,7 +372,7 @@
This tactic works however only if the quick-and-dirty mode of Isabelle
is switched on.
- Another simple tactic is the function @{ML [index] atac}, which, as shown in the previous
+ Another simple tactic is the function @{ML_ind [index] atac}, which, as shown in the previous
section, corresponds to the assumption command.
*}
@@ -383,8 +384,8 @@
(*<*)oops(*>*)
text {*
- Similarly, @{ML [index] rtac}, @{ML [index] dtac}, @{ML [index] etac} and
- @{ML [index] ftac} correspond (roughly)
+ Similarly, @{ML_ind [index] rtac}, @{ML_ind [index] dtac}, @{ML_ind [index] etac} and
+ @{ML_ind [index] ftac} correspond (roughly)
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
respectively. Each of them takes a theorem as argument and attempts to
apply it to a goal. Below are three self-explanatory examples.
@@ -412,7 +413,7 @@
(*<*)oops(*>*)
text {*
- The function @{ML [index] resolve_tac} is similar to @{ML [index] rtac}, except that it
+ The function @{ML_ind [index] resolve_tac} is similar to @{ML_ind [index] rtac}, except that it
expects a list of theorems as arguments. From this list it will apply the
first applicable theorem (later theorems that are also applicable can be
explored via the lazy sequences mechanism). Given the code
@@ -435,11 +436,11 @@
text {*
Similar versions taking a list of theorems exist for the tactics
- @{ML dtac} (@{ML [index] dresolve_tac}), @{ML etac}
- (@{ML [index] eresolve_tac}) and so on.
+ @{ML dtac} (@{ML_ind [index] dresolve_tac}), @{ML etac}
+ (@{ML_ind [index] eresolve_tac}) and so on.
- Another simple tactic is @{ML [index] cut_facts_tac}. It inserts a list of theorems
+ Another simple tactic is @{ML_ind [index] cut_facts_tac}. It inserts a list of theorems
into the assumptions of the current goal state. For example
*}
@@ -474,7 +475,7 @@
should be, then this situation can be avoided by introducing a more
constrained version of the @{text bspec}-rule. Such constraints can be given by
pre-instantiating theorems with other theorems. One function to do this is
- @{ML [index] RS}
+ @{ML_ind [index] "RS"}
@{ML_response_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
@@ -488,7 +489,7 @@
"*** Exception- THM (\"RSN: no unifiers\", 1,
[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
- then the function raises an exception. The function @{ML [index] RSN} is similar to @{ML RS}, but
+ then the function raises an exception. The function @{ML_ind [index] RSN} is similar to @{ML RS}, but
takes an additional number as argument that makes explicit which premise
should be instantiated.
@@ -501,14 +502,14 @@
"no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
If you want to instantiate more than one premise of a theorem, you can use
- the function @{ML [index] MRS}:
+ the function @{ML_ind [index] MRS}:
@{ML_response_fake [display,gray]
"no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
If you need to instantiate lists of theorems, you can use the
- functions @{ML RL} and @{ML [index] MRL}. For example in the code below,
+ functions @{ML RL} and @{ML_ind [index] MRL}. For example in the code below,
every theorem in the second list is instantiated with every
theorem in the first.
@@ -527,8 +528,8 @@
Often proofs on the ML-level involve elaborate operations on assumptions and
@{text "\<And>"}-quantified variables. To do such operations using the basic tactics
shown so far is very unwieldy and brittle. Some convenience and
- safety is provided by the functions @{ML [index] FOCUS in Subgoal} and
- @{ML [index] SUBPROOF}. These tactics fix the parameters
+ safety is provided by the functions @{ML_ind [index] FOCUS in Subgoal} and
+ @{ML_ind [index] SUBPROOF}. These tactics fix the parameters
and bind the various components of a goal state to a record.
To see what happens, use the function defined in Figure~\ref{fig:sptac}, which
takes a record and just prints out the contents of this record. Consider
@@ -667,7 +668,7 @@
Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
@{ML SUBPROOF}, are
- @{ML [index] SUBGOAL} and @{ML [index] CSUBGOAL}. They allow you to
+ @{ML_ind [index] SUBGOAL} and @{ML_ind [index] CSUBGOAL}. They allow you to
inspect a given subgoal (the former
presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
cterm}). With this you can implement a tactic that applies a rule according
@@ -779,7 +780,7 @@
in what follows we will usually prefer it over the ``unprimed'' one.
If there is a list of tactics that should all be tried out in
- sequence, you can use the combinator @{ML [index] EVERY'}. For example
+ sequence, you can use the combinator @{ML_ind [index] EVERY'}. For example
the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
be written as:
*}
@@ -801,11 +802,11 @@
text {*
and call @{ML foo_tac1}.
- With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML [index] EVERY1} it must be
+ With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind [index] EVERY1} it must be
guaranteed that all component tactics successfully apply; otherwise the
whole tactic will fail. If you rather want to try out a number of tactics,
- then you can use the combinator @{ML [index] ORELSE'} for two tactics, and @{ML
- [index] FIRST'} (or @{ML [index] FIRST1}) for a list of tactics. For example, the tactic
+ then you can use the combinator @{ML_ind [index] ORELSE'} for two tactics, and @{ML_ind
+ [index] FIRST'} (or @{ML_ind [index] FIRST1}) for a list of tactics. For example, the tactic
*}
@@ -857,7 +858,7 @@
text {*
Since such repeated applications of a tactic to the reverse order of
\emph{all} subgoals is quite common, there is the tactic combinator
- @{ML [index] ALLGOALS} that simplifies this. Using this combinator you can simply
+ @{ML_ind [index] ALLGOALS} that simplifies this. Using this combinator you can simply
write: *}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -870,7 +871,7 @@
text {*
Remember that we chose to implement @{ML select_tac'} so that it
always succeeds by adding @{ML all_tac} at the end of the tactic
- list. The same can be achieved with the tactic combinator @{ML [index] TRY}.
+ list. The same can be achieved with the tactic combinator @{ML_ind [index] TRY}.
For example:
*}
@@ -903,7 +904,7 @@
from the end of the theorem list. As a result @{ML select_tac'} would only
succeed on goals where it can make progress. But for the sake of argument,
let us suppose that this deletion is \emph{not} an option. In such cases, you can
- use the combinator @{ML [index] CHANGED} to make sure the subgoal has been changed
+ use the combinator @{ML_ind [index] CHANGED} to make sure the subgoal has been changed
by the tactic. Because now
*}
@@ -921,7 +922,7 @@
text {*
We can further extend @{ML select_tac'} so that it not just applies to the topmost
connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal
- completely. For this you can use the tactic combinator @{ML [index] REPEAT}. As an example
+ completely. For this you can use the tactic combinator @{ML_ind [index] REPEAT}. As an example
suppose the following tactic
*}
@@ -942,7 +943,7 @@
Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED},
because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
tactic as long as it succeeds). The function
- @{ML [index] REPEAT1} is similar, but runs the tactic at least once (failing if
+ @{ML_ind [index] REPEAT1} is similar, but runs the tactic at least once (failing if
this is not possible).
If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
@@ -958,7 +959,7 @@
and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
that goals 2 and 3 are not analysed. This is because the tactic
is applied repeatedly only to the first subgoal. To analyse also all
- resulting subgoals, you can use the tactic combinator @{ML [index] REPEAT_ALL_NEW}.
+ resulting subgoals, you can use the tactic combinator @{ML_ind [index] REPEAT_ALL_NEW}.
Suppose the tactic
*}
@@ -1011,7 +1012,7 @@
Sometimes this leads to confusing behaviour of tactics and also has
the potential to explode the search space for tactics.
These problems can be avoided by prefixing the tactic with the tactic
- combinator @{ML [index] DETERM}.
+ combinator @{ML_ind [index] DETERM}.
*}
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
@@ -1048,7 +1049,7 @@
text {*
then the tactic @{ML select_tac''} will be tried out and any failure is harnessed.
We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is
- no primed version of @{ML [index] TRY}. The tactic combinator @{ML [index] TRYALL} will try out
+ no primed version of @{ML_ind [index] TRY}. The tactic combinator @{ML_ind [index] TRYALL} will try out
a tactic on all subgoals. For example the tactic
*}
@@ -1057,7 +1058,7 @@
text {*
will solve all trivial subgoals involving @{term True} or @{term "False"}.
- (FIXME: say something about @{ML [index] COND} and COND')
+ (FIXME: say something about @{ML_ind [index] COND} and COND')
(FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
@@ -1117,7 +1118,7 @@
are discharged. Note that in Isabelle the left-rules need to be implemented
as elimination rules. You need to prove separate lemmas corresponding to
$\longrightarrow_{L_{1..4}}$. In order to explore all possibilities of applying
- the rules, use the tactic combinator @{ML [index] DEPTH_SOLVE}, which searches
+ the rules, use the tactic combinator @{ML_ind [index] DEPTH_SOLVE}, which searches
for a state in which all subgoals are solved. Add also rules for equality and
run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}.
\end{exercise}
@@ -1141,11 +1142,11 @@
\begin{isabelle}
\begin{center}
\begin{tabular}{l@ {\hspace{2cm}}l}
- @{ML [index] simp_tac} & @{text "(simp (no_asm))"} \\
- @{ML [index] asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
- @{ML [index] full_simp_tac} & @{text "(simp (no_asm_use))"} \\
- @{ML [index] asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
- @{ML [index] asm_full_simp_tac} & @{text "(simp)"}
+ @{ML_ind [index] simp_tac} & @{text "(simp (no_asm))"} \\
+ @{ML_ind [index] asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
+ @{ML_ind [index] full_simp_tac} & @{text "(simp (no_asm_use))"} \\
+ @{ML_ind [index] asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
+ @{ML_ind [index] asm_full_simp_tac} & @{text "(simp)"}
\end{tabular}
\end{center}
\end{isabelle}
@@ -1229,9 +1230,9 @@
\begin{isabelle}
\begin{tabular}{ll}
- @{ML [index] addsimps} & @{ML [index] delsimps}\\
- @{ML [index] addcongs} & @{ML [index] delcongs}\\
- @{ML [index] addsimprocs} & @{ML [index] delsimprocs}\\
+ @{ML_ind [index] addsimps} & @{ML_ind [index] delsimps}\\
+ @{ML_ind [index] addcongs} & @{ML_ind [index] delcongs}\\
+ @{ML_ind [index] addsimprocs} & @{ML_ind [index] delsimprocs}\\
\end{tabular}
\end{isabelle}
@@ -1261,7 +1262,7 @@
text_raw {*
\end{isabelle}
\end{minipage}
-\caption{The function @{ML [index] dest_ss in Simplifier} returns a record containing
+\caption{The function @{ML_ind [index] dest_ss in Simplifier} returns a record containing
all printable information stored in a simpset. We are here only interested in the
simplification rules, congruence rules and simprocs.\label{fig:printss}}
\end{figure} *}
@@ -1269,7 +1270,7 @@
text {*
To see how they work, consider the function in Figure~\ref{fig:printss}, which
prints out some parts of a simpset. If you use it to print out the components of the
- empty simpset, i.e., @{ML [index] empty_ss}
+ empty simpset, i.e., @{ML_ind [index] empty_ss}
@{ML_response_fake [display,gray]
"print_ss @{context} empty_ss"
@@ -1316,7 +1317,7 @@
expects this form of the simplification and congruence rules. However, even
when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
- In the context of HOL, the first really useful simpset is @{ML [index] HOL_basic_ss}. While
+ In the context of HOL, the first really useful simpset is @{ML_ind [index] HOL_basic_ss}. While
printing out the components of this simpset
@{ML_response_fake [display,gray]
@@ -1343,9 +1344,9 @@
text {*
This behaviour is not because of simplification rules, but how the subgoaler, solver
- and looper are set up in @{ML [index] HOL_basic_ss}.
+ and looper are set up in @{ML_ind [index] HOL_basic_ss}.
- The simpset @{ML [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing
+ The simpset @{ML_ind [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing
already many useful simplification and congruence rules for the logical
connectives in HOL.
@@ -1365,7 +1366,7 @@
The simplifier is often used to unfold definitions in a proof. For this the
- simplifier implements the tactic @{ML [index] rewrite_goals_tac}.\footnote{FIXME:
+ simplifier implements the tactic @{ML_ind [index] rewrite_goals_tac}.\footnote{FIXME:
see LocalDefs infrastructure.} Suppose for example the
definition
*}
@@ -1679,7 +1680,7 @@
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
The function also takes a list of patterns that can trigger the simproc.
Now the simproc is set up and can be explicitly added using
- @{ML [index] addsimprocs} to a simpset whenever
+ @{ML_ind [index] addsimprocs} to a simpset whenever
needed.
Simprocs are applied from inside to outside and from left to right. You can
@@ -1765,7 +1766,7 @@
| dest_suc_trm t = snd (HOLogic.dest_number t)*}
text {*
- It uses the library function @{ML [index] dest_number in HOLogic} that transforms
+ It uses the library function @{ML_ind [index] dest_number in HOLogic} that transforms
(Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
on, into integer values. This function raises the exception @{ML TERM}, if
the term is not a number. The next function expects a pair consisting of a term
@@ -1885,21 +1886,21 @@
text {*
whereby the produced theorem is always a meta-equality. A simple conversion
- is the function @{ML [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
+ is the function @{ML_ind [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
instance of the (meta)reflexivity theorem. For example:
@{ML_response_fake [display,gray]
"Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
"Foo \<or> Bar \<equiv> Foo \<or> Bar"}
- Another simple conversion is @{ML [index] no_conv in Conv} which always raises the
+ Another simple conversion is @{ML_ind [index] no_conv in Conv} which always raises the
exception @{ML CTERM}.
@{ML_response_fake [display,gray]
"Conv.no_conv @{cterm True}"
"*** Exception- CTERM (\"no conversion\", []) raised"}
- A more interesting conversion is the function @{ML [index] beta_conversion in Thm}: it
+ A more interesting conversion is the function @{ML_ind [index] beta_conversion in Thm}: it
produces a meta-equation between a term and its beta-normal form. For example
@{ML_response_fake [display,gray]
@@ -1941,7 +1942,7 @@
The main point of conversions is that they can be used for rewriting
@{ML_type cterm}s. One example is the function
- @{ML [index] rewr_conv in Conv}, which expects a meta-equation as an
+ @{ML_ind [index] rewr_conv in Conv}, which expects a meta-equation as an
argument. Suppose the following meta-equation.
*}
@@ -1960,15 +1961,15 @@
end"
"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
- Note, however, that the function @{ML [index] rewr_conv in Conv} only rewrites the
+ Note, however, that the function @{ML_ind [index] rewr_conv in Conv} only rewrites the
outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
exactly the
- left-hand side of the theorem, then @{ML [index] rewr_conv in Conv} fails, raising
+ left-hand side of the theorem, then @{ML_ind [index] rewr_conv in Conv} fails, raising
the exception @{ML CTERM}.
This very primitive way of rewriting can be made more powerful by
combining several conversions into one. For this you can use conversion
- combinators. The simplest conversion combinator is @{ML [index] then_conv},
+ combinators. The simplest conversion combinator is @{ML_ind [index] then_conv},
which applies one conversion after another. For example
@{ML_response_fake [display,gray]
@@ -1985,7 +1986,7 @@
@{thm [source] true_conj1}. (When running this example recall the
problem with the pretty-printer normalising all terms.)
- The conversion combinator @{ML [index] else_conv} tries out the
+ The conversion combinator @{ML_ind [index] else_conv} tries out the
first one, and if it does not apply, tries the second. For example
@{ML_response_fake [display,gray]
@@ -2003,7 +2004,7 @@
does not fail, however, because the combinator @{ML else_conv in Conv} will then
try out @{ML all_conv in Conv}, which always succeeds.
- The conversion combinator @{ML [index] try_conv in Conv} constructs a conversion
+ The conversion combinator @{ML_ind [index] try_conv in Conv} constructs a conversion
which is tried out on a term, but in case of failure just does nothing.
For example
@@ -2019,8 +2020,8 @@
Apart from the function @{ML beta_conversion in Thm}, which is able to fully
beta-normalise a term, the conversions so far are restricted in that they
only apply to the outer-most level of a @{ML_type cterm}. In what follows we
- will lift this restriction. The combinators @{ML [index] fun_conv in Conv}
- and @{ML [index] arg_conv in Conv} will apply
+ will lift this restriction. The combinators @{ML_ind [index] fun_conv in Conv}
+ and @{ML_ind [index] arg_conv in Conv} will apply
a conversion to the first, respectively second, argument of an application.
For example
@@ -2039,7 +2040,7 @@
stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply
the conversion to the term @{text "(Const \<dots> $ t1)"}.
- The function @{ML [index] abs_conv in Conv} applies a conversion under an
+ The function @{ML_ind [index] abs_conv in Conv} applies a conversion under an
abstraction. For example:
@{ML_response_fake [display,gray]
@@ -2055,10 +2056,10 @@
conversion as @{text "(K conv)"}, which is a function that ignores its
argument (the argument being a sufficiently freshened version of the
variable that is abstracted and a context). The conversion that goes under
- an application is @{ML [index] combination_conv in Conv}. It expects two
+ an application is @{ML_ind [index] combination_conv in Conv}. It expects two
conversions as arguments, each of which is applied to the corresponding
``branch'' of the application. An abbreviation for this conversion is the
- function @{ML [index] comb_conv in Conv}, which applies the same conversion
+ function @{ML_ind [index] comb_conv in Conv}, which applies the same conversion
to both branches.
We can now apply all these functions in a conversion that recursively
@@ -2123,7 +2124,7 @@
text {*
So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
- also work on theorems using the function @{ML [index] fconv_rule in Conv}. As an example,
+ also work on theorems using the function @{ML_ind [index] fconv_rule in Conv}. As an example,
consider the conversion @{ML all_true1_conv} and the lemma:
*}
@@ -2143,18 +2144,18 @@
"?P \<or> \<not> ?P"}
Finally, conversions can also be turned into tactics and then applied to
- goal states. This can be done with the help of the function @{ML [index] CONVERSION},
+ goal states. This can be done with the help of the function @{ML_ind [index] CONVERSION},
and also some predefined conversion combinators that traverse a goal
state. The combinators for the goal state are:
\begin{itemize}
- \item @{ML [index] params_conv in Conv} for converting under parameters
+ \item @{ML_ind [index] params_conv in Conv} for converting under parameters
(i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"})
- \item @{ML [index] prems_conv in Conv} for applying a conversion to all
+ \item @{ML_ind [index] prems_conv in Conv} for applying a conversion to all
premises of a goal, and
- \item @{ML [index] concl_conv in Conv} for applying a conversion to the
+ \item @{ML_ind [index] concl_conv in Conv} for applying a conversion to the
conclusion of a goal.
\end{itemize}
--- a/ProgTutorial/antiquote_setup.ML Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML Thu Aug 20 14:19:39 2009 +0200
@@ -6,17 +6,18 @@
open OutputTutorial
(* functions for generating appropriate expressions *)
-fun ml_val_open ys strct txt =
+fun ml_val_open ys istruct txt =
let
fun ml_val_open_aux ys txt =
implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"];
in
- (case strct of
+ (case istruct of
NONE => ml_val_open_aux ys txt
| SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
end
fun ml_val txt = ml_val_open [] NONE txt;
+fun ml_val_ind istruct txt = ml_val_open [] istruct txt;
fun ml_pat (lhs, pat) =
let
@@ -42,17 +43,24 @@
#> implode
#> string_explode ""
-(* checks and prints open expressions, calculates index entry *)
+(* checks and prints a possibly open expressions, no index *)
fun output_ml {context = ctxt, ...} (txt, (ovars, istruc)) =
- (eval_fn ctxt (ml_val_open ovars istruc txt);
+ (eval_fn ctxt (ml_val_open ovars istruc txt); output (string_explode "" txt))
+
+val parser_ml = Scan.lift (Args.name --
+ (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
+ Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name)))
+
+(* checks and prinds a single entity, with index *)
+fun output_ml_ind {context = ctxt, ...} (txt, istruc) =
+ (eval_fn ctxt (ml_val_ind istruc txt);
case (istruc, Long_Name.base_name txt, Long_Name.qualifier txt) of
(NONE, bn, "") => output_indexed (transform_cmts_str txt) {main = Code txt, minor = NoString}
| (NONE, bn, qn) => output_indexed (transform_cmts_str txt) {main = Code bn, minor = IStruct qn}
| (SOME st, _, _) => output_indexed (transform_cmts_str txt) {main = Code txt, minor = IStruct st})
-val parser_ml = Scan.lift (Args.name --
- (Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
- Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name)))
+val parser_ml_ind = Scan.lift (Args.name --
+ Scan.option (Args.$$$ "in" |-- OuterParse.!!! Args.name))
(* checks and prints types and structures *)
fun output_struct {context = ctxt, ...} txt =
@@ -81,6 +89,7 @@
val two_args = Scan.lift (Args.name -- Args.name)
val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
+val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
val _ = ThyOutput.antiquotation "ML_response" two_args output_response
--- a/ProgTutorial/output_tutorial.ML Thu Aug 20 10:38:26 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML Thu Aug 20 14:19:39 2009 +0200
@@ -97,6 +97,7 @@
fun explicit "" = Default
| explicit s = Explicit s
+
val _ = ThyOutput.add_options
[("gray", Library.setmp gray o boolean),
("linenos", Library.setmp linenos o boolean),
Binary file progtutorial.pdf has changed