| Fri, 19 Mar 2010 15:43:43 +0100 | Christian Urban | polished | changeset | files |
| Fri, 19 Mar 2010 15:01:01 +0100 | Cezary Kaliszyk | Update Test to use fset. | changeset | files |
| Fri, 19 Mar 2010 14:54:57 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 19 Mar 2010 14:54:30 +0100 | Cezary Kaliszyk | Use fs typeclass in showing finite support + some cheat cleaning. | changeset | files |
| Fri, 19 Mar 2010 12:31:55 +0100 | Christian Urban | merged | changeset | files |
| Fri, 19 Mar 2010 12:31:17 +0100 | Christian Urban | more one the paper | changeset | files |
| Fri, 19 Mar 2010 12:28:35 +0100 | Cezary Kaliszyk | Keep only one copy of infinite_Un. | changeset | files |
| Fri, 19 Mar 2010 12:24:16 +0100 | Cezary Kaliszyk | Added a missing 'import'. | changeset | files |
| Fri, 19 Mar 2010 12:22:10 +0100 | Cezary Kaliszyk | Showed the instance: fset::(at) fs | changeset | files |
| Fri, 19 Mar 2010 10:24:49 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 19 Mar 2010 10:24:16 +0100 | Cezary Kaliszyk | Remove atom_decl from the parser. | changeset | files |
| Fri, 19 Mar 2010 10:23:52 +0100 | Cezary Kaliszyk | TySch strong induction looks ok. | changeset | files |
| Fri, 19 Mar 2010 09:31:38 +0100 | Cezary Kaliszyk | Working on TySch strong induction. | changeset | files |
| Fri, 19 Mar 2010 09:03:10 +0100 | Cezary Kaliszyk | Something is wrong with the statement of strong induction for TySch, as the All case is trivial and Fun case unprovable... | changeset | files |
| Fri, 19 Mar 2010 09:40:57 +0100 | Christian Urban | merged | changeset | files |
| Fri, 19 Mar 2010 09:40:34 +0100 | Christian Urban | more tuning on the paper | changeset | files |
| Fri, 19 Mar 2010 08:31:43 +0100 | Cezary Kaliszyk | The nominal infrastructure for fset. 'fs' missing, but not needed so far. | changeset | files |
| Fri, 19 Mar 2010 06:55:17 +0100 | Cezary Kaliszyk | A few more theorems in FSet. | changeset | files |
| Fri, 19 Mar 2010 00:36:08 +0100 | Cezary Kaliszyk | merge 2 | changeset | files |
| Fri, 19 Mar 2010 00:35:58 +0100 | Cezary Kaliszyk | merge 1 | changeset | files |
| Fri, 19 Mar 2010 00:35:20 +0100 | Cezary Kaliszyk | support of fset_to_set, support of fmap_atom. | changeset | files |
| Thu, 18 Mar 2010 23:39:48 +0100 | Christian Urban | merged | changeset | files |
| Thu, 18 Mar 2010 23:39:26 +0100 | Christian Urban | more tuning on the paper | changeset | files |
| Thu, 18 Mar 2010 23:38:01 +0100 | Christian Urban | added item about size functions | changeset | files |
| Thu, 18 Mar 2010 23:20:46 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Thu, 18 Mar 2010 23:19:55 +0100 | Cezary Kaliszyk | Reached strong_induction in fset-based TySch. Will not work until isabelle changes are pushed. | changeset | files |
| Thu, 18 Mar 2010 22:06:28 +0100 | Christian Urban | tuned | changeset | files |
| Thu, 18 Mar 2010 19:39:01 +0100 | Christian Urban | another little bit for the introduction | changeset | files |
| Thu, 18 Mar 2010 19:02:33 +0100 | Cezary Kaliszyk | Leroy96 supp=fv and fixes to make it compile | changeset | files |
| Thu, 18 Mar 2010 18:43:21 +0100 | Christian Urban | merged | changeset | files |
| Thu, 18 Mar 2010 18:43:03 +0100 | Christian Urban | more of the introduction | changeset | files |
| Thu, 18 Mar 2010 18:10:49 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Thu, 18 Mar 2010 18:10:20 +0100 | Cezary Kaliszyk | Added a cleaned version of FSet. | changeset | files |
| Thu, 18 Mar 2010 16:22:10 +0100 | Christian Urban | corrected the strong induction principle in the lambda-calculus case; gave a second (oartial) version that is more elegant | changeset | files |
| Thu, 18 Mar 2010 15:32:49 +0100 | Cezary Kaliszyk | Continued description of alpha. | changeset | files |
| Thu, 18 Mar 2010 15:13:20 +0100 | Cezary Kaliszyk | Rename "_property" to ".property" | changeset | files |
| Thu, 18 Mar 2010 14:48:27 +0100 | Cezary Kaliszyk | First part of the description of alpha_ty. | changeset | files |
| Thu, 18 Mar 2010 14:29:42 +0100 | Cezary Kaliszyk | Description of generation of alpha_bn. | changeset | files |
| Thu, 18 Mar 2010 14:05:49 +0100 | Cezary Kaliszyk | case names also for _induct | changeset | files |
| Thu, 18 Mar 2010 12:32:03 +0100 | Cezary Kaliszyk | Case_Names for _inducts. Does not work for _induct yet. | changeset | files |
| Thu, 18 Mar 2010 12:09:59 +0100 | Cezary Kaliszyk | Added fv,bn,distinct,perm to the simplifier. | changeset | files |
| Thu, 18 Mar 2010 11:37:10 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Thu, 18 Mar 2010 11:36:03 +0100 | Cezary Kaliszyk | Simplified the description. | changeset | files |
| Thu, 18 Mar 2010 11:33:56 +0100 | Christian Urban | merged | changeset | files |
| Thu, 18 Mar 2010 11:33:37 +0100 | Christian Urban | slightly more in the paper | changeset | files |
| Thu, 18 Mar 2010 11:29:12 +0100 | Cezary Kaliszyk | Update the description of the generation of fv function. | changeset | files |
| Thu, 18 Mar 2010 11:16:53 +0100 | Cezary Kaliszyk | fv_bn may need to call other fv_bns. | changeset | files |
| Thu, 18 Mar 2010 10:15:57 +0100 | Cezary Kaliszyk | Update TODO. | changeset | files |
| Thu, 18 Mar 2010 10:12:41 +0100 | Cezary Kaliszyk | Which proofs need a 'sorry'. | changeset | files |
| Thu, 18 Mar 2010 10:05:36 +0100 | Christian Urban | added TODO | changeset | files |
| Thu, 18 Mar 2010 10:02:21 +0100 | Christian Urban | vixed variable names | changeset | files |
| Thu, 18 Mar 2010 09:31:31 +0100 | Christian Urban | simplified strong induction proof by using flip | changeset | files |
| Thu, 18 Mar 2010 08:32:55 +0100 | Cezary Kaliszyk | Rename bound variables + minor cleaning. | changeset | files |
| Thu, 18 Mar 2010 08:03:42 +0100 | Cezary Kaliszyk | Move most of the exporting out of the parser. | changeset | files |
| Thu, 18 Mar 2010 07:43:44 +0100 | Cezary Kaliszyk | Prove pseudo-inject (eq-iff) on the exported level and rename appropriately. | changeset | files |
| Thu, 18 Mar 2010 07:35:44 +0100 | Cezary Kaliszyk | Prove eqvts on exported terms. | changeset | files |
| Thu, 18 Mar 2010 07:26:36 +0100 | Cezary Kaliszyk | Clean 'Lift', start working only on exported things in Parser. | changeset | files |
| Thu, 18 Mar 2010 00:17:21 +0100 | Christian Urban | slightly more of the paper | changeset | files |
| Wed, 17 Mar 2010 20:42:42 +0100 | Christian Urban | merged | changeset | files |
| Wed, 17 Mar 2010 20:42:22 +0100 | Christian Urban | paper uses now a heap file - does not compile so long anymore | changeset | files |
| Wed, 17 Mar 2010 18:53:23 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 17 Mar 2010 18:52:59 +0100 | Cezary Kaliszyk | compose_sym2 works also for term5 | changeset | files |
| Wed, 17 Mar 2010 17:59:04 +0100 | Cezary Kaliszyk | Updated Term1, including statement of strong induction. | changeset | files |
| Wed, 17 Mar 2010 17:40:14 +0100 | Cezary Kaliszyk | Proper compose_sym2 | changeset | files |
| Wed, 17 Mar 2010 17:11:23 +0100 | Christian Urban | merged | changeset | files |
| Wed, 17 Mar 2010 17:10:19 +0100 | Christian Urban | temporarily disabled tests in Nominal/ROOT | changeset | files |
| Wed, 17 Mar 2010 15:13:31 +0100 | Christian Urban | made paper to compile | changeset | files |
| Wed, 17 Mar 2010 15:13:03 +0100 | Christian Urban | added partial proof for the strong induction principle | changeset | files |
| Wed, 17 Mar 2010 17:09:01 +0100 | Cezary Kaliszyk | Trying to find a compose lemma for 2 arguments. | changeset | files |
| Wed, 17 Mar 2010 12:23:04 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 17 Mar 2010 12:18:35 +0100 | Cezary Kaliszyk | cheat_alpha_eqvt no longer needed. Cleaned the tracing messages. | changeset | files |
| Wed, 17 Mar 2010 11:54:22 +0100 | Christian Urban | merged | changeset | files |
| Wed, 17 Mar 2010 11:53:56 +0100 | Christian Urban | added proof of supp/fv for type schemes | changeset | files |
| Wed, 17 Mar 2010 11:40:58 +0100 | Cezary Kaliszyk | Updated Type Schemes to automatic lifting. One goal is not true because of the restriction. | changeset | files |
| Wed, 17 Mar 2010 11:20:24 +0100 | Cezary Kaliszyk | Remove Term5a, since it is now identical to Term5. | changeset | files |
| Wed, 17 Mar 2010 11:11:42 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 17 Mar 2010 11:11:25 +0100 | Cezary Kaliszyk | Finished all proofs in Term5 and Term5n. | changeset | files |
| Wed, 17 Mar 2010 10:34:25 +0100 | Christian Urban | added partial proof of supp for type schemes | changeset | files |
| Wed, 17 Mar 2010 09:57:54 +0100 | Cezary Kaliszyk | Fix in alpha; support of the recursive Let works :) | changeset | files |
| Wed, 17 Mar 2010 09:42:56 +0100 | Cezary Kaliszyk | The recursive supp just has one equation too much. | changeset | files |
| Wed, 17 Mar 2010 09:25:01 +0100 | Cezary Kaliszyk | Fix for the change of alpha_gen. | changeset | files |
| Wed, 17 Mar 2010 09:18:27 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 17 Mar 2010 09:17:55 +0100 | Cezary Kaliszyk | Generate compound FV and Alpha for recursive bindings. | changeset | files |
| Wed, 17 Mar 2010 08:39:46 +0100 | Cezary Kaliszyk | Lifting theorems with compound fv and compound alpha. | changeset | files |
| Wed, 17 Mar 2010 08:07:25 +0100 | Christian Urban | commented out examples that should not work; but for example type-scheme example should work | changeset | files |
| Wed, 17 Mar 2010 06:49:33 +0100 | Christian Urban | added another supp-proof for the non-recursive case | changeset | files |
| Tue, 16 Mar 2010 20:07:13 +0100 | Cezary Kaliszyk | Revert 7c8cd6eae8e2, now all proofs in Term5 go through, both recursive and not. | changeset | files |
| Tue, 16 Mar 2010 18:19:00 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Tue, 16 Mar 2010 18:18:08 +0100 | Cezary Kaliszyk | The old recursive alpha works fine. | changeset | files |
| Tue, 16 Mar 2010 18:13:34 +0100 | Christian Urban | added the final unfolded result | changeset | files |
| Tue, 16 Mar 2010 18:02:08 +0100 | Christian Urban | merge and proof of support for non-recursive case | changeset | files |
| Tue, 16 Mar 2010 17:20:46 +0100 | Cezary Kaliszyk | Added Term5 non-recursive. The bug is there only for the recursive case. | changeset | files |
| Tue, 16 Mar 2010 17:11:32 +0100 | Cezary Kaliszyk | Alpha is wrong. | changeset | files |
| Tue, 16 Mar 2010 16:51:06 +0100 | Cezary Kaliszyk | alpha_bn doesn't need the permutation in non-recursive case. | changeset | files |
| Tue, 16 Mar 2010 16:17:05 +0100 | Cezary Kaliszyk | alpha5_transp and equivp | changeset | files |
| Tue, 16 Mar 2010 15:38:14 +0100 | Cezary Kaliszyk | alpha5_symp proved. | changeset | files |
| Tue, 16 Mar 2010 15:27:47 +0100 | Cezary Kaliszyk | FV_bn generated for recursive functions as well, and used in main fv for bindings. | changeset | files |
| Tue, 16 Mar 2010 12:08:37 +0100 | Cezary Kaliszyk | The proof in 'Test' gets simpler. | changeset | files |
| Tue, 16 Mar 2010 12:06:22 +0100 | Cezary Kaliszyk | Removed pi o bn = bn' assumption in alpha | changeset | files |
| Mon, 15 Mar 2010 23:42:56 +0100 | Christian Urban | merged (confirmed to work with Isabelle from 6th March) | changeset | files |
| Mon, 15 Mar 2010 17:52:31 +0100 | Christian Urban | another synchronisation | changeset | files |
| Mon, 15 Mar 2010 17:51:35 +0100 | Christian Urban | proof for support when bn-function is present, but fb_function is empty | changeset | files |
| Mon, 15 Mar 2010 17:42:17 +0100 | Cezary Kaliszyk | fv_eqvt_cheat no longer needed. | changeset | files |
| Mon, 15 Mar 2010 14:32:05 +0100 | Cezary Kaliszyk | derive "inducts" from "induct" instead of lifting again is much faster. | changeset | files |
| Mon, 15 Mar 2010 13:56:17 +0100 | Cezary Kaliszyk | build_eqvts works with recursive case if proper induction rule is used. | changeset | files |
| Mon, 15 Mar 2010 11:50:12 +0100 | Cezary Kaliszyk | cheat_alpha_eqvt no longer needed; the proofs work. | changeset | files |
| Mon, 15 Mar 2010 10:36:09 +0100 | Cezary Kaliszyk | LF works with new alpha...? | changeset | files |
| Mon, 15 Mar 2010 10:07:15 +0100 | Cezary Kaliszyk | explicit flag "cheat_equivp" | changeset | files |
| Mon, 15 Mar 2010 10:02:19 +0100 | Cezary Kaliszyk | Prove alpha_gen_compose_eqvt | changeset | files |
| Mon, 15 Mar 2010 09:27:25 +0100 | Cezary Kaliszyk | Use eqvt. | changeset | files |
| Mon, 15 Mar 2010 08:39:23 +0100 | Christian Urban | added preliminary test version....but Test works now | changeset | files |
| Mon, 15 Mar 2010 08:28:10 +0100 | Christian Urban | added an eqvt-proof for bi | changeset | files |
| Mon, 15 Mar 2010 06:11:35 +0100 | Christian Urban | synchronised with main hg-repository; used add_typedef_global in nominal_atoms | changeset | files |
| Sun, 14 Mar 2010 11:36:15 +0100 | Christian Urban | localised the typedef in Attic (requires new Isabelle) | changeset | files |
| Sat, 13 Mar 2010 13:49:15 +0100 | Christian Urban | started supp-fv proofs (is going to work) | changeset | files |
| Fri, 12 Mar 2010 17:42:31 +0100 | Cezary Kaliszyk | Even with pattern simplified to a single clause, the supp equation doesn't seem true. | changeset | files |
| Fri, 12 Mar 2010 12:42:35 +0100 | Cezary Kaliszyk | Still don't know how to prove supp=fv for simplest Let... | changeset | files |
| Thu, 11 Mar 2010 20:49:31 +0100 | Cezary Kaliszyk | Do not fail if the finite support proof fails. | changeset | files |
| Thu, 11 Mar 2010 19:43:50 +0100 | Christian Urban | generalised the supp for atoms to all concrete atoms (not just names) | changeset | files |
| Thu, 11 Mar 2010 19:41:11 +0100 | Christian Urban | support of atoms at the end of Abs.thy | changeset | files |
| Thu, 11 Mar 2010 19:24:07 +0100 | Cezary Kaliszyk | Trying to prove atom_image_fresh_swap | changeset | files |
| Thu, 11 Mar 2010 17:49:07 +0100 | Cezary Kaliszyk | Finite_support proof no longer needed in LF. | changeset | files |
| Thu, 11 Mar 2010 17:47:29 +0100 | Cezary Kaliszyk | Show that the new types are in finite support typeclass. | changeset | files |
| Thu, 11 Mar 2010 16:50:44 +0100 | Cezary Kaliszyk | mk_supports_eq and supports_tac. | changeset | files |
| Thu, 11 Mar 2010 16:16:15 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Thu, 11 Mar 2010 16:15:29 +0100 | Cezary Kaliszyk | Fixes for term1 for new alpha. Still not able to show support equations. | changeset | files |
| Thu, 11 Mar 2010 16:12:15 +0100 | Christian Urban | merged | changeset | files |
| Thu, 11 Mar 2010 15:10:07 +0100 | Christian Urban | finally the proof that new and old alpha agree | changeset | files |
| Thu, 11 Mar 2010 15:11:57 +0100 | Cezary Kaliszyk | Remove "_raw" from lifted theorems. | changeset | files |
| Thu, 11 Mar 2010 14:09:54 +0100 | Cezary Kaliszyk | looking at trm5_equivp | changeset | files |
| Thu, 11 Mar 2010 14:05:36 +0100 | Cezary Kaliszyk | The cheats described explicitely. | changeset | files |
| Thu, 11 Mar 2010 13:44:54 +0100 | Cezary Kaliszyk | The alpha5_eqvt tactic works if I manage to build the goal. | changeset | files |
| Thu, 11 Mar 2010 13:34:45 +0100 | Cezary Kaliszyk | With the 4 cheats, all examples fully lift. | changeset | files |
| Thu, 11 Mar 2010 12:30:53 +0100 | Cezary Kaliszyk | Lift alpha_bn_constants. | changeset | files |
| Thu, 11 Mar 2010 12:26:24 +0100 | Cezary Kaliszyk | Lifting constants. | changeset | files |
| Thu, 11 Mar 2010 11:41:27 +0100 | Cezary Kaliszyk | Proper error message. | changeset | files |
| Thu, 11 Mar 2010 11:32:37 +0100 | Cezary Kaliszyk | Lifting constants works for all examples. | changeset | files |
| Thu, 11 Mar 2010 11:25:56 +0100 | Cezary Kaliszyk | Remove tracing from fv/alpha. | changeset | files |
| Thu, 11 Mar 2010 11:25:18 +0100 | Cezary Kaliszyk | Equivp working only on the standard alpha-equivalences. | changeset | files |
| Thu, 11 Mar 2010 11:20:50 +0100 | Cezary Kaliszyk | explicit cheat_fv_eqvt | changeset | files |
| Thu, 11 Mar 2010 11:15:14 +0100 | Cezary Kaliszyk | extract build_eqvts_tac. | changeset | files |
| Thu, 11 Mar 2010 10:39:29 +0100 | Cezary Kaliszyk | build_eqvts no longer requires permutations. | changeset | files |
| Thu, 11 Mar 2010 10:22:24 +0100 | Cezary Kaliszyk | Add explicit alpha_eqvt_cheat. | changeset | files |
| Thu, 11 Mar 2010 10:10:23 +0100 | Cezary Kaliszyk | Export tactic out of alpha_eqvt. | changeset | files |
| Wed, 10 Mar 2010 16:59:08 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 10 Mar 2010 16:58:14 +0100 | Cezary Kaliszyk | More tries about the proofs in trm5 | changeset | files |
| Wed, 10 Mar 2010 16:51:15 +0100 | Christian Urban | merged | changeset | files |
| Wed, 10 Mar 2010 16:50:42 +0100 | Christian Urban | almost done with showing the equivalence between old and new alpha-equivalence (one subgoal remaining) | changeset | files |
| Wed, 10 Mar 2010 15:40:15 +0100 | Cezary Kaliszyk | alpha_equivp for trm5 | changeset | files |
| Wed, 10 Mar 2010 15:34:13 +0100 | Cezary Kaliszyk | Undoing mistakenly committed parser experiments. | changeset | files |
| Wed, 10 Mar 2010 15:32:51 +0100 | Cezary Kaliszyk | alpha_eqvt for recursive term1. | changeset | files |
| Wed, 10 Mar 2010 14:47:04 +0100 | Cezary Kaliszyk | Looking at alpha_eqvt for term5, not much progress. | changeset | files |
| Wed, 10 Mar 2010 14:24:27 +0100 | Cezary Kaliszyk | Reordered examples in Test. | changeset | files |
| Wed, 10 Mar 2010 13:29:12 +0100 | Cezary Kaliszyk | Allows multiple bindings with same lhs. | changeset | files |
| Wed, 10 Mar 2010 13:10:00 +0100 | Cezary Kaliszyk | Linked parser to fv and alpha. | changeset | files |
| Wed, 10 Mar 2010 12:53:44 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 10 Mar 2010 12:53:30 +0100 | Cezary Kaliszyk | A minor fix for shallow binders. LF works again. | changeset | files |
| Wed, 10 Mar 2010 12:48:55 +0100 | Christian Urban | merged | changeset | files |
| Wed, 10 Mar 2010 12:48:38 +0100 | Christian Urban | parser produces ordered bn-fun information | changeset | files |
| Wed, 10 Mar 2010 11:39:28 +0100 | Cezary Kaliszyk | Testing equalities in trm5, all seems good. | changeset | files |
| Wed, 10 Mar 2010 11:19:59 +0100 | Cezary Kaliszyk | Fv&Alpha seem to work. | changeset | files |
| Wed, 10 Mar 2010 10:47:21 +0100 | Cezary Kaliszyk | include alpha in the definitions. | changeset | files |
| Wed, 10 Mar 2010 10:11:20 +0100 | Cezary Kaliszyk | Filled the algorithm for alpha_bn_arg | changeset | files |
| Wed, 10 Mar 2010 09:58:43 +0100 | Cezary Kaliszyk | rhs of alpha_bn, and template for the arguments. | changeset | files |
| Wed, 10 Mar 2010 09:45:38 +0100 | Cezary Kaliszyk | alpha_bn_constr template | changeset | files |
| Wed, 10 Mar 2010 09:36:07 +0100 | Cezary Kaliszyk | exported template for alpha_bn | changeset | files |
| Wed, 10 Mar 2010 09:10:11 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 10 Mar 2010 09:09:52 +0100 | Cezary Kaliszyk | Use alpha_bns in normal alpha defs. | changeset | files |
| Wed, 10 Mar 2010 08:44:19 +0100 | Cezary Kaliszyk | alpha_bn_frees | changeset | files |
| Tue, 09 Mar 2010 22:10:10 +0100 | Christian Urban | merged | changeset | files |
| Tue, 09 Mar 2010 22:08:38 +0100 | Christian Urban | added bn-information, but it is not yet ordered according to the dts | changeset | files |
| Tue, 09 Mar 2010 21:22:22 +0100 | Cezary Kaliszyk | Separate lists for separate constructors, to match bn_eqs. | changeset | files |
| Tue, 09 Mar 2010 17:25:35 +0100 | Cezary Kaliszyk | All examples should work. | changeset | files |
| Tue, 09 Mar 2010 17:02:29 +0100 | Cezary Kaliszyk | Fix to get old alpha. | changeset | files |
| Tue, 09 Mar 2010 16:57:51 +0100 | Cezary Kaliszyk | Separate primrecs in Fv. | changeset | files |
| Tue, 09 Mar 2010 16:24:39 +0100 | Cezary Kaliszyk | A version of Fv that takes into account recursive and non-recursive bindings. | changeset | files |
| Tue, 09 Mar 2010 11:36:40 +0100 | Cezary Kaliszyk | Trying to prove that old alpha is the same as new recursive one. Lets still to do. | changeset | files |
| Tue, 09 Mar 2010 11:06:57 +0100 | Cezary Kaliszyk | fv_bi and alpha_bi | changeset | files |
| Tue, 09 Mar 2010 09:55:19 +0100 | Christian Urban | merged | changeset | files |
| Tue, 09 Mar 2010 09:54:58 +0100 | Christian Urban | added first test about new compat | changeset | files |
| Tue, 09 Mar 2010 09:38:49 +0100 | Cezary Kaliszyk | fv_compat | changeset | files |
| Tue, 09 Mar 2010 08:46:55 +0100 | Christian Urban | added another compat example | changeset | files |
| Mon, 08 Mar 2010 20:18:27 +0100 | Christian Urban | added a test-file for compatibility | changeset | files |
| Mon, 08 Mar 2010 16:11:42 +0100 | Christian Urban | added compat definitions to some examples | changeset | files |
| Mon, 08 Mar 2010 15:28:25 +0100 | Cezary Kaliszyk | Proper recognition of atoms and atom sets. | changeset | files |
| Mon, 08 Mar 2010 15:06:14 +0100 | Christian Urban | deleted comments about "weird" | changeset | files |
| Mon, 08 Mar 2010 15:01:26 +0100 | Christian Urban | merged | changeset | files |
| Mon, 08 Mar 2010 15:01:01 +0100 | Christian Urban | updated to new Isabelle | changeset | files |
| Mon, 08 Mar 2010 14:31:04 +0100 | Cezary Kaliszyk | Term5 written as nominal_datatype is the recursive let. | changeset | files |
| Mon, 08 Mar 2010 11:25:57 +0100 | Cezary Kaliszyk | With restricted_nominal=1, exp7 and exp8 work. Not sure about proving bn_rsp there. | changeset | files |
| Mon, 08 Mar 2010 11:12:15 +0100 | Cezary Kaliszyk | More fine-grained nominal restriction for debugging. | changeset | files |
| Mon, 08 Mar 2010 11:10:43 +0100 | Cezary Kaliszyk | Fix permutation addition. | changeset | files |
| Mon, 08 Mar 2010 10:33:55 +0100 | Cezary Kaliszyk | Update the comments | changeset | files |
| Mon, 08 Mar 2010 10:08:31 +0100 | Cezary Kaliszyk | Gather bindings with same binder, and generate only one permutation for them. | changeset | files |
| Mon, 08 Mar 2010 02:40:16 +0100 | Cezary Kaliszyk | Undo effects of simp. | changeset | files |
| Sun, 07 Mar 2010 21:30:57 +0100 | Christian Urban | merged | changeset | files |
| Sun, 07 Mar 2010 21:30:12 +0100 | Christian Urban | updated to renamings in Isabelle | changeset | files |
| Thu, 04 Mar 2010 15:56:58 +0100 | Christian Urban | merged | changeset | files |
| Thu, 04 Mar 2010 15:31:34 +0100 | Christian Urban | merged | changeset | files |
| Thu, 04 Mar 2010 15:31:21 +0100 | Christian Urban | more proofs in Abs and work on Core Haskell | changeset | files |
| Wed, 03 Mar 2010 19:10:40 +0100 | Christian Urban | added a lemma that permutations can be represented as sums of swapping | changeset | files |
| Fri, 05 Mar 2010 18:14:04 +0100 | Cezary Kaliszyk | Still unable to show supp=fv for let with one existential. | changeset | files |
| Fri, 05 Mar 2010 17:09:48 +0100 | Cezary Kaliszyk | Ported LF to the parser interface. | changeset | files |
| Fri, 05 Mar 2010 14:56:19 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Fri, 05 Mar 2010 14:55:21 +0100 | Cezary Kaliszyk | Lift fv and bn eqvts; no need to lift alpha_eqvt. | changeset | files |
| Fri, 05 Mar 2010 13:04:47 +0100 | Cezary Kaliszyk | Not much progress about the single existential let case. | changeset | files |
| Fri, 05 Mar 2010 10:23:40 +0100 | Cezary Kaliszyk | Fixed LF for one quantifier over 2 premises. | changeset | files |
| Fri, 05 Mar 2010 09:41:22 +0100 | Cezary Kaliszyk | Trying to fix the proofs for the single existential... So far failed. | changeset | files |
| Thu, 04 Mar 2010 18:57:23 +0100 | Cezary Kaliszyk | Lift distinct. | changeset | files |
| Thu, 04 Mar 2010 15:55:53 +0100 | Cezary Kaliszyk | Added lifting of pseudo-injectivity, commented out the code again and enabled the weird examples. | changeset | files |
| Thu, 04 Mar 2010 15:15:44 +0100 | Cezary Kaliszyk | Lift BV,FV,Permutations and injection :). | changeset | files |
| Thu, 04 Mar 2010 12:00:11 +0100 | Cezary Kaliszyk | Comment out Weird and Phd until we have an idea how to handle multiple permutations. Transp that works for multiple existentials. | changeset | files |
| Thu, 04 Mar 2010 11:16:36 +0100 | Cezary Kaliszyk | A version that just leaves the supp/\supp goal. Obviously not true. | changeset | files |
| Thu, 04 Mar 2010 10:59:52 +0100 | Cezary Kaliszyk | Prove symp and transp of weird without the supp /\ supp = {} assumption. | changeset | files |
| Wed, 03 Mar 2010 17:51:47 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Wed, 03 Mar 2010 17:49:34 +0100 | Cezary Kaliszyk | Experiments with proving weird transp | changeset | files |
| Wed, 03 Mar 2010 17:47:29 +0100 | Cezary Kaliszyk | Code for solving symp goals with multiple existentials. | changeset | files |
| Wed, 03 Mar 2010 15:28:25 +0100 | Cezary Kaliszyk | reflp for multiple quantifiers. | changeset | files |
| Wed, 03 Mar 2010 14:46:14 +0100 | Christian Urban | fixed mess in Test.thy | changeset | files |
| Wed, 03 Mar 2010 14:22:58 +0100 | Cezary Kaliszyk | Fix eqvt for multiple quantifiers. | changeset | files |
| Wed, 03 Mar 2010 12:48:05 +0100 | Christian Urban | only tuned | changeset | files |
| Wed, 03 Mar 2010 12:47:06 +0100 | Christian Urban | merged | changeset | files |
| Wed, 03 Mar 2010 12:45:55 +0100 | Christian Urban | start of paper - does not compile yet | changeset | files |
| Wed, 03 Mar 2010 11:50:25 +0100 | Christian Urban | added ACM style file for ICFP | changeset | files |
| Wed, 03 Mar 2010 11:42:15 +0100 | Cezary Kaliszyk | weird eqvt | changeset | files |
| Wed, 03 Mar 2010 10:39:43 +0100 | Cezary Kaliszyk | Add the supp intersection conditions. | changeset | files |
| Tue, 02 Mar 2010 21:43:27 +0100 | Cezary Kaliszyk | Comment out the part that does not work with 2 quantifiers. | changeset | files |
| Tue, 02 Mar 2010 21:10:04 +0100 | Cezary Kaliszyk | Fixes for the fv problem and alpha problem. | changeset | files |
| Tue, 02 Mar 2010 20:14:21 +0100 | Christian Urban | merged | changeset | files |
| Tue, 02 Mar 2010 20:11:56 +0100 | Christian Urban | preliinary test about alpha-weirdo | changeset | files |
| Tue, 02 Mar 2010 18:57:26 +0100 | Christian Urban | Another problem with permutations in alpha and possibly also in fv | changeset | files |
| Tue, 02 Mar 2010 18:48:20 +0100 | Christian Urban | potential problem with the phd-example, where two permutations are generated, but only one is used | changeset | files |
| Tue, 02 Mar 2010 19:48:44 +0100 | Cezary Kaliszyk | Some tests around Term4. Not sure how to fix the generated fv function. | changeset | files |
| Tue, 02 Mar 2010 17:48:56 +0100 | Cezary Kaliszyk | merge | changeset | files |
| Tue, 02 Mar 2010 17:48:41 +0100 | Cezary Kaliszyk | Porting from Lift to Parser; until defining the Quotient type. | changeset | files |
| Tue, 02 Mar 2010 17:11:58 +0100 | Cezary Kaliszyk | Add image_eqvt and atom_eqvt to eqvt bases. | changeset | files |
| Tue, 02 Mar 2010 17:11:19 +0100 | Cezary Kaliszyk | Include the raw eqvt lemmas. | changeset | files |
| Tue, 02 Mar 2010 16:04:48 +0100 | Christian Urban | merged | changeset | files |
| Tue, 02 Mar 2010 16:03:19 +0100 | Christian Urban | added some more examples from Peter Sewell's bestiary | changeset | files |
| Tue, 02 Mar 2010 15:13:00 +0100 | Cezary Kaliszyk | merge | changeset | files |