
diff -r 95461cf6fd07 -r 5fc2fb34c323 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Fri Jan 01 00:19:11 2010 +0100
+++ b/ProgTutorial/FirstSteps.thy	Fri Jan 08 21:31:45 2010 +0100
@@ -218,13 +218,14 @@
 *)
 
 text {*
-  Most often you want to inspect data of Isabelle's basic data
-  structures, namely @{ML_type term}, @{ML_type cterm} and @{ML_type
-  thm}. Isabelle contains elaborate pretty-printing functions for printing
-  them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
-  are a bit unwieldy. One way to transform a term into a string is to use the
-  function @{ML_ind  string_of_term in Syntax} from the structure @{ML_struct
-  Syntax}. For more convenience, we bind this function to the toplevel.
+  Most often you want to inspect data of Isabelle's basic data structures,
+  namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
+  and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions
+  for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty
+  solutions they are a bit unwieldy. One way to transform a term into a string
+  is to use the function @{ML_ind string_of_term in Syntax} from the structure
+  @{ML_struct Syntax}. For more convenience, we bind this function to the
+  toplevel.
 *}
 
 ML{*val string_of_term = Syntax.string_of_term*}
@@ -358,6 +359,20 @@
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
 text {*
+  The printing functions for types are
+*}
+
+ML{*fun string_of_typ ctxt ty = Syntax.string_of_typ ctxt ty
+fun string_of_typs ctxt tys = commas (map (string_of_typ ctxt) tys)*}
+
+text {*
+  respectively ctypes
+*}
+
+ML{*fun string_of_ctyp ctxt cty = string_of_typ ctxt (typ_of cty)
+fun string_of_ctyps ctxt ctys = commas (map (string_of_ctyp ctxt) ctys)*}
+
+text {*
   \begin{readmore}
   The simple conversion functions from Isabelle's main datatypes to 
   @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. 
@@ -365,10 +380,10 @@
   @{ML_file "Pure/Syntax/printer.ML"}.
   \end{readmore}
 
-  Note that for printing out several ``parcels'' of information that
-  semantically belong together, like a warning message consisting of 
-  a term and its type, you should try to keep this information together in a
-  single string. Therefore do \emph{not} print out information as
+  Note that for printing out several ``parcels'' of information that belong
+  together, like a warning message consisting of a term and its type, you
+  should try to print these parcels together in a single string. Therefore do
+  \emph{not} print out information as
 
 @{ML_response_fake [display,gray]
 "tracing \"First half,\"; 
@@ -388,11 +403,12 @@
   @{ML_ind cat_lines in Library} concatenates a list of strings 
   and inserts newlines in between each element. 
 
-  @{ML_response [display, gray]
-  "cat_lines [\"foo\", \"bar\"]"
-  "\"foo\\nbar\""}
+  @{ML_response_fake [display, gray]
+  "tracing (cat_lines [\"foo\", \"bar\"])"
+  "foo
+bar"}
 
-  Section \ref{sec:pretty} will also explain the infrastructure that Isabelle 
+  Section \ref{sec:pretty} will explain the infrastructure that Isabelle 
   provides for more elaborate pretty printing. 
 
   \begin{readmore}
@@ -443,15 +459,15 @@
     |> (fn x => x + 4)*}
 
 text {*
-  which increments its argument @{text x} by 5. It does this 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
-  common when dealing with theories (for example by adding a definition, followed by
-  lemmas and so on). The reverse application allows you to read what happens in 
-  a top-down manner. This kind of coding should also be familiar, 
-  if you have been exposed to Haskell's {\it do}-notation. Writing the function 
-  @{ML inc_by_five} using the reverse application is much clearer than writing
+  which increments its argument @{text x} by 5. It does this 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 common when dealing with theories. The
+  reverse application allows you to read what happens in a top-down
+  manner. This kind of coding should be familiar, if you have been exposed to
+  Haskell's {\it 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*}
@@ -495,10 +511,10 @@
 
   @{ML_response_fake [display,gray]
 "let
-  val t = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+  val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
   val ctxt = @{context}
 in 
-  apply_fresh_args t ctxt
+  apply_fresh_args trm ctxt
    |> string_of_term ctxt
    |> tracing
 end" 
@@ -512,21 +528,20 @@
   variant_frees in Variable} generates for each @{text "z"} a unique name
   avoiding the given @{text f}; the list of name-type pairs is turned into a
   list of variable terms in Line 6, which in the last line is applied by the
-  function @{ML_ind list_comb in Term} to the term. In this last step we have
+  function @{ML_ind list_comb in Term} to the original term. In this last step we have
   to use the function @{ML_ind curry in Library}, because @{ML list_comb}
   expects the function and the variables list as a pair. 
   
-  Functions like @{ML apply_fresh_args} are often needed when constructing 
-  terms with fresh variables. The
-  infrastructure helps tremendously to avoid any name clashes. Consider for
-  example:
+  Functions like @{ML apply_fresh_args} are often needed when constructing
+  terms involving fresh variables. For this the infrastructure helps
+  tremendously to avoid any name clashes. Consider for example:
 
    @{ML_response_fake [display,gray]
 "let
-  val t = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+  val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
   val ctxt = @{context}
 in
-  apply_fresh_args t ctxt 
+  apply_fresh_args trm ctxt 
    |> string_of_term ctxt
    |> tracing
 end"
@@ -544,13 +559,13 @@
   (fn x => x + 3)*}
 
 text {* 
-  which is the function composed of first the increment-by-one function and then
-  increment-by-two, followed by increment-by-three. Again, the reverse function 
-  composition allows you to read the code top-down. This combinator is often used
-  for setup function inside the \isacommand{setup}-command. These function have to be
-  of type @{ML_type "theory -> theory"} in order to install, for example, some new 
-  data inside the current theory. More than one such setup function can be composed 
-  with @{ML "#>"}. For example
+  which is the function composed of first the increment-by-one function and
+  then increment-by-two, followed by increment-by-three. Again, the reverse
+  function composition allows you to read the code top-down. This combinator
+  is often used for setup functions inside the
+  \isacommand{setup}-command. These functions have to be of type @{ML_type
+  "theory -> theory"}. More than one such setup function can be composed with
+  @{ML "#>"}. For example
 *}
 
 setup %gray {* let
@@ -624,7 +639,7 @@
   intermediate values in functions that return pairs. As an example, suppose you
   want to separate a list of integers into two lists according to a
   treshold. If the treshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
-  should be separated to @{ML "([1,2,3,4], [6,5])"}.  This function can be
+  should be separated as @{ML "([1,2,3,4], [6,5])"}.  Such a function can be
   implemented as
 *}
 
@@ -638,8 +653,8 @@
 
 text {*
   where the return value of the recursive call is bound explicitly to
-  the pair @{ML "(los, grs)" for los grs}. You can implement this function
-  more concisely as
+  the pair @{ML "(los, grs)" for los grs}. However, this function
+  can be implemented more concisely as
 *}
 
 ML{*fun separate i [] = ([], [])
@@ -721,8 +736,8 @@
   sometimes necessary to do some ``plumbing'' in order to fit functions
   together. We have already seen such plumbing in the function @{ML
   apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
-  list_comb}, which works over pairs to fit with the combinator @{ML "|>"}. Such 
-  plumbing is also needed in situations where a function operate over lists, 
+  list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such 
+  plumbing is also needed in situations where a function operates 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 simultaneously type-check 
   a list of terms. Consider the code:
@@ -811,27 +826,48 @@
 ML{*fun not_current_thyname () = Context.theory_name @{theory} *}
 
 text {*
-
   does \emph{not} return the name of the current theory, if it is run in a 
   different theory. Instead, the code above defines the constant function 
   that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
   function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
   \emph{not} replaced with code that will look up the current theory in 
   some data structure and return it. Instead, it is literally
-  replaced with the value representing the theory name.
+  replaced with the value representing the theory.
+
+  Another important antiquotation is @{text "@{context}"}. (What the
+  difference between a theory and a context is will be described in Chapter
+  \ref{chp:advanced}.) A context is for example needed in order to use the
+  function @{ML print_abbrevs in ProofContext} that list of all currently
+  defined abbreviations.
 
-  In a similar way you can use antiquotations to refer to proved theorems: 
+  @{ML_response_fake [display, gray]
+  "ProofContext.print_abbrevs @{context}"
+"Code_Evaluation.valtermify \<equiv> \<lambda>x. (x, \<lambda>u. Code_Evaluation.termify x)
+INTER \<equiv> INFI
+Inter \<equiv> Inf
+\<dots>"}
+
+  You can also use antiquotations to refer to proved theorems: 
   @{text "@{thm \<dots>}"} for a single theorem
 
   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 
   and @{text "@{thms \<dots>}"} for more than one
 
-@{ML_response_fake [display,gray] "@{thms conj_ac}" 
+@{ML_response_fake [display,gray] 
+  "@{thms conj_ac}" 
 "(?P \<and> ?Q) = (?Q \<and> ?P)
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 ((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
 
+  The thm-antiquotations can also be used for manipulating theorems. For 
+  example, if you need the version of te theorem @{thm [source] refl} that 
+  has a meta-equality instead of an equality, you can write
+
+@{ML_response_fake [display,gray] 
+  "@{thm refl[THEN eq_reflection]}"
+  "?x \<equiv> ?x"}
+
   The point of these antiquotations is that referring to theorems in this way
   makes your code independent from what theorems the user might have stored
   under this name (this becomes especially important when you deal with
@@ -848,9 +884,9 @@
   The result can be printed out as follows.
 
   @{ML_response_fake [gray,display]
-"foo_thm |> string_of_thms @{context}
+"foo_thm |> string_of_thms_no_vars @{context}
         |> tracing"
-  "True, True"}
+  "True, False \<Longrightarrow> P"}
 
   You can also refer to the current simpset via an antiquotation. To illustrate 
   this we implement the function that extracts the theorem names stored in a 
@@ -866,7 +902,7 @@
 
 text {*
   The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing all
-  information stored in the simpset, but we are only interested in the names of the
+  information stored in the simpset, but here we are only interested in the names of the
   simp-rules. Now you can feed in the current simpset into this function. 
   The current simpset can be referred to using the antiquotation @{text "@{simpset}"}.
 
@@ -878,43 +914,6 @@
   of lemmas to the simpset by the user, which can potentially cause loops in your
   code.
 
-  On the ML-level of Isabelle, you often have to work with qualified names.
-  These are strings with some additional information, such as positional
-  information and qualifiers. Such qualified names can be generated with the
-  antiquotation @{text "@{binding \<dots>}"}. For example
-
-  @{ML_response [display,gray]
-  "@{binding \"name\"}"
-  "name"}
-
-  An example where a qualified name is needed is the function 
-  @{ML_ind define in Local_Theory}.  This function is used below to define 
-  the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
-*}
-
-local_setup %gray {* 
-  Local_Theory.define ((@{binding "TrueConj"}, NoSyn), 
-      (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
-
-text {* 
-  Now querying the definition you obtain:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{text "TrueConj_def"}\\
-  @{text "> "}~@{thm TrueConj_def}
-  \end{isabelle}
-
-  \begin{readmore}
-  The basic operations on bindings are implemented in 
-  @{ML_file "Pure/General/binding.ML"}.
-  \end{readmore}
-
-  \footnote{\bf FIXME give a better example why bindings are important}
-  \footnote{\bf FIXME give a pointer to \isacommand{local\_setup}; if not, then explain
-  why @{ML snd} is needed.}
-  \footnote{\bf FIXME: There should probably a separate section on binding, long-names
-  and sign.}
-
   It is also possible to define your own antiquotations. But you should
   exercise care when introducing new ones, as they can also make your code
   also difficult to read. In the next chapter we describe how to construct
@@ -1202,7 +1201,7 @@
    fun init _ = [])*}
 
 text {*
-  The function we have to specify has to produce a list once a context 
+  The init-function we have to specify must produce a list for when a context 
   is initialised (possibly taking the theory into account from which the 
   context is derived). We choose here to just return the empty list. Next 
   we define two auxiliary functions for updating the list with a given
@@ -1239,11 +1238,11 @@
 2, 1"}
 
   Many functions in Isabelle manage and update data in a similar
-  fashion. Consequently, such calculation with contexts occur frequently in
+  fashion. Consequently, such calculations with contexts occur frequently in
   Isabelle code, although the ``context flow'' is usually only linear.
   Note also that the calculation above has no effect on the underlying
   theory. Once we throw away the contexts, we have no access to their
-  associated data. This is different to theories, where the command 
+  associated data. This is different for theories, where the command 
   \isacommand{setup} registers the data with the current and future 
   theories, and therefore one can access the data potentially 
   indefinitely.




