src/HOL/Hyperreal/Deriv.thy
 author chaieb Mon Jul 21 13:36:59 2008 +0200 (2008-07-21) changeset 27668 6eb20b2cecf8 parent 26120 2dd43c63c100 permissions -rw-r--r--
Tuned and simplified proofs
 huffman@21164 ` 1` ```(* Title : Deriv.thy ``` huffman@21164 ` 2` ``` ID : \$Id\$ ``` huffman@21164 ` 3` ``` Author : Jacques D. Fleuriot ``` huffman@21164 ` 4` ``` Copyright : 1998 University of Cambridge ``` huffman@21164 ` 5` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2004 ``` huffman@21164 ` 6` ``` GMVT by Benjamin Porter, 2005 ``` huffman@21164 ` 7` ```*) ``` huffman@21164 ` 8` huffman@21164 ` 9` ```header{* Differentiation *} ``` huffman@21164 ` 10` huffman@21164 ` 11` ```theory Deriv ``` chaieb@26120 ` 12` ```imports Lim Univ_Poly ``` huffman@21164 ` 13` ```begin ``` huffman@21164 ` 14` huffman@22984 ` 15` ```text{*Standard Definitions*} ``` huffman@21164 ` 16` huffman@21164 ` 17` ```definition ``` huffman@21784 ` 18` ``` deriv :: "['a::real_normed_field \ 'a, 'a, 'a] \ bool" ``` huffman@21164 ` 19` ``` --{*Differentiation: D is derivative of function f at x*} ``` wenzelm@21404 ` 20` ``` ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) where ``` huffman@21784 ` 21` ``` "DERIV f x :> D = ((%h. (f(x + h) - f x) / h) -- 0 --> D)" ``` huffman@21164 ` 22` wenzelm@21404 ` 23` ```definition ``` huffman@21784 ` 24` ``` differentiable :: "['a::real_normed_field \ 'a, 'a] \ bool" ``` huffman@21784 ` 25` ``` (infixl "differentiable" 60) where ``` huffman@21164 ` 26` ``` "f differentiable x = (\D. DERIV f x :> D)" ``` huffman@21164 ` 27` huffman@21164 ` 28` huffman@21164 ` 29` ```consts ``` huffman@21164 ` 30` ``` Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" ``` huffman@21164 ` 31` ```primrec ``` huffman@21164 ` 32` ``` "Bolzano_bisect P a b 0 = (a,b)" ``` huffman@21164 ` 33` ``` "Bolzano_bisect P a b (Suc n) = ``` huffman@21164 ` 34` ``` (let (x,y) = Bolzano_bisect P a b n ``` huffman@21164 ` 35` ``` in if P(x, (x+y)/2) then ((x+y)/2, y) ``` huffman@21164 ` 36` ``` else (x, (x+y)/2))" ``` huffman@21164 ` 37` huffman@21164 ` 38` huffman@21164 ` 39` ```subsection {* Derivatives *} ``` huffman@21164 ` 40` huffman@21784 ` 41` ```lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --> D)" ``` huffman@21164 ` 42` ```by (simp add: deriv_def) ``` huffman@21164 ` 43` huffman@21784 ` 44` ```lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --> D" ``` huffman@21164 ` 45` ```by (simp add: deriv_def) ``` huffman@21164 ` 46` huffman@21164 ` 47` ```lemma DERIV_const [simp]: "DERIV (\x. k) x :> 0" ``` huffman@21164 ` 48` ```by (simp add: deriv_def) ``` huffman@21164 ` 49` huffman@23069 ` 50` ```lemma DERIV_ident [simp]: "DERIV (\x. x) x :> 1" ``` nipkow@23398 ` 51` ```by (simp add: deriv_def cong: LIM_cong) ``` huffman@21164 ` 52` huffman@21164 ` 53` ```lemma add_diff_add: ``` huffman@21164 ` 54` ``` fixes a b c d :: "'a::ab_group_add" ``` huffman@21164 ` 55` ``` shows "(a + c) - (b + d) = (a - b) + (c - d)" ``` huffman@21164 ` 56` ```by simp ``` huffman@21164 ` 57` huffman@21164 ` 58` ```lemma DERIV_add: ``` huffman@21164 ` 59` ``` "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + g x) x :> D + E" ``` huffman@21784 ` 60` ```by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add) ``` huffman@21164 ` 61` huffman@21164 ` 62` ```lemma DERIV_minus: ``` huffman@21164 ` 63` ``` "DERIV f x :> D \ DERIV (\x. - f x) x :> - D" ``` huffman@21784 ` 64` ```by (simp only: deriv_def minus_diff_minus divide_minus_left LIM_minus) ``` huffman@21164 ` 65` huffman@21164 ` 66` ```lemma DERIV_diff: ``` huffman@21164 ` 67` ``` "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x - g x) x :> D - E" ``` huffman@21164 ` 68` ```by (simp only: diff_def DERIV_add DERIV_minus) ``` huffman@21164 ` 69` huffman@21164 ` 70` ```lemma DERIV_add_minus: ``` huffman@21164 ` 71` ``` "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\x. f x + - g x) x :> D + - E" ``` huffman@21164 ` 72` ```by (simp only: DERIV_add DERIV_minus) ``` huffman@21164 ` 73` huffman@21164 ` 74` ```lemma DERIV_isCont: "DERIV f x :> D \ isCont f x" ``` huffman@21164 ` 75` ```proof (unfold isCont_iff) ``` huffman@21164 ` 76` ``` assume "DERIV f x :> D" ``` huffman@21784 ` 77` ``` hence "(\h. (f(x+h) - f(x)) / h) -- 0 --> D" ``` huffman@21164 ` 78` ``` by (rule DERIV_D) ``` huffman@21784 ` 79` ``` hence "(\h. (f(x+h) - f(x)) / h * h) -- 0 --> D * 0" ``` huffman@23069 ` 80` ``` by (intro LIM_mult LIM_ident) ``` huffman@21784 ` 81` ``` hence "(\h. (f(x+h) - f(x)) * (h / h)) -- 0 --> 0" ``` huffman@21784 ` 82` ``` by simp ``` huffman@21784 ` 83` ``` hence "(\h. f(x+h) - f(x)) -- 0 --> 0" ``` nipkow@23398 ` 84` ``` by (simp cong: LIM_cong) ``` huffman@21164 ` 85` ``` thus "(\h. f(x+h)) -- 0 --> f(x)" ``` huffman@21164 ` 86` ``` by (simp add: LIM_def) ``` huffman@21164 ` 87` ```qed ``` huffman@21164 ` 88` huffman@21164 ` 89` ```lemma DERIV_mult_lemma: ``` huffman@21784 ` 90` ``` fixes a b c d :: "'a::real_field" ``` huffman@21784 ` 91` ``` shows "(a * b - c * d) / h = a * ((b - d) / h) + ((a - c) / h) * d" ``` nipkow@23477 ` 92` ```by (simp add: diff_minus add_divide_distrib [symmetric] ring_distribs) ``` huffman@21164 ` 93` huffman@21164 ` 94` ```lemma DERIV_mult': ``` huffman@21164 ` 95` ``` assumes f: "DERIV f x :> D" ``` huffman@21164 ` 96` ``` assumes g: "DERIV g x :> E" ``` huffman@21164 ` 97` ``` shows "DERIV (\x. f x * g x) x :> f x * E + D * g x" ``` huffman@21164 ` 98` ```proof (unfold deriv_def) ``` huffman@21164 ` 99` ``` from f have "isCont f x" ``` huffman@21164 ` 100` ``` by (rule DERIV_isCont) ``` huffman@21164 ` 101` ``` hence "(\h. f(x+h)) -- 0 --> f x" ``` huffman@21164 ` 102` ``` by (simp only: isCont_iff) ``` huffman@21784 ` 103` ``` hence "(\h. f(x+h) * ((g(x+h) - g x) / h) + ``` huffman@21784 ` 104` ``` ((f(x+h) - f x) / h) * g x) ``` huffman@21164 ` 105` ``` -- 0 --> f x * E + D * g x" ``` huffman@22613 ` 106` ``` by (intro LIM_add LIM_mult LIM_const DERIV_D f g) ``` huffman@21784 ` 107` ``` thus "(\h. (f(x+h) * g(x+h) - f x * g x) / h) ``` huffman@21164 ` 108` ``` -- 0 --> f x * E + D * g x" ``` huffman@21164 ` 109` ``` by (simp only: DERIV_mult_lemma) ``` huffman@21164 ` 110` ```qed ``` huffman@21164 ` 111` huffman@21164 ` 112` ```lemma DERIV_mult: ``` huffman@21164 ` 113` ``` "[| DERIV f x :> Da; DERIV g x :> Db |] ``` huffman@21164 ` 114` ``` ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" ``` huffman@21164 ` 115` ```by (drule (1) DERIV_mult', simp only: mult_commute add_commute) ``` huffman@21164 ` 116` huffman@21164 ` 117` ```lemma DERIV_unique: ``` huffman@21164 ` 118` ``` "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E" ``` huffman@21164 ` 119` ```apply (simp add: deriv_def) ``` huffman@21164 ` 120` ```apply (blast intro: LIM_unique) ``` huffman@21164 ` 121` ```done ``` huffman@21164 ` 122` huffman@21164 ` 123` ```text{*Differentiation of finite sum*} ``` huffman@21164 ` 124` huffman@21164 ` 125` ```lemma DERIV_sumr [rule_format (no_asm)]: ``` huffman@21164 ` 126` ``` "(\r. m \ r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) ``` huffman@21164 ` 127` ``` --> DERIV (%x. \n=m.. (\r=m.. D) = ``` huffman@21164 ` 136` ``` ((%x. (f(x)-f(a)) / (x-a)) -- a --> D)" ``` huffman@21164 ` 137` ```apply (rule iffI) ``` huffman@21164 ` 138` ```apply (drule_tac k="- a" in LIM_offset) ``` huffman@21164 ` 139` ```apply (simp add: diff_minus) ``` huffman@21164 ` 140` ```apply (drule_tac k="a" in LIM_offset) ``` huffman@21164 ` 141` ```apply (simp add: add_commute) ``` huffman@21164 ` 142` ```done ``` huffman@21164 ` 143` huffman@21784 ` 144` ```lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)" ``` huffman@21784 ` 145` ```by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff) ``` huffman@21164 ` 146` huffman@21164 ` 147` ```lemma inverse_diff_inverse: ``` huffman@21164 ` 148` ``` "\(a::'a::division_ring) \ 0; b \ 0\ ``` huffman@21164 ` 149` ``` \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" ``` nipkow@23477 ` 150` ```by (simp add: ring_simps) ``` huffman@21164 ` 151` huffman@21164 ` 152` ```lemma DERIV_inverse_lemma: ``` huffman@21784 ` 153` ``` "\a \ 0; b \ (0::'a::real_normed_field)\ ``` huffman@21784 ` 154` ``` \ (inverse a - inverse b) / h ``` huffman@21784 ` 155` ``` = - (inverse a * ((a - b) / h) * inverse b)" ``` huffman@21164 ` 156` ```by (simp add: inverse_diff_inverse) ``` huffman@21164 ` 157` huffman@21164 ` 158` ```lemma DERIV_inverse': ``` huffman@21164 ` 159` ``` assumes der: "DERIV f x :> D" ``` huffman@21164 ` 160` ``` assumes neq: "f x \ 0" ``` huffman@21164 ` 161` ``` shows "DERIV (\x. inverse (f x)) x :> - (inverse (f x) * D * inverse (f x))" ``` huffman@21164 ` 162` ``` (is "DERIV _ _ :> ?E") ``` huffman@21164 ` 163` ```proof (unfold DERIV_iff2) ``` huffman@21164 ` 164` ``` from der have lim_f: "f -- x --> f x" ``` huffman@21164 ` 165` ``` by (rule DERIV_isCont [unfolded isCont_def]) ``` huffman@21164 ` 166` huffman@21164 ` 167` ``` from neq have "0 < norm (f x)" by simp ``` huffman@21164 ` 168` ``` with LIM_D [OF lim_f] obtain s ``` huffman@21164 ` 169` ``` where s: "0 < s" ``` huffman@21164 ` 170` ``` and less_fx: "\z. \z \ x; norm (z - x) < s\ ``` huffman@21164 ` 171` ``` \ norm (f z - f x) < norm (f x)" ``` huffman@21164 ` 172` ``` by fast ``` huffman@21164 ` 173` huffman@21784 ` 174` ``` show "(\z. (inverse (f z) - inverse (f x)) / (z - x)) -- x --> ?E" ``` huffman@21164 ` 175` ``` proof (rule LIM_equal2 [OF s]) ``` huffman@21784 ` 176` ``` fix z ``` huffman@21164 ` 177` ``` assume "z \ x" "norm (z - x) < s" ``` huffman@21164 ` 178` ``` hence "norm (f z - f x) < norm (f x)" by (rule less_fx) ``` huffman@21164 ` 179` ``` hence "f z \ 0" by auto ``` huffman@21784 ` 180` ``` thus "(inverse (f z) - inverse (f x)) / (z - x) = ``` huffman@21784 ` 181` ``` - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))" ``` huffman@21164 ` 182` ``` using neq by (rule DERIV_inverse_lemma) ``` huffman@21164 ` 183` ``` next ``` huffman@21784 ` 184` ``` from der have "(\z. (f z - f x) / (z - x)) -- x --> D" ``` huffman@21164 ` 185` ``` by (unfold DERIV_iff2) ``` huffman@21784 ` 186` ``` thus "(\z. - (inverse (f z) * ((f z - f x) / (z - x)) * inverse (f x))) ``` huffman@21164 ` 187` ``` -- x --> ?E" ``` huffman@22613 ` 188` ``` by (intro LIM_mult LIM_inverse LIM_minus LIM_const lim_f neq) ``` huffman@21164 ` 189` ``` qed ``` huffman@21164 ` 190` ```qed ``` huffman@21164 ` 191` huffman@21164 ` 192` ```lemma DERIV_divide: ``` huffman@21784 ` 193` ``` "\DERIV f x :> D; DERIV g x :> E; g x \ 0\ ``` huffman@21784 ` 194` ``` \ DERIV (\x. f x / g x) x :> (D * g x - f x * E) / (g x * g x)" ``` huffman@21164 ` 195` ```apply (subgoal_tac "f x * - (inverse (g x) * E * inverse (g x)) + ``` huffman@21164 ` 196` ``` D * inverse (g x) = (D * g x - f x * E) / (g x * g x)") ``` huffman@21164 ` 197` ```apply (erule subst) ``` huffman@21164 ` 198` ```apply (unfold divide_inverse) ``` huffman@21164 ` 199` ```apply (erule DERIV_mult') ``` huffman@21164 ` 200` ```apply (erule (1) DERIV_inverse') ``` nipkow@23477 ` 201` ```apply (simp add: ring_distribs nonzero_inverse_mult_distrib) ``` huffman@21164 ` 202` ```apply (simp add: mult_ac) ``` huffman@21164 ` 203` ```done ``` huffman@21164 ` 204` huffman@21164 ` 205` ```lemma DERIV_power_Suc: ``` huffman@21784 ` 206` ``` fixes f :: "'a \ 'a::{real_normed_field,recpower}" ``` huffman@21164 ` 207` ``` assumes f: "DERIV f x :> D" ``` huffman@23431 ` 208` ``` shows "DERIV (\x. f x ^ Suc n) x :> (1 + of_nat n) * (D * f x ^ n)" ``` huffman@21164 ` 209` ```proof (induct n) ``` huffman@21164 ` 210` ```case 0 ``` huffman@21164 ` 211` ``` show ?case by (simp add: power_Suc f) ``` huffman@21164 ` 212` ```case (Suc k) ``` huffman@21164 ` 213` ``` from DERIV_mult' [OF f Suc] show ?case ``` nipkow@23477 ` 214` ``` apply (simp only: of_nat_Suc ring_distribs mult_1_left) ``` huffman@23431 ` 215` ``` apply (simp only: power_Suc right_distrib mult_ac add_ac) ``` huffman@21164 ` 216` ``` done ``` huffman@21164 ` 217` ```qed ``` huffman@21164 ` 218` huffman@21164 ` 219` ```lemma DERIV_power: ``` huffman@21784 ` 220` ``` fixes f :: "'a \ 'a::{real_normed_field,recpower}" ``` huffman@21164 ` 221` ``` assumes f: "DERIV f x :> D" ``` huffman@21784 ` 222` ``` shows "DERIV (\x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))" ``` huffman@21164 ` 223` ```by (cases "n", simp, simp add: DERIV_power_Suc f) ``` huffman@21164 ` 224` huffman@21164 ` 225` huffman@21164 ` 226` ```(* ------------------------------------------------------------------------ *) ``` huffman@21164 ` 227` ```(* Caratheodory formulation of derivative at a point: standard proof *) ``` huffman@21164 ` 228` ```(* ------------------------------------------------------------------------ *) ``` huffman@21164 ` 229` huffman@21164 ` 230` ```lemma CARAT_DERIV: ``` huffman@21164 ` 231` ``` "(DERIV f x :> l) = ``` huffman@21784 ` 232` ``` (\g. (\z. f z - f x = g z * (z-x)) & isCont g x & g x = l)" ``` huffman@21164 ` 233` ``` (is "?lhs = ?rhs") ``` huffman@21164 ` 234` ```proof ``` huffman@21164 ` 235` ``` assume der: "DERIV f x :> l" ``` huffman@21784 ` 236` ``` show "\g. (\z. f z - f x = g z * (z-x)) \ isCont g x \ g x = l" ``` huffman@21164 ` 237` ``` proof (intro exI conjI) ``` huffman@21784 ` 238` ``` let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))" ``` nipkow@23413 ` 239` ``` show "\z. f z - f x = ?g z * (z-x)" by simp ``` huffman@21164 ` 240` ``` show "isCont ?g x" using der ``` huffman@21164 ` 241` ``` by (simp add: isCont_iff DERIV_iff diff_minus ``` huffman@21164 ` 242` ``` cong: LIM_equal [rule_format]) ``` huffman@21164 ` 243` ``` show "?g x = l" by simp ``` huffman@21164 ` 244` ``` qed ``` huffman@21164 ` 245` ```next ``` huffman@21164 ` 246` ``` assume "?rhs" ``` huffman@21164 ` 247` ``` then obtain g where ``` huffman@21784 ` 248` ``` "(\z. f z - f x = g z * (z-x))" and "isCont g x" and "g x = l" by blast ``` huffman@21164 ` 249` ``` thus "(DERIV f x :> l)" ``` nipkow@23413 ` 250` ``` by (auto simp add: isCont_iff DERIV_iff cong: LIM_cong) ``` huffman@21164 ` 251` ```qed ``` huffman@21164 ` 252` huffman@21164 ` 253` ```lemma DERIV_chain': ``` huffman@21164 ` 254` ``` assumes f: "DERIV f x :> D" ``` huffman@21164 ` 255` ``` assumes g: "DERIV g (f x) :> E" ``` huffman@21784 ` 256` ``` shows "DERIV (\x. g (f x)) x :> E * D" ``` huffman@21164 ` 257` ```proof (unfold DERIV_iff2) ``` huffman@21784 ` 258` ``` obtain d where d: "\y. g y - g (f x) = d y * (y - f x)" ``` huffman@21164 ` 259` ``` and cont_d: "isCont d (f x)" and dfx: "d (f x) = E" ``` huffman@21164 ` 260` ``` using CARAT_DERIV [THEN iffD1, OF g] by fast ``` huffman@21164 ` 261` ``` from f have "f -- x --> f x" ``` huffman@21164 ` 262` ``` by (rule DERIV_isCont [unfolded isCont_def]) ``` huffman@21164 ` 263` ``` with cont_d have "(\z. d (f z)) -- x --> d (f x)" ``` huffman@21239 ` 264` ``` by (rule isCont_LIM_compose) ``` huffman@21784 ` 265` ``` hence "(\z. d (f z) * ((f z - f x) / (z - x))) ``` huffman@21784 ` 266` ``` -- x --> d (f x) * D" ``` huffman@21784 ` 267` ``` by (rule LIM_mult [OF _ f [unfolded DERIV_iff2]]) ``` huffman@21784 ` 268` ``` thus "(\z. (g (f z) - g (f x)) / (z - x)) -- x --> E * D" ``` huffman@21164 ` 269` ``` by (simp add: d dfx real_scaleR_def) ``` huffman@21164 ` 270` ```qed ``` huffman@21164 ` 271` huffman@21164 ` 272` ```(* let's do the standard proof though theorem *) ``` huffman@21164 ` 273` ```(* LIM_mult2 follows from a NS proof *) ``` huffman@21164 ` 274` huffman@21164 ` 275` ```lemma DERIV_cmult: ``` huffman@21164 ` 276` ``` "DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D" ``` huffman@21164 ` 277` ```by (drule DERIV_mult' [OF DERIV_const], simp) ``` huffman@21164 ` 278` huffman@21164 ` 279` ```(* standard version *) ``` huffman@21164 ` 280` ```lemma DERIV_chain: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (f o g) x :> Da * Db" ``` huffman@21164 ` 281` ```by (drule (1) DERIV_chain', simp add: o_def real_scaleR_def mult_commute) ``` huffman@21164 ` 282` huffman@21164 ` 283` ```lemma DERIV_chain2: "[| DERIV f (g x) :> Da; DERIV g x :> Db |] ==> DERIV (%x. f (g x)) x :> Da * Db" ``` huffman@21164 ` 284` ```by (auto dest: DERIV_chain simp add: o_def) ``` huffman@21164 ` 285` huffman@21164 ` 286` ```(*derivative of linear multiplication*) ``` huffman@21164 ` 287` ```lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" ``` huffman@23069 ` 288` ```by (cut_tac c = c and x = x in DERIV_ident [THEN DERIV_cmult], simp) ``` huffman@21164 ` 289` huffman@21164 ` 290` ```lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n - Suc 0))" ``` huffman@23069 ` 291` ```apply (cut_tac DERIV_power [OF DERIV_ident]) ``` huffman@21164 ` 292` ```apply (simp add: real_scaleR_def real_of_nat_def) ``` huffman@21164 ` 293` ```done ``` huffman@21164 ` 294` huffman@21164 ` 295` ```text{*Power of -1*} ``` huffman@21164 ` 296` huffman@21784 ` 297` ```lemma DERIV_inverse: ``` huffman@21784 ` 298` ``` fixes x :: "'a::{real_normed_field,recpower}" ``` huffman@21784 ` 299` ``` shows "x \ 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ Suc (Suc 0)))" ``` huffman@23069 ` 300` ```by (drule DERIV_inverse' [OF DERIV_ident]) (simp add: power_Suc) ``` huffman@21164 ` 301` huffman@21164 ` 302` ```text{*Derivative of inverse*} ``` huffman@21784 ` 303` ```lemma DERIV_inverse_fun: ``` huffman@21784 ` 304` ``` fixes x :: "'a::{real_normed_field,recpower}" ``` huffman@21784 ` 305` ``` shows "[| DERIV f x :> d; f(x) \ 0 |] ``` huffman@21784 ` 306` ``` ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ Suc (Suc 0))))" ``` huffman@21784 ` 307` ```by (drule (1) DERIV_inverse') (simp add: mult_ac power_Suc nonzero_inverse_mult_distrib) ``` huffman@21164 ` 308` huffman@21164 ` 309` ```text{*Derivative of quotient*} ``` huffman@21784 ` 310` ```lemma DERIV_quotient: ``` huffman@21784 ` 311` ``` fixes x :: "'a::{real_normed_field,recpower}" ``` huffman@21784 ` 312` ``` shows "[| DERIV f x :> d; DERIV g x :> e; g(x) \ 0 |] ``` huffman@21784 ` 313` ``` ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ Suc (Suc 0))" ``` huffman@21784 ` 314` ```by (drule (2) DERIV_divide) (simp add: mult_commute power_Suc) ``` huffman@21164 ` 315` huffman@22984 ` 316` huffman@22984 ` 317` ```subsection {* Differentiability predicate *} ``` huffman@21164 ` 318` huffman@21164 ` 319` ```lemma differentiableD: "f differentiable x ==> \D. DERIV f x :> D" ``` huffman@21164 ` 320` ```by (simp add: differentiable_def) ``` huffman@21164 ` 321` huffman@21164 ` 322` ```lemma differentiableI: "DERIV f x :> D ==> f differentiable x" ``` huffman@21164 ` 323` ```by (force simp add: differentiable_def) ``` huffman@21164 ` 324` huffman@21164 ` 325` ```lemma differentiable_const: "(\z. a) differentiable x" ``` huffman@21164 ` 326` ``` apply (unfold differentiable_def) ``` huffman@21164 ` 327` ``` apply (rule_tac x=0 in exI) ``` huffman@21164 ` 328` ``` apply simp ``` huffman@21164 ` 329` ``` done ``` huffman@21164 ` 330` huffman@21164 ` 331` ```lemma differentiable_sum: ``` huffman@21164 ` 332` ``` assumes "f differentiable x" ``` huffman@21164 ` 333` ``` and "g differentiable x" ``` huffman@21164 ` 334` ``` shows "(\x. f x + g x) differentiable x" ``` huffman@21164 ` 335` ```proof - ``` huffman@21164 ` 336` ``` from prems have "\D. DERIV f x :> D" by (unfold differentiable_def) ``` huffman@21164 ` 337` ``` then obtain df where "DERIV f x :> df" .. ``` huffman@21164 ` 338` ``` moreover from prems have "\D. DERIV g x :> D" by (unfold differentiable_def) ``` huffman@21164 ` 339` ``` then obtain dg where "DERIV g x :> dg" .. ``` huffman@21164 ` 340` ``` ultimately have "DERIV (\x. f x + g x) x :> df + dg" by (rule DERIV_add) ``` huffman@21164 ` 341` ``` hence "\D. DERIV (\x. f x + g x) x :> D" by auto ``` huffman@21164 ` 342` ``` thus ?thesis by (fold differentiable_def) ``` huffman@21164 ` 343` ```qed ``` huffman@21164 ` 344` huffman@21164 ` 345` ```lemma differentiable_diff: ``` huffman@21164 ` 346` ``` assumes "f differentiable x" ``` huffman@21164 ` 347` ``` and "g differentiable x" ``` huffman@21164 ` 348` ``` shows "(\x. f x - g x) differentiable x" ``` huffman@21164 ` 349` ```proof - ``` huffman@21164 ` 350` ``` from prems have "f differentiable x" by simp ``` huffman@21164 ` 351` ``` moreover ``` huffman@21164 ` 352` ``` from prems have "\D. DERIV g x :> D" by (unfold differentiable_def) ``` huffman@21164 ` 353` ``` then obtain dg where "DERIV g x :> dg" .. ``` huffman@21164 ` 354` ``` then have "DERIV (\x. - g x) x :> -dg" by (rule DERIV_minus) ``` huffman@21164 ` 355` ``` hence "\D. DERIV (\x. - g x) x :> D" by auto ``` huffman@21164 ` 356` ``` hence "(\x. - g x) differentiable x" by (fold differentiable_def) ``` huffman@21164 ` 357` ``` ultimately ``` huffman@21164 ` 358` ``` show ?thesis ``` huffman@21784 ` 359` ``` by (auto simp: diff_def dest: differentiable_sum) ``` huffman@21164 ` 360` ```qed ``` huffman@21164 ` 361` huffman@21164 ` 362` ```lemma differentiable_mult: ``` huffman@21164 ` 363` ``` assumes "f differentiable x" ``` huffman@21164 ` 364` ``` and "g differentiable x" ``` huffman@21164 ` 365` ``` shows "(\x. f x * g x) differentiable x" ``` huffman@21164 ` 366` ```proof - ``` huffman@21164 ` 367` ``` from prems have "\D. DERIV f x :> D" by (unfold differentiable_def) ``` huffman@21164 ` 368` ``` then obtain df where "DERIV f x :> df" .. ``` huffman@21164 ` 369` ``` moreover from prems have "\D. DERIV g x :> D" by (unfold differentiable_def) ``` huffman@21164 ` 370` ``` then obtain dg where "DERIV g x :> dg" .. ``` huffman@21164 ` 371` ``` ultimately have "DERIV (\x. f x * g x) x :> df * g x + dg * f x" by (simp add: DERIV_mult) ``` huffman@21164 ` 372` ``` hence "\D. DERIV (\x. f x * g x) x :> D" by auto ``` huffman@21164 ` 373` ``` thus ?thesis by (fold differentiable_def) ``` huffman@21164 ` 374` ```qed ``` huffman@21164 ` 375` huffman@22984 ` 376` huffman@21164 ` 377` ```subsection {* Nested Intervals and Bisection *} ``` huffman@21164 ` 378` huffman@21164 ` 379` ```text{*Lemmas about nested intervals and proof by bisection (cf.Harrison). ``` huffman@21164 ` 380` ``` All considerably tidied by lcp.*} ``` huffman@21164 ` 381` huffman@21164 ` 382` ```lemma lemma_f_mono_add [rule_format (no_asm)]: "(\n. (f::nat=>real) n \ f (Suc n)) --> f m \ f(m + no)" ``` huffman@21164 ` 383` ```apply (induct "no") ``` huffman@21164 ` 384` ```apply (auto intro: order_trans) ``` huffman@21164 ` 385` ```done ``` huffman@21164 ` 386` huffman@21164 ` 387` ```lemma f_inc_g_dec_Beq_f: "[| \n. f(n) \ f(Suc n); ``` huffman@21164 ` 388` ``` \n. g(Suc n) \ g(n); ``` huffman@21164 ` 389` ``` \n. f(n) \ g(n) |] ``` huffman@21164 ` 390` ``` ==> Bseq (f :: nat \ real)" ``` huffman@21164 ` 391` ```apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI) ``` huffman@21164 ` 392` ```apply (induct_tac "n") ``` huffman@21164 ` 393` ```apply (auto intro: order_trans) ``` huffman@21164 ` 394` ```apply (rule_tac y = "g (Suc na)" in order_trans) ``` huffman@21164 ` 395` ```apply (induct_tac [2] "na") ``` huffman@21164 ` 396` ```apply (auto intro: order_trans) ``` huffman@21164 ` 397` ```done ``` huffman@21164 ` 398` huffman@21164 ` 399` ```lemma f_inc_g_dec_Beq_g: "[| \n. f(n) \ f(Suc n); ``` huffman@21164 ` 400` ``` \n. g(Suc n) \ g(n); ``` huffman@21164 ` 401` ``` \n. f(n) \ g(n) |] ``` huffman@21164 ` 402` ``` ==> Bseq (g :: nat \ real)" ``` huffman@21164 ` 403` ```apply (subst Bseq_minus_iff [symmetric]) ``` huffman@21164 ` 404` ```apply (rule_tac g = "%x. - (f x)" in f_inc_g_dec_Beq_f) ``` huffman@21164 ` 405` ```apply auto ``` huffman@21164 ` 406` ```done ``` huffman@21164 ` 407` huffman@21164 ` 408` ```lemma f_inc_imp_le_lim: ``` huffman@21164 ` 409` ``` fixes f :: "nat \ real" ``` huffman@21164 ` 410` ``` shows "\\n. f n \ f (Suc n); convergent f\ \ f n \ lim f" ``` huffman@21164 ` 411` ```apply (rule linorder_not_less [THEN iffD1]) ``` huffman@21164 ` 412` ```apply (auto simp add: convergent_LIMSEQ_iff LIMSEQ_iff monoseq_Suc) ``` huffman@21164 ` 413` ```apply (drule real_less_sum_gt_zero) ``` huffman@21164 ` 414` ```apply (drule_tac x = "f n + - lim f" in spec, safe) ``` huffman@21164 ` 415` ```apply (drule_tac P = "%na. no\na --> ?Q na" and x = "no + n" in spec, auto) ``` huffman@21164 ` 416` ```apply (subgoal_tac "lim f \ f (no + n) ") ``` huffman@21164 ` 417` ```apply (drule_tac no=no and m=n in lemma_f_mono_add) ``` huffman@21164 ` 418` ```apply (auto simp add: add_commute) ``` huffman@21164 ` 419` ```apply (induct_tac "no") ``` huffman@21164 ` 420` ```apply simp ``` huffman@21164 ` 421` ```apply (auto intro: order_trans simp add: diff_minus abs_if) ``` huffman@21164 ` 422` ```done ``` huffman@21164 ` 423` huffman@21164 ` 424` ```lemma lim_uminus: "convergent g ==> lim (%x. - g x) = - (lim g)" ``` huffman@21164 ` 425` ```apply (rule LIMSEQ_minus [THEN limI]) ``` huffman@21164 ` 426` ```apply (simp add: convergent_LIMSEQ_iff) ``` huffman@21164 ` 427` ```done ``` huffman@21164 ` 428` huffman@21164 ` 429` ```lemma g_dec_imp_lim_le: ``` huffman@21164 ` 430` ``` fixes g :: "nat \ real" ``` huffman@21164 ` 431` ``` shows "\\n. g (Suc n) \ g(n); convergent g\ \ lim g \ g n" ``` huffman@21164 ` 432` ```apply (subgoal_tac "- (g n) \ - (lim g) ") ``` huffman@21164 ` 433` ```apply (cut_tac [2] f = "%x. - (g x)" in f_inc_imp_le_lim) ``` huffman@21164 ` 434` ```apply (auto simp add: lim_uminus convergent_minus_iff [symmetric]) ``` huffman@21164 ` 435` ```done ``` huffman@21164 ` 436` huffman@21164 ` 437` ```lemma lemma_nest: "[| \n. f(n) \ f(Suc n); ``` huffman@21164 ` 438` ``` \n. g(Suc n) \ g(n); ``` huffman@21164 ` 439` ``` \n. f(n) \ g(n) |] ``` huffman@21164 ` 440` ``` ==> \l m :: real. l \ m & ((\n. f(n) \ l) & f ----> l) & ``` huffman@21164 ` 441` ``` ((\n. m \ g(n)) & g ----> m)" ``` huffman@21164 ` 442` ```apply (subgoal_tac "monoseq f & monoseq g") ``` huffman@21164 ` 443` ```prefer 2 apply (force simp add: LIMSEQ_iff monoseq_Suc) ``` huffman@21164 ` 444` ```apply (subgoal_tac "Bseq f & Bseq g") ``` huffman@21164 ` 445` ```prefer 2 apply (blast intro: f_inc_g_dec_Beq_f f_inc_g_dec_Beq_g) ``` huffman@21164 ` 446` ```apply (auto dest!: Bseq_monoseq_convergent simp add: convergent_LIMSEQ_iff) ``` huffman@21164 ` 447` ```apply (rule_tac x = "lim f" in exI) ``` huffman@21164 ` 448` ```apply (rule_tac x = "lim g" in exI) ``` huffman@21164 ` 449` ```apply (auto intro: LIMSEQ_le) ``` huffman@21164 ` 450` ```apply (auto simp add: f_inc_imp_le_lim g_dec_imp_lim_le convergent_LIMSEQ_iff) ``` huffman@21164 ` 451` ```done ``` huffman@21164 ` 452` huffman@21164 ` 453` ```lemma lemma_nest_unique: "[| \n. f(n) \ f(Suc n); ``` huffman@21164 ` 454` ``` \n. g(Suc n) \ g(n); ``` huffman@21164 ` 455` ``` \n. f(n) \ g(n); ``` huffman@21164 ` 456` ``` (%n. f(n) - g(n)) ----> 0 |] ``` huffman@21164 ` 457` ``` ==> \l::real. ((\n. f(n) \ l) & f ----> l) & ``` huffman@21164 ` 458` ``` ((\n. l \ g(n)) & g ----> l)" ``` huffman@21164 ` 459` ```apply (drule lemma_nest, auto) ``` huffman@21164 ` 460` ```apply (subgoal_tac "l = m") ``` huffman@21164 ` 461` ```apply (drule_tac [2] X = f in LIMSEQ_diff) ``` huffman@21164 ` 462` ```apply (auto intro: LIMSEQ_unique) ``` huffman@21164 ` 463` ```done ``` huffman@21164 ` 464` huffman@21164 ` 465` ```text{*The universal quantifiers below are required for the declaration ``` huffman@21164 ` 466` ``` of @{text Bolzano_nest_unique} below.*} ``` huffman@21164 ` 467` huffman@21164 ` 468` ```lemma Bolzano_bisect_le: ``` huffman@21164 ` 469` ``` "a \ b ==> \n. fst (Bolzano_bisect P a b n) \ snd (Bolzano_bisect P a b n)" ``` huffman@21164 ` 470` ```apply (rule allI) ``` huffman@21164 ` 471` ```apply (induct_tac "n") ``` huffman@21164 ` 472` ```apply (auto simp add: Let_def split_def) ``` huffman@21164 ` 473` ```done ``` huffman@21164 ` 474` huffman@21164 ` 475` ```lemma Bolzano_bisect_fst_le_Suc: "a \ b ==> ``` huffman@21164 ` 476` ``` \n. fst(Bolzano_bisect P a b n) \ fst (Bolzano_bisect P a b (Suc n))" ``` huffman@21164 ` 477` ```apply (rule allI) ``` huffman@21164 ` 478` ```apply (induct_tac "n") ``` huffman@21164 ` 479` ```apply (auto simp add: Bolzano_bisect_le Let_def split_def) ``` huffman@21164 ` 480` ```done ``` huffman@21164 ` 481` huffman@21164 ` 482` ```lemma Bolzano_bisect_Suc_le_snd: "a \ b ==> ``` huffman@21164 ` 483` ``` \n. snd(Bolzano_bisect P a b (Suc n)) \ snd (Bolzano_bisect P a b n)" ``` huffman@21164 ` 484` ```apply (rule allI) ``` huffman@21164 ` 485` ```apply (induct_tac "n") ``` huffman@21164 ` 486` ```apply (auto simp add: Bolzano_bisect_le Let_def split_def) ``` huffman@21164 ` 487` ```done ``` huffman@21164 ` 488` huffman@21164 ` 489` ```lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" ``` huffman@21164 ` 490` ```apply (auto) ``` huffman@21164 ` 491` ```apply (drule_tac f = "%u. (1/2) *u" in arg_cong) ``` huffman@21164 ` 492` ```apply (simp) ``` huffman@21164 ` 493` ```done ``` huffman@21164 ` 494` huffman@21164 ` 495` ```lemma Bolzano_bisect_diff: ``` huffman@21164 ` 496` ``` "a \ b ==> ``` huffman@21164 ` 497` ``` snd(Bolzano_bisect P a b n) - fst(Bolzano_bisect P a b n) = ``` huffman@21164 ` 498` ``` (b-a) / (2 ^ n)" ``` huffman@21164 ` 499` ```apply (induct "n") ``` huffman@21164 ` 500` ```apply (auto simp add: eq_divide_2_times_iff add_divide_distrib Let_def split_def) ``` huffman@21164 ` 501` ```done ``` huffman@21164 ` 502` huffman@21164 ` 503` ```lemmas Bolzano_nest_unique = ``` huffman@21164 ` 504` ``` lemma_nest_unique ``` huffman@21164 ` 505` ``` [OF Bolzano_bisect_fst_le_Suc Bolzano_bisect_Suc_le_snd Bolzano_bisect_le] ``` huffman@21164 ` 506` huffman@21164 ` 507` huffman@21164 ` 508` ```lemma not_P_Bolzano_bisect: ``` huffman@21164 ` 509` ``` assumes P: "!!a b c. [| P(a,b); P(b,c); a \ b; b \ c|] ==> P(a,c)" ``` huffman@21164 ` 510` ``` and notP: "~ P(a,b)" ``` huffman@21164 ` 511` ``` and le: "a \ b" ``` huffman@21164 ` 512` ``` shows "~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))" ``` huffman@21164 ` 513` ```proof (induct n) ``` huffman@23441 ` 514` ``` case 0 show ?case using notP by simp ``` huffman@21164 ` 515` ``` next ``` huffman@21164 ` 516` ``` case (Suc n) ``` huffman@21164 ` 517` ``` thus ?case ``` huffman@21164 ` 518` ``` by (auto simp del: surjective_pairing [symmetric] ``` huffman@21164 ` 519` ``` simp add: Let_def split_def Bolzano_bisect_le [OF le] ``` huffman@21164 ` 520` ``` P [of "fst (Bolzano_bisect P a b n)" _ "snd (Bolzano_bisect P a b n)"]) ``` huffman@21164 ` 521` ```qed ``` huffman@21164 ` 522` huffman@21164 ` 523` ```(*Now we re-package P_prem as a formula*) ``` huffman@21164 ` 524` ```lemma not_P_Bolzano_bisect': ``` huffman@21164 ` 525` ``` "[| \a b c. P(a,b) & P(b,c) & a \ b & b \ c --> P(a,c); ``` huffman@21164 ` 526` ``` ~ P(a,b); a \ b |] ==> ``` huffman@21164 ` 527` ``` \n. ~ P(fst(Bolzano_bisect P a b n), snd(Bolzano_bisect P a b n))" ``` huffman@21164 ` 528` ```by (blast elim!: not_P_Bolzano_bisect [THEN [2] rev_notE]) ``` huffman@21164 ` 529` huffman@21164 ` 530` huffman@21164 ` 531` huffman@21164 ` 532` ```lemma lemma_BOLZANO: ``` huffman@21164 ` 533` ``` "[| \a b c. P(a,b) & P(b,c) & a \ b & b \ c --> P(a,c); ``` huffman@21164 ` 534` ``` \x. \d::real. 0 < d & ``` huffman@21164 ` 535` ``` (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)); ``` huffman@21164 ` 536` ``` a \ b |] ``` huffman@21164 ` 537` ``` ==> P(a,b)" ``` huffman@21164 ` 538` ```apply (rule Bolzano_nest_unique [where P1=P, THEN exE], assumption+) ``` huffman@21164 ` 539` ```apply (rule LIMSEQ_minus_cancel) ``` huffman@21164 ` 540` ```apply (simp (no_asm_simp) add: Bolzano_bisect_diff LIMSEQ_divide_realpow_zero) ``` huffman@21164 ` 541` ```apply (rule ccontr) ``` huffman@21164 ` 542` ```apply (drule not_P_Bolzano_bisect', assumption+) ``` huffman@21164 ` 543` ```apply (rename_tac "l") ``` huffman@21164 ` 544` ```apply (drule_tac x = l in spec, clarify) ``` huffman@21164 ` 545` ```apply (simp add: LIMSEQ_def) ``` huffman@21164 ` 546` ```apply (drule_tac P = "%r. 0 ?Q r" and x = "d/2" in spec) ``` huffman@21164 ` 547` ```apply (drule_tac P = "%r. 0 ?Q r" and x = "d/2" in spec) ``` huffman@21164 ` 548` ```apply (drule real_less_half_sum, auto) ``` huffman@21164 ` 549` ```apply (drule_tac x = "fst (Bolzano_bisect P a b (no + noa))" in spec) ``` huffman@21164 ` 550` ```apply (drule_tac x = "snd (Bolzano_bisect P a b (no + noa))" in spec) ``` huffman@21164 ` 551` ```apply safe ``` huffman@21164 ` 552` ```apply (simp_all (no_asm_simp)) ``` huffman@21164 ` 553` ```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) ``` huffman@21164 ` 554` ```apply (simp (no_asm_simp) add: abs_if) ``` huffman@21164 ` 555` ```apply (rule real_sum_of_halves [THEN subst]) ``` huffman@21164 ` 556` ```apply (rule add_strict_mono) ``` huffman@21164 ` 557` ```apply (simp_all add: diff_minus [symmetric]) ``` huffman@21164 ` 558` ```done ``` huffman@21164 ` 559` huffman@21164 ` 560` huffman@21164 ` 561` ```lemma lemma_BOLZANO2: "((\a b c. (a \ b & b \ c & P(a,b) & P(b,c)) --> P(a,c)) & ``` huffman@21164 ` 562` ``` (\x. \d::real. 0 < d & ``` huffman@21164 ` 563` ``` (\a b. a \ x & x \ b & (b-a) < d --> P(a,b)))) ``` huffman@21164 ` 564` ``` --> (\a b. a \ b --> P(a,b))" ``` huffman@21164 ` 565` ```apply clarify ``` huffman@21164 ` 566` ```apply (blast intro: lemma_BOLZANO) ``` huffman@21164 ` 567` ```done ``` huffman@21164 ` 568` huffman@21164 ` 569` huffman@21164 ` 570` ```subsection {* Intermediate Value Theorem *} ``` huffman@21164 ` 571` huffman@21164 ` 572` ```text {*Prove Contrapositive by Bisection*} ``` huffman@21164 ` 573` huffman@21164 ` 574` ```lemma IVT: "[| f(a::real) \ (y::real); y \ f(b); ``` huffman@21164 ` 575` ``` a \ b; ``` huffman@21164 ` 576` ``` (\x. a \ x & x \ b --> isCont f x) |] ``` huffman@21164 ` 577` ``` ==> \x. a \ x & x \ b & f(x) = y" ``` huffman@21164 ` 578` ```apply (rule contrapos_pp, assumption) ``` huffman@21164 ` 579` ```apply (cut_tac P = "% (u,v) . a \ u & u \ v & v \ b --> ~ (f (u) \ y & y \ f (v))" in lemma_BOLZANO2) ``` huffman@21164 ` 580` ```apply safe ``` huffman@21164 ` 581` ```apply simp_all ``` huffman@21164 ` 582` ```apply (simp add: isCont_iff LIM_def) ``` huffman@21164 ` 583` ```apply (rule ccontr) ``` huffman@21164 ` 584` ```apply (subgoal_tac "a \ x & x \ b") ``` huffman@21164 ` 585` ``` prefer 2 ``` huffman@21164 ` 586` ``` apply simp ``` huffman@21164 ` 587` ``` apply (drule_tac P = "%d. 0 ?P d" and x = 1 in spec, arith) ``` huffman@21164 ` 588` ```apply (drule_tac x = x in spec)+ ``` huffman@21164 ` 589` ```apply simp ``` huffman@21164 ` 590` ```apply (drule_tac P = "%r. ?P r --> (\s>0. ?Q r s) " and x = "\y - f x\" in spec) ``` huffman@21164 ` 591` ```apply safe ``` huffman@21164 ` 592` ```apply simp ``` huffman@21164 ` 593` ```apply (drule_tac x = s in spec, clarify) ``` huffman@21164 ` 594` ```apply (cut_tac x = "f x" and y = y in linorder_less_linear, safe) ``` huffman@21164 ` 595` ```apply (drule_tac x = "ba-x" in spec) ``` huffman@21164 ` 596` ```apply (simp_all add: abs_if) ``` huffman@21164 ` 597` ```apply (drule_tac x = "aa-x" in spec) ``` huffman@21164 ` 598` ```apply (case_tac "x \ aa", simp_all) ``` huffman@21164 ` 599` ```done ``` huffman@21164 ` 600` huffman@21164 ` 601` ```lemma IVT2: "[| f(b::real) \ (y::real); y \ f(a); ``` huffman@21164 ` 602` ``` a \ b; ``` huffman@21164 ` 603` ``` (\x. a \ x & x \ b --> isCont f x) ``` huffman@21164 ` 604` ``` |] ==> \x. a \ x & x \ b & f(x) = y" ``` huffman@21164 ` 605` ```apply (subgoal_tac "- f a \ -y & -y \ - f b", clarify) ``` huffman@21164 ` 606` ```apply (drule IVT [where f = "%x. - f x"], assumption) ``` huffman@21164 ` 607` ```apply (auto intro: isCont_minus) ``` huffman@21164 ` 608` ```done ``` huffman@21164 ` 609` huffman@21164 ` 610` ```(*HOL style here: object-level formulations*) ``` huffman@21164 ` 611` ```lemma IVT_objl: "(f(a::real) \ (y::real) & y \ f(b) & a \ b & ``` huffman@21164 ` 612` ``` (\x. a \ x & x \ b --> isCont f x)) ``` huffman@21164 ` 613` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` huffman@21164 ` 614` ```apply (blast intro: IVT) ``` huffman@21164 ` 615` ```done ``` huffman@21164 ` 616` huffman@21164 ` 617` ```lemma IVT2_objl: "(f(b::real) \ (y::real) & y \ f(a) & a \ b & ``` huffman@21164 ` 618` ``` (\x. a \ x & x \ b --> isCont f x)) ``` huffman@21164 ` 619` ``` --> (\x. a \ x & x \ b & f(x) = y)" ``` huffman@21164 ` 620` ```apply (blast intro: IVT2) ``` huffman@21164 ` 621` ```done ``` huffman@21164 ` 622` huffman@21164 ` 623` ```text{*By bisection, function continuous on closed interval is bounded above*} ``` huffman@21164 ` 624` huffman@21164 ` 625` ```lemma isCont_bounded: ``` huffman@21164 ` 626` ``` "[| a \ b; \x. a \ x & x \ b --> isCont f x |] ``` huffman@21164 ` 627` ``` ==> \M::real. \x::real. a \ x & x \ b --> f(x) \ M" ``` huffman@21164 ` 628` ```apply (cut_tac P = "% (u,v) . a \ u & u \ v & v \ b --> (\M. \x. u \ x & x \ v --> f x \ M)" in lemma_BOLZANO2) ``` huffman@21164 ` 629` ```apply safe ``` huffman@21164 ` 630` ```apply simp_all ``` huffman@21164 ` 631` ```apply (rename_tac x xa ya M Ma) ``` huffman@21164 ` 632` ```apply (cut_tac x = M and y = Ma in linorder_linear, safe) ``` huffman@21164 ` 633` ```apply (rule_tac x = Ma in exI, clarify) ``` huffman@21164 ` 634` ```apply (cut_tac x = xb and y = xa in linorder_linear, force) ``` huffman@21164 ` 635` ```apply (rule_tac x = M in exI, clarify) ``` huffman@21164 ` 636` ```apply (cut_tac x = xb and y = xa in linorder_linear, force) ``` huffman@21164 ` 637` ```apply (case_tac "a \ x & x \ b") ``` huffman@21164 ` 638` ```apply (rule_tac [2] x = 1 in exI) ``` huffman@21164 ` 639` ```prefer 2 apply force ``` huffman@21164 ` 640` ```apply (simp add: LIM_def isCont_iff) ``` huffman@21164 ` 641` ```apply (drule_tac x = x in spec, auto) ``` huffman@21164 ` 642` ```apply (erule_tac V = "\M. \x. a \ x & x \ b & ~ f x \ M" in thin_rl) ``` huffman@21164 ` 643` ```apply (drule_tac x = 1 in spec, auto) ``` huffman@21164 ` 644` ```apply (rule_tac x = s in exI, clarify) ``` huffman@21164 ` 645` ```apply (rule_tac x = "\f x\ + 1" in exI, clarify) ``` huffman@21164 ` 646` ```apply (drule_tac x = "xa-x" in spec) ``` huffman@21164 ` 647` ```apply (auto simp add: abs_ge_self) ``` huffman@21164 ` 648` ```done ``` huffman@21164 ` 649` huffman@21164 ` 650` ```text{*Refine the above to existence of least upper bound*} ``` huffman@21164 ` 651` huffman@21164 ` 652` ```lemma lemma_reals_complete: "((\x. x \ S) & (\y. isUb UNIV S (y::real))) --> ``` huffman@21164 ` 653` ``` (\t. isLub UNIV S t)" ``` huffman@21164 ` 654` ```by (blast intro: reals_complete) ``` huffman@21164 ` 655` huffman@21164 ` 656` ```lemma isCont_has_Ub: "[| a \ b; \x. a \ x & x \ b --> isCont f x |] ``` huffman@21164 ` 657` ``` ==> \M::real. (\x::real. a \ x & x \ b --> f(x) \ M) & ``` huffman@21164 ` 658` ``` (\N. N < M --> (\x. a \ x & x \ b & N < f(x)))" ``` huffman@21164 ` 659` ```apply (cut_tac S = "Collect (%y. \x. a \ x & x \ b & y = f x)" ``` huffman@21164 ` 660` ``` in lemma_reals_complete) ``` huffman@21164 ` 661` ```apply auto ``` huffman@21164 ` 662` ```apply (drule isCont_bounded, assumption) ``` huffman@21164 ` 663` ```apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def) ``` huffman@21164 ` 664` ```apply (rule exI, auto) ``` huffman@21164 ` 665` ```apply (auto dest!: spec simp add: linorder_not_less) ``` huffman@21164 ` 666` ```done ``` huffman@21164 ` 667` huffman@21164 ` 668` ```text{*Now show that it attains its upper bound*} ``` huffman@21164 ` 669` huffman@21164 ` 670` ```lemma isCont_eq_Ub: ``` huffman@21164 ` 671` ``` assumes le: "a \ b" ``` huffman@21164 ` 672` ``` and con: "\x::real. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 673` ``` shows "\M::real. (\x. a \ x & x \ b --> f(x) \ M) & ``` huffman@21164 ` 674` ``` (\x. a \ x & x \ b & f(x) = M)" ``` huffman@21164 ` 675` ```proof - ``` huffman@21164 ` 676` ``` from isCont_has_Ub [OF le con] ``` huffman@21164 ` 677` ``` obtain M where M1: "\x. a \ x \ x \ b \ f x \ M" ``` huffman@21164 ` 678` ``` and M2: "!!N. N \x. a \ x \ x \ b \ N < f x" by blast ``` huffman@21164 ` 679` ``` show ?thesis ``` huffman@21164 ` 680` ``` proof (intro exI, intro conjI) ``` huffman@21164 ` 681` ``` show " \x. a \ x \ x \ b \ f x \ M" by (rule M1) ``` huffman@21164 ` 682` ``` show "\x. a \ x \ x \ b \ f x = M" ``` huffman@21164 ` 683` ``` proof (rule ccontr) ``` huffman@21164 ` 684` ``` assume "\ (\x. a \ x \ x \ b \ f x = M)" ``` huffman@21164 ` 685` ``` with M1 have M3: "\x. a \ x & x \ b --> f x < M" ``` huffman@21164 ` 686` ``` by (fastsimp simp add: linorder_not_le [symmetric]) ``` huffman@21164 ` 687` ``` hence "\x. a \ x & x \ b --> isCont (%x. inverse (M - f x)) x" ``` huffman@21164 ` 688` ``` by (auto simp add: isCont_inverse isCont_diff con) ``` huffman@21164 ` 689` ``` from isCont_bounded [OF le this] ``` huffman@21164 ` 690` ``` obtain k where k: "!!x. a \ x & x \ b --> inverse (M - f x) \ k" by auto ``` huffman@21164 ` 691` ``` have Minv: "!!x. a \ x & x \ b --> 0 < inverse (M - f (x))" ``` huffman@21164 ` 692` ``` by (simp add: M3 compare_rls) ``` huffman@21164 ` 693` ``` have "!!x. a \ x & x \ b --> inverse (M - f x) < k+1" using k ``` huffman@21164 ` 694` ``` by (auto intro: order_le_less_trans [of _ k]) ``` huffman@21164 ` 695` ``` with Minv ``` huffman@21164 ` 696` ``` have "!!x. a \ x & x \ b --> inverse(k+1) < inverse(inverse(M - f x))" ``` huffman@21164 ` 697` ``` by (intro strip less_imp_inverse_less, simp_all) ``` huffman@21164 ` 698` ``` hence invlt: "!!x. a \ x & x \ b --> inverse(k+1) < M - f x" ``` huffman@21164 ` 699` ``` by simp ``` huffman@21164 ` 700` ``` have "M - inverse (k+1) < M" using k [of a] Minv [of a] le ``` huffman@21164 ` 701` ``` by (simp, arith) ``` huffman@21164 ` 702` ``` from M2 [OF this] ``` huffman@21164 ` 703` ``` obtain x where ax: "a \ x & x \ b & M - inverse(k+1) < f x" .. ``` huffman@21164 ` 704` ``` thus False using invlt [of x] by force ``` huffman@21164 ` 705` ``` qed ``` huffman@21164 ` 706` ``` qed ``` huffman@21164 ` 707` ```qed ``` huffman@21164 ` 708` huffman@21164 ` 709` huffman@21164 ` 710` ```text{*Same theorem for lower bound*} ``` huffman@21164 ` 711` huffman@21164 ` 712` ```lemma isCont_eq_Lb: "[| a \ b; \x. a \ x & x \ b --> isCont f x |] ``` huffman@21164 ` 713` ``` ==> \M::real. (\x::real. a \ x & x \ b --> M \ f(x)) & ``` huffman@21164 ` 714` ``` (\x. a \ x & x \ b & f(x) = M)" ``` huffman@21164 ` 715` ```apply (subgoal_tac "\x. a \ x & x \ b --> isCont (%x. - (f x)) x") ``` huffman@21164 ` 716` ```prefer 2 apply (blast intro: isCont_minus) ``` huffman@21164 ` 717` ```apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub) ``` huffman@21164 ` 718` ```apply safe ``` huffman@21164 ` 719` ```apply auto ``` huffman@21164 ` 720` ```done ``` huffman@21164 ` 721` huffman@21164 ` 722` huffman@21164 ` 723` ```text{*Another version.*} ``` huffman@21164 ` 724` huffman@21164 ` 725` ```lemma isCont_Lb_Ub: "[|a \ b; \x. a \ x & x \ b --> isCont f x |] ``` huffman@21164 ` 726` ``` ==> \L M::real. (\x::real. a \ x & x \ b --> L \ f(x) & f(x) \ M) & ``` huffman@21164 ` 727` ``` (\y. L \ y & y \ M --> (\x. a \ x & x \ b & (f(x) = y)))" ``` huffman@21164 ` 728` ```apply (frule isCont_eq_Lb) ``` huffman@21164 ` 729` ```apply (frule_tac [2] isCont_eq_Ub) ``` huffman@21164 ` 730` ```apply (assumption+, safe) ``` huffman@21164 ` 731` ```apply (rule_tac x = "f x" in exI) ``` huffman@21164 ` 732` ```apply (rule_tac x = "f xa" in exI, simp, safe) ``` huffman@21164 ` 733` ```apply (cut_tac x = x and y = xa in linorder_linear, safe) ``` huffman@21164 ` 734` ```apply (cut_tac f = f and a = x and b = xa and y = y in IVT_objl) ``` huffman@21164 ` 735` ```apply (cut_tac [2] f = f and a = xa and b = x and y = y in IVT2_objl, safe) ``` huffman@21164 ` 736` ```apply (rule_tac [2] x = xb in exI) ``` huffman@21164 ` 737` ```apply (rule_tac [4] x = xb in exI, simp_all) ``` huffman@21164 ` 738` ```done ``` huffman@21164 ` 739` huffman@21164 ` 740` huffman@21164 ` 741` ```text{*If @{term "0 < f'(x)"} then @{term x} is Locally Strictly Increasing At The Right*} ``` huffman@21164 ` 742` huffman@21164 ` 743` ```lemma DERIV_left_inc: ``` huffman@21164 ` 744` ``` fixes f :: "real => real" ``` huffman@21164 ` 745` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 746` ``` and l: "0 < l" ``` huffman@21164 ` 747` ``` shows "\d > 0. \h > 0. h < d --> f(x) < f(x + h)" ``` huffman@21164 ` 748` ```proof - ``` huffman@21164 ` 749` ``` from l der [THEN DERIV_D, THEN LIM_D [where r = "l"]] ``` huffman@21164 ` 750` ``` have "\s > 0. (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l)" ``` huffman@21164 ` 751` ``` by (simp add: diff_minus) ``` huffman@21164 ` 752` ``` then obtain s ``` huffman@21164 ` 753` ``` where s: "0 < s" ``` huffman@21164 ` 754` ``` and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < l" ``` huffman@21164 ` 755` ``` by auto ``` huffman@21164 ` 756` ``` thus ?thesis ``` huffman@21164 ` 757` ``` proof (intro exI conjI strip) ``` huffman@23441 ` 758` ``` show "0 real" ``` huffman@21164 ` 775` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 776` ``` and l: "l < 0" ``` huffman@21164 ` 777` ``` shows "\d > 0. \h > 0. h < d --> f(x) < f(x-h)" ``` huffman@21164 ` 778` ```proof - ``` huffman@21164 ` 779` ``` from l der [THEN DERIV_D, THEN LIM_D [where r = "-l"]] ``` huffman@21164 ` 780` ``` have "\s > 0. (\z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < -l)" ``` huffman@21164 ` 781` ``` by (simp add: diff_minus) ``` huffman@21164 ` 782` ``` then obtain s ``` huffman@21164 ` 783` ``` where s: "0 < s" ``` huffman@21164 ` 784` ``` and all: "!!z. z \ 0 \ \z\ < s \ \(f(x+z) - f x) / z - l\ < -l" ``` huffman@21164 ` 785` ``` by auto ``` huffman@21164 ` 786` ``` thus ?thesis ``` huffman@21164 ` 787` ``` proof (intro exI conjI strip) ``` huffman@23441 ` 788` ``` show "0 real" ``` huffman@21164 ` 805` ``` assumes der: "DERIV f x :> l" ``` huffman@21164 ` 806` ``` and d: "0 < d" ``` huffman@21164 ` 807` ``` and le: "\y. \x-y\ < d --> f(y) \ f(x)" ``` huffman@21164 ` 808` ``` shows "l = 0" ``` huffman@21164 ` 809` ```proof (cases rule: linorder_cases [of l 0]) ``` huffman@23441 ` 810` ``` case equal thus ?thesis . ``` huffman@21164 ` 811` ```next ``` huffman@21164 ` 812` ``` case less ``` huffman@21164 ` 813` ``` from DERIV_left_dec [OF der less] ``` huffman@21164 ` 814` ``` obtain d' where d': "0 < d'" ``` huffman@21164 ` 815` ``` and lt: "\h > 0. h < d' \ f x < f (x-h)" by blast ``` huffman@21164 ` 816` ``` from real_lbound_gt_zero [OF d d'] ``` huffman@21164 ` 817` ``` obtain e where "0 < e \ e < d \ e < d'" .. ``` huffman@21164 ` 818` ``` with lt le [THEN spec [where x="x-e"]] ``` huffman@21164 ` 819` ``` show ?thesis by (auto simp add: abs_if) ``` huffman@21164 ` 820` ```next ``` huffman@21164 ` 821` ``` case greater ``` huffman@21164 ` 822` ``` from DERIV_left_inc [OF der greater] ``` huffman@21164 ` 823` ``` obtain d' where d': "0 < d'" ``` huffman@21164 ` 824` ``` and lt: "\h > 0. h < d' \ f x < f (x + h)" by blast ``` huffman@21164 ` 825` ``` from real_lbound_gt_zero [OF d d'] ``` huffman@21164 ` 826` ``` obtain e where "0 < e \ e < d \ e < d'" .. ``` huffman@21164 ` 827` ``` with lt le [THEN spec [where x="x+e"]] ``` huffman@21164 ` 828` ``` show ?thesis by (auto simp add: abs_if) ``` huffman@21164 ` 829` ```qed ``` huffman@21164 ` 830` huffman@21164 ` 831` huffman@21164 ` 832` ```text{*Similar theorem for a local minimum*} ``` huffman@21164 ` 833` ```lemma DERIV_local_min: ``` huffman@21164 ` 834` ``` fixes f :: "real => real" ``` huffman@21164 ` 835` ``` shows "[| DERIV f x :> l; 0 < d; \y. \x-y\ < d --> f(x) \ f(y) |] ==> l = 0" ``` huffman@21164 ` 836` ```by (drule DERIV_minus [THEN DERIV_local_max], auto) ``` huffman@21164 ` 837` huffman@21164 ` 838` huffman@21164 ` 839` ```text{*In particular, if a function is locally flat*} ``` huffman@21164 ` 840` ```lemma DERIV_local_const: ``` huffman@21164 ` 841` ``` fixes f :: "real => real" ``` huffman@21164 ` 842` ``` shows "[| DERIV f x :> l; 0 < d; \y. \x-y\ < d --> f(x) = f(y) |] ==> l = 0" ``` huffman@21164 ` 843` ```by (auto dest!: DERIV_local_max) ``` huffman@21164 ` 844` huffman@21164 ` 845` ```text{*Lemma about introducing open ball in open interval*} ``` huffman@21164 ` 846` ```lemma lemma_interval_lt: ``` huffman@21164 ` 847` ``` "[| a < x; x < b |] ``` huffman@21164 ` 848` ``` ==> \d::real. 0 < d & (\y. \x-y\ < d --> a < y & y < b)" ``` chaieb@27668 ` 849` huffman@22998 ` 850` ```apply (simp add: abs_less_iff) ``` huffman@21164 ` 851` ```apply (insert linorder_linear [of "x-a" "b-x"], safe) ``` huffman@21164 ` 852` ```apply (rule_tac x = "x-a" in exI) ``` huffman@21164 ` 853` ```apply (rule_tac [2] x = "b-x" in exI, auto) ``` huffman@21164 ` 854` ```done ``` huffman@21164 ` 855` huffman@21164 ` 856` ```lemma lemma_interval: "[| a < x; x < b |] ==> ``` huffman@21164 ` 857` ``` \d::real. 0 < d & (\y. \x-y\ < d --> a \ y & y \ b)" ``` huffman@21164 ` 858` ```apply (drule lemma_interval_lt, auto) ``` huffman@21164 ` 859` ```apply (auto intro!: exI) ``` huffman@21164 ` 860` ```done ``` huffman@21164 ` 861` huffman@21164 ` 862` ```text{*Rolle's Theorem. ``` huffman@21164 ` 863` ``` If @{term f} is defined and continuous on the closed interval ``` huffman@21164 ` 864` ``` @{text "[a,b]"} and differentiable on the open interval @{text "(a,b)"}, ``` huffman@21164 ` 865` ``` and @{term "f(a) = f(b)"}, ``` huffman@21164 ` 866` ``` then there exists @{text "x0 \ (a,b)"} such that @{term "f'(x0) = 0"}*} ``` huffman@21164 ` 867` ```theorem Rolle: ``` huffman@21164 ` 868` ``` assumes lt: "a < b" ``` huffman@21164 ` 869` ``` and eq: "f(a) = f(b)" ``` huffman@21164 ` 870` ``` and con: "\x. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 871` ``` and dif [rule_format]: "\x. a < x & x < b --> f differentiable x" ``` huffman@21784 ` 872` ``` shows "\z::real. a < z & z < b & DERIV f z :> 0" ``` huffman@21164 ` 873` ```proof - ``` huffman@21164 ` 874` ``` have le: "a \ b" using lt by simp ``` huffman@21164 ` 875` ``` from isCont_eq_Ub [OF le con] ``` huffman@21164 ` 876` ``` obtain x where x_max: "\z. a \ z \ z \ b \ f z \ f x" ``` huffman@21164 ` 877` ``` and alex: "a \ x" and xleb: "x \ b" ``` huffman@21164 ` 878` ``` by blast ``` huffman@21164 ` 879` ``` from isCont_eq_Lb [OF le con] ``` huffman@21164 ` 880` ``` obtain x' where x'_min: "\z. a \ z \ z \ b \ f x' \ f z" ``` huffman@21164 ` 881` ``` and alex': "a \ x'" and x'leb: "x' \ b" ``` huffman@21164 ` 882` ``` by blast ``` huffman@21164 ` 883` ``` show ?thesis ``` huffman@21164 ` 884` ``` proof cases ``` huffman@21164 ` 885` ``` assume axb: "a < x & x < b" ``` huffman@21164 ` 886` ``` --{*@{term f} attains its maximum within the interval*} ``` chaieb@27668 ` 887` ``` hence ax: "ay. \x-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 890` ``` by blast ``` huffman@21164 ` 891` ``` hence bound': "\y. \x-y\ < d \ f y \ f x" using x_max ``` huffman@21164 ` 892` ``` by blast ``` huffman@21164 ` 893` ``` from differentiableD [OF dif [OF axb]] ``` huffman@21164 ` 894` ``` obtain l where der: "DERIV f x :> l" .. ``` huffman@21164 ` 895` ``` have "l=0" by (rule DERIV_local_max [OF der d bound']) ``` huffman@21164 ` 896` ``` --{*the derivative at a local maximum is zero*} ``` huffman@21164 ` 897` ``` thus ?thesis using ax xb der by auto ``` huffman@21164 ` 898` ``` next ``` huffman@21164 ` 899` ``` assume notaxb: "~ (a < x & x < b)" ``` huffman@21164 ` 900` ``` hence xeqab: "x=a | x=b" using alex xleb by arith ``` huffman@21164 ` 901` ``` hence fb_eq_fx: "f b = f x" by (auto simp add: eq) ``` huffman@21164 ` 902` ``` show ?thesis ``` huffman@21164 ` 903` ``` proof cases ``` huffman@21164 ` 904` ``` assume ax'b: "a < x' & x' < b" ``` huffman@21164 ` 905` ``` --{*@{term f} attains its minimum within the interval*} ``` chaieb@27668 ` 906` ``` hence ax': "ay. \x'-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 909` ``` by blast ``` huffman@21164 ` 910` ``` hence bound': "\y. \x'-y\ < d \ f x' \ f y" using x'_min ``` huffman@21164 ` 911` ``` by blast ``` huffman@21164 ` 912` ``` from differentiableD [OF dif [OF ax'b]] ``` huffman@21164 ` 913` ``` obtain l where der: "DERIV f x' :> l" .. ``` huffman@21164 ` 914` ``` have "l=0" by (rule DERIV_local_min [OF der d bound']) ``` huffman@21164 ` 915` ``` --{*the derivative at a local minimum is zero*} ``` huffman@21164 ` 916` ``` thus ?thesis using ax' x'b der by auto ``` huffman@21164 ` 917` ``` next ``` huffman@21164 ` 918` ``` assume notax'b: "~ (a < x' & x' < b)" ``` huffman@21164 ` 919` ``` --{*@{term f} is constant througout the interval*} ``` huffman@21164 ` 920` ``` hence x'eqab: "x'=a | x'=b" using alex' x'leb by arith ``` huffman@21164 ` 921` ``` hence fb_eq_fx': "f b = f x'" by (auto simp add: eq) ``` huffman@21164 ` 922` ``` from dense [OF lt] ``` huffman@21164 ` 923` ``` obtain r where ar: "a < r" and rb: "r < b" by blast ``` huffman@21164 ` 924` ``` from lemma_interval [OF ar rb] ``` huffman@21164 ` 925` ``` obtain d where d: "0y. \r-y\ < d \ a \ y \ y \ b" ``` huffman@21164 ` 926` ``` by blast ``` huffman@21164 ` 927` ``` have eq_fb: "\z. a \ z --> z \ b --> f z = f b" ``` huffman@21164 ` 928` ``` proof (clarify) ``` huffman@21164 ` 929` ``` fix z::real ``` huffman@21164 ` 930` ``` assume az: "a \ z" and zb: "z \ b" ``` huffman@21164 ` 931` ``` show "f z = f b" ``` huffman@21164 ` 932` ``` proof (rule order_antisym) ``` huffman@21164 ` 933` ``` show "f z \ f b" by (simp add: fb_eq_fx x_max az zb) ``` huffman@21164 ` 934` ``` show "f b \ f z" by (simp add: fb_eq_fx' x'_min az zb) ``` huffman@21164 ` 935` ``` qed ``` huffman@21164 ` 936` ``` qed ``` huffman@21164 ` 937` ``` have bound': "\y. \r-y\ < d \ f r = f y" ``` huffman@21164 ` 938` ``` proof (intro strip) ``` huffman@21164 ` 939` ``` fix y::real ``` huffman@21164 ` 940` ``` assume lt: "\r-y\ < d" ``` huffman@21164 ` 941` ``` hence "f y = f b" by (simp add: eq_fb bound) ``` huffman@21164 ` 942` ``` thus "f r = f y" by (simp add: eq_fb ar rb order_less_imp_le) ``` huffman@21164 ` 943` ``` qed ``` huffman@21164 ` 944` ``` from differentiableD [OF dif [OF conjI [OF ar rb]]] ``` huffman@21164 ` 945` ``` obtain l where der: "DERIV f r :> l" .. ``` huffman@21164 ` 946` ``` have "l=0" by (rule DERIV_local_const [OF der d bound']) ``` huffman@21164 ` 947` ``` --{*the derivative of a constant function is zero*} ``` huffman@21164 ` 948` ``` thus ?thesis using ar rb der by auto ``` huffman@21164 ` 949` ``` qed ``` huffman@21164 ` 950` ``` qed ``` huffman@21164 ` 951` ```qed ``` huffman@21164 ` 952` huffman@21164 ` 953` huffman@21164 ` 954` ```subsection{*Mean Value Theorem*} ``` huffman@21164 ` 955` huffman@21164 ` 956` ```lemma lemma_MVT: ``` huffman@21164 ` 957` ``` "f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)" ``` huffman@21164 ` 958` ```proof cases ``` huffman@21164 ` 959` ``` assume "a=b" thus ?thesis by simp ``` huffman@21164 ` 960` ```next ``` huffman@21164 ` 961` ``` assume "a\b" ``` huffman@21164 ` 962` ``` hence ba: "b-a \ 0" by arith ``` huffman@21164 ` 963` ``` show ?thesis ``` huffman@21164 ` 964` ``` by (rule real_mult_left_cancel [OF ba, THEN iffD1], ``` huffman@21164 ` 965` ``` simp add: right_diff_distrib, ``` huffman@21164 ` 966` ``` simp add: left_diff_distrib) ``` huffman@21164 ` 967` ```qed ``` huffman@21164 ` 968` huffman@21164 ` 969` ```theorem MVT: ``` huffman@21164 ` 970` ``` assumes lt: "a < b" ``` huffman@21164 ` 971` ``` and con: "\x. a \ x & x \ b --> isCont f x" ``` huffman@21164 ` 972` ``` and dif [rule_format]: "\x. a < x & x < b --> f differentiable x" ``` huffman@21784 ` 973` ``` shows "\l z::real. a < z & z < b & DERIV f z :> l & ``` huffman@21164 ` 974` ``` (f(b) - f(a) = (b-a) * l)" ``` huffman@21164 ` 975` ```proof - ``` huffman@21164 ` 976` ``` let ?F = "%x. f x - ((f b - f a) / (b-a)) * x" ``` huffman@21164 ` 977` ``` have contF: "\x. a \ x \ x \ b \ isCont ?F x" using con ``` huffman@23069 ` 978` ``` by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident) ``` huffman@21164 ` 979` ``` have difF: "\x. a < x \ x < b \ ?F differentiable x" ``` huffman@21164 ` 980` ``` proof (clarify) ``` huffman@21164 ` 981` ``` fix x::real ``` huffman@21164 ` 982` ``` assume ax: "a < x" and xb: "x < b" ``` huffman@21164 ` 983` ``` from differentiableD [OF dif [OF conjI [OF ax xb]]] ``` huffman@21164 ` 984` ``` obtain l where der: "DERIV f x :> l" .. ``` huffman@21164 ` 985` ``` show "?F differentiable x" ``` huffman@21164 ` 986` ``` by (rule differentiableI [where D = "l - (f b - f a)/(b-a)"], ``` huffman@21164 ` 987` ``` blast intro: DERIV_diff DERIV_cmult_Id der) ``` huffman@21164 ` 988` ``` qed ``` huffman@21164 ` 989` ``` from Rolle [where f = ?F, OF lt lemma_MVT contF difF] ``` huffman@21164 ` 990` ``` obtain z where az: "a < z" and zb: "z < b" and der: "DERIV ?F z :> 0" ``` huffman@21164 ` 991` ``` by blast ``` huffman@21164 ` 992` ``` have "DERIV (%x. ((f b - f a)/(b-a)) * x) z :> (f b - f a)/(b-a)" ``` huffman@21164 ` 993` ``` by (rule DERIV_cmult_Id) ``` huffman@21164 ` 994` ``` hence derF: "DERIV (\x. ?F x + (f b - f a) / (b - a) * x) z ``` huffman@21164 ` 995` ``` :> 0 + (f b - f a) / (b - a)" ``` huffman@21164 ` 996` ``` by (rule DERIV_add [OF der]) ``` huffman@21164 ` 997` ``` show ?thesis ``` huffman@21164 ` 998` ``` proof (intro exI conjI) ``` huffman@23441 ` 999` ``` show "a < z" using az . ``` huffman@23441 ` 1000` ``` show "z < b" using zb . ``` huffman@21164 ` 1001` ``` show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp) ``` huffman@21164 ` 1002` ``` show "DERIV f z :> ((f b - f a)/(b-a))" using derF by simp ``` huffman@21164 ` 1003` ``` qed ``` huffman@21164 ` 1004` ```qed ``` huffman@21164 ` 1005` huffman@21164 ` 1006` huffman@21164 ` 1007` ```text{*A function is constant if its derivative is 0 over an interval.*} ``` huffman@21164 ` 1008` huffman@21164 ` 1009` ```lemma DERIV_isconst_end: ``` huffman@21164 ` 1010` ``` fixes f :: "real => real" ``` huffman@21164 ` 1011` ``` shows "[| a < b; ``` huffman@21164 ` 1012` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 1013` ``` \x. a < x & x < b --> DERIV f x :> 0 |] ``` huffman@21164 ` 1014` ``` ==> f b = f a" ``` huffman@21164 ` 1015` ```apply (drule MVT, assumption) ``` huffman@21164 ` 1016` ```apply (blast intro: differentiableI) ``` huffman@21164 ` 1017` ```apply (auto dest!: DERIV_unique simp add: diff_eq_eq) ``` huffman@21164 ` 1018` ```done ``` huffman@21164 ` 1019` huffman@21164 ` 1020` ```lemma DERIV_isconst1: ``` huffman@21164 ` 1021` ``` fixes f :: "real => real" ``` huffman@21164 ` 1022` ``` shows "[| a < b; ``` huffman@21164 ` 1023` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 1024` ``` \x. a < x & x < b --> DERIV f x :> 0 |] ``` huffman@21164 ` 1025` ``` ==> \x. a \ x & x \ b --> f x = f a" ``` huffman@21164 ` 1026` ```apply safe ``` huffman@21164 ` 1027` ```apply (drule_tac x = a in order_le_imp_less_or_eq, safe) ``` huffman@21164 ` 1028` ```apply (drule_tac b = x in DERIV_isconst_end, auto) ``` huffman@21164 ` 1029` ```done ``` huffman@21164 ` 1030` huffman@21164 ` 1031` ```lemma DERIV_isconst2: ``` huffman@21164 ` 1032` ``` fixes f :: "real => real" ``` huffman@21164 ` 1033` ``` shows "[| a < b; ``` huffman@21164 ` 1034` ``` \x. a \ x & x \ b --> isCont f x; ``` huffman@21164 ` 1035` ``` \x. a < x & x < b --> DERIV f x :> 0; ``` huffman@21164 ` 1036` ``` a \ x; x \ b |] ``` huffman@21164 ` 1037` ``` ==> f x = f a" ``` huffman@21164 ` 1038` ```apply (blast dest: DERIV_isconst1) ``` huffman@21164 ` 1039` ```done ``` huffman@21164 ` 1040` huffman@21164 ` 1041` ```lemma DERIV_isconst_all: ``` huffman@21164 ` 1042` ``` fixes f :: "real => real" ``` huffman@21164 ` 1043` ``` shows "\x. DERIV f x :> 0 ==> f(x) = f(y)" ``` huffman@21164 ` 1044` ```apply (rule linorder_cases [of x y]) ``` huffman@21164 ` 1045` ```apply (blast intro: sym DERIV_isCont DERIV_isconst_end)+ ``` huffman@21164 ` 1046` ```done ``` huffman@21164 ` 1047` huffman@21164 ` 1048` ```lemma DERIV_const_ratio_const: ``` huffman@21784 ` 1049` ``` fixes f :: "real => real" ``` huffman@21784 ` 1050` ``` shows "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a)) = (b-a) * k" ``` huffman@21164 ` 1051` ```apply (rule linorder_cases [of a b], auto) ``` huffman@21164 ` 1052` ```apply (drule_tac [!] f = f in MVT) ``` huffman@21164 ` 1053` ```apply (auto dest: DERIV_isCont DERIV_unique simp add: differentiable_def) ``` nipkow@23477 ` 1054` ```apply (auto dest: DERIV_unique simp add: ring_distribs diff_minus) ``` huffman@21164 ` 1055` ```done ``` huffman@21164 ` 1056` huffman@21164 ` 1057` ```lemma DERIV_const_ratio_const2: ``` huffman@21784 ` 1058` ``` fixes f :: "real => real" ``` huffman@21784 ` 1059` ``` shows "[|a \ b; \x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k" ``` huffman@21164 ` 1060` ```apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1]) ``` huffman@21164 ` 1061` ```apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc) ``` huffman@21164 ` 1062` ```done ``` huffman@21164 ` 1063` huffman@21164 ` 1064` ```lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)" ``` huffman@21164 ` 1065` ```by (simp) ``` huffman@21164 ` 1066` huffman@21164 ` 1067` ```lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)" ``` huffman@21164 ` 1068` ```by (simp) ``` huffman@21164 ` 1069` huffman@21164 ` 1070` ```text{*Gallileo's "trick": average velocity = av. of end velocities*} ``` huffman@21164 ` 1071` huffman@21164 ` 1072` ```lemma DERIV_const_average: ``` huffman@21164 ` 1073` ``` fixes v :: "real => real" ``` huffman@21164 ` 1074` ``` assumes neq: "a \ (b::real)" ``` huffman@21164 ` 1075` ``` and der: "\x. DERIV v x :> k" ``` huffman@21164 ` 1076` ``` shows "v ((a + b)/2) = (v a + v b)/2" ``` huffman@21164 ` 1077` ```proof (cases rule: linorder_cases [of a b]) ``` huffman@21164 ` 1078` ``` case equal with neq show ?thesis by simp ``` huffman@21164 ` 1079` ```next ``` huffman@21164 ` 1080` ``` case less ``` huffman@21164 ` 1081` ``` have "(v b - v a) / (b - a) = k" ``` huffman@21164 ` 1082` ``` by (rule DERIV_const_ratio_const2 [OF neq der]) ``` huffman@21164 ` 1083` ``` hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp ``` huffman@21164 ` 1084` ``` moreover have "(v ((a + b) / 2) - v a) / ((a + b) / 2 - a) = k" ``` huffman@21164 ` 1085` ``` by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq) ``` huffman@21164 ` 1086` ``` ultimately show ?thesis using neq by force ``` huffman@21164 ` 1087` ```next ``` huffman@21164 ` 1088` ``` case greater ``` huffman@21164 ` 1089` ``` have "(v b - v a) / (b - a) = k" ``` huffman@21164 ` 1090` ``` by (rule DERIV_const_ratio_const2 [OF neq der]) ``` huffman@21164 ` 1091` ``` hence "(b-a) * ((v b - v a) / (b-a)) = (b-a) * k" by simp ``` huffman@21164 ` 1092` ``` moreover have " (v ((b + a) / 2) - v a) / ((b + a) / 2 - a) = k" ``` huffman@21164 ` 1093` ``` by (rule DERIV_const_ratio_const2 [OF _ der], simp add: neq) ``` huffman@21164 ` 1094` ``` ultimately show ?thesis using neq by (force simp add: add_commute) ``` huffman@21164 ` 1095` ```qed ``` huffman@21164 ` 1096` huffman@21164 ` 1097` huffman@21164 ` 1098` ```text{*Dull lemma: an continuous injection on an interval must have a ``` huffman@21164 ` 1099` ```strict maximum at an end point, not in the middle.*} ``` huffman@21164 ` 1100` huffman@21164 ` 1101` ```lemma lemma_isCont_inj: ``` huffman@21164 ` 1102` ``` fixes f :: "real \ real" ``` huffman@21164 ` 1103` ``` assumes d: "0 < d" ``` huffman@21164 ` 1104` ``` and inj [rule_format]: "\z. \z-x\ \ d --> g(f z) = z" ``` huffman@21164 ` 1105` ``` and cont: "\z. \z-x\ \ d --> isCont f z" ``` huffman@21164 ` 1106` ``` shows "\z. \z-x\ \ d & f x < f z" ``` huffman@21164 ` 1107` ```proof (rule ccontr) ``` huffman@21164 ` 1108` ``` assume "~ (\z. \z-x\ \ d & f x < f z)" ``` huffman@21164 ` 1109` ``` hence all [rule_format]: "\z. \z - x\ \ d --> f z \ f x" by auto ``` huffman@21164 ` 1110` ``` show False ``` huffman@21164 ` 1111` ``` proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"]) ``` huffman@21164 ` 1112` ``` case le ``` huffman@21164 ` 1113` ``` from d cont all [of "x+d"] ``` huffman@21164 ` 1114` ``` have flef: "f(x+d) \ f x" ``` huffman@21164 ` 1115` ``` and xlex: "x - d \ x" ``` huffman@21164 ` 1116` ``` and cont': "\z. x - d \ z \ z \ x \ isCont f z" ``` huffman@21164 ` 1117` ``` by (auto simp add: abs_if) ``` huffman@21164 ` 1118` ``` from IVT [OF le flef xlex cont'] ``` huffman@21164 ` 1119` ``` obtain x' where "x-d \ x'" "x' \ x" "f x' = f(x+d)" by blast ``` huffman@21164 ` 1120` ``` moreover ``` huffman@21164 ` 1121` ``` hence "g(f x') = g (f(x+d))" by simp ``` huffman@21164 ` 1122` ``` ultimately show False using d inj [of x'] inj [of "x+d"] ``` huffman@22998 ` 1123` ``` by (simp add: abs_le_iff) ``` huffman@21164 ` 1124` ``` next ``` huffman@21164 ` 1125` ``` case ge ``` huffman@21164 ` 1126` ``` from d cont all [of "x-d"] ``` huffman@21164 ` 1127` ``` have flef: "f(x-d) \ f x" ``` huffman@21164 ` 1128` ``` and xlex: "x \ x+d" ``` huffman@21164 ` 1129` ``` and cont': "\z. x \ z \ z \ x+d \ isCont f z" ``` huffman@21164 ` 1130` ``` by (auto simp add: abs_if) ``` huffman@21164 ` 1131` ``` from IVT2 [OF ge flef xlex cont'] ``` huffman@21164 ` 1132` ``` obtain x' where "x \ x'" "x' \ x+d" "f x' = f(x-d)" by blast ``` huffman@21164 ` 1133` ``` moreover ``` huffman@21164 ` 1134` ``` hence "g(f x') = g (f(x-d))" by simp ``` huffman@21164 ` 1135` ``` ultimately show False using d inj [of x'] inj [of "x-d"] ``` huffman@22998 ` 1136` ``` by (simp add: abs_le_iff) ``` huffman@21164 ` 1137` ``` qed ``` huffman@21164 ` 1138` ```qed ``` huffman@21164 ` 1139` huffman@21164 ` 1140` huffman@21164 ` 1141` ```text{*Similar version for lower bound.*} ``` huffman@21164 ` 1142` huffman@21164 ` 1143` ```lemma lemma_isCont_inj2: ``` huffman@21164 ` 1144` ``` fixes f g :: "real \ real" ``` huffman@21164 ` 1145` ``` shows "[|0 < d; \z. \z-x\ \ d --> g(f z) = z; ``` huffman@21164 ` 1146` ``` \z. \z-x\ \ d --> isCont f z |] ``` huffman@21164 ` 1147` ``` ==> \z. \z-x\ \ d & f z < f x" ``` huffman@21164 ` 1148` ```apply (insert lemma_isCont_inj ``` huffman@21164 ` 1149` ``` [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d]) ``` huffman@21164 ` 1150` ```apply (simp add: isCont_minus linorder_not_le) ``` huffman@21164 ` 1151` ```done ``` huffman@21164 ` 1152` huffman@21164 ` 1153` ```text{*Show there's an interval surrounding @{term "f(x)"} in ``` huffman@21164 ` 1154` ```@{text "f[[x - d, x + d]]"} .*} ``` huffman@21164 ` 1155` huffman@21164 ` 1156` ```lemma isCont_inj_range: ``` huffman@21164 ` 1157` ``` fixes f :: "real \ real" ``` huffman@21164 ` 1158` ``` assumes d: "0 < d" ``` huffman@21164 ` 1159` ``` and inj: "\z. \z-x\ \ d --> g(f z) = z" ``` huffman@21164 ` 1160` ``` and cont: "\z. \z-x\ \ d --> isCont f z" ``` huffman@21164 ` 1161` ``` shows "\e>0. \y. \y - f x\ \ e --> (\z. \z-x\ \ d & f z = y)" ``` huffman@21164 ` 1162` ```proof - ``` huffman@21164 ` 1163` ``` have "x-d \ x+d" "\z. x-d \ z \ z \ x+d \ isCont f z" using cont d ``` huffman@22998 ` 1164` ``` by (auto simp add: abs_le_iff) ``` huffman@21164 ` 1165` ``` from isCont_Lb_Ub [OF this] ``` huffman@21164 ` 1166` ``` obtain L M ``` huffman@21164 ` 1167` ``` where all1 [rule_format]: "\z. x-d \ z \ z \ x+d \ L \ f z \ f z \ M" ``` huffman@21164 ` 1168` ``` and all2 [rule_format]: ``` huffman@21164 ` 1169` ``` "\y. L \ y \ y \ M \ (\z. x-d \ z \ z \ x+d \ f z = y)" ``` huffman@21164 ` 1170` ``` by auto ``` huffman@21164 ` 1171` ``` with d have "L \ f x & f x \ M" by simp ``` huffman@21164 ` 1172` ``` moreover have "L \ f x" ``` huffman@21164 ` 1173` ``` proof - ``` huffman@21164 ` 1174` ``` from lemma_isCont_inj2 [OF d inj cont] ``` huffman@21164 ` 1175` ``` obtain u where "\u - x\ \ d" "f u < f x" by auto ``` huffman@21164 ` 1176` ``` thus ?thesis using all1 [of u] by arith ``` huffman@21164 ` 1177` ``` qed ``` huffman@21164 ` 1178` ``` moreover have "f x \ M" ``` huffman@21164 ` 1179` ``` proof - ``` huffman@21164 ` 1180` ``` from lemma_isCont_inj [OF d inj cont] ``` huffman@21164 ` 1181` ``` obtain u where "\u - x\ \ d" "f x < f u" by auto ``` huffman@21164 ` 1182` ``` thus ?thesis using all1 [of u] by arith ``` huffman@21164 ` 1183` ``` qed ``` huffman@21164 ` 1184` ``` ultimately have "L < f x & f x < M" by arith ``` huffman@21164 ` 1185` ``` hence "0 < f x - L" "0 < M - f x" by arith+ ``` huffman@21164 ` 1186` ``` from real_lbound_gt_zero [OF this] ``` huffman@21164 ` 1187` ``` obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto ``` huffman@21164 ` 1188` ``` thus ?thesis ``` huffman@21164 ` 1189` ``` proof (intro exI conjI) ``` huffman@23441 ` 1190` ``` show "0y. \y - f x\ \ e \ (\z. \z - x\ \ d \ f z = y)" ``` huffman@21164 ` 1192` ``` proof (intro strip) ``` huffman@21164 ` 1193` ``` fix y::real ``` huffman@21164 ` 1194` ``` assume "\y - f x\ \ e" ``` huffman@21164 ` 1195` ``` with e have "L \ y \ y \ M" by arith ``` huffman@21164 ` 1196` ``` from all2 [OF this] ``` huffman@21164 ` 1197` ``` obtain z where "x - d \ z" "z \ x + d" "f z = y" by blast ``` chaieb@27668 ` 1198` ``` thus "\z. \z - x\ \ d \ f z = y" ``` huffman@22998 ` 1199` ``` by (force simp add: abs_le_iff) ``` huffman@21164 ` 1200` ``` qed ``` huffman@21164 ` 1201` ``` qed ``` huffman@21164 ` 1202` ```qed ``` huffman@21164 ` 1203` huffman@21164 ` 1204` huffman@21164 ` 1205` ```text{*Continuity of inverse function*} ``` huffman@21164 ` 1206` huffman@21164 ` 1207` ```lemma isCont_inverse_function: ``` huffman@21164 ` 1208` ``` fixes f g :: "real \ real" ``` huffman@21164 ` 1209` ``` assumes d: "0 < d" ``` huffman@21164 ` 1210` ``` and inj: "\z. \z-x\ \ d --> g(f z) = z" ``` huffman@21164 ` 1211` ``` and cont: "\z. \z-x\ \ d --> isCont f z" ``` huffman@21164 ` 1212` ``` shows "isCont g (f x)" ``` huffman@21164 ` 1213` ```proof (simp add: isCont_iff LIM_eq) ``` huffman@21164 ` 1214` ``` show "\r. 0 < r \ ``` huffman@21164 ` 1215` ``` (\s>0. \z. z\0 \ \z\ < s \ \g(f x + z) - g(f x)\ < r)" ``` huffman@21164 ` 1216` ``` proof (intro strip) ``` huffman@21164 ` 1217` ``` fix r::real ``` huffman@21164 ` 1218` ``` assume r: "0 e < d" by blast ``` huffman@21164 ` 1221` ``` with inj cont ``` huffman@21164 ` 1222` ``` have e_simps: "\z. \z-x\ \ e --> g (f z) = z" ``` huffman@21164 ` 1223` ``` "\z. \z-x\ \ e --> isCont f z" by auto ``` huffman@21164 ` 1224` ``` from isCont_inj_range [OF e this] ``` huffman@21164 ` 1225` ``` obtain e' where e': "0 < e'" ``` huffman@21164 ` 1226` ``` and all: "\y. \y - f x\ \ e' \ (\z. \z - x\ \ e \ f z = y)" ``` huffman@21164 ` 1227` ``` by blast ``` huffman@21164 ` 1228` ``` show "\s>0. \z. z\0 \ \z\ < s \ \g(f x + z) - g(f x)\ < r" ``` huffman@21164 ` 1229` ``` proof (intro exI conjI) ``` huffman@23441 ` 1230` ``` show "0z. z \ 0 \ \z\ < e' \ \g (f x + z) - g (f x)\ < r" ``` huffman@21164 ` 1232` ``` proof (intro strip) ``` huffman@21164 ` 1233` ``` fix z::real ``` huffman@21164 ` 1234` ``` assume z: "z \ 0 \ \z\ < e'" ``` huffman@21164 ` 1235` ``` with e e_lt e_simps all [rule_format, of "f x + z"] ``` huffman@21164 ` 1236` ``` show "\g (f x + z) - g (f x)\ < r" by force ``` huffman@21164 ` 1237` ``` qed ``` huffman@21164 ` 1238` ``` qed ``` huffman@21164 ` 1239` ``` qed ``` huffman@21164 ` 1240` ```qed ``` huffman@21164 ` 1241` huffman@23041 ` 1242` ```text {* Derivative of inverse function *} ``` huffman@23041 ` 1243` huffman@23041 ` 1244` ```lemma DERIV_inverse_function: ``` huffman@23041 ` 1245` ``` fixes f g :: "real \ real" ``` huffman@23041 ` 1246` ``` assumes der: "DERIV f (g x) :> D" ``` huffman@23041 ` 1247` ``` assumes neq: "D \ 0" ``` huffman@23044 ` 1248` ``` assumes a: "a < x" and b: "x < b" ``` huffman@23044 ` 1249` ``` assumes inj: "\y. a < y \ y < b \ f (g y) = y" ``` huffman@23041 ` 1250` ``` assumes cont: "isCont g x" ``` huffman@23041 ` 1251` ``` shows "DERIV g x :> inverse D" ``` huffman@23041 ` 1252` ```unfolding DERIV_iff2 ``` huffman@23044 ` 1253` ```proof (rule LIM_equal2) ``` huffman@23044 ` 1254` ``` show "0 < min (x - a) (b - x)" ``` chaieb@27668 ` 1255` ``` using a b by arith ``` huffman@23044 ` 1256` ```next ``` huffman@23041 ` 1257` ``` fix y ``` huffman@23044 ` 1258` ``` assume "norm (y - x) < min (x - a) (b - x)" ``` chaieb@27668 ` 1259` ``` hence "a < y" and "y < b" ``` huffman@23044 ` 1260` ``` by (simp_all add: abs_less_iff) ``` huffman@23041 ` 1261` ``` thus "(g y - g x) / (y - x) = ``` huffman@23041 ` 1262` ``` inverse ((f (g y) - x) / (g y - g x))" ``` huffman@23041 ` 1263` ``` by (simp add: inj) ``` huffman@23041 ` 1264` ```next ``` huffman@23041 ` 1265` ``` have "(\z. (f z - f (g x)) / (z - g x)) -- g x --> D" ``` huffman@23041 ` 1266` ``` by (rule der [unfolded DERIV_iff2]) ``` huffman@23041 ` 1267` ``` hence 1: "(\z. (f z - x) / (z - g x)) -- g x --> D" ``` huffman@23044 ` 1268` ``` using inj a b by simp ``` huffman@23041 ` 1269` ``` have 2: "\d>0. \y. y \ x \ norm (y - x) < d \ g y \ g x" ``` huffman@23041 ` 1270` ``` proof (safe intro!: exI) ``` huffman@23044 ` 1271` ``` show "0 < min (x - a) (b - x)" ``` huffman@23044 ` 1272` ``` using a b by simp ``` huffman@23041 ` 1273` ``` next ``` huffman@23041 ` 1274` ``` fix y ``` huffman@23044 ` 1275` ``` assume "norm (y - x) < min (x - a) (b - x)" ``` huffman@23044 ` 1276` ``` hence y: "a < y" "y < b" ``` huffman@23044 ` 1277` ``` by (simp_all add: abs_less_iff) ``` huffman@23041 ` 1278` ``` assume "g y = g x" ``` huffman@23041 ` 1279` ``` hence "f (g y) = f (g x)" by simp ``` huffman@23044 ` 1280` ``` hence "y = x" using inj y a b by simp ``` huffman@23041 ` 1281` ``` also assume "y \ x" ``` huffman@23041 ` 1282` ``` finally show False by simp ``` huffman@23041 ` 1283` ``` qed ``` huffman@23041 ` 1284` ``` have "(\y. (f (g y) - x) / (g y - g x)) -- x --> D" ``` huffman@23041 ` 1285` ``` using cont 1 2 by (rule isCont_LIM_compose2) ``` huffman@23041 ` 1286` ``` thus "(\y. inverse ((f (g y) - x) / (g y - g x))) ``` huffman@23041 ` 1287` ``` -- x --> inverse D" ``` huffman@23041 ` 1288` ``` using neq by (rule LIM_inverse) ``` huffman@23041 ` 1289` ```qed ``` huffman@23041 ` 1290` huffman@21164 ` 1291` ```theorem GMVT: ``` huffman@21784 ` 1292` ``` fixes a b :: real ``` huffman@21164 ` 1293` ``` assumes alb: "a < b" ``` huffman@21164 ` 1294` ``` and fc: "\x. a \ x \ x \ b \ isCont f x" ``` huffman@21164 ` 1295` ``` and fd: "\x. a < x \ x < b \ f differentiable x" ``` huffman@21164 ` 1296` ``` and gc: "\x. a \ x \ x \ b \ isCont g x" ``` huffman@21164 ` 1297` ``` and gd: "\x. a < x \ x < b \ g differentiable x" ``` huffman@21164 ` 1298` ``` shows "\g'c f'c c. DERIV g c :> g'c \ DERIV f c :> f'c \ a < c \ c < b \ ((f b - f a) * g'c) = ((g b - g a) * f'c)" ``` huffman@21164 ` 1299` ```proof - ``` huffman@21164 ` 1300` ``` let ?h = "\x. (f b - f a)*(g x) - (g b - g a)*(f x)" ``` huffman@21164 ` 1301` ``` from prems have "a < b" by simp ``` huffman@21164 ` 1302` ``` moreover have "\x. a \ x \ x \ b \ isCont ?h x" ``` huffman@21164 ` 1303` ``` proof - ``` huffman@21164 ` 1304` ``` have "\x. a <= x \ x <= b \ isCont (\x. f b - f a) x" by simp ``` huffman@21164 ` 1305` ``` with gc have "\x. a <= x \ x <= b \ isCont (\x. (f b - f a) * g x) x" ``` huffman@21164 ` 1306` ``` by (auto intro: isCont_mult) ``` huffman@21164 ` 1307` ``` moreover ``` huffman@21164 ` 1308` ``` have "\x. a <= x \ x <= b \ isCont (\x. g b - g a) x" by simp ``` huffman@21164 ` 1309` ``` with fc have "\x. a <= x \ x <= b \ isCont (\x. (g b - g a) * f x) x" ``` huffman@21164 ` 1310` ``` by (auto intro: isCont_mult) ``` huffman@21164 ` 1311` ``` ultimately show ?thesis ``` huffman@21164 ` 1312` ``` by (fastsimp intro: isCont_diff) ``` huffman@21164 ` 1313` ``` qed ``` huffman@21164 ` 1314` ``` moreover ``` huffman@21164 ` 1315` ``` have "\x. a < x \ x < b \ ?h differentiable x" ``` huffman@21164 ` 1316` ``` proof - ``` huffman@21164 ` 1317` ``` have "\x. a < x \ x < b \ (\x. f b - f a) differentiable x" by (simp add: differentiable_const) ``` huffman@21164 ` 1318` ``` with gd have "\x. a < x \ x < b \ (\x. (f b - f a) * g x) differentiable x" by (simp add: differentiable_mult) ``` huffman@21164 ` 1319` ``` moreover ``` huffman@21164 ` 1320` ``` have "\x. a < x \ x < b \ (\x. g b - g a) differentiable x" by (simp add: differentiable_const) ``` huffman@21164 ` 1321` ``` with fd have "\x. a < x \ x < b \ (\x. (g b - g a) * f x) differentiable x" by (simp add: differentiable_mult) ``` huffman@21164 ` 1322` ``` ultimately show ?thesis by (simp add: differentiable_diff) ``` huffman@21164 ` 1323` ``` qed ``` huffman@21164 ` 1324` ``` ultimately have "\l z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" by (rule MVT) ``` huffman@21164 ` 1325` ``` then obtain l where ldef: "\z. a < z \ z < b \ DERIV ?h z :> l \ ?h b - ?h a = (b - a) * l" .. ``` huffman@21164 ` 1326` ``` then obtain c where cdef: "a < c \ c < b \ DERIV ?h c :> l \ ?h b - ?h a = (b - a) * l" .. ``` huffman@21164 ` 1327` huffman@21164 ` 1328` ``` from cdef have cint: "a < c \ c < b" by auto ``` huffman@21164 ` 1329` ``` with gd have "g differentiable c" by simp ``` huffman@21164 ` 1330` ``` hence "\D. DERIV g c :> D" by (rule differentiableD) ``` huffman@21164 ` 1331` ``` then obtain g'c where g'cdef: "DERIV g c :> g'c" .. ``` huffman@21164 ` 1332` huffman@21164 ` 1333` ``` from cdef have "a < c \ c < b" by auto ``` huffman@21164 ` 1334` ``` with fd have "f differentiable c" by simp ``` huffman@21164 ` 1335` ``` hence "\D. DERIV f c :> D" by (rule differentiableD) ``` huffman@21164 ` 1336` ``` then obtain f'c where f'cdef: "DERIV f c :> f'c" .. ``` huffman@21164 ` 1337` huffman@21164 ` 1338` ``` from cdef have "DERIV ?h c :> l" by auto ``` huffman@21164 ` 1339` ``` moreover ``` huffman@21164 ` 1340` ``` { ``` huffman@23441 ` 1341` ``` have "DERIV (\x. (f b - f a) * g x) c :> g'c * (f b - f a)" ``` huffman@21164 ` 1342` ``` apply (insert DERIV_const [where k="f b - f a"]) ``` huffman@21164 ` 1343` ``` apply (drule meta_spec [of _ c]) ``` huffman@23441 ` 1344` ``` apply (drule DERIV_mult [OF _ g'cdef]) ``` huffman@23441 ` 1345` ``` by simp ``` huffman@23441 ` 1346` ``` moreover have "DERIV (\x. (g b - g a) * f x) c :> f'c * (g b - g a)" ``` huffman@21164 ` 1347` ``` apply (insert DERIV_const [where k="g b - g a"]) ``` huffman@21164 ` 1348` ``` apply (drule meta_spec [of _ c]) ``` huffman@23441 ` 1349` ``` apply (drule DERIV_mult [OF _ f'cdef]) ``` huffman@23441 ` 1350` ``` by simp ``` huffman@21164 ` 1351` ``` ultimately have "DERIV ?h c :> g'c * (f b - f a) - f'c * (g b - g a)" ``` huffman@21164 ` 1352` ``` by (simp add: DERIV_diff) ``` huffman@21164 ` 1353` ``` } ``` huffman@21164 ` 1354` ``` ultimately have leq: "l = g'c * (f b - f a) - f'c * (g b - g a)" by (rule DERIV_unique) ``` huffman@21164 ` 1355` huffman@21164 ` 1356` ``` { ``` huffman@21164 ` 1357` ``` from cdef have "?h b - ?h a = (b - a) * l" by auto ``` huffman@21164 ` 1358` ``` also with leq have "\ = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp ``` huffman@21164 ` 1359` ``` finally have "?h b - ?h a = (b - a) * (g'c * (f b - f a) - f'c * (g b - g a))" by simp ``` huffman@21164 ` 1360` ``` } ``` huffman@21164 ` 1361` ``` moreover ``` huffman@21164 ` 1362` ``` { ``` huffman@21164 ` 1363` ``` have "?h b - ?h a = ``` huffman@21164 ` 1364` ``` ((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) - ``` huffman@21164 ` 1365` ``` ((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))" ``` huffman@22998 ` 1366` ``` by (simp add: mult_ac add_ac right_diff_distrib) ``` huffman@21164 ` 1367` ``` hence "?h b - ?h a = 0" by auto ``` huffman@21164 ` 1368` ``` } ``` huffman@21164 ` 1369` ``` ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto ``` huffman@21164 ` 1370` ``` with alb have "g'c * (f b - f a) - f'c * (g b - g a) = 0" by simp ``` huffman@21164 ` 1371` ``` hence "g'c * (f b - f a) = f'c * (g b - g a)" by simp ``` huffman@21164 ` 1372` ``` hence "(f b - f a) * g'c = (g b - g a) * f'c" by (simp add: mult_ac) ``` huffman@21164 ` 1373` huffman@21164 ` 1374` ``` with g'cdef f'cdef cint show ?thesis by auto ``` huffman@21164 ` 1375` ```qed ``` huffman@21164 ` 1376` chaieb@23255 ` 1377` ```lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E" ``` chaieb@23255 ` 1378` ```by auto ``` chaieb@23255 ` 1379` chaieb@26120 ` 1380` ```subsection {* Derivatives of univariate polynomials *} ``` chaieb@26120 ` 1381` chaieb@26120 ` 1382` chaieb@26120 ` 1383` ``` ``` chaieb@26120 ` 1384` ```primrec pderiv_aux :: "nat => real list => real list" where ``` chaieb@26120 ` 1385` ``` pderiv_aux_Nil: "pderiv_aux n [] = []" ``` chaieb@26120 ` 1386` ```| pderiv_aux_Cons: "pderiv_aux n (h#t) = ``` chaieb@26120 ` 1387` ``` (real n * h)#(pderiv_aux (Suc n) t)" ``` chaieb@26120 ` 1388` chaieb@26120 ` 1389` ```definition ``` chaieb@26120 ` 1390` ``` pderiv :: "real list => real list" where ``` chaieb@26120 ` 1391` ``` "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))" ``` chaieb@26120 ` 1392` chaieb@26120 ` 1393` chaieb@26120 ` 1394` ```text{*The derivative*} ``` chaieb@26120 ` 1395` chaieb@26120 ` 1396` ```lemma pderiv_Nil: "pderiv [] = []" ``` chaieb@26120 ` 1397` chaieb@26120 ` 1398` ```apply (simp add: pderiv_def) ``` chaieb@26120 ` 1399` ```done ``` chaieb@26120 ` 1400` ```declare pderiv_Nil [simp] ``` chaieb@26120 ` 1401` chaieb@26120 ` 1402` ```lemma pderiv_singleton: "pderiv [c] = []" ``` chaieb@26120 ` 1403` ```by (simp add: pderiv_def) ``` chaieb@26120 ` 1404` ```declare pderiv_singleton [simp] ``` chaieb@26120 ` 1405` chaieb@26120 ` 1406` ```lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t" ``` chaieb@26120 ` 1407` ```by (simp add: pderiv_def) ``` chaieb@26120 ` 1408` chaieb@26120 ` 1409` ```lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c" ``` chaieb@26120 ` 1410` ```by (simp add: DERIV_cmult mult_commute [of _ c]) ``` chaieb@26120 ` 1411` chaieb@26120 ` 1412` ```lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)" ``` chaieb@26120 ` 1413` ```by (rule lemma_DERIV_subst, rule DERIV_pow, simp) ``` chaieb@26120 ` 1414` ```declare DERIV_pow2 [simp] DERIV_pow [simp] ``` chaieb@26120 ` 1415` chaieb@26120 ` 1416` ```lemma lemma_DERIV_poly1: "\n. DERIV (%x. (x ^ (Suc n) * poly p x)) x :> ``` chaieb@26120 ` 1417` ``` x ^ n * poly (pderiv_aux (Suc n) p) x " ``` chaieb@26120 ` 1418` ```apply (induct "p") ``` chaieb@26120 ` 1419` ```apply (auto intro!: DERIV_add DERIV_cmult2 ``` chaieb@26120 ` 1420` ``` simp add: pderiv_def right_distrib real_mult_assoc [symmetric] ``` chaieb@26120 ` 1421` ``` simp del: realpow_Suc) ``` chaieb@26120 ` 1422` ```apply (subst mult_commute) ``` chaieb@26120 ` 1423` ```apply (simp del: realpow_Suc) ``` chaieb@26120 ` 1424` ```apply (simp add: mult_commute realpow_Suc [symmetric] del: realpow_Suc) ``` chaieb@26120 ` 1425` ```done ``` chaieb@26120 ` 1426` chaieb@26120 ` 1427` ```lemma lemma_DERIV_poly: "DERIV (%x. (x ^ (Suc n) * poly p x)) x :> ``` chaieb@26120 ` 1428` ``` x ^ n * poly (pderiv_aux (Suc n) p) x " ``` chaieb@26120 ` 1429` ```by (simp add: lemma_DERIV_poly1 del: realpow_Suc) ``` chaieb@26120 ` 1430` chaieb@26120 ` 1431` ```lemma DERIV_add_const: "DERIV f x :> D ==> DERIV (%x. a + f x :: real) x :> D" ``` chaieb@26120 ` 1432` ```by (rule lemma_DERIV_subst, rule DERIV_add, auto) ``` chaieb@26120 ` 1433` chaieb@26120 ` 1434` ```lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x" ``` chaieb@26120 ` 1435` ```apply (induct "p") ``` chaieb@26120 ` 1436` ```apply (auto simp add: pderiv_Cons) ``` chaieb@26120 ` 1437` ```apply (rule DERIV_add_const) ``` chaieb@26120 ` 1438` ```apply (rule lemma_DERIV_subst) ``` chaieb@26120 ` 1439` ```apply (rule lemma_DERIV_poly [where n=0, simplified], simp) ``` chaieb@26120 ` 1440` ```done ``` chaieb@26120 ` 1441` chaieb@26120 ` 1442` chaieb@26120 ` 1443` ```text{* Consequences of the derivative theorem above*} ``` chaieb@26120 ` 1444` chaieb@26120 ` 1445` ```lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (x::real)" ``` chaieb@26120 ` 1446` ```apply (simp add: differentiable_def) ``` chaieb@26120 ` 1447` ```apply (blast intro: poly_DERIV) ``` chaieb@26120 ` 1448` ```done ``` chaieb@26120 ` 1449` chaieb@26120 ` 1450` ```lemma poly_isCont[simp]: "isCont (%x. poly p x) (x::real)" ``` chaieb@26120 ` 1451` ```by (rule poly_DERIV [THEN DERIV_isCont]) ``` chaieb@26120 ` 1452` chaieb@26120 ` 1453` ```lemma poly_IVT_pos: "[| a < b; poly p (a::real) < 0; 0 < poly p b |] ``` chaieb@26120 ` 1454` ``` ==> \x. a < x & x < b & (poly p x = 0)" ``` chaieb@26120 ` 1455` ```apply (cut_tac f = "%x. poly p x" and a = a and b = b and y = 0 in IVT_objl) ``` chaieb@26120 ` 1456` ```apply (auto simp add: order_le_less) ``` chaieb@26120 ` 1457` ```done ``` chaieb@26120 ` 1458` chaieb@26120 ` 1459` ```lemma poly_IVT_neg: "[| (a::real) < b; 0 < poly p a; poly p b < 0 |] ``` chaieb@26120 ` 1460` ``` ==> \x. a < x & x < b & (poly p x = 0)" ``` chaieb@26120 ` 1461` ```apply (insert poly_IVT_pos [where p = "-- p" ]) ``` chaieb@26120 ` 1462` ```apply (simp add: poly_minus neg_less_0_iff_less) ``` chaieb@26120 ` 1463` ```done ``` chaieb@26120 ` 1464` chaieb@26120 ` 1465` ```lemma poly_MVT: "a < b ==> ``` chaieb@26120 ` 1466` ``` \x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)" ``` chaieb@26120 ` 1467` ```apply (drule_tac f = "poly p" in MVT, auto) ``` chaieb@26120 ` 1468` ```apply (rule_tac x = z in exI) ``` chaieb@26120 ` 1469` ```apply (auto simp add: real_mult_left_cancel poly_DERIV [THEN DERIV_unique]) ``` chaieb@26120 ` 1470` ```done ``` chaieb@26120 ` 1471` chaieb@26120 ` 1472` ```text{*Lemmas for Derivatives*} ``` chaieb@26120 ` 1473` chaieb@26120 ` 1474` ```lemma lemma_poly_pderiv_aux_add: "\p2 n. poly (pderiv_aux n (p1 +++ p2)) x = ``` chaieb@26120 ` 1475` ``` poly (pderiv_aux n p1 +++ pderiv_aux n p2) x" ``` chaieb@26120 ` 1476` ```apply (induct "p1", simp, clarify) ``` chaieb@26120 ` 1477` ```apply (case_tac "p2") ``` chaieb@26120 ` 1478` ```apply (auto simp add: right_distrib) ``` chaieb@26120 ` 1479` ```done ``` chaieb@26120 ` 1480` chaieb@26120 ` 1481` ```lemma poly_pderiv_aux_add: "poly (pderiv_aux n (p1 +++ p2)) x = ``` chaieb@26120 ` 1482` ``` poly (pderiv_aux n p1 +++ pderiv_aux n p2) x" ``` chaieb@26120 ` 1483` ```apply (simp add: lemma_poly_pderiv_aux_add) ``` chaieb@26120 ` 1484` ```done ``` chaieb@26120 ` 1485` chaieb@26120 ` 1486` ```lemma lemma_poly_pderiv_aux_cmult: "\n. poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x" ``` chaieb@26120 ` 1487` ```apply (induct "p") ``` chaieb@26120 ` 1488` ```apply (auto simp add: poly_cmult mult_ac) ``` chaieb@26120 ` 1489` ```done ``` chaieb@26120 ` 1490` chaieb@26120 ` 1491` ```lemma poly_pderiv_aux_cmult: "poly (pderiv_aux n (c %* p)) x = poly (c %* pderiv_aux n p) x" ``` chaieb@26120 ` 1492` ```by (simp add: lemma_poly_pderiv_aux_cmult) ``` chaieb@26120 ` 1493` chaieb@26120 ` 1494` ```lemma poly_pderiv_aux_minus: ``` chaieb@26120 ` 1495` ``` "poly (pderiv_aux n (-- p)) x = poly (-- pderiv_aux n p) x" ``` chaieb@26120 ` 1496` ```apply (simp add: poly_minus_def poly_pderiv_aux_cmult) ``` chaieb@26120 ` 1497` ```done ``` chaieb@26120 ` 1498` chaieb@26120 ` 1499` ```lemma lemma_poly_pderiv_aux_mult1: "\n. poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x" ``` chaieb@26120 ` 1500` ```apply (induct "p") ``` chaieb@26120 ` 1501` ```apply (auto simp add: real_of_nat_Suc left_distrib) ``` chaieb@26120 ` 1502` ```done ``` chaieb@26120 ` 1503` chaieb@26120 ` 1504` ```lemma lemma_poly_pderiv_aux_mult: "poly (pderiv_aux (Suc n) p) x = poly ((pderiv_aux n p) +++ p) x" ``` chaieb@26120 ` 1505` ```by (simp add: lemma_poly_pderiv_aux_mult1) ``` chaieb@26120 ` 1506` chaieb@26120 ` 1507` ```lemma lemma_poly_pderiv_add: "\q. poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x" ``` chaieb@26120 ` 1508` ```apply (induct "p", simp, clarify) ``` chaieb@26120 ` 1509` ```apply (case_tac "q") ``` chaieb@26120 ` 1510` ```apply (auto simp add: poly_pderiv_aux_add poly_add pderiv_def) ``` chaieb@26120 ` 1511` ```done ``` chaieb@26120 ` 1512` chaieb@26120 ` 1513` ```lemma poly_pderiv_add: "poly (pderiv (p +++ q)) x = poly (pderiv p +++ pderiv q) x" ``` chaieb@26120 ` 1514` ```by (simp add: lemma_poly_pderiv_add) ``` chaieb@26120 ` 1515` chaieb@26120 ` 1516` ```lemma poly_pderiv_cmult: "poly (pderiv (c %* p)) x = poly (c %* (pderiv p)) x" ``` chaieb@26120 ` 1517` ```apply (induct "p") ``` chaieb@26120 ` 1518` ```apply (auto simp add: poly_pderiv_aux_cmult poly_cmult pderiv_def) ``` chaieb@26120 ` 1519` ```done ``` chaieb@26120 ` 1520` chaieb@26120 ` 1521` ```lemma poly_pderiv_minus: "poly (pderiv (--p)) x = poly (--(pderiv p)) x" ``` chaieb@26120 ` 1522` ```by (simp add: poly_minus_def poly_pderiv_cmult) ``` chaieb@26120 ` 1523` chaieb@26120 ` 1524` ```lemma lemma_poly_mult_pderiv: ``` chaieb@26120 ` 1525` ``` "poly (pderiv (h#t)) x = poly ((0 # (pderiv t)) +++ t) x" ``` chaieb@26120 ` 1526` ```apply (simp add: pderiv_def) ``` chaieb@26120 ` 1527` ```apply (induct "t") ``` chaieb@26120 ` 1528` ```apply (auto simp add: poly_add lemma_poly_pderiv_aux_mult) ``` chaieb@26120 ` 1529` ```done ``` chaieb@26120 ` 1530` chaieb@26120 ` 1531` ```lemma poly_pderiv_mult: "\q. poly (pderiv (p *** q)) x = ``` chaieb@26120 ` 1532` ``` poly (p *** (pderiv q) +++ q *** (pderiv p)) x" ``` chaieb@26120 ` 1533` ```apply (induct "p") ``` chaieb@26120 ` 1534` ```apply (auto simp add: poly_add poly_cmult poly_pderiv_cmult poly_pderiv_add poly_mult) ``` chaieb@26120 ` 1535` ```apply (rule lemma_poly_mult_pderiv [THEN ssubst]) ``` chaieb@26120 ` 1536` ```apply (rule lemma_poly_mult_pderiv [THEN ssubst]) ``` chaieb@26120 ` 1537` ```apply (rule poly_add [THEN ssubst]) ``` chaieb@26120 ` 1538` ```apply (rule poly_add [THEN ssubst]) ``` chaieb@26120 ` 1539` ```apply (simp (no_asm_simp) add: poly_mult right_distrib add_ac mult_ac) ``` chaieb@26120 ` 1540` ```done ``` chaieb@26120 ` 1541` chaieb@26120 ` 1542` ```lemma poly_pderiv_exp: "poly (pderiv (p %^ (Suc n))) x = ``` chaieb@26120 ` 1543` ``` poly ((real (Suc n)) %* (p %^ n) *** pderiv p) x" ``` chaieb@26120 ` 1544` ```apply (induct "n") ``` chaieb@26120 ` 1545` ```apply (auto simp add: poly_add poly_pderiv_cmult poly_cmult poly_pderiv_mult ``` chaieb@26120 ` 1546` ``` real_of_nat_zero poly_mult real_of_nat_Suc ``` chaieb@26120 ` 1547` ``` right_distrib left_distrib mult_ac) ``` chaieb@26120 ` 1548` ```done ``` chaieb@26120 ` 1549` chaieb@26120 ` 1550` ```lemma poly_pderiv_exp_prime: "poly (pderiv ([-a, 1] %^ (Suc n))) x = ``` chaieb@26120 ` 1551` ``` poly (real (Suc n) %* ([-a, 1] %^ n)) x" ``` chaieb@26120 ` 1552` ```apply (simp add: poly_pderiv_exp poly_mult del: pexp_Suc) ``` chaieb@26120 ` 1553` ```apply (simp add: poly_cmult pderiv_def) ``` chaieb@26120 ` 1554` ```done ``` chaieb@26120 ` 1555` chaieb@26120 ` 1556` chaieb@26120 ` 1557` ```lemma real_mult_zero_disj_iff[simp]: "(x * y = 0) = (x = (0::real) | y = 0)" ``` chaieb@26120 ` 1558` ```by simp ``` chaieb@26120 ` 1559` chaieb@26120 ` 1560` ```lemma pderiv_aux_iszero [rule_format, simp]: ``` chaieb@26120 ` 1561` ``` "\n. list_all (%c. c = 0) (pderiv_aux (Suc n) p) = list_all (%c. c = 0) p" ``` chaieb@26120 ` 1562` ```by (induct "p", auto) ``` chaieb@26120 ` 1563` chaieb@26120 ` 1564` ```lemma pderiv_aux_iszero_num: "(number_of n :: nat) \ 0 ``` chaieb@26120 ` 1565` ``` ==> (list_all (%c. c = 0) (pderiv_aux (number_of n) p) = ``` chaieb@26120 ` 1566` ``` list_all (%c. c = 0) p)" ``` chaieb@26120 ` 1567` ```unfolding neq0_conv ``` chaieb@26120 ` 1568` ```apply (rule_tac n1 = "number_of n" and m1 = 0 in less_imp_Suc_add [THEN exE], force) ``` chaieb@26120 ` 1569` ```apply (rule_tac n1 = "0 + x" in pderiv_aux_iszero [THEN subst]) ``` chaieb@26120 ` 1570` ```apply (simp (no_asm_simp) del: pderiv_aux_iszero) ``` chaieb@26120 ` 1571` ```done ``` chaieb@26120 ` 1572` chaieb@26120 ` 1573` ```instance real:: idom_char_0 ``` chaieb@26120 ` 1574` ```apply (intro_classes) ``` chaieb@26120 ` 1575` ```done ``` chaieb@26120 ` 1576` chaieb@26120 ` 1577` ```instance real:: recpower_idom_char_0 ``` chaieb@26120 ` 1578` ```apply (intro_classes) ``` chaieb@26120 ` 1579` ```done ``` chaieb@26120 ` 1580` chaieb@26120 ` 1581` ```lemma pderiv_iszero [rule_format]: ``` chaieb@26120 ` 1582` ``` "poly (pderiv p) = poly [] --> (\h. poly p = poly [h])" ``` chaieb@26120 ` 1583` ```apply (simp add: poly_zero) ``` chaieb@26120 ` 1584` ```apply (induct "p", force) ``` chaieb@26120 ` 1585` ```apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons) ``` chaieb@26120 ` 1586` ```apply (auto simp add: poly_zero [symmetric]) ``` chaieb@26120 ` 1587` ```done ``` chaieb@26120 ` 1588` chaieb@26120 ` 1589` ```lemma pderiv_zero_obj: "poly p = poly [] --> (poly (pderiv p) = poly [])" ``` chaieb@26120 ` 1590` ```apply (simp add: poly_zero) ``` chaieb@26120 ` 1591` ```apply (induct "p", force) ``` chaieb@26120 ` 1592` ```apply (simp add: pderiv_Cons pderiv_aux_iszero_num del: poly_Cons) ``` chaieb@26120 ` 1593` ```done ``` chaieb@26120 ` 1594` chaieb@26120 ` 1595` ```lemma pderiv_zero: "poly p = poly [] ==> (poly (pderiv p) = poly [])" ``` chaieb@26120 ` 1596` ```by (blast elim: pderiv_zero_obj [THEN impE]) ``` chaieb@26120 ` 1597` ```declare pderiv_zero [simp] ``` chaieb@26120 ` 1598` chaieb@26120 ` 1599` ```lemma poly_pderiv_welldef: "poly p = poly q ==> (poly (pderiv p) = poly (pderiv q))" ``` chaieb@26120 ` 1600` ```apply (cut_tac p = "p +++ --q" in pderiv_zero_obj) ``` chaieb@26120 ` 1601` ```apply (simp add: fun_eq poly_add poly_minus poly_pderiv_add poly_pderiv_minus del: pderiv_zero) ``` chaieb@26120 ` 1602` ```done ``` chaieb@26120 ` 1603` chaieb@26120 ` 1604` ```lemma lemma_order_pderiv [rule_format]: ``` chaieb@26120 ` 1605` ``` "\p q a. 0 < n & ``` chaieb@26120 ` 1606` ``` poly (pderiv p) \ poly [] & ``` chaieb@26120 ` 1607` ``` poly p = poly ([- a, 1] %^ n *** q) & ~ [- a, 1] divides q ``` chaieb@26120 ` 1608` ``` --> n = Suc (order a (pderiv p))" ``` chaieb@26120 ` 1609` ```apply (induct "n", safe) ``` chaieb@26120 ` 1610` ```apply (rule order_unique_lemma, rule conjI, assumption) ``` chaieb@26120 ` 1611` ```apply (subgoal_tac "\r. r divides (pderiv p) = r divides (pderiv ([-a, 1] %^ Suc n *** q))") ``` chaieb@26120 ` 1612` ```apply (drule_tac [2] poly_pderiv_welldef) ``` chaieb@26120 ` 1613` ``` prefer 2 apply (simp add: divides_def del: pmult_Cons pexp_Suc) ``` chaieb@26120 ` 1614` ```apply (simp del: pmult_Cons pexp_Suc) ``` chaieb@26120 ` 1615` ```apply (rule conjI) ``` chaieb@26120 ` 1616` ```apply (simp add: divides_def fun_eq del: pmult_Cons pexp_Suc) ``` chaieb@26120 ` 1617` ```apply (rule_tac x = "[-a, 1] *** (pderiv q) +++ real (Suc n) %* q" in exI) ``` chaieb@26120 ` 1618` ```apply (simp add: poly_pderiv_mult poly_pderiv_exp_prime poly_add poly_mult poly_cmult right_distrib mult_ac del: pmult_Cons pexp_Suc) ``` chaieb@26120 ` 1619` ```apply (simp add: poly_mult right_distrib left_distrib mult_ac del: pmult_Cons) ``` chaieb@26120 ` 1620` ```apply (erule_tac V = "\r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl) ``` chaieb@26120 ` 1621` ```apply (unfold divides_def) ``` chaieb@26120 ` 1622` ```apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc) ``` chaieb@26120 ` 1623` ```apply (rule contrapos_np, assumption) ``` chaieb@26120 ` 1624` ```apply (rotate_tac 3, erule contrapos_np) ``` chaieb@26120 ` 1625` ```apply (simp del: pmult_Cons pexp_Suc, safe) ``` chaieb@26120 ` 1626` ```apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI) ``` chaieb@26120 ` 1627` ```apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ") ``` chaieb@26120 ` 1628` ```apply (drule poly_mult_left_cancel [THEN iffD1], simp) ``` chaieb@26120 ` 1629` ```apply (simp add: fun_eq poly_mult poly_add poly_cmult poly_minus del: pmult_Cons mult_cancel_left, safe) ``` chaieb@26120 ` 1630` ```apply (rule_tac c1 = "real (Suc n)" in real_mult_left_cancel [THEN iffD1]) ``` chaieb@26120 ` 1631` ```apply (simp (no_asm)) ``` chaieb@26120 ` 1632` ```apply (subgoal_tac "real (Suc n) * (poly ([- a, 1] %^ n) xa * poly q xa) = ``` chaieb@26120 ` 1633` ``` (poly qa xa + - poly (pderiv q) xa) * ``` chaieb@26120 ` 1634` ``` (poly ([- a, 1] %^ n) xa * ``` chaieb@26120 ` 1635` ``` ((- a + xa) * (inverse (real (Suc n)) * real (Suc n))))") ``` chaieb@26120 ` 1636` ```apply (simp only: mult_ac) ``` chaieb@26120 ` 1637` ```apply (rotate_tac 2) ``` chaieb@26120 ` 1638` ```apply (drule_tac x = xa in spec) ``` chaieb@26120 ` 1639` ```apply (simp add: left_distrib mult_ac del: pmult_Cons) ``` chaieb@26120 ` 1640` ```done ``` chaieb@26120 ` 1641` chaieb@26120 ` 1642` ```lemma order_pderiv: "[| poly (pderiv p) \ poly []; order a p \ 0 |] ``` chaieb@26120 ` 1643` ``` ==> (order a p = Suc (order a (pderiv p)))" ``` chaieb@26120 ` 1644` ```apply (case_tac "poly p = poly []") ``` chaieb@26120 ` 1645` ```apply (auto dest: pderiv_zero) ``` chaieb@26120 ` 1646` ```apply (drule_tac a = a and p = p in order_decomp) ``` chaieb@26120 ` 1647` ```using neq0_conv ``` chaieb@26120 ` 1648` ```apply (blast intro: lemma_order_pderiv) ``` chaieb@26120 ` 1649` ```done ``` chaieb@26120 ` 1650` chaieb@26120 ` 1651` ```text{*Now justify the standard squarefree decomposition, i.e. f / gcd(f,f'). *} ``` chaieb@26120 ` 1652` chaieb@26120 ` 1653` ```lemma poly_squarefree_decomp_order: "[| poly (pderiv p) \ poly []; ``` chaieb@26120 ` 1654` ``` poly p = poly (q *** d); ``` chaieb@26120 ` 1655` ``` poly (pderiv p) = poly (e *** d); ``` chaieb@26120 ` 1656` ``` poly d = poly (r *** p +++ s *** pderiv p) ``` chaieb@26120 ` 1657` ``` |] ==> order a q = (if order a p = 0 then 0 else 1)" ``` chaieb@26120 ` 1658` ```apply (subgoal_tac "order a p = order a q + order a d") ``` chaieb@26120 ` 1659` ```apply (rule_tac [2] s = "order a (q *** d)" in trans) ``` chaieb@26120 ` 1660` ```prefer 2 apply (blast intro: order_poly) ``` chaieb@26120 ` 1661` ```apply (rule_tac [2] order_mult) ``` chaieb@26120 ` 1662` ``` prefer 2 apply force ``` chaieb@26120 ` 1663` ```apply (case_tac "order a p = 0", simp) ``` chaieb@26120 ` 1664` ```apply (subgoal_tac "order a (pderiv p) = order a e + order a d") ``` chaieb@26120 ` 1665` ```apply (rule_tac [2] s = "order a (e *** d)" in trans) ``` chaieb@26120 ` 1666` ```prefer 2 apply (blast intro: order_poly) ``` chaieb@26120 ` 1667` ```apply (rule_tac [2] order_mult) ``` chaieb@26120 ` 1668` ``` prefer 2 apply force ``` chaieb@26120 ` 1669` ```apply (case_tac "poly p = poly []") ``` chaieb@26120 ` 1670` ```apply (drule_tac p = p in pderiv_zero, simp) ``` chaieb@26120 ` 1671` ```apply (drule order_pderiv, assumption) ``` chaieb@26120 ` 1672` ```apply (subgoal_tac "order a (pderiv p) \ order a d") ``` chaieb@26120 ` 1673` ```apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides d") ``` chaieb@26120 ` 1674` ``` prefer 2 apply (simp add: poly_entire order_divides) ``` chaieb@26120 ` 1675` ```apply (subgoal_tac [2] " ([-a, 1] %^ (order a (pderiv p))) divides p & ([-a, 1] %^ (order a (pderiv p))) divides (pderiv p) ") ``` chaieb@26120 ` 1676` ``` prefer 3 apply (simp add: order_divides) ``` chaieb@26120 ` 1677` ``` prefer 2 apply (simp add: divides_def del: pexp_Suc pmult_Cons, safe) ``` chaieb@26120 ` 1678` ```apply (rule_tac x = "r *** qa +++ s *** qaa" in exI) ``` chaieb@26120 ` 1679` ```apply (simp add: fun_eq poly_add poly_mult left_distrib right_distrib mult_ac del: pexp_Suc pmult_Cons, auto) ``` chaieb@26120 ` 1680` ```done ``` chaieb@26120 ` 1681` chaieb@26120 ` 1682` chaieb@26120 ` 1683` ```lemma poly_squarefree_decomp_order2: "[| poly (pderiv p) \ poly []; ``` chaieb@26120 ` 1684` ``` poly p = poly (q *** d); ``` chaieb@26120 ` 1685` ``` poly (pderiv p) = poly (e *** d); ``` chaieb@26120 ` 1686` ``` poly d = poly (r *** p +++ s *** pderiv p) ``` chaieb@26120 ` 1687` ``` |] ==> \a. order a q = (if order a p = 0 then 0 else 1)" ``` chaieb@26120 ` 1688` ```apply (blast intro: poly_squarefree_decomp_order) ``` chaieb@26120 ` 1689` ```done ``` chaieb@26120 ` 1690` chaieb@26120 ` 1691` ```lemma order_pderiv2: "[| poly (pderiv p) \ poly []; order a p \ 0 |] ``` chaieb@26120 ` 1692` ``` ==> (order a (pderiv p) = n) = (order a p = Suc n)" ``` chaieb@26120 ` 1693` ```apply (auto dest: order_pderiv) ``` chaieb@26120 ` 1694` ```done ``` chaieb@26120 ` 1695` chaieb@26120 ` 1696` ```lemma rsquarefree_roots: ``` chaieb@26120 ` 1697` ``` "rsquarefree p = (\a. ~(poly p a = 0 & poly (pderiv p) a = 0))" ``` chaieb@26120 ` 1698` ```apply (simp add: rsquarefree_def) ``` chaieb@26120 ` 1699` ```apply (case_tac "poly p = poly []", simp, simp) ``` chaieb@26120 ` 1700` ```apply (case_tac "poly (pderiv p) = poly []") ``` chaieb@26120 ` 1701` ```apply simp ``` chaieb@26120 ` 1702` ```apply (drule pderiv_iszero, clarify) ``` chaieb@26120 ` 1703` ```apply (subgoal_tac "\a. order a p = order a [h]") ``` chaieb@26120 ` 1704` ```apply (simp add: fun_eq) ``` chaieb@26120 ` 1705` ```apply (rule allI) ``` chaieb@26120 ` 1706` ```apply (cut_tac p = "[h]" and a = a in order_root) ``` chaieb@26120 ` 1707` ```apply (simp add: fun_eq) ``` chaieb@26120 ` 1708` ```apply (blast intro: order_poly) ``` chaieb@26120 ` 1709` ```apply (auto simp add: order_root order_pderiv2) ``` chaieb@26120 ` 1710` ```apply (erule_tac x="a" in allE, simp) ``` chaieb@26120 ` 1711` ```done ``` chaieb@26120 ` 1712` chaieb@26120 ` 1713` ```lemma poly_squarefree_decomp: "[| poly (pderiv p) \ poly []; ``` chaieb@26120 ` 1714` ``` poly p = poly (q *** d); ``` chaieb@26120 ` 1715` ``` poly (pderiv p) = poly (e *** d); ``` chaieb@26120 ` 1716` ``` poly d = poly (r *** p +++ s *** pderiv p) ``` chaieb@26120 ` 1717` ``` |] ==> rsquarefree q & (\a. (poly q a = 0) = (poly p a = 0))" ``` chaieb@26120 ` 1718` ```apply (frule poly_squarefree_decomp_order2, assumption+) ``` chaieb@26120 ` 1719` ```apply (case_tac "poly p = poly []") ``` chaieb@26120 ` 1720` ```apply (blast dest: pderiv_zero) ``` chaieb@26120 ` 1721` ```apply (simp (no_asm) add: rsquarefree_def order_root del: pmult_Cons) ``` chaieb@26120 ` 1722` ```apply (simp add: poly_entire del: pmult_Cons) ``` chaieb@26120 ` 1723` ```done ``` chaieb@26120 ` 1724` huffman@21164 ` 1725` ```end ```