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"

Well, first, `scale`

is not defined through a *definition*. Instead it is an arbitrary constant that has 4 properties (`scale_add`

, `add_scale`

, `scale_scale`

, and `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