function for let-rec

TODO/minor

Move lst_fcb to Nominal2_Abs

More minor TODOs

Update TODO

Let/minor

Update Quotient/TODO and remove some attic code

merge

little on cps2

got rid of the boolean flag in the raw_equivariance function

Fix

merge

CPS3 can be defined with eqvt_rhs.

moved for the moment CPS translations into the example directory

merged

added eqvt_at and invariant for boths sides of the equations

Added the CPS translation experiments. CPS1 comes with all the proofs, CPS2,3 just have the function and need eqvt_rhs to finish the obligations.

added a test that every function must be of pt-sort

all tests work again

added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method

added an abstract

added a stub for function paper; "isabelle make fnpaper"

merge

one TODO and one Problem?

merge

Some TODOs

merge

TypeSchemes work with 'default'.

tuned some proofs

fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough

tuned

Move working examples before non-working ones

Optimized proofs and removed some garbage.

merge

Slightly modify fcb for list1 and put in common place.

Experiments with Let

Eval can be defined with additional freshness

Minor simplification

abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.

More experiments with 'default'

Finished the proof with the invariant

Issue with 'default'

merged

merged

using the option "default" the function package allows one to give an explicit default value

Simpler proof of TypeSchemes/substs

Simplify fcb_res

FCB for res binding and simplified proof of subst for type schemes

Simplify ln-trans proof

cbvs can be easily defined without an invariant

defined the "count-bound-variables-occurences" function which has an accumulator like trans

merged

remove garbage (proofs that assumes the invariant outside function)

Proof of trans with invariant

Testing invariant in Lambda_F_T

cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file

fixed problem with earlier commit about nominal_function_common; added facility for specifying an invariant - added a definition of frees_set which need a finiteness invariant

slightly stronger property in fundef_ex_prop

added an option for an invariant (at the moment only a stub)

added a more general lemma fro fundef_ex1

Trying the induction on the graph

Finish and test the locale approach

FiniteSupp precondition in the function is enough to get rid of completeness obligationss

recursion combinator inside a locale

merge

F for lambda used to define translation to locally nameless

typo

removed dead code

finished the missing obligations

merged

a test with a recursion combinator defined on top of nominal_primrec

Use FCB to simplify proof

merge

Remove SMT

hopefully final fix for ho-functions

first test to fix the problem with free variables

proved subst for All constructor in type schemes.

DB translation using index; easier to reason about.

Problem: free variables in the goal

fixed previous commit

equivariance of db_trans

fixed the problem with cps-like functions

DeBruijn translation in a simplifier friendly way

map_term can be defined when equivariance is assumed

map_term is not a function the way it is defined

Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.

Simple eqvt proofs with perm_simps for clarity

tuned last commit

functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition

updated to new Isabelle

added eq_iff and distinct lemmas of nominal datatypes to the simplifier

more on slides

added slides for copenhagen

added a problem with inductive_cases (reported by Randy)

misc

made the subtyping work again

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