1 Highest Priority |
1 Highest Priority |
2 ================ |
2 ================ |
3 |
3 |
4 - better lookup mechanism for quotient definition |
4 - better lookup mechanism for quotient definition |
5 (see fixme in quotient_term.ML) |
5 (see fixme in quotient_term.ML) |
6 |
|
7 - check needs to be fixed in mk_resp_arg (quotient_term.ML), |
|
8 see test for (_, Const _) |
|
9 |
|
10 - clever code in quotiet_tacs.ML needs to be turned into |
|
11 boring code |
|
12 |
|
13 - comment about regularize tactic needs to be adapted |
|
14 |
|
15 - Check all the places where we do "handle _" |
|
16 (They make code changes very difficult: I sat 1/2 |
|
17 a day over a simplification of calculate_inst before |
|
18 I understood things; the reason was that my exceptions |
|
19 where caught by the catch all. There is no problem |
|
20 with throwing and handling exceptions...it just must |
|
21 be clear who throws what and what is thrown.) |
|
22 |
|
23 |
6 |
24 Higher Priority |
7 Higher Priority |
25 =============== |
8 =============== |
26 |
9 |
27 - If the user defines twice the same quotient constant, |
10 - If the user defines twice the same quotient constant, |
32 in quotient_def raises a bind exception. |
15 in quotient_def raises a bind exception. |
33 |
16 |
34 - If the constant definition gives the wrong definition |
17 - If the constant definition gives the wrong definition |
35 term, one gets a cryptic message about absrep_fun |
18 term, one gets a cryptic message about absrep_fun |
36 |
19 |
37 - have FSet.thy to have a simple infrastructure for |
|
38 finite sets (syntax should be \<lbrace> \<rbrace>, |
|
39 look at Set.thy how syntax is been introduced) |
|
40 |
|
41 - Handle theorems that include Ball/Bex. For this, would |
20 - Handle theorems that include Ball/Bex. For this, would |
42 it help if we introduced separate Bex and Ball constants |
21 it help if we introduced separate Bex and Ball constants |
43 for quotienting? |
22 for quotienting? |
44 |
23 |
45 - The user should be able to give quotient_respects and |
24 - The user should be able to give quotient_respects and |
46 preserves theorems in a more natural form. |
25 preserves theorems in a more natural form. |
47 |
26 |
48 |
27 |
49 Lower Priority |
28 Lower Priority |
50 ============== |
29 ============== |
51 |
|
52 - Maybe a quotient_definition should already require |
|
53 a proof of the respectfulness (in this way one |
|
54 already excludes non-sensical definitions) |
|
55 |
30 |
56 - accept partial equivalence relations |
31 - accept partial equivalence relations |
57 |
32 |
58 - think about what happens if things go wrong (like |
33 - think about what happens if things go wrong (like |
59 theorem cannot be lifted) / proper diagnostic |
34 theorem cannot be lifted) / proper diagnostic |