1(*---------------------------------------------------------------------------*) 2(* Develop the theory of reals *) 3(*---------------------------------------------------------------------------*) 4 5(* 6app load ["numLib", 7 "pairLib", 8 "mesonLib", 9 "tautLib", 10 "simpLib", 11 "Ho_Rewrite", 12 "AC", 13 "hol88Lib", 14 "jrhUtils", 15 "realaxTheory"]; 16*) 17 18open HolKernel Parse boolLib hol88Lib numLib reduceLib pairLib 19 arithmeticTheory numTheory prim_recTheory whileTheory 20 mesonLib tautLib simpLib Ho_Rewrite Arithconv 21 jrhUtils Canon_Port hratTheory hrealTheory realaxTheory 22 BasicProvers TotalDefn metisLib bossLib; 23 24val _ = new_theory "real"; 25 26val AC = AC.AC; 27 28val num_EQ_CONV = Arithconv.NEQ_CONV; 29 30(*---------------------------------------------------------------------------*) 31(* Now define the inclusion homomorphism &:num->real. *) 32(*---------------------------------------------------------------------------*) 33 34val real_of_num = new_recursive_definition 35 {name = "real_of_num", 36 def = ���(real_of_num 0 = real_0) /\ 37 (real_of_num(SUC n) = real_of_num n + real_1)���, 38 rec_axiom = num_Axiom} 39 40val _ = add_numeral_form(#"r", SOME "real_of_num"); 41 42val REAL_0 = store_thm("REAL_0", 43 ���real_0 = &0���, 44 REWRITE_TAC[real_of_num]); 45 46val REAL_1 = store_thm("REAL_1", 47 ���real_1 = & 1���, 48 REWRITE_TAC[num_CONV ���1:num���, real_of_num, REAL_ADD_LID]); 49 50local val reeducate = REWRITE_RULE[REAL_0, REAL_1] 51in 52 val REAL_10 = save_thm("REAL_10",reeducate(REAL_10)) 53 val REAL_ADD_SYM = save_thm("REAL_ADD_SYM",reeducate(REAL_ADD_SYM)) 54 val REAL_ADD_COMM = save_thm("REAL_ADD_COMM", REAL_ADD_SYM) 55 val REAL_ADD_ASSOC = save_thm("REAL_ADD_ASSOC",reeducate(REAL_ADD_ASSOC)) 56 val REAL_ADD_LID = save_thm("REAL_ADD_LID",reeducate(REAL_ADD_LID)) 57 val REAL_ADD_LINV = save_thm("REAL_ADD_LINV",reeducate(REAL_ADD_LINV)) 58 val REAL_LDISTRIB = save_thm("REAL_LDISTRIB",reeducate(REAL_LDISTRIB)) 59 val REAL_LT_TOTAL = save_thm("REAL_LT_TOTAL",reeducate(REAL_LT_TOTAL)) 60 val REAL_LT_REFL = save_thm("REAL_LT_REFL",reeducate(REAL_LT_REFL)) 61 val REAL_LT_TRANS = save_thm("REAL_LT_TRANS",reeducate(REAL_LT_TRANS)) 62 val REAL_LT_IADD = save_thm("REAL_LT_IADD",reeducate(REAL_LT_IADD)) 63 val REAL_SUP_ALLPOS = save_thm("REAL_SUP_ALLPOS",reeducate(REAL_SUP_ALLPOS)) 64 val REAL_MUL_SYM = save_thm("REAL_MUL_SYM",reeducate(REAL_MUL_SYM)) 65 val REAL_MUL_COMM = save_thm("REAL_MUL_COMM", REAL_MUL_SYM) 66 val REAL_MUL_ASSOC = save_thm("REAL_MUL_ASSOC",reeducate(REAL_MUL_ASSOC)) 67 val REAL_MUL_LID = save_thm("REAL_MUL_LID",reeducate(REAL_MUL_LID)) 68 val REAL_MUL_LINV = save_thm("REAL_MUL_LINV",reeducate(REAL_MUL_LINV)) 69 val REAL_LT_MUL = save_thm("REAL_LT_MUL",reeducate(REAL_LT_MUL)) 70 val REAL_INV_0 = save_thm("REAL_INV_0",reeducate REAL_INV_0) 71end; 72 73val _ = export_rewrites 74 ["REAL_ADD_LID", "REAL_ADD_LINV", "REAL_LT_REFL", "REAL_MUL_LID"] 75 76(*---------------------------------------------------------------------------*) 77(* Define subtraction, division and the other orderings *) 78(*---------------------------------------------------------------------------*) 79 80val real_sub = new_definition("real_sub", ``real_sub x y = x + ~y``); 81val real_lte = new_definition("real_lte", ``real_lte x y = ~(y < x)``); 82val real_gt = new_definition("real_gt", ``real_gt x y = y < x``); 83val real_ge = new_definition("real_ge", ``real_ge x y = (real_lte y x)``); 84 85val real_div = new_definition("real_div", ``$/ x y = x * inv y``); 86val _ = set_fixity "/" (Infixl 600); 87val _ = overload_on(GrammarSpecials.decimal_fraction_special, ``$/``) 88val _ = overload_on("/", ``$/``) 89 90local open realPP in end 91val _ = add_ML_dependency "realPP" 92val _ = add_user_printer ("real.decimalfractions", 93 ``&(NUMERAL x) : real / &(NUMERAL y)``) 94 95val natsub = Term`$-`; 96val natlte = Term`$<=`; 97val natgt = Term`$>`; 98val natge = Term`$>=`; 99 100val _ = overload_on ("-", natsub); 101val _ = overload_on ("<=", natlte); 102val _ = overload_on (">", natgt); 103val _ = overload_on (">=", natge); 104 105val _ = overload_on ("-", Term`$real_sub`); 106val _ = overload_on ("<=", Term`$real_lte`); 107val _ = overload_on (">", Term`$real_gt`); 108val _ = overload_on (">=", Term`$real_ge`); 109 110(*---------------------------------------------------------------------------*) 111(* Prove lots of boring field theorems *) 112(*---------------------------------------------------------------------------*) 113 114val REAL_ADD_RID = store_thm("REAL_ADD_RID", 115 ���!x. x + 0 = x���, 116 GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 117 MATCH_ACCEPT_TAC REAL_ADD_LID); 118val _ = export_rewrites ["REAL_ADD_RID"] 119 120val REAL_ADD_RINV = store_thm("REAL_ADD_RINV", 121 ���!x:real. x + ~x = 0���, 122 GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 123 MATCH_ACCEPT_TAC REAL_ADD_LINV); 124val _ = export_rewrites ["REAL_ADD_RINV"] 125 126val REAL_MUL_RID = store_thm("REAL_MUL_RID", 127 ���!x. x * 1 = x���, 128 GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 129 MATCH_ACCEPT_TAC REAL_MUL_LID); 130val _ = export_rewrites ["REAL_MUL_RID"] 131 132val REAL_MUL_RINV = store_thm("REAL_MUL_RINV", 133 ���!x. ~(x = 0) ==> (x * inv x = 1)���, 134 GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 135 MATCH_ACCEPT_TAC REAL_MUL_LINV); 136 137val REAL_RDISTRIB = store_thm("REAL_RDISTRIB", 138 ���!x y z. (x + y) * z = (x * z) + (y * z)���, 139 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 140 MATCH_ACCEPT_TAC REAL_LDISTRIB); 141 142val REAL_EQ_LADD = store_thm("REAL_EQ_LADD", 143 ���!x y z. (x + y = x + z) = (y = z)���, 144 REPEAT GEN_TAC THEN EQ_TAC THENL 145 [DISCH_THEN(MP_TAC o AP_TERM ���$+ ~x���) THEN 146 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID], 147 DISCH_THEN SUBST1_TAC THEN REFL_TAC]); 148val _ = export_rewrites ["REAL_EQ_LADD"] 149 150val REAL_EQ_RADD = store_thm("REAL_EQ_RADD", 151 ���!x y z. (x + z = y + z) = (x = y)���, 152 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 153 MATCH_ACCEPT_TAC REAL_EQ_LADD); 154val _ = export_rewrites ["REAL_EQ_RADD"] 155 156val REAL_ADD_LID_UNIQ = store_thm("REAL_ADD_LID_UNIQ", 157 ���!x y. (x + y = y) = (x = 0)���, 158 REPEAT GEN_TAC THEN 159 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [GSYM REAL_ADD_LID] THEN 160 MATCH_ACCEPT_TAC REAL_EQ_RADD); 161 162val REAL_ADD_RID_UNIQ = store_thm("REAL_ADD_RID_UNIQ", 163 ���!x y. (x + y = x) = (y = 0)���, 164 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 165 MATCH_ACCEPT_TAC REAL_ADD_LID_UNIQ); 166 167val REAL_LNEG_UNIQ = store_thm("REAL_LNEG_UNIQ", 168 ���!x y. (x + y = 0) = (x = ~y)���, 169 REPEAT GEN_TAC THEN SUBST1_TAC (SYM(SPEC ���y:real��� REAL_ADD_LINV)) THEN 170 MATCH_ACCEPT_TAC REAL_EQ_RADD); 171 172val REAL_RNEG_UNIQ = store_thm("REAL_RNEG_UNIQ", 173 ���!x y. (x + y = 0) = (y = ~x)���, 174 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 175 MATCH_ACCEPT_TAC REAL_LNEG_UNIQ); 176 177val REAL_NEG_ADD = store_thm("REAL_NEG_ADD", 178 ���!x y. ~(x + y) = ~x + ~y���, 179 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN 180 REWRITE_TAC[GSYM REAL_LNEG_UNIQ] THEN 181 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 182 ���(a + b) + (c + d) = (a + c) + (b + d):real���] THEN 183 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID]); 184 185val REAL_MUL_LZERO = store_thm("REAL_MUL_LZERO", 186 ���!x. 0 * x = 0���, 187 GEN_TAC THEN 188 SUBST1_TAC(SYM(SPECL [���&0 * x���, ���&0 * x���] REAL_ADD_LID_UNIQ)) 189 THEN REWRITE_TAC[GSYM REAL_RDISTRIB, REAL_ADD_LID]); 190val _ = export_rewrites ["REAL_MUL_LZERO"] 191 192val REAL_MUL_RZERO = store_thm("REAL_MUL_RZERO", 193 ���!x. x * 0 = 0���, 194 GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 195 MATCH_ACCEPT_TAC REAL_MUL_LZERO); 196val _ = export_rewrites ["REAL_MUL_RZERO"] 197 198val REAL_NEG_LMUL = store_thm("REAL_NEG_LMUL", 199 ���!x y. ~(x * y) = ~x * y���, 200 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN 201 REWRITE_TAC[GSYM REAL_LNEG_UNIQ, GSYM REAL_RDISTRIB, 202 REAL_ADD_LINV, REAL_MUL_LZERO]); 203 204val REAL_NEG_RMUL = store_thm("REAL_NEG_RMUL", 205 ���!x y. ~(x * y) = x * ~y���, 206 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 207 MATCH_ACCEPT_TAC REAL_NEG_LMUL); 208 209val REAL_NEGNEG = store_thm("REAL_NEGNEG", 210 ���!x. ~~x = x���, 211 GEN_TAC THEN CONV_TAC SYM_CONV THEN 212 REWRITE_TAC[GSYM REAL_LNEG_UNIQ, REAL_ADD_RINV]); 213val _ = export_rewrites ["REAL_NEGNEG"] 214 215val REAL_NEG_MUL2 = store_thm("REAL_NEG_MUL2", 216 ���!x y. ~x * ~y = x * y���, 217 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL, REAL_NEGNEG]); 218 219val REAL_ENTIRE = store_thm("REAL_ENTIRE", 220 ���!x y. (x * y = 0) = (x = 0) \/ (y = 0)���, 221 REPEAT GEN_TAC THEN EQ_TAC THENL 222 [ASM_CASES_TAC ���x = 0��� THEN ASM_REWRITE_TAC[] THEN 223 RULE_ASSUM_TAC(MATCH_MP REAL_MUL_LINV) THEN 224 DISCH_THEN(MP_TAC o AP_TERM ���$* (inv x)���) THEN 225 ASM_REWRITE_TAC[REAL_MUL_ASSOC, REAL_MUL_LID, REAL_MUL_RZERO], 226 DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THEN 227 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO]]); 228val _ = export_rewrites ["REAL_ENTIRE"] 229 230val REAL_LT_LADD = store_thm("REAL_LT_LADD", 231 ���!x y z. (x + y) < (x + z) = y < z���, 232 REPEAT GEN_TAC THEN EQ_TAC THENL 233 [DISCH_THEN(MP_TAC o SPEC ���~x��� o MATCH_MP REAL_LT_IADD) THEN 234 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID], 235 MATCH_ACCEPT_TAC REAL_LT_IADD]); 236val _ = export_rewrites ["REAL_LT_LADD"] 237 238val REAL_LT_RADD = store_thm("REAL_LT_RADD", 239 ���!x y z. (x + z) < (y + z) = x < y���, 240 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 241 MATCH_ACCEPT_TAC REAL_LT_LADD); 242val _ = export_rewrites ["REAL_LT_RADD"] 243 244val REAL_NOT_LT = store_thm("REAL_NOT_LT", 245 ���!x y. ~(x < y) = y <= x���, 246 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte]); 247 248val REAL_LT_ANTISYM = store_thm("REAL_LT_ANTISYM", 249 ���!x y. ~(x < y /\ y < x)���, 250 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_TRANS) THEN 251 REWRITE_TAC[REAL_LT_REFL]); 252 253val REAL_LT_GT = store_thm("REAL_LT_GT", 254 ���!x y. x < y ==> ~(y < x)���, 255 REPEAT GEN_TAC THEN 256 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN 257 REWRITE_TAC[REAL_LT_ANTISYM]); 258 259val REAL_NOT_LE = store_thm("REAL_NOT_LE", 260 ���!x y. ~(x <= y) = y < x���, 261 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte]); 262 263val REAL_LE_TOTAL = store_thm("REAL_LE_TOTAL", 264 ���!x y. x <= y \/ y <= x���, 265 REPEAT GEN_TAC THEN 266 REWRITE_TAC[real_lte, GSYM DE_MORGAN_THM, REAL_LT_ANTISYM]); 267 268val REAL_LET_TOTAL = store_thm("REAL_LET_TOTAL", 269 ���!x y. x <= y \/ y < x���, 270 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN 271 BOOL_CASES_TAC ���y < x��� THEN REWRITE_TAC[]); 272 273val REAL_LTE_TOTAL = store_thm("REAL_LTE_TOTAL", 274 ���!x y. x < y \/ y <= x���, 275 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN 276 BOOL_CASES_TAC ���x < y��� THEN REWRITE_TAC[]); 277 278val REAL_LE_REFL = store_thm("REAL_LE_REFL", 279 ���!x. x <= x���, 280 GEN_TAC THEN REWRITE_TAC[real_lte, REAL_LT_REFL]); 281val _ = export_rewrites ["REAL_LE_REFL"] 282 283val REAL_LE_LT = store_thm("REAL_LE_LT", 284 ���!x y. x <= y = x < y \/ (x = y)���, 285 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN EQ_TAC THENL 286 [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 287 (SPECL [���x:real���, ���y:real���] REAL_LT_TOTAL) THEN ASM_REWRITE_TAC[], 288 DISCH_THEN(DISJ_CASES_THEN2 289 (curry op THEN (MATCH_MP_TAC REAL_LT_GT) o ACCEPT_TAC) SUBST1_TAC) THEN 290 MATCH_ACCEPT_TAC REAL_LT_REFL]); 291 292val REAL_LT_LE = store_thm("REAL_LT_LE", 293 ���!x y. x < y = x <= y /\ ~(x = y)���, 294 let val lemma = TAUT_CONV ���~(a /\ ~a)��� in 295 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT, RIGHT_AND_OVER_OR, lemma] 296 THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 297 POP_ASSUM MP_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN 298 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LT_REFL] end); 299 300val REAL_LT_IMP_LE = store_thm("REAL_LT_IMP_LE", 301 ���!x y. x < y ==> x <= y���, 302 REPEAT GEN_TAC THEN DISCH_TAC THEN 303 ASM_REWRITE_TAC[REAL_LE_LT]); 304 305val REAL_LTE_TRANS = store_thm("REAL_LTE_TRANS", 306 ���!x y z. x < y /\ y <= z ==> x < z���, 307 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT, LEFT_AND_OVER_OR] THEN 308 DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP REAL_LT_TRANS) 309 (CONJUNCTS_THEN2 MP_TAC SUBST1_TAC)) THEN REWRITE_TAC[]); 310 311val REAL_LET_TRANS = store_thm("REAL_LET_TRANS", 312 ���!x y z. x <= y /\ y < z ==> x < z���, 313 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT, RIGHT_AND_OVER_OR] THEN 314 DISCH_THEN(DISJ_CASES_THEN2 (ACCEPT_TAC o MATCH_MP REAL_LT_TRANS) 315 (CONJUNCTS_THEN2 SUBST1_TAC ACCEPT_TAC))); 316 317val REAL_LE_TRANS = store_thm("REAL_LE_TRANS", 318 ���!x y z. x <= y /\ y <= z ==> x <= z���, 319 REPEAT GEN_TAC THEN 320 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_LE_LT] THEN 321 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (DISJ_CASES_THEN2 ASSUME_TAC SUBST1_TAC)) 322 THEN REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o C CONJ (ASSUME ���y < z���)) THEN 323 DISCH_THEN(ACCEPT_TAC o MATCH_MP REAL_LT_IMP_LE o MATCH_MP REAL_LET_TRANS)); 324 325val REAL_LE_ANTISYM = store_thm("REAL_LE_ANTISYM", 326 ���!x y. x <= y /\ y <= x = (x = y)���, 327 REPEAT GEN_TAC THEN EQ_TAC THENL 328 [REWRITE_TAC[real_lte] THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 329 (SPECL [���x:real���, ���y:real���] REAL_LT_TOTAL) THEN 330 ASM_REWRITE_TAC[], 331 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_LE_REFL]]); 332 333val REAL_LET_ANTISYM = store_thm("REAL_LET_ANTISYM", 334 ���!x y. ~(x < y /\ y <= x)���, 335 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN 336 BOOL_CASES_TAC ���x < y��� THEN REWRITE_TAC[]); 337 338val REAL_LTE_ANTISYM = store_thm("REAL_LTE_ANTISYM", 339 ���!x y. ~(x <= y /\ y < x)���, 340 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN 341 MATCH_ACCEPT_TAC REAL_LET_ANTISYM); 342 343(* old name with typo *) 344val REAL_LTE_ANTSYM = save_thm 345 ("REAL_LTE_ANTSYM", REAL_LTE_ANTISYM); 346 347val REAL_NEG_LT0 = store_thm("REAL_NEG_LT0", 348 ���!x. ~x < 0 = 0 < x���, 349 GEN_TAC THEN 350 SUBST1_TAC(SYM(SPECL [���~x���, ���0���, ���x:real���] REAL_LT_RADD)) 351 THEN REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID]); 352val _ = export_rewrites ["REAL_NEG_LT0"] 353 354val REAL_NEG_GT0 = store_thm("REAL_NEG_GT0", 355 ���!x. 0 < ~x = x < 0���, 356 GEN_TAC THEN REWRITE_TAC[GSYM REAL_NEG_LT0, REAL_NEGNEG]); 357val _ = export_rewrites ["REAL_NEG_GT0"] 358 359val REAL_NEG_LE0 = store_thm("REAL_NEG_LE0", 360 ���!x. ~x <= 0 = 0 <= x���, 361 GEN_TAC THEN REWRITE_TAC[real_lte] THEN 362 REWRITE_TAC[REAL_NEG_GT0]); 363val _ = export_rewrites ["REAL_NEG_LE0"] 364 365val REAL_NEG_GE0 = store_thm("REAL_NEG_GE0", 366 ���!x. 0 <= ~x = x <= 0���, 367 GEN_TAC THEN REWRITE_TAC[real_lte] THEN 368 REWRITE_TAC[REAL_NEG_LT0]); 369val _ = export_rewrites ["REAL_NEG_GE0"] 370 371val REAL_LT_NEGTOTAL = store_thm("REAL_LT_NEGTOTAL", 372 ���!x. (x = 0) \/ (0 < x) \/ (0 < ~x)���, 373 GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 374 (SPECL [���x:real���, ���0���] REAL_LT_TOTAL) THEN 375 ASM_REWRITE_TAC[SYM(REWRITE_RULE[REAL_NEGNEG] 376 (SPEC ���~x��� REAL_NEG_LT0))]); 377 378val REAL_LE_NEGTOTAL = store_thm("REAL_LE_NEGTOTAL", 379 ���!x. 0 <= x \/ 0 <= ~x���, 380 GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN 381 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 382 (SPEC ���x:real��� REAL_LT_NEGTOTAL) THEN 383 ASM_REWRITE_TAC[]); 384 385val REAL_LE_MUL = store_thm("REAL_LE_MUL", 386 ���!x y. 0 <= x /\ 0 <= y ==> 0 <= (x * y)���, 387 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN 388 MAP_EVERY ASM_CASES_TAC [���0 = x���, ���0 = y���] THEN 389 ASM_REWRITE_TAC[] THEN TRY(FIRST_ASSUM(SUBST1_TAC o SYM)) THEN 390 REWRITE_TAC[REAL_MUL_LZERO, REAL_MUL_RZERO] THEN 391 DISCH_TAC THEN DISJ1_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN 392 ASM_REWRITE_TAC[]); 393 394val REAL_LE_SQUARE = store_thm("REAL_LE_SQUARE", 395 ���!x. 0 <= x * x���, 396 GEN_TAC THEN DISJ_CASES_TAC (SPEC ���x:real��� REAL_LE_NEGTOTAL) THEN 397 POP_ASSUM(MP_TAC o MATCH_MP REAL_LE_MUL o W CONJ) THEN 398 REWRITE_TAC[GSYM REAL_NEG_RMUL, GSYM REAL_NEG_LMUL, REAL_NEGNEG]); 399 400val REAL_LE_01 = store_thm("REAL_LE_01", 401 ���0 <= &1���, 402 SUBST1_TAC(SYM(SPEC ���&1��� REAL_MUL_LID)) THEN 403 MATCH_ACCEPT_TAC REAL_LE_SQUARE); 404 405val REAL_LT_01 = store_thm("REAL_LT_01", 406 ���0 < &1���, 407 REWRITE_TAC[REAL_LT_LE, REAL_LE_01] THEN 408 CONV_TAC(RAND_CONV SYM_CONV) THEN 409 REWRITE_TAC[REAL_10]); 410 411val REAL_LE_LADD = store_thm("REAL_LE_LADD", 412 ���!x y z. (x + y) <= (x + z) = y <= z���, 413 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN 414 AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_LT_LADD); 415val _ = export_rewrites ["REAL_LE_LADD"] 416 417val REAL_LE_RADD = store_thm("REAL_LE_RADD", 418 ���!x y z. (x + z) <= (y + z) = x <= y���, 419 REPEAT GEN_TAC THEN REWRITE_TAC[real_lte] THEN 420 AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_LT_RADD); 421val _ = export_rewrites ["REAL_LE_RADD"] 422 423val REAL_LT_ADD2 = store_thm("REAL_LT_ADD2", 424 ���!w x y z. w < x /\ y < z ==> (w + y) < (x + z)���, 425 REPEAT GEN_TAC THEN DISCH_TAC THEN 426 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC ���w + z��� THEN 427 ASM_REWRITE_TAC[REAL_LT_LADD, REAL_LT_RADD]); 428 429val REAL_LE_ADD2 = store_thm("REAL_LE_ADD2", 430 ���!w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z)���, 431 REPEAT GEN_TAC THEN DISCH_TAC THEN 432 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���w + z��� THEN 433 ASM_REWRITE_TAC[REAL_LE_LADD, REAL_LE_RADD]); 434 435val REAL_LE_ADD = store_thm("REAL_LE_ADD", 436 ���!x y. 0 <= x /\ 0 <= y ==> 0 <= (x + y)���, 437 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_ADD2) THEN 438 REWRITE_TAC[REAL_ADD_LID]); 439 440val REAL_LT_ADD = store_thm("REAL_LT_ADD", 441 ���!x y. 0 < x /\ 0 < y ==> 0 < (x + y)���, 442 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_ADD2) THEN 443 REWRITE_TAC[REAL_ADD_LID]); 444 445val REAL_LT_ADDNEG = store_thm("REAL_LT_ADDNEG", 446 ���!x y z. y < x + ~z = y+z < x���, 447 REPEAT GEN_TAC THEN SUBST1_TAC 448 (SYM(SPECL [���y:real���, ���x + ~z���, ���z:real���] REAL_LT_RADD)) 449 THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_RID]); 450 451val REAL_LT_ADDNEG2 = store_thm("REAL_LT_ADDNEG2", 452 ���!x y z. (x + ~y) < z = x < (z + y)���, 453 REPEAT GEN_TAC THEN 454 SUBST1_TAC(SYM(SPECL [���x + ~y���, ���z:real���, ���y:real���] REAL_LT_RADD)) THEN 455 REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_RID]); 456 457val REAL_LT_ADD1 = store_thm("REAL_LT_ADD1", 458 ���!x y. x <= y ==> x < (y + &1)���, 459 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN 460 DISCH_THEN DISJ_CASES_TAC THENL 461 [POP_ASSUM(MP_TAC o MATCH_MP REAL_LT_ADD2 o C CONJ REAL_LT_01) THEN 462 REWRITE_TAC[REAL_ADD_RID], 463 POP_ASSUM SUBST1_TAC THEN 464 GEN_REWR_TAC LAND_CONV [GSYM REAL_ADD_RID] THEN 465 REWRITE_TAC[REAL_LT_LADD, REAL_LT_01]]); 466 467val REAL_SUB_ADD = store_thm("REAL_SUB_ADD", 468 ���!x y. (x - y) + y = x���, 469 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, GSYM REAL_ADD_ASSOC, 470 REAL_ADD_LINV, REAL_ADD_RID]); 471 472val REAL_SUB_ADD2 = store_thm("REAL_SUB_ADD2", 473 ���!x y. y + (x - y) = x���, 474 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 475 MATCH_ACCEPT_TAC REAL_SUB_ADD); 476 477val REAL_SUB_REFL = store_thm("REAL_SUB_REFL", 478 ���!x. x - x = 0���, 479 GEN_TAC THEN REWRITE_TAC[real_sub, REAL_ADD_RINV]); 480val _ = export_rewrites ["REAL_SUB_REFL"] 481 482val REAL_SUB_0 = store_thm("REAL_SUB_0", 483 ���!x y. (x - y = 0) = (x = y)���, 484 REPEAT GEN_TAC THEN EQ_TAC THENL 485 [DISCH_THEN(MP_TAC o C AP_THM ���y:real��� o AP_TERM ���$+���) THEN 486 REWRITE_TAC[REAL_SUB_ADD, REAL_ADD_LID], 487 DISCH_THEN SUBST1_TAC THEN MATCH_ACCEPT_TAC REAL_SUB_REFL]); 488val _ = export_rewrites ["REAL_SUB_0"] 489 490val REAL_LE_DOUBLE = store_thm("REAL_LE_DOUBLE", 491 ���!x. 0 <= x + x = 0 <= x���, 492 GEN_TAC THEN EQ_TAC THENL 493 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_NOT_LE] THEN 494 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_ADD2 o W CONJ), 495 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_ADD2 o W CONJ)] THEN 496 REWRITE_TAC[REAL_ADD_LID]); 497 498val REAL_LE_NEGL = store_thm("REAL_LE_NEGL", 499 ���!x. (~x <= x) = (0 <= x)���, 500 GEN_TAC THEN SUBST1_TAC 501 (SYM(SPECL [���x:real���, ���~x���, ���x:real���] REAL_LE_LADD)) 502 THEN REWRITE_TAC[REAL_ADD_RINV, REAL_LE_DOUBLE]); 503 504val REAL_LE_NEGR = store_thm("REAL_LE_NEGR", 505 ���!x. (x <= ~x) = (x <= 0)���, 506 GEN_TAC THEN SUBST1_TAC(SYM(SPEC ���x:real��� REAL_NEGNEG)) THEN 507 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [REAL_NEGNEG] THEN 508 REWRITE_TAC[REAL_LE_NEGL] THEN REWRITE_TAC[REAL_NEG_GE0] THEN 509 REWRITE_TAC[REAL_NEGNEG]); 510 511val REAL_NEG_EQ0 = store_thm("REAL_NEG_EQ0", 512 ���!x. (~x = 0) = (x = 0)���, 513 GEN_TAC THEN EQ_TAC THENL 514 [DISCH_THEN(MP_TAC o AP_TERM ���$+ x���), 515 DISCH_THEN(MP_TAC o AP_TERM ���$+ ~x���)] THEN 516 REWRITE_TAC[REAL_ADD_RINV, REAL_ADD_LINV, REAL_ADD_RID] THEN 517 DISCH_THEN SUBST1_TAC THEN REFL_TAC); 518 519val REAL_NEG_0 = store_thm("REAL_NEG_0", 520 ���~0 = 0���, 521 REWRITE_TAC[REAL_NEG_EQ0]); 522val _ = export_rewrites ["REAL_NEG_0"] 523 524val REAL_NEG_SUB = store_thm("REAL_NEG_SUB", 525 ���!x y. ~(x - y) = y - x���, 526 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEGNEG] THEN 527 MATCH_ACCEPT_TAC REAL_ADD_SYM); 528 529val REAL_SUB_LT = store_thm("REAL_SUB_LT", 530 ���!x y. 0 < x - y = y < x���, 531 REPEAT GEN_TAC THEN 532 SUBST1_TAC(SYM(SPECL [���0���, ���x - y���, ���y:real���] 533 REAL_LT_RADD)) THEN 534 REWRITE_TAC[REAL_SUB_ADD, REAL_ADD_LID]); 535 536val REAL_SUB_LE = store_thm("REAL_SUB_LE", 537 ���!x y. 0 <= (x - y) = y <= x���, 538 REPEAT GEN_TAC THEN 539 SUBST1_TAC(SYM(SPECL [���0���, ���x - y���, ���y:real���] 540 REAL_LE_RADD)) THEN 541 REWRITE_TAC[REAL_SUB_ADD, REAL_ADD_LID]); 542 543val REAL_ADD_SUB = store_thm("REAL_ADD_SUB", 544 ���!x y. (x + y) - x = y���, 545 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 546 REWRITE_TAC[real_sub, GSYM REAL_ADD_ASSOC, REAL_ADD_RINV, REAL_ADD_RID]); 547 548val REAL_EQ_LMUL = store_thm("REAL_EQ_LMUL", 549 ���!x y z. (x * y = x * z) = (x = 0) \/ (y = z)���, 550 REPEAT GEN_TAC THEN EQ_TAC THENL 551 [DISCH_THEN(MP_TAC o AP_TERM ���$* (inv x)���) THEN 552 ASM_CASES_TAC ���x = 0��� THEN ASM_REWRITE_TAC[] THEN 553 POP_ASSUM(fn th => REWRITE_TAC[REAL_MUL_ASSOC, MATCH_MP REAL_MUL_LINV th]) THEN 554 REWRITE_TAC[REAL_MUL_LID], 555 DISCH_THEN(DISJ_CASES_THEN SUBST1_TAC) THEN 556 REWRITE_TAC[REAL_MUL_LZERO]]); 557val _ = export_rewrites ["REAL_EQ_LMUL"] 558 559val REAL_EQ_RMUL = store_thm("REAL_EQ_RMUL", 560 ���!x y z. (x * z = y * z) = (z = 0) \/ (x = y)���, 561 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 562 MATCH_ACCEPT_TAC REAL_EQ_LMUL); 563val _ = export_rewrites ["REAL_EQ_RMUL"] 564 565val REAL_SUB_LDISTRIB = store_thm("REAL_SUB_LDISTRIB", 566 ���!x y z. x * (y - z) = (x * y) - (x * z)���, 567 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_LDISTRIB, REAL_NEG_RMUL]); 568 569val REAL_SUB_RDISTRIB = store_thm("REAL_SUB_RDISTRIB", 570 ���!x y z. (x - y) * z = (x * z) - (y * z)���, 571 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 572 MATCH_ACCEPT_TAC REAL_SUB_LDISTRIB); 573 574val REAL_NEG_EQ = store_thm("REAL_NEG_EQ", 575 ���!x y. (~x = y) = (x = ~y)���, 576 REPEAT GEN_TAC THEN EQ_TAC THENL 577 [DISCH_THEN(SUBST1_TAC o SYM), DISCH_THEN SUBST1_TAC] THEN 578 REWRITE_TAC[REAL_NEGNEG]); 579 580val REAL_NEG_MINUS1 = store_thm("REAL_NEG_MINUS1", 581 ���!x. ~x = ~1 * x���, 582 GEN_TAC THEN REWRITE_TAC[GSYM REAL_NEG_LMUL] THEN 583 REWRITE_TAC[REAL_MUL_LID]); 584 585val REAL_INV_NZ = store_thm("REAL_INV_NZ", 586 ���!x. ~(x = 0) ==> ~(inv x = 0)���, 587 GEN_TAC THEN DISCH_TAC THEN 588 DISCH_THEN(MP_TAC o C AP_THM ���x:real��� o AP_TERM ���$*���) THEN 589 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 590 REWRITE_TAC[REAL_MUL_LZERO, REAL_10]); 591 592val REAL_INVINV = store_thm("REAL_INVINV", 593 ���!x. ~(x = 0) ==> (inv (inv x) = x)���, 594 GEN_TAC THEN DISCH_TAC THEN 595 FIRST_ASSUM(MP_TAC o MATCH_MP REAL_MUL_RINV) THEN 596 ASM_CASES_TAC ���inv x = 0��� THEN 597 ASM_REWRITE_TAC[REAL_MUL_RZERO, GSYM REAL_10] THEN 598 MP_TAC(SPECL [���inv(inv x)���, ���x:real���, ���inv x���] REAL_EQ_RMUL) 599 THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN 600 DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN 601 FIRST_ASSUM ACCEPT_TAC); 602 603val REAL_LT_IMP_NE = store_thm("REAL_LT_IMP_NE", 604 ���!x y. x < y ==> ~(x = y)���, 605 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN 606 REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN 607 REWRITE_TAC[REAL_LT_REFL]); 608 609val REAL_INV_POS = store_thm("REAL_INV_POS", 610 ���!x. 0 < x ==> 0 < inv x���, 611 GEN_TAC THEN DISCH_TAC THEN REPEAT_TCL DISJ_CASES_THEN 612 MP_TAC (SPECL [���inv x���, ���0���] REAL_LT_TOTAL) THENL 613 [POP_ASSUM(ASSUME_TAC o MATCH_MP REAL_INV_NZ o 614 GSYM o MATCH_MP REAL_LT_IMP_NE) THEN ASM_REWRITE_TAC[], 615 ONCE_REWRITE_TAC[GSYM REAL_NEG_GT0] THEN 616 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_MUL o C CONJ (ASSUME ���0 < x���)) THEN 617 REWRITE_TAC[GSYM REAL_NEG_LMUL] THEN 618 POP_ASSUM(fn th => REWRITE_TAC 619 [MATCH_MP REAL_MUL_LINV (GSYM (MATCH_MP REAL_LT_IMP_NE th))]) THEN 620 REWRITE_TAC[REAL_NEG_GT0] THEN DISCH_THEN(MP_TAC o CONJ REAL_LT_01) THEN 621 REWRITE_TAC[REAL_LT_ANTISYM], 622 REWRITE_TAC[]]); 623 624val REAL_LT_LMUL_0 = store_thm("REAL_LT_LMUL_0", 625 ���!x y. 0 < x ==> (0 < (x * y) = 0 < y)���, 626 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THENL 627 [FIRST_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ (MATCH_MP REAL_INV_POS th))) THEN 628 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_MUL) THEN 629 REWRITE_TAC[REAL_MUL_ASSOC] THEN 630 FIRST_ASSUM(fn th => REWRITE_TAC 631 [MATCH_MP REAL_MUL_LINV (GSYM (MATCH_MP REAL_LT_IMP_NE th))]) THEN 632 REWRITE_TAC[REAL_MUL_LID], 633 DISCH_TAC THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]]); 634 635val REAL_LT_RMUL_0 = store_thm("REAL_LT_RMUL_0", 636 ���!x y. 0 < y ==> (0 < (x * y) = 0 < x)���, 637 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 638 MATCH_ACCEPT_TAC REAL_LT_LMUL_0); 639 640val REAL_LT_LMUL = store_thm("REAL_LT_LMUL", 641 ���!x y z. 0 < x ==> ((x * y) < (x * z) = y < z)���, 642 REPEAT GEN_TAC THEN DISCH_TAC THEN 643 ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN 644 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB] THEN 645 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC REAL_LT_LMUL_0); 646 647val REAL_LT_RMUL = store_thm("REAL_LT_RMUL", 648 ���!x y z. 0 < z ==> ((x * z) < (y * z) = x < y)���, 649 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 650 MATCH_ACCEPT_TAC REAL_LT_LMUL); 651 652val REAL_LT_RMUL_IMP = store_thm("REAL_LT_RMUL_IMP", 653 ���!x y z. x < y /\ 0 < z ==> (x * z) < (y * z)���, 654 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 655 POP_ASSUM(fn th => REWRITE_TAC[GEN_ALL(MATCH_MP REAL_LT_RMUL th)])); 656 657val REAL_LT_LMUL_IMP = store_thm("REAL_LT_LMUL_IMP", 658 ���!x y z. y < z /\ 0 < x ==> (x * y) < (x * z)���, 659 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 660 POP_ASSUM(fn th => REWRITE_TAC[GEN_ALL(MATCH_MP REAL_LT_LMUL th)])); 661 662val REAL_LINV_UNIQ = store_thm("REAL_LINV_UNIQ", 663 ���!x y. (x * y = &1) ==> (x = inv y)���, 664 REPEAT GEN_TAC THEN ASM_CASES_TAC ���x = 0��� THEN 665 ASM_REWRITE_TAC[REAL_MUL_LZERO, GSYM REAL_10] THEN 666 DISCH_THEN(MP_TAC o AP_TERM ���$* (inv x)���) THEN 667 REWRITE_TAC[REAL_MUL_ASSOC] THEN 668 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 669 REWRITE_TAC[REAL_MUL_LID, REAL_MUL_RID] THEN 670 DISCH_THEN SUBST1_TAC THEN CONV_TAC SYM_CONV THEN 671 POP_ASSUM MP_TAC THEN MATCH_ACCEPT_TAC REAL_INVINV); 672 673val REAL_RINV_UNIQ = store_thm("REAL_RINV_UNIQ", 674 ���!x y. (x * y = &1) ==> (y = inv x)���, 675 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 676 MATCH_ACCEPT_TAC REAL_LINV_UNIQ); 677 678val REAL_INV_INV = store_thm("REAL_INV_INV", 679 Term`!x. inv(inv x) = x`, 680 GEN_TAC THEN ASM_CASES_TAC (Term `x = 0`) THEN 681 ASM_REWRITE_TAC[REAL_INV_0] THEN 682 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN 683 MATCH_MP_TAC REAL_RINV_UNIQ THEN 684 MATCH_MP_TAC REAL_MUL_LINV THEN 685 ASM_REWRITE_TAC[]);; 686 687val REAL_INV_EQ_0 = store_thm("REAL_INV_EQ_0", 688 Term`!x. (inv(x) = 0) = (x = 0)`, 689 GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_INV_0] THEN 690 ONCE_REWRITE_TAC[GSYM REAL_INV_INV] THEN ASM_REWRITE_TAC[REAL_INV_0]);; 691 692val REAL_NEG_INV = store_thm("REAL_NEG_INV", 693 ���!x. ~(x = 0) ==> (~inv x = inv (~x))���, 694 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LINV_UNIQ THEN 695 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] THEN 696 POP_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 697 REWRITE_TAC[REAL_NEGNEG]); 698 699val REAL_INV_1OVER = store_thm("REAL_INV_1OVER", 700 ���!x. inv x = &1 / x���, 701 GEN_TAC THEN REWRITE_TAC[real_div, REAL_MUL_LID]); 702 703val REAL_LT_INV_EQ = store_thm("REAL_LT_INV_EQ", 704 Term`!x. 0 < inv x = 0 < x`, 705 GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[REAL_INV_POS] THEN 706 GEN_REWRITE_TAC (funpow 2 RAND_CONV) [GSYM REAL_INV_INV] THEN 707 REWRITE_TAC[REAL_INV_POS]);; 708 709val REAL_LE_INV_EQ = store_thm("REAL_LE_INV_EQ", 710 Term`!x. 0 <= inv x = 0 <= x`, 711 REWRITE_TAC[REAL_LE_LT, REAL_LT_INV_EQ, REAL_INV_EQ_0] THEN 712 MESON_TAC[REAL_INV_EQ_0]);; 713 714val REAL_LE_INV = store_thm("REAL_LE_INV", 715 Term `!x. 0 <= x ==> 0 <= inv(x)`, 716 REWRITE_TAC[REAL_LE_INV_EQ]);; 717 718val REAL_LE_ADDR = store_thm("REAL_LE_ADDR", 719 ���!x y. x <= x + y = 0 <= y���, 720 REPEAT GEN_TAC THEN 721 SUBST1_TAC(SYM(SPECL [���x:real���, ���0���, ���y:real���] REAL_LE_LADD)) THEN 722 REWRITE_TAC[REAL_ADD_RID]); 723 724val REAL_LE_ADDL = store_thm("REAL_LE_ADDL", 725 ���!x y. y <= x + y = 0 <= x���, 726 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 727 MATCH_ACCEPT_TAC REAL_LE_ADDR); 728 729val REAL_LT_ADDR = store_thm("REAL_LT_ADDR", 730 ���!x y. x < x + y = 0 < y���, 731 REPEAT GEN_TAC THEN 732 SUBST1_TAC(SYM(SPECL [���x:real���, ���0���, ���y:real���] REAL_LT_LADD)) THEN 733 REWRITE_TAC[REAL_ADD_RID]); 734 735val REAL_LT_ADDL = store_thm("REAL_LT_ADDL", 736 ���!x y. y < x + y = 0 < x���, 737 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 738 MATCH_ACCEPT_TAC REAL_LT_ADDR); 739 740(*---------------------------------------------------------------------------*) 741(* Prove homomorphisms for the inclusion map *) 742(*---------------------------------------------------------------------------*) 743 744val REAL = store_thm("REAL", 745 ���!n. &(SUC n) = &n + &1���, 746 GEN_TAC THEN REWRITE_TAC[real_of_num] THEN 747 REWRITE_TAC[REAL_1]); 748 749val REAL_POS = store_thm("REAL_POS", 750 ���!n. 0 <= &n���, 751 INDUCT_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN 752 MATCH_MP_TAC REAL_LE_TRANS THEN 753 EXISTS_TAC ���&n��� THEN ASM_REWRITE_TAC[REAL] THEN 754 REWRITE_TAC[REAL_LE_ADDR, REAL_LE_01]); 755val _ = export_rewrites ["REAL_POS"] 756 757val REAL_LE = store_thm("REAL_LE", 758 ���!m n. &m <= &n = m <= n���, 759 REPEAT INDUCT_TAC THEN ASM_REWRITE_TAC 760 [REAL, REAL_LE_RADD, ZERO_LESS_EQ, LESS_EQ_MONO, REAL_LE_REFL] THEN 761 REWRITE_TAC[GSYM NOT_LESS, LESS_0] THENL 762 [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC ���&n��� THEN 763 ASM_REWRITE_TAC[ZERO_LESS_EQ, REAL_LE_ADDR, REAL_LE_01], 764 DISCH_THEN(MP_TAC o C CONJ (SPEC ���m:num��� REAL_POS)) THEN 765 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_TRANS) THEN 766 REWRITE_TAC[REAL_NOT_LE, REAL_LT_ADDR, REAL_LT_01]]); 767val _ = export_rewrites ["REAL_LE"] 768 769val REAL_LT = store_thm("REAL_LT", 770 ���!m n. &m < &n = m < n���, 771 REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC 772 ((REWRITE_RULE[] o AP_TERM ���$~:bool->bool��� o 773 REWRITE_RULE[GSYM NOT_LESS, GSYM REAL_NOT_LT]) (SPEC_ALL REAL_LE))); 774val _ = export_rewrites ["REAL_LT"] 775 776val REAL_INJ = store_thm("REAL_INJ", 777 ���!m n. (&m = &n) = (m = n)���, 778 let val th = prove(���(m:num = n) = m <= n /\ n <= m���, 779 EQ_TAC THENL 780 [DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[LESS_EQ_REFL], 781 MATCH_ACCEPT_TAC LESS_EQUAL_ANTISYM]) in 782 REPEAT GEN_TAC THEN REWRITE_TAC[th, GSYM REAL_LE_ANTISYM, REAL_LE] end); 783val _ = export_rewrites ["REAL_INJ"] 784 785val REAL_ADD = store_thm("REAL_ADD", 786 ���!m n. &m + &n = &(m + n)���, 787 INDUCT_TAC THEN REWRITE_TAC[REAL, ADD, REAL_ADD_LID] THEN 788 RULE_ASSUM_TAC GSYM THEN GEN_TAC THEN ASM_REWRITE_TAC[] THEN 789 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 790val _ = export_rewrites ["REAL_ADD"] 791 792val REAL_MUL = store_thm("REAL_MUL", 793 ���!m n. &m * &n = &(m * n)���, 794 INDUCT_TAC THEN REWRITE_TAC[REAL_MUL_LZERO, MULT_CLAUSES, REAL, 795 GSYM REAL_ADD, REAL_RDISTRIB] THEN 796 FIRST_ASSUM(fn th => REWRITE_TAC[GSYM th]) THEN 797 REWRITE_TAC[REAL_MUL_LID]); 798val _ = export_rewrites ["REAL_MUL"] 799 800(*---------------------------------------------------------------------------*) 801(* Now more theorems *) 802(*---------------------------------------------------------------------------*) 803 804val REAL_INV1 = store_thm("REAL_INV1", 805 ���inv(&1) = &1���, 806 CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_LINV_UNIQ THEN 807 REWRITE_TAC[REAL_MUL_LID]); 808 809val REAL_OVER1 = store_thm("REAL_OVER1", 810 ���!x. x / &1 = x���, 811 GEN_TAC THEN REWRITE_TAC[real_div, REAL_INV1, REAL_MUL_RID]); 812val _ = export_rewrites ["REAL_OVER1"] 813 814val REAL_DIV_REFL = store_thm("REAL_DIV_REFL", 815 ���!x. ~(x = 0) ==> (x / x = &1)���, 816 GEN_TAC THEN REWRITE_TAC[real_div, REAL_MUL_RINV]); 817 818val REAL_DIV_LZERO = store_thm("REAL_DIV_LZERO", 819 ���!x. 0 / x = 0���, 820 REPEAT GEN_TAC THEN REWRITE_TAC[real_div, REAL_MUL_LZERO]); 821 822val REAL_LT_NZ = store_thm("REAL_LT_NZ", 823 ���!n. ~(&n = 0) = (0 < &n)���, 824 GEN_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN 825 CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN 826 ASM_CASES_TAC ���&n = 0��� THEN ASM_REWRITE_TAC[REAL_LE_REFL, REAL_POS]); 827 828val REAL_NZ_IMP_LT = store_thm("REAL_NZ_IMP_LT", 829 ���!n. ~(n = 0) ==> 0 < &n���, 830 GEN_TAC THEN REWRITE_TAC[GSYM REAL_INJ, REAL_LT_NZ]); 831 832val REAL_LT_RDIV_0 = store_thm("REAL_LT_RDIV_0", 833 ���!y z. 0 < z ==> (0 < (y / z) = 0 < y)���, 834 REPEAT GEN_TAC THEN DISCH_TAC THEN 835 REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LT_RMUL_0 THEN 836 MATCH_MP_TAC REAL_INV_POS THEN POP_ASSUM ACCEPT_TAC); 837 838val REAL_LT_RDIV = store_thm("REAL_LT_RDIV", 839 ���!x y z. 0 < z ==> ((x / z) < (y / z) = x < y)���, 840 REPEAT GEN_TAC THEN DISCH_TAC THEN 841 REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LT_RMUL THEN 842 MATCH_MP_TAC REAL_INV_POS THEN POP_ASSUM ACCEPT_TAC); 843 844val REAL_LT_FRACTION_0 = store_thm("REAL_LT_FRACTION_0", 845 ���!n d. ~(n = 0) ==> (0 < (d / &n) = 0 < d)���, 846 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LT_RDIV_0 THEN 847 ASM_REWRITE_TAC[GSYM REAL_LT_NZ, REAL_INJ]); 848 849val REAL_LT_MULTIPLE = store_thm("REAL_LT_MULTIPLE", 850 ���!(n:num) d. 1 < n ==> (d < (&n * d) = 0 < d)���, 851 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN INDUCT_TAC THENL 852 [REWRITE_TAC[num_CONV ���1:num���, NOT_LESS_0], 853 POP_ASSUM MP_TAC THEN ASM_CASES_TAC ���1 < n:num��� THEN 854 ASM_REWRITE_TAC[] THENL 855 [DISCH_TAC THEN GEN_TAC THEN DISCH_THEN(K ALL_TAC) THEN 856 REWRITE_TAC[REAL, REAL_LDISTRIB, REAL_MUL_RID, REAL_LT_ADDL] THEN 857 MATCH_MP_TAC REAL_LT_RMUL_0 THEN REWRITE_TAC[REAL_LT] THEN 858 MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC ���1:num��� THEN 859 ASM_REWRITE_TAC[] THEN REWRITE_TAC[num_CONV ���1:num���, LESS_0], 860 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP LESS_LEMMA1) THEN 861 ASM_REWRITE_TAC[] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN 862 REWRITE_TAC[REAL, REAL_LDISTRIB, REAL_MUL_RID] THEN 863 REWRITE_TAC[REAL_LT_ADDL]]]); 864 865val REAL_LT_FRACTION = store_thm("REAL_LT_FRACTION", 866 ���!(n:num) d. 1<n ==> ((d / &n) < d = 0 < d)���, 867 REPEAT GEN_TAC THEN ASM_CASES_TAC ���n = 0:num��� THEN 868 ASM_REWRITE_TAC[NOT_LESS_0] THEN DISCH_TAC THEN 869 UNDISCH_TAC ���1 < n:num��� THEN 870 FIRST_ASSUM(fn th => let val th1 = REWRITE_RULE[GSYM REAL_INJ] th in 871 MAP_EVERY ASSUME_TAC [th1, REWRITE_RULE[REAL_LT_NZ] th1] end) THEN 872 FIRST_ASSUM(fn th => GEN_REWR_TAC (RAND_CONV o LAND_CONV) 873 [GSYM(MATCH_MP REAL_LT_RMUL th)]) THEN 874 REWRITE_TAC[real_div, GSYM REAL_MUL_ASSOC] THEN 875 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 876 REWRITE_TAC[REAL_MUL_RID] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 877 MATCH_ACCEPT_TAC REAL_LT_MULTIPLE); 878 879val REAL_LT_HALF1 = store_thm("REAL_LT_HALF1", 880 ���!d. 0 < (d / &2) = 0 < d���, 881 GEN_TAC THEN MATCH_MP_TAC REAL_LT_FRACTION_0 THEN 882 REWRITE_TAC[num_CONV ���2:num���, NOT_SUC]); 883 884val REAL_LT_HALF2 = store_thm("REAL_LT_HALF2", 885 ���!d. (d / &2) < d = 0 < d���, 886 GEN_TAC THEN MATCH_MP_TAC REAL_LT_FRACTION THEN 887 CONV_TAC(RAND_CONV num_CONV) THEN 888 REWRITE_TAC[LESS_SUC_REFL]); 889 890val REAL_DOUBLE = store_thm("REAL_DOUBLE", 891 ���!x. x + x = &2 * x���, 892 GEN_TAC THEN REWRITE_TAC[num_CONV ���2:num���, REAL] THEN 893 REWRITE_TAC[REAL_RDISTRIB, REAL_MUL_LID]); 894 895val REAL_DIV_LMUL = store_thm("REAL_DIV_LMUL", 896 ���!x y. ~(y = 0) ==> (y * (x / y) = x)���, 897 REPEAT GEN_TAC THEN DISCH_TAC THEN 898 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 899 REWRITE_TAC[real_div] THEN 900 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN 901 FIRST_ASSUM(SUBST1_TAC o MATCH_MP REAL_MUL_LINV) THEN 902 REWRITE_TAC[REAL_MUL_RID]); 903 904val REAL_DIV_RMUL = store_thm("REAL_DIV_RMUL", 905 ���!x y. ~(y = 0) ==> ((x / y) * y = x)���, 906 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 907 MATCH_ACCEPT_TAC REAL_DIV_LMUL); 908 909val REAL_HALF_DOUBLE = store_thm("REAL_HALF_DOUBLE", 910 ���!x. (x / &2) + (x / &2) = x���, 911 GEN_TAC THEN REWRITE_TAC[REAL_DOUBLE] THEN 912 MATCH_MP_TAC REAL_DIV_LMUL THEN REWRITE_TAC[REAL_INJ] THEN 913 CONV_TAC(ONCE_DEPTH_CONV num_EQ_CONV) THEN REWRITE_TAC[]); 914 915val REAL_DOWN = store_thm("REAL_DOWN", 916 ���!x. 0 < x ==> ?y. 0 < y /\ y < x���, 917 GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC ���x / &2��� THEN 918 ASM_REWRITE_TAC[REAL_LT_HALF1, REAL_LT_HALF2]); 919 920val REAL_DOWN2 = store_thm("REAL_DOWN2", 921 ���!x y. 0 < x /\ 0 < y ==> ?z. 0 < z /\ z < x /\ z < y���, 922 REPEAT GEN_TAC THEN 923 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 924 (SPECL [���x:real���, ���y:real���] REAL_LT_TOTAL) THENL 925 [ASM_REWRITE_TAC[REAL_DOWN], 926 DISCH_THEN(X_CHOOSE_TAC ���z:real��� o MATCH_MP REAL_DOWN o CONJUNCT1), 927 DISCH_THEN(X_CHOOSE_TAC ���z:real��� o MATCH_MP REAL_DOWN o CONJUNCT2)] THEN 928 EXISTS_TAC ���z:real��� THEN ASM_REWRITE_TAC[] THEN 929 MATCH_MP_TAC REAL_LT_TRANS THENL 930 [EXISTS_TAC ���x:real���, EXISTS_TAC ���y:real���] THEN 931 ASM_REWRITE_TAC[]); 932 933val REAL_SUB_SUB = store_thm("REAL_SUB_SUB", 934 ���!x y. (x - y) - x = ~y���, 935 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub] THEN 936 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 937 ���(a + b) + c = (c + a) + b���] THEN 938 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID]); 939 940val REAL_LT_ADD_SUB = store_thm("REAL_LT_ADD_SUB", 941 ���!x y z. (x + y) < z = x < (z - y)���, 942 REPEAT GEN_TAC THEN 943 SUBST1_TAC(SYM(SPECL [���x:real���, ���z - y���, ���y:real���] 944 REAL_LT_RADD)) THEN 945 REWRITE_TAC[REAL_SUB_ADD]); 946 947val REAL_LT_SUB_RADD = store_thm("REAL_LT_SUB_RADD", 948 ���!x y z. (x - y) < z = x < z + y���, 949 REPEAT GEN_TAC THEN 950 SUBST1_TAC(SYM(SPECL [���x - y���, ���z:real���, ���y:real���] REAL_LT_RADD)) THEN 951 REWRITE_TAC[REAL_SUB_ADD]); 952 953val REAL_LT_SUB_LADD = store_thm("REAL_LT_SUB_LADD", 954 ���!x y z. x < (y - z) = (x + z) < y���, 955 REPEAT GEN_TAC THEN 956 SUBST1_TAC(SYM(SPECL [���x + z���, ���y:real���, ���~z���] REAL_LT_RADD)) THEN 957 REWRITE_TAC[real_sub, GSYM REAL_ADD_ASSOC, REAL_ADD_RINV, REAL_ADD_RID]); 958 959val REAL_LE_SUB_LADD = store_thm("REAL_LE_SUB_LADD", 960 ���!x y z. x <= (y - z) = (x + z) <= y���, 961 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT, REAL_LT_SUB_RADD]); 962 963val REAL_LE_SUB_RADD = store_thm("REAL_LE_SUB_RADD", 964 ���!x y z. (x - y) <= z = x <= z + y���, 965 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT, REAL_LT_SUB_LADD]); 966 967val REAL_LT_NEG = store_thm("REAL_LT_NEG", 968 ���!x y. ~x < ~y = y < x���, 969 REPEAT GEN_TAC THEN 970 SUBST1_TAC(SYM(SPECL[���~x���, ���~y���, ���x + y���] REAL_LT_RADD)) THEN 971 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID] THEN 972 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 973 REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_RINV, REAL_ADD_LID]); 974val _ = export_rewrites ["REAL_LT_NEG"] 975 976val REAL_LE_NEG = store_thm("REAL_LE_NEG", 977 ���!x y. ~x <= ~y = y <= x���, 978 REPEAT GEN_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LT] THEN 979 REWRITE_TAC[REAL_LT_NEG]); 980val _ = export_rewrites ["REAL_LE_NEG"] 981 982val REAL_ADD2_SUB2 = store_thm("REAL_ADD2_SUB2", 983 ���!a b c d. (a + b) - (c + d) = (a - c) + (b - d)���, 984 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD] THEN 985 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 986 987val REAL_SUB_LZERO = store_thm("REAL_SUB_LZERO", 988 ���!x. 0 - x = ~x���, 989 GEN_TAC THEN REWRITE_TAC[real_sub, REAL_ADD_LID]); 990val _ = export_rewrites ["REAL_SUB_LZERO"] 991 992val REAL_SUB_RZERO = store_thm("REAL_SUB_RZERO", 993 ���!x. x - 0 = x���, 994 GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_0, REAL_ADD_RID]); 995val _ = export_rewrites ["REAL_SUB_RZERO"] 996 997val REAL_LET_ADD2 = store_thm("REAL_LET_ADD2", 998 ���!w x y z. w <= x /\ y < z ==> (w + y) < (x + z)���, 999 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 1000 MATCH_MP_TAC REAL_LTE_TRANS THEN 1001 EXISTS_TAC ���w + z��� THEN 1002 ASM_REWRITE_TAC[REAL_LE_RADD, REAL_LT_LADD]); 1003 1004val REAL_LTE_ADD2 = store_thm("REAL_LTE_ADD2", 1005 ���!w x y z. w < x /\ y <= z ==> (w + y) < (x + z)���, 1006 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN 1007 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 1008 MATCH_ACCEPT_TAC REAL_LET_ADD2); 1009 1010val REAL_LET_ADD = store_thm("REAL_LET_ADD", 1011 ���!x y. 0 <= x /\ 0 < y ==> 0 < (x + y)���, 1012 REPEAT GEN_TAC THEN DISCH_TAC THEN 1013 SUBST1_TAC(SYM(SPEC ���0��� REAL_ADD_LID)) THEN 1014 MATCH_MP_TAC REAL_LET_ADD2 THEN 1015 ASM_REWRITE_TAC[]); 1016 1017val REAL_LTE_ADD = store_thm("REAL_LTE_ADD", 1018 ���!x y. 0 < x /\ 0 <= y ==> 0 < (x + y)���, 1019 REPEAT GEN_TAC THEN DISCH_TAC THEN 1020 SUBST1_TAC(SYM(SPEC ���0��� REAL_ADD_LID)) THEN 1021 MATCH_MP_TAC REAL_LTE_ADD2 THEN 1022 ASM_REWRITE_TAC[]); 1023 1024val REAL_LT_MUL2 = store_thm("REAL_LT_MUL2", 1025 ���!x1 x2 y1 y2. 0 <= x1 /\ 0 <= y1 /\ x1 < x2 /\ y1 < y2 ==> 1026 (x1 * y1) < (x2 * y2)���, 1027 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN 1028 REWRITE_TAC[REAL_SUB_RZERO] THEN 1029 SUBGOAL_THEN ���!a b c d. 1030 (a * b) - (c * d) = ((a * b) - (a * d)) + ((a * d) - (c * d))��� 1031 MP_TAC THENL 1032 [REPEAT GEN_TAC THEN REWRITE_TAC[real_sub] THEN 1033 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1034 ���(a + b) + (c + d) = (b + c) + (a + d)���] THEN 1035 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID], 1036 DISCH_THEN(fn th => ONCE_REWRITE_TAC[th]) THEN 1037 REWRITE_TAC[GSYM REAL_SUB_LDISTRIB, GSYM REAL_SUB_RDISTRIB] THEN 1038 DISCH_THEN STRIP_ASSUME_TAC THEN 1039 MATCH_MP_TAC REAL_LTE_ADD THEN CONJ_TAC THENL 1040 [MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[] THEN 1041 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���x1:real��� THEN 1042 ASM_REWRITE_TAC[] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN 1043 ASM_REWRITE_TAC[], 1044 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[] THEN 1045 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]]]); 1046 1047val REAL_LT_INV = store_thm("REAL_LT_INV", 1048 ���!x y. 0 < x /\ x < y ==> inv y < inv x���, 1049 REPEAT GEN_TAC THEN 1050 DISCH_THEN STRIP_ASSUME_TAC THEN 1051 SUBGOAL_THEN ���0 < y��� ASSUME_TAC THENL 1052 [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC ���x:real��� THEN 1053 ASM_REWRITE_TAC[], ALL_TAC] THEN 1054 SUBGOAL_THEN ���0 < (x * y)��� ASSUME_TAC THENL 1055 [MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 1056 SUBGOAL_THEN ���(inv y) < (inv x) = 1057 ((x * y) * (inv y)) < ((x * y) * (inv x))��� SUBST1_TAC 1058 THENL 1059 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_LT_LMUL THEN 1060 ASM_REWRITE_TAC[], ALL_TAC] THEN 1061 REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN 1062 SUBGOAL_THEN ���(x * (inv x) = &1) /\ (y * (inv y) = &1)��� 1063 STRIP_ASSUME_TAC THENL 1064 [CONJ_TAC THEN MATCH_MP_TAC REAL_MUL_RINV THEN 1065 CONV_TAC(RAND_CONV SYM_CONV) THEN MATCH_MP_TAC REAL_LT_IMP_NE THEN 1066 ASM_REWRITE_TAC[], ALL_TAC] THEN 1067 ASM_REWRITE_TAC[REAL_MUL_RID] THEN 1068 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 1069 ���x * (y * z) = (x * z) * y���] THEN 1070 ASM_REWRITE_TAC[REAL_MUL_LID]); 1071 1072val REAL_SUB_LNEG = store_thm("REAL_SUB_LNEG", 1073 ���!x y. ~x - y = ~(x + y)���, 1074 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEG_ADD]); 1075 1076val REAL_SUB_RNEG = store_thm("REAL_SUB_RNEG", 1077 ���!x y. x - ~y = x + y���, 1078 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, REAL_NEGNEG]); 1079 1080val REAL_SUB_NEG2 = store_thm("REAL_SUB_NEG2", 1081 ���!x y. ~x - ~y = y - x���, 1082 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_SUB_LNEG] THEN 1083 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_NEGNEG] THEN 1084 MATCH_ACCEPT_TAC REAL_ADD_SYM); 1085 1086val REAL_SUB_TRIANGLE = store_thm("REAL_SUB_TRIANGLE", 1087 ���!a b c. (a - b) + (b - c) = a - c���, 1088 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub] THEN 1089 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1090 ���(a + b) + (c + d) = (b + c) + (a + d)���] THEN 1091 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID]); 1092 1093val REAL_EQ_SUB_LADD = store_thm("REAL_EQ_SUB_LADD", 1094 ���!x y z. (x = y - z) = (x + z = y)���, 1095 REPEAT GEN_TAC THEN (SUBST1_TAC o SYM o C SPECL REAL_EQ_RADD) 1096 [���x:real���, ���y - z���, ���z:real���] THEN REWRITE_TAC[REAL_SUB_ADD]); 1097 1098val REAL_EQ_SUB_RADD = store_thm("REAL_EQ_SUB_RADD", 1099 ���!x y z. (x - y = z) = (x = z + y)���, 1100 REPEAT GEN_TAC THEN CONV_TAC(SUB_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN 1101 MATCH_ACCEPT_TAC REAL_EQ_SUB_LADD); 1102 1103val REAL_INV_MUL = store_thm("REAL_INV_MUL", 1104 ���!x y. ~(x = 0) /\ ~(y = 0) ==> 1105 (inv(x * y) = inv(x) * inv(y))���, 1106 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 1107 CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_RINV_UNIQ THEN 1108 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 1109 ���(a * b) * (c * d) = (c * a) * (d * b)���] THEN 1110 GEN_REWR_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN 1111 BINOP_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[]); 1112 1113(* Stronger version 1114val REAL_INV_MUL = store_thm("REAL_INV_MUL", 1115 Term`!x y. inv(x * y) = inv(x) * inv(y)`, 1116 REPEAT GEN_TAC THEN 1117 MAP_EVERY ASM_CASES_TAC [Term`x = 0`, Term`y = 0`] THEN 1118 ASM_REWRITE_TAC[REAL_INV_0, REAL_MUL_LZERO, REAL_MUL_RZERO] THEN 1119 MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN 1120 ONCE_REWRITE_TAC 1121 [AC REAL_MUL_AC (Term`(a * b) * (c * d) = (a * c) * (b * d)`)] THEN 1122 EVERY_ASSUM(SUBST1_TAC o MATCH_MP REAL_MUL_LINV) THEN 1123 REWRITE_TAC[REAL_MUL_LID]) 1124*) 1125 1126val REAL_LE_LMUL = store_thm("REAL_LE_LMUL", 1127 ���!x y z. 0 < x ==> ((x * y) <= (x * z) = y <= z)���, 1128 REPEAT GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NOT_LT] THEN 1129 AP_TERM_TAC THEN MATCH_MP_TAC REAL_LT_LMUL THEN ASM_REWRITE_TAC[]); 1130 1131val REAL_LE_RMUL = store_thm("REAL_LE_RMUL", 1132 ���!x y z. 0 < z ==> ((x * z) <= (y * z) = x <= y)���, 1133 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 1134 MATCH_ACCEPT_TAC REAL_LE_LMUL); 1135 1136val REAL_SUB_INV2 = store_thm("REAL_SUB_INV2", 1137 ���!x y. ~(x = 0) /\ ~(y = 0) ==> 1138 (inv(x) - inv(y) = (y - x) / (x * y))���, 1139 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 1140 REWRITE_TAC[real_div, REAL_SUB_RDISTRIB] THEN 1141 SUBGOAL_THEN ���inv(x * y) = inv(x) * inv(y)��� SUBST1_TAC THENL 1142 [MATCH_MP_TAC REAL_INV_MUL THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 1143 REWRITE_TAC[REAL_MUL_ASSOC] THEN 1144 EVERY_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_RINV th]) THEN 1145 REWRITE_TAC[REAL_MUL_LID] THEN AP_THM_TAC THEN AP_TERM_TAC THEN 1146 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN 1147 EVERY_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 1148 REWRITE_TAC[REAL_MUL_LID]); 1149 1150val REAL_SUB_SUB2 = store_thm("REAL_SUB_SUB2", 1151 ���!x y. x - (x - y) = y���, 1152 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NEGNEG] THEN 1153 AP_TERM_TAC THEN REWRITE_TAC[REAL_NEG_SUB, REAL_SUB_SUB]); 1154 1155val REAL_ADD_SUB2 = store_thm("REAL_ADD_SUB2", 1156 ���!x y. x - (x + y) = ~y���, 1157 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_NEG_SUB] THEN 1158 AP_TERM_TAC THEN REWRITE_TAC[REAL_ADD_SUB]); 1159 1160val REAL_MEAN = store_thm("REAL_MEAN", 1161 ���!x y. x < y ==> ?z. x < z /\ z < y���, 1162 REPEAT GEN_TAC THEN 1163 DISCH_THEN(MP_TAC o MATCH_MP REAL_DOWN o ONCE_REWRITE_RULE[GSYM REAL_SUB_LT]) 1164 THEN DISCH_THEN(X_CHOOSE_THEN ���d:real��� STRIP_ASSUME_TAC) THEN 1165 EXISTS_TAC ���x + d��� THEN ASM_REWRITE_TAC[REAL_LT_ADDR] THEN 1166 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 1167 ASM_REWRITE_TAC[GSYM REAL_LT_SUB_LADD]); 1168 1169val REAL_EQ_LMUL2 = store_thm("REAL_EQ_LMUL2", 1170 ���!x y z. ~(x = 0) ==> ((y = z) = (x * y = x * z))���, 1171 REPEAT GEN_TAC THEN DISCH_TAC THEN 1172 MP_TAC(SPECL [���x:real���, ���y:real���, ���z:real���] REAL_EQ_LMUL) THEN 1173 ASM_REWRITE_TAC[] THEN DISCH_THEN SUBST_ALL_TAC THEN REFL_TAC); 1174 1175val REAL_LE_MUL2 = store_thm("REAL_LE_MUL2", 1176 ���!x1 x2 y1 y2. 1177 (& 0) <= x1 /\ (& 0) <= y1 /\ x1 <= x2 /\ y1 <= y2 ==> 1178 (x1 * y1) <= (x2 * y2)���, 1179 REPEAT GEN_TAC THEN 1180 SUBST1_TAC(SPECL [���x1:real���, ���x2:real���] REAL_LE_LT) THEN 1181 ASM_CASES_TAC ���x1:real = x2��� THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL 1182 [UNDISCH_TAC ���0 <= x2��� THEN 1183 DISCH_THEN(DISJ_CASES_TAC o REWRITE_RULE[REAL_LE_LT]) THENL 1184 [FIRST_ASSUM(fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LE_LMUL th]), 1185 SUBST1_TAC(SYM(ASSUME ���0 = x2���)) THEN 1186 REWRITE_TAC[REAL_MUL_LZERO, REAL_LE_REFL]], ALL_TAC] THEN 1187 UNDISCH_TAC ���y1 <= y2��� THEN 1188 DISCH_THEN(DISJ_CASES_TAC o REWRITE_RULE[REAL_LE_LT]) THENL 1189 [MATCH_MP_TAC REAL_LT_IMP_LE THEN MATCH_MP_TAC REAL_LT_MUL2 THEN 1190 ASM_REWRITE_TAC[], 1191 ASM_REWRITE_TAC[]] THEN 1192 UNDISCH_TAC ���0 <= y1��� THEN ASM_REWRITE_TAC[] THEN 1193 DISCH_THEN(DISJ_CASES_TAC o REWRITE_RULE[REAL_LE_LT]) THENL 1194 [FIRST_ASSUM(fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LE_RMUL th]) THEN 1195 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], 1196 SUBST1_TAC(SYM(ASSUME ���0 = y2���)) THEN 1197 REWRITE_TAC[REAL_MUL_RZERO, REAL_LE_REFL]]); 1198 1199val REAL_LE_LDIV = store_thm("REAL_LE_LDIV", 1200 ���!x y z. 0 < x /\ y <= (z * x) ==> (y / x) <= z���, 1201 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1202 MATCH_MP_TAC(TAUT_CONV ���(a = b) ==> a ==> b���) THEN 1203 SUBGOAL_THEN ���y = (y / x) * x��� MP_TAC THENL 1204 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_RMUL THEN 1205 CONV_TAC(RAND_CONV SYM_CONV) THEN 1206 MATCH_MP_TAC REAL_LT_IMP_NE THEN POP_ASSUM ACCEPT_TAC, 1207 DISCH_THEN(fn t => GEN_REWR_TAC (funpow 2 LAND_CONV) [t]) 1208 THEN MATCH_MP_TAC REAL_LE_RMUL THEN POP_ASSUM ACCEPT_TAC]); 1209 1210val REAL_LE_RDIV = store_thm("REAL_LE_RDIV", 1211 ���!x y z. 0 < x /\ (y * x) <= z ==> y <= (z / x)���, 1212 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1213 MATCH_MP_TAC(TAUT_CONV ���(a = b) ==> a ==> b���) THEN 1214 SUBGOAL_THEN ���z = (z / x) * x��� MP_TAC THENL 1215 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_DIV_RMUL THEN 1216 CONV_TAC(RAND_CONV SYM_CONV) THEN 1217 MATCH_MP_TAC REAL_LT_IMP_NE THEN POP_ASSUM ACCEPT_TAC, 1218 DISCH_THEN(fn t => GEN_REWR_TAC (LAND_CONV o RAND_CONV) [t]) 1219 THEN MATCH_MP_TAC REAL_LE_RMUL THEN POP_ASSUM ACCEPT_TAC]); 1220 1221val REAL_LT_DIV = store_thm("REAL_LT_DIV", 1222 Term`!x y. 0 < x /\ 0 < y ==> 0 < x / y`, 1223 REWRITE_TAC [real_div] THEN REPEAT STRIP_TAC 1224 THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC [REAL_LT_INV_EQ]); 1225 1226val REAL_LE_DIV = store_thm("REAL_LE_DIV", 1227 Term`!x y. 0 <= x /\ 0 <= y ==> 0 <= x / y`, 1228 REWRITE_TAC [real_div] THEN REPEAT STRIP_TAC 1229 THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC [REAL_LE_INV_EQ]); 1230 1231val REAL_LT_1 = store_thm("REAL_LT_1", 1232 ���!x y. 0 <= x /\ x < y ==> (x / y) < &1���, 1233 REPEAT GEN_TAC THEN DISCH_TAC THEN 1234 SUBGOAL_THEN ���(x / y) < &1 = ((x / y) * y) < (&1 * y)��� SUBST1_TAC THENL 1235 [CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_LT_RMUL THEN 1236 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���x:real��� THEN 1237 ASM_REWRITE_TAC[], 1238 SUBGOAL_THEN ���(x / y) * y = x��� SUBST1_TAC THENL 1239 [MATCH_MP_TAC REAL_DIV_RMUL THEN CONV_TAC(RAND_CONV SYM_CONV) THEN 1240 MATCH_MP_TAC REAL_LT_IMP_NE THEN MATCH_MP_TAC REAL_LET_TRANS THEN 1241 EXISTS_TAC ���x:real��� THEN ASM_REWRITE_TAC[], 1242 ASM_REWRITE_TAC[REAL_MUL_LID]]]); 1243 1244val REAL_LE_LMUL_IMP = store_thm("REAL_LE_LMUL_IMP", 1245 ���!x y z. 0 <= x /\ y <= z ==> (x * y) <= (x * z)���, 1246 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 1247 DISCH_THEN(DISJ_CASES_TAC o REWRITE_RULE[REAL_LE_LT]) THENL 1248 [FIRST_ASSUM(fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LE_LMUL th]), 1249 FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[REAL_MUL_LZERO] THEN 1250 MATCH_ACCEPT_TAC REAL_LE_REFL]); 1251 1252val REAL_LE_RMUL_IMP = store_thm("REAL_LE_RMUL_IMP", 1253 ���!x y z. 0 <= x /\ y <= z ==> (y * x) <= (z * x)���, 1254 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_ACCEPT_TAC REAL_LE_LMUL_IMP); 1255 1256val REAL_EQ_IMP_LE = store_thm("REAL_EQ_IMP_LE", 1257 ���!x y. (x = y) ==> x <= y���, 1258 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN 1259 MATCH_ACCEPT_TAC REAL_LE_REFL); 1260 1261val REAL_INV_LT1 = store_thm("REAL_INV_LT1", 1262 ���!x. 0 < x /\ x < &1 ==> &1 < inv(x)���, 1263 GEN_TAC THEN STRIP_TAC THEN 1264 FIRST_ASSUM(ASSUME_TAC o MATCH_MP REAL_INV_POS) THEN 1265 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 1266 PURE_REWRITE_TAC[REAL_NOT_LT] THEN REWRITE_TAC[REAL_LE_LT] THEN 1267 DISCH_THEN(DISJ_CASES_THEN MP_TAC) THENL 1268 [DISCH_TAC THEN 1269 MP_TAC(SPECL [���inv(x)���, ���&1���, ���x:real���, ���&1���] REAL_LT_MUL2) THEN 1270 ASM_REWRITE_TAC[NOT_IMP] THEN REPEAT CONJ_TAC THENL 1271 [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], 1272 MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], 1273 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_IMP_NE) THEN 1274 REWRITE_TAC[REAL_MUL_LID] THEN MATCH_MP_TAC REAL_MUL_LINV THEN 1275 DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC ���0 < 0��� THEN 1276 REWRITE_TAC[REAL_LT_REFL]], 1277 DISCH_THEN(MP_TAC o AP_TERM ���inv���) THEN REWRITE_TAC[REAL_INV1] THEN 1278 SUBGOAL_THEN ���inv(inv x) = x��� SUBST1_TAC THENL 1279 [MATCH_MP_TAC REAL_INVINV THEN CONV_TAC(RAND_CONV SYM_CONV) THEN 1280 MATCH_MP_TAC REAL_LT_IMP_NE THEN FIRST_ASSUM ACCEPT_TAC, 1281 DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC ���&1 < &1��� THEN 1282 REWRITE_TAC[REAL_LT_REFL]]]); 1283 1284val REAL_POS_NZ = store_thm("REAL_POS_NZ", 1285 ���!x. 0 < x ==> ~(x = 0)���, 1286 GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP REAL_LT_IMP_NE) THEN 1287 CONV_TAC(RAND_CONV SYM_CONV) THEN POP_ASSUM ACCEPT_TAC); 1288 1289val REAL_EQ_RMUL_IMP = store_thm("REAL_EQ_RMUL_IMP", 1290 ���!x y z. ~(z = 0) /\ (x * z = y * z) ==> (x = y)���, 1291 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1292 ASM_REWRITE_TAC[REAL_EQ_RMUL]); 1293 1294val REAL_EQ_LMUL_IMP = store_thm("REAL_EQ_LMUL_IMP", 1295 ���!x y z. ~(x = 0) /\ (x * y = x * z) ==> (y = z)���, 1296 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_ACCEPT_TAC REAL_EQ_RMUL_IMP); 1297 1298val REAL_FACT_NZ = store_thm("REAL_FACT_NZ", 1299 ���!n. ~(&(FACT n) = 0)���, 1300 GEN_TAC THEN MATCH_MP_TAC REAL_POS_NZ THEN 1301 REWRITE_TAC[REAL_LT, FACT_LESS]); 1302 1303val REAL_DIFFSQ = store_thm("REAL_DIFFSQ", 1304 ���!x y. (x + y) * (x - y) = (x * x) - (y * y)���, 1305 REPEAT GEN_TAC THEN 1306 REWRITE_TAC[REAL_LDISTRIB, REAL_RDISTRIB, real_sub, GSYM REAL_ADD_ASSOC] THEN 1307 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1308 ���a + (b + (c + d)) = (b + c) + (a + d)���] THEN 1309 REWRITE_TAC[REAL_ADD_LID_UNIQ, GSYM REAL_NEG_RMUL] THEN 1310 REWRITE_TAC[REAL_LNEG_UNIQ] THEN AP_TERM_TAC THEN 1311 MATCH_ACCEPT_TAC REAL_MUL_SYM); 1312 1313val REAL_POSSQ = store_thm("REAL_POASQ", 1314 ���!x. 0 < (x * x) = ~(x = 0)���, 1315 GEN_TAC THEN REWRITE_TAC[GSYM REAL_NOT_LE] THEN AP_TERM_TAC THEN EQ_TAC THENL 1316 [DISCH_THEN(MP_TAC o C CONJ (SPEC ���x:real��� REAL_LE_SQUARE)) THEN 1317 REWRITE_TAC[REAL_LE_ANTISYM, REAL_ENTIRE], 1318 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[REAL_MUL_LZERO, REAL_LE_REFL]]); 1319 1320val REAL_SUMSQ = store_thm("REAL_SUMSQ", 1321 ���!x y. ((x * x) + (y * y) = 0) = (x = 0) /\ (y = 0)���, 1322 REPEAT GEN_TAC THEN EQ_TAC THENL 1323 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[DE_MORGAN_THM] THEN 1324 DISCH_THEN DISJ_CASES_TAC THEN MATCH_MP_TAC REAL_POS_NZ THENL 1325 [MATCH_MP_TAC REAL_LTE_ADD, MATCH_MP_TAC REAL_LET_ADD] THEN 1326 ASM_REWRITE_TAC[REAL_POSSQ, REAL_LE_SQUARE], 1327 DISCH_TAC THEN ASM_REWRITE_TAC[REAL_MUL_LZERO, REAL_ADD_LID]]); 1328 1329val REAL_EQ_NEG = store_thm("REAL_EQ_NEG", 1330 ���!x y. (~x = ~y) = (x = y)���, 1331 REPEAT GEN_TAC THEN 1332 REWRITE_TAC[GSYM REAL_LE_ANTISYM, REAL_LE_NEG] THEN 1333 MATCH_ACCEPT_TAC CONJ_SYM); 1334 1335val REAL_DIV_MUL2 = store_thm("REAL_DIV_MUL2", 1336 ���!x z. ~(x = 0) /\ ~(z = 0) ==> !y. y / z = (x * y) / (x * z)���, 1337 REPEAT GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN 1338 REWRITE_TAC[real_div] THEN IMP_SUBST_TAC REAL_INV_MUL THEN 1339 ASM_REWRITE_TAC[] THEN 1340 ONCE_REWRITE_TAC[AC(REAL_MUL_ASSOC,REAL_MUL_SYM) 1341 ���(a * b) * (c * d) = (c * a) * (b * d)���] THEN 1342 IMP_SUBST_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[] THEN 1343 REWRITE_TAC[REAL_MUL_LID]); 1344 1345val REAL_MIDDLE1 = store_thm("REAL_MIDDLE1", 1346 ���!a b. a <= b ==> a <= (a + b) / &2���, 1347 REPEAT GEN_TAC THEN DISCH_TAC THEN 1348 MATCH_MP_TAC REAL_LE_RDIV THEN 1349 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 1350 REWRITE_TAC[GSYM REAL_DOUBLE] THEN 1351 ASM_REWRITE_TAC[GSYM REAL_DOUBLE, REAL_LE_LADD] THEN 1352 REWRITE_TAC[num_CONV ���2:num���, REAL_LT, LESS_0]); 1353 1354val REAL_MIDDLE2 = store_thm("REAL_MIDDLE2", 1355 ���!a b. a <= b ==> ((a + b) / &2) <= b���, 1356 REPEAT GEN_TAC THEN DISCH_TAC THEN 1357 MATCH_MP_TAC REAL_LE_LDIV THEN 1358 ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN 1359 REWRITE_TAC[GSYM REAL_DOUBLE] THEN 1360 ASM_REWRITE_TAC[GSYM REAL_DOUBLE, REAL_LE_RADD] THEN 1361 REWRITE_TAC[num_CONV ���2:num���, REAL_LT, LESS_0]); 1362 1363(*---------------------------------------------------------------------------*) 1364(* Define usual norm (absolute distance) on the real line *) 1365(*---------------------------------------------------------------------------*) 1366 1367val abs = new_definition("abs", 1368 ���abs(x) = (if (0 <= x) then x else ~x)���); 1369 1370val ABS_ZERO = store_thm("ABS_ZERO", 1371 ���!x. (abs(x) = 0) = (x = 0)���, 1372 GEN_TAC THEN REWRITE_TAC[abs] THEN 1373 COND_CASES_TAC THEN REWRITE_TAC[REAL_NEG_EQ0]); 1374 1375val ABS_0 = store_thm("ABS_0", 1376 ���abs(0) = 0���, 1377 REWRITE_TAC[ABS_ZERO]); 1378 1379val ABS_1 = store_thm("ABS_1", 1380 ���abs(&1) = &1���, 1381 REWRITE_TAC[abs, REAL_LE, ZERO_LESS_EQ]); 1382 1383val ABS_NEG = store_thm("ABS_NEG", 1384 ���!x. abs~x = abs(x)���, 1385 GEN_TAC THEN REWRITE_TAC[abs, REAL_NEGNEG, REAL_NEG_GE0] THEN 1386 REPEAT COND_CASES_TAC THEN REWRITE_TAC[] THENL 1387 [MP_TAC(CONJ (ASSUME ���0 <= x���) (ASSUME ���x <= 0���)) THEN 1388 REWRITE_TAC[REAL_LE_ANTISYM] THEN 1389 DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[REAL_NEG_0], 1390 RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN 1391 W(MP_TAC o end_itlist CONJ o map ASSUME o fst) THEN 1392 REWRITE_TAC[REAL_LT_ANTISYM]]); 1393 1394val ABS_TRIANGLE = store_thm("ABS_TRIANGLE", 1395 ���!x y. abs(x + y) <= abs(x) + abs(y)���, 1396 REPEAT GEN_TAC THEN REWRITE_TAC[abs] THEN 1397 REPEAT COND_CASES_TAC THEN 1398 REWRITE_TAC[REAL_NEG_ADD, REAL_LE_REFL, REAL_LE_LADD, REAL_LE_RADD] THEN 1399 ASM_REWRITE_TAC[GSYM REAL_NEG_ADD, REAL_LE_NEGL, REAL_LE_NEGR] THEN 1400 RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN 1401 TRY(MATCH_MP_TAC REAL_LT_IMP_LE) THEN TRY(FIRST_ASSUM ACCEPT_TAC) THEN 1402 TRY(UNDISCH_TAC ���(x + y) < 0���) THEN SUBST1_TAC(SYM(SPEC ���0��� REAL_ADD_LID)) 1403 THEN REWRITE_TAC[REAL_NOT_LT] THEN 1404 MAP_FIRST MATCH_MP_TAC [REAL_LT_ADD2, REAL_LE_ADD2] THEN 1405 ASM_REWRITE_TAC[]); 1406 1407(* |- !x y. abs(x - y) <= abs(x) + abs(y) *) 1408val ABS_TRIANGLE_NEG = save_thm 1409 ("ABS_TRIANGLE_NEG", 1410 ((Q.GENL [`x`, `y`]) o (REWRITE_RULE [ABS_NEG, GSYM real_sub]) o 1411 (Q.SPECL [`x`, `-y`])) ABS_TRIANGLE); 1412 1413val ABS_TRIANGLE_SUB = store_thm ("ABS_TRIANGLE_SUB", 1414 ``!x y:real. abs(x) <= abs(y) + abs(x - y)``, 1415 MESON_TAC[ABS_TRIANGLE, REAL_SUB_ADD2]); 1416 1417val ABS_TRIANGLE_LT = store_thm ("ABS_TRIANGLE_LT", 1418 ``!x y. abs(x) + abs(y) < e ==> abs(x + y) < e:real``, 1419 MESON_TAC[REAL_LET_TRANS, ABS_TRIANGLE]); 1420 1421val ABS_POS = store_thm("ABS_POS", 1422 ���!x. 0 <= abs(x)���, 1423 GEN_TAC THEN ASM_CASES_TAC ���0 <= x��� THENL 1424 [ALL_TAC, 1425 MP_TAC(SPEC ���x:real��� REAL_LE_NEGTOTAL) THEN ASM_REWRITE_TAC[] THEN 1426 DISCH_TAC] THEN 1427 ASM_REWRITE_TAC[abs]); 1428 1429val ABS_MUL = store_thm("ABS_MUL", 1430 ���!x y. abs(x * y) = abs(x) * abs(y)���, 1431 REPEAT GEN_TAC THEN ASM_CASES_TAC ���0 <= x��� THENL 1432 [ALL_TAC, 1433 MP_TAC(SPEC ���x:real��� REAL_LE_NEGTOTAL) THEN ASM_REWRITE_TAC[] THEN 1434 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN 1435 GEN_REWR_TAC LAND_CONV [GSYM ABS_NEG] THEN 1436 GEN_REWR_TAC (RAND_CONV o LAND_CONV) [GSYM ABS_NEG] 1437 THEN REWRITE_TAC[REAL_NEG_LMUL]] THEN 1438 (ASM_CASES_TAC ���0 <= y��� THENL 1439 [ALL_TAC, 1440 MP_TAC(SPEC ���y:real��� REAL_LE_NEGTOTAL) THEN ASM_REWRITE_TAC[] THEN 1441 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN 1442 GEN_REWR_TAC LAND_CONV [GSYM ABS_NEG] THEN 1443 GEN_REWR_TAC (RAND_CONV o RAND_CONV) 1444 [GSYM ABS_NEG] THEN 1445 REWRITE_TAC[REAL_NEG_RMUL]]) THEN 1446 ASSUM_LIST(ASSUME_TAC o MATCH_MP REAL_LE_MUL o LIST_CONJ o rev) THEN 1447 ASM_REWRITE_TAC[abs]); 1448 1449val ABS_LT_MUL2 = store_thm("ABS_LT_MUL2", 1450 ���!w x y z. abs(w) < y /\ abs(x) < z ==> abs(w * x) < (y * z)���, 1451 REPEAT GEN_TAC THEN DISCH_TAC THEN 1452 REWRITE_TAC[ABS_MUL] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN 1453 ASM_REWRITE_TAC[ABS_POS]); 1454 1455val ABS_SUB = store_thm("ABS_SUB", 1456 ���!x y. abs(x - y) = abs(y - x)���, 1457 REPEAT GEN_TAC THEN 1458 GEN_REWR_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_NEG_SUB] THEN 1459 REWRITE_TAC[ABS_NEG]); 1460 1461val ABS_NZ = store_thm("ABS_NZ", 1462 ���!x. ~(x = 0) = 0 < abs(x)���, 1463 GEN_TAC THEN EQ_TAC THENL 1464 [ONCE_REWRITE_TAC[GSYM ABS_ZERO] THEN 1465 REWRITE_TAC[TAUT_CONV ���~a ==> b = b \/ a���] THEN 1466 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN 1467 REWRITE_TAC[GSYM REAL_LE_LT, ABS_POS], 1468 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[] THEN 1469 DISCH_THEN SUBST1_TAC THEN 1470 REWRITE_TAC[abs, REAL_LT_REFL, REAL_LE_REFL]]); 1471 1472val ABS_INV = store_thm("ABS_INV", 1473 ���!x. ~(x = 0) ==> (abs(inv x) = inv(abs(x)))���, 1474 GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LINV_UNIQ THEN 1475 REWRITE_TAC[GSYM ABS_MUL] THEN 1476 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP REAL_MUL_LINV th]) THEN 1477 REWRITE_TAC[abs, REAL_LE] THEN 1478 REWRITE_TAC[num_CONV ���1:num���, GSYM NOT_LESS, NOT_LESS_0]); 1479 1480val ABS_ABS = store_thm("ABS_ABS", 1481 ���!x. abs(abs(x)) = abs(x)���, 1482 GEN_TAC THEN 1483 GEN_REWR_TAC LAND_CONV [abs] THEN 1484 REWRITE_TAC[ABS_POS]); 1485 1486val ABS_LE = store_thm("ABS_LE", 1487 ���!x. x <= abs(x)���, 1488 GEN_TAC THEN REWRITE_TAC[abs] THEN 1489 COND_CASES_TAC THEN REWRITE_TAC[REAL_LE_REFL] THEN 1490 REWRITE_TAC[REAL_LE_NEGR] THEN 1491 MATCH_MP_TAC REAL_LT_IMP_LE THEN 1492 POP_ASSUM MP_TAC THEN REWRITE_TAC[REAL_NOT_LE]); 1493 1494val ABS_REFL = store_thm("ABS_REFL", 1495 ���!x. (abs(x) = x) = 0 <= x���, 1496 GEN_TAC THEN REWRITE_TAC[abs] THEN 1497 ASM_CASES_TAC ���0 <= x��� THEN ASM_REWRITE_TAC[] THEN 1498 CONV_TAC(RAND_CONV SYM_CONV) THEN 1499 ONCE_REWRITE_TAC[GSYM REAL_RNEG_UNIQ] THEN 1500 REWRITE_TAC[REAL_DOUBLE, REAL_ENTIRE, REAL_INJ] THEN 1501 CONV_TAC(ONCE_DEPTH_CONV num_EQ_CONV) THEN REWRITE_TAC[] THEN 1502 DISCH_THEN SUBST_ALL_TAC THEN POP_ASSUM MP_TAC THEN 1503 REWRITE_TAC[REAL_LE_REFL]); 1504 1505val ABS_N = store_thm("ABS_N", 1506 ���!n. abs(&n) = &n���, 1507 GEN_TAC THEN REWRITE_TAC[ABS_REFL, REAL_LE, ZERO_LESS_EQ]); 1508 1509val ABS_BETWEEN = store_thm("ABS_BETWEEN", 1510 ���!x y d. 0 < d /\ ((x - d) < y) /\ (y < (x + d)) = abs(y - x) < d���, 1511 REPEAT GEN_TAC THEN REWRITE_TAC[abs] THEN 1512 REWRITE_TAC[REAL_SUB_LE] THEN REWRITE_TAC[REAL_NEG_SUB] THEN 1513 COND_CASES_TAC THEN REWRITE_TAC[REAL_LT_SUB_RADD] THEN 1514 GEN_REWR_TAC (funpow 2 RAND_CONV) [REAL_ADD_SYM] THEN 1515 EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THENL 1516 [SUBGOAL_THEN ���x < (x + d)��� MP_TAC THENL 1517 [MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���y:real��� THEN 1518 ASM_REWRITE_TAC[], ALL_TAC] THEN 1519 REWRITE_TAC[REAL_LT_ADDR] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 1520 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���y:real��� THEN 1521 ASM_REWRITE_TAC[REAL_LT_ADDR], 1522 RULE_ASSUM_TAC(REWRITE_RULE[REAL_NOT_LE]) THEN 1523 SUBGOAL_THEN ���y < (y + d)��� MP_TAC THENL 1524 [MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC ���x:real��� THEN 1525 ASM_REWRITE_TAC[], ALL_TAC] THEN 1526 REWRITE_TAC[REAL_LT_ADDR] THEN DISCH_TAC THEN ASM_REWRITE_TAC[] THEN 1527 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC ���x:real��� THEN 1528 ASM_REWRITE_TAC[REAL_LT_ADDR]]); 1529 1530val ABS_BOUND = store_thm("ABS_BOUND", 1531 ���!x y d. abs(x - y) < d ==> y < (x + d)���, 1532 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[ABS_SUB] THEN 1533 ONCE_REWRITE_TAC[GSYM ABS_BETWEEN] THEN 1534 DISCH_TAC THEN ASM_REWRITE_TAC[]); 1535 1536val ABS_STILLNZ = store_thm("ABS_STILLNZ", 1537 ���!x y. abs(x - y) < abs(y) ==> ~(x = 0)���, 1538 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN 1539 REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN 1540 REWRITE_TAC[REAL_SUB_LZERO, ABS_NEG, REAL_LT_REFL]); 1541 1542val ABS_CASES = store_thm("ABS_CASES", 1543 ���!x. (x = 0) \/ 0 < abs(x)���, 1544 GEN_TAC THEN REWRITE_TAC[GSYM ABS_NZ] THEN 1545 BOOL_CASES_TAC ���x = 0��� THEN ASM_REWRITE_TAC[]); 1546 1547val ABS_BETWEEN1 = store_thm("ABS_BETWEEN1", 1548 ���!x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z���, 1549 REPEAT GEN_TAC THEN 1550 DISJ_CASES_TAC (SPECL [���x:real���, ���y:real���] REAL_LET_TOTAL) THENL 1551 [ASM_REWRITE_TAC[abs, REAL_SUB_LE] THEN 1552 REWRITE_TAC[real_sub, REAL_LT_RADD] THEN 1553 DISCH_THEN(ACCEPT_TAC o CONJUNCT2), 1554 DISCH_TAC THEN MATCH_MP_TAC REAL_LT_TRANS THEN 1555 EXISTS_TAC ���x:real��� THEN ASM_REWRITE_TAC[]]); 1556 1557val ABS_SIGN = store_thm("ABS_SIGN", 1558 ���!x y. abs(x - y) < y ==> 0 < x���, 1559 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP ABS_BOUND) THEN 1560 REWRITE_TAC[REAL_LT_ADDL]); 1561 1562val ABS_SIGN2 = store_thm("ABS_SIGN2", 1563 ���!x y. abs(x - y) < ~y ==> x < 0���, 1564 REPEAT GEN_TAC THEN DISCH_TAC THEN 1565 MP_TAC(SPECL [���~x���, ���~y���] ABS_SIGN) THEN 1566 REWRITE_TAC[REAL_SUB_NEG2] THEN 1567 ONCE_REWRITE_TAC[ABS_SUB] THEN 1568 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o MATCH_MP th)) THEN 1569 REWRITE_TAC[GSYM REAL_NEG_LT0, REAL_NEGNEG]); 1570 1571val ABS_DIV = store_thm("ABS_DIV", 1572 ���!y. ~(y = 0) ==> !x. abs(x / y) = abs(x) / abs(y)���, 1573 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN REWRITE_TAC[real_div] THEN 1574 REWRITE_TAC[ABS_MUL] THEN 1575 POP_ASSUM(fn th => REWRITE_TAC[MATCH_MP ABS_INV th])); 1576 1577val ABS_CIRCLE = store_thm("ABS_CIRCLE", 1578 ���!x y h. abs(h) < (abs(y) - abs(x)) ==> abs(x + h) < abs(y)���, 1579 REPEAT GEN_TAC THEN DISCH_TAC THEN 1580 MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC ���abs(x) + abs(h)��� THEN 1581 REWRITE_TAC[ABS_TRIANGLE] THEN 1582 POP_ASSUM(MP_TAC o CONJ (SPEC ���abs(x)��� REAL_LE_REFL)) THEN 1583 DISCH_THEN(MP_TAC o MATCH_MP REAL_LET_ADD2) THEN 1584 REWRITE_TAC[REAL_SUB_ADD2]); 1585 1586val REAL_SUB_ABS = store_thm("REAL_SUB_ABS", 1587 ���!x y. (abs(x) - abs(y)) <= abs(x - y)���, 1588 REPEAT GEN_TAC THEN 1589 MATCH_MP_TAC REAL_LE_TRANS THEN 1590 EXISTS_TAC ���(abs(x - y) + abs(y)) - abs(y)��� THEN CONJ_TAC THENL 1591 [ONCE_REWRITE_TAC[real_sub] THEN REWRITE_TAC[REAL_LE_RADD] THEN 1592 SUBST1_TAC(SYM(SPECL [���x:real���, ���y:real���] REAL_SUB_ADD)) THEN 1593 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [REAL_SUB_ADD] THEN 1594 MATCH_ACCEPT_TAC ABS_TRIANGLE, 1595 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 1596 REWRITE_TAC[REAL_ADD_SUB, REAL_LE_REFL]]); 1597 1598val ABS_SUB_ABS = store_thm("ABS_SUB_ABS", 1599 ���!x y. abs(abs(x) - abs(y)) <= abs(x - y)���, 1600 REPEAT GEN_TAC THEN 1601 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) [abs] THEN 1602 COND_CASES_TAC THEN REWRITE_TAC[REAL_SUB_ABS] THEN 1603 REWRITE_TAC[REAL_NEG_SUB] THEN 1604 ONCE_REWRITE_TAC[ABS_SUB] THEN 1605 REWRITE_TAC[REAL_SUB_ABS]); 1606 1607val ABS_BETWEEN2 = store_thm("ABS_BETWEEN2", 1608 ���!x0 x y0 y. 1609 x0 < y0 /\ 1610 abs(x - x0) < (y0 - x0) / &2 /\ 1611 abs(y - y0) < (y0 - x0) / &2 1612 ==> x < y���, 1613 REPEAT GEN_TAC THEN STRIP_TAC THEN 1614 SUBGOAL_THEN ���x < y0 /\ x0 < y��� STRIP_ASSUME_TAC THENL 1615 [CONJ_TAC THENL 1616 [MP_TAC(SPECL [���x0:real���, ���x:real���, 1617 ���y0 - x0���] ABS_BOUND) THEN 1618 REWRITE_TAC[REAL_SUB_ADD2] THEN DISCH_THEN MATCH_MP_TAC THEN 1619 ONCE_REWRITE_TAC[ABS_SUB] THEN 1620 MATCH_MP_TAC REAL_LT_TRANS THEN 1621 EXISTS_TAC ���(y0 - x0) / &2��� THEN 1622 ASM_REWRITE_TAC[REAL_LT_HALF2] THEN 1623 ASM_REWRITE_TAC[REAL_SUB_LT], 1624 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 1625 PURE_REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN 1626 MP_TAC(AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1627 ���(y0 + ~x0) + (x0 + ~y) = (~x0 + x0) + (y0 + ~y)���) THEN 1628 REWRITE_TAC[GSYM real_sub, REAL_ADD_LINV, REAL_ADD_LID] THEN 1629 DISCH_TAC THEN 1630 MP_TAC(SPECL [���y0 - x0���, 1631 ���x0 - y���] REAL_LE_ADDR) THEN 1632 ASM_REWRITE_TAC[REAL_SUB_LE] THEN DISCH_TAC THEN 1633 SUBGOAL_THEN ���~(y0 <= y)��� ASSUME_TAC THENL 1634 [REWRITE_TAC[REAL_NOT_LE] THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_LT] THEN 1635 MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC ���y0 - x0��� THEN 1636 ASM_REWRITE_TAC[] THEN ASM_REWRITE_TAC[REAL_SUB_LT], ALL_TAC] THEN 1637 UNDISCH_TAC ���abs(y - y0) < (y0 - x0) / &2��� THEN 1638 ASM_REWRITE_TAC[abs, REAL_SUB_LE] THEN 1639 REWRITE_TAC[REAL_NEG_SUB] THEN DISCH_TAC THEN 1640 SUBGOAL_THEN ���(y0 - x0) < (y0 - x0) / &2��� 1641 MP_TAC THENL 1642 [MATCH_MP_TAC REAL_LET_TRANS THEN 1643 EXISTS_TAC ���y0 - y��� THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 1644 REWRITE_TAC[REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 1645 REWRITE_TAC[REAL_LT_HALF2] THEN ASM_REWRITE_TAC[REAL_SUB_LT]], 1646 ALL_TAC] THEN 1647 GEN_REWR_TAC I [TAUT_CONV ���a = ~~a:bool���] THEN 1648 PURE_REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN 1649 SUBGOAL_THEN ���abs(x0 - y) < (y0 - x0) / &2��� ASSUME_TAC 1650 THENL 1651 [REWRITE_TAC[abs, REAL_SUB_LE] THEN ASM_REWRITE_TAC[GSYM REAL_NOT_LT] THEN 1652 REWRITE_TAC[REAL_NEG_SUB] THEN MATCH_MP_TAC REAL_LET_TRANS THEN 1653 EXISTS_TAC ���x - x0��� THEN 1654 REWRITE_TAC[real_sub, REAL_LE_RADD] THEN 1655 ASM_REWRITE_TAC[GSYM real_sub] THEN 1656 MATCH_MP_TAC REAL_LET_TRANS THEN 1657 EXISTS_TAC ���abs(x - x0)��� THEN 1658 ASM_REWRITE_TAC[ABS_LE], ALL_TAC] THEN 1659 SUBGOAL_THEN 1660 ���abs(y0 - x0) < ((y0 - x0) / &2) + ((y0 - x0) / &2)��� 1661 MP_TAC 1662 THENL 1663 [ALL_TAC, 1664 REWRITE_TAC[REAL_HALF_DOUBLE, REAL_NOT_LT, ABS_LE]] THEN 1665 MATCH_MP_TAC REAL_LET_TRANS THEN 1666 EXISTS_TAC ���abs(y0 - y) + abs(y - x0)��� THEN 1667 CONJ_TAC THENL 1668 [ALL_TAC, 1669 MATCH_MP_TAC REAL_LT_ADD2 THEN ONCE_REWRITE_TAC[ABS_SUB] THEN 1670 ASM_REWRITE_TAC[]] THEN 1671 SUBGOAL_THEN ���y0 - x0 = (y0 - y) + (y - x0)��� SUBST1_TAC THEN 1672 REWRITE_TAC[ABS_TRIANGLE] THEN 1673 REWRITE_TAC[real_sub] THEN 1674 ONCE_REWRITE_TAC[AC(REAL_ADD_ASSOC,REAL_ADD_SYM) 1675 ���(a + b) + (c + d) = (b + c) + (a + d)���] THEN 1676 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_LID]); 1677 1678val ABS_BOUNDS = store_thm("ABS_BOUNDS", 1679 ���!x k. abs(x) <= k = ~k <= x /\ x <= k���, 1680 REPEAT GEN_TAC THEN 1681 GEN_REWR_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_LE_NEG] THEN 1682 REWRITE_TAC[REAL_NEGNEG] THEN REWRITE_TAC[abs] THEN 1683 COND_CASES_TAC THENL 1684 [REWRITE_TAC[TAUT_CONV ���(a = b /\ a) = a ==> b���] THEN 1685 DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1686 EXISTS_TAC ���x:real��� THEN ASM_REWRITE_TAC[REAL_LE_NEGL], 1687 REWRITE_TAC[TAUT_CONV ���(a = a /\ b) = a ==> b���] THEN 1688 DISCH_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN 1689 EXISTS_TAC ���~x��� THEN ASM_REWRITE_TAC[] THEN 1690 REWRITE_TAC[REAL_LE_NEGR] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN 1691 ASM_REWRITE_TAC[GSYM REAL_NOT_LE]]); 1692 1693(*---------------------------------------------------------------------------*) 1694(* Define integer powers *) 1695(*---------------------------------------------------------------------------*) 1696 1697val pow = new_recursive_definition 1698 {name = "pow", 1699 def = ���($pow x 0 = &1) /\ ($pow x (SUC n) = x * ($pow x n))���, 1700 rec_axiom = num_Axiom} 1701 1702val _ = set_fixity "pow" (Infixr 700); 1703 1704val POW_0 = store_thm("POW_0", 1705 ���!n. 0 pow (SUC n) = 0���, 1706 INDUCT_TAC THEN REWRITE_TAC[pow, REAL_MUL_LZERO]); 1707 1708val POW_NZ = store_thm("POW_NZ", 1709 ���!c n. ~(c = 0) ==> ~(c pow n = 0)���, 1710 REPEAT GEN_TAC THEN DISCH_TAC THEN SPEC_TAC(���n:num���,���n:num���) THEN 1711 INDUCT_TAC THEN ASM_REWRITE_TAC[pow, REAL_10, REAL_ENTIRE]); 1712 1713val POW_INV = store_thm("POW_INV", 1714 ���!c. ~(c = 0) ==> !n. (inv(c pow n) = (inv c) pow n)���, 1715 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN REWRITE_TAC[pow, REAL_INV1] THEN 1716 MP_TAC(SPECL [���c:real���, ���c pow n���] REAL_INV_MUL) THEN 1717 ASM_REWRITE_TAC[] THEN SUBGOAL_THEN ���~(c pow n = 0)��� ASSUME_TAC THENL 1718 [MATCH_MP_TAC POW_NZ THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 1719 ASM_REWRITE_TAC[]); 1720 1721val POW_ABS = store_thm("POW_ABS", 1722 ���!c n. abs(c) pow n = abs(c pow n)���, 1723 GEN_TAC THEN INDUCT_TAC THEN 1724 ASM_REWRITE_TAC[pow, ABS_1, ABS_MUL]); 1725 1726val POW_PLUS1 = store_thm("POW_PLUS1", 1727 ���!e. 0 < e ==> !n. (&1 + (&n * e)) <= (&1 + e) pow n���, 1728 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN 1729 REWRITE_TAC[pow, REAL_MUL_LZERO, REAL_ADD_RID, REAL_LE_REFL] THEN 1730 MATCH_MP_TAC REAL_LE_TRANS THEN 1731 EXISTS_TAC ���(&1 + e) * (&1 + (&n * e))��� THEN CONJ_TAC THENL 1732 [REWRITE_TAC[REAL_LDISTRIB, REAL_RDISTRIB, REAL, REAL_MUL_LID] THEN 1733 REWRITE_TAC[REAL_MUL_RID, REAL_ADD_ASSOC, REAL_LE_ADDR] THEN 1734 MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THENL 1735 [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 1736 MATCH_MP_TAC REAL_LE_MUL THEN CONJ_TAC THENL 1737 [ALL_TAC, MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]] THEN 1738 REWRITE_TAC[REAL_LE, ZERO_LESS_EQ], 1739 SUBGOAL_THEN ���0 < (&1 + e)��� 1740 (fn th => ASM_REWRITE_TAC[MATCH_MP REAL_LE_LMUL th]) THEN 1741 GEN_REWR_TAC LAND_CONV [GSYM REAL_ADD_LID] THEN 1742 MATCH_MP_TAC REAL_LT_ADD2 THEN ASM_REWRITE_TAC[] THEN 1743 REWRITE_TAC[REAL_LT] THEN REWRITE_TAC[num_CONV ���1:num���, LESS_0]]); 1744 1745val POW_ADD = store_thm("POW_ADD", 1746 ���!c m n. c pow (m + n) = (c pow m) * (c pow n)���, 1747 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 1748 ASM_REWRITE_TAC[pow, ADD_CLAUSES, REAL_MUL_RID] THEN 1749 CONV_TAC(AC_CONV(REAL_MUL_ASSOC,REAL_MUL_SYM))); 1750 1751val POW_1 = store_thm("POW_1", 1752 ���!x. x pow 1 = x���, 1753 GEN_TAC THEN REWRITE_TAC[num_CONV ���1:num���] THEN 1754 REWRITE_TAC[pow, REAL_MUL_RID]); 1755 1756val POW_2 = store_thm("POW_2", 1757 ���!x. x pow 2 = x * x���, 1758 GEN_TAC THEN REWRITE_TAC[num_CONV ���2:num���] THEN 1759 REWRITE_TAC[pow, POW_1]); 1760 1761val POW_ONE = store_thm("POW_ONE", 1762 Term`!n. &1 pow n = &1`, 1763 INDUCT_TAC THEN ASM_REWRITE_TAC[pow, REAL_MUL_LID]); 1764 1765val POW_POS = store_thm("POW_POS", 1766 ���!x. 0 <= x ==> !n. 0 <= (x pow n)���, 1767 GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN 1768 REWRITE_TAC[pow, REAL_LE_01] THEN 1769 MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]); 1770 1771val POW_LE = store_thm("POW_LE", 1772 ���!n x y. 0 <= x /\ x <= y ==> (x pow n) <= (y pow n)���, 1773 INDUCT_TAC THEN REWRITE_TAC[pow, REAL_LE_REFL] THEN 1774 REPEAT GEN_TAC THEN STRIP_TAC THEN 1775 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL 1776 [MATCH_MP_TAC POW_POS THEN FIRST_ASSUM ACCEPT_TAC, 1777 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]); 1778 1779val POW_M1 = store_thm("POW_M1", 1780 ���!n. abs(~1 pow n) = 1���, 1781 INDUCT_TAC THEN REWRITE_TAC[pow, ABS_NEG, ABS_1] THEN 1782 ASM_REWRITE_TAC[ABS_MUL, ABS_NEG, ABS_1, REAL_MUL_LID]); 1783 1784val POW_MUL = store_thm("POW_MUL", 1785 ���!n x y. (x * y) pow n = (x pow n) * (y pow n)���, 1786 INDUCT_TAC THEN REWRITE_TAC[pow, REAL_MUL_LID] THEN 1787 REPEAT GEN_TAC THEN ASM_REWRITE_TAC[] THEN 1788 CONV_TAC(AC_CONV(REAL_MUL_ASSOC,REAL_MUL_SYM))); 1789 1790val REAL_LE_POW2 = store_thm("REAL_LE_POW2", 1791 ���!x. 0 <= x pow 2���, 1792 GEN_TAC THEN REWRITE_TAC[POW_2, REAL_LE_SQUARE]); 1793 1794val ABS_POW2 = store_thm("ABS_POW2", 1795 ���!x. abs(x pow 2) = x pow 2���, 1796 GEN_TAC THEN REWRITE_TAC[ABS_REFL, REAL_LE_POW2]); 1797 1798val REAL_POW2_ABS = store_thm("REAL_POW2_ABS", 1799 ���!x. abs(x) pow 2 = x pow 2���, 1800 GEN_TAC THEN REWRITE_TAC[POW_2, POW_MUL] THEN 1801 REWRITE_TAC[GSYM ABS_MUL] THEN 1802 REWRITE_TAC[GSYM POW_2, ABS_POW2]); 1803 1804val REAL_LE1_POW2 = store_thm("REAL_LE1_POW2", 1805 ���!x. &1 <= x ==> &1 <= (x pow 2)���, 1806 GEN_TAC THEN REWRITE_TAC[POW_2] THEN DISCH_TAC THEN 1807 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN 1808 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_LE_01]); 1809 1810val REAL_LT1_POW2 = store_thm("REAL_LT1_POW2", 1811 ���!x. &1 < x ==> &1 < (x pow 2)���, 1812 GEN_TAC THEN REWRITE_TAC[POW_2] THEN DISCH_TAC THEN 1813 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN 1814 MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[REAL_LE_01]); 1815 1816val POW_POS_LT = store_thm("POW_POS_LT", 1817 ���!x n. 0 < x ==> 0 < (x pow (SUC n))���, 1818 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN 1819 DISCH_TAC THEN CONJ_TAC THENL 1820 [MATCH_MP_TAC POW_POS THEN ASM_REWRITE_TAC[], 1821 CONV_TAC(RAND_CONV SYM_CONV) THEN 1822 MATCH_MP_TAC POW_NZ THEN 1823 CONV_TAC(RAND_CONV SYM_CONV) THEN ASM_REWRITE_TAC[]]); 1824 1825val POW_2_LE1 = store_thm("POW_2_LE1", 1826 ���!n. &1 <= &2 pow n���, 1827 INDUCT_TAC THEN REWRITE_TAC[pow, REAL_LE_REFL] THEN 1828 GEN_REWR_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN 1829 MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[REAL_LE] THEN 1830 REWRITE_TAC[ZERO_LESS_EQ, num_CONV ���2:num���, LESS_EQ_SUC_REFL]); 1831 1832val POW_2_LT = store_thm("POW_2_LT", 1833 ���!n. &n < &2 pow n���, 1834 INDUCT_TAC THEN REWRITE_TAC[pow, REAL_LT_01] THEN 1835 REWRITE_TAC[ADD1, GSYM REAL_ADD, GSYM REAL_DOUBLE] THEN 1836 MATCH_MP_TAC REAL_LTE_ADD2 THEN ASM_REWRITE_TAC[POW_2_LE1]); 1837 1838val POW_MINUS1 = store_thm("POW_MINUS1", 1839 ���!n. ~1 pow (2 * n) = 1���, 1840 INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES, pow] THEN 1841 REWRITE_TAC(map num_CONV [Term`2:num`,Term`1:num`] @ [ADD_CLAUSES]) THEN 1842 REWRITE_TAC[pow] THEN 1843 REWRITE_TAC[SYM(num_CONV ���2:num���), SYM(num_CONV ���1:num���)] THEN 1844 ASM_REWRITE_TAC[] THEN 1845 REWRITE_TAC[GSYM REAL_NEG_LMUL, GSYM REAL_NEG_RMUL] THEN 1846 REWRITE_TAC[REAL_MUL_LID, REAL_NEGNEG]); 1847 1848val POW_LT = store_thm("POW_LT", 1849 ���!n x y. 0 <= x /\ x < y ==> (x pow (SUC n)) < (y pow (SUC n))���, 1850 REPEAT STRIP_TAC THEN SPEC_TAC(���n:num���,���n:num���) 1851 THEN INDUCT_TAC THENL 1852 [ASM_REWRITE_TAC[pow, REAL_MUL_RID], 1853 ONCE_REWRITE_TAC[pow] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN 1854 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC POW_POS THEN ASM_REWRITE_TAC[]]); 1855 1856val REAL_POW_LT = store_thm("REAL_POW_LT", 1857 Term`!x n. 0 < x ==> 0 < (x pow n)`, 1858 REPEAT STRIP_TAC THEN SPEC_TAC(Term`n:num`,Term`n:num`) THEN 1859 INDUCT_TAC THEN REWRITE_TAC[pow, REAL_LT_01] THEN 1860 MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);; 1861 1862val POW_EQ = store_thm("POW_EQ", 1863 ���!n x y. 0 <= x /\ 0 <= y /\ (x pow (SUC n) = y pow (SUC n)) 1864 ==> (x = y)���, 1865 REPEAT STRIP_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 1866 (SPECL [���x:real���, ���y:real���] REAL_LT_TOTAL) THEN 1867 ASM_REWRITE_TAC[] THEN 1868 UNDISCH_TAC ���x pow (SUC n) = y pow (SUC n)��� THEN 1869 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THENL 1870 [ALL_TAC, CONV_TAC(RAND_CONV SYM_CONV)] THEN 1871 MATCH_MP_TAC REAL_LT_IMP_NE THEN 1872 MATCH_MP_TAC POW_LT THEN ASM_REWRITE_TAC[]); 1873 1874val POW_ZERO = store_thm("POW_ZERO", 1875 ���!n x. (x pow n = 0) ==> (x = 0)���, 1876 INDUCT_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[pow] THEN 1877 REWRITE_TAC[REAL_10, REAL_ENTIRE] THEN 1878 DISCH_THEN(DISJ_CASES_THEN2 ACCEPT_TAC ASSUME_TAC) THEN 1879 FIRST_ASSUM MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC); 1880 1881val POW_ZERO_EQ = store_thm("POW_ZERO_EQ", 1882 ���!n x. (x pow (SUC n) = 0) = (x = 0)���, 1883 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[POW_ZERO] THEN 1884 DISCH_THEN SUBST1_TAC THEN REWRITE_TAC[POW_0]); 1885 1886val REAL_POW_LT2 = store_thm("REAL_POW_LT2", 1887 Term `!n x y. ~(n = 0) /\ 0 <= x /\ x < y ==> x pow n < y pow n`, 1888 INDUCT_TAC THEN REWRITE_TAC[NOT_SUC, pow] THEN REPEAT STRIP_TAC THEN 1889 ASM_CASES_TAC (Term `n = 0:num`) THEN ASM_REWRITE_TAC[pow, REAL_MUL_RID] THEN 1890 MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL 1891 [MATCH_MP_TAC POW_POS THEN ASM_REWRITE_TAC[], 1892 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);; 1893 1894val LT_EXISTS = prove 1895 (Term`!m n. m < n = ?d. n = m + SUC d`, 1896 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL 1897 [IMP_RES_TAC LESS_ADD_1 THEN ASM_REWRITE_TAC[] 1898 THEN EXISTS_TAC (Term`p:num`) THEN REWRITE_TAC [ADD1], 1899 ASM_REWRITE_TAC[LESS_ADD_SUC]]); 1900 1901val REAL_POW_MONO_LT = store_thm("REAL_POW_MONO_LT", 1902 Term`!m n x. &1 < x /\ m < n ==> x pow m < x pow n`, 1903 REPEAT GEN_TAC THEN REWRITE_TAC[LT_EXISTS] THEN 1904 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN 1905 DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN 1906 REWRITE_TAC[POW_ADD] THEN 1907 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN 1908 MATCH_MP_TAC REAL_LT_LMUL_IMP THEN CONJ_TAC THENL 1909 [SPEC_TAC(Term`d:num`,Term`d:num`) THEN 1910 INDUCT_TAC THEN ONCE_REWRITE_TAC[pow] THENL 1911 [ASM_REWRITE_TAC[pow, REAL_MUL_RID], ALL_TAC] THEN 1912 GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN 1913 MATCH_MP_TAC REAL_LT_MUL2 THEN 1914 ASM_REWRITE_TAC[REAL_LE, ZERO_LESS_EQ], 1915 MATCH_MP_TAC REAL_POW_LT THEN 1916 MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC (Term`&1`) THEN 1917 ASM_REWRITE_TAC[REAL_LT,prim_recTheory.LESS_0, ONE]]); 1918 1919val REAL_POW_POW = store_thm("REAL_POW_POW", 1920 Term `!x m n. (x pow m) pow n = x pow (m * n)`, 1921 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 1922 ASM_REWRITE_TAC[pow, MULT_CLAUSES, POW_ADD]);; 1923 1924 1925(*---------------------------------------------------------------------------*) 1926(* Derive the supremum property for an arbitrary bounded nonempty set *) 1927(*---------------------------------------------------------------------------*) 1928 1929val REAL_SUP_SOMEPOS = store_thm("REAL_SUP_SOMEPOS", 1930 ���!P. (?x. P x /\ 0 < x) /\ (?z. !x. P x ==> x < z) ==> 1931 (?s. !y. (?x. P x /\ y < x) = y < s)���, 1932 let val lemma = TAUT_CONV ���a /\ b ==> b��� in 1933 GEN_TAC THEN DISCH_TAC THEN 1934 MP_TAC (SPEC ���\x. P x /\ 0 < x��� REAL_SUP_ALLPOS) THEN 1935 BETA_TAC THEN ASM_REWRITE_TAC[lemma] THEN 1936 SUBGOAL_THEN 1937 ���?z. !x. P x /\ 0 < x ==> x < z��� (SUBST1_TAC o EQT_INTRO) 1938 THENL 1939 [POP_ASSUM(X_CHOOSE_TAC ���z:real��� o CONJUNCT2) THEN 1940 EXISTS_TAC ���z:real��� THEN 1941 GEN_TAC THEN 1942 DISCH_THEN(curry op THEN (FIRST_ASSUM MATCH_MP_TAC) o ASSUME_TAC) THEN 1943 ASM_REWRITE_TAC[], ALL_TAC] THEN 1944 REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN ���s:real��� MP_TAC) THEN 1945 DISCH_THEN(curry op THEN (EXISTS_TAC ���s:real��� THEN GEN_TAC) o 1946 (SUBST1_TAC o SYM o SPEC ���y:real���)) THEN EQ_TAC THENL 1947 [REPEAT_TCL DISJ_CASES_THEN MP_TAC (SPECL [���y:real���, ���0���] 1948 REAL_LT_TOTAL) 1949 THENL 1950 [DISCH_THEN SUBST1_TAC THEN DISCH_THEN(X_CHOOSE_TAC ���x:real���) THEN 1951 EXISTS_TAC ���x:real��� THEN ASM_REWRITE_TAC[], 1952 POP_ASSUM(X_CHOOSE_TAC ���x:real��� o CONJUNCT1) THEN 1953 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o CONJ th o CONJUNCT2)) THEN 1954 DISCH_THEN(ASSUME_TAC o MATCH_MP REAL_LT_TRANS) THEN 1955 DISCH_THEN(K ALL_TAC) THEN 1956 EXISTS_TAC ���x:real��� THEN ASM_REWRITE_TAC[], 1957 POP_ASSUM(K ALL_TAC) THEN DISCH_TAC THEN 1958 DISCH_THEN(X_CHOOSE_TAC ���x:real���) THEN 1959 EXISTS_TAC ���x:real��� THEN 1960 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_TRANS THEN 1961 EXISTS_TAC ���y:real��� THEN ASM_REWRITE_TAC[]], 1962 DISCH_THEN(X_CHOOSE_TAC ���x:real���) THEN 1963 EXISTS_TAC ���x:real��� THEN 1964 ASM_REWRITE_TAC[]] end); 1965 1966val SUP_LEMMA1 = store_thm("SUP_LEMMA1", 1967 ���!P s d. (!y. (?x. (\x. P(x + d)) x /\ y < x) = y < s) 1968 ==> (!y. (?x. P x /\ y < x) = y < (s + d))���, 1969 REPEAT GEN_TAC THEN BETA_TAC THEN DISCH_TAC THEN GEN_TAC THEN 1970 POP_ASSUM(MP_TAC o SPEC ���y + ~d���) THEN 1971 REWRITE_TAC[REAL_LT_ADDNEG2] THEN DISCH_THEN(SUBST1_TAC o SYM) THEN 1972 EQ_TAC THEN DISCH_THEN(X_CHOOSE_TAC ���x:real���) THENL 1973 [EXISTS_TAC ���x + ~d��� THEN 1974 ASM_REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_RID], 1975 EXISTS_TAC ���x + d��� THEN POP_ASSUM ACCEPT_TAC]); 1976 1977val SUP_LEMMA2 = store_thm("SUP_LEMMA2", 1978 ���!P. (?x. P x) ==> ?d. ?x. (\x. P(x + d)) x /\ 0 < x���, 1979 GEN_TAC THEN DISCH_THEN(X_CHOOSE_TAC ���x:real���) THEN BETA_TAC THEN 1980 REPEAT_TCL DISJ_CASES_THEN MP_TAC (SPECL [���x:real���, ���0���] 1981 REAL_LT_TOTAL) 1982 THENL 1983 [DISCH_THEN SUBST_ALL_TAC THEN 1984 MAP_EVERY EXISTS_TAC [���~1���, ���1���] THEN 1985 ASM_REWRITE_TAC[REAL_ADD_RINV, REAL_LT_01], 1986 DISCH_TAC THEN 1987 MAP_EVERY EXISTS_TAC [���x + x���, ���~x���] THEN 1988 ASM_REWRITE_TAC[REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_LID, REAL_NEG_GT0], 1989 DISCH_TAC THEN MAP_EVERY EXISTS_TAC [���0���, ���x:real���] THEN 1990 ASM_REWRITE_TAC[REAL_ADD_RID]]); 1991 1992val SUP_LEMMA3 = store_thm("SUP_LEMMA3", 1993 ���!d. (?z. !x. P x ==> x < z) ==> 1994 (?z. !x. (\x. P(x + d)) x ==> x < z)���, 1995 GEN_TAC THEN DISCH_THEN(X_CHOOSE_TAC ���z:real���) THEN 1996 EXISTS_TAC ���z + ~d��� THEN GEN_TAC THEN BETA_TAC THEN 1997 DISCH_THEN(fn th => FIRST_ASSUM(ASSUME_TAC o C MATCH_MP th)) THEN 1998 ASM_REWRITE_TAC[REAL_LT_ADDNEG]); 1999 2000val REAL_SUP_EXISTS = store_thm("REAL_SUP_EXISTS", 2001 ���!P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> 2002 (?s. !y. (?x. P x /\ y < x) = y < s)���, 2003 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 2004 (X_CHOOSE_TAC ���d:real��� o MATCH_MP SUP_LEMMA2) MP_TAC) THEN 2005 DISCH_THEN(MP_TAC o MATCH_MP (SPEC ���d:real��� SUP_LEMMA3)) THEN 2006 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o MATCH_MP REAL_SUP_SOMEPOS o CONJ th)) 2007 THEN 2008 DISCH_THEN(X_CHOOSE_TAC ���s:real���) THEN 2009 EXISTS_TAC ���s + d��� THEN 2010 MATCH_MP_TAC SUP_LEMMA1 THEN POP_ASSUM ACCEPT_TAC); 2011 2012val sup = new_definition("sup", 2013 ���sup P = @s. !y. (?x. P x /\ y < x) = y < s���); 2014 2015val REAL_SUP = store_thm("REAL_SUP", 2016 ���!P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> 2017 (!y. (?x. P x /\ y < x) = y < sup P)���, 2018 GEN_TAC THEN DISCH_THEN(MP_TAC o SELECT_RULE o MATCH_MP REAL_SUP_EXISTS) 2019 THEN REWRITE_TAC[GSYM sup]); 2020 2021val REAL_SUP_UBOUND = store_thm("REAL_SUP_UBOUND", 2022 ���!P. (?x. P x) /\ (?z. !x. P x ==> x < z) ==> 2023 (!y. P y ==> y <= sup P)���, 2024 GEN_TAC THEN DISCH_THEN(MP_TAC o SPEC ���sup P��� o MATCH_MP REAL_SUP) THEN 2025 REWRITE_TAC[REAL_LT_REFL] THEN 2026 DISCH_THEN(ASSUME_TAC o CONV_RULE NOT_EXISTS_CONV) THEN 2027 X_GEN_TAC ���x:real��� THEN RULE_ASSUM_TAC(SPEC ���x:real���) THEN 2028 DISCH_THEN (SUBST_ALL_TAC o EQT_INTRO) THEN POP_ASSUM MP_TAC THEN 2029 REWRITE_TAC[REAL_NOT_LT]); 2030 2031val SETOK_LE_LT = store_thm("SETOK_LE_LT", 2032 ���!P. (?x. P x) /\ (?z. !x. P x ==> x <= z) = 2033 (?x. P x) /\ (?z. !x. P x ==> x < z)���, 2034 GEN_TAC THEN AP_TERM_TAC THEN EQ_TAC THEN 2035 DISCH_THEN(X_CHOOSE_TAC ���z:real���) 2036 THENL (map EXISTS_TAC [���z + &1���, ���z:real���]) THEN 2037 GEN_TAC THEN DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN 2038 REWRITE_TAC[REAL_LT_ADD1, REAL_LT_IMP_LE]); 2039 2040val REAL_SUP_LE = store_thm("REAL_SUP_LE", 2041 ���!P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> 2042 (!y. (?x. P x /\ y < x) = y < sup P)���, 2043 GEN_TAC THEN REWRITE_TAC[SETOK_LE_LT, REAL_SUP]); 2044 2045val REAL_SUP_UBOUND_LE = store_thm("REAL_SUP_UBOUND_LE", 2046 ���!P. (?x. P x) /\ (?z. !x. P x ==> x <= z) ==> 2047 (!y. P y ==> y <= sup P)���, 2048 GEN_TAC THEN REWRITE_TAC[SETOK_LE_LT, REAL_SUP_UBOUND]); 2049 2050(*---------------------------------------------------------------------------*) 2051(* Prove the Archimedean property *) 2052(*---------------------------------------------------------------------------*) 2053 2054val REAL_ARCH = store_thm("REAL_ARCH", 2055 ���!x. 0 < x ==> !y. ?n. y < &n * x���, 2056 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN 2057 ONCE_REWRITE_TAC[TAUT_CONV ���a = ~(~a):bool���] THEN 2058 CONV_TAC(ONCE_DEPTH_CONV NOT_EXISTS_CONV) THEN 2059 REWRITE_TAC[REAL_NOT_LT] THEN DISCH_TAC THEN 2060 MP_TAC(SPEC ���\z. ?n. z = &n * x��� REAL_SUP_LE) THEN 2061 BETA_TAC THEN 2062 W(C SUBGOAL_THEN(fn th => REWRITE_TAC[th]) o funpow 2 (fst o dest_imp) o snd) 2063 THENL [CONJ_TAC THENL 2064 [MAP_EVERY EXISTS_TAC [���&n * x���, ���n:num���] THEN REFL_TAC, 2065 EXISTS_TAC ���y:real��� THEN GEN_TAC THEN 2066 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN ASM_REWRITE_TAC[]], ALL_TAC] THEN 2067 DISCH_TAC THEN 2068 FIRST_ASSUM(MP_TAC o SPEC ���sup(\z. ?n. z = &n * x) - x���) 2069 THEN 2070 REWRITE_TAC[REAL_LT_SUB_RADD, REAL_LT_ADDR] THEN ASM_REWRITE_TAC[] THEN 2071 DISCH_THEN(X_CHOOSE_THEN ���z:real��� MP_TAC) THEN 2072 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC ���n:num���) MP_TAC) THEN 2073 ASM_REWRITE_TAC[] THEN 2074 GEN_REWR_TAC (funpow 3 RAND_CONV) [GSYM REAL_MUL_LID] THEN 2075 REWRITE_TAC[GSYM REAL_RDISTRIB] THEN DISCH_TAC THEN 2076 FIRST_ASSUM(MP_TAC o SPEC ���sup(\z. ?n. z = &n * x)���) THEN 2077 REWRITE_TAC[REAL_LT_REFL] THEN EXISTS_TAC ���(&n + &1) * x��� 2078 THEN 2079 ASM_REWRITE_TAC[] THEN EXISTS_TAC ���n + 1:num��� THEN 2080 REWRITE_TAC[REAL_ADD]); 2081 2082val REAL_ARCH_LEAST = store_thm("REAL_ARCH_LEAST", 2083 ���!y. 0 < y 2084 ==> !x. 0 <= x 2085 ==> ?n. (&n * y) <= x 2086 /\ x < (&(SUC n) * y)���, 2087 GEN_TAC THEN DISCH_THEN(ASSUME_TAC o MATCH_MP REAL_ARCH) THEN 2088 GEN_TAC THEN POP_ASSUM(ASSUME_TAC o SPEC ���x:real���) THEN 2089 POP_ASSUM(X_CHOOSE_THEN ���n:num��� MP_TAC o CONV_RULE EXISTS_LEAST_CONV) 2090 THEN 2091 REWRITE_TAC[REAL_NOT_LT] THEN 2092 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (ASSUME_TAC o SPEC ���PRE n���)) THEN 2093 DISCH_TAC THEN EXISTS_TAC ���PRE n��� THEN 2094 SUBGOAL_THEN ���SUC(PRE n) = n��� ASSUME_TAC THENL 2095 [DISJ_CASES_THEN2 SUBST_ALL_TAC (CHOOSE_THEN SUBST_ALL_TAC) 2096 (SPEC ���n:num��� num_CASES) THENL 2097 [UNDISCH_TAC ���x < 0 * y��� THEN 2098 ASM_REWRITE_TAC[REAL_MUL_LZERO, GSYM REAL_NOT_LE], 2099 REWRITE_TAC[PRE]], 2100 ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2101 FIRST_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[PRE, LESS_SUC_REFL]]); 2102 2103(*---------------------------------------------------------------------------*) 2104(* Now define finite sums; NB: sum(m,n) f = f(m) + f(m+1) + ... + f(m+n-1) *) 2105(*---------------------------------------------------------------------------*) 2106 2107val sum = Lib.with_flag (boolLib.def_suffix, "") Define` 2108 (sum (n,0) f = 0) /\ 2109 (sum (n,SUC m) f = sum (n,m) f + f (n + m): real)` 2110 2111(*---------------------------------------------------------------------------*) 2112(* Useful manipulative theorems for sums *) 2113(*---------------------------------------------------------------------------*) 2114 2115val SUM_TWO = store_thm("SUM_TWO", 2116 ���!f n p. sum(0,n) f + sum(n,p) f = sum(0,n + p) f���, 2117 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 2118 REWRITE_TAC[sum, REAL_ADD_RID, ADD_CLAUSES] THEN 2119 ASM_REWRITE_TAC[REAL_ADD_ASSOC]); 2120 2121val SUM_DIFF = store_thm("SUM_DIFF", 2122 ���!f m n. sum(m,n) f = sum(0,m + n) f - sum(0,m) f���, 2123 REPEAT GEN_TAC THEN REWRITE_TAC[REAL_EQ_SUB_LADD] THEN 2124 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN MATCH_ACCEPT_TAC SUM_TWO); 2125 2126val ABS_SUM = store_thm("ABS_SUM", 2127 ���!f m n. abs(sum(m,n) f) <= sum(m,n) (\n. abs(f n))���, 2128 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 2129 REWRITE_TAC[sum, ABS_0, REAL_LE_REFL] THEN BETA_TAC THEN 2130 MATCH_MP_TAC REAL_LE_TRANS THEN 2131 EXISTS_TAC ���abs(sum(m,n) f) + abs(f(m + n))��� THEN 2132 ASM_REWRITE_TAC[ABS_TRIANGLE, REAL_LE_RADD]); 2133 2134val SUM_LE = store_thm("SUM_LE", 2135 ���!f g m n. (!r. m <= r /\ r < (n + m) ==> f(r) <= g(r)) 2136 ==> (sum(m,n) f <= sum(m,n) g)���, 2137 EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN 2138 INDUCT_TAC THEN REWRITE_TAC[sum, REAL_LE_REFL] THEN 2139 DISCH_TAC THEN MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THEN 2140 FIRST_ASSUM MATCH_MP_TAC THENL 2141 [GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 2142 ASM_REWRITE_TAC[ADD_CLAUSES] THEN 2143 MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC ���n + m:num���, 2144 GEN_REWR_TAC (RAND_CONV o RAND_CONV) [ADD_SYM]] THEN 2145 ASM_REWRITE_TAC[ADD_CLAUSES, LESS_EQ_ADD, LESS_SUC_REFL]); 2146 2147val SUM_EQ = store_thm("SUM_EQ", 2148 ���!f g m n. (!r. m <= r /\ r < (n + m) ==> (f(r) = g(r))) 2149 ==> (sum(m,n) f = sum(m,n) g)���, 2150 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN 2151 CONJ_TAC THEN MATCH_MP_TAC SUM_LE THEN GEN_TAC THEN 2152 DISCH_THEN(fn th => MATCH_MP_TAC REAL_EQ_IMP_LE THEN 2153 FIRST_ASSUM(SUBST1_TAC o C MATCH_MP th)) THEN REFL_TAC); 2154 2155val SUM_POS = store_thm("SUM_POS", 2156 ���!f. (!n. 0 <= f(n)) ==> !m n. 0 <= sum(m,n) f���, 2157 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 2158 REWRITE_TAC[sum, REAL_LE_REFL] THEN 2159 MATCH_MP_TAC REAL_LE_ADD THEN ASM_REWRITE_TAC[]); 2160 2161val SUM_POS_GEN = store_thm("SUM_POS_GEN", 2162 ���!f m. (!n. m <= n ==> 0 <= f(n)) ==> 2163 !n. 0 <= sum(m,n) f���, 2164 REPEAT GEN_TAC THEN DISCH_TAC THEN INDUCT_TAC THEN 2165 REWRITE_TAC[sum, REAL_LE_REFL] THEN 2166 MATCH_MP_TAC REAL_LE_ADD THEN 2167 ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2168 MATCH_ACCEPT_TAC LESS_EQ_ADD); 2169 2170val SUM_ABS = store_thm("SUM_ABS", 2171 ���!f m n. abs(sum(m,n) (\m. abs(f m))) = sum(m,n) (\m. abs(f m))���, 2172 GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[ABS_REFL] THEN 2173 GEN_TAC THEN MATCH_MP_TAC SUM_POS THEN BETA_TAC THEN 2174 REWRITE_TAC[ABS_POS]); 2175 2176val SUM_ABS_LE = store_thm("SUM_ABS_LE", 2177 ���!f m n. abs(sum(m,n) f) <= sum(m,n)(\n. abs(f n))���, 2178 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 2179 REWRITE_TAC[sum, ABS_0, REAL_LE_REFL] THEN 2180 MATCH_MP_TAC REAL_LE_TRANS THEN 2181 EXISTS_TAC ���abs(sum(m,n) f) + abs(f(m + n))��� THEN 2182 REWRITE_TAC[ABS_TRIANGLE] THEN BETA_TAC THEN 2183 ASM_REWRITE_TAC[REAL_LE_RADD]); 2184 2185val SUM_ZERO = store_thm("SUM_ZERO", 2186 ���!f N. (!n. n >= N ==> (f(n) = 0)) 2187 ==> 2188 (!m n. m >= N ==> (sum(m,n) f = 0))���, 2189 REPEAT GEN_TAC THEN DISCH_TAC THEN 2190 MAP_EVERY X_GEN_TAC [���m:num���, ���n:num���] THEN 2191 REWRITE_TAC[GREATER_EQ] THEN 2192 DISCH_THEN(X_CHOOSE_THEN ���d:num��� SUBST1_TAC o MATCH_MP LESS_EQUAL_ADD) 2193 THEN 2194 SPEC_TAC(���n:num���,���n:num���) THEN INDUCT_TAC THEN REWRITE_TAC[sum] 2195 THEN 2196 ASM_REWRITE_TAC[REAL_ADD_LID] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2197 REWRITE_TAC[GREATER_EQ, GSYM ADD_ASSOC, LESS_EQ_ADD]); 2198 2199val SUM_ADD = store_thm("SUM_ADD", 2200 ���!f g m n. 2201 sum(m,n) (\n. f(n) + g(n)) 2202 = 2203 sum(m,n) f + sum(m,n) g���, 2204 EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN 2205 ASM_REWRITE_TAC[sum, REAL_ADD_LID] THEN BETA_TAC THEN 2206 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 2207 2208val SUM_CMUL = store_thm("SUM_CMUL", 2209 ���!f c m n. sum(m,n) (\n. c * f(n)) = c * sum(m,n) f���, 2210 EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN 2211 ASM_REWRITE_TAC[sum, REAL_MUL_RZERO] THEN BETA_TAC THEN 2212 REWRITE_TAC[REAL_LDISTRIB]); 2213 2214val SUM_NEG = store_thm("SUM_NEG", 2215 ���!f n d. sum(n,d) (\n. ~(f n)) = ~(sum(n,d) f)���, 2216 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 2217 ASM_REWRITE_TAC[sum, REAL_NEG_0] THEN 2218 BETA_TAC THEN REWRITE_TAC[REAL_NEG_ADD]); 2219 2220val SUM_SUB = store_thm("SUM_SUB", 2221 ���!f g m n. 2222 sum(m,n)(\n. (f n) - (g n)) 2223 = sum(m,n) f - sum(m,n) g���, 2224 REPEAT GEN_TAC THEN REWRITE_TAC[real_sub, GSYM SUM_NEG, GSYM SUM_ADD] THEN 2225 BETA_TAC THEN REFL_TAC); 2226 2227val SUM_SUBST = store_thm("SUM_SUBST", 2228 ���!f g m n. (!p. m <= p /\ p < (m + n) ==> (f p = g p)) 2229 ==> (sum(m,n) f = sum(m,n) g)���, 2230 EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN 2231 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN BINOP_TAC THEN 2232 FIRST_ASSUM MATCH_MP_TAC THENL 2233 [GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN 2234 ASM_REWRITE_TAC[ADD_CLAUSES] THEN 2235 MATCH_MP_TAC LESS_EQ_IMP_LESS_SUC THEN 2236 MATCH_MP_TAC LESS_IMP_LESS_OR_EQ THEN ASM_REWRITE_TAC[], 2237 REWRITE_TAC[LESS_EQ_ADD] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN 2238 MATCH_MP_TAC LESS_MONO_ADD THEN REWRITE_TAC[LESS_SUC_REFL]]); 2239 2240val SUM_NSUB = store_thm("SUM_NSUB", 2241 ���!n f c. 2242 sum(0,n) f - (&n * c) 2243 = 2244 sum(0,n)(\p. f(p) - c)���, 2245 INDUCT_TAC THEN REWRITE_TAC[sum, REAL_MUL_LZERO, REAL_SUB_REFL] THEN 2246 REWRITE_TAC[ADD_CLAUSES, REAL, REAL_RDISTRIB] THEN BETA_TAC THEN 2247 REPEAT GEN_TAC THEN POP_ASSUM(fn th => REWRITE_TAC[GSYM th]) THEN 2248 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_MUL_LID] THEN 2249 CONV_TAC(AC_CONV(REAL_ADD_ASSOC,REAL_ADD_SYM))); 2250 2251val SUM_BOUND = store_thm("SUM_BOUND", 2252 ���!f k m n. (!p. m <= p /\ p < (m + n) ==> (f(p) <= k)) 2253 ==> (sum(m,n) f <= (&n * k))���, 2254 EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN 2255 REWRITE_TAC[sum, REAL_MUL_LZERO, REAL_LE_REFL] THEN 2256 DISCH_TAC THEN REWRITE_TAC[REAL, REAL_RDISTRIB] THEN 2257 MATCH_MP_TAC REAL_LE_ADD2 THEN CONJ_TAC THENL 2258 [FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN DISCH_TAC THEN 2259 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN 2260 FIRST_ASSUM(MP_TAC o CONJUNCT2) THEN REWRITE_TAC[ADD_CLAUSES] THEN 2261 MATCH_ACCEPT_TAC LESS_SUC, 2262 REWRITE_TAC[REAL_MUL_LID] THEN FIRST_ASSUM MATCH_MP_TAC THEN 2263 REWRITE_TAC[ADD_CLAUSES, LESS_EQ_ADD] THEN 2264 MATCH_ACCEPT_TAC LESS_SUC_REFL]); 2265 2266val SUM_GROUP = store_thm("SUM_GROUP", 2267 ���!n k f. sum(0,n)(\m. sum(m * k,k) f) = sum(0,n * k) f���, 2268 INDUCT_TAC THEN REWRITE_TAC[sum, MULT_CLAUSES] THEN 2269 REPEAT GEN_TAC THEN BETA_TAC THEN ASM_REWRITE_TAC[] THEN 2270 REWRITE_TAC[ADD_CLAUSES, SUM_TWO]); 2271 2272val SUM_1 = store_thm("SUM_1", 2273 ���!f n. sum(n,1) f = f(n)���, 2274 REPEAT GEN_TAC THEN 2275 REWRITE_TAC[num_CONV ���1:num���, sum, ADD_CLAUSES, REAL_ADD_LID]); 2276 2277val SUM_2 = store_thm("SUM_2", 2278 ���!f n. sum(n,2) f = f(n) + f(n + 1)���, 2279 REPEAT GEN_TAC THEN CONV_TAC(REDEPTH_CONV num_CONV) THEN 2280 REWRITE_TAC[sum, ADD_CLAUSES, REAL_ADD_LID]); 2281 2282val SUM_OFFSET = store_thm("SUM_OFFSET", 2283 ���!f n k. 2284 sum(0,n)(\m. f(m + k)) 2285 = sum(0,n + k) f - sum(0,k) f���, 2286 REPEAT GEN_TAC THEN 2287 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN 2288 REWRITE_TAC[GSYM SUM_TWO, REAL_ADD_SUB] THEN 2289 SPEC_TAC(���n:num���,���n:num���) THEN 2290 INDUCT_TAC THEN REWRITE_TAC[sum] THEN 2291 BETA_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN AP_TERM_TAC THEN 2292 AP_TERM_TAC THEN MATCH_ACCEPT_TAC ADD_SYM); 2293 2294val SUM_REINDEX = store_thm("SUM_REINDEX", 2295 ���!f m k n. sum(m + k,n) f = sum(m,n)(\r. f(r + k))���, 2296 EVERY [GEN_TAC, GEN_TAC, GEN_TAC] THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN 2297 ASM_REWRITE_TAC[REAL_EQ_LADD] THEN BETA_TAC THEN AP_TERM_TAC THEN 2298 CONV_TAC(AC_CONV(ADD_ASSOC,ADD_SYM))); 2299 2300val SUM_0 = store_thm("SUM_0", 2301 ���!m n. sum(m,n)(\r. 0) = 0���, 2302 GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[sum] THEN 2303 BETA_TAC THEN ASM_REWRITE_TAC[REAL_ADD_LID]); 2304 2305val SUM_PERMUTE_0 = store_thm("SUM_PERMUTE_0", 2306 ���!n p. (!y. y < n ==> ?!x. x < n /\ (p(x) = y)) 2307 ==> !f. sum(0,n)(\n. f(p n)) = sum(0,n) f���, 2308 INDUCT_TAC THEN GEN_TAC THEN TRY(REWRITE_TAC[sum] THEN NO_TAC) THEN 2309 DISCH_TAC THEN GEN_TAC THEN FIRST_ASSUM(MP_TAC o SPEC ���n:num���) THEN 2310 REWRITE_TAC[LESS_SUC_REFL] THEN 2311 CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) THEN 2312 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC) THEN 2313 DISCH_THEN(X_CHOOSE_THEN ���k:num��� STRIP_ASSUME_TAC) THEN 2314 GEN_REWR_TAC RAND_CONV [sum] THEN 2315 REWRITE_TAC[ADD_CLAUSES] THEN 2316 ABBREV_TAC ���q:num->num = \r. if r < k then p(r) else p(SUC r)��� THEN 2317 SUBGOAL_THEN ���!y:num. y < n ==> ?!x. x < n /\ (q x = y)��� MP_TAC 2318 THENL 2319 [X_GEN_TAC ���y:num��� THEN DISCH_TAC THEN 2320 (MP_TAC o ASSUME) ���!y. y<SUC n ==> ?!x. x<SUC n /\ (p x = y)��� THEN 2321 DISCH_THEN(MP_TAC o SPEC ���y:num���) THEN 2322 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL 2323 [MATCH_MP_TAC LESS_TRANS THEN EXISTS_TAC ���n:num��� THEN 2324 ASM_REWRITE_TAC[LESS_SUC_REFL], 2325 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o C MP th))] THEN 2326 CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) THEN 2327 DISCH_THEN(X_CHOOSE_THEN ���x:num��� STRIP_ASSUME_TAC o CONJUNCT1) THEN 2328 CONJ_TAC THENL 2329 [DISJ_CASES_TAC(SPECL [���x:num���, ���k:num���] LESS_CASES) THENL 2330 [EXISTS_TAC ���x:num��� THEN EXPAND_TAC "q" THEN BETA_TAC THEN 2331 ASM_REWRITE_TAC[] THEN 2332 REWRITE_TAC[GSYM REAL_LT] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN 2333 EXISTS_TAC ���&k��� THEN ASM_REWRITE_TAC[REAL_LE, REAL_LT] THEN 2334 UNDISCH_TAC ���k < SUC n��� THEN 2335 REWRITE_TAC[LESS_EQ, LESS_EQ_MONO], 2336 MP_TAC(ASSUME ���k <= x:num���) THEN REWRITE_TAC[LESS_OR_EQ] THEN 2337 DISCH_THEN(DISJ_CASES_THEN2 ASSUME_TAC SUBST_ALL_TAC) THENL 2338 [EXISTS_TAC ���x - 1:num��� THEN EXPAND_TAC "q" THEN BETA_TAC THEN 2339 UNDISCH_TAC ���k < x:num��� THEN 2340 DISCH_THEN(X_CHOOSE_THEN ���d:num��� MP_TAC o MATCH_MP LESS_ADD_1) 2341 THEN 2342 REWRITE_TAC[GSYM ADD1, ADD_CLAUSES] THEN 2343 DISCH_THEN SUBST_ALL_TAC THEN REWRITE_TAC[SUC_SUB1] THEN 2344 RULE_ASSUM_TAC(REWRITE_RULE[LESS_MONO_EQ]) THEN 2345 ASM_REWRITE_TAC[] THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN 2346 UNDISCH_TAC ���(k + d) < k:num��� THEN 2347 REWRITE_TAC[LESS_EQ] THEN CONV_TAC CONTRAPOS_CONV THEN 2348 REWRITE_TAC[GSYM NOT_LESS, REWRITE_RULE[ADD_CLAUSES] LESS_ADD_SUC], 2349 SUBST_ALL_TAC(ASSUME ���(p:num->num) x = n���) THEN 2350 UNDISCH_TAC ���y < n:num��� THEN ASM_REWRITE_TAC[LESS_REFL]]], 2351 SUBGOAL_THEN 2352 ���!z. q z :num = p(if z < k then z else SUC z)��� MP_TAC THENL 2353 [GEN_TAC THEN EXPAND_TAC "q" THEN BETA_TAC THEN COND_CASES_TAC THEN 2354 REWRITE_TAC[], 2355 DISCH_THEN(fn th => REWRITE_TAC[th])] THEN 2356 MAP_EVERY X_GEN_TAC [���x1:num���, ���x2:num���] THEN STRIP_TAC THEN 2357 UNDISCH_TAC ���!y. y < SUC n ==> ?!x. x < SUC n /\ (p x = y)��� THEN 2358 DISCH_THEN(MP_TAC o SPEC ���y:num���) THEN 2359 REWRITE_TAC[MATCH_MP LESS_SUC (ASSUME ���y < n:num���)] THEN 2360 CONV_TAC(ONCE_DEPTH_CONV EXISTS_UNIQUE_CONV) THEN 2361 DISCH_THEN(MP_TAC 2362 o SPECL [���if x1 < (k:num) then x1 else SUC x1���, 2363 ���if x2 < (k:num) then x2 else SUC x2���] 2364 o CONJUNCT2) THEN 2365 ASM_REWRITE_TAC[] THEN 2366 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL 2367 [CONJ_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[LESS_MONO_EQ] THEN 2368 MATCH_MP_TAC LESS_SUC THEN ASM_REWRITE_TAC[], 2369 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o C MATCH_MP th)) THEN 2370 REPEAT COND_CASES_TAC THEN REWRITE_TAC[INV_SUC_EQ] THENL 2371 [DISCH_THEN SUBST_ALL_TAC THEN UNDISCH_TAC ���~(x2 < k:num)��� THEN 2372 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN 2373 REWRITE_TAC[] THEN MATCH_MP_TAC LESS_TRANS THEN 2374 EXISTS_TAC ���SUC x2��� THEN ASM_REWRITE_TAC[LESS_SUC_REFL], 2375 DISCH_THEN(SUBST_ALL_TAC o SYM) THEN 2376 UNDISCH_TAC ���~(x1 < k:num)��� THEN 2377 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN 2378 REWRITE_TAC[] THEN MATCH_MP_TAC LESS_TRANS THEN 2379 EXISTS_TAC ���SUC x1��� THEN ASM_REWRITE_TAC[LESS_SUC_REFL]]]], 2380 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN 2381 DISCH_THEN(fn th => GEN_REWR_TAC(RAND_CONV o ONCE_DEPTH_CONV)[GSYM th])THEN 2382 BETA_TAC THEN UNDISCH_TAC ���k < SUC n��� THEN 2383 REWRITE_TAC[LESS_EQ, LESS_EQ_MONO] THEN 2384 DISCH_THEN(X_CHOOSE_TAC ���d:num��� o MATCH_MP LESS_EQUAL_ADD) THEN 2385 GEN_REWR_TAC (RAND_CONV o RATOR_CONV o ONCE_DEPTH_CONV) 2386 [ASSUME ���n = k + d:num���] THEN 2387 REWRITE_TAC[GSYM SUM_TWO] THEN 2388 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) 2389 [ASSUME ���n = k + d:num���] THEN 2390 REWRITE_TAC[ONCE_REWRITE_RULE[ADD_SYM] ADD_SUC] THEN 2391 REWRITE_TAC[GSYM SUM_TWO, sum, ADD_CLAUSES] THEN BETA_TAC THEN 2392 REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN BINOP_TAC THENL 2393 [MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC ���r:num��� THEN 2394 REWRITE_TAC[ADD_CLAUSES] THEN STRIP_TAC THEN 2395 BETA_TAC THEN EXPAND_TAC "q" THEN ASM_REWRITE_TAC[], 2396 GEN_REWR_TAC RAND_CONV [REAL_ADD_SYM] THEN 2397 REWRITE_TAC[ASSUME ���(p:num->num) k = n���, REAL_EQ_LADD] THEN 2398 REWRITE_TAC[ADD1, SUM_REINDEX] THEN BETA_TAC THEN 2399 MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC ���r:num��� THEN BETA_TAC THEN 2400 REWRITE_TAC[GSYM NOT_LESS] THEN DISCH_TAC THEN 2401 EXPAND_TAC "q" THEN BETA_TAC THEN ASM_REWRITE_TAC[ADD1]]]); 2402 2403val SUM_CANCEL = store_thm("SUM_CANCEL", 2404 ���!f n d. 2405 sum(n,d) (\n. f(SUC n) - f(n)) 2406 = f(n + d) - f(n)���, 2407 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN 2408 ASM_REWRITE_TAC[sum, ADD_CLAUSES, REAL_SUB_REFL] THEN 2409 BETA_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN 2410 REWRITE_TAC[real_sub, REAL_NEG_ADD, REAL_ADD_ASSOC] THEN 2411 AP_THM_TAC THEN AP_TERM_TAC THEN 2412 REWRITE_TAC[GSYM REAL_ADD_ASSOC, REAL_ADD_LINV, REAL_ADD_RID]); 2413 2414(* ------------------------------------------------------------------------- *) 2415(* Theorems to be compatible with hol-light. *) 2416(* ------------------------------------------------------------------------- *) 2417 2418val REAL_MUL_RNEG = store_thm("REAL_MUL_RNEG", 2419 Term`!x y. x * ~y = ~(x * y)`, 2420 REPEAT GEN_TAC THEN 2421 MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL REAL_EQ_RADD)))) THEN 2422 EXISTS_TAC (Term`x:real * y`) THEN 2423 REWRITE_TAC[GSYM REAL_LDISTRIB, REAL_ADD_LINV, REAL_MUL_RZERO]); 2424 2425val REAL_MUL_LNEG = store_thm ("REAL_MUL_LNEG", 2426Term`!x y. ~x * y = ~(x * y)`, 2427 MESON_TAC[REAL_MUL_SYM, REAL_MUL_RNEG]); 2428 2429val real_lt = store_thm ("real_lt", 2430Term`!y x. x < y = ~(y <= x)`, 2431 let 2432 val th1 = TAUT_PROVE (Term`!t u:bool. (t = ~u) ==> (u = ~t)`) 2433 val th2 = SPECL [``y <= x``,``x < y``] th1 2434 val th3 = SPECL [``y:real``,``x:real``] real_lte 2435 in 2436 ACCEPT_TAC (GENL [``y:real``, ``x:real``] (MP th2 th3)) 2437 end); 2438 2439val REAL_LE_LADD_IMP = save_thm ("REAL_LE_LADD_IMP", 2440 let 2441 val th1 = GSYM (SPEC_ALL REAL_LE_LADD) 2442 val th2 = TAUT_PROVE ``(x:bool = y) ==> (x ==> y)`` 2443 in 2444 GEN ``x:real`` (GEN ``y:real`` (GEN ``z:real`` (MATCH_MP th2 th1))) 2445 end); 2446 2447val REAL_LE_LNEG = store_thm ("REAL_LE_LNEG", 2448 ``!x y. ~x <= y = 0 <= x + y``, 2449 REPEAT GEN_TAC THEN EQ_TAC THEN 2450 DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THENL 2451 [DISCH_THEN(MP_TAC o SPEC ``x:real``) THEN 2452 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV], 2453 DISCH_THEN(MP_TAC o SPEC ``~x``) THEN 2454 REWRITE_TAC[REAL_ADD_LINV, REAL_ADD_ASSOC, REAL_ADD_LID, 2455 ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]]); 2456 2457val REAL_LE_NEG2 = save_thm ("REAL_LE_NEG2", REAL_LE_NEG); 2458 2459val REAL_NEG_NEG = save_thm ("REAL_NEG_NEG", REAL_NEGNEG); 2460 2461val REAL_LE_RNEG = store_thm ("REAL_LE_RNEG", 2462 ``!x y. x <= ~y = x + y <= 0``, 2463 REPEAT GEN_TAC THEN 2464 GEN_REWR_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_NEG_NEG] THEN 2465 REWRITE_TAC[REAL_LE_LNEG, GSYM REAL_NEG_ADD] THEN 2466 GEN_REWR_TAC RAND_CONV [GSYM REAL_LE_NEG2] THEN 2467 AP_THM_TAC THEN AP_TERM_TAC THEN 2468 REWRITE_TAC[GSYM REAL_ADD_LINV] THEN 2469 REWRITE_TAC[REAL_NEG_ADD, REAL_NEG_NEG] THEN 2470 MATCH_ACCEPT_TAC REAL_ADD_SYM); 2471 2472val REAL_POW_INV = Q.store_thm 2473 ("REAL_POW_INV", 2474 `!x n. (inv x) pow n = inv(x pow n)`, 2475 Induct_on `n` THEN REWRITE_TAC [pow] THENL 2476 [REWRITE_TAC [REAL_INV1], 2477 GEN_TAC THEN Cases_on `x = 0r` THENL 2478 [POP_ASSUM SUBST_ALL_TAC 2479 THEN REWRITE_TAC [REAL_INV_0,REAL_MUL_LZERO], 2480 `~(x pow n = 0)` by PROVE_TAC [POW_NZ] THEN 2481 IMP_RES_TAC REAL_INV_MUL THEN ASM_REWRITE_TAC []]]); 2482 2483val REAL_POW_DIV = Q.store_thm 2484("REAL_POW_DIV", 2485 `!x y n. (x / y) pow n = (x pow n) / (y pow n)`, 2486 REWRITE_TAC[real_div, POW_MUL, REAL_POW_INV]); 2487 2488val REAL_POW_ADD = Q.store_thm 2489("REAL_POW_ADD", 2490 `!x m n. x pow (m + n) = x pow m * x pow n`, 2491 Induct_on `m` THEN 2492 ASM_REWRITE_TAC[ADD_CLAUSES, pow, REAL_MUL_LID, REAL_MUL_ASSOC]); 2493 2494val REAL_LE_RDIV_EQ = Q.store_thm 2495("REAL_LE_RDIV_EQ", 2496 `!x y z. &0 < z ==> (x <= y / z = x * z <= y)`, 2497 REPEAT STRIP_TAC THEN 2498 FIRST_ASSUM(fn th => 2499 Rewrite.GEN_REWRITE_TAC LAND_CONV Rewrite.empty_rewrites 2500 [GSYM(MATCH_MP REAL_LE_RMUL th)]) THEN 2501 RW_TAC bool_ss [real_div, GSYM REAL_MUL_ASSOC, REAL_MUL_LINV, 2502 REAL_MUL_RID, REAL_POS_NZ]); 2503 2504val REAL_LE_LDIV_EQ = Q.store_thm 2505("REAL_LE_LDIV_EQ", 2506 `!x y z. &0 < z ==> (x / z <= y = x <= y * z)`, 2507 REPEAT STRIP_TAC THEN 2508 FIRST_ASSUM(fn th => 2509 Rewrite.GEN_REWRITE_TAC LAND_CONV Rewrite.empty_rewrites 2510 [GSYM(MATCH_MP REAL_LE_RMUL th)]) THEN 2511 RW_TAC bool_ss [real_div, GSYM REAL_MUL_ASSOC, REAL_MUL_LINV, 2512 REAL_MUL_RID, REAL_POS_NZ]); 2513 2514val REAL_LT_RDIV_EQ = Q.store_thm 2515("REAL_LT_RDIV_EQ", 2516 `!x y z. &0 < z ==> (x < y / z = x * z < y)`, 2517 RW_TAC bool_ss [GSYM REAL_NOT_LE, REAL_LE_LDIV_EQ]); 2518 2519val REAL_LT_LDIV_EQ = Q.store_thm 2520("REAL_LT_LDIV_EQ", 2521 `!x y z. &0 < z ==> (x / z < y = x < y * z)`, 2522 RW_TAC bool_ss [GSYM REAL_NOT_LE, REAL_LE_RDIV_EQ]); 2523 2524val REAL_EQ_RDIV_EQ = Q.store_thm 2525("REAL_EQ_RDIV_EQ", 2526 `!x y z. &0 < z ==> ((x = y / z) = (x * z = y))`, 2527 REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN 2528 RW_TAC bool_ss [REAL_LE_RDIV_EQ, REAL_LE_LDIV_EQ]); 2529 2530val REAL_EQ_LDIV_EQ = Q.store_thm 2531("REAL_EQ_LDIV_EQ", 2532 `!x y z. &0 < z ==> ((x / z = y) = (x = y * z))`, 2533 REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN 2534 RW_TAC bool_ss [REAL_LE_RDIV_EQ, REAL_LE_LDIV_EQ]); 2535 2536val REAL_OF_NUM_POW = Q.store_thm 2537("REAL_OF_NUM_POW", 2538 `!x n. (&x) pow n = &(x EXP n)`, 2539 Induct_on `n` THEN ASM_REWRITE_TAC[pow, EXP, REAL_MUL]); 2540 2541val REAL_ADD_LDISTRIB = save_thm ("REAL_ADD_LDISTRIB", REAL_LDISTRIB); 2542 2543val REAL_ADD_RDISTRIB = save_thm ("REAL_ADD_RDISTRIB", REAL_RDISTRIB); 2544 2545val REAL_OF_NUM_ADD = save_thm ("REAL_OF_NUM_ADD", REAL_ADD); 2546 2547val REAL_OF_NUM_LE = save_thm ("REAL_OF_NUM_LE", REAL_LE); 2548 2549val REAL_OF_NUM_MUL = save_thm ("REAL_OF_NUM_MUL", REAL_MUL); 2550 2551val REAL_OF_NUM_SUC = store_thm ( 2552 "REAL_OF_NUM_SUC", 2553 ``!n. &n + &1 = &(SUC n)``, 2554 REWRITE_TAC[ADD1, REAL_ADD]); 2555 2556val REAL_OF_NUM_EQ = save_thm ("REAL_OF_NUM_EQ", REAL_INJ); 2557 2558val REAL_EQ_MUL_LCANCEL = store_thm ( 2559 "REAL_EQ_MUL_LCANCEL", 2560 ``!x y z. (x * y = x * z) = (x = 0) \/ (y = z)``, 2561 REWRITE_TAC [REAL_EQ_LMUL]); 2562 2563val REAL_ABS_0 = save_thm ("REAL_ABS_0", ABS_0); 2564val _ = export_rewrites ["REAL_ABS_0"] 2565 2566val REAL_ABS_TRIANGLE = save_thm ("REAL_ABS_TRIANGLE", ABS_TRIANGLE); 2567 2568val REAL_ABS_MUL = save_thm ("REAL_ABS_MUL", ABS_MUL); 2569 2570val REAL_ABS_POS = save_thm ("REAL_ABS_POS", ABS_POS); 2571 2572val REAL_LE_EPSILON = store_thm 2573 ("REAL_LE_EPSILON", 2574 ``!x y : real. (!e. 0 < e ==> x <= y + e) ==> x <= y``, 2575 RW_TAC boolSimps.bool_ss [] 2576 THEN (SUFF_TAC ``~(0r < x - y)`` 2577 THEN1 RW_TAC boolSimps.bool_ss 2578 [REAL_NOT_LT, REAL_LE_SUB_RADD, REAL_ADD_LID]) 2579 THEN STRIP_TAC 2580 THEN Q.PAT_X_ASSUM `!e. P e` MP_TAC 2581 THEN RW_TAC boolSimps.bool_ss [] 2582 THEN (KNOW_TAC ``!a b c : real. ~(a <= b + c) = c < a - b`` 2583 THEN1 (RW_TAC boolSimps.bool_ss [REAL_LT_SUB_LADD, REAL_NOT_LE] 2584 THEN PROVE_TAC [REAL_ADD_SYM])) 2585 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 2586 THEN PROVE_TAC [REAL_DOWN]); 2587 2588val REAL_BIGNUM = store_thm 2589 ("REAL_BIGNUM", 2590 ``!r : real. ?n : num. r < &n``, 2591 GEN_TAC 2592 THEN MP_TAC (Q.SPEC `1` REAL_ARCH) 2593 THEN REWRITE_TAC [REAL_LT_01, REAL_MUL_RID] 2594 THEN PROVE_TAC []); 2595 2596val REAL_INV_LT_ANTIMONO = store_thm 2597 ("REAL_INV_LT_ANTIMONO", 2598 ``!x y : real. 0 < x /\ 0 < y ==> (inv x < inv y = y < x)``, 2599 RW_TAC boolSimps.bool_ss [] 2600 THEN (REVERSE EQ_TAC THEN1 PROVE_TAC [REAL_LT_INV]) 2601 THEN STRIP_TAC 2602 THEN ONCE_REWRITE_TAC [GSYM REAL_INV_INV] 2603 THEN MATCH_MP_TAC REAL_LT_INV 2604 THEN RW_TAC boolSimps.bool_ss [REAL_INV_POS]); 2605 2606val REAL_INV_INJ = store_thm 2607 ("REAL_INV_INJ", 2608 ``!x y : real. (inv x = inv y) = (x = y)``, 2609 PROVE_TAC [REAL_INV_INV]) 2610 2611val REAL_DIV_RMUL_CANCEL = store_thm 2612 ("REAL_DIV_RMUL_CANCEL", 2613 ``!c a b : real. ~(c = 0) ==> ((a * c) / (b * c) = a / b)``, 2614 RW_TAC boolSimps.bool_ss [real_div] 2615 THEN Cases_on `b = 0` 2616 THEN RW_TAC boolSimps.bool_ss 2617 [REAL_MUL_LZERO, REAL_INV_0, REAL_INV_MUL, REAL_MUL_RZERO, 2618 REAL_EQ_MUL_LCANCEL, GSYM REAL_MUL_ASSOC] 2619 THEN DISJ2_TAC 2620 THEN (KNOW_TAC ``!a b c : real. a * (b * c) = (a * c) * b`` 2621 THEN1 PROVE_TAC [REAL_MUL_ASSOC, REAL_MUL_SYM]) 2622 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 2623 THEN RW_TAC boolSimps.bool_ss [REAL_MUL_RINV, REAL_MUL_LID]); 2624 2625val REAL_DIV_LMUL_CANCEL = store_thm 2626 ("REAL_DIV_LMUL_CANCEL", 2627 ``!c a b : real. ~(c = 0) ==> ((c * a) / (c * b) = a / b)``, 2628 METIS_TAC [REAL_DIV_RMUL_CANCEL, REAL_MUL_SYM]); 2629 2630val REAL_DIV_ADD = store_thm 2631 ("REAL_DIV_ADD", 2632 ``!x y z : real. y / x + z / x = (y + z) / x``, 2633 RW_TAC boolSimps.bool_ss [real_div, REAL_ADD_RDISTRIB]); 2634 2635val REAL_ADD_RAT = store_thm 2636 ("REAL_ADD_RAT", 2637 ``!a b c d : real. 2638 ~(b = 0) /\ ~(d = 0) ==> 2639 (a / b + c / d = (a * d + b * c) / (b * d))``, 2640 RW_TAC boolSimps.bool_ss 2641 [GSYM REAL_DIV_ADD, REAL_DIV_RMUL_CANCEL, REAL_DIV_LMUL_CANCEL]); 2642 2643val REAL_SUB_RAT = store_thm 2644 ("REAL_SUB_RAT", 2645 ``!a b c d : real. 2646 ~(b = 0) /\ ~(d = 0) ==> 2647 (a / b - c / d = (a * d - b * c) / (b * d))``, 2648 RW_TAC boolSimps.bool_ss [real_sub, real_div, REAL_NEG_LMUL] 2649 THEN RW_TAC boolSimps.bool_ss [GSYM real_div] 2650 THEN METIS_TAC [REAL_ADD_RAT, REAL_NEG_LMUL, REAL_NEG_RMUL]); 2651 2652val REAL_SUB = store_thm 2653 ("REAL_SUB", 2654 ``!m n : num. 2655 (& m : real) - & n = if m - n = 0 then ~(& (n - m)) else & (m - n)``, 2656 RW_TAC old_arith_ss [REAL_EQ_SUB_RADD, REAL_ADD] 2657 THEN ONCE_REWRITE_TAC [REAL_ADD_SYM] 2658 THEN RW_TAC old_arith_ss [GSYM real_sub, REAL_EQ_SUB_LADD, REAL_ADD]); 2659 2660(* ------------------------------------------------------------------------- *) 2661(* Define a constant for extracting "the positive part" of real numbers. *) 2662(* ------------------------------------------------------------------------- *) 2663 2664val pos_def = Define `pos (x : real) = if 0 <= x then x else 0`; 2665 2666val REAL_POS_POS = store_thm 2667 ("REAL_POS_POS", 2668 ``!x. 0 <= pos x``, 2669 RW_TAC boolSimps.bool_ss [pos_def, REAL_LE_REFL]); 2670 2671val REAL_POS_ID = store_thm 2672 ("REAL_POS_ID", 2673 ``!x. 0 <= x ==> (pos x = x)``, 2674 RW_TAC boolSimps.bool_ss [pos_def]); 2675 2676val REAL_POS_INFLATE = store_thm 2677 ("REAL_POS_INFLATE", 2678 ``!x. x <= pos x``, 2679 RW_TAC boolSimps.bool_ss [pos_def, REAL_LE_REFL] 2680 THEN PROVE_TAC [REAL_LE_TOTAL]); 2681 2682val REAL_POS_MONO = store_thm 2683 ("REAL_POS_MONO", 2684 ``!x y. x <= y ==> pos x <= pos y``, 2685 RW_TAC boolSimps.bool_ss [pos_def, REAL_LE_REFL] 2686 THEN PROVE_TAC [REAL_LE_TOTAL, REAL_LE_TRANS]); 2687 2688val REAL_POS_EQ_ZERO = store_thm 2689 ("REAL_POS_EQ_ZERO", 2690 ``!x. (pos x = 0) = x <= 0``, 2691 RW_TAC boolSimps.bool_ss [pos_def] 2692 THEN PROVE_TAC [REAL_LE_ANTISYM, REAL_LE_TOTAL]) 2693 2694val REAL_POS_LE_ZERO = store_thm 2695 ("REAL_POS_LE_ZERO", 2696 ``!x. (pos x <= 0) = x <= 0``, 2697 RW_TAC boolSimps.bool_ss [pos_def] 2698 THEN PROVE_TAC [REAL_LE_ANTISYM, REAL_LE_TOTAL]) 2699 2700(* ------------------------------------------------------------------------- *) 2701(* Define the minimum of two real numbers *) 2702(* ------------------------------------------------------------------------- *) 2703 2704val min_def = Define `min (x : real) y = if x <= y then x else y`; 2705 2706val REAL_MIN_REFL = store_thm 2707 ("REAL_MIN_REFL", 2708 ``!x. min x x = x``, 2709 RW_TAC boolSimps.bool_ss [min_def]); 2710 2711val REAL_LE_MIN = store_thm 2712 ("REAL_LE_MIN", 2713 ``!z x y. z <= min x y = z <= x /\ z <= y``, 2714 RW_TAC boolSimps.bool_ss [min_def] 2715 THEN PROVE_TAC [REAL_LE_TRANS, REAL_LE_TOTAL]); 2716 2717val REAL_MIN_LE = store_thm 2718 ("REAL_MIN_LE", 2719 ``!z x y. min x y <= z = x <= z \/ y <= z``, 2720 RW_TAC boolSimps.bool_ss [min_def, REAL_LE_REFL] 2721 THEN PROVE_TAC [REAL_LE_TOTAL, REAL_LE_TRANS]); 2722 2723val REAL_MIN_LE1 = store_thm 2724 ("REAL_MIN_LE1", 2725 ``!x y. min x y <= x``, 2726 RW_TAC boolSimps.bool_ss [REAL_MIN_LE, REAL_LE_REFL]); 2727 2728val REAL_MIN_LE2 = store_thm 2729 ("REAL_MIN_LE2", 2730 ``!x y. min x y <= y``, 2731 RW_TAC boolSimps.bool_ss [REAL_MIN_LE, REAL_LE_REFL]); 2732 2733val REAL_LT_MIN = store_thm 2734 ("REAL_LT_MIN", 2735 ``!x y z. z < min x y <=> z < x /\ z < y``, 2736 RW_TAC boolSimps.bool_ss [min_def] 2737 THEN PROVE_TAC [REAL_LTE_TRANS, REAL_LT_TRANS, REAL_NOT_LE]); 2738 2739val REAL_MIN_LT = store_thm 2740 ("REAL_MIN_LT", 2741 ``!x y z:real. min x y < z <=> x < z \/ y < z``, 2742 RW_TAC boolSimps.bool_ss [min_def] 2743 THEN PROVE_TAC [REAL_LTE_TRANS, REAL_LT_TRANS, REAL_NOT_LE]); 2744 2745val REAL_MIN_ALT = store_thm 2746 ("REAL_MIN_ALT", 2747 ``!x y. (x <= y ==> (min x y = x)) /\ (y <= x ==> (min x y = y))``, 2748 RW_TAC boolSimps.bool_ss [min_def] 2749 THEN PROVE_TAC [REAL_LE_ANTISYM]); 2750 2751val REAL_MIN_LE_LIN = store_thm 2752 ("REAL_MIN_LE_LIN", 2753 ``!z x y. 0 <= z /\ z <= 1 ==> min x y <= z * x + (1 - z) * y``, 2754 RW_TAC boolSimps.bool_ss [] 2755 THEN MP_TAC (Q.SPECL [`x`, `y`] REAL_LE_TOTAL) 2756 THEN (STRIP_TAC THEN RW_TAC boolSimps.bool_ss [REAL_MIN_ALT]) 2757 THENL [MATCH_MP_TAC REAL_LE_TRANS 2758 THEN Q.EXISTS_TAC `z * x + (1 - z) * x` 2759 THEN (CONJ_TAC THEN1 2760 RW_TAC boolSimps.bool_ss 2761 [GSYM REAL_RDISTRIB, REAL_SUB_ADD2, REAL_LE_REFL, REAL_MUL_LID]) 2762 THEN MATCH_MP_TAC REAL_LE_ADD2 2763 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LE_REFL]) 2764 THEN MATCH_MP_TAC REAL_LE_LMUL_IMP 2765 THEN ASM_REWRITE_TAC [REAL_SUB_LE], 2766 MATCH_MP_TAC REAL_LE_TRANS 2767 THEN Q.EXISTS_TAC `z * y + (1 - z) * y` 2768 THEN (CONJ_TAC THEN1 2769 RW_TAC boolSimps.bool_ss 2770 [GSYM REAL_RDISTRIB, REAL_SUB_ADD2, REAL_LE_REFL, REAL_MUL_LID]) 2771 THEN MATCH_MP_TAC REAL_LE_ADD2 2772 THEN (REVERSE CONJ_TAC THEN1 PROVE_TAC [REAL_LE_REFL]) 2773 THEN MATCH_MP_TAC REAL_LE_LMUL_IMP 2774 THEN ASM_REWRITE_TAC []]); 2775 2776val REAL_MIN_ADD = store_thm 2777 ("REAL_MIN_ADD", 2778 ``!z x y. min (x + z) (y + z) = min x y + z``, 2779 RW_TAC boolSimps.bool_ss [min_def, REAL_LE_RADD]); 2780 2781val REAL_MIN_SUB = store_thm 2782 ("REAL_MIN_SUB", 2783 ``!z x y. min (x - z) (y - z) = min x y - z``, 2784 RW_TAC boolSimps.bool_ss [min_def, REAL_LE_SUB_RADD, REAL_SUB_ADD]); 2785 2786val REAL_IMP_MIN_LE2 = store_thm 2787 ("REAL_IMP_MIN_LE2", 2788 ``!x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> min x1 x2 <= min y1 y2``, 2789 RW_TAC boolSimps.bool_ss [REAL_LE_MIN] 2790 THEN RW_TAC boolSimps.bool_ss [REAL_MIN_LE]); 2791 2792(* from rich_topologyTheory *) 2793val REAL_MIN_ACI = store_thm 2794 ("REAL_MIN_ACI", 2795 ``!x y z. (min x y = min y x) /\ 2796 (min (min x y) z = min x (min y z)) /\ 2797 (min x (min y z) = min y (min x z)) /\ 2798 (min x x = x) /\ 2799 (min x (min x y) = min x y)``, 2800 RW_TAC bool_ss [min_def] 2801 >> FULL_SIMP_TAC bool_ss [] (* 7 subgoals *) 2802 >| [ PROVE_TAC [REAL_LE_ANTISYM], 2803 PROVE_TAC [REAL_NOT_LE, REAL_LT_ANTISYM], 2804 REV_FULL_SIMP_TAC bool_ss [], 2805 Cases_on `y <= z` 2806 >- ( FULL_SIMP_TAC bool_ss [] \\ 2807 PROVE_TAC [REAL_LE_TRANS] ) \\ 2808 FULL_SIMP_TAC bool_ss [] >> FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2809 `x <= y` by PROVE_TAC [REAL_LET_TRANS, REAL_LT_IMP_LE] \\ 2810 FULL_SIMP_TAC bool_ss [] \\ 2811 PROVE_TAC [REAL_LTE_ANTISYM], 2812 REVERSE (Cases_on `(y <= z)`) 2813 >- ( FULL_SIMP_TAC bool_ss [] >> REV_FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2814 PROVE_TAC [REAL_LTE_ANTISYM, REAL_LTE_TRANS] ) \\ 2815 FULL_SIMP_TAC bool_ss [] \\ 2816 FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2817 `x <= z` by PROVE_TAC [REAL_LE_TRANS] \\ 2818 FULL_SIMP_TAC bool_ss [] >> PROVE_TAC [REAL_LE_ANTISYM], 2819 FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2820 PROVE_TAC [REAL_LT_ANTISYM], 2821 REV_FULL_SIMP_TAC bool_ss [] ]); 2822 2823(* ------------------------------------------------------------------------- *) 2824(* Define the maximum of two real numbers *) 2825(* ------------------------------------------------------------------------- *) 2826 2827val max_def = Define `max (x : real) y = if x <= y then y else x`; 2828 2829val REAL_MAX_REFL = store_thm 2830 ("REAL_MAX_REFL", 2831 ``!x. max x x = x``, 2832 RW_TAC boolSimps.bool_ss [max_def]); 2833 2834val REAL_LE_MAX = store_thm 2835 ("REAL_LE_MAX", 2836 ``!z x y. z <= max x y = z <= x \/ z <= y``, 2837 RW_TAC boolSimps.bool_ss [max_def] 2838 THEN PROVE_TAC [REAL_LE_TOTAL, REAL_LE_TRANS]); 2839 2840val REAL_LE_MAX1 = store_thm 2841 ("REAL_LE_MAX1", 2842 ``!x y. x <= max x y``, 2843 RW_TAC boolSimps.bool_ss [REAL_LE_MAX, REAL_LE_REFL]); 2844 2845val REAL_LE_MAX2 = store_thm 2846 ("REAL_LE_MAX2", 2847 ``!x y. y <= max x y``, 2848 RW_TAC boolSimps.bool_ss [REAL_LE_MAX, REAL_LE_REFL]); 2849 2850val REAL_MAX_LE = store_thm 2851 ("REAL_MAX_LE", 2852 ``!z x y. max x y <= z = x <= z /\ y <= z``, 2853 RW_TAC boolSimps.bool_ss [max_def] 2854 THEN PROVE_TAC [REAL_LE_TRANS, REAL_LE_TOTAL]); 2855 2856val REAL_LT_MAX = store_thm 2857 ("REAL_LT_MAX", 2858 ``!x y z. z < max x y <=> z < x \/ z < y``, 2859 RW_TAC boolSimps.bool_ss [max_def] 2860 THEN PROVE_TAC [REAL_LT_TRANS, REAL_LTE_TRANS, REAL_NOT_LE]); 2861 2862val REAL_MAX_LT = store_thm 2863 ("REAL_MAX_LT", 2864 ``!x y z. max x y < z <=> x < z /\ y < z``, 2865 RW_TAC boolSimps.bool_ss [max_def] 2866 THEN PROVE_TAC [REAL_LT_TRANS, REAL_LTE_TRANS, REAL_NOT_LE]); 2867 2868val REAL_MAX_ALT = store_thm 2869 ("REAL_MAX_ALT", 2870 ``!x y. (x <= y ==> (max x y = y)) /\ (y <= x ==> (max x y = x))``, 2871 RW_TAC boolSimps.bool_ss [max_def] 2872 THEN PROVE_TAC [REAL_LE_ANTISYM]); 2873 2874val REAL_MAX_MIN = store_thm 2875 ("REAL_MAX_MIN", 2876 ``!x y. max x y = ~min (~x) (~y)``, 2877 REPEAT GEN_TAC 2878 THEN MP_TAC (Q.SPECL [`x`, `y`] REAL_LE_TOTAL) 2879 THEN STRIP_TAC 2880 THEN RW_TAC boolSimps.bool_ss 2881 [REAL_MAX_ALT, REAL_MIN_ALT, REAL_LE_NEG2, REAL_NEGNEG]); 2882 2883val REAL_MIN_MAX = store_thm 2884 ("REAL_MIN_MAX", 2885 ``!x y. min x y = ~max (~x) (~y)``, 2886 REPEAT GEN_TAC 2887 THEN MP_TAC (Q.SPECL [`x`, `y`] REAL_LE_TOTAL) 2888 THEN STRIP_TAC 2889 THEN RW_TAC boolSimps.bool_ss 2890 [REAL_MAX_ALT, REAL_MIN_ALT, REAL_LE_NEG2, REAL_NEGNEG]); 2891 2892val REAL_LIN_LE_MAX = store_thm 2893 ("REAL_LIN_LE_MAX", 2894 ``!z x y. 0 <= z /\ z <= 1 ==> z * x + (1 - z) * y <= max x y``, 2895 RW_TAC boolSimps.bool_ss [] 2896 THEN MP_TAC (Q.SPECL [`z`, `~x`, `~y`] REAL_MIN_LE_LIN) 2897 THEN RW_TAC boolSimps.bool_ss 2898 [REAL_MIN_MAX, REAL_NEGNEG, REAL_MUL_RNEG, GSYM REAL_NEG_ADD, 2899 REAL_LE_NEG2]); 2900 2901val REAL_MAX_ADD = store_thm 2902 ("REAL_MAX_ADD", 2903 ``!z x y. max (x + z) (y + z) = max x y + z``, 2904 RW_TAC boolSimps.bool_ss [max_def, REAL_LE_RADD]); 2905 2906val REAL_MAX_SUB = store_thm 2907 ("REAL_MAX_SUB", 2908 ``!z x y. max (x - z) (y - z) = max x y - z``, 2909 RW_TAC boolSimps.bool_ss [max_def, REAL_LE_SUB_RADD, REAL_SUB_ADD]); 2910 2911val REAL_IMP_MAX_LE2 = store_thm 2912 ("REAL_IMP_MAX_LE2", 2913 ``!x1 x2 y1 y2. x1 <= y1 /\ x2 <= y2 ==> max x1 x2 <= max y1 y2``, 2914 RW_TAC boolSimps.bool_ss [REAL_MAX_LE] 2915 THEN RW_TAC boolSimps.bool_ss [REAL_LE_MAX]); 2916 2917(* from rich_topologyTheory *) 2918val REAL_MAX_ACI = store_thm 2919 ("REAL_MAX_ACI", 2920 ``!x y z. (max x y = max y x) /\ 2921 (max (max x y) z = max x (max y z)) /\ 2922 (max x (max y z) = max y (max x z)) /\ 2923 (max x x = x) /\ 2924 (max x (max x y) = max x y)``, 2925 RW_TAC bool_ss [max_def] 2926 >> FULL_SIMP_TAC bool_ss [] (* 7 subgoals *) 2927 >| [ PROVE_TAC [REAL_LE_ANTISYM], 2928 PROVE_TAC [REAL_NOT_LE, REAL_LT_ANTISYM], 2929 REVERSE (Cases_on `(y <= z)`) 2930 >- ( FULL_SIMP_TAC bool_ss [] >> FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2931 PROVE_TAC [REAL_LT_ANTISYM, REAL_LET_TRANS] ) \\ 2932 FULL_SIMP_TAC bool_ss [] \\ 2933 FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2934 `~(x <= y)` by PROVE_TAC [REAL_LET_TRANS, REAL_NOT_LE] \\ 2935 FULL_SIMP_TAC bool_ss [] \\ 2936 PROVE_TAC [REAL_LT_ANTISYM, REAL_LET_TRANS], 2937 REV_FULL_SIMP_TAC bool_ss [], 2938 REV_FULL_SIMP_TAC bool_ss [], 2939 PROVE_TAC [REAL_LE_ANTISYM], 2940 Cases_on `y <= z` 2941 >- ( FULL_SIMP_TAC bool_ss [] >> REV_FULL_SIMP_TAC bool_ss [] \\ 2942 FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2943 PROVE_TAC [REAL_LT_ANTISYM, REAL_LTE_TRANS] ) \\ 2944 FULL_SIMP_TAC bool_ss [] >> FULL_SIMP_TAC bool_ss [REAL_NOT_LE] \\ 2945 PROVE_TAC [REAL_LT_ANTISYM, REAL_LET_TRANS] ]); 2946 2947 2948(* ------------------------------------------------------------------------- *) 2949(* More theorems about sup, and corresponding theorems about an inf operator *) 2950(* ------------------------------------------------------------------------- *) 2951 2952val inf_def = Define `inf p = ~(sup (\r. p (~r)))`; 2953 2954val REAL_SUP_EXISTS_UNIQUE = store_thm 2955 ("REAL_SUP_EXISTS_UNIQUE", 2956 ``!p : real -> bool. 2957 (?x. p x) /\ (?z. !x. p x ==> x <= z) ==> 2958 ?!s. !y. (?x. p x /\ y < x) = y < s``, 2959 REPEAT STRIP_TAC 2960 THEN CONV_TAC EXISTS_UNIQUE_CONV 2961 THEN (RW_TAC boolSimps.bool_ss [] 2962 THEN1 (MP_TAC (Q.SPEC `p` REAL_SUP_LE) THEN PROVE_TAC [])) 2963 THEN REWRITE_TAC [GSYM REAL_LE_ANTISYM, GSYM REAL_NOT_LT] 2964 THEN REPEAT STRIP_TAC 2965 THENL [(SUFF_TAC ``!x : real. p x ==> ~(s' < x)`` THEN1 PROVE_TAC []) 2966 THEN REPEAT STRIP_TAC 2967 THEN (SUFF_TAC ``~((s' : real) < s')`` THEN1 PROVE_TAC []) 2968 THEN REWRITE_TAC [REAL_LT_REFL], 2969 (SUFF_TAC ``!x : real. p x ==> ~(s < x)`` THEN1 PROVE_TAC []) 2970 THEN REPEAT STRIP_TAC 2971 THEN (SUFF_TAC ``~((s : real) < s)`` THEN1 PROVE_TAC []) 2972 THEN REWRITE_TAC [REAL_LT_REFL]]); 2973 2974val REAL_SUP_MAX = store_thm 2975 ("REAL_SUP_MAX", 2976 ``!p z. p z /\ (!x. p x ==> x <= z) ==> (sup p = z)``, 2977 REPEAT STRIP_TAC 2978 THEN (KNOW_TAC ``!y : real. (?x. p x /\ y < x) = y < z`` 2979 THEN1 (STRIP_TAC 2980 THEN REVERSE EQ_TAC THEN1 PROVE_TAC [] 2981 THEN REPEAT STRIP_TAC 2982 THEN PROVE_TAC [REAL_LTE_TRANS])) 2983 THEN STRIP_TAC 2984 THEN (KNOW_TAC ``!y. (?x. p x /\ y < x) = y < sup p`` 2985 THEN1 PROVE_TAC [REAL_SUP_LE]) 2986 THEN STRIP_TAC 2987 THEN (KNOW_TAC ``(?x : real. p x) /\ (?z. !x. p x ==> x <= z)`` 2988 THEN1 PROVE_TAC []) 2989 THEN STRIP_TAC 2990 THEN ASSUME_TAC ((SPEC ``p:real->bool`` o CONV_RULE 2991 (DEPTH_CONV EXISTS_UNIQUE_CONV)) REAL_SUP_EXISTS_UNIQUE) 2992 THEN RES_TAC); 2993 2994val REAL_IMP_SUP_LE = store_thm 2995 ("REAL_IMP_SUP_LE", 2996 ``!p x. (?r. p r) /\ (!r. p r ==> r <= x) ==> sup p <= x``, 2997 RW_TAC boolSimps.bool_ss [] 2998 THEN REWRITE_TAC [GSYM REAL_NOT_LT] 2999 THEN STRIP_TAC 3000 THEN MP_TAC (SPEC ``p:real->bool`` REAL_SUP_LE) 3001 THEN RW_TAC boolSimps.bool_ss [] 3002 THENL [PROVE_TAC [], 3003 PROVE_TAC [], 3004 EXISTS_TAC ``x:real`` 3005 THEN RW_TAC boolSimps.bool_ss [] 3006 THEN PROVE_TAC [real_lte]]); 3007 3008val REAL_IMP_LE_SUP = store_thm 3009 ("REAL_IMP_LE_SUP", 3010 ``!p x. 3011 (?r. p r) /\ (?z. !r. p r ==> r <= z) /\ (?r. p r /\ x <= r) ==> 3012 x <= sup p``, 3013 RW_TAC boolSimps.bool_ss [] 3014 THEN (SUFF_TAC ``!y. p y ==> y <= sup p`` THEN1 PROVE_TAC [REAL_LE_TRANS]) 3015 THEN MATCH_MP_TAC REAL_SUP_UBOUND_LE 3016 THEN PROVE_TAC []); 3017 3018val REAL_INF_MIN = store_thm 3019 ("REAL_INF_MIN", 3020 ``!p z. p z /\ (!x. p x ==> z <= x) ==> (inf p = z)``, 3021 RW_TAC boolSimps.bool_ss [] 3022 THEN MP_TAC (SPECL [``(\r. (p:real->bool) (~r))``, ``~(z:real)``] 3023 REAL_SUP_MAX) 3024 THEN RW_TAC boolSimps.bool_ss [REAL_NEGNEG, inf_def] 3025 THEN (SUFF_TAC ``!x : real. p ~x ==> x <= ~z`` THEN1 PROVE_TAC [REAL_NEGNEG]) 3026 THEN REPEAT STRIP_TAC 3027 THEN ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 3028 THEN ONCE_REWRITE_TAC [REAL_LE_NEG] 3029 THEN REWRITE_TAC [REAL_NEGNEG] 3030 THEN PROVE_TAC []); 3031 3032val REAL_IMP_LE_INF = store_thm 3033 ("REAL_IMP_LE_INF", 3034 ``!p r. (?x. p x) /\ (!x. p x ==> r <= x) ==> r <= inf p``, 3035 RW_TAC boolSimps.bool_ss [inf_def] 3036 THEN POP_ASSUM MP_TAC 3037 THEN ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 3038 THEN Q.SPEC_TAC (`~r`, `r`) 3039 THEN RW_TAC boolSimps.bool_ss [REAL_NEGNEG, REAL_LE_NEG] 3040 THEN MATCH_MP_TAC REAL_IMP_SUP_LE 3041 THEN RW_TAC boolSimps.bool_ss [] 3042 THEN PROVE_TAC [REAL_NEGNEG]); 3043 3044val REAL_IMP_INF_LE = store_thm 3045 ("REAL_IMP_INF_LE", 3046 ``!p r. (?z. !x. p x ==> z <= x) /\ (?x. p x /\ x <= r) ==> inf p <= r``, 3047 RW_TAC boolSimps.bool_ss [inf_def] 3048 THEN POP_ASSUM MP_TAC 3049 THEN ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 3050 THEN Q.SPEC_TAC (`~r`, `r`) 3051 THEN RW_TAC boolSimps.bool_ss [REAL_NEGNEG, REAL_LE_NEG] 3052 THEN MATCH_MP_TAC REAL_IMP_LE_SUP 3053 THEN RW_TAC boolSimps.bool_ss [] 3054 THEN PROVE_TAC [REAL_NEGNEG, REAL_LE_NEG]); 3055 3056val REAL_INF_LT = store_thm 3057 ("REAL_INF_LT", 3058 ``!p z. (?x. p x) /\ inf p < z ==> (?x. p x /\ x < z)``, 3059 RW_TAC boolSimps.bool_ss [] 3060 THEN (SUFF_TAC ``~(!x. p x ==> ~(x < z))`` THEN1 PROVE_TAC []) 3061 THEN REWRITE_TAC [GSYM real_lte] 3062 THEN STRIP_TAC 3063 THEN Q.PAT_X_ASSUM `inf p < z` MP_TAC 3064 THEN RW_TAC boolSimps.bool_ss [GSYM real_lte] 3065 THEN MATCH_MP_TAC REAL_IMP_LE_INF 3066 THEN PROVE_TAC []); 3067 3068val REAL_INF_CLOSE = store_thm 3069 ("REAL_INF_CLOSE", 3070 ``!p e. (?x. p x) /\ 0 < e ==> (?x. p x /\ x < inf p + e)``, 3071 RW_TAC boolSimps.bool_ss [] 3072 THEN MATCH_MP_TAC REAL_INF_LT 3073 THEN (CONJ_TAC THEN1 PROVE_TAC []) 3074 THEN RW_TAC boolSimps.bool_ss [REAL_LT_ADDR]); 3075 3076val SUP_EPSILON = store_thm 3077 ("SUP_EPSILON", 3078 ``!p e. 3079 0 < e /\ (?x. p x) /\ (?z. !x. p x ==> x <= z) ==> 3080 ?x. p x /\ sup p <= x + e``, 3081 REPEAT GEN_TAC 3082 THEN REPEAT DISCH_TAC 3083 THEN REWRITE_TAC [GSYM REAL_NOT_LT] 3084 THEN MP_TAC (Q.SPEC `p` REAL_SUP_LE) 3085 THEN ASM_REWRITE_TAC [] 3086 THEN DISCH_THEN (fn th => REWRITE_TAC [GSYM th]) 3087 THEN POP_ASSUM MP_TAC 3088 THEN RW_TAC boolSimps.bool_ss [GSYM IMP_DISJ_THM, REAL_NOT_LT] 3089 THEN (SUFF_TAC 3090 ``?n : num. 3091 ?x : real. p x /\ z - &(SUC n) * e <= x /\ x <= z - & n * e /\ 3092 !y. p y ==> y <= z - &n * e`` 3093 THEN1 (RW_TAC boolSimps.bool_ss [] 3094 THEN Q.EXISTS_TAC `x'` 3095 THEN RW_TAC boolSimps.bool_ss [] 3096 THEN Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x''`) 3097 THEN RW_TAC boolSimps.bool_ss [] 3098 THEN MATCH_MP_TAC REAL_LE_TRANS 3099 THEN Q.EXISTS_TAC `z - &n * e` 3100 THEN RW_TAC boolSimps.bool_ss [] 3101 THEN (SUFF_TAC ``(z:real) - &n * e = z - &(SUC n) * e + 1 * e`` 3102 THEN1 RW_TAC boolSimps.bool_ss 3103 [REAL_MUL_LID, REAL_LE_RADD]) 3104 THEN RW_TAC boolSimps.bool_ss 3105 [real_sub, GSYM REAL_ADD_ASSOC, REAL_EQ_LADD] 3106 THEN ONCE_REWRITE_TAC [GSYM REAL_EQ_NEG] 3107 THEN RW_TAC boolSimps.bool_ss 3108 [REAL_NEGNEG, REAL_NEG_ADD, GSYM REAL_MUL_LNEG, 3109 GSYM REAL_ADD_RDISTRIB, REAL_EQ_RMUL] 3110 THEN DISJ2_TAC 3111 THEN RW_TAC boolSimps.bool_ss 3112 [REAL_EQ_SUB_LADD, GSYM real_sub, REAL_ADD, REAL_INJ, 3113 arithmeticTheory.ADD1])) 3114 THEN (KNOW_TAC ``?n : num. ?x : real. p x /\ z - &(SUC n) * e <= x`` 3115 THEN1 (MP_TAC (Q.SPEC `(z - x) / e` REAL_BIGNUM) 3116 THEN STRIP_TAC 3117 THEN Q.EXISTS_TAC `n` 3118 THEN Q.EXISTS_TAC `x` 3119 THEN RW_TAC boolSimps.bool_ss [REAL_LE_SUB_RADD] 3120 THEN ONCE_REWRITE_TAC [REAL_ADD_SYM] 3121 THEN REWRITE_TAC [GSYM REAL_LE_SUB_RADD] 3122 THEN (KNOW_TAC ``((z - x) / e) * e = (z:real) - x`` 3123 THEN1 (MATCH_MP_TAC REAL_DIV_RMUL 3124 THEN PROVE_TAC [REAL_LT_LE])) 3125 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 3126 THEN RW_TAC boolSimps.bool_ss [REAL_LE_RMUL] 3127 THEN MATCH_MP_TAC REAL_LE_TRANS 3128 THEN Q.EXISTS_TAC `&n` 3129 THEN REWRITE_TAC [REAL_LE] 3130 THEN PROVE_TAC 3131 [arithmeticTheory.LESS_EQ_SUC_REFL, REAL_LT_LE])) 3132 THEN DISCH_THEN (MP_TAC o HO_MATCH_MP LEAST_EXISTS_IMP) 3133 THEN Q.SPEC_TAC (`$LEAST (\n. ?x. p x /\ z - & (SUC n) * e <= x)`, `m`) 3134 THEN RW_TAC boolSimps.bool_ss [GSYM IMP_DISJ_THM] 3135 THEN Q.EXISTS_TAC `m` 3136 THEN Q.EXISTS_TAC `x'` 3137 THEN ASM_REWRITE_TAC [] 3138 THEN (Cases_on `m` 3139 THEN1 RW_TAC boolSimps.bool_ss [REAL_MUL_LZERO, REAL_SUB_RZERO]) 3140 THEN POP_ASSUM (MP_TAC o Q.SPEC `n`) 3141 THEN RW_TAC boolSimps.bool_ss [prim_recTheory.LESS_SUC_REFL, GSYM real_lt] 3142 THEN PROVE_TAC [REAL_LT_LE]); 3143 3144val REAL_LE_SUP = store_thm 3145 ("REAL_LE_SUP", 3146 ``!p x : real. 3147 (?y. p y) /\ (?y. !z. p z ==> z <= y) ==> 3148 (x <= sup p = !y. (!z. p z ==> z <= y) ==> x <= y)``, 3149 RW_TAC boolSimps.bool_ss [] 3150 THEN EQ_TAC 3151 THENL [RW_TAC boolSimps.bool_ss [] 3152 THEN MATCH_MP_TAC REAL_LE_EPSILON 3153 THEN RW_TAC boolSimps.bool_ss [GSYM REAL_LE_SUB_RADD] 3154 THEN (KNOW_TAC ``(x:real) - e < sup p`` 3155 THEN1 (MATCH_MP_TAC REAL_LTE_TRANS 3156 THEN Q.EXISTS_TAC `x` 3157 THEN RW_TAC boolSimps.bool_ss 3158 [REAL_LT_SUB_RADD, REAL_LT_ADDR])) 3159 THEN Q.PAT_X_ASSUM `0 < e` (K ALL_TAC) 3160 THEN Q.PAT_X_ASSUM `x <= sup p` (K ALL_TAC) 3161 THEN Q.SPEC_TAC (`x - e`, `x`) 3162 THEN GEN_TAC 3163 THEN MP_TAC (Q.SPEC `p` REAL_SUP_LE) 3164 THEN MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) 3165 THEN (CONJ_TAC THEN1 PROVE_TAC []) 3166 THEN DISCH_THEN (fn th => REWRITE_TAC [GSYM th]) 3167 THEN STRIP_TAC 3168 THEN MATCH_MP_TAC REAL_LE_TRANS 3169 THEN PROVE_TAC [REAL_LT_LE], 3170 RW_TAC boolSimps.bool_ss [] 3171 THEN MATCH_MP_TAC REAL_LE_EPSILON 3172 THEN RW_TAC boolSimps.bool_ss [GSYM REAL_LE_SUB_RADD] 3173 THEN (SUFF_TAC ``(x:real) - e < sup p`` THEN1 PROVE_TAC [REAL_LT_LE]) 3174 THEN Q.PAT_X_ASSUM `!y. P y` (MP_TAC o Q.SPEC `x - e`) 3175 THEN (KNOW_TAC ``!a b : real. a <= a - b = ~(0 < b)`` 3176 THEN1 (RW_TAC boolSimps.bool_ss [real_lt, REAL_LE_SUB_LADD] 3177 THEN PROVE_TAC [REAL_ADD_RID, REAL_LE_LADD])) 3178 THEN DISCH_THEN (fn th => ASM_REWRITE_TAC [th]) 3179 THEN POP_ASSUM (K ALL_TAC) 3180 THEN Q.SPEC_TAC (`x - e`, `x`) 3181 THEN GEN_TAC 3182 THEN RW_TAC boolSimps.bool_ss [] 3183 THEN MP_TAC (Q.SPEC `p` REAL_SUP_LE) 3184 THEN MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) 3185 THEN (CONJ_TAC THEN1 PROVE_TAC []) 3186 THEN DISCH_THEN (fn th => REWRITE_TAC [GSYM th]) 3187 THEN PROVE_TAC [real_lt]]); 3188 3189val REAL_INF_LE = store_thm 3190 ("REAL_INF_LE", 3191 ``!p x : real. 3192 (?y. p y) /\ (?y. !z. p z ==> y <= z) ==> 3193 (inf p <= x = !y. (!z. p z ==> y <= z) ==> y <= x)``, 3194 RW_TAC boolSimps.bool_ss [] 3195 THEN MP_TAC (Q.SPECL [`\r. p ~r`, `~x`] REAL_LE_SUP) 3196 THEN MATCH_MP_TAC (PROVE [] ``x /\ (y ==> z) ==> (x ==> y) ==> z``) 3197 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_NEGNEG, REAL_LE_NEG]) 3198 THEN ONCE_REWRITE_TAC [GSYM REAL_NEGNEG] 3199 THEN REWRITE_TAC [GSYM inf_def] 3200 THEN REWRITE_TAC [REAL_LE_NEG] 3201 THEN RW_TAC boolSimps.bool_ss [REAL_NEGNEG] 3202 THEN POP_ASSUM (K ALL_TAC) 3203 THEN EQ_TAC 3204 THEN RW_TAC boolSimps.bool_ss [] 3205 THEN Q.PAT_X_ASSUM `!a. (!b. P a b) ==> Q a` (MP_TAC o Q.SPEC `~y''`) 3206 THEN PROVE_TAC [REAL_NEGNEG, REAL_LE_NEG]); 3207 3208val REAL_SUP_CONST = store_thm 3209 ("REAL_SUP_CONST", 3210 ``!x : real. sup (\r. r = x) = x``, 3211 RW_TAC boolSimps.bool_ss [] 3212 THEN ONCE_REWRITE_TAC [GSYM REAL_LE_ANTISYM] 3213 THEN CONJ_TAC 3214 THENL [MATCH_MP_TAC REAL_IMP_SUP_LE 3215 THEN PROVE_TAC [REAL_LE_REFL], 3216 MATCH_MP_TAC REAL_IMP_LE_SUP 3217 THEN PROVE_TAC [REAL_LE_REFL]]); 3218 3219(* ------------------------------------------------------------------------- *) 3220(* Theorems to put in the real simpset *) 3221(* ------------------------------------------------------------------------- *) 3222 3223val REAL_MUL_SUB2_CANCEL = store_thm 3224 ("REAL_MUL_SUB2_CANCEL", 3225 ``!z x y : real. x * y + (z - x) * y = z * y``, 3226 RW_TAC boolSimps.bool_ss [GSYM REAL_RDISTRIB, REAL_SUB_ADD2]); 3227 3228val REAL_MUL_SUB1_CANCEL = store_thm 3229 ("REAL_MUL_SUB1_CANCEL", 3230 ``!z x y : real. y * x + y * (z - x) = y * z``, 3231 RW_TAC boolSimps.bool_ss [GSYM REAL_LDISTRIB, REAL_SUB_ADD2]); 3232 3233val REAL_NEG_HALF = store_thm 3234 ("REAL_NEG_HALF", 3235 ``!x : real. x - x / 2 = x / 2``, 3236 STRIP_TAC 3237 THEN (SUFF_TAC ``((x:real) - x / 2) + x / 2 = x / 2 + x / 2`` 3238 THEN1 RW_TAC boolSimps.bool_ss [REAL_EQ_RADD]) 3239 THEN RW_TAC boolSimps.bool_ss [REAL_SUB_ADD, REAL_HALF_DOUBLE]); 3240 3241val REAL_NEG_THIRD = store_thm 3242 ("REAL_NEG_THIRD", 3243 ``!x : real. x - x / 3 = (2 * x) / 3``, 3244 STRIP_TAC 3245 THEN MATCH_MP_TAC REAL_EQ_LMUL_IMP 3246 THEN Q.EXISTS_TAC `3` 3247 THEN (KNOW_TAC ``~(3r = 0)`` 3248 THEN1 (REWRITE_TAC [REAL_INJ] THEN numLib.ARITH_TAC)) 3249 THEN RW_TAC boolSimps.bool_ss [REAL_SUB_LDISTRIB, REAL_DIV_LMUL] 3250 THEN (KNOW_TAC ``!x y z : real. (y = 1 * x + z) ==> (y - x = z)`` 3251 THEN1 RW_TAC boolSimps.bool_ss [REAL_MUL_LID, REAL_ADD_SUB]) 3252 THEN DISCH_THEN MATCH_MP_TAC 3253 THEN RW_TAC boolSimps.bool_ss [GSYM REAL_ADD_RDISTRIB, REAL_ADD, 3254 REAL_EQ_RMUL, REAL_INJ] 3255 THEN DISJ2_TAC 3256 THEN numLib.ARITH_TAC); 3257 3258val REAL_DIV_DENOM_CANCEL = store_thm 3259 ("REAL_DIV_DENOM_CANCEL", 3260 ``!x y z : real. ~(x = 0) ==> ((y / x) / (z / x) = y / z)``, 3261 RW_TAC boolSimps.bool_ss [real_div] 3262 THEN (Cases_on `y = 0` THEN1 RW_TAC boolSimps.bool_ss [REAL_MUL_LZERO]) 3263 THEN (Cases_on `z = 0` 3264 THEN1 RW_TAC boolSimps.bool_ss 3265 [REAL_INV_0, REAL_MUL_RZERO, REAL_MUL_LZERO]) 3266 THEN RW_TAC boolSimps.bool_ss [REAL_INV_MUL, REAL_INV_EQ_0, REAL_INVINV] 3267 THEN (KNOW_TAC ``!a b c d : real. a * b * (c * d) = (a * c) * (b * d)`` 3268 THEN1 metisLib.METIS_TAC [REAL_MUL_SYM, REAL_MUL_ASSOC]) 3269 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 3270 THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_MUL_RID]); 3271 3272val REAL_DIV_DENOM_CANCEL2 = save_thm 3273 ("REAL_DIV_DENOM_CANCEL2", 3274 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ] 3275 (Q.SPEC `2` REAL_DIV_DENOM_CANCEL)); 3276 3277val REAL_DIV_DENOM_CANCEL3 = save_thm 3278 ("REAL_DIV_DENOM_CANCEL3", 3279 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ] 3280 (Q.SPEC `3` REAL_DIV_DENOM_CANCEL)); 3281 3282val REAL_DIV_INNER_CANCEL = store_thm 3283 ("REAL_DIV_INNER_CANCEL", 3284 ``!x y z : real. ~(x = 0) ==> ((y / x) * (x / z) = y / z)``, 3285 RW_TAC boolSimps.bool_ss [real_div] 3286 THEN (KNOW_TAC ``!a b c d : real. a * b * (c * d) = (a * d) * (b * c)`` 3287 THEN1 metisLib.METIS_TAC [REAL_MUL_SYM, REAL_MUL_ASSOC]) 3288 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 3289 THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_MUL_RID]); 3290 3291val REAL_DIV_INNER_CANCEL2 = save_thm 3292 ("REAL_DIV_INNER_CANCEL2", 3293 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ] 3294 (Q.SPEC `2` REAL_DIV_INNER_CANCEL)); 3295 3296val REAL_DIV_INNER_CANCEL3 = save_thm 3297 ("REAL_DIV_INNER_CANCEL3", 3298 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ] 3299 (Q.SPEC `3` REAL_DIV_INNER_CANCEL)); 3300 3301val REAL_DIV_OUTER_CANCEL = store_thm 3302 ("REAL_DIV_OUTER_CANCEL", 3303 ``!x y z : real. ~(x = 0) ==> ((x / y) * (z / x) = z / y)``, 3304 RW_TAC boolSimps.bool_ss [real_div] 3305 THEN (KNOW_TAC ``!a b c d : real. a * b * (c * d) = (a * d) * (c * b)`` 3306 THEN1 metisLib.METIS_TAC [REAL_MUL_SYM, REAL_MUL_ASSOC]) 3307 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 3308 THEN RW_TAC boolSimps.bool_ss [REAL_MUL_RINV, REAL_MUL_LID]); 3309 3310val REAL_DIV_OUTER_CANCEL2 = save_thm 3311 ("REAL_DIV_OUTER_CANCEL2", 3312 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ] 3313 (Q.SPEC `2` REAL_DIV_OUTER_CANCEL)); 3314 3315val REAL_DIV_OUTER_CANCEL3 = save_thm 3316 ("REAL_DIV_OUTER_CANCEL3", 3317 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ] 3318 (Q.SPEC `3` REAL_DIV_OUTER_CANCEL)); 3319 3320val REAL_DIV_REFL2 = save_thm 3321 ("REAL_DIV_REFL2", 3322 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(2n = 0)``, REAL_INJ] 3323 (Q.SPEC `2` REAL_DIV_REFL)); 3324 3325val REAL_DIV_REFL3 = save_thm 3326 ("REAL_DIV_REFL3", 3327 SIMP_RULE boolSimps.bool_ss [numLib.ARITH_PROVE ``~(3n = 0)``, REAL_INJ] 3328 (Q.SPEC `3` REAL_DIV_REFL)); 3329 3330val REAL_HALF_BETWEEN = store_thm 3331 ("REAL_HALF_BETWEEN", 3332 ``((0:real) < 1 / 2 /\ 1 / 2 < (1:real)) /\ 3333 ((0:real) <= 1 / 2 /\ 1 / 2 <= (1:real))``, 3334 MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``) 3335 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LE_TOTAL, real_lt]) 3336 THEN RW_TAC boolSimps.bool_ss [real_lt] 3337 THEN MP_TAC (Q.SPEC `2` REAL_LE_LMUL) 3338 THEN (KNOW_TAC ``0r < 2 /\ ~(2r = 0)`` 3339 THEN1 (REWRITE_TAC [REAL_LT, REAL_INJ] THEN numLib.ARITH_TAC)) 3340 THEN STRIP_TAC 3341 THEN ASM_REWRITE_TAC [] 3342 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 3343 THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] 3344 THEN RW_TAC boolSimps.bool_ss [real_div, GSYM REAL_MUL_ASSOC] 3345 THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_INJ] 3346 THEN RW_TAC boolSimps.bool_ss [REAL_MUL, REAL_LE] 3347 THEN numLib.ARITH_TAC); 3348 3349val REAL_THIRDS_BETWEEN = store_thm 3350 ("REAL_THIRDS_BETWEEN", 3351 ``((0:real) < 1 / 3 /\ 1 / 3 < (1:real) /\ 3352 (0:real) < 2 / 3 /\ 2 / 3 < (1:real)) /\ 3353 ((0:real) <= 1 / 3 /\ 1 / 3 <= (1:real) /\ 3354 (0:real) <= 2 / 3 /\ 2 / 3 <= (1:real))``, 3355 MATCH_MP_TAC (PROVE [] ``(x ==> y) /\ x ==> x /\ y``) 3356 THEN (CONJ_TAC THEN1 PROVE_TAC [REAL_LE_TOTAL, real_lt]) 3357 THEN RW_TAC boolSimps.bool_ss [real_lt] 3358 THEN MP_TAC (Q.SPEC `3` REAL_LE_LMUL) 3359 THEN (KNOW_TAC ``0r < 3 /\ ~(3r = 0)`` 3360 THEN1 (REWRITE_TAC [REAL_LT, REAL_INJ] THEN numLib.ARITH_TAC)) 3361 THEN STRIP_TAC 3362 THEN ASM_REWRITE_TAC [] 3363 THEN DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 3364 THEN ONCE_REWRITE_TAC [REAL_MUL_SYM] 3365 THEN RW_TAC boolSimps.bool_ss [real_div, GSYM REAL_MUL_ASSOC] 3366 THEN RW_TAC boolSimps.bool_ss [REAL_MUL_LINV, REAL_INJ] 3367 THEN RW_TAC boolSimps.bool_ss [REAL_MUL, REAL_LE] 3368 THEN numLib.ARITH_TAC); 3369 3370val REAL_LE_SUB_CANCEL2 = store_thm 3371 ("REAL_LE_SUB_CANCEL2", 3372 ``!x y z : real. x - z <= y - z = x <= y``, 3373 RW_TAC boolSimps.bool_ss [REAL_LE_SUB_RADD, REAL_SUB_ADD]); 3374 3375val REAL_ADD_SUB_ALT = store_thm 3376 ("REAL_ADD_SUB_ALT", 3377 ``!x y : real. (x + y) - y = x``, 3378 RW_TAC boolSimps.bool_ss [REAL_EQ_SUB_RADD]); 3379 3380val INFINITE_REAL_UNIV = store_thm( 3381 "INFINITE_REAL_UNIV", 3382 ``INFINITE univ(:real)``, 3383 REWRITE_TAC [] THEN STRIP_TAC THEN 3384 `FINITE (IMAGE real_of_num univ(:num))` 3385 by METIS_TAC [pred_setTheory.SUBSET_FINITE, 3386 pred_setTheory.SUBSET_UNIV] THEN 3387 FULL_SIMP_TAC (srw_ss()) [pred_setTheory.INJECTIVE_IMAGE_FINITE]); 3388val _ = export_rewrites ["INFINITE_REAL_UNIV"] 3389 3390(* ---------------------------------------------------------------------- 3391 theorems for calculating with the reals; naming scheme taken from 3392 Joe Hurd's development of the positive reals with an infinity 3393 ---------------------------------------------------------------------- *) 3394 3395local open markerTheory in end; (* for unint *) 3396 3397val ui = markerTheory.unint_def 3398 3399val add_rat = store_thm( 3400 "add_rat", 3401 ``x / y + u / v = 3402 if y = 0 then unint (x/y) + u/v 3403 else if v = 0 then x/y + unint (u/v) 3404 else if y = v then (x + u) / v 3405 else (x * v + u * y) / (y * v)``, 3406 SRW_TAC [][ui, REAL_DIV_LZERO, REAL_DIV_ADD] THEN 3407 SRW_TAC [][REAL_ADD_RAT, REAL_MUL_COMM]); 3408 3409val add_ratl = store_thm( 3410 "add_ratl", 3411 ``x / y + z = 3412 if y = 0 then unint(x/y) + z 3413 else (x + z * y) / y``, 3414 SRW_TAC [][ui, REAL_DIV_LZERO] THEN 3415 `z = z/1` by SRW_TAC [][] THEN 3416 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN 3417 SRW_TAC [][REAL_ADD_RAT, REAL_MUL_COMM]); 3418 3419val add_ratr = store_thm( 3420 "add_ratr", 3421 ``x + y / z = 3422 if z = 0 then x + unint (y/z) 3423 else (x * z + y) / z``, 3424 ONCE_REWRITE_TAC [REAL_ADD_COMM] THEN 3425 SRW_TAC [][add_ratl, REAL_DIV_LZERO]); 3426 3427val add_ints = store_thm( 3428 "add_ints", 3429 ``(&n + &m = &(n + m)) /\ 3430 (~&n + &m = if n <= m then &(m - n) else ~&(n - m)) /\ 3431 (&n + ~&m = if n < m then ~&(m - n) else &(n - m)) /\ 3432 (~&n + ~&m = ~&(n + m))``, 3433 `!x y. ~x + y = y + ~x` by SRW_TAC [][REAL_ADD_COMM] THEN 3434 SRW_TAC [][GSYM REAL_NEG_ADD, GSYM real_sub, REAL_SUB] THEN 3435 FULL_SIMP_TAC (srw_ss() ++ old_ARITH_ss) [] THEN 3436 `m = n` by SRW_TAC [old_ARITH_ss][] THEN SRW_TAC [][]) 3437 3438val mult_rat = store_thm( 3439 "mult_rat", 3440 ``(x / y) * (u / v) = 3441 if y = 0 then unint (x/y) * (u/v) 3442 else if v = 0 then (x/y) * unint(u/v) 3443 else (x * u) / (y * v)``, 3444 SRW_TAC [][ui, REAL_DIV_LZERO] THEN 3445 SRW_TAC [][REAL_DIV_LZERO] THEN 3446 MATCH_MP_TAC REAL_EQ_LMUL_IMP THEN 3447 Q.EXISTS_TAC `y * v` THEN ASM_REWRITE_TAC [REAL_MUL_ASSOC, REAL_ENTIRE] THEN 3448 SRW_TAC [][REAL_DIV_LMUL, REAL_ENTIRE] THEN 3449 `y * v * (x / y) * (u / v) = (y * (x / y)) * (v * (u / v))` 3450 by CONV_TAC (AC_CONV (REAL_MUL_ASSOC, REAL_MUL_COMM)) THEN 3451 POP_ASSUM SUBST_ALL_TAC THEN 3452 SRW_TAC [][REAL_DIV_LMUL]); 3453 3454val mult_ratl = store_thm( 3455 "mult_ratl", 3456 ``(x / y) * z = if y = 0 then unint (x/y) * z else (x * z) / y``, 3457 SRW_TAC [][ui] THEN 3458 SRW_TAC [][REAL_DIV_LZERO] THEN 3459 `z = z / 1` by SRW_TAC [][] THEN 3460 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th]))) THEN 3461 REWRITE_TAC [mult_rat] THEN SRW_TAC [][]); 3462 3463val mult_ratr = store_thm( 3464 "mult_ratr", 3465 ``x * (y/z) = if z = 0 then x * unint (y/z) else (x * y) / z``, 3466 CONV_TAC (LAND_CONV (REWR_CONV REAL_MUL_COMM)) THEN 3467 SRW_TAC [][mult_ratl] THEN SRW_TAC [][ui, REAL_MUL_COMM]); 3468 3469val mult_ints = store_thm( 3470 "mult_ints", 3471 ``(&a * &b = &(a * b)) /\ 3472 (~&a * &b = ~&(a * b)) /\ 3473 (&a * ~&b = ~&(a * b)) /\ 3474 (~&a * ~&b = &(a * b))``, 3475 SRW_TAC [][REAL_MUL_LNEG, REAL_MUL_RNEG]); 3476 3477val pow_rat = store_thm( 3478 "pow_rat", 3479 ``(x pow 0 = 1) /\ 3480 (0 pow (NUMERAL (BIT1 n)) = 0) /\ 3481 (0 pow (NUMERAL (BIT2 n)) = 0) /\ 3482 (&(NUMERAL a) pow (NUMERAL n) = &(NUMERAL a EXP NUMERAL n)) /\ 3483 (~&(NUMERAL a) pow (NUMERAL n) = 3484 (if ODD (NUMERAL n) then (~) else (\x.x)) 3485 (&(NUMERAL a EXP NUMERAL n))) /\ 3486 ((x / y) pow n = (x pow n) / (y pow n))``, 3487 SIMP_TAC bool_ss [pow, NUMERAL_DEF, BIT1, BIT2, POW_ADD, 3488 ALT_ZERO, ADD_CLAUSES, REAL_MUL, MULT_CLAUSES, 3489 REAL_MUL_RZERO, REAL_OF_NUM_POW, REAL_POW_DIV, EXP] THEN 3490 Induct_on `n` THEN ASM_SIMP_TAC bool_ss [pow, ODD, EXP] THEN 3491 Cases_on `ODD n` THEN 3492 ASM_SIMP_TAC bool_ss [REAL_MUL, REAL_MUL_LNEG, 3493 REAL_MUL_RNEG, REAL_NEG_NEG]); 3494 3495val neg_rat = store_thm( 3496 "neg_rat", 3497 ``(~(x / y) = if y = 0 then ~ (unint(x/y)) else ~x / y) /\ 3498 (x / ~y = if y = 0 then unint(x/y) else ~x/y)``, 3499 SRW_TAC [][ui] THEN 3500 SRW_TAC [][real_div, GSYM REAL_NEG_INV, REAL_MUL_LNEG, REAL_MUL_RNEG]); 3501 3502val eq_rat = store_thm( 3503 "eq_rat", 3504 ``(x / y = u / v) = if y = 0 then unint (x/y) = u / v 3505 else if v = 0 then x / y = unint (u/v) 3506 else if y = v then x = u 3507 else x * v = y * u``, 3508 SRW_TAC [][ui] THENL [ 3509 METIS_TAC [REAL_DIV_LMUL, REAL_EQ_LMUL], 3510 `~(y * v = 0)` by SRW_TAC [][REAL_ENTIRE] THEN 3511 `(x/y = u/v) = ((y * v) * (x/y) = (y * v) * (u/v))` 3512 by METIS_TAC [REAL_EQ_LMUL2] THEN 3513 POP_ASSUM SUBST_ALL_TAC THEN 3514 `((y * v) * (x/y) = v * (y * (x/y))) /\ 3515 ((y * v) * (u/v) = y * (v * (u/v)))` 3516 by (CONJ_TAC THEN 3517 CONV_TAC (AC_CONV(REAL_MUL_ASSOC, REAL_MUL_COMM))) THEN 3518 ASM_REWRITE_TAC [] THEN SRW_TAC [][REAL_DIV_LMUL] THEN 3519 SRW_TAC [][REAL_MUL_COMM] 3520 ]); 3521 3522val eq_ratl = store_thm( 3523 "eq_ratl", 3524 ``(x/y = z) = if y = 0 then unint(x/y) = z else x = y * z``, 3525 SRW_TAC [][ui] THEN METIS_TAC [REAL_DIV_LMUL, REAL_EQ_LMUL]); 3526 3527val eq_ratr = store_thm( 3528 "eq_ratr", 3529 ``(z = x/y) = if y = 0 then z = unint(x/y) else y * z = x``, 3530 METIS_TAC [eq_ratl]); 3531 3532val eq_ints = store_thm( 3533 "eq_ints", 3534 ``((&n = &m) = (n = m)) /\ 3535 ((~&n = &m) = (n = 0) /\ (m = 0)) /\ 3536 ((&n = ~&m) = (n = 0) /\ (m = 0)) /\ 3537 ((~&n = ~&m) = (n = m))``, 3538 REWRITE_TAC [REAL_INJ, REAL_EQ_NEG] THEN 3539 Q_TAC SUFF_TAC `!n m. (&n = ~&m) = (n = 0) /\ (m = 0)` THEN1 3540 METIS_TAC [] THEN 3541 REPEAT GEN_TAC THEN EQ_TAC THENL [ 3542 STRIP_TAC THEN 3543 `&n <= ~&m` by METIS_TAC [REAL_LE_ANTISYM] THEN 3544 `0 <= ~&m` by METIS_TAC [REAL_LE_TRANS, REAL_LE, 3545 arithmeticTheory.ZERO_LESS_EQ] THEN 3546 `m <= 0` by METIS_TAC [REAL_LE, REAL_NEG_GE0] THEN 3547 `m = 0` by SRW_TAC [old_ARITH_ss][] THEN 3548 FULL_SIMP_TAC (srw_ss()) [], 3549 SRW_TAC [][] 3550 ]); 3551 3552val REALMUL_AC = CONV_TAC (AC_CONV (REAL_MUL_ASSOC, REAL_MUL_COMM)) 3553 3554val div_ratr = store_thm( 3555 "div_ratr", 3556 ``x / (y / z) = if (y = 0) \/ (z = 0) then x / unint(y/z) 3557 else x * z / y``, 3558 SRW_TAC [][ui] THEN 3559 FULL_SIMP_TAC (srw_ss()) [] THEN 3560 SRW_TAC [][real_div, REAL_INV_MUL, REAL_INV_EQ_0, REAL_INV_INV] THEN 3561 REALMUL_AC); 3562 3563val div_ratl = store_thm( 3564 "div_ratl", 3565 ``(x/y) / z = if y = 0 then unint(x/y) / z 3566 else if z = 0 then unint((x/y)/ z) 3567 else x / (y * z)``, 3568 SRW_TAC [][ui, real_div, REAL_INV_MUL, REAL_INV_EQ_0, REAL_INV_INV] THEN 3569 REALMUL_AC); 3570 3571 3572 3573val div_rat = store_thm( 3574 "div_rat", 3575 ``(x/y) / (u/v) = 3576 if (u = 0) \/ (v = 0) then (x/y) / unint (u/v) 3577 else if y = 0 then unint(x/y) / (u/v) 3578 else (x * v) / (y * u)``, 3579 SRW_TAC [][ui] THEN 3580 FULL_SIMP_TAC (srw_ss()) [] THEN 3581 SRW_TAC [][real_div, REAL_INV_MUL, REAL_INV_EQ_0, REAL_INV_INV] THEN 3582 REALMUL_AC); 3583 3584val le_rat = store_thm( 3585 "le_rat", 3586 ``x / &n <= u / &m = if n = 0 then unint(x/0) <= u / &m 3587 else if m = 0 then x/ &n <= unint(u/0) 3588 else &m * x <= &n * u``, 3589 SRW_TAC [][ui] THEN 3590 `0 < m /\ 0 < n` by SRW_TAC [old_ARITH_ss][] THEN 3591 `0 < &m * &n` by SRW_TAC [][REAL_LT_MUL] THEN 3592 POP_ASSUM (ASSUME_TAC o MATCH_MP REAL_LE_LMUL) THEN 3593 POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [GSYM th]))) THEN 3594 `&m * &n * (x / &n) = &m * (&n * (x/ &n))` by REALMUL_AC THEN 3595 `&m * &n * (u / &m) = &n * (&m * (u / &m))` by REALMUL_AC THEN 3596 SRW_TAC [][REAL_DIV_LMUL]); 3597 3598val le_ratl = save_thm( 3599 "le_ratl", 3600 SIMP_RULE (srw_ss()) [] (Thm.INST [``m:num`` |-> ``1n``] le_rat)); 3601 3602val le_ratr = save_thm( 3603 "le_ratr", 3604 SIMP_RULE (srw_ss()) [] (Thm.INST [``n:num`` |-> ``1n``] le_rat)); 3605 3606val le_int = store_thm( 3607 "le_int", 3608 ``(&n <= &m = n <= m) /\ 3609 (~&n <= &m = T) /\ 3610 (&n <= ~&m = (n = 0) /\ (m = 0)) /\ 3611 (~&n <= ~&m = m <= n)``, 3612 SRW_TAC [][REAL_LE_NEG] THENL [ 3613 MATCH_MP_TAC REAL_LE_TRANS THEN 3614 Q.EXISTS_TAC `0` THEN SRW_TAC [][REAL_NEG_LE0], 3615 Cases_on `m` THEN SRW_TAC [][REAL_NEG_LE0] THEN 3616 SRW_TAC [][REAL_NOT_LE] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN 3617 Q.EXISTS_TAC `0` THEN SRW_TAC [][REAL_NEG_LT0] 3618 ]); 3619 3620val lt_rat = store_thm( 3621 "lt_rat", 3622 ``x / &n < u / &m = if n = 0 then unint(x/0) < u / &m 3623 else if m = 0 then x / & n < unint(u/0) 3624 else &m * x < &n * u``, 3625 SRW_TAC [][ui] THEN 3626 `0 < m /\ 0 < n` by SRW_TAC [old_ARITH_ss][] THEN 3627 `0 < &m * &n` by SRW_TAC [][REAL_LT_MUL] THEN 3628 POP_ASSUM (ASSUME_TAC o MATCH_MP REAL_LT_LMUL) THEN 3629 POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [GSYM th]))) THEN 3630 `&m * &n * (x / &n) = &m * (&n * (x / &n))` by REALMUL_AC THEN 3631 `&m * &n * (u / &m) = &n * (&m * (u / &m))` by REALMUL_AC THEN 3632 SRW_TAC [][REAL_DIV_LMUL]); 3633 3634val lt_ratl = save_thm( 3635 "lt_ratl", 3636 SIMP_RULE (srw_ss()) [] (Thm.INST [``m:num`` |-> ``1n``] lt_rat)); 3637 3638val lt_ratr = save_thm( 3639 "lt_ratr", 3640 SIMP_RULE (srw_ss()) [] (Thm.INST [``n:num`` |-> ``1n``] lt_rat)); 3641 3642val lt_int = store_thm( 3643 "lt_int", 3644 ``(&n < &m = n < m) /\ 3645 (~&n < &m = ~(n = 0) \/ ~(m = 0)) /\ 3646 (&n < ~&m = F) /\ 3647 (~&n < ~&m = m < n)``, 3648 SRW_TAC [][REAL_LT_NEG] THENL [ 3649 Cases_on `m` THEN SRW_TAC [old_ARITH_ss][REAL_NEG_LT0] THEN 3650 MATCH_MP_TAC REAL_LET_TRANS THEN Q.EXISTS_TAC `0` THEN 3651 SRW_TAC [old_ARITH_ss][REAL_NEG_LE0], 3652 SRW_TAC [][REAL_NOT_LT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN 3653 Q.EXISTS_TAC `0` THEN SRW_TAC [][REAL_NEG_LE0] 3654 ]); 3655 3656 3657(*---------------------------------------------------------------------------*) 3658(* Floor and ceiling (nums) *) 3659(*---------------------------------------------------------------------------*) 3660 3661val NUM_FLOOR_def = zDefine` 3662 NUM_FLOOR (x:real) = LEAST (n:num). real_of_num (n+1) > x`; 3663 3664val NUM_CEILING_def = zDefine` 3665 NUM_CEILING (x:real) = LEAST (n:num). x <= real_of_num n`; 3666 3667val _ = overload_on ("flr",``NUM_FLOOR``); 3668val _ = overload_on ("clg",``NUM_CEILING``); 3669 3670val lem = SIMP_RULE arith_ss [REAL_POS,REAL_ADD_RID] 3671 (Q.SPECL[`y`,`&n`,`0r`,`1r`] REAL_LTE_ADD2); 3672 3673val add1_gt_exists = prove( 3674 ``!y : real. ?n. & (n + 1) > y``, 3675 GEN_TAC THEN Q.SPEC_THEN `1` MP_TAC REAL_ARCH THEN 3676 SIMP_TAC (srw_ss()) [] THEN 3677 DISCH_THEN (Q.SPEC_THEN `y` STRIP_ASSUME_TAC) THEN 3678 Q.EXISTS_TAC `n` THEN 3679 SIMP_TAC arith_ss [GSYM REAL_ADD,real_gt,REAL_LT_ADDL,REAL_LT_ADDR] THEN 3680 METIS_TAC [lem]); 3681 3682val lt_add1_exists = prove( 3683 ``!y: real. ?n. y < &(n + 1)``, 3684 GEN_TAC THEN Q.SPEC_THEN `1` MP_TAC REAL_ARCH THEN 3685 SIMP_TAC (srw_ss()) [] THEN 3686 DISCH_THEN (Q.SPEC_THEN `y` STRIP_ASSUME_TAC) THEN 3687 Q.EXISTS_TAC `n` THEN 3688 SIMP_TAC bool_ss [GSYM REAL_ADD] THEN METIS_TAC [lem]); 3689 3690val NUM_FLOOR_LE = store_thm 3691("NUM_FLOOR_LE", 3692 ``0 <= x ==> &(NUM_FLOOR x) <= x``, 3693 SRW_TAC [][NUM_FLOOR_def] THEN 3694 LEAST_ELIM_TAC THEN 3695 SRW_TAC [][add1_gt_exists] THEN 3696 Cases_on `n` THEN SRW_TAC [][] THEN 3697 FIRST_X_ASSUM (Q.SPEC_THEN `n'` MP_TAC) THEN 3698 SRW_TAC [old_ARITH_ss] [real_gt, REAL_NOT_LT, ADD1]); 3699 3700val NUM_FLOOR_LE2 = store_thm 3701("NUM_FLOOR_LE2", 3702 ``0 <= y ==> (x <= NUM_FLOOR y = &x <= y)``, 3703 SRW_TAC [][NUM_FLOOR_def] THEN LEAST_ELIM_TAC THEN 3704 SRW_TAC [][lt_add1_exists, real_gt,REAL_NOT_LT, EQ_IMP_THM] 3705 THENL [ 3706 Cases_on `n` THENL [ 3707 FULL_SIMP_TAC (srw_ss()) [], 3708 FIRST_X_ASSUM (Q.SPEC_THEN `n'` MP_TAC) THEN 3709 FULL_SIMP_TAC (bool_ss ++ old_ARITH_ss) 3710 [ADD1, GSYM REAL_ADD, GSYM REAL_LE] THEN 3711 METIS_TAC [REAL_LE_TRANS] 3712 ], 3713 `&x < &(n + 1):real` by PROVE_TAC [REAL_LET_TRANS] THEN 3714 FULL_SIMP_TAC (srw_ss() ++ old_ARITH_ss) [] 3715 ]); 3716 3717val NUM_FLOOR_LET = store_thm 3718("NUM_FLOOR_LET", 3719 ``(NUM_FLOOR x <= y) = (x < &y + 1)``, 3720 SRW_TAC [][NUM_FLOOR_def] THEN LEAST_ELIM_TAC THEN 3721 SRW_TAC [][lt_add1_exists, real_gt,REAL_NOT_LT, EQ_IMP_THM] 3722 THENL [ 3723 FULL_SIMP_TAC bool_ss [GSYM REAL_LE,GSYM REAL_ADD] THEN 3724 MATCH_MP_TAC REAL_LTE_TRANS THEN 3725 Q.EXISTS_TAC `&n + 1` THEN SRW_TAC [][], 3726 Cases_on `n` THEN SRW_TAC [][] THEN 3727 FIRST_X_ASSUM (Q.SPEC_THEN `n'` MP_TAC) THEN 3728 FULL_SIMP_TAC (bool_ss ++ old_ARITH_ss) [ADD1] THEN 3729 STRIP_TAC THEN 3730 `&(n' + 1) < &(y + 1):real` by METIS_TAC [REAL_LET_TRANS] THEN 3731 FULL_SIMP_TAC (srw_ss() ++ old_ARITH_ss) [] 3732 ]); 3733 3734val NUM_FLOOR_DIV = store_thm 3735("NUM_FLOOR_DIV", 3736 ``0 <= x /\ 0 < y ==> &(NUM_FLOOR (x / y)) * y <= x``, 3737 SRW_TAC [][NUM_FLOOR_def] THEN LEAST_ELIM_TAC THEN 3738 SRW_TAC [][add1_gt_exists] THEN 3739 Cases_on `n` THEN1 SRW_TAC [][] THEN 3740 FIRST_X_ASSUM (Q.SPEC_THEN `n'` MP_TAC) THEN 3741 SRW_TAC [old_ARITH_ss] [real_gt,REAL_NOT_LT,ADD1,REAL_LE_RDIV_EQ]); 3742 3743val NUM_FLOOR_DIV_LOWERBOUND = store_thm 3744("NUM_FLOOR_DIV_LOWERBOUND", 3745 ``0 <= x:real /\ 0 < y:real ==> x < &(NUM_FLOOR (x/y) + 1) * y ``, 3746 SRW_TAC [][NUM_FLOOR_def] THEN LEAST_ELIM_TAC THEN 3747 SRW_TAC [][add1_gt_exists] THEN Cases_on `n` THEN 3748 POP_ASSUM MP_TAC THEN SRW_TAC [][real_gt, REAL_LT_LDIV_EQ]); 3749 3750val NUM_FLOOR_BASE = Q.store_thm("NUM_FLOOR_BASE", 3751 `!r. r < 1 ==> (NUM_FLOOR r = 0)`, 3752 SRW_TAC [] [NUM_FLOOR_def] 3753 THEN numLib.LEAST_ELIM_TAC 3754 THEN SRW_TAC [] [] 3755 THEN1 (Q.EXISTS_TAC `0` THEN ASM_SIMP_TAC std_ss [real_gt]) 3756 THEN Cases_on `n = 0` 3757 THEN1 ASM_REWRITE_TAC [] 3758 THEN `0 < n` by DECIDE_TAC 3759 THEN RES_TAC 3760 THEN FULL_SIMP_TAC arith_ss [real_gt] 3761 ) 3762 3763val lem = 3764 metisLib.METIS_PROVE [REAL_LT_01, REAL_LET_TRANS] 3765 ``!r: real. r <= 0 ==> r < 1`` 3766 3767val NUM_FLOOR_NEG = Q.prove( 3768 `NUM_FLOOR (~real_of_num n) = 0`, 3769 MATCH_MP_TAC NUM_FLOOR_BASE 3770 THEN MATCH_MP_TAC lem 3771 THEN REWRITE_TAC [REAL_NEG_LE0, REAL_POS]) 3772 3773val NUM_FLOOR_NEGQ = Q.prove( 3774 `0 < m ==> (NUM_FLOOR (~real_of_num n / real_of_num m) = 0)`, 3775 ONCE_REWRITE_TAC [GSYM REAL_LT] 3776 THEN STRIP_TAC 3777 THEN MATCH_MP_TAC NUM_FLOOR_BASE 3778 THEN ASM_SIMP_TAC std_ss [REAL_LT_LDIV_EQ, REAL_MUL_LID, lt_int] 3779 THEN FULL_SIMP_TAC arith_ss [REAL_LT] 3780 ) 3781 3782val NUM_FLOOR_EQNS = store_thm( 3783 "NUM_FLOOR_EQNS", 3784 ``(NUM_FLOOR (real_of_num n) = n) /\ 3785 (NUM_FLOOR (~real_of_num n) = 0) /\ 3786 (0 < m ==> (NUM_FLOOR (real_of_num n / real_of_num m) = n DIV m)) /\ 3787 (0 < m ==> (NUM_FLOOR (~real_of_num n / real_of_num m) = 0))``, 3788 REWRITE_TAC [NUM_FLOOR_NEG, NUM_FLOOR_NEGQ] 3789 THEN SRW_TAC [][NUM_FLOOR_def] THEN LEAST_ELIM_TAC THENL [ 3790 SIMP_TAC (srw_ss()) [real_gt, REAL_LT] THEN 3791 CONJ_TAC THENL 3792 [Q.EXISTS_TAC `n` THEN RW_TAC old_arith_ss [], 3793 Cases THEN FULL_SIMP_TAC old_arith_ss [] 3794 THEN STRIP_TAC 3795 THEN Q.PAT_X_ASSUM `$! M` (MP_TAC o Q.SPEC `n''`) 3796 THEN RW_TAC old_arith_ss []], 3797 ASM_SIMP_TAC (srw_ss()) [real_gt, REAL_LT_LDIV_EQ] THEN 3798 CONJ_TAC THENL [ 3799 Q.EXISTS_TAC `n` THEN 3800 SRW_TAC [][RIGHT_ADD_DISTRIB] THEN 3801 MATCH_MP_TAC LESS_EQ_LESS_TRANS THEN 3802 Q.EXISTS_TAC `n * m` THEN 3803 SRW_TAC [old_ARITH_ss][] THEN 3804 CONV_TAC (LAND_CONV (REWR_CONV (GSYM MULT_RIGHT_1))) THEN 3805 SRW_TAC [old_ARITH_ss][], 3806 Q.HO_MATCH_ABBREV_TAC 3807 `!p:num. (!i. i < p ==> ~(n < (i + 1) * m)) /\ n < (p + 1) * m 3808 ==> (p = n DIV m)` THEN 3809 REPEAT STRIP_TAC THEN 3810 CONV_TAC (REWR_CONV EQ_SYM_EQ) THEN 3811 MATCH_MP_TAC DIV_UNIQUE THEN 3812 `(p = 0) \/ (?p0. p = SUC p0)` 3813 by PROVE_TAC [arithmeticTheory.num_CASES] THEN 3814 FULL_SIMP_TAC (srw_ss() ++ old_ARITH_ss) 3815 [ADD1,RIGHT_ADD_DISTRIB] THEN 3816 FIRST_X_ASSUM (Q.SPEC_THEN `p0` MP_TAC) THEN 3817 SRW_TAC [old_ARITH_ss][NOT_LESS] THEN 3818 Q.EXISTS_TAC `n - (m + p0 * m)` THEN 3819 SRW_TAC [old_ARITH_ss][] 3820 ] 3821 ]); 3822 3823val NUM_FLOOR_LOWER_BOUND = store_thm( 3824 "NUM_FLOOR_LOWER_BOUND", 3825 ``(x:real < &n) = (NUM_FLOOR(x+1) <= n)``, 3826 MP_TAC (Q.INST [`x` |-> `x + 1`, `y` |-> `n`] NUM_FLOOR_LET) THEN 3827 SIMP_TAC (srw_ss()) []); 3828 3829val NUM_FLOOR_UPPER_BOUND = store_thm( 3830 "NUM_FLOOR_upper_bound", 3831 ``(&n <= x:real) = (n < NUM_FLOOR(x + 1))``, 3832 MP_TAC (AP_TERM negation NUM_FLOOR_LOWER_BOUND) THEN 3833 PURE_REWRITE_TAC [REAL_NOT_LT, NOT_LESS_EQUAL,IMP_CLAUSES]); 3834 3835val NUM_CEILING_NUM_FLOOR = Q.store_thm("NUM_CEILING_NUM_FLOOR", 3836 `!r. NUM_CEILING r = 3837 let n = NUM_FLOOR r in 3838 if r <= 0 \/ (r = real_of_num n) then n else n + 1`, 3839 SRW_TAC [boolSimps.LET_ss] [NUM_CEILING_def, NUM_FLOOR_BASE] 3840 THEN1 (IMP_RES_TAC lem 3841 THEN ASM_SIMP_TAC std_ss [NUM_FLOOR_BASE] 3842 THEN numLib.LEAST_ELIM_TAC 3843 THEN CONJ_TAC 3844 THEN1 METIS_TAC [] 3845 THEN SRW_TAC [] [] 3846 THEN FULL_SIMP_TAC std_ss [REAL_NOT_LE] 3847 THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC 3848 THEN `0 < n` by DECIDE_TAC 3849 THEN METIS_TAC [REAL_LTE_ANTSYM]) 3850 THEN1 (POP_ASSUM (fn th => CONV_TAC (LHS_CONV (ONCE_REWRITE_CONV [th]))) 3851 THEN SRW_TAC [] [NUM_FLOOR_LET, NUM_FLOOR_def, real_gt]) 3852 THEN FULL_SIMP_TAC std_ss [REAL_NOT_LE] 3853 THEN numLib.LEAST_ELIM_TAC 3854 THEN CONJ_TAC 3855 THEN1 (Q.EXISTS_TAC `flr r + 1` 3856 THEN Cases_on `r < 1` 3857 THEN1 SRW_TAC [] [NUM_FLOOR_BASE, REAL_LT_IMP_LE] 3858 THEN `0 <= r` by METIS_TAC [REAL_NOT_LT, REAL_LE_01, REAL_LE_TRANS] 3859 THEN METIS_TAC 3860 [NUM_FLOOR_DIV_LOWERBOUND 3861 |> Q.INST [`y` |-> `1r`] 3862 |> SIMP_RULE (srw_ss()) [], 3863 REAL_LT_IMP_LE]) 3864 THEN SRW_TAC [] [] 3865 THEN Q.PAT_X_ASSUM `x <> y` MP_TAC 3866 THEN SIMP_TAC std_ss [NUM_FLOOR_def] 3867 THEN numLib.LEAST_ELIM_TAC 3868 THEN CONJ_TAC 3869 THEN1 (Q.EXISTS_TAC `n` 3870 THEN ASM_SIMP_TAC std_ss [real_gt, GSYM REAL_ADD, REAL_LT_ADD1]) 3871 THEN SRW_TAC [] [real_gt] 3872 THEN FULL_SIMP_TAC std_ss [REAL_NOT_LE, REAL_NOT_LT] 3873 THEN Cases_on `n' + 1 < n` 3874 THEN1 METIS_TAC [REAL_LT_ANTISYM] 3875 THEN Cases_on `n' + 1 = n` 3876 THEN1 ASM_REWRITE_TAC [] 3877 THEN `n < n' + 1` by DECIDE_TAC 3878 THEN Cases_on `n = 0` 3879 THEN FULL_SIMP_TAC std_ss [] 3880 THEN1 METIS_TAC [REAL_LET_ANTISYM] 3881 THEN `n - 1 < n'` by DECIDE_TAC 3882 THEN RES_TAC 3883 THEN FULL_SIMP_TAC arith_ss [] 3884 THEN REV_FULL_SIMP_TAC std_ss [DECIDE ``n <> 0n ==> (n - 1 + 1 = n)``] 3885 THEN IMP_RES_TAC REAL_LE_ANTISYM 3886 THEN FULL_SIMP_TAC (srw_ss()) [] 3887 THEN `n' - 1 < n'` by DECIDE_TAC 3888 THEN RES_TAC 3889 THEN FULL_SIMP_TAC arith_ss [] 3890 ) 3891 3892(*---------------------------------------------------------------------------*) 3893(* Ceiling function *) 3894(*---------------------------------------------------------------------------*) 3895 3896val LE_NUM_CEILING = store_thm 3897("LE_NUM_CEILING", 3898 ``!x. x <= &(clg x)``, 3899 RW_TAC std_ss [NUM_CEILING_def] 3900 THEN numLib.LEAST_ELIM_TAC 3901 THEN Q.SPEC_THEN `1` MP_TAC REAL_ARCH 3902 THEN SIMP_TAC (srw_ss()) [] 3903 THEN METIS_TAC [REAL_LT_IMP_LE]); 3904 3905val NUM_CEILING_LE = store_thm 3906("NUM_CEILING_LE", 3907 ``!x n. x <= &n ==> clg(x) <= n``, 3908 RW_TAC std_ss [NUM_CEILING_def] 3909 THEN numLib.LEAST_ELIM_TAC 3910 THEN METIS_TAC [NOT_LESS_EQUAL]); 3911 3912val _ = export_theory(); 3913