More cleaning and commenting AbsRepTest. Now tests work; just slow.

cleaning in AbsRepTest.

Further in the proof

Tried to prove the lemma manually; only left with quotient proofs.

Sledgehammer bug.

merge

Trying the proof

merged

Struggling with composition

Trying to state composition quotient.

proper handling of error messages (code copy - maybe this can be avoided)

added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)

Readded 'regularize_to_injection' which I believe will be needed.

added a warning to the quotient_type definition, if a map function is missing

tuned

a slight change to abs/rep generation

tuned

fixed comment errors

some slight tuning

renamed transfer to transform (Markus)

some small changes

added a functor that allows checking what is added to the theorem lists

corrected wrong [quot_respect] attribute; tuned

renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy

added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)

as expected problems occure when lifting concat lemmas

tuned

commeted the absrep function

generalised absrep function; needs consolidation

tuned

added sanity checks for quotient_type

made the quotient_type definition more like typedef; now type variables need to be explicitly given

used Local_Theory.declaration for storing quotdata

tuning

renamed some fields in the info records

modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants

cleaed a bit function mk_typedef_main

renamed QUOT_TYPE to Quot_Type

explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions

corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file

added "Highest Priority" category; and tuned slightly code

added a print_maps command; updated the keyword file accordingly

renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions

tuned

moved get_fun into quotient_term; this simplifies the overall including structure of the package

tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works

on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst

simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed

used eq_reflection not with OF, but directly in @{thm ...}

cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)

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

on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file

renamed "quotient" command to "quotient_type"; needs new keyword file to be installed

this file is now obsolete; replaced by isar-keywords-quot.el

with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place

added a very old paper about Quotients in Isabelle (related work)

avoided global "open"s - replaced by local "open"s

small tuning

various tunings; map_lookup now raises an exception; addition to FIXME-TODO

minor cleaning