2010-03-05 Cezary Kaliszyk Still unable to show supp=fv for let with one existential.
2010-03-05 Cezary Kaliszyk Ported LF to the parser interface.
2010-03-05 Cezary Kaliszyk merge
2010-03-05 Cezary Kaliszyk Lift fv and bn eqvts; no need to lift alpha_eqvt.
2010-03-05 Cezary Kaliszyk Not much progress about the single existential let case.
2010-03-05 Cezary Kaliszyk Fixed LF for one quantifier over 2 premises.
2010-03-05 Cezary Kaliszyk Trying to fix the proofs for the single existential... So far failed.
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 Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials.
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 Cezary Kaliszyk Code for solving symp goals with multiple existentials.
2010-03-03 Cezary Kaliszyk reflp for multiple quantifiers.
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
2010-03-03 Christian Urban start of paper - does not compile yet
2010-03-03 Christian Urban added ACM style file for ICFP
2010-03-03 Cezary Kaliszyk weird eqvt
2010-03-03 Cezary Kaliszyk Add the supp intersection conditions.
2010-03-02 Cezary Kaliszyk Comment out the part that does not work with 2 quantifiers.
2010-03-02 Cezary Kaliszyk Fixes for the fv problem and alpha problem.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban preliinary test about alpha-weirdo
2010-03-02 Christian Urban Another problem with permutations in alpha and possibly also in fv
2010-03-02 Christian Urban potential problem with the phd-example, where two permutations are generated, but only one is used
2010-03-02 Cezary Kaliszyk Some tests around Term4. Not sure how to fix the generated fv function.
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Porting from Lift to Parser; until defining the Quotient type.
2010-03-02 Cezary Kaliszyk Add image_eqvt and atom_eqvt to eqvt bases.
2010-03-02 Cezary Kaliszyk Include the raw eqvt lemmas.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added some more examples from Peter Sewell's bestiary
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Minor
2010-03-02 Cezary Kaliszyk Working bv_eqvt
2010-03-02 Cezary Kaliszyk Moving wrappers out of Lift.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban added distinctness of perms
2010-03-02 Christian Urban updated (added lemma about commuting permutations)
2010-03-02 Cezary Kaliszyk Change type schemes to name set.
2010-03-02 Cezary Kaliszyk More fixes for new alpha, the whole lift script should now work again.
2010-03-02 Cezary Kaliszyk Length fix for nested recursions.
2010-03-02 Cezary Kaliszyk Fix equivp.
2010-03-02 Cezary Kaliszyk Fixed eqvt code.
2010-03-02 Christian Urban most tests work - the ones that do not I commented out
2010-03-02 Cezary Kaliszyk merge
2010-03-02 Cezary Kaliszyk Add a check of fv_functions.
2010-03-02 Christian Urban some tuning
2010-03-02 Cezary Kaliszyk Link calls to Raw permutations, FV definition and alpha_definition into the parser.
2010-03-02 Christian Urban merged
2010-03-02 Christian Urban rawified the bind specs (ready to be used now)
2010-03-01 Cezary Kaliszyk merge
2010-03-01 Cezary Kaliszyk Trying to prove equivariance.
2010-03-01 Christian Urban modified for new binding format - hope it is the intended one
2010-03-01 Christian Urban further code-refactoring in the parser
2010-03-01 Cezary Kaliszyk The new alpha-equivalence and testing in Trm2 and Trm5.
2010-03-01 Christian Urban slight simplification of the raw-decl generation
2010-03-01 Cezary Kaliszyk Example that shows that current alpha is wrong.
2010-03-01 Christian Urban added example from my phd
2010-02-27 Christian Urban streamlined parser
2010-02-26 Christian Urban generated the "binding list" from the input; at the moment it is only printed out as tracing; does not yet include the "bind itself binders"
2010-02-26 Cezary Kaliszyk More about the general lifting procedure.
2010-02-26 Cezary Kaliszyk Update TODO
2010-02-26 Cezary Kaliszyk Progress with general lifting procedure.
2010-02-26 Cezary Kaliszyk RSP of perms can be shown in one go.
2010-02-26 Cezary Kaliszyk Change in signature of prove_const_rsp for general lifting.
2010-02-26 Cezary Kaliszyk Permutation and FV_Alpha interface change.
2010-02-26 Cezary Kaliszyk To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.
2010-02-25 Cezary Kaliszyk merge
2010-02-25 Cezary Kaliszyk Preparing the generalized lifting procedure
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban added ott-example about Leroy96
2010-02-25 Cezary Kaliszyk Forgot to add one file.
2010-02-25 Cezary Kaliszyk Split Terms into separate files and add them to tests.
2010-02-25 Cezary Kaliszyk merge
2010-02-25 Cezary Kaliszyk Move the eqvt code out of Terms and fixed induction for single-rule examples.
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban a few simplifications
2010-02-25 Christian Urban first attempt to make sense out of the core-haskell definition
2010-02-25 Cezary Kaliszyk Code for proving eqvt, still in Terms.
2010-02-25 Cezary Kaliszyk Use eqvt infrastructure.
2010-02-25 Cezary Kaliszyk Simple function eqvt code.
2010-02-25 Christian Urban added IsaMakefile...but so far included only a test for the parser
2010-02-25 Christian Urban moved Quot package to Attic (still compiles there with "isabelle make")
2010-02-25 Christian Urban merged
2010-02-25 Christian Urban moved Nominal to "toplevel"
2010-02-25 Cezary Kaliszyk Export perm_frees.
2010-02-24 Cezary Kaliszyk Restructuring the code in Perm
2010-02-24 Cezary Kaliszyk Simplified and finised eqvt proofs for t1 and t5
2010-02-24 Cezary Kaliszyk merge
2010-02-24 Cezary Kaliszyk Define lifted perms.
2010-02-24 Christian Urban merged
2010-02-24 Christian Urban parsing and definition of raw datatype and bv-function work (not very beautiful)
2010-02-24 Cezary Kaliszyk With permute_rsp we can lift the instance proofs :).
2010-02-24 Cezary Kaliszyk Note the instance proofs, since they can be easily lifted.
2010-02-24 Cezary Kaliszyk More refactoring and removed references to the global simpset in Perm.
2010-02-24 Cezary Kaliszyk Factor-out 'prove_perm_empty'; I plan to use it in defining permutations on the lifted type.
2010-02-24 Cezary Kaliszyk Regularize finite support proof for trm1
2010-02-24 Cezary Kaliszyk Made the fv-supp proof much more straightforward.
2010-02-24 Cezary Kaliszyk Regularize the proofs about finite support.
2010-02-24 Cezary Kaliszyk Respects of permute and constructors.
2010-02-24 Cezary Kaliszyk Generate fv_rsp automatically.
2010-02-24 Cezary Kaliszyk Define the constants automatically.
2010-02-24 Cezary Kaliszyk Rename also the lifted types to non-capital.
2010-02-24 Cezary Kaliszyk Use the infrastructure in LF. Much shorter :).
2010-02-24 Cezary Kaliszyk Final synchronization of names.
2010-02-24 Cezary Kaliszyk LF renaming part 3 (proper names of alpha equvalences)
2010-02-24 Cezary Kaliszyk LF renaming part 2 (proper fv functions)
2010-02-24 Cezary Kaliszyk merge
2010-02-24 Cezary Kaliszyk LF renaming part1.
2010-02-24 Christian Urban merged
2010-02-24 Christian Urban parsing of function definitions almost works now; still an error with undefined constants
2010-02-23 Cezary Kaliszyk merge
2010-02-23 Cezary Kaliszyk rsp for bv; the only issue is that it requires an appropriate induction principle.
(0) -1000 -120 +120 +1000 tip