Stream: Beginner Questions

Topic: Access fixed constants from locale interpretation

Alicia (Oct 17 2023 at 15:09):

Hi,

having a locale "L" that fixes some constant "c" and an interpretation "intp" of that locale L, is there a way to access the instantiated/interpreted c without explicitly using the instantiating term?

I tried using "intp.c", but that is either undefined or I'm doing sth. wrong.

Thanks a lot in advance :)

Mathias Fleury (Oct 18 2023 at 06:48):

There is no way to do that

Mathias Fleury (Oct 18 2023 at 06:49):

but in general you should avoid instantiating with complex terms anyway, because the simplifier can simplify them and break the entire local mechanism.

Mathias Fleury (Oct 18 2023 at 06:52):

locale L =
  fixes n :: nat
  assumes n: "n ≥ 1"
begin

definition double where "double = n + n"
lemma T: "double > 0"
  using n unfolding double_def by simp
end

interpretation test: L "0+1"
  by unfold_locales auto

lemma ‹0 < test.double›
  apply simp
(*goal involves L.double (Suc 0), not expected at all!*)

Mathias Fleury (Oct 18 2023 at 06:53):

so introducing definition is often the best way to both instantiate and later refer to the term

Alicia (Oct 18 2023 at 14:26):

Alright, thanks for the example! :-)

Last updated: Dec 21 2024 at 16:20 UTC