Stream: Beginner Questions

Topic: Is it possible to expose sublocale namespace?

view this post on Zulip James Hanson (Apr 01 2024 at 19:39):

I want to be able to access definitions and facts inherited via a sublocale relationship outside of the context of the locale, but this doesn't seem work automatically. Here's an example of what I'm talking about:

locale foo =
  fixes
    foo :: 'a and
    f :: "'a \<Rightarrow> 'a"
  assumes
    foo_fixed: "f foo = foo"

abbreviation (in foo)
  f5 :: "'a \<Rightarrow> 'a"
  where "f5 x \<equiv> f (f (f (f (f x))))"

locale bar =
  fixes
    bar :: 'b and
    g :: "'b \<Rightarrow> 'b"
  assumes
    bar_fixed: "g (g bar) = bar"

sublocale bar \<subseteq> double: foo bar "g \<circ> g"
  by (simp add: bar_fixed foo.intro)

context bar
begin
  term "double.f5"
  (* Returns:
  * "double.f5"
  *   :: "'b \<Rightarrow> 'b" *)
end

  term "bar.double.f5"
  (* Returns:
  *   Undefined constant: "bar.double.f5" *)

Is it possible to access double.f5 when not in the context of the bar locale? If so what is the right way to do it?

view this post on Zulip Mathias Fleury (Apr 01 2024 at 19:53):

...
definition (in foo)
  f5 :: "'a ⇒ 'a"
  where "f5 x ≡ f (f (f (f (f x))))"

...
context bar
begin
term "f5"

thm double.f5_def
  (* Returns:
  * "double.f5"
  *   :: "'b ⇒ 'b" *)
lemmas test = double.f5_def
end

thm bar.test
(*
bar ?bar ?g ⟹ foo.f5 (?g ∘ ?g) ?x ≡ (?g ∘ ?g) ((?g ∘ ?g) ((?g ∘ ?g) ((?g ∘ ?g) ((?g ∘ ?g) ?x))))

sublocales do not define constants
*)

view this post on Zulip Mathias Fleury (Apr 01 2024 at 20:00):

And with rewrites:

locale foo =
  fixes
    foo :: 'a and
    f :: "'a ⇒ 'a"
  assumes
    foo_fixed: "f foo = foo"

definition (in foo)
  f5 :: "'a ⇒ 'a"
  where "f5 x ≡ f (f (f (f (f x))))"

locale bar =
  fixes
    bar :: 'b and
    g :: "'b ⇒ 'b"
  assumes
    bar_fixed: "g (g bar) = bar"

definition (in bar) bar_f5 where
  ‹bar_f5 x = (g ∘ g) ((g ∘ g) ((g ∘ g) ((g ∘ g) ((g ∘ g) x))))›

sublocale bar ⊆ double: foo bar "g ∘ g"
  rewrites "double.f5 = bar_f5"
  subgoal by (auto simp add: bar_fixed bar_f5_def foo.intro
      intro!: ext)
  subgoal ―‹prove the rewrites›
    using foo.f5_def[of bar ‹g o g›]
    by (auto simp add: bar_fixed bar_f5_def foo.intro
      intro!: ext)
  done

context bar
begin
term "f5"

thm double.f5_def
  (* Returns:
  * "double.f5"
  *   :: "'b ⇒ 'b" *)
lemmas test = double.f5_def
end

thm bar.test

Last updated: May 07 2024 at 04:19 UTC