
diff -r 95461cf6fd07 -r 5fc2fb34c323 ProgTutorial/Essential.thy
--- 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 ":"}




