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
```