src/HOL/Hilbert_Choice.thy
changeset 63981 6f7db4f8df4c
parent 63980 f8e556c8ad6f
child 64591 240a39af9ec4
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Sat Oct 01 17:38:14 2016 +0200
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Sat Oct 01 19:29:48 2016 +0200
     1.3 @@ -466,30 +466,48 @@
     1.4  
     1.5  
     1.6  text \<open>A relation is wellfounded iff it has no infinite descending chain.\<close>
     1.7 -lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<not> (\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r))"
     1.8 -  apply (simp only: wf_eq_minimal)
     1.9 -  apply (rule iffI)
    1.10 -   apply (rule notI)
    1.11 -   apply (erule exE)
    1.12 -   apply (erule_tac x = "{w. \<exists>i. w = f i}" in allE)
    1.13 -   apply blast
    1.14 -  apply (erule contrapos_np)
    1.15 -  apply simp
    1.16 -  apply clarify
    1.17 -  apply (subgoal_tac "\<forall>n. rec_nat x (\<lambda>i y. SOME z. z \<in> Q \<and> (z, y) \<in> r) n \<in> Q")
    1.18 -   apply (rule_tac x = "rec_nat x (\<lambda>i y. SOME z. z \<in> Q \<and> (z, y) \<in> r)" in exI)
    1.19 -   apply (rule allI)
    1.20 -   apply simp
    1.21 -   apply (rule someI2_ex)
    1.22 -    apply blast
    1.23 -   apply blast
    1.24 -  apply (rule allI)
    1.25 -  apply (induct_tac n)
    1.26 -   apply simp_all
    1.27 -  apply (rule someI2_ex)
    1.28 -   apply blast
    1.29 -  apply blast
    1.30 -  done
    1.31 +lemma wf_iff_no_infinite_down_chain: "wf r \<longleftrightarrow> (\<nexists>f. \<forall>i. (f (Suc i), f i) \<in> r)"
    1.32 +  (is "_ \<longleftrightarrow> \<not> ?ex")
    1.33 +proof
    1.34 +  assume "wf r"
    1.35 +  show "\<not> ?ex"
    1.36 +  proof
    1.37 +    assume ?ex
    1.38 +    then obtain f where f: "(f (Suc i), f i) \<in> r" for i
    1.39 +      by blast
    1.40 +    from \<open>wf r\<close> have minimal: "x \<in> Q \<Longrightarrow> \<exists>z\<in>Q. \<forall>y. (y, z) \<in> r \<longrightarrow> y \<notin> Q" for x Q
    1.41 +      by (auto simp: wf_eq_minimal)
    1.42 +    let ?Q = "{w. \<exists>i. w = f i}"
    1.43 +    fix n
    1.44 +    have "f n \<in> ?Q" by blast
    1.45 +    from minimal [OF this] obtain j where "(y, f j) \<in> r \<Longrightarrow> y \<notin> ?Q" for y by blast
    1.46 +    with this [OF \<open>(f (Suc j), f j) \<in> r\<close>] have "f (Suc j) \<notin> ?Q" by simp
    1.47 +    then show False by blast
    1.48 +  qed
    1.49 +next
    1.50 +  assume "\<not> ?ex"
    1.51 +  then show "wf r"
    1.52 +  proof (rule contrapos_np)
    1.53 +    assume "\<not> wf r"
    1.54 +    then obtain Q x where x: "x \<in> Q" and rec: "z \<in> Q \<Longrightarrow> \<exists>y. (y, z) \<in> r \<and> y \<in> Q" for z
    1.55 +      by (auto simp add: wf_eq_minimal)
    1.56 +    obtain descend :: "nat \<Rightarrow> 'a"
    1.57 +      where descend_0: "descend 0 = x"
    1.58 +        and descend_Suc: "descend (Suc n) = (SOME y. y \<in> Q \<and> (y, descend n) \<in> r)" for n
    1.59 +      by (rule that [of "rec_nat x (\<lambda>_ rec. (SOME y. y \<in> Q \<and> (y, rec) \<in> r))"]) simp_all
    1.60 +    have descend_Q: "descend n \<in> Q" for n
    1.61 +    proof (induct n)
    1.62 +      case 0
    1.63 +      with x show ?case by (simp only: descend_0)
    1.64 +    next
    1.65 +      case Suc
    1.66 +      then show ?case by (simp only: descend_Suc) (rule someI2_ex; use rec in blast)
    1.67 +    qed
    1.68 +    have "(descend (Suc i), descend i) \<in> r" for i
    1.69 +      by (simp only: descend_Suc) (rule someI2_ex; use descend_Q rec in blast)
    1.70 +    then show "\<exists>f. \<forall>i. (f (Suc i), f i) \<in> r" by blast
    1.71 +  qed
    1.72 +qed
    1.73  
    1.74  lemma wf_no_infinite_down_chainE:
    1.75    assumes "wf r"