| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Tue, 13 Apr 2010 15:59:53 +0200 | |
| changeset 1820 | de28a91eaca3 |
| parent 1281 | 66fc26f32f25 |
| child 1940 | 0913f697fe73 |
| permissions | -rw-r--r-- |
|
778
54f186bb5e3e
added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de>
parents:
768
diff
changeset
|
1 |
Highest Priority |
|
54f186bb5e3e
added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de>
parents:
768
diff
changeset
|
2 |
================ |
|
54f186bb5e3e
added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de>
parents:
768
diff
changeset
|
3 |
|
|
952
9c3b3eaecaff
use of equiv_relation_chk in quotient_term
Christian Urban <urbanc@in.tum.de>
parents:
921
diff
changeset
|
4 |
- give examples for the new quantifier translations in regularization |
|
9c3b3eaecaff
use of equiv_relation_chk in quotient_term
Christian Urban <urbanc@in.tum.de>
parents:
921
diff
changeset
|
5 |
(quotient_term.ML) |
|
9c3b3eaecaff
use of equiv_relation_chk in quotient_term
Christian Urban <urbanc@in.tum.de>
parents:
921
diff
changeset
|
6 |
|
|
9c3b3eaecaff
use of equiv_relation_chk in quotient_term
Christian Urban <urbanc@in.tum.de>
parents:
921
diff
changeset
|
7 |
|
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
Higher Priority |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
=============== |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
|
1204
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
11 |
|
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
12 |
- Also, in the interest of making nicer generated documentation, you |
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
13 |
might want to change all your "section" headings in Quotient.thy to |
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
14 |
"subsection", and add a "header" statement to the top of the file. |
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
15 |
Otherwise, each "section" gets its own chapter in the generated pdf, |
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
16 |
when the rest of HOL has one chapter per theory file (the chapter |
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
17 |
title comes from the "header" statement). |
|
7e9e96158025
Added Brian's suggestion.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
1203
diff
changeset
|
18 |
|
|
794
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
parents:
778
diff
changeset
|
19 |
- If the constant definition gives the wrong definition |
|
778
54f186bb5e3e
added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de>
parents:
768
diff
changeset
|
20 |
term, one gets a cryptic message about absrep_fun |
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
21 |
|
|
794
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
parents:
778
diff
changeset
|
22 |
- Handle theorems that include Ball/Bex. For this, would |
|
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
parents:
778
diff
changeset
|
23 |
it help if we introduced separate Bex and Ball constants |
|
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
parents:
778
diff
changeset
|
24 |
for quotienting? |
|
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
503
diff
changeset
|
25 |
|
|
794
f0a78fda343f
added an item about when the same quotient constant is defined twice (throws a bind exception in quoteint_def.ML)
Christian Urban <urbanc@in.tum.de>
parents:
778
diff
changeset
|
26 |
- The user should be able to give quotient_respects and |
|
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
753
diff
changeset
|
27 |
preserves theorems in a more natural form. |
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
28 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
29 |
Lower Priority |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
30 |
============== |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
31 |
|
| 1281 | 32 |
- the quot_lifted attribute should rename variables so they do not |
33 |
suggest that they talk about raw terms. |
|
34 |
||
|
778
54f186bb5e3e
added "Highest Priority" category; and tuned slightly code
Christian Urban <urbanc@in.tum.de>
parents:
768
diff
changeset
|
35 |
- accept partial equivalence relations |
|
716
1e08743b6997
FSet3 minor fixes + cases
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
713
diff
changeset
|
36 |
|
|
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
37 |
- think about what happens if things go wrong (like |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
38 |
theorem cannot be lifted) / proper diagnostic |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
39 |
messages for the user |
|
760
c1989de100b4
various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
753
diff
changeset
|
40 |
|
|
713
54cb69112477
Updated TODO list together.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
700
diff
changeset
|
41 |
- inductions from the datatype package have a strange |
|
54cb69112477
Updated TODO list together.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
700
diff
changeset
|
42 |
order of quantifiers in assumptions. |
|
54cb69112477
Updated TODO list together.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
700
diff
changeset
|
43 |
|
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
44 |
- find clean ways how to write down the "mathematical" |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
45 |
procedure for a possible submission (Peter submitted |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
46 |
his work only to TPHOLs 2005...we would have to go |
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
47 |
maybe for the Journal of Formalised Mathematics) |
|
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
48 |
|
|
515
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
49 |
- add tests for adding theorems to the various thm lists |
|
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
50 |
|
| 746 | 51 |
- Maybe quotient and equiv theorems like the ones for |
52 |
[QuotList, QuotOption, QuotPair...] could be automatically |
|
53 |
proven? |
|
|
753
544b05e03ec0
Removed lambdas on the right hand side. This fixes all 'PROBLEM' comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
746
diff
changeset
|
54 |
|
|
768
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
55 |
- Examples: Finite multiset. |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
56 |
|
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
57 |
- The current syntax of the quotient_definition is |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
58 |
|
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
59 |
"qconst :: qty" |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
60 |
as "rconst" |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
61 |
|
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
62 |
Is it possible to have the more Isabelle-like |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
63 |
syntax |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
64 |
|
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
65 |
qconst :: "qty" |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
66 |
as "rconst" |
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
67 |
|
|
e9e205b904e2
get_fun needed change to cope with "('a fset) fset" types...this needs composition (op o); now id_simps contains also id_o and o_id, and map_id is also added in QuotList.thy; regularize and cleaning needed to be hacked (indicated by "HACK")...THIS NEEDS ATTENTION!!!; except two lemmas in IntEx, all examples go through; added considerable material to FSet3; tuned FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
760
diff
changeset
|
68 |
That means "qconst :: qty" is not read as a term, but |
|
912
aa960d16570f
Lifted Peter's Sigma lemma with Ex1.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
866
diff
changeset
|
69 |
as two entities. |
| 1203 | 70 |
|
71 |
- Restrict automatic translation to particular quotient types |
|
72 |