# HG changeset patch # User Christian Urban # Date 1255293929 -7200 # Node ID 8f73e80c8c6fa29a3e0f3d24db4345ba5e3ee1c9 # Parent 930b1308fd96acaf831723fcb6195499d9c76964 polished first chapter diff -r 930b1308fd96 -r 8f73e80c8c6f ProgTutorial/FirstSteps.thy --- 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 \ int \ unit \ 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 \ 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 \}"}-antiquotation. + + @{ML_response_fake [display,gray] + "@{term \"Suc (x::nat)\"}" + "Const (\"Suc\", \"nat \ 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. *} diff -r 930b1308fd96 -r 8f73e80c8c6f ProgTutorial/General.thy --- a/ProgTutorial/General.thy Sun Oct 11 16:30:59 2009 +0200 +++ b/ProgTutorial/General.thy Sun Oct 11 22:45:29 2009 +0200 @@ -2,7 +2,7 @@ imports Base FirstSteps begin -chapter {* Isabelle -- The Good, the Bad and the Ugly *} +chapter {* Let's Talk About the Good, the Bad and the Ugly *} text {* Isabelle is build around a few central ideas. One is the LCF-approach to diff -r 930b1308fd96 -r 8f73e80c8c6f ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Sun Oct 11 16:30:59 2009 +0200 +++ b/ProgTutorial/Intro.thy Sun Oct 11 22:45:29 2009 +0200 @@ -94,10 +94,10 @@ \end{isabelle} These boxes correspond to how code can be processed inside the interactive - environment of Isabelle. It is therefore easy to experiment with what is - displayed. However, for better readability we will drop the enclosing - \isacommand{ML}~@{text "\ \ \"} and just write: - + environment of Isabelle. It is therefore easy to experiment with the code + that is given in this tutorial. However, for better readability we will drop + the enclosing \isacommand{ML}~@{text "\ \ \"} and just + write: @{ML [display,gray] "3 + 4"} @@ -218,7 +218,7 @@ \item {\bf Armin Heller} helped with recipe \ref{rec:sat}. \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' - chapter and also contributed the material on @{ML_functor Named_Thms}. + chapter and also contributed the material on @{ML_funct Named_Thms}. \item {\bf Christian Sternagel} proofread the tutorial and made many improvemets to the text. diff -r 930b1308fd96 -r 8f73e80c8c6f progtutorial.pdf Binary file progtutorial.pdf has changed