src/HOL/Tools/nat_numeral_simprocs.ML
changeset 31068 f591144b0f17
parent 30685 dd5fe091ff04
child 31368 763f4b0fd579
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri May 08 09:48:07 2009 +0200
     1.3 @@ -0,0 +1,538 @@
     1.4 +(* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5 +
     1.6 +Simprocs for nat numerals.
     1.7 +*)
     1.8 +
     1.9 +signature NAT_NUMERAL_SIMPROCS =
    1.10 +sig
    1.11 +  val combine_numerals: simproc
    1.12 +  val cancel_numerals: simproc list
    1.13 +  val cancel_factors: simproc list
    1.14 +  val cancel_numeral_factors: simproc list
    1.15 +end;
    1.16 +
    1.17 +structure Nat_Numeral_Simprocs =
    1.18 +struct
    1.19 +
    1.20 +(*Maps n to #n for n = 0, 1, 2*)
    1.21 +val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    1.22 +val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    1.23 +
    1.24 +fun rename_numerals th =
    1.25 +    simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
    1.26 +
    1.27 +(*Utilities*)
    1.28 +
    1.29 +fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
    1.30 +fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    1.31 +
    1.32 +fun find_first_numeral past (t::terms) =
    1.33 +        ((dest_number t, t, rev past @ terms)
    1.34 +         handle TERM _ => find_first_numeral (t::past) terms)
    1.35 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    1.36 +
    1.37 +val zero = mk_number 0;
    1.38 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    1.39 +
    1.40 +(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    1.41 +fun mk_sum []        = zero
    1.42 +  | mk_sum [t,u]     = mk_plus (t, u)
    1.43 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.44 +
    1.45 +(*this version ALWAYS includes a trailing zero*)
    1.46 +fun long_mk_sum []        = HOLogic.zero
    1.47 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.48 +
    1.49 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    1.50 +
    1.51 +
    1.52 +(** Other simproc items **)
    1.53 +
    1.54 +val bin_simps =
    1.55 +     [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    1.56 +      @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    1.57 +      @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    1.58 +      @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    1.59 +      @{thm less_nat_number_of}, 
    1.60 +      @{thm Let_number_of}, @{thm nat_number_of}] @
    1.61 +     @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
    1.62 +
    1.63 +
    1.64 +(*** CancelNumerals simprocs ***)
    1.65 +
    1.66 +val one = mk_number 1;
    1.67 +val mk_times = HOLogic.mk_binop @{const_name HOL.times};
    1.68 +
    1.69 +fun mk_prod [] = one
    1.70 +  | mk_prod [t] = t
    1.71 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
    1.72 +                        else mk_times (t, mk_prod ts);
    1.73 +
    1.74 +val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
    1.75 +
    1.76 +fun dest_prod t =
    1.77 +      let val (t,u) = dest_times t
    1.78 +      in  dest_prod t @ dest_prod u  end
    1.79 +      handle TERM _ => [t];
    1.80 +
    1.81 +(*DON'T do the obvious simplifications; that would create special cases*)
    1.82 +fun mk_coeff (k,t) = mk_times (mk_number k, t);
    1.83 +
    1.84 +(*Express t as a product of (possibly) a numeral with other factors, sorted*)
    1.85 +fun dest_coeff t =
    1.86 +    let val ts = sort TermOrd.term_ord (dest_prod t)
    1.87 +        val (n, _, ts') = find_first_numeral [] ts
    1.88 +                          handle TERM _ => (1, one, ts)
    1.89 +    in (n, mk_prod ts') end;
    1.90 +
    1.91 +(*Find first coefficient-term THAT MATCHES u*)
    1.92 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    1.93 +  | find_first_coeff past u (t::terms) =
    1.94 +        let val (n,u') = dest_coeff t
    1.95 +        in  if u aconv u' then (n, rev past @ terms)
    1.96 +                          else find_first_coeff (t::past) u terms
    1.97 +        end
    1.98 +        handle TERM _ => find_first_coeff (t::past) u terms;
    1.99 +
   1.100 +
   1.101 +(*Split up a sum into the list of its constituent terms, on the way removing any
   1.102 +  Sucs and counting them.*)
   1.103 +fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
   1.104 +  | dest_Suc_sum (t, (k,ts)) = 
   1.105 +      let val (t1,t2) = dest_plus t
   1.106 +      in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
   1.107 +      handle TERM _ => (k, t::ts);
   1.108 +
   1.109 +(*Code for testing whether numerals are already used in the goal*)
   1.110 +fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
   1.111 +  | is_numeral _ = false;
   1.112 +
   1.113 +fun prod_has_numeral t = exists is_numeral (dest_prod t);
   1.114 +
   1.115 +(*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
   1.116 +  an exception is raised unless the original expression contains at least one
   1.117 +  numeral in a coefficient position.  This prevents nat_combine_numerals from 
   1.118 +  introducing numerals to goals.*)
   1.119 +fun dest_Sucs_sum relaxed t = 
   1.120 +  let val (k,ts) = dest_Suc_sum (t,(0,[]))
   1.121 +  in
   1.122 +     if relaxed orelse exists prod_has_numeral ts then 
   1.123 +       if k=0 then ts
   1.124 +       else mk_number k :: ts
   1.125 +     else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
   1.126 +  end;
   1.127 +
   1.128 +
   1.129 +(*Simplify 1*n and n*1 to n*)
   1.130 +val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
   1.131 +val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
   1.132 +
   1.133 +(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
   1.134 +
   1.135 +(*And these help the simproc return False when appropriate, which helps
   1.136 +  the arith prover.*)
   1.137 +val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
   1.138 +  @{thm Suc_not_Zero}, @{thm le_0_eq}];
   1.139 +
   1.140 +val simplify_meta_eq =
   1.141 +    Arith_Data.simplify_meta_eq
   1.142 +        ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
   1.143 +          @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
   1.144 +
   1.145 +
   1.146 +(*** Applying CancelNumeralsFun ***)
   1.147 +
   1.148 +structure CancelNumeralsCommon =
   1.149 +  struct
   1.150 +  val mk_sum            = (fn T:typ => mk_sum)
   1.151 +  val dest_sum          = dest_Sucs_sum true
   1.152 +  val mk_coeff          = mk_coeff
   1.153 +  val dest_coeff        = dest_coeff
   1.154 +  val find_first_coeff  = find_first_coeff []
   1.155 +  val trans_tac         = K Arith_Data.trans_tac
   1.156 +
   1.157 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   1.158 +    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   1.159 +  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   1.160 +  fun norm_tac ss = 
   1.161 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.162 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.163 +
   1.164 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   1.165 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   1.166 +  val simplify_meta_eq  = simplify_meta_eq
   1.167 +  end;
   1.168 +
   1.169 +
   1.170 +structure EqCancelNumerals = CancelNumeralsFun
   1.171 + (open CancelNumeralsCommon
   1.172 +  val prove_conv = Arith_Data.prove_conv
   1.173 +  val mk_bal   = HOLogic.mk_eq
   1.174 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   1.175 +  val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   1.176 +  val bal_add2 = @{thm nat_eq_add_iff2} RS trans
   1.177 +);
   1.178 +
   1.179 +structure LessCancelNumerals = CancelNumeralsFun
   1.180 + (open CancelNumeralsCommon
   1.181 +  val prove_conv = Arith_Data.prove_conv
   1.182 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   1.183 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   1.184 +  val bal_add1 = @{thm nat_less_add_iff1} RS trans
   1.185 +  val bal_add2 = @{thm nat_less_add_iff2} RS trans
   1.186 +);
   1.187 +
   1.188 +structure LeCancelNumerals = CancelNumeralsFun
   1.189 + (open CancelNumeralsCommon
   1.190 +  val prove_conv = Arith_Data.prove_conv
   1.191 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   1.192 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   1.193 +  val bal_add1 = @{thm nat_le_add_iff1} RS trans
   1.194 +  val bal_add2 = @{thm nat_le_add_iff2} RS trans
   1.195 +);
   1.196 +
   1.197 +structure DiffCancelNumerals = CancelNumeralsFun
   1.198 + (open CancelNumeralsCommon
   1.199 +  val prove_conv = Arith_Data.prove_conv
   1.200 +  val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   1.201 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   1.202 +  val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   1.203 +  val bal_add2 = @{thm nat_diff_add_eq2} RS trans
   1.204 +);
   1.205 +
   1.206 +
   1.207 +val cancel_numerals =
   1.208 +  map Arith_Data.prep_simproc
   1.209 +   [("nateq_cancel_numerals",
   1.210 +     ["(l::nat) + m = n", "(l::nat) = m + n",
   1.211 +      "(l::nat) * m = n", "(l::nat) = m * n",
   1.212 +      "Suc m = n", "m = Suc n"],
   1.213 +     K EqCancelNumerals.proc),
   1.214 +    ("natless_cancel_numerals",
   1.215 +     ["(l::nat) + m < n", "(l::nat) < m + n",
   1.216 +      "(l::nat) * m < n", "(l::nat) < m * n",
   1.217 +      "Suc m < n", "m < Suc n"],
   1.218 +     K LessCancelNumerals.proc),
   1.219 +    ("natle_cancel_numerals",
   1.220 +     ["(l::nat) + m <= n", "(l::nat) <= m + n",
   1.221 +      "(l::nat) * m <= n", "(l::nat) <= m * n",
   1.222 +      "Suc m <= n", "m <= Suc n"],
   1.223 +     K LeCancelNumerals.proc),
   1.224 +    ("natdiff_cancel_numerals",
   1.225 +     ["((l::nat) + m) - n", "(l::nat) - (m + n)",
   1.226 +      "(l::nat) * m - n", "(l::nat) - m * n",
   1.227 +      "Suc m - n", "m - Suc n"],
   1.228 +     K DiffCancelNumerals.proc)];
   1.229 +
   1.230 +
   1.231 +(*** Applying CombineNumeralsFun ***)
   1.232 +
   1.233 +structure CombineNumeralsData =
   1.234 +  struct
   1.235 +  type coeff            = int
   1.236 +  val iszero            = (fn x => x = 0)
   1.237 +  val add               = op +
   1.238 +  val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   1.239 +  val dest_sum          = dest_Sucs_sum false
   1.240 +  val mk_coeff          = mk_coeff
   1.241 +  val dest_coeff        = dest_coeff
   1.242 +  val left_distrib      = @{thm left_add_mult_distrib} RS trans
   1.243 +  val prove_conv        = Arith_Data.prove_conv_nohyps
   1.244 +  val trans_tac         = K Arith_Data.trans_tac
   1.245 +
   1.246 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   1.247 +  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   1.248 +  fun norm_tac ss =
   1.249 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.250 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.251 +
   1.252 +  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   1.253 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.254 +  val simplify_meta_eq  = simplify_meta_eq
   1.255 +  end;
   1.256 +
   1.257 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.258 +
   1.259 +val combine_numerals =
   1.260 +  Arith_Data.prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   1.261 +
   1.262 +
   1.263 +(*** Applying CancelNumeralFactorFun ***)
   1.264 +
   1.265 +structure CancelNumeralFactorCommon =
   1.266 +  struct
   1.267 +  val mk_coeff          = mk_coeff
   1.268 +  val dest_coeff        = dest_coeff
   1.269 +  val trans_tac         = K Arith_Data.trans_tac
   1.270 +
   1.271 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps
   1.272 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   1.273 +  val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   1.274 +  fun norm_tac ss =
   1.275 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.276 +    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.277 +
   1.278 +  val numeral_simp_ss = HOL_ss addsimps bin_simps
   1.279 +  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.280 +  val simplify_meta_eq  = simplify_meta_eq
   1.281 +  end
   1.282 +
   1.283 +structure DivCancelNumeralFactor = CancelNumeralFactorFun
   1.284 + (open CancelNumeralFactorCommon
   1.285 +  val prove_conv = Arith_Data.prove_conv
   1.286 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   1.287 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   1.288 +  val cancel = @{thm nat_mult_div_cancel1} RS trans
   1.289 +  val neg_exchanges = false
   1.290 +)
   1.291 +
   1.292 +structure DvdCancelNumeralFactor = CancelNumeralFactorFun
   1.293 + (open CancelNumeralFactorCommon
   1.294 +  val prove_conv = Arith_Data.prove_conv
   1.295 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   1.296 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   1.297 +  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
   1.298 +  val neg_exchanges = false
   1.299 +)
   1.300 +
   1.301 +structure EqCancelNumeralFactor = CancelNumeralFactorFun
   1.302 + (open CancelNumeralFactorCommon
   1.303 +  val prove_conv = Arith_Data.prove_conv
   1.304 +  val mk_bal   = HOLogic.mk_eq
   1.305 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   1.306 +  val cancel = @{thm nat_mult_eq_cancel1} RS trans
   1.307 +  val neg_exchanges = false
   1.308 +)
   1.309 +
   1.310 +structure LessCancelNumeralFactor = CancelNumeralFactorFun
   1.311 + (open CancelNumeralFactorCommon
   1.312 +  val prove_conv = Arith_Data.prove_conv
   1.313 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   1.314 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   1.315 +  val cancel = @{thm nat_mult_less_cancel1} RS trans
   1.316 +  val neg_exchanges = true
   1.317 +)
   1.318 +
   1.319 +structure LeCancelNumeralFactor = CancelNumeralFactorFun
   1.320 + (open CancelNumeralFactorCommon
   1.321 +  val prove_conv = Arith_Data.prove_conv
   1.322 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   1.323 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   1.324 +  val cancel = @{thm nat_mult_le_cancel1} RS trans
   1.325 +  val neg_exchanges = true
   1.326 +)
   1.327 +
   1.328 +val cancel_numeral_factors =
   1.329 +  map Arith_Data.prep_simproc
   1.330 +   [("nateq_cancel_numeral_factors",
   1.331 +     ["(l::nat) * m = n", "(l::nat) = m * n"],
   1.332 +     K EqCancelNumeralFactor.proc),
   1.333 +    ("natless_cancel_numeral_factors",
   1.334 +     ["(l::nat) * m < n", "(l::nat) < m * n"],
   1.335 +     K LessCancelNumeralFactor.proc),
   1.336 +    ("natle_cancel_numeral_factors",
   1.337 +     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   1.338 +     K LeCancelNumeralFactor.proc),
   1.339 +    ("natdiv_cancel_numeral_factors",
   1.340 +     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   1.341 +     K DivCancelNumeralFactor.proc),
   1.342 +    ("natdvd_cancel_numeral_factors",
   1.343 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   1.344 +     K DvdCancelNumeralFactor.proc)];
   1.345 +
   1.346 +
   1.347 +
   1.348 +(*** Applying ExtractCommonTermFun ***)
   1.349 +
   1.350 +(*this version ALWAYS includes a trailing one*)
   1.351 +fun long_mk_prod []        = one
   1.352 +  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
   1.353 +
   1.354 +(*Find first term that matches u*)
   1.355 +fun find_first_t past u []         = raise TERM("find_first_t", [])
   1.356 +  | find_first_t past u (t::terms) =
   1.357 +        if u aconv t then (rev past @ terms)
   1.358 +        else find_first_t (t::past) u terms
   1.359 +        handle TERM _ => find_first_t (t::past) u terms;
   1.360 +
   1.361 +(** Final simplification for the CancelFactor simprocs **)
   1.362 +val simplify_one = Arith_Data.simplify_meta_eq  
   1.363 +  [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
   1.364 +
   1.365 +fun cancel_simplify_meta_eq ss cancel_th th =
   1.366 +    simplify_one ss (([th, cancel_th]) MRS trans);
   1.367 +
   1.368 +structure CancelFactorCommon =
   1.369 +  struct
   1.370 +  val mk_sum            = (fn T:typ => long_mk_prod)
   1.371 +  val dest_sum          = dest_prod
   1.372 +  val mk_coeff          = mk_coeff
   1.373 +  val dest_coeff        = dest_coeff
   1.374 +  val find_first        = find_first_t []
   1.375 +  val trans_tac         = K Arith_Data.trans_tac
   1.376 +  val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   1.377 +  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   1.378 +  val simplify_meta_eq  = cancel_simplify_meta_eq
   1.379 +  end;
   1.380 +
   1.381 +structure EqCancelFactor = ExtractCommonTermFun
   1.382 + (open CancelFactorCommon
   1.383 +  val prove_conv = Arith_Data.prove_conv
   1.384 +  val mk_bal   = HOLogic.mk_eq
   1.385 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   1.386 +  val simp_conv = K(K (SOME @{thm nat_mult_eq_cancel_disj}))
   1.387 +);
   1.388 +
   1.389 +structure LessCancelFactor = ExtractCommonTermFun
   1.390 + (open CancelFactorCommon
   1.391 +  val prove_conv = Arith_Data.prove_conv
   1.392 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   1.393 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   1.394 +  val simp_conv = K(K (SOME @{thm nat_mult_less_cancel_disj}))
   1.395 +);
   1.396 +
   1.397 +structure LeCancelFactor = ExtractCommonTermFun
   1.398 + (open CancelFactorCommon
   1.399 +  val prove_conv = Arith_Data.prove_conv
   1.400 +  val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   1.401 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   1.402 +  val simp_conv = K(K (SOME @{thm nat_mult_le_cancel_disj}))
   1.403 +);
   1.404 +
   1.405 +structure DivideCancelFactor = ExtractCommonTermFun
   1.406 + (open CancelFactorCommon
   1.407 +  val prove_conv = Arith_Data.prove_conv
   1.408 +  val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   1.409 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   1.410 +  val simp_conv = K(K (SOME @{thm nat_mult_div_cancel_disj}))
   1.411 +);
   1.412 +
   1.413 +structure DvdCancelFactor = ExtractCommonTermFun
   1.414 + (open CancelFactorCommon
   1.415 +  val prove_conv = Arith_Data.prove_conv
   1.416 +  val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
   1.417 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.natT
   1.418 +  val simp_conv = K(K (SOME @{thm nat_mult_dvd_cancel_disj}))
   1.419 +);
   1.420 +
   1.421 +val cancel_factor =
   1.422 +  map Arith_Data.prep_simproc
   1.423 +   [("nat_eq_cancel_factor",
   1.424 +     ["(l::nat) * m = n", "(l::nat) = m * n"],
   1.425 +     K EqCancelFactor.proc),
   1.426 +    ("nat_less_cancel_factor",
   1.427 +     ["(l::nat) * m < n", "(l::nat) < m * n"],
   1.428 +     K LessCancelFactor.proc),
   1.429 +    ("nat_le_cancel_factor",
   1.430 +     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   1.431 +     K LeCancelFactor.proc),
   1.432 +    ("nat_divide_cancel_factor",
   1.433 +     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   1.434 +     K DivideCancelFactor.proc),
   1.435 +    ("nat_dvd_cancel_factor",
   1.436 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   1.437 +     K DvdCancelFactor.proc)];
   1.438 +
   1.439 +end;
   1.440 +
   1.441 +
   1.442 +Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   1.443 +Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   1.444 +Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   1.445 +Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
   1.446 +
   1.447 +
   1.448 +(*examples:
   1.449 +print_depth 22;
   1.450 +set timing;
   1.451 +set trace_simp;
   1.452 +fun test s = (Goal s; by (Simp_tac 1));
   1.453 +
   1.454 +(*cancel_numerals*)
   1.455 +test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
   1.456 +test "(2*length xs < 2*length xs + j)";
   1.457 +test "(2*length xs < length xs * 2 + j)";
   1.458 +test "2*u = (u::nat)";
   1.459 +test "2*u = Suc (u)";
   1.460 +test "(i + j + 12 + (k::nat)) - 15 = y";
   1.461 +test "(i + j + 12 + (k::nat)) - 5 = y";
   1.462 +test "Suc u - 2 = y";
   1.463 +test "Suc (Suc (Suc u)) - 2 = y";
   1.464 +test "(i + j + 2 + (k::nat)) - 1 = y";
   1.465 +test "(i + j + 1 + (k::nat)) - 2 = y";
   1.466 +
   1.467 +test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
   1.468 +test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
   1.469 +test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
   1.470 +test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
   1.471 +test "Suc ((u*v)*4) - v*3*u = w";
   1.472 +test "Suc (Suc ((u*v)*3)) - v*3*u = w";
   1.473 +
   1.474 +test "(i + j + 12 + (k::nat)) = u + 15 + y";
   1.475 +test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
   1.476 +test "(i + j + 12 + (k::nat)) = u + 5 + y";
   1.477 +(*Suc*)
   1.478 +test "(i + j + 12 + k) = Suc (u + y)";
   1.479 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
   1.480 +test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   1.481 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
   1.482 +test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   1.483 +test "2*y + 3*z + 2*u = Suc (u)";
   1.484 +test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
   1.485 +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::nat)";
   1.486 +test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
   1.487 +test "(2*n*m) < (3*(m*n)) + (u::nat)";
   1.488 +
   1.489 +test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
   1.490 + 
   1.491 +test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
   1.492 +
   1.493 +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
   1.494 +
   1.495 +test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))";
   1.496 +
   1.497 +
   1.498 +(*negative numerals: FAIL*)
   1.499 +test "(i + j + -23 + (k::nat)) < u + 15 + y";
   1.500 +test "(i + j + 3 + (k::nat)) < u + -15 + y";
   1.501 +test "(i + j + -12 + (k::nat)) - 15 = y";
   1.502 +test "(i + j + 12 + (k::nat)) - -15 = y";
   1.503 +test "(i + j + -12 + (k::nat)) - -15 = y";
   1.504 +
   1.505 +(*combine_numerals*)
   1.506 +test "k + 3*k = (u::nat)";
   1.507 +test "Suc (i + 3) = u";
   1.508 +test "Suc (i + j + 3 + k) = u";
   1.509 +test "k + j + 3*k + j = (u::nat)";
   1.510 +test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
   1.511 +test "(2*n*m) + (3*(m*n)) = (u::nat)";
   1.512 +(*negative numerals: FAIL*)
   1.513 +test "Suc (i + j + -3 + k) = u";
   1.514 +
   1.515 +(*cancel_numeral_factors*)
   1.516 +test "9*x = 12 * (y::nat)";
   1.517 +test "(9*x) div (12 * (y::nat)) = z";
   1.518 +test "9*x < 12 * (y::nat)";
   1.519 +test "9*x <= 12 * (y::nat)";
   1.520 +
   1.521 +(*cancel_factor*)
   1.522 +test "x*k = k*(y::nat)";
   1.523 +test "k = k*(y::nat)";
   1.524 +test "a*(b*c) = (b::nat)";
   1.525 +test "a*(b*c) = d*(b::nat)*(x*a)";
   1.526 +
   1.527 +test "x*k < k*(y::nat)";
   1.528 +test "k < k*(y::nat)";
   1.529 +test "a*(b*c) < (b::nat)";
   1.530 +test "a*(b*c) < d*(b::nat)*(x*a)";
   1.531 +
   1.532 +test "x*k <= k*(y::nat)";
   1.533 +test "k <= k*(y::nat)";
   1.534 +test "a*(b*c) <= (b::nat)";
   1.535 +test "a*(b*c) <= d*(b::nat)*(x*a)";
   1.536 +
   1.537 +test "(x*k) div (k*(y::nat)) = (uu::nat)";
   1.538 +test "(k) div (k*(y::nat)) = (uu::nat)";
   1.539 +test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
   1.540 +test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
   1.541 +*)