|
1555
|
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
|
|
1573
|
11 |
ty1_tyn.supp empty when for too many bindings
|
|
1555
|
12 |
|
|
1501
|
13 |
Smaller things:
|
|
|
14 |
|
|
1510
|
15 |
- maybe <type>_perm whould be called permute_<type>.simps;
|
|
1501
|
16 |
that would conform with the terminology in Nominal2
|
|
|
17 |
|
|
1527
|
18 |
- we also need to lift the size function for nominal
|
|
|
19 |
datatypes
|
|
1501
|
20 |
|
|
|
21 |
Bigger things:
|
|
|
22 |
|
|
|
23 |
- nested recursion, like types "trm list" in a constructor
|
|
|
24 |
|
|
1649
|
25 |
- define permute_bn automatically and prove properties of it
|
|
|
26 |
|
|
|
27 |
- prove renaming-of-binders lemmas
|
|
|
28 |
|
|
1501
|
29 |
- strong induction rules
|
|
|
30 |
|
|
1561
|
31 |
- check support equations for more bindings per constructor
|
|
1501
|
32 |
|
|
1649
|
33 |
- For binding functions that call other binding functions
|
|
|
34 |
the following are proved with cheat_tac:
|
|
|
35 |
bn_eqvt, bn_rsp, alpha_bn_rsp, constr_rsp
|
|
1503
|
36 |
|
|
|
37 |
- store information about defined nominal datatypes, so that
|
|
|
38 |
it can be used to define new types that depend on these
|
|
|
39 |
|
|
|
40 |
- make parser aware of recursive and of different versions of abs
|
|
1573
|
41 |
|
|
|
42 |
Less important:
|
|
|
43 |
|
|
|
44 |
- fv_rsp uses 'blast' to show goals of the type:
|
|
|
45 |
a u b = c u d ==> a u x u b = c u x u d
|