equal
deleted
inserted
replaced
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 |