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

[Florian Haftmann]

Hi all,

again a report about the current affairs:

a) state of discussion
IMHO I view the discussion at the point that we want 'a set back after
the next release.  As a consequence, developers are cordially invited to
figure out remaining problems involving their contributions to the
system, or scream aloud when their resources do not allow so at the moment.

b) state of affairs in the distribution

failing:
    HOL-ex FAILED
      -> figure out problem with »refute« in Refute_Examples.thy with
"distinct [a, b]"
      -> two proofs commented out, would need to enter the game of
proof-text minimazation
    HOL-Nominal-Examples FAILED
      -> still existing user-space problem, I will look after it
    HOL-Metis_Examples FAILED
    HOL-MicroJava FAILED
      -> user-space problem, should be easy to solve
    HOL-Nitpick_Examples FAILED
    HOL-Predicate_Compile_Examples FAILED
    HOL-Word-SMT_Examples FAILED
    HOL-TPTP FAILED
    HOL-IMP FAILED
      -> codegen problem, I will look after it

working, but needs improvement:
    HOL-ex FAILED
      -> two proofs in Set_Theory commented out, would need to enter the
game of proof-text minimazation
    HOLCF
      -> type class instantiation for sets needed, c.f. ->
http://isabelle.in.tum.de/reports/Isabelle/rev/535290c908ae

c) state of affairs in the AFP

currently failing (including transitive failures):
    BDD Cauchy Coinductive Collections Completeness CoreC++
DataRefinementIBP FinFun Free-Groups Functional-Automata GraphMarkingIBP
HRB-Slicing InformationFlowSlicing Jinja LightweightJava
LinearQuantifierElim Ordinals_and_Cardinals POPLmark-deBruijn
Regular-Sets Shivers-CFA Simpl Slicing Tree-Automata

I.e 23 out of 99, which does not look that bad.  I guess most of these
sessions have come into being after Isabelle2008.

It would be a bad idea to go ahead and provide forked versions of these.
 Better:
* Figure out where the problem is, maybe with some experiments.
* Contact the author and ask what (s)he thinks about that.
* Some things have already been reported to be repaired by a change in a
distribution theory rather than the AFP application.

Maybe good starting points are sessions whose contributors are also
developers.

d) enivsaged working plan

  1.
    * go on with activities from above
    * (maybe)
        hide_fact (open) Set.mem_def Set.Collect_def
      to indicate that something is going on with these

  2. RELEASE

  3. introduce set type constructor
    * backport necessary changes (as little invasive as possible) from
isabelle_set
    * add naive code generator setup for sets in Set.thy (using set ::
'a list => 'a set)
    * instantiation set :: ("{random, type}") random
    * drop theory Executable_Set
    * drop optional special type alias treatment in Pure/Isar/code.ML
(Florian)
    * drop theory CSet (naive version, maybe not quotient version)
    * restore previous rule declarations:
      * lemma predicate1I [Pure.intro!, intro!]
      * lemma pred_equals_eq [pred_set_conv]
      * lemma pred_subset_eq [pred_set_conv]
    * mark _apply rules for pointwise operations on functions as [simp]
    * provide theories Dlist_Set, RBT_Set (or maybe Mapping_Set), etc.
    * backport Set_Algebras to type classes

e) References:

  Isabelle patched:
http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/isabelle_set
  AFP patched: http://www4.in.tum.de/~haftmann/cgi-bin/hgweb.cgi/afp_set
    (although its there, we should avoid using it)
  The historical critical changesets:
http://isabelle.in.tum.de/reports/Isabelle/shortlog/d889d57445dc

	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/20110907/46cd737d/attachment.sig>