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
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
Tue, 03 May 2011 13:09:08 +0100 Christian Urban proved that lfp is equivariant (that simplifies equivariance proofs of inductively defined predicates) file | diff | annotate
Mon, 18 Apr 2011 15:57:45 +0100 Christian Urban merged file | diff | annotate
Mon, 18 Apr 2011 15:56:07 +0100 Christian Urban added permute_pure back into the nominal_inductive procedure; updated to Isabelle 17 April file | diff | annotate
Fri, 15 Apr 2011 15:20:56 +0900 Cezary Kaliszyk New way of forward elimination of Abs1_eq and simplifications of the function obligation proofs. file | diff | annotate
Wed, 13 Apr 2011 13:41:52 +0100 Christian Urban introduced framework for finetuning eqvt-rules; this solves problem with permute_pure called in nominal_inductive file | diff | annotate
Wed, 23 Feb 2011 11:11:02 +0900 Cezary Kaliszyk Reduce the definition of trans to FCB; test that FCB can be proved with simp rules. file | diff | annotate
Tue, 01 Feb 2011 09:07:55 +0900 Cezary Kaliszyk Only one of the subgoals is needed file | diff | annotate
Tue, 25 Jan 2011 18:58:26 +0100 Christian Urban made eqvt-proof explicit in the function definitions file | diff | annotate
Wed, 19 Jan 2011 19:41:50 +0100 Christian Urban added obtain_fresh lemma; tuned Lambda.thy file | diff | annotate
Wed, 19 Jan 2011 18:56:28 +0100 Christian Urban ported some of the old proofs to serve as testcases file | diff | annotate
Wed, 19 Jan 2011 07:06:47 +0100 Christian Urban defined height as a function that returns an integer file | diff | annotate
Tue, 18 Jan 2011 19:27:30 +0100 Christian Urban defined properly substitution file | diff | annotate
Tue, 18 Jan 2011 11:02:57 +0100 Christian Urban the function translating lambda terms to locally nameless lambda terms; still needs a stronger abs_eq_iff lemma...at the moment only proved for restrictions file | diff | annotate
Mon, 17 Jan 2011 17:20:21 +0100 Christian Urban added a translation function from lambda-terms to deBruijn terms (equivariance fails at the moment) file | diff | annotate
Mon, 17 Jan 2011 15:12:03 +0100 Christian Urban added a few examples of functions to Lambda.thy file | diff | annotate
less more (0) -100 -60 tip
nominal2