diff -r 83d5bca38bec -r 4c54ef4dc84d ProgTutorial/General.thy --- 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 \}"}}. For example @{ML_response [display,gray] @@ -24,8 +25,8 @@ "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} - 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 \"\x y. x y\"}" @@ -75,7 +76,7 @@ mentioned earlier, you cannot construct schematic variables using the antiquotation @{text "@{term \}"}). 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 \ nat\"}) $ Free (\"x\", @{typ nat}) in tracing (string_of_term @{context} omega) end" @@ -224,10 +225,11 @@ Const \ $ (Const \ $ (Free (\"P\",\) $ \)) $ (Const \ $ (Free (\"Q\",\) $ \)))"} - 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 \ nat \ nat) 0 x"} the subterm @{term "(f::nat \ nat \ 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]