
diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/General.thy
--- a/ProgTutorial/General.thy	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/General.thy	Thu Nov 19 14:11:50 2009 +0100
@@ -1333,23 +1333,22 @@
   While we obtained a theorem as result, this theorem is not
   yet stored in Isabelle's theorem database. Consequently, it cannot be 
   referenced on the user level. One way to store it in the theorem database is
-  by using the function @{ML_ind note in LocalTheory}.\footnote{\bf FIXME: make sure a pointer
+  by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
   to the section about local-setup is given earlier.}
 *}
 
 local_setup %gray {*
-  LocalTheory.note Thm.theoremK
-     ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
 
 text {*
-  The fourth argument of @{ML note in LocalTheory} is the list of theorems we
+  The fourth 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}, for an axiom @{ML_ind axiomK in Thm}, and for
+  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 LocalTheory} is the name under
+  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
   list of theorem attributes, which we will explain in detail in
   Section~\ref{sec:attributes}. Below we just use one such attribute for
@@ -1357,13 +1356,12 @@
 *}
 
 local_setup %gray {*
-  LocalTheory.note Thm.theoremK
-    ((@{binding "my_thm_simp"}, 
+  Local_Theory.note ((@{binding "my_thm_simp"}, 
        [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
 
 text {*
   Note that we have to use another name under which the theorem is stored,
-  since Isabelle does not allow us to call  @{ML_ind note in LocalTheory} twice
+  since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
   with the same name. The attribute needs to be wrapped inside the function @{ML_ind
   internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function 
   @{ML get_thm_names_from_ss} from
@@ -1392,7 +1390,7 @@
   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
+  Recall that Isabelle does not let you call @{ML note in Local_Theory} twice
   with the same theorem name. In effect, once a theorem is stored under a name, 
   this association is fixed. While this is a ``safety-net'' to make sure a
   theorem name refers to a particular theorem or collection of theorems, it is 
@@ -1407,9 +1405,9 @@
   (type T = thm list
    val empty = []
    val extend = I
-   val merge = op @)
-
-fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}
+   val merge = merge Thm.eq_thm_prop)
+
+fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
 
 text {*
   The function @{ML update} allows us to update the theorem list, for example
@@ -1650,10 +1648,9 @@
 *}
 
 local_setup %gray {*
-  LocalTheory.note Thm.lemmaK
-    ((@{binding "foo_data'"}, []), 
-      [(Rule_Cases.name ["foo_case_one", "foo_case_two"] 
-        @{thm foo_data})]) #> snd *}
+  Local_Theory.note ((@{binding "foo_data'"}, []), 
+    [(Rule_Cases.name ["foo_case_one", "foo_case_two"] 
+       @{thm foo_data})]) #> snd *}
 
 text {*
   The data of the theorem @{thm [source] foo_data'} is then as follows:
@@ -2139,6 +2136,9 @@
 
 section {* Local Theories (TBD) *}
 
+text {*
+  @{ML_ind "Local_Theory.declaration"}
+*}
 
 (*
 setup {*
@@ -2477,6 +2477,50 @@
 ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
 *)
 
+section {* Morphisms (TBD) *}
+
+text {*
+  Morphisms are arbitrary transformations over terms, types, theorems and bindings.
+  They can be constructed using the function @{ML_ind morphism in Morphism},
+  which expects a record with functions of type
+
+  \begin{isabelle}
+  \begin{tabular}{rl}
+  @{text "binding:"} & @{text "binding -> binding"}\\
+  @{text "typ:"}     & @{text "typ -> typ"}\\
+  @{text "term:"}    & @{text "term -> term"}\\
+  @{text "fact:"}    & @{text "thm list -> thm list"}
+  \end{tabular}
+  \end{isabelle}
+
+  The simplest morphism is the  @{ML_ind identity in Morphism}-morphism defined as
+*}
+
+ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*}
+  
+text {*
+  Morphisms can be composed with the function @{ML_ind "$>" in Morphism}
+*}
+
+ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T) 
+  | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)
+  | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)
+  | trm_phi t = t*}
+
+ML{*val phi = Morphism.term_morphism trm_phi*}
+
+ML{*Morphism.term phi @{term "P x y"}*}
+
+text {*
+  @{ML_ind term_morphism in Morphism}
+
+  @{ML_ind term in Morphism},
+  @{ML_ind thm in Morphism}
+
+  \begin{readmore}
+  Morphisms are implemented in the file @{ML_file "Pure/morphism.ML"}.
+  \end{readmore}
+*}
 
 section {* Misc (TBD) *}
 
@@ -2501,6 +2545,8 @@
 text {* 
   @{ML_ind "Binding.str_of"} returns the string with markup;
   @{ML_ind "Binding.name_of"} returns the string without markup
+
+  @{ML_ind "Binding.conceal"} 
 *}
 
 section {* Concurrency (TBD) *}




