src/rational/fracScript.sml

91  *  |- !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==>
92  *     ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )
99   ``!a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==>
100     ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )``,
125  *  |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
126  *      (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2))
129 val FRAC_NOT_EQ = store_thm("FRAC_NOT_EQ", ``!a1 b1 a2 b2. 0i<b1 ==> 0i<b2 ==> (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2))``,
136  *  |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
137  *     ~((a1,b1) = (a2,b2)) ==> ~(abs_frac (a1,b1) = abs_frac (a2,b2))
143   ``!a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==>
144     ~((a1,b1) = (a2,b2)) ==> ~(abs_frac (a1,b1) = abs_frac (a2,b2))``,
152  *     A ?- abs_frac(a1,b1) = abs_frac(a2,b2)
154  *     A ?- a1=a2 | A ?- b1=b2
408  *  |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
409  *      frac_add (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2+a2*b1 , b1*b2 )
412 val FRAC_ADD_CALCULATE = store_thm("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 ))``,
417                 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
422  *  |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
423  *      frac_sub (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2-a2*b1 , b1*b2 )
426 val FRAC_SUB_CALCULATE = store_thm("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 ))``,
431                 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
432         SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (~a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (~a2,b2))``] THEN
437  *  |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
438  *      frac_mul (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*a2 , b1*b2 )
441 val FRAC_MULT_CALCULATE = store_thm("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 ))``,
446                 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
451  *  |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> ~(a2 = 0) ==>
452  *      frac_div (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*SGN(a2)*b2 , b1*ABS(a2) )
455 val FRAC_DIV_CALCULATE = store_thm("FRAC_DIV_CALCULATE", ``!a1 b1 a2 b2. 0i<b1 ==> 0i<b2 ==> ~(a2=0i) ==> (frac_div (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*SGN(a2)*b2 , b1*ABS(a2) ) )``,
460                 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
462         SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (SGN a2 * b2,ABS a2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (SGN a2 * b2,ABS a2))``] THEN
958  *  |- !a1 b1 a2 b2.
959  *      frac_add (frac_save a1 b1) (frac_save a2 b2) =
960  *      frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2)
963  *  |- !a1 b1 a2 b2.
964  *      frac_mul (frac_save a1 b1) (frac_save a2 b2) =
965  *      frac_save (a1 * a2) (b1 * b2 + b1 + b2)
970   ``!a1 b1 a2 b2.
971          frac_add (frac_save a1 b1) (frac_save a2 b2) =
972          frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2)``,
976   ASSUME_TAC (ARITH_PROVE ``0i < &b2 + 1``) THEN
984   ``!a1 b1 a2 b2. frac_mul (frac_save a1 b1) (frac_save a2 b2) =
985                   frac_save (a1 * a2) (b1 * b2 + b1 + b2)``,
989   ASSUME_TAC (ARITH_PROVE ``0i < &b2 + 1``) THEN