[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 18 09:18:03 CEST 2011
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
does not exhibit any clues that something went utterly wrong.
>> Possible showstoppers:
> 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.
> 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:
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev