src/HOL/Transfer.thy
changeset 53927 abe2b313f0e5
parent 53011 aeee0a4be6cf
child 53944 50c8f7f21327
     1.1 --- a/src/HOL/Transfer.thy	Thu Sep 26 13:51:08 2013 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Thu Sep 26 15:50:33 2013 +0200
     1.3 @@ -158,6 +158,18 @@
     1.4      (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
     1.5      (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
     1.6  
     1.7 +lemma bi_uniqueDr: "\<lbrakk> bi_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
     1.8 +by(simp add: bi_unique_def)
     1.9 +
    1.10 +lemma bi_uniqueDl: "\<lbrakk> bi_unique A; A x y; A z y \<rbrakk> \<Longrightarrow> x = z"
    1.11 +by(simp add: bi_unique_def)
    1.12 +
    1.13 +lemma right_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
    1.14 +unfolding right_unique_def by blast
    1.15 +
    1.16 +lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
    1.17 +unfolding right_unique_def by blast
    1.18 +
    1.19  lemma right_total_alt_def:
    1.20    "right_total R \<longleftrightarrow> ((R ===> op \<longrightarrow>) ===> op \<longrightarrow>) All All"
    1.21    unfolding right_total_def fun_rel_def