2010-01-21 Cezary Kaliszyk Automatic injection of Bexeq
2010-01-21 Cezary Kaliszyk Automatic cleaning of Bexeq<->Ex1 theorems.
2010-01-21 Cezary Kaliszyk Using Bexeq_rsp, and manually lifted lemma with Ex1.
2010-01-21 Cezary Kaliszyk Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.
2010-01-21 Cezary Kaliszyk The missing rule.
2010-01-21 Cezary Kaliszyk Ex1 -> Bex1 Regularization, Preparing Exeq.
2010-01-20 Cezary Kaliszyk Added the Sigma Calculus example
2010-01-20 Cezary Kaliszyk Better error messages for non matching quantifiers.
2010-01-20 Cezary Kaliszyk Statement of term1_hom_rsp
2010-01-20 Christian Urban proved that the function is a function
2010-01-20 Cezary Kaliszyk term1_hom as a function
2010-01-19 Cezary Kaliszyk A version of hom with quantifiers.
2010-01-17 Christian Urban added permutation functions for the raw calculi
2010-01-16 Christian Urban fixed broken (partial) proof
2010-01-16 Christian Urban used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on
2010-01-16 Christian Urban liftin and lifing_tac can now lift several "and"-separated goals at once; the raw-theorems have to be given in the order of goals
2010-01-15 Christian Urban added a partial proof under which conditions rlam_rec Respects alpha...I guess something like this is true; this means the Hom lemmas need to have preconditions
2010-01-15 Christian Urban tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely
2010-01-15 Christian Urban merged
2010-01-15 Christian Urban added free_variable function (do not know about the algorithm yet)
2010-01-15 Cezary Kaliszyk hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.
2010-01-15 Christian Urban slight tuning of relation_error
2010-01-15 Cezary Kaliszyk Appropriate respects and a statement of the lifted hom lemma
2010-01-15 Christian Urban recursion-hom for lambda
2010-01-15 Cezary Kaliszyk Incorrect version of the homomorphism lemma
2010-01-14 Christian Urban trivial
2010-01-14 Christian Urban tuned quotient_typ.ML
2010-01-14 Christian Urban tuned quotient_def.ML and cleaned somewhat LamEx.thy
2010-01-14 Christian Urban a few more lemmas...except supp of lambda-abstractions
2010-01-14 Christian Urban removed one sorry
2010-01-14 Christian Urban nearly all of the proof
2010-01-14 Christian Urban right generalisation
2010-01-14 Cezary Kaliszyk First subgoal.
2010-01-14 Christian Urban setup for strong induction
2010-01-14 Cezary Kaliszyk exported absrep_const for nitpick.
2010-01-14 Cezary Kaliszyk minor
2010-01-14 Cezary Kaliszyk Simplified matches_typ.
2010-01-14 Christian Urban added bound-variable functions to terms
2010-01-14 Christian Urban merged
2010-01-14 Christian Urban added 3 calculi with interesting binding structure
2010-01-14 Cezary Kaliszyk produce defs with lthy, like prs and ids
2010-01-14 Cezary Kaliszyk Remove SOLVED from quotient_tac. Move atomize_eqv to 'Unused'.
2010-01-14 Cezary Kaliszyk Finished organising an efficient datastructure for qconst_info.
2010-01-14 Cezary Kaliszyk Undid changes from symtab to termtab, since we need to lookup specialized types.
2010-01-13 Cezary Kaliszyk Moved the matches_typ function outside a?d simplified it.
2010-01-13 Christian Urban one more item in the list of Markus
2010-01-13 Cezary Kaliszyk Put relation_error as a separate function.
2010-01-13 Cezary Kaliszyk Better error message for definition failure.
2010-01-13 Cezary Kaliszyk merge
2010-01-13 Cezary Kaliszyk Stored Termtab for constant information.
2010-01-13 Christian Urban merged
2010-01-13 Christian Urban deleted SOLVED'
2010-01-13 Cezary Kaliszyk Removed the 'oops' in IntEx.
2010-01-13 Christian Urban tuned
2010-01-13 Christian Urban added SOLVED' which is now part of Isabelle....must be removed eventually
2010-01-13 Christian Urban merged
2010-01-12 Christian Urban tuned
2010-01-12 Christian Urban absrep_fun and equiv_relation do not produce anymore spurious maps; two problems arose in IntEx, which are marked with "INJECTION PROBLEM"
2010-01-12 Cezary Kaliszyk More indenting, bracket removing and comment restructuring.
2010-01-12 Cezary Kaliszyk Finished replacing OO by OOO
2010-01-12 Cezary Kaliszyk Change OO to OOO in FSet3.
2010-01-12 Cezary Kaliszyk minor comment editing
2010-01-12 Cezary Kaliszyk modifying comments/indentation in quotient_term.ml
2010-01-12 Cezary Kaliszyk Cleaning comments, indentation etc in quotient_tacs.
2010-01-12 Cezary Kaliszyk No more exception handling in rep_abs_rsp_tac
2010-01-12 Cezary Kaliszyk handle all is no longer necessary in lambda_prs.
2010-01-12 Cezary Kaliszyk removed 3 hacks.
2010-01-12 Cezary Kaliszyk Updated some comments.
2010-01-12 Cezary Kaliszyk merge
2010-01-12 Cezary Kaliszyk Removed exception handling from equals_rsp_tac.
2010-01-11 Christian Urban added an abbreviation for OOO
2010-01-11 Cezary Kaliszyk merge
2010-01-11 Cezary Kaliszyk Undid the non-working part.
2010-01-11 Christian Urban started to adhere to Wenzel-Standard
2010-01-11 Cezary Kaliszyk Changing exceptions to 'try', part 1.
2010-01-11 Cezary Kaliszyk removed quotdata_lookup_type
2010-01-11 Cezary Kaliszyk Fix for testing matching constants in regularize.
2010-01-11 Christian Urban tuned previous commit further
2010-01-10 Christian Urban the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"
2010-01-09 Christian Urban introduced separate match function
2010-01-09 Christian Urban removed obsolete equiv_relation and rnamed new_equiv_relation
2010-01-08 Cezary Kaliszyk New_relations, all works again including concat examples.
2010-01-08 Cezary Kaliszyk map and rel simps for all quotients; needed when changing the relations to aggregate ones.
2010-01-08 Cezary Kaliszyk id_simps needs to be taken out not used directly, otherwise the new lemmas are not there.
2010-01-08 Cezary Kaliszyk Experimients with fconcat_insert
2010-01-08 Cezary Kaliszyk Modifications for new_equiv_rel, part2
2010-01-08 Cezary Kaliszyk Modifictaions for new_relation.
2010-01-08 Cezary Kaliszyk Proved concat_empty.
2010-01-07 Cezary Kaliszyk Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
2010-01-07 Cezary Kaliszyk some cleaning.
2010-01-07 Cezary Kaliszyk First generalization.
2010-01-07 Cezary Kaliszyk The working proof of the special case.
2010-01-07 Cezary Kaliszyk Reduced the proof to two simple but not obvious to prove facts.
2010-01-07 Cezary Kaliszyk More cleaning and commenting AbsRepTest. Now tests work; just slow.
2010-01-07 Cezary Kaliszyk cleaning in AbsRepTest.
2010-01-06 Cezary Kaliszyk Further in the proof
2010-01-06 Cezary Kaliszyk Tried to prove the lemma manually; only left with quotient proofs.
2010-01-06 Cezary Kaliszyk Sledgehammer bug.
2010-01-05 Cezary Kaliszyk merge
2010-01-05 Cezary Kaliszyk Trying the proof
2010-01-05 Christian Urban merged
2010-01-05 Cezary Kaliszyk Struggling with composition
2010-01-05 Cezary Kaliszyk Trying to state composition quotient.
2010-01-05 Christian Urban proper handling of error messages (code copy - maybe this can be avoided)
2010-01-05 Christian Urban added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
2010-01-05 Cezary Kaliszyk Readded 'regularize_to_injection' which I believe will be needed.
2010-01-02 Christian Urban added a warning to the quotient_type definition, if a map function is missing
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban a slight change to abs/rep generation
2010-01-01 Christian Urban tuned
2010-01-01 Christian Urban fixed comment errors
2010-01-01 Christian Urban some slight tuning
2009-12-31 Christian Urban renamed transfer to transform (Markus)
2009-12-30 cu some small changes
2009-12-27 Christian Urban added a functor that allows checking what is added to the theorem lists
2009-12-26 Christian Urban corrected wrong [quot_respect] attribute; tuned
2009-12-26 Christian Urban renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
2009-12-26 Christian Urban added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
2009-12-26 Christian Urban as expected problems occure when lifting concat lemmas
2009-12-26 Christian Urban tuned
2009-12-26 Christian Urban commeted the absrep function
2009-12-26 Christian Urban generalised absrep function; needs consolidation
2009-12-24 Christian Urban tuned
2009-12-24 Christian Urban added sanity checks for quotient_type
2009-12-24 Christian Urban made the quotient_type definition more like typedef; now type variables need to be explicitly given
2009-12-23 Christian Urban used Local_Theory.declaration for storing quotdata
2009-12-23 Christian Urban tuning
2009-12-23 Christian Urban renamed some fields in the info records
2009-12-23 Christian Urban modified mk_resp_arg so that the user can give terms as equivalence relations, not just constants
2009-12-23 Christian Urban cleaed a bit function mk_typedef_main
2009-12-23 Christian Urban renamed QUOT_TYPE to Quot_Type
2009-12-23 Christian Urban explicit handling of mem_def, avoiding the use of the simplifier; this fixes some quotient_type definitions
2009-12-23 Christian Urban corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
2009-12-22 Christian Urban added "Highest Priority" category; and tuned slightly code
2009-12-22 Christian Urban added a print_maps command; updated the keyword file accordingly
2009-12-22 Christian Urban renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
2009-12-22 Christian Urban tuned
2009-12-22 Christian Urban moved get_fun into quotient_term; this simplifies the overall including structure of the package
2009-12-22 Christian Urban 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
2009-12-22 Christian Urban on the hunt for what condition raises which exception in the CLEVER CODE of calculate_inst
2009-12-22 Christian Urban simplified calculate_instance; worked around some clever code; clever code is unfortunately still there...needs to be removed
2009-12-21 Christian Urban used eq_reflection not with OF, but directly in @{thm ...}
2009-12-21 Christian Urban cleaned a bit calculate_inst a bit; eta-contraction seems to be not necessary? (all examples go through)
2009-12-21 Christian Urban 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
2009-12-19 Christian Urban on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
2009-12-19 Christian Urban renamed "quotient" command to "quotient_type"; needs new keyword file to be installed
2009-12-19 Christian Urban this file is now obsolete; replaced by isar-keywords-quot.el
2009-12-19 Christian Urban with "isabelle make keywords" you can create automatically a "quot" keywordfile, provided all Logics are in place
2009-12-19 Christian Urban added a very old paper about Quotients in Isabelle (related work)
2009-12-19 Christian Urban avoided global "open"s - replaced by local "open"s
2009-12-19 Christian Urban small tuning
2009-12-19 Christian Urban various tunings; map_lookup now raises an exception; addition to FIXME-TODO
2009-12-17 Christian Urban minor cleaning
2009-12-17 Christian Urban moved the QuotMain code into two ML-files
2009-12-16 Christian Urban complete fix for IsaMakefile
2009-12-16 Christian Urban first fix
2009-12-16 Christian Urban merged
2009-12-16 Christian Urban added a paper for possible notes
2009-12-16 Cezary Kaliszyk Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
2009-12-15 Cezary Kaliszyk lambda_prs & solve_quotient_assum cleaned.
2009-12-15 Christian Urban some commenting
2009-12-14 Cezary Kaliszyk Fixed previous commit.
2009-12-14 Cezary Kaliszyk merge
2009-12-14 Cezary Kaliszyk Moved DETERM inside Repeat & added SOLVE around quotient_tac.
2009-12-14 Cezary Kaliszyk merge.
2009-12-14 Cezary Kaliszyk FIXME/TODO.
2009-12-14 Cezary Kaliszyk reply to question in code
2009-12-14 Cezary Kaliszyk Reply in code.
2009-12-14 Cezary Kaliszyk Replies to questions from the weekend: Uncommenting the renamed theorem commented out in 734.
2009-12-13 Christian Urban a few code annotations
2009-12-13 Christian Urban another pass on apply_rsp
2009-12-13 Christian Urban managed to simplify apply_rsp
2009-12-12 Christian Urban tried to simplify apply_rsp_tac; failed at the moment; added some questions
2009-12-12 Christian Urban some trivial changes
2009-12-12 Christian Urban trivial cleaning of make_inst
2009-12-12 Christian Urban tried to improve test; but fails
2009-12-12 Christian Urban merged
2009-12-12 Christian Urban annotated some questions to the code; some simple changes
2009-12-12 Cezary Kaliszyk Answering the question in code.
2009-12-12 Christian Urban merged
2009-12-12 Christian Urban trivial
2009-12-12 Christian Urban tuned code
2009-12-12 Cezary Kaliszyk Minor
2009-12-12 Cezary Kaliszyk Some proofs.
2009-12-12 Cezary Kaliszyk Proof of finite_set_storng_cases_raw.
2009-12-12 Cezary Kaliszyk A bracket was missing; with it proved the 'definitely false' lemma.
2009-12-12 Christian Urban renamed quotient.ML to quotient_typ.ML
2009-12-11 Christian Urban merged
2009-12-11 Christian Urban tuned
2009-12-11 Christian Urban started to have a look at it; redefined the relation
2009-12-11 Cezary Kaliszyk More name and indentation cleaning.
2009-12-11 Cezary Kaliszyk Merge + Added LarryInt & Fset3 to tests.
2009-12-11 Cezary Kaliszyk Renaming
2009-12-11 Christian Urban merged
2009-12-11 Christian Urban deleted struct_match by Pattern.match (fixes a problem in LarryInt)
2009-12-11 Cezary Kaliszyk FSet3 minor fixes + cases
2009-12-11 Christian Urban added Int example from Larry
2009-12-11 Cezary Kaliszyk Added FSet3 with a formalisation of finite sets based on Michael's one.
2009-12-11 Cezary Kaliszyk Updated TODO list together.
2009-12-11 Cezary Kaliszyk Merge
2009-12-11 Cezary Kaliszyk More theorem renaming.
2009-12-11 Cezary Kaliszyk Renamed theorems in IntEx2 to conform to names in Int.
2009-12-11 Cezary Kaliszyk Updated comments.
2009-12-11 Christian Urban merged
2009-12-11 Christian Urban tuned
2009-12-11 Christian Urban renamed Larrys example
2009-12-11 Cezary Kaliszyk New syntax for definitions.
2009-12-11 Christian Urban changed error message
2009-12-11 Christian Urban reformulated the lemma lifting_procedure as ML value; gave better warning message for injection case
2009-12-10 Christian Urban slightly tuned
2009-12-10 Christian Urban merged
2009-12-10 Christian Urban added Larry's theory; introduced lemma equivpI; added something to the TODO about error messages
2009-12-10 Christian Urban added maps-printout and tuned some comments
2009-12-10 Cezary Kaliszyk Option and Sum quotients.
2009-12-10 Cezary Kaliszyk Regularized the hard lemma.
2009-12-10 Cezary Kaliszyk Simplification of Babses for regularize; will probably become injection
2009-12-10 Cezary Kaliszyk Found the problem with ttt3.
2009-12-10 Cezary Kaliszyk minor
2009-12-10 Cezary Kaliszyk Moved Unused part of locale to Unused QuotMain.
2009-12-10 Cezary Kaliszyk Moved 'int_induct' to IntEx to keep IntEx2 being just theory of integers in order.
2009-12-10 Cezary Kaliszyk Removed 'Presburger' as it introduces int & other minor cleaning in Int2.
2009-12-10 Christian Urban more tuning
2009-12-10 Christian Urban tuned
2009-12-10 Christian Urban simplified the instantiation of QUOT_TRUE in procedure_tac
2009-12-10 Christian Urban completed previous commit
2009-12-10 Christian Urban deleted DT/NDT diagnostic code
2009-12-10 Christian Urban moved the interpretation code into Unused.thy
2009-12-10 Christian Urban added an attempt to get a finite set theory
2009-12-10 Christian Urban removed memb and used standard mem (member from List.thy)
2009-12-10 Christian Urban merged
2009-12-10 Christian Urban simplified proofs
2009-12-10 Christian Urban removed quot_respect attribute of a non-standard lemma
2009-12-10 Cezary Kaliszyk With int_of_nat as a quotient_def, lemmas about it can be easily lifted.
2009-12-10 Christian Urban merged
2009-12-10 Christian Urban naming in this file cannot be made to agree to the original (PROBLEM?)
2009-12-10 Cezary Kaliszyk Lifted some kind of induction.
2009-12-09 Christian Urban more proofs in IntEx2
2009-12-09 Cezary Kaliszyk Finished one proof in IntEx2.
2009-12-09 Christian Urban slightly more on IntEx2
2009-12-09 Christian Urban proved (with a lot of pain) that times_raw is respectful
(0) -240 +240 +1000 tip