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

Dear Makarius Wenzel/All,

Thank you for you reply. I would be very interested in learning more about
the concrete feedback that you provided in 2016 and 2017. Has it been
published anywhere? Would it be possible to provide any hyperlinks to this

I would also like to provide feedback with regard to your concerns about my

   1. I have already mentioned on this mailing list that I can provide my
   name/real contact details upon request, with the understanding that you
   agree not mention them on the mailing list. In fact, I have recently edited
   my signature for this email account to include this information. Given that
   you expressed your concerns about my identity and possibility of me being
   involved in mischief, I will send you a letter from the email that I
   normally use for professional correspondence later today. Of course, if I
   will ever make an attempt to submit any of my work to the AFP, it will be
   under my real name.
   2. There is a number of reasons why I do not wish to disclose my
      1. In the past, I had problems with spam and online/telephone scam. I
      had to close two email accounts, one Skype account and had to change my
      mobile telephone number twice. I can only assume that I was
targeted due to
      a combination of my country of origin (Eastern Europe) and
having some kind
      of public profile at a certain point in my life. Some people will go
      through great lengths if they suspect that you have money and may be,
      somehow, susceptible to share it :).
      2. At the moment, Isabelle/formal proof is merely a hobby for me.
      Given that I have no publications in this area, I would prefer potential
      employers not to know too much about my involvement in this area, given
      that most of my previous experience was in an area that was not closely
      related. I believe that I will become more forthcoming about my
      if I will ever submit anything to the AFP.
      3. I have further, slightly more personal reasons, for not wishing to
      disclose my identity publicly.
   3. While I have no evidence, I can only guess that there may be poorly
   written articles on wikipedia that were written by people who disclosed
   their identities. However, I have little doubt that there are also many
   good contributions from people who did not wish to disclose their
   identities. For what it is worth, I have seen published articles in
   academic journals of good standing that were (many years after their
   publication) shown to contain substantial errors and served to cause great
   confusion. Also, there are many regular users of Stack Overflow who
   provided good answers without disclosing their identities.
   4. We owe Bitcoin to an anonymous contributor :).

Thank you

On Mon, Apr 15, 2019 at 3:08 PM mailing-list anonymous <
mailing.list.anonymous at> wrote:

> 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> 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> 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.

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 MHonArc.