1(* ========================================================================= *) 2(* FIELD THEORY TOOLS *) 3(* ========================================================================= *) 4 5structure fieldTools :> fieldTools = 6struct 7 8open HolKernel Parse boolLib bossLib res_quanLib groupTools fieldTheory; 9 10val Bug = mlibUseful.Bug; 11 12val cond_rewr_conv = subtypeTools.cond_rewr_conv; 13 14val cond_rewrs_conv = subtypeTools.cond_rewrs_conv; 15 16val named_conv_to_simpset_conv = subtypeTools.named_conv_to_simpset_conv; 17 18(* ------------------------------------------------------------------------- *) 19(* Syntax operations. *) 20(* ------------------------------------------------------------------------- *) 21 22val field_ty_op = "field"; 23 24fun mk_field_type ty = mk_type (field_ty_op,[ty]); 25 26fun dest_field_type ty = 27 case dest_type ty of 28 (ty_op,[a]) => if ty_op = field_ty_op then a 29 else raise ERR "dest_field_type" "" 30 | _ => raise ERR "dest_field_type" ""; 31 32val is_field_type = can dest_field_type; 33 34val field_zero_tm = ``field_zero : 'a field -> 'a``; 35 36fun mk_field_zero f = 37 let 38 val ty = dest_field_type (type_of f) 39 val zero_tm = inst [{redex = alpha, residue = ty}] field_zero_tm 40 in 41 mk_comb (zero_tm,f) 42 end; 43 44fun dest_field_zero tm = 45 let 46 val (tm,f) = dest_comb tm 47 val _ = same_const tm field_zero_tm orelse raise ERR "dest_field_zero" "" 48 in 49 f 50 end; 51 52val is_field_zero = can dest_field_zero; 53 54val field_one_tm = ``field_one : 'a field -> 'a``; 55 56fun mk_field_one f = 57 let 58 val ty = dest_field_type (type_of f) 59 val one_tm = inst [{redex = alpha, residue = ty}] field_one_tm 60 in 61 mk_comb (one_tm,f) 62 end; 63 64fun dest_field_one tm = 65 let 66 val (tm,f) = dest_comb tm 67 val _ = same_const tm field_one_tm orelse raise ERR "dest_field_one" "" 68 in 69 f 70 end; 71 72val is_field_one = can dest_field_one; 73 74val field_num_tm = ``field_num : 'a field -> num -> 'a``; 75 76fun mk_field_num (f,n) = 77 let 78 val ty = dest_field_type (type_of f) 79 val num_tm = inst [{redex = alpha, residue = ty}] field_num_tm 80 in 81 list_mk_comb (num_tm,[f,n]) 82 end; 83 84fun dest_field_num tm = 85 let 86 val (tm,x) = dest_comb tm 87 val (tm,f) = dest_comb tm 88 val _ = same_const tm field_num_tm orelse raise ERR "dest_field_num" "" 89 in 90 (f,x) 91 end; 92 93val is_field_num = can dest_field_num; 94 95val field_neg_tm = ``field_neg : 'a field -> 'a -> 'a``; 96 97fun mk_field_neg (f,x) = 98 let 99 val ty = dest_field_type (type_of f) 100 val neg_tm = inst [{redex = alpha, residue = ty}] field_neg_tm 101 in 102 list_mk_comb (neg_tm,[f,x]) 103 end; 104 105fun dest_field_neg tm = 106 let 107 val (tm,x) = dest_comb tm 108 val (tm,f) = dest_comb tm 109 val _ = same_const tm field_neg_tm orelse raise ERR "dest_field_neg" "" 110 in 111 (f,x) 112 end; 113 114val is_field_neg = can dest_field_neg; 115 116val field_add_tm = ``field_add : 'a field -> 'a -> 'a -> 'a``; 117 118fun mk_field_add (f,x,y) = 119 let 120 val ty = dest_field_type (type_of f) 121 val add_tm = inst [{redex = alpha, residue = ty}] field_add_tm 122 in 123 list_mk_comb (add_tm,[f,x,y]) 124 end; 125 126fun dest_field_add tm = 127 let 128 val (tm,y) = dest_comb tm 129 val (tm,x) = dest_comb tm 130 val (tm,f) = dest_comb tm 131 val _ = same_const tm field_add_tm orelse raise ERR "dest_field_add" "" 132 in 133 (f,x,y) 134 end; 135 136val is_field_add = can dest_field_add; 137 138val field_sub_tm = ``field_sub : 'a field -> 'a -> 'a -> 'a``; 139 140fun mk_field_sub (f,x,y) = 141 let 142 val ty = dest_field_type (type_of f) 143 val sub_tm = inst [{redex = alpha, residue = ty}] field_sub_tm 144 in 145 list_mk_comb (sub_tm,[f,x,y]) 146 end; 147 148fun dest_field_sub tm = 149 let 150 val (tm,y) = dest_comb tm 151 val (tm,x) = dest_comb tm 152 val (tm,f) = dest_comb tm 153 val _ = same_const tm field_sub_tm orelse raise ERR "dest_field_sub" "" 154 in 155 (f,x,y) 156 end; 157 158val is_field_sub = can dest_field_sub; 159 160val field_inv_tm = ``field_inv : 'a field -> 'a -> 'a``; 161 162fun mk_field_inv (f,x) = 163 let 164 val ty = dest_field_type (type_of f) 165 val inv_tm = inst [{redex = alpha, residue = ty}] field_inv_tm 166 in 167 list_mk_comb (inv_tm,[f,x]) 168 end; 169 170fun dest_field_inv tm = 171 let 172 val (tm,x) = dest_comb tm 173 val (tm,f) = dest_comb tm 174 val _ = same_const tm field_inv_tm orelse raise ERR "dest_field_inv" "" 175 in 176 (f,x) 177 end; 178 179val is_field_inv = can dest_field_inv; 180 181val field_mult_tm = ``field_mult : 'a field -> 'a -> 'a -> 'a``; 182 183fun mk_field_mult (f,x,y) = 184 let 185 val ty = dest_field_type (type_of f) 186 val mult_tm = inst [{redex = alpha, residue = ty}] field_mult_tm 187 in 188 list_mk_comb (mult_tm,[f,x,y]) 189 end; 190 191fun dest_field_mult tm = 192 let 193 val (tm,y) = dest_comb tm 194 val (tm,x) = dest_comb tm 195 val (tm,f) = dest_comb tm 196 val _ = same_const tm field_mult_tm orelse raise ERR "dest_field_mult" "" 197 in 198 (f,x,y) 199 end; 200 201val is_field_mult = can dest_field_mult; 202 203val field_exp_tm = ``field_exp : 'a field -> 'a -> num -> 'a``; 204 205fun mk_field_exp (f,x,n) = 206 let 207 val ty = dest_field_type (type_of f) 208 val exp_tm = inst [{redex = alpha, residue = ty}] field_exp_tm 209 in 210 list_mk_comb (exp_tm,[f,x,n]) 211 end; 212 213fun dest_field_exp tm = 214 let 215 val (tm,n) = dest_comb tm 216 val (tm,x) = dest_comb tm 217 val (tm,f) = dest_comb tm 218 val _ = same_const tm field_exp_tm orelse raise ERR "dest_field_exp" "" 219 in 220 (f,x,n) 221 end; 222 223val is_field_exp = can dest_field_exp; 224 225val field_div_tm = ``field_div : 'a field -> 'a -> 'a -> 'a``; 226 227fun mk_field_div (f,x,y) = 228 let 229 val ty = dest_field_type (type_of f) 230 val div_tm = inst [{redex = alpha, residue = ty}] field_div_tm 231 in 232 list_mk_comb (div_tm,[f,x,y]) 233 end; 234 235fun dest_field_div tm = 236 let 237 val (tm,y) = dest_comb tm 238 val (tm,x) = dest_comb tm 239 val (tm,f) = dest_comb tm 240 val _ = same_const tm field_div_tm orelse raise ERR "dest_field_div" "" 241 in 242 (f,x,y) 243 end; 244 245val is_field_div = can dest_field_div; 246 247fun mk_field_num_mult (f,x,n) = mk_field_mult (f, mk_field_num (f,n), x); 248 249fun dest_field_num_mult tm = 250 let 251 val (f,t,x) = dest_field_mult tm 252 val (_,n) = dest_field_num t 253 in 254 (f,x,n) 255 end; 256 257val is_field_num_mult = can dest_field_num_mult; 258 259(* ------------------------------------------------------------------------- *) 260(* Pretty printing. *) 261(* ------------------------------------------------------------------------- *) 262 263val field_pretty_print = ref true; 264 265val field_pretty_print_max_size = ref 1000; 266 267fun field_print Gs sys (ppfns:term_pp_types.ppstream_funs) gravs d pp = 268 let 269 open Portable term_pp_types 270 val (str,brk) = (#add_string ppfns, #add_break ppfns); 271 272 fun field_num tm = 273 let 274 val (_,x) = dest_field_num tm 275 in 276 sys gravs (d - 1) x 277 end 278 279 fun field_unop dest s prec tm = 280 let 281 val (_,x) = dest tm 282 in 283 begin_block pp INCONSISTENT 0; 284 str s; 285 brk (1,0); 286 sys (Prec (prec,s), Top, Top) (d - 1) x; 287 end_block pp 288 end 289 290 fun field_binop_prec x s = 291 let 292 val (p,l,r) = gravs 293 val b = 294 (case p of Prec (y,_) => y > x | _ => false) orelse 295 (case l of Prec (y,_) => y >= x | _ => false) orelse 296 (case r of Prec (y,_) => y > x | _ => false) 297 val p = Prec (x,s) 298 and l = if b then Top else l 299 and r = if b then Top else r 300 in 301 (b,p,l,r) 302 end 303 304 fun field_binop dest s prec tm = 305 let 306 val (_,x,y) = dest tm 307 val (b,p,l,r) = field_binop_prec prec s 308 val n = term_size tm 309 in 310 if n > !field_pretty_print_max_size then 311 (begin_block pp INCONSISTENT 0; 312 str ("<<" ^ int_to_string n ^ ">>"); 313 end_block pp) 314 else 315 (begin_block pp INCONSISTENT (if b then 1 else 0); 316 if b then str "(" else (); 317 sys (p,l,p) (d - 1) x; 318 str (" " ^ s); 319 brk (1,0); 320 sys (p,p,r) (d - 1) y; 321 if b then str ")" else (); 322 end_block pp) 323 end 324 325 fun first_printer [] _ = raise term_pp_types.UserPP_Failed 326 | first_printer (p :: ps) tm = 327 (p tm handle HOL_ERR _ => first_printer ps tm) 328 in 329 fn tm => 330 if not (!field_pretty_print) then raise term_pp_types.UserPP_Failed 331 else 332 first_printer 333 [field_num, 334 field_unop dest_field_neg "~" 900, 335 field_binop dest_field_add "+" 500, 336 field_binop dest_field_sub "-" 500, 337 field_binop dest_field_mult "*" 600, 338 field_binop dest_field_div "/" 600, 339 field_binop dest_field_exp "**" 700] 340 tm 341 end; 342 343val () = temp_add_user_printer ("field_print", Term `x:'a`, field_print); 344 345(* ------------------------------------------------------------------------- *) 346(* AC normalization. *) 347(* ------------------------------------------------------------------------- *) 348 349fun field_compare (x,y) = 350 case (total dest_field_num x, total dest_field_num y) of 351 (NONE,NONE) => compare (x,y) 352 | (SOME _, NONE) => LESS 353 | (NONE, SOME _) => GREATER 354 | (SOME (_,x), SOME (_,y)) => compare (x,y); 355 356val field_add_ac_conv = 357 {name = "field_add_ac_conv", 358 key = ``field_add f x y``, 359 conv = 360 subtypeTools.binop_ac_conv 361 {term_compare = field_compare, 362 dest_binop = dest_field_add, 363 dest_inv = dest_field_neg, 364 dest_exp = dest_field_num_mult, 365 assoc_th = field_add_assoc, 366 comm_th = field_add_comm, 367 comm_th' = field_add_comm', 368 id_ths = 369 [field_add_lzero, 370 field_add_lzero', 371 field_add_rzero, 372 field_add_rzero'], 373 simplify_ths = 374 [GSYM field_num_one, 375 field_neg_zero, 376 field_neg_neg, 377 field_neg_add, 378 field_mult_lzero, 379 field_mult_lzero', 380 field_mult_rzero, 381 field_mult_rzero', 382 field_mult_lone, 383 field_mult_lone', 384 field_mult_rone, 385 field_mult_rone'], 386 combine_ths = 387 [field_single_add_single, 388 field_single_add_mult, 389 field_rneg, 390 field_single_add_neg_mult, 391 field_mult_add_mult, 392 field_mult_add_neg, 393 field_mult_add_neg_mult, 394 field_neg_add_neg, 395 field_neg_add_neg_mult, 396 field_neg_mult_add_neg_mult], 397 combine_ths' = 398 [field_single_add_single', 399 field_single_add_mult', 400 field_rneg', 401 field_single_add_neg_mult', 402 field_mult_add_mult', 403 field_mult_add_neg', 404 field_mult_add_neg_mult', 405 field_neg_add_neg', 406 field_neg_add_neg_mult', 407 field_neg_mult_add_neg_mult']}}; 408 409val field_mult_ac_conv = 410 {name = "field_mult_ac_conv", 411 key = ``field_mult f x y``, 412 conv = 413 subtypeTools.binop_ac_conv 414 {term_compare = field_compare, 415 dest_binop = dest_field_mult, 416 dest_inv = dest_field_inv, 417 dest_exp = dest_field_exp, 418 assoc_th = field_mult_assoc, 419 comm_th = field_mult_comm, 420 comm_th' = field_mult_comm', 421 id_ths = 422 [field_mult_lone, 423 field_mult_lone', 424 field_mult_rone, 425 field_mult_rone'], 426 simplify_ths = 427 [field_inv_one, 428 field_inv_inv, 429 field_inv_mult, 430 field_exp_zero, 431 field_exp_one, 432 field_exp_exp, 433 field_exp_mult, 434 field_exp_inv], 435 combine_ths = 436 [field_single_mult_single, 437 field_single_mult_exp, 438 field_rinv, 439 field_single_mult_inv_exp, 440 field_exp_mult_exp, 441 field_exp_mult_inv, 442 field_exp_mult_inv_exp, 443 field_inv_mult_inv, 444 field_inv_mult_inv_exp, 445 field_inv_exp_mult_inv_exp], 446 combine_ths' = 447 [field_single_mult_single', 448 field_single_mult_exp', 449 field_rinv', 450 field_single_mult_inv_exp', 451 field_exp_mult_exp', 452 field_exp_mult_inv', 453 field_exp_mult_inv_exp', 454 field_inv_mult_inv', 455 field_inv_mult_inv_exp', 456 field_inv_exp_mult_inv_exp']}}; 457 458(* ------------------------------------------------------------------------- *) 459(* Proof tools. *) 460(* ------------------------------------------------------------------------- *) 461 462local 463 val field_sub_eq_zero_conv = 464 let 465 val th = CONV_RULE RES_FORALL_CONV (GSYM field_sub_eq_zero) 466 in 467 fn f => cond_rewr_conv (ISPEC f th) 468 end; 469 470 fun left_conv solver tm = 471 let 472 val (x,y) = dest_eq tm 473 val _ = not (is_field_zero y) orelse 474 raise ERR "field_sub_eq_zero_conv (left)" "looping" 475 val (f,_,_) = dest_field_add x 476 in 477 field_sub_eq_zero_conv f solver 478 end tm; 479 480 fun right_conv solver tm = 481 let 482 val (_,y) = dest_eq tm 483 val (f,_,_) = dest_field_add y 484 in 485 field_sub_eq_zero_conv f solver 486 end tm; 487in 488 val field_sub_eq_zero_l_conv = 489 {name = "field_sub_eq_zero_conv (left)", 490 key = ``field_add (f : 'a field) x y = z``, 491 conv = left_conv} 492 and field_sub_eq_zero_r_conv = 493 {name = "field_sub_eq_zero_conv (right)", 494 key = ``x = field_add (f : 'a field) y z``, 495 conv = right_conv}; 496end; 497 498local 499 fun field_field tm = 500 case total dest_field_zero tm of 501 SOME f => f 502 | NONE => 503 case total dest_field_one tm of 504 SOME f => f 505 | NONE => 506 case total dest_field_num tm of 507 SOME (f,_) => f 508 | NONE => 509 case total dest_field_neg tm of 510 SOME (f,_) => f 511 | NONE => 512 case total dest_field_add tm of 513 SOME (f,_,_) => f 514 | NONE => 515 case total dest_field_mult tm of 516 SOME (f,_,_) => f 517 | NONE => 518 case total dest_field_exp tm of 519 SOME (f,_,_) => f 520 | NONE => raise ERR "field_field" ""; 521 522 fun field_to_exp tm varmap = 523 case total dest_field_zero tm of 524 SOME _ => (Algebra.fromInt 0, varmap) 525 | NONE => 526 case total dest_field_one tm of 527 SOME _ => (Algebra.fromInt 1, varmap) 528 | NONE => 529 case total dest_field_num tm of 530 SOME (_,n) => (Algebra.fromInt (numLib.int_of_term n), varmap) 531 | NONE => 532 case total dest_field_neg tm of 533 SOME (_,a) => 534 let 535 val (a,varmap) = field_to_exp a varmap 536 in 537 (Algebra.negate a, varmap) 538 end 539 | NONE => 540 case total dest_field_add tm of 541 SOME (_,a,b) => 542 let 543 val (a,varmap) = field_to_exp a varmap 544 val (b,varmap) = field_to_exp b varmap 545 in 546 (Algebra.add (a,b), varmap) 547 end 548 | NONE => 549 case total dest_field_sub tm of 550 SOME (_,a,b) => 551 let 552 val (a,varmap) = field_to_exp a varmap 553 val (b,varmap) = field_to_exp b varmap 554 in 555 (Algebra.subtract (a,b), varmap) 556 end 557 | NONE => 558 case total dest_field_mult tm of 559 SOME (_,a,b) => 560 let 561 val (a,varmap) = field_to_exp a varmap 562 val (b,varmap) = field_to_exp b varmap 563 in 564 (Algebra.multiply (a,b), varmap) 565 end 566 | NONE => 567 case total dest_field_exp tm of 568 SOME (_,a,n) => 569 let 570 val (a,varmap) = field_to_exp a varmap 571 in 572 (Algebra.power (a, numLib.int_of_term n), varmap) 573 end 574 | NONE => 575 let 576 val s = term_to_string tm 577 val v = Algebra.Var s 578 in 579 case List.find (equal s o fst) varmap of 580 NONE => (v, (s,tm) :: varmap) 581 | SOME (_,tm') => 582 let 583 val _ = tm = tm' orelse raise Bug "field_to_exp" 584 in 585 (v,varmap) 586 end 587 end; 588 589 fun exp_to_field f varmap e = 590 case Algebra.toInt e of 591 SOME n => 592 if 0 <= n then mk_field_num (f, numLib.term_of_int n) 593 else mk_field_neg (f, mk_field_num (f, numLib.term_of_int (~n))) 594 | NONE => 595 case e of 596 Algebra.Var v => 597 (case List.find (equal v o fst) varmap of 598 NONE => raise Bug "exp_to_field: variable not found" 599 | SOME (_,tm) => tm) 600 | Algebra.Sum m => 601 (case map (exp_sum_to_field f varmap) (rev (Map.toList m)) of 602 [] => raise Bug "exp_to_field: empty sum" 603 | x :: xs => foldl (fn (y,z) => mk_field_add (f,y,z)) x xs) 604 | Algebra.Prod m => 605 (case map (exp_prod_to_field f varmap) (rev (Map.toList m)) of 606 [] => raise Bug "exp_to_field: empty product" 607 | x :: xs => foldl (fn (y,z) => mk_field_mult (f,y,z)) x xs) 608 and exp_sum_to_field f varmap (e,n) = 609 let 610 val e = exp_to_field f varmap e 611 in 612 if n = 1 then e 613 else if n = ~1 then mk_field_neg (f,e) 614 else if 0 <= n then mk_field_num_mult (f, e, numLib.term_of_int n) 615 else mk_field_neg (f, mk_field_num_mult (f, e, numLib.term_of_int (~n))) 616 end 617 and exp_prod_to_field f varmap (e,n) = 618 let 619 val e = exp_to_field f varmap e 620 in 621 if n = 1 then e 622 else if n = ~1 then mk_field_inv (f,e) 623 else if 0 <= n then mk_field_exp (f, e, numLib.term_of_int n) 624 else mk_field_inv (f, mk_field_exp (f, e, numLib.term_of_int (~n))) 625 end; 626in 627 fun ORACLE_field_poly_conv term_normalize_ths _ tm = 628 let 629 val field = field_field tm 630 631 val _ = print ("ORACLE_field_poly_conv: input =\n" 632 ^ term_to_string tm ^ "\n") 633 634 val _ = print ("ORACLE_field_poly_conv: reducing with " 635 ^ int_to_string (length term_normalize_ths) 636 ^ " equations.\n") 637 638 val _ = print ("ORACLE_field_poly_conv: field = " 639 ^ term_to_string field ^ "\n") 640 641 val (exp,varmap) = field_to_exp tm [] 642 643 fun mk_eqn th varmap = 644 let 645 val (l_tm,r_tm) = dest_eq (concl th) 646 val (l_exp,varmap) = field_to_exp l_tm varmap 647 val (r_exp,varmap) = field_to_exp r_tm varmap 648 in 649 ((l_exp,r_exp),varmap) 650 end 651 652 val (eqns,varmap) = Useful.maps mk_eqn term_normalize_ths varmap 653 654 val _ = print ("ORACLE_field_poly_conv: variables =\n\"" 655 ^ Useful.join "\" \"" (map fst varmap) ^ "\"\n") 656 657 val exp = Algebra.normalize {equations = eqns} exp 658 659 val tm' = exp_to_field field varmap exp 660 661 val _ = print ("ORACLE_field_poly_conv: result =\n" 662 ^ term_to_string tm' ^ "\n") 663 664 val _ = tm <> tm' orelse raise ERR "ORACLE_field_poly_conv" "unchanged" 665 in 666 mk_oracle_thm "field_poly" ([], mk_eq (tm,tm')) 667 end; 668end; 669 670local 671 val field_single_mult_exp_alt = prove 672 (``!f x n. 673 f IN Field /\ x IN f.carrier ==> 674 (field_exp f x (SUC n) = field_mult f x (field_exp f x n))``, 675 METIS_TAC [field_single_mult_exp, arithmeticTheory.ADD1]); 676 677 val field_exp_mult_exp_alt = prove 678 (``!f x m n. 679 f IN Field /\ x IN f.carrier ==> 680 (field_exp f x (m + n) = 681 field_mult f (field_exp f x m) (field_exp f x n))``, 682 METIS_TAC [field_exp_mult_exp]); 683 684 val field_mult_lone_conv = 685 let 686 val th = CONV_RULE RES_FORALL_CONV (GSYM field_mult_lone) 687 in 688 fn f => cond_rewr_conv (ISPEC f th) 689 end; 690 691 val field_mult_rone_conv = 692 let 693 val th = CONV_RULE RES_FORALL_CONV (GSYM field_mult_rone) 694 in 695 fn f => cond_rewr_conv (ISPEC f th) 696 end; 697 698 fun field_single_mult_exp_conv f x n = 699 let 700 val th = ISPECL [f, x, numLib.term_of_int n] field_single_mult_exp_alt 701 val conv = RAND_CONV (LAND_CONV (RAND_CONV reduceLib.SUC_CONV)) 702 val th = CONV_RULE conv th 703 in 704 cond_rewr_conv th 705 end; 706 707 fun field_exp_mult_exp_conv f x m n = 708 let 709 val th = field_exp_mult_exp_alt 710 val th = ISPECL [f, x, numLib.term_of_int m, numLib.term_of_int n] th 711 val conv = RAND_CONV (LAND_CONV (RAND_CONV reduceLib.ADD_CONV)) 712 val th = CONV_RULE conv th 713 in 714 cond_rewr_conv th 715 end; 716 717 fun field_mult_presimp_conv solver = 718(*** 719 trace_conv "field_mult_presimp_conv" 720***) 721 (QCONV (TRY_CONV (#conv field_mult_ac_conv solver) THENC 722 reduceLib.REDUCE_CONV)); 723 724 fun field_mult_postsimp_conv solver = 725 BINOP_CONV (field_mult_presimp_conv solver); 726 727 fun dest_field_power tm = 728 case total dest_field_exp tm of 729 NONE => (tm,NONE) 730 | SOME (_,t,n) => (t, SOME (numLib.int_of_term n)) 731 732 fun hcf_power_conv2 f (a,b) = 733 if aconv a b then (field_mult_rone_conv f, field_mult_rone_conv f) 734 else 735 let 736 val _ = not (is_field_mult a) orelse raise Bug "a is a mult" 737 and _ = not (is_field_mult b) orelse raise Bug "b is a mult" 738 739 val (at,an) = dest_field_power a 740 and (bt,bn) = dest_field_power b 741 742 val _ = aconv at bt orelse raise Bug "at <> bt" 743 744 val _ = (case an of NONE => true | SOME n => n >= 2) orelse 745 raise Bug "exponenent of a is less than 2 (nyi)" 746 747 val _ = (case bn of NONE => true | SOME n => n >= 2) orelse 748 raise Bug "exponenent of b is less than 2 (nyi)" 749 in 750 case (an,bn) of 751 (NONE,NONE) => raise Bug "a = b" 752 | (SOME an, NONE) => 753 (field_single_mult_exp_conv f at (an - 1), field_mult_rone_conv f) 754 | (NONE, SOME bn) => 755 (field_mult_rone_conv f, field_single_mult_exp_conv f bt (bn - 1)) 756 | (SOME an, SOME bn) => 757 (case Int.compare (an,bn) of 758 LESS => (field_mult_rone_conv f, 759 field_exp_mult_exp_conv f bt an (bn - an)) 760 | EQUAL => raise Bug "a = b (power)" 761 | GREATER => (field_exp_mult_exp_conv f at bn (an - bn), 762 field_mult_rone_conv f)) 763 end; 764 765 local 766 val field_mult_comm_conv' = cond_rewr_conv field_mult_comm'; 767 768 val field_mult_assoc_conv = cond_rewr_conv field_mult_assoc; 769 770 val field_mult_assoc_conv' = cond_rewr_conv (GSYM field_mult_assoc); 771 in 772 fun push_conv solver a_th = 773 RAND_CONV (K a_th) THENC field_mult_comm_conv' solver; 774 775 fun double_push_conv solver ac a_th = 776 LAND_CONV (ac solver) THENC 777 field_mult_assoc_conv solver THENC 778 RAND_CONV (push_conv solver a_th) THENC 779 field_mult_assoc_conv' solver; 780 end; 781 782 fun hcf_conv2 f solver (a,b) = 783 if is_field_one a orelse is_field_one b then 784 (field_mult_lone_conv f solver a, 785 field_mult_lone_conv f solver b) 786 else if not (is_field_mult a) then 787 let 788 val a_th = field_mult_rone_conv f solver a 789 val (a_th',b_th) = hcf_conv2 f solver (rhs (concl a_th), b) 790 in 791 (TRANS a_th a_th', b_th) 792 end 793 else if not (is_field_mult b) then 794 let 795 val b_th = field_mult_rone_conv f solver b 796 val (a_th,b_th') = hcf_conv2 f solver (a, rhs (concl b_th)) 797 in 798 (a_th, TRANS b_th b_th') 799 end 800 else 801 let 802 val (a1,a2) = 803 case total dest_field_mult a of 804 NONE => raise Bug "a not a mult" 805 | SOME (_,a1,a2) => (a1,a2) 806 807 val (b1,b2) = 808 case total dest_field_mult b of 809 NONE => raise Bug "b not a mult" 810 | SOME (_,b1,b2) => (b1,b2) 811 812 val (at,an) = dest_field_power a1 813 and (bt,bn) = dest_field_power b1 814 in 815 case field_compare (at,bt) of 816 LESS => 817 let 818 val (a_th,b_th) = hcf_conv2 f solver (a2,b) 819 in 820 (push_conv solver a_th a, b_th) 821 end 822 | EQUAL => 823 let 824 val (ac,bc) = hcf_power_conv2 f (a1,b1) 825 val (a_th,b_th) = hcf_conv2 f solver (a2,b2) 826 in 827 (double_push_conv solver ac a_th a, 828 double_push_conv solver bc b_th b) 829 end 830 | GREATER => 831 let 832 val (a_th,b_th) = hcf_conv2 f solver (a,b2) 833 in 834 (a_th, push_conv solver b_th b) 835 end 836 end; 837in 838 fun field_hcf_conv2 f solver (a,b) = 839 let 840(* 841 val () = (print "field_hcf_conv2: "; print_term a; print ", "; 842 print_term b; print "\n") 843*) 844 val a_th = field_mult_presimp_conv solver a 845 and b_th = field_mult_presimp_conv solver b 846(* 847 val () = (print "field_hcf_conv2: "; print_thm a_th; print ", "; 848 print_thm b_th; print "\n") 849*) 850 val (a',b') = (rhs (concl a_th), rhs (concl b_th)) 851 val (a_th',b_th') = hcf_conv2 f solver (a',b') 852 val a_th'' = field_mult_postsimp_conv solver (rhs (concl a_th')) 853 and b_th'' = field_mult_postsimp_conv solver (rhs (concl b_th')) 854 val a_th = TRANS a_th (TRANS a_th' a_th'') 855 and b_th = TRANS b_th (TRANS b_th' b_th'') 856(*** 857 val () = (print "field_hcf_conv2: "; print_thm a_th; print ", "; 858 print_thm b_th; print "\n") 859***) 860 in 861 (a_th,b_th) 862 end; 863end; 864 865local 866 val has_nested_divs = can (find_term (same_const field_div_tm)); 867 868 fun is_normal_numerator tm = not (has_nested_divs tm); 869 870 fun is_normal_denominator tm = not (has_nested_divs tm); 871 872 fun is_normal_fraction is_div tm = 873 if not is_div then is_normal_numerator tm 874 else 875 let 876 val (_,n,d) = dest_field_div tm 877 in 878 is_normal_numerator n andalso is_normal_denominator d 879 end; 880 881 fun check_normal_fraction is_div tm = 882 if is_normal_fraction is_div tm then () 883 else raise ERR "check_normal_fraction" ""; 884 885 val field_add_divl_conv = cond_rewr_conv field_add_divl 886 and field_add_divr_conv = cond_rewr_conv field_add_divr 887 and field_add_div2_conv = cond_rewr_conv field_add_div 888 and field_add_divl_conv' = cond_rewr_conv field_add_divl' 889 and field_add_divr_conv' = cond_rewr_conv field_add_divr' 890 and field_add_div2_conv' = cond_rewr_conv field_add_div'; 891 892 fun field_add_div_hcf solver x1 x2 = 893 let 894 val (f,a1,b1) = dest_field_div x1 895 and (_,a2,b2) = dest_field_div x2 896 in 897 field_hcf_conv2 f solver (b1,b2) 898 end; 899 900 fun field_add_div_hcf_conv (th1,th2) solver = 901 LAND_CONV (RAND_CONV (K th1)) THENC 902 RAND_CONV (RAND_CONV (K th2)) THENC 903 field_add_div2_conv solver; 904 905 fun field_add_div_hcf_conv' (th1,th2) solver = 906 LAND_CONV (RAND_CONV (K th1)) THENC 907 RAND_CONV (LAND_CONV (RAND_CONV (K th2))) THENC 908 field_add_div2_conv' solver; 909 910 fun field_add_div_conv solver tm = 911(*** 912 trace_conv "field_add_div_conv" 913***) 914 let 915 val (f,a,b) = dest_field_add tm 916 val ap = is_field_div a 917 and bp = is_field_div b 918 val () = check_normal_fraction ap a 919 and () = check_normal_fraction bp b 920 in 921 case (ap,bp) of 922 (false,false) => raise ERR "field_add_div_conv" "no div" 923 | (true,false) => field_add_divl_conv solver 924 | (false,true) => field_add_divr_conv solver 925 | (true,true) => 926 field_add_div_hcf_conv (field_add_div_hcf solver a b) solver 927 end tm; 928 929 fun field_add_div_conv' solver tm = 930(*** 931 trace_conv "field_add_div_conv'" 932***) 933 let 934 val (f,a,b) = dest_field_add tm 935 val (_,b,_) = dest_field_add b 936 val ap = is_field_div a 937 and bp = is_field_div b 938 val () = check_normal_fraction ap a 939 and () = check_normal_fraction bp b 940 in 941 case (ap,bp) of 942 (false,false) => raise ERR "field_add_div_conv'" "no div" 943 | (true,false) => field_add_divl_conv' solver 944 | (false,true) => field_add_divr_conv' solver 945 | (true,true) => 946 field_add_div_hcf_conv' (field_add_div_hcf solver a b) solver 947 end tm; 948in 949 val field_add_div_conv_left = 950 {name = "field_add_div_conv (left)", 951 key = ``field_add (f : 'a field) (field_div f x y) z``, 952 conv = field_add_div_conv} 953 and field_add_div_conv_right = 954 {name = "field_add_div_conv (right)", 955 key = ``field_add (f : 'a field) x (field_div f y z)``, 956 conv = field_add_div_conv} 957 and field_add_div_conv_left' = 958 {name = "field_add_div_conv' (left)", 959 key = ``field_add (f : 'a field) (field_div f x y) (field_add f z p)``, 960 conv = field_add_div_conv'} 961 and field_add_div_conv_right' = 962 {name = "field_add_div_conv' (right)", 963 key = ``field_add (f : 'a field) x (field_add f (field_div f y z) p)``, 964 conv = field_add_div_conv'}; 965end; 966 967fun field_div_elim_ss context = 968 let 969 val rewrs = 970 [field_sub_def, 971 field_neg_add, 972 GSYM field_div_lneg, field_div_rneg, 973 field_div_multl,field_div_multr, 974 field_div_divl,field_div_divr, 975 field_div_exp, 976 field_mult_assoc, 977 field_single_mult_single, 978 field_single_mult_single'] 979 980 val convs = 981 map 982 named_conv_to_simpset_conv 983 [field_add_div_conv_left, 984 field_add_div_conv_right] 985 986 val data = 987 simpLib.SSFRAG 988 {name = NONE, ac = [], congs = [], convs = convs, rewrs = rewrs, 989 dprocs = [], filter = NONE} 990 991 val {simplify = alg_ss, ...} = subtypeTools.simpset2 context 992 in 993 simpLib.++ (alg_ss,data) 994 end; 995 996local 997 val add_assoc_conv = cond_rewr_conv field_add_assoc 998 and neg_neg_conv = cond_rewr_conv field_neg_neg 999 and neg_add_conv = cond_rewr_conv field_neg_add 1000 and mult_lneg_conv = cond_rewr_conv field_mult_lneg 1001 and mult_rneg_conv = cond_rewr_conv field_mult_rneg 1002 and distrib_ladd_conv = cond_rewr_conv field_distrib_ladd 1003 and distrib_radd_conv = cond_rewr_conv field_distrib_radd 1004 and mult_assoc_conv = cond_rewr_conv field_mult_assoc 1005 and exp_zero_conv = cond_rewr_conv field_exp_zero 1006 and exp_one_conv = cond_rewr_conv field_exp_one 1007 and exp_num_conv = cond_rewr_conv field_num_exp 1008 and exp_exp_conv = cond_rewr_conv field_exp_exp 1009 and exp_mult_conv = cond_rewr_conv field_exp_mult 1010 and exp_neg_conv = cond_rewr_conv field_exp_neg 1011 and binomial_2_conv = cond_rewr_conv field_binomial_2 1012 and binomial_3_conv = cond_rewr_conv field_binomial_3 1013 and binomial_4_conv = cond_rewr_conv field_binomial_4; 1014 1015 val num_conv = 1016 cond_rewrs_conv [field_num_exp,field_num_mult,field_num_mult']; 1017in 1018 val ORACLE_field_poly = ref false; 1019 1020 val field_poly_print_term = ref false; 1021 1022 fun field_poly_conv term_normalize_ths solver tm = 1023 if !ORACLE_field_poly then 1024 ORACLE_field_poly_conv term_normalize_ths solver tm 1025 else 1026(*** 1027 trace_conv "field_poly_conv" 1028***) 1029 let 1030 val term_normalize_conv = PURE_REWRITE_CONV term_normalize_ths 1031 1032 fun exp_conv tm = 1033 let 1034 val (_,a,n) = dest_field_exp tm 1035 in 1036 FIRST_CONV 1037 [exp_zero_conv solver, 1038 exp_one_conv solver, 1039 exp_num_conv solver THENC RAND_CONV reduceLib.EXP_CONV, 1040 exp_exp_conv solver THENC 1041 TRY_CONV (RAND_CONV reduceLib.MUL_CONV) THENC 1042 TRY_CONV exp_conv, 1043 exp_mult_conv solver, 1044 exp_neg_conv solver THENC 1045 RATOR_CONV (LAND_CONV reduceLib.EVEN_CONV) THENC 1046 COND_CONV, 1047 binomial_2_conv solver, 1048 binomial_3_conv solver, 1049 binomial_4_conv solver] 1050 end tm 1051 1052 fun mult_conv tm = 1053 (case total dest_field_mult tm of 1054 NONE => exp_conv THENC TRY_CONV mult_conv 1055 | SOME (_,a,b) => 1056 FIRST_CONV 1057 [mult_lneg_conv solver, 1058 mult_rneg_conv solver, 1059 distrib_radd_conv solver, 1060 distrib_ladd_conv solver, 1061 mult_assoc_conv solver THENC TRY_CONV mult_conv, 1062 LAND_CONV exp_conv THENC TRY_CONV mult_conv, 1063 RAND_CONV mult_conv THENC TRY_CONV mult_conv]) tm 1064 1065 fun term_conv tm = 1066 (mult_conv ORELSEC 1067 CHANGED_CONV 1068 (TRY_CONV (#conv field_mult_ac_conv solver) THENC 1069 DEPTH_CONV (num_conv solver) THENC 1070 reduceLib.REDUCE_CONV THENC 1071 term_normalize_conv)) tm 1072 1073 fun neg_conv tm = 1074 (case total dest_field_neg tm of 1075 NONE => term_conv THENC TRY_CONV neg_conv 1076 | SOME (_,a) => 1077 FIRST_CONV 1078 [neg_neg_conv solver, 1079 neg_add_conv solver, 1080 RAND_CONV term_conv THENC TRY_CONV neg_conv]) tm 1081 1082 fun add_conv n tm = 1083 (case total dest_field_add tm of 1084 NONE => neg_conv THENC TRY_CONV (add_conv n) 1085 | SOME (_,a,b) => 1086 let 1087 fun print_term_conv conv tm = 1088 let 1089 val n = n + term_size a 1090 val () = print ("term<<" ^ int_to_string n ^ ">>: ") 1091 val () = print_term a 1092 val () = print "\n" 1093 in 1094 conv n tm 1095 end 1096 in 1097 FIRST_CONV 1098 [add_assoc_conv solver THENC TRY_CONV (add_conv n), 1099 LAND_CONV neg_conv THENC TRY_CONV (add_conv n), 1100 print_term_conv (RAND_CONV o add_conv)] 1101 end) tm 1102 1103 val cancel_conv = #conv field_add_ac_conv solver 1104 1105 val poly_conv = 1106 (add_conv 0 THENC TRY_CONV cancel_conv) ORELSEC cancel_conv 1107 in 1108 poly_conv 1109 end tm; 1110end; 1111 1112val field_op_patterns = 1113 [``field_add (f : 'a field) x y``, 1114 ``field_neg (f : 'a field) x``, 1115 ``field_mult (f : 'a field) x y``, 1116 ``field_exp (f : 'a field) x n``, 1117 ``field_num (f : 'a field) n``]; 1118 1119val field_op_blocking_congs = 1120 let 1121 fun in_pattern pattern = 1122 let 1123 val (_,l) = strip_comb pattern 1124 val ty = hd (snd (dest_type (type_of (hd l)))) --> bool 1125 in 1126 pred_setSyntax.mk_in (pattern, mk_var ("s",ty)) 1127 end 1128 1129 val patterns = field_op_patterns 1130 in 1131 map REFL patterns @ map (REFL o in_pattern) patterns 1132 end; 1133 1134fun field_poly_ss context term_normalize_ths = 1135 let 1136 val patterns = field_op_patterns 1137 1138 val congs = field_op_blocking_congs 1139 1140 val convs = 1141 map 1142 (fn (n,key) => 1143 named_conv_to_simpset_conv 1144 {name = "field_poly_conv (" ^ int_to_string n ^ ")", 1145 key = key, 1146 conv = field_poly_conv term_normalize_ths}) 1147 (enumerate 0 patterns) 1148 1149 val data = 1150 simpLib.SSFRAG 1151 {name = NONE, ac = [], congs = congs, convs = convs, rewrs = [], 1152 dprocs = [], filter = NONE} 1153 1154 val {simplify = alg_ss, ...} = subtypeTools.simpset2 context 1155 in 1156 simpLib.++ (alg_ss,data) 1157 end; 1158 1159local 1160 val push_disch = 1161 let 1162 val f = MATCH_MP (PROVE [] ``(a ==> (b = c)) ==> (a ==> b = a ==> c)``) 1163 in 1164 fn d => fn th => f (DISCH d th) 1165 end; 1166 1167 val and_imp_intro = CONV_RULE (BINOP_CONV (REWR_CONV AND_IMP_INTRO)); 1168in 1169 fun field_poly_basis_conv solver tm = 1170 let 1171 fun f [] _ = raise Bug "field_poly_basis_conv" 1172 | f [eqn] th = push_disch eqn th 1173 | f (eqn :: (eqns as _ :: _)) th = 1174 and_imp_intro (push_disch eqn (f eqns th)) 1175 1176 val (eqns,tm) = dest_imp_only tm 1177 val eqns = strip_conj eqns 1178 val reduce_ths = map ASSUME eqns 1179 1180(*** 1181 val _ = print ("field_poly_basis_conv: reducing with " 1182 ^ int_to_string (length eqns) ^ " equations.\n") 1183***) 1184 1185 val th = f eqns (LAND_CONV (field_poly_conv reduce_ths solver) tm) 1186 1187 val _ = (print "field_poly_basis_conv: result thm =\n"; 1188 print_thm th; print "\n") 1189 in 1190 th 1191 end; 1192end; 1193 1194fun field_poly_basis_ss context = 1195 let 1196 val patterns = 1197 [``((x : 'a) = y) ==> (z = field_zero (f : 'a field))``, 1198 ``((x : 'a) = y) /\ E ==> (z = field_zero (f : 'a field))``] 1199 1200 val congs = map REFL patterns @ field_op_blocking_congs 1201 1202 val convs = 1203 map 1204 (fn (n,key) => 1205 named_conv_to_simpset_conv 1206 {name = "field_poly_basis_conv (" ^ int_to_string n ^ ")", 1207 key = key, 1208 conv = field_poly_basis_conv}) 1209 (enumerate 0 patterns) 1210 1211 val data = 1212 simpLib.SSFRAG 1213 {name = NONE, ac = [], congs = [], convs = convs, rewrs = [], 1214 dprocs = [], filter = NONE} 1215 1216 val {simplify = alg_ss, ...} = subtypeTools.simpset2 context 1217 in 1218 simpLib.++ (alg_ss,data) 1219 end; 1220 1221(* ------------------------------------------------------------------------- *) 1222(* Subtype context. *) 1223(* ------------------------------------------------------------------------- *) 1224 1225val context = group_context; 1226val context = subtypeTools.add_rewrite2'' field_sub_def context; 1227val context = subtypeTools.add_judgement2 FiniteField_Field context; 1228val context = subtypeTools.add_judgement2 field_nonzero_carrier context; 1229val context = subtypeTools.add_reduction2 field_zero_carrier context; 1230val context = subtypeTools.add_rewrite2 field_one_zero context; 1231val context = subtypeTools.add_reduction2 field_one_nonzero context; 1232val context = subtypeTools.add_reduction2 field_neg_carrier context; 1233val context = subtypeTools.add_reduction2 field_add_carrier context; 1234val context = subtypeTools.add_rewrite2'' field_add_assoc context; 1235val context = subtypeTools.add_rewrite2 field_num_zero context; 1236val context = subtypeTools.add_rewrite2 field_add_lzero context; 1237val context = subtypeTools.add_rewrite2'' (GSYM field_num_one) context; 1238val context = subtypeTools.add_rewrite2 field_add_lzero' context; 1239val context = subtypeTools.add_rewrite2 field_add_rzero context; 1240val context = subtypeTools.add_rewrite2 field_add_rzero' context; 1241val context = subtypeTools.add_rewrite2 field_lneg context; 1242val context = subtypeTools.add_rewrite2 field_lneg' context; 1243val context = subtypeTools.add_rewrite2 field_rneg context; 1244val context = subtypeTools.add_rewrite2 field_rneg' context; 1245val context = subtypeTools.add_rewrite2' field_add_lcancel context; 1246val context = subtypeTools.add_rewrite2' field_add_rcancel context; 1247val context = subtypeTools.add_reduction2 field_inv_nonzero context; 1248val context = subtypeTools.add_rewrite2 field_mult_lzero context; 1249val context = subtypeTools.add_rewrite2 field_mult_lzero' context; 1250val context = subtypeTools.add_rewrite2 field_mult_rzero context; 1251val context = subtypeTools.add_rewrite2 field_mult_rzero' context; 1252val context = subtypeTools.add_reduction2 field_mult_nonzero context; 1253val context = subtypeTools.add_reduction2 field_mult_carrier context; 1254val context = subtypeTools.add_rewrite2'' field_mult_assoc context; 1255val context = subtypeTools.add_rewrite2' field_entire context; 1256val context = subtypeTools.add_rewrite2 field_mult_lone context; 1257val context = subtypeTools.add_rewrite2 field_mult_lone' context; 1258val context = subtypeTools.add_rewrite2 field_mult_rone context; 1259val context = subtypeTools.add_rewrite2 field_mult_rone' context; 1260val context = subtypeTools.add_rewrite2 field_linv context; 1261val context = subtypeTools.add_rewrite2 field_linv' context; 1262val context = subtypeTools.add_rewrite2 field_rinv context; 1263val context = subtypeTools.add_rewrite2 field_rinv' context; 1264val context = subtypeTools.add_rewrite2' field_mult_lcancel context; 1265val context = subtypeTools.add_rewrite2' field_mult_rcancel context; 1266val context = subtypeTools.add_rewrite2 field_neg_neg context; 1267val context = subtypeTools.add_rewrite2 field_neg_cancel context; 1268val context = subtypeTools.add_rewrite2 field_neg_zero context; 1269val context = subtypeTools.add_rewrite2 field_mult_lneg context; 1270val context = subtypeTools.add_rewrite2 field_mult_rneg context; 1271val context = subtypeTools.add_rewrite2'' field_inv_mult context; 1272val context = subtypeTools.add_reduction2 field_exp_carrier context; 1273val context = subtypeTools.add_reduction2 field_exp_nonzero context; 1274val context = subtypeTools.add_reduction2 field_num_carrier context; 1275val context = subtypeTools.add_rewrite2 field_inv_one context; 1276val context = subtypeTools.add_rewrite2 field_exp_zero context; 1277val context = subtypeTools.add_rewrite2 field_exp_one context; 1278val context = subtypeTools.add_rewrite2'' field_neg_add context; 1279val context = subtypeTools.add_rewrite2 field_num_add context; 1280val context = subtypeTools.add_rewrite2'' field_num_add' context; 1281val context = subtypeTools.add_rewrite2 field_num_mult context; 1282val context = subtypeTools.add_rewrite2'' field_num_mult' context; 1283val context = subtypeTools.add_rewrite2 field_num_exp context; 1284val context = subtypeTools.add_rewrite2'' field_single_add_single context; 1285val context = subtypeTools.add_rewrite2'' field_single_add_single' context; 1286val context = subtypeTools.add_rewrite2'' field_single_add_mult context; 1287val context = subtypeTools.add_rewrite2'' field_single_add_mult' context; 1288val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult context; 1289val context = subtypeTools.add_rewrite2'' field_single_add_neg_mult' context; 1290val context = subtypeTools.add_rewrite2'' field_mult_add_mult context; 1291val context = subtypeTools.add_rewrite2'' field_mult_add_mult' context; 1292val context = subtypeTools.add_rewrite2'' field_mult_add_neg context; 1293val context = subtypeTools.add_rewrite2'' field_mult_add_neg' context; 1294val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult context; 1295val context = subtypeTools.add_rewrite2'' field_mult_add_neg_mult' context; 1296val context = subtypeTools.add_rewrite2'' field_neg_add_neg context; 1297val context = subtypeTools.add_rewrite2'' field_neg_add_neg' context; 1298val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult context; 1299val context = subtypeTools.add_rewrite2'' field_neg_add_neg_mult' context; 1300val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult context; 1301val context = subtypeTools.add_rewrite2'' field_neg_mult_add_neg_mult' context; 1302val context = subtypeTools.add_rewrite2'' field_single_mult_single context; 1303val context = subtypeTools.add_rewrite2'' field_single_mult_single' context; 1304val context = subtypeTools.add_rewrite2'' field_single_mult_exp context; 1305val context = subtypeTools.add_rewrite2'' field_single_mult_exp' context; 1306val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp context; 1307val context = subtypeTools.add_rewrite2'' field_single_mult_inv_exp' context; 1308val context = subtypeTools.add_rewrite2'' field_exp_mult_exp context; 1309val context = subtypeTools.add_rewrite2'' field_exp_mult_exp' context; 1310val context = subtypeTools.add_rewrite2'' field_exp_mult_inv context; 1311val context = subtypeTools.add_rewrite2'' field_exp_mult_inv' context; 1312val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp context; 1313val context = subtypeTools.add_rewrite2'' field_exp_mult_inv_exp' context; 1314val context = subtypeTools.add_rewrite2'' field_inv_mult_inv context; 1315val context = subtypeTools.add_rewrite2'' field_inv_mult_inv' context; 1316val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp context; 1317val context = subtypeTools.add_rewrite2'' field_inv_mult_inv_exp' context; 1318val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp context; 1319val context = subtypeTools.add_rewrite2'' field_inv_exp_mult_inv_exp' context; 1320val context = subtypeTools.add_rewrite2 field_one_exp context; 1321val context = subtypeTools.add_rewrite2 field_zero_exp context; 1322val context = subtypeTools.add_rewrite2 field_exp_eq_zero context; 1323val context = subtypeTools.add_rewrite2'' field_exp_neg context; 1324val context = subtypeTools.add_rewrite2'' field_exp_exp context; 1325val context = subtypeTools.add_conversion2'' field_sub_eq_zero_r_conv context; 1326val context = subtypeTools.add_conversion2'' field_sub_eq_zero_l_conv context; 1327val context = subtypeTools.add_rewrite2 field_inv_inv context; 1328val context = subtypeTools.add_reduction2 field_sub_carrier context; 1329val context = subtypeTools.add_reduction2 field_neg_nonzero context; 1330val context = subtypeTools.add_rewrite2'' field_inv_neg context; 1331val context = subtypeTools.add_rewrite2'' field_exp_mult context; 1332val context = subtypeTools.add_rewrite2'' field_exp_inv context; 1333val context = subtypeTools.add_conversion2'' field_add_ac_conv context; 1334val context = subtypeTools.add_conversion2'' field_mult_ac_conv context; 1335val context = subtypeTools.add_reduction2 field_div_carrier context; 1336val context = subtypeTools.add_reduction2 field_div_nonzero context; 1337val context = subtypeTools.add_rewrite2 field_inv_eq_zero context; 1338val context = subtypeTools.add_rewrite2 field_div_eq_zero context; 1339val context = subtypeTools.add_judgement2 GF_in_carrier_imp context; 1340val context = subtypeTools.add_reduction2 GF context; 1341 1342val field_context = context; 1343 1344end 1345