Highest Priority+ −
================+ −
+ −
- give examples for the new quantifier translations in regularization+ −
(quotient_term.ML)+ −
+ −
+ −
Higher Priority+ −
===============+ −
+ −
+ −
- Also, in the interest of making nicer generated documentation, you+ −
might want to change all your "section" headings in Quotient.thy to+ −
"subsection", and add a "header" statement to the top of the file.+ −
Otherwise, each "section" gets its own chapter in the generated pdf,+ −
when the rest of HOL has one chapter per theory file (the chapter+ −
title comes from the "header" statement).+ −
+ −
- If the constant definition gives the wrong definition+ −
term, one gets a cryptic message about absrep_fun+ −
+ −
- 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+ −
==============+ −
+ −
- the quot_lifted attribute should rename variables so they do not+ −
suggest that they talk about raw terms.+ −
+ −
- 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.+ −
+ −
- 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.+ −