author nipkow Thu, 24 May 2018 16:38:24 +0200 changeset 68262 d231238bd977 parent 68261 035c78bb0a66 child 68263 e4e536a71e3d
tuned
 src/HOL/Wellfounded.thy file | annotate | diff | comparison | revisions
```--- 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)"```