3 imports "Quotient" |
3 imports "Quotient" |
4 "~~/src/HOL/Library/Quotient_Syntax" |
4 "~~/src/HOL/Library/Quotient_Syntax" |
5 "~~/src/HOL/Library/LaTeXsugar" |
5 "~~/src/HOL/Library/LaTeXsugar" |
6 "~~/src/HOL/Quotient_Examples/FSet" |
6 "~~/src/HOL/Quotient_Examples/FSet" |
7 begin |
7 begin |
8 |
|
9 (**** |
|
10 |
|
11 ** things to do for the next version |
|
12 * |
|
13 * - what are quot_thms? |
|
14 * - what do all preservation theorems look like, |
|
15 in particular preservation for quotient |
|
16 compositions |
|
17 - explain how Quotient R Abs Rep is proved (j-version) |
|
18 - give an example where precise specification helps (core Haskell in nominal?) |
|
19 |
|
20 - Mention Andreas Lochbiler in Acknowledgements and 'desceding'. |
|
21 |
|
22 *) |
|
23 |
8 |
24 notation (latex output) |
9 notation (latex output) |
25 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
10 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
26 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
11 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
27 implies (infix "\<longrightarrow>" 100) and |
12 implies (infix "\<longrightarrow>" 100) and |
1328 where @{text x} is of type integer. |
1313 where @{text x} is of type integer. |
1329 Although seemingly simple, arriving at this result without the help of a quotient |
1314 Although seemingly simple, arriving at this result without the help of a quotient |
1330 package requires a substantial reasoning effort (see \cite{Paulson06}). |
1315 package requires a substantial reasoning effort (see \cite{Paulson06}). |
1331 |
1316 |
1332 {\bf \begin{itemize} |
1317 {\bf \begin{itemize} |
|
1318 \item explain how Quotient R Abs Rep is proved |
1333 \item Type maps and Relation maps (show the case for functions) |
1319 \item Type maps and Relation maps (show the case for functions) |
1334 \item Quotient extensions |
1320 \item Quotient extensions (quot\_thms) |
1335 \item Respectfulness and preservation |
1321 \item Respectfulness and preservation |
1336 - Show special cases for quantifiers and lambda |
1322 - Show special cases for quantifiers and lambda |
|
1323 - How do prs theorems look like for quotient compositions |
1337 \item Quotient-type locale |
1324 \item Quotient-type locale |
1338 - Show the proof as much simpler than Homeier's one |
1325 - Show the proof as much simpler than Homeier's one |
1339 \item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp) |
1326 \item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp) |
1340 \item Lifting vs Descending vs quot\_lifted |
1327 \item Lifting vs Descending vs quot\_lifted |
|
1328 - Mention Andreas Lochbiler in Acknowledgements |
1341 - automatic theorem translation heuristic |
1329 - automatic theorem translation heuristic |
1342 \item Partial equivalence quotients |
1330 \item Partial equivalence quotients |
1343 - Bounded abstraction |
1331 - Bounded abstraction |
1344 - Respects |
1332 - Respects |
1345 - partial descending |
1333 - partial descending |
1346 \item The heuristics for automatic regularization, injection and cleaning. |
1334 \item The heuristics for automatic regularization, injection and cleaning. |
1347 \item A complete example of a lifted theorem together with the regularized |
1335 \item A complete example of a lifted theorem together with the regularized |
1348 injected and cleaned statement |
1336 injected and cleaned statement |
1349 \item Examples of quotients and properties that we used the package for. |
1337 \item Examples of quotients and properties that we used the package for. |
1350 \item co/contra-variance from Ondrej should be taken into account |
1338 \item co/contra-variance from Ondrej should be taken into account |
|
1339 \item give an example where precise specification of goal is necessary |
|
1340 \item mention multiple map\_prs2 theorems for compositional quotients |
1351 \end{itemize}} |
1341 \end{itemize}} |
1352 *} |
1342 *} |
1353 |
1343 |
1354 |
1344 |
1355 |
1345 |