src/HOL/Relation.thy
changeset 59518 28cfc60dea7a
parent 58889 5b7a9633cfa8
child 60057 86fa63ce8156
equal deleted inserted replaced
59517:22c9e6cf5572 59518:28cfc60dea7a
   424 
   424 
   425 lemma transp_trans:
   425 lemma transp_trans:
   426   "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   426   "transp r \<longleftrightarrow> trans {(x, y). r x y}"
   427   by (simp add: trans_def transp_def)
   427   by (simp add: trans_def transp_def)
   428 
   428 
       
   429 lemma transp_equality [simp]: "transp op ="
       
   430 by(auto intro: transpI)
   429 
   431 
   430 subsubsection {* Totality *}
   432 subsubsection {* Totality *}
   431 
   433 
   432 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   434 definition total_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
   433 where
   435 where