--- a/CookBook/FirstSteps.thy Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/FirstSteps.thy Mon Mar 16 00:12:32 2009 +0100
@@ -248,8 +248,8 @@
avoided: it is more than easy to get the intermediate values wrong, not to
mention the nightmares the maintenance of this code causes!
- A ``real world'' example for a function written in the waterfall fashion might
- be the following:
+ In the context of Isabelle, a ``real world'' example for a function written in
+ the waterfall fashion might be the following code:
*}
ML %linenosgray{*fun apply_fresh_args pred ctxt =
@@ -261,12 +261,12 @@
|> (curry list_comb) pred *}
text {*
- The point of this function is to extract the argument types of the given
+ The point of this code is to extract the argument types of the given
predicate and then generate for each type a distinct variable; finally it
applies the generated variables to the predicate. You can read this off from
how the function is coded: in Line 2, the function @{ML fastype_of}
calculates the type of the predicate; in Line 3, @{ML binder_types} produces
- the list of argument types; Line 4 pairs up each type with the string/name
+ the list of argument types; Line 4 pairs up each type with the string (or name)
@{text "z"}; the function @{ML variant_frees in Variable} generates for each
@{text "z"} a unique name avoiding @{text pred}; the list of name-type pairs
is turned into a list of variable terms in Line 6, which in the last line
@@ -782,9 +782,9 @@
(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:
+ In Isabelle not just types need to be certified, but also types. 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})"
@@ -800,8 +800,8 @@
result that type-checks.
\end{exercise}
- Remember that in Isabelle a term contains enough typing information
- (constants, free variables and abstractions all have typing
+ Remember Isabelle foolows the Church-style typing for terms, i.e.~a term contains
+ enough typing information (constants, free variables and abstractions all have typing
information) so that it is always clear what the type of a term is.
Given a well-typed term, the function @{ML type_of} returns the
type of a term. Consider for example:
@@ -965,16 +965,16 @@
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.
+ using the function @{ML Attrib.setup} as follows.
*}
-setup %gray {* Attrib.add_attributes
- [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *}
+setup %gray {* Attrib.setup @{binding "my_sym"}
+ (Scan.succeed my_symmetric) "applying the sym rule"*}
text {*
The attribute does not expect any further arguments (unlike @{text "[OF
\<dots>]"}, for example, which can take a list of theorems as argument). Therefore
- we use the function @{ML Attrib.no_args}. Later on we will also consider
+ we use the parser @{ML Scan.succeed}. Later on we will also consider
attributes taking further arguments. An example for the attribute @{text
"[my_sym]"} is the proof
*}
@@ -1035,9 +1035,8 @@
and set up the attributes as follows
*}
-setup %gray {* Attrib.add_attributes
- [("my_thms", Attrib.add_del_args my_add my_del,
- "maintaining a list of my_thms")] *}
+setup %gray {* Attrib.setup @{binding "my_thms"}
+ (Attrib.add_del my_add my_del) "maintaining a list of my_thms" *}
text {*
Now if you prove the lemma attaching the attribute @{text "[my_thms]"}
@@ -1165,13 +1164,62 @@
*}
+section {* Setups (TBD) *}
+
+text {*
+ In the previous section we used \isacommand{setup} in order to make
+ a theorem attribute known to Isabelle. What happens behind the scenes
+ is that \isacommand{setup} expects a functions from @{ML_type theory}
+ to @{ML_type theory}: the input theory is the current theory and the
+ output the theory where the theory attribute has been stored.
+
+ This is a fundamental principle in Isabelle. A similar situation occurs
+ for example with declaring constants. The function that declares a
+ constant on the ML-level is @{ML Sign.add_consts_i}. Recall that ML-code
+ needs to be \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}.
+ If you write
+*}
+
+ML{*Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] @{theory} *}
+
+text {*
+ for declaring the constant @{text "BAR"} with type @{typ nat} and
+ run the code, then you indeed obtain a theory as result. But if you
+ query the constant with \isacommand{term}
+
+ \begin{isabelle}
+ \isacommand{term}~@{text [quotes] "BAR"}\\
+ @{text "> \"BAR\" :: \"'a\""}
+ \end{isabelle}
+
+ you do not obtain a constant of type @{typ nat}, but a free variable (printed in
+ blue) of polymorphic type. The problem is that the ML-expression above did
+ not register the declaration with the current theory. This is what the command
+ \isacommand{setup} is for. The constant is properly declared with
+*}
+
+setup %gray {* Sign.add_consts_i [(Binding.name "BAR", @{typ "nat"}, NoSyn)] *}
+
+text {*
+ Now
+
+ \begin{isabelle}
+ \isacommand{term}~@{text [quotes] "BAR"}\\
+ @{text "> \"BAR\" :: \"nat\""}
+ \end{isabelle}
+
+ returns a (black) constant with the type @{typ nat}.
+
+ A similar command is \isacommand{local\_setup}, which expects a function
+ of type @{ML_type "local_theory -> local_theory"}. Later on we will also
+ use the commands \isacommand{method\_setup} for installing methods in the
+ current theory and \isacommand{simproc\_setup} for adding new simprocs to
+ the current simpset.
+*}
+
section {* Theories, Contexts and Local Theories (TBD) *}
text {*
- (FIXME: expand)
-
- (FIXME: explain \isacommand{setup})
-
There are theories, proof contexts and local theories (in this order, if you
want to order them).
@@ -1182,10 +1230,7 @@
@{ML_type local_theory} is identical to the type of \emph{proof contexts}
@{ML_type "Proof.context"}, although not every proof context constitutes a
valid local theory.
-
- *}
-
-
+*}
section {* Storing Theorems\label{sec:storing} (TBD) *}