# HG changeset patch
# User hoelzl
# Date 1363945303 -3600
# Node ID 0c0efde246d1a32e0d0d3554cdb4980e29d95d9b
# Parent  ebf9d4fd00ba84ab425d9562f483beb94a29af5f
simplify proof of the Bolzano bisection lemma; use more meta-logic to state it; renamed lemma_Bolzano to Bolzano

diff -r ebf9d4fd00ba -r 0c0efde246d1 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -19,15 +19,6 @@
           ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where
   "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)"
 
-primrec
-  Bolzano_bisect :: "(real \<times> real \<Rightarrow> bool) \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real \<times> real" where
-  "Bolzano_bisect P a b 0 = (a, b)"
-  | "Bolzano_bisect P a b (Suc n) =
-      (let (x, y) = Bolzano_bisect P a b n
-       in if P (x, (x+y) / 2) then ((x+y)/2, y)
-                              else (x, (x+y)/2))"
-
-
 subsection {* Derivatives *}
 
 lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)"
@@ -509,101 +500,61 @@
 apply (auto intro: LIMSEQ_unique)
 done
 
-text{*The universal quantifiers below are required for the declaration
-  of @{text Bolzano_nest_unique} below.*}
-
-lemma Bolzano_bisect_le:
- "a \<le> b ==> \<forall>n. fst (Bolzano_bisect P a b n) \<le> snd (Bolzano_bisect P a b n)"
-apply (rule allI)
-apply (induct_tac "n")
-apply (auto simp add: Let_def split_def)
-done
+lemma Bolzano[consumes 1, case_names trans local]:
+  fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
+  assumes [arith]: "a \<le> b"
+  assumes trans: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
+  assumes local: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<exists>d>0. \<forall>a b. a \<le> x \<and> x \<le> b \<and> b - a < d \<longrightarrow> P a b"
+  shows "P a b"
+proof -
+  def bisect \<equiv> "nat_rec (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))"
+  def l \<equiv> "\<lambda>n. fst (bisect n)" and u \<equiv> "\<lambda>n. snd (bisect n)"
+  have l[simp]: "l 0 = a" "\<And>n. l (Suc n) = (if P (l n) ((l n + u n) / 2) then (l n + u n) / 2 else l n)"
+    and u[simp]: "u 0 = b" "\<And>n. u (Suc n) = (if P (l n) ((l n + u n) / 2) then u n else (l n + u n) / 2)"
+    by (simp_all add: l_def u_def bisect_def split: prod.split)
 
-lemma Bolzano_bisect_fst_le_Suc: "a \<le> b ==>
-   \<forall>n. fst(Bolzano_bisect P a b n) \<le> fst (Bolzano_bisect P a b (Suc n))"
-apply (rule allI)
-apply (induct_tac "n")
-apply (auto simp add: Bolzano_bisect_le Let_def split_def)
-done
-
-lemma Bolzano_bisect_Suc_le_snd: "a \<le> b ==>
-   \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
-apply (rule allI)
-apply (induct_tac "n")
-apply (auto simp add: Bolzano_bisect_le Let_def split_def)
-done
-
-lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)"
-apply (auto)
-apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
-apply (simp)
-done
+  { fix n have "l n \<le> u n" by (induct n) auto } note this[simp]
 
-lemma Bolzano_bisect_diff:
-     "a \<le> b ==>
-      snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) =
-      (b-a) / (2 ^ n)"
-apply (induct "n")
-apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def)
-done
-
-lemmas Bolzano_nest_unique =
-    lemma_nest_unique
-    [OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le]
-
+  have "\<exists>x. ((\<forall>n. l n \<le> x) \<and> l ----> x) \<and> ((\<forall>n. x \<le> u n) \<and> u ----> x)"
+  proof (safe intro!: lemma_nest_unique)
+    fix n show "l n \<le> l (Suc n)" "u (Suc n) \<le> u n" by (induct n) auto
+  next
+    { fix n have "l n - u n = (a - b) / 2^n" by (induct n) (auto simp: field_simps) }
+    then show "(\<lambda>n. l n - u n) ----> 0" by (simp add: LIMSEQ_divide_realpow_zero)
+  qed fact
+  then obtain x where x: "\<And>n. l n \<le> x" "\<And>n. x \<le> u n" and "l ----> x" "u ----> x" by auto
+  obtain d where "0 < d" and d: "\<And>a b. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> b - a < d \<Longrightarrow> P a b"
+    using `l 0 \<le> x` `x \<le> u 0` local[of x] by auto
 
-lemma not_P_Bolzano_bisect:
-  assumes P:    "!!a b c. [| P(a,b); P(b,c); a \<le> b; b \<le> c|] ==> P(a,c)"
-      and notP: "~ P(a,b)"
-      and le:   "a \<le> b"
-  shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
-proof (induct n)
-  case 0 show ?case using notP by simp
- next
-  case (Suc n)
-  thus ?case
- by (auto simp del: surjective_pairing [symmetric]
-             simp add: Let_def split_def Bolzano_bisect_le [OF le]
-     P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"])
+  show "P a b"
+  proof (rule ccontr)
+    assume "\<not> P a b" 
+    { fix n have "\<not> P (l n) (u n)"
+      proof (induct n)
+        case (Suc n) with trans[of "l n" "(l n + u n) / 2" "u n"] show ?case by auto
+      qed (simp add: `\<not> P a b`) }
+    moreover
+    { have "eventually (\<lambda>n. x - d / 2 < l n) sequentially"
+        using `0 < d` `l ----> x` by (intro order_tendstoD[of _ x]) auto
+      moreover have "eventually (\<lambda>n. u n < x + d / 2) sequentially"
+        using `0 < d` `u ----> x` by (intro order_tendstoD[of _ x]) auto
+      ultimately have "eventually (\<lambda>n. P (l n) (u n)) sequentially"
+      proof eventually_elim
+        fix n assume "x - d / 2 < l n" "u n < x + d / 2"
+        from add_strict_mono[OF this] have "u n - l n < d" by simp
+        with x show "P (l n) (u n)" by (rule d)
+      qed }
+    ultimately show False by simp
+  qed
 qed
 
-(*Now we re-package P_prem as a formula*)
-lemma not_P_Bolzano_bisect':
-     "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
-         ~ P(a,b);  a \<le> b |] ==>
-      \<forall>n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))"
-by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE])
-
-
-
 lemma lemma_BOLZANO:
      "[| \<forall>a b c. P(a,b) & P(b,c) & a \<le> b & b \<le> c --> P(a,c);
          \<forall>x. \<exists>d::real. 0 < d &
                 (\<forall>a b. a \<le> x & x \<le> b & (b-a) < d --> P(a,b));
          a \<le> b |]
       ==> P(a,b)"
-apply (rule Bolzano_nest_unique [where P=P, THEN exE], assumption+)
-apply (rule tendsto_minus_cancel)
-apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero)
-apply (rule ccontr)
-apply (drule not_P_Bolzano_bisect', assumption+)
-apply (rename_tac "l")
-apply (drule_tac x = l in spec, clarify)
-apply (simp add: LIMSEQ_iff)
-apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
-apply (drule_tac P = "%r. 0<r --> ?Q r" and x = "d/2" in spec)
-apply (drule real_less_half_sum, auto)
-apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec)
-apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec)
-apply safe
-apply (simp_all (no_asm_simp))
-apply (rule_tac y = "abs (fst (Bolzano_bisect P a b (no + noa)) - l) + abs (snd (Bolzano_bisect P a b (no + noa)) - l)" in order_le_less_trans)
-apply (simp (no_asm_simp) add: abs_if)
-apply (rule real_sum_of_halves [THEN subst])
-apply (rule add_strict_mono)
-apply (simp_all add: diff_minus [symmetric])
-done
-
+  using Bolzano[of a b "\<lambda>a b. P (a, b)"] by metis
 
 lemma lemma_BOLZANO2: "((\<forall>a b c. (a \<le> b & b \<le> c & P(a,b) & P(b,c)) --> P(a,c)) &
        (\<forall>x. \<exists>d::real. 0 < d &