1(*===========================================================================*) 2(* Construct reals from positive reals *) 3(*===========================================================================*) 4 5(* 6app load ["hol88Lib", 7 "numLib", 8 "reduceLib", 9 "pairTheory", 10 "arithmeticTheory", 11 "quotient", 12 "jrhUtils", 13 "hratTheory", 14 "hrealTheory"]; 15*) 16 17open HolKernel Parse boolLib hol88Lib numLib reduceLib pairLib 18 pairTheory arithmeticTheory numTheory prim_recTheory 19 jrhUtils hratTheory hrealTheory; 20 21infix THEN THENL ORELSE ORELSEC ##; 22 23val _ = new_theory "realax"; 24 25(*---------------------------------------------------------------------------*) 26(* Required lemmas about the halfreals - mostly to drive CANCEL_TAC *) 27(*---------------------------------------------------------------------------*) 28 29val HREAL_RDISTRIB = store_thm("HREAL_RDISTRIB", 30 ���!x y z. (x hreal_add y) hreal_mul z = 31 (x hreal_mul z) hreal_add (y hreal_mul z)���, 32 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN 33 MATCH_ACCEPT_TAC HREAL_LDISTRIB); 34 35val HREAL_EQ_ADDR = store_thm("HREAL_EQ_ADDR", 36 ���!x y. ~(x hreal_add y = x)���, 37 REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC HREAL_NOZERO); 38 39val HREAL_EQ_ADDL = store_thm("HREAL_EQ_ADDL", 40 ���!x y. ~(x = x hreal_add y)���, 41 REPEAT GEN_TAC THEN CONV_TAC(RAND_CONV SYM_CONV) THEN 42 MATCH_ACCEPT_TAC HREAL_EQ_ADDR); 43 44val HREAL_EQ_LADD = store_thm("HREAL_EQ_LADD", 45 ���!x y z. (x hreal_add y = x hreal_add z) = (y = z)���, 46 REPEAT GEN_TAC THEN EQ_TAC THENL 47 [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 48 (SPECL [���y:hreal���, ���z:hreal���] HREAL_ADD_TOTAL) THENL 49 [DISCH_THEN(K ALL_TAC) THEN POP_ASSUM ACCEPT_TAC, ALL_TAC, ALL_TAC] THEN 50 POP_ASSUM(X_CHOOSE_THEN ���d:hreal��� SUBST1_TAC) THEN 51 REWRITE_TAC[HREAL_ADD_ASSOC, HREAL_EQ_ADDR, HREAL_EQ_ADDL], 52 DISCH_THEN SUBST1_TAC THEN REFL_TAC]); 53 54val HREAL_LT_REFL = store_thm("HREAL_LT_REFL", 55 ���!x. ~(x hreal_lt x)���, 56 GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN 57 REWRITE_TAC[HREAL_EQ_ADDL]); 58 59val HREAL_LT_ADDL = store_thm("HREAL_LT_ADDL", 60 ���!x y. x hreal_lt (x hreal_add y)���, 61 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN 62 EXISTS_TAC ���y:hreal��� THEN REFL_TAC); 63 64val HREAL_LT_NE = store_thm("HREAL_LT_NE", 65 ���!x y. x hreal_lt y ==> ~(x = y)���, 66 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN 67 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN 68 MATCH_ACCEPT_TAC HREAL_EQ_ADDL); 69 70val HREAL_LT_ADDR = store_thm("HREAL_LT_ADDR", 71 ���!x y. ~((x hreal_add y) hreal_lt x)���, 72 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN 73 REWRITE_TAC[GSYM HREAL_ADD_ASSOC, HREAL_EQ_ADDL]); 74 75val HREAL_LT_GT = store_thm("HREAL_LT_GT", 76 ���!x y. x hreal_lt y ==> ~(y hreal_lt x)���, 77 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN 78 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN 79 REWRITE_TAC[GSYM HREAL_ADD_ASSOC, HREAL_EQ_ADDL]); 80 81val HREAL_LT_ADD2 = store_thm("HREAL_LT_ADD2", 82 ���!x1 x2 y1 y2. x1 hreal_lt y1 /\ x2 hreal_lt y2 ==> 83 (x1 hreal_add x2) hreal_lt (y1 hreal_add y2)���, 84 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN 85 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN ���d1:hreal��� SUBST1_TAC) 86 (X_CHOOSE_THEN ���d2:hreal��� SUBST1_TAC)) THEN 87 EXISTS_TAC ���d1 hreal_add d2��� THEN 88 CONV_TAC(AC_CONV(HREAL_ADD_ASSOC,HREAL_ADD_SYM))); 89 90val HREAL_LT_LADD = store_thm("HREAL_LT_LADD", 91 ���!x y z. (x hreal_add y) hreal_lt (x hreal_add z) = y hreal_lt z���, 92 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN EQ_TAC THEN 93 DISCH_THEN(X_CHOOSE_THEN ���d:hreal��� (curry op THEN (EXISTS_TAC ���d:hreal���) o MP_TAC)) 94 THEN REWRITE_TAC[GSYM HREAL_ADD_ASSOC, HREAL_EQ_LADD]); 95 96(*---------------------------------------------------------------------------*) 97(* CANCEL_CONV - Try to cancel, rearranging using AC laws as needed *) 98(* *) 99(* The first two arguments are the associative and commutative laws, as *) 100(* given to AC_CONV. The remaining list of theorems should be of the form: *) 101(* *) 102(* |- (a & b ~ a & c) = w (e.g. b ~ c) *) 103(* |- (a & b ~ a) = x (e.g. F) *) 104(* |- (a ~ a & c) = y (e.g. T) *) 105(* |- (a ~ a) = z (e.g. F) *) 106(* *) 107(* For some operator (written as infix &) and relation (~). *) 108(* *) 109(* Theorems may be of the form |- ~ P or |- P, rather that equations; they *) 110(* will be transformed to |- P = F and |- P = T automatically if needed. *) 111(* *) 112(* Note that terms not cancelled will remain in their original order, but *) 113(* will be flattened to right-associated form. *) 114(*---------------------------------------------------------------------------*) 115 116fun intro th = 117 if is_eq(concl th) then th else 118 if is_neg(concl th) then EQF_INTRO th 119 else EQT_INTRO th; 120 121val lhs_rator2 = rator o rator o lhs o snd o strip_forall o concl; 122 123fun rmel i list = 124 case list of 125 [] => [] 126 | h::t => if aconv h i then t else h :: rmel i t 127 128fun ERR s = HOL_ERR{origin_structure = "realaxScript", 129 origin_function = "CANCEL_CONV", message = s}; 130 131fun CANCEL_CONV(assoc,sym,lcancelthms) tm = 132 let val lcthms = map (intro o SPEC_ALL) lcancelthms 133 val eqop = lhs_rator2 (Lib.trye hd lcthms) 134 val binop = lhs_rator2 sym 135 fun strip_binop tm = 136 if (rator(rator tm) = binop handle HOL_ERR _ => false) 137 then strip_binop (rand(rator tm)) @ strip_binop(rand tm) 138 else [tm] 139 val mk_binop = curry mk_comb o curry mk_comb binop 140 val list_mk_binop = end_itlist mk_binop 141 val (c,alist) = strip_comb tm 142 val _ = assert (curry op = eqop) c 143 in 144 case alist of 145 [l1,r1] => let 146 val l = strip_binop l1 147 and r = strip_binop r1 148 val i = op_intersect aconv l r 149 in 150 if (i = []) then raise ERR "unchanged" 151 else let 152 val itm = list_mk_binop i 153 val l' = end_itlist (C (curry op o)) (map rmel i) l 154 and r' = end_itlist (C (curry op o)) (map rmel i) r 155 fun mk ts = mk_binop itm (list_mk_binop ts) 156 handle HOL_ERR _ => itm 157 val l2 = mk l' 158 val r2 = mk r' 159 val le = (EQT_ELIM o AC_CONV(assoc,sym) o mk_eq) (l1,l2) 160 val re = (EQT_ELIM o AC_CONV(assoc,sym) o mk_eq) (r1,r2) 161 val eqv = MK_COMB(AP_TERM eqop le,re) 162 in 163 CONV_RULE(RAND_CONV 164 (end_itlist (curry op ORELSEC) (map REWR_CONV lcthms))) 165 eqv 166 end 167 end 168 | _ => raise ERR "" 169 end 170 171(*---------------------------------------------------------------------------*) 172(* Tactic to do all the obvious simplifications via cancellation etc. *) 173(*---------------------------------------------------------------------------*) 174fun mk_rewrites th = 175 let val th = Drule.SPEC_ALL th 176 val t = Thm.concl th 177 in 178 if is_eq t 179 then [th] 180 else if is_conj t 181 then (op @ o (mk_rewrites##mk_rewrites) o Drule.CONJ_PAIR) th 182 else if is_neg t 183 then [Drule.EQF_INTRO th] 184 else [Drule.EQT_INTRO th] 185 end; 186 187val CANCEL_TAC = (C (curry op THEN) 188 (PURE_REWRITE_TAC 189 (itlist (append o mk_rewrites) 190 [REFL_CLAUSE, EQ_CLAUSES, NOT_CLAUSES, 191 AND_CLAUSES, OR_CLAUSES, IMP_CLAUSES, 192 COND_CLAUSES, FORALL_SIMP, EXISTS_SIMP, 193 ABS_SIMP] [])) 194 o CONV_TAC o ONCE_DEPTH_CONV o end_itlist (curry op ORELSEC)) 195 (map CANCEL_CONV 196 [(HREAL_ADD_ASSOC,HREAL_ADD_SYM, 197 [HREAL_EQ_LADD, HREAL_EQ_ADDL, HREAL_EQ_ADDR, EQ_SYM]), 198 (HREAL_ADD_ASSOC,HREAL_ADD_SYM, 199 [HREAL_LT_LADD, HREAL_LT_ADDL, HREAL_LT_ADDR, HREAL_LT_REFL])]); 200 201(*---------------------------------------------------------------------------*) 202(* Define operations on representatives. *) 203(*---------------------------------------------------------------------------*) 204 205val treal_0 = new_definition("treal_0", 206 ���treal_0 = (hreal_1,hreal_1)���); 207 208val treal_1 = new_definition("treal_1", 209 ���treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)���); 210 211val treal_neg = new_definition("treal_neg", 212 ���treal_neg (x:hreal,(y:hreal)) = (y,x)���); 213 214val treal_add = new_infixl_definition("treal_add", 215 ���$treal_add (x1,y1) (x2,y2) = (x1 hreal_add x2, y1 hreal_add y2)���,500); 216 217val treal_mul = new_infixl_definition("treal_mul", 218 ���treal_mul (x1,y1) (x2,y2) = 219 ((x1 hreal_mul x2) hreal_add (y1 hreal_mul y2), 220 (x1 hreal_mul y2) hreal_add (y1 hreal_mul x2))���, 600); 221 222val treal_lt = new_definition("treal_lt", 223���treal_lt (x1,y1) (x2,y2) = (x1 hreal_add y2) hreal_lt (x2 hreal_add y1)���); 224val _ = temp_set_fixity "treal_lt" (Infix(NONASSOC, 450)) 225 226val treal_inv = new_definition("treal_inv", 227 ���treal_inv (x,y) = 228 if (x = y) then treal_0 229 else if y hreal_lt x then 230 ((hreal_inv (x hreal_sub y)) hreal_add hreal_1,hreal_1) 231 else (hreal_1,(hreal_inv(y hreal_sub x)) hreal_add hreal_1)���); 232 233(*---------------------------------------------------------------------------*) 234(* Define the equivalence relation and prove it *is* one *) 235(*---------------------------------------------------------------------------*) 236 237val treal_eq = new_definition("treal_eq", 238 ���treal_eq (x1,y1) (x2,y2) = (x1 hreal_add y2 = x2 hreal_add y1)���); 239val _ = temp_set_fixity "treal_eq" (Infix(NONASSOC, 450)) 240 241val TREAL_EQ_REFL = store_thm("TREAL_EQ_REFL", 242 ���!x. x treal_eq x���, 243 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq] THEN REFL_TAC); 244 245val TREAL_EQ_SYM = store_thm("TREAL_EQ_SYM", 246 ���!x y. x treal_eq y = y treal_eq x���, 247 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq] THEN 248 CONV_TAC(RAND_CONV SYM_CONV) THEN REFL_TAC); 249 250val TREAL_EQ_TRANS = store_thm("TREAL_EQ_TRANS", 251 ���!x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z���, 252 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq] THEN 253 DISCH_THEN(MP_TAC o MK_COMB o (AP_TERM ���$hreal_add��� ## I) o CONJ_PAIR) 254 THEN CANCEL_TAC THEN DISCH_THEN SUBST1_TAC THEN CANCEL_TAC); 255 256val TREAL_EQ_EQUIV = store_thm("TREAL_EQ_EQUIV", 257 ���!p q. p treal_eq q = ($treal_eq p = $treal_eq q)���, 258 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN 259 CONV_TAC (ONCE_DEPTH_CONV (X_FUN_EQ_CONV ���r:hreal#hreal���)) THEN 260 EQ_TAC THENL 261 [DISCH_THEN(MP_TAC o SPEC ���q:hreal#hreal���) THEN 262 REWRITE_TAC[TREAL_EQ_REFL], 263 DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL 264 [RULE_ASSUM_TAC(ONCE_REWRITE_RULE[TREAL_EQ_SYM]), ALL_TAC] THEN 265 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN 266 MATCH_ACCEPT_TAC TREAL_EQ_TRANS]); 267 268val TREAL_EQ_AP = store_thm("TREAL_EQ_AP", 269 ���!p q. (p = q) ==> p treal_eq q���, 270 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN 271 MATCH_ACCEPT_TAC TREAL_EQ_REFL); 272 273(*---------------------------------------------------------------------------*) 274(* Prove the properties of representatives *) 275(*---------------------------------------------------------------------------*) 276 277val TREAL_10 = store_thm("TREAL_10", 278 ���~(treal_1 treal_eq treal_0)���, 279 REWRITE_TAC[treal_1, treal_0, treal_eq, HREAL_NOZERO]); 280 281val TREAL_ADD_SYM = store_thm("TREAL_ADD_SYM", 282 ���!x y. x treal_add y = y treal_add x���, 283 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_add] THEN 284 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) 285 [HREAL_ADD_SYM] THEN 286 REFL_TAC); 287 288val TREAL_MUL_SYM = store_thm("TREAL_MUL_SYM", 289 ���!x y. x treal_mul y = y treal_mul x���, 290 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul] THEN 291 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) 292 [HREAL_MUL_SYM] THEN 293 REWRITE_TAC[PAIR_EQ] THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM); 294 295val TREAL_ADD_ASSOC = store_thm("TREAL_ADD_ASSOC", 296 ���!x y z. x treal_add (y treal_add z) = (x treal_add y) treal_add z���, 297 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_add] THEN 298 REWRITE_TAC[HREAL_ADD_ASSOC]); 299 300val TREAL_MUL_ASSOC = store_thm("TREAL_MUL_ASSOC", 301 ���!x y z. x treal_mul (y treal_mul z) = (x treal_mul y) treal_mul z���, 302 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul] THEN 303 REWRITE_TAC[HREAL_LDISTRIB, HREAL_RDISTRIB, PAIR_EQ, GSYM HREAL_MUL_ASSOC] 304 THEN CONJ_TAC THEN CANCEL_TAC); 305 306val TREAL_LDISTRIB = store_thm("TREAL_LDISTRIB", 307 ���!x y z. x treal_mul (y treal_add z) = 308 (x treal_mul y) treal_add (x treal_mul z)���, 309 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul, treal_add] THEN 310 REWRITE_TAC[HREAL_LDISTRIB, PAIR_EQ] THEN 311 CONJ_TAC THEN CANCEL_TAC); 312 313val TREAL_ADD_LID = store_thm("TREAL_ADD_LID", 314 ���!x. (treal_0 treal_add x) treal_eq x���, 315 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_add, treal_eq] THEN 316 CANCEL_TAC); 317 318val TREAL_MUL_LID = store_thm("TREAL_MUL_LID", 319 ���!x. (treal_1 treal_mul x) treal_eq x���, 320 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_1, treal_mul, treal_eq] THEN 321 REWRITE_TAC[HREAL_MUL_LID, HREAL_LDISTRIB, HREAL_RDISTRIB] THEN 322 CANCEL_TAC THEN CANCEL_TAC); 323 324val TREAL_ADD_LINV = store_thm("TREAL_ADD_LINV", 325 ���!x. ((treal_neg x) treal_add x) treal_eq treal_0���, 326 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_neg, treal_add, treal_eq, treal_0] 327 THEN CANCEL_TAC); 328 329val TREAL_INV_0 = store_thm("TREAL_INV_0", 330 Term`treal_inv (treal_0) treal_eq (treal_0)`, 331 REWRITE_TAC[treal_inv, treal_eq, treal_0]); 332 333val TREAL_MUL_LINV = store_thm("TREAL_MUL_LINV", 334 ���!x. ~(x treal_eq treal_0) ==> 335 (((treal_inv x) treal_mul x) treal_eq treal_1)���, 336 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_eq, treal_inv] THEN 337 CANCEL_TAC THEN DISCH_TAC THEN DISJ_CASES_THEN2 338 (fn th => MP_TAC th THEN ASM_REWRITE_TAC[]) (DISJ_CASES_THEN ASSUME_TAC) 339 (SPECL [���FST (x:hreal#hreal)���, ���SND (x:hreal#hreal)���] HREAL_LT_TOTAL) THEN 340 FIRST_ASSUM(ASSUME_TAC o MATCH_MP HREAL_LT_GT) THEN 341 PURE_ASM_REWRITE_TAC[COND_CLAUSES, treal_mul, treal_eq, treal_1] THEN 342 REWRITE_TAC[HREAL_MUL_LID, HREAL_LDISTRIB, HREAL_RDISTRIB] THEN 343 CANCEL_TAC THEN W(SUBST1_TAC o SYM o C SPEC HREAL_MUL_LINV o 344 find_term(fn tm => rator(rator tm) = ���$hreal_sub��� handle _ => false) o snd) THEN 345 REWRITE_TAC[GSYM HREAL_LDISTRIB] THEN AP_TERM_TAC THEN 346 FIRST_ASSUM(SUBST1_TAC o MATCH_MP HREAL_SUB_ADD) THEN REFL_TAC); 347 348val TREAL_LT_TOTAL = store_thm("TREAL_LT_TOTAL", 349 ���!x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x���, 350 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_eq] THEN 351 MATCH_ACCEPT_TAC HREAL_LT_TOTAL); 352 353val TREAL_LT_REFL = store_thm("TREAL_LT_REFL", 354 ���!x. ~(x treal_lt x)���, 355 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt] THEN 356 MATCH_ACCEPT_TAC HREAL_LT_REFL); 357 358val TREAL_LT_TRANS = store_thm("TREAL_LT_TRANS", 359 ���!x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z���, 360 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt] THEN 361 DISCH_THEN(MP_TAC o MATCH_MP HREAL_LT_ADD2) THEN CANCEL_TAC THEN 362 DISCH_TAC THEN GEN_REWR_TAC RAND_CONV [HREAL_ADD_SYM] 363 THEN POP_ASSUM ACCEPT_TAC); 364 365val TREAL_LT_ADD = store_thm("TREAL_LT_ADD", 366 ���!x y z. (y treal_lt z) ==> (x treal_add y) treal_lt (x treal_add z)���, 367 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_add] THEN 368 CANCEL_TAC); 369 370val TREAL_LT_MUL = store_thm("TREAL_LT_MUL", 371 ���!x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==> 372 treal_0 treal_lt (x treal_mul y)���, 373 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_lt, treal_mul] THEN 374 CANCEL_TAC THEN DISCH_THEN(CONJUNCTS_THEN 375 (CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[HREAL_LT])) THEN 376 REWRITE_TAC[HREAL_LDISTRIB, HREAL_RDISTRIB] THEN CANCEL_TAC THEN CANCEL_TAC); 377 378(*---------------------------------------------------------------------------*) 379(* Rather than grub round proving the supremum property for representatives, *) 380(* we prove the appropriate order-isomorphism {x::R|0 < r} <-> R^+ *) 381(*---------------------------------------------------------------------------*) 382 383val treal_of_hreal = new_definition("treal_of_hreal", 384 ���treal_of_hreal x = (x hreal_add hreal_1,hreal_1)���); 385 386val hreal_of_treal = new_definition("hreal_of_treal", 387 ���hreal_of_treal (x,y) = @d. x = y hreal_add d���); 388 389val TREAL_BIJ = store_thm("TREAL_BIJ", 390 ���(!h. (hreal_of_treal(treal_of_hreal h)) = h) /\ 391 (!r. treal_0 treal_lt r = (treal_of_hreal(hreal_of_treal r)) treal_eq r)���, 392 CONJ_TAC THENL 393 [GEN_TAC THEN REWRITE_TAC[treal_of_hreal, hreal_of_treal] THEN 394 CANCEL_TAC THEN CONV_TAC SYM_CONV THEN 395 CONV_TAC(funpow 2 RAND_CONV ETA_CONV) THEN 396 MATCH_MP_TAC SELECT_AX THEN EXISTS_TAC ���h:hreal��� THEN REFL_TAC, 397 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_lt, treal_eq, 398 treal_of_hreal, hreal_of_treal] THEN CANCEL_TAC THEN EQ_TAC THENL 399 [DISCH_THEN(MP_TAC o MATCH_MP HREAL_SUB_ADD) THEN 400 DISCH_THEN(CONV_TAC o RAND_CONV o REWR_CONV o SYM o SELECT_RULE o 401 EXISTS(���?d. d hreal_add (SND r) = FST r���, ���(FST r) hreal_sub (SND r)���)) 402 THEN AP_THM_TAC THEN AP_TERM_TAC THEN 403 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV) 404 [HREAL_ADD_SYM] THEN 405 CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN REFL_TAC, 406 DISCH_THEN(SUBST1_TAC o SYM) THEN CANCEL_TAC]]); 407 408val TREAL_ISO = store_thm("TREAL_ISO", 409 ���!h i. h hreal_lt i ==> (treal_of_hreal h) treal_lt (treal_of_hreal i)���, 410 REPEAT GEN_TAC THEN REWRITE_TAC[treal_of_hreal, treal_lt] THEN CANCEL_TAC THEN 411 CANCEL_TAC); 412 413val TREAL_BIJ_WELLDEF = store_thm("TREAL_BIJ_WELLDEF", 414 ���!h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i)���, 415 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq, hreal_of_treal] THEN 416 DISCH_TAC THEN AP_TERM_TAC THEN CONV_TAC(X_FUN_EQ_CONV ���d:hreal���) THEN 417 GEN_TAC THEN BETA_TAC THEN EQ_TAC THENL 418 [DISCH_THEN(MP_TAC o C AP_THM ���SND(i:hreal#hreal)��� o AP_TERM ���$hreal_add���) 419 THEN POP_ASSUM SUBST1_TAC, 420 DISCH_THEN(MP_TAC o C AP_THM ���SND(h:hreal#hreal)��� o AP_TERM ���$hreal_add���) 421 THEN POP_ASSUM(SUBST1_TAC o SYM)] THEN 422 CANCEL_TAC THEN DISCH_THEN SUBST1_TAC THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM); 423 424(*---------------------------------------------------------------------------*) 425(* Prove that the operations on representatives are well-defined *) 426(*---------------------------------------------------------------------------*) 427 428val TREAL_NEG_WELLDEF = store_thm("TREAL_NEG_WELLDEF", 429 ���!x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2)���, 430 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_neg, treal_eq] THEN 431 DISCH_THEN(curry op THEN (ONCE_REWRITE_TAC[HREAL_ADD_SYM]) o SUBST1_TAC) THEN 432 REFL_TAC); 433 434val TREAL_ADD_WELLDEFR = store_thm("TREAL_ADD_WELLDEFR", 435 ���!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y)���, 436 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_add, treal_eq] THEN 437 CANCEL_TAC); 438 439val TREAL_ADD_WELLDEF = store_thm("TREAL_ADD_WELLDEF", 440 ���!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==> 441 (x1 treal_add y1) treal_eq (x2 treal_add y2)���, 442 REPEAT GEN_TAC THEN DISCH_TAC THEN 443 MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC ���x1 treal_add y2��� THEN 444 CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_ADD_SYM], ALL_TAC] THEN 445 MATCH_MP_TAC TREAL_ADD_WELLDEFR THEN ASM_REWRITE_TAC[]); 446 447val TREAL_MUL_WELLDEFR = store_thm("TREAL_MUL_WELLDEFR", 448 ���!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y)���, 449 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul, treal_eq] THEN 450 ONCE_REWRITE_TAC[AC(HREAL_ADD_ASSOC,HREAL_ADD_SYM) 451 ���(a hreal_add b) hreal_add (c hreal_add d) = 452 (a hreal_add d) hreal_add (b hreal_add c)���] THEN 453 REWRITE_TAC[GSYM HREAL_RDISTRIB] THEN DISCH_TAC THEN 454 ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN 455 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC); 456 457val TREAL_MUL_WELLDEF = store_thm("TREAL_MUL_WELLDEF", 458 ���!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==> 459 (x1 treal_mul y1) treal_eq (x2 treal_mul y2)���, 460 REPEAT GEN_TAC THEN DISCH_TAC THEN 461 MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC ���x1 treal_mul y2��� THEN 462 CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_MUL_SYM], ALL_TAC] THEN 463 MATCH_MP_TAC TREAL_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]); 464 465val TREAL_LT_WELLDEFR = store_thm("TREAL_LT_WELLDEFR", 466 ���!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_lt y = x2 treal_lt y)���, 467 let fun mkc v tm = SYM(SPECL (v::snd(strip_comb tm)) HREAL_LT_LADD) in 468 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_eq] THEN 469 DISCH_TAC THEN CONV_TAC(RAND_CONV(mkc ���SND (x1:hreal#hreal)���)) THEN 470 CONV_TAC(LAND_CONV(mkc ���SND (x2:hreal#hreal)���)) THEN 471 ONCE_REWRITE_TAC[AC(HREAL_ADD_ASSOC,HREAL_ADD_SYM) 472 ���a hreal_add (b hreal_add c) = (b hreal_add a) hreal_add c���] THEN 473 POP_ASSUM SUBST1_TAC THEN CANCEL_TAC end); 474 475val TREAL_LT_WELLDEFL = store_thm("TREAL_LT_WELLDEFL", 476 ���!x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2)���, 477 let fun mkc v tm = SYM(SPECL (v::snd(strip_comb tm)) HREAL_LT_LADD) in 478 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_eq] THEN 479 DISCH_TAC THEN CONV_TAC(RAND_CONV(mkc ���FST (y1:hreal#hreal)���)) THEN 480 CONV_TAC(LAND_CONV(mkc ���FST (y2:hreal#hreal)���)) THEN 481 ONCE_REWRITE_TAC[AC(HREAL_ADD_ASSOC,HREAL_ADD_SYM) 482 ���a hreal_add (b hreal_add c) = (a hreal_add c) hreal_add b���] THEN 483 POP_ASSUM SUBST1_TAC THEN CANCEL_TAC THEN AP_TERM_TAC THEN CANCEL_TAC end); 484 485val TREAL_LT_WELLDEF = store_thm("TREAL_LT_WELLDEF", 486 ���!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==> 487 (x1 treal_lt y1 = x2 treal_lt y2)���, 488 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN 489 EXISTS_TAC ���x1 treal_lt y2��� THEN CONJ_TAC THENL 490 [MATCH_MP_TAC TREAL_LT_WELLDEFL, MATCH_MP_TAC TREAL_LT_WELLDEFR] THEN 491 ASM_REWRITE_TAC[]); 492 493val TREAL_INV_WELLDEF = store_thm("TREAL_INV_WELLDEF", 494 ���!x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2)���, 495 let val lemma1 = prove 496 (���(a hreal_add b' = b hreal_add a') ==> 497 (a' hreal_lt a = b' hreal_lt b)���, 498 DISCH_TAC THEN EQ_TAC THEN 499 DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC o REWRITE_RULE[HREAL_LT]) THEN 500 POP_ASSUM MP_TAC THEN CANCEL_TAC THENL 501 [DISCH_THEN(SUBST1_TAC o SYM), DISCH_THEN SUBST1_TAC] THEN CANCEL_TAC) 502 val lemma2 = prove 503 (���(a hreal_add b' = b hreal_add a') ==> 504 ((a = a') = (b = b'))���, 505 DISCH_TAC THEN EQ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN POP_ASSUM MP_TAC 506 THEN CANCEL_TAC THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC) in 507 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_inv, treal_eq] THEN 508 DISCH_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP lemma1) THEN 509 FIRST_ASSUM(SUBST1_TAC o MATCH_MP lemma2) THEN COND_CASES_TAC THEN 510 REWRITE_TAC[TREAL_EQ_REFL] THEN COND_CASES_TAC THEN REWRITE_TAC[treal_eq] 511 THEN CANCEL_TAC THEN CANCEL_TAC THEN AP_TERM_TAC THEN 512 W(FREEZE_THEN(CONV_TAC o REWR_CONV) o GSYM o C SPEC HREAL_EQ_LADD o 513 mk_comb o (curry mk_comb ���$hreal_add��� ## I) o (rand ## rand) o dest_eq o snd) 514 THEN ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN 515 GEN_REWR_TAC (funpow 2 RAND_CONV) [HREAL_ADD_SYM] THEN 516 REWRITE_TAC[HREAL_ADD_ASSOC] THENL 517 [RULE_ASSUM_TAC GSYM, 518 MP_TAC(SPECL[���FST(x2:hreal#hreal)���, ���SND(x2:hreal#hreal)���] 519 HREAL_LT_TOTAL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN 520 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[HREAL_ADD_SYM])] THEN 521 FIRST_ASSUM(fn th => FIRST_ASSUM(MP_TAC o EQ_MP (MATCH_MP lemma1 th))) THEN 522 FIRST_ASSUM(UNDISCH_TAC o assert(curry op =���$hreal_lt��� o rator o rator) o concl) 523 THEN REPEAT(DISCH_THEN(SUBST1_TAC o MATCH_MP HREAL_SUB_ADD)) THEN 524 FIRST_ASSUM SUBST1_TAC THEN REFL_TAC end); 525 526(*---------------------------------------------------------------------------*) 527(* Now define the functions over the equivalence classes *) 528(*---------------------------------------------------------------------------*) 529 530val [REAL_10, REAL_ADD_SYM, REAL_MUL_SYM, REAL_ADD_ASSOC, 531 REAL_MUL_ASSOC, REAL_LDISTRIB, REAL_ADD_LID, REAL_MUL_LID, 532 REAL_ADD_LINV, REAL_MUL_LINV, REAL_LT_TOTAL, REAL_LT_REFL, 533 REAL_LT_TRANS, REAL_LT_IADD, REAL_LT_MUL, REAL_BIJ, REAL_ISO,REAL_INV_0] = 534 let fun mk_def (d,t,n,f) = {def_name=d, fixity=f, fname=n, func=t} 535 in 536 quotient.define_equivalence_type 537 {name = "real", 538 equiv = TREAL_EQ_EQUIV, 539 defs = [mk_def("real_0", Term`treal_0`, "real_0", NONE), 540 mk_def("real_1", Term`treal_1`, "real_1", NONE), 541 mk_def("real_neg", Term`treal_neg`, "real_neg", NONE), 542 mk_def("real_inv", Term`treal_inv`, "inv", NONE), 543 mk_def("real_add", Term`$treal_add`, "real_add", SOME(Infixl 500)), 544 mk_def("real_mul", Term`$treal_mul`, "real_mul", SOME(Infixl 600)), 545 mk_def("real_lt", Term`$treal_lt`, "real_lt", NONE), 546 mk_def("real_of_hreal",Term`$treal_of_hreal`, "real_of_hreal",NONE), 547 mk_def("hreal_of_real", Term`$hreal_of_treal`,"hreal_of_real",NONE)], 548 welldefs = [TREAL_NEG_WELLDEF, TREAL_INV_WELLDEF, TREAL_LT_WELLDEF, 549 TREAL_ADD_WELLDEF, TREAL_MUL_WELLDEF, TREAL_BIJ_WELLDEF], 550 old_thms = ([TREAL_10] 551 @ (map (GEN_ALL o MATCH_MP TREAL_EQ_AP o SPEC_ALL) 552 [TREAL_ADD_SYM, TREAL_MUL_SYM, TREAL_ADD_ASSOC, 553 TREAL_MUL_ASSOC, TREAL_LDISTRIB]) 554 @ [TREAL_ADD_LID, TREAL_MUL_LID, TREAL_ADD_LINV, 555 TREAL_MUL_LINV, TREAL_LT_TOTAL, TREAL_LT_REFL, 556 TREAL_LT_TRANS, TREAL_LT_ADD, TREAL_LT_MUL, TREAL_BIJ, 557 TREAL_ISO,TREAL_INV_0])} 558 end; 559 560val _ = 561 add_rule { block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 562 fixity = Suffix 2100, 563 paren_style = OnlyIfNecessary, 564 pp_elements = [TOK (UnicodeChars.sup_minus ^ UnicodeChars.sup_1)], 565 term_name = "realinv"} 566val _ = overload_on("realinv", ``inv``); 567 568(*--------------------------------------------------------------------------- 569 Overload arithmetic operations. 570 ---------------------------------------------------------------------------*) 571 572val natplus = Term`$+`; 573val natless = Term`$<`; 574val bool_not = Term`$~` 575val natmult = Term`$*`; 576 577val _ = overload_on ("~", bool_not); 578 579val _ = overload_on ("+", natplus); 580val _ = overload_on ("*", natmult); 581val _ = overload_on ("<", natless); 582 583val _ = overload_on ("~", Term`$real_neg`); 584val _ = overload_on ("numeric_negate", Term`$real_neg`); 585val _ = overload_on ("+", Term`$real_add`); 586val _ = overload_on ("*", Term`$real_mul`); 587val _ = overload_on ("<", Term`real_lt`); 588 589 590(*---------------------------------------------------------------------------*) 591(* Transfer of supremum property for all-positive sets - bit painful *) 592(*---------------------------------------------------------------------------*) 593 594val REAL_ISO_EQ = store_thm("REAL_ISO_EQ", 595 ���!h i. h hreal_lt i = real_of_hreal h < real_of_hreal i���, 596 REPEAT GEN_TAC THEN EQ_TAC THENL 597 [MATCH_ACCEPT_TAC REAL_ISO, 598 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 599 (SPECL [���h:hreal���, ���i:hreal���] HREAL_LT_TOTAL) THEN 600 ASM_REWRITE_TAC[REAL_LT_REFL] THEN 601 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ (MATCH_MP REAL_ISO th))) THEN 602 DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_TRANS) THEN 603 REWRITE_TAC[REAL_LT_REFL]]); 604 605val REAL_POS = store_thm("REAL_POS", 606 ���!X. real_0 < real_of_hreal X���, 607 GEN_TAC THEN REWRITE_TAC[REAL_BIJ]); 608 609val SUP_ALLPOS_LEMMA1 = store_thm("SUP_ALLPOS_LEMMA1", 610 ���!P y. (!x. P x ==> real_0 < x) ==> 611 ((?x. P x /\ y < x) = 612 (?X. P(real_of_hreal X) /\ y < (real_of_hreal X)))���, 613 REPEAT GEN_TAC THEN DISCH_TAC THEN EQ_TAC THENL 614 [DISCH_THEN(X_CHOOSE_THEN ���x:real��� (fn th => MP_TAC th THEN POP_ASSUM 615 (SUBST1_TAC o SYM o REWRITE_RULE[REAL_BIJ] o C MATCH_MP (CONJUNCT1 th)))) 616 THEN DISCH_TAC THEN EXISTS_TAC ���hreal_of_real x��� THEN ASM_REWRITE_TAC[], 617 DISCH_THEN(X_CHOOSE_THEN ���X:hreal��� ASSUME_TAC) THEN 618 EXISTS_TAC ���real_of_hreal X��� THEN ASM_REWRITE_TAC[]]); 619 620val SUP_ALLPOS_LEMMA2 = store_thm("SUP_ALLPOS_LEMMA2", 621 ���!P X. P(real_of_hreal X) :bool = (\h. P(real_of_hreal h)) X���, 622 REPEAT GEN_TAC THEN BETA_TAC THEN REFL_TAC); 623 624val SUP_ALLPOS_LEMMA3 = store_thm("SUP_ALLPOS_LEMMA3", 625 ���!P. (!x. P x ==> real_0 < x) /\ 626 (?x. P x) /\ 627 (?z. !x. P x ==> x < z) 628 ==> (?X. (\h. P(real_of_hreal h)) X) /\ 629 (?Y. !X. (\h. P(real_of_hreal h)) X ==> X hreal_lt Y)���, 630 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC STRIP_ASSUME_TAC) THEN 631 CONJ_TAC THENL 632 [EXISTS_TAC ���hreal_of_real x��� THEN BETA_TAC THEN 633 FIRST_ASSUM(SUBST1_TAC o REWRITE_RULE[REAL_BIJ] o 634 C MATCH_MP (ASSUME ���(P:real->bool) x���)) THEN 635 FIRST_ASSUM ACCEPT_TAC, 636 EXISTS_TAC ���hreal_of_real z��� THEN BETA_TAC THEN GEN_TAC THEN 637 UNDISCH_TAC ���(P:real->bool) x��� THEN DISCH_THEN(K ALL_TAC) THEN 638 DISCH_THEN(fn th => EVERY_ASSUM(MP_TAC o C MATCH_MP th)) THEN 639 POP_ASSUM_LIST(K ALL_TAC) THEN REPEAT DISCH_TAC THEN 640 REWRITE_TAC[REAL_ISO_EQ] THEN 641 MP_TAC(SPECL[���real_0���, ���real_of_hreal X���, ���z:real���] REAL_LT_TRANS) THEN 642 ASM_REWRITE_TAC[REAL_BIJ] THEN 643 DISCH_THEN SUBST_ALL_TAC THEN FIRST_ASSUM ACCEPT_TAC]); 644 645val SUP_ALLPOS_LEMMA4 = store_thm("SUP_ALLPOS_LEMMA4", 646 ���!y. ~(real_0 < y) ==> !x. y < (real_of_hreal x)���, 647 GEN_TAC THEN DISCH_THEN(curry op THEN GEN_TAC o MP_TAC) THEN 648 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC 649 (SPECL [���y:real���, ���real_0���] REAL_LT_TOTAL) THEN 650 ASM_REWRITE_TAC[REAL_POS] THEN DISCH_THEN(K ALL_TAC) THEN 651 POP_ASSUM(MP_TAC o C CONJ (SPEC ���x:hreal��� REAL_POS)) THEN 652 DISCH_THEN(ACCEPT_TAC o MATCH_MP REAL_LT_TRANS)); 653 654val REAL_SUP_ALLPOS = store_thm("REAL_SUP_ALLPOS", 655 ���!P. (!x. P x ==> real_0 < x) /\ (?x. P x) /\ (?z. !x. P x ==> x < z) 656 ==> (?s. !y. (?x. P x /\ y < x) = y < s)���, 657 let val lemma = TAUT_CONV ���a /\ b ==> (a = b)��� in 658 GEN_TAC THEN DISCH_TAC THEN 659 EXISTS_TAC ���real_of_hreal(hreal_sup(\h. P(real_of_hreal h)))��� THEN 660 GEN_TAC THEN 661 FIRST_ASSUM(fn th => REWRITE_TAC[MATCH_MP SUP_ALLPOS_LEMMA1(CONJUNCT1 th)]) THEN 662 ASM_CASES_TAC ���real_0 < y��� THENL 663 [FIRST_ASSUM(SUBST1_TAC o SYM o REWRITE_RULE[REAL_BIJ]) THEN 664 REWRITE_TAC[GSYM REAL_ISO_EQ] THEN 665 GEN_REWR_TAC (RATOR_CONV o ONCE_DEPTH_CONV) 666 [SUP_ALLPOS_LEMMA2] THEN 667 FIRST_ASSUM(ASSUME_TAC o MATCH_MP HREAL_SUP o MATCH_MP SUP_ALLPOS_LEMMA3) 668 THEN ASM_REWRITE_TAC[], 669 MATCH_MP_TAC lemma THEN CONJ_TAC THENL 670 [FIRST_ASSUM(MP_TAC o MATCH_MP SUP_ALLPOS_LEMMA3) THEN 671 BETA_TAC THEN DISCH_THEN(X_CHOOSE_TAC ���X:hreal��� o CONJUNCT1) THEN 672 EXISTS_TAC ���X:hreal��� THEN ASM_REWRITE_TAC[], ALL_TAC] THEN 673 FIRST_ASSUM(MATCH_ACCEPT_TAC o MATCH_MP SUP_ALLPOS_LEMMA4)] end); 674 675(*---------------------------------------------------------------------------*) 676(* Now save all the unsaved theorems *) 677(*---------------------------------------------------------------------------*) 678 679val _ = map save_thm 680 [("REAL_10",REAL_10), ("REAL_ADD_SYM",REAL_ADD_SYM), 681 ("REAL_MUL_SYM",REAL_MUL_SYM), ("REAL_ADD_ASSOC",REAL_ADD_ASSOC), 682 ("REAL_MUL_ASSOC",REAL_MUL_ASSOC), ("REAL_LDISTRIB",REAL_LDISTRIB), 683 ("REAL_ADD_LID",REAL_ADD_LID), ("REAL_MUL_LID",REAL_MUL_LID), 684 ("REAL_ADD_LINV",REAL_ADD_LINV), ("REAL_MUL_LINV",REAL_MUL_LINV), 685 ("REAL_LT_TOTAL",REAL_LT_TOTAL), ("REAL_LT_REFL",REAL_LT_REFL), 686 ("REAL_LT_TRANS",REAL_LT_TRANS), ("REAL_LT_IADD",REAL_LT_IADD), 687 ("REAL_LT_MUL",REAL_LT_MUL), ("REAL_INV_0",REAL_INV_0)]; 688 689val _ = export_theory(); 690