isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:e6f583366779
+:6bf955db9b62
 We also generally assume you are working with the logic HOL. The examples
 that will be given might need to be adapted if you work in a different logic.
 *}
-section {* Including ML-Code *}
+section {* Including ML-Code\label{sec:include} *}
 text {*
 The easiest and quickest way to include code in a theory is by using the
 \isacommand{ML}-command. For example:
 ML{*fun string_of_terms ctxt ts =
 commas (map (string_of_term ctxt) ts)*}
 text {*
-Sometimes you want to print out a term together with some type information.
+You can also print out term together with type information.
 This can be achieved by setting the reference @{ML_ind show_types in Syntax}
 to @{ML true}.
 *}
 ML{*show_types := true*}
 @{ML_response_fake [display, gray]
 "tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
 "(1::nat, x::'a)"}
-where @{text 1} and @{text x} are displayed with their type.
+where @{text 1} and @{text x} are displayed with their inferred type.
 Even more type information can be printed by setting
-@{ML_ind show_all_types in Syntax} to @{ML true}. We obtain
+@{ML_ind show_all_types in Syntax} to @{ML true}. We obtain then
 *}
 (*<*)ML %linenos {*show_all_types := true*}
 (*>*)
 text {*
 @{ML_response_fake [display, gray]
 variant_frees in Variable} generates for each @{text "z"} a unique name
 avoiding the given @{text f}; the list of name-type pairs is turned into a
 list of variable terms in Line 6, which in the last line is applied by the
 function @{ML_ind list_comb in Term} to the term. In this last step we have
 to use the function @{ML_ind curry in Library}, because @{ML list_comb}
-expects the function and the variables list as a pair. This kind of
+expects the function and the variables list as a pair.
-functions is often needed when constructing terms with fresh variables. The
+Functions like @{ML apply_fresh_args} are often needed when constructing
+terms with fresh variables. The
 infrastructure helps tremendously to avoid any name clashes. Consider for
 example:
 @{ML_response_fake [display,gray]
 "let
 end"
 "m + n, m * n, m - n"}
 *}
 text {*
-In this example we obtain three terms (using @{ML_ind parse_term in Syntax}) whose
+In this example we obtain three terms (using the function
-variables @{text m} and @{text n} are of type @{typ "nat"}. If you have only
+@{ML_ind parse_term in Syntax}) whose variables @{text m} and @{text n}
-a single term, then @{ML
+are of type @{typ "nat"}. If you have only a single term, then @{ML
 check_terms in Syntax} needs plumbing. This can be done with the function
-@{ML singleton}.\footnote{There is already a function @{ML check_term in
+@{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in
-Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
+Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented
-and @{ML check_terms in Syntax}.} For example
+in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
-@{ML_response_fake [display, gray]
+@{ML_response_fake [display, gray, linenos]
 "let
 val ctxt = @{context}
 in
 Syntax.parse_term ctxt \"m - (n::nat)\"
 |> singleton (Syntax.check_terms ctxt)
 |> string_of_term ctxt
 |> tracing
 end"
 "m - n"}
+where in Line 5, the function operating over lists fits with the
+single term generated in Line 4.
 \begin{readmore}
 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.
 section {* ML-Antiquotations *}
 text {*
-Recall that code in Isabelle is always embedded in a theory.  The main
+Recall from Section \ref{sec:include} that code in Isabelle is always
-advantage of this is that the code can contain references to entities
+embedded in a theory.  The main advantage of this is that the code can
-defined on the logical level of Isabelle. By this we mean definitions,
+contain references to entities defined on the logical level of Isabelle. By
-theorems, terms and so on. This kind of reference is realised in Isabelle
+this we mean references to definitions, theorems, terms and so on. These
-with ML-antiquotations, often just called antiquotations.\footnote{There are
+reference are realised in Isabelle with ML-antiquotations, often just called
-two kinds of antiquotations in Isabelle, which have very different purposes
+antiquotations.\footnote{Note that there are two kinds of antiquotations in
-and infrastructures. The first kind, described in this section, are
+Isabelle, which have very different purposes and infrastructures. The first
-\emph{\index*{ML-antiquotation}}. They are used to refer to entities (like terms,
+kind, described in this section, are \emph{\index*{ML-antiquotation}}. They
-types etc) from Isabelle's logic layer inside ML-code. The other kind of
+are used to refer to entities (like terms, types etc) from Isabelle's logic
-antiquotations are \emph{document}\index{document antiquotation} antiquotations.
+layer inside ML-code. The other kind of antiquotations are
-They are used only in the
+\emph{document}\index{document antiquotation} antiquotations. They are used
-text parts of Isabelle and their purpose is to print logical entities inside
+only in the text parts of Isabelle and their purpose is to print logical
-\LaTeX-documents. Document antiquotations are part of the user level and
+entities inside \LaTeX-documents. Document antiquotations are part of the
-therefore we are not interested in them in this Tutorial, except in Appendix
+user level and therefore we are not interested in them in this Tutorial,
-\ref{rec:docantiquotations} where we show how to implement your own document
+except in Appendix \ref{rec:docantiquotations} where we show how to
-antiquotations.}  For example, one can print out the name of the current
+implement your own document antiquotations.}  Syntactically antiquotations
-theory with the code
+are indicated by the @{ML_text @}-sign followed by text wrapped in @{text
+"{\<dots>}"}.  For example, one can print out the name of the current 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
 \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 describe how the (build in)
+also difficult to read. In the next chapter we describe how to construct
-antiquotation @{text "@{term \<dots>}"} for constructing terms.  A
+terms with the (build in) antiquotation @{text "@{term \<dots>}"}.  A restriction
-restriction of this antiquotation is that it does not allow you to use
+of this antiquotation is that it does not allow you to use schematic
-schematic variables in terms. If you want to have an antiquotation that does not have
+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} in the structure @{ML_struct ML_Antiquote}. The code
+inline in ML_Antiquote} from the structure @{ML_struct ML_Antiquote}. The code
 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 this antiquotation is:
+so that the ML-system can understand it. (All these functions will be explained
+in more detail in later sections.) An example for this antiquotation is:
 @{ML_response_fake [display,gray]
 "@{term_pat \"Suc (?x::nat)\"}"
 "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 @{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.
 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
+some \emph{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.
 \begin{readmore}
 in
 [thirteen, truth_val]
 end*}
 text {*
-The data can be retrieved using the projection functions.
+The data can be retrieved with the projection functions defined above.
-@{ML_response [display, gray]
+@{ML_response_fake [display, gray]
-"(project_int (nth foo_list 0), project_bool (nth foo_list 1))"
+"project_int (nth foo_list 0);
-"(13, true)"}
+project_bool (nth foo_list 1)"
+"13
+true"}
 Notice that we access the integer as an integer and the boolean as
 a boolean. If we attempt to access the integer as a boolean, then we get
 a runtime error.
 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 Isabelle: in \emph{theories} and in \emph{proof
-contexts}. Data such as simpsets need to be stored
+contexts}. Data such as simpsets are ``global'' and therefore need to be stored
-in a theory, since they need to be maintained across proofs and even across
+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
+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.
+maintained inside a proof context, which represents ``local'' data.
 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
+with the data storage. Below we show how to implement a table in which you
 can store theorems and look them up according to a string key. The
 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.
-Therefore we use the functor @{ML_funct TheoryDataFun}.
+Consequently we use the functor @{ML_funct TheoryDataFun}.
 The code for the table is:
 *}
 ML %linenosgray{*structure Data = TheoryDataFun
 (type T = thm Symtab.table
 producing an associated @{ML_type thm}. We also have to specify four
 functions to use this functor: namely how to initialise the data storage
 (Line 3), how to copy it (Line 4), how to extend it (Line 5) and how two
 tables should be merged (Line 6). These functions correspond roughly to the
 operations performed on theories and we just give some sensible
-defaults\footnote{\bf FIXME: Say more about the
+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 are not relevant here. Below we define two
 auxiliary functions, which help us with accessing the table.
 fun init _ = [])*}
 text {*
 The function we have to specify has to produce a list once a context
 is initialised (possibly taking the theory into account from which the
-context is derived). We choose to just return the empty list. Next
+context is derived). We choose here to just return the empty list. Next
 we define two auxiliary functions for updating the list with a given
 term and printing the list.
 *}
 ML{*fun update trm = Data.map (fn trms => trm::trms)

changeset 372	6bf955db9b62
parent 371	e6f583366779
child 373	28a49fe024c9