changed the definitions of liftet constants to use fun_maps

Merge

Finally lifted induction, with some manually added simplification lemmas.

changed encoding from utf8 to ISO8 (needed to work with xemacs)

Merge

Preparing infrastructire for LAMBDA_PRS

moved the map_funs setup into QuotMain

Finally completely lift the previously lifted theorems + clean some old stuff

More infrastructure for automatic lifting of theorems lifted before

More infrastructure for automatic lifting of theorems lifted before

Undid wrong merge

Tried rolling back

Cleaning the mess

Merge

Better tactic and simplified the proof further

fixed problem with incorrect ABS/REP name

Stronger tactic, simpler proof.

Split Finite Set example into separate file

eqsubst_tac

Trying to get a simpler lemma with the whole infrastructure

Using RANGE tactical allows getting rid of the quotients immediately.

Further developing the tactic and simplifying the proof

res_forall_rsp_tac further simplifies the proof

Working on the proof and the tactic.

The proof gets simplified

Removed an assumption

The proof now including manually unfolded higher-order RES_FORALL_RSP.

The problems with 'abs' term.

Simplified the proof with some tactic... Still hangs sometimes.

More proof

Got rid of instantiations in the proof

Removed some debugging messages

tuned and attempted to store data about the quotients (does not work yet)

tuned

slight tuning

fixed my_reg

Reorganization of the construction part

Simplified proof more

Cleaning the code

Further reorganization

Further reorganizing the file

Reordering

cterm_instantiate also fails for some strange reason...

preparing arguments for res_inst_tac

Trying res_inst_tac

started to write code for storing data about the quotients

some minor tuning

tuned and fixed the earlier fix

fixed the abs case in my_reg and added an app case

my version of regularise (still needs to be completed)

moved the map-info and fun-info section to quotient.ML

Test if we can already do sth with the transformed theorem.

slight fix and tuning

the command "quotient" can now define more than one quotient at the same time; quotients need to be separated by and

Partial simplification of the proof

Some QUOTIENTS

Only QUOTIENSs are left to fnish proof

More higher order unification problems

Merged

Simplified

Further in the proof

compose_tac works with the full instantiation.

slightly simplified get_fun function

The instantiated version is the same modulo beta

Fully manually instantiated. Still fails...

Little progress with match/instantiate

Fighting with the instantiation

Symmetric version of REP_ABS_RSP

Progressing with the proof

Finally fix get_fun.

A fix for one fun_map; doesn't work for more.

fixed the problem with function types; but only type_of works; cterm_of does not work

Description of the problem with get_fun.

A proper build_goal_term function.

Cleaning the code

Merged

Cleaning the proofs

Cleaning the code, part 4

slightly improved tyRel

Reordering the code, part 3

Reordering the code, part 2.

Reordering the code, part 1.

Minor cleaning.

The definition of Fold1

A number of lemmas for REGULARIZE_TAC and regularizing card1.

Proving the proper RepAbs version

Forgot to save, second part of the commit

Manually regularized list_induct2

Fixed bug in regularise types. Now we can regularise list.induct.

Function for checking recursively if lifting is needed

Merge

Proper handling of non-lifted quantifiers, testing type freezing.

slight simplification of atomize_thm

atomize_thm and meta_quantify.

Regularizing HOL all.

":" is used for being in a set, "IN" means something else...

First (untested) version of regularize for abstractions.

restored old version

tuned

slightly modified the parser

deleted diagnostic code

added quotient command (you need to update isar-keywords-prove.el)

added new keyword

Bounded quantifier

The tyREL function.

started some strange functions

Further with the manual proof

Further experiments with proving induction manually

Testing if I can prove the regularized version of induction manually

exported parts of QuotMain into a separate ML-file

consistent usage of rty (for the raw, unquotient type); tuned a bit the Isar proof of atomize_eqv.

simplified typedef_quot_type_tac (using MetaSimplifier.rewrite_rule instead of the simplifier)

renamed unlam_def to unabs_def (matching the function abs_def in drule.ML)

tuned; nothing serious

another improvement to unlam_def

one further improvement to unlam_def

simplified the unlam_def function

added an explicit syntax-argument to the function make_def (is needed if the user gives an syntax annotation for quotient types)

used prop_of to get the term of a theorem (replaces crep_thm)

Merged