src/HOL/Integ/int_arith1.ML
changeset 9436 62bb04ab4b01
child 9544 f9202e219a29
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Jul 25 00:06:46 2000 +0200
     1.3 @@ -0,0 +1,467 @@
     1.4 +(*  Title:      HOL/Integ/int_arith1.ML
     1.5 +    ID:         $Id$
     1.6 +    Authors:    Larry Paulson and Tobias Nipkow
     1.7 +
     1.8 +Simprocs and decision procedure for linear arithmetic.
     1.9 +*)
    1.10 +
    1.11 +(*** Simprocs for numeric literals ***)
    1.12 +
    1.13 +(** Combining of literal coefficients in sums of products **)
    1.14 +
    1.15 +Goal "(x < y) = (x-y < (#0::int))";
    1.16 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.17 +qed "zless_iff_zdiff_zless_0";
    1.18 +
    1.19 +Goal "(x = y) = (x-y = (#0::int))";
    1.20 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.21 +qed "eq_iff_zdiff_eq_0";
    1.22 +
    1.23 +Goal "(x <= y) = (x-y <= (#0::int))";
    1.24 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.25 +qed "zle_iff_zdiff_zle_0";
    1.26 +
    1.27 +
    1.28 +(** For combine_numerals **)
    1.29 +
    1.30 +Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
    1.31 +by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
    1.32 +qed "left_zadd_zmult_distrib";
    1.33 +
    1.34 +
    1.35 +(** For cancel_numerals **)
    1.36 +
    1.37 +val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
    1.38 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    1.39 +			   zle_iff_zdiff_zle_0] @
    1.40 +		        map (inst "y" "n")
    1.41 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    1.42 +			   zle_iff_zdiff_zle_0];
    1.43 +
    1.44 +Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    1.45 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.46 +		                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.47 +qed "eq_add_iff1";
    1.48 +
    1.49 +Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    1.50 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.51 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.52 +qed "eq_add_iff2";
    1.53 +
    1.54 +Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
    1.55 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.56 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.57 +qed "less_add_iff1";
    1.58 +
    1.59 +Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
    1.60 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.61 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.62 +qed "less_add_iff2";
    1.63 +
    1.64 +Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
    1.65 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.66 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.67 +qed "le_add_iff1";
    1.68 +
    1.69 +Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
    1.70 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
    1.71 +                                     @zadd_ac@rel_iff_rel_0_rls) 1);
    1.72 +qed "le_add_iff2";
    1.73 +
    1.74 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
    1.75 +Goal "u = u' ==> (t==u) == (t==u')";
    1.76 +by Auto_tac;
    1.77 +qed "eq_cong2";
    1.78 +
    1.79 +
    1.80 +structure Int_Numeral_Simprocs =
    1.81 +struct
    1.82 +
    1.83 +(*Utilities*)
    1.84 +
    1.85 +fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
    1.86 +                   NumeralSyntax.mk_bin n;
    1.87 +
    1.88 +(*Decodes a binary INTEGER*)
    1.89 +fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
    1.90 +     (NumeralSyntax.dest_bin w
    1.91 +      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    1.92 +  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    1.93 +
    1.94 +fun find_first_numeral past (t::terms) =
    1.95 +	((dest_numeral t, rev past @ terms)
    1.96 +	 handle TERM _ => find_first_numeral (t::past) terms)
    1.97 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    1.98 +
    1.99 +val zero = mk_numeral 0;
   1.100 +val mk_plus = HOLogic.mk_binop "op +";
   1.101 +
   1.102 +val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
   1.103 +
   1.104 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   1.105 +fun mk_sum []        = zero
   1.106 +  | mk_sum [t,u]     = mk_plus (t, u)
   1.107 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.108 +
   1.109 +(*this version ALWAYS includes a trailing zero*)
   1.110 +fun long_mk_sum []        = zero
   1.111 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.112 +
   1.113 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
   1.114 +
   1.115 +(*decompose additions AND subtractions as a sum*)
   1.116 +fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
   1.117 +        dest_summing (pos, t, dest_summing (pos, u, ts))
   1.118 +  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
   1.119 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
   1.120 +  | dest_summing (pos, t, ts) =
   1.121 +	if pos then t::ts else uminus_const$t :: ts;
   1.122 +
   1.123 +fun dest_sum t = dest_summing (true, t, []);
   1.124 +
   1.125 +val mk_diff = HOLogic.mk_binop "op -";
   1.126 +val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT;
   1.127 +
   1.128 +val one = mk_numeral 1;
   1.129 +val mk_times = HOLogic.mk_binop "op *";
   1.130 +
   1.131 +fun mk_prod [] = one
   1.132 +  | mk_prod [t] = t
   1.133 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
   1.134 +                        else mk_times (t, mk_prod ts);
   1.135 +
   1.136 +val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
   1.137 +
   1.138 +fun dest_prod t =
   1.139 +      let val (t,u) = dest_times t 
   1.140 +      in  dest_prod t @ dest_prod u  end
   1.141 +      handle TERM _ => [t];
   1.142 +
   1.143 +(*DON'T do the obvious simplifications; that would create special cases*) 
   1.144 +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
   1.145 +
   1.146 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   1.147 +fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
   1.148 +  | dest_coeff sign t =
   1.149 +    let val ts = sort Term.term_ord (dest_prod t)
   1.150 +	val (n, ts') = find_first_numeral [] ts
   1.151 +                          handle TERM _ => (1, ts)
   1.152 +    in (sign*n, mk_prod ts') end;
   1.153 +
   1.154 +(*Find first coefficient-term THAT MATCHES u*)
   1.155 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
   1.156 +  | find_first_coeff past u (t::terms) =
   1.157 +	let val (n,u') = dest_coeff 1 t
   1.158 +	in  if u aconv u' then (n, rev past @ terms)
   1.159 +			  else find_first_coeff (t::past) u terms
   1.160 +	end
   1.161 +	handle TERM _ => find_first_coeff (t::past) u terms;
   1.162 +
   1.163 +
   1.164 +(*Simplify #1*n and n*#1 to n*)
   1.165 +val add_0s = [zadd_0, zadd_0_right];
   1.166 +val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
   1.167 +
   1.168 +(*To perform binary arithmetic*)
   1.169 +val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
   1.170 +
   1.171 +(*To evaluate binary negations of coefficients*)
   1.172 +val zminus_simps = NCons_simps @
   1.173 +                   [number_of_minus RS sym, 
   1.174 +		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   1.175 +		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   1.176 +
   1.177 +(*To let us treat subtraction as addition*)
   1.178 +val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
   1.179 +
   1.180 +(*Apply the given rewrite (if present) just once*)
   1.181 +fun trans_tac None      = all_tac
   1.182 +  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
   1.183 +
   1.184 +fun prove_conv name tacs sg (t, u) =
   1.185 +  if t aconv u then None
   1.186 +  else
   1.187 +  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
   1.188 +  in Some
   1.189 +     (prove_goalw_cterm [] ct (K tacs)
   1.190 +      handle ERROR => error 
   1.191 +	  ("The error(s) above occurred while trying to prove " ^
   1.192 +	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   1.193 +  end;
   1.194 +
   1.195 +fun simplify_meta_eq rules =
   1.196 +    mk_meta_eq o
   1.197 +    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
   1.198 +
   1.199 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.200 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT);
   1.201 +val prep_pats = map prep_pat;
   1.202 +
   1.203 +structure CancelNumeralsCommon =
   1.204 +  struct
   1.205 +  val mk_sum    	= mk_sum
   1.206 +  val dest_sum		= dest_sum
   1.207 +  val mk_coeff		= mk_coeff
   1.208 +  val dest_coeff	= dest_coeff 1
   1.209 +  val find_first_coeff	= find_first_coeff []
   1.210 +  val trans_tac         = trans_tac
   1.211 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.212 +                                                     zminus_simps@zadd_ac))
   1.213 +                 THEN ALLGOALS
   1.214 +                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
   1.215 +                                               bin_simps@zadd_ac@zmult_ac))
   1.216 +  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.217 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   1.218 +  end;
   1.219 +
   1.220 +
   1.221 +structure EqCancelNumerals = CancelNumeralsFun
   1.222 + (open CancelNumeralsCommon
   1.223 +  val prove_conv = prove_conv "inteq_cancel_numerals"
   1.224 +  val mk_bal   = HOLogic.mk_eq
   1.225 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   1.226 +  val bal_add1 = eq_add_iff1 RS trans
   1.227 +  val bal_add2 = eq_add_iff2 RS trans
   1.228 +);
   1.229 +
   1.230 +structure LessCancelNumerals = CancelNumeralsFun
   1.231 + (open CancelNumeralsCommon
   1.232 +  val prove_conv = prove_conv "intless_cancel_numerals"
   1.233 +  val mk_bal   = HOLogic.mk_binrel "op <"
   1.234 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
   1.235 +  val bal_add1 = less_add_iff1 RS trans
   1.236 +  val bal_add2 = less_add_iff2 RS trans
   1.237 +);
   1.238 +
   1.239 +structure LeCancelNumerals = CancelNumeralsFun
   1.240 + (open CancelNumeralsCommon
   1.241 +  val prove_conv = prove_conv "intle_cancel_numerals"
   1.242 +  val mk_bal   = HOLogic.mk_binrel "op <="
   1.243 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
   1.244 +  val bal_add1 = le_add_iff1 RS trans
   1.245 +  val bal_add2 = le_add_iff2 RS trans
   1.246 +);
   1.247 +
   1.248 +val cancel_numerals = 
   1.249 +  map prep_simproc
   1.250 +   [("inteq_cancel_numerals",
   1.251 +     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
   1.252 +		"(l::int) - m = n", "(l::int) = m - n", 
   1.253 +		"(l::int) * m = n", "(l::int) = m * n"], 
   1.254 +     EqCancelNumerals.proc),
   1.255 +    ("intless_cancel_numerals", 
   1.256 +     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
   1.257 +		"(l::int) - m < n", "(l::int) < m - n", 
   1.258 +		"(l::int) * m < n", "(l::int) < m * n"], 
   1.259 +     LessCancelNumerals.proc),
   1.260 +    ("intle_cancel_numerals", 
   1.261 +     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
   1.262 +		"(l::int) - m <= n", "(l::int) <= m - n", 
   1.263 +		"(l::int) * m <= n", "(l::int) <= m * n"], 
   1.264 +     LeCancelNumerals.proc)];
   1.265 +
   1.266 +
   1.267 +structure CombineNumeralsData =
   1.268 +  struct
   1.269 +  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
   1.270 +  val dest_sum		= dest_sum
   1.271 +  val mk_coeff		= mk_coeff
   1.272 +  val dest_coeff	= dest_coeff 1
   1.273 +  val left_distrib	= left_zadd_zmult_distrib RS trans
   1.274 +  val prove_conv	= prove_conv "int_combine_numerals"
   1.275 +  val trans_tac          = trans_tac
   1.276 +  val norm_tac = ALLGOALS
   1.277 +                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   1.278 +                                              zminus_simps@zadd_ac))
   1.279 +                 THEN ALLGOALS
   1.280 +                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
   1.281 +                                               bin_simps@zadd_ac@zmult_ac))
   1.282 +  val numeral_simp_tac	= ALLGOALS 
   1.283 +                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   1.284 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   1.285 +  end;
   1.286 +
   1.287 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.288 +  
   1.289 +val combine_numerals = 
   1.290 +    prep_simproc ("int_combine_numerals",
   1.291 +		  prep_pats ["(i::int) + j", "(i::int) - j"],
   1.292 +		  CombineNumerals.proc);
   1.293 +
   1.294 +end;
   1.295 +
   1.296 +Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   1.297 +Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   1.298 +
   1.299 +(*The Abel_Cancel simprocs are now obsolete*)
   1.300 +Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
   1.301 +
   1.302 +(*examples:
   1.303 +print_depth 22;
   1.304 +set timing;
   1.305 +set trace_simp;
   1.306 +fun test s = (Goal s; by (Simp_tac 1)); 
   1.307 +
   1.308 +test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
   1.309 +
   1.310 +test "#2*u = (u::int)";
   1.311 +test "(i + j + #12 + (k::int)) - #15 = y";
   1.312 +test "(i + j + #12 + (k::int)) - #5 = y";
   1.313 +
   1.314 +test "y - b < (b::int)";
   1.315 +test "y - (#3*b + c) < (b::int) - #2*c";
   1.316 +
   1.317 +test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
   1.318 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
   1.319 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
   1.320 +test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
   1.321 +
   1.322 +test "(i + j + #12 + (k::int)) = u + #15 + y";
   1.323 +test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
   1.324 +
   1.325 +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)";
   1.326 +
   1.327 +test "a + -(b+c) + b = (d::int)";
   1.328 +test "a + -(b+c) - b = (d::int)";
   1.329 +
   1.330 +(*negative numerals*)
   1.331 +test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
   1.332 +test "(i + j + #-3 + (k::int)) < u + #5 + y";
   1.333 +test "(i + j + #3 + (k::int)) < u + #-6 + y";
   1.334 +test "(i + j + #-12 + (k::int)) - #15 = y";
   1.335 +test "(i + j + #12 + (k::int)) - #-15 = y";
   1.336 +test "(i + j + #-12 + (k::int)) - #-15 = y";
   1.337 +*)
   1.338 +
   1.339 +
   1.340 +(** Constant folding for integer plus and times **)
   1.341 +
   1.342 +(*We do not need
   1.343 +    structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
   1.344 +    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
   1.345 +  because combine_numerals does the same thing*)
   1.346 +
   1.347 +structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.348 +struct
   1.349 +  val ss		= HOL_ss
   1.350 +  val eq_reflection	= eq_reflection
   1.351 +  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
   1.352 +  val T	     = HOLogic.intT
   1.353 +  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
   1.354 +  val add_ac = zmult_ac
   1.355 +end;
   1.356 +
   1.357 +structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
   1.358 +
   1.359 +Addsimprocs [Int_Times_Assoc.conv];
   1.360 +
   1.361 +
   1.362 +(** The same for the naturals **)
   1.363 +
   1.364 +structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
   1.365 +struct
   1.366 +  val ss		= HOL_ss
   1.367 +  val eq_reflection	= eq_reflection
   1.368 +  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
   1.369 +  val T	     = HOLogic.natT
   1.370 +  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
   1.371 +  val add_ac = mult_ac
   1.372 +end;
   1.373 +
   1.374 +structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
   1.375 +
   1.376 +Addsimprocs [Nat_Times_Assoc.conv];
   1.377 +
   1.378 +
   1.379 +(*** decision procedure for linear arithmetic ***)
   1.380 +
   1.381 +(*---------------------------------------------------------------------------*)
   1.382 +(* Linear arithmetic                                                         *)
   1.383 +(*---------------------------------------------------------------------------*)
   1.384 +
   1.385 +(*
   1.386 +Instantiation of the generic linear arithmetic package for int.
   1.387 +*)
   1.388 +
   1.389 +(* Update parameters of arithmetic prover *)
   1.390 +local
   1.391 +
   1.392 +(* reduce contradictory <= to False *)
   1.393 +val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
   1.394 +                [int_0, zadd_0, zadd_0_right, zdiff_def,
   1.395 +		 zadd_zminus_inverse, zadd_zminus_inverse2, 
   1.396 +		 zmult_0, zmult_0_right, 
   1.397 +		 zmult_1, zmult_1_right, 
   1.398 +		 zmult_minus1, zmult_minus1_right,
   1.399 +		 zminus_zadd_distrib, zminus_zminus];
   1.400 +
   1.401 +val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
   1.402 +               Int_Numeral_Simprocs.cancel_numerals;
   1.403 +
   1.404 +val add_mono_thms_int =
   1.405 +  map (fn s => prove_goal (the_context ()) s
   1.406 +                 (fn prems => [cut_facts_tac prems 1,
   1.407 +                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
   1.408 +    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
   1.409 +     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
   1.410 +     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
   1.411 +     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
   1.412 +    ];
   1.413 +
   1.414 +in
   1.415 +
   1.416 +val int_arith_setup =
   1.417 + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
   1.418 +   {add_mono_thms = add_mono_thms @ add_mono_thms_int,
   1.419 +    lessD = lessD @ [add1_zle_eq RS iffD2],
   1.420 +    simpset = simpset addsimps add_rules
   1.421 +                      addsimprocs simprocs
   1.422 +                      addcongs [if_weak_cong]}),
   1.423 +  arith_discrete ("IntDef.int", true)];
   1.424 +
   1.425 +end;
   1.426 +
   1.427 +let
   1.428 +val int_arith_simproc_pats =
   1.429 +  map (fn s => Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.boolT))
   1.430 +      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
   1.431 +
   1.432 +val fast_int_arith_simproc = mk_simproc
   1.433 +  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
   1.434 +in
   1.435 +Addsimprocs [fast_int_arith_simproc]
   1.436 +end;
   1.437 +
   1.438 +(* Some test data
   1.439 +Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   1.440 +by (fast_arith_tac 1);
   1.441 +Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
   1.442 +by (fast_arith_tac 1);
   1.443 +Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
   1.444 +by (fast_arith_tac 1);
   1.445 +Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
   1.446 +by (fast_arith_tac 1);
   1.447 +Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
   1.448 +\     ==> a+a <= j+j";
   1.449 +by (fast_arith_tac 1);
   1.450 +Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
   1.451 +\     ==> a+a - - #-1 < j+j - #3";
   1.452 +by (fast_arith_tac 1);
   1.453 +Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   1.454 +by (arith_tac 1);
   1.455 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.456 +\     ==> a <= l";
   1.457 +by (fast_arith_tac 1);
   1.458 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.459 +\     ==> a+a+a+a <= l+l+l+l";
   1.460 +by (fast_arith_tac 1);
   1.461 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.462 +\     ==> a+a+a+a+a <= l+l+l+l+i";
   1.463 +by (fast_arith_tac 1);
   1.464 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.465 +\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   1.466 +by (fast_arith_tac 1);
   1.467 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   1.468 +\     ==> #6*a <= #5*l+i";
   1.469 +by (fast_arith_tac 1);
   1.470 +*)