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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev