merge

qpaper/unfold the ball_reg_right statement

merged

some tuning and start work on section 4

qpaper

qpaper / INJ

qpaper / REG

qpaper / minor

qpaper/various

qpaper

qpaper/more on example

qpaper/examples

completed proof and started section about respectfulness and preservation

more on the qpaper

tuned

more on the constant lifting section

something about the quotient ype definitions

added some examples

improved definition of ABS and REP

qpaper.

some spelling

minor

qpaper / tuning in preservation and general display

polishing of ABS/REP

some slight tuning of the intro

Fix integer relation.

completed the intro (except minor things)

more intro

more on the qpaper

even more on the qpaper (intro almost done)

more to the introduction of the qpaper

adapted to the official sigplan style file (this gives us more space)

added to the popl-paper a pointer to work by Altenkirch

more on the qpaper

new title for POPL paper

more work on intro and abstract (done for today)

a bit more in the introduction and abstract

improved abstract, some tuning

Qpaper / minor on cleaning

qpaper / injection proof.

qpaper / example interaction

Qpaper/regularization proof.

qpaper

Qpaper/more.

Qpaper/Minor

added larry's quote

added larry's paper

tuned

first version of the abstract

merged

fixed bug where perm_simp 'forgets' how to prove equivariance for the empty set

qpaper / lemmas used in proofs

qpaper / injection statement

qpaper / regularize

qpaper / a bit about prs

Functionalized the ABS/REP definition.

qpaper / lifting introduction

merged

fixed compile error

qpaper / composition of quotients.

qpaper

qpaper..

qpaper.

Name some respectfullness

added FSet to the correct paper

merged

added FSet

qpaper

qpaper

Substitution Lemma for TypeSchemes.

Simplified the proof

A lemma about substitution in TypeSchemes.

reversing the direction of fresh_star

overlapping deep binders proof

edits from the reviewers

tuned paper

changed qpaper to lncs-style

Match_Lam defined on Quotient Level.

More on Function-defined subst.

Isabelle renamings

merge

Renamings.

Renamings

merge (non-trival)

Previously uncommited direct subst definition changes.

Function experiments

merged

added comments about pottiers work

more subst experiments

More subst experminets

more on subst

Single variable substitution

subst fix

subst experiments

soem minor tuning

Fix broken add

add missing .bib

merge

starting bibliography

merged

updated to new Isabelle (More_Conv -> Conv)

made this example to work again

merge

alpha_alphabn for bindings in a type under bn.

minor tuning

Ex4 does work, and I don't see the difference between the alphas.

slight tuning

somewhat simplified the main parsing function; failed to move a Note-statement to define_raw_perms

moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat

tuned paper

tuned paper

tuned a bit the paper

started a new file for the parser to make some experiments

moved old parser and fv into attic

polished example

merged

tuned a bit the paper

Proper fv/alpha for multiple compound binders

SingleLetFoo with everything.

Fv for multiple binding functions

added a more instructive example - has some problems with fv though

added flip_eqvt and swap_eqvt to the equivariance lists

tuned the paper

properly declared outer keyword

added an example which goes outside our current speciifcation

made out of STEPS a configuration value so that it can be set individually in each file

tuned eqvt-proofs about prod_rel and prod_fv

removed internal functions from the signature (they are not needed anymore)

added term4 back to the examples

Make Term4 use 'equivariance'.

fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy

merged

moved the data-transformation into the parser

added a test whether some of the constants already equivariant (then the procedure has to fail).

include set_simps and append_simps in fv_rsp

Move alpha_eqvt to unused.

Use equivariance instead of alpha_eqvt

merge

merge

fvbv_rsp include prod_rel.simps

better ML-interface (returning only a list of theorems and a context)

merge

Use raw_induct instead of induct

ingnored parameters in equivariance; added a proper interface to be called from ML

properly exported defined bn-functions

Include raw permutation definitions in eqvt

Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'

a bit for the introduction of the q-paper

added some of the quotient literature; a bit more to the qpaper

fixed a problem with non-existant alphas2

added comment about bind_set

fixing bind_set problem

merge

Term8 comment

merge

Restore set bindings in CoreHaskell

Recursive examples with relation composition

merge

prod_rel and prod_fv eqvt and mono

ExLetRec

merge

Parser changes for compound relations

merge

Use mk_compound_fv' and mk_compound_rel'

merge

Membership in a pair of lists.

Synchronize FSet with repository

tuned file names for examples

cleaned up a bit the examples; added equivariance to all examples

fixed the problem with alpha containing splits

added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied

Manually added some newer keywords from the distribution

Regularize experiments

alpha_eqvt_tac with prod_rel and prod_fv simps

mem => member

merge

Fixes for new Isabelle

compound versions with prod_rel and prod_fun, not made default yet.

prod_rel and prod_fv simps

mem => member

prod_rel.simps and Fixed for new isabelle

Fixes for new isabelle

prod_fv and its respectfullness and preservation.

Experiments with equivariance.

merged

a bit mor on the pearl journal paper

solved the problem with equivariance by first eta-normalising the goal

Some cleaning in Term4

"isabelle make" compiles all examples with newparser/newfv/newalpha only.

Move Term4 to NewParser

Fix Term4 for permutation signature change

Move LF to NewParser. Just works.

merge

ExLetMult

Ex1Rec.

merge

merge

ExPS3 in NewParser

Move ExPS8 to new parser.

Fix for new isabelle

merge

Minor

increased step counter so that all steps go through

fixed my error with define_raw_fv

tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function

Separate Term8, as it may work soon.

moved CoreHaskell to NewParser.

ExPS7 in NewParser

Move ExLeroy to New Parser

Move 2 more to NewParser

Move TypeSchemes to NewParser

Move ExLet to NewParser.

tuned

roll back of the last commit (there was a difference)

tuned

to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm

merged

some preliminary changes to the pearl-jv paper

some preliminary notes of the abstract (qpaper); still need to see the motivating example

Added cheats to classical

Ex2 moved to new parser.

alpha_eqvt_tac fixed to work when the existential is not at the top level.

SingleLet and Ex3 work with NewParser.

Comment

Another example where only alpha_eqvt fails.

Register only non-looping rules in eq_iff

Equivariance fails for single let?

NewParser

Introduce eq_iff_simp to match the one from Parser.

remove tracing

Cheat support equations in new parser

Remove dependency on NewFv

Fix Parser

Add explicit cheats in NewParser and comment out the examples for outside use.

Fix Datatype_Aux calls in NewParser.

Move old fv_alpha_export to Fv.

moved old parser and old fv back into their original places; isabelle make works again

slight tuning

simplified the supp-of-finite-sets proof

tried to add some comments in the huge(!) nominal2_cmd function