Hi, I have a very stupid but weird question. If I get the locale like that:
locale real_vector_space = abelian_group V add zero for V and add (infixl "+" 70) and zero ("𝟬") + fixes scale:: "real ⇒ 'a ⇒ 'a" (infixr "⋅⇩ℝ" 75) assumes scale_add: "⟦x ∈ V; y ∈ V⟧ ⟹ r ⋅⇩ℝ (x + y) = r ⋅⇩ℝ x + r ⋅⇩ℝ y" and add_scale: "x ∈ V ⟹ (r + s) ⋅⇩ℝ x = r ⋅⇩ℝ x + s ⋅⇩ℝ x" and scale_scale: "x ∈ V ⟹ r ⋅⇩ℝ s ⋅⇩ℝ x = (r * s) ⋅⇩ℝ x" and one_scale: "x ∈ V ⟹ 1 ⋅⇩ℝ x = x"
then how can I prove
x ∈ V ⟹ r ⋅⇩ℝ x ∈ V
since I find it nothing feedback when I code like "using scale_def"
scale is not defined through a definition. Instead it is an arbitrary constant that has 4 properties (
one_scale). Hence there is no definition (I don't even see what you expect here).
And for you actual question, you need to assume that
⋅⇩ℝ stays in
V. If you look at the module definition in the Isabelle Library (
~~/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy), this is what it is done:
locale module_on = fixes S and scale :: "'a::comm_ring_1 \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75) assumes [...] and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
Thanks, I got it. let me think a while
@zibo yang As pointed out by Mathias, in
locale real_vector_space the closure property of
scale has been forgotten and needs to be added among the assumptions within the locale.
Last updated: Sep 25 2022 at 23:25 UTC