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

[Brian Huffman]

On Thu, Aug 11, 2011 at 5:44 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi again,
>
> as feasibility study I re-introduced the good old set type constructor
> at a recent revision in the history.  The result can be inspected at
>
> http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/rev/d14eb3a07329

> Then the following sessions fail:
>  HOL-Algebra
>  HOL-Auth
>  HOLCF
>  HOL-ex
>  HOL-Hahn_Banach
>  HOL-Hoare_Parallel
>  HOL-IMP
>  HOL-Imperative_HOL
>  HOL-Induct
>  HOL-Library
>  HOL-Matrix
>  HOL-Metis_Examples
>  HOL-MicroJava
>  HOL-Multivariate_Analysis
>  HOL-Nitpick_Examples
>  HOL-Nominal
>  HOL-NSA
>  HOL-Old_Number_Theory
>  HOL-Predicate_Compile_Examples
>  HOL-Quotient_Examples
>  HOL-TPTP
>  HOL-UNITY
>  HOL-Word-SMT_Examples

Working from a copy of Florian's repo, I have got HOLCF and
HOL-Multivariate_Analysis working again. I transferred the changes
back to the main repo as well:

http://isabelle.in.tum.de/repos/isabelle/rev/bdcc11b2fdc8
http://isabelle.in.tum.de/repos/isabelle/rev/510ac30f44c0

> I estimate that half of these failures are marginal and are just due to
> use of mem_def or Collect_def in proofs.

Indeed, many of the changes are simply removing mem_def and
Collect_def (possibly adding mem_Collect_eq) from calls to metis.

HOLCF required one such change in Library/Infinite_Set.thy, removing
Collect_def in a metis call. The other HOLCF changes were in ML code
in packages: Specifically, when building terms, I was sometimes using
"T --> boolT" instead of "mk_setT T". Overall, HOLCF was very good
about respecting the distinction between sets and predicates, probably
because most of it was written before 2008, back when 'a set and 'a =>
bool were actually distinct types.

> Other failures
> are caused by some constructs which somehow exploit the set-predicate
> identification (Library/Cset.thy "set = member",
> HOL-Multivariate_Analysis "mono (S :: 'a set ==> _"), but this can be
> changed with comparably little effort.

There was a lot more of this kind of thing in the
Multivariate_Analysis libraries. This was to be expected, since much
of it was written in 2009 or later, after 'a set became an
abbreviation.

In the case of "mono" used at type "'a set => bool", I ended up
defining a separate constant called "mono_set". This seems to work
just fine, although it is a user-visible change. In other cases, an
single operation was defined in the library, and then used sometimes
as a set, and other times as a predicate. In these situations, I had
to decide on a specific type signature for each constant, and restate
some lemmas accordingly. Making these decisions is not trivial, and
requires a bit of understanding of the library involved, and how the
constants defined in them are usually used.

> What can be drawn for that?  If there is an agreement that
> re-introducing set is a good idea, this requires some effort, but it is
> not unrealistic.  A working plan could look like the following:
>
> Step A
> * eliminate predicate / set »misfits«
> * eliminate proofs with mem_def / Collect_def
> * repair proofs which fail in this ad-hoc adjustment setup
> The advantage is that these quality improvements can be committed to
> Isabelle as it is by now and do not demand a reintroduction of set
> immediately, but eliminate obstacles later on.

I have already started on this, and I will continue to do more.

> Step B
> * solve problems which existing packages (quotient)
> * re-construct from relevant changesets what still has to be done to
> keep the system consistent
> * re-introduce 'a set
>
> Step C
> * cleaning up the situation: type class instantiations for sets,
> appropriate simp rules for predicates, …
> * code generation setup for sets
>
> It should be self-evident that nothing beyond Step A can be undertaken
> before the next release.

As long as we put off reintroducing 'a set as a separate type, we will
continue to accumulate more theories (like Multivariate_Analysis) that
confuse sets and predicates. The job of introducing 'a set will only
get more difficult the longer we wait. I would certainly like to see
the job completed before the next release, although it might require
more time than we have.

- Brian