- frac_TY_DEF
-
|- ∃rep. TYPE_DEFINITION (λf. 0 < SND f) rep
- frac_tybij
-
|- (∀a. abs_frac (rep_frac a) = a) ∧
∀r. (λf. 0 < SND f) r ⇔ (rep_frac (abs_frac r) = r)
- frac_nmr_def
-
|- ∀f. frac_nmr f = FST (rep_frac f)
- frac_dnm_def
-
|- ∀f. frac_dnm f = SND (rep_frac f)
- frac_sgn_def
-
|- ∀f1. frac_sgn f1 = SGN (frac_nmr f1)
- frac_ainv_def
-
|- ∀f1. frac_ainv f1 = abs_frac (-frac_nmr f1,frac_dnm f1)
- frac_minv_def
-
|- ∀f1. frac_minv f1 = abs_frac (frac_sgn f1 * frac_dnm f1,ABS (frac_nmr f1))
- frac_0_def
-
|- frac_0 = abs_frac (0,1)
- frac_1_def
-
|- frac_1 = abs_frac (1,1)
- les_abs_def
-
|- ∀f1 f2.
les_abs f1 f2 ⇔ frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1
- frac_add_def
-
|- ∀f1 f2.
frac_add f1 f2 =
abs_frac
(frac_nmr f1 * frac_dnm f2 + frac_nmr f2 * frac_dnm f1,
frac_dnm f1 * frac_dnm f2)
- frac_sub_def
-
|- ∀f1 f2. frac_sub f1 f2 = frac_add f1 (frac_ainv f2)
- frac_mul_def
-
|- ∀f1 f2.
frac_mul f1 f2 =
abs_frac (frac_nmr f1 * frac_nmr f2,frac_dnm f1 * frac_dnm f2)
- frac_div_def
-
|- ∀f1 f2. frac_div f1 f2 = frac_mul f1 (frac_minv f2)
- frac_save_def
-
|- ∀nmr dnm. frac_save nmr dnm = abs_frac (nmr,&dnm + 1)
- frac_bij
-
|- (∀a. abs_frac (rep_frac a) = a) ∧
∀r. (λf. 0 < SND f) r ⇔ (rep_frac (abs_frac r) = r)
- FRAC
-
|- ∀f. abs_frac (frac_nmr f,frac_dnm f) = f
- FRAC_EQ
-
|- ∀a1 b1 a2 b2.
0 < b1 ⇒
0 < b2 ⇒
((abs_frac (a1,b1) = abs_frac (a2,b2)) ⇔ (a1 = a2) ∧ (b1 = b2))
- FRAC_EQ_ALT
-
|- ∀f1 f2.
(f1 = f2) ⇔ (frac_nmr f1 = frac_nmr f2) ∧ (frac_dnm f1 = frac_dnm f2)
- FRAC_NOT_EQ
-
|- ∀a1 b1 a2 b2.
0 < b1 ⇒ 0 < b2 ⇒ (a1,b1) ≠ (a2,b2) ⇒ abs_frac (a1,b1) ≠ abs_frac (a2,b2)
- FRAC_DNMPOS
-
|- ∀f. 0 < frac_dnm f
- NMR
-
|- ∀a b. 0 < b ⇒ (frac_nmr (abs_frac (a,b)) = a)
- DNM
-
|- ∀a b. 0 < b ⇒ (frac_dnm (abs_frac (a,b)) = b)
- FRAC_AINV_CALCULATE
-
|- ∀a1 b1. 0 < b1 ⇒ (frac_ainv (abs_frac (a1,b1)) = abs_frac (-a1,b1))
- FRAC_MINV_CALCULATE
-
|- ∀a1 b1.
0 < b1 ⇒
a1 ≠ 0 ⇒
(frac_minv (abs_frac (a1,b1)) = abs_frac (SGN a1 * b1,ABS a1))
- FRAC_SGN_CALCULATE
-
|- ∀a1 b1. 0 < b1 ⇒ (frac_sgn (abs_frac (a1,b1)) = SGN a1)
- FRAC_ADD_CALCULATE
-
|- ∀a1 b1 a2 b2.
0 < b1 ⇒
0 < b2 ⇒
(frac_add (abs_frac (a1,b1)) (abs_frac (a2,b2)) =
abs_frac (a1 * b2 + a2 * b1,b1 * b2))
- FRAC_SUB_CALCULATE
-
|- ∀a1 b1 a2 b2.
0 < b1 ⇒
0 < b2 ⇒
(frac_sub (abs_frac (a1,b1)) (abs_frac (a2,b2)) =
abs_frac (a1 * b2 − a2 * b1,b1 * b2))
- FRAC_MULT_CALCULATE
-
|- ∀a1 b1 a2 b2.
0 < b1 ⇒
0 < b2 ⇒
(frac_mul (abs_frac (a1,b1)) (abs_frac (a2,b2)) =
abs_frac (a1 * a2,b1 * b2))
- FRAC_DIV_CALCULATE
-
|- ∀a1 b1 a2 b2.
0 < b1 ⇒
0 < b2 ⇒
a2 ≠ 0 ⇒
(frac_div (abs_frac (a1,b1)) (abs_frac (a2,b2)) =
abs_frac (a1 * SGN a2 * b2,b1 * ABS a2))
- FRAC_ADD_ASSOC
-
|- ∀a b c. frac_add a (frac_add b c) = frac_add (frac_add a b) c
- FRAC_MUL_ASSOC
-
|- ∀a b c. frac_mul a (frac_mul b c) = frac_mul (frac_mul a b) c
- FRAC_ADD_COMM
-
|- ∀a b. frac_add a b = frac_add b a
- FRAC_MUL_COMM
-
|- ∀a b. frac_mul a b = frac_mul b a
- FRAC_ADD_RID
-
|- ∀a. frac_add a frac_0 = a
- FRAC_MUL_RID
-
|- ∀a. frac_mul a frac_1 = a
- FRAC_1_0
-
|- frac_1 ≠ frac_0
- FRAC_AINV_0
-
|- frac_ainv frac_0 = frac_0
- FRAC_AINV_AINV
-
|- ∀f1. frac_ainv (frac_ainv f1) = f1
- FRAC_AINV_ADD
-
|- ∀f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2)
- FRAC_AINV_SUB
-
|- ∀f1 f2. frac_ainv (frac_sub f2 f1) = frac_sub f1 f2
- FRAC_AINV_RMUL
-
|- ∀f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2)
- FRAC_AINV_LMUL
-
|- ∀f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2
- FRAC_SUB_ADD
-
|- ∀a b c. frac_sub a (frac_add b c) = frac_sub (frac_sub a b) c
- FRAC_SUB_SUB
-
|- ∀a b c. frac_sub a (frac_sub b c) = frac_add (frac_sub a b) c
- FRAC_SGN_TOTAL
-
|- ∀f1. (frac_sgn f1 = -1) ∨ (frac_sgn f1 = 0) ∨ (frac_sgn f1 = 1)
- FRAC_SGN_POS
-
|- ∀f1. (frac_sgn f1 = 1) ⇔ 0 < frac_nmr f1
- FRAC_SGN_NOT_NEG
-
|- ∀f1. frac_sgn f1 ≠ -1 ⇔ (0 = frac_nmr f1) ∨ 0 < frac_nmr f1
- FRAC_SGN_NEG
-
|- ∀f. -frac_sgn (frac_ainv f) = frac_sgn f
- FRAC_SGN_IMP_EQGT
-
|- ∀f1. frac_sgn f1 ≠ -1 ⇔ (frac_sgn f1 = 0) ∨ (frac_sgn f1 = 1)
- FRAC_SGN_MUL
-
|- ∀f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
- FRAC_ABS_SGN
-
|- ∀f1. frac_nmr f1 ≠ 0 ⇒ (ABS (frac_sgn f1) = 1)
- FRAC_SGN_MUL2
-
|- ∀f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
- FRAC_SGN_CASES
-
|- ∀f1 P.
((frac_sgn f1 = -1) ⇒ P) ∧ ((frac_sgn f1 = 0) ⇒ P) ∧
((frac_sgn f1 = 1) ⇒ P) ⇒
P
- FRAC_SGN_AINV
-
|- ∀f1. -frac_sgn (frac_ainv f1) = frac_sgn f1
- FRAC_AINV_ONEONE
-
|- ONE_ONE frac_ainv
- FRAC_AINV_ONTO
-
|- ONTO frac_ainv
- FRAC_NMR_SAVE
-
|- ∀a1 b1. frac_nmr (frac_save a1 b1) = a1
- FRAC_DNM_SAVE
-
|- ∀a1 b1. frac_dnm (frac_save a1 b1) = &b1 + 1
- FRAC_0_SAVE
-
|- frac_0 = frac_save 0 0
- FRAC_1_SAVE
-
|- frac_1 = frac_save 1 0
- FRAC_AINV_SAVE
-
|- ∀a1 b1. frac_ainv (frac_save a1 b1) = frac_save (-a1) b1
- FRAC_MINV_SAVE
-
|- ∀a1 b1.
a1 ≠ 0 ⇒
(frac_minv (frac_save a1 b1) =
frac_save (SGN a1 * (&b1 + 1)) (Num (ABS a1 − 1)))
- FRAC_ADD_SAVE
-
|- ∀a1 b1 a2 b2.
frac_add (frac_save a1 b1) (frac_save a2 b2) =
frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2)
- FRAC_MUL_SAVE
-
|- ∀a1 b1 a2 b2.
frac_mul (frac_save a1 b1) (frac_save a2 b2) =
frac_save (a1 * a2) (b1 * b2 + b1 + b2)