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

replaced make_pair with library function HOLogic.mk_prod

removed duplicate eqvt attribute

attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)

merged

tuned

replaced hide by the new hide_const

generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)

added lemmas establishing the support of finite sets of finitely supported elements

added eqvt-lemmas for Bex, Ball and Union

NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.

Merged nominal_datatype into NewParser until eqvts

more parser/new parser synchronization.

Simplify old parser for integration

merge

Change signature of fv and alpha generation.

reorganised eqvt-file (now uses perm_simp already)

qpaper

merge

New Alpha.

Minimal cleaning in LamEx

Remove things moved to the isabelle distribution

Unify and give only one name to 'setify', 'listify' and 'set'

Fixing the definitions in the Parser.

Some of the exceptions that the parser should check in TODO.

Extracting the fv body function and exporting the terms.

Fix for recursive binders.

revert 0c9ef14e9ba4

Support in positive position and atoms in negative positions.

merge

Include support of unknown datatypes in new fv

merged

added basic functions for constructing supp-terms

quotient paper

added missing latex-style file

merged

added stub for quotient paper; call with isabelle make qpaper

Cleaning of Int and FSet Examples

use the more general type-class at_base

deleted left-over code

simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base

use sort at_base instead of at

white spaces

avoided repeated dest of dt_info

tuned

factured out common functionality of prefixing the dt-names with a string

closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy

added some further problemetic tests

some tuning

moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base

merged

Rewrote FV code and included the function package.

merge

Function in Core Haskell

one more pass over the paper

more polishing on the paper

merged

some changes to the paper

rewrote eqvts_raw to be a symtab, that can be looked up

merge ???

infix for In

eliminated command so that all compiles

changed theorem_i to theorem....requires new Isabelle

tuned

tuned and cleaned

tuned and made to compile

added definition of raw-permutations to the new-parser

tuned

slight tuning

added a comment about a function where I am not sure who wrote it.

merged

Minor

Minor cleaning of IntEx

Further cleaning of proofs in FSet

Update term8

Converted 'thm' to a lemma.

Moved working Fset3 properties to FSet.

tuned parser

moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms

tuned proofs

merged

moved some lemmas into the right places

minor

merge

append_rsp2 + isarification

some small changes

merged

deleted the incomplete proof about pairs of abstractions

added a variant of the induction principle for permutations

merge

More about concat

merged

incomplete tests

added an improved version of the induction principle for permutations

Working lifting of concat with inline proofs of second level preservation.

FSet3 cleaning part2

merge

Remove the part already in FSet and leave the experiments

merged

removed a sorry

renamed Ex1.thy to SingleLet.thy

tuning of the code

Reorder FSet

merge

lattice properties.

All lifted in Term4. Requires new isabelle.

fsets are distributive lattices.

Fix of comment

reordered code

renamed "_empty" and "_append" to "_zero" and "_plus"

removed dead code (nominal cannot deal with argument types of constructors that are functions)

added comment about abstraction in raw permuations

optimised the code of define_raw_perm

deleting function perm_arg in favour of the library function mk_perm

merged

tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)

FSet is a semi-lattice

merge

Putting FSet in bot typeclass.

reorder

merged

small updates to the paper; remaining points in PAPER-TODO

sub_list definition and respects

Alternate list_eq and equivalence

Some new lemmas

More cleaning

remove more metis

more metis cleaning

Getting rid of 'metis'.

merge

Remove 'defer'.

merged

tuned proofs

2 more lifted lemmas needed for second representation

Accept non-equality eqvt rules in support proofs.

merge

Locations of files in Parser

merge

minor FSet3 edits.

tuned

moved some general function into nominal_library.ML

tuned; transformation functions now take a context, a thm and return a thm

tuned

equivariance for alpha_raw in CoreHaskell is automatically derived

preliminary parser for perm_simp metod

automatic proofs for equivariance of alphas

Finished proof in Lambda.thy

merged

attempt to manual prove eqvt for alpha

Lifting in Term4.

some tuning of eqvt-infrastructure

some tuning of proofs

typo

merged

half of the pair-abs-equivalence

More on Manual/Trm4

alpha4_equivp and constant lifting.

alpha4_eqvt and alpha4_reflp

fv_eqvt in term4

Updating in Term4.

merge

Prove insert_rsp2

merged

changed header

Minor paper fixes.

temporary fix for CoreHaskell

deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell

merge

Fix the 'subscript' error.

merged

thmdecls can deal with lemmas like alpha_gen which contain pairs or tuples

merge

merge

Separate alpha_definition.

Fix spelling in theory header

Separate define_fv.

tuned and removed dead code

moved a couple of more functions to the library

added a library for basic nominal functions; separated nominal_eqvt file

merged

first working version of the automatic equivariance procedure

Initial cleaning/reorganization in Fv.

merged

preliminary tests

deleted test

merge

merge part: delete_rsp

merge part1: none_memb_nil

added header and more tuning

more tuning

tuned

Working FSet with additional lemmas.

Much more in FSet (currently non-working)

made everything to compile

merged

some small tunings (incompleted work in Lambda.thy)

moved equivariance of map into Nominal2_Eqvt file

early ott paper

Porting lemmas from Quotient package FSet to new FSet.

added alpha-caml paper

implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _

fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _

folded changes from the conference version

added TODO item about parser creating syntax for the wrong type

corrected imports header

tuned

a few tests

added eqvt rules that are more standard

used warning instead of tracing (does not seem to produce stable output)

added small ittems about equivaraince of alpha_gens and name of lam.perm

added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed

changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac

rewrite paragraph introducing equivariance, add citation to Pitts03

edit 'contributions' section so we do not just quote directly from the reviewer

renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper

clarified comment about distinct lists in th efuture work section

tuned type-schemes example

updated (comment about weirdo example)

check whether the "weirdo" example from the binding bestiary works with shallow binders

properly separated the example from my PhD and gave the correct alpha-equivalence relation (according to the paper)

merged