| author | Christian Urban <christian dot urban at kcl dot ac dot uk> |
| Sat, 19 Mar 2016 21:06:48 +0000 | |
| branch | Nominal2-Isabelle2016 |
| changeset 3243 | c4f31f1564b7 |
| parent 3082 | a6b0220fb8ae |
| permissions | -rw-r--r-- |
|
3082
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
1 |
Things to describe not in the original quotient paper: |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
2 |
|
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
3 |
* Type maps and Relation maps (show the case for functions) |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
4 |
* Quotient extensions |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
5 |
* Respectfulness and preservation |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
6 |
- Show special cases for quantifiers and lambda |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
7 |
* Quotient-type locale |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
8 |
- Show the proof as much simpler than Homeier's one |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
9 |
* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp) |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
10 |
* Lifting vs Descending vs quot_lifted |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
11 |
- automatic theorem translation heuristic |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
12 |
* Partial equivalence quotients |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
13 |
- Bounded abstraction |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
14 |
- Respects |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
15 |
- partial_descending |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
16 |
* The heuristics for automatic regularization, injection and cleaning. |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
17 |
* A complete example of a lifted theorem together with the regularized |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
18 |
injected and cleaned statement |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
19 |
* Examples of quotients and properties that we used the package for. |
|
a6b0220fb8ae
Added an initial version of qpaper-jv and a TODO of things to write about.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff
changeset
|
20 |
* co/contra-variance from Ondrej should be taken into account |