diff -r ffd93dcc269d -r 8cd51a25a7ca ProgTutorial/FirstSteps.thy --- a/ProgTutorial/FirstSteps.thy Mon Mar 23 12:13:33 2009 +0100 +++ b/ProgTutorial/FirstSteps.thy Mon Mar 23 18:17:24 2009 +0100 @@ -180,7 +180,7 @@ into a @{ML_type cterm} using the function @{ML crep_thm}. *} -ML{*fun str_of_thm_raw ctxt thm = +ML{*fun str_of_thm ctxt thm = str_of_cterm ctxt (#prop (crep_thm thm))*} text {* @@ -188,7 +188,7 @@ @{text "?Q"} and so on. @{ML_response_fake [display, gray] - "warning (str_of_thm_raw @{context} @{thm conjI})" + "warning (str_of_thm @{context} @{thm conjI})" "\?P; ?Q\ \ ?P \ ?Q"} In order to improve the readability of theorems we convert @@ -203,15 +203,15 @@ thm' end -fun str_of_thm ctxt thm = +fun str_of_thm_no_vars ctxt thm = str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} text {* - Theorem @{thm [source] conjI} looks now as follows + Theorem @{thm [source] conjI} looks now as follows: @{ML_response_fake [display, gray] - "warning (str_of_thm_raw @{context} @{thm conjI})" - "\?P; ?Q\ \ ?P \ ?Q"} + "warning (str_of_thm_no_vars @{context} @{thm conjI})" + "\P; Q\ \ P \ Q"} Again the function @{ML commas} helps with printing more than one theorem. *} @@ -219,8 +219,8 @@ ML{*fun str_of_thms ctxt thms = commas (map (str_of_thm ctxt) thms) -fun str_of_thms_raw ctxt thms = - commas (map (str_of_thm_raw ctxt) thms)*} +fun str_of_thms_no_vars ctxt thms = + commas (map (str_of_thm_no_vars ctxt) thms) *} section {* Combinators\label{sec:combinators} *} @@ -305,9 +305,9 @@ |> (curry list_comb) f *} text {* - This code extracts the argument types of a given function and then generates + This code extracts the argument types of a given function @{text "f"} and then generates for each argument type a distinct variable; finally it applies the generated - variables to the function. For example + variables to the function. For example: @{ML_response_fake [display,gray] "apply_fresh_args @{term \"P::nat \ int \ unit \ bool\"} @{context} @@ -323,8 +323,8 @@ function @{ML variant_frees in Variable} generates for each @{text "z"} a unique name avoiding the given @{text f}; the list of name-type pairs is turned into a list of variable terms in Line 6, which in the last line is applied - by the function @{ML list_comb} to the function. We have to use the - function @{ML curry}, because @{ML list_comb} expects the function and the + by the function @{ML list_comb} to the function. In this last step we have to + use the function @{ML curry}, because @{ML list_comb} expects the function and the variables list as a pair. The combinator @{ML "#>"} is the reverse function composition. It can be @@ -525,7 +525,8 @@ @{text "> "}@{thm TrueConj_def} \end{isabelle} - (FIXME give a better example why bindings are important) + (FIXME give a better example why bindings are important; maybe + give a pointer to \isacommand{local\_setup}) While antiquotations have many applications, they were originally introduced in order to avoid explicit bindings for theorems such as: @@ -578,7 +579,7 @@ "@{term \"(x::nat) x\"}" "Type unification failed \"} - raises a typing error, while it perfectly ok to construct + raises a typing error, while it perfectly ok to construct the term @{ML [display,gray] "Free (\"x\", @{typ nat}) $ Free (\"x\", @{typ nat})"} @@ -659,7 +660,7 @@ ML{*fun make_wrong_imp P Q = @{prop "\(x::nat). P x \ Q x"} *} text {* - To see this apply @{text "@{term S}"} and @{text "@{term T}"} + To see this, apply @{text "@{term S}"} and @{text "@{term T}"} to both functions. With @{ML make_imp} you obtain the intended term involving the given arguments @@ -679,7 +680,7 @@ There are a number of handy functions that are frequently used for constructing terms. One is the function @{ML list_comb}, which takes - a term and a list of terms as argument, and produces as output the term + a term and a list of terms as arguments, and produces as output the term list applied to the term. For example @{ML_response_fake [display,gray] @@ -693,7 +694,7 @@ "lambda @{term \"x::nat\"} @{term \"(P::nat\bool) x\"}" "Abs (\"x\", \"nat\", Free (\"P\", \"bool \ bool\") $ Bound 0)"} - In the example @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), + In the example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), and an abstraction. It also records the type of the abstracted variable and for printing purposes also its name. Note that because of the typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"} @@ -710,8 +711,9 @@ have different type. There is also the function @{ML subst_free} with which terms can - be replaced by other terms. For example below we replace in @{term "f 0 x"} - the subterm @{term "f 0"} by @{term y} and @{term x} by @{term True}. + be replaced by other terms. For example below, we will replace in + @{term "(f::nat\nat\nat) 0 x"} + the subterm @{term "(f::nat\nat\nat) 0"} by @{term y}, and @{term x} by @{term True}. @{ML_response_fake [display,gray] "subst_free [(@{term \"(f::nat\nat\nat) 0\"}, @{term \"y::nat\nat\"}), @@ -1066,7 +1068,8 @@ @{ML_file "Pure/thm.ML"}. \end{readmore} - (FIXME: how to add case-names to goal states - maybe in the next section) + (FIXME: handy functions working on theorems; how to add case-names to goal + states - maybe in the next section) *} section {* Theorem Attributes *} @@ -1145,16 +1148,17 @@ \end{isabelle} As an example of a slightly more complicated theorem attribute, we implement - our version of @{text "[THEN \]"}. This attribute takes a list of theorems - as argument and resolves the proved theorem with this list (one theorem - after another). The code for this attribute is: + our 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 *} ML{*fun MY_THEN thms = Thm.rule_attribute (fn _ => fn thm => foldl ((op RS) o swap) thm thms)*} text {* - where @{ML swap} swaps the components of a pair. The setup of this theorem + 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 attribute uses the parser @{ML Attrib.thms}, which parses a list of theorems. *} @@ -1178,7 +1182,7 @@ @{text "> "}~@{thm test[MY_THEN sym eq_reflection]} \end{isabelle} - Of course, it is also possible to combine different theorem attributes, as in: + It is also possible to combine different theorem attributes, as in: \begin{isabelle} \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\ @@ -1186,7 +1190,7 @@ \end{isabelle} However, here also a weakness of the concept - of theorem attributes show through: since theorem attributes can be an + of theorem attributes shows through: since theorem attributes can be arbitrary functions, they do not in general commute. If you try \begin{isabelle} @@ -1198,8 +1202,8 @@ does not resolve with meta-equations. The purpose of @{ML Thm.rule_attribute} is to directly manipulate theorems. - Another usage of attributes is to add and delete theorems from stored data. - For example the attribute @{text "[simp]"} adds or deletes a theorem from the + 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 Thm.declaration_attribute}. To illustrate this function, let us introduce a reference containing a list of theorems. @@ -1229,12 +1233,13 @@ here it is sufficient that they just return the context unchanged. They change however the reference @{ML my_thms}, whereby the function @{ML Thm.add_thm} adds a theorem if it is not already included in the list, and @{ML - Thm.del_thm} deletes one. Both functions use the predicate @{ML - Thm.eq_thm_prop} which compares theorems according to their proved - propositions (modulo alpha-equivalence). + Thm.del_thm} deletes one (both functions use the predicate @{ML + Thm.eq_thm_prop}, which compares theorems according to their proved + propositions modulo alpha-equivalence). - You can turn both functions into attributes using + You can turn functions @{ML my_thms_add} and @{ML my_thms_del} into + attributes with the code *} ML{*val my_add = Thm.declaration_attribute my_thms_add @@ -1248,13 +1253,16 @@ "maintaining a list of my_thms" text {* - Now if you prove the lemma attaching the attribute @{text "[my_thms]"} + The parser @{ML Attrib.add_del} is a predefined parser for + adding and deleting lemmas. Now if you prove the next lemma + and attach the attribute + @{text "[my_thms]"} *} lemma trueI_2[my_thms]: "True" by simp text {* - then you can see the lemma is added to the initially empty list. + then you can see it is added to the initially empty list. @{ML_response_fake [display,gray] "!my_thms" "[\"True\"]"} @@ -1266,8 +1274,8 @@ text {* The @{text "add"} is the default operation and does not need - to be given. This declaration will cause the theorem list to be - updated as follows. + to be explicitly given. These two declarations will cause the + theorem list to be updated as: @{ML_response_fake [display,gray] "!my_thms" @@ -1292,7 +1300,8 @@ 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'' in a context by using the functor @{text GenericDataFun}: + start a ``data slot'', below called @{text MyThmsData}, by using the functor + @{text GenericDataFun}: *} ML {*structure MyThmsData = GenericDataFun @@ -1310,40 +1319,67 @@ val thm_del = MyThmsData.map o Thm.del_thm*} text {* - where @{ML MyThmsData.map} updates the data appropriately in the context. The - theorem addtributes are + 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 *} text {* - ad the setup is as follows + and the setup is as follows *} attribute_setup %gray my_thms2 = {* Attrib.add_del add del *} "properly maintaining a list of my_thms" -ML {* MyThmsData.get (Context.Proof @{context}) *} - -lemma [my_thms2]: "2 = Suc (Suc 0)" by simp +text {* + Initially, the data slot is empty -ML {* MyThmsData.get (Context.Proof @{context}) *} + @{ML_response_fake [display,gray] + "MyThmsData.get (Context.Proof @{context})" + "[]"} -ML {* !my_thms *} + but if you prove +*} + +lemma three[my_thms2]: "3 = Suc (Suc (Suc 0))" by simp text {* - (FIXME: explain problem with backtracking) + the lemma is now included + + @{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 + 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: +*} + +lemma four[my_thms]: "4 = Suc (Suc (Suc (Suc 0)))" by simp - Since storing - theorems in a special list is such a common task, there is the functor @{text NamedThmsFun}, - which does most of the work for you. To obtain such a named theorem lists, you just - declare +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 we 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! + + Since storing theorems in a special list is such a common task, there is the + functor @{text NamedThmsFun}, which does most of the work for you. To obtain + such a named theorem lists, you just declare *} ML{*structure FooRules = NamedThmsFun (val name = "foo" - val description = "Rules for foo"); *} + val description = "Rules for foo") *} text {* and set up the @{ML_struct FooRules} with the command