# HG changeset patch # User Christian Urban # Date 1235739739 0 # Node ID 7e0bf13bf7431d7dd504bab208460ab9ee6b4905 # Parent cb39c41548bd775ee827c80b43054d58afe4968c added more material to the attribute section; merged the recipe about named theorems into the main body; added a solution to an exercise in the conversion section diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/FirstSteps.thy --- a/CookBook/FirstSteps.thy Thu Feb 26 14:20:52 2009 +0000 +++ b/CookBook/FirstSteps.thy Fri Feb 27 13:02:19 2009 +0000 @@ -894,8 +894,7 @@ theorem is proven. In particular, it is not possible to find out what are all theorems that have a given attribute in common, unless of course the function behind the attribute stores the theorems in a retrivable - datastructure. This can be easily done by the recipe described in - \ref{rec:named}. + datastructure. If you want to print out all currently known attributes a theorem can have, you can use the function: @@ -927,8 +926,7 @@ setup {* Attrib.add_attributes - [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] -*} + [("my_sym", Attrib.no_args my_symmetric, "applying the sym rule")] *} text {* The attribute does not expect any further arguments (unlike @{text "[OF @@ -949,28 +947,186 @@ @{text "> "}~@{thm test[my_sym]} \end{isabelle} + 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 + 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. *} +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 function @{ML Thm.declaration_attribute} expects us to + provide two functions that add and delete theorems from this list. At + the moment we use the two functions: +*} + +ML{*fun my_thms_add thm ctxt = + (my_thms := Thm.add_thm thm (!my_thms); ctxt) + +fun my_thms_del thm ctxt = + (my_thms := Thm.del_thm thm (!my_thms); ctxt)*} + text {* -What are: + These functions take a theorem and a context and, for what we are explaining + here it is sufficient to 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). -@{text "declaration_attribute"} + We can turn both functions into attributes using +*} + +ML{*val my_add = Thm.declaration_attribute my_thms_add +val my_del = Thm.declaration_attribute my_thms_del *} + +text {* + and set up the attributes as follows +*} + +setup {* + Attrib.add_attributes + [("my_thms", Attrib.add_del_args my_add my_del, + "maintaining a list of my_thms")] *} + +text {* + Now if you prove the lemma attaching 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. + + @{ML_response_fake [display,gray] + "!my_thms" "[\"True\"]"} + + We can also add theorems using the command \isacommand{declare} +*} + +declare test[my_thms] trueI_2[my_thms add] + +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. + + @{ML_response_fake [display,gray] + "!my_thms" + "[\"True\", \"Suc (Suc 0) = 2\"]"} + + The theorem @{thm [source] trueI_2} only appears once, since the + function @{ML Thm.add_thm} tests for duplicates, before extending + the list. Deletion from the list works as follows: +*} + +declare test[my_thms del] + +text {* After this, the theorem list is: + + @{ML_response_fake [display,gray] + "!my_thms" + "[\"True\"]"} + + We used in this example two functions declared as @{ML Thm.declaration_attribute}, + 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 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}: +*} -@{text "theory_attributes"} +ML {*structure Data = GenericDataFun + (type T = thm list + val empty = [] + val extend = I + fun merge _ = Thm.merge_thms) *} + +text {* + To use this data slot, we only have to change the functions @{ML my_thms_add} and + @{ML my_thms_del} to: +*} + +ML{*val thm_add = Data.map o Thm.add_thm +val thm_del = Data.map o Thm.del_thm*} + +text {* + where @{ML Data.map} updates the data appropriately in the context. 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"); *} + +text {* + and set up the @{ML_struct FooRules} with the command +*} + +setup {* 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. -@{text "proof_attributes"} + Furthermore, the facts are made available on the user level under the dynamic + fact name @{text foo}. For example we 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"} an 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"} and also + the recipe in Section~\ref{recipe:storingdata} about storing arbitrary + data. + \end{readmore} + + What are: + + @{text "theory_attributes"} + @{text "proof_attributes"} \begin{readmore} FIXME: @{ML_file "Pure/more_thm.ML"} @{ML_file "Pure/Isar/attrib.ML"} \end{readmore} - - *} -section {* Theories and Local Theories *} +section {* Theories, Contexts and Local Theories *} text {* (FIXME: expand) diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/Intro.thy --- a/CookBook/Intro.thy Thu Feb 26 14:20:52 2009 +0000 +++ b/CookBook/Intro.thy Fri Feb 27 13:02:19 2009 +0000 @@ -132,7 +132,7 @@ about parsing. \item {\bf Alexander Krauss} wrote the first version of the ``first-steps'' - chapter and also contributed recipe \ref{rec:named}. + chapter and also contributed the material on @{text NamedThmsFun}. \end{itemize} Please let me know of any omissions. Responsibility for any remaining diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/ROOT.ML --- a/CookBook/ROOT.ML Thu Feb 26 14:20:52 2009 +0000 +++ b/CookBook/ROOT.ML Fri Feb 27 13:02:19 2009 +0000 @@ -15,7 +15,6 @@ use_thy "Package/Ind_Code"; use_thy "Appendix"; -use_thy "Recipes/NamedThms"; use_thy "Recipes/Antiquotes"; use_thy "Recipes/TimeLimit"; use_thy "Recipes/Config"; diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/Recipes/NamedThms.thy --- a/CookBook/Recipes/NamedThms.thy Thu Feb 26 14:20:52 2009 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,80 +0,0 @@ -theory NamedThms -imports "../Base" -begin - -section {* Accumulate a List of Theorems under a Name\label{rec:named} *} - - -text {* - {\bf Problem:} - Your tool @{text foo} works with special rules, called @{text foo}-rules. - Users should be able to declare @{text foo}-rules in the theory, - which are then used in a method.\smallskip - - {\bf Solution:} This can be achieved using named theorem lists.\smallskip - - Named theorem lists can be set up using the code - - *} - -ML{*structure FooRules = NamedThmsFun ( - val name = "foo" - val description = "Rules for foo"); *} - -text {* - and the command -*} - -setup {* FooRules.setup *} - -text {* - This code declares a context data slot where the theorems are stored, - an attribute @{text foo} (with the usual @{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 we 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"} an 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"} and also - the recipe in Section~\ref{recipe:storingdata} about storing arbitrary - data. - \end{readmore} - *} - -text {* - (FIXME: maybe add a comment about the case when the theorems - to be added need to satisfy certain properties) - -*} - - -end - - - - diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/Solutions.thy --- a/CookBook/Solutions.thy Thu Feb 26 14:20:52 2009 +0000 +++ b/CookBook/Solutions.thy Fri Feb 27 13:02:19 2009 +0000 @@ -1,5 +1,6 @@ theory Solutions imports Base +uses "infix_conv.ML" begin chapter {* Solutions to Most Exercises *} @@ -90,9 +91,50 @@ \begin{minipage}{\textwidth} @{subgoals [display]} - \end{minipage} + \end{minipage}\bigskip +*}(*<*)oops(*>*) + +text {* \solution{ex:addconversion} *} + +text {* + (FIXME This solution works but is awkward.) +*} + +ML{*fun add_conv ctxt ctrm = + (case Thm.term_of ctrm of + @{term "(op +)::nat \ nat \ nat"} $ _ $ _ => + (let + val eq1 = Conv.binop_conv (add_conv ctxt) ctrm; + val ctrm' = Thm.rhs_of eq1; + val trm' = Thm.term_of ctrm'; + val eq2 = Conv.rewr_conv (get_sum_thm ctxt trm' (dest_sum trm')) ctrm' + in + Thm.transitive eq1 eq2 + end) + | _ $ _ => Conv.combination_conv + (add_conv ctxt) (add_conv ctxt) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => add_conv ctxt) ctxt ctrm + | _ => Conv.all_conv ctrm) + +val add_tac = CSUBGOAL (fn (goal, i) => + let + val ctxt = ProofContext.init (Thm.theory_of_cterm goal) + in + CONVERSION + (Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (add_conv ctxt) then_conv + Conv.concl_conv ~1 (add_conv ctxt))) ctxt) i + end)*} + +lemma "P (Suc (99 + 1)) ((0 + 0)::nat) (Suc (3 + 3 + 3)) (4 + 1)" + apply(tactic {* add_tac 1 *})? +txt {* + where the simproc produces the goal state + + \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage}\bigskip *}(*<*)oops(*>*) - end \ No newline at end of file diff -r cb39c41548bd -r 7e0bf13bf743 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Thu Feb 26 14:20:52 2009 +0000 +++ b/CookBook/Tactical.thy Fri Feb 27 13:02:19 2009 +0000 @@ -662,17 +662,20 @@ also described in \isccite{sec:results}. \end{readmore} - A similar but less powerful function than @{ML SUBPROOF} is @{ML SUBGOAL}. - It allows you to inspect a given subgoal. With this you can implement - a tactic that applies a rule according to the topmost logic connective in the - subgoal (to illustrate this we only analyse a few connectives). The code - of the tactic is as follows.\label{tac:selecttac} + Similar but less powerful functions than @{ML SUBPROOF} are @{ML SUBGOAL} + and @{ML CSUBGOAL}. They allow you to inspect a given subgoal (the former + presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type + cterm}). With this you can implement a tactic that applies a rule according + to the topmost logic connective in the subgoal (to illustrate this we only + analyse a few connectives). The code of the tactic is as + follows.\label{tac:selecttac} + *} -ML %linenosgray{*fun select_tac (t,i) = +ML %linenosgray{*fun select_tac (t, i) = case t of - @{term "Trueprop"} $ t' => select_tac (t',i) - | @{term "op \"} $ _ $ t' => select_tac (t',i) + @{term "Trueprop"} $ t' => select_tac (t', i) + | @{term "op \"} $ _ $ t' => select_tac (t', i) | @{term "op \"} $ _ $ _ => rtac @{thm conjI} i | @{term "op \"} $ _ $ _ => rtac @{thm impI} i | @{term "Not"} $ _ => rtac @{thm notI} i @@ -727,8 +730,7 @@ the first goal. To do this can result in quite messy code. In contrast, the ``reverse application'' is easy to implement. - The tactic @{ML "CSUBGOAL"} is similar to @{ML SUBGOAL} except that it takes - a @{ML_type cterm} instead of a @{ML_type term}. Of course, this example is + Of course, this example is contrived: there are much simpler methods available in Isabelle for implementing a proof procedure analysing a goal according to its topmost connective. These simpler methods use tactic combinators, which we will @@ -1013,7 +1015,7 @@ *} -section {* Rewriting and Simplifier Tactics *} +section {* Simplifier Tactics *} text {* @{ML rewrite_goals_tac} @@ -1458,7 +1460,7 @@ Here the conversion of @{thm [source] true_conj1} only applies in the first case, but fails in the second. The whole conversion - does not fail, however, because the combinator @{ML else_conv} will then + does not fail, however, because the combinator @{ML Conv.else_conv} will then try out @{ML Conv.all_conv}, which always succeeds. Apart from the function @{ML beta_conversion in Thm}, which is able to fully @@ -1600,8 +1602,8 @@ in CONVERSION (Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (if_true1_conv ctxt)) then_conv - Conv.concl_conv ~1 (all_true1_conv ctxt)) ctxt) i + (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv + Conv.concl_conv ~1 (all_true1_conv ctxt))) ctxt) i end)*} text {* @@ -1629,15 +1631,23 @@ and simprocs; the advantage of conversions, however, is that you never have to worry about non-termination. + \begin{exercise}\label{ex:addconversion} + Write a tactic that is based on conversions which does the same as the simproc in + exercise \ref{ex:addsimproc}, that is replaces terms of the form @{term "t\<^isub>1 + t\<^isub>2"} + by their result. You can make the same assumptions as in \ref{ex:addsimproc}. + \end{exercise} + \begin{readmore} See @{ML_file "Pure/conv.ML"} for more information about conversion combinators. Further conversions are defined in @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/drule.ML"} and @{ML_file "Pure/meta_simplifier.ML"}. \end{readmore} + *} + section {* Structured Proofs *} text {* TBD *} diff -r cb39c41548bd -r 7e0bf13bf743 cookbook.pdf Binary file cookbook.pdf has changed