some tuning

naming scheme is now *_fset (not f*_)

more cleaning

further tuning

renamed fminus_raw to diff_list

renamed fcard_raw to card_list

slight update

Further reorganisation and cleaning

further cleaning

typo

FSet: stronger fact in Isabelle.

FSet synchronizing

Synchronizing FSet further.

Partially merging changes from Isabelle

fixed the typo in the abstract and the problem with append (the type of map_k and map_list seems to be indeed incorrect....did not yet look at this)

changed format of the pearl paper

deleted some unused lemmas

major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)

more on the pearl paper

added a section about abstractions

tiny work on the pearl paper

tuned

added apendix to paper detailing one proof

minor

minor

down to 20 pages

minor

down to 21 pages and changed strong induction section

tuned

down to 22 pages

down to 23 pages

down to 24 pages and a bit

llncs and more sqeezing

first part of sqeezing everything into 20 pages (at the moment we have 26)

changed to llncs

merged

minor experiments

merged

simplified exhaust proofs

Made the paper to compile with the renamings.

merged

worked example Foo1 with induct_schema

merged

use also induct_schema for the Let-example (permute_bn is used)

test with induct_schema for simpler strong_ind proofs

substitution definition with 'next_name'.

merged

added Foo1 to explore a contrived example

added postprocessed fresh-lemmas for constructors

post-processed eq_iff and supp threormes according to the fv-supp equality

more consistent naming in Abs.thy

some experiments

added simp rules for prod_fv and prod_alpha

a few more words about Ott

lifted size_thms and exported them as <name>.size

cleaned up two examples

added example about datatypes

updated to Isabelle 22 Sept

removed dead code

fixed

made supp proofs more robust by not using the standard induction; renamed some example files

introduced a general procedure for structural inductions; simplified reflexivity proof

updated to Isabelle Sept 16

updated to Isabelle Sept 13

tuned code

tuned (to conform with indentation policy of Markus)

supp-proofs work except for CoreHaskell and Modules (induct is probably not finding the correct instance)

generated inducts rule by Project_Rule.projections

added the definition supp_rel (support w.r.t. a relation)

merged

got rid of Nominal2_Supp (is now in Nomina2_Base)

moved everything out of Nominal_Supp

renamed alpha_gen -> alpha_set and Abs -> Abs_set etc

moved a proof to Abs

got rid of Nominal_Atoms (folded into Nominal2_Base)

cleaned a bit various thy-files in Nominal-General

adapted paper to changes

made the fv-definition aggree more with alpha (needed in the support proofs)

removed lemma finite_set (already in simpset)

added supp_set lemma

some experiments with support

added eqvt-attribute for permute_abs lemmas

slides of my talk

merge

update qpaper to new isabelle

No need to unfold mem_def with rsp/prs (requires new isabelle).

Anonymize, change Quotient to Quot and fix indentation

renamed NewParser to Nominal2

tuned

updated todos

added fs-instance proofs

added proofs for fsupp properties

fiexed problem with constructors that have no arguments

proved supports lemmas

slight cleaning

updated to new Isabelle

cut out most of the lifting section and cleaned up everything

made all typographic changes

first pass on section 1

make copies of the "old" files

Ball Bex can be lifted after unfolding.

"isabelle make test" makes all major examples....they work up to supp theorems (excluding)

merged

corrected bug with fv-function generation (that was the problem with recursive binders)

minor

cleaned up (almost completely) the examples

cleaning of unused files and code

automatic lifting

everything now lifts as expected

now every lemma lifts (even with type variables)

can now deal with type variables in nominal datatype definitions

updated to new Isabelle

merged

updated to new Isabelle

not needed anymore

moved lifting code from Lift.thy to nominal_dt_quot.ML

nominal_datatypes with type variables do not work

changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default

Clarifications to FIXMEs.

Finished adding remarks from the reviewers.

few remaining remarks as fixme's.

used @{const_name} hopefully everywhere

Intuition behind REL

add missing mathpartir

Add 2 FIXMEs

The type does determine respectfulness, the constant without an instantiated type does not.

Add the SAC stylesheet and updated root file.

TODO

further comments from the referees

fixes for referees

put everything in a "timeit"

improved runtime slightly, by constructing an explicit size measure for the function definitions

more tuning of the code

deleted unused code

improved code

can also lift the various eqvt lemmas for bn, fv, fv_bn and size

also able to lift the bn_defs

added rsp-lemmas for alpha_bns

cezary made the eq_iff lemmas to lift (still needs some infrastructure in quotient)

pinpointed the problem

modified the code for class instantiations (with help from Florian)

defined qperms and qsizes

simplified code

improved code

more experiments with lifting

updated to Isabelle 12th Aug

rsp for constructors

updated to Isabelle 11 Aug

added a function that transforms the helper-rsp lemmas into real rsp lemmas

proved rsp-helper lemmas of size functions

tuning

further simplification with alpha_prove

introduced a general alpha_prove method

equivariance for size

helper lemmas for rsp-lemmas

tests

cleaned up a bit Abs.thy

fixed order of fold_union to make alpha and fv agree

small cleaning

added paper by james; some minor cleaning

samll changes

made compatible

added

updated to new Isabelle; made FSet more "quiet"

merged

minor

minor polishing

quote for a new paper

corrected lambda-preservation theorem

minor

minor things on the paper

merged

minor things

some test with quotient

some minor changes

changes suggested by Peter Homeier

tests

submitted version

more paper

more on the paper

more on the paper

a bit more to the paper

more on the paper

more on slides

slides

more on slides

slides

slides

more on slides

more on slides

added material for slides

fixed

before examples

finished alpha-section

more on the paper

more on the paper

more on the paper

finished fv-section

more on the paper

spell check

more work on the paper

removed an "eqvt"-warning

more quotient-definitions

slight cleaning

fixed according to changes in quotient

added definition of the quotient types

fixed according to changes in quotient

added comment about partial equivalence relations

even further polishing of the qpaper

polished paper again (and took out some claims about Homeier's package)

some slight polishing on the paper

merged cezary's changes

whitespace

Un-do the second change to SingleLet.

merge

Changes for PER and list_all2 committed to Isabelle

changes for partial-equivalence quotient package

deleted compose-lemmas in Abs (not needed anymore)

deleted equivp_hack

proved eqvip theorems for alphas

cleaned up the FSet (noise was introduced by error)

prove that alpha implies alpha_bn (needed for rsp proofs)

further post-submission tuning

merged with main line

merged

also symmetry

merged

premerge

transitivity proofs done

merged

work on transitivity proof

added uminus_eqvt

fixed problem with eqvt proofs

fixed problem with bn_info

merged

equivariance done

smaller code for raw-eqvt proofs

all raw definitions are defined using function

merged

intermediate state

merged

added FSet to the correct paper

added slides

tuned

tuned

alpha works now

started to work on alpha

properly exported bn_descr

hving a working fv-definition without the export

tuned

proper parser for "exclude:"

tuned

moved some mk_union and mk_diff into the library

new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files

some post-submission polishing

added a few points that need to be looked at the next version of the qpaper

eliminated a quot_thm flag

fixed example

small addition to the acknowledgement

qpaper / address FIXMEs.

forgot to save

Fix regularization. Two "FIXME" left in introduction. Minor spellings.

polished everything and submitted

conclusion done

Answer questions in comments

tuned

finished section 4, but put some things I do not understand on comment

4 almost finished

cleaned up definitions

merge

qpaper/Rewrite section5

merged

tuned everytinh up to section 4

Definition of Respects.

conclusion

Qpaper / Clarify the typing system and composition of quotients issue.

Remove only reference to 'equivp'.

merge

qpaper/ackno

tuned

qpaper

qpaper / hol4

qpaper/related work

finished preliminary section

typo

some slight tuning of the preliminary section

merge

qpaper

merged

tuned

Qpaper / beginnig of sec5

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.