tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
Highest Priority================- better lookup mechanism for quotient definition (see fixme in quotient_term.ML)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- 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==============- 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.