updated to new Isabelle (> 9 May)

merged

added two mutual recursive inductive definitions

deleted two functions from the API

proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)

more on pearl-paper

more on pearl-paper

updated Quotient paper so that it compiles again

merged

added slides for beijing

more to the pearl paper

updated to snapshot Isabelle 19 April

merged

added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April

New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.

merged

introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive

shanghai slides

pictures for slides

Shanghai slides

more paper

eqvt of supp and fresh is proved using equivariance infrastructure

more paper

more on the paper

tuned paper

tuned paper

typo

more on paper

eqvt_lambda without eta-expansion

changed default preprocessor that does not catch variables only occuring on the right

final version of slides

more on the slides

tuned IsaMakefile

rearranged directories and updated to new Isabelle

precise path to LaTeXsugar

a lit bit more on the pearl-jv paper

ported changes from function package....needs Isabelle 16 March or above

more on the pearl paper

equivariance for All and Ex can be proved in terms of their definition

more on the paper

merged

more on the pearl paper

distinct names at toplevel

merge

Pairing function

updated pearl papers

a bit more tuning

included old test cases for perm_simp into ROOT.ML file

split the library into a basics file; merged Nominal_Eqvt into Nominal_Base

some slight polishing

merged

added a lemma about fresh_star and Abs

Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.

typeschemes/subst

further experiments with typeschemes subst

Finished the proof of a function that invents fresh variable names.

added eqvt for length

added eqvt lemmas for filter and distinct

added eqvt for cartesian products

cleaned up the experiments so that the tests go through

merge

Experiments defining a function on Let

updated TODO

Lambda.thy which works with Nominal_Isabelle2011

merged

removed diagnostic code

Only one of the subgoals is needed

Experiments with substitution on set+

More properties that relate abs_res and abs_set. Also abs_res with less binders.

alpha_res implies alpha_set :)

Showing that the binders difference is fresh for the left side solves the goal for 'set'.

Experiments with functions

some experiments

the proofs with eqvt_at

made eqvt-proof explicit in the function definitions

merge

minor

Down as infixr

added some slides

added Tutorial6

cleaning up

merged

cleaned up Tutorial 3 with solutions

Missing val.simps

merge

Tutorial 4s

cleaned up and solution section

cleaned up tutorial1...added solution file

better version of Tutorial 1

better flow of proofs and definitions and proof

separated type preservation and progress into a separate file

substitution lemma in separate file

added unbind example

a bit tuning

first split of tutorrial theory

added a very rough version of the tutorial; all seems to work

added obtain_fresh lemma; tuned Lambda.thy

base file for the tutorial (contains definitions for heigt, subst and beta-reduction)

ported some of the old proofs to serve as testcases

added eqvt and supp lemma for removeAll (function from List.thy)

theory name as it should be

removed diagnostic code

added Minimal file to test things

defined height as a function that returns an integer

deleted diagnostic code

some tryes about substitution over type-schemes

defined properly substitution

derived stronger Abs_eq_iff2 theorems

made alpha_abs_set_stronger1 stronger

removed finiteness assumption from set_rename_perm

alpha_abs_set_stronger1

alpha_abs_let_stronger is not true in the same form

the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions

modified the renaming_perm lemmas

added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)

added a few examples of functions to Lambda.thy

exported nominal function code to external file

removed old testing code from Lambda.thy

moved high level code from LamTest into the main libraries.

eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation