tuned
authornipkow
Thu May 24 16:38:24 2018 +0200 (21 months ago)
changeset 68262d231238bd977
parent 68261 035c78bb0a66
child 68263 e4e536a71e3d
tuned
src/HOL/Wellfounded.thy
     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)"