simple cases for strong inducts done; infrastructure for the difficult ones is there

added theorem-rewriter conversion

freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)

created strong_exhausts terms

moved setify and listify functions into the library; introduced versions that have a type argument

updated

a bit more tuning of the paper

brought the paper to 20 pages plus one page appendix

first tests about exhaust

moved some code into the nominal_library

moved definition of raw bn-functions into nominal_dt_rawfuns

kept the nested structure of constructors (belonging to one datatype)

moved general theorems into the libraries

automated permute_bn theorems

updated to changes in Isabelle

deleted nominal_dt_supp.ML

moved code from nominal_dt_supp to nominal_dt_quot

automated alpha_perm_bn theorems

ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof

updated to Isabelle 2nd December

isarfied some of the high-level proofs

added abs_rename_res lemma

completed proofs in Foo2

completed the strong exhausts rules for Foo2 using general lemmas

tuned proof to reduce number of warnings

disabled the Foo examples, because of heavy work

slightly simplified the Foo2 tests and hint at a general lemma

completely different method fro deriving the exhaust lemma

merged

merged

added example from the F-ing paper by Rossberg, Russo and Dreyer

implemented concrete suggestion of 3rd reviewer

missing freshness assumptions

foo2 strong induction

foo2 full exhausts

Foo2 strong_exhaust for first variable.

single rename in let2

current isabelle

added example Foo2.thy

tuned example

proved that bn functions return a finite set

added a test for the various shallow binders

fixed bug in fv function where a shallow binder binds lists of names

merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy

deleted special Nominal2_FSet theory

moved rest of the lemmas from Nominal2_FSet to the TypeScheme example

moved most material fron Nominal2_FSet into the Nominal_Base theory

tuned example

lifted permute_bn simp rules

lifted permute_bn constants

respectfulness for permute_bn functions

automated permute_bn functions (raw ones first)

adapted to changes by Florian on the quotient package and removed local fix for function package

expanded the paper by uncommenting the comments and adding the appendix

fixed locally the problem with the function package; all tests work again

added a test about subtyping; disabled two tests, because of problem with function package

small typo

squeezed qpaper to 6 pages

Qpaper / Move examples to commented out appendix

Unanonymize qpaper

FSet changes for Qpaper

Remove FSet and use the one from Isabelle

took out comment about map-types / adapted to recent changes

use definitions instead of functions

tuned

used functions instead of definitions

added missing style file

Use the generalized compositional quotient theorem

fixed typo

all tests work again

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