nominal2: TODO@b39108f42638 (annotated)

1555 73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	1	Automatically created functions:
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	2
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	3	ty1_tyn.bn[simp] lifted equations for bn funs
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	4	ty1_tyn.fv[simp] lifted equations for fv funs
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	5	ty1_tyn.perm[simp] lifted permutation equations
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	6	ty1_tyn.distinct[simp] lifted distincts
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	7	ty1_tyn.eq_iff
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	8	ty1_tyn.induct
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	9	ty1_tyn.inducts
73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	10	instance ty1 and tyn :: fs
1573 b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	11	ty1_tyn.supp empty when for too many bindings
1555 73992021c8f0 Described automatically created funs. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1527 diff changeset	12
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	13	Smaller things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	14
1510 be911e869fde Added fv,bn,distinct,perm to the simplifier. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1504 diff changeset	15	- maybe <type>_perm whould be called permute_<type>.simps;
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	that would conform with the terminology in Nominal2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
1527 e1c74b864b1b added item about size functions Christian Urban <urbanc@in.tum.de> parents: 1516 diff changeset	18	- we also need to lift the size function for nominal
e1c74b864b1b added item about size functions Christian Urban <urbanc@in.tum.de> parents: 1516 diff changeset	19	datatypes
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	20
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	21	Bigger things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	22
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	23	- nested recursion, like types "trm list" in a constructor
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	24
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	- strong induction rules
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	26
1561 c3dca6e600c8 Use 'alpha_bn_refl' to get rid of one of the sorrys. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1555 diff changeset	27	- check support equations for more bindings per constructor
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	28
1502 cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	29	- automate the proofs that are currently proved with sorry:
1573 b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	30	alpha_equivp, alpha_bn_rsp
1503 8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	31
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	32	- store information about defined nominal datatypes, so that
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	33	it can be used to define new types that depend on these
8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	34
1504 f685be70a464 fv_bn may need to call other fv_bns. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1503 diff changeset	35	- make parser aware of bn functions that call other bn functions
f685be70a464 fv_bn may need to call other fv_bns. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1503 diff changeset	36	and reflect it in the datastructure passed to Fv/Alpha generation
f685be70a464 fv_bn may need to call other fv_bns. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1503 diff changeset	37
1503 8639077e0f43 Update TODO. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1502 diff changeset	38	- make parser aware of recursive and of different versions of abs
1573 b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	39
b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	40	Less important:
b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	41
b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	42	- fv_rsp uses 'blast' to show goals of the type:
b39108f42638 fv_rsp proved automatically. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1561 diff changeset	43	a u b = c u d ==> a u x u b = c u x u d

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Mon, 22 Mar 2010 14:07:07 +0100
changeset 1573	b39108f42638
parent 1561	c3dca6e600c8
child 1576	7b8f570b2450
permissions	-rw-r--r--