Better error messages for non matching quantifiers.

Statement of term1_hom_rsp

proved that the function is a function

term1_hom as a function

A version of hom with quantifiers.

added permutation functions for the raw calculi

fixed broken (partial) proof

used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on

liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals

added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions

tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely

merged

added free_variable function (do not know about the algorithm yet)

hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.

slight tuning of relation_error

Appropriate respects and a statement of the lifted hom lemma

recursion-hom for lambda

Incorrect version of the homomorphism lemma

trivial

tuned quotient_typ.ML

tuned quotient_def.ML and cleaned somewhat LamEx.thy

a few more lemmas...except supp of lambda-abstractions

removed one sorry

nearly all of the proof

right generalisation

First subgoal.

setup for strong induction

exported absrep_const for nitpick.

minor

Simplified matches_typ.

added bound-variable functions to terms

merged

added 3 calculi with interesting binding structure

produce defs with lthy, like prs and ids

Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.

Finished organising an efficient datastructure for qconst_info.

Undid changes from symtab to termtab, since we need to lookup specialized types.

Moved the matches_typ function outside a?d simplified it.

one more item in the list of Markus

Put relation_error as a separate function.

Better error message for definition failure.

merge

Stored Termtab for constant information.

merged

deleted SOLVED'

Removed the 'oops' in IntEx.

tuned

added SOLVED' which is now part of Isabelle....must be removed eventually

merged

tuned

absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"

More indenting, bracket removing and comment restructuring.

Finished replacing OO by OOO

Change OO to OOO in FSet3.

minor comment editing

modifying comments/indentation in quotient_term.ml

Cleaning comments, indentation etc in quotient_tacs.

No more exception handling in rep_abs_rsp_tac

handle all is no longer necessary in lambda_prs.

removed 3 hacks.

Updated some comments.

merge

Removed exception handling from equals_rsp_tac.

added an abbreviation for OOO

merge

Undid the non-working part.

started to adhere to Wenzel-Standard

Changing exceptions to 'try', part 1.

removed quotdata_lookup_type

Fix for testing matching constants in regularize.

tuned previous commit further

the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"

introduced separate match function

removed obsolete equiv_relation and rnamed new_equiv_relation

New_relations, all works again including concat examples.

map and rel simps for all quotients; needed when changing the relations to aggregate ones.

id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.

Experimients with fconcat_insert

Modifications for new_equiv_rel, part2

Modifictaions for new_relation.

Proved concat_empty.

Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.

some cleaning.

First generalization.

The working proof of the special case.

Reduced the proof to two simple but not obvious to prove facts.

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

moved the QuotMain code into two ML-files

complete fix for IsaMakefile

first fix

merged

added a paper for possible notes

Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.

lambda_prs & solve_quotient_assum cleaned.

some commenting

Fixed previous commit.

merge

Moved DETERM inside Repeat & added SOLVE around quotient_tac.

merge.

FIXME/TODO.

reply to question in code

Reply in code.

Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.

a few code annotations

another pass on apply_rsp

managed to simplify apply_rsp

tried to simplify apply_rsp_tac; failed at the moment; added some questions

some trivial changes

trivial cleaning of make_inst

tried to improve test; but fails

merged

annotated some questions to the code; some simple changes

Answering the question in code.

merged

trivial

tuned code

Minor

Some proofs.

Proof of finite_set_storng_cases_raw.

A bracket was missing; with it proved the 'definitely false' lemma.

renamed quotient.ML to quotient_typ.ML

merged

tuned

started to have a look at it; redefined the relation

More name and indentation cleaning.

Merge + Added LarryInt & Fset3 to tests.

Renaming

merged

deleted struct_match by Pattern.match (fixes a problem in LarryInt)

FSet3 minor fixes + cases

added Int example from Larry

Added FSet3 with a formalisation of finite sets based on Michael's one.

Updated TODO list together.

Merge

More theorem renaming.

Renamed theorems in IntEx2 to conform to names in Int.

Updated comments.

merged

tuned

renamed Larrys example

New syntax for definitions.

changed error message

reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case

slightly tuned

merged

added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages

added maps-printout and tuned some comments

Option and Sum quotients.

Regularized the hard lemma.

Simplification of Babses for regularize; will probably become injection

Found the problem with ttt3.

minor

Moved Unused part of locale to Unused QuotMain.

Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.

Removed 'Presburger' as it introduces int & other minor cleaning in Int2.

more tuning

tuned

simplified the instantiation of QUOT_TRUE in procedure_tac

completed previous commit

deleted DT/NDT diagnostic code

moved the interpretation code into Unused.thy

added an attempt to get a finite set theory

removed memb and used standard mem (member from List.thy)

merged

simplified proofs

removed quot_respect attribute of a non-standard lemma

With int_of_nat as a quotient_def, lemmas about it can be easily lifted.

merged

naming in this file cannot be made to agree to the original (PROBLEM?)

Lifted some kind of induction.

more proofs in IntEx2

Finished one proof in IntEx2.

slightly more on IntEx2

proved (with a lot of pain) that times_raw is respectful

merged

fixed minor stupidity

Exception handling.

Code cleaning.

merge

foldr_rsp.

tuned