equal
deleted
inserted
replaced
15 Workaround: Unfolding Ball_def/Bex_def is enough to lift, |
15 Workaround: Unfolding Ball_def/Bex_def is enough to lift, |
16 in some cases regularization is harder though. |
16 in some cases regularization is harder though. |
17 |
17 |
18 - The user should be able to give quotient_respects and |
18 - The user should be able to give quotient_respects and |
19 preserves theorems in a more natural form. |
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 |
20 |
32 Lower Priority |
21 Lower Priority |
33 ============== |
22 ============== |
34 |
23 |
35 - the quot_lifted attribute should rename variables so they do not |
24 - the quot_lifted attribute should rename variables so they do not |
51 |
40 |
52 - Maybe quotient and equiv theorems like the ones for |
41 - Maybe quotient and equiv theorems like the ones for |
53 [QuotList, QuotOption, QuotPair...] could be automatically |
42 [QuotList, QuotOption, QuotPair...] could be automatically |
54 proven? |
43 proven? |
55 |
44 |
56 - Examples: Finite multiset, Dlist. |
45 - Examples: Finite multiset. |
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. |
|