src/HOL/Tools/int_arith.ML
 author haftmann Mon Mar 23 19:01:15 2009 +0100 (2009-03-23) changeset 30685 dd5fe091ff04 parent 30518 07b45c1aa788 child 30732 afca5be252d6 permissions -rw-r--r--
structure LinArith now named Lin_Arith
 haftmann@30496 ` 1` ```(* Authors: Larry Paulson and Tobias Nipkow ``` wenzelm@23164 ` 2` haftmann@30496 ` 3` ```Simprocs and decision procedure for numerals and linear arithmetic. ``` haftmann@30496 ` 4` ```*) ``` wenzelm@23164 ` 5` wenzelm@23164 ` 6` ```structure Int_Numeral_Simprocs = ``` wenzelm@23164 ` 7` ```struct ``` wenzelm@23164 ` 8` haftmann@30496 ` 9` ```(*reorientation simprules using ==, for the following simproc*) ``` haftmann@30496 ` 10` ```val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection ``` haftmann@30496 ` 11` ```val meta_one_reorient = @{thm one_reorient} RS eq_reflection ``` haftmann@30496 ` 12` ```val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection ``` haftmann@30496 ` 13` haftmann@30496 ` 14` ```(*reorientation simplification procedure: reorients (polymorphic) ``` haftmann@30496 ` 15` ``` 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*) ``` haftmann@30496 ` 16` ```fun reorient_proc sg _ (_ \$ t \$ u) = ``` haftmann@30496 ` 17` ``` case u of ``` haftmann@30496 ` 18` ``` Const(@{const_name HOL.zero}, _) => NONE ``` haftmann@30496 ` 19` ``` | Const(@{const_name HOL.one}, _) => NONE ``` haftmann@30496 ` 20` ``` | Const(@{const_name Int.number_of}, _) \$ _ => NONE ``` haftmann@30496 ` 21` ``` | _ => SOME (case t of ``` haftmann@30496 ` 22` ``` Const(@{const_name HOL.zero}, _) => meta_zero_reorient ``` haftmann@30496 ` 23` ``` | Const(@{const_name HOL.one}, _) => meta_one_reorient ``` haftmann@30496 ` 24` ``` | Const(@{const_name Int.number_of}, _) \$ _ => meta_number_of_reorient) ``` haftmann@30496 ` 25` haftmann@30496 ` 26` ```val reorient_simproc = ``` haftmann@30496 ` 27` ``` Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc); ``` haftmann@30496 ` 28` haftmann@30496 ` 29` ```(*Maps 0 to Numeral0 and 1 to Numeral1 so that arithmetic isn't complicated by the abstract 0 and 1.*) ``` haftmann@25481 ` 30` ```val numeral_syms = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym]; ``` wenzelm@23164 ` 31` wenzelm@23164 ` 32` wenzelm@23164 ` 33` ```(** Utilities **) ``` wenzelm@23164 ` 34` wenzelm@23164 ` 35` ```fun mk_number T n = HOLogic.number_of_const T \$ HOLogic.mk_numeral n; ``` wenzelm@23164 ` 36` wenzelm@23164 ` 37` ```fun find_first_numeral past (t::terms) = ``` wenzelm@23164 ` 38` ``` ((snd (HOLogic.dest_number t), rev past @ terms) ``` wenzelm@23164 ` 39` ``` handle TERM _ => find_first_numeral (t::past) terms) ``` wenzelm@23164 ` 40` ``` | find_first_numeral past [] = raise TERM("find_first_numeral", []); ``` wenzelm@23164 ` 41` wenzelm@23164 ` 42` ```val mk_plus = HOLogic.mk_binop @{const_name HOL.plus}; ``` wenzelm@23164 ` 43` wenzelm@23164 ` 44` ```fun mk_minus t = ``` wenzelm@23164 ` 45` ``` let val T = Term.fastype_of t ``` nipkow@23400 ` 46` ``` in Const (@{const_name HOL.uminus}, T --> T) \$ t end; ``` wenzelm@23164 ` 47` wenzelm@23164 ` 48` ```(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*) ``` wenzelm@23164 ` 49` ```fun mk_sum T [] = mk_number T 0 ``` wenzelm@23164 ` 50` ``` | mk_sum T [t,u] = mk_plus (t, u) ``` wenzelm@23164 ` 51` ``` | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); ``` wenzelm@23164 ` 52` wenzelm@23164 ` 53` ```(*this version ALWAYS includes a trailing zero*) ``` wenzelm@23164 ` 54` ```fun long_mk_sum T [] = mk_number T 0 ``` wenzelm@23164 ` 55` ``` | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts); ``` wenzelm@23164 ` 56` wenzelm@23164 ` 57` ```val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} Term.dummyT; ``` wenzelm@23164 ` 58` wenzelm@23164 ` 59` ```(*decompose additions AND subtractions as a sum*) ``` wenzelm@23164 ` 60` ```fun dest_summing (pos, Const (@{const_name HOL.plus}, _) \$ t \$ u, ts) = ``` wenzelm@23164 ` 61` ``` dest_summing (pos, t, dest_summing (pos, u, ts)) ``` wenzelm@23164 ` 62` ``` | dest_summing (pos, Const (@{const_name HOL.minus}, _) \$ t \$ u, ts) = ``` wenzelm@23164 ` 63` ``` dest_summing (pos, t, dest_summing (not pos, u, ts)) ``` wenzelm@23164 ` 64` ``` | dest_summing (pos, t, ts) = ``` wenzelm@23164 ` 65` ``` if pos then t::ts else mk_minus t :: ts; ``` wenzelm@23164 ` 66` wenzelm@23164 ` 67` ```fun dest_sum t = dest_summing (true, t, []); ``` wenzelm@23164 ` 68` wenzelm@23164 ` 69` ```val mk_diff = HOLogic.mk_binop @{const_name HOL.minus}; ``` wenzelm@23164 ` 70` ```val dest_diff = HOLogic.dest_bin @{const_name HOL.minus} Term.dummyT; ``` wenzelm@23164 ` 71` wenzelm@23164 ` 72` ```val mk_times = HOLogic.mk_binop @{const_name HOL.times}; ``` wenzelm@23164 ` 73` nipkow@23400 ` 74` ```fun one_of T = Const(@{const_name HOL.one},T); ``` nipkow@23400 ` 75` nipkow@23400 ` 76` ```(* build product with trailing 1 rather than Numeral 1 in order to avoid the ``` nipkow@23400 ` 77` ``` unnecessary restriction to type class number_ring ``` nipkow@23400 ` 78` ``` which is not required for cancellation of common factors in divisions. ``` nipkow@23400 ` 79` ```*) ``` wenzelm@23164 ` 80` ```fun mk_prod T = ``` nipkow@23400 ` 81` ``` let val one = one_of T ``` wenzelm@23164 ` 82` ``` fun mk [] = one ``` wenzelm@23164 ` 83` ``` | mk [t] = t ``` wenzelm@23164 ` 84` ``` | mk (t :: ts) = if t = one then mk ts else mk_times (t, mk ts) ``` wenzelm@23164 ` 85` ``` in mk end; ``` wenzelm@23164 ` 86` wenzelm@23164 ` 87` ```(*This version ALWAYS includes a trailing one*) ``` nipkow@23400 ` 88` ```fun long_mk_prod T [] = one_of T ``` wenzelm@23164 ` 89` ``` | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts); ``` wenzelm@23164 ` 90` wenzelm@23164 ` 91` ```val dest_times = HOLogic.dest_bin @{const_name HOL.times} Term.dummyT; ``` wenzelm@23164 ` 92` wenzelm@23164 ` 93` ```fun dest_prod t = ``` wenzelm@23164 ` 94` ``` let val (t,u) = dest_times t ``` nipkow@23400 ` 95` ``` in dest_prod t @ dest_prod u end ``` wenzelm@23164 ` 96` ``` handle TERM _ => [t]; ``` wenzelm@23164 ` 97` wenzelm@23164 ` 98` ```(*DON'T do the obvious simplifications; that would create special cases*) ``` wenzelm@23164 ` 99` ```fun mk_coeff (k, t) = mk_times (mk_number (Term.fastype_of t) k, t); ``` wenzelm@23164 ` 100` wenzelm@23164 ` 101` ```(*Express t as a product of (possibly) a numeral with other sorted terms*) ``` wenzelm@23164 ` 102` ```fun dest_coeff sign (Const (@{const_name HOL.uminus}, _) \$ t) = dest_coeff (~sign) t ``` wenzelm@23164 ` 103` ``` | dest_coeff sign t = ``` wenzelm@29269 ` 104` ``` let val ts = sort TermOrd.term_ord (dest_prod t) ``` wenzelm@23164 ` 105` ``` val (n, ts') = find_first_numeral [] ts ``` wenzelm@23164 ` 106` ``` handle TERM _ => (1, ts) ``` wenzelm@23164 ` 107` ``` in (sign*n, mk_prod (Term.fastype_of t) ts') end; ``` wenzelm@23164 ` 108` wenzelm@23164 ` 109` ```(*Find first coefficient-term THAT MATCHES u*) ``` wenzelm@23164 ` 110` ```fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) ``` wenzelm@23164 ` 111` ``` | find_first_coeff past u (t::terms) = ``` wenzelm@23164 ` 112` ``` let val (n,u') = dest_coeff 1 t ``` nipkow@23400 ` 113` ``` in if u aconv u' then (n, rev past @ terms) ``` nipkow@23400 ` 114` ``` else find_first_coeff (t::past) u terms ``` wenzelm@23164 ` 115` ``` end ``` wenzelm@23164 ` 116` ``` handle TERM _ => find_first_coeff (t::past) u terms; ``` wenzelm@23164 ` 117` wenzelm@23164 ` 118` ```(*Fractions as pairs of ints. Can't use Rat.rat because the representation ``` wenzelm@23164 ` 119` ``` needs to preserve negative values in the denominator.*) ``` wenzelm@24630 ` 120` ```fun mk_frac (p, q) = if q = 0 then raise Div else (p, q); ``` wenzelm@23164 ` 121` wenzelm@23164 ` 122` ```(*Don't reduce fractions; sums must be proved by rule add_frac_eq. ``` wenzelm@23164 ` 123` ``` Fractions are reduced later by the cancel_numeral_factor simproc.*) ``` wenzelm@24630 ` 124` ```fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2); ``` wenzelm@23164 ` 125` wenzelm@23164 ` 126` ```val mk_divide = HOLogic.mk_binop @{const_name HOL.divide}; ``` wenzelm@23164 ` 127` wenzelm@23164 ` 128` ```(*Build term (p / q) * t*) ``` wenzelm@23164 ` 129` ```fun mk_fcoeff ((p, q), t) = ``` wenzelm@23164 ` 130` ``` let val T = Term.fastype_of t ``` nipkow@23400 ` 131` ``` in mk_times (mk_divide (mk_number T p, mk_number T q), t) end; ``` wenzelm@23164 ` 132` wenzelm@23164 ` 133` ```(*Express t as a product of a fraction with other sorted terms*) ``` wenzelm@23164 ` 134` ```fun dest_fcoeff sign (Const (@{const_name HOL.uminus}, _) \$ t) = dest_fcoeff (~sign) t ``` wenzelm@23164 ` 135` ``` | dest_fcoeff sign (Const (@{const_name HOL.divide}, _) \$ t \$ u) = ``` wenzelm@23164 ` 136` ``` let val (p, t') = dest_coeff sign t ``` wenzelm@23164 ` 137` ``` val (q, u') = dest_coeff 1 u ``` nipkow@23400 ` 138` ``` in (mk_frac (p, q), mk_divide (t', u')) end ``` wenzelm@23164 ` 139` ``` | dest_fcoeff sign t = ``` wenzelm@23164 ` 140` ``` let val (p, t') = dest_coeff sign t ``` wenzelm@23164 ` 141` ``` val T = Term.fastype_of t ``` nipkow@23400 ` 142` ``` in (mk_frac (p, 1), mk_divide (t', one_of T)) end; ``` wenzelm@23164 ` 143` wenzelm@23164 ` 144` haftmann@30518 ` 145` ```(** New term ordering so that AC-rewriting brings numerals to the front **) ``` haftmann@30518 ` 146` haftmann@30518 ` 147` ```(*Order integers by absolute value and then by sign. The standard integer ``` haftmann@30518 ` 148` ``` ordering is not well-founded.*) ``` haftmann@30518 ` 149` ```fun num_ord (i,j) = ``` haftmann@30518 ` 150` ``` (case int_ord (abs i, abs j) of ``` haftmann@30518 ` 151` ``` EQUAL => int_ord (Int.sign i, Int.sign j) ``` haftmann@30518 ` 152` ``` | ord => ord); ``` haftmann@30518 ` 153` haftmann@30518 ` 154` ```(*This resembles TermOrd.term_ord, but it puts binary numerals before other ``` haftmann@30518 ` 155` ``` non-atomic terms.*) ``` haftmann@30518 ` 156` ```local open Term ``` haftmann@30518 ` 157` ```in ``` haftmann@30518 ` 158` ```fun numterm_ord (Abs (_, T, t), Abs(_, U, u)) = ``` haftmann@30518 ` 159` ``` (case numterm_ord (t, u) of EQUAL => TermOrd.typ_ord (T, U) | ord => ord) ``` haftmann@30518 ` 160` ``` | numterm_ord ``` haftmann@30518 ` 161` ``` (Const(@{const_name Int.number_of}, _) \$ v, Const(@{const_name Int.number_of}, _) \$ w) = ``` haftmann@30518 ` 162` ``` num_ord (HOLogic.dest_numeral v, HOLogic.dest_numeral w) ``` haftmann@30518 ` 163` ``` | numterm_ord (Const(@{const_name Int.number_of}, _) \$ _, _) = LESS ``` haftmann@30518 ` 164` ``` | numterm_ord (_, Const(@{const_name Int.number_of}, _) \$ _) = GREATER ``` haftmann@30518 ` 165` ``` | numterm_ord (t, u) = ``` haftmann@30518 ` 166` ``` (case int_ord (size_of_term t, size_of_term u) of ``` haftmann@30518 ` 167` ``` EQUAL => ``` haftmann@30518 ` 168` ``` let val (f, ts) = strip_comb t and (g, us) = strip_comb u in ``` haftmann@30518 ` 169` ``` (case TermOrd.hd_ord (f, g) of EQUAL => numterms_ord (ts, us) | ord => ord) ``` haftmann@30518 ` 170` ``` end ``` haftmann@30518 ` 171` ``` | ord => ord) ``` haftmann@30518 ` 172` ```and numterms_ord (ts, us) = list_ord numterm_ord (ts, us) ``` haftmann@30518 ` 173` ```end; ``` haftmann@30518 ` 174` haftmann@30518 ` 175` ```fun numtermless tu = (numterm_ord tu = LESS); ``` haftmann@30518 ` 176` haftmann@30518 ` 177` ```val num_ss = HOL_ss settermless numtermless; ``` haftmann@30518 ` 178` haftmann@30518 ` 179` nipkow@23400 ` 180` ```(*Simplify Numeral0+n, n+Numeral0, Numeral1*n, n*Numeral1, 1*x, x*1, x/1 *) ``` wenzelm@23164 ` 181` ```val add_0s = thms "add_0s"; ``` nipkow@23400 ` 182` ```val mult_1s = thms "mult_1s" @ [thm"mult_1_left", thm"mult_1_right", thm"divide_1"]; ``` wenzelm@23164 ` 183` wenzelm@23164 ` 184` ```(*Simplify inverse Numeral1, a/Numeral1*) ``` wenzelm@23164 ` 185` ```val inverse_1s = [@{thm inverse_numeral_1}]; ``` wenzelm@23164 ` 186` ```val divide_1s = [@{thm divide_numeral_1}]; ``` wenzelm@23164 ` 187` wenzelm@23164 ` 188` ```(*To perform binary arithmetic. The "left" rewriting handles patterns ``` haftmann@30496 ` 189` ``` created by the Int_Numeral_Simprocs, such as 3 * (5 * x). *) ``` haftmann@25481 ` 190` ```val simps = [@{thm numeral_0_eq_0} RS sym, @{thm numeral_1_eq_1} RS sym, ``` haftmann@25481 ` 191` ``` @{thm add_number_of_left}, @{thm mult_number_of_left}] @ ``` haftmann@25481 ` 192` ``` @{thms arith_simps} @ @{thms rel_simps}; ``` wenzelm@23164 ` 193` wenzelm@23164 ` 194` ```(*Binary arithmetic BUT NOT ADDITION since it may collapse adjacent terms ``` wenzelm@23164 ` 195` ``` during re-arrangement*) ``` wenzelm@23164 ` 196` ```val non_add_simps = ``` haftmann@25481 ` 197` ``` subtract Thm.eq_thm [@{thm add_number_of_left}, @{thm number_of_add} RS sym] simps; ``` wenzelm@23164 ` 198` wenzelm@23164 ` 199` ```(*To evaluate binary negations of coefficients*) ``` huffman@26075 ` 200` ```val minus_simps = [@{thm numeral_m1_eq_minus_1} RS sym, @{thm number_of_minus} RS sym] @ ``` huffman@26075 ` 201` ``` @{thms minus_bin_simps} @ @{thms pred_bin_simps}; ``` wenzelm@23164 ` 202` wenzelm@23164 ` 203` ```(*To let us treat subtraction as addition*) ``` wenzelm@23164 ` 204` ```val diff_simps = [@{thm diff_minus}, @{thm minus_add_distrib}, @{thm minus_minus}]; ``` wenzelm@23164 ` 205` wenzelm@23164 ` 206` ```(*To let us treat division as multiplication*) ``` wenzelm@23164 ` 207` ```val divide_simps = [@{thm divide_inverse}, @{thm inverse_mult_distrib}, @{thm inverse_inverse_eq}]; ``` wenzelm@23164 ` 208` wenzelm@23164 ` 209` ```(*push the unary minus down: - x * y = x * - y *) ``` wenzelm@23164 ` 210` ```val minus_mult_eq_1_to_2 = ``` wenzelm@23164 ` 211` ``` [@{thm minus_mult_left} RS sym, @{thm minus_mult_right}] MRS trans |> standard; ``` wenzelm@23164 ` 212` wenzelm@23164 ` 213` ```(*to extract again any uncancelled minuses*) ``` wenzelm@23164 ` 214` ```val minus_from_mult_simps = ``` wenzelm@23164 ` 215` ``` [@{thm minus_minus}, @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym]; ``` wenzelm@23164 ` 216` wenzelm@23164 ` 217` ```(*combine unary minus with numeric literals, however nested within a product*) ``` wenzelm@23164 ` 218` ```val mult_minus_simps = ``` wenzelm@23164 ` 219` ``` [@{thm mult_assoc}, @{thm minus_mult_left}, minus_mult_eq_1_to_2]; ``` wenzelm@23164 ` 220` wenzelm@23164 ` 221` ```structure CancelNumeralsCommon = ``` wenzelm@23164 ` 222` ``` struct ``` wenzelm@23164 ` 223` ``` val mk_sum = mk_sum ``` wenzelm@23164 ` 224` ``` val dest_sum = dest_sum ``` wenzelm@23164 ` 225` ``` val mk_coeff = mk_coeff ``` wenzelm@23164 ` 226` ``` val dest_coeff = dest_coeff 1 ``` wenzelm@23164 ` 227` ``` val find_first_coeff = find_first_coeff [] ``` haftmann@30518 ` 228` ``` val trans_tac = K Arith_Data.trans_tac ``` wenzelm@23164 ` 229` wenzelm@23164 ` 230` ``` val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ ``` haftmann@23881 ` 231` ``` diff_simps @ minus_simps @ @{thms add_ac} ``` wenzelm@23164 ` 232` ``` val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps ``` haftmann@23881 ` 233` ``` val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} ``` wenzelm@23164 ` 234` ``` fun norm_tac ss = ``` wenzelm@23164 ` 235` ``` ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) ``` wenzelm@23164 ` 236` ``` THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) ``` wenzelm@23164 ` 237` ``` THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) ``` wenzelm@23164 ` 238` wenzelm@23164 ` 239` ``` val numeral_simp_ss = HOL_ss addsimps add_0s @ simps ``` wenzelm@23164 ` 240` ``` fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) ``` haftmann@30518 ` 241` ``` val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) ``` wenzelm@23164 ` 242` ``` end; ``` wenzelm@23164 ` 243` wenzelm@23164 ` 244` wenzelm@23164 ` 245` ```structure EqCancelNumerals = CancelNumeralsFun ``` wenzelm@23164 ` 246` ``` (open CancelNumeralsCommon ``` haftmann@30496 ` 247` ``` val prove_conv = Arith_Data.prove_conv ``` wenzelm@23164 ` 248` ``` val mk_bal = HOLogic.mk_eq ``` wenzelm@23164 ` 249` ``` val dest_bal = HOLogic.dest_bin "op =" Term.dummyT ``` haftmann@25481 ` 250` ``` val bal_add1 = @{thm eq_add_iff1} RS trans ``` haftmann@25481 ` 251` ``` val bal_add2 = @{thm eq_add_iff2} RS trans ``` wenzelm@23164 ` 252` ```); ``` wenzelm@23164 ` 253` wenzelm@23164 ` 254` ```structure LessCancelNumerals = CancelNumeralsFun ``` wenzelm@23164 ` 255` ``` (open CancelNumeralsCommon ``` haftmann@30496 ` 256` ``` val prove_conv = Arith_Data.prove_conv ``` haftmann@23881 ` 257` ``` val mk_bal = HOLogic.mk_binrel @{const_name HOL.less} ``` haftmann@23881 ` 258` ``` val dest_bal = HOLogic.dest_bin @{const_name HOL.less} Term.dummyT ``` haftmann@25481 ` 259` ``` val bal_add1 = @{thm less_add_iff1} RS trans ``` haftmann@25481 ` 260` ``` val bal_add2 = @{thm less_add_iff2} RS trans ``` wenzelm@23164 ` 261` ```); ``` wenzelm@23164 ` 262` wenzelm@23164 ` 263` ```structure LeCancelNumerals = CancelNumeralsFun ``` wenzelm@23164 ` 264` ``` (open CancelNumeralsCommon ``` haftmann@30496 ` 265` ``` val prove_conv = Arith_Data.prove_conv ``` haftmann@23881 ` 266` ``` val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq} ``` haftmann@23881 ` 267` ``` val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} Term.dummyT ``` haftmann@25481 ` 268` ``` val bal_add1 = @{thm le_add_iff1} RS trans ``` haftmann@25481 ` 269` ``` val bal_add2 = @{thm le_add_iff2} RS trans ``` wenzelm@23164 ` 270` ```); ``` wenzelm@23164 ` 271` wenzelm@23164 ` 272` ```val cancel_numerals = ``` haftmann@30496 ` 273` ``` map Arith_Data.prep_simproc ``` wenzelm@23164 ` 274` ``` [("inteq_cancel_numerals", ``` wenzelm@23164 ` 275` ``` ["(l::'a::number_ring) + m = n", ``` wenzelm@23164 ` 276` ``` "(l::'a::number_ring) = m + n", ``` wenzelm@23164 ` 277` ``` "(l::'a::number_ring) - m = n", ``` wenzelm@23164 ` 278` ``` "(l::'a::number_ring) = m - n", ``` wenzelm@23164 ` 279` ``` "(l::'a::number_ring) * m = n", ``` wenzelm@23164 ` 280` ``` "(l::'a::number_ring) = m * n"], ``` wenzelm@23164 ` 281` ``` K EqCancelNumerals.proc), ``` wenzelm@23164 ` 282` ``` ("intless_cancel_numerals", ``` wenzelm@23164 ` 283` ``` ["(l::'a::{ordered_idom,number_ring}) + m < n", ``` wenzelm@23164 ` 284` ``` "(l::'a::{ordered_idom,number_ring}) < m + n", ``` wenzelm@23164 ` 285` ``` "(l::'a::{ordered_idom,number_ring}) - m < n", ``` wenzelm@23164 ` 286` ``` "(l::'a::{ordered_idom,number_ring}) < m - n", ``` wenzelm@23164 ` 287` ``` "(l::'a::{ordered_idom,number_ring}) * m < n", ``` wenzelm@23164 ` 288` ``` "(l::'a::{ordered_idom,number_ring}) < m * n"], ``` wenzelm@23164 ` 289` ``` K LessCancelNumerals.proc), ``` wenzelm@23164 ` 290` ``` ("intle_cancel_numerals", ``` wenzelm@23164 ` 291` ``` ["(l::'a::{ordered_idom,number_ring}) + m <= n", ``` wenzelm@23164 ` 292` ``` "(l::'a::{ordered_idom,number_ring}) <= m + n", ``` wenzelm@23164 ` 293` ``` "(l::'a::{ordered_idom,number_ring}) - m <= n", ``` wenzelm@23164 ` 294` ``` "(l::'a::{ordered_idom,number_ring}) <= m - n", ``` wenzelm@23164 ` 295` ``` "(l::'a::{ordered_idom,number_ring}) * m <= n", ``` wenzelm@23164 ` 296` ``` "(l::'a::{ordered_idom,number_ring}) <= m * n"], ``` wenzelm@23164 ` 297` ``` K LeCancelNumerals.proc)]; ``` wenzelm@23164 ` 298` wenzelm@23164 ` 299` wenzelm@23164 ` 300` ```structure CombineNumeralsData = ``` wenzelm@23164 ` 301` ``` struct ``` wenzelm@24630 ` 302` ``` type coeff = int ``` wenzelm@24630 ` 303` ``` val iszero = (fn x => x = 0) ``` wenzelm@24630 ` 304` ``` val add = op + ``` wenzelm@23164 ` 305` ``` val mk_sum = long_mk_sum (*to work for e.g. 2*x + 3*x *) ``` wenzelm@23164 ` 306` ``` val dest_sum = dest_sum ``` wenzelm@23164 ` 307` ``` val mk_coeff = mk_coeff ``` wenzelm@23164 ` 308` ``` val dest_coeff = dest_coeff 1 ``` haftmann@25481 ` 309` ``` val left_distrib = @{thm combine_common_factor} RS trans ``` haftmann@30496 ` 310` ``` val prove_conv = Arith_Data.prove_conv_nohyps ``` haftmann@30518 ` 311` ``` val trans_tac = K Arith_Data.trans_tac ``` wenzelm@23164 ` 312` wenzelm@23164 ` 313` ``` val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ ``` haftmann@23881 ` 314` ``` diff_simps @ minus_simps @ @{thms add_ac} ``` wenzelm@23164 ` 315` ``` val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps ``` haftmann@23881 ` 316` ``` val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} ``` wenzelm@23164 ` 317` ``` fun norm_tac ss = ``` wenzelm@23164 ` 318` ``` ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) ``` wenzelm@23164 ` 319` ``` THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) ``` wenzelm@23164 ` 320` ``` THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) ``` wenzelm@23164 ` 321` wenzelm@23164 ` 322` ``` val numeral_simp_ss = HOL_ss addsimps add_0s @ simps ``` wenzelm@23164 ` 323` ``` fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) ``` haftmann@30518 ` 324` ``` val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s) ``` wenzelm@23164 ` 325` ``` end; ``` wenzelm@23164 ` 326` wenzelm@23164 ` 327` ```structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData); ``` wenzelm@23164 ` 328` wenzelm@23164 ` 329` ```(*Version for fields, where coefficients can be fractions*) ``` wenzelm@23164 ` 330` ```structure FieldCombineNumeralsData = ``` wenzelm@23164 ` 331` ``` struct ``` wenzelm@24630 ` 332` ``` type coeff = int * int ``` wenzelm@24630 ` 333` ``` val iszero = (fn (p, q) => p = 0) ``` wenzelm@23164 ` 334` ``` val add = add_frac ``` wenzelm@23164 ` 335` ``` val mk_sum = long_mk_sum ``` wenzelm@23164 ` 336` ``` val dest_sum = dest_sum ``` wenzelm@23164 ` 337` ``` val mk_coeff = mk_fcoeff ``` wenzelm@23164 ` 338` ``` val dest_coeff = dest_fcoeff 1 ``` haftmann@25481 ` 339` ``` val left_distrib = @{thm combine_common_factor} RS trans ``` haftmann@30496 ` 340` ``` val prove_conv = Arith_Data.prove_conv_nohyps ``` haftmann@30518 ` 341` ``` val trans_tac = K Arith_Data.trans_tac ``` wenzelm@23164 ` 342` wenzelm@23164 ` 343` ``` val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ ``` haftmann@23881 ` 344` ``` inverse_1s @ divide_simps @ diff_simps @ minus_simps @ @{thms add_ac} ``` wenzelm@23164 ` 345` ``` val norm_ss2 = num_ss addsimps non_add_simps @ mult_minus_simps ``` haftmann@23881 ` 346` ``` val norm_ss3 = num_ss addsimps minus_from_mult_simps @ @{thms add_ac} @ @{thms mult_ac} ``` wenzelm@23164 ` 347` ``` fun norm_tac ss = ``` wenzelm@23164 ` 348` ``` ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1)) ``` wenzelm@23164 ` 349` ``` THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2)) ``` wenzelm@23164 ` 350` ``` THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss3)) ``` wenzelm@23164 ` 351` wenzelm@23164 ` 352` ``` val numeral_simp_ss = HOL_ss addsimps add_0s @ simps @ [@{thm add_frac_eq}] ``` wenzelm@23164 ` 353` ``` fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) ``` haftmann@30518 ` 354` ``` val simplify_meta_eq = Arith_Data.simplify_meta_eq (add_0s @ mult_1s @ divide_1s) ``` wenzelm@23164 ` 355` ``` end; ``` wenzelm@23164 ` 356` wenzelm@23164 ` 357` ```structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData); ``` wenzelm@23164 ` 358` wenzelm@23164 ` 359` ```val combine_numerals = ``` haftmann@30496 ` 360` ``` Arith_Data.prep_simproc ``` wenzelm@23164 ` 361` ``` ("int_combine_numerals", ``` wenzelm@23164 ` 362` ``` ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], ``` wenzelm@23164 ` 363` ``` K CombineNumerals.proc); ``` wenzelm@23164 ` 364` wenzelm@23164 ` 365` ```val field_combine_numerals = ``` haftmann@30496 ` 366` ``` Arith_Data.prep_simproc ``` wenzelm@23164 ` 367` ``` ("field_combine_numerals", ``` wenzelm@23164 ` 368` ``` ["(i::'a::{number_ring,field,division_by_zero}) + j", ``` wenzelm@23164 ` 369` ``` "(i::'a::{number_ring,field,division_by_zero}) - j"], ``` wenzelm@23164 ` 370` ``` K FieldCombineNumerals.proc); ``` wenzelm@23164 ` 371` haftmann@30496 ` 372` ```(** Constant folding for multiplication in semirings **) ``` haftmann@30496 ` 373` haftmann@30496 ` 374` ```(*We do not need folding for addition: combine_numerals does the same thing*) ``` haftmann@30496 ` 375` haftmann@30496 ` 376` ```structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA = ``` haftmann@30496 ` 377` ```struct ``` haftmann@30496 ` 378` ``` val assoc_ss = HOL_ss addsimps @{thms mult_ac} ``` haftmann@30496 ` 379` ``` val eq_reflection = eq_reflection ``` wenzelm@23164 ` 380` ```end; ``` wenzelm@23164 ` 381` haftmann@30496 ` 382` ```structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data); ``` haftmann@30496 ` 383` haftmann@30496 ` 384` ```val assoc_fold_simproc = ``` haftmann@30496 ` 385` ``` Arith_Data.prep_simproc ``` haftmann@30496 ` 386` ``` ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"], ``` haftmann@30496 ` 387` ``` K Semiring_Times_Assoc.proc); ``` haftmann@30496 ` 388` haftmann@30496 ` 389` ```end; ``` haftmann@30496 ` 390` haftmann@30496 ` 391` ```Addsimprocs [Int_Numeral_Simprocs.reorient_simproc]; ``` wenzelm@23164 ` 392` ```Addsimprocs Int_Numeral_Simprocs.cancel_numerals; ``` wenzelm@23164 ` 393` ```Addsimprocs [Int_Numeral_Simprocs.combine_numerals]; ``` wenzelm@23164 ` 394` ```Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals]; ``` haftmann@30496 ` 395` ```Addsimprocs [Int_Numeral_Simprocs.assoc_fold_simproc]; ``` wenzelm@23164 ` 396` wenzelm@23164 ` 397` ```(*examples: ``` wenzelm@23164 ` 398` ```print_depth 22; ``` wenzelm@23164 ` 399` ```set timing; ``` wenzelm@23164 ` 400` ```set trace_simp; ``` wenzelm@23164 ` 401` ```fun test s = (Goal s, by (Simp_tac 1)); ``` wenzelm@23164 ` 402` wenzelm@23164 ` 403` ```test "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"; ``` wenzelm@23164 ` 404` wenzelm@23164 ` 405` ```test "2*u = (u::int)"; ``` wenzelm@23164 ` 406` ```test "(i + j + 12 + (k::int)) - 15 = y"; ``` wenzelm@23164 ` 407` ```test "(i + j + 12 + (k::int)) - 5 = y"; ``` wenzelm@23164 ` 408` wenzelm@23164 ` 409` ```test "y - b < (b::int)"; ``` wenzelm@23164 ` 410` ```test "y - (3*b + c) < (b::int) - 2*c"; ``` wenzelm@23164 ` 411` wenzelm@23164 ` 412` ```test "(2*x - (u*v) + y) - v*3*u = (w::int)"; ``` wenzelm@23164 ` 413` ```test "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"; ``` wenzelm@23164 ` 414` ```test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"; ``` wenzelm@23164 ` 415` ```test "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"; ``` wenzelm@23164 ` 416` wenzelm@23164 ` 417` ```test "(i + j + 12 + (k::int)) = u + 15 + y"; ``` wenzelm@23164 ` 418` ```test "(i + j*2 + 12 + (k::int)) = j + 5 + y"; ``` wenzelm@23164 ` 419` wenzelm@23164 ` 420` ```test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"; ``` wenzelm@23164 ` 421` wenzelm@23164 ` 422` ```test "a + -(b+c) + b = (d::int)"; ``` wenzelm@23164 ` 423` ```test "a + -(b+c) - b = (d::int)"; ``` wenzelm@23164 ` 424` wenzelm@23164 ` 425` ```(*negative numerals*) ``` wenzelm@23164 ` 426` ```test "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"; ``` wenzelm@23164 ` 427` ```test "(i + j + -3 + (k::int)) < u + 5 + y"; ``` wenzelm@23164 ` 428` ```test "(i + j + 3 + (k::int)) < u + -6 + y"; ``` wenzelm@23164 ` 429` ```test "(i + j + -12 + (k::int)) - 15 = y"; ``` wenzelm@23164 ` 430` ```test "(i + j + 12 + (k::int)) - -15 = y"; ``` wenzelm@23164 ` 431` ```test "(i + j + -12 + (k::int)) - -15 = y"; ``` wenzelm@23164 ` 432` ```*) ``` wenzelm@23164 ` 433` wenzelm@23164 ` 434` ```(*** decision procedure for linear arithmetic ***) ``` wenzelm@23164 ` 435` wenzelm@23164 ` 436` ```(*---------------------------------------------------------------------------*) ``` wenzelm@23164 ` 437` ```(* Linear arithmetic *) ``` wenzelm@23164 ` 438` ```(*---------------------------------------------------------------------------*) ``` wenzelm@23164 ` 439` wenzelm@23164 ` 440` ```(* ``` wenzelm@23164 ` 441` ```Instantiation of the generic linear arithmetic package for int. ``` wenzelm@23164 ` 442` ```*) ``` wenzelm@23164 ` 443` haftmann@30496 ` 444` ```structure Int_Arith = ``` haftmann@30496 ` 445` ```struct ``` haftmann@30496 ` 446` wenzelm@23164 ` 447` ```(* Update parameters of arithmetic prover *) ``` wenzelm@23164 ` 448` nipkow@24266 ` 449` ```(* reduce contradictory =/ if s = @{const_name "HOL.one"} then not (t = @{typ int}) ``` nipkow@24266 ` 492` ``` else s mem_string allowed_consts ``` nipkow@24266 ` 493` ``` | a\$b => check a andalso check b ``` nipkow@24266 ` 494` ``` | _ => false; ``` nipkow@24266 ` 495` nipkow@24266 ` 496` ```val conv = ``` nipkow@24266 ` 497` ``` Simplifier.rewrite ``` nipkow@24266 ` 498` ``` (HOL_basic_ss addsimps ``` nipkow@24266 ` 499` ``` ((map (fn th => th RS sym) [@{thm of_int_add}, @{thm of_int_mult}, ``` nipkow@24266 ` 500` ``` @{thm of_int_diff}, @{thm of_int_minus}])@ ``` nipkow@24266 ` 501` ``` [@{thm of_int_less_iff}, @{thm of_int_le_iff}, @{thm of_int_eq_iff}]) ``` nipkow@24266 ` 502` ``` addsimprocs [zero_to_of_int_zero_simproc,one_to_of_int_one_simproc]); ``` nipkow@24266 ` 503` nipkow@24266 ` 504` ```fun sproc phi ss ct = if check (term_of ct) then SOME (conv ct) else NONE ``` haftmann@30496 ` 505` nipkow@24266 ` 506` ```val lhss' = ``` nipkow@24266 ` 507` ``` [@{cpat "(?x::?'a::ring_char_0) = (?y::?'a)"}, ``` nipkow@24266 ` 508` ``` @{cpat "(?x::?'a::ordered_idom) < (?y::?'a)"}, ``` nipkow@24266 ` 509` ``` @{cpat "(?x::?'a::ordered_idom) <= (?y::?'a)"}] ``` haftmann@30496 ` 510` nipkow@24266 ` 511` ```val zero_one_idom_simproc = ``` nipkow@24266 ` 512` ``` make_simproc {lhss = lhss' , name = "zero_one_idom_simproc", ``` nipkow@24266 ` 513` ``` proc = sproc, identifier = []} ``` nipkow@24266 ` 514` wenzelm@23164 ` 515` ```val add_rules = ``` haftmann@25481 ` 516` ``` simp_thms @ @{thms arith_simps} @ @{thms rel_simps} @ @{thms arith_special} @ ``` wenzelm@23164 ` 517` ``` [@{thm neg_le_iff_le}, @{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}, ``` wenzelm@23164 ` 518` ``` @{thm minus_zero}, @{thm diff_minus}, @{thm left_minus}, @{thm right_minus}, ``` huffman@26086 ` 519` ``` @{thm mult_zero_left}, @{thm mult_zero_right}, @{thm mult_Bit1}, @{thm mult_1_right}, ``` wenzelm@23164 ` 520` ``` @{thm minus_mult_left} RS sym, @{thm minus_mult_right} RS sym, ``` wenzelm@23164 ` 521` ``` @{thm minus_add_distrib}, @{thm minus_minus}, @{thm mult_assoc}, ``` huffman@23365 ` 522` ``` @{thm of_nat_0}, @{thm of_nat_1}, @{thm of_nat_Suc}, @{thm of_nat_add}, ``` huffman@23365 ` 523` ``` @{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, ``` huffman@23365 ` 524` ``` @{thm of_int_mult}] ``` wenzelm@23164 ` 525` huffman@23365 ` 526` ```val nat_inj_thms = [@{thm zle_int} RS iffD2, @{thm int_int_eq} RS iffD2] ``` wenzelm@23164 ` 527` haftmann@30496 ` 528` ```val int_numeral_base_simprocs = Int_Numeral_Simprocs.assoc_fold_simproc :: zero_one_idom_simproc ``` wenzelm@23164 ` 529` ``` :: Int_Numeral_Simprocs.combine_numerals ``` wenzelm@23164 ` 530` ``` :: Int_Numeral_Simprocs.cancel_numerals; ``` wenzelm@23164 ` 531` haftmann@30496 ` 532` ```val setup = ``` haftmann@30685 ` 533` ``` Lin_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => ``` wenzelm@23164 ` 534` ``` {add_mono_thms = add_mono_thms, ``` wenzelm@23164 ` 535` ``` mult_mono_thms = @{thm mult_strict_left_mono} :: @{thm mult_left_mono} :: mult_mono_thms, ``` wenzelm@23164 ` 536` ``` inj_thms = nat_inj_thms @ inj_thms, ``` haftmann@25481 ` 537` ``` lessD = lessD @ [@{thm zless_imp_add1_zle}], ``` wenzelm@23164 ` 538` ``` neqE = neqE, ``` wenzelm@23164 ` 539` ``` simpset = simpset addsimps add_rules ``` haftmann@30496 ` 540` ``` addsimprocs int_numeral_base_simprocs ``` wenzelm@23164 ` 541` ``` addcongs [if_weak_cong]}) #> ``` haftmann@24196 ` 542` ``` arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #> ``` haftmann@25919 ` 543` ``` arith_discrete @{type_name Int.int} ``` wenzelm@23164 ` 544` wenzelm@23164 ` 545` ```val fast_int_arith_simproc = ``` wenzelm@28262 ` 546` ``` Simplifier.simproc (the_context ()) ``` wenzelm@23164 ` 547` ``` "fast_int_arith" ``` wenzelm@23164 ` 548` ``` ["(m::'a::{ordered_idom,number_ring}) < n", ``` wenzelm@23164 ` 549` ``` "(m::'a::{ordered_idom,number_ring}) <= n", ``` haftmann@30685 ` 550` ``` "(m::'a::{ordered_idom,number_ring}) = n"] (K Lin_Arith.lin_arith_simproc); ``` wenzelm@23164 ` 551` haftmann@30496 ` 552` ```end; ``` haftmann@30496 ` 553` haftmann@30496 ` 554` ```Addsimprocs [Int_Arith.fast_int_arith_simproc]; ```