rearranged setup of arithmetic procedures, avoiding global reference values;
authorwenzelm
Tue Jul 25 00:06:46 2000 +0200 (2000-07-25)
changeset 943662bb04ab4b01
parent 9435 c3a13a7d4424
child 9437 93e91040c286
rearranged setup of arithmetic procedures, avoiding global reference values;
src/HOL/Arith.ML
src/HOL/Arith.thy
src/HOL/Integ/Bin.ML
src/HOL/Integ/Int.ML
src/HOL/Integ/IntArith.ML
src/HOL/Integ/IntArith.thy
src/HOL/Integ/NatSimprocs.ML
src/HOL/Integ/NatSimprocs.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/int_arith2.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/IsaMakefile
src/HOL/Nat.ML
src/HOL/Nat.thy
src/HOL/Real/RealArith.ML
src/HOL/Real/RealArith.thy
src/HOL/Real/real_arith.ML
src/HOL/Univ.thy
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Arith.ML	Tue Jul 25 00:03:39 2000 +0200
     1.2 +++ b/src/HOL/Arith.ML	Tue Jul 25 00:06:46 2000 +0200
     1.3 @@ -3,1030 +3,13 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -Proofs about elementary arithmetic: addition, multiplication, etc.
     1.8 -Some from the Hoare example from Norbert Galm
     1.9 +Further proofs about elementary arithmetic, using the arithmetic proof
    1.10 +procedures.
    1.11  *)
    1.12  
    1.13 -(*** Basic rewrite rules for the arithmetic operators ***)
    1.14 -
    1.15 -
    1.16 -(** Difference **)
    1.17 -
    1.18 -Goal "0 - n = (0::nat)";
    1.19 -by (induct_tac "n" 1);
    1.20 -by (ALLGOALS Asm_simp_tac);
    1.21 -qed "diff_0_eq_0";
    1.22 -
    1.23 -(*Must simplify BEFORE the induction!  (Else we get a critical pair)
    1.24 -  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
    1.25 -Goal "Suc(m) - Suc(n) = m - n";
    1.26 -by (Simp_tac 1);
    1.27 -by (induct_tac "n" 1);
    1.28 -by (ALLGOALS Asm_simp_tac);
    1.29 -qed "diff_Suc_Suc";
    1.30 -
    1.31 -Addsimps [diff_0_eq_0, diff_Suc_Suc];
    1.32 -
    1.33 -(* Could be (and is, below) generalized in various ways;
    1.34 -   However, none of the generalizations are currently in the simpset,
    1.35 -   and I dread to think what happens if I put them in *)
    1.36 -Goal "0 < n ==> Suc(n-1) = n";
    1.37 -by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
    1.38 -qed "Suc_pred";
    1.39 -Addsimps [Suc_pred];
    1.40 -
    1.41 -Delsimps [diff_Suc];
    1.42 -
    1.43 -
    1.44 -(**** Inductive properties of the operators ****)
    1.45 -
    1.46 -(*** Addition ***)
    1.47 -
    1.48 -Goal "m + 0 = (m::nat)";
    1.49 -by (induct_tac "m" 1);
    1.50 -by (ALLGOALS Asm_simp_tac);
    1.51 -qed "add_0_right";
    1.52 -
    1.53 -Goal "m + Suc(n) = Suc(m+n)";
    1.54 -by (induct_tac "m" 1);
    1.55 -by (ALLGOALS Asm_simp_tac);
    1.56 -qed "add_Suc_right";
    1.57 -
    1.58 -Addsimps [add_0_right,add_Suc_right];
    1.59 -
    1.60 -
    1.61 -(*Associative law for addition*)
    1.62 -Goal "(m + n) + k = m + ((n + k)::nat)";
    1.63 -by (induct_tac "m" 1);
    1.64 -by (ALLGOALS Asm_simp_tac);
    1.65 -qed "add_assoc";
    1.66 -
    1.67 -(*Commutative law for addition*)  
    1.68 -Goal "m + n = n + (m::nat)";
    1.69 -by (induct_tac "m" 1);
    1.70 -by (ALLGOALS Asm_simp_tac);
    1.71 -qed "add_commute";
    1.72 -
    1.73 -Goal "x+(y+z)=y+((x+z)::nat)";
    1.74 -by (rtac (add_commute RS trans) 1);
    1.75 -by (rtac (add_assoc RS trans) 1);
    1.76 -by (rtac (add_commute RS arg_cong) 1);
    1.77 -qed "add_left_commute";
    1.78 -
    1.79 -(*Addition is an AC-operator*)
    1.80 -bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
    1.81 -
    1.82 -Goal "(k + m = k + n) = (m=(n::nat))";
    1.83 -by (induct_tac "k" 1);
    1.84 -by (Simp_tac 1);
    1.85 -by (Asm_simp_tac 1);
    1.86 -qed "add_left_cancel";
    1.87 -
    1.88 -Goal "(m + k = n + k) = (m=(n::nat))";
    1.89 -by (induct_tac "k" 1);
    1.90 -by (Simp_tac 1);
    1.91 -by (Asm_simp_tac 1);
    1.92 -qed "add_right_cancel";
    1.93 -
    1.94 -Goal "(k + m <= k + n) = (m<=(n::nat))";
    1.95 -by (induct_tac "k" 1);
    1.96 -by (Simp_tac 1);
    1.97 -by (Asm_simp_tac 1);
    1.98 -qed "add_left_cancel_le";
    1.99 -
   1.100 -Goal "(k + m < k + n) = (m<(n::nat))";
   1.101 -by (induct_tac "k" 1);
   1.102 -by (Simp_tac 1);
   1.103 -by (Asm_simp_tac 1);
   1.104 -qed "add_left_cancel_less";
   1.105 -
   1.106 -Addsimps [add_left_cancel, add_right_cancel,
   1.107 -          add_left_cancel_le, add_left_cancel_less];
   1.108 -
   1.109 -(** Reasoning about m+0=0, etc. **)
   1.110 -
   1.111 -Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
   1.112 -by (case_tac "m" 1);
   1.113 -by (Auto_tac);
   1.114 -qed "add_is_0";
   1.115 -AddIffs [add_is_0];
   1.116 -
   1.117 -Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
   1.118 -by (case_tac "m" 1);
   1.119 -by (Auto_tac);
   1.120 -qed "zero_is_add";
   1.121 -AddIffs [zero_is_add];
   1.122 -
   1.123 -Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
   1.124 -by (case_tac "m" 1);
   1.125 -by (Auto_tac);
   1.126 -qed "add_is_1";
   1.127 -
   1.128 -Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
   1.129 -by (case_tac "m" 1);
   1.130 -by (Auto_tac);
   1.131 -qed "one_is_add";
   1.132 -
   1.133 -Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
   1.134 -by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
   1.135 -qed "add_gr_0";
   1.136 -AddIffs [add_gr_0];
   1.137 -
   1.138 -(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
   1.139 -Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
   1.140 -by (case_tac "m" 1);
   1.141 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
   1.142 -                                      addsplits [nat.split])));
   1.143 -qed "add_pred";
   1.144 -Addsimps [add_pred];
   1.145 -
   1.146 -Goal "!!m::nat. m + n = m ==> n = 0";
   1.147 -by (dtac (add_0_right RS ssubst) 1);
   1.148 -by (asm_full_simp_tac (simpset() addsimps [add_assoc]
   1.149 -                                 delsimps [add_0_right]) 1);
   1.150 -qed "add_eq_self_zero";
   1.151 -
   1.152 -
   1.153 -(**** Additional theorems about "less than" ****)
   1.154 -
   1.155 -(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
   1.156 -Goal "m<n --> (EX k. n=Suc(m+k))";
   1.157 -by (induct_tac "n" 1);
   1.158 -by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
   1.159 -by (blast_tac (claset() addSEs [less_SucE] 
   1.160 -                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
   1.161 -qed_spec_mp "less_eq_Suc_add";
   1.162 -
   1.163 -Goal "n <= ((m + n)::nat)";
   1.164 -by (induct_tac "m" 1);
   1.165 -by (ALLGOALS Simp_tac);
   1.166 -by (etac le_SucI 1);
   1.167 -qed "le_add2";
   1.168 -
   1.169 -Goal "n <= ((n + m)::nat)";
   1.170 -by (simp_tac (simpset() addsimps add_ac) 1);
   1.171 -by (rtac le_add2 1);
   1.172 -qed "le_add1";
   1.173 -
   1.174 -bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
   1.175 -bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
   1.176 -
   1.177 -Goal "(m<n) = (EX k. n=Suc(m+k))";
   1.178 -by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
   1.179 -qed "less_iff_Suc_add";
   1.180 -
   1.181 -
   1.182 -(*"i <= j ==> i <= j+m"*)
   1.183 -bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
   1.184 -
   1.185 -(*"i <= j ==> i <= m+j"*)
   1.186 -bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
   1.187 -
   1.188 -(*"i < j ==> i < j+m"*)
   1.189 -bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
   1.190 -
   1.191 -(*"i < j ==> i < m+j"*)
   1.192 -bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
   1.193 -
   1.194 -Goal "i+j < (k::nat) --> i<k";
   1.195 -by (induct_tac "j" 1);
   1.196 -by (ALLGOALS Asm_simp_tac);
   1.197 -by (blast_tac (claset() addDs [Suc_lessD]) 1);
   1.198 -qed_spec_mp "add_lessD1";
   1.199 -
   1.200 -Goal "~ (i+j < (i::nat))";
   1.201 -by (rtac notI 1);
   1.202 -by (etac (add_lessD1 RS less_irrefl) 1);
   1.203 -qed "not_add_less1";
   1.204 -
   1.205 -Goal "~ (j+i < (i::nat))";
   1.206 -by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
   1.207 -qed "not_add_less2";
   1.208 -AddIffs [not_add_less1, not_add_less2];
   1.209 -
   1.210 -Goal "m+k<=n --> m<=(n::nat)";
   1.211 -by (induct_tac "k" 1);
   1.212 -by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
   1.213 -qed_spec_mp "add_leD1";
   1.214 -
   1.215 -Goal "m+k<=n ==> k<=(n::nat)";
   1.216 -by (full_simp_tac (simpset() addsimps [add_commute]) 1);
   1.217 -by (etac add_leD1 1);
   1.218 -qed_spec_mp "add_leD2";
   1.219 -
   1.220 -Goal "m+k<=n ==> m<=n & k<=(n::nat)";
   1.221 -by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
   1.222 -bind_thm ("add_leE", result() RS conjE);
   1.223 -
   1.224 -(*needs !!k for add_ac to work*)
   1.225 -Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
   1.226 -by (force_tac (claset(),
   1.227 -	      simpset() delsimps [add_Suc_right]
   1.228 -	                addsimps [less_iff_Suc_add,
   1.229 -				  add_Suc_right RS sym] @ add_ac) 1);
   1.230 -qed "less_add_eq_less";
   1.231 -
   1.232 -
   1.233 -(*** Monotonicity of Addition ***)
   1.234 -
   1.235 -(*strict, in 1st argument*)
   1.236 -Goal "i < j ==> i + k < j + (k::nat)";
   1.237 -by (induct_tac "k" 1);
   1.238 -by (ALLGOALS Asm_simp_tac);
   1.239 -qed "add_less_mono1";
   1.240 -
   1.241 -(*strict, in both arguments*)
   1.242 -Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
   1.243 -by (rtac (add_less_mono1 RS less_trans) 1);
   1.244 -by (REPEAT (assume_tac 1));
   1.245 -by (induct_tac "j" 1);
   1.246 -by (ALLGOALS Asm_simp_tac);
   1.247 -qed "add_less_mono";
   1.248 -
   1.249 -(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
   1.250 -val [lt_mono,le] = Goal
   1.251 -     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
   1.252 -\        i <= j                                 \
   1.253 -\     |] ==> f(i) <= (f(j)::nat)";
   1.254 -by (cut_facts_tac [le] 1);
   1.255 -by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
   1.256 -by (blast_tac (claset() addSIs [lt_mono]) 1);
   1.257 -qed "less_mono_imp_le_mono";
   1.258 -
   1.259 -(*non-strict, in 1st argument*)
   1.260 -Goal "i<=j ==> i + k <= j + (k::nat)";
   1.261 -by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
   1.262 -by (etac add_less_mono1 1);
   1.263 -by (assume_tac 1);
   1.264 -qed "add_le_mono1";
   1.265 -
   1.266 -(*non-strict, in both arguments*)
   1.267 -Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
   1.268 -by (etac (add_le_mono1 RS le_trans) 1);
   1.269 -by (simp_tac (simpset() addsimps [add_commute]) 1);
   1.270 -qed "add_le_mono";
   1.271 -
   1.272 -
   1.273 -(*** Multiplication ***)
   1.274 -
   1.275 -(*right annihilation in product*)
   1.276 -Goal "!!m::nat. m * 0 = 0";
   1.277 -by (induct_tac "m" 1);
   1.278 -by (ALLGOALS Asm_simp_tac);
   1.279 -qed "mult_0_right";
   1.280 -
   1.281 -(*right successor law for multiplication*)
   1.282 -Goal  "m * Suc(n) = m + (m * n)";
   1.283 -by (induct_tac "m" 1);
   1.284 -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
   1.285 -qed "mult_Suc_right";
   1.286 -
   1.287 -Addsimps [mult_0_right, mult_Suc_right];
   1.288 -
   1.289 -Goal "1 * n = n";
   1.290 -by (Asm_simp_tac 1);
   1.291 -qed "mult_1";
   1.292 -
   1.293 -Goal "n * 1 = n";
   1.294 -by (Asm_simp_tac 1);
   1.295 -qed "mult_1_right";
   1.296 -
   1.297 -(*Commutative law for multiplication*)
   1.298 -Goal "m * n = n * (m::nat)";
   1.299 -by (induct_tac "m" 1);
   1.300 -by (ALLGOALS Asm_simp_tac);
   1.301 -qed "mult_commute";
   1.302 -
   1.303 -(*addition distributes over multiplication*)
   1.304 -Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
   1.305 -by (induct_tac "m" 1);
   1.306 -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
   1.307 -qed "add_mult_distrib";
   1.308 -
   1.309 -Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
   1.310 -by (induct_tac "m" 1);
   1.311 -by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
   1.312 -qed "add_mult_distrib2";
   1.313 -
   1.314 -(*Associative law for multiplication*)
   1.315 -Goal "(m * n) * k = m * ((n * k)::nat)";
   1.316 -by (induct_tac "m" 1);
   1.317 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
   1.318 -qed "mult_assoc";
   1.319 -
   1.320 -Goal "x*(y*z) = y*((x*z)::nat)";
   1.321 -by (rtac trans 1);
   1.322 -by (rtac mult_commute 1);
   1.323 -by (rtac trans 1);
   1.324 -by (rtac mult_assoc 1);
   1.325 -by (rtac (mult_commute RS arg_cong) 1);
   1.326 -qed "mult_left_commute";
   1.327 -
   1.328 -bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
   1.329 -
   1.330 -Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
   1.331 -by (induct_tac "m" 1);
   1.332 -by (induct_tac "n" 2);
   1.333 -by (ALLGOALS Asm_simp_tac);
   1.334 -qed "mult_is_0";
   1.335 -
   1.336 -Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
   1.337 -by (stac eq_commute 1 THEN stac mult_is_0 1);
   1.338 -by Auto_tac;
   1.339 -qed "zero_is_mult";
   1.340 -
   1.341 -Addsimps [mult_is_0, zero_is_mult];
   1.342 -
   1.343 -
   1.344 -(*** Difference ***)
   1.345 -
   1.346 -Goal "!!m::nat. m - m = 0";
   1.347 -by (induct_tac "m" 1);
   1.348 -by (ALLGOALS Asm_simp_tac);
   1.349 -qed "diff_self_eq_0";
   1.350 -
   1.351 -Addsimps [diff_self_eq_0];
   1.352 -
   1.353 -(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   1.354 -Goal "~ m<n --> n+(m-n) = (m::nat)";
   1.355 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.356 -by (ALLGOALS Asm_simp_tac);
   1.357 -qed_spec_mp "add_diff_inverse";
   1.358 -
   1.359 -Goal "n<=m ==> n+(m-n) = (m::nat)";
   1.360 -by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
   1.361 -qed "le_add_diff_inverse";
   1.362 -
   1.363 -Goal "n<=m ==> (m-n)+n = (m::nat)";
   1.364 -by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
   1.365 -qed "le_add_diff_inverse2";
   1.366 -
   1.367 -Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
   1.368 -
   1.369 -
   1.370 -(*** More results about difference ***)
   1.371 -
   1.372 -Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
   1.373 -by (etac rev_mp 1);
   1.374 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.375 -by (ALLGOALS Asm_simp_tac);
   1.376 -qed "Suc_diff_le";
   1.377 -
   1.378 -Goal "m - n < Suc(m)";
   1.379 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.380 -by (etac less_SucE 3);
   1.381 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
   1.382 -qed "diff_less_Suc";
   1.383 -
   1.384 -Goal "m - n <= (m::nat)";
   1.385 -by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
   1.386 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
   1.387 -qed "diff_le_self";
   1.388 -Addsimps [diff_le_self];
   1.389 -
   1.390 -(* j<k ==> j-n < k *)
   1.391 -bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
   1.392 -
   1.393 -Goal "!!i::nat. i-j-k = i - (j+k)";
   1.394 -by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
   1.395 -by (ALLGOALS Asm_simp_tac);
   1.396 -qed "diff_diff_left";
   1.397 -
   1.398 -Goal "(Suc m - n) - Suc k = m - n - k";
   1.399 -by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
   1.400 -qed "Suc_diff_diff";
   1.401 -Addsimps [Suc_diff_diff];
   1.402 -
   1.403 -Goal "0<n ==> n - Suc i < n";
   1.404 -by (case_tac "n" 1);
   1.405 -by Safe_tac;
   1.406 -by (asm_simp_tac (simpset() addsimps le_simps) 1);
   1.407 -qed "diff_Suc_less";
   1.408 -Addsimps [diff_Suc_less];
   1.409 -
   1.410 -(*This and the next few suggested by Florian Kammueller*)
   1.411 -Goal "!!i::nat. i-j-k = i-k-j";
   1.412 -by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
   1.413 -qed "diff_commute";
   1.414 -
   1.415 -Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
   1.416 -by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
   1.417 -by (ALLGOALS Asm_simp_tac);
   1.418 -qed_spec_mp "diff_add_assoc";
   1.419 -
   1.420 -Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
   1.421 -by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
   1.422 -qed_spec_mp "diff_add_assoc2";
   1.423 -
   1.424 -Goal "(n+m) - n = (m::nat)";
   1.425 -by (induct_tac "n" 1);
   1.426 -by (ALLGOALS Asm_simp_tac);
   1.427 -qed "diff_add_inverse";
   1.428 -
   1.429 -Goal "(m+n) - n = (m::nat)";
   1.430 -by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
   1.431 -qed "diff_add_inverse2";
   1.432 -
   1.433 -Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
   1.434 -by Safe_tac;
   1.435 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
   1.436 -qed "le_imp_diff_is_add";
   1.437 -
   1.438 -Goal "!!m::nat. (m-n = 0) = (m <= n)";
   1.439 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.440 -by (ALLGOALS Asm_simp_tac);
   1.441 -qed "diff_is_0_eq";
   1.442 -
   1.443 -Goal "!!m::nat. (0 = m-n) = (m <= n)";
   1.444 -by (stac (diff_is_0_eq RS sym) 1);
   1.445 -by (rtac eq_sym_conv 1);
   1.446 -qed "zero_is_diff_eq";
   1.447 -Addsimps [diff_is_0_eq, zero_is_diff_eq];
   1.448 -
   1.449 -Goal "!!m::nat. (0<n-m) = (m<n)";
   1.450 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.451 -by (ALLGOALS Asm_simp_tac);
   1.452 -qed "zero_less_diff";
   1.453 -Addsimps [zero_less_diff];
   1.454 -
   1.455 -Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
   1.456 -by (res_inst_tac [("x","j - i")] exI 1);
   1.457 -by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
   1.458 -qed "less_imp_add_positive";
   1.459 -
   1.460 -Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
   1.461 -by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
   1.462 -by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
   1.463 -qed "zero_induct_lemma";
   1.464 -
   1.465 -val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
   1.466 -by (rtac (diff_self_eq_0 RS subst) 1);
   1.467 -by (rtac (zero_induct_lemma RS mp RS mp) 1);
   1.468 -by (REPEAT (ares_tac ([impI,allI]@prems) 1));
   1.469 -qed "zero_induct";
   1.470 -
   1.471 -Goal "(k+m) - (k+n) = m - (n::nat)";
   1.472 -by (induct_tac "k" 1);
   1.473 -by (ALLGOALS Asm_simp_tac);
   1.474 -qed "diff_cancel";
   1.475 -
   1.476 -Goal "(m+k) - (n+k) = m - (n::nat)";
   1.477 -by (asm_simp_tac
   1.478 -    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
   1.479 -qed "diff_cancel2";
   1.480 -
   1.481 -Goal "n - (n+m) = (0::nat)";
   1.482 -by (induct_tac "n" 1);
   1.483 -by (ALLGOALS Asm_simp_tac);
   1.484 -qed "diff_add_0";
   1.485 -
   1.486 -
   1.487 -(** Difference distributes over multiplication **)
   1.488 -
   1.489 -Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
   1.490 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   1.491 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
   1.492 -qed "diff_mult_distrib" ;
   1.493 -
   1.494 -Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
   1.495 -val mult_commute_k = read_instantiate [("m","k")] mult_commute;
   1.496 -by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
   1.497 -qed "diff_mult_distrib2" ;
   1.498 -(*NOT added as rewrites, since sometimes they are used from right-to-left*)
   1.499 -
   1.500 -
   1.501 -(*** Monotonicity of Multiplication ***)
   1.502 -
   1.503 -Goal "i <= (j::nat) ==> i*k<=j*k";
   1.504 -by (induct_tac "k" 1);
   1.505 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
   1.506 -qed "mult_le_mono1";
   1.507 -
   1.508 -Goal "i <= (j::nat) ==> k*i <= k*j";
   1.509 -by (dtac mult_le_mono1 1);
   1.510 -by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.511 -qed "mult_le_mono2";
   1.512 -
   1.513 -(* <= monotonicity, BOTH arguments*)
   1.514 -Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
   1.515 -by (etac (mult_le_mono1 RS le_trans) 1);
   1.516 -by (etac mult_le_mono2 1);
   1.517 -qed "mult_le_mono";
   1.518 +(*legacy ...*)
   1.519 +structure Arith = struct val thy = the_context () end;
   1.520  
   1.521 -(*strict, in 1st argument; proof is by induction on k>0*)
   1.522 -Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
   1.523 -by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
   1.524 -by (Asm_simp_tac 1);
   1.525 -by (induct_tac "x" 1);
   1.526 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
   1.527 -qed "mult_less_mono2";
   1.528 -
   1.529 -Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
   1.530 -by (dtac mult_less_mono2 1);
   1.531 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
   1.532 -qed "mult_less_mono1";
   1.533 -
   1.534 -Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
   1.535 -by (induct_tac "m" 1);
   1.536 -by (case_tac "n" 2);
   1.537 -by (ALLGOALS Asm_simp_tac);
   1.538 -qed "zero_less_mult_iff";
   1.539 -Addsimps [zero_less_mult_iff];
   1.540 -
   1.541 -Goal "(1 <= m*n) = (1<=m & 1<=n)";
   1.542 -by (induct_tac "m" 1);
   1.543 -by (case_tac "n" 2);
   1.544 -by (ALLGOALS Asm_simp_tac);
   1.545 -qed "one_le_mult_iff";
   1.546 -Addsimps [one_le_mult_iff];
   1.547 -
   1.548 -Goal "(m*n = 1) = (m=1 & n=1)";
   1.549 -by (induct_tac "m" 1);
   1.550 -by (Simp_tac 1);
   1.551 -by (induct_tac "n" 1);
   1.552 -by (Simp_tac 1);
   1.553 -by (fast_tac (claset() addss simpset()) 1);
   1.554 -qed "mult_eq_1_iff";
   1.555 -Addsimps [mult_eq_1_iff];
   1.556 -
   1.557 -Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
   1.558 -by (safe_tac (claset() addSIs [mult_less_mono1]));
   1.559 -by (cut_facts_tac [less_linear] 1);
   1.560 -by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
   1.561 -qed "mult_less_cancel2";
   1.562 -
   1.563 -Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
   1.564 -by (dtac mult_less_cancel2 1);
   1.565 -by (etac subst 1);
   1.566 -by (simp_tac (simpset() addsimps [mult_commute]) 1);
   1.567 -qed "mult_less_cancel1";
   1.568 -Addsimps [mult_less_cancel1, mult_less_cancel2];
   1.569 -
   1.570 -Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
   1.571 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
   1.572 -qed "mult_le_cancel2";
   1.573 -
   1.574 -Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
   1.575 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
   1.576 -qed "mult_le_cancel1";
   1.577 -Addsimps [mult_le_cancel1, mult_le_cancel2];
   1.578 -
   1.579 -Goal "(Suc k * m < Suc k * n) = (m < n)";
   1.580 -by (rtac mult_less_cancel1 1);
   1.581 -by (Simp_tac 1);
   1.582 -qed "Suc_mult_less_cancel1";
   1.583 -
   1.584 -Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
   1.585 -by (simp_tac (simpset_of HOL.thy) 1);
   1.586 -by (rtac Suc_mult_less_cancel1 1);
   1.587 -qed "Suc_mult_le_cancel1";
   1.588 -
   1.589 -Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
   1.590 -by (cut_facts_tac [less_linear] 1);
   1.591 -by Safe_tac;
   1.592 -by (assume_tac 2);
   1.593 -by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
   1.594 -by (ALLGOALS Asm_full_simp_tac);
   1.595 -qed "mult_cancel2";
   1.596 -
   1.597 -Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
   1.598 -by (dtac mult_cancel2 1);
   1.599 -by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   1.600 -qed "mult_cancel1";
   1.601 -Addsimps [mult_cancel1, mult_cancel2];
   1.602 -
   1.603 -Goal "(Suc k * m = Suc k * n) = (m = n)";
   1.604 -by (rtac mult_cancel1 1);
   1.605 -by (Simp_tac 1);
   1.606 -qed "Suc_mult_cancel1";
   1.607 -
   1.608 -
   1.609 -(*Lemma for gcd*)
   1.610 -Goal "!!m::nat. m = m*n ==> n=1 | m=0";
   1.611 -by (dtac sym 1);
   1.612 -by (rtac disjCI 1);
   1.613 -by (rtac nat_less_cases 1 THEN assume_tac 2);
   1.614 -by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
   1.615 -by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
   1.616 -qed "mult_eq_self_implies_10";
   1.617 -
   1.618 -
   1.619 -
   1.620 -
   1.621 -(*---------------------------------------------------------------------------*)
   1.622 -(* Various arithmetic proof procedures                                       *)
   1.623 -(*---------------------------------------------------------------------------*)
   1.624 -
   1.625 -(*---------------------------------------------------------------------------*)
   1.626 -(* 1. Cancellation of common terms                                           *)
   1.627 -(*---------------------------------------------------------------------------*)
   1.628 -
   1.629 -(*  Title:      HOL/arith_data.ML
   1.630 -    ID:         $Id$
   1.631 -    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
   1.632 -
   1.633 -Setup various arithmetic proof procedures.
   1.634 -*)
   1.635 -
   1.636 -signature ARITH_DATA =
   1.637 -sig
   1.638 -  val nat_cancel_sums_add: simproc list
   1.639 -  val nat_cancel_sums: simproc list
   1.640 -  val nat_cancel_factor: simproc list
   1.641 -  val nat_cancel: simproc list
   1.642 -end;
   1.643 -
   1.644 -structure ArithData: ARITH_DATA =
   1.645 -struct
   1.646 -
   1.647 -
   1.648 -(** abstract syntax of structure nat: 0, Suc, + **)
   1.649 -
   1.650 -(* mk_sum, mk_norm_sum *)
   1.651 -
   1.652 -val one = HOLogic.mk_nat 1;
   1.653 -val mk_plus = HOLogic.mk_binop "op +";
   1.654 -
   1.655 -fun mk_sum [] = HOLogic.zero
   1.656 -  | mk_sum [t] = t
   1.657 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.658 -
   1.659 -(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   1.660 -fun mk_norm_sum ts =
   1.661 -  let val (ones, sums) = partition (equal one) ts in
   1.662 -    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   1.663 -  end;
   1.664 -
   1.665 -
   1.666 -(* dest_sum *)
   1.667 -
   1.668 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   1.669 -
   1.670 -fun dest_sum tm =
   1.671 -  if HOLogic.is_zero tm then []
   1.672 -  else
   1.673 -    (case try HOLogic.dest_Suc tm of
   1.674 -      Some t => one :: dest_sum t
   1.675 -    | None =>
   1.676 -        (case try dest_plus tm of
   1.677 -          Some (t, u) => dest_sum t @ dest_sum u
   1.678 -        | None => [tm]));
   1.679 -
   1.680 -
   1.681 -(** generic proof tools **)
   1.682 -
   1.683 -(* prove conversions *)
   1.684 -
   1.685 -val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   1.686 -
   1.687 -fun prove_conv expand_tac norm_tac sg (t, u) =
   1.688 -  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
   1.689 -    (K [expand_tac, norm_tac]))
   1.690 -  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   1.691 -    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
   1.692 -
   1.693 -val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   1.694 -  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
   1.695 -
   1.696 -
   1.697 -(* rewriting *)
   1.698 -
   1.699 -fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
   1.700 -
   1.701 -val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   1.702 -val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
   1.703 -
   1.704 -
   1.705 -
   1.706 -(** cancel common summands **)
   1.707 -
   1.708 -structure Sum =
   1.709 -struct
   1.710 -  val mk_sum = mk_norm_sum;
   1.711 -  val dest_sum = dest_sum;
   1.712 -  val prove_conv = prove_conv;
   1.713 -  val norm_tac = simp_all add_rules THEN simp_all add_ac;
   1.714 -end;
   1.715 -
   1.716 -fun gen_uncancel_tac rule ct =
   1.717 -  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
   1.718 -
   1.719 -
   1.720 -(* nat eq *)
   1.721 -
   1.722 -structure EqCancelSums = CancelSumsFun
   1.723 -(struct
   1.724 -  open Sum;
   1.725 -  val mk_bal = HOLogic.mk_eq;
   1.726 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.727 -  val uncancel_tac = gen_uncancel_tac add_left_cancel;
   1.728 -end);
   1.729 -
   1.730 -
   1.731 -(* nat less *)
   1.732 -
   1.733 -structure LessCancelSums = CancelSumsFun
   1.734 -(struct
   1.735 -  open Sum;
   1.736 -  val mk_bal = HOLogic.mk_binrel "op <";
   1.737 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.738 -  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
   1.739 -end);
   1.740 -
   1.741 -
   1.742 -(* nat le *)
   1.743 -
   1.744 -structure LeCancelSums = CancelSumsFun
   1.745 -(struct
   1.746 -  open Sum;
   1.747 -  val mk_bal = HOLogic.mk_binrel "op <=";
   1.748 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.749 -  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
   1.750 -end);
   1.751 -
   1.752 -
   1.753 -(* nat diff *)
   1.754 -
   1.755 -structure DiffCancelSums = CancelSumsFun
   1.756 -(struct
   1.757 -  open Sum;
   1.758 -  val mk_bal = HOLogic.mk_binop "op -";
   1.759 -  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
   1.760 -  val uncancel_tac = gen_uncancel_tac diff_cancel;
   1.761 -end);
   1.762 -
   1.763 -
   1.764 -
   1.765 -(** cancel common factor **)
   1.766 -
   1.767 -structure Factor =
   1.768 -struct
   1.769 -  val mk_sum = mk_norm_sum;
   1.770 -  val dest_sum = dest_sum;
   1.771 -  val prove_conv = prove_conv;
   1.772 -  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
   1.773 -end;
   1.774 -
   1.775 -fun mk_cnat n = cterm_of (Theory.sign_of Nat.thy) (HOLogic.mk_nat n);
   1.776 -
   1.777 -fun gen_multiply_tac rule k =
   1.778 -  if k > 0 then
   1.779 -    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
   1.780 -  else no_tac;
   1.781 -
   1.782 -
   1.783 -(* nat eq *)
   1.784 -
   1.785 -structure EqCancelFactor = CancelFactorFun
   1.786 -(struct
   1.787 -  open Factor;
   1.788 -  val mk_bal = HOLogic.mk_eq;
   1.789 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
   1.790 -  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
   1.791 -end);
   1.792 -
   1.793 -
   1.794 -(* nat less *)
   1.795 -
   1.796 -structure LessCancelFactor = CancelFactorFun
   1.797 -(struct
   1.798 -  open Factor;
   1.799 -  val mk_bal = HOLogic.mk_binrel "op <";
   1.800 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
   1.801 -  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
   1.802 -end);
   1.803 -
   1.804 -
   1.805 -(* nat le *)
   1.806 -
   1.807 -structure LeCancelFactor = CancelFactorFun
   1.808 -(struct
   1.809 -  open Factor;
   1.810 -  val mk_bal = HOLogic.mk_binrel "op <=";
   1.811 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
   1.812 -  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
   1.813 -end);
   1.814 -
   1.815 -
   1.816 -
   1.817 -(** prepare nat_cancel simprocs **)
   1.818 -
   1.819 -fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
   1.820 -val prep_pats = map prep_pat;
   1.821 -
   1.822 -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   1.823 -
   1.824 -val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
   1.825 -val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
   1.826 -val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
   1.827 -val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
   1.828 -
   1.829 -val nat_cancel_sums_add = map prep_simproc
   1.830 -  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
   1.831 -   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
   1.832 -   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
   1.833 -
   1.834 -val nat_cancel_sums = nat_cancel_sums_add @
   1.835 -  [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
   1.836 -
   1.837 -val nat_cancel_factor = map prep_simproc
   1.838 -  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
   1.839 -   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
   1.840 -   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
   1.841 -
   1.842 -val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
   1.843 -
   1.844 -
   1.845 -end;
   1.846 -
   1.847 -open ArithData;
   1.848 -
   1.849 -Addsimprocs nat_cancel;
   1.850 -
   1.851 -(*---------------------------------------------------------------------------*)
   1.852 -(* 2. Linear arithmetic                                                      *)
   1.853 -(*---------------------------------------------------------------------------*)
   1.854 -
   1.855 -(* Parameters data for general linear arithmetic functor *)
   1.856 -
   1.857 -structure LA_Logic: LIN_ARITH_LOGIC =
   1.858 -struct
   1.859 -val ccontr = ccontr;
   1.860 -val conjI = conjI;
   1.861 -val neqE = linorder_neqE;
   1.862 -val notI = notI;
   1.863 -val sym = sym;
   1.864 -val not_lessD = linorder_not_less RS iffD1;
   1.865 -val not_leD = linorder_not_le RS iffD1;
   1.866 -
   1.867 -
   1.868 -fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   1.869 -
   1.870 -val mk_Trueprop = HOLogic.mk_Trueprop;
   1.871 -
   1.872 -fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
   1.873 -  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
   1.874 -
   1.875 -fun is_False thm =
   1.876 -  let val _ $ t = #prop(rep_thm thm)
   1.877 -  in t = Const("False",HOLogic.boolT) end;
   1.878 -
   1.879 -fun is_nat(t) = fastype_of1 t = HOLogic.natT;
   1.880 -
   1.881 -fun mk_nat_thm sg t =
   1.882 -  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
   1.883 -  in instantiate ([],[(cn,ct)]) le0 end;
   1.884 -
   1.885 -end;
   1.886 -
   1.887 -signature LIN_ARITH_DATA2 =
   1.888 -sig
   1.889 -  include LIN_ARITH_DATA
   1.890 -  val discrete: (string * bool)list ref
   1.891 -end;
   1.892 -
   1.893 -structure LA_Data_Ref: LIN_ARITH_DATA2 =
   1.894 -struct
   1.895 -  val add_mono_thms = ref ([]:thm list);
   1.896 -  val lessD = ref ([]:thm list);
   1.897 -  val ss_ref = ref HOL_basic_ss;
   1.898 -  val discrete = ref ([]:(string*bool)list);
   1.899 -
   1.900 -(* Decomposition of terms *)
   1.901 -
   1.902 -fun nT (Type("fun",[N,_])) = N = HOLogic.natT
   1.903 -  | nT _ = false;
   1.904 -
   1.905 -fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
   1.906 -                           | Some n => (overwrite(p,(t,n+m:int)), i));
   1.907 -
   1.908 -(* Turn term into list of summand * multiplicity plus a constant *)
   1.909 -fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   1.910 -  | poly(all as Const("op -",T) $ s $ t, m, pi) =
   1.911 -      if nT T then add_atom(all,m,pi)
   1.912 -      else poly(s,m,poly(t,~1*m,pi))
   1.913 -  | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi)
   1.914 -  | poly(Const("0",_), _, pi) = pi
   1.915 -  | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m))
   1.916 -  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)=
   1.917 -      (poly(t,m*HOLogic.dest_binum c,pi)
   1.918 -       handle TERM _ => add_atom(all,m,pi))
   1.919 -  | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)=
   1.920 -      (poly(t,m*HOLogic.dest_binum c,pi)
   1.921 -       handle TERM _ => add_atom(all,m,pi))
   1.922 -  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
   1.923 -     ((p,i + m*HOLogic.dest_binum t)
   1.924 -      handle TERM _ => add_atom(all,m,(p,i)))
   1.925 -  | poly x  = add_atom x;
   1.926 -
   1.927 -fun decomp2(rel,lhs,rhs) =
   1.928 -  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
   1.929 -  in case rel of
   1.930 -       "op <"  => Some(p,i,"<",q,j)
   1.931 -     | "op <=" => Some(p,i,"<=",q,j)
   1.932 -     | "op ="  => Some(p,i,"=",q,j)
   1.933 -     | _       => None
   1.934 -  end;
   1.935 -
   1.936 -fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
   1.937 -  | negate None = None;
   1.938 -
   1.939 -fun decomp1 (T,xxx) =
   1.940 -  (case T of
   1.941 -     Type("fun",[Type(D,[]),_]) =>
   1.942 -       (case assoc(!discrete,D) of
   1.943 -          None => None
   1.944 -        | Some d => (case decomp2 xxx of
   1.945 -                       None => None
   1.946 -                     | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
   1.947 -   | _ => None);
   1.948 -
   1.949 -fun decomp (_$(Const(rel,T)$lhs$rhs)) = decomp1 (T,(rel,lhs,rhs))
   1.950 -  | decomp (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   1.951 -      negate(decomp1 (T,(rel,lhs,rhs)))
   1.952 -  | decomp _ = None
   1.953 -end;
   1.954 -
   1.955 -let
   1.956 -
   1.957 -(* reduce contradictory <= to False.
   1.958 -   Most of the work is done by the cancel tactics.
   1.959 -*)
   1.960 -val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
   1.961 -
   1.962 -val add_mono_thms = map (fn s => prove_goal Arith.thy s
   1.963 - (fn prems => [cut_facts_tac prems 1,
   1.964 -               blast_tac (claset() addIs [add_le_mono]) 1]))
   1.965 -["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
   1.966 - "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
   1.967 - "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
   1.968 - "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
   1.969 -];
   1.970 -
   1.971 -in
   1.972 -LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
   1.973 -LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [Suc_leI];
   1.974 -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
   1.975 -                      addsimprocs nat_cancel_sums_add;
   1.976 -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("nat",true)]
   1.977 -end;
   1.978 -
   1.979 -structure Fast_Arith =
   1.980 -  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
   1.981 -
   1.982 -val fast_arith_tac = Fast_Arith.lin_arith_tac
   1.983 -and trace_arith    = Fast_Arith.trace;
   1.984 -
   1.985 -let
   1.986 -val nat_arith_simproc_pats =
   1.987 -  map (fn s => Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.boolT))
   1.988 -      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
   1.989 -
   1.990 -val fast_nat_arith_simproc = mk_simproc
   1.991 -  "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
   1.992 -in
   1.993 -Addsimprocs [fast_nat_arith_simproc]
   1.994 -end;
   1.995 -
   1.996 -(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
   1.997 -useful to detect inconsistencies among the premises for subgoals which are
   1.998 -*not* themselves (in)equalities, because the latter activate
   1.999 -fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
  1.1000 -solver all the time rather than add the additional check. *)
  1.1001 -
  1.1002 -simpset_ref () := (simpset() addSolver
  1.1003 -   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
  1.1004 -
  1.1005 -(*Elimination of `-' on nat*)
  1.1006 -Goal "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))";
  1.1007 -by (case_tac "a < b" 1);
  1.1008 -by (auto_tac (claset(), simpset() addsimps [diff_is_0_eq RS iffD2]));
  1.1009 -qed "nat_diff_split";
  1.1010 -
  1.1011 -(* FIXME: K true should be replaced by a sensible test to speed things up
  1.1012 -   in case there are lots of irrelevant terms involved;
  1.1013 -   elimination of min/max can be optimized:
  1.1014 -   (max m n + k <= r) = (m+k <= r & n+k <= r)
  1.1015 -   (l <= min m n + k) = (l <= m+k & l <= n+k)
  1.1016 -*)
  1.1017 -val arith_tac_split_thms = ref [nat_diff_split,split_min,split_max];
  1.1018 -fun arith_tac i =
  1.1019 -  refute_tac (K true) (REPEAT o split_tac (!arith_tac_split_thms))
  1.1020 -             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i;
  1.1021 -
  1.1022 -
  1.1023 -(* proof method setup *)
  1.1024 -
  1.1025 -fun arith_method prems =
  1.1026 -  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
  1.1027 -
  1.1028 -val arith_setup =
  1.1029 - [Method.add_methods
  1.1030 -  [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]];
  1.1031 -
  1.1032 -(*---------------------------------------------------------------------------*)
  1.1033 -(* End of proof procedures. Now go and USE them!                             *)
  1.1034 -(*---------------------------------------------------------------------------*)
  1.1035  
  1.1036  Goal "m <= m*(m::nat)";
  1.1037  by (induct_tac "m" 1);
     2.1 --- a/src/HOL/Arith.thy	Tue Jul 25 00:03:39 2000 +0200
     2.2 +++ b/src/HOL/Arith.thy	Tue Jul 25 00:06:46 2000 +0200
     2.3 @@ -1,29 +1,21 @@
     2.4  (*  Title:      HOL/Arith.thy
     2.5      ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1993  University of Cambridge
     2.8  
     2.9 -Arithmetic operators + - and * (for div, mod and dvd, see Divides)
    2.10 +Setup arithmetic proof procedures.
    2.11  *)
    2.12  
    2.13 -Arith = Nat +
    2.14 +theory Arith = Nat
    2.15 +files "arith_data.ML":
    2.16  
    2.17 -instance
    2.18 -  nat :: {plus, minus, times, power}
    2.19 -
    2.20 -(* size of a datatype value; overloaded *)
    2.21 -consts size :: 'a => nat
    2.22 +setup arith_setup
    2.23  
    2.24 -primrec
    2.25 -  add_0    "0 + n = n"
    2.26 -  add_Suc  "Suc m + n = Suc(m + n)"
    2.27 +(*elimination of `-' on nat*)
    2.28 +lemma nat_diff_split:
    2.29 +    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
    2.30 +  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [RS iffD2])
    2.31  
    2.32 -primrec
    2.33 -  diff_0   "m - 0 = m"
    2.34 -  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
    2.35 +ML {* val nat_diff_split = thm "nat_diff_split" *}
    2.36  
    2.37 -primrec
    2.38 -  mult_0   "0 * n = 0"
    2.39 -  mult_Suc "Suc m * n = n + (m * n)"
    2.40 +lemmas [arith_split] = nat_diff_split split_min split_max
    2.41  
    2.42  end
     3.1 --- a/src/HOL/Integ/Bin.ML	Tue Jul 25 00:03:39 2000 +0200
     3.2 +++ b/src/HOL/Integ/Bin.ML	Tue Jul 25 00:06:46 2000 +0200
     3.3 @@ -258,7 +258,7 @@
     3.4  
     3.5  (*Negation of a coefficient*)
     3.6  Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
     3.7 -by (simp_tac (simpset_of Int.thy addsimps [number_of_minus, zmult_zminus]) 1);
     3.8 +by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1);
     3.9  qed "zminus_number_of_zmult";
    3.10  
    3.11  Addsimps [zminus_number_of_zmult];
     4.1 --- a/src/HOL/Integ/Int.ML	Tue Jul 25 00:03:39 2000 +0200
     4.2 +++ b/src/HOL/Integ/Int.ML	Tue Jul 25 00:06:46 2000 +0200
     4.3 @@ -34,7 +34,7 @@
     4.4    val ss		= HOL_ss
     4.5    val eq_reflection	= eq_reflection
     4.6  
     4.7 -  val thy	= IntDef.thy
     4.8 +  val sg_ref 		= Sign.self_ref (Theory.sign_of (the_context ()))
     4.9    val T		= HOLogic.intT
    4.10    val zero	= Const ("IntDef.int", HOLogic.natT --> T) $ HOLogic.zero
    4.11    val restrict_to_left  = restrict_to_left
     5.1 --- a/src/HOL/Integ/IntArith.ML	Tue Jul 25 00:03:39 2000 +0200
     5.2 +++ b/src/HOL/Integ/IntArith.ML	Tue Jul 25 00:06:46 2000 +0200
     5.3 @@ -1,575 +1,8 @@
     5.4 -(*  Title:      HOL/Integ/IntArith.thy
     5.5 +(*  Title:      HOL/Integ/IntArith.ML
     5.6      ID:         $Id$
     5.7      Authors:    Larry Paulson and Tobias Nipkow
     5.8 -
     5.9 -Simprocs and decision procedure for linear arithmetic.
    5.10  *)
    5.11  
    5.12 -(*** Simprocs for numeric literals ***)
    5.13 -
    5.14 -(** Combining of literal coefficients in sums of products **)
    5.15 -
    5.16 -Goal "(x < y) = (x-y < (#0::int))";
    5.17 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
    5.18 -qed "zless_iff_zdiff_zless_0";
    5.19 -
    5.20 -Goal "(x = y) = (x-y = (#0::int))";
    5.21 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
    5.22 -qed "eq_iff_zdiff_eq_0";
    5.23 -
    5.24 -Goal "(x <= y) = (x-y <= (#0::int))";
    5.25 -by (simp_tac (simpset() addsimps zcompare_rls) 1);
    5.26 -qed "zle_iff_zdiff_zle_0";
    5.27 -
    5.28 -
    5.29 -(** For combine_numerals **)
    5.30 -
    5.31 -Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
    5.32 -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
    5.33 -qed "left_zadd_zmult_distrib";
    5.34 -
    5.35 -
    5.36 -(** For cancel_numerals **)
    5.37 -
    5.38 -val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
    5.39 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    5.40 -			   zle_iff_zdiff_zle_0] @
    5.41 -		        map (inst "y" "n")
    5.42 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    5.43 -			   zle_iff_zdiff_zle_0];
    5.44 -
    5.45 -Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    5.46 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    5.47 -		                     zadd_ac@rel_iff_rel_0_rls) 1);
    5.48 -qed "eq_add_iff1";
    5.49 -
    5.50 -Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    5.51 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    5.52 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
    5.53 -qed "eq_add_iff2";
    5.54 -
    5.55 -Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
    5.56 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    5.57 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
    5.58 -qed "less_add_iff1";
    5.59 -
    5.60 -Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
    5.61 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    5.62 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
    5.63 -qed "less_add_iff2";
    5.64 -
    5.65 -Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
    5.66 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    5.67 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
    5.68 -qed "le_add_iff1";
    5.69 -
    5.70 -Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
    5.71 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
    5.72 -                                     @zadd_ac@rel_iff_rel_0_rls) 1);
    5.73 -qed "le_add_iff2";
    5.74 -
    5.75 -(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
    5.76 -Goal "u = u' ==> (t==u) == (t==u')";
    5.77 -by Auto_tac;
    5.78 -qed "eq_cong2";
    5.79 -
    5.80 -
    5.81 -structure Int_Numeral_Simprocs =
    5.82 -struct
    5.83 -
    5.84 -(*Utilities*)
    5.85 -
    5.86 -fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
    5.87 -                   NumeralSyntax.mk_bin n;
    5.88 -
    5.89 -(*Decodes a binary INTEGER*)
    5.90 -fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
    5.91 -     (NumeralSyntax.dest_bin w
    5.92 -      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    5.93 -  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    5.94 -
    5.95 -fun find_first_numeral past (t::terms) =
    5.96 -	((dest_numeral t, rev past @ terms)
    5.97 -	 handle TERM _ => find_first_numeral (t::past) terms)
    5.98 -  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    5.99 -
   5.100 -val zero = mk_numeral 0;
   5.101 -val mk_plus = HOLogic.mk_binop "op +";
   5.102 -
   5.103 -val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
   5.104 -
   5.105 -(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   5.106 -fun mk_sum []        = zero
   5.107 -  | mk_sum [t,u]     = mk_plus (t, u)
   5.108 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   5.109 -
   5.110 -(*this version ALWAYS includes a trailing zero*)
   5.111 -fun long_mk_sum []        = zero
   5.112 -  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   5.113 -
   5.114 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
   5.115 -
   5.116 -(*decompose additions AND subtractions as a sum*)
   5.117 -fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
   5.118 -        dest_summing (pos, t, dest_summing (pos, u, ts))
   5.119 -  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
   5.120 -        dest_summing (pos, t, dest_summing (not pos, u, ts))
   5.121 -  | dest_summing (pos, t, ts) =
   5.122 -	if pos then t::ts else uminus_const$t :: ts;
   5.123 -
   5.124 -fun dest_sum t = dest_summing (true, t, []);
   5.125 -
   5.126 -val mk_diff = HOLogic.mk_binop "op -";
   5.127 -val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT;
   5.128 -
   5.129 -val one = mk_numeral 1;
   5.130 -val mk_times = HOLogic.mk_binop "op *";
   5.131 -
   5.132 -fun mk_prod [] = one
   5.133 -  | mk_prod [t] = t
   5.134 -  | mk_prod (t :: ts) = if t = one then mk_prod ts
   5.135 -                        else mk_times (t, mk_prod ts);
   5.136 -
   5.137 -val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
   5.138 -
   5.139 -fun dest_prod t =
   5.140 -      let val (t,u) = dest_times t 
   5.141 -      in  dest_prod t @ dest_prod u  end
   5.142 -      handle TERM _ => [t];
   5.143 -
   5.144 -(*DON'T do the obvious simplifications; that would create special cases*) 
   5.145 -fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
   5.146 -
   5.147 -(*Express t as a product of (possibly) a numeral with other sorted terms*)
   5.148 -fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
   5.149 -  | dest_coeff sign t =
   5.150 -    let val ts = sort Term.term_ord (dest_prod t)
   5.151 -	val (n, ts') = find_first_numeral [] ts
   5.152 -                          handle TERM _ => (1, ts)
   5.153 -    in (sign*n, mk_prod ts') end;
   5.154 -
   5.155 -(*Find first coefficient-term THAT MATCHES u*)
   5.156 -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
   5.157 -  | find_first_coeff past u (t::terms) =
   5.158 -	let val (n,u') = dest_coeff 1 t
   5.159 -	in  if u aconv u' then (n, rev past @ terms)
   5.160 -			  else find_first_coeff (t::past) u terms
   5.161 -	end
   5.162 -	handle TERM _ => find_first_coeff (t::past) u terms;
   5.163 -
   5.164 -
   5.165 -(*Simplify #1*n and n*#1 to n*)
   5.166 -val add_0s = [zadd_0, zadd_0_right];
   5.167 -val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
   5.168 -
   5.169 -(*To perform binary arithmetic*)
   5.170 -val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
   5.171 -
   5.172 -(*To evaluate binary negations of coefficients*)
   5.173 -val zminus_simps = NCons_simps @
   5.174 -                   [number_of_minus RS sym, 
   5.175 -		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   5.176 -		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   5.177 -
   5.178 -(*To let us treat subtraction as addition*)
   5.179 -val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
   5.180 -
   5.181 -(*Apply the given rewrite (if present) just once*)
   5.182 -fun trans_tac None      = all_tac
   5.183 -  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
   5.184 -
   5.185 -fun prove_conv name tacs sg (t, u) =
   5.186 -  if t aconv u then None
   5.187 -  else
   5.188 -  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
   5.189 -  in Some
   5.190 -     (prove_goalw_cterm [] ct (K tacs)
   5.191 -      handle ERROR => error 
   5.192 -	  ("The error(s) above occurred while trying to prove " ^
   5.193 -	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   5.194 -  end;
   5.195 -
   5.196 -fun simplify_meta_eq rules =
   5.197 -    mk_meta_eq o
   5.198 -    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
   5.199 -
   5.200 -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   5.201 -fun prep_pat s = Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.termT);
   5.202 -val prep_pats = map prep_pat;
   5.203 -
   5.204 -structure CancelNumeralsCommon =
   5.205 -  struct
   5.206 -  val mk_sum    	= mk_sum
   5.207 -  val dest_sum		= dest_sum
   5.208 -  val mk_coeff		= mk_coeff
   5.209 -  val dest_coeff	= dest_coeff 1
   5.210 -  val find_first_coeff	= find_first_coeff []
   5.211 -  val trans_tac         = trans_tac
   5.212 -  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   5.213 -                                                     zminus_simps@zadd_ac))
   5.214 -                 THEN ALLGOALS
   5.215 -                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
   5.216 -                                               bin_simps@zadd_ac@zmult_ac))
   5.217 -  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   5.218 -  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   5.219 -  end;
   5.220 -
   5.221 -
   5.222 -structure EqCancelNumerals = CancelNumeralsFun
   5.223 - (open CancelNumeralsCommon
   5.224 -  val prove_conv = prove_conv "inteq_cancel_numerals"
   5.225 -  val mk_bal   = HOLogic.mk_eq
   5.226 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   5.227 -  val bal_add1 = eq_add_iff1 RS trans
   5.228 -  val bal_add2 = eq_add_iff2 RS trans
   5.229 -);
   5.230 -
   5.231 -structure LessCancelNumerals = CancelNumeralsFun
   5.232 - (open CancelNumeralsCommon
   5.233 -  val prove_conv = prove_conv "intless_cancel_numerals"
   5.234 -  val mk_bal   = HOLogic.mk_binrel "op <"
   5.235 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
   5.236 -  val bal_add1 = less_add_iff1 RS trans
   5.237 -  val bal_add2 = less_add_iff2 RS trans
   5.238 -);
   5.239 -
   5.240 -structure LeCancelNumerals = CancelNumeralsFun
   5.241 - (open CancelNumeralsCommon
   5.242 -  val prove_conv = prove_conv "intle_cancel_numerals"
   5.243 -  val mk_bal   = HOLogic.mk_binrel "op <="
   5.244 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
   5.245 -  val bal_add1 = le_add_iff1 RS trans
   5.246 -  val bal_add2 = le_add_iff2 RS trans
   5.247 -);
   5.248 -
   5.249 -val cancel_numerals = 
   5.250 -  map prep_simproc
   5.251 -   [("inteq_cancel_numerals",
   5.252 -     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
   5.253 -		"(l::int) - m = n", "(l::int) = m - n", 
   5.254 -		"(l::int) * m = n", "(l::int) = m * n"], 
   5.255 -     EqCancelNumerals.proc),
   5.256 -    ("intless_cancel_numerals", 
   5.257 -     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
   5.258 -		"(l::int) - m < n", "(l::int) < m - n", 
   5.259 -		"(l::int) * m < n", "(l::int) < m * n"], 
   5.260 -     LessCancelNumerals.proc),
   5.261 -    ("intle_cancel_numerals", 
   5.262 -     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
   5.263 -		"(l::int) - m <= n", "(l::int) <= m - n", 
   5.264 -		"(l::int) * m <= n", "(l::int) <= m * n"], 
   5.265 -     LeCancelNumerals.proc)];
   5.266 -
   5.267 -
   5.268 -structure CombineNumeralsData =
   5.269 -  struct
   5.270 -  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
   5.271 -  val dest_sum		= dest_sum
   5.272 -  val mk_coeff		= mk_coeff
   5.273 -  val dest_coeff	= dest_coeff 1
   5.274 -  val left_distrib	= left_zadd_zmult_distrib RS trans
   5.275 -  val prove_conv	= prove_conv "int_combine_numerals"
   5.276 -  val trans_tac          = trans_tac
   5.277 -  val norm_tac = ALLGOALS
   5.278 -                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   5.279 -                                              zminus_simps@zadd_ac))
   5.280 -                 THEN ALLGOALS
   5.281 -                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
   5.282 -                                               bin_simps@zadd_ac@zmult_ac))
   5.283 -  val numeral_simp_tac	= ALLGOALS 
   5.284 -                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   5.285 -  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   5.286 -  end;
   5.287 -
   5.288 -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   5.289 -  
   5.290 -val combine_numerals = 
   5.291 -    prep_simproc ("int_combine_numerals",
   5.292 -		  prep_pats ["(i::int) + j", "(i::int) - j"],
   5.293 -		  CombineNumerals.proc);
   5.294 -
   5.295 -end;
   5.296 -
   5.297 -
   5.298 -Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   5.299 -Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   5.300 -
   5.301 -(*The Abel_Cancel simprocs are now obsolete*)
   5.302 -Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
   5.303 -
   5.304 -(*examples:
   5.305 -print_depth 22;
   5.306 -set timing;
   5.307 -set trace_simp;
   5.308 -fun test s = (Goal s; by (Simp_tac 1)); 
   5.309 -
   5.310 -test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
   5.311 -
   5.312 -test "#2*u = (u::int)";
   5.313 -test "(i + j + #12 + (k::int)) - #15 = y";
   5.314 -test "(i + j + #12 + (k::int)) - #5 = y";
   5.315 -
   5.316 -test "y - b < (b::int)";
   5.317 -test "y - (#3*b + c) < (b::int) - #2*c";
   5.318 -
   5.319 -test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
   5.320 -test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
   5.321 -test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
   5.322 -test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
   5.323 -
   5.324 -test "(i + j + #12 + (k::int)) = u + #15 + y";
   5.325 -test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
   5.326 -
   5.327 -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)";
   5.328 -
   5.329 -test "a + -(b+c) + b = (d::int)";
   5.330 -test "a + -(b+c) - b = (d::int)";
   5.331 -
   5.332 -(*negative numerals*)
   5.333 -test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
   5.334 -test "(i + j + #-3 + (k::int)) < u + #5 + y";
   5.335 -test "(i + j + #3 + (k::int)) < u + #-6 + y";
   5.336 -test "(i + j + #-12 + (k::int)) - #15 = y";
   5.337 -test "(i + j + #12 + (k::int)) - #-15 = y";
   5.338 -test "(i + j + #-12 + (k::int)) - #-15 = y";
   5.339 -*)
   5.340 -
   5.341 -
   5.342 -(** Constant folding for integer plus and times **)
   5.343 -
   5.344 -(*We do not need
   5.345 -    structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
   5.346 -    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
   5.347 -  because combine_numerals does the same thing*)
   5.348 -
   5.349 -structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
   5.350 -struct
   5.351 -  val ss		= HOL_ss
   5.352 -  val eq_reflection	= eq_reflection
   5.353 -  val thy    = Bin.thy
   5.354 -  val T	     = HOLogic.intT
   5.355 -  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
   5.356 -  val add_ac = zmult_ac
   5.357 -end;
   5.358 -
   5.359 -structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
   5.360 -
   5.361 -Addsimprocs [Int_Times_Assoc.conv];
   5.362 -
   5.363 -
   5.364 -(** The same for the naturals **)
   5.365 -
   5.366 -structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
   5.367 -struct
   5.368 -  val ss		= HOL_ss
   5.369 -  val eq_reflection	= eq_reflection
   5.370 -  val thy    = Bin.thy
   5.371 -  val T	     = HOLogic.natT
   5.372 -  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
   5.373 -  val add_ac = mult_ac
   5.374 -end;
   5.375 -
   5.376 -structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
   5.377 -
   5.378 -Addsimprocs [Nat_Times_Assoc.conv];
   5.379 -
   5.380 -
   5.381 -
   5.382 -(*** decision procedure for linear arithmetic ***)
   5.383 -
   5.384 -(*---------------------------------------------------------------------------*)
   5.385 -(* Linear arithmetic                                                         *)
   5.386 -(*---------------------------------------------------------------------------*)
   5.387 -
   5.388 -(*
   5.389 -Instantiation of the generic linear arithmetic package for int.
   5.390 -*)
   5.391 -
   5.392 -(* Update parameters of arithmetic prover *)
   5.393 -let
   5.394 -
   5.395 -(* reduce contradictory <= to False *)
   5.396 -val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
   5.397 -                [int_0, zadd_0, zadd_0_right, zdiff_def,
   5.398 -		 zadd_zminus_inverse, zadd_zminus_inverse2, 
   5.399 -		 zmult_0, zmult_0_right, 
   5.400 -		 zmult_1, zmult_1_right, 
   5.401 -		 zmult_minus1, zmult_minus1_right,
   5.402 -		 zminus_zadd_distrib, zminus_zminus];
   5.403 -
   5.404 -val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
   5.405 -               Int_Numeral_Simprocs.cancel_numerals;
   5.406 -
   5.407 -val add_mono_thms =
   5.408 -  map (fn s => prove_goal Int.thy s
   5.409 -                 (fn prems => [cut_facts_tac prems 1,
   5.410 -                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
   5.411 -    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
   5.412 -     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
   5.413 -     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
   5.414 -     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
   5.415 -    ];
   5.416 -
   5.417 -in
   5.418 -LA_Data_Ref.add_mono_thms := !LA_Data_Ref.add_mono_thms @ add_mono_thms;
   5.419 -LA_Data_Ref.lessD := !LA_Data_Ref.lessD @ [add1_zle_eq RS iffD2];
   5.420 -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules
   5.421 -                      addsimprocs simprocs
   5.422 -                      addcongs [if_weak_cong];
   5.423 -LA_Data_Ref.discrete := !LA_Data_Ref.discrete @ [("IntDef.int",true)]
   5.424 -end;
   5.425 -
   5.426 -let
   5.427 -val int_arith_simproc_pats =
   5.428 -  map (fn s => Thm.read_cterm (Theory.sign_of Int.thy) (s, HOLogic.boolT))
   5.429 -      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
   5.430 -
   5.431 -val fast_int_arith_simproc = mk_simproc
   5.432 -  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
   5.433 -in
   5.434 -Addsimprocs [fast_int_arith_simproc]
   5.435 -end;
   5.436 -
   5.437 -(* Some test data
   5.438 -Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   5.439 -by (fast_arith_tac 1);
   5.440 -Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
   5.441 -by (fast_arith_tac 1);
   5.442 -Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
   5.443 -by (fast_arith_tac 1);
   5.444 -Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
   5.445 -by (fast_arith_tac 1);
   5.446 -Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
   5.447 -\     ==> a+a <= j+j";
   5.448 -by (fast_arith_tac 1);
   5.449 -Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
   5.450 -\     ==> a+a - - #-1 < j+j - #3";
   5.451 -by (fast_arith_tac 1);
   5.452 -Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   5.453 -by (arith_tac 1);
   5.454 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   5.455 -\     ==> a <= l";
   5.456 -by (fast_arith_tac 1);
   5.457 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   5.458 -\     ==> a+a+a+a <= l+l+l+l";
   5.459 -by (fast_arith_tac 1);
   5.460 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   5.461 -\     ==> a+a+a+a+a <= l+l+l+l+i";
   5.462 -by (fast_arith_tac 1);
   5.463 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   5.464 -\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   5.465 -by (fast_arith_tac 1);
   5.466 -Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   5.467 -\     ==> #6*a <= #5*l+i";
   5.468 -by (fast_arith_tac 1);
   5.469 -*)
   5.470 -
   5.471 -(*---------------------------------------------------------------------------*)
   5.472 -(* End of linear arithmetic                                                  *)
   5.473 -(*---------------------------------------------------------------------------*)
   5.474 -
   5.475 -(** Simplification of inequalities involving numerical constants **)
   5.476 -
   5.477 -Goal "(w <= z - (#1::int)) = (w<(z::int))";
   5.478 -by (arith_tac 1);
   5.479 -qed "zle_diff1_eq";
   5.480 -Addsimps [zle_diff1_eq];
   5.481 -
   5.482 -Goal "(w < z + #1) = (w<=(z::int))";
   5.483 -by (arith_tac 1);
   5.484 -qed "zle_add1_eq_le";
   5.485 -Addsimps [zle_add1_eq_le];
   5.486 -
   5.487 -Goal "(z = z + w) = (w = (#0::int))";
   5.488 -by (arith_tac 1);
   5.489 -qed "zadd_left_cancel0";
   5.490 -Addsimps [zadd_left_cancel0];
   5.491 -
   5.492 -
   5.493 -(* nat *)
   5.494 -
   5.495 -Goal "#0 <= z ==> int (nat z) = z"; 
   5.496 -by (asm_full_simp_tac
   5.497 -    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
   5.498 -qed "nat_0_le"; 
   5.499 -
   5.500 -Goal "z <= #0 ==> nat z = 0"; 
   5.501 -by (case_tac "z = #0" 1);
   5.502 -by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
   5.503 -by (asm_full_simp_tac 
   5.504 -    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
   5.505 -qed "nat_le_0"; 
   5.506 -
   5.507 -Addsimps [nat_0_le, nat_le_0];
   5.508 -
   5.509 -val [major,minor] = Goal "[| #0 <= z;  !!m. z = int m ==> P |] ==> P"; 
   5.510 -by (rtac (major RS nat_0_le RS sym RS minor) 1);
   5.511 -qed "nonneg_eq_int"; 
   5.512 -
   5.513 -Goal "#0 <= w ==> (nat w = m) = (w = int m)";
   5.514 -by Auto_tac;
   5.515 -qed "nat_eq_iff";
   5.516 -
   5.517 -Goal "#0 <= w ==> (m = nat w) = (w = int m)";
   5.518 -by Auto_tac;
   5.519 -qed "nat_eq_iff2";
   5.520 -
   5.521 -Goal "#0 <= w ==> (nat w < m) = (w < int m)";
   5.522 -by (rtac iffI 1);
   5.523 -by (asm_full_simp_tac 
   5.524 -    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
   5.525 -by (etac (nat_0_le RS subst) 1);
   5.526 -by (Simp_tac 1);
   5.527 -qed "nat_less_iff";
   5.528 -
   5.529 -
   5.530 -(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
   5.531 -Addsimps [int_0, int_Suc, symmetric zdiff_def];
   5.532 -
   5.533 -Goal "nat #0 = 0";
   5.534 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   5.535 -qed "nat_0";
   5.536 -
   5.537 -Goal "nat #1 = 1";
   5.538 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   5.539 -qed "nat_1";
   5.540 -
   5.541 -Goal "nat #2 = 2";
   5.542 -by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   5.543 -qed "nat_2";
   5.544 -
   5.545 -Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
   5.546 -by (case_tac "neg z" 1);
   5.547 -by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   5.548 -by (auto_tac (claset() addIs [zless_trans], 
   5.549 -	      simpset() addsimps [neg_eq_less_0, zle_def]));
   5.550 -qed "nat_less_eq_zless";
   5.551 -
   5.552 -Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
   5.553 -by (auto_tac (claset(), 
   5.554 -	      simpset() addsimps [linorder_not_less RS sym, 
   5.555 -				  zless_nat_conj]));
   5.556 -qed "nat_le_eq_zle";
   5.557 -
   5.558 -(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
   5.559 -Goal "n<=m --> int m - int n = int (m-n)";
   5.560 -by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   5.561 -by Auto_tac;
   5.562 -qed_spec_mp "zdiff_int";
   5.563 -
   5.564 -
   5.565 -(*** abs: absolute value, as an integer ****)
   5.566 -
   5.567 -(* Simpler: use zabs_def as rewrite rule;
   5.568 -   but arith_tac is not parameterized by such simp rules
   5.569 -*)
   5.570 -Goalw [zabs_def]
   5.571 - "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))";
   5.572 -by(Simp_tac 1);
   5.573 -qed "zabs_split";
   5.574 -
   5.575 -arith_tac_split_thms := !arith_tac_split_thms @ [zabs_split];
   5.576 -
   5.577  Goal "abs(abs(x::int)) = abs(x)";
   5.578  by(arith_tac 1);
   5.579  qed "abs_abs";
   5.580 @@ -634,4 +67,3 @@
   5.581                simpset() addsimps [int_0_less_mult_iff, 
   5.582                                    linorder_not_less RS sym]));
   5.583  qed "zmult_le_0_iff";
   5.584 -
     6.1 --- a/src/HOL/Integ/IntArith.thy	Tue Jul 25 00:03:39 2000 +0200
     6.2 +++ b/src/HOL/Integ/IntArith.thy	Tue Jul 25 00:06:46 2000 +0200
     6.3 @@ -1,2 +1,8 @@
     6.4 -theory IntArith = Bin:
     6.5 +
     6.6 +theory IntArith = Bin
     6.7 +files ("int_arith1.ML") ("int_arith2.ML"):
     6.8 +
     6.9 +use "int_arith1.ML"	setup int_arith_setup
    6.10 +use "int_arith2.ML"	lemmas [arith_split] = zabs_split
    6.11 +
    6.12  end
     7.1 --- a/src/HOL/Integ/NatSimprocs.ML	Tue Jul 25 00:03:39 2000 +0200
     7.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Tue Jul 25 00:06:46 2000 +0200
     7.3 @@ -3,374 +3,9 @@
     7.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.5      Copyright   2000  University of Cambridge
     7.6  
     7.7 -Simprocs for nat numerals
     7.8 +Simprocs for nat numerals (see also nat_simprocs.ML).
     7.9  *)
    7.10  
    7.11 -Goal "number_of v + (number_of v' + (k::nat)) = \
    7.12 -\        (if neg (number_of v) then number_of v' + k \
    7.13 -\         else if neg (number_of v') then number_of v + k \
    7.14 -\         else number_of (bin_add v v') + k)";
    7.15 -by (Simp_tac 1);
    7.16 -qed "nat_number_of_add_left";
    7.17 -
    7.18 -
    7.19 -(** For combine_numerals **)
    7.20 -
    7.21 -Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
    7.22 -by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
    7.23 -qed "left_add_mult_distrib";
    7.24 -
    7.25 -
    7.26 -(** For cancel_numerals **)
    7.27 -
    7.28 -Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
    7.29 -by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
    7.30 -		            addsimps [add_mult_distrib]) 1);
    7.31 -qed "nat_diff_add_eq1";
    7.32 -
    7.33 -Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
    7.34 -by (asm_simp_tac (simpset() addsplits [nat_diff_split] 
    7.35 -		            addsimps [add_mult_distrib]) 1);
    7.36 -qed "nat_diff_add_eq2";
    7.37 -
    7.38 -Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    7.39 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
    7.40 -                                  addsimps [add_mult_distrib]));
    7.41 -qed "nat_eq_add_iff1";
    7.42 -
    7.43 -Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    7.44 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
    7.45 -                                  addsimps [add_mult_distrib]));
    7.46 -qed "nat_eq_add_iff2";
    7.47 -
    7.48 -Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
    7.49 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
    7.50 -                                  addsimps [add_mult_distrib]));
    7.51 -qed "nat_less_add_iff1";
    7.52 -
    7.53 -Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
    7.54 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
    7.55 -                                  addsimps [add_mult_distrib]));
    7.56 -qed "nat_less_add_iff2";
    7.57 -
    7.58 -Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
    7.59 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
    7.60 -                                  addsimps [add_mult_distrib]));
    7.61 -qed "nat_le_add_iff1";
    7.62 -
    7.63 -Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
    7.64 -by (auto_tac (claset(), simpset() addsplits [nat_diff_split] 
    7.65 -                                  addsimps [add_mult_distrib]));
    7.66 -qed "nat_le_add_iff2";
    7.67 -
    7.68 -
    7.69 -structure Nat_Numeral_Simprocs =
    7.70 -struct
    7.71 -
    7.72 -(*Utilities*)
    7.73 -
    7.74 -fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ 
    7.75 -                   NumeralSyntax.mk_bin n;
    7.76 -
    7.77 -(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
    7.78 -fun dest_numeral (Const ("0", _)) = 0
    7.79 -  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
    7.80 -  | dest_numeral (Const("Numeral.number_of", _) $ w) = 
    7.81 -      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
    7.82 -       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
    7.83 -  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
    7.84 -
    7.85 -fun find_first_numeral past (t::terms) =
    7.86 -	((dest_numeral t, t, rev past @ terms)
    7.87 -	 handle TERM _ => find_first_numeral (t::past) terms)
    7.88 -  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    7.89 -
    7.90 -val zero = mk_numeral 0;
    7.91 -val mk_plus = HOLogic.mk_binop "op +";
    7.92 -
    7.93 -(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
    7.94 -fun mk_sum []        = zero
    7.95 -  | mk_sum [t,u]     = mk_plus (t, u)
    7.96 -  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    7.97 -
    7.98 -(*this version ALWAYS includes a trailing zero*)
    7.99 -fun long_mk_sum []        = zero
   7.100 -  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   7.101 -
   7.102 -val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   7.103 -
   7.104 -(*extract the outer Sucs from a term and convert them to a binary numeral*)
   7.105 -fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
   7.106 -  | dest_Sucs (0, t) = t
   7.107 -  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
   7.108 -
   7.109 -fun dest_sum t =
   7.110 -      let val (t,u) = dest_plus t 
   7.111 -      in  dest_sum t @ dest_sum u  end
   7.112 -      handle TERM _ => [t];
   7.113 -
   7.114 -fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
   7.115 -
   7.116 -val trans_tac = Int_Numeral_Simprocs.trans_tac;
   7.117 -
   7.118 -val prove_conv = Int_Numeral_Simprocs.prove_conv;
   7.119 -
   7.120 -val bin_simps = [add_nat_number_of, nat_number_of_add_left,
   7.121 -		 diff_nat_number_of, le_nat_number_of_eq_not_less, 
   7.122 -		 less_nat_number_of, Let_number_of, nat_number_of] @ 
   7.123 -                bin_arith_simps @ bin_rel_simps;
   7.124 -
   7.125 -fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   7.126 -fun prep_pat s = Thm.read_cterm (Theory.sign_of Arith.thy) (s, HOLogic.termT);
   7.127 -val prep_pats = map prep_pat;
   7.128 -
   7.129 -
   7.130 -(*** CancelNumerals simprocs ***)
   7.131 -
   7.132 -val one = mk_numeral 1;
   7.133 -val mk_times = HOLogic.mk_binop "op *";
   7.134 -
   7.135 -fun mk_prod [] = one
   7.136 -  | mk_prod [t] = t
   7.137 -  | mk_prod (t :: ts) = if t = one then mk_prod ts
   7.138 -                        else mk_times (t, mk_prod ts);
   7.139 -
   7.140 -val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
   7.141 -
   7.142 -fun dest_prod t =
   7.143 -      let val (t,u) = dest_times t 
   7.144 -      in  dest_prod t @ dest_prod u  end
   7.145 -      handle TERM _ => [t];
   7.146 -
   7.147 -(*DON'T do the obvious simplifications; that would create special cases*) 
   7.148 -fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
   7.149 -
   7.150 -(*Express t as a product of (possibly) a numeral with other sorted terms*)
   7.151 -fun dest_coeff t =
   7.152 -    let val ts = sort Term.term_ord (dest_prod t)
   7.153 -	val (n, _, ts') = find_first_numeral [] ts
   7.154 -                          handle TERM _ => (1, one, ts)
   7.155 -    in (n, mk_prod ts') end;
   7.156 -
   7.157 -(*Find first coefficient-term THAT MATCHES u*)
   7.158 -fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
   7.159 -  | find_first_coeff past u (t::terms) =
   7.160 -	let val (n,u') = dest_coeff t
   7.161 -	in  if u aconv u' then (n, rev past @ terms)
   7.162 -			  else find_first_coeff (t::past) u terms
   7.163 -	end
   7.164 -	handle TERM _ => find_first_coeff (t::past) u terms;
   7.165 -
   7.166 -
   7.167 -(*Simplify #1*n and n*#1 to n*)
   7.168 -val add_0s = map (rename_numerals NatBin.thy) [add_0, add_0_right];
   7.169 -val mult_1s = map (rename_numerals NatBin.thy) [mult_1, mult_1_right];
   7.170 -
   7.171 -(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
   7.172 -val simplify_meta_eq = 
   7.173 -    Int_Numeral_Simprocs.simplify_meta_eq
   7.174 -         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
   7.175 -	 mult_0, mult_0_right, mult_1, mult_1_right];
   7.176 -
   7.177 -structure CancelNumeralsCommon =
   7.178 -  struct
   7.179 -  val mk_sum    	= mk_sum
   7.180 -  val dest_sum		= dest_Sucs_sum
   7.181 -  val mk_coeff		= mk_coeff
   7.182 -  val dest_coeff	= dest_coeff
   7.183 -  val find_first_coeff	= find_first_coeff []
   7.184 -  val trans_tac          = trans_tac
   7.185 -  val norm_tac = ALLGOALS
   7.186 -                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
   7.187 -                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
   7.188 -                 THEN ALLGOALS (simp_tac
   7.189 -				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
   7.190 -  val numeral_simp_tac	= ALLGOALS
   7.191 -                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
   7.192 -  val simplify_meta_eq  = simplify_meta_eq
   7.193 -  end;
   7.194 -
   7.195 -
   7.196 -structure EqCancelNumerals = CancelNumeralsFun
   7.197 - (open CancelNumeralsCommon
   7.198 -  val prove_conv = prove_conv "nateq_cancel_numerals"
   7.199 -  val mk_bal   = HOLogic.mk_eq
   7.200 -  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   7.201 -  val bal_add1 = nat_eq_add_iff1 RS trans
   7.202 -  val bal_add2 = nat_eq_add_iff2 RS trans
   7.203 -);
   7.204 -
   7.205 -structure LessCancelNumerals = CancelNumeralsFun
   7.206 - (open CancelNumeralsCommon
   7.207 -  val prove_conv = prove_conv "natless_cancel_numerals"
   7.208 -  val mk_bal   = HOLogic.mk_binrel "op <"
   7.209 -  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
   7.210 -  val bal_add1 = nat_less_add_iff1 RS trans
   7.211 -  val bal_add2 = nat_less_add_iff2 RS trans
   7.212 -);
   7.213 -
   7.214 -structure LeCancelNumerals = CancelNumeralsFun
   7.215 - (open CancelNumeralsCommon
   7.216 -  val prove_conv = prove_conv "natle_cancel_numerals"
   7.217 -  val mk_bal   = HOLogic.mk_binrel "op <="
   7.218 -  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
   7.219 -  val bal_add1 = nat_le_add_iff1 RS trans
   7.220 -  val bal_add2 = nat_le_add_iff2 RS trans
   7.221 -);
   7.222 -
   7.223 -structure DiffCancelNumerals = CancelNumeralsFun
   7.224 - (open CancelNumeralsCommon
   7.225 -  val prove_conv = prove_conv "natdiff_cancel_numerals"
   7.226 -  val mk_bal   = HOLogic.mk_binop "op -"
   7.227 -  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
   7.228 -  val bal_add1 = nat_diff_add_eq1 RS trans
   7.229 -  val bal_add2 = nat_diff_add_eq2 RS trans
   7.230 -);
   7.231 -
   7.232 -
   7.233 -val cancel_numerals = 
   7.234 -  map prep_simproc
   7.235 -   [("nateq_cancel_numerals",
   7.236 -     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", 
   7.237 -		"(l::nat) * m = n", "(l::nat) = m * n", 
   7.238 -		"Suc m = n", "m = Suc n"], 
   7.239 -     EqCancelNumerals.proc),
   7.240 -    ("natless_cancel_numerals", 
   7.241 -     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", 
   7.242 -		"(l::nat) * m < n", "(l::nat) < m * n", 
   7.243 -		"Suc m < n", "m < Suc n"], 
   7.244 -     LessCancelNumerals.proc),
   7.245 -    ("natle_cancel_numerals", 
   7.246 -     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", 
   7.247 -		"(l::nat) * m <= n", "(l::nat) <= m * n", 
   7.248 -		"Suc m <= n", "m <= Suc n"], 
   7.249 -     LeCancelNumerals.proc),
   7.250 -    ("natdiff_cancel_numerals", 
   7.251 -     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", 
   7.252 -		"(l::nat) * m - n", "(l::nat) - m * n", 
   7.253 -		"Suc m - n", "m - Suc n"], 
   7.254 -     DiffCancelNumerals.proc)];
   7.255 -
   7.256 -
   7.257 -structure CombineNumeralsData =
   7.258 -  struct
   7.259 -  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
   7.260 -  val dest_sum		= dest_Sucs_sum
   7.261 -  val mk_coeff		= mk_coeff
   7.262 -  val dest_coeff	= dest_coeff
   7.263 -  val left_distrib	= left_add_mult_distrib RS trans
   7.264 -  val prove_conv	= prove_conv "nat_combine_numerals"
   7.265 -  val trans_tac          = trans_tac
   7.266 -  val norm_tac = ALLGOALS
   7.267 -                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
   7.268 -                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
   7.269 -                 THEN ALLGOALS (simp_tac
   7.270 -				(HOL_ss addsimps bin_simps@add_ac@mult_ac))
   7.271 -  val numeral_simp_tac	= ALLGOALS
   7.272 -                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
   7.273 -  val simplify_meta_eq  = simplify_meta_eq
   7.274 -  end;
   7.275 -
   7.276 -structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   7.277 -  
   7.278 -val combine_numerals = 
   7.279 -    prep_simproc ("nat_combine_numerals",
   7.280 -		  prep_pats ["(i::nat) + j", "Suc (i + j)"],
   7.281 -		  CombineNumerals.proc);
   7.282 -
   7.283 -end;
   7.284 -
   7.285 -
   7.286 -Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   7.287 -Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   7.288 -
   7.289 -
   7.290 -(*examples:
   7.291 -print_depth 22;
   7.292 -set timing;
   7.293 -set trace_simp;
   7.294 -fun test s = (Goal s; by (Simp_tac 1)); 
   7.295 -
   7.296 -(*cancel_numerals*)
   7.297 -test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";
   7.298 -test "(#2*length xs < #2*length xs + j)";
   7.299 -test "(#2*length xs < length xs * #2 + j)";
   7.300 -test "#2*u = (u::nat)";
   7.301 -test "#2*u = Suc (u)";
   7.302 -test "(i + j + #12 + (k::nat)) - #15 = y";
   7.303 -test "(i + j + #12 + (k::nat)) - #5 = y";
   7.304 -test "Suc u - #2 = y";
   7.305 -test "Suc (Suc (Suc u)) - #2 = y";
   7.306 -test "(i + j + #2 + (k::nat)) - 1 = y";
   7.307 -test "(i + j + #1 + (k::nat)) - 2 = y";
   7.308 -
   7.309 -test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
   7.310 -test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
   7.311 -test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
   7.312 -test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
   7.313 -test "Suc ((u*v)*#4) - v*#3*u = w";
   7.314 -test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
   7.315 -
   7.316 -test "(i + j + #12 + (k::nat)) = u + #15 + y";
   7.317 -test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
   7.318 -test "(i + j + #12 + (k::nat)) = u + #5 + y";
   7.319 -(*Suc*)
   7.320 -test "(i + j + #12 + k) = Suc (u + y)";
   7.321 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
   7.322 -test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   7.323 -test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
   7.324 -test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   7.325 -test "#2*y + #3*z + #2*u = Suc (u)";
   7.326 -test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
   7.327 -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)";
   7.328 -test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
   7.329 -test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
   7.330 -
   7.331 -(*negative numerals: FAIL*)
   7.332 -test "(i + j + #-23 + (k::nat)) < u + #15 + y";
   7.333 -test "(i + j + #3 + (k::nat)) < u + #-15 + y";
   7.334 -test "(i + j + #-12 + (k::nat)) - #15 = y";
   7.335 -test "(i + j + #12 + (k::nat)) - #-15 = y";
   7.336 -test "(i + j + #-12 + (k::nat)) - #-15 = y";
   7.337 -
   7.338 -(*combine_numerals*)
   7.339 -test "k + #3*k = (u::nat)";
   7.340 -test "Suc (i + #3) = u";
   7.341 -test "Suc (i + j + #3 + k) = u";
   7.342 -test "k + j + #3*k + j = (u::nat)";
   7.343 -test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
   7.344 -test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
   7.345 -(*negative numerals: FAIL*)
   7.346 -test "Suc (i + j + #-3 + k) = u";
   7.347 -*)
   7.348 -
   7.349 -
   7.350 -(*** Prepare linear arithmetic for nat numerals ***)
   7.351 -
   7.352 -let
   7.353 -
   7.354 -(* reduce contradictory <= to False *)
   7.355 -val add_rules =
   7.356 -  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
   7.357 -   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
   7.358 -   le_Suc_number_of,le_number_of_Suc,
   7.359 -   less_Suc_number_of,less_number_of_Suc,
   7.360 -   Suc_eq_number_of,eq_number_of_Suc,
   7.361 -   eq_number_of_0, eq_0_number_of, less_0_number_of,
   7.362 -   nat_number_of, Let_number_of, if_True, if_False];
   7.363 -
   7.364 -val simprocs = [Nat_Times_Assoc.conv,
   7.365 -		Nat_Numeral_Simprocs.combine_numerals]@ 
   7.366 -		Nat_Numeral_Simprocs.cancel_numerals;
   7.367 -
   7.368 -in
   7.369 -LA_Data_Ref.ss_ref := !LA_Data_Ref.ss_ref addsimps add_rules 
   7.370 -                                          addsimps basic_renamed_arith_simps
   7.371 -                                          addsimprocs simprocs
   7.372 -end;
   7.373 -
   7.374 -
   7.375 -
   7.376  (** For simplifying  Suc m - #n **)
   7.377  
   7.378  Goal "#0 < n ==> Suc m - n = m - (n - #1)";
   7.379 @@ -393,8 +28,8 @@
   7.380  by (Simp_tac 1);
   7.381  by (Simp_tac 1);
   7.382  by (asm_full_simp_tac
   7.383 -    (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym, 
   7.384 -				  neg_number_of_bin_pred_iff_0]) 1);
   7.385 +    (simpset_of Int.thy addsimps [diff_nat_number_of, less_0_number_of RS sym,
   7.386 +                                  neg_number_of_bin_pred_iff_0]) 1);
   7.387  qed "Suc_diff_number_of";
   7.388  
   7.389  (* now redundant because of the inverse_fold simproc
   7.390 @@ -405,8 +40,8 @@
   7.391  \        if neg pv then a else f (nat pv))";
   7.392  by (simp_tac
   7.393      (simpset() addsplits [nat.split]
   7.394 -			addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
   7.395 -qed "nat_case_number_of"; 
   7.396 +                        addsimps [Let_def, neg_number_of_bin_pred_iff_0]) 1);
   7.397 +qed "nat_case_number_of";
   7.398  
   7.399  Goal "nat_case a f ((number_of v) + n) = \
   7.400  \      (let pv = number_of (bin_pred v) in \
   7.401 @@ -414,8 +49,8 @@
   7.402  by (stac add_eq_if 1);
   7.403  by (asm_simp_tac
   7.404      (simpset() addsplits [nat.split]
   7.405 -               addsimps [Let_def, neg_imp_number_of_eq_0, 
   7.406 -			 neg_number_of_bin_pred_iff_0]) 1);
   7.407 +               addsimps [Let_def, neg_imp_number_of_eq_0,
   7.408 +                         neg_number_of_bin_pred_iff_0]) 1);
   7.409  qed "nat_case_add_eq_if";
   7.410  
   7.411  Addsimps [nat_case_number_of, nat_case_add_eq_if];
   7.412 @@ -426,9 +61,9 @@
   7.413  \        if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))";
   7.414  by (case_tac "(number_of v)::nat" 1);
   7.415  by (ALLGOALS (asm_simp_tac
   7.416 -	      (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
   7.417 +              (simpset() addsimps [Let_def, neg_number_of_bin_pred_iff_0])));
   7.418  by (asm_full_simp_tac (simpset() addsplits [split_if_asm]) 1);
   7.419 -qed "nat_rec_number_of"; 
   7.420 +qed "nat_rec_number_of";
   7.421  
   7.422  Goal "nat_rec a f (number_of v + n) = \
   7.423  \       (let pv = number_of (bin_pred v) in \
   7.424 @@ -437,9 +72,9 @@
   7.425  by (stac add_eq_if 1);
   7.426  by (asm_simp_tac
   7.427      (simpset() addsplits [nat.split]
   7.428 -               addsimps [Let_def, neg_imp_number_of_eq_0, 
   7.429 -			 neg_number_of_bin_pred_iff_0]) 1);
   7.430 -qed "nat_rec_add_eq_if"; 
   7.431 +               addsimps [Let_def, neg_imp_number_of_eq_0,
   7.432 +                         neg_number_of_bin_pred_iff_0]) 1);
   7.433 +qed "nat_rec_add_eq_if";
   7.434  
   7.435  Addsimps [nat_rec_number_of, nat_rec_add_eq_if];
   7.436  
   7.437 @@ -476,7 +111,7 @@
   7.438  by (Asm_simp_tac 2);
   7.439  by (auto_tac (claset(), simpset() delsimps [mod_less_divisor]));
   7.440  qed "mod2_gr_0";
   7.441 -Addsimps [mod2_gr_0, rename_numerals thy mod2_gr_0];
   7.442 +Addsimps [mod2_gr_0, rename_numerals mod2_gr_0];
   7.443  
   7.444  (** Removal of small numerals: #0, #1 and (in additive positions) #2 **)
   7.445  
     8.1 --- a/src/HOL/Integ/NatSimprocs.thy	Tue Jul 25 00:03:39 2000 +0200
     8.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Tue Jul 25 00:06:46 2000 +0200
     8.3 @@ -1,2 +1,7 @@
     8.4 -theory NatSimprocs = NatBin:
     8.5 +
     8.6 +theory NatSimprocs = NatBin
     8.7 +files "nat_simprocs.ML":
     8.8 +
     8.9 +setup nat_simprocs_setup
    8.10 +
    8.11  end
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/HOL/Integ/int_arith1.ML	Tue Jul 25 00:06:46 2000 +0200
     9.3 @@ -0,0 +1,467 @@
     9.4 +(*  Title:      HOL/Integ/int_arith1.ML
     9.5 +    ID:         $Id$
     9.6 +    Authors:    Larry Paulson and Tobias Nipkow
     9.7 +
     9.8 +Simprocs and decision procedure for linear arithmetic.
     9.9 +*)
    9.10 +
    9.11 +(*** Simprocs for numeric literals ***)
    9.12 +
    9.13 +(** Combining of literal coefficients in sums of products **)
    9.14 +
    9.15 +Goal "(x < y) = (x-y < (#0::int))";
    9.16 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    9.17 +qed "zless_iff_zdiff_zless_0";
    9.18 +
    9.19 +Goal "(x = y) = (x-y = (#0::int))";
    9.20 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    9.21 +qed "eq_iff_zdiff_eq_0";
    9.22 +
    9.23 +Goal "(x <= y) = (x-y <= (#0::int))";
    9.24 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    9.25 +qed "zle_iff_zdiff_zle_0";
    9.26 +
    9.27 +
    9.28 +(** For combine_numerals **)
    9.29 +
    9.30 +Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
    9.31 +by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
    9.32 +qed "left_zadd_zmult_distrib";
    9.33 +
    9.34 +
    9.35 +(** For cancel_numerals **)
    9.36 +
    9.37 +val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
    9.38 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    9.39 +			   zle_iff_zdiff_zle_0] @
    9.40 +		        map (inst "y" "n")
    9.41 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0, 
    9.42 +			   zle_iff_zdiff_zle_0];
    9.43 +
    9.44 +Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
    9.45 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    9.46 +		                     zadd_ac@rel_iff_rel_0_rls) 1);
    9.47 +qed "eq_add_iff1";
    9.48 +
    9.49 +Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
    9.50 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    9.51 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    9.52 +qed "eq_add_iff2";
    9.53 +
    9.54 +Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
    9.55 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    9.56 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    9.57 +qed "less_add_iff1";
    9.58 +
    9.59 +Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
    9.60 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    9.61 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    9.62 +qed "less_add_iff2";
    9.63 +
    9.64 +Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
    9.65 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    9.66 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    9.67 +qed "le_add_iff1";
    9.68 +
    9.69 +Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
    9.70 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
    9.71 +                                     @zadd_ac@rel_iff_rel_0_rls) 1);
    9.72 +qed "le_add_iff2";
    9.73 +
    9.74 +(*To tidy up the result of a simproc.  Only the RHS will be simplified.*)
    9.75 +Goal "u = u' ==> (t==u) == (t==u')";
    9.76 +by Auto_tac;
    9.77 +qed "eq_cong2";
    9.78 +
    9.79 +
    9.80 +structure Int_Numeral_Simprocs =
    9.81 +struct
    9.82 +
    9.83 +(*Utilities*)
    9.84 +
    9.85 +fun mk_numeral n = HOLogic.number_of_const HOLogic.intT $ 
    9.86 +                   NumeralSyntax.mk_bin n;
    9.87 +
    9.88 +(*Decodes a binary INTEGER*)
    9.89 +fun dest_numeral (Const("Numeral.number_of", _) $ w) = 
    9.90 +     (NumeralSyntax.dest_bin w
    9.91 +      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
    9.92 +  | dest_numeral t = raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
    9.93 +
    9.94 +fun find_first_numeral past (t::terms) =
    9.95 +	((dest_numeral t, rev past @ terms)
    9.96 +	 handle TERM _ => find_first_numeral (t::past) terms)
    9.97 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    9.98 +
    9.99 +val zero = mk_numeral 0;
   9.100 +val mk_plus = HOLogic.mk_binop "op +";
   9.101 +
   9.102 +val uminus_const = Const ("uminus", HOLogic.intT --> HOLogic.intT);
   9.103 +
   9.104 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   9.105 +fun mk_sum []        = zero
   9.106 +  | mk_sum [t,u]     = mk_plus (t, u)
   9.107 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   9.108 +
   9.109 +(*this version ALWAYS includes a trailing zero*)
   9.110 +fun long_mk_sum []        = zero
   9.111 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   9.112 +
   9.113 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.intT;
   9.114 +
   9.115 +(*decompose additions AND subtractions as a sum*)
   9.116 +fun dest_summing (pos, Const ("op +", _) $ t $ u, ts) =
   9.117 +        dest_summing (pos, t, dest_summing (pos, u, ts))
   9.118 +  | dest_summing (pos, Const ("op -", _) $ t $ u, ts) =
   9.119 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
   9.120 +  | dest_summing (pos, t, ts) =
   9.121 +	if pos then t::ts else uminus_const$t :: ts;
   9.122 +
   9.123 +fun dest_sum t = dest_summing (true, t, []);
   9.124 +
   9.125 +val mk_diff = HOLogic.mk_binop "op -";
   9.126 +val dest_diff = HOLogic.dest_bin "op -" HOLogic.intT;
   9.127 +
   9.128 +val one = mk_numeral 1;
   9.129 +val mk_times = HOLogic.mk_binop "op *";
   9.130 +
   9.131 +fun mk_prod [] = one
   9.132 +  | mk_prod [t] = t
   9.133 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
   9.134 +                        else mk_times (t, mk_prod ts);
   9.135 +
   9.136 +val dest_times = HOLogic.dest_bin "op *" HOLogic.intT;
   9.137 +
   9.138 +fun dest_prod t =
   9.139 +      let val (t,u) = dest_times t 
   9.140 +      in  dest_prod t @ dest_prod u  end
   9.141 +      handle TERM _ => [t];
   9.142 +
   9.143 +(*DON'T do the obvious simplifications; that would create special cases*) 
   9.144 +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
   9.145 +
   9.146 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   9.147 +fun dest_coeff sign (Const ("uminus", _) $ t) = dest_coeff (~sign) t
   9.148 +  | dest_coeff sign t =
   9.149 +    let val ts = sort Term.term_ord (dest_prod t)
   9.150 +	val (n, ts') = find_first_numeral [] ts
   9.151 +                          handle TERM _ => (1, ts)
   9.152 +    in (sign*n, mk_prod ts') end;
   9.153 +
   9.154 +(*Find first coefficient-term THAT MATCHES u*)
   9.155 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", []) 
   9.156 +  | find_first_coeff past u (t::terms) =
   9.157 +	let val (n,u') = dest_coeff 1 t
   9.158 +	in  if u aconv u' then (n, rev past @ terms)
   9.159 +			  else find_first_coeff (t::past) u terms
   9.160 +	end
   9.161 +	handle TERM _ => find_first_coeff (t::past) u terms;
   9.162 +
   9.163 +
   9.164 +(*Simplify #1*n and n*#1 to n*)
   9.165 +val add_0s = [zadd_0, zadd_0_right];
   9.166 +val mult_1s = [zmult_1, zmult_1_right, zmult_minus1, zmult_minus1_right];
   9.167 +
   9.168 +(*To perform binary arithmetic*)
   9.169 +val bin_simps = [add_number_of_left] @ bin_arith_simps @ bin_rel_simps;
   9.170 +
   9.171 +(*To evaluate binary negations of coefficients*)
   9.172 +val zminus_simps = NCons_simps @
   9.173 +                   [number_of_minus RS sym, 
   9.174 +		    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   9.175 +		    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   9.176 +
   9.177 +(*To let us treat subtraction as addition*)
   9.178 +val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
   9.179 +
   9.180 +(*Apply the given rewrite (if present) just once*)
   9.181 +fun trans_tac None      = all_tac
   9.182 +  | trans_tac (Some th) = ALLGOALS (rtac (th RS trans));
   9.183 +
   9.184 +fun prove_conv name tacs sg (t, u) =
   9.185 +  if t aconv u then None
   9.186 +  else
   9.187 +  let val ct = cterm_of sg (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u)))
   9.188 +  in Some
   9.189 +     (prove_goalw_cterm [] ct (K tacs)
   9.190 +      handle ERROR => error 
   9.191 +	  ("The error(s) above occurred while trying to prove " ^
   9.192 +	   string_of_cterm ct ^ "\nInternal failure of simproc " ^ name))
   9.193 +  end;
   9.194 +
   9.195 +fun simplify_meta_eq rules =
   9.196 +    mk_meta_eq o
   9.197 +    simplify (HOL_basic_ss addeqcongs[eq_cong2] addsimps rules)
   9.198 +
   9.199 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
   9.200 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.termT);
   9.201 +val prep_pats = map prep_pat;
   9.202 +
   9.203 +structure CancelNumeralsCommon =
   9.204 +  struct
   9.205 +  val mk_sum    	= mk_sum
   9.206 +  val dest_sum		= dest_sum
   9.207 +  val mk_coeff		= mk_coeff
   9.208 +  val dest_coeff	= dest_coeff 1
   9.209 +  val find_first_coeff	= find_first_coeff []
   9.210 +  val trans_tac         = trans_tac
   9.211 +  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   9.212 +                                                     zminus_simps@zadd_ac))
   9.213 +                 THEN ALLGOALS
   9.214 +                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
   9.215 +                                               bin_simps@zadd_ac@zmult_ac))
   9.216 +  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   9.217 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   9.218 +  end;
   9.219 +
   9.220 +
   9.221 +structure EqCancelNumerals = CancelNumeralsFun
   9.222 + (open CancelNumeralsCommon
   9.223 +  val prove_conv = prove_conv "inteq_cancel_numerals"
   9.224 +  val mk_bal   = HOLogic.mk_eq
   9.225 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.intT
   9.226 +  val bal_add1 = eq_add_iff1 RS trans
   9.227 +  val bal_add2 = eq_add_iff2 RS trans
   9.228 +);
   9.229 +
   9.230 +structure LessCancelNumerals = CancelNumeralsFun
   9.231 + (open CancelNumeralsCommon
   9.232 +  val prove_conv = prove_conv "intless_cancel_numerals"
   9.233 +  val mk_bal   = HOLogic.mk_binrel "op <"
   9.234 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.intT
   9.235 +  val bal_add1 = less_add_iff1 RS trans
   9.236 +  val bal_add2 = less_add_iff2 RS trans
   9.237 +);
   9.238 +
   9.239 +structure LeCancelNumerals = CancelNumeralsFun
   9.240 + (open CancelNumeralsCommon
   9.241 +  val prove_conv = prove_conv "intle_cancel_numerals"
   9.242 +  val mk_bal   = HOLogic.mk_binrel "op <="
   9.243 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.intT
   9.244 +  val bal_add1 = le_add_iff1 RS trans
   9.245 +  val bal_add2 = le_add_iff2 RS trans
   9.246 +);
   9.247 +
   9.248 +val cancel_numerals = 
   9.249 +  map prep_simproc
   9.250 +   [("inteq_cancel_numerals",
   9.251 +     prep_pats ["(l::int) + m = n", "(l::int) = m + n", 
   9.252 +		"(l::int) - m = n", "(l::int) = m - n", 
   9.253 +		"(l::int) * m = n", "(l::int) = m * n"], 
   9.254 +     EqCancelNumerals.proc),
   9.255 +    ("intless_cancel_numerals", 
   9.256 +     prep_pats ["(l::int) + m < n", "(l::int) < m + n", 
   9.257 +		"(l::int) - m < n", "(l::int) < m - n", 
   9.258 +		"(l::int) * m < n", "(l::int) < m * n"], 
   9.259 +     LessCancelNumerals.proc),
   9.260 +    ("intle_cancel_numerals", 
   9.261 +     prep_pats ["(l::int) + m <= n", "(l::int) <= m + n", 
   9.262 +		"(l::int) - m <= n", "(l::int) <= m - n", 
   9.263 +		"(l::int) * m <= n", "(l::int) <= m * n"], 
   9.264 +     LeCancelNumerals.proc)];
   9.265 +
   9.266 +
   9.267 +structure CombineNumeralsData =
   9.268 +  struct
   9.269 +  val mk_sum    	= long_mk_sum    (*to work for e.g. #2*x + #3*x *)
   9.270 +  val dest_sum		= dest_sum
   9.271 +  val mk_coeff		= mk_coeff
   9.272 +  val dest_coeff	= dest_coeff 1
   9.273 +  val left_distrib	= left_zadd_zmult_distrib RS trans
   9.274 +  val prove_conv	= prove_conv "int_combine_numerals"
   9.275 +  val trans_tac          = trans_tac
   9.276 +  val norm_tac = ALLGOALS
   9.277 +                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@diff_simps@
   9.278 +                                              zminus_simps@zadd_ac))
   9.279 +                 THEN ALLGOALS
   9.280 +                    (simp_tac (HOL_ss addsimps [zmult_zminus_right RS sym]@
   9.281 +                                               bin_simps@zadd_ac@zmult_ac))
   9.282 +  val numeral_simp_tac	= ALLGOALS 
   9.283 +                    (simp_tac (HOL_ss addsimps add_0s@bin_simps))
   9.284 +  val simplify_meta_eq  = simplify_meta_eq (add_0s@mult_1s)
   9.285 +  end;
   9.286 +
   9.287 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   9.288 +  
   9.289 +val combine_numerals = 
   9.290 +    prep_simproc ("int_combine_numerals",
   9.291 +		  prep_pats ["(i::int) + j", "(i::int) - j"],
   9.292 +		  CombineNumerals.proc);
   9.293 +
   9.294 +end;
   9.295 +
   9.296 +Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   9.297 +Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
   9.298 +
   9.299 +(*The Abel_Cancel simprocs are now obsolete*)
   9.300 +Delsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
   9.301 +
   9.302 +(*examples:
   9.303 +print_depth 22;
   9.304 +set timing;
   9.305 +set trace_simp;
   9.306 +fun test s = (Goal s; by (Simp_tac 1)); 
   9.307 +
   9.308 +test "l + #2 + #2 + #2 + (l + #2) + (oo + #2) = (uu::int)";
   9.309 +
   9.310 +test "#2*u = (u::int)";
   9.311 +test "(i + j + #12 + (k::int)) - #15 = y";
   9.312 +test "(i + j + #12 + (k::int)) - #5 = y";
   9.313 +
   9.314 +test "y - b < (b::int)";
   9.315 +test "y - (#3*b + c) < (b::int) - #2*c";
   9.316 +
   9.317 +test "(#2*x - (u*v) + y) - v*#3*u = (w::int)";
   9.318 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u*#4 = (w::int)";
   9.319 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::int)";
   9.320 +test "u*v - (x*u*v + (u*v)*#4 + y) = (w::int)";
   9.321 +
   9.322 +test "(i + j + #12 + (k::int)) = u + #15 + y";
   9.323 +test "(i + j*#2 + #12 + (k::int)) = j + #5 + y";
   9.324 +
   9.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)";
   9.326 +
   9.327 +test "a + -(b+c) + b = (d::int)";
   9.328 +test "a + -(b+c) - b = (d::int)";
   9.329 +
   9.330 +(*negative numerals*)
   9.331 +test "(i + j + #-2 + (k::int)) - (u + #5 + y) = zz";
   9.332 +test "(i + j + #-3 + (k::int)) < u + #5 + y";
   9.333 +test "(i + j + #3 + (k::int)) < u + #-6 + y";
   9.334 +test "(i + j + #-12 + (k::int)) - #15 = y";
   9.335 +test "(i + j + #12 + (k::int)) - #-15 = y";
   9.336 +test "(i + j + #-12 + (k::int)) - #-15 = y";
   9.337 +*)
   9.338 +
   9.339 +
   9.340 +(** Constant folding for integer plus and times **)
   9.341 +
   9.342 +(*We do not need
   9.343 +    structure Nat_Plus_Assoc = Assoc_Fold (Nat_Plus_Assoc_Data);
   9.344 +    structure Int_Plus_Assoc = Assoc_Fold (Int_Plus_Assoc_Data);
   9.345 +  because combine_numerals does the same thing*)
   9.346 +
   9.347 +structure Int_Times_Assoc_Data : ASSOC_FOLD_DATA =
   9.348 +struct
   9.349 +  val ss		= HOL_ss
   9.350 +  val eq_reflection	= eq_reflection
   9.351 +  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
   9.352 +  val T	     = HOLogic.intT
   9.353 +  val plus   = Const ("op *", [HOLogic.intT,HOLogic.intT] ---> HOLogic.intT);
   9.354 +  val add_ac = zmult_ac
   9.355 +end;
   9.356 +
   9.357 +structure Int_Times_Assoc = Assoc_Fold (Int_Times_Assoc_Data);
   9.358 +
   9.359 +Addsimprocs [Int_Times_Assoc.conv];
   9.360 +
   9.361 +
   9.362 +(** The same for the naturals **)
   9.363 +
   9.364 +structure Nat_Times_Assoc_Data : ASSOC_FOLD_DATA =
   9.365 +struct
   9.366 +  val ss		= HOL_ss
   9.367 +  val eq_reflection	= eq_reflection
   9.368 +  val sg_ref = Sign.self_ref (Theory.sign_of (the_context ()))
   9.369 +  val T	     = HOLogic.natT
   9.370 +  val plus   = Const ("op *", [HOLogic.natT,HOLogic.natT] ---> HOLogic.natT);
   9.371 +  val add_ac = mult_ac
   9.372 +end;
   9.373 +
   9.374 +structure Nat_Times_Assoc = Assoc_Fold (Nat_Times_Assoc_Data);
   9.375 +
   9.376 +Addsimprocs [Nat_Times_Assoc.conv];
   9.377 +
   9.378 +
   9.379 +(*** decision procedure for linear arithmetic ***)
   9.380 +
   9.381 +(*---------------------------------------------------------------------------*)
   9.382 +(* Linear arithmetic                                                         *)
   9.383 +(*---------------------------------------------------------------------------*)
   9.384 +
   9.385 +(*
   9.386 +Instantiation of the generic linear arithmetic package for int.
   9.387 +*)
   9.388 +
   9.389 +(* Update parameters of arithmetic prover *)
   9.390 +local
   9.391 +
   9.392 +(* reduce contradictory <= to False *)
   9.393 +val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
   9.394 +                [int_0, zadd_0, zadd_0_right, zdiff_def,
   9.395 +		 zadd_zminus_inverse, zadd_zminus_inverse2, 
   9.396 +		 zmult_0, zmult_0_right, 
   9.397 +		 zmult_1, zmult_1_right, 
   9.398 +		 zmult_minus1, zmult_minus1_right,
   9.399 +		 zminus_zadd_distrib, zminus_zminus];
   9.400 +
   9.401 +val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
   9.402 +               Int_Numeral_Simprocs.cancel_numerals;
   9.403 +
   9.404 +val add_mono_thms_int =
   9.405 +  map (fn s => prove_goal (the_context ()) s
   9.406 +                 (fn prems => [cut_facts_tac prems 1,
   9.407 +                      asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
   9.408 +    ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
   9.409 +     "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
   9.410 +     "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
   9.411 +     "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
   9.412 +    ];
   9.413 +
   9.414 +in
   9.415 +
   9.416 +val int_arith_setup =
   9.417 + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
   9.418 +   {add_mono_thms = add_mono_thms @ add_mono_thms_int,
   9.419 +    lessD = lessD @ [add1_zle_eq RS iffD2],
   9.420 +    simpset = simpset addsimps add_rules
   9.421 +                      addsimprocs simprocs
   9.422 +                      addcongs [if_weak_cong]}),
   9.423 +  arith_discrete ("IntDef.int", true)];
   9.424 +
   9.425 +end;
   9.426 +
   9.427 +let
   9.428 +val int_arith_simproc_pats =
   9.429 +  map (fn s => Thm.read_cterm (Theory.sign_of (the_context())) (s, HOLogic.boolT))
   9.430 +      ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
   9.431 +
   9.432 +val fast_int_arith_simproc = mk_simproc
   9.433 +  "fast_int_arith" int_arith_simproc_pats Fast_Arith.lin_arith_prover;
   9.434 +in
   9.435 +Addsimprocs [fast_int_arith_simproc]
   9.436 +end;
   9.437 +
   9.438 +(* Some test data
   9.439 +Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   9.440 +by (fast_arith_tac 1);
   9.441 +Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
   9.442 +by (fast_arith_tac 1);
   9.443 +Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
   9.444 +by (fast_arith_tac 1);
   9.445 +Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
   9.446 +by (fast_arith_tac 1);
   9.447 +Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
   9.448 +\     ==> a+a <= j+j";
   9.449 +by (fast_arith_tac 1);
   9.450 +Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
   9.451 +\     ==> a+a - - #-1 < j+j - #3";
   9.452 +by (fast_arith_tac 1);
   9.453 +Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   9.454 +by (arith_tac 1);
   9.455 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   9.456 +\     ==> a <= l";
   9.457 +by (fast_arith_tac 1);
   9.458 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   9.459 +\     ==> a+a+a+a <= l+l+l+l";
   9.460 +by (fast_arith_tac 1);
   9.461 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   9.462 +\     ==> a+a+a+a+a <= l+l+l+l+i";
   9.463 +by (fast_arith_tac 1);
   9.464 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   9.465 +\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   9.466 +by (fast_arith_tac 1);
   9.467 +Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   9.468 +\     ==> #6*a <= #5*l+i";
   9.469 +by (fast_arith_tac 1);
   9.470 +*)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/HOL/Integ/int_arith2.ML	Tue Jul 25 00:06:46 2000 +0200
    10.3 @@ -0,0 +1,107 @@
    10.4 +(*  Title:      HOL/Integ/int_arith2.ML
    10.5 +    ID:         $Id$
    10.6 +    Authors:    Larry Paulson and Tobias Nipkow
    10.7 +*)
    10.8 +
    10.9 +(** Simplification of inequalities involving numerical constants **)
   10.10 +
   10.11 +Goal "(w <= z - (#1::int)) = (w<(z::int))";
   10.12 +by (arith_tac 1);
   10.13 +qed "zle_diff1_eq";
   10.14 +Addsimps [zle_diff1_eq];
   10.15 +
   10.16 +Goal "(w < z + #1) = (w<=(z::int))";
   10.17 +by (arith_tac 1);
   10.18 +qed "zle_add1_eq_le";
   10.19 +Addsimps [zle_add1_eq_le];
   10.20 +
   10.21 +Goal "(z = z + w) = (w = (#0::int))";
   10.22 +by (arith_tac 1);
   10.23 +qed "zadd_left_cancel0";
   10.24 +Addsimps [zadd_left_cancel0];
   10.25 +
   10.26 +
   10.27 +(* nat *)
   10.28 +
   10.29 +Goal "#0 <= z ==> int (nat z) = z"; 
   10.30 +by (asm_full_simp_tac
   10.31 +    (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
   10.32 +qed "nat_0_le"; 
   10.33 +
   10.34 +Goal "z <= #0 ==> nat z = 0"; 
   10.35 +by (case_tac "z = #0" 1);
   10.36 +by (asm_simp_tac (simpset() addsimps [nat_le_int0]) 1); 
   10.37 +by (asm_full_simp_tac 
   10.38 +    (simpset() addsimps [neg_eq_less_0, neg_nat, linorder_neq_iff]) 1);
   10.39 +qed "nat_le_0"; 
   10.40 +
   10.41 +Addsimps [nat_0_le, nat_le_0];
   10.42 +
   10.43 +val [major,minor] = Goal "[| #0 <= z;  !!m. z = int m ==> P |] ==> P"; 
   10.44 +by (rtac (major RS nat_0_le RS sym RS minor) 1);
   10.45 +qed "nonneg_eq_int"; 
   10.46 +
   10.47 +Goal "#0 <= w ==> (nat w = m) = (w = int m)";
   10.48 +by Auto_tac;
   10.49 +qed "nat_eq_iff";
   10.50 +
   10.51 +Goal "#0 <= w ==> (m = nat w) = (w = int m)";
   10.52 +by Auto_tac;
   10.53 +qed "nat_eq_iff2";
   10.54 +
   10.55 +Goal "#0 <= w ==> (nat w < m) = (w < int m)";
   10.56 +by (rtac iffI 1);
   10.57 +by (asm_full_simp_tac 
   10.58 +    (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
   10.59 +by (etac (nat_0_le RS subst) 1);
   10.60 +by (Simp_tac 1);
   10.61 +qed "nat_less_iff";
   10.62 +
   10.63 +
   10.64 +(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
   10.65 +Addsimps [int_0, int_Suc, symmetric zdiff_def];
   10.66 +
   10.67 +Goal "nat #0 = 0";
   10.68 +by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   10.69 +qed "nat_0";
   10.70 +
   10.71 +Goal "nat #1 = 1";
   10.72 +by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   10.73 +qed "nat_1";
   10.74 +
   10.75 +Goal "nat #2 = 2";
   10.76 +by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
   10.77 +qed "nat_2";
   10.78 +
   10.79 +Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
   10.80 +by (case_tac "neg z" 1);
   10.81 +by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   10.82 +by (auto_tac (claset() addIs [zless_trans], 
   10.83 +	      simpset() addsimps [neg_eq_less_0, zle_def]));
   10.84 +qed "nat_less_eq_zless";
   10.85 +
   10.86 +Goal "#0 < w | #0 <= z ==> (nat w <= nat z) = (w<=z)";
   10.87 +by (auto_tac (claset(), 
   10.88 +	      simpset() addsimps [linorder_not_less RS sym, 
   10.89 +				  zless_nat_conj]));
   10.90 +qed "nat_le_eq_zle";
   10.91 +
   10.92 +(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
   10.93 +Goal "n<=m --> int m - int n = int (m-n)";
   10.94 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   10.95 +by Auto_tac;
   10.96 +qed_spec_mp "zdiff_int";
   10.97 +
   10.98 +
   10.99 +(*** abs: absolute value, as an integer ****)
  10.100 +
  10.101 +(* Simpler: use zabs_def as rewrite rule;
  10.102 +   but arith_tac is not parameterized by such simp rules
  10.103 +*)
  10.104 +
  10.105 +Goalw [zabs_def]
  10.106 + "P(abs(i::int)) = ((#0 <= i --> P i) & (i < #0 --> P(-i)))";
  10.107 +by(Simp_tac 1);
  10.108 +qed "zabs_split";
  10.109 +
  10.110 +(*continued in IntArith.ML ...*)
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Tue Jul 25 00:06:46 2000 +0200
    11.3 @@ -0,0 +1,375 @@
    11.4 +(*  Title:      HOL/nat_simprocs.ML
    11.5 +    ID:         $Id$
    11.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    11.7 +    Copyright   2000  University of Cambridge
    11.8 +
    11.9 +Simprocs for nat numerals.
   11.10 +*)
   11.11 +
   11.12 +Goal "number_of v + (number_of v' + (k::nat)) = \
   11.13 +\        (if neg (number_of v) then number_of v' + k \
   11.14 +\         else if neg (number_of v') then number_of v + k \
   11.15 +\         else number_of (bin_add v v') + k)";
   11.16 +by (Simp_tac 1);
   11.17 +qed "nat_number_of_add_left";
   11.18 +
   11.19 +
   11.20 +(** For combine_numerals **)
   11.21 +
   11.22 +Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
   11.23 +by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
   11.24 +qed "left_add_mult_distrib";
   11.25 +
   11.26 +
   11.27 +(** For cancel_numerals **)
   11.28 +
   11.29 +Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
   11.30 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]
   11.31 +                            addsimps [add_mult_distrib]) 1);
   11.32 +qed "nat_diff_add_eq1";
   11.33 +
   11.34 +Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
   11.35 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]
   11.36 +                            addsimps [add_mult_distrib]) 1);
   11.37 +qed "nat_diff_add_eq2";
   11.38 +
   11.39 +Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
   11.40 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
   11.41 +                                  addsimps [add_mult_distrib]));
   11.42 +qed "nat_eq_add_iff1";
   11.43 +
   11.44 +Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
   11.45 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
   11.46 +                                  addsimps [add_mult_distrib]));
   11.47 +qed "nat_eq_add_iff2";
   11.48 +
   11.49 +Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
   11.50 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
   11.51 +                                  addsimps [add_mult_distrib]));
   11.52 +qed "nat_less_add_iff1";
   11.53 +
   11.54 +Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
   11.55 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
   11.56 +                                  addsimps [add_mult_distrib]));
   11.57 +qed "nat_less_add_iff2";
   11.58 +
   11.59 +Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
   11.60 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
   11.61 +                                  addsimps [add_mult_distrib]));
   11.62 +qed "nat_le_add_iff1";
   11.63 +
   11.64 +Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
   11.65 +by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
   11.66 +                                  addsimps [add_mult_distrib]));
   11.67 +qed "nat_le_add_iff2";
   11.68 +
   11.69 +
   11.70 +structure Nat_Numeral_Simprocs =
   11.71 +struct
   11.72 +
   11.73 +(*Utilities*)
   11.74 +
   11.75 +fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $
   11.76 +                   NumeralSyntax.mk_bin n;
   11.77 +
   11.78 +(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
   11.79 +fun dest_numeral (Const ("0", _)) = 0
   11.80 +  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
   11.81 +  | dest_numeral (Const("Numeral.number_of", _) $ w) =
   11.82 +      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
   11.83 +       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
   11.84 +  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
   11.85 +
   11.86 +fun find_first_numeral past (t::terms) =
   11.87 +        ((dest_numeral t, t, rev past @ terms)
   11.88 +         handle TERM _ => find_first_numeral (t::past) terms)
   11.89 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
   11.90 +
   11.91 +val zero = mk_numeral 0;
   11.92 +val mk_plus = HOLogic.mk_binop "op +";
   11.93 +
   11.94 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   11.95 +fun mk_sum []        = zero
   11.96 +  | mk_sum [t,u]     = mk_plus (t, u)
   11.97 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   11.98 +
   11.99 +(*this version ALWAYS includes a trailing zero*)
  11.100 +fun long_mk_sum []        = zero
  11.101 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
  11.102 +
  11.103 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
  11.104 +
  11.105 +(*extract the outer Sucs from a term and convert them to a binary numeral*)
  11.106 +fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
  11.107 +  | dest_Sucs (0, t) = t
  11.108 +  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
  11.109 +
  11.110 +fun dest_sum t =
  11.111 +      let val (t,u) = dest_plus t
  11.112 +      in  dest_sum t @ dest_sum u  end
  11.113 +      handle TERM _ => [t];
  11.114 +
  11.115 +fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
  11.116 +
  11.117 +val trans_tac = Int_Numeral_Simprocs.trans_tac;
  11.118 +
  11.119 +val prove_conv = Int_Numeral_Simprocs.prove_conv;
  11.120 +
  11.121 +val bin_simps = [add_nat_number_of, nat_number_of_add_left,
  11.122 +                 diff_nat_number_of, le_nat_number_of_eq_not_less,
  11.123 +                 less_nat_number_of, Let_number_of, nat_number_of] @
  11.124 +                bin_arith_simps @ bin_rel_simps;
  11.125 +
  11.126 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
  11.127 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
  11.128 +val prep_pats = map prep_pat;
  11.129 +
  11.130 +
  11.131 +(*** CancelNumerals simprocs ***)
  11.132 +
  11.133 +val one = mk_numeral 1;
  11.134 +val mk_times = HOLogic.mk_binop "op *";
  11.135 +
  11.136 +fun mk_prod [] = one
  11.137 +  | mk_prod [t] = t
  11.138 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
  11.139 +                        else mk_times (t, mk_prod ts);
  11.140 +
  11.141 +val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
  11.142 +
  11.143 +fun dest_prod t =
  11.144 +      let val (t,u) = dest_times t
  11.145 +      in  dest_prod t @ dest_prod u  end
  11.146 +      handle TERM _ => [t];
  11.147 +
  11.148 +(*DON'T do the obvious simplifications; that would create special cases*)
  11.149 +fun mk_coeff (k, ts) = mk_times (mk_numeral k, ts);
  11.150 +
  11.151 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
  11.152 +fun dest_coeff t =
  11.153 +    let val ts = sort Term.term_ord (dest_prod t)
  11.154 +        val (n, _, ts') = find_first_numeral [] ts
  11.155 +                          handle TERM _ => (1, one, ts)
  11.156 +    in (n, mk_prod ts') end;
  11.157 +
  11.158 +(*Find first coefficient-term THAT MATCHES u*)
  11.159 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
  11.160 +  | find_first_coeff past u (t::terms) =
  11.161 +        let val (n,u') = dest_coeff t
  11.162 +        in  if u aconv u' then (n, rev past @ terms)
  11.163 +                          else find_first_coeff (t::past) u terms
  11.164 +        end
  11.165 +        handle TERM _ => find_first_coeff (t::past) u terms;
  11.166 +
  11.167 +
  11.168 +(*Simplify #1*n and n*#1 to n*)
  11.169 +val add_0s = map rename_numerals [add_0, add_0_right];
  11.170 +val mult_1s = map rename_numerals [mult_1, mult_1_right];
  11.171 +
  11.172 +(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
  11.173 +val simplify_meta_eq =
  11.174 +    Int_Numeral_Simprocs.simplify_meta_eq
  11.175 +         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
  11.176 +         mult_0, mult_0_right, mult_1, mult_1_right];
  11.177 +
  11.178 +structure CancelNumeralsCommon =
  11.179 +  struct
  11.180 +  val mk_sum            = mk_sum
  11.181 +  val dest_sum          = dest_Sucs_sum
  11.182 +  val mk_coeff          = mk_coeff
  11.183 +  val dest_coeff        = dest_coeff
  11.184 +  val find_first_coeff  = find_first_coeff []
  11.185 +  val trans_tac          = trans_tac
  11.186 +  val norm_tac = ALLGOALS
  11.187 +                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
  11.188 +                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
  11.189 +                 THEN ALLGOALS (simp_tac
  11.190 +                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
  11.191 +  val numeral_simp_tac  = ALLGOALS
  11.192 +                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
  11.193 +  val simplify_meta_eq  = simplify_meta_eq
  11.194 +  end;
  11.195 +
  11.196 +
  11.197 +structure EqCancelNumerals = CancelNumeralsFun
  11.198 + (open CancelNumeralsCommon
  11.199 +  val prove_conv = prove_conv "nateq_cancel_numerals"
  11.200 +  val mk_bal   = HOLogic.mk_eq
  11.201 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
  11.202 +  val bal_add1 = nat_eq_add_iff1 RS trans
  11.203 +  val bal_add2 = nat_eq_add_iff2 RS trans
  11.204 +);
  11.205 +
  11.206 +structure LessCancelNumerals = CancelNumeralsFun
  11.207 + (open CancelNumeralsCommon
  11.208 +  val prove_conv = prove_conv "natless_cancel_numerals"
  11.209 +  val mk_bal   = HOLogic.mk_binrel "op <"
  11.210 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
  11.211 +  val bal_add1 = nat_less_add_iff1 RS trans
  11.212 +  val bal_add2 = nat_less_add_iff2 RS trans
  11.213 +);
  11.214 +
  11.215 +structure LeCancelNumerals = CancelNumeralsFun
  11.216 + (open CancelNumeralsCommon
  11.217 +  val prove_conv = prove_conv "natle_cancel_numerals"
  11.218 +  val mk_bal   = HOLogic.mk_binrel "op <="
  11.219 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
  11.220 +  val bal_add1 = nat_le_add_iff1 RS trans
  11.221 +  val bal_add2 = nat_le_add_iff2 RS trans
  11.222 +);
  11.223 +
  11.224 +structure DiffCancelNumerals = CancelNumeralsFun
  11.225 + (open CancelNumeralsCommon
  11.226 +  val prove_conv = prove_conv "natdiff_cancel_numerals"
  11.227 +  val mk_bal   = HOLogic.mk_binop "op -"
  11.228 +  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
  11.229 +  val bal_add1 = nat_diff_add_eq1 RS trans
  11.230 +  val bal_add2 = nat_diff_add_eq2 RS trans
  11.231 +);
  11.232 +
  11.233 +
  11.234 +val cancel_numerals =
  11.235 +  map prep_simproc
  11.236 +   [("nateq_cancel_numerals",
  11.237 +     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n",
  11.238 +                "(l::nat) * m = n", "(l::nat) = m * n",
  11.239 +                "Suc m = n", "m = Suc n"],
  11.240 +     EqCancelNumerals.proc),
  11.241 +    ("natless_cancel_numerals",
  11.242 +     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n",
  11.243 +                "(l::nat) * m < n", "(l::nat) < m * n",
  11.244 +                "Suc m < n", "m < Suc n"],
  11.245 +     LessCancelNumerals.proc),
  11.246 +    ("natle_cancel_numerals",
  11.247 +     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n",
  11.248 +                "(l::nat) * m <= n", "(l::nat) <= m * n",
  11.249 +                "Suc m <= n", "m <= Suc n"],
  11.250 +     LeCancelNumerals.proc),
  11.251 +    ("natdiff_cancel_numerals",
  11.252 +     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)",
  11.253 +                "(l::nat) * m - n", "(l::nat) - m * n",
  11.254 +                "Suc m - n", "m - Suc n"],
  11.255 +     DiffCancelNumerals.proc)];
  11.256 +
  11.257 +
  11.258 +structure CombineNumeralsData =
  11.259 +  struct
  11.260 +  val mk_sum            = long_mk_sum    (*to work for e.g. #2*x + #3*x *)
  11.261 +  val dest_sum          = dest_Sucs_sum
  11.262 +  val mk_coeff          = mk_coeff
  11.263 +  val dest_coeff        = dest_coeff
  11.264 +  val left_distrib      = left_add_mult_distrib RS trans
  11.265 +  val prove_conv        = prove_conv "nat_combine_numerals"
  11.266 +  val trans_tac          = trans_tac
  11.267 +  val norm_tac = ALLGOALS
  11.268 +                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
  11.269 +                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
  11.270 +                 THEN ALLGOALS (simp_tac
  11.271 +                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
  11.272 +  val numeral_simp_tac  = ALLGOALS
  11.273 +                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
  11.274 +  val simplify_meta_eq  = simplify_meta_eq
  11.275 +  end;
  11.276 +
  11.277 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
  11.278 +
  11.279 +val combine_numerals =
  11.280 +    prep_simproc ("nat_combine_numerals",
  11.281 +                  prep_pats ["(i::nat) + j", "Suc (i + j)"],
  11.282 +                  CombineNumerals.proc);
  11.283 +
  11.284 +end;
  11.285 +
  11.286 +
  11.287 +Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
  11.288 +Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
  11.289 +
  11.290 +
  11.291 +(*examples:
  11.292 +print_depth 22;
  11.293 +set timing;
  11.294 +set trace_simp;
  11.295 +fun test s = (Goal s; by (Simp_tac 1));
  11.296 +
  11.297 +(*cancel_numerals*)
  11.298 +test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";
  11.299 +test "(#2*length xs < #2*length xs + j)";
  11.300 +test "(#2*length xs < length xs * #2 + j)";
  11.301 +test "#2*u = (u::nat)";
  11.302 +test "#2*u = Suc (u)";
  11.303 +test "(i + j + #12 + (k::nat)) - #15 = y";
  11.304 +test "(i + j + #12 + (k::nat)) - #5 = y";
  11.305 +test "Suc u - #2 = y";
  11.306 +test "Suc (Suc (Suc u)) - #2 = y";
  11.307 +test "(i + j + #2 + (k::nat)) - 1 = y";
  11.308 +test "(i + j + #1 + (k::nat)) - 2 = y";
  11.309 +
  11.310 +test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
  11.311 +test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
  11.312 +test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
  11.313 +test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
  11.314 +test "Suc ((u*v)*#4) - v*#3*u = w";
  11.315 +test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
  11.316 +
  11.317 +test "(i + j + #12 + (k::nat)) = u + #15 + y";
  11.318 +test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
  11.319 +test "(i + j + #12 + (k::nat)) = u + #5 + y";
  11.320 +(*Suc*)
  11.321 +test "(i + j + #12 + k) = Suc (u + y)";
  11.322 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
  11.323 +test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
  11.324 +test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
  11.325 +test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
  11.326 +test "#2*y + #3*z + #2*u = Suc (u)";
  11.327 +test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
  11.328 +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)";
  11.329 +test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
  11.330 +test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
  11.331 +
  11.332 +(*negative numerals: FAIL*)
  11.333 +test "(i + j + #-23 + (k::nat)) < u + #15 + y";
  11.334 +test "(i + j + #3 + (k::nat)) < u + #-15 + y";
  11.335 +test "(i + j + #-12 + (k::nat)) - #15 = y";
  11.336 +test "(i + j + #12 + (k::nat)) - #-15 = y";
  11.337 +test "(i + j + #-12 + (k::nat)) - #-15 = y";
  11.338 +
  11.339 +(*combine_numerals*)
  11.340 +test "k + #3*k = (u::nat)";
  11.341 +test "Suc (i + #3) = u";
  11.342 +test "Suc (i + j + #3 + k) = u";
  11.343 +test "k + j + #3*k + j = (u::nat)";
  11.344 +test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
  11.345 +test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
  11.346 +(*negative numerals: FAIL*)
  11.347 +test "Suc (i + j + #-3 + k) = u";
  11.348 +*)
  11.349 +
  11.350 +
  11.351 +(*** Prepare linear arithmetic for nat numerals ***)
  11.352 +
  11.353 +local
  11.354 +
  11.355 +(* reduce contradictory <= to False *)
  11.356 +val add_rules =
  11.357 +  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
  11.358 +   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
  11.359 +   le_Suc_number_of,le_number_of_Suc,
  11.360 +   less_Suc_number_of,less_number_of_Suc,
  11.361 +   Suc_eq_number_of,eq_number_of_Suc,
  11.362 +   eq_number_of_0, eq_0_number_of, less_0_number_of,
  11.363 +   nat_number_of, Let_number_of, if_True, if_False];
  11.364 +
  11.365 +val simprocs = [Nat_Times_Assoc.conv,
  11.366 +                Nat_Numeral_Simprocs.combine_numerals]@
  11.367 +                Nat_Numeral_Simprocs.cancel_numerals;
  11.368 +
  11.369 +in
  11.370 +
  11.371 +val nat_simprocs_setup =
  11.372 + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
  11.373 +   {add_mono_thms = add_mono_thms, lessD = lessD,
  11.374 +    simpset = simpset addsimps add_rules
  11.375 +                      addsimps basic_renamed_arith_simps
  11.376 +                      addsimprocs simprocs})];
  11.377 +
  11.378 +end;
    12.1 --- a/src/HOL/IsaMakefile	Tue Jul 25 00:03:39 2000 +0200
    12.2 +++ b/src/HOL/IsaMakefile	Tue Jul 25 00:06:46 2000 +0200
    12.3 @@ -8,10 +8,11 @@
    12.4  
    12.5  default: HOL
    12.6  images: HOL HOL-Real TLA
    12.7 -test: HOL-Subst HOL-Induct HOL-IMP HOL-IMPP HOL-Hoare HOL-Lex HOL-Algebra \
    12.8 -  HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML \
    12.9 -  HOL-BCV HOL-MicroJava HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   12.10 -  HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
   12.11 +test: HOL-Isar_examples HOL-Induct HOL-ex HOL-Subst HOL-IMP HOL-IMPP \
   12.12 +  HOL-Hoare HOL-Lex HOL-Algebra HOL-Auth HOL-UNITY HOL-Modelcheck \
   12.13 +  HOL-Lambda HOL-Prolog HOL-W0 HOL-MiniML HOL-BCV HOL-MicroJava \
   12.14 +  HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   12.15 +  HOL-AxClasses-Tutorial HOL-Quot HOL-Real-ex \
   12.16    HOL-Real-HahnBanach TLA-Inc TLA-Buffer TLA-Memory
   12.17  
   12.18  all: images test
   12.19 @@ -31,44 +32,43 @@
   12.20  Pure:
   12.21  	@cd $(SRC)/Pure; $(ISATOOL) make Pure
   12.22  
   12.23 -$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML \
   12.24 -  $(SRC)/Provers/Arith/cancel_sums.ML		\
   12.25 -  $(SRC)/Provers/Arith/assoc_fold.ML		\
   12.26 -  $(SRC)/Provers/Arith/combine_numerals.ML	\
   12.27 -  $(SRC)/Provers/Arith/cancel_numerals.ML	\
   12.28 -  $(SRC)/Provers/Arith/fast_lin_arith.ML \
   12.29 -  $(SRC)/Provers/blast.ML $(SRC)/Provers/make_elim.ML \
   12.30 -  $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
   12.31 -  $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/simplifier.ML \
   12.32 -  $(SRC)/Provers/split_paired_all.ML $(SRC)/Provers/splitter.ML \
   12.33 -  $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml $(SRC)/TFL/rules.sml \
   12.34 -  $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig $(SRC)/TFL/tfl.sml \
   12.35 -  $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml $(SRC)/TFL/thry.sig \
   12.36 -  $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig $(SRC)/TFL/usyntax.sml \
   12.37 -  $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml Arith.ML Arith.thy \
   12.38 -  Calculation.thy Datatype.thy Divides.ML Divides.thy Finite.ML \
   12.39 -  Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy HOL.ML HOL.thy \
   12.40 -  HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
   12.41 -  Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML Integ/IntArith.thy \
   12.42 -  Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML Integ/Int.thy \
   12.43 -  Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML Integ/NatBin.thy \
   12.44 -  Integ/NatSimprocs.thy Integ/NatSimprocs.ML \
   12.45 -  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML \
   12.46 -  Map.thy Nat.ML Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML \
   12.47 -  Option.thy Ord.ML Ord.thy Power.ML Power.thy PreList.thy Prod.ML \
   12.48 -  Prod.thy ROOT.ML Recdef.thy Record.thy RelPow.ML RelPow.thy \
   12.49 -  Relation.ML Relation.thy Set.ML Set.thy SetInterval.ML SetInterval.thy \
   12.50 -  String.thy SVC_Oracle.ML \
   12.51 -  SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML \
   12.52 -  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML \
   12.53 -  Tools/datatype_prop.ML Tools/datatype_rep_proofs.ML \
   12.54 -  Tools/induct_method.ML Tools/inductive_package.ML \
   12.55 -  Tools/numeral_syntax.ML Tools/primrec_package.ML \
   12.56 -  Tools/recdef_package.ML Tools/record_package.ML Tools/svc_funcs.ML \
   12.57 -  Tools/typedef_package.ML Trancl.ML Trancl.thy Univ.ML Univ.thy \
   12.58 -  Vimage.ML Vimage.thy WF.ML WF.thy WF_Rel.ML WF_Rel.thy blastdata.ML \
   12.59 -  cladata.ML equalities.ML equalities.thy hologic.ML mono.ML mono.thy \
   12.60 -  simpdata.ML subset.ML subset.thy thy_syntax.ML
   12.61 +$(OUT)/HOL: $(OUT)/Pure $(SRC)/Provers/Arith/abel_cancel.ML		\
   12.62 +  $(SRC)/Provers/Arith/cancel_sums.ML					\
   12.63 +  $(SRC)/Provers/Arith/assoc_fold.ML					\
   12.64 +  $(SRC)/Provers/Arith/combine_numerals.ML				\
   12.65 +  $(SRC)/Provers/Arith/cancel_numerals.ML				\
   12.66 +  $(SRC)/Provers/Arith/fast_lin_arith.ML $(SRC)/Provers/blast.ML	\
   12.67 +  $(SRC)/Provers/make_elim.ML $(SRC)/Provers/clasimp.ML			\
   12.68 +  $(SRC)/Provers/classical.ML $(SRC)/Provers/hypsubst.ML		\
   12.69 +  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/split_paired_all.ML	\
   12.70 +  $(SRC)/Provers/splitter.ML $(SRC)/TFL/dcterm.sml $(SRC)/TFL/post.sml	\
   12.71 +  $(SRC)/TFL/rules.sml $(SRC)/TFL/rules.sig $(SRC)/TFL/tfl.sig		\
   12.72 +  $(SRC)/TFL/tfl.sml $(SRC)/TFL/thms.sig $(SRC)/TFL/thms.sml		\
   12.73 +  $(SRC)/TFL/thry.sig $(SRC)/TFL/thry.sml $(SRC)/TFL/usyntax.sig	\
   12.74 +  $(SRC)/TFL/usyntax.sml $(SRC)/TFL/utils.sig $(SRC)/TFL/utils.sml	\
   12.75 +  Arith.ML Arith.thy Calculation.thy Datatype.thy Divides.ML		\
   12.76 +  Divides.thy Finite.ML Finite.thy Fun.ML Fun.thy Gfp.ML Gfp.thy	\
   12.77 +  HOL.ML HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML		\
   12.78 +  Integ/Bin.thy Integ/Equiv.ML Integ/Equiv.thy Integ/IntArith.ML	\
   12.79 +  Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy Integ/Int.ML	\
   12.80 +  Integ/Int.thy Integ/IntDiv.ML Integ/IntDiv.thy Integ/NatBin.ML	\
   12.81 +  Integ/NatBin.thy Integ/NatSimprocs.thy Integ/NatSimprocs.ML		\
   12.82 +  Integ/int_arith1.ML Integ/int_arith2.ML Integ/nat_simprocs.ML         \
   12.83 +  Lfp.ML Lfp.thy List.ML List.thy Main.thy Map.ML Map.thy Nat.ML        \
   12.84 +  Nat.thy NatDef.ML NatDef.thy Numeral.thy Option.ML Option.thy Ord.ML  \
   12.85 +  Ord.thy Power.ML Power.thy PreList.thy Prod.ML Prod.thy ROOT.ML       \
   12.86 +  Recdef.thy Record.thy RelPow.ML RelPow.thy Relation.ML Relation.thy   \
   12.87 +  Set.ML Set.thy SetInterval.ML	SetInterval.thy String.thy              \
   12.88 +  SVC_Oracle.ML SVC_Oracle.thy Sum.ML Sum.thy Tools/datatype_aux.ML     \
   12.89 +  Tools/datatype_abs_proofs.ML Tools/datatype_package.ML Tools/datatype_prop.ML	\
   12.90 +  Tools/datatype_rep_proofs.ML Tools/induct_method.ML			\
   12.91 +  Tools/inductive_package.ML Tools/numeral_syntax.ML			\
   12.92 +  Tools/primrec_package.ML Tools/recdef_package.ML			\
   12.93 +  Tools/record_package.ML Tools/svc_funcs.ML Tools/typedef_package.ML	\
   12.94 +  Trancl.ML Trancl.thy Univ.ML Univ.thy Vimage.ML Vimage.thy WF.ML	\
   12.95 +  WF.thy WF_Rel.ML WF_Rel.thy arith_data.ML blastdata.ML cladata.ML	\
   12.96 +  equalities.ML equalities.thy hologic.ML mono.ML mono.thy simpdata.ML	\
   12.97 +  subset.ML subset.thy thy_syntax.ML
   12.98  	@$(ISATOOL) usedir -b $(OUT)/Pure HOL
   12.99  
  12.100  
  12.101 @@ -76,16 +76,17 @@
  12.102  
  12.103  HOL-Real: HOL $(OUT)/HOL-Real
  12.104  
  12.105 -$(OUT)/HOL-Real: $(OUT)/HOL Real/Lubs.ML Real/Lubs.thy Real/PNat.ML \
  12.106 -  Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \
  12.107 -  Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \
  12.108 -  Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \
  12.109 -  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
  12.110 -  Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \
  12.111 -  Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \
  12.112 -  Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \
  12.113 -  Real/Hyperreal/HyperDef.ML Real/Hyperreal/HyperDef.thy \
  12.114 -  Real/Hyperreal/Zorn.ML Real/Hyperreal/Zorn.thy
  12.115 +$(OUT)/HOL-Real: $(OUT)/HOL Real/Hyperreal/Filter.ML			\
  12.116 +  Real/Hyperreal/Filter.thy Real/Hyperreal/HyperDef.ML			\
  12.117 +  Real/Hyperreal/HyperDef.thy Real/Hyperreal/Zorn.ML			\
  12.118 +  Real/Hyperreal/Zorn.thy Real/Hyperreal/fuf.ML Real/Lubs.ML		\
  12.119 +  Real/Lubs.thy Real/PNat.ML Real/PNat.thy Real/PRat.ML Real/PRat.thy	\
  12.120 +  Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy	\
  12.121 +  Real/ROOT.ML Real/Real.thy Real/RealAbs.ML Real/RealAbs.thy		\
  12.122 +  Real/RealArith.ML Real/RealArith.thy Real/RealBin.ML			\
  12.123 +  Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML	\
  12.124 +  Real/RealInt.thy Real/RealOrd.ML Real/RealOrd.thy Real/RealPow.ML	\
  12.125 +  Real/RealPow.thy Real/real_arith.ML
  12.126  	@cd Real; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Real
  12.127  
  12.128  
    13.1 --- a/src/HOL/Nat.ML	Tue Jul 25 00:03:39 2000 +0200
    13.2 +++ b/src/HOL/Nat.ML	Tue Jul 25 00:06:46 2000 +0200
    13.3 @@ -1,7 +1,9 @@
    13.4  (*  Title:      HOL/Nat.ML
    13.5      ID:         $Id$
    13.6 -    Author:     Tobias Nipkow
    13.7 -    Copyright   1997 TU Muenchen
    13.8 +    Author:     Lawrence C Paulson and Tobias Nipkow
    13.9 +
   13.10 +Proofs about natural numbers and elementary arithmetic: addition,
   13.11 +multiplication, etc.  Some from the Hoare example from Norbert Galm.
   13.12  *)
   13.13  
   13.14  (** conversion rules for nat_rec **)
   13.15 @@ -128,3 +130,606 @@
   13.16  qed "max_Suc_Suc";
   13.17  
   13.18  Addsimps [max_0L,max_0R,max_Suc_Suc];
   13.19 +
   13.20 +
   13.21 +(*** Basic rewrite rules for the arithmetic operators ***)
   13.22 +
   13.23 +(** Difference **)
   13.24 +
   13.25 +Goal "0 - n = (0::nat)";
   13.26 +by (induct_tac "n" 1);
   13.27 +by (ALLGOALS Asm_simp_tac);
   13.28 +qed "diff_0_eq_0";
   13.29 +
   13.30 +(*Must simplify BEFORE the induction!  (Else we get a critical pair)
   13.31 +  Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
   13.32 +Goal "Suc(m) - Suc(n) = m - n";
   13.33 +by (Simp_tac 1);
   13.34 +by (induct_tac "n" 1);
   13.35 +by (ALLGOALS Asm_simp_tac);
   13.36 +qed "diff_Suc_Suc";
   13.37 +
   13.38 +Addsimps [diff_0_eq_0, diff_Suc_Suc];
   13.39 +
   13.40 +(* Could be (and is, below) generalized in various ways;
   13.41 +   However, none of the generalizations are currently in the simpset,
   13.42 +   and I dread to think what happens if I put them in *)
   13.43 +Goal "0 < n ==> Suc(n-1) = n";
   13.44 +by (asm_simp_tac (simpset() addsplits [nat.split]) 1);
   13.45 +qed "Suc_pred";
   13.46 +Addsimps [Suc_pred];
   13.47 +
   13.48 +Delsimps [diff_Suc];
   13.49 +
   13.50 +
   13.51 +(**** Inductive properties of the operators ****)
   13.52 +
   13.53 +(*** Addition ***)
   13.54 +
   13.55 +Goal "m + 0 = (m::nat)";
   13.56 +by (induct_tac "m" 1);
   13.57 +by (ALLGOALS Asm_simp_tac);
   13.58 +qed "add_0_right";
   13.59 +
   13.60 +Goal "m + Suc(n) = Suc(m+n)";
   13.61 +by (induct_tac "m" 1);
   13.62 +by (ALLGOALS Asm_simp_tac);
   13.63 +qed "add_Suc_right";
   13.64 +
   13.65 +Addsimps [add_0_right,add_Suc_right];
   13.66 +
   13.67 +
   13.68 +(*Associative law for addition*)
   13.69 +Goal "(m + n) + k = m + ((n + k)::nat)";
   13.70 +by (induct_tac "m" 1);
   13.71 +by (ALLGOALS Asm_simp_tac);
   13.72 +qed "add_assoc";
   13.73 +
   13.74 +(*Commutative law for addition*)
   13.75 +Goal "m + n = n + (m::nat)";
   13.76 +by (induct_tac "m" 1);
   13.77 +by (ALLGOALS Asm_simp_tac);
   13.78 +qed "add_commute";
   13.79 +
   13.80 +Goal "x+(y+z)=y+((x+z)::nat)";
   13.81 +by (rtac (add_commute RS trans) 1);
   13.82 +by (rtac (add_assoc RS trans) 1);
   13.83 +by (rtac (add_commute RS arg_cong) 1);
   13.84 +qed "add_left_commute";
   13.85 +
   13.86 +(*Addition is an AC-operator*)
   13.87 +bind_thms ("add_ac", [add_assoc, add_commute, add_left_commute]);
   13.88 +
   13.89 +Goal "(k + m = k + n) = (m=(n::nat))";
   13.90 +by (induct_tac "k" 1);
   13.91 +by (Simp_tac 1);
   13.92 +by (Asm_simp_tac 1);
   13.93 +qed "add_left_cancel";
   13.94 +
   13.95 +Goal "(m + k = n + k) = (m=(n::nat))";
   13.96 +by (induct_tac "k" 1);
   13.97 +by (Simp_tac 1);
   13.98 +by (Asm_simp_tac 1);
   13.99 +qed "add_right_cancel";
  13.100 +
  13.101 +Goal "(k + m <= k + n) = (m<=(n::nat))";
  13.102 +by (induct_tac "k" 1);
  13.103 +by (Simp_tac 1);
  13.104 +by (Asm_simp_tac 1);
  13.105 +qed "add_left_cancel_le";
  13.106 +
  13.107 +Goal "(k + m < k + n) = (m<(n::nat))";
  13.108 +by (induct_tac "k" 1);
  13.109 +by (Simp_tac 1);
  13.110 +by (Asm_simp_tac 1);
  13.111 +qed "add_left_cancel_less";
  13.112 +
  13.113 +Addsimps [add_left_cancel, add_right_cancel,
  13.114 +          add_left_cancel_le, add_left_cancel_less];
  13.115 +
  13.116 +(** Reasoning about m+0=0, etc. **)
  13.117 +
  13.118 +Goal "!!m::nat. (m+n = 0) = (m=0 & n=0)";
  13.119 +by (case_tac "m" 1);
  13.120 +by (Auto_tac);
  13.121 +qed "add_is_0";
  13.122 +AddIffs [add_is_0];
  13.123 +
  13.124 +Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
  13.125 +by (case_tac "m" 1);
  13.126 +by (Auto_tac);
  13.127 +qed "zero_is_add";
  13.128 +AddIffs [zero_is_add];
  13.129 +
  13.130 +Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
  13.131 +by (case_tac "m" 1);
  13.132 +by (Auto_tac);
  13.133 +qed "add_is_1";
  13.134 +
  13.135 +Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
  13.136 +by (case_tac "m" 1);
  13.137 +by (Auto_tac);
  13.138 +qed "one_is_add";
  13.139 +
  13.140 +Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
  13.141 +by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
  13.142 +qed "add_gr_0";
  13.143 +AddIffs [add_gr_0];
  13.144 +
  13.145 +(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
  13.146 +Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
  13.147 +by (case_tac "m" 1);
  13.148 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
  13.149 +                                      addsplits [nat.split])));
  13.150 +qed "add_pred";
  13.151 +Addsimps [add_pred];
  13.152 +
  13.153 +Goal "!!m::nat. m + n = m ==> n = 0";
  13.154 +by (dtac (add_0_right RS ssubst) 1);
  13.155 +by (asm_full_simp_tac (simpset() addsimps [add_assoc]
  13.156 +                                 delsimps [add_0_right]) 1);
  13.157 +qed "add_eq_self_zero";
  13.158 +
  13.159 +
  13.160 +(**** Additional theorems about "less than" ****)
  13.161 +
  13.162 +(*Deleted less_natE; instead use less_eq_Suc_add RS exE*)
  13.163 +Goal "m<n --> (EX k. n=Suc(m+k))";
  13.164 +by (induct_tac "n" 1);
  13.165 +by (ALLGOALS (simp_tac (simpset() addsimps [order_le_less])));
  13.166 +by (blast_tac (claset() addSEs [less_SucE]
  13.167 +                        addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
  13.168 +qed_spec_mp "less_eq_Suc_add";
  13.169 +
  13.170 +Goal "n <= ((m + n)::nat)";
  13.171 +by (induct_tac "m" 1);
  13.172 +by (ALLGOALS Simp_tac);
  13.173 +by (etac le_SucI 1);
  13.174 +qed "le_add2";
  13.175 +
  13.176 +Goal "n <= ((n + m)::nat)";
  13.177 +by (simp_tac (simpset() addsimps add_ac) 1);
  13.178 +by (rtac le_add2 1);
  13.179 +qed "le_add1";
  13.180 +
  13.181 +bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
  13.182 +bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
  13.183 +
  13.184 +Goal "(m<n) = (EX k. n=Suc(m+k))";
  13.185 +by (blast_tac (claset() addSIs [less_add_Suc1, less_eq_Suc_add]) 1);
  13.186 +qed "less_iff_Suc_add";
  13.187 +
  13.188 +
  13.189 +(*"i <= j ==> i <= j+m"*)
  13.190 +bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
  13.191 +
  13.192 +(*"i <= j ==> i <= m+j"*)
  13.193 +bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
  13.194 +
  13.195 +(*"i < j ==> i < j+m"*)
  13.196 +bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
  13.197 +
  13.198 +(*"i < j ==> i < m+j"*)
  13.199 +bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
  13.200 +
  13.201 +Goal "i+j < (k::nat) --> i<k";
  13.202 +by (induct_tac "j" 1);
  13.203 +by (ALLGOALS Asm_simp_tac);
  13.204 +by (blast_tac (claset() addDs [Suc_lessD]) 1);
  13.205 +qed_spec_mp "add_lessD1";
  13.206 +
  13.207 +Goal "~ (i+j < (i::nat))";
  13.208 +by (rtac notI 1);
  13.209 +by (etac (add_lessD1 RS less_irrefl) 1);
  13.210 +qed "not_add_less1";
  13.211 +
  13.212 +Goal "~ (j+i < (i::nat))";
  13.213 +by (simp_tac (simpset() addsimps [add_commute, not_add_less1]) 1);
  13.214 +qed "not_add_less2";
  13.215 +AddIffs [not_add_less1, not_add_less2];
  13.216 +
  13.217 +Goal "m+k<=n --> m<=(n::nat)";
  13.218 +by (induct_tac "k" 1);
  13.219 +by (ALLGOALS (asm_simp_tac (simpset() addsimps le_simps)));
  13.220 +qed_spec_mp "add_leD1";
  13.221 +
  13.222 +Goal "m+k<=n ==> k<=(n::nat)";
  13.223 +by (full_simp_tac (simpset() addsimps [add_commute]) 1);
  13.224 +by (etac add_leD1 1);
  13.225 +qed_spec_mp "add_leD2";
  13.226 +
  13.227 +Goal "m+k<=n ==> m<=n & k<=(n::nat)";
  13.228 +by (blast_tac (claset() addDs [add_leD1, add_leD2]) 1);
  13.229 +bind_thm ("add_leE", result() RS conjE);
  13.230 +
  13.231 +(*needs !!k for add_ac to work*)
  13.232 +Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
  13.233 +by (force_tac (claset(),
  13.234 +              simpset() delsimps [add_Suc_right]
  13.235 +                        addsimps [less_iff_Suc_add,
  13.236 +                                  add_Suc_right RS sym] @ add_ac) 1);
  13.237 +qed "less_add_eq_less";
  13.238 +
  13.239 +
  13.240 +(*** Monotonicity of Addition ***)
  13.241 +
  13.242 +(*strict, in 1st argument*)
  13.243 +Goal "i < j ==> i + k < j + (k::nat)";
  13.244 +by (induct_tac "k" 1);
  13.245 +by (ALLGOALS Asm_simp_tac);
  13.246 +qed "add_less_mono1";
  13.247 +
  13.248 +(*strict, in both arguments*)
  13.249 +Goal "[|i < j; k < l|] ==> i + k < j + (l::nat)";
  13.250 +by (rtac (add_less_mono1 RS less_trans) 1);
  13.251 +by (REPEAT (assume_tac 1));
  13.252 +by (induct_tac "j" 1);
  13.253 +by (ALLGOALS Asm_simp_tac);
  13.254 +qed "add_less_mono";
  13.255 +
  13.256 +(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
  13.257 +val [lt_mono,le] = Goal
  13.258 +     "[| !!i j::nat. i<j ==> f(i) < f(j);       \
  13.259 +\        i <= j                                 \
  13.260 +\     |] ==> f(i) <= (f(j)::nat)";
  13.261 +by (cut_facts_tac [le] 1);
  13.262 +by (asm_full_simp_tac (simpset() addsimps [order_le_less]) 1);
  13.263 +by (blast_tac (claset() addSIs [lt_mono]) 1);
  13.264 +qed "less_mono_imp_le_mono";
  13.265 +
  13.266 +(*non-strict, in 1st argument*)
  13.267 +Goal "i<=j ==> i + k <= j + (k::nat)";
  13.268 +by (res_inst_tac [("f", "%j. j+k")] less_mono_imp_le_mono 1);
  13.269 +by (etac add_less_mono1 1);
  13.270 +by (assume_tac 1);
  13.271 +qed "add_le_mono1";
  13.272 +
  13.273 +(*non-strict, in both arguments*)
  13.274 +Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::nat)";
  13.275 +by (etac (add_le_mono1 RS le_trans) 1);
  13.276 +by (simp_tac (simpset() addsimps [add_commute]) 1);
  13.277 +qed "add_le_mono";
  13.278 +
  13.279 +
  13.280 +(*** Multiplication ***)
  13.281 +
  13.282 +(*right annihilation in product*)
  13.283 +Goal "!!m::nat. m * 0 = 0";
  13.284 +by (induct_tac "m" 1);
  13.285 +by (ALLGOALS Asm_simp_tac);
  13.286 +qed "mult_0_right";
  13.287 +
  13.288 +(*right successor law for multiplication*)
  13.289 +Goal  "m * Suc(n) = m + (m * n)";
  13.290 +by (induct_tac "m" 1);
  13.291 +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
  13.292 +qed "mult_Suc_right";
  13.293 +
  13.294 +Addsimps [mult_0_right, mult_Suc_right];
  13.295 +
  13.296 +Goal "1 * n = n";
  13.297 +by (Asm_simp_tac 1);
  13.298 +qed "mult_1";
  13.299 +
  13.300 +Goal "n * 1 = n";
  13.301 +by (Asm_simp_tac 1);
  13.302 +qed "mult_1_right";
  13.303 +
  13.304 +(*Commutative law for multiplication*)
  13.305 +Goal "m * n = n * (m::nat)";
  13.306 +by (induct_tac "m" 1);
  13.307 +by (ALLGOALS Asm_simp_tac);
  13.308 +qed "mult_commute";
  13.309 +
  13.310 +(*addition distributes over multiplication*)
  13.311 +Goal "(m + n)*k = (m*k) + ((n*k)::nat)";
  13.312 +by (induct_tac "m" 1);
  13.313 +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
  13.314 +qed "add_mult_distrib";
  13.315 +
  13.316 +Goal "k*(m + n) = (k*m) + ((k*n)::nat)";
  13.317 +by (induct_tac "m" 1);
  13.318 +by (ALLGOALS(asm_simp_tac (simpset() addsimps add_ac)));
  13.319 +qed "add_mult_distrib2";
  13.320 +
  13.321 +(*Associative law for multiplication*)
  13.322 +Goal "(m * n) * k = m * ((n * k)::nat)";
  13.323 +by (induct_tac "m" 1);
  13.324 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_mult_distrib])));
  13.325 +qed "mult_assoc";
  13.326 +
  13.327 +Goal "x*(y*z) = y*((x*z)::nat)";
  13.328 +by (rtac trans 1);
  13.329 +by (rtac mult_commute 1);
  13.330 +by (rtac trans 1);
  13.331 +by (rtac mult_assoc 1);
  13.332 +by (rtac (mult_commute RS arg_cong) 1);
  13.333 +qed "mult_left_commute";
  13.334 +
  13.335 +bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
  13.336 +
  13.337 +Goal "!!m::nat. (m*n = 0) = (m=0 | n=0)";
  13.338 +by (induct_tac "m" 1);
  13.339 +by (induct_tac "n" 2);
  13.340 +by (ALLGOALS Asm_simp_tac);
  13.341 +qed "mult_is_0";
  13.342 +
  13.343 +Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
  13.344 +by (stac eq_commute 1 THEN stac mult_is_0 1);
  13.345 +by Auto_tac;
  13.346 +qed "zero_is_mult";
  13.347 +
  13.348 +Addsimps [mult_is_0, zero_is_mult];
  13.349 +
  13.350 +
  13.351 +(*** Difference ***)
  13.352 +
  13.353 +Goal "!!m::nat. m - m = 0";
  13.354 +by (induct_tac "m" 1);
  13.355 +by (ALLGOALS Asm_simp_tac);
  13.356 +qed "diff_self_eq_0";
  13.357 +
  13.358 +Addsimps [diff_self_eq_0];
  13.359 +
  13.360 +(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
  13.361 +Goal "~ m<n --> n+(m-n) = (m::nat)";
  13.362 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  13.363 +by (ALLGOALS Asm_simp_tac);
  13.364 +qed_spec_mp "add_diff_inverse";
  13.365 +
  13.366 +Goal "n<=m ==> n+(m-n) = (m::nat)";
  13.367 +by (asm_simp_tac (simpset() addsimps [add_diff_inverse, not_less_iff_le]) 1);
  13.368 +qed "le_add_diff_inverse";
  13.369 +
  13.370 +Goal "n<=m ==> (m-n)+n = (m::nat)";
  13.371 +by (asm_simp_tac (simpset() addsimps [le_add_diff_inverse, add_commute]) 1);
  13.372 +qed "le_add_diff_inverse2";
  13.373 +
  13.374 +Addsimps  [le_add_diff_inverse, le_add_diff_inverse2];
  13.375 +
  13.376 +
  13.377 +(*** More results about difference ***)
  13.378 +
  13.379 +Goal "n <= m ==> Suc(m)-n = Suc(m-n)";
  13.380 +by (etac rev_mp 1);
  13.381 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  13.382 +by (ALLGOALS Asm_simp_tac);
  13.383 +qed "Suc_diff_le";
  13.384 +
  13.385 +Goal "m - n < Suc(m)";
  13.386 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  13.387 +by (etac less_SucE 3);
  13.388 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
  13.389 +qed "diff_less_Suc";
  13.390 +
  13.391 +Goal "m - n <= (m::nat)";
  13.392 +by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
  13.393 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [le_SucI])));
  13.394 +qed "diff_le_self";
  13.395 +Addsimps [diff_le_self];
  13.396 +
  13.397 +(* j<k ==> j-n < k *)
  13.398 +bind_thm ("less_imp_diff_less", diff_le_self RS le_less_trans);
  13.399 +
  13.400 +Goal "!!i::nat. i-j-k = i - (j+k)";
  13.401 +by (res_inst_tac [("m","i"),("n","j")] diff_induct 1);
  13.402 +by (ALLGOALS Asm_simp_tac);
  13.403 +qed "diff_diff_left";
  13.404 +
  13.405 +Goal "(Suc m - n) - Suc k = m - n - k";
  13.406 +by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
  13.407 +qed "Suc_diff_diff";
  13.408 +Addsimps [Suc_diff_diff];
  13.409 +
  13.410 +Goal "0<n ==> n - Suc i < n";
  13.411 +by (case_tac "n" 1);
  13.412 +by Safe_tac;
  13.413 +by (asm_simp_tac (simpset() addsimps le_simps) 1);
  13.414 +qed "diff_Suc_less";
  13.415 +Addsimps [diff_Suc_less];
  13.416 +
  13.417 +(*This and the next few suggested by Florian Kammueller*)
  13.418 +Goal "!!i::nat. i-j-k = i-k-j";
  13.419 +by (simp_tac (simpset() addsimps [diff_diff_left, add_commute]) 1);
  13.420 +qed "diff_commute";
  13.421 +
  13.422 +Goal "k <= (j::nat) --> (i + j) - k = i + (j - k)";
  13.423 +by (res_inst_tac [("m","j"),("n","k")] diff_induct 1);
  13.424 +by (ALLGOALS Asm_simp_tac);
  13.425 +qed_spec_mp "diff_add_assoc";
  13.426 +
  13.427 +Goal "k <= (j::nat) --> (j + i) - k = (j - k) + i";
  13.428 +by (asm_simp_tac (simpset() addsimps [add_commute, diff_add_assoc]) 1);
  13.429 +qed_spec_mp "diff_add_assoc2";
  13.430 +
  13.431 +Goal "(n+m) - n = (m::nat)";
  13.432 +by (induct_tac "n" 1);
  13.433 +by (ALLGOALS Asm_simp_tac);
  13.434 +qed "diff_add_inverse";
  13.435 +
  13.436 +Goal "(m+n) - n = (m::nat)";
  13.437 +by (simp_tac (simpset() addsimps [diff_add_assoc]) 1);
  13.438 +qed "diff_add_inverse2";
  13.439 +
  13.440 +Goal "i <= (j::nat) ==> (j-i=k) = (j=k+i)";
  13.441 +by Safe_tac;
  13.442 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_add_inverse2])));
  13.443 +qed "le_imp_diff_is_add";
  13.444 +
  13.445 +Goal "!!m::nat. (m-n = 0) = (m <= n)";
  13.446 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  13.447 +by (ALLGOALS Asm_simp_tac);
  13.448 +qed "diff_is_0_eq";
  13.449 +
  13.450 +Goal "!!m::nat. (0 = m-n) = (m <= n)";
  13.451 +by (stac (diff_is_0_eq RS sym) 1);
  13.452 +by (rtac eq_sym_conv 1);
  13.453 +qed "zero_is_diff_eq";
  13.454 +Addsimps [diff_is_0_eq, zero_is_diff_eq];
  13.455 +
  13.456 +Goal "!!m::nat. (0<n-m) = (m<n)";
  13.457 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  13.458 +by (ALLGOALS Asm_simp_tac);
  13.459 +qed "zero_less_diff";
  13.460 +Addsimps [zero_less_diff];
  13.461 +
  13.462 +Goal "i < j  ==> EX k::nat. 0<k & i+k = j";
  13.463 +by (res_inst_tac [("x","j - i")] exI 1);
  13.464 +by (asm_simp_tac (simpset() addsimps [add_diff_inverse, less_not_sym]) 1);
  13.465 +qed "less_imp_add_positive";
  13.466 +
  13.467 +Goal "P(k) --> (ALL n. P(Suc(n))--> P(n)) --> P(k-i)";
  13.468 +by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
  13.469 +by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
  13.470 +qed "zero_induct_lemma";
  13.471 +
  13.472 +val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
  13.473 +by (rtac (diff_self_eq_0 RS subst) 1);
  13.474 +by (rtac (zero_induct_lemma RS mp RS mp) 1);
  13.475 +by (REPEAT (ares_tac ([impI,allI]@prems) 1));
  13.476 +qed "zero_induct";
  13.477 +
  13.478 +Goal "(k+m) - (k+n) = m - (n::nat)";
  13.479 +by (induct_tac "k" 1);
  13.480 +by (ALLGOALS Asm_simp_tac);
  13.481 +qed "diff_cancel";
  13.482 +
  13.483 +Goal "(m+k) - (n+k) = m - (n::nat)";
  13.484 +by (asm_simp_tac
  13.485 +    (simpset() addsimps [diff_cancel, inst "n" "k" add_commute]) 1);
  13.486 +qed "diff_cancel2";
  13.487 +
  13.488 +Goal "n - (n+m) = (0::nat)";
  13.489 +by (induct_tac "n" 1);
  13.490 +by (ALLGOALS Asm_simp_tac);
  13.491 +qed "diff_add_0";
  13.492 +
  13.493 +
  13.494 +(** Difference distributes over multiplication **)
  13.495 +
  13.496 +Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
  13.497 +by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
  13.498 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
  13.499 +qed "diff_mult_distrib" ;
  13.500 +
  13.501 +Goal "!!m::nat. k * (m - n) = (k * m) - (k * n)";
  13.502 +val mult_commute_k = read_instantiate [("m","k")] mult_commute;
  13.503 +by (simp_tac (simpset() addsimps [diff_mult_distrib, mult_commute_k]) 1);
  13.504 +qed "diff_mult_distrib2" ;
  13.505 +(*NOT added as rewrites, since sometimes they are used from right-to-left*)
  13.506 +
  13.507 +
  13.508 +(*** Monotonicity of Multiplication ***)
  13.509 +
  13.510 +Goal "i <= (j::nat) ==> i*k<=j*k";
  13.511 +by (induct_tac "k" 1);
  13.512 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
  13.513 +qed "mult_le_mono1";
  13.514 +
  13.515 +Goal "i <= (j::nat) ==> k*i <= k*j";
  13.516 +by (dtac mult_le_mono1 1);
  13.517 +by (asm_simp_tac (simpset() addsimps [mult_commute]) 1);
  13.518 +qed "mult_le_mono2";
  13.519 +
  13.520 +(* <= monotonicity, BOTH arguments*)
  13.521 +Goal "[| i <= (j::nat); k <= l |] ==> i*k <= j*l";
  13.522 +by (etac (mult_le_mono1 RS le_trans) 1);
  13.523 +by (etac mult_le_mono2 1);
  13.524 +qed "mult_le_mono";
  13.525 +
  13.526 +(*strict, in 1st argument; proof is by induction on k>0*)
  13.527 +Goal "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
  13.528 +by (eres_inst_tac [("m1","0")] (less_eq_Suc_add RS exE) 1);
  13.529 +by (Asm_simp_tac 1);
  13.530 +by (induct_tac "x" 1);
  13.531 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_less_mono])));
  13.532 +qed "mult_less_mono2";
  13.533 +
  13.534 +Goal "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
  13.535 +by (dtac mult_less_mono2 1);
  13.536 +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
  13.537 +qed "mult_less_mono1";
  13.538 +
  13.539 +Goal "!!m::nat. (0 < m*n) = (0<m & 0<n)";
  13.540 +by (induct_tac "m" 1);
  13.541 +by (case_tac "n" 2);
  13.542 +by (ALLGOALS Asm_simp_tac);
  13.543 +qed "zero_less_mult_iff";
  13.544 +Addsimps [zero_less_mult_iff];
  13.545 +
  13.546 +Goal "(1 <= m*n) = (1<=m & 1<=n)";
  13.547 +by (induct_tac "m" 1);
  13.548 +by (case_tac "n" 2);
  13.549 +by (ALLGOALS Asm_simp_tac);
  13.550 +qed "one_le_mult_iff";
  13.551 +Addsimps [one_le_mult_iff];
  13.552 +
  13.553 +Goal "(m*n = 1) = (m=1 & n=1)";
  13.554 +by (induct_tac "m" 1);
  13.555 +by (Simp_tac 1);
  13.556 +by (induct_tac "n" 1);
  13.557 +by (Simp_tac 1);
  13.558 +by (fast_tac (claset() addss simpset()) 1);
  13.559 +qed "mult_eq_1_iff";
  13.560 +Addsimps [mult_eq_1_iff];
  13.561 +
  13.562 +Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
  13.563 +by (safe_tac (claset() addSIs [mult_less_mono1]));
  13.564 +by (cut_facts_tac [less_linear] 1);
  13.565 +by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
  13.566 +qed "mult_less_cancel2";
  13.567 +
  13.568 +Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
  13.569 +by (dtac mult_less_cancel2 1);
  13.570 +by (etac subst 1);
  13.571 +by (simp_tac (simpset() addsimps [mult_commute]) 1);
  13.572 +qed "mult_less_cancel1";
  13.573 +Addsimps [mult_less_cancel1, mult_less_cancel2];
  13.574 +
  13.575 +Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
  13.576 +by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
  13.577 +qed "mult_le_cancel2";
  13.578 +
  13.579 +Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
  13.580 +by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
  13.581 +qed "mult_le_cancel1";
  13.582 +Addsimps [mult_le_cancel1, mult_le_cancel2];
  13.583 +
  13.584 +Goal "(Suc k * m < Suc k * n) = (m < n)";
  13.585 +by (rtac mult_less_cancel1 1);
  13.586 +by (Simp_tac 1);
  13.587 +qed "Suc_mult_less_cancel1";
  13.588 +
  13.589 +Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
  13.590 +by (simp_tac (simpset_of HOL.thy) 1);
  13.591 +by (rtac Suc_mult_less_cancel1 1);
  13.592 +qed "Suc_mult_le_cancel1";
  13.593 +
  13.594 +Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
  13.595 +by (cut_facts_tac [less_linear] 1);
  13.596 +by Safe_tac;
  13.597 +by (assume_tac 2);
  13.598 +by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
  13.599 +by (ALLGOALS Asm_full_simp_tac);
  13.600 +qed "mult_cancel2";
  13.601 +
  13.602 +Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
  13.603 +by (dtac mult_cancel2 1);
  13.604 +by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
  13.605 +qed "mult_cancel1";
  13.606 +Addsimps [mult_cancel1, mult_cancel2];
  13.607 +
  13.608 +Goal "(Suc k * m = Suc k * n) = (m = n)";
  13.609 +by (rtac mult_cancel1 1);
  13.610 +by (Simp_tac 1);
  13.611 +qed "Suc_mult_cancel1";
  13.612 +
  13.613 +
  13.614 +(*Lemma for gcd*)
  13.615 +Goal "!!m::nat. m = m*n ==> n=1 | m=0";
  13.616 +by (dtac sym 1);
  13.617 +by (rtac disjCI 1);
  13.618 +by (rtac nat_less_cases 1 THEN assume_tac 2);
  13.619 +by (fast_tac (claset() addSEs [less_SucE] addss simpset()) 1);
  13.620 +by (best_tac (claset() addDs [mult_less_mono2] addss simpset()) 1);
  13.621 +qed "mult_eq_self_implies_10";
    14.1 --- a/src/HOL/Nat.thy	Tue Jul 25 00:03:39 2000 +0200
    14.2 +++ b/src/HOL/Nat.thy	Tue Jul 25 00:06:46 2000 +0200
    14.3 @@ -1,13 +1,15 @@
    14.4  (*  Title:      HOL/Nat.thy
    14.5      ID:         $Id$
    14.6 -    Author:     Tobias Nipkow
    14.7 -    Copyright   1997 TU Muenchen
    14.8 +    Author:     Tobias Nipkow and Lawrence C Paulson
    14.9  
   14.10 -Type "nat" is a linear order, and a datatype
   14.11 +Type "nat" is a linear order, and a datatype; arithmetic operators + -
   14.12 +and * (for div, mod and dvd, see theory Divides).
   14.13  *)
   14.14  
   14.15  Nat = NatDef + Inductive +
   14.16  
   14.17 +(* type "nat" is a linear order, and a datatype *)
   14.18 +
   14.19  rep_datatype nat
   14.20    distinct Suc_not_Zero, Zero_not_Suc
   14.21    inject   Suc_Suc_eq
   14.22 @@ -19,4 +21,25 @@
   14.23  consts
   14.24    "^"           :: ['a::power,nat] => 'a            (infixr 80)
   14.25  
   14.26 +
   14.27 +(* arithmetic operators + - and * *)
   14.28 +
   14.29 +instance
   14.30 +  nat :: {plus, minus, times, power}
   14.31 +
   14.32 +(* size of a datatype value; overloaded *)
   14.33 +consts size :: 'a => nat
   14.34 +
   14.35 +primrec
   14.36 +  add_0    "0 + n = n"
   14.37 +  add_Suc  "Suc m + n = Suc(m + n)"
   14.38 +
   14.39 +primrec
   14.40 +  diff_0   "m - 0 = m"
   14.41 +  diff_Suc "m - Suc n = (case m - n of 0 => 0 | Suc k => k)"
   14.42 +
   14.43 +primrec
   14.44 +  mult_0   "0 * n = 0"
   14.45 +  mult_Suc "Suc m * n = n + (m * n)"
   14.46 +
   14.47  end
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/src/HOL/Real/RealArith.ML	Tue Jul 25 00:06:46 2000 +0200
    15.3 @@ -0,0 +1,6 @@
    15.4 +
    15.5 +(*useful??*)
    15.6 +Goal "(z = z + w) = (w = (#0::real))";
    15.7 +by Auto_tac;
    15.8 +qed "real_add_left_cancel0";
    15.9 +Addsimps [real_add_left_cancel0];
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/src/HOL/Real/RealArith.thy	Tue Jul 25 00:06:46 2000 +0200
    16.3 @@ -0,0 +1,7 @@
    16.4 +
    16.5 +theory RealArith = RealBin
    16.6 +files "real_arith.ML":
    16.7 +
    16.8 +setup real_arith_setup
    16.9 +
   16.10 +end
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/src/HOL/Real/real_arith.ML	Tue Jul 25 00:06:46 2000 +0200
    17.3 @@ -0,0 +1,109 @@
    17.4 +(*  Title:      HOL/Real/real_arith.ML
    17.5 +    ID:         $Id$
    17.6 +    Author:     Tobias Nipkow, TU Muenchen
    17.7 +    Copyright   1999 TU Muenchen
    17.8 +
    17.9 +Instantiation of the generic linear arithmetic package for type real.
   17.10 +*)
   17.11 +
   17.12 +local
   17.13 +
   17.14 +(* reduce contradictory <= to False *)
   17.15 +val simps = [order_less_irrefl, zero_eq_numeral_0, one_eq_numeral_1,
   17.16 +             add_real_number_of, minus_real_number_of, diff_real_number_of,
   17.17 +             mult_real_number_of, eq_real_number_of, less_real_number_of,
   17.18 +             le_real_number_of_eq_not_less, real_diff_def,
   17.19 +             real_minus_add_distrib, real_minus_minus];
   17.20 +
   17.21 +val add_rules =
   17.22 +    map rename_numerals
   17.23 +        [real_add_zero_left, real_add_zero_right,
   17.24 +         real_add_minus, real_add_minus_left,
   17.25 +         real_mult_0, real_mult_0_right,
   17.26 +         real_mult_1, real_mult_1_right,
   17.27 +         real_mult_minus_1, real_mult_minus_1_right];
   17.28 +
   17.29 +val simprocs = [Real_Times_Assoc.conv, Real_Numeral_Simprocs.combine_numerals]@
   17.30 +               Real_Numeral_Simprocs.cancel_numerals;
   17.31 +
   17.32 +val mono_ss = simpset() addsimps
   17.33 +                [real_add_le_mono,real_add_less_mono,
   17.34 +                 real_add_less_le_mono,real_add_le_less_mono];
   17.35 +
   17.36 +val add_mono_thms_real =
   17.37 +  map (fn s => prove_goal (the_context ()) s
   17.38 +                 (fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1]))
   17.39 +    ["(i <= j) & (k <= l) ==> i + k <= j + (l::real)",
   17.40 +     "(i  = j) & (k <= l) ==> i + k <= j + (l::real)",
   17.41 +     "(i <= j) & (k  = l) ==> i + k <= j + (l::real)",
   17.42 +     "(i  = j) & (k  = l) ==> i + k  = j + (l::real)",
   17.43 +     "(i < j) & (k = l)   ==> i + k < j + (l::real)",
   17.44 +     "(i = j) & (k < l)   ==> i + k < j + (l::real)",
   17.45 +     "(i < j) & (k <= l)  ==> i + k < j + (l::real)",
   17.46 +     "(i <= j) & (k < l)  ==> i + k < j + (l::real)",
   17.47 +     "(i < j) & (k < l)   ==> i + k < j + (l::real)"];
   17.48 +
   17.49 +val real_arith_simproc_pats =
   17.50 +  map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
   17.51 +      ["(m::real) < n","(m::real) <= n", "(m::real) = n"];
   17.52 +
   17.53 +in
   17.54 +
   17.55 +val fast_real_arith_simproc = mk_simproc
   17.56 +  "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
   17.57 +
   17.58 +val real_arith_setup =
   17.59 + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
   17.60 +   {add_mono_thms = add_mono_thms @ add_mono_thms_real,
   17.61 +    lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
   17.62 +    simpset = simpset addsimps simps@add_rules
   17.63 +                      addsimprocs simprocs
   17.64 +                      addcongs [if_weak_cong]}),
   17.65 +  arith_discrete ("RealDef.real",false),
   17.66 +  Simplifier.change_simpset_of (op addsimprocs) [fast_real_arith_simproc]];
   17.67 +
   17.68 +end;
   17.69 +
   17.70 +
   17.71 +(* Some test data [omitting examples that assume the ordering to be discrete!]
   17.72 +Goal "!!a::real. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   17.73 +by (fast_arith_tac 1);
   17.74 +qed "";
   17.75 +
   17.76 +Goal "!!a::real. [| a <= b; b+b <= c |] ==> a+a <= c";
   17.77 +by (fast_arith_tac 1);
   17.78 +qed "";
   17.79 +
   17.80 +Goal "!!a::real. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j";
   17.81 +by (fast_arith_tac 1);
   17.82 +qed "";
   17.83 +
   17.84 +Goal "!!a::real. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   17.85 +by (arith_tac 1);
   17.86 +qed "";
   17.87 +
   17.88 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   17.89 +\     ==> a <= l";
   17.90 +by (fast_arith_tac 1);
   17.91 +qed "";
   17.92 +
   17.93 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   17.94 +\     ==> a+a+a+a <= l+l+l+l";
   17.95 +by (fast_arith_tac 1);
   17.96 +qed "";
   17.97 +
   17.98 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   17.99 +\     ==> a+a+a+a+a <= l+l+l+l+i";
  17.100 +by (fast_arith_tac 1);
  17.101 +qed "";
  17.102 +
  17.103 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
  17.104 +\     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
  17.105 +by (fast_arith_tac 1);
  17.106 +qed "";
  17.107 +
  17.108 +Goal "!!a::real. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
  17.109 +\     ==> #6*a <= #5*l+i";
  17.110 +by (fast_arith_tac 1);
  17.111 +qed "";
  17.112 +*)
    18.1 --- a/src/HOL/Univ.thy	Tue Jul 25 00:03:39 2000 +0200
    18.2 +++ b/src/HOL/Univ.thy	Tue Jul 25 00:06:46 2000 +0200
    18.3 @@ -11,8 +11,6 @@
    18.4  
    18.5  Univ = Arith + Sum +
    18.6  
    18.7 -setup arith_setup
    18.8 -
    18.9  
   18.10  (** lists, trees will be sets of nodes **)
   18.11  
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/src/HOL/arith_data.ML	Tue Jul 25 00:06:46 2000 +0200
    19.3 @@ -0,0 +1,429 @@
    19.4 +(*  Title:      HOL/arith_data.ML
    19.5 +    ID:         $Id$
    19.6 +    Author:     Markus Wenzel, Stefan Berghofer and Tobias Nipkow
    19.7 +
    19.8 +Various arithmetic proof procedures.
    19.9 +*)
   19.10 +
   19.11 +(*---------------------------------------------------------------------------*)
   19.12 +(* 1. Cancellation of common terms                                           *)
   19.13 +(*---------------------------------------------------------------------------*)
   19.14 +
   19.15 +signature ARITH_DATA =
   19.16 +sig
   19.17 +  val nat_cancel_sums_add: simproc list
   19.18 +  val nat_cancel_sums: simproc list
   19.19 +  val nat_cancel_factor: simproc list
   19.20 +  val nat_cancel: simproc list
   19.21 +end;
   19.22 +
   19.23 +structure ArithData: ARITH_DATA =
   19.24 +struct
   19.25 +
   19.26 +
   19.27 +(** abstract syntax of structure nat: 0, Suc, + **)
   19.28 +
   19.29 +(* mk_sum, mk_norm_sum *)
   19.30 +
   19.31 +val one = HOLogic.mk_nat 1;
   19.32 +val mk_plus = HOLogic.mk_binop "op +";
   19.33 +
   19.34 +fun mk_sum [] = HOLogic.zero
   19.35 +  | mk_sum [t] = t
   19.36 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   19.37 +
   19.38 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
   19.39 +fun mk_norm_sum ts =
   19.40 +  let val (ones, sums) = partition (equal one) ts in
   19.41 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
   19.42 +  end;
   19.43 +
   19.44 +
   19.45 +(* dest_sum *)
   19.46 +
   19.47 +val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
   19.48 +
   19.49 +fun dest_sum tm =
   19.50 +  if HOLogic.is_zero tm then []
   19.51 +  else
   19.52 +    (case try HOLogic.dest_Suc tm of
   19.53 +      Some t => one :: dest_sum t
   19.54 +    | None =>
   19.55 +        (case try dest_plus tm of
   19.56 +          Some (t, u) => dest_sum t @ dest_sum u
   19.57 +        | None => [tm]));
   19.58 +
   19.59 +
   19.60 +(** generic proof tools **)
   19.61 +
   19.62 +(* prove conversions *)
   19.63 +
   19.64 +val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   19.65 +
   19.66 +fun prove_conv expand_tac norm_tac sg (t, u) =
   19.67 +  mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv (t, u)))
   19.68 +    (K [expand_tac, norm_tac]))
   19.69 +  handle ERROR => error ("The error(s) above occurred while trying to prove " ^
   19.70 +    (string_of_cterm (cterm_of sg (mk_eqv (t, u)))));
   19.71 +
   19.72 +val subst_equals = prove_goal HOL.thy "[| t = s; u = t |] ==> u = s"
   19.73 +  (fn prems => [cut_facts_tac prems 1, SIMPSET' asm_simp_tac 1]);
   19.74 +
   19.75 +
   19.76 +(* rewriting *)
   19.77 +
   19.78 +fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
   19.79 +
   19.80 +val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
   19.81 +val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
   19.82 +
   19.83 +
   19.84 +
   19.85 +(** cancel common summands **)
   19.86 +
   19.87 +structure Sum =
   19.88 +struct
   19.89 +  val mk_sum = mk_norm_sum;
   19.90 +  val dest_sum = dest_sum;
   19.91 +  val prove_conv = prove_conv;
   19.92 +  val norm_tac = simp_all add_rules THEN simp_all add_ac;
   19.93 +end;
   19.94 +
   19.95 +fun gen_uncancel_tac rule ct =
   19.96 +  rtac (instantiate' [] [None, Some ct] (rule RS subst_equals)) 1;
   19.97 +
   19.98 +
   19.99 +(* nat eq *)
  19.100 +
  19.101 +structure EqCancelSums = CancelSumsFun
  19.102 +(struct
  19.103 +  open Sum;
  19.104 +  val mk_bal = HOLogic.mk_eq;
  19.105 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
  19.106 +  val uncancel_tac = gen_uncancel_tac add_left_cancel;
  19.107 +end);
  19.108 +
  19.109 +
  19.110 +(* nat less *)
  19.111 +
  19.112 +structure LessCancelSums = CancelSumsFun
  19.113 +(struct
  19.114 +  open Sum;
  19.115 +  val mk_bal = HOLogic.mk_binrel "op <";
  19.116 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
  19.117 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_less;
  19.118 +end);
  19.119 +
  19.120 +
  19.121 +(* nat le *)
  19.122 +
  19.123 +structure LeCancelSums = CancelSumsFun
  19.124 +(struct
  19.125 +  open Sum;
  19.126 +  val mk_bal = HOLogic.mk_binrel "op <=";
  19.127 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
  19.128 +  val uncancel_tac = gen_uncancel_tac add_left_cancel_le;
  19.129 +end);
  19.130 +
  19.131 +
  19.132 +(* nat diff *)
  19.133 +
  19.134 +structure DiffCancelSums = CancelSumsFun
  19.135 +(struct
  19.136 +  open Sum;
  19.137 +  val mk_bal = HOLogic.mk_binop "op -";
  19.138 +  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT;
  19.139 +  val uncancel_tac = gen_uncancel_tac diff_cancel;
  19.140 +end);
  19.141 +
  19.142 +
  19.143 +
  19.144 +(** cancel common factor **)
  19.145 +
  19.146 +structure Factor =
  19.147 +struct
  19.148 +  val mk_sum = mk_norm_sum;
  19.149 +  val dest_sum = dest_sum;
  19.150 +  val prove_conv = prove_conv;
  19.151 +  val norm_tac = simp_all (add_rules @ mult_rules) THEN simp_all add_ac;
  19.152 +end;
  19.153 +
  19.154 +fun mk_cnat n = cterm_of (Theory.sign_of (the_context ())) (HOLogic.mk_nat n);
  19.155 +
  19.156 +fun gen_multiply_tac rule k =
  19.157 +  if k > 0 then
  19.158 +    rtac (instantiate' [] [None, Some (mk_cnat (k - 1))] (rule RS subst_equals)) 1
  19.159 +  else no_tac;
  19.160 +
  19.161 +
  19.162 +(* nat eq *)
  19.163 +
  19.164 +structure EqCancelFactor = CancelFactorFun
  19.165 +(struct
  19.166 +  open Factor;
  19.167 +  val mk_bal = HOLogic.mk_eq;
  19.168 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
  19.169 +  val multiply_tac = gen_multiply_tac Suc_mult_cancel1;
  19.170 +end);
  19.171 +
  19.172 +
  19.173 +(* nat less *)
  19.174 +
  19.175 +structure LessCancelFactor = CancelFactorFun
  19.176 +(struct
  19.177 +  open Factor;
  19.178 +  val mk_bal = HOLogic.mk_binrel "op <";
  19.179 +  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT;
  19.180 +  val multiply_tac = gen_multiply_tac Suc_mult_less_cancel1;
  19.181 +end);
  19.182 +
  19.183 +
  19.184 +(* nat le *)
  19.185 +
  19.186 +structure LeCancelFactor = CancelFactorFun
  19.187 +(struct
  19.188 +  open Factor;
  19.189 +  val mk_bal = HOLogic.mk_binrel "op <=";
  19.190 +  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT;
  19.191 +  val multiply_tac = gen_multiply_tac Suc_mult_le_cancel1;
  19.192 +end);
  19.193 +
  19.194 +
  19.195 +
  19.196 +(** prepare nat_cancel simprocs **)
  19.197 +
  19.198 +fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
  19.199 +val prep_pats = map prep_pat;
  19.200 +
  19.201 +fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
  19.202 +
  19.203 +val eq_pats = prep_pats ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"];
  19.204 +val less_pats = prep_pats ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"];
  19.205 +val le_pats = prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"];
  19.206 +val diff_pats = prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"];
  19.207 +
  19.208 +val nat_cancel_sums_add = map prep_simproc
  19.209 +  [("nateq_cancel_sums", eq_pats, EqCancelSums.proc),
  19.210 +   ("natless_cancel_sums", less_pats, LessCancelSums.proc),
  19.211 +   ("natle_cancel_sums", le_pats, LeCancelSums.proc)];
  19.212 +
  19.213 +val nat_cancel_sums = nat_cancel_sums_add @
  19.214 +  [prep_simproc("natdiff_cancel_sums", diff_pats, DiffCancelSums.proc)];
  19.215 +
  19.216 +val nat_cancel_factor = map prep_simproc
  19.217 +  [("nateq_cancel_factor", eq_pats, EqCancelFactor.proc),
  19.218 +   ("natless_cancel_factor", less_pats, LessCancelFactor.proc),
  19.219 +   ("natle_cancel_factor", le_pats, LeCancelFactor.proc)];
  19.220 +
  19.221 +val nat_cancel = nat_cancel_factor @ nat_cancel_sums;
  19.222 +
  19.223 +
  19.224 +end;
  19.225 +
  19.226 +open ArithData;
  19.227 +
  19.228 +
  19.229 +(*---------------------------------------------------------------------------*)
  19.230 +(* 2. Linear arithmetic                                                      *)
  19.231 +(*---------------------------------------------------------------------------*)
  19.232 +
  19.233 +(* Parameters data for general linear arithmetic functor *)
  19.234 +
  19.235 +structure LA_Logic: LIN_ARITH_LOGIC =
  19.236 +struct
  19.237 +val ccontr = ccontr;
  19.238 +val conjI = conjI;
  19.239 +val neqE = linorder_neqE;
  19.240 +val notI = notI;
  19.241 +val sym = sym;
  19.242 +val not_lessD = linorder_not_less RS iffD1;
  19.243 +val not_leD = linorder_not_le RS iffD1;
  19.244 +
  19.245 +
  19.246 +fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
  19.247 +
  19.248 +val mk_Trueprop = HOLogic.mk_Trueprop;
  19.249 +
  19.250 +fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
  19.251 +  | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
  19.252 +
  19.253 +fun is_False thm =
  19.254 +  let val _ $ t = #prop(rep_thm thm)
  19.255 +  in t = Const("False",HOLogic.boolT) end;
  19.256 +
  19.257 +fun is_nat(t) = fastype_of1 t = HOLogic.natT;
  19.258 +
  19.259 +fun mk_nat_thm sg t =
  19.260 +  let val ct = cterm_of sg t  and cn = cterm_of sg (Var(("n",0),HOLogic.natT))
  19.261 +  in instantiate ([],[(cn,ct)]) le0 end;
  19.262 +
  19.263 +end;
  19.264 +
  19.265 +
  19.266 +(* arith theory data *)
  19.267 +
  19.268 +structure ArithDataArgs =
  19.269 +struct
  19.270 +  val name = "HOL/arith";
  19.271 +  type T = {splits: thm list, discrete: (string * bool) list};
  19.272 +
  19.273 +  val empty = {splits = [], discrete = []};
  19.274 +  val copy = I;
  19.275 +  val prep_ext = I;
  19.276 +  fun merge ({splits = splits1, discrete = discrete1}, {splits = splits2, discrete = discrete2}) =
  19.277 +   {splits = Drule.merge_rules (splits1, splits2),
  19.278 +    discrete = merge_alists discrete1 discrete2};
  19.279 +  fun print _ _ = ();
  19.280 +end;
  19.281 +
  19.282 +structure ArithData = TheoryDataFun(ArithDataArgs);
  19.283 +
  19.284 +fun arith_split_add (thy, thm) = (ArithData.map (fn {splits, discrete} =>
  19.285 +  {splits = thm :: splits, discrete = discrete}) thy, thm);
  19.286 +
  19.287 +fun arith_discrete d = ArithData.map (fn {splits, discrete} =>
  19.288 +  {splits = splits, discrete = d :: discrete});
  19.289 +
  19.290 +
  19.291 +structure LA_Data_Ref: LIN_ARITH_DATA =
  19.292 +struct
  19.293 +
  19.294 +(* Decomposition of terms *)
  19.295 +
  19.296 +fun nT (Type("fun",[N,_])) = N = HOLogic.natT
  19.297 +  | nT _ = false;
  19.298 +
  19.299 +fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
  19.300 +                           | Some n => (overwrite(p,(t,n+m:int)), i));
  19.301 +
  19.302 +(* Turn term into list of summand * multiplicity plus a constant *)
  19.303 +fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
  19.304 +  | poly(all as Const("op -",T) $ s $ t, m, pi) =
  19.305 +      if nT T then add_atom(all,m,pi)
  19.306 +      else poly(s,m,poly(t,~1*m,pi))
  19.307 +  | poly(Const("uminus",_) $ t, m, pi) = poly(t,~1*m,pi)
  19.308 +  | poly(Const("0",_), _, pi) = pi
  19.309 +  | poly(Const("Suc",_)$t, m, (p,i)) = poly(t, m, (p,i+m))
  19.310 +  | poly(all as Const("op *",_) $ (Const("Numeral.number_of",_)$c) $ t, m, pi)=
  19.311 +      (poly(t,m*HOLogic.dest_binum c,pi)
  19.312 +       handle TERM _ => add_atom(all,m,pi))
  19.313 +  | poly(all as Const("op *",_) $ t $ (Const("Numeral.number_of",_)$c), m, pi)=
  19.314 +      (poly(t,m*HOLogic.dest_binum c,pi)
  19.315 +       handle TERM _ => add_atom(all,m,pi))
  19.316 +  | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
  19.317 +     ((p,i + m*HOLogic.dest_binum t)
  19.318 +      handle TERM _ => add_atom(all,m,(p,i)))
  19.319 +  | poly x  = add_atom x;
  19.320 +
  19.321 +fun decomp2(rel,lhs,rhs) =
  19.322 +  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
  19.323 +  in case rel of
  19.324 +       "op <"  => Some(p,i,"<",q,j)
  19.325 +     | "op <=" => Some(p,i,"<=",q,j)
  19.326 +     | "op ="  => Some(p,i,"=",q,j)
  19.327 +     | _       => None
  19.328 +  end;
  19.329 +
  19.330 +fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
  19.331 +  | negate None = None;
  19.332 +
  19.333 +fun decomp1 discrete (T,xxx) =
  19.334 +  (case T of
  19.335 +     Type("fun",[Type(D,[]),_]) =>
  19.336 +       (case assoc(discrete,D) of
  19.337 +          None => None
  19.338 +        | Some d => (case decomp2 xxx of
  19.339 +                       None => None
  19.340 +                     | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
  19.341 +   | _ => None);
  19.342 +
  19.343 +fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs))
  19.344 +  | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
  19.345 +      negate(decomp1 discrete (T,(rel,lhs,rhs)))
  19.346 +  | decomp2 discrete _ = None
  19.347 +
  19.348 +val decomp = decomp2 o #discrete o ArithData.get_sg;
  19.349 +
  19.350 +end;
  19.351 +
  19.352 +
  19.353 +structure Fast_Arith =
  19.354 +  Fast_Lin_Arith(structure LA_Logic=LA_Logic and LA_Data=LA_Data_Ref);
  19.355 +
  19.356 +val fast_arith_tac = Fast_Arith.lin_arith_tac
  19.357 +and trace_arith    = Fast_Arith.trace;
  19.358 +
  19.359 +local
  19.360 +
  19.361 +(* reduce contradictory <= to False.
  19.362 +   Most of the work is done by the cancel tactics.
  19.363 +*)
  19.364 +val add_rules = [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq];
  19.365 +
  19.366 +val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s
  19.367 + (fn prems => [cut_facts_tac prems 1,
  19.368 +               blast_tac (claset() addIs [add_le_mono]) 1]))
  19.369 +["(i <= j) & (k <= l) ==> i + k <= j + (l::nat)",
  19.370 + "(i  = j) & (k <= l) ==> i + k <= j + (l::nat)",
  19.371 + "(i <= j) & (k  = l) ==> i + k <= j + (l::nat)",
  19.372 + "(i  = j) & (k  = l) ==> i + k  = j + (l::nat)"
  19.373 +];
  19.374 +
  19.375 +in
  19.376 +
  19.377 +val init_lin_arith_data =
  19.378 + Fast_Arith.setup @
  19.379 + [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} =>
  19.380 +   {add_mono_thms = add_mono_thms @ add_mono_thms_nat,
  19.381 +    lessD = lessD @ [Suc_leI],
  19.382 +    simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
  19.383 +  ArithData.init, arith_discrete ("nat", true)];
  19.384 +
  19.385 +end;
  19.386 +
  19.387 +
  19.388 +local
  19.389 +val nat_arith_simproc_pats =
  19.390 +  map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.boolT))
  19.391 +      ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"];
  19.392 +in
  19.393 +val fast_nat_arith_simproc = mk_simproc
  19.394 +  "fast_nat_arith" nat_arith_simproc_pats Fast_Arith.lin_arith_prover;
  19.395 +end;
  19.396 +
  19.397 +(* Because of fast_nat_arith_simproc, the arithmetic solver is really only
  19.398 +useful to detect inconsistencies among the premises for subgoals which are
  19.399 +*not* themselves (in)equalities, because the latter activate
  19.400 +fast_nat_arith_simproc anyway. However, it seems cheaper to activate the
  19.401 +solver all the time rather than add the additional check. *)
  19.402 +
  19.403 +
  19.404 +(* arith proof method *)
  19.405 +
  19.406 +(* FIXME: K true should be replaced by a sensible test to speed things up
  19.407 +   in case there are lots of irrelevant terms involved;
  19.408 +   elimination of min/max can be optimized:
  19.409 +   (max m n + k <= r) = (m+k <= r & n+k <= r)
  19.410 +   (l <= min m n + k) = (l <= m+k & l <= n+k)
  19.411 +*)
  19.412 +fun arith_tac i st =
  19.413 +  refute_tac (K true) (REPEAT o split_tac (#splits (ArithData.get_sg (Thm.sign_of_thm st))))
  19.414 +             ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac) i st;
  19.415 +
  19.416 +fun arith_method prems =
  19.417 +  Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
  19.418 +
  19.419 +
  19.420 +(* theory setup *)
  19.421 +
  19.422 +val arith_setup =
  19.423 + [Simplifier.change_simpset_of (op addsimprocs) nat_cancel] @
  19.424 +  init_lin_arith_data @
  19.425 +  [Simplifier.change_simpset_of (op addSolver)
  19.426 +   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
  19.427 +  Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
  19.428 +  Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
  19.429 +    "decide linear arithmethic")],
  19.430 +  Attrib.add_attributes [("arith_split",
  19.431 +    (Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),
  19.432 +    "declare split rules for arithmetic procedure")]];