Highest Priority+
−
================+
−
+
−
- better lookup mechanism for quotient definition+
−
  (see fixme in quotient_term.ML)+
−
+
−
- check needs to be fixed in mk_resp_arg (quotient_term.ML),+
−
  see test for (_, Const _)+
−
+
−
- clever code in quotiet_tacs.ML needs to be turned into+
−
  boring code+
−
+
−
- comment about regularize tactic needs to be adapted+
−
+
−
- Check all the places where we do "handle _"+
−
  (They make code changes very difficult: I sat 1/2+
−
  a day over a simplification of calculate_inst before+
−
  I understood things; the reason was that my exceptions+
−
  where caught by the catch all. There is no problem+
−
  with throwing and handling exceptions...it just must+
−
  be clear who throws what and what is thrown.)+
−
+
−
+
−
Higher Priority+
−
===============+
−
+
−
- If the user defines twice the same quotient constant,+
−
  for example funion, then the line +
−
+
−
    val Free (lhs_str, lhs_ty) = lhs+
−
+
−
  in quotient_def raises a bind exception.+
−
+
−
- If the constant definition gives the wrong definition+
−
  term, one gets a cryptic message about absrep_fun+
−
+
−
- have FSet.thy to have a simple infrastructure for +
−
  finite sets (syntax should be \<lbrace> \<rbrace>,+
−
  look at Set.thy how syntax is been introduced)+
−
+
−
- Handle theorems that include Ball/Bex. For this, would +
−
  it help if we introduced separate Bex and Ball constants +
−
  for quotienting?+
−
+
−
- The user should be able to give quotient_respects and +
−
  preserves theorems in a more natural form.+
−
+
−
+
−
Lower Priority+
−
==============+
−
+
−
- Maybe a quotient_definition should already require+
−
  a proof of the respectfulness (in this way one+
−
  already excludes non-sensical definitions)+
−
+
−
- accept partial equivalence relations+
−
+
−
- think about what happens if things go wrong (like+
−
  theorem cannot be lifted) / proper diagnostic +
−
  messages for the user+
−
+
−
- inductions from the datatype package have a strange+
−
  order of quantifiers in assumptions.+
−
+
−
- wrapper for lifting ... to be used as an attribute+
−
+
−
- find clean ways how to write down the "mathematical"+
−
  procedure for a possible submission (Peter submitted +
−
  his work only to TPHOLs 2005...we would have to go+
−
  maybe for the Journal of Formalised Mathematics)+
−
+
−
- add tests for adding theorems to the various thm lists+
−
+
−
- Maybe quotient and equiv theorems like the ones for+
−
  [QuotList, QuotOption, QuotPair...] could be automatically+
−
  proven?+
−
+
−
- Examples: Finite multiset.+
−
+
−
- The current syntax of the quotient_definition is+
−
+
−
      "qconst :: qty"+
−
      as "rconst"+
−
+
−
  Is it possible to have the more Isabelle-like+
−
  syntax+
−
   +
−
      qconst :: "qty"+
−
      as "rconst"+
−
+
−
  That means "qconst :: qty" is not read as a term, but+
−
  as two entities.+
−