| 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
|
| Mon, 18 Jul 2011 17:40:13 +0100 |
Christian Urban |
added a flag (eqvt) to termination proofs arising fron nominal_primrecs
|
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
|
| Wed, 22 Jun 2011 13:40:25 +0100 |
Christian Urban |
deleted some dead code
|
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 23:11:50 +0900 |
Cezary Kaliszyk |
Fix
|
file |
diff |
annotate
|
| Thu, 16 Jun 2011 11:03:01 +0100 |
Christian Urban |
all tests work again
|
file |
diff |
annotate
|
| Wed, 15 Jun 2011 09:25:36 +0900 |
Cezary Kaliszyk |
TypeSchemes work with 'default'.
|
file |
diff |
annotate
|
| Tue, 14 Jun 2011 14:07:07 +0100 |
Christian Urban |
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
|
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 11:10:41 +0900 |
Cezary Kaliszyk |
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 09:44:51 +0900 |
Cezary Kaliszyk |
More experiments with 'default'
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 21:32:35 +0900 |
Cezary Kaliszyk |
Issue with 'default'
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 12:30:56 +0100 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 08:44:01 +0100 |
Christian Urban |
using the option "default" the function package allows one to give an explicit default value
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 17:52:06 +0900 |
Cezary Kaliszyk |
Simpler proof of TypeSchemes/substs
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 17:25:54 +0900 |
Cezary Kaliszyk |
Simplify fcb_res
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 09:56:39 +0900 |
Cezary Kaliszyk |
FCB for res binding and simplified proof of subst for type schemes
|
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
|
| Thu, 02 Jun 2011 10:11:50 +0900 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| Thu, 02 Jun 2011 10:09:23 +0900 |
Cezary Kaliszyk |
Remove SMT
|
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 16:13:42 +0900 |
Cezary Kaliszyk |
proved subst for All constructor in type schemes.
|
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, 19 Feb 2011 09:31:22 +0900 |
Cezary Kaliszyk |
typeschemes/subst
|
file |
diff |
annotate
|
| Thu, 17 Feb 2011 17:02:25 +0900 |
Cezary Kaliszyk |
further experiments with typeschemes subst
|
file |
diff |
annotate
|
| Mon, 07 Feb 2011 15:59:37 +0000 |
Christian Urban |
cleaned up the experiments so that the tests go through
|
file |
diff |
annotate
|
| Tue, 01 Feb 2011 08:57:50 +0900 |
Cezary Kaliszyk |
Experiments with substitution on set+
|
file |
diff |
annotate
|
| Sun, 30 Jan 2011 09:57:37 +0900 |
Cezary Kaliszyk |
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
|
file |
diff |
annotate
|
| Sat, 29 Jan 2011 14:26:47 +0900 |
Cezary Kaliszyk |
Experiments with functions
|
file |
diff |
annotate
|
| Thu, 27 Jan 2011 20:19:13 +0100 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
| Tue, 25 Jan 2011 18:58:26 +0100 |
Christian Urban |
made eqvt-proof explicit in the function definitions
|
file |
diff |
annotate
|
| Tue, 18 Jan 2011 21:26:58 +0100 |
Christian Urban |
some tryes about substitution over type-schemes
|
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 21:13:44 +0000 |
Christian Urban |
tuned examples
|
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
|
| Thu, 16 Dec 2010 08:42:48 +0000 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
| Sun, 14 Nov 2010 11:46:39 +0000 |
Christian Urban |
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
|
file |
diff |
annotate
|
| Sat, 06 Nov 2010 06:18:41 +0000 |
Christian Urban |
added a test about subtyping; disabled two tests, because of problem with function package
|
file |
diff |
annotate
|
| Thu, 14 Oct 2010 04:14:22 +0100 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 05:56:11 -0400 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 12:19:17 -0400 |
Christian Urban |
added postprocessed fresh-lemmas for constructors
|
file |
diff |
annotate
|
| Sat, 25 Sep 2010 08:28:45 -0400 |
Christian Urban |
cleaned up two examples
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 21:52:45 +0800 |
Christian Urban |
introduced a general procedure for structural inductions; simplified reflexivity proof
|
file |
diff |
annotate
|
| Sat, 04 Sep 2010 06:23:31 +0800 |
Christian Urban |
moved a proof to Abs
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 13:36:03 +0800 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 01:45:07 +0800 |
Christian Urban |
added fs-instance proofs
|
file |
diff |
annotate
|
| Sun, 29 Aug 2010 01:17:36 +0800 |
Christian Urban |
added proofs for fsupp properties
|
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
|
| 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
|
| Sun, 27 Jun 2010 21:41:21 +0100 |
Christian Urban |
fixed according to changes in quotient
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 11:37:51 +0200 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
| Tue, 25 May 2010 18:38:52 +0200 |
Cezary Kaliszyk |
Substitution Lemma for TypeSchemes.
|
file |
diff |
annotate
|
| Tue, 25 May 2010 17:29:05 +0200 |
Cezary Kaliszyk |
Simplified the proof
|
file |
diff |
annotate
|
| Tue, 25 May 2010 17:09:29 +0200 |
Cezary Kaliszyk |
A lemma about substitution in TypeSchemes.
|
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
|