1 Highest Priority |
|
2 ================ |
|
3 |
|
4 - give examples for the new quantifier translations in regularization |
|
5 (quotient_term.ML) |
|
6 |
|
7 |
|
8 Higher Priority |
|
9 =============== |
|
10 |
|
11 - If the constant definition gives the wrong definition |
|
12 term, one gets a cryptic message about absrep_fun |
|
13 |
|
14 - Handle theorems that include Ball/Bex. |
|
15 Workaround: Unfolding Ball_def/Bex_def is enough to lift, |
|
16 in some cases regularization is harder though. |
|
17 |
|
18 - The user should be able to give quotient_respects and |
|
19 preserves theorems in a more natural form. |
|
20 |
|
21 - Provide syntax for different names of Abs and Rep functions |
|
22 in a similar way to typedef |
|
23 |
|
24 typedef (open) 'a dlist = "{xs::'a list. distinct xs}" |
|
25 morphisms list_of_dlist Abs_dlist |
|
26 |
|
27 - Allow defining constants with existing names. |
|
28 Since 'insert' is defined for sets, |
|
29 "quotient_definition insert" fails for fset |
|
30 however "definition" succeeds. |
|
31 |
|
32 Lower Priority |
|
33 ============== |
|
34 |
|
35 - the quot_lifted attribute should rename variables so they do not |
|
36 suggest that they talk about raw terms. |
|
37 |
|
38 - think about what happens if things go wrong (like |
|
39 theorem cannot be lifted) / proper diagnostic |
|
40 messages for the user |
|
41 |
|
42 - inductions from the datatype package have a strange |
|
43 order of quantifiers in assumptions. |
|
44 |
|
45 - find clean ways how to write down the "mathematical" |
|
46 procedure for a possible submission (Peter submitted |
|
47 his work only to TPHOLs 2005...we would have to go |
|
48 maybe for the Journal of Formalised Mathematics) |
|
49 |
|
50 - add tests for adding theorems to the various thm lists |
|
51 |
|
52 - Maybe quotient and equiv theorems like the ones for |
|
53 [QuotList, QuotOption, QuotPair...] could be automatically |
|
54 proven? |
|
55 |
|
56 - Examples: Finite multiset, Dlist. |
|
57 |
|
58 - The current syntax of the quotient_definition is |
|
59 |
|
60 "qconst :: qty" |
|
61 as "rconst" |
|
62 |
|
63 Is it possible to have the more Isabelle-like |
|
64 syntax |
|
65 |
|
66 qconst :: "qty" |
|
67 as "rconst" |
|
68 |
|
69 That means "qconst :: qty" is not read as a term, but |
|
70 as two entities. |
|