isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:92f6a772e013
+:4172c0743cf2
 \begin{flushright}
 {\em
 ``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
 \begin{quote}
 \isacommand{begin}\\
 \ldots
 \end{tabular}
 \end{quote}
-We also generally assume you are working with HOL. The given examples might
+We also generally assume you are working with the logic HOL. The examples
-need to be adapted if you work in a different logic.
+that will be given might need to be adapted if you work in a different logic.
 *}
 section {* Including ML-Code *}
 text {*
 ML{*fun string_of_cterm ctxt ct =
 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 =
 commas (map (string_of_cterm ctxt) cts)*}
 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"},
 @{text "?Q"} and so on. They are needed in order to able to
 instantiate theorems when they are applied. For example the theorem
 in
 thm'
 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:
 @{ML_response_fake [display, gray]
 text {*
 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,\";
 tracing \"and second half.\""
 "First half,
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
 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*}
 text {* and typographically more economical than *}
 ML{*fun inc_by_five x =
 let val y1 = x + 1
 end"
 "P z za zb"}
 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
 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
 @{ML_response_fake [display, gray]
 "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
+In this example we obtain three terms where @{text m} and @{text n} are of
-have only a single term, then @{ML check_terms in Syntax} needs to be
+type @{typ "nat"}. However, if you have only a single term, then @{ML
-adapted. This can be done with the ``plumbing'' function @{ML
+check_terms in Syntax} needs plumbing. This can be done with the function
-singleton}.\footnote{There is already a function @{ML check_term in Syntax}
+@{ML singleton}.\footnote{There is already a function @{ML check_term in
-in the Isabelle sources that is defined in terms of @{ML singleton} and @{ML
+Syntax} in the Isabelle sources that is defined in terms of @{ML singleton}
-check_terms in Syntax}.} For example
+and @{ML check_terms in Syntax}.} For example
 @{ML_response_fake [display, gray]
 "let
 val ctxt = @{context}
 in
 text {*
 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
+ML-code. The other kind of antiquotations are \emph{document}
-are used only in the text parts of Isabelle and their purpose is to print
+antiquotations. They are used only in the text parts of Isabelle and their
-logical entities inside \LaTeX-documents. They are part of the user level
+purpose is to print logical entities inside \LaTeX-documents. They are part
-and therefore we are not interested in them in this Tutorial, except in
+of the user level and therefore we are not interested in them in this
-Appendix \ref{rec:docantiquotations} where we show how to implement your own
+Tutorial, except in Appendix \ref{rec:docantiquotations} where we show how
-document antiquotations.}
+to implement your own document antiquotations.}  For example, one can print
-For example, one can print out the name of the current
+out the name of the current theory by typing
-theory by typing
 @{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_Syntax.print_term
 |> ML_Syntax.atomic))*}
 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
+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
+ProofContext} (Line 4); the next two lines transform the term into a string
-ML-system can understand them. The function @{ML atomic in ML_Syntax}
+so that the ML-system can understand them. The function @{ML_ind atomic in
-just encloses the term in parentheses. An example for the usage of this
+ML_Syntax} just encloses the term in parentheses. An example for the usage
-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\")"}
 section {* Storing Data (TBD) *}
 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 =
 sig
 type t

changeset 324	4172c0743cf2
parent 323	92f6a772e013
child 325	352e31d9dacc