Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Various questions on theory vs. local_theory

Email Gateway (Aug 18 2022 at 19:31):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
I am currently trying to automate some definitions and subsequent proofs and
declarations. However, I am currently unsure how to go about with a few points
and I'd appreciate any help to point me in the right direction. By the way, I am
using the Isabelle repository version 29aa0c071875.

Here's what I am doing: I have implemented a function as a transformer of
local_theory. Given some parameters,

1. it constructs an Isabelle term and uses this to define a new constant using
   Local_Theory.define. Call the resulting theory lthy1.

2. From the definition, it proves some equations for simplification, adds them
   to a dynamic theorem list, and declares them as [iff]. This is the first bit
   which looks odd to me. Here are the details:

a) I use Goal.prove based on lthy1 to prove the simplification equations (say
simp_thm) whose term representation whose I have constructed using the ML
primitives.

b) Then, I add the proven theorems to the dynamic theorem list via
Local_Theory.declaration {syntax = false, pervasive=true} f
where f phi applies the morphism to the theorem to be stored (i.e. simp_thm)
before it updates the Generic_Data slot that manages the dynamic theorem list.
This gives lthy2.

c) Next, I declare thms as [iff] via

val lthy3 = Local_Theory.declaration {syntax=false, pervasive=false}
(fn phi => Thm.attribute_declaration (Clasimp.iff_add o Morphism.thm phi)
simp_thm) lthy2

For now, let lthy3 be the result of the whole function.

When I execute these steps inside a locale via local_setup, step c) outputs two
warnings each about duplicate rewrite rules and duplicate safe elimination rules
for the simp_thm. Is that normal? What should I do instead?

3. Next, I would like to register the newly defined constant as another datatype
   constructor for the code generator via Code.add_datatype. Unfortunately,
   Code.add_datatype is a theory morphism, not a local_theory transformer.

Anyway, the problem is that Code.add_datatype expects a list of constructor
names, i.e., the names that the constructors have in the background theory. How
can I obtain the global name of the newly defined constant?

4. Since the constructors for code generation have changed, I would also like to
   add the corresponding code equations for equal_class.equal, i.e., prove some
   code equations and declare them in the background theory as [code], i.e., using
   Code.add_eqn, which again is a theory transformer.

Am I right to assume that Local_Theory.background_theory converts that into a
transformer on the local_theory?
And how do I correctly export the code equations that I have proved in lthy1 to
the background theory?

I hope that the above description provides sufficient information about what I
am doing to answer my problems. If not, I could also post the full code, but it
is currently in a messy state.

Andreas

Last updated: Apr 23 2024 at 12:29 UTC