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 lineand 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:
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 notationThe 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