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

subst also works now

nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions

strengthened renaming lemmas

added eqvt_lemmas for subset and psubset

a few lemmas about freshness for at and at_base

added a property about finite support in the presense of eqvt_at

instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis

solved subgoals for depth and subst function

added eqvt_at premises in function definition - however not proved at the moment

added one further lemma about equivariance of THE_default

equivariance of THE_default under the uniqueness assumption

derived equivariance for the function graph and function relation

a modified function package where, as a test, True has been injected into the compatibility condictions

removed last traces of debugging code

removed debugging code abd introduced a guarded tracing function

moved Weakening up....it does not compile when put at the last position

tuned

added weakening to the test cases

cleaned up weakening proof and added a version with finit sets

same

some further lemmas for fsets

made sure the raw datatypes and raw functions do not get any mixfix syntax

exported the code into a separate file

strong rule inductions; as an example the weakening lemma works