[isabelle] Locale Interpretation Question



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

--
Ashley Yakeley






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