Re: [isabelle] Storing Generic_Data in a local theory



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 of
documentation, I decided to use the well-documented old-fashioned way of doing
things. 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




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