--- a/NEWS Sat Mar 15 09:17:46 2025 +0100
+++ b/NEWS Sat Mar 15 10:39:45 2025 +0100
@@ -53,6 +53,8 @@
quotient_disj_strong
* Theory "HOL.Transfer":
+ - Moved right_unique from HOL.Transfer to HOL.Relations.
+ Minor INCOMPATIBILITY.
- Added lemmas.
single_valuedp_eq_right_unique
--- a/src/HOL/Relation.thy Sat Mar 15 09:17:46 2025 +0100
+++ b/src/HOL/Relation.thy Sat Mar 15 10:39:45 2025 +0100
@@ -832,6 +832,12 @@
definition single_valuedp :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "single_valuedp r \<longleftrightarrow> (\<forall>x y. r x y \<longrightarrow> (\<forall>z. r x z \<longrightarrow> y = z))"
+definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+ "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
+
+lemma single_valuedp_eq_right_unique: "single_valuedp = right_unique"
+ by (rule ext) (simp add: single_valuedp_def right_unique_def)
+
lemma single_valuedp_single_valued_eq [pred_set_conv]:
"single_valuedp (\<lambda>x y. (x, y) \<in> r) \<longleftrightarrow> single_valued r"
by (simp add: single_valued_def single_valuedp_def)
@@ -848,6 +854,9 @@
"(\<And>x y. r x y \<Longrightarrow> (\<And>z. r x z \<Longrightarrow> y = z)) \<Longrightarrow> single_valuedp r"
by (fact single_valuedI [to_pred])
+lemma right_uniqueI: "(\<And>x y z. R x y \<Longrightarrow> R x z \<Longrightarrow> y = z) \<Longrightarrow> right_unique R"
+ unfolding right_unique_def by fast
+
lemma single_valuedD:
"single_valued r \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> (x, z) \<in> r \<Longrightarrow> y = z"
by (simp add: single_valued_def)
@@ -856,6 +865,9 @@
"single_valuedp r \<Longrightarrow> r x y \<Longrightarrow> r x z \<Longrightarrow> y = z"
by (fact single_valuedD [to_pred])
+lemma right_uniqueD: "right_unique R \<Longrightarrow> R x y \<Longrightarrow> R x z \<Longrightarrow> y = z"
+ unfolding right_unique_def by fast
+
lemma single_valued_empty [simp]:
"single_valued {}"
by (simp add: single_valued_def)
--- a/src/HOL/Transfer.thy Sat Mar 15 09:17:46 2025 +0100
+++ b/src/HOL/Transfer.thy Sat Mar 15 10:39:45 2025 +0100
@@ -115,9 +115,6 @@
definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
-definition right_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
- where "right_unique R \<longleftrightarrow> (\<forall>x y z. R x y \<longrightarrow> R x z \<longrightarrow> y = z)"
-
definition bi_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
where "bi_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y) \<and> (\<forall>y. \<exists>x. R x y)"
@@ -126,9 +123,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 single_valuedp_eq_right_unique: "single_valuedp = right_unique"
- by (rule ext) (simp add: single_valuedp_def right_unique_def)
-
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
@@ -159,12 +153,6 @@
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_uniqueI: "(\<And>x y z. \<lbrakk> A x y; A x z \<rbrakk> \<Longrightarrow> y = z) \<Longrightarrow> right_unique A"
-unfolding right_unique_def by fast
-
-lemma right_uniqueD: "\<lbrakk> right_unique A; A x y; A x z \<rbrakk> \<Longrightarrow> y = z"
-unfolding right_unique_def by fast
-
lemma right_totalI: "(\<And>y. \<exists>x. A x y) \<Longrightarrow> right_total A"
by(simp add: right_total_def)