src/HOL/SupInf.thy
 changeset 33609 059cd49e4b1e parent 33271 7be66dee1a5a child 33657 a4179bf442d1
```     1.1 --- a/src/HOL/SupInf.thy	Wed Nov 11 09:02:37 2009 +0100
1.2 +++ b/src/HOL/SupInf.thy	Wed Nov 11 14:04:56 2009 +0000
1.3 @@ -88,6 +88,12 @@
1.4    finally show "(LEAST z. \<forall>x\<in>X. x \<le> z) \<le> z" .
1.5  qed
1.6
1.7 +lemma less_SupE:
1.8 +  fixes y :: real
1.9 +  assumes "y < Sup X" "X \<noteq> {}"
1.10 +  obtains x where "x\<in>X" "y < x"
1.11 +by (metis SupInf.Sup_least assms linorder_not_less that)
1.12 +
1.13  lemma Sup_singleton [simp]: "Sup {x::real} = x"
1.14    by (force intro: Least_equality simp add: Sup_real_def)
1.15
1.16 @@ -459,4 +465,36 @@
1.17    ultimately show ?thesis by arith
1.18  qed
1.19
1.20 +lemma reals_complete_interval:
1.21 +  fixes a::real and b::real
1.22 +  assumes "a < b" and "P a" and "~P b"
1.23 +  shows "\<exists>c. a \<le> c & c \<le> b & (\<forall>x. a \<le> x & x < c --> P x) &
1.24 +             (\<forall>d. (\<forall>x. a \<le> x & x < d --> P x) --> d \<le> c)"
1.25 +proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto)
1.26 +  show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.27 +    by (rule SupInf.Sup_upper [where z=b], auto)
1.28 +       (metis prems real_le_linear real_less_def)
1.29 +next
1.30 +  show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b"
1.31 +    apply (rule SupInf.Sup_least)
1.32 +    apply (auto simp add: )
1.33 +    apply (metis less_le_not_le)
1.34 +    apply (metis `a<b` `~ P b` real_le_linear real_less_def)
1.35 +    done
1.36 +next
1.37 +  fix x
1.38 +  assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.39 +  show "P x"
1.40 +    apply (rule less_SupE [OF lt], auto)
1.41 +    apply (metis less_le_not_le)
1.42 +    apply (metis x)
1.43 +    done
1.44 +next
1.45 +  fix d
1.46 +    assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x"
1.47 +    thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}"
1.48 +      by (rule_tac z="b" in SupInf.Sup_upper, auto)
1.49 +         (metis `a<b` `~ P b` real_le_linear real_less_def)
1.50 +qed
1.51 +
1.52  end
```