# [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.
```
Andreas

--
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
http://pp.info.uni-karlsruhe.de
```
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.