1(*************************************************************************** 2 * 3 * Theory of rational numbers. 4 * 5 * Jens Brandt, November 2005 6 * 7 ***************************************************************************) 8 9open HolKernel boolLib Parse BasicProvers bossLib; 10 11(* interactive mode 12app load [ 13 "integerTheory", "intLib", 14 "intExtensionTheory", "intExtensionLib", 15 "ringLib", "integerRingLib", 16 "fracTheory", "fracLib", "ratUtils", "jbUtils", 17 "quotient", "schneiderUtils"]; 18*) 19 20open 21 arithmeticTheory 22 integerTheory intLib 23 intExtensionTheory intExtensionLib 24 ringLib integerRingLib 25 fracTheory fracLib ratUtils jbUtils 26 quotient schneiderUtils; 27 28val arith_ss = old_arith_ss 29 30val _ = new_theory "rat"; 31val _ = ParseExtras.temp_loose_equality() 32 33val ERR = mk_HOL_ERR "ratScript" 34 35(*--------------------------------------------------------------------------* 36 * rat_equiv: definition and proof of equivalence relation 37 *--------------------------------------------------------------------------*) 38 39(* definition of equivalence relation *) 40val rat_equiv_def = Define `rat_equiv f1 f2 = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)`; 41 42(* RAT_EQUIV_REF: |- !a:frac. rat_equiv a a *) 43val RAT_EQUIV_REF = store_thm("RAT_EQUIV_REF", ``!a:frac. rat_equiv a a``, 44 STRIP_TAC THEN 45 REWRITE_TAC[rat_equiv_def] ); 46 47(* RAT_EQUIV_SYM: |- !a b. rat_equiv a b = rat_equiv b a *) 48val RAT_EQUIV_SYM = store_thm("RAT_EQUIV_SYM", 49 ``!a b. rat_equiv a b = rat_equiv b a``, 50 REPEAT STRIP_TAC THEN 51 REWRITE_TAC[rat_equiv_def] THEN 52 MATCH_ACCEPT_TAC EQ_SYM_EQ) ; 53 54val INT_ENTIRE' = CONV_RULE (ONCE_DEPTH_CONV (LHS_CONV SYM_CONV)) INT_ENTIRE ; 55val FRAC_DNMNZ = GSYM (MATCH_MP INT_LT_IMP_NE (SPEC_ALL FRAC_DNMPOS)) ; 56val FRAC_DNMNN = let val th = MATCH_MP INT_LT_IMP_LE (SPEC_ALL FRAC_DNMPOS) 57 in MATCH_MP (snd (EQ_IMP_RULE (SPEC_ALL INT_NOT_LT))) th end ; 58fun ifcan f x = f x handle _ => x ; 59 60val RAT_EQUIV_NMR_Z_IFF = store_thm ("RAT_EQUIV_NMR_Z_IFF", 61 ``!a b. rat_equiv a b ==> ((frac_nmr a = 0) = (frac_nmr b = 0))``, 62 REWRITE_TAC[rat_equiv_def] THEN 63 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN 64 FULL_SIMP_TAC std_ss [INT_MUL_LZERO, INT_MUL_RZERO, 65 INT_ENTIRE, INT_ENTIRE', FRAC_DNMNZ]) ; 66 67val RAT_EQUIV_NMR_GTZ_IFF = store_thm ("RAT_EQUIV_NMR_GTZ_IFF", 68 ``!a b. rat_equiv a b ==> ((frac_nmr a > 0) = (frac_nmr b > 0))``, 69 REWRITE_TAC[rat_equiv_def] THEN 70 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN 71 RULE_ASSUM_TAC (ifcan (AP_TERM ``int_lt 0i``)) THEN 72 FULL_SIMP_TAC std_ss [int_gt, INT_MUL_SIGN_CASES, FRAC_DNMPOS, FRAC_DNMNN ]) ; 73 74val RAT_EQUIV_NMR_LTZ_IFF = store_thm ("RAT_EQUIV_NMR_LTZ_IFF", 75 ``!a b. rat_equiv a b ==> ((frac_nmr a < 0) = (frac_nmr b < 0))``, 76 REWRITE_TAC[rat_equiv_def] THEN 77 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN 78 RULE_ASSUM_TAC (ifcan (AP_TERM ``int_gt 0i``)) THEN 79 FULL_SIMP_TAC std_ss [int_gt, INT_MUL_SIGN_CASES, FRAC_DNMPOS, FRAC_DNMNN ]) ; 80 81val RAT_NMR_Z_IFF_EQUIV = store_thm ("RAT_NMR_Z_IFF_EQUIV", 82 ``!a b. (frac_nmr a = 0) ==> (rat_equiv a b = (frac_nmr b = 0))``, 83 REWRITE_TAC[rat_equiv_def] THEN 84 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN 85 REV_FULL_SIMP_TAC std_ss [INT_MUL_LZERO, INT_MUL_RZERO, 86 INT_ENTIRE, INT_ENTIRE', FRAC_DNMNZ]) ; 87 88val times_dnmb = MATCH_MP INT_EQ_RMUL_EXP (Q.SPEC `b` FRAC_DNMPOS) ; 89 90val box_equals = prove (``(a = b) ==> (c = a) /\ (d = b) ==> (c = d)``, 91 REPEAT STRIP_TAC THEN BasicProvers.VAR_EQ_TAC THEN ASM_SIMP_TAC bool_ss []) ; 92 93val RAT_EQUIV_TRANS = store_thm("RAT_EQUIV_TRANS", 94 ``!a b c. rat_equiv a b /\ rat_equiv b c ==> rat_equiv a c``, 95 REPEAT GEN_TAC THEN Cases_on `frac_nmr b = 0` 96 THENL [ STRIP_TAC THEN 97 RULE_ASSUM_TAC (ifcan (MATCH_MP RAT_EQUIV_NMR_Z_IFF)) THEN 98 FULL_SIMP_TAC std_ss [RAT_NMR_Z_IFF_EQUIV], 99 REWRITE_TAC[rat_equiv_def] THEN STRIP_TAC THEN 100 ONCE_REWRITE_TAC [times_dnmb] THEN 101 FIRST_X_ASSUM (fn th => ONCE_REWRITE_TAC [MATCH_MP INT_EQ_LMUL2 th]) THEN 102 POP_ASSUM_LIST (fn [thbc, thab] => ASSUME_TAC 103 (MK_COMB (AP_TERM ``int_mul`` thab, thbc))) THEN 104 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN 105 CONJ_TAC THEN CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM)) ] ) ; 106 107val RAT_EQUIV_TRANS' = REWRITE_RULE [GSYM AND_IMP_INTRO] RAT_EQUIV_TRANS ; 108 109fun e2tac tthm = FIRST_X_ASSUM (fn th1 => 110 let val tha1 = MATCH_MP tthm th1 ; 111 in FIRST_X_ASSUM (fn th2 => ACCEPT_TAC (MATCH_MP tha1 th2)) end) ; 112 113val RAT_EQUIV = store_thm("RAT_EQUIV", 114 ``!f1 f2. rat_equiv f1 f2 = (rat_equiv f1 = rat_equiv f2)``, 115 REPEAT GEN_TAC THEN EQ_TAC 116 THENL [ 117 REWRITE_TAC[FUN_EQ_THM] THEN 118 REPEAT STRIP_TAC THEN EQ_TAC THEN_LT 119 NTH_GOAL (ONCE_REWRITE_TAC [RAT_EQUIV_SYM]) 1 THEN 120 DISCH_TAC THEN e2tac RAT_EQUIV_TRANS', 121 DISCH_TAC THEN ASM_SIMP_TAC bool_ss [RAT_EQUIV_REF]]) ; 122 123(*--------------------------------------------------------------------------* 124 * RAT_EQUIV_ALT 125 * 126 * |- !a. rat_equiv a = 127 * \x. (?b c. 0<b /\ 0<c /\ 128 * (frac_mul a (abs_frac(b,b)) = frac_mul x (abs_frac(c,c)) )) 129 * 130 * alternative representation of equivalence relation 131 *--------------------------------------------------------------------------*) 132 133fun feqconv thm = let val thm' = UNDISCH_ALL (SPEC_ALL thm) ; 134 in DEPTH_CONV (REWR_CONV_A thm') end ; 135fun feqtac thm = VALIDATE (POP_ASSUM (ASSUME_TAC o CONV_RULE (feqconv thm))) ; 136 137fun msprod th = let val [thbc, thab] = CONJUNCTS th 138 in MK_COMB (AP_TERM ``int_mul`` (MATCH_MP EQ_SYM thab), thbc) end ; 139 140val RAT_EQUIV_ALT = store_thm("RAT_EQUIV_ALT", 141 ``!a. rat_equiv a = \x. (?b c. 0<b /\ 0<c /\ 142 (frac_mul a (abs_frac(b,b)) = frac_mul x (abs_frac(c,c)) ))``, 143 SIMP_TAC bool_ss [FUN_EQ_THM, rat_equiv_def, frac_mul_def] THEN 144 REPEAT GEN_TAC THEN EQ_TAC 145 THENL [ DISCH_TAC THEN 146 EXISTS_TAC ``frac_dnm x`` THEN EXISTS_TAC ``frac_dnm a`` THEN 147 ASM_SIMP_TAC bool_ss [FRAC_DNMPOS, NMR, DNM] THEN 148 VALIDATE (CONV_TAC (feqconv FRAC_EQ)) THEN 149 TRY (irule INT_MUL_POS_SIGN >> conj_tac >> irule FRAC_DNMPOS) THEN 150 CONJ_TAC 151 (* ASM_SIMP_TAC bool_ss [] does nothing - why ??? *) 152 THENL [ POP_ASSUM ACCEPT_TAC, ASM_SIMP_TAC bool_ss [INT_MUL_COMM] ], 153 REPEAT STRIP_TAC THEN 154 REV_FULL_SIMP_TAC bool_ss [NMR, DNM] THEN feqtac FRAC_EQ THEN 155 TRY (irule INT_MUL_POS_SIGN THEN 156 ASM_SIMP_TAC bool_ss [FRAC_DNMPOS]) THEN 157 POP_ASSUM (ASSUME_TAC o msprod) THEN 158 FIRST_X_ASSUM (fn th => 159 ONCE_REWRITE_TAC [MATCH_MP INT_EQ_RMUL_EXP th]) THEN 160 FIRST_X_ASSUM (fn th => 161 ONCE_REWRITE_TAC [MATCH_MP INT_EQ_RMUL_EXP th]) THEN 162 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN 163 CONJ_TAC THEN CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM)) ] ) ; 164 165(*--------------------------------------------------------------------------* 166 * type definition 167 *--------------------------------------------------------------------------*) 168 169(* following also stored as rat_QUOTIENT *) 170val rat_def = save_thm("rat_def", 171 define_quotient_type "rat" "abs_rat" "rep_rat" RAT_EQUIV); 172 173val QUOTIENT_def = DB.fetch "quotient" "QUOTIENT_def"; 174val rat_thm = REWRITE_RULE[QUOTIENT_def] rat_def ; (* was rat_def *) 175val rat_type_thm = save_thm ("rat_type_thm", 176 REWRITE_RULE[QUOTIENT_def, RAT_EQUIV_REF] rat_def) ; 177 178val rat_equiv_reps = store_thm ("rat_equiv_reps", 179 ``rat_equiv (rep_rat r1) (rep_rat r2) = (r1 = r2)``, 180 REWRITE_TAC [rat_type_thm]) ; 181 182val rat_equiv_rep_abs = store_thm ("rat_equiv_rep_abs", 183 ``rat_equiv (rep_rat (abs_rat f)) f``, 184 REWRITE_TAC [rat_type_thm]) ; 185 186(*--------------------------------------------------------------------------* 187 * operations 188 *--------------------------------------------------------------------------*) 189 190(* numerator, denominator, sign of a fraction *) 191val rat_nmr_def = Define `rat_nmr r = frac_nmr (rep_rat r)`; 192val rat_dnm_def = Define `rat_dnm r = frac_dnm (rep_rat r)`; 193val rat_sgn_def = Define `rat_sgn r = frac_sgn (rep_rat r)`; 194 195(* additive, multiplicative inverse of a fraction *) 196val rat_0_def = Define `rat_0 = abs_rat( frac_0 )`; 197val rat_1_def = Define `rat_1 = abs_rat( frac_1 )`; 198 199(* neutral elements *) 200val rat_ainv_def = Define `rat_ainv r1 = abs_rat( frac_ainv (rep_rat r1))`; 201val rat_minv_def = Define `rat_minv r1 = abs_rat( frac_minv (rep_rat r1))`; 202 203(* basic arithmetics *) 204val rat_add_def = zDefine `rat_add r1 r2 = abs_rat( frac_add (rep_rat r1) (rep_rat r2) )`; 205val rat_sub_def = zDefine `rat_sub r1 r2 = abs_rat( frac_sub (rep_rat r1) (rep_rat r2) )`; 206val rat_mul_def = zDefine `rat_mul r1 r2 = abs_rat( frac_mul (rep_rat r1) (rep_rat r2) )`; 207val rat_div_def = zDefine `rat_div r1 r2 = abs_rat( frac_div (rep_rat r1) (rep_rat r2) )`; 208 209(* order relations *) 210val rat_les_def = Define `rat_les r1 r2 = (rat_sgn (rat_sub r2 r1) = 1)`; 211val rat_gre_def = Define `rat_gre r1 r2 = rat_les r2 r1`; 212val rat_leq_def = Define `rat_leq r1 r2 = rat_les r1 r2 \/ (r1=r2)`; 213val rat_geq_def = Define `rat_geq r1 r2 = rat_leq r2 r1`; 214 215 216 217(* construction of rational numbers, support of numerals *) 218val rat_cons_def = Define `rat_cons (nmr:int) (dnm:int) = abs_rat (abs_frac(SGN nmr * SGN dnm * ABS nmr, ABS dnm))`; 219 220val rat_of_num_def = Define ` (rat_of_num 0 = rat_0) /\ (rat_of_num (SUC 0) = rat_1) /\ (rat_of_num (SUC (SUC n)) = rat_add (rat_of_num (SUC n)) rat_1)`; 221val _ = add_numeral_form(#"q", SOME "rat_of_num"); 222 223val rat_0 = store_thm("rat_0", ``0q = abs_rat( frac_0 )``, 224 PROVE_TAC[rat_of_num_def, rat_0_def] ); 225 226val rat_1 = store_thm("rat_1", ``1q = abs_rat( frac_1 )``, 227 SUBST_TAC[ARITH_PROVE ``1=SUC 0``] THEN RW_TAC arith_ss [rat_of_num_def, rat_1_def] ); 228 229(*-------------------------------------------------------------------------- 230 * parser rules 231 *--------------------------------------------------------------------------*) 232 233val _ = set_fixity "//" (Infixl 600) 234 235val _ = overload_on ("+", ``rat_add``); 236val _ = overload_on ("-", ``rat_sub``); 237val _ = overload_on ("*", ``rat_mul``); 238val _ = overload_on (GrammarSpecials.decimal_fraction_special, ``rat_div``); 239val _ = overload_on ("/", ``rat_div``); 240val _ = overload_on ("<", ``rat_les``); 241val _ = overload_on ("<=", ``rat_leq``); 242val _ = overload_on (">", ``rat_gre``); 243val _ = overload_on (">=", ``rat_geq``); 244val _ = overload_on ("~", ``rat_ainv``); 245val _ = overload_on ("numeric_negate", ``rat_ainv``); 246val _ = overload_on ("//", ``rat_cons``); 247 248local open ratPP in end 249val _ = add_ML_dependency "ratPP" 250val _ = add_user_printer ("rat.decimalfractions", 251 ``&(NUMERAL x):rat / &(NUMERAL y):rat``) 252 253(*-------------------------------------------------------------------------- 254 * RAT: thm 255 * |- !r. abs_rat ( rep_rat r ) = r 256 *--------------------------------------------------------------------------*) 257 258val RAT = store_thm("RAT", ``!r. abs_rat ( rep_rat r ) = r``, 259 ACCEPT_TAC (CONJUNCT1 rat_thm)) ; 260 261(*-------------------------------------------------------------------------- 262 * some lemmas 263 *--------------------------------------------------------------------------*) 264 265val RAT_ABS_EQUIV = store_thm("RAT_ABS_EQUIV", 266 ``!f1 f2. (abs_rat f1 = abs_rat f2) = rat_equiv f1 f2``, 267 REWRITE_TAC [rat_type_thm]) ; 268 269val REP_ABS_EQUIV = prove(``!a. rat_equiv a (rep_rat (abs_rat a))``, 270 REWRITE_TAC [rat_type_thm]) ; 271 272val RAT_ABS_EQUIV' = GSYM RAT_ABS_EQUIV ; 273val REP_ABS_EQUIV' = ONCE_REWRITE_RULE [RAT_EQUIV_SYM] REP_ABS_EQUIV ; 274 275val REP_ABS_DFN_EQUIV = prove(``!x. frac_nmr x * frac_dnm (rep_rat(abs_rat x)) = frac_nmr (rep_rat(abs_rat x)) * frac_dnm x``, 276 GEN_TAC THEN 277 REWRITE_TAC[GSYM rat_equiv_def] THEN 278 REWRITE_TAC[REP_ABS_EQUIV] ); 279 280val RAT_IMP_EQUIV = prove(``!r1 r2. (r1 = r2) ==> rat_equiv r1 r2``, 281 REPEAT STRIP_TAC THEN 282 ASM_REWRITE_TAC[RAT_EQUIV_REF]) ; 283 284(*========================================================================== 285 * equivalence of rational numbers 286 *==========================================================================*) 287 288(*-------------------------------------------------------------------------- 289 * RAT_EQ: thm 290 * |- !f1 f2. (abs_rat f1 = abs_rat f2) 291 * = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1) 292 *--------------------------------------------------------------------------*) 293 294val RAT_EQ = store_thm("RAT_EQ", 295``!f1 f2. (abs_rat f1 = abs_rat f2) = 296 (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)``, 297 REPEAT GEN_TAC THEN 298 REWRITE_TAC [RAT_ABS_EQUIV, rat_equiv_def] ); 299 300(*-------------------------------------------------------------------------- 301 * RAT_EQ_ALT: thm 302 * |- ! r1 r2. (r1=r2) = (rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1) 303 *--------------------------------------------------------------------------*) 304 305val RAT_EQ_ALT = store_thm("RAT_EQ_ALT", ``! r1 r2. (r1=r2) = (rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1)``, 306 REPEAT GEN_TAC THEN 307 REWRITE_TAC[rat_nmr_def, rat_dnm_def] THEN 308 REWRITE_TAC[GSYM rat_equiv_def] THEN 309 REWRITE_TAC[rat_type_thm] ); 310 311(*========================================================================== 312 * congruence theorems 313 *==========================================================================*) 314 315(*-------------------------------------------------------------------------- 316 * RAT_NMREQ0_CONG: thm 317 * |- !f1. (frac_nmr (rep_rat (abs_rat f1)) = 0) = (frac_nmr f1 = 0) 318 * 319 * RAT_NMRLT0_CONG: thmRAT_NMREQ0_CONG 320 * |- !f1. (frac_nmr (rep_rat (abs_rat f1)) < 0) = (frac_nmr f1 < 0) 321 * 322 * RAT_NMRGT0_CONG: thmRAT_NMREQ0_CONG 323 * |- !f1. (frac_nmr (rep_rat (abs_rat f1)) > 0) = (frac_nmr f1 > 0) 324 * 325 *--------------------------------------------------------------------------*) 326 327val RAT_NMREQ0_CONG = store_thm("RAT_NMREQ0_CONG", 328 ``!f1. (frac_nmr (rep_rat (abs_rat f1)) = 0) = (frac_nmr f1 = 0)``, 329 GEN_TAC THEN MATCH_ACCEPT_TAC 330 (MATCH_MP RAT_EQUIV_NMR_Z_IFF (SPEC_ALL REP_ABS_EQUIV'))) ; 331 332val RAT_NMRLT0_CONG = store_thm("RAT_NMRLT0_CONG", 333 ``!f1. (frac_nmr (rep_rat (abs_rat f1)) < 0) = (frac_nmr f1 < 0)``, 334 GEN_TAC THEN MATCH_ACCEPT_TAC 335 (MATCH_MP RAT_EQUIV_NMR_LTZ_IFF (SPEC_ALL REP_ABS_EQUIV'))) ; 336 337val RAT_NMRGT0_CONG = store_thm("RAT_NMRGT0_CONG", 338 ``!f1. (frac_nmr (rep_rat (abs_rat f1)) > 0) = (frac_nmr f1 > 0)``, 339 GEN_TAC THEN MATCH_ACCEPT_TAC 340 (MATCH_MP RAT_EQUIV_NMR_GTZ_IFF (SPEC_ALL REP_ABS_EQUIV'))) ; 341 342(*-------------------------------------------------------------------------- 343 * RAT_SGN_CONG: thm 344 * |- !f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1 345 *--------------------------------------------------------------------------*) 346 347val RAT_SGN_CONG = store_thm("RAT_SGN_CONG", ``!f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1``, 348 GEN_TAC THEN 349 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 350 REWRITE_TAC[RAT_NMREQ0_CONG, RAT_NMRLT0_CONG] ); 351 352(*-------------------------------------------------------------------------- 353 * RAT_AINV_CONG: thm 354 * |- !x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x) 355 *--------------------------------------------------------------------------*) 356 357val RAT_AINV_CONG = store_thm("RAT_AINV_CONG", ``!x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x)``, 358 REPEAT GEN_TAC THEN 359 REWRITE_TAC[RAT_ABS_EQUIV] THEN 360 REWRITE_TAC[rat_equiv_def,frac_ainv_def] THEN 361 SIMP_TAC bool_ss [NMR, DNM, FRAC_DNMPOS] THEN 362 REWRITE_TAC[INT_MUL_CALCULATE,INT_EQ_NEG] THEN 363 REWRITE_TAC[GSYM rat_equiv_def] THEN 364 ONCE_REWRITE_TAC[RAT_EQUIV_SYM] THEN 365 REWRITE_TAC[REP_ABS_EQUIV] ); 366 367(*-------------------------------------------------------------------------- 368 * RAT_MINV_CONG: thm 369 * |- !x. ~(frac_nmr x=0) ==> 370 * (abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x)) 371 *--------------------------------------------------------------------------*) 372 373val FRAC_MINV_EQUIV = store_thm ("FRAC_MINV_EQUIV", 374 ``~(frac_nmr y=0) ==> rat_equiv x y ==> 375 rat_equiv (frac_minv x) (frac_minv y)``, 376 DISCH_TAC THEN DISCH_THEN (fn th => MP_TAC th THEN ASSUME_TAC th) THEN 377 POP_ASSUM (ASSUME_TAC o MATCH_MP RAT_EQUIV_NMR_Z_IFF) THEN 378 REWRITE_TAC[frac_minv_def, rat_equiv_def, frac_sgn_def] THEN 379 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 380 (TRY (irule INT_ABS_NOT0POS THEN ASM_SIMP_TAC bool_ss [])) THEN 381 REWRITE_TAC[SGN_def] THEN REPEAT IF_CASES_TAC THEN 382 ASM_SIMP_TAC int_ss [INT_ABS, 383 GSYM INT_NEG_MINUS1, GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL] THEN 384 SIMP_TAC bool_ss [INT_MUL_COMM]) ; 385 386val RAT_MINV_CONG = store_thm("RAT_MINV_CONG", 387 ``!x. ~(frac_nmr x=0) ==> 388 (abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x))``, 389 REPEAT STRIP_TAC THEN 390 IMP_RES_TAC FRAC_MINV_EQUIV THEN 391 ASSUME_TAC (Q.SPEC `x` REP_ABS_EQUIV') THEN 392 RES_TAC THEN ASM_SIMP_TAC bool_ss [RAT_ABS_EQUIV]) ; 393 394(*-------------------------------------------------------------------------- 395 * RAT_ADD_CONG1: thm 396 * |- !x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y) 397 * 398 * RAT_ADD_CONG2: thm 399 * |- !x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y) 400 * 401 * RAT_ADD_CONG: thm 402 * |- !x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y) /\ 403 * !x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y) 404 *--------------------------------------------------------------------------*) 405 406val FRAC_ADD_EQUIV1 = store_thm ("FRAC_ADD_EQUIV1", 407 ``rat_equiv x x' ==> rat_equiv (frac_add x y) (frac_add x' y)``, 408 REWRITE_TAC[frac_add_def, rat_equiv_def] THEN 409 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 410 TRY (irule INT_MUL_POS_SIGN >> conj_tac >> irule FRAC_DNMPOS) THEN 411 REWRITE_TAC[INT_RDISTRIB] THEN DISCH_TAC THEN 412 MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC] 413 THENL [ 414 RULE_ASSUM_TAC (AP_TERM ``int_mul (frac_dnm y * frac_dnm y)``) THEN 415 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN CONJ_TAC, 416 ALL_TAC ] THEN 417 CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM)) ) ; 418 419val RAT_ADD_CONG1 = store_thm("RAT_ADD_CONG1", 420 ``!x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)``, 421 REPEAT STRIP_TAC THEN 422 SIMP_TAC bool_ss [RAT_ABS_EQUIV] THEN 423 irule FRAC_ADD_EQUIV1 THEN irule REP_ABS_EQUIV') ; 424 425val RAT_ADD_CONG2 = store_thm("RAT_ADD_CONG2", ``!x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)``, 426 ONCE_REWRITE_TAC[FRAC_ADD_COMM] THEN 427 REWRITE_TAC[RAT_ADD_CONG1]); 428 429val RAT_ADD_CONG = save_thm("RAT_ADD_CONG", CONJ RAT_ADD_CONG1 RAT_ADD_CONG2); 430 431(*-------------------------------------------------------------------------- 432 * RAT_MUL_CONG1: thm 433 * |- !x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y) 434 * 435 * RAT_MUL_CONG2: thm 436 * |- !x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y) 437 * 438 * RAT_MUL_CONG: thm 439 * |- !x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y) /\ 440 * !x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y) 441 *--------------------------------------------------------------------------*) 442 443val FRAC_MUL_EQUIV1 = store_thm ("FRAC_MUL_EQUIV1", 444 ``rat_equiv x x' ==> rat_equiv (frac_mul x y) (frac_mul x' y)``, 445 REWRITE_TAC[frac_mul_def, rat_equiv_def] THEN 446 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 447 TRY (irule INT_MUL_POS_SIGN >> conj_tac >> irule FRAC_DNMPOS) >> DISCH_TAC >> 448 RULE_ASSUM_TAC (AP_TERM ``int_mul (frac_nmr y * frac_dnm y)``) THEN 449 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN 450 CONJ_TAC THEN CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM)) ) ; 451 452val FRAC_MUL_EQUIV2 = save_thm ("FRAC_MUL_EQUIV2", 453 ONCE_REWRITE_RULE [FRAC_MUL_COMM] FRAC_MUL_EQUIV1) ; 454 455val RAT_MUL_CONG1 = store_thm("RAT_MUL_CONG1", 456 ``!x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)``, 457 REPEAT STRIP_TAC THEN 458 SIMP_TAC bool_ss [RAT_ABS_EQUIV] THEN 459 irule FRAC_MUL_EQUIV1 THEN irule REP_ABS_EQUIV') ; 460 461val RAT_MUL_CONG2 = store_thm("RAT_MUL_CONG2", ``!x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)``, 462 ONCE_REWRITE_TAC[FRAC_MUL_COMM] THEN 463 RW_TAC int_ss[RAT_MUL_CONG1]); 464 465val RAT_MUL_CONG = save_thm("RAT_MUL_CONG", CONJ RAT_MUL_CONG1 RAT_MUL_CONG2); 466 467(*-------------------------------------------------------------------------- 468 * RAT_SUB_CONG1: thm 469 * |- !x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y) 470 * 471 * RAT_SUB_CONG2: thm 472 * |- !x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y) 473 * 474 * RAT_SUB_CONG: thm 475 * |- !x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y) /\ 476 * !x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y) 477 *--------------------------------------------------------------------------*) 478 479val RAT_SUB_CONG1 = store_thm("RAT_SUB_CONG1", ``!x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)``, 480 REWRITE_TAC[frac_sub_def] THEN 481 REWRITE_TAC[RAT_ADD_CONG]); 482 483val RAT_SUB_CONG2 = store_thm("RAT_SUB_CONG2", ``!x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)``, 484 ONCE_REWRITE_TAC[GSYM FRAC_AINV_SUB] THEN 485 ONCE_REWRITE_TAC[GSYM RAT_AINV_CONG] THEN 486 REWRITE_TAC[RAT_SUB_CONG1] ); 487 488val RAT_SUB_CONG = save_thm("RAT_SUB_CONG", CONJ RAT_SUB_CONG1 RAT_SUB_CONG2); 489 490(*-------------------------------------------------------------------------- 491 * RAT_DIV_CONG1: thm 492 * |- !x y. ~(frac_nmr y = 0) ==> 493 * (abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)) 494 * 495 * RAT_DIV_CONG2: thm 496 * |- !x y. ~(frac_nmr y = 0) ==> 497 (abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y)) 498 * 499 * RAT_DIV_CONG: thm 500 * |- !x y. ~(frac_nmr y = 0) ==> 501 * (abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)) /\ 502 * !x y. ~(frac_nmr y = 0) ==> 503 (abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y)) 504 *--------------------------------------------------------------------------*) 505 506val RAT_DIV_CONG1 = store_thm("RAT_DIV_CONG1", 507 ``!x y. ~(frac_nmr y = 0) ==> 508 (abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y))``, 509 REPEAT STRIP_TAC THEN 510 REWRITE_TAC[frac_div_def] THEN 511 REWRITE_TAC[RAT_MUL_CONG] ); 512 513val RAT_DIV_CONG2 = store_thm("RAT_DIV_CONG2", 514 ``!x y. ~(frac_nmr y = 0) ==> 515 (abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y))``, 516 REPEAT STRIP_TAC THEN 517 REWRITE_TAC[frac_div_def, RAT_ABS_EQUIV] THEN 518 irule FRAC_MUL_EQUIV2 THEN 519 IMP_RES_THEN MATCH_MP_TAC FRAC_MINV_EQUIV THEN 520 irule rat_equiv_rep_abs) ; 521 522val RAT_DIV_CONG = save_thm("RAT_DIV_CONG", CONJ RAT_DIV_CONG1 RAT_DIV_CONG2 ); 523 524(*========================================================================== 525 * numerator and denominator 526 *==========================================================================*) 527 528(*-------------------------------------------------------------------------- 529 * RAT_NMRDNM_EQ: thm 530 * |- (abs_rat(abs_frac(frac_nmr f1,frac_dnm f1)) = 1q) = (frac_nmr f1 = frac_dnm f1) 531 *--------------------------------------------------------------------------*) 532 533val RAT_NMRDNM_EQ = store_thm("RAT_NMRDNM_EQ",``(abs_rat(abs_frac(frac_nmr f1,frac_dnm f1)) = 1q) = (frac_nmr f1 = frac_dnm f1)``, 534 SIMP_TAC bool_ss [rat_equiv_def, RAT_ABS_EQUIV, 535 rat_1, frac_1_def, NMR, DNM, FRAC_DNMPOS, INT_LT_01, 536 INT_MUL_LID, INT_MUL_RID]) ; 537 538(*========================================================================== 539 * calculation 540 *==========================================================================*) 541 542(*-------------------------------------------------------------------------- 543 * RAT_AINV_CALCULATE: thm 544 * |- !f1. rat_ainv (abs_rat(f1)) = abs_rat( frac_ainv f1 ) 545 *--------------------------------------------------------------------------*) 546 547val RAT_AINV_CALCULATE = store_thm("RAT_AINV_CALCULATE", ``!f1. rat_ainv (abs_rat(f1)) = abs_rat( frac_ainv f1 )``, 548 REPEAT GEN_TAC THEN 549 REWRITE_TAC[rat_ainv_def] THEN 550 PROVE_TAC[RAT_AINV_CONG] ); 551 552(*-------------------------------------------------------------------------- 553 * RAT_MINV_CALCULATE: thm 554 * |- !f1. rat_ainv (abs_rat(f1)) = abs_rat( frac_ainv f1 ) 555 *--------------------------------------------------------------------------*) 556 557val RAT_MINV_CALCULATE = store_thm("RAT_MINV_CALCULATE", ``!f1. ~(0 = frac_nmr f1) ==> (rat_minv (abs_rat(f1)) = abs_rat( frac_minv f1 ))``, 558 REPEAT GEN_TAC THEN 559 REWRITE_TAC[rat_minv_def] THEN 560 PROVE_TAC[RAT_MINV_CONG] ); 561 562(*-------------------------------------------------------------------------- 563 * RAT_ADD_CALCULATE: thm 564 * |- !f1 f2. rat_add (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_add f1 f2 ) 565 *--------------------------------------------------------------------------*) 566 567val RAT_ADD_CALCULATE = store_thm( 568 "RAT_ADD_CALCULATE", 569 ���!f1 f2. rat_add (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_add f1 f2 )���, 570 REPEAT GEN_TAC THEN REWRITE_TAC[rat_add_def] THEN PROVE_TAC[RAT_ADD_CONG] ); 571 572(*-------------------------------------------------------------------------- 573 * RAT_SUB_CALCULATE: thm 574 * |- !f1 f2. rat_sub (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_sub f1 f2 ) 575 *--------------------------------------------------------------------------*) 576 577val RAT_SUB_CALCULATE = store_thm( 578 "RAT_SUB_CALCULATE", 579 ���!f1 f2. rat_sub (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_sub f1 f2 )���, 580 REPEAT GEN_TAC THEN REWRITE_TAC[rat_sub_def] THEN PROVE_TAC[RAT_SUB_CONG] ); 581 582(*-------------------------------------------------------------------------- 583 * RAT_MUL_CALCULATE: thm 584 * |- !f1 f2. rat_mul (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_mul f1 f2 ) 585 *--------------------------------------------------------------------------*) 586 587val RAT_MUL_CALCULATE = store_thm( 588 "RAT_MUL_CALCULATE", 589 ���!f1 f2. rat_mul (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_mul f1 f2 )���, 590 REPEAT GEN_TAC THEN REWRITE_TAC[rat_mul_def] THEN PROVE_TAC[RAT_MUL_CONG]); 591 592(* ---------------------------------------------------------------------- 593 RAT_DIV_CALCULATE: thm 594 |- !f1 f2. 595 frac_nmr f2 <> 0 ==> 596 (rat_div (abs_rat f1) (abs_rat f2) = abs_rat(frac_div f1 f2)) 597 ---------------------------------------------------------------------- *) 598 599val RAT_DIV_CALCULATE = store_thm( 600 "RAT_DIV_CALCULATE", 601 ���!f1 f2. frac_nmr f2 <> 0 ==> 602 (rat_div (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_div f1 f2 ))���, 603 REPEAT STRIP_TAC THEN REWRITE_TAC[rat_div_def] THEN PROVE_TAC[RAT_DIV_CONG]); 604 605(*-------------------------------------------------------------------------- 606 * RAT_EQ_CALCULATE: thm 607 * |- !f1 f2. (abs_rat f1 = abs_rat f2) = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1) 608 *--------------------------------------------------------------------------*) 609 610val RAT_EQ_CALCULATE = store_thm( 611 "RAT_EQ_CALCULATE", 612 ���!f1 f2. (abs_rat f1 = abs_rat f2) <=> 613 (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)���, 614 PROVE_TAC[RAT_ABS_EQUIV, rat_equiv_def] ); 615 616 617(* ---------------------------------------------------------------------- 618 RAT_LES_CALCULATE: thm 619 |- !f1 f2. (abs_rat f1 < abs_rat f2) = 620 (frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1) 621 ---------------------------------------------------------------------- *) 622 623val RAT_LES_CALCULATE = store_thm( 624 "RAT_LES_CALCULATE", 625 ���!f1 f2. (abs_rat f1 < abs_rat f2) = 626 (frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1)���, 627 REPEAT GEN_TAC THEN 628 REWRITE_TAC[rat_les_def, rat_sgn_def, RAT_SUB_CALCULATE, RAT_SGN_CONG] THEN 629 REWRITE_TAC[frac_sgn_def, frac_sub_def, frac_add_def, frac_ainv_def] THEN 630 FRAC_POS_TAC 631 ���frac_dnm f2 * frac_dnm (abs_frac (~frac_nmr f1,frac_dnm f1))��� THEN 632 FRAC_NMRDNM_TAC THEN 633 REWRITE_TAC[INT_SGN_CLAUSES, int_gt] THEN 634 `~frac_nmr f1 * frac_dnm f2 = ~(frac_nmr f1 * frac_dnm f2)` by ARITH_TAC THEN 635 ASM_REWRITE_TAC[INT_LT_ADDNEG, INT_ADD_LID] ); 636 637val RAT_LEQ_CALCULATE = store_thm("RAT_LEQ_CALCULATE", 638 ``!f1 f2. (abs_rat f1 <= abs_rat f2) = 639 (frac_nmr f1 * frac_dnm f2 <= frac_nmr f2 * frac_dnm f1)``, 640 REPEAT GEN_TAC THEN 641 REWRITE_TAC[rat_leq_def, RAT_LES_CALCULATE, INT_LE_LT, RAT_EQ_CALCULATE]) ; 642 643val RAT_OF_NUM_CALCULATE = store_thm( 644 "RAT_OF_NUM_CALCULATE", 645 ``!n1. rat_of_num n1 = abs_rat( abs_frac( &n1, 1) )``, 646 recInduct (DB.fetch "-" "rat_of_num_ind") THEN 647 RW_TAC arith_ss [rat_of_num_def, rat_0_def, frac_0_def, rat_1_def, frac_1_def, 648 RAT_ADD_CALCULATE, frac_add_def] THEN 649 FRAC_POS_TAC ``1i`` THEN 650 RW_TAC int_ss 651 [NMR, DNM, ARITH_PROVE ���int_of_num (SUC n) + 1 = int_of_num (SUC (SUC n))���] 652); 653 654val RAT_OF_NUM_LEQ = store_thm("RAT_OF_NUM_LEQ[simp]", 655 ``rat_of_num a <= rat_of_num b = a <= b``, 656 SIMP_TAC std_ss [RAT_OF_NUM_CALCULATE, RAT_LEQ_CALCULATE, 657 NMR, DNM, INT_LT_01, INT_MUL_RID, INT_LE]); 658 659val RAT_OF_NUM_LES = store_thm("RAT_OF_NUM_LES[simp]", 660 ``rat_of_num a < rat_of_num b = a < b``, 661 SIMP_TAC std_ss [RAT_OF_NUM_CALCULATE, RAT_LES_CALCULATE, 662 NMR, DNM, INT_LT_01, INT_MUL_RID, INT_LT]); 663 664(*-------------------------------------------------------------------------- 665 * rat_calculate_table : (term * thm) list 666 *--------------------------------------------------------------------------*) 667 668val rat_calculate_table = [ 669 ( ``rat_0``, rat_0_def ), 670 ( ``rat_1``, rat_1_def ), 671 ( ``rat_ainv``, RAT_AINV_CALCULATE ), 672 ( ``rat_minv``, RAT_MINV_CALCULATE ), 673 ( ``rat_add``, RAT_ADD_CALCULATE ), 674 ( ``rat_sub``, RAT_SUB_CALCULATE ), 675 ( ``rat_mul``, RAT_MUL_CALCULATE ), 676 ( ``rat_div``, RAT_DIV_CALCULATE ) 677]; 678 679(*-------------------------------------------------------------------------- 680 * RAT_CALC_CONV : conv 681 * 682 * r1 683 * --------------------- 684 * |- r1 = abs_rat(f1) 685 *--------------------------------------------------------------------------*) 686 687fun RAT_CALC_CONV (t1:term) = 688let 689 val thm = REFL t1; 690 val (top_rator, top_rands) = strip_comb t1; 691 val calc_table_entry = 692 List.find (fn x => fst(x) ~~ top_rator) rat_calculate_table; 693in 694 (* do nothing if term is already in the form abs_rat(...) *) 695 if top_rator ~~ ``abs_rat`` then 696 thm 697 (* if it is a numeral, simply rewrite it *) 698 else if (top_rator ~~ ``rat_of_num``) then 699 SUBST [``x:rat`` |-> SPEC (rand t1) (RAT_OF_NUM_CALCULATE)] ``^t1 = x:rat`` thm 700 (* if there is an entry in the calculation table, calculate it *) 701 else if (isSome calc_table_entry) then 702 let 703 val arg_thms = map RAT_CALC_CONV top_rands; 704 val arg_fracs = map (fn x => rand(rhs(concl x))) arg_thms; 705 val arg_vars = map (fn x => genvar ``:rat``) arg_thms; 706 707 val subst_list = map (fn x => fst(x) |-> snd(x)) (ListPair.zip (arg_vars,arg_thms)); 708 (* subst_term: t1 = top_rator arg_vars[1] ... arg_vars[n] *) 709 val subst_term = mk_eq (t1 , list_mk_comb (top_rator,arg_vars)) 710 711 val thm1 = SUBST subst_list subst_term thm; 712 val (thm1_lhs, thm1_rhs) = dest_eq(concl thm1); 713 val thm1_lhs_var = genvar ``:rat``; 714 715 val calc_thm = snd (valOf( calc_table_entry )); 716 in 717 SUBST [thm1_lhs_var |-> UNDISCH_ALL (SPECL arg_fracs calc_thm)] ``^thm1_lhs = ^thm1_lhs_var`` thm1 718 end 719 (* otherwise: applying r = abs_rat(rep_rat r)) always works *) 720 else 721 SUBST [``x:rat`` |-> SPEC t1 (GSYM RAT)] ``^t1 = x:rat`` thm 722end; 723 724(*-------------------------------------------------------------------------- 725 * RAT_CALCTERM_TAC : term -> tactic 726 * 727 * calculates the value of t1:rat 728 *--------------------------------------------------------------------------*) 729 730fun RAT_CALCTERM_TAC (t1:term) (asm_list,goal) = 731 let 732 val calc_thm = RAT_CALC_CONV t1; 733 val (calc_asms, calc_concl) = dest_thm calc_thm; 734 in 735 ( 736 MAP_EVERY ASSUME_TAC (map (fn x => TAC_PROOF ((asm_list,x), RW_TAC intLib.int_ss [FRAC_DNMPOS,INT_MUL_POS_SIGN,INT_NOTPOS0_NEG,INT_NOT0_MUL,INT_GT0_IMP_NOT0,INT_ABS_NOT0POS])) calc_asms) THEN 737 SUBST_TAC[calc_thm] 738 ) (asm_list,goal) 739 end 740handle HOL_ERR _ => raise ERR "RAT_CALCTERM_TAC" ""; 741 742 743(*-------------------------------------------------------------------------- 744 * RAT_CALC_TAC : tactic 745 * 746 * calculates the value of all subterms (of type ``:rat``) 747 * assumptions that were needed for the simplification are added to the goal 748 *--------------------------------------------------------------------------*) 749 750fun RAT_CALC_TAC (asm_list,goal) = 751 let 752 (* extract terms of type ``:rat`` *) 753 val rat_terms = extract_rat goal; 754 (* build conversions *) 755 val calc_thms = map RAT_CALC_CONV rat_terms; 756 (* split list into assumptions and conclusions *) 757 val (calc_asmlists, calc_concl) = ListPair.unzip (map (fn x => dest_thm x) calc_thms); 758 (* merge assumptions lists *) 759 val calc_asms = op_U aconv calc_asmlists; 760 (* function to prove an assumption, TODO: fracLib benutzen *) 761 val gen_thm = (fn x => TAC_PROOF ((asm_list,x), RW_TAC intLib.int_ss [] )); 762 (* try to prove assumptions *) 763 val prove_list = List.map (total gen_thm) calc_asms; 764 (* combine assumptions and their proofs *) 765 val list1 = ListPair.zip (calc_asms,prove_list); 766 (* partition assumptions into proved assumptions and assumptions to be proved *) 767 val list2 = partition (fn x => isSome (snd x)) list1; 768 val asms_toprove = map fst (snd list2); 769 val asms_proved = map (fn x => valOf (snd x)) (fst list2); 770 (* generate new subgoal goal *) 771 val subst_goal = snd (dest_eq (snd (dest_thm (ONCE_REWRITE_CONV calc_thms goal)))); 772 val subgoal = (list_mk_conj (asms_toprove @ [subst_goal]) ); 773 val mp_thm = TAC_PROOF 774 ( 775 (asm_list, mk_imp (subgoal,goal)) 776 , 777 STRIP_TAC THEN 778 MAP_EVERY ASSUME_TAC asms_proved THEN 779 ONCE_REWRITE_TAC calc_thms THEN 780 PROVE_TAC [] 781 ); 782 in 783 ( [(asm_list,subgoal)], fn (thms:thm list) => MP mp_thm (hd thms) ) 784 end 785handle HOL_ERR _ => raise ERR "RAT_CALC_TAC" ""; 786 787(*-------------------------------------------------------------------------- 788 * RAT_CALCEQ_TAC : tactic 789 *--------------------------------------------------------------------------*) 790 791val RAT_CALCEQ_TAC = 792 RAT_CALC_TAC THEN 793 FRAC_CALC_TAC THEN 794 REWRITE_TAC[RAT_EQ] THEN 795 FRAC_NMRDNM_TAC THEN 796 INT_RING_TAC; 797 798 799(*========================================================================== 800 * numerator of rational number: sign reduction 801 *==========================================================================*) 802 803(*-------------------------------------------------------------------------- 804 RAT_EQ0_NMR: thm 805 |- !r1. (r1 = 0q) = (rat_nmr r1 = 0) 806 *--------------------------------------------------------------------------*) 807 808val RAT_EQ0_NMR = store_thm("RAT_EQ0_NMR", ``!r1. (r1 = 0q) = (rat_nmr r1 = 0)``, 809 GEN_TAC THEN 810 REWRITE_TAC[rat_nmr_def] THEN 811 SUBST_TAC[SPEC ``r1:rat`` (GSYM RAT)] THEN 812 REWRITE_TAC[RAT_NMREQ0_CONG] THEN 813 REWRITE_TAC[rat_0, frac_0_def, RAT_ABS_EQUIV, rat_equiv_def] THEN 814 FRAC_POS_TAC ``1i`` THEN 815 FRAC_NMRDNM_TAC ); 816 817(*-------------------------------------------------------------------------- 818 RAT_0LES_NMR: thm 819 |- !r1. (0q < r1) = (0 < rat_nmr r1) 820 821 RAT_0LES_NMR: thm 822 |- !r1. (r1 < 0q) = (rat_nmr r1 < 0i) 823 *--------------------------------------------------------------------------*) 824 825val RAT_0LES_NMR = store_thm("RAT_0LES_NMR", ``!r1. rat_les 0q r1 = 0i < rat_nmr r1``, 826 GEN_TAC THEN 827 REWRITE_TAC[rat_0, rat_nmr_def, rat_les_def, rat_sgn_def, frac_0_def, frac_sgn_def, SGN_def] THEN 828 RAT_CALC_TAC THEN 829 FRAC_POS_TAC ``1i`` THEN 830 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN 831 SUBST_TAC[FRAC_CALC_CONV ``frac_sub (rep_rat r1) (abs_frac (0,1))``] THEN 832 REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG,RAT_NMRGT0_CONG] THEN 833 FRAC_NMRDNM_TAC THEN 834 RW_TAC int_ss [RAT, FRAC, INT_SUB_RZERO] THEN 835 PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL] ); 836 837val RAT_LES0_NMR = store_thm("RAT_LES0_NMR", ``!r1. rat_les r1 0q = rat_nmr r1 < 0i``, 838 GEN_TAC THEN 839 REWRITE_TAC[rat_0, rat_nmr_def, rat_les_def, rat_sgn_def, frac_0_def, frac_sgn_def, SGN_def] THEN 840 RAT_CALC_TAC THEN 841 FRAC_POS_TAC ``1i`` THEN 842 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN 843 SUBST_TAC[FRAC_CALC_CONV ``frac_sub (abs_frac (0,1)) (rep_rat r1)``] THEN 844 REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG,RAT_NMRGT0_CONG] THEN 845 FRAC_NMRDNM_TAC THEN 846 RW_TAC int_ss [RAT, FRAC, INT_SUB_LZERO] THEN 847 PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL, INT_NEG_LT0, INT_NEG_EQ, INT_NEG_0] ); 848 849(*-------------------------------------------------------------------------- 850 RAT_0LES_NMR: thm 851 |- !r1. (0q <= r1) = (0i <= rat_nmr r1) 852 853 RAT_0LES_NMR: thm 854 |- !r1. (r1 <= 0q) = (rat_nmr r1 <= 0i) 855 *--------------------------------------------------------------------------*) 856 857val RAT_0LEQ_NMR = store_thm("RAT_0LEQ_NMR", ``!r1. rat_leq 0q r1 = 0i <= rat_nmr r1``, 858 GEN_TAC THEN 859 REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN 860 NEW_GOAL_TAC ``!a b c d. ((a=c) /\ (b=d)) ==> (a \/ b = c \/ d)`` THEN 861 PROVE_TAC[RAT_0LES_NMR, RAT_EQ0_NMR, rat_nmr_def] ); 862 863val RAT_LEQ0_NMR = store_thm("RAT_LEQ0_NMR", ``!r1. rat_leq r1 0q = rat_nmr r1 <= 0i``, 864 GEN_TAC THEN 865 REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN 866 NEW_GOAL_TAC ``!a b c d. ((a=c) /\ (b=d)) ==> (a \/ b = c \/ d)`` THEN 867 PROVE_TAC[RAT_LES0_NMR, RAT_EQ0_NMR, rat_nmr_def] ); 868 869(*========================================================================== 870 * field properties 871 *==========================================================================*) 872 873(*-------------------------------------------------------------------------- 874 RAT_ADD_ASSOC: thm 875 |- !a b c. rat_add a (rat_add b c) = rat_add (rat_add a b) c 876 877 RAT_MUL_ASSOC: thm 878 |- !a b c. rat_mul a (rat_mul b c) = rat_mul (rat_mul a b) c 879 *--------------------------------------------------------------------------*) 880 881val RAT_ADD_ASSOC = store_thm("RAT_ADD_ASSOC", ``!a b c. rat_add a (rat_add b c) = rat_add (rat_add a b) c``, 882 REWRITE_TAC[rat_add_def] THEN 883 REWRITE_TAC[RAT_ADD_CONG] THEN 884 REWRITE_TAC[FRAC_ADD_ASSOC] ); 885 886val RAT_MUL_ASSOC = store_thm("RAT_MUL_ASSOC", ``!a b c. rat_mul a (rat_mul b c) = rat_mul (rat_mul a b) c``, 887 REWRITE_TAC[rat_mul_def] THEN 888 REWRITE_TAC[RAT_MUL_CONG] THEN 889 REWRITE_TAC[FRAC_MUL_ASSOC] ); 890 891(*-------------------------------------------------------------------------- 892 RAT_ADD_COMM: thm 893 |- !a b. rat_add a b = rat_add b a 894 895 RAT_MUL_COMM: thm 896 |- !a b. rat_mul a b = rat_mul b a 897 *--------------------------------------------------------------------------*) 898 899val RAT_ADD_COMM = store_thm("RAT_ADD_COMM", ``!a b. rat_add a b = rat_add b a``, 900 REPEAT GEN_TAC THEN 901 REWRITE_TAC[rat_add_def] THEN 902 AP_TERM_TAC THEN 903 MATCH_ACCEPT_TAC FRAC_ADD_COMM) ; 904 905val RAT_MUL_COMM = store_thm("RAT_MUL_COMM", ``!a b. rat_mul a b = rat_mul b a``, 906 REPEAT GEN_TAC THEN 907 REWRITE_TAC[rat_mul_def] THEN 908 AP_TERM_TAC THEN 909 MATCH_ACCEPT_TAC FRAC_MUL_COMM) ; 910 911(*-------------------------------------------------------------------------- 912 RAT_ADD_RID: thm 913 |- !a. rat_add a 0q = a 914 915 RAT_ADD_LID: thm 916 |- !a. rat_add 0q a = a 917 918 RAT_MUL_RID: thm 919 |- !a. rat_mul a 1q = a 920 921 RAT_MUL_LID: thm 922 |- !a. rat_mul 1q a = a 923 *--------------------------------------------------------------------------*) 924 925val RAT_ADD_RID = store_thm("RAT_ADD_RID[simp]", ``!a. rat_add a 0q = a``, 926 REWRITE_TAC[rat_add_def,rat_0] THEN 927 REWRITE_TAC[RAT_ADD_CONG] THEN 928 REWRITE_TAC[FRAC_ADD_RID] THEN 929 REWRITE_TAC[CONJUNCT1 rat_thm]); 930 931val RAT_ADD_LID = store_thm("RAT_ADD_LID[simp]", ``!a. rat_add 0q a = a``, 932 ONCE_REWRITE_TAC[RAT_ADD_COMM] THEN 933 REWRITE_TAC[RAT_ADD_RID] ); 934 935val RAT_MUL_RID = store_thm("RAT_MUL_RID[simp]", ``!a. rat_mul a 1q = a``, 936 REWRITE_TAC[rat_mul_def,rat_1] THEN 937 REWRITE_TAC[RAT_MUL_CONG] THEN 938 REWRITE_TAC[FRAC_MUL_RID] THEN 939 REWRITE_TAC[CONJUNCT1 rat_thm]); 940 941val RAT_MUL_LID = store_thm("RAT_MUL_LID[simp]", ``!a. rat_mul 1q a = a``, 942 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN 943 REWRITE_TAC[RAT_MUL_RID] ); 944 945(*-------------------------------------------------------------------------- 946 RAT_ADD_RINV: thm 947 |- !a. rat_add a (rat_ainv a) = 0q 948 949 RAT_ADD_LINV: thm 950 |- !a. rat_add (rat_ainv a) a = 0q 951 952 RAT_MUL_RINV: thm 953 |- !a. ~(a=0q) ==> (rat_mul a (rat_minv a) = 1q) 954 955 RAT_MUL_LINV: thm 956 |- !a. ~(a = 0q) ==> (rat_mul (rat_minv a) a = 1q) 957 *--------------------------------------------------------------------------*) 958 959val RAT_ADD_RINV = store_thm("RAT_ADD_RINV", 960 ``!a. rat_add a (rat_ainv a) = 0q``, 961 GEN_TAC THEN 962 REWRITE_TAC[rat_add_def,rat_ainv_def,rat_0,RAT_ADD_CONG] THEN 963 REWRITE_TAC[frac_add_def,frac_ainv_def,frac_0_def] THEN 964 SIMP_TAC bool_ss [NMR, DNM, FRAC_DNMPOS] THEN 965 REWRITE_TAC[RAT_ABS_EQUIV,rat_equiv_def] THEN 966 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 967 simp[INT_MUL_POS_SIGN, FRAC_DNMPOS] THEN 968 REWRITE_TAC [INT_MUL_LZERO, INT_MUL_RID, INT_LT_01, 969 GSYM INT_NEG_LMUL, INT_ADD_RINV]) ; 970 971val RAT_ADD_LINV = store_thm("RAT_ADD_LINV", 972 ``!a. rat_add (rat_ainv a) a = 0q``, 973 ONCE_REWRITE_TAC[RAT_ADD_COMM] THEN 974 REWRITE_TAC[RAT_ADD_RINV] ); 975 976val RAT_MUL_RINV = store_thm("RAT_MUL_RINV", 977 ``!a. ~(a=0q) ==> (rat_mul a (rat_minv a) = 1q)``, 978 REPEAT STRIP_TAC THEN 979 REWRITE_TAC[rat_mul_def, rat_minv_def, rat_1, RAT_MUL_CONG] THEN 980 REWRITE_TAC[frac_mul_def, frac_minv_def, frac_1_def] THEN 981 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN 982 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 983 TRY (irule INT_MUL_POS_SIGN >> conj_tac) THEN 984 TRY (irule FRAC_DNMPOS) THEN 985 TRY (irule INT_LT_01) THEN 986 TRY (irule INT_ABS_NOT0POS) THEN 987 ASM_REWRITE_TAC [GSYM RAT_EQ0_NMR, GSYM rat_nmr_def] THEN 988 REWRITE_TAC[INT_MUL_LID, INT_MUL_RID, frac_sgn_def, 989 ABS_EQ_MUL_SGN, rat_nmr_def] THEN 990 CONV_TAC (AC_CONV (INT_MUL_ASSOC, INT_MUL_COMM))) ; 991 992val RAT_MUL_LINV = store_thm("RAT_MUL_LINV", 993 ``!a. ~(a = 0q) ==> (rat_mul (rat_minv a) a = 1q)``, 994 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN 995 RW_TAC int_ss[RAT_MUL_RINV] ); 996 997(*-------------------------------------------------------------------------- 998 RAT_RDISTRIB: thm 999 |- !a b c. rat_mul (rat_add a b) c = rat_add (rat_mul a c) (rat_mul b c) 1000 1001 RAT_LDISTRIB: thm 1002 |- !a b c. rat_mul c (rat_add a b) = rat_add (rat_mul c a) (rat_mul c b) 1003 *--------------------------------------------------------------------------*) 1004 1005val RAT_RDISTRIB = store_thm("RAT_RDISTRIB", 1006 ``!a b c. rat_mul (rat_add a b) c = rat_add (rat_mul a c) (rat_mul b c)``, 1007 REPEAT GEN_TAC THEN 1008 REWRITE_TAC[rat_mul_def,rat_add_def] THEN 1009 REWRITE_TAC[RAT_MUL_CONG, RAT_ADD_CONG] THEN 1010 REWRITE_TAC[frac_mul_def,frac_add_def] THEN 1011 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 1012 simp[INT_MUL_POS_SIGN, FRAC_DNMPOS] THEN 1013 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN 1014 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN 1015 simp[INT_MUL_POS_SIGN, FRAC_DNMPOS] THEN 1016 REWRITE_TAC[INT_RDISTRIB] THEN BINOP_TAC THEN 1017 CONV_TAC (AC_CONV (INT_MUL_ASSOC, INT_MUL_COMM))) ; 1018 1019val RAT_LDISTRIB = store_thm("RAT_LDISTRIB", 1020 ``!a b c. rat_mul c (rat_add a b) = rat_add (rat_mul c a) (rat_mul c b)``, 1021 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN 1022 REWRITE_TAC[RAT_RDISTRIB] ); 1023 1024(*-------------------------------------------------------------------------- 1025 RAT_1_NOT_0: thm 1026 |- ~ (1q=0q) 1027 *--------------------------------------------------------------------------*) 1028 1029val RAT_1_NOT_0 = store_thm("RAT_1_NOT_0", ``~ (1q=0q)``, 1030 REWRITE_TAC[rat_0, rat_1] THEN 1031 REWRITE_TAC[frac_1_def, frac_0_def] THEN 1032 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN 1033 FRAC_POS_TAC ``1i`` THEN 1034 RW_TAC int_ss[NMR,DNM] ); 1035 1036(*========================================================================== 1037 * arithmetic rules 1038 *==========================================================================*) 1039 1040(*-------------------------------------------------------------------------- 1041 RAT_MUL_LZERO: thm 1042 |- !r1. rat_mul 0q r1 = 0q 1043 1044 RAT_MUL_RZERO: thm 1045 |- !r1. rat_mul r1 0q = 0q 1046 *--------------------------------------------------------------------------*) 1047 1048val RAT_MUL_LZERO = store_thm( 1049 "RAT_MUL_LZERO[simp]", ���!r1. rat_mul 0q r1 = 0q���, 1050 GEN_TAC THEN RAT_CALCEQ_TAC); 1051 1052val RAT_MUL_RZERO = store_thm( 1053 "RAT_MUL_RZERO[simp]", 1054 ���!r1. rat_mul r1 0q = 0q���, 1055 PROVE_TAC[RAT_MUL_LZERO, RAT_MUL_COMM] ); 1056 1057(*-------------------------------------------------------------------------- 1058 RAT_SUB_ADDAINV: thm 1059 |- !r1 r2. rat_sub r1 r2 = rat_add r1 (rat_ainv r2) 1060 1061 RAT_DIV_MULMINV: thm 1062 |- !r1 r2. rat_div r1 r2 = rat_mul r1 (rat_minv r2) 1063 *--------------------------------------------------------------------------*) 1064 1065val RAT_SUB_ADDAINV = store_thm( "RAT_SUB_ADDAINV",``!r1 r2. rat_sub r1 r2 = rat_add r1 (rat_ainv r2)``, 1066 REPEAT GEN_TAC THEN 1067 REWRITE_TAC[rat_sub_def, rat_add_def, rat_ainv_def] THEN 1068 REWRITE_TAC[frac_sub_def] THEN 1069 REWRITE_TAC[RAT_ADD_CONG] ); 1070 1071val RAT_DIV_MULMINV = store_thm("RAT_DIV_MULMINV", 1072 ``!r1 r2. rat_div r1 r2 = rat_mul r1 (rat_minv r2)``, 1073 REPEAT GEN_TAC THEN 1074 REWRITE_TAC[rat_div_def, rat_mul_def, rat_minv_def] THEN 1075 REWRITE_TAC[frac_div_def] THEN 1076 REWRITE_TAC[RAT_MUL_CONG] ); 1077 1078val RAT_DIV_0 = Q.store_thm( 1079 "RAT_DIV_0[simp]", 1080 ���rat_div 0 x = 0���, 1081 simp[RAT_DIV_MULMINV]); 1082 1083 1084(*-------------------------------------------------------------------------- 1085 RAT_AINV_0: thm 1086 |- rat_ainv 0q = 0q 1087 1088 RAT_AINV_AINV: thm 1089 |- !r1. rat_ainv (rat_ainv r1) = r1 1090 1091 RAT_AINV_ADD: thm 1092 |- ! r1 r2. rat_ainv (rat_add r1 r2) = rat_add (rat_ainv r1) (rat_ainv r2) 1093 1094 RAT_AINV_SUB: thm 1095 |- ! r1 r2. rat_ainv (rat_sub r1 r2) = rat_sub r2 r1 1096 1097 RAT_AINV_RMUL: thm 1098 |- !r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul r1 (rat_ainv r2) 1099 1100 RAT_AINV_LMUL: thm 1101 |- !r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul (rat_ainv r1) r2 1102 1103 RAT_AINV_MINV: thm 1104 |- !r1. ~(r1=0q) ==> (rat_ainv (rat_minv r1) = rat_minv (rat_ainv r1)) 1105 *--------------------------------------------------------------------------*) 1106 1107val RAT_AINV_0 = store_thm("RAT_AINV_0[simp]", ``rat_ainv 0q = 0q``, 1108 REWRITE_TAC[rat_0,rat_ainv_def] THEN 1109 RW_TAC int_ss[RAT_AINV_CONG] THEN 1110 RW_TAC int_ss[FRAC_AINV_0] ); 1111 1112val RAT_AINV_AINV = store_thm("RAT_AINV_AINV[simp]", 1113 ``!r1. rat_ainv (rat_ainv r1) = r1``, 1114 GEN_TAC THEN 1115 REWRITE_TAC[rat_ainv_def] THEN 1116 RW_TAC int_ss[RAT_AINV_CONG, FRAC_AINV_AINV, rat_thm] ); 1117 1118val RAT_AINV_ADD = store_thm("RAT_AINV_ADD", ``! r1 r2. rat_ainv (rat_add r1 r2) = rat_add (rat_ainv r1) (rat_ainv r2)``, 1119 REPEAT GEN_TAC THEN 1120 REWRITE_TAC[rat_add_def,rat_ainv_def] THEN 1121 REWRITE_TAC[RAT_ADD_CONG, RAT_AINV_CONG] THEN 1122 RW_TAC int_ss[FRAC_AINV_ADD] ); 1123 1124val RAT_AINV_SUB = store_thm("RAT_AINV_SUB", ``! r1 r2. rat_ainv (rat_sub r1 r2) = rat_sub r2 r1``, 1125 REPEAT GEN_TAC THEN 1126 REWRITE_TAC[RAT_SUB_ADDAINV] THEN 1127 REWRITE_TAC[RAT_AINV_ADD] THEN 1128 REWRITE_TAC[RAT_AINV_AINV] THEN 1129 PROVE_TAC[RAT_ADD_COMM] ); 1130 1131val RAT_AINV_RMUL = store_thm("RAT_AINV_RMUL", ``!r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul r1 (rat_ainv r2)``, 1132 REPEAT GEN_TAC THEN 1133 REWRITE_TAC[rat_ainv_def, rat_mul_def] THEN 1134 REWRITE_TAC[RAT_MUL_CONG, RAT_AINV_CONG] THEN 1135 PROVE_TAC[FRAC_AINV_RMUL] ); 1136 1137val RAT_AINV_LMUL = store_thm("RAT_AINV_LMUL", ``!r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul (rat_ainv r1) r2``, 1138 REPEAT GEN_TAC THEN 1139 REWRITE_TAC[rat_ainv_def, rat_mul_def] THEN 1140 REWRITE_TAC[RAT_MUL_CONG, RAT_AINV_CONG] THEN 1141 PROVE_TAC[FRAC_AINV_LMUL] ); 1142 1143(*-------------------------------------------------------------------------- 1144 RAT_EQ_AINV 1145 |- !r1 r2. (~r1 = ~r2) = (r1=r2) 1146 1147 RAT_AINV_EQ 1148 |- !r1 r2. (~r1 = r2) = (r1 = ~r2) 1149 *--------------------------------------------------------------------------*) 1150 1151val RAT_AINV_EQ = store_thm("RAT_AINV_EQ", 1152 ``!r1 r2. (rat_ainv r1 = r2) = (r1 = rat_ainv r2)``, 1153 REPEAT GEN_TAC THEN 1154 EQ_TAC THEN 1155 STRIP_TAC THEN 1156 BasicProvers.VAR_EQ_TAC THEN 1157 REWRITE_TAC[RAT_AINV_AINV] ); 1158 1159val RAT_EQ_AINV = store_thm("RAT_EQ_AINV[simp]", 1160 ``!r1 r2. (rat_ainv r1 = rat_ainv r2) = (r1=r2)``, 1161 REWRITE_TAC[RAT_AINV_EQ, RAT_AINV_AINV] ) ; 1162 1163val RAT_AINV_MINV = store_thm("RAT_AINV_MINV", 1164 ���!r1. r1 <> 0q ==> (rat_ainv (rat_minv r1) = rat_minv (rat_ainv r1))���, 1165 REPEAT STRIP_TAC THEN 1166 COPY_ASM_NO 0 THEN 1167 APPLY_ASM_TAC 0 (REWRITE_TAC[rat_nmr_def, RAT_EQ0_NMR]) THEN 1168 SUBST_TAC[GSYM RAT_AINV_0] THEN 1169 ONCE_REWRITE_TAC[GSYM RAT_AINV_EQ] THEN 1170 REWRITE_TAC[rat_nmr_def, RAT_EQ0_NMR] THEN 1171 REWRITE_TAC[rat_ainv_def, rat_minv_def] THEN 1172 REWRITE_TAC[RAT_NMREQ0_CONG] THEN 1173 STRIP_TAC THEN 1174 RW_TAC int_ss[RAT_AINV_CONG, RAT_MINV_CONG] THEN 1175 COPY_ASM_NO 1 THEN 1176 ONCE_REWRITE_TAC[GSYM INT_EQ_NEG] THEN 1177 ONCE_REWRITE_TAC[INT_NEG_0] THEN 1178 STRIP_TAC THEN 1179 FRAC_CALC_TAC THEN 1180 REWRITE_TAC[RAT_EQ] THEN 1181 FRAC_NMRDNM_TAC THEN 1182 RW_TAC int_ss[INT_ABS, SGN_def] THEN 1183 TRY (INT_RING_TAC THEN NO_TAC) THEN 1184 METIS_TAC[integerTheory.INT_LT_REFL, integerTheory.INT_LT_TRANS, 1185 integerTheory.INT_NOT_LT, integerTheory.INT_LE_ANTISYM, 1186 integerTheory.INT_MUL_RZERO]); 1187 1188(*-------------------------------------------------------------------------- 1189 RAT_SUB_RDISTRIB: thm 1190 |- !a b c. rat_mul (rat_sub a b) c = rat_sub (rat_mul a c) (rat_mul b c) 1191 1192 RAT_SUB_LDISTRIB: thm 1193 |- !a b c. rat_mul c (rat_sub a b) = rat_sub (rat_mul c a) (rat_mul c b) 1194 *--------------------------------------------------------------------------*) 1195 1196val RAT_SUB_RDISTRIB = store_thm("RAT_SUB_RDISTRIB", ``!a b c. rat_mul (rat_sub a b) c = rat_sub (rat_mul a c) (rat_mul b c)``, 1197 REPEAT GEN_TAC THEN 1198 REWRITE_TAC[RAT_SUB_ADDAINV] THEN 1199 REWRITE_TAC[RAT_AINV_LMUL] THEN 1200 PROVE_TAC[RAT_RDISTRIB] ); 1201 1202val RAT_SUB_LDISTRIB = store_thm("RAT_SUB_LDISTRIB", ``!a b c. rat_mul c (rat_sub a b) = rat_sub (rat_mul c a) (rat_mul c b)``, 1203 REPEAT GEN_TAC THEN 1204 REWRITE_TAC[RAT_SUB_ADDAINV] THEN 1205 REWRITE_TAC[RAT_AINV_RMUL] THEN 1206 PROVE_TAC[RAT_LDISTRIB] ); 1207 1208(*-------------------------------------------------------------------------- 1209 RAT_SUB_LID: thm 1210 |- !r1. rat_sub 0q r1 = rat_ainv r1 1211 1212 RAT_SUB_RID: thm 1213 |- !r1. rat_sub r1 0q = r1 1214 *--------------------------------------------------------------------------*) 1215 1216val RAT_SUB_LID = store_thm("RAT_SUB_LID[simp]", 1217 ``!r1. rat_sub 0q r1 = rat_ainv r1``, 1218 GEN_TAC THEN 1219 REWRITE_TAC[RAT_SUB_ADDAINV] THEN 1220 REWRITE_TAC[RAT_ADD_LID] ); 1221 1222val RAT_SUB_RID = store_thm("RAT_SUB_RID[simp]", 1223 ``!r1. rat_sub r1 0q = r1``, 1224 GEN_TAC THEN 1225 REWRITE_TAC[RAT_SUB_ADDAINV] THEN 1226 REWRITE_TAC[RAT_AINV_0] THEN 1227 RW_TAC int_ss[RAT_ADD_RID] ); 1228 1229(*-------------------------------------------------------------------------- 1230 RAT_SUB_ID: thm 1231 |- ! r. r - r = 0q 1232 *--------------------------------------------------------------------------*) 1233 1234val RAT_SUB_ID = store_thm("RAT_SUB_ID[simp]", 1235 ``! r. rat_sub r r = 0q``, 1236 RW_TAC bool_ss [RAT_SUB_ADDAINV, RAT_ADD_RINV]); 1237 1238(*-------------------------------------------------------------------------- 1239 RAT_EQ_SUB0: thm 1240 |- !r1 r2. (rat_sub r1 r2 = 0q) = (r1 = r2) 1241 *--------------------------------------------------------------------------*) 1242 1243val RAT_EQ_SUB0 = store_thm("RAT_EQ_SUB0", ``!r1 r2. (rat_sub r1 r2 = 0q) = (r1 = r2)``, 1244 REPEAT GEN_TAC THEN 1245 SUBST_TAC[SPEC ``r1:rat`` (GSYM RAT), SPEC ``r2:rat`` (GSYM RAT)] THEN 1246 REWRITE_TAC[RAT_SUB_CALCULATE, rat_0] THEN 1247 FRAC_CALC_TAC THEN 1248 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN 1249 FRAC_NMRDNM_TAC THEN 1250 RW_TAC int_ss[INT_MUL_CALCULATE, GSYM INT_SUB_CALCULATE, INT_SUB_0, INT_MUL_RID, INT_MUL_LZERO] ); 1251 1252(*-------------------------------------------------------------------------- 1253 RAT_EQ_0SUB: thm 1254 |- !r1 r2. (0q = rat_sub r1 r2) = (r1 = r2) 1255 *--------------------------------------------------------------------------*) 1256 1257val RAT_EQ_0SUB = store_thm("RAT_EQ_0SUB", ``!r1 r2. (0q = rat_sub r1 r2) = (r1 = r2)``, 1258 PROVE_TAC[RAT_EQ_SUB0] ); 1259 1260(*-------------------------------------------------------------------------- 1261 * signum function 1262 *--------------------------------------------------------------------------*) 1263 1264(*-------------------------------------------------------------------------- 1265 * RAT_SGN_CALCULATE: thm 1266 * |- rat_sgn (abs_rat( f1 ) = frac_sgn f1 1267 *--------------------------------------------------------------------------*) 1268 1269val RAT_SGN_CALCULATE = store_thm("RAT_SGN_CALCULATE", ``rat_sgn (abs_rat( f1 )) = frac_sgn f1``, 1270 REWRITE_TAC[rat_sgn_def, rat_0] THEN 1271 REWRITE_TAC[RAT_SGN_CONG] THEN 1272 REWRITE_TAC[frac_sgn_def, frac_0_def] THEN 1273 FRAC_NMRDNM_TAC THEN 1274 REWRITE_TAC[SGN_def] ); 1275 1276(*-------------------------------------------------------------------------- 1277 RAT_SGN_CLAUSES: thm 1278 |- !r1. 1279 ((rat_sgn r1 = ~1) = (r1 < 0q)) /\ 1280 ((rat_sgn r1 = 0i) = (r1 = 0q) ) /\ 1281 ((rat_sgn r1 = 1i) = (r1 > 0q)) 1282 *--------------------------------------------------------------------------*) 1283 1284val RAT_SGN_CLAUSES = store_thm("RAT_SGN_CLAUSES", 1285 ``!r1. ((rat_sgn r1 = ~1) = (rat_les r1 0q)) /\ 1286 ((rat_sgn r1 = 0i) = (r1 = 0q)) /\ 1287 ((rat_sgn r1 = 1i) = (rat_gre r1 0q))``, 1288 GEN_TAC THEN 1289 REWRITE_TAC[rat_sgn_def, rat_les_def, rat_gre_def] THEN 1290 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_ADD_LID, RAT_SUB_RID] THEN 1291 RAT_CALC_TAC THEN 1292 REWRITE_TAC[RAT_SGN_CONG] THEN 1293 REPEAT CONJ_TAC THENL 1294 [ 1295 EQ_TAC THEN 1296 STRIP_TAC THEN 1297 PROVE_TAC[FRAC_SGN_AINV, INT_NEG_EQ] 1298 , 1299 REWRITE_TAC[frac_sgn_def, frac_0_def] THEN 1300 REWRITE_TAC[RAT_EQ] THEN 1301 FRAC_NMRDNM_TAC THEN 1302 PROVE_TAC[INT_SGN_CLAUSES] 1303 ] ); 1304 1305(*-------------------------------------------------------------------------- 1306 RAT_SGN_0: thm 1307 |- rat_sgn 0q = 0i 1308 *--------------------------------------------------------------------------*) 1309 1310val RAT_SGN_0 = store_thm("RAT_SGN_0[simp]", 1311 ``rat_sgn 0q = 0i``, 1312 REWRITE_TAC[rat_sgn_def, rat_0] THEN REWRITE_TAC[RAT_SGN_CONG] THEN 1313 REWRITE_TAC[frac_sgn_def, frac_0_def] THEN 1314 FRAC_NMRDNM_TAC THEN REWRITE_TAC[SGN_def] ); 1315 1316(*-------------------------------------------------------------------------- 1317 RAT_SGN_AINV: thm 1318 |- !r1. ~rat_sgn ~r1 = rat_sgn r1 1319 *--------------------------------------------------------------------------*) 1320 1321val RAT_SGN_AINV = store_thm("RAT_SGN_AINV", ``!r1. ~rat_sgn (rat_ainv r1) = rat_sgn r1``, 1322 GEN_TAC THEN 1323 REWRITE_TAC[rat_sgn_def, rat_ainv_def] THEN 1324 REWRITE_TAC[RAT_SGN_CONG] THEN 1325 PROVE_TAC[FRAC_SGN_AINV] ); 1326 1327(*-------------------------------------------------------------------------- 1328 RAT_SGN_MUL: thm 1329 |- !r1 r2. rat_sgn (r1 * r2) = rat_sgn r1 * rat_sgn r2 1330 *--------------------------------------------------------------------------*) 1331 1332val RAT_SGN_MUL = store_thm("RAT_SGN_MUL[simp]", 1333 ``!r1 r2. rat_sgn (rat_mul r1 r2) = rat_sgn r1 * rat_sgn r2``, 1334 REPEAT GEN_TAC THEN REWRITE_TAC[rat_sgn_def, rat_mul_def] THEN 1335 REWRITE_TAC[RAT_SGN_CONG] THEN PROVE_TAC[FRAC_SGN_MUL2] ); 1336 1337(*-------------------------------------------------------------------------- 1338 RAT_SGN_MINV: thm 1339 |- !r1. ~(r1 = 0q) ==> (rat_sgn (rat_minv r1) = rat_sgn r1) 1340 *--------------------------------------------------------------------------*) 1341 1342val RAT_SGN_MINV = store_thm("RAT_SGN_MINV[simp]", 1343 ``!r1. ~(r1 = 0q) ==> (rat_sgn (rat_minv r1) = rat_sgn r1)``, 1344 GEN_TAC THEN STRIP_TAC THEN 1345 REWRITE_TAC[rat_sgn_def, rat_minv_def] THEN 1346 MATCH_MP_TAC (SPEC ``rep_rat r1`` FRAC_SGN_CASES) THEN 1347 REPEAT CONJ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN 1348 UNDISCH_ALL_TAC THEN REWRITE_TAC[RAT_EQ0_NMR, rat_nmr_def] THEN STRIP_TAC THEN 1349 REWRITE_TAC[frac_sgn_def, frac_minv_def, INT_SGN_CLAUSES] THEN 1350 STRIP_TAC THEN 1351 REWRITE_TAC[RAT_NMREQ0_CONG, RAT_NMRGT0_CONG, RAT_NMRLT0_CONG] THEN 1352 FRAC_NMRDNM_TAC THEN 1353 RW_TAC int_ss 1354 [INT_MUL_SIGN_CASES, SGN_def, FRAC_DNMPOS, INT_MUL_LID, int_gt] THEN 1355 PROVE_TAC[INT_LT_ANTISYM, int_gt] ); 1356 1357(*-------------------------------------------------------------------------- 1358 RAT_SGN_TOTAL 1359 |- !r1. (rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i) 1360 *--------------------------------------------------------------------------*) 1361 1362val RAT_SGN_TOTAL = store_thm("RAT_SGN_TOTAL", 1363 ``!r1. (rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i)``, 1364 REWRITE_TAC[rat_sgn_def] THEN 1365 REWRITE_TAC[frac_sgn_def, SGN_def] THEN 1366 PROVE_TAC[] ); 1367 1368(*-------------------------------------------------------------------------- 1369 RAT_SGN_COMPLEMENT 1370 |- !r1. 1371 (~(rat_sgn r1 = ~1) = ((rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i))) /\ 1372 (~(rat_sgn r1 = 0) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 1i))) /\ 1373 (~(rat_sgn r1 = 1) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0))) 1374 *--------------------------------------------------------------------------*) 1375 1376val RAT_SGN_COMPLEMENT = store_thm("RAT_SGN_COMPLEMENT", 1377 ``!r1. (~(rat_sgn r1 = ~1) = ((rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i))) /\ 1378 (~(rat_sgn r1 = 0) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 1i))) /\ 1379 (~(rat_sgn r1 = 1) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0)))``, 1380 GEN_TAC THEN REPEAT CONJ_TAC THEN 1381 ASSUME_TAC (SPEC ``r1:rat`` RAT_SGN_TOTAL) THEN 1382 UNDISCH_ALL_TAC THEN STRIP_TAC THEN 1383 RW_TAC int_ss [RAT_1_NOT_0] ); 1384 1385(*========================================================================== 1386 * order of the rational numbers (less, greater, ...) 1387 *==========================================================================*) 1388 1389(*-------------------------------------------------------------------------- 1390 RAT_LES_REF, RAT_LES_ANTISYM, RAT_LES_TRANS, RAT_LES_TOTAL 1391 1392 |- !r1. ~(r1 < r1) 1393 |- ! r1 r2. r1 < r2 ==> ~(r2 < r1) 1394 |- !r1 r2 r3. r1 < r2 /\ r2 < r3 ==> r1 < r3 1395 |- !r1 r2. r1 < r2 \/ (r1 = r2) \/ r2 < r1 1396 *--------------------------------------------------------------------------*) 1397 1398val RAT_LES_REF = store_thm("RAT_LES_REF", ``!r1. ~(rat_les r1 r1)``, 1399 REWRITE_TAC[rat_les_def] THEN 1400 REWRITE_TAC[RAT_SUB_ID] THEN 1401 RW_TAC int_ss[RAT_SGN_0] ); 1402 1403val RAT_LES_ANTISYM = 1404let 1405 val lemmaX = prove(``!f. frac_sgn (frac_ainv f) = ~frac_sgn f``, 1406 REWRITE_TAC[GSYM INT_NEG_EQ] THEN 1407 RW_TAC int_ss[FRAC_SGN_NEG] ); 1408in 1409 store_thm( 1410 "RAT_LES_ANTISYM", 1411 ``!r1 r2. rat_les r1 r2 ==> ~(rat_les r2 r1)``, 1412 REPEAT GEN_TAC THEN 1413 REWRITE_TAC[rat_les_def, rat_sgn_def, rat_sub_def] THEN 1414 REWRITE_TAC[RAT_SGN_CONG] THEN 1415 SUBST_TAC[SPECL [``rep_rat r1``, ``rep_rat r2``] (GSYM FRAC_AINV_SUB)] THEN 1416 REWRITE_TAC[lemmaX] THEN REWRITE_TAC[INT_NEG_EQ] THEN RW_TAC int_ss[] ) 1417end; 1418 1419val RAT_LES_TRANS = store_thm("RAT_LES_TRANS", 1420 ``!r1 r2 r3. rat_les r1 r2 /\ rat_les r2 r3 ==> rat_les r1 r3``, 1421 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def] THEN 1422 SUBGOAL_THEN 1423 ``rat_sub r3 r1 = rat_add (rat_sub r3 r2) (rat_sub r2 r1)`` 1424 SUBST1_TAC THEN1 1425 RAT_CALCEQ_TAC THEN REWRITE_TAC[rat_sgn_def, rat_sub_def, rat_add_def] THEN 1426 REWRITE_TAC[RAT_ADD_CONG, RAT_SUB_CONG] THEN 1427 REWRITE_TAC[RAT_SGN_CONG] THEN REWRITE_TAC[frac_sgn_def] THEN 1428 FRAC_CALC_TAC THEN FRAC_NMRDNM_TAC THEN 1429 REWRITE_TAC[INT_SGN_CLAUSES] THEN REWRITE_TAC[int_gt] THEN 1430 FRAC_POS_TAC ``frac_dnm (rep_rat r2) * frac_dnm (rep_rat r1)`` THEN 1431 FRAC_POS_TAC ``frac_dnm (rep_rat r3) * frac_dnm (rep_rat r2)`` THEN 1432 REPEAT STRIP_TAC THEN 1433 PROVE_TAC[INT_LT_ADD,INT_MUL_POS_SIGN] ); 1434 1435val RAT_LES_TOTAL = store_thm("RAT_LES_TOTAL", 1436 ``!r1 r2. rat_les r1 r2 \/ (r1 = r2) \/ rat_les r2 r1``, 1437 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def] THEN 1438 SUBST_TAC[SPECL[``r1:rat``,``r2:rat``] (GSYM RAT_AINV_SUB)] THEN 1439 SUBST_TAC[ 1440 SPECL[``rat_sgn (rat_ainv (rat_sub r1 r2))``,``1i``] (GSYM INT_EQ_NEG)] THEN 1441 REWRITE_TAC[RAT_SGN_AINV] THEN 1442 ONCE_REWRITE_TAC[GSYM RAT_EQ_SUB0] THEN 1443 SUBST_TAC[ 1444 CONJUNCT1 (CONJUNCT2 (SPEC ``rat_sub r1 r2`` (GSYM RAT_SGN_CLAUSES)))] THEN 1445 PROVE_TAC[RAT_SGN_TOTAL] ); 1446 1447 1448(*-------------------------------------------------------------------------- 1449 RAT_LEQ_REF, RAT_LEQ_ANTISYM, RAT_LEQ_TRANS 1450 |- !r1. r1 <= r1 1451 |- !r1 r2. r1 <= r2 = r2 >= r1 1452 |- !r1 r2 r3. r1 <= r2 /\ r2 <= r3 ==> r1 <= r3 1453 *--------------------------------------------------------------------------*) 1454 1455val RAT_LEQ_REF = store_thm("RAT_LEQ_REF", ``!r1. rat_leq r1 r1``, 1456 GEN_TAC THEN 1457 REWRITE_TAC[rat_leq_def] THEN 1458 REWRITE_TAC[RAT_SUB_ID] THEN 1459 REWRITE_TAC[rat_sgn_def,rat_0] THEN 1460 REWRITE_TAC[frac_sgn_def,SGN_def, frac_0_def] THEN 1461 REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG] THEN 1462 RW_TAC int_ss[NMR,DNM] ); 1463 1464val RAT_LEQ_ANTISYM = store_thm("RAT_LEQ_ANTISYM", 1465 ``!r1 r2. rat_leq r1 r2 /\ rat_leq r2 r1 ==> (r1=r2)``, 1466 REPEAT GEN_TAC THEN 1467 REWRITE_TAC[rat_leq_def] THEN 1468 RW_TAC bool_ss [] THEN 1469 PROVE_TAC[RAT_LES_ANTISYM]); 1470 1471val RAT_LEQ_TRANS = store_thm("RAT_LEQ_TRANS", 1472 ``!r1 r2 r3. rat_leq r1 r2 /\ rat_leq r2 r3 ==> rat_leq r1 r3``, 1473 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN 1474 RW_TAC bool_ss [] THEN PROVE_TAC[RAT_LES_TRANS]); 1475 1476 1477(*-------------------------------------------------------------------------- 1478 RAT_LES_01 1479 |- 0q < 1q 1480 *--------------------------------------------------------------------------*) 1481 1482val RAT_LES_01 = store_thm("RAT_LES_01", ``rat_les 0q 1q``, 1483 REWRITE_TAC[rat_les_def] THEN 1484 RAT_CALC_TAC THEN 1485 FRAC_CALC_TAC THEN 1486 REWRITE_TAC[rat_sgn_def, frac_sgn_def, SGN_def] THEN 1487 REWRITE_TAC[RAT_NMREQ0_CONG, RAT_NMRLT0_CONG] THEN 1488 FRAC_NMRDNM_TAC ); 1489 1490(*-------------------------------------------------------------------------- 1491 RAT_LES_IMP_LEQ 1492 |- !r1 r2. r1 < r2 ==> r1 <= r2 1493 *--------------------------------------------------------------------------*) 1494 1495val RAT_LES_IMP_LEQ = store_thm("RAT_LES_IMP_LEQ", 1496 ``!r1 r2. rat_les r1 r2 ==> rat_leq r1 r2``, 1497 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def, rat_leq_def] THEN 1498 RW_TAC bool_ss [] ); 1499 1500(*-------------------------------------------------------------------------- 1501 RAT_LES_IMP_NEQ 1502 |- !r1 r2. r1 < r2 ==> ~(r1 = r2) 1503 *--------------------------------------------------------------------------*) 1504 1505val RAT_LES_IMP_NEQ = store_thm("RAT_LES_IMP_NEQ", 1506 ``!r1 r2. rat_les r1 r2 ==> ~(r1 = r2)``, 1507 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def] THEN 1508 SUBST_TAC[ISPECL[``r1:rat``,``r2:rat``] EQ_SYM_EQ] THEN 1509 ONCE_REWRITE_TAC[GSYM RAT_EQ_SUB0] THEN 1510 SUBST_TAC[ 1511 CONJUNCT1 (CONJUNCT2 (SPEC ``rat_sub r2 r1`` (GSYM RAT_SGN_CLAUSES)))] THEN 1512 SIMP_TAC int_ss []); 1513 1514(*-------------------------------------------------------------------------- 1515 RAT_LEQ_LES (RAT_NOT_LES_LEQ) 1516 |- !r1 r2. ~(r2 < r1) = r1 <= r2 1517 *--------------------------------------------------------------------------*) 1518 1519val RAT_LEQ_LES = store_thm("RAT_LEQ_LES", 1520 ``!r1 r2. ~(rat_les r2 r1) = rat_leq r1 r2``, 1521 RW_TAC bool_ss[rat_leq_def] THEN 1522 PROVE_TAC[RAT_LES_TOTAL, RAT_LES_ANTISYM] ); 1523 1524(*-------------------------------------------------------------------------- 1525 RAT_LES_LEQ, RAT_LES_LEQ2 1526 1527 |- !r1 r2. ~(rat_leq r2 r1) = r1 < r2 1528 |- !r1 r2. r1 < r2 = r1 <= r2 /\ ~(r2 = r1) 1529 *--------------------------------------------------------------------------*) 1530 1531val RAT_LES_LEQ = store_thm("RAT_LES_LEQ", 1532 ``!r1 r2. ~(rat_leq r2 r1) = rat_les r1 r2``, 1533 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN 1534 PROVE_TAC[RAT_LES_TOTAL, RAT_LES_IMP_NEQ, RAT_LES_ANTISYM] ); 1535 1536val RAT_LES_LEQ2 = store_thm("RAT_LES_LEQ2", 1537 ``!r1 r2. rat_les r1 r2 = rat_leq r1 r2 /\ ~(rat_leq r2 r1)``, 1538 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN EQ_TAC THEN 1539 RW_TAC bool_ss [] THEN PROVE_TAC[RAT_LES_ANTISYM, RAT_LES_IMP_NEQ] ); 1540 1541(*-------------------------------------------------------------------------- 1542 RAT_LES_LEQ_TRANS, RAT_LEQ_LES_TRANS 1543 1544 |- !a b c. a < b /\ b <= c ==> a < c 1545 |- !a b c. a <= b /\ b < c ==> a < c 1546 *--------------------------------------------------------------------------*) 1547 1548val RAT_LES_LEQ_TRANS = store_thm("RAT_LES_LEQ_TRANS", 1549 ``!a b c. rat_les a b /\ rat_leq b c ==> rat_les a c``, 1550 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN 1551 PROVE_TAC[RAT_LES_TRANS] ); 1552 1553val RAT_LEQ_LES_TRANS = store_thm("RAT_LEQ_LES_TRANS", 1554 ``!a b c. rat_leq a b /\ rat_les b c ==> rat_les a c``, 1555 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN PROVE_TAC[RAT_LES_TRANS] ); 1556 1557(*-------------------------------------------------------------------------- 1558 RAT_0LES_0LES_ADD, RAT_LES0_LES0_ADD 1559 1560 |- !r1 r2. 0q < r1 ==> 0q < r2 ==> 0q < r1 + r2 1561 |- !r1 r2. r1 < 0q ==> r2 < 0q ==> r1 + r2 < 0q 1562 *--------------------------------------------------------------------------*) 1563 1564val RAT_0LES_0LES_ADD = store_thm("RAT_0LES_0LES_ADD", 1565 ``!r1 r2. rat_les 0q r1 ==> rat_les 0q r2 ==> rat_les 0q (rat_add r1 r2)``, 1566 REPEAT GEN_TAC THEN REWRITE_TAC[RAT_0LES_NMR] THEN 1567 RAT_CALC_TAC THEN FRAC_CALC_TAC THEN 1568 REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRGT0_CONG, (GSYM int_gt)] THEN 1569 FRAC_NMRDNM_TAC THEN REWRITE_TAC[int_gt] THEN 1570 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN 1571 FRAC_POS_TAC ``frac_dnm (rep_rat r2)`` THEN 1572 REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD] ); 1573 1574val RAT_LES0_LES0_ADD = store_thm("RAT_LES0_LES0_ADD", 1575 ``!r1 r2. rat_les r1 0q ==> rat_les r2 0q ==> rat_les (rat_add r1 r2) 0q``, 1576 REPEAT GEN_TAC THEN REWRITE_TAC[RAT_LES0_NMR] THEN 1577 RAT_CALC_TAC THEN FRAC_CALC_TAC THEN 1578 REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRLT0_CONG] THEN 1579 FRAC_NMRDNM_TAC THEN REWRITE_TAC[int_gt] THEN 1580 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN 1581 FRAC_POS_TAC ``frac_dnm (rep_rat r2)`` THEN 1582 REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD_NEG] ); 1583 1584(*-------------------------------------------------------------------------- 1585 RAT_0LES_0LEQ_ADD, RAT_LES0_LEQ0_ADD 1586 1587 |- !r1 r2. 0q < r1 ==> 0q <= r2 ==> 0q < r1 + r2 1588 |- !r1 r2. r1 < 0q ==> r2 <= 0q ==> r1 + r2 < 0q 1589 *--------------------------------------------------------------------------*) 1590 1591val RAT_0LES_0LEQ_ADD = store_thm("RAT_0LES_0LEQ_ADD", 1592 ``!r1 r2. rat_les 0q r1 ==> rat_leq 0q r2 ==> rat_les 0q (rat_add r1 r2)``, 1593 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN RW_TAC bool_ss [] THEN 1594 PROVE_TAC[RAT_0LES_0LES_ADD, RAT_ADD_RID] ); 1595 1596 1597val RAT_LES0_LEQ0_ADD = store_thm("RAT_LES0_LEQ0_ADD", 1598 ``!r1 r2. rat_les r1 0q ==> rat_leq r2 0q ==> rat_les (rat_add r1 r2) 0q``, 1599 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN RW_TAC bool_ss [] THEN 1600 PROVE_TAC[RAT_LES0_LES0_ADD, RAT_ADD_RID] ); 1601 1602(*-------------------------------------------------------------------------- 1603 RAT_LSUB_EQ, RAT_RSUB_EQ 1604 1605 |- !r1 r2 r3. (r1 - r2 = r3) = (r1 = r2 + r3) 1606 |- !r1 r2 r3. (r1 = r2 - r3) = (r1 + r3 = r2) 1607 *--------------------------------------------------------------------------*) 1608 1609val RAT_LSUB_EQ = store_thm("RAT_LSUB_EQ", 1610 ``!r1 r2 r3. (rat_sub r1 r2 = r3) = (r1 = rat_add r2 r3)``, 1611 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN BasicProvers.VAR_EQ_TAC THEN 1612 REWRITE_TAC[RAT_SUB_ADDAINV] THEN ONCE_REWRITE_TAC[RAT_ADD_COMM] THENL [ 1613 ONCE_REWRITE_TAC[GSYM RAT_ADD_ASSOC] 1614 , 1615 ONCE_REWRITE_TAC[RAT_ADD_ASSOC] 1616 ] THEN 1617 REWRITE_TAC[RAT_ADD_LINV] THEN REWRITE_TAC[RAT_ADD_LID, RAT_ADD_RID] ); 1618 1619val RAT_RSUB_EQ = store_thm("RAT_RSUB_EQ", 1620 ``!r1 r2 r3. (r1 = rat_sub r2 r3) = (rat_add r1 r3 = r2)``, 1621 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN BasicProvers.VAR_EQ_TAC THEN 1622 REWRITE_TAC[RAT_SUB_ADDAINV] THEN ONCE_REWRITE_TAC[GSYM RAT_ADD_ASSOC] THEN 1623 REWRITE_TAC[RAT_ADD_LINV, RAT_ADD_RINV] THEN 1624 REWRITE_TAC[RAT_ADD_LID, RAT_ADD_RID] ); 1625 1626(*-------------------------------------------------------------------------- 1627 RAT_LDIV_EQ, RAT_RDIV_EQ 1628 1629 |- !r1 r2 r3. ~(r2 = 0q) ==> ((r1 / r2 = r3) = (r1 = r2 * r3)) 1630 |- !r1 r2 r3. ~(r3 = 0q) ==> ((r1 = r2 / r3) = (r1 * r3 = r2)) 1631 *--------------------------------------------------------------------------*) 1632 1633val RAT_LDIV_EQ = store_thm("RAT_LDIV_EQ", 1634 ``!r1 r2 r3. ~(r2 = 0q) ==> ((rat_div r1 r2 = r3) = (r1 = rat_mul r2 r3))``, 1635 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN 1636 BasicProvers.VAR_EQ_TAC THEN 1637 ONCE_REWRITE_TAC [RAT_MUL_COMM] THEN 1638 REWRITE_TAC [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC] THEN 1639 ASM_SIMP_TAC std_ss [RAT_MUL_RINV, RAT_MUL_LINV, RAT_MUL_RID, RAT_MUL_LID]) ; 1640 1641val RAT_RDIV_EQ = store_thm("RAT_RDIV_EQ", 1642 ``!r1 r2 r3. ~(r3 = 0q) ==> ((r1 = rat_div r2 r3) = (rat_mul r1 r3 = r2))``, 1643 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN 1644 BasicProvers.VAR_EQ_TAC THEN 1645 REWRITE_TAC [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC] THEN 1646 ASM_SIMP_TAC std_ss [RAT_MUL_RINV, RAT_MUL_LINV, RAT_MUL_RID, RAT_MUL_LID]) ; 1647 1648 1649(*========================================================================== 1650 * one-to-one and onto theorems 1651 *==========================================================================*) 1652 1653(*-------------------------------------------------------------------------- 1654 RAT_AINV_ONE_ONE 1655 1656 |- ONE_ONE rat_ainv 1657 *--------------------------------------------------------------------------*) 1658 1659val RAT_AINV_ONE_ONE = store_thm("RAT_AINV_ONE_ONE", ``ONE_ONE rat_ainv``, 1660 REWRITE_TAC[ONE_ONE_DEF] THEN 1661 BETA_TAC THEN 1662 REWRITE_TAC[RAT_EQ_AINV] ); 1663 1664(*-------------------------------------------------------------------------- 1665 RAT_ADD_ONE_ONE 1666 1667 |- !r1. ONE_ONE (rat_add r1) 1668 *--------------------------------------------------------------------------*) 1669 1670val RAT_ADD_ONE_ONE = store_thm("RAT_ADD_ONE_ONE", 1671 ``!r1. ONE_ONE (rat_add r1)``, 1672 REPEAT GEN_TAC THEN 1673 SIMP_TAC std_ss [ONE_ONE_DEF, GSYM RAT_LSUB_EQ] THEN 1674 SIMP_TAC std_ss [RAT_RSUB_EQ] THEN 1675 MATCH_ACCEPT_TAC RAT_ADD_COMM) ; 1676 1677(*-------------------------------------------------------------------------- 1678 RAT_MUL_ONE_ONE 1679 1680 |- !r1. ~(r1=0q) = ONE_ONE (rat_mul r1) 1681 *--------------------------------------------------------------------------*) 1682 1683val RAT_MUL_ONE_ONE = store_thm("RAT_MUL_ONE_ONE", 1684 ``!r1. ~(r1=0q) = ONE_ONE (rat_mul r1)``, 1685 REPEAT GEN_TAC THEN REWRITE_TAC [ONE_ONE_DEF] THEN BETA_TAC THEN 1686 EQ_TAC THEN REPEAT DISCH_TAC 1687 THENL [ 1688 ASM_SIMP_TAC std_ss [GSYM RAT_LDIV_EQ] THEN 1689 ASM_SIMP_TAC std_ss [RAT_RDIV_EQ] THEN 1690 MATCH_ACCEPT_TAC RAT_MUL_COMM, 1691 FIRST_X_ASSUM (ASSUME_TAC o Q.SPECL [`1q`, `0q`]) THEN 1692 REV_FULL_SIMP_TAC std_ss [RAT_1_NOT_0, RAT_MUL_LZERO] ]) ; 1693 1694(*========================================================================== 1695 * transformation of equations 1696 *==========================================================================*) 1697 1698(*-------------------------------------------------------------------------- 1699 RAT_EQ_LADD, RAT_EQ_RADD 1700 1701 |- !r1 r2 r3. (r3 + r1 = r3 + r2) = (r1=r2) 1702 |- !r1 r2 r3. (r1 + r3 = r2 + r3) = (r1=r2) 1703 *--------------------------------------------------------------------------*) 1704 1705val RAT_EQ_LADD = store_thm("RAT_EQ_LADD", ``!r1 r2 r3. (rat_add r3 r1 = rat_add r3 r2) = (r1=r2)``, 1706 PROVE_TAC [REWRITE_RULE[ONE_ONE_THM] RAT_ADD_ONE_ONE, RAT_ADD_COMM] ); 1707 1708val RAT_EQ_RADD = store_thm("RAT_EQ_RADD", ``!r1 r2 r3. (rat_add r1 r3 = rat_add r2 r3) = (r1=r2)``, 1709 PROVE_TAC [REWRITE_RULE[ONE_ONE_THM] RAT_ADD_ONE_ONE, RAT_ADD_COMM] ); 1710 1711(*-------------------------------------------------------------------------- 1712 RAT_EQ_LMUL, RAT_EQ_RMUL 1713 1714 |- !r1 r2 r3. ~(r3=0q) ==> ((r3 * r1 = r3 * r2) = (r1=r2)) 1715 |- !r1 r2 r3. ~(r3=0q) ==> ((r1 * r3 = r2 * r3) = (r1=r2)) 1716 *--------------------------------------------------------------------------*) 1717 1718val RAT_EQ_RMUL = store_thm("RAT_EQ_RMUL", ``!r1 r2 r3. ~(r3=0q) ==> ((rat_mul r1 r3 = rat_mul r2 r3) = (r1=r2))``, 1719 REPEAT GEN_TAC THEN 1720 REWRITE_TAC[SPEC ``r3:rat`` RAT_MUL_ONE_ONE] THEN 1721 REWRITE_TAC[ONE_ONE_THM] THEN 1722 STRIP_TAC THEN 1723 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN 1724 PROVE_TAC[] ); 1725 1726val RAT_EQ_LMUL = store_thm("RAT_EQ_LMUL", ``!r1 r2 r3. ~(r3=0q) ==> ((rat_mul r3 r1 = rat_mul r3 r2) = (r1=r2))``, 1727 PROVE_TAC[RAT_EQ_RMUL, RAT_MUL_COMM] ); 1728 1729(*========================================================================== 1730 * transformation of inequations 1731 *==========================================================================*) 1732 1733(*-------------------------------------------------------------------------- 1734 RAT_LES_LADD, RAT_LES_RADD, RAT_LEQ_LADD, RAT_LEQ_RADD 1735 1736 |- !r1 r2 r3. (r3 + r1) < (r3 + r2) = r1 < r2 1737 |- !r1 r2 r3. (r1 + r3) < (r2 + r3) = r1 < r2 1738 |- !r1 r2 r3. (r3 + r1) <= (r3 + r2) = r1 <= r2 1739 |- !r1 r2 r3. (r1 + r3) <= (r2 + r3) = r1 <= r2 1740 *--------------------------------------------------------------------------*) 1741 1742val RAT_LES_RADD = store_thm("RAT_LES_RADD", ``!r1 r2 r3. rat_les (rat_add r1 r3) (rat_add r2 r3) = rat_les r1 r2``, 1743 REPEAT GEN_TAC THEN 1744 REWRITE_TAC[rat_les_def, rat_sgn_def] THEN 1745 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_AINV_ADD] THEN 1746 SUBST_TAC[ EQT_ELIM (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add r2 r3) (rat_add (rat_ainv r1) (rat_ainv r3)) = rat_add (rat_add r2 (rat_ainv r1)) (rat_add r3 (rat_ainv r3))``) ] THEN 1747 REWRITE_TAC[RAT_ADD_RINV, RAT_ADD_RID] ); 1748 1749val RAT_LES_LADD = store_thm("RAT_LES_LADD", ``!r1 r2 r3. rat_les (rat_add r3 r1) (rat_add r3 r2) = rat_les r1 r2``, 1750 PROVE_TAC[RAT_LES_RADD, RAT_ADD_COMM] ); 1751 1752val RAT_LEQ_RADD = store_thm("RAT_LEQ_RADD", 1753 ``!r1 r2 r3. rat_leq (rat_add r1 r3) (rat_add r2 r3) = rat_leq r1 r2``, 1754 REWRITE_TAC[rat_leq_def, RAT_LES_RADD, RAT_EQ_RADD]) ; 1755 1756val RAT_LEQ_LADD = store_thm("RAT_LEQ_LADD", 1757 ``!r1 r2 r3. rat_leq (rat_add r3 r1) (rat_add r3 r2) = rat_leq r1 r2``, 1758 REWRITE_TAC[rat_leq_def, RAT_LES_LADD, RAT_EQ_LADD]) ; 1759 1760val RAT_ADD_MONO = Q.store_thm ("RAT_ADD_MONO", 1761 `!a b c d. a <= b /\ c <= d ==> rat_add a c <= rat_add b d`, 1762 REPEAT STRIP_TAC THEN irule RAT_LEQ_TRANS THEN 1763 Q.EXISTS_TAC `b + c` THEN 1764 ASM_SIMP_TAC std_ss [RAT_LEQ_LADD, RAT_LEQ_RADD]) ; 1765 1766(*-------------------------------------------------------------------------- 1767 RAT_LES_AINV 1768 1769 |- !r1 r2. ~r1 < ~r2 = r2 < r1 1770 *--------------------------------------------------------------------------*) 1771 1772val RAT_LES_AINV = store_thm("RAT_LES_AINV", ``!r1 r2. rat_les (rat_ainv r1) (rat_ainv r2) = rat_les r2 r1``, 1773 REPEAT GEN_TAC THEN 1774 SUBST_TAC[ SPECL[``rat_ainv r1``,``rat_ainv r2``,``r1:rat``] (GSYM RAT_LES_RADD)] THEN 1775 SUBST_TAC[ SPECL[``rat_add (rat_ainv r1) r1``,``rat_add (rat_ainv r2) r1``,``r2:rat``] (GSYM RAT_LES_RADD)] THEN 1776 SUBST_TAC[ EQT_ELIM (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add (rat_ainv r2) r1) r2 = rat_add (rat_add (rat_ainv r2) r2) r1``) ] THEN 1777 REWRITE_TAC[RAT_ADD_LINV, RAT_ADD_LID] ); 1778 1779(*-------------------------------------------------------------------------- 1780 RAT_LSUB_LES, RAT_RSUB_LES 1781 1782 |- !r1 r2 r3. (r1 - r2) < r3 = r1 < (r2 + r3) 1783 |- !r1 r2 r3. r1 < (r2 - r3) = (r1 + r3) < r2 1784 *--------------------------------------------------------------------------*) 1785 1786val RAT_LSUB_LES = store_thm("RAT_LSUB_LES", ``!r1 r2 r3. rat_les (rat_sub r1 r2) r3 = rat_les r1 (rat_add r2 r3)``, 1787 REPEAT GEN_TAC THEN 1788 REWRITE_TAC[rat_les_def] THEN 1789 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_AINV_ADD, RAT_AINV_AINV] THEN 1790 PROVE_TAC [AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add r3 (rat_add (rat_ainv r1) r2) = rat_add (rat_add r2 r3) (rat_ainv r1)``] ); 1791 1792val RAT_RSUB_LES = store_thm("RAT_RSUB_LES", ``!r1 r2 r3. rat_les r1 (rat_sub r2 r3) = rat_les (rat_add r1 r3) r2``, 1793 REPEAT GEN_TAC THEN 1794 REWRITE_TAC[rat_les_def] THEN 1795 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_AINV_ADD] THEN 1796 PROVE_TAC [AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add r2 (rat_ainv r3)) (rat_ainv r1) = rat_add r2 (rat_add (rat_ainv r1) (rat_ainv r3))``] ); 1797 1798val RAT_LSUB_LEQ = store_thm("RAT_LSUB_LEQ", 1799 ``!r1 r2 r3. rat_leq (rat_sub r1 r2) r3 = rat_leq r1 (rat_add r2 r3)``, 1800 REWRITE_TAC[rat_leq_def, RAT_LSUB_LES, RAT_LSUB_EQ]) ; 1801 1802val RAT_RSUB_LEQ = store_thm("RAT_RSUB_LEQ", 1803 ``!r1 r2 r3. rat_leq r1 (rat_sub r2 r3) = rat_leq (rat_add r1 r3) r2``, 1804 REWRITE_TAC[rat_leq_def, RAT_RSUB_LES, RAT_RSUB_EQ]) ; 1805 1806(*-------------------------------------------------------------------------- 1807 RAT_LES_LMUL_NEG RAT_LES_LMUL_POS RAT_LES_RMUL_POS RAT_LES_RMUL_NEG 1808 1809 |- !r1 r2 r3. r3 < 0q ==> (r3 * r2 < r3 * r1) = r1 < r2) 1810 |- !r1 r2 r3. 0q < r3 ==> (r3 * r1 < r3 * r2) = r1 < r2) 1811 |- !r1 r2 r3. 0q < r3 ==> (r1 * r3 < r2 * r3) = r1 < r2) 1812 |- !r1 r2 r3. r3 < 0q ==> (r2 * r3 < r1 * r3) = r1 < r2) 1813 *--------------------------------------------------------------------------*) 1814 1815val RAT_LES_RMUL_POS = store_thm("RAT_LES_RMUL_POS", ``!r1 r2 r3. rat_les 0q r3 ==> (rat_les (rat_mul r1 r3) (rat_mul r2 r3) = rat_les r1 r2)``, 1816 REPEAT GEN_TAC THEN 1817 REWRITE_TAC[rat_les_def] THEN 1818 REWRITE_TAC[RAT_SUB_RID] THEN 1819 STRIP_TAC THEN 1820 REWRITE_TAC[GSYM RAT_SUB_RDISTRIB] THEN 1821 EQ_TAC THENL 1822 [ 1823 SUBGOAL_THEN ``~(r3 = 0q)`` ASSUME_TAC THENL 1824 [ 1825 SUBST_TAC[CONJUNCT1 (CONJUNCT2 (SPEC ``r3:rat`` (GSYM RAT_SGN_CLAUSES)))] THEN 1826 RW_TAC int_ss[] 1827 , 1828 UNDISCH_TAC ``rat_sgn r3 = 1i`` THEN 1829 SUBST_TAC [GSYM (UNDISCH (SPEC ``r3:rat`` RAT_SGN_MINV))] THEN 1830 REPEAT DISCH_TAC THEN 1831 ONCE_REWRITE_TAC[GSYM RAT_MUL_RID] THEN 1832 SUBST_TAC[GSYM (UNDISCH (SPEC ``r3:rat`` RAT_MUL_RINV))] THEN 1833 SUBST_TAC[EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``rat_mul (rat_sub r2 r1) (rat_mul r3 (rat_minv r3)) = rat_mul (rat_mul (rat_sub r2 r1) r3) (rat_minv r3)``)] THEN 1834 PROVE_TAC[RAT_SGN_MUL, INT_MUL_LID] 1835 ] 1836 , 1837 STRIP_TAC THEN 1838 PROVE_TAC[RAT_SGN_MUL, INT_MUL_LID] 1839 ] ); 1840 1841val RAT_LES_LMUL_POS = store_thm("RAT_LES_LMUL_POS", ``!r1 r2 r3. rat_les 0q r3 ==> (rat_les (rat_mul r3 r1) (rat_mul r3 r2) = rat_les r1 r2)``, 1842 PROVE_TAC[RAT_LES_RMUL_POS, RAT_MUL_COMM] ); 1843 1844val RAT_LES_RMUL_NEG = store_thm("RAT_LES_RMUL_NEG", ``!r1 r2 r3. rat_les r3 0q ==> (rat_les (rat_mul r2 r3) (rat_mul r1 r3) = rat_les r1 r2)``, 1845 REPEAT GEN_TAC THEN 1846 REWRITE_TAC[rat_les_def] THEN 1847 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_ADD_LID] THEN 1848 SUBST_TAC[REWRITE_RULE [INT_NEG_EQ] (SPECL[``r3:rat``] (RAT_SGN_AINV))] THEN 1849 REWRITE_TAC[INT_NEG_EQ] THEN 1850 STRIP_TAC THEN 1851 SUBST_TAC[REWRITE_RULE [RAT_AINV_EQ] (SPECL[``r1:rat``,``r3:rat``] RAT_AINV_LMUL)] THEN 1852 REWRITE_TAC[GSYM RAT_AINV_ADD] THEN 1853 REWRITE_TAC[GSYM RAT_RDISTRIB] THEN 1854 SUBST_TAC[SPECL[``rat_ainv r1``,``r2:rat``] RAT_ADD_COMM] THEN 1855 EQ_TAC THENL 1856 [ 1857 SUBGOAL_THEN ``~(r3 = 0q)`` ASSUME_TAC THENL 1858 [ 1859 SUBST_TAC[CONJUNCT1 (CONJUNCT2 (SPEC ``r3:rat`` (GSYM RAT_SGN_CLAUSES)))] THEN 1860 RW_TAC int_ss[] 1861 , 1862 UNDISCH_TAC ``rat_sgn r3 = ~1`` THEN 1863 SUBST_TAC [GSYM (UNDISCH (SPEC ``r3:rat`` RAT_SGN_MINV))] THEN 1864 REPEAT DISCH_TAC THEN 1865 ONCE_REWRITE_TAC[GSYM RAT_MUL_RID] THEN 1866 SUBST_TAC[GSYM (UNDISCH (SPEC ``r3:rat`` RAT_MUL_RINV))] THEN 1867 SUBST_TAC[EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``rat_mul (rat_add r2 (rat_ainv r1)) (rat_mul r3 (rat_minv r3)) = rat_mul (rat_mul (rat_add r2 (rat_ainv r1)) r3) (rat_minv r3)``)] THEN 1868 ONCE_REWRITE_TAC[GSYM RAT_SGN_AINV] THEN 1869 REWRITE_TAC[INT_NEG_EQ] THEN 1870 ONCE_REWRITE_TAC[RAT_AINV_LMUL] THEN 1871 RW_TAC int_ss [RAT_SGN_MUL] 1872 1873 ] 1874 , 1875 STRIP_TAC THEN 1876 ONCE_REWRITE_TAC[GSYM INT_EQ_NEG] THEN 1877 REWRITE_TAC[RAT_SGN_AINV] THEN 1878 RW_TAC int_ss [RAT_SGN_MUL] 1879 ] ); 1880 1881val RAT_LES_LMUL_NEG = store_thm("RAT_LES_LMUL_NEG", ``!r1 r2 r3. rat_les r3 0q ==> (rat_les (rat_mul r3 r2) (rat_mul r3 r1) = rat_les r1 r2)``, 1882 PROVE_TAC[RAT_LES_RMUL_NEG, RAT_MUL_COMM] ); 1883 1884(*-------------------------------------------------------------------------- 1885 RAT_AINV_LES 1886 1887 |- !r1 r2. ~r1 < r2 = ~r2 < r1 1888 *--------------------------------------------------------------------------*) 1889 1890val RAT_AINV_LES = store_thm("RAT_AINV_LES", ``!r1 r2. rat_les (rat_ainv r1) r2 = rat_les (rat_ainv r2) r1``, 1891 REPEAT GEN_TAC THEN 1892 SUBST_TAC[SPECL [``r1:rat``,``~r2:rat``] (GSYM RAT_LES_AINV)] THEN 1893 PROVE_TAC[RAT_AINV_AINV] ); 1894 1895(*-------------------------------------------------------------------------- 1896 RAT_LDIV_LES_POS, RAT_LDIV_LES_NEG, RAT_RDIV_LES_POS, RAT_RDIV_LES_NEG 1897 1898 |- !r1 r2 r3. 0q < r2 ==> ((r1 / r2 < r3) = (r1 < r2 * r3)) 1899 |- !r1 r2 r3. r2 < 0q ==> ((r1 / r2 < r3) = (r2 * r3 < r1)) 1900 |- !r1 r2 r3. 0q < r3 ==> ((r1 < r2 / r3) = (r1 * r3 < r2)) 1901 |- !r1 r2 r3. r3 < 0q ==> ((r1 < r2 / r3) = (r2 < r1 * r3)) 1902 1903 RAT_LDIV_LEQ_POS, RAT_LDIV_LEQ_NEG, RAT_RDIV_LEQ_POS, RAT_RDIV_LEQ_NEG 1904 for <= likewise 1905 *--------------------------------------------------------------------------*) 1906 1907val RAT_LDIV_LES_POS = store_thm("RAT_LDIV_LES_POS", ``!r1 r2 r3. 0q < r2 ==> ((rat_div r1 r2 < r3) = (r1 < rat_mul r2 r3))``, 1908 REPEAT STRIP_TAC THEN 1909 SUBST_TAC [UNDISCH (SPECL[``rat_div r1 r2``,``r3:rat``,``r2:rat``] (GSYM RAT_LES_LMUL_POS))] THEN 1910 SUBGOAL_THEN ``~(r2=0q)`` ASSUME_TAC THEN1 1911 PROVE_TAC[RAT_LES_REF] THEN 1912 REWRITE_TAC [RAT_DIV_MULMINV] THEN 1913 SUBST_TAC [EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``r2 * (r1 * rat_minv r2) = r1 * (r2 * rat_minv r2)``)] THEN 1914 RW_TAC bool_ss [RAT_MUL_RINV, RAT_MUL_RID] ); 1915 1916val RAT_LDIV_LES_NEG = store_thm("RAT_LDIV_LES_NEG", ``!r1 r2 r3. r2 < 0q ==> ((rat_div r1 r2 < r3) = (rat_mul r2 r3 < r1))``, 1917 REPEAT STRIP_TAC THEN 1918 SUBST_TAC [UNDISCH (SPECL[``rat_div r1 r2``,``r3:rat``,``r2:rat``] (GSYM RAT_LES_RMUL_NEG))] THEN 1919 SUBGOAL_THEN ``~(r2=0q)`` ASSUME_TAC THEN1 1920 PROVE_TAC[RAT_LES_REF] THEN 1921 RW_TAC bool_ss [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC, RAT_MUL_LINV, RAT_MUL_RID] THEN 1922 PROVE_TAC[RAT_MUL_COMM] ); 1923 1924val RAT_RDIV_LES_POS = store_thm("RAT_RDIV_LES_POS", ``!r1 r2 r3. 0q < r3 ==> ((r1 < rat_div r2 r3) = (rat_mul r1 r3 < r2))``, 1925 REPEAT STRIP_TAC THEN 1926 SUBST_TAC [UNDISCH (SPECL[``r1:rat``,``rat_div r2 r3``,``r3:rat``] (GSYM RAT_LES_RMUL_POS))] THEN 1927 SUBGOAL_THEN ``~(r3=0q)`` ASSUME_TAC THEN1 1928 PROVE_TAC[RAT_LES_REF] THEN 1929 REWRITE_TAC [RAT_DIV_MULMINV] THEN 1930 SUBST_TAC [EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``r2 * rat_minv r3 * r3 = r2 * (r3 * rat_minv r3)``)] THEN 1931 RW_TAC bool_ss [RAT_MUL_RINV, RAT_MUL_RID] ); 1932 1933val RAT_RDIV_LES_NEG = store_thm("RAT_RDIV_LES_NEG", ``!r1 r2 r3. r3 < 0q ==> ((r1 < rat_div r2 r3) = (r2 < rat_mul r1 r3))``, 1934 REPEAT STRIP_TAC THEN 1935 SUBST_TAC [UNDISCH (SPECL[``r1:rat``,``rat_div r2 r3``,``r3:rat``] (GSYM RAT_LES_RMUL_NEG))] THEN 1936 SUBGOAL_THEN ``~(r3=0q)`` ASSUME_TAC THEN1 1937 PROVE_TAC[RAT_LES_REF] THEN 1938 REWRITE_TAC [RAT_DIV_MULMINV] THEN 1939 SUBST_TAC [EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``r2 * rat_minv r3 * r3 = r2 * (r3 * rat_minv r3)``)] THEN 1940 RW_TAC bool_ss [RAT_MUL_RINV, RAT_MUL_RID] ); 1941 1942val RAT_LDIV_LEQ_POS = store_thm("RAT_LDIV_LEQ_POS", 1943 ``!r1 r2 r3. 0q < r2 ==> ((rat_div r1 r2 <= r3) = (r1 <= rat_mul r2 r3))``, 1944 REPEAT STRIP_TAC THEN 1945 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_LDIV_LES_POS] THEN 1946 RULE_ASSUM_TAC (CONJUNCT2 o 1947 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o 1948 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN 1949 ASM_SIMP_TAC bool_ss [RAT_LDIV_EQ]) ; 1950 1951val RAT_LDIV_LEQ_NEG = store_thm("RAT_LDIV_LEQ_NEG", 1952 ``!r1 r2 r3. r2 < 0q ==> ((rat_div r1 r2 <= r3) = (rat_mul r2 r3 <= r1))``, 1953 REPEAT STRIP_TAC THEN 1954 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_LDIV_LES_NEG] THEN 1955 RULE_ASSUM_TAC (GSYM o CONJUNCT2 o 1956 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o 1957 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN 1958 CONV_TAC (RHS_CONV (ONCE_DEPTH_CONV SYM_CONV)) THEN 1959 ASM_SIMP_TAC bool_ss [RAT_LDIV_EQ]) ; 1960 1961val RAT_RDIV_LEQ_POS = store_thm("RAT_RDIV_LEQ_POS", 1962 ``!r1 r2 r3. 0q < r3 ==> ((r1 <= rat_div r2 r3) = (rat_mul r1 r3 <= r2))``, 1963 REPEAT STRIP_TAC THEN 1964 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_RDIV_LES_POS] THEN 1965 RULE_ASSUM_TAC (CONJUNCT2 o 1966 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o 1967 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN 1968 ASM_SIMP_TAC bool_ss [RAT_RDIV_EQ]) ; 1969 1970val RAT_RDIV_LEQ_NEG = store_thm("RAT_RDIV_LEQ_NEG", 1971 ``!r1 r2 r3. r3 < 0q ==> ((r1 <= rat_div r2 r3) = (r2 <= rat_mul r1 r3))``, 1972 REPEAT STRIP_TAC THEN 1973 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_RDIV_LES_NEG] THEN 1974 RULE_ASSUM_TAC (GSYM o CONJUNCT2 o 1975 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o 1976 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN 1977 CONV_TAC (RHS_CONV (ONCE_DEPTH_CONV SYM_CONV)) THEN 1978 ASM_SIMP_TAC bool_ss [RAT_RDIV_EQ]) ; 1979 1980(*-------------------------------------------------------------------------- 1981 RAT_LES_SUB0 1982 1983 |- !r1 r2. (r1 - r2) < 0q = r1 < r2 1984 *--------------------------------------------------------------------------*) 1985 1986val RAT_LES_SUB0 = store_thm("RAT_LES_SUB0", ``!r1 r2. rat_les (rat_sub r1 r2) 0q = rat_les r1 r2``, 1987 REPEAT GEN_TAC THEN 1988 SUBST_TAC[GSYM (SPECL[``rat_sub r1 r2``,``0q``,``r2:rat``] RAT_LES_RADD)] THEN 1989 REWRITE_TAC[RAT_SUB_ADDAINV] THEN 1990 SUBST_TAC[EQT_ELIM(AC_CONV(RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add r1 (rat_ainv r2)) r2 = rat_add r1 (rat_add (rat_ainv r2) r2)``)] THEN 1991 REWRITE_TAC[RAT_ADD_LID, RAT_ADD_RID, RAT_ADD_LINV] ); 1992 1993(*-------------------------------------------------------------------------- 1994 RAT_LES_0SUB 1995 1996 |- !r1 r2. 0q < r1 - r2 = r2 < r1 1997 *--------------------------------------------------------------------------*) 1998 1999val RAT_LES_0SUB = store_thm("RAT_LES_0SUB", ``!r1 r2. rat_les 0q (rat_sub r1 r2) = rat_les r2 r1``, 2000 ONCE_REWRITE_TAC[GSYM RAT_LES_AINV] THEN 2001 REWRITE_TAC[RAT_AINV_SUB, RAT_AINV_0] THEN 2002 REWRITE_TAC[RAT_LES_SUB0] THEN 2003 PROVE_TAC[RAT_LES_AINV] ); 2004 2005 2006(*-------------------------------------------------------------------------- 2007 RAT_MINV_LES 2008 2009 |- !r1. 0q < r1 ==> 2010 (rat_minv r1 < 0q = r1 < 0q) /\ 2011 (0q < rat_minv r1 = 0q < r1) 2012 *--------------------------------------------------------------------------*) 2013 2014val RAT_MINV_LES = store_thm("RAT_MINV_LES", ``!r1. 0q < r1 ==> (rat_minv r1 < 0q = r1 < 0q) /\ (0q < rat_minv r1 = 0q < r1)``, 2015 GEN_TAC THEN 2016 DISCH_TAC THEN 2017 REWRITE_TAC[rat_les_def] THEN 2018 REWRITE_TAC[RAT_SUB_LID, RAT_SUB_RID] THEN 2019 ASSUME_TAC (UNDISCH (SPECL[``0q``,``r1:rat``] (prove(``!r1 r2. rat_les r1 r2 ==> ~(r1=r2)``, 2020 PROVE_TAC[RAT_LES_REF])))) THEN 2021 UNDISCH_HD_TAC THEN 2022 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 2023 DISCH_TAC THEN 2024 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 2025 RW_TAC bool_ss [RAT_SGN_MINV] THEN 2026 ONCE_REWRITE_TAC[GSYM INT_EQ_NEG] THEN 2027 ONCE_REWRITE_TAC[RAT_SGN_AINV] THEN 2028 RW_TAC bool_ss [RAT_SGN_MINV] ); 2029 2030 2031(*========================================================================== 2032 * other theorems 2033 *==========================================================================*) 2034 2035(*-------------------------------------------------------------------------- 2036 RAT_MUL_SIGN_CASES 2037 2038 |- !p q. 2039 (0q < p * q = 0q < p /\ 0q < q \/ p < 0q /\ q < 0q) /\ 2040 (p * q < 0q = 0q < p /\ q < 0q \/ p < 0q /\ 0q < q) 2041 *--------------------------------------------------------------------------*) 2042 2043val RAT_MUL_SIGN_CASES = store_thm("RAT_MUL_SIGN_CASES", ``!p q. (0q < p * q = 0q < p /\ 0q < q \/ p < 0q /\ q < 0q) /\ (p * q < 0q = 0q < p /\ q < 0q \/ p < 0q /\ 0q < q)``, 2044 REPEAT GEN_TAC THEN 2045 REWRITE_TAC[rat_les_def, RAT_SUB_LID, RAT_SUB_RID] THEN 2046 SUBST_TAC[GSYM (SPECL[``rat_sgn ~p``,``1i``] INT_EQ_NEG), GSYM (SPECL[``rat_sgn ~q``,``1i``] INT_EQ_NEG), GSYM (SPECL[``rat_sgn ~(p*q)``,``1i``] INT_EQ_NEG)] THEN 2047 REWRITE_TAC[RAT_SGN_AINV,RAT_SGN_MUL] THEN 2048 CONJ_TAC THEN 2049 ASSUME_TAC (SPEC ``p:rat`` RAT_SGN_TOTAL) THEN 2050 ASSUME_TAC (SPEC ``q:rat`` RAT_SGN_TOTAL) THEN 2051 UNDISCH_ALL_TAC THEN 2052 REPEAT STRIP_TAC THEN 2053 ASM_REWRITE_TAC[] THEN 2054 SIMP_TAC int_ss [] ); 2055 2056(*-------------------------------------------------------------------------- 2057 RAT_NO_ZERODIV 2058 |- !r1 r2. (r1 = 0q) \/ (r2 = 0q) = (r1 * r2 = 0q) 2059 2060 RAT_NO_ZERODIV_NEG 2061 |- !r1 r2. ~(r1 * r2 = 0q) = ~(r1 = 0q) /\ ~(r2 = 0q) 2062 *--------------------------------------------------------------------------*) 2063 2064val RAT_NO_ZERODIV = store_thm("RAT_NO_ZERODIV", ``!r1 r2. (r1 = 0q) \/ (r2 = 0q) = (rat_mul r1 r2 = 0q)``, 2065 REPEAT GEN_TAC THEN 2066 ASM_CASES_TAC ``r1=0q`` THEN 2067 ASM_CASES_TAC ``r2=0q`` THEN 2068 RW_TAC int_ss[RAT_MUL_LZERO, RAT_MUL_RZERO] THEN 2069 UNDISCH_ALL_TAC THEN 2070 REWRITE_TAC[RAT_EQ0_NMR, rat_nmr_def] THEN 2071 DISCH_TAC THEN 2072 DISCH_TAC THEN 2073 RAT_CALCTERM_TAC ``rat_mul r1 r2`` THEN 2074 FRAC_CALCTERM_TAC ``frac_mul (rep_rat r1) (rep_rat r2)`` THEN 2075 REWRITE_TAC[RAT_NMREQ0_CONG] THEN 2076 FRAC_NMRDNM_TAC THEN 2077 PROVE_TAC[INT_NO_ZERODIV] ); 2078 2079val RAT_NO_ZERODIV_THM = save_thm( 2080 "RAT_NO_ZERODIV_THM[simp]", 2081 ONCE_REWRITE_RULE [EQ_SYM_EQ] RAT_NO_ZERODIV); 2082 2083val RAT_NO_ZERODIV_NEG = store_thm("RAT_NO_ZERODIV_NEG",``!r1 r2. ~(r1 * r2 = 0q) = ~(r1 = 0q) /\ ~(r2 = 0q)``, 2084 PROVE_TAC[RAT_NO_ZERODIV]); 2085 2086(*-------------------------------------------------------------------------- 2087 RAT_NO_IDDIV 2088 2089 |- !r1 r2. (r1 * r2 = r2) = (r1=1q) \/ (r2=0q) 2090 *--------------------------------------------------------------------------*) 2091 2092val RAT_NO_IDDIV = store_thm("RAT_NO_IDDIV", ``!r1 r2. (rat_mul r1 r2 = r2) = (r1=1q) \/ (r2=0q)``, 2093 REPEAT GEN_TAC THEN 2094 ASM_CASES_TAC ``r2 = 0q`` THEN 2095 RW_TAC bool_ss [RAT_MUL_LID, RAT_MUL_RID, RAT_MUL_LZERO, RAT_MUL_RZERO] THEN 2096 SUBST_TAC[GSYM (SPEC ``r2:rat`` RAT_MUL_LID)] THEN 2097 SUBST1_TAC (EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``rat_mul r1 (rat_mul 1q r2) = rat_mul (rat_mul r1 1q) r2``)) THEN 2098 REWRITE_TAC[RAT_MUL_RID] THEN 2099 SUBST_TAC [UNDISCH (SPECL[``r1:rat``,``1q``,``r2:rat``] RAT_EQ_RMUL)] THEN 2100 PROVE_TAC[] ); 2101 2102(* moving divisions out *) 2103 2104val RDIV_MUL_OUT = Q.store_thm( 2105 "RDIV_MUL_OUT", 2106 ���r1 * (r2 / r3) = (r1 * r2) / r3���, 2107 metis_tac[RAT_MUL_ASSOC, RAT_DIV_MULMINV]); 2108 2109val LDIV_MUL_OUT = Q.store_thm( 2110 "LDIV_MUL_OUT", 2111 ���(r1 / r2) * r3 = (r1 * r3) / r2���, 2112 metis_tac[RAT_MUL_ASSOC, RAT_DIV_MULMINV, RAT_MUL_COMM]); 2113 2114(*-------------------------------------------------------------------------- 2115 RAT_DENSE_THM 2116 2117 |- !r1 r3. r1 < r3 ==> ?r2. r1 < r2 /\ r2 < r3 2118 *--------------------------------------------------------------------------*) 2119 2120val RAT_DENSE_THM = 2121let 2122 val lemmaZ = prove(``! a b. 0i<b ==> ((a*b > 0i) = (a > 0i))``, 2123 REPEAT GEN_TAC THEN 2124 STRIP_TAC THEN 2125 EQ_TAC THEN 2126 SUBST_TAC[SPEC ``b:int`` (GSYM INT_MUL_LZERO)] THEN 2127 REWRITE_TAC[UNDISCH_ALL (SPEC ``b:int`` (SPEC ``0i`` (SPEC ``a:int`` (GSYM INT_GT_RMUL_EXP))))] THEN 2128 REWRITE_TAC[INT_MUL_LZERO] ); 2129 val subst1 = 2130 EQT_ELIM (INT_RING_CONV ``(frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) + frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1)) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * (2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3)) = frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) * frac_dnm (rep_rat r1)``); 2131 val subst2 = 2132 EQT_ELIM (INT_RING_CONV ``frac_nmr (rep_rat r3) * (2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3)) + ~(frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) + frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1)) * frac_dnm (rep_rat r3) = frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3) * frac_dnm (rep_rat r3)``); 2133in 2134 store_thm("RAT_DENSE_THM", ``!r1 r3. rat_les r1 r3 ==> ?r2. rat_les r1 r2 /\ rat_les r2 r3``, 2135 REPEAT GEN_TAC THEN 2136 STRIP_TAC THEN 2137 EXISTS_TAC ``abs_rat(abs_frac(rat_nmr r1 * rat_dnm r3 + rat_nmr r3 * rat_dnm r1, 2 * rat_dnm r1 * rat_dnm r3))`` THEN 2138 UNDISCH_TAC ``rat_les r1 r3`` THEN 2139 REWRITE_TAC[rat_les_def,rat_sgn_def, rat_sub_def] THEN 2140 REWRITE_TAC[rat_nmr_def, rat_dnm_def] THEN 2141 REWRITE_TAC[RAT_SUB_CONG] THEN 2142 REWRITE_TAC[FRAC_SGN_POS] THEN 2143 REWRITE_TAC[GSYM int_gt] THEN 2144 REWRITE_TAC[RAT_NMRGT0_CONG] THEN 2145 REWRITE_TAC[frac_sub_def,frac_ainv_def,frac_add_def] THEN 2146 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN 2147 FRAC_POS_TAC ``frac_dnm (rep_rat r3)`` THEN 2148 FRAC_POS_TAC ``frac_dnm (rep_rat r3) * frac_dnm (rep_rat r1)`` THEN 2149 FRAC_POS_TAC ``2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3)`` THEN 2150 FRAC_POS_TAC ``2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3) * frac_dnm (rep_rat r1)`` THEN 2151 FRAC_POS_TAC ``frac_dnm (rep_rat r3) * (2 * frac_dnm (rep_rat r1) * frac_dnm (rep_rat r3))`` THEN 2152 RW_TAC int_ss[NMR,DNM] THENL 2153 [ 2154 SUBST_TAC[subst1] THEN 2155 REWRITE_TAC[GSYM INT_RDISTRIB] THEN 2156 REWRITE_TAC[UNDISCH_ALL (SPEC ``frac_dnm (rep_rat r1)`` (SPEC ``(frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3))`` lemmaZ))] THEN 2157 PROVE_TAC[] 2158 , 2159 SUBST_TAC[subst2] THEN 2160 REWRITE_TAC[GSYM INT_RDISTRIB] THEN 2161 REWRITE_TAC[UNDISCH_ALL (SPEC ``frac_dnm (rep_rat r3)`` (SPEC ``(frac_nmr (rep_rat r3) * frac_dnm (rep_rat r1) + ~frac_nmr (rep_rat r1) * frac_dnm (rep_rat r3))`` lemmaZ))] THEN 2162 PROVE_TAC[] 2163 ] ) 2164end; 2165 2166 2167(*========================================================================== 2168 * calculation via frac_save terms 2169 *==========================================================================*) 2170 2171(*-------------------------------------------------------------------------- 2172 RAT_SAVE: thm 2173 |- !r1. ?a1 b1. r1 = abs_rat(frac_save a1 b1) 2174 *--------------------------------------------------------------------------*) 2175 2176val RAT_SAVE = store_thm("RAT_SAVE", ``!r1. ?a1 b1. r1 = abs_rat(frac_save a1 b1)``, 2177 REPEAT GEN_TAC THEN 2178 SUBST_TAC[GSYM (SPEC ``r1:rat`` RAT)] THEN 2179 SUBST_TAC[GSYM (SPEC ``rep_rat r1`` FRAC)] THEN 2180 EXISTS_TAC ``rat_nmr r1`` THEN 2181 EXISTS_TAC ``Num (rat_dnm r1 -1i)`` THEN 2182 REWRITE_TAC[frac_save_def, rat_nmr_def, rat_dnm_def, RAT_ABS_EQUIV, rat_equiv_def] THEN 2183 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN 2184 ASSUME_TAC (ARITH_PROVE ``0 < & (Num (frac_dnm (rep_rat r1) - 1i)) + 1i``) THEN 2185 FRAC_NMRDNM_TAC THEN 2186 `0 <= frac_dnm (rep_rat r1) - 1i` by ARITH_TAC THEN 2187 `& (Num (frac_dnm (rep_rat r1) - 1i)) = frac_dnm (rep_rat r1) - 1i` by PROVE_TAC[INT_OF_NUM] THEN 2188 ARITH_TAC ); 2189 2190(*-------------------------------------------------------------------------- 2191 RAT_SAVE_MINV: thm 2192 |- !a1 b1. ~(abs_rat (frac_save a1 b1) = 0q) ==> 2193 (rat_minv (abs_rat (frac_save a1 b1)) = 2194 abs_rat( frac_save (SGN a1 * (& b1 + 1)) (Num (ABS a1 - 1))) ) 2195 *--------------------------------------------------------------------------*) 2196 2197val RAT_SAVE_MINV = store_thm("RAT_SAVE_MINV", ``!a1 b1. ~(abs_rat (frac_save a1 b1) = 0q) ==> (rat_minv (abs_rat (frac_save a1 b1)) = abs_rat( frac_save (SGN a1 * (& b1 + 1i)) (Num (ABS a1 - 1i))) )``, 2198 REPEAT GEN_TAC THEN 2199 REWRITE_TAC[RAT_EQ0_NMR, rat_nmr_def, RAT_NMREQ0_CONG] THEN 2200 STRIP_TAC THEN 2201 `~(0i = frac_nmr (frac_save a1 b1))` by PROVE_TAC[] THEN 2202 REWRITE_TAC[UNDISCH (SPEC ``frac_save a1 b1`` RAT_MINV_CALCULATE)] THEN 2203 `~(a1 = 0i)` by PROVE_TAC[FRAC_NMR_SAVE] THEN 2204 RW_TAC int_ss [FRAC_MINV_SAVE] ); 2205 2206(*-------------------------------------------------------------------------- 2207 RAT_SAVE_TO_CONS: thm 2208 |- !a1 b1. abs_rat (frac_save a1 b1) = rat_cons a1 (& b1 + 1) 2209 *--------------------------------------------------------------------------*) 2210 2211val RAT_SAVE_TO_CONS = store_thm("RAT_SAVE_TO_CONS", ``!a1 b1. abs_rat (frac_save a1 b1) = rat_cons a1 (& b1 + 1)``, 2212 REPEAT GEN_TAC THEN 2213 REWRITE_TAC[rat_cons_def, frac_save_def, RAT_ABS_EQUIV, rat_equiv_def] THEN 2214 ASSUME_TAC (ARITH_PROVE ``0i < & b1 + 1i``) THEN 2215 ASSUME_TAC (ARITH_PROVE ``~(& b1 + 1i < 0i)``) THEN 2216 ASM_REWRITE_TAC[INT_ABS] THEN 2217 FRAC_NMRDNM_TAC THEN 2218 RW_TAC int_ss [SGN_def] ); 2219 2220(*========================================================================== 2221 * calculation of numeral forms 2222 *==========================================================================*) 2223 2224(*-------------------------------------------------------------------------- 2225 RAT_OF_NUM: thm 2226 |- !n. (0 = rat_0) /\ (!n. & (SUC n) = &n + rat_1) 2227 *--------------------------------------------------------------------------*) 2228 2229val RAT_OF_NUM = store_thm("RAT_OF_NUM", ``!n. (0 = rat_0) /\ (!n. & (SUC n) = &n + rat_1)``, 2230 REWRITE_TAC[rat_of_num_def] THEN 2231 Induct_on `n` THEN 2232 REWRITE_TAC[RAT_ADD_LID, rat_of_num_def] ); 2233 2234(*-------------------------------------------------------------------------- 2235 RAT_SAVE: thm 2236 |- !n. &n = abs_rat(frac_save (&n) 0) 2237 *--------------------------------------------------------------------------*) 2238 2239val RAT_SAVE_NUM = store_thm("RAT_SAVE_NUM", ``!n. &n = abs_rat(frac_save (&n) 0)``, 2240 Induct_on `n` THEN 2241 RW_TAC int_ss [frac_save_def, RAT_OF_NUM] THEN1 2242 PROVE_TAC[rat_0_def, frac_0_def] THEN 2243 RAT_CALC_TAC THEN 2244 FRAC_CALC_TAC THEN 2245 REWRITE_TAC[RAT_EQ] THEN 2246 FRAC_NMRDNM_TAC THEN 2247 ARITH_TAC ); 2248 2249(*-------------------------------------------------------------------------- 2250 RAT_CONS_TO_NUM: thm 2251 |- !n. (&n // 1 = &n) /\ ((~&n) // 1 = ~&n) 2252 *--------------------------------------------------------------------------*) 2253 2254val RAT_CONS_TO_NUM = store_thm("RAT_CONS_TO_NUM", ``!n. (&n // 1 = &n) /\ ((~&n) // 1 = ~&n)``, 2255 Induct_on `n` THEN1 2256 RW_TAC int_ss [rat_cons_def, RAT_AINV_0, rat_0, frac_0_def] THEN 2257 APPLY_ASM_TAC 0 (ONCE_REWRITE_TAC[EQ_SYM_EQ]) THEN 2258 ASM_REWRITE_TAC[rat_cons_def, RAT_OF_NUM, RAT_AINV_ADD] THEN 2259 RAT_CALC_TAC THEN 2260 `0 < ABS 1` by ARITH_TAC THEN 2261 FRAC_CALC_TAC THEN 2262 REWRITE_TAC[RAT_EQ] THEN 2263 FRAC_NMRDNM_TAC THEN 2264 RW_TAC int_ss [SGN_def] THEN 2265 ARITH_TAC ); 2266 2267(*-------------------------------------------------------------------------- 2268 RAT_0: thm 2269 |- rat_0 = 0 2270 2271 RAT_1: thm 2272 |- rat_1 = 1 2273 *--------------------------------------------------------------------------*) 2274 2275val RAT_0 = store_thm("RAT_0", ``rat_0 = 0q``, 2276 REWRITE_TAC[rat_of_num_def] ); 2277 2278val RAT_1 = store_thm("RAT_1", ``rat_1 = 1q``, 2279 `1 = SUC 0` by ARITH_TAC THEN 2280 ASM_REWRITE_TAC[] THEN 2281 REWRITE_TAC[rat_of_num_def, RAT_ADD_LID] ); 2282 2283val RAT_OF_NUM_LEQ_0 = prove(``!n. 0 <= &n``, 2284 Induct_on `n` THEN1 2285 PROVE_TAC[RAT_LEQ_REF] THEN 2286 REWRITE_TAC[RAT_OF_NUM] THEN 2287 ASSUME_TAC RAT_LES_01 THEN 2288 ASSUME_TAC (SPECL [``1:rat``, ``&n:rat``] RAT_0LES_0LEQ_ADD) THEN 2289 REWRITE_TAC[RAT_1, RAT_0] THEN 2290 REWRITE_TAC[rat_leq_def] THEN 2291 PROVE_TAC[RAT_ADD_COMM] ); 2292 2293(*-------------------------------------------------------------------------- 2294 * RAT_MINV_1: thm 2295 * |- rat_minv 1 = 1 2296 *--------------------------------------------------------------------------*) 2297 2298val RAT_MINV_1 = Q.store_thm ("RAT_MINV_1[simp]", `rat_minv 1 = 1`, 2299 REWRITE_TAC [SYM RAT_1, rat_1_def] THEN 2300 SIMP_TAC intLib.int_ss [RAT_MINV_CALCULATE, NMR, frac_1_def, 2301 REWRITE_RULE [frac_1_def] FRAC_MINV_1]) ; 2302 2303val RAT_DIV_1 = Q.store_thm( 2304 "RAT_DIV_1[simp]", 2305 ���r / 1q = r���, 2306 simp[RAT_DIV_MULMINV]); 2307 2308val RAT_DIV_NEG1 = Q.store_thm( 2309 "RAT_DIV_NEG1[simp]", 2310 ���r / -1q = -r���, 2311 simp[RAT_DIV_MULMINV, GSYM RAT_AINV_MINV, RAT_1_NOT_0, GSYM RAT_AINV_RMUL]); 2312 2313val RAT_DIV_INV = Q.store_thm( 2314 "RAT_DIV_INV[simp]", 2315 ���r <> 0 ==> (r / r = 1)���, 2316 simp[RAT_DIV_MULMINV, RAT_MUL_RINV]); 2317 2318val RAT_MINV_MUL = Q.store_thm( 2319 "RAT_MINV_MUL", 2320 ���a <> 0 /\ b <> 0 ==> (rat_minv (a * b) = rat_minv a * rat_minv b)���, 2321 strip_tac >> 2322 qspecl_then [���rat_minv (a * b)���, ���rat_minv a * rat_minv b���, ���a���] mp_tac 2323 RAT_EQ_LMUL >> simp[] >> disch_then (SUBST1_TAC o SYM) >> 2324 simp[RAT_MUL_ASSOC, RAT_MUL_RINV] >> 2325 qspecl_then [���a * rat_minv (a * b)���, ���rat_minv b���, ���b���] mp_tac 2326 RAT_EQ_LMUL >> simp[] >> disch_then (SUBST1_TAC o SYM) >> 2327 simp[RAT_MUL_RINV, RAT_MUL_ASSOC] >> 2328 ���b * a * rat_minv (a * b) = a * b * rat_minv (a * b)��� 2329 by simp[AC RAT_MUL_ASSOC RAT_MUL_COMM] >> 2330 pop_assum SUBST_ALL_TAC >> 2331 ���a * b <> 0��� by simp[RAT_NO_ZERODIV_NEG] >> 2332 simp[RAT_MUL_RINV]); 2333 2334val RAT_DIVDIV_MUL = Q.store_thm( 2335 "RAT_DIVDIV_MUL", 2336 ���b <> 0 /\ d <> 0 ==> ((a / b) * (c / d) = (a * c) / (b * d))���, 2337 simp[RAT_DIV_MULMINV, RAT_MINV_MUL, AC RAT_MUL_COMM RAT_MUL_ASSOC]) 2338 2339val RAT_DIVDIV_ADD = Q.store_thm( 2340 "RAT_DIVDIV_ADD", 2341 ���y <> 0 /\ b <> 0 ==> (x / y + a / b = (x * b + a * y) / (y * b))���, 2342 strip_tac >> qmatch_abbrev_tac ���LHS = RHS��� >> 2343 ���LHS = LHS * (y/y) * (b/b)��� by simp[] >> 2344 pop_assum SUBST1_TAC >> simp_tac bool_ss [Abbr`LHS`, RAT_RDISTRIB] >> 2345 ���x / y * (y / y) = x / y��� by simp[] >> pop_assum SUBST1_TAC >> 2346 ���x / y * (b / b) = (x * b) / (y * b)��� by simp[RAT_DIVDIV_MUL] >> 2347 pop_assum SUBST1_TAC >> ���b / b = 1��� by simp[] >> 2348 asm_simp_tac bool_ss [RAT_MUL_RID] >> simp[RAT_DIVDIV_MUL] >> 2349 simp[Abbr`RHS`, RAT_RDISTRIB, RAT_DIV_MULMINV, AC RAT_MUL_ASSOC RAT_MUL_COMM]) 2350 2351val RAT_DIV_AINV = Q.store_thm( 2352 "RAT_DIV_AINV", 2353 ���-(x/y) = (-x)/y���, 2354 simp[RAT_DIV_MULMINV, RAT_AINV_LMUL]); 2355 2356val RAT_MINV_EQ_0 = Q.store_thm( 2357 "RAT_MINV_EQ_0[simp]", 2358 ���r <> 0 ==> rat_minv r <> 0���, 2359 strip_tac >> disch_then (mp_tac o Q.AP_TERM ���$* r���) >> 2360 simp[RAT_MUL_RINV, RAT_1_NOT_0]); 2361 2362val RAT_DIV_MINV = Q.store_thm( 2363 "RAT_DIV_MINV", 2364 ���x <> 0 /\ y <> 0 ==> (rat_minv (x/y) = y / x)���, 2365 strip_tac >> 2366 ���x / y <> 0��� by simp[RAT_DIV_MULMINV, RAT_NO_ZERODIV_NEG] >> 2367 qspecl_then [���rat_minv (x / y)���, ���y / x���, ���x / y���] mp_tac 2368 RAT_EQ_LMUL >> simp[] >> disch_then (SUBST1_TAC o SYM) >> 2369 simp[RAT_MUL_RINV, RAT_DIVDIV_MUL] >> 2370 simp[RAT_MUL_COMM, RAT_NO_ZERODIV_NEG]); 2371 2372val RAT_DIV_EQ0 = Q.store_thm( 2373 "RAT_DIV_EQ0[simp]", 2374 ���d <> 0 ==> ((n / d = 0) <=> (n = 0)) /\ ((0 = n / d) <=> (n = 0))���, 2375 strip_tac >> simp[RAT_DIV_MULMINV, GSYM RAT_NO_ZERODIV, RAT_MINV_EQ_0]); 2376 2377(*-------------------------------------------------------------------------- 2378 RAT_ADD_NUM: thm 2379 2380 |- !n m. ( &n + &m = &(n+m)) 2381 |- !n m. (~&n + &m = if n<=m then &(m-n) else ~&(n-m)) 2382 |- !n m. &n + ~&m = if m<=n then &(n-m) else ~&(m-n) 2383 |- !n m. ~&n + ~&m = ~&(n+m) 2384 *--------------------------------------------------------------------------*) 2385 2386val RAT_ADD_NUM1 = prove(``!n m. ( &n + &m = &(n+m))``, 2387 Induct_on `m` THEN 2388 Induct_on `n` THEN 2389 RW_TAC int_ss [RAT_ADD_LID, RAT_ADD_RID] THEN 2390 LEFT_NO_FORALL_TAC 1 ``SUC (SUC n)`` THEN 2391 UNDISCH_HD_TAC THEN 2392 REWRITE_TAC[RAT_OF_NUM] THEN 2393 `SUC (SUC n) + m = SUC m + SUC n` by ARITH_TAC THEN 2394 PROVE_TAC[RAT_ADD_ASSOC, RAT_ADD_COMM] ); 2395 2396val RAT_ADD_NUM2 = prove(``!n m. (~&n + &m = if n<=m then &(m-n) else ~&(n-m))``, 2397 Induct_on `n` THEN 2398 Induct_on `m` THEN 2399 SIMP_TAC int_ss [RAT_AINV_0, RAT_ADD_LID, RAT_ADD_RID] THEN 2400 LEFT_NO_FORALL_TAC 1 ``m:num`` THEN 2401 APPLY_ASM_TAC 0 (ONCE_REWRITE_TAC[EQ_SYM_EQ]) THEN 2402 ASM_REWRITE_TAC[] THEN 2403 REWRITE_TAC[RAT_OF_NUM] THEN 2404 REWRITE_TAC[RAT_AINV_ADD] THEN 2405 SUBST1_TAC (EQT_ELIM (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``~& n + ~rat_1 + (& m + rat_1) = ~& n + & m + (rat_1 + ~rat_1)``)) THEN 2406 REWRITE_TAC[RAT_ADD_RINV, RAT_ADD_RID] ); 2407 2408val RAT_ADD_NUM3 = prove(``!n m. &n + ~&m = if m<=n then &(n-m) else ~&(m-n)``, 2409 PROVE_TAC[RAT_ADD_NUM2, RAT_ADD_COMM] ); 2410 2411val RAT_ADD_NUM4 = prove(``!n m. ~&n + ~&m = ~&(n+m)``, 2412 PROVE_TAC[RAT_ADD_NUM1, RAT_EQ_AINV, RAT_AINV_ADD] ); 2413 2414val RAT_ADD_NUM_CALCULATE = save_thm("RAT_ADD_NUM_CALCULATE", LIST_CONJ[RAT_ADD_NUM1, RAT_ADD_NUM2, RAT_ADD_NUM3, RAT_ADD_NUM4] ); 2415 2416(*-------------------------------------------------------------------------- 2417 RAT_ADD_MUL: thm 2418 2419 |- !n m. &n * &m = &(n*m) 2420 |- !n m. ~&n * &m = ~&(n*m) 2421 |- !n m. &n * ~&m = ~&(n*m) 2422 |- !n m. ~&n * ~&m = &(n*m) 2423 *--------------------------------------------------------------------------*) 2424 2425val RAT_MUL_NUM1 = prove(``!n m. &n * &m = &(n*m)``, 2426 Induct_on `m` THEN 2427 Induct_on `n` THEN 2428 RW_TAC int_ss [RAT_MUL_LZERO, RAT_MUL_RZERO] THEN 2429 `!x. SUC x = x + 1` by ARITH_TAC THEN 2430 `(n+1) * (m+1) = n * m + n + m + 1:num` by ARITH_TAC THEN 2431 ASM_REWRITE_TAC[GSYM RAT_ADD_NUM1, RAT_LDISTRIB, RAT_RDISTRIB, RAT_ADD_ASSOC, RAT_MUL_ASSOC, RAT_MUL_LID, RAT_MUL_RID, MULT_CLAUSES] THEN 2432 METIS_TAC[RAT_ADD_ASSOC, RAT_ADD_COMM, MULT_COMM] ); 2433 2434val RAT_MUL_NUM2 = prove(``!n m. ~&n * &m = ~&(n*m)``, 2435 PROVE_TAC[GSYM RAT_AINV_LMUL, RAT_EQ_AINV, RAT_MUL_NUM1] ); 2436 2437val RAT_MUL_NUM3 = prove(``!n m. &n * ~&m = ~&(n*m)``, 2438 PROVE_TAC[GSYM RAT_AINV_RMUL, RAT_EQ_AINV, RAT_MUL_NUM1] ); 2439 2440val RAT_MUL_NUM4 = prove(``!n m. ~&n * ~&m = &(n*m)``, 2441 PROVE_TAC[GSYM RAT_AINV_RMUL, GSYM RAT_AINV_LMUL, RAT_AINV_AINV, RAT_MUL_NUM1] ); 2442 2443val RAT_MUL_NUM_CALCULATE = save_thm("RAT_MUL_NUM_CALCULATE", LIST_CONJ[RAT_MUL_NUM1, RAT_MUL_NUM2, RAT_MUL_NUM3, RAT_MUL_NUM4] ); 2444 2445(*-------------------------------------------------------------------------- 2446 RAT_EQ_NUM: thm 2447 2448 |- !n m. ( &n = &m) = (n=m) 2449 |- !n m. ( &n = ~&m) = (n=0) /\ (m=0) 2450 |- !n m. (~&n = &m) = (n=0) /\ (m=0) 2451 |- !n m. (~&n = ~&m) = (n=m) 2452 *--------------------------------------------------------------------------*) 2453 2454val RAT_EQ_NUM1 = prove(``!n m. ( &n = &m) = (n=m)``, 2455 Induct_on `n` THEN 2456 Induct_on `m` THEN 2457 RW_TAC arith_ss [RAT_OF_NUM] THENL 2458 [ 2459 MATCH_MP_TAC (prove(``!r1 r2. (r1 < r2) ==> ~(r1 = r2)``, PROVE_TAC[RAT_LES_ANTISYM])) THEN 2460 ASSUME_TAC (ONCE_REWRITE_RULE[RAT_ADD_COMM, GSYM RAT_0] (SPECL[``rat_1``,``&m:rat``] RAT_0LES_0LEQ_ADD)) THEN 2461 ASSUME_TAC (SPEC ``m:num`` RAT_OF_NUM_LEQ_0) THEN 2462 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0] 2463 , 2464 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 2465 MATCH_MP_TAC (prove(``!r1 r2. (r1 < r2) ==> ~(r1 = r2)``, PROVE_TAC[RAT_LES_ANTISYM])) THEN 2466 ASSUME_TAC (ONCE_REWRITE_RULE[RAT_ADD_COMM, GSYM RAT_0] (SPECL[``rat_1``,``&n:rat``] RAT_0LES_0LEQ_ADD)) THEN 2467 ASSUME_TAC (SPEC ``n:num`` RAT_OF_NUM_LEQ_0) THEN 2468 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0] 2469 , 2470 LEFT_NO_FORALL_TAC 1 ``m:num`` THEN 2471 REWRITE_TAC[RAT_EQ_RADD] THEN 2472 PROVE_TAC[] 2473 ] ); 2474 2475val RAT_EQ_NUM2 = prove(``!n m. ( &n = ~&m) = (n=0) /\ (m=0)``, 2476 Induct_on `n` THEN 2477 Induct_on `m` THEN 2478 RW_TAC arith_ss [RAT_OF_NUM] THENL 2479 [ 2480 PROVE_TAC[RAT_AINV_0, RAT_0] 2481 , 2482 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 2483 MATCH_MP_TAC (prove(``!r1 r2. (r1 < r2) ==> ~(r1 = r2)``, PROVE_TAC[RAT_LES_ANTISYM])) THEN 2484 REWRITE_TAC[RAT_0] THEN 2485 ONCE_REWRITE_TAC[GSYM RAT_AINV_0] THEN 2486 REWRITE_TAC[RAT_LES_AINV] THEN 2487 ASSUME_TAC (ONCE_REWRITE_RULE[RAT_ADD_COMM, GSYM RAT_0] (SPECL[``rat_1``,``&m:rat``] RAT_0LES_0LEQ_ADD)) THEN 2488 ASSUME_TAC (SPEC ``m:num`` RAT_OF_NUM_LEQ_0) THEN 2489 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0] 2490 , 2491 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN 2492 MATCH_MP_TAC (prove(``!r1 r2. (r1 < r2) ==> ~(r1 = r2)``, PROVE_TAC[RAT_LES_ANTISYM])) THEN 2493 REWRITE_TAC[RAT_0] THEN 2494 REWRITE_TAC[RAT_AINV_0] THEN 2495 ASSUME_TAC (ONCE_REWRITE_RULE[RAT_ADD_COMM, GSYM RAT_0] (SPECL[``rat_1``,``&n:rat``] RAT_0LES_0LEQ_ADD)) THEN 2496 ASSUME_TAC (SPEC ``n:num`` RAT_OF_NUM_LEQ_0) THEN 2497 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0] 2498 , 2499 REWRITE_TAC[GSYM RAT_RSUB_EQ] THEN 2500 REWRITE_TAC[RAT_SUB_ADDAINV, GSYM RAT_AINV_ADD] THEN 2501 LEFT_NO_FORALL_TAC 1 ``SUC (SUC m):num`` THEN 2502 UNDISCH_HD_TAC THEN 2503 SIMP_TAC arith_ss [RAT_OF_NUM] 2504 ] ); 2505 2506val RAT_EQ_NUM3 = prove(``!n m. (~&n = &m) = (n=0)/\(m=0)``, 2507 PROVE_TAC[RAT_EQ_AINV, RAT_EQ_NUM2] ); 2508 2509val RAT_EQ_NUM4 = prove(``!n m. (~&n = ~&m) = (n=m)``, 2510 PROVE_TAC[RAT_AINV_EQ, RAT_EQ_NUM1] ); 2511 2512val RAT_EQ_NUM_CALCULATE = save_thm("RAT_EQ_NUM_CALCULATE[simp]", 2513 LIST_CONJ [RAT_EQ_NUM1, RAT_EQ_NUM2, RAT_EQ_NUM3, RAT_EQ_NUM4] ); 2514 2515(* ---------------------------------------------------------------------- 2516 RAT_LT_NUM 2517 ---------------------------------------------------------------------- *) 2518 2519val RAT_LT_NUM1 = RAT_OF_NUM_LES 2520 2521val RAT_LT_NUM2 = Q.prove( 2522 ���-&m < &n <=> 0 < m \/ 0 < n���, 2523 eq_tac >- (spose_not_then strip_assume_tac >> fs[]) >> 2524 strip_tac 2525 >- (irule RAT_LES_LEQ_TRANS >> qexists_tac `0` >> simp[] >> 2526 simp[Once RAT_AINV_LES]) >> 2527 irule RAT_LEQ_LES_TRANS >> qexists_tac `0` >> simp[] >> 2528 simp[rat_leq_def] >> 2529 simp[Once RAT_AINV_LES]); 2530 2531val RAT_LT_NUM3 = Q.prove( 2532 ���&m < -&n <=> F���, 2533 simp[] >> strip_tac >> 2534 ���-&n <= 0��� by simp[rat_leq_def, Once RAT_AINV_LES] >> 2535 ���&m < 0��� by metis_tac[RAT_LES_LEQ_TRANS] >> fs[]) 2536 2537val RAT_LT_NUM4 = Q.prove( 2538 ���-&m < -&n <=> n < m���, 2539 simp[RAT_LES_AINV]); 2540 2541val RAT_LT_NUM_CALCULATE = save_thm( 2542 "RAT_LT_NUM_CALCULATE[simp]", 2543 LIST_CONJ [RAT_LT_NUM1, RAT_LT_NUM2, RAT_LT_NUM3, RAT_LT_NUM4]); 2544 2545(* ---------------------------------------------------------------------- 2546 RAT_LE_NUM 2547 ---------------------------------------------------------------------- *) 2548 2549val RAT_LE_NUM2 = Q.prove( 2550 ���-&m <= &n <=> T���, 2551 simp[rat_leq_def]); 2552 2553val RAT_LE_NUM3 = Q.prove( 2554 ���&m <= -&n <=> (m = 0) /\ (n = 0)���, 2555 simp[rat_leq_def]); 2556 2557val RAT_LE_NUM4 = Q.prove( 2558 ���-&m <= -&n <=> n <= m���, 2559 simp[rat_leq_def]); 2560 2561val RAT_LE_NUM_CALCULATE = save_thm( 2562 "RAT_LE_NUM_CALCULATE[simp]", 2563 LIST_CONJ [RAT_OF_NUM_LEQ, RAT_LE_NUM2, RAT_LE_NUM3, RAT_LE_NUM4]); 2564 2565(* ---------------------------------------------------------------------- 2566 rat_of_int 2567 ---------------------------------------------------------------------- *) 2568 2569val rat_of_int_def = Define ��� 2570 rat_of_int i : rat = if i < 0 then - (& (Num (-i))) else &(Num i) 2571���; 2572 2573val rat_of_int_11 = Q.store_thm( 2574 "rat_of_int_11[simp]", 2575 ���(rat_of_int i1 = rat_of_int i2) <=> (i1 = i2)���, 2576 simp[EQ_IMP_THM] >> simp[rat_of_int_def] >> Cases_on ���i1 < 0��� >> 2577 Cases_on ���i2 < 0��� >> simp[] 2578 >- (���0 <= -i1 /\ 0 <= -i2��� by simp[] >> 2579 rpt (pop_assum 2580 (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>> 2581 ntac 2 strip_tac >> disch_then (mp_tac o AP_TERM ``$& : num -> int``) >> 2582 ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE]) 2583 >- (rename [���a < 0���, ���~(b < 0)���] >> 2584 ���0 <= -a /\ 0 <= b��� by (simp[] >> fs[integerTheory.INT_NOT_LT]) >> 2585 rpt (pop_assum 2586 (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>> 2587 ntac 2 strip_tac >> 2588 disch_then (CONJUNCTS_THEN (mp_tac o AP_TERM ``$& : num -> int``)) >> 2589 ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE]) 2590 >- (rename [���a < 0���, ���~(b < 0)���] >> 2591 ���0 <= -a /\ 0 <= b��� by (simp[] >> fs[integerTheory.INT_NOT_LT]) >> 2592 rpt (pop_assum 2593 (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>> 2594 ntac 2 strip_tac >> 2595 disch_then (CONJUNCTS_THEN (mp_tac o AP_TERM ``$& : num -> int``)) >> 2596 ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE]) 2597 >- (���0 <= i1 /\ 0 <= i2��� by fs[integerTheory.INT_NOT_LT] >> 2598 rpt (pop_assum 2599 (mp_tac o CONV_RULE (REWR_CONV (GSYM integerTheory.INT_OF_NUM))))>> 2600 ntac 2 strip_tac >> disch_then (mp_tac o AP_TERM ``$& : num -> int``) >> 2601 ntac 2 (pop_assum SUBST1_TAC) >> simp[integerTheory.INT_EQ_CALCULATE])); 2602 2603val rat_of_int_of_num = Q.store_thm( 2604 "rat_of_int_of_num[simp]", 2605 ���rat_of_int (&x) = &x���, 2606 simp[rat_of_int_def]); 2607 2608val elim1 = intLib.ARITH_PROVE ``y <= x /\ x <= y ==> (x = y:int)`` 2609val elim2 = intLib.ARITH_PROVE ``x:int < y /\ y < x ==> F`` 2610fun elim_tac k = 2611 REPEAT_GTCL 2612 (fn ttcl => fn th => 2613 first_assum (mp_then.mp_then (mp_then.Pos hd) ttcl th)) 2614 (k o assert (not o is_imp o #2 o strip_forall o concl)) 2615 2616val num_rwt = integerTheory.INT_OF_NUM |> SPEC_ALL |> EQ_IMP_RULE |> #2 2617 2618val rat_of_int_MUL = Q.store_thm( 2619 "rat_of_int_MUL", 2620 ���rat_of_int x * rat_of_int y = rat_of_int (x * y)���, 2621 simp[rat_of_int_def, integerTheory.INT_MUL_SIGN_CASES] >> rw[] >> 2622 fs[integerTheory.INT_NOT_LT, RAT_MUL_NUM_CALCULATE, RAT_EQ_NUM_CALCULATE] >> 2623 TRY (elim_tac assume_tac elim1 ORELSE elim_tac assume_tac elim2) >> rw[] >> 2624 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2625 [GSYM integerTheory.INT_INJ, GSYM integerRingTheory.int_calculate, 2626 num_rwt, integerTheory.INT_LE_MUL, integerTheory.INT_LE_LT, 2627 integerTheory.INT_MUL_SIGN_CASES, integerTheory.INT_NEG_GT0]); 2628 2629val rat_of_int_ADD = Q.store_thm( 2630 "rat_of_int_ADD", 2631 ���rat_of_int x + rat_of_int y = rat_of_int (x + y)���, 2632 simp[rat_of_int_def] >> rw[] 2633 >- (simp[GSYM RAT_AINV_ADD, RAT_ADD_NUM_CALCULATE] >> 2634 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2635 [GSYM integerTheory.INT_INJ, GSYM integerRingTheory.int_calculate, 2636 num_rwt, integerTheory.INT_LE_MUL, integerTheory.INT_LE_LT, 2637 integerTheory.INT_MUL_SIGN_CASES, integerTheory.INT_NEG_GT0]) 2638 >- (full_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) []) 2639 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[] >> 2640 TRY (rename [���Num (-a) <= Num b���] >> 2641 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >> 2642 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt]) >> 2643 rename [���Num (-a) - Num b���] >> 2644 ���Num b <= Num (-a)��� 2645 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2646 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LE] >> 2647 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2648 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB]) 2649 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[] 2650 >- (rename [���Num (-a) <= Num b���] >> 2651 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >> 2652 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt] >> 2653 `Num (-a) <= Num b` 2654 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2655 [num_rwt, GSYM integerTheory.INT_INJ, 2656 GSYM integerTheory.INT_LE] >> 2657 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2658 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB]) 2659 >- (pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >> 2660 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt])) 2661 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[] >> 2662 TRY (rename [���Num (-a) <= Num b���] >> 2663 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >> 2664 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt]) >> 2665 rename [���Num (-a) - Num b���] >> 2666 ���Num b <= Num (-a)��� 2667 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2668 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LE] >> 2669 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2670 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB]) 2671 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[] 2672 >- (rename [���Num (-a) <= Num b���] >> 2673 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >> 2674 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt] >> 2675 `Num (-a) <= Num b` 2676 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2677 [num_rwt, GSYM integerTheory.INT_INJ, 2678 GSYM integerTheory.INT_LE] >> 2679 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2680 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB]) 2681 >- (pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >> 2682 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt])) 2683 >- (full_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) []) 2684 >- (simp[RAT_ADD_NUM_CALCULATE] >> 2685 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2686 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_ADD])) 2687 2688val rat_of_int_LE = Q.store_thm( 2689 "rat_of_int_LE[simp]", 2690 ���rat_of_int i <= rat_of_int j <=> i <= j���, 2691 simp[rat_of_int_def] >> rw[] >> 2692 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2693 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LE]) 2694 2695val rat_of_int_LT = Q.store_thm( 2696 "rat_of_int_LT[simp]", 2697 ���rat_of_int i < rat_of_int j <=> i < j���, 2698 simp[rat_of_int_def] >> rw[] >> 2699 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2700 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LT]); 2701 2702val rat_of_int_ainv = Q.store_thm( 2703 "rat_of_int_ainv", 2704 ���rat_of_int (-i) = -(rat_of_int i)���, 2705 simp[rat_of_int_def] >> rw[] >> 2706 TRY (elim_tac mp_tac elim2 >> simp[]) >> 2707 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) 2708 [num_rwt, GSYM integerTheory.INT_INJ]) 2709 2710val RAT_OF_INT_CALCULATE = Q.store_thm( 2711 "RAT_OF_INT_CALCULATE", 2712 ���!i. rat_of_int i = abs_rat (abs_frac (i, 1))���, 2713 gen_tac >> Cases_on ���i��� >> simp[rat_of_int_def] 2714 >- simp[RAT_OF_NUM_CALCULATE] 2715 >- (simp[GSYM fracTheory.FRAC_AINV_CALCULATE, GSYM RAT_AINV_CALCULATE] >> 2716 simp[RAT_OF_NUM_CALCULATE]) 2717 >- simp[RAT_OF_NUM_CALCULATE]); 2718 2719(* ---------------------------------------------------------------------- 2720 RATN and RATD, which take rational numbers and return unique 2721 numerator and denominator values. Numerator is integer with smallest 2722 possible absolute value; denominator is a natural number. If 2723 numerator is zero, denominator is always one. 2724 ---------------------------------------------------------------------- *) 2725 2726val frac_exists = Q.prove( 2727 ���!r. ?n:int d:num. 0 < d /\ (&d * r = rat_of_int n)���, 2728 gen_tac >> 2729 qabbrev_tac ���f = rep_rat r��� >> 2730 ���r = abs_rat f��� by metis_tac[rat_type_thm] >> 2731 ���?n0 d0. rep_frac f = (n0,d0)��� by (Cases_on ���rep_frac f��� >> simp[]) >> 2732 map_every qexists_tac [���n0���, ���Num d0���] >> 2733 ���rep_frac (abs_frac (rep_frac f)) = rep_frac f��� 2734 by simp [fracTheory.frac_tybij] >> 2735 pop_assum mp_tac >> simp[GSYM (CONJUNCT2 fracTheory.frac_tybij)] >> 2736 strip_tac >> Cases_on ���d0��� >> fs[] >> 2737 rename [���rep_frac f = (n,&d)���] >> 2738 simp[RAT_OF_NUM_CALCULATE, RAT_OF_INT_CALCULATE, RAT_MUL_CALCULATE] >> 2739 ���f = abs_frac (n,&d)��� by metis_tac[fracTheory.frac_tybij] >> 2740 simp[fracTheory.FRAC_MULT_CALCULATE, RAT_ABS_EQUIV] >> 2741 simp[RAT_EQUIV_ALT] >> 2742 map_every qexists_tac [���1���, ���&d���] >> 2743 simp[fracTheory.FRAC_MULT_CALCULATE, integerTheory.INT_MUL_COMM]); 2744 2745val numdenom_exists = Q.prove( 2746 ���!r:rat. 2747 ?n:int d:num. 2748 (r = rat_of_int n / &d) /\ 0 < d /\ ((n = 0) ==> (d = 1)) /\ 2749 !n' d'. (r = rat_of_int n' / &d') /\ 0 < d' ==> ABS n <= ABS n'���, 2750 gen_tac >> 2751 qabbrev_tac `reps = { (a,b) | (&b * r = rat_of_int a) /\ 0 < b }` >> 2752 `WF (measure (Num o ABS o (FST : int # num -> int)))` by simp[] >> 2753 full_simp_tac bool_ss [relationTheory.WF_DEF] >> 2754 ���?e. reps e��� 2755 by (simp[Abbr���reps���, pairTheory.EXISTS_PROD] >> metis_tac[frac_exists]) >> 2756 fs[PULL_EXISTS] >> 2757 Cases_on ���r = 0��� 2758 >- (map_every qexists_tac [���0���, ���1���] >> simp[] >> gen_tac >> Cases_on ���n'��� >> 2759 simp[integerTheory.INT_ABS_NUM, integerTheory.INT_ABS_NEG]) >> 2760 res_tac >> 2761 ���?mn md. min = (mn,md)��� by (Cases_on ���min��� >> simp[]) >> rw[] >> 2762 map_every qexists_tac [���mn���, ���md���] >> fs[Abbr���reps���] >> pairarg_tac >> 2763 fs[pairTheory.FORALL_PROD] >> rpt var_eq_tac >> 2764 qpat_x_assum ���(_,_) = _��� kall_tac >> rpt conj_tac 2765 >- (rename [���&d * r = rat_of_int n���] >> first_x_assum (SUBST1_TAC o SYM) >> 2766 simp[RAT_DIV_MULMINV] >> 2767 ���&d:rat <> 0��� by simp[] >> 2768 metis_tac[RAT_MUL_ASSOC, RAT_MUL_COMM, RAT_MUL_RINV, RAT_MUL_LID]) 2769 >- (rename [���(_ = 0) ==> (_ = 1)���] >> strip_tac >> fs[]) 2770 >- (rpt strip_tac >> 2771 rename [���&d * r = rat_of_int n���, ���r = rat_of_int nn / &dd���] >> 2772 spose_not_then (assume_tac o REWRITE_RULE[integerTheory.INT_NOT_LE]) >> 2773 first_x_assum (qspecl_then [���nn���, ���dd���] mp_tac) >> simp[] >> 2774 reverse conj_tac 2775 >- (���&dd <> 0��� by simp[] >> simp[RAT_DIV_MULMINV] >> 2776 metis_tac[RAT_MUL_ASSOC, RAT_MUL_COMM, RAT_MUL_RINV, RAT_MUL_LID]) >> 2777 simp[NUM_LT])) 2778 2779val RATND_THM = new_specification("RATND_THM", ["RATN", "RATD"], 2780 CONV_RULE (SKOLEM_CONV THENC BINDER_CONV SKOLEM_CONV) numdenom_exists) 2781 2782val RATD_NZERO = save_thm( 2783 "RATD_NZERO[simp]", 2784 let val th = List.nth(RATND_THM |> SPEC_ALL |> CONJUNCTS, 1) 2785 in 2786 CONJ th (CONV_RULE (REWR_CONV (GSYM NOT_ZERO_LT_ZERO)) th) 2787 end); 2788 2789val RATN_LEAST = save_thm( 2790 "RATN_LEAST", 2791 List.nth(RATND_THM |> SPEC_ALL |> CONJUNCTS, 3)) 2792 2793val RATN_RATD_EQ_THM = save_thm( 2794 "RATN_RATD_EQ_THM", 2795 RATND_THM |> SPEC_ALL |> CONJUNCTS |> hd); 2796 2797val RATN_RATD_MULT = save_thm( 2798 "RATN_RATD_MULT", 2799 RATN_RATD_EQ_THM |> Q.AP_TERM ���\x. x * &RATD r��� |> BETA_RULE 2800 |> SIMP_RULE (srw_ss()) [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC, 2801 RAT_MUL_LINV]); 2802 2803val RATND_RAT_OF_NUM = Q.store_thm( 2804 "RATND_RAT_OF_NUM[simp]", 2805 ���(RATN (&n) = &n) /\ (RATD (&n) = 1)���, 2806 mp_tac (Q.INST [`r` |-> `&n`] RATN_RATD_MULT) >> strip_tac >> 2807 ���&n:rat = rat_of_int (&n) / 1��� by simp[] >> 2808 ���ABS (RATN (&n)) <= ABS (&n)��� by metis_tac[RATN_LEAST, DECIDE ``0n < 1``] >> 2809 full_simp_tac bool_ss [integerTheory.INT_ABS_NUM, GSYM rat_of_int_of_num, 2810 rat_of_int_MUL, rat_of_int_11, 2811 integerTheory.INT_MUL] >> 2812 fs[] >> 2813 ���?rn. RATN (&n) = &rn��� by (Cases_on ���RATN (&n)��� >> fs[]) >> 2814 fs[integerTheory.INT_ABS_NUM] >> 2815 conj_asm1_tac 2816 >- (���n <= rn��� suffices_by simp[] >> 2817 Cases_on ���RATD(&n)��� >> fs[MULT_CLAUSES]) >> rpt var_eq_tac >> 2818 ���(RATD(&n) = 1) \/ (n = 0)��� by metis_tac[MULT_RIGHT_1,EQ_MULT_LCANCEL] >> 2819 metis_tac[RATND_THM]); 2820 2821val RATN_EQ0 = Q.store_thm( 2822 "RATN_EQ0[simp]", 2823 ���((RATN r = 0) <=> (r = 0)) /\ ((0 = RATN r) <=> (r = 0))���, 2824 reverse conj_asm1_tac >- metis_tac[] >> 2825 simp[EQ_IMP_THM] >> strip_tac >> 2826 mp_tac RATN_RATD_MULT >> simp[]); 2827 2828val RATN_SIGN = Q.store_thm( 2829 "RATN_SIGN[simp]", 2830 ���(0 < RATN x <=> 0 < x) /\ (0 <= RATN x <=> 0 <= x) /\ (RATN x < 0 <=> x < 0) /\ 2831 (RATN x <= 0 <=> x <= 0)���, 2832 reverse conj_asm1_tac 2833 >- (simp[integerTheory.INT_LE_LT, rat_leq_def, EQ_SYM_EQ] >> 2834 conj_tac >> ONCE_REWRITE_TAC [DECIDE ``(p:bool = q) = (~p = ~q)``] >> 2835 ASM_REWRITE_TAC [integerTheory.INT_NOT_LT, integerTheory.INT_LE_LT, RAT_LEQ_LES, 2836 rat_leq_def, DE_MORGAN_THM] >> simp[] >> metis_tac[]) >> 2837 eq_tac >> strip_tac >> mp_tac (Q.INST [`r` |-> `x`] RATN_RATD_MULT) 2838 >- (���0 < rat_of_int (RATN x)��� 2839 by asm_simp_tac bool_ss [GSYM rat_of_int_of_num, rat_of_int_LT] >> 2840 strip_tac >> 2841 ���0 < x * &RATD x��� by metis_tac[] >> 2842 pop_assum mp_tac >> simp[RAT_MUL_SIGN_CASES]) >> 2843 ���0 < x * &RATD x��� by simp[RAT_MUL_SIGN_CASES] >> strip_tac >> 2844 ���0 < rat_of_int (RATN x)��� by metis_tac[] >> 2845 full_simp_tac bool_ss [GSYM rat_of_int_of_num, rat_of_int_LT]); 2846 2847val RATN_MUL_LEAST = 2848 SIMP_RULE (srw_ss() ++ boolSimps.CONJ_ss ++ ARITH_ss) [RAT_RDIV_EQ] RATN_LEAST; 2849 2850val RAT_AINV_SGN = Q.store_thm( 2851 "RAT_AINV_SGN[simp]", 2852 ���(0 < -r <=> r < 0) /\ (-r < 0 <=> 0 < r)���, 2853 metis_tac[RAT_LES_AINV, RAT_AINV_0]); 2854 2855val RATN_NEG = Q.store_thm( 2856 "RATN_NEG[simp]", 2857 ���RATN (-r) = -RATN r���, 2858 assume_tac RATN_RATD_MULT >> assume_tac (Q.INST [`r` |-> `-r`] RATN_RATD_MULT) >> 2859 first_assum (mp_tac o Q.AP_TERM `rat_ainv`) >> 2860 REWRITE_TAC[RAT_AINV_LMUL] >> simp[] >> strip_tac >> 2861 ���ABS (RATN r) <= ABS (-RATN (-r))��� 2862 by (irule RATN_MUL_LEAST >> qexists_tac ���&RATD (-r)��� >> simp[rat_of_int_ainv]) >> 2863 fs[] >> 2864 last_assum (mp_tac o Q.AP_TERM `rat_ainv`) >> 2865 REWRITE_TAC[RAT_AINV_LMUL] >> simp[] >> strip_tac >> 2866 ���ABS (RATN (-r)) <= ABS (-RATN (r))��� 2867 by (irule RATN_MUL_LEAST >> qexists_tac ���&RATD r��� >> simp[rat_of_int_ainv]) >> 2868 fs[] >> 2869 ���ABS (RATN (-r)) = ABS (RATN r)��� by metis_tac[INT_LE_ANTISYM] >> 2870 fs[INT_ABS_EQ_ABS] >> fs[] >> 2871 ���r * &RATD r = -r * &RATD (-r)��� by simp[] >> pop_assum mp_tac >> 2872 rpt (pop_assum kall_tac) >> strip_tac >> 2873 qspecl_then [���0���, ���r���] strip_assume_tac RAT_LES_TOTAL 2874 >- (���0 < r * &RATD r��� by simp[RAT_MUL_SIGN_CASES] >> 2875 ���~(0 < -r * &RATD (-r))��� 2876 by (simp[RAT_MUL_SIGN_CASES] >> metis_tac[RAT_LES_REF, RAT_LES_TRANS]) >> 2877 metis_tac[]) 2878 >- simp[] 2879 >- (���r * &RATD r < 0��� by simp[RAT_MUL_SIGN_CASES] >> 2880 ���~(-r * &RATD(-r) < 0)��� 2881 by (simp[RAT_MUL_SIGN_CASES] >> metis_tac[RAT_LES_REF, RAT_LES_TRANS]) >> 2882 metis_tac[])); 2883 2884val RATD_NEG = Q.store_thm( 2885 "RATD_NEG[simp]", 2886 ���RATD (-r) = RATD r���, 2887 Cases_on ���r = 0��� >> fs[] >> 2888 assume_tac RATN_RATD_MULT >> assume_tac (Q.INST [`r` |-> `-r`] RATN_RATD_MULT) >> fs[] >> 2889 pop_assum (mp_tac o Q.AP_TERM ���rat_ainv���) >> REWRITE_TAC [RAT_AINV_LMUL] >> 2890 simp[rat_of_int_ainv] >> metis_tac[RAT_EQ_LMUL, RAT_EQ_NUM_CALCULATE]); 2891 2892val RATN_RATD_RAT_OF_INT = Q.store_thm( 2893 "RATN_RATD_RAT_OF_INT[simp]", 2894 ���(RATN (rat_of_int i) = i) /\ (RATD (rat_of_int i) = 1)���, 2895 Cases_on ���i��� >> simp[rat_of_int_ainv]); 2896 2897val RATN_DIV_RATD = Q.store_thm( 2898 "RATN_DIV_RATD[simp]", 2899 ���rat_of_int (RATN r) / &RATD r = r���, 2900 ONCE_REWRITE_TAC [EQ_SYM_EQ] >> simp[RAT_RDIV_EQ, RATN_RATD_MULT]); 2901 2902val RAT_AINV_EQ_NUM = Q.store_thm( 2903 "RAT_AINV_EQ_NUM[simp]", 2904 ���(rat_ainv x = rat_of_num n) <=> (x = rat_of_int (-&n))���, 2905 simp[EQ_IMP_THM, rat_of_int_ainv] >> disch_then (SUBST1_TAC o SYM) >> simp[]); 2906 2907(* ---------------------------------------------------------------------- 2908 more theorems about RAT_SGN : rat -> int (-1,0,1) 2909 ---------------------------------------------------------------------- *) 2910 2911val _ = temp_overload_on ("RAT_SGN", ``rat_sgn``) 2912val RAT_SGN_NUM_COND = Q.store_thm( 2913 "RAT_SGN_NUM_COND", 2914 ���rat_sgn (&n) = if n = 0 then 0 else 1���, 2915 rw[] >> `0 < n` by simp[] >> 2916 `0 < &n` by simp[] >> 2917 pop_assum (mp_tac o REWRITE_RULE [rat_les_def]) >> simp[]); 2918 2919val RAT_SGN_AINV_RWT = Q.store_thm( 2920 "RAT_SGN_AINV_RWT[simp]", 2921 ���rat_sgn (-r) = -rat_sgn r���, 2922 simp[SimpLHS, Once (GSYM RAT_SGN_AINV)]); 2923 2924val RAT_SGN_ALT = Q.store_thm("RAT_SGN_ALT", 2925 ���rat_sgn r = SGN (RATN r)���, 2926 assume_tac RATN_RATD_EQ_THM >> 2927 map_every qabbrev_tac [`n = RATN r`, `nr = rat_of_int n`, `d = &(RATD r)`] >> 2928 `d <> 0` by simp[Abbr`d`] >> 2929 simp[RAT_DIV_MULMINV, RAT_SGN_MUL, RAT_SGN_MINV] >> 2930 `d > 0` by simp[Abbr`d`, rat_gre_def] >> 2931 `rat_sgn d = 1` by metis_tac[RAT_SGN_CLAUSES] >> simp[] >> 2932 simp[Abbr`nr`, rat_of_int_def, SGN_def] >> Cases_on `n = 0` >> simp[] >> 2933 rw[] >> rw[RAT_SGN_NUM_COND] >> 2934 Cases_on `n` >> fs[]); 2935 2936val RAT_SGN_NUM_BITs = Q.store_thm( 2937 "RAT_SGN_NUM_BITs[simp]", 2938 ���(rat_sgn (&(NUMERAL (BIT1 n))) = 1) /\ (rat_sgn (&(NUMERAL (BIT2 n))) = 1)���, 2939 REWRITE_TAC[arithmeticTheory.BIT1, arithmeticTheory.BIT2, 2940 arithmeticTheory.NUMERAL_DEF, arithmeticTheory.ALT_ZERO] >> 2941 simp[RAT_SGN_NUM_COND]); 2942 2943val RAT_SGN_EQ0 = Q.store_thm( 2944 "RAT_SGN_EQ0[simp]", 2945 ���((rat_sgn r = 0) <=> (r = 0)) /\ ((0 = rat_sgn r) <=> (r = 0))���, 2946 metis_tac[RAT_SGN_CLAUSES]); 2947 2948val RAT_SGN_POS = Q.store_thm( 2949 "RAT_SGN_POS[simp]", 2950 ���(rat_sgn r = 1) <=> 0 < r���, 2951 rw[RAT_SGN_CLAUSES, rat_gre_def]); 2952 2953val RAT_SGN_NEG = Q.store_thm( 2954 "RAT_SGN_NEG[simp]", 2955 ���(rat_sgn r = -1) <=> r < 0���, 2956 rw[RAT_SGN_CLAUSES]); 2957 2958val RAT_SGN_DIV = Q.store_thm( 2959 "RAT_SGN_DIV[simp]", 2960 ���d <> 0 ==> (rat_sgn (n/d) = rat_sgn n * rat_sgn d)���, 2961 simp[RAT_SGN_MINV, RAT_DIV_MULMINV]); 2962 2963val RAT_MINV_RATND = Q.store_thm( 2964 "RAT_MINV_RATND", 2965 ���r <> 0 ==> 2966 (rat_minv r = 2967 (rat_of_int (rat_sgn r) * &RATD r) / rat_of_int (ABS (RATN r)))���, 2968 assume_tac (SYM RATN_DIV_RATD) >> 2969 map_every qabbrev_tac [���n = RATN r���, ���d = RATD r���] >> 2970 first_x_assum SUBST1_TAC >> ���0 < d��� by simp[Abbr���d���] >> simp[RAT_DIV_EQ0] >> 2971 simp[RAT_SGN_NUM_COND] >> Cases_on ���n��� >> 2972 simp[RAT_DIV_MINV, rat_of_int_ainv, RAT_SGN_NUM_COND] >> 2973 simp[RAT_DIV_MULMINV, GSYM RAT_AINV_MINV, GSYM RAT_AINV_LMUL, 2974 GSYM RAT_AINV_RMUL]); 2975 2976(* ---------------------------------------------------------------------- 2977 rational min and max 2978 ---------------------------------------------------------------------- *) 2979 2980val rat_min_def = Define���rat_min (r1:rat) r2 = if r1 < r2 then r1 else r2���; 2981val rat_max_def = Define���rat_max (r1:rat) r2 = if r1 > r2 then r1 else r2���; 2982 2983(*========================================================================== 2984 * end of theory 2985 *==========================================================================*) 2986 2987val _ = export_theory(); 2988