*To*: Ashley Yakeley <ashleyy at microsoft.com>*Subject*: Re: [isabelle] Locale Interpretation Question*From*: Andreas Lochbihler <andreas.lochbihler at kit.edu>*Date*: Thu, 06 Oct 2011 08:07:02 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <j6j4d8$2nm$1@dough.gmane.org>*References*: <j6j4d8$2nm$1@dough.gmane.org>*User-agent*: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7

Hi Ashley, there are in several ways to do that.

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

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

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

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

**References**:**[isabelle] Locale Interpretation Question***From:*Ashley Yakeley

- Previous by Date: [isabelle] Locale Interpretation Question
- Next by Date: [isabelle] syntax, translations
- Previous by Thread: [isabelle] Locale Interpretation Question
- Next by Thread: [isabelle] syntax, translations
- Cl-isabelle-users October 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list