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
2009-12-09 Christian Urban merged
2009-12-09 Christian Urban fixed minor stupidity
2009-12-09 Cezary Kaliszyk Exception handling.
2009-12-09 Cezary Kaliszyk Code cleaning.
2009-12-09 Cezary Kaliszyk merge
2009-12-09 Cezary Kaliszyk foldr_rsp.
2009-12-09 Christian Urban tuned
2009-12-09 Cezary Kaliszyk merge
2009-12-09 Cezary Kaliszyk Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
2009-12-09 Christian Urban deleted make_inst3
2009-12-09 Christian Urban tuned
2009-12-09 Christian Urban tuned
2009-12-09 Christian Urban moved function and tuned comment
2009-12-09 Christian Urban improved fun_map_conv
2009-12-09 Cezary Kaliszyk Arbitrary number of fun_map_tacs.
2009-12-09 Cezary Kaliszyk Temporarily repeated fun_map_tac 4 times. Cleaning for all examples work.
2009-12-08 Christian Urban tuned code
2009-12-08 Christian Urban tuned the examples and flagged the problematic cleaning lemmas in FSet
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban implemented cleaning strategy with fun_map.simps on non-bounded variables; still a few rough edges
2009-12-08 Cezary Kaliszyk merge
2009-12-08 Cezary Kaliszyk manually cleaned the hard lemma.
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban decoupled QuotProd from QuotMain and also started new cleaning strategy
2009-12-08 Cezary Kaliszyk merge
2009-12-08 Cezary Kaliszyk An example which is hard to lift because of the interplay between lambda_prs and unfolding.
2009-12-08 Christian Urban proper formulation of all preservation theorems
2009-12-08 Christian Urban started to reformulate preserve lemmas
2009-12-08 Christian Urban properly set up the prs_rules
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban added preserve rules to the cleaning_tac
2009-12-08 Cezary Kaliszyk merge
2009-12-08 Cezary Kaliszyk cleaning.
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban chnaged syntax to "lifting theorem"
2009-12-08 Christian Urban changed names of attributes
2009-12-08 Cezary Kaliszyk merge
2009-12-08 Cezary Kaliszyk Manual regularization of a goal in FSet.
2009-12-08 Christian Urban merged
2009-12-08 Christian Urban added methods for the lifting_tac and the other tacs
2009-12-08 Cezary Kaliszyk make_inst3
2009-12-08 Cezary Kaliszyk Merge
2009-12-08 Cezary Kaliszyk trans2 replaced with equals_rsp_tac
2009-12-08 Christian Urban corrected name of FSet in ROOT.ML
2009-12-08 Cezary Kaliszyk Made fset work again to test all.
2009-12-08 Cezary Kaliszyk Finished the proof of ttt2 and found bug in regularize when trying ttt3.
2009-12-08 Cezary Kaliszyk Another lambda example theorem proved. Seems it starts working properly.
2009-12-08 Cezary Kaliszyk Removed pattern from quot_rel_rsp, since list_rel and all used introduced ones cannot be patterned
2009-12-08 Cezary Kaliszyk Proper checked map_rsp.
2009-12-08 Cezary Kaliszyk Nitpick found a counterexample for one lemma.
2009-12-08 Cezary Kaliszyk Added a 'rep_abs' in inj_repabs_trm of babs; and proved two lam examples.
2009-12-08 Cezary Kaliszyk It also regularizes.
2009-12-08 Cezary Kaliszyk inj_repabs also works.
2009-12-08 Cezary Kaliszyk merge
2009-12-08 Cezary Kaliszyk An example of working cleaning for lambda lifting. Still not sure why Babs helps.
2009-12-08 Christian Urban tuned
2009-12-08 Christian Urban the lift_tac produces a warning message if one of the three automatic proofs fails
2009-12-08 Christian Urban added a thm list for ids
2009-12-08 Christian Urban removed a fixme: map_info is now checked
2009-12-07 Christian Urban tuning of the code
2009-12-07 Christian Urban merged
2009-12-07 Christian Urban 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 ===>
2009-12-07 Cezary Kaliszyk 3 lambda examples in FSet. In the last one regularize_term fails.
2009-12-07 Cezary Kaliszyk Handling of errors in lambda_prs_conv.
2009-12-07 Cezary Kaliszyk babs_prs
2009-12-07 Christian Urban clarified the function examples
2009-12-07 Christian Urban first attempt to deal with Babs in regularise and cleaning (not yet working)
2009-12-07 Christian Urban isabelle make tests all examples
2009-12-07 Cezary Kaliszyk merge
2009-12-07 Cezary Kaliszyk make_inst for lambda_prs where the second quotient is not identity.
2009-12-07 Christian Urban added "end" to each example theory
2009-12-07 Cezary Kaliszyk List moved after QuotMain
2009-12-07 Christian Urban cleaning
2009-12-07 Christian Urban final move
2009-12-07 Christian Urban directory re-arrangement
2009-12-07 Cezary Kaliszyk inj_repabs_tac handles Babs now.
2009-12-07 Cezary Kaliszyk Fix of regularize for babs and proof of babs_rsp.
2009-12-07 Cezary Kaliszyk Using pair_prs; debugging the error in regularize of a lambda.
2009-12-07 Cezary Kaliszyk QuotProd with product_quotient and a 3 respects and preserves lemmas.
2009-12-07 Cezary Kaliszyk merge
2009-12-07 Cezary Kaliszyk 3 new example thms in MyInt; reveal problems with handling of lambdas; regularize fails with "Loose Bound".
2009-12-07 Christian Urban simplified the regularize simproc
2009-12-07 Christian Urban now simpler regularize_tac with added solver works
2009-12-07 Christian Urban removed usage of HOL_basic_ss by using a slighly extended version of empty_ss
2009-12-06 Christian Urban merged
2009-12-06 Christian Urban fixed examples
2009-12-06 Cezary Kaliszyk Fix IntEx2 for equiv_list
(0) -240 +240 +1000 tip