src/HOL/RealDef.thy
 author huffman Thu Feb 18 14:21:44 2010 -0800 (2010-02-18) changeset 35216 7641e8d831d2 parent 35050 9f841f20dca6 child 35344 e0b46cd72414 permissions -rw-r--r--
get rid of many duplicate simp rule warnings
 haftmann@28952 ` 1` ```(* Title : HOL/RealDef.thy ``` paulson@5588 ` 2` ``` Author : Jacques D. Fleuriot ``` paulson@5588 ` 3` ``` Copyright : 1998 University of Cambridge ``` paulson@14387 ` 4` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 ``` avigad@16819 ` 5` ``` Additional contributions by Jeremy Avigad ``` paulson@14269 ` 6` ```*) ``` paulson@14269 ` 7` paulson@14387 ` 8` ```header{*Defining the Reals from the Positive Reals*} ``` paulson@14387 ` 9` nipkow@15131 ` 10` ```theory RealDef ``` nipkow@15140 ` 11` ```imports PReal ``` nipkow@15131 ` 12` ```begin ``` paulson@5588 ` 13` wenzelm@19765 ` 14` ```definition ``` wenzelm@21404 ` 15` ``` realrel :: "((preal * preal) * (preal * preal)) set" where ``` haftmann@28562 ` 16` ``` [code del]: "realrel = {p. \x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" ``` paulson@14269 ` 17` paulson@14484 ` 18` ```typedef (Real) real = "UNIV//realrel" ``` paulson@14269 ` 19` ``` by (auto simp add: quotient_def) ``` paulson@5588 ` 20` wenzelm@19765 ` 21` ```definition ``` paulson@14484 ` 22` ``` (** these don't use the overloaded "real" function: users don't see them **) ``` wenzelm@21404 ` 23` ``` real_of_preal :: "preal => real" where ``` haftmann@28562 ` 24` ``` [code del]: "real_of_preal m = Abs_Real (realrel `` {(m + 1, 1)})" ``` paulson@14484 ` 25` haftmann@25762 ` 26` ```instantiation real :: "{zero, one, plus, minus, uminus, times, inverse, ord, abs, sgn}" ``` haftmann@25571 ` 27` ```begin ``` paulson@5588 ` 28` haftmann@25571 ` 29` ```definition ``` haftmann@28562 ` 30` ``` real_zero_def [code del]: "0 = Abs_Real(realrel``{(1, 1)})" ``` haftmann@25571 ` 31` haftmann@25571 ` 32` ```definition ``` haftmann@28562 ` 33` ``` real_one_def [code del]: "1 = Abs_Real(realrel``{(1 + 1, 1)})" ``` paulson@5588 ` 34` haftmann@25571 ` 35` ```definition ``` haftmann@28562 ` 36` ``` real_add_def [code del]: "z + w = ``` paulson@14484 ` 37` ``` contents (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). ``` nipkow@27964 ` 38` ``` { Abs_Real(realrel``{(x+u, y+v)}) })" ``` bauerg@10606 ` 39` haftmann@25571 ` 40` ```definition ``` haftmann@28562 ` 41` ``` real_minus_def [code del]: "- r = contents (\(x,y) \ Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })" ``` haftmann@25571 ` 42` haftmann@25571 ` 43` ```definition ``` haftmann@28562 ` 44` ``` real_diff_def [code del]: "r - (s::real) = r + - s" ``` paulson@14484 ` 45` haftmann@25571 ` 46` ```definition ``` haftmann@28562 ` 47` ``` real_mult_def [code del]: ``` haftmann@25571 ` 48` ``` "z * w = ``` paulson@14484 ` 49` ``` contents (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). ``` nipkow@27964 ` 50` ``` { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ``` paulson@5588 ` 51` haftmann@25571 ` 52` ```definition ``` haftmann@28562 ` 53` ``` real_inverse_def [code del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)" ``` haftmann@25571 ` 54` haftmann@25571 ` 55` ```definition ``` haftmann@28562 ` 56` ``` real_divide_def [code del]: "R / (S::real) = R * inverse S" ``` paulson@14269 ` 57` haftmann@25571 ` 58` ```definition ``` haftmann@28562 ` 59` ``` real_le_def [code del]: "z \ (w::real) \ ``` haftmann@25571 ` 60` ``` (\x y u v. x+v \ u+y & (x,y) \ Rep_Real z & (u,v) \ Rep_Real w)" ``` haftmann@25571 ` 61` haftmann@25571 ` 62` ```definition ``` haftmann@28562 ` 63` ``` real_less_def [code del]: "x < (y\real) \ x \ y \ x \ y" ``` paulson@5588 ` 64` haftmann@25571 ` 65` ```definition ``` haftmann@25571 ` 66` ``` real_abs_def: "abs (r::real) = (if r < 0 then - r else r)" ``` paulson@14334 ` 67` haftmann@25571 ` 68` ```definition ``` haftmann@25571 ` 69` ``` real_sgn_def: "sgn (x::real) = (if x=0 then 0 else if 0 realrel) = (x1 + y2 = x2 + y1)" ``` paulson@14484 ` 93` ```by (simp add: realrel_def) ``` paulson@14269 ` 94` paulson@14269 ` 95` ```lemma equiv_realrel: "equiv UNIV realrel" ``` nipkow@30198 ` 96` ```apply (auto simp add: equiv_def refl_on_def sym_def trans_def realrel_def) ``` paulson@14365 ` 97` ```apply (blast dest: preal_trans_lemma) ``` paulson@14269 ` 98` ```done ``` paulson@14269 ` 99` paulson@14497 ` 100` ```text{*Reduces equality of equivalence classes to the @{term realrel} relation: ``` paulson@14497 ` 101` ``` @{term "(realrel `` {x} = realrel `` {y}) = ((x,y) \ realrel)"} *} ``` paulson@14269 ` 102` ```lemmas equiv_realrel_iff = ``` paulson@14269 ` 103` ``` eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I] ``` paulson@14269 ` 104` paulson@14269 ` 105` ```declare equiv_realrel_iff [simp] ``` paulson@14269 ` 106` paulson@14497 ` 107` paulson@14484 ` 108` ```lemma realrel_in_real [simp]: "realrel``{(x,y)}: Real" ``` paulson@14484 ` 109` ```by (simp add: Real_def realrel_def quotient_def, blast) ``` paulson@14269 ` 110` huffman@22958 ` 111` ```declare Abs_Real_inject [simp] ``` paulson@14484 ` 112` ```declare Abs_Real_inverse [simp] ``` paulson@14269 ` 113` paulson@14269 ` 114` paulson@14484 ` 115` ```text{*Case analysis on the representation of a real number as an equivalence ``` paulson@14484 ` 116` ``` class of pairs of positive reals.*} ``` paulson@14484 ` 117` ```lemma eq_Abs_Real [case_names Abs_Real, cases type: real]: ``` paulson@14484 ` 118` ``` "(!!x y. z = Abs_Real(realrel``{(x,y)}) ==> P) ==> P" ``` paulson@14484 ` 119` ```apply (rule Rep_Real [of z, unfolded Real_def, THEN quotientE]) ``` paulson@14484 ` 120` ```apply (drule arg_cong [where f=Abs_Real]) ``` paulson@14484 ` 121` ```apply (auto simp add: Rep_Real_inverse) ``` paulson@14269 ` 122` ```done ``` paulson@14269 ` 123` paulson@14269 ` 124` huffman@23287 ` 125` ```subsection {* Addition and Subtraction *} ``` paulson@14269 ` 126` paulson@14269 ` 127` ```lemma real_add_congruent2_lemma: ``` paulson@14269 ` 128` ``` "[|a + ba = aa + b; ab + bc = ac + bb|] ``` paulson@14269 ` 129` ``` ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))" ``` huffman@23287 ` 130` ```apply (simp add: add_assoc) ``` huffman@23287 ` 131` ```apply (rule add_left_commute [of ab, THEN ssubst]) ``` huffman@23287 ` 132` ```apply (simp add: add_assoc [symmetric]) ``` huffman@23287 ` 133` ```apply (simp add: add_ac) ``` paulson@14269 ` 134` ```done ``` paulson@14269 ` 135` paulson@14269 ` 136` ```lemma real_add: ``` paulson@14497 ` 137` ``` "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) = ``` paulson@14497 ` 138` ``` Abs_Real (realrel``{(x+u, y+v)})" ``` paulson@14497 ` 139` ```proof - ``` paulson@15169 ` 140` ``` have "(\z w. (\(x,y). (\(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z) ``` paulson@15169 ` 141` ``` respects2 realrel" ``` paulson@14497 ` 142` ``` by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) ``` paulson@14497 ` 143` ``` thus ?thesis ``` paulson@14497 ` 144` ``` by (simp add: real_add_def UN_UN_split_split_eq ``` paulson@14658 ` 145` ``` UN_equiv_class2 [OF equiv_realrel equiv_realrel]) ``` paulson@14497 ` 146` ```qed ``` paulson@14269 ` 147` paulson@14484 ` 148` ```lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})" ``` paulson@14484 ` 149` ```proof - ``` paulson@15169 ` 150` ``` have "(\(x,y). {Abs_Real (realrel``{(y,x)})}) respects realrel" ``` huffman@23288 ` 151` ``` by (simp add: congruent_def add_commute) ``` paulson@14484 ` 152` ``` thus ?thesis ``` paulson@14484 ` 153` ``` by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel]) ``` paulson@14484 ` 154` ```qed ``` paulson@14334 ` 155` huffman@23287 ` 156` ```instance real :: ab_group_add ``` huffman@23287 ` 157` ```proof ``` huffman@23287 ` 158` ``` fix x y z :: real ``` huffman@23287 ` 159` ``` show "(x + y) + z = x + (y + z)" ``` huffman@23287 ` 160` ``` by (cases x, cases y, cases z, simp add: real_add add_assoc) ``` huffman@23287 ` 161` ``` show "x + y = y + x" ``` huffman@23287 ` 162` ``` by (cases x, cases y, simp add: real_add add_commute) ``` huffman@23287 ` 163` ``` show "0 + x = x" ``` huffman@23287 ` 164` ``` by (cases x, simp add: real_add real_zero_def add_ac) ``` huffman@23287 ` 165` ``` show "- x + x = 0" ``` huffman@23287 ` 166` ``` by (cases x, simp add: real_minus real_add real_zero_def add_commute) ``` huffman@23287 ` 167` ``` show "x - y = x + - y" ``` huffman@23287 ` 168` ``` by (simp add: real_diff_def) ``` huffman@23287 ` 169` ```qed ``` paulson@14269 ` 170` paulson@14269 ` 171` huffman@23287 ` 172` ```subsection {* Multiplication *} ``` paulson@14269 ` 173` paulson@14329 ` 174` ```lemma real_mult_congruent2_lemma: ``` paulson@14329 ` 175` ``` "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> ``` paulson@14484 ` 176` ``` x * x1 + y * y1 + (x * y2 + y * x2) = ``` paulson@14484 ` 177` ``` x * x2 + y * y2 + (x * y1 + y * x1)" ``` huffman@23287 ` 178` ```apply (simp add: add_left_commute add_assoc [symmetric]) ``` huffman@23288 ` 179` ```apply (simp add: add_assoc right_distrib [symmetric]) ``` huffman@23288 ` 180` ```apply (simp add: add_commute) ``` paulson@14269 ` 181` ```done ``` paulson@14269 ` 182` paulson@14269 ` 183` ```lemma real_mult_congruent2: ``` paulson@15169 ` 184` ``` "(%p1 p2. ``` paulson@14484 ` 185` ``` (%(x1,y1). (%(x2,y2). ``` paulson@15169 ` 186` ``` { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1) ``` paulson@15169 ` 187` ``` respects2 realrel" ``` paulson@14658 ` 188` ```apply (rule congruent2_commuteI [OF equiv_realrel], clarify) ``` huffman@23288 ` 189` ```apply (simp add: mult_commute add_commute) ``` paulson@14269 ` 190` ```apply (auto simp add: real_mult_congruent2_lemma) ``` paulson@14269 ` 191` ```done ``` paulson@14269 ` 192` paulson@14269 ` 193` ```lemma real_mult: ``` paulson@14484 ` 194` ``` "Abs_Real((realrel``{(x1,y1)})) * Abs_Real((realrel``{(x2,y2)})) = ``` paulson@14484 ` 195` ``` Abs_Real(realrel `` {(x1*x2+y1*y2,x1*y2+y1*x2)})" ``` paulson@14484 ` 196` ```by (simp add: real_mult_def UN_UN_split_split_eq ``` paulson@14658 ` 197` ``` UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2]) ``` paulson@14269 ` 198` paulson@14269 ` 199` ```lemma real_mult_commute: "(z::real) * w = w * z" ``` huffman@23288 ` 200` ```by (cases z, cases w, simp add: real_mult add_ac mult_ac) ``` paulson@14269 ` 201` paulson@14269 ` 202` ```lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)" ``` paulson@14484 ` 203` ```apply (cases z1, cases z2, cases z3) ``` nipkow@29667 ` 204` ```apply (simp add: real_mult algebra_simps) ``` paulson@14269 ` 205` ```done ``` paulson@14269 ` 206` paulson@14269 ` 207` ```lemma real_mult_1: "(1::real) * z = z" ``` paulson@14484 ` 208` ```apply (cases z) ``` nipkow@29667 ` 209` ```apply (simp add: real_mult real_one_def algebra_simps) ``` paulson@14269 ` 210` ```done ``` paulson@14269 ` 211` paulson@14269 ` 212` ```lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" ``` paulson@14484 ` 213` ```apply (cases z1, cases z2, cases w) ``` nipkow@29667 ` 214` ```apply (simp add: real_add real_mult algebra_simps) ``` paulson@14269 ` 215` ```done ``` paulson@14269 ` 216` paulson@14329 ` 217` ```text{*one and zero are distinct*} ``` paulson@14365 ` 218` ```lemma real_zero_not_eq_one: "0 \ (1::real)" ``` paulson@14484 ` 219` ```proof - ``` huffman@23287 ` 220` ``` have "(1::preal) < 1 + 1" ``` huffman@23287 ` 221` ``` by (simp add: preal_self_less_add_left) ``` paulson@14484 ` 222` ``` thus ?thesis ``` huffman@23288 ` 223` ``` by (simp add: real_zero_def real_one_def) ``` paulson@14484 ` 224` ```qed ``` paulson@14269 ` 225` huffman@23287 ` 226` ```instance real :: comm_ring_1 ``` huffman@23287 ` 227` ```proof ``` huffman@23287 ` 228` ``` fix x y z :: real ``` huffman@23287 ` 229` ``` show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) ``` huffman@23287 ` 230` ``` show "x * y = y * x" by (rule real_mult_commute) ``` huffman@23287 ` 231` ``` show "1 * x = x" by (rule real_mult_1) ``` huffman@23287 ` 232` ``` show "(x + y) * z = x * z + y * z" by (rule real_add_mult_distrib) ``` huffman@23287 ` 233` ``` show "0 \ (1::real)" by (rule real_zero_not_eq_one) ``` huffman@23287 ` 234` ```qed ``` huffman@23287 ` 235` huffman@23287 ` 236` ```subsection {* Inverse and Division *} ``` paulson@14365 ` 237` paulson@14484 ` 238` ```lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0" ``` huffman@23288 ` 239` ```by (simp add: real_zero_def add_commute) ``` paulson@14269 ` 240` paulson@14365 ` 241` ```text{*Instead of using an existential quantifier and constructing the inverse ``` paulson@14365 ` 242` ```within the proof, we could define the inverse explicitly.*} ``` paulson@14365 ` 243` paulson@14365 ` 244` ```lemma real_mult_inverse_left_ex: "x \ 0 ==> \y. y*x = (1::real)" ``` paulson@14484 ` 245` ```apply (simp add: real_zero_def real_one_def, cases x) ``` paulson@14269 ` 246` ```apply (cut_tac x = xa and y = y in linorder_less_linear) ``` paulson@14365 ` 247` ```apply (auto dest!: less_add_left_Ex simp add: real_zero_iff) ``` paulson@14334 ` 248` ```apply (rule_tac ``` huffman@23287 ` 249` ``` x = "Abs_Real (realrel``{(1, inverse (D) + 1)})" ``` paulson@14334 ` 250` ``` in exI) ``` paulson@14334 ` 251` ```apply (rule_tac [2] ``` huffman@23287 ` 252` ``` x = "Abs_Real (realrel``{(inverse (D) + 1, 1)})" ``` paulson@14334 ` 253` ``` in exI) ``` nipkow@29667 ` 254` ```apply (auto simp add: real_mult preal_mult_inverse_right algebra_simps) ``` paulson@14269 ` 255` ```done ``` paulson@14269 ` 256` paulson@14365 ` 257` ```lemma real_mult_inverse_left: "x \ 0 ==> inverse(x)*x = (1::real)" ``` paulson@14484 ` 258` ```apply (simp add: real_inverse_def) ``` huffman@23287 ` 259` ```apply (drule real_mult_inverse_left_ex, safe) ``` huffman@23287 ` 260` ```apply (rule theI, assumption, rename_tac z) ``` huffman@23287 ` 261` ```apply (subgoal_tac "(z * x) * y = z * (x * y)") ``` huffman@23287 ` 262` ```apply (simp add: mult_commute) ``` huffman@23287 ` 263` ```apply (rule mult_assoc) ``` paulson@14269 ` 264` ```done ``` paulson@14334 ` 265` paulson@14341 ` 266` paulson@14341 ` 267` ```subsection{*The Real Numbers form a Field*} ``` paulson@14341 ` 268` paulson@14334 ` 269` ```instance real :: field ``` paulson@14334 ` 270` ```proof ``` paulson@14334 ` 271` ``` fix x y z :: real ``` paulson@14365 ` 272` ``` show "x \ 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left) ``` paulson@14430 ` 273` ``` show "x / y = x * inverse y" by (simp add: real_divide_def) ``` paulson@14334 ` 274` ```qed ``` paulson@14334 ` 275` paulson@14334 ` 276` paulson@14341 ` 277` ```text{*Inverse of zero! Useful to simplify certain equations*} ``` paulson@14269 ` 278` paulson@14334 ` 279` ```lemma INVERSE_ZERO: "inverse 0 = (0::real)" ``` paulson@14484 ` 280` ```by (simp add: real_inverse_def) ``` paulson@14334 ` 281` paulson@14334 ` 282` ```instance real :: division_by_zero ``` paulson@14334 ` 283` ```proof ``` paulson@14334 ` 284` ``` show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) ``` paulson@14334 ` 285` ```qed ``` paulson@14334 ` 286` paulson@14269 ` 287` paulson@14365 ` 288` ```subsection{*The @{text "\"} Ordering*} ``` paulson@14269 ` 289` paulson@14365 ` 290` ```lemma real_le_refl: "w \ (w::real)" ``` paulson@14484 ` 291` ```by (cases w, force simp add: real_le_def) ``` paulson@14269 ` 292` paulson@14378 ` 293` ```text{*The arithmetic decision procedure is not set up for type preal. ``` paulson@14378 ` 294` ``` This lemma is currently unused, but it could simplify the proofs of the ``` paulson@14378 ` 295` ``` following two lemmas.*} ``` paulson@14378 ` 296` ```lemma preal_eq_le_imp_le: ``` paulson@14378 ` 297` ``` assumes eq: "a+b = c+d" and le: "c \ a" ``` paulson@14378 ` 298` ``` shows "b \ (d::preal)" ``` paulson@14378 ` 299` ```proof - ``` huffman@23288 ` 300` ``` have "c+d \ a+d" by (simp add: prems) ``` paulson@14378 ` 301` ``` hence "a+b \ a+d" by (simp add: prems) ``` huffman@23288 ` 302` ``` thus "b \ d" by simp ``` paulson@14378 ` 303` ```qed ``` paulson@14378 ` 304` paulson@14378 ` 305` ```lemma real_le_lemma: ``` paulson@14378 ` 306` ``` assumes l: "u1 + v2 \ u2 + v1" ``` paulson@14378 ` 307` ``` and "x1 + v1 = u1 + y1" ``` paulson@14378 ` 308` ``` and "x2 + v2 = u2 + y2" ``` paulson@14378 ` 309` ``` shows "x1 + y2 \ x2 + (y1::preal)" ``` paulson@14365 ` 310` ```proof - ``` paulson@14378 ` 311` ``` have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems) ``` huffman@23288 ` 312` ``` hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: add_ac) ``` huffman@23288 ` 313` ``` also have "... \ (x2+y1) + (u2+v1)" by (simp add: prems) ``` huffman@23288 ` 314` ``` finally show ?thesis by simp ``` huffman@23288 ` 315` ```qed ``` paulson@14378 ` 316` paulson@14378 ` 317` ```lemma real_le: ``` paulson@14484 ` 318` ``` "(Abs_Real(realrel``{(x1,y1)}) \ Abs_Real(realrel``{(x2,y2)})) = ``` paulson@14484 ` 319` ``` (x1 + y2 \ x2 + y1)" ``` huffman@23288 ` 320` ```apply (simp add: real_le_def) ``` paulson@14387 ` 321` ```apply (auto intro: real_le_lemma) ``` paulson@14378 ` 322` ```done ``` paulson@14378 ` 323` nipkow@33657 ` 324` ```lemma real_le_antisym: "[| z \ w; w \ z |] ==> z = (w::real)" ``` nipkow@15542 ` 325` ```by (cases z, cases w, simp add: real_le) ``` paulson@14378 ` 326` paulson@14378 ` 327` ```lemma real_trans_lemma: ``` paulson@14378 ` 328` ``` assumes "x + v \ u + y" ``` paulson@14378 ` 329` ``` and "u + v' \ u' + v" ``` paulson@14378 ` 330` ``` and "x2 + v2 = u2 + y2" ``` paulson@14378 ` 331` ``` shows "x + v' \ u' + (y::preal)" ``` paulson@14378 ` 332` ```proof - ``` huffman@23288 ` 333` ``` have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: add_ac) ``` huffman@23288 ` 334` ``` also have "... \ (u+y) + (u+v')" by (simp add: prems) ``` huffman@23288 ` 335` ``` also have "... \ (u+y) + (u'+v)" by (simp add: prems) ``` huffman@23288 ` 336` ``` also have "... = (u'+y) + (u+v)" by (simp add: add_ac) ``` huffman@23288 ` 337` ``` finally show ?thesis by simp ``` nipkow@15542 ` 338` ```qed ``` paulson@14269 ` 339` paulson@14365 ` 340` ```lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (k::real)" ``` paulson@14484 ` 341` ```apply (cases i, cases j, cases k) ``` paulson@14484 ` 342` ```apply (simp add: real_le) ``` huffman@23288 ` 343` ```apply (blast intro: real_trans_lemma) ``` paulson@14334 ` 344` ```done ``` paulson@14334 ` 345` paulson@14365 ` 346` ```instance real :: order ``` haftmann@27682 ` 347` ```proof ``` haftmann@27682 ` 348` ``` fix u v :: real ``` haftmann@27682 ` 349` ``` show "u < v \ u \ v \ \ v \ u" ``` nipkow@33657 ` 350` ``` by (auto simp add: real_less_def intro: real_le_antisym) ``` nipkow@33657 ` 351` ```qed (assumption | rule real_le_refl real_le_trans real_le_antisym)+ ``` paulson@14365 ` 352` paulson@14378 ` 353` ```(* Axiom 'linorder_linear' of class 'linorder': *) ``` paulson@14378 ` 354` ```lemma real_le_linear: "(z::real) \ w | w \ z" ``` huffman@23288 ` 355` ```apply (cases z, cases w) ``` huffman@23288 ` 356` ```apply (auto simp add: real_le real_zero_def add_ac) ``` paulson@14334 ` 357` ```done ``` paulson@14334 ` 358` paulson@14334 ` 359` ```instance real :: linorder ``` paulson@14334 ` 360` ``` by (intro_classes, rule real_le_linear) ``` paulson@14334 ` 361` paulson@14334 ` 362` paulson@14378 ` 363` ```lemma real_le_eq_diff: "(x \ y) = (x-y \ (0::real))" ``` paulson@14484 ` 364` ```apply (cases x, cases y) ``` paulson@14378 ` 365` ```apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus ``` huffman@23288 ` 366` ``` add_ac) ``` huffman@23288 ` 367` ```apply (simp_all add: add_assoc [symmetric]) ``` nipkow@15542 ` 368` ```done ``` paulson@14378 ` 369` paulson@14484 ` 370` ```lemma real_add_left_mono: ``` paulson@14484 ` 371` ``` assumes le: "x \ y" shows "z + x \ z + (y::real)" ``` paulson@14484 ` 372` ```proof - ``` chaieb@27668 ` 373` ``` have "z + x - (z + y) = (z + -z) + (x - y)" ``` nipkow@29667 ` 374` ``` by (simp add: algebra_simps) ``` paulson@14484 ` 375` ``` with le show ?thesis ``` obua@14754 ` 376` ``` by (simp add: real_le_eq_diff[of x] real_le_eq_diff[of "z+x"] diff_minus) ``` paulson@14484 ` 377` ```qed ``` paulson@14334 ` 378` paulson@14365 ` 379` ```lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)" ``` paulson@14365 ` 380` ```by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus) ``` paulson@14365 ` 381` paulson@14365 ` 382` ```lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))" ``` paulson@14365 ` 383` ```by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus) ``` paulson@14334 ` 384` paulson@14334 ` 385` ```lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y" ``` paulson@14484 ` 386` ```apply (cases x, cases y) ``` paulson@14378 ` 387` ```apply (simp add: linorder_not_le [where 'a = real, symmetric] ``` paulson@14378 ` 388` ``` linorder_not_le [where 'a = preal] ``` paulson@14378 ` 389` ``` real_zero_def real_le real_mult) ``` paulson@14365 ` 390` ``` --{*Reduce to the (simpler) @{text "\"} relation *} ``` wenzelm@16973 ` 391` ```apply (auto dest!: less_add_left_Ex ``` nipkow@29667 ` 392` ``` simp add: algebra_simps preal_self_less_add_left) ``` paulson@14334 ` 393` ```done ``` paulson@14334 ` 394` paulson@14334 ` 395` ```lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" ``` paulson@14334 ` 396` ```apply (rule real_sum_gt_zero_less) ``` paulson@14334 ` 397` ```apply (drule real_less_sum_gt_zero [of x y]) ``` paulson@14334 ` 398` ```apply (drule real_mult_order, assumption) ``` paulson@14334 ` 399` ```apply (simp add: right_distrib) ``` paulson@14334 ` 400` ```done ``` paulson@14334 ` 401` haftmann@25571 ` 402` ```instantiation real :: distrib_lattice ``` haftmann@25571 ` 403` ```begin ``` haftmann@25571 ` 404` haftmann@25571 ` 405` ```definition ``` haftmann@25571 ` 406` ``` "(inf \ real \ real \ real) = min" ``` haftmann@25571 ` 407` haftmann@25571 ` 408` ```definition ``` haftmann@25571 ` 409` ``` "(sup \ real \ real \ real) = max" ``` haftmann@25571 ` 410` haftmann@25571 ` 411` ```instance ``` haftmann@22456 ` 412` ``` by default (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1) ``` haftmann@22456 ` 413` haftmann@25571 ` 414` ```end ``` haftmann@25571 ` 415` paulson@14378 ` 416` paulson@14334 ` 417` ```subsection{*The Reals Form an Ordered Field*} ``` paulson@14334 ` 418` haftmann@35028 ` 419` ```instance real :: linordered_field ``` paulson@14334 ` 420` ```proof ``` paulson@14334 ` 421` ``` fix x y z :: real ``` paulson@14334 ` 422` ``` show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) ``` huffman@22962 ` 423` ``` show "x < y ==> 0 < z ==> z * x < z * y" by (rule real_mult_less_mono2) ``` huffman@22962 ` 424` ``` show "\x\ = (if x < 0 then -x else x)" by (simp only: real_abs_def) ``` nipkow@24506 ` 425` ``` show "sgn x = (if x=0 then 0 else if 0m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)" ``` paulson@14484 ` 445` ```apply (simp add: real_of_preal_def real_zero_def, cases x) ``` huffman@23288 ` 446` ```apply (auto simp add: real_minus add_ac) ``` paulson@14365 ` 447` ```apply (cut_tac x = x and y = y in linorder_less_linear) ``` huffman@23288 ` 448` ```apply (auto dest!: less_add_left_Ex simp add: add_assoc [symmetric]) ``` paulson@14365 ` 449` ```done ``` paulson@14365 ` 450` paulson@14365 ` 451` ```lemma real_of_preal_leD: ``` paulson@14365 ` 452` ``` "real_of_preal m1 \ real_of_preal m2 ==> m1 \ m2" ``` huffman@23288 ` 453` ```by (simp add: real_of_preal_def real_le) ``` paulson@14365 ` 454` paulson@14365 ` 455` ```lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2" ``` paulson@14365 ` 456` ```by (auto simp add: real_of_preal_leD linorder_not_le [symmetric]) ``` paulson@14365 ` 457` paulson@14365 ` 458` ```lemma real_of_preal_lessD: ``` paulson@14365 ` 459` ``` "real_of_preal m1 < real_of_preal m2 ==> m1 < m2" ``` huffman@23288 ` 460` ```by (simp add: real_of_preal_def real_le linorder_not_le [symmetric]) ``` paulson@14365 ` 461` paulson@14365 ` 462` ```lemma real_of_preal_less_iff [simp]: ``` paulson@14365 ` 463` ``` "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" ``` paulson@14365 ` 464` ```by (blast intro: real_of_preal_lessI real_of_preal_lessD) ``` paulson@14365 ` 465` paulson@14365 ` 466` ```lemma real_of_preal_le_iff: ``` paulson@14365 ` 467` ``` "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" ``` huffman@23288 ` 468` ```by (simp add: linorder_not_less [symmetric]) ``` paulson@14365 ` 469` paulson@14365 ` 470` ```lemma real_of_preal_zero_less: "0 < real_of_preal m" ``` huffman@23288 ` 471` ```apply (insert preal_self_less_add_left [of 1 m]) ``` huffman@23288 ` 472` ```apply (auto simp add: real_zero_def real_of_preal_def ``` huffman@23288 ` 473` ``` real_less_def real_le_def add_ac) ``` huffman@23288 ` 474` ```apply (rule_tac x="m + 1" in exI, rule_tac x="1" in exI) ``` huffman@23288 ` 475` ```apply (simp add: add_ac) ``` paulson@14365 ` 476` ```done ``` paulson@14365 ` 477` paulson@14365 ` 478` ```lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0" ``` paulson@14365 ` 479` ```by (simp add: real_of_preal_zero_less) ``` paulson@14365 ` 480` paulson@14365 ` 481` ```lemma real_of_preal_not_minus_gt_zero: "~ 0 < - real_of_preal m" ``` paulson@14484 ` 482` ```proof - ``` paulson@14484 ` 483` ``` from real_of_preal_minus_less_zero ``` paulson@14484 ` 484` ``` show ?thesis by (blast dest: order_less_trans) ``` paulson@14484 ` 485` ```qed ``` paulson@14365 ` 486` paulson@14365 ` 487` paulson@14365 ` 488` ```subsection{*Theorems About the Ordering*} ``` paulson@14365 ` 489` paulson@14365 ` 490` ```lemma real_gt_zero_preal_Ex: "(0 < x) = (\y. x = real_of_preal y)" ``` paulson@14365 ` 491` ```apply (auto simp add: real_of_preal_zero_less) ``` paulson@14365 ` 492` ```apply (cut_tac x = x in real_of_preal_trichotomy) ``` paulson@14365 ` 493` ```apply (blast elim!: real_of_preal_not_minus_gt_zero [THEN notE]) ``` paulson@14365 ` 494` ```done ``` paulson@14365 ` 495` paulson@14365 ` 496` ```lemma real_gt_preal_preal_Ex: ``` paulson@14365 ` 497` ``` "real_of_preal z < x ==> \y. x = real_of_preal y" ``` paulson@14365 ` 498` ```by (blast dest!: real_of_preal_zero_less [THEN order_less_trans] ``` paulson@14365 ` 499` ``` intro: real_gt_zero_preal_Ex [THEN iffD1]) ``` paulson@14365 ` 500` paulson@14365 ` 501` ```lemma real_ge_preal_preal_Ex: ``` paulson@14365 ` 502` ``` "real_of_preal z \ x ==> \y. x = real_of_preal y" ``` paulson@14365 ` 503` ```by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) ``` paulson@14365 ` 504` paulson@14365 ` 505` ```lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" ``` paulson@14365 ` 506` ```by (auto elim: order_le_imp_less_or_eq [THEN disjE] ``` paulson@14365 ` 507` ``` intro: real_of_preal_zero_less [THEN [2] order_less_trans] ``` paulson@14365 ` 508` ``` simp add: real_of_preal_zero_less) ``` paulson@14365 ` 509` paulson@14365 ` 510` ```lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" ``` paulson@14365 ` 511` ```by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) ``` paulson@14365 ` 512` paulson@14334 ` 513` paulson@14334 ` 514` ```subsection{*More Lemmas*} ``` paulson@14334 ` 515` paulson@14334 ` 516` ```lemma real_mult_left_cancel: "(c::real) \ 0 ==> (c*a=c*b) = (a=b)" ``` paulson@14334 ` 517` ```by auto ``` paulson@14334 ` 518` paulson@14334 ` 519` ```lemma real_mult_right_cancel: "(c::real) \ 0 ==> (a*c=b*c) = (a=b)" ``` paulson@14334 ` 520` ```by auto ``` paulson@14334 ` 521` paulson@14334 ` 522` ```lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" ``` paulson@14334 ` 523` ``` by (force elim: order_less_asym ``` haftmann@35050 ` 524` ``` simp add: mult_less_cancel_right) ``` paulson@14334 ` 525` paulson@14334 ` 526` ```lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \ y*z) = (x\y)" ``` paulson@14365 ` 527` ```apply (simp add: mult_le_cancel_right) ``` huffman@23289 ` 528` ```apply (blast intro: elim: order_less_asym) ``` paulson@14365 ` 529` ```done ``` paulson@14334 ` 530` paulson@14334 ` 531` ```lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x\y)" ``` nipkow@15923 ` 532` ```by(simp add:mult_commute) ``` paulson@14334 ` 533` paulson@14365 ` 534` ```lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" ``` huffman@23289 ` 535` ```by (simp add: one_less_inverse_iff) (* TODO: generalize/move *) ``` paulson@14334 ` 536` paulson@14334 ` 537` haftmann@24198 ` 538` ```subsection {* Embedding numbers into the Reals *} ``` haftmann@24198 ` 539` haftmann@24198 ` 540` ```abbreviation ``` haftmann@24198 ` 541` ``` real_of_nat :: "nat \ real" ``` haftmann@24198 ` 542` ```where ``` haftmann@24198 ` 543` ``` "real_of_nat \ of_nat" ``` haftmann@24198 ` 544` haftmann@24198 ` 545` ```abbreviation ``` haftmann@24198 ` 546` ``` real_of_int :: "int \ real" ``` haftmann@24198 ` 547` ```where ``` haftmann@24198 ` 548` ``` "real_of_int \ of_int" ``` haftmann@24198 ` 549` haftmann@24198 ` 550` ```abbreviation ``` haftmann@24198 ` 551` ``` real_of_rat :: "rat \ real" ``` haftmann@24198 ` 552` ```where ``` haftmann@24198 ` 553` ``` "real_of_rat \ of_rat" ``` haftmann@24198 ` 554` haftmann@24198 ` 555` ```consts ``` haftmann@24198 ` 556` ``` (*overloaded constant for injecting other types into "real"*) ``` haftmann@24198 ` 557` ``` real :: "'a => real" ``` paulson@14365 ` 558` paulson@14378 ` 559` ```defs (overloaded) ``` haftmann@31998 ` 560` ``` real_of_nat_def [code_unfold]: "real == real_of_nat" ``` haftmann@31998 ` 561` ``` real_of_int_def [code_unfold]: "real == real_of_int" ``` paulson@14365 ` 562` avigad@16819 ` 563` ```lemma real_eq_of_nat: "real = of_nat" ``` haftmann@24198 ` 564` ``` unfolding real_of_nat_def .. ``` avigad@16819 ` 565` avigad@16819 ` 566` ```lemma real_eq_of_int: "real = of_int" ``` haftmann@24198 ` 567` ``` unfolding real_of_int_def .. ``` avigad@16819 ` 568` paulson@14365 ` 569` ```lemma real_of_int_zero [simp]: "real (0::int) = 0" ``` paulson@14378 ` 570` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 571` paulson@14365 ` 572` ```lemma real_of_one [simp]: "real (1::int) = (1::real)" ``` paulson@14378 ` 573` ```by (simp add: real_of_int_def) ``` paulson@14334 ` 574` avigad@16819 ` 575` ```lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y" ``` paulson@14378 ` 576` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 577` avigad@16819 ` 578` ```lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)" ``` paulson@14378 ` 579` ```by (simp add: real_of_int_def) ``` avigad@16819 ` 580` avigad@16819 ` 581` ```lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y" ``` avigad@16819 ` 582` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 583` avigad@16819 ` 584` ```lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y" ``` paulson@14378 ` 585` ```by (simp add: real_of_int_def) ``` paulson@14334 ` 586` avigad@16819 ` 587` ```lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))" ``` avigad@16819 ` 588` ``` apply (subst real_eq_of_int)+ ``` avigad@16819 ` 589` ``` apply (rule of_int_setsum) ``` avigad@16819 ` 590` ```done ``` avigad@16819 ` 591` avigad@16819 ` 592` ```lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) = ``` avigad@16819 ` 593` ``` (PROD x:A. real(f x))" ``` avigad@16819 ` 594` ``` apply (subst real_eq_of_int)+ ``` avigad@16819 ` 595` ``` apply (rule of_int_setprod) ``` avigad@16819 ` 596` ```done ``` paulson@14365 ` 597` chaieb@27668 ` 598` ```lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))" ``` paulson@14378 ` 599` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 600` chaieb@27668 ` 601` ```lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)" ``` paulson@14378 ` 602` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 603` chaieb@27668 ` 604` ```lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)" ``` paulson@14378 ` 605` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 606` chaieb@27668 ` 607` ```lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \ real y) = (x \ y)" ``` paulson@14378 ` 608` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 609` chaieb@27668 ` 610` ```lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)" ``` avigad@16819 ` 611` ```by (simp add: real_of_int_def) ``` avigad@16819 ` 612` chaieb@27668 ` 613` ```lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)" ``` avigad@16819 ` 614` ```by (simp add: real_of_int_def) ``` avigad@16819 ` 615` chaieb@27668 ` 616` ```lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)" ``` avigad@16819 ` 617` ```by (simp add: real_of_int_def) ``` avigad@16819 ` 618` chaieb@27668 ` 619` ```lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)" ``` avigad@16819 ` 620` ```by (simp add: real_of_int_def) ``` avigad@16819 ` 621` avigad@16888 ` 622` ```lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))" ``` avigad@16888 ` 623` ```by (auto simp add: abs_if) ``` avigad@16888 ` 624` avigad@16819 ` 625` ```lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)" ``` avigad@16819 ` 626` ``` apply (subgoal_tac "real n + 1 = real (n + 1)") ``` avigad@16819 ` 627` ``` apply (simp del: real_of_int_add) ``` avigad@16819 ` 628` ``` apply auto ``` avigad@16819 ` 629` ```done ``` avigad@16819 ` 630` avigad@16819 ` 631` ```lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)" ``` avigad@16819 ` 632` ``` apply (subgoal_tac "real m + 1 = real (m + 1)") ``` avigad@16819 ` 633` ``` apply (simp del: real_of_int_add) ``` avigad@16819 ` 634` ``` apply simp ``` avigad@16819 ` 635` ```done ``` avigad@16819 ` 636` avigad@16819 ` 637` ```lemma real_of_int_div_aux: "d ~= 0 ==> (real (x::int)) / (real d) = ``` avigad@16819 ` 638` ``` real (x div d) + (real (x mod d)) / (real d)" ``` avigad@16819 ` 639` ```proof - ``` avigad@16819 ` 640` ``` assume "d ~= 0" ``` avigad@16819 ` 641` ``` have "x = (x div d) * d + x mod d" ``` avigad@16819 ` 642` ``` by auto ``` avigad@16819 ` 643` ``` then have "real x = real (x div d) * real d + real(x mod d)" ``` avigad@16819 ` 644` ``` by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym]) ``` avigad@16819 ` 645` ``` then have "real x / real d = ... / real d" ``` avigad@16819 ` 646` ``` by simp ``` avigad@16819 ` 647` ``` then show ?thesis ``` nipkow@29667 ` 648` ``` by (auto simp add: add_divide_distrib algebra_simps prems) ``` avigad@16819 ` 649` ```qed ``` avigad@16819 ` 650` avigad@16819 ` 651` ```lemma real_of_int_div: "(d::int) ~= 0 ==> d dvd n ==> ``` avigad@16819 ` 652` ``` real(n div d) = real n / real d" ``` avigad@16819 ` 653` ``` apply (frule real_of_int_div_aux [of d n]) ``` avigad@16819 ` 654` ``` apply simp ``` nipkow@30042 ` 655` ``` apply (simp add: dvd_eq_mod_eq_0) ``` avigad@16819 ` 656` ```done ``` avigad@16819 ` 657` avigad@16819 ` 658` ```lemma real_of_int_div2: ``` avigad@16819 ` 659` ``` "0 <= real (n::int) / real (x) - real (n div x)" ``` avigad@16819 ` 660` ``` apply (case_tac "x = 0") ``` avigad@16819 ` 661` ``` apply simp ``` avigad@16819 ` 662` ``` apply (case_tac "0 < x") ``` nipkow@29667 ` 663` ``` apply (simp add: algebra_simps) ``` avigad@16819 ` 664` ``` apply (subst real_of_int_div_aux) ``` avigad@16819 ` 665` ``` apply simp ``` avigad@16819 ` 666` ``` apply simp ``` avigad@16819 ` 667` ``` apply (subst zero_le_divide_iff) ``` avigad@16819 ` 668` ``` apply auto ``` nipkow@29667 ` 669` ``` apply (simp add: algebra_simps) ``` avigad@16819 ` 670` ``` apply (subst real_of_int_div_aux) ``` avigad@16819 ` 671` ``` apply simp ``` avigad@16819 ` 672` ``` apply simp ``` avigad@16819 ` 673` ``` apply (subst zero_le_divide_iff) ``` avigad@16819 ` 674` ``` apply auto ``` avigad@16819 ` 675` ```done ``` avigad@16819 ` 676` avigad@16819 ` 677` ```lemma real_of_int_div3: ``` avigad@16819 ` 678` ``` "real (n::int) / real (x) - real (n div x) <= 1" ``` avigad@16819 ` 679` ``` apply(case_tac "x = 0") ``` avigad@16819 ` 680` ``` apply simp ``` nipkow@29667 ` 681` ``` apply (simp add: algebra_simps) ``` avigad@16819 ` 682` ``` apply (subst real_of_int_div_aux) ``` avigad@16819 ` 683` ``` apply assumption ``` avigad@16819 ` 684` ``` apply simp ``` avigad@16819 ` 685` ``` apply (subst divide_le_eq) ``` avigad@16819 ` 686` ``` apply clarsimp ``` avigad@16819 ` 687` ``` apply (rule conjI) ``` avigad@16819 ` 688` ``` apply (rule impI) ``` avigad@16819 ` 689` ``` apply (rule order_less_imp_le) ``` avigad@16819 ` 690` ``` apply simp ``` avigad@16819 ` 691` ``` apply (rule impI) ``` avigad@16819 ` 692` ``` apply (rule order_less_imp_le) ``` avigad@16819 ` 693` ``` apply simp ``` avigad@16819 ` 694` ```done ``` avigad@16819 ` 695` avigad@16819 ` 696` ```lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" ``` nipkow@27964 ` 697` ```by (insert real_of_int_div2 [of n x], simp) ``` nipkow@27964 ` 698` nipkow@27964 ` 699` paulson@14365 ` 700` ```subsection{*Embedding the Naturals into the Reals*} ``` paulson@14365 ` 701` paulson@14334 ` 702` ```lemma real_of_nat_zero [simp]: "real (0::nat) = 0" ``` paulson@14365 ` 703` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 704` huffman@30082 ` 705` ```lemma real_of_nat_1 [simp]: "real (1::nat) = 1" ``` huffman@30082 ` 706` ```by (simp add: real_of_nat_def) ``` huffman@30082 ` 707` paulson@14334 ` 708` ```lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" ``` paulson@14365 ` 709` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 710` paulson@14365 ` 711` ```lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n" ``` paulson@14378 ` 712` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 713` paulson@14334 ` 714` ```(*Not for addsimps: often the LHS is used to represent a positive natural*) ``` paulson@14334 ` 715` ```lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" ``` paulson@14378 ` 716` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 717` paulson@14334 ` 718` ```lemma real_of_nat_less_iff [iff]: ``` paulson@14334 ` 719` ``` "(real (n::nat) < real m) = (n < m)" ``` paulson@14365 ` 720` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 721` paulson@14334 ` 722` ```lemma real_of_nat_le_iff [iff]: "(real (n::nat) \ real m) = (n \ m)" ``` paulson@14378 ` 723` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 724` paulson@14334 ` 725` ```lemma real_of_nat_ge_zero [iff]: "0 \ real (n::nat)" ``` paulson@14378 ` 726` ```by (simp add: real_of_nat_def zero_le_imp_of_nat) ``` paulson@14334 ` 727` paulson@14365 ` 728` ```lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" ``` paulson@14378 ` 729` ```by (simp add: real_of_nat_def del: of_nat_Suc) ``` paulson@14365 ` 730` paulson@14334 ` 731` ```lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" ``` huffman@23431 ` 732` ```by (simp add: real_of_nat_def of_nat_mult) ``` paulson@14334 ` 733` avigad@16819 ` 734` ```lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = ``` avigad@16819 ` 735` ``` (SUM x:A. real(f x))" ``` avigad@16819 ` 736` ``` apply (subst real_eq_of_nat)+ ``` avigad@16819 ` 737` ``` apply (rule of_nat_setsum) ``` avigad@16819 ` 738` ```done ``` avigad@16819 ` 739` avigad@16819 ` 740` ```lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) = ``` avigad@16819 ` 741` ``` (PROD x:A. real(f x))" ``` avigad@16819 ` 742` ``` apply (subst real_eq_of_nat)+ ``` avigad@16819 ` 743` ``` apply (rule of_nat_setprod) ``` avigad@16819 ` 744` ```done ``` avigad@16819 ` 745` avigad@16819 ` 746` ```lemma real_of_card: "real (card A) = setsum (%x.1) A" ``` avigad@16819 ` 747` ``` apply (subst card_eq_setsum) ``` avigad@16819 ` 748` ``` apply (subst real_of_nat_setsum) ``` avigad@16819 ` 749` ``` apply simp ``` avigad@16819 ` 750` ```done ``` avigad@16819 ` 751` paulson@14334 ` 752` ```lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" ``` paulson@14378 ` 753` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 754` paulson@14387 ` 755` ```lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" ``` paulson@14378 ` 756` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 757` paulson@14365 ` 758` ```lemma real_of_nat_diff: "n \ m ==> real (m - n) = real (m::nat) - real n" ``` huffman@23438 ` 759` ```by (simp add: add: real_of_nat_def of_nat_diff) ``` paulson@14334 ` 760` nipkow@25162 ` 761` ```lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)" ``` nipkow@25140 ` 762` ```by (auto simp: real_of_nat_def) ``` paulson@14365 ` 763` paulson@14365 ` 764` ```lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \ 0) = (n = 0)" ``` paulson@14378 ` 765` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 766` paulson@14365 ` 767` ```lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" ``` paulson@14378 ` 768` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 769` huffman@35216 ` 770` ```(* FIXME: duplicates real_of_nat_ge_zero *) ``` huffman@35216 ` 771` ```lemma real_of_nat_ge_zero_cancel_iff: "(0 \ real (n::nat))" ``` paulson@14378 ` 772` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 773` avigad@16819 ` 774` ```lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)" ``` avigad@16819 ` 775` ``` apply (subgoal_tac "real n + 1 = real (Suc n)") ``` avigad@16819 ` 776` ``` apply simp ``` avigad@16819 ` 777` ``` apply (auto simp add: real_of_nat_Suc) ``` avigad@16819 ` 778` ```done ``` avigad@16819 ` 779` avigad@16819 ` 780` ```lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)" ``` avigad@16819 ` 781` ``` apply (subgoal_tac "real m + 1 = real (Suc m)") ``` avigad@16819 ` 782` ``` apply (simp add: less_Suc_eq_le) ``` avigad@16819 ` 783` ``` apply (simp add: real_of_nat_Suc) ``` avigad@16819 ` 784` ```done ``` avigad@16819 ` 785` avigad@16819 ` 786` ```lemma real_of_nat_div_aux: "0 < d ==> (real (x::nat)) / (real d) = ``` avigad@16819 ` 787` ``` real (x div d) + (real (x mod d)) / (real d)" ``` avigad@16819 ` 788` ```proof - ``` avigad@16819 ` 789` ``` assume "0 < d" ``` avigad@16819 ` 790` ``` have "x = (x div d) * d + x mod d" ``` avigad@16819 ` 791` ``` by auto ``` avigad@16819 ` 792` ``` then have "real x = real (x div d) * real d + real(x mod d)" ``` avigad@16819 ` 793` ``` by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym]) ``` avigad@16819 ` 794` ``` then have "real x / real d = \ / real d" ``` avigad@16819 ` 795` ``` by simp ``` avigad@16819 ` 796` ``` then show ?thesis ``` nipkow@29667 ` 797` ``` by (auto simp add: add_divide_distrib algebra_simps prems) ``` avigad@16819 ` 798` ```qed ``` avigad@16819 ` 799` avigad@16819 ` 800` ```lemma real_of_nat_div: "0 < (d::nat) ==> d dvd n ==> ``` avigad@16819 ` 801` ``` real(n div d) = real n / real d" ``` avigad@16819 ` 802` ``` apply (frule real_of_nat_div_aux [of d n]) ``` avigad@16819 ` 803` ``` apply simp ``` avigad@16819 ` 804` ``` apply (subst dvd_eq_mod_eq_0 [THEN sym]) ``` avigad@16819 ` 805` ``` apply assumption ``` avigad@16819 ` 806` ```done ``` avigad@16819 ` 807` avigad@16819 ` 808` ```lemma real_of_nat_div2: ``` avigad@16819 ` 809` ``` "0 <= real (n::nat) / real (x) - real (n div x)" ``` nipkow@25134 ` 810` ```apply(case_tac "x = 0") ``` nipkow@25134 ` 811` ``` apply (simp) ``` nipkow@29667 ` 812` ```apply (simp add: algebra_simps) ``` nipkow@25134 ` 813` ```apply (subst real_of_nat_div_aux) ``` nipkow@25134 ` 814` ``` apply simp ``` nipkow@25134 ` 815` ```apply simp ``` nipkow@25134 ` 816` ```apply (subst zero_le_divide_iff) ``` nipkow@25134 ` 817` ```apply simp ``` avigad@16819 ` 818` ```done ``` avigad@16819 ` 819` avigad@16819 ` 820` ```lemma real_of_nat_div3: ``` avigad@16819 ` 821` ``` "real (n::nat) / real (x) - real (n div x) <= 1" ``` nipkow@25134 ` 822` ```apply(case_tac "x = 0") ``` nipkow@25134 ` 823` ```apply (simp) ``` nipkow@29667 ` 824` ```apply (simp add: algebra_simps) ``` nipkow@25134 ` 825` ```apply (subst real_of_nat_div_aux) ``` nipkow@25134 ` 826` ``` apply simp ``` nipkow@25134 ` 827` ```apply simp ``` avigad@16819 ` 828` ```done ``` avigad@16819 ` 829` avigad@16819 ` 830` ```lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" ``` nipkow@29667 ` 831` ```by (insert real_of_nat_div2 [of n x], simp) ``` avigad@16819 ` 832` paulson@14365 ` 833` ```lemma real_of_int_real_of_nat: "real (int n) = real n" ``` paulson@14378 ` 834` ```by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat) ``` paulson@14378 ` 835` paulson@14426 ` 836` ```lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" ``` paulson@14426 ` 837` ```by (simp add: real_of_int_def real_of_nat_def) ``` paulson@14334 ` 838` avigad@16819 ` 839` ```lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x" ``` avigad@16819 ` 840` ``` apply (subgoal_tac "real(int(nat x)) = real(nat x)") ``` avigad@16819 ` 841` ``` apply force ``` avigad@16819 ` 842` ``` apply (simp only: real_of_int_real_of_nat) ``` avigad@16819 ` 843` ```done ``` paulson@14387 ` 844` nipkow@28001 ` 845` nipkow@28001 ` 846` ```subsection{* Rationals *} ``` nipkow@28001 ` 847` nipkow@28091 ` 848` ```lemma Rats_real_nat[simp]: "real(n::nat) \ \" ``` nipkow@28091 ` 849` ```by (simp add: real_eq_of_nat) ``` nipkow@28091 ` 850` nipkow@28091 ` 851` nipkow@28001 ` 852` ```lemma Rats_eq_int_div_int: ``` nipkow@28091 ` 853` ``` "\ = { real(i::int)/real(j::int) |i j. j \ 0}" (is "_ = ?S") ``` nipkow@28001 ` 854` ```proof ``` nipkow@28091 ` 855` ``` show "\ \ ?S" ``` nipkow@28001 ` 856` ``` proof ``` nipkow@28091 ` 857` ``` fix x::real assume "x : \" ``` nipkow@28001 ` 858` ``` then obtain r where "x = of_rat r" unfolding Rats_def .. ``` nipkow@28001 ` 859` ``` have "of_rat r : ?S" ``` nipkow@28001 ` 860` ``` by (cases r)(auto simp add:of_rat_rat real_eq_of_int) ``` nipkow@28001 ` 861` ``` thus "x : ?S" using `x = of_rat r` by simp ``` nipkow@28001 ` 862` ``` qed ``` nipkow@28001 ` 863` ```next ``` nipkow@28091 ` 864` ``` show "?S \ \" ``` nipkow@28001 ` 865` ``` proof(auto simp:Rats_def) ``` nipkow@28001 ` 866` ``` fix i j :: int assume "j \ 0" ``` nipkow@28001 ` 867` ``` hence "real i / real j = of_rat(Fract i j)" ``` nipkow@28001 ` 868` ``` by (simp add:of_rat_rat real_eq_of_int) ``` nipkow@28001 ` 869` ``` thus "real i / real j \ range of_rat" by blast ``` nipkow@28001 ` 870` ``` qed ``` nipkow@28001 ` 871` ```qed ``` nipkow@28001 ` 872` nipkow@28001 ` 873` ```lemma Rats_eq_int_div_nat: ``` nipkow@28091 ` 874` ``` "\ = { real(i::int)/real(n::nat) |i n. n \ 0}" ``` nipkow@28001 ` 875` ```proof(auto simp:Rats_eq_int_div_int) ``` nipkow@28001 ` 876` ``` fix i j::int assume "j \ 0" ``` nipkow@28001 ` 877` ``` show "EX (i'::int) (n::nat). real i/real j = real i'/real n \ 00" ``` nipkow@28001 ` 880` ``` hence "real i/real j = real i/real(nat j) \ 00" ``` nipkow@28001 ` 885` ``` hence "real i/real j = real(-i)/real(nat(-j)) \ 00` ``` nipkow@28001 ` 886` ``` by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) ``` nipkow@28001 ` 887` ``` thus ?thesis by blast ``` nipkow@28001 ` 888` ``` qed ``` nipkow@28001 ` 889` ```next ``` nipkow@28001 ` 890` ``` fix i::int and n::nat assume "0 < n" ``` nipkow@28001 ` 891` ``` hence "real i/real n = real i/real(int n) \ int n \ 0" by simp ``` nipkow@28001 ` 892` ``` thus "\(i'::int) j::int. real i/real n = real i'/real j \ j \ 0" by blast ``` nipkow@28001 ` 893` ```qed ``` nipkow@28001 ` 894` nipkow@28001 ` 895` ```lemma Rats_abs_nat_div_natE: ``` nipkow@28001 ` 896` ``` assumes "x \ \" ``` huffman@31706 ` 897` ``` obtains m n :: nat ``` huffman@31706 ` 898` ``` where "n \ 0" and "\x\ = real m / real n" and "gcd m n = 1" ``` nipkow@28001 ` 899` ```proof - ``` nipkow@28001 ` 900` ``` from `x \ \` obtain i::int and n::nat where "n \ 0" and "x = real i / real n" ``` nipkow@28001 ` 901` ``` by(auto simp add: Rats_eq_int_div_nat) ``` nipkow@28001 ` 902` ``` hence "\x\ = real(nat(abs i)) / real n" by simp ``` nipkow@28001 ` 903` ``` then obtain m :: nat where x_rat: "\x\ = real m / real n" by blast ``` nipkow@28001 ` 904` ``` let ?gcd = "gcd m n" ``` huffman@31706 ` 905` ``` from `n\0` have gcd: "?gcd \ 0" by simp ``` nipkow@28001 ` 906` ``` let ?k = "m div ?gcd" ``` nipkow@28001 ` 907` ``` let ?l = "n div ?gcd" ``` nipkow@28001 ` 908` ``` let ?gcd' = "gcd ?k ?l" ``` nipkow@28001 ` 909` ``` have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m" ``` nipkow@28001 ` 910` ``` by (rule dvd_mult_div_cancel) ``` nipkow@28001 ` 911` ``` have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n" ``` nipkow@28001 ` 912` ``` by (rule dvd_mult_div_cancel) ``` nipkow@28001 ` 913` ``` from `n\0` and gcd_l have "?l \ 0" by (auto iff del: neq0_conv) ``` nipkow@28001 ` 914` ``` moreover ``` nipkow@28001 ` 915` ``` have "\x\ = real ?k / real ?l" ``` nipkow@28001 ` 916` ``` proof - ``` nipkow@28001 ` 917` ``` from gcd have "real ?k / real ?l = ``` nipkow@28001 ` 918` ``` real (?gcd * ?k) / real (?gcd * ?l)" by simp ``` nipkow@28001 ` 919` ``` also from gcd_k and gcd_l have "\ = real m / real n" by simp ``` nipkow@28001 ` 920` ``` also from x_rat have "\ = \x\" .. ``` nipkow@28001 ` 921` ``` finally show ?thesis .. ``` nipkow@28001 ` 922` ``` qed ``` nipkow@28001 ` 923` ``` moreover ``` nipkow@28001 ` 924` ``` have "?gcd' = 1" ``` nipkow@28001 ` 925` ``` proof - ``` nipkow@28001 ` 926` ``` have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)" ``` nipkow@31952 ` 927` ``` by (rule gcd_mult_distrib_nat) ``` nipkow@28001 ` 928` ``` with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp ``` huffman@31706 ` 929` ``` with gcd show ?thesis by auto ``` nipkow@28001 ` 930` ``` qed ``` nipkow@28001 ` 931` ``` ultimately show ?thesis .. ``` nipkow@28001 ` 932` ```qed ``` nipkow@28001 ` 933` nipkow@28001 ` 934` paulson@14387 ` 935` ```subsection{*Numerals and Arithmetic*} ``` paulson@14387 ` 936` haftmann@25571 ` 937` ```instantiation real :: number_ring ``` haftmann@25571 ` 938` ```begin ``` haftmann@25571 ` 939` haftmann@25571 ` 940` ```definition ``` haftmann@28562 ` 941` ``` real_number_of_def [code del]: "number_of w = real_of_int w" ``` haftmann@25571 ` 942` haftmann@25571 ` 943` ```instance ``` haftmann@24198 ` 944` ``` by intro_classes (simp add: real_number_of_def) ``` paulson@14387 ` 945` haftmann@25571 ` 946` ```end ``` haftmann@25571 ` 947` haftmann@32069 ` 948` ```lemma [code_unfold_post]: ``` haftmann@24198 ` 949` ``` "number_of k = real_of_int (number_of k)" ``` haftmann@24198 ` 950` ``` unfolding number_of_is_id real_number_of_def .. ``` paulson@14387 ` 951` paulson@14387 ` 952` paulson@14387 ` 953` ```text{*Collapse applications of @{term real} to @{term number_of}*} ``` paulson@14387 ` 954` ```lemma real_number_of [simp]: "real (number_of v :: int) = number_of v" ``` huffman@35216 ` 955` ```by (simp add: real_of_int_def) ``` paulson@14387 ` 956` paulson@14387 ` 957` ```lemma real_of_nat_number_of [simp]: ``` paulson@14387 ` 958` ``` "real (number_of v :: nat) = ``` paulson@14387 ` 959` ``` (if neg (number_of v :: int) then 0 ``` paulson@14387 ` 960` ``` else (number_of v :: real))" ``` huffman@35216 ` 961` ```by (simp add: real_of_int_real_of_nat [symmetric]) ``` paulson@14387 ` 962` haftmann@31100 ` 963` ```declaration {* ``` haftmann@31100 ` 964` ``` K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2] ``` haftmann@31100 ` 965` ``` (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *) ``` haftmann@31100 ` 966` ``` #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2] ``` haftmann@31100 ` 967` ``` (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *) ``` haftmann@31100 ` 968` ``` #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add}, ``` haftmann@31100 ` 969` ``` @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one}, ``` haftmann@31100 ` 970` ``` @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff}, ``` haftmann@31100 ` 971` ``` @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq}, ``` haftmann@31100 ` 972` ``` @{thm real_of_nat_number_of}, @{thm real_number_of}] ``` haftmann@31100 ` 973` ``` #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) ``` haftmann@31100 ` 974` ``` #> Lin_Arith.add_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)) ``` haftmann@31100 ` 975` ```*} ``` paulson@14387 ` 976` kleing@19023 ` 977` paulson@14387 ` 978` ```subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*} ``` paulson@14387 ` 979` paulson@14387 ` 980` ```text{*Needed in this non-standard form by Hyperreal/Transcendental*} ``` paulson@14387 ` 981` ```lemma real_0_le_divide_iff: ``` paulson@14387 ` 982` ``` "((0::real) \ x/y) = ((x \ 0 | 0 \ y) & (0 \ x | y \ 0))" ``` paulson@14387 ` 983` ```by (simp add: real_divide_def zero_le_mult_iff, auto) ``` paulson@14387 ` 984` paulson@14387 ` 985` ```lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" ``` paulson@14387 ` 986` ```by arith ``` paulson@14387 ` 987` paulson@15085 ` 988` ```lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)" ``` paulson@14387 ` 989` ```by auto ``` paulson@14387 ` 990` paulson@15085 ` 991` ```lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)" ``` paulson@14387 ` 992` ```by auto ``` paulson@14387 ` 993` paulson@15085 ` 994` ```lemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)" ``` paulson@14387 ` 995` ```by auto ``` paulson@14387 ` 996` paulson@15085 ` 997` ```lemma real_add_le_0_iff: "(x+y \ (0::real)) = (y \ -x)" ``` paulson@14387 ` 998` ```by auto ``` paulson@14387 ` 999` paulson@15085 ` 1000` ```lemma real_0_le_add_iff: "((0::real) \ x+y) = (-x \ y)" ``` paulson@14387 ` 1001` ```by auto ``` paulson@14387 ` 1002` paulson@14387 ` 1003` paulson@14387 ` 1004` ```(* ``` paulson@14387 ` 1005` ```FIXME: we should have this, as for type int, but many proofs would break. ``` paulson@14387 ` 1006` ```It replaces x+-y by x-y. ``` paulson@15086 ` 1007` ```declare real_diff_def [symmetric, simp] ``` paulson@14387 ` 1008` ```*) ``` paulson@14387 ` 1009` paulson@14387 ` 1010` ```subsubsection{*Density of the Reals*} ``` paulson@14387 ` 1011` paulson@14387 ` 1012` ```lemma real_lbound_gt_zero: ``` paulson@14387 ` 1013` ``` "[| (0::real) < d1; 0 < d2 |] ==> \e. 0 < e & e < d1 & e < d2" ``` paulson@14387 ` 1014` ```apply (rule_tac x = " (min d1 d2) /2" in exI) ``` paulson@14387 ` 1015` ```apply (simp add: min_def) ``` paulson@14387 ` 1016` ```done ``` paulson@14387 ` 1017` paulson@14387 ` 1018` haftmann@35050 ` 1019` ```text{*Similar results are proved in @{text Fields}*} ``` paulson@14387 ` 1020` ```lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" ``` paulson@14387 ` 1021` ``` by auto ``` paulson@14387 ` 1022` paulson@14387 ` 1023` ```lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" ``` paulson@14387 ` 1024` ``` by auto ``` paulson@14387 ` 1025` paulson@14387 ` 1026` paulson@14387 ` 1027` ```subsection{*Absolute Value Function for the Reals*} ``` paulson@14387 ` 1028` paulson@14387 ` 1029` ```lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" ``` paulson@15003 ` 1030` ```by (simp add: abs_if) ``` paulson@14387 ` 1031` huffman@23289 ` 1032` ```(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *) ``` paulson@14387 ` 1033` ```lemma abs_le_interval_iff: "(abs x \ r) = (-r\x & x\(r::real))" ``` haftmann@35050 ` 1034` ```by (force simp add: abs_le_iff) ``` paulson@14387 ` 1035` paulson@14387 ` 1036` ```lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" ``` paulson@15003 ` 1037` ```by (simp add: abs_if) ``` paulson@14387 ` 1038` paulson@14387 ` 1039` ```lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" ``` huffman@22958 ` 1040` ```by (rule abs_of_nonneg [OF real_of_nat_ge_zero]) ``` paulson@14387 ` 1041` paulson@14387 ` 1042` ```lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" ``` webertj@20217 ` 1043` ```by simp ``` paulson@14387 ` 1044` ``` ``` paulson@14387 ` 1045` ```lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)" ``` webertj@20217 ` 1046` ```by simp ``` paulson@14387 ` 1047` berghofe@24534 ` 1048` haftmann@27544 ` 1049` ```subsection {* Implementation of rational real numbers *} ``` berghofe@24534 ` 1050` haftmann@27544 ` 1051` ```definition Ratreal :: "rat \ real" where ``` haftmann@27544 ` 1052` ``` [simp]: "Ratreal = of_rat" ``` berghofe@24534 ` 1053` haftmann@24623 ` 1054` ```code_datatype Ratreal ``` berghofe@24534 ` 1055` haftmann@31998 ` 1056` ```lemma Ratreal_number_collapse [code_post]: ``` haftmann@27544 ` 1057` ``` "Ratreal 0 = 0" ``` haftmann@27544 ` 1058` ``` "Ratreal 1 = 1" ``` haftmann@27544 ` 1059` ``` "Ratreal (number_of k) = number_of k" ``` haftmann@27544 ` 1060` ```by simp_all ``` berghofe@24534 ` 1061` haftmann@31998 ` 1062` ```lemma zero_real_code [code, code_unfold]: ``` haftmann@27544 ` 1063` ``` "0 = Ratreal 0" ``` haftmann@27544 ` 1064` ```by simp ``` berghofe@24534 ` 1065` haftmann@31998 ` 1066` ```lemma one_real_code [code, code_unfold]: ``` haftmann@27544 ` 1067` ``` "1 = Ratreal 1" ``` haftmann@27544 ` 1068` ```by simp ``` haftmann@27544 ` 1069` haftmann@31998 ` 1070` ```lemma number_of_real_code [code_unfold]: ``` haftmann@27544 ` 1071` ``` "number_of k = Ratreal (number_of k)" ``` haftmann@27544 ` 1072` ```by simp ``` haftmann@27544 ` 1073` haftmann@31998 ` 1074` ```lemma Ratreal_number_of_quotient [code_post]: ``` haftmann@27544 ` 1075` ``` "Ratreal (number_of r) / Ratreal (number_of s) = number_of r / number_of s" ``` haftmann@27544 ` 1076` ```by simp ``` haftmann@27544 ` 1077` haftmann@31998 ` 1078` ```lemma Ratreal_number_of_quotient2 [code_post]: ``` haftmann@27544 ` 1079` ``` "Ratreal (number_of r / number_of s) = number_of r / number_of s" ``` haftmann@27544 ` 1080` ```unfolding Ratreal_number_of_quotient [symmetric] Ratreal_def of_rat_divide .. ``` berghofe@24534 ` 1081` haftmann@26513 ` 1082` ```instantiation real :: eq ``` haftmann@26513 ` 1083` ```begin ``` haftmann@26513 ` 1084` haftmann@27544 ` 1085` ```definition "eq_class.eq (x\real) y \ x - y = 0" ``` haftmann@26513 ` 1086` haftmann@26513 ` 1087` ```instance by default (simp add: eq_real_def) ``` berghofe@24534 ` 1088` haftmann@27544 ` 1089` ```lemma real_eq_code [code]: "eq_class.eq (Ratreal x) (Ratreal y) \ eq_class.eq x y" ``` haftmann@27544 ` 1090` ``` by (simp add: eq_real_def eq) ``` haftmann@26513 ` 1091` haftmann@28351 ` 1092` ```lemma real_eq_refl [code nbe]: ``` haftmann@28351 ` 1093` ``` "eq_class.eq (x::real) x \ True" ``` haftmann@28351 ` 1094` ``` by (rule HOL.eq_refl) ``` haftmann@28351 ` 1095` haftmann@26513 ` 1096` ```end ``` berghofe@24534 ` 1097` haftmann@27544 ` 1098` ```lemma real_less_eq_code [code]: "Ratreal x \ Ratreal y \ x \ y" ``` haftmann@27652 ` 1099` ``` by (simp add: of_rat_less_eq) ``` berghofe@24534 ` 1100` haftmann@27544 ` 1101` ```lemma real_less_code [code]: "Ratreal x < Ratreal y \ x < y" ``` haftmann@27652 ` 1102` ``` by (simp add: of_rat_less) ``` berghofe@24534 ` 1103` haftmann@27544 ` 1104` ```lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)" ``` haftmann@27544 ` 1105` ``` by (simp add: of_rat_add) ``` berghofe@24534 ` 1106` haftmann@27544 ` 1107` ```lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)" ``` haftmann@27544 ` 1108` ``` by (simp add: of_rat_mult) ``` haftmann@27544 ` 1109` haftmann@27544 ` 1110` ```lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)" ``` haftmann@27544 ` 1111` ``` by (simp add: of_rat_minus) ``` berghofe@24534 ` 1112` haftmann@27544 ` 1113` ```lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)" ``` haftmann@27544 ` 1114` ``` by (simp add: of_rat_diff) ``` berghofe@24534 ` 1115` haftmann@27544 ` 1116` ```lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)" ``` haftmann@27544 ` 1117` ``` by (simp add: of_rat_inverse) ``` haftmann@27544 ` 1118` ``` ``` haftmann@27544 ` 1119` ```lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)" ``` haftmann@27544 ` 1120` ``` by (simp add: of_rat_divide) ``` berghofe@24534 ` 1121` haftmann@31203 ` 1122` ```definition (in term_syntax) ``` haftmann@32657 ` 1123` ``` valterm_ratreal :: "rat \ (unit \ Code_Evaluation.term) \ real \ (unit \ Code_Evaluation.term)" where ``` haftmann@32657 ` 1124` ``` [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {\} k" ``` haftmann@31203 ` 1125` haftmann@31203 ` 1126` ```notation fcomp (infixl "o>" 60) ``` haftmann@31203 ` 1127` ```notation scomp (infixl "o\" 60) ``` haftmann@31203 ` 1128` haftmann@31203 ` 1129` ```instantiation real :: random ``` haftmann@31203 ` 1130` ```begin ``` haftmann@31203 ` 1131` haftmann@31203 ` 1132` ```definition ``` haftmann@31641 ` 1133` ``` "Quickcheck.random i = Quickcheck.random i o\ (\r. Pair (valterm_ratreal r))" ``` haftmann@31203 ` 1134` haftmann@31203 ` 1135` ```instance .. ``` haftmann@31203 ` 1136` haftmann@31203 ` 1137` ```end ``` haftmann@31203 ` 1138` haftmann@31203 ` 1139` ```no_notation fcomp (infixl "o>" 60) ``` haftmann@31203 ` 1140` ```no_notation scomp (infixl "o\" 60) ``` haftmann@31203 ` 1141` haftmann@24623 ` 1142` ```text {* Setup for SML code generator *} ``` nipkow@23031 ` 1143` nipkow@23031 ` 1144` ```types_code ``` berghofe@24534 ` 1145` ``` real ("(int */ int)") ``` nipkow@23031 ` 1146` ```attach (term_of) {* ``` berghofe@24534 ` 1147` ```fun term_of_real (p, q) = ``` haftmann@24623 ` 1148` ``` let ``` haftmann@24623 ` 1149` ``` val rT = HOLogic.realT ``` berghofe@24534 ` 1150` ``` in ``` berghofe@24534 ` 1151` ``` if q = 1 orelse p = 0 then HOLogic.mk_number rT p ``` haftmann@24623 ` 1152` ``` else @{term "op / \ real \ real \ real"} \$ ``` berghofe@24534 ` 1153` ``` HOLogic.mk_number rT p \$ HOLogic.mk_number rT q ``` berghofe@24534 ` 1154` ``` end; ``` nipkow@23031 ` 1155` ```*} ``` nipkow@23031 ` 1156` ```attach (test) {* ``` nipkow@23031 ` 1157` ```fun gen_real i = ``` berghofe@24534 ` 1158` ``` let ``` berghofe@24534 ` 1159` ``` val p = random_range 0 i; ``` berghofe@24534 ` 1160` ``` val q = random_range 1 (i + 1); ``` berghofe@24534 ` 1161` ``` val g = Integer.gcd p q; ``` wenzelm@24630 ` 1162` ``` val p' = p div g; ``` wenzelm@24630 ` 1163` ``` val q' = q div g; ``` berghofe@25885 ` 1164` ``` val r = (if one_of [true, false] then p' else ~ p', ``` haftmann@31666 ` 1165` ``` if p' = 0 then 1 else q') ``` berghofe@24534 ` 1166` ``` in ``` berghofe@25885 ` 1167` ``` (r, fn () => term_of_real r) ``` berghofe@24534 ` 1168` ``` end; ``` nipkow@23031 ` 1169` ```*} ``` nipkow@23031 ` 1170` nipkow@23031 ` 1171` ```consts_code ``` haftmann@24623 ` 1172` ``` Ratreal ("(_)") ``` berghofe@24534 ` 1173` berghofe@24534 ` 1174` ```consts_code ``` berghofe@24534 ` 1175` ``` "of_int :: int \ real" ("\real'_of'_int") ``` berghofe@24534 ` 1176` ```attach {* ``` haftmann@31666 ` 1177` ```fun real_of_int i = (i, 1); ``` berghofe@24534 ` 1178` ```*} ``` berghofe@24534 ` 1179` blanchet@33197 ` 1180` ```setup {* ``` wenzelm@33209 ` 1181` ``` Nitpick.register_frac_type @{type_name real} ``` wenzelm@33209 ` 1182` ``` [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}), ``` wenzelm@33209 ` 1183` ``` (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}), ``` wenzelm@33209 ` 1184` ``` (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}), ``` wenzelm@33209 ` 1185` ``` (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}), ``` wenzelm@33209 ` 1186` ``` (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}), ``` wenzelm@33209 ` 1187` ``` (@{const_name number_real_inst.number_of_real}, @{const_name Nitpick.number_of_frac}), ``` wenzelm@33209 ` 1188` ``` (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}), ``` wenzelm@33209 ` 1189` ``` (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})] ``` blanchet@33197 ` 1190` ```*} ``` blanchet@33197 ` 1191` blanchet@33197 ` 1192` ```lemmas [nitpick_def] = inverse_real_inst.inverse_real ``` blanchet@33197 ` 1193` ``` number_real_inst.number_of_real one_real_inst.one_real ``` blanchet@33197 ` 1194` ``` ord_real_inst.less_eq_real plus_real_inst.plus_real ``` blanchet@33197 ` 1195` ``` times_real_inst.times_real uminus_real_inst.uminus_real ``` blanchet@33197 ` 1196` ``` zero_real_inst.zero_real ``` blanchet@33197 ` 1197` paulson@5588 ` 1198` ```end ```