# HG changeset patch
# User wenzelm
# Date 1378157758 -7200
# Node ID f5a6313c7fe4960a8d2ff8675759a941633be915
# Parent  47b23c58212771da82135ed24d7517a40e87d120
tuned proof;

diff -r 47b23c582127 -r f5a6313c7fe4 src/HOL/Library/ContNotDenum.thy
--- a/src/HOL/Library/ContNotDenum.thy	Mon Sep 02 16:10:26 2013 +0200
+++ b/src/HOL/Library/ContNotDenum.thy	Mon Sep 02 23:35:58 2013 +0200
@@ -323,64 +323,46 @@
 
 lemma closed_subset_ex:
   fixes c::real
-  assumes alb: "a < b"
-  shows
-    "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-proof -
-  {
-    assume clb: "c < b"
-    {
-      assume cla: "c < a"
-      from alb cla clb have "c \<notin> closed_int a b" by (unfold closed_int_def, auto)
-      with alb have
-        "a < b \<and> closed_int a b \<subseteq> closed_int a b \<and> c \<notin> closed_int a b"
-        by auto
-      hence
-        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-        by auto
-    }
-    moreover
-    {
-      assume ncla: "\<not>(c < a)"
-      with clb have cdef: "a \<le> c \<and> c < b" by simp
-      obtain ka where kadef: "ka = (c + b)/2" by blast
+  assumes "a < b"
+  shows "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> closed_int ka kb"
+proof (cases "c < b")
+  case True
+  show ?thesis
+  proof (cases "c < a")
+    case True
+    with `a < b` `c < b` have "c \<notin> closed_int a b"
+      unfolding closed_int_def by auto
+    with `a < b` show ?thesis by auto
+  next
+    case False
+    then have "a \<le> c" by simp
+    def ka \<equiv> "(c + b)/2"
 
-      from kadef clb have kalb: "ka < b" by auto
-      moreover from kadef cdef have kagc: "ka > c" by simp
-      ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
-      moreover from cdef kagc have "ka \<ge> a" by simp
-      hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
-      ultimately have
-        "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
-        using kalb by auto
-      hence
-        "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-        by auto
-
-    }
+    from ka_def `c < b` have kalb: "ka < b" by auto
+    moreover from ka_def `c < b` have kagc: "ka > c" by simp
+    ultimately have "c\<notin>(closed_int ka b)" by (unfold closed_int_def, auto)
+    moreover from `a \<le> c` kagc have "ka \<ge> a" by simp
+    hence "closed_int ka b \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
     ultimately have
-      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-      by (rule case_split)
-  }
-  moreover
-  {
-    assume "\<not> (c < b)"
-    hence cgeb: "c \<ge> b" by simp
+      "ka < b  \<and> closed_int ka b \<subseteq> closed_int a b \<and> c \<notin> closed_int ka b"
+      using kalb by auto
+    then show ?thesis
+      by auto
+  qed
+next
+  case False
+  then have "c \<ge> b" by simp
 
-    obtain kb where kbdef: "kb = (a + b)/2" by blast
-    with alb have kblb: "kb < b" by auto
-    with kbdef cgeb have "a < kb \<and> kb < c" by auto
-    moreover hence "c \<notin> (closed_int a kb)" by (unfold closed_int_def, auto)
-    moreover from kblb have
-      "closed_int a kb \<subseteq> closed_int a b" by (unfold closed_int_def, auto)
-    ultimately have
-      "a < kb \<and>  closed_int a kb \<subseteq> closed_int a b \<and> c\<notin>closed_int a kb"
-      by simp
-    hence
-      "\<exists>ka kb. ka < kb \<and> closed_int ka kb \<subseteq> closed_int a b \<and> c \<notin> (closed_int ka kb)"
-      by auto
-  }
-  ultimately show ?thesis by (rule case_split)
+  def kb \<equiv> "(a + b)/2"
+  with `a < b` have "kb < b" by auto
+  with kb_def `c \<ge> b` have "a < kb" "kb < c" by auto
+  from `kb < c` have c: "c \<notin> closed_int a kb"
+    unfolding closed_int_def by auto
+  with `kb < b` have "closed_int a kb \<subseteq> closed_int a b"
+    unfolding closed_int_def by auto
+  with `a < kb` c have "a < kb \<and> closed_int a kb \<subseteq> closed_int a b \<and> c \<notin> closed_int a kb"
+    by simp
+  then show ?thesis by auto
 qed
 
 subsection {* newInt: Interval generation *}