Email Gateway (Aug 22 2022 at 18:57): Email Gateway (Aug 22 2022 at 18:57):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
Recently, I started using the functionality of Isabelle/HOL that is
associated with "types to sets". However, I am not certain if I am using
this functionality in the most appropriate manner. Questions 1-3 are
general questions about the functionality of "types to sets" and its
applications in HOL; question 4 is specific to my application and not
directly related to "types to sets".
I would like to apologise in advance for asking questions 2 and 3 if the
answers to these questions are already available in the documentation or in
another post on the mailing list.
Theories Finite.thy and T2_Spaces.thy in the folder
HOL/Types_To_Sets/Examples contain the following line: "The aforementioned
development can be automated. The main part is already automated by the
transfer_prover.". This comment follows immediately after the specification
of the 'relativised' definitions and the transfer rules for these
definitions (e.g. lines 27-103 in the theory T2_Spaces.thy). I would like
to understand how exactly one should approach the automation of the
specification of the 'relativised' definitions and the transfer rules for
them. Indeed, some of the transfer rules that are used in my application do
not seem to be entirely trivial to prove. It would also be useful to be
able to generate definitions automatically. However, the aforementioned
examples do not elaborate on how this can be done. I would appreciate if
someone with experience in using 'types to sets' could provide an example
of an application of the automation to the lines 27-103 in the theory
T2_Spaces.thy.
At the moment I am in the process of the relativisation of several
theorems about topological spaces in HOL (e.g. results in
Analysis/Topology_Euclidean_Space). However, I am curious to know if
the main results about topological spaces have already been relativised
somewhere. If not, are there any plans to do it in the context of the
official development of HOL. I find it rather odd that the relativised
versions of theorems about topological spaces in HOL do not seem to be
available anywhere in the standard distribution (unless, of course, they
are and I am not being able to find them).
The final question is technical in nature and not directly related to
"types to sets". The theory Analysis/Topology_Euclidean_Space defines the
class "second_countable_topology". This class provides an explicit type
sort constraint in the specification of its assumptions:
class second_countable_topology = topological_space +
assumes ex_countable_subbasis:
"∃B::'a::topological_space set set. countable B ∧ open =
generate_topology B"
This seems to cause a problem when using "class.second_countable_topology"
as an explicit predicate. For example, anecdotally, it is possible to prove
definition "Sorgenfrey_Basis_ll = {x. x ∈ {x::real set. ∃a b. x = {a..<b}}}"
definition "Sorgenfrey_Line_ll = generate_topology Sorgenfrey_Basis_ll"
interpretation real : second_countable_topology "Sorgenfrey_Line_ll"
sorry
because the goal of the interpretation unfolds to 'class.topological_space
Sorgenfrey_Line_ll ∧ class.second_countable_topology_axioms TYPE(real)'
The same issue causes problems for other use cases of the
"class.second_countable_topology" as an explicit predicate (e.g. in the
specification of the transfer rules for a relativised definition following
the methodology in the example T2_Spaces.thy). Thus, I would like to
understand if there is any method that one can use to resolve the issue and
ensure that the "class.second_countable_topology" can be used as an
explicit predicate with the 'intended' meaning of 'open'.
Thank you
Email Gateway (Aug 22 2022 at 18:57):From: Lawrence Paulson <lp15@cam.ac.uk>
As it happens, I have been porting large sections of the HOL Light metric space library, which includes many results about topological spaces relativized to explicit topologies (as opposed to the topological_space type class). I have gradually been transferring these results into the Analysis library, where they will become visible in the development version of Isabelle and ultimately in the next release.
I’m interested in the “types to sets” mechanism, but I have never been able to figure it out.
Larry Paulson
Email Gateway (Aug 22 2022 at 18:57):From: Makarius <makarius@sketis.net>
Here is the initial NEWS entry from Isabelle2016-1 (December 2016):
That was the proof-of-concept implementation from the ITP2016 paper by
Ondrej Kuncar and Andrei Popescu.
There was still quite a lot missing for production quality. Already in
summer 2016 I had sent a many concrete hints to the authors to improve
the implementation, but hardly anything has happened since then.
More recently, Fabian Immler has polished this preliminary version a
bit, see NEWS in Isabelle2018 (August 2018):
Makarius
Email Gateway (Aug 22 2022 at 18:57):From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks. I hope it will be usable soon, though I’m not sure whether it will ever replace large-scale porting efforts such as the one I’m engaged in (as opposed to allowing one-off instantiations of important theorems within proofs).
Larry
Email Gateway (Aug 22 2022 at 18:57):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Professor Lawrence Paulson,
Thank you for your reply. If possible, I would like to understand if the
development work that you are referring to is related to the type
'topology' (line 19 in the theory Analysis/Abstract_Topology.thy in the
development version of Isabelle). In this case, of course, I am familiar
with some of the content of the theories that are related to this type.
Indeed, my intention is to use "types to sets" as an interface between the
type class 'topological_space' (and its subclasses) and the type 'topology'.
As a side note, I would like to clarify for anyone else who might wish to
provide any comments in relation to my original query that in Question 3 in
my email I am referring specifically to the relativisation of the results
about the type class 'topological_spaces' (and its subclasses) using the
methodology associated with "types to sets" (nevertheless, of course, any
further comments about similar developments are highly appreciated). Thus,
to be more specific, I would like to understand if anyone is using "types
to sets" for the relativisation of the results about the type class
'topological_spaces' (and its subclasses) to sets.
Thank you
Email Gateway (Aug 22 2022 at 18:57):From: Fabian Immler <immler@in.tum.de>
I am not using it, but I would like to use "types to sets" at some point
for the purpose of relativizing topological results.
Just recently (isabelle/ab5a8a2519b0), I added some more tooling towards
this goal: automatically defining unoverloaded constants from overloaded
definitions. A "print_theorems" after the unoverload_definition command
in src/HOL/Types_To_Sets/Examples/Unoverload_Def.thy should give an
intuition about what it is supposed to achieve.
Best regards,
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 18:58):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Fabian Immler,
Thank you for your reply.
Unfortunately, I did not update the repository immediately before asking
the question and it was several days out of date. Thus, I was not aware of
your work on 'unoverload_definition'. Indeed, the functionality that is
provided by this tool is very useful and partially answers Question 2 from
my original query. Also, I look forward to seeing your version of the
relativised results about the topological spaces in HOL.
To complete my understanding of the current status of the development of
"types to sets" (from the 'user' perspective), I would like to know if, at
the moment, it is necessary to prove the transfer rules for each definition
manually. It seems that for some definitions the goals for the transfer
rules are not trivial to prove automatically, i.e. it seems to be necessary
to use a substantial amount of code for such proofs (although, indeed, all
proofs follow a very similar outline). Perhaps, I am not familiar enough
with the methods that one would normally use for such proofs. For example,
the only method that I know that can be used to prove
inductive generate_topology_on :: "'a set set ⇒ 'a set ⇒ 'a set ⇒ bool"
for S :: "'a set set"
where
UNIV: "generate_topology_on S A A"
| Int: "generate_topology_on S A (a ∩ b)"
if "generate_topology_on S A a" and "generate_topology_on S A b" and
"a ⊆ A" and "b ⊆ A"
| UN: "generate_topology_on S A (⋃K)"
if "(⋀k. k ∈ K ⟹ k ⊆ A ⟹ generate_topology_on S A k)"
| Basis: "generate_topology_on S A s" if "s ∈ S" and "s ⊆ A"
lemma [transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total T" "bi_unique T"
shows
"((rel_set (rel_set T)) ===> (rel_set T ===> (=)))
(λB. generate_topology_on B (Collect (Domainp T))) generate_topology"
is induction used explicitly in both directions. The resulting proof is
over one hundred lines long. Therefore, it seems that the required effort
is not reasonable for something that should be possible to automate. Even
partial advice on either one of the queries in this paragraph will be
highly appreciated.
Thank you
Email Gateway (Aug 22 2022 at 19:00):From: Fabian Immler <immler@in.tum.de>
Hi ,
On 1/21/2019 5:59 PM, mailing-list anonymous wrote:
To complete my understanding of the current status of the development of
"types to sets" (from the 'user' perspective), I would like to know if, at
the moment, it is necessary to prove the transfer rules for each definition
manually.
In a way, yes. At the moment, you need to state the transfer rule for
each of your constants manually. For plain definitions, the method
"transfer_prover" will automatically prove those rules.
For definitions that involve e.g., choice, the situation is not so
clear. I guess it usually helps to define a similar constant that
defaults to a parametric value when the choice is non-unique.
See for example the definition of sum_with:
http://isabelle.in.tum.de/repos/isabelle/file/2755c387f1e6/src/HOL/Types_To_Sets/Examples/Group_On_With.thy#l290
It seems that for some definitions the goals for the transfer
rules are not trivial to prove automatically, i.e. it seems to be necessary
to use a substantial amount of code for such proofs (although, indeed, all
proofs follow a very similar outline). Perhaps, I am not familiar enough
with the methods that one would normally use for such proofs. For example,
the only method that I know that can be used to proveinductive generate_topology_on :: "'a set set ⇒ 'a set ⇒ 'a set ⇒ bool"
for S :: "'a set set"
where
UNIV: "generate_topology_on S A A"
| Int: "generate_topology_on S A (a ∩ b)"
if "generate_topology_on S A a" and "generate_topology_on S A b" and
"a ⊆ A" and "b ⊆ A"
| UN: "generate_topology_on S A (⋃K)"
if "(⋀k. k ∈ K ⟹ k ⊆ A ⟹ generate_topology_on S A k)"
| Basis: "generate_topology_on S A s" if "s ∈ S" and "s ⊆ A"lemma [transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total T" "bi_unique T"
shows
"((rel_set (rel_set T)) ===> (rel_set T ===> (=)))
(λB. generate_topology_on B (Collect (Domainp T))) generate_topology"is induction used explicitly in both directions.
Another option might be to prove transfer rules for lfp (like in the
attached Scratch.thy). It looks like the named theorems collection
"nitpick_unfold" contains definitions of inductive predicates in terms
of lfp (I am not sure where they come from, though). It could be that
this helps to carry out the proof without induction and in a more
principled way.
Fabian
Scratch.thy
smime.p7s
Email Gateway (Aug 22 2022 at 19:00):From: Fabian Immler <immler@in.tum.de>
Are you sure that this is the definition that you want?
Every set that is not a subset of the "carrier" A is in the topology:
lemma "generate_topology_on S A B" if "¬B ⊆ A"
using UN[of "{B}" A S] that
by simp
This probably won't play nicely with the topology type in
Abstract_Topology, which assumes that the carrier is the union of all
members of the topology.
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 19:00):From: Fabian Immler <immler@in.tum.de>
This does indeed lead to strange effects. I removed the sort constraint
in isabelle/7aafd0472661.
Fabian
smime.p7s
Email Gateway (Aug 22 2022 at 19:00):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear Fabian Immler/All,
Thank you for your replies.
At the moment, you need to state the transfer rule for
each of your constants manually. For plain definitions, the method
"transfer_prover" will automatically prove those rules.
Thank you for clarifying this. I believe that the comment "The
aforementioned development can be automated. The main part is already
automated by the transfer_prover." that could be found in some of the
examples in HOL/Types_To_Sets/Examples is slightly confusing. Initially, I
misinterpreted the comment "The aforementioned development can be
automated" as an indication that the functionality for automation was
already implemented in the context of the development of "types to sets",
but the examples do not show how this functionality can be used.
Another option might be to prove transfer rules for lfp (like in the
attached Scratch.thy). It looks like the named theorems collection
"nitpick_unfold" contains definitions of inductive predicates in terms
of lfp (I am not sure where they come from, though). It could be that
this helps to carry out the proof without induction and in a more
principled way.
Indeed, I suspected that my proof is naive. Also, thank you for pointing
out the existence of nitpick_unfold. I can foresee that the theorems from
this collection may be useful for other purposes.
Are you sure that this is the definition that you want?
Every set that is not a subset of the "carrier" A is in the topology:
lemma "generate_topology_on S A B" if "¬B ⊆ A"
using UN[of "{B}" A S] that
by simpThis probably won't play nicely with the topology type in
Abstract_Topology, which assumes that the carrier is the union of all
members of the topology.
Thank you for pointing out this 'impurity' in the definition. However, of
course, it was very easy to correct:
inductive generate_topology_on :: "'a set set ⇒ 'a set ⇒ 'a set ⇒ bool"
for S :: "'a set set"
where
UNIV: "generate_topology_on S A A"
| Int: "generate_topology_on S A (a ∩ b)"
if "generate_topology_on S A a" and "generate_topology_on S A b" and
"a ⊆ A" and "b ⊆ A"
| UN: "generate_topology_on S A (⋃K)"
if "K ⊆ Pow A" and "(⋀k. k ∈ K ⟹ generate_topology_on S A k)"
| Basis: "generate_topology_on S A s" if "s ∈ S" and "s ⊆ A"
lemma "generate_topology_on S A B ⟹ B ⊆ A"
by (induction rule: generate_topology_on.induct) auto
The issue was left unnoticed because I have not yet used the definition in
the context of the results about the type 'topology'. Thus far, it did not
cause any problems because the definition topological_space_on_with_def
from HOL/Types_To_Sets/Examples/T2_Spaces does not impose any restrictions
on the sets for which O holds true, provided that these sets are not
elements of the power set of A, e.g.
lemma "topological_space_on_with A (λx. x ∈ {{}, A} ∨ x = UNIV)"
unfolding topological_space_on_with_def by blast
In my own relativised theorems I restrict the statements to the carrier set
explicitly (following the outline presented in
HOL/Types_To_Sets/Examples/T2_Spaces), e.g.
lemma topological_basis_imp_subbasis_rel:
fixes "open" and B and A and S
assumes "topological_space_on_with A open"
and "B ⊆ Pow A"
and "topological_basis_on_with A open B"
and "S ⊆ A"
shows "open S = generate_topology_on B A S"
However, I wonder if some of the statements of the relativised theorems
could be simplified further if the definition topological_space_on_with
could guarantee that all open sets are in the power set of the carrier.
There is yet another minor issue that I would like to mention in the
context of the present discussion. The theorem compact_imp_closed_set_based
from the example HOL/Types_To_Sets/Examples/T2_Spaces is stated under the
assumption that the set A is not empty, i.e.
lemma compact_imp_closed_set_based:
assumes "(A::'a set) ≠ {}"
shows "∀open. t2_space_on_with A open ⟶ (∀S⊆A. compact_on_with A open S ⟶
closed_on_with A open S)"
However, the assumption "(A::'a set) ≠ {}" is redundant:
lemma compact_imp_closed_set_based_with_empty:
"∀open. t2_space_on_with A open ⟶
(∀S⊆A. compact_on_with A open S ⟶ closed_on_with A open S)"
proof(cases "A={}")
case True then show ?thesis
unfolding
t2_space_on_with_def
compact_on_with_def
closed_on_with_def
topological_space_on_with_def
by simp
next
case False then show ?thesis by (rule compact_imp_closed_set_based)
qed
In fact, many other relativised results about topological spaces hold even
if the carrier set is empty (e.g. see topological_basis_imp_subbasis_rel
above). In my view, it would be useful to mention this in the example
HOL/Types_To_Sets/Examples/T2_Spaces.
In conclusion, Questions 1 - 3 from my original query have now been
answered in full. Most certainly, it would be nice to see the 'official'
version of the relativised results about the topological spaces sooner
rather than later.
As a side note, I am still not certain as to whether there is a way to
interpret a type as a second_countable_topology (Question 4) with an
alternative predicate for 'open'. Of course, this issue is nearly
orthogonal to the main line of the inquiry.
Thank you
Email Gateway (Aug 22 2022 at 19:00):From: mailing-list anonymous <mailing.list.anonymous@gmail.com>
Dear All,
I would like to apologise for making the remark "As a side note, I am still
not certain as to whether there is a way to interpret a type as a
second_countable_topology (Question 4) with an alternative predicate for
'open'." in my last email.
The issue was resolved by Fabian Immler earlier today (
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-January/msg00074.html)
Therefore, all questions from my original inquiry were answered and I would
like to propose to close this topic. Of course, if anyone has anything to
add, I will appreciate further comments.
Thank you
Email Gateway (Aug 22 2022 at 19:01):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
As far as I know, proving these transfer rules explicitly has to be done manually,
though they are often easy to prove. The final deletion of the types via types-to-sets
is usually only a small last step that needs to be done. Therefore, I my opinion the
description in the initial Types-to-Sets paper is misleading as it, which indicates
a lot more automation.
I can further provide you with two developments where transfer + types-to-sets has been used
and can answer you questions on these developments. In both applications, we proved transfer
rules manually!
In AFP/Berlekamp_Zassenhaus there is quite a simple application of types-to-sets:
prime-fields are modeled via types first, and later on several algorithms that
work on types are basically copied to a setting where the prime is a term.
A description is available at https://dl.acm.org/citation.cfm?doid=3018610.3018617
and you can contact me personally for an extended (submitted) journal version.
In AFP/Perron_Frobenius there is a more involved setup where the type-based
Brouwer’s fixpoint theorem has been converted into a set-based version,
and where the HOL-Analysis vectors/matrices are connected to the ones in AFP/Jordan_Normal_Form.
The corresponding description is at https://dl.acm.org/citation.cfm?doid=3176245.3167103
Maybe, these examples are of interest.
Cheers,
René
signature.asc
Last updated: Nov 21 2024 at 12:39 UTC