isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:95461cf6fd07
+:5fc2fb34c323
 24~Nov.~2009
 \end{flushright}
 \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
+LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there
-everything else is built on top of this trusted core
+is a small trusted core and everything else is built on top of this trusted
-\cite{GordonMilnerWadsworth79}. The fundamental data
+core. The fundamental data structures involved in this core are certified
-structures involved in this core are certified terms and certified types,
+terms and certified types, as well as theorems.
-as well as theorems.
 *}
 section {* Terms and Types *}
 @{ML_response_fake_both [display,gray]
 "@{term \"x x\"}"
 "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
 val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in
 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
 parsing/type-checking/pretty printing can be quite elaborate.
 @{ML_response [display, gray]
 "@{typ \"bool\"}"
 "bool"}
-that is the pretty printed version of @{text "bool"}. However, in PolyML
+which 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
+(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}).
 *}
 term list applied to the term. For example
 @{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
 @{ML_response_fake [display,gray]
 Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
 end"
 "(\"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
+in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in
-example @{ML_ind mk_eq in HOLogic} constructs an equality out of two terms.
+HOLogic} constructs an equality out of two terms.  The types needed in this
-The types needed in this equality are calculated from the type of the
+equality are calculated from the type of the arguments. For example
-arguments. For example
 @{ML_response_fake [gray,display]
 "let
 val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
 string_of_term @{context} eq
 |> 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
 constructions of terms and types easier.
 \end{readmore}
 The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
 For example
 @{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
 type is as follows:
 text {*
 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}.
 @{ML_response_fake [display,gray]
 end"
 "[?X := P]"}
 *}
 text {*
-Unification of abstractions is more thoroughly studied in the context
+Unification of abstractions is more thoroughly studied in the context of
-of higher-order pattern unification and higher-order pattern matching.  A
+higher-order pattern unification and higher-order pattern matching.  A
-\emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that is the
+\emph{\index*{pattern}} is an abstraction term whose ``head symbol'' (that
-first symbol under an abstraction) is either a constant, a schematic or a free
+is the first symbol under an abstraction) is either a constant, a schematic
-variable. If it is a schematic variable then it can only have distinct bound
+variable or a free variable. If it is a schematic variable then it can only
-variables as arguments. This excludes terms where a schematic variable is an
+have distinct bound variables as arguments. This excludes terms where a
-argument of another one and where a schematic variable is applied
+schematic variable is an argument of another one and where a schematic
-twice with the same bound variable. The function @{ML_ind pattern in Pattern}
+variable is applied twice with the same bound variable. The function
-in the structure @{ML_struct Pattern} tests whether a term satisfies these
+@{ML_ind pattern in Pattern} in the structure @{ML_struct Pattern} tests
-restrictions.
+whether a term satisfies these restrictions.
 @{ML_response [display, gray]
 "let
 val trm_list =
 [@{term_pat \"?X\"},              @{term_pat \"a\"},
 The point of the restriction to patterns is that unification and matching
 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
+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 a term environment). The corresponding functions are @{ML_ind match in Pattern}
-and @{ML_ind unify in Pattern} both implemented in the structure
+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]
 "let
 val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
 The function @{ML_ind "Envir.empty"} generates a record with a specified
 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
+corresponding function for type environment is @{ML_ind
-this function is that the terms to be unified have already the same type. In
+"Envir.type_env"}. An assumption of this function is that the terms to be
-case of failure, the exceptions that are raised are either @{text Pattern},
+unified have already the same type. In case of failure, the exceptions that
-@{text MATCH} or @{text Unif}.
+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
+unrestricted higher-order matching, is in general undecidable and might also
-single most general solution. Therefore Isabelle implements the unification
+not posses a single most general solution. Therefore Isabelle implements the
-function @{ML_ind unifiers in Unify} so that it returns a lazy list of
+unification function @{ML_ind unifiers in Unify} so that it returns a lazy
-potentially infinite unifiers.  An example is as follows
+list of potentially infinite unifiers.  An example is as follows
 *}
 ML{*val uni_seq =
 let
 val trm1 = @{term_pat "?X ?Y"}
 Unify}, this function does not raise an exception in case of failure, but
 returns an empty sequence. It also first tries out whether the matching
 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
+appropriately. More on this will be given in Sections~\ref{sec:theorems}.
-detail in Sections~\ref{sec:theorems}). This is for example the
+Here we only have a look at a simple case, namely the theorem
-case when applying the rule @{thm [source] spec}:
+@{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
+as an introduction rule. Applying it directly can lead to unexpected
-instantiation function for theorems is @{ML_ind instantiate in Drule} from
+behaviour since the unification has more than one solution. One way round
-the structure @{ML_struct Drule}. One problem, however, is that this
+this problem is to instantiate the schematic variables @{text "?P"} and
-function expects the instantiations as lists of @{ML_type ctyp} and
+@{text "?x"}.  instantiation function for theorems is @{ML_ind instantiate
-@{ML_type cterm} pairs:
+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 ":"}
 @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
 \end{isabelle}

changeset 414	5fc2fb34c323
parent 412	73f716b9201a
child 415	dc76ba24e81b