1.1 --- a/src/HOL/Lifting.thy	Fri Sep 27 08:59:22 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Fri Sep 27 09:07:45 2013 +0200
     1.3 @@ -76,6 +76,16 @@
     1.4  
     1.5  lemma left_unique_eq: "left_unique op=" unfolding left_unique_def by blast
     1.6  
     1.7 +lemma [simp]:
     1.8 +  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
     1.9 +  and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
    1.10 +by(auto simp add: left_unique_def right_unique_def)
    1.11 +
    1.12 +lemma [simp]:
    1.13 +  shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
    1.14 +  and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
    1.15 +by(simp_all add: left_total_def right_total_def)
    1.16 +
    1.17  subsection {* Quotient Predicate *}
    1.18  
    1.19  definition

     2.1 --- a/src/HOL/Transfer.thy	Fri Sep 27 08:59:22 2013 +0200
     2.2 +++ b/src/HOL/Transfer.thy	Fri Sep 27 09:07:45 2013 +0200
     2.3 @@ -201,6 +201,12 @@
     2.4    "bi_unique R \<longleftrightarrow> (R ===> R ===> op =) (op =) (op =)"
     2.5    unfolding bi_unique_def fun_rel_def by auto
     2.6  
     2.7 +lemma bi_unique_conversep [simp]: "bi_unique R\<inverse>\<inverse> = bi_unique R"
     2.8 +by(auto simp add: bi_unique_def)
     2.9 +
    2.10 +lemma bi_total_conversep [simp]: "bi_total R\<inverse>\<inverse> = bi_total R"
    2.11 +by(auto simp add: bi_total_def)
    2.12 +
    2.13  text {* Properties are preserved by relation composition. *}
    2.14  
    2.15  lemma OO_def: "R OO S = (\<lambda>x z. \<exists>y. R x y \<and> S y z)"