# [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.*