[isabelle] Various questions on theory vs. local_theory

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.


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Am Fasanengarten 5, Geb. 50.34, Raum 025
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.