equal
deleted
inserted
replaced
1 Higher Priority |
1 Higher Priority |
2 =============== |
2 =============== |
3 |
|
4 - handling constant definitions is ugly at the moment |
|
5 |
3 |
6 - if the constant definition gives the wrong definition |
4 - if the constant definition gives the wrong definition |
7 term, one gets a cryptic message about get_fun |
5 term, one gets a cryptic message about get_fun |
8 |
6 |
9 - have FSet.thy to have a simple infrastructure for |
7 - have FSet.thy to have a simple infrastructure for |
12 |
10 |
13 - think about what happens if things go wrong (like |
11 - think about what happens if things go wrong (like |
14 theorem cannot be lifted) / proper diagnostic |
12 theorem cannot be lifted) / proper diagnostic |
15 messages for the user |
13 messages for the user |
16 |
14 |
17 - Ask Peter and Michael for challenging examples |
|
18 And for examples where it is useful to lift types |
|
19 over a relation being only a partial equivalence |
|
20 |
|
21 - Handle theorems that include Ball/Bex |
15 - Handle theorems that include Ball/Bex |
22 |
16 |
23 - Test theorems with abstractions |
17 - quotient_respects and preserves in a natural form. |
24 |
|
25 |
|
26 |
|
27 |
18 |
28 |
19 |
29 Lower Priority |
20 Lower Priority |
30 ============== |
21 ============== |
31 |
22 |
32 - allow the user to provide the rsp lemmas in a more |
23 - inductions from the datatype package have a strange |
33 natural form |
24 order of quantifiers in assumptions. |
|
25 |
|
26 - wrapper that translates an an original theorem given |
|
27 a list of quotient_types as an attribute |
|
28 |
|
29 |
|
30 |
34 |
31 |
35 - find clean ways how to write down the "mathematical" |
32 - find clean ways how to write down the "mathematical" |
36 procedure for a possible submission (Peter submitted |
33 procedure for a possible submission (Peter submitted |
37 his work only to TPHOLs 2005...we would have to go |
34 his work only to TPHOLs 2005...we would have to go |
38 maybe for the Journal of Formalised Mathematics) |
35 maybe for the Journal of Formalised Mathematics) |
41 to make Markus happy |
38 to make Markus happy |
42 |
39 |
43 - add tests for adding theorems to the various thm lists |
40 - add tests for adding theorems to the various thm lists |
44 |
41 |
45 |
42 |
46 |
|
47 - Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc. |
|
48 |
|
49 - Check all the places where we do "handle _" |
43 - Check all the places where we do "handle _" |
50 |
44 |
51 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
45 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
52 Call it 'quotient_type' |
46 Call it 'quotient_type' |