Definition of Respects.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 15 Jun 2010 10:08:12 +0200
changeset 2268 1fd6809f5a44
parent 2267 3bcd715abd39
child 2270 4ae32dd02d14
child 2271 c0c5bc4ee8cb
Definition of Respects.
Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Tue Jun 15 09:22:38 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Tue Jun 15 10:08:12 2010 +0200
@@ -353,6 +353,10 @@
       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
   \end{proposition}
 
+  \begin{definition}[Respects]
+  An element @{text "x"} respects a relation @{text "R"} if and only if @{text "R x x"}.
+  \end{definition}
+
   \noindent
   We will heavily rely on this part of Homeier's work including an extension 
   to deal with compositions of equivalence relations defined as follows
@@ -370,6 +374,7 @@
   the HOL type system). However, we can prove useful instances for compatible
   containers. We will show such example in Section \ref{sec:resp}.
 
+
 *}
 
 section {* Quotient Types and Quotient Definitions\label{sec:type} *}