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