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 = List.find (fn x => fst(x)= top_rator) rat_calculate_table; 157in 158 (* do nothing if term is already in the form abs_rat(...) *) 159 if top_rator=``abs_rat`` then 160 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 = map (fn x => fst(x) |-> snd(x)) (ListPair.zip (arg_vars,arg_thms)); 172 (* subst_term: t1 = top_rator arg_vars[1] ... arg_vars[n] *) 173 val subst_term = mk_eq (t1 , list_mk_comb (top_rator,arg_vars)) 174 175 val thm1 = SUBST subst_list subst_term thm; 176 val (thm1_lhs, thm1_rhs) = dest_eq(concl thm1); 177 val thm1_lhs_var = genvar ``:rat``; 178 179 val calc_thm = snd (valOf( calc_table_entry )); 180 in 181 SUBST [thm1_lhs_var |-> UNDISCH_ALL (SPECL arg_fracs calc_thm)] ``^thm1_lhs = ^thm1_lhs_var`` thm1 182 end 183 (* otherwise: applying r = abs_rat(rep_rat r)) always works *) 184 else 185 SUBST [``x:rat`` |-> SPEC t1 (GSYM RAT)] ``^t1 = x:rat`` thm 186end; 187 188(* ---------- test cases ---------- * 189 RAT_CALC_CONV ``abs_rat(f1)``; 190 RAT_CALC_CONV ``r1:rat``; 191 RAT_CALC_CONV ``rat_ainv ( abs_rat(f1) )`` 192 RAT_CALC_CONV ``rat_add (abs_rat(f1)) (abs_rat(f2))``; 193 RAT_CALC_CONV ``rat_add r1 ( rat_sub (abs_rat(abs_frac(4i,5i))) r2)``; 194 RAT_CALC_CONV ``rat_mul r1 ( rat_div (abs_rat(abs_frac(4i,5i))) r2)``; 195 RAT_CALC_CONV ``rat_add rat_0 rat_1``; 196 * ---------- test cases ---------- *) 197 198 199(*-------------------------------------------------------------------------- 200 * RAT_CALCTERM_TAC : term -> tactic 201 * 202 * calculates the value of t1:rat 203 *--------------------------------------------------------------------------*) 204 205fun RAT_CALCTERM_TAC (t1:term) (asm_list,goal) = 206 let 207 val calc_thm = RAT_CALC_CONV t1; 208 val (calc_asms, calc_concl) = dest_thm calc_thm; 209 in 210 ( 211 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 212 SUBST_TAC[calc_thm] 213 ) (asm_list,goal) 214 end 215handle HOL_ERR _ => raise ERR "RAT_CALCTERM_TAC" ""; 216 217 218(*-------------------------------------------------------------------------- 219 * RAT_STRICT_CALC_TAC : tactic 220 * 221 * calculates the value of all subterms (of type ``:rat``) 222 *--------------------------------------------------------------------------*) 223 224fun RAT_STRICT_CALC_TAC (asm_list,goal) = 225 let 226 val rat_terms = extract_rat goal; 227 val calc_thms = map RAT_CALC_CONV rat_terms; 228 val calc_asms = list_xmerge (map (fn x => fst (dest_thm x)) calc_thms); 229 in 230 ( 231 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 232 SUBST_TAC calc_thms 233 ) (asm_list,goal) 234 end 235handle HOL_ERR _ => raise ERR "RAT_STRICT_CALC_TAC" ""; 236 237(*-------------------------------------------------------------------------- 238 * RAT_CALC_TAC : tactic 239 * 240 * calculates the value of all subterms (of type ``:rat``) 241 * assumptions that were needed for the simplification are added to the goal 242 *--------------------------------------------------------------------------*) 243 244fun RAT_CALC_TAC (asm_list,goal) = 245 let 246 (* extract terms of type ``:rat`` *) 247 val rat_terms = extract_rat goal; 248 (* build conversions *) 249 val calc_thms = map RAT_CALC_CONV rat_terms; 250 (* split list into assumptions and conclusions *) 251 val (calc_asmlists, calc_concl) = ListPair.unzip (map (fn x => dest_thm x) calc_thms); 252 (* merge assumptions lists *) 253 val calc_asms = list_xmerge calc_asmlists; 254 (* function to prove an assumption, TODO: fracLib benutzen *) 255 val gen_thm = (fn x => TAC_PROOF ((asm_list,x), RW_TAC intLib.int_ss [] )); 256 (* try to prove assumptions *) 257 val prove_list = List.map (total gen_thm) calc_asms; 258 (* combine assumptions and their proofs *) 259 val list1 = ListPair.zip (calc_asms,prove_list); 260 (* partition assumptions into proved assumptions and assumptions to be proved *) 261 val list2 = partition (fn x => isSome (snd x)) list1; 262 val asms_toprove = map fst (snd list2); 263 val asms_proved = map (fn x => valOf (snd x)) (fst list2); 264 (* generate new subgoal goal *) 265 val subst_goal = snd (dest_eq (snd (dest_thm (ONCE_REWRITE_CONV calc_thms goal)))); 266 val subgoal = (list_mk_conj (asms_toprove @ [subst_goal]) ); 267 val mp_thm = TAC_PROOF 268 ( 269 (asm_list, mk_imp (subgoal,goal)) 270 , 271 STRIP_TAC THEN 272 MAP_EVERY ASSUME_TAC asms_proved THEN 273 ONCE_REWRITE_TAC calc_thms THEN 274 PROVE_TAC [] 275 ); 276 in 277 ( [(asm_list,subgoal)], fn (thms:thm list) => MP mp_thm (hd thms) ) 278 end 279handle HOL_ERR _ => raise ERR "RAT_CALC_TAC" ""; 280 281(*-------------------------------------------------------------------------- 282 * RAT_CALCEQ_TAC : tactic 283 *--------------------------------------------------------------------------*) 284 285val RAT_CALCEQ_TAC = 286 RAT_CALC_TAC THEN 287 FRAC_CALC_TAC THEN 288 REWRITE_TAC[RAT_EQ] THEN 289 FRAC_NMRDNM_TAC THEN 290 INT_RING_TAC; 291 292 293(*========================================================================== 294 * transformation of rational numbers into "defined rational numbers" 295 *==========================================================================*) 296 297(*-------------------------------------------------------------------------- 298 * RAT_SAVE_TAC : term -> tactic 299 *--------------------------------------------------------------------------*) 300 301fun RAT_SAVE_TAC t1 (asm_list, goal) = 302 let val subst_thm = SPEC t1 RAT_SAVE in 303 (ASSUME_TAC subst_thm THEN LEFT_EXISTS_TAC THEN LEFT_EXISTS_TAC THEN FILTER_ASM_REWRITE_TAC (fn t => not (mem t asm_list)) [] THEN POP_NO_TAC 0) (asm_list, goal) 304 end; 305 306(*-------------------------------------------------------------------------- 307 * RAT_SAVE_ALLVARS_TAC : tactic 308 *--------------------------------------------------------------------------*) 309 310fun RAT_SAVE_ALLVARS_TAC (asm_list, goal) = 311 MAP_EVERY RAT_SAVE_TAC (extract_rat_vars goal) (asm_list, goal); 312 313 314(*========================================================================== 315 * elimination of rat_minv_terms 316 *==========================================================================*) 317 318(*-------------------------------------------------------------------------- 319 * rat_eq_rmul_list_conv: term list -> term -> thm 320 *--------------------------------------------------------------------------*) 321 322fun rat_eq_rmul_list_conv (factor_list:term list) (equation:term) = 323let 324 val (lhs,rhs) = dest_eq equation; 325 val product = list_rat_mul factor_list; 326in 327 REWRITE_RULE[RAT_MUL_ASSOC, RAT_RDISTRIB] (GSYM (UNDISCH( SPECL[lhs,rhs,product] RAT_EQ_RMUL) )) 328end; 329 330(*-------------------------------------------------------------------------- 331 * rat_eliminate_minv_conv: term -> thm 332 *--------------------------------------------------------------------------*) 333 334fun rat_eliminate_minv_conv (t1:term) = 335let 336 (* update the appropiate counter : each element of the list counts the number of occurences of a given term and its multiplicative inverse *) 337 fun insert_into_factor_list (term1:term) (i1:int,i2:int) (h::t) = 338 if( fst h = term1 ) then 339 (fst h, (fst (snd h)+i1, snd (snd h)+i2) )::t 340 else 341 h::(insert_into_factor_list term1 (i1,i2) t) 342 | insert_into_factor_list term1 (i1:int,i2:int) [] = [(term1,(i1,i2))] 343 (* count all factors *) 344 fun count_factors l0 (h::t) = 345 if (is_rat_minv h) then 346 count_factors (insert_into_factor_list (dest_rat_minv h) (0,1) l0) t 347 else 348 count_factors (insert_into_factor_list h (1,0) l0) t 349 | count_factors l0 [] = l0; 350 (* generate the part of a product (product of the same terms and multiplicative inverses resp.) *) 351 fun gen_product_part (term1, (i1,i2)) = 352 if (i1>0) andalso (i2>0) then 353 ``rat_minv ^term1 * ^term1``::gen_product_part(term1,(i1-1,i2-1)) 354 else if (i1=0) andalso (i2>0) then 355 ``rat_minv ^term1``::gen_product_part (term1,(i1,i2-1)) 356 else if (i1>0) andalso (i2=0) then 357 ``^term1``::gen_product_part (term1,(i1-1,i2)) 358 else 359 []; 360 (* generate the whole product *) 361 fun reorder_product (h::t) = gen_product_part h::reorder_product t 362 | reorder_product [] = []; 363 364 (* extract all fractors of the product given by term t1 *) 365 val factors = strip_rat_mul t1; 366 (* filter out all multiplicative inverses *) 367 val minv_factors = filter is_rat_minv factors; 368 (* generate the new product in which factors and their corresponding multiplicative inverses have been cancelled *) 369 val desired_product = list_rat_mul (map list_rat_mul (reorder_product (count_factors [] factors))); 370in 371 (* this is basically proven by the specialised versions of RAT_MUL_LINV *) 372 ((fn tx => EQT_ELIM (RAT_MULAC_CONV ``^tx = ^desired_product``)) THENC (REWRITE_CONV (RAT_MUL_LID::RAT_MUL_RID::(map (fn fx=> UNDISCH (SPEC fx RAT_MUL_LINV)) (map dest_rat_minv minv_factors))))) t1 373end; 374 375 376(*-------------------------------------------------------------------------- 377 * rat_eliminate_minv_eq_conv: term -> thm 378 *--------------------------------------------------------------------------*) 379 380fun rat_eliminate_minv_eq_conv (t1:term) = 381let 382 val (lhs,rhs) = dest_eq t1; 383 (* extract all summands *) 384 val summands = (strip_rat_add lhs) @ (strip_rat_add rhs); 385 (* generate elimination theorems for all of them *) 386 val reorder_thms = map rat_eliminate_minv_conv summands; 387in 388 (* apply all theorems - TODO: only rewrite on the right side! *) 389 ONCE_REWRITE_CONV reorder_thms (t1:term) 390end; 391 392 393(*-------------------------------------------------------------------------- 394 * RAT_ELIMINATE_MINV_EQ_CONV: term -> thm 395 *--------------------------------------------------------------------------*) 396 397fun RAT_ELIMINATE_MINV_EQ_CONV (t1:term) = 398let 399 (* generate elimination theorem *) 400 val thm1 = (rat_eq_rmul_list_conv (map dest_rat_minv (extract_rat_minv t1)) THENC rat_eliminate_minv_eq_conv) t1; 401in 402 (* simplify assumption list *) 403 UNDISCH_ALL (IMP_AND_RULE (REWRITE_RULE[RAT_NO_ZERODIV_NEG] (DISCH_ALL thm1 ))) 404end; 405 406(*-------------------------------------------------------------------------- 407 * RAT_ELIMINATE_MINV_CONV: term -> thm 408 *--------------------------------------------------------------------------*) 409 410fun RAT_ELIMINATE_MINV_CONV (t1:term) = 411 ONCE_REWRITE_CONV (map RAT_ELIMINATE_MINV_EQ_CONV (extract_rat_equations t1)) t1; 412 413(*-------------------------------------------------------------------------- 414 * RAT_ELIMINATE_MINV_TAC: tactic -> thm 415 *--------------------------------------------------------------------------*) 416 417val RAT_ELIMINATE_MINV_TAC = CONV_TAC RAT_ELIMINATE_MINV_CONV; 418 419 420 421(*========================================================================== 422 * calculation of rational expressions 423 *==========================================================================*) 424 425(*-------------------------------------------------------------------------- 426 * rewrite rules to calculate rational expressions 427 *--------------------------------------------------------------------------*) 428 429(* rewrites to calculate operations on integers - (TODO) remove dependencies: numRingTheory and integerRingTheory *) 430local open numeralTheory numRingTheory integerRingTheory in 431 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 ]; 432 val int_rewrites = [int_calculate, INT_0, INT_1, numeral_lt, numeral_lte, numeral_sub, iSUB_THM, AND_CLAUSES, SGN_def] @ num_rewrites 433end; 434(* rewrites to calculate operations on fractions *) 435val frac_rewrites = [FRAC_0_SAVE, FRAC_1_SAVE, FRAC_AINV_SAVE, FRAC_ADD_SAVE, FRAC_MUL_SAVE]; 436(* rewrites to calculate operations on rational numbers *) 437val rat_basic_rewrites = [rat_0, rat_1, rat_0_def, rat_1_def, RAT_AINV_CALCULATE, RAT_ADD_CALCULATE, RAT_MUL_CALCULATE] @ frac_rewrites; 438(* rewrites to additionally decide equalities and inequalities on rational numbers *) 439val 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; 440(* rewrites to decide equalities on rationals in numeral form *) 441val rat_num_rewrites = [RAT_ADD_NUM_CALCULATE, RAT_MUL_NUM_CALCULATE, RAT_EQ_NUM_CALCULATE, RAT_AINV_AINV, RAT_AINV_0] @ num_rewrites; 442 443(*-------------------------------------------------------------------------- 444 * RAT_PRECALC_CONV 445 * RAT_POSTCALC_CONV 446 *--------------------------------------------------------------------------*) 447 448val RAT_PRECALC_CONV = 449 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; 450 451val RAT_POSTCALC_CONV = 452 REWRITE_CONV[GSYM RAT_SUB_ADDAINV, GSYM RAT_DIV_MULMINV] THENC SIMP_CONV int_ss [RAT_SAVE_TO_CONS, RAT_CONS_TO_NUM]; 453 454(*-------------------------------------------------------------------------- 455 * RAT_BASIC_ARITH_CONV 456 *--------------------------------------------------------------------------*) 457 458val RAT_BASIC_ARITH_CONV = 459 RAT_PRECALC_CONV THENC REWRITE_CONV ([GSYM INT_ADD, GSYM INT_MUL] @ rat_rewrites) THENC ARITH_CONV; 460 461(*-------------------------------------------------------------------------- 462 * RAT_BASIC_ARITH_TAC 463 *--------------------------------------------------------------------------*) 464 465val RAT_BASIC_ARITH_TAC = 466 CONV_TAC RAT_BASIC_ARITH_CONV; 467 468(* generic normalisation *) 469open ratSyntax 470fun mk_rvar s = mk_var(s, rat) 471val x = mk_rvar "x" 472val y = mk_rvar "y" 473val z = mk_rvar "z" 474val l_asscomm = prove( 475 mk_eq(mk_rat_add(mk_rat_add(x,y), z), 476 mk_rat_add(mk_rat_add(x,z), y)), 477 CONV_TAC (BINOP_CONV (REWR_CONV (GSYM ratTheory.RAT_ADD_ASSOC))) >> 478 CONV_TAC (LAND_CONV (RAND_CONV (REWR_CONV ratTheory.RAT_ADD_COMM))) >> 479 REFL_TAC); 480val r_asscomm = prove( 481 mk_eq(mk_rat_add(x, mk_rat_add(y, z)), 482 mk_rat_add(y, mk_rat_add(x,z))), 483 CONV_TAC (BINOP_CONV (REWR_CONV ratTheory.RAT_ADD_ASSOC)) >> 484 CONV_TAC (LAND_CONV (LAND_CONV (REWR_CONV ratTheory.RAT_ADD_COMM))) >> 485 REFL_TAC); 486 487val one_r = ratSyntax.mk_rat_of_num (numSyntax.mk_numeral Arbnum.one) 488 489fun non_coeff t = 490 let 491 open ratSyntax 492 in 493 case Lib.total dest_rat_mul t of 494 SOME (c,x) => if is_literal c then x 495 else if is_literal x then c 496 else t 497 | NONE => if is_literal t then one_r else t 498 end 499 500(* 501val merge = REWR_CONV (GSYM ratTheory.RAT_RDISTRIB) THENC 502 LAND_CONV RAT_ADD_CONV 503 let 504 open ratSyntax 505 val (t1,t2) = dest_rat_add t 506 507val RAT_SUM_CANON = GenPolyCanon.gencanon { 508 dest = ratSyntax.dest_rat_add, 509 is_literal = ratSyntax.is_literal, 510 assoc_mode = GenPolyCanon.L, 511 assoc = SPEC_ALL ratTheory.RAT_ADD_ASSOC, 512 symassoc = SYM (SPEC_ALL ratTheory.RAT_ADD_ASSOC), 513 comm = SPEC_ALL ratTheory.RAT_ADD_COMM, 514 l_asscom = l_asscomm, 515 r_asscomm = r_asscomm, 516 non_coeff = non_coeff, 517 merge = merge, 518*) 519 520(*========================================================================== 521 * end of structure 522 *==========================================================================*) 523end; 524