Re: [isabelle] Local_Theory.map_naming in locales



Hi Andreas,

> context begin
> local_setup â Local_Theory.map_naming (Name_Space.mandatory_path "foo") â
> lemma bar: "bar â True" ..
> end
> 
> Unfortunately, this does not seem to work when I am inside a locale.
> 
> locale test = assumes *: True begin
> context begin
> local_setup â Local_Theory.map_naming (Name_Space.mandatory_path "foo") â
> lemma bar: "bar â True" ..
> end
> 
> Now, the theorem names "bar", "local.bar", and "test.foo.bar" are
> available. I would have expected "foo.bar", "local.foo.bar", and
> "test.foo.bar", but the first two do not exist.

Having a look at Local_Theory.map_naming this is quite obvious

fun map_naming f =
  map_top (fn (naming, operations, after_close, brittle, target) =>
    (f naming, operations, after_close, brittle, target));

I.e. only the topmost context in the stack of local theories is affected.

It is unclear to me what can be done in our current infrastructure to
achieve the desired effect.  I will spend some time to understand this
occasionally.

	Florian



> 
> Moreover, when I later interpret test, the foo prefix does not show up
> either. What is the recommended way to install such mandatory prefixes?
> What am I doing wrong here?
> 
> 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. To get the same
> names (foo.intros, foo.cases, ...), I open an unnamed context, add the
> mandatory prefix foo to the name space with map_naming and transfer the
> theorems for foop using [pred_to_set]. This works fine at the theory level.
> 
> Best,
> Andreas
> 

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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