hrealScript.sml
1(*---------------------------------------------------------------------------*)
2(* Construct positive reals from positive rationals *)
3(*---------------------------------------------------------------------------*)
4Theory hreal
5Ancestors
6 pair arithmetic num prim_rec hrat
7Libs
8 hol88Lib numLib reduceLib pairLib jrhUtils
9
10
11infix THEN THENL ORELSE ORELSEC;
12
13val _ = ParseExtras.temp_loose_equality()
14
15val GEN_ALL = hol88Lib.GEN_ALL; (* it has old reverted variable order *)
16
17(*---------------------------------------------------------------------------*)
18(* Lemmas about the half-rationals, including definition of ordering *)
19(*---------------------------------------------------------------------------*)
20
21Definition hrat_lt[nocompute]:
22 $hrat_lt x y = ?d. y = x hrat_add d
23End
24val _ = temp_set_fixity "hrat_lt" (Infix(NONASSOC, 450))
25
26Theorem HRAT_LT_REFL:
27 !x. ~(x hrat_lt x)
28Proof
29 GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
30 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
31 REWRITE_TAC[HRAT_NOZERO]
32QED
33
34Theorem HRAT_LT_TRANS:
35 !x y z. x hrat_lt y /\ y hrat_lt z ==> x hrat_lt z
36Proof
37 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
38 DISCH_THEN(CONJUNCTS_THEN2 CHOOSE_TAC (CHOOSE_THEN SUBST1_TAC)) THEN
39 POP_ASSUM SUBST1_TAC THEN REWRITE_TAC[GSYM HRAT_ADD_ASSOC] THEN
40 W(EXISTS_TAC o rand o lhs o body o rand o snd) THEN REFL_TAC
41QED
42
43Theorem HRAT_LT_ANTISYM:
44 !x y. ~(x hrat_lt y /\ y hrat_lt x)
45Proof
46 REPEAT GEN_TAC THEN
47 DISCH_THEN(MP_TAC o MATCH_MP HRAT_LT_TRANS) THEN
48 REWRITE_TAC[HRAT_LT_REFL]
49QED
50
51Theorem HRAT_LT_TOTAL:
52 !x y. (x = y) \/ x hrat_lt y \/ y hrat_lt x
53Proof
54 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
55 REPEAT_TCL DISJ_CASES_THEN (SUBST1_TAC o EQT_INTRO)
56 (SPECL [“x:hrat”, “y:hrat”] HRAT_ADD_TOTAL) THEN
57 REWRITE_TAC[]
58QED
59
60Theorem HRAT_MUL_RID:
61 !x. x hrat_mul hrat_1 = x
62Proof
63 GEN_TAC THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
64 MATCH_ACCEPT_TAC HRAT_MUL_LID
65QED
66
67Theorem HRAT_MUL_RINV:
68 !x. x hrat_mul (hrat_inv x) = hrat_1
69Proof
70 GEN_TAC THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
71 MATCH_ACCEPT_TAC HRAT_MUL_LINV
72QED
73
74Theorem HRAT_RDISTRIB:
75 !x y z. (x hrat_add y) hrat_mul z =
76 (x hrat_mul z) hrat_add (y hrat_mul z)
77Proof
78 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
79 MATCH_ACCEPT_TAC HRAT_LDISTRIB
80QED
81
82Theorem HRAT_LT_ADDL:
83 !x y. x hrat_lt (x hrat_add y)
84Proof
85 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
86 EXISTS_TAC “y:hrat” THEN REFL_TAC
87QED
88
89Theorem HRAT_LT_ADDR:
90 !x y. y hrat_lt (x hrat_add y)
91Proof
92 ONCE_REWRITE_TAC[HRAT_ADD_SYM] THEN
93 MATCH_ACCEPT_TAC HRAT_LT_ADDL
94QED
95
96Theorem HRAT_LT_GT:
97 !x y. x hrat_lt y ==> ~(y hrat_lt x)
98Proof
99 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
100 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
101 REWRITE_TAC[GSYM HRAT_ADD_ASSOC] THEN
102 CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN
103 REWRITE_TAC[HRAT_NOZERO]
104QED
105
106Theorem HRAT_LT_NE:
107 !x y. x hrat_lt y ==> ~(x = y)
108Proof
109 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
110 REWRITE_TAC[] THEN DISCH_THEN SUBST1_TAC THEN
111 MATCH_ACCEPT_TAC HRAT_LT_REFL
112QED
113
114Theorem HRAT_EQ_LADD:
115 !x y z. (x hrat_add y = x hrat_add z) = (y = z)
116Proof
117 REPEAT GEN_TAC THEN EQ_TAC THENL
118 [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
119 (SPECL [“y:hrat”, “z:hrat”] HRAT_ADD_TOTAL) THEN
120 ASM_REWRITE_TAC[] THEN POP_ASSUM(CHOOSE_THEN SUBST1_TAC) THEN
121 REWRITE_TAC[HRAT_ADD_ASSOC, HRAT_NOZERO, GSYM HRAT_NOZERO],
122 DISCH_THEN SUBST1_TAC THEN REFL_TAC]
123QED
124
125Theorem HRAT_EQ_LMUL:
126 !x y z. (x hrat_mul y = x hrat_mul z) = (y = z)
127Proof
128 REPEAT GEN_TAC THEN EQ_TAC THENL
129 [DISCH_THEN(MP_TAC o AP_TERM “$hrat_mul (hrat_inv x)”) THEN
130 REWRITE_TAC[HRAT_MUL_ASSOC, HRAT_MUL_LINV, HRAT_MUL_LID],
131 DISCH_THEN SUBST1_TAC THEN REFL_TAC]
132QED
133
134Theorem HRAT_LT_ADD2:
135 !u v x y. u hrat_lt x /\ v hrat_lt y ==>
136 (u hrat_add v) hrat_lt (x hrat_add y)
137Proof
138 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
139 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN “d1:hrat” SUBST1_TAC)
140 (X_CHOOSE_THEN “d2:hrat” SUBST1_TAC)) THEN
141 EXISTS_TAC “d1 hrat_add d2” THEN
142 CONV_TAC(AC_CONV(HRAT_ADD_ASSOC,HRAT_ADD_SYM))
143QED
144
145Theorem HRAT_LT_LADD:
146 !x y z. (z hrat_add x) hrat_lt (z hrat_add y) = x hrat_lt y
147Proof
148 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN EQ_TAC THEN
149 DISCH_THEN(X_CHOOSE_THEN “d:hrat” (curry op THEN (EXISTS_TAC “d:hrat”) o MP_TAC))
150 THEN REWRITE_TAC[GSYM HRAT_ADD_ASSOC, HRAT_EQ_LADD]
151QED
152
153Theorem HRAT_LT_RADD:
154 !x y z. (x hrat_add z) hrat_lt (y hrat_add z) = x hrat_lt y
155Proof
156 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[HRAT_ADD_SYM] THEN
157 MATCH_ACCEPT_TAC HRAT_LT_LADD
158QED
159
160Theorem HRAT_LT_MUL2:
161 !u v x y. u hrat_lt x /\ v hrat_lt y ==>
162 (u hrat_mul v) hrat_lt (x hrat_mul y)
163Proof
164 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN
165 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN “d1:hrat” SUBST1_TAC)
166 (X_CHOOSE_THEN “d2:hrat” SUBST1_TAC)) THEN
167 REWRITE_TAC[HRAT_LDISTRIB, HRAT_RDISTRIB, GSYM HRAT_ADD_ASSOC] THEN
168 REWRITE_TAC[HRAT_EQ_LADD] THEN
169 W(EXISTS_TAC o lhs o body o rand o snd) THEN REFL_TAC
170QED
171
172Theorem HRAT_LT_LMUL:
173 !x y z. (z hrat_mul x) hrat_lt (z hrat_mul y) = x hrat_lt y
174Proof
175 REPEAT GEN_TAC THEN REWRITE_TAC[hrat_lt] THEN EQ_TAC THEN
176 DISCH_THEN(X_CHOOSE_TAC “d:hrat”) THENL
177 [EXISTS_TAC “(hrat_inv z) hrat_mul d”,
178 EXISTS_TAC “z hrat_mul d”] THEN POP_ASSUM MP_TAC THEN
179 REWRITE_TAC[GSYM HRAT_LDISTRIB, GSYM HRAT_MUL_ASSOC, HRAT_EQ_LMUL] THEN
180 DISCH_THEN(MP_TAC o AP_TERM “$hrat_mul (hrat_inv z)”) THEN
181 REWRITE_TAC[HRAT_MUL_ASSOC, HRAT_MUL_LINV, HRAT_MUL_LID, HRAT_LDISTRIB]
182QED
183
184Theorem HRAT_LT_RMUL:
185 !x y z. (x hrat_mul z) hrat_lt (y hrat_mul z) = x hrat_lt y
186Proof
187 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
188 MATCH_ACCEPT_TAC HRAT_LT_LMUL
189QED
190
191Theorem HRAT_LT_LMUL1:
192 !x y. (x hrat_mul y) hrat_lt y = x hrat_lt hrat_1
193Proof
194 REPEAT GEN_TAC THEN
195 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [GSYM HRAT_MUL_LID] THEN
196 MATCH_ACCEPT_TAC HRAT_LT_RMUL
197QED
198
199Theorem HRAT_LT_RMUL1:
200 !x y. (x hrat_mul y) hrat_lt x = y hrat_lt hrat_1
201Proof
202 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
203 MATCH_ACCEPT_TAC HRAT_LT_LMUL1
204QED
205
206Theorem HRAT_GT_LMUL1:
207 !x y. y hrat_lt (x hrat_mul y) = hrat_1 hrat_lt x
208Proof
209 REPEAT GEN_TAC THEN
210 GEN_REWR_TAC (funpow 2 LAND_CONV) [GSYM HRAT_MUL_LID]
211 THEN MATCH_ACCEPT_TAC HRAT_LT_RMUL
212QED
213
214Theorem HRAT_LT_L1:
215 !x y. ((hrat_inv x) hrat_mul y) hrat_lt hrat_1 = y hrat_lt x
216Proof
217 REPEAT GEN_TAC THEN SUBST1_TAC(SYM(SPEC “x:hrat” HRAT_MUL_LINV)) THEN
218 MATCH_ACCEPT_TAC HRAT_LT_LMUL
219QED
220
221Theorem HRAT_LT_R1:
222 !x y. (x hrat_mul (hrat_inv y)) hrat_lt hrat_1 = x hrat_lt y
223Proof
224 REPEAT GEN_TAC THEN SUBST1_TAC(SYM(SPEC “y:hrat” HRAT_MUL_RINV)) THEN
225 MATCH_ACCEPT_TAC HRAT_LT_RMUL
226QED
227
228Theorem HRAT_GT_L1:
229 !x y. hrat_1 hrat_lt ((hrat_inv x) hrat_mul y) = x hrat_lt y
230Proof
231 REPEAT GEN_TAC THEN SUBST1_TAC(SYM(SPEC “x:hrat” HRAT_MUL_LINV)) THEN
232 MATCH_ACCEPT_TAC HRAT_LT_LMUL
233QED
234
235Theorem HRAT_INV_MUL:
236 !x y. hrat_inv (x hrat_mul y) = (hrat_inv x) hrat_mul (hrat_inv y)
237Proof
238 REPEAT GEN_TAC THEN SUBST1_TAC
239 (SYM(SPECL [“x hrat_mul y”, “hrat_inv (x hrat_mul y)”,
240 “(hrat_inv x) hrat_mul (hrat_inv y)”] HRAT_EQ_LMUL)) THEN
241 ONCE_REWRITE_TAC[AC(HRAT_MUL_ASSOC,HRAT_MUL_SYM)
242 “(a hrat_mul b) hrat_mul (c hrat_mul d) =
243 (a hrat_mul c) hrat_mul (b hrat_mul d)”] THEN
244 REWRITE_TAC[HRAT_MUL_RINV, HRAT_MUL_LID]
245QED
246
247Theorem HRAT_UP:
248 !x. ?y. x hrat_lt y
249Proof
250 GEN_TAC THEN EXISTS_TAC “x hrat_add x” THEN
251 REWRITE_TAC[hrat_lt] THEN EXISTS_TAC “x:hrat” THEN REFL_TAC
252QED
253
254Theorem HRAT_DOWN:
255 !x. ?y. y hrat_lt x
256Proof
257 GEN_TAC THEN
258 EXISTS_TAC “x hrat_mul (hrat_inv (hrat_1 hrat_add hrat_1))” THEN
259 REWRITE_TAC[HRAT_LT_RMUL1] THEN
260 GEN_REWR_TAC LAND_CONV [GSYM HRAT_MUL_LID] THEN
261 REWRITE_TAC[HRAT_LT_R1] THEN REWRITE_TAC[hrat_lt] THEN
262 EXISTS_TAC “hrat_1” THEN REFL_TAC
263QED
264
265Theorem HRAT_DOWN2:
266 !x y. ?z. z hrat_lt x /\ z hrat_lt y
267Proof
268 REPEAT GEN_TAC THEN
269 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
270 (SPECL [“x:hrat”, “y:hrat”] HRAT_ADD_TOTAL) THEN
271 ASM_REWRITE_TAC[HRAT_DOWN] THEN
272 POP_ASSUM(X_CHOOSE_THEN “d:hrat” SUBST1_TAC) THENL
273 [X_CHOOSE_TAC “z:hrat” (SPEC “y:hrat” HRAT_DOWN),
274 X_CHOOSE_TAC “z:hrat” (SPEC “x:hrat” HRAT_DOWN)] THEN
275 EXISTS_TAC “z:hrat” THEN RULE_ASSUM_TAC(REWRITE_RULE[hrat_lt]) THEN
276 POP_ASSUM(CHOOSE_THEN SUBST1_TAC) THEN
277 REWRITE_TAC[GSYM HRAT_ADD_ASSOC, HRAT_LT_ADDL]
278QED
279
280Theorem HRAT_MEAN:
281 !x y. x hrat_lt y ==> (?z. x hrat_lt z /\ z hrat_lt y)
282Proof
283 REPEAT GEN_TAC THEN DISCH_TAC THEN
284 EXISTS_TAC “(x hrat_add y) hrat_mul (hrat_inv(hrat_1 hrat_add hrat_1))” THEN
285 FREEZE_THEN (fn th => ONCE_REWRITE_TAC[th]) ((GENL [“x:hrat”, “y:hrat”] o SYM o
286 SPECL [“x:hrat”, “y:hrat”, “hrat_1 hrat_add hrat_1”]) HRAT_LT_RMUL) THEN
287 REWRITE_TAC[GSYM HRAT_MUL_ASSOC, HRAT_MUL_LINV, HRAT_MUL_RID] THEN
288 REWRITE_TAC[HRAT_LDISTRIB, HRAT_MUL_RID] THEN
289 ASM_REWRITE_TAC[HRAT_LT_LADD, HRAT_LT_RADD]
290QED
291
292(*---------------------------------------------------------------------------*)
293(* Define cuts and the type ":hreal" *)
294(*---------------------------------------------------------------------------*)
295
296val _ = Parse.hide "C"; (* in combinTheory *)
297
298Definition isacut[nocompute]:
299isacut C =
300 (?x. C x) /\ (* Nonempty *)
301 (?x. ~C x) /\ (* Bounded above *)
302 (!x y. C x /\ y hrat_lt x ==> C y) /\ (* Downward closed *)
303 (!x. C x ==> ?y. C y /\ x hrat_lt y) (* No greatest element*)
304End
305
306Definition cut_of_hrat[nocompute]:
307 cut_of_hrat x = \y. y hrat_lt x
308End
309
310Theorem ISACUT_HRAT:
311 !h. isacut(cut_of_hrat h)
312Proof
313 let val th = TAUT_CONV “!x y. ~(x /\ y) ==> (x ==> ~y)” in
314 GEN_TAC THEN REWRITE_TAC[cut_of_hrat, isacut] THEN BETA_TAC THEN
315 REPEAT CONJ_TAC THEN ONCE_REWRITE_TAC[CONJ_SYM] THEN
316 REWRITE_TAC[HRAT_DOWN, HRAT_MEAN, HRAT_LT_TRANS] THEN
317 X_CHOOSE_TAC “x:hrat” (SPEC “h:hrat” HRAT_UP) THEN
318 EXISTS_TAC “x:hrat” THEN POP_ASSUM MP_TAC THEN
319 MATCH_MP_TAC th THEN MATCH_ACCEPT_TAC HRAT_LT_ANTISYM end
320QED
321
322val hreal_tydef = new_type_definition
323 ("hreal",
324 prove (“?C. isacut C”,
325 EXISTS_TAC “cut_of_hrat($@(K T))” THEN
326 MATCH_ACCEPT_TAC ISACUT_HRAT));
327
328val hreal_tybij =
329 define_new_type_bijections
330 {name="hreal_tybij",ABS="hreal",REP="cut",tyax=hreal_tydef};
331
332Theorem EQUAL_CUTS:
333 !X Y. (cut X = cut Y) ==> (X = Y)
334Proof
335 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM “hreal”) THEN
336 REWRITE_TAC[hreal_tybij]
337QED
338
339(*---------------------------------------------------------------------------*)
340(* Required lemmas about cuts *)
341(*---------------------------------------------------------------------------*)
342
343Theorem CUT_ISACUT:
344 !X. isacut (cut X)
345Proof
346 REWRITE_TAC[hreal_tybij]
347QED
348
349val CUT_PROPERTIES = EQ_MP (SPEC “cut X” isacut)
350 (SPEC “X:hreal” CUT_ISACUT);
351
352Theorem CUT_NONEMPTY:
353 !X. ?x. (cut X) x
354Proof
355 REWRITE_TAC[CUT_PROPERTIES]
356QED
357
358Theorem CUT_BOUNDED:
359 !X. ?x. ~((cut X) x)
360Proof
361 REWRITE_TAC[CUT_PROPERTIES]
362QED
363
364Theorem CUT_DOWN:
365 !X x y. cut X x /\ y hrat_lt x ==> cut X y
366Proof
367 REWRITE_TAC[CUT_PROPERTIES]
368QED
369
370Theorem CUT_UP:
371 !X x. cut X x ==> (?y. cut X y /\ x hrat_lt y)
372Proof
373 REWRITE_TAC[CUT_PROPERTIES]
374QED
375
376Theorem CUT_UBOUND:
377 !X x y. ~((cut X) x) /\ x hrat_lt y ==> ~((cut X) y)
378Proof
379 let val lemma = TAUT_CONV “(~a /\ b ==> ~c) = (c /\ b ==> a)” in
380 REWRITE_TAC[lemma, CUT_DOWN] end
381QED
382
383Theorem CUT_STRADDLE:
384 !X x y. (cut X) x /\ ~((cut X) y) ==> x hrat_lt y
385Proof
386 let val lemma = TAUT_CONV “~(a /\ ~a)” in
387 REPEAT GEN_TAC THEN
388 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
389 (SPECL [“x:hrat”, “y:hrat”] HRAT_LT_TOTAL) THEN
390 ASM_REWRITE_TAC[lemma] THEN
391 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
392 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
393 REWRITE_TAC[] THEN MATCH_MP_TAC CUT_DOWN THEN
394 EXISTS_TAC “x:hrat” THEN ASM_REWRITE_TAC[] end
395QED
396
397Theorem CUT_NEARTOP_ADD:
398 !X e. ?x. (cut X) x /\ ~((cut X) (x hrat_add e))
399Proof
400 REPEAT GEN_TAC THEN X_CHOOSE_TAC “x1:hrat”
401 (SPEC “X:hreal” CUT_BOUNDED) THEN
402 EVERY_TCL (map X_CHOOSE_THEN [“n:num”, “d:hrat”])
403 (MP_TAC o AP_TERM “$hrat_mul e”)
404 (SPEC “(hrat_inv e) hrat_mul x1” HRAT_ARCH) THEN
405 REWRITE_TAC[HRAT_LDISTRIB, HRAT_MUL_ASSOC,
406 HRAT_MUL_RINV, HRAT_MUL_LID] THEN
407 DISCH_THEN(MP_TAC o EXISTS
408 (“?d. e hrat_mul (hrat_sucint n) = x1 hrat_add d”,
409 “e hrat_mul d”)) THEN
410 REWRITE_TAC[GSYM hrat_lt] THEN
411 POP_ASSUM(fn th => DISCH_THEN (MP_TAC o MATCH_MP CUT_UBOUND o CONJ th)) THEN
412 DISCH_THEN(X_CHOOSE_THEN “k:num” MP_TAC o CONV_RULE EXISTS_LEAST_CONV o
413 EXISTS(“?n. ~((cut X) (e hrat_mul (hrat_sucint n)))”,
414 “n:num”)) THEN
415 DISJ_CASES_THEN2 SUBST1_TAC (X_CHOOSE_THEN “n:num” SUBST1_TAC)
416 (SPEC “k:num” num_CASES) THEN ASM_REWRITE_TAC[HRAT_SUCINT] THENL
417 [REWRITE_TAC[NOT_LESS_0, HRAT_MUL_RINV, HRAT_MUL_RID] THEN
418 X_CHOOSE_TAC “x:hrat” (SPEC “X:hreal” CUT_NONEMPTY) THEN
419 DISCH_THEN(curry op THEN (EXISTS_TAC “x:hrat”) o MP_TAC) THEN
420 POP_ASSUM(SUBST1_TAC o EQT_INTRO) THEN REWRITE_TAC[] THEN
421 DISCH_THEN(ACCEPT_TAC o MATCH_MP CUT_UBOUND o
422 C CONJ (SPECL [“x:hrat”, “e:hrat”] HRAT_LT_ADDR)),
423 REWRITE_TAC[HRAT_LDISTRIB, HRAT_MUL_RID] THEN
424 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
425 (ASSUME_TAC o REWRITE_RULE[LESS_SUC_REFL] o SPEC “n:num”)) THEN
426 EXISTS_TAC “e hrat_mul (hrat_sucint n)” THEN ASM_REWRITE_TAC[]]
427QED
428
429Theorem CUT_NEARTOP_MUL:
430 !X u. hrat_1 hrat_lt u ==> ?x. (cut X) x /\ ~((cut X)(u hrat_mul x))
431Proof
432 REPEAT GEN_TAC THEN
433 X_CHOOSE_TAC “x0:hrat”
434 (SPEC “X:hreal” CUT_NONEMPTY) THEN
435 ASM_CASES_TAC “(cut X)(u hrat_mul x0)” THENL
436 [REWRITE_TAC[hrat_lt] THEN DISCH_THEN(X_CHOOSE_TAC “d:hrat”) THEN
437 X_CHOOSE_TAC “x:hrat” (SPECL [“X:hreal”,
438 “d hrat_mul x0”] CUT_NEARTOP_ADD)
439 THEN EXISTS_TAC “x:hrat” THEN ASM_REWRITE_TAC[] THEN
440 FIRST_ASSUM(UNDISCH_TAC o assert is_eq o concl) THEN
441 DISCH_THEN SUBST_ALL_TAC THEN
442 RULE_ASSUM_TAC(REWRITE_RULE[HRAT_RDISTRIB, HRAT_MUL_LID]) THEN
443 REWRITE_TAC[HRAT_RDISTRIB, HRAT_MUL_LID] THEN
444 MATCH_MP_TAC CUT_UBOUND THEN
445 EXISTS_TAC “x hrat_add (d hrat_mul x0)” THEN ASM_REWRITE_TAC[] THEN
446 FIRST_ASSUM(MP_TAC
447 o MATCH_MP CUT_STRADDLE
448 o CONJ (ASSUME “(cut X)(x0 hrat_add (d hrat_mul x0))”)
449 o CONJUNCT2) THEN
450 REWRITE_TAC[HRAT_LT_RADD, HRAT_LT_LADD, HRAT_LT_LMUL],
451 DISCH_THEN(K ALL_TAC) THEN EXISTS_TAC “x0:hrat” THEN
452 ASM_REWRITE_TAC[]]
453QED
454
455(*---------------------------------------------------------------------------*)
456(* Define the operations. "hreal_lt" and "hreal_sub are convenient later *)
457(*---------------------------------------------------------------------------*)
458
459Definition hreal_1[nocompute]:
460 hreal_1 = hreal (cut_of_hrat hrat_1)
461End
462
463val hreal_add = new_infixl_definition("hreal_add",
464 “hreal_add X Y = hreal (\w. ?x y. (w = x hrat_add y) /\
465 (cut X) x /\ (cut Y) y)”, 500);
466
467val hreal_mul = new_infixl_definition("hreal_mul",
468 “hreal_mul X Y = hreal (\w. ?x y. (w = x hrat_mul y) /\
469 (cut X) x /\ (cut Y) y)”,600);
470
471Definition hreal_inv[nocompute]:
472 hreal_inv X = hreal (\w. ?d. (d hrat_lt hrat_1) /\
473 (!x. (cut X) x ==> ($hrat_mul w x) hrat_lt d))
474End
475
476Definition hreal_sup[nocompute]:
477 hreal_sup P = hreal (\w. ?X. (P X) /\ (cut X) w)
478End
479
480Definition hreal_lt[nocompute]:
481 hreal_lt X Y = ~(X = Y) /\ !x. (cut X) x ==> (cut Y) x
482End
483val _ = set_fixity "hreal_lt" (Infix(NONASSOC, 450))
484
485
486(*---------------------------------------------------------------------------*)
487(* Prove the appropriate closure properties of the basic operations *)
488(*---------------------------------------------------------------------------*)
489
490Theorem HREAL_INV_ISACUT:
491 !X. isacut (\w.
492 ?d. d hrat_lt hrat_1 /\ (!x. cut X x ==> (w hrat_mul x) hrat_lt d))
493Proof
494 GEN_TAC THEN REWRITE_TAC[isacut] THEN REPEAT CONJ_TAC THEN BETA_TAC THENL
495 [X_CHOOSE_TAC “d:hrat” (SPEC “hrat_1” HRAT_DOWN) THEN
496 X_CHOOSE_TAC “z:hrat” (SPEC “X:hreal” CUT_BOUNDED) THEN
497 MAP_EVERY EXISTS_TAC [“d hrat_mul (hrat_inv z)”, “d:hrat”] THEN
498 ASM_REWRITE_TAC[] THEN GEN_TAC THEN
499 DISCH_THEN(MP_TAC o MATCH_MP CUT_STRADDLE o
500 C CONJ (ASSUME “~(cut X z)”)) THEN
501 REWRITE_TAC[GSYM HRAT_MUL_ASSOC, HRAT_LT_RMUL1, HRAT_LT_L1],
502
503 X_CHOOSE_TAC “y:hrat” (SPEC “X:hreal” CUT_NONEMPTY) THEN
504 EXISTS_TAC “hrat_inv y” THEN CONV_TAC NOT_EXISTS_CONV THEN
505 GEN_TAC THEN
506 DISCH_THEN(CONJUNCTS_THEN2 MP_TAC (MP_TAC o SPEC “y:hrat”)) THEN
507 ASM_REWRITE_TAC[HRAT_MUL_LINV, HRAT_LT_GT],
508
509 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
510 (X_CHOOSE_THEN “d:hrat” STRIP_ASSUME_TAC) ASSUME_TAC) THEN
511 EXISTS_TAC “d:hrat” THEN ASM_REWRITE_TAC[] THEN
512 X_GEN_TAC “z:hrat” THEN
513 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
514 DISCH_TAC THEN MATCH_MP_TAC HRAT_LT_TRANS THEN
515 EXISTS_TAC “x hrat_mul z” THEN ASM_REWRITE_TAC[] THEN
516 ASM_REWRITE_TAC[HRAT_LT_RMUL],
517
518 GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN “d:hrat” STRIP_ASSUME_TAC) THEN
519 X_CHOOSE_THEN “e:hrat” STRIP_ASSUME_TAC
520 (MATCH_MP HRAT_MEAN (ASSUME “d hrat_lt hrat_1”)) THEN
521 EXISTS_TAC “(e hrat_mul x) hrat_mul (hrat_inv d)” THEN CONJ_TAC THENL
522 [EXISTS_TAC “e:hrat” THEN ASM_REWRITE_TAC[] THEN
523 X_GEN_TAC “z:hrat” THEN
524 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
525 REWRITE_TAC[GSYM HRAT_MUL_ASSOC, HRAT_LT_RMUL1] THEN
526 ONCE_REWRITE_TAC[AC(HRAT_MUL_ASSOC,HRAT_MUL_SYM)
527 “a hrat_mul (b hrat_mul c) = b hrat_mul (a hrat_mul c)”] THEN
528 REWRITE_TAC[HRAT_LT_L1],
529 ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
530 ASM_REWRITE_TAC[HRAT_MUL_ASSOC, HRAT_GT_LMUL1, HRAT_GT_L1]]]
531QED
532
533Theorem HREAL_ADD_ISACUT:
534 !X Y. isacut (\w. ?x y. (w = x hrat_add y) /\ cut X x /\ cut Y y)
535Proof
536 REPEAT GEN_TAC THEN REWRITE_TAC[isacut] THEN REPEAT CONJ_TAC THENL
537 [X_CHOOSE_TAC “x:hrat” (SPEC “X:hreal” CUT_NONEMPTY) THEN
538 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_NONEMPTY) THEN
539 EXISTS_TAC “x hrat_add y” THEN BETA_TAC THEN
540 MAP_EVERY EXISTS_TAC [“x:hrat”, “y:hrat”] THEN
541 ASM_REWRITE_TAC[],
542
543 X_CHOOSE_TAC “x:hrat” (SPEC “X:hreal” CUT_BOUNDED) THEN
544 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_BOUNDED) THEN
545 EXISTS_TAC “x hrat_add y” THEN BETA_TAC THEN
546 DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN [“u:hrat”, “v:hrat”])
547 (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
548 REWRITE_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
549 MATCH_MP_TAC HRAT_LT_NE THEN MATCH_MP_TAC HRAT_LT_ADD2 THEN
550 CONJ_TAC THEN MATCH_MP_TAC CUT_STRADDLE THENL
551 [EXISTS_TAC “X:hreal”, EXISTS_TAC “Y:hreal”] THEN
552 ASM_REWRITE_TAC[],
553
554 MAP_EVERY X_GEN_TAC [“w:hrat”, “z:hrat”] THEN BETA_TAC THEN
555 DISCH_THEN(CONJUNCTS_THEN2 (EVERY_TCL (map X_CHOOSE_THEN
556 [“u:hrat”, “v:hrat”]) STRIP_ASSUME_TAC) ASSUME_TAC) THEN
557 FIRST_ASSUM (UNDISCH_TAC o assert is_eq o concl) THEN
558 DISCH_THEN SUBST_ALL_TAC THEN
559 MAP_EVERY (fn tm => EXISTS_TAC “(z hrat_mul (hrat_inv (u hrat_add v)))
560 hrat_mul ^tm”)
561 [“u:hrat”, “v:hrat”]
562 THEN REWRITE_TAC[GSYM HRAT_LDISTRIB, GSYM HRAT_MUL_ASSOC,
563 HRAT_MUL_LINV, HRAT_MUL_RID] THEN
564 CONJ_TAC THEN MATCH_MP_TAC CUT_DOWN THENL
565 [EXISTS_TAC “u:hrat”, EXISTS_TAC “v:hrat”] THEN
566 ASM_REWRITE_TAC[HRAT_MUL_ASSOC, HRAT_LT_LMUL1, HRAT_LT_R1],
567
568 X_GEN_TAC “w:hrat” THEN BETA_TAC THEN
569 DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN [“x:hrat”, “y:hrat”])
570 (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC)) THEN
571 X_CHOOSE_TAC “u:hrat” (UNDISCH_ALL (SPECL [“X:hreal”,
572 “x:hrat”] CUT_UP))
573 THEN EXISTS_TAC “u hrat_add y” THEN CONJ_TAC THENL
574 [MAP_EVERY EXISTS_TAC [“u:hrat”, “y:hrat”], ALL_TAC] THEN
575 ASM_REWRITE_TAC[HRAT_LT_RADD]]
576QED
577
578Theorem HREAL_MUL_ISACUT:
579 !X Y. isacut (\w. ?x y. (w = x hrat_mul y) /\ cut X x /\ cut Y y)
580Proof
581 REPEAT GEN_TAC THEN REWRITE_TAC[isacut] THEN REPEAT CONJ_TAC THENL
582 [X_CHOOSE_TAC “x:hrat” (SPEC “X:hreal” CUT_NONEMPTY) THEN
583 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_NONEMPTY) THEN
584 EXISTS_TAC “x hrat_mul y” THEN BETA_TAC THEN
585 MAP_EVERY EXISTS_TAC [“x:hrat”, “y:hrat”] THEN
586 ASM_REWRITE_TAC[],
587
588 X_CHOOSE_TAC “x:hrat” (SPEC “X:hreal” CUT_BOUNDED) THEN
589 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_BOUNDED) THEN
590 EXISTS_TAC “x hrat_mul y” THEN BETA_TAC THEN
591 DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN [“u:hrat”, “v:hrat”])
592 (CONJUNCTS_THEN2 MP_TAC STRIP_ASSUME_TAC)) THEN
593 REWRITE_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
594 MATCH_MP_TAC HRAT_LT_NE THEN MATCH_MP_TAC HRAT_LT_MUL2 THEN
595 CONJ_TAC THEN MATCH_MP_TAC CUT_STRADDLE THENL
596 [EXISTS_TAC “X:hreal”, EXISTS_TAC “Y:hreal”] THEN
597 ASM_REWRITE_TAC[],
598
599 MAP_EVERY X_GEN_TAC [“w:hrat”, “z:hrat”] THEN BETA_TAC THEN
600 DISCH_THEN(CONJUNCTS_THEN2 (EVERY_TCL (map X_CHOOSE_THEN
601 [“u:hrat”, “v:hrat”]) STRIP_ASSUME_TAC) ASSUME_TAC) THEN
602 FIRST_ASSUM (UNDISCH_TAC o assert is_eq o concl) THEN
603 DISCH_THEN SUBST_ALL_TAC THEN EXISTS_TAC “u:hrat” THEN
604 EXISTS_TAC “v hrat_mul (z hrat_mul (hrat_inv (u hrat_mul v)))” THEN
605 ASM_REWRITE_TAC[HRAT_MUL_ASSOC] THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN
606 ONCE_REWRITE_TAC[HRAT_MUL_ASSOC] THEN
607 REWRITE_TAC[HRAT_MUL_LINV, HRAT_MUL_LID] THEN
608 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “v:hrat” THEN
609 ASM_REWRITE_TAC[] THEN
610 ONCE_REWRITE_TAC
611 [AC(HRAT_MUL_ASSOC,HRAT_MUL_SYM)
612 “(a hrat_mul b) hrat_mul c = (c hrat_mul a) hrat_mul b”]
613 THEN ASM_REWRITE_TAC[HRAT_LT_LMUL1, HRAT_LT_R1],
614
615 X_GEN_TAC “w:hrat” THEN BETA_TAC THEN
616 DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN [“x:hrat”, “y:hrat”])
617 (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC)) THEN
618 X_CHOOSE_TAC “u:hrat”
619 (UNDISCH_ALL (SPECL [“X:hreal”, “x:hrat”] CUT_UP))
620 THEN EXISTS_TAC “u hrat_mul y” THEN CONJ_TAC THENL
621 [MAP_EVERY EXISTS_TAC [“u:hrat”, “y:hrat”], ALL_TAC] THEN
622 ASM_REWRITE_TAC[HRAT_LT_RMUL]]
623QED
624
625(*---------------------------------------------------------------------------*)
626(* Now prove the various theorems about the new type *)
627(*---------------------------------------------------------------------------*)
628
629Theorem HREAL_ADD_SYM:
630 !X Y. X hreal_add Y = Y hreal_add X
631Proof
632 let val vars = [“a:hrat”, “b:hrat”] in
633 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_add] THEN AP_TERM_TAC THEN
634 CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN EQ_TAC THEN
635 DISCH_THEN((EVERY_TCL o map X_CHOOSE_THEN) vars ASSUME_TAC) THEN
636 MAP_EVERY EXISTS_TAC (rev vars) THEN ONCE_REWRITE_TAC[HRAT_ADD_SYM]
637 THEN ASM_REWRITE_TAC[] end
638QED
639
640Theorem HREAL_MUL_SYM:
641 !X Y. X hreal_mul Y = Y hreal_mul X
642Proof
643 let val vars = [“a:hrat”, “b:hrat”] in
644 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_mul] THEN AP_TERM_TAC THEN
645 CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN EQ_TAC THEN
646 DISCH_THEN((EVERY_TCL o map X_CHOOSE_THEN) vars ASSUME_TAC) THEN
647 MAP_EVERY EXISTS_TAC (rev vars) THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM]
648 THEN ASM_REWRITE_TAC[] end
649QED
650
651Theorem HREAL_ADD_ASSOC:
652 !X Y Z. X hreal_add (Y hreal_add Z) = (X hreal_add Y) hreal_add Z
653Proof
654 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_add] THEN AP_TERM_TAC THEN
655 CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN
656 REWRITE_TAC[REWRITE_RULE[hreal_tybij] HREAL_ADD_ISACUT] THEN BETA_TAC THEN
657 CONV_TAC(REDEPTH_CONV(LEFT_AND_EXISTS_CONV ORELSEC RIGHT_AND_EXISTS_CONV))
658 THEN EQ_TAC THEN
659 DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==))
660 ["u", "v", "x", "y"]) STRIP_ASSUME_TAC) THENL
661 [MAP_EVERY EXISTS_TAC [“u hrat_add x”, “y:hrat”,
662 “u:hrat”, “x:hrat”],
663 MAP_EVERY EXISTS_TAC [“x:hrat”, “y hrat_add v”,
664 “y:hrat”, “v:hrat”]]
665 THEN ASM_REWRITE_TAC[HRAT_ADD_ASSOC]
666QED
667
668Theorem HREAL_MUL_ASSOC:
669 !X Y Z. X hreal_mul (Y hreal_mul Z) = (X hreal_mul Y) hreal_mul Z
670Proof
671 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_mul] THEN AP_TERM_TAC THEN
672 CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN
673 REWRITE_TAC[REWRITE_RULE[hreal_tybij] HREAL_MUL_ISACUT] THEN BETA_TAC THEN
674 CONV_TAC(REDEPTH_CONV(LEFT_AND_EXISTS_CONV ORELSEC RIGHT_AND_EXISTS_CONV))
675 THEN EQ_TAC THEN
676 DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==))
677 ["u", "v", "x", "y"]) STRIP_ASSUME_TAC) THENL
678 [MAP_EVERY EXISTS_TAC [“u hrat_mul x”, “y:hrat”,
679 “u:hrat”, “x:hrat”],
680 MAP_EVERY EXISTS_TAC [“x:hrat”, “y hrat_mul v”,
681 “y:hrat”, “v:hrat”]]
682 THEN ASM_REWRITE_TAC[HRAT_MUL_ASSOC]
683QED
684
685Theorem HREAL_LDISTRIB:
686 !X Y Z. X hreal_mul (Y hreal_add Z) =
687 (X hreal_mul Y) hreal_add (X hreal_mul Z)
688Proof
689 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_mul, hreal_add] THEN AP_TERM_TAC THEN
690 CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN BETA_TAC THEN
691 (REWRITE_TAC o map (REWRITE_RULE[hreal_tybij]))
692 [HREAL_MUL_ISACUT, HREAL_ADD_ISACUT] THEN BETA_TAC THEN
693 CONV_TAC(REDEPTH_CONV(LEFT_AND_EXISTS_CONV ORELSEC RIGHT_AND_EXISTS_CONV))
694 THEN EQ_TAC THENL
695 [DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==))
696 ["a", "b", "c", "d"]) STRIP_ASSUME_TAC) THEN
697 MAP_EVERY EXISTS_TAC [“a hrat_mul c”, “a hrat_mul d”,
698 “a:hrat”, “c:hrat”, “a:hrat”, “d:hrat”] THEN
699 ASM_REWRITE_TAC[HRAT_LDISTRIB],
700 DISCH_THEN(EVERY_TCL (map (X_CHOOSE_THEN o C (curry mk_var) (==`:hrat`==))
701 ["a", "b", "c", "d", "e", "f"]) STRIP_ASSUME_TAC) THEN
702 REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
703 (SPECL [“c:hrat”, “e:hrat”] HRAT_LT_TOTAL) THENL
704 [MAP_EVERY EXISTS_TAC [“e:hrat”, “d hrat_add f”,
705 “d:hrat”, “f:hrat”] THEN
706 ASM_REWRITE_TAC[HRAT_LDISTRIB],
707
708 MAP_EVERY EXISTS_TAC [“e:hrat”,
709 “((hrat_inv e) hrat_mul (c hrat_mul d)) hrat_add f”,
710 “(hrat_inv e) hrat_mul (c hrat_mul d)”, “f:hrat”] THEN
711 ASM_REWRITE_TAC
712 [HRAT_LDISTRIB, HRAT_MUL_ASSOC, HRAT_MUL_RINV, HRAT_MUL_LID] THEN
713 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “d:hrat” THEN
714 ASM_REWRITE_TAC[HRAT_LT_LMUL1, HRAT_LT_L1],
715
716 MAP_EVERY EXISTS_TAC [“c:hrat”,
717 “d hrat_add ((hrat_inv c) hrat_mul (e hrat_mul f))”,
718 “d:hrat”, “(hrat_inv c) hrat_mul (e hrat_mul f)”] THEN
719 ASM_REWRITE_TAC
720 [HRAT_LDISTRIB, HRAT_MUL_ASSOC, HRAT_MUL_RINV, HRAT_MUL_LID] THEN
721 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “f:hrat” THEN
722 ASM_REWRITE_TAC[HRAT_LT_LMUL1, HRAT_LT_L1]]]
723QED
724
725Theorem HREAL_MUL_LID:
726 !X. hreal_1 hreal_mul X = X
727Proof
728 GEN_TAC THEN REWRITE_TAC[hreal_1, hreal_mul] THEN
729 MATCH_MP_TAC EQUAL_CUTS THEN
730 REWRITE_TAC[REWRITE_RULE[hreal_tybij] HREAL_MUL_ISACUT] THEN
731 REWRITE_TAC[REWRITE_RULE[hreal_tybij] ISACUT_HRAT] THEN
732 REWRITE_TAC[cut_of_hrat] THEN BETA_TAC THEN
733 CONV_TAC(X_FUN_EQ_CONV “w:hrat”) THEN GEN_TAC THEN BETA_TAC THEN
734 EQ_TAC THENL
735 [DISCH_THEN(REPEAT_TCL CHOOSE_THEN
736 (CONJUNCTS_THEN2 SUBST1_TAC STRIP_ASSUME_TAC)) THEN
737 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “y:hrat” THEN
738 ASM_REWRITE_TAC[HRAT_LT_LMUL1],
739 DISCH_THEN(X_CHOOSE_THEN “v:hrat” STRIP_ASSUME_TAC o MATCH_MP CUT_UP)
740 THEN MAP_EVERY EXISTS_TAC [“w hrat_mul (hrat_inv v)”,“v:hrat”]
741 THEN ASM_REWRITE_TAC[GSYM HRAT_MUL_ASSOC, HRAT_MUL_LINV, HRAT_MUL_RID]
742 THEN ONCE_REWRITE_TAC[HRAT_MUL_SYM] THEN ASM_REWRITE_TAC[HRAT_LT_L1]]
743QED
744
745Theorem HREAL_MUL_LINV:
746 !X. (hreal_inv X) hreal_mul X = hreal_1
747Proof
748 GEN_TAC THEN REWRITE_TAC[hreal_inv, hreal_mul, hreal_1] THEN
749 REWRITE_TAC[REWRITE_RULE[hreal_tybij] HREAL_INV_ISACUT] THEN
750 AP_TERM_TAC THEN REWRITE_TAC[cut_of_hrat] THEN
751 CONV_TAC(X_FUN_EQ_CONV “z:hrat”) THEN BETA_TAC THEN GEN_TAC THEN
752 EQ_TAC THENL
753 [DISCH_THEN STRIP_ASSUME_TAC THEN
754 FIRST_ASSUM(ASSUME_TAC o C MATCH_MP (ASSUME “cut X y”)) THEN
755 MATCH_MP_TAC HRAT_LT_TRANS THEN EXISTS_TAC “d:hrat” THEN
756 ASM_REWRITE_TAC[],
757
758 DISCH_THEN(X_CHOOSE_THEN “d:hrat” (CONJUNCTS_THEN2 (MP_TAC o
759 ONCE_REWRITE_RULE[GSYM HRAT_GT_L1]) ASSUME_TAC) o MATCH_MP HRAT_MEAN)
760 THEN DISCH_THEN(X_CHOOSE_TAC “x:hrat” o
761 SPEC “X:hreal” o MATCH_MP CUT_NEARTOP_MUL) THEN
762 MAP_EVERY EXISTS_TAC [“z hrat_mul (hrat_inv x)”, “x:hrat”] THEN
763(* begin change *)
764 GEN_REWR_TAC (LAND_CONV o RAND_CONV) [GSYM HRAT_MUL_ASSOC]
765 THEN ASM_REWRITE_TAC[HRAT_MUL_LINV, HRAT_MUL_RID] THEN
766(* end change *)
767(* Rewriting change forces change in proof
768 * ASM_REWRITE_TAC[GSYM HRAT_MUL_ASSOC, HRAT_MUL_LINV, HRAT_MUL_RID] THEN
769 *)
770 EXISTS_TAC “d:hrat” THEN ASM_REWRITE_TAC[] THEN
771 X_GEN_TAC “y:hrat” THEN
772 FIRST_ASSUM(UNDISCH_TAC o assert is_conj o concl) THEN
773 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o C CONJ (CONJUNCT2 th))) THEN
774 DISCH_THEN(MP_TAC o MATCH_MP CUT_STRADDLE) THEN
775 SUBST1_TAC(SYM(SPECL [“y:hrat”,
776 “((hrat_inv z) hrat_mul d) hrat_mul x”,
777 “z hrat_mul (hrat_inv x)”] HRAT_LT_LMUL)) THEN
778 ONCE_REWRITE_TAC[AC(HRAT_MUL_ASSOC,HRAT_MUL_SYM)
779 “(a hrat_mul b) hrat_mul ((c hrat_mul d) hrat_mul e) =
780 ((c hrat_mul a) hrat_mul (b hrat_mul e)) hrat_mul d”]
781 THEN REWRITE_TAC[HRAT_MUL_LINV, HRAT_MUL_LID]]
782QED
783
784Theorem HREAL_NOZERO:
785 !X Y. ~(X hreal_add Y = X)
786Proof
787 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_add] THEN
788 DISCH_THEN(MP_TAC o AP_TERM “cut”) THEN
789 REWRITE_TAC[REWRITE_RULE[hreal_tybij] HREAL_ADD_ISACUT] THEN
790 DISCH_THEN(MP_TAC o CONV_RULE (X_FUN_EQ_CONV “w:hrat”)) THEN
791 REWRITE_TAC[] THEN CONV_TAC NOT_FORALL_CONV THEN BETA_TAC THEN
792 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_NONEMPTY) THEN
793 X_CHOOSE_TAC “x:hrat”
794 (SPECL [“X:hreal”, “y:hrat”] CUT_NEARTOP_ADD) THEN
795 EXISTS_TAC “x hrat_add y” THEN ASM_REWRITE_TAC[] THEN
796 MAP_EVERY EXISTS_TAC [“x:hrat”, “y:hrat”] THEN
797 ASM_REWRITE_TAC[]
798QED
799
800(*---------------------------------------------------------------------------*)
801(* Need a sequence of lemmas for totality of addition; it's convenient *)
802(* to define a "subtraction" function and prove its closure *)
803(*---------------------------------------------------------------------------*)
804
805val hreal_sub = new_infixl_definition("hreal_sub",
806“hreal_sub Y X = hreal (\w. ?x. ~((cut X) x) /\ (cut Y) ($hrat_add x w))”,
807 500);
808
809Theorem HREAL_LT_LEMMA:
810 !X Y. X hreal_lt Y ==> ?x. ~(cut X x) /\ (cut Y x)
811Proof
812 let val lemma1 = TAUT_CONV “~(~a /\ b) = b ==> a”
813 val lemma2 = TAUT_CONV “(a ==> b) /\ (b ==> a) = (a = b)”
814 in
815 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN
816 CONV_TAC(LAND_CONV NOT_EXISTS_CONV) THEN
817 REWRITE_TAC[hreal_lt, lemma1] THEN
818 DISCH_THEN(fn th => DISCH_THEN(MP_TAC o C CONJ th)) THEN
819 CONV_TAC(LAND_CONV AND_FORALL_CONV) THEN
820 REWRITE_TAC[lemma2] THEN CONV_TAC(LAND_CONV EXT_CONV) THEN
821 DISCH_THEN(MP_TAC o AP_TERM “hreal”) THEN REWRITE_TAC[hreal_tybij]
822 end
823QED
824
825Theorem HREAL_SUB_ISACUT:
826 !X Y. X hreal_lt Y ==> isacut(\w. ?x. ~cut X x /\ cut Y(x hrat_add w))
827Proof
828 REPEAT GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[isacut] THEN
829 BETA_TAC THEN REPEAT CONJ_TAC THENL
830 [FIRST_ASSUM(X_CHOOSE_TAC “y:hrat” o MATCH_MP HREAL_LT_LEMMA) THEN
831 FIRST_ASSUM(X_CHOOSE_THEN “z:hrat” MP_TAC
832 o MATCH_MP (SPECL [“Y:hreal”, “y:hrat”] CUT_UP)
833 o CONJUNCT2) THEN
834 REWRITE_TAC[hrat_lt] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
835 (X_CHOOSE_THEN “x:hrat” SUBST_ALL_TAC)) THEN
836 MAP_EVERY EXISTS_TAC [“x:hrat”, “y:hrat”] THEN
837 ASM_REWRITE_TAC[],
838
839 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_BOUNDED) THEN
840 EXISTS_TAC “y:hrat” THEN CONV_TAC NOT_EXISTS_CONV THEN
841 X_GEN_TAC “d:hrat” THEN REWRITE_TAC[DE_MORGAN_THM] THEN
842 DISJ2_TAC THEN MATCH_MP_TAC CUT_UBOUND THEN EXISTS_TAC “y:hrat” THEN
843 ASM_REWRITE_TAC[HRAT_LT_ADDR],
844
845 REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
846 (X_CHOOSE_THEN “z:hrat” STRIP_ASSUME_TAC) ASSUME_TAC) THEN
847 EXISTS_TAC “z:hrat” THEN ASM_REWRITE_TAC[] THEN
848 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “z hrat_add x” THEN
849 ASM_REWRITE_TAC[HRAT_LT_LADD],
850
851 GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN “z:hrat” STRIP_ASSUME_TAC) THEN
852 FIRST_ASSUM(X_CHOOSE_THEN “w:hrat” MP_TAC o MATCH_MP
853 (SPECL [“Y:hreal”, “z hrat_add x”] CUT_UP)) THEN
854 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
855 (X_CHOOSE_THEN “d:hrat” SUBST_ALL_TAC) o REWRITE_RULE[hrat_lt]) THEN
856 EXISTS_TAC “x hrat_add d” THEN REWRITE_TAC[HRAT_LT_ADDL] THEN
857 EXISTS_TAC “z:hrat” THEN ASM_REWRITE_TAC[HRAT_ADD_ASSOC]]
858QED
859
860Theorem HREAL_SUB_ADD:
861 !X Y. X hreal_lt Y ==> ((Y hreal_sub X) hreal_add X = Y)
862Proof
863 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_add, hreal_sub] THEN
864 DISCH_TAC THEN MATCH_MP_TAC EQUAL_CUTS THEN
865 REWRITE_TAC[REWRITE_RULE[hreal_tybij] HREAL_ADD_ISACUT] THEN
866 FIRST_ASSUM(fn th => REWRITE_TAC[REWRITE_RULE[hreal_tybij]
867 (MATCH_MP HREAL_SUB_ISACUT th)]) THEN
868 CONV_TAC (X_FUN_EQ_CONV “w:hrat”) THEN BETA_TAC THEN GEN_TAC THEN
869 EQ_TAC THENL
870 [DISCH_THEN(REPEAT_TCL CHOOSE_THEN(CONJUNCTS_THEN2 MP_TAC (CONJUNCTS_THEN2
871 (X_CHOOSE_THEN “z:hrat” STRIP_ASSUME_TAC) ASSUME_TAC))) THEN
872 DISCH_THEN SUBST1_TAC THEN MATCH_MP_TAC CUT_DOWN THEN
873 EXISTS_TAC “z hrat_add x” THEN ASM_REWRITE_TAC[] THEN
874 GEN_REWR_TAC RAND_CONV [HRAT_ADD_SYM] THEN
875 REWRITE_TAC[HRAT_LT_LADD] THEN MATCH_MP_TAC CUT_STRADDLE THEN
876 EXISTS_TAC “X:hreal” THEN ASM_REWRITE_TAC[],
877
878 DISCH_TAC THEN ASM_CASES_TAC “(cut X) w” THENL
879 [FIRST_ASSUM (X_CHOOSE_THEN “z:hrat” MP_TAC o MATCH_MP
880 (SPECL [“X:hreal”, “Y:hreal”] HREAL_LT_LEMMA)) THEN
881 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
882 (X_CHOOSE_THEN “k:hrat” (CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) o
883 MATCH_MP CUT_UP)) THEN REWRITE_TAC[hrat_lt] THEN
884 DISCH_THEN(X_CHOOSE_THEN “e:hrat” SUBST_ALL_TAC) THEN
885 X_CHOOSE_THEN “x:hrat”
886 MP_TAC (SPECL[“e:hrat”, “w:hrat”] HRAT_DOWN2) THEN
887 SUBST1_TAC(SYM(SPECL [“x:hrat”, “e:hrat”,
888 “z:hrat”] HRAT_LT_LADD)) THEN
889 DISCH_THEN(CONJUNCTS_THEN2 (ASSUME_TAC o MATCH_MP CUT_DOWN o
890 CONJ (ASSUME “cut Y(z hrat_add e)”)) MP_TAC) THEN
891 REWRITE_TAC[hrat_lt] THEN DISCH_THEN(X_CHOOSE_TAC “y:hrat”) THEN
892 MAP_EVERY EXISTS_TAC [“x:hrat”, “y:hrat”] THEN ASM_REWRITE_TAC[]
893 THEN CONJ_TAC THENL
894 [EXISTS_TAC “z:hrat” THEN ASM_REWRITE_TAC[],
895 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “w:hrat” THEN
896 ASM_REWRITE_TAC[HRAT_LT_ADDR]],
897
898 FIRST_ASSUM(X_CHOOSE_THEN “k:hrat” MP_TAC o MATCH_MP CUT_UP) THEN
899 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[hrat_lt]
900 THEN DISCH_THEN(X_CHOOSE_THEN “e:hrat” SUBST_ALL_TAC) THEN
901 X_CHOOSE_THEN “y:hrat” STRIP_ASSUME_TAC
902 (SPECL [“X:hreal”, “e:hrat”] CUT_NEARTOP_ADD) THEN
903 ASM_CASES_TAC “(cut Y) (y hrat_add e)” THENL
904 [SUBGOAL_THEN “y hrat_lt w” MP_TAC THENL
905 [MATCH_MP_TAC CUT_STRADDLE THEN EXISTS_TAC “X:hreal” THEN
906 ASM_REWRITE_TAC[], ALL_TAC] THEN REWRITE_TAC[hrat_lt] THEN
907 DISCH_THEN(X_CHOOSE_THEN “x:hrat” SUBST_ALL_TAC) THEN
908 MAP_EVERY EXISTS_TAC [“x:hrat”, “y:hrat”] THEN
909 REPEAT CONJ_TAC THENL
910 [MATCH_ACCEPT_TAC HRAT_ADD_SYM,
911 EXISTS_TAC “y hrat_add e” THEN
912 ONCE_REWRITE_TAC[AC(HRAT_ADD_ASSOC,HRAT_ADD_SYM)
913 “(a hrat_add b) hrat_add c = (a hrat_add c) hrat_add b”] THEN
914 ASM_REWRITE_TAC[],
915 FIRST_ASSUM ACCEPT_TAC],
916
917 UNDISCH_TAC “cut X y” THEN CONV_TAC CONTRAPOS_CONV THEN
918 DISCH_THEN(K ALL_TAC) THEN MATCH_MP_TAC CUT_UBOUND THEN
919 EXISTS_TAC “w:hrat” THEN ASM_REWRITE_TAC[] THEN
920 SUBST1_TAC(SYM(SPECL [“w:hrat”, “y:hrat”, “e:hrat”] HRAT_LT_RADD)) THEN
921 MATCH_MP_TAC CUT_STRADDLE THEN EXISTS_TAC “Y:hreal” THEN
922 ASM_REWRITE_TAC[]]]]
923QED
924
925Theorem HREAL_LT_TOTAL:
926 !X Y. (X = Y) \/ (X hreal_lt Y) \/ (Y hreal_lt X)
927Proof
928 let val lemma = TAUT_CONV “a \/ (~a /\ b) \/ (~a /\ c) = ~b /\ ~c ==> a”
929 val negneg = TAUT_CONV “a = ~(~a)” in
930 REPEAT GEN_TAC THEN REWRITE_TAC[hreal_lt] THEN
931 SUBST1_TAC(ISPECL[“Y:hreal”, “X:hreal”] EQ_SYM_EQ) THEN
932 REWRITE_TAC[lemma] THEN CONV_TAC CONTRAPOS_CONV THEN
933 DISCH_THEN(MP_TAC o MATCH_MP(CONTRAPOS(SPEC_ALL EQUAL_CUTS))) THEN
934 CONV_TAC(ONCE_DEPTH_CONV(X_FUN_EQ_CONV “x:hrat”)) THEN
935 DISCH_THEN(X_CHOOSE_THEN “z:hrat” MP_TAC o CONV_RULE NOT_FORALL_CONV) THEN
936 ASM_CASES_TAC “cut X z” THEN ASM_REWRITE_TAC[DE_MORGAN_THM] THEN DISCH_TAC
937 THENL [DISJ2_TAC, DISJ1_TAC] THEN
938 GEN_REWR_TAC I [negneg] THEN
939 DISCH_THEN(X_CHOOSE_THEN “w:hrat” MP_TAC o CONV_RULE NOT_FORALL_CONV) THEN
940 REWRITE_TAC[] THEN DISCH_THEN(fn th =>
941 FIRST_ASSUM(ASSUME_TAC o MATCH_MP CUT_STRADDLE o CONJ th)) THEN
942 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “z:hrat” THEN ASM_REWRITE_TAC[] end
943QED
944
945Theorem HREAL_LT:
946 !X Y. X hreal_lt Y = ?D. Y = X hreal_add D
947Proof
948 REPEAT GEN_TAC THEN EQ_TAC THENL
949 [DISCH_THEN(curry op THEN (EXISTS_TAC “Y hreal_sub X”) o MP_TAC) THEN
950 DISCH_THEN(CONV_TAC o (LAND_CONV o REWR_CONV) o
951 SYM o MATCH_MP HREAL_SUB_ADD) THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM,
952 DISCH_THEN(X_CHOOSE_THEN “D:hreal” SUBST_ALL_TAC) THEN
953 REWRITE_TAC[hreal_lt, NOT_EQ_SYM(SPEC_ALL HREAL_NOZERO)] THEN
954 X_GEN_TAC “x:hrat” THEN DISCH_TAC THEN
955 X_CHOOSE_TAC “e:hrat” (SPEC “D:hreal” CUT_NONEMPTY) THEN
956 X_CHOOSE_THEN “d:hrat” MP_TAC (SPECL [“x:hrat”, “e:hrat”] HRAT_DOWN2) THEN
957 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC “w:hrat” o REWRITE_RULE[hrat_lt])
958 (ASSUME_TAC o MATCH_MP CUT_DOWN o CONJ (ASSUME “cut D e”))) THEN
959 REWRITE_TAC[hreal_add, REWRITE_RULE[hreal_tybij] HREAL_ADD_ISACUT] THEN
960 BETA_TAC THEN MAP_EVERY EXISTS_TAC [“w:hrat”, “d:hrat”] THEN
961 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
962 [MATCH_ACCEPT_TAC HRAT_ADD_SYM,
963 MATCH_MP_TAC CUT_DOWN THEN EXISTS_TAC “x:hrat” THEN
964 ASM_REWRITE_TAC[HRAT_LT_ADDR]]]
965QED
966
967Theorem HREAL_ADD_TOTAL:
968 !X Y. (X = Y) \/ (?D. Y = X hreal_add D) \/ (?D. X = Y hreal_add D)
969Proof
970 REPEAT GEN_TAC THEN REWRITE_TAC[SYM(SPEC_ALL HREAL_LT)] THEN
971 MATCH_ACCEPT_TAC HREAL_LT_TOTAL
972QED
973
974(*---------------------------------------------------------------------------*)
975(* Now prove the supremum property *)
976(*---------------------------------------------------------------------------*)
977
978Theorem HREAL_SUP_ISACUT:
979 !P. (?X:hreal. P X) /\ (?Y. (!X. P X ==> X hreal_lt Y))
980 ==> isacut (\w. ?X. P X /\ cut X w)
981Proof
982 let val lemma = TAUT_CONV “~(a /\ b) = (a ==> ~b)” in
983 GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN CHOOSE_TAC) THEN
984 REWRITE_TAC[isacut] THEN BETA_TAC THEN REPEAT CONJ_TAC THENL
985 [X_CHOOSE_TAC “x:hrat” (SPEC “X:hreal” CUT_NONEMPTY) THEN
986 MAP_EVERY EXISTS_TAC [“x:hrat”, “X:hreal”] THEN ASM_REWRITE_TAC[],
987
988 X_CHOOSE_TAC “y:hrat” (SPEC “Y:hreal” CUT_BOUNDED) THEN
989 EXISTS_TAC “y:hrat” THEN CONV_TAC NOT_EXISTS_CONV THEN
990 X_GEN_TAC “Z:hreal” THEN REWRITE_TAC[lemma] THEN
991 DISCH_THEN(fn th => FIRST_ASSUM(MP_TAC o C MATCH_MP th)) THEN
992 REWRITE_TAC[hreal_lt] THEN
993 DISCH_THEN(MP_TAC o SPEC “y:hrat” o CONJUNCT2) THEN ASM_REWRITE_TAC[],
994
995 REPEAT GEN_TAC THEN
996 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC “Z:hreal”) ASSUME_TAC) THEN
997 EXISTS_TAC “Z:hreal” THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC CUT_DOWN THEN
998 EXISTS_TAC “x:hrat” THEN ASM_REWRITE_TAC[],
999
1000 GEN_TAC THEN DISCH_THEN(X_CHOOSE_THEN “Z:hreal” STRIP_ASSUME_TAC) THEN
1001 FIRST_ASSUM(X_CHOOSE_TAC “y:hrat” o MATCH_MP
1002 (SPECL [“Z:hreal”, “x:hrat”] CUT_UP)) THEN
1003 EXISTS_TAC “y:hrat” THEN ASM_REWRITE_TAC[] THEN
1004 EXISTS_TAC “Z:hreal” THEN ASM_REWRITE_TAC[]] end
1005QED
1006
1007Theorem HREAL_SUP:
1008 !P. (?X. P X) /\ (?Y. (!X. P X ==> X hreal_lt Y)) ==>
1009 (!Y. (?X. P X /\ Y hreal_lt X) = Y hreal_lt (hreal_sup P))
1010Proof
1011 let val stac = FIRST_ASSUM(SUBST1_TAC o MATCH_MP
1012 (REWRITE_RULE[hreal_tybij] HREAL_SUP_ISACUT)) in
1013 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL
1014 [REWRITE_TAC[hreal_sup, hreal_lt] THEN stac THEN
1015 REWRITE_TAC[GSYM hreal_lt] THEN BETA_TAC THENL
1016 [DISCH_THEN(X_CHOOSE_THEN “X:hreal” STRIP_ASSUME_TAC) THEN
1017 CONJ_TAC THENL
1018 [DISCH_THEN(MP_TAC o AP_TERM “cut”) THEN stac THEN
1019 DISCH_THEN(MP_TAC o CONV_RULE (X_FUN_EQ_CONV “x:hrat”)) THEN
1020 BETA_TAC THEN REWRITE_TAC[] THEN CONV_TAC NOT_FORALL_CONV THEN
1021 FIRST_ASSUM(X_CHOOSE_TAC “x:hrat” o MATCH_MP HREAL_LT_LEMMA) THEN
1022 EXISTS_TAC “x:hrat” THEN ASM_REWRITE_TAC[] THEN
1023 EXISTS_TAC “X:hreal” THEN ASM_REWRITE_TAC[],
1024 X_GEN_TAC “x:hrat” THEN DISCH_THEN(ASSUME_TAC o MATCH_MP
1025 (CONJUNCT2(REWRITE_RULE[hreal_lt] (ASSUME “Y hreal_lt X”)))) THEN
1026 EXISTS_TAC “X:hreal” THEN ASM_REWRITE_TAC[]]],
1027 DISCH_THEN(X_CHOOSE_THEN “x:hrat” MP_TAC o MATCH_MP HREAL_LT_LEMMA) THEN
1028 REWRITE_TAC[hreal_sup] THEN stac THEN BETA_TAC THEN
1029 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC (X_CHOOSE_TAC “X:hreal”)) THEN
1030 EXISTS_TAC “X:hreal” THEN ASM_REWRITE_TAC[] THEN
1031 REPEAT_TCL DISJ_CASES_THEN (fn th => SUBST_ALL_TAC th ORELSE ASSUME_TAC th)
1032 (SPECL [“X:hreal”, “Y:hreal”] HREAL_LT_TOTAL) THEN
1033 ASM_REWRITE_TAC[] THENL
1034 [FIRST_ASSUM(SUBST_ALL_TAC o EQT_INTRO o CONJUNCT2) THEN
1035 RULE_ASSUM_TAC(REWRITE_RULE[]) THEN FIRST_ASSUM CONTR_TAC,
1036 MP_TAC (CONJUNCT2 (REWRITE_RULE[hreal_lt] (ASSUME “X hreal_lt Y”))) THEN
1037 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
1038 CONV_TAC NOT_FORALL_CONV THEN EXISTS_TAC “x:hrat” THEN
1039 ASM_REWRITE_TAC[]]] end
1040QED
1041
1042(*---------------------------------------------------------------------------*)
1043(* Required lemmas about the halfreals - mostly to drive CANCEL_TAC *)
1044(*---------------------------------------------------------------------------*)
1045
1046Theorem HREAL_RDISTRIB:
1047 !x y z. (x hreal_add y) hreal_mul z =
1048 (x hreal_mul z) hreal_add (y hreal_mul z)
1049Proof
1050 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN
1051 MATCH_ACCEPT_TAC HREAL_LDISTRIB
1052QED
1053
1054Theorem HREAL_EQ_ADDR:
1055 !x y. ~(x hreal_add y = x)
1056Proof
1057 REPEAT GEN_TAC THEN MATCH_ACCEPT_TAC HREAL_NOZERO
1058QED
1059
1060Theorem HREAL_EQ_ADDL:
1061 !x y. ~(x = x hreal_add y)
1062Proof
1063 REPEAT GEN_TAC THEN CONV_TAC(RAND_CONV SYM_CONV) THEN
1064 MATCH_ACCEPT_TAC HREAL_EQ_ADDR
1065QED
1066
1067Theorem HREAL_EQ_LADD:
1068 !x y z. (x hreal_add y = x hreal_add z) = (y = z)
1069Proof
1070 REPEAT GEN_TAC THEN EQ_TAC THENL
1071 [REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
1072 (SPECL [“y:hreal”, “z:hreal”] HREAL_ADD_TOTAL) THENL
1073 [DISCH_THEN(K ALL_TAC) THEN POP_ASSUM ACCEPT_TAC, ALL_TAC, ALL_TAC] THEN
1074 POP_ASSUM(X_CHOOSE_THEN “d:hreal” SUBST1_TAC) THEN
1075 REWRITE_TAC[HREAL_ADD_ASSOC, HREAL_EQ_ADDR, HREAL_EQ_ADDL],
1076 DISCH_THEN SUBST1_TAC THEN REFL_TAC]
1077QED
1078
1079Theorem HREAL_LT_REFL:
1080 !x. ~(x hreal_lt x)
1081Proof
1082 GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN
1083 REWRITE_TAC[HREAL_EQ_ADDL]
1084QED
1085
1086Theorem HREAL_LT_ADDL:
1087 !x y. x hreal_lt (x hreal_add y)
1088Proof
1089 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN
1090 EXISTS_TAC “y:hreal” THEN REFL_TAC
1091QED
1092
1093Theorem HREAL_LT_NE:
1094 !x y. x hreal_lt y ==> ~(x = y)
1095Proof
1096 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN
1097 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
1098 MATCH_ACCEPT_TAC HREAL_EQ_ADDL
1099QED
1100
1101Theorem HREAL_LT_ADDR:
1102 !x y. ~((x hreal_add y) hreal_lt x)
1103Proof
1104 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN
1105 REWRITE_TAC[GSYM HREAL_ADD_ASSOC, HREAL_EQ_ADDL]
1106QED
1107
1108Theorem HREAL_LT_GT:
1109 !x y. x hreal_lt y ==> ~(y hreal_lt x)
1110Proof
1111 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN
1112 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
1113 REWRITE_TAC[GSYM HREAL_ADD_ASSOC, HREAL_EQ_ADDL]
1114QED
1115
1116Theorem HREAL_LT_ADD2:
1117 !x1 x2 y1 y2. x1 hreal_lt y1 /\ x2 hreal_lt y2 ==>
1118 (x1 hreal_add x2) hreal_lt (y1 hreal_add y2)
1119Proof
1120 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN
1121 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_THEN “d1:hreal” SUBST1_TAC)
1122 (X_CHOOSE_THEN “d2:hreal” SUBST1_TAC)) THEN
1123 EXISTS_TAC “d1 hreal_add d2” THEN
1124 CONV_TAC(AC_CONV(HREAL_ADD_ASSOC,HREAL_ADD_SYM))
1125QED
1126
1127Theorem HREAL_LT_LADD:
1128 !x y z. (x hreal_add y) hreal_lt (x hreal_add z) = y hreal_lt z
1129Proof
1130 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LT] THEN EQ_TAC THEN
1131 DISCH_THEN(X_CHOOSE_THEN “d:hreal” (curry op THEN (EXISTS_TAC “d:hreal”) o MP_TAC))
1132 THEN REWRITE_TAC[GSYM HREAL_ADD_ASSOC, HREAL_EQ_LADD]
1133QED
1134
1135(*---------------------------------------------------------------------------*)
1136(* CANCEL_CONV - Try to cancel, rearranging using AC laws as needed *)
1137(* *)
1138(* The first two arguments are the associative and commutative laws, as *)
1139(* given to AC_CONV. The remaining list of theorems should be of the form: *)
1140(* *)
1141(* |- (a & b ~ a & c) = w (e.g. b ~ c) *)
1142(* |- (a & b ~ a) = x (e.g. F) *)
1143(* |- (a ~ a & c) = y (e.g. T) *)
1144(* |- (a ~ a) = z (e.g. F) *)
1145(* *)
1146(* For some operator (written as infix &) and relation (~). *)
1147(* *)
1148(* Theorems may be of the form |- ~ P or |- P, rather that equations; they *)
1149(* will be transformed to |- P = F and |- P = T automatically if needed. *)
1150(* *)
1151(* Note that terms not cancelled will remain in their original order, but *)
1152(* will be flattened to right-associated form. *)
1153(*---------------------------------------------------------------------------*)
1154
1155fun intro th =
1156 if is_eq(concl th) then th else
1157 if is_neg(concl th) then EQF_INTRO th
1158 else EQT_INTRO th;
1159
1160val lhs_rator2 = rator o rator o lhs o snd o strip_forall o concl;
1161
1162fun rmel i list =
1163 case list of
1164 [] => []
1165 | h::t => if aconv h i then t else h :: rmel i t
1166
1167fun ERR s = mk_HOL_ERR "realaxScript" "CANCEL_CONV"s
1168
1169fun CANCEL_CONV(assoc,sym,lcancelthms) tm =
1170 let val lcthms = map (intro o SPEC_ALL) lcancelthms
1171 val eqop = lhs_rator2 (Lib.trye hd lcthms)
1172 val binop = lhs_rator2 sym
1173 fun strip_binop tm =
1174 if (rator(rator tm) ~~ binop handle HOL_ERR _ => false)
1175 then strip_binop (rand(rator tm)) @ strip_binop(rand tm)
1176 else [tm]
1177 val mk_binop = curry mk_comb o curry mk_comb binop
1178 val list_mk_binop = end_itlist mk_binop
1179 val (c,alist) = strip_comb tm
1180 val _ = assert (aconv eqop) c
1181 in
1182 case alist of
1183 [l1,r1] => let
1184 val l = strip_binop l1
1185 and r = strip_binop r1
1186 val i = op_intersect aconv l r
1187 in
1188 if null i then raise ERR "unchanged"
1189 else let
1190 val itm = list_mk_binop i
1191 val l' = end_itlist (C (curry op o)) (map rmel i) l
1192 and r' = end_itlist (C (curry op o)) (map rmel i) r
1193 fun mk ts = mk_binop itm (list_mk_binop ts)
1194 handle HOL_ERR _ => itm
1195 val l2 = mk l'
1196 val r2 = mk r'
1197 val le = (EQT_ELIM o AC_CONV(assoc,sym) o mk_eq) (l1,l2)
1198 val re = (EQT_ELIM o AC_CONV(assoc,sym) o mk_eq) (r1,r2)
1199 val eqv = MK_COMB(AP_TERM eqop le,re)
1200 in
1201 CONV_RULE(RAND_CONV
1202 (end_itlist (curry op ORELSEC) (map REWR_CONV lcthms)))
1203 eqv
1204 end
1205 end
1206 | _ => raise ERR ""
1207 end
1208
1209(*---------------------------------------------------------------------------*)
1210(* Tactic to do all the obvious simplifications via cancellation etc. *)
1211(*---------------------------------------------------------------------------*)
1212fun mk_rewrites th =
1213 let val th = Drule.SPEC_ALL th
1214 val t = Thm.concl th
1215 in
1216 if is_eq t
1217 then [th]
1218 else if is_conj t
1219 then (op @ o (mk_rewrites##mk_rewrites) o Drule.CONJ_PAIR) th
1220 else if is_neg t
1221 then [Drule.EQF_INTRO th]
1222 else [Drule.EQT_INTRO th]
1223 end;
1224
1225val CANCEL_TAC = (C (curry op THEN)
1226 (PURE_REWRITE_TAC
1227 (itlist (append o mk_rewrites)
1228 [REFL_CLAUSE, EQ_CLAUSES, NOT_CLAUSES,
1229 AND_CLAUSES, OR_CLAUSES, IMP_CLAUSES,
1230 COND_CLAUSES, FORALL_SIMP, EXISTS_SIMP,
1231 ABS_SIMP] []))
1232 o CONV_TAC o ONCE_DEPTH_CONV o end_itlist (curry op ORELSEC))
1233 (map CANCEL_CONV
1234 [(HREAL_ADD_ASSOC,HREAL_ADD_SYM,
1235 [HREAL_EQ_LADD, HREAL_EQ_ADDL, HREAL_EQ_ADDR, EQ_SYM]),
1236 (HREAL_ADD_ASSOC,HREAL_ADD_SYM,
1237 [HREAL_LT_LADD, HREAL_LT_ADDL, HREAL_LT_ADDR, HREAL_LT_REFL])]);
1238
1239(*---------------------------------------------------------------------------*)
1240(* Define operations on representatives. *)
1241(*---------------------------------------------------------------------------*)
1242
1243Definition treal_0[nocompute]:
1244 treal_0 = (hreal_1,hreal_1)
1245End
1246
1247Definition treal_1[nocompute]:
1248 treal_1 = (hreal_1 hreal_add hreal_1,hreal_1)
1249End
1250
1251Definition treal_neg[nocompute]:
1252 treal_neg (x:hreal,(y:hreal)) = (y,x)
1253End
1254
1255val treal_add = new_infixl_definition("treal_add",
1256 “$treal_add (x1,y1) (x2,y2) = (x1 hreal_add x2, y1 hreal_add y2)”,500);
1257
1258val treal_mul = new_infixl_definition("treal_mul",
1259 “treal_mul (x1,y1) (x2,y2) =
1260 ((x1 hreal_mul x2) hreal_add (y1 hreal_mul y2),
1261 (x1 hreal_mul y2) hreal_add (y1 hreal_mul x2))”, 600);
1262
1263Definition treal_lt[nocompute]:
1264treal_lt (x1,y1) (x2,y2) = (x1 hreal_add y2) hreal_lt (x2 hreal_add y1)
1265End
1266val _ = temp_set_fixity "treal_lt" (Infix(NONASSOC, 450))
1267
1268Definition treal_inv[nocompute]:
1269 treal_inv (x,y) =
1270 if (x = y) then treal_0
1271 else if y hreal_lt x then
1272 ((hreal_inv (x hreal_sub y)) hreal_add hreal_1,hreal_1)
1273 else (hreal_1,(hreal_inv(y hreal_sub x)) hreal_add hreal_1)
1274End
1275
1276(*---------------------------------------------------------------------------*)
1277(* Define the equivalence relation and prove it *is* one *)
1278(*---------------------------------------------------------------------------*)
1279
1280Definition treal_eq[nocompute]:
1281 treal_eq (x1,y1) (x2,y2) = (x1 hreal_add y2 = x2 hreal_add y1)
1282End
1283val _ = temp_set_fixity "treal_eq" (Infix(NONASSOC, 450))
1284
1285Theorem TREAL_EQ_REFL:
1286 !x. x treal_eq x
1287Proof
1288 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq] THEN REFL_TAC
1289QED
1290
1291Theorem TREAL_EQ_SYM:
1292 !x y. x treal_eq y = y treal_eq x
1293Proof
1294 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq] THEN
1295 CONV_TAC(RAND_CONV SYM_CONV) THEN REFL_TAC
1296QED
1297
1298Theorem TREAL_EQ_TRANS:
1299 !x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z
1300Proof
1301 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq] THEN
1302 DISCH_THEN(MP_TAC o MK_COMB o (AP_TERM “$hreal_add” ## I) o CONJ_PAIR)
1303 THEN CANCEL_TAC THEN DISCH_THEN SUBST1_TAC THEN CANCEL_TAC
1304QED
1305
1306Theorem TREAL_EQ_EQUIV:
1307 !p q. p treal_eq q = ($treal_eq p = $treal_eq q)
1308Proof
1309 REPEAT GEN_TAC THEN CONV_TAC SYM_CONV THEN
1310 CONV_TAC (ONCE_DEPTH_CONV (X_FUN_EQ_CONV “r:hreal#hreal”)) THEN
1311 EQ_TAC THENL
1312 [DISCH_THEN(MP_TAC o SPEC “q:hreal#hreal”) THEN
1313 REWRITE_TAC[TREAL_EQ_REFL],
1314 DISCH_TAC THEN GEN_TAC THEN EQ_TAC THENL
1315 [RULE_ASSUM_TAC(ONCE_REWRITE_RULE[TREAL_EQ_SYM]), ALL_TAC] THEN
1316 POP_ASSUM(fn th => DISCH_THEN(MP_TAC o CONJ th)) THEN
1317 MATCH_ACCEPT_TAC TREAL_EQ_TRANS]
1318QED
1319
1320Theorem TREAL_EQ_AP:
1321 !p q. (p = q) ==> p treal_eq q
1322Proof
1323 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
1324 MATCH_ACCEPT_TAC TREAL_EQ_REFL
1325QED
1326
1327(*---------------------------------------------------------------------------*)
1328(* Prove the properties of representatives *)
1329(*---------------------------------------------------------------------------*)
1330
1331Theorem TREAL_10:
1332 ~(treal_1 treal_eq treal_0)
1333Proof
1334 REWRITE_TAC[treal_1, treal_0, treal_eq, HREAL_NOZERO]
1335QED
1336
1337Theorem TREAL_ADD_SYM:
1338 !x y. x treal_add y = y treal_add x
1339Proof
1340 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_add] THEN
1341 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV)
1342 [HREAL_ADD_SYM] THEN
1343 REFL_TAC
1344QED
1345
1346Theorem TREAL_MUL_SYM:
1347 !x y. x treal_mul y = y treal_mul x
1348Proof
1349 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul] THEN
1350 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV)
1351 [HREAL_MUL_SYM] THEN
1352 REWRITE_TAC[PAIR_EQ] THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM
1353QED
1354
1355Theorem TREAL_ADD_ASSOC:
1356 !x y z. x treal_add (y treal_add z) = (x treal_add y) treal_add z
1357Proof
1358 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_add] THEN
1359 REWRITE_TAC[HREAL_ADD_ASSOC]
1360QED
1361
1362Theorem TREAL_MUL_ASSOC:
1363 !x y z. x treal_mul (y treal_mul z) = (x treal_mul y) treal_mul z
1364Proof
1365 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul] THEN
1366 REWRITE_TAC[HREAL_LDISTRIB, HREAL_RDISTRIB, PAIR_EQ, GSYM HREAL_MUL_ASSOC]
1367 THEN CONJ_TAC THEN CANCEL_TAC
1368QED
1369
1370Theorem TREAL_LDISTRIB:
1371 !x y z. x treal_mul (y treal_add z) =
1372 (x treal_mul y) treal_add (x treal_mul z)
1373Proof
1374 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul, treal_add] THEN
1375 REWRITE_TAC[HREAL_LDISTRIB, PAIR_EQ] THEN
1376 CONJ_TAC THEN CANCEL_TAC
1377QED
1378
1379Theorem TREAL_ADD_LID:
1380 !x. (treal_0 treal_add x) treal_eq x
1381Proof
1382 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_add, treal_eq] THEN
1383 CANCEL_TAC
1384QED
1385
1386Theorem TREAL_MUL_LID:
1387 !x. (treal_1 treal_mul x) treal_eq x
1388Proof
1389 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_1, treal_mul, treal_eq] THEN
1390 REWRITE_TAC[HREAL_MUL_LID, HREAL_LDISTRIB, HREAL_RDISTRIB] THEN
1391 CANCEL_TAC THEN CANCEL_TAC
1392QED
1393
1394Theorem TREAL_ADD_LINV:
1395 !x. ((treal_neg x) treal_add x) treal_eq treal_0
1396Proof
1397 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_neg, treal_add, treal_eq, treal_0]
1398 THEN CANCEL_TAC
1399QED
1400
1401Theorem TREAL_INV_0:
1402 treal_inv (treal_0) treal_eq (treal_0)
1403Proof
1404 REWRITE_TAC[treal_inv, treal_eq, treal_0]
1405QED
1406
1407Theorem TREAL_MUL_LINV:
1408 !x. ~(x treal_eq treal_0) ==>
1409 (((treal_inv x) treal_mul x) treal_eq treal_1)
1410Proof
1411 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_eq, treal_inv] THEN
1412 CANCEL_TAC THEN DISCH_TAC THEN DISJ_CASES_THEN2
1413 (fn th => MP_TAC th THEN ASM_REWRITE_TAC[]) (DISJ_CASES_THEN ASSUME_TAC)
1414 (SPECL [“FST (x:hreal#hreal)”, “SND (x:hreal#hreal)”] HREAL_LT_TOTAL) THEN
1415 FIRST_ASSUM(ASSUME_TAC o MATCH_MP HREAL_LT_GT) THEN
1416 PURE_ASM_REWRITE_TAC[COND_CLAUSES, treal_mul, treal_eq, treal_1] THEN
1417 REWRITE_TAC[HREAL_MUL_LID, HREAL_LDISTRIB, HREAL_RDISTRIB] THEN
1418 CANCEL_TAC THEN W(SUBST1_TAC o SYM o C SPEC HREAL_MUL_LINV o
1419 find_term(fn tm => rator(rator tm) ~~ “$hreal_sub” handle _ => false) o snd)
1420 THEN
1421 REWRITE_TAC[GSYM HREAL_LDISTRIB] THEN AP_TERM_TAC THEN
1422 FIRST_ASSUM(SUBST1_TAC o MATCH_MP HREAL_SUB_ADD) THEN REFL_TAC
1423QED
1424
1425Theorem TREAL_LT_TOTAL:
1426 !x y. x treal_eq y \/ x treal_lt y \/ y treal_lt x
1427Proof
1428 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_eq] THEN
1429 MATCH_ACCEPT_TAC HREAL_LT_TOTAL
1430QED
1431
1432Theorem TREAL_LT_REFL:
1433 !x. ~(x treal_lt x)
1434Proof
1435 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt] THEN
1436 MATCH_ACCEPT_TAC HREAL_LT_REFL
1437QED
1438
1439Theorem TREAL_LT_TRANS:
1440 !x y z. x treal_lt y /\ y treal_lt z ==> x treal_lt z
1441Proof
1442 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt] THEN
1443 DISCH_THEN(MP_TAC o MATCH_MP HREAL_LT_ADD2) THEN CANCEL_TAC THEN
1444 DISCH_TAC THEN GEN_REWR_TAC RAND_CONV [HREAL_ADD_SYM]
1445 THEN POP_ASSUM ACCEPT_TAC
1446QED
1447
1448Theorem TREAL_LT_ADD:
1449 !x y z. (y treal_lt z) ==> (x treal_add y) treal_lt (x treal_add z)
1450Proof
1451 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_add] THEN
1452 CANCEL_TAC
1453QED
1454
1455Theorem TREAL_LT_MUL:
1456 !x y. treal_0 treal_lt x /\ treal_0 treal_lt y ==>
1457 treal_0 treal_lt (x treal_mul y)
1458Proof
1459 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_lt, treal_mul] THEN
1460 CANCEL_TAC THEN DISCH_THEN(CONJUNCTS_THEN
1461 (CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[HREAL_LT])) THEN
1462 REWRITE_TAC[HREAL_LDISTRIB, HREAL_RDISTRIB] THEN CANCEL_TAC THEN CANCEL_TAC
1463QED
1464
1465(*---------------------------------------------------------------------------*)
1466(* Rather than grub round proving the supremum property for representatives, *)
1467(* we prove the appropriate order-isomorphism {x::R|0 < r} <-> R^+ *)
1468(*---------------------------------------------------------------------------*)
1469
1470Definition treal_of_hreal[nocompute]:
1471 treal_of_hreal x = (x hreal_add hreal_1,hreal_1)
1472End
1473
1474Definition hreal_of_treal[nocompute]:
1475 hreal_of_treal (x,y) = @d. x = y hreal_add d
1476End
1477
1478Theorem TREAL_BIJ:
1479 (!h. (hreal_of_treal(treal_of_hreal h)) = h) /\
1480 (!r. treal_0 treal_lt r = (treal_of_hreal(hreal_of_treal r)) treal_eq r)
1481Proof
1482 CONJ_TAC THENL
1483 [GEN_TAC THEN REWRITE_TAC[treal_of_hreal, hreal_of_treal] THEN
1484 CANCEL_TAC THEN CONV_TAC SYM_CONV THEN
1485 CONV_TAC(funpow 2 RAND_CONV ETA_CONV) THEN
1486 MATCH_MP_TAC SELECT_AX THEN EXISTS_TAC “h:hreal” THEN REFL_TAC,
1487 GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_0, treal_lt, treal_eq,
1488 treal_of_hreal, hreal_of_treal] THEN CANCEL_TAC THEN EQ_TAC THENL
1489 [DISCH_THEN(MP_TAC o MATCH_MP HREAL_SUB_ADD) THEN
1490 DISCH_THEN(CONV_TAC o RAND_CONV o REWR_CONV o SYM o SELECT_RULE o
1491 EXISTS(“?d. d hreal_add (SND r) = FST r”, “(FST r) hreal_sub (SND r)”))
1492 THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1493 GEN_REWR_TAC (RAND_CONV o ONCE_DEPTH_CONV)
1494 [HREAL_ADD_SYM] THEN
1495 CONV_TAC(RAND_CONV(ONCE_DEPTH_CONV SYM_CONV)) THEN REFL_TAC,
1496 DISCH_THEN(SUBST1_TAC o SYM) THEN CANCEL_TAC]]
1497QED
1498
1499Theorem TREAL_ISO:
1500 !h i. h hreal_lt i ==> (treal_of_hreal h) treal_lt (treal_of_hreal i)
1501Proof
1502 REPEAT GEN_TAC THEN REWRITE_TAC[treal_of_hreal, treal_lt] THEN CANCEL_TAC THEN
1503 CANCEL_TAC
1504QED
1505
1506Theorem TREAL_BIJ_WELLDEF:
1507 !h i. h treal_eq i ==> (hreal_of_treal h = hreal_of_treal i)
1508Proof
1509 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_eq, hreal_of_treal] THEN
1510 DISCH_TAC THEN AP_TERM_TAC THEN CONV_TAC(X_FUN_EQ_CONV “d:hreal”) THEN
1511 GEN_TAC THEN BETA_TAC THEN EQ_TAC THENL
1512 [DISCH_THEN(MP_TAC o C AP_THM “SND(i:hreal#hreal)” o AP_TERM “$hreal_add”)
1513 THEN POP_ASSUM SUBST1_TAC,
1514 DISCH_THEN(MP_TAC o C AP_THM “SND(h:hreal#hreal)” o AP_TERM “$hreal_add”)
1515 THEN POP_ASSUM(SUBST1_TAC o SYM)] THEN
1516 CANCEL_TAC THEN DISCH_THEN SUBST1_TAC THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM
1517QED
1518
1519(*---------------------------------------------------------------------------*)
1520(* Prove that the operations on representatives are well-defined *)
1521(*---------------------------------------------------------------------------*)
1522
1523Theorem TREAL_NEG_WELLDEF:
1524 !x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2)
1525Proof
1526 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_neg, treal_eq] THEN
1527 DISCH_THEN(curry op THEN (ONCE_REWRITE_TAC[HREAL_ADD_SYM]) o SUBST1_TAC) THEN
1528 REFL_TAC
1529QED
1530
1531Theorem TREAL_ADD_WELLDEFR:
1532 !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y)
1533Proof
1534 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_add, treal_eq] THEN
1535 CANCEL_TAC
1536QED
1537
1538Theorem TREAL_ADD_WELLDEF:
1539 !x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1540 (x1 treal_add y1) treal_eq (x2 treal_add y2)
1541Proof
1542 REPEAT GEN_TAC THEN DISCH_TAC THEN
1543 MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC “x1 treal_add y2” THEN
1544 CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_ADD_SYM], ALL_TAC] THEN
1545 MATCH_MP_TAC TREAL_ADD_WELLDEFR THEN ASM_REWRITE_TAC[]
1546QED
1547
1548Theorem TREAL_MUL_WELLDEFR:
1549 !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y)
1550Proof
1551 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_mul, treal_eq] THEN
1552 ONCE_REWRITE_TAC[AC(HREAL_ADD_ASSOC,HREAL_ADD_SYM)
1553 “(a hreal_add b) hreal_add (c hreal_add d) =
1554 (a hreal_add d) hreal_add (b hreal_add c)”] THEN
1555 REWRITE_TAC[GSYM HREAL_RDISTRIB] THEN DISCH_TAC THEN
1556 ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
1557 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC
1558QED
1559
1560Theorem TREAL_MUL_WELLDEF:
1561 !x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1562 (x1 treal_mul y1) treal_eq (x2 treal_mul y2)
1563Proof
1564 REPEAT GEN_TAC THEN DISCH_TAC THEN
1565 MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC “x1 treal_mul y2” THEN
1566 CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_MUL_SYM], ALL_TAC] THEN
1567 MATCH_MP_TAC TREAL_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]
1568QED
1569
1570Theorem TREAL_LT_WELLDEFR:
1571 !x1 x2 y. x1 treal_eq x2 ==> (x1 treal_lt y = x2 treal_lt y)
1572Proof
1573 let fun mkc v tm = SYM(SPECL (v::snd(strip_comb tm)) HREAL_LT_LADD) in
1574 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_eq] THEN
1575 DISCH_TAC THEN CONV_TAC(RAND_CONV(mkc “SND (x1:hreal#hreal)”)) THEN
1576 CONV_TAC(LAND_CONV(mkc “SND (x2:hreal#hreal)”)) THEN
1577 ONCE_REWRITE_TAC[AC(HREAL_ADD_ASSOC,HREAL_ADD_SYM)
1578 “a hreal_add (b hreal_add c) = (b hreal_add a) hreal_add c”] THEN
1579 POP_ASSUM SUBST1_TAC THEN CANCEL_TAC end
1580QED
1581
1582Theorem TREAL_LT_WELLDEFL:
1583 !x y1 y2. y1 treal_eq y2 ==> (x treal_lt y1 = x treal_lt y2)
1584Proof
1585 let fun mkc v tm = SYM(SPECL (v::snd(strip_comb tm)) HREAL_LT_LADD) in
1586 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_lt, treal_eq] THEN
1587 DISCH_TAC THEN CONV_TAC(RAND_CONV(mkc “FST (y1:hreal#hreal)”)) THEN
1588 CONV_TAC(LAND_CONV(mkc “FST (y2:hreal#hreal)”)) THEN
1589 ONCE_REWRITE_TAC[AC(HREAL_ADD_ASSOC,HREAL_ADD_SYM)
1590 “a hreal_add (b hreal_add c) = (a hreal_add c) hreal_add b”] THEN
1591 POP_ASSUM SUBST1_TAC THEN CANCEL_TAC THEN AP_TERM_TAC THEN CANCEL_TAC end
1592QED
1593
1594Theorem TREAL_LT_WELLDEF:
1595 !x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1596 (x1 treal_lt y1 = x2 treal_lt y2)
1597Proof
1598 REPEAT GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC EQ_TRANS THEN
1599 EXISTS_TAC “x1 treal_lt y2” THEN CONJ_TAC THENL
1600 [MATCH_MP_TAC TREAL_LT_WELLDEFL, MATCH_MP_TAC TREAL_LT_WELLDEFR] THEN
1601 ASM_REWRITE_TAC[]
1602QED
1603
1604Theorem TREAL_INV_WELLDEF:
1605 !x1 x2. x1 treal_eq x2 ==> (treal_inv x1) treal_eq (treal_inv x2)
1606Proof
1607 let val lemma1 = prove
1608 (“(a hreal_add b' = b hreal_add a') ==>
1609 (a' hreal_lt a = b' hreal_lt b)”,
1610 DISCH_TAC THEN EQ_TAC THEN
1611 DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC o REWRITE_RULE[HREAL_LT]) THEN
1612 POP_ASSUM MP_TAC THEN CANCEL_TAC THENL
1613 [DISCH_THEN(SUBST1_TAC o SYM), DISCH_THEN SUBST1_TAC] THEN CANCEL_TAC)
1614 val lemma2 = prove
1615 (“(a hreal_add b' = b hreal_add a') ==>
1616 ((a = a') = (b = b'))”,
1617 DISCH_TAC THEN EQ_TAC THEN DISCH_THEN SUBST_ALL_TAC THEN POP_ASSUM MP_TAC
1618 THEN CANCEL_TAC THEN DISCH_THEN SUBST1_TAC THEN REFL_TAC) in
1619 REPEAT GEN_PAIR_TAC THEN PURE_REWRITE_TAC[treal_inv, treal_eq] THEN
1620 DISCH_TAC THEN FIRST_ASSUM(SUBST1_TAC o MATCH_MP lemma1) THEN
1621 FIRST_ASSUM(SUBST1_TAC o MATCH_MP lemma2) THEN COND_CASES_TAC THEN
1622 REWRITE_TAC[TREAL_EQ_REFL] THEN COND_CASES_TAC THEN REWRITE_TAC[treal_eq]
1623 THEN CANCEL_TAC THEN CANCEL_TAC THEN AP_TERM_TAC THEN
1624 W(FREEZE_THEN(CONV_TAC o REWR_CONV) o GSYM o C SPEC HREAL_EQ_LADD o
1625 mk_comb o (curry mk_comb “$hreal_add” ## I) o (rand ## rand) o dest_eq o snd)
1626 THEN ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
1627 GEN_REWR_TAC (funpow 2 RAND_CONV) [HREAL_ADD_SYM] THEN
1628 REWRITE_TAC[HREAL_ADD_ASSOC] THENL
1629 [RULE_ASSUM_TAC GSYM,
1630 MP_TAC(SPECL[“FST(x2:hreal#hreal)”, “SND(x2:hreal#hreal)”]
1631 HREAL_LT_TOTAL) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1632 RULE_ASSUM_TAC(ONCE_REWRITE_RULE[HREAL_ADD_SYM])] THEN
1633 FIRST_ASSUM(fn th => FIRST_ASSUM(MP_TAC o EQ_MP (MATCH_MP lemma1 th))) THEN
1634 FIRST_ASSUM(UNDISCH_TAC o assert(aconv “$hreal_lt” o rator o rator) o concl)
1635 THEN REPEAT(DISCH_THEN(SUBST1_TAC o MATCH_MP HREAL_SUB_ADD)) THEN
1636 FIRST_ASSUM SUBST1_TAC THEN REFL_TAC end
1637QED