--- 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 ":"}