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

[Florian Haftmann]

Hi Brian,

thanks for the excellent work you are doing.

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

Strange.  I guess refute was not modified in 2008 (at least according to
hg diff -r e8cc166ba123 -r ec46381f149d | grep -i refute).  Maybe this
crept in silently over the last years?

@list: btw. what is the status of »refute« in general?  Is it supposed
to be superseded by nitpick entirely?

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

Similar strange.  The history
http://isabelle.in.tum.de/repos/isabelle/log/355d5438f5fb/src/HOL/ex/set.thy
does not exhibit any clues that something went utterly wrong.

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

member :: 'a Cset.set => 'a => bool
Set :: ('a => bool) => 'a Cset.set

Eventually Cset.thy should disappear of course.

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

Maybe, as intermediate solution, these instances can be provided in a
separate theory in the isabelle_set repository?  Which one to add should
be obvious from the 2008 changesets, or maybe we can even inspect
instances for _ => _ and bool and derive the possible set instances from
there.

Cheers,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20110818/8b7bdadd/attachment.sig>