--- a/ProgTutorial/Advanced.thy Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/Advanced.thy Fri Jan 08 21:31:45 2010 +0100
@@ -11,7 +11,7 @@
(*>*)
-chapter {* Advanced Isabelle *}
+chapter {* Advanced Isabelle\label{chp:advanced} *}
text {*
\begin{flushright}
@@ -225,11 +225,71 @@
*}
-section {* Managing Name Spaces (TBD) *}
+section {* What Is In an Isabelle Name? (TBD) *}
+
+text {*
+ On the ML-level of Isabelle, you often have to work with qualified names.
+ These are strings with some additional information, such as positional
+ information and qualifiers. Such qualified names can be generated with the
+ antiquotation @{text "@{binding \<dots>}"}. For example
+
+ @{ML_response [display,gray]
+ "@{binding \"name\"}"
+ "name"}
+
+ An example where a qualified name is needed is the function
+ @{ML_ind define in Local_Theory}. This function is used below to define
+ the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
+*}
+
+local_setup %gray {*
+ Local_Theory.define ((@{binding "TrueConj"}, NoSyn),
+ (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
+
+text {*
+ Now querying the definition you obtain:
+
+ \begin{isabelle}
+ \isacommand{thm}~@{text "TrueConj_def"}\\
+ @{text "> "}~@{thm TrueConj_def}
+ \end{isabelle}
+
+ \begin{readmore}
+ The basic operations on bindings are implemented in
+ @{ML_file "Pure/General/binding.ML"}.
+ \end{readmore}
+
+ \footnote{\bf FIXME give a better example why bindings are important}
+ \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
+ why @{ML snd} is needed.}
+ \footnote{\bf FIXME: There should probably a separate section on binding, long-names
+ and sign.}
+
+*}
+
ML {* Sign.intern_type @{theory} "list" *}
ML {* Sign.intern_const @{theory} "prod_fun" *}
+text {*
+ \footnote{\bf FIXME: Explain the following better; maybe put in a separate
+ section and link with the comment in the antiquotation section.}
+
+ Occasionally you have to calculate what the ``base'' name of a given
+ 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\""}
+
+ The difference between both functions is that @{ML extern_const in Sign} returns
+ the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
+ strips off all qualifiers.
+
+ \begin{readmore}
+ Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
+ functions about signatures in @{ML_file "Pure/sign.ML"}.
+ \end{readmore}
+*}
text {*
@{ML_ind "Binding.str_of"} returns the string with markup;
--- a/ProgTutorial/Essential.thy Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/Essential.thy Fri Jan 08 21:31:45 2010 +0100
@@ -22,11 +22,10 @@
\medskip
Isabelle is build around a few central ideas. One central idea is the
- LCF-approach to theorem proving where there is a small trusted core and
- everything else is built on top of this trusted core
- \cite{GordonMilnerWadsworth79}. The fundamental data
- structures involved in this core are certified terms and certified types,
- as well as theorems.
+ LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there
+ is a small trusted core and everything else is built on top of this trusted
+ core. The fundamental data structures involved in this core are certified
+ terms and certified types, as well as theorems.
*}
@@ -113,6 +112,7 @@
"Type unification failed: Occurs check!"}
raises a typing error, while it perfectly ok to construct the term
+ with the raw ML-constructors:
@{ML_response_fake [display,gray]
"let
@@ -121,8 +121,6 @@
tracing (string_of_term @{context} omega)
end"
"x x"}
-
- with the raw ML-constructors.
Sometimes the internal representation of terms can be surprisingly different
from what you see at the user-level, because the layers of
@@ -192,8 +190,8 @@
"@{typ \"bool\"}"
"bool"}
- that is the pretty printed version of @{text "bool"}. However, in PolyML
- (version 5.3) it is easy to install your own pretty printer. With the
+ which is the pretty printed version of @{text "bool"}. However, in PolyML
+ (version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the
function below we mimic the behaviour of the usual pretty printer for
datatypes (it uses pretty-printing functions which will be explained in more
detail in Section~\ref{sec:pretty}).
@@ -325,12 +323,13 @@
@{ML_response_fake [display,gray]
"let
- val trm = @{term \"P::nat\"}
+ val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}
val args = [@{term \"True\"}, @{term \"False\"}]
in
list_comb (trm, args)
end"
-"Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
+"Free (\"P\", \"bool \<Rightarrow> bool \<Rightarrow> bool\")
+ $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
Another handy function is @{ML_ind lambda in Term}, which abstracts a variable
in a term. For example
@@ -450,10 +449,9 @@
"(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
There are also many convenient functions that construct specific HOL-terms
- in the structure @{ML_struct HOLogic}. For
- 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
+ in the structure @{ML_struct HOLogic}. For 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
@{ML_response_fake [gray,display]
"let
@@ -463,9 +461,7 @@
|> tracing
end"
"True = False"}
-*}
-
-text {*
+
\begin{readmore}
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
"Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make manual
@@ -562,24 +558,6 @@
@{ML_response [display,gray]
"@{type_name \"list\"}" "\"List.list\""}
- \footnote{\bf FIXME: Explain the following better; maybe put in a separate
- section and link with the comment in the antiquotation section.}
-
- Occasionally you have to calculate what the ``base'' name of a given
- 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\""}
-
- The difference between both functions is that @{ML extern_const in Sign} returns
- the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
- strips off all qualifiers.
-
- \begin{readmore}
- Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
- functions about signatures in @{ML_file "Pure/sign.ML"}.
- \end{readmore}
-
Although types of terms can often be inferred, there are many
situations where you need to construct types manually, especially
when defining constants. For example the function returning a function
@@ -718,7 +696,7 @@
The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
environment, which is needed for starting the unification without any
(pre)instantiations. The @{text 0} is an integer index that will be explained
- below. In case of failure @{ML typ_unify in Sign} will throw the exception
+ below. In case of failure, @{ML typ_unify in Sign} will throw the exception
@{text TUNIFY}. We can print out the resulting type environment bound to
@{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
structure @{ML_struct Vartab}.
@@ -987,16 +965,16 @@
*}
text {*
- Unification of abstractions is more thoroughly studied in the context
- of higher-order pattern unification and higher-order pattern matching. A
- \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the
- first symbol under an abstraction) is either a constant, a schematic or a free
- variable. If it is a schematic variable then it can only have distinct bound
- variables as arguments. This excludes terms where a schematic variable is an
- argument of another one and where a schematic variable is applied
- twice with the same bound variable. The function @{ML_ind pattern in Pattern}
- in the structure @{ML_struct Pattern} tests whether a term satisfies these
- restrictions.
+ Unification of abstractions is more thoroughly studied in the context of
+ higher-order pattern unification and higher-order pattern matching. A
+ \emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that
+ is the first symbol under an abstraction) is either a constant, a schematic
+ variable or a free variable. If it is a schematic variable then it can only
+ have distinct bound variables as arguments. This excludes terms where a
+ schematic variable is an argument of another one and where a schematic
+ variable is applied twice with the same bound variable. The function
+ @{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
+ whether a term satisfies these restrictions.
@{ML_response [display, gray]
"let
@@ -1014,9 +992,9 @@
are decidable and produce most general unifiers, respectively matchers.
In this way, matching and unification can be implemented as functions that
produce a type and term environment (unification actually returns a
- record of type @{ML_type Envir.env} containing a maxind, a type environment
- and a term environment). The corresponding functions are @{ML_ind match in Pattern},
- and @{ML_ind unify in Pattern} both implemented in the structure
+ record of type @{ML_type Envir.env} containing a max-index, a type environment
+ and a term environment). The corresponding functions are @{ML_ind match in Pattern}
+ and @{ML_ind unify in Pattern}, both implemented in the structure
@{ML_struct Pattern}. An example for higher-order pattern unification is
@{ML_response_fake [display, gray]
@@ -1034,16 +1012,16 @@
max-index for the schematic variables (in the example the index is @{text
0}) and empty type and term environments. The function @{ML_ind
"Envir.term_env"} pulls out the term environment from the result record. The
- function for type environment is @{ML_ind "Envir.type_env"}. An assumption of
- this function is that the terms to be unified have already the same type. In
- case of failure, the exceptions that are raised are either @{text Pattern},
- @{text MATCH} or @{text Unif}.
+ corresponding function for type environment is @{ML_ind
+ "Envir.type_env"}. An assumption of this function is that the terms to be
+ unified have already the same type. In case of failure, the exceptions that
+ are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
As mentioned before, unrestricted higher-order unification, respectively
- higher-order matching, is in general undecidable and might also not posses a
- single most general solution. Therefore Isabelle implements the unification
- function @{ML_ind unifiers in Unify} so that it returns a lazy list of
- potentially infinite unifiers. An example is as follows
+ unrestricted higher-order matching, is in general undecidable and might also
+ not posses a single most general solution. Therefore Isabelle implements the
+ unification function @{ML_ind unifiers in Unify} so that it returns a lazy
+ list of potentially infinite unifiers. An example is as follows
*}
ML{*val uni_seq =
@@ -1118,20 +1096,22 @@
problem can be solved by first-order matching.
Higher-order matching might be necessary for instantiating a theorem
- appropriately (theorems and their instantiation will be described in more
- detail in Sections~\ref{sec:theorems}). This is for example the
- case when applying the rule @{thm [source] spec}:
+ appropriately. More on this will be given in Sections~\ref{sec:theorems}.
+ Here we only have a look at a simple case, namely the theorem
+ @{thm [source] spec}:
\begin{isabelle}
\isacommand{thm}~@{thm [source] spec}\\
@{text "> "}~@{thm spec}
\end{isabelle}
- as an introduction rule. One way is to instantiate this rule. The
- instantiation function for theorems is @{ML_ind instantiate in Drule} from
- the structure @{ML_struct Drule}. One problem, however, is that this
- function expects the instantiations as lists of @{ML_type ctyp} and
- @{ML_type cterm} pairs:
+ as an introduction rule. Applying it directly can lead to unexpected
+ behaviour since the unification has more than one solution. One way round
+ this problem is to instantiate the schematic variables @{text "?P"} and
+ @{text "?x"}. instantiation function for theorems is @{ML_ind instantiate
+ in Drule} from the structure @{ML_struct Drule}. One problem, however, is
+ that this function expects the instantiations as lists of @{ML_type ctyp}
+ and @{ML_type cterm} pairs:
\begin{isabelle}
@{ML instantiate in Drule}@{text ":"}
--- a/ProgTutorial/FirstSteps.thy Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/FirstSteps.thy Fri Jan 08 21:31:45 2010 +0100
@@ -218,13 +218,14 @@
*)
text {*
- Most often you want to inspect data of Isabelle's basic data
- structures, namely @{ML_type term}, @{ML_type cterm} and @{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 a bit unwieldy. One way to transform a term into a string is to use the
- function @{ML_ind string_of_term in Syntax} from the structure @{ML_struct
- Syntax}. For more convenience, we bind this function to the toplevel.
+ Most often you want to inspect data of Isabelle's basic data structures,
+ namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
+ and @{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 a bit unwieldy. One way to transform a term into a string
+ is to use the function @{ML_ind string_of_term in Syntax} from the structure
+ @{ML_struct Syntax}. For more convenience, we bind this function to the
+ toplevel.
*}
ML{*val string_of_term = Syntax.string_of_term*}
@@ -358,6 +359,20 @@
commas (map (string_of_thm_no_vars ctxt) thms) *}
text {*
+ The printing functions for types are
+*}
+
+ML{*fun string_of_typ ctxt ty = Syntax.string_of_typ ctxt ty
+fun string_of_typs ctxt tys = commas (map (string_of_typ ctxt) tys)*}
+
+text {*
+ respectively ctypes
+*}
+
+ML{*fun string_of_ctyp ctxt cty = string_of_typ ctxt (typ_of cty)
+fun string_of_ctyps ctxt ctys = commas (map (string_of_ctyp ctxt) ctys)*}
+
+text {*
\begin{readmore}
The simple conversion functions from Isabelle's main datatypes to
@{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}.
@@ -365,10 +380,10 @@
@{ML_file "Pure/Syntax/printer.ML"}.
\end{readmore}
- Note that for printing out several ``parcels'' of information that
- semantically belong together, like a warning message consisting of
- a term and its type, you should try to keep this information together in a
- single string. Therefore do \emph{not} print out information as
+ Note that for printing out several ``parcels'' of information that belong
+ together, like a warning message consisting of a term and its type, you
+ should try to print these parcels together in a single string. Therefore do
+ \emph{not} print out information as
@{ML_response_fake [display,gray]
"tracing \"First half,\";
@@ -388,11 +403,12 @@
@{ML_ind cat_lines in Library} concatenates a list of strings
and inserts newlines in between each element.
- @{ML_response [display, gray]
- "cat_lines [\"foo\", \"bar\"]"
- "\"foo\\nbar\""}
+ @{ML_response_fake [display, gray]
+ "tracing (cat_lines [\"foo\", \"bar\"])"
+ "foo
+bar"}
- Section \ref{sec:pretty} will also explain the infrastructure that Isabelle
+ Section \ref{sec:pretty} will explain the infrastructure that Isabelle
provides for more elaborate pretty printing.
\begin{readmore}
@@ -443,15 +459,15 @@
|> (fn x => x + 4)*}
text {*
- which increments its argument @{text x} by 5. It does this by first incrementing
- the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
- the first component of the pair (Line 4) and finally incrementing the first
- component by 4 (Line 5). This kind of cascading manipulations of values is quite
- common when dealing with theories (for example by adding a definition, followed by
- lemmas and so on). The reverse application allows you to read what happens in
- a top-down manner. This kind of coding should also be familiar,
- if you have been exposed to Haskell's {\it do}-notation. Writing the function
- @{ML inc_by_five} using the reverse application is much clearer than writing
+ which increments its argument @{text x} by 5. It does this by first
+ incrementing the argument by 1 (Line 2); then storing the result in a pair
+ (Line 3); taking the first component of the pair (Line 4) and finally
+ incrementing the first component by 4 (Line 5). This kind of cascading
+ manipulations of values is quite common when dealing with theories. The
+ reverse application allows you to read what happens in a top-down
+ manner. This kind of coding should be familiar, if you have been exposed to
+ Haskell's {\it do}-notation. Writing the function @{ML inc_by_five} using
+ the reverse application is much clearer than writing
*}
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
@@ -495,10 +511,10 @@
@{ML_response_fake [display,gray]
"let
- val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+ val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
val ctxt = @{context}
in
- apply_fresh_args t ctxt
+ apply_fresh_args trm ctxt
|> string_of_term ctxt
|> tracing
end"
@@ -512,21 +528,20 @@
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 list_comb in Term} to the term. In this last step we have
+ function @{ML_ind list_comb in Term} to the original term. In this last step we have
to use the function @{ML_ind curry in Library}, because @{ML list_comb}
expects the function and the variables list as a pair.
- Functions like @{ML apply_fresh_args} are often needed when constructing
- terms with fresh variables. The
- infrastructure helps tremendously to avoid any name clashes. Consider for
- example:
+ Functions like @{ML apply_fresh_args} are often needed when constructing
+ terms involving fresh variables. For this the infrastructure helps
+ tremendously to avoid any name clashes. Consider for example:
@{ML_response_fake [display,gray]
"let
- val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+ val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
val ctxt = @{context}
in
- apply_fresh_args t ctxt
+ apply_fresh_args trm ctxt
|> string_of_term ctxt
|> tracing
end"
@@ -544,13 +559,13 @@
(fn x => x + 3)*}
text {*
- which is the function composed of first the increment-by-one function and then
- increment-by-two, followed by increment-by-three. Again, the reverse function
- composition allows you to read the code top-down. This combinator is often used
- for setup function inside the \isacommand{setup}-command. These function have to be
- of type @{ML_type "theory -> theory"} in order to install, for example, some new
- data inside the current theory. More than one such setup function can be composed
- with @{ML "#>"}. For example
+ which is the function composed of first the increment-by-one function and
+ then increment-by-two, followed by increment-by-three. Again, the reverse
+ function composition allows you to read the code top-down. This combinator
+ is often used for setup functions inside the
+ \isacommand{setup}-command. These functions have to be of type @{ML_type
+ "theory -> theory"}. More than one such setup function can be composed with
+ @{ML "#>"}. For example
*}
setup %gray {* let
@@ -624,7 +639,7 @@
intermediate values in functions that return pairs. As an example, suppose you
want to separate a list of integers into two lists according to a
treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
- should be separated to @{ML "([1,2,3,4], [6,5])"}. This function can be
+ should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be
implemented as
*}
@@ -638,8 +653,8 @@
text {*
where the return value of the recursive call is bound explicitly to
- the pair @{ML "(los, grs)" for los grs}. You can implement this function
- more concisely as
+ the pair @{ML "(los, grs)" for los grs}. However, this function
+ can be implemented more concisely as
*}
ML{*fun separate i [] = ([], [])
@@ -721,8 +736,8 @@
sometimes necessary to do some ``plumbing'' in order to fit functions
together. We have already seen such plumbing in the function @{ML
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
- list_comb}, which works over pairs to fit with the combinator @{ML "|>"}. Such
- plumbing is also needed in situations where a function operate over lists,
+ list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such
+ plumbing is also needed in situations where a function operates over lists,
but one calculates only with a single element. An example is the function
@{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
a list of terms. Consider the code:
@@ -811,27 +826,48 @@
ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
text {*
-
does \emph{not} return the name of the current theory, if it is run in a
different theory. Instead, the code above defines the constant function
that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
\emph{not} replaced with code that will look up the current theory in
some data structure and return it. Instead, it is literally
- replaced with the value representing the theory name.
+ replaced with the value representing the theory.
+
+ Another important antiquotation is @{text "@{context}"}. (What the
+ difference between a theory and a context is will be described in Chapter
+ \ref{chp:advanced}.) A context is for example needed in order to use the
+ function @{ML print_abbrevs in ProofContext} that list of all currently
+ defined abbreviations.
- In a similar way you can use antiquotations to refer to proved theorems:
+ @{ML_response_fake [display, gray]
+ "ProofContext.print_abbrevs @{context}"
+"Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
+INTER \<equiv> INFI
+Inter \<equiv> Inf
+\<dots>"}
+
+ You can also use antiquotations to refer to proved theorems:
@{text "@{thm \<dots>}"} for a single theorem
@{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
and @{text "@{thms \<dots>}"} for more than one
-@{ML_response_fake [display,gray] "@{thms conj_ac}"
+@{ML_response_fake [display,gray]
+ "@{thms conj_ac}"
"(?P \<and> ?Q) = (?Q \<and> ?P)
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
+ The thm-antiquotations can also be used for manipulating theorems. For
+ example, if you need the version of te theorem @{thm [source] refl} that
+ has a meta-equality instead of an equality, you can write
+
+@{ML_response_fake [display,gray]
+ "@{thm refl[THEN eq_reflection]}"
+ "?x \<equiv> ?x"}
+
The point of these antiquotations is that referring to theorems in this way
makes your code independent from what theorems the user might have stored
under this name (this becomes especially important when you deal with
@@ -848,9 +884,9 @@
The result can be printed out as follows.
@{ML_response_fake [gray,display]
-"foo_thm |> string_of_thms @{context}
+"foo_thm |> string_of_thms_no_vars @{context}
|> tracing"
- "True, True"}
+ "True, False \<Longrightarrow> P"}
You can also refer to the current simpset via an antiquotation. To illustrate
this we implement the function that extracts the theorem names stored in a
@@ -866,7 +902,7 @@
text {*
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
+ information stored in the simpset, but here 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}"}.
@@ -878,43 +914,6 @@
of lemmas to the simpset by the user, which can potentially cause loops in your
code.
- On the ML-level of Isabelle, you often have to work with qualified names.
- These are strings with some additional information, such as positional
- information and qualifiers. Such qualified names can be generated with the
- antiquotation @{text "@{binding \<dots>}"}. For example
-
- @{ML_response [display,gray]
- "@{binding \"name\"}"
- "name"}
-
- An example where a qualified name is needed is the function
- @{ML_ind define in Local_Theory}. This function is used below to define
- the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
-*}
-
-local_setup %gray {*
- Local_Theory.define ((@{binding "TrueConj"}, NoSyn),
- (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
-
-text {*
- Now querying the definition you obtain:
-
- \begin{isabelle}
- \isacommand{thm}~@{text "TrueConj_def"}\\
- @{text "> "}~@{thm TrueConj_def}
- \end{isabelle}
-
- \begin{readmore}
- The basic operations on bindings are implemented in
- @{ML_file "Pure/General/binding.ML"}.
- \end{readmore}
-
- \footnote{\bf FIXME give a better example why bindings are important}
- \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
- why @{ML snd} is needed.}
- \footnote{\bf FIXME: There should probably a separate section on binding, long-names
- and sign.}
-
It is also possible to define your own antiquotations. But you should
exercise care when introducing new ones, as they can also make your code
also difficult to read. In the next chapter we describe how to construct
@@ -1202,7 +1201,7 @@
fun init _ = [])*}
text {*
- The function we have to specify has to produce a list once a context
+ The init-function we have to specify must produce a list for when a context
is initialised (possibly taking the theory into account from which the
context is derived). We choose here to just return the empty list. Next
we define two auxiliary functions for updating the list with a given
@@ -1239,11 +1238,11 @@
2, 1"}
Many functions in Isabelle manage and update data in a similar
- fashion. Consequently, such calculation with contexts occur frequently in
+ fashion. Consequently, such calculations with contexts occur frequently in
Isabelle code, although the ``context flow'' is usually only linear.
Note also that the calculation above has no effect on the underlying
theory. Once we throw away the contexts, we have no access to their
- associated data. This is different to theories, where the command
+ associated data. This is different for theories, where the command
\isacommand{setup} registers the data with the current and future
theories, and therefore one can access the data potentially
indefinitely.
--- a/ProgTutorial/Intro.thy Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/Intro.thy Fri Jan 08 21:31:45 2010 +0100
@@ -40,7 +40,7 @@
operating system or editor in which Isabelle is used. If you have comments,
criticism or like to add to the tutorial, please feel free---you are most
welcome! The tutorial is meant to be gentle and comprehensive. To achieve
- this we need your feedback.
+ this we need your help and feedback.
*}
section {* Intended Audience and Prior Knowledge *}
@@ -62,8 +62,8 @@
\begin{description}
\item[The Isabelle/Isar Implementation Manual] describes Isabelle
- from a high-level perspective, documenting both the underlying
- concepts and some of the interfaces.
+ from a high-level perspective, documenting some of the underlying
+ concepts and interfaces.
\item[The Isabelle Reference Manual] is an older document that used
to be the main reference of Isabelle at a time when all proof scripts
@@ -84,8 +84,8 @@
good to look at code that does similar things as you want to do and
learn from it. This tutorial contains frequently pointers to the
Isabelle sources. Still, the UNIX command \mbox{@{text "grep -R"}} is
- often your best friend while programming with Isabelle, or
- hypersearch if you program using jEdit under MacOSX. To understand the sources,
+ often your best friend while programming with Isabelle.\footnote{Or
+ hypersearch if you program using jEdit under MacOSX.} To understand the sources,
it is often also necessary to track the change history of a file or
files. The Mercurial repository\footnote{\url{http://isabelle.in.tum.de/repos/isabelle/}}
for Isabelle provides convenient interfaces to query the history of
@@ -136,8 +136,9 @@
\end{readmore}
The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
- repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
- {http://isabelle.in.tum.de/repos/isabelle/}.
+ repository at \href{http://isabelle.in.tum.de/repos/isabelle/}
+ {http://isabelle.in.tum.de/repos/isabelle/}, not the latest release
+ of Isabelle.
A few exercises are scattered around the text. Their solutions are given
in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
@@ -216,9 +217,9 @@
\begin{itemize}
\item {\bf Stefan Berghofer} wrote nearly all of the ML-code of the
\simpleinductive-package and the code for the @{text
- "chunk"}-antiquotation. He also wrote the first version of this chapter
- describing the package and has been helpful \emph{beyond measure} with
- answering questions about Isabelle.
+ "chunk"}-antiquotation. He also wrote the first version of chapter
+ \ref{chp:package} describing this package and has been helpful \emph{beyond
+ measure} with answering questions about Isabelle.
\item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty}.
@@ -227,15 +228,15 @@
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
are by him.
- \item {\bf Lukas Bulwahn} made me aware of the problems with recursive
+ \item {\bf Lukas Bulwahn} made me aware of a problem with recursive
parsers and contributed exercise \ref{ex:contextfree}.
- \item {\bf Jeremy Dawson} wrote the first version of the chapter
+ \item {\bf Jeremy Dawson} wrote the first version of chapter \ref{chp:parsing}
about parsing.
\item {\bf Armin Heller} helped with recipe \ref{rec:sat}.
- \item {\bf Alexander Krauss} wrote the first version of the ``first-steps''
+ \item {\bf Alexander Krauss} wrote a very early version of the ``first-steps''
chapter and also contributed the material on @{ML_funct Named_Thms}.
\item {\bf Christian Sternagel} proofread the tutorial and made
--- a/ProgTutorial/Parsing.thy Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/Parsing.thy Fri Jan 08 21:31:45 2010 +0100
@@ -12,7 +12,7 @@
*}
(*>*)
-chapter {* Parsing *}
+chapter {* Parsing\label{chp:parsing} *}
text {*
Isabelle distinguishes between \emph{outer} and \emph{inner}
Binary file progtutorial.pdf has changed