Stream: Beginner Questions

Topic: Using locales as "namespace"?


view this post on Zulip Max Kirchmeier (Oct 14 2020 at 11:39):

I would like to use locales as a kind of "namespace", to define functions for a general type first and then be able to concretize them for a number of different types after, like so:

locale Id =
  fixes t :: 'a
begin
definition id' :: "'a ⇒ 'a" where "id' ≡ id"
end

locale IdInt = Id "(0::int)"
locale IdNat = Id "(0::nat)"

And indeed, Id.id' is accessible at this point, but sadly IdInt.id' and IdNat.id are not.
What's the right way to go about this?

view this post on Zulip Mathias Fleury (Oct 14 2020 at 11:48):

why not use abbreviation for that?

view this post on Zulip Mathias Fleury (Oct 14 2020 at 11:49):

Max Kirchmeier said:
Id.id' is accessible at this point, but sadly IdInt.id' is not.

That is the behavior I expected from locales actually. If you don't introduce a new definition, why would a locale spontaneously introduce a new symbol?

view this post on Zulip Max Kirchmeier (Oct 14 2020 at 11:51):

Yes, that's precisely the problem, I would like the locale to introduce new symbols for things that have gotten "more concrete" :D
(I've also edited the first post to make it clear I want to be able to concretize the locale for a number of different types and not just one.)

view this post on Zulip Mathias Fleury (Oct 14 2020 at 11:55):

I am not sure why you would want to do that (you also have to duplicate all theorems)

view this post on Zulip Max Kirchmeier (Oct 14 2020 at 11:56):

Ah, I think I've solved it:

interpretation IdInt : Id "0::int"
  done

view this post on Zulip Mathias Fleury (Oct 14 2020 at 11:56):

ahahah no good try

view this post on Zulip Mathias Fleury (Oct 14 2020 at 11:56):

that lasts only in the current block

view this post on Zulip Max Kirchmeier (Oct 14 2020 at 11:57):

Mathias Fleury said:

I am not sure why you would want to do that (you also have to duplicate all theorems)

I want to do that because I have a number of operations that I would like to define for machine-words of different sizes simultaneously without re-defining everything for every word size.

view this post on Zulip Max Kirchmeier (Oct 14 2020 at 11:58):

Mathias Fleury said:

that lasts only in the current block

Also, it seems to work, IdInt.id' is accessible even in other theories :P

view this post on Zulip Mathias Fleury (Oct 14 2020 at 11:59):

Depends where it is defined:

locale IdInt
begin
interpretation H: Id where t = ‹0 :: int›
  .
lemma H: ‹H.id' x = x›
  sorry
end

context IdInt
begin
thm H
(*Id.id' ?x = ?x*)
end

view this post on Zulip Max Kirchmeier (Oct 14 2020 at 12:02):

Ah no, I'm not wrapping the interpretation in a locale:

locale Id =
  fixes t :: 'a
begin
definition id' :: "'a ⇒ 'a" where "id' ≡ id"

lemma id': "id' x = x" unfolding id'_def by simp
end

interpretation IdInt : Id "0::int"
  done

print_statement IdInt.id'

view this post on Zulip maximilian p.l. haslbeck (Oct 14 2020 at 12:03):

there is global_interpretation

view this post on Zulip Max Kirchmeier (Oct 14 2020 at 12:06):

maximilian p.l. haslbeck said:

there is global_interpretation

Yep, although interpretation seems to work the same when used at theory-level:

When used on the level of a global theory, there is no end of a
current context block, hence interpretation behaves identically to
global_interpretation then.


Last updated: Sep 25 2021 at 09:17 UTC