isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:9e374cd891e1
+:364fffa80794
 text {*
 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
+structures involved in this core are certified terms and certified types,
-theorems.
+as well as theorems.
 *}
 section {* Terms and Types *}
 text {*
-There are certified terms and uncertified terms (respectively types).
+In Isabelle, there are certified terms and uncertified terms (respectively types).
-Uncertified terms are just called terms. One way to construct them is by
+Uncertified terms are often 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>"}
-constructs the term @{term "(a::nat) + b = c"}, but it printed using the internal
+constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
-representation corresponding to the datatype @{ML_type_ind "term"} defined as follows:
+the internal representation corresponding to the datatype @{ML_type_ind "term"},
+which is defined as follows:
 *}
 ML_val %linenosgray{*datatype term =
 Const of string * typ
 | Free of string * typ
 | Abs of string * typ * term
 | $ of term * term *}
 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
 @{ML_response_fake [display, gray]
 "@{term \"\<lambda>x y. x y\"}"
 "(Const (\"==>\", \<dots>) $ \<dots> $ \<dots>,
 Const (\"==>\", \<dots>) $ \<dots> $ \<dots>)"}
 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
 @{text "@{typ \<dots>}"}. For example:
 | TFree of string * sort
 | TVar  of indexname * sort *}
 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
 example, because Isabelle always pretty-prints types (unlike terms).
 Here is a contrived example:
 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 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
 @{ML_response_fake [display,gray]
 "let
 lambda x_nat trm
 end"
 "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> 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,
 as in
 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
+the body of the universal quantification. For example
 @{ML_response_fake [display, gray]
 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
 "([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
 Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
 Note that in Line 4 we had to reverse the list of variables that @{ML strip_alls}
 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
+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
 @{ML_response_fake [gray,display]
 the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}
 associates to the left. Try your function on some examples.
 \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
+Implement the function, which we below name deBruijn, that depends on a natural
-personal communication of de Bruijn to Dyckhoff.}, that depends on a natural
 number n$>$0 and constructs terms of the form:
 \begin{center}
 \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
 {\it rhs n} & $\dn$ & {\large$\bigwedge$}{\it i=1\ldots n.  P\,i}\\
 (P 3 = P 1 $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3) $\longrightarrow$ P 1 $\wedge$ P 2 $\wedge$ P 3
 \end{tabular}
 \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}
 *}
 section {* Type-Checking\label{sec:typechecking} *}
 use the commands \isacommand{method\_setup} for installing methods in the
 current theory and \isacommand{simproc\_setup} for adding new simprocs to
 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
 want to order them).

changeset 350	364fffa80794
parent 349	9e374cd891e1
child 351	f118240ab44a