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.

With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.

More fine-grained nominal restriction for debugging.

Fix permutation addition.

Update the comments

Gather bindings with same binder, and generate only one permutation for them.

Undo effects of simp.

merged

updated to renamings in Isabelle

merged

merged

more proofs in Abs and work on Core Haskell

added a lemma that permutations can be represented as sums of swapping

Still unable to show supp=fv for let with one existential.

Ported LF to the parser interface.

merge

Lift fv and bn eqvts; no need to lift alpha_eqvt.

Not much progress about the single existential let case.

Fixed LF for one quantifier over 2 premises.

Trying to fix the proofs for the single existential... So far failed.

Lift distinct.

Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.

Lift BV,FV,Permutations and injection :).

Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.

A version that just leaves the supp/\supp goal. Obviously not true.

Prove symp and transp of weird without the supp /\ supp = {} assumption.

merge

Experiments with proving weird transp

Code for solving symp goals with multiple existentials.

reflp for multiple quantifiers.

fixed mess in Test.thy

Fix eqvt for multiple quantifiers.

only tuned

merged

start of paper - does not compile yet

added ACM style file for ICFP

weird eqvt

Add the supp intersection conditions.

Comment out the part that does not work with 2 quantifiers.

Fixes for the fv problem and alpha problem.

merged

preliinary test about alpha-weirdo

Another problem with permutations in alpha and possibly also in fv

potential problem with the phd-example, where two permutations are generated, but only one is used

Some tests around Term4. Not sure how to fix the generated fv function.

merge

Porting from Lift to Parser; until defining the Quotient type.

Add image_eqvt and atom_eqvt to eqvt bases.

Include the raw eqvt lemmas.

merged

added some more examples from Peter Sewell's bestiary

merge

Minor

Working bv_eqvt

Moving wrappers out of Lift.

merged