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.

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