# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256034320 -7200
# Node ID 42a1c230daff04e089ba689334f018c1a6ba6420
# Parent  544c149005cf892814252b1e1f4edce3a6df3df6
added something about add_thms_dynamic

diff -r 544c149005cf -r 42a1c230daff ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Mon Oct 19 17:31:13 2009 +0200
+++ b/ProgTutorial/General.thy	Tue Oct 20 12:25:20 2009 +0200
@@ -834,7 +834,8 @@
 
 text {*
   The fourth argument of @{ML note in LocalTheory} is the list of theorems we
-  want to store under a name.  The first argument @{ML_ind theoremK in Thm} is
+  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}, for an axiom @{ML_ind axiomK in Thm}, and for
@@ -842,8 +843,8 @@
   in Thm}.  The second argument of @{ML note in LocalTheory} is the name under
   which we store the theorem or theorems. The third 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 in order
-  add the theorem to the simpset:
+  Section~\ref{sec:attributes}. Below we just use one such attribute for
+  adding the theorem to the simpset:
 *}
 
 local_setup %gray {*
@@ -879,15 +880,71 @@
    @{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. 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 that we have to 
-  construct meta-variables in theorems explicitly.
+  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the 
+  user has no access to these theorems. 
+
+  Recall that Isabelle does not let you call @{ML note in LocalTheory} twice
+  with the same theorem name. In effect, once a theorem is stored under a name, 
+  this association will be fixed. While this is a ``safety-net'' to make sure a
+  theorem name refers to a particular theorem or collection of theorems, it is 
+  also a bit too restrictive in cases where a theorem name should refer to a 
+  dynamically expanding list of theorems (like a simpset). Therefore Isabelle 
+  also implements a mechanism where a theorem name can refer to a custom theorem 
+  list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. 
+  To see how it works let us assume we defined our own theorem list maintained 
+  in the data storage @{text MyThmList}.
+*}
 
-  \footnote{\bf FIXME say something about @{ML_ind add_thms_dynamic in PureThy}}
+ML{*structure MyThmList = GenericDataFun
+  (type T = thm list
+   val empty = []
+   val extend = I
+   val merge = K (op @) 
+)
+
+fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}
+
+text {*
+  The function @{ML update} allows us to update the theorem list, for example
+  by adding the theorem @{thm [source] TrueI}.
+*}
+
+setup %gray {* update @{thm TrueI} *}
+ 
+text {*
+  We can now install the theorem list so that it is visible to the user and 
+  can be refered to by a theorem name. For this need to call 
+  @{ML_ind add_thms_dynamic in PureThy}
+*}
+
+setup %gray {* 
+  PureThy.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) 
 *}
 
 text {*
+  with a name and a function that accesses the theorem list. Now if the
+  user issues the command
+
+  \begin{isabelle}
+  \isacommand{thm}~@{text "mythmlist"}\\
+  @{text "> True"}
+  \end{isabelle}
+
+  the current content of the theorem list is displayed. If more theorems are stored in 
+  the list, say
+*}
+
+setup %gray {* update @{thm FalseE} *}
+
+text {*
+  then the same command produces
+  
+  \begin{isabelle}
+  \isacommand{thm}~@{text "mythmlist"}\\
+  @{text "> False \<Longrightarrow> ?P"}\\
+  @{text "> True"}
+  \end{isabelle}
+
   There is a multitude of functions that manage or manipulate theorems in the 
   structures @{ML_struct Thm} and @{ML_struct Drule}. For example 
   we can test theorems for alpha equality. Suppose you proved the following three 
@@ -1083,7 +1140,7 @@
  (\"case_names\", \"foo_case_one;foo_case_two\")]"}
 
   You can observe the case names of this lemma on the user level when using 
-  the proof methods @{ML_text cases} and @{ML_text induct}. In the proof below
+  the proof methods @{text cases} and @{text induct}. In the proof below
 *}
 
 lemma
@@ -1206,7 +1263,7 @@
 end *}
 
 text {*
-  The parser reads a list of names. In the function @{ML_text action} we first
+  The parser reads a list of names. In the function @{text action} we first
   call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}
   on the resulting term. We can now suggest, for example, two variables for
   stripping off the first two @{text \<forall>}-quantifiers.
diff -r 544c149005cf -r 42a1c230daff progtutorial.pdf
Binary file progtutorial.pdf has changed