--- a/ProgTutorial/FirstSteps.thy Sun Oct 11 16:30:59 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy Sun Oct 11 22:45:29 2009 +0200
@@ -13,7 +13,7 @@
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}
@@ -82,7 +82,7 @@
\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
@@ -238,7 +238,7 @@
"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.
*}
@@ -271,7 +271,7 @@
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"}.
@@ -283,7 +283,7 @@
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 =
@@ -316,7 +316,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. 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,\";
@@ -339,8 +339,8 @@
"cat_lines [\"foo\", \"bar\"]"
"\"foo\\nbar\""}
- Section \ref{sec:pretty} will also explain infrastructure that helps
- with more elaborate pretty printing.
+ Section \ref{sec:pretty} will also explain the infrastructure of Isabelle
+ that helps with more elaborate pretty printing.
*}
@@ -429,7 +429,7 @@
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]
@@ -638,7 +638,7 @@
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
@@ -679,7 +679,6 @@
\end{readmore}
\footnote{\bf FIXME: find a good exercise for combinators}
-
\footnote{\bf FIXME: say something about calling conventions}
*}
@@ -687,23 +686,22 @@
section {* ML-Antiquotations *}
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 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{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. Document
- antiquotations are part of the user level and therefore we are not
- interested in them in this Tutorial, except in Appendix
+ 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{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. 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 by typing
-
@{ML_response [display,gray] "Context.theory_name @{theory}" "\"FirstSteps\""}
@@ -835,7 +833,7 @@
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]
@@ -843,6 +841,11 @@
"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
@@ -1238,6 +1241,22 @@
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.
*}