8 see test for (_, Const _) |
8 see test for (_, Const _) |
9 |
9 |
10 - clever code in quotiet_tacs.ML needs to be turned into |
10 - clever code in quotiet_tacs.ML needs to be turned into |
11 boring code |
11 boring code |
12 |
12 |
13 - comment about regularize tactic eeds to be adapted |
13 - comment about regularize tactic needs to be adapted |
14 |
14 |
15 - Check all the places where we do "handle _" |
15 - Check all the places where we do "handle _" |
16 (They make code changes very difficult: I sat 1/2 |
16 (They make code changes very difficult: I sat 1/2 |
17 a day over simplification of calculate_inst before |
17 a day over a simplification of calculate_inst before |
18 I understood things; the reason was that my exceptions |
18 I understood things; the reason was that my exceptions |
19 where caught by the catch all. There is no problem |
19 where caught by the catch all. There is no problem |
20 with throwing and handling exceptions...it just must |
20 with throwing and handling exceptions...it just must |
21 be clear who throws what ad what is thrown.) |
21 be clear who throws what and what is thrown.) |
|
22 |
22 |
23 |
23 Higher Priority |
24 Higher Priority |
24 =============== |
25 =============== |
25 |
26 |
26 - if the constant definition gives the wrong definition |
27 - If the user defines twice the same quotient constant, |
|
28 for example funion, then the line |
|
29 |
|
30 val Free (lhs_str, lhs_ty) = lhs |
|
31 |
|
32 in quotient_def raises a bind exception. |
|
33 |
|
34 - If the constant definition gives the wrong definition |
27 term, one gets a cryptic message about absrep_fun |
35 term, one gets a cryptic message about absrep_fun |
28 |
36 |
29 - have FSet.thy to have a simple infrastructure for |
37 - have FSet.thy to have a simple infrastructure for |
30 finite sets (syntax should be \<lbrace> \<rbrace>, |
38 finite sets (syntax should be \<lbrace> \<rbrace>, |
31 look at Set.thy how syntax is been introduced) |
39 look at Set.thy how syntax is been introduced) |
32 |
40 |
33 - Handle theorems that include Ball/Bex. Would it help |
41 - Handle theorems that include Ball/Bex. For this, would |
34 if we introduced separate Bex and Ball constants for |
42 it help if we introduced separate Bex and Ball constants |
35 quotienting? |
43 for quotienting? |
36 |
44 |
37 - user should be able to give quotient_respects and |
45 - The user should be able to give quotient_respects and |
38 preserves theorems in a more natural form. |
46 preserves theorems in a more natural form. |
39 |
|
40 |
47 |
41 |
48 |
42 Lower Priority |
49 Lower Priority |
43 ============== |
50 ============== |
44 |
51 |
53 messages for the user |
60 messages for the user |
54 |
61 |
55 - inductions from the datatype package have a strange |
62 - inductions from the datatype package have a strange |
56 order of quantifiers in assumptions. |
63 order of quantifiers in assumptions. |
57 |
64 |
58 - wrapper that translates an an original theorem given |
65 - wrapper for lifting ... to be used as an attribute |
59 a list of quotient_types as an attribute |
|
60 |
66 |
61 - find clean ways how to write down the "mathematical" |
67 - find clean ways how to write down the "mathematical" |
62 procedure for a possible submission (Peter submitted |
68 procedure for a possible submission (Peter submitted |
63 his work only to TPHOLs 2005...we would have to go |
69 his work only to TPHOLs 2005...we would have to go |
64 maybe for the Journal of Formalised Mathematics) |
70 maybe for the Journal of Formalised Mathematics) |
65 |
71 |
66 - use lower-case letters where appropriate in order |
|
67 to make Markus happy |
|
68 |
|
69 - add tests for adding theorems to the various thm lists |
72 - add tests for adding theorems to the various thm lists |
70 |
|
71 - We shouldn't use the command 'quotient' as this shadows Larry's quotient. |
|
72 Call it 'quotient_type' |
|
73 |
73 |
74 - Maybe quotient and equiv theorems like the ones for |
74 - Maybe quotient and equiv theorems like the ones for |
75 [QuotList, QuotOption, QuotPair...] could be automatically |
75 [QuotList, QuotOption, QuotPair...] could be automatically |
76 proven? |
76 proven? |
77 |
77 |