Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Locale Interpretation Question

Email Gateway (Aug 18 2022 at 18:30):

From: Ashley Yakeley <ashleyy@microsoft.com>
Hi, how do I express "if V is a vector space, then V is an affine space on
V" given this locale for affine spaces? Note that vector_space is also a
locale. I know how to show something is an interpretation of my affine_space
locale if that something is a class instead of a locale.

theory Affine
imports RealVector
begin

locale affine_space =
vector_space scale for scale ::"'a::field ⇒ 'b::ab_group_add ⇒ 'b" +
fixes affplus :: "'b ⇒ 'f ⇒ 'f"
fixes affminus :: "'f ⇒ 'f ⇒ 'b"
assumes affine_zero [simp]: "affplus 0 p = p"
and affine_assoc [simp]: "affplus v (affplus w p) = affplus (v + w) p"
and affine_invert_1 [simp]: "affplus (affminus q p) p = q"
and affine_invert_2 [simp]: "affminus (affplus v p) p = v"

end

Email Gateway (Aug 18 2022 at 18:30):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi Ashley,

there are in several ways to do that.

1. "sublocale" for locales is the analogue of "subclass" for type classes, see
   the tutorial on locales, section 4. Thus, you could write

sublocale vector_space < affine_space
"space"
"implementation for affplus"
"implementation for affminus"

followed by a proof that your implementations for affplus and affminus satisfy
the assumptions. Although this is the standard way, it does not work in your
case because affine_space is already a sublocale of vector_space, as the former
inherits from the latter. Therefore, after this declaration, the context
vector_space may no longer be opened.

2. Instead, section 7.1 of the locale tutorial applies. Declare a new locale
   that collects all facts about vector spaces viewed as affine spaces.

locale vector_space_as_affine_space = vector_space
sublocale vector_space_as_affine_space < affine_space
"space"
"implementation_for_affplus"
"implementation_for_affminus"

3. If you only seldomly need to refer to vector spaces as affine spaces, it
   might be a good idea (for performance reasons) not to declare the sublocale
   relation. In that case, you want to prove a lemma in vector_space that allows
   you to quickly interpret affine_space whenever needed:

lemma (in vector_space) affine_space:
"affine_space space
(implementation_for_affplus) (implementation_for_affminus)"

Then, whenever you need a fact F from affine_space in a proof of vector_space,
either locally interpret affine_space

lemma ...
proof
interpret affine_space
"space"
"implementation for affplus"
"implementation for affminus"
by(rule affine_space)
note F
qed

or bypass the locale mechanism and work on the foundational layer directly, i.e.

note affine_space.F[OF affine_space]

Hope this helps,
Andreas

Last updated: Nov 21 2024 at 12:39 UTC