Removed exception handling from equals_rsp_tac.
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.+ −