nominal2: Graph

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, by Christian Urban
More about the general lifting procedure.
2010-02-26, by Cezary Kaliszyk
Update TODO
2010-02-26, by Cezary Kaliszyk
Progress with general lifting procedure.
2010-02-26, by Cezary Kaliszyk
RSP of perms can be shown in one go.
2010-02-26, by Cezary Kaliszyk
Change in signature of prove_const_rsp for general lifting.
2010-02-26, by Cezary Kaliszyk
Permutation and FV_Alpha interface change.
2010-02-26, by Cezary Kaliszyk
To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-26, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Preparing the generalized lifting procedure
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
added ott-example about Leroy96
2010-02-25, by Christian Urban
Forgot to add one file.
2010-02-25, by Cezary Kaliszyk
Split Terms into separate files and add them to tests.
2010-02-25, by Cezary Kaliszyk
merge
2010-02-25, by Cezary Kaliszyk
Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25, by Cezary Kaliszyk
merged
2010-02-25, by Christian Urban
a few simplifications
2010-02-25, by Christian Urban
first attempt to make sense out of the core-haskell definition
2010-02-25, by Christian Urban
Code for proving eqvt, still in Terms.
2010-02-25, by Cezary Kaliszyk
Use eqvt infrastructure.
2010-02-25, by Cezary Kaliszyk
Simple function eqvt code.
2010-02-25, by Cezary Kaliszyk
added IsaMakefile...but so far included only a test for the parser
2010-02-25, by Christian Urban
moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25, by Christian Urban
merged
2010-02-25, by Christian Urban
moved Nominal to "toplevel"
2010-02-25, by Christian Urban
Export perm_frees.
2010-02-25, by Cezary Kaliszyk
Restructuring the code in Perm
2010-02-24, by Cezary Kaliszyk
Simplified and finised eqvt proofs for t1 and t5
2010-02-24, by Cezary Kaliszyk
merge
2010-02-24, by Cezary Kaliszyk
Define lifted perms.
2010-02-24, by Cezary Kaliszyk
merged
2010-02-24, by Christian Urban
parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24, by Christian Urban
With permute_rsp we can lift the instance proofs :).
2010-02-24, by Cezary Kaliszyk
Note the instance proofs, since they can be easily lifted.
2010-02-24, by Cezary Kaliszyk
More refactoring and removed references to the global simpset in Perm.
2010-02-24, by Cezary Kaliszyk
Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24, by Cezary Kaliszyk
Regularize finite support proof for trm1
2010-02-24, by Cezary Kaliszyk
Made the fv-supp proof much more straightforward.
2010-02-24, by Cezary Kaliszyk
Regularize the proofs about finite support.
2010-02-24, by Cezary Kaliszyk
Respects of permute and constructors.
2010-02-24, by Cezary Kaliszyk
Generate fv_rsp automatically.
2010-02-24, by Cezary Kaliszyk
Define the constants automatically.
2010-02-24, by Cezary Kaliszyk
Rename also the lifted types to non-capital.
2010-02-24, by Cezary Kaliszyk
Use the infrastructure in LF. Much shorter :).
2010-02-24, by Cezary Kaliszyk
Final synchronization of names.
2010-02-24, by Cezary Kaliszyk
LF renaming part 3 (proper names of alpha equvalences)
2010-02-24, by Cezary Kaliszyk
LF renaming part 2 (proper fv functions)
2010-02-24, by Cezary Kaliszyk
merge
2010-02-24, by Cezary Kaliszyk
LF renaming part1.
2010-02-24, by Cezary Kaliszyk
merged
2010-02-24, by Christian Urban
parsing of function definitions almost works now; still an error with undefined constants
2010-02-24, by Christian Urban
merge
2010-02-23, by Cezary Kaliszyk
rsp for bv; the only issue is that it requires an appropriate induction principle.
2010-02-23, by Cezary Kaliszyk
merged
2010-02-23, by Christian Urban
declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types
2010-02-23, by Christian Urban
rsp infrastructure.
2010-02-23, by Cezary Kaliszyk
merge
2010-02-23, by Cezary Kaliszyk
Progress towards automatic rsp of constants and fv.
2010-02-23, by Cezary Kaliszyk
merged
2010-02-23, by Christian Urban
"raw"-ified the term-constructors and types given in the specification
2010-02-23, by Christian Urban
Looking at proving the rsp rules automatically.
2010-02-23, by Cezary Kaliszyk
Minor beutification.
2010-02-23, by Cezary Kaliszyk
Define the quotient from ML
2010-02-23, by Cezary Kaliszyk
All works in LF but will require renaming.
2010-02-23, by Cezary Kaliszyk
Reordering in LF.
2010-02-23, by Cezary Kaliszyk
Fixes for auxiliary datatypes.
2010-02-23, by Cezary Kaliszyk
Fixed pseudo_injectivity for trm4
2010-02-22, by Cezary Kaliszyk
Testing auto equivp code.
2010-02-22, by Cezary Kaliszyk
A tactic for final equivp
2010-02-22, by Cezary Kaliszyk
More equivp infrastructure.
2010-02-22, by Cezary Kaliszyk
tactify transp
2010-02-22, by Cezary Kaliszyk
export the reflp and symp tacs.
2010-02-22, by Cezary Kaliszyk
Generalize atom_trans and atom_sym.
2010-02-22, by Cezary Kaliszyk
Some progress about transp
2010-02-22, by Cezary Kaliszyk
alpha-symmetric addons.
2010-02-22, by Cezary Kaliszyk
alpha reflexivity
2010-02-22, by Cezary Kaliszyk
Renaming.
2010-02-22, by Cezary Kaliszyk
Added missing description.
2010-02-22, by Cezary Kaliszyk
Added Brian's suggestion.
2010-02-22, by Cezary Kaliszyk
Update TODO
2010-02-22, by Cezary Kaliszyk
Removed bindings 'in itself' where possible.
2010-02-21, by Cezary Kaliszyk
Some adaptation
2010-02-20, by Cezary Kaliszyk
proof cleaning and standardizing.
2010-02-19, by Cezary Kaliszyk
Automatic production and proving of pseudo-injectivity.
2010-02-19, by Cezary Kaliszyk
Experiments for the pseudo-injectivity tactic.
2010-02-19, by Cezary Kaliszyk
merge
2010-02-19, by Cezary Kaliszyk
Constructing alpha_inj goal.
2010-02-19, by Cezary Kaliszyk
merged
2010-02-18, by Christian Urban
start work with the parser
2010-02-18, by Christian Urban
Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.
2010-02-18, by Cezary Kaliszyk
First (non-working) version of alpha-equivalence
2010-02-18, by Cezary Kaliszyk
Description of the fv procedure.
2010-02-18, by Cezary Kaliszyk
Testing auto constant lifting.
2010-02-18, by Cezary Kaliszyk
Fix for new Isabelle (primrec)
2010-02-18, by Cezary Kaliszyk
Automatic lifting of constants.
2010-02-18, by Cezary Kaliszyk
Changed back to original version of trm5
2010-02-18, by Cezary Kaliszyk
The alternate version of trm5 with additional binding. All proofs work the same.
2010-02-18, by Cezary Kaliszyk
Code for handling atom sets.
2010-02-18, by Cezary Kaliszyk
Replace Terms by Terms2.
2010-02-18, by Cezary Kaliszyk
Fixed proofs in Terms2 and found a mistake in Terms.
2010-02-18, by Cezary Kaliszyk
Terms2 with bindings for binders synchronized with bindings they are used in.
2010-02-17, by Cezary Kaliszyk
Cleaning of proofs in Terms.
2010-02-17, by Cezary Kaliszyk
Testing Fv
2010-02-17, by Cezary Kaliszyk
Fix the strong induction principle.
2010-02-17, by Cezary Kaliszyk
Reorder
2010-02-17, by Cezary Kaliszyk
Add bindings of recursive types by free_variables.
2010-02-17, by Cezary Kaliszyk
Bindings adapted to multiple defined datatypes.
2010-02-17, by Cezary Kaliszyk
Reorganization
2010-02-17, by Cezary Kaliszyk
Now should work.
2010-02-17, by Cezary Kaliszyk
Some optimizations and fixes.
2010-02-17, by Cezary Kaliszyk
Simplified format of bindings.
2010-02-17, by Cezary Kaliszyk
Tested the Perm code; works everywhere in Terms.
2010-02-17, by Cezary Kaliszyk
Wrapped the permutation code.
2010-02-17, by Cezary Kaliszyk
Description of intended bindings.
2010-02-17, by Cezary Kaliszyk
Code for generating the fv function, no bindings yet.
2010-02-17, by Cezary Kaliszyk
merge
2010-02-17, by Cezary Kaliszyk
indent
2010-02-17, by Cezary Kaliszyk
merge
2010-02-17, by Cezary Kaliszyk
Simplifying perm_eq
2010-02-17, by Cezary Kaliszyk