## Stream: Beginner Questions

#### Nicolò Cavalleri (May 06 2021 at 10:41):

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?

#### Jakub Kądziołka (May 06 2021 at 10:47):

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`

#### Jakub Kądziołka (May 06 2021 at 10:47):

when you're defining `test_1`, you're outside of the `weird_topological_space`

#### Jakub Kądziołka (May 06 2021 at 10:48):

Take a look at how `group_hom` is defined here

#### Nicolò Cavalleri (May 06 2021 at 10:49):

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

#### Jakub Kądziołka (May 06 2021 at 10:49):

you need to provide the implicit parameters of the locale somehow

#### Jakub Kądziołka (May 06 2021 at 10:49):

I assume that you want to have two topological spaces involved

#### Jakub Kądziołka (May 06 2021 at 10:50):

if you only needed one, you could do `locale test_1 = weird_topological_space +` and `nbhds` would be in scope

#### Jakub Kądziołka (May 06 2021 at 10:51):

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

#### Nicolò Cavalleri (May 06 2021 at 11:14):

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

#### Nicolò Cavalleri (May 06 2021 at 11:24):

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!

#### Lukas Stevens (May 06 2021 at 11:26):

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?

#### Jakub Kądziołka (May 06 2021 at 11:36):

ah, ignore the ⊗, copy-paste mishap

#### Nicolò Cavalleri (May 06 2021 at 11:52):

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 (May 06 2021 at 11:53):

say `for X (structure) and Y (structure)` and add subscripts to invokations of `nbhds`

#### Nicolò Cavalleri (May 06 2021 at 12:00):

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"
``````

#### Nicolò Cavalleri (May 06 2021 at 12:03):

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"

#### Jakub Kądziołka (May 06 2021 at 12:09):

hmm, I do not understand why this is happening

#### Nicolò Cavalleri (May 06 2021 at 12:10):

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?

#### Jakub Kądziołka (May 06 2021 at 12:18):

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"
``````

#### Nicolò Cavalleri (May 06 2021 at 13:40):

What is happening in the parenthesis `("is'_openı _")`? I mean what is that and what is its role?

#### Nicolò Cavalleri (May 06 2021 at 13:45):

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"`

#### Jakub Kądziołka (May 06 2021 at 14:49):

ctrl+click on `partial_object` -- it is just a record field `carrier :: "'a set"`

#### Jakub Kądziołka (May 06 2021 at 14:49):

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

#### Jakub Kądziołka (May 06 2021 at 14:53):

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

#### Jakub Kądziołka (May 06 2021 at 14:54):

The carrier is your set `S`

#### Nicolò Cavalleri (May 06 2021 at 14:55):

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

#### Jakub Kądziołka (May 06 2021 at 14:56):

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

#### Jakub Kądziołka (May 06 2021 at 14:56):

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)"
``````

#### Jakub Kądziołka (May 06 2021 at 14:58):

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

#### Jakub Kądziołka (May 06 2021 at 14:59):

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

#### Jakub Kądziołka (May 06 2021 at 15:00):

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

#### Nicolò Cavalleri (May 07 2021 at 00:02):

Thank you very much!!

Last updated: Aug 13 2022 at 05:18 UTC