126 \noindent |
126 \noindent |
127 This constructions yields the new type @{typ int}, and definitions for @{text |
127 This constructions yields the new type @{typ int}, and definitions for @{text |
128 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
128 "0"} and @{text "1"} of type @{typ int} can be given in terms of pairs of |
129 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |
129 natural numbers (namely @{text "(0, 0)"} and @{text "(1, 0)"}). Operations |
130 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in |
130 such as @{text "add"} with type @{typ "int \<Rightarrow> int \<Rightarrow> int"} can be defined in |
131 terms of operations on pairs of natural numbers (namely @{text |
131 terms of operations on pairs of natural numbers: |
132 "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, |
132 |
133 m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"}). |
133 \begin{isabelle}\ \ \ \ \ %%% |
134 Similarly one can construct %%the type of |
134 @{text "add_pair (n\<^isub>1, m\<^isub>1) (n\<^isub>2, m\<^isub>2) \<equiv> (n\<^isub>1 + n\<^isub>2, m\<^isub>1 + m\<^isub>2)"} |
|
135 \end{isabelle} |
|
136 |
|
137 \noindent |
|
138 Similarly one can construct the type of |
135 finite sets, written @{term "\<alpha> fset"}, |
139 finite sets, written @{term "\<alpha> fset"}, |
136 by quotienting the type @{text "\<alpha> list"} according to the equivalence relation |
140 by quotienting the type @{text "\<alpha> list"} according to the equivalence relation |
137 |
141 |
138 \begin{isabelle}\ \ \ \ \ %%% |
142 \begin{isabelle}\ \ \ \ \ %%% |
139 @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv} |
143 @{text "xs \<approx> ys \<equiv> (\<forall>x. memb x xs \<longleftrightarrow> memb x ys)"}\hfill\numbered{listequiv} |
319 according to the type of the raw constant and the type |
323 according to the type of the raw constant and the type |
320 of the quotient constant. This means we also have to extend the notions |
324 of the quotient constant. This means we also have to extend the notions |
321 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
325 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
322 from Homeier \cite{Homeier05}. |
326 from Homeier \cite{Homeier05}. |
323 |
327 |
|
328 {\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}} |
|
329 |
324 In addition we are able to clearly specify what is involved |
330 In addition we are able to clearly specify what is involved |
325 in the lifting process (this was only hinted at in \cite{Homeier05} and |
331 in the lifting process (this was only hinted at in \cite{Homeier05} and |
326 implemented as a ``rough recipe'' in ML-code). A pleasing side-result |
332 implemented as a ``rough recipe'' in ML-code). A pleasing side-result |
327 is that our procedure for lifting theorems is completely deterministic |
333 is that our procedure for lifting theorems is completely deterministic |
328 following the structure of the theorem being lifted and the theorem |
334 following the structure of the theorem being lifted and the theorem |
329 on the quotient level. Space constraints, unfortunately, allow us to only |
335 on the quotient level. {\it Space constraints, unfortunately, allow us to only |
330 sketch this part of our work in Section 5 and we defer the reader to a longer |
336 sketch this part of our work in Section 5 and we defer the reader to a longer |
331 version for the details. However, we will give in Section 3 and 4 all |
337 version for the details.} However, we will give in Section 3 and 4 all |
332 definitions that specify the input and output data of our three-step |
338 definitions that specify the input and output data of our three-step |
333 lifting procedure. Appendix A gives an example how our quotient |
339 lifting procedure. Appendix A gives an example how our quotient |
334 package works in practise. |
340 package works in practise. |
335 *} |
341 *} |
336 |
342 |
1211 LF \cite{UrbanCheneyBerghofer08}, Typed |
1217 LF \cite{UrbanCheneyBerghofer08}, Typed |
1212 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
1218 Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency |
1213 \cite{BengtsonParow09} and a strong normalisation result for cut-elimination |
1219 \cite{BengtsonParow09} and a strong normalisation result for cut-elimination |
1214 in classical logic \cite{UrbanZhu08}. |
1220 in classical logic \cite{UrbanZhu08}. |
1215 |
1221 |
|
1222 {\bf INSTEAD OF NOMINAL WORK, GIVE WORK BY BULWAHN ET AL?} |
1216 |
1223 |
1217 There is a wide range of existing literature for dealing with quotients |
1224 There is a wide range of existing literature for dealing with quotients |
1218 in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that |
1225 in theorem provers. Slotosch~\cite{Slotosch97} implemented a mechanism that |
1219 automatically defines quotient types for Isabelle/HOL. But he did not |
1226 automatically defines quotient types for Isabelle/HOL. But he did not |
1220 include theorem lifting. Harrison's quotient package~\cite{harrison-thesis} |
1227 include theorem lifting. Harrison's quotient package~\cite{harrison-thesis} |
1356 \noindent |
1363 \noindent |
1357 Both methods give the same result, namely @{text "0 + x = x"} |
1364 Both methods give the same result, namely @{text "0 + x = x"} |
1358 where @{text x} is of type integer. |
1365 where @{text x} is of type integer. |
1359 Although seemingly simple, arriving at this result without the help of a quotient |
1366 Although seemingly simple, arriving at this result without the help of a quotient |
1360 package requires a substantial reasoning effort (see \cite{Paulson06}). |
1367 package requires a substantial reasoning effort (see \cite{Paulson06}). |
|
1368 |
|
1369 {\bf \begin{itemize} |
|
1370 \item Type maps and Relation maps (show the case for functions) |
|
1371 \item Quotient extensions |
|
1372 \item Respectfulness and preservation |
|
1373 - Show special cases for quantifiers and lambda |
|
1374 \item Quotient-type locale |
|
1375 - Show the proof as much simpler than Homeier's one |
|
1376 \item ??? Infrastructure for storing theorems (rsp, prs, eqv, quot and idsimp) |
|
1377 \item Lifting vs Descending vs quot\_lifted |
|
1378 - automatic theorem translation heuristic |
|
1379 \item Partial equivalence quotients |
|
1380 - Bounded abstraction |
|
1381 - Respects |
|
1382 - partial descending |
|
1383 \item The heuristics for automatic regularization, injection and cleaning. |
|
1384 \item A complete example of a lifted theorem together with the regularized |
|
1385 injected and cleaned statement |
|
1386 \item Examples of quotients and properties that we used the package for. |
|
1387 \item co/contra-variance from Ondrej should be taken into account |
|
1388 \end{itemize}} |
1361 *} |
1389 *} |
1362 |
1390 |
1363 |
1391 |
1364 |
1392 |
1365 (*<*) |
1393 (*<*) |