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

[Brian Huffman]

On Wed, Aug 17, 2011 at 11:51 AM, Florian Haftmann
<florian.haftmann at informatik.tu-muenchen.de> wrote:
> HOLCF-Library FAILED
Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/c478cd500dc4

> HOL-Bali FAILED
> HOL-Decision_Procs FAILED
> HOL-Induct FAILED
> HOL-Subst FAILED
> HOL-NanoJava FAILED
Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/b922e91dd1d9

> HOL-Multivariate_Analysis FAILED
Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/7784fa3232ce

> HOL-IMP FAILED
Fixed: http://isabelle.in.tum.de/repos/isabelle/rev/e44f465c00a1

> HOL-ex FAILED
I looked into this, and as far as I can tell, there are two theories
left that have problems.

First, ex/Refute_Examples.thy raises exception REFUTE on line 113:
lemma "distinct [a,b]" refute

Second, ex/set.thy freezes on the "force" methods from lines 180 and 197:
lemma "a < b & b < (c::int) ==> EX A. a ~: A & b : A & c ~: A" by force
lemma "(ALL u v. u < (0::int) --> u ~= abs v)
    --> (EX A::int set. (ALL y. abs y ~: A) & -2 : A)" by (simp add:
abs_if, force)

> Possible showstoppers:
> src/HOL/Library/Cset.thy
This one requires a design decision: What should the type of the
"member" function be? It could be either "'a Cset.set => 'a set" or
"'a Cset.set => 'a => bool". Similarly, "Set" could be either "'a set
=> 'a Cset.set" or "('a => bool) => 'a Cset.set".

> src/HOL/Nominal/Nominal.thy
I have done some playing around with this, but the required changes
include class instances for the "set" type, and so they cannot be
merged back into the main distribution.

> A glimpse at the AFP:

> thys/Shivers-CFA/ExCFSV.thy
> thys/Shivers-CFA/HOLCFUtils.thy
Updating this one will require class instances for the "set" type; the
changes are not backward compatible.

> thys/Presburger-Automata/Presburger_Automata.thy
> thys/Presburger-Automata/DFS.thy
Fixed: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/b8be79162da4

> thys/SIFPL/VS.thy
> thys/SIFPL/VS_OBJ.thy
> thys/SIFPL/HuntSands.thy
Fixed: http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/8d44eafb4517

- Brian