author wenzelm Mon Sep 02 23:35:58 2013 +0200 (2013-09-02) changeset 53372 f5a6313c7fe4 parent 53371 47b23c582127 child 53373 3ca9e79ac926
tuned proof;
```     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 *}
```