Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
Dear Lawrence Paulson/All,
Thank you for your reply.
I have followed the development of HOL-Analysis in the last several months.
Indeed, the work that is being done in the context of this development is
Thank you for your kind words about my work. However, of course, the credit
for the development of Types-To-Sets belongs to the authors of the original
article and the credit for the development of the methodology that I am
using belongs to Fabian Immler and Bohua Zhan.
With my application of Types-To-Sets, I wanted to obtain a mathematics
library that is based entirely on classes and locales and uses a uniform
('software') structure both for algebraic structures and abstract spaces.
The main library of Isabelle/HOL, effectively, already achieves this goal.
However, the carrier sets for all structures are UNIVs. Types-To-Sets
allows for a nearly seamless conversion of each class/locale that treats
the carrier sets as UNIV to an equivalent locale with an explicitly defined
carrier set in a semi-automated manner. The main selling points of this
1. Both explicit carrier sets and UNIV are treated in a uniform manner
(also, my intention, is to introduce a database that relates the
relativised and non-relativised theorems somehow).
2. The results about explicit carrier sets are obtained from the results
about UNIV in a semi-automatic manner, which implies less typing and
3. Uniform 'software' structure for all algebraic structures and
4. It promotes the development of the main Isabelle/HOL library.
To elaborate on clause 3, please see the comparison of the locale
topological_space_ow (relativisation of the class topological_space from
the theory Topological_Spaces) and the locale group_add_ow (relativisation
of the class group_add from the theory Groups):
locale topological_space_ow =
fixes 𝔘 :: "'at set" and τ :: "'at set ⇒ bool"
assumes open_UNIV[simp, intro]: "τ 𝔘"
assumes open_Int[intro]: "⟦ S ⊆ 𝔘; T ⊆ 𝔘; τ S; τ T ⟧ ⟹ τ (S ∩ T)"
assumes open_Union[intro]: "⟦ K ⊆ Pow 𝔘; ∀S∈K. τ S ⟧ ⟹ τ (⋃K)"
locale group_add_ow =
minus_ow 𝔘 minus + uminus_ow 𝔘 uminus + monoid_add_ow 𝔘 plus zero
for 𝔘 :: "'ag set"
and plus (infixl "⇧+⇩o⇩w" 65)
and minus (infixl "-⇩o⇩w" 65)
and uminus :: "'ag ⇒ 'ag" ("-⇩o⇩w _"  80)
and zero ("0⇩o⇩w") +
assumes left_inverse: "a ∈ 𝔘 ⟹ (-⇩o⇩w a) ⇧+⇩o⇩w a = 0⇩o⇩w"
and add_inv_conv_diff: "⟦ a ∈ 𝔘; b ∈ 𝔘 ⟧ ⟹ a ⇧+⇩o⇩w (-⇩o⇩w b) = a
As you can guess, it is now a very small step to provide the relativisation
of the class topological_group_add on an explicit carrier set.
Please accept my apologies for another sales pitch. The main reason why I
am drawing so much attention to the development is that there is no other
way for me to find out whether or not someone else is doing something
similar, which is, of course, a grave concern to me.
As a side note, I noticed that my previous email contains a great number of
typographical errors (normally, I do not confuse types and type
On Mon, Apr 15, 2019 at 1:02 PM Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> Let me just offer my enthusiastic encouragement for you to continue!
> I have never managed to figure out how Types-To-Sets can be used, despite
> scrutinising example developments, so you deserve full credit simply for
> that. It definitely needs to be made more usable.
> Meanwhile the next release will contain tens of thousands of lines of new
> material about relativised concepts, not using Types-To-Sets but simply
> with new proofs ported from HOL Light. This is independent from your work,
> of course, but maybe the efforts can eventually be combined.
> > On 13 Apr 2019, at 12:06, mailing-list anonymous <
> mailing.list.anonymous at gmail.com> wrote:
> > I would like to ask a question in relation to the further development of
> > the functionality of the framework "Types-To-Sets".
> > I am working on several personal projects that rely on "Types-To-Sets".
> > However, as was previously noted on the mailing list, the framework does
> > have its limitations. I would be interested in improving the
> > of the framework. However, before I do any work in this direction I would
> > like to understand if anyone else is already working towards this goal
> > whether or not there exists a development plan for this framework.
> > Naturally, if anyone has any particular ideas about how the framework can
> > be improved, I would be interested in learning about them.
Please accept my apologies for posting anonymously. This is done to protect
my privacy. I can make my identity and my real contact details available
upon request in private communication under the condition that they are not
to be mentioned on the mailing list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and