1(*************************************************************************** 2 * 3 * Theory of fractions. 4 * 5 * Jens Brandt, November 2005 6 * 7 ***************************************************************************) 8 9open HolKernel boolLib Parse bossLib; 10 11(* interactive mode 12app load [ 13 "pairTheory", "jbUtils", "schneiderUtils", 14 "arithmeticTheory", "integerTheory", "intLib", "integerRingLib", "intSyntax", 15 "intExtensionTheory", "intExtensionLib", "fracUtils"]; 16*) 17 18open 19 pairTheory jbUtils schneiderUtils 20 arithmeticTheory integerTheory intLib integerRingLib intSyntax 21 intExtensionTheory intExtensionLib fracUtils; 22 23val _ = new_theory "frac"; 24 25val ERR = mk_HOL_ERR "fracScript" 26 27(*--------------------------------------------------------------------------* 28 * type definition 29 *--------------------------------------------------------------------------*) 30 31val frac_tyax = new_type_definition( "frac", 32 Q.prove(`?x. (\f:int#int. 0i<SND(f)) x`, 33 EXISTS_TAC ``(1i,1i)`` THEN 34 BETA_TAC THEN 35 REWRITE_TAC[SND] THEN 36 RW_TAC int_ss []) ); 37 38val frac_bij = save_thm("frac_bij", define_new_type_bijections{ 39 name="frac_tybij", 40 ABS="abs_frac", 41 REP="rep_frac", 42 tyax=frac_tyax } ); 43 44(*--------------------------------------------------------------------------* 45 * operations 46 *--------------------------------------------------------------------------*) 47 48(* numerator, denominator, sign of a fraction *) 49val frac_nmr_def = Define `frac_nmr f = FST(rep_frac f)`; 50val frac_dnm_def = Define `frac_dnm f = SND(rep_frac f)`; 51val frac_sgn_def = Define `frac_sgn f1 = SGN (frac_nmr f1)`; 52 53(* additive, multiplicative inverse of a fraction *) 54val frac_ainv_def = Define `frac_ainv f1 = abs_frac(~frac_nmr f1, frac_dnm f1)`; 55val frac_minv_def = Define `frac_minv f1 = abs_frac(frac_sgn f1 * frac_dnm f1, ABS(frac_nmr f1) )`; 56 57(* neutral elements *) 58val frac_0_def = Define `frac_0 = abs_frac(0i,1i)`; 59val frac_1_def = Define `frac_1 = abs_frac(1i,1i)`; 60 61(* less (absolute value) *) 62val les_abs_def = Define`les_abs f1 f2 = frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1`; 63 64(* basic arithmetics *) 65val 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)`; 66val frac_sub_def = Define `frac_sub f1 f2 = frac_add f1 (frac_ainv f2)`; 67val frac_mul_def = Define `frac_mul f1 f2 = abs_frac(frac_nmr f1 * frac_nmr f2, frac_dnm f1*frac_dnm f2)`; 68val frac_div_def = Define `frac_div f1 f2 = frac_mul f1 (frac_minv f2)`; 69 70(* frac_save terms are always defined (encode the definition of a fraction in the syntax) *) 71val frac_save_def = Define `frac_save (nmr:int) (dnm:num) = abs_frac(nmr,&dnm + 1)`; 72 73(*-------------------------------------------------------------------------- 74 * FRAC: thm 75 * |- !f. abs_frac (frac_nmr f,frac_dnm f) = f 76 *--------------------------------------------------------------------------*) 77 78val FRAC = store_thm("FRAC", ``!f. abs_frac (frac_nmr f,frac_dnm f) = f``, 79 STRIP_TAC THEN 80 REWRITE_TAC[frac_nmr_def,frac_dnm_def] 81 THEN RW_TAC int_ss [CONJUNCT1 frac_bij]); 82 83(*========================================================================== 84 * equivalence of fractions 85 *==========================================================================*) 86 87(*-------------------------------------------------------------------------- 88 * FRAC_EQ: thm 89 * |- !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==> 90 * ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) ) 91 *--------------------------------------------------------------------------*) 92 93val [abs_rep_frac, rep_abs_frac] = CONJUNCTS frac_bij ; 94val (raf_eqI, raf_eqD) = EQ_IMP_RULE (SPEC_ALL rep_abs_frac) ; 95 96val FRAC_EQ = store_thm("FRAC_EQ", 97 ``!a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==> 98 ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )``, 99 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL [ 100 POP_ASSUM (MP_TAC o AP_TERM ``rep_frac``) THEN 101 VALIDATE (CONV_TAC (DEPTH_CONV (REWR_CONV_A (UNDISCH raf_eqI)))), 102 ALL_TAC] THEN 103 ASM_SIMP_TAC std_ss []) ; 104 105(*-------------------------------------------------------------------------- 106 * FRAC_EQ_ALT : thm 107 * |- !f1 f2. (f1=f2) = (frac_nmr f1 = frac_nmr f2) /\ (frac_dnm f1 = frac_dnm f2) 108 *--------------------------------------------------------------------------*) 109 110val FRAC_EQ_ALT = store_thm("FRAC_EQ_ALT", ``!f1 f2. (f1=f2) = (frac_nmr f1 = frac_nmr f2) /\ (frac_dnm f1 = frac_dnm f2)``, 111 REPEAT GEN_TAC THEN 112 EQ_TAC THEN 113 STRIP_TAC THENL 114 [ 115 ALL_TAC 116 , 117 ONCE_REWRITE_TAC[GSYM FRAC] 118 ] THEN 119 ASM_REWRITE_TAC[] ); 120 121(*-------------------------------------------------------------------------- 122 * FRAC_NOT_EQ : thm 123 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> 124 * (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2)) 125 *--------------------------------------------------------------------------*) 126 127val 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))``, 128 REPEAT STRIP_TAC THEN 129 RW_TAC int_ss [] THEN 130 PROVE_TAC[FRAC_EQ] ); 131 132(*-------------------------------------------------------------------------- 133 * FRAC_NOT_EQ_IMP : thm 134 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> 135 * ~((a1,b1) = (a2,b2)) ==> ~(abs_frac (a1,b1) = abs_frac (a2,b2)) 136 *--------------------------------------------------------------------------*) 137 138(* following theorem (with longer proof) 139 was previously stored as "FRAC_NOT_EQ", must be an error JED 16.9.15 *) 140val FRAC_NOT_EQ_IMP = store_thm("FRAC_NOT_EQ_IMP", 141 ``!a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==> 142 ~((a1,b1) = (a2,b2)) ==> ~(abs_frac (a1,b1) = abs_frac (a2,b2))``, 143 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN 144 ASM_SIMP_TAC std_ss [FRAC_EQ]) ; 145 146 147(*-------------------------------------------------------------------------- 148 * FRAC_EQ_TAC : tactic 149 * 150 * A ?- abs_frac(a1,b1) = abs_frac(a2,b2) 151 * ========================================= FRAC_EQ_TAC 152 * A ?- a1=a2 | A ?- b1=b2 153 * 154 * simplified version - note, doesn't check that goal is of given form 155 *--------------------------------------------------------------------------*) 156 157val FRAC_EQ_TAC:tactic = fn (asm_list,goal) => 158 (AP_TERM_TAC THEN MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC]) (asm_list,goal) 159 handle HOL_ERR _ => raise ERR "FRAC_EQ_TAC" ""; 160 161(*========================================================================== 162 * some useful things about positive and non-zero 163 * numbers in the context of fractions 164 *==========================================================================*) 165 166(*-------------------------------------------------------------------------- 167 * FRAC_DNMPOS : thm 168 * |- !f. 0 < frac_dnm f 169 *--------------------------------------------------------------------------*) 170 171val FRAC_DNMPOS = store_thm("FRAC_DNMPOS",``!f. 0 < frac_dnm f``, 172 REWRITE_TAC[frac_dnm_def] THEN 173 RW_TAC int_ss [REWRITE_RULE [CONJUNCT1 frac_bij] (SPEC ``rep_frac(f)`` (BETA_RULE (ONCE_REWRITE_RULE [EQ_SYM_EQ] (CONJUNCT2 frac_bij)))) ]); 174 175(*-------------------------------------------------------------------------- 176 * frac_pos_conv : term list -> conv 177 *--------------------------------------------------------------------------*) 178 179fun frac_pos_conv (asm_list:term list) (t1:term) = 180 if (in_list asm_list ``0i < ^t1``) then 181 ASSUME ``0i < ^t1`` 182 else 183 if (is_comb t1) then 184 let 185 val (rator, rand) = dest_comb t1; 186 in 187 if (is_mult t1) then 188 let 189 val (fac1, fac2) = intSyntax.dest_mult t1; 190 val fac1_thm = frac_pos_conv asm_list fac1; 191 val fac2_thm = frac_pos_conv asm_list fac2; 192 in 193 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_MUL_POS_SIGN) 194 end 195 else if (rator=``frac_dnm``) then 196 SPEC rand FRAC_DNMPOS 197 else if (rator=``ABS``) andalso (in_list asm_list ``~(^rand = 0)``) then 198 UNDISCH (SPEC rand INT_ABS_NOT0POS) 199 else if (is_int_literal t1) then 200 EQT_ELIM (ARITH_CONV ``0 < ^t1``) 201 else 202 ASSUME ``0i < ^t1`` 203 end 204 else 205 ASSUME ``0i < ^t1``; 206 207(*-------------------------------------------------------------------------- 208 * frac_not0_conv : term list -> conv 209 *--------------------------------------------------------------------------*) 210 211fun frac_not0_conv (asm_list:term list) (t1:term) = 212 if (in_list asm_list ``~(^t1 = 0i)``) then 213 ASSUME ``~(^t1 = 0i)`` 214 else 215 if (is_comb t1) then 216 let 217 val (rator, rand) = dest_comb t1; 218 in 219 if (is_mult t1) then 220 let 221 val (fac1, fac2) = intSyntax.dest_mult t1; 222 val fac1_thm = frac_not0_conv asm_list fac1; 223 val fac2_thm = frac_not0_conv asm_list fac2; 224 in 225 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_NOT0_MUL) 226 end 227 else if (rator=``frac_dnm``) then 228 MP (SPEC t1 INT_GT0_IMP_NOT0) (SPEC rand FRAC_DNMPOS) 229 else if (rator=``SGN``) andalso (in_list asm_list ``~(^rand = 0)``) then 230 UNDISCH (SPEC rand INT_NOT0_SGNNOT0) 231 else if (is_int_literal t1) then 232 EQT_ELIM (ARITH_CONV ``~(^t1 = 0i)``) 233 else 234 ASSUME ``~(^t1 = 0i)`` 235 end 236 else 237 ASSUME ``~(^t1 = 0i)``; 238 239(*-------------------------------------------------------------------------- 240 * FRAC_POS_TAC : term -> tactic 241 *--------------------------------------------------------------------------*) 242 243fun FRAC_POS_TAC term1 (asm_list, goal) = 244 (ASSUME_TAC (frac_pos_conv asm_list term1)) (asm_list, goal); 245 246(*-------------------------------------------------------------------------- 247 * FRAC_NOT0_TAC : term -> tactic 248 *--------------------------------------------------------------------------*) 249 250fun FRAC_NOT0_TAC term1 (asm_list, goal) = 251 (ASSUME_TAC (frac_not0_conv asm_list term1)) (asm_list, goal); 252 253(*========================================================================== 254 * numerator and denominator extraction 255 *==========================================================================*) 256 257val FRAC_REP_ABS_SUBST = 258let 259 val lemma01 = prove( ``(\f. 0<SND f) (a1:int,b1:int) = (0<b1)``, BETA_TAC THEN REWRITE_TAC[SND]); 260 val lemma02 = fst(EQ_IMP_RULE (ONCE_REWRITE_RULE[EQ_SYM_EQ] (SPEC ``(a:int,b:int)`` (ONCE_REWRITE_RULE [EQ_SYM_EQ] (CONJUNCT2 frac_bij))))) 261in 262 UNDISCH(ONCE_REWRITE_RULE [lemma01] lemma02) 263end; 264 265(*-------------------------------------------------------------------------- 266 * NMR: thm 267 * |- !a b. 0 < b ==> (frac_nmr (abs_frac (a,b)) = a) 268 *--------------------------------------------------------------------------*) 269 270val NMR = store_thm("NMR", ``!a b. 0 < b ==> (frac_nmr (abs_frac (a,b)) = a)``, 271 REPEAT STRIP_TAC THEN 272 REWRITE_TAC[frac_nmr_def] THEN 273 REWRITE_TAC[FRAC_REP_ABS_SUBST] ); 274 275(*-------------------------------------------------------------------------- 276 * DNM: thm 277 * |- !a b. 0 < b ==> (frac_dnm (abs_frac (a,b)) = b) 278 *--------------------------------------------------------------------------*) 279 280val DNM = store_thm("DNM", ``!a b. 0 < b ==> (frac_dnm (abs_frac (a,b)) = b)``, 281 REPEAT STRIP_TAC THEN 282 REWRITE_TAC[frac_dnm_def] THEN 283 REWRITE_TAC[FRAC_REP_ABS_SUBST] ); 284 285(*-------------------------------------------------------------------------- 286 * FRAC_NMR_CONV: conv 287 * 288 * frac_nmr (abs_frac (a1,b1)) 289 * ----------------------------------------- 290 * 0 < b1 |- (frac_nmr (abs_frac (a1,b1)) = a1) 291 *--------------------------------------------------------------------------*) 292 293val FRAC_NMR_CONV:conv = fn term => 294let 295 val (nmr,f) = dest_comb term; 296 val (abs,args) = dest_comb f; 297 val (a,b) = dest_pair args; 298in 299 UNDISCH_ALL(SPEC b (SPEC a NMR)) 300end 301handle HOL_ERR _ => raise ERR "FRAC_NMR_CONV" ""; 302 303 304(*-------------------------------------------------------------------------- 305 * FRAC_DNM_CONV: conv 306 * 307 * frac_dnm (abs_frac (a1,b1)) 308 * ----------------------------------------- 309 * 0 < b1 |- (frac_dnm (abs_frac (a1,b1)) = a1) 310 *--------------------------------------------------------------------------*) 311 312val FRAC_DNM_CONV:conv = fn term => 313let 314 val (nmr,f) = dest_comb term; 315 val (abs,args) = dest_comb f; 316 val (a,b) = dest_pair args; 317in 318 UNDISCH_ALL(SPEC b (SPEC a DNM)) 319end 320handle HOL_ERR _ => raise ERR "FRAC_DNM_CONV" ""; 321 322(*-------------------------------------------------------------------------- 323 * frac_nmr_tac : term*term -> tactic 324 *--------------------------------------------------------------------------*) 325 326 fun frac_nmr_tac (asm_list:term list) (nmr,dnm) = 327 let 328 val asm_thm = frac_pos_conv asm_list dnm; 329 val sub_thm = DISCH_ALL (FRAC_NMR_CONV ``nmr( abs_frac (^nmr, ^dnm) )``); 330 in 331 TRY ( 332 SUBST1_TAC (MP sub_thm asm_thm) 333 ) 334 end; 335 336(*-------------------------------------------------------------------------- 337 * frac_dnm_tac : term*term -> tactic 338 *--------------------------------------------------------------------------*) 339 340fun frac_dnm_tac (asm_list:term list) (nmr,dnm) = 341 let 342 val asm_thm = frac_pos_conv asm_list dnm; 343 val sub_thm = DISCH_ALL (FRAC_DNM_CONV ``dnm( abs_frac (^nmr, ^dnm) )``); 344 in 345 TRY ( 346 SUBST1_TAC (MP sub_thm asm_thm) 347 ) 348 end; 349 350(*-------------------------------------------------------------------------- 351 * FRAC_NMRDNM_TAC : tactic 352 * 353 * simplify resp. nmr(abs_frac(a1,b1)) to a1 and frac_dnm(abs_frac(a1,b1)) to b1 354 *--------------------------------------------------------------------------*) 355 356fun FRAC_NMRDNM_TAC (asm_list, goal) = 357let 358 val term_list = extract_frac_fun [``frac_nmr``,``frac_dnm``] goal 359 val nmr_term_list = map (fn (rator,nmr,dnm) => (nmr,dnm)) 360 (filter (fn (a1,_,_) => a1=``frac_nmr``) term_list) 361 val dnm_term_list = map (fn (rator,nmr,dnm) => (nmr,dnm)) 362 (filter (fn (a1,_,_) => a1=``frac_dnm``) term_list) 363in 364 ( 365 MAP_EVERY (frac_nmr_tac asm_list) nmr_term_list THEN 366 MAP_EVERY (frac_dnm_tac asm_list) dnm_term_list THEN 367 SIMP_TAC int_ss [INT_MUL_LID, INT_MUL_RID, INT_MUL_LZERO, INT_MUL_RZERO] 368 ) (asm_list,goal) 369end 370handle HOL_ERR _ => raise ERR "FRAC_NMRDNM_TAC" ""; 371 372(*========================================================================== 373 * calculation 374 *==========================================================================*) 375 376(*-------------------------------------------------------------------------- 377 * FRAC_AINV_CALCULATE : thm 378 * |- !a1 b1. 0 < b1 ==> 379 * frac_ainv (abs_frac(a1,b1)) = abs_frac(~a1,b1) 380 *--------------------------------------------------------------------------*) 381 382val FRAC_AINV_CALCULATE = store_thm("FRAC_AINV_CALCULATE", ``!a1 b1. 0i<b1 ==> (frac_ainv (abs_frac(a1,b1)) = abs_frac(~a1,b1))``, 383 REPEAT STRIP_TAC THEN 384 REWRITE_TAC[frac_ainv_def] THEN 385 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``] THEN 386 RW_TAC int_ss [] ); 387 388(*-------------------------------------------------------------------------- 389 * FRAC_MINV_CALCULATE : thm 390 * |- !a1 b1. (0i < b1) ==> ~(a1 = 0i) ==> 391 * frac_minv (abs_frac(a1,b1)) = if 0 < a1 then abs_frac(b1,a1) else abs_frac(~b1, ~a1) ) 392 *--------------------------------------------------------------------------*) 393 394val FRAC_MINV_CALCULATE = store_thm("FRAC_MINV_CALCULATE", ``!a1 b1. (0i < b1) ==> ~(a1 = 0i) ==> (frac_minv (abs_frac(a1,b1)) = abs_frac(SGN(a1)*b1,ABS(a1)) )``, 395 REPEAT STRIP_TAC THEN 396 REWRITE_TAC[frac_minv_def, frac_sgn_def] THEN 397 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``] THEN 398 PROVE_TAC[] ); 399 400(*-------------------------------------------------------------------------- 401 * FRAC_SGN_CALCULATE : thm 402 * |- !a1 b1. (0 < b1) ==> 403 * (frac_sgn (abs_frac(a1,b1)) = SGN a1) 404 *--------------------------------------------------------------------------*) 405 406val FRAC_SGN_CALCULATE = store_thm("FRAC_SGN_CALCULATE", ``!a1 b1. (0i < b1) ==> (frac_sgn (abs_frac(a1,b1)) = SGN a1)``, 407 REPEAT STRIP_TAC THEN 408 REWRITE_TAC[frac_sgn_def] THEN 409 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``] THEN 410 RW_TAC int_ss []); 411 412(*-------------------------------------------------------------------------- 413 * FRAC_ADD_CALCULATE : thm 414 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> 415 * frac_add (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2+a2*b1 , b1*b2 ) 416 *--------------------------------------------------------------------------*) 417 418val 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 ))``, 419 REPEAT STRIP_TAC THEN 420 REWRITE_TAC[frac_add_def] THEN 421 SUBST_TAC[ 422 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``, 423 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN 424 RW_TAC int_ss [] ); 425 426(*-------------------------------------------------------------------------- 427 * FRAC_SUB_CALCULATE : thm 428 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> 429 * frac_sub (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2-a2*b1 , b1*b2 ) 430 *--------------------------------------------------------------------------*) 431 432val 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 ))``, 433 REPEAT STRIP_TAC THEN 434 REWRITE_TAC[frac_sub_def,frac_add_def,frac_ainv_def] THEN 435 SUBST_TAC[ 436 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``, 437 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN 438 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (~a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (~a2,b2))``] THEN 439 RW_TAC int_ss [INT_SUB_CALCULATE, INT_MUL_CALCULATE] ); 440 441(*-------------------------------------------------------------------------- 442 * FRAC_MULT_CALCULATE : thm 443 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> 444 * frac_mul (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*a2 , b1*b2 ) 445 *--------------------------------------------------------------------------*) 446 447val 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 ))``, 448 REPEAT STRIP_TAC THEN 449 REWRITE_TAC[frac_mul_def] THEN 450 SUBST_TAC[ 451 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``, 452 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN 453 RW_TAC int_ss [] ); 454 455(*-------------------------------------------------------------------------- 456 * FRAC_DIV_CALCULATE : thm 457 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> ~(a2 = 0) ==> 458 * frac_div (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*SGN(a2)*b2 , b1*ABS(a2) ) 459 *--------------------------------------------------------------------------*) 460 461val 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) ) )``, 462 REPEAT STRIP_TAC THEN 463 REWRITE_TAC[frac_div_def,frac_mul_def,frac_minv_def, frac_sgn_def] THEN 464 SUBST_TAC[ 465 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``, 466 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN 467 ASSUME_TAC (UNDISCH_ALL (SPEC ``a2:int`` INT_ABS_NOT0POS)) THEN 468 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 469 RW_TAC (int_ss ++ (simpLib.ac_ss [(INT_MUL_ASSOC, INT_MUL_COMM)])) [] ); 470 471(*========================================================================== 472 * basic theorems (associativity, commutativity, identity elements, ...) 473 *==========================================================================*) 474 475(*-------------------------------------------------------------------------- 476 * FRAC_ADD_ASSOC: thm 477 * |- !a b c. frac_add a (frac_add b c) = frac_add (frac_add a b) c 478 * 479 * FRAC_MULT_ASSOC: thm 480 * |- !a b c. frac_mul a (frac_mul b c) = frac_mul (frac_mul a b) c 481 *--------------------------------------------------------------------------*) 482 483val FRAC_ADD_ASSOC = store_thm("FRAC_ADD_ASSOC", ``!a b c. frac_add a (frac_add b c) = frac_add (frac_add a b) c``, 484 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_add_def] 485 THEN FRAC_POS_TAC ``frac_dnm a * frac_dnm b`` 486 THEN FRAC_POS_TAC ``frac_dnm b * frac_dnm c`` 487 THEN RW_TAC int_ss [NMR,DNM] 488 THEN FRAC_EQ_TAC THEN INT_RING_TAC ); 489 490val FRAC_MUL_ASSOC = store_thm("FRAC_MUL_ASSOC", ``!a b c. frac_mul a (frac_mul b c) = frac_mul (frac_mul a b) c``, 491 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_mul_def] 492 THEN FRAC_POS_TAC ``frac_dnm a * frac_dnm b`` 493 THEN FRAC_POS_TAC ``frac_dnm b * frac_dnm c`` 494 THEN RW_TAC int_ss [NMR,DNM] 495 THEN FRAC_EQ_TAC THEN INT_RING_TAC); 496 497(*-------------------------------------------------------------------------- 498 * FRAC_ADD_COMM: thm 499 * |- !a b c. frac_add a b = frac_add b a 500 * 501 * FRAC_MUL_COMM: thm 502 * |- !a b c. frac_mul a b = frac_mul b a 503 *--------------------------------------------------------------------------*) 504 505val FRAC_ADD_COMM = store_thm("FRAC_ADD_COMM",``!a b. frac_add a b = frac_add b a``, 506 REPEAT STRIP_TAC THEN 507 REWRITE_TAC[frac_add_def] 508 THEN FRAC_EQ_TAC 509 THEN INT_RING_TAC ); 510 511val FRAC_MUL_COMM = store_thm("FRAC_MUL_COMM",``!a b. frac_mul a b = frac_mul b a``, 512 REPEAT STRIP_TAC THEN 513 REWRITE_TAC[frac_mul_def] 514 THEN FRAC_EQ_TAC THEN 515 INT_RING_TAC ); 516 517(*-------------------------------------------------------------------------- 518 * FRAC_ADD_RID: thm 519 * |- !a. frac_add a frac_0 = a 520 * 521 * FRAC_MUL_RID: thm 522 * |- !a. frac_mul a frac_1 = a 523 *--------------------------------------------------------------------------*) 524 525val FRAC_ADD_RID = store_thm("FRAC_ADD_RID",``!a. frac_add a frac_0 = a``, 526 STRIP_TAC THEN 527 REWRITE_TAC[frac_add_def, frac_0_def] THEN 528 RW_TAC int_ss [NMR,DNM] THEN 529 RW_TAC int_ss [FRAC] ); 530 531val FRAC_MUL_RID = store_thm("FRAC_MUL_RID",``!a. frac_mul a frac_1 = a``, 532 STRIP_TAC THEN 533 REWRITE_TAC[frac_mul_def, frac_1_def] THEN 534 RW_TAC int_ss [NMR,DNM] THEN 535 RW_TAC int_ss [FRAC] ); 536 537(*-------------------------------------------------------------------------- 538 * FRAC_1_0: thm 539 * |- ~ (frac_1=frac_0) 540 *--------------------------------------------------------------------------*) 541 542val FRAC_1_0 = store_thm("FRAC_1_0", ``~ (frac_1=frac_0)``, 543 REWRITE_TAC[frac_0_def, frac_1_def] THEN 544 FRAC_POS_TAC ``1i`` THEN 545 MATCH_MP_TAC (UNDISCH (UNDISCH (SPEC ``1i`` (SPEC ``0i`` (SPEC ``1i`` (SPEC ``1i`` FRAC_NOT_EQ_IMP)))))) THEN 546 RW_TAC int_ss [] ); 547 548(*========================================================================== 549 * calculation rules of basic arithmetics 550 *==========================================================================*) 551 552(*-------------------------------------------------------------------------- 553 * FRAC_AINV_0: thm 554 * |- frac_ainv frac_0 = frac_0 555 * 556 * FRAC_AINV_AINV: thm 557 * |- !f1. frac_ainv (frac_ainv f1) = f1 558 * 559 * FRAC_AINV_ADD: thm 560 * |- ! f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2) 561 * 562 * FRAC_AINV_SUB: thm 563 * |- !a b. frac_sub a b = frac_ainv (frac_sub b a) 564 * 565 * FRAC_AINV_LMUL: thm 566 * |- !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2) 567 * 568 * FRAC_AINV_LMUL: thm 569 * |- !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2 570 *--------------------------------------------------------------------------*) 571 572val FRAC_AINV_0 = store_thm("FRAC_AINV_0", ``frac_ainv frac_0 = frac_0``, 573 REWRITE_TAC[frac_0_def,frac_ainv_def] THEN 574 FRAC_POS_TAC ``1i`` THEN 575 RW_TAC int_ss [NMR,DNM] THEN 576 RW_TAC int_ss [INT_NEG_0] ); 577 578val FRAC_AINV_AINV = store_thm("FRAC_AINV_AINV", ``!f1. frac_ainv (frac_ainv f1) = f1``, 579 GEN_TAC THEN 580 REWRITE_TAC[frac_ainv_def] THEN 581 FRAC_POS_TAC ``frac_dnm f1`` THEN 582 RW_TAC int_ss [NMR, DNM, INT_NEGNEG, FRAC] ); 583 584val FRAC_AINV_ADD = store_thm( "FRAC_AINV_ADD", ``! f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2)``, 585 REPEAT GEN_TAC THEN 586 REWRITE_TAC[frac_add_def, frac_ainv_def] THEN 587 FRAC_POS_TAC ``frac_dnm f1`` THEN 588 FRAC_POS_TAC ``frac_dnm f2`` THEN 589 FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN 590 RW_TAC int_ss [NMR,DNM] THEN 591 FRAC_EQ_TAC THENL 592 [INT_RING_TAC,RW_TAC int_ss []] ); 593 594val FRAC_AINV_SUB = store_thm("FRAC_AINV_SUB", ``!f1 f2. frac_ainv (frac_sub f2 f1) = frac_sub f1 f2``, 595 REPEAT GEN_TAC THEN 596 REWRITE_TAC[frac_ainv_def, frac_add_def, frac_sub_def] THEN 597 FRAC_POS_TAC ``frac_dnm f1`` THEN 598 FRAC_POS_TAC ``frac_dnm f2`` THEN 599 FRAC_POS_TAC ``frac_dnm f2 * frac_dnm f1`` THEN 600 RW_TAC int_ss [NMR,DNM] THEN 601 FRAC_EQ_TAC THEN 602 INT_RING_TAC ); 603 604val FRAC_AINV_RMUL = store_thm("FRAC_AINV_RMUL", ``!f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2)``, 605 REPEAT GEN_TAC THEN 606 REWRITE_TAC[frac_mul_def, frac_ainv_def] THEN 607 FRAC_POS_TAC ``frac_dnm f2`` THEN 608 FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN 609 RW_TAC int_ss [NMR,DNM] THEN 610 FRAC_EQ_TAC THENL 611 [ 612 integerRingLib.INT_RING_TAC 613 , 614 PROVE_TAC[] 615 ] ); 616 617val FRAC_AINV_LMUL = store_thm("FRAC_AINV_LMUL", ``!f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2``, 618 PROVE_TAC[FRAC_MUL_COMM, FRAC_AINV_RMUL] ); 619 620(*-------------------------------------------------------------------------- 621 * FRAC_MINV_1: thm 622 * |- frac_minv frac_1 = frac_1 623 *--------------------------------------------------------------------------*) 624 625val FRAC_MINV_1 = Q.store_thm ("FRAC_MINV_1", `frac_minv frac_1 = frac_1`, 626 SIMP_TAC intLib.int_ss 627 [FRAC_MINV_CALCULATE, intExtensionTheory.SGN_def, frac_1_def]) ; 628 629(*-------------------------------------------------------------------------- 630 * FRAC_SUB_ADD: thm 631 * |- !a b c. frac_sub a (frac_add b c) = frac_sub (frac_sub a b) c 632 * 633 * FRAC_SUB_SUB: thm 634 * |- !a b c. frac_sub a (frac_sub b c) = frac_add (frac_sub a b) c 635 *--------------------------------------------------------------------------*) 636 637val FRAC_SUB_ADD = store_thm("FRAC_SUB_ADD", ``!a b c. frac_sub a (frac_add b c) = frac_sub (frac_sub a b) c``, 638 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_add_def,frac_sub_def,frac_ainv_def] THEN 639 FRAC_POS_TAC ``frac_dnm a * frac_dnm b`` THEN 640 FRAC_POS_TAC ``frac_dnm b * frac_dnm c`` THEN 641 FRAC_POS_TAC ``frac_dnm b`` THEN 642 FRAC_POS_TAC ``frac_dnm c`` THEN 643 RW_TAC int_ss [NMR,DNM] THEN 644 FRAC_EQ_TAC THEN 645 INT_RING_TAC ); 646 647val FRAC_SUB_SUB = store_thm("FRAC_SUB_SUB", ``!a b c. frac_sub a (frac_sub b c) = frac_add (frac_sub a b) c``, 648 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_add_def,frac_sub_def,frac_ainv_def] THEN 649 FRAC_POS_TAC ``frac_dnm a * frac_dnm b`` THEN 650 FRAC_POS_TAC ``frac_dnm b * frac_dnm c`` THEN 651 FRAC_POS_TAC ``frac_dnm b`` THEN 652 FRAC_POS_TAC ``frac_dnm c`` THEN 653 RW_TAC int_ss [NMR,DNM] THEN 654 FRAC_EQ_TAC THEN 655 INT_RING_TAC ); 656 657(*========================================================================== 658 * signum, absolute value 659 *==========================================================================*) 660 661(*-------------------------------------------------------------------------- 662 * FRAC_SGN_TOTAL: thm 663 * |- !f. (frac_sgn f1 = ~1) \/ (frac_sgn f1 = 0) \/ (frac_sgn f1 = 1) 664 *--------------------------------------------------------------------------*) 665 666val FRAC_SGN_TOTAL = store_thm("FRAC_SGN_TOTAL", ``!f1. (frac_sgn f1 = ~1) \/ (frac_sgn f1 = 0) \/ (frac_sgn f1 = 1)``, 667 REPEAT GEN_TAC THEN 668 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 669 ASM_CASES_TAC ``frac_nmr f1 = 0`` THENL 670 [ 671 PROVE_TAC[] 672 , 673 ASM_CASES_TAC ``frac_nmr f1 < 0`` THEN 674 PROVE_TAC[] 675 ] ); 676 677(*-------------------------------------------------------------------------- 678 * FRAC_SGN_POS: thm 679 * |- !f1. (frac_sgn f1 = 1) = 0 < nmr f1 680 *--------------------------------------------------------------------------*) 681 682val FRAC_SGN_POS = store_thm("FRAC_SGN_POS", ``!f1. (frac_sgn f1 = 1) = 0 < frac_nmr f1``, 683 GEN_TAC THEN 684 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 685 RW_TAC int_ss [] THENL 686 [ 687 PROVE_TAC[INT_LT_GT] 688 , 689 PROVE_TAC[INT_LT_TOTAL] 690 ] ); 691 692(*-------------------------------------------------------------------------- 693 * FRAC_SGN_NOT_NEG: thm 694 * |- !f1. ~(frac_sgn f1 = ~1) = (0 = frac_nmr f1) \/ (0 < frac_nmr f1) 695 *--------------------------------------------------------------------------*) 696 697val FRAC_SGN_NOT_NEG = store_thm("FRAC_SGN_NOT_NEG", ``!f1. ~(frac_sgn f1 = ~1) = (0 = frac_nmr f1) \/ (0 < frac_nmr f1)``, 698 GEN_TAC THEN 699 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 700 RW_TAC int_ss [] THENL 701 [ 702 PROVE_TAC[INT_LT_GT] 703 , 704 PROVE_TAC[INT_LT_TOTAL] 705 ] ); 706 707(*-------------------------------------------------------------------------- 708 * FRAC_SGN_NEG: thm 709 * |- ! f. ~frac_sgn (frac_ainv f) = frac_sgn f 710 *--------------------------------------------------------------------------*) 711 712val FRAC_SGN_NEG = store_thm("FRAC_SGN_NEG", ``! f. ~frac_sgn (frac_ainv f) = frac_sgn f``, 713 GEN_TAC THEN 714 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 715 REWRITE_TAC[frac_ainv_def] THEN 716 ONCE_REWRITE_TAC[GSYM FRAC] THEN 717 FRAC_POS_TAC ``frac_dnm f`` THEN 718 RW_TAC int_ss [NMR,DNM] THEN 719 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 720 SUBST_TAC[UNDISCH_ALL (SPEC ``frac_dnm f`` (SPEC ``frac_nmr f`` NMR))] THEN 721 COND_CASES_TAC THENL 722 [ 723 ASM_REWRITE_TAC[] THEN 724 SUBST_TAC[UNDISCH_ALL (SPEC ``frac_dnm f`` (SPEC ``~0`` NMR))] THEN 725 PROVE_TAC[INT_NEG_0] 726 , 727 SUBST_TAC[UNDISCH_ALL (SPEC ``frac_dnm f`` (SPEC ``~frac_nmr f`` NMR))] THEN 728 REWRITE_TAC[INT_NEG_EQ,INT_NEG_LT0,INT_NEG_0] THEN 729 COND_CASES_TAC THENL 730 [ 731 ASSUME_TAC (UNDISCH (SPEC ``0i`` (SPEC ``frac_nmr f`` INT_LT_GT))) THEN 732 PROVE_TAC[] 733 , 734 ASSUME_TAC (SPEC ``frac_nmr f`` INT_NOTGT_IMP_EQLT) THEN 735 UNDISCH_TAC ``~(frac_nmr f < 0) = (0 = frac_nmr f) \/ 0 < frac_nmr f`` THEN 736 RW_TAC int_ss [] 737 ] 738 ] ); 739 740(*-------------------------------------------------------------------------- 741 * FRAC_SGN_IMP_EQGT: thm 742 * |- !f1 f2. frac_sub f1 f2 = frac_ainv (frac_sub f2 f1) 743 *--------------------------------------------------------------------------*) 744 745val FRAC_SGN_IMP_EQGT = store_thm("FRAC_SGN_IMP_EQGT",``!f1. ~(frac_sgn f1 = ~1) = (frac_sgn f1 = 0i) \/ (frac_sgn f1 = 1i)``, 746 GEN_TAC THEN 747 ASSUME_TAC (SPEC_ALL FRAC_SGN_TOTAL) THEN 748 REPEAT (RW_TAC int_ss []) ); 749 750(*-------------------------------------------------------------------------- 751 * FRAC_SGN_MUL: thm 752 * |- !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2 753 *--------------------------------------------------------------------------*) 754 755val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL", ``!f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2``, 756 REPEAT GEN_TAC THEN 757 REWRITE_TAC[frac_mul_def, frac_sgn_def, SGN_def] THEN 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 760 ASM_CASES_TAC ``frac_nmr f1=0i`` THEN 761 ASM_CASES_TAC ``frac_nmr f1 < 0i`` THEN 762 ASM_CASES_TAC ``frac_nmr f2=0i`` THEN 763 ASM_CASES_TAC ``frac_nmr f2 < 0i`` THEN 764 RW_TAC int_ss [INT_MUL_LZERO, INT_MUL_RZERO] THEN 765 PROVE_TAC[INT_NO_ZERODIV,INT_MUL_SIGN_CASES,INT_LT_GT,INT_LT_TOTAL] ); 766 767 768(*-------------------------------------------------------------------------- 769 * FRAC_ABS_SGN : thm 770 * |- !f1. ~(frac_nmr f1 = 0i) ==> (ABS (frac_sgn f1) = 1) 771 *--------------------------------------------------------------------------*) 772 773val FRAC_ABS_SGN = store_thm("FRAC_ABS_SGN", ``!f1. ~(frac_nmr f1 = 0i) ==> (ABS (frac_sgn f1) = 1i)``, 774 GEN_TAC THEN 775 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 776 RW_TAC int_ss [] THEN 777 RW_TAC int_ss [INT_ABS] ); 778 779(*-------------------------------------------------------------------------- 780 * FRAC_SGN_MUL : thm 781 * |- !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2 782 * TODO: was FRAC_SGN_MUL2 783 *--------------------------------------------------------------------------*) 784 785val FRAC_SGN_MUL = store_thm("FRAC_SGN_MUL2", ``!f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2``, 786 REPEAT GEN_TAC THEN 787 REWRITE_TAC[frac_sgn_def, frac_mul_def] THEN 788 FRAC_NMRDNM_TAC THEN 789 PROVE_TAC[INT_SGN_MUL2] ); 790 791(*-------------------------------------------------------------------------- 792 * FRAC_SGN_MUL : thm 793 * |- !f1 f2 i1 i2. (frac_sgn f1 = i1) ==> (frac_sgn f2 = i2) ==> 794 * (frac_sgn (frac_mul f1 f2) = i1 * i2) 795 * deleted 796 *--------------------------------------------------------------------------*) 797 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)``, 799 REPEAT GEN_TAC THEN 800 REWRITE_TAC[frac_sgn_def] THEN 801 FRAC_CALC_TAC THEN 802 FRAC_NMRDNM_TAC THEN 803 PROVE_TAC[INT_SGN_MUL] );*) 804 805(*-------------------------------------------------------------------------- 806 * FRAC_SGN_CASES : thm 807 * |- !f1 P. 808 * ((frac_sgn f1 = ~1) ==> P) /\ 809 * ((frac_sgn f1 = 0i) ==> P) /\ 810 * ((frac_sgn f1 = 1i) ==> P) ==> P 811 *--------------------------------------------------------------------------*) 812 813val FRAC_SGN_CASES = store_thm("FRAC_SGN_CASES", ``!f1 P. ((frac_sgn f1 = ~1) ==> P) /\ ((frac_sgn f1 = 0i) ==> P) /\ ((frac_sgn f1 = 1i) ==> P) ==> P``, 814 REPEAT GEN_TAC THEN 815 ASM_CASES_TAC ``frac_sgn f1 = ~1`` THEN 816 ASM_CASES_TAC ``frac_sgn f1 = 0i`` THEN 817 ASM_CASES_TAC ``frac_sgn f1 = 1i`` THEN 818 UNDISCH_ALL_TAC THEN 819 PROVE_TAC[FRAC_SGN_TOTAL] ); 820 821(*-------------------------------------------------------------------------- 822 * FRAC_SGN_AINV : thm 823 * |- !f1. ~frac_sgn (frac_ainv f1) = frac_sgn f1 824 *--------------------------------------------------------------------------*) 825 826val FRAC_SGN_AINV = store_thm("FRAC_SGN_AINV", ``!f1. ~frac_sgn (frac_ainv f1) = frac_sgn f1``, 827 GEN_TAC THEN 828 REWRITE_TAC[frac_sgn_def, frac_ainv_def] THEN 829 FRAC_NMRDNM_TAC THEN 830 REWRITE_TAC[SGN_def] THEN 831 REWRITE_TAC[INT_NEG_EQ, INT_NEG_0] THEN 832 SUBGOAL_THEN ``(~frac_nmr f1 < 0) = (0 < frac_nmr f1)`` SUBST1_TAC THENL 833 [ 834 EQ_TAC THEN 835 STRIP_TAC THEN 836 ONCE_REWRITE_TAC[GSYM INT_LT_NEG] THEN 837 PROVE_TAC[INT_NEG_0, INT_NEGNEG] 838 , 839 RW_TAC int_ss [] THEN 840 PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL] 841 ] ); 842 843 844 845(*========================================================================== 846 * one-to-one and onto theorems 847 *==========================================================================*) 848 849(*-------------------------------------------------------------------------- 850 * FRAC_AINV_ONE_ONE : thm 851 * |- ONE_ONE frac_ainv 852 *--------------------------------------------------------------------------*) 853 854val FRAC_AINV_ONEONE = store_thm("FRAC_AINV_ONEONE", ``ONE_ONE frac_ainv``, 855 REWRITE_TAC[ONE_ONE_DEF] THEN 856 BETA_TAC THEN 857 REPEAT GEN_TAC THEN 858 REWRITE_TAC[frac_ainv_def] THEN 859 FRAC_POS_TAC ``frac_dnm x1`` THEN 860 FRAC_POS_TAC ``frac_dnm x2`` THEN 861 REWRITE_TAC[UNDISCH_ALL (SPECL[``~frac_nmr x1``,``frac_dnm x1``,``~frac_nmr x2``,``frac_dnm x2``] FRAC_EQ)] THEN 862 REWRITE_TAC[INT_EQ_NEG] THEN 863 SUBST_TAC[SPEC ``x1:frac`` (GSYM FRAC), SPEC ``x2:frac`` (GSYM FRAC)] THEN 864 RW_TAC bool_ss [NMR,DNM] ); 865 866(*-------------------------------------------------------------------------- 867 * FRAC_AINV_ONTO : thm 868 * |- ONTO frac_ainv 869 *--------------------------------------------------------------------------*) 870 871val FRAC_AINV_ONTO = store_thm("FRAC_AINV_ONTO", ``ONTO frac_ainv``, 872 REWRITE_TAC[ONTO_DEF] THEN 873 BETA_TAC THEN 874 GEN_TAC THEN 875 EXISTS_TAC ``frac_ainv y`` THEN 876 PROVE_TAC[FRAC_AINV_AINV] ); 877 878 879 880(*========================================================================== 881 * encode whether a fraction is defined or not in the syntax 882 *==========================================================================*) 883 884 885(*========================================================================== 886 * compute the numerator and denominator of a fraction 887 *==========================================================================*) 888 889(*-------------------------------------------------------------------------- 890 * FRAC_NMR_SAVE: thm 891 * |- !a1 b1. frac_nmr( frac_save a1 b1 ) = a1 892 * 893 * FRAC_DNM_SAVE: thm 894 * |- !a1 b1. frac_dnm( frac_save a1 b1 ) = &b1 + 1i 895 *--------------------------------------------------------------------------*) 896 897val FRAC_NMR_SAVE = store_thm("FRAC_NMR_SAVE", ``!a1 b1. frac_nmr( frac_save a1 b1 ) = a1``, 898 REPEAT GEN_TAC THEN 899 REWRITE_TAC[frac_save_def] THEN 900 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 901 PROVE_TAC[NMR] ); 902 903val FRAC_DNM_SAVE = store_thm("FRAC_DNM_SAVE", ``!a1 b1. frac_dnm( frac_save a1 b1 ) = &b1 + 1i``, 904 REPEAT GEN_TAC THEN 905 REWRITE_TAC[frac_save_def] THEN 906 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 907 PROVE_TAC[DNM] ); 908 909(*-------------------------------------------------------------------------- 910 * FRAC_0_SAVE: thm 911 * |- frac_0 = frac_save 0 0 912 * 913 * FRAC_1_SAVE: thm 914 * |- frac_1 = frac_save 1 0 915 *--------------------------------------------------------------------------*) 916 917val FRAC_0_SAVE = store_thm("FRAC_0_SAVE", ``frac_0 = frac_save 0 0``, 918 REPEAT GEN_TAC THEN 919 REWRITE_TAC[frac_0_def, frac_save_def] THEN 920 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 921 FRAC_EQ_TAC THEN 922 ARITH_TAC ); 923 924val FRAC_1_SAVE = store_thm("FRAC_1_SAVE", ``frac_1 = frac_save 1 0``, 925 REPEAT GEN_TAC THEN 926 REWRITE_TAC[frac_1_def, frac_save_def] THEN 927 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 928 FRAC_EQ_TAC THEN 929 ARITH_TAC ); 930 931(*-------------------------------------------------------------------------- 932 * FRAC_AINV_SAVE: thm 933 * |- !a1 b1. frac_ainv (frac_save a1 b1) = frac_save (~a1) b1 934 * 935 * RAT_MINV_SAVE: thm 936 * |- !a1 b1. ~(abs_rat (frac_save a1 b1) = rat_0) ==> 937 * (rat_minv (abs_rat (frac_save a1 b1)) = 938 * abs_rat( frac_save (SGN a1 * (& b1 + 1)) (Num (ABS a1 - 1))) ) 939 *--------------------------------------------------------------------------*) 940 941val FRAC_AINV_SAVE = store_thm("FRAC_AINV_SAVE", ``!a1 b1. frac_ainv (frac_save a1 b1) = frac_save (~a1) b1``, 942 REPEAT GEN_TAC THEN 943 REWRITE_TAC[frac_ainv_def, frac_save_def] THEN 944 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 945 FRAC_NMRDNM_TAC THEN 946 FRAC_EQ_TAC ); 947 948 949val FRAC_MINV_SAVE = store_thm("FRAC_MINV_SAVE",``!a1 b1. ~(a1=0) ==> (frac_minv (frac_save a1 b1) = frac_save (SGN a1 * (&b1 + 1)) (Num (ABS a1 - 1)))``, 950 REPEAT STRIP_TAC THEN 951 REWRITE_TAC[frac_minv_def, frac_sgn_def, frac_save_def] THEN 952 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 953 ASSUME_TAC (ARITH_PROVE ``0i < & (Num (ABS a1 - 1)) + 1``) THEN 954 FRAC_NMRDNM_TAC THEN 955 FRAC_EQ_TAC THEN 956 RW_TAC int_ss [SGN_def, GSYM INT_EQ_SUB_RADD] THEN 957 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 958 REWRITE_TAC[INT_OF_NUM] THEN 959 ARITH_TAC ); 960 961 962(*-------------------------------------------------------------------------- 963 * FRAC_ADD_SAVE: thm 964 * |- !a1 b1 a2 b2. 965 * frac_add (frac_save a1 b1) (frac_save a2 b2) = 966 * frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2) 967 * 968 * FRAC_MUL_SAVE: thm 969 * |- !a1 b1 a2 b2. 970 * frac_mul (frac_save a1 b1) (frac_save a2 b2) = 971 * frac_save (a1 * a2) (b1 * b2 + b1 + b2) 972 *--------------------------------------------------------------------------*) 973 974val FRAC_ADD_SAVE = store_thm( 975 "FRAC_ADD_SAVE", 976 ``!a1 b1 a2 b2. 977 frac_add (frac_save a1 b1) (frac_save a2 b2) = 978 frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2)``, 979 REPEAT GEN_TAC THEN 980 REWRITE_TAC[frac_add_def, frac_save_def] THEN 981 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 982 ASSUME_TAC (ARITH_PROVE ``0i < &b2 + 1``) THEN 983 FRAC_NMRDNM_TAC THEN 984 FRAC_EQ_TAC THEN 985 SIMP_TAC (srw_ss()) [INT_LDISTRIB, INT_RDISTRIB, GSYM INT_ADD, 986 AC INT_ADD_COMM INT_ADD_ASSOC]); 987 988val FRAC_MUL_SAVE = store_thm( 989 "FRAC_MUL_SAVE", 990 ``!a1 b1 a2 b2. frac_mul (frac_save a1 b1) (frac_save a2 b2) = 991 frac_save (a1 * a2) (b1 * b2 + b1 + b2)``, 992 REPEAT GEN_TAC THEN 993 REWRITE_TAC[frac_mul_def, frac_save_def] THEN 994 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN 995 ASSUME_TAC (ARITH_PROVE ``0i < &b2 + 1``) THEN 996 FRAC_NMRDNM_TAC THEN 997 FRAC_EQ_TAC THEN 998 REWRITE_TAC[INT_ADD_CALCULATE, INT_MUL_CALCULATE, INT_EQ_CALCULATE] THEN 999 RW_TAC arith_ss [arithmeticTheory.LEFT_ADD_DISTRIB, 1000 arithmeticTheory.RIGHT_ADD_DISTRIB] THEN 1001 ARITH_TAC); 1002 1003(*========================================================================== 1004 * end of theory 1005 *==========================================================================*) 1006 1007val _ = export_theory(); 1008