diff -r 9e374cd891e1 -r 364fffa80794 ProgTutorial/General.thy --- a/ProgTutorial/General.thy Wed Oct 14 14:56:19 2009 +0200 +++ b/ProgTutorial/General.thy Sun Oct 18 08:44:39 2009 +0200 @@ -17,16 +17,16 @@ 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. + structures involved in this core are certified terms and certified types, + as well as theorems. *} section {* Terms and Types *} text {* - There are certified terms and uncertified terms (respectively types). - Uncertified terms are just called terms. One way to construct them is by + In Isabelle, there are certified terms and uncertified terms (respectively types). + Uncertified terms are often just called terms. One way to construct them is by using the antiquotation \mbox{@{text "@{term \}"}}. For example @{ML_response [display,gray] @@ -34,8 +34,9 @@ "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} - 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: + constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using + the internal representation corresponding to the datatype @{ML_type_ind "term"}, + which is defined as follows: *} ML_val %linenosgray{*datatype term = @@ -48,7 +49,7 @@ text {* This datatype implements Church-style lambda-terms, where types are - explicitly recorded in the variables, constants and abstractions. As can be + explicitly recorded in 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 @@ -153,7 +154,7 @@ where it is not (since it is already constructed by a meta-implication). The purpose of the @{text "Trueprop"}-coercion is to embed formulae of - an object logic, for example HOL, into the meta-logic of Isabelle. It + an object logic, for example HOL, into the meta-logic of Isabelle. The coercion is needed whenever a term is constructed that will be proved as a theorem. As already seen above, types can be constructed using the antiquotation @@ -171,7 +172,7 @@ text {* Like with terms, there is the distinction between free type - variables (term-constructor @{ML "TFree"} and schematic + variables (term-constructor @{ML "TFree"}) and schematic type variables (term-constructor @{ML "TVar"}). A type constant, like @{typ "int"} or @{typ bool}, are types with an empty list of argument types. However, it is a bit difficult to show an @@ -236,7 +237,7 @@ 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 + takes as argument a term and a list of terms, and produces as output the term list applied to the term. For example @@ -262,7 +263,7 @@ "Abs (\"x\", \"nat\", Free (\"P\", \"bool \ bool\") $ Bound 0)"} In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), - and an abstraction. It also records the type of the abstracted + and an abstraction, where it also records the type of the abstracted variable and for printing purposes also its name. Note that because of the typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} is of the same type as the abstracted variable. If it is of different type, @@ -320,7 +321,7 @@ text {* The function returns a pair consisting of the stripped off variables and - the body of the universal quantifications. For example + the body of the universal quantification. For example @{ML_response_fake [display, gray] "strip_alls @{term \"\x y. x = (y::bool)\"}" @@ -346,7 +347,8 @@ 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 + 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 @@ -545,14 +547,13 @@ \end{exercise} \begin{exercise}\label{fun:makesum} - Write a function which takes two terms representing natural numbers + Write a function that takes two terms representing natural numbers in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the number representing their sum. \end{exercise} \begin{exercise}\label{ex:debruijn} - Implement the function, which we below name deBruijn\footnote{According to - personal communication of de Bruijn to Dyckhoff.}, that depends on a natural + Implement the function, which we below name deBruijn, that depends on a natural number n$>$0 and constructs terms of the form: \begin{center} @@ -575,7 +576,8 @@ \end{center} Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"} - for constructing the terms for the logical connectives. + for constructing the terms for the logical connectives.\footnote{Thanks to Roy + Dyckhoff for this exercise.} \end{exercise} *} @@ -1382,7 +1384,7 @@ the current simpset. *} -section {* Theories (TBD) *} +section {* Theories\label{sec:theories} (TBD) *} text {* There are theories, proof contexts and local theories (in this order, if you