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)

support of atoms at the end of Abs.thy

Trying to prove atom_image_fresh_swap

Finite_support proof no longer needed in LF.

Show that the new types are in finite support typeclass.

mk_supports_eq and supports_tac.

merge

Fixes for term1 for new alpha. Still not able to show support equations.

merged

finally the proof that new and old alpha agree

Remove "_raw" from lifted theorems.

looking at trm5_equivp

The cheats described explicitely.

The alpha5_eqvt tactic works if I manage to build the goal.

With the 4 cheats, all examples fully lift.

Lift alpha_bn_constants.

Lifting constants.

Proper error message.

Lifting constants works for all examples.

Remove tracing from fv/alpha.

Equivp working only on the standard alpha-equivalences.

explicit cheat_fv_eqvt

extract build_eqvts_tac.

build_eqvts no longer requires permutations.

Add explicit alpha_eqvt_cheat.

Export tactic out of alpha_eqvt.

merge

More tries about the proofs in trm5

merged

almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining)

alpha_equivp for trm5

Undoing mistakenly committed parser experiments.

alpha_eqvt for recursive term1.

Looking at alpha_eqvt for term5, not much progress.

Reordered examples in Test.

Allows multiple bindings with same lhs.

Linked parser to fv and alpha.

merge

A minor fix for shallow binders. LF works again.

merged

parser produces ordered bn-fun information

Testing equalities in trm5, all seems good.

Fv&Alpha seem to work.

include alpha in the definitions.

Filled the algorithm for alpha_bn_arg

rhs of alpha_bn, and template for the arguments.

alpha_bn_constr template

exported template for alpha_bn

merge

Use alpha_bns in normal alpha defs.

alpha_bn_frees

merged

added bn-information, but it is not yet ordered according to the dts

Separate lists for separate constructors, to match bn_eqs.

All examples should work.

Fix to get old alpha.

Separate primrecs in Fv.

A version of Fv that takes into account recursive and non-recursive bindings.

Trying to prove that old alpha is the same as new recursive one. Lets still to do.

fv_bi and alpha_bi

merged

added first test about new compat

fv_compat

added another compat example

added a test-file for compatibility

added compat definitions to some examples

Proper recognition of atoms and atom sets.

deleted comments about "weird"

merged

updated to new Isabelle

Term5 written as nominal_datatype is the recursive let.