Started proving strong induction.

stating the strong induction; further.

Working on stating induct.

some tuning; possible fix for strange paper generation

more on the paper

merge

Showed support of Core Haskell

Support proof modification for Core Haskell.

Experiments with Core Haskell support.

Export all the cheats needed for Core Haskell.

Compute Fv for non-recursive bn functions calling other bn functions

Core Haskell experiments.

tuned paper

more of the paper

merged

more tuning in the paper

merge

Parsing bn functions that call other bn functions and transmitting this information to fv/alpha.

merged

more tuning

tuned paper

more on the paper

merge

Modification to Core Haskell to make it accepted with an empty binding function.

merged

tuned paper

Initial list unfoldings in Core Haskell.

compiles

More modification needed for compilation

Moved let properties from Term5 to ExLetRec.

Move Let properties to ExLet

Added missing file

More reorganization.

Move Leroy out of Test, rename accordingly.

Term1 is identical to Example 3

Move example3 out.

Move Ex1 and Ex2 out of Test

Move examples which create more permutations out

Move LamEx out of Test.

Move lambda examples to manual

Move manual examples to a subdirectory.

Removed compat tests.

merge

Move Non-respectful examples to NotRsp

merged

more on the paper

Move the comment to appropriate place.

Remove compose_eqvt

sym proof with compose.

Marked the place where a compose lemma applies.

merge

equivp_cheat can be removed for all one-permutation examples.

merged

more on the paper

merged

tuned paper

Got rid of alpha_bn_rsp_cheat.

alpha_bn_rsp_pre automatized.

merge

fv_rsp proved automatically.

more on the paper

merged

tuned paper

some tuning

Strong induction for Type Schemes.

Fixed missing colon.

tuned paper

merged

proved at_set_avoiding2 which is needed for strong induction principles

moved lemmas supp_perm_eq and exists_perm to Nominal2_Supp

Size experiments.

Use 'alpha_bn_refl' to get rid of one of the sorrys.

Build alpha-->alphabn implications

Prove reflp for all relations.

started cleaning up and introduced 3 versions of ~~gen

moved infinite_Un into mainstream Isabelle; moved permute_boolI/E lemmas

more work on the paper

Described automatically created funs.

merge

Automatically derive support for datatypes with at-most one binding per constructor.

picture

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)

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.

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

added distinctness of perms

updated (added lemma about commuting permutations)

Change type schemes to name set.

More fixes for new alpha, the whole lift script should now work again.

Length fix for nested recursions.

Fix equivp.

Fixed eqvt code.

most tests work - the ones that do not I commented out

merge

Add a check of fv_functions.

some tuning

Link calls to Raw permutations, FV definition and alpha_definition into the parser.

merged

rawified the bind specs (ready to be used now)

merge

Trying to prove equivariance.

modified for new binding format - hope it is the intended one

further code-refactoring in the parser

The new alpha-equivalence and testing in Trm2 and Trm5.

slight simplification of the raw-decl generation

Example that shows that current alpha is wrong.

added example from my phd

streamlined parser

generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"

More about the general lifting procedure.

Update TODO

Progress with general lifting procedure.

RSP of perms can be shown in one go.

Change in signature of prove_const_rsp for general lifting.

Permutation and FV_Alpha interface change.

To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.

merge

Preparing the generalized lifting procedure

merged

added ott-example about Leroy96

Forgot to add one file.

Split Terms into separate files and add them to tests.

merge

Move the eqvt code out of Terms and fixed induction for single-rule examples.

merged

a few simplifications

first attempt to make sense out of the core-haskell definition

Code for proving eqvt, still in Terms.

Use eqvt infrastructure.

Simple function eqvt code.

added IsaMakefile...but so far included only a test for the parser

moved Quot package to Attic (still compiles there with "isabelle make")

merged

moved Nominal to "toplevel"

Export perm_frees.

Restructuring the code in Perm

Simplified and finised eqvt proofs for t1 and t5

merge

Define lifted perms.

merged

parsing and definition of raw datatype and bv-function work (not very beautiful)

With permute_rsp we can lift the instance proofs :).

Note the instance proofs, since they can be easily lifted.

More refactoring and removed references to the global simpset in Perm.

Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.

Regularize finite support proof for trm1

Made the fv-supp proof much more straightforward.

Regularize the proofs about finite support.

Respects of permute and constructors.

Generate fv_rsp automatically.

Define the constants automatically.

Rename also the lifted types to non-capital.

Use the infrastructure in LF. Much shorter :).

Final synchronization of names.

LF renaming part 3 (proper names of alpha equvalences)

LF renaming part 2 (proper fv functions)

merge

LF renaming part1.

merged

parsing of function definitions almost works now; still an error with undefined constants

merge

rsp for bv; the only issue is that it requires an appropriate induction principle.

merged

declarartion of the raw datatype already works; raw binding functions throw an exception about mutual recursive types

rsp infrastructure.

merge

Progress towards automatic rsp of constants and fv.

merged

"raw"-ified the term-constructors and types given in the specification

Looking at proving the rsp rules automatically.

Minor beutification.

Define the quotient from ML

All works in LF but will require renaming.

Reordering in LF.

Fixes for auxiliary datatypes.

Fixed pseudo_injectivity for trm4

Testing auto equivp code.

A tactic for final equivp

More equivp infrastructure.

tactify transp

export the reflp and symp tacs.

Generalize atom_trans and atom_sym.

Some progress about transp

alpha-symmetric addons.

alpha reflexivity

Renaming.

Added missing description.

Added Brian's suggestion.

Update TODO

Removed bindings 'in itself' where possible.

Some adaptation

proof cleaning and standardizing.

Automatic production and proving of pseudo-injectivity.

Experiments for the pseudo-injectivity tactic.

merge

Constructing alpha_inj goal.

merged

start work with the parser

Full alpha equivalence + testing in terms. Some differ but it seems the generated version is more correct.

First (non-working) version of alpha-equivalence

Description of the fv procedure.

Testing auto constant lifting.

Fix for new Isabelle (primrec)

Automatic lifting of constants.

Changed back to original version of trm5

The alternate version of trm5 with additional binding. All proofs work the same.

Code for handling atom sets.

Replace Terms by Terms2.

Fixed proofs in Terms2 and found a mistake in Terms.

Terms2 with bindings for binders synchronized with bindings they are used in.

Cleaning of proofs in Terms.

Testing Fv

Fix the strong induction principle.

Reorder

Add bindings of recursive types by free_variables.

Bindings adapted to multiple defined datatypes.

Reorganization

Now should work.

Some optimizations and fixes.

Simplified format of bindings.

Tested the Perm code; works everywhere in Terms.

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.