made the quotient_type definition more like typedef; now type variables need to be explicitly given

used Local_Theory.declaration for storing quotdata

tuning

renamed some fields in the info records

modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants

cleaed a bit function mk_typedef_main

renamed QUOT_TYPE to Quot_Type

explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions

corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file

added "Highest Priority" category; and tuned slightly code

added a print_maps command; updated the keyword file accordingly

renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions

tuned

moved get_fun into quotient_term; this simplifies the overall including structure of the package

tuned comments; renamed QUOT_TRUE to Quot_True; atomize_eqv seems to not be neccessary (has it been added to Isabelle)...it is now comented out and everything still works

on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst

simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed

used eq_reflection not with OF, but directly in @{thm ...}

cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)

get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO

on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file

renamed "quotient" command to "quotient_type"; needs new keyword file to be installed

this file is now obsolete; replaced by isar-keywords-quot.el

with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place

added a very old paper about Quotients in Isabelle (related work)

avoided global "open"s - replaced by local "open"s

small tuning

various tunings; map_lookup now raises an exception; addition to FIXME-TODO

minor cleaning

moved the QuotMain code into two ML-files

complete fix for IsaMakefile

first fix

merged

added a paper for possible notes

Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.

lambda_prs & solve_quotient_assum cleaned.

some commenting

Fixed previous commit.

merge

Moved DETERM inside Repeat & added SOLVE around quotient_tac.

merge.

FIXME/TODO.

reply to question in code

Reply in code.

Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.

a few code annotations

another pass on apply_rsp

managed to simplify apply_rsp

tried to simplify apply_rsp_tac; failed at the moment; added some questions

some trivial changes

trivial cleaning of make_inst

tried to improve test; but fails

merged

annotated some questions to the code; some simple changes

Answering the question in code.

merged

trivial

tuned code

Minor

Some proofs.

Proof of finite_set_storng_cases_raw.

A bracket was missing; with it proved the 'definitely false' lemma.

renamed quotient.ML to quotient_typ.ML

merged

tuned

started to have a look at it; redefined the relation

More name and indentation cleaning.

Merge + Added LarryInt & Fset3 to tests.

Renaming

merged

deleted struct_match by Pattern.match (fixes a problem in LarryInt)

FSet3 minor fixes + cases

added Int example from Larry

Added FSet3 with a formalisation of finite sets based on Michael's one.

Updated TODO list together.

Merge

More theorem renaming.

Renamed theorems in IntEx2 to conform to names in Int.

Updated comments.

merged

tuned

renamed Larrys example

New syntax for definitions.

changed error message

reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case

slightly tuned

merged

added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages

added maps-printout and tuned some comments

Option and Sum quotients.

Regularized the hard lemma.

Simplification of Babses for regularize; will probably become injection

Found the problem with ttt3.

minor

Moved Unused part of locale to Unused QuotMain.

Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.

Removed 'Presburger' as it introduces int & other minor cleaning in Int2.

more tuning

tuned

simplified the instantiation of QUOT_TRUE in procedure_tac

completed previous commit

deleted DT/NDT diagnostic code

moved the interpretation code into Unused.thy

added an attempt to get a finite set theory

removed memb and used standard mem (member from List.thy)

merged

simplified proofs

removed quot_respect attribute of a non-standard lemma

With int_of_nat as a quotient_def, lemmas about it can be easily lifted.

merged

naming in this file cannot be made to agree to the original (PROBLEM?)

Lifted some kind of induction.

more proofs in IntEx2

Finished one proof in IntEx2.

slightly more on IntEx2

proved (with a lot of pain) that times_raw is respectful

merged

fixed minor stupidity

Exception handling.

Code cleaning.

merge

foldr_rsp.

tuned

merge

Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.

deleted make_inst3

tuned

tuned

moved function and tuned comment

improved fun_map_conv

Arbitrary number of fun_map_tacs.

Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.

tuned code

tuned the examples and flagged the problematic cleaning lemmas in FSet

merged

implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges

merge

manually cleaned the hard lemma.

merged

decoupled QuotProd from QuotMain and also started new cleaning strategy

merge

An example which is hard to lift because of the interplay between lambda_prs and unfolding.

proper formulation of all preservation theorems

started to reformulate preserve lemmas

properly set up the prs_rules

merged

added preserve rules to the cleaning_tac

merge

cleaning.

merged

chnaged syntax to "lifting theorem"

changed names of attributes

merge

Manual regularization of a goal in FSet.

merged

added methods for the lifting_tac and the other tacs

make_inst3

Merge

trans2 replaced with equals_rsp_tac

corrected name of FSet in ROOT.ML

Made fset work again to test all.

Finished the proof of ttt2 and found bug in regularize when trying ttt3.

Another lambda example theorem proved. Seems it starts working properly.

Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned

Proper checked map_rsp.

Nitpick found a counterexample for one lemma.

Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.

It also regularizes.

inj_repabs also works.

merge

An example of working cleaning for lambda lifting. Still not sure why Babs helps.

tuned

the lift_tac produces a warning message if one of the three automatic proofs fails

added a thm list for ids

removed a fixme: map_info is now checked

tuning of the code

merged

removed "global" data and lookup functions; had to move a tactic out from the inj_repabs_match tactic since apply_rsp interferes with a trans2 rule for ===>

3 lambda examples in FSet. In the last one regularize_term fails.

Handling of errors in lambda_prs_conv.

babs_prs

clarified the function examples

first attempt to deal with Babs in regularise and cleaning (not yet working)

isabelle make tests all examples

merge

make_inst for lambda_prs where the second quotient is not identity.

added "end" to each example theory

List moved after QuotMain

cleaning

final move

directory re-arrangement

inj_repabs_tac handles Babs now.

Fix of regularize for babs and proof of babs_rsp.

Using pair_prs; debugging the error in regularize of a lambda.

QuotProd with product_quotient and a 3 respects and preserves lemmas.

merge

3 new example thms in MyInt; reveal problems with handling of lambdas; regularize fails with "Loose Bound".

simplified the regularize simproc

now simpler regularize_tac with added solver works

removed usage of HOL_basic_ss by using a slighly extended version of empty_ss

merged

fixed examples

Fix IntEx2 for equiv_list

merged

working state again

added a theorem list for equivalence theorems

Merge

Name changes.

Solved all quotient goals.

updated Isabelle and deleted mono rules

more tuning of the code

puting code in separate sections

Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.

merge

Simpler definition code that works with any type maps.

working on lambda_prs with examples; polished code of clean_tac

renamed lambda_allex_prs

added more to IntEx2

merged

added new example for Ints; regularise does not work in all instances

Definitions folded first.

Used symmetric definitions. Moved quotient_rsp to QuotMain.

Proved foldl_rsp and ho_map_rsp

moved all_prs and ex_prs out from the conversion into the simplifier

further cleaning

Merge

Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.

simplified inj_repabs_trm

merged

merged

merged

simpler version of clean_tac

Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.

Solutions to IntEx tests.

made some slight simplifications to the examples

added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet

tuned code

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