isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:84aef87b348a
+:ffa5c4ec9611
 for converting values into strings, namely the antiquotation
 @{text "@{make_string}"}:
 @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""}
-However, @{text "@{makes_tring}"} only works if the type of what
+However, @{text "@{make_string}"} only works if the type of what
 is converted is monomorphic and not a function.
 You can print out error messages with the function @{ML_ind error in Library};
 for example:
 This function raises the exception @{text ERROR}, which will then
 be displayed by the infrastructure indicating that it is an error by
 painting the output red. Note that this exception is meant
 for ``user-level'' error messages seen by the ``end-user''.
-For messages where you want to indicate a genuine program error, then
+For messages where you want to indicate a genuine program error
 use the exception @{text Fail}.
-Most often you want to inspect data of Isabelle's basic data structures,
+Most often you want to inspect contents of Isabelle's basic data structures,
 namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
-and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions,
+and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,
 which we will explain in more detail in Section \ref{sec:pretty}. For now
 we just use the functions @{ML_ind writeln in Pretty}  from the structure
 @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
 @{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
 *}
 ML %grayML{*val pretty_term = Syntax.pretty_term
 val pwriteln = Pretty.writeln*}
 text {*
-They can now be used as follows
+They can be used as follows
 @{ML_response_fake [display,gray]
 "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 ML %grayML{*fun pretty_terms ctxt trms =
 Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
 text {*
-You can also print out terms together with their typing information.
+To print out terms together with their typing information,
-For this you need to set the configuration value
+set the configuration value
 @{ML_ind show_types in Syntax} to @{ML true}.
 *}
 ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*}
 @{ML_response_fake [display, gray]
 "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
 "(1::nat, x::'a)"}
-where @{text 1} and @{text x} are displayed with their inferred type.
+where @{text 1} and @{text x} are displayed with their inferred types.
 Other configuration values that influence
 printing of terms include
 \begin{itemize}
 \item @{ML_ind show_brackets in Syntax}
 ML %grayML{*fun pretty_thm ctxt thm =
 pretty_term ctxt (prop_of thm)*}
 text {*
 Theorems include schematic variables, such as @{text "?P"},
-@{text "?Q"} and so on. They are needed in Isabelle in order to able to
+@{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied.
-instantiate theorems when they are applied. For example the theorem
+For example, the theorem
 @{thm [source] conjI} shown below can be used for any (typable)
 instantiation of @{text "?P"} and @{text "?Q"}.
 @{ML_response_fake [display, gray]
 "pwriteln (pretty_thm @{context} @{thm conjI})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
-However, in order to improve the readability when printing theorems, we
+However, to improve the readability when printing theorems, we
 can switch off the question marks as follows:
 *}
 ML %grayML{*fun pretty_thm_no_vars ctxt thm =
 let
 val y3 = fst y2
 val y4 = y3 + 4
 in y4 end*}
 text {*
-Another reason why the let-bindings in the code above are better to be
+Another reasons to avoid the let-bindings in the code above:
-avoided: it is more than easy to get the intermediate values wrong, not to
+it is easy to get the intermediate values wrong and
-mention the nightmares the maintenance of this code causes!
+the resulting code is difficult to maintain.
 In Isabelle a ``real world'' example for a function written in
 the waterfall fashion might be the following code:
 *}
 |> Variable.variant_frees ctxt [f]
 |> map Free
 |> curry list_comb f *}
 text {*
-This function takes a term and a context as argument. If the term is of function
+This function takes a term and a context as arguments. If the term is of function
 type, then @{ML "apply_fresh_args"} returns the term with distinct variables
-applied to it. For example below three variables are applied to the term
+applied to it. For example, below three variables are applied to the term
 @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 @{ML_response_fake [display,gray]
 "let
 val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
 end *}
 text {*
 The function @{ML_text "my_note"} in line 3 is just a wrapper for the function
 @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory};
-its purpose is to store a theorem under a name.
+it stores a theorem under a name.
 In lines 5 to 6 we call this function to give alternative names for the three
 theorems. The point of @{ML "#>"} is that you can sequence such function calls.
 The remaining combinators we describe in this section add convenience for
 the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
 some data structure and return it. Instead, it is literally
 replaced with the value representing the theory.
 Another important antiquotation is @{text "@{context}"}. (What the
 difference between a theory and a context is will be described in Chapter
-\ref{chp:advanced}.) A context is for example needed in order to use the
+\ref{chp:advanced}.) A context is for example needed to use the
 function @{ML print_abbrevs in Proof_Context} that list of all currently
 defined abbreviations. For example
 @{ML_response_fake [display, gray]
 "Proof_Context.print_abbrevs @{context}"
 of lemmas to the simpset by the user, which can potentially cause loops in your
 code.
 It is also possible to define your own antiquotations. But you should
 exercise care when introducing new ones, as they can also make your code
-also difficult to read. In the next chapter we describe how to construct
+difficult to read. In the next chapter we describe how to construct
-terms with the (build in) antiquotation @{text "@{term \<dots>}"}.  A restriction
+terms with the (built-in) antiquotation @{text "@{term \<dots>}"}.  A restriction
 of this antiquotation is that it does not allow you to use schematic
 variables in terms. If you want to have an antiquotation that does not have
 this restriction, you can implement your own using the function @{ML_ind
 inline in ML_Antiquotation} from the structure @{ML_struct ML_Antiquotation}. The code
 for the antiquotation @{text "term_pat"} is as follows.
 *}
 setup %gray {* type_pat_setup *}
 text {*
-However, a word of warning is in order: Introducing new antiquotations should be done only after
+However, a word of warning is in order: new antiquotations should be introduced only after
-careful deliberations. They can potentially make your code harder to read, than making it easier.
+careful deliberations. They can potentially make your code harder, rather than easier, to read.
 \begin{readmore}
 The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
 contain the infrastructure and definitions for most antiquotations. Most of the basic operations
 on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
 in a theory (simpsets need to be maintained across proofs and even across
 theories).  On the other hand, data such as facts change inside a proof and
 are only relevant to the proof at hand. Therefore such data needs to be
 maintained inside a proof context, which represents ``local'' data.
 You can think of a theory as the ``longterm memory'' of Isabelle (nothing will
-be deleted from it), and a proof-context as a ``shortterm memory'' (it dynamically
+be deleted from it), and a proof-context as a ``shortterm memory'' (it
 changes according to what is needed at the time).
 For theories and proof contexts there are, respectively, the functors
 @{ML_funct_ind Theory_Data} and @{ML_funct_ind Proof_Data} that help
 with the data storage. Below we show how to implement a table in which you
 tables should be merged (Line 5). These functions correspond roughly to the
 operations performed on theories and we just give some sensible
 defaults.\footnote{\bf FIXME: Say more about the
 assumptions of these operations.} The result structure @{ML_text Data}
 contains functions for accessing the table (@{ML Data.get}) and for updating
-it (@{ML Data.map}). There is also the functions @{ML Data.put}, which however is
+it (@{ML Data.map}). There is also the function @{ML Data.put}, but it is
 not relevant here. Below we define two
 auxiliary functions, which help us with accessing the table.
 *}
 ML %grayML{*val lookup = Symtab.lookup o Data.get
 *}
 text {*
 The use of the command \isacommand{setup} makes sure the table in the
 \emph{current} theory is updated (this is explained further in
-section~\ref{sec:theories}). The lookup can now be performed as follows.
+Section~\ref{sec:theories}). The lookup can now be performed as follows.
 @{ML_response_fake [display, gray]
 "lookup @{theory} \"conj\""
 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}

changeset 559	ffa5c4ec9611
parent 557	77ea2de0ca62
child 562	daf404920ab9