Re: [isabelle] Storing Data and naming theorems in ML

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


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
    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" ...


  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, 

 > Thanks,
 > Moa

