merged

a few more attempts to show the equivalence between old and new way of defining alpha-equivalence

minor tuning

Explicitly marked what is bound.

Cleaning and updating in Terms.

Looking at the trm2 example

Fixed pattern matching, now the test in Abs works correctly.

added a test case

merged

moved some lemmas to Nominal; updated all files

merge

Comments.

slightly tuned

Proper context fixes lifting inside instantiations.

Fixed the context import/export and simplified LFex.

added 2 papers about core haskell

fixed lemma name

updated to latest Nominal2

minor

some tuning

merge

merge

Fixes for Bex1 removal.

Cleaned Terms using [lifted] and found a workaround for the instantiation problem.

A procedure that properly instantiates the types too.

More code abstracted away

A bit more intelligent and cleaner code.

merge

A proper version of the attribute

merged

eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts

The automatic lifting translation function, still with dummy types, but works everywhere in the LF example.

Quotdata_dest needed for lifting theorem translation.

fixed (permute_eqvt in eqvts makes this simpset always looping)

rollback of the test

linked versions - instead of copies

merged

restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw

More let-rec experiments

proposal for an alpha equivalence

Lets different.

Simplified the proof.

merged

proved that bv for lists respects alpha for terms

Finished remains on the let proof.

merge

Lets are ok.

merged

added type-scheme example

merge

Definitions for trm5

another adaptation for the eqvt-change

merged

fixed proofs that broke because of eqvt

Minor fix.

merge

alpha5 pseudo-injective

fixed proofs in Abs.thy

merged

added a first eqvt_tac which pushes permutations inside terms

The alpha-equivalence relation for let-rec. Not sure if correct...

Starting with a let-rec example.

Minor

Some cleaning and eqvt proof

The trm1_support lemma explicitly and stated a strong induction principle.

More ingredients in Terms.

Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)

More in Terms

First experiments in Terms.

LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.

Disambiguating the syntax.

Minor uncommited changes from LamEx2.

Some equivariance machinery that comes useful in LF.

Generalized the eqvt proof for single binders.

With induct instead of induct_tac, just one induction is sufficient.

General alpha_gen_trans for one-variable abstraction.

With unfolding Rep/Abs_eqvt no longer needed.

Lam2 finished apart from Rep_eqvt.

merge

All should be ok now.

repaired according to changes in Abs.thy

added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case

cleaned

updated from huffman

updated from nominal-huffman

Fixed wrong rename.

merge

Lambda based on alpha_gen, under construction.

updated from huffman - repo

renamed Abst/abst to Abs/abs

got rid of RAbst type - is now just pairs

Monotonicity of ~~gen, needed for using it in inductive definitions.

The current state of fv vs supp proofs in LF.

merge

More proofs in the LF example.

merged

slight tuning

renamed function according to the name of the constant

fixed problem with Bex1_rel renaming

Ported LF to the generic lambda and solved the simpler _supp cases.

merged

introduced a generic alpha (but not sure whether it is helpful)

More in the LF example in the new nominal way, all is clear until support.

Fixed the induction problem + some more proofs.

equivariance of rfv and alpha.

Added the experiments with fun and function.

now also final step is proved - the supp of lambdas is now completely characterised

the supp of a lambda can now be characterised, *provided* the notion of free variables coincides with support on lambda terms

improved the proof slightly by defining alpha as a function and completely characterised the equality between two abstractions

merged

general abstraction operator and complete characterisation of its support and freshness

Ported existing part of LF to new permutations and alphas.

attempt of a general abstraction operator

attempt to prove equivalence between alpha definitions

End of renaming.

Minor when looking at lam.distinct and lam.inject

Renamed Bexeq to Bex1_rel

Substracting bounds from free variables.

Improper interface for datatype and function packages and proper interface lateron.

merged