Quotient-Paper-jv/TODO
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 19 Mar 2016 21:06:48 +0000 (2016-03-19)
branchNominal2-Isabelle2016
changeset 3243 c4f31f1564b7
parent 3082 a6b0220fb8ae
permissions -rw-r--r--
updated to Isabelle 2016
Things to describe not in the original quotient paper:

* Type maps and Relation maps (show the case for functions)
* Quotient extensions
* Respectfulness and preservation
  - Show special cases for quantifiers and lambda
* Quotient-type locale
  - Show the proof as much simpler than Homeier's one
* Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp)
* Lifting vs Descending vs quot_lifted
  - automatic theorem translation heuristic
* Partial equivalence quotients
  - Bounded abstraction
  - Respects
  - partial_descending
* The heuristics for automatic regularization, injection and cleaning.
* A complete example of a lifted theorem together with the regularized
  injected and cleaned statement
* Examples of quotients and properties that we used the package for.
* co/contra-variance from Ondrej should be taken into account