Stream: Archive Mirror: Isabelle Users Mailing List

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

Email Gateway (Aug 19 2022 at 13:45):

From: Moa Johansson <moa.johansson@chalmers.se>
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}) *}

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?

Thanks,
Moa

Email Gateway (Aug 19 2022 at 13:45):

From: Christian Urban <christian.urban@kcl.ac.uk>
Hi Moa,

Last updated: Apr 19 2024 at 08:19 UTC