| author | Cezary Kaliszyk <kaliszyk@in.tum.de> |
| Fri, 04 Dec 2009 09:33:32 +0100 | |
| changeset 515 | b00a9b58264d |
| parent 514 | 6b3be083229c |
| child 522 | 6b77cfd508e9 |
| permissions | -rw-r--r-- |
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
Higher Priority |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
=============== |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
- redoing Int.thy (problem at the moment with overloaded |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
definitions....Florian) |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
- have FSet.thy to have a simple infrastructure for |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
finite sets (syntax should be \<lbrace> \<rbrace>, |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
look at Set.thy how syntax is been introduced) |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
- think about what happens if things go wrong (like |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
theorem cannot be lifted) / proper diagnostic |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
messages for the user |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
- Ask Peter and Michael for challenging examples |
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
17 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
18 |
|
|
512
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
503
diff
changeset
|
19 |
- Handle theorems that include Ball/Bex |
|
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
503
diff
changeset
|
20 |
|
|
8c7597b19f0e
First version of the deterministic rep-abs-inj-tac.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
503
diff
changeset
|
21 |
|
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
22 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
23 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
25 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
26 |
|
|
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
27 |
Lower Priority |
|
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 |
|
|
506
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
30 |
- allow the user to provide the rsp lemmas in a more |
|
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
31 |
natural form |
|
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
32 |
|
|
503
d2c9a72e52e0
first version of internalised quotient theorems; added FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
33 |
- 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
|
34 |
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
|
35 |
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
|
36 |
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
|
37 |
|
|
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
38 |
- use lower-case letters where appropriate in order |
|
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
39 |
to make Markus happy |
|
91c374abde06
removed quot argument...not all examples work anymore
Christian Urban <urbanc@in.tum.de>
parents:
503
diff
changeset
|
40 |
|
|
515
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
41 |
- 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
|
42 |
|
|
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
43 |
|
|
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
44 |
|
|
b00a9b58264d
Fixes after big merge.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
514
diff
changeset
|
45 |
- Integrate RSP/PRS lemmas in QuotList with the ones from IntEx etc. |