[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation – feasibility study
Brian Huffman
brianh at cs.pdx.edu
Thu Aug 18 01:26:36 CEST 2011
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
More information about the isabelle-dev
mailing list