get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Higher Priority===============- if the constant definition gives the wrong definition term, one gets a cryptic message about get_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. Would it help if we introduced separate Bex and Ball constants for quotienting?- user should be able to give quotient_respects and preserves theorems in a more natural form.- the test in the (_, Const _) needs to be fixedLower Priority==============- Maybe a quotient_definition should already require a proof of the respectfulness (in this way one already excludes non-sensical definitions)- accept partial equvalence 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 that translates an an original theorem given a list of quotient_types 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)- use lower-case letters where appropriate in order to make Markus happy- add tests for adding theorems to the various thm lists- Check all the places where we do "handle _"- We shouldn't use the command 'quotient' as this shadows Larry's quotient. Call it 'quotient_type'- 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.