[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Thu Aug 18 09:18:03 CEST 2011
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>
More information about the isabelle-dev
mailing list