Theory "frac"

Parents intExtension

Signature

Type	Arity
frac	0
Constant	Type
rep_frac	:frac -> int # int
les_abs	:frac -> frac -> bool
frac_sub	:frac -> frac -> frac
frac_sgn	:frac -> int
frac_save	:int -> num -> frac
frac_nmr	:frac -> int
frac_mul	:frac -> frac -> frac
frac_minv	:frac -> frac
frac_dnm	:frac -> int
frac_div	:frac -> frac -> frac
frac_ainv	:frac -> frac
frac_add	:frac -> frac -> frac
frac_1	:frac
frac_0	:frac
abs_frac	:int # int -> frac

Definitions

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)

Theorems

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)