--- a/ProgTutorial/FirstSteps.thy	Tue Oct 13 22:57:25 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Oct 14 02:32:53 2009 +0200
@@ -17,7 +17,7 @@
   {\em
   ``We will most likely never realize the full importance of painting the Tower,\\ 
   that it is the essential element in the conservation of metal works and the\\ 
-  more meticulous the paint job, the longer the Tower shall endure.''} \\[1ex]
+  more meticulous the paint job, the longer the tower shall endure.''} \\[1ex]
   Gustave Eiffel, In his book {\em The 300-Meter Tower}.\footnote{The Eiffel Tower has been 
   re-painted 18 times since its initial construction, an average of once every 
   seven years. It takes more than a year for a team of 25 painters to paint the tower 
@@ -214,7 +214,7 @@
 *)
 
 text {*
-  Most often you want to inspect data of Isabelle's most basic data
+  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
@@ -1045,11 +1045,11 @@
 
 text {*
   which takes an integer and adds it to the content of the reference.
-  As above we update the reference with the command 
+  As done above, we update the reference with the command 
   \isacommand{setup}. 
 *}
 
-setup %gray{* ref_update 1 *}
+setup %gray {* ref_update 1 *}
 
 text {*
   A lookup in the current theory gives then the expected list 
@@ -1059,13 +1059,13 @@
   "WrongRefData.get @{theory}"
   "ref [1]"}
 
-  So far everything is as expected. But, the trouble starts if we attempt
-  to backtrack to ``before'' the \isacommand{setup}-command. There, we 
-  would expect that the list is empty again. But since it is stored in 
-  a reference, Isabelle has no control over it. So it is not
-  empty, but still @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, 
-  if we execute the \isacommand{setup}-command again, we do not obtain 
-  @{ML "ref [1]" in Unsynchronized}, but
+  So far everything is as expected. But, the trouble starts if we attempt to
+  backtrack to the point ``before'' the \isacommand{setup}-command. There, we
+  would expect that the list is empty again. But since it is stored in a
+  reference, Isabelle has no control over it. So it is not empty, but still
+  @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
+  \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
+  Unsynchronized}, but
 
   @{ML_response_fake [display,gray]
   "WrongRefData.get @{theory}"
@@ -1080,7 +1080,7 @@
   The functors for data storage are defined in @{ML_file "Pure/context.ML"}.
   Isabelle contains implementations of several container data structures,
   including association lists in @{ML_file "Pure/General/alist.ML"},
-  directed graphs in @{ML_file "Pure/General/graph.ML"}. and 
+  directed graphs in @{ML_file "Pure/General/graph.ML"}, and 
   tables and symtables in @{ML_file "Pure/General/table.ML"}.
   \end{readmore}
 
@@ -1114,16 +1114,16 @@
 
   @{ML_response_fake [display,gray]
 "let
-  val ctxt    = @{context}
-  val ctxt'   = ctxt   |> update @{term \"False\"}
-                       |> update @{term \"True \<and> True\"} 
-  val ctxt''  = ctxt   |> update @{term \"1::nat\"}
-  val ctxt''' = ctxt'' |> update @{term \"2::nat\"}
+  val ctxt0 = @{context}
+  val ctxt1 = ctxt0 |> update @{term \"False\"}
+                    |> update @{term \"True \<and> True\"} 
+  val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
+  val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
 in
-  print ctxt; 
-  print ctxt';
-  print ctxt'';
-  print ctxt'''
+  print ctxt0; 
+  print ctxt1;
+  print ctxt2;
+  print ctxt3
 end"
 "Empty!
 True \<and> True, False
@@ -1138,8 +1138,7 @@
   associated data. This is different to theories, where the command 
   \isacommand{setup} registers the data with the current and future 
   theories, and therefore one can access the data potentially 
-  indefinitely.\footnote{\bf FIXME: check this; it seems that is in
-  conflict with the statements below.} 
+  indefinitely.
 
   For convenience there is an abstract layer, the type @{ML_type Context.generic}, 
   for theories and proof contexts. This type is defined as follows
@@ -1199,18 +1198,24 @@
   On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
 *} 
 
-setup %gray {* 
-  Context.theory_map (FooRules.add_thm @{thm TrueI}) 
-*}
+setup %gray {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *}
 
 text {*
   The rules in the list can be retrieved using the function 
   @{ML FooRules.get}:
 
-  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"True\", \"?C\",\"?B\"]"}
+  @{ML_response_fake [display,gray] 
+  "FooRules.get @{context}" 
+  "[\"True\", \"?C\",\"?B\"]"}
+
+  Note that this function takes a proof context as argument. This might be 
+  confusing, since the theorem list is stored as theory data. The proof context 
+  however conatains the information about the current theory and so the function
+  can access the theorem list in the theory via the context. 
 
   \begin{readmore}
-  For more information see @{ML_file "Pure/Tools/named_thms.ML"}.
+  For more information about named theorem lists see 
+  @{ML_file "Pure/Tools/named_thms.ML"}.
   \end{readmore}
 
   The second special instance of the data storage mechanism are configuration
@@ -1251,24 +1256,25 @@
   "Config.get @{context} bval" 
   "true"}
 
-  or from a theory using the function @{ML_ind get_thy in Config}
+  or directly from a theory using the function @{ML_ind get_thy in Config}
 
   @{ML_response [display,gray] 
   "Config.get_thy @{theory} bval" 
   "true"}
 
   It is also possible to manipulate the configuration values
-  from the ML-level with the function @{ML_ind put in Config}
-  or @{ML_ind put_thy in Config}. For example
+  from the ML-level with the functions @{ML_ind put in Config}
+  and @{ML_ind put_thy in Config}. For example
 
   @{ML_response [display,gray]
   "let
   val ctxt = @{context}
   val ctxt' = Config.put sval \"foo\" ctxt
+  val ctxt'' = Config.put sval \"bar\" ctxt'
 in
-  (Config.get ctxt sval, Config.get ctxt' sval)
+  (Config.get ctxt sval, Config.get ctxt' sval, Config.get ctxt'' sval)
 end"
-  "(\"some string\", \"foo\")"}
+  "(\"some string\", \"foo\", \"bar\")"}
 
   \begin{readmore}
   For more information about configuration values see 
@@ -1287,9 +1293,13 @@
   contains mechanisms for storing arbitrary data in theory and proof 
   contexts.
 
-  This chapter also mentions two coding conventions: namely printing
-  entities belonging together as one string, and not using references
-  in any Isabelle code.
+  \begin{conventions}
+  \begin{itemize}
+  \item Print messages that belong together as a single string.
+  \item Do not use references in any Isabelle code.
+  \end{itemize}
+  \end{conventions}
+
 *}
 
 

--- a/ProgTutorial/General.thy	Tue Oct 13 22:57:25 2009 +0200
+++ b/ProgTutorial/General.thy	Wed Oct 14 02:32:53 2009 +0200
@@ -11,7 +11,7 @@
 (*>*)
 
 
-chapter {* Isabelle in More Detail \mbox{or, the Good, the Bad and the Ugly} *}
+chapter {* Isabelle in More Detail *}
 
 text {*
   Isabelle is build around a few central ideas. One central idea is the
@@ -693,7 +693,7 @@
   val zero = @{term \"0::nat\"}
 in
   cterm_of @{theory} 
-      (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
+      (Const (@{const_name plus}, [natT, natT] ---> natT) $ zero $ zero)
 end" "0 + 0"}
 
   In Isabelle not just terms need to be certified, but also types. For example, 
@@ -779,7 +779,8 @@
   final statement of the theorem.
 
   @{ML_response_fake [display, gray]
-  "string_of_thm @{context} my_thm |> tracing"
+  "string_of_thm @{context} my_thm 
+|> tracing"
   "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 
   However, internally the code-snippet constructs the following 
@@ -811,24 +812,26 @@
 text {*
   The first argument @{ML_ind theoremK in Thm} is a kind indicator, which
   classifies the theorem. For a theorem arising from a definition we should
-  state @{ML_ind definitionK in Thm}, instead. The second argument is the 
-  name under which we store the theorem or theorems. The third can contain 
-  a list of (theorem) attributes. Above it is empty, but if we want to store
-  the theorem and at the same time add it to the simpset we have to declare:
+  use @{ML_ind definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, for
+  ``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
+  in Thm}.  The second argument is the name under which we store the theorem
+  or theorems. The third can contain a list of (theorem) attributes. We will
+  explain them in detail in Section~\ref{sec:attributes}. Below we
+  use such an attribute in order add the theorem to the simpset. 
+  have to declare:
 *}
 
 local_setup %gray {*
   LocalTheory.note Thm.theoremK
-     ((@{binding "my_thm_simp"}, 
-          [Attrib.internal (K Simplifier.simp_add)]), 
-             [my_thm]) #> snd *}
+    ((@{binding "my_thm_simp"}, 
+       [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
 
 text {*
   Note that we have to use another name for the theorem, since Isabelle does
-  not allow to add another theorem under the same name.  The attribute can be
-  given @{ML_ind internal in Attrib}. If we use the function @{ML
-  get_thm_names_from_ss} from the previous chapter, we can check whether the
-  theorem has been added.
+  not allow to store another theorem under the same name. The attribute needs to
+  be wrapped inside the function @{ML_ind internal in Attrib}. If we use the 
+  function @{ML get_thm_names_from_ss} from the previous chapter, we can check 
+  whether the theorem has actually been added.
 
   @{ML_response [display,gray]
   "let
@@ -838,20 +841,23 @@
 end"
   "true"}
 
-  Now the theorems @{thm [source] my_thm} and @{thm [source] my_thm_simp} can 
-  also be referenced  with the \isacommand{thm}-command on the user-level of 
-  Isabelle
+  The main point of storing the theorems @{thm [source] my_thm} and @{thm
+  [source] my_thm_simp} is that they can now also be referenced with the
+  \isacommand{thm}-command on the user-level of Isabelle
+
 
   \begin{isabelle}
   \isacommand{thm}~@{text "my_thm"}\isanewline
    @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
   \end{isabelle}
 
-  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Note that the
-  theorem does not have any meta-variables that would be present if we proved
-  this theorem on the user-level. As we shall see later on, we have to construct
-  meta-variables explicitly.
+  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. As can be seen
+  the theorem does not have any meta-variables that would be present if we proved
+  this theorem on the user-level. We will see later on, we have to construct
+  meta-variables in a theorem explicitly.
+*}
 
+text {*
   There is a multitude of functions that manage or manipulate theorems. For example 
   we can test theorems for (alpha) equality. Suppose you proved the following three 
   facts.
@@ -922,6 +928,16 @@
   @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}. 
   \end{readmore}
 
+  The simplifier can be used to unfold definition in theorms. To show
+  this we build the theorem @{term "True \<equiv> True"} (Line 1) and then 
+  unfold the constant according to its definition (Line 2).
+
+  @{ML_response_fake [display,gray,linenos]
+  "Thm.reflexive @{cterm \"True\"}
+  |> Simplifier.rewrite_rule [@{thm True_def}]
+  |> string_of_thm @{context}
+  |> tracing"
+  "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
 
   Often it is necessary to transform theorems to and from the object 
   logic.  For example, the function @{ML_ind rulify in ObjectLogic}
@@ -946,10 +962,32 @@
 
   In this code the function @{ML atomize in ObjectLogic} produces 
   a meta-equation between the given theorem and the theorem transformed
-  into the object logic. The function @{ML_ind rewrite_rule in MetaSimplifier}
-  unfolds this meta-equation in the given theorem. The result is
-  the theorem with object logic connectives.
-x
+  into the object logic. The result is the theorem with object logic 
+  connectives. However, in order to completely transform a theorem
+  such as @{thm [source] list.induct}
+
+  @{thm [display] list.induct}
+
+  we have to first abstract over the variables @{text "?P"} and 
+  @{text "?list"}. For this we can use the function 
+  @{ML_ind forall_intr_vars in Drule}. 
+*}
+
+ML{*fun atomize_thm thm =
+let
+  val thm' = forall_intr_vars thm
+  val thm'' = ObjectLogic.atomize (cprop_of thm')
+in
+  MetaSimplifier.rewrite_rule [thm''] thm'
+end*}
+
+text {*
+  For @{thm [source] list.induct} it produces:
+
+  @{ML_response_fake [display, gray]
+  "atomize_thm @{thm list.induct}"
+  "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
+
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achive this is by using the function @{ML_ind prove in Goal}. 
   For example

--- a/ProgTutorial/document/root.tex	Tue Oct 13 22:57:25 2009 +0200
+++ b/ProgTutorial/document/root.tex	Wed Oct 14 02:32:53 2009 +0200
@@ -74,6 +74,8 @@
 
 \newenvironment{readmore}%
 {\begin{leftrightbar}\small\it{\textbf{Read More}}\\}{\end{leftrightbar}}
+\newenvironment{conventions}%
+{\begin{leftrightbar}\small\it{\textbf{Coding Conventions}}}{\end{leftrightbar}}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % some mathematical notation
 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}

Binary file progtutorial.pdf has changed