# HG changeset patch
# User Andreas Lochbihler
# Date 1380265665 -7200
# Node ID 50c8f7f21327f05c4abe8a6fa758825bb7c5a1dc
# Parent  2b761d9a74f5b6e1af7a178f20779d84940f8ac3
add lemmas

diff -r 2b761d9a74f5 -r 50c8f7f21327 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Fri Sep 27 08:59:22 2013 +0200
+++ b/src/HOL/Lifting.thy	Fri Sep 27 09:07:45 2013 +0200
@@ -76,6 +76,16 @@
 
 lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
 
+lemma [simp]:
+  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
+  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+by(auto simp add: left_unique_def right_unique_def)
+
+lemma [simp]:
+  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
+  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
+by(simp_all add: left_total_def right_total_def)
+
 subsection {* Quotient Predicate *}
 
 definition
diff -r 2b761d9a74f5 -r 50c8f7f21327 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Sep 27 08:59:22 2013 +0200
+++ b/src/HOL/Transfer.thy	Fri Sep 27 09:07:45 2013 +0200
@@ -201,6 +201,12 @@
   "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
   unfolding bi_unique_def fun_rel_def by auto
 
+lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
+by(auto simp add: bi_unique_def)
+
+lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
+by(auto simp add: bi_total_def)
+
 text {* Properties are preserved by relation composition. *}
 
 lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"