--- a/ProgTutorial/Advanced.thy	Thu Nov 19 17:48:44 2009 +0100
+++ b/ProgTutorial/Advanced.thy	Thu Nov 19 20:00:10 2009 +0100
@@ -227,6 +227,8 @@
   @{ML_ind fork_pri in Future}
 *}
 
+section {* Parse and Print Translations (TBD) *}
+
 section {* Summary *}
 
 text {*

--- a/ProgTutorial/Base.thy	Thu Nov 19 17:48:44 2009 +0100
+++ b/ProgTutorial/Base.thy	Thu Nov 19 20:00:10 2009 +0100
@@ -8,7 +8,6 @@
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-
 (* rebinding of writeln and tracing so that it can *)
 (* be compared in intiquotations                   *)
 ML {* 
@@ -141,6 +140,19 @@
          IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
 *}
 
+ML {*
+fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
+
+fun rhs 1 = P 1
+  | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
+
+fun lhs 1 n = HOLogic.mk_imp (HOLogic.mk_eq (P 1, P n), rhs n)
+  | lhs m n = HOLogic.mk_conj (HOLogic.mk_imp 
+                 (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
+
+fun de_bruijn n =
+  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
+*}
 
 use "output_tutorial.ML"
 use "antiquote_setup.ML"

--- a/ProgTutorial/Essential.thy	Thu Nov 19 17:48:44 2009 +0100
+++ b/ProgTutorial/Essential.thy	Thu Nov 19 20:00:10 2009 +0100
@@ -1341,15 +1341,10 @@
   Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 
 text {*
-  The fourth argument of @{ML note in Local_Theory} is the list of theorems we
+  The third argument of @{ML note in Local_Theory} is the list of theorems we
   want to store under a name. We can store more than one under a single name. 
-  The first argument @{ML_ind theoremK in Thm} is
-  a kind indicator, which classifies the theorem. There are several such kind
-  indicators: for a theorem arising from a definition you should use @{ML_ind
-  definitionK in Thm}, and for
-  ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
-  in Thm}.  The second argument of @{ML note in Local_Theory} is the name under
-  which we store the theorem or theorems. The third argument can contain a
+  The first argument of @{ML note in Local_Theory} is the name under
+  which we store the theorem or theorems. The second argument can contain a
   list of theorem attributes, which we will explain in detail in
   Section~\ref{sec:attributes}. Below we just use one such attribute for
   adding the theorem to the simpset:
@@ -1900,13 +1895,16 @@
 *}
 
 ML{*fun MY_THEN thms = 
-  Thm.rule_attribute 
-    (fn _ => fn thm => fold (curry ((op RS) o swap)) thms thm)*}
+let
+  fun RS_rev thm1 thm2 = thm2 RS thm1
+in
+  Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
+end*}
 
 text {* 
-  where @{ML swap} swaps the components of a pair. The setup of this theorem
-  attribute uses the parser @{ML thms in Attrib}, which parses a list of
-  theorems. 
+  where for convenience we define the reverse and curried version of @{ML RS}. 
+  The setup of this theorem attribute uses the parser @{ML thms in Attrib}, 
+  which parses a list of theorems. 
 *}
 
 attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} 
@@ -2023,6 +2021,7 @@
   have to change the parser for reading the arguments accordingly.
 
   \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
+  \footnote{\bf FIXME readmore}
 
   \begin{readmore}
   FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in 
@@ -2220,42 +2219,20 @@
 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
 28"}
 
-  Next we like to pretty-print a term and its type. For this we use the
-  function @{text "tell_type"}.
-*}
-
-ML %linenosgray{*fun tell_type ctxt t = 
-let
-  fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
-  val ptrm = Pretty.quote (Syntax.pretty_term ctxt t)
-  val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of t))
-in
-  pprint (Pretty.blk (0, 
-    (pstr "The term " @ [ptrm] @ pstr " has type " 
-      @ [pty, Pretty.str "."])))
-end*}
-
-text {*
-  In Line 3 we define a function that inserts possible linebreaks in places
-  where a space is. In Lines 4 and 5 we pretty-print the term and its type
-  using the functions @{ML_ind  pretty_term in Syntax} and @{ML_ind 
-  pretty_typ in Syntax}. We also use the function @{ML_ind quote in
-  Pretty} in order to enclose the term and type inside quotation marks. In
-  Line 9 we add a period right after the type without the possibility of a
-  line break, because we do not want that a line break occurs there.
-  Now you can write
+  Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
+  a list of items, but automatically inserts forced breaks between each item.
+  Compare
 
   @{ML_response_fake [display,gray]
-  "tell_type @{context} @{term \"min (Suc 0)\"}"
-  "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
-  
-  To see the proper line breaking, you can try out the function on a bigger term 
-  and type. For example:
-
-  @{ML_response_fake [display,gray]
-  "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
-  "The term \"op = (op = (op = (op = (op = op =))))\" has type 
-\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
+  "let
+  val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
+in
+  pprint (Pretty.blk (0, a_and_b));
+  pprint (Pretty.chunks a_and_b)
+end"
+"ab
+a
+b"}
 
   The function @{ML_ind big_list in Pretty} helps with printing long lists.
   It is used for example in the command \isacommand{print\_theorems}. An
@@ -2276,24 +2253,56 @@
   9
   10"}
 
-  Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
-  a list of items, but automatically inserts forced breaks between each item.
-  Compare
+  The point of the pretty-printing functions is to conveninetly obtain 
+  a lay-out of terms and types that is pleasing to the eye. If we print
+  out the the terms produced by the the function @{ML de_bruijn} from 
+  exercise~\ref{ex:debruijn} we obtain the following: 
 
   @{ML_response_fake [display,gray]
-  "let
-  val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
+  "pprint (Syntax.pretty_term  @{context} (de_bruijn 4))"
+  "(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
+(P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
+(P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and> 
+(P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
+P 4 \<and> P 3 \<and> P 2 \<and> P 1"}
+
+  We use the function @{ML_ind pretty_term in Syntax} for pretty-printing
+  terms. Next we like to pretty-print a term and its type. For this we use the
+  function @{text "tell_type"}.
+*}
+
+ML %linenosgray{*fun tell_type ctxt trm = 
+let
+  fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
+  val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm)
+  val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of trm))
 in
-  pprint (Pretty.blk (0, a_and_b));
-  pprint (Pretty.chunks a_and_b)
-end"
-"ab
-a
-b"}
+  pprint (Pretty.blk (0, 
+    (pstr "The term " @ [ptrm] @ pstr " has type " 
+      @ [pty, Pretty.str "."])))
+end*}
+
+text {*
+  In Line 3 we define a function that inserts possible linebreaks in places
+  where a space is. In Lines 4 and 5 we pretty-print the term and its type
+  using the functions @{ML pretty_term in Syntax} and @{ML_ind 
+  pretty_typ in Syntax}. We also use the function @{ML_ind quote in
+  Pretty} in order to enclose the term and type inside quotation marks. In
+  Line 9 we add a period right after the type without the possibility of a
+  line break, because we do not want that a line break occurs there.
+  Now you can write
+
+  @{ML_response_fake [display,gray]
+  "tell_type @{context} @{term \"min (Suc 0)\"}"
+  "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
   
-  \footnote{\bf FIXME: What happens with printing big formulae?}
+  To see the proper line breaking, you can try out the function on a bigger term 
+  and type. For example:
 
-  
+  @{ML_response_fake [display,gray]
+  "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
+  "The term \"op = (op = (op = (op = (op = op =))))\" has type 
+\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
 
   \begin{readmore}
   The general infrastructure for pretty-printing is implemented in the file
@@ -2304,47 +2313,6 @@
   \end{readmore}
 *}
 
-(*
-text {*
-  printing into the goal buffer as part of the proof state
-*}
-
-text {* writing into the goal buffer *}
-
-ML {* fun my_hook interactive state =
-         (interactive ? Proof.goal_message (fn () => Pretty.str  
-"foo")) state
-*}
-
-setup %gray {* Context.theory_map (Specification.add_theorem_hook my_hook) *}
-
-lemma "False"
-oops
-*)
-
-(*
-ML {*
-fun setmp_show_all_types f =
-   setmp show_all_types
-         (! show_types orelse ! show_sorts orelse ! show_all_types) f;
-
-val ctxt = @{context};
-val t1 = @{term "undefined::nat"};
-val t2 = @{term "Suc y"};
-val pty =        Pretty.block (Pretty.breaks
-             [(setmp show_question_marks false o setmp_show_all_types)
-                  (Syntax.pretty_term ctxt) t1,
-              Pretty.str "=", Syntax.pretty_term ctxt t2]);
-pty |> Pretty.string_of  
-*}
-
-text {* the infrastructure of Syntax-pretty-term makes sure it is printed nicely  *}
-
-
-ML {* Pretty.mark Markup.hilite (Pretty.str "foo") |> Pretty.string_of  |> tracing *}
-ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
-*)
-
 section {* Summary *}
 
 text {*

Binary file progtutorial.pdf has changed