1 (* ========================================================================= *)
2 (* Theory of real numbers. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* The main infix overloaded operations *)
14 (* ------------------------------------------------------------------------- *)
16 parse_as_infix("++",(16,"right"));;
17 parse_as_infix("**",(20,"right"));;
18 parse_as_infix("<<=",(12,"right"));;
19 parse_as_infix("===",(10,"right"));;
21 parse_as_infix ("treal_mul",(20,"right"));;
22 parse_as_infix ("treal_add",(16,"right"));;
23 parse_as_infix ("treal_le",(12,"right"));;
24 parse_as_infix ("treal_eq",(10,"right"));;
26 make_overloadable "+" `:A->A->A`;;
27 make_overloadable "-" `:A->A->A`;;
28 make_overloadable "*" `:A->A->A`;;
29 make_overloadable "/" `:A->A->A`;;
30 make_overloadable "<" `:A->A->bool`;;
31 make_overloadable "<=" `:A->A->bool`;;
32 make_overloadable ">" `:A->A->bool`;;
33 make_overloadable ">=" `:A->A->bool`;;
34 make_overloadable "--" `:A->A`;;
35 make_overloadable "pow" `:A->num->A`;;
36 make_overloadable "inv" `:A->A`;;
37 make_overloadable "abs" `:A->A`;;
38 make_overloadable "max" `:A->A->A`;;
39 make_overloadable "min" `:A->A->A`;;
40 make_overloadable "&" `:num->A`;;
42 do_list overload_interface
43 ["+",`(+):num->num->num`; "-",`(-):num->num->num`;
44 "*",`(*):num->num->num`; "<",`(<):num->num->bool`;
45 "<=",`(<=):num->num->bool`; ">",`(>):num->num->bool`;
46 ">=",`(>=):num->num->bool`];;
48 let prioritize_num() = prioritize_overload(mk_type("num",[]));;
50 (* ------------------------------------------------------------------------- *)
51 (* Absolute distance function on the naturals. *)
52 (* ------------------------------------------------------------------------- *)
54 let dist = new_definition
55 `dist(m,n) = (m - n) + (n - m)`;;
57 (* ------------------------------------------------------------------------- *)
58 (* Some easy theorems. *)
59 (* ------------------------------------------------------------------------- *)
63 REWRITE_TAC[dist; SUB_REFL; ADD_CLAUSES]);;
65 let DIST_LZERO = prove
67 REWRITE_TAC[dist; SUB_0; ADD_CLAUSES]);;
69 let DIST_RZERO = prove
71 REWRITE_TAC[dist; SUB_0; ADD_CLAUSES]);;
74 (`!m n. dist(m,n) = dist(n,m)`,
75 REWRITE_TAC[dist] THEN MATCH_ACCEPT_TAC ADD_SYM);;
78 (`!m p n. dist(m + n,m + p) = dist(n,p)`,
79 REWRITE_TAC[dist; SUB_ADD_LCANCEL]);;
82 (`!m p n. dist(m + p,n + p) = dist(m,n)`,
83 REWRITE_TAC[dist; SUB_ADD_RCANCEL]);;
85 let DIST_LADD_0 = prove
86 (`!m n. dist(m + n,m) = n`,
87 REWRITE_TAC[dist; ADD_SUB2; ADD_SUBR2; ADD_CLAUSES]);;
89 let DIST_RADD_0 = prove
90 (`!m n. dist(m,m + n) = n`,
91 ONCE_REWRITE_TAC[DIST_SYM] THEN MATCH_ACCEPT_TAC DIST_LADD_0);;
94 (`!m n p. m * dist(n,p) = dist(m * n,m * p)`,
95 REWRITE_TAC[dist; LEFT_ADD_DISTRIB; LEFT_SUB_DISTRIB]);;
98 (`!m n p. dist(m,n) * p = dist(m * p,n * p)`,
99 REWRITE_TAC[dist; RIGHT_ADD_DISTRIB; RIGHT_SUB_DISTRIB]);;
101 let DIST_EQ_0 = prove
102 (`!m n. (dist(m,n) = 0) <=> (m = n)`,
103 REWRITE_TAC[dist; ADD_EQ_0; SUB_EQ_0; LE_ANTISYM]);;
105 (* ------------------------------------------------------------------------- *)
106 (* Simplifying theorem about the distance operation. *)
107 (* ------------------------------------------------------------------------- *)
109 let DIST_ELIM_THM = prove
110 (`P(dist(x,y)) <=> !d. ((x = y + d) ==> P(d)) /\ ((y = x + d) ==> P(d))`,
111 DISJ_CASES_TAC(SPECL [`x:num`; `y:num`] LE_CASES) THEN
112 POP_ASSUM(X_CHOOSE_THEN `e:num` SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
113 REWRITE_TAC[dist; ADD_SUB; ADD_SUB2; ADD_SUBR; ADD_SUBR2] THEN
114 REWRITE_TAC[ADD_CLAUSES; EQ_ADD_LCANCEL] THEN
115 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [EQ_SYM_EQ] THEN
116 REWRITE_TAC[GSYM ADD_ASSOC; EQ_ADD_LCANCEL_0; ADD_EQ_0] THEN
117 ASM_CASES_TAC `e = 0` THEN ASM_REWRITE_TAC[] THEN
118 EQ_TAC THEN REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
119 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
121 (* ------------------------------------------------------------------------- *)
122 (* Now some more theorems. *)
123 (* ------------------------------------------------------------------------- *)
125 let DIST_LE_CASES,DIST_ADDBOUND,DIST_TRIANGLE,DIST_ADD2,DIST_ADD2_REV =
128 HIGHER_REWRITE_CONV[SUB_ELIM_THM; COND_ELIM_THM; DIST_ELIM_THM] false in
129 CONV_TAC conv THEN TRY GEN_TAC THEN CONJ_TAC THEN
130 DISCH_THEN(fun th -> SUBST_ALL_TAC th THEN
131 (let l,r = dest_eq (concl th) in
132 if is_var l & not (vfree_in l r) then ALL_TAC
133 else ASSUME_TAC th)) in
135 REPEAT STRIP_TAC THEN REPEAT DIST_ELIM_TAC THEN
136 REWRITE_TAC[GSYM NOT_LT; LT_EXISTS] THEN
137 DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN POP_ASSUM MP_TAC THEN
138 CONV_TAC(LAND_CONV NUM_CANCEL_CONV) THEN
139 REWRITE_TAC[ADD_CLAUSES; NOT_SUC] in
140 let DIST_LE_CASES = prove
141 (`!m n p. dist(m,n) <= p <=> (m <= n + p) /\ (n <= m + p)`,
142 REPEAT GEN_TAC THEN REPEAT DIST_ELIM_TAC THEN
143 REWRITE_TAC[GSYM ADD_ASSOC; LE_ADD; LE_ADD_LCANCEL])
144 and DIST_ADDBOUND = prove
145 (`!m n. dist(m,n) <= m + n`,
146 REPEAT GEN_TAC THEN DIST_ELIM_TAC THENL
147 [ONCE_REWRITE_TAC[ADD_SYM]; ALL_TAC] THEN
148 REWRITE_TAC[ADD_ASSOC; LE_ADDR])
149 and [DIST_TRIANGLE; DIST_ADD2; DIST_ADD2_REV] = (CONJUNCTS o prove)
150 (`(!m n p. dist(m,p) <= dist(m,n) + dist(n,p)) /\
151 (!m n p q. dist(m + n,p + q) <= dist(m,p) + dist(n,q)) /\
152 (!m n p q. dist(m,p) <= dist(m + n,p + q) + dist(n,q))`,
154 DIST_LE_CASES,DIST_ADDBOUND,DIST_TRIANGLE,DIST_ADD2,DIST_ADD2_REV;;
156 let DIST_TRIANGLE_LE = prove
157 (`!m n p q. dist(m,n) + dist(n,p) <= q ==> dist(m,p) <= q`,
158 REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
159 EXISTS_TAC `dist(m,n) + dist(n,p)` THEN ASM_REWRITE_TAC[DIST_TRIANGLE]);;
161 let DIST_TRIANGLES_LE = prove
163 dist(m,n) <= r /\ dist(p,q) <= s ==> dist(m,p) <= dist(n,q) + r + s`,
164 REPEAT STRIP_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
165 EXISTS_TAC `n:num` THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
166 REWRITE_TAC[GSYM ADD_ASSOC] THEN MATCH_MP_TAC LE_ADD2 THEN
167 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
168 EXISTS_TAC `q:num` THEN GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
169 REWRITE_TAC[LE_ADD_LCANCEL] THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
172 (* ------------------------------------------------------------------------- *)
173 (* Useful lemmas about bounds. *)
174 (* ------------------------------------------------------------------------- *)
176 let BOUNDS_LINEAR = prove
177 (`!A B C. (!n. A * n <= B * n + C) <=> A <= B`,
178 REPEAT GEN_TAC THEN EQ_TAC THENL
179 [CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LE] THEN
180 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LT_EXISTS]) THEN
181 REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
182 DISCH_THEN(MP_TAC o SPEC `SUC C`) THEN
183 REWRITE_TAC[NOT_LE; MULT_CLAUSES; ADD_CLAUSES; LT_SUC_LE] THEN
184 REWRITE_TAC[ADD_ASSOC; LE_ADDR];
185 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o REWRITE_RULE[LE_EXISTS]) THEN
186 REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]]);;
188 let BOUNDS_LINEAR_0 = prove
189 (`!A B. (!n. A * n <= B) <=> (A = 0)`,
190 REPEAT GEN_TAC THEN MP_TAC(SPECL [`A:num`; `0`; `B:num`] BOUNDS_LINEAR) THEN
191 REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; LE]);;
193 let BOUNDS_DIVIDED = prove
194 (`!P. (?B. !n. P(n) <= B) <=>
195 (?A B. !n. n * P(n) <= A * n + B)`,
196 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
197 [MAP_EVERY EXISTS_TAC [`B:num`; `0`] THEN
198 GEN_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
199 GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
200 ASM_REWRITE_TAC[LE_MULT_LCANCEL];
201 EXISTS_TAC `P(0) + A + B` THEN GEN_TAC THEN
202 MP_TAC(SPECL [`n:num`; `(P:num->num) n`; `P(0) + A + B`]
203 LE_MULT_LCANCEL) THEN
204 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[LE_ADD] THEN
205 DISCH_THEN(SUBST1_TAC o SYM) THEN
206 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN
207 ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
208 GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
209 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
210 REWRITE_TAC[GSYM ADD_ASSOC; LE_ADD_LCANCEL] THEN
211 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B * n` THEN
212 REWRITE_TAC[LE_ADD] THEN UNDISCH_TAC `~(n = 0)` THEN
213 SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
214 ASM_REWRITE_TAC[MULT_CLAUSES; LE_ADD]]);;
216 let BOUNDS_NOTZERO = prove
217 (`!P A B. (P 0 0 = 0) /\ (!m n. P m n <= A * (m + n) + B) ==>
218 (?B. !m n. P m n <= B * (m + n))`,
219 REPEAT STRIP_TAC THEN EXISTS_TAC `A + B` THEN
220 REPEAT GEN_TAC THEN ASM_CASES_TAC `m + n = 0` THENL
221 [RULE_ASSUM_TAC(REWRITE_RULE[ADD_EQ_0]) THEN ASM_REWRITE_TAC[LE_0];
222 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * (m + n) + B` THEN
223 ASM_REWRITE_TAC[] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
224 UNDISCH_TAC `~(m + n = 0)` THEN SPEC_TAC(`m + n`,`p:num`) THEN
225 INDUCT_TAC THEN REWRITE_TAC[MULT_CLAUSES; LE_ADD]]);;
227 let BOUNDS_IGNORE = prove
228 (`!P Q. (?B. !i. P(i) <= Q(i) + B) <=>
229 (?B N. !i. N <= i ==> P(i) <= Q(i) + B)`,
230 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
231 [EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[];
232 POP_ASSUM MP_TAC THEN SPEC_TAC(`B:num`,`B:num`) THEN
233 SPEC_TAC(`N:num`,`N:num`) THEN INDUCT_TAC THENL
234 [REWRITE_TAC[LE_0] THEN GEN_TAC THEN DISCH_TAC THEN
235 EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[];
236 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
237 EXISTS_TAC `B + P(N:num)` THEN X_GEN_TAC `i:num` THEN
238 DISCH_TAC THEN ASM_CASES_TAC `SUC N <= i` THENL
239 [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `Q(i:num) + B` THEN
240 REWRITE_TAC[LE_ADD; ADD_ASSOC] THEN FIRST_ASSUM MATCH_MP_TAC THEN
242 UNDISCH_TAC `~(SUC N <= i)` THEN REWRITE_TAC[NOT_LE; LT] THEN
243 ASM_REWRITE_TAC[GSYM NOT_LE] THEN DISCH_THEN SUBST1_TAC THEN
244 REWRITE_TAC[ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
245 REWRITE_TAC[LE_ADD]]]]);;
247 (* ------------------------------------------------------------------------- *)
248 (* Define type of nearly additive functions. *)
249 (* ------------------------------------------------------------------------- *)
251 let is_nadd = new_definition
252 `is_nadd x <=> (?B. !m n. dist(m * x(n),n * x(m)) <= B * (m + n))`;;
254 let is_nadd_0 = prove
256 REWRITE_TAC[is_nadd; MULT_CLAUSES; DIST_REFL; LE_0]);;
258 let nadd_abs,nadd_rep =
259 new_basic_type_definition "nadd" ("mk_nadd","dest_nadd") is_nadd_0;;
261 override_interface ("fn",`dest_nadd`);;
262 override_interface ("afn",`mk_nadd`);;
264 (* ------------------------------------------------------------------------- *)
265 (* Properties of nearly-additive functions. *)
266 (* ------------------------------------------------------------------------- *)
268 let NADD_CAUCHY = prove
269 (`!x. ?B. !m n. dist(m * fn x n,n * fn x m) <= B * (m + n)`,
270 REWRITE_TAC[GSYM is_nadd; nadd_rep; nadd_abs; ETA_AX]);;
272 let NADD_BOUND = prove
273 (`!x. ?A B. !n. fn x n <= A * n + B`,
274 GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
275 MAP_EVERY EXISTS_TAC [`B + fn x 1`; `B:num`] THEN GEN_TAC THEN
276 POP_ASSUM(MP_TAC o SPECL [`n:num`; `1`]) THEN
277 REWRITE_TAC[DIST_LE_CASES; MULT_CLAUSES] THEN
278 DISCH_THEN(MP_TAC o CONJUNCT2) THEN
279 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_CLAUSES] THEN
280 REWRITE_TAC[ADD_AC; MULT_AC]);;
282 let NADD_MULTIPLICATIVE = prove
283 (`!x. ?B. !m n. dist(fn x (m * n),m * fn x n) <= B * m + B`,
284 GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
285 EXISTS_TAC `B + fn x 0` THEN REPEAT GEN_TAC THEN
286 ASM_CASES_TAC `n = 0` THENL
287 [MATCH_MP_TAC (LE_IMP DIST_ADDBOUND) THEN
288 ASM_REWRITE_TAC[MULT_CLAUSES; RIGHT_ADD_DISTRIB; MULT_AC] THEN
289 REWRITE_TAC[LE_EXISTS] THEN CONV_TAC(ONCE_DEPTH_CONV NUM_CANCEL_CONV) THEN
290 REWRITE_TAC[GSYM EXISTS_REFL]; UNDISCH_TAC `~(n = 0)`] THEN
291 REWRITE_TAC[TAUT `(~a ==> b) <=> a \/ b`; GSYM LE_MULT_LCANCEL;
293 REWRITE_TAC[MULT_ASSOC] THEN GEN_REWRITE_TAC
294 (LAND_CONV o RAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
295 POP_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
296 REWRITE_TAC[LE_EXISTS; RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB; MULT_AC] THEN
297 CONV_TAC(ONCE_DEPTH_CONV NUM_CANCEL_CONV) THEN
298 REWRITE_TAC[GSYM EXISTS_REFL]);;
300 let NADD_ADDITIVE = prove
301 (`!x. ?B. !m n. dist(fn x (m + n),fn x m + fn x n) <= B`,
302 GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
303 EXISTS_TAC `3 * B + fn x 0` THEN REPEAT GEN_TAC THEN
304 ASM_CASES_TAC `m + n = 0` THENL
305 [RULE_ASSUM_TAC(REWRITE_RULE[ADD_EQ_0]) THEN ONCE_REWRITE_TAC[DIST_SYM] THEN
306 ASM_REWRITE_TAC[ADD_CLAUSES; DIST_LADD_0; LE_ADDR];
307 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `3 * B` THEN
308 REWRITE_TAC[LE_ADD] THEN UNDISCH_TAC `~(m + n = 0)`] THEN
309 REWRITE_TAC[TAUT `(~a ==> b) <=> a \/ b`; GSYM LE_MULT_LCANCEL] THEN
310 REWRITE_TAC[DIST_LMUL; LEFT_ADD_DISTRIB] THEN
311 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [RIGHT_ADD_DISTRIB] THEN
312 MATCH_MP_TAC(LE_IMP DIST_ADD2) THEN
313 SUBGOAL_THEN `(m + n) * 3 * B = B * (m + m + n) + B * (n + m + n)`
315 [REWRITE_TAC[SYM(REWRITE_CONV [ARITH] `1 + 1 + 1`)] THEN
316 REWRITE_TAC[RIGHT_ADD_DISTRIB; LEFT_ADD_DISTRIB; MULT_CLAUSES] THEN
317 REWRITE_TAC[MULT_AC] THEN CONV_TAC NUM_CANCEL_CONV THEN REFL_TAC;
318 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]]);;
321 (`!x. ?B. !n. dist(fn x (SUC n),fn x n) <= B`,
322 GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_ADDITIVE) THEN
323 EXISTS_TAC `B + fn x 1` THEN GEN_TAC THEN
324 MATCH_MP_TAC(LE_IMP DIST_TRIANGLE) THEN
325 EXISTS_TAC `fn x n + fn x 1` THEN
326 ASM_REWRITE_TAC[ADD1] THEN MATCH_MP_TAC LE_ADD2 THEN
327 ASM_REWRITE_TAC[DIST_LADD_0; LE_REFL]);;
329 let NADD_DIST_LEMMA = prove
330 (`!x. ?B. !m n. dist(fn x (m + n),fn x m) <= B * n`,
331 GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_SUC) THEN
332 EXISTS_TAC `B:num` THEN GEN_TAC THEN
333 INDUCT_TAC THEN REWRITE_TAC[ADD_CLAUSES; DIST_REFL; LE_0] THEN
334 MATCH_MP_TAC(LE_IMP DIST_TRIANGLE) THEN
335 EXISTS_TAC `fn x (m + n)` THEN
336 REWRITE_TAC[ADD1; LEFT_ADD_DISTRIB] THEN
337 GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
338 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[GSYM ADD1; MULT_CLAUSES]);;
340 let NADD_DIST = prove
341 (`!x. ?B. !m n. dist(fn x m,fn x n) <= B * dist(m,n)`,
342 GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_DIST_LEMMA) THEN
343 EXISTS_TAC `B:num` THEN REPEAT GEN_TAC THEN
344 DISJ_CASES_THEN MP_TAC (SPECL [`m:num`; `n:num`] LE_CASES) THEN
345 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o ONCE_REWRITE_RULE[LE_EXISTS]) THENL
346 [ONCE_REWRITE_TAC[DIST_SYM]; ALL_TAC] THEN
347 ASM_REWRITE_TAC[DIST_LADD_0]);;
349 let NADD_ALTMUL = prove
350 (`!x y. ?A B. !n. dist(n * fn x (fn y n),fn x n * fn y n) <= A * n + B`,
351 REPEAT GEN_TAC THEN X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
352 MP_TAC(SPEC `y:nadd` NADD_BOUND) THEN
353 DISCH_THEN(X_CHOOSE_THEN `M:num` (X_CHOOSE_TAC `L:num`)) THEN
354 MAP_EVERY EXISTS_TAC [`B * (1 + M)`; `B * L`] THEN GEN_TAC THEN
355 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV) [MULT_SYM] THEN
356 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B * (n + fn y n)` THEN
357 ASM_REWRITE_TAC[] THEN REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB] THEN
358 REWRITE_TAC[MULT_CLAUSES; GSYM ADD_ASSOC; LE_ADD_LCANCEL] THEN
359 ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB; GSYM MULT_ASSOC; LE_MULT_LCANCEL]);;
361 (* ------------------------------------------------------------------------- *)
362 (* Definition of the equivalence relation and proof that it *is* one. *)
363 (* ------------------------------------------------------------------------- *)
365 override_interface ("===",`(nadd_eq):nadd->nadd->bool`);;
367 let nadd_eq = new_definition
368 `x === y <=> ?B. !n. dist(fn x n,fn y n) <= B`;;
370 let NADD_EQ_REFL = prove
372 GEN_TAC THEN REWRITE_TAC[nadd_eq; DIST_REFL; LE_0]);;
374 let NADD_EQ_SYM = prove
375 (`!x y. x === y <=> y === x`,
376 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
377 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [DIST_SYM] THEN REFL_TAC);;
379 let NADD_EQ_TRANS = prove
380 (`!x y z. x === y /\ y === z ==> x === z`,
381 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
382 DISCH_THEN(CONJUNCTS_THEN2
383 (X_CHOOSE_TAC `B1:num`) (X_CHOOSE_TAC `B2:num`)) THEN
384 EXISTS_TAC `B1 + B2` THEN X_GEN_TAC `n:num` THEN
385 MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN EXISTS_TAC `fn y n` THEN
386 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
388 (* ------------------------------------------------------------------------- *)
389 (* Injection of the natural numbers. *)
390 (* ------------------------------------------------------------------------- *)
392 override_interface ("&",`nadd_of_num:num->nadd`);;
394 let nadd_of_num = new_definition
395 `&k = afn(\n. k * n)`;;
397 let NADD_OF_NUM = prove
398 (`!k. fn(&k) = \n. k * n`,
399 REWRITE_TAC[nadd_of_num; GSYM nadd_rep; is_nadd] THEN
400 REWRITE_TAC[DIST_REFL; LE_0; MULT_AC]);;
402 let NADD_OF_NUM_WELLDEF = prove
403 (`!m n. (m = n) ==> &m === &n`,
404 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
405 MATCH_ACCEPT_TAC NADD_EQ_REFL);;
407 let NADD_OF_NUM_EQ = prove
408 (`!m n. (&m === &n) <=> (m = n)`,
409 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[NADD_OF_NUM_WELLDEF] THEN
410 REWRITE_TAC[nadd_eq; NADD_OF_NUM] THEN
411 REWRITE_TAC[GSYM DIST_RMUL; BOUNDS_LINEAR_0; DIST_EQ_0]);;
413 (* ------------------------------------------------------------------------- *)
414 (* Definition of (reflexive) ordering and the only special property needed. *)
415 (* ------------------------------------------------------------------------- *)
417 override_interface ("<<=",`nadd_le:nadd->nadd->bool`);;
419 let nadd_le = new_definition
420 `x <<= y <=> ?B. !n. fn x n <= fn y n + B`;;
422 let NADD_LE_WELLDEF_LEMMA = prove
423 (`!x x' y y'. x === x' /\ y === y' /\ x <<= y ==> x' <<= y'`,
424 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; nadd_le] THEN
425 REWRITE_TAC[DIST_LE_CASES; FORALL_AND_THM] THEN
426 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`) MP_TAC) THEN
427 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B2:num`) MP_TAC) THEN
428 DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN
429 EXISTS_TAC `(B2 + B) + B1` THEN X_GEN_TAC `n:num` THEN
430 FIRST_ASSUM(MATCH_MP_TAC o LE_IMP o CONJUNCT2) THEN
431 REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
432 FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN ASM_REWRITE_TAC[LE_ADD_RCANCEL]);;
434 let NADD_LE_WELLDEF = prove
435 (`!x x' y y'. x === x' /\ y === y' ==> (x <<= y <=> x' <<= y')`,
436 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
437 MATCH_MP_TAC NADD_LE_WELLDEF_LEMMA THEN ASM_REWRITE_TAC[] THENL
438 [MAP_EVERY EXISTS_TAC [`x:nadd`; `y:nadd`];
439 MAP_EVERY EXISTS_TAC [`x':nadd`; `y':nadd`] THEN
440 ONCE_REWRITE_TAC[NADD_EQ_SYM]] THEN
443 let NADD_LE_REFL = prove
445 REWRITE_TAC[nadd_le; LE_ADD]);;
447 let NADD_LE_TRANS = prove
448 (`!x y z. x <<= y /\ y <<= z ==> x <<= z`,
449 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le] THEN
450 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`) MP_TAC) THEN
451 DISCH_THEN(X_CHOOSE_TAC `B2:num`) THEN
452 EXISTS_TAC `B2 + B1` THEN GEN_TAC THEN
453 FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
454 ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL]);;
456 let NADD_LE_ANTISYM = prove
457 (`!x y. x <<= y /\ y <<= x <=> (x === y)`,
458 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; nadd_eq; DIST_LE_CASES] THEN
460 [DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `B1:num`)
461 (X_CHOOSE_TAC `B2:num`)) THEN
462 EXISTS_TAC `B1 + B2` THEN GEN_TAC THEN CONJ_TAC THEN
463 FIRST_ASSUM(MATCH_MP_TAC o LE_IMP) THEN
464 ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL; LE_ADD; LE_ADDR];
465 DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN
466 CONJ_TAC THEN EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[]]);;
468 let NADD_LE_TOTAL_LEMMA = prove
469 (`!x y. ~(x <<= y) ==> !B. ?n. ~(n = 0) /\ fn y n + B < fn x n`,
470 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NOT_FORALL_THM; NOT_EXISTS_THM] THEN
471 REWRITE_TAC[NOT_LE] THEN DISCH_TAC THEN GEN_TAC THEN
472 POP_ASSUM(X_CHOOSE_TAC `n:num` o SPEC `B + fn x 0`) THEN
473 EXISTS_TAC `n:num` THEN POP_ASSUM MP_TAC THEN
474 ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[NOT_LT; ADD_ASSOC; LE_ADDR] THEN
475 CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[NOT_LT] THEN
476 DISCH_THEN(MATCH_MP_TAC o LE_IMP) THEN REWRITE_TAC[ADD_ASSOC; LE_ADD]);;
478 let NADD_LE_TOTAL = prove
479 (`!x y. x <<= y \/ y <<= x`,
480 REPEAT GEN_TAC THEN GEN_REWRITE_TAC I [TAUT `a <=> ~ ~ a`] THEN
481 X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
482 X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
483 PURE_ONCE_REWRITE_TAC[DE_MORGAN_THM] THEN
484 DISCH_THEN(MP_TAC o end_itlist CONJ o
485 map (MATCH_MP NADD_LE_TOTAL_LEMMA) o CONJUNCTS) THEN
486 REWRITE_TAC[AND_FORALL_THM] THEN DISCH_THEN(MP_TAC o SPEC `B1 + B2`) THEN
487 REWRITE_TAC[RIGHT_AND_EXISTS_THM] THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
488 DISCH_THEN(X_CHOOSE_THEN `m:num` (X_CHOOSE_THEN `n:num` MP_TAC)) THEN
489 DISCH_THEN(MP_TAC o MATCH_MP
490 (ITAUT `(~a /\ b) /\ (~c /\ d) ==> ~(c \/ ~b) /\ ~(a \/ ~d)`)) THEN
491 REWRITE_TAC[NOT_LT; GSYM LE_MULT_LCANCEL] THEN REWRITE_TAC[NOT_LE] THEN
492 DISCH_THEN(MP_TAC o MATCH_MP LT_ADD2) THEN REWRITE_TAC[NOT_LT] THEN
493 REWRITE_TAC[LEFT_ADD_DISTRIB] THEN
494 ONCE_REWRITE_TAC[AC ADD_AC
495 `(a + b + c) + (d + e + f) = (d + b + e) + (a + c + f)`] THEN
496 MATCH_MP_TAC LE_ADD2 THEN REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
497 CONJ_TAC THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [MULT_SYM] THEN
498 RULE_ASSUM_TAC(REWRITE_RULE[DIST_LE_CASES]) THEN ASM_REWRITE_TAC[]);;
500 let NADD_ARCH = prove
502 REWRITE_TAC[nadd_le; NADD_OF_NUM; NADD_BOUND]);;
504 let NADD_OF_NUM_LE = prove
505 (`!m n. (&m <<= &n) <=> m <= n`,
506 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_OF_NUM] THEN
507 REWRITE_TAC[BOUNDS_LINEAR]);;
509 (* ------------------------------------------------------------------------- *)
511 (* ------------------------------------------------------------------------- *)
513 override_interface ("++",`nadd_add:nadd->nadd->nadd`);;
515 let nadd_add = new_definition
516 `x ++ y = afn(\n. fn x n + fn y n)`;;
519 (`!x y. fn(x ++ y) = \n. fn x n + fn y n`,
521 REWRITE_TAC[nadd_add; GSYM nadd_rep; is_nadd] THEN
522 X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
523 X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
524 EXISTS_TAC `B1 + B2` THEN MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN
525 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LEFT_ADD_DISTRIB] THEN
526 MATCH_MP_TAC (LE_IMP DIST_ADD2) THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
527 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
529 let NADD_ADD_WELLDEF = prove
530 (`!x x' y y'. x === x' /\ y === y' ==> (x ++ y === x' ++ y')`,
531 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD] THEN
532 DISCH_THEN(CONJUNCTS_THEN2
533 (X_CHOOSE_TAC `B1:num`) (X_CHOOSE_TAC `B2:num`)) THEN
534 EXISTS_TAC `B1 + B2` THEN X_GEN_TAC `n:num` THEN
535 MATCH_MP_TAC (LE_IMP DIST_ADD2) THEN
536 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[]);;
538 (* ------------------------------------------------------------------------- *)
539 (* Basic properties of addition. *)
540 (* ------------------------------------------------------------------------- *)
542 let NADD_ADD_SYM = prove
543 (`!x y. (x ++ y) === (y ++ x)`,
544 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_add] THEN
545 GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [ADD_SYM] THEN
546 REWRITE_TAC[NADD_EQ_REFL]);;
548 let NADD_ADD_ASSOC = prove
549 (`!x y z. (x ++ (y ++ z)) === ((x ++ y) ++ z)`,
550 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[nadd_add] THEN
551 REWRITE_TAC[NADD_ADD; ADD_ASSOC; NADD_EQ_REFL]);;
553 let NADD_ADD_LID = prove
554 (`!x. (&0 ++ x) === x`,
555 GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD; NADD_OF_NUM] THEN
556 REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES; DIST_REFL; LE_0]);;
558 let NADD_ADD_LCANCEL = prove
559 (`!x y z. (x ++ y) === (x ++ z) ==> y === z`,
560 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_ADD; DIST_LADD]);;
562 let NADD_LE_ADD = prove
563 (`!x y. x <<= (x ++ y)`,
564 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_ADD] THEN
565 EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; LE_ADD]);;
567 let NADD_LE_EXISTS = prove
568 (`!x y. x <<= y ==> ?d. y === x ++ d`,
569 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le] THEN
570 DISCH_THEN(X_CHOOSE_THEN `B:num` MP_TAC) THEN
571 REWRITE_TAC[LE_EXISTS; SKOLEM_THM] THEN
572 DISCH_THEN(X_CHOOSE_THEN `d:num->num` (ASSUME_TAC o GSYM)) THEN
573 EXISTS_TAC `afn d` THEN REWRITE_TAC[nadd_eq; NADD_ADD] THEN
574 EXISTS_TAC `B:num` THEN X_GEN_TAC `n:num` THEN
575 SUBGOAL_THEN `fn(afn d) = d` SUBST1_TAC THENL
576 [REWRITE_TAC[GSYM nadd_rep; is_nadd] THEN
577 X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
578 X_CHOOSE_TAC `B2:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
579 EXISTS_TAC `B1 + (B2 + B)` THEN REPEAT GEN_TAC THEN
580 MATCH_MP_TAC(LE_IMP DIST_ADD2_REV) THEN
581 MAP_EVERY EXISTS_TAC [`m * fn x n`; `n * fn x m`] THEN
582 ONCE_REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
583 GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN
584 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
585 ONCE_REWRITE_TAC[ADD_SYM] THEN
586 ASM_REWRITE_TAC[GSYM LEFT_ADD_DISTRIB] THEN
587 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [LEFT_ADD_DISTRIB] THEN
588 MATCH_MP_TAC(LE_IMP DIST_ADD2) THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
589 GEN_REWRITE_TAC RAND_CONV [ADD_SYM] THEN MATCH_MP_TAC LE_ADD2 THEN
590 ONCE_REWRITE_TAC[ADD_SYM] THEN ASM_REWRITE_TAC[] THEN
591 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [MULT_SYM] THEN
592 REWRITE_TAC[GSYM DIST_LMUL; DIST_ADDBOUND; LE_MULT_LCANCEL];
593 ASM_REWRITE_TAC[DIST_RADD_0; LE_REFL]]);;
595 let NADD_OF_NUM_ADD = prove
596 (`!m n. &m ++ &n === &(m + n)`,
597 REWRITE_TAC[nadd_eq; NADD_OF_NUM; NADD_ADD] THEN
598 REWRITE_TAC[RIGHT_ADD_DISTRIB; DIST_REFL; LE_0]);;
600 (* ------------------------------------------------------------------------- *)
601 (* Multiplication. *)
602 (* ------------------------------------------------------------------------- *)
604 override_interface ("**",`nadd_mul:nadd->nadd->nadd`);;
606 let nadd_mul = new_definition
607 `x ** y = afn(\n. fn x (fn y n))`;;
610 (`!x y. fn(x ** y) = \n. fn x (fn y n)`,
612 REWRITE_TAC[nadd_mul; GSYM nadd_rep; is_nadd] THEN
613 X_CHOOSE_TAC `B:num` (SPEC `y:nadd` NADD_CAUCHY) THEN
614 X_CHOOSE_TAC `C:num` (SPEC `x:nadd` NADD_DIST) THEN
615 X_CHOOSE_TAC `D:num` (SPEC `x:nadd` NADD_MULTIPLICATIVE) THEN
616 MATCH_MP_TAC BOUNDS_NOTZERO THEN
617 REWRITE_TAC[MULT_CLAUSES; DIST_REFL] THEN
618 MAP_EVERY EXISTS_TAC [`D + C * B`; `D + D`] THEN
619 REPEAT GEN_TAC THEN MATCH_MP_TAC LE_TRANS THEN
620 EXISTS_TAC `(D * m + D) + (D * n + D) + C * B * (m + n)` THEN CONJ_TAC THENL
621 [MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
622 EXISTS_TAC `fn x (m * fn y n)` THEN
623 MATCH_MP_TAC LE_ADD2 THEN
624 ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN
625 MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
626 EXISTS_TAC `fn x (n * fn y m)` THEN
627 MATCH_MP_TAC LE_ADD2 THEN
628 ONCE_REWRITE_TAC[DIST_SYM] THEN ASM_REWRITE_TAC[] THEN
629 MATCH_MP_TAC LE_TRANS THEN
630 EXISTS_TAC `C * dist(m * fn y n,n * fn y m)` THEN
631 ASM_REWRITE_TAC[LE_MULT_LCANCEL];
632 MATCH_MP_TAC EQ_IMP_LE THEN
633 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; MULT_ASSOC; ADD_AC]]);;
635 (* ------------------------------------------------------------------------- *)
636 (* Properties of multiplication. *)
637 (* ------------------------------------------------------------------------- *)
639 let NADD_MUL_SYM = prove
640 (`!x y. (x ** y) === (y ** x)`,
641 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
642 X_CHOOSE_THEN `A1:num` MP_TAC (SPECL [`x:nadd`; `y:nadd`] NADD_ALTMUL) THEN
643 DISCH_THEN(X_CHOOSE_TAC `B1:num`) THEN
644 X_CHOOSE_THEN `A2:num` MP_TAC (SPECL [`y:nadd`; `x:nadd`] NADD_ALTMUL) THEN
645 DISCH_THEN(X_CHOOSE_TAC `B2:num`) THEN REWRITE_TAC[BOUNDS_DIVIDED] THEN
646 REWRITE_TAC[DIST_LMUL] THEN MAP_EVERY EXISTS_TAC [`A1 + A2`; `B1 + B2`] THEN
647 GEN_TAC THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
648 ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + (c + d) = (a + c) + (b + d)`] THEN
649 MATCH_MP_TAC (LE_IMP DIST_TRIANGLE) THEN
650 EXISTS_TAC `fn x n * fn y n` THEN
651 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
652 ONCE_REWRITE_TAC [DIST_SYM] THEN
653 GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV) [MULT_SYM] THEN
656 let NADD_MUL_ASSOC = prove
657 (`!x y z. (x ** (y ** z)) === ((x ** y) ** z)`,
658 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[nadd_mul] THEN
659 REWRITE_TAC[NADD_MUL; NADD_EQ_REFL]);;
661 let NADD_MUL_LID = prove
662 (`!x. (&1 ** x) === x`,
663 REWRITE_TAC[NADD_OF_NUM; nadd_mul; MULT_CLAUSES] THEN
664 REWRITE_TAC[nadd_abs; NADD_EQ_REFL; ETA_AX]);;
666 let NADD_LDISTRIB = prove
667 (`!x y z. x ** (y ++ z) === (x ** y) ++ (x ** z)`,
668 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq] THEN
669 REWRITE_TAC[NADD_ADD; NADD_MUL] THEN
670 X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_ADDITIVE) THEN
671 EXISTS_TAC `B:num` THEN ASM_REWRITE_TAC[]);;
673 let NADD_MUL_WELLDEF_LEMMA = prove
674 (`!x y y'. y === y' ==> (x ** y) === (x ** y')`,
675 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
676 DISCH_THEN(X_CHOOSE_TAC `B1:num`) THEN
677 X_CHOOSE_TAC `B2:num` (SPEC `x:nadd` NADD_DIST) THEN
678 EXISTS_TAC `B2 * B1` THEN X_GEN_TAC `n:num` THEN
679 MATCH_MP_TAC LE_TRANS THEN
680 EXISTS_TAC `B2 * dist(fn y n,fn y' n)` THEN
681 ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
683 let NADD_MUL_WELLDEF = prove
684 (`!x x' y y'. x === x' /\ y === y'
685 ==> (x ** y) === (x' ** y')`,
686 REPEAT GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC NADD_EQ_TRANS THEN
687 EXISTS_TAC `x' ** y` THEN CONJ_TAC THENL
688 [MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ** x'` THEN
689 REWRITE_TAC[NADD_MUL_SYM] THEN MATCH_MP_TAC NADD_EQ_TRANS THEN
690 EXISTS_TAC `y ** x` THEN REWRITE_TAC[NADD_MUL_SYM]; ALL_TAC] THEN
691 MATCH_MP_TAC NADD_MUL_WELLDEF_LEMMA THEN ASM_REWRITE_TAC[]);;
693 let NADD_OF_NUM_MUL = prove
694 (`!m n. &m ** &n === &(m * n)`,
695 REWRITE_TAC[nadd_eq; NADD_OF_NUM; NADD_MUL] THEN
696 REWRITE_TAC[MULT_ASSOC; DIST_REFL; LE_0]);;
698 (* ------------------------------------------------------------------------- *)
699 (* A few handy lemmas. *)
700 (* ------------------------------------------------------------------------- *)
702 let NADD_LE_0 = prove
705 REWRITE_TAC[nadd_le; NADD_OF_NUM; MULT_CLAUSES; LE_0]);;
707 let NADD_EQ_IMP_LE = prove
708 (`!x y. x === y ==> x <<= y`,
710 REWRITE_TAC[nadd_eq; nadd_le; DIST_LE_CASES] THEN
711 DISCH_THEN(X_CHOOSE_TAC `B:num`) THEN EXISTS_TAC `B:num` THEN
714 let NADD_LE_LMUL = prove
715 (`!x y z. y <<= z ==> (x ** y) <<= (x ** z)`,
717 DISCH_THEN(X_CHOOSE_TAC `d:nadd` o MATCH_MP NADD_LE_EXISTS) THEN
718 MATCH_MP_TAC NADD_LE_TRANS THEN
719 EXISTS_TAC `x ** y ++ x ** d` THEN REWRITE_TAC[NADD_LE_ADD] THEN
720 MATCH_MP_TAC NADD_EQ_IMP_LE THEN
721 MATCH_MP_TAC NADD_EQ_TRANS THEN
722 EXISTS_TAC `x ** (y ++ d)` THEN
723 ONCE_REWRITE_TAC[NADD_EQ_SYM] THEN
724 REWRITE_TAC[NADD_LDISTRIB] THEN
725 MATCH_MP_TAC NADD_MUL_WELLDEF THEN
726 ASM_REWRITE_TAC[NADD_EQ_REFL]);;
728 let NADD_LE_RMUL = prove
729 (`!x y z. x <<= y ==> (x ** z) <<= (y ** z)`,
730 MESON_TAC[NADD_LE_LMUL; NADD_LE_WELLDEF; NADD_MUL_SYM]);;
732 let NADD_LE_RADD = prove
733 (`!x y z. x ++ z <<= y ++ z <=> x <<= y`,
734 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_le; NADD_ADD] THEN
735 GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o RAND_CONV)
737 REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
738 GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o RAND_CONV)
739 [ADD_SYM] THEN REFL_TAC);;
741 let NADD_LE_LADD = prove
742 (`!x y z. x ++ y <<= x ++ z <=> y <<= z`,
743 MESON_TAC[NADD_LE_RADD; NADD_ADD_SYM; NADD_LE_WELLDEF]);;
745 let NADD_RDISTRIB = prove
746 (`!x y z. (x ++ y) ** z === x ** z ++ y ** z`,
747 MESON_TAC[NADD_LDISTRIB; NADD_MUL_SYM; NADD_ADD_WELLDEF;
748 NADD_EQ_TRANS; NADD_EQ_REFL; NADD_EQ_SYM]);;
750 (* ------------------------------------------------------------------------- *)
751 (* The Archimedean property in a more useful form. *)
752 (* ------------------------------------------------------------------------- *)
754 let NADD_ARCH_MULT = prove
755 (`!x k. ~(x === &0) ==> ?N. &k <<= &N ** x`,
756 REPEAT GEN_TAC THEN REWRITE_TAC[nadd_eq; nadd_le; NOT_EXISTS_THM] THEN
757 X_CHOOSE_TAC `B:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
758 DISCH_THEN(MP_TAC o SPEC `B + k`) THEN
759 REWRITE_TAC[NOT_FORALL_THM; NADD_OF_NUM] THEN
760 REWRITE_TAC[MULT_CLAUSES; DIST_RZERO; NOT_LE] THEN
761 DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN
762 MAP_EVERY EXISTS_TAC [`N:num`; `B * N`] THEN X_GEN_TAC `i:num` THEN
763 REWRITE_TAC[NADD_MUL; NADD_OF_NUM] THEN
764 MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL LE_ADD_RCANCEL)))) THEN
765 EXISTS_TAC `B * i` THEN
766 REWRITE_TAC[GSYM ADD_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
767 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `i * fn x N` THEN
768 RULE_ASSUM_TAC(REWRITE_RULE[DIST_LE_CASES]) THEN ASM_REWRITE_TAC[] THEN
769 REWRITE_TAC[GSYM RIGHT_ADD_DISTRIB] THEN
770 GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
771 REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
772 MATCH_MP_TAC LT_IMP_LE THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
773 FIRST_ASSUM ACCEPT_TAC);;
775 let NADD_ARCH_ZERO = prove
776 (`!x k. (!n. &n ** x <<= k) ==> (x === &0)`,
777 REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN DISCH_TAC THEN
778 REWRITE_TAC[NOT_FORALL_THM] THEN
779 X_CHOOSE_TAC `p:num` (SPEC `k:nadd` NADD_ARCH) THEN
780 FIRST_ASSUM(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
781 DISCH_THEN(X_CHOOSE_TAC `N:num` o SPEC `p:num`) THEN
782 EXISTS_TAC `N + 1` THEN DISCH_TAC THEN UNDISCH_TAC `~(x === &0)` THEN
783 REWRITE_TAC[GSYM NADD_LE_ANTISYM; NADD_LE_0] THEN
784 MATCH_MP_TAC(GEN_ALL(fst(EQ_IMP_RULE(SPEC_ALL NADD_LE_RADD)))) THEN
785 EXISTS_TAC `&N ** x` THEN MATCH_MP_TAC NADD_LE_TRANS THEN
786 EXISTS_TAC `k:nadd` THEN CONJ_TAC THENL
787 [SUBGOAL_THEN `&(N + 1) ** x === x ++ &N ** x` MP_TAC THENL
788 [ONCE_REWRITE_TAC[ADD_SYM] THEN
789 MATCH_MP_TAC NADD_EQ_TRANS THEN
790 EXISTS_TAC `&1 ** x ++ &N ** x` THEN CONJ_TAC THENL
791 [MATCH_MP_TAC NADD_EQ_TRANS THEN
792 EXISTS_TAC `(&1 ++ &N) ** x` THEN CONJ_TAC THENL
793 [MESON_TAC[NADD_OF_NUM_ADD; NADD_MUL_WELLDEF; NADD_EQ_REFL;
795 MESON_TAC[NADD_RDISTRIB; NADD_MUL_SYM; NADD_EQ_SYM; NADD_EQ_TRANS]];
796 MESON_TAC[NADD_ADD_WELLDEF; NADD_EQ_REFL; NADD_MUL_LID]];
797 ASM_MESON_TAC[NADD_LE_WELLDEF; NADD_EQ_REFL]];
798 ASM_MESON_TAC[NADD_LE_TRANS; NADD_LE_WELLDEF; NADD_EQ_REFL;
801 let NADD_ARCH_LEMMA = prove
802 (`!x y z. (!n. &n ** x <<= &n ** y ++ z) ==> x <<= y`,
803 REPEAT STRIP_TAC THEN
804 DISJ_CASES_TAC(SPECL [`x:nadd`; `y:nadd`] NADD_LE_TOTAL) THEN
805 ASM_REWRITE_TAC[] THEN
806 FIRST_ASSUM(X_CHOOSE_TAC `d:nadd` o MATCH_MP NADD_LE_EXISTS) THEN
807 MATCH_MP_TAC NADD_EQ_IMP_LE THEN
808 MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ++ d` THEN
809 ASM_REWRITE_TAC[] THEN
810 MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC `y ++ &0` THEN CONJ_TAC THENL
811 [MATCH_MP_TAC NADD_ADD_WELLDEF THEN REWRITE_TAC[NADD_EQ_REFL] THEN
812 MATCH_MP_TAC NADD_ARCH_ZERO THEN EXISTS_TAC `z:nadd` THEN
813 ASM_MESON_TAC[NADD_MUL_WELLDEF; NADD_LE_WELLDEF; NADD_LDISTRIB;
814 NADD_LE_LADD; NADD_EQ_REFL];
815 ASM_MESON_TAC[NADD_ADD_LID; NADD_ADD_WELLDEF; NADD_EQ_TRANS;
818 (* ------------------------------------------------------------------------- *)
820 (* ------------------------------------------------------------------------- *)
822 let NADD_COMPLETE = prove
823 (`!P. (?x. P x) /\ (?M. !x. P x ==> x <<= M) ==>
824 ?M. (!x. P x ==> x <<= M) /\
825 !M'. (!x. P x ==> x <<= M') ==> M <<= M'`,
826 GEN_TAC THEN DISCH_THEN
827 (CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:nadd`) (X_CHOOSE_TAC `m:nadd`)) THEN
829 `!n. ?r. (?x. P x /\ &r <<= &n ** x) /\
830 !r'. (?x. P x /\ &r' <<= &n ** x) ==> r' <= r` MP_TAC THENL
831 [GEN_TAC THEN REWRITE_TAC[GSYM num_MAX] THEN CONJ_TAC THENL
832 [MAP_EVERY EXISTS_TAC [`0`; `a:nadd`] THEN ASM_REWRITE_TAC[NADD_LE_0];
833 X_CHOOSE_TAC `N:num` (SPEC `m:nadd` NADD_ARCH) THEN
834 EXISTS_TAC `n * N` THEN X_GEN_TAC `p:num` THEN
835 DISCH_THEN(X_CHOOSE_THEN `w:nadd` STRIP_ASSUME_TAC) THEN
836 ONCE_REWRITE_TAC[GSYM NADD_OF_NUM_LE] THEN
837 MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** w` THEN
838 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NADD_LE_TRANS THEN
839 EXISTS_TAC `&n ** &N` THEN CONJ_TAC THENL
840 [MATCH_MP_TAC NADD_LE_LMUL THEN MATCH_MP_TAC NADD_LE_TRANS THEN
841 EXISTS_TAC `m:nadd` THEN ASM_REWRITE_TAC[] THEN
842 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
843 MATCH_MP_TAC NADD_EQ_IMP_LE THEN
844 MATCH_ACCEPT_TAC NADD_OF_NUM_MUL]];
845 ONCE_REWRITE_TAC[SKOLEM_THM] THEN
846 DISCH_THEN(X_CHOOSE_THEN `r:num->num`
847 (fun th -> let th1,th2 = CONJ_PAIR(SPEC `n:num` th) in
848 MAP_EVERY (MP_TAC o GEN `n:num`) [th1; th2])) THEN
849 DISCH_THEN(MP_TAC o GEN `n:num` o SPECL [`n:num`; `SUC(r(n:num))`]) THEN
850 REWRITE_TAC[LE_SUC_LT; LT_REFL; NOT_EXISTS_THM] THEN
851 DISCH_THEN(ASSUME_TAC o GENL [`n:num`; `x:nadd`] o MATCH_MP
852 (ITAUT `(a \/ b) /\ ~(c /\ b) ==> c ==> a`) o CONJ
853 (SPECL [`&n ** x`; `&(SUC(r(n:num)))`] NADD_LE_TOTAL) o SPEC_ALL) THEN
855 SUBGOAL_THEN `!n i. i * r(n) <= n * r(i) + n` ASSUME_TAC THENL
857 FIRST_ASSUM(X_CHOOSE_THEN `x:nadd` STRIP_ASSUME_TAC o SPEC `n:num`) THEN
858 ONCE_REWRITE_TAC[GSYM NADD_OF_NUM_LE] THEN
859 MATCH_MP_TAC NADD_LE_TRANS THEN
860 EXISTS_TAC `&i ** &n ** x` THEN CONJ_TAC THENL
861 [MATCH_MP_TAC NADD_LE_TRANS THEN
862 EXISTS_TAC `&i ** &(r(n:num))` THEN CONJ_TAC THENL
863 [MATCH_MP_TAC NADD_EQ_IMP_LE THEN
864 ONCE_REWRITE_TAC[NADD_EQ_SYM] THEN MATCH_ACCEPT_TAC NADD_OF_NUM_MUL;
865 MATCH_MP_TAC NADD_LE_LMUL THEN ASM_REWRITE_TAC[]];
866 MATCH_MP_TAC NADD_LE_TRANS THEN
867 EXISTS_TAC `&n ** &(SUC(r(i:num)))` THEN CONJ_TAC THENL
868 [MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** &i ** x` THEN
870 [MATCH_MP_TAC NADD_EQ_IMP_LE THEN
871 MATCH_MP_TAC NADD_EQ_TRANS THEN
872 EXISTS_TAC `(&i ** &n) ** x` THEN
873 REWRITE_TAC[NADD_MUL_ASSOC] THEN
874 MATCH_MP_TAC NADD_EQ_TRANS THEN
875 EXISTS_TAC `(&n ** &i) ** x` THEN
876 REWRITE_TAC[ONCE_REWRITE_RULE[NADD_EQ_SYM] NADD_MUL_ASSOC] THEN
877 MATCH_MP_TAC NADD_MUL_WELLDEF THEN
878 REWRITE_TAC[NADD_MUL_SYM; NADD_EQ_REFL];
879 MATCH_MP_TAC NADD_LE_LMUL THEN
880 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]];
881 ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[GSYM MULT_SUC] THEN
882 MATCH_MP_TAC NADD_EQ_IMP_LE THEN
883 REWRITE_TAC[NADD_OF_NUM_MUL]]]; ALL_TAC] THEN
884 EXISTS_TAC `afn r` THEN SUBGOAL_THEN `fn(afn r) = r` ASSUME_TAC THENL
885 [REWRITE_TAC[GSYM nadd_rep] THEN REWRITE_TAC[is_nadd; DIST_LE_CASES] THEN
886 EXISTS_TAC `1` THEN REWRITE_TAC[MULT_CLAUSES] THEN
887 REWRITE_TAC[FORALL_AND_THM] THEN
888 GEN_REWRITE_TAC RAND_CONV [SWAP_FORALL_THM] THEN
889 GEN_REWRITE_TAC (LAND_CONV o funpow 2 BINDER_CONV o
890 funpow 2 RAND_CONV) [ADD_SYM] THEN
891 REWRITE_TAC[] THEN MAP_EVERY X_GEN_TAC [`i:num`; `n:num`] THEN
892 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n * r(i:num) + n` THEN
893 ASM_REWRITE_TAC[ADD_ASSOC; LE_ADD]; ALL_TAC] THEN
895 [X_GEN_TAC `x:nadd` THEN DISCH_TAC THEN
896 MATCH_MP_TAC NADD_ARCH_LEMMA THEN
897 EXISTS_TAC `&2` THEN X_GEN_TAC `n:num` THEN
898 MATCH_MP_TAC NADD_LE_TRANS THEN
899 EXISTS_TAC `&(SUC(r(n:num)))` THEN CONJ_TAC THENL
900 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
901 ASM_REWRITE_TAC[nadd_le; NADD_ADD; NADD_MUL; NADD_OF_NUM] THEN
902 ONCE_REWRITE_TAC[ADD_SYM] THEN
903 REWRITE_TAC[ADD1; RIGHT_ADD_DISTRIB] THEN
904 REWRITE_TAC[MULT_2; MULT_CLAUSES; ADD_ASSOC; LE_ADD_RCANCEL] THEN
905 REWRITE_TAC[GSYM ADD_ASSOC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN
906 ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
907 MAP_EVERY EXISTS_TAC [`0`; `n:num`] THEN
908 X_GEN_TAC `i:num` THEN DISCH_TAC THEN
909 GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
910 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `n * r(i:num) + n` THEN
911 ASM_REWRITE_TAC[LE_ADD_LCANCEL; ADD_CLAUSES]];
912 X_GEN_TAC `z:nadd` THEN DISCH_TAC THEN
913 MATCH_MP_TAC NADD_ARCH_LEMMA THEN EXISTS_TAC `&1` THEN
914 X_GEN_TAC `n:num` THEN MATCH_MP_TAC NADD_LE_TRANS THEN
915 EXISTS_TAC `&(r(n:num)) ++ &1` THEN CONJ_TAC THENL
916 [ASM_REWRITE_TAC[nadd_le; NADD_ADD; NADD_MUL; NADD_OF_NUM] THEN
917 EXISTS_TAC `0` THEN REWRITE_TAC[ADD_CLAUSES; MULT_CLAUSES] THEN
918 GEN_TAC THEN GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [MULT_SYM] THEN
920 REWRITE_TAC[NADD_LE_RADD] THEN
921 FIRST_ASSUM(X_CHOOSE_THEN `x:nadd` MP_TAC o SPEC `n:num`) THEN
922 DISCH_THEN STRIP_ASSUME_TAC THEN
923 MATCH_MP_TAC NADD_LE_TRANS THEN EXISTS_TAC `&n ** x` THEN
924 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC NADD_LE_LMUL THEN
925 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]]);;
927 (* ------------------------------------------------------------------------- *)
928 (* A bit more on nearly-multiplicative functions. *)
929 (* ------------------------------------------------------------------------- *)
931 let NADD_UBOUND = prove
932 (`!x. ?B N. !n. N <= n ==> fn x n <= B * n`,
933 GEN_TAC THEN X_CHOOSE_THEN `A1:num`
934 (X_CHOOSE_TAC `A2:num`) (SPEC `x:nadd` NADD_BOUND) THEN
935 EXISTS_TAC `A1 + A2` THEN EXISTS_TAC `1` THEN
936 REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
937 EXISTS_TAC `A1 * n + A2` THEN ASM_REWRITE_TAC[] THEN
938 REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
939 GEN_REWRITE_TAC LAND_CONV [GSYM(el 3 (CONJUNCTS MULT_CLAUSES))] THEN
940 ASM_REWRITE_TAC[LE_MULT_LCANCEL]);;
942 let NADD_NONZERO = prove
943 (`!x. ~(x === &0) ==> ?N. !n. N <= n ==> ~(fn x n = 0)`,
944 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
945 DISCH_THEN(MP_TAC o SPEC `1`) THEN
946 REWRITE_TAC[nadd_le; NADD_MUL; NADD_OF_NUM; MULT_CLAUSES] THEN
947 DISCH_THEN(X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `A2:num`)) THEN
948 EXISTS_TAC `A2 + 1` THEN X_GEN_TAC `n:num` THEN REPEAT DISCH_TAC THEN
949 FIRST_ASSUM(UNDISCH_TAC o check is_forall o concl) THEN
950 REWRITE_TAC[NOT_FORALL_THM; NOT_LE; GSYM LE_SUC_LT; ADD1] THEN
951 EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[MULT_CLAUSES; ADD_CLAUSES]);;
953 let NADD_LBOUND = prove
954 (`!x. ~(x === &0) ==> ?A N. !n. N <= n ==> n <= A * fn x n`,
955 GEN_TAC THEN DISCH_TAC THEN
956 FIRST_ASSUM(X_CHOOSE_TAC `N:num` o MATCH_MP NADD_NONZERO) THEN
957 FIRST_ASSUM(MP_TAC o MATCH_MP NADD_ARCH_MULT) THEN
958 DISCH_THEN(MP_TAC o SPEC `1`) THEN
959 REWRITE_TAC[nadd_le; NADD_MUL; NADD_OF_NUM; MULT_CLAUSES] THEN
960 DISCH_THEN(X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `A2:num`)) THEN
961 EXISTS_TAC `A1 + A2` THEN EXISTS_TAC `N:num` THEN GEN_TAC THEN
962 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
963 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A1 * fn x n + A2` THEN
964 ASM_REWRITE_TAC[RIGHT_ADD_DISTRIB; LE_ADD_LCANCEL] THEN
965 GEN_REWRITE_TAC LAND_CONV [GSYM(el 3 (CONJUNCTS MULT_CLAUSES))] THEN
966 REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
967 REWRITE_TAC[GSYM(REWRITE_CONV[ARITH_SUC] `SUC 0`)] THEN
968 ASM_REWRITE_TAC[GSYM NOT_LT; LT]);;
970 (* ------------------------------------------------------------------------- *)
971 (* Auxiliary function for the multiplicative inverse. *)
972 (* ------------------------------------------------------------------------- *)
974 let nadd_rinv = new_definition
975 `nadd_rinv(x) = \n. (n * n) DIV (fn x n)`;;
977 let NADD_MUL_LINV_LEMMA0 = prove
978 (`!x. ~(x === &0) ==> ?A B. !n. nadd_rinv x n <= A * n + B`,
979 GEN_TAC THEN DISCH_TAC THEN ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
980 FIRST_ASSUM(MP_TAC o MATCH_MP NADD_LBOUND) THEN
981 DISCH_THEN(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `N:num`)) THEN
982 MAP_EVERY EXISTS_TAC [`A:num`; `0`; `SUC N`] THEN
983 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[ADD_CLAUSES] THEN
984 MP_TAC(SPECL [`nadd_rinv x n`; `A * n`; `n:num`] LE_MULT_RCANCEL) THEN
985 UNDISCH_TAC `SUC N <= n` THEN ASM_CASES_TAC `n = 0` THEN
986 ASM_REWRITE_TAC[LE; NOT_SUC] THEN DISCH_TAC THEN
987 DISCH_THEN(SUBST1_TAC o SYM) THEN
988 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `nadd_rinv x n * A * fn x n` THEN
989 ASM_REWRITE_TAC[LE_MULT_LCANCEL] THEN CONJ_TAC THENL
990 [DISJ2_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
991 EXISTS_TAC `SUC N` THEN ASM_REWRITE_TAC[LE; LE_REFL];
992 GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
993 REWRITE_TAC[GSYM MULT_ASSOC; LE_MULT_LCANCEL] THEN
994 DISJ2_TAC THEN ASM_CASES_TAC `fn x n = 0` THEN
995 ASM_REWRITE_TAC[MULT_CLAUSES; LE_0; nadd_rinv] THEN
996 FIRST_ASSUM(MP_TAC o MATCH_MP DIVISION) THEN
997 DISCH_THEN(fun t -> GEN_REWRITE_TAC RAND_CONV [CONJUNCT1(SPEC_ALL t)]) THEN
998 GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN REWRITE_TAC[LE_ADD]]);;
1000 let NADD_MUL_LINV_LEMMA1 = prove
1001 (`!x n. ~(fn x n = 0) ==> dist(fn x n * nadd_rinv(x) n, n * n) <= fn x n`,
1002 REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP DIVISION) THEN
1003 DISCH_THEN(CONJUNCTS_THEN2 SUBST1_TAC ASSUME_TAC o SPEC `n * n`) THEN
1004 REWRITE_TAC[nadd_rinv] THEN
1005 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
1006 REWRITE_TAC[DIST_RADD_0] THEN MATCH_MP_TAC LT_IMP_LE THEN
1007 FIRST_ASSUM MATCH_ACCEPT_TAC);;
1009 let NADD_MUL_LINV_LEMMA2 = prove
1010 (`!x. ~(x === &0) ==> ?N. !n. N <= n ==>
1011 dist(fn x n * nadd_rinv(x) n, n * n) <= fn x n`,
1012 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_NONZERO) THEN
1013 DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
1014 REPEAT STRIP_TAC THEN MATCH_MP_TAC NADD_MUL_LINV_LEMMA1 THEN
1015 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
1017 let NADD_MUL_LINV_LEMMA3 = prove
1018 (`!x. ~(x === &0) ==> ?N. !m n. N <= n ==>
1019 dist(m * fn x m * fn x n * nadd_rinv(x) n,
1020 m * fn x m * n * n) <= m * fn x m * fn x n`,
1021 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA2) THEN
1022 DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
1023 REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM DIST_LMUL; MULT_ASSOC] THEN
1024 REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
1025 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;
1027 let NADD_MUL_LINV_LEMMA4 = prove
1028 (`!x. ~(x === &0) ==> ?N. !m n. N <= m /\ N <= n ==>
1029 (fn x m * fn x n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
1030 (m * n) * dist(m * fn x n,n * fn x m) + (fn x m * fn x n) * (m + n)`,
1031 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA3) THEN
1032 DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN
1033 REPEAT STRIP_TAC THEN REWRITE_TAC[DIST_LMUL; LEFT_ADD_DISTRIB] THEN
1034 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [DIST_SYM] THEN
1035 MATCH_MP_TAC DIST_TRIANGLES_LE THEN CONJ_TAC THENL
1036 [ANTE_RES_THEN(MP_TAC o SPEC `m:num`) (ASSUME `N <= n`);
1037 ANTE_RES_THEN(MP_TAC o SPEC `n:num`) (ASSUME `N <= m`)] THEN
1038 MATCH_MP_TAC EQ_IMP THEN REWRITE_TAC[MULT_AC]);;
1040 let NADD_MUL_LINV_LEMMA5 = prove
1041 (`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
1042 (fn x m * fn x n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
1043 B * (m * n) * (m + n)`,
1044 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA4) THEN
1045 DISCH_THEN(X_CHOOSE_TAC `N1:num`) THEN
1046 X_CHOOSE_TAC `B1:num` (SPEC `x:nadd` NADD_CAUCHY) THEN
1047 X_CHOOSE_THEN `B2:num` (X_CHOOSE_TAC `N2:num`)
1048 (SPEC `x:nadd` NADD_UBOUND) THEN
1049 EXISTS_TAC `B1 + B2 * B2` THEN EXISTS_TAC `N1 + N2` THEN
1050 REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
1051 EXISTS_TAC `(m * n) * dist(m * fn x n,n * fn x m) +
1052 (fn x m * fn x n) * (m + n)` THEN
1054 [FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC THEN
1055 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
1056 ASM_REWRITE_TAC[LE_ADD; LE_ADDR];
1057 REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN MATCH_MP_TAC LE_ADD2] THEN
1059 [GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN
1060 GEN_REWRITE_TAC RAND_CONV [GSYM MULT_ASSOC] THEN
1061 GEN_REWRITE_TAC (funpow 2 RAND_CONV) [MULT_SYM] THEN
1062 ASM_REWRITE_TAC[LE_MULT_LCANCEL];
1063 ONCE_REWRITE_TAC[AC MULT_AC
1064 `(a * b) * (c * d) * e = ((a * c) * (b * d)) * e`] THEN
1065 REWRITE_TAC[LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1066 MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN
1067 FIRST_ASSUM MATCH_MP_TAC THEN
1068 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
1069 ASM_REWRITE_TAC[LE_ADD; LE_ADDR]]);;
1071 let NADD_MUL_LINV_LEMMA6 = prove
1072 (`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
1073 (m * n) * dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <=
1074 B * (m * n) * (m + n)`,
1075 GEN_TAC THEN DISCH_TAC THEN
1076 FIRST_ASSUM(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA5) THEN
1077 DISCH_THEN(X_CHOOSE_THEN `B1:num` (X_CHOOSE_TAC `N1:num`)) THEN
1078 FIRST_ASSUM(MP_TAC o MATCH_MP NADD_LBOUND) THEN
1079 DISCH_THEN(X_CHOOSE_THEN `B2:num` (X_CHOOSE_TAC `N2:num`)) THEN
1080 EXISTS_TAC `B1 * B2 * B2` THEN EXISTS_TAC `N1 + N2` THEN
1081 REPEAT STRIP_TAC THEN MATCH_MP_TAC LE_TRANS THEN
1082 EXISTS_TAC `(B2 * B2) * (fn x m * fn x n) *
1083 dist (m * nadd_rinv x n,n * nadd_rinv x m)` THEN
1085 [REWRITE_TAC[MULT_ASSOC; LE_MULT_RCANCEL] THEN DISJ1_TAC THEN
1086 ONCE_REWRITE_TAC[AC MULT_AC `((a * b) * c) * d = (a * c) * (b * d)`] THEN
1087 MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN FIRST_ASSUM MATCH_MP_TAC;
1088 ONCE_REWRITE_TAC[AC MULT_AC
1089 `(a * b * c) * (d * e) * f = (b * c) * (a * (d * e) * f)`] THEN
1090 REWRITE_TAC[LE_MULT_LCANCEL] THEN DISJ2_TAC THEN
1091 FIRST_ASSUM MATCH_MP_TAC THEN CONJ_TAC] THEN
1092 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N1 + N2` THEN
1093 ASM_REWRITE_TAC[LE_ADD; LE_ADDR]);;
1095 let NADD_MUL_LINV_LEMMA7 = prove
1096 (`!x. ~(x === &0) ==> ?B N. !m n. N <= m /\ N <= n ==>
1097 dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= B * (m + n)`,
1098 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA6) THEN
1099 DISCH_THEN(X_CHOOSE_THEN `B:num` (X_CHOOSE_TAC `N:num`)) THEN
1100 MAP_EVERY EXISTS_TAC [`B:num`; `N + 1`] THEN
1101 MAP_EVERY X_GEN_TAC [`m:num`; `n:num`] THEN STRIP_TAC THEN
1102 SUBGOAL_THEN `N <= m /\ N <= n` MP_TAC THENL
1103 [CONJ_TAC THEN MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N + 1` THEN
1104 ASM_REWRITE_TAC[LE_ADD];
1105 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1106 ONCE_REWRITE_TAC[AC MULT_AC `a * b * c = b * a * c`] THEN
1107 REWRITE_TAC[LE_MULT_LCANCEL] THEN
1108 DISCH_THEN(DISJ_CASES_THEN2 MP_TAC ACCEPT_TAC) THEN
1109 CONV_TAC CONTRAPOS_CONV THEN DISCH_THEN(K ALL_TAC) THEN
1110 ONCE_REWRITE_TAC[GSYM(CONJUNCT1 LE)] THEN
1111 REWRITE_TAC[NOT_LE; GSYM LE_SUC_LT] THEN
1112 REWRITE_TAC[EQT_ELIM(REWRITE_CONV[ARITH] `SUC 0 = 1 * 1`)] THEN
1113 MATCH_MP_TAC LE_MULT2 THEN CONJ_TAC THEN
1114 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `N + 1` THEN
1115 ASM_REWRITE_TAC[LE_ADDR]]);;
1117 let NADD_MUL_LINV_LEMMA7a = prove
1118 (`!x. ~(x === &0) ==> !N. ?A B. !m n. m <= N ==>
1119 dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= A * n + B`,
1120 GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA0) THEN
1121 DISCH_THEN(X_CHOOSE_THEN `A0:num` (X_CHOOSE_TAC `B0:num`)) THEN
1123 [MAP_EVERY EXISTS_TAC [`nadd_rinv x 0`; `0`] THEN
1124 REPEAT GEN_TAC THEN REWRITE_TAC[LE] THEN DISCH_THEN SUBST1_TAC THEN
1125 REWRITE_TAC[MULT_CLAUSES; DIST_LZERO; ADD_CLAUSES] THEN
1126 GEN_REWRITE_TAC RAND_CONV [MULT_SYM] THEN MATCH_ACCEPT_TAC LE_REFL;
1127 FIRST_ASSUM(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `B:num`)) THEN
1128 EXISTS_TAC `A + (nadd_rinv(x)(SUC N) + SUC N * A0)` THEN
1129 EXISTS_TAC `SUC N * B0 + B` THEN
1130 REPEAT GEN_TAC THEN REWRITE_TAC[LE] THEN
1131 DISCH_THEN(DISJ_CASES_THEN2 SUBST1_TAC ASSUME_TAC) THENL
1132 [MATCH_MP_TAC LE_TRANS THEN
1133 EXISTS_TAC `SUC N * nadd_rinv x n + n * nadd_rinv x (SUC N)` THEN
1134 REWRITE_TAC[DIST_ADDBOUND] THEN REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1135 ONCE_REWRITE_TAC[AC ADD_AC
1136 `(a + b + c) + d + e = (c + d) + (b + a + e)`] THEN
1137 MATCH_MP_TAC LE_ADD2 THEN CONJ_TAC THENL
1138 [REWRITE_TAC[GSYM MULT_ASSOC; GSYM LEFT_ADD_DISTRIB] THEN
1139 ASM_REWRITE_TAC[LE_MULT_LCANCEL];
1140 GEN_REWRITE_TAC LAND_CONV [MULT_SYM] THEN
1141 MATCH_ACCEPT_TAC LE_ADD];
1142 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN CONJ_TAC THENL
1143 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1144 REWRITE_TAC[ADD_ASSOC; LE_ADD_RCANCEL] THEN
1145 REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]]]]);;
1147 let NADD_MUL_LINV_LEMMA8 = prove
1148 (`!x. ~(x === &0) ==>
1149 ?B. !m n. dist(m * nadd_rinv(x) n,n * nadd_rinv(x) m) <= B * (m + n)`,
1150 GEN_TAC THEN DISCH_TAC THEN
1151 FIRST_ASSUM(MP_TAC o MATCH_MP NADD_MUL_LINV_LEMMA7) THEN
1152 DISCH_THEN(X_CHOOSE_THEN `B0:num` (X_CHOOSE_TAC `N:num`)) THEN
1153 FIRST_ASSUM(MP_TAC o SPEC `N:num` o MATCH_MP NADD_MUL_LINV_LEMMA7a) THEN
1154 DISCH_THEN(X_CHOOSE_THEN `A:num` (X_CHOOSE_TAC `B:num`)) THEN
1155 MATCH_MP_TAC BOUNDS_NOTZERO THEN REWRITE_TAC[DIST_REFL] THEN
1156 EXISTS_TAC `A + B0` THEN EXISTS_TAC `B:num` THEN REPEAT GEN_TAC THEN
1157 DISJ_CASES_THEN2 ASSUME_TAC MP_TAC (SPECL [`N:num`; `m:num`] LE_CASES) THENL
1158 [DISJ_CASES_THEN2 ASSUME_TAC MP_TAC (SPECL [`N:num`; `n:num`] LE_CASES)
1160 [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `B0 * (m + n)` THEN CONJ_TAC THENL
1161 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1162 GEN_REWRITE_TAC (RAND_CONV o funpow 2 LAND_CONV) [ADD_SYM] THEN
1163 REWRITE_TAC[RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC; LE_ADD]];
1164 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
1165 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * m + B` THEN
1166 ONCE_REWRITE_TAC[DIST_SYM] THEN
1167 ASM_REWRITE_TAC[LE_ADD_RCANCEL] THEN
1168 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC;
1170 DISCH_THEN(ANTE_RES_THEN ASSUME_TAC) THEN
1171 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `A * n + B` THEN
1172 ASM_REWRITE_TAC[LE_ADD_RCANCEL] THEN
1173 GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [ADD_SYM] THEN
1174 REWRITE_TAC[LEFT_ADD_DISTRIB; RIGHT_ADD_DISTRIB; GSYM ADD_ASSOC;
1177 (* ------------------------------------------------------------------------- *)
1178 (* Now the multiplicative inverse proper. *)
1179 (* ------------------------------------------------------------------------- *)
1181 let nadd_inv = new_definition
1182 `nadd_inv(x) = if x === &0 then &0 else afn(nadd_rinv x)`;;
1184 override_interface ("inv",`nadd_inv:nadd->nadd`);;
1186 let NADD_INV = prove
1187 (`!x. fn(nadd_inv x) = if x === &0 then (\n. 0) else nadd_rinv x`,
1188 GEN_TAC THEN REWRITE_TAC[nadd_inv] THEN
1189 ASM_CASES_TAC `x === &0` THEN ASM_REWRITE_TAC[NADD_OF_NUM; MULT_CLAUSES] THEN
1190 REWRITE_TAC[GSYM nadd_rep; is_nadd] THEN
1191 MATCH_MP_TAC NADD_MUL_LINV_LEMMA8 THEN POP_ASSUM ACCEPT_TAC);;
1193 let NADD_MUL_LINV = prove
1194 (`!x. ~(x === &0) ==> inv(x) ** x === &1`,
1195 GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[nadd_eq; NADD_MUL] THEN
1196 ONCE_REWRITE_TAC[BOUNDS_DIVIDED] THEN
1197 X_CHOOSE_THEN `A1:num` (X_CHOOSE_TAC `B1:num`)
1198 (SPECL [`inv(x)`; `x:nadd`] NADD_ALTMUL) THEN
1199 REWRITE_TAC[DIST_LMUL; NADD_OF_NUM; MULT_CLAUSES] THEN
1200 FIRST_ASSUM(X_CHOOSE_TAC `N:num` o MATCH_MP NADD_MUL_LINV_LEMMA2) THEN
1201 X_CHOOSE_THEN `A':num` (X_CHOOSE_TAC `B':num`)
1202 (SPEC `x:nadd` NADD_BOUND) THEN
1203 SUBGOAL_THEN `?A2 B2. !n. dist(fn x n * nadd_rinv x n,n * n) <= A2 * n + B2`
1204 STRIP_ASSUME_TAC THENL
1205 [EXISTS_TAC `A':num` THEN ONCE_REWRITE_TAC[BOUNDS_IGNORE] THEN
1206 MAP_EVERY EXISTS_TAC [`B':num`; `N:num`] THEN REPEAT STRIP_TAC THEN
1207 MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `fn x n` THEN ASM_REWRITE_TAC[] THEN
1208 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1209 MAP_EVERY EXISTS_TAC [`A1 + A2`; `B1 + B2`] THEN
1210 GEN_TAC THEN MATCH_MP_TAC DIST_TRIANGLE_LE THEN
1211 EXISTS_TAC `fn (inv x) n * fn x n` THEN
1212 REWRITE_TAC[RIGHT_ADD_DISTRIB] THEN
1213 ONCE_REWRITE_TAC[AC ADD_AC `(a + b) + c + d = (a + c) + (b + d)`] THEN
1214 MATCH_MP_TAC LE_ADD2 THEN ASM_REWRITE_TAC[] THEN
1215 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o LAND_CONV) [MULT_SYM] THEN
1216 ASM_REWRITE_TAC[NADD_INV]]);;
1218 let NADD_INV_0 = prove
1220 REWRITE_TAC[nadd_inv; NADD_EQ_REFL]);;
1222 (* ------------------------------------------------------------------------- *)
1223 (* Welldefinedness follows from already established principles because if *)
1224 (* x = y then y' = y' 1 = y' (x' x) = y' (x' y) = (y' y) x' = 1 x' = x' *)
1225 (* ------------------------------------------------------------------------- *)
1227 let NADD_INV_WELLDEF = prove
1228 (`!x y. x === y ==> inv(x) === inv(y)`,
1230 MATCH_MP_TAC NADD_EQ_TRANS THEN EXISTS_TAC tm THEN
1231 CONJ_TAC THENL [ALL_TAC; ASM_MESON_TAC ths] in
1232 REPEAT STRIP_TAC THEN
1233 ASM_CASES_TAC `x === &0` THENL
1234 [SUBGOAL_THEN `y === &0` ASSUME_TAC THENL
1235 [ASM_MESON_TAC[NADD_EQ_TRANS; NADD_EQ_SYM];
1236 ASM_REWRITE_TAC[nadd_inv; NADD_EQ_REFL]];
1237 SUBGOAL_THEN `~(y === &0)` ASSUME_TAC THENL
1238 [ASM_MESON_TAC[NADD_EQ_TRANS; NADD_EQ_SYM]; ALL_TAC]] THEN
1240 [NADD_MUL_SYM; NADD_MUL_LID; NADD_EQ_TRANS] THEN
1241 TAC `inv(y) ** (inv(x) ** x)`
1242 [NADD_MUL_LINV; NADD_MUL_WELLDEF; NADD_EQ_REFL] THEN
1243 TAC `inv(y) ** (inv(x) ** y)`
1244 [NADD_MUL_WELLDEF; NADD_EQ_REFL; NADD_EQ_SYM] THEN
1245 TAC `(inv(y) ** y) ** inv(x)`
1246 [NADD_MUL_ASSOC; NADD_MUL_SYM; NADD_EQ_TRANS;
1247 NADD_MUL_WELLDEF; NADD_EQ_REFL] THEN
1248 ASM_MESON_TAC[NADD_MUL_LINV; NADD_MUL_WELLDEF; NADD_EQ_REFL;
1249 NADD_MUL_LID; NADD_EQ_TRANS; NADD_EQ_SYM]);;
1251 (* ------------------------------------------------------------------------- *)
1252 (* Definition of the new type. *)
1253 (* ------------------------------------------------------------------------- *)
1256 define_quotient_type "hreal" ("mk_hreal","dest_hreal") `(===)`;;
1258 do_list overload_interface
1259 ["+",`hreal_add:hreal->hreal->hreal`;
1260 "*",`hreal_mul:hreal->hreal->hreal`;
1261 "<=",`hreal_le:hreal->hreal->bool`];;
1263 do_list override_interface
1264 ["&",`hreal_of_num:num->hreal`;
1265 "inv",`hreal_inv:hreal->hreal`];;
1267 let hreal_of_num,hreal_of_num_th =
1268 lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1269 "hreal_of_num" NADD_OF_NUM_WELLDEF;;
1271 let hreal_add,hreal_add_th =
1272 lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1273 "hreal_add" NADD_ADD_WELLDEF;;
1275 let hreal_mul,hreal_mul_th =
1276 lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1277 "hreal_mul" NADD_MUL_WELLDEF;;
1279 let hreal_le,hreal_le_th =
1280 lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1281 "hreal_le" NADD_LE_WELLDEF;;
1283 let hreal_inv,hreal_inv_th =
1284 lift_function (snd hreal_tybij) (NADD_EQ_REFL,NADD_EQ_TRANS)
1285 "hreal_inv" NADD_INV_WELLDEF;;
1287 let HREAL_COMPLETE =
1288 let th1 = ASSUME `(P:nadd->bool) = (\x. Q(mk_hreal((===) x)))` in
1289 let th2 = BETA_RULE(AP_THM th1 `x:nadd`) in
1290 let th3 = lift_theorem hreal_tybij
1291 (NADD_EQ_REFL,NADD_EQ_SYM,NADD_EQ_TRANS)
1292 [hreal_of_num_th; hreal_add_th; hreal_mul_th; hreal_le_th; th2]
1293 (SPEC_ALL NADD_COMPLETE) in
1294 let th4 = MATCH_MP (DISCH_ALL th3) (REFL `\x. Q(mk_hreal((===) x)):bool`) in
1295 CONV_RULE(GEN_ALPHA_CONV `P:hreal->bool`) (GEN_ALL th4);;
1297 let [HREAL_OF_NUM_EQ; HREAL_OF_NUM_LE; HREAL_OF_NUM_ADD; HREAL_OF_NUM_MUL;
1298 HREAL_LE_REFL; HREAL_LE_TRANS; HREAL_LE_ANTISYM; HREAL_LE_TOTAL;
1299 HREAL_LE_ADD; HREAL_LE_EXISTS; HREAL_ARCH; HREAL_ADD_SYM; HREAL_ADD_ASSOC;
1300 HREAL_ADD_LID; HREAL_ADD_LCANCEL; HREAL_MUL_SYM; HREAL_MUL_ASSOC;
1301 HREAL_MUL_LID; HREAL_ADD_LDISTRIB; HREAL_MUL_LINV; HREAL_INV_0] =
1302 map (lift_theorem hreal_tybij
1303 (NADD_EQ_REFL,NADD_EQ_SYM,NADD_EQ_TRANS)
1304 [hreal_of_num_th; hreal_add_th; hreal_mul_th;
1305 hreal_le_th; hreal_inv_th])
1306 [NADD_OF_NUM_EQ; NADD_OF_NUM_LE; NADD_OF_NUM_ADD; NADD_OF_NUM_MUL;
1307 NADD_LE_REFL; NADD_LE_TRANS; NADD_LE_ANTISYM; NADD_LE_TOTAL; NADD_LE_ADD;
1308 NADD_LE_EXISTS; NADD_ARCH; NADD_ADD_SYM; NADD_ADD_ASSOC; NADD_ADD_LID;
1309 NADD_ADD_LCANCEL; NADD_MUL_SYM; NADD_MUL_ASSOC; NADD_MUL_LID; NADD_LDISTRIB;
1310 NADD_MUL_LINV; NADD_INV_0];;
1312 (* ------------------------------------------------------------------------- *)
1313 (* Consequential theorems needed later. *)
1314 (* ------------------------------------------------------------------------- *)
1316 let HREAL_LE_EXISTS_DEF = prove
1317 (`!m n. m <= n <=> ?d. n = m + d`,
1318 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS] THEN
1319 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[HREAL_LE_ADD]);;
1321 let HREAL_EQ_ADD_LCANCEL = prove
1322 (`!m n p. (m + n = m + p) <=> (n = p)`,
1323 REPEAT GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[HREAL_ADD_LCANCEL] THEN
1324 DISCH_THEN SUBST1_TAC THEN REFL_TAC);;
1326 let HREAL_EQ_ADD_RCANCEL = prove
1327 (`!m n p. (m + p = n + p) <=> (m = n)`,
1328 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN REWRITE_TAC[HREAL_EQ_ADD_LCANCEL]);;
1330 let HREAL_LE_ADD_LCANCEL = prove
1331 (`!m n p. (m + n <= m + p) <=> (n <= p)`,
1332 REWRITE_TAC[HREAL_LE_EXISTS_DEF; GSYM HREAL_ADD_ASSOC;
1333 HREAL_EQ_ADD_LCANCEL]);;
1335 let HREAL_LE_ADD_RCANCEL = prove
1336 (`!m n p. (m + p <= n + p) <=> (m <= n)`,
1337 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN MATCH_ACCEPT_TAC HREAL_LE_ADD_LCANCEL);;
1339 let HREAL_ADD_RID = prove
1341 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN MATCH_ACCEPT_TAC HREAL_ADD_LID);;
1343 let HREAL_ADD_RDISTRIB = prove
1344 (`!m n p. (m + n) * p = m * p + n * p`,
1345 ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN MATCH_ACCEPT_TAC HREAL_ADD_LDISTRIB);;
1347 let HREAL_MUL_LZERO = prove
1349 GEN_TAC THEN MP_TAC(SPECL [`&0`; `&1`; `m:hreal`] HREAL_ADD_RDISTRIB) THEN
1350 REWRITE_TAC[HREAL_ADD_LID] THEN
1351 GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM HREAL_ADD_LID] THEN
1352 REWRITE_TAC[HREAL_EQ_ADD_RCANCEL] THEN
1353 DISCH_THEN(ACCEPT_TAC o SYM));;
1355 let HREAL_MUL_RZERO = prove
1357 ONCE_REWRITE_TAC[HREAL_MUL_SYM] THEN MATCH_ACCEPT_TAC HREAL_MUL_LZERO);;
1359 let HREAL_ADD_AC = prove
1360 (`(m + n = n + m) /\
1361 ((m + n) + p = m + (n + p)) /\
1362 (m + (n + p) = n + (m + p))`,
1363 REWRITE_TAC[HREAL_ADD_ASSOC; EQT_INTRO(SPEC_ALL HREAL_ADD_SYM)] THEN
1364 AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC HREAL_ADD_SYM);;
1366 let HREAL_LE_ADD2 = prove
1367 (`!a b c d. a <= b /\ c <= d ==> a + c <= b + d`,
1368 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS_DEF] THEN
1369 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `d1:hreal`)
1370 (X_CHOOSE_TAC `d2:hreal`)) THEN
1371 EXISTS_TAC `d1 + d2` THEN ASM_REWRITE_TAC[HREAL_ADD_AC]);;
1373 let HREAL_LE_MUL_RCANCEL_IMP = prove
1374 (`!a b c. a <= b ==> a * c <= b * c`,
1375 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_LE_EXISTS_DEF] THEN
1376 DISCH_THEN(X_CHOOSE_THEN `d:hreal` SUBST1_TAC) THEN
1377 EXISTS_TAC `d * c` THEN REWRITE_TAC[HREAL_ADD_RDISTRIB]);;
1379 (* ------------------------------------------------------------------------- *)
1380 (* Define operations on representatives of signed reals. *)
1381 (* ------------------------------------------------------------------------- *)
1383 let treal_of_num = new_definition
1384 `treal_of_num n = (&n, &0)`;;
1386 let treal_neg = new_definition
1387 `treal_neg ((x:hreal),(y:hreal)) = (y,x)`;;
1389 let treal_add = new_definition
1390 `(x1,y1) treal_add (x2,y2) = (x1 + x2, y1 + y2)`;;
1392 let treal_mul = new_definition
1393 `(x1,y1) treal_mul (x2,y2) = ((x1 * x2) + (y1 * y2),(x1 * y2) + (y1 * x2))`;;
1395 let treal_le = new_definition
1396 `(x1,y1) treal_le (x2,y2) <=> x1 + y2 <= x2 + y1`;;
1398 let treal_inv = new_definition
1399 `treal_inv(x,y) = if x = y then (&0, &0)
1400 else if y <= x then (inv(@d. x = y + d), &0)
1401 else (&0, inv(@d. y = x + d))`;;
1403 (* ------------------------------------------------------------------------- *)
1404 (* Define the equivalence relation and prove it *is* one. *)
1405 (* ------------------------------------------------------------------------- *)
1407 let treal_eq = new_definition
1408 `(x1,y1) treal_eq (x2,y2) <=> (x1 + y2 = x2 + y1)`;;
1410 let TREAL_EQ_REFL = prove
1411 (`!x. x treal_eq x`,
1412 REWRITE_TAC[FORALL_PAIR_THM; treal_eq]);;
1414 let TREAL_EQ_SYM = prove
1415 (`!x y. x treal_eq y <=> y treal_eq x`,
1416 REWRITE_TAC[FORALL_PAIR_THM; treal_eq; EQ_SYM_EQ]);;
1418 let TREAL_EQ_TRANS = prove
1419 (`!x y z. x treal_eq y /\ y treal_eq z ==> x treal_eq z`,
1420 REWRITE_TAC[FORALL_PAIR_THM; treal_eq] THEN REPEAT GEN_TAC THEN
1421 DISCH_THEN(MP_TAC o MK_COMB o (AP_TERM `(+)` F_F I) o CONJ_PAIR) THEN
1422 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [HREAL_ADD_SYM] THEN
1423 REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_EQ_ADD_LCANCEL] THEN
1424 REWRITE_TAC[HREAL_ADD_ASSOC; HREAL_EQ_ADD_RCANCEL] THEN
1425 DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[HREAL_ADD_SYM]));;
1427 (* ------------------------------------------------------------------------- *)
1428 (* Useful to avoid unnecessary use of the equivalence relation. *)
1429 (* ------------------------------------------------------------------------- *)
1431 let TREAL_EQ_AP = prove
1432 (`!x y. (x = y) ==> x treal_eq y`,
1433 SIMP_TAC[TREAL_EQ_REFL]);;
1435 (* ------------------------------------------------------------------------- *)
1436 (* Commutativity properties for injector. *)
1437 (* ------------------------------------------------------------------------- *)
1439 let TREAL_OF_NUM_EQ = prove
1440 (`!m n. (treal_of_num m treal_eq treal_of_num n) <=> (m = n)`,
1441 REWRITE_TAC[treal_of_num; treal_eq; HREAL_OF_NUM_EQ; HREAL_ADD_RID]);;
1443 let TREAL_OF_NUM_LE = prove
1444 (`!m n. (treal_of_num m treal_le treal_of_num n) <=> m <= n`,
1445 REWRITE_TAC[treal_of_num; treal_le; HREAL_OF_NUM_LE; HREAL_ADD_RID]);;
1447 let TREAL_OF_NUM_ADD = prove
1448 (`!m n. (treal_of_num m treal_add treal_of_num n) treal_eq
1449 (treal_of_num(m + n))`,
1450 REWRITE_TAC[treal_of_num; treal_eq; treal_add;
1451 HREAL_OF_NUM_ADD; HREAL_ADD_RID; ADD_CLAUSES]);;
1453 let TREAL_OF_NUM_MUL = prove
1454 (`!m n. (treal_of_num m treal_mul treal_of_num n) treal_eq
1455 (treal_of_num(m * n))`,
1456 REWRITE_TAC[treal_of_num; treal_eq; treal_mul;
1457 HREAL_OF_NUM_MUL; HREAL_MUL_RZERO; HREAL_MUL_LZERO; HREAL_ADD_RID;
1458 HREAL_ADD_LID; HREAL_ADD_RID; MULT_CLAUSES]);;
1460 (* ------------------------------------------------------------------------- *)
1461 (* Strong forms of equality are useful to simplify welldefinedness proofs. *)
1462 (* ------------------------------------------------------------------------- *)
1464 let TREAL_ADD_SYM_EQ = prove
1465 (`!x y. x treal_add y = y treal_add x`,
1466 REWRITE_TAC[FORALL_PAIR_THM; treal_add; PAIR_EQ; HREAL_ADD_SYM]);;
1468 let TREAL_MUL_SYM_EQ = prove
1469 (`!x y. x treal_mul y = y treal_mul x`,
1470 REWRITE_TAC[FORALL_PAIR_THM; treal_mul; HREAL_MUL_SYM; HREAL_ADD_SYM]);;
1472 (* ------------------------------------------------------------------------- *)
1473 (* Prove the properties of operations on representatives. *)
1474 (* ------------------------------------------------------------------------- *)
1476 let TREAL_ADD_SYM = prove
1477 (`!x y. (x treal_add y) treal_eq (y treal_add x)`,
1478 REPEAT GEN_TAC THEN MATCH_MP_TAC TREAL_EQ_AP THEN
1479 MATCH_ACCEPT_TAC TREAL_ADD_SYM_EQ);;
1481 let TREAL_ADD_ASSOC = prove
1482 (`!x y z. (x treal_add (y treal_add z)) treal_eq
1483 ((x treal_add y) treal_add z)`,
1484 SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_add; HREAL_ADD_ASSOC]);;
1486 let TREAL_ADD_LID = prove
1487 (`!x. ((treal_of_num 0) treal_add x) treal_eq x`,
1488 REWRITE_TAC[FORALL_PAIR_THM; treal_of_num; treal_add; treal_eq;
1491 let TREAL_ADD_LINV = prove
1492 (`!x. ((treal_neg x) treal_add x) treal_eq (treal_of_num 0)`,
1493 REWRITE_TAC[FORALL_PAIR_THM; treal_neg; treal_add; treal_eq; treal_of_num;
1494 HREAL_ADD_LID; HREAL_ADD_RID; HREAL_ADD_SYM]);;
1496 let TREAL_MUL_SYM = prove
1497 (`!x y. (x treal_mul y) treal_eq (y treal_mul x)`,
1498 SIMP_TAC[TREAL_EQ_AP; TREAL_MUL_SYM_EQ]);;
1500 let TREAL_MUL_ASSOC = prove
1501 (`!x y z. (x treal_mul (y treal_mul z)) treal_eq
1502 ((x treal_mul y) treal_mul z)`,
1503 SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_mul; HREAL_ADD_LDISTRIB;
1504 HREAL_ADD_RDISTRIB; GSYM HREAL_MUL_ASSOC; HREAL_ADD_AC]);;
1506 let TREAL_MUL_LID = prove
1507 (`!x. ((treal_of_num 1) treal_mul x) treal_eq x`,
1508 SIMP_TAC[FORALL_PAIR_THM; treal_of_num; treal_mul; treal_eq] THEN
1509 REWRITE_TAC[HREAL_MUL_LZERO; HREAL_MUL_LID; HREAL_ADD_LID; HREAL_ADD_RID]);;
1511 let TREAL_ADD_LDISTRIB = prove
1512 (`!x y z. (x treal_mul (y treal_add z)) treal_eq
1513 ((x treal_mul y) treal_add (x treal_mul z))`,
1514 SIMP_TAC[FORALL_PAIR_THM; TREAL_EQ_AP; treal_mul; treal_add;
1515 HREAL_ADD_LDISTRIB; PAIR_EQ; HREAL_ADD_AC]);;
1517 let TREAL_LE_REFL = prove
1518 (`!x. x treal_le x`,
1519 REWRITE_TAC[FORALL_PAIR_THM; treal_le; HREAL_LE_REFL]);;
1521 let TREAL_LE_ANTISYM = prove
1522 (`!x y. x treal_le y /\ y treal_le x <=> (x treal_eq y)`,
1523 REWRITE_TAC[FORALL_PAIR_THM; treal_le; treal_eq; HREAL_LE_ANTISYM]);;
1525 let TREAL_LE_TRANS = prove
1526 (`!x y z. x treal_le y /\ y treal_le z ==> x treal_le z`,
1527 REWRITE_TAC[FORALL_PAIR_THM; treal_le] THEN REPEAT GEN_TAC THEN
1528 DISCH_THEN(MP_TAC o MATCH_MP HREAL_LE_ADD2) THEN
1529 GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [HREAL_ADD_SYM] THEN
1530 REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL] THEN
1531 REWRITE_TAC[HREAL_ADD_ASSOC; HREAL_LE_ADD_RCANCEL] THEN
1532 DISCH_THEN(MATCH_ACCEPT_TAC o ONCE_REWRITE_RULE[HREAL_ADD_SYM]));;
1534 let TREAL_LE_TOTAL = prove
1535 (`!x y. x treal_le y \/ y treal_le x`,
1536 REWRITE_TAC[FORALL_PAIR_THM; treal_le; HREAL_LE_TOTAL]);;
1538 let TREAL_LE_LADD_IMP = prove
1539 (`!x y z. (y treal_le z) ==> (x treal_add y) treal_le (x treal_add z)`,
1540 REWRITE_TAC[FORALL_PAIR_THM; treal_le; treal_add] THEN
1541 REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL] THEN
1542 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
1543 REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_LE_ADD_LCANCEL]);;
1545 let TREAL_LE_MUL = prove
1546 (`!x y. (treal_of_num 0) treal_le x /\ (treal_of_num 0) treal_le y
1547 ==> (treal_of_num 0) treal_le (x treal_mul y)`,
1548 REWRITE_TAC[FORALL_PAIR_THM; treal_of_num; treal_le; treal_mul] THEN
1549 REPEAT GEN_TAC THEN REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
1550 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
1551 DISCH_THEN(CHOOSE_THEN SUBST1_TAC o MATCH_MP HREAL_LE_EXISTS) THEN
1552 REWRITE_TAC[HREAL_ADD_LDISTRIB; HREAL_LE_ADD_LCANCEL;
1553 GSYM HREAL_ADD_ASSOC] THEN
1554 GEN_REWRITE_TAC RAND_CONV [HREAL_ADD_SYM] THEN
1555 ASM_REWRITE_TAC[HREAL_LE_ADD_LCANCEL] THEN
1556 MATCH_MP_TAC HREAL_LE_MUL_RCANCEL_IMP THEN ASM_REWRITE_TAC[]);;
1558 let TREAL_INV_0 = prove
1559 (`treal_inv (treal_of_num 0) treal_eq (treal_of_num 0)`,
1560 REWRITE_TAC[treal_inv; treal_eq; treal_of_num]);;
1562 let TREAL_MUL_LINV = prove
1563 (`!x. ~(x treal_eq treal_of_num 0) ==>
1564 (treal_inv(x) treal_mul x) treal_eq (treal_of_num 1)`,
1565 REWRITE_TAC[FORALL_PAIR_THM] THEN
1566 MAP_EVERY X_GEN_TAC [`x:hreal`; `y:hreal`] THEN
1567 PURE_REWRITE_TAC[treal_eq; treal_of_num; treal_mul; treal_inv] THEN
1568 PURE_REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN DISCH_TAC THEN
1569 PURE_ASM_REWRITE_TAC[COND_CLAUSES] THEN COND_CASES_TAC THEN
1570 PURE_REWRITE_TAC[treal_mul; treal_eq] THEN
1571 REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID;
1572 HREAL_MUL_LZERO; HREAL_MUL_RZERO] THENL
1574 DISJ_CASES_THEN MP_TAC(SPECL [`x:hreal`; `y:hreal`] HREAL_LE_TOTAL) THEN
1575 ASM_REWRITE_TAC[] THEN DISCH_TAC] THEN
1576 FIRST_ASSUM(MP_TAC o MATCH_MP HREAL_LE_EXISTS) THEN
1577 DISCH_THEN(MP_TAC o SELECT_RULE) THEN
1578 DISCH_THEN(fun th -> ASSUME_TAC (SYM th) THEN
1579 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [th]) THEN
1580 REWRITE_TAC[HREAL_ADD_LDISTRIB] THEN
1581 GEN_REWRITE_TAC RAND_CONV [HREAL_ADD_SYM] THEN
1582 AP_TERM_TAC THEN MATCH_MP_TAC HREAL_MUL_LINV THEN
1583 DISCH_THEN SUBST_ALL_TAC THEN
1584 FIRST_ASSUM(UNDISCH_TAC o check is_eq o concl) THEN
1585 ASM_REWRITE_TAC[HREAL_ADD_RID] THEN
1586 PURE_ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN ASM_REWRITE_TAC[]);;
1588 (* ------------------------------------------------------------------------- *)
1589 (* Show that the operations respect the equivalence relation. *)
1590 (* ------------------------------------------------------------------------- *)
1592 let TREAL_OF_NUM_WELLDEF = prove
1593 (`!m n. (m = n) ==> (treal_of_num m) treal_eq (treal_of_num n)`,
1594 REPEAT GEN_TAC THEN DISCH_THEN SUBST1_TAC THEN
1595 MATCH_ACCEPT_TAC TREAL_EQ_REFL);;
1597 let TREAL_NEG_WELLDEF = prove
1598 (`!x1 x2. x1 treal_eq x2 ==> (treal_neg x1) treal_eq (treal_neg x2)`,
1599 REWRITE_TAC[FORALL_PAIR_THM; treal_neg; treal_eq] THEN REPEAT STRIP_TAC THEN
1600 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN ASM_REWRITE_TAC[]);;
1602 let TREAL_ADD_WELLDEFR = prove
1603 (`!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_add y) treal_eq (x2 treal_add y)`,
1604 REWRITE_TAC[FORALL_PAIR_THM; treal_add; treal_eq] THEN
1605 REWRITE_TAC[HREAL_EQ_ADD_RCANCEL; HREAL_ADD_ASSOC] THEN
1606 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN
1607 REWRITE_TAC[HREAL_EQ_ADD_RCANCEL; HREAL_ADD_ASSOC]);;
1609 let TREAL_ADD_WELLDEF = prove
1610 (`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1611 (x1 treal_add y1) treal_eq (x2 treal_add y2)`,
1612 REPEAT GEN_TAC THEN DISCH_TAC THEN
1613 MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC `x1 treal_add y2` THEN
1614 CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_ADD_SYM_EQ]; ALL_TAC] THEN
1615 MATCH_MP_TAC TREAL_ADD_WELLDEFR THEN ASM_REWRITE_TAC[]);;
1617 let TREAL_MUL_WELLDEFR = prove
1618 (`!x1 x2 y. x1 treal_eq x2 ==> (x1 treal_mul y) treal_eq (x2 treal_mul y)`,
1619 REWRITE_TAC[FORALL_PAIR_THM; treal_mul; treal_eq] THEN REPEAT GEN_TAC THEN
1620 ONCE_REWRITE_TAC[AC HREAL_ADD_AC
1621 `(a + b) + (c + d) = (a + d) + (b + c)`] THEN
1622 REWRITE_TAC[GSYM HREAL_ADD_RDISTRIB] THEN DISCH_TAC THEN
1623 ASM_REWRITE_TAC[] THEN AP_TERM_TAC THEN
1624 ONCE_REWRITE_TAC[HREAL_ADD_SYM] THEN POP_ASSUM SUBST1_TAC THEN REFL_TAC);;
1626 let TREAL_MUL_WELLDEF = prove
1627 (`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1628 (x1 treal_mul y1) treal_eq (x2 treal_mul y2)`,
1629 REPEAT GEN_TAC THEN DISCH_TAC THEN
1630 MATCH_MP_TAC TREAL_EQ_TRANS THEN EXISTS_TAC `x1 treal_mul y2` THEN
1631 CONJ_TAC THENL [ONCE_REWRITE_TAC[TREAL_MUL_SYM_EQ]; ALL_TAC] THEN
1632 MATCH_MP_TAC TREAL_MUL_WELLDEFR THEN ASM_REWRITE_TAC[]);;
1634 let TREAL_EQ_IMP_LE = prove
1635 (`!x y. x treal_eq y ==> x treal_le y`,
1636 SIMP_TAC[FORALL_PAIR_THM; treal_eq; treal_le; HREAL_LE_REFL]);;
1638 let TREAL_LE_WELLDEF = prove
1639 (`!x1 x2 y1 y2. x1 treal_eq x2 /\ y1 treal_eq y2 ==>
1640 (x1 treal_le y1 <=> x2 treal_le y2)`,
1641 REPEAT (STRIP_TAC ORELSE EQ_TAC) THENL
1642 [MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `y1:hreal#hreal` THEN
1644 [MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `x1:hreal#hreal` THEN
1645 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TREAL_EQ_IMP_LE THEN
1646 ONCE_REWRITE_TAC[TREAL_EQ_SYM];
1647 MATCH_MP_TAC TREAL_EQ_IMP_LE];
1648 MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `y2:hreal#hreal` THEN
1650 [MATCH_MP_TAC TREAL_LE_TRANS THEN EXISTS_TAC `x2:hreal#hreal` THEN
1651 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC TREAL_EQ_IMP_LE;
1652 MATCH_MP_TAC TREAL_EQ_IMP_LE THEN ONCE_REWRITE_TAC[TREAL_EQ_SYM]]] THEN
1653 ASM_REWRITE_TAC[]);;
1655 let TREAL_INV_WELLDEF = prove
1656 (`!x y. x treal_eq y ==> (treal_inv x) treal_eq (treal_inv y)`,
1658 (`(@d. x = x + d) = &0`,
1659 MATCH_MP_TAC SELECT_UNIQUE THEN BETA_TAC THEN
1660 GEN_TAC THEN GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM HREAL_ADD_RID] THEN
1661 REWRITE_TAC[HREAL_EQ_ADD_LCANCEL] THEN
1662 MATCH_ACCEPT_TAC EQ_SYM_EQ) in
1663 REWRITE_TAC[FORALL_PAIR_THM] THEN
1664 MAP_EVERY X_GEN_TAC [`x1:hreal`; `x2:hreal`; `y1:hreal`; `y2:hreal`] THEN
1665 PURE_REWRITE_TAC[treal_eq; treal_inv] THEN
1666 ASM_CASES_TAC `x1 :hreal = x2` THEN
1667 ASM_CASES_TAC `y1 :hreal = y2` THEN ASM_REWRITE_TAC[] THEN
1668 REWRITE_TAC[TREAL_EQ_REFL] THEN
1669 DISCH_THEN(MP_TAC o GEN_REWRITE_RULE RAND_CONV [HREAL_ADD_SYM]) THEN
1670 REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; HREAL_EQ_ADD_RCANCEL] THEN DISCH_TAC THEN
1671 ASM_REWRITE_TAC[HREAL_LE_REFL; lemma; HREAL_INV_0;TREAL_EQ_REFL] THEN
1672 ASM_CASES_TAC `x2 <= x1` THEN ASM_REWRITE_TAC[] THENL
1673 [FIRST_ASSUM(ASSUME_TAC o SYM o SELECT_RULE o MATCH_MP HREAL_LE_EXISTS) THEN
1674 UNDISCH_TAC `x1 + y2 = x2 + y1` THEN
1675 FIRST_ASSUM(SUBST1_TAC o SYM) THEN
1676 REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; GSYM HREAL_ADD_ASSOC] THEN
1677 DISCH_THEN(SUBST1_TAC o SYM) THEN
1678 REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD] THEN
1679 GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o RAND_CONV o BINDER_CONV o
1680 LAND_CONV) [HREAL_ADD_SYM] THEN
1681 REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; TREAL_EQ_REFL];
1682 DISJ_CASES_THEN MP_TAC
1683 (SPECL [`x1:hreal`; `x2:hreal`] HREAL_LE_TOTAL) THEN
1684 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1685 FIRST_ASSUM(ASSUME_TAC o SYM o SELECT_RULE o MATCH_MP HREAL_LE_EXISTS) THEN
1686 UNDISCH_TAC `x1 + y2 = x2 + y1` THEN
1687 FIRST_ASSUM(SUBST1_TAC o SYM) THEN
1688 REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; GSYM HREAL_ADD_ASSOC] THEN
1689 DISCH_THEN SUBST1_TAC THEN
1690 REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD] THEN
1691 COND_CASES_TAC THENL
1692 [UNDISCH_TAC `(@d. x2 = x1 + d) + y1 <= y1:hreal` THEN
1693 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [GSYM HREAL_ADD_LID] THEN
1694 REWRITE_TAC[ONCE_REWRITE_RULE[HREAL_ADD_SYM] HREAL_LE_ADD_LCANCEL] THEN
1695 DISCH_TAC THEN SUBGOAL_THEN `(@d. x2 = x1 + d) = &0` MP_TAC THENL
1696 [ASM_REWRITE_TAC[GSYM HREAL_LE_ANTISYM] THEN
1697 GEN_REWRITE_TAC RAND_CONV [GSYM HREAL_ADD_LID] THEN
1698 REWRITE_TAC[HREAL_LE_ADD];
1699 DISCH_THEN SUBST_ALL_TAC THEN
1700 UNDISCH_TAC `x1 + & 0 = x2` THEN
1701 ASM_REWRITE_TAC[HREAL_ADD_RID]];
1702 GEN_REWRITE_TAC (funpow 3 RAND_CONV o BINDER_CONV o LAND_CONV)
1703 [HREAL_ADD_SYM] THEN
1704 REWRITE_TAC[HREAL_EQ_ADD_LCANCEL; TREAL_EQ_REFL]]]);;
1706 (* ------------------------------------------------------------------------- *)
1707 (* Now define the quotient type -- the reals at last! *)
1708 (* ------------------------------------------------------------------------- *)
1711 define_quotient_type "real" ("mk_real","dest_real") `(treal_eq)`;;
1713 let real_of_num,real_of_num_th =
1714 lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1715 "real_of_num" TREAL_OF_NUM_WELLDEF;;
1717 let real_neg,real_neg_th =
1718 lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1719 "real_neg" TREAL_NEG_WELLDEF;;
1721 let real_add,real_add_th =
1722 lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1723 "real_add" TREAL_ADD_WELLDEF;;
1725 let real_mul,real_mul_th =
1726 lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1727 "real_mul" TREAL_MUL_WELLDEF;;
1729 let real_le,real_le_th =
1730 lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1731 "real_le" TREAL_LE_WELLDEF;;
1733 let real_inv,real_inv_th =
1734 lift_function (snd real_tybij) (TREAL_EQ_REFL,TREAL_EQ_TRANS)
1735 "real_inv" TREAL_INV_WELLDEF;;
1737 let [REAL_ADD_SYM; REAL_ADD_ASSOC; REAL_ADD_LID; REAL_ADD_LINV;
1738 REAL_MUL_SYM; REAL_MUL_ASSOC; REAL_MUL_LID;
1740 REAL_LE_REFL; REAL_LE_ANTISYM; REAL_LE_TRANS; REAL_LE_TOTAL;
1741 REAL_LE_LADD_IMP; REAL_LE_MUL;
1742 REAL_INV_0; REAL_MUL_LINV;
1743 REAL_OF_NUM_EQ; REAL_OF_NUM_LE; REAL_OF_NUM_ADD; REAL_OF_NUM_MUL] =
1745 (lift_theorem real_tybij (TREAL_EQ_REFL,TREAL_EQ_SYM,TREAL_EQ_TRANS)
1746 [real_of_num_th; real_neg_th; real_add_th;
1747 real_mul_th; real_le_th; real_inv_th])
1748 [TREAL_ADD_SYM; TREAL_ADD_ASSOC; TREAL_ADD_LID; TREAL_ADD_LINV;
1749 TREAL_MUL_SYM; TREAL_MUL_ASSOC; TREAL_MUL_LID;
1751 TREAL_LE_REFL; TREAL_LE_ANTISYM; TREAL_LE_TRANS; TREAL_LE_TOTAL;
1752 TREAL_LE_LADD_IMP; TREAL_LE_MUL;
1753 TREAL_INV_0; TREAL_MUL_LINV;
1754 TREAL_OF_NUM_EQ; TREAL_OF_NUM_LE; TREAL_OF_NUM_ADD; TREAL_OF_NUM_MUL];;
1756 (* ------------------------------------------------------------------------- *)
1757 (* Set up a friendly interface. *)
1758 (* ------------------------------------------------------------------------- *)
1760 parse_as_prefix "--";;
1761 parse_as_infix ("/",(22,"left"));;
1762 parse_as_infix ("pow",(24,"left"));;
1764 do_list overload_interface
1765 ["+",`real_add:real->real->real`; "-",`real_sub:real->real->real`;
1766 "*",`real_mul:real->real->real`; "/",`real_div:real->real->real`;
1767 "<",`real_lt:real->real->bool`; "<=",`real_le:real->real->bool`;
1768 ">",`real_gt:real->real->bool`; ">=",`real_ge:real->real->bool`;
1769 "--",`real_neg:real->real`; "pow",`real_pow:real->num->real`;
1770 "inv",`real_inv:real->real`; "abs",`real_abs:real->real`;
1771 "max",`real_max:real->real->real`; "min",`real_min:real->real->real`;
1772 "&",`real_of_num:num->real`];;
1774 let prioritize_real() = prioritize_overload(mk_type("real",[]));;
1776 (* ------------------------------------------------------------------------- *)
1777 (* Additional definitions. *)
1778 (* ------------------------------------------------------------------------- *)
1780 let real_sub = new_definition
1783 let real_lt = new_definition
1784 `x < y <=> ~(y <= x)`;;
1786 let real_ge = new_definition
1787 `x >= y <=> y <= x`;;
1789 let real_gt = new_definition
1792 let real_abs = new_definition
1793 `abs(x) = if &0 <= x then x else --x`;;
1795 let real_pow = new_recursive_definition num_RECURSION
1797 (!n. x pow (SUC n) = x * (x pow n))`;;
1799 let real_div = new_definition
1800 `x / y = x * inv(y)`;;
1802 let real_max = new_definition
1803 `real_max m n = if m <= n then n else m`;;
1805 let real_min = new_definition
1806 `real_min m n = if m <= n then m else n`;;
1808 (*----------------------------------------------------------------------------*)
1809 (* Derive the supremum property for an arbitrary bounded nonempty set *)
1810 (*----------------------------------------------------------------------------*)
1812 let REAL_HREAL_LEMMA1 = prove
1814 (!x. &0 <= x <=> ?y. x = r y) /\
1815 (!y z. y <= z <=> r y <= r z)`,
1816 EXISTS_TAC `\y. mk_real((treal_eq)(y,hreal_of_num 0))` THEN
1817 REWRITE_TAC[GSYM real_le_th] THEN
1818 REWRITE_TAC[treal_le; HREAL_ADD_LID; HREAL_ADD_RID] THEN
1819 GEN_TAC THEN EQ_TAC THENL
1820 [MP_TAC(INST [`dest_real x`,`r:hreal#hreal->bool`] (snd real_tybij)) THEN
1821 REWRITE_TAC[fst real_tybij] THEN
1822 DISCH_THEN(X_CHOOSE_THEN `p:hreal#hreal` MP_TAC) THEN
1823 DISCH_THEN(MP_TAC o AP_TERM `mk_real`) THEN
1824 REWRITE_TAC[fst real_tybij] THEN DISCH_THEN SUBST1_TAC THEN
1825 REWRITE_TAC[GSYM real_of_num_th; GSYM real_le_th] THEN
1826 SUBST1_TAC(GSYM(ISPEC `p:hreal#hreal` PAIR)) THEN
1827 PURE_REWRITE_TAC[treal_of_num; treal_le] THEN
1828 PURE_REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
1829 DISCH_THEN(X_CHOOSE_THEN `d:hreal` SUBST1_TAC o
1830 MATCH_MP HREAL_LE_EXISTS) THEN
1831 EXISTS_TAC `d:hreal` THEN AP_TERM_TAC THEN
1832 ONCE_REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `q:hreal#hreal` THEN
1833 SUBST1_TAC(GSYM(ISPEC `q:hreal#hreal` PAIR)) THEN
1834 PURE_REWRITE_TAC[treal_eq] THEN
1835 GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [HREAL_ADD_SYM] THEN
1836 REWRITE_TAC[GSYM HREAL_ADD_ASSOC; HREAL_EQ_ADD_LCANCEL] THEN
1837 REWRITE_TAC[HREAL_ADD_RID];
1838 DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN
1839 REWRITE_TAC[GSYM real_of_num_th; GSYM real_le_th] THEN
1840 REWRITE_TAC[treal_of_num; treal_le] THEN
1841 REWRITE_TAC[HREAL_ADD_LID; HREAL_ADD_RID] THEN
1842 GEN_REWRITE_TAC RAND_CONV [GSYM HREAL_ADD_LID] THEN
1843 REWRITE_TAC[HREAL_LE_ADD]]);;
1845 let REAL_HREAL_LEMMA2 = prove
1846 (`?h r. (!x:hreal. h(r x) = x) /\
1847 (!x. &0 <= x ==> (r(h x) = x)) /\
1848 (!x:hreal. &0 <= r x) /\
1849 (!x y. x <= y <=> r x <= r y)`,
1850 STRIP_ASSUME_TAC REAL_HREAL_LEMMA1 THEN
1851 EXISTS_TAC `\x:real. @y:hreal. x = r y` THEN
1852 EXISTS_TAC `r:hreal->real` THEN
1853 ASM_REWRITE_TAC[BETA_THM] THEN
1854 SUBGOAL_THEN `!y z. ((r:hreal->real) y = r z) <=> (y = z)` ASSUME_TAC THENL
1855 [ASM_REWRITE_TAC[GSYM REAL_LE_ANTISYM; GSYM HREAL_LE_ANTISYM]; ALL_TAC] THEN
1856 ASM_REWRITE_TAC[GEN_REWRITE_RULE (LAND_CONV o BINDER_CONV) [EQ_SYM_EQ]
1857 (SPEC_ALL SELECT_REFL); GSYM EXISTS_REFL] THEN
1858 GEN_TAC THEN DISCH_THEN(ACCEPT_TAC o SYM o SELECT_RULE));;
1860 let REAL_COMPLETE_SOMEPOS = prove
1861 (`!P. (?x. P x /\ &0 <= x) /\
1862 (?M. !x. P x ==> x <= M)
1863 ==> ?M. (!x. P x ==> x <= M) /\
1864 !M'. (!x. P x ==> x <= M') ==> M <= M'`,
1865 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC REAL_HREAL_LEMMA2 THEN
1866 MP_TAC(SPEC `\y:hreal. (P:real->bool)(r y)` HREAL_COMPLETE) THEN
1868 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
1870 [EXISTS_TAC `(h:real->hreal) x` THEN
1871 UNDISCH_TAC `(P:real->bool) x` THEN
1872 MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
1873 AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1874 EXISTS_TAC `(h:real->hreal) M` THEN
1875 X_GEN_TAC `y:hreal` THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1876 ASM_REWRITE_TAC[] THEN
1877 MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
1878 AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1879 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
1880 ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1882 MATCH_MP_TAC(TAUT `(b ==> c) ==> a ==> (a ==> b) ==> c`) THEN
1883 DISCH_THEN(X_CHOOSE_THEN `B:hreal` STRIP_ASSUME_TAC)] THEN
1884 EXISTS_TAC `(r:hreal->real) B` THEN CONJ_TAC THENL
1885 [X_GEN_TAC `z:real` THEN DISCH_TAC THEN
1886 DISJ_CASES_TAC(SPECL [`&0`; `z:real`] REAL_LE_TOTAL) THENL
1887 [ANTE_RES_THEN(SUBST1_TAC o SYM) (ASSUME `&0 <= z`) THEN
1888 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC I [GSYM th]) THEN
1889 FIRST_ASSUM MATCH_MP_TAC THEN
1890 UNDISCH_TAC `(P:real->bool) z` THEN
1891 MATCH_MP_TAC(TAUT `(b <=> a) ==> a ==> b`) THEN
1892 AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
1894 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&0` THEN
1896 X_GEN_TAC `C:real` THEN DISCH_TAC THEN
1897 SUBGOAL_THEN `B:hreal <= (h(C:real))` MP_TAC THENL
1898 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN
1899 SUBGOAL_THEN `(r:hreal->real)(h C) = C` (fun th -> ASM_REWRITE_TAC[th]);
1900 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC EQ_IMP THEN AP_TERM_TAC] THEN
1901 FIRST_ASSUM MATCH_MP_TAC THEN
1902 MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `x:real` THEN
1903 ASM_REWRITE_TAC[] THEN FIRST_ASSUM MATCH_MP_TAC THEN
1904 ASM_REWRITE_TAC[]]);;
1906 let REAL_COMPLETE = prove
1908 (?M. !x. P x ==> x <= M)
1909 ==> ?M. (!x. P x ==> x <= M) /\
1910 !M'. (!x. P x ==> x <= M') ==> M <= M'`,
1913 REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
1914 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_ADD_LID]) in
1915 REPEAT STRIP_TAC THEN
1916 DISJ_CASES_TAC (SPECL [`&0`; `x:real`] REAL_LE_TOTAL) THENL
1917 [MATCH_MP_TAC REAL_COMPLETE_SOMEPOS THEN CONJ_TAC THENL
1918 [EXISTS_TAC `x:real`; EXISTS_TAC `M:real`] THEN
1920 FIRST_ASSUM(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THEN
1921 DISCH_THEN(MP_TAC o SPEC `--x`) THEN
1922 REWRITE_TAC[REAL_ADD_LINV] THEN
1923 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[REAL_ADD_LID] THEN
1925 MP_TAC(SPEC `\y. P(y + x) :bool` REAL_COMPLETE_SOMEPOS) THEN
1927 W(C SUBGOAL_THEN MP_TAC o funpow 2 (fst o dest_imp) o snd) THENL
1929 [EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[REAL_LE_REFL; REAL_ADD_LID];
1930 EXISTS_TAC `M + --x` THEN GEN_TAC THEN
1931 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
1932 DISCH_THEN(MP_TAC o SPEC `--x` o MATCH_MP REAL_LE_LADD_IMP) THEN
1933 DISCH_THEN(MP_TAC o ONCE_REWRITE_RULE[REAL_ADD_SYM]) THEN
1934 REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1935 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV] THEN
1936 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]];
1937 MATCH_MP_TAC(TAUT `(b ==> c) ==> a ==> (a ==> b) ==> c`) THEN
1938 DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC)] THEN
1939 EXISTS_TAC `B + x` THEN CONJ_TAC THENL
1940 [GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [lemma] THEN
1941 DISCH_THEN(ANTE_RES_THEN
1942 (MP_TAC o SPEC `x:real` o MATCH_MP REAL_LE_LADD_IMP)) THEN
1943 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1944 REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
1945 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID] THEN
1946 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1948 REPEAT STRIP_TAC THEN SUBGOAL_THEN `B <= M' - x` MP_TAC THENL
1949 [FIRST_ASSUM MATCH_MP_TAC THEN X_GEN_TAC `z:real` THEN DISCH_TAC THEN
1950 SUBGOAL_THEN `z + x <= M'` MP_TAC THENL
1951 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
1952 DISCH_THEN(MP_TAC o SPEC `--x` o MATCH_MP REAL_LE_LADD_IMP) THEN
1953 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN
1954 REWRITE_TAC[real_sub] THEN MATCH_MP_TAC EQ_IMP THEN AP_THM_TAC THEN
1955 AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC] THEN
1956 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LINV] THEN
1957 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]];
1958 DISCH_THEN(MP_TAC o SPEC `x:real` o MATCH_MP REAL_LE_LADD_IMP) THEN
1959 MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THENL
1960 [MATCH_ACCEPT_TAC REAL_ADD_SYM;
1961 ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[real_sub] THEN
1962 REWRITE_TAC[GSYM REAL_ADD_ASSOC; REAL_ADD_LINV] THEN
1963 REWRITE_TAC[ONCE_REWRITE_RULE[REAL_ADD_SYM] REAL_ADD_LID]]]]]);;
1965 do_list reduce_interface
1966 ["+",`hreal_add:hreal->hreal->hreal`;
1967 "*",`hreal_mul:hreal->hreal->hreal`;
1968 "<=",`hreal_le:hreal->hreal->bool`;
1969 "inv",`hreal_inv:hreal->hreal`];;
1971 do_list remove_interface ["**"; "++"; "<<="; "==="; "fn"; "afn"];;