isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:abdac57dfd9a
+:3857d987576a
 then there is a convenient, though again ``quick-and-dirty'', method for
 converting values into strings, namely the function @{ML makestring}:
 @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
-However @{ML makestring} only works if the type of what is converted is monomorphic
+However, @{ML makestring} only works if the type of what is converted is monomorphic
 and not a function.
 The function @{ML "warning"} should only be used for testing purposes, because any
 output this function generates will be overwritten as soon as an error is
 raised. For printing anything more serious and elaborate, the
 a separate tracing buffer. For example:
 @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
 It is also possible to redirect the ``channel'' where the string @{text "foo"} is
-printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive
+printed to a separate file, e.g., to prevent ProofGeneral from choking on massive
 amounts of trace output. This redirection can be achieved with the code:
 *}
 ML{*val strip_specials =
 let
 |> (fn x => (x, x))
 |> fst
 |> (fn x => x + 4)*}
 text {*
-which increments its argument @{text x} by 5. It does this by first incrementing
+which increments its argument @{text x} by 5. It proceeds by first incrementing
 the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
 the first component of the pair (Line 4) and finally incrementing the first
 component by 4 (Line 5). This kind of cascading manipulations of values is quite
 common when dealing with theories (for example by adding a definition, followed by
 lemmas and so on). The reverse application allows you to read what happens in
 intermediate result inside the tracing buffer. The function @{ML tap} can
 only be used for side-calculations, because any value that is computed
 cannot be merged back into the ``main waterfall''. To do this, you can use
 the next combinator.
-The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
+The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a
-and returns the result together with the value (as a pair). For example
+function to the value and returns the result together with the value (as a
-the function
+pair). For example the function
 *}
 ML{*fun inc_as_pair x =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 ML{*fun double x =
 x |>  (fn x => (x, x))
 |-> (fn x => fn y => x + y)*}
 text {*
-Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
+Recall that @{ML "|>"} is the reverse function application. Recall also that
+the related
 reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"},
 @{ML "|>>"} and @{ML "||>"} described above have related combinators for function
 composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
 for example, the function @{text double} can also be written as:
 *}
 text {*
 (FIXME: find a good exercise for combinators)
 \begin{readmore}
-The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+The most frequently used combinators are defined in the files @{ML_file
+"Pure/library.ML"}
 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
 contains further information about combinators.
 \end{readmore}
 *}
 @{ML_response_fake [display,gray]
 "get_thm_names_from_ss @{simpset}"
 "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
-Again, this way or referencing simpsets makes you independent from additions
+Again, this way of referencing simpsets makes you independent from additions
 of lemmas to the simpset by the user that potentially cause loops.
 On the ML-level of Isabelle, you often have to work with qualified names;
-these are strings with some additional information, such positional information
+these are strings with some additional information, such as positional information
 and qualifiers. Such bindings can be generated with the antiquotation
 @{text "@{binding \<dots>}"}.
 @{ML_response [display,gray]
 "@{binding \"name\"}"
 "name"}
-An example where a binding is needed is the function @{ML define in LocalTheory}.
+An example where a binding is needed is the function @{ML define in
-Below this function defines the constant @{term "TrueConj"} as the conjunction
+LocalTheory}.  Below, this function is used to define the constant @{term
+"TrueConj"} as the conjunction
 @{term "True \<and> True"}.
 *}
 local_setup %gray {*
 snd o LocalTheory.define Thm.internalK
 ((@{binding "TrueConj"}, NoSyn),
 (Attrib.empty_binding, @{term "True \<and> True"})) *}
+<<<<<<< local
 text {*
 Now querying the definition you obtain:
 \begin{isabelle}
 \isacommand{thm}~@{text "TrueConj_def"}\\
 \end{isabelle}
 (FIXME give a better example why bindings are important; maybe
 give a pointer to \isacommand{local\_setup})
-While antiquotations have many applications, they were originally introduced in order
+While antiquotations have many applications, they were originally introduced
-to avoid explicit bindings for theorems such as:
+in order to avoid explicit bindings of theorems such as:
 *}
 ML{*val allI = thm "allI" *}
 text {*
-These bindings are difficult to maintain and also can be accidentally
+Such bindings are difficult to maintain and can be overwritten by the
-overwritten by the user. This often broke Isabelle
+user accidentally. This often broke Isabelle
 packages. Antiquotations solve this problem, since they are ``linked''
 statically at compile-time.  However, this static linkage also limits their
-usefulness in cases where data needs to be build up dynamically. In the
+usefulness in cases where data needs to be built up dynamically. In the
-course of this chapter you will learn more about these antiquotations:
+course of this chapter you will learn more about antiquotations:
 they can simplify Isabelle programming since one can directly access all
-kinds of logical elements from th ML-level.
+kinds of logical elements from the ML-level.
 *}
 section {* Terms and Types *}
 text {*
-One way to construct terms of Isabelle is by using the antiquotation
+One way to construct Isabelle terms, 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>"}
-This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
+will show the term @{term "(a::nat) + b = c"}, but printed using an internal
-representation of this term. This internal representation corresponds to the
+representation corresponding to the data type @{ML_type "term"}.
-datatype @{ML_type "term"}.
+This internal representation uses the usual de Bruijn index mechanism---where
-The internal representation of terms uses the usual de Bruijn index mechanism where bound
+bound variables are represented by the constructor @{ML Bound}.  The index in
-variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
+@{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip
-the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
+until we hit the @{ML Abs} that binds the corresponding variable. Note that
-binds the corresponding variable. However, in Isabelle the names of bound variables are
+the names of bound variables are kept at abstractions for printing purposes,
-kept at abstractions for printing purposes, and so should be treated only as ``comments''.
+and so should be treated only as ``comments''.  Application in Isabelle is
-Application in Isabelle is realised with the term-constructor @{ML $}.
+realised with the term-constructor @{ML $}.
 \begin{readmore}
 Terms are described in detail in \isccite{sec:terms}. Their
 definition and many useful operations are implemented in @{ML_file "Pure/term.ML"}.
 \end{readmore}
 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 list_comb}, which takes
+constructing terms. One is the function @{ML list_comb}, which takes a term
-a term and a list of terms as arguments, and produces as output the 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]
 "list_comb (@{term \"P::nat\"}, [@{term \"True\"}, @{term \"False\"}])"
 "Free (\"P\", \"nat\") $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
 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
-in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produce the
+in unary notation (like @{term "Suc (Suc (Suc 0))"}), and produces the
 number representing their sum.
 \end{exercise}
 There are a few subtle issues with constants. They usually crop up when
 pattern matching terms or types, or when constructing them. While it is perfectly ok
 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
 @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 the name of the constant @{text "Nil"} depends on the theory in which the
-term constructor is defined (@{text "List"}) and also in which datatype
+term constructor is defined (@{text "List"}) and also in which data type
 (@{text "list"}). Even worse, some constants have a name involving
 type-classes. Consider for example the constants for @{term "zero"} and
 \mbox{@{text "(op *)"}}:
 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"op *\"})"
 Const (\"HOL.times_class.times\", \<dots>))"}
 While you could use the complete name, for example
 @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
 matching against @{text "Nil"}, this would make the code rather brittle.
-The reason is that the theory and the name of the datatype can easily change.
+The reason is that the theory and the name of the data type can easily change.
 To make the code more robust, it is better to use the antiquotation
 @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the
-variable parts of the constant's name. Therefore a functions for
+variable parts of the constant's name. Therefore a function for
 matching against constants that have a polymorphic type should
 be written as follows.
 *}
 ML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
 | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
 | is_nil_or_all _ = false *}
 text {*
-Occasional you have to calculate what the ``base'' name of a given
+Occasionally you have to calculate what the ``base'' name of a given
 constant is. For this you can use the function @{ML Sign.extern_const} or
 @{ML Long_Name.base_name}. For example:
 @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 @{typ nat} => @{typ int}
 | Type (s, ts) => Type (s, map nat_to_int ts)
 | _ => t)*}
 text {*
-An example as follows:
+Here is an example:
 @{ML_response_fake [display,gray]
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
 \begin{exercise}
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
 result that type-checks.
 \end{exercise}
-Remember Isabelle follows the Church-style typing for terms, i.e.~a term contains
+Remember Isabelle follows the Church-style typing for terms, i.e., a term contains
 enough typing information (constants, free variables and abstractions all have typing
 information) so that it is always clear what the type of a term is.
 Given a well-typed term, the function @{ML type_of} returns the
 type of a term. Consider for example:
 end"
 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
 Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 Instead of giving explicitly the type for the constant @{text "plus"} and the free
-variable @{text "x"}, the type-inference fills in the missing information.
+variable @{text "x"}, type-inference fills in the missing information.
 \begin{readmore}
 See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
-checking and pretty-printing of terms are defined. Functions related to the
+checking and pretty-printing of terms are defined. Functions related to
-type inference are implemented in @{ML_file "Pure/type.ML"} and
+type-inference are implemented in @{ML_file "Pure/type.ML"} and
 @{ML_file "Pure/type_infer.ML"}.
 \end{readmore}
 (FIXME: say something about sorts)
 *}
 section {* Theorems *}
 text {*
 Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
-that can only be build by going through interfaces. As a consequence, every proof
+that can only be built by going through interfaces. As a consequence, every proof
 in Isabelle is correct by construction. This follows the tradition of the LCF approach
 \cite{GordonMilnerWadsworth79}.
 To see theorems in ``action'', let us give a proof on the ML-level for the following
 "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
 annotated to theorems, but functions that do further processing once a
 theorem is proved. In particular, it is not possible to find out
 what are all theorems that have a given attribute in common, unless of course
 the function behind the attribute stores the theorems in a retrievable
-datastructure.
+data structure.
 If you want to print out all currently known attributes a theorem can have,
 you can use the Isabelle command
 \begin{isabelle}
 section {* Setups (TBD) *}
 text {*
 In the previous section we used \isacommand{setup} in order to make
 a theorem attribute known to Isabelle. What happens behind the scenes
-is that \isacommand{setup} expects a functions of type
+is that \isacommand{setup} expects a function of type
 @{ML_type "theory -> theory"}: the input theory is the current theory and the
 output the theory where the theory attribute has been stored.
 This is a fundamental principle in Isabelle. A similar situation occurs
 for example with declaring constants. The function that declares a
 There are theories, proof contexts and local theories (in this order, if you
 want to order them).
 In contrast to an ordinary theory, which simply consists of a type
 signature, as well as tables for constants, axioms and theorems, a local
-theory also contains additional context information, such as locally fixed
+theory contains additional context information, such as locally fixed
 variables and local assumptions that may be used by the package. The type
 @{ML_type local_theory} is identical to the type of \emph{proof contexts}
 @{ML_type "Proof.context"}, although not every proof context constitutes a
 valid local theory.
 *}

changeset 204	3857d987576a
parent 194	8cd51a25a7ca
parent 202	16ec70218d26
child 207	d3cd633e8240