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