--- a/src/HOL/Wellfounded.thy Thu May 24 14:42:47 2018 +0200
+++ b/src/HOL/Wellfounded.thy Thu May 24 16:38:24 2018 +0200
@@ -258,18 +258,18 @@
and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> 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 \<in> Q"
- define Q' where "Q' \<equiv> f -` Q \<inter> Domain r"
- show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> Q"
- proof (cases "Q' = {}")
+ fix B :: "'b set" and b::"'b"
+ assume "b \<in> B"
+ define A where "A = f -` B \<inter> Domain r"
+ show "\<exists>z\<in>B. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> B"
+ proof (cases "A = {}")
case False
- then obtain b0 where "b0\<in>Q'" and "\<forall>b. (b, b0) \<in> r \<longrightarrow> b \<notin> Q'"
+ then obtain a0 where "a0 \<in> A" and "\<forall>a. (a, a0) \<in> r \<longrightarrow> a \<notin> A"
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)
+ using inj unfolding A_def
+ by (intro bexI[of _ "f a0"]) auto
+ qed (insert \<open>b \<in> B\<close>, unfold A_def, auto)
qed
lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"