merged
authordesharna
Mon, 10 Jun 2024 13:39:09 +0200
changeset 80318 cdf26ac90f87
parent 80317 be2e772e0adf (diff)
parent 80315 a82db14570cd (current diff)
child 80319 f83f402bc9a4
child 80321 31b9dfbe534c
merged
--- a/NEWS	Fri Jun 07 19:14:36 2024 +0200
+++ b/NEWS	Mon Jun 10 13:39:09 2024 +0200
@@ -9,8 +9,10 @@
 
 * Theory "HOL.Wellfounded":
   - Renamed lemmas. Minor INCOMPATIBILITY.
+      wfP_accp_iff ~> wfp_accp_iff
       wfP_if_convertible_to_nat ~> wfp_if_convertible_to_nat
       wfP_if_convertible_to_wfP ~> wfp_if_convertible_to_wfp
+      wf_acc_iff ~> wf_iff_acc
 
 
 New in Isabelle2024 (May 2024)
--- a/src/HOL/List.thy	Fri Jun 07 19:14:36 2024 +0200
+++ b/src/HOL/List.thy	Mon Jun 10 13:39:09 2024 +0200
@@ -7383,7 +7383,7 @@
 qed
 
 lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
-by (auto simp: wf_acc_iff
+by (auto simp: wf_iff_acc
       intro: lists_accD lists_accI[THEN Cons_in_lists_iff[THEN iffD1, THEN conjunct1]])
 
 subsubsection \<open>Lifting Relations to Lists: all elements\<close>
--- a/src/HOL/Wellfounded.thy	Fri Jun 07 19:14:36 2024 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Jun 10 13:39:09 2024 +0200
@@ -935,7 +935,7 @@
   apply blast
   done
 
-theorem wfP_accp_iff: "wfP r = (\<forall>x. accp r x)"
+theorem wfp_iff_accp: "wfp r = (\<forall>x. accp r x)"
   by (blast intro: accp_wfPI dest: accp_wfPD)
 
 
@@ -988,7 +988,7 @@
 lemmas acc_downwards = accp_downwards [to_set]
 lemmas acc_wfI = accp_wfPI [to_set]
 lemmas acc_wfD = accp_wfPD [to_set]
-lemmas wf_acc_iff = wfP_accp_iff [to_set]
+lemmas wf_iff_acc = wfp_iff_accp [to_set]
 lemmas acc_subset = accp_subset [to_set]
 lemmas acc_subset_induct = accp_subset_induct [to_set]
 
@@ -1065,7 +1065,7 @@
     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
@@ -1073,7 +1073,7 @@
 
 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"
+  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])