--- a/src/HOL/Transfer.thy Sat Mar 15 20:27:25 2025 +0100
+++ b/src/HOL/Transfer.thy Sat Mar 15 20:33:19 2025 +0100
@@ -106,6 +106,8 @@
subsection \<open>Predicates on relations, i.e. ``class constraints''\<close>
+text \<open>See also \<^const>\<open>Relation.left_unique\<close> and \<^const>\<open>Relation.right_unique\<close>.\<close>
+
definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
@@ -120,9 +122,6 @@
(\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z) \<and>
(\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
-lemma left_unique_iff: "left_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z)"
- unfolding Uniq_def left_unique_def by force
-
lemma left_totalI:
"(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
unfolding left_total_def by blast
@@ -141,9 +140,6 @@
lemma bi_unique_iff: "bi_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R x z) \<and> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
unfolding Uniq_def bi_unique_def by force
-lemma right_unique_iff: "right_unique R \<longleftrightarrow> (\<forall>z. \<exists>\<^sub>\<le>\<^sub>1x. R z x)"
- unfolding Uniq_def right_unique_def by force
-
lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
by(simp add: right_total_def)