Nominal/Test.thy
2010-03-19 Cezary Kaliszyk Update Test to use fset.
2010-03-18 Cezary Kaliszyk Leroy96 supp=fv and fixes to make it compile
2010-03-18 Christian Urban corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant
2010-03-18 Cezary Kaliszyk Rename "_property" to ".property"
2010-03-18 Cezary Kaliszyk Added fv,bn,distinct,perm to the simplifier.
2010-03-18 Cezary Kaliszyk Which proofs need a 'sorry'.
2010-03-18 Christian Urban vixed variable names
2010-03-18 Christian Urban simplified strong induction proof by using flip
2010-03-18 Cezary Kaliszyk Rename bound variables + minor cleaning.
2010-03-18 Cezary Kaliszyk Prove pseudo-inject (eq-iff) on the exported level and rename appropriately.
2010-03-17 Christian Urban merged
2010-03-17 Christian Urban added partial proof for the strong induction principle
2010-03-17 Cezary Kaliszyk merge
2010-03-17 Cezary Kaliszyk cheat_alpha_eqvt no longer needed. Cleaned the tracing messages.
2010-03-17 Christian Urban added proof of supp/fv for type schemes
2010-03-17 Christian Urban added partial proof of supp for type schemes
2010-03-17 Cezary Kaliszyk Fix in alpha; support of the recursive Let works :)
2010-03-17 Cezary Kaliszyk The recursive supp just has one equation too much.
2010-03-17 Christian Urban commented out examples that should not work; but for example type-scheme example should work
2010-03-17 Christian Urban added another supp-proof for the non-recursive case
2010-03-16 Christian Urban added the final unfolded result
2010-03-16 Christian Urban merge and proof of support for non-recursive case
2010-03-16 Cezary Kaliszyk alpha_bn doesn't need the permutation in non-recursive case.
2010-03-16 Cezary Kaliszyk FV_bn generated for recursive functions as well, and used in main fv for bindings.
2010-03-16 Cezary Kaliszyk The proof in 'Test' gets simpler.
2010-03-15 Christian Urban merged (confirmed to work with Isabelle from 6th March)
2010-03-15 Christian Urban proof for support when bn-function is present, but fb_function is empty
2010-03-15 Cezary Kaliszyk fv_eqvt_cheat no longer needed.
2010-03-15 Cezary Kaliszyk derive "inducts" from "induct" instead of lifting again is much faster.
2010-03-15 Cezary Kaliszyk cheat_alpha_eqvt no longer needed; the proofs work.
2010-03-15 Cezary Kaliszyk Use eqvt.
2010-03-15 Christian Urban added an eqvt-proof for bi
2010-03-13 Christian Urban started supp-fv proofs (is going to work)
2010-03-11 Cezary Kaliszyk Show that the new types are in finite support typeclass.
2010-03-11 Cezary Kaliszyk With the 4 cheats, all examples fully lift.
2010-03-11 Cezary Kaliszyk Lifting constants.
2010-03-10 Cezary Kaliszyk Reordered examples in Test.
2010-03-10 Cezary Kaliszyk Linked parser to fv and alpha.
2010-03-10 Christian Urban parser produces ordered bn-fun information
2010-03-09 Christian Urban added bn-information, but it is not yet ordered according to the dts
2010-03-09 Cezary Kaliszyk All examples should work.
2010-03-08 Christian Urban added a test-file for compatibility
2010-03-08 Christian Urban added compat definitions to some examples
2010-03-08 Christian Urban deleted comments about "weird"
2010-03-08 Cezary Kaliszyk With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there.
2010-03-07 Christian Urban merged
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban merged
2010-03-04 Christian Urban more proofs in Abs and work on Core Haskell
2010-03-04 Cezary Kaliszyk Lift distinct.
2010-03-04 Cezary Kaliszyk Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples.
2010-03-04 Cezary Kaliszyk Lift BV,FV,Permutations and injection :).
2010-03-04 Cezary Kaliszyk A version that just leaves the supp/\supp goal. Obviously not true.
2010-03-04 Cezary Kaliszyk Prove symp and transp of weird without the supp /\ supp = {} assumption.
2010-03-03 Cezary Kaliszyk merge
2010-03-03 Cezary Kaliszyk Experiments with proving weird transp
2010-03-03 Christian Urban fixed mess in Test.thy
2010-03-03 Cezary Kaliszyk Fix eqvt for multiple quantifiers.
2010-03-03 Christian Urban only tuned
2010-03-03 Christian Urban merged
less more (0) -60 tip