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

All eq_reflections apart from the one of 'id_apply' can be removed.

continued

More eqreflection/equiv cleaning.

more eq_reflection & other cleaning.

Removing more eq_reflections.

ids *cannot* be object equalities

re-inserted lemma in QuotList

added prs and rsp lemmas for Some and None

tuned proofs (mainly in QuotProd)

properly commented out the "unused lemmas section" and moved actually used lemmas elsewhere; added two minor items to the TODO list

renamed QuotScript to QuotBase

cleaned some theorems

test with splits

The alpha equivalence relations for structures in 'Terms'

More experiments with defining the homomorphism directly, lifting of 'distinct' and of 'exhaust'.

Trying to define hom for the lifted type directly.

Proper alpha equivalence for Sigma calculus.

Changed fun_map and rel_map to definitions.

Lifted Peter's Sigma lemma with Ex1.

Automatic injection of Bexeq

Automatic cleaning of Bexeq<->Ex1 theorems.

Using Bexeq_rsp, and manually lifted lemma with Ex1.

Bexeq definition, Ex1_prs lemma, Bex1_rsp lemma, compiles.

The missing rule.

Ex1 -> Bex1 Regularization, Preparing Exeq.

Added the Sigma Calculus example

Better error messages for non matching quantifiers.

Statement of term1_hom_rsp

proved that the function is a function

term1_hom as a function

A version of hom with quantifiers.

added permutation functions for the raw calculi

fixed broken (partial) proof

used "new" alpha-equivalence relation (according to new scheme); proved equivalence theorems and so on

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

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

tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely

merged

added free_variable function (do not know about the algorithm yet)

hom lifted to hom', so it is true. Infrastructure for partially regularized quantifiers. Nicer errors for regularize.

slight tuning of relation_error

Appropriate respects and a statement of the lifted hom lemma

recursion-hom for lambda

Incorrect version of the homomorphism lemma

trivial

tuned quotient_typ.ML

tuned quotient_def.ML and cleaned somewhat LamEx.thy

a few more lemmas...except supp of lambda-abstractions

removed one sorry

nearly all of the proof