6 |
6 |
7 |
7 |
8 Higher Priority |
8 Higher Priority |
9 =============== |
9 =============== |
10 |
10 |
11 |
|
12 - Also, in the interest of making nicer generated documentation, you |
|
13 might want to change all your "section" headings in Quotient.thy to |
|
14 "subsection", and add a "header" statement to the top of the file. |
|
15 Otherwise, each "section" gets its own chapter in the generated pdf, |
|
16 when the rest of HOL has one chapter per theory file (the chapter |
|
17 title comes from the "header" statement). |
|
18 |
|
19 - If the constant definition gives the wrong definition |
11 - If the constant definition gives the wrong definition |
20 term, one gets a cryptic message about absrep_fun |
12 term, one gets a cryptic message about absrep_fun |
21 |
13 |
22 - Handle theorems that include Ball/Bex. For this, would |
14 - Handle theorems that include Ball/Bex. |
23 it help if we introduced separate Bex and Ball constants |
15 Workaround: Unfolding Ball_def/Bex_def is enough to lift, |
24 for quotienting? |
16 in some cases regularization is harder though. |
25 |
17 |
26 - The user should be able to give quotient_respects and |
18 - The user should be able to give quotient_respects and |
27 preserves theorems in a more natural form. |
19 preserves theorems in a more natural form. |
28 |
20 |
29 Lower Priority |
21 Lower Priority |
30 ============== |
22 ============== |
31 |
23 |
32 - the quot_lifted attribute should rename variables so they do not |
24 - the quot_lifted attribute should rename variables so they do not |
33 suggest that they talk about raw terms. |
25 suggest that they talk about raw terms. |
34 |
|
35 - accept partial equivalence relations |
|
36 |
26 |
37 - think about what happens if things go wrong (like |
27 - think about what happens if things go wrong (like |
38 theorem cannot be lifted) / proper diagnostic |
28 theorem cannot be lifted) / proper diagnostic |
39 messages for the user |
29 messages for the user |
40 |
30 |
50 |
40 |
51 - Maybe quotient and equiv theorems like the ones for |
41 - Maybe quotient and equiv theorems like the ones for |
52 [QuotList, QuotOption, QuotPair...] could be automatically |
42 [QuotList, QuotOption, QuotPair...] could be automatically |
53 proven? |
43 proven? |
54 |
44 |
55 - Examples: Finite multiset. |
45 - Examples: Finite multiset, Dlist. |
56 |
46 |
57 - The current syntax of the quotient_definition is |
47 - The current syntax of the quotient_definition is |
58 |
48 |
59 "qconst :: qty" |
49 "qconst :: qty" |
60 as "rconst" |
50 as "rconst" |