# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237829758 -3600
# Node ID 3857d987576a63bab32ccd67037e7a86cbf36395
# Parent  abdac57dfd9a48468da29110ea96f118269aab0b# Parent  16ec70218d26d6dea5aa1cc94e17a2ff342cf014
merged

diff -r abdac57dfd9a -r 3857d987576a ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Mon Mar 23 18:28:41 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Mon Mar 23 18:35:58 2009 +0100
@@ -89,7 +89,7 @@
 
   @{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
@@ -101,7 +101,7 @@
   @{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:
 *}
 
@@ -260,7 +260,7 @@
     |> (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
@@ -361,9 +361,9 @@
   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
-  and returns the result together with the value (as a pair). For example
-  the function 
+  The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a
+  function to the value and returns the result together with the value (as a
+  pair). For example the function 
 *}
 
 ML{*fun inc_as_pair x =
@@ -405,7 +405,8 @@
         |-> (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 "#->"}, 
@@ -421,7 +422,8 @@
   (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}
@@ -495,11 +497,11 @@
   "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>}"}.
 
@@ -507,8 +509,9 @@
   "@{binding \"name\"}"
   "name"}
 
-  An example where a binding is needed is the function @{ML define in LocalTheory}.
-  Below this function defines the constant @{term "TrueConj"} as the conjunction
+  An example where a binding is needed is the function @{ML define in
+  LocalTheory}.  Below, this function is used to define the constant @{term
+  "TrueConj"} as the conjunction
   @{term "True \<and> True"}.
 *}
   
@@ -517,6 +520,7 @@
     ((@{binding "TrueConj"}, NoSyn), 
      (Attrib.empty_binding, @{term "True \<and> True"})) *}
 
+<<<<<<< local
 text {* 
   Now querying the definition you obtain:
 
@@ -528,27 +532,27 @@
   (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 
-  to avoid explicit bindings for theorems such as:
+  While antiquotations have many applications, they were originally introduced
+  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
-  overwritten by the user. This often broke Isabelle
+  Such bindings are difficult to maintain and can be overwritten by the
+  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
-  course of this chapter you will learn more about these antiquotations:
+  usefulness in cases where data needs to be built up dynamically. In the
+  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] 
@@ -556,16 +560,16 @@
 "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
-  representation of this term. This internal representation corresponds to the 
-  datatype @{ML_type "term"}.
+  will show the term @{term "(a::nat) + b = c"}, but printed using an internal
+  representation corresponding to the data type @{ML_type "term"}.
   
-  The internal representation of terms uses the usual de Bruijn index mechanism where bound 
-  variables are represented by the constructor @{ML Bound}. The index in @{ML Bound} refers to
-  the number of Abstractions (@{ML Abs}) we have to skip until we hit the @{ML Abs} that
-  binds the corresponding variable. However, in Isabelle the names of bound variables are 
-  kept at abstractions for printing purposes, and so should be treated only as ``comments''. 
-  Application in Isabelle is realised with the term-constructor @{ML $}.
+  This internal representation uses the usual de Bruijn index mechanism---where
+  bound variables are represented by the constructor @{ML Bound}.  The index in
+  @{ML Bound} refers to the number of Abstractions (@{ML Abs}) we have to skip
+  until we hit the @{ML Abs} that binds the corresponding variable. Note that
+  the names of bound variables are kept at abstractions for printing purposes,
+  and so should be treated only as ``comments''.  Application in Isabelle is
+  realised with the term-constructor @{ML $}.
 
   \begin{readmore}
   Terms are described in detail in \isccite{sec:terms}. Their
@@ -679,8 +683,8 @@
                 (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 
-  a term and a list of terms as arguments, and produces as output the term
+  constructing terms. One is the function @{ML 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
 
 @{ML_response_fake [display,gray]
@@ -746,7 +750,7 @@
 
   \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}
 
@@ -808,7 +812,7 @@
   @{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 *)"}}:
@@ -820,10 +824,10 @@
   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.
 *}
@@ -833,7 +837,7 @@
   | 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:
 
@@ -874,7 +878,7 @@
    | _ => t)*}
 
 text {*
-  An example as follows:
+  Here is an example:
 
 @{ML_response_fake [display,gray] 
 "map_types nat_to_int @{term \"a = (1::nat)\"}" 
@@ -943,7 +947,7 @@
   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 
@@ -993,12 +997,12 @@
   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
-  type inference are implemented in @{ML_file "Pure/type.ML"} and 
+  checking and pretty-printing of terms are defined. Functions related to
+  type-inference are implemented in @{ML_file "Pure/type.ML"} and 
   @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
 
@@ -1010,7 +1014,7 @@
 
 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}.
 
@@ -1081,7 +1085,7 @@
   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
@@ -1439,7 +1443,7 @@
 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.
   
@@ -1495,7 +1499,7 @@
 
   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
@@ -1549,4 +1553,4 @@
 
 ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
 
-end
\ No newline at end of file
+end
diff -r abdac57dfd9a -r 3857d987576a progtutorial.pdf