--- a/ProgTutorial/FirstSteps.thy Tue Mar 24 09:34:03 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Tue Mar 24 12:09:38 2009 +0100
@@ -132,15 +132,17 @@
*}
(*
-ML {* set Toplevel.debug *}
+ML {* reset Toplevel.debug *}
+
+ML {* fun dodgy_fun () = (raise TYPE ("",[],[]); 1) *}
-ML {*
-fun dodgy_fun () = (raise (ERROR "bar"); 1)
-*}
+ML {* fun innocent () = dodgy_fun () *}
+ML {* exception_trace (fn () => cterm_of @{theory} (Bound 0)) *}
+ML {* exception_trace (fn () => innocent ()) *}
-ML {* fun f1 () = dodgy_fun () *}
+ML {* Toplevel.program (fn () => cterm_of @{theory} (Bound 0)) *}
-ML {* f1 () *}
+ML {* Toplevel.program (fn () => innocent ()) *}
*)
text {*
@@ -207,7 +209,7 @@
str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*}
text {*
- Theorem @{thm [source] conjI} looks now as follows:
+ Theorem @{thm [source] conjI} is now printed as follows:
@{ML_response_fake [display, gray]
"warning (str_of_thm_no_vars @{context} @{thm conjI})"
@@ -520,7 +522,6 @@
((@{binding "TrueConj"}, NoSyn),
(Attrib.empty_binding, @{term "True \<and> True"})) *}
-<<<<<<< local
text {*
Now querying the definition you obtain:
@@ -560,7 +561,7 @@
"Const (\"op =\", \<dots>) $
(Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
- will show the term @{term "(a::nat) + b = c"}, but printed using an internal
+ will show the term @{term "(a::nat) + b = c"}, but printed using the internal
representation corresponding to the data type @{ML_type "term"}.
This internal representation uses the usual de Bruijn index mechanism---where
@@ -937,6 +938,12 @@
"ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
"nat \<Rightarrow> bool"}
+ or with the antiquotation:
+
+ @{ML_response_fake [display,gray]
+ "@{ctyp \"nat \<Rightarrow> 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"}.
@@ -1072,8 +1079,10 @@
@{ML_file "Pure/thm.ML"}.
\end{readmore}
- (FIXME: handy functions working on theorems; how to add case-names to goal
- states - maybe in the next section)
+ (FIXME: handy functions working on theorems, like @{ML ObjectLogic.rulify} and so on)
+
+ (FIXME how to add case-names to goal states - maybe in the
+ next section)
*}
section {* Theorem Attributes *}
@@ -1099,8 +1108,8 @@
\end{isabelle}
The theorem attributes fall roughly into two categories: the first category manipulates
- the proved theorem (like @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
- stores the proved theorem somewhere as data (like @{text "[simp]"}, which adds
+ the proved theorem (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
+ stores the proved theorem somewhere as data (for example @{text "[simp]"}, which adds
the theorem to the current simpset).
To explain how to write your own attribute, let us start with an extremely simple
@@ -1114,8 +1123,10 @@
text {*
where the function @{ML "Thm.rule_attribute"} expects a function taking a
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
+ returns another theorem (namely @{text thm} resolved with the theorem
+ @{thm [source] sym}: @{thm sym[no_vars]}).\footnote{The function @{ML RS} is explained
+ later on in Section~\ref{sec:simpletacs}.} The function
+ @{ML "Thm.rule_attribute"} then returns
an attribute.
Before we can use the attribute, we need to set it up. This can be done
@@ -1126,11 +1137,11 @@
"applying the sym rule"
text {*
- The attribute does not expect any further arguments (unlike @{text "[THEN
- \<dots>]"}, for example). Therefore
- 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
+ Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
+ for the theorem attribute. Since the attribute does not expect any further
+ arguments (unlike @{text "[THEN \<dots>]"}, for example), 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
*}
lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
@@ -1152,7 +1163,7 @@
\end{isabelle}
As an example of a slightly more complicated theorem attribute, we implement
- our version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
+ our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
as argument and resolve the proved theorem with this list (one theorem
after another). The code for this attribute is
*}
@@ -1161,8 +1172,7 @@
Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*}
text {*
- where @{ML swap} swaps the components of a pair (@{ML RS} is explained
- later on in Section~\ref{sec:simpletacs}). The setup of this theorem
+ where @{ML swap} swaps the components of a pair. The setup of this theorem
attribute uses the parser @{ML Attrib.thms}, which parses a list of
theorems.
*}
@@ -1216,20 +1226,20 @@
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 purpose of this reference is that we are going to add and delete theorems
+ to the referenced list. 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.
- The function @{ML Thm.declaration_attribute} expects us to
- provide two functions that add and delete theorems from this list.
+ We need 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 =
+ML{*fun my_thm_add thm ctxt =
(my_thms := Thm.add_thm thm (!my_thms); ctxt)
-fun my_thms_del thm ctxt =
+fun my_thm_del thm ctxt =
(my_thms := Thm.del_thm thm (!my_thms); ctxt)*}
text {*
@@ -1242,25 +1252,24 @@
propositions modulo alpha-equivalence).
- You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into
+ You can turn functions @{ML my_thm_add} and @{ML my_thm_del} into
attributes with the code
*}
-ML{*val my_add = Thm.declaration_attribute my_thms_add
-val my_del = Thm.declaration_attribute my_thms_del *}
+ML{*val my_add = Thm.declaration_attribute my_thm_add
+val my_del = Thm.declaration_attribute my_thm_del *}
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"
+ "maintaining a list of my_thms - rough test only!"
text {*
- The parser @{ML Attrib.add_del} is a predefined parser for
+ The parser @{ML Attrib.add_del} is a pre-defined parser for
adding and deleting lemmas. Now if you prove the next lemma
- and attach the attribute
- @{text "[my_thms]"}
+ and attach to it the attribute @{text "[my_thms]"}
*}
lemma trueI_2[my_thms]: "True" by simp
@@ -1274,11 +1283,11 @@
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 {*
- The @{text "add"} is the default operation and does not need
- to be explicitly given. These two declarations will cause the
+ With this attribute, the @{text "add"} operation is the default and does
+ not need to be explicitly given. These three declarations will cause the
theorem list to be updated as:
@{ML_response_fake [display,gray]
@@ -1304,7 +1313,7 @@
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}, by using the functor
+ start a ``data slot'', below called @{text MyThmsData}, generated by the functor
@{text GenericDataFun}:
*}
@@ -1315,30 +1324,32 @@
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:
+ 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 thm_add = MyThmsData.map o Thm.add_thm
-val thm_del = MyThmsData.map o Thm.del_thm*}
+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 addtributes are
*}
-ML{*val add = Thm.declaration_attribute thm_add
-val del = Thm.declaration_attribute thm_del *}
+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 add del *}
+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
+ Initially, the data slot is empty
@{ML_response_fake [display,gray]
"MyThmsData.get (Context.Proof @{context})"
@@ -1350,17 +1361,18 @@
lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp
text {*
- the lemma is now included
+ then the lemma is recorded.
@{ML_response_fake [display,gray]
"MyThmsData.get (Context.Proof @{context})"
"[\"3 = Suc (Suc (Suc 0))\"]"}
- With @{text my_thms2} you can also nicely see why it is important to
+ 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} is proved and
- check the the content of @{ML_struct "MyThmsData"}: it is now again
- empty. The addition has been properly retracted. Now consider the proof:
+ 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:
*}
lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp
@@ -1372,13 +1384,14 @@
"!my_thms"
"[\"4 = Suc (Suc (Suc (Suc 0)))\", \"True\"]"}
- as expected, but if we backtrack before the lemma @{thm [source] four}, the
+ 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!
+ of Isabelle is completely oblivious about what to do with references, but
+ properly treats ``data slots''!
- Since storing theorems in a special list is such a common task, there is the
+ Since storing theorems in a list is such a common task, there is the special
functor @{text NamedThmsFun}, which does most of the work for you. To obtain
- such a named theorem lists, you just declare
+ a named theorem lists, you just declare
*}
ML{*structure FooRules = NamedThmsFun
@@ -1433,7 +1446,9 @@
\begin{readmore}
- FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"}
+ FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in
+ @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
+ parsing.
\end{readmore}
*}