Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Lambda.thy
Fri, 22 Jul 2011 11:37:16 +0100 Christian Urban completed the eqvt-proofs for functions; they are stored under the name function_name.eqvt and added to the eqvt-list file | diff | annotate
Tue, 19 Jul 2011 02:30:05 +0100 Christian Urban preliminary version of automatically generation the eqvt-lemmas for functions defined with nominal_primrec file | diff | annotate
Tue, 19 Jul 2011 01:40:36 +0100 Christian Urban generated the partial eqvt-theorem for functions file | diff | annotate
Mon, 18 Jul 2011 17:40:13 +0100 Christian Urban added a flag (eqvt) to termination proofs arising fron nominal_primrecs file | diff | annotate
Mon, 18 Jul 2011 10:50:21 +0100 Christian Urban moved eqvt for Option.map file | diff | annotate
Tue, 05 Jul 2011 23:47:20 +0200 Christian Urban added some relatively simple examples from paper by Norrish file | diff | annotate
Tue, 05 Jul 2011 18:42:34 +0200 Christian Urban changed bind to binds in specifications; bind will cause trouble with Monad_Syntax file | diff | annotate
Tue, 05 Jul 2011 16:22:18 +0200 Christian Urban made the tests go through again file | diff | annotate
Tue, 05 Jul 2011 04:23:33 +0200 Christian Urban merged file | diff | annotate
Tue, 05 Jul 2011 04:18:45 +0200 Christian Urban exported various FCB-lemmas to a separate file file | diff | annotate
Tue, 05 Jul 2011 10:13:34 +0900 Cezary Kaliszyk Express trans_db with Option.map and Option.bind. Possibly mbind is a copy of bind? file | diff | annotate
Tue, 05 Jul 2011 09:28:16 +0900 Cezary Kaliszyk Define a version of aux only for same binders. Completeness is fine. file | diff | annotate
Tue, 05 Jul 2011 09:26:20 +0900 Cezary Kaliszyk Move If / Let with 'True' to the end of Lambda file | diff | annotate
Mon, 04 Jul 2011 23:54:05 +0200 Christian Urban added an example that recurses over two arguments; the interesting proof-obligation is not yet done file | diff | annotate
Tue, 28 Jun 2011 00:30:30 +0100 Christian Urban copied all work to Lambda.thy; had to derive a special version of fcb1 for concrete atom file | diff | annotate
Sun, 26 Jun 2011 17:55:22 +0100 Christian Urban another change to the fcb2; this is needed in order to get all proofs through in Lambda.thy file | diff | annotate
Thu, 23 Jun 2011 22:21:43 +0100 Christian Urban the simplifier can simplify "sort (atom a)" if a is a concrete atom type declared with atom_decl file | diff | annotate
Wed, 22 Jun 2011 12:18:22 +0100 Christian Urban some rudimentary infrastructure for storing data about nominal datatypes file | diff | annotate
Thu, 16 Jun 2011 20:07:03 +0100 Christian Urban got rid of the boolean flag in the raw_equivariance function file | diff | annotate
Thu, 16 Jun 2011 12:12:25 +0100 Christian Urban added a test that every function must be of pt-sort file | diff | annotate
Wed, 15 Jun 2011 22:36:59 +0100 Christian Urban added size-lemmas to simplifier; as a result termination can be proved by the standard lexicographic_order method file | diff | annotate
Wed, 15 Jun 2011 09:50:53 +0900 Cezary Kaliszyk Some TODOs file | diff | annotate
Fri, 10 Jun 2011 15:52:17 +0900 Cezary Kaliszyk Move working examples before non-working ones file | diff | annotate
Fri, 10 Jun 2011 15:45:49 +0900 Cezary Kaliszyk Optimized proofs and removed some garbage. file | diff | annotate
Fri, 10 Jun 2011 15:30:09 +0900 Cezary Kaliszyk Slightly modify fcb for list1 and put in common place. file | diff | annotate
Thu, 09 Jun 2011 15:34:51 +0900 Cezary Kaliszyk Eval can be defined with additional freshness file | diff | annotate
Thu, 09 Jun 2011 15:03:58 +0900 Cezary Kaliszyk Minor simplification file | diff | annotate
Wed, 08 Jun 2011 12:30:56 +0100 Christian Urban merged file | diff | annotate
Wed, 08 Jun 2011 12:30:46 +0100 Christian Urban merged file | diff | annotate
Wed, 08 Jun 2011 07:06:20 +0900 Cezary Kaliszyk Simplify ln-trans proof file | diff | annotate
Wed, 08 Jun 2011 07:02:52 +0900 Cezary Kaliszyk cbvs can be easily defined without an invariant file | diff | annotate
Tue, 07 Jun 2011 20:58:00 +0100 Christian Urban defined the "count-bound-variables-occurences" function which has an accumulator like trans file | diff | annotate
Tue, 07 Jun 2011 17:45:38 +0100 Christian Urban merged file | diff | annotate
Tue, 07 Jun 2011 23:42:12 +0900 Cezary Kaliszyk remove garbage (proofs that assumes the invariant outside function) file | diff | annotate
Tue, 07 Jun 2011 23:38:39 +0900 Cezary Kaliszyk Proof of trans with invariant file | diff | annotate
Tue, 07 Jun 2011 10:40:06 +0100 Christian Urban cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file file | diff | annotate
Tue, 07 Jun 2011 08:52:59 +0100 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 file | diff | annotate
Sun, 05 Jun 2011 21:14:23 +0100 Christian Urban added an option for an invariant (at the moment only a stub) file | diff | annotate
Sat, 04 Jun 2011 09:07:50 +0900 Cezary Kaliszyk Finish and test the locale approach file | diff | annotate
Fri, 03 Jun 2011 12:46:23 +0100 Christian Urban recursion combinator inside a locale file | diff | annotate
Thu, 02 Jun 2011 22:24:33 +0900 Cezary Kaliszyk finished the missing obligations file | diff | annotate
Thu, 02 Jun 2011 12:14:03 +0100 Christian Urban merged file | diff | annotate
Thu, 02 Jun 2011 12:09:31 +0100 Christian Urban a test with a recursion combinator defined on top of nominal_primrec file | diff | annotate
Thu, 02 Jun 2011 16:41:09 +0900 Cezary Kaliszyk Use FCB to simplify proof file | diff | annotate
Wed, 01 Jun 2011 22:55:14 +0100 Christian Urban hopefully final fix for ho-functions file | diff | annotate
Wed, 01 Jun 2011 21:03:30 +0100 Christian Urban first test to fix the problem with free variables file | diff | annotate
Wed, 01 Jun 2011 13:41:30 +0900 Cezary Kaliszyk DB translation using index; easier to reason about. file | diff | annotate
Wed, 01 Jun 2011 13:35:37 +0900 Cezary Kaliszyk Problem: free variables in the goal file | diff | annotate
Wed, 01 Jun 2011 11:01:39 +0900 Cezary Kaliszyk fixed previous commit file | diff | annotate
Wed, 01 Jun 2011 10:59:07 +0900 Cezary Kaliszyk equivariance of db_trans file | diff | annotate
Tue, 31 May 2011 12:22:28 +0100 Christian Urban fixed the problem with cps-like functions file | diff | annotate
Tue, 31 May 2011 14:12:31 +0900 Cezary Kaliszyk DeBruijn translation in a simplifier friendly way file | diff | annotate
Tue, 31 May 2011 13:25:35 +0900 Cezary Kaliszyk map_term can be defined when equivariance is assumed file | diff | annotate
Tue, 31 May 2011 13:21:00 +0900 Cezary Kaliszyk map_term is not a function the way it is defined file | diff | annotate
Tue, 31 May 2011 12:59:10 +0900 Cezary Kaliszyk Defined translation from nominal to de-Bruijn; with a freshness condition for the lambda case. file | diff | annotate
Tue, 31 May 2011 12:54:21 +0900 Cezary Kaliszyk Simple eqvt proofs with perm_simps for clarity file | diff | annotate
Tue, 31 May 2011 00:17:22 +0100 Christian Urban functions involving if and case do not throw exceptions anymore; but eqvt_at assumption has now a precondition file | diff | annotate
Wed, 25 May 2011 21:38:50 +0200 Christian Urban added eq_iff and distinct lemmas of nominal datatypes to the simplifier file | diff | annotate
Sat, 14 May 2011 10:16:16 +0100 Christian Urban added a problem with inductive_cases (reported by Randy) file | diff | annotate
Tue, 03 May 2011 15:39:30 +0100 Christian Urban added two mutual recursive inductive definitions file | diff | annotate
less more (0) -100 -60 tip
nominal2