2010-03-04 Cezary Kaliszyk Lift distinct.
2010-03-04 Cezary Kaliszyk Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Cezary Kaliszyk Lift BV,FV,Permutations and injection :).
2010-03-04 Cezary Kaliszyk Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
2010-03-04 Cezary Kaliszyk A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Cezary Kaliszyk Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 Cezary Kaliszyk merge
2010-03-03 Cezary Kaliszyk Experiments with proving weird transp
2010-03-03 Cezary Kaliszyk Code for solving symp goals with multiple existentials.
2010-03-03 Cezary Kaliszyk reflp for multiple quantifiers.
2010-03-03 Christian Urban fixed mess in Test.thy
2010-03-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Christian Urban only tuned
2010-03-03 Christian Urban merged
2010-03-03 Christian Urban start of paper - does not compile yet
2010-03-03 Christian Urban added ACM style file for ICFP
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-03 Cezary Kaliszyk Add the supp intersection conditions.
2010-03-02 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
2010-03-02 Cezary Kaliszyk Fixes for the fv problem and alpha problem.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban preliinary test about alpha-weirdo
2010-03-02 Christian Urban Another problem with permutations in alpha and possibly also in fv
2010-03-02 Christian Urban potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02 Cezary Kaliszyk Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02 Cezary Kaliszyk Include the raw eqvt lemmas.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added some more examples from Peter Sewell's bestiary
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Minor
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk Moving wrappers out of Lift.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added distinctness of perms
2010-03-02 Christian Urban updated (added lemma about commuting permutations)
2010-03-02 Cezary Kaliszyk Change type schemes to name set.
2010-03-02 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
2010-03-02 Cezary Kaliszyk Length fix for nested recursions.
2010-03-02 Cezary Kaliszyk Fix equivp.
2010-03-02 Cezary Kaliszyk Fixed eqvt code.
2010-03-02 Christian Urban most tests work - the ones that do not I commented out
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Add a check of fv_functions.
2010-03-02 Christian Urban some tuning
2010-03-02 Cezary Kaliszyk Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban rawified the bind specs (ready to be used now)
2010-03-01 Cezary Kaliszyk merge
2010-03-01 Cezary Kaliszyk Trying to prove equivariance.
2010-03-01 Christian Urban modified for new binding format - hope it is the intended one
2010-03-01 Christian Urban further code-refactoring in the parser
2010-03-01 Cezary Kaliszyk The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01 Christian Urban slight simplification of the raw-decl generation
2010-03-01 Cezary Kaliszyk Example that shows that current alpha is wrong.
2010-03-01 Christian Urban added example from my phd
2010-02-27 Christian Urban streamlined parser
2010-02-26 Christian Urban generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
2010-02-26 Cezary Kaliszyk More about the general lifting procedure.
2010-02-26 Cezary Kaliszyk Update TODO
2010-02-26 Cezary Kaliszyk Progress with general lifting procedure.
2010-02-26 Cezary Kaliszyk RSP of perms can be shown in one go.
2010-02-26 Cezary Kaliszyk Change in signature of prove_const_rsp for general lifting.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-26 Cezary Kaliszyk To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-25 Cezary Kaliszyk merge
2010-02-25 Cezary Kaliszyk Preparing the generalized lifting procedure
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban added ott-example about Leroy96
2010-02-25 Cezary Kaliszyk Forgot to add one file.
2010-02-25 Cezary Kaliszyk Split Terms into separate files and add them to tests.
2010-02-25 Cezary Kaliszyk merge
2010-02-25 Cezary Kaliszyk Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban a few simplifications
2010-02-25 Christian Urban first attempt to make sense out of the core-haskell definition
2010-02-25 Cezary Kaliszyk Code for proving eqvt, still in Terms.
2010-02-25 Cezary Kaliszyk Use eqvt infrastructure.
2010-02-25 Cezary Kaliszyk Simple function eqvt code.
2010-02-25 Christian Urban added IsaMakefile...but so far included only a test for the parser
2010-02-25 Christian Urban moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban moved Nominal to "toplevel"
2010-02-25 Cezary Kaliszyk Export perm_frees.
2010-02-24 Cezary Kaliszyk Restructuring the code in Perm
2010-02-24 Cezary Kaliszyk Simplified and finised eqvt proofs for t1 and t5
2010-02-24 Cezary Kaliszyk merge
2010-02-24 Cezary Kaliszyk Define lifted perms.
2010-02-24 Christian Urban merged
2010-02-24 Christian Urban parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24 Cezary Kaliszyk With permute_rsp we can lift the instance proofs :).
2010-02-24 Cezary Kaliszyk Note the instance proofs, since they can be easily lifted.
2010-02-24 Cezary Kaliszyk More refactoring and removed references to the global simpset in Perm.
2010-02-24 Cezary Kaliszyk Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24 Cezary Kaliszyk Regularize finite support proof for trm1
2010-02-24 Cezary Kaliszyk Made the fv-supp proof much more straightforward.
2010-02-24 Cezary Kaliszyk Regularize the proofs about finite support.
2010-02-24 Cezary Kaliszyk Respects of permute and constructors.
2010-02-24 Cezary Kaliszyk Generate fv_rsp automatically.
2010-02-24 Cezary Kaliszyk Define the constants automatically.
2010-02-24 Cezary Kaliszyk Rename also the lifted types to non-capital.
2010-02-24 Cezary Kaliszyk Use the infrastructure in LF. Much shorter :).
2010-02-24 Cezary Kaliszyk Final synchronization of names.
2010-02-24 Cezary Kaliszyk LF renaming part 3 (proper names of alpha equvalences)
2010-02-24 Cezary Kaliszyk LF renaming part 2 (proper fv functions)
2010-02-24 Cezary Kaliszyk merge
2010-02-24 Cezary Kaliszyk LF renaming part1.
2010-02-24 Christian Urban merged
2010-02-24 Christian Urban parsing of function definitions almost works now; still an error with undefined constants
2010-02-23 Cezary Kaliszyk merge
2010-02-23 Cezary Kaliszyk rsp for bv; the only issue is that it requires an appropriate induction principle.
2010-02-23 Christian Urban merged
2010-02-23 Christian Urban declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
2010-02-23 Cezary Kaliszyk rsp infrastructure.
2010-02-23 Cezary Kaliszyk merge
2010-02-23 Cezary Kaliszyk Progress towards automatic rsp of constants and fv.
2010-02-23 Christian Urban merged
2010-02-23 Christian Urban "raw"-ified the term-constructors and types given in the specification
2010-02-23 Cezary Kaliszyk Looking at proving the rsp rules automatically.
2010-02-23 Cezary Kaliszyk Minor beutification.
2010-02-23 Cezary Kaliszyk Define the quotient from ML
2010-02-23 Cezary Kaliszyk All works in LF but will require renaming.
2010-02-23 Cezary Kaliszyk Reordering in LF.
2010-02-23 Cezary Kaliszyk Fixes for auxiliary datatypes.
2010-02-22 Cezary Kaliszyk Fixed pseudo_injectivity for trm4
2010-02-22 Cezary Kaliszyk Testing auto equivp code.
2010-02-22 Cezary Kaliszyk A tactic for final equivp
2010-02-22 Cezary Kaliszyk More equivp infrastructure.
2010-02-22 Cezary Kaliszyk tactify transp
2010-02-22 Cezary Kaliszyk export the reflp and symp tacs.
2010-02-22 Cezary Kaliszyk Generalize atom_trans and atom_sym.
2010-02-22 Cezary Kaliszyk Some progress about transp
2010-02-22 Cezary Kaliszyk alpha-symmetric addons.
2010-02-22 Cezary Kaliszyk alpha reflexivity
2010-02-22 Cezary Kaliszyk Renaming.
2010-02-22 Cezary Kaliszyk Added missing description.
2010-02-22 Cezary Kaliszyk Added Brian's suggestion.
2010-02-22 Cezary Kaliszyk Update TODO
2010-02-21 Cezary Kaliszyk Removed bindings 'in itself' where possible.
2010-02-20 Cezary Kaliszyk Some adaptation
2010-02-19 Cezary Kaliszyk proof cleaning and standardizing.
2010-02-19 Cezary Kaliszyk Automatic production and proving of pseudo-injectivity.
2010-02-19 Cezary Kaliszyk Experiments for the pseudo-injectivity tactic.
2010-02-19 Cezary Kaliszyk merge
2010-02-19 Cezary Kaliszyk Constructing alpha_inj goal.
2010-02-18 Christian Urban merged
2010-02-18 Christian Urban start work with the parser
2010-02-18 Cezary Kaliszyk Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
2010-02-18 Cezary Kaliszyk First (non-working) version of alpha-equivalence
2010-02-18 Cezary Kaliszyk Description of the fv procedure.
2010-02-18 Cezary Kaliszyk Testing auto constant lifting.
2010-02-18 Cezary Kaliszyk Fix for new Isabelle (primrec)
2010-02-18 Cezary Kaliszyk Automatic lifting of constants.
2010-02-18 Cezary Kaliszyk Changed back to original version of trm5
2010-02-18 Cezary Kaliszyk The alternate version of trm5 with additional binding. All proofs work the same.
2010-02-18 Cezary Kaliszyk Code for handling atom sets.
2010-02-18 Cezary Kaliszyk Replace Terms by Terms2.
2010-02-18 Cezary Kaliszyk Fixed proofs in Terms2 and found a mistake in Terms.
2010-02-17 Cezary Kaliszyk Terms2 with bindings for binders synchronized with bindings they are used in.
2010-02-17 Cezary Kaliszyk Cleaning of proofs in Terms.
2010-02-17 Cezary Kaliszyk Testing Fv
2010-02-17 Cezary Kaliszyk Fix the strong induction principle.
2010-02-17 Cezary Kaliszyk Reorder
2010-02-17 Cezary Kaliszyk Add bindings of recursive types by free_variables.
2010-02-17 Cezary Kaliszyk Bindings adapted to multiple defined datatypes.
2010-02-17 Cezary Kaliszyk Reorganization
2010-02-17 Cezary Kaliszyk Now should work.
2010-02-17 Cezary Kaliszyk Some optimizations and fixes.
2010-02-17 Cezary Kaliszyk Simplified format of bindings.
2010-02-17 Cezary Kaliszyk Tested the Perm code; works everywhere in Terms.
2010-02-17 Cezary Kaliszyk Wrapped the permutation code.
2010-02-17 Cezary Kaliszyk Description of intended bindings.
2010-02-17 Cezary Kaliszyk Code for generating the fv function, no bindings yet.
2010-02-17 Cezary Kaliszyk merge
2010-02-17 Cezary Kaliszyk indent
2010-02-17 Cezary Kaliszyk merge
2010-02-17 Cezary Kaliszyk Simplifying perm_eq
2010-02-16 Cezary Kaliszyk merge
2010-02-16 Cezary Kaliszyk indenting
2010-02-16 Cezary Kaliszyk Minor
2010-02-16 Cezary Kaliszyk Merge
2010-02-16 Cezary Kaliszyk Ported Stefan's permutation code, still needs some localizing.
2010-02-15 Cezary Kaliszyk merge
2010-02-15 Cezary Kaliszyk Removed varifyT.
2010-02-15 Christian Urban merged
2010-02-15 Christian Urban 2-spaces rule (where it makes sense)
2010-02-15 Cezary Kaliszyk merge
2010-02-15 Cezary Kaliszyk Fixed the definition of less and finished the missing proof.
2010-02-15 Christian Urban further tuning
2010-02-15 Christian Urban small tuning
2010-02-15 Christian Urban tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
2010-02-15 Cezary Kaliszyk der_bname -> derived_bname
2010-02-15 Cezary Kaliszyk Names of files.
2010-02-15 Cezary Kaliszyk Finished introducing the binding.
2010-02-15 Cezary Kaliszyk Synchronize the commands.
2010-02-15 Cezary Kaliszyk Passing the binding to quotient_def
2010-02-15 Cezary Kaliszyk Added a binding to the parser.
2010-02-15 Cezary Kaliszyk Second inline
2010-02-15 Cezary Kaliszyk remove one-line wrapper.
2010-02-12 Cezary Kaliszyk Undid the read_terms change; now compiles.
2010-02-12 Cezary Kaliszyk merge
2010-02-12 Cezary Kaliszyk renamed 'as' to 'is' everywhere.
2010-02-12 Cezary Kaliszyk "is" defined as the keyword
2010-02-12 Christian Urban moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
2010-02-12 Cezary Kaliszyk The lattice instantiations are gone from Isabelle/Main, so
2010-02-11 Cezary Kaliszyk the lam/bla example.
2010-02-11 Cezary Kaliszyk Finished a working foo/bar.
2010-02-11 Cezary Kaliszyk fv_foo is not regular.
2010-02-11 Cezary Kaliszyk Testing foo/bar
2010-02-11 Cezary Kaliszyk Even when bv = fv it still doesn't lift.
2010-02-11 Cezary Kaliszyk Added the missing syntax file
2010-02-11 Cezary Kaliszyk Notation available locally
2010-02-11 Cezary Kaliszyk Main renaming + fixes for new Isabelle in IntEx2.
2010-02-11 Cezary Kaliszyk Merging QuotBase into QuotMain.
2010-02-10 Christian Urban removed dead code
2010-02-10 Christian Urban cleaned a bit
2010-02-10 Cezary Kaliszyk lowercase locale
2010-02-10 Cezary Kaliszyk hg-added the added file.
2010-02-10 Cezary Kaliszyk Changes from Makarius's code review + some noticed fixes.
2010-02-10 Cezary Kaliszyk example with a respectful bn function defined over the type itself
2010-02-10 Cezary Kaliszyk Finishe the renaming.
2010-02-10 Cezary Kaliszyk Another mistake found with OTT.
2010-02-10 Cezary Kaliszyk merge
2010-02-10 Cezary Kaliszyk Fixed rbv6, when translating to OTT.
2010-02-10 Cezary Kaliszyk Some cleaning of proofs.
2010-02-10 Christian Urban merged again
2010-02-10 Christian Urban merged
2010-02-10 Cezary Kaliszyk more minor space and bracket modifications.
2010-02-10 Cezary Kaliszyk More changes according to the standards.
2010-02-10 Cezary Kaliszyk A concrete example, with a proof that rbv is not regular and
2010-02-09 Christian Urban proper declaration of types and terms during parsing (removes the varifyT when storing data)
2010-02-09 Christian Urban merged
2010-02-09 Christian Urban slight correction
2010-02-09 Cezary Kaliszyk merge
2010-02-09 Cezary Kaliszyk More about trm6
2010-02-09 Christian Urban merged
2010-02-09 Cezary Kaliszyk the specifications of the respects.
2010-02-09 Cezary Kaliszyk trm6 with the 'Foo' constructor.
2010-02-09 Cezary Kaliszyk removing unnecessary brackets
2010-02-09 Cezary Kaliszyk More indentation cleaning.
2010-02-09 Cezary Kaliszyk 'exc' -> 'exn' and more name and space cleaning.
2010-02-09 Cezary Kaliszyk Fully qualified exception names.
2010-02-09 Cezary Kaliszyk merge
2010-02-09 Cezary Kaliszyk More indentation, names and todo cleaning in the quotient package
2010-02-09 Christian Urban merged
2010-02-09 Christian Urban a few more attempts to show the equivalence between old and new way of defining alpha-equivalence
2010-02-09 Christian Urban minor tuning
2010-02-09 Cezary Kaliszyk Explicitly marked what is bound.
2010-02-09 Cezary Kaliszyk Cleaning and updating in Terms.
2010-02-09 Cezary Kaliszyk Looking at the trm2 example
2010-02-09 Cezary Kaliszyk Fixed pattern matching, now the test in Abs works correctly.
2010-02-08 Christian Urban added a test case
2010-02-08 Christian Urban merged
2010-02-08 Christian Urban moved some lemmas to Nominal; updated all files
2010-02-08 Cezary Kaliszyk merge
2010-02-08 Cezary Kaliszyk Comments.
2010-02-08 Christian Urban slightly tuned
2010-02-08 Cezary Kaliszyk Proper context fixes lifting inside instantiations.
2010-02-08 Cezary Kaliszyk Fixed the context import/export and simplified LFex.
2010-02-08 Christian Urban added 2 papers about core haskell
2010-02-07 Christian Urban fixed lemma name
2010-02-07 Christian Urban updated to latest Nominal2
2010-02-06 Christian Urban minor
2010-02-06 Christian Urban some tuning
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk Fixes for Bex1 removal.
2010-02-05 Cezary Kaliszyk Cleaned Terms using [lifted] and found a workaround for the instantiation problem.
2010-02-05 Cezary Kaliszyk A procedure that properly instantiates the types too.
2010-02-05 Cezary Kaliszyk More code abstracted away
2010-02-05 Cezary Kaliszyk A bit more intelligent and cleaner code.
2010-02-05 Cezary Kaliszyk merge
2010-02-05 Cezary Kaliszyk A proper version of the attribute
2010-02-05 Christian Urban merged
2010-02-05 Christian Urban eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts
2010-02-04 Cezary Kaliszyk The automatic lifting translation function, still with dummy types,
2010-02-04 Cezary Kaliszyk Quotdata_dest needed for lifting theorem translation.
2010-02-04 Christian Urban fixed (permute_eqvt in eqvts makes this simpset always looping)
2010-02-04 Christian Urban rollback of the test
2010-02-04 Christian Urban linked versions - instead of copies
2010-02-04 Christian Urban merged
2010-02-04 Christian Urban restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw
2010-02-03 Cezary Kaliszyk More let-rec experiments
2010-02-03 Christian Urban proposal for an alpha equivalence
2010-02-03 Cezary Kaliszyk Lets different.
2010-02-03 Cezary Kaliszyk Simplified the proof.
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban proved that bv for lists respects alpha for terms
2010-02-03 Cezary Kaliszyk Finished remains on the let proof.
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk Lets are ok.
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban added type-scheme example
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk Definitions for trm5
2010-02-03 Christian Urban another adaptation for the eqvt-change
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban fixed proofs that broke because of eqvt
2010-02-03 Cezary Kaliszyk Minor fix.
2010-02-03 Cezary Kaliszyk merge
2010-02-03 Cezary Kaliszyk alpha5 pseudo-injective
2010-02-03 Christian Urban fixed proofs in Abs.thy
2010-02-03 Christian Urban merged
2010-02-03 Christian Urban added a first eqvt_tac which pushes permutations inside terms
2010-02-03 Cezary Kaliszyk The alpha-equivalence relation for let-rec. Not sure if correct...
2010-02-03 Cezary Kaliszyk Starting with a let-rec example.
2010-02-03 Cezary Kaliszyk Minor
2010-02-03 Cezary Kaliszyk Some cleaning and eqvt proof
2010-02-03 Cezary Kaliszyk The trm1_support lemma explicitly and stated a strong induction principle.
2010-02-03 Cezary Kaliszyk More ingredients in Terms.
2010-02-02 Cezary Kaliszyk Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)
2010-02-02 Cezary Kaliszyk More in Terms
2010-02-02 Cezary Kaliszyk First experiments in Terms.
2010-02-02 Cezary Kaliszyk LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.
2010-02-02 Cezary Kaliszyk Disambiguating the syntax.
2010-02-02 Cezary Kaliszyk Minor uncommited changes from LamEx2.
2010-02-02 Cezary Kaliszyk Some equivariance machinery that comes useful in LF.
2010-02-02 Cezary Kaliszyk Generalized the eqvt proof for single binders.
2010-02-02 Cezary Kaliszyk With induct instead of induct_tac, just one induction is sufficient.
2010-02-02 Cezary Kaliszyk General alpha_gen_trans for one-variable abstraction.
2010-02-02 Cezary Kaliszyk With unfolding Rep/Abs_eqvt no longer needed.
2010-02-02 Cezary Kaliszyk Lam2 finished apart from Rep_eqvt.
2010-02-01 Cezary Kaliszyk merge
2010-02-01 Cezary Kaliszyk All should be ok now.
2010-02-01 Christian Urban repaired according to changes in Abs.thy
2010-02-01 Christian Urban added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case
2010-02-01 Christian Urban cleaned
2010-02-01 Christian Urban updated from huffman
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
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
(0) -1000 -480 +480 +1000 tip