Mercurial Mercurial > hg > nominal2 / shortlog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -1000 -224 +224 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
 
2011-06-23 Christian Urban added file changeset | files
2011-06-23 Christian Urban expanded the example changeset | files
2011-06-23 Christian Urban fixed nasty bug with type variables in nominal_datatypes; this included to be careful with the output of the inductive and function package changeset | files
2011-06-22 Christian Urban tuned changeset | files
2011-06-22 Christian Urban deleted some dead code changeset | files
2011-06-22 Christian Urban some rudimentary infrastructure for storing data about nominal datatypes changeset | files
2011-06-22 Cezary Kaliszyk constants with the same names changeset | files
2011-06-21 Cezary Kaliszyk Quotients/TODO addtion changeset | files
2011-06-21 Cezary Kaliszyk Minor changeset | files
2011-06-21 Cezary Kaliszyk merge changeset | files
2011-06-21 Cezary Kaliszyk spelling changeset | files
2011-06-20 Cezary Kaliszyk merge changeset | files
2011-06-20 Cezary Kaliszyk Abs_set_fcb changeset | files
2011-06-20 Cezary Kaliszyk function for let-rec changeset | files
2011-06-20 Cezary Kaliszyk TODO/minor changeset | files
2011-06-20 Cezary Kaliszyk Move lst_fcb to Nominal2_Abs changeset | files
2011-06-20 Cezary Kaliszyk More minor TODOs changeset | files
2011-06-20 Cezary Kaliszyk Update TODO changeset | files
2011-06-20 Cezary Kaliszyk Let/minor changeset | files
2011-06-19 Cezary Kaliszyk Update Quotient/TODO and remove some attic code changeset | files
2011-06-19 Cezary Kaliszyk merge changeset | files
2011-06-19 Cezary Kaliszyk little on cps2 changeset | files
2011-06-16 Christian Urban got rid of the boolean flag in the raw_equivariance function changeset | files
2011-06-16 Cezary Kaliszyk Fix changeset | files
2011-06-16 Cezary Kaliszyk merge changeset | files
2011-06-16 Cezary Kaliszyk CPS3 can be defined with eqvt_rhs. changeset | files
2011-06-16 Christian Urban moved for the moment CPS translations into the example directory changeset | files
2011-06-16 Christian Urban merged changeset | files
2011-06-16 Christian Urban added eqvt_at and invariant for boths sides of the equations changeset | files
2011-06-16 Cezary Kaliszyk 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. changeset | files
2011-06-16 Christian Urban added a test that every function must be of pt-sort changeset | files
2011-06-16 Christian Urban all tests work again changeset | files
2011-06-15 Christian Urban added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method changeset | files
2011-06-15 Christian Urban added an abstract changeset | files
2011-06-15 Christian Urban added a stub for function paper; "isabelle make fnpaper" changeset | files
2011-06-15 Cezary Kaliszyk merge changeset | files
2011-06-15 Cezary Kaliszyk one TODO and one Problem? changeset | files
2011-06-15 Cezary Kaliszyk merge changeset | files
2011-06-15 Cezary Kaliszyk Some TODOs changeset | files
2011-06-15 Cezary Kaliszyk merge changeset | files
2011-06-15 Cezary Kaliszyk TypeSchemes work with 'default'. changeset | files
2011-06-14 Christian Urban tuned some proofs changeset | files
2011-06-14 Christian Urban fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough changeset | files
2011-06-14 Christian Urban tuned changeset | files
2011-06-10 Cezary Kaliszyk Move working examples before non-working ones changeset | files
2011-06-10 Cezary Kaliszyk Optimized proofs and removed some garbage. changeset | files
2011-06-10 Cezary Kaliszyk merge changeset | files
2011-06-10 Cezary Kaliszyk Slightly modify fcb for list1 and put in common place. changeset | files
2011-06-10 Cezary Kaliszyk Experiments with Let changeset | files
2011-06-09 Cezary Kaliszyk Eval can be defined with additional freshness changeset | files
2011-06-09 Cezary Kaliszyk Minor simplification changeset | files
2011-06-09 Cezary Kaliszyk abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'. changeset | files
2011-06-09 Cezary Kaliszyk More experiments with 'default' changeset | files
2011-06-08 Cezary Kaliszyk Finished the proof with the invariant changeset | files
2011-06-08 Cezary Kaliszyk Issue with 'default' changeset | files
2011-06-08 Christian Urban merged changeset | files
2011-06-08 Christian Urban merged changeset | files
2011-06-08 Christian Urban using the option "default" the function package allows one to give an explicit default value changeset | files
2011-06-08 Cezary Kaliszyk Simpler proof of TypeSchemes/substs changeset | files
2011-06-08 Cezary Kaliszyk Simplify fcb_res changeset | files
2011-06-08 Cezary Kaliszyk FCB for res binding and simplified proof of subst for type schemes changeset | files
2011-06-07 Cezary Kaliszyk Simplify ln-trans proof changeset | files
2011-06-07 Cezary Kaliszyk cbvs can be easily defined without an invariant changeset | files
2011-06-07 Christian Urban defined the "count-bound-variables-occurences" function which has an accumulator like trans changeset | files
2011-06-07 Christian Urban merged changeset | files
2011-06-07 Cezary Kaliszyk remove garbage (proofs that assumes the invariant outside function) changeset | files
2011-06-07 Cezary Kaliszyk Proof of trans with invariant changeset | files
2011-06-07 Cezary Kaliszyk Testing invariant in Lambda_F_T changeset | files
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 changeset | files
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 changeset | files
2011-06-06 Christian Urban slightly stronger property in fundef_ex_prop changeset | files
2011-06-05 Christian Urban added an option for an invariant (at the moment only a stub) changeset | files
2011-06-05 Christian Urban added a more general lemma fro fundef_ex1 changeset | files
2011-06-04 Cezary Kaliszyk Trying the induction on the graph changeset | files
2011-06-04 Cezary Kaliszyk Finish and test the locale approach changeset | files
2011-06-03 Cezary Kaliszyk FiniteSupp precondition in the function is enough to get rid of completeness obligationss changeset | files
2011-06-03 Christian Urban recursion combinator inside a locale changeset | files
2011-06-03 Cezary Kaliszyk merge changeset | files
2011-06-03 Cezary Kaliszyk F for lambda used to define translation to locally nameless changeset | files
2011-06-02 Christian Urban typo changeset | files
2011-06-02 Christian Urban removed dead code changeset | files
2011-06-02 Cezary Kaliszyk finished the missing obligations changeset | files
2011-06-02 Christian Urban merged changeset | files
2011-06-02 Christian Urban a test with a recursion combinator defined on top of nominal_primrec changeset | files
2011-06-02 Cezary Kaliszyk Use FCB to simplify proof changeset | files
2011-06-02 Cezary Kaliszyk merge changeset | files
2011-06-02 Cezary Kaliszyk Remove SMT changeset | files
2011-06-01 Christian Urban hopefully final fix for ho-functions changeset | files
2011-06-01 Christian Urban first test to fix the problem with free variables changeset | files
2011-06-01 Cezary Kaliszyk proved subst for All constructor in type schemes. changeset | files
2011-06-01 Cezary Kaliszyk DB translation using index; easier to reason about. changeset | files
2011-06-01 Cezary Kaliszyk Problem: free variables in the goal changeset | files
2011-06-01 Cezary Kaliszyk fixed previous commit changeset | files
2011-06-01 Cezary Kaliszyk equivariance of db_trans changeset | files
2011-05-31 Christian Urban fixed the problem with cps-like functions changeset | files
2011-05-31 Cezary Kaliszyk DeBruijn translation in a simplifier friendly way changeset | files
2011-05-31 Cezary Kaliszyk map_term can be defined when equivariance is assumed changeset | files
2011-05-31 Cezary Kaliszyk map_term is not a function the way it is defined changeset | files
2011-05-31 Cezary Kaliszyk Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case. changeset | files
2011-05-31 Cezary Kaliszyk Simple eqvt proofs with perm_simps for clarity changeset | files
2011-05-30 Christian Urban tuned last commit changeset | files
2011-05-30 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition changeset | files
2011-05-26 Christian Urban updated to new Isabelle changeset | files
2011-05-25 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier changeset | files
2011-05-24 Christian Urban more on slides changeset | files
2011-05-22 Christian Urban added slides for copenhagen changeset | files
2011-05-14 Christian Urban added a problem with inductive_cases (reported by Randy) changeset | files
2011-05-13 Christian Urban misc changeset | files
2011-05-10 Christian Urban made the subtyping work again changeset | files
2011-05-10 Christian Urban updated to new Isabelle (> 9 May) changeset | files
2011-05-09 Christian Urban merged changeset | files
2011-05-03 Christian Urban added two mutual recursive inductive definitions changeset | files
2011-05-03 Christian Urban deleted two functions from the API changeset | files
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) changeset | files
2011-05-09 Christian Urban more on pearl-paper changeset | files
2011-05-04 Christian Urban more on pearl-paper changeset | files
2011-05-02 Christian Urban updated Quotient paper so that it compiles again changeset | files
2011-04-28 Christian Urban merged changeset | files
2011-04-28 Christian Urban added slides for beijing changeset | files
2011-04-21 Christian Urban more to the pearl paper changeset | files
2011-04-19 Christian Urban updated to snapshot Isabelle 19 April changeset | files
2011-04-18 Christian Urban merged changeset | files
2011-04-18 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April changeset | files
2011-04-15 Cezary Kaliszyk New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs. changeset | files
2011-04-13 Christian Urban merged changeset | files
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive changeset | files
2011-04-12 Christian Urban shanghai slides changeset | files
2011-04-11 Christian Urban pictures for slides changeset | files
2011-04-11 Christian Urban Shanghai slides changeset | files
2011-04-10 Christian Urban more paper changeset | files
2011-04-09 Christian Urban eqvt of supp and fresh is proved using equivariance infrastructure changeset | files
2011-04-09 Christian Urban more paper changeset | files
2011-04-09 Christian Urban more on the paper changeset | files
2011-04-08 Christian Urban tuned paper changeset | files
2011-04-08 Christian Urban tuned paper changeset | files
2011-04-08 Christian Urban typo changeset | files
2011-04-08 Christian Urban more on paper changeset | files
2011-04-07 Christian Urban eqvt_lambda without eta-expansion changeset | files
2011-04-06 Christian Urban changed default preprocessor that does not catch variables only occuring on the right changeset | files
2011-03-31 Christian Urban final version of slides changeset | files
2011-03-30 Christian Urban more on the slides changeset | files
2011-03-30 Christian Urban tuned IsaMakefile changeset | files
2011-03-29 Christian Urban rearranged directories and updated to new Isabelle changeset | files
2011-03-16 Christian Urban precise path to LaTeXsugar changeset | files
2011-03-16 Christian Urban a lit bit more on the pearl-jv paper changeset | files
2011-03-16 Christian Urban ported changes from function package....needs Isabelle 16 March or above changeset | files
2011-03-14 Christian Urban more on the pearl paper changeset | files
2011-03-14 Christian Urban equivariance for All and Ex can be proved in terms of their definition changeset | files
2011-03-11 Christian Urban more on the paper changeset | files
2011-03-08 Christian Urban merged changeset | files
2011-03-08 Christian Urban more on the pearl paper changeset | files
2011-03-02 Cezary Kaliszyk distinct names at toplevel changeset | files
2011-03-02 Cezary Kaliszyk merge changeset | files
2011-03-02 Cezary Kaliszyk Pairing function changeset | files
2011-03-02 Christian Urban updated pearl papers changeset | files
2011-03-01 Christian Urban a bit more tuning changeset | files
2011-02-28 Christian Urban included old test cases for perm_simp into ROOT.ML file changeset | files
2011-02-28 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base changeset | files
2011-02-25 Christian Urban some slight polishing changeset | files
2011-02-24 Christian Urban merged changeset | files
2011-02-24 Christian Urban added a lemma about fresh_star and Abs changeset | files
2011-02-23 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules. changeset | files
2011-02-19 Cezary Kaliszyk typeschemes/subst changeset | files
2011-02-17 Cezary Kaliszyk further experiments with typeschemes subst changeset | files
2011-02-17 Cezary Kaliszyk Finished the proof of a function that invents fresh variable names. changeset | files
2011-02-16 Christian Urban added eqvt for length changeset | files
2011-02-16 Christian Urban added eqvt lemmas for filter and distinct changeset | files
2011-02-07 Christian Urban added eqvt for cartesian products changeset | files
2011-02-07 Christian Urban cleaned up the experiments so that the tests go through changeset | files
2011-02-04 Cezary Kaliszyk merge changeset | files
2011-02-04 Cezary Kaliszyk Experiments defining a function on Let changeset | files
2011-02-04 Christian Urban updated TODO changeset | files
2011-02-04 Christian Urban Lambda.thy which works with Nominal_Isabelle2011 changeset | files
2011-02-03 Christian Urban merged changeset | files
2011-02-03 Christian Urban removed diagnostic code changeset | files
2011-02-01 Cezary Kaliszyk Only one of the subgoals is needed changeset | files
2011-01-31 Cezary Kaliszyk Experiments with substitution on set+ changeset | files
2011-01-31 Cezary Kaliszyk More properties that relate abs_res and abs_set. Also abs_res with less binders. changeset | files
2011-01-30 Cezary Kaliszyk alpha_res implies alpha_set :) changeset | files
2011-01-30 Cezary Kaliszyk Showing that the binders difference is fresh for the left side solves the goal for 'set'. changeset | files
2011-01-29 Cezary Kaliszyk Experiments with functions changeset | files
2011-01-27 Christian Urban some experiments changeset | files
2011-01-27 Christian Urban the proofs with eqvt_at changeset | files
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions changeset | files
2011-01-24 Cezary Kaliszyk merge changeset | files
2011-01-24 Cezary Kaliszyk minor changeset | files
2011-01-24 Cezary Kaliszyk Down as infixr changeset | files
2011-01-23 Christian Urban added some slides changeset | files
2011-01-23 Christian Urban added Tutorial6 changeset | files
2011-01-23 Christian Urban cleaning up changeset | files
2011-01-22 Christian Urban merged changeset | files
2011-01-22 Christian Urban cleaned up Tutorial 3 with solutions changeset | files
2011-01-22 Cezary Kaliszyk Missing val.simps changeset | files
2011-01-22 Cezary Kaliszyk merge changeset | files
2011-01-22 Cezary Kaliszyk Tutorial 4s changeset | files
2011-01-22 Christian Urban cleaned up and solution section changeset | files
2011-01-22 Christian Urban cleaned up tutorial1...added solution file changeset | files
2011-01-22 Christian Urban better version of Tutorial 1 changeset | files
2011-01-21 Christian Urban better flow of proofs and definitions and proof changeset | files
2011-01-21 Christian Urban separated type preservation and progress into a separate file changeset | files
2011-01-21 Christian Urban substitution lemma in separate file changeset | files
2011-01-21 Christian Urban added unbind example changeset | files
2011-01-20 Christian Urban a bit tuning changeset | files
2011-01-20 Christian Urban first split of tutorrial theory changeset | files
2011-01-19 Christian Urban added a very rough version of the tutorial; all seems to work changeset | files
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy changeset | files
2011-01-19 Christian Urban base file for the tutorial (contains definitions for heigt, subst and beta-reduction) changeset | files
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases changeset | files
2011-01-19 Christian Urban added eqvt and supp lemma for removeAll (function from List.thy) changeset | files
2011-01-19 Christian Urban theory name as it should be changeset | files
2011-01-19 Christian Urban removed diagnostic code changeset | files
2011-01-19 Christian Urban added Minimal file to test things changeset | files
2011-01-19 Christian Urban defined height as a function that returns an integer changeset | files
2011-01-18 Christian Urban deleted diagnostic code changeset | files
2011-01-18 Christian Urban some tryes about substitution over type-schemes changeset | files
2011-01-18 Christian Urban defined properly substitution changeset | files
2011-01-18 Christian Urban derived stronger Abs_eq_iff2 theorems changeset | files
2011-01-18 Christian Urban made alpha_abs_set_stronger1 stronger changeset | files
2011-01-18 Christian Urban removed finiteness assumption from set_rename_perm changeset | files
2011-01-18 Cezary Kaliszyk alpha_abs_set_stronger1 changeset | files
2011-01-18 Cezary Kaliszyk alpha_abs_let_stronger is not true in the same form changeset | files
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 changeset | files
2011-01-18 Christian Urban modified the renaming_perm lemmas changeset | files
2011-01-17 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) changeset | files
(0) -1000 -224 +224 tip
nominal2