*To*: Moa Johansson <moa.johansson at chalmers.se>*Subject*: Re: [isabelle] Storing Data and naming theorems in ML*From*: Christian Urban <christian.urban at kcl.ac.uk>*Date*: Fri, 7 Feb 2014 18:50:14 +0000*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*References*: <211E8B13-134F-4987-AD7A-E60CB2B2C8F9@chalmers.se>*Reply-to*: christian.urban at kcl.ac.uk

Hi Moa, On Friday, February 7, 2014 at 17:20:16 (+0000), Moa Johansson wrote: > Hello again, > > I've got another few implementational questions, just to make sure I get things the right way around. > > 1) My application discovers and proves some new lemmas that it > thinks might be useful, so these need to be stored suitably, in > some Theory_Data for the current theory. So far so good, following > the instructions in section 2.5 of the Isabelle > Cookbook/programming tutorial. However, I would like to be able to > update my collection of useful lemmas programatically, but in the > tutorial, it is only shown how to do this using the Isar command > "setup", e.g. as below: > > setup {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *} The answer to your question depends how you want your code to be "called" by the user. If your discovery of theorems is part of an initialisation without any user interaction, then setup (or local_setup) is really the point of entry. For example at the beginning of HOL.thy you have a section where data is initialised for the iprover. In these "sections" you are expected to provide a function from local_theory to local_theory (or thy to thy for setup). This can be seen as a transaction where you get a (local) theory as input and need to provide a new (local) theory, where your function has done your modifications to it - for example adding new theorems. If this is the situation you have in mind, then you can use the function Local_Theory.note in order to install new theorems. These theorems will be visible under a name you can choose. For example local_setup {* let fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd in my_note @{binding "foo_conjI"} @{thm conjI} #> my_note @{binding "bar_conjunct1"} @{thm conjunct1} #> my_note @{binding "bar_conjunct2"} @{thm conjunct2} end *} "re-introduces" the theorems conjI etc under some silly names. You can replace conjI with any theorem you prove. If your discovery is in "response" to some command the user types in, then essentially the parser of this command gives you a local theory and you are expected to make your modifications to this local theory. Finally you "hand back" the theory to the parser. The Programming Tutorial describes this in section 7.2 for a command called simple_inductive. > Presumably there must be an ML function corresponding to setup somewhere? > > > 2) I would like to also give individual nice names to my > automatically discovered lemmas. What is the procedure for doing > this? Again there a few options. If you discover a theorem, or theorems, then you can give them a name when you "install" them into the current theory with the function Local_Theory.note. This corresponds roughly to the situation where a user gives a theorem a name, say foo_name lemma foo_name: shows "False" ... If you want that your discovered theorems to be part of collection of theorems known under a single name, then you can use the functor Named_Thms. For example this snippet installs a collection under the name "foo". ML {* structure FooRules = Named_Thms (val name = @{binding "foo"} val description = "Theorems for foo") *} setup {* FooRules.setup *} The user can expand this list by writing lemma [foo]: "False" ... or declare [foo add] ... declare [foo del] ... You as ML-programmer can expand this collection with the FooRules.add_thm. Again the necessary local_theory (or thy) you get via local_setup or by the "command" you are implementing. Hope this is helpful, Christian > > > Thanks, > Moa > --

**References**:**[isabelle] Storing Data and naming theorems in ML***From:*Moa Johansson

- Previous by Date: [isabelle] Storing Data and naming theorems in ML
- Next by Date: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Previous by Thread: [isabelle] Storing Data and naming theorems in ML
- Next by Thread: [isabelle] Want a type of non-negatives for a field, to work like nat/int
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list