Nominal/Ex/Lambda.thy
2016-03-19 Christian Urban updated to Isabelle 2016 Nominal2-Isabelle2016
2015-07-20 Christian Urban removed junk
2015-07-09 Christian Urban updated for Isabelle 2015
2014-05-19 Christian Urban changed nominal_primrec to nominal_function and termination to nominal_termination
2014-05-19 Christian Urban changed nominal_primrec into the more appropriate nominal_function
2014-04-06 Christian Urban some small additions to examples
2014-03-24 Christian Urban updated to massive changes in Isabelle
2014-03-13 Christian Urban updated to Isabelle changes
2013-06-04 Christian Urban updated to new Isabelle
2013-02-19 Christian Urban updated for 2013 release Nominal2-Isabelle2013
2012-08-07 Christian Urban definition of an auxiliary graph in nominal-primrec definitions
2012-07-15 Christian Urban added a simproc for alpha-equivalence to the simplifier
2012-07-12 Christian Urban streamlined definition of alpha-equivalence for single binders (used flip instead of swap)
2012-06-04 Christian Urban added permutation simplification to the simplifier; this makes the simplifier more powerful, but it potentially loops more often
2012-05-31 Christian Urban added to the simplifier nominal_datatype.fresh lemmas
2012-05-23 Christian Urban improved handling in the simplifier for inequalities derived from freshness assumptions
2012-04-10 Christian Urban updated to latest changes (10 April) to quotient package (lift_raw_const only takes dummy theorem TrueI....in the future this will not work anymore)
2012-03-17 Christian Urban updated to new Isabelle (declared keywords)
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
2011-05-31 Cezary Kaliszyk Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case.
2011-05-31 Cezary Kaliszyk Simple eqvt proofs with perm_simps for clarity
2011-05-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition
2011-05-25 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier
2011-05-14 Christian Urban added a problem with inductive_cases (reported by Randy)
2011-05-03 Christian Urban added two mutual recursive inductive definitions
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
2011-04-18 Christian Urban merged
2011-04-18 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April
2011-04-15 Cezary Kaliszyk New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs.
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2011-02-23 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.
2011-02-01 Cezary Kaliszyk Only one of the subgoals is needed
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases
2011-01-19 Christian Urban defined height as a function that returns an integer
2011-01-18 Christian Urban defined properly substitution
2011-01-18 Christian Urban 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
2011-01-17 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment)
2011-01-17 Christian Urban added a few examples of functions to Lambda.thy
2011-01-17 Christian Urban removed old testing code from Lambda.thy
2011-01-09 Christian Urban solved subgoals for depth and subst function
2011-01-06 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions
2011-01-06 Christian Urban tuned
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-09-29 Christian Urban simplified exhaust proofs
2010-09-29 Christian Urban test with induct_schema for simpler strong_ind proofs
2010-08-29 Christian Urban renamed NewParser to Nominal2
2010-08-27 Christian Urban make copies of the "old" files
2010-08-26 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding)
2010-08-25 Christian Urban cleaned up (almost completely) the examples
2010-08-25 Christian Urban automatic lifting
2010-08-25 Christian Urban now every lemma lifts (even with type variables)
2010-08-25 Christian Urban can now deal with type variables in nominal datatype definitions
2010-08-21 Christian Urban nominal_datatypes with type variables do not work
2010-08-21 Christian Urban changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
2010-06-07 Christian Urban work on transitivity proof
2010-05-21 Cezary Kaliszyk Match_Lam defined on Quotient Level.
less more (0) -120 tip