2011-06-22 Christian Urban deleted some dead code
2011-06-22 Christian Urban some rudimentary infrastructure for storing data about nominal datatypes
2011-06-22 Cezary Kaliszyk constants with the same names
2011-06-21 Cezary Kaliszyk Quotients/TODO addtion
2011-06-21 Cezary Kaliszyk Minor
2011-06-21 Cezary Kaliszyk merge
2011-06-21 Cezary Kaliszyk spelling
2011-06-20 Cezary Kaliszyk merge
2011-06-20 Cezary Kaliszyk Abs_set_fcb
2011-06-20 Cezary Kaliszyk function for let-rec
2011-06-20 Cezary Kaliszyk TODO/minor
2011-06-20 Cezary Kaliszyk Move lst_fcb to Nominal2_Abs
2011-06-20 Cezary Kaliszyk More minor TODOs
2011-06-20 Cezary Kaliszyk Update TODO
2011-06-20 Cezary Kaliszyk Let/minor
2011-06-19 Cezary Kaliszyk Update Quotient/TODO and remove some attic code
2011-06-19 Cezary Kaliszyk merge
2011-06-19 Cezary Kaliszyk little on cps2
2011-06-16 Christian Urban got rid of the boolean flag in the raw_equivariance function
2011-06-16 Cezary Kaliszyk Fix
2011-06-16 Cezary Kaliszyk merge
2011-06-16 Cezary Kaliszyk CPS3 can be defined with eqvt_rhs.
2011-06-16 Christian Urban moved for the moment CPS translations into the example directory
2011-06-16 Christian Urban merged
2011-06-16 Christian Urban added eqvt_at and invariant for boths sides of the equations
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.
2011-06-16 Christian Urban added a test that every function must be of pt-sort
2011-06-16 Christian Urban all tests work again
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 Christian Urban added an abstract
2011-06-15 Christian Urban added a stub for function paper; "isabelle make fnpaper"
2011-06-15 Cezary Kaliszyk merge
2011-06-15 Cezary Kaliszyk one TODO and one Problem?
2011-06-15 Cezary Kaliszyk merge
2011-06-15 Cezary Kaliszyk Some TODOs
2011-06-15 Cezary Kaliszyk merge
2011-06-15 Cezary Kaliszyk TypeSchemes work with 'default'.
2011-06-14 Christian Urban tuned some proofs
2011-06-14 Christian Urban fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
2011-06-14 Christian Urban tuned
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 merge
2011-06-10 Cezary Kaliszyk Slightly modify fcb for list1 and put in common place.
2011-06-10 Cezary Kaliszyk Experiments with Let
2011-06-09 Cezary Kaliszyk Eval can be defined with additional freshness
2011-06-09 Cezary Kaliszyk Minor simplification
2011-06-09 Cezary Kaliszyk abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
2011-06-09 Cezary Kaliszyk More experiments with 'default'
2011-06-08 Cezary Kaliszyk Finished the proof with the invariant
2011-06-08 Cezary Kaliszyk Issue with 'default'
2011-06-08 Christian Urban merged
2011-06-08 Christian Urban merged
2011-06-08 Christian Urban using the option "default" the function package allows one to give an explicit default value
2011-06-08 Cezary Kaliszyk Simpler proof of TypeSchemes/substs
2011-06-08 Cezary Kaliszyk Simplify fcb_res
2011-06-08 Cezary Kaliszyk FCB for res binding and simplified proof of subst for type schemes
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 Cezary Kaliszyk Testing invariant in Lambda_F_T
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-06 Christian Urban slightly stronger property in fundef_ex_prop
2011-06-05 Christian Urban added an option for an invariant (at the moment only a stub)
2011-06-05 Christian Urban added a more general lemma fro fundef_ex1
2011-06-04 Cezary Kaliszyk Trying the induction on the graph
2011-06-04 Cezary Kaliszyk Finish and test the locale approach
2011-06-03 Cezary Kaliszyk FiniteSupp precondition in the function is enough to get rid of completeness obligationss
2011-06-03 Christian Urban recursion combinator inside a locale
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.
(0) -1000 -120 +120 tip