Re: [isabelle] Locale Interpretation Question



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

Am 06.10.2011 04:39, schrieb Ashley Yakeley:
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


--
Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at kit.edu
http://pp.info.uni-karlsruhe.de
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.