merged

polished

Update Test to use fset.

merge

Use fs typeclass in showing finite support + some cheat cleaning.

merged

more one the paper

Keep only one copy of infinite_Un.

Added a missing 'import'.

Showed the instance: fset::(at) fs

merge

Remove atom_decl from the parser.

TySch strong induction looks ok.

Working on TySch strong induction.

Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable...

merged

more tuning on the paper

The nominal infrastructure for fset. 'fs' missing, but not needed so far.

A few more theorems in FSet.

merge 2

merge 1

support of fset_to_set, support of fmap_atom.

merged

more tuning on the paper

added item about size functions

merge

Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed.

tuned

another little bit for the introduction

Leroy96 supp=fv and fixes to make it compile

merged

more of the introduction

merge

Added a cleaned version of FSet.

corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant

Continued description of alpha.

Rename "_property" to ".property"

First part of the description of alpha_ty.

Description of generation of alpha_bn.

case names also for _induct

Case_Names for _inducts. Does not work for _induct yet.

Added fv,bn,distinct,perm to the simplifier.

merge

Simplified the description.

merged

slightly more in the paper

Update the description of the generation of fv function.

fv_bn may need to call other fv_bns.

Update TODO.

Which proofs need a 'sorry'.

added TODO

vixed variable names

simplified strong induction proof by using flip

Rename bound variables + minor cleaning.

Move most of the exporting out of the parser.

Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.

Prove eqvts on exported terms.

Clean 'Lift', start working only on exported things in Parser.

slightly more of the paper

merged

paper uses now a heap file - does not compile so long anymore

merge

compose_sym2 works also for term5

Updated Term1, including statement of strong induction.

Proper compose_sym2

merged

temporarily disabled tests in Nominal/ROOT

made paper to compile

added partial proof for the strong induction principle

Trying to find a compose lemma for 2 arguments.

merge

cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.

merged

added proof of supp/fv for type schemes

Updated Type Schemes to automatic lifting. One goal is not true because of the restriction.

Remove Term5a, since it is now identical to Term5.

merge

Finished all proofs in Term5 and Term5n.

added partial proof of supp for type schemes

Fix in alpha; support of the recursive Let works :)

The recursive supp just has one equation too much.

Fix for the change of alpha_gen.

merge

Generate compound FV and Alpha for recursive bindings.

Lifting theorems with compound fv and compound alpha.

commented out examples that should not work; but for example type-scheme example should work

added another supp-proof for the non-recursive case

Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not.

merge

The old recursive alpha works fine.

added the final unfolded result

merge and proof of support for non-recursive case

Added Term5 non-recursive. The bug is there only for the recursive case.

Alpha is wrong.

alpha_bn doesn't need the permutation in non-recursive case.

alpha5_transp and equivp

alpha5_symp proved.

FV_bn generated for recursive functions as well, and used in main fv for bindings.

The proof in 'Test' gets simpler.

Removed pi o bn = bn' assumption in alpha

merged (confirmed to work with Isabelle from 6th March)

another synchronisation

proof for support when bn-function is present, but fb_function is empty

fv_eqvt_cheat no longer needed.

derive "inducts" from "induct" instead of lifting again is much faster.

build_eqvts works with recursive case if proper induction rule is used.

cheat_alpha_eqvt no longer needed; the proofs work.

LF works with new alpha...?

explicit flag "cheat_equivp"

Prove alpha_gen_compose_eqvt

Use eqvt.

added preliminary test version....but Test works now

added an eqvt-proof for bi

synchronised with main hg-repository; used add_typedef_global in nominal_atoms

localised the typedef in Attic (requires new Isabelle)

started supp-fv proofs (is going to work)

Even with pattern simplified to a single clause, the supp equation doesn't seem true.

Still don't know how to prove supp=fv for simplest Let...

Do not fail if the finite support proof fails.

generalised the supp for atoms to all concrete atoms (not just names)