*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)*From*: mailing-list anonymous <mailing.list.anonymous at gmail.com>*Date*: Mon, 15 Apr 2019 15:08:27 +0300*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <2916445A-23D1-4327-A0E0-984D80462BCA@cam.ac.uk>*References*: <CALaF1UKm=Jky1977K-yu+62fhMujt+yVpevdd5kmYP5c-uyXoQ@mail.gmail.com> <2916445A-23D1-4327-A0E0-984D80462BCA@cam.ac.uk>

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 very impressive. 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 approach are 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 fewer loc. 3. Uniform 'software' structure for all algebraic structures and abstract spaces. 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 _" [81] 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 -⇩o⇩w b" 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 constructors). Thank you 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. > > Larry > > > 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 > functionality > > 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 > and > > 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.

**Follow-Ups**:

**References**:**[isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)***From:*mailing-list anonymous

**Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
- Next by Date: [isabelle] FTfJP 2019: Second Call for Papers
- Previous by Thread: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
- Next by Thread: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)
- Cl-isabelle-users April 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list