src/HOL/Library/ContNotDenum.thy
changeset 53372 f5a6313c7fe4
parent 40702 cf26dd7395e4
child 54263 c4159fe6fa46
     1.1 --- a/src/HOL/Library/ContNotDenum.thy	Mon Sep 02 16:10:26 2013 +0200
     1.2 +++ b/src/HOL/Library/ContNotDenum.thy	Mon Sep 02 23:35:58 2013 +0200
     1.3 @@ -323,64 +323,46 @@
     1.4  
     1.5  lemma closed_subset_ex:
     1.6    fixes c::real
     1.7 -  assumes alb: "a < b"
     1.8 -  shows
     1.9 -    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
    1.10 -proof -
    1.11 -  {
    1.12 -    assume clb: "c < b"
    1.13 -    {
    1.14 -      assume cla: "c < a"
    1.15 -      from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
    1.16 -      with alb have
    1.17 -        "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
    1.18 -        by auto
    1.19 -      hence
    1.20 -        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
    1.21 -        by auto
    1.22 -    }
    1.23 -    moreover
    1.24 -    {
    1.25 -      assume ncla: "\<not>(c < a)"
    1.26 -      with clb have cdef: "a \<le> c \<and> c < b" by simp
    1.27 -      obtain ka where kadef: "ka = (c + b)/2" by blast
    1.28 +  assumes "a < b"
    1.29 +  shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
    1.30 +proof (cases "c < b")
    1.31 +  case True
    1.32 +  show ?thesis
    1.33 +  proof (cases "c < a")
    1.34 +    case True
    1.35 +    with `a < b` `c < b` have "c \<notin> closed_int a b"
    1.36 +      unfolding closed_int_def by auto
    1.37 +    with `a < b` show ?thesis by auto
    1.38 +  next
    1.39 +    case False
    1.40 +    then have "a \<le> c" by simp
    1.41 +    def ka \<equiv> "(c + b)/2"
    1.42  
    1.43 -      from kadef clb have kalb: "ka < b" by auto
    1.44 -      moreover from kadef cdef have kagc: "ka > c" by simp
    1.45 -      ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
    1.46 -      moreover from cdef kagc have "ka \<ge> a" by simp
    1.47 -      hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
    1.48 -      ultimately have
    1.49 -        "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
    1.50 -        using kalb by auto
    1.51 -      hence
    1.52 -        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
    1.53 -        by auto
    1.54 -
    1.55 -    }
    1.56 +    from ka_def `c < b` have kalb: "ka < b" by auto
    1.57 +    moreover from ka_def `c < b` have kagc: "ka > c" by simp
    1.58 +    ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
    1.59 +    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
    1.60 +    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
    1.61      ultimately have
    1.62 -      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
    1.63 -      by (rule case_split)
    1.64 -  }
    1.65 -  moreover
    1.66 -  {
    1.67 -    assume "\<not> (c < b)"
    1.68 -    hence cgeb: "c \<ge> b" by simp
    1.69 +      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
    1.70 +      using kalb by auto
    1.71 +    then show ?thesis
    1.72 +      by auto
    1.73 +  qed
    1.74 +next
    1.75 +  case False
    1.76 +  then have "c \<ge> b" by simp
    1.77  
    1.78 -    obtain kb where kbdef: "kb = (a + b)/2" by blast
    1.79 -    with alb have kblb: "kb < b" by auto
    1.80 -    with kbdef cgeb have "a < kb \<and> kb < c" by auto
    1.81 -    moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
    1.82 -    moreover from kblb have
    1.83 -      "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
    1.84 -    ultimately have
    1.85 -      "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
    1.86 -      by simp
    1.87 -    hence
    1.88 -      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
    1.89 -      by auto
    1.90 -  }
    1.91 -  ultimately show ?thesis by (rule case_split)
    1.92 +  def kb \<equiv> "(a + b)/2"
    1.93 +  with `a < b` have "kb < b" by auto
    1.94 +  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
    1.95 +  from `kb < c` have c: "c \<notin> closed_int a kb"
    1.96 +    unfolding closed_int_def by auto
    1.97 +  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
    1.98 +    unfolding closed_int_def by auto
    1.99 +  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
   1.100 +    by simp
   1.101 +  then show ?thesis by auto
   1.102  qed
   1.103  
   1.104  subsection {* newInt: Interval generation *}