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
2010-11-21 Christian Urban added example Foo2.thy
2010-11-15 Christian Urban tuned example
2010-11-15 Christian Urban proved that bn functions return a finite set
2010-11-15 Christian Urban added a test for the various shallow binders
2010-11-15 Christian Urban fixed bug in fv function where a shallow binder binds lists of names
2010-11-14 Christian Urban merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
2010-11-14 Christian Urban deleted special Nominal2_FSet theory
2010-11-14 Christian Urban moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
2010-11-14 Christian Urban moved most material fron Nominal2_FSet into the Nominal_Base theory
2010-11-14 Christian Urban tuned example
2010-11-14 Christian Urban lifted permute_bn simp rules
2010-11-13 Christian Urban lifted permute_bn constants
2010-11-13 Christian Urban respectfulness for permute_bn functions
2010-11-12 Christian Urban automated permute_bn functions (raw ones first)
2010-11-10 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package
2010-11-10 Christian Urban expanded the paper by uncommenting the comments and adding the appendix
2010-11-07 Christian Urban fixed locally the problem with the function package; all tests work again
2010-11-06 Christian Urban added a test about subtyping; disabled two tests, because of problem with function package
2010-11-05 Christian Urban small typo
2010-10-29 Christian Urban squeezed qpaper to 6 pages
2010-10-29 Cezary Kaliszyk Qpaper / Move examples to commented out appendix
2010-10-28 Cezary Kaliszyk Unanonymize qpaper
2010-10-28 Cezary Kaliszyk FSet changes for Qpaper
2010-10-28 Cezary Kaliszyk Remove FSet and use the one from Isabelle
2010-10-19 Christian Urban took out comment about map-types / adapted to recent changes
2010-10-19 Christian Urban use definitions instead of functions
2010-10-18 Christian Urban tuned
2010-10-18 Christian Urban used functions instead of definitions
2010-10-18 Christian Urban added missing style file
2010-10-18 Cezary Kaliszyk Use the generalized compositional quotient theorem
2010-10-17 Christian Urban fixed typo
2010-10-17 Christian Urban all tests work again
2010-10-17 Christian Urban some tuning
2010-10-17 Christian Urban naming scheme is now *_fset (not f*_)
2010-10-15 Christian Urban more cleaning
2010-10-15 Christian Urban further tuning
2010-10-15 Christian Urban renamed fminus_raw to diff_list
2010-10-15 Christian Urban renamed fcard_raw to card_list
2010-10-15 Christian Urban slight update
2010-10-15 Christian Urban Further reorganisation and cleaning
2010-10-15 Christian Urban further cleaning
2010-10-15 Christian Urban typo
2010-10-15 Cezary Kaliszyk FSet: stronger fact in Isabelle.
2010-10-15 Cezary Kaliszyk FSet synchronizing
2010-10-15 Cezary Kaliszyk Synchronizing FSet further.
2010-10-15 Cezary Kaliszyk Partially merging changes from Isabelle
2010-10-14 Christian Urban fixed the typo in the abstract and the problem with append (the type of map_k
2010-10-14 Christian Urban changed format of the pearl paper
2010-10-14 Christian Urban deleted some unused lemmas
2010-10-14 Christian Urban major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
2010-10-13 Christian Urban more on the pearl paper
2010-10-12 Christian Urban added a section about abstractions
2010-10-12 Christian Urban tiny work on the pearl paper
2010-10-08 Christian Urban tuned
2010-10-08 Christian Urban added apendix to paper detailing one proof
2010-10-08 Christian Urban minor
2010-10-08 Christian Urban minor
2010-10-08 Christian Urban down to 20 pages
2010-10-07 Cezary Kaliszyk minor
2010-10-06 Christian Urban down to 21 pages and changed strong induction section
2010-10-06 Christian Urban tuned
2010-10-06 Christian Urban down to 22 pages
2010-10-05 Christian Urban down to 23 pages
2010-10-05 Christian Urban down to 24 pages and a bit
2010-10-05 Christian Urban llncs and more sqeezing
2010-10-04 Christian Urban first part of sqeezing everything into 20 pages (at the moment we have 26)
2010-10-04 Christian Urban changed to llncs
2010-10-01 Christian Urban merged
2010-10-01 Christian Urban minor experiments
2010-09-30 Christian Urban merged
2010-09-29 Christian Urban simplified exhaust proofs
2010-10-01 Cezary Kaliszyk Made the paper to compile with the renamings.
2010-09-29 Christian Urban merged
2010-09-29 Christian Urban worked example Foo1 with induct_schema
2010-09-29 Christian Urban merged
2010-09-29 Christian Urban use also induct_schema for the Let-example (permute_bn is used)
2010-09-29 Christian Urban test with induct_schema for simpler strong_ind proofs
2010-09-29 Cezary Kaliszyk substitution definition with 'next_name'.
2010-09-28 Christian Urban merged
2010-09-28 Christian Urban added Foo1 to explore a contrived example
2010-09-27 Christian Urban added postprocessed fresh-lemmas for constructors
2010-09-27 Christian Urban post-processed eq_iff and supp threormes according to the fv-supp equality
2010-09-27 Christian Urban more consistent naming in Abs.thy
2010-09-27 Christian Urban some experiments
2010-09-27 Christian Urban added simp rules for prod_fv and prod_alpha
2010-09-26 Christian Urban a few more words about Ott
2010-09-25 Christian Urban lifted size_thms and exported them as <name>.size
2010-09-25 Christian Urban cleaned up two examples
2010-09-25 Christian Urban added example about datatypes
2010-09-23 Christian Urban updated to Isabelle 22 Sept
2010-09-22 Christian Urban removed dead code
2010-09-22 Christian Urban fixed
2010-09-22 Christian Urban made supp proofs more robust by not using the standard induction; renamed some example files
2010-09-20 Christian Urban introduced a general procedure for structural inductions; simplified reflexivity proof
2010-09-17 Christian Urban updated to Isabelle Sept 16
2010-09-17 Christian Urban updated to Isabelle Sept 13
(0) -1000 -240 +240 tip