equal
deleted
inserted
replaced
323 according to the type of the raw constant and the type |
323 according to the type of the raw constant and the type |
324 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 |
325 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
325 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
326 from Homeier \cite{Homeier05}. |
326 from Homeier \cite{Homeier05}. |
327 |
327 |
328 {\bf EXAMPLE BY HUFFMAN ABOUT @{thm map_concat}} |
328 {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset[no_vars]}} |
329 |
329 |
330 In addition we are able to clearly specify what is involved |
330 In addition we are able to clearly specify what is involved |
331 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 |
332 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 |
333 is that our procedure for lifting theorems is completely deterministic |
333 is that our procedure for lifting theorems is completely deterministic |
435 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}. |
435 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}. |
436 \end{definition} |
436 \end{definition} |
437 |
437 |
438 \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs} |
438 \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs} |
439 @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"}; |
439 @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"}; |
440 and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}. |
440 and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}. |
441 \end{definition} |
441 \end{definition} |
442 |
442 |
443 The central definition in Homeier's work \cite{Homeier05} relates equivalence |
443 The central definition in Homeier's work \cite{Homeier05} relates equivalence |
444 relations, abstraction and representation functions: |
444 relations, abstraction and representation functions: |
445 |
445 |
1292 the raw type with which the quotienting will be performed. We give |
1292 the raw type with which the quotienting will be performed. We give |
1293 the same integer relation as the one presented in \eqref{natpairequiv}: |
1293 the same integer relation as the one presented in \eqref{natpairequiv}: |
1294 |
1294 |
1295 \begin{isabelle}\ \ \ \ \ % |
1295 \begin{isabelle}\ \ \ \ \ % |
1296 \begin{tabular}{@ {}l} |
1296 \begin{tabular}{@ {}l} |
1297 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\ |
1297 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\ |
1298 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} |
1298 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} |
1299 \end{tabular} |
1299 \end{tabular} |
1300 \end{isabelle} |
1300 \end{isabelle} |
1301 |
1301 |
1302 \noindent |
1302 \noindent |