--- a/NEWS Fri Jun 07 18:50:46 2024 +0200
+++ b/NEWS Sat Jun 08 14:57:14 2024 +0200
@@ -7,6 +7,10 @@
New in this Isabelle version
----------------------------
+* Theory "HOL.Wellfounded":
+ - Renamed lemmas. Minor INCOMPATIBILITY.
+ wfP_if_convertible_to_nat ~> wfp_if_convertible_to_nat
+ wfP_if_convertible_to_wfP ~> wfp_if_convertible_to_wfp
New in Isabelle2024 (May 2024)
--- a/src/HOL/Library/FSet.thy Fri Jun 07 18:50:46 2024 +0200
+++ b/src/HOL/Library/FSet.thy Sat Jun 08 14:57:14 2024 +0200
@@ -1335,7 +1335,7 @@
subsubsection \<open>@{term fsubset}\<close>
lemma wfP_pfsubset: "wfP (|\<subset>|)"
-proof (rule wfP_if_convertible_to_nat)
+proof (rule wfp_if_convertible_to_nat)
show "\<And>x y. x |\<subset>| y \<Longrightarrow> fcard x < fcard y"
by (rule pfsubset_fcard_mono)
qed
--- a/src/HOL/Library/Multiset.thy Fri Jun 07 18:50:46 2024 +0200
+++ b/src/HOL/Library/Multiset.thy Sat Jun 08 14:57:14 2024 +0200
@@ -1548,7 +1548,7 @@
text \<open>Well-foundedness of strict subset relation\<close>
lemma wf_subset_mset_rel: "wf {(M, N :: 'a multiset). M \<subset># N}"
- using mset_subset_size wfP_def wfP_if_convertible_to_nat by blast
+ using mset_subset_size wfP_def wfp_if_convertible_to_nat by blast
lemma wfP_subset_mset[simp]: "wfP (\<subset>#)"
by (rule wf_subset_mset_rel[to_pred])
--- a/src/HOL/Wellfounded.thy Fri Jun 07 18:50:46 2024 +0200
+++ b/src/HOL/Wellfounded.thy Sat Jun 08 14:57:14 2024 +0200
@@ -1065,16 +1065,16 @@
using convertible .
qed
-lemma wfP_if_convertible_to_wfP: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
+lemma wfp_if_convertible_to_wfp: "wfP S \<Longrightarrow> (\<And>x y. R x y \<Longrightarrow> S (f x) (f y)) \<Longrightarrow> wfP R"
using wf_if_convertible_to_wf[to_pred, of S R f] by simp
text \<open>Converting to @{typ nat} is a very common special case that might be found more easily by
Sledgehammer.\<close>
-lemma wfP_if_convertible_to_nat:
+lemma wfp_if_convertible_to_nat:
fixes f :: "_ \<Rightarrow> nat"
shows "(\<And>x y. R x y \<Longrightarrow> f x < f y) \<Longrightarrow> wfP R"
- by (rule wfP_if_convertible_to_wfP[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
+ by (rule wfp_if_convertible_to_wfp[of "(<) :: nat \<Rightarrow> nat \<Rightarrow> bool", simplified])
subsubsection \<open>Measure functions into \<^typ>\<open>nat\<close>\<close>