ratScript.sml
1(***************************************************************************
2 *
3 * Theory of rational numbers.
4 *
5 * Jens Brandt, November 2005
6 *
7 ***************************************************************************)
8Theory rat
9Ancestors
10 arithmetic pred_set integer intExtension frac gcd divides
11 primeFactor
12Libs
13 BasicProvers intLib intExtensionLib fracLib ratUtils quotient
14 schneiderUtils ratPP[qualified]
15
16
17val arith_ss = old_arith_ss
18
19val ERR = mk_HOL_ERR "ratScript"
20
21(*--------------------------------------------------------------------------*
22 * rat_equiv: definition and proof of equivalence relation
23 *--------------------------------------------------------------------------*)
24
25(* definition of equivalence relation *)
26Definition rat_equiv_def:
27 rat_equiv f1 f2 <=> (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
28End
29
30(* RAT_EQUIV_REF: |- !a:frac. rat_equiv a a *)
31Theorem RAT_EQUIV_REF: !a:frac. rat_equiv a a
32Proof
33 STRIP_TAC THEN REWRITE_TAC[rat_equiv_def]
34QED
35
36(* RAT_EQUIV_SYM: |- !a b. rat_equiv a b = rat_equiv b a *)
37Theorem RAT_EQUIV_SYM:
38 !a b. rat_equiv a b <=> rat_equiv b a
39Proof
40 rpt STRIP_TAC >> REWRITE_TAC[rat_equiv_def] >> MATCH_ACCEPT_TAC EQ_SYM_EQ
41QED
42
43val INT_ENTIRE' = CONV_RULE (ONCE_DEPTH_CONV (LHS_CONV SYM_CONV)) INT_ENTIRE ;
44val FRAC_DNMNZ = GSYM (MATCH_MP INT_LT_IMP_NE (SPEC_ALL FRAC_DNMPOS)) ;
45val FRAC_DNMNN = let val th = MATCH_MP INT_LT_IMP_LE (SPEC_ALL FRAC_DNMPOS)
46 in MATCH_MP (snd (EQ_IMP_RULE (SPEC_ALL INT_NOT_LT))) th end ;
47fun ifcan f x = f x handle _ => x ;
48
49Theorem RAT_EQUIV_NMR_Z_IFF:
50 !a b. rat_equiv a b ==> ((frac_nmr a = 0) <=> (frac_nmr b = 0))
51Proof
52 REWRITE_TAC[rat_equiv_def] THEN
53 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
54 FULL_SIMP_TAC std_ss [INT_MUL_LZERO, INT_MUL_RZERO,
55 INT_ENTIRE, INT_ENTIRE', FRAC_DNMNZ]
56QED
57
58Theorem RAT_EQUIV_NMR_GTZ_IFF:
59 !a b. rat_equiv a b ==> (frac_nmr a > 0 <=> frac_nmr b > 0)
60Proof
61 REWRITE_TAC[rat_equiv_def] THEN
62 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
63 RULE_ASSUM_TAC (ifcan (AP_TERM “int_lt 0i”)) THEN
64 FULL_SIMP_TAC std_ss [int_gt, INT_MUL_SIGN_CASES, FRAC_DNMPOS, FRAC_DNMNN ]
65QED
66
67Theorem RAT_EQUIV_NMR_LTZ_IFF:
68 !a b. rat_equiv a b ==> ((frac_nmr a < 0) <=> (frac_nmr b < 0))
69Proof
70 REWRITE_TAC[rat_equiv_def] THEN
71 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
72 RULE_ASSUM_TAC (ifcan (AP_TERM “int_gt 0i”)) THEN
73 FULL_SIMP_TAC std_ss [int_gt, INT_MUL_SIGN_CASES, FRAC_DNMPOS, FRAC_DNMNN ]
74QED
75
76Theorem RAT_NMR_Z_IFF_EQUIV:
77 !a b. (frac_nmr a = 0) ==> (rat_equiv a b <=> (frac_nmr b = 0))
78Proof
79 REWRITE_TAC[rat_equiv_def] THEN
80 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THEN
81 REV_FULL_SIMP_TAC std_ss [INT_MUL_LZERO, INT_MUL_RZERO,
82 INT_ENTIRE, INT_ENTIRE', FRAC_DNMNZ]
83QED
84
85val times_dnmb = MATCH_MP INT_EQ_RMUL_EXP (Q.SPEC `b` FRAC_DNMPOS) ;
86
87Theorem box_equals[local]:
88 (a = b) ==> (c = a) /\ (d = b) ==> (c = d)
89Proof
90 REPEAT STRIP_TAC THEN BasicProvers.VAR_EQ_TAC THEN ASM_SIMP_TAC bool_ss []
91QED
92
93Theorem RAT_EQUIV_TRANS:
94 !a b c. rat_equiv a b /\ rat_equiv b c ==> rat_equiv a c
95Proof
96 REPEAT GEN_TAC THEN Cases_on `frac_nmr b = 0`
97 THENL [ STRIP_TAC THEN
98 RULE_ASSUM_TAC (ifcan (MATCH_MP RAT_EQUIV_NMR_Z_IFF)) THEN
99 FULL_SIMP_TAC std_ss [RAT_NMR_Z_IFF_EQUIV],
100 REWRITE_TAC[rat_equiv_def] THEN STRIP_TAC THEN
101 ONCE_REWRITE_TAC [times_dnmb] THEN
102 FIRST_X_ASSUM (fn th => ONCE_REWRITE_TAC [MATCH_MP INT_EQ_LMUL2 th]) THEN
103 POP_ASSUM_LIST (fn [thbc, thab] => ASSUME_TAC
104 (MK_COMB (AP_TERM ``int_mul`` thab, thbc))) THEN
105 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN
106 CONJ_TAC THEN CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM)) ]
107QED
108
109val RAT_EQUIV_TRANS' = REWRITE_RULE [GSYM AND_IMP_INTRO] RAT_EQUIV_TRANS ;
110
111fun e2tac tthm = FIRST_X_ASSUM (fn th1 =>
112 let val tha1 = MATCH_MP tthm th1 ;
113 in FIRST_X_ASSUM (fn th2 => ACCEPT_TAC (MATCH_MP tha1 th2)) end) ;
114
115Theorem RAT_EQUIV:
116 !f1 f2. rat_equiv f1 f2 = (rat_equiv f1 = rat_equiv f2)
117Proof
118 REPEAT GEN_TAC THEN EQ_TAC
119 THENL [
120 REWRITE_TAC[FUN_EQ_THM] THEN
121 REPEAT STRIP_TAC THEN EQ_TAC THEN_LT
122 NTH_GOAL (ONCE_REWRITE_TAC [RAT_EQUIV_SYM]) 1 THEN
123 DISCH_TAC THEN e2tac RAT_EQUIV_TRANS',
124 DISCH_TAC THEN ASM_SIMP_TAC bool_ss [RAT_EQUIV_REF]]
125QED
126
127(*--------------------------------------------------------------------------*
128 * RAT_EQUIV_ALT
129 *
130 * |- !a. rat_equiv a =
131 * \x. (?b c. 0<b /\ 0<c /\
132 * (frac_mul a (abs_frac(b,b)) = frac_mul x (abs_frac(c,c)) ))
133 *
134 * alternative representation of equivalence relation
135 *--------------------------------------------------------------------------*)
136
137fun feqconv thm = let val thm' = UNDISCH_ALL (SPEC_ALL thm) ;
138 in DEPTH_CONV (REWR_CONV_A thm') end ;
139fun feqtac thm = VALIDATE (POP_ASSUM (ASSUME_TAC o CONV_RULE (feqconv thm))) ;
140
141fun msprod th = let val [thbc, thab] = CONJUNCTS th
142 in MK_COMB (AP_TERM ``int_mul`` (MATCH_MP EQ_SYM thab), thbc) end ;
143
144Theorem RAT_EQUIV_ALT:
145 !a. rat_equiv a =
146 λx. (?b c. 0<b /\ 0<c /\
147 (frac_mul a (abs_frac(b,b)) = frac_mul x (abs_frac(c,c)) ))
148Proof
149 SIMP_TAC bool_ss [FUN_EQ_THM, rat_equiv_def, frac_mul_def] THEN
150 REPEAT GEN_TAC THEN EQ_TAC
151 >- (DISCH_TAC THEN
152 EXISTS_TAC ``frac_dnm x`` THEN EXISTS_TAC ``frac_dnm a`` THEN
153 ASM_SIMP_TAC bool_ss [FRAC_DNMPOS, NMR, DNM] THEN
154 VALIDATE (CONV_TAC (feqconv FRAC_EQ)) THEN
155 TRY (irule INT_MUL_POS_SIGN >> conj_tac >> irule FRAC_DNMPOS) THEN
156 gs[AC INT_MUL_ASSOC INT_MUL_COMM]) >>
157 REPEAT STRIP_TAC THEN
158 REV_FULL_SIMP_TAC bool_ss [NMR, DNM] THEN feqtac FRAC_EQ THEN
159 TRY (irule INT_MUL_POS_SIGN THEN
160 ASM_SIMP_TAC bool_ss [FRAC_DNMPOS]) THEN
161 POP_ASSUM (ASSUME_TAC o msprod) THEN
162 FIRST_X_ASSUM (fn th =>
163 ONCE_REWRITE_TAC [MATCH_MP INT_EQ_RMUL_EXP th]) THEN
164 FIRST_X_ASSUM (fn th =>
165 ONCE_REWRITE_TAC [MATCH_MP INT_EQ_RMUL_EXP th]) THEN
166 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN
167 CONJ_TAC THEN CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM))
168QED
169
170(*--------------------------------------------------------------------------*
171 * type definition
172 *--------------------------------------------------------------------------*)
173
174(* following also stored as rat_QUOTIENT *)
175Theorem rat_def =
176 define_quotient_type "rat" "abs_rat" "rep_rat" RAT_EQUIV
177
178val QUOTIENT_def = quotientTheory.QUOTIENT_def
179val rat_thm = REWRITE_RULE[QUOTIENT_def] rat_def ; (* was rat_def *)
180
181Theorem rat_type_thm = REWRITE_RULE[QUOTIENT_def, RAT_EQUIV_REF] rat_def
182
183Theorem rat_equiv_reps: rat_equiv (rep_rat r1) (rep_rat r2) = (r1 = r2)
184Proof REWRITE_TAC [rat_type_thm]
185QED
186
187Theorem rat_equiv_rep_abs: rat_equiv (rep_rat (abs_rat f)) f
188Proof
189 REWRITE_TAC [rat_type_thm]
190QED
191
192(*--------------------------------------------------------------------------*
193 * operations
194 *--------------------------------------------------------------------------*)
195
196(* numerator, denominator, sign of a fraction *)
197Definition rat_nmr_def: rat_nmr r = frac_nmr (rep_rat r)
198End
199Definition rat_dnm_def: rat_dnm r = frac_dnm (rep_rat r)
200End
201Definition rat_sgn_def: rat_sgn r = frac_sgn (rep_rat r)
202End
203
204(* additive, multiplicative inverse of a fraction *)
205Definition rat_0_def: rat_0 = abs_rat( frac_0 )
206End
207Definition rat_1_def: rat_1 = abs_rat( frac_1 )
208End
209
210(* neutral elements *)
211Definition rat_ainv_def: rat_ainv r1 = abs_rat( frac_ainv (rep_rat r1))
212End
213Definition rat_minv_def: rat_minv r1 = abs_rat( frac_minv (rep_rat r1))
214End
215
216(* basic arithmetics *)
217Definition rat_add_def[nocompute]:
218 rat_add r1 r2 = abs_rat( frac_add (rep_rat r1) (rep_rat r2) )
219End
220Definition rat_sub_def[nocompute]:
221 rat_sub r1 r2 = abs_rat( frac_sub (rep_rat r1) (rep_rat r2) )
222End
223Definition rat_mul_def[nocompute]:
224 rat_mul r1 r2 = abs_rat( frac_mul (rep_rat r1) (rep_rat r2) )
225End
226Definition rat_div_def[nocompute]:
227 rat_div r1 r2 = abs_rat( frac_div (rep_rat r1) (rep_rat r2) )
228End
229
230(* order relations *)
231Definition rat_les_def: rat_les r1 r2 <=> (rat_sgn (rat_sub r2 r1) = 1)
232End
233Definition rat_gre_def: rat_gre r1 r2 = rat_les r2 r1
234End
235Definition rat_leq_def: rat_leq r1 r2 <=> rat_les r1 r2 \/ (r1=r2)
236End
237Definition rat_geq_def: rat_geq r1 r2 = rat_leq r2 r1
238End
239
240
241
242(* construction of rational numbers, support of numerals *)
243Definition rat_cons_def:
244 rat_cons (nmr:int) (dnm:int) =
245 abs_rat (abs_frac(SGN nmr * SGN dnm * ABS nmr, ABS dnm))
246End
247
248Definition rat_of_num_def: (rat_of_num 0 = rat_0) /\ (rat_of_num (SUC 0) = rat_1) /\ (rat_of_num (SUC (SUC n)) = rat_add (rat_of_num (SUC n)) rat_1)
249End
250val _ = add_numeral_form(#"q", SOME "rat_of_num");
251
252Theorem rat_0: 0q = abs_rat( frac_0 )
253Proof
254 PROVE_TAC[rat_of_num_def, rat_0_def]
255QED
256
257Theorem rat_1: 1q = abs_rat( frac_1 )
258Proof
259 SUBST_TAC[ARITH_PROVE ``1=SUC 0``] THEN RW_TAC arith_ss [rat_of_num_def, rat_1_def]
260QED
261
262(*--------------------------------------------------------------------------
263 * parser rules
264 *--------------------------------------------------------------------------*)
265
266val _ = set_fixity "//" (Infixl 600)
267
268Overload "+" = ``rat_add``
269Overload "-" = ``rat_sub``
270Overload "*" = ``rat_mul``
271val _ = overload_on (GrammarSpecials.decimal_fraction_special, ``rat_div``);
272Overload "/" = ``rat_div``
273Overload "<" = ``rat_les``
274Overload "<=" = ``rat_leq``
275Overload ">" = ``rat_gre``
276Overload ">=" = ``rat_geq``
277Overload "~" = ``rat_ainv``
278Overload numeric_negate = ``rat_ainv``
279Overload "//" = ``rat_cons``
280
281val _ = add_ML_dependency "ratPP"
282val _ = add_user_printer ("rat.decimalfractions",
283 ``&(NUMERAL x):rat / &(NUMERAL y):rat``)
284
285(*--------------------------------------------------------------------------
286 * RAT: thm
287 * |- !r. abs_rat ( rep_rat r ) = r
288 *--------------------------------------------------------------------------*)
289
290Theorem RAT: !r. abs_rat ( rep_rat r ) = r
291Proof
292 ACCEPT_TAC (CONJUNCT1 rat_thm)
293QED
294
295(*--------------------------------------------------------------------------
296 * some lemmas
297 *--------------------------------------------------------------------------*)
298
299Theorem RAT_ABS_EQUIV:
300 !f1 f2. (abs_rat f1 = abs_rat f2) = rat_equiv f1 f2
301Proof
302 REWRITE_TAC [rat_type_thm]
303QED
304
305Theorem REP_ABS_EQUIV[local]:
306 !a. rat_equiv a (rep_rat (abs_rat a))
307Proof
308 REWRITE_TAC [rat_type_thm]
309QED
310
311val RAT_ABS_EQUIV' = GSYM RAT_ABS_EQUIV ;
312val REP_ABS_EQUIV' = ONCE_REWRITE_RULE [RAT_EQUIV_SYM] REP_ABS_EQUIV ;
313
314Theorem REP_ABS_DFN_EQUIV[local]:
315 !x. frac_nmr x * frac_dnm (rep_rat(abs_rat x)) = frac_nmr (rep_rat(abs_rat x)) * frac_dnm x
316Proof
317 GEN_TAC THEN
318 REWRITE_TAC[GSYM rat_equiv_def] THEN
319 REWRITE_TAC[REP_ABS_EQUIV]
320QED
321
322Theorem RAT_IMP_EQUIV[local]:
323 !r1 r2. (r1 = r2) ==> rat_equiv r1 r2
324Proof
325 REPEAT STRIP_TAC THEN
326 ASM_REWRITE_TAC[RAT_EQUIV_REF]
327QED
328
329(*==========================================================================
330 * equivalence of rational numbers
331 *==========================================================================*)
332
333(*--------------------------------------------------------------------------
334 * RAT_EQ: thm
335 * |- !f1 f2. (abs_rat f1 = abs_rat f2)
336 * = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
337 *--------------------------------------------------------------------------*)
338
339Theorem RAT_EQ:
340 !f1 f2. (abs_rat f1 = abs_rat f2) =
341 (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
342Proof
343 REPEAT GEN_TAC THEN
344 REWRITE_TAC [RAT_ABS_EQUIV, rat_equiv_def]
345QED
346
347(*--------------------------------------------------------------------------
348 * RAT_EQ_ALT: thm
349 * |- ! r1 r2. (r1=r2) = (rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1)
350 *--------------------------------------------------------------------------*)
351
352Theorem RAT_EQ_ALT: ! r1 r2. (r1=r2) = (rat_nmr r1 * rat_dnm r2 = rat_nmr r2 * rat_dnm r1)
353Proof
354 REPEAT GEN_TAC THEN
355 REWRITE_TAC[rat_nmr_def, rat_dnm_def] THEN
356 REWRITE_TAC[GSYM rat_equiv_def] THEN
357 REWRITE_TAC[rat_type_thm]
358QED
359
360(*==========================================================================
361 * congruence theorems
362 *==========================================================================*)
363
364(*--------------------------------------------------------------------------
365 * RAT_NMREQ0_CONG: thm
366 * |- !f1. (frac_nmr (rep_rat (abs_rat f1)) = 0) = (frac_nmr f1 = 0)
367 *
368 * RAT_NMRLT0_CONG: thmRAT_NMREQ0_CONG
369 * |- !f1. (frac_nmr (rep_rat (abs_rat f1)) < 0) = (frac_nmr f1 < 0)
370 *
371 * RAT_NMRGT0_CONG: thmRAT_NMREQ0_CONG
372 * |- !f1. (frac_nmr (rep_rat (abs_rat f1)) > 0) = (frac_nmr f1 > 0)
373 *
374 *--------------------------------------------------------------------------*)
375
376Theorem RAT_NMREQ0_CONG:
377 !f1. (frac_nmr (rep_rat (abs_rat f1)) = 0) = (frac_nmr f1 = 0)
378Proof
379 GEN_TAC THEN MATCH_ACCEPT_TAC
380 (MATCH_MP RAT_EQUIV_NMR_Z_IFF (SPEC_ALL REP_ABS_EQUIV'))
381QED
382
383Theorem RAT_NMRLT0_CONG:
384 !f1. (frac_nmr (rep_rat (abs_rat f1)) < 0) = (frac_nmr f1 < 0)
385Proof
386 GEN_TAC THEN MATCH_ACCEPT_TAC
387 (MATCH_MP RAT_EQUIV_NMR_LTZ_IFF (SPEC_ALL REP_ABS_EQUIV'))
388QED
389
390Theorem RAT_NMRGT0_CONG:
391 !f1. 0 < frac_nmr (rep_rat (abs_rat f1)) <=> 0 < frac_nmr f1
392Proof
393 GEN_TAC THEN MATCH_ACCEPT_TAC
394 (MATCH_MP (SRULE [int_gt] RAT_EQUIV_NMR_GTZ_IFF)
395 (SPEC_ALL REP_ABS_EQUIV'))
396QED
397
398(*--------------------------------------------------------------------------
399 * RAT_SGN_CONG: thm
400 * |- !f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1
401 *--------------------------------------------------------------------------*)
402
403Theorem RAT_SGN_CONG: !f1. frac_sgn (rep_rat (abs_rat f1)) = frac_sgn f1
404Proof
405 GEN_TAC THEN
406 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
407 REWRITE_TAC[RAT_NMREQ0_CONG, RAT_NMRLT0_CONG]
408QED
409
410(*--------------------------------------------------------------------------
411 * RAT_AINV_CONG: thm
412 * |- !x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x)
413 *--------------------------------------------------------------------------*)
414
415Theorem RAT_AINV_CONG: !x. abs_rat (frac_ainv (rep_rat (abs_rat x))) = abs_rat (frac_ainv x)
416Proof
417 REPEAT GEN_TAC THEN
418 REWRITE_TAC[RAT_ABS_EQUIV] THEN
419 REWRITE_TAC[rat_equiv_def,frac_ainv_def] THEN
420 SIMP_TAC bool_ss [NMR, DNM, FRAC_DNMPOS] THEN
421 REWRITE_TAC[INT_MUL_CALCULATE,INT_EQ_NEG] THEN
422 REWRITE_TAC[GSYM rat_equiv_def] THEN
423 ONCE_REWRITE_TAC[RAT_EQUIV_SYM] THEN
424 REWRITE_TAC[REP_ABS_EQUIV]
425QED
426
427(*--------------------------------------------------------------------------
428 * RAT_MINV_CONG: thm
429 * |- !x. ~(frac_nmr x=0) ==>
430 * (abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x))
431 *--------------------------------------------------------------------------*)
432
433Theorem FRAC_MINV_EQUIV:
434 ~(frac_nmr y=0) ==> rat_equiv x y ==>
435 rat_equiv (frac_minv x) (frac_minv y)
436Proof
437 DISCH_TAC THEN DISCH_THEN (fn th => MP_TAC th THEN ASSUME_TAC th) THEN
438 POP_ASSUM (ASSUME_TAC o MATCH_MP RAT_EQUIV_NMR_Z_IFF) THEN
439 REWRITE_TAC[frac_minv_def, rat_equiv_def, frac_sgn_def] THEN
440 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
441 (TRY (irule INT_ABS_NOT0POS THEN ASM_SIMP_TAC bool_ss [])) THEN
442 REWRITE_TAC[SGN_def] THEN REPEAT IF_CASES_TAC THEN
443 ASM_SIMP_TAC int_ss [INT_ABS,
444 GSYM INT_NEG_MINUS1, GSYM INT_NEG_LMUL, GSYM INT_NEG_RMUL] THEN
445 SIMP_TAC bool_ss [INT_MUL_COMM]
446QED
447
448Theorem RAT_MINV_CONG:
449 !x. ~(frac_nmr x=0) ==>
450 (abs_rat (frac_minv (rep_rat (abs_rat x))) = abs_rat (frac_minv x))
451Proof
452 REPEAT STRIP_TAC THEN
453 IMP_RES_TAC FRAC_MINV_EQUIV THEN
454 ASSUME_TAC (Q.SPEC `x` REP_ABS_EQUIV') THEN
455 RES_TAC THEN ASM_SIMP_TAC bool_ss [RAT_ABS_EQUIV]
456QED
457
458(*--------------------------------------------------------------------------
459 * RAT_ADD_CONG1: thm
460 * |- !x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)
461 *
462 * RAT_ADD_CONG2: thm
463 * |- !x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)
464 *
465 * RAT_ADD_CONG: thm
466 * |- !x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y) /\
467 * !x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)
468 *--------------------------------------------------------------------------*)
469
470Theorem FRAC_ADD_EQUIV1:
471 rat_equiv x x' ==> rat_equiv (frac_add x y) (frac_add x' y)
472Proof
473 REWRITE_TAC[frac_add_def, rat_equiv_def] THEN
474 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
475 TRY (irule INT_MUL_POS_SIGN >> conj_tac >> irule FRAC_DNMPOS) THEN
476 REWRITE_TAC[INT_RDISTRIB] THEN DISCH_TAC THEN
477 MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC]
478 THENL [
479 RULE_ASSUM_TAC (AP_TERM ``int_mul (frac_dnm y * frac_dnm y)``) THEN
480 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN CONJ_TAC,
481 ALL_TAC ] THEN
482 CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM))
483QED
484
485Theorem RAT_ADD_CONG1:
486 !x y. abs_rat (frac_add (rep_rat (abs_rat x)) y) = abs_rat (frac_add x y)
487Proof
488 REPEAT STRIP_TAC THEN
489 SIMP_TAC bool_ss [RAT_ABS_EQUIV] THEN
490 irule FRAC_ADD_EQUIV1 THEN irule REP_ABS_EQUIV'
491QED
492
493Theorem RAT_ADD_CONG2: !x y. abs_rat (frac_add x (rep_rat (abs_rat y))) = abs_rat (frac_add x y)
494Proof
495 ONCE_REWRITE_TAC[FRAC_ADD_COMM] THEN
496 REWRITE_TAC[RAT_ADD_CONG1]
497QED
498
499Theorem RAT_ADD_CONG = CONJ RAT_ADD_CONG1 RAT_ADD_CONG2;
500
501(*--------------------------------------------------------------------------
502 * RAT_MUL_CONG1: thm
503 * |- !x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)
504 *
505 * RAT_MUL_CONG2: thm
506 * |- !x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)
507 *
508 * RAT_MUL_CONG: thm
509 * |- !x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y) /\
510 * !x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)
511 *--------------------------------------------------------------------------*)
512
513Theorem FRAC_MUL_EQUIV1:
514 rat_equiv x x' ==> rat_equiv (frac_mul x y) (frac_mul x' y)
515Proof
516 REWRITE_TAC[frac_mul_def, rat_equiv_def] THEN
517 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
518 TRY (irule INT_MUL_POS_SIGN >> conj_tac >> irule FRAC_DNMPOS) >> DISCH_TAC >>
519 RULE_ASSUM_TAC (AP_TERM ``int_mul (frac_nmr y * frac_dnm y)``) THEN
520 POP_ASSUM (fn th => MATCH_MP_TAC (MATCH_MP box_equals th)) THEN
521 CONJ_TAC THEN CONV_TAC (AC_CONV (INT_MUL_ASSOC,INT_MUL_SYM))
522QED
523
524Theorem FRAC_MUL_EQUIV2 =
525 ONCE_REWRITE_RULE [FRAC_MUL_COMM] FRAC_MUL_EQUIV1 ;
526
527Theorem RAT_MUL_CONG1:
528 !x y. abs_rat (frac_mul (rep_rat (abs_rat x)) y) = abs_rat (frac_mul x y)
529Proof
530 REPEAT STRIP_TAC THEN
531 SIMP_TAC bool_ss [RAT_ABS_EQUIV] THEN
532 irule FRAC_MUL_EQUIV1 THEN irule REP_ABS_EQUIV'
533QED
534
535Theorem RAT_MUL_CONG2: !x y. abs_rat (frac_mul x (rep_rat (abs_rat y))) = abs_rat (frac_mul x y)
536Proof
537 ONCE_REWRITE_TAC[FRAC_MUL_COMM] THEN
538 RW_TAC int_ss[RAT_MUL_CONG1]
539QED
540
541Theorem RAT_MUL_CONG = CONJ RAT_MUL_CONG1 RAT_MUL_CONG2;
542
543(*--------------------------------------------------------------------------
544 * RAT_SUB_CONG1: thm
545 * |- !x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)
546 *
547 * RAT_SUB_CONG2: thm
548 * |- !x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)
549 *
550 * RAT_SUB_CONG: thm
551 * |- !x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y) /\
552 * !x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)
553 *--------------------------------------------------------------------------*)
554
555Theorem RAT_SUB_CONG1: !x y. abs_rat (frac_sub (rep_rat (abs_rat x)) y) = abs_rat (frac_sub x y)
556Proof
557 REWRITE_TAC[frac_sub_def] THEN
558 REWRITE_TAC[RAT_ADD_CONG]
559QED
560
561Theorem RAT_SUB_CONG2: !x y. abs_rat (frac_sub x (rep_rat (abs_rat y))) = abs_rat (frac_sub x y)
562Proof
563 ONCE_REWRITE_TAC[GSYM FRAC_AINV_SUB] THEN
564 ONCE_REWRITE_TAC[GSYM RAT_AINV_CONG] THEN
565 REWRITE_TAC[RAT_SUB_CONG1]
566QED
567
568Theorem RAT_SUB_CONG = CONJ RAT_SUB_CONG1 RAT_SUB_CONG2;
569
570(*--------------------------------------------------------------------------
571 * RAT_DIV_CONG1: thm
572 * |- !x y. ~(frac_nmr y = 0) ==>
573 * (abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y))
574 *
575 * RAT_DIV_CONG2: thm
576 * |- !x y. ~(frac_nmr y = 0) ==>
577 (abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y))
578 *
579 * RAT_DIV_CONG: thm
580 * |- !x y. ~(frac_nmr y = 0) ==>
581 * (abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y)) /\
582 * !x y. ~(frac_nmr y = 0) ==>
583 (abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y))
584 *--------------------------------------------------------------------------*)
585
586Theorem RAT_DIV_CONG1:
587 !x y. ~(frac_nmr y = 0) ==>
588 (abs_rat (frac_div (rep_rat (abs_rat x)) y) = abs_rat (frac_div x y))
589Proof
590 REPEAT STRIP_TAC THEN
591 REWRITE_TAC[frac_div_def] THEN
592 REWRITE_TAC[RAT_MUL_CONG]
593QED
594
595Theorem RAT_DIV_CONG2:
596 !x y. ~(frac_nmr y = 0) ==>
597 (abs_rat (frac_div x (rep_rat (abs_rat y))) = abs_rat (frac_div x y))
598Proof
599 REPEAT STRIP_TAC THEN
600 REWRITE_TAC[frac_div_def, RAT_ABS_EQUIV] THEN
601 irule FRAC_MUL_EQUIV2 THEN
602 IMP_RES_THEN MATCH_MP_TAC FRAC_MINV_EQUIV THEN
603 irule rat_equiv_rep_abs
604QED
605
606Theorem RAT_DIV_CONG = CONJ RAT_DIV_CONG1 RAT_DIV_CONG2;
607
608(*==========================================================================
609 * numerator and denominator
610 *==========================================================================*)
611
612(*--------------------------------------------------------------------------
613 * RAT_NMRDNM_EQ: thm
614 * |- (abs_rat(abs_frac(frac_nmr f1,frac_dnm f1)) = 1q) = (frac_nmr f1 = frac_dnm f1)
615 *--------------------------------------------------------------------------*)
616
617Theorem RAT_NMRDNM_EQ:
618 (abs_rat(abs_frac(frac_nmr f1,frac_dnm f1)) = 1q) <=>
619 (frac_nmr f1 = frac_dnm f1)
620Proof
621 SIMP_TAC bool_ss [rat_equiv_def, RAT_ABS_EQUIV,
622 rat_1, frac_1_def, NMR, DNM, FRAC_DNMPOS, INT_LT_01,
623 INT_MUL_LID, INT_MUL_RID]
624QED
625
626(*==========================================================================
627 * calculation
628 *==========================================================================*)
629
630Theorem RAT_AINV_CALCULATE:
631 !f1. rat_ainv (abs_rat(f1)) = abs_rat( frac_ainv f1 )
632Proof
633 REPEAT GEN_TAC THEN REWRITE_TAC[rat_ainv_def] THEN PROVE_TAC[RAT_AINV_CONG]
634QED
635
636(*--------------------------------------------------------------------------
637 * RAT_MINV_CALCULATE: thm
638 * |- !f1. rat_ainv (abs_rat(f1)) = abs_rat( frac_ainv f1 )
639 *--------------------------------------------------------------------------*)
640
641Theorem RAT_MINV_CALCULATE: !f1. ~(0 = frac_nmr f1) ==> (rat_minv (abs_rat(f1)) = abs_rat( frac_minv f1 ))
642Proof
643 REPEAT GEN_TAC THEN
644 REWRITE_TAC[rat_minv_def] THEN
645 PROVE_TAC[RAT_MINV_CONG]
646QED
647
648(*--------------------------------------------------------------------------
649 * RAT_ADD_CALCULATE: thm
650 * |- !f1 f2. rat_add (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_add f1 f2 )
651 *--------------------------------------------------------------------------*)
652
653Theorem RAT_ADD_CALCULATE:
654 !f1 f2. rat_add (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_add f1 f2 )
655Proof
656 REPEAT GEN_TAC THEN REWRITE_TAC[rat_add_def] THEN PROVE_TAC[RAT_ADD_CONG]
657QED
658
659(*--------------------------------------------------------------------------
660 * RAT_SUB_CALCULATE: thm
661 * |- !f1 f2. rat_sub (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_sub f1 f2 )
662 *--------------------------------------------------------------------------*)
663
664Theorem RAT_SUB_CALCULATE:
665 !f1 f2. rat_sub (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_sub f1 f2 )
666Proof
667 REPEAT GEN_TAC THEN REWRITE_TAC[rat_sub_def] THEN PROVE_TAC[RAT_SUB_CONG]
668QED
669
670(*--------------------------------------------------------------------------
671 * RAT_MUL_CALCULATE: thm
672 * |- !f1 f2. rat_mul (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_mul f1 f2 )
673 *--------------------------------------------------------------------------*)
674
675Theorem RAT_MUL_CALCULATE:
676 !f1 f2. rat_mul (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_mul f1 f2 )
677Proof
678 REPEAT GEN_TAC THEN REWRITE_TAC[rat_mul_def] THEN PROVE_TAC[RAT_MUL_CONG]
679QED
680
681(* ----------------------------------------------------------------------
682 RAT_DIV_CALCULATE: thm
683 |- !f1 f2.
684 frac_nmr f2 <> 0 ==>
685 (rat_div (abs_rat f1) (abs_rat f2) = abs_rat(frac_div f1 f2))
686 ---------------------------------------------------------------------- *)
687
688Theorem RAT_DIV_CALCULATE:
689 !f1 f2. frac_nmr f2 <> 0 ==>
690 (rat_div (abs_rat(f1)) (abs_rat(f2)) = abs_rat( frac_div f1 f2 ))
691Proof
692 REPEAT STRIP_TAC THEN REWRITE_TAC[rat_div_def] THEN PROVE_TAC[RAT_DIV_CONG]
693QED
694
695(*--------------------------------------------------------------------------
696 * RAT_EQ_CALCULATE: thm
697 * |- !f1 f2. (abs_rat f1 = abs_rat f2) = (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
698 *--------------------------------------------------------------------------*)
699
700Theorem RAT_EQ_CALCULATE:
701 !f1 f2. (abs_rat f1 = abs_rat f2) <=>
702 (frac_nmr f1 * frac_dnm f2 = frac_nmr f2 * frac_dnm f1)
703Proof
704 PROVE_TAC[RAT_ABS_EQUIV, rat_equiv_def]
705QED
706
707
708(* ----------------------------------------------------------------------
709 RAT_LES_CALCULATE: thm
710 |- !f1 f2. (abs_rat f1 < abs_rat f2) =
711 (frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1)
712 ---------------------------------------------------------------------- *)
713
714Theorem RAT_LES_CALCULATE:
715 !f1 f2. (abs_rat f1 < abs_rat f2) =
716 (frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1)
717Proof
718 REPEAT GEN_TAC THEN
719 REWRITE_TAC[rat_les_def, rat_sgn_def, RAT_SUB_CALCULATE, RAT_SGN_CONG] THEN
720 REWRITE_TAC[frac_sgn_def, frac_sub_def, frac_add_def, frac_ainv_def] THEN
721 FRAC_POS_TAC
722 “frac_dnm f2 * frac_dnm (abs_frac (~frac_nmr f1,frac_dnm f1))” THEN
723 FRAC_NMRDNM_TAC THEN
724 REWRITE_TAC[INT_SGN_CLAUSES, int_gt] THEN
725 `~frac_nmr f1 * frac_dnm f2 = ~(frac_nmr f1 * frac_dnm f2)` by ARITH_TAC THEN
726 ASM_REWRITE_TAC[INT_LT_ADDNEG, INT_ADD_LID]
727QED
728
729Theorem RAT_LEQ_CALCULATE:
730 !f1 f2. (abs_rat f1 <= abs_rat f2) =
731 (frac_nmr f1 * frac_dnm f2 <= frac_nmr f2 * frac_dnm f1)
732Proof
733 REPEAT GEN_TAC THEN
734 REWRITE_TAC[rat_leq_def, RAT_LES_CALCULATE, INT_LE_LT, RAT_EQ_CALCULATE]
735QED
736
737Theorem RAT_OF_NUM_CALCULATE:
738 !n1. rat_of_num n1 = abs_rat( abs_frac( &n1, 1) )
739Proof
740 recInduct (DB.fetch "-" "rat_of_num_ind") THEN
741 RW_TAC arith_ss [rat_of_num_def, rat_0_def, frac_0_def, rat_1_def, frac_1_def,
742 RAT_ADD_CALCULATE, frac_add_def] THEN
743 FRAC_POS_TAC ``1i`` THEN
744 RW_TAC int_ss
745 [NMR, DNM, ARITH_PROVE “int_of_num (SUC n) + 1 = int_of_num (SUC (SUC n))”]
746QED
747
748Theorem RAT_OF_NUM_LEQ[simp]:
749 rat_of_num a <= rat_of_num b <=> a <= b
750Proof
751 SIMP_TAC std_ss [RAT_OF_NUM_CALCULATE, RAT_LEQ_CALCULATE,
752 NMR, DNM, INT_LT_01, INT_MUL_RID, INT_LE]
753QED
754
755Theorem RAT_OF_NUM_LES[simp]:
756 rat_of_num a < rat_of_num b <=> a < b
757Proof
758 SIMP_TAC std_ss [RAT_OF_NUM_CALCULATE, RAT_LES_CALCULATE,
759 NMR, DNM, INT_LT_01, INT_MUL_RID, INT_LT]
760QED
761
762(*--------------------------------------------------------------------------
763 * rat_calculate_table : (term * thm) list
764 *--------------------------------------------------------------------------*)
765
766val rat_calculate_table = [
767 ( ``rat_0``, rat_0_def ),
768 ( ``rat_1``, rat_1_def ),
769 ( ``rat_ainv``, RAT_AINV_CALCULATE ),
770 ( ``rat_minv``, RAT_MINV_CALCULATE ),
771 ( ``rat_add``, RAT_ADD_CALCULATE ),
772 ( ``rat_sub``, RAT_SUB_CALCULATE ),
773 ( ``rat_mul``, RAT_MUL_CALCULATE ),
774 ( ``rat_div``, RAT_DIV_CALCULATE )
775];
776
777(*--------------------------------------------------------------------------
778 * RAT_CALC_CONV : conv
779 *
780 * r1
781 * ---------------------
782 * |- r1 = abs_rat(f1)
783 *--------------------------------------------------------------------------*)
784
785fun RAT_CALC_CONV (t1:term) =
786let
787 val thm = REFL t1;
788 val (top_rator, top_rands) = strip_comb t1;
789 val calc_table_entry =
790 List.find (fn x => fst(x) ~~ top_rator) rat_calculate_table;
791in
792 (* do nothing if term is already in the form abs_rat(...) *)
793 if top_rator ~~ ``abs_rat`` then
794 thm
795 (* if it is a numeral, simply rewrite it *)
796 else if (top_rator ~~ ``rat_of_num``) then
797 SUBST [``x:rat`` |-> SPEC (rand t1) (RAT_OF_NUM_CALCULATE)] ``^t1 = x:rat`` thm
798 (* if there is an entry in the calculation table, calculate it *)
799 else if (isSome calc_table_entry) then
800 let
801 val arg_thms = map RAT_CALC_CONV top_rands;
802 val arg_fracs = map (fn x => rand(rhs(concl x))) arg_thms;
803 val arg_vars = map (fn x => genvar ``:rat``) arg_thms;
804
805 val subst_list = map (fn x => fst(x) |-> snd(x)) (ListPair.zip (arg_vars,arg_thms));
806 (* subst_term: t1 = top_rator arg_vars[1] ... arg_vars[n] *)
807 val subst_term = mk_eq (t1 , list_mk_comb (top_rator,arg_vars))
808
809 val thm1 = SUBST subst_list subst_term thm;
810 val (thm1_lhs, thm1_rhs) = dest_eq(concl thm1);
811 val thm1_lhs_var = genvar ``:rat``;
812
813 val calc_thm = snd (valOf( calc_table_entry ));
814 in
815 SUBST [thm1_lhs_var |-> UNDISCH_ALL (SPECL arg_fracs calc_thm)] ``^thm1_lhs = ^thm1_lhs_var`` thm1
816 end
817 (* otherwise: applying r = abs_rat(rep_rat r)) always works *)
818 else
819 SUBST [``x:rat`` |-> SPEC t1 (GSYM RAT)] ``^t1 = x:rat`` thm
820end;
821
822(*--------------------------------------------------------------------------
823 * RAT_CALCTERM_TAC : term -> tactic
824 *
825 * calculates the value of t1:rat
826 *--------------------------------------------------------------------------*)
827
828fun RAT_CALCTERM_TAC (t1:term) (asm_list,goal) =
829 let
830 val calc_thm = RAT_CALC_CONV t1;
831 val (calc_asms, calc_concl) = dest_thm calc_thm;
832 in
833 (
834 MAP_EVERY ASSUME_TAC (map (fn x => TAC_PROOF ((asm_list,x), RW_TAC intLib.int_ss [FRAC_DNMPOS,INT_MUL_POS_SIGN,INT_NOTPOS0_NEG,INT_NOT0_MUL,INT_GT0_IMP_NOT0,INT_ABS_NOT0POS])) calc_asms) THEN
835 SUBST_TAC[calc_thm]
836 ) (asm_list,goal)
837 end
838handle HOL_ERR _ => raise ERR "RAT_CALCTERM_TAC" "";
839
840
841(*--------------------------------------------------------------------------
842 * RAT_CALC_TAC : tactic
843 *
844 * calculates the value of all subterms (of type ``:rat``)
845 * assumptions that were needed for the simplification are added to the goal
846 *--------------------------------------------------------------------------*)
847
848fun RAT_CALC_TAC (asm_list,goal) =
849 let
850 (* extract terms of type ``:rat`` *)
851 val rat_terms = extract_rat goal;
852 (* build conversions *)
853 val calc_thms = map RAT_CALC_CONV rat_terms;
854 (* split list into assumptions and conclusions *)
855 val (calc_asmlists, calc_concl) = ListPair.unzip (map (fn x => dest_thm x) calc_thms);
856 (* merge assumptions lists *)
857 val calc_asms = op_U aconv calc_asmlists;
858 (* function to prove an assumption, TODO: fracLib benutzen *)
859 val gen_thm = (fn x => TAC_PROOF ((asm_list,x), RW_TAC intLib.int_ss [] ));
860 (* try to prove assumptions *)
861 val prove_list = List.map (total gen_thm) calc_asms;
862 (* combine assumptions and their proofs *)
863 val list1 = ListPair.zip (calc_asms,prove_list);
864 (* partition assumptions into proved assumptions and assumptions to be proved *)
865 val list2 = partition (fn x => isSome (snd x)) list1;
866 val asms_toprove = map fst (snd list2);
867 val asms_proved = map (fn x => valOf (snd x)) (fst list2);
868 (* generate new subgoal goal *)
869 val subst_goal = snd (dest_eq (snd (dest_thm (ONCE_REWRITE_CONV calc_thms goal))));
870 val subgoal = (list_mk_conj (asms_toprove @ [subst_goal]) );
871 val mp_thm = TAC_PROOF
872 (
873 (asm_list, mk_imp (subgoal,goal))
874 ,
875 STRIP_TAC THEN
876 MAP_EVERY ASSUME_TAC asms_proved THEN
877 ONCE_REWRITE_TAC calc_thms THEN
878 PROVE_TAC []
879 );
880 in
881 ( [(asm_list,subgoal)], fn (thms:thm list) => MP mp_thm (hd thms) )
882 end
883handle HOL_ERR _ => raise ERR "RAT_CALC_TAC" "";
884
885(*--------------------------------------------------------------------------
886 * RAT_CALCEQ_TAC : tactic
887 *--------------------------------------------------------------------------*)
888
889val RAT_CALCEQ_TAC =
890 RAT_CALC_TAC THEN
891 FRAC_CALC_TAC THEN
892 REWRITE_TAC[RAT_EQ] THEN
893 FRAC_NMRDNM_TAC THEN
894 INT_RING_TAC;
895
896
897(*==========================================================================
898 * numerator of rational number: sign reduction
899 *==========================================================================*)
900
901(*--------------------------------------------------------------------------
902 RAT_EQ0_NMR: thm
903 |- !r1. (r1 = 0q) = (rat_nmr r1 = 0)
904 *--------------------------------------------------------------------------*)
905
906Theorem RAT_EQ0_NMR: !r1. (r1 = 0q) = (rat_nmr r1 = 0)
907Proof
908 GEN_TAC THEN
909 REWRITE_TAC[rat_nmr_def] THEN
910 SUBST_TAC[SPEC ``r1:rat`` (GSYM RAT)] THEN
911 REWRITE_TAC[RAT_NMREQ0_CONG] THEN
912 REWRITE_TAC[rat_0, frac_0_def, RAT_ABS_EQUIV, rat_equiv_def] THEN
913 FRAC_POS_TAC ``1i`` THEN
914 FRAC_NMRDNM_TAC
915QED
916
917(*--------------------------------------------------------------------------
918 RAT_0LES_NMR: thm
919 |- !r1. (0q < r1) = (0 < rat_nmr r1)
920
921 RAT_0LES_NMR: thm
922 |- !r1. (r1 < 0q) = (rat_nmr r1 < 0i)
923 *--------------------------------------------------------------------------*)
924
925Theorem RAT_0LES_NMR:
926 !r1. rat_les 0q r1 <=> 0i < rat_nmr r1
927Proof
928 GEN_TAC THEN
929 REWRITE_TAC[rat_0, rat_nmr_def, rat_les_def, rat_sgn_def, frac_0_def,
930 frac_sgn_def, SGN_def] THEN
931 RAT_CALC_TAC THEN
932 FRAC_POS_TAC ``1i`` THEN
933 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
934 SUBST_TAC[FRAC_CALC_CONV ``frac_sub (rep_rat r1) (abs_frac (0,1))``] THEN
935 REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG,RAT_NMRGT0_CONG] THEN
936 FRAC_NMRDNM_TAC THEN
937 RW_TAC int_ss [RAT, FRAC, INT_SUB_RZERO] THEN
938 PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL]
939QED
940
941Theorem RAT_LES0_NMR: !r1. rat_les r1 0q <=> rat_nmr r1 < 0i
942Proof
943 GEN_TAC THEN
944 REWRITE_TAC[rat_0, rat_nmr_def, rat_les_def, rat_sgn_def, frac_0_def, frac_sgn_def, SGN_def] THEN
945 RAT_CALC_TAC THEN
946 FRAC_POS_TAC ``1i`` THEN
947 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
948 SUBST_TAC[FRAC_CALC_CONV ``frac_sub (abs_frac (0,1)) (rep_rat r1)``] THEN
949 REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG,RAT_NMRGT0_CONG] THEN
950 FRAC_NMRDNM_TAC THEN
951 RW_TAC int_ss [RAT, FRAC, INT_SUB_LZERO] THEN
952 PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL, INT_NEG_LT0, INT_NEG_EQ, INT_NEG_0]
953QED
954
955(*--------------------------------------------------------------------------
956 RAT_0LES_NMR: thm
957 |- !r1. (0q <= r1) = (0i <= rat_nmr r1)
958
959 RAT_0LES_NMR: thm
960 |- !r1. (r1 <= 0q) = (rat_nmr r1 <= 0i)
961 *--------------------------------------------------------------------------*)
962
963Theorem RAT_0LEQ_NMR:
964 !r1. rat_leq 0q r1 <=> 0i <= rat_nmr r1
965Proof
966 GEN_TAC THEN
967 REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN
968 PROVE_TAC[RAT_0LES_NMR, RAT_EQ0_NMR, rat_nmr_def]
969QED
970
971Theorem RAT_LEQ0_NMR:
972 !r1. rat_leq r1 0q <=> rat_nmr r1 <= 0i
973Proof
974 GEN_TAC THEN
975 REWRITE_TAC[rat_leq_def, INT_LE_LT] THEN
976 PROVE_TAC[RAT_LES0_NMR, RAT_EQ0_NMR, rat_nmr_def]
977QED
978
979(*==========================================================================
980 * field properties
981 *==========================================================================*)
982
983(*--------------------------------------------------------------------------
984 RAT_ADD_ASSOC: thm
985 |- !a b c. rat_add a (rat_add b c) = rat_add (rat_add a b) c
986
987 RAT_MUL_ASSOC: thm
988 |- !a b c. rat_mul a (rat_mul b c) = rat_mul (rat_mul a b) c
989 *--------------------------------------------------------------------------*)
990
991Theorem RAT_ADD_ASSOC: !a b c. rat_add a (rat_add b c) = rat_add (rat_add a b) c
992Proof
993 REWRITE_TAC[rat_add_def] THEN
994 REWRITE_TAC[RAT_ADD_CONG] THEN
995 REWRITE_TAC[FRAC_ADD_ASSOC]
996QED
997
998Theorem RAT_MUL_ASSOC: !a b c. rat_mul a (rat_mul b c) = rat_mul (rat_mul a b) c
999Proof
1000 REWRITE_TAC[rat_mul_def] THEN
1001 REWRITE_TAC[RAT_MUL_CONG] THEN
1002 REWRITE_TAC[FRAC_MUL_ASSOC]
1003QED
1004
1005(*--------------------------------------------------------------------------
1006 RAT_ADD_COMM: thm
1007 |- !a b. rat_add a b = rat_add b a
1008
1009 RAT_MUL_COMM: thm
1010 |- !a b. rat_mul a b = rat_mul b a
1011 *--------------------------------------------------------------------------*)
1012
1013Theorem RAT_ADD_COMM: !a b. rat_add a b = rat_add b a
1014Proof
1015 REPEAT GEN_TAC THEN
1016 REWRITE_TAC[rat_add_def] THEN
1017 AP_TERM_TAC THEN
1018 MATCH_ACCEPT_TAC FRAC_ADD_COMM
1019QED
1020
1021Theorem RAT_MUL_COMM: !a b. rat_mul a b = rat_mul b a
1022Proof
1023 REPEAT GEN_TAC THEN
1024 REWRITE_TAC[rat_mul_def] THEN
1025 AP_TERM_TAC THEN
1026 MATCH_ACCEPT_TAC FRAC_MUL_COMM
1027QED
1028
1029(*--------------------------------------------------------------------------
1030 RAT_ADD_RID: thm
1031 |- !a. rat_add a 0q = a
1032
1033 RAT_ADD_LID: thm
1034 |- !a. rat_add 0q a = a
1035
1036 RAT_MUL_RID: thm
1037 |- !a. rat_mul a 1q = a
1038
1039 RAT_MUL_LID: thm
1040 |- !a. rat_mul 1q a = a
1041 *--------------------------------------------------------------------------*)
1042
1043Theorem RAT_ADD_RID[simp]: !a. rat_add a 0q = a
1044Proof
1045 REWRITE_TAC[rat_add_def,rat_0] THEN
1046 REWRITE_TAC[RAT_ADD_CONG] THEN
1047 REWRITE_TAC[FRAC_ADD_RID] THEN
1048 REWRITE_TAC[CONJUNCT1 rat_thm]
1049QED
1050
1051Theorem RAT_ADD_LID[simp]: !a. rat_add 0q a = a
1052Proof
1053 ONCE_REWRITE_TAC[RAT_ADD_COMM] THEN
1054 REWRITE_TAC[RAT_ADD_RID]
1055QED
1056
1057Theorem RAT_MUL_RID[simp]: !a. rat_mul a 1q = a
1058Proof
1059 REWRITE_TAC[rat_mul_def,rat_1] THEN
1060 REWRITE_TAC[RAT_MUL_CONG] THEN
1061 REWRITE_TAC[FRAC_MUL_RID] THEN
1062 REWRITE_TAC[CONJUNCT1 rat_thm]
1063QED
1064
1065Theorem RAT_MUL_LID[simp]: !a. rat_mul 1q a = a
1066Proof
1067 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN
1068 REWRITE_TAC[RAT_MUL_RID]
1069QED
1070
1071(*--------------------------------------------------------------------------
1072 RAT_ADD_RINV: thm
1073 |- !a. rat_add a (rat_ainv a) = 0q
1074
1075 RAT_ADD_LINV: thm
1076 |- !a. rat_add (rat_ainv a) a = 0q
1077
1078 RAT_MUL_RINV: thm
1079 |- !a. ~(a=0q) ==> (rat_mul a (rat_minv a) = 1q)
1080
1081 RAT_MUL_LINV: thm
1082 |- !a. ~(a = 0q) ==> (rat_mul (rat_minv a) a = 1q)
1083 *--------------------------------------------------------------------------*)
1084
1085Theorem RAT_ADD_RINV:
1086 !a. rat_add a (rat_ainv a) = 0q
1087Proof
1088 GEN_TAC THEN
1089 REWRITE_TAC[rat_add_def,rat_ainv_def,rat_0,RAT_ADD_CONG] THEN
1090 REWRITE_TAC[frac_add_def,frac_ainv_def,frac_0_def] THEN
1091 SIMP_TAC bool_ss [NMR, DNM, FRAC_DNMPOS] THEN
1092 REWRITE_TAC[RAT_ABS_EQUIV,rat_equiv_def] THEN
1093 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
1094 simp[INT_MUL_POS_SIGN, FRAC_DNMPOS] THEN
1095 REWRITE_TAC [INT_MUL_LZERO, INT_MUL_RID, INT_LT_01,
1096 GSYM INT_NEG_LMUL, INT_ADD_RINV]
1097QED
1098
1099Theorem RAT_ADD_LINV:
1100 !a. rat_add (rat_ainv a) a = 0q
1101Proof
1102 ONCE_REWRITE_TAC[RAT_ADD_COMM] THEN
1103 REWRITE_TAC[RAT_ADD_RINV]
1104QED
1105
1106Theorem RAT_MUL_RINV:
1107 !a. ~(a=0q) ==> (rat_mul a (rat_minv a) = 1q)
1108Proof
1109 REPEAT STRIP_TAC THEN
1110 REWRITE_TAC[rat_mul_def, rat_minv_def, rat_1, RAT_MUL_CONG] THEN
1111 REWRITE_TAC[frac_mul_def, frac_minv_def, frac_1_def] THEN
1112 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN
1113 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
1114 TRY (irule INT_MUL_POS_SIGN >> conj_tac) THEN
1115 TRY (irule FRAC_DNMPOS) THEN
1116 TRY (irule INT_LT_01) THEN
1117 TRY (irule INT_ABS_NOT0POS) THEN
1118 ASM_REWRITE_TAC [GSYM RAT_EQ0_NMR, GSYM rat_nmr_def] THEN
1119 REWRITE_TAC[INT_MUL_LID, INT_MUL_RID, frac_sgn_def,
1120 ABS_EQ_MUL_SGN, rat_nmr_def] THEN
1121 CONV_TAC (AC_CONV (INT_MUL_ASSOC, INT_MUL_COMM))
1122QED
1123
1124Theorem RAT_MUL_LINV:
1125 !a. ~(a = 0q) ==> (rat_mul (rat_minv a) a = 1q)
1126Proof
1127 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN
1128 RW_TAC int_ss[RAT_MUL_RINV]
1129QED
1130
1131(*--------------------------------------------------------------------------
1132 RAT_RDISTRIB: thm
1133 |- !a b c. rat_mul (rat_add a b) c = rat_add (rat_mul a c) (rat_mul b c)
1134
1135 RAT_LDISTRIB: thm
1136 |- !a b c. rat_mul c (rat_add a b) = rat_add (rat_mul c a) (rat_mul c b)
1137 *--------------------------------------------------------------------------*)
1138
1139Theorem RAT_RDISTRIB:
1140 !a b c. rat_mul (rat_add a b) c = rat_add (rat_mul a c) (rat_mul b c)
1141Proof
1142 REPEAT GEN_TAC THEN
1143 REWRITE_TAC[rat_mul_def,rat_add_def] THEN
1144 REWRITE_TAC[RAT_MUL_CONG, RAT_ADD_CONG] THEN
1145 REWRITE_TAC[frac_mul_def,frac_add_def] THEN
1146 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
1147 simp[INT_MUL_POS_SIGN, FRAC_DNMPOS] THEN
1148 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN
1149 VALIDATE (CONV_TAC (feqconv NMR THENC feqconv DNM)) THEN
1150 simp[INT_MUL_POS_SIGN, FRAC_DNMPOS] THEN
1151 REWRITE_TAC[INT_RDISTRIB] THEN BINOP_TAC THEN
1152 CONV_TAC (AC_CONV (INT_MUL_ASSOC, INT_MUL_COMM))
1153QED
1154
1155Theorem RAT_LDISTRIB:
1156 !a b c. rat_mul c (rat_add a b) = rat_add (rat_mul c a) (rat_mul c b)
1157Proof
1158 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN
1159 REWRITE_TAC[RAT_RDISTRIB]
1160QED
1161
1162(*--------------------------------------------------------------------------
1163 RAT_1_NOT_0: thm
1164 |- ~ (1q=0q)
1165 *--------------------------------------------------------------------------*)
1166
1167Theorem RAT_1_NOT_0: ~ (1q=0q)
1168Proof
1169 REWRITE_TAC[rat_0, rat_1] THEN
1170 REWRITE_TAC[frac_1_def, frac_0_def] THEN
1171 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN
1172 FRAC_POS_TAC ``1i`` THEN
1173 RW_TAC int_ss[NMR,DNM]
1174QED
1175
1176(*==========================================================================
1177 * arithmetic rules
1178 *==========================================================================*)
1179
1180(*--------------------------------------------------------------------------
1181 RAT_MUL_LZERO: thm
1182 |- !r1. rat_mul 0q r1 = 0q
1183
1184 RAT_MUL_RZERO: thm
1185 |- !r1. rat_mul r1 0q = 0q
1186 *--------------------------------------------------------------------------*)
1187
1188Theorem RAT_MUL_LZERO[simp]: !r1. rat_mul 0q r1 = 0q
1189Proof
1190 GEN_TAC THEN RAT_CALCEQ_TAC
1191QED
1192
1193Theorem RAT_MUL_RZERO[simp]:
1194 !r1. rat_mul r1 0q = 0q
1195Proof
1196 PROVE_TAC[RAT_MUL_LZERO, RAT_MUL_COMM]
1197QED
1198
1199(*--------------------------------------------------------------------------
1200 RAT_SUB_ADDAINV: thm
1201 |- !r1 r2. rat_sub r1 r2 = rat_add r1 (rat_ainv r2)
1202
1203 RAT_DIV_MULMINV: thm
1204 |- !r1 r2. rat_div r1 r2 = rat_mul r1 (rat_minv r2)
1205 *--------------------------------------------------------------------------*)
1206
1207Theorem RAT_SUB_ADDAINV: !r1 r2. rat_sub r1 r2 = rat_add r1 (rat_ainv r2)
1208Proof
1209 REPEAT GEN_TAC THEN
1210 REWRITE_TAC[rat_sub_def, rat_add_def, rat_ainv_def] THEN
1211 REWRITE_TAC[frac_sub_def] THEN
1212 REWRITE_TAC[RAT_ADD_CONG]
1213QED
1214
1215Theorem RAT_DIV_MULMINV:
1216 !r1 r2. rat_div r1 r2 = rat_mul r1 (rat_minv r2)
1217Proof
1218 REPEAT GEN_TAC THEN
1219 REWRITE_TAC[rat_div_def, rat_mul_def, rat_minv_def] THEN
1220 REWRITE_TAC[frac_div_def] THEN
1221 REWRITE_TAC[RAT_MUL_CONG]
1222QED
1223
1224Theorem RAT_DIV_0[simp]:
1225 rat_div 0 x = 0
1226Proof
1227 simp[RAT_DIV_MULMINV]
1228QED
1229
1230
1231(*--------------------------------------------------------------------------
1232 RAT_AINV_0: thm
1233 |- rat_ainv 0q = 0q
1234
1235 RAT_AINV_AINV: thm
1236 |- !r1. rat_ainv (rat_ainv r1) = r1
1237
1238 RAT_AINV_ADD: thm
1239 |- ! r1 r2. rat_ainv (rat_add r1 r2) = rat_add (rat_ainv r1) (rat_ainv r2)
1240
1241 RAT_AINV_SUB: thm
1242 |- ! r1 r2. rat_ainv (rat_sub r1 r2) = rat_sub r2 r1
1243
1244 RAT_AINV_RMUL: thm
1245 |- !r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul r1 (rat_ainv r2)
1246
1247 RAT_AINV_LMUL: thm
1248 |- !r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul (rat_ainv r1) r2
1249
1250 RAT_AINV_MINV: thm
1251 |- !r1. ~(r1=0q) ==> (rat_ainv (rat_minv r1) = rat_minv (rat_ainv r1))
1252 *--------------------------------------------------------------------------*)
1253
1254Theorem RAT_AINV_0[simp]: rat_ainv 0q = 0q
1255Proof
1256 REWRITE_TAC[rat_0,rat_ainv_def] THEN
1257 RW_TAC int_ss[RAT_AINV_CONG] THEN
1258 RW_TAC int_ss[FRAC_AINV_0]
1259QED
1260
1261Theorem RAT_AINV_AINV[simp]:
1262 !r1. rat_ainv (rat_ainv r1) = r1
1263Proof
1264 GEN_TAC THEN
1265 REWRITE_TAC[rat_ainv_def] THEN
1266 RW_TAC int_ss[RAT_AINV_CONG, FRAC_AINV_AINV, rat_thm]
1267QED
1268
1269Theorem RAT_AINV_ADD: ! r1 r2. rat_ainv (rat_add r1 r2) = rat_add (rat_ainv r1) (rat_ainv r2)
1270Proof
1271 REPEAT GEN_TAC THEN
1272 REWRITE_TAC[rat_add_def,rat_ainv_def] THEN
1273 REWRITE_TAC[RAT_ADD_CONG, RAT_AINV_CONG] THEN
1274 RW_TAC int_ss[FRAC_AINV_ADD]
1275QED
1276
1277Theorem RAT_AINV_SUB: ! r1 r2. rat_ainv (rat_sub r1 r2) = rat_sub r2 r1
1278Proof
1279 REPEAT GEN_TAC THEN
1280 REWRITE_TAC[RAT_SUB_ADDAINV] THEN
1281 REWRITE_TAC[RAT_AINV_ADD] THEN
1282 REWRITE_TAC[RAT_AINV_AINV] THEN
1283 PROVE_TAC[RAT_ADD_COMM]
1284QED
1285
1286Theorem RAT_AINV_RMUL: !r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul r1 (rat_ainv r2)
1287Proof
1288 REPEAT GEN_TAC THEN
1289 REWRITE_TAC[rat_ainv_def, rat_mul_def] THEN
1290 REWRITE_TAC[RAT_MUL_CONG, RAT_AINV_CONG] THEN
1291 PROVE_TAC[FRAC_AINV_RMUL]
1292QED
1293
1294Theorem RAT_AINV_LMUL: !r1 r2. rat_ainv (rat_mul r1 r2) = rat_mul (rat_ainv r1) r2
1295Proof
1296 REPEAT GEN_TAC THEN
1297 REWRITE_TAC[rat_ainv_def, rat_mul_def] THEN
1298 REWRITE_TAC[RAT_MUL_CONG, RAT_AINV_CONG] THEN
1299 PROVE_TAC[FRAC_AINV_LMUL]
1300QED
1301
1302(*--------------------------------------------------------------------------
1303 RAT_EQ_AINV
1304 |- !r1 r2. (~r1 = ~r2) = (r1=r2)
1305
1306 RAT_AINV_EQ
1307 |- !r1 r2. (~r1 = r2) = (r1 = ~r2)
1308 *--------------------------------------------------------------------------*)
1309
1310Theorem RAT_AINV_EQ:
1311 !r1 r2. (rat_ainv r1 = r2) = (r1 = rat_ainv r2)
1312Proof
1313 REPEAT GEN_TAC THEN
1314 EQ_TAC THEN
1315 STRIP_TAC THEN
1316 BasicProvers.VAR_EQ_TAC THEN
1317 REWRITE_TAC[RAT_AINV_AINV]
1318QED
1319
1320Theorem RAT_EQ_AINV[simp]:
1321 !r1 r2. (rat_ainv r1 = rat_ainv r2) = (r1=r2)
1322Proof
1323 REWRITE_TAC[RAT_AINV_EQ, RAT_AINV_AINV]
1324QED
1325
1326Theorem RAT_AINV_MINV:
1327 !r1. r1 <> 0q ==> (rat_ainv (rat_minv r1) = rat_minv (rat_ainv r1))
1328Proof
1329 REPEAT STRIP_TAC THEN
1330 FIRST_ASSUM MP_TAC THEN
1331 RULE_ASSUM_TAC (REWRITE_RULE[rat_nmr_def, RAT_EQ0_NMR]) THEN
1332 SUBST_TAC[GSYM RAT_AINV_0] THEN
1333 ONCE_REWRITE_TAC[GSYM RAT_AINV_EQ] THEN
1334 REWRITE_TAC[rat_nmr_def, RAT_EQ0_NMR] THEN
1335 REWRITE_TAC[rat_ainv_def, rat_minv_def] THEN
1336 REWRITE_TAC[RAT_NMREQ0_CONG] THEN
1337 STRIP_TAC THEN
1338 RW_TAC int_ss[RAT_AINV_CONG, RAT_MINV_CONG] THEN
1339 LAST_ASSUM MP_TAC THEN
1340 ONCE_REWRITE_TAC[GSYM INT_EQ_NEG] THEN
1341 ONCE_REWRITE_TAC[INT_NEG_0] THEN
1342 STRIP_TAC THEN
1343 FRAC_CALC_TAC THEN
1344 REWRITE_TAC[RAT_EQ] THEN
1345 FRAC_NMRDNM_TAC THEN
1346 RW_TAC int_ss[INT_ABS, SGN_def] THEN
1347 TRY (INT_RING_TAC THEN NO_TAC) THEN
1348 METIS_TAC[integerTheory.INT_LT_REFL, integerTheory.INT_LT_TRANS,
1349 integerTheory.INT_NOT_LT, integerTheory.INT_LE_ANTISYM,
1350 integerTheory.INT_MUL_RZERO]
1351QED
1352
1353(*--------------------------------------------------------------------------
1354 RAT_SUB_RDISTRIB: thm
1355 |- !a b c. rat_mul (rat_sub a b) c = rat_sub (rat_mul a c) (rat_mul b c)
1356
1357 RAT_SUB_LDISTRIB: thm
1358 |- !a b c. rat_mul c (rat_sub a b) = rat_sub (rat_mul c a) (rat_mul c b)
1359 *--------------------------------------------------------------------------*)
1360
1361Theorem RAT_SUB_RDISTRIB: !a b c. rat_mul (rat_sub a b) c = rat_sub (rat_mul a c) (rat_mul b c)
1362Proof
1363 REPEAT GEN_TAC THEN
1364 REWRITE_TAC[RAT_SUB_ADDAINV] THEN
1365 REWRITE_TAC[RAT_AINV_LMUL] THEN
1366 PROVE_TAC[RAT_RDISTRIB]
1367QED
1368
1369Theorem RAT_SUB_LDISTRIB: !a b c. rat_mul c (rat_sub a b) = rat_sub (rat_mul c a) (rat_mul c b)
1370Proof
1371 REPEAT GEN_TAC THEN
1372 REWRITE_TAC[RAT_SUB_ADDAINV] THEN
1373 REWRITE_TAC[RAT_AINV_RMUL] THEN
1374 PROVE_TAC[RAT_LDISTRIB]
1375QED
1376
1377(*--------------------------------------------------------------------------
1378 RAT_SUB_LID: thm
1379 |- !r1. rat_sub 0q r1 = rat_ainv r1
1380
1381 RAT_SUB_RID: thm
1382 |- !r1. rat_sub r1 0q = r1
1383 *--------------------------------------------------------------------------*)
1384
1385Theorem RAT_SUB_LID[simp]:
1386 !r1. rat_sub 0q r1 = rat_ainv r1
1387Proof
1388 GEN_TAC THEN
1389 REWRITE_TAC[RAT_SUB_ADDAINV] THEN
1390 REWRITE_TAC[RAT_ADD_LID]
1391QED
1392
1393Theorem RAT_SUB_RID[simp]:
1394 !r1. rat_sub r1 0q = r1
1395Proof
1396 GEN_TAC THEN
1397 REWRITE_TAC[RAT_SUB_ADDAINV] THEN
1398 REWRITE_TAC[RAT_AINV_0] THEN
1399 RW_TAC int_ss[RAT_ADD_RID]
1400QED
1401
1402(*--------------------------------------------------------------------------
1403 RAT_SUB_ID: thm
1404 |- ! r. r - r = 0q
1405 *--------------------------------------------------------------------------*)
1406
1407Theorem RAT_SUB_ID[simp]:
1408 ! r. rat_sub r r = 0q
1409Proof
1410 RW_TAC bool_ss [RAT_SUB_ADDAINV, RAT_ADD_RINV]
1411QED
1412
1413(*--------------------------------------------------------------------------
1414 RAT_EQ_SUB0: thm
1415 |- !r1 r2. (rat_sub r1 r2 = 0q) = (r1 = r2)
1416 *--------------------------------------------------------------------------*)
1417
1418Theorem RAT_EQ_SUB0: !r1 r2. (rat_sub r1 r2 = 0q) = (r1 = r2)
1419Proof
1420 REPEAT GEN_TAC THEN
1421 SUBST_TAC[SPEC ``r1:rat`` (GSYM RAT), SPEC ``r2:rat`` (GSYM RAT)] THEN
1422 REWRITE_TAC[RAT_SUB_CALCULATE, rat_0] THEN
1423 FRAC_CALC_TAC THEN
1424 REWRITE_TAC[RAT_ABS_EQUIV, rat_equiv_def] THEN
1425 FRAC_NMRDNM_TAC THEN
1426 RW_TAC int_ss[INT_MUL_CALCULATE, GSYM INT_SUB_CALCULATE, INT_SUB_0, INT_MUL_RID, INT_MUL_LZERO]
1427QED
1428
1429(*--------------------------------------------------------------------------
1430 RAT_EQ_0SUB: thm
1431 |- !r1 r2. (0q = rat_sub r1 r2) = (r1 = r2)
1432 *--------------------------------------------------------------------------*)
1433
1434Theorem RAT_EQ_0SUB: !r1 r2. (0q = rat_sub r1 r2) = (r1 = r2)
1435Proof
1436 PROVE_TAC[RAT_EQ_SUB0]
1437QED
1438
1439(*--------------------------------------------------------------------------
1440 * signum function
1441 *--------------------------------------------------------------------------*)
1442
1443(*--------------------------------------------------------------------------
1444 * RAT_SGN_CALCULATE: thm
1445 * |- rat_sgn (abs_rat( f1 ) = frac_sgn f1
1446 *--------------------------------------------------------------------------*)
1447
1448Theorem RAT_SGN_CALCULATE: rat_sgn (abs_rat( f1 )) = frac_sgn f1
1449Proof
1450 REWRITE_TAC[rat_sgn_def, rat_0] THEN
1451 REWRITE_TAC[RAT_SGN_CONG] THEN
1452 REWRITE_TAC[frac_sgn_def, frac_0_def] THEN
1453 FRAC_NMRDNM_TAC THEN
1454 REWRITE_TAC[SGN_def]
1455QED
1456
1457(*--------------------------------------------------------------------------
1458 RAT_SGN_CLAUSES: thm
1459 |- !r1.
1460 ((rat_sgn r1 = ~1) = (r1 < 0q)) /\
1461 ((rat_sgn r1 = 0i) = (r1 = 0q) ) /\
1462 ((rat_sgn r1 = 1i) = (r1 > 0q))
1463 *--------------------------------------------------------------------------*)
1464
1465Theorem RAT_SGN_CLAUSES:
1466 !r1. ((rat_sgn r1 = ~1) = (rat_les r1 0q)) /\
1467 ((rat_sgn r1 = 0i) = (r1 = 0q)) /\
1468 ((rat_sgn r1 = 1i) = (rat_gre r1 0q))
1469Proof
1470 GEN_TAC THEN
1471 REWRITE_TAC[rat_sgn_def, rat_les_def, rat_gre_def] THEN
1472 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_ADD_LID, RAT_SUB_RID] THEN
1473 RAT_CALC_TAC THEN
1474 REWRITE_TAC[RAT_SGN_CONG] THEN
1475 REPEAT CONJ_TAC THENL
1476 [
1477 EQ_TAC THEN
1478 STRIP_TAC THEN
1479 PROVE_TAC[FRAC_SGN_AINV, INT_NEG_EQ]
1480 ,
1481 REWRITE_TAC[frac_sgn_def, frac_0_def] THEN
1482 REWRITE_TAC[RAT_EQ] THEN
1483 FRAC_NMRDNM_TAC THEN
1484 PROVE_TAC[INT_SGN_CLAUSES]
1485 ]
1486QED
1487
1488(*--------------------------------------------------------------------------
1489 RAT_SGN_0: thm
1490 |- rat_sgn 0q = 0i
1491 *--------------------------------------------------------------------------*)
1492
1493Theorem RAT_SGN_0[simp]:
1494 rat_sgn 0q = 0i
1495Proof
1496 REWRITE_TAC[rat_sgn_def, rat_0] THEN REWRITE_TAC[RAT_SGN_CONG] THEN
1497 REWRITE_TAC[frac_sgn_def, frac_0_def] THEN
1498 FRAC_NMRDNM_TAC THEN REWRITE_TAC[SGN_def]
1499QED
1500
1501(*--------------------------------------------------------------------------
1502 RAT_SGN_AINV: thm
1503 |- !r1. ~rat_sgn ~r1 = rat_sgn r1
1504 *--------------------------------------------------------------------------*)
1505
1506Theorem RAT_SGN_AINV: !r1. ~rat_sgn (rat_ainv r1) = rat_sgn r1
1507Proof
1508 GEN_TAC THEN
1509 REWRITE_TAC[rat_sgn_def, rat_ainv_def] THEN
1510 REWRITE_TAC[RAT_SGN_CONG] THEN
1511 PROVE_TAC[FRAC_SGN_AINV]
1512QED
1513
1514(*--------------------------------------------------------------------------
1515 RAT_SGN_MUL: thm
1516 |- !r1 r2. rat_sgn (r1 * r2) = rat_sgn r1 * rat_sgn r2
1517 *--------------------------------------------------------------------------*)
1518
1519Theorem RAT_SGN_MUL[simp]:
1520 !r1 r2. rat_sgn (rat_mul r1 r2) = rat_sgn r1 * rat_sgn r2
1521Proof
1522 REPEAT GEN_TAC THEN REWRITE_TAC[rat_sgn_def, rat_mul_def] THEN
1523 REWRITE_TAC[RAT_SGN_CONG] THEN PROVE_TAC[FRAC_SGN_MUL2]
1524QED
1525
1526Theorem RAT_SGN_MINV[simp]:
1527 !r1:rat. r1 <> 0 ==> (rat_sgn (rat_minv r1) = rat_sgn r1)
1528Proof
1529 GEN_TAC THEN STRIP_TAC THEN
1530 REWRITE_TAC[rat_sgn_def, rat_minv_def] THEN
1531 MATCH_MP_TAC (SPEC ``rep_rat r1`` FRAC_SGN_CASES) THEN
1532 REPEAT CONJ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1533 UNDISCH_ALL_TAC THEN REWRITE_TAC[RAT_EQ0_NMR, rat_nmr_def] THEN STRIP_TAC THEN
1534 REWRITE_TAC[frac_sgn_def, frac_minv_def, INT_SGN_CLAUSES] THEN
1535 STRIP_TAC THEN
1536 REWRITE_TAC[RAT_NMREQ0_CONG, RAT_NMRGT0_CONG, RAT_NMRLT0_CONG] THEN
1537 FRAC_NMRDNM_TAC THEN
1538 RW_TAC int_ss
1539 [INT_MUL_SIGN_CASES, SGN_def, FRAC_DNMPOS, INT_MUL_LID, int_gt] THEN
1540 PROVE_TAC[INT_LT_ANTISYM, int_gt]
1541QED
1542
1543(*--------------------------------------------------------------------------
1544 RAT_SGN_TOTAL
1545 |- !r1. (rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i)
1546 *--------------------------------------------------------------------------*)
1547
1548Theorem RAT_SGN_TOTAL:
1549 !r1. (rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i)
1550Proof
1551 REWRITE_TAC[rat_sgn_def] THEN
1552 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
1553 PROVE_TAC[]
1554QED
1555
1556(*--------------------------------------------------------------------------
1557 RAT_SGN_COMPLEMENT
1558 |- !r1.
1559 (~(rat_sgn r1 = ~1) = ((rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i))) /\
1560 (~(rat_sgn r1 = 0) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 1i))) /\
1561 (~(rat_sgn r1 = 1) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0)))
1562 *--------------------------------------------------------------------------*)
1563
1564Theorem RAT_SGN_COMPLEMENT:
1565 !r1. (~(rat_sgn r1 = ~1) = ((rat_sgn r1 = 0) \/ (rat_sgn r1 = 1i))) /\
1566 (~(rat_sgn r1 = 0) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 1i))) /\
1567 (~(rat_sgn r1 = 1) = ((rat_sgn r1 = ~1) \/ (rat_sgn r1 = 0)))
1568Proof
1569 GEN_TAC THEN REPEAT CONJ_TAC THEN
1570 ASSUME_TAC (SPEC ``r1:rat`` RAT_SGN_TOTAL) THEN
1571 UNDISCH_ALL_TAC THEN STRIP_TAC THEN
1572 RW_TAC int_ss [RAT_1_NOT_0]
1573QED
1574
1575(*==========================================================================
1576 * order of the rational numbers (less, greater, ...)
1577 *==========================================================================*)
1578
1579(*--------------------------------------------------------------------------
1580 RAT_LES_REF, RAT_LES_ANTISYM, RAT_LES_TRANS, RAT_LES_TOTAL
1581
1582 |- !r1. ~(r1 < r1)
1583 |- ! r1 r2. r1 < r2 ==> ~(r2 < r1)
1584 |- !r1 r2 r3. r1 < r2 /\ r2 < r3 ==> r1 < r3
1585 |- !r1 r2. r1 < r2 \/ (r1 = r2) \/ r2 < r1
1586 *--------------------------------------------------------------------------*)
1587
1588Theorem RAT_LES_REF: !r1. ~(rat_les r1 r1)
1589Proof
1590 REWRITE_TAC[rat_les_def] THEN
1591 REWRITE_TAC[RAT_SUB_ID] THEN
1592 RW_TAC int_ss[RAT_SGN_0]
1593QED
1594
1595Theorem lemmaX[local]:
1596 !f. frac_sgn (frac_ainv f) = ~frac_sgn f
1597Proof
1598 REWRITE_TAC[GSYM INT_NEG_EQ] THEN
1599 RW_TAC int_ss[FRAC_SGN_NEG]
1600QED
1601
1602Theorem RAT_LES_ANTISYM:
1603 !r1 r2. rat_les r1 r2 ==> ~(rat_les r2 r1)
1604Proof
1605 REPEAT GEN_TAC THEN
1606 REWRITE_TAC[rat_les_def, rat_sgn_def, rat_sub_def] THEN
1607 REWRITE_TAC[RAT_SGN_CONG] THEN
1608 SUBST_TAC[SPECL [``rep_rat r1``, ``rep_rat r2``] (GSYM FRAC_AINV_SUB)] THEN
1609 REWRITE_TAC[lemmaX] THEN REWRITE_TAC[INT_NEG_EQ] THEN RW_TAC int_ss[]
1610QED
1611
1612Theorem RAT_LES_TRANS:
1613 !r1 r2 r3. rat_les r1 r2 /\ rat_les r2 r3 ==> rat_les r1 r3
1614Proof
1615 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def] THEN
1616 SUBGOAL_THEN
1617 ``rat_sub r3 r1 = rat_add (rat_sub r3 r2) (rat_sub r2 r1)``
1618 SUBST1_TAC THEN1
1619 RAT_CALCEQ_TAC THEN REWRITE_TAC[rat_sgn_def, rat_sub_def, rat_add_def] THEN
1620 REWRITE_TAC[RAT_ADD_CONG, RAT_SUB_CONG] THEN
1621 REWRITE_TAC[RAT_SGN_CONG] THEN REWRITE_TAC[frac_sgn_def] THEN
1622 FRAC_CALC_TAC THEN FRAC_NMRDNM_TAC THEN
1623 REWRITE_TAC[INT_SGN_CLAUSES] THEN REWRITE_TAC[int_gt] THEN
1624 FRAC_POS_TAC ``frac_dnm (rep_rat r2) * frac_dnm (rep_rat r1)`` THEN
1625 FRAC_POS_TAC ``frac_dnm (rep_rat r3) * frac_dnm (rep_rat r2)`` THEN
1626 REPEAT STRIP_TAC THEN
1627 PROVE_TAC[INT_LT_ADD,INT_MUL_POS_SIGN]
1628QED
1629
1630Theorem RAT_LES_TOTAL:
1631 !r1 r2. rat_les r1 r2 \/ (r1 = r2) \/ rat_les r2 r1
1632Proof
1633 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def] THEN
1634 SUBST_TAC[SPECL[``r1:rat``,``r2:rat``] (GSYM RAT_AINV_SUB)] THEN
1635 SUBST_TAC[
1636 SPECL[``rat_sgn (rat_ainv (rat_sub r1 r2))``,``1i``] (GSYM INT_EQ_NEG)] THEN
1637 REWRITE_TAC[RAT_SGN_AINV] THEN
1638 ONCE_REWRITE_TAC[GSYM RAT_EQ_SUB0] THEN
1639 SUBST_TAC[
1640 CONJUNCT1 (CONJUNCT2 (SPEC ``rat_sub r1 r2`` (GSYM RAT_SGN_CLAUSES)))] THEN
1641 PROVE_TAC[RAT_SGN_TOTAL]
1642QED
1643
1644
1645(*--------------------------------------------------------------------------
1646 RAT_LEQ_REF, RAT_LEQ_ANTISYM, RAT_LEQ_TRANS
1647 |- !r1. r1 <= r1
1648 |- !r1 r2. r1 <= r2 = r2 >= r1
1649 |- !r1 r2 r3. r1 <= r2 /\ r2 <= r3 ==> r1 <= r3
1650 *--------------------------------------------------------------------------*)
1651
1652Theorem RAT_LEQ_REF: !r1. rat_leq r1 r1
1653Proof
1654 GEN_TAC THEN
1655 REWRITE_TAC[rat_leq_def] THEN
1656 REWRITE_TAC[RAT_SUB_ID] THEN
1657 REWRITE_TAC[rat_sgn_def,rat_0] THEN
1658 REWRITE_TAC[frac_sgn_def,SGN_def, frac_0_def] THEN
1659 REWRITE_TAC[RAT_NMREQ0_CONG,RAT_NMRLT0_CONG] THEN
1660 RW_TAC int_ss[NMR,DNM]
1661QED
1662
1663Theorem RAT_LEQ_ANTISYM:
1664 !r1 r2. rat_leq r1 r2 /\ rat_leq r2 r1 ==> (r1=r2)
1665Proof
1666 REPEAT GEN_TAC THEN
1667 REWRITE_TAC[rat_leq_def] THEN
1668 RW_TAC bool_ss [] THEN
1669 PROVE_TAC[RAT_LES_ANTISYM]
1670QED
1671
1672Theorem RAT_LEQ_TRANS:
1673 !r1 r2 r3. rat_leq r1 r2 /\ rat_leq r2 r3 ==> rat_leq r1 r3
1674Proof
1675 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN
1676 RW_TAC bool_ss [] THEN PROVE_TAC[RAT_LES_TRANS]
1677QED
1678
1679
1680(*--------------------------------------------------------------------------
1681 RAT_LES_01
1682 |- 0q < 1q
1683 *--------------------------------------------------------------------------*)
1684
1685Theorem RAT_LES_01: rat_les 0q 1q
1686Proof
1687 REWRITE_TAC[rat_les_def] THEN
1688 RAT_CALC_TAC THEN
1689 FRAC_CALC_TAC THEN
1690 REWRITE_TAC[rat_sgn_def, frac_sgn_def, SGN_def] THEN
1691 REWRITE_TAC[RAT_NMREQ0_CONG, RAT_NMRLT0_CONG] THEN
1692 FRAC_NMRDNM_TAC
1693QED
1694
1695(*--------------------------------------------------------------------------
1696 RAT_LES_IMP_LEQ
1697 |- !r1 r2. r1 < r2 ==> r1 <= r2
1698 *--------------------------------------------------------------------------*)
1699
1700Theorem RAT_LES_IMP_LEQ:
1701 !r1 r2. rat_les r1 r2 ==> rat_leq r1 r2
1702Proof
1703 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def, rat_leq_def] THEN
1704 RW_TAC bool_ss []
1705QED
1706
1707(*--------------------------------------------------------------------------
1708 RAT_LES_IMP_NEQ
1709 |- !r1 r2. r1 < r2 ==> ~(r1 = r2)
1710 *--------------------------------------------------------------------------*)
1711
1712Theorem RAT_LES_IMP_NEQ:
1713 !r1 r2. rat_les r1 r2 ==> ~(r1 = r2)
1714Proof
1715 REPEAT GEN_TAC THEN REWRITE_TAC[rat_les_def] THEN
1716 SUBST_TAC[ISPECL[``r1:rat``,``r2:rat``] EQ_SYM_EQ] THEN
1717 ONCE_REWRITE_TAC[GSYM RAT_EQ_SUB0] THEN
1718 SUBST_TAC[
1719 CONJUNCT1 (CONJUNCT2 (SPEC ``rat_sub r2 r1`` (GSYM RAT_SGN_CLAUSES)))] THEN
1720 SIMP_TAC int_ss []
1721QED
1722
1723(*--------------------------------------------------------------------------
1724 RAT_LEQ_LES (RAT_NOT_LES_LEQ)
1725 |- !r1 r2. ~(r2 < r1) = r1 <= r2
1726 *--------------------------------------------------------------------------*)
1727
1728Theorem RAT_LEQ_LES:
1729 !r1 r2. ~(rat_les r2 r1) = rat_leq r1 r2
1730Proof
1731 RW_TAC bool_ss[rat_leq_def] THEN
1732 PROVE_TAC[RAT_LES_TOTAL, RAT_LES_ANTISYM]
1733QED
1734
1735(*--------------------------------------------------------------------------
1736 RAT_LES_LEQ, RAT_LES_LEQ2
1737
1738 |- !r1 r2. ~(rat_leq r2 r1) = r1 < r2
1739 |- !r1 r2. r1 < r2 = r1 <= r2 /\ ~(r2 = r1)
1740 *--------------------------------------------------------------------------*)
1741
1742Theorem RAT_LES_LEQ:
1743 !r1 r2. ~(rat_leq r2 r1) = rat_les r1 r2
1744Proof
1745 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN
1746 PROVE_TAC[RAT_LES_TOTAL, RAT_LES_IMP_NEQ, RAT_LES_ANTISYM]
1747QED
1748
1749Theorem RAT_LES_LEQ2:
1750 !r1 r2. rat_les r1 r2 <=> rat_leq r1 r2 /\ ~(rat_leq r2 r1)
1751Proof
1752 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN EQ_TAC THEN
1753 RW_TAC bool_ss [] THEN PROVE_TAC[RAT_LES_ANTISYM, RAT_LES_IMP_NEQ]
1754QED
1755
1756(*--------------------------------------------------------------------------
1757 RAT_LES_LEQ_TRANS, RAT_LEQ_LES_TRANS
1758
1759 |- !a b c. a < b /\ b <= c ==> a < c
1760 |- !a b c. a <= b /\ b < c ==> a < c
1761 *--------------------------------------------------------------------------*)
1762
1763Theorem RAT_LES_LEQ_TRANS:
1764 !a b c. rat_les a b /\ rat_leq b c ==> rat_les a c
1765Proof
1766 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN
1767 PROVE_TAC[RAT_LES_TRANS]
1768QED
1769
1770Theorem RAT_LEQ_LES_TRANS:
1771 !a b c. rat_leq a b /\ rat_les b c ==> rat_les a c
1772Proof
1773 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN PROVE_TAC[RAT_LES_TRANS]
1774QED
1775
1776(*--------------------------------------------------------------------------
1777 RAT_0LES_0LES_ADD, RAT_LES0_LES0_ADD
1778
1779 |- !r1 r2. 0q < r1 ==> 0q < r2 ==> 0q < r1 + r2
1780 |- !r1 r2. r1 < 0q ==> r2 < 0q ==> r1 + r2 < 0q
1781 *--------------------------------------------------------------------------*)
1782
1783Theorem RAT_0LES_0LES_ADD:
1784 !r1 r2. rat_les 0q r1 ==> rat_les 0q r2 ==> rat_les 0q (rat_add r1 r2)
1785Proof
1786 REPEAT GEN_TAC THEN REWRITE_TAC[RAT_0LES_NMR] THEN
1787 RAT_CALC_TAC THEN FRAC_CALC_TAC THEN
1788 REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRGT0_CONG] THEN
1789 FRAC_NMRDNM_TAC THEN
1790 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
1791 FRAC_POS_TAC ``frac_dnm (rep_rat r2)`` THEN
1792 REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD]
1793QED
1794
1795Theorem RAT_LES0_LES0_ADD:
1796 !r1 r2. rat_les r1 0q ==> rat_les r2 0q ==> rat_les (rat_add r1 r2) 0q
1797Proof
1798 REPEAT GEN_TAC THEN REWRITE_TAC[RAT_LES0_NMR] THEN
1799 RAT_CALC_TAC THEN FRAC_CALC_TAC THEN
1800 REWRITE_TAC[rat_nmr_def, RAT, FRAC, RAT_NMRLT0_CONG] THEN
1801 FRAC_NMRDNM_TAC THEN
1802 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
1803 FRAC_POS_TAC ``frac_dnm (rep_rat r2)`` THEN
1804 REPEAT STRIP_TAC THEN PROVE_TAC[INT_MUL_SIGN_CASES, INT_LT_ADD_NEG]
1805QED
1806
1807(*--------------------------------------------------------------------------
1808 RAT_0LES_0LEQ_ADD, RAT_LES0_LEQ0_ADD
1809
1810 |- !r1 r2. 0q < r1 ==> 0q <= r2 ==> 0q < r1 + r2
1811 |- !r1 r2. r1 < 0q ==> r2 <= 0q ==> r1 + r2 < 0q
1812 *--------------------------------------------------------------------------*)
1813
1814Theorem RAT_0LES_0LEQ_ADD:
1815 !r1 r2. rat_les 0q r1 ==> rat_leq 0q r2 ==> rat_les 0q (rat_add r1 r2)
1816Proof
1817 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN RW_TAC bool_ss [] THEN
1818 PROVE_TAC[RAT_0LES_0LES_ADD, RAT_ADD_RID]
1819QED
1820
1821
1822Theorem RAT_LES0_LEQ0_ADD:
1823 !r1 r2. rat_les r1 0q ==> rat_leq r2 0q ==> rat_les (rat_add r1 r2) 0q
1824Proof
1825 REPEAT GEN_TAC THEN REWRITE_TAC[rat_leq_def] THEN RW_TAC bool_ss [] THEN
1826 PROVE_TAC[RAT_LES0_LES0_ADD, RAT_ADD_RID]
1827QED
1828
1829(*--------------------------------------------------------------------------
1830 RAT_LSUB_EQ, RAT_RSUB_EQ
1831
1832 |- !r1 r2 r3. (r1 - r2 = r3) = (r1 = r2 + r3)
1833 |- !r1 r2 r3. (r1 = r2 - r3) = (r1 + r3 = r2)
1834 *--------------------------------------------------------------------------*)
1835
1836Theorem RAT_LSUB_EQ:
1837 !r1 r2 r3. (rat_sub r1 r2 = r3) = (r1 = rat_add r2 r3)
1838Proof
1839 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN BasicProvers.VAR_EQ_TAC THEN
1840 REWRITE_TAC[RAT_SUB_ADDAINV] THEN ONCE_REWRITE_TAC[RAT_ADD_COMM] THENL [
1841 ONCE_REWRITE_TAC[GSYM RAT_ADD_ASSOC]
1842 ,
1843 ONCE_REWRITE_TAC[RAT_ADD_ASSOC]
1844 ] THEN
1845 REWRITE_TAC[RAT_ADD_LINV] THEN REWRITE_TAC[RAT_ADD_LID, RAT_ADD_RID]
1846QED
1847
1848Theorem RAT_RSUB_EQ:
1849 !r1 r2 r3. (r1 = rat_sub r2 r3) = (rat_add r1 r3 = r2)
1850Proof
1851 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN BasicProvers.VAR_EQ_TAC THEN
1852 REWRITE_TAC[RAT_SUB_ADDAINV] THEN ONCE_REWRITE_TAC[GSYM RAT_ADD_ASSOC] THEN
1853 REWRITE_TAC[RAT_ADD_LINV, RAT_ADD_RINV] THEN
1854 REWRITE_TAC[RAT_ADD_LID, RAT_ADD_RID]
1855QED
1856
1857(*--------------------------------------------------------------------------
1858 RAT_LDIV_EQ, RAT_RDIV_EQ
1859
1860 |- !r1 r2 r3. ~(r2 = 0q) ==> ((r1 / r2 = r3) = (r1 = r2 * r3))
1861 |- !r1 r2 r3. ~(r3 = 0q) ==> ((r1 = r2 / r3) = (r1 * r3 = r2))
1862 *--------------------------------------------------------------------------*)
1863
1864Theorem RAT_LDIV_EQ:
1865 !r1 r2 r3. ~(r2 = 0q) ==> ((rat_div r1 r2 = r3) = (r1 = rat_mul r2 r3))
1866Proof
1867 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN
1868 BasicProvers.VAR_EQ_TAC THEN
1869 ONCE_REWRITE_TAC [RAT_MUL_COMM] THEN
1870 REWRITE_TAC [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC] THEN
1871 ASM_SIMP_TAC std_ss [RAT_MUL_RINV, RAT_MUL_LINV, RAT_MUL_RID, RAT_MUL_LID]
1872QED
1873
1874Theorem RAT_RDIV_EQ:
1875 !r1 r2 r3. ~(r3 = 0q) ==> ((r1 = rat_div r2 r3) = (rat_mul r1 r3 = r2))
1876Proof
1877 REPEAT (STRIP_TAC ORELSE EQ_TAC) THEN
1878 BasicProvers.VAR_EQ_TAC THEN
1879 REWRITE_TAC [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC] THEN
1880 ASM_SIMP_TAC std_ss [RAT_MUL_RINV, RAT_MUL_LINV, RAT_MUL_RID, RAT_MUL_LID]
1881QED
1882
1883
1884(*==========================================================================
1885 * one-to-one and onto theorems
1886 *==========================================================================*)
1887
1888(*--------------------------------------------------------------------------
1889 RAT_AINV_ONE_ONE
1890
1891 |- ONE_ONE rat_ainv
1892 *--------------------------------------------------------------------------*)
1893
1894Theorem RAT_AINV_ONE_ONE: ONE_ONE rat_ainv
1895Proof
1896 REWRITE_TAC[ONE_ONE_DEF] THEN
1897 BETA_TAC THEN
1898 REWRITE_TAC[RAT_EQ_AINV]
1899QED
1900
1901(*--------------------------------------------------------------------------
1902 RAT_ADD_ONE_ONE
1903
1904 |- !r1. ONE_ONE (rat_add r1)
1905 *--------------------------------------------------------------------------*)
1906
1907Theorem RAT_ADD_ONE_ONE:
1908 !r1. ONE_ONE (rat_add r1)
1909Proof
1910 REPEAT GEN_TAC THEN
1911 SIMP_TAC std_ss [ONE_ONE_DEF, GSYM RAT_LSUB_EQ] THEN
1912 SIMP_TAC std_ss [RAT_RSUB_EQ] THEN
1913 MATCH_ACCEPT_TAC RAT_ADD_COMM
1914QED
1915
1916(*--------------------------------------------------------------------------
1917 RAT_MUL_ONE_ONE
1918
1919 |- !r1. ~(r1=0q) = ONE_ONE (rat_mul r1)
1920 *--------------------------------------------------------------------------*)
1921
1922Theorem RAT_MUL_ONE_ONE:
1923 !r1. ~(r1=0q) = ONE_ONE (rat_mul r1)
1924Proof
1925 REPEAT GEN_TAC THEN REWRITE_TAC [ONE_ONE_DEF] THEN BETA_TAC THEN
1926 EQ_TAC THEN REPEAT DISCH_TAC
1927 THENL [
1928 ASM_SIMP_TAC std_ss [GSYM RAT_LDIV_EQ] THEN
1929 ASM_SIMP_TAC std_ss [RAT_RDIV_EQ] THEN
1930 MATCH_ACCEPT_TAC RAT_MUL_COMM,
1931 FIRST_X_ASSUM (ASSUME_TAC o Q.SPECL [`1q`, `0q`]) THEN
1932 REV_FULL_SIMP_TAC std_ss [RAT_1_NOT_0, RAT_MUL_LZERO] ]
1933QED
1934
1935(*==========================================================================
1936 * transformation of equations
1937 *==========================================================================*)
1938
1939(*--------------------------------------------------------------------------
1940 RAT_EQ_LADD, RAT_EQ_RADD
1941
1942 |- !r1 r2 r3. (r3 + r1 = r3 + r2) = (r1=r2)
1943 |- !r1 r2 r3. (r1 + r3 = r2 + r3) = (r1=r2)
1944 *--------------------------------------------------------------------------*)
1945
1946Theorem RAT_EQ_LADD: !r1 r2 r3. (rat_add r3 r1 = rat_add r3 r2) = (r1=r2)
1947Proof
1948 PROVE_TAC [REWRITE_RULE[ONE_ONE_THM] RAT_ADD_ONE_ONE, RAT_ADD_COMM]
1949QED
1950
1951Theorem RAT_EQ_RADD: !r1 r2 r3. (rat_add r1 r3 = rat_add r2 r3) = (r1=r2)
1952Proof
1953 PROVE_TAC [REWRITE_RULE[ONE_ONE_THM] RAT_ADD_ONE_ONE, RAT_ADD_COMM]
1954QED
1955
1956(*--------------------------------------------------------------------------
1957 RAT_EQ_LMUL, RAT_EQ_RMUL
1958
1959 |- !r1 r2 r3. ~(r3=0q) ==> ((r3 * r1 = r3 * r2) = (r1=r2))
1960 |- !r1 r2 r3. ~(r3=0q) ==> ((r1 * r3 = r2 * r3) = (r1=r2))
1961 *--------------------------------------------------------------------------*)
1962
1963Theorem RAT_EQ_RMUL: !r1 r2 r3. ~(r3=0q) ==> ((rat_mul r1 r3 = rat_mul r2 r3) = (r1=r2))
1964Proof
1965 REPEAT GEN_TAC THEN
1966 REWRITE_TAC[SPEC ``r3:rat`` RAT_MUL_ONE_ONE] THEN
1967 REWRITE_TAC[ONE_ONE_THM] THEN
1968 STRIP_TAC THEN
1969 ONCE_REWRITE_TAC[RAT_MUL_COMM] THEN
1970 PROVE_TAC[]
1971QED
1972
1973Theorem RAT_EQ_LMUL: !r1 r2 r3. ~(r3=0q) ==> ((rat_mul r3 r1 = rat_mul r3 r2) = (r1=r2))
1974Proof
1975 PROVE_TAC[RAT_EQ_RMUL, RAT_MUL_COMM]
1976QED
1977
1978(*==========================================================================
1979 * transformation of inequations
1980 *==========================================================================*)
1981
1982(*--------------------------------------------------------------------------
1983 RAT_LES_LADD, RAT_LES_RADD, RAT_LEQ_LADD, RAT_LEQ_RADD
1984
1985 |- !r1 r2 r3. (r3 + r1) < (r3 + r2) = r1 < r2
1986 |- !r1 r2 r3. (r1 + r3) < (r2 + r3) = r1 < r2
1987 |- !r1 r2 r3. (r3 + r1) <= (r3 + r2) = r1 <= r2
1988 |- !r1 r2 r3. (r1 + r3) <= (r2 + r3) = r1 <= r2
1989 *--------------------------------------------------------------------------*)
1990
1991Theorem RAT_LES_RADD: !r1 r2 r3. rat_les (rat_add r1 r3) (rat_add r2 r3) = rat_les r1 r2
1992Proof
1993 REPEAT GEN_TAC THEN
1994 REWRITE_TAC[rat_les_def, rat_sgn_def] THEN
1995 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_AINV_ADD] THEN
1996 SUBST_TAC[ EQT_ELIM (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add r2 r3) (rat_add (rat_ainv r1) (rat_ainv r3)) = rat_add (rat_add r2 (rat_ainv r1)) (rat_add r3 (rat_ainv r3))``) ] THEN
1997 REWRITE_TAC[RAT_ADD_RINV, RAT_ADD_RID]
1998QED
1999
2000Theorem RAT_LES_LADD: !r1 r2 r3. rat_les (rat_add r3 r1) (rat_add r3 r2) = rat_les r1 r2
2001Proof
2002 PROVE_TAC[RAT_LES_RADD, RAT_ADD_COMM]
2003QED
2004
2005Theorem RAT_LEQ_RADD:
2006 !r1 r2 r3. rat_leq (rat_add r1 r3) (rat_add r2 r3) = rat_leq r1 r2
2007Proof
2008 REWRITE_TAC[rat_leq_def, RAT_LES_RADD, RAT_EQ_RADD]
2009QED
2010
2011Theorem RAT_LEQ_LADD:
2012 !r1 r2 r3. rat_leq (rat_add r3 r1) (rat_add r3 r2) = rat_leq r1 r2
2013Proof
2014 REWRITE_TAC[rat_leq_def, RAT_LES_LADD, RAT_EQ_LADD]
2015QED
2016
2017Theorem RAT_ADD_MONO:
2018 !a b c d. a <= b /\ c <= d ==> rat_add a c <= rat_add b d
2019Proof
2020 REPEAT STRIP_TAC THEN irule RAT_LEQ_TRANS THEN
2021 Q.EXISTS_TAC `b + c` THEN
2022 ASM_SIMP_TAC std_ss [RAT_LEQ_LADD, RAT_LEQ_RADD]
2023QED
2024
2025(*--------------------------------------------------------------------------
2026 RAT_LES_AINV
2027
2028 |- !r1 r2. ~r1 < ~r2 = r2 < r1
2029 *--------------------------------------------------------------------------*)
2030
2031Theorem RAT_LES_AINV: !r1 r2. rat_les (rat_ainv r1) (rat_ainv r2) = rat_les r2 r1
2032Proof
2033 REPEAT GEN_TAC THEN
2034 SUBST_TAC[ SPECL[``rat_ainv r1``,``rat_ainv r2``,``r1:rat``] (GSYM RAT_LES_RADD)] THEN
2035 SUBST_TAC[ SPECL[``rat_add (rat_ainv r1) r1``,``rat_add (rat_ainv r2) r1``,``r2:rat``] (GSYM RAT_LES_RADD)] THEN
2036 SUBST_TAC[ EQT_ELIM (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add (rat_ainv r2) r1) r2 = rat_add (rat_add (rat_ainv r2) r2) r1``) ] THEN
2037 REWRITE_TAC[RAT_ADD_LINV, RAT_ADD_LID]
2038QED
2039
2040(*--------------------------------------------------------------------------
2041 RAT_LSUB_LES, RAT_RSUB_LES
2042
2043 |- !r1 r2 r3. (r1 - r2) < r3 = r1 < (r2 + r3)
2044 |- !r1 r2 r3. r1 < (r2 - r3) = (r1 + r3) < r2
2045 *--------------------------------------------------------------------------*)
2046
2047Theorem RAT_LSUB_LES: !r1 r2 r3. rat_les (rat_sub r1 r2) r3 = rat_les r1 (rat_add r2 r3)
2048Proof
2049 REPEAT GEN_TAC THEN
2050 REWRITE_TAC[rat_les_def] THEN
2051 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_AINV_ADD, RAT_AINV_AINV] THEN
2052 PROVE_TAC [AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add r3 (rat_add (rat_ainv r1) r2) = rat_add (rat_add r2 r3) (rat_ainv r1)``]
2053QED
2054
2055Theorem RAT_RSUB_LES: !r1 r2 r3. rat_les r1 (rat_sub r2 r3) = rat_les (rat_add r1 r3) r2
2056Proof
2057 REPEAT GEN_TAC THEN
2058 REWRITE_TAC[rat_les_def] THEN
2059 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_AINV_ADD] THEN
2060 PROVE_TAC [AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add r2 (rat_ainv r3)) (rat_ainv r1) = rat_add r2 (rat_add (rat_ainv r1) (rat_ainv r3))``]
2061QED
2062
2063Theorem RAT_LSUB_LEQ:
2064 !r1 r2 r3. rat_leq (rat_sub r1 r2) r3 = rat_leq r1 (rat_add r2 r3)
2065Proof
2066 REWRITE_TAC[rat_leq_def, RAT_LSUB_LES, RAT_LSUB_EQ]
2067QED
2068
2069Theorem RAT_RSUB_LEQ:
2070 !r1 r2 r3. rat_leq r1 (rat_sub r2 r3) = rat_leq (rat_add r1 r3) r2
2071Proof
2072 REWRITE_TAC[rat_leq_def, RAT_RSUB_LES, RAT_RSUB_EQ]
2073QED
2074
2075(*--------------------------------------------------------------------------
2076 RAT_LES_LMUL_NEG RAT_LES_LMUL_POS RAT_LES_RMUL_POS RAT_LES_RMUL_NEG
2077
2078 |- !r1 r2 r3. r3 < 0q ==> (r3 * r2 < r3 * r1) = r1 < r2)
2079 |- !r1 r2 r3. 0q < r3 ==> (r3 * r1 < r3 * r2) = r1 < r2)
2080 |- !r1 r2 r3. 0q < r3 ==> (r1 * r3 < r2 * r3) = r1 < r2)
2081 |- !r1 r2 r3. r3 < 0q ==> (r2 * r3 < r1 * r3) = r1 < r2)
2082 *--------------------------------------------------------------------------*)
2083
2084Theorem RAT_LES_RMUL_POS: !r1 r2 r3. rat_les 0q r3 ==> (rat_les (rat_mul r1 r3) (rat_mul r2 r3) = rat_les r1 r2)
2085Proof
2086 REPEAT GEN_TAC THEN
2087 REWRITE_TAC[rat_les_def] THEN
2088 REWRITE_TAC[RAT_SUB_RID] THEN
2089 STRIP_TAC THEN
2090 REWRITE_TAC[GSYM RAT_SUB_RDISTRIB] THEN
2091 EQ_TAC THENL
2092 [
2093 SUBGOAL_THEN ``~(r3 = 0q)`` ASSUME_TAC THENL
2094 [
2095 SUBST_TAC[CONJUNCT1 (CONJUNCT2 (SPEC ``r3:rat`` (GSYM RAT_SGN_CLAUSES)))] THEN
2096 RW_TAC int_ss[]
2097 ,
2098 UNDISCH_TAC ``rat_sgn r3 = 1i`` THEN
2099 SUBST_TAC [GSYM (UNDISCH (SPEC ``r3:rat`` RAT_SGN_MINV))] THEN
2100 REPEAT DISCH_TAC THEN
2101 ONCE_REWRITE_TAC[GSYM RAT_MUL_RID] THEN
2102 SUBST_TAC[GSYM (UNDISCH (SPEC ``r3:rat`` RAT_MUL_RINV))] THEN
2103 SUBST_TAC[EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``rat_mul (rat_sub r2 r1) (rat_mul r3 (rat_minv r3)) = rat_mul (rat_mul (rat_sub r2 r1) r3) (rat_minv r3)``)] THEN
2104 PROVE_TAC[RAT_SGN_MUL, INT_MUL_LID]
2105 ]
2106 ,
2107 STRIP_TAC THEN
2108 PROVE_TAC[RAT_SGN_MUL, INT_MUL_LID]
2109 ]
2110QED
2111
2112Theorem RAT_LES_LMUL_POS: !r1 r2 r3. rat_les 0q r3 ==> (rat_les (rat_mul r3 r1) (rat_mul r3 r2) = rat_les r1 r2)
2113Proof
2114 PROVE_TAC[RAT_LES_RMUL_POS, RAT_MUL_COMM]
2115QED
2116
2117Theorem RAT_LES_RMUL_NEG: !r1 r2 r3. rat_les r3 0q ==> (rat_les (rat_mul r2 r3) (rat_mul r1 r3) = rat_les r1 r2)
2118Proof
2119 REPEAT GEN_TAC THEN
2120 REWRITE_TAC[rat_les_def] THEN
2121 REWRITE_TAC[RAT_SUB_ADDAINV, RAT_ADD_LID] THEN
2122 SUBST_TAC[REWRITE_RULE [INT_NEG_EQ] (SPECL[``r3:rat``] (RAT_SGN_AINV))] THEN
2123 REWRITE_TAC[INT_NEG_EQ] THEN
2124 STRIP_TAC THEN
2125 SUBST_TAC[REWRITE_RULE [RAT_AINV_EQ] (SPECL[``r1:rat``,``r3:rat``] RAT_AINV_LMUL)] THEN
2126 REWRITE_TAC[GSYM RAT_AINV_ADD] THEN
2127 REWRITE_TAC[GSYM RAT_RDISTRIB] THEN
2128 SUBST_TAC[SPECL[``rat_ainv r1``,``r2:rat``] RAT_ADD_COMM] THEN
2129 EQ_TAC THENL
2130 [
2131 SUBGOAL_THEN ``~(r3 = 0q)`` ASSUME_TAC THENL
2132 [
2133 SUBST_TAC[CONJUNCT1 (CONJUNCT2 (SPEC ``r3:rat`` (GSYM RAT_SGN_CLAUSES)))] THEN
2134 RW_TAC int_ss[]
2135 ,
2136 UNDISCH_TAC ``rat_sgn r3 = ~1`` THEN
2137 SUBST_TAC [GSYM (UNDISCH (SPEC ``r3:rat`` RAT_SGN_MINV))] THEN
2138 REPEAT DISCH_TAC THEN
2139 ONCE_REWRITE_TAC[GSYM RAT_MUL_RID] THEN
2140 SUBST_TAC[GSYM (UNDISCH (SPEC ``r3:rat`` RAT_MUL_RINV))] THEN
2141 SUBST_TAC[EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``rat_mul (rat_add r2 (rat_ainv r1)) (rat_mul r3 (rat_minv r3)) = rat_mul (rat_mul (rat_add r2 (rat_ainv r1)) r3) (rat_minv r3)``)] THEN
2142 ONCE_REWRITE_TAC[GSYM RAT_SGN_AINV] THEN
2143 REWRITE_TAC[INT_NEG_EQ] THEN
2144 ONCE_REWRITE_TAC[RAT_AINV_LMUL] THEN
2145 RW_TAC int_ss [RAT_SGN_MUL]
2146
2147 ]
2148 ,
2149 STRIP_TAC THEN
2150 ONCE_REWRITE_TAC[GSYM INT_EQ_NEG] THEN
2151 REWRITE_TAC[RAT_SGN_AINV] THEN
2152 RW_TAC int_ss [RAT_SGN_MUL]
2153 ]
2154QED
2155
2156Theorem RAT_LES_LMUL_NEG: !r1 r2 r3. rat_les r3 0q ==> (rat_les (rat_mul r3 r2) (rat_mul r3 r1) = rat_les r1 r2)
2157Proof
2158 PROVE_TAC[RAT_LES_RMUL_NEG, RAT_MUL_COMM]
2159QED
2160
2161(*--------------------------------------------------------------------------
2162 RAT_AINV_LES
2163
2164 |- !r1 r2. ~r1 < r2 = ~r2 < r1
2165 *--------------------------------------------------------------------------*)
2166
2167Theorem RAT_AINV_LES: !r1 r2. rat_les (rat_ainv r1) r2 = rat_les (rat_ainv r2) r1
2168Proof
2169 REPEAT GEN_TAC THEN
2170 SUBST_TAC[SPECL [``r1:rat``,``~r2:rat``] (GSYM RAT_LES_AINV)] THEN
2171 PROVE_TAC[RAT_AINV_AINV]
2172QED
2173
2174(*--------------------------------------------------------------------------
2175 RAT_LDIV_LES_POS, RAT_LDIV_LES_NEG, RAT_RDIV_LES_POS, RAT_RDIV_LES_NEG
2176
2177 |- !r1 r2 r3. 0q < r2 ==> ((r1 / r2 < r3) = (r1 < r2 * r3))
2178 |- !r1 r2 r3. r2 < 0q ==> ((r1 / r2 < r3) = (r2 * r3 < r1))
2179 |- !r1 r2 r3. 0q < r3 ==> ((r1 < r2 / r3) = (r1 * r3 < r2))
2180 |- !r1 r2 r3. r3 < 0q ==> ((r1 < r2 / r3) = (r2 < r1 * r3))
2181
2182 RAT_LDIV_LEQ_POS, RAT_LDIV_LEQ_NEG, RAT_RDIV_LEQ_POS, RAT_RDIV_LEQ_NEG
2183 for <= likewise
2184 *--------------------------------------------------------------------------*)
2185
2186Theorem RAT_LDIV_LES_POS: !r1 r2 r3. 0q < r2 ==> ((rat_div r1 r2 < r3) = (r1 < rat_mul r2 r3))
2187Proof
2188 REPEAT STRIP_TAC THEN
2189 SUBST_TAC [UNDISCH (SPECL[``rat_div r1 r2``,``r3:rat``,``r2:rat``] (GSYM RAT_LES_LMUL_POS))] THEN
2190 SUBGOAL_THEN ``~(r2=0q)`` ASSUME_TAC THEN1
2191 PROVE_TAC[RAT_LES_REF] THEN
2192 REWRITE_TAC [RAT_DIV_MULMINV] THEN
2193 SUBST_TAC [EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``r2 * (r1 * rat_minv r2) = r1 * (r2 * rat_minv r2)``)] THEN
2194 RW_TAC bool_ss [RAT_MUL_RINV, RAT_MUL_RID]
2195QED
2196
2197Theorem RAT_LDIV_LES_NEG: !r1 r2 r3. r2 < 0q ==> ((rat_div r1 r2 < r3) = (rat_mul r2 r3 < r1))
2198Proof
2199 REPEAT STRIP_TAC THEN
2200 SUBST_TAC [UNDISCH (SPECL[``rat_div r1 r2``,``r3:rat``,``r2:rat``] (GSYM RAT_LES_RMUL_NEG))] THEN
2201 SUBGOAL_THEN ``~(r2=0q)`` ASSUME_TAC THEN1
2202 PROVE_TAC[RAT_LES_REF] THEN
2203 RW_TAC bool_ss [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC, RAT_MUL_LINV, RAT_MUL_RID] THEN
2204 PROVE_TAC[RAT_MUL_COMM]
2205QED
2206
2207Theorem RAT_RDIV_LES_POS: !r1 r2 r3. 0q < r3 ==> ((r1 < rat_div r2 r3) = (rat_mul r1 r3 < r2))
2208Proof
2209 REPEAT STRIP_TAC THEN
2210 SUBST_TAC [UNDISCH (SPECL[``r1:rat``,``rat_div r2 r3``,``r3:rat``] (GSYM RAT_LES_RMUL_POS))] THEN
2211 SUBGOAL_THEN ``~(r3=0q)`` ASSUME_TAC THEN1
2212 PROVE_TAC[RAT_LES_REF] THEN
2213 REWRITE_TAC [RAT_DIV_MULMINV] THEN
2214 SUBST_TAC [EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``r2 * rat_minv r3 * r3 = r2 * (r3 * rat_minv r3)``)] THEN
2215 RW_TAC bool_ss [RAT_MUL_RINV, RAT_MUL_RID]
2216QED
2217
2218Theorem RAT_RDIV_LES_NEG: !r1 r2 r3. r3 < 0q ==> ((r1 < rat_div r2 r3) = (r2 < rat_mul r1 r3))
2219Proof
2220 REPEAT STRIP_TAC THEN
2221 SUBST_TAC [UNDISCH (SPECL[``r1:rat``,``rat_div r2 r3``,``r3:rat``] (GSYM RAT_LES_RMUL_NEG))] THEN
2222 SUBGOAL_THEN ``~(r3=0q)`` ASSUME_TAC THEN1
2223 PROVE_TAC[RAT_LES_REF] THEN
2224 REWRITE_TAC [RAT_DIV_MULMINV] THEN
2225 SUBST_TAC [EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) ``r2 * rat_minv r3 * r3 = r2 * (r3 * rat_minv r3)``)] THEN
2226 RW_TAC bool_ss [RAT_MUL_RINV, RAT_MUL_RID]
2227QED
2228
2229Theorem RAT_LDIV_LEQ_POS:
2230 !r1 r2 r3. 0q < r2 ==> ((rat_div r1 r2 <= r3) = (r1 <= rat_mul r2 r3))
2231Proof
2232 REPEAT STRIP_TAC THEN
2233 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_LDIV_LES_POS] THEN
2234 RULE_ASSUM_TAC (CONJUNCT2 o
2235 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o
2236 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN
2237 ASM_SIMP_TAC bool_ss [RAT_LDIV_EQ]
2238QED
2239
2240Theorem RAT_LDIV_LEQ_NEG:
2241 !r1 r2 r3. r2 < 0q ==> ((rat_div r1 r2 <= r3) = (rat_mul r2 r3 <= r1))
2242Proof
2243 REPEAT STRIP_TAC THEN
2244 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_LDIV_LES_NEG] THEN
2245 RULE_ASSUM_TAC (GSYM o CONJUNCT2 o
2246 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o
2247 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN
2248 CONV_TAC (RHS_CONV (ONCE_DEPTH_CONV SYM_CONV)) THEN
2249 ASM_SIMP_TAC bool_ss [RAT_LDIV_EQ]
2250QED
2251
2252Theorem RAT_RDIV_LEQ_POS:
2253 !r1 r2 r3. 0q < r3 ==> ((r1 <= rat_div r2 r3) = (rat_mul r1 r3 <= r2))
2254Proof
2255 REPEAT STRIP_TAC THEN
2256 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_RDIV_LES_POS] THEN
2257 RULE_ASSUM_TAC (CONJUNCT2 o
2258 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o
2259 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN
2260 ASM_SIMP_TAC bool_ss [RAT_RDIV_EQ]
2261QED
2262
2263Theorem RAT_RDIV_LEQ_NEG:
2264 !r1 r2 r3. r3 < 0q ==> ((r1 <= rat_div r2 r3) = (r2 <= rat_mul r1 r3))
2265Proof
2266 REPEAT STRIP_TAC THEN
2267 ASM_SIMP_TAC bool_ss [rat_leq_def, RAT_RDIV_LES_NEG] THEN
2268 RULE_ASSUM_TAC (GSYM o CONJUNCT2 o
2269 REWRITE_RULE [rat_leq_def, DE_MORGAN_THM] o
2270 REWRITE_RULE [GSYM RAT_LES_LEQ]) THEN
2271 CONV_TAC (RHS_CONV (ONCE_DEPTH_CONV SYM_CONV)) THEN
2272 ASM_SIMP_TAC bool_ss [RAT_RDIV_EQ]
2273QED
2274
2275(*--------------------------------------------------------------------------
2276 RAT_LES_SUB0
2277
2278 |- !r1 r2. (r1 - r2) < 0q = r1 < r2
2279 *--------------------------------------------------------------------------*)
2280
2281Theorem RAT_LES_SUB0: !r1 r2. rat_les (rat_sub r1 r2) 0q = rat_les r1 r2
2282Proof
2283 REPEAT GEN_TAC THEN
2284 SUBST_TAC[GSYM (SPECL[``rat_sub r1 r2``,``0q``,``r2:rat``] RAT_LES_RADD)] THEN
2285 REWRITE_TAC[RAT_SUB_ADDAINV] THEN
2286 SUBST_TAC[EQT_ELIM(AC_CONV(RAT_ADD_ASSOC, RAT_ADD_COMM) ``rat_add (rat_add r1 (rat_ainv r2)) r2 = rat_add r1 (rat_add (rat_ainv r2) r2)``)] THEN
2287 REWRITE_TAC[RAT_ADD_LID, RAT_ADD_RID, RAT_ADD_LINV]
2288QED
2289
2290(*--------------------------------------------------------------------------
2291 RAT_LES_0SUB
2292
2293 |- !r1 r2. 0q < r1 - r2 = r2 < r1
2294 *--------------------------------------------------------------------------*)
2295
2296Theorem RAT_LES_0SUB: !r1 r2. rat_les 0q (rat_sub r1 r2) = rat_les r2 r1
2297Proof
2298 ONCE_REWRITE_TAC[GSYM RAT_LES_AINV] THEN
2299 REWRITE_TAC[RAT_AINV_SUB, RAT_AINV_0] THEN
2300 REWRITE_TAC[RAT_LES_SUB0] THEN
2301 PROVE_TAC[RAT_LES_AINV]
2302QED
2303
2304
2305(*--------------------------------------------------------------------------
2306 RAT_MINV_LES
2307
2308 |- !r1. 0q < r1 ==>
2309 (rat_minv r1 < 0q = r1 < 0q) /\
2310 (0q < rat_minv r1 = 0q < r1)
2311 *--------------------------------------------------------------------------*)
2312
2313Theorem RAT_SGN_AINV' = RAT_SGN_AINV |> Q.SPEC ‘-r’
2314 |> REWRITE_RULE [RAT_AINV_AINV]
2315 |> GSYM
2316
2317Theorem RAT_MINV_LES:
2318 !r1. r1 <> 0q ==>
2319 (rat_minv r1 < 0q <=> r1 < 0q) /\ (0q < rat_minv r1 <=> 0q < r1)
2320Proof
2321 GEN_TAC THEN
2322 DISCH_TAC THEN
2323 simp[RAT_SGN_MINV, RAT_SGN_AINV', RAT_SUB_LID, RAT_SUB_RID, rat_les_def]
2324QED
2325
2326
2327(*==========================================================================
2328 * other theorems
2329 *==========================================================================*)
2330
2331(*--------------------------------------------------------------------------
2332 RAT_MUL_SIGN_CASES
2333
2334 |- !p q.
2335 (0q < p * q = 0q < p /\ 0q < q \/ p < 0q /\ q < 0q) /\
2336 (p * q < 0q = 0q < p /\ q < 0q \/ p < 0q /\ 0q < q)
2337 *--------------------------------------------------------------------------*)
2338
2339Theorem RAT_MUL_SIGN_CASES:
2340 !p q. (0q < p * q <=> 0q < p /\ 0q < q \/ p < 0q /\ q < 0q) /\
2341 (p * q < 0q <=> 0q < p /\ q < 0q \/ p < 0q /\ 0q < q)
2342Proof
2343 REPEAT GEN_TAC THEN
2344 REWRITE_TAC[rat_les_def, RAT_SUB_LID, RAT_SUB_RID] THEN
2345 SUBST_TAC[GSYM (SPECL[“rat_sgn ~p”,“1i”] INT_EQ_NEG),
2346 GSYM (SPECL[“rat_sgn ~q”,“1i”] INT_EQ_NEG),
2347 GSYM (SPECL[“rat_sgn ~(p*q)”,“1i”] INT_EQ_NEG)] THEN
2348 REWRITE_TAC[RAT_SGN_AINV,RAT_SGN_MUL] THEN
2349 CONJ_TAC THEN
2350 ASSUME_TAC (SPEC “p:rat” RAT_SGN_TOTAL) THEN
2351 ASSUME_TAC (SPEC “q:rat” RAT_SGN_TOTAL) THEN
2352 UNDISCH_ALL_TAC THEN
2353 REPEAT STRIP_TAC THEN
2354 ASM_REWRITE_TAC[] THEN
2355 SIMP_TAC int_ss []
2356QED
2357
2358(*--------------------------------------------------------------------------
2359 RAT_NO_ZERODIV
2360 |- !r1 r2. (r1 = 0q) \/ (r2 = 0q) = (r1 * r2 = 0q)
2361
2362 RAT_NO_ZERODIV_NEG
2363 |- !r1 r2. ~(r1 * r2 = 0q) = ~(r1 = 0q) /\ ~(r2 = 0q)
2364 *--------------------------------------------------------------------------*)
2365
2366Theorem RAT_NO_ZERODIV:
2367 !r1 r2. r1 = 0q \/ r2 = 0q <=> rat_mul r1 r2 = 0q
2368Proof
2369 REPEAT GEN_TAC THEN
2370 ASM_CASES_TAC “r1=0q” THEN
2371 ASM_CASES_TAC “r2=0q” THEN
2372 RW_TAC int_ss[RAT_MUL_LZERO, RAT_MUL_RZERO] THEN
2373 UNDISCH_ALL_TAC THEN
2374 REWRITE_TAC[RAT_EQ0_NMR, rat_nmr_def] THEN
2375 DISCH_TAC THEN
2376 DISCH_TAC THEN
2377 RAT_CALCTERM_TAC “rat_mul r1 r2” THEN
2378 FRAC_CALCTERM_TAC “frac_mul (rep_rat r1) (rep_rat r2)” THEN
2379 REWRITE_TAC[RAT_NMREQ0_CONG] THEN
2380 FRAC_NMRDNM_TAC THEN
2381 PROVE_TAC[INT_ENTIRE]
2382QED
2383
2384Theorem RAT_NO_ZERODIV_THM[simp] =
2385 ONCE_REWRITE_RULE [EQ_SYM_EQ] RAT_NO_ZERODIV
2386
2387Theorem RAT_NO_ZERODIV_NEG: !r1 r2. r1 * r2 <> 0q <=> r1 <> 0q /\ r2 <> 0q
2388Proof PROVE_TAC[RAT_NO_ZERODIV]
2389QED
2390
2391(*--------------------------------------------------------------------------
2392 RAT_NO_IDDIV
2393
2394 |- !r1 r2. (r1 * r2 = r2) = (r1=1q) \/ (r2=0q)
2395 *--------------------------------------------------------------------------*)
2396
2397Theorem RAT_NO_IDDIV:
2398 !r1 r2. rat_mul r1 r2 = r2 <=> r1 = 1 \/ r2 = 0
2399Proof
2400 REPEAT GEN_TAC THEN
2401 ASM_CASES_TAC “r2 = 0q” THEN
2402 RW_TAC bool_ss [RAT_MUL_LID, RAT_MUL_RID, RAT_MUL_LZERO, RAT_MUL_RZERO] THEN
2403 SUBST_TAC[GSYM (SPEC “r2:rat” RAT_MUL_LID)] THEN
2404 SUBST1_TAC
2405 (EQT_ELIM (AC_CONV
2406 (RAT_MUL_ASSOC, RAT_MUL_COMM)
2407 “rat_mul r1 (rat_mul 1q r2) = rat_mul (rat_mul r1 1q) r2”)) THEN
2408 REWRITE_TAC[RAT_MUL_RID] THEN
2409 SUBST_TAC [UNDISCH (SPECL[“r1:rat”,“1q”,“r2:rat”] RAT_EQ_RMUL)] THEN
2410 PROVE_TAC[]
2411QED
2412
2413(* moving divisions out *)
2414
2415Theorem RDIV_MUL_OUT:
2416 r1 * (r2 / r3) = (r1 * r2) / r3
2417Proof
2418 metis_tac[RAT_MUL_ASSOC, RAT_DIV_MULMINV]
2419QED
2420
2421Theorem LDIV_MUL_OUT:
2422 (r1 / r2) * r3 = (r1 * r3) / r2
2423Proof
2424 metis_tac[RAT_MUL_ASSOC, RAT_DIV_MULMINV, RAT_MUL_COMM]
2425QED
2426
2427(*==========================================================================
2428 * calculation via frac_save terms
2429 *==========================================================================*)
2430
2431(*--------------------------------------------------------------------------
2432 RAT_SAVE: thm
2433 |- !r1. ?a1 b1. r1 = abs_rat(frac_save a1 b1)
2434 *--------------------------------------------------------------------------*)
2435
2436Theorem RAT_SAVE: !r1. ?a1 b1. r1 = abs_rat(frac_save a1 b1)
2437Proof
2438 REPEAT GEN_TAC THEN
2439 SUBST_TAC[GSYM (SPEC ``r1:rat`` RAT)] THEN
2440 SUBST_TAC[GSYM (SPEC ``rep_rat r1`` FRAC)] THEN
2441 EXISTS_TAC ``rat_nmr r1`` THEN
2442 EXISTS_TAC ``Num (rat_dnm r1 -1i)`` THEN
2443 REWRITE_TAC[frac_save_def, rat_nmr_def, rat_dnm_def, RAT_ABS_EQUIV, rat_equiv_def] THEN
2444 FRAC_POS_TAC ``frac_dnm (rep_rat r1)`` THEN
2445 ASSUME_TAC (ARITH_PROVE ``0 < & (Num (frac_dnm (rep_rat r1) - 1i)) + 1i``) THEN
2446 FRAC_NMRDNM_TAC THEN
2447 `0 <= frac_dnm (rep_rat r1) - 1i` by ARITH_TAC THEN
2448 `& (Num (frac_dnm (rep_rat r1) - 1i)) = frac_dnm (rep_rat r1) - 1i` by PROVE_TAC[INT_OF_NUM] THEN
2449 ARITH_TAC
2450QED
2451
2452(*--------------------------------------------------------------------------
2453 RAT_SAVE_MINV: thm
2454 |- !a1 b1. ~(abs_rat (frac_save a1 b1) = 0q) ==>
2455 (rat_minv (abs_rat (frac_save a1 b1)) =
2456 abs_rat( frac_save (SGN a1 * (& b1 + 1)) (Num (ABS a1 - 1))) )
2457 *--------------------------------------------------------------------------*)
2458
2459Theorem RAT_SAVE_MINV: !a1 b1. ~(abs_rat (frac_save a1 b1) = 0q) ==> (rat_minv (abs_rat (frac_save a1 b1)) = abs_rat( frac_save (SGN a1 * (& b1 + 1i)) (Num (ABS a1 - 1i))) )
2460Proof
2461 REPEAT GEN_TAC THEN
2462 REWRITE_TAC[RAT_EQ0_NMR, rat_nmr_def, RAT_NMREQ0_CONG] THEN
2463 STRIP_TAC THEN
2464 `~(0i = frac_nmr (frac_save a1 b1))` by PROVE_TAC[] THEN
2465 REWRITE_TAC[UNDISCH (SPEC ``frac_save a1 b1`` RAT_MINV_CALCULATE)] THEN
2466 `~(a1 = 0i)` by PROVE_TAC[FRAC_NMR_SAVE] THEN
2467 RW_TAC int_ss [FRAC_MINV_SAVE]
2468QED
2469
2470(*--------------------------------------------------------------------------
2471 RAT_SAVE_TO_CONS: thm
2472 |- !a1 b1. abs_rat (frac_save a1 b1) = rat_cons a1 (& b1 + 1)
2473 *--------------------------------------------------------------------------*)
2474
2475Theorem RAT_SAVE_TO_CONS: !a1 b1. abs_rat (frac_save a1 b1) = rat_cons a1 (& b1 + 1)
2476Proof
2477 REPEAT GEN_TAC THEN
2478 REWRITE_TAC[rat_cons_def, frac_save_def, RAT_ABS_EQUIV, rat_equiv_def] THEN
2479 ASSUME_TAC (ARITH_PROVE ``0i < & b1 + 1i``) THEN
2480 ASSUME_TAC (ARITH_PROVE ``~(& b1 + 1i < 0i)``) THEN
2481 ASM_REWRITE_TAC[INT_ABS] THEN
2482 FRAC_NMRDNM_TAC THEN
2483 RW_TAC int_ss [SGN_def]
2484QED
2485
2486(*==========================================================================
2487 * calculation of numeral forms
2488 *==========================================================================*)
2489
2490(*--------------------------------------------------------------------------
2491 RAT_OF_NUM: thm
2492 |- !n. (0 = rat_0) /\ (!n. & (SUC n) = &n + rat_1)
2493 *--------------------------------------------------------------------------*)
2494
2495Theorem RAT_OF_NUM: !n. (0 = rat_0) /\ (!n. & (SUC n) = &n + rat_1)
2496Proof
2497 REWRITE_TAC[rat_of_num_def] THEN
2498 Induct_on `n` THEN
2499 REWRITE_TAC[RAT_ADD_LID, rat_of_num_def]
2500QED
2501
2502(*--------------------------------------------------------------------------
2503 RAT_SAVE: thm
2504 |- !n. &n = abs_rat(frac_save (&n) 0)
2505 *--------------------------------------------------------------------------*)
2506
2507Theorem RAT_SAVE_NUM: !n. &n = abs_rat(frac_save (&n) 0)
2508Proof
2509 Induct_on `n` THEN
2510 RW_TAC int_ss [frac_save_def, RAT_OF_NUM] THEN1
2511 PROVE_TAC[rat_0_def, frac_0_def] THEN
2512 RAT_CALC_TAC THEN
2513 FRAC_CALC_TAC THEN
2514 REWRITE_TAC[RAT_EQ] THEN
2515 FRAC_NMRDNM_TAC THEN
2516 ARITH_TAC
2517QED
2518
2519(*--------------------------------------------------------------------------
2520 RAT_CONS_TO_NUM: thm
2521 |- !n. (&n // 1 = &n) /\ ((~&n) // 1 = ~&n)
2522 *--------------------------------------------------------------------------*)
2523
2524Theorem RAT_CONS_TO_NUM:
2525 !n. (&n // 1 = &n) /\ ((~&n) // 1 = ~&n)
2526Proof
2527 Induct_on ‘n’ THEN1
2528 RW_TAC int_ss [rat_cons_def, RAT_AINV_0, rat_0, frac_0_def] THEN
2529 RULE_ASSUM_TAC (ONCE_REWRITE_RULE[EQ_SYM_EQ]) THEN
2530 ASM_REWRITE_TAC[rat_cons_def, RAT_OF_NUM, RAT_AINV_ADD] THEN
2531 RAT_CALC_TAC THEN
2532 ‘0 < ABS 1’ by ARITH_TAC THEN
2533 FRAC_CALC_TAC THEN
2534 REWRITE_TAC[RAT_EQ] THEN
2535 FRAC_NMRDNM_TAC THEN
2536 RW_TAC int_ss [SGN_def] THEN
2537 ARITH_TAC
2538QED
2539
2540(*--------------------------------------------------------------------------
2541 RAT_0: thm
2542 |- rat_0 = 0
2543
2544 RAT_1: thm
2545 |- rat_1 = 1
2546 *--------------------------------------------------------------------------*)
2547
2548Theorem RAT_0: rat_0 = 0q
2549Proof
2550 REWRITE_TAC[rat_of_num_def]
2551QED
2552
2553Theorem RAT_1: rat_1 = 1q
2554Proof
2555 `1 = SUC 0` by ARITH_TAC THEN
2556 ASM_REWRITE_TAC[] THEN
2557 REWRITE_TAC[rat_of_num_def, RAT_ADD_LID]
2558QED
2559
2560Theorem RAT_OF_NUM_LEQ_0[local]:
2561 !n. 0 <= &n
2562Proof
2563 Induct_on `n` THEN1
2564 PROVE_TAC[RAT_LEQ_REF] THEN
2565 REWRITE_TAC[RAT_OF_NUM] THEN
2566 ASSUME_TAC RAT_LES_01 THEN
2567 ASSUME_TAC (SPECL [``1:rat``, ``&n:rat``] RAT_0LES_0LEQ_ADD) THEN
2568 REWRITE_TAC[RAT_1, RAT_0] THEN
2569 REWRITE_TAC[rat_leq_def] THEN
2570 PROVE_TAC[RAT_ADD_COMM]
2571QED
2572
2573(*--------------------------------------------------------------------------
2574 * RAT_MINV_1: thm
2575 * |- rat_minv 1 = 1
2576 *--------------------------------------------------------------------------*)
2577
2578Theorem RAT_MINV_1[simp]: rat_minv 1 = 1
2579Proof
2580 REWRITE_TAC [SYM RAT_1, rat_1_def] THEN
2581 SIMP_TAC intLib.int_ss [RAT_MINV_CALCULATE, NMR, frac_1_def,
2582 REWRITE_RULE [frac_1_def] FRAC_MINV_1]
2583QED
2584
2585Theorem RAT_DIV_1[simp]:
2586 r / 1q = r
2587Proof
2588 simp[RAT_DIV_MULMINV]
2589QED
2590
2591Theorem RAT_DIV_NEG1[simp]:
2592 r / -1q = -r
2593Proof
2594 simp[RAT_DIV_MULMINV, GSYM RAT_AINV_MINV, RAT_1_NOT_0, GSYM RAT_AINV_RMUL]
2595QED
2596
2597Theorem RAT_DIV_INV[simp]:
2598 r <> 0 ==> (r / r = 1)
2599Proof
2600 simp[RAT_DIV_MULMINV, RAT_MUL_RINV]
2601QED
2602
2603Theorem RAT_MINV_MUL:
2604 a <> 0 /\ b <> 0 ==> (rat_minv (a * b) = rat_minv a * rat_minv b)
2605Proof
2606 strip_tac >>
2607 qspecl_then [‘rat_minv (a * b)’, ‘rat_minv a * rat_minv b’, ‘a’] mp_tac
2608 RAT_EQ_LMUL >> simp[] >> disch_then (SUBST1_TAC o SYM) >>
2609 simp[RAT_MUL_ASSOC, RAT_MUL_RINV] >>
2610 qspecl_then [‘a * rat_minv (a * b)’, ‘rat_minv b’, ‘b’] mp_tac
2611 RAT_EQ_LMUL >> simp[] >> disch_then (SUBST1_TAC o SYM) >>
2612 simp[RAT_MUL_RINV, RAT_MUL_ASSOC] >>
2613 ‘b * a * rat_minv (a * b) = a * b * rat_minv (a * b)’
2614 by simp[AC RAT_MUL_ASSOC RAT_MUL_COMM] >>
2615 pop_assum SUBST_ALL_TAC >>
2616 ‘a * b <> 0’ by simp[RAT_NO_ZERODIV_NEG] >>
2617 simp[RAT_MUL_RINV]
2618QED
2619
2620Theorem RAT_DIVDIV_MUL:
2621 b <> 0 /\ d <> 0 ==> ((a / b) * (c / d) = (a * c) / (b * d))
2622Proof
2623 simp[RAT_DIV_MULMINV, RAT_MINV_MUL, AC RAT_MUL_COMM RAT_MUL_ASSOC]
2624QED
2625
2626Theorem RAT_DIVDIV_ADD:
2627 y <> 0 /\ b <> 0 ==> (x / y + a / b = (x * b + a * y) / (y * b))
2628Proof
2629 strip_tac >> qmatch_abbrev_tac ‘LHS = RHS’ >>
2630 ‘LHS = LHS * (y/y) * (b/b)’ by simp[] >>
2631 pop_assum SUBST1_TAC >> simp_tac bool_ss [Abbr`LHS`, RAT_RDISTRIB] >>
2632 ‘x / y * (y / y) = x / y’ by simp[] >> pop_assum SUBST1_TAC >>
2633 ‘x / y * (b / b) = (x * b) / (y * b)’ by simp[RAT_DIVDIV_MUL] >>
2634 pop_assum SUBST1_TAC >> ‘b / b = 1’ by simp[] >>
2635 asm_simp_tac bool_ss [RAT_MUL_RID] >> simp[RAT_DIVDIV_MUL] >>
2636 simp[Abbr`RHS`, RAT_RDISTRIB, RAT_DIV_MULMINV, AC RAT_MUL_ASSOC RAT_MUL_COMM]
2637QED
2638
2639Theorem RAT_DIV_AINV:
2640 -(x/y) = (-x)/y
2641Proof
2642 simp[RAT_DIV_MULMINV, RAT_AINV_LMUL]
2643QED
2644
2645Theorem RAT_MINV_EQ_0[simp]:
2646 r <> 0 ==> rat_minv r <> 0
2647Proof
2648 strip_tac >> disch_then (mp_tac o Q.AP_TERM ‘$* r’) >>
2649 simp[RAT_MUL_RINV, RAT_1_NOT_0]
2650QED
2651
2652Theorem RAT_DIV_MINV:
2653 x <> 0 /\ y <> 0 ==> (rat_minv (x/y) = y / x)
2654Proof
2655 strip_tac >>
2656 ‘x / y <> 0’ by simp[RAT_DIV_MULMINV, RAT_NO_ZERODIV_NEG] >>
2657 qspecl_then [‘rat_minv (x / y)’, ‘y / x’, ‘x / y’] mp_tac
2658 RAT_EQ_LMUL >> simp[] >> disch_then (SUBST1_TAC o SYM) >>
2659 simp[RAT_MUL_RINV, RAT_DIVDIV_MUL] >>
2660 simp[RAT_MUL_COMM, RAT_NO_ZERODIV_NEG]
2661QED
2662
2663Theorem RAT_DIV_EQ0[simp]:
2664 d <> 0 ==> ((n / d = 0) <=> (n = 0)) /\ ((0 = n / d) <=> (n = 0))
2665Proof
2666 strip_tac >> simp[RAT_DIV_MULMINV, GSYM RAT_NO_ZERODIV, RAT_MINV_EQ_0]
2667QED
2668
2669(*--------------------------------------------------------------------------
2670 RAT_ADD_NUM: thm
2671
2672 |- !n m. ( &n + &m = &(n+m))
2673 |- !n m. (~&n + &m = if n<=m then &(m-n) else ~&(n-m))
2674 |- !n m. &n + ~&m = if m<=n then &(n-m) else ~&(m-n)
2675 |- !n m. ~&n + ~&m = ~&(n+m)
2676 *--------------------------------------------------------------------------*)
2677
2678Theorem RAT_ADD_NUM1[local]:
2679 !n m. ( &n + &m = &(n+m))
2680Proof
2681 Induct_on `m` THEN
2682 Induct_on `n` THEN
2683 RW_TAC int_ss [RAT_ADD_LID, RAT_ADD_RID] THEN
2684 LEFT_NO_FORALL_TAC 1 ``SUC (SUC n)`` THEN
2685 UNDISCH_HD_TAC THEN
2686 REWRITE_TAC[RAT_OF_NUM] THEN
2687 `SUC (SUC n) + m = SUC m + SUC n` by ARITH_TAC THEN
2688 PROVE_TAC[RAT_ADD_ASSOC, RAT_ADD_COMM]
2689QED
2690
2691Theorem RAT_ADD_NUM2[local]:
2692 !n m. (~&n + &m = if n<=m then &(m-n) else ~&(n-m))
2693Proof
2694 Induct_on ‘n’ THEN
2695 Induct_on ‘m’ THEN
2696 SIMP_TAC int_ss [RAT_AINV_0, RAT_ADD_LID, RAT_ADD_RID] THEN
2697 FIRST_X_ASSUM
2698 (Q.SPEC_THEN ‘m’ (ASSUME_TAC o ONCE_REWRITE_RULE[EQ_SYM_EQ])) THEN
2699 ASM_REWRITE_TAC[] THEN
2700 REWRITE_TAC[RAT_OF_NUM] THEN
2701 REWRITE_TAC[RAT_AINV_ADD] THEN
2702 SUBST1_TAC
2703 (EQT_ELIM
2704 (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM)
2705 “~& n + ~rat_1 + (& m + rat_1) = ~& n + & m + (rat_1 + ~rat_1)”)) THEN
2706 REWRITE_TAC[RAT_ADD_RINV, RAT_ADD_RID]
2707QED
2708
2709Theorem RAT_ADD_NUM3[local]:
2710 !n m. &n + ~&m = if m<=n then &(n-m) else ~&(m-n)
2711Proof
2712 PROVE_TAC[RAT_ADD_NUM2, RAT_ADD_COMM]
2713QED
2714
2715Theorem RAT_ADD_NUM4[local]:
2716 !n m. ~&n + ~&m = ~&(n+m)
2717Proof
2718 PROVE_TAC[RAT_ADD_NUM1, RAT_EQ_AINV, RAT_AINV_ADD]
2719QED
2720
2721Theorem RAT_ADD_NUM_CALCULATE = LIST_CONJ[RAT_ADD_NUM1, RAT_ADD_NUM2, RAT_ADD_NUM3, RAT_ADD_NUM4];
2722
2723Theorem RAT_TIMES2:
2724 2 * (x:rat) = x + x
2725Proof
2726 ‘2n = 1 + 1’ by simp[] >> pop_assum SUBST_ALL_TAC >>
2727 REWRITE_TAC[GSYM RAT_ADD_NUM_CALCULATE, RAT_RDISTRIB, RAT_MUL_LID]
2728QED
2729
2730(*--------------------------------------------------------------------------
2731 RAT_ADD_MUL: thm
2732
2733 |- !n m. &n * &m = &(n*m)
2734 |- !n m. ~&n * &m = ~&(n*m)
2735 |- !n m. &n * ~&m = ~&(n*m)
2736 |- !n m. ~&n * ~&m = &(n*m)
2737 *--------------------------------------------------------------------------*)
2738
2739Theorem RAT_MUL_NUM1[local]:
2740 !n m. &n * &m = &(n*m)
2741Proof
2742 Induct_on `m` THEN
2743 Induct_on `n` THEN
2744 RW_TAC int_ss [RAT_MUL_LZERO, RAT_MUL_RZERO] THEN
2745 `!x. SUC x = x + 1` by ARITH_TAC THEN
2746 `(n+1) * (m+1) = n * m + n + m + 1:num` by ARITH_TAC THEN
2747 ASM_REWRITE_TAC[GSYM RAT_ADD_NUM1, RAT_LDISTRIB, RAT_RDISTRIB, RAT_ADD_ASSOC, RAT_MUL_ASSOC, RAT_MUL_LID, RAT_MUL_RID, MULT_CLAUSES] THEN
2748 METIS_TAC[RAT_ADD_ASSOC, RAT_ADD_COMM, MULT_COMM]
2749QED
2750
2751Theorem RAT_MUL_NUM2[local]:
2752 !n m. ~&n * &m = ~&(n*m)
2753Proof
2754 PROVE_TAC[GSYM RAT_AINV_LMUL, RAT_EQ_AINV, RAT_MUL_NUM1]
2755QED
2756
2757Theorem RAT_MUL_NUM3[local]:
2758 !n m. &n * ~&m = ~&(n*m)
2759Proof
2760 PROVE_TAC[GSYM RAT_AINV_RMUL, RAT_EQ_AINV, RAT_MUL_NUM1]
2761QED
2762
2763Theorem RAT_MUL_NUM4[local]:
2764 !n m. ~&n * ~&m = &(n*m)
2765Proof
2766 PROVE_TAC[GSYM RAT_AINV_RMUL, GSYM RAT_AINV_LMUL, RAT_AINV_AINV, RAT_MUL_NUM1]
2767QED
2768
2769Theorem RAT_MUL_NUM_CALCULATE = LIST_CONJ[RAT_MUL_NUM1, RAT_MUL_NUM2, RAT_MUL_NUM3, RAT_MUL_NUM4];
2770
2771(*--------------------------------------------------------------------------
2772 RAT_EQ_NUM: thm
2773
2774 |- !n m. ( &n = &m) = (n=m)
2775 |- !n m. ( &n = ~&m) = (n=0) /\ (m=0)
2776 |- !n m. (~&n = &m) = (n=0) /\ (m=0)
2777 |- !n m. (~&n = ~&m) = (n=m)
2778 *--------------------------------------------------------------------------*)
2779
2780Theorem RAT_EQ_NUM1[local]: !n m. &n = &m <=> n = m
2781Proof
2782 Induct_on ‘n’ THEN
2783 Induct_on ‘m’ THEN
2784 RW_TAC arith_ss [RAT_OF_NUM] THENL
2785 [
2786 MATCH_MP_TAC (prove(“!r1 r2. (r1 < r2) ==> ~(r1 = r2)”,
2787 PROVE_TAC[RAT_LES_ANTISYM])) THEN
2788 ASSUME_TAC (ONCE_REWRITE_RULE
2789 [RAT_ADD_COMM, GSYM RAT_0]
2790 (SPECL[“rat_1”,“&m:rat”] RAT_0LES_0LEQ_ADD)) THEN
2791 ASSUME_TAC (SPEC “m:num” RAT_OF_NUM_LEQ_0) THEN
2792 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0]
2793 ,
2794 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
2795 MATCH_MP_TAC (prove(“!r1 r2. (r1 < r2) ==> ~(r1 = r2)”,
2796 PROVE_TAC[RAT_LES_ANTISYM])) THEN
2797 ASSUME_TAC (ONCE_REWRITE_RULE
2798 [RAT_ADD_COMM, GSYM RAT_0]
2799 (SPECL[“rat_1”,“&n:rat”] RAT_0LES_0LEQ_ADD)) THEN
2800 ASSUME_TAC (SPEC “n:num” RAT_OF_NUM_LEQ_0) THEN
2801 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0]
2802 ,
2803 simp[RAT_EQ_RADD]
2804 ]
2805QED
2806
2807Theorem RAT_EQ_NUM2[local]: !n m. ( &n = ~&m) <=> (n=0) /\ (m=0)
2808Proof
2809 Induct_on ‘n’ THEN
2810 Induct_on ‘m’ THEN
2811 RW_TAC arith_ss [RAT_OF_NUM] THENL
2812 [
2813 PROVE_TAC[RAT_AINV_0, RAT_0]
2814 ,
2815 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
2816 MATCH_MP_TAC (prove(“!r1 r2. (r1 < r2) ==> ~(r1 = r2)”,
2817 PROVE_TAC[RAT_LES_ANTISYM])) THEN
2818 REWRITE_TAC[RAT_0] THEN
2819 ONCE_REWRITE_TAC[GSYM RAT_AINV_0] THEN
2820 REWRITE_TAC[RAT_LES_AINV] THEN
2821 ASSUME_TAC
2822 (ONCE_REWRITE_RULE[RAT_ADD_COMM, GSYM RAT_0]
2823 (SPECL[“rat_1”,“&m:rat”] RAT_0LES_0LEQ_ADD)) THEN
2824 ASSUME_TAC (SPEC “m:num” RAT_OF_NUM_LEQ_0) THEN
2825 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0]
2826 ,
2827 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
2828 MATCH_MP_TAC (prove(“!r1 r2. (r1 < r2) ==> ~(r1 = r2)”,
2829 PROVE_TAC[RAT_LES_ANTISYM])) THEN
2830 REWRITE_TAC[RAT_0] THEN
2831 REWRITE_TAC[RAT_AINV_0] THEN
2832 ASSUME_TAC (ONCE_REWRITE_RULE
2833 [RAT_ADD_COMM, GSYM RAT_0]
2834 (SPECL[“rat_1”,“&n:rat”] RAT_0LES_0LEQ_ADD)) THEN
2835 ASSUME_TAC (SPEC “n:num” RAT_OF_NUM_LEQ_0) THEN
2836 PROVE_TAC[RAT_LES_01, RAT_1, RAT_0]
2837 ,
2838 REWRITE_TAC[GSYM RAT_RSUB_EQ] THEN
2839 REWRITE_TAC[RAT_SUB_ADDAINV, GSYM RAT_AINV_ADD] THEN
2840 LEFT_NO_FORALL_TAC 1 “SUC (SUC m):num” THEN
2841 UNDISCH_HD_TAC THEN
2842 SIMP_TAC arith_ss [RAT_OF_NUM]
2843 ]
2844QED
2845
2846Theorem RAT_EQ_NUM3[local]: !n m. (~&n = &m) <=> (n=0)/\(m=0)
2847Proof PROVE_TAC[RAT_EQ_AINV, RAT_EQ_NUM2]
2848QED
2849
2850Theorem RAT_EQ_NUM4[local]: !n m. (~&n = ~&m) <=> n=m
2851Proof PROVE_TAC[RAT_AINV_EQ, RAT_EQ_NUM1]
2852QED
2853
2854Theorem RAT_EQ_NUM_CALCULATE[simp] =
2855 LIST_CONJ [RAT_EQ_NUM1, RAT_EQ_NUM2, RAT_EQ_NUM3, RAT_EQ_NUM4]
2856
2857(* ----------------------------------------------------------------------
2858 RAT_LT_NUM
2859 ---------------------------------------------------------------------- *)
2860
2861val RAT_LT_NUM1 = RAT_OF_NUM_LES
2862
2863Theorem RAT_LT_NUM2[local]:
2864 -&m < &n <=> 0 < m \/ 0 < n
2865Proof
2866 eq_tac >- (spose_not_then strip_assume_tac >> fs[]) >>
2867 strip_tac
2868 >- (irule RAT_LES_LEQ_TRANS >> qexists_tac `0` >> simp[] >>
2869 simp[Once RAT_AINV_LES]) >>
2870 irule RAT_LEQ_LES_TRANS >> qexists_tac `0` >> simp[] >>
2871 simp[rat_leq_def] >>
2872 simp[Once RAT_AINV_LES]
2873QED
2874
2875Theorem RAT_LT_NUM3[local]:
2876 &m < -&n <=> F
2877Proof
2878 simp[] >> strip_tac >>
2879 ‘-&n <= 0’ by simp[rat_leq_def, Once RAT_AINV_LES] >>
2880 ‘&m < 0’ by metis_tac[RAT_LES_LEQ_TRANS] >> fs[]
2881QED
2882
2883Theorem RAT_LT_NUM4[local]:
2884 -&m < -&n <=> n < m
2885Proof
2886 simp[RAT_LES_AINV]
2887QED
2888
2889Theorem RAT_LT_NUM_CALCULATE[simp] =
2890 LIST_CONJ [RAT_LT_NUM1, RAT_LT_NUM2, RAT_LT_NUM3, RAT_LT_NUM4];
2891
2892(* ----------------------------------------------------------------------
2893 RAT_LE_NUM
2894 ---------------------------------------------------------------------- *)
2895
2896Theorem RAT_LE_NUM2[local]:
2897 -&m <= &n <=> T
2898Proof
2899 simp[rat_leq_def]
2900QED
2901
2902Theorem RAT_LE_NUM3[local]:
2903 &m <= -&n <=> (m = 0) /\ (n = 0)
2904Proof
2905 simp[rat_leq_def]
2906QED
2907
2908Theorem RAT_LE_NUM4[local]:
2909 -&m <= -&n <=> n <= m
2910Proof
2911 simp[rat_leq_def]
2912QED
2913
2914Theorem RAT_LE_NUM_CALCULATE[simp] =
2915 LIST_CONJ [RAT_OF_NUM_LEQ, RAT_LE_NUM2, RAT_LE_NUM3, RAT_LE_NUM4];
2916
2917(* ----------------------------------------------------------------------
2918 rat_of_int
2919 ---------------------------------------------------------------------- *)
2920
2921Definition rat_of_int_def:
2922 rat_of_int i : rat = if i < 0 then - (& (Num (-i))) else &(Num i)
2923End
2924
2925Theorem rat_of_int_11[simp]:
2926 (rat_of_int i1 = rat_of_int i2) <=> (i1 = i2)
2927Proof
2928 Cases_on ‘i1’ >> Cases_on ‘i2’ >> simp[rat_of_int_def]
2929QED
2930
2931Theorem rat_of_int_of_num[simp]: rat_of_int (&x) = &x
2932Proof simp[rat_of_int_def]
2933QED
2934
2935val elim1 = intLib.ARITH_PROVE ``y <= x /\ x <= y ==> (x = y:int)``
2936val elim2 = intLib.ARITH_PROVE ``x:int < y /\ y < x ==> F``
2937fun elim_tac k =
2938 REPEAT_GTCL
2939 (fn ttcl => fn th =>
2940 first_assum (mp_then.mp_then (mp_then.Pos hd) ttcl th))
2941 (k o assert (not o is_imp o #2 o strip_forall o concl))
2942
2943val num_rwt = integerTheory.INT_OF_NUM |> SPEC_ALL |> EQ_IMP_RULE |> #2
2944
2945Theorem rat_of_int_MUL:
2946 rat_of_int x * rat_of_int y = rat_of_int (x * y)
2947Proof
2948 simp[rat_of_int_def, integerTheory.INT_MUL_SIGN_CASES] >> rw[] >>
2949 fs[integerTheory.INT_NOT_LT, RAT_MUL_NUM_CALCULATE, RAT_EQ_NUM_CALCULATE] >>
2950 TRY (elim_tac assume_tac elim1 ORELSE elim_tac assume_tac elim2) >> rw[] >>
2951 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2952 [GSYM integerTheory.INT_INJ, GSYM integerTheory.int_calculate,
2953 num_rwt, integerTheory.INT_LE_MUL, integerTheory.INT_LE_LT,
2954 integerTheory.INT_MUL_SIGN_CASES, integerTheory.INT_NEG_GT0]
2955QED
2956
2957Theorem rat_of_int_ADD:
2958 rat_of_int x + rat_of_int y = rat_of_int (x + y)
2959Proof
2960 simp[rat_of_int_def] >> rw[]
2961 >- (simp[GSYM RAT_AINV_ADD, RAT_ADD_NUM_CALCULATE] >>
2962 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2963 [GSYM integerTheory.INT_INJ, GSYM integerTheory.int_calculate,
2964 num_rwt, integerTheory.INT_LE_MUL, integerTheory.INT_LE_LT,
2965 integerTheory.INT_MUL_SIGN_CASES, integerTheory.INT_NEG_GT0])
2966 >- (full_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [])
2967 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[] >>
2968 TRY (rename [‘Num (-a) <= Num b’] >>
2969 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >>
2970 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt]) >>
2971 rename [‘Num (-a) - Num b’] >>
2972 ‘Num b <= Num (-a)’
2973 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2974 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LE] >>
2975 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2976 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB])
2977 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[]
2978 >- (rename [‘Num (-a) <= Num b’] >>
2979 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >>
2980 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt] >>
2981 `Num (-a) <= Num b`
2982 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2983 [num_rwt, GSYM integerTheory.INT_INJ,
2984 GSYM integerTheory.INT_LE] >>
2985 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2986 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB])
2987 >- (pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >>
2988 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt]))
2989 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[] >>
2990 TRY (rename [‘Num (-a) <= Num b’] >>
2991 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >>
2992 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt]) >>
2993 rename [‘Num (-a) - Num b’] >>
2994 ‘Num b <= Num (-a)’
2995 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2996 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LE] >>
2997 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
2998 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB])
2999 >- (simp[RAT_ADD_NUM_CALCULATE] >> rw[]
3000 >- (rename [‘Num (-a) <= Num b’] >>
3001 pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >>
3002 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt] >>
3003 `Num (-a) <= Num b`
3004 by asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
3005 [num_rwt, GSYM integerTheory.INT_INJ,
3006 GSYM integerTheory.INT_LE] >>
3007 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
3008 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_SUB])
3009 >- (pop_assum (mp_tac o REWRITE_RULE [GSYM integerTheory.INT_LE]) >>
3010 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [num_rwt]))
3011 >- (full_simp_tac (bool_ss ++ intLib.INT_ARITH_ss) [])
3012 >- (simp[RAT_ADD_NUM_CALCULATE] >>
3013 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
3014 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_ADD])
3015QED
3016
3017Theorem rat_of_int_LE[simp]:
3018 rat_of_int i <= rat_of_int j <=> i <= j
3019Proof
3020 simp[rat_of_int_def] >> rw[] >>
3021 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
3022 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LE]
3023QED
3024
3025Theorem rat_of_int_LT[simp]:
3026 rat_of_int i < rat_of_int j <=> i < j
3027Proof
3028 simp[rat_of_int_def] >> rw[] >>
3029 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
3030 [num_rwt, GSYM integerTheory.INT_INJ, GSYM integerTheory.INT_LT]
3031QED
3032
3033Theorem rat_of_int_ainv:
3034 rat_of_int (-i) = -(rat_of_int i)
3035Proof
3036 simp[rat_of_int_def] >> rw[] >>
3037 TRY (elim_tac mp_tac elim2 >> simp[]) >>
3038 asm_simp_tac (bool_ss ++ intLib.INT_ARITH_ss)
3039 [num_rwt, GSYM integerTheory.INT_INJ]
3040QED
3041
3042Theorem RAT_OF_INT_CALCULATE:
3043 !i. rat_of_int i = abs_rat (abs_frac (i, 1))
3044Proof
3045 gen_tac >> Cases_on ‘i’ >> simp[rat_of_int_def]
3046 >- simp[RAT_OF_NUM_CALCULATE]
3047 >- (simp[GSYM fracTheory.FRAC_AINV_CALCULATE, GSYM RAT_AINV_CALCULATE] >>
3048 simp[RAT_OF_NUM_CALCULATE])
3049 >- simp[RAT_OF_NUM_CALCULATE]
3050QED
3051
3052(* ----------------------------------------------------------------------
3053 RATN and RATD, which take rational numbers and return unique
3054 numerator and denominator values. Numerator is integer with smallest
3055 possible absolute value; denominator is a natural number. If
3056 numerator is zero, denominator is always one.
3057 ---------------------------------------------------------------------- *)
3058
3059Theorem frac_exists[local]:
3060 !r. ?n:int d:num. 0 < d /\ (&d * r = rat_of_int n)
3061Proof
3062 gen_tac >>
3063 qabbrev_tac ‘f = rep_rat r’ >>
3064 ‘r = abs_rat f’ by metis_tac[rat_type_thm] >>
3065 ‘?n0 d0. rep_frac f = (n0,d0)’ by (Cases_on ‘rep_frac f’ >> simp[]) >>
3066 map_every qexists_tac [‘n0’, ‘Num d0’] >>
3067 ‘rep_frac (abs_frac (rep_frac f)) = rep_frac f’
3068 by simp [fracTheory.frac_tybij] >>
3069 pop_assum mp_tac >> simp[GSYM (CONJUNCT2 fracTheory.frac_tybij)] >>
3070 strip_tac >> Cases_on ‘d0’ >> fs[] >>
3071 rename [‘rep_frac f = (n,&d)’] >>
3072 simp[RAT_OF_NUM_CALCULATE, RAT_OF_INT_CALCULATE, RAT_MUL_CALCULATE] >>
3073 ‘f = abs_frac (n,&d)’ by metis_tac[fracTheory.frac_tybij] >>
3074 simp[fracTheory.FRAC_MULT_CALCULATE, RAT_ABS_EQUIV] >>
3075 simp[RAT_EQUIV_ALT] >>
3076 map_every qexists_tac [‘1’, ‘&d’] >>
3077 simp[fracTheory.FRAC_MULT_CALCULATE, integerTheory.INT_MUL_COMM]
3078QED
3079
3080Theorem numdenom_exists[local]:
3081 !r:rat.
3082 ?n:int d:num.
3083 (r = rat_of_int n / &d) /\ 0 < d /\ ((n = 0) ==> (d = 1)) /\
3084 !n' d'. (r = rat_of_int n' / &d') /\ 0 < d' ==> ABS n <= ABS n'
3085Proof
3086 gen_tac >>
3087 qabbrev_tac `reps = { (a,b) | (&b * r = rat_of_int a) /\ 0 < b }` >>
3088 `WF (measure (Num o ABS o (FST : int # num -> int)))` by simp[] >>
3089 full_simp_tac bool_ss [relationTheory.WF_DEF] >>
3090 ‘?e. reps e’
3091 by (simp[Abbr‘reps’, pairTheory.EXISTS_PROD] >> metis_tac[frac_exists]) >>
3092 fs[PULL_EXISTS] >>
3093 Cases_on ‘r = 0’
3094 >- (map_every qexists_tac [‘0’, ‘1’] >> simp[] >> gen_tac >> Cases_on ‘n'’ >>
3095 simp[integerTheory.INT_ABS_NUM, integerTheory.INT_ABS_NEG]) >>
3096 res_tac >>
3097 ‘?mn md. min = (mn,md)’ by (Cases_on ‘min’ >> simp[]) >> rw[] >>
3098 map_every qexists_tac [‘mn’, ‘md’] >> fs[Abbr‘reps’] >> pairarg_tac >>
3099 fs[pairTheory.FORALL_PROD] >> rpt var_eq_tac >>
3100 qpat_x_assum ‘(_,_) = _’ kall_tac >> rpt conj_tac
3101 >- (rename [‘&d * r = rat_of_int n’] >> first_x_assum (SUBST1_TAC o SYM) >>
3102 simp[RAT_DIV_MULMINV] >>
3103 ‘&d:rat <> 0’ by simp[] >>
3104 metis_tac[RAT_MUL_ASSOC, RAT_MUL_COMM, RAT_MUL_RINV, RAT_MUL_LID])
3105 >- (rename [‘(_ = 0) ==> (_ = 1)’] >> strip_tac >> fs[])
3106 >- (rpt strip_tac >>
3107 rename [‘&d * r = rat_of_int n’, ‘r = rat_of_int nn / &dd’] >>
3108 spose_not_then (assume_tac o REWRITE_RULE[integerTheory.INT_NOT_LE]) >>
3109 first_x_assum (qspecl_then [‘nn’, ‘dd’] mp_tac) >> simp[] >>
3110 reverse conj_tac
3111 >- (‘&dd <> 0’ by simp[] >> simp[RAT_DIV_MULMINV] >>
3112 metis_tac[RAT_MUL_ASSOC, RAT_MUL_COMM, RAT_MUL_RINV, RAT_MUL_LID]) >>
3113 simp[NUM_LT])
3114QED
3115
3116val RATND_THM = new_specification("RATND_THM", ["RATN", "RATD"],
3117 CONV_RULE (SKOLEM_CONV THENC BINDER_CONV SKOLEM_CONV) numdenom_exists)
3118
3119Theorem RATD_NZERO[simp] = (
3120 let val th = List.nth(RATND_THM |> SPEC_ALL |> CONJUNCTS, 1)
3121 in
3122 CONJ th (CONV_RULE (REWR_CONV (GSYM NOT_ZERO_LT_ZERO)) th)
3123 end)
3124
3125Theorem RATN_LEAST =
3126 List.nth(RATND_THM |> SPEC_ALL |> CONJUNCTS, 3)
3127
3128Theorem RATN_RATD_EQ_THM =
3129 RATND_THM |> SPEC_ALL |> CONJUNCTS |> hd;
3130
3131Theorem RATN_RATD_MULT =
3132 RATN_RATD_EQ_THM |> Q.AP_TERM ‘\x. x * &RATD r’ |> BETA_RULE
3133 |> SIMP_RULE (srw_ss()) [RAT_DIV_MULMINV, GSYM RAT_MUL_ASSOC,
3134 RAT_MUL_LINV];
3135
3136Theorem RATND_RAT_OF_NUM[simp]:
3137 (RATN (&n) = &n) /\ (RATD (&n) = 1)
3138Proof
3139 mp_tac (Q.INST [`r` |-> `&n`] RATN_RATD_MULT) >> strip_tac >>
3140 ‘&n:rat = rat_of_int (&n) / 1’ by simp[] >>
3141 ‘ABS (RATN (&n)) <= ABS (&n)’ by metis_tac[RATN_LEAST, DECIDE ``0n < 1``] >>
3142 full_simp_tac bool_ss [integerTheory.INT_ABS_NUM, GSYM rat_of_int_of_num,
3143 rat_of_int_MUL, rat_of_int_11,
3144 integerTheory.INT_MUL] >>
3145 fs[] >>
3146 ‘?rn. RATN (&n) = &rn’ by (Cases_on ‘RATN (&n)’ >> fs[]) >>
3147 fs[integerTheory.INT_ABS_NUM] >>
3148 conj_asm1_tac
3149 >- (‘n <= rn’ suffices_by simp[] >>
3150 Cases_on ‘RATD(&n)’ >> fs[MULT_CLAUSES]) >> rpt var_eq_tac >>
3151 ‘(RATD(&n) = 1) \/ (n = 0)’ by metis_tac[MULT_RIGHT_1,EQ_MULT_LCANCEL] >>
3152 metis_tac[RATND_THM]
3153QED
3154
3155Theorem RATN_EQ0[simp]:
3156 ((RATN r = 0) <=> (r = 0)) /\ ((0 = RATN r) <=> (r = 0))
3157Proof
3158 reverse conj_asm1_tac >- metis_tac[] >>
3159 simp[EQ_IMP_THM] >> strip_tac >>
3160 mp_tac RATN_RATD_MULT >> simp[]
3161QED
3162
3163Theorem RATN_SIGN[simp]:
3164 (0 < RATN x <=> 0 < x) /\ (0 <= RATN x <=> 0 <= x) /\ (RATN x < 0 <=> x < 0) /\
3165 (RATN x <= 0 <=> x <= 0)
3166Proof
3167 reverse conj_asm1_tac
3168 >- (simp[integerTheory.INT_LE_LT, rat_leq_def, EQ_SYM_EQ] >>
3169 conj_tac >> ONCE_REWRITE_TAC [DECIDE ``(p:bool = q) = (~p = ~q)``] >>
3170 ASM_REWRITE_TAC [integerTheory.INT_NOT_LT, integerTheory.INT_LE_LT, RAT_LEQ_LES,
3171 rat_leq_def, DE_MORGAN_THM] >> simp[] >> metis_tac[]) >>
3172 eq_tac >> strip_tac >> mp_tac (Q.INST [`r` |-> `x`] RATN_RATD_MULT)
3173 >- (‘0 < rat_of_int (RATN x)’
3174 by asm_simp_tac bool_ss [GSYM rat_of_int_of_num, rat_of_int_LT] >>
3175 strip_tac >>
3176 ‘0 < x * &RATD x’ by metis_tac[] >>
3177 pop_assum mp_tac >> simp[RAT_MUL_SIGN_CASES]) >>
3178 ‘0 < x * &RATD x’ by simp[RAT_MUL_SIGN_CASES] >> strip_tac >>
3179 ‘0 < rat_of_int (RATN x)’ by metis_tac[] >>
3180 full_simp_tac bool_ss [GSYM rat_of_int_of_num, rat_of_int_LT]
3181QED
3182
3183val RATN_MUL_LEAST =
3184 SIMP_RULE (srw_ss() ++ boolSimps.CONJ_ss ++ ARITH_ss) [RAT_RDIV_EQ] RATN_LEAST;
3185
3186Theorem RAT_AINV_SGN[simp]:
3187 (0 < -r <=> r < 0) /\ (-r < 0 <=> 0 < r)
3188Proof
3189 metis_tac[RAT_LES_AINV, RAT_AINV_0]
3190QED
3191
3192Theorem RATN_NEG[simp]:
3193 RATN (-r) = -RATN r
3194Proof
3195 assume_tac RATN_RATD_MULT >> assume_tac (Q.INST [`r` |-> `-r`] RATN_RATD_MULT) >>
3196 first_assum (mp_tac o Q.AP_TERM `rat_ainv`) >>
3197 REWRITE_TAC[RAT_AINV_LMUL] >> simp[] >> strip_tac >>
3198 ‘ABS (RATN r) <= ABS (-RATN (-r))’
3199 by (irule RATN_MUL_LEAST >> qexists_tac ‘&RATD (-r)’ >> simp[rat_of_int_ainv]) >>
3200 fs[] >>
3201 last_assum (mp_tac o Q.AP_TERM `rat_ainv`) >>
3202 REWRITE_TAC[RAT_AINV_LMUL] >> simp[] >> strip_tac >>
3203 ‘ABS (RATN (-r)) <= ABS (-RATN (r))’
3204 by (irule RATN_MUL_LEAST >> qexists_tac ‘&RATD r’ >> simp[rat_of_int_ainv]) >>
3205 fs[] >>
3206 ‘ABS (RATN (-r)) = ABS (RATN r)’ by metis_tac[INT_LE_ANTISYM] >>
3207 fs[INT_ABS_EQ_ABS] >> fs[] >>
3208 ‘r * &RATD r = -r * &RATD (-r)’ by simp[] >> pop_assum mp_tac >>
3209 rpt (pop_assum kall_tac) >> strip_tac >>
3210 qspecl_then [‘0’, ‘r’] strip_assume_tac RAT_LES_TOTAL
3211 >- (‘0 < r * &RATD r’ by simp[RAT_MUL_SIGN_CASES] >>
3212 ‘~(0 < -r * &RATD (-r))’
3213 by (simp[RAT_MUL_SIGN_CASES] >> metis_tac[RAT_LES_REF, RAT_LES_TRANS]) >>
3214 metis_tac[])
3215 >- simp[]
3216 >- (‘r * &RATD r < 0’ by simp[RAT_MUL_SIGN_CASES] >>
3217 ‘~(-r * &RATD(-r) < 0)’
3218 by (simp[RAT_MUL_SIGN_CASES] >> metis_tac[RAT_LES_REF, RAT_LES_TRANS]) >>
3219 metis_tac[])
3220QED
3221
3222Theorem RATD_NEG[simp]:
3223 RATD (-r) = RATD r
3224Proof
3225 Cases_on ‘r = 0’ >> fs[] >>
3226 assume_tac RATN_RATD_MULT >> assume_tac (Q.INST [`r` |-> `-r`] RATN_RATD_MULT) >> fs[] >>
3227 pop_assum (mp_tac o Q.AP_TERM ‘rat_ainv’) >> REWRITE_TAC [RAT_AINV_LMUL] >>
3228 simp[rat_of_int_ainv] >> metis_tac[RAT_EQ_LMUL, RAT_EQ_NUM_CALCULATE]
3229QED
3230
3231Theorem RATN_RATD_RAT_OF_INT[simp]:
3232 (RATN (rat_of_int i) = i) /\ (RATD (rat_of_int i) = 1)
3233Proof
3234 Cases_on ‘i’ >> simp[rat_of_int_ainv]
3235QED
3236
3237Theorem RATN_DIV_RATD[simp]:
3238 rat_of_int (RATN r) / &RATD r = r
3239Proof
3240 ONCE_REWRITE_TAC [EQ_SYM_EQ] >> simp[RAT_RDIV_EQ, RATN_RATD_MULT]
3241QED
3242
3243Theorem RAT_AINV_EQ_NUM[simp]:
3244 (rat_ainv x = rat_of_num n) <=> (x = rat_of_int (-&n))
3245Proof
3246 simp[EQ_IMP_THM, rat_of_int_ainv] >> disch_then (SUBST1_TAC o SYM) >> simp[]
3247QED
3248
3249(* ----------------------------------------------------------------------
3250 more theorems about RAT_SGN : rat -> int (-1,0,1)
3251 ---------------------------------------------------------------------- *)
3252
3253Overload RAT_SGN[local] = ``rat_sgn``
3254Theorem RAT_SGN_NUM_COND:
3255 rat_sgn (&n) = if n = 0 then 0 else 1
3256Proof
3257 rw[] >> `0 < n` by simp[] >>
3258 `0 < &n` by simp[] >>
3259 pop_assum (mp_tac o REWRITE_RULE [rat_les_def]) >> simp[]
3260QED
3261
3262Theorem RAT_SGN_AINV_RWT[simp]:
3263 rat_sgn (-r) = -rat_sgn r
3264Proof
3265 simp[SimpLHS, Once (GSYM RAT_SGN_AINV)]
3266QED
3267
3268Theorem RAT_SGN_ALT:
3269 rat_sgn r = SGN (RATN r)
3270Proof
3271 assume_tac RATN_RATD_EQ_THM >>
3272 map_every qabbrev_tac [`n = RATN r`, `nr = rat_of_int n`, `d = &(RATD r)`] >>
3273 `d <> 0` by simp[Abbr`d`] >>
3274 simp[RAT_DIV_MULMINV, RAT_SGN_MUL, RAT_SGN_MINV] >>
3275 `d > 0` by simp[Abbr`d`, rat_gre_def] >>
3276 `rat_sgn d = 1` by metis_tac[RAT_SGN_CLAUSES] >> simp[] >>
3277 simp[Abbr`nr`, rat_of_int_def, SGN_def] >> Cases_on `n = 0` >> simp[] >>
3278 rw[] >> rw[RAT_SGN_NUM_COND] >>
3279 Cases_on `n` >> fs[]
3280QED
3281
3282Theorem RAT_SGN_NUM_BITs[simp]:
3283 (rat_sgn (&(NUMERAL (BIT1 n))) = 1) /\ (rat_sgn (&(NUMERAL (BIT2 n))) = 1)
3284Proof
3285 REWRITE_TAC[arithmeticTheory.BIT1, arithmeticTheory.BIT2,
3286 arithmeticTheory.NUMERAL_DEF, arithmeticTheory.ALT_ZERO] >>
3287 simp[RAT_SGN_NUM_COND]
3288QED
3289
3290Theorem RAT_SGN_EQ0[simp]:
3291 ((rat_sgn r = 0) <=> (r = 0)) /\ ((0 = rat_sgn r) <=> (r = 0))
3292Proof
3293 metis_tac[RAT_SGN_CLAUSES]
3294QED
3295
3296Theorem RAT_SGN_POS[simp]:
3297 (rat_sgn r = 1) <=> 0 < r
3298Proof
3299 rw[RAT_SGN_CLAUSES, rat_gre_def]
3300QED
3301
3302Theorem RAT_SGN_NEG[simp]:
3303 (rat_sgn r = -1) <=> r < 0
3304Proof
3305 rw[RAT_SGN_CLAUSES]
3306QED
3307
3308Theorem RAT_SGN_DIV[simp]:
3309 d <> 0 ==> (rat_sgn (n/d) = rat_sgn n * rat_sgn d)
3310Proof
3311 simp[RAT_SGN_MINV, RAT_DIV_MULMINV]
3312QED
3313
3314Theorem RAT_MINV_RATND:
3315 r <> 0 ==>
3316 (rat_minv r =
3317 (rat_of_int (rat_sgn r) * &RATD r) / rat_of_int (ABS (RATN r)))
3318Proof
3319 assume_tac (SYM RATN_DIV_RATD) >>
3320 map_every qabbrev_tac [‘n = RATN r’, ‘d = RATD r’] >>
3321 first_x_assum SUBST1_TAC >> ‘0 < d’ by simp[Abbr‘d’] >> simp[RAT_DIV_EQ0] >>
3322 simp[RAT_SGN_NUM_COND] >> Cases_on ‘n’ >>
3323 simp[RAT_DIV_MINV, rat_of_int_ainv, RAT_SGN_NUM_COND] >>
3324 simp[RAT_DIV_MULMINV, GSYM RAT_AINV_MINV, GSYM RAT_AINV_LMUL,
3325 GSYM RAT_AINV_RMUL]
3326QED
3327
3328(* ----------------------------------------------------------------------
3329 relating RAT{N,D} back to abs_frac etc
3330 ---------------------------------------------------------------------- *)
3331
3332Theorem rat_of_int_EQN[simp]:
3333 ((rat_of_int i = &n) <=> (i = &n)) /\
3334 ((&n = rat_of_int i) <=> (i = &n))
3335Proof
3336 Cases_on ‘i’ >> simp[rat_of_int_def]
3337QED
3338
3339Theorem frac_dnm_EQ0[simp]:
3340 frac_dnm f <> 0
3341Proof
3342 metis_tac[INT_LT_REFL, FRAC_DNMPOS]
3343QED
3344
3345Theorem rep_rat_of_int:
3346 !i. ?j. 0 < j /\ (rep_rat (rat_of_int i) = abs_frac (j * i, j))
3347Proof
3348 gen_tac >> simp[FRAC_EQ_ALT, SF CONJ_ss, NMR, DNM, FRAC_DNMPOS] >>
3349 qabbrev_tac ‘IR = rep_rat (rat_of_int i)’ >>
3350 ‘rat_equiv (abs_frac (i,1)) IR’
3351 by (simp[RAT_OF_INT_CALCULATE, Abbr‘IR’] >>
3352 metis_tac[RAT_EQUIV_SYM, rat_equiv_rep_abs]) >>
3353 gs[rat_equiv_def, NMR, DNM] >> metis_tac[INT_MUL_COMM]
3354QED
3355
3356Theorem rat_of_int_nmrdnm:
3357 rat_of_int (frac_nmr (rep_rat q)) / rat_of_int (frac_dnm (rep_rat q)) = q
3358Proof
3359 simp[RAT_OF_INT_CALCULATE, RAT_DIV_CALCULATE, NMR] >>
3360 simp[frac_div_def, frac_mul_def, NMR, DNM, frac_minv_def, frac_sgn_def] >>
3361 ‘q = abs_rat (rep_rat q)’ by simp[rat_type_thm] >>
3362 pop_assum (fn th => simp[Once th, SimpRHS]) >>
3363 irule $ iffLR $ cj 2 rat_type_thm >>
3364 simp[rat_equiv_def, NMR, DNM] >>
3365 simp[ABS_EQ_MUL_SGN, AC INT_MUL_ASSOC INT_MUL_COMM]
3366QED
3367
3368Theorem RAT_DIVMUL_CANCEL:
3369 d <> 0 ==> (n / d * d = n)
3370Proof
3371 simp[LDIV_MUL_OUT, RAT_LDIV_EQ] >> simp[AC RAT_MUL_COMM RAT_MUL_ASSOC]
3372QED
3373
3374Theorem ABS_RATFRAC_DIV:
3375 0 < d ==> (abs_rat (abs_frac (n, d)) = rat_of_int n / rat_of_int d)
3376Proof
3377 rw[rat_div_def, frac_div_def, frac_mul_def, frac_minv_def, DNM, NMR,
3378 frac_sgn_def, RAT_NMREQ0_CONG, RAT_OF_INT_CALCULATE,
3379 intLib.ARITH_PROVE “0i < d ==> d <> 0”, RAT_EQ, INT_MUL_SIGN_CASES,
3380 FRAC_DNMPOS] >>
3381 simp[ABS_EQ_MUL_SGN, AC INT_MUL_ASSOC INT_MUL_COMM] >>
3382 simp[GSYM RAT_OF_INT_CALCULATE, INT_MUL_ASSOC, INT_EQ_RMUL,
3383 INT_SGN_CLAUSES] >>
3384 ‘(?dj. 0 < dj /\ (rep_rat (rat_of_int d) = abs_frac(dj * d, dj))) /\
3385 (?nj. 0 < nj /\ (rep_rat (rat_of_int n) = abs_frac(nj * n, nj)))’
3386 by metis_tac[rep_rat_of_int] >>
3387 simp[NMR, DNM] >>
3388 simp[AC INT_MUL_COMM INT_MUL_ASSOC]
3389QED
3390
3391Theorem ABS_RATFRAC_RATND:
3392 abs_rat (abs_frac (RATN q, &RATD q)) = q
3393Proof
3394 simp[ABS_RATFRAC_DIV]
3395QED
3396
3397(* ----------------------------------------------------------------------
3398 Further characterisation of RAT{N,D}
3399 ---------------------------------------------------------------------- *)
3400
3401Theorem nmr_dnm_unique[local]:
3402 gcd n1 d1 = 1 /\ gcd n2 d2 = 1 /\
3403 n1 * d2 = n2 * d1
3404 ==> n1 = n2 /\ d1 = d2
3405Proof
3406 strip_tac >> imp_res_tac gcdTheory.divides_coprime_mul >> gvs[] >>
3407 first_x_assum $ qspec_then `n2` $ mp_tac o iffLR >> gvs[] >>
3408 impl_tac >- (gvs[dividesTheory.divides_def] >> qexists `d2` >> gvs[]) >>
3409 strip_tac >> first_x_assum $ qspec_then `n1` assume_tac >> gvs[] >>
3410 dxrule_all dividesTheory.DIVIDES_ANTISYM >> strip_tac >> gvs[]
3411QED
3412
3413Theorem gcd_RATND[simp]:
3414 gcd (Num $ RATN r) (RATD r) = 1
3415Proof
3416 CCONTR_TAC >> gvs[] >>
3417 qmatch_asmsub_abbrev_tac `gcd n d` >>
3418 `d <> 0` by (unabbrev_all_tac >> gvs[]) >>
3419 qspecl_then [`n`,`d`] assume_tac gcdTheory.FACTOR_OUT_GCD >> gvs[] >>
3420 Cases_on `n = 0` >> gvs[] >>
3421 qspecl_then [`rat_sgn r * &p`,`q`] mp_tac RATN_LEAST >> simp[] >>
3422 Cases_on `q = 0` >> gvs[] >> reverse $ rw[]
3423 >- (
3424 simp[RAT_SGN_ALT, GSYM INT_ABS_MUL, ABS_SGN] >>
3425 Cases_on `r = 0` >> gvs[] >>
3426 `ABS (RATN r) = &n` by (unabbrev_all_tac >> Cases_on `RATN r` >> gvs[]) >>
3427 simp[] >> qpat_assum `n = _` SUBST1_TAC >> simp[] >>
3428 Cases_on `p = 0` >> gvs[] >> simp[NOT_LESS_EQUAL] >>
3429 Cases_on `gcd n d = 0` >- gvs[] >- simp[]
3430 ) >>
3431 rewrite_tac[Once RATN_RATD_EQ_THM] >>
3432 dep_rewrite.DEP_REWRITE_TAC[RAT_LDIV_EQ] >> simp[] >>
3433 simp[RDIV_MUL_OUT] >> dep_rewrite.DEP_REWRITE_TAC[RAT_RDIV_EQ] >> simp[] >>
3434 `RATN r = rat_sgn r * &n` by (simp[RAT_SGN_ALT] >> unabbrev_all_tac >> gvs[]) >>
3435 simp[GSYM rat_of_int_MUL, AC RAT_MUL_ASSOC RAT_MUL_COMM] >>
3436 simp[RAT_MUL_ASSOC] >> rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >>
3437 simp[RAT_MUL_NUM_CALCULATE] >>
3438 qsuff_tac `(p * gcd n d) * q = (q * gcd n d) * p`
3439 >- metis_tac[]
3440 >- simp[]
3441QED
3442
3443Theorem RATND_suff_eq:
3444 gcd (Num n) d = 1 /\ d <> 0
3445 ==> RATN (rat_of_int n / &d) = n /\ RATD (rat_of_int n / &d) = d
3446Proof
3447 strip_tac >>
3448 qpat_abbrev_tac `r = _ / _` >>
3449 qsuff_tac `rat_sgn r = SGN n /\ Num (RATN r) = Num n /\ RATD r = d`
3450 >- (rw[RAT_SGN_ALT] >> once_rewrite_tac[GSYM SGN_MUL_Num] >> metis_tac[]) >>
3451 conj_asm1_tac
3452 >- (
3453 unabbrev_all_tac >> simp[RAT_SGN_ALT, intExtensionTheory.SGN_def] >>
3454 Cases_on `n` >> gvs[] >> simp[rat_of_int_ainv]
3455 ) >>
3456 `rat_of_int n * &RATD r = rat_of_int (RATN r) * &d` by (
3457 dep_rewrite.DEP_REWRITE_TAC[GSYM RAT_RDIV_EQ] >> simp[] >>
3458 simp[GSYM LDIV_MUL_OUT] >> rewrite_tac[Once RAT_MUL_COMM] >>
3459 dep_rewrite.DEP_REWRITE_TAC[GSYM RAT_LDIV_EQ] >> unabbrev_all_tac >> gvs[]) >>
3460 pop_assum mp_tac >> simp[rat_of_int_def] >>
3461 `n < 0 <=> r < 0` by (
3462 unabbrev_all_tac >> gvs[RAT_LDIV_LES_POS] >>
3463 Cases_on `n` >> gvs[] >> simp[rat_of_int_ainv]) >>
3464 IF_CASES_TAC >> gvs[Num_neg] >>
3465 simp[RAT_MUL_NUM_CALCULATE] >> strip_tac >> irule nmr_dnm_unique >> simp[]
3466QED
3467
3468(* This is another form of RATND_suff_eq using only natural numbers *)
3469Theorem RATND_of_coprimes :
3470 !p q. gcd p q = 1 /\ q <> 0 ==> RATN (&p / &q) = &p /\ RATD (&p / &q) = q
3471Proof
3472 rpt GEN_TAC >> STRIP_TAC
3473 >> qabbrev_tac ‘n = int_of_num p’
3474 >> ‘&p = rat_of_int n’ by rw [rat_of_int_def]
3475 >> ‘gcd (Num n) q = 1’ by rw [Abbr ‘n’]
3476 >> rw [RATND_suff_eq]
3477QED
3478
3479Theorem RATND_of_coprimes' :
3480 !p q. gcd p q = 1 /\ q <> 0 ==> RATN (-&p / &q) = -&p /\ RATD (-&p / &q) = q
3481Proof
3482 rw [GSYM RAT_DIV_AINV, RATND_of_coprimes]
3483QED
3484
3485Definition div_gcd_def:
3486 div_gcd a b =
3487 let d = gcd (Num a) b in
3488 if d = 0 \/ d = 1 then (a, b) else (a / &d, b DIV d)
3489End
3490
3491Theorem div_gcd_reduces:
3492 div_gcd a b = (n,d) /\ b <> 0 ==> d <> 0 /\ gcd (Num n) d = 1 /\ a * &d = n * &b
3493Proof
3494 rw[div_gcd_def] >> gvs[]
3495 >- (
3496 Cases_on `b = 1` >> gvs[] >>
3497 dep_rewrite.DEP_REWRITE_TAC[DIV_EQ_0] >> simp[NOT_LESS] >>
3498 Cases_on `gcd (Num a) b` >> gvs[] >>
3499 qspecl_then [`Num a`,`b`] assume_tac gcdTheory.gcd_LESS_EQ >> gvs[]
3500 )
3501 >- (
3502 Cases_on `Num a = 0` >> simp[] >>
3503 qspecl_then [`Num a`,`b`] assume_tac gcdTheory.FACTOR_OUT_GCD >> gvs[] >>
3504 qsuff_tac `b DIV gcd (Num a) b = q /\ Num (a / &gcd (Num a) b) = p` >> rw[]
3505 >- (
3506 qpat_x_assum `b = _` $ simp o single o Once >>
3507 irule MULT_DIV >> Cases_on `gcd (Num a) b` >> gvs[]
3508 ) >>
3509 simp[int_div] >> rw[] >> gvs[Num_neg]
3510 >- (
3511 qpat_x_assum `Num a = _` $ simp o single o Once >>
3512 irule MULT_DIV >> Cases_on `gcd (Num a) b` >> gvs[]
3513 )
3514 >- (
3515 qpat_x_assum `Num a = _` $ simp o single o Once >>
3516 irule MULT_DIV >> Cases_on `gcd (Num a) b` >> gvs[]
3517 )
3518 >- (
3519 irule FALSITY >> pop_assum mp_tac >> simp[] >>
3520 qpat_x_assum `Num a = _` $ rewrite_tac o single o Once >>
3521 irule MOD_EQ_0 >> simp[]
3522 )
3523 )
3524 >- (
3525 qspecl_then [`Num a`,`b`] assume_tac gcdTheory.FACTOR_OUT_GCD >>
3526 Cases_on `a = 0` >> gvs[] >>
3527 qabbrev_tac `g = gcd (Num a) b` >>
3528 `b DIV g = q` by (irule DIV_UNIQUE >> qexists `0` >> gvs[]) >>
3529 `a / &g = SGN a * &p` by (
3530 qspec_then `a` mp_tac $ GEN_ALL (GSYM SGN_MUL_Num) >>
3531 disch_then $ rewrite_tac o single o Once >>
3532 dep_rewrite.DEP_REWRITE_TAC[INT_MUL_DIV] >> conj_tac >- gvs[] >>
3533 AP_TERM_TAC >> gvs[INT_DIV_CALCULATE] >>
3534 rewrite_tac[Once MULT_COMM] >> irule MULT_DIV >> gvs[]) >>
3535 simp[] >>
3536 qspec_then `a` mp_tac $ GEN_ALL (GSYM SGN_MUL_Num) >>
3537 disch_then $ rewrite_tac o single o Once >>
3538 once_rewrite_tac[GSYM INT_MUL_ASSOC] >>
3539 AP_TERM_TAC >> simp[INT_MUL_CALCULATE]
3540 )
3541QED
3542
3543Theorem div_gcd_correct:
3544 div_gcd a b = (n,d) /\ b <> 0 ==>
3545 rat_of_int a / &b = rat_of_int n / &d /\
3546 RATN (rat_of_int a / &b) = n /\
3547 RATD (rat_of_int a / &b) = d
3548Proof
3549 strip_tac >> reverse conj_asm1_tac
3550 >- (
3551 pop_assum SUBST_ALL_TAC >> match_mp_tac RATND_suff_eq >>
3552 imp_res_tac div_gcd_reduces >> simp[]
3553 ) >>
3554 simp[RAT_LDIV_EQ, RDIV_MUL_OUT] >>
3555 dep_rewrite.DEP_REWRITE_TAC[RAT_RDIV_EQ] >> simp[] >>
3556 once_rewrite_tac[GSYM rat_of_int_of_num] >> simp[rat_of_int_MUL] >>
3557 imp_res_tac div_gcd_reduces >> gvs[] >>
3558 gvs[AC INT_MUL_ASSOC INT_MUL_COMM]
3559QED
3560
3561(* ----------------------------------------------------------------------
3562 rational min and max
3563 ---------------------------------------------------------------------- *)
3564
3565Definition rat_min_def: rat_min (r1:rat) r2 = if r1 < r2 then r1 else r2
3566End
3567Definition rat_max_def: rat_max (r1:rat) r2 = if r1 > r2 then r1 else r2
3568End
3569
3570
3571Theorem RAT_DENSE_THM:
3572 !r1 r3. r1 < r3 ==> ?r2. r1 < r2 /\ r2 < r3
3573Proof
3574 rpt strip_tac >>
3575 qexists ‘(r1 + r3) / 2’ >>
3576 simp[RAT_RDIV_LES_POS, RAT_LDIV_LES_POS, RAT_TIMES2] >>
3577 ONCE_REWRITE_TAC[RAT_MUL_COMM] >>
3578 simp[RAT_TIMES2, RAT_LES_LADD, RAT_LES_RADD]
3579QED
3580
3581(* ----------------------------------------------------------------------
3582 rational exponentiation
3583
3584 with natural number and integer exponents
3585 ---------------------------------------------------------------------- *)
3586
3587Definition rat_expn_def:
3588 rat_expn (r:rat) 0 = (1:rat) /\
3589 rat_expn r (SUC n) = r * rat_expn r n
3590End
3591
3592Overload expn[local] = “rat_expn”
3593
3594Theorem RAT_EXPN_ADD:
3595 expn r (a+b) = expn r a * expn r b
3596Proof
3597 Induct_on ‘b’
3598 >> simp[GSYM ADD_SUC, AC RAT_MUL_ASSOC RAT_MUL_COMM,rat_expn_def]
3599QED
3600
3601Theorem RAT_EXPN_MUL:
3602 expn r (a*b) = expn (expn r a) b
3603Proof
3604 Induct_on ‘b’
3605 >> simp[MULT_SUC,rat_expn_def,RAT_EXPN_ADD]
3606QED
3607
3608Theorem RAT_EXPN_R_NONZERO:
3609 r <> 0 ==> expn r n <> 0
3610Proof
3611 rw[] >> Induct_on ‘n’ >> simp[rat_expn_def]
3612QED
3613
3614Theorem RAT_EXPN_R_POS:
3615 0<r ==> 0 < expn r n
3616Proof
3617 rw[] >> Induct_on ‘n’ >> simp[rat_expn_def,RAT_MUL_SIGN_CASES]
3618QED
3619
3620Theorem RAT_EXPN_SUB:
3621 r<> 0 /\ b <= a ==> expn r (a - b) = expn r a / expn r b
3622Proof
3623 rw[] >> ‘expn r a = expn r (a - b) * expn r b’ by simp[GSYM RAT_EXPN_ADD]
3624 >> simp[RAT_MUL_RINV,GSYM RAT_MUL_ASSOC,RAT_EXPN_R_NONZERO,RAT_DIV_MULMINV]
3625QED
3626
3627Theorem RAT_EXPN_1:
3628 expn 1 n = 1
3629Proof
3630 Induct_on ‘n’ >> simp[rat_expn_def]
3631QED
3632
3633Theorem RAT_EXPN_0:
3634 !n. (0<n ==> expn 0 n = 0) /\ expn 0 (SUC n) = 0
3635Proof
3636 CONV_TAC FORALL_AND_CONV >> conj_asm2_tac
3637 >- metis_tac[num_CASES,prim_recTheory.LESS_NOT_EQ]
3638 >- (once_rewrite_tac[rat_expn_def] >> simp[MULT])
3639QED
3640
3641Theorem RAT_EXPN_TO_0:
3642 expn r 0 = 1
3643Proof
3644 simp[rat_expn_def]
3645QED
3646
3647Theorem RAT_EXPN_TO_1:
3648 expn r 1 = r
3649Proof
3650 once_rewrite_tac[ONE] >> simp[rat_expn_def]
3651QED
3652
3653Theorem RAT_EXPN_PROD:
3654 expn (a*b) n = expn a n * expn b n
3655Proof
3656 Induct_on ‘n’ >> simp[rat_expn_def,AC RAT_MUL_ASSOC RAT_MUL_COMM]
3657QED
3658
3659Theorem RAT_EXPN_DIV:
3660 b<>0 ==> expn (a/b) n = expn a n / expn b n
3661Proof
3662 rw[] >> Induct_on ‘n’ >> simp[rat_expn_def,RAT_DIVDIV_MUL,RAT_EXPN_R_NONZERO]
3663QED
3664
3665Theorem RAT_EXPN_RAT_MINV:
3666 r<>0 ==> expn (rat_minv r) n = rat_minv (expn r n)
3667Proof
3668 Induct_on ‘n’
3669 >- simp[rat_expn_def]
3670 >- simp[RAT_EXPN_ADD,ADD1,RAT_MINV_MUL,RAT_EXPN_R_NONZERO,rat_expn_def,
3671 RAT_EXPN_TO_1]
3672QED
3673
3674Theorem RAT_EXPN_EQ0[simp]:
3675 expn r n = 0 <=> r = 0 /\ n <> 0
3676Proof
3677 Induct_on ‘n’ >> simp[rat_expn_def] >> simp[EQ_IMP_THM, DISJ_IMP_THM]
3678QED
3679
3680Theorem RAT_EXPN_CALCULATE:
3681 (expn r n = 0 <=> r = 0 /\ n <> 0) /\ expn 1 n = 1 /\ expn r 0 = 1 /\
3682 expn r 1 = r
3683Proof
3684 simp[RAT_EXPN_1,RAT_EXPN_TO_0,RAT_EXPN_TO_1]
3685QED
3686
3687Theorem RAT_EXPN_MINUS1:
3688 expn (-1) n = if EVEN n then 1 else -1
3689Proof
3690 Induct_on ‘n’
3691 >- simp[rat_expn_def]
3692 >- rw[rat_expn_def,EVEN,RAT_MUL_NUM_CALCULATE,RAT_MUL_RID]
3693QED
3694
3695
3696Theorem RAT_AINV_MUL_AINV:
3697 -1 * r:rat = -r
3698Proof
3699 ‘r + -r = 0’ by simp[RAT_ADD_RINV]
3700 >> ‘r + -1 * r = 0’
3701 by metis_tac[RAT_MUL_LID,RAT_RDISTRIB,RAT_ADD_RINV,RAT_MUL_LZERO]
3702 >> metis_tac[RAT_EQ_LADD]
3703QED
3704
3705Theorem RAT_EXPN_NEG:
3706 expn (-r) n = if EVEN n then expn r n else -expn r n
3707Proof
3708 rw[Once $ GSYM RAT_AINV_MUL_AINV,RAT_EXPN_PROD,RAT_EXPN_MINUS1] >>
3709 simp[RAT_AINV_MUL_AINV]
3710QED
3711
3712Theorem LT_MUL:
3713 a<b /\ (c<d \/ c<=d /\ d<>0) ==> a*c < b*d:num
3714Proof
3715 rw[] >> (Cases_on ‘a’ >> Cases_on ‘c’
3716 >- simp[]
3717 >- simp[]
3718 >- simp[]
3719 >- (‘SUC n * SUC n' < b * SUC n'’ by simp[]
3720 >> ‘b * SUC n' <= b*d’ by simp[]
3721 >> simp[])
3722 )
3723QED
3724
3725Theorem RAT_LT_MUL:
3726 0<a /\ a<c /\ 0<b /\ b<d ==> a*b < c*d
3727Proof
3728 metis_tac[RAT_LES_TRANS,RAT_LES_RMUL_POS,RAT_LES_LMUL_POS]
3729QED
3730
3731Theorem RAT_LT_LE_NEQ:
3732 a<b <=> a <= b /\ a<>b
3733Proof
3734 rw[rat_leq_def] >> iff_tac >> simp[RAT_LES_REF] >> metis_tac[RAT_LES_REF]
3735QED
3736
3737Theorem RAT_LEQ_MUL:
3738 0 <= a /\ a <= b /\ 0 <= c /\ c <= d ==> a*c <= b*d
3739Proof
3740 rw[] >> Cases_on ‘a=b’ >> Cases_on ‘c=d’ >> gvs[RAT_LEQ_REF]
3741 >- (‘c<d’ by simp[RAT_LT_LE_NEQ] >> Cases_on ‘a=0’
3742 >- simp[]
3743 >- (‘0<a’ by simp[RAT_LT_LE_NEQ] >> irule RAT_LES_IMP_LEQ
3744 >> simp[RAT_LES_LMUL_POS])
3745 )
3746 >- (‘a<b’ by simp[RAT_LT_LE_NEQ] >> Cases_on ‘c=0’
3747 >- simp[]
3748 >- (‘0<c’ by simp[RAT_LT_LE_NEQ] >> irule RAT_LES_IMP_LEQ
3749 >> simp[RAT_LES_RMUL_POS])
3750 )
3751 >- (‘a<b /\ c<d’ by simp[RAT_LT_LE_NEQ] >> irule RAT_LES_IMP_LEQ
3752 >> ‘0<b /\ 0<d’ by metis_tac[RAT_LEQ_LES_TRANS] >> Cases_on ‘c=0’
3753 >- simp[RAT_MUL_SIGN_CASES]
3754 >- (‘0<c’ by simp[RAT_LT_LE_NEQ] >> ‘a*c < b*c’ by simp[RAT_LES_RMUL_POS]
3755 >> ‘b*c < b*d’ by simp[RAT_LES_LMUL_POS] >> metis_tac[RAT_LES_TRANS])
3756 )
3757QED
3758
3759Theorem RAT_EXPN_LT:
3760 0<p /\ 0<q /\ 0<n ==> (expn p n < expn q n <=> p < q)
3761Proof
3762 rw[] >> ‘?m. n = SUC m’ by metis_tac[num_CASES,NOT_ZERO_LT_ZERO]
3763 >> gvs[] >> iff_tac
3764 >- (Induct_on ‘m’
3765 >- simp[Once ONE,RAT_EXPN_CALCULATE]
3766 >- (once_rewrite_tac[rat_expn_def] >> rw[] >> CCONTR_TAC
3767 >> gs[RAT_LEQ_LES]
3768 >> ‘q * expn q (SUC m) <= p * expn p (SUC m)’
3769 by (irule RAT_LEQ_MUL >> simp[RAT_LES_IMP_LEQ,RAT_EXPN_R_POS])
3770 >> metis_tac[RAT_LEQ_LES]))
3771 >- (Induct_on ‘m’
3772 >- simp[RAT_EXPN_TO_1]
3773 >- (once_rewrite_tac[rat_expn_def] >> rw[] >> gs[] >> irule RAT_LT_MUL
3774 >> simp[RAT_EXPN_R_POS]))
3775QED
3776
3777Theorem RAT_MINV_ID:
3778 r<>0 ==> (rat_minv r = r <=> (r=1 \/ r=-1 \/ r=0))
3779Proof
3780 rw[EQ_IMP_THM]
3781 >- (‘r*r=1’ by metis_tac[RAT_MUL_RINV]
3782 >> ‘(r-1)*(r+1) = 0’
3783 by (PURE_REWRITE_TAC[RAT_LDISTRIB,RAT_RDISTRIB,RAT_SUB_ADDAINV]
3784 >> ‘r*r + -1*r + (r*1 + -1 * 1) = r*r + (-1*r + 1*r) + -1’
3785 by metis_tac[RAT_ADD_ASSOC,RAT_MUL_COMM,RAT_MUL_RID]
3786 >> ‘_ = r*r + -1’
3787 by metis_tac[RAT_RDISTRIB,RAT_ADD_LINV,RAT_MUL_LZERO,RAT_ADD_RID]
3788 >> metis_tac[RAT_SUB_ADDAINV,RAT_LSUB_EQ,RAT_ADD_RINV])
3789 >> gs[]
3790 >> metis_tac[RAT_LSUB_EQ,RAT_AINV_AINV,RAT_SUB_ADDAINV,RAT_ADD_RID])
3791 >> simp[GSYM RAT_AINV_MINV]
3792QED
3793
3794Theorem RAT_EXPN_NEG_LT_ZERO:
3795 r<0 ==> (0 < expn r n <=> EVEN n) /\ (expn r n < 0 <=> ODD n)
3796Proof
3797 strip_tac >> ‘?m. r=-m /\ 0<m’ by (qexists_tac ‘-r’ >> simp[])
3798 >> rw[RAT_EXPN_NEG,RAT_EXPN_R_POS,RAT_LES_ANTISYM,EVEN_ODD]
3799QED
3800
3801Theorem RAT_EXPN_EQ_1_POS:
3802 0<r ==> (expn r n = 1 <=> (r=1 \/ n=0))
3803Proof
3804 rw[EQ_IMP_THM,RAT_EXPN_1,RAT_EXPN_TO_0]
3805 >- (CCONTR_TAC >> gs[NOT_ZERO_LT_ZERO] >> Cases_on ‘1<r’
3806 >-(‘expn 1 n < expn r n’ by simp[RAT_EXPN_LT]
3807 >> ‘1 < expn r n’ by metis_tac[RAT_EXPN_1]
3808 >> metis_tac[RAT_LES_IMP_NEQ]
3809 )
3810 >-(gs[RAT_LEQ_LES,rat_leq_def]
3811 >> ‘expn r n < expn 1 n’ by simp[RAT_EXPN_LT]
3812 >> ‘expn r n < 1’ by metis_tac[RAT_EXPN_1]
3813 >> metis_tac[RAT_LES_IMP_NEQ]
3814 )
3815 )
3816 >-simp[RAT_EXPN_1]
3817 >-simp[RAT_EXPN_TO_0]
3818QED
3819
3820Theorem RAT_EXPN_EQ_1_NEG:
3821 r<0 ==> (expn r n = 1 <=> (r=-1 /\ EVEN n \/ n=0))
3822Proof
3823 rw[EQ_IMP_THM]
3824 >-(CCONTR_TAC >> Cases_on ‘r=-1’ >> gs[]
3825 >-gs[RAT_EXPN_MINUS1]
3826 >-(‘EVEN n’ by metis_tac[RAT_EXPN_NEG_LT_ZERO,RAT_LES_01]
3827 >> ‘?m. r=-m /\ 0<m’ by (qexists_tac ‘-r’ >> simp[])
3828 >> gs[RAT_EXPN_NEG,RAT_EXPN_EQ_1_POS]
3829 )
3830 )
3831 >-simp[RAT_EXPN_MINUS1]
3832 >-simp[RAT_EXPN_TO_0]
3833QED
3834
3835Theorem RAT_EXPN_EQ_1:
3836 expn r n = 1 <=> (r=1 \/ r=-1 /\ EVEN n \/ n=0)
3837Proof
3838 Cases_on ‘0<r’
3839 >-(‘-1<>r’ by (CCONTR_TAC >> gs[])
3840 >> simp[RAT_EXPN_EQ_1_POS]
3841 )
3842 >-(Cases_on ‘r=0’ >> gs[RAT_LEQ_LES,rat_leq_def,RAT_LES_IMP_NEQ]
3843 >-(iff_tac
3844 >-(CCONTR_TAC >> gs[RAT_EXPN_0])
3845 >-(simp[RAT_EXPN_TO_0])
3846 )
3847 >-(‘r<>1’ by (CCONTR_TAC >> gs[])
3848 >> simp[RAT_EXPN_EQ_1_NEG]
3849 )
3850 )
3851QED
3852
3853Theorem RAT_EXPN_INJ:
3854 r<>0 /\ r<>1 /\ r<>-1 ==> (expn r i = expn r j <=> i = j)
3855Proof
3856 rw[EQ_IMP_THM] >> wlog_tac ‘i <= j’ [‘i’,‘j’]
3857 >- gs[INT_NOT_LE,INT_LT_IMP_LE]
3858 >-(‘expn r (j-i) = 1’
3859 by simp[RAT_EXPN_SUB,RAT_LDIV_EQ,RAT_MUL_RID,RAT_EXPN_R_NONZERO]
3860 >> ‘!m. m<>0 ==> expn r m <> 1’
3861 suffices_by metis_tac[SUB_EQ_0,LESS_EQUAL_ANTISYM]
3862 >> rw[]
3863 >> Cases_on ‘0<r’
3864 >- simp[RAT_EXPN_EQ_1_POS]
3865 >- (gs[RAT_LEQ_LES,rat_leq_def] >> metis_tac[RAT_EXPN_EQ_1_NEG]))
3866QED
3867
3868Definition rat_exp_def:
3869 rat_exp r (i:int) = if 0<=i then expn r (Num i) else rat_minv (expn r (Num i))
3870End
3871
3872Overload exp[local] = “rat$rat_exp”
3873Overload "**" = “rat$rat_exp”;
3874
3875Theorem RAT_EXP_TO_0:
3876 exp r 0 = 1
3877Proof
3878 simp[rat_exp_def,rat_expn_def]
3879QED
3880
3881Theorem RAT_EXP_NUM:
3882 exp r (&n) = expn r n
3883Proof
3884 simp[rat_exp_def]
3885QED
3886
3887Theorem RAT_EXP_NEG_INT:
3888 exp r (-&n) = rat_minv (expn r n)
3889Proof
3890 rw[rat_exp_def,rat_expn_def]
3891QED
3892
3893Theorem RAT_EXP_RAT_MINV:
3894 r<>0 ==> exp (rat_minv r) i = rat_minv (exp r i)
3895Proof
3896 Cases_on ‘i’
3897 >> simp[RAT_EXP_NUM,RAT_EXP_NEG_INT,RAT_EXP_TO_0,RAT_EXPN_RAT_MINV]
3898QED
3899
3900Theorem RAT_EXP_1:
3901 exp 1 i = 1
3902Proof
3903 Cases_on ‘i’ >> simp[RAT_EXP_NUM,RAT_EXP_NEG_INT,RAT_EXP_TO_0,RAT_EXPN_1]
3904QED
3905
3906Theorem NUM_NZERO:
3907 i<>0 ==> Num i <> 0 /\ 0 < Num i
3908Proof
3909 rw[] >> Cases_on ‘i’ >> simp[] >> intLib.ARITH_TAC
3910QED
3911
3912Theorem RAT_EXP_0:
3913 0<i ==> 0 ** i = 0
3914Proof
3915 simp[rat_exp_def,NUM_NZERO,RAT_EXPN_0,INT_LT_IMP_NE]
3916QED
3917
3918Theorem RAT_EXP_CALCULATE[simp]:
3919 exp r 0 = 1 /\ exp r 1 = r /\ exp 1 i = 1 /\ exp r (&n) = expn r n /\
3920 exp r (-&n) = rat_minv (expn r n)
3921Proof
3922 simp[RAT_EXP_NUM,RAT_EXP_NEG_INT,RAT_EXP_TO_0,RAT_EXPN_TO_1,RAT_EXP_1]
3923QED
3924
3925Theorem RAT_EXP_R_NONZERO:
3926 r<>0 ==> exp r i <> 0
3927Proof
3928 Cases_on ‘i’ >> simp[RAT_EXP_CALCULATE,RAT_EXPN_R_NONZERO]
3929QED
3930
3931Theorem RAT_EXP_R_POS:
3932 0<r ==> 0 < exp r i
3933Proof
3934 Cases_on ‘i’
3935 >> simp[RAT_EXP_CALCULATE,RAT_EXPN_R_POS,RAT_MINV_LES,RAT_LES_IMP_NEQ]
3936QED
3937
3938Theorem RAT_MINV_RAT_MINV:
3939 r <> 0 ==> rat_minv (rat_minv r) = r
3940Proof
3941 metis_tac[RAT_EQ_RMUL,RAT_MINV_EQ_0,RAT_MUL_LINV,RAT_MUL_RINV]
3942QED
3943
3944Theorem RAT_MINV_DIV:
3945 a<>0 /\ b<>0 ==> rat_minv (a/b) = rat_minv a / rat_minv b
3946Proof
3947 rw[RAT_DIV_MULMINV,RAT_MINV_MUL]
3948QED
3949
3950Theorem RAT_EXP_ADD:
3951 r<>0 \/ (0 <= a /\ 0 <= b) ==> exp r (a+b) = exp r a * exp r b
3952Proof
3953 rw[] >> Cases_on ‘a’ >> Cases_on ‘b’ >> rw[]
3954 >- simp[RAT_EXP_NUM,INT_ADD_CALCULATE,RAT_EXPN_ADD]
3955 >- (gs[] >> rw[RAT_EXP_NUM,RAT_EXP_NEG_INT,INT_ADD_CALCULATE,RAT_EXPN_SUB]
3956 >> simp[RAT_MINV_MUL,RAT_EXPN_R_NONZERO,RAT_MINV_EQ_0,RAT_MINV_RAT_MINV,
3957 RAT_MUL_COMM,RAT_DIV_MULMINV,RAT_MINV_DIV])
3958 >- (gs[] >> rw[RAT_EXP_NUM,RAT_EXP_NEG_INT,INT_ADD_CALCULATE,RAT_EXPN_SUB]
3959 >> simp[RAT_MINV_MUL,RAT_EXPN_R_NONZERO,RAT_MINV_EQ_0,RAT_MINV_RAT_MINV,
3960 RAT_MUL_COMM,RAT_DIV_MULMINV,RAT_MINV_DIV])
3961 >- (gs[] >> simp[INT_ADD_CALCULATE,RAT_EXP_NEG_INT,RAT_EXPN_ADD,RAT_MINV_MUL,
3962 RAT_EXPN_R_NONZERO])
3963QED
3964
3965Theorem RAT_EXP_MUL:
3966 r<>0 \/ (0 <= a /\ 0 <= b) ==> exp r (a*b) = exp (exp r a) b
3967Proof
3968 Cases_on ‘a’ >> Cases_on ‘b’
3969 >> simp[RAT_EXPN_MUL,RAT_EXP_CALCULATE,INT_MUL_CALCULATE,RAT_EXPN_RAT_MINV,
3970 RAT_EXPN_CALCULATE,RAT_MINV_RAT_MINV]
3971QED
3972
3973Theorem RAT_EXP_PROD:
3974 a<>0 /\ b<>0 \/ (0 <= i) ==> exp (a*b) i = exp a i * exp b i
3975Proof
3976 Cases_on ‘i’
3977 >> simp[RAT_EXP_CALCULATE,RAT_EXPN_PROD,RAT_MINV_MUL,RAT_EXPN_CALCULATE]
3978QED
3979
3980Theorem RAT_MUL_NEG:
3981 -a * -b:rat = a*b
3982Proof
3983 simp[GSYM RAT_AINV_LMUL,Once $ RAT_MUL_COMM,RAT_AINV_AINV,Once $ RAT_MUL_COMM]
3984QED
3985
3986Theorem RAT_EXP_DIV:
3987 b<>0 /\ (a<>0 \/ 0 <= i) ==> exp (a/b) i = exp a i / exp b i
3988Proof
3989 rw[] >> Cases_on ‘i’ >> gs[]
3990 >> simp[RAT_EXP_CALCULATE,RAT_EXPN_DIV,RAT_EXPN_R_NONZERO,RAT_MINV_DIV]
3991QED
3992
3993Theorem RAT_EXP_TO_NEG:
3994 r <> 0 ==> exp r (-i) = rat_minv (exp r i)
3995Proof
3996 rw[] >> ‘r ** -i * r ** i = 1’ by simp[GSYM RAT_EXP_ADD] >>
3997 metis_tac[RAT_MUL_LINV,RAT_EQ_RMUL,RAT_EXP_R_NONZERO]
3998QED
3999
4000Theorem RAT_EXP_LT:
4001 0<r /\ 0<q /\ 0<i ==> (exp r i < exp q i <=> r < q)
4002Proof
4003 rw[] >> simp[rat_exp_def,RAT_EXPN_LT] >>
4004 ‘0 < Num i’ by (irule (cj 2 NUM_NZERO) >> intLib.ARITH_TAC)
4005 >> simp[RAT_EXPN_LT]
4006QED
4007
4008Theorem NUM_POSINT_EXISTS_SUC:
4009 0<i ==> ?n. i:int = &(SUC n)
4010Proof
4011 rw[] >> ‘0 < Num i’ by simp[NUM_NZERO,INT_POS_NZ] >>
4012 qexists_tac ‘PRE (Num i)’ >> simp[iffLR SUC_PRE,INT_OF_NUM,INT_LT_IMP_LE]
4013QED
4014
4015Theorem RAT_LES_MUL_GTR_1:
4016 0 < r /\ 1 < q ==> r < r*q
4017Proof
4018 rw[]
4019 >> ‘0<q-1’ by simp[RAT_LES_0SUB]
4020 >> ‘0 < r * (q-1)’ by simp[RAT_MUL_SIGN_CASES]
4021 >> metis_tac[RAT_LES_0SUB,RAT_SUB_LDISTRIB,RAT_MUL_RID]
4022QED
4023
4024Theorem RAT_EXP_LT2:
4025 !r i j. 1<r ==> (exp r i < exp r j <=> i < j)
4026Proof
4027 rpt strip_tac >> simp[EQ_IMP_THM]
4028 >> qid_spec_tac ‘j’ >> CONV_TAC FORALL_AND_CONV
4029 >> qid_spec_tac ‘i’ >> CONV_TAC FORALL_AND_CONV
4030 >> conj_asm2_tac
4031 >- (rw[] >> CCONTR_TAC >> ‘j<i \/ j=i’ by simp[GSYM INT_NOT_LT,GSYM INT_LE_LT]
4032 >- metis_tac[RAT_LES_ANTISYM]
4033 >- gs[RAT_LES_REF])
4034 >- (rw[]
4035 >> ‘?n. j = &(SUC n) + i’
4036 by simp[NUM_POSINT_EXISTS_SUC,INT_SUB_LT,GSYM INT_EQ_SUB_RADD] >> gvs[]
4037 >> ‘r<>0 /\ 0<r’ by metis_tac[RAT_LES_REF,RAT_LES_01,RAT_LES_TRANS]
4038 >> Induct_on ‘n’
4039 >- (simp[RAT_EXP_ADD,RAT_EXPN_TO_1]
4040 >> metis_tac[RAT_LES_MUL_GTR_1,RAT_MUL_COMM,RAT_EXP_R_POS])
4041 >- (‘exp r (&SUC (SUC n) + i) = exp r (&SUC n + i) * r’
4042 by simp[INT,RAT_EXP_ADD,RAT_EXP_CALCULATE,rat_expn_def,
4043 AC RAT_MUL_ASSOC RAT_MUL_COMM]
4044 >> ‘exp r (&SUC n + i) < exp r (&SUC (SUC n) + i)’
4045 by simp[RAT_LES_MUL_GTR_1,RAT_EXP_R_POS]
4046 >> metis_tac[RAT_LES_TRANS]))
4047QED
4048
4049Theorem RAT_MINV_LT_1:
4050 !r. 0<r ==> (1 < rat_minv r <=> r < 1) /\ (rat_minv r < 1 <=> 1 < r)
4051Proof
4052 rw[]
4053 >-(‘rat_minv r * r < rat_minv r * 1 <=> r<1’
4054 suffices_by gs[RAT_MUL_LINV,RAT_MUL_RID,RAT_LES_IMP_NEQ]
4055 >> simp[RAT_LES_LMUL_POS,RAT_MINV_LES,Excl "RAT_MUL_RID",RAT_LES_IMP_NEQ])
4056 >-(‘rat_minv r * r < 1 * r <=> 1 < r’ by simp[RAT_MUL_LINV,RAT_LES_IMP_NEQ]
4057 >> gs[RAT_LES_RMUL_POS])
4058QED
4059
4060Theorem RAT_LES_AINV2:
4061 !r1 r2. r1 < -r2 <=> r2 < -r1
4062Proof
4063 metis_tac[RAT_AINV_LES,RAT_AINV_AINV]
4064QED
4065
4066Theorem RAT_MINV_LT_MINUS1:
4067 !r. r<0 ==> (-1 < rat_minv r <=> r < -1) /\ (rat_minv r < -1 <=> -1 < r)
4068Proof
4069 once_rewrite_tac[RAT_AINV_LES,RAT_LES_AINV2]
4070 >> simp[RAT_AINV_MINV,RAT_LES_IMP_NEQ,RAT_AINV_SGN,RAT_MINV_LT_1]
4071QED
4072
4073
4074Theorem INT_MOD_MUL:
4075 m<>0 ==> (a*b) % m = ((a % m) * (b % m)) % m
4076Proof
4077 rw[] >> ‘a = a/m*m + a%m /\ b = b/m*m + b%m’ by simp[INT_DIVISION]
4078 >> ‘(a*b) % m = ((a/m*m + a%m) * (b/m*m + b%m))%m’ by metis_tac[]
4079 >> ‘_ = ((a/m) * m * (b/m) * m + (a/m) * m * (b%m) + (a%m) * (b/m)*m +
4080 (a%m * b%m))%m’
4081 by (simp[INT_RDISTRIB,INT_LDISTRIB]
4082 >> metis_tac[INT_ADD_ASSOC,INT_MUL_ASSOC])
4083 >> simp[GSYM INT_ADD_ASSOC,INT_MOD_ADD_MULTIPLES]
4084 >> simp[Once $ INT_MUL_COMM,Once $ INT_MUL_ASSOC,INT_MOD_ADD_MULTIPLES]
4085QED
4086
4087Theorem RAT_EXP_MINUS1:
4088 -1 ** i = if i % 2 = 0 then 1 else -1
4089Proof
4090 Cases_on ‘i’ >> rw[rat_exp_def]
4091 >> gs[Once $ INT_NEG_MINUS1,Once $ INT_MOD_MUL]
4092 >> simp[RAT_EXPN_MINUS1,EVEN_MOD2,GSYM RAT_AINV_MINV]
4093QED
4094
4095Theorem RAT_EXP_NEG:
4096 (r<>0 \/ 0<i) ==> (-r:rat) ** i = if i % 2 = 0 then r ** i else - (r ** i)
4097Proof
4098 Cases_on ‘r=0’
4099 >- simp[RAT_EXP_0]
4100 >- (once_rewrite_tac[GSYM RAT_AINV_MUL_AINV]
4101 >> rw[RAT_EXP_PROD,RAT_EXP_MINUS1])
4102QED
4103
4104Theorem RAT_EXP_SUB:
4105 !r i j. r<>0 ==> r ** (i-j) = (r ** i) / (r ** j)
4106Proof
4107 simp[int_sub,RAT_DIV_MULMINV,GSYM RAT_EXP_TO_NEG,RAT_EXP_ADD]
4108QED
4109
4110Theorem RAT_EXP_INJ:
4111 !r i j. r<>0 /\ r<>1 /\ r<>-1 ==> (r ** i = r ** j <=> i = j)
4112Proof
4113 rw[EQ_IMP_THM]
4114 >> ‘r ** (i-j) = 1’ by simp[RAT_EXP_SUB,RAT_DIV_INV,RAT_EXP_R_NONZERO]
4115 >> ‘!m. r ** m = 1 ==> m=0’ suffices_by metis_tac[INT_SUB_0]
4116 >> rw[rat_exp_def]
4117 >-(‘Num m = 0’ by gs[RAT_EXPN_EQ_1] >> metis_tac[NUM_NZERO])
4118 >-(‘expn r (Num m) = 1’
4119 by metis_tac[RAT_MINV_1,RAT_MINV_RAT_MINV,RAT_EXPN_R_NONZERO]
4120 >> ‘Num m = 0’ by gs[RAT_EXPN_EQ_1] >> metis_tac[NUM_NZERO]
4121 )
4122QED
4123
4124Theorem RAT_EXP_LE:
4125 !r i j. 1<r ==> (exp r i <= exp r j <=> i <= j)
4126Proof
4127 rw[INT_LE_LT,rat_leq_def]
4128 >> ‘r<>0 /\ r<>1 /\ r<>-1’ by (CCONTR_TAC >> gs[])
4129 >> metis_tac[RAT_EXP_LT2,RAT_EXP_INJ]
4130QED
4131
4132
4133(*==========================================================================
4134 * end of theory
4135 *==========================================================================*)