diff -r 92f6a772e013 -r 4172c0743cf2 ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Sep 28 01:21:27 2009 +0200 +++ b/ProgTutorial/FirstSteps.thy Mon Sep 28 23:52:06 2009 +0200 @@ -11,12 +11,13 @@ ``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 The 300-Meter Tower.\footnote{The Eiffel Tower has been + 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 - from top to bottom.}\\[1ex] + from top to bottom.} \end{flushright} + \medskip Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for Isabelle must be part of a theory. If you want to follow the code given in this chapter, we assume you are working inside the theory starting with @@ -30,8 +31,8 @@ \end{tabular} \end{quote} - We also generally assume you are working with HOL. The given examples might - need to be adapted if you work in a different logic. + 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 *} @@ -252,9 +253,9 @@ string_of_term ctxt (term_of ct)*} text {* - In this example the function @{ML_ind term_of} extracts the @{ML_type + In this example the function @{ML_ind term_of} extracts the @{ML_type term} from a @{ML_type cterm}. More than one @{ML_type cterm}s can again be - printed with @{ML_ind commas}. + printed with @{ML_ind commas}. *} ML{*fun string_of_cterms ctxt cts = @@ -262,11 +263,13 @@ text {* The easiest way to get the string of a theorem is to transform it - into a @{ML_type cterm} using the function @{ML_ind crep_thm}. + into a @{ML_type term} using the function @{ML_ind prop_of}. *} +ML {* Thm.rep_thm @{thm mp} *} + ML{*fun string_of_thm ctxt thm = - string_of_cterm ctxt (#prop (crep_thm thm))*} + Syntax.string_of_term ctxt (prop_of thm)*} text {* Theorems also include schematic variables, such as @{text "?P"}, @@ -293,7 +296,7 @@ end fun string_of_thm_no_vars ctxt thm = - string_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} + Syntax.string_of_term ctxt (prop_of (no_vars ctxt thm))*} text {* Theorem @{thm [source] conjI} is now printed as follows: @@ -315,7 +318,7 @@ Note, that when printing out several parcels of information that semantically belong together, like a warning message consisting for example of a term and a type, you should try to keep this information together in a - single string. So do not print out information as + single string. Therefore do not print out information as @{ML_response_fake [display,gray] "tracing \"First half,\"; @@ -397,7 +400,7 @@ text {* or *} ML{*fun inc_by_five x = - ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*} + ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*} text {* and typographically more economical than *} @@ -444,7 +447,7 @@ You can read off this behaviour from how @{ML apply_fresh_args} is coded: in Line 2, the function @{ML_ind fastype_of} calculates the type of the - term; @{ML_ind binder_types} in the next line produces the list of argument + term; @{ML_ind binder_types} in the next line produces the list of argument types (in the case above the list @{text "[nat, int, unit]"}); Line 4 pairs up each type with the string @{text "z"}; the function @{ML_ind variant_frees in Variable} generates for each @{text "z"} a @@ -643,21 +646,21 @@ "let val ctxt = @{context} in - map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"] + map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"] |> Syntax.check_terms ctxt |> string_of_terms ctxt |> tracing end" - "m + n, m - n"} + "m + n, m * n, m - n"} *} text {* - In this example we obtain two terms with appropriate typing. However, if you - have only a single term, then @{ML check_terms in Syntax} needs to be - adapted. This can be done with the ``plumbing'' 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 + In this example we obtain three terms where @{text m} and @{text n} are of + type @{typ "nat"}. However, 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_response_fake [display, gray] "let @@ -689,20 +692,18 @@ The main advantage of embedding all code in a theory 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 with ML-antiquotations, often also referred to as just + is realised with ML-antiquotations, often just called antiquotations.\footnote{There are two kinds of antiquotations in Isabelle, which have very different purpose and infrastructures. The first kind, described in this section, are \emph{ML-antiquotations}. 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} antiquotations. They - are used only in the text parts of Isabelle and their purpose is to print - logical entities inside \LaTeX-documents. They 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 - + ML-code. The other kind of antiquotations are \emph{document} + antiquotations. They are used only in the text parts of Isabelle and their + purpose is to print logical entities inside \LaTeX-documents. They 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 @{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""} @@ -821,11 +822,11 @@ 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 4); the next two lines print the term so that the - ML-system can understand them. The function @{ML atomic in ML_Syntax} - just encloses the term in parentheses. An example for the usage of this - antiquotation is: + transformed into a term using the function @{ML_ind read_term_pattern in + ProofContext} (Line 4); the next two lines transform the term into a string + so that the ML-system can understand them. The function @{ML_ind atomic in + ML_Syntax} just encloses the term in parentheses. An example for the usage + of this antiquotation is: @{ML_response_fake [display,gray] "@{term_pat \"Suc (?x::nat)\"}" @@ -844,7 +845,9 @@ text {* Isabelle provides a mechanism to store (and retrieve) arbitrary data. Before we - explain this mechanism. + explain this mechanism, let us digress a bit. Convenitional wisdom is that the + type-system of ML ensures that for example an @{ML_type "'a list"} can only + hold elements of type @{ML_type "'a"}. *} ML{*signature UNIVERSAL_TYPE =