Suppose I wanted to define the type of local homeomorphisms in the context of `Abstract_topology`

. I cannot transform this:

```
definition is_chart :: "'a topology ⇒ 'e topology ⇒ 'a set ⇒ 'e set ⇒ ('a ⇒ 'e) ⇒ ('e ⇒ 'a)
⇒ bool" where
"is_chart Ta Te A E f g ≡ openin Ta A ∧ openin Te E ∧
homeomorphic_maps (subtopology Ta A) (subtopology Te E) f g"
```

into a type with fixed topologies right? I mean using `typedef`

with some trick.

I gave up on fixing the topologies, but why does this:

```
import Analysis.Abstract_topology
definition is_chart :: "'a topology ⇒ 'e topology ⇒ 'a set ⇒ 'e set ⇒ ('a ⇒ 'e) ⇒ ('e ⇒ 'a)
⇒ bool" where
"is_chart Ta Te A E f g ≡ openin Ta A ∧ openin Te E ∧
homeomorphic_maps (subtopology Ta A) (subtopology Te E) f g"
typedef (overloaded) ('a, 'e) chart =
"{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
is_chart Ta Te A E f g}"
by (rule exI[where x="(discrete_topology, discrete_topology, {}, {}, (λx. undefined),
(λx. undefined))"]) simp
setup_lifting type_definition_chart
```

not work?

How about this one?

```
typedef (overloaded) ('a, 'e) chart =
"{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
is_chart Ta Te A E f g}"
apply (rule exI[where x="(discrete_topology {}, discrete_topology {}, {},
{}, (λx. undefined),(λx. undefined))"])
unfolding is_chart_def homeomorphic_maps_def by auto
```

It works thank you very much! I am puzzeld though (apart from the fact that I forgot to add something after `discrete_topology`

): if I write this

```
typedef (overloaded) ('a, 'e) chart =
"{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
is_chart Ta Te A E f g}"
apply (rule exI[where x="(discrete_topology {}, discrete_topology {}, {},
{}, (λx. undefined),(λx. undefined))"])
```

and then I run sledgehammer it does not find a proof. Is it normal?

Also, `setup_lifting type_definition_chart`

gives a warning

```
Generation of a parametrized correspondence relation failed.
Reason: No relator for the type "Abstract_Topology.topology" found.
```

but the code works fine. Should I worry about it?

Nicolò Cavalleri said:

and then I run sledgehammer it does not find a proof. Is it normal?

Yes, it is normal. Sledgehammer is bad when the goal is of higher-order nature (i.e., functions as arguments). Generally, Sledgehammer is a bit unpredictable -- it may fail at some goal that appears easy to us, but sometimes it can exceed our expectation by succeeding on extremely challenging problems.

Also I wonder why the last lemma in this mwe

```
typedef (overloaded) ('a, 'e) chart =
"{(Ta::'a topology, Te::'e topology, A::'a set, E::'e set, f, g).
openin Ta A ∧ openin Te E ∧ homeomorphic_maps (subtopology Ta A) (subtopology Te E) f g}"
apply (rule exI[where x="(discrete_topology {}, discrete_topology {}, {},
{}, (λx. undefined),(λx. undefined))"])
unfolding homeomorphic_maps_def by auto
setup_lifting type_definition_chart
lift_definition apply_chart::"('a, 'e) chart ⇒ 'a ⇒ 'e"
is "λ(Ta, Te, A, E, f, g). f" .
declare [[coercion apply_chart]]
lift_definition inv_chart::"('a, 'e) chart ⇒ 'e ⇒ 'a"
is "λ(Ta, Te, A, E, f, g). g" .
lift_definition source_topology::"('a, 'e) chart ⇒ 'a topology"
is "λ(Ta, Te, A, E, f, g). Ta" .
lift_definition range_topology::"('a, 'e) chart ⇒ 'e topology"
is "λ(Ta, Te, A, E, f, g). Te" .
lift_definition domain::"('a, 'e) chart ⇒ 'a set"
is "λ(Ta, Te, A, E, f, g). A" .
lift_definition codomain::"('a, 'e) chart ⇒ 'e set"
is "λ(Ta, Te, A, E, f, g). E" .
subsection ‹Properties›
lemma open_domain[intro, simp]: "openin (source_topology c) (domain c)"
and open_codomain[intro, simp]: "openin (range_topology c) (codomain c)"
and chart_homeomorphism: "homeomorphic_maps (subtopology (source_topology c) (domain c))
(subtopology (range_topology c) (codomain c)) c (inv_chart c)"
by (transfer, auto)+
lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
by (rule at_within_open[OF that open_domain])
```

does not work...

Wenda Li said:

Nicolò Cavalleri said:

and then I run sledgehammer it does not find a proof. Is it normal?

Yes, it is normal. Sledgehammer is bad when the goal is of higher-order nature (i.e., functions as arguments). Generally, Sledgehammer is a bit unpredictable -- it may fail at some goal that appears easy to us, but sometimes it can exceed our expectation by succeeding on extremely challenging problems.

Ok thank you very much!

Nicolò Cavalleri said:

Also,

`setup_lifting type_definition_chart`

gives a warning`Generation of a parametrized correspondence relation failed. Reason: No relator for the type "Abstract_Topology.topology" found.`

but the code works fine. Should I worry about it?

There might be a problem if you want to use the **lift and transfer framework** sometimes later. If you don't plan to use that framework, `setup_lifting type_definition_chart`

is actually not necessary.

Wenda Li said:

Nicolò Cavalleri said:

Also,

`setup_lifting type_definition_chart`

gives a warning`Generation of a parametrized correspondence relation failed. Reason: No relator for the type "Abstract_Topology.topology" found.`

but the code works fine. Should I worry about it?

There might be a problem if you want to use the

lift and transfer frameworksometimes later. If you don't plan to use that framework,`setup_lifting type_definition_chart`

is actually not necessary.

I do plan to use (you can see my use in the mwe) it but it works despite the warning!

Nicolò Cavalleri said:

Also I wonder why the last lemma in this mwe

`...`

does not work...

The problem is that these proofs should be super easy but Isabelle does not find them automatically and apparently I am not able to write any proof by hand, I can only use auto simp fastforce and sledgehammer

Nicolò Cavalleri said:

I do plan to use (you can see my use in the mwe) it but it works despite the warning!

Yes, I just saw that. It is nice that `transfer`

works so far. You may need to work out those relator stuff when it fails.

Wenda Li said:

Nicolò Cavalleri said:

I do plan to use (you can see my use in the mwe) it but it works despite the warning!

Yes, I just saw that. It is nice that

`transfer`

works so far. You may need to work out those relator stuff when it fails.

Yep I would not know how to do that because I do not know either abstract topology nor the transfer package but I will ask for help here in case!

Nicolò Cavalleri said:

The problem is that these proofs should be super easy but Isabelle does not find them automatically and apparently I am not able to write any proof by hand, I can only use auto simp fastforce and sledgehammer

That is the idea of **interactive** theorem proving and the difference between us and those ATPs -- we can always learn to proceed when automation fails even though we may proceed at a mush slower pace :-)

Wenda Li said:

Nicolò Cavalleri said:

The problem is that these proofs should be super easy but Isabelle does not find them automatically and apparently I am not able to write any proof by hand, I can only use auto simp fastforce and sledgehammer

That is the idea of

interactivetheorem proving and the difference between us and those ATPs -- we can always learn to proceed when automation fails even though we may proceed at a mush slower pace :-)

Yeah actually I saw the problem in my proof... the theorem `at_within_open`

does not apply here.

As for

```
lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
by (rule at_within_open[OF that open_domain])
```

Your `at_within_open[OF that open_domain]`

is not valid. The proof can be fixed if you can prove `open (domain c)`

(I am not sure if it is provable or not):

```
lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c"
proof -
have "open (domain c)" sorry
then show ?thesis using at_within_open[OF that] by auto
qed
```

Wenda Li said:

As for

`lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c" by (rule at_within_open[OF that open_domain])`

Your

`at_within_open[OF that open_domain]`

is not valid. The proof can be fixed if you can prove`open (domain c)`

(I am not sure if it is true or not):`lemma at_within_domain: "at x within domain c = at x" if "x ∈ domain c" proof - have "open (domain c)" sorry then show ?thesis using at_within_open[OF that] by auto qed`

No I think it is not true but hopefully I should manage to recover a proof if someone who knows well Abstract topology will answer me in the thread `Filters in abstract topology`

Thank you very much though!

Last updated: Sep 25 2022 at 22:23 UTC