isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:84aef87b348a
+:ffa5c4ec9611
 end"
 "?x3, ?x1.3, x"}
 When constructing terms, you are usually concerned with free
 variables (as mentioned earlier, you cannot construct schematic
-variables using the built in antiquotation \mbox{@{text "@{term
+variables using the built-in antiquotation \mbox{@{text "@{term
 \<dots>}"}}). If you deal with theorems, you have to, however, observe the
 distinction. The reason is that only schematic variables can be
 instantiated with terms when a theorem is applied. A similar
 distinction between free and schematic variables holds for types
 (see below).
 @{ML_response_fake_both [display,gray]
 "@{term \"x x\"}"
 "Type unification failed: Occurs check!"}
-raises a typing error, while it perfectly ok to construct the term
+raises a typing error, while it is perfectly ok to construct the term
 with the raw ML-constructors:
 @{ML_response_fake [display,gray]
 "let
 val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
 we can see the full name of the type is actually @{text "List.list"}, indicating
 that it is defined in the theory @{text "List"}. However, one has to be
 careful with names of types, because even if
 @{text "fun"} is defined in the theory @{text "HOL"}, it is
-still represented by their simple name.
+still represented by its simple name.
 @{ML_response [display,gray]
 "@{typ \"bool \<Rightarrow> nat\"}"
 "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
 in
 lambda x_nat trm
 end"
 "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
-In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}),
+In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML "Bound 0"}),
 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
 text {*
 The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
 environment, which is needed for starting the unification without any
 (pre)instantiations. The @{text 0} is an integer index that will be explained
-below. In case of failure, @{ML typ_unify in Sign} will throw the exception
+below. In case of failure, @{ML typ_unify in Sign} will raise the exception
 @{text TUNIFY}.  We can print out the resulting type environment bound to
 @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
 structure @{ML_struct Vartab}.
 @{ML_response_fake [display,gray]
 unified have already the same type. In case of failure, the exceptions that
 are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
 As mentioned before, unrestricted higher-order unification, respectively
 unrestricted higher-order matching, is in general undecidable and might also
-not posses a single most general solution. Therefore Isabelle implements the
+not possess a single most general solution. Therefore Isabelle implements the
 unification function @{ML_ind unifiers in Unify} so that it returns a lazy
 list of potentially infinite unifiers.  An example is as follows
 *}
 ML %grayML{*val uni_seq =
 Unify}, this function does not raise an exception in case of failure, but
 returns an empty sequence. It also first tries out whether the matching
 problem can be solved by first-order matching.
 Higher-order matching might be necessary for instantiating a theorem
-appropriately. More on this will be given in Sections~\ref{sec:theorems}.
+appropriately. More on this will be given in Section~\ref{sec:theorems}.
 Here we only have a look at a simple case, namely the theorem
 @{thm [source] spec}:
 \begin{isabelle}
 \isacommand{thm}~@{thm [source] spec}\\
 \end{isabelle}
 as an introduction rule. Applying it directly can lead to unexpected
 behaviour since the unification has more than one solution. One way round
 this problem is to instantiate the schematic variables @{text "?P"} and
-@{text "?x"}.  instantiation function for theorems is
+@{text "?x"}.  Instantiation function for theorems is
 @{ML_ind instantiate_normalize in Drule} from the structure
 @{ML_struct Drule}. One problem, however, is
 that this function expects the instantiations as lists of @{ML_type ctyp}
 and @{ML_type cterm} pairs:
 and may use so-called type class parameters. These are type-indexed constants
 dependent on the sole type variable and are implemented via overloading.
 Overloading a constant means specifying its value on a type based on
 a well-founded reduction towards other values of constants on types.
 When instantiating type classes
-(i.e. proving arities) you are specifying overloading via primitive recursion.
+(i.e.\ proving arities) you are specifying overloading via primitive recursion.
 Sorts are finite intersections of type classes and are implemented as lists
-of type class names. The empty intersection, i.e. the empty list, is therefore
+of type class names. The empty intersection, i.e.\ the empty list, is therefore
 inhabited by all types and is called the topsort.
 Free and schematic type variables are always annotated with sorts, thereby restricting
 the domain of types they quantify over and corresponding to an implicit hypothesis
 about the type variable.
 section {* Type-Checking\label{sec:typechecking} *}
 text {*
-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_ind type_of in Term} returns the
 type of a term. Consider for example:

changeset 559	ffa5c4ec9611
parent 557	77ea2de0ca62
child 562	daf404920ab9