diff -r e6f583366779 -r 6bf955db9b62 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Nov 02 16:26:03 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Tue Nov 03 07:10:05 2009 +0100 @@ -42,7 +42,7 @@ 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 @@ -254,7 +254,7 @@ 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}. *} @@ -268,9 +268,9 @@ "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*} (*>*) @@ -507,8 +507,9 @@ 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 - functions is often needed when constructing terms with fresh variables. The + expects the function and the variables list as a pair. + 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: @@ -712,15 +713,15 @@ *} text {* - In this example we obtain three terms (using @{ML_ind parse_term in Syntax}) whose - variables @{text m} and @{text n} are of type @{typ "nat"}. If you have only - a single term, then @{ML + In this example we obtain three terms (using the function + @{ML_ind parse_term in Syntax}) whose variables @{text m} and @{text n} + 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 - Syntax} in the Isabelle sources that is defined in terms of @{ML singleton} - and @{ML check_terms in Syntax}.} For example + @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in + Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented + 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 @@ -731,6 +732,9 @@ 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"} @@ -746,23 +750,25 @@ section {* ML-Antiquotations *} text {* - Recall that code in Isabelle is always embedded in a theory. The main - advantage of this is that the code can contain references to entities - defined on the logical level of Isabelle. By this we mean definitions, - theorems, terms and so on. This kind of reference is realised in Isabelle - with ML-antiquotations, often just called antiquotations.\footnote{There are - two kinds of antiquotations in Isabelle, which have very different purposes - and infrastructures. The first kind, described in this section, are - \emph{\index*{ML-antiquotation}}. They are used to refer to entities (like terms, - types etc) from Isabelle's logic layer inside ML-code. The other kind of - antiquotations are \emph{document}\index{document antiquotation} antiquotations. - They are used only in the - 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 with the code + Recall from Section \ref{sec:include} that code in Isabelle is always + embedded in a theory. The main advantage of this is that the code can + contain references to entities defined on the logical level of Isabelle. By + this we mean references to definitions, theorems, terms and so on. These + reference are realised in Isabelle with ML-antiquotations, often just called + antiquotations.\footnote{Note that there are two kinds of antiquotations in + Isabelle, which have very different purposes and infrastructures. The first + kind, described in this section, are \emph{\index*{ML-antiquotation}}. They + are used to refer to entities (like terms, types etc) from Isabelle's logic + layer inside ML-code. The other kind of antiquotations are + \emph{document}\index{document antiquotation} antiquotations. They are used + only in the 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.} Syntactically antiquotations + are indicated by the @{ML_text @}-sign followed by text wrapped in @{text + "{\}"}. For example, one can print out the name of the current theory with + the code @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""} @@ -870,12 +876,12 @@ 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) - antiquotation @{text "@{term \}"} for constructing terms. 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 + also difficult to read. In the next chapter we describe how to construct + terms with the (build in) antiquotation @{text "@{term \}"}. 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_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. *} @@ -894,7 +900,8 @@ 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)\"}" @@ -921,7 +928,7 @@ 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. @@ -962,11 +969,13 @@ 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] -"(project_int (nth foo_list 0), project_bool (nth foo_list 1))" -"(13, true)"} + @{ML_response_fake [display, gray] +"project_int (nth foo_list 0); +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 @@ -982,20 +991,20 @@ 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 - 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 + contexts}. Data such as simpsets are ``global'' and therefore need to be stored + 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. + 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: *} @@ -1015,7 +1024,7 @@ (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 @@ -1142,7 +1151,7 @@ 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. *}