1(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory 2 Copyright 2000 University of Cambridge 3 4Simprocs for the (integer) numerals. 5*) 6 7(*To quote from Provers/Arith/cancel_numeral_factor.ML: 8 9Cancels common coefficients in balanced expressions: 10 11 u*#m ~~ u'*#m' == #n*u ~~ #n'*u' 12 13where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /) 14and d = gcd(m,m') and n=m/d and n'=m'/d. 15*) 16 17signature NUMERAL_SIMPROCS = 18sig 19 val trans_tac: Proof.context -> thm option -> tactic 20 val assoc_fold: Proof.context -> cterm -> thm option 21 val combine_numerals: Proof.context -> cterm -> thm option 22 val eq_cancel_numerals: Proof.context -> cterm -> thm option 23 val less_cancel_numerals: Proof.context -> cterm -> thm option 24 val le_cancel_numerals: Proof.context -> cterm -> thm option 25 val eq_cancel_factor: Proof.context -> cterm -> thm option 26 val le_cancel_factor: Proof.context -> cterm -> thm option 27 val less_cancel_factor: Proof.context -> cterm -> thm option 28 val div_cancel_factor: Proof.context -> cterm -> thm option 29 val mod_cancel_factor: Proof.context -> cterm -> thm option 30 val dvd_cancel_factor: Proof.context -> cterm -> thm option 31 val divide_cancel_factor: Proof.context -> cterm -> thm option 32 val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option 33 val less_cancel_numeral_factor: Proof.context -> cterm -> thm option 34 val le_cancel_numeral_factor: Proof.context -> cterm -> thm option 35 val div_cancel_numeral_factor: Proof.context -> cterm -> thm option 36 val divide_cancel_numeral_factor: Proof.context -> cterm -> thm option 37 val field_combine_numerals: Proof.context -> cterm -> thm option 38 val field_divide_cancel_numeral_factor: simproc 39 val num_ss: simpset 40 val field_comp_conv: Proof.context -> conv 41end; 42 43structure Numeral_Simprocs : NUMERAL_SIMPROCS = 44struct 45 46fun trans_tac _ NONE = all_tac 47 | trans_tac ctxt (SOME th) = ALLGOALS (resolve_tac ctxt [th RS trans]); 48 49val mk_number = Arith_Data.mk_number; 50val mk_sum = Arith_Data.mk_sum; 51val long_mk_sum = Arith_Data.long_mk_sum; 52val dest_sum = Arith_Data.dest_sum; 53 54val mk_times = HOLogic.mk_binop \<^const_name>\<open>Groups.times\<close>; 55 56fun one_of T = Const(\<^const_name>\<open>Groups.one\<close>, T); 57 58(* build product with trailing 1 rather than Numeral 1 in order to avoid the 59 unnecessary restriction to type class number_ring 60 which is not required for cancellation of common factors in divisions. 61 UPDATE: this reasoning no longer applies (number_ring is gone) 62*) 63fun mk_prod T = 64 let val one = one_of T 65 fun mk [] = one 66 | mk [t] = t 67 | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) 68 in mk end; 69 70(*This version ALWAYS includes a trailing one*) 71fun long_mk_prod T [] = one_of T 72 | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); 73 74val dest_times = HOLogic.dest_bin \<^const_name>\<open>Groups.times\<close> dummyT; 75 76fun dest_prod t = 77 let val (t,u) = dest_times t 78 in dest_prod t @ dest_prod u end 79 handle TERM _ => [t]; 80 81fun find_first_numeral past (t::terms) = 82 ((snd (HOLogic.dest_number t), rev past @ terms) 83 handle TERM _ => find_first_numeral (t::past) terms) 84 | find_first_numeral past [] = raise TERM("find_first_numeral", []); 85 86(*DON'T do the obvious simplifications; that would create special cases*) 87fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); 88 89(*Express t as a product of (possibly) a numeral with other sorted terms*) 90fun dest_coeff sign (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ t) = dest_coeff (~sign) t 91 | dest_coeff sign t = 92 let val ts = sort Term_Ord.term_ord (dest_prod t) 93 val (n, ts') = find_first_numeral [] ts 94 handle TERM _ => (1, ts) 95 in (sign*n, mk_prod (Term.fastype_of t) ts') end; 96 97(*Find first coefficient-term THAT MATCHES u*) 98fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 99 | find_first_coeff past u (t::terms) = 100 let val (n,u') = dest_coeff 1 t 101 in if u aconv u' then (n, rev past @ terms) 102 else find_first_coeff (t::past) u terms 103 end 104 handle TERM _ => find_first_coeff (t::past) u terms; 105 106(*Fractions as pairs of ints. Can't use Rat.rat because the representation 107 needs to preserve negative values in the denominator.*) 108fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); 109 110(*Don't reduce fractions; sums must be proved by rule add_frac_eq. 111 Fractions are reduced later by the cancel_numeral_factor simproc.*) 112fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); 113 114val mk_divide = HOLogic.mk_binop \<^const_name>\<open>Rings.divide\<close>; 115 116(*Build term (p / q) * t*) 117fun mk_fcoeff ((p, q), t) = 118 let val T = Term.fastype_of t 119 in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; 120 121(*Express t as a product of a fraction with other sorted terms*) 122fun dest_fcoeff sign (Const (\<^const_name>\<open>Groups.uminus\<close>, _) $ t) = dest_fcoeff (~sign) t 123 | dest_fcoeff sign (Const (\<^const_name>\<open>Rings.divide\<close>, _) $ t $ u) = 124 let val (p, t') = dest_coeff sign t 125 val (q, u') = dest_coeff 1 u 126 in (mk_frac (p, q), mk_divide (t', u')) end 127 | dest_fcoeff sign t = 128 let val (p, t') = dest_coeff sign t 129 val T = Term.fastype_of t 130 in (mk_frac (p, 1), mk_divide (t', one_of T)) end; 131 132 133(** New term ordering so that AC-rewriting brings numerals to the front **) 134 135(*Order integers by absolute value and then by sign. The standard integer 136 ordering is not well-founded.*) 137fun num_ord (i,j) = 138 (case int_ord (abs i, abs j) of 139 EQUAL => int_ord (Int.sign i, Int.sign j) 140 | ord => ord); 141 142(*This resembles Term_Ord.term_ord, but it puts binary numerals before other 143 non-atomic terms.*) 144local open Term 145in 146fun numterm_ord (t, u) = 147 case (try HOLogic.dest_number t, try HOLogic.dest_number u) of 148 (SOME (_, i), SOME (_, j)) => num_ord (i, j) 149 | (SOME _, NONE) => LESS 150 | (NONE, SOME _) => GREATER 151 | _ => ( 152 case (t, u) of 153 (Abs (_, T, t), Abs(_, U, u)) => 154 (prod_ord numterm_ord Term_Ord.typ_ord ((t, T), (u, U))) 155 | _ => ( 156 case int_ord (size_of_term t, size_of_term u) of 157 EQUAL => 158 let val (f, ts) = strip_comb t and (g, us) = strip_comb u in 159 (prod_ord Term_Ord.hd_ord numterms_ord ((f, ts), (g, us))) 160 end 161 | ord => ord)) 162and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) 163end; 164 165val num_ss = 166 simpset_of (put_simpset HOL_basic_ss \<^context> |> Simplifier.set_term_ord numterm_ord); 167 168(*Maps 1 to Numeral1 so that arithmetic isn't complicated by the abstract 1.*) 169val numeral_syms = [@{thm numeral_One} RS sym]; 170 171(*Simplify 0+n, n+0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) 172val add_0s = @{thms add_0_left add_0_right}; 173val mult_1s = @{thms mult_1s divide_numeral_1 mult_1_left mult_1_right mult_minus1 mult_minus1_right div_by_1}; 174 175(* For post-simplification of the rhs of simproc-generated rules *) 176val post_simps = 177 [@{thm numeral_One}, 178 @{thm add_0_left}, @{thm add_0_right}, 179 @{thm mult_zero_left}, @{thm mult_zero_right}, 180 @{thm mult_1_left}, @{thm mult_1_right}, 181 @{thm mult_minus1}, @{thm mult_minus1_right}] 182 183val field_post_simps = 184 post_simps @ [@{thm div_0}, @{thm div_by_1}] 185 186(*Simplify inverse Numeral1*) 187val inverse_1s = [@{thm inverse_numeral_1}]; 188 189(*To perform binary arithmetic. The "left" rewriting handles patterns 190 created by the Numeral_Simprocs, such as 3 * (5 * x). *) 191val simps = 192 [@{thm numeral_One} RS sym] @ 193 @{thms add_numeral_left} @ 194 @{thms add_neg_numeral_left} @ 195 @{thms mult_numeral_left} @ 196 @{thms arith_simps} @ @{thms rel_simps}; 197 198(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms 199 during re-arrangement*) 200val non_add_simps = 201 subtract Thm.eq_thm 202 (@{thms add_numeral_left} @ 203 @{thms add_neg_numeral_left} @ 204 @{thms numeral_plus_numeral} @ 205 @{thms add_neg_numeral_simps}) simps; 206 207(*To evaluate binary negations of coefficients*) 208val minus_simps = [@{thm minus_zero}, @{thm minus_minus}]; 209 210(*To let us treat subtraction as addition*) 211val diff_simps = [@{thm diff_conv_add_uminus}, @{thm minus_add_distrib}, @{thm minus_minus}]; 212 213(*To let us treat division as multiplication*) 214val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; 215 216(*to extract again any uncancelled minuses*) 217val minus_from_mult_simps = 218 [@{thm minus_minus}, @{thm mult_minus_left}, @{thm mult_minus_right}]; 219 220(*combine unary minus with numeric literals, however nested within a product*) 221val mult_minus_simps = 222 [@{thm mult.assoc}, @{thm minus_mult_right}, @{thm minus_mult_commute}, @{thm numeral_times_minus_swap}]; 223 224val norm_ss1 = 225 simpset_of (put_simpset num_ss \<^context> 226 addsimps numeral_syms @ add_0s @ mult_1s @ 227 diff_simps @ minus_simps @ @{thms ac_simps}) 228 229val norm_ss2 = 230 simpset_of (put_simpset num_ss \<^context> 231 addsimps non_add_simps @ mult_minus_simps) 232 233val norm_ss3 = 234 simpset_of (put_simpset num_ss \<^context> 235 addsimps minus_from_mult_simps @ @{thms ac_simps} @ @{thms ac_simps minus_mult_commute}) 236 237structure CancelNumeralsCommon = 238struct 239 val mk_sum = mk_sum 240 val dest_sum = dest_sum 241 val mk_coeff = mk_coeff 242 val dest_coeff = dest_coeff 1 243 val find_first_coeff = find_first_coeff [] 244 val trans_tac = trans_tac 245 246 fun norm_tac ctxt = 247 ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) 248 THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) 249 THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) 250 251 val numeral_simp_ss = 252 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps) 253 fun numeral_simp_tac ctxt = 254 ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) 255 val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps 256 val prove_conv = Arith_Data.prove_conv 257end; 258 259structure EqCancelNumerals = CancelNumeralsFun 260 (open CancelNumeralsCommon 261 val mk_bal = HOLogic.mk_eq 262 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>HOL.eq\<close> dummyT 263 val bal_add1 = @{thm eq_add_iff1} RS trans 264 val bal_add2 = @{thm eq_add_iff2} RS trans 265); 266 267structure LessCancelNumerals = CancelNumeralsFun 268 (open CancelNumeralsCommon 269 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less\<close> 270 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less\<close> dummyT 271 val bal_add1 = @{thm less_add_iff1} RS trans 272 val bal_add2 = @{thm less_add_iff2} RS trans 273); 274 275structure LeCancelNumerals = CancelNumeralsFun 276 (open CancelNumeralsCommon 277 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close> 278 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less_eq\<close> dummyT 279 val bal_add1 = @{thm le_add_iff1} RS trans 280 val bal_add2 = @{thm le_add_iff2} RS trans 281); 282 283val eq_cancel_numerals = EqCancelNumerals.proc 284val less_cancel_numerals = LessCancelNumerals.proc 285val le_cancel_numerals = LeCancelNumerals.proc 286 287structure CombineNumeralsData = 288struct 289 type coeff = int 290 val iszero = (fn x => x = 0) 291 val add = op + 292 val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) 293 val dest_sum = dest_sum 294 val mk_coeff = mk_coeff 295 val dest_coeff = dest_coeff 1 296 val left_distrib = @{thm combine_common_factor} RS trans 297 val prove_conv = Arith_Data.prove_conv_nohyps 298 val trans_tac = trans_tac 299 300 fun norm_tac ctxt = 301 ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) 302 THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) 303 THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) 304 305 val numeral_simp_ss = 306 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps add_0s @ simps) 307 fun numeral_simp_tac ctxt = 308 ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) 309 val simplify_meta_eq = Arith_Data.simplify_meta_eq post_simps 310end; 311 312structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); 313 314(*Version for fields, where coefficients can be fractions*) 315structure FieldCombineNumeralsData = 316struct 317 type coeff = int * int 318 val iszero = (fn (p, _) => p = 0) 319 val add = add_frac 320 val mk_sum = long_mk_sum 321 val dest_sum = dest_sum 322 val mk_coeff = mk_fcoeff 323 val dest_coeff = dest_fcoeff 1 324 val left_distrib = @{thm combine_common_factor} RS trans 325 val prove_conv = Arith_Data.prove_conv_nohyps 326 val trans_tac = trans_tac 327 328 val norm_ss1a = 329 simpset_of (put_simpset norm_ss1 \<^context> addsimps inverse_1s @ divide_simps) 330 fun norm_tac ctxt = 331 ALLGOALS (simp_tac (put_simpset norm_ss1a ctxt)) 332 THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) 333 THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) 334 335 val numeral_simp_ss = 336 simpset_of (put_simpset HOL_basic_ss \<^context> 337 addsimps add_0s @ simps @ [@{thm add_frac_eq}, @{thm not_False_eq_True}]) 338 fun numeral_simp_tac ctxt = 339 ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) 340 val simplify_meta_eq = Arith_Data.simplify_meta_eq field_post_simps 341end; 342 343structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); 344 345val combine_numerals = CombineNumerals.proc 346 347val field_combine_numerals = FieldCombineNumerals.proc 348 349 350(** Constant folding for multiplication in semirings **) 351 352(*We do not need folding for addition: combine_numerals does the same thing*) 353 354structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = 355struct 356 val assoc_ss = simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms ac_simps minus_mult_commute}) 357 val eq_reflection = eq_reflection 358 val is_numeral = can HOLogic.dest_number 359end; 360 361structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); 362 363fun assoc_fold ctxt ct = Semiring_Times_Assoc.proc ctxt (Thm.term_of ct) 364 365structure CancelNumeralFactorCommon = 366struct 367 val mk_coeff = mk_coeff 368 val dest_coeff = dest_coeff 1 369 val trans_tac = trans_tac 370 371 val norm_ss1 = 372 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps minus_from_mult_simps @ mult_1s) 373 val norm_ss2 = 374 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps @ mult_minus_simps) 375 val norm_ss3 = 376 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps @{thms ac_simps minus_mult_commute numeral_times_minus_swap}) 377 fun norm_tac ctxt = 378 ALLGOALS (simp_tac (put_simpset norm_ss1 ctxt)) 379 THEN ALLGOALS (simp_tac (put_simpset norm_ss2 ctxt)) 380 THEN ALLGOALS (simp_tac (put_simpset norm_ss3 ctxt)) 381 382 (* simp_thms are necessary because some of the cancellation rules below 383 (e.g. mult_less_cancel_left) introduce various logical connectives *) 384 val numeral_simp_ss = 385 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps simps @ @{thms simp_thms}) 386 fun numeral_simp_tac ctxt = 387 ALLGOALS (simp_tac (put_simpset numeral_simp_ss ctxt)) 388 val simplify_meta_eq = Arith_Data.simplify_meta_eq 389 ([@{thm Nat.add_0}, @{thm Nat.add_0_right}] @ post_simps) 390 val prove_conv = Arith_Data.prove_conv 391end 392 393(*Version for semiring_div*) 394structure DivCancelNumeralFactor = CancelNumeralFactorFun 395 (open CancelNumeralFactorCommon 396 val mk_bal = HOLogic.mk_binop \<^const_name>\<open>Rings.divide\<close> 397 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Rings.divide\<close> dummyT 398 val cancel = @{thm div_mult_mult1} RS trans 399 val neg_exchanges = false 400) 401 402(*Version for fields*) 403structure DivideCancelNumeralFactor = CancelNumeralFactorFun 404 (open CancelNumeralFactorCommon 405 val mk_bal = HOLogic.mk_binop \<^const_name>\<open>Rings.divide\<close> 406 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Rings.divide\<close> dummyT 407 val cancel = @{thm mult_divide_mult_cancel_left} RS trans 408 val neg_exchanges = false 409) 410 411structure EqCancelNumeralFactor = CancelNumeralFactorFun 412 (open CancelNumeralFactorCommon 413 val mk_bal = HOLogic.mk_eq 414 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>HOL.eq\<close> dummyT 415 val cancel = @{thm mult_cancel_left} RS trans 416 val neg_exchanges = false 417) 418 419structure LessCancelNumeralFactor = CancelNumeralFactorFun 420 (open CancelNumeralFactorCommon 421 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less\<close> 422 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less\<close> dummyT 423 val cancel = @{thm mult_less_cancel_left} RS trans 424 val neg_exchanges = true 425) 426 427structure LeCancelNumeralFactor = CancelNumeralFactorFun 428( 429 open CancelNumeralFactorCommon 430 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close> 431 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less_eq\<close> dummyT 432 val cancel = @{thm mult_le_cancel_left} RS trans 433 val neg_exchanges = true 434) 435 436val eq_cancel_numeral_factor = EqCancelNumeralFactor.proc 437val less_cancel_numeral_factor = LessCancelNumeralFactor.proc 438val le_cancel_numeral_factor = LeCancelNumeralFactor.proc 439val div_cancel_numeral_factor = DivCancelNumeralFactor.proc 440val divide_cancel_numeral_factor = DivideCancelNumeralFactor.proc 441 442val field_divide_cancel_numeral_factor = 443 Simplifier.make_simproc \<^context> "field_divide_cancel_numeral_factor" 444 {lhss = 445 [\<^term>\<open>((l::'a::field) * m) / n\<close>, 446 \<^term>\<open>(l::'a::field) / (m * n)\<close>, 447 \<^term>\<open>((numeral v)::'a::field) / (numeral w)\<close>, 448 \<^term>\<open>((numeral v)::'a::field) / (- numeral w)\<close>, 449 \<^term>\<open>((- numeral v)::'a::field) / (numeral w)\<close>, 450 \<^term>\<open>((- numeral v)::'a::field) / (- numeral w)\<close>], 451 proc = K DivideCancelNumeralFactor.proc} 452 453val field_cancel_numeral_factors = 454 [Simplifier.make_simproc \<^context> "field_eq_cancel_numeral_factor" 455 {lhss = 456 [\<^term>\<open>(l::'a::field) * m = n\<close>, 457 \<^term>\<open>(l::'a::field) = m * n\<close>], 458 proc = K EqCancelNumeralFactor.proc}, 459 field_divide_cancel_numeral_factor] 460 461 462(** Declarations for ExtractCommonTerm **) 463 464(*Find first term that matches u*) 465fun find_first_t past u [] = raise TERM ("find_first_t", []) 466 | find_first_t past u (t::terms) = 467 if u aconv t then (rev past @ terms) 468 else find_first_t (t::past) u terms 469 handle TERM _ => find_first_t (t::past) u terms; 470 471(** Final simplification for the CancelFactor simprocs **) 472val simplify_one = Arith_Data.simplify_meta_eq 473 [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_by_1}, @{thm numeral_One}]; 474 475fun cancel_simplify_meta_eq ctxt cancel_th th = 476 simplify_one ctxt (([th, cancel_th]) MRS trans); 477 478local 479 val Tp_Eq = Thm.reflexive (Thm.cterm_of \<^theory_context>\<open>HOL\<close> HOLogic.Trueprop) 480 fun Eq_True_elim Eq = 481 Thm.equal_elim (Thm.combination Tp_Eq (Thm.symmetric Eq)) @{thm TrueI} 482in 483fun sign_conv pos_th neg_th ctxt t = 484 let val T = fastype_of t; 485 val zero = Const(\<^const_name>\<open>Groups.zero\<close>, T); 486 val less = Const(\<^const_name>\<open>Orderings.less\<close>, [T,T] ---> HOLogic.boolT); 487 val pos = less $ zero $ t and neg = less $ t $ zero 488 fun prove p = 489 SOME (Eq_True_elim (Simplifier.asm_rewrite ctxt (Thm.cterm_of ctxt p))) 490 handle THM _ => NONE 491 in case prove pos of 492 SOME th => SOME(th RS pos_th) 493 | NONE => (case prove neg of 494 SOME th => SOME(th RS neg_th) 495 | NONE => NONE) 496 end; 497end 498 499structure CancelFactorCommon = 500struct 501 val mk_sum = long_mk_prod 502 val dest_sum = dest_prod 503 val mk_coeff = mk_coeff 504 val dest_coeff = dest_coeff 505 val find_first = find_first_t [] 506 val trans_tac = trans_tac 507 val norm_ss = 508 simpset_of (put_simpset HOL_basic_ss \<^context> addsimps mult_1s @ @{thms ac_simps minus_mult_commute}) 509 fun norm_tac ctxt = 510 ALLGOALS (simp_tac (put_simpset norm_ss ctxt)) 511 val simplify_meta_eq = cancel_simplify_meta_eq 512 fun mk_eq (a, b) = HOLogic.mk_Trueprop (HOLogic.mk_eq (a, b)) 513end; 514 515(*mult_cancel_left requires a ring with no zero divisors.*) 516structure EqCancelFactor = ExtractCommonTermFun 517 (open CancelFactorCommon 518 val mk_bal = HOLogic.mk_eq 519 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>HOL.eq\<close> dummyT 520 fun simp_conv _ _ = SOME @{thm mult_cancel_left} 521); 522 523(*for ordered rings*) 524structure LeCancelFactor = ExtractCommonTermFun 525 (open CancelFactorCommon 526 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less_eq\<close> 527 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less_eq\<close> dummyT 528 val simp_conv = sign_conv 529 @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg} 530); 531 532(*for ordered rings*) 533structure LessCancelFactor = ExtractCommonTermFun 534 (open CancelFactorCommon 535 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Orderings.less\<close> 536 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Orderings.less\<close> dummyT 537 val simp_conv = sign_conv 538 @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg} 539); 540 541(*for semirings with division*) 542structure DivCancelFactor = ExtractCommonTermFun 543 (open CancelFactorCommon 544 val mk_bal = HOLogic.mk_binop \<^const_name>\<open>Rings.divide\<close> 545 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Rings.divide\<close> dummyT 546 fun simp_conv _ _ = SOME @{thm div_mult_mult1_if} 547); 548 549structure ModCancelFactor = ExtractCommonTermFun 550 (open CancelFactorCommon 551 val mk_bal = HOLogic.mk_binop \<^const_name>\<open>modulo\<close> 552 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>modulo\<close> dummyT 553 fun simp_conv _ _ = SOME @{thm mod_mult_mult1} 554); 555 556(*for idoms*) 557structure DvdCancelFactor = ExtractCommonTermFun 558 (open CancelFactorCommon 559 val mk_bal = HOLogic.mk_binrel \<^const_name>\<open>Rings.dvd\<close> 560 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Rings.dvd\<close> dummyT 561 fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left} 562); 563 564(*Version for all fields, including unordered ones (type complex).*) 565structure DivideCancelFactor = ExtractCommonTermFun 566 (open CancelFactorCommon 567 val mk_bal = HOLogic.mk_binop \<^const_name>\<open>Rings.divide\<close> 568 val dest_bal = HOLogic.dest_bin \<^const_name>\<open>Rings.divide\<close> dummyT 569 fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if} 570); 571 572fun eq_cancel_factor ctxt ct = EqCancelFactor.proc ctxt (Thm.term_of ct) 573fun le_cancel_factor ctxt ct = LeCancelFactor.proc ctxt (Thm.term_of ct) 574fun less_cancel_factor ctxt ct = LessCancelFactor.proc ctxt (Thm.term_of ct) 575fun div_cancel_factor ctxt ct = DivCancelFactor.proc ctxt (Thm.term_of ct) 576fun mod_cancel_factor ctxt ct = ModCancelFactor.proc ctxt (Thm.term_of ct) 577fun dvd_cancel_factor ctxt ct = DvdCancelFactor.proc ctxt (Thm.term_of ct) 578fun divide_cancel_factor ctxt ct = DivideCancelFactor.proc ctxt (Thm.term_of ct) 579 580local 581 582val cterm_of = Thm.cterm_of \<^context>; 583fun tvar S = (("'a", 0), S); 584 585val zero_tvar = tvar \<^sort>\<open>zero\<close>; 586val zero = cterm_of (Const (\<^const_name>\<open>zero_class.zero\<close>, TVar zero_tvar)); 587 588val type_tvar = tvar \<^sort>\<open>type\<close>; 589val geq = cterm_of (Const (\<^const_name>\<open>HOL.eq\<close>, TVar type_tvar --> TVar type_tvar --> \<^typ>\<open>bool\<close>)); 590 591val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} 592val add_frac_num = mk_meta_eq @{thm "add_frac_num"} 593val add_num_frac = mk_meta_eq @{thm "add_num_frac"} 594 595fun prove_nz ctxt T t = 596 let 597 val z = Thm.instantiate_cterm ([(zero_tvar, T)], []) zero 598 val eq = Thm.instantiate_cterm ([(type_tvar, T)], []) geq 599 val th = 600 Simplifier.rewrite (ctxt addsimps @{thms simp_thms}) 601 (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close> 602 (Thm.apply (Thm.apply eq t) z))) 603 in Thm.equal_elim (Thm.symmetric th) TrueI end 604 605fun proc ctxt ct = 606 let 607 val ((x,y),(w,z)) = 608 (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct 609 val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z,w] 610 val T = Thm.ctyp_of_cterm x 611 val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z] 612 val th = Thm.instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq 613 in SOME (Thm.implies_elim (Thm.implies_elim th y_nz) z_nz) end 614 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE 615 616fun proc2 ctxt ct = 617 let 618 val (l,r) = Thm.dest_binop ct 619 val T = Thm.ctyp_of_cterm l 620 in (case (Thm.term_of l, Thm.term_of r) of 621 (Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_, _) => 622 let val (x,y) = Thm.dest_binop l val z = r 623 val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z] 624 val ynz = prove_nz ctxt T y 625 in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) 626 end 627 | (_, Const (\<^const_name>\<open>Rings.divide\<close>,_)$_$_) => 628 let val (x,y) = Thm.dest_binop r val z = l 629 val _ = map (HOLogic.dest_number o Thm.term_of) [x,y,z] 630 val ynz = prove_nz ctxt T y 631 in SOME (Thm.implies_elim (Thm.instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) 632 end 633 | _ => NONE) 634 end 635 handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE 636 637fun is_number (Const(\<^const_name>\<open>Rings.divide\<close>,_)$a$b) = is_number a andalso is_number b 638 | is_number t = can HOLogic.dest_number t 639 640val is_number = is_number o Thm.term_of 641 642fun proc3 ctxt ct = 643 (case Thm.term_of ct of 644 Const(\<^const_name>\<open>Orderings.less\<close>,_)$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_)$_ => 645 let 646 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop 647 val _ = map is_number [a,b,c] 648 val T = Thm.ctyp_of_cterm c 649 val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} 650 in SOME (mk_meta_eq th) end 651 | Const(\<^const_name>\<open>Orderings.less_eq\<close>,_)$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_)$_ => 652 let 653 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop 654 val _ = map is_number [a,b,c] 655 val T = Thm.ctyp_of_cterm c 656 val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} 657 in SOME (mk_meta_eq th) end 658 | Const(\<^const_name>\<open>HOL.eq\<close>,_)$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_)$_ => 659 let 660 val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop 661 val _ = map is_number [a,b,c] 662 val T = Thm.ctyp_of_cterm c 663 val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} 664 in SOME (mk_meta_eq th) end 665 | Const(\<^const_name>\<open>Orderings.less\<close>,_)$_$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_) => 666 let 667 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop 668 val _ = map is_number [a,b,c] 669 val T = Thm.ctyp_of_cterm c 670 val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} 671 in SOME (mk_meta_eq th) end 672 | Const(\<^const_name>\<open>Orderings.less_eq\<close>,_)$_$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_) => 673 let 674 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop 675 val _ = map is_number [a,b,c] 676 val T = Thm.ctyp_of_cterm c 677 val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} 678 in SOME (mk_meta_eq th) end 679 | Const(\<^const_name>\<open>HOL.eq\<close>,_)$_$(Const(\<^const_name>\<open>Rings.divide\<close>,_)$_$_) => 680 let 681 val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop 682 val _ = map is_number [a,b,c] 683 val T = Thm.ctyp_of_cterm c 684 val th = Thm.instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} 685 in SOME (mk_meta_eq th) end 686 | _ => NONE) handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE 687 688val add_frac_frac_simproc = 689 Simplifier.make_simproc \<^context> "add_frac_frac_simproc" 690 {lhss = [\<^term>\<open>(x::'a::field) / y + (w::'a::field) / z\<close>], 691 proc = K proc} 692 693val add_frac_num_simproc = 694 Simplifier.make_simproc \<^context> "add_frac_num_simproc" 695 {lhss = [\<^term>\<open>(x::'a::field) / y + z\<close>, \<^term>\<open>z + (x::'a::field) / y\<close>], 696 proc = K proc2} 697 698val ord_frac_simproc = 699 Simplifier.make_simproc \<^context> "ord_frac_simproc" 700 {lhss = 701 [\<^term>\<open>(a::'a::{field,ord}) / b < c\<close>, 702 \<^term>\<open>(a::'a::{field,ord}) / b \<le> c\<close>, 703 \<^term>\<open>c < (a::'a::{field,ord}) / b\<close>, 704 \<^term>\<open>c \<le> (a::'a::{field,ord}) / b\<close>, 705 \<^term>\<open>c = (a::'a::{field,ord}) / b\<close>, 706 \<^term>\<open>(a::'a::{field, ord}) / b = c\<close>], 707 proc = K proc3} 708 709val ths = 710 [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 711 @{thm "divide_numeral_1"}, 712 @{thm "div_by_0"}, @{thm div_0}, 713 @{thm "divide_divide_eq_left"}, 714 @{thm "times_divide_eq_left"}, @{thm "times_divide_eq_right"}, 715 @{thm "times_divide_times_eq"}, 716 @{thm "divide_divide_eq_right"}, 717 @{thm diff_conv_add_uminus}, @{thm "minus_divide_left"}, 718 @{thm "add_divide_distrib"} RS sym, 719 @{thm Fields.field_divide_inverse} RS sym, @{thm inverse_divide}, 720 Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv (Conv.rewr_conv (mk_meta_eq @{thm mult.commute})))) 721 (@{thm Fields.field_divide_inverse} RS sym)] 722 723val field_comp_ss = 724 simpset_of 725 (put_simpset HOL_basic_ss \<^context> 726 addsimps @{thms "semiring_norm"} 727 addsimps ths addsimps @{thms simp_thms} 728 addsimprocs field_cancel_numeral_factors 729 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc, ord_frac_simproc] 730 |> Simplifier.add_cong @{thm "if_weak_cong"}) 731 732in 733 734fun field_comp_conv ctxt = 735 Simplifier.rewrite (put_simpset field_comp_ss ctxt) 736 then_conv 737 Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps [@{thm numeral_One}]) 738 739end 740 741end; 742