Re: [isabelle] Local_Theory.map_naming in locales



Hi Makarius,

Thanks for keeping this on the radar.

On 07/05/15 11:54, Makarius wrote:
Extra qualification of name bindings is possible in Isabelle/ML via Binding.qualified, but
there is no Isar syntax for it.  Naming prefixes in the name space are used by the system
in other situations.  Above the open question is what happens with the naming under
interpretation.

Moreover, many tools break down when they see more name prefixes than expected.  This is a
problem of these tools, but the usual reason why the system cannot move forward right now.
In my use case, I am not adding more levels of prefixes than would be there anyway, because I just want to emulate the effect of any other command.

Background: Why do I need this? The command inductive_set does not allow instantiations
in the parameters. Therefore, I first define my set foo as a predicate foop with
inductive and then manually perform the translation to sets as would be done with
inductive_set.

Can you point to the concrete definitions for this?
I stumbled over this limitation of inductive_set in JinjaThreads. In Isabelle2011-1, I used an inductive to actually define an inductive set, because 'a set and 'a => bool were the same at that time:
http://sourceforge.net/p/afp/afp-2011-1/ci/default/tree/thys/JinjaThreads/MM/JMM_Spec.thy#l113

When the two types were separated again, I converted the inductive into a function and manually derived all the necessary theorems, as can be seen in
http://sourceforge.net/p/afp/afp-2014/ci/default/tree/thys/JinjaThreads/MM/JMM_Spec.thy#l111

Of course, it would be great if the names were action_loc_aux.intros instead of action_loc_aux_intros etc.

I do not have a public real example in a locale, but I have attached a stripped-down version. By the way, it would be great if parameters for inductive(_set) that are always the same could be declared with for even if they are not the first ones (such as the x in the attached example).

Best,
Andreas

Attachment: Scratch.thy
Description: application/example



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