Stream: Beginner Questions

Topic: Using locales as "namespace"?

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?

Mathias Fleury (Oct 14 2020 at 11:48):

why not use abbreviation for that?

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?

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.)

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)

Max Kirchmeier (Oct 14 2020 at 11:56):

Ah, I think I've solved it:

interpretation IdInt : Id "0::int"
  done

Mathias Fleury (Oct 14 2020 at 11:56):

ahahah no good try

Mathias Fleury (Oct 14 2020 at 11:56):

that lasts only in the current block

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.

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

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

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'

maximilian p.l. haslbeck (Oct 14 2020 at 12:03):

there is global_interpretation

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: Apr 19 2024 at 08:19 UTC