fracScript.sml
1(***************************************************************************
2 *
3 * Theory of fractions.
4 *
5 * Jens Brandt, November 2005
6 *
7 ***************************************************************************)
8Theory frac
9Ancestors
10 pair arithmetic integer intExtension
11Libs
12 pairSyntax schneiderUtils intLib intSyntax intExtensionLib
13
14
15val _ = ParseExtras.temp_loose_equality()
16
17
18val ERR = mk_HOL_ERR "fracScript"
19
20(*--------------------------------------------------------------------------*
21 * type definition
22 *--------------------------------------------------------------------------*)
23
24val frac_tyax = new_type_definition( "frac",
25 Q.prove(`?x. (\f:int#int. 0i<SND(f)) x`,
26 EXISTS_TAC ``(1i,1i)`` THEN
27 BETA_TAC THEN
28 REWRITE_TAC[SND] THEN
29 RW_TAC int_ss []) );
30
31Theorem frac_bij = define_new_type_bijections{
32 name="frac_tybij",
33 ABS="abs_frac",
34 REP="rep_frac",
35 tyax=frac_tyax };
36
37(*--------------------------------------------------------------------------*
38 * operations
39 *--------------------------------------------------------------------------*)
40
41(* numerator, denominator, sign of a fraction *)
42Definition frac_nmr_def: frac_nmr f = FST(rep_frac f)
43End
44Definition frac_dnm_def: frac_dnm f = SND(rep_frac f)
45End
46Definition frac_sgn_def: frac_sgn f1 = SGN (frac_nmr f1)
47End
48
49(* additive, multiplicative inverse of a fraction *)
50Definition frac_ainv_def: frac_ainv f1 = abs_frac(~frac_nmr f1, frac_dnm f1)
51End
52Definition frac_minv_def: frac_minv f1 = abs_frac(frac_sgn f1 * frac_dnm f1, ABS(frac_nmr f1) )
53End
54
55(* neutral elements *)
56Definition frac_0_def: frac_0 = abs_frac(0i,1i)
57End
58Definition frac_1_def: frac_1 = abs_frac(1i,1i)
59End
60
61(* less (absolute value) *)
62Definition les_abs_def: les_abs f1 f2 = frac_nmr f1 * frac_dnm f2 < frac_nmr f2 * frac_dnm f1
63End
64
65(* basic arithmetics *)
66Definition frac_add_def: frac_add f1 f2 = abs_frac(frac_nmr f1 * frac_dnm f2 + frac_nmr f2 * frac_dnm f1, frac_dnm f1*frac_dnm f2)
67End
68Definition frac_sub_def: frac_sub f1 f2 = frac_add f1 (frac_ainv f2)
69End
70Definition frac_mul_def: frac_mul f1 f2 = abs_frac(frac_nmr f1 * frac_nmr f2, frac_dnm f1*frac_dnm f2)
71End
72Definition frac_div_def: frac_div f1 f2 = frac_mul f1 (frac_minv f2)
73End
74
75(* frac_save terms are always defined (encode the definition of a fraction in the syntax) *)
76Definition frac_save_def: frac_save (nmr:int) (dnm:num) = abs_frac(nmr,&dnm + 1)
77End
78
79(*--------------------------------------------------------------------------
80 * FRAC: thm
81 * |- !f. abs_frac (frac_nmr f,frac_dnm f) = f
82 *--------------------------------------------------------------------------*)
83
84Theorem FRAC: !f. abs_frac (frac_nmr f,frac_dnm f) = f
85Proof
86 STRIP_TAC THEN
87 REWRITE_TAC[frac_nmr_def,frac_dnm_def]
88 THEN RW_TAC int_ss [CONJUNCT1 frac_bij]
89QED
90
91(*==========================================================================
92 * equivalence of fractions
93 *==========================================================================*)
94
95(*--------------------------------------------------------------------------
96 * FRAC_EQ: thm
97 * |- !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==>
98 * ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )
99 *--------------------------------------------------------------------------*)
100
101val [abs_rep_frac, rep_abs_frac] = CONJUNCTS frac_bij ;
102val (raf_eqI, raf_eqD) = EQ_IMP_RULE (SPEC_ALL rep_abs_frac) ;
103
104Theorem FRAC_EQ:
105 !a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==>
106 ((abs_frac(a1,b1)=abs_frac(a2,b2)) = (a1=a2) /\ (b1=b2) )
107Proof
108 REPEAT STRIP_TAC THEN EQ_TAC THEN DISCH_TAC THENL [
109 POP_ASSUM (MP_TAC o AP_TERM ``rep_frac``) THEN
110 VALIDATE (CONV_TAC (DEPTH_CONV (REWR_CONV_A (UNDISCH raf_eqI)))),
111 ALL_TAC] THEN
112 ASM_SIMP_TAC std_ss []
113QED
114
115(*--------------------------------------------------------------------------
116 * FRAC_EQ_ALT : thm
117 * |- !f1 f2. (f1=f2) = (frac_nmr f1 = frac_nmr f2) /\ (frac_dnm f1 = frac_dnm f2)
118 *--------------------------------------------------------------------------*)
119
120Theorem FRAC_EQ_ALT: !f1 f2. (f1=f2) = (frac_nmr f1 = frac_nmr f2) /\ (frac_dnm f1 = frac_dnm f2)
121Proof
122 REPEAT GEN_TAC THEN
123 EQ_TAC THEN
124 STRIP_TAC THENL
125 [
126 ALL_TAC
127 ,
128 ONCE_REWRITE_TAC[GSYM FRAC]
129 ] THEN
130 ASM_REWRITE_TAC[]
131QED
132
133(*--------------------------------------------------------------------------
134 * FRAC_NOT_EQ : thm
135 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
136 * (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2))
137 *--------------------------------------------------------------------------*)
138
139Theorem FRAC_NOT_EQ: !a1 b1 a2 b2. 0i<b1 ==> 0i<b2 ==> (~(abs_frac(a1,b1) = abs_frac(a2,b2)) = ~(a1=a2) \/ ~(b1=b2))
140Proof
141 REPEAT STRIP_TAC THEN
142 RW_TAC int_ss [] THEN
143 PROVE_TAC[FRAC_EQ]
144QED
145
146(*--------------------------------------------------------------------------
147 * FRAC_NOT_EQ_IMP : thm
148 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
149 * ~((a1,b1) = (a2,b2)) ==> ~(abs_frac (a1,b1) = abs_frac (a2,b2))
150 *--------------------------------------------------------------------------*)
151
152(* following theorem (with longer proof)
153 was previously stored as "FRAC_NOT_EQ", must be an error JED 16.9.15 *)
154Theorem FRAC_NOT_EQ_IMP:
155 !a1 b1 a2 b2. 0i < b1 ==> 0i < b2 ==>
156 ~((a1,b1) = (a2,b2)) ==> ~(abs_frac (a1,b1) = abs_frac (a2,b2))
157Proof
158 REPEAT GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THEN
159 ASM_SIMP_TAC std_ss [FRAC_EQ]
160QED
161
162
163(*--------------------------------------------------------------------------
164 * FRAC_EQ_TAC : tactic
165 *
166 * A ?- abs_frac(a1,b1) = abs_frac(a2,b2)
167 * ========================================= FRAC_EQ_TAC
168 * A ?- a1=a2 | A ?- b1=b2
169 *
170 * simplified version - note, doesn't check that goal is of given form
171 *--------------------------------------------------------------------------*)
172
173val FRAC_EQ_TAC:tactic = fn (asm_list,goal) =>
174 (AP_TERM_TAC THEN MK_COMB_TAC THENL [AP_TERM_TAC, ALL_TAC]) (asm_list,goal)
175 handle HOL_ERR _ => raise ERR "FRAC_EQ_TAC" "";
176
177(*==========================================================================
178 * some useful things about positive and non-zero
179 * numbers in the context of fractions
180 *==========================================================================*)
181
182(*--------------------------------------------------------------------------
183 * FRAC_DNMPOS : thm
184 * |- !f. 0 < frac_dnm f
185 *--------------------------------------------------------------------------*)
186
187Theorem FRAC_DNMPOS: !f. 0 < frac_dnm f
188Proof
189 REWRITE_TAC[frac_dnm_def] THEN
190 RW_TAC int_ss [REWRITE_RULE [CONJUNCT1 frac_bij] (SPEC ``rep_frac(f)`` (BETA_RULE (ONCE_REWRITE_RULE [EQ_SYM_EQ] (CONJUNCT2 frac_bij)))) ]
191QED
192
193(*--------------------------------------------------------------------------
194 * frac_pos_conv : term list -> conv
195 *--------------------------------------------------------------------------*)
196
197fun frac_pos_conv (asm_list:term list) (t1:term) =
198 if tmem ``0i < ^t1`` asm_list then ASSUME ``0i < ^t1``
199 else
200 if is_comb t1 then
201 let
202 val (rator, rand) = dest_comb t1
203 in
204 if is_mult t1 then
205 let
206 val (fac1, fac2) = intSyntax.dest_mult t1
207 val fac1_thm = frac_pos_conv asm_list fac1
208 val fac2_thm = frac_pos_conv asm_list fac2
209 in
210 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_MUL_POS_SIGN)
211 end
212 else if rator ~~ ``frac_dnm`` then SPEC rand FRAC_DNMPOS
213 else if rator ~~ ``ABS`` andalso tmem ``~(^rand = 0)`` asm_list then
214 UNDISCH (SPEC rand INT_ABS_NOT0POS)
215 else if is_int_literal t1 then EQT_ELIM (ARITH_CONV ``0 < ^t1``)
216 else ASSUME ``0i < ^t1``
217 end
218 else
219 ASSUME ``0i < ^t1``;
220
221(*--------------------------------------------------------------------------
222 * frac_not0_conv : term list -> conv
223 *--------------------------------------------------------------------------*)
224
225fun frac_not0_conv (asm_list:term list) (t1:term) =
226 if tmem ``~(^t1 = 0i)`` asm_list then ASSUME ``~(^t1 = 0i)``
227 else if is_comb t1 then
228 let
229 val (rator, rand) = dest_comb t1
230 in
231 if is_mult t1 then
232 let
233 val (fac1, fac2) = intSyntax.dest_mult t1
234 val fac1_thm = frac_not0_conv asm_list fac1
235 val fac2_thm = frac_not0_conv asm_list fac2
236 in
237 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_NOT0_MUL)
238 end
239 else if rator ~~ ``frac_dnm`` then
240 MP (SPEC t1 INT_GT0_IMP_NOT0) (SPEC rand FRAC_DNMPOS)
241 else if rator ~~ “SGN” andalso tmem “~(^rand = 0)” asm_list then
242 UNDISCH (SPEC rand INT_NOT0_SGNNOT0)
243 else if is_int_literal t1 then EQT_ELIM (ARITH_CONV ``~(^t1 = 0i)``)
244 else ASSUME ``~(^t1 = 0i)``
245 end
246 else
247 ASSUME ``~(^t1 = 0i)``;
248
249(*--------------------------------------------------------------------------
250 * FRAC_POS_TAC : term -> tactic
251 *--------------------------------------------------------------------------*)
252
253fun FRAC_POS_TAC term1 (asm_list, goal) =
254 (ASSUME_TAC (frac_pos_conv asm_list term1)) (asm_list, goal);
255
256(*--------------------------------------------------------------------------
257 * FRAC_NOT0_TAC : term -> tactic
258 *--------------------------------------------------------------------------*)
259
260fun FRAC_NOT0_TAC term1 (asm_list, goal) =
261 (ASSUME_TAC (frac_not0_conv asm_list term1)) (asm_list, goal);
262
263(*==========================================================================
264 * numerator and denominator extraction
265 *==========================================================================*)
266
267val FRAC_REP_ABS_SUBST =
268let
269 val lemma01 = prove( ``(\f. 0<SND f) (a1:int,b1:int) = (0<b1)``, BETA_TAC THEN REWRITE_TAC[SND]);
270 val lemma02 = fst(EQ_IMP_RULE (ONCE_REWRITE_RULE[EQ_SYM_EQ] (SPEC ``(a:int,b:int)`` (ONCE_REWRITE_RULE [EQ_SYM_EQ] (CONJUNCT2 frac_bij)))))
271in
272 UNDISCH(ONCE_REWRITE_RULE [lemma01] lemma02)
273end;
274
275(*--------------------------------------------------------------------------
276 * NMR: thm
277 * |- !a b. 0 < b ==> (frac_nmr (abs_frac (a,b)) = a)
278 *--------------------------------------------------------------------------*)
279
280Theorem NMR: !a b. 0 < b ==> (frac_nmr (abs_frac (a,b)) = a)
281Proof
282 REPEAT STRIP_TAC THEN
283 REWRITE_TAC[frac_nmr_def] THEN
284 REWRITE_TAC[FRAC_REP_ABS_SUBST]
285QED
286
287(*--------------------------------------------------------------------------
288 * DNM: thm
289 * |- !a b. 0 < b ==> (frac_dnm (abs_frac (a,b)) = b)
290 *--------------------------------------------------------------------------*)
291
292Theorem DNM: !a b. 0 < b ==> (frac_dnm (abs_frac (a,b)) = b)
293Proof
294 REPEAT STRIP_TAC THEN
295 REWRITE_TAC[frac_dnm_def] THEN
296 REWRITE_TAC[FRAC_REP_ABS_SUBST]
297QED
298
299(*--------------------------------------------------------------------------
300 * FRAC_NMR_CONV: conv
301 *
302 * frac_nmr (abs_frac (a1,b1))
303 * -----------------------------------------
304 * 0 < b1 |- (frac_nmr (abs_frac (a1,b1)) = a1)
305 *--------------------------------------------------------------------------*)
306
307val FRAC_NMR_CONV:conv = fn term =>
308let
309 val (nmr,f) = dest_comb term;
310 val (abs,args) = dest_comb f;
311 val (a,b) = dest_pair args;
312in
313 UNDISCH_ALL(SPEC b (SPEC a NMR))
314end
315handle HOL_ERR _ => raise ERR "FRAC_NMR_CONV" "";
316
317
318(*--------------------------------------------------------------------------
319 * FRAC_DNM_CONV: conv
320 *
321 * frac_dnm (abs_frac (a1,b1))
322 * -----------------------------------------
323 * 0 < b1 |- (frac_dnm (abs_frac (a1,b1)) = a1)
324 *--------------------------------------------------------------------------*)
325
326val FRAC_DNM_CONV:conv = fn term =>
327let
328 val (nmr,f) = dest_comb term;
329 val (abs,args) = dest_comb f;
330 val (a,b) = dest_pair args;
331in
332 UNDISCH_ALL(SPEC b (SPEC a DNM))
333end
334handle HOL_ERR _ => raise ERR "FRAC_DNM_CONV" "";
335
336(*--------------------------------------------------------------------------
337 * frac_nmr_tac : term*term -> tactic
338 *--------------------------------------------------------------------------*)
339
340 fun frac_nmr_tac (asm_list:term list) (nmr,dnm) =
341 let
342 val asm_thm = frac_pos_conv asm_list dnm;
343 val sub_thm = DISCH_ALL (FRAC_NMR_CONV ``nmr( abs_frac (^nmr, ^dnm) )``);
344 in
345 TRY (
346 SUBST1_TAC (MP sub_thm asm_thm)
347 )
348 end;
349
350(*--------------------------------------------------------------------------
351 * frac_dnm_tac : term*term -> tactic
352 *--------------------------------------------------------------------------*)
353
354fun frac_dnm_tac (asm_list:term list) (nmr,dnm) =
355 let
356 val asm_thm = frac_pos_conv asm_list dnm;
357 val sub_thm = DISCH_ALL (FRAC_DNM_CONV ``dnm( abs_frac (^nmr, ^dnm) )``);
358 in
359 TRY (
360 SUBST1_TAC (MP sub_thm asm_thm)
361 )
362 end;
363
364(*--------------------------------------------------------------------------
365 * FRAC_NMRDNM_TAC : tactic
366 *
367 * simplify resp. nmr(abs_frac(a1,b1)) to a1 and frac_dnm(abs_frac(a1,b1)) to b1
368 *--------------------------------------------------------------------------*)
369
370fun ttrip_eq (t1,t2,t3) (ta,tb,tc) =
371 pair_eq (pair_eq aconv aconv) aconv ((t1,t2),t3) ((ta,tb),tc)
372
373fun extract_frac_fun (l2:term list) (t1:term) =
374 if is_comb t1 then
375 let
376 val (top_rator, top_rand) = dest_comb t1;
377 in
378 if tmem top_rator l2 andalso is_comb top_rand then
379 let
380 val (second_rator, second_rand) = dest_comb top_rand;
381 in
382 if second_rator ~~ ``abs_frac`` then
383 let
384 val (this_nmr, this_dnm) = dest_pair (second_rand)
385 val sub_fracs =
386 op_union ttrip_eq
387 (extract_frac_fun l2 this_nmr)
388 (extract_frac_fun l2 this_dnm)
389 in
390 [(top_rator,this_nmr,this_dnm)] @ sub_fracs
391 end
392 else (* not second_rator = ``abs_frac`` *)
393 extract_frac_fun l2 top_rand
394 end
395 else (* not (top_rator = l2 andalso is_comb top_rand) *)
396 op_union ttrip_eq (extract_frac_fun l2 top_rator)
397 (extract_frac_fun l2 top_rand)
398 end
399 else (* not is_comb t1 *)
400 [];
401
402fun FRAC_NMRDNM_TAC (asm_list, goal) =
403let
404 val term_list = extract_frac_fun [``frac_nmr``,``frac_dnm``] goal
405 val nmr_term_list = map (fn (rator,nmr,dnm) => (nmr,dnm))
406 (filter (fn (a1,_,_) => a1~~“frac_nmr”) term_list)
407 val dnm_term_list = map (fn (rator,nmr,dnm) => (nmr,dnm))
408 (filter (fn (a1,_,_) => a1~~“frac_dnm”) term_list)
409in
410 (
411 MAP_EVERY (frac_nmr_tac asm_list) nmr_term_list THEN
412 MAP_EVERY (frac_dnm_tac asm_list) dnm_term_list THEN
413 SIMP_TAC int_ss [INT_MUL_LID, INT_MUL_RID, INT_MUL_LZERO, INT_MUL_RZERO]
414 ) (asm_list,goal)
415end
416handle HOL_ERR _ => raise ERR "FRAC_NMRDNM_TAC" "";
417
418(*==========================================================================
419 * calculation
420 *==========================================================================*)
421
422(*--------------------------------------------------------------------------
423 * FRAC_AINV_CALCULATE : thm
424 * |- !a1 b1. 0 < b1 ==>
425 * frac_ainv (abs_frac(a1,b1)) = abs_frac(~a1,b1)
426 *--------------------------------------------------------------------------*)
427
428Theorem FRAC_AINV_CALCULATE: !a1 b1. 0i<b1 ==> (frac_ainv (abs_frac(a1,b1)) = abs_frac(~a1,b1))
429Proof
430 REPEAT STRIP_TAC THEN
431 REWRITE_TAC[frac_ainv_def] THEN
432 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``] THEN
433 RW_TAC int_ss []
434QED
435
436(*--------------------------------------------------------------------------
437 * FRAC_MINV_CALCULATE : thm
438 * |- !a1 b1. (0i < b1) ==> ~(a1 = 0i) ==>
439 * frac_minv (abs_frac(a1,b1)) = if 0 < a1 then abs_frac(b1,a1) else abs_frac(~b1, ~a1) )
440 *--------------------------------------------------------------------------*)
441
442Theorem FRAC_MINV_CALCULATE: !a1 b1. (0i < b1) ==> ~(a1 = 0i) ==> (frac_minv (abs_frac(a1,b1)) = abs_frac(SGN(a1)*b1,ABS(a1)) )
443Proof
444 REPEAT STRIP_TAC THEN
445 REWRITE_TAC[frac_minv_def, frac_sgn_def] THEN
446 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``] THEN
447 PROVE_TAC[]
448QED
449
450(*--------------------------------------------------------------------------
451 * FRAC_SGN_CALCULATE : thm
452 * |- !a1 b1. (0 < b1) ==>
453 * (frac_sgn (abs_frac(a1,b1)) = SGN a1)
454 *--------------------------------------------------------------------------*)
455
456Theorem FRAC_SGN_CALCULATE: !a1 b1. (0i < b1) ==> (frac_sgn (abs_frac(a1,b1)) = SGN a1)
457Proof
458 REPEAT STRIP_TAC THEN
459 REWRITE_TAC[frac_sgn_def] THEN
460 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``] THEN
461 RW_TAC int_ss []
462QED
463
464(*--------------------------------------------------------------------------
465 * FRAC_ADD_CALCULATE : thm
466 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
467 * frac_add (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2+a2*b1 , b1*b2 )
468 *--------------------------------------------------------------------------*)
469
470Theorem FRAC_ADD_CALCULATE: !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==> (frac_add (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2+a2*b1 , b1*b2 ))
471Proof
472 REPEAT STRIP_TAC THEN
473 REWRITE_TAC[frac_add_def] THEN
474 SUBST_TAC[
475 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``,
476 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
477 RW_TAC int_ss []
478QED
479
480(*--------------------------------------------------------------------------
481 * FRAC_SUB_CALCULATE : thm
482 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
483 * frac_sub (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2-a2*b1 , b1*b2 )
484 *--------------------------------------------------------------------------*)
485
486Theorem FRAC_SUB_CALCULATE: !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==> (frac_sub (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*b2-a2*b1 , b1*b2 ))
487Proof
488 REPEAT STRIP_TAC THEN
489 REWRITE_TAC[frac_sub_def,frac_add_def,frac_ainv_def] THEN
490 SUBST_TAC[
491 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``,
492 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
493 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (~a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (~a2,b2))``] THEN
494 RW_TAC int_ss [INT_SUB_CALCULATE, INT_MUL_CALCULATE]
495QED
496
497(*--------------------------------------------------------------------------
498 * FRAC_MULT_CALCULATE : thm
499 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==>
500 * frac_mul (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*a2 , b1*b2 )
501 *--------------------------------------------------------------------------*)
502
503Theorem FRAC_MULT_CALCULATE: !a1 b1 a2 b2. 0<b1 ==> 0<b2 ==> (frac_mul (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*a2 , b1*b2 ))
504Proof
505 REPEAT STRIP_TAC THEN
506 REWRITE_TAC[frac_mul_def] THEN
507 SUBST_TAC[
508 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``,
509 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
510 RW_TAC int_ss []
511QED
512
513(*--------------------------------------------------------------------------
514 * FRAC_DIV_CALCULATE : thm
515 * |- !a1 b1 a2 b2. 0 < b1 ==> 0 < b2 ==> ~(a2 = 0) ==>
516 * frac_div (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*SGN(a2)*b2 , b1*ABS(a2) )
517 *--------------------------------------------------------------------------*)
518
519Theorem FRAC_DIV_CALCULATE: !a1 b1 a2 b2. 0i<b1 ==> 0i<b2 ==> ~(a2=0i) ==> (frac_div (abs_frac(a1,b1)) (abs_frac(a2,b2)) = abs_frac( a1*SGN(a2)*b2 , b1*ABS(a2) ) )
520Proof
521 REPEAT STRIP_TAC THEN
522 REWRITE_TAC[frac_div_def,frac_mul_def,frac_minv_def, frac_sgn_def] THEN
523 SUBST_TAC[
524 FRAC_NMR_CONV ``frac_nmr (abs_frac (a1,b1))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a1,b1))``,
525 FRAC_NMR_CONV ``frac_nmr (abs_frac (a2,b2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (a2,b2))``] THEN
526 ASSUME_TAC (UNDISCH_ALL (SPEC ``a2:int`` INT_ABS_NOT0POS)) THEN
527 SUBST_TAC[FRAC_NMR_CONV ``frac_nmr (abs_frac (SGN a2 * b2,ABS a2))``,FRAC_DNM_CONV ``frac_dnm (abs_frac (SGN a2 * b2,ABS a2))``] THEN
528 RW_TAC (int_ss ++ (simpLib.ac_ss [(INT_MUL_ASSOC, INT_MUL_COMM)])) []
529QED
530
531(*==========================================================================
532 * basic theorems (associativity, commutativity, identity elements, ...)
533 *==========================================================================*)
534
535(*--------------------------------------------------------------------------
536 * FRAC_ADD_ASSOC: thm
537 * |- !a b c. frac_add a (frac_add b c) = frac_add (frac_add a b) c
538 *
539 * FRAC_MULT_ASSOC: thm
540 * |- !a b c. frac_mul a (frac_mul b c) = frac_mul (frac_mul a b) c
541 *--------------------------------------------------------------------------*)
542
543Theorem FRAC_ADD_ASSOC: !a b c. frac_add a (frac_add b c) = frac_add (frac_add a b) c
544Proof
545 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_add_def]
546 THEN FRAC_POS_TAC ``frac_dnm a * frac_dnm b``
547 THEN FRAC_POS_TAC ``frac_dnm b * frac_dnm c``
548 THEN RW_TAC int_ss [NMR,DNM]
549 THEN FRAC_EQ_TAC THEN INT_RING_TAC
550QED
551
552Theorem FRAC_MUL_ASSOC: !a b c. frac_mul a (frac_mul b c) = frac_mul (frac_mul a b) c
553Proof
554 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_mul_def]
555 THEN FRAC_POS_TAC ``frac_dnm a * frac_dnm b``
556 THEN FRAC_POS_TAC ``frac_dnm b * frac_dnm c``
557 THEN RW_TAC int_ss [NMR,DNM]
558 THEN FRAC_EQ_TAC THEN INT_RING_TAC
559QED
560
561(*--------------------------------------------------------------------------
562 * FRAC_ADD_COMM: thm
563 * |- !a b c. frac_add a b = frac_add b a
564 *
565 * FRAC_MUL_COMM: thm
566 * |- !a b c. frac_mul a b = frac_mul b a
567 *--------------------------------------------------------------------------*)
568
569Theorem FRAC_ADD_COMM: !a b. frac_add a b = frac_add b a
570Proof
571 REPEAT STRIP_TAC THEN
572 REWRITE_TAC[frac_add_def]
573 THEN FRAC_EQ_TAC
574 THEN INT_RING_TAC
575QED
576
577Theorem FRAC_MUL_COMM: !a b. frac_mul a b = frac_mul b a
578Proof
579 REPEAT STRIP_TAC THEN
580 REWRITE_TAC[frac_mul_def]
581 THEN FRAC_EQ_TAC THEN
582 INT_RING_TAC
583QED
584
585(*--------------------------------------------------------------------------
586 * FRAC_ADD_RID: thm
587 * |- !a. frac_add a frac_0 = a
588 *
589 * FRAC_MUL_RID: thm
590 * |- !a. frac_mul a frac_1 = a
591 *--------------------------------------------------------------------------*)
592
593Theorem FRAC_ADD_RID: !a. frac_add a frac_0 = a
594Proof
595 STRIP_TAC THEN
596 REWRITE_TAC[frac_add_def, frac_0_def] THEN
597 RW_TAC int_ss [NMR,DNM] THEN
598 RW_TAC int_ss [FRAC]
599QED
600
601Theorem FRAC_MUL_RID: !a. frac_mul a frac_1 = a
602Proof
603 STRIP_TAC THEN
604 REWRITE_TAC[frac_mul_def, frac_1_def] THEN
605 RW_TAC int_ss [NMR,DNM] THEN
606 RW_TAC int_ss [FRAC]
607QED
608
609(*--------------------------------------------------------------------------
610 * FRAC_1_0: thm
611 * |- ~ (frac_1=frac_0)
612 *--------------------------------------------------------------------------*)
613
614Theorem FRAC_1_0: ~ (frac_1=frac_0)
615Proof
616 REWRITE_TAC[frac_0_def, frac_1_def] THEN
617 FRAC_POS_TAC ``1i`` THEN
618 MATCH_MP_TAC (UNDISCH (UNDISCH (SPEC ``1i`` (SPEC ``0i`` (SPEC ``1i`` (SPEC ``1i`` FRAC_NOT_EQ_IMP)))))) THEN
619 RW_TAC int_ss []
620QED
621
622(*==========================================================================
623 * calculation rules of basic arithmetics
624 *==========================================================================*)
625
626(*--------------------------------------------------------------------------
627 * FRAC_AINV_0: thm
628 * |- frac_ainv frac_0 = frac_0
629 *
630 * FRAC_AINV_AINV: thm
631 * |- !f1. frac_ainv (frac_ainv f1) = f1
632 *
633 * FRAC_AINV_ADD: thm
634 * |- ! f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2)
635 *
636 * FRAC_AINV_SUB: thm
637 * |- !a b. frac_sub a b = frac_ainv (frac_sub b a)
638 *
639 * FRAC_AINV_LMUL: thm
640 * |- !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2)
641 *
642 * FRAC_AINV_LMUL: thm
643 * |- !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2
644 *--------------------------------------------------------------------------*)
645
646Theorem FRAC_AINV_0: frac_ainv frac_0 = frac_0
647Proof
648 REWRITE_TAC[frac_0_def,frac_ainv_def] THEN
649 FRAC_POS_TAC ``1i`` THEN
650 RW_TAC int_ss [NMR,DNM] THEN
651 RW_TAC int_ss [INT_NEG_0]
652QED
653
654Theorem FRAC_AINV_AINV: !f1. frac_ainv (frac_ainv f1) = f1
655Proof
656 GEN_TAC THEN
657 REWRITE_TAC[frac_ainv_def] THEN
658 FRAC_POS_TAC ``frac_dnm f1`` THEN
659 RW_TAC int_ss [NMR, DNM, INT_NEGNEG, FRAC]
660QED
661
662Theorem FRAC_AINV_ADD: ! f1 f2. frac_ainv (frac_add f1 f2) = frac_add (frac_ainv f1) (frac_ainv f2)
663Proof
664 REPEAT GEN_TAC THEN
665 REWRITE_TAC[frac_add_def, frac_ainv_def] THEN
666 FRAC_POS_TAC ``frac_dnm f1`` THEN
667 FRAC_POS_TAC ``frac_dnm f2`` THEN
668 FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN
669 RW_TAC int_ss [NMR,DNM] THEN
670 FRAC_EQ_TAC THENL
671 [INT_RING_TAC,RW_TAC int_ss []]
672QED
673
674Theorem FRAC_AINV_SUB: !f1 f2. frac_ainv (frac_sub f2 f1) = frac_sub f1 f2
675Proof
676 REPEAT GEN_TAC THEN
677 REWRITE_TAC[frac_ainv_def, frac_add_def, frac_sub_def] THEN
678 FRAC_POS_TAC ``frac_dnm f1`` THEN
679 FRAC_POS_TAC ``frac_dnm f2`` THEN
680 FRAC_POS_TAC ``frac_dnm f2 * frac_dnm f1`` THEN
681 RW_TAC int_ss [NMR,DNM] THEN
682 FRAC_EQ_TAC THEN
683 INT_RING_TAC
684QED
685
686Theorem FRAC_AINV_RMUL: !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul f1 (frac_ainv f2)
687Proof
688 REPEAT GEN_TAC THEN
689 REWRITE_TAC[frac_mul_def, frac_ainv_def] THEN
690 FRAC_POS_TAC ``frac_dnm f2`` THEN
691 FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN
692 RW_TAC int_ss [NMR,DNM] THEN
693 FRAC_EQ_TAC THENL
694 [ INT_RING_TAC, PROVE_TAC[] ]
695QED
696
697Theorem FRAC_AINV_LMUL: !f1 f2. frac_ainv (frac_mul f1 f2) = frac_mul (frac_ainv f1) f2
698Proof
699 PROVE_TAC[FRAC_MUL_COMM, FRAC_AINV_RMUL]
700QED
701
702(*--------------------------------------------------------------------------
703 * FRAC_MINV_1: thm
704 * |- frac_minv frac_1 = frac_1
705 *--------------------------------------------------------------------------*)
706
707Theorem FRAC_MINV_1: frac_minv frac_1 = frac_1
708Proof
709 SIMP_TAC intLib.int_ss
710 [FRAC_MINV_CALCULATE, intExtensionTheory.SGN_def, frac_1_def]
711QED
712
713(*--------------------------------------------------------------------------
714 * FRAC_SUB_ADD: thm
715 * |- !a b c. frac_sub a (frac_add b c) = frac_sub (frac_sub a b) c
716 *
717 * FRAC_SUB_SUB: thm
718 * |- !a b c. frac_sub a (frac_sub b c) = frac_add (frac_sub a b) c
719 *--------------------------------------------------------------------------*)
720
721Theorem FRAC_SUB_ADD: !a b c. frac_sub a (frac_add b c) = frac_sub (frac_sub a b) c
722Proof
723 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_add_def,frac_sub_def,frac_ainv_def] THEN
724 FRAC_POS_TAC ``frac_dnm a * frac_dnm b`` THEN
725 FRAC_POS_TAC ``frac_dnm b * frac_dnm c`` THEN
726 FRAC_POS_TAC ``frac_dnm b`` THEN
727 FRAC_POS_TAC ``frac_dnm c`` THEN
728 RW_TAC int_ss [NMR,DNM] THEN
729 FRAC_EQ_TAC THEN
730 INT_RING_TAC
731QED
732
733Theorem FRAC_SUB_SUB: !a b c. frac_sub a (frac_sub b c) = frac_add (frac_sub a b) c
734Proof
735 REPEAT STRIP_TAC THEN REWRITE_TAC[frac_add_def,frac_sub_def,frac_ainv_def] THEN
736 FRAC_POS_TAC ``frac_dnm a * frac_dnm b`` THEN
737 FRAC_POS_TAC ``frac_dnm b * frac_dnm c`` THEN
738 FRAC_POS_TAC ``frac_dnm b`` THEN
739 FRAC_POS_TAC ``frac_dnm c`` THEN
740 RW_TAC int_ss [NMR,DNM] THEN
741 FRAC_EQ_TAC THEN
742 INT_RING_TAC
743QED
744
745(*==========================================================================
746 * signum, absolute value
747 *==========================================================================*)
748
749(*--------------------------------------------------------------------------
750 * FRAC_SGN_TOTAL: thm
751 * |- !f. (frac_sgn f1 = ~1) \/ (frac_sgn f1 = 0) \/ (frac_sgn f1 = 1)
752 *--------------------------------------------------------------------------*)
753
754Theorem FRAC_SGN_TOTAL: !f1. (frac_sgn f1 = ~1) \/ (frac_sgn f1 = 0) \/ (frac_sgn f1 = 1)
755Proof
756 REPEAT GEN_TAC THEN
757 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
758 ASM_CASES_TAC ``frac_nmr f1 = 0`` THENL
759 [
760 PROVE_TAC[]
761 ,
762 ASM_CASES_TAC ``frac_nmr f1 < 0`` THEN
763 PROVE_TAC[]
764 ]
765QED
766
767(*--------------------------------------------------------------------------
768 * FRAC_SGN_POS: thm
769 * |- !f1. (frac_sgn f1 = 1) = 0 < nmr f1
770 *--------------------------------------------------------------------------*)
771
772Theorem FRAC_SGN_POS: !f1. (frac_sgn f1 = 1) = 0 < frac_nmr f1
773Proof
774 GEN_TAC THEN
775 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
776 RW_TAC int_ss [] THENL
777 [
778 PROVE_TAC[INT_LT_GT]
779 ,
780 PROVE_TAC[INT_LT_TOTAL]
781 ]
782QED
783
784(*--------------------------------------------------------------------------
785 * FRAC_SGN_NOT_NEG: thm
786 * |- !f1. ~(frac_sgn f1 = ~1) = (0 = frac_nmr f1) \/ (0 < frac_nmr f1)
787 *--------------------------------------------------------------------------*)
788
789Theorem FRAC_SGN_NOT_NEG: !f1. ~(frac_sgn f1 = ~1) = (0 = frac_nmr f1) \/ (0 < frac_nmr f1)
790Proof
791 GEN_TAC THEN
792 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
793 RW_TAC int_ss [] THENL
794 [
795 PROVE_TAC[INT_LT_GT]
796 ,
797 PROVE_TAC[INT_LT_TOTAL]
798 ]
799QED
800
801(*--------------------------------------------------------------------------
802 * FRAC_SGN_NEG: thm
803 * |- ! f. ~frac_sgn (frac_ainv f) = frac_sgn f
804 *--------------------------------------------------------------------------*)
805
806Theorem FRAC_SGN_NEG: ! f. ~frac_sgn (frac_ainv f) = frac_sgn f
807Proof
808 GEN_TAC THEN
809 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
810 REWRITE_TAC[frac_ainv_def] THEN
811 ONCE_REWRITE_TAC[GSYM FRAC] THEN
812 FRAC_POS_TAC ``frac_dnm f`` THEN
813 RW_TAC int_ss [NMR,DNM] THEN
814 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
815 SUBST_TAC[UNDISCH_ALL (SPEC ``frac_dnm f`` (SPEC ``frac_nmr f`` NMR))] THEN
816 COND_CASES_TAC THENL
817 [
818 ASM_REWRITE_TAC[] THEN
819 SUBST_TAC[UNDISCH_ALL (SPEC ``frac_dnm f`` (SPEC ``~0`` NMR))] THEN
820 PROVE_TAC[INT_NEG_0]
821 ,
822 SUBST_TAC[UNDISCH_ALL (SPEC ``frac_dnm f`` (SPEC ``~frac_nmr f`` NMR))] THEN
823 REWRITE_TAC[INT_NEG_EQ,INT_NEG_LT0,INT_NEG_0] THEN
824 COND_CASES_TAC THENL
825 [
826 ASSUME_TAC (UNDISCH (SPEC ``0i`` (SPEC ``frac_nmr f`` INT_LT_GT))) THEN
827 PROVE_TAC[]
828 ,
829 ASSUME_TAC (SPEC ``frac_nmr f`` INT_NOTGT_IMP_EQLT) THEN
830 UNDISCH_TAC ``~(frac_nmr f < 0) = (0 = frac_nmr f) \/ 0 < frac_nmr f`` THEN
831 RW_TAC int_ss []
832 ]
833 ]
834QED
835
836(*--------------------------------------------------------------------------
837 * FRAC_SGN_IMP_EQGT: thm
838 * |- !f1 f2. frac_sub f1 f2 = frac_ainv (frac_sub f2 f1)
839 *--------------------------------------------------------------------------*)
840
841Theorem FRAC_SGN_IMP_EQGT: !f1. ~(frac_sgn f1 = ~1) = (frac_sgn f1 = 0i) \/ (frac_sgn f1 = 1i)
842Proof
843 GEN_TAC THEN
844 ASSUME_TAC (SPEC_ALL FRAC_SGN_TOTAL) THEN
845 REPEAT (RW_TAC int_ss [])
846QED
847
848(*--------------------------------------------------------------------------
849 * FRAC_SGN_MUL: thm
850 * |- !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
851 *--------------------------------------------------------------------------*)
852
853Theorem FRAC_SGN_MUL: !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
854Proof
855 REPEAT GEN_TAC THEN
856 REWRITE_TAC[frac_mul_def, frac_sgn_def, SGN_def] THEN
857 FRAC_POS_TAC ``frac_dnm f1 * frac_dnm f2`` THEN
858 REWRITE_TAC[UNDISCH_ALL (SPEC ``frac_dnm f1 * frac_dnm f2`` (SPEC ``frac_nmr f1 * frac_nmr f2`` NMR))] THEN
859 ASM_CASES_TAC ``frac_nmr f1=0i`` THEN
860 ASM_CASES_TAC ``frac_nmr f1 < 0i`` THEN
861 ASM_CASES_TAC ``frac_nmr f2=0i`` THEN
862 ASM_CASES_TAC ``frac_nmr f2 < 0i`` THEN
863 RW_TAC int_ss [INT_MUL_LZERO, INT_MUL_RZERO] THEN
864 PROVE_TAC[INT_ENTIRE,INT_MUL_SIGN_CASES,INT_LT_GT,INT_LT_TOTAL]
865QED
866
867
868(*--------------------------------------------------------------------------
869 * FRAC_ABS_SGN : thm
870 * |- !f1. ~(frac_nmr f1 = 0i) ==> (ABS (frac_sgn f1) = 1)
871 *--------------------------------------------------------------------------*)
872
873Theorem FRAC_ABS_SGN: !f1. ~(frac_nmr f1 = 0i) ==> (ABS (frac_sgn f1) = 1i)
874Proof
875 GEN_TAC THEN
876 REWRITE_TAC[frac_sgn_def, SGN_def] THEN
877 RW_TAC int_ss [] THEN
878 RW_TAC int_ss [INT_ABS]
879QED
880
881(*--------------------------------------------------------------------------
882 * FRAC_SGN_MUL : thm
883 * |- !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
884 * TODO: was FRAC_SGN_MUL2
885 *--------------------------------------------------------------------------*)
886
887Theorem FRAC_SGN_MUL2: !f1 f2. frac_sgn (frac_mul f1 f2) = frac_sgn f1 * frac_sgn f2
888Proof
889 REPEAT GEN_TAC THEN
890 REWRITE_TAC[frac_sgn_def, frac_mul_def] THEN
891 FRAC_NMRDNM_TAC THEN
892 PROVE_TAC[INT_SGN_MUL2]
893QED
894
895(*--------------------------------------------------------------------------
896 * FRAC_SGN_CASES : thm
897 * |- !f1 P.
898 * ((frac_sgn f1 = ~1) ==> P) /\
899 * ((frac_sgn f1 = 0i) ==> P) /\
900 * ((frac_sgn f1 = 1i) ==> P) ==> P
901 *--------------------------------------------------------------------------*)
902
903Theorem FRAC_SGN_CASES: !f1 P. ((frac_sgn f1 = ~1) ==> P) /\ ((frac_sgn f1 = 0i) ==> P) /\ ((frac_sgn f1 = 1i) ==> P) ==> P
904Proof
905 REPEAT GEN_TAC THEN
906 ASM_CASES_TAC ``frac_sgn f1 = ~1`` THEN
907 ASM_CASES_TAC ``frac_sgn f1 = 0i`` THEN
908 ASM_CASES_TAC ``frac_sgn f1 = 1i`` THEN
909 UNDISCH_ALL_TAC THEN
910 PROVE_TAC[FRAC_SGN_TOTAL]
911QED
912
913(*--------------------------------------------------------------------------
914 * FRAC_SGN_AINV : thm
915 * |- !f1. ~frac_sgn (frac_ainv f1) = frac_sgn f1
916 *--------------------------------------------------------------------------*)
917
918Theorem FRAC_SGN_AINV: !f1. ~frac_sgn (frac_ainv f1) = frac_sgn f1
919Proof
920 GEN_TAC THEN
921 REWRITE_TAC[frac_sgn_def, frac_ainv_def] THEN
922 FRAC_NMRDNM_TAC THEN
923 REWRITE_TAC[SGN_def] THEN
924 REWRITE_TAC[INT_NEG_EQ, INT_NEG_0] THEN
925 SUBGOAL_THEN ``(~frac_nmr f1 < 0) = (0 < frac_nmr f1)`` SUBST1_TAC THENL
926 [
927 EQ_TAC THEN
928 STRIP_TAC THEN
929 ONCE_REWRITE_TAC[GSYM INT_LT_NEG] THEN
930 PROVE_TAC[INT_NEG_0, INT_NEGNEG]
931 ,
932 RW_TAC int_ss [] THEN
933 PROVE_TAC[INT_LT_ANTISYM, INT_LT_TOTAL]
934 ]
935QED
936
937
938
939(*==========================================================================
940 * one-to-one and onto theorems
941 *==========================================================================*)
942
943(*--------------------------------------------------------------------------
944 * FRAC_AINV_ONE_ONE : thm
945 * |- ONE_ONE frac_ainv
946 *--------------------------------------------------------------------------*)
947
948Theorem FRAC_AINV_ONEONE: ONE_ONE frac_ainv
949Proof
950 REWRITE_TAC[ONE_ONE_DEF] THEN
951 BETA_TAC THEN
952 REPEAT GEN_TAC THEN
953 REWRITE_TAC[frac_ainv_def] THEN
954 FRAC_POS_TAC ``frac_dnm x1`` THEN
955 FRAC_POS_TAC ``frac_dnm x2`` THEN
956 REWRITE_TAC[UNDISCH_ALL (SPECL[``~frac_nmr x1``,``frac_dnm x1``,``~frac_nmr x2``,``frac_dnm x2``] FRAC_EQ)] THEN
957 REWRITE_TAC[INT_EQ_NEG] THEN
958 SUBST_TAC[SPEC ``x1:frac`` (GSYM FRAC), SPEC ``x2:frac`` (GSYM FRAC)] THEN
959 RW_TAC bool_ss [NMR,DNM]
960QED
961
962(*--------------------------------------------------------------------------
963 * FRAC_AINV_ONTO : thm
964 * |- ONTO frac_ainv
965 *--------------------------------------------------------------------------*)
966
967Theorem FRAC_AINV_ONTO: ONTO frac_ainv
968Proof
969 REWRITE_TAC[ONTO_DEF] THEN
970 BETA_TAC THEN
971 GEN_TAC THEN
972 EXISTS_TAC ``frac_ainv y`` THEN
973 PROVE_TAC[FRAC_AINV_AINV]
974QED
975
976
977
978(*==========================================================================
979 * encode whether a fraction is defined or not in the syntax
980 *==========================================================================*)
981
982
983(*==========================================================================
984 * compute the numerator and denominator of a fraction
985 *==========================================================================*)
986
987(*--------------------------------------------------------------------------
988 * FRAC_NMR_SAVE: thm
989 * |- !a1 b1. frac_nmr( frac_save a1 b1 ) = a1
990 *
991 * FRAC_DNM_SAVE: thm
992 * |- !a1 b1. frac_dnm( frac_save a1 b1 ) = &b1 + 1i
993 *--------------------------------------------------------------------------*)
994
995Theorem FRAC_NMR_SAVE: !a1 b1. frac_nmr( frac_save a1 b1 ) = a1
996Proof
997 REPEAT GEN_TAC THEN
998 REWRITE_TAC[frac_save_def] THEN
999 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1000 PROVE_TAC[NMR]
1001QED
1002
1003Theorem FRAC_DNM_SAVE: !a1 b1. frac_dnm( frac_save a1 b1 ) = &b1 + 1i
1004Proof
1005 REPEAT GEN_TAC THEN
1006 REWRITE_TAC[frac_save_def] THEN
1007 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1008 PROVE_TAC[DNM]
1009QED
1010
1011(*--------------------------------------------------------------------------
1012 * FRAC_0_SAVE: thm
1013 * |- frac_0 = frac_save 0 0
1014 *
1015 * FRAC_1_SAVE: thm
1016 * |- frac_1 = frac_save 1 0
1017 *--------------------------------------------------------------------------*)
1018
1019Theorem FRAC_0_SAVE: frac_0 = frac_save 0 0
1020Proof
1021 REPEAT GEN_TAC THEN
1022 REWRITE_TAC[frac_0_def, frac_save_def] THEN
1023 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1024 FRAC_EQ_TAC THEN
1025 ARITH_TAC
1026QED
1027
1028Theorem FRAC_1_SAVE: frac_1 = frac_save 1 0
1029Proof
1030 REPEAT GEN_TAC THEN
1031 REWRITE_TAC[frac_1_def, frac_save_def] THEN
1032 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1033 FRAC_EQ_TAC THEN
1034 ARITH_TAC
1035QED
1036
1037(*--------------------------------------------------------------------------
1038 * FRAC_AINV_SAVE: thm
1039 * |- !a1 b1. frac_ainv (frac_save a1 b1) = frac_save (~a1) b1
1040 *
1041 * RAT_MINV_SAVE: thm
1042 * |- !a1 b1. ~(abs_rat (frac_save a1 b1) = rat_0) ==>
1043 * (rat_minv (abs_rat (frac_save a1 b1)) =
1044 * abs_rat( frac_save (SGN a1 * (& b1 + 1)) (Num (ABS a1 - 1))) )
1045 *--------------------------------------------------------------------------*)
1046
1047Theorem FRAC_AINV_SAVE: !a1 b1. frac_ainv (frac_save a1 b1) = frac_save (~a1) b1
1048Proof
1049 REPEAT GEN_TAC THEN
1050 REWRITE_TAC[frac_ainv_def, frac_save_def] THEN
1051 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1052 FRAC_NMRDNM_TAC THEN
1053 FRAC_EQ_TAC
1054QED
1055
1056
1057Theorem FRAC_MINV_SAVE: !a1 b1. ~(a1=0) ==> (frac_minv (frac_save a1 b1) = frac_save (SGN a1 * (&b1 + 1)) (Num (ABS a1 - 1)))
1058Proof
1059 REPEAT STRIP_TAC THEN
1060 REWRITE_TAC[frac_minv_def, frac_sgn_def, frac_save_def] THEN
1061 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1062 ASSUME_TAC (ARITH_PROVE ``0i < & (Num (ABS a1 - 1)) + 1``) THEN
1063 FRAC_NMRDNM_TAC THEN
1064 FRAC_EQ_TAC THEN
1065 RW_TAC int_ss [SGN_def, GSYM INT_EQ_SUB_RADD] THEN
1066 ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
1067 REWRITE_TAC[INT_OF_NUM] THEN
1068 ARITH_TAC
1069QED
1070
1071
1072(*--------------------------------------------------------------------------
1073 * FRAC_ADD_SAVE: thm
1074 * |- !a1 b1 a2 b2.
1075 * frac_add (frac_save a1 b1) (frac_save a2 b2) =
1076 * frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2)
1077 *
1078 * FRAC_MUL_SAVE: thm
1079 * |- !a1 b1 a2 b2.
1080 * frac_mul (frac_save a1 b1) (frac_save a2 b2) =
1081 * frac_save (a1 * a2) (b1 * b2 + b1 + b2)
1082 *--------------------------------------------------------------------------*)
1083
1084Theorem FRAC_ADD_SAVE:
1085 !a1 b1 a2 b2.
1086 frac_add (frac_save a1 b1) (frac_save a2 b2) =
1087 frac_save (a1 * &b2 + a2 * &b1 + a1 + a2) (b1 * b2 + b1 + b2)
1088Proof
1089 REPEAT GEN_TAC THEN
1090 REWRITE_TAC[frac_add_def, frac_save_def] THEN
1091 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1092 ASSUME_TAC (ARITH_PROVE ``0i < &b2 + 1``) THEN
1093 FRAC_NMRDNM_TAC THEN
1094 FRAC_EQ_TAC THEN
1095 SIMP_TAC (srw_ss()) [INT_LDISTRIB, INT_RDISTRIB, GSYM INT_ADD,
1096 AC INT_ADD_COMM INT_ADD_ASSOC]
1097QED
1098
1099Theorem FRAC_MUL_SAVE:
1100 !a1 b1 a2 b2. frac_mul (frac_save a1 b1) (frac_save a2 b2) =
1101 frac_save (a1 * a2) (b1 * b2 + b1 + b2)
1102Proof
1103 REPEAT GEN_TAC THEN
1104 REWRITE_TAC[frac_mul_def, frac_save_def] THEN
1105 ASSUME_TAC (ARITH_PROVE ``0i < &b1 + 1``) THEN
1106 ASSUME_TAC (ARITH_PROVE ``0i < &b2 + 1``) THEN
1107 FRAC_NMRDNM_TAC THEN
1108 FRAC_EQ_TAC THEN
1109 REWRITE_TAC[INT_ADD_CALCULATE, INT_MUL_CALCULATE, INT_EQ_CALCULATE] THEN
1110 RW_TAC arith_ss [arithmeticTheory.LEFT_ADD_DISTRIB,
1111 arithmeticTheory.RIGHT_ADD_DISTRIB] THEN
1112 ARITH_TAC
1113QED
1114
1115(*==========================================================================
1116 * end of theory
1117 *==========================================================================*)
1118