Theory "rat"

Signature

Definitions

rat_equiv_def

⊢ ∀f1 f2.
      rat_equiv f1 f2 ⇔ frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1

rat_TY_DEF

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. rat_equiv r r ∧ c = rat_equiv r) rep

rat_bijections

⊢ (∀a. abs_rat_CLASS (rep_rat_CLASS a) = a) ∧
  ∀r.
      (λc. ∃r. rat_equiv r r ∧ c = rat_equiv r) r ⇔
      rep_rat_CLASS (abs_rat_CLASS r) = r

rep_rat_def

⊢ ∀a. rep_rat a = $@ (rep_rat_CLASS a)

abs_rat_def

⊢ ∀r. abs_rat r = abs_rat_CLASS (rat_equiv r)

rat_nmr_def

⊢ ∀r. rat_nmr r = frac_nmr (rep_rat r)

rat_dnm_def

⊢ ∀r. rat_dnm r = frac_dnm (rep_rat r)

rat_sgn_def

⊢ ∀r. rat_sgn r = frac_sgn (rep_rat r)

rat_0_def

⊢ rat_0 = abs_rat frac_0

rat_1_def

⊢ rat_1 = abs_rat frac_1

rat_ainv_def

⊢ ∀r1. -r1 = abs_rat (frac_ainv (rep_rat r1))

rat_minv_def

⊢ ∀r1. rat_minv r1 = abs_rat (frac_minv (rep_rat r1))

rat_add_def

⊢ ∀r1 r2. r1 + r2 = abs_rat (frac_add (rep_rat r1) (rep_rat r2))

rat_sub_def

⊢ ∀r1 r2. r1 − r2 = abs_rat (frac_sub (rep_rat r1) (rep_rat r2))

rat_mul_def

⊢ ∀r1 r2. r1 * r2 = abs_rat (frac_mul (rep_rat r1) (rep_rat r2))

rat_div_def

⊢ ∀r1 r2. r1 / r2 = abs_rat (frac_div (rep_rat r1) (rep_rat r2))

rat_les_def

⊢ ∀r1 r2. r1 < r2 ⇔ rat_sgn (r2 − r1) = 1

rat_gre_def

⊢ ∀r1 r2. r1 > r2 ⇔ r2 < r1

rat_leq_def

⊢ ∀r1 r2. r1 ≤ r2 ⇔ r1 < r2 ∨ r1 = r2

rat_geq_def

⊢ ∀r1 r2. r1 ≥ r2 ⇔ r2 ≤ r1

rat_cons_def

⊢ ∀nmr dnm.
      nmr // dnm = abs_rat (abs_frac (SGN nmr * SGN dnm * ABS nmr,ABS dnm))

rat_of_num_primitive_def

⊢ $& =
  WFREC (@R. WF R ∧ ∀n. R (SUC n) (SUC (SUC n)))
    (λrat_of_num a.
         case a of
           0 => I rat_0
         | SUC 0 => I rat_1
         | SUC (SUC n) => I (rat_of_num (SUC n) + rat_1))

rat_of_int_def

⊢ ∀i. rat_of_int i = if i < 0 then -&Num (-i) else &Num i

RATND_THM

⊢ ∀r.
      r = rat_of_int (RATN r) / &RATD r ∧ 0 < RATD r ∧
      (RATN r = 0 ⇒ RATD r = 1) ∧
      ∀n' d'. r = rat_of_int n' / &d' ∧ 0 < d' ⇒ ABS (RATN r) ≤ ABS n'

rat_min_def

⊢ ∀r1 r2. rat_min r1 r2 = if r1 < r2 then r1 else r2

rat_max_def

⊢ ∀r1 r2. rat_max r1 r2 = if r1 > r2 then r1 else r2

Theorems

RAT_EQUIV_REF

⊢ ∀a. rat_equiv a a

RAT_EQUIV_SYM

⊢ ∀a b. rat_equiv a b ⇔ rat_equiv b a

RAT_EQUIV_NMR_Z_IFF

⊢ ∀a b. rat_equiv a b ⇒ (frac_nmr a = 0 ⇔ frac_nmr b = 0)

RAT_EQUIV_NMR_GTZ_IFF

⊢ ∀a b. rat_equiv a b ⇒ (frac_nmr a > 0 ⇔ frac_nmr b > 0)

RAT_EQUIV_NMR_LTZ_IFF

⊢ ∀a b. rat_equiv a b ⇒ (frac_nmr a < 0 ⇔ frac_nmr b < 0)

RAT_NMR_Z_IFF_EQUIV

⊢ ∀a b. frac_nmr a = 0 ⇒ (rat_equiv a b ⇔ frac_nmr b = 0)

RAT_EQUIV_TRANS

⊢ ∀a b c. rat_equiv a b ∧ rat_equiv b c ⇒ rat_equiv a c

RAT_EQUIV

⊢ ∀f1 f2. rat_equiv f1 f2 ⇔ rat_equiv f1 = rat_equiv f2

RAT_EQUIV_ALT

⊢ ∀a.
      rat_equiv a =
      (λx.
           ∃b c.
               0 < b ∧ 0 < c ∧
               frac_mul a (abs_frac (b,b)) = frac_mul x (abs_frac (c,c)))

rat_ABS_REP_CLASS

⊢ (∀a. abs_rat_CLASS (rep_rat_CLASS a) = a) ∧
  ∀c.
      (∃r. rat_equiv r r ∧ c = rat_equiv r) ⇔
      rep_rat_CLASS (abs_rat_CLASS c) = c

rat_QUOTIENT

⊢ QUOTIENT rat_equiv abs_rat rep_rat

rat_def

⊢ QUOTIENT rat_equiv abs_rat rep_rat

rat_type_thm

⊢ (∀a. abs_rat (rep_rat a) = a) ∧ ∀r s. rat_equiv r s ⇔ abs_rat r = abs_rat s

rat_equiv_reps

⊢ rat_equiv (rep_rat r1) (rep_rat r2) ⇔ r1 = r2

rat_equiv_rep_abs

⊢ rat_equiv (rep_rat (abs_rat f)) f

rat_of_num_ind

⊢ ∀P. P 0 ∧ P (SUC 0) ∧ (∀n. P (SUC n) ⇒ P (SUC (SUC n))) ⇒ ∀v. P v

rat_of_num_def

⊢ 0 = rat_0 ∧ &SUC 0 = rat_1 ∧ ∀n. &SUC (SUC n) = &SUC n + rat_1

rat_of_num_def_compute

⊢ 0 = rat_0 ∧ &SUC 0 = rat_1 ∧
  (∀n. &SUC (NUMERAL (BIT1 n)) = &NUMERAL (BIT1 n) + rat_1) ∧
  ∀n. &SUC (NUMERAL (BIT2 n)) = &NUMERAL (BIT2 n) + rat_1

rat_0

⊢ 0 = abs_rat frac_0

rat_1

⊢ 1 = abs_rat frac_1

RAT

⊢ ∀r. abs_rat (rep_rat r) = r

RAT_ABS_EQUIV

⊢ ∀f1 f2. abs_rat f1 = abs_rat f2 ⇔ rat_equiv f1 f2

RAT_EQ

⊢ ∀f1 f2.
      abs_rat f1 = abs_rat f2 ⇔
      frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1

RAT_EQ_ALT

⊢ ∀r1 r2. r1 = r2 ⇔ rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1

RAT_NMREQ0_CONG

⊢ ∀f1. frac_nmr (rep_rat (abs_rat f1)) = 0 ⇔ frac_nmr f1 = 0

RAT_NMRLT0_CONG

⊢ ∀f1. frac_nmr (rep_rat (abs_rat f1)) < 0 ⇔ frac_nmr f1 < 0

RAT_NMRGT0_CONG

⊢ ∀f1. frac_nmr (rep_rat (abs_rat f1)) > 0 ⇔ frac_nmr f1 > 0

RAT_SGN_CONG

⊢ ∀f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1

RAT_AINV_CONG

⊢ ∀x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x)

FRAC_MINV_EQUIV

⊢ frac_nmr y ≠ 0 ⇒ rat_equiv x y ⇒ rat_equiv (frac_minv x) (frac_minv y)

RAT_MINV_CONG

⊢ ∀x.
      frac_nmr x ≠ 0 ⇒
      abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x)

FRAC_ADD_EQUIV1

⊢ rat_equiv x x' ⇒ rat_equiv (frac_add x y) (frac_add x' y)

RAT_ADD_CONG1

⊢ ∀x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)

RAT_ADD_CONG2

⊢ ∀x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)

RAT_ADD_CONG

⊢ (∀x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)) ∧
  ∀x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)

FRAC_MUL_EQUIV1

⊢ rat_equiv x x' ⇒ rat_equiv (frac_mul x y) (frac_mul x' y)

FRAC_MUL_EQUIV2

⊢ rat_equiv x x' ⇒ rat_equiv (frac_mul y x) (frac_mul y x')

RAT_MUL_CONG1

⊢ ∀x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)

RAT_MUL_CONG2

⊢ ∀x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)

RAT_MUL_CONG

⊢ (∀x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)) ∧
  ∀x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)

RAT_SUB_CONG1

⊢ ∀x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)

RAT_SUB_CONG2

⊢ ∀x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)

RAT_SUB_CONG

⊢ (∀x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)) ∧
  ∀x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)

RAT_DIV_CONG1

⊢ ∀x y.
      frac_nmr y ≠ 0 ⇒
      abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)

RAT_DIV_CONG2

⊢ ∀x y.
      frac_nmr y ≠ 0 ⇒
      abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y)

RAT_DIV_CONG

⊢ (∀x y.
       frac_nmr y ≠ 0 ⇒
       abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)) ∧
  ∀x y.
      frac_nmr y ≠ 0 ⇒
      abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y)

RAT_NMRDNM_EQ

⊢ abs_rat (abs_frac (frac_nmr f1,frac_dnm f1)) = 1 ⇔ frac_nmr f1 = frac_dnm f1

RAT_AINV_CALCULATE

⊢ ∀f1. -abs_rat f1 = abs_rat (frac_ainv f1)

RAT_MINV_CALCULATE

⊢ ∀f1. 0 ≠ frac_nmr f1 ⇒ rat_minv (abs_rat f1) = abs_rat (frac_minv f1)

RAT_ADD_CALCULATE

⊢ ∀f1 f2. abs_rat f1 + abs_rat f2 = abs_rat (frac_add f1 f2)

RAT_SUB_CALCULATE

⊢ ∀f1 f2. abs_rat f1 − abs_rat f2 = abs_rat (frac_sub f1 f2)

RAT_MUL_CALCULATE

⊢ ∀f1 f2. abs_rat f1 * abs_rat f2 = abs_rat (frac_mul f1 f2)

RAT_DIV_CALCULATE

⊢ ∀f1 f2. frac_nmr f2 ≠ 0 ⇒ abs_rat f1 / abs_rat f2 = abs_rat (frac_div f1 f2)

RAT_EQ_CALCULATE

⊢ ∀f1 f2.
      abs_rat f1 = abs_rat f2 ⇔
      frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1

RAT_LES_CALCULATE

⊢ ∀f1 f2.
      abs_rat f1 < abs_rat f2 ⇔
      frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1

RAT_LEQ_CALCULATE

⊢ ∀f1 f2.
      abs_rat f1 ≤ abs_rat f2 ⇔
      frac_nmr f1 * frac_dnm f2 ≤ frac_nmr f2 * frac_dnm f1

RAT_OF_NUM_CALCULATE

⊢ ∀n1. &n1 = abs_rat (abs_frac (&n1,1))

RAT_OF_NUM_LEQ

⊢ &a ≤ &b ⇔ a ≤ b

RAT_OF_NUM_LES

⊢ &a < &b ⇔ a < b

RAT_EQ0_NMR

⊢ ∀r1. r1 = 0 ⇔ rat_nmr r1 = 0

RAT_0LES_NMR

⊢ ∀r1. 0 < r1 ⇔ 0 < rat_nmr r1

RAT_LES0_NMR

⊢ ∀r1. r1 < 0 ⇔ rat_nmr r1 < 0

RAT_0LEQ_NMR

⊢ ∀r1. 0 ≤ r1 ⇔ 0 ≤ rat_nmr r1

RAT_LEQ0_NMR

⊢ ∀r1. r1 ≤ 0 ⇔ rat_nmr r1 ≤ 0

RAT_ADD_ASSOC

⊢ ∀a b c. a + (b + c) = a + b + c

RAT_MUL_ASSOC

⊢ ∀a b c. a * (b * c) = a * b * c

RAT_ADD_COMM

⊢ ∀a b. a + b = b + a

RAT_MUL_COMM

⊢ ∀a b. a * b = b * a

RAT_ADD_RID

⊢ ∀a. a + 0 = a

RAT_ADD_LID

⊢ ∀a. 0 + a = a

RAT_MUL_RID

⊢ ∀a. a * 1 = a

RAT_MUL_LID

⊢ ∀a. 1 * a = a

RAT_ADD_RINV

⊢ ∀a. a + -a = 0

RAT_ADD_LINV

⊢ ∀a. -a + a = 0

RAT_MUL_RINV

⊢ ∀a. a ≠ 0 ⇒ a * rat_minv a = 1

RAT_MUL_LINV

⊢ ∀a. a ≠ 0 ⇒ rat_minv a * a = 1

RAT_RDISTRIB

⊢ ∀a b c. (a + b) * c = a * c + b * c

RAT_LDISTRIB

⊢ ∀a b c. c * (a + b) = c * a + c * b

RAT_1_NOT_0

⊢ 1 ≠ 0

RAT_MUL_LZERO

⊢ ∀r1. 0 * r1 = 0

RAT_MUL_RZERO

⊢ ∀r1. r1 * 0 = 0

RAT_SUB_ADDAINV

⊢ ∀r1 r2. r1 − r2 = r1 + -r2

RAT_DIV_MULMINV

⊢ ∀r1 r2. r1 / r2 = r1 * rat_minv r2

RAT_DIV_0

⊢ 0 / x = 0

RAT_AINV_0

⊢ -0 = 0

RAT_AINV_AINV

⊢ ∀r1. - -r1 = r1

RAT_AINV_ADD

⊢ ∀r1 r2. -(r1 + r2) = -r1 + -r2

RAT_AINV_SUB

⊢ ∀r1 r2. -(r1 − r2) = r2 − r1

RAT_AINV_RMUL

⊢ ∀r1 r2. -(r1 * r2) = r1 * -r2

RAT_AINV_LMUL

⊢ ∀r1 r2. -(r1 * r2) = -r1 * r2

RAT_AINV_EQ

⊢ ∀r1 r2. -r1 = r2 ⇔ r1 = -r2

RAT_EQ_AINV

⊢ ∀r1 r2. -r1 = -r2 ⇔ r1 = r2

RAT_AINV_MINV

⊢ ∀r1. r1 ≠ 0 ⇒ -rat_minv r1 = rat_minv (-r1)

RAT_SUB_RDISTRIB

⊢ ∀a b c. (a − b) * c = a * c − b * c

RAT_SUB_LDISTRIB

⊢ ∀a b c. c * (a − b) = c * a − c * b

RAT_SUB_LID

⊢ ∀r1. 0 − r1 = -r1

RAT_SUB_RID

⊢ ∀r1. r1 − 0 = r1

RAT_SUB_ID

⊢ ∀r. r − r = 0

RAT_EQ_SUB0

⊢ ∀r1 r2. r1 − r2 = 0 ⇔ r1 = r2

RAT_EQ_0SUB

⊢ ∀r1 r2. 0 = r1 − r2 ⇔ r1 = r2

RAT_SGN_CALCULATE

⊢ rat_sgn (abs_rat f1) = frac_sgn f1

RAT_SGN_CLAUSES

⊢ ∀r1.
      (rat_sgn r1 = -1 ⇔ r1 < 0) ∧ (rat_sgn r1 = 0 ⇔ r1 = 0) ∧
      (rat_sgn r1 = 1 ⇔ r1 > 0)

RAT_SGN_0

⊢ rat_sgn 0 = 0

RAT_SGN_AINV

⊢ ∀r1. -rat_sgn (-r1) = rat_sgn r1

RAT_SGN_MUL

⊢ ∀r1 r2. rat_sgn (r1 * r2) = rat_sgn r1 * rat_sgn r2

RAT_SGN_MINV

⊢ ∀r1. r1 ≠ 0 ⇒ rat_sgn (rat_minv r1) = rat_sgn r1

RAT_SGN_TOTAL

⊢ ∀r1. rat_sgn r1 = -1 ∨ rat_sgn r1 = 0 ∨ rat_sgn r1 = 1

RAT_SGN_COMPLEMENT

⊢ ∀r1.
      (rat_sgn r1 ≠ -1 ⇔ rat_sgn r1 = 0 ∨ rat_sgn r1 = 1) ∧
      (rat_sgn r1 ≠ 0 ⇔ rat_sgn r1 = -1 ∨ rat_sgn r1 = 1) ∧
      (rat_sgn r1 ≠ 1 ⇔ rat_sgn r1 = -1 ∨ rat_sgn r1 = 0)

RAT_LES_REF

⊢ ∀r1. ¬(r1 < r1)

RAT_LES_ANTISYM

⊢ ∀r1 r2. r1 < r2 ⇒ ¬(r2 < r1)

RAT_LES_TRANS

⊢ ∀r1 r2 r3. r1 < r2 ∧ r2 < r3 ⇒ r1 < r3

RAT_LES_TOTAL

⊢ ∀r1 r2. r1 < r2 ∨ r1 = r2 ∨ r2 < r1

RAT_LEQ_REF

⊢ ∀r1. r1 ≤ r1

RAT_LEQ_ANTISYM

⊢ ∀r1 r2. r1 ≤ r2 ∧ r2 ≤ r1 ⇒ r1 = r2

RAT_LEQ_TRANS

⊢ ∀r1 r2 r3. r1 ≤ r2 ∧ r2 ≤ r3 ⇒ r1 ≤ r3

RAT_LES_01

⊢ 0 < 1

RAT_LES_IMP_LEQ

⊢ ∀r1 r2. r1 < r2 ⇒ r1 ≤ r2

RAT_LES_IMP_NEQ

⊢ ∀r1 r2. r1 < r2 ⇒ r1 ≠ r2

RAT_LEQ_LES

⊢ ∀r1 r2. ¬(r2 < r1) ⇔ r1 ≤ r2

RAT_LES_LEQ

⊢ ∀r1 r2. ¬(r2 ≤ r1) ⇔ r1 < r2

RAT_LES_LEQ2

⊢ ∀r1 r2. r1 < r2 ⇔ r1 ≤ r2 ∧ ¬(r2 ≤ r1)

RAT_LES_LEQ_TRANS

⊢ ∀a b c. a < b ∧ b ≤ c ⇒ a < c

RAT_LEQ_LES_TRANS

⊢ ∀a b c. a ≤ b ∧ b < c ⇒ a < c

RAT_0LES_0LES_ADD

⊢ ∀r1 r2. 0 < r1 ⇒ 0 < r2 ⇒ 0 < r1 + r2

RAT_LES0_LES0_ADD

⊢ ∀r1 r2. r1 < 0 ⇒ r2 < 0 ⇒ r1 + r2 < 0

RAT_0LES_0LEQ_ADD

⊢ ∀r1 r2. 0 < r1 ⇒ 0 ≤ r2 ⇒ 0 < r1 + r2

RAT_LES0_LEQ0_ADD

⊢ ∀r1 r2. r1 < 0 ⇒ r2 ≤ 0 ⇒ r1 + r2 < 0

RAT_LSUB_EQ

⊢ ∀r1 r2 r3. r1 − r2 = r3 ⇔ r1 = r2 + r3

RAT_RSUB_EQ

⊢ ∀r1 r2 r3. r1 = r2 − r3 ⇔ r1 + r3 = r2

RAT_LDIV_EQ

⊢ ∀r1 r2 r3. r2 ≠ 0 ⇒ (r1 / r2 = r3 ⇔ r1 = r2 * r3)

RAT_RDIV_EQ

⊢ ∀r1 r2 r3. r3 ≠ 0 ⇒ (r1 = r2 / r3 ⇔ r1 * r3 = r2)

RAT_AINV_ONE_ONE

⊢ ONE_ONE numeric_negate

RAT_ADD_ONE_ONE

⊢ ∀r1. ONE_ONE ($+ r1)

RAT_MUL_ONE_ONE

⊢ ∀r1. r1 ≠ 0 ⇔ ONE_ONE ($* r1)

RAT_EQ_LADD

⊢ ∀r1 r2 r3. r3 + r1 = r3 + r2 ⇔ r1 = r2

RAT_EQ_RADD

⊢ ∀r1 r2 r3. r1 + r3 = r2 + r3 ⇔ r1 = r2

RAT_EQ_RMUL

⊢ ∀r1 r2 r3. r3 ≠ 0 ⇒ (r1 * r3 = r2 * r3 ⇔ r1 = r2)

RAT_EQ_LMUL

⊢ ∀r1 r2 r3. r3 ≠ 0 ⇒ (r3 * r1 = r3 * r2 ⇔ r1 = r2)

RAT_LES_RADD

⊢ ∀r1 r2 r3. r1 + r3 < r2 + r3 ⇔ r1 < r2

RAT_LES_LADD

⊢ ∀r1 r2 r3. r3 + r1 < r3 + r2 ⇔ r1 < r2

RAT_LEQ_RADD

⊢ ∀r1 r2 r3. r1 + r3 ≤ r2 + r3 ⇔ r1 ≤ r2

RAT_LEQ_LADD

⊢ ∀r1 r2 r3. r3 + r1 ≤ r3 + r2 ⇔ r1 ≤ r2

RAT_ADD_MONO

⊢ ∀a b c d. a ≤ b ∧ c ≤ d ⇒ a + c ≤ b + d

RAT_LES_AINV

⊢ ∀r1 r2. -r1 < -r2 ⇔ r2 < r1

RAT_LSUB_LES

⊢ ∀r1 r2 r3. r1 − r2 < r3 ⇔ r1 < r2 + r3

RAT_RSUB_LES

⊢ ∀r1 r2 r3. r1 < r2 − r3 ⇔ r1 + r3 < r2

RAT_LSUB_LEQ

⊢ ∀r1 r2 r3. r1 − r2 ≤ r3 ⇔ r1 ≤ r2 + r3

RAT_RSUB_LEQ

⊢ ∀r1 r2 r3. r1 ≤ r2 − r3 ⇔ r1 + r3 ≤ r2

RAT_LES_RMUL_POS

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r1 * r3 < r2 * r3 ⇔ r1 < r2)

RAT_LES_LMUL_POS

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r3 * r1 < r3 * r2 ⇔ r1 < r2)

RAT_LES_RMUL_NEG

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r2 * r3 < r1 * r3 ⇔ r1 < r2)

RAT_LES_LMUL_NEG

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r3 * r2 < r3 * r1 ⇔ r1 < r2)

RAT_AINV_LES

⊢ ∀r1 r2. -r1 < r2 ⇔ -r2 < r1

RAT_LDIV_LES_POS

⊢ ∀r1 r2 r3. 0 < r2 ⇒ (r1 / r2 < r3 ⇔ r1 < r2 * r3)

RAT_LDIV_LES_NEG

⊢ ∀r1 r2 r3. r2 < 0 ⇒ (r1 / r2 < r3 ⇔ r2 * r3 < r1)

RAT_RDIV_LES_POS

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r1 < r2 / r3 ⇔ r1 * r3 < r2)

RAT_RDIV_LES_NEG

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r1 < r2 / r3 ⇔ r2 < r1 * r3)

RAT_LDIV_LEQ_POS

⊢ ∀r1 r2 r3. 0 < r2 ⇒ (r1 / r2 ≤ r3 ⇔ r1 ≤ r2 * r3)

RAT_LDIV_LEQ_NEG

⊢ ∀r1 r2 r3. r2 < 0 ⇒ (r1 / r2 ≤ r3 ⇔ r2 * r3 ≤ r1)

RAT_RDIV_LEQ_POS

⊢ ∀r1 r2 r3. 0 < r3 ⇒ (r1 ≤ r2 / r3 ⇔ r1 * r3 ≤ r2)

RAT_RDIV_LEQ_NEG

⊢ ∀r1 r2 r3. r3 < 0 ⇒ (r1 ≤ r2 / r3 ⇔ r2 ≤ r1 * r3)

RAT_LES_SUB0

⊢ ∀r1 r2. r1 − r2 < 0 ⇔ r1 < r2

RAT_LES_0SUB

⊢ ∀r1 r2. 0 < r1 − r2 ⇔ r2 < r1

RAT_MINV_LES

⊢ ∀r1. 0 < r1 ⇒ (rat_minv r1 < 0 ⇔ r1 < 0) ∧ (0 < rat_minv r1 ⇔ 0 < r1)

RAT_MUL_SIGN_CASES

⊢ ∀p q.
      (0 < p * q ⇔ 0 < p ∧ 0 < q ∨ p < 0 ∧ q < 0) ∧
      (p * q < 0 ⇔ 0 < p ∧ q < 0 ∨ p < 0 ∧ 0 < q)

RAT_NO_ZERODIV

⊢ ∀r1 r2. r1 = 0 ∨ r2 = 0 ⇔ r1 * r2 = 0

RAT_NO_ZERODIV_THM

⊢ ∀r1 r2. r1 * r2 = 0 ⇔ r1 = 0 ∨ r2 = 0

RAT_NO_ZERODIV_NEG

⊢ ∀r1 r2. r1 * r2 ≠ 0 ⇔ r1 ≠ 0 ∧ r2 ≠ 0

RAT_NO_IDDIV

⊢ ∀r1 r2. r1 * r2 = r2 ⇔ r1 = 1 ∨ r2 = 0

RDIV_MUL_OUT

⊢ r1 * (r2 / r3) = r1 * r2 / r3

LDIV_MUL_OUT

⊢ r1 / r2 * r3 = r1 * r3 / r2

RAT_DENSE_THM

⊢ ∀r1 r3. r1 < r3 ⇒ ∃r2. r1 < r2 ∧ r2 < r3

RAT_SAVE

⊢ ∀r1. ∃a1 b1. r1 = abs_rat (frac_save a1 b1)

RAT_SAVE_MINV

⊢ ∀a1 b1.
      abs_rat (frac_save a1 b1) ≠ 0 ⇒
      rat_minv (abs_rat (frac_save a1 b1)) =
      abs_rat (frac_save (SGN a1 * (&b1 + 1)) (Num (ABS a1 − 1)))

RAT_SAVE_TO_CONS

⊢ ∀a1 b1. abs_rat (frac_save a1 b1) = a1 // (&b1 + 1)

RAT_OF_NUM

⊢ ∀n. 0 = rat_0 ∧ ∀n. &SUC n = &n + rat_1

RAT_SAVE_NUM

⊢ ∀n. &n = abs_rat (frac_save (&n) 0)

RAT_CONS_TO_NUM

⊢ ∀n. &n // 1 = &n ∧ -&n // 1 = -&n

RAT_0

⊢ rat_0 = 0

RAT_1

⊢ rat_1 = 1

RAT_MINV_1

⊢ rat_minv 1 = 1

RAT_DIV_1

⊢ r / 1 = r

RAT_DIV_NEG1

⊢ r / -1 = -r

RAT_DIV_INV

⊢ r ≠ 0 ⇒ r / r = 1

RAT_MINV_MUL

⊢ a ≠ 0 ∧ b ≠ 0 ⇒ rat_minv (a * b) = rat_minv a * rat_minv b

RAT_DIVDIV_MUL

⊢ b ≠ 0 ∧ d ≠ 0 ⇒ a / b * (c / d) = a * c / (b * d)

RAT_DIVDIV_ADD

⊢ y ≠ 0 ∧ b ≠ 0 ⇒ x / y + a / b = (x * b + a * y) / (y * b)

RAT_DIV_AINV

⊢ -(x / y) = -x / y

RAT_MINV_EQ_0

⊢ r ≠ 0 ⇒ rat_minv r ≠ 0

RAT_DIV_MINV

⊢ x ≠ 0 ∧ y ≠ 0 ⇒ rat_minv (x / y) = y / x

RAT_DIV_EQ0

⊢ d ≠ 0 ⇒ (n / d = 0 ⇔ n = 0) ∧ (0 = n / d ⇔ n = 0)

RAT_ADD_NUM_CALCULATE

⊢ (∀n m. &n + &m = &(n + m)) ∧
  (∀n m. -&n + &m = if n ≤ m then &(m − n) else -&(n − m)) ∧
  (∀n m. &n + -&m = if m ≤ n then &(n − m) else -&(m − n)) ∧
  ∀n m. -&n + -&m = -&(n + m)

RAT_MUL_NUM_CALCULATE

⊢ (∀n m. &n * &m = &(n * m)) ∧ (∀n m. -&n * &m = -&(n * m)) ∧
  (∀n m. &n * -&m = -&(n * m)) ∧ ∀n m. -&n * -&m = &(n * m)

RAT_EQ_NUM_CALCULATE

⊢ (∀n m. &n = &m ⇔ n = m) ∧ (∀n m. &n = -&m ⇔ n = 0 ∧ m = 0) ∧
  (∀n m. -&n = &m ⇔ n = 0 ∧ m = 0) ∧ ∀n m. -&n = -&m ⇔ n = m

RAT_LT_NUM_CALCULATE

⊢ (&a < &b ⇔ a < b) ∧ (-&m < &n ⇔ 0 < m ∨ 0 < n) ∧ (&m < -&n ⇔ F) ∧
  (-&m < -&n ⇔ n < m)

RAT_LE_NUM_CALCULATE

⊢ (&a ≤ &b ⇔ a ≤ b) ∧ (-&m ≤ &n ⇔ T) ∧ (&m ≤ -&n ⇔ m = 0 ∧ n = 0) ∧
  (-&m ≤ -&n ⇔ n ≤ m)

rat_of_int_11

⊢ rat_of_int i1 = rat_of_int i2 ⇔ i1 = i2

rat_of_int_of_num

⊢ rat_of_int (&x) = &x

rat_of_int_MUL

⊢ rat_of_int x * rat_of_int y = rat_of_int (x * y)

rat_of_int_ADD

⊢ rat_of_int x + rat_of_int y = rat_of_int (x + y)

rat_of_int_LE

⊢ rat_of_int i ≤ rat_of_int j ⇔ i ≤ j

rat_of_int_LT

⊢ rat_of_int i < rat_of_int j ⇔ i < j

rat_of_int_ainv

⊢ rat_of_int (-i) = -rat_of_int i

RAT_OF_INT_CALCULATE

⊢ ∀i. rat_of_int i = abs_rat (abs_frac (i,1))

RATD_NZERO

⊢ 0 < RATD r ∧ RATD r ≠ 0

RATN_LEAST

⊢ ∀n' d'. r = rat_of_int n' / &d' ∧ 0 < d' ⇒ ABS (RATN r) ≤ ABS n'

RATN_RATD_EQ_THM

⊢ r = rat_of_int (RATN r) / &RATD r

RATN_RATD_MULT

⊢ r * &RATD r = rat_of_int (RATN r)

RATND_RAT_OF_NUM

⊢ RATN (&n) = &n ∧ RATD (&n) = 1

RATN_EQ0

⊢ (RATN r = 0 ⇔ r = 0) ∧ (0 = RATN r ⇔ r = 0)

RATN_SIGN

⊢ (0 < RATN x ⇔ 0 < x) ∧ (0 ≤ RATN x ⇔ 0 ≤ x) ∧ (RATN x < 0 ⇔ x < 0) ∧
  (RATN x ≤ 0 ⇔ x ≤ 0)

RAT_AINV_SGN

⊢ (0 < -r ⇔ r < 0) ∧ (-r < 0 ⇔ 0 < r)

RATN_NEG

⊢ RATN (-r) = -RATN r

RATD_NEG

⊢ RATD (-r) = RATD r

RATN_RATD_RAT_OF_INT

⊢ RATN (rat_of_int i) = i ∧ RATD (rat_of_int i) = 1

RATN_DIV_RATD

⊢ rat_of_int (RATN r) / &RATD r = r

RAT_AINV_EQ_NUM

⊢ -x = &n ⇔ x = rat_of_int (-&n)

RAT_SGN_NUM_COND

⊢ rat_sgn (&n) = if n = 0 then 0 else 1

RAT_SGN_AINV_RWT

⊢ rat_sgn (-r) = -rat_sgn r

RAT_SGN_ALT

⊢ rat_sgn r = SGN (RATN r)

RAT_SGN_NUM_BITs

⊢ rat_sgn (&NUMERAL (BIT1 n)) = 1 ∧ rat_sgn (&NUMERAL (BIT2 n)) = 1

RAT_SGN_EQ0

⊢ (rat_sgn r = 0 ⇔ r = 0) ∧ (0 = rat_sgn r ⇔ r = 0)

RAT_SGN_POS

⊢ rat_sgn r = 1 ⇔ 0 < r

RAT_SGN_NEG

⊢ rat_sgn r = -1 ⇔ r < 0

RAT_SGN_DIV

⊢ d ≠ 0 ⇒ rat_sgn (n / d) = rat_sgn n * rat_sgn d

RAT_MINV_RATND

⊢ r ≠ 0 ⇒
  rat_minv r = rat_of_int (rat_sgn r) * &RATD r / rat_of_int (ABS (RATN r))