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
(0) -1000 -240 +240 +1000 tip