I have the following code, which is not the original but just a mwe to recreate the problem I have:

```
theory Scratch
imports Main
begin
locale weird_topological_space = fixes S :: "'a set" and is_open :: "'a set ⇒ bool"
assumes open_space [simp, intro]: "is_open S" and open_empty [simp, intro]: "is_open {}"
and open_imp_subset: "is_open U ⟹ U ⊆ S"
and open_inter [intro]: "⟦is_open U; is_open V⟧ ⟹ is_open (U ∩ V)"
and open_union [intro]: "⋀F::('a set) set. (⋀x. x ∈ F ⟹ is_open x) ⟹ is_open (⋃x∈F. x)"
begin
definition nbhds :: "'a ⇒ 'a filter"
where "nbhds a = (INF S∈{S. is_open S ∧ a ∈ S}. principal S)"
end
definition pippo :: "'a ⇒ 'a filter"
where "pippo a = (INF S∈{S. a ∈ S}. principal S)"
locale test_1 =
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes has_derivative_hd: "filterlim f (nbhds y) (nbhds x)"
(* Type unification failed
Type error in application: incompatible operand type
Operator: nbhds :: 'b ⇒ 'b filter
Operand: x :: 'a *)
locale test_2 =
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes has_derivative_hd: "filterlim f (pippo y) (nbhds x)"
locale test_3 =
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes has_derivative_hd: "filterlim f (pippo y) (pippox)"
end
```

and for some reason test 2 and 3 work, whereas test 1 does not. It is as if for some reason the function `is_open`

does not allow the function `nbhds`

to change type in different instances.

Does anybody know why?

as you can see by the identifier being blue, the `nbhds`

in `test_1`

is a free variable, it does not refer to the definition in `weird_topological_space`

when you're defining `test_1`

, you're outside of the `weird_topological_space`

Take a look at how `group_hom`

is defined here

Ok ops that was a stupid mistake, sorry I am not used to Isabelle colors! How can I use it outside?

you need to provide the implicit parameters of the locale somehow

I assume that you want to have two topological spaces involved

if you only needed one, you could do `locale test_1 = weird_topological_space +`

and `nbhds`

would be in scope

if you do need two, you'll need to give explicit names to the topological spaces and then use `nbhds⊗⇘T⇙`

and `nbhds⊗⇘U⇙`

(again, see the `group_hom`

example

Thank you very much for your help! I am trying to imitate the example you linked. Now it recognizes `nbhds`

but it still have a type overloading problem: if I replace `test_1`

above with

```
locale test_1 =
X?: weird_topological_space X + Y?: weird_topological_space Y
for X and Y +
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes at_mem_x : "x ∈ X"
and at_mem_y : "y ∈ Y"
and lim: "filterlim f (nbhds x) (nbhds y)"
(* Type unification failed
Type error in application: incompatible operand type
Operator: (∈) y :: 'b set ⇒ bool
Operand: Y :: 'a set *)
```

I get the above error. What am I doing wrong this time? Again it is as if it forces both topological spaces to be built on the same type

Also I am not sure what the symbols in `nbhds⊗⇘T⇙`

are! Is it something important? I can't find anything about this notation in the online tutorial on locales!

This is like `\<sub>`

but you are allowed to use multiple characters (`\<bsub>`

...`\<esub>`

). Additionally, you are allowed to use parameters inside this notation, which is not allowed for `\<sub>`

. The notation is not displayed correctly but there are patches for jEdit flying around @Mohammad Abdulaziz?

ah, ignore the ⊗, copy-paste mishap

Nicolò Cavalleri said:

I get the above error. What am I doing wrong this time? Again it is as if it forces both topological spaces to be built on the same type

@Jakub Kądziołka do you by chance know anything about this?

say `for X (structure) and Y (structure)`

and add subscripts to invokations of `nbhds`

I added `(structure)`

, but as for subscripts, the error comes out even if I remove the line about nbhds: it comes out for the line

```
and at_mem_y : "y ∈ Y"
```

Also I tried to add subscripts your way, with \<bsub> and \<esub> but Isabelle does not seem to recognize them, it says ```
Inner syntax error⌂
Failed to parse prop
```

. I don't really know how subscripts work in isabelle and they don't appear to be in any tutorial: neither `prog-prove`

nor "A proof Assistant for Higher-Order Logic"

hmm, I do not understand why this is happening

Nicolò Cavalleri said:

I added

`(structure)`

, but as for subscripts, the error comes out even if I remove the line about nbhds: it comes out for the line`and at_mem_y : "y ∈ Y"`

You mean this right?

Looks like locales with multiple parameters aren't behaving like they should. I'd suggest posting on the mailing list. Meanwhile you can package up your topological space into a record like HOL-Algebra does:

```
theory Scratch
imports Main "HOL-Algebra.Congruence"
begin
record 'a weird_topological_space = "'a partial_object" +
is_open :: "'a set ⇒ bool" ("is'_openı _")
locale weird_topological_space = fixes S (structure)
assumes open_space [simp, intro]: "is_open (carrier S)"
begin
end
locale test_1 =
X?: weird_topological_space X + Y?: weird_topological_space Y
for X (structure) and Y (structure) +
fixes f :: "'a ⇒ 'b" and x y
assumes at_mem_x : "x ∈ carrier X"
and at_mem_y : "y ∈ carrier Y"
```

What is happening in the parenthesis `("is'_openı _")`

? I mean what is that and what is its role?

Also do you know about somewhere where I can read more about how are locales related to records? I don't really understand what is going on and I can't manage to get rid of the carriers, I mean I'd just like to write `S :: 'a set`

instead of `"'a partial_object"`

ctrl+click on `partial_object`

-- it is just a record field `carrier :: "'a set"`

using this common definition lets you use HOL-Algebra and your definitions without having to disambugate the meaning of `carrier`

Nicolò Cavalleri said:

What is happening in the parenthesis

`("is'_openı _")`

? I mean what is that and what is its role?

Right. The motivation is that `is_open`

needs an argument which is the record (topological space) itself. This is the role of the `structure`

mechanism:

- If a variable has been defined with
`fixes X (structure)`

or`for X (structure)`

(with optional type signature before the parenthesis), it can be used as a subscript in a place corresponding to a`ı`

in notation - if only one structure is in scope, the structure parameter will be inferred

The carrier is your set `S`

What is the ' after "is" in `is'_open`

?

the `'`

is an escape character — unescaped, an underscore indicates an argument. Think `if _ then _ else _`

BTW, I realized why your earlier example wasn't working. This works:

```
locale test_1 =
X?: weird_topological_space X open_in_X + Y?: weird_topological_space Y open_in_Y
for X open_in_X Y and open_in_Y +
fixes f :: "'a ⇒ 'b" and x :: 'a and y :: 'b
assumes at_mem_x : "x ∈ X"
and at_mem_y : "y ∈ Y"
and lim: "filterlim f (Y.nbhds y) (X.nbhds x)"
```

note that you need to do `for <set> and <open predicate for that set>`

, and provide both to `weird_topological_space`

, as only both values at once can define a topological space

This is why records are so common — a record is essentially a tuple where its elements have been named

Nicolò Cavalleri said:

Also do you know about somewhere where I can read more about how are locales related to records? I don't really understand what is going on and I can't manage to get rid of the carriers, I mean I'd just like to write

`S :: 'a set`

instead of`"'a partial_object"`

I guess I wrote some notes on how and why abstract structures like these are defined by Isabelle as they are: https://github.com/NieDzejkob/isabelle-math-contests/blob/master/NOTES.md#abstract-algebra

Thank you very much!!

Last updated: Oct 13 2024 at 01:36 UTC