# HG changeset patch # User Christian Urban # Date 1237892978 -3600 # Node ID d3cd633e82404256f92c6bc3ea03dac6cbf65ac8 # Parent 096776f180fcb73019b62eadbf98e41decdf0fc9 some polishing 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} *} diff -r 096776f180fc -r d3cd633e8240 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Tue Mar 24 09:34:03 2009 +0100 +++ b/ProgTutorial/Intro.thy Tue Mar 24 12:09:38 2009 +0100 @@ -56,7 +56,7 @@ Then of course there is: \begin{description} - \item[The code.] Which is the ultimate reference for how + \item[The code.] It is the ultimate reference for how things really work. Therefore you should not hesitate to look at the way things are actually implemented. More importantly, it is often good to look at code that does similar things as you want to do and @@ -145,8 +145,8 @@ \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' chapter and also contributed the material on @{text NamedThmsFun}. - \item {\bf Christian Sternagel} proof read the tutorial and made - comments. + \item {\bf Christian Sternagel} proofread the tutorial and made + comments on the text. \end{itemize} Please let me know of any omissions. Responsibility for any remaining diff -r 096776f180fc -r d3cd633e8240 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Tue Mar 24 09:34:03 2009 +0100 +++ b/ProgTutorial/Parsing.thy Tue Mar 24 12:09:38 2009 +0100 @@ -563,6 +563,8 @@ Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}. *} +section {* Argument and Attribute Parsers (TBD) *} + section {* Parsing Inner Syntax *} text {* @@ -722,9 +724,11 @@ text_raw {* \begin{exercise} - If you look closely how @{ML SpecParse.where_alt_specs} is implemented - in file @{ML_file "Pure/Isar/spec_parse.ML"} and compare it to our @{ML "spec_parser"}, - you can notice an additional ``tail'' (Lines 8 to 10): + Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented + in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds + to the ``where-part'' of the introduction rules given above. Below + we paraphrase the code of @{ML SpecParse.where_alt_specs} adapted to our + purposes. \begin{isabelle} *} ML %linenosgray{*val spec_parser' = @@ -739,14 +743,16 @@ OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} text_raw {* \end{isabelle} - What is the purpose of this additional ``tail''? + Both parsers accept the same input, but if you look closely, you can notice + an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of + this additional ``tail''? \end{exercise} *} section {* New Commands and Keyword Files\label{sec:newcommand} *} text {* - (FIXME: update to the right command setup) + (FIXME: update to the right command setup --- is this still needed) Often new commands, for example for providing new definitional principles, need to be implemented. While this is not difficult on the ML-level, @@ -847,7 +853,7 @@ You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"} and add the line - @{text [display] "use_thy \"Command\";"} + @{text [display] "no_document use_thy \"Command\";"} to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing: @@ -1005,27 +1011,33 @@ section {* Methods *} text {* - Methods are a central concept in Isabelle. They are the ones you use for example + (FIXME: maybe move to after the tactic section) + + Methods are a central to Isabelle. They are the ones you use for example in \isacommand{apply}. To print out all currently known methods you can use the Isabelle command: -*} -print_methods + \begin{isabelle} + \isacommand{print\_methods}\\ + @{text "> methods:"}\\ + @{text "> -: do nothing (insert current facts only)"}\\ + @{text "> HOL.default: apply some intro/elim rule (potentially classical)"}\\ + @{text "> ..."} + \end{isabelle} -text {* An example of a very simple method is: *} method_setup %gray foobar_meth = {* Scan.succeed (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} - "foobar method" + "foobar method for conjE and conjI" text {* It defines the method @{text foobar_meth}, which takes no arguments (therefore the - parser @{ML Scan.succeed}) and - only applies the tactic @{thm [source] conjE} and then @{thm [source] conjI}. - This method can be used in the following proof + parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which + applies @{thm [source] conjE} and then @{thm [source] conjI}. The function @{ML SIMPLE_METHOD} + turns such a tactic into a method. @{text "Foobar_meth"} can be used as follows *} lemma shows "A \ B \ C \ D" diff -r 096776f180fc -r d3cd633e8240 progtutorial.pdf Binary file progtutorial.pdf has changed