2010-02-01 Christian Urban updated from nominal-huffman
2010-02-01 Cezary Kaliszyk Fixed wrong rename.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk Lambda based on alpha_gen, under construction.
2010-02-01 Christian Urban updated from huffman - repo
2010-02-01 Christian Urban renamed Abst/abst to Abs/abs
2010-02-01 Christian Urban got rid of RAbst type - is now just pairs
2010-02-01 Cezary Kaliszyk Monotonicity of ~~gen, needed for using it in inductive definitions.
2010-02-01 Cezary Kaliszyk The current state of fv vs supp proofs in LF.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk More proofs in the LF example.
2010-02-01 Christian Urban merged
2010-02-01 Christian Urban slight tuning
2010-02-01 Christian Urban renamed function according to the name of the constant
2010-02-01 Christian Urban fixed problem with Bex1_rel renaming
2010-02-01 Cezary Kaliszyk Ported LF to the generic lambda and solved the simpler _supp cases.
2010-01-30 Christian Urban merged
2010-01-30 Christian Urban introduced a generic alpha (but not sure whether it is helpful)
2010-01-29 Cezary Kaliszyk More in the LF example in the new nominal way, all is clear until support.
2010-01-29 Cezary Kaliszyk Fixed the induction problem + some more proofs.
2010-01-29 Cezary Kaliszyk equivariance of rfv and alpha.
2010-01-29 Cezary Kaliszyk Added the experiments with fun and function.
2010-01-29 Christian Urban now also final step is proved - the supp of lambdas is now completely characterised
2010-01-28 Christian Urban the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms
2010-01-28 Christian Urban improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban general abstraction operator and complete characterisation of its support and freshness
2010-01-28 Cezary Kaliszyk Ported existing part of LF to new permutations and alphas.
2010-01-28 Christian Urban attempt of a general abstraction operator
2010-01-28 Christian Urban attempt to prove equivalence between alpha definitions
2010-01-28 Cezary Kaliszyk End of renaming.
2010-01-28 Cezary Kaliszyk Minor when looking at lam.distinct and lam.inject
2010-01-28 Cezary Kaliszyk Renamed Bexeq to Bex1_rel
2010-01-28 Cezary Kaliszyk Substracting bounds from free variables.
2010-01-28 Cezary Kaliszyk Improper interface for datatype and function packages and proper interface lateron.
2010-01-28 Christian Urban merged
2010-01-28 Christian Urban minor
2010-01-28 Christian Urban test about supp/freshness for lam (old proofs work in principle - for single binders)
2010-01-28 Cezary Kaliszyk Recommited the changes for nitpick
2010-01-27 Cezary Kaliszyk Correct types which fixes the printing.
2010-01-27 Cezary Kaliszyk fv for subterms
2010-01-27 Cezary Kaliszyk Fix the problem with later examples. Maybe need to go back to textual specifications.
2010-01-27 Cezary Kaliszyk Some processing of variables in constructors to get free variables.
2010-01-27 Cezary Kaliszyk Parsing of the input as terms and types, and passing them as such to the function package.
2010-01-27 Cezary Kaliszyk Undid the parsing, as it is not possible with thy->lthy interaction.
2010-01-27 Cezary Kaliszyk merge
2010-01-27 Cezary Kaliszyk Some cleaning of thy vs lthy vs context.
2010-01-27 Christian Urban merged
2010-01-27 Christian Urban tuned comment
2010-01-27 Christian Urban completely ported
2010-01-27 Cezary Kaliszyk Another string in the specification.
2010-01-27 Cezary Kaliszyk Variable takes a 'name'.
2010-01-27 Cezary Kaliszyk merge
2010-01-27 Cezary Kaliszyk When commenting discovered a missing case of Babs->Abs regularization.
2010-01-27 Christian Urban merged
2010-01-27 Christian Urban mostly ported Terms.thy to new Nominal
2010-01-27 Cezary Kaliszyk merge
2010-01-27 Cezary Kaliszyk Commenting regularize
2010-01-27 Christian Urban very rough example file for how nominal2 specification can be parsed
2010-01-27 Christian Urban reordered cases in regularize (will be merged into two cases)
2010-01-27 Christian Urban use of equiv_relation_chk in quotient_term
2010-01-27 Christian Urban some slight tuning
2010-01-27 Christian Urban added Terms to Nominal - Instantiation of two types does not work (ask Florian)
2010-01-27 Christian Urban added another example with indirect recursion over lists
2010-01-26 Christian Urban just moved obsolete material into Attic
2010-01-26 Christian Urban added an LamEx example together with the new nominal infrastructure
2010-01-26 Cezary Kaliszyk Bex1_Bexeq_regular.
2010-01-26 Cezary Kaliszyk Hom Theorem with exists unique
2010-01-26 Cezary Kaliszyk 2 cases for regularize with split, lemmas with split now lift.
2010-01-26 Cezary Kaliszyk Simpler statement that has the problem.
2010-01-26 Cezary Kaliszyk Found a term that does not regularize.
2010-01-26 Cezary Kaliszyk A triple is still ok.
2010-01-26 Cezary Kaliszyk Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.
2010-01-26 Cezary Kaliszyk Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
2010-01-26 Cezary Kaliszyk Sigma cleaning works with split_prs (still manual proof).
2010-01-26 Christian Urban tuned
2010-01-26 Christian Urban merged
2010-01-26 Christian Urban cleaning of QuotProd; a little cleaning of QuotList
2010-01-26 Christian Urban added prs and rsp lemmas for Inl and Inr
2010-01-25 Christian Urban used split_option_all lemma
2010-01-25 Christian Urban used the internal Option.map instead of custom option_map
2010-01-26 Cezary Kaliszyk Generalized split_prs and split_rsp
2010-01-26 Cezary Kaliszyk All eq_reflections apart from the one of 'id_apply' can be removed.
2010-01-26 Cezary Kaliszyk continued
2010-01-26 Cezary Kaliszyk More eqreflection/equiv cleaning.
2010-01-26 Cezary Kaliszyk more eq_reflection & other cleaning.
2010-01-26 Cezary Kaliszyk Removing more eq_reflections.
2010-01-25 Christian Urban ids *cannot* be object equalities
2010-01-25 Christian Urban re-inserted lemma in QuotList
2010-01-25 Christian Urban added prs and rsp lemmas for Some and None
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
(0) -1000 -120 +120 +1000 tip