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

[Florian Haftmann]

Hi again,

thanks to all contributors who already started to sort out some of the
set-pred mixture issues.

I have merged recent changes back into
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set/ -- this
is meant as a mere basis for figuring out problems experimentally, not
as a proper history to be taken over finally!

Currently makeall says:

HOL-ex FAILED
HOL-Decision_Procs FAILED
HOL-Nominal FAILED
HOL-Bali FAILED
HOL-Hoare_Parallel FAILED
HOLCF-Library FAILED
HOL-Induct FAILED
HOL-Library FAILED
HOL-Metis_Examples FAILED
HOL-MicroJava FAILED
HOL-NanoJava FAILED
HOL-Nitpick_Examples FAILED
HOL-Quotient_Examples FAILED
HOL-Predicate_Compile_Examples FAILED
HOL-Word-SMT_Examples FAILED
HOL-Subst FAILED
HOL-TPTP FAILED
HOL-Multivariate_Analysis FAILED
HOL-IMP FAILED

Possible showstoppers:

haftmann at macbroy20:~/data/isabelle/with_set$ grep -rIPl
'Collect_def|mem_def' src/HOL/*/
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Executable_Set.thy
src/HOL/Library/Cset.thy
src/HOL/Library/More_Set.thy
src/HOL/Library/List_Cset.thy
src/HOL/Quotient_Examples/FSet.thy
src/HOL/Quotient_Examples/List_Cset.thy
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Nominal/Examples/Standardization.thy
src/HOL/Nominal/Nominal.thy
src/HOL/TPTP/CASC_Setup.thy
src/HOL/SMT_Examples/SMT_Tests.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/BV/BVExample.thy
src/HOL/Metis_Examples/Message.thy
src/HOL/Metis_Examples/Tarski.thy
src/HOL/Metis_Examples/Trans_Closure.thy
src/HOL/Metis_Examples/Sets.thy
src/HOL/Metis_Examples/Proxies.thy
src/HOL/Metis_Examples/Abstraction.thy

A glimpse at the AFP:

haftmann at macbroy20:~/data/isabelle/afp/blank$ grep -rIPl
'Collect_def|mem_def' thys/
thys/HRB-Slicing/JinjaVM_Inter/JVMInterpretation.thy
thys/Group-Ring-Module/Algebra1.thy
thys/FinFun/FinFunSet.thy
thys/FinFun/FinFun.thy
thys/Slicing/JinjaVM/SemanticsWF.thy.orig
thys/LinearQuantifierElim/Thys/QE.thy
thys/DataRefinementIBP/Diagram.thy
thys/DataRefinementIBP/DataRefinement.thy
thys/DataRefinementIBP/Preliminaries.thy
thys/Tree-Automata/Ta_impl.thy
thys/Lower_Semicontinuous/Lower_Semicontinuous.thy
thys/Flyspeck-Tame/LowerBound.thy
thys/Flyspeck-Tame/ScoreProps.thy
thys/JinjaThreads/BV/BCVExec.thy
thys/JinjaThreads/MM/Orders.thy
thys/JinjaThreads/MM/JMM_Spec.thy
thys/JinjaThreads/Execute/ExternalCall_Execute.thy
thys/JinjaThreads/Execute/JVMExec_Execute.thy
thys/JinjaThreads/Execute/JVM_Execute2.thy
thys/JinjaThreads/Execute/TypeRelRefine.thy
thys/JinjaThreads/Common/SemiType.thy
thys/JinjaThreads/Common/Cset_Monad.thy
thys/JinjaThreads/Common/Aux.thy
thys/JinjaThreads/Compiler/PCompiler.thy
thys/JinjaThreads/Compiler/JVMJ1.thy
thys/JinjaThreads/Compiler/Execs.thy
thys/JinjaThreads/Framework/LTS.thy
thys/JinjaThreads/Framework/FWLTS.thy
thys/JinjaThreads/Framework/FWDeadlock.thy
thys/JinjaThreads/Framework/FWBisimDeadlock.thy
thys/JinjaThreads/Framework/FWBisimulation.thy
thys/JinjaThreads/Framework/Bisimulation.thy
thys/Coinductive/Coinductive_Nat.thy
thys/Coinductive/TLList.thy
thys/Coinductive/Coinductive_List_Lib.thy
thys/Binomial-Heaps/SkewBinomialHeap.thy
thys/Perfect-Number-Thm/Sigma.thy
thys/GraphMarkingIBP/DSWMark.thy
thys/GraphMarkingIBP/Preliminaries.thy
thys/GraphMarkingIBP/LinkMark.thy
thys/GraphMarkingIBP/StackMark.thy
thys/POPLmark-deBruijn/Execute.thy
thys/Shivers-CFA/ExCFSV.thy
thys/Shivers-CFA/HOLCFUtils.thy
thys/Abstract-Rewriting/Abstract_Rewriting.thy
thys/Presburger-Automata/Presburger_Automata.thy
thys/Presburger-Automata/DFS.thy
thys/Collections/ListSetImpl.thy
thys/Collections/common/FTGAAdd.thy
thys/Collections/AnnotatedListGAPrioUniqueImpl.thy
thys/NormByEval/NBE.thy
thys/Free-Groups/Isomorphisms.thy
thys/KBPs/DFS.thy
thys/SIFPL/VS.thy
thys/SIFPL/VS_OBJ.thy
thys/SIFPL/HuntSands.thy
thys/ArrowImpossibilityGS/Thys/Arrow_Order.thy

A vast area for volunteers.

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/20110817/50441112/attachment.sig>