1structure ratLib :> ratLib = 2struct 3 4open HolKernel boolLib Parse bossLib; 5 6(* interactive mode 7app load ["simpLib", "pairLib", "intExtensionTheory", 8 "jbUtils", "schneiderUtils", "intLib", 9 "fracTheory", "fracLib", "fracUtils", 10 "ratTheory", "ratUtils", "integerRingLib"]; 11*) 12 13open 14 simpLib pairLib integerTheory intLib intExtensionTheory 15 jbUtils schneiderUtils 16 fracTheory fracLib fracUtils 17 ratTheory ratUtils integerRingLib ratSyntax; 18 19val ERR = mk_HOL_ERR "ratLib" 20 21(*-------------------------------------------------------------------------- 22 * imported from fracLib 23 *--------------------------------------------------------------------------*) 24 25val FRAC_EQ_TAC = fracLib.FRAC_EQ_TAC; 26val FRAC_POS_TAC = fracLib.FRAC_POS_TAC; 27 28(*========================================================================== 29 * equivalence of rational numbers 30 *==========================================================================*) 31 32(*-------------------------------------------------------------------------- 33 * RAT_EQ_CONV : conv 34 * 35 * abs_rat f1 = abs_rat f2 36 * ---------------------------------------------------- 37 * |- (abs_rat f1 = abs_rat f2) 38 * = (nmr f1 * dnm f2 = nmr f2 * dnm f1) : thm 39 *--------------------------------------------------------------------------*) 40 41val RAT_EQ_CONV:conv = fn term1 => 42let 43 val eqn = dest_neg term1; 44 val (lhs,rhs) = dest_eq eqn; 45 val (lhc, f1) = dest_comb lhs; 46 val (rhc, f2) = dest_comb rhs; 47in 48 UNDISCH_ALL (SPECL[f1,f2] RAT_EQ) 49end 50handle HOL_ERR _ => raise ERR "RAT_EQ_CONV" ""; 51 52 53(*-------------------------------------------------------------------------- 54 * RAT_EQ_TAC : tactic 55 * 56 * A ?- abs_rat f1 = abs_rat f2 57 * ========================================= RAT_EQ_TAC 58 * A ?- nmr f1 * dnm f2 = nmr f2 * dnm f1 59 *--------------------------------------------------------------------------*) 60 61fun RAT_EQ_TAC (asm_list,goal) = 62 (SUBST_TAC[RAT_EQ_CONV goal]) (asm_list,goal) 63handle HOL_ERR _ => raise ERR "RAT_EQ_TAC" ""; 64 65 66(*========================================================================== 67 * associativity, commutativity 68 *==========================================================================*) 69 70(*-------------------------------------------------------------------------- 71 * RAT_ADDAC_TAC : tactic 72 * RAT_MULAC_TAC : tactic 73 *--------------------------------------------------------------------------*) 74 75val RAT_ADDAC_CONV = AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM); 76val RAT_MULAC_CONV = AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM); 77 78fun RAT_ADDAC_TAC t1 = SUBST1_TAC (EQT_ELIM (AC_CONV (RAT_ADD_ASSOC, RAT_ADD_COMM) t1)); 79fun RAT_MULAC_TAC t1 = SUBST1_TAC (EQT_ELIM (AC_CONV (RAT_MUL_ASSOC, RAT_MUL_COMM) t1)); 80 81(*========================================================================== 82 manipulation of terms/equations 83 *==========================================================================*) 84 85(*-------------------------------------------------------------------------- 86 * RAT_ADDSUB_TAC : tactic 87 *--------------------------------------------------------------------------*) 88 89fun RAT_ADDSUB_TAC t1 t2 = SUBST1_TAC (SUBS [SPEC t2 (GSYM RAT_ADD_RINV)] (SPEC t1 (GSYM RAT_ADD_RID))); 90 91(*-------------------------------------------------------------------------- 92 * RAT_EQ_LMUL_TAC : tactic 93 *--------------------------------------------------------------------------*) 94 95fun RAT_EQ_LMUL_TAC term1 (asm_list,goal) = 96let 97 val (eq_lhs,eq_rhs) = dest_eq goal; 98in 99 SUBST_TAC[GSYM (UNDISCH_ALL (SPECL [eq_lhs,eq_rhs,term1] RAT_EQ_LMUL))] 100end 101 (asm_list,goal) 102handle HOL_ERR _ => raise ERR "RAT_EQ_RMUL_TAC" ""; 103 104(*-------------------------------------------------------------------------- 105 * RAT_EQ_RMUL_TAC : tactic 106 *--------------------------------------------------------------------------*) 107 108fun RAT_EQ_RMUL_TAC term1 (asm_list,goal) = 109let 110 val (eq_lhs,eq_rhs) = dest_eq goal; 111in 112 SUBST_TAC[GSYM (UNDISCH_ALL (SPECL [eq_lhs,eq_rhs,term1] RAT_EQ_RMUL))] 113end 114 (asm_list,goal) 115handle HOL_ERR _ => raise ERR "RAT_EQ_RMUL_TAC" ""; 116 117(*========================================================================== 118 calculation 119 *==========================================================================*) 120 121(*-------------------------------------------------------------------------- 122 * RAT_CALCULATE_rewrites : thm list 123 *--------------------------------------------------------------------------*) 124 125val RAT_CALCULATE_rewrites = 126 [RAT_ADD_CALCULATE, RAT_SUB_CALCULATE, RAT_MUL_CALCULATE, RAT_DIV_CALCULATE, RAT_AINV_CALCULATE, RAT_MINV_CALCULATE, rat_0_def, rat_1_def]; 127 128(*-------------------------------------------------------------------------- 129 * rat_calculate_table : (term * thm) list 130 *--------------------------------------------------------------------------*) 131 132val rat_calculate_table = [ 133 ( ``rat_0``, rat_0_def ), 134 ( ``rat_1``, rat_1_def ), 135 ( ``rat_ainv``, RAT_AINV_CALCULATE ), 136 ( ``rat_minv``, RAT_MINV_CALCULATE ), 137 ( ``rat_add``, RAT_ADD_CALCULATE ), 138 ( ``rat_sub``, RAT_SUB_CALCULATE ), 139 ( ``rat_mul``, RAT_MUL_CALCULATE ), 140 ( ``rat_div``, RAT_DIV_CALCULATE ) 141]; 142 143(*-------------------------------------------------------------------------- 144 * RAT_CALC_CONV : conv 145 * 146 * r1 147 * --------------------- 148 * |- r1 = abs_rat(f1) 149 *--------------------------------------------------------------------------*) 150 151 152fun RAT_CALC_CONV (t1:term) = 153let 154 val thm = REFL t1 155 val (top_rator, top_rands) = strip_comb t1 156 val calc_table_entry = 157 List.find (fn x => fst(x) ~~ top_rator) rat_calculate_table 158in 159 (* do nothing if term is already in the form abs_rat(...) *) 160 if top_rator ~~ ``abs_rat`` then thm 161 (* if it is a numeral, simply rewrite it *) 162 else if (top_rator ~~ ``rat_of_num``) then 163 SUBST [���x:rat��� |-> SPEC (rand t1) (RAT_OF_NUM_CALCULATE)] ���^t1 = x:rat��� thm 164 (* if there is an entry in the calculation table, calculate it *) 165 else if (isSome calc_table_entry) then 166 let 167 val arg_thms = map RAT_CALC_CONV top_rands; 168 val arg_fracs = map (fn x => rand(rhs(concl x))) arg_thms; 169 val arg_vars = map (fn x => genvar ``:rat``) arg_thms; 170 171 val subst_list = 172 map (fn x => fst(x) |-> snd(x)) (ListPair.zip (arg_vars,arg_thms)); 173 (* subst_term: t1 = top_rator arg_vars[1] ... arg_vars[n] *) 174 val subst_term = mk_eq (t1 , list_mk_comb (top_rator,arg_vars)) 175 176 val thm1 = SUBST subst_list subst_term thm; 177 val (thm1_lhs, thm1_rhs) = dest_eq(concl thm1); 178 val thm1_lhs_var = genvar ``:rat``; 179 180 val calc_thm = snd (valOf( calc_table_entry )); 181 in 182 SUBST [thm1_lhs_var |-> UNDISCH_ALL (SPECL arg_fracs calc_thm)] 183 ���^thm1_lhs = ^thm1_lhs_var��� thm1 184 end 185 (* otherwise: applying r = abs_rat(rep_rat r)) always works *) 186 else 187 SUBST [``x:rat`` |-> SPEC t1 (GSYM RAT)] ``^t1 = x:rat`` thm 188end; 189 190(* ---------- test cases ---------- * 191 RAT_CALC_CONV ``abs_rat(f1)``; 192 RAT_CALC_CONV ``r1:rat``; 193 RAT_CALC_CONV ``rat_ainv ( abs_rat(f1) )`` 194 RAT_CALC_CONV ``rat_add (abs_rat(f1)) (abs_rat(f2))``; 195 RAT_CALC_CONV ``rat_add r1 ( rat_sub (abs_rat(abs_frac(4i,5i))) r2)``; 196 RAT_CALC_CONV ``rat_mul r1 ( rat_div (abs_rat(abs_frac(4i,5i))) r2)``; 197 RAT_CALC_CONV ``rat_add rat_0 rat_1``; 198 * ---------- test cases ---------- *) 199 200 201(*-------------------------------------------------------------------------- 202 * RAT_CALCTERM_TAC : term -> tactic 203 * 204 * calculates the value of t1:rat 205 *--------------------------------------------------------------------------*) 206 207fun RAT_CALCTERM_TAC (t1:term) (asm_list,goal) = 208 let 209 val calc_thm = RAT_CALC_CONV t1; 210 val (calc_asms, calc_concl) = dest_thm calc_thm; 211 in 212 ( 213 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 214 SUBST_TAC[calc_thm] 215 ) (asm_list,goal) 216 end 217handle HOL_ERR _ => raise ERR "RAT_CALCTERM_TAC" ""; 218 219 220(*-------------------------------------------------------------------------- 221 * RAT_STRICT_CALC_TAC : tactic 222 * 223 * calculates the value of all subterms (of type ``:rat``) 224 *--------------------------------------------------------------------------*) 225 226fun RAT_STRICT_CALC_TAC (asm_list,goal) = 227 let 228 val rat_terms = extract_rat goal; 229 val calc_thms = map RAT_CALC_CONV rat_terms; 230 val calc_asms = op_U aconv (map (fn x => fst (dest_thm x)) calc_thms); 231 in 232 ( 233 MAP_EVERY 234 ASSUME_TAC 235 (map (fn x => TAC_PROOF 236 ((asm_list,x), 237 RW_TAC intLib.int_ss [FRAC_DNMPOS,INT_MUL_POS_SIGN, 238 INT_NOTPOS0_NEG,INT_NOT0_MUL, 239 INT_GT0_IMP_NOT0, 240 INT_ABS_NOT0POS])) 241 calc_asms) THEN 242 SUBST_TAC calc_thms) (asm_list,goal) 243 end handle HOL_ERR _ => raise ERR "RAT_STRICT_CALC_TAC" ""; 244 245(*-------------------------------------------------------------------------- 246 * RAT_CALC_TAC : tactic 247 * 248 * calculates the value of all subterms (of type ``:rat``) 249 * assumptions that were needed for the simplification are added to the goal 250 *--------------------------------------------------------------------------*) 251 252fun RAT_CALC_TAC (asm_list,goal) = 253 let 254 (* extract terms of type ``:rat`` *) 255 val rat_terms = extract_rat goal; 256 (* build conversions *) 257 val calc_thms = map RAT_CALC_CONV rat_terms; 258 (* split list into assumptions and conclusions *) 259 val (calc_asmlists, calc_concl) = ListPair.unzip (map (fn x => dest_thm x) calc_thms); 260 (* merge assumptions lists *) 261 val calc_asms = op_U aconv calc_asmlists; 262 (* function to prove an assumption, TODO: fracLib benutzen *) 263 val gen_thm = (fn x => TAC_PROOF ((asm_list,x), RW_TAC intLib.int_ss [] )); 264 (* try to prove assumptions *) 265 val prove_list = List.map (total gen_thm) calc_asms; 266 (* combine assumptions and their proofs *) 267 val list1 = ListPair.zip (calc_asms,prove_list); 268 (* partition assumptions into proved assumptions and assumptions to be proved *) 269 val list2 = partition (fn x => isSome (snd x)) list1; 270 val asms_toprove = map fst (snd list2); 271 val asms_proved = map (fn x => valOf (snd x)) (fst list2); 272 (* generate new subgoal goal *) 273 val subst_goal = snd (dest_eq (snd (dest_thm (ONCE_REWRITE_CONV calc_thms goal)))); 274 val subgoal = (list_mk_conj (asms_toprove @ [subst_goal]) ); 275 val mp_thm = TAC_PROOF 276 ( 277 (asm_list, mk_imp (subgoal,goal)) 278 , 279 STRIP_TAC THEN 280 MAP_EVERY ASSUME_TAC asms_proved THEN 281 ONCE_REWRITE_TAC calc_thms THEN 282 PROVE_TAC [] 283 ); 284 in 285 ( [(asm_list,subgoal)], fn (thms:thm list) => MP mp_thm (hd thms) ) 286 end 287handle HOL_ERR _ => raise ERR "RAT_CALC_TAC" ""; 288 289(*-------------------------------------------------------------------------- 290 * RAT_CALCEQ_TAC : tactic 291 *--------------------------------------------------------------------------*) 292 293val RAT_CALCEQ_TAC = 294 RAT_CALC_TAC THEN 295 FRAC_CALC_TAC THEN 296 REWRITE_TAC[RAT_EQ] THEN 297 FRAC_NMRDNM_TAC THEN 298 INT_RING_TAC; 299 300 301(*========================================================================== 302 * transformation of rational numbers into "defined rational numbers" 303 *==========================================================================*) 304 305(*-------------------------------------------------------------------------- 306 * RAT_SAVE_TAC : term -> tactic 307 *--------------------------------------------------------------------------*) 308 309fun RAT_SAVE_TAC t1 (asm_list, goal) = 310 let val subst_thm = SPEC t1 RAT_SAVE 311 in 312 (ASSUME_TAC subst_thm THEN LEFT_EXISTS_TAC THEN LEFT_EXISTS_TAC THEN 313 FILTER_ASM_REWRITE_TAC (fn t => not (tmem t asm_list)) [] THEN 314 POP_NO_TAC 0) 315 (asm_list, goal) 316 end 317 318(*-------------------------------------------------------------------------- 319 * RAT_SAVE_ALLVARS_TAC : tactic 320 *--------------------------------------------------------------------------*) 321 322fun RAT_SAVE_ALLVARS_TAC (asm_list, goal) = 323 MAP_EVERY RAT_SAVE_TAC (extract_rat_vars goal) (asm_list, goal); 324 325 326(*========================================================================== 327 * elimination of rat_minv_terms 328 *==========================================================================*) 329 330(*-------------------------------------------------------------------------- 331 * rat_eq_rmul_list_conv: term list -> term -> thm 332 *--------------------------------------------------------------------------*) 333 334fun rat_eq_rmul_list_conv (factor_list:term list) (equation:term) = 335let 336 val (lhs,rhs) = dest_eq equation; 337 val product = list_rat_mul factor_list; 338in 339 REWRITE_RULE[RAT_MUL_ASSOC, RAT_RDISTRIB] (GSYM (UNDISCH( SPECL[lhs,rhs,product] RAT_EQ_RMUL) )) 340end; 341 342(*-------------------------------------------------------------------------- 343 * rat_eliminate_minv_conv: term -> thm 344 *--------------------------------------------------------------------------*) 345 346fun rat_eliminate_minv_conv (t1:term) = 347let 348 (* update the appropiate counter : each element of the list counts the number of occurences of a given term and its multiplicative inverse *) 349 fun insert_into_factor_list (term1:term) (i1:int,i2:int) (h::t) = 350 if( fst h ~~ term1 ) then (fst h, (fst (snd h)+i1, snd (snd h)+i2) )::t 351 else h::(insert_into_factor_list term1 (i1,i2) t) 352 | insert_into_factor_list term1 (i1:int,i2:int) [] = [(term1,(i1,i2))] 353 (* count all factors *) 354 fun count_factors l0 (h::t) = 355 if (is_rat_minv h) then 356 count_factors (insert_into_factor_list (dest_rat_minv h) (0,1) l0) t 357 else 358 count_factors (insert_into_factor_list h (1,0) l0) t 359 | count_factors l0 [] = l0; 360 (* generate the part of a product (product of the same terms and multiplicative inverses resp.) *) 361 fun gen_product_part (term1, (i1,i2)) = 362 if (i1>0) andalso (i2>0) then 363 ���rat_minv ^term1 * ^term1���::gen_product_part(term1,(i1-1,i2-1)) 364 else if (i1=0) andalso (i2>0) then 365 ���rat_minv ^term1���::gen_product_part (term1,(i1,i2-1)) 366 else if (i1>0) andalso (i2=0) then 367 ���^term1���::gen_product_part (term1,(i1-1,i2)) 368 else 369 []; 370 (* generate the whole product *) 371 fun reorder_product (h::t) = gen_product_part h::reorder_product t 372 | reorder_product [] = [] 373 374 (* extract all fractors of the product given by term t1 *) 375 val factors = strip_rat_mul t1; 376 (* filter out all multiplicative inverses *) 377 val minv_factors = filter is_rat_minv factors; 378 (* generate the new product in which factors and their corresponding multiplicative inverses have been cancelled *) 379 val desired_product = 380 list_rat_mul 381 (map list_rat_mul (reorder_product (count_factors [] factors))) 382in 383 (* this is basically proven by the specialised versions of RAT_MUL_LINV *) 384 ((fn tx => EQT_ELIM (RAT_MULAC_CONV ���^tx = ^desired_product���)) THENC 385 (REWRITE_CONV (RAT_MUL_LID::RAT_MUL_RID:: 386 (map (fn fx=> UNDISCH (SPEC fx RAT_MUL_LINV)) 387 (map dest_rat_minv minv_factors))))) t1 388end; 389 390 391(*-------------------------------------------------------------------------- 392 * rat_eliminate_minv_eq_conv: term -> thm 393 *--------------------------------------------------------------------------*) 394 395fun rat_eliminate_minv_eq_conv (t1:term) = 396let 397 val (lhs,rhs) = dest_eq t1; 398 (* extract all summands *) 399 val summands = (strip_rat_add lhs) @ (strip_rat_add rhs); 400 (* generate elimination theorems for all of them *) 401 val reorder_thms = map rat_eliminate_minv_conv summands; 402in 403 (* apply all theorems - TODO: only rewrite on the right side! *) 404 ONCE_REWRITE_CONV reorder_thms (t1:term) 405end; 406 407 408(*-------------------------------------------------------------------------- 409 * RAT_ELIMINATE_MINV_EQ_CONV: term -> thm 410 *--------------------------------------------------------------------------*) 411 412fun RAT_ELIMINATE_MINV_EQ_CONV (t1:term) = 413let 414 (* generate elimination theorem *) 415 val thm1 = (rat_eq_rmul_list_conv (map dest_rat_minv (extract_rat_minv t1)) THENC rat_eliminate_minv_eq_conv) t1; 416in 417 (* simplify assumption list *) 418 UNDISCH_ALL (IMP_AND_RULE (REWRITE_RULE[RAT_NO_ZERODIV_NEG] (DISCH_ALL thm1 ))) 419end; 420 421(*-------------------------------------------------------------------------- 422 * RAT_ELIMINATE_MINV_CONV: term -> thm 423 *--------------------------------------------------------------------------*) 424 425fun RAT_ELIMINATE_MINV_CONV (t1:term) = 426 ONCE_REWRITE_CONV (map RAT_ELIMINATE_MINV_EQ_CONV (extract_rat_equations t1)) t1; 427 428(*-------------------------------------------------------------------------- 429 * RAT_ELIMINATE_MINV_TAC: tactic -> thm 430 *--------------------------------------------------------------------------*) 431 432val RAT_ELIMINATE_MINV_TAC = CONV_TAC RAT_ELIMINATE_MINV_CONV; 433 434 435 436(*========================================================================== 437 * calculation of rational expressions 438 *==========================================================================*) 439 440(*-------------------------------------------------------------------------- 441 * rewrite rules to calculate rational expressions 442 *--------------------------------------------------------------------------*) 443 444(* rewrites to calculate operations on integers - (TODO) remove dependencies: numRingTheory and integerRingTheory *) 445local open numeralTheory numRingTheory integerRingTheory in 446 val num_rewrites = [numeral_distrib, numeral_eq, numeral_suc, numeral_iisuc, numeral_add, numeral_mult, iDUB_removal, ISPEC(``arithmetic$ZERO``) REFL_CLAUSE, ISPEC(``0:num``) REFL_CLAUSE ]; 447 val int_rewrites = [int_calculate, INT_0, INT_1, numeral_lt, numeral_lte, numeral_sub, iSUB_THM, AND_CLAUSES, SGN_def] @ num_rewrites 448end; 449(* rewrites to calculate operations on fractions *) 450val frac_rewrites = [FRAC_0_SAVE, FRAC_1_SAVE, FRAC_AINV_SAVE, FRAC_ADD_SAVE, FRAC_MUL_SAVE]; 451(* rewrites to calculate operations on rational numbers *) 452val rat_basic_rewrites = [rat_0, rat_1, rat_0_def, rat_1_def, RAT_AINV_CALCULATE, RAT_ADD_CALCULATE, RAT_MUL_CALCULATE] @ frac_rewrites; 453(* rewrites to additionally decide equalities and inequalities on rational numbers *) 454val rat_rewrites = [RAT_EQ_CALCULATE, RAT_LES_CALCULATE, rat_gre_def, rat_leq_def, rat_geq_def, FRAC_NMR_SAVE, FRAC_DNM_SAVE] @ rat_basic_rewrites; 455(* rewrites to decide equalities on rationals in numeral form *) 456val rat_num_rewrites = [RAT_ADD_NUM_CALCULATE, RAT_MUL_NUM_CALCULATE, RAT_EQ_NUM_CALCULATE, RAT_AINV_AINV, RAT_AINV_0] @ num_rewrites; 457 458(*-------------------------------------------------------------------------- 459 * RAT_PRECALC_CONV 460 * RAT_POSTCALC_CONV 461 *--------------------------------------------------------------------------*) 462 463val RAT_PRECALC_CONV = 464 SIMP_CONV int_ss [rat_cons_def, RAT_SAVE_NUM, SGN_def] THENC REWRITE_CONV[RAT_SUB_ADDAINV, RAT_DIV_MULMINV] THENC FRAC_SAVE_CONV; 465 466val RAT_POSTCALC_CONV = 467 REWRITE_CONV[GSYM RAT_SUB_ADDAINV, GSYM RAT_DIV_MULMINV] THENC SIMP_CONV int_ss [RAT_SAVE_TO_CONS, RAT_CONS_TO_NUM]; 468 469(*-------------------------------------------------------------------------- 470 * RAT_BASIC_ARITH_CONV 471 *--------------------------------------------------------------------------*) 472 473val RAT_BASIC_ARITH_CONV = 474 RAT_PRECALC_CONV THENC REWRITE_CONV ([GSYM INT_ADD, GSYM INT_MUL] @ rat_rewrites) THENC ARITH_CONV; 475 476(*-------------------------------------------------------------------------- 477 * RAT_BASIC_ARITH_TAC 478 *--------------------------------------------------------------------------*) 479 480val RAT_BASIC_ARITH_TAC = 481 CONV_TAC RAT_BASIC_ARITH_CONV; 482 483(* generic normalisation *) 484open ratSyntax 485fun mk_rvar s = mk_var(s, rat) 486val x = mk_rvar "x" 487val y = mk_rvar "y" 488val z = mk_rvar "z" 489val l_asscomm = prove( 490 mk_eq(mk_rat_add(mk_rat_add(x,y), z), 491 mk_rat_add(mk_rat_add(x,z), y)), 492 CONV_TAC (BINOP_CONV (REWR_CONV (GSYM ratTheory.RAT_ADD_ASSOC))) >> 493 CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV ratTheory.RAT_ADD_COMM))) >> 494 REFL_TAC); 495val r_asscomm = prove( 496 mk_eq(mk_rat_add(x, mk_rat_add(y, z)), 497 mk_rat_add(y, mk_rat_add(x,z))), 498 CONV_TAC (BINOP_CONV (REWR_CONV ratTheory.RAT_ADD_ASSOC)) >> 499 CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV ratTheory.RAT_ADD_COMM))) >> 500 REFL_TAC); 501 502val one_r = ratSyntax.mk_rat_of_num (numSyntax.mk_numeral Arbnum.one) 503 504fun non_coeff t = 505 let 506 open ratSyntax 507 in 508 case Lib.total dest_rat_mul t of 509 SOME (c,x) => if is_literal c then x 510 else if is_literal x then c 511 else t 512 | NONE => if is_literal t then one_r else t 513 end 514 515(* 516val merge = REWR_CONV (GSYM ratTheory.RAT_RDISTRIB) THENC 517 LAND_CONV RAT_ADD_CONV 518 let 519 open ratSyntax 520 val (t1,t2) = dest_rat_add t 521 522val RAT_SUM_CANON = GenPolyCanon.gencanon { 523 dest = ratSyntax.dest_rat_add, 524 is_literal = ratSyntax.is_literal, 525 assoc_mode = GenPolyCanon.L, 526 assoc = SPEC_ALL ratTheory.RAT_ADD_ASSOC, 527 symassoc = SYM (SPEC_ALL ratTheory.RAT_ADD_ASSOC), 528 comm = SPEC_ALL ratTheory.RAT_ADD_COMM, 529 l_asscom = l_asscomm, 530 r_asscomm = r_asscomm, 531 non_coeff = non_coeff, 532 merge = merge, 533*) 534 535(*========================================================================== 536 * end of structure 537 *==========================================================================*) 538end; 539