2011-06-03 Cezary Kaliszyk merge
2011-06-03 Cezary Kaliszyk F for lambda used to define translation to locally nameless
2011-06-02 Christian Urban typo
2011-06-02 Christian Urban removed dead code
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-02 Cezary Kaliszyk merge
2011-06-02 Cezary Kaliszyk Remove SMT
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 proved subst for All constructor in type schemes.
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 tuned last commit
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-26 Christian Urban updated to new Isabelle
2011-05-25 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier
2011-05-24 Christian Urban more on slides
2011-05-22 Christian Urban added slides for copenhagen
2011-05-14 Christian Urban added a problem with inductive_cases (reported by Randy)
2011-05-13 Christian Urban misc
2011-05-10 Christian Urban made the subtyping work again
2011-05-10 Christian Urban updated to new Isabelle (> 9 May)
2011-05-09 Christian Urban merged
2011-05-03 Christian Urban added two mutual recursive inductive definitions
2011-05-03 Christian Urban deleted two functions from the API
2011-05-03 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates)
2011-05-09 Christian Urban more on pearl-paper
2011-05-04 Christian Urban more on pearl-paper
2011-05-02 Christian Urban updated Quotient paper so that it compiles again
2011-04-28 Christian Urban merged
2011-04-28 Christian Urban added slides for beijing
2011-04-21 Christian Urban more to the pearl paper
2011-04-19 Christian Urban updated to snapshot Isabelle 19 April
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 merged
2011-04-13 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive
2011-04-12 Christian Urban shanghai slides
2011-04-11 Christian Urban pictures for slides
2011-04-11 Christian Urban Shanghai slides
2011-04-10 Christian Urban more paper
2011-04-09 Christian Urban eqvt of supp and fresh is proved using equivariance infrastructure
2011-04-09 Christian Urban more paper
2011-04-09 Christian Urban more on the paper
2011-04-08 Christian Urban tuned paper
2011-04-08 Christian Urban tuned paper
2011-04-08 Christian Urban typo
2011-04-08 Christian Urban more on paper
2011-04-07 Christian Urban eqvt_lambda without eta-expansion
2011-04-06 Christian Urban changed default preprocessor that does not catch variables only occuring on the right
2011-03-31 Christian Urban final version of slides
2011-03-30 Christian Urban more on the slides
2011-03-30 Christian Urban tuned IsaMakefile
2011-03-29 Christian Urban rearranged directories and updated to new Isabelle
2011-03-16 Christian Urban precise path to LaTeXsugar
2011-03-16 Christian Urban a lit bit more on the pearl-jv paper
2011-03-16 Christian Urban ported changes from function package....needs Isabelle 16 March or above
2011-03-14 Christian Urban more on the pearl paper
2011-03-14 Christian Urban equivariance for All and Ex can be proved in terms of their definition
2011-03-11 Christian Urban more on the paper
2011-03-08 Christian Urban merged
2011-03-08 Christian Urban more on the pearl paper
2011-03-02 Cezary Kaliszyk distinct names at toplevel
2011-03-02 Cezary Kaliszyk merge
2011-03-02 Cezary Kaliszyk Pairing function
2011-03-02 Christian Urban updated pearl papers
2011-03-01 Christian Urban a bit more tuning
2011-02-28 Christian Urban included old test cases for perm_simp into ROOT.ML file
2011-02-28 Christian Urban split the library into a basics file; merged Nominal_Eqvt into Nominal_Base
2011-02-25 Christian Urban some slight polishing
2011-02-24 Christian Urban merged
2011-02-24 Christian Urban added a lemma about fresh_star and Abs
2011-02-23 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules.
2011-02-19 Cezary Kaliszyk typeschemes/subst
2011-02-17 Cezary Kaliszyk further experiments with typeschemes subst
2011-02-17 Cezary Kaliszyk Finished the proof of a function that invents fresh variable names.
2011-02-16 Christian Urban added eqvt for length
2011-02-16 Christian Urban added eqvt lemmas for filter and distinct
2011-02-07 Christian Urban added eqvt for cartesian products
2011-02-07 Christian Urban cleaned up the experiments so that the tests go through
2011-02-04 Cezary Kaliszyk merge
2011-02-04 Cezary Kaliszyk Experiments defining a function on Let
2011-02-04 Christian Urban updated TODO
2011-02-04 Christian Urban Lambda.thy which works with Nominal_Isabelle2011
2011-02-03 Christian Urban merged
2011-02-03 Christian Urban removed diagnostic code
2011-02-01 Cezary Kaliszyk Only one of the subgoals is needed
2011-01-31 Cezary Kaliszyk Experiments with substitution on set+
2011-01-31 Cezary Kaliszyk More properties that relate abs_res and abs_set. Also abs_res with less binders.
2011-01-30 Cezary Kaliszyk alpha_res implies alpha_set :)
2011-01-30 Cezary Kaliszyk Showing that the binders difference is fresh for the left side solves the goal for 'set'.
2011-01-29 Cezary Kaliszyk Experiments with functions
2011-01-27 Christian Urban some experiments
2011-01-27 Christian Urban the proofs with eqvt_at
2011-01-25 Christian Urban made eqvt-proof explicit in the function definitions
2011-01-24 Cezary Kaliszyk merge
2011-01-24 Cezary Kaliszyk minor
2011-01-24 Cezary Kaliszyk Down as infixr
2011-01-23 Christian Urban added some slides
2011-01-23 Christian Urban added Tutorial6
2011-01-23 Christian Urban cleaning up
2011-01-22 Christian Urban merged
2011-01-22 Christian Urban cleaned up Tutorial 3 with solutions
2011-01-22 Cezary Kaliszyk Missing val.simps
2011-01-22 Cezary Kaliszyk merge
2011-01-22 Cezary Kaliszyk Tutorial 4s
2011-01-22 Christian Urban cleaned up and solution section
2011-01-22 Christian Urban cleaned up tutorial1...added solution file
2011-01-22 Christian Urban better version of Tutorial 1
2011-01-21 Christian Urban better flow of proofs and definitions and proof
2011-01-21 Christian Urban separated type preservation and progress into a separate file
2011-01-21 Christian Urban substitution lemma in separate file
2011-01-21 Christian Urban added unbind example
2011-01-20 Christian Urban a bit tuning
2011-01-20 Christian Urban first split of tutorrial theory
2011-01-19 Christian Urban added a very rough version of the tutorial; all seems to work
2011-01-19 Christian Urban added obtain_fresh lemma; tuned Lambda.thy
2011-01-19 Christian Urban base file for the tutorial (contains definitions for heigt, subst and beta-reduction)
2011-01-19 Christian Urban ported some of the old proofs to serve as testcases
2011-01-19 Christian Urban added eqvt and supp lemma for removeAll (function from List.thy)
2011-01-19 Christian Urban theory name as it should be
2011-01-19 Christian Urban removed diagnostic code
2011-01-19 Christian Urban added Minimal file to test things
2011-01-19 Christian Urban defined height as a function that returns an integer
2011-01-18 Christian Urban deleted diagnostic code
2011-01-18 Christian Urban some tryes about substitution over type-schemes
2011-01-18 Christian Urban defined properly substitution
2011-01-18 Christian Urban derived stronger Abs_eq_iff2 theorems
2011-01-18 Christian Urban made alpha_abs_set_stronger1 stronger
2011-01-18 Christian Urban removed finiteness assumption from set_rename_perm
2011-01-18 Cezary Kaliszyk alpha_abs_set_stronger1
2011-01-18 Cezary Kaliszyk alpha_abs_let_stronger is not true in the same form
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-18 Christian Urban modified the renaming_perm lemmas
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 exported nominal function code to external file
2011-01-17 Christian Urban removed old testing code from Lambda.thy
2011-01-17 Christian Urban moved high level code from LamTest into the main libraries.
2011-01-17 Christian Urban eliminated tracing code; added flag so that equivariance is only proved for the function graph, not the relation
2011-01-15 Christian Urban subst also works now
2011-01-15 Christian Urban nominal_function works now completely for frees and depth; still a propbelm with subst; no unproved assumptions
2011-01-14 Christian Urban strengthened renaming lemmas
2011-01-13 Christian Urban added eqvt_lemmas for subset and psubset
2011-01-10 Christian Urban a few lemmas about freshness for at and at_base
2011-01-10 Christian Urban added a property about finite support in the presense of eqvt_at
2011-01-09 Christian Urban instantiated fundef_ex1_eqvt_at theorem with the indction hypothesis
2011-01-09 Christian Urban solved subgoals for depth and subst function
2011-01-09 Christian Urban added eqvt_at premises in function definition - however not proved at the moment
2011-01-07 Christian Urban added one further lemma about equivariance of THE_default
2011-01-07 Christian Urban equivariance of THE_default under the uniqueness assumption
2011-01-07 Christian Urban derived equivariance for the function graph and function relation
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 removed last traces of debugging code
2011-01-06 Christian Urban removed debugging code abd introduced a guarded tracing function
2011-01-06 Christian Urban moved Weakening up....it does not compile when put at the last position
2011-01-06 Christian Urban tuned
2011-01-06 Christian Urban added weakening to the test cases
2011-01-06 Christian Urban cleaned up weakening proof and added a version with finit sets
2011-01-06 Christian Urban same
2011-01-06 Christian Urban some further lemmas for fsets
2011-01-06 Christian Urban made sure the raw datatypes and raw functions do not get any mixfix syntax
2011-01-05 Christian Urban exported the code into a separate file
2011-01-05 Christian Urban strong rule inductions; as an example the weakening lemma works
2011-01-04 Christian Urban final version of the ESOP paper; used set+ instead of res as requested by one reviewer
2011-01-03 Christian Urban file with most of the strong rule induction development
2011-01-03 Christian Urban simple cases for string rule inductions
2010-12-31 Christian Urban changed res keyword to set+ for restrictions; comment by a referee
2010-12-31 Christian Urban added proper case names for all induct and exhaust theorems
2010-12-31 Christian Urban added small example for strong inductions; functions still need a sorry
2010-12-30 Christian Urban removed local fix for bug in induction_schema; added setup method for strong inductions
2010-12-28 Christian Urban automated all strong induction lemmas
2010-12-28 Christian Urban proper application of induction_schema and strong_exhaust rules; needs local fix in induction_schema.ML
2010-12-26 Christian Urban generated goals for strong induction theorems.
2010-12-23 Christian Urban test with strong inductions
2010-12-23 Christian Urban moved all strong_exhaust code to nominal_dt_quot; tuned examples
2010-12-23 Christian Urban moved generic functions into nominal_library
2010-12-22 Christian Urban slight tuning
2010-12-22 Christian Urban slight tuning
2010-12-22 Christian Urban tuned examples
2010-12-22 Christian Urban added fold_right which produces the correct term for left-infix operators
2010-12-22 Christian Urban updated to Isabelle 22 December
2010-12-22 Christian Urban a bit tuning
2010-12-22 Christian Urban corrected premises of strong exhausts theorems
2010-12-22 Christian Urban properly exported strong exhaust theorem; cleaned up some examples
2010-12-21 Christian Urban all examples for strong exhausts work; recursive binders need to be treated differently; still unclean version with lots of diagnostic code
2010-12-19 Christian Urban one interesting case done
2010-12-19 Christian Urban a stronger statement for at_set_avoiding
2010-12-17 Christian Urban tuned
2010-12-17 Christian Urban tuned
2010-12-16 Christian Urban simple cases for strong inducts done; infrastructure for the difficult ones is there
2010-12-16 Christian Urban added theorem-rewriter conversion
2010-12-14 Christian Urban freshness theorem in strong exhausts; (temporarily includes a cheat_tac to make all tests go through)
2010-12-12 Christian Urban created strong_exhausts terms
2010-12-12 Christian Urban moved setify and listify functions into the library; introduced versions that have a type argument
2010-12-10 Christian Urban updated
2010-12-09 Christian Urban a bit more tuning of the paper
2010-12-09 Christian Urban brought the paper to 20 pages plus one page appendix
2010-12-08 Christian Urban first tests about exhaust
2010-12-08 Christian Urban moved some code into the nominal_library
2010-12-08 Christian Urban moved definition of raw bn-functions into nominal_dt_rawfuns
2010-12-08 Christian Urban kept the nested structure of constructors (belonging to one datatype)
2010-12-07 Christian Urban moved general theorems into the libraries
2010-12-07 Christian Urban automated permute_bn theorems
2010-12-07 Christian Urban updated to changes in Isabelle
2010-12-06 Christian Urban deleted nominal_dt_supp.ML
2010-12-06 Christian Urban moved code from nominal_dt_supp to nominal_dt_quot
2010-12-06 Christian Urban automated alpha_perm_bn theorems
2010-12-06 Christian Urban ordered raw_bn_info to agree with the order of the raw_bn_functions; started alpha_bn proof
2010-12-03 Christian Urban updated to Isabelle 2nd December
2010-11-29 Christian Urban isarfied some of the high-level proofs
2010-11-29 Christian Urban added abs_rename_res lemma
2010-11-29 Christian Urban completed proofs in Foo2
2010-11-28 Christian Urban completed the strong exhausts rules for Foo2 using general lemmas
2010-11-27 Christian Urban tuned proof to reduce number of warnings
2010-11-27 Christian Urban disabled the Foo examples, because of heavy work
2010-11-26 Christian Urban slightly simplified the Foo2 tests and hint at a general lemma
2010-11-26 Christian Urban completely different method fro deriving the exhaust lemma
2010-11-26 Christian Urban merged
2010-11-25 Christian Urban merged
2010-11-24 Christian Urban added example from the F-ing paper by Rossberg, Russo and Dreyer
2010-11-24 Christian Urban implemented concrete suggestion of 3rd reviewer
2010-11-26 Cezary Kaliszyk missing freshness assumptions
2010-11-25 Cezary Kaliszyk foo2 strong induction
2010-11-24 Cezary Kaliszyk foo2 full exhausts
2010-11-24 Cezary Kaliszyk Foo2 strong_exhaust for first variable.
2010-11-22 Cezary Kaliszyk single rename in let2
2010-11-22 Cezary Kaliszyk current isabelle
(0) -1000 -240 +240 tip