6 |
6 |
7 - have FSet.thy to have a simple infrastructure for |
7 - have FSet.thy to have a simple infrastructure for |
8 finite sets (syntax should be \<lbrace> \<rbrace>, |
8 finite sets (syntax should be \<lbrace> \<rbrace>, |
9 look at Set.thy how syntax is been introduced) |
9 look at Set.thy how syntax is been introduced) |
10 |
10 |
11 - think about what happens if things go wrong (like |
11 - Handle theorems that include Ball/Bex. Would it help |
12 theorem cannot be lifted) / proper diagnostic |
12 if we introduced separate Bex and Ball constants for |
13 messages for the user |
13 quotienting? |
14 |
|
15 - Handle theorems that include Ball/Bex |
|
16 |
14 |
17 - user should be able to give quotient_respects and |
15 - user should be able to give quotient_respects and |
18 preserves theorems in a more natural form. |
16 preserves theorems in a more natural form. |
19 |
17 |
20 - the test in the (_, Const _) needs to be fixed |
18 - the test in the (_, Const _) needs to be fixed |
21 |
19 |
22 Lower Priority |
20 Lower Priority |
23 ============== |
21 ============== |
24 |
22 |
|
23 - Maybe a quotient_definition should already require |
|
24 a proof of the respectfulness (in this way one |
|
25 already excludes non-sensical definitions) |
|
26 |
25 - accept partial equvalence relations |
27 - accept partial equvalence relations |
26 |
28 |
27 - what happens if the original theorem contains bounded |
29 - think about what happens if things go wrong (like |
28 quantifiers? can such theorems be lifted? If not, would |
30 theorem cannot be lifted) / proper diagnostic |
29 it help if we introduced separate Bex and Ball constants |
31 messages for the user |
30 for quotienting? |
|
31 |
32 |
32 - inductions from the datatype package have a strange |
33 - inductions from the datatype package have a strange |
33 order of quantifiers in assumptions. |
34 order of quantifiers in assumptions. |
34 |
35 |
35 - wrapper that translates an an original theorem given |
36 - wrapper that translates an an original theorem given |
54 - Maybe quotient and equiv theorems like the ones for |
55 - Maybe quotient and equiv theorems like the ones for |
55 [QuotList, QuotOption, QuotPair...] could be automatically |
56 [QuotList, QuotOption, QuotPair...] could be automatically |
56 proven? |
57 proven? |
57 |
58 |
58 - Examples: Finite multiset. |
59 - Examples: Finite multiset. |
|
60 |
|
61 - The current syntax of the quotient_definition is |
|
62 |
|
63 "qconst :: qty" |
|
64 as "rconst" |
|
65 |
|
66 Is it possible to have the more Isabelle-like |
|
67 syntax |
|
68 |
|
69 qconst :: "qty" |
|
70 as "rconst" |
|
71 |
|
72 That means "qconst :: qty" is not read as a term, but |
|
73 as two entities. |