src/HOL/Relation.thy

 
 lemma conversep_conversep [simp]:
   "(r\<inverse>\<inverse>)\<inverse>\<inverse> = r"
   by (fact converse_converse [to_pred])
 
+lemma converse_empty[simp]: "{}\<inverse> = {}"
+by auto
+
+lemma converse_UNIV[simp]: "UNIV\<inverse> = UNIV"
+by auto
+
 lemma converse_relcomp: "(r O s)^-1 = s^-1 O r^-1"
   by blast
 
 lemma converse_relcompp: "(r OO s)^--1 = s^--1 OO r^--1"
   by (iprover intro: order_antisym conversepI relcomppI

   by (auto simp add: fun_eq_iff)
 
 lemma conversep_eq [simp]: "(op =)^--1 = op ="
   by (auto simp add: fun_eq_iff)
 
-lemma converse_unfold:
+lemma converse_unfold [code]:
   "r\<inverse> = {(y, x). (x, y) \<in> r}"
   by (simp add: set_eq_iff)
 
 
 subsubsection {* Domain, range and field *}