By Andrei Popescu based on an initial version by Kasper F. Brandt
authornipkow
Thu May 24 07:59:41 2018 +0200 (21 months ago)
changeset 6825980df7c90e315
parent 68258 4e7937704843
child 68260 61188c781cdd
By Andrei Popescu based on an initial version by Kasper F. Brandt
src/HOL/Wellfounded.thy
     1.1 --- a/src/HOL/Wellfounded.thy	Wed May 23 21:34:08 2018 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu May 24 07:59:41 2018 +0200
     1.3 @@ -251,14 +251,29 @@
     1.4  
     1.5  subsubsection \<open>Well-foundedness of image\<close>
     1.6  
     1.7 +lemma wf_map_prod_image_Dom_Ran:
     1.8 +  fixes r:: "('a \<times> 'a) set"
     1.9 +    and f:: "'a \<Rightarrow> 'b"
    1.10 +  assumes wf_r: "wf r"
    1.11 +    and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> a = a'"
    1.12 +  shows "wf (map_prod f f ` r)"
    1.13 +proof (unfold wf_eq_minimal, clarify)
    1.14 +  fix Q::"'b set" and b::"'b"
    1.15 +  assume b: "b \<in> Q"
    1.16 +  define Q' where "Q' \<equiv> f -` Q \<inter> Domain r"
    1.17 +  show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> Q"
    1.18 +  proof (cases "Q' = {}")
    1.19 +    case False
    1.20 +    then obtain b0 where "b0\<in>Q'" and "\<forall>b. (b, b0) \<in> r \<longrightarrow> b \<notin> Q'"
    1.21 +      using wfE_min[OF wf_r] by auto
    1.22 +    thus ?thesis 
    1.23 +      using inj unfolding Q'_def   
    1.24 +      by (intro bexI[of _ "f b0"]) auto
    1.25 +  qed(insert b, unfold Q'_def, auto) 
    1.26 +qed
    1.27 +
    1.28  lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"
    1.29 -  apply (simp only: wf_eq_minimal)
    1.30 -  apply clarify
    1.31 -  apply (case_tac "\<exists>p. f p \<in> Q")
    1.32 -   apply (erule_tac x = "{p. f p \<in> Q}" in allE)
    1.33 -   apply (fast dest: inj_onD)
    1.34 -  apply blast
    1.35 -  done
    1.36 +by(rule wf_map_prod_image_Dom_Ran) (auto dest: inj_onD)
    1.37  
    1.38  
    1.39  subsection \<open>Well-Foundedness Results for Unions\<close>