Hi Makarius, Thanks for keeping this on the radar. On 07/05/15 11:54, Makarius wrote:
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.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.
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: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?
http://sourceforge.net/p/afp/afp-2011-1/ci/default/tree/thys/JinjaThreads/MM/JMM_Spec.thy#l113When 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#l111Of 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).