author nipkow Thu May 24 16:38:24 2018 +0200 (21 months ago) changeset 68262 d231238bd977 parent 68261 035c78bb0a66 child 68263 e4e536a71e3d
tuned
 src/HOL/Wellfounded.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Wellfounded.thy	Thu May 24 14:42:47 2018 +0200
1.2 +++ b/src/HOL/Wellfounded.thy	Thu May 24 16:38:24 2018 +0200
1.3 @@ -258,18 +258,18 @@
1.4      and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> a = a'"
1.5    shows "wf (map_prod f f ` r)"
1.6  proof (unfold wf_eq_minimal, clarify)
1.7 -  fix Q::"'b set" and b::"'b"
1.8 -  assume b: "b \<in> Q"
1.9 -  define Q' where "Q' \<equiv> f -` Q \<inter> Domain r"
1.10 -  show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> Q"
1.11 -  proof (cases "Q' = {}")
1.12 +  fix B :: "'b set" and b::"'b"
1.13 +  assume "b \<in> B"
1.14 +  define A where "A = f -` B \<inter> Domain r"
1.15 +  show "\<exists>z\<in>B. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> B"
1.16 +  proof (cases "A = {}")
1.17      case False
1.18 -    then obtain b0 where "b0\<in>Q'" and "\<forall>b. (b, b0) \<in> r \<longrightarrow> b \<notin> Q'"
1.19 +    then obtain a0 where "a0 \<in> A" and "\<forall>a. (a, a0) \<in> r \<longrightarrow> a \<notin> A"
1.20        using wfE_min[OF wf_r] by auto
1.21      thus ?thesis
1.22 -      using inj unfolding Q'_def
1.23 -      by (intro bexI[of _ "f b0"]) auto
1.24 -  qed(insert b, unfold Q'_def, auto)
1.25 +      using inj unfolding A_def
1.26 +      by (intro bexI[of _ "f a0"]) auto
1.27 +  qed (insert \<open>b \<in> B\<close>, unfold A_def, auto)
1.28  qed
1.29
1.30  lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
```