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

final version of the ESOP paper; used set+ instead of res as requested by one reviewer

file with most of the strong rule induction development

simple cases for string rule inductions

changed res keyword to set+ for restrictions; comment by a referee

added proper case names for all induct and exhaust theorems

added small example for strong inductions; functions still need a sorry

removed local fix for bug in induction_schema; added setup method for strong inductions

automated all strong induction lemmas

proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML

generated goals for strong induction theorems.

test with strong inductions

moved all strong_exhaust code to nominal_dt_quot; tuned examples

moved generic functions into nominal_library

slight tuning

slight tuning

tuned examples

added fold_right which produces the correct term for left-infix operators

updated to Isabelle 22 December

a bit tuning

corrected premises of strong exhausts theorems

properly exported strong exhaust theorem; cleaned up some examples

all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code

one interesting case done

a stronger statement for at_set_avoiding

tuned

tuned

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