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 *}