# HG changeset patch
# User desharna
# Date 1742198440 -3600
# Node ID 4dd01eb1e0cbb02afaff1bc1064480072841e018
# Parent  3fb2525699e64263acbbd12962092617567f15d2# Parent  5da251ee8b58aa12dcf5c0bac43a77d424b1d1d6
merged

diff -r 3fb2525699e6 -r 4dd01eb1e0cb NEWS
--- a/NEWS	Sun Mar 16 17:02:41 2025 +0000
+++ b/NEWS	Mon Mar 17 09:00:40 2025 +0100
@@ -22,24 +22,33 @@
     the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
   - Removed predicate single_valuedp. Use predicate right_unique instead.
     INCOMPATIBILITY.
+  - Removed lemmas. Minor INCOMPATIBILITY.
+      antisym_empty[simp] (use antisym_on_bot instead)
+      antisym_bot[simp] (use antisymp_on_bot instead)
+      trans_empty[simp] (use trans_on_bot instead)
   - Strengthened lemmas. Minor INCOMPATIBILITY.
       refl_on_empty[simp]
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       antisymp_equality[simp] ~> antisymp_on_equality[simp]
       transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
+      antisym_on_bot[simp]
       antisymp_on_bot[simp]
+      asym_on_bot[simp]
       asymp_on_bot[simp]
+      irrefl_on_bot[simp]
       irreflp_on_bot[simp]
       left_unique_bot[simp]
       left_unique_iff_Uniq
       reflp_on_refl_on_eq[pred_set_conv]
+      sym_on_bot[simp]
       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
+      trans_on_bot[simp]
       transp_on_bot[simp]
 
 * Theory "HOL.Wellfounded":
diff -r 3fb2525699e6 -r 4dd01eb1e0cb src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Sun Mar 16 17:02:41 2025 +0000
+++ b/src/HOL/Relation.thy	Mon Mar 17 09:00:40 2025 +0100
@@ -316,8 +316,11 @@
 lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
   by (rule irreflD[to_pred])
 
+lemma irrefl_on_bot[simp]: "irrefl_on A \<bottom>"
+  by (simp add: irrefl_on_def)
+
 lemma irreflp_on_bot[simp]: "irreflp_on A \<bottom>"
-  by (simp add: irreflp_on_def)
+  using irrefl_on_bot[to_pred] .
 
 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)
@@ -385,8 +388,11 @@
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
 
+lemma asym_on_bot[simp]: "asym_on A \<bottom>"
+  by (simp add: asym_on_def)
+
 lemma asymp_on_bot[simp]: "asymp_on A \<bottom>"
-  by (simp add: asymp_on_def)
+  using asym_on_bot[to_pred] .
 
 lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
   by (blast dest: asymD)
@@ -440,8 +446,11 @@
 
 lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma sym_on_bot[simp]: "sym_on A \<bottom>"
+  by (simp add: sym_on_def)
+
 lemma symp_on_bot[simp]: "symp_on A \<bottom>"
-  by (simp add: symp_on_def)
+  using sym_on_bot[to_pred] .
 
 lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
   by (auto simp: sym_on_def)
@@ -542,8 +551,11 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma antisym_on_bot[simp]: "antisym_on A \<bottom>"
+  by (simp add: antisym_on_def)
+
 lemma antisymp_on_bot[simp]: "antisymp_on A \<bottom>"
-  by (simp add: antisymp_on_def)
+  using antisym_on_bot[to_pred] .
 
 lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
   by (auto simp: antisym_on_def)
@@ -596,14 +608,6 @@
   "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r"
   by (fact antisym_subset [to_pred])
     
-lemma antisym_empty [simp]:
-  "antisym {}"
-  unfolding antisym_def by blast
-
-lemma antisym_bot [simp]:
-  "antisymp \<bottom>"
-  by (fact antisym_empty [to_pred])
-    
 lemma antisymp_on_equality[simp]: "antisymp_on A (=)"
   by (auto intro: antisymp_onI)
 
@@ -732,11 +736,11 @@
 lemma transp_on_equality[simp]: "transp_on A (=)"
   by (auto intro: transp_onI)
 
-lemma trans_empty [simp]: "trans {}"
-  by (blast intro: transI)
+lemma trans_on_bot[simp]: "trans_on A \<bottom>"
+  by (simp add: trans_on_def)
 
 lemma transp_on_bot[simp]: "transp_on A \<bottom>"
-  by (simp add: transp_on_def)
+  using trans_on_bot[to_pred] .
 
 lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
   using transp_on_bot unfolding bot_fun_def bot_bool_def .