--- a/ProgTutorial/General.thy Sun Oct 11 23:16:34 2009 +0200
+++ b/ProgTutorial/General.thy Mon Oct 12 17:07:17 2009 +0200
@@ -5,18 +5,19 @@
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
- theorem proving where there is a small trusted core and everything else is
- build on top of this trusted core. The central data structures involved
- in this core are certified terms and types as well as theorems.
+ 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 build on top of this trusted core. The fundamental data
+ 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
- terms. The latter are called just terms. One way to construct them is by
+ There are certified terms and uncertified terms (respectively types).
+ 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]
@@ -24,8 +25,8 @@
"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
- representation corresponding to the datatype @{ML_type "term"} defined as follows:
+ constructs the term @{term "(a::nat) + b = c"}, but it printed using the internal
+ representation corresponding to the datatype @{ML_type_ind "term"} defined as follows:
*}
ML_val %linenosgray{*datatype term =
@@ -37,10 +38,10 @@
| $ of term * term *}
text {*
- This datatype implements lambda-terms typed in Church-style.
- As can be seen in Line 5, terms use the usual de Bruijn index mechanism
- for representing bound variables. For
- example in
+ This datatype implements Church-style lambda-terms, where types are
+ explicitly recorded in the variables, constants and abstractions. As can be
+ seen in Line 5, terms use the usual de Bruijn index mechanism for
+ representing bound variables. For example in
@{ML_response_fake [display, gray]
"@{term \"\<lambda>x y. x y\"}"
@@ -75,7 +76,7 @@
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).
@@ -97,7 +98,7 @@
@{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"
@@ -224,10 +225,11 @@
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
- and a list of terms as arguments, and produces as output the term
- list applied to the term. For example
+ There are a number of handy functions that are frequently used for
+ constructing terms. One is the function @{ML_ind list_comb in Term}, which
+ takes a term and a list of terms as arguments, and produces as output the
+ term list applied to the term. For example
+
@{ML_response_fake [display,gray]
"let
@@ -238,7 +240,7 @@
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]
@@ -271,7 +273,7 @@
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}.
@@ -298,13 +300,13 @@
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 |>> cons (Free (n, T))
| strip_alls t = ([], t) *}
text {*
@@ -318,7 +320,7 @@
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
@@ -336,7 +338,7 @@
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
@@ -451,7 +453,7 @@
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\""}
@@ -474,13 +476,13 @@
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 *}
@@ -607,7 +609,7 @@
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]