--- a/IsaMakefile Sat May 30 11:12:46 2009 +0200
+++ b/IsaMakefile Sat May 30 17:40:20 2009 +0200
@@ -26,7 +26,8 @@
ProgTutorial/*.ML \
ProgTutorial/Recipes/*.thy \
ProgTutorial/Package/*.thy \
- ProgTutorial/Package/*.ML
+ ProgTutorial/Package/*.ML
+ @rm -rf ProgTutorial/generated/*
$(USEDIR) HOL ProgTutorial
$(ISATOOL) version > ProgTutorial/generated/version
$(ML_HOME)/poly -v > ProgTutorial/generated/pversion
--- a/ProgTutorial/Base.thy Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Base.thy Sat May 30 17:40:20 2009 +0200
@@ -1,7 +1,7 @@
theory Base
imports Main
uses
- "outputfn.ML"
+ "output_tutorial.ML"
"chunks.ML"
"antiquote_setup.ML"
begin
--- a/ProgTutorial/FirstSteps.thy Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sat May 30 17:40:20 2009 +0200
@@ -111,7 +111,7 @@
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 [indexc] "writeln"}. For example
+ the function @{ML [index] "writeln"}. For example
@{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
@@ -122,13 +122,13 @@
@{ML_response_fake [display,gray] "writeln (PolyML.makestring 1)" "\"1\""}
- However, @{ML makestring} only works if the type of what is converted is monomorphic
+ However, @{ML [index] makestring} only works if the type of what is converted is monomorphic
and not a function.
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 tracing} is more appropriate. This function writes all output into
+ function @{ML [index] tracing} is more appropriate. This function writes all output into
a separate tracing buffer. For example:
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
@@ -155,13 +155,14 @@
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
will cause that all tracing information is printed into the file @{text "foo.bar"}.
- You can print out error messages with the function @{ML error}; for example:
+ You can print out error messages with the function @{ML [index] error}; for example:
@{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")"
"Exception- ERROR \"foo\" raised
At command \"ML\"."}
- (FIXME Mention how to work with @{ML Toplevel.debug} and @{ML Toplevel.profiling}.)
+ (FIXME Mention how to work with @{ML [index] debug in Toplevel} and
+ @{ML [index] profiling in Toplevel}.)
*}
(*
@@ -183,14 +184,14 @@
or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing
them (see Section \ref{sec:pretty}),
but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
- a term into a string is to use the function @{ML Syntax.string_of_term}.
+ a term into a string is to use the function @{ML [index] string_of_term in Syntax}.
@{ML_response_fake [display,gray]
"Syntax.string_of_term @{context} @{term \"1::nat\"}"
"\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
This produces a string with some additional information encoded in it. The string
- can be properly printed by using the function @{ML writeln}.
+ can be properly printed by using the function @{ML [index] writeln}.
@{ML_response_fake [display,gray]
"writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
@@ -203,9 +204,9 @@
Syntax.string_of_term ctxt (term_of t)*}
text {*
- In this example the function @{ML term_of} extracts the @{ML_type term} from
+ In this example the function @{ML [index] term_of} extracts the @{ML_type term} from
a @{ML_type cterm}. If there are more than one @{ML_type cterm}s to be
- printed, you can use the function @{ML commas} to separate them.
+ printed, you can use the function @{ML [index] commas} to separate them.
*}
ML{*fun string_of_cterms ctxt ts =
@@ -213,7 +214,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 crep_thm}.
+ into a @{ML_type cterm} using the function @{ML [index] crep_thm}.
*}
ML{*fun string_of_thm ctxt thm =
@@ -229,7 +230,7 @@
In order to improve the readability of theorems we convert
these schematic variables into free variables using the
- function @{ML Variable.import_thms}.
+ function @{ML [index] import_thms in Variable}.
*}
ML{*fun no_vars ctxt thm =
@@ -266,21 +267,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 I}, which is just the identity function defined as
+ The simplest combinator is @{ML [index] I}, which is just the identity function defined as
*}
ML{*fun I x = x*}
-text {* Another simple combinator is @{ML K}, defined as *}
+text {* Another simple combinator is @{ML [index] K}, defined as *}
ML{*fun K x = fn _ => x*}
text {*
- @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
+ @{ML [index] K} ``wraps'' a function around the argument @{text "x"}. However, this
function ignores its argument. As a result, @{ML K} defines a constant function
always returning @{text x}.
- The next combinator is reverse application, @{ML "|>"}, defined as:
+ The next combinator is reverse application, @{ML [index] "|>"}, defined as:
*}
ML{*fun x |> f = f x*}
@@ -352,16 +353,16 @@
"P z za zb"}
You can read off this behaviour from how @{ML apply_fresh_args} is
- coded: in Line 2, the function @{ML fastype_of} calculates the type of the
- function; @{ML binder_types} in the next line produces the list of argument
+ coded: in Line 2, the function @{ML [index] fastype_of} calculates the type of the
+ function; @{ML [index] binder_types} in the next line produces the list of argument
types (in the case above the list @{text "[nat, int, unit]"}); Line 4
pairs up each type with the string @{text "z"}; the
- function @{ML variant_frees in Variable} generates for each @{text "z"} a
+ function @{ML [index] variant_frees in Variable} generates for each @{text "z"} a
unique name avoiding the given @{text f}; the list of name-type pairs is turned
into a list of variable terms in Line 6, which in the last line is applied
- by the function @{ML list_comb} to the function. In this last step we have to
- use the function @{ML curry}, because @{ML list_comb} expects the function and the
- variables list as a pair. This kind of functions is often needed when
+ by the function @{ML [index] list_comb} to the function. In this last step we have to
+ use the function @{ML [index] curry}, because @{ML [index] list_comb} expects the
+ function and the variables list as a pair. This kind of functions is often needed when
constructing terms and the infrastructure helps tremendously to avoid
any name clashes. Consider for example:
@@ -371,7 +372,7 @@
|> writeln"
"za z zb"}
- The combinator @{ML "#>"} is the reverse function composition. It can be
+ The combinator @{ML [index] "#>"} is the reverse function composition. It can be
used to define the following function
*}
@@ -386,7 +387,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 tap} allows
+ ``waterfall method'' of writing functions. The combinator @{ML [index] tap} allows
you to get hold of an intermediate result (to do some side-calculations for
instance). The function
@@ -399,13 +400,13 @@
text {*
increments the argument first by @{text "1"} and then by @{text "2"}. In the
- middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
- intermediate result inside the tracing buffer. The function @{ML tap} can
+ middle (Line 3), however, it uses @{ML [index] tap} for printing the ``plus-one''
+ intermediate result inside the tracing buffer. The function @{ML [index] tap} can
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 "`"} (a backtick) is similar to @{ML tap}, but applies a
+ The combinator @{ML [index] "`"} (a backtick) is similar to @{ML tap}, but applies a
function to the value and returns the result together with the value (as a
pair). For example the function
*}
@@ -420,7 +421,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 "|>>"} and @{ML "||>"} are defined for
+ The combinators @{ML [index] "|>>"} and @{ML [index] "||>"} are defined for
functions manipulating pairs. The first applies the function to
the first component of the pair, defined as
*}
@@ -434,7 +435,7 @@
ML{*fun (x, y) ||> f = (x, f y)*}
text {*
- With the combinator @{ML "|->"} you can re-combine the elements from a pair.
+ With the combinator @{ML [index] "|->"} you can re-combine the elements from a pair.
This combinator is defined as
*}
@@ -450,10 +451,10 @@
|-> (fn x => fn y => x + y)*}
text {*
- The combinator @{ML ||>>} plays a central rôle whenever your task is to update a
+ The combinator @{ML [index] ||>>} plays a central rôle whenever your task is to update a
theory and the update also produces a side-result (for example a theorem). Functions
for such tasks return a pair whose second component is the theory and the fist
- component is the side-result. Using @{ML ||>>}, you can do conveniently the update
+ component is the side-result. Using @{ML [index] ||>>}, you can do conveniently the update
and also accumulate the side-results. Considder the following simple function.
*}
@@ -465,7 +466,7 @@
text {*
The purpose of Line 2 is to just pair up the argument with a dummy value (since
- @{ML "||>>"} operates on pairs). Each of the next three lines just increment
+ @{ML [index] "||>>"} operates on pairs). Each of the next three lines just increment
the value by one, but also nest the intrermediate results to the left. For example
@{ML_response [display,gray]
@@ -482,12 +483,14 @@
*}
text {*
- Recall that @{ML "|>"} is the reverse function application. Recall also that
+ Recall that @{ML [index] "|>"} is the reverse function application. Recall also that
the related
- reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
- @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"} described above have related combinators for
- function composition, namely @{ML "#->"}, @{ML "#>>"}, @{ML "##>"} and @{ML "##>>"}.
- Using @{ML "#->"}, for example, the function @{text double} can also be written as:
+ reverse function composition is @{ML [index] "#>"}. In fact all the combinators
+ @{ML [index] "|->"}, @{ML [index] "|>>"} , @{ML [index] "||>"} and @{ML [index]
+ "||>>"} described above have related combinators for
+ function composition, namely @{ML [index] "#->"}, @{ML [index] "#>>"},
+ @{ML [index] "##>"} and @{ML [index] "##>>"}.
+ Using @{ML [index] "#->"}, for example, the function @{text double} can also be written as:
*}
ML{*val double =
@@ -524,7 +527,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 "Context.theory_name"}.
+ the function @{ML [index] theory_name in Context}.
Note, however, that antiquotations are statically linked, that is their value is
determined at ``compile-time'', not ``run-time''. For example the function
@@ -566,7 +569,7 @@
end*}
text {*
- The function @{ML dest_ss in MetaSimplifier} returns a record containing all
+ The function @{ML [index] dest_ss in MetaSimplifier} returns a record containing all
information stored in the simpset, but we are only interested in the names of the
simp-rules. Now you can feed in the current simpset into this function.
The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
@@ -587,7 +590,7 @@
"@{binding \"name\"}"
"name"}
- An example where a binding is needed is the function @{ML define in
+ An example where a binding is needed is the function @{ML [index] define in
LocalTheory}. This function is below used to define the constant @{term
"TrueConj"} as the conjunction
@{term "True \<and> True"}.
@@ -639,7 +642,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 "term"} defined as follows:
+ representation corresponding to the datatype @{ML_type [index] "term"} defined as follows:
*}
ML_val %linenosgray{*datatype term =
@@ -829,7 +832,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 list_comb}, which takes a term
+ constructing terms. One is the function @{ML [index] list_comb}, which takes a term
and a list of terms as arguments, and produces as output the term
list applied to the term. For example
@@ -837,7 +840,7 @@
"list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
- Another handy function is @{ML lambda}, which abstracts a variable
+ Another handy function is @{ML [index] lambda}, which abstracts a variable
in a term. For example
@{ML_response_fake [display,gray]
@@ -860,7 +863,7 @@
of Church-style typing, where variables with the same name still differ, if they
have different type.
- There is also the function @{ML subst_free} with which terms can
+ There is also the function @{ML [index] subst_free} with which terms can
be replaced by other terms. For example below, we will replace in
@{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0 x"}
the subterm @{term "(f::nat\<Rightarrow>nat\<Rightarrow>nat) 0"} by @{term y}, and @{term x} by @{term True}.
@@ -880,7 +883,7 @@
"Free (\"x\", \"nat\")"}
There are many convenient functions that construct specific HOL-terms. For
- example @{ML "HOLogic.mk_eq"} constructs an equality out of two terms.
+ example @{ML [index] mk_eq in HOLogic} constructs an equality out of two terms.
The types needed in this equality are calculated from the type of the
arguments. For example
@@ -1006,8 +1009,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 Sign.extern_const} or
- @{ML Long_Name.base_name}. For example:
+ constant is. For this you can use the function @{ML [index] extern_const in Sign} or
+ @{ML base_name in Long_Name}. For example:
@{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
@@ -1033,19 +1036,19 @@
ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-text {* This can be equally written with the combinator @{ML "-->"} as: *}
+text {* This can be equally written with the combinator @{ML [index] "-->"} as: *}
ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
text {*
If you want to construct a function type with more than one argument
- type, then you can use @{ML "--->"}.
+ type, then you can use @{ML [index] "--->"}.
*}
ML{*fun make_fun_types tys ty = tys ---> ty *}
text {*
- A handy function for manipulating terms is @{ML map_types}: it takes a
+ A handy function for manipulating terms is @{ML [index] map_types}: it takes a
function and applies it to every type in a term. You can, for example,
change every @{typ nat} in a term into an @{typ int} using the function:
*}
@@ -1065,8 +1068,9 @@
$ 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 Term.add_tfrees} (similarly @{ML Term.add_tvars}
- for the schematic type-variables). One would expect that such functions
+ can use the function @{ML [index] add_tfrees in Term}
+ (similarly @{ML [index] add_tvars in Term} for the schematic type-variables).
+ One would expect that such functions
take a term as input and return a list of types. But their type is actually
@{text[display] "Term.term -> (string * Term.sort) list -> (string * Term.sort) list"}
@@ -1079,7 +1083,7 @@
"Term.add_tfrees @{term \"(a,b)\"} []"
"[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
- The reason for this definition is that @{ML Term.add_tfrees} can
+ The reason for this definition is that @{ML add_tfrees in Term} can
be easily folded over a list of terms. Similarly for all functions
named @{text "add_"}some\_name in @{ML_file "Pure/term.ML"}.
@@ -1093,8 +1097,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 cterm_of}, which
- converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
+ a theory. Type-checking is done via the function @{ML [index] cterm_of}, which
+ converts a @{ML_type [index] term} into a @{ML_type [index] cterm}, a \emph{certified}
term. Unlike @{ML_type term}s, which are just trees, @{ML_type "cterm"}s are
abstract objects that are guaranteed to be type-correct, and they can only
be constructed via ``official interfaces''.
@@ -1153,7 +1157,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 type_of} returns the
+ Given a well-typed term, the function @{ML [index] type_of} returns the
type of a term. Consider for example:
@{ML_response [display,gray]
@@ -1168,7 +1172,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 fastype_of}, which
+ not necessary, there is the function @{ML [index] fastype_of}, which
also returns the type of a term.
@{ML_response [display,gray]
@@ -1185,7 +1189,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 "dummyT"} and then let type-inference figure out the
+ type @{ML [index] dummyT} and then let type-inference figure out the
complete type. An example is as follows:
@{ML_response_fake [display,gray]
@@ -1275,7 +1279,7 @@
@{ML_file "Pure/thm.ML"}.
\end{readmore}
- (FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on)
+ (FIXME: handy functions working on theorems, like @{ML [index] rulify in ObjectLogic} and so on)
(FIXME: how to add case-names to goal states - maybe in the
next section)
@@ -1292,7 +1296,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 Sign.add_consts_i}.
+ constant on the ML-level is @{ML [index] add_consts_i in Sign}.
If you write\footnote{Recall that ML-code needs to be
enclosed in \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.}
*}
@@ -1370,13 +1374,12 @@
ML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
text {*
- where the function @{ML "Thm.rule_attribute"} expects a function taking a
+ where the function @{ML [index] rule_attribute in Thm} expects a function taking a
context (which we ignore in the code above) and a theorem (@{text thm}), and
returns another theorem (namely @{text thm} resolved with the theorem
- @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
- in Section~\ref{sec:simpletacs}.} The function
- @{ML "Thm.rule_attribute"} then returns
- an attribute.
+ @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML [index] 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
using the Isabelle command \isacommand{attribute\_setup} as follows:
@@ -1411,7 +1414,7 @@
@{text "> "}~@{thm test[my_sym]}
\end{isabelle}
- An alternative for setting up an attribute is the function @{ML Attrib.setup}.
+ An alternative for setting up an attribute is the function @{ML [index] setup in Attrib}.
So instead of using \isacommand{attribute\_setup}, you can also set up the
attribute as follows:
*}
@@ -1434,7 +1437,7 @@
text {*
where @{ML swap} swaps the components of a pair. The setup of this theorem
- attribute uses the parser @{ML Attrib.thms}, which parses a list of
+ attribute uses the parser @{ML thms in Attrib}, which parses a list of
theorems.
*}
@@ -1476,10 +1479,10 @@
you get an exception indicating that the theorem @{thm [source] sym}
does not resolve with meta-equations.
- The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
+ The purpose of @{ML [index] rule_attribute in Thm} is to directly manipulate theorems.
Another usage of theorem attributes is to add and delete theorems from stored data.
For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
- current simpset. For these applications, you can use @{ML Thm.declaration_attribute}.
+ current simpset. For these applications, you can use @{ML [index] declaration_attribute in Thm}.
To illustrate this function, let us introduce a reference containing a list
of theorems.
*}
@@ -1506,12 +1509,11 @@
text {*
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 Thm.add_thm}
- adds a theorem if it is not already included in the list, and @{ML
- Thm.del_thm} deletes one (both functions use the predicate @{ML
- Thm.eq_thm_prop}, which compares theorems according to their proved
- propositions modulo alpha-equivalence).
-
+ however the reference @{ML my_thms}, whereby the function
+ @{ML [index] add_thm in Thm} adds a theorem if it is not already included in
+ the list, and @{ML [index] del_thm in Thm} deletes one (both functions use the
+ predicate @{ML [index] eq_thm_prop in Thm}, which compares theorems according to
+ their proved propositions modulo alpha-equivalence).
You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into
attributes with the code
@@ -1528,7 +1530,7 @@
"maintaining a list of my_thms - rough test only!"
text {*
- The parser @{ML Attrib.add_del} is a pre-defined parser for
+ The parser @{ML [index] add_del in Attrib} is a pre-defined parser for
adding and deleting lemmas. Now if you prove the next lemma
and attach to it the attribute @{text "[my_thms]"}
*}
@@ -1556,7 +1558,7 @@
"[\"True\", \"Suc (Suc 0) = 2\"]"}
The theorem @{thm [source] trueI_2} only appears once, since the
- function @{ML Thm.add_thm} tests for duplicates, before extending
+ function @{ML [index] add_thm in Thm} tests for duplicates, before extending
the list. Deletion from the list works as follows:
*}
@@ -1568,7 +1570,7 @@
"!my_thms"
"[\"True\"]"}
- We used in this example two functions declared as @{ML Thm.declaration_attribute},
+ We used in this example two functions declared as @{ML [index] declaration_attribute in Thm},
but there can be any number of them. We just have to change the parser for reading
the arguments accordingly.
@@ -1632,7 +1634,7 @@
is important to
store data in a ``data slot'' and \emph{not} in a reference. Backtrack
to the point just before the lemma @{thm [source] three} was proved and
- check the the content of @{ML_struct "MyThmsData"}: it should be empty.
+ check the the content of @{ML_struct MyThmsData}: it should be empty.
The addition has been properly retracted. Now consider the proof:
*}
@@ -1799,7 +1801,7 @@
section {* Storing Theorems\label{sec:storing} (TBD) *}
-text {* @{ML PureThy.add_thms_dynamic} *}
+text {* @{ML [index] add_thms_dynamic in PureThy} *}
local_setup {*
LocalTheory.note Thm.theoremK
@@ -1845,9 +1847,9 @@
its functions do not operate on @{ML_type string}s, but on instances of the
type:
- @{ML_type [display, gray] "Pretty.T"}
-
- The function @{ML "Pretty.str"} transforms a (plain) string into such a pretty
+ @{ML_type [display, gray, index] "Pretty.T"}
+
+ The function @{ML str in Pretty} transforms a (plain) string into such a pretty
type. For example
@{ML_response_fake [display,gray]
@@ -1858,7 +1860,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 Pretty.string_of}. In what
+ string}. This can be done with the function @{ML [index] string_of in Pretty}. In what
follows we will use the following wrapper function for printing a pretty
type:
*}
@@ -1903,10 +1905,10 @@
However by using pretty types you have the ability to indicate a possible
linebreak for example at each space. You can achieve this with the function
- @{ML Pretty.breaks}, which expects a list of pretty types and inserts a
+ @{ML [index] breaks in Pretty}, which expects a list of pretty types and inserts a
possible linebreak 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 Pretty.blk} as follows:
+ with the function @{ML [index] blk in Pretty} as follows:
@{ML_response_fake [display,gray]
@@ -1921,7 +1923,7 @@
fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
Here the layout of @{ML test_str} is much more pleasing to the
- eye. The @{ML "0"} in @{ML Pretty.blk} stands for no indentation
+ eye. The @{ML "0"} in @{ML [index] blk in Pretty} stands for no indentation
of the printed string. You can increase the indentation and obtain
@{ML_response_fake [display,gray]
@@ -1937,7 +1939,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 Pretty.indent} as follows:
+ function @{ML [index] indent in Pretty} as follows:
@{ML_response_fake [display,gray]
"let
@@ -1952,7 +1954,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 Pretty.commas}. For example
+ @{ML [index] commas in Pretty}. For example
@{ML_response_fake [display,gray]
"let
@@ -1967,7 +1969,7 @@
where @{ML upto} generates a list of integers. You can print this
list out as an ``set'', that means enclosed inside @{text [quotes] "{"} and
@{text [quotes] "}"}, and separated by commas using the function
- @{ML Pretty.enum}. For example
+ @{ML [index] enum in Pretty}. For example
*}
text {*
@@ -2038,8 +2040,8 @@
text {*
In Line 3 we define a function that inserts according to spaces
possible linebreaks into an (English). In Lines 4 and 5 we pretty-print
- the term and its type using the functions @{ML Syntax.pretty_term} and
- @{ML Syntax.pretty_typ}. We also use the function @{ML Pretty.quote}
+ the term and its type using the functions @{ML [index] pretty_term in Syntax} and
+ @{ML [index] pretty_typ in Syntax}. We also use the function @{ML [index] quote in 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
linebreak, because we do not want that a linebreak occurs there.
--- a/ProgTutorial/Package/Ind_Code.thy Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy Sat May 30 17:40: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 LocalTheory.define}. The wrapper takes a predicate name, a syntax
+ @{ML [index] define in LocalTheory}. The wrapper takes a predicate name, a syntax
annotation and a term representing the right-hand side of the definition.
*}
@@ -35,12 +35,12 @@
text {*
It returns the definition (as a theorem) and the local theory in which the
- definition has been made. In Line 4, @{ML internalK in Thm} is a flag
- attached to the theorem (others possibile flags are @{ML definitionK in Thm}
- and @{ML axiomK in Thm}). These flags just classify theorems and have no
+ definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
+ attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}
+ and @{ML [index] axiomK in Thm}). These flags just classify theorems and have no
significant meaning, except for tools that, for example, find theorems in
the theorem database.\footnote{FIXME: put in the section about theorems.} We
- also use @{ML empty_binding in Attrib} in Line 3, since the definitions for
+ also use @{ML [index] empty_binding in Attrib} in Line 3, since the definitions for
our inductive predicates are not meant to be seen by the user and therefore
do not need to have any theorem attributes. A testcase for this function is
*}
@@ -170,7 +170,7 @@
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 (Line 3); with this theory we can use the function
- @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
+ @{ML [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
to @{ML defn_aux} in Line 5 produces all right-hand sides of the
definitions. The actual definitions are then made in Line 7. The result of
the function is a list of theorems and a local theory (the theorems are
@@ -437,7 +437,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 subst_free}. Line 14 and 15 just iterate
+ (Line 11) using the function @{ML [index] subst_free}. Line 14 and 15 just iterate
the proofs for all predicates.
From this we obtain a list of theorems. Finally we need to export the
fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"}
@@ -579,7 +579,7 @@
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 SUBPROOF}, since this tactic provides us with the parameters (as
+ tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as
list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s).
The problem we have to overcome with @{ML SUBPROOF}
is, however, that this tactic always expects us to completely discharge the
@@ -627,7 +627,7 @@
going in our example, we will print out these values using the printing
function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
supply us the @{text "params"} and @{text "prems"} as lists, we can
- separate them using the function @{ML chop}.
+ separate them using the function @{ML [index] chop}.
*}
ML{*fun chop_test_tac preds rules =
@@ -691,7 +691,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 "ObjectLogic.rulify"}. So we can modify the
+ format (using @{ML [index] rulify in ObjectLogic}. So we can modify the
subproof as follows:
*}
@@ -854,7 +854,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 MRS} does nothing. Similarly, in the
+ just the empty list and the function @{ML [index] MRS} does nothing. Similarly, in the
cases where the recursive premises of the rule do not have preconditions.
In case there are preconditions, then Line 4 discharges them. After
that we can proceed as before, i.e., check whether the outermost
@@ -932,7 +932,7 @@
end*}
text {*
- The iteration is done with the function @{ML map_index} since we
+ The iteration is done with the function @{ML [index] map_index} since we
need the introduction rule together with its number (counted from
@{text 0}). This completes the code for the functions deriving the
reasoning infrastructure. It remains to implement some administrative
@@ -945,7 +945,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 LocalTheory.note} does.
+ @{ML [index] note in LocalTheory} does.
For convenience, we use the following
@@ -1027,7 +1027,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 "case_names" in RuleCases}
+ to use some specific attributes. The first @{ML [index] case_names in RuleCases}
corresponds to the case names that are used by Isar to reference the proof
obligations in the induction. The second @{ML "consumes 1" in RuleCases}
indicates that the first premise of the induction principle (namely
--- a/ProgTutorial/Package/Ind_Interface.thy Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy Sat May 30 17:40:20 2009 +0200
@@ -165,8 +165,8 @@
OuterKeyword.thy_decl specification*}
text {*
- We call @{ML local_theory in OuterSyntax} with the kind-indicator
- @{ML thy_decl in OuterKeyword} since the package does not need to open
+ We call @{ML [index] local_theory in OuterSyntax} with the kind-indicator
+ @{ML [index] thy_decl in OuterKeyword} since the package does not need to open
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
@@ -178,7 +178,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 read_spec in Specification}. This function takes some strings
+ function @{ML [index] read_spec in Specification}. This function takes some strings
(with possible typing annotations) and some rule specifications, and attempts
to find a typing according to the given type constraints given by the
user and the type constraints by the ``ambient'' theory. It returns
--- a/ProgTutorial/Parsing.thy Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Parsing.thy Sat May 30 17:40:20 2009 +0200
@@ -36,7 +36,7 @@
text {*
Let us first have a look at parsing strings using generic parsing
- combinators. The function @{ML "$$"} takes a string as argument and will
+ combinators. The function @{ML [index] "$$"} takes a string as argument and will
``consume'' this string from a given input list of strings. ``Consume'' in
this context means that it will return a pair consisting of this string and
the rest of the input list. For example:
@@ -70,6 +70,8 @@
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,
@@ -85,8 +87,9 @@
"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
[\"\\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
- Slightly more general than the parser @{ML "$$"} is the function @{ML
- Scan.one}, in that it takes a predicate as argument and then parses exactly
+ Slightly more general than the parser @{ML "$$"} is the function
+ @{ML [index] one in Scan}, in that it takes a predicate as argument and
+ then parses exactly
one item from the input list satisfying this predicate. For example the
following parser either consumes an @{text [quotes] "h"} or a @{text
[quotes] "w"}:
@@ -101,7 +104,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- Two parsers can be connected in sequence by using the function @{ML "--"}.
+ Two parsers can be connected in sequence by using the function @{ML [index] "--"}.
For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this
order) you can achieve by:
@@ -112,14 +115,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 Scan.this_string}:
+ then you should use the function @{ML [index] this_string in Scan}:
@{ML_response [display,gray]
"Scan.this_string \"hell\" (Symbol.explode \"hello\")"
"(\"hell\", [\"o\"])"}
- Parsers that explore alternatives can be constructed using the function @{ML
- "||"}. The parser @{ML "(p || q)" for p q} returns the
+ Parsers that explore alternatives can be constructed using the function
+ @{ML [index] "||"}. The parser @{ML "(p || q)" for p q} returns the
result of @{text "p"}, in case it succeeds, otherwise it returns the
result of @{text "q"}. For example:
@@ -134,7 +137,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
- The functions @{ML "|--"} and @{ML "--|"} work like the sequencing function
+ The functions @{ML [index] "|--"} and @{ML [index] "--|"} work like the sequencing function
for parsers, except that they discard the item being parsed by the first (respectively second)
parser. For example:
@@ -148,6 +151,7 @@
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:
@@ -162,7 +166,7 @@
end"
"((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML Scan.option} works similarly, except no default value can
+ The function @{ML [index] option in Scan} works similarly, except no default value can
be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
@{ML_response [display,gray]
@@ -174,7 +178,7 @@
(p input1, p input2)
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
- The function @{ML "!!"} helps to produce appropriate error messages
+ The function @{ML [index] "!!"} helps to produce appropriate error messages
for parsing. For example if you want to parse @{text p} immediately
followed by @{text q}, or start a completely different parser @{text r},
you might write:
@@ -210,13 +214,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 "Scan.error"}. For example:
+ @{ML [index] error in Scan}. For example:
@{ML_response_fake [display,gray]
"Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
"Exception Error \"foo\" raised"}
- This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.local_theory"}
+ This ``prefixing'' is usually done by wrappers such as @{ML [index] local_theory in OuterSyntax}
(see Section~\ref{sec:newcommand} which explains this function in more detail).
Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
@@ -253,14 +257,14 @@
@{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")"
"([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
- Note that @{ML "Scan.repeat"} stores the parsed items in a list. The function
- @{ML "Scan.repeat1"} is similar, but requires that the parser @{text "p"}
+ Note that @{ML [index] repeat in Scan} stores the parsed items in a list. The function
+ @{ML [index] repeat1 in Scan} is similar, but requires that the parser @{text "p"}
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 Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With
- them you can write:
+ the wrapper @{ML [index] finite in Scan} and the ``stopper-token''
+ @{ML [index] stopper in Symbol}. With them you can write:
@{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")"
"([\"h\", \"h\", \"h\", \"h\"], [])"}
@@ -269,7 +273,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 Scan.repeat} can be used with @{ML Scan.one} to read any
+ The function @{ML [index] repeat in Scan} can be used with @{ML [index] one in Scan} to read any
string as in
@{ML_response [display,gray]
@@ -281,9 +285,10 @@
end"
"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
- where the function @{ML Symbol.not_eof} ensures that we do not read beyond the
+ where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
+ \indexdef{unless@ {\tt\slshape{unless}}}{in {\tt\slshape Scan}}
The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore
@@ -297,9 +302,9 @@
succeeds.
- The functions @{ML Scan.repeat} and @{ML Scan.unless} 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] "*"}.
+ The functions @{ML [index] repeat in Scan} and @{ML [index] unless in Scan} can
+ be combined to read any input until a certain marker symbol is reached. In the
+ example below the marker symbol is a @{text [quotes] "*"}.
@{ML_response [display,gray]
"let
@@ -313,8 +318,10 @@
"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
+
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 "(p >> f)" for p f}, which runs
+ items. One way to do this is the function @{ML [index]">>"} where
+ @{ML "(p >> f)" for p f} runs
first the parser @{text p} and upon successful completion applies the
function @{text f} to the result. For example
@@ -342,14 +349,14 @@
(FIXME: move to an earlier place)
- The function @{ML Scan.ahead} parses some input, but leaves the original
+ The function @{ML [index] ahead in Scan} parses some input, but leaves the original
input unchanged. For example:
@{ML_response [display,gray]
"Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")"
"(\"foo\", [\"f\", \"o\", \"o\"])"}
- The function @{ML Scan.lift} takes a parser and a pair as arguments. This function applies
+ The function @{ML [index] lift in Scan} takes a parser and a pair as arguments. This function applies
the given parser to the second component of the pair and leaves the first component
untouched. For example
@@ -389,12 +396,13 @@
The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
\end{readmore}
- The structure @{ML_struct OuterLex} defines several kinds of tokens (for
- example @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in
- OuterLex} for keywords and @{ML "Command" in OuterLex} for commands). Some
+ The structure @{ML_struct [index] OuterLex} defines several kinds of tokens (for
+ example @{ML [index] Ident in OuterLex} for identifiers, @{ML Keyword in
+ OuterLex} for keywords and @{ML [index] Command in OuterLex} for commands). Some
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
- "OuterSyntax.scan"}. It is given the argument @{ML "Position.none"} since,
+ how to generate a token list out of a string using the function
+ @{ML [index] scan in OuterSyntax}. It is given the argument
+ @{ML "Position.none"} since,
at the moment, we are not interested in generating precise error
messages. The following code\footnote{Note that because of a possible bug in
the PolyML runtime system, the result is printed as @{text [quotes] "?"},
@@ -411,7 +419,7 @@
other syntactic category. The second indicates a space.
We can easily change what is recognised as a keyword with
- @{ML OuterKeyword.keyword}. For example calling this function
+ @{ML [index] keyword in OuterKeyword}. For example calling this function
*}
ML{*val _ = OuterKeyword.keyword "hello"*}
@@ -426,7 +434,8 @@
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 OuterLex.is_proper} to do this. For example:
+ functions @{ML filter} and @{ML [index] is_proper in OuterLex} to do this.
+ For example:
@{ML_response_fake [display,gray]
"let
@@ -463,10 +472,10 @@
end"
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
- You might have to adjust the @{ML print_depth} in order to
+ You might have to adjust the @{ML [index] print_depth} in order to
see the complete list.
- The parser @{ML "OuterParse.$$$"} parses a single keyword. For example:
+ The parser @{ML [index] "$$$" in OuterParse} parses a single keyword. For example:
@{ML_response [display,gray]
"let
@@ -477,7 +486,7 @@
end"
"((\"where\",\<dots>), (\"|\",\<dots>))"}
- Any non-keyword string can be parsed with the function @{ML OuterParse.reserved}.
+ Any non-keyword string can be parsed with the function @{ML [index] reserved in OuterParse}.
For example:
@{ML_response [display,gray]
@@ -489,7 +498,7 @@
end"
"(\"bar\",[])"}
- Like before, you can sequentially connect parsers with @{ML "--"}. For example:
+ Like before, you can sequentially connect parsers with @{ML [index] "--"}. For example:
@{ML_response [display,gray]
"let
@@ -499,6 +508,7 @@
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:
@@ -511,7 +521,7 @@
end"
"([\"in\", \"in\", \"in\"], [\<dots>])"}
- @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
+ @{ML [index] enum1 in OuterParse} works similarly, except that the parsed list must
be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the
end of the parsed string, otherwise the parser would have consumed all
tokens and then failed with the exception @{text "MORE"}. Like in the
@@ -535,7 +545,7 @@
text {*
- The function @{ML "OuterParse.!!!"} can be used to force termination of the
+ The function @{ML [index] "!!!" in OuterParse} can be used to force termination of the
parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section).
Except that the error message of @{ML "OuterParse.!!!"} is fixed to be
@{text [quotes] "Outer syntax error"}
@@ -554,8 +564,8 @@
\begin{exercise} (FIXME)
A type-identifier, for example @{typ "'a"}, is a token of
- kind @{ML "Keyword" in OuterLex}. It can be parsed using
- the function @{ML OuterParse.type_ident}.
+ kind @{ML [index] Keyword in OuterLex}. It can be parsed using
+ the function @{ML type_ident in OuterParse}.
\end{exercise}
(FIXME: or give parser for numbers)
@@ -713,7 +723,7 @@
variables with optional type-annotation and syntax-annotation, and a list of
rules where every rule has optionally a name and an attribute.
- The function @{ML OuterParse.fixes} in Line 2 of the parser reads an
+ The function @{ML [index] "fixes" in OuterParse} in Line 2 of the parser reads an
\isacommand{and}-separated
list of variables that can include optional type annotations and syntax translations.
For example:\footnote{Note that in the code we need to write
@@ -737,8 +747,8 @@
not yet used to type the variables: this must be done by type-inference later
on. Since types are part of the inner syntax they are strings with some
encoded information (see previous section). If a mixfix-syntax is
- present for a variable, then it is stored in the @{ML Mixfix} data structure;
- no syntax translation is indicated by @{ML NoSyn}.
+ present for a variable, then it is stored in the @{ML [index] Mixfix} data structure;
+ no syntax translation is indicated by @{ML [index] NoSyn}.
\begin{readmore}
The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
@@ -747,7 +757,7 @@
Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
list of introduction rules, that is propositions with theorem annotations
such as rule names and attributes. The introduction rules are propositions
- parsed by @{ML OuterParse.prop}. However, they can include an optional
+ parsed by @{ML [index] prop in OuterParse}. However, they can include an optional
theorem name plus some attributes. For example
@{ML_response [display,gray] "let
@@ -757,8 +767,8 @@
(name, map Args.dest_src attrib)
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
- The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of
- @{ML thm_name in SpecParse}. Theorem names can contain attributes. The name
+ The function @{ML [index] opt_thm_name in SpecParse} is the ``optional'' variant of
+ @{ML [index] thm_name in SpecParse}. Theorem names can contain attributes. The name
has to end with @{text [quotes] ":"}---see the argument of
the function @{ML SpecParse.opt_thm_name} in Line 7.
@@ -773,7 +783,7 @@
Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
to the ``where-part'' of the introduction rules given above. Below
- we paraphrase the code of @{ML SpecParse.where_alt_specs} adapted to our
+ we paraphrase the code of @{ML [index] where_alt_specs in SpecParse} adapted to our
purposes.
\begin{isabelle}
*}
@@ -822,7 +832,7 @@
end *}
text {*
- The crucial function @{ML OuterSyntax.local_theory} expects a name for the command, a
+ The crucial function @{ML [index] local_theory in OuterSyntax} expects a name for the command, a
short description, a kind indicator (which we will explain later more thoroughly) and a
parser producing a local theory transition (its purpose will also explained
later).
@@ -962,7 +972,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 Scan.succeed} does not parse any argument, but immediately
+ because of @{ML [index] succeed in Scan} does not parse any argument, but immediately
returns the simple function @{ML "LocalTheory.theory I"}. We can
replace this code by a function that first parses a proposition (using the
parser @{ML OuterParse.prop}), then prints out the tracing
@@ -992,7 +1002,7 @@
and see the proposition in the tracing buffer.
- Note that so far we used @{ML thy_decl in OuterKeyword} as the kind
+ Note that so far we used @{ML [index] thy_decl in OuterKeyword} as the kind
indicator for the command. This means that the command finishes as soon as
the arguments are processed. Examples of this kind of commands are
\isacommand{definition} and \isacommand{declare}. In other cases, commands
@@ -1000,7 +1010,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 thy_goal in OuterKeyword} and the function @{ML
+ the kind indicator @{ML [index] thy_goal in OuterKeyword} and the function @{ML
"local_theory_to_proof" in OuterSyntax} to set up the command. Note,
however, once you change the ``kind'' of a command from @{ML thy_decl in
OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
@@ -1029,8 +1039,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 Syntax.read_prop}, which converts a string into a proper proposition.
- In Line 6 the function @{ML Proof.theorem_i} starts the proof for the
+ @{ML [index] read_prop in Syntax}, which converts a string into a proper proposition.
+ In Line 6 the function @{ML [index] theorem_i in Proof} starts the proof for the
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
@@ -1054,7 +1064,7 @@
\isacommand{done}
\end{isabelle}
- (FIXME: read a name and show how to store theorems; see @{ML LocalTheory.note})
+ (FIXME: read a name and show how to store theorems; see @{ML [index] note in LocalTheory})
*}
@@ -1086,7 +1096,8 @@
text {*
It defines the method @{text foobar}, 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 SIMPLE_METHOD}
+ applies @{thm [source] conjE} and then @{thm [source] conjI}. The function
+ @{ML [index] SIMPLE_METHOD}
turns such a tactic into a method. The method @{text "foobar"} can be used as follows
*}
--- a/ProgTutorial/Tactical.thy Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Tactical.thy Sat May 30 17:40:20 2009 +0200
@@ -56,12 +56,12 @@
@{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 etac}, @{ML rtac} and @{ML atac} in the code above correspond
+ The tactics @{ML [index] etac}, @{ML [index] rtac} and @{ML [index] atac} in the code above correspond
roughly to @{text erule}, @{text rule} and @{text assumption}, respectively.
- The operator @{ML THEN} strings the tactics together.
+ The operator @{ML [index] THEN} strings the tactics together.
\begin{readmore}
- To learn more about the function @{ML Goal.prove} see \isccite{sec:results}
+ To learn more about the function @{ML [index] prove in Goal} see \isccite{sec:results}
and the file @{ML_file "Pure/goal.ML"}. See @{ML_file
"Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic
tactics and tactic combinators; see also Chapters 3 and 4 in the old
@@ -119,7 +119,7 @@
THEN' atac)*}text_raw{*\label{tac:footacprime}*}
text {*
- where @{ML THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
+ where @{ML [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give
the number for the subgoal explicitly when the tactic is
called. So in the next proof you can first discharge the second subgoal, and
subsequently the first.
@@ -160,7 +160,7 @@
willy-nilly; only in very grave failure situations should a tactic raise the
exception @{text THM}.
- The simplest tactics are @{ML no_tac} and @{ML all_tac}. The first returns
+ The simplest tactics are @{ML [index] no_tac} and @{ML [index] all_tac}. The first returns
the empty sequence and is defined as
*}
@@ -333,7 +333,7 @@
section {* Simple Tactics\label{sec:simpletacs} *}
text {*
- Let us start with explaining the simple tactic @{ML print_tac}, which is quite useful
+ Let us start with explaining the simple tactic @{ML [index] print_tac}, which is quite useful
for low-level debugging of tactics. It just prints out a message and the current
goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state
as the user would see it. For example, processing the proof
@@ -353,7 +353,7 @@
text {*
A simple tactic for easy discharge of any proof obligations is
- @{ML SkipProof.cheat_tac}. This tactic corresponds to
+ @{ML [index] cheat_tac in SkipProof}. This tactic corresponds to
the Isabelle command \isacommand{sorry} and is sometimes useful
during the development of tactics.
*}
@@ -369,7 +369,7 @@
This tactic works however only if the quick-and-dirty mode of Isabelle
is switched on.
- Another simple tactic is the function @{ML atac}, which, as shown in the previous
+ Another simple tactic is the function @{ML [index] atac}, which, as shown in the previous
section, corresponds to the assumption command.
*}
@@ -381,7 +381,8 @@
(*<*)oops(*>*)
text {*
- Similarly, @{ML rtac}, @{ML dtac}, @{ML etac} and @{ML ftac} correspond (roughly)
+ Similarly, @{ML [index] rtac}, @{ML [index] dtac}, @{ML [index] etac} and
+ @{ML [index] ftac} correspond (roughly)
to @{text rule}, @{text drule}, @{text erule} and @{text frule},
respectively. Each of them take a theorem as argument and attempt to
apply it to a goal. Below are three self-explanatory examples.
@@ -409,7 +410,7 @@
(*<*)oops(*>*)
text {*
- The function @{ML resolve_tac} is similar to @{ML rtac}, except that it
+ The function @{ML [index] resolve_tac} is similar to @{ML [index] rtac}, except that it
expects a list of theorems as arguments. From this list it will apply the
first applicable theorem (later theorems that are also applicable can be
explored via the lazy sequences mechanism). Given the code
@@ -432,10 +433,11 @@
text {*
Similar versions taking a list of theorems exist for the tactics
- @{ML dtac} (@{ML dresolve_tac}), @{ML etac} (@{ML eresolve_tac}) and so on.
+ @{ML dtac} (@{ML [index] dresolve_tac}), @{ML etac}
+ (@{ML [index] eresolve_tac}) and so on.
- Another simple tactic is @{ML cut_facts_tac}. It inserts a list of theorems
+ Another simple tactic is @{ML [index] cut_facts_tac}. It inserts a list of theorems
into the assumptions of the current goal state. For example
*}
@@ -470,7 +472,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 RS}
+ @{ML [index] RS}
@{ML_response_fake [display,gray]
"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
@@ -484,7 +486,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 RSN} is similar to @{ML RS}, but
+ then the function raises an exception. The function @{ML [index] RSN} is similar to @{ML RS}, but
takes an additional number as argument that makes explicit which premise
should be instantiated.
@@ -497,14 +499,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 MRS}:
+ the function @{ML [index] MRS}:
@{ML_response_fake [display,gray]
"no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})"
"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
If you need to instantiate lists of theorems, you can use the
- functions @{ML RL} and @{ML MRL}. For example in the code below,
+ functions @{ML RL} and @{ML [index] MRL}. For example in the code below,
every theorem in the second list is instantiated with every
theorem in the first.
@@ -523,7 +525,7 @@
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 @{ML SUBPROOF}. This tactic fixes the parameters
+ safety is provided by @{ML [index] SUBPROOF}. This tactic fixes the parameters
and binds the various components of a goal state to a record.
To see what happens, assume the function defined in Figure~\ref{fig:sptac}, which
takes a record and just prints out the content of this record (using the
@@ -586,7 +588,7 @@
@{text asms}, but also as @{ML_type thm} to @{text prems}.
Notice also that we had to append @{text [quotes] "?"} to the
- \isacommand{apply}-command. The reason is that @{ML SUBPROOF} normally
+ \isacommand{apply}-command. The reason is that @{ML [index] SUBPROOF} normally
expects that the subgoal is solved completely. Since in the function @{ML
sp_tac} we returned the tactic @{ML no_tac}, the subproof obviously
fails. The question-mark allows us to recover from this failure in a
@@ -663,8 +665,8 @@
also described in \isccite{sec:results}.
\end{readmore}
- Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL}
- and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former
+ Similar but less powerful functions than @{ML SUBPROOF} are @{ML [index] SUBGOAL}
+ and @{ML [index] CSUBGOAL}. They allow you to inspect a given subgoal (the former
presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
cterm}). With this you can implement a tactic that applies a rule according
to the topmost logic connective in the subgoal (to illustrate this we only
@@ -775,7 +777,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 EVERY'}. For example
+ sequence, you can use the combinator @{ML [index] EVERY'}. For example
the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also
be written as:
*}
@@ -797,11 +799,11 @@
text {*
and call @{ML foo_tac1}.
- With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML EVERY1} it must be
+ With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML [index] EVERY1} it must be
guaranteed that all component tactics successfully apply; otherwise the
whole tactic will fail. If you rather want to try out a number of tactics,
- then you can use the combinator @{ML ORELSE'} for two tactics, and @{ML
- FIRST'} (or @{ML FIRST1}) for a list of tactics. For example, the tactic
+ then you can use the combinator @{ML [index] ORELSE'} for two tactics, and @{ML
+ [index] FIRST'} (or @{ML [index] FIRST1}) for a list of tactics. For example, the tactic
*}
@@ -853,7 +855,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 ALLGOALS} that simplifies this. Using this combinator you can simply
+ @{ML [index] ALLGOALS} that simplifies this. Using this combinator you can simply
write: *}
lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -866,7 +868,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 TRY}.
+ list. The same can be achieved with the tactic combinator @{ML [index] TRY}.
For example:
*}
@@ -899,7 +901,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 CHANGED} to make sure the subgoal has been changed
+ use the combinator @{ML [index] CHANGED} to make sure the subgoal has been changed
by the tactic. Because now
*}
@@ -917,7 +919,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 REPEAT}. As an example
+ completely. For this you can use the tactic combinator @{ML [index] REPEAT}. As an example
suppose the following tactic
*}
@@ -938,7 +940,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 REPEAT1} is similar, but runs the tactic at least once (failing if
+ @{ML [index] REPEAT1} is similar, but runs the tactic at least once (failing if
this is not possible).
If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you
@@ -954,7 +956,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 REPEAT_ALL_NEW}.
+ resulting subgoals, you can use the tactic combinator @{ML [index] REPEAT_ALL_NEW}.
Suppose the tactic
*}
@@ -1007,7 +1009,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 DETERM}.
+ combinator @{ML [index] DETERM}.
*}
lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
@@ -1044,7 +1046,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 TRY}. The tactic combinator @{ML TRYALL} will try out
+ no primed version of @{ML [index] TRY}. The tactic combinator @{ML [index] TRYALL} will try out
a tactic on all subgoals. For example the tactic
*}
@@ -1053,7 +1055,7 @@
text {*
will solve all trivial subgoals involving @{term True} or @{term "False"}.
- (FIXME: say something about @{ML COND} and COND')
+ (FIXME: say something about @{ML [index] COND} and COND')
\begin{readmore}
Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}.
@@ -1079,11 +1081,11 @@
\begin{isabelle}
\begin{center}
\begin{tabular}{l@ {\hspace{2cm}}l}
- @{ML simp_tac} & @{text "(simp (no_asm))"} \\
- @{ML asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
- @{ML full_simp_tac} & @{text "(simp (no_asm_use))"} \\
- @{ML asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
- @{ML asm_full_simp_tac} & @{text "(simp)"}
+ @{ML [index] simp_tac} & @{text "(simp (no_asm))"} \\
+ @{ML [index] asm_simp_tac} & @{text "(simp (no_asm_simp))"} \\
+ @{ML [index] full_simp_tac} & @{text "(simp (no_asm_use))"} \\
+ @{ML [index] asm_lr_simp_tac} & @{text "(simp (asm_lr))"} \\
+ @{ML [index] asm_full_simp_tac} & @{text "(simp)"}
\end{tabular}
\end{center}
\end{isabelle}
@@ -1164,9 +1166,9 @@
\begin{isabelle}
\begin{tabular}{ll}
- @{ML addsimps} & @{ML delsimps}\\
- @{ML addcongs} & @{ML delcongs}\\
- @{ML addsimprocs} & @{ML delsimprocs}\\
+ @{ML [index] addsimps} & @{ML [index] delsimps}\\
+ @{ML [index] addcongs} & @{ML [index] delcongs}\\
+ @{ML [index] addsimprocs} & @{ML [index] delsimprocs}\\
\end{tabular}
\end{isabelle}
@@ -1196,7 +1198,7 @@
text_raw {*
\end{isabelle}
\end{minipage}
-\caption{The function @{ML Simplifier.dest_ss} returns a record containing
+\caption{The function @{ML [index] dest_ss in Simplifier} returns a record containing
all printable information stored in a simpset. We are here only interested in the
simplification rules, congruence rules and simprocs.\label{fig:printss}}
\end{figure} *}
@@ -1204,7 +1206,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 empty_ss}
+ empty simpset, i.e., @{ML [index] empty_ss}
@{ML_response_fake [display,gray]
"print_ss @{context} empty_ss"
@@ -1251,7 +1253,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 HOL_basic_ss}. While
+ In the context of HOL, the first really useful simpset is @{ML [index] HOL_basic_ss}. While
printing out the components of this simpset
@{ML_response_fake [display,gray]
@@ -1278,9 +1280,9 @@
text {*
This behaviour is not because of simplification rules, but how the subgoaler, solver
- and looper are set up in @{ML HOL_basic_ss}.
+ and looper are set up in @{ML [index] HOL_basic_ss}.
- The simpset @{ML HOL_ss} is an extension of @{ML HOL_basic_ss} containing
+ The simpset @{ML [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing
already many useful simplification and congruence rules for the logical
connectives in HOL.
@@ -1300,7 +1302,7 @@
The simplifier is often used to unfold definitions in a proof. For this the
- simplifier implements the tactic @{ML rewrite_goals_tac}.\footnote{FIXME:
+ simplifier implements the tactic @{ML [index] rewrite_goals_tac}.\footnote{FIXME:
see LocalDefs infrastructure.} Suppose for example the
definition
*}
@@ -1614,7 +1616,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 addsimprocs} to a simpset whenever
+ @{ML [index] addsimprocs} to a simpset whenever
needed.
Simprocs are applied from inside to outside and from left to right. You can
@@ -1700,7 +1702,7 @@
| dest_suc_trm t = snd (HOLogic.dest_number t)*}
text {*
- It uses the library function @{ML dest_number in HOLogic} that transforms
+ It uses the library function @{ML [index] dest_number in HOLogic} that transforms
(Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
on, into integer values. This function raises the exception @{ML TERM}, if
the term is not a number. The next function expects a pair consisting of a term
@@ -1820,21 +1822,21 @@
text {*
whereby the produced theorem is always a meta-equality. A simple conversion
- is the function @{ML "Conv.all_conv"}, which maps a @{ML_type cterm} to an
+ is the function @{ML [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
instance of the (meta)reflexivity theorem. For example:
@{ML_response_fake [display,gray]
"Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
"Foo \<or> Bar \<equiv> Foo \<or> Bar"}
- Another simple conversion is @{ML Conv.no_conv} which always raises the
+ Another simple conversion is @{ML [index] no_conv in Conv} which always raises the
exception @{ML CTERM}.
@{ML_response_fake [display,gray]
"Conv.no_conv @{cterm True}"
"*** Exception- CTERM (\"no conversion\", []) raised"}
- A more interesting conversion is the function @{ML "Thm.beta_conversion"}: it
+ A more interesting conversion is the function @{ML [index] beta_conversion in Thm}: it
produces a meta-equation between a term and its beta-normal form. For example
@{ML_response_fake [display,gray]
@@ -1850,7 +1852,7 @@
Note that the actual response in this example is @{term "2 + 10 \<equiv> 2 + (10::nat)"},
since the pretty-printer for @{ML_type cterm}s eta-normalises terms.
But how we constructed the term (using the function
- @{ML Thm.capply}, which is the application @{ML $} for @{ML_type cterm}s)
+ @{ML [index] capply in Thm}, which is the application @{ML $} for @{ML_type cterm}s)
ensures that the left-hand side must contain beta-redexes. Indeed
if we obtain the ``raw'' representation of the produced theorem, we
can see the difference:
@@ -1904,15 +1906,15 @@
end"
"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
- Note, however, that the function @{ML Conv.rewr_conv} only rewrites the
+ Note, however, that the function @{ML [index] rewr_conv in Conv} only rewrites the
outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
exactly the
- left-hand side of the theorem, then @{ML Conv.rewr_conv} fails by raising
+ left-hand side of the theorem, then @{ML [index] rewr_conv in Conv} fails by 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 then_conv},
+ combinators. The simplest conversion combinator is @{ML [index] then_conv},
which applies one conversion after another. For example
@{ML_response_fake [display,gray]
@@ -1929,7 +1931,7 @@
@{thm [source] true_conj1}. (Recall the problem with the pretty-printer
normalising all terms.)
- The conversion combinator @{ML else_conv} tries out the
+ The conversion combinator @{ML [index] else_conv} tries out the
first one, and if it does not apply, tries the second. For example
@{ML_response_fake [display,gray]
@@ -1944,10 +1946,10 @@
Here the conversion of @{thm [source] true_conj1} only applies
in the first case, but fails in the second. The whole conversion
- does not fail, however, because the combinator @{ML Conv.else_conv} will then
- try out @{ML Conv.all_conv}, which always succeeds.
+ 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 Conv.try_conv} constructs a conversion
+ The conversion combinator @{ML [index] try_conv in Conv} constructs a conversion
which is tried out on a term, but in case of failure just does nothing.
For example
@@ -1958,7 +1960,7 @@
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 combinator @{ML Conv.arg_conv} will apply
+ will lift this restriction. The combinator @{ML [index] arg_conv in Conv} will apply
the conversion to the first argument of an application, that is the term
must be of the form @{ML "t1 $ t2" for t1 t2} and the conversion is applied
to @{text t2}. For example
@@ -1975,10 +1977,10 @@
The reason for this behaviour is that @{text "(op \<or>)"} expects two
arguments. Therefore the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
conversion is then applied to @{text "t2"} which in the example above
- stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
+ stands for @{term "True \<and> Q"}. The function @{ML [index] fun_conv in Conv} applies
the conversion to the first argument of an application.
- The function @{ML Conv.abs_conv} applies a conversion under an abstraction.
+ The function @{ML [index] abs_conv in Conv} applies a conversion under an abstraction.
For example:
@{ML_response_fake [display,gray]
@@ -1991,7 +1993,7 @@
"\<lambda>P. True \<and> P \<and> Foo \<equiv> \<lambda>P. P \<and> Foo"}
Note that this conversion needs a context as an argument. The conversion that
- goes under an application is @{ML Conv.combination_conv}. It expects two conversions
+ goes under an application is @{ML [index] combination_conv in Conv}. It expects two conversions
as arguments, each of which is applied to the corresponding ``branch'' of the
application.
@@ -2059,7 +2061,7 @@
text {*
So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
- also work on theorems using the function @{ML "Conv.fconv_rule"}. As an example,
+ also work on theorems using the function @{ML [index] fconv_rule in Conv}. As an example,
consider the conversion @{ML all_true1_conv} and the lemma:
*}
@@ -2074,12 +2076,12 @@
"?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 CONVERSION},
+ goal states. This can be done with the help of the function @{ML [index] CONVERSION},
and also some predefined conversion combinators that traverse a goal
- state. The combinators for the goal state are: @{ML Conv.params_conv} for
+ state. The combinators for the goal state are: @{ML [index] params_conv in Conv} for
converting under parameters (i.e.~where goals are of the form @{text "\<And>x. P \<Longrightarrow>
- Q"}); the function @{ML Conv.prems_conv} for applying a conversion to all
- premises of a goal, and @{ML Conv.concl_conv} for applying a conversion to
+ Q"}); the function @{ML [index] prems_conv in Conv} for applying a conversion to all
+ premises of a goal, and @{ML [index] concl_conv in Conv} for applying a conversion to
the conclusion of a goal.
Assume we want to apply @{ML all_true1_conv} only in the conclusion
--- a/ProgTutorial/antiquote_setup.ML Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML Sat May 30 17:40:20 2009 +0200
@@ -1,10 +1,12 @@
(* Auxiliary antiquotations for the tutorial. *)
-structure AntiquoteSetup: sig end =
+structure AntiquoteSetup =
struct
+open OutputTutorial
+
(* functions for generating appropriate expressions *)
-fun ml_val_open (ys, xs) txt =
+fun ml_val_open ys xs txt =
let fun ml_val_open_aux ys txt =
"fn " ^ (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) ^ " => (" ^ txt ^ ")";
in
@@ -13,7 +15,7 @@
| _ => ml_val_open_aux ys ("let open " ^ (space_implode " " xs) ^ " in " ^ txt ^ " end"))
end;
-fun ml_val txt = ml_val_open ([],[]) txt;
+fun ml_val txt = ml_val_open [] [] txt;
fun ml_pat (lhs, pat) =
let
@@ -28,8 +30,8 @@
ML_Context.eval_in (SOME ctxt) false Position.none exp
(* string functions *)
-fun string_explode str txt =
- map (fn s => str ^ s) (space_explode "\n" txt)
+fun string_explode prefix_str txt =
+ map (fn s => prefix_str ^ s) (split_lines txt)
val transform_cmts_str =
Source.of_string
@@ -37,45 +39,49 @@
#> Source.exhaust
#> Chunks.transform_cmts
#> implode
- #> string_explode "";
-
-(* output function *)
-fun output_fn txt = OutputFN.output txt
+ #> string_explode ""
(* checks and prints open expressions *)
-fun output_ml {context = ctxt, ...} (txt, ovars) =
- (eval_fn ctxt (ml_val_open ovars txt);
- output_fn (transform_cmts_str txt))
+fun output_ml {context = ctxt, ...} (txt, (ovars, structs)) =
+ (eval_fn ctxt (ml_val_open ovars structs txt);
+ if structs = []
+ then output_indexed (transform_cmts_str txt) {main = Code txt, minor = ""}
+ else output_indexed (transform_cmts_str txt)
+ {main = Code txt, minor = ("in {\\tt\\slshape{}" ^ (implode structs) ^ "}")})
val parser_ml = Scan.lift (Args.name --
(Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) []))
(* checks and prints types and structures *)
-fun output_exp ml {context = ctxt, ...} txt =
- (eval_fn ctxt (ml txt);
- output_fn (string_explode "" txt))
+fun output_struct {context = ctxt, ...} txt =
+ (eval_fn ctxt (ml_struct txt);
+ output_indexed (string_explode "" txt) {main = Code txt, minor = "structure"})
+
+fun output_type {context = ctxt, ...} txt =
+ (eval_fn ctxt (ml_type txt);
+ output_indexed (string_explode "" txt) {main = Code txt, minor = "type"})
(* checks and expression agains a result pattern *)
fun output_response {context = ctxt, ...} (lhs, pat) =
(eval_fn ctxt (ml_pat (lhs, pat));
- output_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
+ output ((string_explode "" lhs) @ (string_explode "> " 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_fn ((string_explode "" lhs) @ (string_explode "> " pat)))
+ output ((string_explode "" lhs) @ (string_explode "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
fun ouput_response_fake_both _ (lhs, pat) =
- output_fn ((string_explode "" lhs) @ (string_explode "> " pat))
+ output ((string_explode "" lhs) @ (string_explode "> " pat))
val single_arg = Scan.lift (Args.name)
val two_args = Scan.lift (Args.name -- Args.name)
val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
-val _ = ThyOutput.antiquotation "ML_type" single_arg (output_exp ml_type)
-val _ = ThyOutput.antiquotation "ML_struct" single_arg (output_exp ml_struct)
+val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
+val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
val _ = ThyOutput.antiquotation "ML_response" two_args output_response
val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
@@ -91,7 +97,7 @@
(* 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_fn [href_link txt]
+ then output [href_link txt]
else error ("Source file " ^ (quote txt) ^ " does not exist."))
val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
--- a/ProgTutorial/chunks.ML Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/chunks.ML Sat May 30 17:40:20 2009 +0200
@@ -125,7 +125,7 @@
end)
val txt = spc ^ implode (transform_cmts toks')
in
- txt |> split_lines |> OutputFN.output
+ OutputTutorial.output (split_lines txt)
end;
val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;
--- a/ProgTutorial/document/root.tex Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/document/root.tex Sat May 30 17:40:20 2009 +0200
@@ -31,6 +31,7 @@
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% indexing
\makeindex
+\newcommand{\indexdef}[2]{\index{#1 (#2)}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% For cross references to the other manuals:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/output_tutorial.ML Sat May 30 17:40:20 2009 +0200
@@ -0,0 +1,101 @@
+
+structure OutputTutorial =
+struct
+
+(* rebuilding the output function from ThyOutput in order to *)
+(* enable the options [gray, linenos, index] *)
+
+val gray = ref false
+val linenos = ref false
+
+fun output txt =
+let
+ val prts = map Pretty.str txt
+in
+ prts
+ |> (if ! ThyOutput.quotes then map Pretty.quote else I)
+ |> (if ! ThyOutput.display then
+ map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
+ #> space_implode "\\isasep\\isanewline%\n"
+ #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
+ #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
+ #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+ else
+ map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
+ #> space_implode "\\isasep\\isanewline%\n"
+ #> enclose "\\isa{" "}")
+end
+
+datatype qstring =
+ Plain of string
+| Code of string
+
+datatype entry =
+ No_Entry
+ | Default
+ | Explicit of string
+
+val index = ref No_Entry
+
+fun translate f = Symbol.explode #> map f #> implode;
+
+val clean_string = translate
+ (fn "_" => "\\_"
+ | "#" => "\\#"
+ | "<" => "\\isacharless"
+ | ">" => "\\isachargreater"
+ | "{" => "\\{"
+ | "|" => "\\isacharbar"
+ | "}" => "\\}"
+ | "$" => "\\isachardollar"
+ | "!" => "\\isacharbang"
+ | "\\<dash>" => "-"
+ | c => c);
+
+fun get_word str =
+let
+ fun only_letters [] = true
+ | 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)
+end
+
+fun get_qstring (Plain s) = get_word s
+ | get_qstring (Code s) = let val w = get_word s in (w ^ "@{\\tt\\slshape{}" ^ w ^ "}") end
+
+fun is_empty_qstr (Plain "") = true
+ | is_empty_qstr (Code "") = true
+ | is_empty_qstr _ = false
+
+fun get_index_info {main = m, minor = n} =
+ (if n = ""
+ then "\\index{" ^ (get_qstring m) ^ "}"
+ else "\\indexdef{" ^ (get_qstring m) ^ "}{" ^ 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 =
+ txt |> output
+ |> index_entry (!index) index_info
+
+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)]
+
+
+end
\ No newline at end of file
--- a/ProgTutorial/outputfn.ML Sat May 30 11:12:46 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,79 +0,0 @@
-
-structure OutputFN =
-struct
-
-(* rebuilding the output function from ThyOutput in order to *)
-(* enable the options [gray, linenos, index] *)
-
-val gray = ref false
-val linenos = ref false
-
-datatype entry =
- No_Entry
- | Code_Entry of string
- | String_Entry of string
-
-val index = ref No_Entry
-
-fun string_entry s = prefix ("\\index{" ^ s ^ "}")
-fun code_entry s = prefix ("\\index{" ^ s ^ "@{\\tt\\slshape{}" ^ s ^ "}}")
-
-fun get_word str =
-let
- fun only_letters [] = true
- | only_letters (x::xs) =
- if (Symbol.is_ascii_blank x) then false else only_letters xs
-in
- if (only_letters (Symbol.explode str)) then str
- else error ("Underspecified index entry only for single words allowed! Error with " ^ str)
-end
-
-fun index_entry entry txt =
- case entry of
- No_Entry => I
- | String_Entry "" => string_entry (get_word (implode txt))
- | String_Entry s => string_entry s
- | Code_Entry "" => code_entry (get_word (implode txt))
- | Code_Entry s => code_entry s
-
-
-fun translate f = Symbol.explode #> map f #> implode;
-
-val clean_string = translate
- (fn "_" => "\\_"
- | c => c);
-
-fun output txt =
-let
- val prts = map Pretty.str txt
-in
- prts
- |> (if ! ThyOutput.quotes then map Pretty.quote else I)
- |> (if ! ThyOutput.display then
- map (Output.output o Pretty.string_of o Pretty.indent (! ThyOutput.indent))
- #> space_implode "\\isasep\\isanewline%\n"
- #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
- #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
- #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- #> index_entry (!index) txt
- else
- map (Output.output o (if ! ThyOutput.break then Pretty.string_of else Pretty.str_of))
- #> space_implode "\\isasep\\isanewline%\n"
- #> enclose "\\isa{" "}"
- #> index_entry (!index) txt)
-end
-
-
-fun boolean "" = true
- | boolean "true" = true
- | boolean "false" = false
- | boolean s = error ("Bad boolean value: " ^ quote s);
-
-val _ = ThyOutput.add_options
- [("gray", Library.setmp gray o boolean),
- ("linenos", Library.setmp linenos o boolean),
- ("index", Library.setmp index o String_Entry o clean_string),
- ("indexc", Library.setmp index o Code_Entry o clean_string)]
-
-
-end
\ No newline at end of file
Binary file progtutorial.pdf has changed