# HG changeset patch
# User desharna
# Date 1742113997 -3600
# Node ID 6ace531790b44c3467486cc7132a1cd0822e1217
# Parent  4042628fffa5f17c84e02ce0a4c98f0fba782365
added lemmas, antisymp_on_bot[simp], asymp_on_bot[simp], irreflp_on_bot[simp], left_unique_bot[simp], symp_on_bot[simp], transp_on_bot[simp]

diff -r 4042628fffa5 -r 6ace531790b4 NEWS
--- a/NEWS	Sun Mar 16 09:11:17 2025 +0100
+++ b/NEWS	Sun Mar 16 09:33:17 2025 +0100
@@ -28,13 +28,19 @@
       antisymp_equality[simp] ~> antisymp_on_equality[simp]
       transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
+      antisymp_on_bot[simp]
+      asymp_on_bot[simp]
+      irreflp_on_bot[simp]
+      left_unique_bot[simp]
       left_unique_iff_Uniq
       reflp_on_refl_on_eq[pred_set_conv]
+      symp_on_bot[simp]
       symp_on_equality[simp]
       totalp_on_mono[mono]
       totalp_on_mono_strong
       totalp_on_mono_stronger
       totalp_on_mono_stronger_alt
+      transp_on_bot[simp]
 
 * Theory "HOL.Wellfounded":
   - Added lemmas.
diff -r 4042628fffa5 -r 6ace531790b4 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Mar 16 09:11:17 2025 +0100
+++ b/src/HOL/Relation.thy	Sun Mar 16 09:33:17 2025 +0100
@@ -316,6 +316,9 @@
 lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
   by (rule irreflD[to_pred])
 
+lemma irreflp_on_bot[simp]: "irreflp_on A \<bottom>"
+  by (simp add: irreflp_on_def)
+
 lemma irrefl_on_distinct [code]: "irrefl_on A r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<noteq> b)"
   by (auto simp add: irrefl_on_def)
 
@@ -382,6 +385,9 @@
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
 
+lemma asymp_on_bot[simp]: "asymp_on A \<bottom>"
+  by (simp add: asymp_on_def)
+
 lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
   by (blast dest: asymD)
 
@@ -434,6 +440,9 @@
 
 lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma symp_on_bot[simp]: "symp_on A \<bottom>"
+  by (simp add: symp_on_def)
+
 lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
   by (auto simp: sym_on_def)
 
@@ -533,6 +542,9 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma antisymp_on_bot[simp]: "antisymp_on A \<bottom>"
+  by (simp add: antisymp_on_def)
+
 lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
   by (auto simp: antisym_on_def)
 
@@ -723,8 +735,11 @@
 lemma trans_empty [simp]: "trans {}"
   by (blast intro: transI)
 
+lemma transp_on_bot[simp]: "transp_on A \<bottom>"
+  by (simp add: transp_on_def)
+
 lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
-  using trans_empty[to_pred] by (simp add: bot_fun_def)
+  using transp_on_bot unfolding bot_fun_def bot_bool_def .
 
 lemma trans_singleton [simp]: "trans {(a, a)}"
   by (blast intro: transI)
@@ -886,6 +901,9 @@
 lemma left_unique_iff_Uniq: "left_unique r \<longleftrightarrow> (\<forall>y. \<exists>\<^sub>\<le>\<^sub>1x. r x y)"
   unfolding Uniq_def left_unique_def by blast
 
+lemma left_unique_bot[simp]: "left_unique \<bottom>"
+  by (simp add: left_unique_def)
+
 
 subsubsection \<open>Right uniqueness\<close>