1 Highest Priority

     2 ================

     3 

     4 - give examples for the new quantifier translations in regularization

     5   (quotient_term.ML)

     6 

     7 

     8 Higher Priority

     9 ===============

    10 

    11 

    12 - Also, in the interest of making nicer generated documentation, you

    13   might want to change all your "section" headings in Quotient.thy to

    14   "subsection", and add a "header" statement to the top of the file.

    15   Otherwise, each "section" gets its own chapter in the generated pdf,

    16   when the rest of HOL has one chapter per theory file (the chapter

    17   title comes from the "header" statement).

    18 

    19 - If the constant definition gives the wrong definition

    20   term, one gets a cryptic message about absrep_fun

    21 

    22 - Handle theorems that include Ball/Bex. For this, would 

    23   it help if we introduced separate Bex and Ball constants 

    24   for quotienting?

    25 

    26 - The user should be able to give quotient_respects and 

    27   preserves theorems in a more natural form.

    28 

    29 Lower Priority

    30 ==============

    31 

    32 - accept partial equivalence relations

    33 

    34 - think about what happens if things go wrong (like

    35   theorem cannot be lifted) / proper diagnostic 

    36   messages for the user

    37 

    38 - inductions from the datatype package have a strange

    39   order of quantifiers in assumptions.

    40 

    41 - find clean ways how to write down the "mathematical"

    42   procedure for a possible submission (Peter submitted 

    43   his work only to TPHOLs 2005...we would have to go

    44   maybe for the Journal of Formalised Mathematics)

    45 

    46 - add tests for adding theorems to the various thm lists

    47 

    48 - Maybe quotient and equiv theorems like the ones for

    49   [QuotList, QuotOption, QuotPair...] could be automatically

    50   proven?

    51 

    52 - Examples: Finite multiset.

    53 

    54 - The current syntax of the quotient_definition is

    55 

    56       "qconst :: qty"

    57       as "rconst"

    58 

    59   Is it possible to have the more Isabelle-like

    60   syntax

    61    

    62       qconst :: "qty"

    63       as "rconst"

    64 

    65   That means "qconst :: qty" is not read as a term, but

    66   as two entities.

    67 

    68 - Restrict automatic translation to particular quotient types

    69