Nominal/Ex/Lambda.thy
2011-12-21 Cezary Kaliszyk Port CR_Takahashi from Nominal1, no more "sorry" in BetaCR.
2011-12-17 Christian Urban cleaned examples for stable branch Nominal2-Isabelle2011-1
2011-12-15 Christian Urban updated to lates changes in the datatype package
2011-11-08 Cezary Kaliszyk Add equivariance for alpha_lam_raw and abs_lam.
2011-11-07 Christian Urban all examples work again after quotient package has been "de-localised"
2011-08-19 Cezary Kaliszyk Comment out examples with 'True' that do not work because function still does not work
2011-07-22 Christian Urban completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list
2011-07-19 Christian Urban preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec
2011-07-19 Christian Urban generated the partial eqvt-theorem for functions
2011-07-18 Christian Urban added a flag (eqvt) to termination proofs arising fron nominal_primrecs
2011-07-18 Christian Urban moved eqvt for Option.map
2011-07-05 Christian Urban added some relatively simple examples from paper by Norrish
2011-07-05 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
2011-07-05 Christian Urban made the tests go through again
2011-07-05 Christian Urban merged
2011-07-05 Christian Urban exported various FCB-lemmas to a separate file
2011-07-05 Cezary Kaliszyk Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind?
2011-07-05 Cezary Kaliszyk Define a version of aux only for same binders. Completeness is fine.
2011-07-05 Cezary Kaliszyk Move If / Let with 'True' to the end of Lambda
2011-07-04 Christian Urban added an example that recurses over two arguments; the interesting proof-obligation is not yet done
2011-06-27 Christian Urban copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom
2011-06-26 Christian Urban another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy
2011-06-23 Christian Urban the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl
2011-06-22 Christian Urban some rudimentary infrastructure for storing data about nominal datatypes
2011-06-16 Christian Urban got rid of the boolean flag in the raw_equivariance function
2011-06-16 Christian Urban added a test that every function must be of pt-sort
2011-06-15 Christian Urban added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method
2011-06-15 Cezary Kaliszyk Some TODOs
2011-06-10 Cezary Kaliszyk Move working examples before non-working ones
2011-06-10 Cezary Kaliszyk Optimized proofs and removed some garbage.
2011-06-10 Cezary Kaliszyk Slightly modify fcb for list1 and put in common place.
2011-06-09 Cezary Kaliszyk Eval can be defined with additional freshness
2011-06-09 Cezary Kaliszyk Minor simplification
2011-06-08 Christian Urban merged
2011-06-08 Christian Urban merged
2011-06-07 Cezary Kaliszyk Simplify ln-trans proof
2011-06-07 Cezary Kaliszyk cbvs can be easily defined without an invariant
2011-06-07 Christian Urban defined the "count-bound-variables-occurences" function which has an accumulator like trans
2011-06-07 Christian Urban merged
2011-06-07 Cezary Kaliszyk remove garbage (proofs that assumes the invariant outside function)
2011-06-07 Cezary Kaliszyk Proof of trans with invariant
2011-06-07 Christian Urban cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
2011-06-07 Christian Urban 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
2011-06-05 Christian Urban added an option for an invariant (at the moment only a stub)
2011-06-04 Cezary Kaliszyk Finish and test the locale approach
2011-06-03 Christian Urban recursion combinator inside a locale
2011-06-02 Cezary Kaliszyk finished the missing obligations
2011-06-02 Christian Urban merged
2011-06-02 Christian Urban a test with a recursion combinator defined on top of nominal_primrec
2011-06-02 Cezary Kaliszyk Use FCB to simplify proof
2011-06-01 Christian Urban hopefully final fix for ho-functions
2011-06-01 Christian Urban first test to fix the problem with free variables
2011-06-01 Cezary Kaliszyk DB translation using index; easier to reason about.
2011-06-01 Cezary Kaliszyk Problem: free variables in the goal
2011-06-01 Cezary Kaliszyk fixed previous commit
2011-06-01 Cezary Kaliszyk equivariance of db_trans
2011-05-31 Christian Urban fixed the problem with cps-like functions
2011-05-31 Cezary Kaliszyk DeBruijn translation in a simplifier friendly way
2011-05-31 Cezary Kaliszyk map_term can be defined when equivariance is assumed
2011-05-31 Cezary Kaliszyk map_term is not a function the way it is defined
less more (0) -100 -60 tip