|
1501
|
1 |
Smaller things:
|
|
|
2 |
|
|
|
3 |
- case names for "weak" induction rules (names of the
|
|
|
4 |
constructors); see page 61/62 and 170 in Tutorial
|
|
|
5 |
|
|
|
6 |
- <type>_perm rules should be added to the simplifier;
|
|
|
7 |
maybe <type>_perm whould be called permute_<type>.simps;
|
|
|
8 |
that would conform with the terminology in Nominal2
|
|
|
9 |
|
|
|
10 |
- <type>_fv / <type>_bn / <type>_distinct should also be
|
|
|
11 |
added to the simplifier
|
|
|
12 |
|
|
|
13 |
|
|
|
14 |
Bigger things:
|
|
|
15 |
|
|
|
16 |
- nested recursion, like types "trm list" in a constructor
|
|
|
17 |
|
|
|
18 |
- strong induction rules
|
|
|
19 |
|
|
|
20 |
|
|
|
21 |
What are the proofs that are still proved by sorry? |