--- a/NEWS Wed Mar 27 22:56:03 2024 +0100
+++ b/NEWS Thu Mar 28 08:30:42 2024 +0100
@@ -123,7 +123,6 @@
predicates such as asymp, transp, or totalp.
- Added lemmas.
wellorder.wfp_on_less[simp]
- wfp_iff_ex_minimal
wf_iff_ex_minimal
wf_onE_pf
wf_onI_pf
@@ -134,10 +133,12 @@
wf_on_iff_wf
wf_on_induct
wf_on_subset
+ wfp_iff_ex_minimal
wfp_on_antimono
wfp_on_antimono_strong
wfp_on_if_convertible_to_wfp_on
wfp_on_iff_ex_minimal
+ wfp_on_image
wfp_on_induct
wfp_on_inv_imagep
wfp_on_subset
--- a/src/HOL/Wellfounded.thy Wed Mar 27 22:56:03 2024 +0100
+++ b/src/HOL/Wellfounded.thy Thu Mar 28 08:30:42 2024 +0100
@@ -4,6 +4,7 @@
Author: Konrad Slind
Author: Alexander Krauss
Author: Andrei Popescu, TU Muenchen
+ Author: Martin Desharnais, MPI-INF Saarbruecken
*)
section \<open>Well-founded Recursion\<close>
@@ -490,6 +491,61 @@
lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD)
+lemma wfp_on_image: "wfp_on (f ` A) R \<longleftrightarrow> wfp_on A (\<lambda>a b. R (f a) (f b))"
+proof (rule iffI)
+ assume hyp: "wfp_on (f ` A) R"
+ show "wfp_on A (\<lambda>a b. R (f a) (f b))"
+ unfolding wfp_on_iff_ex_minimal
+ proof (intro allI impI)
+ fix B
+ assume "B \<subseteq> A" and "B \<noteq> {}"
+ hence "f ` B \<subseteq> f ` A" and "f ` B \<noteq> {}"
+ unfolding atomize_conj image_is_empty
+ using image_mono by iprover
+ hence "\<exists>z\<in>f ` B. \<forall>y. R y z \<longrightarrow> y \<notin> f ` B"
+ using hyp[unfolded wfp_on_iff_ex_minimal, rule_format] by iprover
+ then obtain fz where "fz \<in> f ` B" and fz_max: "\<forall>y. R y fz \<longrightarrow> y \<notin> f ` B" ..
+
+ obtain z where "z \<in> B" and "fz = f z"
+ using \<open>fz \<in> f ` B\<close> unfolding image_iff ..
+
+ show "\<exists>z\<in>B. \<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> B"
+ proof (intro bexI allI impI)
+ show "z \<in> B"
+ using \<open>z \<in> B\<close> .
+ next
+ fix y assume "R (f y) (f z)"
+ hence "f y \<notin> f ` B"
+ using fz_max \<open>fz = f z\<close> by iprover
+ thus "y \<notin> B"
+ by (rule contrapos_nn) (rule imageI)
+ qed
+ qed
+next
+ assume hyp: "wfp_on A (\<lambda>a b. R (f a) (f b))"
+ show "wfp_on (f ` A) R"
+ unfolding wfp_on_iff_ex_minimal
+ proof (intro allI impI)
+ fix fA
+ assume "fA \<subseteq> f ` A" and "fA \<noteq> {}"
+ then obtain A' where "A' \<subseteq> A" and "A' \<noteq> {}" and "fA = f ` A'"
+ by (auto simp only: subset_image_iff)
+
+ obtain z where "z \<in> A'" and z_max: "\<forall>y. R (f y) (f z) \<longrightarrow> y \<notin> A'"
+ using hyp[unfolded wfp_on_iff_ex_minimal, rule_format, OF \<open>A' \<subseteq> A\<close> \<open>A' \<noteq> {}\<close>] by blast
+
+ show "\<exists>z\<in>fA. \<forall>y. R y z \<longrightarrow> y \<notin> fA"
+ proof (intro bexI allI impI)
+ show "f z \<in> fA"
+ unfolding \<open>fA = f ` A'\<close>
+ using imageI[OF \<open>z \<in> A'\<close>] .
+ next
+ show "\<And>y. R y (f z) \<Longrightarrow> y \<notin> fA"
+ unfolding \<open>fA = f ` A'\<close>
+ using z_max by auto
+ qed
+ qed
+qed
subsection \<open>Well-Foundedness Results for Unions\<close>