--- a/ProgTutorial/FirstSteps.thy	Thu Oct 01 10:19:21 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Fri Oct 02 15:38:14 2009 +0200
@@ -187,8 +187,8 @@
   be displayed by the infrastructure.
 
 
-  (FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 
-  @{ML_ind  profiling in Toplevel}.)
+  \footnote{\bf FIXME Mention how to work with @{ML_ind  debug in Toplevel} and 
+  @{ML_ind  profiling in Toplevel}.}
 *}
 
 (* FIXME
@@ -610,7 +610,7 @@
   "acc_incs 1 ||>> (fn x => (x, x + 2))"
   "(((((\"\", 1), 2), 3), 4), 6)"}
 
-  (FIXME: maybe give a ``real world'' example for this combinator)
+  \footnote{\bf FIXME: maybe give a ``real world'' example for this combinator.}
 *}
 
 text {*
@@ -678,9 +678,9 @@
   contains further information about combinators.
   \end{readmore}
 
-  (FIXME: find a good exercise for combinators)
+  \footnote{\bf FIXME: find a good exercise for combinators}
 
-  (FIXME: say something about calling conventions) 
+  \footnote{\bf FIXME: say something about calling conventions} 
 *}
 
 
@@ -798,9 +798,9 @@
   @{text "> "}~@{thm TrueConj_def}
   \end{isabelle}
 
-  (FIXME give a better example why bindings are important; maybe
+  \footnote{\bf FIXME give a better example why bindings are important; maybe
   give a pointer to \isacommand{local\_setup}; if not, then explain
-  why @{ML snd} is needed)
+  why @{ML snd} is needed.}
 
   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
@@ -844,20 +844,32 @@
   \end{readmore}
 *}
 
-section {* Storing Data in Isabelle (TBD) *}
+section {* Storing Data in Isabelle *}
 
 text {*
-  Isabelle provides mechanisms to store (and retrieve) arbitrary data. Before we 
-  explain them, let us digress: Convenitional wisdom has it that 
-  ML's type-system ensures that for example an @{ML_type "'a list"} can only
-  hold elements of the same type, namely @{ML_type "'a"}. Still, by some arguably
-  accidental features of ML, one can implement a universal type. In Isabelle it
-  is implemented as @{ML_type Universal.universal}. This type allows one to
-  inject and project elements of different type into for example into a list.
-  We will show this by storing an integer and boolean in a list. What is important
-  that access to the data is done in a type-safe manner. 
+  Isabelle provides mechanisms for storing (and retrieving) arbitrary
+  data. Before we delve into the details, let us digress a bit. Conventional
+  wisdom has it that the type-system of ML ensures that for example an
+  @{ML_type "'a list"} can only hold elements of the same type, namely
+  @{ML_type "'a"}. Despite this wisdom, however, it is possible to implement a
+  universal type in ML, although by some arguably accidental features of ML.
+  This universal type can be used to store data of different type into a single list.
+  It allows one to inject and to project data of \emph{arbitrary} type. This is
+  in contrast to datatypes, which only allow injection and projection of data for
+  some fixed collection of types. In light of the conventional wisdom cited
+  above it is important to keep in mind that the universal type does not
+  destroy type-safety of ML: storing and accessing the data can only be done
+  in a type-safe manner.
 
-  Let us first define projection and injection functions for booleans and integers.
+  \begin{readmore}
+  In Isabelle the universal type is implemented as the type @{ML_type
+  Universal.universal} in the file
+  @{ML_file "Pure/ML-Systems/universal.ML"}.
+  \end{readmore}
+
+  We will show the usage of the universal type by storing an integer and
+  a boolean into a single list. Let us first define injection and projection 
+  functions for booleans and integers into and from @{ML_type Universal.universal}.
 *}
 
 ML{*local
@@ -871,34 +883,216 @@
 end*}
 
 text {*
-  We can now build a list injecting @{ML_text "13"} and @{ML_text "true"} as
-  its two elements.
-*}
-
-ML{* val list = [inject_int 13, inject_bool true]*}
-
-ML {*
- project_int (nth list 0)
+  Using the injection functions, we can inject the integer @{ML_text "13"} 
+  and the boolean @{ML_text "true"} into @{ML_type Universal.universal}, and
+  then store them in a @{ML_type "Universal.universal list"} as follows:
 *}
 
-ML {*
- project_bool (nth list 1)
+ML{*val foo_list = 
+let
+  val thirteen  = inject_int 13
+  val truth_val = inject_bool true
+in
+  [thirteen, truth_val]
+end*}
+
+text {*
+  The data can be retrieved using the projection functions.
+  
+  @{ML_response [display, gray]
+"(project_int (nth foo_list 0), project_bool (nth foo_list 1))" 
+"(13, true)"}
+
+  Notice that we access the integer as an integer and the boolean as
+  a boolean. If we attempt to access the integer as a boolean, then we get 
+  a runtime error. 
+  
+  @{ML_response_fake [display, gray]
+"project_bool (nth foo_list 0)"  
+"*** Exception- Match raised"}
+
+  This runtime error is the reason why ML is still type-sound despite
+  containing a universal type.
+
+  Now, Isabelle heavily uses this mechanism to store all sorts of data: theorem lists,
+  simpsets, facts etc.  Roughly speaking, there are two places where data can 
+  be stored: in \emph{theories} and in \emph{proof contexts}. Again
+  roughly speaking, data such as simpsets need to be stored in a theory,
+  since they need to be maintained across proofs and even theories.
+  On the other hands, data such as facts change inside a proof and
+  therefore need to be maintained inside a proof 
+  context.\footnote{\bf TODO: explain more bout this.} 
+
+  For both theories and proof contexts there are convenient functors that help
+  with the data storage. Below we show how to implement a table in which we
+  can store theorems that can be looked up according to a string key. The
+  intention is to be able to look up introduction rules for logical
+  connectives. Such a table might be useful in an automatic proof procedure
+  and therefore it makes sense to store this data inside a theory.  The code
+  for the table is:
 *}
 
-ML {* 
-  Context.the_thread_data ();
-  Context.display_names @{theory};
-  Context.pretty_thy @{theory}
-    |> Pretty.string_of
-    |> tracing
+ML %linenosgray{*structure Data = TheoryDataFun
+  (type T = thm Symtab.table
+   val empty = Symtab.empty
+   val copy = I
+   val extend = I
+   fun merge _ = Symtab.merge (K true))*}
+
+text {*
+  In order to store data in a theory, we have to specify the type of the data
+  (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"}, which 
+  stands for tables in which @{ML_type string}s can be looked up producing an associated
+  @{ML_type thm}. We also have to specify four functions: how to initialise
+  the data storage (Line 3), how to copy it (Line 4), how to extend it (Line
+  5) and how two tables should be merged (Line 6). These functions correspond
+  roughly to the operations performed on theories.\footnote{\bf FIXME: Say more
+  about the assumptions of these operations.} The result structure @{ML_text Data}
+  contains functions for accessing the table (@{ML Data.get}) and for updating
+  it (@{ML Data.map}). There are also two more functions, which however we
+  ignore here. Below we define two auxiliary functions, which help us with
+  accessing the table.
+*}
+
+ML{*val lookup = Symtab.lookup o Data.get
+fun update k v = Data.map (Symtab.update (k, v))*}
+
+text {*
+  Since we want to store introduction rules associated with their 
+  logical connective, we can fill the table as follows.
+*}
+
+setup %gray {*
+  update "op &"   @{thm conjI} #>
+  update "op -->" @{thm impI}  #>
+  update "All"    @{thm allI}
 *}
 
 text {*
+  The use of \isacommand{setup} makes sure the table in the current theory 
+  is updated. The lookup can now be performed as follows.
+
+  @{ML_response_fake [display, gray]
+"lookup @{theory} \"op &\""
+"SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
+
+  An important point to note is that these tables (and data in general)
+  need to be treated in a purely functional fashion. Although
+  we can update the table as follows
+*}
+
+setup %gray {* update "op &" @{thm TrueI} *}
+
+text {*
+  and lookup now produces the introduction rule for @{term "True"}
+  
+@{ML_response_fake [display, gray]
+"lookup @{theory} \"op &\""
+"SOME \"True\""}
+
+  there are no references involved. This is one of the most fundamental
+  coding conventions for programming in Isabelle. References would interfere
+  with the multithreaded execution model of Isabelle.\footnote{\bf FIXME: say more}
+  
   \begin{readmore}
-  @{ML_file "Pure/ML-Systems/universal.ML"}
+  Isabelle contains implementations of several container data structures,
+  including association lists in @{ML_file "Pure/General/alist.ML"},
+  tables and symtables in @{ML_file "Pure/General/table.ML"}, and
+  directed graphs in @{ML_file "Pure/General/graph.ML"}.
+  \end{readmore}
+
+  Storing data in a proof context is similar. With the following code we
+  can store a list of terms in a proof context. 
+*}
+
+ML{*structure Data = ProofDataFun
+  (type T = term list
+   val init = (K []))*}
+
+text {*
+  The function we have to specify has to produce a list once a context 
+  is initialised (taking the theory into account from which the 
+  context is derived). We choose to just return the empty list. Next 
+  we define two auxiliary functions for updating the list with a given
+  term and printing the list. 
+*}
+
+ML{*fun update trm = Data.map (fn xs => trm::xs)
+
+fun print ctxt =
+  case (Data.get ctxt) of
+    [] => tracing "Empty!"
+  | xs => tracing (string_of_terms ctxt xs)*}
+
+text {*
+  Next we start with the context given by @{text "@{context}"} and 
+  update it in various ways. 
+
+  @{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\"}
+in
+  print ctxt; 
+  print ctxt';
+  print ctxt'';
+  print ctxt'''
+end"
+"Empty!
+True \<and> True, False
+1
+2, 1"}
+
+  Many functions in Isabelle manage and update data in a similar
+  fashion. Consequently, such calculation with contexts occur frequently in
+  Isabelle code, although the ``context flow'' is usually only linear.
+
+  A special instance of the mechanisms described above are configuration
+  values. They are used to in order to configure tools by the user without
+  having to resort to the ML-level. Assume you want the user to control three
+  values, say @{text bval} containing a boolean, @{text ival} containing an
+  integer and @{text sval} containing a string. These values can be declared
+  by
+*}
+
+ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
+val (ival, setup_ival) = Attrib.config_int "ival" 0
+val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
+
+text {* 
+  where each value needs to be given a default. To enable these values, they need to 
+  be set up with
+*}
+
+setup %gray {* 
+  setup_bval #> 
+  setup_ival 
+*}
+
+text {*
+  The user can now manipulate the values from the user-level of Isabelle 
+  with the command
+*}
+
+declare [[bval = true, ival = 3]]
+
+text {*
+  On the ML-level these values can be retrieved using the 
+  function @{ML Config.get}:
+
+  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
+
+  \begin{readmore}
+  For more information about configuration values see 
+  @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
   \end{readmore}
 *}
 
+
+
 (**************************************************)
 (* bak                                            *)
 (**************************************************)

--- a/ProgTutorial/Parsing.thy	Thu Oct 01 10:19:21 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Fri Oct 02 15:38:14 2009 +0200
@@ -697,6 +697,7 @@
 | evenS: "odd n \<Longrightarrow> even (Suc n)"
 | oddS: "even n \<Longrightarrow> odd (Suc n)"
 
+
 text {*
   For this we are going to use the parser:
 *}
@@ -980,10 +981,10 @@
 
 text {* 
   but you will not see any action as we chose to implement this command to do
-  nothing. The point of this command is to only show the procedure of how
+  nothing. The point of this command is only to show the procedure of how
   to interact with ProofGeneral. A similar procedure has to be done with any 
   other new command, and also any new keyword that is introduced with 
-  @{ML_ind OuterKeyword.keyword}.
+  the function @{ML_ind keyword in OuterKeyword}. For example:
 *}
 
 ML{*val _ = OuterKeyword.keyword "blink" *}
@@ -1005,13 +1006,12 @@
 
 ML{*let
   fun trace_prop str = 
-     LocalTheory.theory (fn lthy => (tracing str; lthy))
+     LocalTheory.theory (fn ctxt => (tracing str; ctxt))
 
-  val trace_prop_parser = OuterParse.prop >> trace_prop
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.local_theory "foobar_trace" "traces a proposition" 
-    kind trace_prop_parser
+    kind (OuterParse.prop >> trace_prop)
 end *}
 
 text {*
@@ -1036,28 +1036,28 @@
   OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
   to be re-created!
 
-  Below we change \isacommand{foobar\_trace} so that it takes a proposition as
-  argument and then starts a proof in order to prove it. Therefore in Line 13, 
-  we set the kind indicator to @{ML thy_goal in OuterKeyword}.
+  Below we show the command \isacommand{foobar\_goal} which takes a
+  proposition as argument and then starts a proof in order to prove
+  it. Therefore in Line 9, we set the kind indicator to @{ML thy_goal in
+  OuterKeyword}.
 *}
 
 ML%linenosgray{*let
-  fun prove_prop str lthy =
+  fun goal_prop str lthy =
     let
       val prop = Syntax.read_prop lthy str
     in
       Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
-    end;
+    end
   
-  val prove_prop_parser = OuterParse.prop >> prove_prop 
   val kind = OuterKeyword.thy_goal
 in
-  OuterSyntax.local_theory_to_proof "foobar_goal" "proving a proposition" 
-    kind prove_prop_parser
+  OuterSyntax.local_theory_to_proof "foobar_goal" "proves a proposition" 
+    kind (OuterParse.prop >> goal_prop)
 end *}
 
 text {*
-  The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
+  The function @{text goal_prop} in Lines 2 to 7 takes a string (the proposition to be
   proved) and a context as argument.  The context is necessary in order to be able to use
   @{ML_ind  read_prop in Syntax}, which converts a string into a proper proposition.
   In Line 6 the function @{ML_ind  theorem_i in Proof} starts the proof for the
@@ -1083,6 +1083,7 @@
 done
 
 text {*
+  {\bf TBD below}
 
   (FIXME: read a name and show how to store theorems; see @{ML_ind  note in LocalTheory})
   

--- a/ProgTutorial/ROOT.ML	Thu Oct 01 10:19:21 2009 +0200
+++ b/ProgTutorial/ROOT.ML	Fri Oct 02 15:38:14 2009 +0200
@@ -20,8 +20,6 @@
 use_thy "Recipes/Antiquotes";
 use_thy "Recipes/TimeLimit";
 use_thy "Recipes/Timing";
-use_thy "Recipes/Config";
-use_thy "Recipes/StoringData";
 use_thy "Recipes/ExternalSolver";
 use_thy "Recipes/Oracle";
 use_thy "Recipes/Sat";

--- a/ProgTutorial/Recipes/Config.thy	Thu Oct 01 10:19:21 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,82 +0,0 @@
-theory Config
-imports "../Base"
-begin
-
-section {* Configuration Options\label{rec:config} *} 
-
-text {*
-  {\bf Problem:} 
-  You would like to enhance your tool with options that can be changed 
-  by the user without having to resort to the ML-level.\smallskip
-
-  {\bf Solution:} This can be achieved using configuration values.\smallskip
-
-  Assume you want to control three values, say @{text bval} containing a
-  boolean,  @{text ival} containing an integer and @{text sval} 
-  containing a string. These values can be declared on the ML-level by
-*}
-
-ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false
-val (ival, setup_ival) = Attrib.config_int "ival" 0
-val (sval, setup_sval) = Attrib.config_string "sval" "some string" *}
-
-text {* 
-  where each value needs to be given a default. To enable these values, they need to 
-  be set up with
-*}
-
-setup {* setup_bval *} 
-setup {* setup_ival *}
-
-text {* or on the ML-level with *}
-
-ML{*setup_sval @{theory} *}
-
-text {*
-  The user can now manipulate the values from within Isabelle with the command
-*}
-
-declare [[bval = true, ival = 3]]
-
-text {*
-  On the ML-level these values can be retrieved using the 
-  function @{ML Config.get}:
-
-  @{ML_response [display,gray] "Config.get @{context} bval" "true"}
-
-  @{ML_response [display,gray] "Config.get @{context} ival" "3"}
-
-  The function @{ML Config.put} manipulates the values. For example
-
-  @{ML_response [display,gray] "Config.put sval \"foo\" @{context}; Config.get @{context} sval" "foo"}
-
-  The same can be achieved using the command \isacommand{setup}.
-*}
-
-setup {* Config.put_thy sval "bar" *}
-
-text {* 
-  Now the retrieval of this value yields:
-
-  @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""}
-
-  We can apply a function to a value using @{ML Config.map}. For example incrementing
-  @{ML ival} can be done by:
-
-  @{ML_response [display,gray] 
-"let 
-  val ctxt' = Config.map ival (fn i => i + 1) @{context}
-in 
-  Config.get ctxt' ival
-end" "4"}
-
-  \begin{readmore}
-  For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}.
-  \end{readmore}
-
-  There are many good reasons to control parameters in this way. One is
-  that no global reference is needed, which would cause many headaches 
-  with the multithreaded execution of Isabelle.
-*}
-
-end
\ No newline at end of file

--- a/ProgTutorial/Recipes/StoringData.thy	Thu Oct 01 10:19:21 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-theory StoringData
-imports "../Base"
-begin
-
-section {* Storing Data (TBD)\label{rec:storingdata} *} 
-
-
-text {*
-  {\bf Problem:} 
-  Your tool needs to manage data.\smallskip
-
-  {\bf Solution:} This can be achieved using a generic data slot.\smallskip
-
-  Every generic data slot may keep data of any kind which is stored in the
-  context.
-
-  *}
-
-ML{*local
-
-structure Data = GenericDataFun
- ( type T = int Symtab.table
-   val empty = Symtab.empty
-   val extend = I
-   fun merge _ = Symtab.merge (K true)
- )
-
-in
- val lookup = Symtab.lookup o Data.get
- fun update k v = Data.map (Symtab.update (k, v))
-end *}
-
-setup {* Context.theory_map (update "foo" 1) *}
-
-text {*
- 
-  @{ML_response [display,gray] "lookup (Context.Proof @{context}) \"foo\"" "SOME 1"} 
-
-
-*}
-
-text {*
-  alternatives: TheoryDataFun, ProofDataFun
-  Code: Pure/context.ML *}
-
-end
\ No newline at end of file

Binary file progtutorial.pdf has changed