real_of_ratScript.sml
1(*---------------------------------------------------------------------------*)
2(* real_of_ratTheory, mapping between rationals and a subset of reals *)
3(*---------------------------------------------------------------------------*)
4Theory real_of_rat
5Ancestors
6 realax rat integer real intreal pred_set gcd
7Libs
8 hurdUtils
9
10
11val _ = augment_srw_ss [intSimps.INT_ARITH_ss]
12
13Theorem NUM_OPP_SIGNS_COMPARE:
14 !i1 i2. i1 <= 0 /\ 0 <= i2 ==>
15 (Num i1 < Num i2 <=> 0 < i1 + i2) /\
16 (Num i2 < Num i1 <=> i1 + i2 < 0) /\
17 (Num i1 = Num i2 <=> i1 + i2 = 0)
18Proof
19 rw[]
20 >> ‘i1 = - ABS i1’ by (Cases_on ‘i1=0’ >- simp[] >- metis_tac[INT_ABS,INT_LE_LT,INT_NEGNEG])
21 >> ‘i2 = ABS i2’ by simp[INT_ABS,INT_NOT_LT]
22 >> metis_tac[int_arithTheory.lt_move_all_left,int_arithTheory.lt_move_all_right,INT_ADD_COMM,INT_LT,Num_EQ_ABS,INT_NEGNEG,INT_ADD_LINV,INT_LNEG_UNIQ,INT_RNEG_UNIQ,INT_INJ]
23QED
24
25Theorem ABS_SQUARE:
26 !i. ABS i * ABS i = i*i
27Proof
28 Cases_on ‘i’ >> rw[]
29QED
30
31Theorem NUM_NEG:
32 Num (-i) = Num i
33Proof
34 Cases_on ‘i’ >> simp[]
35QED
36
37Theorem NUM_LT_NEG:
38 !i1 i2. i1 <= 0 /\ i2 <= 0 ==> (Num i1 < Num i2 <=> i2 < i1)
39Proof
40 rw[] >> once_rewrite_tac[GSYM NUM_NEG] >> once_rewrite_tac[GSYM INT_LT_NEG] >> simp[NUM_LT,INT_NEG_GE0]
41QED
42
43Definition real_of_rat_def:
44 real_of_rat q = real_of_int (RATN q) / &RATD q
45End
46
47Theorem REAL_OF_RAT_0[simp]:
48 real_of_rat 0 = 0
49Proof
50 simp[real_of_rat_def]
51QED
52
53Theorem REAL_OF_RAT_1[simp]:
54 real_of_rat 1 = 1
55Proof
56 simp[real_of_rat_def]
57QED
58
59Theorem REAL_OF_RAT_OF_INT:
60 real_of_rat (rat_of_int i) = real_of_int i
61Proof
62 simp[real_of_rat_def]
63QED
64
65Theorem RAT_DIV_LEMMA:
66 q1 <> 0:rat /\ q2<>0:rat ==> (p1/q1=p2/q2 <=> p1*q2 = p2*q1)
67Proof
68 rw[] >> simp[RAT_DIV_MULMINV]
69 >> ‘p1 * q2 = p1 * q2 * (rat_minv q1 * q1)’ by simp[RAT_MUL_LINV]
70 >> ‘_ = p1 * rat_minv q1 * (q1 * q2)’ by metis_tac[RAT_MUL_ASSOC,RAT_MUL_COMM]
71 >> ‘p2 * q1 = p2 * q1 * (rat_minv q2 * q2)’ by simp[RAT_MUL_LINV]
72 >> ‘_ = p2 * rat_minv q2 * (q1 * q2)’ by metis_tac[RAT_MUL_ASSOC,RAT_MUL_COMM]
73 >> simp[RAT_EQ_RMUL]
74QED
75
76Theorem REAL_OF_RAT_INJ:
77 real_of_rat r1 = real_of_rat r2 <=> r1 = r2
78Proof
79 simp[EQ_IMP_THM] >> simp[real_of_rat_def]
80 >> simp[RAT_LEMMA5_BETTER] >> once_rewrite_tac[GSYM real_of_int_num] >> once_rewrite_tac[GSYM real_of_int_mul]
81 >> simp[real_of_int_11] >> once_rewrite_tac[GSYM rat_of_int_11] >> once_rewrite_tac[GSYM rat_of_int_MUL]
82 >> simp[rat_of_int_of_num,GSYM RAT_DIV_LEMMA]
83QED
84
85Theorem RATND_ADD:
86 rat_of_int (RATN r1 * &RATD r2 + &RATD r1 * RATN r2) / &(RATD r1 * RATD r2) = r1 + r2
87Proof
88 ‘r1 + r2 = rat_of_int (RATN r1) / &RATD r1 + rat_of_int (RATN r2) / &RATD r2’ by simp[GSYM RATN_RATD_EQ_THM]
89 >> ‘_ = (rat_of_int (RATN r1) * &RATD r2 + rat_of_int (RATN r2) * &RATD r1)/(&RATD r1 * &RATD r2)’ by simp[RAT_DIVDIV_ADD]
90 >> simp[]
91 >> once_rewrite_tac[GSYM rat_of_int_of_num] >> simp[rat_of_int_MUL,rat_of_int_ADD] >> metis_tac[INT_MUL_COMM]
92QED
93
94Theorem RAT_DIV_PROD:
95 b<>0 /\ d<>0 ==> a/b:rat * (c/d) = (a*c)/(b*d)
96Proof
97 simp[RAT_DIV_MULMINV,RAT_MINV_MUL] >> metis_tac[RAT_MUL_ASSOC,RAT_MUL_COMM]
98QED
99
100Theorem RATND_MUL:
101 rat_of_int (RATN r1 * RATN r2) / &(RATD r1 * RATD r2) = r1 * r2
102Proof
103 ‘r1 * r2 = rat_of_int (RATN r1) / &RATD r1 * (rat_of_int (RATN r2) / &RATD r2)’ by simp[GSYM RATN_RATD_EQ_THM]
104 >> ‘_ = rat_of_int (RATN r1 * RATN r2) / &(RATD r1 * RATD r2)’ by simp[RAT_DIV_PROD,rat_of_int_MUL,RAT_MUL_NUM_CALCULATE]
105 >> simp[]
106QED
107
108Theorem REAL_OF_RAT_ADD:
109 real_of_rat r1 + real_of_rat r2 = real_of_rat (r1 + r2)
110Proof
111 simp[real_of_rat_def,RAT_LEMMA5_BETTER,REAL_ADD_RAT] >> once_rewrite_tac[GSYM real_of_int_num]
112 >> once_rewrite_tac[GSYM real_of_int_mul] >> once_rewrite_tac[GSYM real_of_int_add] >> once_rewrite_tac[GSYM real_of_int_mul]
113 >> simp[real_of_int_11]
114 >> once_rewrite_tac[GSYM rat_of_int_11] >> once_rewrite_tac[GSYM rat_of_int_MUL]
115 >> simp[GSYM RAT_DIV_LEMMA]
116 >> ‘r1 + r2 = rat_of_int (RATN r1) / &RATD r1 + rat_of_int (RATN r2) / &RATD r2’ by simp[GSYM RATN_RATD_EQ_THM]
117 >> ‘_ = (rat_of_int (RATN r1) * &RATD r2 + rat_of_int (RATN r2) * &RATD r1)/(&RATD r1 * &RATD r2)’ by simp[RAT_DIVDIV_ADD]
118 >> simp[]
119 >> once_rewrite_tac[GSYM rat_of_int_of_num] >> simp[rat_of_int_MUL,rat_of_int_ADD] >> metis_tac[INT_MUL_COMM]
120QED
121
122val _ = temp_delsimps ["real_of_int_num"]
123
124Theorem REAL_OF_RAT_MUL:
125 real_of_rat r1 * real_of_rat r2 = real_of_rat (r1 * r2)
126Proof
127 simp[real_of_rat_def,REAL_DIV_PROD,RAT_LEMMA5_BETTER,GSYM real_of_int_num]
128 >> once_rewrite_tac[GSYM real_of_int_mul]
129 >> once_rewrite_tac[GSYM real_of_int_mul]
130 >> simp[real_of_int_11] >> once_rewrite_tac[GSYM rat_of_int_11]
131 >> once_rewrite_tac[GSYM rat_of_int_MUL]
132 >> simp[rat_of_int_of_num]
133 >> simp[RAT_EQ_NUM_CALCULATE,GSYM RAT_DIV_LEMMA,RATND_MUL]
134QED
135
136Theorem REAL_OF_RAT_NEG:
137 -real_of_rat r = real_of_rat (-r)
138Proof
139 ‘real_of_rat r + real_of_rat (-r) = 0’ by simp[REAL_OF_RAT_ADD,RAT_ADD_RINV]
140 >> ‘real_of_rat r + -real_of_rat r = 0’ by simp[REAL_ADD_RINV]
141 >> metis_tac[REAL_EQ_LADD]
142QED
143
144Theorem REAL_OF_RAT_SUB:
145 real_of_rat r1 - real_of_rat r2 = real_of_rat (r1 - r2)
146Proof
147 simp[real_sub,RAT_SUB_ADDAINV,REAL_OF_RAT_ADD,REAL_OF_RAT_NEG]
148QED
149
150Theorem REAL_OF_RAT_MINV:
151 r<>0 ==> inv (real_of_rat r) = real_of_rat (rat_minv r)
152Proof
153 rw[] >> ‘real_of_rat r * real_of_rat (rat_minv r) = 1’ by simp[REAL_OF_RAT_MUL,RAT_MUL_RINV]
154 >> ‘real_of_rat r <> 0’ by (once_rewrite_tac[GSYM REAL_OF_RAT_0] >> simp[REAL_OF_RAT_INJ])
155 >> ‘real_of_rat r * inv (real_of_rat r) = 1’ by simp[REAL_MUL_RINV]
156 >> metis_tac[REAL_EQ_MUL_LCANCEL]
157QED
158
159Theorem REAL_OF_RAT_DIV:
160 r2<>0 ==> real_of_rat r1 / real_of_rat r2 = real_of_rat (r1/r2)
161Proof
162 rw[real_div,RAT_DIV_MULMINV,REAL_OF_RAT_MUL,REAL_OF_RAT_MINV]
163QED
164
165val _ = temp_delsimps ["RATN_DIV_RATD"]
166
167Theorem REAL_OF_RAT_OF_NUM:
168 real_of_rat (&n) = &n
169Proof
170 simp[real_of_rat_def,real_of_int_num]
171QED
172
173Theorem REAL_OF_RAT_LT:
174 real_of_rat r1 < real_of_rat r2 <=> r1 < r2
175Proof
176 once_rewrite_tac[RATN_RATD_EQ_THM] >> simp[GSYM REAL_OF_RAT_DIV,REAL_OF_RAT_OF_NUM]
177 >> simp[REAL_NZ_IMP_LT,RATD_NZERO,REAL_DIV_LT,REAL_OF_RAT_OF_INT]
178 >> once_rewrite_tac[GSYM real_of_int_num]
179 >> once_rewrite_tac[GSYM real_of_int_mul]
180 >> simp[real_of_int_lt,RAT_LDIV_LES_POS,RDIV_MUL_OUT,RAT_RDIV_LES_POS]
181 >> once_rewrite_tac[GSYM rat_of_int_of_num]
182 >> simp[rat_of_int_MUL]
183QED
184
185Theorem REAL_OF_RAT_LE:
186 real_of_rat r1 <= real_of_rat r2 <=> r1 <= r2
187Proof
188 simp[REAL_LE_LT,rat_leq_def,REAL_OF_RAT_LT,REAL_OF_RAT_INJ]
189QED
190
191(* much, but not all, of the below is just for fun, mostly looking at proving Q is dense in R*)
192Theorem INT_BI_INDUCTION:
193 !P. (P (0:int) /\ !x. (P x <=> P (x+1))) <=> !x. P x
194Proof
195 rw[EQ_IMP_THM] >> Cases_on ‘x’ >> simp[]
196 >- (‘!m. P (&m)’ by (Induct_on ‘m’ >> simp[INT])
197 >> simp[])
198 >> ‘!m. P (-&m)’ by (
199 Induct_on ‘m’ >- simp[] \\
200 ‘P ((-&m + -1) + 1)’ by simp[INT_ADD_LINV,GSYM INT_ADD_ASSOC] \\
201 simp[INT,INT_NEG_ADD])
202 >> simp[]
203QED
204
205Theorem INT_FLOOR_REAL_OF_INT:
206 INT_FLOOR (real_of_int i) = i
207Proof
208 rw[real_of_int_def,INT_FLOOR_EQNS]
209QED
210
211Theorem IS_INT_REAL_OF_INT:
212 is_int x <=> ?i. x = real_of_int i
213Proof
214 rw[EQ_IMP_THM,is_int_def]
215 >-(qexists_tac ‘INT_FLOOR x’ >> simp[])
216 >- simp[INT_FLOOR_REAL_OF_INT]
217QED
218
219Theorem IS_INT_NUM:
220 is_int (&n)
221Proof
222 simp[is_int_def,INT_FLOOR_EQNS,real_of_int_num]
223QED
224
225Theorem IS_INT_ADD:
226 is_int x /\ is_int y ==> is_int (x+y)
227Proof
228 rw[IS_INT_REAL_OF_INT] >> qexists_tac ‘i+i'’ >> simp[real_of_int_add]
229QED
230
231Theorem IS_INT_MUL:
232 is_int x /\ is_int y ==> is_int (x*y)
233Proof
234 rw[IS_INT_REAL_OF_INT] >> qexists_tac ‘i * i'’ >> simp[real_of_int_mul]
235QED
236
237Theorem IS_INT_ADD2:
238 is_int x /\ is_int (x+y) ==> is_int y
239Proof
240 rw[IS_INT_REAL_OF_INT] >> qexists_tac ‘i' - i’ >> simp[real_of_int_sub,REAL_EQ_SUB_LADD,Once REAL_ADD_SYM]
241QED
242
243Theorem INT_FLOOR_ADD:
244 is_int x /\ is_int y ==> INT_FLOOR x + INT_FLOOR y = INT_FLOOR (x+y)
245Proof
246 rw[IS_INT_REAL_OF_INT] >> simp[INT_FLOOR_REAL_OF_INT]
247QED
248
249Theorem INT_FLOOR_MUL:
250 is_int x /\ is_int y ==> INT_FLOOR x * INT_FLOOR y = INT_FLOOR (x*y)
251Proof
252 rw[IS_INT_REAL_OF_INT] >> once_rewrite_tac[GSYM real_of_int_mul] >> simp[INT_FLOOR_REAL_OF_INT]
253QED
254
255Theorem REAL_PYTH:
256 !r1. ?x. is_int x /\ r1 < x
257Proof
258 rw[] >> qexists_tac ‘real_of_int (INT_FLOOR r1) + 1’
259 >> ‘is_int 1’ by simp[is_int_def,INT_FLOOR_EQNS,real_of_int_num]
260 >> simp[IS_INT_ADD,IS_INT_REAL_OF_INT]
261 >> ‘1 = real_of_int 1’ by simp[real_of_int_num]
262 >> simp[] >> once_rewrite_tac[GSYM real_of_int_add] >> simp[INT_FLOOR_BOUNDS]
263QED
264
265Theorem REAL_IS_INT_LT_LE:
266 is_int a /\ is_int b ==> (a<b <=> a+1 <= b)
267Proof
268 rw[IS_INT_REAL_OF_INT] >> once_rewrite_tac[GSYM real_of_int_num] >> once_rewrite_tac[GSYM real_of_int_add] >> simp[]
269QED
270
271val _ = temp_delsimps["real_of_int_11"]
272
273Theorem RAT_OF_INT_SUB:
274 rat_of_int a - rat_of_int b = rat_of_int (a-b)
275Proof
276 simp[RAT_SUB_ADDAINV,int_sub,rat_of_int_ADD,GSYM rat_of_int_ainv]
277QED
278
279Theorem REAL_LT_SUB_SWAP:
280 a:real < b-c <=> c<b-a
281Proof
282 simp[REAL_LT_SUB_LADD,REAL_ADD_SYM]
283QED
284
285Theorem REAL_Q_DENSE:
286 !r1 r2. r1 < r2 ==> ?q:rat. r1 < real_of_rat q /\ real_of_rat q < r2
287Proof
288 rw[]
289 >> ‘0 < r2 - r1’ by simp[REAL_SUB_LT]
290 >> ‘?n. is_int n /\ 1/(r2-r1) < n’ by simp[REAL_PYTH]
291 >> ‘0 < 1 / (r2 - r1)’ by simp[REAL_LT_DIV]
292 >> ‘0 < n’ by metis_tac[REAL_LT_TRANS]
293 >> ‘1/n < r2 - r1’ by (simp[REAL_LT_LDIV_EQ] >> once_rewrite_tac[REAL_MUL_SYM] >> simp[GSYM REAL_LT_LDIV_EQ])
294 >> ‘?q. q = (rat_of_int (INT_FLOOR (r2*2*n)) - 1) / rat_of_int (INT_FLOOR (2*n))’ by simp[]
295 >> qexists_tac ‘q’
296 >> ‘is_int (2*n)’ by simp[IS_INT_MUL,IS_INT_NUM]
297 >> ‘INT_FLOOR (2*n) <> 0’ by (
298 ‘1 <= n’ by (PURE_REWRITE_TAC[Once $ GSYM REAL_ADD_LID] >> simp[GSYM REAL_IS_INT_LT_LE,IS_INT_NUM])
299 >> once_rewrite_tac[GSYM real_of_int_11] >> simp[GSYM (iffLR is_int_def),real_of_int_num,REAL_LT_IMP_NE]
300 )
301 >> ‘r1 * (2*n) < r2 * (2 * n) - 2’ by (
302 simp[Once $ REAL_LT_SUB_SWAP,GSYM REAL_SUB_RDISTRIB, Once $ REAL_MUL_RID]
303 >> ‘2 = 1/n * (2*n)’ by (simp[real_div] >> simp[REAL_MUL_ASSOC,REAL_MUL_SYM,REAL_MUL_RINV,REAL_MUL_LID,REAL_LT_IMP_NE])
304 >> metis_tac[REAL_LT_RMUL,REAL_LT_MUL',arithmeticTheory.TWO,REAL_POS_LT]
305 )
306 >> rw[]
307 >> ‘rat_of_int (INT_FLOOR (2*n)) <> 0’ by simp[]
308 >> once_rewrite_tac[SPEC “1:num” $ GEN_ALL $ GSYM rat_of_int_of_num]
309 >> simp[RAT_OF_INT_SUB]
310 >> simp[GSYM REAL_OF_RAT_DIV] >> PURE_REWRITE_TAC[REAL_OF_RAT_OF_INT] >> simp[GSYM $ iffLR is_int_def]
311 >- (simp[REAL_LT_RDIV_EQ,REAL_LT_MUL',real_of_int_num]
312 >> ‘r2 * (2*n) - 2 < real_of_int (INT_FLOOR (r2 * 2 * n)) - 1’ suffices_by metis_tac[REAL_LT_TRANS]
313 >> once_rewrite_tac[SPECL [“x:real”,“y:real”,“1:real”] $ GSYM REAL_LT_RADD]
314 >> PURE_REWRITE_TAC[REAL_SUB_ADD]
315 >> ‘!x. x-2+1=x-1:real’ by simp[real_sub,GSYM REAL_ADD_ASSOC,add_ints]
316 >> simp[REAL_MUL_ASSOC, INT_FLOOR_BOUNDS']
317 )
318 >> simp[REAL_LT_LDIV_EQ,REAL_LT_MUL',real_of_int_num]
319 >> ‘-1 < 0:real’ by simp[]
320 >> metis_tac[REAL_ADD_RID,REAL_LTE_ADD2,INT_FLOOR_BOUNDS,REAL_ADD_SYM,REAL_MUL_ASSOC,real_sub]
321QED
322
323Theorem REAL_OF_RAT_NUM_CLAUSES:
324 (real_of_rat q = &n <=> q = &n) /\ (real_of_rat q = -&n <=> q = -&n) /\
325 (real_of_rat q < &n <=> q < &n) /\ (real_of_rat q < -&n <=> q < -&n) /\
326 (real_of_rat q <= &n <=> q <= &n) /\ (real_of_rat q <= -&n <=> q <= -&n) /\
327 (&n < real_of_rat q <=> &n < q) /\ (-&n < real_of_rat q <=> -&n < q) /\
328 (&n <= real_of_rat q <=> &n <= q) /\ (-&n <= real_of_rat q <=> -&n <= q)
329Proof
330 once_rewrite_tac[GSYM REAL_OF_RAT_OF_NUM] >> simp[REAL_OF_RAT_NEG,REAL_OF_RAT_INJ,REAL_OF_RAT_LT,REAL_OF_RAT_LE]
331QED
332
333Theorem REAL_OF_RAT_MAX:
334 max (real_of_rat r) (real_of_rat q) = real_of_rat (rat_max r q)
335Proof
336 Cases_on ‘r <= q’ >> simp[REAL_OF_RAT_LE,real_max,rat_max_def,rat_gre_def,GSYM RAT_LES_LEQ]
337QED
338
339Theorem REAL_OF_RAT_MIN:
340 min (real_of_rat r) (real_of_rat q) = real_of_rat (rat_min r q)
341Proof
342 Cases_on ‘r < q’
343 >> simp[Once $ cj 1 REAL_MIN_ACI,rat_min_def,GSYM REAL_NOT_LT,real_min,REAL_OF_RAT_LT]
344QED
345
346(* ========================================================================= *)
347(* Rational numbers as a subset of real numbers (real_rat_set or q_set) *)
348(* (was in util_probTheory and then in real_sigmaTheory) *)
349(* ========================================================================= *)
350
351Definition Q_SET :
352 real_rat_set = IMAGE real_of_rat UNIV
353End
354
355Theorem real_rat_set :
356 real_rat_set = {r | ?q. r = real_of_rat q}
357Proof
358 rw [Q_SET, Once EXTENSION]
359QED
360
361Overload q_set = “real_rat_set”
362
363(* Unicode Character 'DOUBLE-STRUCK CAPITAL Q' (U+211A) *)
364val _ = Unicode.unicode_version {u = UTF8.chr 0x211A, tmnm = "q_set"};
365val _ = TeX_notation {hol = "q_set", TeX = ("\\ensuremath{\\mathbb{Q}}", 1)};
366
367Theorem q_set_def :
368 q_set = {x:real | ?a b. (x = (&a/(&b))) /\ (0:real < &b)} UNION
369 {x:real | ?a b. (x = -(&a/(&b))) /\ (0:real < &b)}
370Proof
371 rw [real_rat_set, real_of_rat_def]
372 >> MATCH_MP_TAC SUBSET_ANTISYM
373 >> CONJ_TAC
374 >- (rw [SUBSET_DEF] \\
375 qabbrev_tac ‘i = RATN q’ \\
376 reverse (Cases_on ‘i < 0’)
377 >- (DISJ1_TAC >> rw [real_of_int_def] \\
378 qexistsl_tac [‘num_of_int i’, ‘RATD q’] >> rw [RATD_NZERO]) \\
379 DISJ2_TAC >> rw [real_of_int_def] \\
380 qexistsl_tac [‘num_of_int i’, ‘RATD q’] >> rw [RATD_NZERO] \\
381 ‘i <= 0’ by rw [] \\
382 ‘?n. i = -&n’ by PROVE_TAC [NUM_NEGINT_EXISTS] \\
383 simp [neg_rat])
384 >> rw [SUBSET_DEF]
385 >| [ (* goal 1 (of 2) *)
386 Cases_on ‘a = 0’
387 >- (rw [REAL_DIV_LZERO] >> Q.EXISTS_TAC ‘0’ >> rw [real_of_int_num]) \\
388 qabbrev_tac ‘c = gcd a b’ \\
389 MP_TAC (Q.SPECL [‘a’, ‘b’] FACTOR_OUT_GCD) >> rw [] \\
390 REWRITE_TAC [GSYM REAL_OF_NUM_MUL] \\
391 Know ‘((&c) :real) * &p / (&c * &q) = &p / &q’
392 >- (MATCH_MP_TAC REAL_DIV_LMUL_CANCEL >> rw [] \\
393 CCONTR_TAC >> rfs []) >> Rewr' \\
394 Q.EXISTS_TAC ‘rat_of_num p / rat_of_num q’ \\
395 ‘q <> 0’ by fs [] \\
396 rw [RATND_of_coprimes, real_of_int_num],
397 (* goal 2 (of 2) *)
398 Cases_on ‘a = 0’
399 >- (rw [REAL_DIV_LZERO] >> Q.EXISTS_TAC ‘0’ >> rw [real_of_int_num]) \\
400 qabbrev_tac ‘c = gcd a b’ \\
401 MP_TAC (Q.SPECL [‘a’, ‘b’] FACTOR_OUT_GCD) >> rw [] \\
402 REWRITE_TAC [GSYM REAL_OF_NUM_MUL] \\
403 Know ‘((&c) :real) * &p / (&c * &q) = &p / &q’
404 >- (MATCH_MP_TAC REAL_DIV_LMUL_CANCEL >> rw [] \\
405 CCONTR_TAC >> rfs []) >> Rewr' \\
406 Q.EXISTS_TAC ‘-rat_of_num p / rat_of_num q’ \\
407 ‘q <> 0’ by fs [] \\
408 rw [RATND_of_coprimes', neg_rat, real_of_int_num] ]
409QED
410
411Theorem real_rat_set_def = q_set_def
412
413Theorem QSET_COUNTABLE :
414 countable q_set
415Proof
416 RW_TAC std_ss [q_set_def] THEN
417 MATCH_MP_TAC union_countable THEN CONJ_TAC THENL
418 [RW_TAC std_ss [COUNTABLE_ALT] THEN
419 MP_TAC NUM_2D_BIJ_NZ_INV THEN RW_TAC std_ss [] THEN
420 Q.EXISTS_TAC `(\(a,b). &a/(&b)) o f` THEN RW_TAC std_ss [GSPECIFICATION] THEN
421 FULL_SIMP_TAC std_ss [BIJ_DEF,INJ_DEF,SURJ_DEF,IN_UNIV] THEN
422 PAT_X_ASSUM ``!x. x IN P ==> Q x y`` (MP_TAC o Q.SPEC `(&a,&b)`) THEN
423 RW_TAC std_ss [] THEN
424 FULL_SIMP_TAC std_ss [IN_CROSS,IN_UNIV,IN_SING,DIFF_DEF,
425 GSPECIFICATION,GSYM REAL_LT_NZ] THEN
426 `?y. f y = (a,b)` by METIS_TAC [] THEN
427 Q.EXISTS_TAC `y` THEN RW_TAC std_ss [], ALL_TAC] THEN
428 RW_TAC std_ss [COUNTABLE_ALT] THEN
429 MP_TAC NUM_2D_BIJ_NZ_INV THEN
430 RW_TAC std_ss [] THEN Q.EXISTS_TAC `(\(a,b). -(&a/(&b))) o f` THEN
431 RW_TAC std_ss [GSPECIFICATION] THEN
432 FULL_SIMP_TAC std_ss [BIJ_DEF,INJ_DEF,SURJ_DEF,IN_UNIV] THEN
433 PAT_X_ASSUM ``!x. x IN P ==> Q x y`` (MP_TAC o Q.SPEC `(&a,&b)`) THEN
434 RW_TAC std_ss [] THEN
435 FULL_SIMP_TAC std_ss [IN_CROSS,IN_UNIV,IN_SING,
436 DIFF_DEF,GSPECIFICATION,GSYM REAL_LT_NZ] THEN
437 `?y. f y = (a,b)` by METIS_TAC [] THEN Q.EXISTS_TAC `y` THEN
438 RW_TAC std_ss []
439QED
440
441Theorem countable_real_rat_set = QSET_COUNTABLE
442
443Theorem NUM_IN_QSET :
444 !n. &n IN q_set /\ -&n IN q_set
445Proof
446 rw [real_rat_set]
447 >- (Q.EXISTS_TAC ‘&n’ \\
448 rw [REAL_OF_RAT_OF_NUM])
449 >> rw [Once EQ_SYM_EQ, REAL_OF_RAT_NUM_CLAUSES]
450QED
451
452Theorem OPP_IN_QSET :
453 !x. x IN q_set ==> -x IN q_set
454Proof
455 rw [real_rat_set]
456 >> Q.EXISTS_TAC ‘-q’
457 >> rw [REAL_OF_RAT_NEG]
458QED
459
460Theorem INV_IN_QSET :
461 !x. x IN q_set /\ x <> 0 ==> 1/x IN q_set
462Proof
463 rw [real_rat_set]
464 >> Q.EXISTS_TAC ‘rat_minv q’
465 >> rw [GSYM REAL_INV_1OVER]
466 >> MATCH_MP_TAC REAL_OF_RAT_MINV
467 >> CCONTR_TAC >> fs []
468QED
469
470Theorem ADD_IN_QSET :
471 !x y. x IN q_set /\ y IN q_set ==> x + y IN q_set
472Proof
473 rw [real_rat_set]
474 >> Q.EXISTS_TAC ‘q + q'’
475 >> rw [REAL_OF_RAT_ADD]
476QED
477
478Theorem SUB_IN_QSET :
479 !x y. x IN q_set /\ y IN q_set ==> x - y IN q_set
480Proof
481 rw [real_rat_set]
482 >> Q.EXISTS_TAC ‘q - q'’
483 >> rw [REAL_OF_RAT_SUB]
484QED
485
486Theorem MUL_IN_QSET :
487 !x y. x IN q_set /\ y IN q_set ==> x * y IN q_set
488Proof
489 rw [real_rat_set]
490 >> Q.EXISTS_TAC ‘q * q'’
491 >> rw [REAL_OF_RAT_MUL]
492QED
493
494Theorem DIV_IN_QSET :
495 !x y. x IN q_set /\ y IN q_set /\ y <> 0 ==> x / y IN q_set
496Proof
497 rw [real_rat_set]
498 >> Q.EXISTS_TAC ‘q / q'’
499 >> MATCH_MP_TAC REAL_OF_RAT_DIV
500 >> CCONTR_TAC >> fs []
501QED
502
503Theorem Q_DENSE_IN_REAL :
504 !x y. x < y ==> ?r. r IN q_set /\ x < r /\ r < y
505Proof
506 rw [real_rat_set]
507 >> MP_TAC (Q.SPECL [‘x’, ‘y’] REAL_Q_DENSE) >> rw []
508 >> Q.EXISTS_TAC ‘real_of_rat q’ >> rw []
509 >> Q.EXISTS_TAC ‘q’ >> rw []
510QED
511
512Theorem Q_DENSE_IN_REAL_LEMMA :
513 !x y. 0 <= x /\ x < y ==> ?r. r IN q_set /\ x < r /\ r < y
514Proof
515 rpt STRIP_TAC
516 >> MATCH_MP_TAC Q_DENSE_IN_REAL >> rw []
517QED
518
519Theorem REAL_RAT_DENSE = Q_DENSE_IN_REAL
520