# HG changeset patch # User griff # Date 1237806801 -3600 # Node ID 840b49bfb1cfd5e686b691ae8b44985293a4f533 # Parent 7305beb698939f86d5ecab72959d898aa1f6afb6 fixed `str_of_thms' output in example + small changes diff -r 7305beb69893 -r 840b49bfb1cf ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Mar 23 09:18:46 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Mon Mar 23 12:13:21 2009 +0100 @@ -80,7 +80,7 @@ @{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""} - However @{ML makestring} only works if the type of what is converted is monomorphic + However, @{ML makestring} only works if the type of what is converted is monomorphic and not a function. The function @{ML "warning"} should only be used for testing purposes, because any @@ -92,7 +92,7 @@ @{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""} It is also possible to redirect the ``channel'' where the string @{text "foo"} is - printed to a separate file, e.g.~to prevent ProofGeneral from choking on massive + printed to a separate file, e.g., to prevent ProofGeneral from choking on massive amounts of trace output. This redirection can be achieved with the code: *} @@ -201,8 +201,8 @@ Theorem @{thm [source] conjI} looks now as follows @{ML_response_fake [display, gray] - "warning (str_of_thm_raw @{context} @{thm conjI})" - "\?P; ?Q\ \ ?P \ ?Q"} + "warning (str_of_thm @{context} @{thm conjI})" + "\P; Q\ \ P \ Q"} Again the function @{ML commas} helps with printing more than one theorem. *} @@ -251,7 +251,7 @@ |> (fn x => x + 4)*} text {* - which increments its argument @{text x} by 5. It does this by first incrementing + which increments its argument @{text x} by 5. It proceeds by first incrementing the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking the first component of the pair (Line 4) and finally incrementing the first component by 4 (Line 5). This kind of cascading manipulations of values is quite @@ -352,9 +352,9 @@ cannot be merged back into the ``main waterfall''. To do this, you can use the next combinator. - The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value - and returns the result together with the value (as a pair). For example - the function + The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a + function to the value and returns the result together with the value (as a + pair). For example the function *} ML{*fun inc_as_pair x = @@ -396,7 +396,8 @@ |-> (fn x => fn y => x + y)*} text {* - Recall that @{ML "|>"} is the reverse function applications. Recall also that the related + Recall that @{ML "|>"} is the reverse function application. Recall also that + the related reverse function composition is @{ML "#>"}. In fact all the combinators @{ML "|->"}, @{ML "|>>"} and @{ML "||>"} described above have related combinators for function composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"}, @@ -412,7 +413,8 @@ (FIXME: find a good exercise for combinators) \begin{readmore} - The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"} + The most frequently used combinators are defined in the files @{ML_file + "Pure/library.ML"} and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans} contains further information about combinators. \end{readmore} @@ -486,20 +488,21 @@ "get_thm_names_from_ss @{simpset}" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \]"} - Again, this way or referencing simpsets makes you independent from additions + Again, this way of referencing simpsets makes you independent from additions of lemmas to the simpset by the user that potentially cause loops. On the ML-level of Isabelle, you often have to work with qualified names; - these are strings with some additional information, such positional information + these are strings with some additional information, such as positional information and qualifiers. Such bindings can be generated with the antiquotation - @{text "@{bindin \}"}. + @{text "@{binding \}"}. @{ML_response [display,gray] "@{binding \"name\"}" "name"} - An example where a binding is needed is the function @{ML define in LocalTheory}. - Below this function defines the constant @{term "TrueConj"} as the conjunction + An example where a binding is needed is the function @{ML define in + LocalTheory}. Below, this function is used to define the constant @{term + "TrueConj"} as the conjunction @{term "True \ True"}. *} @@ -509,21 +512,21 @@ (Attrib.empty_binding, @{term "True \ True"})) *} text {* - While antiquotations have many applications, they were originally introduced in order - to avoid explicit bindings for theorems such as: + While antiquotations have many applications, they were originally introduced + in order to avoid explicit bindings of theorems such as: *} ML{*val allI = thm "allI" *} text {* - These bindings are difficult to maintain and also can be accidentally - overwritten by the user. This often broke Isabelle + Such bindings are difficult to maintain and can be overwritten by the + user accidentally. This often broke Isabelle packages. Antiquotations solve this problem, since they are ``linked'' statically at compile-time. However, this static linkage also limits their usefulness in cases where data needs to be build up dynamically. In the - course of this chapter you will learn more about these antiquotations: + course of this chapter you will learn more about antiquotations: they can simplify Isabelle programming since one can directly access all - kinds of logical elements from th ML-level. + kinds of logical elements from the ML-level. *} section {* Terms and Types *} @@ -1360,4 +1363,4 @@ ML {*DatatypePackage.get_datatype @{theory} "List.list"*} -end \ No newline at end of file +end diff -r 7305beb69893 -r 840b49bfb1cf progtutorial.pdf Binary file progtutorial.pdf has changed