src/HOL/Lifting.thy
changeset 53927 abe2b313f0e5
parent 53651 ee90c67502c9
child 53944 50c8f7f21327
     1.1 --- a/src/HOL/Lifting.thy	Thu Sep 26 13:51:08 2013 +0200
     1.2 +++ b/src/HOL/Lifting.thy	Thu Sep 26 15:50:33 2013 +0200
     1.3 @@ -38,9 +38,21 @@
     1.4    obtains "(\<And>x. \<exists>y. R x y)"
     1.5  using assms unfolding left_total_def by blast
     1.6  
     1.7 +lemma bi_total_conv_left_right: "bi_total R \<longleftrightarrow> left_total R \<and> right_total R"
     1.8 +by(simp add: left_total_def right_total_def bi_total_def)
     1.9 +
    1.10  definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
    1.11    where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
    1.12  
    1.13 +lemma bi_unique_conv_left_right: "bi_unique R \<longleftrightarrow> left_unique R \<and> right_unique R"
    1.14 +by(auto simp add: left_unique_def right_unique_def bi_unique_def)
    1.15 +
    1.16 +lemma left_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
    1.17 +unfolding left_unique_def by blast
    1.18 +
    1.19 +lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
    1.20 +unfolding left_unique_def by blast
    1.21 +
    1.22  lemma left_total_fun:
    1.23    "\<lbrakk>left_unique A; left_total B\<rbrakk> \<Longrightarrow> left_total (A ===> B)"
    1.24    unfolding left_total_def fun_rel_def