# HG changeset patch
# User desharna
# Date 1742066223 -3600
# Node ID 919eb0e6793060ff001f8e8c2b8bbd319c6c7b82
# Parent  9357ef19fc565ee2b64614aef5c2ebc20548628d
Moved predicate left_unique from HOL.Transfer to HOL.Relation

diff -r 9357ef19fc56 -r 919eb0e67930 NEWS
--- a/NEWS	Sat Mar 15 19:40:10 2025 +0100
+++ b/NEWS	Sat Mar 15 20:17:03 2025 +0100
@@ -55,8 +55,8 @@
       quotient_disj_strong
 
 * Theory "HOL.Transfer":
-  - Moved right_unique from HOL.Transfer to HOL.Relation.
-    Minor INCOMPATIBILITY.
+  - Moved predicates left_unique and right_unique from HOL.Transfer to
+    HOL.Relation. Minor INCOMPATIBILITY.
   - Added lemmas.
       single_valuedp_eq_right_unique
 
diff -r 9357ef19fc56 -r 919eb0e67930 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Mar 15 19:40:10 2025 +0100
+++ b/src/HOL/Relation.thy	Sat Mar 15 20:17:03 2025 +0100
@@ -824,7 +824,19 @@
   by (rule totalp_onI, rule linear)
 
 
-subsubsection \<open>Single valued relations\<close>
+subsubsection \<open>Left uniqueness\<close>
+
+definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" where
+  "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
+
+lemma left_uniqueI: "(\<And>x y z. A x z \<Longrightarrow> A y z \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
+  unfolding left_unique_def by blast
+
+lemma left_uniqueD: "left_unique A \<Longrightarrow> A x z \<Longrightarrow> A y z \<Longrightarrow> x = y"
+  unfolding left_unique_def by blast
+
+
+subsubsection \<open>Right uniqueness\<close>
 
 definition single_valued :: "('a \<times> 'b) set \<Rightarrow> bool"
   where "single_valued r \<longleftrightarrow> (\<forall>x y. (x, y) \<in> r \<longrightarrow> (\<forall>z. (x, z) \<in> r \<longrightarrow> y = z))"
diff -r 9357ef19fc56 -r 919eb0e67930 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sat Mar 15 19:40:10 2025 +0100
+++ b/src/HOL/Transfer.thy	Sat Mar 15 20:17:03 2025 +0100
@@ -109,9 +109,6 @@
 definition left_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   where "left_total R \<longleftrightarrow> (\<forall>x. \<exists>y. R x y)"
 
-definition left_unique :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
-  where "left_unique R \<longleftrightarrow> (\<forall>x y z. R x z \<longrightarrow> R y z \<longrightarrow> x = y)"
-
 definition right_total :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool"
   where "right_total R \<longleftrightarrow> (\<forall>y. \<exists>x. R x y)"
 
@@ -126,12 +123,6 @@
 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_uniqueI: "(\<And>x y z. \<lbrakk> A x z; A y z \<rbrakk> \<Longrightarrow> x = y) \<Longrightarrow> left_unique A"
-unfolding left_unique_def by blast
-
-lemma left_uniqueD: "\<lbrakk> left_unique A; A x z; A y z \<rbrakk> \<Longrightarrow> x = y"
-unfolding left_unique_def by blast
-
 lemma left_totalI:
   "(\<And>x. \<exists>y. R x y) \<Longrightarrow> left_total R"
 unfolding left_total_def by blast