--- a/ProgTutorial/Base.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Base.thy Thu Aug 20 22:30:20 2009 +0200
@@ -2,7 +2,6 @@
imports Main LaTeXsugar
uses
"output_tutorial.ML"
- "chunks.ML"
"antiquote_setup.ML"
begin
--- a/ProgTutorial/FirstSteps.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Thu Aug 20 22:30:20 2009 +0200
@@ -3,8 +3,6 @@
uses "FirstSteps.ML"
begin
-
-
chapter {* First Steps *}
text {*
@@ -115,7 +113,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_ind [index] "writeln"}. For example
+ @{ML_ind "writeln"}. For example
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
@@ -123,7 +121,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_ind [index] makestring in PolyML}:
+ @{ML_ind makestring in PolyML}:
@{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""}
@@ -133,7 +131,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_ind [index] tracing} is more appropriate. This function writes all
+ function @{ML_ind 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 +164,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_ind [index] error}; for
+ You can print out error messages with the function @{ML_ind error}; for
example:
@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
@@ -177,8 +175,8 @@
be displayed by the infrastructure.
- (FIXME Mention how to work with @{ML_ind [index] debug in Toplevel} and
- @{ML_ind [index] profiling in Toplevel}.)
+ (FIXME Mention how to work with @{ML_ind debug in Toplevel} and
+ @{ML_ind profiling in Toplevel}.)
*}
(*
@@ -201,7 +199,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_ind [index] string_of_term in Syntax} in structure @{ML_struct
+ function @{ML_ind string_of_term in Syntax} in structure @{ML_struct
Syntax}, which we bind for more convenience to the toplevel.
*}
@@ -216,7 +214,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_ind [index] writeln} or @{ML_ind [index] tracing}:
+ using either the function @{ML_ind writeln} or @{ML_ind tracing}:
@{ML_response_fake [display,gray]
"writeln (string_of_term @{context} @{term \"1::nat\"})"
@@ -229,7 +227,7 @@
"\"1\""}
If there are more than one @{ML_type term}s to be printed, you can use the
- function @{ML_ind [index] commas} to separate them.
+ function @{ML_ind commas} to separate them.
*}
ML{*fun string_of_terms ctxt ts =
@@ -243,9 +241,9 @@
string_of_term ctxt (term_of ct)*}
text {*
- In this example the function @{ML_ind [index] term_of} extracts the @{ML_type
+ In this example the function @{ML_ind 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_ind [index] commas}.
+ printed with @{ML_ind commas}.
*}
ML{*fun string_of_cterms ctxt cts =
@@ -253,7 +251,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_ind [index] crep_thm}.
+ into a @{ML_type cterm} using the function @{ML_ind crep_thm}.
*}
ML{*fun string_of_thm ctxt thm =
@@ -272,7 +270,7 @@
However, in order to improve the readability when printing theorems, we
convert these schematic variables into free variables using the function
- @{ML_ind [index] import in Variable}. This is similar to statements like @{text
+ @{ML_ind import in Variable}. This is similar to statements like @{text
"conjI[no_vars]"} from Isabelle's user-level.
*}
@@ -322,7 +320,7 @@
and second half."}
To ease this kind of string manipulations, there are a number
- of library functions. For example, the function @{ML_ind [index] cat_lines}
+ of library functions. For example, the function @{ML_ind cat_lines}
concatenates a list of strings and inserts newlines.
@{ML_response [display, gray]
@@ -342,21 +340,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_ind [index] I}, which is just the identity function defined as
+ The simplest combinator is @{ML_ind I}, which is just the identity function defined as
*}
ML{*fun I x = x*}
-text {* Another simple combinator is @{ML_ind [index] K}, defined as *}
+text {* Another simple combinator is @{ML_ind K}, defined as *}
ML{*fun K x = fn _ => x*}
text {*
- @{ML_ind [index] K} ``wraps'' a function around the argument @{text "x"}. However, this
+ @{ML_ind 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_ind [index] "|>"}, defined as:
+ The next combinator is reverse application, @{ML_ind "|>"}, defined as:
*}
ML{*fun x |> f = f x*}
@@ -434,15 +432,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_ind [index] fastype_of} calculates the type of the
- term; @{ML_ind [index] binder_types} in the next line produces the list of argument
+ coded: in Line 2, the function @{ML_ind fastype_of} calculates the type of the
+ term; @{ML_ind 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_ind [index] variant_frees in Variable} generates for each @{text "z"} a
+ function @{ML_ind 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_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
+ by the function @{ML_ind list_comb} to the term. In this last step we have to
+ use the function @{ML_ind curry}, because @{ML_ind 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 +458,7 @@
where the @{text "za"} is correctly avoided.
- The combinator @{ML_ind [index] "#>"} is the reverse function composition. It can be
+ The combinator @{ML_ind "#>"} is the reverse function composition. It can be
used to define the following function
*}
@@ -475,7 +473,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_ind [index] tap} allows
+ ``waterfall method'' of writing functions. The combinator @{ML_ind tap} allows
you to get hold of an intermediate result (to do some side-calculations for
instance). The function
@@ -488,13 +486,13 @@
text {*
increments the argument first by @{text "1"} and then by @{text "2"}. In the
- 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
+ middle (Line 3), however, it uses @{ML_ind tap} for printing the ``plus-one''
+ intermediate result inside the tracing buffer. The function @{ML_ind 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_ind [index] "`"} (a backtick) is similar to @{ML tap}, but applies a
+ The combinator @{ML_ind "`"} (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 +507,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_ind [index] "|>>"} and @{ML_ind [index] "||>"} are defined for
+ The combinators @{ML_ind "|>>"} and @{ML_ind "||>"} are defined for
functions manipulating pairs. The first applies the function to
the first component of the pair, defined as
*}
@@ -556,7 +554,7 @@
conciseness is only small, in more complicated situations the benefit of
avoiding @{text "lets"} can be substantial.
- With the combinator @{ML_ind [index] "|->"} you can re-combine the elements from a pair.
+ With the combinator @{ML_ind "|->"} you can re-combine the elements from a pair.
This combinator is defined as
*}
@@ -572,10 +570,10 @@
|-> (fn x => fn y => x + y)*}
text {*
- The combinator @{ML_ind [index] ||>>} plays a central rôle whenever your task is to update a
+ The combinator @{ML_ind ||>>} 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_ind [index] ||>>}, you can do conveniently the update
+ component is the side-result. Using @{ML_ind ||>>}, you can do conveniently the update
and also accumulate the side-results. Consider the following simple function.
*}
@@ -587,7 +585,7 @@
text {*
The purpose of Line 2 is to just pair up the argument with a dummy value (since
- @{ML_ind [index] "||>>"} operates on pairs). Each of the next three lines just increment
+ @{ML_ind "||>>"} 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 +602,14 @@
*}
text {*
- Recall that @{ML_ind [index] "|>"} is the reverse function application. Recall also that
+ Recall that @{ML_ind "|>"} is the reverse function application. Recall also that
the related
- 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]
+ reverse function composition is @{ML_ind "#>"}. In fact all the combinators
+ @{ML_ind "|->"}, @{ML_ind "|>>"} , @{ML_ind "||>"} and @{ML_ind
"||>>"} described above have related combinators for
- 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:
+ function composition, namely @{ML_ind "#->"}, @{ML_ind "#>>"},
+ @{ML_ind "##>"} and @{ML_ind "##>>"}.
+ Using @{ML_ind "#->"}, for example, the function @{text double} can also be written as:
*}
ML{*val double =
@@ -627,7 +625,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_ind [index] check_terms in Syntax}, whose purpose is to type-check a list
+ @{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
of terms.
@{ML_response_fake [display, gray]
@@ -690,7 +688,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_ind [index] theory_name in Context}.
+ the function @{ML_ind 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 +736,7 @@
end*}
text {*
- The function @{ML_ind [index] dest_ss in MetaSimplifier} returns a record containing all
+ The function @{ML_ind 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}"}.
@@ -761,7 +759,7 @@
"name"}
An example where a qualified name is needed is the function
- @{ML_ind [index] define in LocalTheory}. This function is used below to define
+ @{ML_ind define in LocalTheory}. This function is used below to define
the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
@@ -788,7 +786,7 @@
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]
+ this restriction, you can implement your own using the function @{ML_ind
ML_Antiquote.inline}. The code is as follows.
*}
@@ -801,7 +799,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_ind [index] read_term_pattern in
+ transformed into a term using the function @{ML_ind 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.
@@ -845,7 +843,7 @@
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
will show the term @{term "(a::nat) + b = c"}, but printed using the internal
- representation corresponding to the datatype @{ML_type [index] "term"} defined as follows:
+ representation corresponding to the datatype @{ML_type "term"} defined as follows:
*}
ML_val %linenosgray{*datatype term =
@@ -1045,7 +1043,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_ind [index] list_comb}, which takes a term
+ constructing terms. One is the function @{ML_ind 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
@@ -1058,7 +1056,7 @@
end"
"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
- Another handy function is @{ML_ind [index] lambda}, which abstracts a variable
+ Another handy function is @{ML_ind lambda}, which abstracts a variable
in a term. For example
@{ML_response_fake [display,gray]
@@ -1091,7 +1089,7 @@
of Church-style typing, where variables with the same name still differ, if they
have different type.
- There is also the function @{ML_ind [index] subst_free} with which terms can be
+ There is also the function @{ML_ind 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}.
@@ -1118,7 +1116,7 @@
end"
"Free (\"x\", \"nat\")"}
- Similarly the function @{ML_ind [index] subst_bounds}, replaces lose bound
+ Similarly the function @{ML_ind 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.
*}
@@ -1137,7 +1135,7 @@
Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
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]
+ the function @{ML subst_bounds}, you can replace these lose @{ML_ind
Bound}s with the stripped off variables.
@{ML_response_fake [display, gray, linenos]
@@ -1156,7 +1154,7 @@
and so on.
There are many convenient functions that construct specific HOL-terms. For
- example @{ML_ind [index] mk_eq in HOLogic} constructs an equality out of two terms.
+ example @{ML_ind 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
@@ -1270,8 +1268,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_ind [index] "Sign.extern_const"} or
- @{ML_ind [index] Long_Name.base_name}. For example:
+ constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or
+ @{ML_ind Long_Name.base_name}. For example:
@{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
@@ -1293,19 +1291,19 @@
ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-text {* This can be equally written with the combinator @{ML_ind [index] "-->"} as: *}
+text {* This can be equally written with the combinator @{ML_ind "-->"} 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_ind [index] "--->"}.
+ type, then you can use @{ML_ind "--->"}.
*}
ML{*fun make_fun_types tys ty = tys ---> ty *}
text {*
- A handy function for manipulating terms is @{ML_ind [index] map_types}: it takes a
+ A handy function for manipulating terms is @{ML_ind 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:
*}
@@ -1325,8 +1323,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_ind [index] add_tfrees in Term}
- (similarly @{ML_ind [index] add_tvars in Term} for the schematic type-variables).
+ can use the function @{ML_ind add_tfrees in Term}
+ (similarly @{ML_ind 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
@@ -1395,8 +1393,8 @@
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_ind [index] cterm_of}, which
- converts a @{ML_type [index] term} into a @{ML_type [index] cterm}, a \emph{certified}
+ a theory. Type-checking is done via the function @{ML_ind cterm_of}, which
+ converts a @{ML_type term} into a @{ML_type 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
be constructed via ``official interfaces''.
@@ -1450,7 +1448,7 @@
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_ind [index] type_of} returns the
+ Given a well-typed term, the function @{ML_ind type_of} returns the
type of a term. Consider for example:
@{ML_response [display,gray]
@@ -1465,7 +1463,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_ind [index] fastype_of}, which
+ not necessary, there is the function @{ML_ind fastype_of}, which
also returns the type of a term.
@{ML_response [display,gray]
@@ -1482,7 +1480,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_ind [index] dummyT} and then let type-inference figure out the
+ type @{ML_ind dummyT} and then let type-inference figure out the
complete type. An example is as follows:
@{ML_response_fake [display,gray]
@@ -1579,7 +1577,7 @@
@{ML_file "Pure/thm.ML"}.
\end{readmore}
- (FIXME: handy functions working on theorems, like @{ML_ind [index] rulify in ObjectLogic} and so on)
+ (FIXME: handy functions working on theorems, like @{ML_ind rulify in ObjectLogic} and so on)
(FIXME: how to add case-names to goal states - maybe in the
next section)
@@ -1623,7 +1621,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_ind [index] add_consts_i in Sign}.
+ constant on the ML-level is @{ML_ind add_consts_i in Sign}.
If you write\footnote{Recall that ML-code needs to be
enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
*}
@@ -1701,11 +1699,11 @@
ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
text {*
- where the function @{ML_ind [index] rule_attribute in Thm} expects a function taking a
+ where the function @{ML_ind 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_ind [index] "RS"}
- is explained in Section~\ref{sec:simpletacs}.} The function
+ @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind "RS"}
+ is explained in Section~\ref{sec:simpletacs}). The function
@{ML rule_attribute in Thm} then returns an attribute.
Before we can use the attribute, we need to set it up. This can be done
@@ -1741,7 +1739,7 @@
@{text "> "}~@{thm test[my_sym]}
\end{isabelle}
- An alternative for setting up an attribute is the function @{ML_ind [index] setup in Attrib}.
+ An alternative for setting up an attribute is the function @{ML_ind setup in Attrib}.
So instead of using \isacommand{attribute\_setup}, you can also set up the
attribute as follows:
*}
@@ -1806,10 +1804,10 @@
you get an exception indicating that the theorem @{thm [source] sym}
does not resolve with meta-equations.
- The purpose of @{ML_ind [index] rule_attribute in Thm} is to directly manipulate theorems.
+ The purpose of @{ML_ind 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_ind [index] declaration_attribute in Thm}.
+ current simpset. For these applications, you can use @{ML_ind declaration_attribute in Thm}.
To illustrate this function, let us introduce a reference containing a list
of theorems.
*}
@@ -1838,9 +1836,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_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
+ @{ML_ind add_thm in Thm} adds a theorem if it is not already included in
+ the list, and @{ML_ind del_thm in Thm} deletes one (both functions use the
+ predicate @{ML_ind 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
@@ -1858,7 +1856,7 @@
"maintaining a list of my_thms - rough test only!"
text {*
- The parser @{ML_ind [index] add_del in Attrib} is a predefined parser for
+ The parser @{ML_ind 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]"}
*}
@@ -1886,7 +1884,7 @@
"[\"True\", \"Suc (Suc 0) = 2\"]"}
The theorem @{thm [source] trueI_2} only appears once, since the
- function @{ML_ind [index] add_thm in Thm} tests for duplicates, before extending
+ function @{ML_ind add_thm in Thm} tests for duplicates, before extending
the list. Deletion from the list works as follows:
*}
@@ -1898,7 +1896,7 @@
"!my_thms"
"[\"True\"]"}
- We used in this example two functions declared as @{ML_ind [index] declaration_attribute in Thm},
+ We used in this example two functions declared as @{ML_ind declaration_attribute in Thm},
but there can be any number of them. We just have to change the parser for reading
the arguments accordingly.
@@ -2127,7 +2125,7 @@
section {* Storing Theorems\label{sec:storing} (TBD) *}
-text {* @{ML_ind [index] add_thms_dynamic in PureThy} *}
+text {* @{ML_ind add_thms_dynamic in PureThy} *}
local_setup %gray {*
LocalTheory.note Thm.theoremK
@@ -2173,7 +2171,7 @@
its functions do not operate on @{ML_type string}s, but on instances of the
type:
- @{ML_type [display, gray, index] "Pretty.T"}
+ @{ML_type_ind [display, gray] "Pretty.T"}
The function @{ML str in Pretty} transforms a (plain) string into such a pretty
type. For example
@@ -2186,7 +2184,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_ind [index] string_of in Pretty}. In what
+ string}. This can be done with the function @{ML_ind string_of in Pretty}. In what
follows we will use the following wrapper function for printing a pretty
type:
*}
@@ -2231,10 +2229,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_ind [index] breaks in Pretty}, which expects a list of pretty types and inserts a
+ @{ML_ind 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_ind [index] blk in Pretty} as follows:
+ with the function @{ML_ind blk in Pretty} as follows:
@{ML_response_fake [display,gray]
@@ -2249,7 +2247,7 @@
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
Here the layout of @{ML test_str} is much more pleasing to the
- eye. The @{ML "0"} in @{ML_ind [index] blk in Pretty} stands for no indentation
+ eye. The @{ML "0"} in @{ML_ind blk in Pretty} stands for no indentation
of the printed string. You can increase the indentation and obtain
@{ML_response_fake [display,gray]
@@ -2265,7 +2263,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_ind [index] indent in Pretty} as follows:
+ function @{ML_ind indent in Pretty} as follows:
@{ML_response_fake [display,gray]
"let
@@ -2280,7 +2278,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_ind [index] commas in Pretty}. For example
+ @{ML_ind commas in Pretty}. For example
@{ML_response_fake [display,gray]
"let
@@ -2295,7 +2293,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_ind [index] enum in Pretty}. For example
+ @{ML_ind enum in Pretty}. For example
*}
text {*
@@ -2366,8 +2364,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_ind [index] pretty_term in Syntax} and @{ML_ind [index]
- pretty_typ in Syntax}. We also use the function @{ML_ind [index] quote in
+ using the functions @{ML_ind pretty_term in Syntax} and @{ML_ind
+ pretty_typ in Syntax}. We also use the function @{ML_ind 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.
--- a/ProgTutorial/Package/Ind_Code.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy Thu Aug 20 22:30:20 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_ind [index] define in LocalTheory}. The wrapper takes a predicate name, a syntax
+ @{ML_ind 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_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
+ definition has been made. In Line 4, @{ML_ind internalK in Thm} is a flag
+ attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm}
+ and @{ML_ind 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_ind [index] empty_binding in Attrib} in Line 3, since the definitions for
+ also use @{ML_ind 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_ind [index] theory_of in ProofContext}
+ behind the local theory using the function @{ML_ind theory_of in ProofContext}
(Line 3); with this theory we can use the function
- @{ML_ind [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
+ @{ML_ind 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_ind [index]
+ In Line 11 we set up the goal to be proved using the function @{ML_ind
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_ind [index] subst_free}. Line 14 and 15 just iterate
+ (Line 11) using the function @{ML_ind 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_ind [index] SUBPROOF}, since this tactic provides us with the parameters (as
+ tactic @{ML_ind 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_ind [index] FOCUS in Subgoal}, which does s
+ we use first the function @{ML_ind 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_ind [index] chop}.
+ separate them using the function @{ML_ind 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_ind [index] rulify in ObjectLogic}). So we can modify the
+ format (using @{ML_ind 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_ind [index] MRS} does nothing. Similarly, in the
+ just the empty list and the function @{ML_ind 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_ind [index] map_index} since we
+ The iteration is done with the function @{ML_ind 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_ind [index] note in LocalTheory} does.
+ @{ML_ind 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_ind [index] case_names in RuleCases}
+ to use some specific attributes. The first @{ML_ind 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 14:19:39 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy Thu Aug 20 22:30:20 2009 +0200
@@ -138,8 +138,8 @@
OuterKeyword.thy_decl specification*}
text {*
- 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
+ We call @{ML_ind local_theory in OuterSyntax} with the kind-indicator
+ @{ML_ind 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_ind [index] read_spec in Specification}. This function takes some strings
+ function @{ML_ind 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/Package/Simple_Inductive_Package.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Thu Aug 20 22:30:20 2009 +0200
@@ -54,7 +54,7 @@
thm rel.accpart'.induct
*)
-use_chunks "simple_inductive_package.ML"
+use "simple_inductive_package.ML"
end
--- a/ProgTutorial/Parsing.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Parsing.thy Thu Aug 20 22:30:20 2009 +0200
@@ -37,7 +37,7 @@
text {*
Let us first have a look at parsing strings using generic parsing
- combinators. The function @{ML_ind [index] "$$"} takes a string as argument and will
+ combinators. The function @{ML_ind "$$"} 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:
@@ -71,11 +71,9 @@
However, note that these exceptions are private to the parser and cannot be accessed
by the programmer (for example to handle them).
- \indexdef{explode@ {\tt\slshape{}explode}}{in {\tt\slshape Symbol}}
- \index{explode@ {\tt\slshape{}explode}}
- In the examples above we use the function @{ML Symbol.explode}, instead of the
- more standard library function @{ML explode}, for obtaining an input list for
- the parser. The reason is that @{ML Symbol.explode} is aware of character sequences,
+ In the examples above we use the function @{ML_ind Symbol.explode}, instead of the
+ more standard library function @{ML_ind explode}, for obtaining an input list for
+ the parser. The reason is that @{ML_ind Symbol.explode} is aware of character sequences,
for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see
the difference consider
@@ -89,7 +87,7 @@
[\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
Slightly more general than the parser @{ML "$$"} is the function
- @{ML_ind [index] one in Scan}, in that it takes a predicate as argument and
+ @{ML_ind 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 +103,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- Two parsers can be connected in sequence by using the function @{ML_ind [index] "--"}.
+ Two parsers can be connected in sequence by using the function @{ML_ind "--"}.
For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
order) you can achieve by:
@@ -116,14 +114,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_ind [index] this_string in Scan}:
+ then you should use the function @{ML_ind 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_ind [index] "||"}. The parser @{ML "(p || q)" for p q} returns the
+ @{ML_ind "||"}. 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 +136,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- The functions @{ML_ind [index] "|--"} and @{ML_ind [index] "--|"} work like the sequencing function
+ The functions @{ML_ind "|--"} and @{ML_ind "--|"} work like the sequencing function
for parsers, except that they discard the item being parsed by the first (respectively second)
parser. For example:
@@ -152,7 +150,6 @@
end"
"((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
- \indexdef{optional@ {\tt\slshape{optional}}}{in {\tt\slshape Scan}}
The parser @{ML "Scan.optional p x" for p x} returns the result of the parser
@{text "p"}, if it succeeds; otherwise it returns
the default value @{text "x"}. For example:
@@ -167,7 +164,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML_ind [index] option in Scan} works similarly, except no default value can
+ The function @{ML_ind 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 +176,7 @@
(p input1, p input2)
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML_ind [index] "!!"} helps to produce appropriate error messages
+ The function @{ML_ind "!!"} 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 +212,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_ind [index] error in Scan}. For example:
+ @{ML_ind 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_ind [index] local_theory in OuterSyntax}
+ This ``prefixing'' is usually done by wrappers such as @{ML_ind 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 +255,14 @@
@{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
- 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"}
+ Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
+ @{ML_ind 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_ind [index] finite in Scan} and the ``stopper-token''
- @{ML_ind [index] stopper in Symbol}. With them you can write:
+ the wrapper @{ML_ind finite in Scan} and the ``stopper-token''
+ @{ML_ind 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 +271,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_ind [index] repeat in Scan} can be used with @{ML_ind [index] one in Scan} to read any
+ The function @{ML_ind repeat in Scan} can be used with @{ML_ind one in Scan} to read any
string as in
@{ML_response [display,gray]
@@ -286,10 +283,10 @@
end"
"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
- where the function @{ML_ind [index] not_eof in Symbol} ensures that we do not read beyond the
+ where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
- The function @{ML_ind [index] unless in Scan} takes two parsers: if the first one can
+ The function @{ML_ind 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 +299,7 @@
succeeds.
- The functions @{ML_ind [index] repeat in Scan} and @{ML_ind [index] unless in Scan} can
+ The functions @{ML_ind repeat in Scan} and @{ML_ind 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 +317,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_ind [index]">>"} where
+ items. One way to do this is the function @{ML_ind ">>"} 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 +346,14 @@
(FIXME: move to an earlier place)
- The function @{ML_ind [index] ahead in Scan} parses some input, but leaves the original
+ The function @{ML_ind 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_ind [index] lift in Scan} takes a parser and a pair as arguments. This function applies
+ The function @{ML_ind 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
@@ -396,12 +393,12 @@
The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
\end{readmore}
- The structure @{ML_struct [index] OuterLex} defines several kinds of tokens (for
- 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
+ The structure @{ML_struct OuterLex} defines several kinds of tokens (for
+ example @{ML_ind Ident in OuterLex} for identifiers, @{ML Keyword in
+ OuterLex} for keywords and @{ML_ind 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_ind [index] scan in OuterSyntax}. It is given the argument
+ @{ML_ind 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 +416,7 @@
other syntactic category. The second indicates a space.
We can easily change what is recognised as a keyword with
- @{ML_ind [index] keyword in OuterKeyword}. For example calling this function
+ @{ML_ind keyword in OuterKeyword}. For example calling this function
*}
ML{*val _ = OuterKeyword.keyword "hello"*}
@@ -434,7 +431,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_ind [index] is_proper in OuterLex} to do this.
+ functions @{ML filter} and @{ML_ind is_proper in OuterLex} to do this.
For example:
@{ML_response_fake [display,gray]
@@ -472,10 +469,10 @@
end"
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
- You might have to adjust the @{ML_ind [index] print_depth} in order to
+ You might have to adjust the @{ML_ind print_depth} in order to
see the complete list.
- The parser @{ML_ind [index] "$$$" in OuterParse} parses a single keyword. For example:
+ The parser @{ML_ind "$$$" in OuterParse} parses a single keyword. For example:
@{ML_response [display,gray]
"let
@@ -486,7 +483,7 @@
end"
"((\"where\",\<dots>), (\"|\",\<dots>))"}
- Any non-keyword string can be parsed with the function @{ML_ind [index] reserved in OuterParse}.
+ Any non-keyword string can be parsed with the function @{ML_ind reserved in OuterParse}.
For example:
@{ML_response [display,gray]
@@ -498,7 +495,7 @@
end"
"(\"bar\",[])"}
- Like before, you can sequentially connect parsers with @{ML_ind [index] "--"}. For example:
+ Like before, you can sequentially connect parsers with @{ML_ind "--"}. For example:
@{ML_response [display,gray]
"let
@@ -508,7 +505,6 @@
end"
"((\"|\", \"in\"), [])"}
- \indexdef{enum@ {\tt\slshape{enum}}}{in {\tt\slshape OuterParse}}
The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty
list of items recognised by the parser @{text p}, where the items being parsed
are separated by the string @{text s}. For example:
@@ -521,7 +517,7 @@
end"
"([\"in\", \"in\", \"in\"], [\<dots>])"}
- @{ML_ind [index] enum1 in OuterParse} works similarly, except that the parsed list must
+ @{ML_ind 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 +541,7 @@
text {*
- The function @{ML_ind [index] "!!!" in OuterParse} can be used to force termination of the
+ The function @{ML_ind "!!!" 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 +560,7 @@
\begin{exercise} (FIXME)
A type-identifier, for example @{typ "'a"}, is a token of
- kind @{ML_ind [index] Keyword in OuterLex}. It can be parsed using
+ kind @{ML_ind Keyword in OuterLex}. It can be parsed using
the function @{ML type_ident in OuterParse}.
\end{exercise}
@@ -626,7 +622,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_ind [index] term in OuterParse}. For example:
+ be parsed using the function @{ML_ind term in OuterParse}. For example:
@{ML_response [display,gray]
"let
@@ -636,10 +632,10 @@
end"
"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
- The function @{ML_ind [index] prop in OuterParse} is similar, except that it gives a different
+ The function @{ML_ind 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_ind [index] parse in YXML}. For example
+ information with the function @{ML_ind parse in YXML}. For example
@{ML_response [display,gray]
"YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
@@ -723,7 +719,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_ind [index] "fixes" in OuterParse} in Line 2 of the parser reads an
+ The function @{ML_ind "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 +743,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_ind [index] Mixfix} data structure;
- no syntax translation is indicated by @{ML_ind [index] NoSyn}.
+ present for a variable, then it is stored in the @{ML_ind Mixfix} data structure;
+ no syntax translation is indicated by @{ML_ind NoSyn}.
\begin{readmore}
The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
@@ -757,7 +753,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_ind [index] prop in OuterParse}. However, they can include an optional
+ parsed by @{ML_ind prop in OuterParse}. However, they can include an optional
theorem name plus some attributes. For example
@{ML_response [display,gray] "let
@@ -767,8 +763,8 @@
(name, map Args.dest_src attrib)
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
- 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
+ The function @{ML_ind opt_thm_name in SpecParse} is the ``optional'' variant of
+ @{ML_ind 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 +779,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_ind [index] where_alt_specs in SpecParse} adapted to our
+ we paraphrase the code of @{ML_ind where_alt_specs in SpecParse} adapted to our
purposes.
\begin{isabelle}
*}
@@ -834,7 +830,7 @@
end *}
text {*
- The crucial function @{ML_ind [index] local_theory in OuterSyntax} expects a name for the command, a
+ The crucial function @{ML_ind 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 +970,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_ind [index] succeed in Scan} does not parse any argument, but immediately
+ because of @{ML_ind 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 +1000,7 @@
and see the proposition in the tracing buffer.
- Note that so far we used @{ML_ind [index] thy_decl in OuterKeyword} as the kind
+ Note that so far we used @{ML_ind 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 +1008,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_ind [index] thy_goal in OuterKeyword} and the function @{ML
+ the kind indicator @{ML_ind 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 +1037,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_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
+ @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
+ In Line 6 the function @{ML_ind 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 +1062,7 @@
\isacommand{done}
\end{isabelle}
- (FIXME: read a name and show how to store theorems; see @{ML_ind [index] note in LocalTheory})
+ (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
*}
@@ -1099,7 +1095,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_ind [index] SIMPLE_METHOD}
+ @{ML_ind SIMPLE_METHOD}
turns such a tactic into a method. The method @{text "foo"} can be used as follows
*}
--- a/ProgTutorial/Solutions.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Solutions.thy Thu Aug 20 22:30:20 2009 +0200
@@ -11,7 +11,7 @@
| rev_sum t = t *}
text {*
- An alternative solution using the function @{ML [index] mk_binop in HOLogic} is:
+ An alternative solution using the function @{ML_ind mk_binop in HOLogic} is:
*}
ML{*fun rev_sum t =
--- a/ProgTutorial/Tactical.thy Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Tactical.thy Thu Aug 20 22:30:20 2009 +0200
@@ -56,13 +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_ind [index] etac}, @{ML_ind [index] rtac} and @{ML_ind [index] atac}
+ The tactics @{ML_ind etac}, @{ML_ind rtac} and @{ML_ind atac}
in the code above correspond
roughly to @{text erule}, @{text rule} and @{text assumption}, respectively.
- The operator @{ML_ind [index] THEN} strings the tactics together.
+ The operator @{ML_ind THEN} strings the tactics together.
\begin{readmore}
- To learn more about the function @{ML_ind [index] prove in Goal} see \isccite{sec:results}
+ To learn more about the function @{ML_ind 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
@@ -120,7 +120,7 @@
THEN' atac)*}text_raw{*\label{tac:footacprime}*}
text {*
- where @{ML_ind [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+ where @{ML_ind 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.
@@ -161,7 +161,7 @@
willy-nilly; only in very grave failure situations should a tactic raise the
exception @{text THM}.
- The simplest tactics are @{ML_ind [index] no_tac} and @{ML_ind [index] all_tac}. The first returns
+ The simplest tactics are @{ML_ind no_tac} and @{ML_ind all_tac}. The first returns
the empty sequence and is defined as
*}
@@ -336,7 +336,7 @@
section {* Simple Tactics\label{sec:simpletacs} *}
text {*
- Let us start with explaining the simple tactic @{ML_ind [index] print_tac}, which is quite useful
+ Let us start with explaining the simple tactic @{ML_ind 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
@@ -356,7 +356,7 @@
text {*
A simple tactic for easy discharge of any proof obligations is
- @{ML_ind [index] cheat_tac in SkipProof}. This tactic corresponds to
+ @{ML_ind cheat_tac in SkipProof}. This tactic corresponds to
the Isabelle command \isacommand{sorry} and is sometimes useful
during the development of tactics.
*}
@@ -372,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_ind [index] atac}, which, as shown in the previous
+ Another simple tactic is the function @{ML_ind atac}, which, as shown in the previous
section, corresponds to the assumption command.
*}
@@ -384,8 +384,8 @@
(*<*)oops(*>*)
text {*
- Similarly, @{ML_ind [index] rtac}, @{ML_ind [index] dtac}, @{ML_ind [index] etac} and
- @{ML_ind [index] ftac} correspond (roughly)
+ Similarly, @{ML_ind rtac}, @{ML_ind dtac}, @{ML_ind etac} and
+ @{ML_ind 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.
@@ -413,7 +413,7 @@
(*<*)oops(*>*)
text {*
- The function @{ML_ind [index] resolve_tac} is similar to @{ML_ind [index] rtac}, except that it
+ The function @{ML_ind resolve_tac} is similar to @{ML_ind 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
@@ -436,11 +436,11 @@
text {*
Similar versions taking a list of theorems exist for the tactics
- @{ML dtac} (@{ML_ind [index] dresolve_tac}), @{ML etac}
- (@{ML_ind [index] eresolve_tac}) and so on.
+ @{ML dtac} (@{ML_ind dresolve_tac}), @{ML etac}
+ (@{ML_ind eresolve_tac}) and so on.
- Another simple tactic is @{ML_ind [index] cut_facts_tac}. It inserts a list of theorems
+ Another simple tactic is @{ML_ind cut_facts_tac}. It inserts a list of theorems
into the assumptions of the current goal state. For example
*}
@@ -475,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_ind [index] "RS"}
+ @{ML_ind "RS"}
@{ML_response_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
@@ -489,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_ind [index] RSN} is similar to @{ML RS}, but
+ then the function raises an exception. The function @{ML_ind RSN} is similar to @{ML RS}, but
takes an additional number as argument that makes explicit which premise
should be instantiated.
@@ -502,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_ind [index] MRS}:
+ the function @{ML_ind 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_ind [index] MRL}. For example in the code below,
+ functions @{ML RL} and @{ML_ind MRL}. For example in the code below,
every theorem in the second list is instantiated with every
theorem in the first.
@@ -528,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_ind [index] FOCUS in Subgoal} and
- @{ML_ind [index] SUBPROOF}. These tactics fix the parameters
+ safety is provided by the functions @{ML_ind FOCUS in Subgoal} and
+ @{ML_ind 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
@@ -668,7 +668,7 @@
Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
@{ML SUBPROOF}, are
- @{ML_ind [index] SUBGOAL} and @{ML_ind [index] CSUBGOAL}. They allow you to
+ @{ML_ind SUBGOAL} and @{ML_ind 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
@@ -780,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_ind [index] EVERY'}. For example
+ sequence, you can use the combinator @{ML_ind EVERY'}. For example
the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
be written as:
*}
@@ -802,11 +802,11 @@
text {*
and call @{ML foo_tac1}.
- With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind [index] EVERY1} it must be
+ With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind 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_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
+ then you can use the combinator @{ML_ind ORELSE'} for two tactics, and @{ML_ind
+ FIRST'} (or @{ML_ind FIRST1}) for a list of tactics. For example, the tactic
*}
@@ -858,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_ind [index] ALLGOALS} that simplifies this. Using this combinator you can simply
+ @{ML_ind 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"
@@ -871,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_ind [index] TRY}.
+ list. The same can be achieved with the tactic combinator @{ML_ind TRY}.
For example:
*}
@@ -904,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_ind [index] CHANGED} to make sure the subgoal has been changed
+ use the combinator @{ML_ind CHANGED} to make sure the subgoal has been changed
by the tactic. Because now
*}
@@ -922,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_ind [index] REPEAT}. As an example
+ completely. For this you can use the tactic combinator @{ML_ind REPEAT}. As an example
suppose the following tactic
*}
@@ -943,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_ind [index] REPEAT1} is similar, but runs the tactic at least once (failing if
+ @{ML_ind 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
@@ -959,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_ind [index] REPEAT_ALL_NEW}.
+ resulting subgoals, you can use the tactic combinator @{ML_ind REPEAT_ALL_NEW}.
Suppose the tactic
*}
@@ -1012,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_ind [index] DETERM}.
+ combinator @{ML_ind DETERM}.
*}
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
@@ -1049,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_ind [index] TRY}. The tactic combinator @{ML_ind [index] TRYALL} will try out
+ no primed version of @{ML_ind TRY}. The tactic combinator @{ML_ind TRYALL} will try out
a tactic on all subgoals. For example the tactic
*}
@@ -1058,7 +1058,7 @@
text {*
will solve all trivial subgoals involving @{term True} or @{term "False"}.
- (FIXME: say something about @{ML_ind [index] COND} and COND')
+ (FIXME: say something about @{ML_ind COND} and COND')
(FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
@@ -1118,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_ind [index] DEPTH_SOLVE}, which searches
+ the rules, use the tactic combinator @{ML_ind 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}
@@ -1142,11 +1142,11 @@
\begin{isabelle}
\begin{center}
\begin{tabular}{l@ {\hspace{2cm}}l}
- @{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)"}
+ @{ML_ind simp_tac} & @{text "(simp (no_asm))"} \\
+ @{ML_ind asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
+ @{ML_ind full_simp_tac} & @{text "(simp (no_asm_use))"} \\
+ @{ML_ind asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
+ @{ML_ind asm_full_simp_tac} & @{text "(simp)"}
\end{tabular}
\end{center}
\end{isabelle}
@@ -1230,9 +1230,9 @@
\begin{isabelle}
\begin{tabular}{ll}
- @{ML_ind [index] addsimps} & @{ML_ind [index] delsimps}\\
- @{ML_ind [index] addcongs} & @{ML_ind [index] delcongs}\\
- @{ML_ind [index] addsimprocs} & @{ML_ind [index] delsimprocs}\\
+ @{ML_ind addsimps} & @{ML_ind delsimps}\\
+ @{ML_ind addcongs} & @{ML_ind delcongs}\\
+ @{ML_ind addsimprocs} & @{ML_ind delsimprocs}\\
\end{tabular}
\end{isabelle}
@@ -1262,7 +1262,7 @@
text_raw {*
\end{isabelle}
\end{minipage}
-\caption{The function @{ML_ind [index] dest_ss in Simplifier} returns a record containing
+\caption{The function @{ML_ind 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} *}
@@ -1270,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_ind [index] empty_ss}
+ empty simpset, i.e., @{ML_ind empty_ss}
@{ML_response_fake [display,gray]
"print_ss @{context} empty_ss"
@@ -1317,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_ind [index] HOL_basic_ss}. While
+ In the context of HOL, the first really useful simpset is @{ML_ind HOL_basic_ss}. While
printing out the components of this simpset
@{ML_response_fake [display,gray]
@@ -1344,9 +1344,9 @@
text {*
This behaviour is not because of simplification rules, but how the subgoaler, solver
- and looper are set up in @{ML_ind [index] HOL_basic_ss}.
+ and looper are set up in @{ML_ind HOL_basic_ss}.
- The simpset @{ML_ind [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing
+ The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing
already many useful simplification and congruence rules for the logical
connectives in HOL.
@@ -1366,7 +1366,7 @@
The simplifier is often used to unfold definitions in a proof. For this the
- simplifier implements the tactic @{ML_ind [index] rewrite_goals_tac}.\footnote{FIXME:
+ simplifier implements the tactic @{ML_ind rewrite_goals_tac}.\footnote{FIXME:
see LocalDefs infrastructure.} Suppose for example the
definition
*}
@@ -1680,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_ind [index] addsimprocs} to a simpset whenever
+ @{ML_ind addsimprocs} to a simpset whenever
needed.
Simprocs are applied from inside to outside and from left to right. You can
@@ -1766,7 +1766,7 @@
| dest_suc_trm t = snd (HOLogic.dest_number t)*}
text {*
- It uses the library function @{ML_ind [index] dest_number in HOLogic} that transforms
+ It uses the library function @{ML_ind 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
@@ -1886,21 +1886,21 @@
text {*
whereby the produced theorem is always a meta-equality. A simple conversion
- is the function @{ML_ind [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
+ is the function @{ML_ind 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_ind [index] no_conv in Conv} which always raises the
+ Another simple conversion is @{ML_ind 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_ind [index] beta_conversion in Thm}: it
+ A more interesting conversion is the function @{ML_ind beta_conversion in Thm}: it
produces a meta-equation between a term and its beta-normal form. For example
@{ML_response_fake [display,gray]
@@ -1942,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_ind [index] rewr_conv in Conv}, which expects a meta-equation as an
+ @{ML_ind rewr_conv in Conv}, which expects a meta-equation as an
argument. Suppose the following meta-equation.
*}
@@ -1961,15 +1961,15 @@
end"
"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
- Note, however, that the function @{ML_ind [index] rewr_conv in Conv} only rewrites the
+ Note, however, that the function @{ML_ind 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_ind [index] rewr_conv in Conv} fails, raising
+ left-hand side of the theorem, then @{ML_ind 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_ind [index] then_conv},
+ combinators. The simplest conversion combinator is @{ML_ind then_conv},
which applies one conversion after another. For example
@{ML_response_fake [display,gray]
@@ -1986,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_ind [index] else_conv} tries out the
+ The conversion combinator @{ML_ind else_conv} tries out the
first one, and if it does not apply, tries the second. For example
@{ML_response_fake [display,gray]
@@ -2004,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_ind [index] try_conv in Conv} constructs a conversion
+ The conversion combinator @{ML_ind try_conv in Conv} constructs a conversion
which is tried out on a term, but in case of failure just does nothing.
For example
@@ -2020,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_ind [index] fun_conv in Conv}
- and @{ML_ind [index] arg_conv in Conv} will apply
+ will lift this restriction. The combinators @{ML_ind fun_conv in Conv}
+ and @{ML_ind arg_conv in Conv} will apply
a conversion to the first, respectively second, argument of an application.
For example
@@ -2040,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_ind [index] abs_conv in Conv} applies a conversion under an
+ The function @{ML_ind abs_conv in Conv} applies a conversion under an
abstraction. For example:
@{ML_response_fake [display,gray]
@@ -2056,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_ind [index] combination_conv in Conv}. It expects two
+ an application is @{ML_ind 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_ind [index] comb_conv in Conv}, which applies the same conversion
+ function @{ML_ind comb_conv in Conv}, which applies the same conversion
to both branches.
We can now apply all these functions in a conversion that recursively
@@ -2124,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_ind [index] fconv_rule in Conv}. As an example,
+ also work on theorems using the function @{ML_ind fconv_rule in Conv}. As an example,
consider the conversion @{ML all_true1_conv} and the lemma:
*}
@@ -2144,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_ind [index] CONVERSION},
+ goal states. This can be done with the help of the function @{ML_ind CONVERSION},
and also some predefined conversion combinators that traverse a goal
state. The combinators for the goal state are:
\begin{itemize}
- \item @{ML_ind [index] params_conv in Conv} for converting under parameters
+ \item @{ML_ind 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_ind [index] prems_conv in Conv} for applying a conversion to all
+ \item @{ML_ind prems_conv in Conv} for applying a conversion to all
premises of a goal, and
- \item @{ML_ind [index] concl_conv in Conv} for applying a conversion to the
+ \item @{ML_ind concl_conv in Conv} for applying a conversion to the
conclusion of a goal.
\end{itemize}
--- a/ProgTutorial/antiquote_setup.ML Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML Thu Aug 20 22:30:20 2009 +0200
@@ -6,84 +6,84 @@
open OutputTutorial
(* functions for generating appropriate expressions *)
-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 istruct of
- NONE => ml_val_open_aux ys txt
- | SOME st => ml_val_open_aux ys ("let open " ^ st ^ " in " ^ txt ^ " end"))
-end
+fun translate_string f str =
+ implode (map f (Symbol.explode str))
+
+fun prefix_lines prfx txt =
+ map (fn s => prfx ^ s) (split_lines txt)
-fun ml_val txt = ml_val_open [] NONE txt;
-fun ml_val_ind istruct txt = ml_val_open [] istruct txt;
+fun ml_with_vars ys txt =
+ implode ["fn ", (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)), " => (", txt, ")"]
+
+fun ml_with_struct (NONE) txt = txt
+ | ml_with_struct (SOME st) txt = implode ["let open ", st, " in ", txt, " end"]
+
+fun ml_val vs stru txt =
+ txt |> ml_with_struct stru
+ |> ml_with_vars vs
fun ml_pat (lhs, pat) =
- let
- val pat' = implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
- in "val " ^ pat' ^ " = " ^ lhs end;
+ implode ["val ", translate_string (fn "\<dots>" => "_" | s => s) pat, " = ", lhs]
-fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end";
-fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option";
+fun ml_struct txt =
+ implode ["functor DUMMY_FUNCTOR() = struct structure DUMMY = ", txt, " end"]
+
+fun ml_type txt =
+ implode ["val _ = NONE : (", txt, ") option"];
(* eval function *)
fun eval_fn ctxt exp =
ML_Context.eval_in (SOME ctxt) false Position.none exp
-(* string functions *)
-fun string_explode prefix_str txt =
- map (fn s => prefix_str ^ s) (split_lines txt)
-
-val transform_cmts_str =
- Source.of_string
- #> ML_Lex.source
- #> Source.exhaust
- #> Chunks.transform_cmts
- #> implode
- #> string_explode ""
-
(* 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); output (string_explode "" txt))
+fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
+ (eval_fn ctxt (ml_val vs stru txt);
+ output (split_lines 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})
+(* checks and prints a single ML-item and produces an index entry *)
+fun output_ml_ind {context = ctxt, ...} (txt, stru) =
+ (eval_fn ctxt (ml_val [] stru txt);
+ case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
+ (NONE, bn, "") => output_indexed {main = Code txt, minor = NoString} (split_lines txt)
+ | (NONE, bn, qn) => output_indexed {main = Code bn, minor = Struct qn} (split_lines txt)
+ | (SOME st, _, _) => output_indexed {main = Code txt, minor = Struct st} (split_lines txt))
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 =
- (eval_fn ctxt (ml_struct txt);
- output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "structure"})
+(* checks and prints structures *)
+fun gen_output_struct outfn {context = ctxt, ...} txt =
+ (eval_fn ctxt (ml_struct txt);
+ outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
+
+val output_struct = gen_output_struct (K output)
+val output_struct_ind = gen_output_struct output_indexed
-fun output_type {context = ctxt, ...} txt =
- (eval_fn ctxt (ml_type txt);
- output_indexed (string_explode "" txt) {main = Code txt, minor = Plain "type"})
+(* checks and prints types *)
+fun gen_output_type outfn {context = ctxt, ...} txt =
+ (eval_fn ctxt (ml_type txt);
+ outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
+
+val output_type = gen_output_type (K output)
+val output_type_ind = gen_output_type output_indexed
(* checks and expression agains a result pattern *)
fun output_response {context = ctxt, ...} (lhs, pat) =
(eval_fn ctxt (ml_pat (lhs, pat));
- output ((string_explode "" lhs) @ (string_explode "> " pat)))
+ output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
fun output_response_fake {context = ctxt, ...} (lhs, pat) =
- (eval_fn ctxt (ml_val lhs);
- output ((string_explode "" lhs) @ (string_explode "> " pat)))
+ (eval_fn ctxt (ml_val [] NONE lhs);
+ output ((split_lines lhs) @ (prefix_lines "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
fun ouput_response_fake_both _ (lhs, pat) =
- output ((string_explode "" lhs) @ (string_explode "> " pat))
+ output ((split_lines lhs) @ (prefix_lines "> " pat))
val single_arg = Scan.lift (Args.name)
val two_args = Scan.lift (Args.name -- Args.name)
@@ -91,7 +91,9 @@
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_type_ind" single_arg output_type_ind
val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
+val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
val _ = ThyOutput.antiquotation "ML_response" two_args output_response
val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
@@ -101,14 +103,15 @@
val raw = Symbol.encode_raw
val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"
in
- (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")
+ implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
end
(* checks whether a file exists in the Isabelle distribution *)
fun check_file_exists _ txt =
(if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt))
then output [href_link txt]
- else error ("Source file " ^ (quote txt) ^ " does not exist."))
+ else error (implode ["Source file ", quote txt, " does not exist."]))
+
val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
@@ -150,7 +153,6 @@
ThyOutput.output output
end
-
val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
--- a/ProgTutorial/document/root.tex Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/document/root.tex Thu Aug 20 22:30:20 2009 +0200
@@ -27,7 +27,6 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% indexing
\makeindex
-\newcommand{\indexdef}[2]{\index{#1 (#2)}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% For cross references to the other manuals:
--- a/ProgTutorial/output_tutorial.ML Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/output_tutorial.ML Thu Aug 20 22:30:20 2009 +0200
@@ -3,7 +3,7 @@
struct
(* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos, index] *)
+(* enable the options [gray, linenos] *)
val gray = ref false
val linenos = ref false
@@ -27,22 +27,15 @@
#> enclose "\\isa{" "}")
end
-datatype qstring =
+datatype indstring =
NoString
| Plain of string
| Code of string
-| IStruct of string
+| Struct of string
-datatype entry =
- No_Entry
- | Default
- | Explicit of string
+fun translate_string f = Symbol.explode #> map f #> implode;
-val index = ref No_Entry
-
-fun translate f = Symbol.explode #> map f #> implode;
-
-val clean_string = translate
+val clean_string = translate_string
(fn "_" => "\\_"
| "#" => "\\#"
| "<" => "\\isacharless"
@@ -53,7 +46,7 @@
| "$" => "\\isachardollar"
| "!" => "\\isacharbang"
| "\<dash>" => "-"
- | c => c);
+ | c => c)
fun get_word str =
let
@@ -61,47 +54,32 @@
| only_letters (x::xs) =
if (Symbol.is_ascii_blank x) then false else only_letters xs
in
- if (only_letters (Symbol.explode str)) then (clean_string str)
- else error ("Underspecified index entry only for single words allowed! Error with " ^ quote str)
+ if only_letters (Symbol.explode str)
+ then clean_string str
+ else error ("Only single word allowed! Error with " ^ quote str)
end
-fun get_qstring NoString = ""
- | get_qstring (Plain s) = get_word s
- | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end
- | get_qstring (IStruct s) = "in {\\tt\\slshape{}" ^ (get_word s) ^ "}"
+fun get_indstring NoString = ""
+ | get_indstring (Plain s) = get_word s
+ | get_indstring (Code s) = let val w = get_word s in implode[w, "@{\\tt\\slshape{}", w, "}"] end
+ | get_indstring (Struct s) = implode ["in {\\tt\\slshape{}", get_word s, "}"]
-fun is_empty_qstr (Plain "") = true
- | is_empty_qstr (Code "") = true
- | is_empty_qstr _ = false
-
-fun get_index_info {main = m, minor = n} =
+fun get_index {main = m, minor = n} =
(if n = NoString
- then "\\index{" ^ (get_qstring m) ^ "}"
- else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ (get_qstring n) ^ "}")
+ then implode ["\\index{", get_indstring m, "}"]
+ else implode ["\\index{", get_indstring m, " (", get_indstring n, ")}"])
-fun index_entry entry index_info =
- case entry of
- No_Entry => I
- | Explicit s => prefix s
- | Default => prefix (get_index_info index_info)
-
-fun output_indexed txt index_info =
+fun output_indexed ind txt =
txt |> output
- |> index_entry (!index) index_info
+ |> prefix (get_index ind)
fun boolean "" = true
| boolean "true" = true
| boolean "false" = false
| boolean s = error ("Bad boolean value: " ^ quote s);
-fun explicit "" = Default
- | explicit s = Explicit s
-
-
val _ = ThyOutput.add_options
[("gray", Library.setmp gray o boolean),
- ("linenos", Library.setmp linenos o boolean),
- ("index", Library.setmp index o explicit)]
-
+ ("linenos", Library.setmp linenos o boolean)]
end
\ No newline at end of file
Binary file progtutorial.pdf has changed