# HG changeset patch
# User desharna
# Date 1742031585 -3600
# Node ID c17902fcf5e7996aa46e3ca855a8c02d751baabe
# Parent  c61367ada9bbeac928b18bd1a1b8272e07c4e222
moved predicate right_unique to theory Relation

diff -r c61367ada9bb -r c17902fcf5e7 NEWS
--- 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
 
diff -r c61367ada9bb -r c17902fcf5e7 src/HOL/Relation.thy
--- 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)
diff -r c61367ada9bb -r c17902fcf5e7 src/HOL/Transfer.thy
--- 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)