nominal2: TODO@cc0dcf248da3 (annotated)

1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	Smaller things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	- case names for "weak" induction rules (names of the
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	constructors); see page 61/62 and 170 in Tutorial
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	- <type>_perm rules should be added to the simplifier;
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	maybe <type>_perm whould be called permute_<type>.simps;
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	8	that would conform with the terminology in Nominal2
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	9
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	10	- <type>_fv / <type>_bn / <type>_distinct should also be
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	11	added to the simplifier
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	12
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	13
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	14	Bigger things:
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	15
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	16	- nested recursion, like types "trm list" in a constructor
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	17
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	- strong induction rules
7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	19
1502 cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	20	- show support equations
1501 7e7dc267ae6b added TODO Christian Urban <urbanc@in.tum.de> parents: diff changeset	21
1502 cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	22	- automate the proofs that are currently proved with sorry:
cc0dcf248da3 Which proofs need a 'sorry'. Cezary Kaliszyk <kaliszyk@in.tum.de> parents: 1501 diff changeset	23	alpha_equivp, fv_rsp, alpha_bn_rsp, alpha_bn_reflp

author	Cezary Kaliszyk <kaliszyk@in.tum.de>
	Thu, 18 Mar 2010 10:12:41 +0100
changeset 1502	cc0dcf248da3
parent 1501	7e7dc267ae6b
child 1503	8639077e0f43
permissions	-rw-r--r--