isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:930b1308fd96
+:8f73e80c8c6f
 ``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 a 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
 \isacommand{oops}
 \end{isabelle}
 \end{quote}
 However, both commands will only play minor roles in this tutorial (we will
-always arrange that the ML-code is defined outside of proofs, for example).
+always arrange that the ML-code is defined outside of proofs).
 Once a portion of code is relatively stable, you usually want to export it
 to a separate ML-file. Such files can then be included somewhere inside a
 theory by using the command \isacommand{use}. For example
 @{ML_response_fake [display,gray]
 "tracing (string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
-If there are more than one @{ML_type term}s to be printed, you can use the
+If there are more than one term to be printed, you can use the
 function @{ML_ind  commas} to separate them.
 *}
 ML{*fun string_of_terms ctxt ts =
 commas (map (string_of_term ctxt) ts)*}
 ML{*fun string_of_thm ctxt thm =
 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
+@{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"}.
 @{ML_response_fake [display, gray]
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 However, in order to improve the readability when printing theorems, we
 convert these schematic variables into free variables using the function
 @{ML_ind  import in Variable}. This is similar to statements like @{text
-"conjI[no_vars]"} from Isabelle's user-level.
+"conjI[no_vars]"} on Isabelle's user-level.
 *}
 ML{*fun no_vars ctxt thm =
 let
 val ((_, [thm']), _) = Variable.import true [thm] ctxt
 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. Therefore do not print out information as
+single string. Therefore do \emph{not} print out information as
 @{ML_response_fake [display,gray]
 "tracing \"First half,\";
 tracing \"and second half.\""
 "First half,
 @{ML_response [display, gray]
 "cat_lines [\"foo\", \"bar\"]"
 "\"foo\\nbar\""}
-Section \ref{sec:pretty} will also explain infrastructure that helps
+Section \ref{sec:pretty} will also explain the infrastructure of Isabelle
-with more elaborate pretty printing.
+that helps with more elaborate pretty printing.
 *}
 section {* Combinators\label{sec:combinators} *}
 |> curry list_comb f *}
 text {*
 This function takes a term and a context as argument. If the term is of function
 type, then @{ML "apply_fresh_args"} returns the term with distinct variables
-applied to it. For example below variables are applied to the term
+applied to it. For example below three variables are applied to the term
 @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 @{ML_response_fake [display,gray]
 "let
 val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
 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
 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
-of terms.
+of terms. Consider the code:
 @{ML_response_fake [display, gray]
 "let
 val ctxt = @{context}
 in
 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
 contains further information about combinators.
 \end{readmore}
 \footnote{\bf FIXME: find a good exercise for combinators}
 \footnote{\bf FIXME: say something about calling conventions}
 *}
 section {* ML-Antiquotations *}
 text {*
-The main advantage of embedding all code in a theory is that the code can
+Recall that code in Isabelle is always embedded in a theory.  The main
-contain references to entities defined on the logical level of Isabelle. By
+advantage of this is that the code can contain references to entities
-this we mean definitions, theorems, terms and so on. This kind of reference
+defined on the logical level of Isabelle. By this we mean definitions,
-is realised in Isabelle with ML-antiquotations, often just called
+theorems, terms and so on. This kind of reference is realised in Isabelle
-antiquotations.\footnote{There are two kinds of antiquotations in Isabelle,
+with ML-antiquotations, often just called antiquotations.\footnote{There are
-which have very different purposes and infrastructures. The first kind,
+two kinds of antiquotations in Isabelle, which have very different purposes
-described in this section, are \emph{ML-antiquotations}. They are used to
+and infrastructures. The first kind, described in this section, are
-refer to entities (like terms, types etc) from Isabelle's logic layer inside
+\emph{ML-antiquotations}. They are used to refer to entities (like terms,
-ML-code. The other kind of antiquotations are \emph{document}
+types etc) from Isabelle's logic layer inside ML-code. The other kind of
-antiquotations. They are used only in the text parts of Isabelle and their
+antiquotations are \emph{document} antiquotations. They are used only in the
-purpose is to print logical entities inside \LaTeX-documents. Document
+text parts of Isabelle and their purpose is to print logical entities inside
-antiquotations are part of the user level and therefore we are not
+\LaTeX-documents. Document antiquotations are part of the user level and
-interested in them in this Tutorial, except in Appendix
+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\""}
 where @{text "@{theory}"} is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 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 them. An example for the usage
+so that the ML-system can understand it. An example for the usage
 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"}.
 \begin{readmore}
 For more information about configuration values see
 @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
 \end{readmore}
+*}
+section {* Summary *}
+text {*
+This chapter describes the combinators that are used in Isabelle, as well
+as a simple printing infrastructure for @{ML_type term}, @{ML_type cterm}
+and @{ML_type thm}. The section on ML-antiquotations shows how to refer
+statically to entities from the logic level of Isabelle. Isabelle also
+contains mechanisms for storing arbitrary data in theory and proof
+contexts.
+This chapter also mentions two coding conventions: namely printing
+entities belonging together as one string, and not using references
+in any Isabelle code.
 *}
 (**************************************************)
 (* bak                                            *)

changeset 343	8f73e80c8c6f
parent 339	c588e8422737
child 344	83d5bca38bec