isabelle-cookbook: comparison ProgTutorial/General.thy

equal deleted inserted replaced

-:97518188ef0e
+:3f153aa4f231
 the unification and matching algorithms. Below we shall use the
 antiquotations @{text "@{typ_pat \<dots>}"} and @{text "@{term_pat \<dots>}"} from
 Section~\ref{sec:antiquote} in order to construct examples involving
 schematic variables.
-Let us begin with describing the unification and the matching function for
+Let us begin with describing the unification and matching function for
 types.  Both return type environments, ML-type @{ML_type "Type.tyenv"},
 which map schematic type variables to types (and sorts). Below we use the
 function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
 for unifying the types @{text "?'a * ?'b"} and @{text "?'b list *
 nat"}. This will produce the mapping, or type environment, @{text "[?'a :=
 ?'b list, ?'b := nat]"}.
 *}
-ML{*val (tyenv_unif, _) = let
+ML %linenosgray{*val (tyenv_unif, _) = let
 val ty1 = @{typ_pat "?'a * ?'b"}
 val ty2 = @{typ_pat "?'b list * nat"}
 in
 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
 end*}
 text {*
-The environment @{ML_ind "Vartab.empty"} stands for the empty type environment,
+The environment @{ML_ind "Vartab.empty"} in line 5 stands for the
-which is needed for starting the unification without any
+empty type environment, which is needed for starting the unification
-(pre)instantiations.  In case of a failure
+without any (pre)instantiations.  In case of a failure
 @{ML typ_unify in Sign} will throw the exception @{text TUNIFY}.
 We can print out the resulting type environment @{ML tyenv_unif}
 with the built-in function @{ML_ind dest in Vartab} from the structure
 @{ML_struct Vartab}.
 \end{figure}
 *}
 text {*
 The first components in this list stand for the schematic type variables and
-the second are the associated sorts and types. In what follows we will use
+the second are the associated sorts and types. In this example the sort
-the pretty-printing function in Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s.
+is the default sort @{text "HOL.type"}. We will use in what follows
-For the type environment from the example this function prints out the
+the pretty-printing function from Figure~\ref{fig:prettyenv} for
-more legible:
+@{ML_type "Type.tyenv"}s. For the type environment in the example
+this function prints out the more legible:
 @{ML_response_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'a := ?'b list, ?'b := nat]"}
-The index @{text 0} in the example above is the maximal index of the schematic
+The index @{text 0} in Line 5 in the example above is the maximal index of
-type variables occuring in @{text ty1} and @{text ty2}. It will be increased
+the schematic type variables occuring in @{text ty1} and @{text ty2}. This
-whenever a new schematic type variable is introduced during unification.
+index will be increased whenever a new schematic type variable is introduced
-This is for example the case when two schematic type variables have different,
+during unification.  This is for example the case when two schematic type
-incomparable sorts. Then a new schematic type variable is introduced with
+variables have different, incomparable sorts. Then a new schematic type
-the combined sorts. To show this let us use two sorts, @{text "s1"} and @{text "s2"},
+variable is introduced with the combined sorts. To show this let us assume two
-which we attach to the schematic type variables @{text "?'a"} and @{text "?'b"}.
+sorts, say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
+variables @{text "?'a"} and @{text "?'b"}. Since we do not make any assumption
+about the sors, they are incomparable, leading to the type environment:
 *}
 ML{*val (tyenv, index) = let
 val ty2 = @{typ_pat "?'a::s1"}
 val ty1 = @{typ_pat "?'b::s2"}
 in
 Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0)
 end*}
 text {*
-To print out the calculated type environment we also switch on the printing
+To print out this type environment we switch on the printing of sort
-of sort information.
+information.
 *}
 ML{*show_sorts := true*}
 text {*
 *}(*<*)ML %linenos{*show_sorts := false*}(*>*)
 text {*
 The way the unification function @{ML typ_unify in Sign} is implemented
 using an initial type environment and initial index makes it easy to
-unifying of more than two terms. For example
+unify more than two terms. For example
 *}
 ML{*val (tyenvs, _) = let
 val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
 val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
 in
 fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0)
 end*}
 text {*
-Let us now return again to the unifier from the first example.
+Let us now return again to the unifier from the first example in this
+section.
 @{ML_response_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'a := ?'b list, ?'b := nat]"}
 Sign} returns is in \emph{not} an instantiation in fully solved form: while @{text
 "?'b"} is instantiated to @{typ nat}, this is not propagated to the
 instantiation for @{text "?'a"}.  In unification theory, this is often
 called an instantiation in \emph{triangular form}. These not fully solved
 instantiations are used because of performance reasons.
 To apply a type environment in triangular form to a type, say @{text "?'a *
 ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
 @{ML_response_fake [display, gray]
 "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
 The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
 \end{readmore}
 The simplifier can be used to unfold definition in theorems. To show
-this we build the theorem @{term "True \<equiv> True"} (Line 1) and then
+this, we build the theorem @{term "True \<equiv> True"} (Line 1) and then
 unfold the constant @{term "True"} according to its definition (Line 2).
 @{ML_response_fake [display,gray,linenos]
 "Thm.reflexive @{cterm \"True\"}
 |> Simplifier.rewrite_rule [@{thm True_def}]

changeset 382	3f153aa4f231
parent 381	97518188ef0e
child 383	72a53b07d264