Theorems
β’ βi. ABS i * ABS i = i * i
β’ βx y. x β β β§ y β β β x + y β β
β’ βx y. x β β β§ y β β β§ y β 0 β x / y β β
β’ βP. P 0 β§ (βx. P x β P (x + 1)) β βx. P x
β’ is_int x β§ is_int y β βxβ + βyβ = βx + yβ
β’ is_int x β§ is_int y β βxβ * βyβ = βx * yβ
β’ βreal_of_int iβ = i
β’ βx. x β β β§ x β 0 β 1 / x β β
β’ is_int x β§ is_int y β is_int (x + y)
β’ is_int x β§ is_int (x + y) β is_int y
β’ is_int x β§ is_int y β is_int (x * y)
β’ is_int x β βi. x = real_of_int i
β’ βx y. x β β β§ y β β β x * y β β
β’ βn. &n β β β§ -&n β β
β’ βi1 i2. i1 β€ 0 β§ i2 β€ 0 β (Num i1 < Num i2 β i2 < i1)
β’ βi1 i2.
i1 β€ 0 β§ 0 β€ i2 β
(Num i1 < Num i2 β 0 < i1 + i2) β§ (Num i2 < Num i1 β i1 + i2 < 0) β§
(Num i1 = Num i2 β i1 + i2 = 0)
β’ βx. x β β β -x β β
β’ βx y. x < y β βr. r β β β§ x < r β§ r < y
β’ βx y. 0 β€ x β§ x < y β βr. r β β β§ x < r β§ r < y
β’ rat_of_int (RATN r1 * &RATD r2 + &RATD r1 * RATN r2) /
&(RATD r1 * RATD r2) =
r1 + r2
β’ rat_of_int (RATN r1 * RATN r2) / &(RATD r1 * RATD r2) = r1 * r2
β’ q1 β 0 β§ q2 β 0 β (p1 / q1 = p2 / q2 β p1 * q2 = p2 * q1)
β’ b β 0 β§ d β 0 β a / b * (c / d) = a * c / (b * d)
β’ rat_of_int a β rat_of_int b = rat_of_int (a β b)
β’ is_int a β§ is_int b β (a < b β a + 1 β€ b)
β’ a < b β c β c < b β a
β’ real_of_rat r1 + real_of_rat r2 = real_of_rat (r1 + r2)
β’ r2 β 0 β real_of_rat r1 / real_of_rat r2 = real_of_rat (r1 / r2)
β’ real_of_rat r1 = real_of_rat r2 β r1 = r2
β’ real_of_rat r1 β€ real_of_rat r2 β r1 β€ r2
β’ real_of_rat r1 < real_of_rat r2 β r1 < r2
β’ max (real_of_rat r) (real_of_rat q) = real_of_rat (rat_max r q)
β’ min (real_of_rat r) (real_of_rat q) = real_of_rat (rat_min r q)
β’ r β 0 β (real_of_rat r)β»ΒΉ = real_of_rat (rat_minv r)
β’ real_of_rat r1 * real_of_rat r2 = real_of_rat (r1 * r2)
β’ -real_of_rat r = real_of_rat (-r)
β’ (real_of_rat q = &n β q = &n) β§ (real_of_rat q = -&n β q = -&n) β§
(real_of_rat q < &n β q < &n) β§ (real_of_rat q < -&n β q < -&n) β§
(real_of_rat q β€ &n β q β€ &n) β§ (real_of_rat q β€ -&n β q β€ -&n) β§
(&n < real_of_rat q β &n < q) β§ (-&n < real_of_rat q β -&n < q) β§
(&n β€ real_of_rat q β &n β€ q) β§ (-&n β€ real_of_rat q β -&n β€ q)
β’ real_of_rat (rat_of_int i) = real_of_int i
β’ real_of_rat (&n) = &n
β’ real_of_rat r1 β real_of_rat r2 = real_of_rat (r1 β r2)
β’ βr1. βx. is_int x β§ r1 < x
β’ βr1 r2. r1 < r2 β βq. r1 < real_of_rat q β§ real_of_rat q < r2
β’ βx y. x < y β βr. r β β β§ x < r β§ r < y
β’ βx y. x β β β§ y β β β x β y β β
β’ β =
{x | βa b. x = &a / &b β§ 0 < &b} βͺ {x | βa b. x = -(&a / &b) β§ 0 < &b}
β’ β = {r | βq. r = real_of_rat q}
β’ β =
{x | βa b. x = &a / &b β§ 0 < &b} βͺ {x | βa b. x = -(&a / &b) β§ 0 < &b}