equal
deleted
inserted
replaced
6 ty1_tyn.distinct[simp] lifted distincts |
6 ty1_tyn.distinct[simp] lifted distincts |
7 ty1_tyn.eq_iff |
7 ty1_tyn.eq_iff |
8 ty1_tyn.induct |
8 ty1_tyn.induct |
9 ty1_tyn.inducts |
9 ty1_tyn.inducts |
10 instance ty1 and tyn :: fs |
10 instance ty1 and tyn :: fs |
11 ty1_tyn.supp for too many bindings empty |
11 ty1_tyn.supp empty when for too many bindings |
12 |
12 |
13 Smaller things: |
13 Smaller things: |
14 |
14 |
15 - maybe <type>_perm whould be called permute_<type>.simps; |
15 - maybe <type>_perm whould be called permute_<type>.simps; |
16 that would conform with the terminology in Nominal2 |
16 that would conform with the terminology in Nominal2 |
25 - strong induction rules |
25 - strong induction rules |
26 |
26 |
27 - check support equations for more bindings per constructor |
27 - check support equations for more bindings per constructor |
28 |
28 |
29 - automate the proofs that are currently proved with sorry: |
29 - automate the proofs that are currently proved with sorry: |
30 alpha_equivp, fv_rsp, alpha_bn_rsp |
30 alpha_equivp, alpha_bn_rsp |
31 |
31 |
32 - store information about defined nominal datatypes, so that |
32 - store information about defined nominal datatypes, so that |
33 it can be used to define new types that depend on these |
33 it can be used to define new types that depend on these |
34 |
|
35 - make 3 versions of Abs |
|
36 |
34 |
37 - make parser aware of bn functions that call other bn functions |
35 - make parser aware of bn functions that call other bn functions |
38 and reflect it in the datastructure passed to Fv/Alpha generation |
36 and reflect it in the datastructure passed to Fv/Alpha generation |
39 |
37 |
40 - make parser aware of recursive and of different versions of abs |
38 - make parser aware of recursive and of different versions of abs |
|
39 |
|
40 Less important: |
|
41 |
|
42 - fv_rsp uses 'blast' to show goals of the type: |
|
43 a u b = c u d ==> a u x u b = c u x u d |