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 tmem ���0i < ^t1��� asm_list then ASSUME ���0i < ^t1��� 114 else 115 if is_comb t1 then 116 let 117 val (rator, rand) = dest_comb t1 118 in 119 if is_mult t1 then 120 let 121 val (fac1, fac2) = dest_mult t1; 122 val fac1_thm = frac_pos_conv asm_list fac1; 123 val fac2_thm = frac_pos_conv asm_list fac2; 124 in 125 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_MUL_POS_SIGN) 126 end 127 else if rator ~~ frac_dnm_tm then SPEC rand FRAC_DNMPOS 128 else if rator ~~ ���ABS��� andalso tmem ���~(^rand = 0)��� asm_list then 129 UNDISCH (SPEC rand INT_ABS_NOT0POS) 130 else if (is_int_literal t1) then 131 EQT_ELIM (ARITH_CONV ``0 < ^t1``) 132 else ASSUME ``0i < ^t1`` 133 end 134 else 135 ASSUME ``0i < ^t1``; 136 137(*-------------------------------------------------------------------------- 138 * frac_not0_conv : term list -> conv 139 *--------------------------------------------------------------------------*) 140 141fun frac_not0_conv (asm_list:term list) (t1:term) = 142 if tmem ���~(^t1 = 0i)��� asm_list then ASSUME ``~(^t1 = 0i)`` 143 else if is_comb t1 then 144 let 145 val (rator, rand) = dest_comb t1 146 in 147 if is_mult t1 then 148 let 149 val (fac1, fac2) = dest_mult t1; 150 val fac1_thm = frac_not0_conv asm_list fac1; 151 val fac2_thm = frac_not0_conv asm_list fac2; 152 in 153 LIST_MP [fac1_thm,fac2_thm] (SPECL[fac1,fac2] INT_NOT0_MUL) 154 end 155 else if rator ~~ frac_dnm_tm then 156 MP (SPEC t1 INT_GT0_IMP_NOT0) (SPEC rand FRAC_DNMPOS) 157 else if rator ~~ ���SGN��� andalso tmem ���~(^rand = 0)��� asm_list then 158 UNDISCH (SPEC rand INT_NOT0_SGNNOT0) 159 else if (is_int_literal t1) then EQT_ELIM (ARITH_CONV ``~(^t1 = 0i)``) 160 else 161 ASSUME ``~(^t1 = 0i)`` 162 end 163 else 164 ASSUME ``~(^t1 = 0i)``; 165 166(*-------------------------------------------------------------------------- 167 * FRAC_POS_CONV : conv 168 *--------------------------------------------------------------------------*) 169 170val FRAC_POS_CONV = frac_pos_conv []; 171 172(*-------------------------------------------------------------------------- 173 * FRAC_NOT0_CONV : conv 174 *--------------------------------------------------------------------------*) 175 176val FRAC_NOT0_CONV = frac_not0_conv []; 177 178(*-------------------------------------------------------------------------- 179 * FRAC_POS_TAC : term -> tactic 180 *--------------------------------------------------------------------------*) 181 182fun FRAC_POS_TAC term1 (asm_list, goal) = 183 (ASSUME_TAC (frac_pos_conv asm_list term1)) (asm_list, goal); 184 185(*-------------------------------------------------------------------------- 186 * FRAC_NOT0_TAC : term -> tactic 187 *--------------------------------------------------------------------------*) 188 189fun FRAC_NOT0_TAC term1 (asm_list, goal) = 190 (ASSUME_TAC (frac_not0_conv asm_list term1)) (asm_list, goal); 191 192 193(*========================================================================== 194 * numerator and denominator extraction 195 *==========================================================================*) 196 197(*-------------------------------------------------------------------------- 198 * FRAC_NMR_CONV: conv 199 * 200 * frac_nmr (abs_frac (a1,b1)) 201 * ----------------------------------------- 202 * 0 < b1 |- (frac_nmr (abs_frac (a1,b1)) = a1) 203 *--------------------------------------------------------------------------*) 204 205val FRAC_NMR_CONV:conv = fn term => 206let 207 val (nmr,f) = dest_comb term; 208 val (abs,args) = dest_comb f; 209 val (a,b) = dest_pair args; 210in 211 UNDISCH_ALL(SPEC b (SPEC a NMR)) 212end 213handle HOL_ERR _ => raise ERR "FRAC_NMR_CONV" ""; 214 215 216(*-------------------------------------------------------------------------- 217 * FRAC_DNM_CONV: conv 218 * 219 * frac_dnm (abs_frac (a1,b1)) 220 * ----------------------------------------- 221 * 0 < b1 |- (frac_dnm (abs_frac (a1,b1)) = a1) 222 *--------------------------------------------------------------------------*) 223 224val FRAC_DNM_CONV:conv = fn term => 225let 226 val (nmr,f) = dest_comb term; 227 val (abs,args) = dest_comb f; 228 val (a,b) = dest_pair args; 229in 230 UNDISCH_ALL(SPEC b (SPEC a DNM)) 231end 232handle HOL_ERR _ => raise ERR "FRAC_DNM_CONV" ""; 233 234(*-------------------------------------------------------------------------- 235 * frac_nmr_tac : term*term -> tactic 236 *--------------------------------------------------------------------------*) 237 238fun frac_nmr_tac (asm_list:term list) (nmr,dnm) = 239 let 240 val asm_thm = frac_pos_conv asm_list dnm; 241 val sub_thm = DISCH_ALL (FRAC_NMR_CONV ``frac_nmr( abs_frac (^nmr, ^dnm) )``); 242 in 243 TRY ( 244 SUBST1_TAC (MP sub_thm asm_thm) 245 ) 246 end; 247 248(*-------------------------------------------------------------------------- 249 * frac_dnm_tac : term*term -> tactic 250 *--------------------------------------------------------------------------*) 251 252fun frac_dnm_tac (asm_list:term list) (nmr,dnm) = 253 let 254 val asm_thm = frac_pos_conv asm_list dnm; 255 val sub_thm = DISCH_ALL (FRAC_DNM_CONV ``frac_dnm( abs_frac (^nmr, ^dnm) )``); 256 in 257 TRY ( 258 SUBST1_TAC (MP sub_thm asm_thm) 259 ) 260 end; 261 262(*-------------------------------------------------------------------------- 263 * FRAC_NMRDNM_TAC : tactic 264 * 265 * simplify resp. nmr(abs_frac(a1,b1)) to a1 and frac_dnm(abs_frac(a1,b1)) to b1 266 *--------------------------------------------------------------------------*) 267 268fun FRAC_NMRDNM_TAC (asm_list, goal) = 269 let 270 val term_list = extract_frac_fun [frac_nmr_tm,frac_dnm_tm] goal 271 val nmr_term_list = 272 map (fn x => let val (rator,nmr,dnm) = x in (nmr,dnm) end) 273 (filter (fn x => let val (a1,a2,a3) = x in a1 ~~ frac_nmr_tm end) 274 term_list) 275 val dnm_term_list = 276 map (fn x => let val (rator,nmr,dnm) = x in (nmr,dnm) end) 277 (filter (fn x => let val (a1,a2,a3) = x in a1 ~~ frac_dnm_tm end) 278 term_list) 279 in 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 FRAC_ADD_CALCULATE 298 else if top_rator ~~ frac_sub_tm then FRAC_SUB_CALCULATE 299 else if top_rator ~~ frac_mul_tm then FRAC_MULT_CALCULATE 300 else if top_rator ~~ frac_div_tm then FRAC_DIV_CALCULATE 301 else if top_rator ~~ frac_ainv_tm then FRAC_AINV_CALCULATE 302 else if top_rator ~~ frac_minv_tm then FRAC_MINV_CALCULATE 303 else 304 REFL ���x:frac���; 305 306(*-------------------------------------------------------------------------- 307 * FRAC_CALC_CONV : term -> conv 308 * 309 * t1 310 * ------------------------- 311 * |- t1 = abs_frac(a1,b1) 312 *--------------------------------------------------------------------------*) 313fun FRAC_CALC_CONV (t1:term) = 314 let 315 val (top_rator, top_rands) = dest_frac t1 316 val thm = REFL t1 317 in 318 if top_rator ~~ ``abs_frac`` then thm 319 else if top_rator ~~ t1 orelse top_rator ~~ ``rep_rat`` then 320 if is_var top_rator orelse top_rator ~~ ``rep_rat`` then 321 SUBST [``x:frac`` |-> SPEC t1 (GSYM FRAC)] ``^t1 = x:frac`` thm 322 else if t1 ~~ ``frac_0`` then frac_0_def 323 else frac_1_def 324 else if null (tl top_rands) then 325 let 326 val fst_arg = FRAC_CALC_CONV (hd top_rands) 327 val (fst_nmr,fst_dnm) = 328 dest_pair (snd(dest_comb (snd(dest_eq (snd(dest_thm fst_arg)) )) )) 329 val fst_var = genvar ``:frac`` 330 in 331 let 332 val thm1 = 333 SUBST [fst_var |-> fst_arg] ``^t1 = ^top_rator ^fst_var`` thm 334 val (lhs, rhs) = dest_eq( snd (dest_thm thm1) ) 335 val lhs_var = genvar ``:frac`` 336 in 337 SUBST [lhs_var |-> 338 UNDISCH_ALL (SPECL[fst_nmr, fst_dnm] 339 (subst_thm top_rator))] 340 ``^lhs = ^lhs_var`` thm1 341 end 342 end 343 else 344 let 345 val fst_arg = FRAC_CALC_CONV (hd top_rands) 346 val snd_arg = FRAC_CALC_CONV (hd (tl top_rands)) 347 val (fst_nmr,fst_dnm) = 348 dest_pair (snd(dest_comb (snd(dest_eq (snd(dest_thm fst_arg)) )) )) 349 val (snd_nmr,snd_dnm) = 350 dest_pair (snd(dest_comb (snd(dest_eq (snd(dest_thm snd_arg)) )) )) 351 val fst_var = genvar ``:frac``; 352 val snd_var = genvar ``:frac``; 353 in 354 let 355 val thm1 = SUBST [fst_var |-> fst_arg, snd_var |-> snd_arg] 356 ``^t1 = ^top_rator ^fst_var ^snd_var`` thm 357 val (lhs, rhs) = dest_eq( snd (dest_thm thm1) ) 358 val lhs_var = genvar ``:frac``; 359 in 360 SUBST [lhs_var |-> 361 UNDISCH_ALL (SPECL[fst_nmr, fst_dnm, snd_nmr, snd_dnm] 362 (subst_thm top_rator))] 363 ``^lhs = ^lhs_var`` thm1 364 end 365 end 366 end; 367 368(* ---------- test cases ---------- * 369 FRAC_CALC_CONV ``frac_add (abs_frac(3i,4i)) (abs_frac(4i,5i))``; 370 FRAC_CALC_CONV ``frac_add f1 f2``; 371 FRAC_CALC_CONV ``frac_add f1 ( frac_sub (abs_frac(4i,5i)) f2)``; 372 FRAC_CALC_CONV ``frac_add f1 ( frac_div (abs_frac(4i,5i)) f2)``; 373 FRAC_CALC_CONV ``frac_add (frac_ainv f1) ( frac_mul f2 (frac_minv f3))``; 374 FRAC_CALC_CONV ``frac_add (frac_ainv frac_1) frac_0``; 375 FRAC_CALC_CONV ``frac_sub (rep_rat r1) frac_0``; 376 FRAC_CALC_CONV ``frac_sub (frac_add (rep_rat r1) (rep_rat r2)) frac_0``; 377 * ---------- test cases ---------- *) 378 379 380(*-------------------------------------------------------------------------- 381 * FRAC_STRICT_CALC_TAC : tactic 382 *--------------------------------------------------------------------------*) 383 384fun FRAC_STRICT_CALC_TAC (asm_list,goal) = 385 let 386 val frac_terms = extract_frac goal; 387 val calc_thms = map FRAC_CALC_CONV frac_terms; 388 in 389 ( 390 SUBST_TAC calc_thms 391 ) (asm_list,goal) 392 end 393handle HOL_ERR _ => raise ERR "FRAC_STRICT_CALCULATE_TAC" ""; 394 395 396 397(*-------------------------------------------------------------------------- 398 * frac_calc_tac : term list -> tactic 399 *--------------------------------------------------------------------------*) 400 401fun frac_calc_tac (frac_terms:term list) (asm_list:term list,goal:term) = 402 let 403 (* generate calculation theorems for these terms *) 404 val calc_thms = map FRAC_CALC_CONV frac_terms 405 (* extract hypotheses and conclusions *) 406 val (calc_thms_hyps,calc_thms_concls) = unzip (map dest_thm calc_thms) 407 (* was calc_asms2 *) 408 (* extract left-hand sides and right-hand sides of calculation theorem 409 conclusions *) 410 val calc_thms_conls_sides = map dest_eq calc_thms_concls 411 (* merge lists of hypotheses *) 412 val calc_hyps = op_U aconv (map (fn x => fst (dest_thm x)) calc_thms); 413 (* divide lists of hypotheses into parts ``0 < x`` and ``~(x = 0)`` *) 414 val (calc_hyps_gt0, calc_hyps_not0) = partition is_less calc_hyps 415 416 (* generate theorems for gt0 and not0 hypotheses *) 417 val asm_gt0_thms = 418 map (fn x => frac_pos_conv asm_list (snd (dest_less x)) ) calc_hyps_gt0 419 val asm_not0_thms = 420 map (fn x => frac_not0_conv asm_list (fst (dest_eq (dest_neg x))) ) 421 calc_hyps_not0 422 val precond_thms = asm_gt0_thms @ asm_not0_thms; 423 424 (* partition them *) 425 fun proved (x:thm) = null (hyp x) orelse List.all (C tmem asm_list) (hyp x) 426 val (asms_proved,asms_toprove) = 427 partition proved (asm_gt0_thms @ asm_not0_thms); 428 429 (* hypothesis, TODO: eventuell gleich triviale entfernen *) 430 val asms_hyp = op_U aconv (map (fn x => fst (dest_thm x)) asms_toprove) 431 432 (* generate subgoal: prove the proposition in which the fractions are 433 subsituted by their calculated values *) 434 val subs_sg = (asm_list, subst (map (fn (lhs,rhs) => (lhs |-> rhs)) 435 calc_thms_conls_sides) goal); 436 (* generate subgoals: prove the hypothesis of the hypothesis of the 437 calculation theorems *) 438 val hyps_sgs = map (fn x => (asm_list,x)) asms_hyp; 439 440 (* TODO: statt oben hier noch ein paar Theoreme erg��nzen, die dann mit (UOK) 441 thms konkateniert werden *) 442 443 (*val thms = map mk_thm ([subs_sg] @ hyps_sgs);*) 444 445 in 446 ([subs_sg] @ hyps_sgs , 447 fn (thms:thm list) => 448 let 449 (* first theorem: the "main subgoal" *) 450 val subs_thm = hd thms 451 (* all other theorems: hyptothesis subgoals *) 452 val asm_thms = tl thms 453 454 (* erster Schritt: baue Voraussetzungen f��r die calc_thms (UOK) 455 zusammen *) 456 457 458 (* extract proof from asm_thms list (TODO: other list) *) 459 fun proof_from_asm_thms (t1:term) = 460 let 461 val corres_asm_thm = List.find (fn x => concl x ~~ t1) asm_thms 462 val corres_pro_thm = List.find (fn x => concl x ~~ t1) asms_proved 463 in 464 if isSome corres_pro_thm then valOf corres_pro_thm 465 else if isSome corres_asm_thm then valOf corres_asm_thm 466 else ASSUME ``T`` 467 end; 468 469 470 471 fun get_step1_proofs (thm1:thm) = map proof_from_asm_thms (hyp thm1) 472 fun mapped_precond_thm (thm1:thm) = 473 LIST_MP (List.rev (get_step1_proofs thm1)) (DISCH_ALL thm1) 474 475 val step1_proofs = map mapped_precond_thm precond_thms 476 477 478 fun proof_from_step1 (t1:term) = 479 let 480 val corres_asm_thm = List.find (fn x => concl x ~~ t1) step1_proofs 481 (*val corres_pro_thm = List.find (fn x => concl x = t1) asms_proved;*) 482 in 483 (*if (isSome corres_pro_thm) then 484 valOf corres_pro_thm 485 else*) 486 if isSome corres_asm_thm then valOf corres_asm_thm 487 else ASSUME ``T`` 488 end 489 490 491 fun get_step2_proofs (thm1:thm) = map proof_from_step1 (hyp thm1) 492 fun step2_thm (thm1:thm) = 493 LIST_MP (List.rev (get_step2_proofs thm1)) (DISCH_ALL thm1) 494 495 val step2_proofs = map step2_thm calc_thms; 496 in 497 (* PROBLEM: calc_thms bringen viele Hypothesen rein -> eliminieren *) 498 SUBS (map GSYM step2_proofs) subs_thm 499 end 500 ) 501 end 502handle HOL_ERR _ => raise ERR "FRAC_CALC_TAC" ""; 503 504 505(*-------------------------------------------------------------------------- 506 * FRAC_CALCTERM_TAC : term -> tactic 507 *--------------------------------------------------------------------------*) 508 509fun FRAC_CALCTERM_TAC (t1:term) (asm_list:term list,goal:term) = 510 (frac_calc_tac [t1]) (asm_list:term list,goal:term); 511 512(*-------------------------------------------------------------------------- 513 * FRAC_CALC_TAC : tactic 514 *--------------------------------------------------------------------------*) 515 516fun FRAC_CALC_TAC (asm_list, goal) = 517 (frac_calc_tac (extract_frac goal)) (asm_list, goal); 518 519(*-------------------------------------------------------------------------- 520 * FRAC_STRICT_CALCEQ_TAC : tactic 521 *--------------------------------------------------------------------------*) 522 523val FRAC_STRICT_CALCEQ_TAC = 524 FRAC_STRICT_CALC_TAC THEN 525 REWRITE_TAC[FRAC_EQ_ALT] THEN 526 FRAC_NMRDNM_TAC THEN 527 INT_CALCEQ_TAC; 528 529(*-------------------------------------------------------------------------- 530 * FRAC_CALCEQ_TAC : tactic 531 *--------------------------------------------------------------------------*) 532 533val FRAC_CALCEQ_TAC = 534 FRAC_CALC_TAC THEN 535 REWRITE_TAC[FRAC_EQ_ALT] THEN 536 FRAC_NMRDNM_TAC THEN 537 INT_CALCEQ_TAC; 538 539(*========================================================================== 540 * transformation of fractions into "valid fractions" 541 *==========================================================================*) 542 543(*-------------------------------------------------------------------------- 544 * frac_saveterm_conv : conv 545 *--------------------------------------------------------------------------*) 546 547fun frac_saveterm_conv t1 = 548 let 549 val (comb, args) = dest_comb t1; 550 val (a1,b1) = dest_pair args; 551 val a2 = a1; 552 val b2x = ``Num (^b1 - 1i)``; 553 val b2 = ``& ^b2x + 1i``; 554 val to_show = ``abs_frac (^a1, ^b1) = frac_save ^a1 (Num (^b1 - 1i))``; 555 val dnm_thm1 = ARITH_PROVE ``0i < ^b1``; 556 val dnm_thm2 = ARITH_PROVE ``0i < ^b2``; 557 val frac_thm = SPECL[a1,b1,a1,b2] FRAC_EQ 558 in 559 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)) 560 end; 561 562(*-------------------------------------------------------------------------- 563 * FRAC_SAVE_CONV : conv 564 *--------------------------------------------------------------------------*) 565 566fun FRAC_SAVE_CONV t1 = 567 REWRITE_CONV (map (TRY_CONV frac_saveterm_conv) (extract_abs_frac t1)) t1; 568 569(*-------------------------------------------------------------------------- 570 * FRAC_SAVE_TAC : tactic 571 *--------------------------------------------------------------------------*) 572 573val FRAC_SAVE_TAC = CONV_TAC FRAC_SAVE_CONV; 574 575(*========================================================================== 576 * end of structure 577 *==========================================================================*) 578end; 579