More name changes

Naming changes

code cleaning and renaming

merge

Removed previous inj_repabs_tac

some tuning

merge

rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.

merged

merged

Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.

compose_tac instead of rtac to avoid unification; some code cleaning.

Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.

Using APPLY_RSP1; again a little bit faster.

Fixes after big merge.

The big merge; probably non-functional.

Testing the new tactic everywhere

First version of the deterministic rep-abs-inj-tac.

Changing = to \<equiv> in case if we want to use simp.

Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac

merge

Made your version work again with LIST_REL_EQ.

the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied

removed quot argument...not all examples work anymore

merged

merged

first version of internalised quotient theorems; added FIXME-TODO

further dead code

Reintroduced varifyT; we still need it for permutation definition.

Updated the examples

Fixed previous mistake

defs used automatically by clean_tac

Added qoutient_consts dest for getting all the constant definitions in the cleaning step.

Added the definition to quotient constant data.

removing unused code

merged

deleted some dead code

Included all_prs and ex_prs in the lambda_prs conversion.

further simplification

simplified lambda_prs_conv

deleted now obsolete argument rty everywhere

deleted tests at the beginning of QuotMain

Experiments with OPTION_map

merge

More experiments with higher order quotients and theorems with non-lifted constants.

merged

Lifting to 2 different types :)

New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.

Fixed unlam for non-abstractions and updated list_induct_part proof.

Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.

The conversion approach works.

Trying a conversion based approach.

A bit of progress; but the object-logic vs meta-logic distinction is troublesome.

Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.

back in working state

clean

fixed previous commit

fixed problems with FOCUS

added a make_inst test

Transformation of QUOT_TRUE assumption by any given function

QUOT_TRUE joke

Removed last HOL_ss

more cleaning

Cleaning 'aps'.

merge

cleaned inj_regabs_trm

merge

clean_tac rewrites the definitions the other way

merged

added facilities to get all stored quotient data (equiv thms etc)

More code cleaning

Code cleaning.

Commented clean-tac

Added another induction to LFex

tried to improve the inj_repabs_trm function but left the new part commented out

added a new version of QuotMain to experiment with qids

started functions for qid-insertion and fixed a bug in regularise

Removed unnecessary HOL_ss which proved one of the subgoals.

Added 'TRY' to refl in clean_tac to get as far as possible. Removed unnecessary [quot_rsp] in FSet. Added necessary [quot_rsp] and one lifted thm in LamEx.

introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]

tuned

improved pattern matching inside the inj_repabs_tacs

selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)

removed old inj_repabs_tac; kept only the one with (selective) debugging information

renamed r_mk_comb_tac to inj_repabs_tac

tuning

tuned comments

renamed LAMBDA_RES_TAC and WEAK_LAMBDA_RES_TAC to lower case names

Manually finished LF induction.

Moved fast instantiation to QuotMain

LFex proof a bit further.

merge

Looking at repabs proof in LF.

further proper merge

merged

more simplification

Merged and tested that all works.

Finished and tested the new regularize

more tuning of the repabs-tactics

fixed examples in IntEx and FSet

merged

fixed previous commit

Cleaned all lemmas about regularisation of Ball and Bex and moved in one place. Second Ball simprox.

Merged comment

Integrated Stefan's tactic and changed substs to simps with empty context.

some slight tuning of the apply-tactic

annotated a proof with all steps and simplified LAMBDA_RES_TAC

Merge

The magical code from Stefan, will need to be integrated in the Simproc.

replaced FIRST' (map rtac list) with resolve_tac list

Simplifying arguments; got rid of trans2_thm.

Cleaning of LFex. Lambda_prs fails to unify in 2 places.

Recommit

Removing arguments of tactics: absrep, rel_refl, reps_same are computed.

More cleaning in QuotMain, identity handling.

Minor cleaning

tuned

some tuning

simplified gen_frees_tac and properly named abstracted variables

removed CHANGED'