1 Automatically created functions: |
|
2 |
|
3 ty1_tyn.bn[simp] lifted equations for bn funs |
|
4 ty1_tyn.fv[simp] lifted equations for fv funs |
|
5 ty1_tyn.perm[simp] lifted permutation equations |
|
6 ty1_tyn.distinct[simp] lifted distincts |
|
7 ty1_tyn.eq_iff |
|
8 ty1_tyn.induct |
|
9 ty1_tyn.inducts |
|
10 instance ty1 and tyn :: fs |
|
11 ty1_tyn.supp empty when for too many bindings |
|
12 |
1 |
13 Parser should check that: |
2 Parser should check that: |
|
3 |
14 - types of bindings match types of binding functions |
4 - types of bindings match types of binding functions |
15 - fsets are not bound in lst bindings |
5 - fsets are not bound in lst bindings |
16 - bound arguments are not datatypes |
6 - bound arguments are not datatypes |
17 - binder is referred to by name and not by type |
7 - binder is referred to by name and not by type |
18 |
8 |
19 Smaller things: |
9 Smaller things: |
20 |
10 |
21 - lam.perm should be called permute_lam.simps (that is |
|
22 the convention from Nominal2) |
|
23 |
|
24 - maybe <type>_perm whould be called permute_<type>.simps; |
11 - maybe <type>_perm whould be called permute_<type>.simps; |
25 that would conform with the terminology in Nominal2 |
12 that would conform with the terminology in Nominal2 |
26 |
13 |
27 - we also need to lift the size function for nominal |
|
28 datatypes |
|
29 |
14 |
30 - Abs.thy contains lemmas for equivariance of the alphas; |
15 Other: |
31 they are not yet used anywhere |
|
32 |
|
33 Bigger things: |
|
34 |
|
35 - Parser adds syntax for raw datatype, but should |
|
36 add for lifted datatype. |
|
37 |
16 |
38 - nested recursion, like types "trm list" in a constructor |
17 - nested recursion, like types "trm list" in a constructor |
39 |
18 |
40 - define permute_bn automatically and prove properties of it |
19 - define permute_bn automatically and prove properties of it |
41 |
20 |
42 - prove renaming-of-binders lemmas |
21 - prove renaming-of-binders lemmas |
43 |
22 |
44 - strong induction rules |
23 - strong induction rules |
45 |
24 |
46 - check support equations for more bindings per constructor |
|
47 |
|
48 - For binding functions that call other binding functions |
|
49 the following are proved with cheat_tac: constr_rsp |
|
50 |
|
51 - store information about defined nominal datatypes, so that |
25 - store information about defined nominal datatypes, so that |
52 it can be used to define new types that depend on these |
26 it can be used to define new types that depend on these |
53 |
27 |
54 - make parser aware of recursive and of different versions of abs |
|
55 |
|
56 Less important: |
|
57 |
|
58 - fv_rsp uses 'blast' to show goals of the type: |
|
59 a u b = c u d ==> a u x u b = c u x u d |
|
60 |
|
61 When cleaning: |
|
62 |
|
63 - remove all 'PolyML.makestring'. |
|