Wrapped the permutation code.

Description of intended bindings.

Code for generating the fv function, no bindings yet.

merge

indent

merge

Simplifying perm_eq

merge

indenting

Minor

Merge

Ported Stefan's permutation code, still needs some localizing.

merge

Removed varifyT.

merged

2-spaces rule (where it makes sense)

merge

Fixed the definition of less and finished the missing proof.

further tuning

small tuning

tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy

der_bname -> derived_bname

Names of files.

Finished introducing the binding.

Synchronize the commands.

Passing the binding to quotient_def

Added a binding to the parser.

Second inline

remove one-line wrapper.

Undid the read_terms change; now compiles.

merge

renamed 'as' to 'is' everywhere.

"is" defined as the keyword

moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned

The lattice instantiations are gone from Isabelle/Main, so this can be removed.

the lam/bla example.

Finished a working foo/bar.

fv_foo is not regular.

Testing foo/bar

Even when bv = fv it still doesn't lift.

Added the missing syntax file

Notation available locally

Main renaming + fixes for new Isabelle in IntEx2.

Merging QuotBase into QuotMain.

removed dead code

cleaned a bit

lowercase locale

hg-added the added file.

Changes from Makarius's code review + some noticed fixes.

example with a respectful bn function defined over the type itself

Finishe the renaming.

Another mistake found with OTT.

merge

Fixed rbv6, when translating to OTT.

Some cleaning of proofs.

merged again

merged

more minor space and bracket modifications.

More changes according to the standards.

A concrete example, with a proof that rbv is not regular and with proofs of induction and pseudo-injectivity that require this

proper declaration of types and terms during parsing (removes the varifyT when storing data)

merged

slight correction

merge

More about trm6

merged

the specifications of the respects.

trm6 with the 'Foo' constructor.

removing unnecessary brackets

More indentation cleaning.

'exc' -> 'exn' and more name and space cleaning.

Fully qualified exception names.

merge

More indentation, names and todo cleaning in the quotient package

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

minor

test about supp/freshness for lam (old proofs work in principle - for single binders)

Recommited the changes for nitpick

Correct types which fixes the printing.

fv for subterms

Fix the problem with later examples. Maybe need to go back to textual specifications.

Some processing of variables in constructors to get free variables.

Parsing of the input as terms and types, and passing them as such to the function package.

Undid the parsing, as it is not possible with thy->lthy interaction.

merge

Some cleaning of thy vs lthy vs context.

merged

tuned comment

completely ported

Another string in the specification.

Variable takes a 'name'.

merge

When commenting discovered a missing case of Babs->Abs regularization.

merged

mostly ported Terms.thy to new Nominal

merge

Commenting regularize

very rough example file for how nominal2 specification can be parsed

reordered cases in regularize (will be merged into two cases)

use of equiv_relation_chk in quotient_term

some slight tuning

added Terms to Nominal - Instantiation of two types does not work (ask Florian)

added another example with indirect recursion over lists

just moved obsolete material into Attic

added an LamEx example together with the new nominal infrastructure

Bex1_Bexeq_regular.

Hom Theorem with exists unique

2 cases for regularize with split, lemmas with split now lift.

Simpler statement that has the problem.

Found a term that does not regularize.

A triple is still ok.

Combined the simpsets in clean_tac and updated the comment. Now cleaning of splits does work.

Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.

Sigma cleaning works with split_prs (still manual proof).

tuned

merged

cleaning of QuotProd; a little cleaning of QuotList

added prs and rsp lemmas for Inl and Inr

used split_option_all lemma

used the internal Option.map instead of custom option_map

Generalized split_prs and split_rsp