src/rational/ratScript.sml

39 val rat_equiv_def = Define `rat_equiv f1 f2 = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)`;
113   ``!f1 f2. rat_equiv f1 f2 = (rat_equiv f1 = rat_equiv f2)``,
265   ``!f1 f2. (abs_rat f1 = abs_rat f2) = rat_equiv f1 f2``,
289  *  |- !f1 f2. (abs_rat f1 = abs_rat f2)
290  *      = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
294 ``!f1 f2. (abs_rat f1 = abs_rat f2) =
295           (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)``,
563  *  |- !f1 f2. rat_add (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_add f1 f2 )
568   ���!f1 f2. rat_add (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_add f1 f2 )���,
573  *  |- !f1 f2. rat_sub (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_sub f1 f2 )
578   ���!f1 f2. rat_sub (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_sub f1 f2 )���,
583  *  |- !f1 f2. rat_mul (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_mul f1 f2 )
588   ���!f1 f2. rat_mul (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_mul f1 f2 )���,
593     |- !f1 f2.
594          frac_nmr f2 <> 0 ==>
595          (rat_div (abs_rat f1) (abs_rat f2) = abs_rat(frac_div f1 f2))
600   ���!f1 f2. frac_nmr f2 <> 0 ==>
601            (rat_div (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_div f1 f2 ))���,
606  *  |- !f1 f2. (abs_rat f1 = abs_rat f2) = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
611   ���!f1 f2. (abs_rat f1 = abs_rat f2) <=>
612            (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)���,
618     |- !f1 f2. (abs_rat f1 < abs_rat f2) =
619                (frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1)
624   ���!f1 f2. (abs_rat f1 < abs_rat f2) =
625            (frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1)���,
630     ���frac_dnm f2 * frac_dnm (abs_frac (~frac_nmr f1,frac_dnm f1))��� THEN
633   `~frac_nmr f1 * frac_dnm f2 = ~(frac_nmr f1 * frac_dnm f2)` by ARITH_TAC THEN
637   ``!f1 f2. (abs_rat f1 <= abs_rat f2) =
638     (frac_nmr f1 * frac_dnm f2 <= frac_nmr f2 * frac_dnm f1)``,