
diff -r ed797395fab6 -r 007922777ff1 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Sun Aug 16 22:14:36 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Aug 17 20:57:32 2009 +0200
@@ -1,7 +1,10 @@
 theory FirstSteps
 imports Base
+uses "FirstSteps.ML"
 begin
 
+
+
 chapter {* First Steps *}
 
 text {*
@@ -165,7 +168,7 @@
   will cause that all tracing information is printed into the file @{text "foo.bar"}.
 
   You can print out error messages with the function @{ML [index] error}; for 
-  example:\footnote{FIXME: unwanted pagebreak}
+  example:
 
 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" 
 "Exception- ERROR \"foo\" raised
@@ -194,46 +197,60 @@
 *)
 
 text {*
-  Most often you want to inspect data of Isabelle's most basic datastructures,
-  namely @{ML_type term}, @{ML_type cterm} or @{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 far too
-  unwieldy. One way to transform a term into a string is to use the function
-  @{ML [index] string_of_term in Syntax}.
-
+  Most often you want to inspect data of Isabelle's most basic data
+  structures, namely @{ML_type term}, @{ML_type cterm} or @{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 [index] string_of_term in Syntax} in structure @{ML_struct
+  Syntax}, which we bind for more convenience to the toplevel.
+*}
+
+ML{*val string_of_term = Syntax.string_of_term*}
+
+text {*
+  It can now be used as follows
 
   @{ML_response_fake [display,gray]
-  "Syntax.string_of_term @{context} @{term \"1::nat\"}"
+  "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 with some additional information encoded in it. The string
-  can be properly printed by using either the function @{ML [index] writeln} or 
-  @{ML [index] tracing}:
+  This produces a string corrsponding to the term @{term [show_types] "1::nat"} with some
+  additional information encoded in it. The string can be properly printed by
+  using either the function @{ML [index] writeln} or @{ML [index] tracing}:
 
   @{ML_response_fake [display,gray]
-  "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+  "writeln (string_of_term @{context} @{term \"1::nat\"})"
   "\"1\""}
 
   or
 
   @{ML_response_fake [display,gray]
-  "tracing (Syntax.string_of_term @{context} @{term \"1::nat\"})"
+  "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 
+  function @{ML [index] commas} to separate them.
+*} 
+
+ML{*fun string_of_terms ctxt ts =  
+  commas (map (string_of_term ctxt) ts)*}
+
+text {*
   A @{ML_type cterm} can be transformed into a string by the following function.
 *}
 
 ML{*fun string_of_cterm ctxt t =  
-  Syntax.string_of_term ctxt (term_of t)*}
+  string_of_term ctxt (term_of t)*}
 
 text {*
   In this example the function @{ML [index] term_of} extracts the @{ML_type term} from
-  a @{ML_type cterm}.  If there are more than one @{ML_type cterm}s to be
-  printed, you can use the function @{ML [index] commas} to separate them.
+  a @{ML_type cterm}.  More than one @{ML_type cterm}s can again be printed
+  with @{ML [index] commas}.
 *} 
 
-ML{*fun string_of_cterms ctxt ts =  
-  commas (map (string_of_cterm ctxt) ts)*}
+ML{*fun string_of_cterms ctxt cts =  
+  commas (map (string_of_cterm ctxt) cts)*}
 
 text {*
   The easiest way to get the string of a theorem is to transform it
@@ -251,10 +268,10 @@
   "tracing (string_of_thm @{context} @{thm conjI})"
   "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 
-  In order to improve the readability of theorems we convert
-  these schematic variables into free variables using the 
-  function @{ML [index] import in Variable}. This is similar
-  to the attribute @{text "[no_vars]"} from Isabelle's user-level.
+  In order to improve the readability of theorems we convert these schematic
+  variables into free variables using the function @{ML [index] import in
+  Variable}. This is similar to the theorem attribute @{text "[no_vars]"} from
+  Isabelle's user-level.
 *}
 
 ML{*fun no_vars ctxt thm =
@@ -409,7 +426,7 @@
   val ctxt = @{context}
 in 
   apply_fresh_args t ctxt
-   |> Syntax.string_of_term ctxt
+   |> string_of_term ctxt
    |> tracing
 end" 
   "P z za zb"}
@@ -434,7 +451,7 @@
   val ctxt = @{context}
 in
   apply_fresh_args t ctxt 
-   |> Syntax.string_of_term ctxt
+   |> string_of_term ctxt
    |> tracing
 end"
   "za z zb"}
@@ -599,20 +616,59 @@
             (fn x => (x, x))
         #-> (fn x => fn y => x + y)*}
 
+
+text {* 
+  When using combinators for writing function in waterfall fashion, it is
+  sometimes necessary to do some ``plumbing'' for fitting 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} that works over pairs to fit with the combinator @{ML "|>"}. Such 
+  plumbing is also needed in situations where a functions operate over lists, 
+  but one calculates only with a single entity. An example is the function 
+  @{ML [index] check_terms in Syntax}, whose purpose is to type-check a list 
+  of terms.
+
+  @{ML_response_fake [display, gray]
+  "let
+  val ctxt = @{context}
+in
+  map (Syntax.parse_term ctxt) [\"m + n\", \"m - (n::nat)\"] 
+  |> Syntax.check_terms ctxt
+  |> string_of_terms ctxt
+  |> tracing
+end"
+  "m + n, m - n"}
+*}
+
 text {*
-  
-  (FIXME: find a good exercise for combinators)
-
+  In this example we obtain two terms with appropriate typing. However, if you
+  have only a single term, then @{ML check_terms in Syntax} needs to be
+  adapted. This can be done with the ``plumbing'' function @{ML
+  singleton}.\footnote{There is in fact alread a function @{ML check_term in Syntax},
+  which however is defined in terms of @{ML singleton} and @{ML check_terms in
+  Syntax}.} For example
+
+  @{ML_response_fake [display, gray]
+  "let 
+  val ctxt = @{context}
+in
+  Syntax.parse_term ctxt \"m - (n::nat)\" 
+  |> singleton (Syntax.check_terms ctxt)
+  |> string_of_term ctxt
+  |> tracing
+end"
+  "m - n"}
+   
   \begin{readmore}
   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}
- 
-  (FIXME: say something about calling conventions)
- 
-  (FIXME: say something about singleton)
+
+  (FIXME: find a good exercise for combinators)
+
+  (FIXME: say something about calling conventions) 
 *}
 
 
@@ -831,13 +887,10 @@
   val v2 = Var ((\"x1\", 3), @{typ bool})
   val v3 = Free (\"x\", @{typ bool})
 in
-  map (Syntax.string_of_term @{context}) [v1, v2, v3]
-  |> cat_lines
+  string_of_terms @{context} [v1, v2, v3]
   |> tracing
 end"
-"?x3
-?x1.3
-x"}
+"?x3, ?x1.3, x"}
 
   When constructing terms, you are usually concerned with free variables (as mentioned earlier,
   you cannot construct schematic variables using the antiquotation @{text "@{term \<dots>}"}). 
@@ -864,7 +917,7 @@
 "let
   val omega = Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})
 in 
-  tracing (Syntax.string_of_term @{context} omega)
+  tracing (string_of_term @{context} omega)
 end"
   "x x"}
 
@@ -1085,7 +1138,7 @@
   val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
 in 
   subst_bounds (rev vrs, trm) 
-  |> Syntax.string_of_term @{context}
+  |> string_of_term @{context}
   |> tracing
 end"
   "x = y"}
@@ -1104,7 +1157,7 @@
 "let
   val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
 in
-  tracing (Syntax.string_of_term @{context} eq)
+  tracing (string_of_term @{context} eq)
 end"
   "True = False"}
 *}
@@ -1516,7 +1569,7 @@
     then let val (params,t) = strip_assums_all([], nth prems (i - 1))
          in subst_bounds(map Free params, t) end
     else error ("Not enough premises for prem" ^ string_of_int i ^
-      " in propositon: " ^ Syntax.string_of_term ctxt t)
+      " in propositon: " ^ string_of_term ctxt t)
   end;
 *}
 




