# HG changeset patch
# User desharna
# Date 1742803339 -3600
# Node ID 9a9120ec481561bbce102e8b308fb7f96090ae12
# Parent  933d8068a0233ee7f5f785ec01ef2cabaa8cd72d
added lemmas left_unique_mono_strong, left_unique_mono[mono], right_unique_mono_strong, right_unique_mono[mono]

diff -r 933d8068a023 -r 9a9120ec4815 NEWS
--- a/NEWS	Sun Mar 23 22:33:19 2025 +0000
+++ b/NEWS	Mon Mar 24 09:02:19 2025 +0100
@@ -64,9 +64,13 @@
       irreflp_on_bot[simp]
       left_unique_bot[simp]
       left_unique_iff_Uniq
+      left_unique_mono[mono]
+      left_unique_mono_strong
       refl_on_top[simp]
       reflp_on_refl_on_eq[pred_set_conv]
       reflp_on_top[simp]
+      right_unique_mono[mono]
+      right_unique_mono_strong
       sym_on_bot[simp]
       sym_on_top[simp]
       symp_on_bot[simp]
diff -r 933d8068a023 -r 9a9120ec4815 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Mar 23 22:33:19 2025 +0000
+++ b/src/HOL/Relation.thy	Mon Mar 24 09:02:19 2025 +0100
@@ -932,6 +932,14 @@
 lemma left_unique_bot[simp]: "left_unique \<bottom>"
   by (simp add: left_unique_def)
 
+lemma left_unique_mono_strong:
+  "left_unique Q \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> left_unique R"
+  by (rule left_uniqueI) (auto dest: left_uniqueD)
+
+lemma left_unique_mono[mono]: "R \<le> Q \<Longrightarrow> left_unique Q \<le> left_unique R"
+  using left_unique_mono_strong[of Q R]
+  by (simp add: le_fun_def)
+
 
 subsubsection \<open>Right uniqueness\<close>
 
@@ -970,6 +978,14 @@
 lemma right_unique_bot[simp]: "right_unique \<bottom>"
   by (fact single_valued_empty[to_pred])
 
+lemma right_unique_mono_strong:
+  "right_unique Q \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> Q x y) \<Longrightarrow> right_unique R"
+  by (rule right_uniqueI) (auto dest: right_uniqueD)
+
+lemma right_unique_mono[mono]: "R \<le> Q \<Longrightarrow> right_unique Q \<le> right_unique R"
+  using right_unique_mono_strong[of Q R]
+  by (simp add: le_fun_def)
+
 lemma single_valued_subset:
   "r \<subseteq> s \<Longrightarrow> single_valued s \<Longrightarrow> single_valued r"
   unfolding single_valued_def by blast