--- a/ProgTutorial/General.thy Sat Oct 03 13:01:39 2009 +0200
+++ b/ProgTutorial/General.thy Sat Oct 03 19:10:23 2009 +0200
@@ -7,7 +7,8 @@
text {*
Isabelle is build around a few central ideas. One is the LCF-approach to
theorem proving where there is a small trusted core and everything else is
- build on top of this trusted core.
+ build on top of this trusted core. The central data structures involved
+ in this core are certified terms and types as well as theorems.
*}
@@ -15,8 +16,9 @@
section {* Terms and Types *}
text {*
- One way to construct Isabelle terms, is by using the antiquotation
- \mbox{@{text "@{term \<dots>}"}}. For example
+ In Isabelle there are certified terms (respectively types) and uncertified
+ terms. The latter are called just terms. One way to construct them is by
+ using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
@{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
@@ -446,7 +448,8 @@
@{ML_response [display,gray]
"@{type_name \"list\"}" "\"List.list\""}
- (FIXME: Explain the following better.)
+ \footnote{\bf FIXME: Explain the following better; maybe put in a separate
+ section and link with the comment in the antiquotation section.}
Occasionally you have to calculate what the ``base'' name of a given
constant is. For this you can use the function @{ML_ind "Sign.extern_const"} or
@@ -537,9 +540,9 @@
number representing their sum.
\end{exercise}
- \begin{exercise}\footnote{Personal communication of
- de Bruijn to Dyckhoff.}\label{ex:debruijn}
- Implement the function, which we below name deBruijn, that depends on a natural
+ \begin{exercise}\label{ex:debruijn}
+ Implement the function, which we below name deBruijn\footnote{According to
+ personal communication of de Bruijn to Dyckhoff.}, that depends on a natural
number n$>$0 and constructs terms of the form:
\begin{center}
@@ -551,7 +554,7 @@
\end{tabular}
\end{center}
- For n=3 this function returns the term
+ This function returns for n=3 the term
\begin{center}
\begin{tabular}{l}
@@ -685,13 +688,13 @@
@{ML_file "Pure/type_infer.ML"}.
\end{readmore}
- (FIXME: say something about sorts)
+ \footnote{\bf FIXME: say something about sorts.}
\begin{exercise}
Check that the function defined in Exercise~\ref{fun:revsum} returns a
result that type-checks. See what happens to the solutions of this
- exercise given in \ref{ch:solutions} when they receive an ill-typed term
- as input.
+ exercise given in Appendix \ref{ch:solutions} when they receive an
+ ill-typed term as input.
\end{exercise}
*}
@@ -982,7 +985,7 @@
However, here also a weakness of the concept
of theorem attributes shows through: since theorem attributes can be
- arbitrary functions, they do not in general commute. If you try
+ arbitrary functions, they do not commute in general. If you try
\begin{isabelle}
\isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
@@ -992,56 +995,34 @@
you get an exception indicating that the theorem @{thm [source] sym}
does not resolve with meta-equations.
- The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate theorems.
- Another usage of theorem attributes is to add and delete theorems from stored data.
- For example the theorem attribute @{text "[simp]"} adds or deletes a theorem from the
- current simpset. For these applications, you can use @{ML_ind declaration_attribute in Thm}.
- To illustrate this function, let us introduce a reference containing a list
- of theorems.
-*}
-
-ML{*val my_thms = Unsynchronized.ref ([] : thm list)*}
-
-text {*
- The purpose of this reference is to store a list of theorems.
- We are going to modify it by adding and deleting theorems.
- However, 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.
-
- We need to provide two functions that add and delete theorems from this list.
- For this we use the two functions:
+ The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate
+ theorems. Another usage of theorem attributes is to add and delete theorems
+ from stored data. For example the theorem attribute @{text "[simp]"} adds
+ or deletes a theorem from the current simpset. For these applications, you
+ can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,
+ let us introduce a theorem list.
*}
-ML{*fun my_thm_add thm ctxt =
- (my_thms := Thm.add_thm thm (!my_thms); ctxt)
-
-fun my_thm_del thm ctxt =
- (my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
+ML{*structure MyThms = Named_Thms
+ (val name = "attr_thms"
+ val description = "Theorems for an Attribute") *}
-text {*
- 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_ind add_thm in Thm} adds a theorem if it is not already included in
- the list, and @{ML_ind del_thm in Thm} deletes one (both functions use the
- predicate @{ML_ind eq_thm_prop in Thm}, which compares theorems according to
- their proved propositions modulo alpha-equivalence).
-
- You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into
- attributes with the code
+text {*
+ We are going to modify this list by adding and deleting theorems.
+ For this we use the two functions @{ML MyThms.add_thm} and
+ @{ML MyThms.del_thm}. You can turn them into attributes
+ with the code
*}
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
+ML{*val my_add = Thm.declaration_attribute MyThms.add_thm
+val my_del = Thm.declaration_attribute MyThms.del_thm *}
text {*
and set up the attributes as follows
*}
attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
- "maintaining a list of my_thms - rough test only!"
+ "maintaining a list of my_thms"
text {*
The parser @{ML_ind add_del in Attrib} is a predefined parser for
@@ -1055,12 +1036,13 @@
then you can see it is added to the initially empty list.
@{ML_response_fake [display,gray]
- "!my_thms" "[\"True\"]"}
+ "MyThms.get @{context}"
+ "[\"True\"]"}
You can also add theorems using the command \isacommand{declare}.
*}
-declare test[my_thms] trueI_2[my_thms add]
+declare test[my_thms] trueI_2[my_thms add]
text {*
With this attribute, the @{text "add"} operation is the default and does
@@ -1068,7 +1050,7 @@
theorem list to be updated as:
@{ML_response_fake [display,gray]
- "!my_thms"
+ "MyThms.get @{context}"
"[\"True\", \"Suc (Suc 0) = 2\"]"}
The theorem @{thm [source] trueI_2} only appears once, since the
@@ -1081,144 +1063,14 @@
text {* After this, the theorem list is again:
@{ML_response_fake [display,gray]
- "!my_thms"
+ "MyThms.get @{context}"
"[\"True\"]"}
- We used in this example two functions declared as @{ML_ind declaration_attribute in Thm},
- 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'', below called @{text MyThmsData}, generated by the functor
- @{text GenericDataFun}:
-*}
-
-ML{*structure MyThmsData = GenericDataFun
- (type T = thm list
- val empty = []
- val extend = I
- fun merge _ = Thm.merge_thms) *}
-
-text {*
- The type @{text "T"} of this data slot is @{ML_type "thm list"}.\footnote{FIXME: give a pointer
- to where data slots are explained properly.}
- To use this data slot, you only have to change @{ML my_thm_add} and
- @{ML my_thm_del} to:
-*}
-
-ML{*val my_thm_add = MyThmsData.map o Thm.add_thm
-val my_thm_del = MyThmsData.map o Thm.del_thm*}
-
-text {*
- where @{ML MyThmsData.map} updates the data appropriately. The
- corresponding theorem attributes are
-*}
-
-ML{*val my_add = Thm.declaration_attribute my_thm_add
-val my_del = Thm.declaration_attribute my_thm_del *}
-
-text {*
- and the setup is as follows
-*}
-
-attribute_setup %gray my_thms2 = {* Attrib.add_del my_add my_del *}
- "properly maintaining a list of my_thms"
-
-text {*
- Initially, the data slot is empty
-
- @{ML_response_fake [display,gray]
- "MyThmsData.get (Context.Proof @{context})"
- "[]"}
-
- but if you prove
-*}
-
-lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
-
-text {*
- then the lemma is recorded.
-
- @{ML_response_fake [display,gray]
- "MyThmsData.get (Context.Proof @{context})"
- "[\"3 = Suc (Suc (Suc 0))\"]"}
-
- With theorem attribute @{text my_thms2} you can also nicely see why it
- is important to
- store data in a ``data slot'' and \emph{not} in a reference. Backtrack
- to the point just before the lemma @{thm [source] three} was proved and
- check the the content of @{ML_struct MyThmsData}: it should be empty.
- The addition has been properly retracted. Now consider the proof:
-*}
+ We used in this example two functions declared as @{ML_ind
+ declaration_attribute in Thm}, but there can be any number of them. We just
+ have to change the parser for reading the arguments accordingly.
-lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
-
-text {*
- Checking the content of @{ML my_thms} gives
-
- @{ML_response_fake [display,gray]
- "!my_thms"
- "[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
-
- as expected, but if you backtrack before the lemma @{thm [source] four}, the
- content of @{ML my_thms} is unchanged. The backtracking mechanism
- of Isabelle is completely oblivious about what to do with references, but
- properly treats ``data slots''!
-
- Since storing theorems in a list is such a common task, there is the special
- functor @{ML_functor Named_Thms}, which does most of the work for you. To obtain
- a named theorem list, you just declare
-*}
-
-ML{*structure FooRules = Named_Thms
- (val name = "foo"
- val description = "Rules for foo") *}
-
-text {*
- and set up the @{ML_struct FooRules} with the command
-*}
-
-setup %gray {* FooRules.setup *}
-
-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"}.
- \end{readmore}
-
- (FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?)
-
+ \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
\begin{readmore}
FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in