2847 assumes [arith]: "a \<le> b" |
2847 assumes [arith]: "a \<le> b" |
2848 and trans: "\<And>a b c. P a b \<Longrightarrow> P b c \<Longrightarrow> a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> P a c" |
2848 and trans: "\<And>a b c. P a b \<Longrightarrow> P b c \<Longrightarrow> a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> P a c" |
2849 and 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" |
2849 and 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" |
2850 shows "P a b" |
2850 shows "P a b" |
2851 proof - |
2851 proof - |
2852 define bisect where "bisect = |
2852 define bisect where "bisect \<equiv> \<lambda>(x,y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2)" |
2853 rec_nat (a, b) (\<lambda>n (x, y). if P x ((x+y) / 2) then ((x+y)/2, y) else (x, (x+y)/2))" |
2853 define l u where "l n \<equiv> fst ((bisect^^n)(a,b))" and "u n \<equiv> snd ((bisect^^n)(a,b))" for n |
2854 define l u where "l n = fst (bisect n)" and "u n = snd (bisect n)" for n |
|
2855 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)" |
2854 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)" |
2856 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)" |
2855 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)" |
2857 by (simp_all add: l_def u_def bisect_def split: prod.split) |
2856 by (simp_all add: l_def u_def bisect_def split: prod.split) |
2858 |
2857 |
2859 have [simp]: "l n \<le> u n" for n by (induct n) auto |
2858 have [simp]: "l n \<le> u n" for n by (induct n) auto |