2010-01-25 Christian Urban tuned proofs (mainly in QuotProd)
2010-01-25 Christian Urban properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list
2010-01-25 Christian Urban renamed QuotScript to QuotBase
2010-01-25 Christian Urban cleaned some theorems
2010-01-24 Christian Urban test with splits
2010-01-23 Cezary Kaliszyk The alpha equivalence relations for structures in 'Terms'
2010-01-23 Cezary Kaliszyk More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.
2010-01-23 Cezary Kaliszyk Trying to define hom for the lifted type directly.
2010-01-22 Cezary Kaliszyk Proper alpha equivalence for Sigma calculus.
2010-01-21 Cezary Kaliszyk Changed fun_map and rel_map to definitions.
2010-01-21 Cezary Kaliszyk Lifted Peter's Sigma lemma with Ex1.
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
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
2009-12-06 Christian Urban merged
2009-12-06 Christian Urban working state again
2009-12-06 Christian Urban added a theorem list for equivalence theorems
2009-12-06 Cezary Kaliszyk Merge
2009-12-06 Cezary Kaliszyk Name changes.
2009-12-06 Cezary Kaliszyk Solved all quotient goals.
2009-12-06 Christian Urban updated Isabelle and deleted mono rules
2009-12-06 Christian Urban more tuning of the code
2009-12-06 Christian Urban puting code in separate sections
2009-12-06 Cezary Kaliszyk Handle 'find_qt_asm' exception. Now all inj_repabs_goals should be solved automatically.
2009-12-06 Cezary Kaliszyk merge
2009-12-06 Cezary Kaliszyk Simpler definition code that works with any type maps.
2009-12-06 Christian Urban working on lambda_prs with examples; polished code of clean_tac
2009-12-06 Christian Urban renamed lambda_allex_prs
2009-12-06 Christian Urban added more to IntEx2
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban added new example for Ints; regularise does not work in all instances
2009-12-05 Cezary Kaliszyk Definitions folded first.
2009-12-05 Cezary Kaliszyk Used symmetric definitions. Moved quotient_rsp to QuotMain.
2009-12-05 Cezary Kaliszyk Proved foldl_rsp and ho_map_rsp
2009-12-05 Christian Urban moved all_prs and ex_prs out from the conversion into the simplifier
2009-12-05 Christian Urban further cleaning
2009-12-05 Cezary Kaliszyk Merge
2009-12-05 Cezary Kaliszyk Added nil_rsp and cons_rsp to quotient_rsp; simplified IntEx.
2009-12-05 Christian Urban simplified inj_repabs_trm
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban merged
2009-12-05 Christian Urban simpler version of clean_tac
2009-12-05 Cezary Kaliszyk Handling of respects in the fast inj_repabs_tac; includes respects with quotient assumptions.
2009-12-05 Cezary Kaliszyk Solutions to IntEx tests.
2009-12-05 Christian Urban made some slight simplifications to the examples
2009-12-05 Christian Urban added three examples to IntEx for testing ideas - regularisation and injection seem to be not quite right yet
2009-12-04 Christian Urban tuned code
2009-12-04 Christian Urban merged
2009-12-04 Christian Urban not yet quite functional treatment of constants
2009-12-04 Cezary Kaliszyk Changed FOCUS to SUBGOAL in rep_abs_rsp_tac; another 20% speedup :)
2009-12-04 Cezary Kaliszyk Changing FOCUS to CSUBGOAL (part 1)
2009-12-04 Cezary Kaliszyk abs_rep as ==
2009-12-04 Cezary Kaliszyk Cleaning the Quotients file
2009-12-04 Cezary Kaliszyk Minor renames and moving
2009-12-04 Cezary Kaliszyk Cleaning/review of QuotScript.
2009-12-04 Cezary Kaliszyk More cleaning
2009-12-04 Cezary Kaliszyk more name cleaning and removing
2009-12-04 Cezary Kaliszyk More code cleaning and renaming: moved rsp and prs lemmas from Int to QuotList
2009-12-04 Cezary Kaliszyk Cleaning & Renaming coming from QuotList
2009-12-04 Cezary Kaliszyk Cleaning in Quotients
2009-12-04 Cezary Kaliszyk Even more name changes and cleaning
2009-12-04 Cezary Kaliszyk More code cleaning and name changes
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk merged
2009-12-04 Christian Urban smaller theory footprint
2009-12-04 Christian Urban merged
2009-12-04 Christian Urban merge
2009-12-04 Christian Urban smaller theory footprint
2009-12-04 Cezary Kaliszyk More name changes
2009-12-04 Cezary Kaliszyk Naming changes
2009-12-04 Cezary Kaliszyk code cleaning and renaming
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk Removed previous inj_repabs_tac
2009-12-04 Christian Urban some tuning
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk rep_abs_rsp_tac to replace the last use of instantiate_tac with matching and unification.
2009-12-04 Christian Urban merged
2009-12-04 Christian Urban merged
2009-12-04 Cezary Kaliszyk Change equiv_trans2 to EQUALS_RSP, since we can prove it for any quotient type, not only for eqv relations.
2009-12-04 Cezary Kaliszyk compose_tac instead of rtac to avoid unification; some code cleaning.
2009-12-04 Cezary Kaliszyk Got to about 5 seconds for the longest proof. APPLY_RSP_TAC' solves the quotient internally without instantiation resulting in a faster proof.
2009-12-04 Cezary Kaliszyk Using APPLY_RSP1; again a little bit faster.
2009-12-04 Cezary Kaliszyk Fixes after big merge.
2009-12-04 Cezary Kaliszyk The big merge; probably non-functional.
2009-12-04 Cezary Kaliszyk Testing the new tactic everywhere
2009-12-04 Cezary Kaliszyk First version of the deterministic rep-abs-inj-tac.
2009-12-04 Cezary Kaliszyk Changing = to \<equiv> in case if we want to use simp.
2009-12-04 Cezary Kaliszyk Even better: Completely got rid of the simps in both quotient_tac and inj_repabs_tac
2009-12-04 Cezary Kaliszyk merge
2009-12-04 Cezary Kaliszyk Made your version work again with LIST_REL_EQ.
2009-12-03 Christian Urban the error occurs in APPLY_RSP_TAC where the wrong quotient (for LIST_REL) is applied
2009-12-03 Christian Urban removed quot argument...not all examples work anymore
2009-12-03 Christian Urban merged
2009-12-03 Christian Urban merged
2009-12-03 Christian Urban first version of internalised quotient theorems; added FIXME-TODO
2009-12-03 Christian Urban further dead code
2009-12-03 Cezary Kaliszyk Reintroduced varifyT; we still need it for permutation definition.
2009-12-03 Cezary Kaliszyk Updated the examples
2009-12-03 Cezary Kaliszyk Fixed previous mistake
2009-12-03 Cezary Kaliszyk defs used automatically by clean_tac
2009-12-03 Cezary Kaliszyk Added qoutient_consts dest for getting all the constant definitions in the cleaning step.
2009-12-03 Cezary Kaliszyk Added the definition to quotient constant data.
2009-12-03 Cezary Kaliszyk removing unused code
2009-12-03 Christian Urban merged
2009-12-03 Christian Urban deleted some dead code
2009-12-03 Cezary Kaliszyk Included all_prs and ex_prs in the lambda_prs conversion.
2009-12-03 Christian Urban further simplification
2009-12-03 Christian Urban simplified lambda_prs_conv
2009-12-02 Christian Urban deleted now obsolete argument rty everywhere
2009-12-02 Christian Urban deleted tests at the beginning of QuotMain
2009-12-02 Cezary Kaliszyk Experiments with OPTION_map
2009-12-02 Cezary Kaliszyk merge
2009-12-02 Cezary Kaliszyk More experiments with higher order quotients and theorems with non-lifted constants.
2009-12-02 Christian Urban merged
2009-12-02 Cezary Kaliszyk Lifting to 2 different types :)
2009-12-02 Cezary Kaliszyk New APPLY_RSP which finally does automatic partial lifting :). Doesn't support same relation yet.
2009-12-02 Cezary Kaliszyk Fixed unlam for non-abstractions and updated list_induct_part proof.
2009-12-02 Cezary Kaliszyk Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
2009-12-02 Cezary Kaliszyk The conversion approach works.
2009-12-02 Cezary Kaliszyk Trying a conversion based approach.
2009-12-02 Cezary Kaliszyk A bit of progress; but the object-logic vs meta-logic distinction is troublesome.
2009-12-02 Cezary Kaliszyk Added tactic for dealing with QUOT_TRUE and introducing QUOT_TRUE.
2009-12-01 Cezary Kaliszyk back in working state
2009-12-01 Cezary Kaliszyk clean
2009-12-01 Christian Urban fixed previous commit
2009-12-01 Christian Urban fixed problems with FOCUS
2009-12-01 Christian Urban added a make_inst test
2009-12-01 Cezary Kaliszyk Transformation of QUOT_TRUE assumption by any given function
2009-12-01 Christian Urban QUOT_TRUE joke
2009-12-01 Cezary Kaliszyk Removed last HOL_ss
2009-12-01 Cezary Kaliszyk more cleaning
2009-12-01 Cezary Kaliszyk Cleaning 'aps'.
2009-11-30 Cezary Kaliszyk merge
2009-11-30 Christian Urban cleaned inj_regabs_trm
2009-11-30 Cezary Kaliszyk merge
2009-11-30 Cezary Kaliszyk clean_tac rewrites the definitions the other way
2009-11-30 Christian Urban merged
2009-11-30 Christian Urban added facilities to get all stored quotient data (equiv thms etc)
2009-11-30 Cezary Kaliszyk More code cleaning
2009-11-30 Cezary Kaliszyk Code cleaning.
2009-11-30 Cezary Kaliszyk Commented clean-tac
2009-11-30 Cezary Kaliszyk Added another induction to LFex
2009-11-29 Christian Urban tried to improve the inj_repabs_trm function but left the new part commented out
2009-11-29 Christian Urban added a new version of QuotMain to experiment with qids
2009-11-29 Christian Urban started functions for qid-insertion and fixed a bug in regularise
2009-11-29 Cezary Kaliszyk Removed unnecessary HOL_ss which proved one of the subgoals.
2009-11-29 Cezary Kaliszyk 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.
2009-11-29 Christian Urban introduced a global list of respectfulness lemmas; the attribute is [quot_rsp]
2009-11-29 Christian Urban tuned
2009-11-28 Christian Urban improved pattern matching inside the inj_repabs_tacs
2009-11-28 Christian Urban selective debugging of the inj_repabs_tac (at the moment for step 3 and 4 debugging information is printed)
2009-11-28 Christian Urban removed old inj_repabs_tac; kept only the one with (selective) debugging information
2009-11-28 Christian Urban renamed r_mk_comb_tac to inj_repabs_tac
2009-11-28 Christian Urban tuning
2009-11-28 Christian Urban tuned comments
(0) -480 +480 +1000 tip