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