2 cases for regularize with split, lemmas with split now lift.

Simpler statement that has the problem.

Found a term that does not regularize.

A triple is still ok.

Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.

Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.

Sigma cleaning works with split_prs (still manual proof).

tuned

merged

cleaning of QuotProd; a little cleaning of QuotList

added prs and rsp lemmas for Inl and Inr

used split_option_all lemma

used the internal Option.map instead of custom option_map

Generalized split_prs and split_rsp

All eq_reflections apart from the one of 'id_apply' can be removed.

continued

More eqreflection/equiv cleaning.

more eq_reflection & other cleaning.

Removing more eq_reflections.

ids *cannot* be object equalities

re-inserted lemma in QuotList

added prs and rsp lemmas for Some and None

tuned proofs (mainly in QuotProd)

properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list

renamed QuotScript to QuotBase

cleaned some theorems

test with splits

The alpha equivalence relations for structures in 'Terms'

More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.

Trying to define hom for the lifted type directly.

Proper alpha equivalence for Sigma calculus.

Changed fun_map and rel_map to definitions.

Lifted Peter's Sigma lemma with Ex1.

Automatic injection of Bexeq

Automatic cleaning of Bexeq<->Ex1 theorems.

Using Bexeq_rsp, and manually lifted lemma with Ex1.

Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.

The missing rule.

Ex1 -> Bex1 Regularization, Preparing Exeq.

Added the Sigma Calculus example

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.