17 deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" |
17 deriv :: "['a::real_normed_field \<Rightarrow> 'a, 'a, 'a] \<Rightarrow> bool" |
18 --{*Differentiation: D is derivative of function f at x*} |
18 --{*Differentiation: D is derivative of function f at x*} |
19 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where |
19 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where |
20 "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" |
20 "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" |
21 |
21 |
22 consts |
|
23 Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" |
|
24 primrec |
22 primrec |
25 "Bolzano_bisect P a b 0 = (a,b)" |
23 Bolzano_bisect :: "(real \<times> real \<Rightarrow> bool) \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> real \<times> real" where |
26 "Bolzano_bisect P a b (Suc n) = |
24 "Bolzano_bisect P a b 0 = (a, b)" |
27 (let (x,y) = Bolzano_bisect P a b n |
25 | "Bolzano_bisect P a b (Suc n) = |
28 in if P(x, (x+y)/2) then ((x+y)/2, y) |
26 (let (x, y) = Bolzano_bisect P a b n |
29 else (x, (x+y)/2))" |
27 in if P (x, (x+y) / 2) then ((x+y)/2, y) |
|
28 else (x, (x+y)/2))" |
30 |
29 |
31 |
30 |
32 subsection {* Derivatives *} |
31 subsection {* Derivatives *} |
33 |
32 |
34 lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)" |
33 lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)" |