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