--- a/NEWS Mon Mar 17 11:30:39 2025 +0100
+++ b/NEWS Mon Mar 17 16:29:48 2025 +0100
@@ -60,6 +60,8 @@
transp_on_top[simp]
* Theory "HOL.Wellfounded":
+ - Removed lemmas. Minor INCOMPATIBILITY.
+ wf_empty[iff] (use wf_on_bot instead)
- Added lemmas.
bex_rtrancl_min_element_if_wf_on
bex_rtrancl_min_element_if_wfp_on
--- a/src/HOL/BNF_Wellorder_Constructions.thy Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/BNF_Wellorder_Constructions.thy Mon Mar 17 16:29:48 2025 +0100
@@ -847,7 +847,7 @@
moreover
{assume Case2: "\<not> Well_order r0"
hence "?R = {}" unfolding ordLess_def by auto
- hence "wf ?R" using wf_empty by simp
+ hence "wf ?R" by simp
}
ultimately have "wf ?R" by blast
}
--- a/src/HOL/Library/Extended_Real.thy Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Library/Extended_Real.thy Mon Mar 17 16:29:48 2025 +0100
@@ -298,7 +298,7 @@
| "real_of_ereal \<infinity> = 0"
| "real_of_ereal (-\<infinity>) = 0"
by (auto intro: ereal_cases)
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
lemma real_of_ereal[simp]:
"real_of_ereal (- x :: ereal) = - (real_of_ereal x)"
@@ -327,7 +327,7 @@
| "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
| "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
by (auto intro: ereal_cases)
-termination proof qed (rule wf_empty)
+termination proof qed (rule wf_on_bot)
instance ..
@@ -377,7 +377,7 @@
with prems show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
lemma Infty_neq_0[simp]:
"(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -852,7 +852,7 @@
| "sgn (\<infinity>::ereal) = 1"
| "sgn (-\<infinity>::ereal) = -1"
by (auto intro: ereal_cases)
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
function times_ereal where
"ereal r * ereal p = ereal (r * p)"
--- a/src/HOL/Library/Old_Recdef.thy Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Mon Mar 17 16:29:48 2025 +0100
@@ -82,6 +82,6 @@
wf_measures
wf_pred_nat
wf_same_fst
- wf_empty
+ wf_on_bot
end
--- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Mar 17 16:29:48 2025 +0100
@@ -203,7 +203,7 @@
st |>
(PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
- THEN (resolve_tac ctxt @{thms wf_empty} 1)
+ THEN (resolve_tac ctxt @{thms wf_on_def} 1)
THEN EVERY (map (prove_row_tac ctxt) clean_table))
end
end) 1 st;
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Mon Mar 17 16:29:48 2025 +0100
@@ -299,7 +299,7 @@
NONE => no_tac
| SOME cert =>
SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
- THEN TRY (resolve_tac ctxt @{thms wf_empty} i))
+ THEN TRY (resolve_tac ctxt @{thms wf_on_bot} i))
end)
fun gen_decomp_scnp_tac orders autom_tac ctxt =
@@ -314,7 +314,7 @@
fun gen_sizechange_tac orders autom_tac ctxt =
TRY (Function_Common.termination_rule_tac ctxt 1)
THEN TRY (Termination.wf_union_tac ctxt)
- THEN (resolve_tac ctxt @{thms wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
+ THEN (resolve_tac ctxt @{thms wf_on_bot} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
fun sizechange_tac ctxt autom_tac =
gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
--- a/src/HOL/Wellfounded.thy Mon Mar 17 11:30:39 2025 +0100
+++ b/src/HOL/Wellfounded.thy Mon Mar 17 16:29:48 2025 +0100
@@ -536,9 +536,6 @@
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)"
using wfp_on_bot by (simp add: bot_fun_def)