isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:9e374cd891e1
+:364fffa80794
 ``We will most likely never realize the full importance of painting the Tower,\\
 that it is the essential element in the conservation of metal works and the\\
 more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
 Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been
 re-painted 18 times since its initial construction, an average of once every
-seven years. It takes more than a year for a team of 25 painters to paint the tower
+seven years. It takes more than one year for a team of 25 painters to paint the tower
 from top to bottom.}
 \end{flushright}
 \medskip
 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
 structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
 thm}. Isabelle contains elaborate pretty-printing functions for printing
 them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
 are a bit unwieldy. One way to transform a term into a string is to use the
 function @{ML_ind  string_of_term in Syntax} in the structure @{ML_struct
-Syntax}, which we bind for more convenience to the toplevel.
+Syntax}. For more convenience, we bind this function to the toplevel.
 *}
 ML{*val string_of_term = Syntax.string_of_term*}
 text {*
 @{ML_response_fake [display,gray]
 "string_of_term @{context} @{term \"1::nat\"}"
 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
-This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
+We obtain a string corrsponding to the term @{term [show_types] "1::nat"} with some
 additional information encoded in it. The string can be properly printed by
 using either the function @{ML_ind  writeln} or @{ML_ind  tracing}:
 @{ML_response_fake [display,gray]
 "writeln (string_of_term @{context} @{term \"1::nat\"})"
 ML{*fun string_of_thm ctxt thm =
 string_of_term ctxt (prop_of thm)*}
 text {*
-Theorems also include schematic variables, such as @{text "?P"},
+Theorems include schematic variables, such as @{text "?P"},
 @{text "?Q"} and so on. They are needed in Isabelle in order to able to
 instantiate theorems when they are applied. For example the theorem
 @{thm [source] conjI} shown below can be used for any (typable)
 instantiation of @{text "?P"} and @{text "?Q"}.
 fun string_of_thms_no_vars ctxt thms =
 commas (map (string_of_thm_no_vars ctxt) thms) *}
 text {*
-Note, that when printing out several parcels of information that
+Note that when printing out several ``parcels'' of information that
-semantically belong together, like a warning message consisting for example
+semantically belong together, like a warning message consisting of
-of a term and a type, you should try to keep this information together in a
+a term and its type, you should try to keep this information together in a
 single string. Therefore do \emph{not} print out information as
 @{ML_response_fake [display,gray]
 "tracing \"First half,\";
 tracing \"and second half.\""
 "cat_lines [\"foo\", \"bar\"]"
 "\"foo\\nbar\""}
 Section \ref{sec:pretty} will also explain the infrastructure of Isabelle
 that helps with more elaborate pretty printing.
+\begin{readmore}
+Most of the basic string functions of Isabelle are defined in
+@{ML_file "Pure/library.ML"}.
+\end{readmore}
 *}
 section {* Combinators\label{sec:combinators} *}
 *}
 ML{*fun K x = fn _ => x*}
 text {*
-@{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
+@{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a
-function ignores its argument. As a result, @{ML K} defines a constant function
+result, @{ML K} defines a constant function always returning @{text x}.
-always returning @{text x}.
 The next combinator is reverse application, @{ML_ind  "|>" in Basics}, defined as:
 *}
 ML{*fun x |> f = f x*}
 |> (fn x => (x, x))
 |> fst
 |> (fn x => x + 4)*}
 text {*
-which increments its argument @{text x} by 5. It proceeds by first incrementing
+which increments its argument @{text x} by 5. It does this 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
 text {*
 Another reason why the let-bindings in the code above are better to be
 avoided: it is more than easy to get the intermediate values wrong, not to
 mention the nightmares the maintenance of this code causes!
-In Isabelle, a ``real world'' example for a function written in
+In Isabelle a ``real world'' example for a function written in
 the waterfall fashion might be the following code:
 *}
 ML %linenosgray{*fun apply_fresh_args f ctxt =
 f |> fastype_of
 text {*
 which is the function composed of first the increment-by-one function and then
 increment-by-two, followed by increment-by-three. Again, the reverse function
 composition allows you to read the code top-down.
-The remaining combinators described in this section add convenience for the
+The remaining combinators we describe in this section add convenience for the
 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in
 Basics} allows you to get hold of an intermediate result (to do some
 side-calculations for instance). The function
 *}
 |> (fn x => x + 2)*}
 text {*
 increments the argument first by @{text "1"} and then by @{text "2"}. In the
 middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
-intermediate result inside the tracing buffer. The function @{ML tap} can
+intermediate result. The function @{ML tap} can only be used for
-only be used for side-calculations, because any value that is computed
+side-calculations, because any value that is computed cannot be merged back
-cannot be merged back into the ``main waterfall''. To do this, you can use
+into the ``main waterfall''. To do this, you can use the next combinator.
-the next combinator.
 The combinator @{ML_ind "`" in Basics} (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
+value (as a pair). It is defined as
+*}
+ML{*fun `f = fn x => (f x, x)*}
+text {*
+An example for this combinator is the function
 *}
 ML{*fun inc_as_pair x =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 text {*
-takes @{text x} as argument, and then increments @{text x}, but also keeps
+which takes @{text x} as argument, and then increments @{text x}, but also keeps
 @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
 for x}. After that, the function increments the right-hand component of the
 pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
 The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
 in
 if i <= x then (los, x::grs) else (x::los, grs)
 end*}
 text {*
-where however the return value of the recursive call is bound explicitly to
+where the return value of the recursive call is bound explicitly to
 the pair @{ML "(los, grs)" for los grs}. You can implement this function
 more concisely as
 *}
 ML{*fun separate i [] = ([], [])
 text {*
 When using combinators for writing functions in waterfall fashion, it is
 sometimes necessary to do some ``plumbing'' in order to fit functions
 together. We have already seen such plumbing in the function @{ML
 apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
-list_comb} that works over pairs to fit with the combinator @{ML "|>"}. Such
+list_comb}, which works over pairs to fit with the combinator @{ML "|>"}. Such
 plumbing is also needed in situations where a function operate over lists,
 but one calculates only with a single element. An example is the function
-@{ML_ind check_terms in Syntax}, whose purpose is to type-check a list
+@{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
-of terms. Consider the code:
+a list of terms. Consider the code:
 @{ML_response_fake [display, gray]
 "let
 val ctxt = @{context}
 in
 text parts of Isabelle and their purpose is to print logical entities inside
 \LaTeX-documents. Document antiquotations are part of the user level and
 therefore we are not interested in them in this Tutorial, except in Appendix
 \ref{rec:docantiquotations} where we show how to implement your own document
 antiquotations.}  For example, one can print out the name of the current
-theory by typing
+theory with the code
 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
 where @{text "@{theory}"} is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 @{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 of referencing simpsets makes you independent from additions
-of lemmas to the simpset by the user that can potentially cause loops in your
+of lemmas to the simpset by the user, which can potentially cause loops in your
 code.
 On the ML-level of Isabelle, you often have to work with qualified names.
 These are strings with some additional information, such as positional
 information and qualifiers. Such qualified names can be generated with the
 \footnote{\bf FIXME: There should probably a separate section on binding, long-names
 and sign.}
 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 will see how the (build in)
+also difficult to read. In the next chapter we describe how the (build in)
-antiquotation @{text "@{term \<dots>}"} can be used to construct terms.  A
+antiquotation @{text "@{term \<dots>}"} for constructing terms.  A
 restriction of this antiquotation is that it does not allow you to use
-schematic variables. If you want to have an antiquotation that does not have
+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_Antiquote}. The code for the antiquotation @{text "term_pat"} is
+inline in ML_Antiquote} in the structure @{ML_struct ML_Antiquote}. The code
-as follows.
+for the antiquotation @{text "term_pat"} is as follows.
 *}
 ML %linenosgray{*let
 val parser = Args.context -- Scan.lift Args.name_source
 text {*
 The parser in Line 2 provides us with a context and a string; this string is
 transformed into a term using the function @{ML_ind read_term_pattern in
 ProofContext} (Line 5); the next two lines transform the term into a string
-so that the ML-system can understand it. An example for the usage
+so that the ML-system can understand it. An example for this antiquotation is:
-of this antiquotation is:
 @{ML_response_fake [display,gray]
 "@{term_pat \"Suc (?x::nat)\"}"
 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 which shows the internal representation of the term @{text "Suc ?x"}.
-This is different from the build-in @{text "@{term \<dots>}"}-antiquotation.
-@{ML_response_fake [display,gray]
-"@{term \"Suc (x::nat)\"}"
-"Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Free (\"x\", \"nat\")"}
 \begin{readmore}
 The file @{ML_file "Pure/ML/ml_antiquote.ML"} contains the the definitions
 for most antiquotations. Most of the basic operations on ML-syntax are implemented
 in @{ML_file "Pure/ML/ml_syntax.ML"}.
 section {* Storing Data in Isabelle\label{sec:storing} *}
 text {*
 Isabelle provides mechanisms for storing (and retrieving) arbitrary
 data. Before we delve into the details, let us digress a bit. Conventional
-wisdom has it that the type-system of ML ensures that for example an
+wisdom has it that the type-system of ML ensures that  an
-@{ML_type "'a list"} can only hold elements of the same type, namely
+@{ML_type "'a list"}, say, can only hold elements of the same type, namely
 @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a
 universal type in ML, although by some arguably accidental features of ML.
 This universal type can be used to store data of different type into a single list.
-It allows one to inject and to project data of \emph{arbitrary} type. This is
+In fact, it allows one to inject and to project data of \emph{arbitrary} type. This is
 in contrast to datatypes, which only allow injection and projection of data for
 some fixed collection of types. In light of the conventional wisdom cited
 above it is important to keep in mind that the universal type does not
 destroy type-safety of ML: storing and accessing the data can only be done
 in a type-safe manner.
 @{ML_file "Pure/ML-Systems/universal.ML"}.
 \end{readmore}
 We will show the usage of the universal type by storing an integer and
 a boolean into a single list. Let us first define injection and projection
-functions for booleans and integers into and from @{ML_type Universal.universal}.
+functions for booleans and integers into and from the type @{ML_type Universal.universal}.
 *}
 ML{*local
 val fn_int  = Universal.tag () : int  Universal.tag
 val fn_bool = Universal.tag () : bool Universal.tag
 This runtime error is the reason why ML is still type-sound despite
 containing a universal type.
 Now, Isabelle heavily uses this mechanism for storing all sorts of
 data: theorem lists, simpsets, facts etc.  Roughly speaking, there are two
-places where data can be stored: in \emph{theories} and in \emph{proof
+places where data can be stored in Isabelle: in \emph{theories} and in \emph{proof
-contexts}. Again roughly speaking, data such as simpsets need to be stored
+contexts}. Data such as simpsets need to be stored
 in a theory, since they 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.\footnote{\bf TODO: explain more about
+maintained inside a proof context.
-this in a separate section.}
 For theories and proof contexts there are, respectively, the functors
 @{ML_funct_ind TheoryDataFun} and @{ML_funct_ind ProofDataFun} that help
 with the data storage. Below we show how to implement a table in which we
 can store theorems and look them up according to a string key. The
-intention is to be able to look up introduction rules for logical
+intention in this example is to be able to look up introduction rules for logical
 connectives. Such a table might be useful in an automatic proof procedure
-and therefore it makes sense to store this data inside a theory.  The code
+and therefore it makes sense to store this data inside a theory.
-for the table is:
+Therefore we use the functor @{ML_funct TheoryDataFun}.
+The code for the table is:
 *}
 ML %linenosgray{*structure Data = TheoryDataFun
 (type T = thm Symtab.table
 val empty = Symtab.empty
 val extend = I
 fun merge _ = Symtab.merge (K true))*}
 text {*
 In order to store data in a theory, we have to specify the type of the data
-(Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which
+(Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},
-stands for tables in which @{ML_type string}s can be looked up producing an associated
+which stands for a table in which @{ML_type string}s can be looked up
-@{ML_type thm}. We also have to specify four functions: how to initialise
+producing an associated @{ML_type thm}. We also have to specify four
-the data storage (Line 3), how to copy it (Line 4), how to extend it (Line
+functions to use this functor: namely how to initialise the data storage
-5) and how two tables should be merged (Line 6). These functions correspond
+(Line 3), how to copy it (Line 4), how to extend it (Line 5) and how two
-roughly to the operations performed on theories.\footnote{\bf FIXME: Say more
+tables should be merged (Line 6). These functions correspond roughly to the
-about the assumptions of these operations.} The result structure @{ML_text Data}
+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 are also two more functions (@{ML Data.init} and
-@{ML Data.put}), which however we ignore here. Below we define two auxiliary
+@{ML Data.put}), which however are not relevant here. Below we define two
-functions, which help us with accessing the table.
+auxiliary functions, which help us with accessing the table.
 *}
 ML{*val lookup = Symtab.lookup o Data.get
 fun update k v = Data.map (Symtab.update (k, v))*}
 update "All"    @{thm allI}
 *}
 text {*
 The use of the command \isacommand{setup} makes sure the table in the
-\emph{current} theory is updated. The lookup can now be performed as
+\emph{current} theory is updated (this is explained further in
-follows.
+section~\ref{sec:theories}). The lookup can now be performed as follows.
 @{ML_response_fake [display, gray]
 "lookup @{theory} \"op &\""
 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
 *}
 setup %gray {* update "op &" @{thm TrueI} *}
 text {*
-and @{ML lookup} now produces the introduction rule for @{term "True"}
+and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
 @{ML_response_fake [display, gray]
 "lookup @{theory} \"op &\""
 "SOME \"True\""}
 there are no references involved. This is one of the most fundamental
-coding conventions for programming in Isabelle. References would
+coding conventions for programming in Isabelle. References
 interfere with the multithreaded execution model of Isabelle and also
-defeat its undo-mechanism in proof scripts. For this consider the
+defeat its undo-mechanism. To see the latter, consider the
 following data container where we maintain a reference to a list of
 integers.
 *}
 ML{*structure WrongRefData = TheoryDataFun
 ML{*fun ref_update n = WrongRefData.map
 (fn r => let val _ = r := n::(!r) in r end)*}
 text {*
 which takes an integer and adds it to the content of the reference.
-As done above, we update the reference with the command
+As before, we update the reference with the command
 \isacommand{setup}.
 *}
 setup %gray {* ref_update 1 *}
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 "ref [1]"}
 So far everything is as expected. But, the trouble starts if we attempt to
-backtrack to the point ``before'' the \isacommand{setup}-command. There, we
+backtrack to the ``point'' before the \isacommand{setup}-command. There, we
 would expect that the list is empty again. But since it is stored in a
 reference, Isabelle has no control over it. So it is not empty, but still
 @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
 \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
 Unsynchronized}, but
 including association lists in @{ML_file "Pure/General/alist.ML"},
 directed graphs in @{ML_file "Pure/General/graph.ML"}, and
 tables and symtables in @{ML_file "Pure/General/table.ML"}.
 \end{readmore}
-Storing data in a proof context is done in a similar fashion. The
+Storing data in a proof context is done in a similar fashion. As mentioned
-corresponding functor is @{ML_funct_ind ProofDataFun}. With the
+before, the corresponding functor is @{ML_funct_ind ProofDataFun}. With the
 following code we can store a list of terms in a proof context.
 *}
 ML{*structure Data = ProofDataFun
 (type T = term list
 fun init _ = [])*}
 text {*
 The function we have to specify has to produce a list once a context
-is initialised (taking the theory into account from which the
+is initialised (possibly taking the theory into account from which the
 context is derived). We choose to just return the empty list. Next
 we define two auxiliary functions for updating the list with a given
 term and printing the list.
 *}
 associated data. This is different to theories, where the command
 \isacommand{setup} registers the data with the current and future
 theories, and therefore one can access the data potentially
 indefinitely.
-For convenience there is an abstract layer, the type @{ML_type Context.generic},
+For convenience there is an abstract layer, namely the type @{ML_type Context.generic},
-for theories and proof contexts. This type is defined as follows
+for treating theories and proof contexts more uniformly. This type is defined as follows
 *}
 ML_val{*datatype generic =
 Theory of theory
 | Proof of proof*}
 text {*
-For this type a number of operations are defined which allow the
+\footnote{\bf FIXME: say more about generic contexts.}
-uniform treatment of theories and proof contexts.
 There are two special instances of the data storage mechanism described
-above. The first instance are named theorem lists. Since storing theorems in a list
+above. The first instance implements named theorem lists using the functor
-is such a common task, there is the special functor @{ML_funct_ind Named_Thms}.
+@{ML_funct_ind Named_Thms}. This is because storing theorems in a list
-To obtain a named theorem list, you just declare
+is such a common task.  To obtain a named theorem list, you just declare
 *}
 ML{*structure FooRules = Named_Thms
 (val name = "foo"
 val description = "Theorems for foo") *}
 text {*
 This code declares a data container where the theorems are stored,
 an attribute @{text foo} (with the @{text add} and @{text del} options
 for adding and deleting theorems) and an internal ML-interface to retrieve and
 modify the theorems.
+Furthermore, the theorems are made available on the user-level under the name
-Furthermore, the facts are made available on the user-level under the dynamic
+@{text foo}. For example you can declare three lemmas to be a member of the
-fact name @{text foo}. For example you can declare three lemmas to be of the kind
+theorem list @{text foo} by:
-@{text foo} by:
 *}
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
 lemma rule3[foo]: "C" sorry
 text {* and undeclare the first one by: *}
 declare rule1[foo del]
-text {* and query the remaining ones with:
+text {* You can query the remaining ones with:
 \begin{isabelle}
 \isacommand{thm}~@{text "foo"}\\
 @{text "> ?C"}\\
 @{text "> ?B"}
 @{ML_response_fake [display,gray]
 "FooRules.get @{context}"
 "[\"True\", \"?C\",\"?B\"]"}
 Note that this function takes a proof context as argument. This might be
-confusing, since the theorem list is stored as theory data. The proof context
+confusing, since the theorem list is stored as theory data. It becomes clear by knowing
-however conatains the information about the current theory and so the function
+that the proof context contains the information about the current theory and so the function
 can access the theorem list in the theory via the context.
 \begin{readmore}
 For more information about named theorem lists see
 @{ML_file "Pure/Tools/named_thms.ML"}.
 "let
 val ctxt = @{context}
 val ctxt' = Config.put sval \"foo\" ctxt
 val ctxt'' = Config.put sval \"bar\" ctxt'
 in
-(Config.get ctxt sval, Config.get ctxt' sval, Config.get ctxt'' sval)
+(Config.get ctxt sval,
+Config.get ctxt' sval,
+Config.get ctxt'' sval)
 end"
 "(\"some string\", \"foo\", \"bar\")"}
 \begin{readmore}
 For more information about configuration values see
 contexts.
 \begin{conventions}
 \begin{itemize}
 \item Print messages that belong together as a single string.
-\item Do not use references in any Isabelle code.
+\item Do not use references in Isabelle code.
 \end{itemize}
 \end{conventions}
 *}

changeset 350	364fffa80794
parent 347	01e71cddf6a3
child 351	f118240ab44a