1structure fracLib :> fracLib = 2struct 3 4open HolKernel boolLib Parse bossLib; 5 6(* interactive mode 7app load ["pairTheory", "pairLib", "integerTheory","intLib","intSyntax", 8 "ringLib", "integerRingTheory","integerRingLib", 9 "intExtensionTheory", "intExtensionLib", "jbUtils", 10 "fracTheory","fracUtils", "fracSyntax"]; 11*) 12 13open 14 arithmeticTheory 15 pairTheory pairLib integerTheory intLib intSyntax 16 ringLib integerRingTheory integerRingLib 17 intExtensionTheory intExtensionLib 18 jbUtils fracTheory fracUtils fracSyntax; 19 20val ERR = mk_HOL_ERR "fracLib" 21 22(*========================================================================== 23 * equivalence of fractions 24 *==========================================================================*) 25 26(*-------------------------------------------------------------------------- 27 * FRAC_EQ_CONV : conv 28 * 29 * (abs_frac (a1,b1) = abs_frac (a2,b2) 30 * ---------------------------------------------------- 31 * 0<b1, 0<b2 |- (abs_frac (a1,b1) = abs_frac (a1,b1)) 32 * = (a1 = a2) /\ (b1 = b2) : thm 33 *--------------------------------------------------------------------------*) 34 35val FRAC_EQ_CONV:conv = fn term1 => 36let 37 val eqn = dest_neg term1; 38 val (lhs,rhs) = dest_eq eqn; 39 val (lhc, lha) = dest_comb lhs; 40 val (rhc, rha ) = dest_comb rhs; 41 val (a1,b1) = dest_pair lha; 42 val (a2,b2) = dest_pair rha; 43in 44 UNDISCH_ALL (SPECL[a1,b1,a2,b2] FRAC_EQ) 45end 46handle HOL_ERR _ => raise ERR "FRAC_EQ_CONV" ""; 47 48(*-------------------------------------------------------------------------- 49 * FRAC_NOTEQ_CONV : conv 50 * 51 * ~((abs_frac (a1,b1) = abs_frac (a2,b2)) 52 * ---------------------------------------------------- 53 * 0<b1, 0<b2 |- ~(abs_frac (a1,b1) = abs_frac (a2,b2)) 54 * = ~(a1 = a2) \/ ~(b1 = b2) 55 *--------------------------------------------------------------------------*) 56 57val FRAC_NOTEQ_CONV:conv = fn term1 => 58let 59 val eqn = dest_neg term1; 60 val (lhs,rhs) = dest_eq eqn; 61 val (lhc, lha) = dest_comb lhs; 62 val (rhc, rha ) = dest_comb rhs; 63 val (a1,b1) = dest_pair lha; 64 val (a2,b2) = dest_pair rha; 65in 66 UNDISCH_ALL (SPECL[a1,b1,a2,b2] FRAC_NOT_EQ) 67end 68handle HOL_ERR _ => raise ERR "FRAC_NOTEQ_CONV" ""; 69 70(*-------------------------------------------------------------------------- 71 * FRAC_EQ_TAC : tactic 72 * 73 * A ?- abs_frac(a1,b1) = abs_frac(a2,b2) 74 * ========================================= FRAC_EQ_TAC 75 * A ?- a1=a2 | A ?- b1=b2 76 *--------------------------------------------------------------------------*) 77 78val FRAC_EQ_TAC:tactic = fn (asm_list,goal) => 79let 80 val (lhs,rhs) = dest_eq goal; 81 val (lhc, lha) = dest_comb lhs; 82 val (rhc, rha ) = dest_comb rhs; 83 val (a1,b1) = dest_pair lha; 84 val (a2,b2) = dest_pair rha; 85in 86 let 87 val subgoal1 = mk_eq(a1,a2); 88 val subgoal2 = mk_eq(b1,b2); 89 in 90 ( 91 [(asm_list,subgoal1), (asm_list,subgoal2)], 92 fn thms => MP 93 (SPEC b2 (SPEC a2 (SPEC b1 (SPEC a1 ( 94 prove(``!a1 b1 a2 b2. (a1=a2) /\ (b1=b2) ==> (abs_frac(a1,b1)=abs_frac(a2,b2))``, RW_TAC int_ss []) 95 ))))) 96 (LIST_CONJ thms) 97 ) 98 end 99end 100handle HOL_ERR _ => raise ERR "FRAC_EQ_TAC" ""; 101 102 103(*========================================================================== 104 * some useful conversion and tactics about 105 * positive and non-zero numbers in the context of fractions 106 *==========================================================================*) 107 108(*-------------------------------------------------------------------------- 109 * frac_pos_conv : term list -> conv 110 *--------------------------------------------------------------------------*) 111 112fun frac_pos_conv (asm_list:term list) (t1:term) = 113 if (in_list asm_list ``0i < ^t1``) then 114 ASSUME ``0i < ^t1`` 115 else 116 if (is_comb t1) then 117 let 118 val (rator, rand) = dest_comb t1; 119 in 120 if (is_mult t1) then 121 let 122 val (fac1, fac2) = dest_mult t1; 123 val fac1_thm = frac_pos_conv asm_list fac1; 124 val fac2_thm = frac_pos_conv asm_list fac2; 125 in 126 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_MUL_POS_SIGN) 127 end 128 else if (rator=frac_dnm_tm) then 129 SPEC rand FRAC_DNMPOS 130 else if (rator=``ABS``) andalso (in_list asm_list ``~(^rand = 0)``) then 131 UNDISCH (SPEC rand INT_ABS_NOT0POS) 132 else if (is_int_literal t1) then 133 EQT_ELIM (ARITH_CONV ``0 < ^t1``) 134 else 135 ASSUME ``0i < ^t1`` 136 end 137 else 138 ASSUME ``0i < ^t1``; 139 140(*-------------------------------------------------------------------------- 141 * frac_not0_conv : term list -> conv 142 *--------------------------------------------------------------------------*) 143 144fun frac_not0_conv (asm_list:term list) (t1:term) = 145 if (in_list asm_list ``~(^t1 = 0i)``) then 146 ASSUME ``~(^t1 = 0i)`` 147 else 148 if (is_comb t1) then 149 let 150 val (rator, rand) = dest_comb t1; 151 in 152 if (is_mult t1) then 153 let 154 val (fac1, fac2) = dest_mult t1; 155 val fac1_thm = frac_not0_conv asm_list fac1; 156 val fac2_thm = frac_not0_conv asm_list fac2; 157 in 158 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_NOT0_MUL) 159 end 160 else if (rator=frac_dnm_tm) then 161 MP (SPEC t1 INT_GT0_IMP_NOT0) (SPEC rand FRAC_DNMPOS) 162 else if (rator=``SGN``) andalso (in_list asm_list ``~(^rand = 0)``) then 163 UNDISCH (SPEC rand INT_NOT0_SGNNOT0) 164 else if (is_int_literal t1) then 165 EQT_ELIM (ARITH_CONV ``~(^t1 = 0i)``) 166 else 167 ASSUME ``~(^t1 = 0i)`` 168 end 169 else 170 ASSUME ``~(^t1 = 0i)``; 171 172(*-------------------------------------------------------------------------- 173 * FRAC_POS_CONV : conv 174 *--------------------------------------------------------------------------*) 175 176val FRAC_POS_CONV = frac_pos_conv []; 177 178(*-------------------------------------------------------------------------- 179 * FRAC_NOT0_CONV : conv 180 *--------------------------------------------------------------------------*) 181 182val FRAC_NOT0_CONV = frac_not0_conv []; 183 184(*-------------------------------------------------------------------------- 185 * FRAC_POS_TAC : term -> tactic 186 *--------------------------------------------------------------------------*) 187 188fun FRAC_POS_TAC term1 (asm_list, goal) = 189 (ASSUME_TAC (frac_pos_conv asm_list term1)) (asm_list, goal); 190 191(*-------------------------------------------------------------------------- 192 * FRAC_NOT0_TAC : term -> tactic 193 *--------------------------------------------------------------------------*) 194 195fun FRAC_NOT0_TAC term1 (asm_list, goal) = 196 (ASSUME_TAC (frac_not0_conv asm_list term1)) (asm_list, goal); 197 198 199(*========================================================================== 200 * numerator and denominator extraction 201 *==========================================================================*) 202 203(*-------------------------------------------------------------------------- 204 * FRAC_NMR_CONV: conv 205 * 206 * frac_nmr (abs_frac (a1,b1)) 207 * ----------------------------------------- 208 * 0 < b1 |- (frac_nmr (abs_frac (a1,b1)) = a1) 209 *--------------------------------------------------------------------------*) 210 211val FRAC_NMR_CONV:conv = fn term => 212let 213 val (nmr,f) = dest_comb term; 214 val (abs,args) = dest_comb f; 215 val (a,b) = dest_pair args; 216in 217 UNDISCH_ALL(SPEC b (SPEC a NMR)) 218end 219handle HOL_ERR _ => raise ERR "FRAC_NMR_CONV" ""; 220 221 222(*-------------------------------------------------------------------------- 223 * FRAC_DNM_CONV: conv 224 * 225 * frac_dnm (abs_frac (a1,b1)) 226 * ----------------------------------------- 227 * 0 < b1 |- (frac_dnm (abs_frac (a1,b1)) = a1) 228 *--------------------------------------------------------------------------*) 229 230val FRAC_DNM_CONV:conv = fn term => 231let 232 val (nmr,f) = dest_comb term; 233 val (abs,args) = dest_comb f; 234 val (a,b) = dest_pair args; 235in 236 UNDISCH_ALL(SPEC b (SPEC a DNM)) 237end 238handle HOL_ERR _ => raise ERR "FRAC_DNM_CONV" ""; 239 240(*-------------------------------------------------------------------------- 241 * frac_nmr_tac : term*term -> tactic 242 *--------------------------------------------------------------------------*) 243 244fun frac_nmr_tac (asm_list:term list) (nmr,dnm) = 245 let 246 val asm_thm = frac_pos_conv asm_list dnm; 247 val sub_thm = DISCH_ALL (FRAC_NMR_CONV ``frac_nmr( abs_frac (^nmr, ^dnm) )``); 248 in 249 TRY ( 250 SUBST1_TAC (MP sub_thm asm_thm) 251 ) 252 end; 253 254(*-------------------------------------------------------------------------- 255 * frac_dnm_tac : term*term -> tactic 256 *--------------------------------------------------------------------------*) 257 258fun frac_dnm_tac (asm_list:term list) (nmr,dnm) = 259 let 260 val asm_thm = frac_pos_conv asm_list dnm; 261 val sub_thm = DISCH_ALL (FRAC_DNM_CONV ``frac_dnm( abs_frac (^nmr, ^dnm) )``); 262 in 263 TRY ( 264 SUBST1_TAC (MP sub_thm asm_thm) 265 ) 266 end; 267 268(*-------------------------------------------------------------------------- 269 * FRAC_NMRDNM_TAC : tactic 270 * 271 * simplify resp. nmr(abs_frac(a1,b1)) to a1 and frac_dnm(abs_frac(a1,b1)) to b1 272 *--------------------------------------------------------------------------*) 273 274fun FRAC_NMRDNM_TAC (asm_list, goal) = 275let 276 val term_list = extract_frac_fun [frac_nmr_tm,frac_dnm_tm] goal; 277 val nmr_term_list = map (fn x => let val (rator,nmr,dnm) = x in (nmr,dnm) end) (filter (fn x => let val (a1,a2,a3) = x in a1=frac_nmr_tm end) term_list); 278 val dnm_term_list = map (fn x => let val (rator,nmr,dnm) = x in (nmr,dnm) end) (filter (fn x => let val (a1,a2,a3) = x in a1=frac_dnm_tm end) term_list); 279in 280 ( 281 MAP_EVERY (frac_nmr_tac asm_list) nmr_term_list THEN 282 MAP_EVERY (frac_dnm_tac asm_list) dnm_term_list THEN 283 SIMP_TAC int_ss [INT_MUL_LID, INT_MUL_RID, INT_MUL_LZERO, INT_MUL_RZERO] 284 ) (asm_list,goal) 285end 286handle HOL_ERR _ => raise ERR "FRAC_NMRDNM_TAC" ""; 287 288(*========================================================================== 289 * calculation 290 *==========================================================================*) 291 292(*-------------------------------------------------------------------------- 293 * subst_thm : term -> thm 294 *--------------------------------------------------------------------------*) 295 296fun subst_thm (top_rator:term) = 297 if top_rator=frac_add_tm then 298 FRAC_ADD_CALCULATE 299 else if top_rator=frac_sub_tm then 300 FRAC_SUB_CALCULATE 301 else if top_rator=frac_mul_tm then 302 FRAC_MULT_CALCULATE 303 else if top_rator=frac_div_tm then 304 FRAC_DIV_CALCULATE 305 else if top_rator=frac_ainv_tm then 306 FRAC_AINV_CALCULATE 307 else if top_rator=frac_minv_tm then 308 FRAC_MINV_CALCULATE 309 else 310 REFL ``x:frac``; 311 312(*-------------------------------------------------------------------------- 313 * FRAC_CALC_CONV : term -> conv 314 * 315 * t1 316 * ------------------------- 317 * |- t1 = abs_frac(a1,b1) 318 *--------------------------------------------------------------------------*) 319fun FRAC_CALC_CONV (t1:term) = 320let 321 val (top_rator, top_rands) = dest_frac t1; 322 val thm = REFL t1; 323in 324 if top_rator=``abs_frac`` then 325 thm 326 else 327 if top_rator=t1 orelse top_rator=``rep_rat`` then 328 if is_var top_rator orelse top_rator=``rep_rat`` then 329 SUBST [``x:frac`` |-> SPEC t1 (GSYM FRAC)] ``^t1 = x:frac`` thm 330 else 331 if t1=``frac_0`` then 332 frac_0_def 333 else 334 frac_1_def 335 else 336 if tl top_rands = [] then 337 let 338 val fst_arg = FRAC_CALC_CONV (hd top_rands); 339 val (fst_nmr,fst_dnm) = dest_pair (snd(dest_comb (snd(dest_eq (snd(dest_thm fst_arg)) )) )); 340 val fst_var = genvar ``:frac``; 341 in 342 let 343 val thm1 = SUBST [fst_var |-> fst_arg] ``^t1 = ^top_rator ^fst_var`` thm; 344 val (lhs, rhs) = dest_eq( snd (dest_thm thm1) ); 345 val lhs_var = genvar ``:frac``; 346 in 347 SUBST [lhs_var |-> UNDISCH_ALL (SPECL[fst_nmr, fst_dnm] (subst_thm top_rator))] ``^lhs = ^lhs_var`` thm1 348 end 349 end 350 else 351 let 352 val fst_arg = FRAC_CALC_CONV (hd top_rands); 353 val snd_arg = FRAC_CALC_CONV (hd (tl top_rands)); 354 val (fst_nmr,fst_dnm) = dest_pair (snd(dest_comb (snd(dest_eq (snd(dest_thm fst_arg)) )) )); 355 val (snd_nmr,snd_dnm) = dest_pair (snd(dest_comb (snd(dest_eq (snd(dest_thm snd_arg)) )) )); 356 val fst_var = genvar ``:frac``; 357 val snd_var = genvar ``:frac``; 358 in 359 let 360 val thm1 = SUBST [fst_var |-> fst_arg, snd_var |-> snd_arg] ``^t1 = ^top_rator ^fst_var ^snd_var`` thm; 361 val (lhs, rhs) = dest_eq( snd (dest_thm thm1) ); 362 val lhs_var = genvar ``:frac``; 363 in 364 SUBST [lhs_var |-> UNDISCH_ALL (SPECL[fst_nmr, fst_dnm, snd_nmr, snd_dnm] (subst_thm top_rator))] ``^lhs = ^lhs_var`` thm1 365 end 366 end 367end; 368 369(* ---------- test cases ---------- * 370 FRAC_CALC_CONV ``frac_add (abs_frac(3i,4i)) (abs_frac(4i,5i))``; 371 FRAC_CALC_CONV ``frac_add f1 f2``; 372 FRAC_CALC_CONV ``frac_add f1 ( frac_sub (abs_frac(4i,5i)) f2)``; 373 FRAC_CALC_CONV ``frac_add f1 ( frac_div (abs_frac(4i,5i)) f2)``; 374 FRAC_CALC_CONV ``frac_add (frac_ainv f1) ( frac_mul f2 (frac_minv f3))``; 375 FRAC_CALC_CONV ``frac_add (frac_ainv frac_1) frac_0``; 376 FRAC_CALC_CONV ``frac_sub (rep_rat r1) frac_0``; 377 FRAC_CALC_CONV ``frac_sub (frac_add (rep_rat r1) (rep_rat r2)) frac_0``; 378 * ---------- test cases ---------- *) 379 380 381(*-------------------------------------------------------------------------- 382 * FRAC_STRICT_CALC_TAC : tactic 383 *--------------------------------------------------------------------------*) 384 385fun FRAC_STRICT_CALC_TAC (asm_list,goal) = 386 let 387 val frac_terms = extract_frac goal; 388 val calc_thms = map FRAC_CALC_CONV frac_terms; 389 in 390 ( 391 SUBST_TAC calc_thms 392 ) (asm_list,goal) 393 end 394handle HOL_ERR _ => raise ERR "FRAC_STRICT_CALCULATE_TAC" ""; 395 396 397 398(*-------------------------------------------------------------------------- 399 * frac_calc_tac : term list -> tactic 400 *--------------------------------------------------------------------------*) 401 402fun frac_calc_tac (frac_terms:term list) (asm_list:term list,goal:term) = 403 let 404 (* generate calculation theorems for these terms *) 405 val calc_thms = map FRAC_CALC_CONV frac_terms; 406 (* extract hypotheses and conclusions *) 407 val (calc_thms_hyps,calc_thms_concls) = unzip (map dest_thm calc_thms); (* was calc_asms2 *) 408 (* extract left-hand sides and right-hand sides of calculation theorem conclusions *) 409 val calc_thms_conls_sides = map dest_eq calc_thms_concls; 410 (* merge lists of hypotheses *) 411 val calc_hyps = list_xmerge (map (fn x => fst (dest_thm x)) calc_thms); 412 (* divide lists of hypotheses into parts ``0 < x`` and ``~(x = 0)`` *) 413 val (calc_hyps_gt0, calc_hyps_not0) = partition is_less calc_hyps; 414 415 (* generate theorems for gt0 and not0 hypotheses *) 416 val asm_gt0_thms = map (fn x => frac_pos_conv asm_list (snd (dest_less x)) ) calc_hyps_gt0; 417 val asm_not0_thms = map (fn x => frac_not0_conv asm_list (fst (dest_eq (dest_neg x))) ) calc_hyps_not0; 418 val precond_thms = asm_gt0_thms @ asm_not0_thms; 419 420 (* partition them *) 421 fun proved (x:thm) = hyp x = [] orelse List.all (in_list asm_list) (hyp x); 422 val (asms_proved,asms_toprove) = partition proved (asm_gt0_thms @ asm_not0_thms); 423 424 (* hypothesis, TODO: eventuell gleich triviale entfernen *) 425 val asms_hyp = list_xmerge (map (fn x => fst (dest_thm x)) asms_toprove); 426 427 (* generate subgoal: prove the proposition in which the fractions are subsituted by their calculated values *) 428 val subs_sg = (asm_list, subst (map (fn (lhs,rhs) => (lhs |-> rhs)) calc_thms_conls_sides) goal); 429 (* generate subgoals: prove the hypothesis of the hypothesis of the calculation theorems *) 430 val hyps_sgs = map (fn x => (asm_list,x)) asms_hyp; 431 432 (* TODO: statt oben hier noch ein paar Theoreme erg��nzen, die dann mit thms konkateniert werden (UOK) *) 433 434 (*val thms = map mk_thm ([subs_sg] @ hyps_sgs);*) 435 436 in 437 ([subs_sg] @ hyps_sgs , fn (thms:thm list) => 438 let 439 (* first theorem: the "main subgoal" *) 440 val subs_thm = hd thms; 441 (* all other theorems: hyptothesis subgoals *) 442 val asm_thms = tl thms; 443 444 (* erster Schritt: baue Voraussetzungen f��r die calc_thms zusammen (UOK) *) 445 446 447 (* extract proof from asm_thms list (TODO: other list) *) 448 fun proof_from_asm_thms (t1:term) = 449 let 450 val corres_asm_thm = List.find (fn x => concl x = t1) asm_thms; 451 val corres_pro_thm = List.find (fn x => concl x = t1) asms_proved; 452 in 453 if (isSome corres_pro_thm) then 454 valOf corres_pro_thm 455 else if (isSome corres_asm_thm) then 456 valOf corres_asm_thm 457 else 458 ASSUME ``T`` 459 end; 460 461 462 463 fun get_step1_proofs (thm1:thm) = map proof_from_asm_thms (hyp thm1); 464 fun mapped_precond_thm (thm1:thm) = LIST_MP (List.rev (get_step1_proofs thm1)) (DISCH_ALL thm1); 465 466 val step1_proofs = map mapped_precond_thm precond_thms; 467 468 469 fun proof_from_step1 (t1:term) = 470 let 471 val corres_asm_thm = List.find (fn x => concl x = t1) step1_proofs; 472 (*val corres_pro_thm = List.find (fn x => concl x = t1) asms_proved;*) 473 in 474 (*if (isSome corres_pro_thm) then 475 valOf corres_pro_thm 476 else*) if (isSome corres_asm_thm) then 477 valOf corres_asm_thm 478 else 479 ASSUME ``T`` 480 end; 481 482 483 fun get_step2_proofs (thm1:thm) = map proof_from_step1 (hyp thm1); 484 fun step2_thm (thm1:thm) = LIST_MP (List.rev (get_step2_proofs thm1)) (DISCH_ALL thm1); 485 486 val step2_proofs = map step2_thm calc_thms; 487 in 488 (* PROBLEM: calc_thms bringen viele Hypothesen rein -> eliminieren *) 489 SUBS (map GSYM step2_proofs) subs_thm 490 end 491 ) 492 end 493handle HOL_ERR _ => raise ERR "FRAC_CALC_TAC" ""; 494 495 496(*-------------------------------------------------------------------------- 497 * FRAC_CALCTERM_TAC : term -> tactic 498 *--------------------------------------------------------------------------*) 499 500fun FRAC_CALCTERM_TAC (t1:term) (asm_list:term list,goal:term) = 501 (frac_calc_tac [t1]) (asm_list:term list,goal:term); 502 503(*-------------------------------------------------------------------------- 504 * FRAC_CALC_TAC : tactic 505 *--------------------------------------------------------------------------*) 506 507fun FRAC_CALC_TAC (asm_list, goal) = 508 (frac_calc_tac (extract_frac goal)) (asm_list, goal); 509 510(*-------------------------------------------------------------------------- 511 * FRAC_STRICT_CALCEQ_TAC : tactic 512 *--------------------------------------------------------------------------*) 513 514val FRAC_STRICT_CALCEQ_TAC = 515 FRAC_STRICT_CALC_TAC THEN 516 REWRITE_TAC[FRAC_EQ_ALT] THEN 517 FRAC_NMRDNM_TAC THEN 518 INT_CALCEQ_TAC; 519 520(*-------------------------------------------------------------------------- 521 * FRAC_CALCEQ_TAC : tactic 522 *--------------------------------------------------------------------------*) 523 524val FRAC_CALCEQ_TAC = 525 FRAC_CALC_TAC THEN 526 REWRITE_TAC[FRAC_EQ_ALT] THEN 527 FRAC_NMRDNM_TAC THEN 528 INT_CALCEQ_TAC; 529 530(*========================================================================== 531 * transformation of fractions into "valid fractions" 532 *==========================================================================*) 533 534(*-------------------------------------------------------------------------- 535 * frac_saveterm_conv : conv 536 *--------------------------------------------------------------------------*) 537 538fun frac_saveterm_conv t1 = 539 let 540 val (comb, args) = dest_comb t1; 541 val (a1,b1) = dest_pair args; 542 val a2 = a1; 543 val b2x = ``Num (^b1 - 1i)``; 544 val b2 = ``& ^b2x + 1i``; 545 val to_show = ``abs_frac (^a1, ^b1) = frac_save ^a1 (Num (^b1 - 1i))``; 546 val dnm_thm1 = ARITH_PROVE ``0i < ^b1``; 547 val dnm_thm2 = ARITH_PROVE ``0i < ^b2``; 548 val frac_thm = SPECL[a1,b1,a1,b2] FRAC_EQ 549 in 550 REWRITE_RULE [SIMP_CONV int_ss [] b2x] (EQT_ELIM (REWRITE_CONV [frac_save_def,LIST_MP [dnm_thm1,dnm_thm2] frac_thm,SIMP_CONV int_ss [] ``^b1 = ^b2``] to_show)) 551 end; 552 553(*-------------------------------------------------------------------------- 554 * FRAC_SAVE_CONV : conv 555 *--------------------------------------------------------------------------*) 556 557fun FRAC_SAVE_CONV t1 = 558 REWRITE_CONV (map (TRY_CONV frac_saveterm_conv) (extract_abs_frac t1)) t1; 559 560(*-------------------------------------------------------------------------- 561 * FRAC_SAVE_TAC : tactic 562 *--------------------------------------------------------------------------*) 563 564val FRAC_SAVE_TAC = CONV_TAC FRAC_SAVE_CONV; 565 566(*========================================================================== 567 * end of structure 568 *==========================================================================*) 569end; 570