isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:83d5bca38bec
+:4c54ef4dc84d
 begin
 chapter {* Let's Talk About the Good, the Bad and the Ugly *}
 text {*
-Isabelle is build around a few central ideas. One is the LCF-approach to
+Isabelle is build around a few central ideas. One central idea is the
-theorem proving where there is a small trusted core and everything else is
+LCF-approach to theorem proving where there is a small trusted core and
-build on top of this trusted core. The central data structures involved
+everything else is build on top of this trusted core. The fundamental data
-in this core are certified terms and types as well as theorems.
+structures involved in this core are certified terms and types, as well as
+theorems.
 *}
 section {* Terms and Types *}
 text {*
-In Isabelle there are certified terms (respectively types) and uncertified
+There are certified terms and uncertified terms (respectively types).
-terms. The latter are called just terms. One way to construct them is by
+Uncertified terms are just called terms. One way to construct them is by
 using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
 @{ML_response [display,gray]
 "@{term \"(a::nat) + b = c\"}"
 "Const (\"op =\", \<dots>) $
 (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
-will show the term @{term "(a::nat) + b = c"}, but printed using the internal
+constructs the term @{term "(a::nat) + b = c"}, but it printed using the internal
-representation corresponding to the datatype @{ML_type  "term"} defined as follows:
+representation corresponding to the datatype @{ML_type_ind "term"} defined as follows:
 *}
 ML_val %linenosgray{*datatype term =
 Const of string * typ
 | Free of string * typ
 | Bound of int
 | Abs of string * typ * term
 | $ of term * term *}
 text {*
-This datatype implements lambda-terms typed in Church-style.
+This datatype implements Church-style lambda-terms, where types are
-As can be seen in Line 5, terms use the usual de Bruijn index mechanism
+explicitly recorded in the variables, constants and abstractions.  As can be
-for representing bound variables.  For
+seen in Line 5, terms use the usual de Bruijn index mechanism for
-example in
+representing bound variables.  For example in
 @{ML_response_fake [display, gray]
 "@{term \"\<lambda>x y. x y\"}"
 "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
 When constructing terms, you are usually concerned with free variables (as
 mentioned earlier, you cannot construct schematic variables using the
 antiquotation @{text "@{term \<dots>}"}). If you deal with theorems, you have to,
 however, observe the distinction. The reason is that only schematic
-varaibles can be instantiated with terms when a theorem is applied. A
+variables can be instantiated with terms when a theorem is applied. A
 similar distinction between free and schematic variables holds for types
 (see below).
 \begin{readmore}
 Terms and types are described in detail in \isccite{sec:terms}. Their
 raises a typing error, while it perfectly ok to construct the term
 @{ML_response_fake [display,gray]
 "let
-val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
+val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 in
 tracing (string_of_term @{context} omega)
 end"
 "x x"}
 "Const \<dots> $
 Abs (\"x\", \<dots>,
 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
 (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 There are a number of handy functions that are frequently used for
-constructing terms. One is the function @{ML_ind  list_comb}, which takes a term
+constructing terms. One is the function @{ML_ind list_comb in Term}, which
-and a list of terms as arguments, and produces as output the term
+takes a term and a list of terms as arguments, and produces as output the
-list applied to the term. For example
+term list applied to the term. For example
 @{ML_response_fake [display,gray]
 "let
 val trm = @{term \"P::nat\"}
 val args = [@{term \"True\"}, @{term \"False\"}]
 in
 list_comb (trm, args)
 end"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
-Another handy function is @{ML_ind  lambda}, which abstracts a variable
+Another handy function is @{ML_ind lambda in Term}, which abstracts a variable
 in a term. For example
 @{ML_response_fake [display,gray]
 "let
 val x_nat = @{term \"x::nat\"}
 then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted.
 This is a fundamental principle
 of Church-style typing, where variables with the same name still differ, if they
 have different type.
-There is also the function @{ML_ind  subst_free} with which terms can be
+There is also the function @{ML_ind subst_free in Term} with which terms can be
 replaced by other terms. For example below, we will replace in @{term
 "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0 x"} the subterm @{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"} by
 @{term y}, and @{term x} by @{term True}.
 @{ML_response_fake [display,gray]
 in
 subst_free [sub] trm
 end"
 "Free (\"x\", \"nat\")"}
-Similarly the function @{ML_ind  subst_bounds}, replaces lose bound
+Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound
 variables with terms. To see how this function works, let us implement a
 function that strips off the outermost quantifiers in a term.
 *}
 ML{*fun strip_alls (Const ("All", _) $ Abs (n, T, t)) =
 strip_alls t |>> cons (Free (n, T))
 | strip_alls t = ([], t) *}
 text {*
 The function returns a pair consisting of the stripped off variables and
 the body of the universal quantifications. For example
 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
 Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
 After calling @{ML strip_alls}, you obtain a term with lose bound variables. With
 the function @{ML subst_bounds}, you can replace these lose @{ML_ind
-Bound}s with the stripped off variables.
+Bound in Term}s with the stripped off variables.
 @{ML_response_fake [display, gray, linenos]
 "let
 val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
 in
 returned. The reason is that the head of the list the function @{ML subst_bounds}
 takes is the replacement for @{ML "Bound 0"}, the next element for @{ML "Bound 1"}
 and so on.
 There are many convenient functions that construct specific HOL-terms. For
-example @{ML_ind  mk_eq in HOLogic} constructs an equality out of two terms.
+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
 \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
+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
 *}
 ML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-text {* This can be equally written with the combinator @{ML_ind  "-->"} as: *}
+text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
 ML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
 text {*
 If you want to construct a function type with more than one argument
-type, then you can use @{ML_ind  "--->"}.
+type, then you can use @{ML_ind "--->" in Term}.
 *}
 ML{*fun make_fun_types tys ty = tys ---> ty *}
 text {*
 where no error is detected.
 Sometimes it is a bit inconvenient to construct a term with
 complete typing annotations, especially in cases where the typing
 information is redundant. A short-cut is to use the ``place-holder''
-type @{ML_ind  dummyT} and then let type-inference figure out the
+type @{ML_ind dummyT in Term} and then let type-inference figure out the
 complete type. An example is as follows:
 @{ML_response_fake [display,gray]
 "let
 val c = Const (@{const_name \"plus\"}, dummyT)

changeset 345	4c54ef4dc84d
parent 343	8f73e80c8c6f
child 346	0fea8b7a14a1