merged

not yet quite functional treatment of constants

Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)

Changing FOCUS to CSUBGOAL (part 1)

abs_rep as ==

Cleaning the Quotients file

Minor renames and moving

Cleaning/review of QuotScript.

More cleaning

more name cleaning and removing

More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList

Cleaning & Renaming coming from QuotList

Cleaning in Quotients

Even more name changes and cleaning

More code cleaning and name changes

merge

merged

smaller theory footprint

merged

merge

smaller theory footprint

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'

introduced a separate lemma for id_simps

renamed inj_REPABS to inj_repabs_trm

tuned comments and moved slightly some code

deleted obsolete qenv code

renamed REGULARIZE to be regularize

more tuning

deleted get_fun_old and stuff

recommited changes of comments

Merge Again

Merged

tuned comments

some diagnostic code for r_mk_comb

introduced a new property for Ball and ===> on the left

fixed QuotList

changed left-res

Manually regularized akind_aty_atrm.induct

Playing with Monos in LFex.

Fixed FSet after merge.

merged

test with monos

applic_prs

polishing

reordered the code

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

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

First theorem with quantifiers. Learned how to use sledgehammer.

simplified the storage of the map-functions by using TheoryDataFun

Just one atomize is enough for the currently lifted theorems. Properly lift 'all' and 'Ex'.

used new cong_tac

First version of handling of the universal quantifier

Handling abstraction correctly.

second test

Test line

Partially fix lifting of card_suc. The quantified variable still needs to be changed.

Tested new build_goal and removed old one, eq_reflection is included in atomize, card_suc tests.

Checked again with the version on my hard-drive backedup yesterday and fixed small whitespace issues.

Merged

added name to prove

consistent state

some tuning of my code

Cleanup

Merged

Cleaning the code with Makarius

Instnatiation with a schematic variable

added ctxt as explicit argument to build_goal; tuned

slightly tuned the comment for unlam

fixed a bug in my code: function typedef_term constructs now now the correct term when the relation is called x

tuned slightly one proof

A version of the tactic that exports variables correctly. It still does not know how to instantiate the obtained theorems.

Minor cleaning: whitespace, commas etc.

Correctly handling abstractions while building goals Use DatatypeAux cong_tac instead of own functions since it handles universal quantifiers properly.

Minor cleanup

Found the source for the exception and added a handle for it.

Make the tactic use Trueprop_cong and atomize.

Proper code for getting the prop out of the theorem.

Using "atomize" the versions with arbitrary Trueprops can be proven.

Proper definition of CARD and some properties of it. Translation should now support Pure assumptions and Trueprops anywhere, but a problem needs to be fixed with the tactic.

some comments

merged

slight tuning

The tactic with REPEAT, CHANGED and a proper simpset.

Merged with my changes from the morning: further working on the tactic and produced goals.

some more beautification

beautification of some proofs

Added more useful quotient facts.

Testing the tactic further.

The tactic still only for fset

Infrastructure for the tactic

More naming/binding suggestions from Makarius

Code cleanup

Cleaning the code

Generalized interpretation, works for all examples.

Fixes after suggestions from Makarius: - indentation - lowercase/uppercase - axioms -> axiomatization - proper operator priorities - proper exception handling

More examples.

Use metavariables in the 'non-lambda' definitions

Make both kinds of definitions.

Changed to the use of "modern interface" (removed the _cmd and passing of strings) Fixed Trueprop handling and the first proof starts working properly.

Initial version of the function that builds goals.

- Build an interpretation for fset from ML level and use it - Added CARD

added the prove command

Fixed

tuned

UNION - Append theorem

update

updated slightly

initial commit