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.

further tuning

small tuning

tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy

der_bname -> derived_bname

Names of files.

Finished introducing the binding.

Synchronize the commands.

Passing the binding to quotient_def

Added a binding to the parser.

Second inline

remove one-line wrapper.

Undid the read_terms change; now compiles.

merge

renamed 'as' to 'is' everywhere.

"is" defined as the keyword

moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned

The lattice instantiations are gone from Isabelle/Main, so this can be removed.

the lam/bla example.

Finished a working foo/bar.

fv_foo is not regular.

Testing foo/bar

Even when bv = fv it still doesn't lift.

Added the missing syntax file

Notation available locally

Main renaming + fixes for new Isabelle in IntEx2.

Merging QuotBase into QuotMain.

removed dead code

cleaned a bit

lowercase locale

hg-added the added file.

Changes from Makarius's code review + some noticed fixes.

example with a respectful bn function defined over the type itself

Finishe the renaming.

Another mistake found with OTT.

merge

Fixed rbv6, when translating to OTT.

Some cleaning of proofs.

merged again

merged

more minor space and bracket modifications.

More changes according to the standards.

A concrete example, with a proof that rbv is not regular and with proofs of induction and pseudo-injectivity that require this

proper declaration of types and terms during parsing (removes the varifyT when storing data)

merged

slight correction

merge

More about trm6

merged

the specifications of the respects.

trm6 with the 'Foo' constructor.

removing unnecessary brackets

More indentation cleaning.

'exc' -> 'exn' and more name and space cleaning.

Fully qualified exception names.

merge

More indentation, names and todo cleaning in the quotient package

merged

a few more attempts to show the equivalence between old and new way of defining alpha-equivalence

minor tuning

Explicitly marked what is bound.

Cleaning and updating in Terms.

Looking at the trm2 example

Fixed pattern matching, now the test in Abs works correctly.

added a test case

merged

moved some lemmas to Nominal; updated all files

merge

Comments.

slightly tuned

Proper context fixes lifting inside instantiations.

Fixed the context import/export and simplified LFex.

added 2 papers about core haskell

fixed lemma name

updated to latest Nominal2

minor

some tuning

merge

merge

Fixes for Bex1 removal.

Cleaned Terms using [lifted] and found a workaround for the instantiation problem.

A procedure that properly instantiates the types too.

More code abstracted away

A bit more intelligent and cleaner code.

merge

A proper version of the attribute

merged

eqvts and eqvts_raw are separate thm-lists; otherwise permute_eqvt is problematic as it causes looks in eqvts

The automatic lifting translation function, still with dummy types, but works everywhere in the LF example.

Quotdata_dest needed for lifting theorem translation.

fixed (permute_eqvt in eqvts makes this simpset always looping)

rollback of the test

linked versions - instead of copies

merged

restored the old behaviour of having an eqvts list; the transformed theorems are stored in eqvts_raw

More let-rec experiments

proposal for an alpha equivalence

Lets different.

Simplified the proof.

merged

proved that bv for lists respects alpha for terms

Finished remains on the let proof.

merge

Lets are ok.

merged

added type-scheme example

merge

Definitions for trm5

another adaptation for the eqvt-change

merged

fixed proofs that broke because of eqvt

Minor fix.

merge

alpha5 pseudo-injective

fixed proofs in Abs.thy

merged

added a first eqvt_tac which pushes permutations inside terms

The alpha-equivalence relation for let-rec. Not sure if correct...

Starting with a let-rec example.

Minor

Some cleaning and eqvt proof

The trm1_support lemma explicitly and stated a strong induction principle.

More ingredients in Terms.

Finished the supp_fv proof; first proof that analyses the structure of 'Let' :)

More in Terms

First experiments in Terms.

LF ported to alpha_gen, equivp solved and one of the missing proofs in support<-> fv solved. Still some supp properties left.

Disambiguating the syntax.

Minor uncommited changes from LamEx2.

Some equivariance machinery that comes useful in LF.

Generalized the eqvt proof for single binders.

With induct instead of induct_tac, just one induction is sufficient.

General alpha_gen_trans for one-variable abstraction.

With unfolding Rep/Abs_eqvt no longer needed.

Lam2 finished apart from Rep_eqvt.

merge

All should be ok now.

repaired according to changes in Abs.thy

added a single-binder alpha equivalence; showed one half of the equivalence proof between general and single binder case

cleaned

updated from huffman

updated from nominal-huffman

Fixed wrong rename.

merge

Lambda based on alpha_gen, under construction.

updated from huffman - repo

renamed Abst/abst to Abs/abs

got rid of RAbst type - is now just pairs

Monotonicity of ~~gen, needed for using it in inductive definitions.

The current state of fv vs supp proofs in LF.

merge

More proofs in the LF example.

merged

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