src/rational/fracScript.sml

62 val les_abs_def = Define`les_abs f1 f2 = frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1`;
65 val frac_add_def = Define `frac_add f1 f2 = abs_frac(frac_nmr f1 * frac_dnm f2 + frac_nmr f2 * frac_dnm f1, frac_dnm f1*frac_dnm f2)`;
66 val frac_sub_def = Define `frac_sub f1 f2 = frac_add f1 (frac_ainv f2)`;
67 val frac_mul_def = Define `frac_mul f1 f2 = abs_frac(frac_nmr f1 * frac_nmr f2, frac_dnm f1*frac_dnm f2)`;
68 val frac_div_def = Define `frac_div f1 f2 = frac_mul f1 (frac_minv f2)`;
107  *  |- !f1 f2. (f1=f2) = (frac_nmr f1 = frac_nmr f2) /\ (frac_dnm f1 = frac_dnm f2)
110 val FRAC_EQ_ALT = store_thm("FRAC_EQ_ALT", ``!f1 f2. (f1=f2) = (frac_nmr f1 = frac_nmr f2) /\ (frac_dnm f1 = frac_dnm f2)``,
560  *  |- ! f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2)
566  *  |- !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2)
569  *  |- !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2
584 val FRAC_AINV_ADD = store_thm( "FRAC_AINV_ADD", ``! f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2)``,
588         FRAC_POS_TAC ``frac_dnm f2`` THEN
589         FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN
594 val FRAC_AINV_SUB = store_thm("FRAC_AINV_SUB", ``!f1 f2. frac_ainv (frac_sub f2 f1) = frac_sub f1 f2``,
598         FRAC_POS_TAC ``frac_dnm f2`` THEN
599         FRAC_POS_TAC ``frac_dnm f2 * frac_dnm f1`` THEN
604 val FRAC_AINV_RMUL = store_thm("FRAC_AINV_RMUL", ``!f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2)``,
607         FRAC_POS_TAC ``frac_dnm f2`` THEN
608         FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN
617 val FRAC_AINV_LMUL = store_thm("FRAC_AINV_LMUL", ``!f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2``,
742  *  |- !f1 f2. frac_sub f1 f2 = frac_ainv (frac_sub f2 f1)
752  *  |- !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
755 val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2``,
758         FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN
759         REWRITE_TAC[UNDISCH_ALL (SPEC ``frac_dnm f1 * frac_dnm f2`` (SPEC ``frac_nmr f1 * frac_nmr f2`` NMR))] THEN
762         ASM_CASES_TAC ``frac_nmr f2=0i`` THEN
763         ASM_CASES_TAC ``frac_nmr f2 < 0i`` THEN
781  *  |- !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
785 val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL2", ``!f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2``,
793  *  |- !f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==>
794  *      (frac_sgn (frac_mul f1 f2) = i1 * i2)
798 (*val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==> (frac_sgn (frac_mul f1 f2) = i1 * i2)``,