Mercurial Mercurial > hg > nominal2 / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/Lambda.thy
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
Mon, 17 Jan 2011 12:37:37 +0000 Christian Urban removed old testing code from Lambda.thy file | diff | annotate
Sun, 09 Jan 2011 04:28:24 +0000 Christian Urban solved subgoals for depth and subst function file | diff | annotate
Thu, 06 Jan 2011 23:06:45 +0000 Christian Urban a modified function package where, as a test, True has been injected into the compatibility condictions file | diff | annotate
Thu, 06 Jan 2011 14:02:10 +0000 Christian Urban tuned file | diff | annotate
Fri, 31 Dec 2010 15:37:04 +0000 Christian Urban changed res keyword to set+ for restrictions; comment by a referee file | diff | annotate
Tue, 28 Dec 2010 19:51:25 +0000 Christian Urban automated all strong induction lemmas file | diff | annotate
Wed, 22 Dec 2010 09:13:25 +0000 Christian Urban properly exported strong exhaust theorem; cleaned up some examples file | diff | annotate
Wed, 10 Nov 2010 13:46:21 +0000 Christian Urban adapted to changes by Florian on the quotient package and removed local fix for function package file | diff | annotate
Wed, 29 Sep 2010 16:49:13 -0400 Christian Urban simplified exhaust proofs file | diff | annotate
Wed, 29 Sep 2010 04:42:37 -0400 Christian Urban test with induct_schema for simpler strong_ind proofs file | diff | annotate
Sun, 29 Aug 2010 13:36:03 +0800 Christian Urban renamed NewParser to Nominal2 file | diff | annotate
Fri, 27 Aug 2010 13:57:00 +0800 Christian Urban make copies of the "old" files file | diff | annotate
Fri, 27 Aug 2010 03:37:17 +0800 Christian Urban "isabelle make test" makes all major examples....they work up to supp theorems (excluding) file | diff | annotate
Thu, 26 Aug 2010 02:08:00 +0800 Christian Urban cleaned up (almost completely) the examples file | diff | annotate
Wed, 25 Aug 2010 22:55:42 +0800 Christian Urban automatic lifting file | diff | annotate
Wed, 25 Aug 2010 11:58:37 +0800 Christian Urban now every lemma lifts (even with type variables) file | diff | annotate
Wed, 25 Aug 2010 09:02:06 +0800 Christian Urban can now deal with type variables in nominal datatype definitions file | diff | annotate
Sat, 21 Aug 2010 17:55:42 +0800 Christian Urban nominal_datatypes with type variables do not work file | diff | annotate
Sat, 21 Aug 2010 16:20:10 +0800 Christian Urban changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default file | diff | annotate
Mon, 07 Jun 2010 11:43:01 +0200 Christian Urban work on transitivity proof file | diff | annotate
Fri, 21 May 2010 17:17:51 +0200 Cezary Kaliszyk Match_Lam defined on Quotient Level. file | diff | annotate
Fri, 21 May 2010 11:55:22 +0200 Cezary Kaliszyk More on Function-defined subst. file | diff | annotate
Fri, 21 May 2010 10:47:45 +0200 Cezary Kaliszyk merge file | diff | annotate
Fri, 21 May 2010 10:43:14 +0200 Cezary Kaliszyk Renamings. file | diff | annotate
Fri, 21 May 2010 10:47:07 +0200 Cezary Kaliszyk merge (non-trival) file | diff | annotate
Fri, 21 May 2010 10:45:29 +0200 Cezary Kaliszyk Previously uncommited direct subst definition changes. file | diff | annotate
Fri, 21 May 2010 10:44:07 +0200 Cezary Kaliszyk Function experiments file | diff | annotate
Wed, 19 May 2010 12:29:08 +0200 Cezary Kaliszyk more subst experiments file | diff | annotate
Wed, 19 May 2010 11:29:42 +0200 Cezary Kaliszyk More subst experminets file | diff | annotate
Tue, 18 May 2010 17:56:41 +0200 Cezary Kaliszyk more on subst file | diff | annotate
Tue, 18 May 2010 17:17:54 +0200 Cezary Kaliszyk Single variable substitution file | diff | annotate
Tue, 18 May 2010 17:06:21 +0200 Cezary Kaliszyk subst fix file | diff | annotate
Tue, 18 May 2010 15:58:52 +0200 Cezary Kaliszyk subst experiments file | diff | annotate
Wed, 12 May 2010 16:59:53 +0100 Christian Urban fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy file | diff | annotate
Tue, 11 May 2010 18:20:25 +0200 Cezary Kaliszyk Include raw permutation definitions in eqvt file | diff | annotate
Tue, 11 May 2010 17:16:57 +0200 Cezary Kaliszyk Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]' file | diff | annotate
Sun, 09 May 2010 12:26:10 +0100 Christian Urban cleaned up a bit the examples; added equivariance to all examples file | diff | annotate
Tue, 04 May 2010 11:22:22 +0200 Cezary Kaliszyk Move 2 more to NewParser file | diff | annotate
Mon, 26 Apr 2010 20:17:41 +0200 Christian Urban some changes to the paper file | diff | annotate
Mon, 26 Apr 2010 08:19:11 +0200 Christian Urban eliminated command so that all compiles file | diff | annotate
Mon, 26 Apr 2010 08:08:20 +0200 Christian Urban changed theorem_i to theorem....requires new Isabelle file | diff | annotate
Sun, 25 Apr 2010 09:13:16 +0200 Christian Urban tuned and cleaned file | diff | annotate
Fri, 16 Apr 2010 16:29:11 +0200 Christian Urban automatic proofs for equivariance of alphas file | diff | annotate
Fri, 16 Apr 2010 11:09:32 +0200 Cezary Kaliszyk Finished proof in Lambda.thy file | diff | annotate
Fri, 16 Apr 2010 10:46:50 +0200 Christian Urban attempt to manual prove eqvt for alpha file | diff | annotate
Fri, 16 Apr 2010 10:18:16 +0200 Christian Urban some tuning of eqvt-infrastructure file | diff | annotate
Wed, 14 Apr 2010 22:23:52 +0200 Christian Urban deleted offending [eqvt]-attribute in Abs; Lambda works again, but there is now a problem in CoreHaskell file | diff | annotate
Wed, 14 Apr 2010 16:05:58 +0200 Christian Urban tuned and removed dead code file | diff | annotate
Wed, 14 Apr 2010 14:41:54 +0200 Christian Urban added a library for basic nominal functions; separated nominal_eqvt file file | diff | annotate
Wed, 14 Apr 2010 13:21:11 +0200 Christian Urban first working version of the automatic equivariance procedure file | diff | annotate
Wed, 14 Apr 2010 10:29:34 +0200 Christian Urban preliminary tests file | diff | annotate
Tue, 13 Apr 2010 07:40:54 +0200 Christian Urban made everything to compile file | diff | annotate
Tue, 13 Apr 2010 00:53:32 +0200 Christian Urban some small tunings (incompleted work in Lambda.thy) file | diff | annotate
Mon, 12 Apr 2010 17:44:26 +0200 Christian Urban early ott paper file | diff | annotate
Mon, 12 Apr 2010 13:34:54 +0200 Christian Urban implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _ file | diff | annotate
Sun, 11 Apr 2010 22:48:49 +0200 Christian Urban fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _ file | diff | annotate
Sun, 11 Apr 2010 18:11:13 +0200 Christian Urban a few tests file | diff | annotate
Fri, 09 Apr 2010 21:51:01 +0200 Christian Urban changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac file | diff | annotate
Fri, 09 Apr 2010 11:08:05 +0200 Christian Urban renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper file | diff | annotate | base
less more (0) tip
nominal2