[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

Fri Aug 12 11:26:18 CEST 2011

Hi all,

On 08/11/2011 02:43 PM, Florian Haftmann wrote:
> What is your opinion?

The grass is always greener on the other side...

Instead of stating an opinion, let me recall the parts of the story so
far that I know, to avoid that history repeats itself. I am sure that
Stefan will add some interesting details, too. (He wrote to me that it
may take him a few days to comment on this thread.)

[Below, I will take the liberty to add some comments of my own in
square brackets. I try to be objective in the other parts.]

2007
----

In 2007, Stefan reengineered the inductive package, which could only
define inductive sets at the time. For many applications, inductive
predicates were more natural, in particular since one could directly
attach mixfix notation to them, without having to introduce another
abbreviation. This was a big improvement.

Supporting both inductive predicates and sets complicated the
implementation considerably, and Stefan looked for possible ways to
simplify the situation. At the time, there was still the idea that one
might be able to get rid of inductive sets completely, and just use
predicates, like in Coq. But many were skeptical, since one then would
lose set theoretic reasoning for inductively defined things.

One observation was that, to complement the new predicates, a new
version ^** of the transitive closure operation ^* was necessary,
which worked on "'a => 'a => bool" instead of "('a * 'a)
set". Basically, the whole theory of ^* and related operations like ^+
and ^= had to be duplicated. This situation still persists today (with
types "'a => 'a => bool" vs. "('a * 'a) => bool"), except that there
are now tools to automate the transition.

In particular, Stefan discovered that replacing inductive set
definitions by predicates was by no means as easy as everybody had
expected. One good example is the small-step relation from Jinja and
its various cousins. It had type "((expr * state) * (expr * state))
set", and turning it into a 4-ary predicate (expr => state => expr =>
state => bool) would cause problems with either version of the
transitive closure operator. [Btw, the newer HOL/IMP/Small_Step.thy
uses a binary predicate over pairs, which requires massaging the
induction rule using [split_format (complete)]].

After some ups and downs, it was decided that inductive_set would
stay, but as a "thin wrapper" around inductive (which then turned out
to be not quite as thin as expected). This tool could then be used in
situations where sets are preferred for some reasons. I am attaching a
summary I wrote from May 2007.

Part of the conclusion was that one should investigate getting rid of
sets completely as a separate type. [Apparently, there was the
(naive?)  hope that by doing this, the problems mentioned above would
somehow vanish in the air, even though it was already clear that the
distinction between curried and tupled relations would still
persist... maybe the idea was to standardize later and it never
happened? Maybe one just did not think about all consequences???]

[I think, at that time there was also the fear that more more
developments would have to be duplicated just like
Transitive_Closure. This, however, did not happen.]

2008
----

In April 2008, Tobias asked Stefan to work again on the elimination of
the set type, and it turned out that it was possible and that the
problems that arised could be solved or circumvented. I am attaching
(with permission from the authors) an email thread from 2008, where
the technicalities are discussed. [This is interesting to read, but it
mainly discusses the new problems that were introduced by the change,
not so much the problems that were solved. There is almost no
discussion on whether the change would give us what we (implicitly)
expected and what that actually was. Obviously, the whole discussion
came from the discussion around inductive(_set) from the year before,
but I do not recall what exactly one hoped to achieve.]

Also compare the NEWS entry: 
http://isabelle.in.tum.de/repos/isabelle/rev/df1f238a05f7

Only a few weeks after this change, Isabelle2008 was
released. Complaints from users are probably best summarized by this
thread, which Brian already pointed to:
http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/

I am not sure what exactly happened afterwards. I think the
infrastructure for predicates was improved further, but Florian may be
able to give more details if necessary.

Alex
-------------- next part --------------
An embedded message was scrubbed...
From: Alexander Krauss <krauss at in.tum.de>
Subject: predicates and sets
Date: Fri, 11 May 2007 15:19:34 +0200
Size: 6032
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0036.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Stefan Berghofer <berghofe at in.tum.de>
Subject: Replacing sets by predicates
Date: Mon, 21 Apr 2008 18:36:14 +0200
Size: 12128
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0037.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
Subject: Re: Replacing sets by predicates
Date: Tue, 22 Apr 2008 09:15:35 +0200
Size: 6539
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0038.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Lawrence Paulson <lp15 at cam.ac.uk>
Subject: Re: Replacing sets by predicates
Date: Tue, 22 Apr 2008 12:20:23 +0100
Size: 3629
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0039.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Stefan Berghofer <berghofe at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Tue, 22 Apr 2008 14:41:22 +0200
Size: 7804
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0040.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Stefan Berghofer <berghofe at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 16:22:14 +0200
Size: 4070
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0041.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Lawrence Paulson <lp15 at cam.ac.uk>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 15:33:52 +0100
Size: 4420
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0042.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Tobias Nipkow <nipkow at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 16:41:48 +0200
Size: 4306
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0043.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Jeremy Avigad <avigad at cmu.edu>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 10:43:59 -0400
Size: 5184
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0044.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Lawrence Paulson <lp15 at cam.ac.uk>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 16:10:05 +0100
Size: 3965
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0045.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Lawrence Paulson <lp15 at cam.ac.uk>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 16:10:56 +0100
Size: 3977
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0046.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Tobias Nipkow <nipkow at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 17:13:50 +0200
Size: 3421
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0047.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 17:24:29 +0200
Size: 5007
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0048.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Jeremy Avigad <avigad at cmu.edu>
Subject: Re: Replacing sets by predicates
Date: Wed, 23 Apr 2008 12:03:24 -0400
Size: 5208
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0049.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Stefan Berghofer <berghofe at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Fri, 02 May 2008 19:39:30 +0200
Size: 7369
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0050.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Makarius <makarius at sketis.net>
Subject: Re: Replacing sets by predicates
Date: Fri, 2 May 2008 22:58:58 +0200 (CEST)
Size: 4470
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0051.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Tobias Nipkow <nipkow at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Sat, 03 May 2008 07:37:49 +0200
Size: 3451
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0052.mht>
-------------- next part --------------
An embedded message was scrubbed...
From: Stefan Berghofer <berghofe at in.tum.de>
Subject: Re: Replacing sets by predicates
Date: Sat, 03 May 2008 12:01:32 +0200
Size: 37753
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110812/cd6349ed/attachment-0053.mht>