# HG changeset patch # User nipkow # Date 1527141581 -7200 # Node ID 80df7c90e3151ada2005bd9c8e7ad25ad3555fff # Parent 4e79377048432c9375739f19690ae21be4cdebec By Andrei Popescu based on an initial version by Kasper F. Brandt diff -r 4e7937704843 -r 80df7c90e315 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed May 23 21:34:08 2018 +0100 +++ b/src/HOL/Wellfounded.thy Thu May 24 07:59:41 2018 +0200 @@ -251,14 +251,29 @@ subsubsection \Well-foundedness of image\ +lemma wf_map_prod_image_Dom_Ran: + fixes r:: "('a \ 'a) set" + and f:: "'a \ 'b" + assumes wf_r: "wf r" + and inj: "\ a a'. a \ Domain r \ a' \ Range r \ f a = f a' \ a = a'" + shows "wf (map_prod f f ` r)" +proof (unfold wf_eq_minimal, clarify) + fix Q::"'b set" and b::"'b" + assume b: "b \ Q" + define Q' where "Q' \ f -` Q \ Domain r" + show "\z\Q. \y. (y, z) \ map_prod f f ` r \ y \ Q" + proof (cases "Q' = {}") + case False + then obtain b0 where "b0\Q'" and "\b. (b, b0) \ r \ b \ Q'" + using wfE_min[OF wf_r] by auto + thus ?thesis + using inj unfolding Q'_def + by (intro bexI[of _ "f b0"]) auto + qed(insert b, unfold Q'_def, auto) +qed + lemma wf_map_prod_image: "wf r \ inj f \ wf (map_prod f f ` r)" - apply (simp only: wf_eq_minimal) - apply clarify - apply (case_tac "\p. f p \ Q") - apply (erule_tac x = "{p. f p \ Q}" in allE) - apply (fast dest: inj_onD) - apply blast - done +by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD) subsection \Well-Foundedness Results for Unions\