equal
deleted
inserted
replaced
426 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}. |
426 An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}. |
427 \end{definition} |
427 \end{definition} |
428 |
428 |
429 \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs} |
429 \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs} |
430 @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"}; |
430 @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"}; |
431 and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}. |
431 and @{text "(\<lambda>x \<in> S. f x) x = f x"} provided @{text "x \<in> S"}. |
432 \end{definition} |
432 \end{definition} |
433 |
433 |
434 The central definition in Homeier's work \cite{Homeier05} relates equivalence |
434 The central definition in Homeier's work \cite{Homeier05} relates equivalence |
435 relations, abstraction and representation functions: |
435 relations, abstraction and representation functions: |
436 |
436 |
1282 the raw type with which the quotienting will be performed. We give |
1282 the raw type with which the quotienting will be performed. We give |
1283 the same integer relation as the one presented in \eqref{natpairequiv}: |
1283 the same integer relation as the one presented in \eqref{natpairequiv}: |
1284 |
1284 |
1285 \begin{isabelle}\ \ \ \ \ % |
1285 \begin{isabelle}\ \ \ \ \ % |
1286 \begin{tabular}{@ {}l} |
1286 \begin{tabular}{@ {}l} |
1287 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> (nat \<times> nat)"}\\ |
1287 \isacommand{fun}~~@{text "int_rel :: (nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"}\\ |
1288 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} |
1288 \isacommand{where}~~@{text "int_rel (m, n) (p, q) = (m + q = n + p)"} |
1289 \end{tabular} |
1289 \end{tabular} |
1290 \end{isabelle} |
1290 \end{isabelle} |
1291 |
1291 |
1292 \noindent |
1292 \noindent |