diff -r c0cae24b9d46 -r 5dffcab68680 ProgTutorial/General.thy --- 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 \}"}}. 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 \}"}}. 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