added multisets to stable branch

added fs and pt for multisets

same as in function_common

qpaper-jv: merge and add to TODOs in the paper and in front.

minor

merged

added FROOT

Use the theorem by Brian, requires new Isabelle.

2 typos found by John Wickerson in QPaper

repaired all slides

tuned make-file

made all papers work again

added a session entry in order to quickly build the heap file (tests took too long)

commented out parts of TypeScheme1 in order to run all tests

updated to Isabelle 16 January

merged

added the simple fixes for the paper

added an FCB for res (will not define evry function, but is a good datapoint)

updated to explicit set type constructor (post Isabelle 3rd January)

proved that generalisation is closed under substitution

added definition for generalisation of type schemes (for paper)

added two eqvt lemmas for fset-operators

separated the two versions of type schemes into two files

added notes by referees to comment about our changes

made the paper running again

included Pi theory in tests

added file by Kirstin

merged

moved TODO into the paper

merged

some slight tuning

the default sort for type-variables in nominal specifications is fs; it is automatically addded

fixed problem with equivariance for beta_star

Reorder constructors to match Lambda

SFT/LambdaTerms: rename 'var' to 'name' to match Lambda.

SFT: Rename Lambda to LambdaTerms, rename constants to match Lambda, remove smt proofs.

Remove transitivity from the definition of One_star and show it instead.

Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.

Add Sigma.thy, an example that defines a sigma-calculus in the style of Peter Homeier's HOL4 formalization.

Update Quotient FIXME-TODO, some issues were already fixed.

Added an initial version of qpaper-jv and a TODO of things to write about.

Remove 'HERE1' and 'HERE3'.

Lift substitution of an Abstraction for BetaCR :)

Tuned renaming

Retry Beta using a reduction relation and its reflexive-symmetric-transitive closure.

Disproved the property described as 'Tzevelakos'.

partially localised the parsing process using functions fron Datatype

updated

updated in stable branch

updated all examples in stable branch

deleted Manual directory in stable branch

cleaned examples for stable branch

cleaned all papers from the stable branch

cleaned Attic in stable branch

backported no_eqvt changeset 1afcbaf4242b

Started Nominal2-Isabelle2011-1 branch and backported changeset 32abaea424bd

Beta: equ and equ2 are not the same relations, equ2 seems not to be beta-eta equality.

updated to lates changes in the datatype package

a bit more on alpha-beta-equated terms

generated the correct thm-list for showing that qfv are equal to support

updated to Isabelle 13 Dec

updated to Isabelle 6 Dec (thanks to Odrej Kuncar)

tiny improvement by removing one unnecessary assumption

deleted old strong_exhaust proof

tuned

silly syntax bug

updated to changes in the quotient package (patch by Ondrej Kuncar)

termination does not automatically prove equivariance for the defined function (label: no_eqvt)

a few more experiments with alpha-beta

used simproc-antiquotation

slides for talk in Leicester

updated to Isabelle 26 Nov

added eqvt-lemma for Image

proved supp for QVar; QApp still fails - probably stronger condistion is needed

added initial test about alpha-beta-equated terms

Add equivariance for alpha_lam_raw and abs_lam.

all examples work again after quotient package has been "de-localised"

updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package

final polishing?

space

spelling

added comments from Andrei

bib

more polishing

added a footnote

some minor polishing

some minor polishing

merged

some polishing

Alternate versions of alpha for finitely supported types on the raw level

merged

changes

deleted PNil

deleted PNil

Load pdfsetup and hyperref last.

Correct BIB entry

updated to Isabelle 19 Sept

more polishing

minor

polished

included comments from Ramana

polished

all material

all material

almost finished

more on paper

more on the paper

more on paper

minor

more on paper

more on paper

more on paper

more on the paper

more

more on paper

more

paper

merged

more on paper

more

more on the paper

more on paper

more on the lmcs paper

updated to Isabelle 28 Aug

Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].

Add lmcs-paper to hgignore

Add 'no-brackets' to avoid '[| |]' in papers.

Comment out examples with 'True' that do not work because function still does not work

Update to new Isabelle

a bit more on the paper

made same changes as in main branch

more on the lmcs paper

a little tuning on the paper

more on the intro and correct style-files

uodated to new Isabelle (15. Aug)

updated for new Isabelle (11. Aug.)

merged

started lmcs paper (isabelle make lmcs)

update to 'termination (eqvt)'.

tuned

completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list

temporary fix

Add an ".hgignore" file

merged

merged

merged

added termination file

preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec

generated the partial eqvt-theorem for functions

added a flag (eqvt) to termination proofs arising fron nominal_primrecs

moved eqvt for Option.map

some tuning

direct definition of height using bn

defined a function directly over a nominal datatype with bn

more one the NBE example

some improvements to the NBE example

slight tuning

use eqvt_at_perm

Remove copy of FCB and cleanup

Experiment with permuting eqvt_at

combinators for local theories and lists

merged

some more experiments with let and bns

some code refactoring

merged

code refactoring; introduced a record for raw_dt_info

more on NBE

more on the NBE function

a little further with NBE

Setup eqvt_at for first goal

attempt for NBE

added some relatively simple examples from paper by Norrish

changed bind to binds in specifications; bind will cause trouble with Monad_Syntax

side commment for future use

made the tests go through again

added another example which seems difficult to define

added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.

merged

all FCB lemmas

exported various FCB-lemmas to a separate file

Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?

Define a version of aux only for same binders. Completeness is fine.

Move If / Let with 'True' to the end of Lambda

merged

tuned

added an example that recurses over two arguments; the interesting proof-obligation is not yet done

Let with a different invariant; not true.

Add non-working Lambda_F_T using FCB2

Added non-working CPS3 using FCB2

Change CPS1 to FCB2

Did the proofs of height and subst for Let with list-like binders. Having apply_assns allows proving things by alpha_bn

side-by-side tests of lets with single assignment; deep-binder case works if the recursion is avoided using an auxiliary function

Exhaust Issue

clarified a sentence

more code refactoring

combined distributed data for alpha in alpha_result (partially done)

moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through

added a warning if a theorem is already declared as equivariant

merged

Prove bn injectivity and experiment more with Let

some experiments

trying new fcb in let/subst

Leftover only inj and eqvt

eapply fcb ok

Removed Inl and Inr

relaxed type in fcb

fcb with explicit bn function

added let-rec example

Experiments with res

proved the fcb also for sets (no restriction yet)

copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom

streamlined the fcb-proof and made fcb1 a special case of fcb

completed proof in Classical; the fcb lemma works for any list of atoms (despite what was written earlier)

fcb for multible (list) binders; at the moment all of them have to have the same sort (at-class); this should also work for set binders, but not yet for restriction.

renamed ds to dset (disagreement set)

added small lemma about disagreement set

merge

New-style fcb for multiple binders.

equality of lst_binder and a few helper lemmas [l]lst. T = [l]lst. S <-> T = S

only one of the fcb precondistions are needed (probably the same with the perm-conditions)

another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy

did all cases, except the multiple binder case

an alternative FCB for Abs_lst1; seems simpler but not as simple as I thought; not sure whether it generalises to multiple binders.

except for the interated binder case, finished definition in Calssical.thy

Make examples work with non-precompiled image

Remove Lambda_add.thy

The examples in Lambda_add can be defined by nominal_function directly

Theory name changes for JEdit

More usual names for substitution properties

Second Fixed Point Theorem

Speed-up the completeness proof.

the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl

added file

expanded the example

fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package

tuned

deleted some dead code

some rudimentary infrastructure for storing data about nominal datatypes

constants with the same names

Quotients/TODO addtion