Moved exception handling to QuotMain and cleaned FSet.

Merge

Finished manual lifting of list_induct_part :)

comments tuning and slight reordering

Merge

More moving from QuotMain to UnusedQuotMain

deleted some obsolete diagnostic code

Removed unused things from QuotMain.

All examples work again.

cleaning in MyInt

lambda_prs and cleaning the existing examples.

merged

fixed the problem with generalising variables; at the moment it is quite a hack

Ho-matching failures...

changed unification to matching

unification

Lambda & SOLVED' for new quotient_tac

merged

Conversion

The non-working procedure_tac.

merged

use error instead of raising our own exception

Fixes to the tactic after quotient_tac changed.

merged

added a prepare_tac

TRY' for clean_tac

Moved cleaning to QuotMain

New cleaning tactic

explicit phases for the cleaning

Separate regularize_tac

Another theorem for which the new regularize differs from old one, so the goal is not proved. But it seems, that the new one is better.

More fixes for inj_REPABS

addded a tactic, which sets up the three goals of the `algorithm'

fixed the error by a temporary fix (the data of the eqivalence relation should be only its name)

merged

tuned some comments

Another not-typechecking regularized term.

domain_type in regularizing equality

More theorems lifted in the goal-directed way.

Finished temporary goal-directed lift_theorem wrapper.

merged

a version of inj_REPABS (needs to be looked at again later)

Fixes for atomize

merge

lift_thm with a goal.

slight change in code layout

Fixes for new code

Removing dead code

Move atomize_goal to QuotMain

Removed second implementation of Regularize/Inject from FSet.

Moved new repabs_inj code to QuotMain

New repabs behaves the same way as old one.

code review with Cezary

The other branch does not seem to work...

Fixes for recent changes.

updated to Isabelle 22nd November

a little tuning of comments

slight tuning

some debugging code, but cannot find the place where the cprems_of exception is raised

tried to prove the repabs_inj lemma, but failed for the moment

my first version of repabs injection

tuned

tunded

tuned

flagged qenv-stuff as obsolete

simplified get_fun so that it uses directly rty and qty, instead of qenv

started regularize of rtrm/qtrm version; looks quite promising

updated to new Isabelle

fixed the storage of qconst definitions

Still don't know how to do the proof automatically.

added some tracing information to all phases of lifting to the function lift_thm

merge of the merge?

merged

added a FIXME commment

looking up data in quot_info works now (needs qualified string)

changed the quotdata to be a symtab table (needs fixing)

added a container for quotient constants (does not work yet though)

Lifting towards goal and manually finished the proof.

merge

Modifications while preparing the goal-directed version.

updated to new Theory_Data and to new Isabelle

Removed 'Toplevel.program' for polyml 5.3

Atomizing a "goal" theorems.

More code cleaning and commenting

Minor cleaning and removing of some 'handle _'.

Cleaning and commenting

Fixes for the other get_fun implementation.

permutation lifting works now also

merged

updated to new Isabelle version and added a new example file

Minor changes

merge

fold_rsp

tuned the code in quotient and quotient_def

More functionality for lifting list.cases and list.recs.

merged

removed typing information from get_fun in quotient_def; *potentially* dangerous

Remaining fixes for polymorphic types. map_append now lifts properly with 'a list and 'b list.

removed Simplifier.context

replaced check_term o parse_term by read_term

merged

Infrastructure for polymorphic types

Two new tests for get_fun. Second one fails.

Type instantiation in regularize

Description of regularize

Experiments with lifting partially applied constants.

more tuning

slightly tuned

merged

separated the quotient_def into a separate file

Experiments in Int

fixed definition of PLUS

simplified the quotient_def code

Lifting 'fold1.simps(2)' and some cleaning.

Playing with alpha_refl.

Alpha.induct now lifts automatically.

merge

applic_prs

simplified the quotient_def code; type of the defined constant must now be given; for-part eliminated

Automatic FORALL_PRS. 'list.induct' lifts automatically. Faster ALLEX_RSP

merge

Preparing infrastructure for general FORALL_PRS

split quotient.ML into two files

slightly saner way of parsing the quotient_def

merged

changed Type.typ_match to Sign.typ_match

Fixes after optimization and preparing for a general FORALL_PRS

Optimization

Map does not fully work yet.

Fixed quotdata_lookup.

fixed problem with maps_update

merged

fixed the problem with types in map

Automatic computation of application preservation and manually finished "alpha.induct". Slow...

Regularize for equalities and a better tactic. "alpha.cases" now lifts.

Regularization

merged

added some facts about fresh and support of lam

Finally merged the code of the versions of regularize and tested examples.

Lemmas about fv.

changed the order of rfv and reformulated a3 with rfv

merged

not sure what changed here

added fv-function

The proper real_alpha

Finding applications and duplicates filtered out in abstractions

Cleaning also in Lam

Cleaning of the interface to lift.

Tried manually lifting real_alpha

More tests in Lam

Cleaning of 'map id' and 'prod_fun id id' in lower_defs.

Using subst for identity definition.

Lifting of the 3 lemmas in LamEx

Fixed wrong CARD definition and removed the "Does not work anymore" comment.

merged

updated some definitions; had to give sometimes different names; somewhere I introduced a bug, since not everything is working anymore (needs fixing!)

ported all constant definitions to new scheme

fixed the definition of alpha; this *breaks* some of the experiments

disambiguate ===> syntax

More cleaning in Lam code

cleaned FSet

Some cleaning

Cleaning the unnecessary theorems in 'IntEx'.

Fix also in the general procedure.

merge

Fixes

updated all definitions

merged

added infrastructure for defining lifted constants

First experiments with Lambda

Fixed mistake in const generation, will postpone this.

More finshed proofs and cleaning

Proof of append_rsp

merged

added a function for matching types

Manual conversion of equality to equivalence allows lifting append_assoc.

Simplfied interface to repabs_injection.

map_append lifted automatically.

Manually lifted Map_Append.

Merged

Fixed APPLY_RSP vs Cong in the InjRepAbs tactic.

tuned

merged

added equiv-thm to the quot_info

Simplifying FSet with new functions.

added an example about lambda-terms

made quotients compatiple with Nominal; updated keyword file

merged

Completely cleaned Int.

Further reordering in Int code.

Simplifying Int.

Merge

Simplifying Int and Working on map

merged

Simplifying code in int

Symmetry of integer addition

Finished the code for adding lower defs, and more things moved to QuotMain

Making all the definitions from the original ones

Finished COND_PRS proof.

Cleaning and fixing.

updated with quotient_def

added code for declaring map-functions

added "print_quotients" command to th ekeyword file

proved the two lemmas in QuotScript (reformulated them without leading forall)

added data-storage about the quotients

added another example file about integers (see HOL/Int.thy)

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