diff -r 096776f180fc -r d3cd633e8240 ProgTutorial/FirstSteps.thy --- 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 \ True"})) *} -<<<<<<< local text {* Now querying the definition you obtain: @@ -560,7 +561,7 @@ "Const (\"op =\", \) $ (Const (\"HOL.plus_class.plus\", \) $ \ $ \) $ \"} - 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 \ bool"} + or with the antiquotation: + + @{ML_response_fake [display,gray] + "@{ctyp \"nat \ bool\"}" + "nat \ 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 \]"}), 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 \]"}), 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 - \]"}, 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 "\ \ \"}, we have to specify a parser + for the theorem attribute. Since the attribute does not expect any further + arguments (unlike @{text "[THEN \]"}, 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 \]"}. This attribute will take a list of theorems + our own version of @{text "[THEN \]"}. 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} *}