src/HOL/Real/RealDef.thy
 author paulson Fri Apr 23 11:04:07 2004 +0200 (2004-04-23) changeset 14658 b1293d0f8d5f parent 14497 76cdbeb0c9de child 14691 e1eedc8cad37 permissions -rw-r--r--
congruent2 now allows different equiv relations
 paulson@5588 ` 1` ```(* Title : Real/RealDef.thy ``` paulson@7219 ` 2` ``` ID : \$Id\$ ``` paulson@5588 ` 3` ``` Author : Jacques D. Fleuriot ``` paulson@5588 ` 4` ``` Copyright : 1998 University of Cambridge ``` paulson@14387 ` 5` ``` Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 ``` paulson@14269 ` 6` ```*) ``` paulson@14269 ` 7` paulson@14387 ` 8` ```header{*Defining the Reals from the Positive Reals*} ``` paulson@14387 ` 9` paulson@14387 ` 10` ```theory RealDef = PReal ``` paulson@14387 ` 11` ```files ("real_arith.ML"): ``` paulson@5588 ` 12` paulson@5588 ` 13` ```constdefs ``` paulson@5588 ` 14` ``` realrel :: "((preal * preal) * (preal * preal)) set" ``` paulson@14269 ` 15` ``` "realrel == {p. \x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" ``` paulson@14269 ` 16` paulson@14484 ` 17` ```typedef (Real) real = "UNIV//realrel" ``` paulson@14269 ` 18` ``` by (auto simp add: quotient_def) ``` paulson@5588 ` 19` paulson@14269 ` 20` ```instance real :: ord .. ``` paulson@14269 ` 21` ```instance real :: zero .. ``` paulson@14269 ` 22` ```instance real :: one .. ``` paulson@14269 ` 23` ```instance real :: plus .. ``` paulson@14269 ` 24` ```instance real :: times .. ``` paulson@14269 ` 25` ```instance real :: minus .. ``` paulson@14269 ` 26` ```instance real :: inverse .. ``` paulson@14269 ` 27` paulson@14484 ` 28` ```constdefs ``` paulson@14484 ` 29` paulson@14484 ` 30` ``` (** these don't use the overloaded "real" function: users don't see them **) ``` paulson@14484 ` 31` paulson@14484 ` 32` ``` real_of_preal :: "preal => real" ``` paulson@14484 ` 33` ``` "real_of_preal m == ``` paulson@14484 ` 34` ``` Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})" ``` paulson@14484 ` 35` paulson@14269 ` 36` ```consts ``` paulson@14378 ` 37` ``` (*Overloaded constant denoting the Real subset of enclosing ``` paulson@14269 ` 38` ``` types such as hypreal and complex*) ``` paulson@14269 ` 39` ``` Reals :: "'a set" ``` paulson@14269 ` 40` paulson@14269 ` 41` ``` (*overloaded constant for injecting other types into "real"*) ``` paulson@14269 ` 42` ``` real :: "'a => real" ``` paulson@5588 ` 43` paulson@5588 ` 44` paulson@14269 ` 45` ```defs (overloaded) ``` paulson@5588 ` 46` paulson@14269 ` 47` ``` real_zero_def: ``` paulson@14484 ` 48` ``` "0 == Abs_Real(realrel``{(preal_of_rat 1, preal_of_rat 1)})" ``` paulson@12018 ` 49` paulson@14269 ` 50` ``` real_one_def: ``` paulson@14484 ` 51` ``` "1 == Abs_Real(realrel`` ``` paulson@14365 ` 52` ``` {(preal_of_rat 1 + preal_of_rat 1, ``` paulson@14365 ` 53` ``` preal_of_rat 1)})" ``` paulson@5588 ` 54` paulson@14269 ` 55` ``` real_minus_def: ``` paulson@14484 ` 56` ``` "- r == contents (\(x,y) \ Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })" ``` paulson@14484 ` 57` paulson@14484 ` 58` ``` real_add_def: ``` paulson@14484 ` 59` ``` "z + w == ``` paulson@14484 ` 60` ``` contents (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). ``` paulson@14484 ` 61` ``` { Abs_Real(realrel``{(x+u, y+v)}) })" ``` bauerg@10606 ` 62` paulson@14269 ` 63` ``` real_diff_def: ``` paulson@14484 ` 64` ``` "r - (s::real) == r + - s" ``` paulson@14484 ` 65` paulson@14484 ` 66` ``` real_mult_def: ``` paulson@14484 ` 67` ``` "z * w == ``` paulson@14484 ` 68` ``` contents (\(x,y) \ Rep_Real(z). \(u,v) \ Rep_Real(w). ``` paulson@14484 ` 69` ``` { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })" ``` paulson@5588 ` 70` paulson@14269 ` 71` ``` real_inverse_def: ``` wenzelm@11713 ` 72` ``` "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1)" ``` paulson@5588 ` 73` paulson@14269 ` 74` ``` real_divide_def: ``` bauerg@10606 ` 75` ``` "R / (S::real) == R * inverse S" ``` paulson@14269 ` 76` paulson@14484 ` 77` ``` real_le_def: ``` paulson@14484 ` 78` ``` "z \ (w::real) == ``` paulson@14484 ` 79` ``` \x y u v. x+v \ u+y & (x,y) \ Rep_Real z & (u,v) \ Rep_Real w" ``` paulson@5588 ` 80` paulson@14365 ` 81` ``` real_less_def: "(x < (y::real)) == (x \ y & x \ y)" ``` paulson@14365 ` 82` paulson@14334 ` 83` ``` real_abs_def: "abs (r::real) == (if 0 \ r then r else -r)" ``` paulson@14334 ` 84` paulson@14334 ` 85` wenzelm@12114 ` 86` ```syntax (xsymbols) ``` paulson@14269 ` 87` ``` Reals :: "'a set" ("\") ``` paulson@14365 ` 88` paulson@14365 ` 89` paulson@14329 ` 90` ```subsection{*Proving that realrel is an equivalence relation*} ``` paulson@14269 ` 91` paulson@14270 ` 92` ```lemma preal_trans_lemma: ``` paulson@14365 ` 93` ``` assumes "x + y1 = x1 + y" ``` paulson@14365 ` 94` ``` and "x + y2 = x2 + y" ``` paulson@14365 ` 95` ``` shows "x1 + y2 = x2 + (y1::preal)" ``` paulson@14365 ` 96` ```proof - ``` paulson@14365 ` 97` ``` have "(x1 + y2) + x = (x + y2) + x1" by (simp add: preal_add_ac) ``` paulson@14365 ` 98` ``` also have "... = (x2 + y) + x1" by (simp add: prems) ``` paulson@14365 ` 99` ``` also have "... = x2 + (x1 + y)" by (simp add: preal_add_ac) ``` paulson@14365 ` 100` ``` also have "... = x2 + (x + y1)" by (simp add: prems) ``` paulson@14365 ` 101` ``` also have "... = (x2 + y1) + x" by (simp add: preal_add_ac) ``` paulson@14365 ` 102` ``` finally have "(x1 + y2) + x = (x2 + y1) + x" . ``` paulson@14365 ` 103` ``` thus ?thesis by (simp add: preal_add_right_cancel_iff) ``` paulson@14365 ` 104` ```qed ``` paulson@14365 ` 105` paulson@14269 ` 106` paulson@14484 ` 107` ```lemma realrel_iff [simp]: "(((x1,y1),(x2,y2)) \ realrel) = (x1 + y2 = x2 + y1)" ``` paulson@14484 ` 108` ```by (simp add: realrel_def) ``` paulson@14269 ` 109` paulson@14269 ` 110` ```lemma equiv_realrel: "equiv UNIV realrel" ``` paulson@14365 ` 111` ```apply (auto simp add: equiv_def refl_def sym_def trans_def realrel_def) ``` paulson@14365 ` 112` ```apply (blast dest: preal_trans_lemma) ``` paulson@14269 ` 113` ```done ``` paulson@14269 ` 114` paulson@14497 ` 115` ```text{*Reduces equality of equivalence classes to the @{term realrel} relation: ``` paulson@14497 ` 116` ``` @{term "(realrel `` {x} = realrel `` {y}) = ((x,y) \ realrel)"} *} ``` paulson@14269 ` 117` ```lemmas equiv_realrel_iff = ``` paulson@14269 ` 118` ``` eq_equiv_class_iff [OF equiv_realrel UNIV_I UNIV_I] ``` paulson@14269 ` 119` paulson@14269 ` 120` ```declare equiv_realrel_iff [simp] ``` paulson@14269 ` 121` paulson@14497 ` 122` paulson@14484 ` 123` ```lemma realrel_in_real [simp]: "realrel``{(x,y)}: Real" ``` paulson@14484 ` 124` ```by (simp add: Real_def realrel_def quotient_def, blast) ``` paulson@14269 ` 125` paulson@14365 ` 126` paulson@14484 ` 127` ```lemma inj_on_Abs_Real: "inj_on Abs_Real Real" ``` paulson@14269 ` 128` ```apply (rule inj_on_inverseI) ``` paulson@14484 ` 129` ```apply (erule Abs_Real_inverse) ``` paulson@14269 ` 130` ```done ``` paulson@14269 ` 131` paulson@14484 ` 132` ```declare inj_on_Abs_Real [THEN inj_on_iff, simp] ``` paulson@14484 ` 133` ```declare Abs_Real_inverse [simp] ``` paulson@14269 ` 134` paulson@14269 ` 135` paulson@14484 ` 136` ```text{*Case analysis on the representation of a real number as an equivalence ``` paulson@14484 ` 137` ``` class of pairs of positive reals.*} ``` paulson@14484 ` 138` ```lemma eq_Abs_Real [case_names Abs_Real, cases type: real]: ``` paulson@14484 ` 139` ``` "(!!x y. z = Abs_Real(realrel``{(x,y)}) ==> P) ==> P" ``` paulson@14484 ` 140` ```apply (rule Rep_Real [of z, unfolded Real_def, THEN quotientE]) ``` paulson@14484 ` 141` ```apply (drule arg_cong [where f=Abs_Real]) ``` paulson@14484 ` 142` ```apply (auto simp add: Rep_Real_inverse) ``` paulson@14269 ` 143` ```done ``` paulson@14269 ` 144` paulson@14269 ` 145` paulson@14329 ` 146` ```subsection{*Congruence property for addition*} ``` paulson@14269 ` 147` paulson@14269 ` 148` ```lemma real_add_congruent2_lemma: ``` paulson@14269 ` 149` ``` "[|a + ba = aa + b; ab + bc = ac + bb|] ``` paulson@14269 ` 150` ``` ==> a + ab + (ba + bc) = aa + ac + (b + (bb::preal))" ``` paulson@14269 ` 151` ```apply (simp add: preal_add_assoc) ``` paulson@14269 ` 152` ```apply (rule preal_add_left_commute [of ab, THEN ssubst]) ``` paulson@14269 ` 153` ```apply (simp add: preal_add_assoc [symmetric]) ``` paulson@14269 ` 154` ```apply (simp add: preal_add_ac) ``` paulson@14269 ` 155` ```done ``` paulson@14269 ` 156` paulson@14269 ` 157` ```lemma real_add: ``` paulson@14497 ` 158` ``` "Abs_Real (realrel``{(x,y)}) + Abs_Real (realrel``{(u,v)}) = ``` paulson@14497 ` 159` ``` Abs_Real (realrel``{(x+u, y+v)})" ``` paulson@14497 ` 160` ```proof - ``` paulson@14658 ` 161` ``` have "congruent2 realrel realrel ``` paulson@14497 ` 162` ``` (\z w. (\(x,y). (\(u,v). {Abs_Real (realrel `` {(x+u, y+v)})}) w) z)" ``` paulson@14497 ` 163` ``` by (simp add: congruent2_def, blast intro: real_add_congruent2_lemma) ``` paulson@14497 ` 164` ``` thus ?thesis ``` paulson@14497 ` 165` ``` by (simp add: real_add_def UN_UN_split_split_eq ``` paulson@14658 ` 166` ``` UN_equiv_class2 [OF equiv_realrel equiv_realrel]) ``` paulson@14497 ` 167` ```qed ``` paulson@14269 ` 168` paulson@14269 ` 169` ```lemma real_add_commute: "(z::real) + w = w + z" ``` paulson@14497 ` 170` ```by (cases z, cases w, simp add: real_add preal_add_ac) ``` paulson@14269 ` 171` paulson@14269 ` 172` ```lemma real_add_assoc: "((z1::real) + z2) + z3 = z1 + (z2 + z3)" ``` paulson@14497 ` 173` ```by (cases z1, cases z2, cases z3, simp add: real_add preal_add_assoc) ``` paulson@14269 ` 174` paulson@14269 ` 175` ```lemma real_add_zero_left: "(0::real) + z = z" ``` paulson@14497 ` 176` ```by (cases z, simp add: real_add real_zero_def preal_add_ac) ``` paulson@14269 ` 177` paulson@14269 ` 178` ```instance real :: plus_ac0 ``` paulson@14269 ` 179` ``` by (intro_classes, ``` paulson@14269 ` 180` ``` (assumption | ``` paulson@14269 ` 181` ``` rule real_add_commute real_add_assoc real_add_zero_left)+) ``` paulson@14269 ` 182` paulson@14269 ` 183` paulson@14334 ` 184` ```subsection{*Additive Inverse on real*} ``` paulson@14334 ` 185` paulson@14484 ` 186` ```lemma real_minus: "- Abs_Real(realrel``{(x,y)}) = Abs_Real(realrel `` {(y,x)})" ``` paulson@14484 ` 187` ```proof - ``` paulson@14484 ` 188` ``` have "congruent realrel (\(x,y). {Abs_Real (realrel``{(y,x)})})" ``` paulson@14484 ` 189` ``` by (simp add: congruent_def preal_add_commute) ``` paulson@14484 ` 190` ``` thus ?thesis ``` paulson@14484 ` 191` ``` by (simp add: real_minus_def UN_equiv_class [OF equiv_realrel]) ``` paulson@14484 ` 192` ```qed ``` paulson@14334 ` 193` paulson@14334 ` 194` ```lemma real_add_minus_left: "(-z) + z = (0::real)" ``` paulson@14497 ` 195` ```by (cases z, simp add: real_minus real_add real_zero_def preal_add_commute) ``` paulson@14269 ` 196` paulson@14269 ` 197` paulson@14329 ` 198` ```subsection{*Congruence property for multiplication*} ``` paulson@14269 ` 199` paulson@14329 ` 200` ```lemma real_mult_congruent2_lemma: ``` paulson@14329 ` 201` ``` "!!(x1::preal). [| x1 + y2 = x2 + y1 |] ==> ``` paulson@14484 ` 202` ``` x * x1 + y * y1 + (x * y2 + y * x2) = ``` paulson@14484 ` 203` ``` x * x2 + y * y2 + (x * y1 + y * x1)" ``` paulson@14484 ` 204` ```apply (simp add: preal_add_left_commute preal_add_assoc [symmetric]) ``` paulson@14269 ` 205` ```apply (simp add: preal_add_assoc preal_add_mult_distrib2 [symmetric]) ``` paulson@14269 ` 206` ```apply (simp add: preal_add_commute) ``` paulson@14269 ` 207` ```done ``` paulson@14269 ` 208` paulson@14269 ` 209` ```lemma real_mult_congruent2: ``` paulson@14658 ` 210` ``` "congruent2 realrel realrel (%p1 p2. ``` paulson@14484 ` 211` ``` (%(x1,y1). (%(x2,y2). ``` paulson@14484 ` 212` ``` { Abs_Real (realrel``{(x1*x2 + y1*y2, x1*y2+y1*x2)}) }) p2) p1)" ``` paulson@14658 ` 213` ```apply (rule congruent2_commuteI [OF equiv_realrel], clarify) ``` paulson@14269 ` 214` ```apply (simp add: preal_mult_commute preal_add_commute) ``` paulson@14269 ` 215` ```apply (auto simp add: real_mult_congruent2_lemma) ``` paulson@14269 ` 216` ```done ``` paulson@14269 ` 217` paulson@14269 ` 218` ```lemma real_mult: ``` paulson@14484 ` 219` ``` "Abs_Real((realrel``{(x1,y1)})) * Abs_Real((realrel``{(x2,y2)})) = ``` paulson@14484 ` 220` ``` Abs_Real(realrel `` {(x1*x2+y1*y2,x1*y2+y1*x2)})" ``` paulson@14484 ` 221` ```by (simp add: real_mult_def UN_UN_split_split_eq ``` paulson@14658 ` 222` ``` UN_equiv_class2 [OF equiv_realrel equiv_realrel real_mult_congruent2]) ``` paulson@14269 ` 223` paulson@14269 ` 224` ```lemma real_mult_commute: "(z::real) * w = w * z" ``` paulson@14497 ` 225` ```by (cases z, cases w, simp add: real_mult preal_add_ac preal_mult_ac) ``` paulson@14269 ` 226` paulson@14269 ` 227` ```lemma real_mult_assoc: "((z1::real) * z2) * z3 = z1 * (z2 * z3)" ``` paulson@14484 ` 228` ```apply (cases z1, cases z2, cases z3) ``` paulson@14484 ` 229` ```apply (simp add: real_mult preal_add_mult_distrib2 preal_add_ac preal_mult_ac) ``` paulson@14269 ` 230` ```done ``` paulson@14269 ` 231` paulson@14269 ` 232` ```lemma real_mult_1: "(1::real) * z = z" ``` paulson@14484 ` 233` ```apply (cases z) ``` paulson@14484 ` 234` ```apply (simp add: real_mult real_one_def preal_add_mult_distrib2 ``` paulson@14484 ` 235` ``` preal_mult_1_right preal_mult_ac preal_add_ac) ``` paulson@14269 ` 236` ```done ``` paulson@14269 ` 237` paulson@14269 ` 238` ```lemma real_add_mult_distrib: "((z1::real) + z2) * w = (z1 * w) + (z2 * w)" ``` paulson@14484 ` 239` ```apply (cases z1, cases z2, cases w) ``` paulson@14484 ` 240` ```apply (simp add: real_add real_mult preal_add_mult_distrib2 ``` paulson@14484 ` 241` ``` preal_add_ac preal_mult_ac) ``` paulson@14269 ` 242` ```done ``` paulson@14269 ` 243` paulson@14329 ` 244` ```text{*one and zero are distinct*} ``` paulson@14365 ` 245` ```lemma real_zero_not_eq_one: "0 \ (1::real)" ``` paulson@14484 ` 246` ```proof - ``` paulson@14484 ` 247` ``` have "preal_of_rat 1 < preal_of_rat 1 + preal_of_rat 1" ``` paulson@14484 ` 248` ``` by (simp add: preal_self_less_add_left) ``` paulson@14484 ` 249` ``` thus ?thesis ``` paulson@14484 ` 250` ``` by (simp add: real_zero_def real_one_def preal_add_right_cancel_iff) ``` paulson@14484 ` 251` ```qed ``` paulson@14269 ` 252` paulson@14329 ` 253` ```subsection{*existence of inverse*} ``` paulson@14365 ` 254` paulson@14484 ` 255` ```lemma real_zero_iff: "Abs_Real (realrel `` {(x, x)}) = 0" ``` paulson@14497 ` 256` ```by (simp add: real_zero_def preal_add_commute) ``` paulson@14269 ` 257` paulson@14365 ` 258` ```text{*Instead of using an existential quantifier and constructing the inverse ``` paulson@14365 ` 259` ```within the proof, we could define the inverse explicitly.*} ``` paulson@14365 ` 260` paulson@14365 ` 261` ```lemma real_mult_inverse_left_ex: "x \ 0 ==> \y. y*x = (1::real)" ``` paulson@14484 ` 262` ```apply (simp add: real_zero_def real_one_def, cases x) ``` paulson@14269 ` 263` ```apply (cut_tac x = xa and y = y in linorder_less_linear) ``` paulson@14365 ` 264` ```apply (auto dest!: less_add_left_Ex simp add: real_zero_iff) ``` paulson@14334 ` 265` ```apply (rule_tac ``` paulson@14484 ` 266` ``` x = "Abs_Real (realrel `` { (preal_of_rat 1, ``` paulson@14365 ` 267` ``` inverse (D) + preal_of_rat 1)}) " ``` paulson@14334 ` 268` ``` in exI) ``` paulson@14334 ` 269` ```apply (rule_tac [2] ``` paulson@14484 ` 270` ``` x = "Abs_Real (realrel `` { (inverse (D) + preal_of_rat 1, ``` paulson@14365 ` 271` ``` preal_of_rat 1)})" ``` paulson@14334 ` 272` ``` in exI) ``` paulson@14365 ` 273` ```apply (auto simp add: real_mult preal_mult_1_right ``` paulson@14329 ` 274` ``` preal_add_mult_distrib2 preal_add_mult_distrib preal_mult_1 ``` paulson@14365 ` 275` ``` preal_mult_inverse_right preal_add_ac preal_mult_ac) ``` paulson@14269 ` 276` ```done ``` paulson@14269 ` 277` paulson@14365 ` 278` ```lemma real_mult_inverse_left: "x \ 0 ==> inverse(x)*x = (1::real)" ``` paulson@14484 ` 279` ```apply (simp add: real_inverse_def) ``` paulson@14365 ` 280` ```apply (frule real_mult_inverse_left_ex, safe) ``` paulson@14269 ` 281` ```apply (rule someI2, auto) ``` paulson@14269 ` 282` ```done ``` paulson@14334 ` 283` paulson@14341 ` 284` paulson@14341 ` 285` ```subsection{*The Real Numbers form a Field*} ``` paulson@14341 ` 286` paulson@14334 ` 287` ```instance real :: field ``` paulson@14334 ` 288` ```proof ``` paulson@14334 ` 289` ``` fix x y z :: real ``` paulson@14334 ` 290` ``` show "(x + y) + z = x + (y + z)" by (rule real_add_assoc) ``` paulson@14334 ` 291` ``` show "x + y = y + x" by (rule real_add_commute) ``` paulson@14334 ` 292` ``` show "0 + x = x" by simp ``` paulson@14334 ` 293` ``` show "- x + x = 0" by (rule real_add_minus_left) ``` paulson@14334 ` 294` ``` show "x - y = x + (-y)" by (simp add: real_diff_def) ``` paulson@14334 ` 295` ``` show "(x * y) * z = x * (y * z)" by (rule real_mult_assoc) ``` paulson@14334 ` 296` ``` show "x * y = y * x" by (rule real_mult_commute) ``` paulson@14334 ` 297` ``` show "1 * x = x" by (rule real_mult_1) ``` paulson@14334 ` 298` ``` show "(x + y) * z = x * z + y * z" by (simp add: real_add_mult_distrib) ``` paulson@14334 ` 299` ``` show "0 \ (1::real)" by (rule real_zero_not_eq_one) ``` paulson@14365 ` 300` ``` show "x \ 0 ==> inverse x * x = 1" by (rule real_mult_inverse_left) ``` paulson@14430 ` 301` ``` show "x / y = x * inverse y" by (simp add: real_divide_def) ``` paulson@14334 ` 302` ```qed ``` paulson@14334 ` 303` paulson@14334 ` 304` paulson@14341 ` 305` ```text{*Inverse of zero! Useful to simplify certain equations*} ``` paulson@14269 ` 306` paulson@14334 ` 307` ```lemma INVERSE_ZERO: "inverse 0 = (0::real)" ``` paulson@14484 ` 308` ```by (simp add: real_inverse_def) ``` paulson@14334 ` 309` paulson@14334 ` 310` ```instance real :: division_by_zero ``` paulson@14334 ` 311` ```proof ``` paulson@14334 ` 312` ``` show "inverse 0 = (0::real)" by (rule INVERSE_ZERO) ``` paulson@14334 ` 313` ```qed ``` paulson@14334 ` 314` paulson@14334 ` 315` paulson@14334 ` 316` ```(*Pull negations out*) ``` paulson@14334 ` 317` ```declare minus_mult_right [symmetric, simp] ``` paulson@14334 ` 318` ``` minus_mult_left [symmetric, simp] ``` paulson@14334 ` 319` paulson@14334 ` 320` ```lemma real_mult_1_right: "z * (1::real) = z" ``` paulson@14334 ` 321` ``` by (rule Ring_and_Field.mult_1_right) ``` paulson@14269 ` 322` paulson@14269 ` 323` paulson@14365 ` 324` ```subsection{*The @{text "\"} Ordering*} ``` paulson@14269 ` 325` paulson@14365 ` 326` ```lemma real_le_refl: "w \ (w::real)" ``` paulson@14484 ` 327` ```by (cases w, force simp add: real_le_def) ``` paulson@14269 ` 328` paulson@14378 ` 329` ```text{*The arithmetic decision procedure is not set up for type preal. ``` paulson@14378 ` 330` ``` This lemma is currently unused, but it could simplify the proofs of the ``` paulson@14378 ` 331` ``` following two lemmas.*} ``` paulson@14378 ` 332` ```lemma preal_eq_le_imp_le: ``` paulson@14378 ` 333` ``` assumes eq: "a+b = c+d" and le: "c \ a" ``` paulson@14378 ` 334` ``` shows "b \ (d::preal)" ``` paulson@14378 ` 335` ```proof - ``` paulson@14378 ` 336` ``` have "c+d \ a+d" by (simp add: prems preal_cancels) ``` paulson@14378 ` 337` ``` hence "a+b \ a+d" by (simp add: prems) ``` paulson@14378 ` 338` ``` thus "b \ d" by (simp add: preal_cancels) ``` paulson@14378 ` 339` ```qed ``` paulson@14378 ` 340` paulson@14378 ` 341` ```lemma real_le_lemma: ``` paulson@14378 ` 342` ``` assumes l: "u1 + v2 \ u2 + v1" ``` paulson@14378 ` 343` ``` and "x1 + v1 = u1 + y1" ``` paulson@14378 ` 344` ``` and "x2 + v2 = u2 + y2" ``` paulson@14378 ` 345` ``` shows "x1 + y2 \ x2 + (y1::preal)" ``` paulson@14365 ` 346` ```proof - ``` paulson@14378 ` 347` ``` have "(x1+v1) + (u2+y2) = (u1+y1) + (x2+v2)" by (simp add: prems) ``` paulson@14378 ` 348` ``` hence "(x1+y2) + (u2+v1) = (x2+y1) + (u1+v2)" by (simp add: preal_add_ac) ``` paulson@14378 ` 349` ``` also have "... \ (x2+y1) + (u2+v1)" ``` paulson@14365 ` 350` ``` by (simp add: prems preal_add_le_cancel_left) ``` paulson@14378 ` 351` ``` finally show ?thesis by (simp add: preal_add_le_cancel_right) ``` paulson@14378 ` 352` ```qed ``` paulson@14378 ` 353` paulson@14378 ` 354` ```lemma real_le: ``` paulson@14484 ` 355` ``` "(Abs_Real(realrel``{(x1,y1)}) \ Abs_Real(realrel``{(x2,y2)})) = ``` paulson@14484 ` 356` ``` (x1 + y2 \ x2 + y1)" ``` paulson@14378 ` 357` ```apply (simp add: real_le_def) ``` paulson@14387 ` 358` ```apply (auto intro: real_le_lemma) ``` paulson@14378 ` 359` ```done ``` paulson@14378 ` 360` paulson@14378 ` 361` ```lemma real_le_anti_sym: "[| z \ w; w \ z |] ==> z = (w::real)" ``` paulson@14497 ` 362` ```by (cases z, cases w, simp add: real_le order_antisym) ``` paulson@14378 ` 363` paulson@14378 ` 364` ```lemma real_trans_lemma: ``` paulson@14378 ` 365` ``` assumes "x + v \ u + y" ``` paulson@14378 ` 366` ``` and "u + v' \ u' + v" ``` paulson@14378 ` 367` ``` and "x2 + v2 = u2 + y2" ``` paulson@14378 ` 368` ``` shows "x + v' \ u' + (y::preal)" ``` paulson@14378 ` 369` ```proof - ``` paulson@14378 ` 370` ``` have "(x+v') + (u+v) = (x+v) + (u+v')" by (simp add: preal_add_ac) ``` paulson@14378 ` 371` ``` also have "... \ (u+y) + (u+v')" ``` paulson@14378 ` 372` ``` by (simp add: preal_add_le_cancel_right prems) ``` paulson@14378 ` 373` ``` also have "... \ (u+y) + (u'+v)" ``` paulson@14378 ` 374` ``` by (simp add: preal_add_le_cancel_left prems) ``` paulson@14378 ` 375` ``` also have "... = (u'+y) + (u+v)" by (simp add: preal_add_ac) ``` paulson@14378 ` 376` ``` finally show ?thesis by (simp add: preal_add_le_cancel_right) ``` paulson@14365 ` 377` ```qed ``` paulson@14269 ` 378` paulson@14365 ` 379` ```lemma real_le_trans: "[| i \ j; j \ k |] ==> i \ (k::real)" ``` paulson@14484 ` 380` ```apply (cases i, cases j, cases k) ``` paulson@14484 ` 381` ```apply (simp add: real_le) ``` paulson@14378 ` 382` ```apply (blast intro: real_trans_lemma) ``` paulson@14334 ` 383` ```done ``` paulson@14334 ` 384` paulson@14334 ` 385` ```(* Axiom 'order_less_le' of class 'order': *) ``` paulson@14334 ` 386` ```lemma real_less_le: "((w::real) < z) = (w \ z & w \ z)" ``` paulson@14365 ` 387` ```by (simp add: real_less_def) ``` paulson@14365 ` 388` paulson@14365 ` 389` ```instance real :: order ``` paulson@14365 ` 390` ```proof qed ``` paulson@14365 ` 391` ``` (assumption | ``` paulson@14365 ` 392` ``` rule real_le_refl real_le_trans real_le_anti_sym real_less_le)+ ``` paulson@14365 ` 393` paulson@14378 ` 394` ```(* Axiom 'linorder_linear' of class 'linorder': *) ``` paulson@14378 ` 395` ```lemma real_le_linear: "(z::real) \ w | w \ z" ``` paulson@14484 ` 396` ```apply (cases z, cases w) ``` paulson@14378 ` 397` ```apply (auto simp add: real_le real_zero_def preal_add_ac preal_cancels) ``` paulson@14334 ` 398` ```done ``` paulson@14334 ` 399` paulson@14334 ` 400` paulson@14334 ` 401` ```instance real :: linorder ``` paulson@14334 ` 402` ``` by (intro_classes, rule real_le_linear) ``` paulson@14334 ` 403` paulson@14334 ` 404` paulson@14378 ` 405` ```lemma real_le_eq_diff: "(x \ y) = (x-y \ (0::real))" ``` paulson@14484 ` 406` ```apply (cases x, cases y) ``` paulson@14378 ` 407` ```apply (auto simp add: real_le real_zero_def real_diff_def real_add real_minus ``` paulson@14378 ` 408` ``` preal_add_ac) ``` paulson@14378 ` 409` ```apply (simp_all add: preal_add_assoc [symmetric] preal_cancels) ``` paulson@14378 ` 410` ```done ``` paulson@14378 ` 411` paulson@14484 ` 412` ```lemma real_add_left_mono: ``` paulson@14484 ` 413` ``` assumes le: "x \ y" shows "z + x \ z + (y::real)" ``` paulson@14484 ` 414` ```proof - ``` paulson@14484 ` 415` ``` have "z + x - (z + y) = (z + -z) + (x - y)" ``` paulson@14484 ` 416` ``` by (simp add: diff_minus add_ac) ``` paulson@14484 ` 417` ``` with le show ?thesis ``` paulson@14484 ` 418` ``` by (simp add: real_le_eq_diff [of x] real_le_eq_diff [of "z+x"]) ``` paulson@14484 ` 419` ```qed ``` paulson@14334 ` 420` paulson@14365 ` 421` ```lemma real_sum_gt_zero_less: "(0 < S + (-W::real)) ==> (W < S)" ``` paulson@14365 ` 422` ```by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus) ``` paulson@14365 ` 423` paulson@14365 ` 424` ```lemma real_less_sum_gt_zero: "(W < S) ==> (0 < S + (-W::real))" ``` paulson@14365 ` 425` ```by (simp add: linorder_not_le [symmetric] real_le_eq_diff [of S] diff_minus) ``` paulson@14334 ` 426` paulson@14334 ` 427` ```lemma real_mult_order: "[| 0 < x; 0 < y |] ==> (0::real) < x * y" ``` paulson@14484 ` 428` ```apply (cases x, cases y) ``` paulson@14378 ` 429` ```apply (simp add: linorder_not_le [where 'a = real, symmetric] ``` paulson@14378 ` 430` ``` linorder_not_le [where 'a = preal] ``` paulson@14378 ` 431` ``` real_zero_def real_le real_mult) ``` paulson@14365 ` 432` ``` --{*Reduce to the (simpler) @{text "\"} relation *} ``` paulson@14378 ` 433` ```apply (auto dest!: less_add_left_Ex ``` paulson@14365 ` 434` ``` simp add: preal_add_ac preal_mult_ac ``` paulson@14378 ` 435` ``` preal_add_mult_distrib2 preal_cancels preal_self_less_add_right) ``` paulson@14334 ` 436` ```done ``` paulson@14334 ` 437` paulson@14334 ` 438` ```lemma real_mult_less_mono2: "[| (0::real) < z; x < y |] ==> z * x < z * y" ``` paulson@14334 ` 439` ```apply (rule real_sum_gt_zero_less) ``` paulson@14334 ` 440` ```apply (drule real_less_sum_gt_zero [of x y]) ``` paulson@14334 ` 441` ```apply (drule real_mult_order, assumption) ``` paulson@14334 ` 442` ```apply (simp add: right_distrib) ``` paulson@14334 ` 443` ```done ``` paulson@14334 ` 444` paulson@14365 ` 445` ```text{*lemma for proving @{term "0<(1::real)"}*} ``` paulson@14365 ` 446` ```lemma real_zero_le_one: "0 \ (1::real)" ``` paulson@14387 ` 447` ```by (simp add: real_zero_def real_one_def real_le ``` paulson@14378 ` 448` ``` preal_self_less_add_left order_less_imp_le) ``` paulson@14334 ` 449` paulson@14378 ` 450` paulson@14334 ` 451` ```subsection{*The Reals Form an Ordered Field*} ``` paulson@14334 ` 452` paulson@14334 ` 453` ```instance real :: ordered_field ``` paulson@14334 ` 454` ```proof ``` paulson@14334 ` 455` ``` fix x y z :: real ``` paulson@14334 ` 456` ``` show "x \ y ==> z + x \ z + y" by (rule real_add_left_mono) ``` paulson@14334 ` 457` ``` show "x < y ==> 0 < z ==> z * x < z * y" by (simp add: real_mult_less_mono2) ``` paulson@14334 ` 458` ``` show "\x\ = (if x < 0 then -x else x)" ``` paulson@14334 ` 459` ``` by (auto dest: order_le_less_trans simp add: real_abs_def linorder_not_le) ``` paulson@14334 ` 460` ```qed ``` paulson@14334 ` 461` paulson@14365 ` 462` paulson@14365 ` 463` paulson@14365 ` 464` ```text{*The function @{term real_of_preal} requires many proofs, but it seems ``` paulson@14365 ` 465` ```to be essential for proving completeness of the reals from that of the ``` paulson@14365 ` 466` ```positive reals.*} ``` paulson@14365 ` 467` paulson@14365 ` 468` ```lemma real_of_preal_add: ``` paulson@14365 ` 469` ``` "real_of_preal ((x::preal) + y) = real_of_preal x + real_of_preal y" ``` paulson@14365 ` 470` ```by (simp add: real_of_preal_def real_add preal_add_mult_distrib preal_mult_1 ``` paulson@14365 ` 471` ``` preal_add_ac) ``` paulson@14365 ` 472` paulson@14365 ` 473` ```lemma real_of_preal_mult: ``` paulson@14365 ` 474` ``` "real_of_preal ((x::preal) * y) = real_of_preal x* real_of_preal y" ``` paulson@14365 ` 475` ```by (simp add: real_of_preal_def real_mult preal_add_mult_distrib2 ``` paulson@14365 ` 476` ``` preal_mult_1 preal_mult_1_right preal_add_ac preal_mult_ac) ``` paulson@14365 ` 477` paulson@14365 ` 478` paulson@14365 ` 479` ```text{*Gleason prop 9-4.4 p 127*} ``` paulson@14365 ` 480` ```lemma real_of_preal_trichotomy: ``` paulson@14365 ` 481` ``` "\m. (x::real) = real_of_preal m | x = 0 | x = -(real_of_preal m)" ``` paulson@14484 ` 482` ```apply (simp add: real_of_preal_def real_zero_def, cases x) ``` paulson@14365 ` 483` ```apply (auto simp add: real_minus preal_add_ac) ``` paulson@14365 ` 484` ```apply (cut_tac x = x and y = y in linorder_less_linear) ``` paulson@14365 ` 485` ```apply (auto dest!: less_add_left_Ex simp add: preal_add_assoc [symmetric]) ``` paulson@14365 ` 486` ```apply (auto simp add: preal_add_commute) ``` paulson@14365 ` 487` ```done ``` paulson@14365 ` 488` paulson@14365 ` 489` ```lemma real_of_preal_leD: ``` paulson@14365 ` 490` ``` "real_of_preal m1 \ real_of_preal m2 ==> m1 \ m2" ``` paulson@14484 ` 491` ```by (simp add: real_of_preal_def real_le preal_cancels) ``` paulson@14365 ` 492` paulson@14365 ` 493` ```lemma real_of_preal_lessI: "m1 < m2 ==> real_of_preal m1 < real_of_preal m2" ``` paulson@14365 ` 494` ```by (auto simp add: real_of_preal_leD linorder_not_le [symmetric]) ``` paulson@14365 ` 495` paulson@14365 ` 496` ```lemma real_of_preal_lessD: ``` paulson@14365 ` 497` ``` "real_of_preal m1 < real_of_preal m2 ==> m1 < m2" ``` paulson@14484 ` 498` ```by (simp add: real_of_preal_def real_le linorder_not_le [symmetric] ``` paulson@14484 ` 499` ``` preal_cancels) ``` paulson@14484 ` 500` paulson@14365 ` 501` paulson@14365 ` 502` ```lemma real_of_preal_less_iff [simp]: ``` paulson@14365 ` 503` ``` "(real_of_preal m1 < real_of_preal m2) = (m1 < m2)" ``` paulson@14365 ` 504` ```by (blast intro: real_of_preal_lessI real_of_preal_lessD) ``` paulson@14365 ` 505` paulson@14365 ` 506` ```lemma real_of_preal_le_iff: ``` paulson@14365 ` 507` ``` "(real_of_preal m1 \ real_of_preal m2) = (m1 \ m2)" ``` paulson@14365 ` 508` ```by (simp add: linorder_not_less [symmetric]) ``` paulson@14365 ` 509` paulson@14365 ` 510` ```lemma real_of_preal_zero_less: "0 < real_of_preal m" ``` paulson@14365 ` 511` ```apply (auto simp add: real_zero_def real_of_preal_def real_less_def real_le_def ``` paulson@14365 ` 512` ``` preal_add_ac preal_cancels) ``` paulson@14365 ` 513` ```apply (simp_all add: preal_add_assoc [symmetric] preal_cancels) ``` paulson@14365 ` 514` ```apply (blast intro: preal_self_less_add_left order_less_imp_le) ``` paulson@14365 ` 515` ```apply (insert preal_not_eq_self [of "preal_of_rat 1" m]) ``` paulson@14365 ` 516` ```apply (simp add: preal_add_ac) ``` paulson@14365 ` 517` ```done ``` paulson@14365 ` 518` paulson@14365 ` 519` ```lemma real_of_preal_minus_less_zero: "- real_of_preal m < 0" ``` paulson@14365 ` 520` ```by (simp add: real_of_preal_zero_less) ``` paulson@14365 ` 521` paulson@14365 ` 522` ```lemma real_of_preal_not_minus_gt_zero: "~ 0 < - real_of_preal m" ``` paulson@14484 ` 523` ```proof - ``` paulson@14484 ` 524` ``` from real_of_preal_minus_less_zero ``` paulson@14484 ` 525` ``` show ?thesis by (blast dest: order_less_trans) ``` paulson@14484 ` 526` ```qed ``` paulson@14365 ` 527` paulson@14365 ` 528` paulson@14365 ` 529` ```subsection{*Theorems About the Ordering*} ``` paulson@14365 ` 530` paulson@14365 ` 531` ```text{*obsolete but used a lot*} ``` paulson@14365 ` 532` paulson@14365 ` 533` ```lemma real_not_refl2: "x < y ==> x \ (y::real)" ``` paulson@14365 ` 534` ```by blast ``` paulson@14365 ` 535` paulson@14365 ` 536` ```lemma real_le_imp_less_or_eq: "!!(x::real). x \ y ==> x < y | x = y" ``` paulson@14365 ` 537` ```by (simp add: order_le_less) ``` paulson@14365 ` 538` paulson@14365 ` 539` ```lemma real_gt_zero_preal_Ex: "(0 < x) = (\y. x = real_of_preal y)" ``` paulson@14365 ` 540` ```apply (auto simp add: real_of_preal_zero_less) ``` paulson@14365 ` 541` ```apply (cut_tac x = x in real_of_preal_trichotomy) ``` paulson@14365 ` 542` ```apply (blast elim!: real_of_preal_not_minus_gt_zero [THEN notE]) ``` paulson@14365 ` 543` ```done ``` paulson@14365 ` 544` paulson@14365 ` 545` ```lemma real_gt_preal_preal_Ex: ``` paulson@14365 ` 546` ``` "real_of_preal z < x ==> \y. x = real_of_preal y" ``` paulson@14365 ` 547` ```by (blast dest!: real_of_preal_zero_less [THEN order_less_trans] ``` paulson@14365 ` 548` ``` intro: real_gt_zero_preal_Ex [THEN iffD1]) ``` paulson@14365 ` 549` paulson@14365 ` 550` ```lemma real_ge_preal_preal_Ex: ``` paulson@14365 ` 551` ``` "real_of_preal z \ x ==> \y. x = real_of_preal y" ``` paulson@14365 ` 552` ```by (blast dest: order_le_imp_less_or_eq real_gt_preal_preal_Ex) ``` paulson@14365 ` 553` paulson@14365 ` 554` ```lemma real_less_all_preal: "y \ 0 ==> \x. y < real_of_preal x" ``` paulson@14365 ` 555` ```by (auto elim: order_le_imp_less_or_eq [THEN disjE] ``` paulson@14365 ` 556` ``` intro: real_of_preal_zero_less [THEN [2] order_less_trans] ``` paulson@14365 ` 557` ``` simp add: real_of_preal_zero_less) ``` paulson@14365 ` 558` paulson@14365 ` 559` ```lemma real_less_all_real2: "~ 0 < y ==> \x. y < real_of_preal x" ``` paulson@14365 ` 560` ```by (blast intro!: real_less_all_preal linorder_not_less [THEN iffD1]) ``` paulson@14365 ` 561` paulson@14334 ` 562` ```lemma real_add_less_le_mono: "[| w'z |] ==> w' + z' < w + (z::real)" ``` paulson@14365 ` 563` ``` by (rule Ring_and_Field.add_less_le_mono) ``` paulson@14334 ` 564` paulson@14334 ` 565` ```lemma real_add_le_less_mono: ``` paulson@14334 ` 566` ``` "!!z z'::real. [| w'\w; z' w' + z' < w + z" ``` paulson@14365 ` 567` ``` by (rule Ring_and_Field.add_le_less_mono) ``` paulson@14334 ` 568` paulson@14334 ` 569` ```lemma real_le_square [simp]: "(0::real) \ x*x" ``` paulson@14334 ` 570` ``` by (rule Ring_and_Field.zero_le_square) ``` paulson@14334 ` 571` paulson@14334 ` 572` paulson@14334 ` 573` ```subsection{*More Lemmas*} ``` paulson@14334 ` 574` paulson@14334 ` 575` ```lemma real_mult_left_cancel: "(c::real) \ 0 ==> (c*a=c*b) = (a=b)" ``` paulson@14334 ` 576` ```by auto ``` paulson@14334 ` 577` paulson@14334 ` 578` ```lemma real_mult_right_cancel: "(c::real) \ 0 ==> (a*c=b*c) = (a=b)" ``` paulson@14334 ` 579` ```by auto ``` paulson@14334 ` 580` paulson@14334 ` 581` ```text{*The precondition could be weakened to @{term "0\x"}*} ``` paulson@14334 ` 582` ```lemma real_mult_less_mono: ``` paulson@14334 ` 583` ``` "[| u u*x < v* y" ``` paulson@14334 ` 584` ``` by (simp add: Ring_and_Field.mult_strict_mono order_less_imp_le) ``` paulson@14334 ` 585` paulson@14334 ` 586` ```lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" ``` paulson@14334 ` 587` ``` by (force elim: order_less_asym ``` paulson@14334 ` 588` ``` simp add: Ring_and_Field.mult_less_cancel_right) ``` paulson@14334 ` 589` paulson@14334 ` 590` ```lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \ y*z) = (x\y)" ``` paulson@14365 ` 591` ```apply (simp add: mult_le_cancel_right) ``` paulson@14365 ` 592` ```apply (blast intro: elim: order_less_asym) ``` paulson@14365 ` 593` ```done ``` paulson@14334 ` 594` paulson@14334 ` 595` ```lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \ z*y) = (x\y)" ``` paulson@14334 ` 596` ``` by (force elim: order_less_asym ``` paulson@14334 ` 597` ``` simp add: Ring_and_Field.mult_le_cancel_left) ``` paulson@14334 ` 598` paulson@14334 ` 599` ```text{*Only two uses?*} ``` paulson@14334 ` 600` ```lemma real_mult_less_mono': ``` paulson@14334 ` 601` ``` "[| x < y; r1 < r2; (0::real) \ r1; 0 \ x|] ==> r1 * x < r2 * y" ``` paulson@14334 ` 602` ``` by (rule Ring_and_Field.mult_strict_mono') ``` paulson@14334 ` 603` paulson@14334 ` 604` ```text{*FIXME: delete or at least combine the next two lemmas*} ``` paulson@14334 ` 605` ```lemma real_sum_squares_cancel: "x * x + y * y = 0 ==> x = (0::real)" ``` paulson@14334 ` 606` ```apply (drule Ring_and_Field.equals_zero_I [THEN sym]) ``` paulson@14334 ` 607` ```apply (cut_tac x = y in real_le_square) ``` paulson@14476 ` 608` ```apply (auto, drule order_antisym, auto) ``` paulson@14334 ` 609` ```done ``` paulson@14334 ` 610` paulson@14334 ` 611` ```lemma real_sum_squares_cancel2: "x * x + y * y = 0 ==> y = (0::real)" ``` paulson@14334 ` 612` ```apply (rule_tac y = x in real_sum_squares_cancel) ``` paulson@14476 ` 613` ```apply (simp add: add_commute) ``` paulson@14334 ` 614` ```done ``` paulson@14334 ` 615` paulson@14334 ` 616` ```lemma real_add_order: "[| 0 < x; 0 < y |] ==> (0::real) < x + y" ``` paulson@14365 ` 617` ```by (drule add_strict_mono [of concl: 0 0], assumption, simp) ``` paulson@14334 ` 618` paulson@14334 ` 619` ```lemma real_le_add_order: "[| 0 \ x; 0 \ y |] ==> (0::real) \ x + y" ``` paulson@14334 ` 620` ```apply (drule order_le_imp_less_or_eq)+ ``` paulson@14334 ` 621` ```apply (auto intro: real_add_order order_less_imp_le) ``` paulson@14334 ` 622` ```done ``` paulson@14334 ` 623` paulson@14365 ` 624` ```lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" ``` paulson@14365 ` 625` ```apply (case_tac "x \ 0") ``` paulson@14365 ` 626` ```apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) ``` paulson@14365 ` 627` ```done ``` paulson@14334 ` 628` paulson@14365 ` 629` ```lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" ``` paulson@14365 ` 630` ```by (auto dest: less_imp_inverse_less) ``` paulson@14334 ` 631` paulson@14365 ` 632` ```lemma real_mult_self_sum_ge_zero: "(0::real) \ x*x + y*y" ``` paulson@14365 ` 633` ```proof - ``` paulson@14365 ` 634` ``` have "0 + 0 \ x*x + y*y" by (blast intro: add_mono zero_le_square) ``` paulson@14365 ` 635` ``` thus ?thesis by simp ``` paulson@14365 ` 636` ```qed ``` paulson@14365 ` 637` paulson@14334 ` 638` paulson@14365 ` 639` ```subsection{*Embedding the Integers into the Reals*} ``` paulson@14365 ` 640` paulson@14378 ` 641` ```defs (overloaded) ``` paulson@14378 ` 642` ``` real_of_nat_def: "real z == of_nat z" ``` paulson@14378 ` 643` ``` real_of_int_def: "real z == of_int z" ``` paulson@14365 ` 644` paulson@14365 ` 645` ```lemma real_of_int_zero [simp]: "real (0::int) = 0" ``` paulson@14378 ` 646` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 647` paulson@14365 ` 648` ```lemma real_of_one [simp]: "real (1::int) = (1::real)" ``` paulson@14378 ` 649` ```by (simp add: real_of_int_def) ``` paulson@14334 ` 650` paulson@14365 ` 651` ```lemma real_of_int_add: "real (x::int) + real y = real (x + y)" ``` paulson@14378 ` 652` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 653` ```declare real_of_int_add [symmetric, simp] ``` paulson@14365 ` 654` paulson@14365 ` 655` ```lemma real_of_int_minus: "-real (x::int) = real (-x)" ``` paulson@14378 ` 656` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 657` ```declare real_of_int_minus [symmetric, simp] ``` paulson@14365 ` 658` paulson@14365 ` 659` ```lemma real_of_int_diff: "real (x::int) - real y = real (x - y)" ``` paulson@14378 ` 660` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 661` ```declare real_of_int_diff [symmetric, simp] ``` paulson@14334 ` 662` paulson@14365 ` 663` ```lemma real_of_int_mult: "real (x::int) * real y = real (x * y)" ``` paulson@14378 ` 664` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 665` ```declare real_of_int_mult [symmetric, simp] ``` paulson@14365 ` 666` paulson@14365 ` 667` ```lemma real_of_int_zero_cancel [simp]: "(real x = 0) = (x = (0::int))" ``` paulson@14378 ` 668` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 669` paulson@14365 ` 670` ```lemma real_of_int_inject [iff]: "(real (x::int) = real y) = (x = y)" ``` paulson@14378 ` 671` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 672` paulson@14365 ` 673` ```lemma real_of_int_less_iff [iff]: "(real (x::int) < real y) = (x < y)" ``` paulson@14378 ` 674` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 675` paulson@14365 ` 676` ```lemma real_of_int_le_iff [simp]: "(real (x::int) \ real y) = (x \ y)" ``` paulson@14378 ` 677` ```by (simp add: real_of_int_def) ``` paulson@14365 ` 678` paulson@14365 ` 679` paulson@14365 ` 680` ```subsection{*Embedding the Naturals into the Reals*} ``` paulson@14365 ` 681` paulson@14334 ` 682` ```lemma real_of_nat_zero [simp]: "real (0::nat) = 0" ``` paulson@14365 ` 683` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 684` paulson@14334 ` 685` ```lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" ``` paulson@14365 ` 686` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 687` paulson@14365 ` 688` ```lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n" ``` paulson@14378 ` 689` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 690` paulson@14334 ` 691` ```(*Not for addsimps: often the LHS is used to represent a positive natural*) ``` paulson@14334 ` 692` ```lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" ``` paulson@14378 ` 693` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 694` paulson@14334 ` 695` ```lemma real_of_nat_less_iff [iff]: ``` paulson@14334 ` 696` ``` "(real (n::nat) < real m) = (n < m)" ``` paulson@14365 ` 697` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 698` paulson@14334 ` 699` ```lemma real_of_nat_le_iff [iff]: "(real (n::nat) \ real m) = (n \ m)" ``` paulson@14378 ` 700` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 701` paulson@14334 ` 702` ```lemma real_of_nat_ge_zero [iff]: "0 \ real (n::nat)" ``` paulson@14378 ` 703` ```by (simp add: real_of_nat_def zero_le_imp_of_nat) ``` paulson@14334 ` 704` paulson@14365 ` 705` ```lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" ``` paulson@14378 ` 706` ```by (simp add: real_of_nat_def del: of_nat_Suc) ``` paulson@14365 ` 707` paulson@14334 ` 708` ```lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" ``` paulson@14378 ` 709` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 710` paulson@14334 ` 711` ```lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" ``` paulson@14378 ` 712` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 713` paulson@14387 ` 714` ```lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" ``` paulson@14378 ` 715` ```by (simp add: real_of_nat_def) ``` paulson@14334 ` 716` paulson@14365 ` 717` ```lemma real_of_nat_diff: "n \ m ==> real (m - n) = real (m::nat) - real n" ``` paulson@14378 ` 718` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 719` paulson@14365 ` 720` ```lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)" ``` paulson@14378 ` 721` ```by (simp add: add: real_of_nat_def) ``` paulson@14365 ` 722` paulson@14365 ` 723` ```lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \ 0) = (n = 0)" ``` paulson@14378 ` 724` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 725` paulson@14365 ` 726` ```lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" ``` paulson@14378 ` 727` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 728` paulson@14365 ` 729` ```lemma real_of_nat_ge_zero_cancel_iff [simp]: "(0 \ real (n::nat)) = (0 \ n)" ``` paulson@14378 ` 730` ```by (simp add: add: real_of_nat_def) ``` paulson@14334 ` 731` paulson@14365 ` 732` ```lemma real_of_int_real_of_nat: "real (int n) = real n" ``` paulson@14378 ` 733` ```by (simp add: real_of_nat_def real_of_int_def int_eq_of_nat) ``` paulson@14378 ` 734` paulson@14426 ` 735` ```lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" ``` paulson@14426 ` 736` ```by (simp add: real_of_int_def real_of_nat_def) ``` paulson@14334 ` 737` paulson@14387 ` 738` paulson@14387 ` 739` paulson@14387 ` 740` ```subsection{*Numerals and Arithmetic*} ``` paulson@14387 ` 741` paulson@14387 ` 742` ```instance real :: number .. ``` paulson@14387 ` 743` paulson@14387 ` 744` ```primrec (*the type constraint is essential!*) ``` paulson@14387 ` 745` ``` number_of_Pls: "number_of bin.Pls = 0" ``` paulson@14387 ` 746` ``` number_of_Min: "number_of bin.Min = - (1::real)" ``` paulson@14387 ` 747` ``` number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) + ``` paulson@14387 ` 748` ``` (number_of w) + (number_of w)" ``` paulson@14387 ` 749` paulson@14387 ` 750` ```declare number_of_Pls [simp del] ``` paulson@14387 ` 751` ``` number_of_Min [simp del] ``` paulson@14387 ` 752` ``` number_of_BIT [simp del] ``` paulson@14387 ` 753` paulson@14387 ` 754` ```instance real :: number_ring ``` paulson@14387 ` 755` ```proof ``` paulson@14387 ` 756` ``` show "Numeral0 = (0::real)" by (rule number_of_Pls) ``` paulson@14387 ` 757` ``` show "-1 = - (1::real)" by (rule number_of_Min) ``` paulson@14387 ` 758` ``` fix w :: bin and x :: bool ``` paulson@14387 ` 759` ``` show "(number_of (w BIT x) :: real) = ``` paulson@14387 ` 760` ``` (if x then 1 else 0) + number_of w + number_of w" ``` paulson@14387 ` 761` ``` by (rule number_of_BIT) ``` paulson@14387 ` 762` ```qed ``` paulson@14387 ` 763` paulson@14387 ` 764` paulson@14387 ` 765` ```text{*Collapse applications of @{term real} to @{term number_of}*} ``` paulson@14387 ` 766` ```lemma real_number_of [simp]: "real (number_of v :: int) = number_of v" ``` paulson@14387 ` 767` ```by (simp add: real_of_int_def of_int_number_of_eq) ``` paulson@14387 ` 768` paulson@14387 ` 769` ```lemma real_of_nat_number_of [simp]: ``` paulson@14387 ` 770` ``` "real (number_of v :: nat) = ``` paulson@14387 ` 771` ``` (if neg (number_of v :: int) then 0 ``` paulson@14387 ` 772` ``` else (number_of v :: real))" ``` paulson@14387 ` 773` ```by (simp add: real_of_int_real_of_nat [symmetric] int_nat_number_of) ``` paulson@14387 ` 774` ``` ``` paulson@14387 ` 775` paulson@14387 ` 776` ```use "real_arith.ML" ``` paulson@14387 ` 777` paulson@14387 ` 778` ```setup real_arith_setup ``` paulson@14387 ` 779` paulson@14387 ` 780` ```subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*} ``` paulson@14387 ` 781` paulson@14387 ` 782` ```text{*Needed in this non-standard form by Hyperreal/Transcendental*} ``` paulson@14387 ` 783` ```lemma real_0_le_divide_iff: ``` paulson@14387 ` 784` ``` "((0::real) \ x/y) = ((x \ 0 | 0 \ y) & (0 \ x | y \ 0))" ``` paulson@14387 ` 785` ```by (simp add: real_divide_def zero_le_mult_iff, auto) ``` paulson@14387 ` 786` paulson@14387 ` 787` ```lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" ``` paulson@14387 ` 788` ```by arith ``` paulson@14387 ` 789` paulson@14387 ` 790` ```lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)" ``` paulson@14387 ` 791` ```by auto ``` paulson@14387 ` 792` paulson@14387 ` 793` ```lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)" ``` paulson@14387 ` 794` ```by auto ``` paulson@14387 ` 795` paulson@14387 ` 796` ```lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)" ``` paulson@14387 ` 797` ```by auto ``` paulson@14387 ` 798` paulson@14387 ` 799` ```lemma real_add_le_0_iff [iff]: "(x+y \ (0::real)) = (y \ -x)" ``` paulson@14387 ` 800` ```by auto ``` paulson@14387 ` 801` paulson@14387 ` 802` ```lemma real_0_le_add_iff [iff]: "((0::real) \ x+y) = (-x \ y)" ``` paulson@14387 ` 803` ```by auto ``` paulson@14387 ` 804` paulson@14387 ` 805` paulson@14387 ` 806` ```(** Simprules combining x-y and 0 (needed??) **) ``` paulson@14387 ` 807` paulson@14387 ` 808` ```lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)" ``` paulson@14387 ` 809` ```by auto ``` paulson@14387 ` 810` paulson@14387 ` 811` ```lemma real_0_le_diff_iff [iff]: "((0::real) \ x-y) = (y \ x)" ``` paulson@14387 ` 812` ```by auto ``` paulson@14387 ` 813` paulson@14387 ` 814` ```(* ``` paulson@14387 ` 815` ```FIXME: we should have this, as for type int, but many proofs would break. ``` paulson@14387 ` 816` ```It replaces x+-y by x-y. ``` paulson@14387 ` 817` ```Addsimps [symmetric real_diff_def] ``` paulson@14387 ` 818` ```*) ``` paulson@14387 ` 819` paulson@14387 ` 820` paulson@14387 ` 821` ```subsubsection{*Density of the Reals*} ``` paulson@14387 ` 822` paulson@14387 ` 823` ```lemma real_lbound_gt_zero: ``` paulson@14387 ` 824` ``` "[| (0::real) < d1; 0 < d2 |] ==> \e. 0 < e & e < d1 & e < d2" ``` paulson@14387 ` 825` ```apply (rule_tac x = " (min d1 d2) /2" in exI) ``` paulson@14387 ` 826` ```apply (simp add: min_def) ``` paulson@14387 ` 827` ```done ``` paulson@14387 ` 828` paulson@14387 ` 829` paulson@14387 ` 830` ```text{*Similar results are proved in @{text Ring_and_Field}*} ``` paulson@14387 ` 831` ```lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" ``` paulson@14387 ` 832` ``` by auto ``` paulson@14387 ` 833` paulson@14387 ` 834` ```lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" ``` paulson@14387 ` 835` ``` by auto ``` paulson@14387 ` 836` paulson@14387 ` 837` paulson@14387 ` 838` ```subsection{*Absolute Value Function for the Reals*} ``` paulson@14387 ` 839` paulson@14387 ` 840` ```text{*FIXME: these should go!*} ``` paulson@14387 ` 841` ```lemma abs_eqI1: "(0::real)\x ==> abs x = x" ``` paulson@14484 ` 842` ```by (simp add: real_abs_def) ``` paulson@14387 ` 843` paulson@14387 ` 844` ```lemma abs_eqI2: "(0::real) < x ==> abs x = x" ``` paulson@14484 ` 845` ```by (simp add: real_abs_def) ``` paulson@14387 ` 846` paulson@14387 ` 847` ```lemma abs_minus_eqI2: "x < (0::real) ==> abs x = -x" ``` paulson@14387 ` 848` ```by (simp add: real_abs_def linorder_not_less [symmetric]) ``` paulson@14387 ` 849` paulson@14387 ` 850` ```lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" ``` paulson@14484 ` 851` ```by (simp add: real_abs_def) ``` paulson@14387 ` 852` paulson@14387 ` 853` ```lemma abs_interval_iff: "(abs x < r) = (-r < x & x < (r::real))" ``` paulson@14387 ` 854` ```by (force simp add: Ring_and_Field.abs_less_iff) ``` paulson@14387 ` 855` paulson@14387 ` 856` ```lemma abs_le_interval_iff: "(abs x \ r) = (-r\x & x\(r::real))" ``` paulson@14387 ` 857` ```by (force simp add: Ring_and_Field.abs_le_iff) ``` paulson@14387 ` 858` paulson@14484 ` 859` ```(*FIXME: used only once, in SEQ.ML*) ``` paulson@14387 ` 860` ```lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)" ``` paulson@14484 ` 861` ```by (simp add: real_abs_def) ``` paulson@14387 ` 862` paulson@14387 ` 863` ```lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)" ``` paulson@14387 ` 864` ```by (auto intro: abs_eqI1 simp add: real_of_nat_ge_zero) ``` paulson@14387 ` 865` paulson@14387 ` 866` ```lemma abs_add_one_not_less_self [simp]: "~ abs(x) + (1::real) < x" ``` paulson@14387 ` 867` ```apply (simp add: linorder_not_less) ``` paulson@14387 ` 868` ```apply (auto intro: abs_ge_self [THEN order_trans]) ``` paulson@14387 ` 869` ```done ``` paulson@14387 ` 870` ``` ``` paulson@14387 ` 871` ```text{*Used only in Hyperreal/Lim.ML*} ``` paulson@14387 ` 872` ```lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)" ``` paulson@14387 ` 873` ```apply (simp add: real_add_assoc) ``` paulson@14387 ` 874` ```apply (rule_tac a1 = y in add_left_commute [THEN ssubst]) ``` paulson@14387 ` 875` ```apply (rule real_add_assoc [THEN subst]) ``` paulson@14387 ` 876` ```apply (rule abs_triangle_ineq) ``` paulson@14387 ` 877` ```done ``` paulson@14387 ` 878` paulson@14387 ` 879` paulson@14387 ` 880` paulson@14334 ` 881` ```ML ``` paulson@14334 ` 882` ```{* ``` paulson@14387 ` 883` ```val real_0_le_divide_iff = thm"real_0_le_divide_iff"; ``` paulson@14387 ` 884` ```val real_add_minus_iff = thm"real_add_minus_iff"; ``` paulson@14387 ` 885` ```val real_add_eq_0_iff = thm"real_add_eq_0_iff"; ``` paulson@14387 ` 886` ```val real_add_less_0_iff = thm"real_add_less_0_iff"; ``` paulson@14387 ` 887` ```val real_0_less_add_iff = thm"real_0_less_add_iff"; ``` paulson@14387 ` 888` ```val real_add_le_0_iff = thm"real_add_le_0_iff"; ``` paulson@14387 ` 889` ```val real_0_le_add_iff = thm"real_0_le_add_iff"; ``` paulson@14387 ` 890` ```val real_0_less_diff_iff = thm"real_0_less_diff_iff"; ``` paulson@14387 ` 891` ```val real_0_le_diff_iff = thm"real_0_le_diff_iff"; ``` paulson@14387 ` 892` ```val real_lbound_gt_zero = thm"real_lbound_gt_zero"; ``` paulson@14387 ` 893` ```val real_less_half_sum = thm"real_less_half_sum"; ``` paulson@14387 ` 894` ```val real_gt_half_sum = thm"real_gt_half_sum"; ``` paulson@14341 ` 895` paulson@14387 ` 896` ```val abs_eqI1 = thm"abs_eqI1"; ``` paulson@14387 ` 897` ```val abs_eqI2 = thm"abs_eqI2"; ``` paulson@14387 ` 898` ```val abs_minus_eqI2 = thm"abs_minus_eqI2"; ``` paulson@14387 ` 899` ```val abs_ge_zero = thm"abs_ge_zero"; ``` paulson@14387 ` 900` ```val abs_idempotent = thm"abs_idempotent"; ``` paulson@14387 ` 901` ```val abs_zero_iff = thm"abs_zero_iff"; ``` paulson@14387 ` 902` ```val abs_ge_self = thm"abs_ge_self"; ``` paulson@14387 ` 903` ```val abs_ge_minus_self = thm"abs_ge_minus_self"; ``` paulson@14387 ` 904` ```val abs_mult = thm"abs_mult"; ``` paulson@14387 ` 905` ```val abs_inverse = thm"abs_inverse"; ``` paulson@14387 ` 906` ```val abs_triangle_ineq = thm"abs_triangle_ineq"; ``` paulson@14387 ` 907` ```val abs_minus_cancel = thm"abs_minus_cancel"; ``` paulson@14387 ` 908` ```val abs_minus_add_cancel = thm"abs_minus_add_cancel"; ``` paulson@14387 ` 909` ```val abs_interval_iff = thm"abs_interval_iff"; ``` paulson@14387 ` 910` ```val abs_le_interval_iff = thm"abs_le_interval_iff"; ``` paulson@14387 ` 911` ```val abs_add_one_gt_zero = thm"abs_add_one_gt_zero"; ``` paulson@14387 ` 912` ```val abs_le_zero_iff = thm"abs_le_zero_iff"; ``` paulson@14387 ` 913` ```val abs_add_one_not_less_self = thm"abs_add_one_not_less_self"; ``` paulson@14387 ` 914` ```val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq"; ``` paulson@14334 ` 915` paulson@14387 ` 916` ```val abs_mult_less = thm"abs_mult_less"; ``` paulson@14334 ` 917` ```*} ``` paulson@10752 ` 918` paulson@14387 ` 919` paulson@5588 ` 920` ```end ```