*To*: isabelle-users at cl.cam.ac.uk, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Storing Generic_Data in a local theory*From*: Richard Molitor <gattschardo at googlemail.com>*Date*: Thu, 12 Mar 2015 18:38:52 +0100 (CET)*In-reply-to*: <alpine.LNX.2.03.1503121556440.4559@localdomain.local>*References*: <alpine.LNX.2.03.1503071953420.13118@localdomain.local> <550177AB.205@informatik.tu-muenchen.de> <alpine.LNX.2.03.1503121556440.4559@localdomain.local>*User-agent*: Alpine 2.03 (LNX 1266 2009-07-14)

Hello again, I managed to implement the suggested morphsim variant to some success now, thanks to your example! On Thu, 12 Mar 2015, Richard Molitor wrote:

Put differently: * Your data is of a certain type T. * You explain how a fundamental morphism phi is applied to a value of type T by giving a suitable lifting f :: morphism -> T -> T * Then your declaration for a particular x :: T looks as follows: fun decl phi = Data.put (f phi x) Unfortunately, there is no elaborate section on this in the implementation manual yet.I will look into this. I had seen the morphisms before, but given the lack ofdocumentation, I decided to use the well-documented old-fashioned way ofdoingthings. Maybe reading functor.ML will enlighten me, thanks for the pointer!

What somewhat worries me is that I end up ignoring the morphism argument completely, since it can contain thms and terms and (I think) they do not affect the outcome of my commands, since they are just storing data. When I figure out which additional thms may affect my commands though, this way at least the infrastructure is in place in contrast to just storing in the background theory as I did before [1], so I think I stick with this for now. In the last part of the linked commit, I have a local_theory_to_proof command. What I do now is store the result I get in after_qed using background_theory, I could not get declaration to work here: No matter how I produce the initial generic context, either from the local or the background theory, I somehow always end up needing the other variant in the end. Richard [1]: https://github.com/gattschardo/open-inductive/commit/62a4bd010e91540a00427b18c5a5656f57686591

**Follow-Ups**:**Re: [isabelle] Storing Generic_Data in a local theory***From:*Andreas Lochbihler

**References**:**[isabelle] Storing Generic_Data in a local theory***From:*Richard Molitor

**Re: [isabelle] Storing Generic_Data in a local theory***From:*Florian Haftmann

**Re: [isabelle] Storing Generic_Data in a local theory***From:*Richard Molitor

- Previous by Date: Re: [isabelle] Rearranging equations before taking limits
- Next by Date: Re: [isabelle] Storing Generic_Data in a local theory
- Previous by Thread: Re: [isabelle] Storing Generic_Data in a local theory
- Next by Thread: Re: [isabelle] Storing Generic_Data in a local theory
- Cl-isabelle-users March 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list