# HG changeset patch
# User desharna
# Date 1742207439 -3600
# Node ID c65013be534bfc0903544571519b8e1dbee3db43
# Parent  d10a49b7b620d2ea8d34f2bd3c58720176a9894a
added lemmas wf_on_bot[simp] and wfp_on_bot[simp]

diff -r d10a49b7b620 -r c65013be534b NEWS
--- a/NEWS	Mon Mar 17 09:12:18 2025 +0100
+++ b/NEWS	Mon Mar 17 11:30:39 2025 +0100
@@ -63,7 +63,9 @@
   - Added lemmas.
       bex_rtrancl_min_element_if_wf_on
       bex_rtrancl_min_element_if_wfp_on
+      wf_on_bot[simp]
       wf_on_lex_prod[intro]
+      wfp_on_bot[simp]
       wfp_on_iff_wfp
 
 * Theory "HOL.Order_Relation":
diff -r d10a49b7b620 -r c65013be534b src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Mon Mar 17 09:12:18 2025 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Mar 17 11:30:39 2025 +0100
@@ -530,16 +530,17 @@
 
 text \<open>Well-foundedness of the empty relation\<close>
 
+lemma wf_on_bot[simp]: "wf_on A \<bottom>"
+  by (simp add: wf_on_def)
+
+lemma wfp_on_bot[simp]: "wfp_on A \<bottom>"
+  using wf_on_bot[to_pred] .
+
 lemma wf_empty [iff]: "wf {}"
   by (simp add: wf_def)
 
 lemma wfp_empty [iff]: "wfp (\<lambda>x y. False)"
-proof -
-  have "wfp bot"
-    by (fact wf_empty[to_pred bot_empty_eq2])
-  then show ?thesis
-    by (simp add: bot_fun_def)
-qed
+  using wfp_on_bot by (simp add: bot_fun_def)
 
 lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')"
   by (erule wf_subset) (rule Int_lower1)