
diff -r d3fcc1a0272c -r 90bee31628dc CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Thu Feb 26 13:46:05 2009 +0100
+++ b/CookBook/FirstSteps.thy	Thu Mar 12 08:11:02 2009 +0100
@@ -18,6 +18,9 @@
   \ldots
   \end{tabular}
   \end{center}
+
+  We also generally assume you are working with HOL. The given examples might
+  need to be adapted slightly if you work in a different logic.
 *}
 
 section {* Including ML-Code *}
@@ -41,7 +44,7 @@
   evaluated by using the advance and undo buttons of your Isabelle
   environment. The code inside the \isacommand{ML}-command can also contain
   value and function bindings, and even those can be undone when the proof
-  script is retracted. As mentioned earlier, we will drop the
+  script is retracted. As mentioned in the Introduction, we will drop the
   \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we
   show code. The lines prefixed with @{text [quotes] ">"} are not part of the
   code, rather they indicate what the response is when the code is evaluated.
@@ -151,15 +154,26 @@
 
 text {*
   The easiest way to get the string of a theorem is to transform it
-  into a @{ML_type cterm} using the function @{ML crep_thm}.
+  into a @{ML_type cterm} using the function @{ML crep_thm}. Theorems
+  also include schematic variables, such as @{text "?P"}, @{text "?Q"}
+  and so on. In order to improve the readability of theorems we convert
+  these schematic variables into free variables using the 
+  function @{ML Variable.import_thms}.
 *}
 
-ML{*fun str_of_thm ctxt thm =
-  let
-    val {prop, ...} = crep_thm thm
-  in 
-    str_of_cterm ctxt prop
-  end*}
+ML{*fun no_vars ctxt thm =
+let 
+  val ((_, [thm']), _) = Variable.import_thms true [thm] ctxt
+in
+  thm'
+end
+
+fun str_of_thm ctxt thm =
+let
+  val {prop, ...} = crep_thm (no_vars ctxt thm)
+in 
+  str_of_cterm ctxt prop
+end*}
 
 text {* 
   Again the function @{ML commas} helps with printing more than one theorem. 
@@ -168,7 +182,6 @@
 ML{*fun str_of_thms ctxt thms =  
   commas (map (str_of_thm ctxt) thms)*}
 
-
 section {* Combinators\label{sec:combinators} *}
 
 text {*
@@ -395,29 +408,23 @@
 
 ML{*fun get_thm_names_from_ss simpset =
 let
-  val ({rules,...}, _) = MetaSimplifier.rep_ss simpset
+  val {simps,...} = MetaSimplifier.dest_ss simpset
 in
-  map #name (Net.entries rules)
+  map #1 simps
 end*}
 
 text {*
-  The function @{ML rep_ss in MetaSimplifier} returns a record containing all
-  information about the simpset. The rules of a simpset are stored in a
-  \emph{discrimination net} (a data structure for fast indexing). From this
-  net you can extract the entries using the function @{ML Net.entries}.
-  You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
-  in the current simpset---this simpset can be referred to using the antiquotation
+  The function @{ML dest_ss in MetaSimplifier} returns a record containing all
+  information stored in the simpset. We are only interested in the You can now use @{ML get_thm_names_from_ss} to obtain all names of theorems stored
+  in the current simpset. This simpset can be referred to using the antiquotation
   @{text "@{simpset}"}.
 
   @{ML_response_fake [display,gray] 
   "get_thm_names_from_ss @{simpset}" 
   "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
-  \begin{readmore}
-  The infrastructure for simpsets is implemented in @{ML_file "Pure/meta_simplifier.ML"}
-  and @{ML_file "Pure/simplifier.ML"}. Discrimination nets are implemented
-  in @{ML_file "Pure/net.ML"}.
-  \end{readmore}
+  Again, this way or referencing simpsets makes you independent from additions
+  of lemmas to the simpset by the user that potentially cause loops.
 
   While antiquotations have many applications, they were originally introduced in order 
   to avoid explicit bindings for theorems such as:
@@ -427,14 +434,13 @@
 
 text {*
   These bindings are difficult to maintain and also can be accidentally
-  overwritten by the user. This often breakes Isabelle
+  overwritten by the user. This often broke Isabelle
   packages. Antiquotations solve this problem, since they are ``linked''
   statically at compile-time.  However, this static linkage also limits their
   usefulness in cases where data needs to be build up dynamically. In the
   course of this chapter you will learn more about these antiquotations:
   they can simplify Isabelle programming since one can directly access all
   kinds of logical elements from th ML-level.
-
 *}
 
 section {* Terms and Types *}
@@ -465,7 +471,7 @@
   \end{readmore}
 
   Sometimes the internal representation of terms can be surprisingly different
-  from what you see at the user level, because the layers of
+  from what you see at the user-level, because the layers of
   parsing/type-checking/pretty printing can be quite elaborate. 
 
   \begin{exercise}
@@ -513,7 +519,7 @@
 *}
 
 
-section {* Constructing Terms and Types Manually *} 
+section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
 
 text {*
   While antiquotations are very convenient for constructing terms, they can
@@ -545,19 +551,18 @@
   the given arguments
 
   @{ML_response [display,gray] "make_imp @{term S} @{term T} @{typ nat}" 
-    "Const \<dots> $ 
-    Abs (\"x\", Type (\"nat\",[]),
-      Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ 
-                  (Free (\"T\",\<dots>) $ \<dots>))"}
+"Const \<dots> $ 
+  Abs (\"x\", Type (\"nat\",[]),
+    Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
 
   whereas with @{ML make_wrong_imp} we obtain a term involving the @{term "P"} 
   and @{text "Q"} from the antiquotation.
 
   @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T} @{typ nat}" 
-    "Const \<dots> $ 
-    Abs (\"x\", \<dots>,
-      Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
-                  (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
+"Const \<dots> $ 
+  Abs (\"x\", \<dots>,
+    Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $ 
+               (Const \<dots> $ (Free (\"Q\",\<dots>) $ \<dots>)))"}
 
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
@@ -566,15 +571,15 @@
 
 *} 
 
-ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
+ML{*fun make_fun_type tau1 tau2 = Type ("fun", [tau1, tau2]) *}
 
-text {* This can be equally written as: *}
+text {* This can be equally written with the combinator @{ML "-->"} as: *}
 
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 
 text {*
   A handy function for manipulating terms is @{ML map_types}: it takes a 
-  function and applies it to every type in the term. You can, for example,
+  function and applies it to every type in a term. You can, for example,
   change every @{typ nat} in a term into an @{typ int} using the function:
 *}
 
@@ -701,16 +706,18 @@
 text {*
   Occasional you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML Sign.extern_const} or
-  @{ML Sign.base_name}. For example:
+  @{ML Long_Name.base_name}. For example:
 
   @{ML_response [display,gray] "Sign.extern_const @{theory} \"List.list.Nil\"" "\"Nil\""}
 
   The difference between both functions is that @{ML extern_const in Sign} returns
-  the smallest name that is still unique, whereas @{ML base_name in Sign} always
+  the smallest name that is still unique, whereas @{ML base_name in Long_Name} always
   strips off all qualifiers.
 
   \begin{readmore}
-  FIXME
+  Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
+  functions about signatures in @{ML_file "Pure/sign.ML"}.
+  
   \end{readmore}
 *}
 
@@ -755,6 +762,19 @@
       (Const (@{const_name plus}, natT --> natT --> natT) $ zero $ zero)
 end" "0 + 0"}
 
+  In Isabelle also types need can be certified. For example, you obtain
+  the certified type for the Isablle type @{typ "nat \<Rightarrow> bool"} on the ML-level
+  as follows:
+
+  @{ML_response_fake [display,gray]
+  "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+  "nat \<Rightarrow> bool"}
+
+  \begin{readmore}
+  For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
+  the file @{ML_file "Pure/thm.ML"}.
+  \end{readmore}
+
   \begin{exercise}
   Check that the function defined in Exercise~\ref{fun:revsum} returns a
   result that type-checks.
@@ -814,8 +834,12 @@
 
   \begin{readmore}
   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
-  checking and pretty-printing of terms are defined.
+  checking and pretty-printing of terms are defined. Fuctions related to the
+  type inference are implemented in @{ML_file "Pure/type.ML"} and 
+  @{ML_file "Pure/type_infer.ML"}. 
   \end{readmore}
+
+  (FIXME: say something about sorts)
 *}
 
 
@@ -894,8 +918,7 @@
   theorem is proven. In particular, it is not possible to find out
   what are all theorems that have a given attribute in common, unless of course
   the function behind the attribute stores the theorems in a retrivable 
-  datastructure. This can be easily done by the recipe described in 
-  \ref{rec:named}. 
+  datastructure. 
 
   If you want to print out all currently known attributes a theorem 
   can have, you can use the function:
@@ -919,7 +942,7 @@
   context (which we ignore in the code above) and a theorem (@{text thm}), and 
   returns another theorem (namely @{text thm} resolved with the lemma 
   @{thm [source] sym}: @{thm sym[no_vars]}). The function @{ML "Thm.rule_attribute"} then returns 
-  an attribute (of type @{ML_type "attribute"}).
+  an attribute.
 
   Before we can use the attribute, we need to set it up. This can be done
   using the function @{ML Attrib.add_attributes} as follows.
@@ -927,8 +950,7 @@
 
 setup {*
   Attrib.add_attributes 
-    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")]
-*}
+    [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
 
 text {*
   The attribute does not expect any further arguments (unlike @{text "[OF
@@ -949,28 +971,183 @@
   @{text "> "}~@{thm test[my_sym]}
   \end{isabelle}
 
+  The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems.
+  Another usage of attributes is to add and delete theorems from stored data.
+  For example the attribute @{text "[simp]"} adds or deletes a theorem from the
+  current simpset. For these applications, you can use @{ML Thm.declaration_attribute}. 
+  To illustrate this function, let us introduce a reference containing a list
+  of theorems.
 *}
 
+ML{*val my_thms = ref ([]:thm list)*}
+
+text {* 
+  A word of warning: such references must not be used in any code that
+  is meant to be more than just for testing purposes! Here it is only used 
+  to illustrate matters. We will show later how to store data properly without 
+  using references. The function @{ML Thm.declaration_attribute} expects us to 
+  provide two functions that add and delete theorems from this list. 
+  For this we use the two functions:
+*}
+
+ML{*fun my_thms_add thm ctxt =
+  (my_thms := Thm.add_thm thm (!my_thms); ctxt)
+
+fun my_thms_del thm ctxt =
+  (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
+
 text {*
-What are: 
+  These functions take a theorem and a context and, for what we are explaining
+  here it is sufficient that they just return the context unchanged. They change
+  however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm}
+  adds a theorem if it is not already included in the list, and @{ML
+  Thm.del_thm} deletes one. Both functions use the predicate @{ML
+  Thm.eq_thm_prop} which compares theorems according to their proved
+  propositions (modulo alpha-equivalence).
 
 
-@{text "declaration_attribute"}
+  You can turn both functions into attributes using
+*}
+
+ML{*val my_add = Thm.declaration_attribute my_thms_add
+val my_del = Thm.declaration_attribute my_thms_del *}
+
+text {* 
+  and set up the attributes as follows
+*}
+
+setup {*
+  Attrib.add_attributes 
+    [("my_thms", Attrib.add_del_args my_add my_del, 
+        "maintaining a list of my_thms")] *}
+
+text {*
+  Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
+*}
+
+lemma trueI_2[my_thms]: "True" by simp
+
+text {*
+  then you can see the lemma is added to the initially empty list.
+
+  @{ML_response_fake [display,gray]
+  "!my_thms" "[\"True\"]"}
+
+  You can also add theorems using the command \isacommand{declare}.
+*}
+
+declare test[my_thms] trueI_2[my_thms add]
+
+text {*
+  The @{text "add"} is the default operation and does not need
+  to be given. This declaration will cause the theorem list to be 
+  updated as follows.
+
+  @{ML_response_fake [display,gray]
+  "!my_thms"
+  "[\"True\", \"Suc (Suc 0) = 2\"]"}
+
+  The theorem @{thm [source] trueI_2} only appears once, since the 
+  function @{ML Thm.add_thm} tests for duplicates, before extending
+  the list. Deletion from the list works as follows:
+*}
+
+declare test[my_thms del]
+
+text {* After this, the theorem list is again: 
+
+  @{ML_response_fake [display,gray]
+  "!my_thms"
+  "[\"True\"]"}
+
+  We used in this example two functions declared as @{ML Thm.declaration_attribute}, 
+  but there can be any number of them. We just have to change the parser for reading
+  the arguments accordingly. 
+
+  However, as said at the beginning of this example, using references for storing theorems is
+  \emph{not} the received way of doing such things. The received way is to 
+  start a ``data slot'' in a context by using the functor @{text GenericDataFun}:
+*}
 
-@{text "theory_attributes"}
+ML {*structure Data = GenericDataFun
+ (type T = thm list
+  val empty = []
+  val extend = I
+  fun merge _ = Thm.merge_thms) *}
+
+text {*
+  To use this data slot, you only have to change @{ML my_thms_add} and
+  @{ML my_thms_del} to:
+*}
+
+ML{*val thm_add = Data.map o Thm.add_thm
+val thm_del = Data.map o Thm.del_thm*}
+
+text {*
+  where @{ML Data.map} updates the data appropriately in the context. Since storing
+  theorems in a special list is such a common task, there is the functor @{text NamedThmsFun},
+  which does most of the work for you. To obtain such a named theorem lists, you just
+  declare 
+*}
+
+ML{*structure FooRules = NamedThmsFun 
+ (val name = "foo" 
+  val description = "Rules for foo"); *}
+
+text {*
+  and set up the @{ML_struct FooRules} with the command
+*}
+
+setup {* FooRules.setup *}
 
-@{text "proof_attributes"}
+text {*
+  This code declares a data slot where the theorems are stored,
+  an attribute @{text foo} (with the @{text add} and @{text del} options
+  for adding and deleting theorems) and an internal ML interface to retrieve and 
+  modify the theorems.
+
+  Furthermore, the facts are made available on the user-level under the dynamic 
+  fact name @{text foo}. For example you can declare three lemmas to be of the kind
+  @{text foo} by:
+*}
+
+lemma rule1[foo]: "A" sorry
+lemma rule2[foo]: "B" sorry
+lemma rule3[foo]: "C" sorry
+
+text {* and undeclare the first one by: *}
+
+declare rule1[foo del]
+
+text {* and query the remaining ones with:
+
+  \begin{isabelle}
+  \isacommand{thm}~@{text "foo"}\\
+  @{text "> ?C"}\\
+  @{text "> ?B"}
+  \end{isabelle}
+
+  On the ML-level the rules marked with @{text "foo"} can be retrieved
+  using the function @{ML FooRules.get}:
+
+  @{ML_response_fake [display,gray] "FooRules.get @{context}" "[\"?C\",\"?B\"]"}
+
+  \begin{readmore}
+  For more information see @{ML_file "Pure/Tools/named_thms.ML"} and also
+  the recipe in Section~\ref{recipe:storingdata} about storing arbitrary
+  data.
+  \end{readmore}
+
+  (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
 
 
   \begin{readmore}
   FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
   \end{readmore}
-
-
 *}
 
 
-section {* Theories and Local Theories *}
+section {* Theories, Contexts and Local Theories (TBD) *}
 
 text {*
   (FIXME: expand)
@@ -992,7 +1169,7 @@
 
 
 
-section {* Storing Theorems\label{sec:storing} *}
+section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}
 
@@ -1001,28 +1178,41 @@
 (* FIXME: some code below *)
 
 (*<*)
+(*
 setup {*
- Sign.add_consts_i [("bar", @{typ "nat"},NoSyn)] 
+ Sign.add_consts_i [(Binding"bar", @{typ "nat"},NoSyn)] 
 *}
-
+*)
 lemma "bar = (1::nat)"
   oops
 
+(*
 setup {*   
   Sign.add_consts_i [("foo", @{typ "nat"},NoSyn)] 
  #> PureThy.add_defs false [((Binding.name "foo_def", 
        Logic.mk_equals (Const ("FirstSteps.foo", @{typ "nat"}), @{term "1::nat"})), [])] 
  #> snd
 *}
-
+*)
+(*
 lemma "foo = (1::nat)"
   apply(simp add: foo_def)
   done
 
 thm foo_def
+*)
 (*>*)
 
-section {* Misc *}
+section {* Pretty-Printing (TBD) *}
+
+text {*
+  @{ML Pretty.big_list},
+  @{ML Pretty.brk},
+  @{ML Pretty.block},
+  @{ML Pretty.chunks}
+*}
+
+section {* Misc (TBD) *}
 
 ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
 




