--- a/CookBook/FirstSteps.thy Thu Feb 05 22:40:46 2009 +0000
+++ b/CookBook/FirstSteps.thy Thu Feb 05 22:44:11 2009 +0000
@@ -516,6 +516,59 @@
section {* Theorem Attributes *}
+section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
+
+text {*
+ It will often be necesseary to inspect terms, cterms or theorems. Isabelle
+ contains elaborate pretty-printing functions for that, but for quick-and-dirty
+ solutions they are too unwieldy. A term can be transformed into a string using
+ the function @{ML Syntax.string_of_term}
+
+ @{ML_response_fake [display,gray]
+ "Syntax.string_of_term @{context} @{term \"1::nat\"}"
+ "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
+
+ This produces a string, though with printing directions encoded in it. This
+ can be properly printed, when enclosed in a @{ML warning}
+
+ @{ML_response_fake [display,gray]
+ "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+ "\"1\""}
+
+ A @{ML_type cterm} can be transformed into a string by the function:
+*}
+
+ML{*fun str_of_cterm ctxt t =
+ Syntax.string_of_term ctxt (term_of t)*}
+
+text {*
+ If there are more than one @{ML_type cterm} to be printed, we can use the function
+ @{ML commas} to conveniently separate them.
+*}
+
+ML{*fun str_of_cterms ctxt ts =
+ commas (map (str_of_cterm ctxt) ts)*}
+
+text {*
+ The easiest way to get the string of a theorem, is to transform it
+ into a @{ML_type cterm} using the function @{ML crep_thm}.
+*}
+
+ML{*fun str_of_thm ctxt thm =
+ let
+ val {prop, ...} = crep_thm thm
+ in
+ str_of_cterm ctxt prop
+ end*}
+
+text {*
+ For more than one theorem, the following function adds commas in between them.
+*}
+
+ML{*fun str_of_thms ctxt thms =
+ commas (map (str_of_thm ctxt) thms)*}
+
+
section {* Operations on Constants (Names) *}
text {*
@@ -589,9 +642,10 @@
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
common when dealing with theories (for example by adding a definition, followed by
- lemmas and so on). It should also be familiar to anyone who has used Haskell's
- do-notation. Writing the function @{ML inc_by_five} using the reverse
- application is much clearer than writing
+ lemmas and so on). The reverse application allows you to read what happens inside
+ the function in a top-down manner. This kind of codeing should also be familiar,
+ if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using
+ the reverse application is much clearer than writing
*}
ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
@@ -648,8 +702,8 @@
however, it uses @{ML tap} for printing the ``plus-one'' intermediate
result inside the tracing buffer. The function @{ML tap} can only
be used for side-calculations, because any value that is computed cannot
- be merged back into the ``main waterfall''. To do this, the next combinator
- can be used.
+ 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
@@ -661,11 +715,10 @@
|> (fn (x, y) => (x, y + 1))*}
text {*
- takes @{text x} as argument, and then first
- increments @{text x}, but also keeps @{text x}. The intermediate result is
- therefore the pair @{ML "(x + 1, x)" for x}. The function then increments the
- right-hand component of the pair. So finally the result will be
- @{ML "(x + 1, x + 1)" for x}.
+ takes @{text x} as argument, and then increments @{text x}, but also keeps
+ @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+ for x}. After that, the function increments the right-hand component of the
+ pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
The combinators @{ML "|>>"} and @{ML "||>"} are defined for
functions manipulating pairs. The first applies the function to