Stream: Beginner Questions

Topic: Bundle locale notation

view this post on Zulip Hanno Becker (Mar 07 2023 at 09:11):

Hi. I tried to bundle some locale-specific notation using bundle but get a bad context error. Defining the bundle outside of the locale does not work as desired because locale parameter are then explicit and have to be reflected in the syntax -- or so it seems. Is there a way to package locale-specific notation together?

view this post on Zulip Manuel Eberl (Mar 07 2023 at 09:22):

Can you give a minimal example to show what you tried?

view this post on Zulip Hanno Becker (Mar 07 2023 at 09:44):

Here's some dummy example:

definition dummy :: ‹'a ⇒ 'a› where
  ‹dummy x ≡ x›

locale foo =
  fixes bar :: ‹'a ⇒ 'b ⇒ 'c ⇒ bool›
begin
  abbreviation bar_with_dummy :: ‹'a ⇒ 'b ⇒ 'c ⇒ bool›
     where ‹bar_with_dummy a b c ≡ dummy (bar a b c)›

  abbreviation bar_no_dummy :: ‹'a ⇒ 'b ⇒ 'c ⇒ bool›
     where ‹bar_no_dummy a b c ≡ (bar a b c)›
end

bundle bar_notation_autodummy    begin notation    foo.bar_with_dummy ("_ ⋄ _ ↝ _") end
bundle bar_no_notation_autodummy begin no_notation foo.bar_with_dummy ("_ ⋄ _ ↝ _") end
bundle bar_notation_raw          begin notation    foo.bar_no_dummy   ("_ ⋄ _ ↝ _") end
bundle bar_no_notation_raw       begin no_notation foo.bar_no_dummy   ("_ ⋄ _ ↝ _") end

context foo
begin
  unbundle bar_notation_autodummy
  ―‹WANT: dummy (bar a b c)›
  ―‹GET: λca. dummy (a b c ca), because of locale parameter›
  term ‹a ⋄ b ↝ c›

  ―‹The notation should really be registered within the locale, but then it appears
    it can't be bundled: Bad context for command "bundle"⌂›
  bundle you_cant_do_that begin notation foo.bar_with_dummy ("_ ⋄ _ ↝ _") end
end

view this post on Zulip Manuel Eberl (Mar 07 2023 at 09:53):

Not an expert on locales and bundles but here's my best guess: I don't think this is possible. At least as of now, you can only use the bundle command in a restricted form inside local theory contexts, namely e.g. bundle foo = [[simp_trace, show_types]].

Now what you can do and what I think I've seen people do is just use a sublocale instead:

locale foo_with_notation = foo
begin
notation bar_with_dummy ("_ ⋄ _ ↝ _")
end

If you want the notation, you just interpret foo_with_notation in addition to foo.

view this post on Zulip Hanno Becker (Mar 07 2023 at 09:57):

Ah, that's an interesting workaround... I will have a look if that's feasible in my context. Thanks!

Last updated: Apr 25 2024 at 20:15 UTC