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, Larry and Anonymous Contributor,

I thank you for your support of, and contribution to the types-to-sets methodology. I believe the underlying local typedef rule is a very useful (yet gentle) upgrade of HOL, and have always advocated its candidacy for HOL citizenship. (Incidentally, one of my original motivations was to simplify our BNF/(co)datatype package constructions back in 2011, but in the end the package was developed without it.)

However, I cannot help with making the types-to-sets machinery more user-friendly since I am not fluent in Isabelle/ML. It is Ondrej Kuncar who has implemented the local typedef rule and the accompanying "unoverloading" rule. And since Ondrej is also a co-developer of the lifting and transfer package, he is in an ideal position to make things happen; or to share some insights with people who might be interested in taking on such a development. Without more progress on this front, only power-users will use types-to-sets -- this is a shame, since types-to-sets could be part of the regular users' daily menu.

Best wishes,


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Makarius <makarius at>
Sent: 15 April 2019 11:26
To: Lawrence Paulson; cl-isabelle-users at
Subject: Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)

On 15/04/2019 12:02, Lawrence Paulson 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.

Recall that it is just an experiment to support a research paper in 2016
by Ondřej Kunčar and Andrei Popescu;;sdata=eRLNFLsiaQEq%2B%2BtqlqThR%2B3q9BUGUg1YCEijWZWDYeE%3D&amp;reserved=0

In 2016 and 2017 I have provided a lot of concrete feedback on the
implementation to turn it into more usable state (e.g. proper use of
Isar context commands), but somehow the project seems to have become

In the meantime Fabian Immler has made some improvements, but it is
still only experimental.

Overall, there is also a high-level question about the use (or better
non-use of Types-To-Set). It is based on a genuine extension of the HOL
logic, and I am unsure what other HOL users say about it. For me this
discussion is still pending.

Meta note: I am not communicating with people that don't expose there
real name. I have just seen a bit too many recent reports about
anonymous authors doing mischief on Wikipedia.

A proper open-source project works like scientific research, by people
who stand with their own name and reputation for what they do and describe.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.