# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1281696178 -28800
# Node ID 4c32349b9875904fc023ae49c4b7012eb14ab29b
# Parent  2f39df9ceb6328696e598a18294668a8e9c6486a
added an example to be used for conversions later on

diff -r 2f39df9ceb63 -r 4c32349b9875 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/Essential.thy	Fri Aug 13 18:42:58 2010 +0800
@@ -632,6 +632,14 @@
   number representing their sum.
   \end{exercise}
 
+  \begin{exercise}\label{fun:makelist}
+  Write a function that takes an integer @{text i} and
+  produces an Isabelle integer list from @{text 1} upto @{text i}, 
+  and then builds the reverse of this list using @{const rev}. 
+  The relevant helper functions are @{ML upto}, 
+  @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}.
+  \end{exercise}
+
   \begin{exercise}\label{ex:debruijn}
   Implement the function, which we below name deBruijn, that depends on a natural
   number n$>$0 and constructs terms of the form:
diff -r 2f39df9ceb63 -r 4c32349b9875 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/First_Steps.thy	Fri Aug 13 18:42:58 2010 +0800
@@ -250,11 +250,12 @@
   "\"1\""}
 
   If there is more than one term to be printed, you can use the 
-  function @{ML_ind enum in Pretty} and commas to separate them.
+  function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 
+  to separate them.
 *} 
 
 ML{*fun pretty_terms ctxt ts =  
-  Pretty.enum "," "" "" (map (pretty_term ctxt) ts)*}
+  Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*}
 
 text {*
   You can also print out terms together with their typing information.
@@ -299,11 +300,11 @@
 text {*
   Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
   term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can be
-  printed again with @{ML enum in Pretty}.
+  printed again with @{ML commas in Pretty}.
 *} 
 
 ML{*fun pretty_cterms ctxt cts =  
-  Pretty.enum "," "" "" (map (pretty_cterm ctxt) cts)*}
+  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) cts))*}
 
 text {*
   The easiest way to get the string of a theorem is to transform it
@@ -352,24 +353,26 @@
 *}
 
 ML{*fun pretty_thms ctxt thms =  
-  Pretty.enum "," "" "" (map (pretty_thm ctxt) thms)
+  Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
 
 fun pretty_thms_no_vars ctxt thms =  
-  Pretty.enum "," "" "" (map (pretty_thm_no_vars ctxt) thms)*}
+  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
 
 text {*
   The printing functions for types are
 *}
 
 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
-fun pretty_typs ctxt tys = Pretty.commas (map (pretty_typ ctxt) tys)*}
+fun pretty_typs ctxt tys = 
+  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
 
 text {*
   respectively ctypes
 *}
 
 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
-fun pretty_ctyps ctxt ctys = Pretty.commas (map (pretty_ctyp ctxt) ctys)*}
+fun pretty_ctyps ctxt ctys = 
+  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
 
 text {*
   \begin{readmore}
diff -r 2f39df9ceb63 -r 4c32349b9875 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/Solutions.thy	Fri Aug 13 18:42:58 2010 +0800
@@ -35,6 +35,15 @@
 ML{*fun make_sum t1 t2 =
       HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
+
+text {* \solution{fun:makelist} *}
+
+ML{*fun mk_rev_upto i = 
+  1 upto i
+  |> map (HOLogic.mk_number @{typ int})
+  |> HOLogic.mk_list @{typ int}
+  |> curry (op $) @{term "rev :: int list \<Rightarrow> int list"}*}
+
 text {* \solution{ex:debruijn} *}
 
 ML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
diff -r 2f39df9ceb63 -r 4c32349b9875 progtutorial.pdf
Binary file progtutorial.pdf has changed