# HG changeset patch
# User desharna
# Date 1742112677 -3600
# Node ID 4042628fffa5f17c84e02ce0a4c98f0fba782365
# Parent  d804c8e78ed36f36800b117eb89403a685140d0e
moved left_unique_conversep[simp] and right_unique_conversep[simp] to HOL.Relation

diff -r d804c8e78ed3 -r 4042628fffa5 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sat Mar 15 22:42:29 2025 +0100
+++ b/src/HOL/Relation.thy	Sun Mar 16 09:11:17 2025 +0100
@@ -1283,6 +1283,12 @@
 lemma totalp_on_converse [simp]: "totalp_on A R\<inverse>\<inverse> = totalp_on A R"
   by (rule total_on_converse[to_pred])
 
+lemma left_unique_conversep[simp]: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
+  by (auto simp add: left_unique_def right_unique_def)
+
+lemma right_unique_conversep[simp]: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
+  by (auto simp add: left_unique_def right_unique_def)
+
 lemma conversep_noteq [simp]: "(\<noteq>)\<inverse>\<inverse> = (\<noteq>)"
   by (auto simp add: fun_eq_iff)
 
diff -r d804c8e78ed3 -r 4042628fffa5 src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sat Mar 15 22:42:29 2025 +0100
+++ b/src/HOL/Transfer.thy	Sun Mar 16 09:11:17 2025 +0100
@@ -182,11 +182,6 @@
   unfolding bi_unique_def rel_fun_def by auto
 
 lemma [simp]:
-  shows left_unique_conversep: "left_unique A\<inverse>\<inverse> \<longleftrightarrow> right_unique A"
-    and right_unique_conversep: "right_unique A\<inverse>\<inverse> \<longleftrightarrow> left_unique A"
-  by(auto simp add: left_unique_def right_unique_def)
-
-lemma [simp]:
   shows left_total_conversep: "left_total A\<inverse>\<inverse> \<longleftrightarrow> right_total A"
     and right_total_conversep: "right_total A\<inverse>\<inverse> \<longleftrightarrow> left_total A"
   by(simp_all add: left_total_def right_total_def)