Linear arithmetic now copes with mixed nat/int formulae.
authornipkow
Fri Dec 01 19:53:29 2000 +0100 (2000-12-01)
changeset 105748f98f0301d67
parent 10573 1751ab881289
child 10575 c78d26d5c3c1
Linear arithmetic now copes with mixed nat/int formulae.
src/HOL/Integ/IntArith.thy
src/HOL/Integ/NatBin.ML
src/HOL/Integ/NatBin.thy
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_bin.ML
src/HOL/Integ/nat_simprocs.ML
src/HOL/IsaMakefile
src/HOL/Real/RealArith.ML
src/HOL/Real/RealArith.thy
src/HOL/Real/real_arith.ML
src/HOL/arith_data.ML
     1.1 --- a/src/HOL/Integ/IntArith.thy	Fri Dec 01 19:44:48 2000 +0100
     1.2 +++ b/src/HOL/Integ/IntArith.thy	Fri Dec 01 19:53:29 2000 +0100
     1.3 @@ -1,4 +1,3 @@
     1.4 -
     1.5  theory IntArith = Bin
     1.6  files ("int_arith1.ML") ("int_arith2.ML"):
     1.7  
     2.1 --- a/src/HOL/Integ/NatBin.ML	Fri Dec 01 19:44:48 2000 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,538 +0,0 @@
     2.4 -(*  Title:      HOL/NatBin.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1999  University of Cambridge
     2.8 -
     2.9 -Binary arithmetic for the natural numbers
    2.10 -*)
    2.11 -
    2.12 -(** nat (coercion from int to nat) **)
    2.13 -
    2.14 -Goal "nat (number_of w) = number_of w";
    2.15 -by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
    2.16 -qed "nat_number_of";
    2.17 -Addsimps [nat_number_of];
    2.18 -
    2.19 -(*These rewrites should one day be re-oriented...*)
    2.20 -
    2.21 -Goal "#0 = (0::nat)";
    2.22 -by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1);
    2.23 -qed "numeral_0_eq_0";
    2.24 -
    2.25 -Goal "#1 = (1::nat)";
    2.26 -by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1);
    2.27 -qed "numeral_1_eq_1";
    2.28 -
    2.29 -Goal "#2 = (2::nat)";
    2.30 -by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1);
    2.31 -qed "numeral_2_eq_2";
    2.32 -
    2.33 -bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
    2.34 -
    2.35 -(** int (coercion from nat to int) **)
    2.36 -
    2.37 -(*"neg" is used in rewrite rules for binary comparisons*)
    2.38 -Goal "int (number_of v :: nat) = \
    2.39 -\        (if neg (number_of v) then #0 \
    2.40 -\         else (number_of v :: int))";
    2.41 -by (simp_tac
    2.42 -    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
    2.43 -				  not_neg_nat, int_0]) 1);
    2.44 -qed "int_nat_number_of";
    2.45 -Addsimps [int_nat_number_of];
    2.46 -
    2.47 -
    2.48 -(** Successor **)
    2.49 -
    2.50 -Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
    2.51 -by (rtac sym 1);
    2.52 -by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    2.53 -qed "Suc_nat_eq_nat_zadd1";
    2.54 -
    2.55 -Goal "Suc (number_of v) = \
    2.56 -\       (if neg (number_of v) then #1 else number_of (bin_succ v))";
    2.57 -by (simp_tac
    2.58 -    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
    2.59 -				  nat_number_of_def, int_Suc, 
    2.60 -				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
    2.61 -qed "Suc_nat_number_of";
    2.62 -Addsimps [Suc_nat_number_of];
    2.63 -
    2.64 -Goal "Suc (number_of v + n) = \
    2.65 -\       (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
    2.66 -by (Simp_tac 1);
    2.67 -qed "Suc_nat_number_of_add";
    2.68 -
    2.69 -Goal "Suc #0 = #1";
    2.70 -by (Simp_tac 1);
    2.71 -qed "Suc_numeral_0_eq_1";
    2.72 -
    2.73 -Goal "Suc #1 = #2";
    2.74 -by (Simp_tac 1);
    2.75 -qed "Suc_numeral_1_eq_2";
    2.76 -
    2.77 -(** Addition **)
    2.78 -
    2.79 -Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
    2.80 -by (rtac (inj_int RS injD) 1);
    2.81 -by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
    2.82 -qed "nat_add_distrib";
    2.83 -
    2.84 -(*"neg" is used in rewrite rules for binary comparisons*)
    2.85 -Goal "(number_of v :: nat) + number_of v' = \
    2.86 -\        (if neg (number_of v) then number_of v' \
    2.87 -\         else if neg (number_of v') then number_of v \
    2.88 -\         else number_of (bin_add v v'))";
    2.89 -by (simp_tac
    2.90 -    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
    2.91 -				  nat_add_distrib RS sym, number_of_add]) 1);
    2.92 -qed "add_nat_number_of";
    2.93 -
    2.94 -Addsimps [add_nat_number_of];
    2.95 -
    2.96 -
    2.97 -(** Subtraction **)
    2.98 -
    2.99 -Goal "[| (#0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
   2.100 -by (rtac (inj_int RS injD) 1);
   2.101 -by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
   2.102 -qed "nat_diff_distrib";
   2.103 -
   2.104 -
   2.105 -Goal "nat z - nat z' = \
   2.106 -\       (if neg z' then nat z  \
   2.107 -\        else let d = z-z' in    \
   2.108 -\             if neg d then 0 else nat d)";
   2.109 -by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
   2.110 -				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   2.111 -by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
   2.112 -qed "diff_nat_eq_if";
   2.113 -
   2.114 -Goalw [nat_number_of_def]
   2.115 -     "(number_of v :: nat) - number_of v' = \
   2.116 -\       (if neg (number_of v') then number_of v \
   2.117 -\        else let d = number_of (bin_add v (bin_minus v')) in    \
   2.118 -\             if neg d then #0 else nat d)";
   2.119 -by (simp_tac
   2.120 -    (simpset_of Int.thy delcongs [if_weak_cong]
   2.121 -			addsimps [not_neg_eq_ge_0, nat_0,
   2.122 -				  diff_nat_eq_if, diff_number_of_eq]) 1);
   2.123 -qed "diff_nat_number_of";
   2.124 -
   2.125 -Addsimps [diff_nat_number_of];
   2.126 -
   2.127 -
   2.128 -(** Multiplication **)
   2.129 -
   2.130 -Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
   2.131 -by (case_tac "#0 <= z'" 1);
   2.132 -by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
   2.133 -by (rtac (inj_int RS injD) 1);
   2.134 -by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
   2.135 -				      int_0_le_mult_iff]) 1);
   2.136 -qed "nat_mult_distrib";
   2.137 -
   2.138 -Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
   2.139 -by (rtac trans 1); 
   2.140 -by (rtac nat_mult_distrib 2); 
   2.141 -by Auto_tac;  
   2.142 -qed "nat_mult_distrib_neg";
   2.143 -
   2.144 -Goal "(number_of v :: nat) * number_of v' = \
   2.145 -\      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
   2.146 -by (simp_tac
   2.147 -    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   2.148 -				  nat_mult_distrib RS sym, number_of_mult, 
   2.149 -				  nat_0]) 1);
   2.150 -qed "mult_nat_number_of";
   2.151 -
   2.152 -Addsimps [mult_nat_number_of];
   2.153 -
   2.154 -
   2.155 -(** Quotient **)
   2.156 -
   2.157 -Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
   2.158 -by (case_tac "#0 <= z'" 1);
   2.159 -by (auto_tac (claset(), 
   2.160 -	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
   2.161 -by (zdiv_undefined_case_tac "z' = #0" 1);
   2.162 - by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
   2.163 -by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   2.164 -by (rename_tac "m m'" 1);
   2.165 -by (subgoal_tac "#0 <= int m div int m'" 1);
   2.166 - by (asm_full_simp_tac 
   2.167 -     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
   2.168 -by (rtac (inj_int RS injD) 1);
   2.169 -by (Asm_simp_tac 1);
   2.170 -by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
   2.171 - by (Force_tac 2);
   2.172 -by (asm_full_simp_tac 
   2.173 -    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   2.174 -	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
   2.175 -by (rtac (mod_div_equality RS sym RS trans) 1);
   2.176 -by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   2.177 -qed "nat_div_distrib";
   2.178 -
   2.179 -Goal "(number_of v :: nat)  div  number_of v' = \
   2.180 -\         (if neg (number_of v) then #0 \
   2.181 -\          else nat (number_of v div number_of v'))";
   2.182 -by (simp_tac
   2.183 -    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   2.184 -				  nat_div_distrib RS sym, nat_0]) 1);
   2.185 -qed "div_nat_number_of";
   2.186 -
   2.187 -Addsimps [div_nat_number_of];
   2.188 -
   2.189 -
   2.190 -(** Remainder **)
   2.191 -
   2.192 -(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
   2.193 -Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
   2.194 -by (zdiv_undefined_case_tac "z' = #0" 1);
   2.195 - by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
   2.196 -by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   2.197 -by (rename_tac "m m'" 1);
   2.198 -by (subgoal_tac "#0 <= int m mod int m'" 1);
   2.199 - by (asm_full_simp_tac 
   2.200 -     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
   2.201 -by (rtac (inj_int RS injD) 1);
   2.202 -by (Asm_simp_tac 1);
   2.203 -by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
   2.204 - by (Force_tac 2);
   2.205 -by (asm_full_simp_tac 
   2.206 -     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   2.207 -		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
   2.208 -by (rtac (mod_div_equality RS sym RS trans) 1);
   2.209 -by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   2.210 -qed "nat_mod_distrib";
   2.211 -
   2.212 -Goal "(number_of v :: nat)  mod  number_of v' = \
   2.213 -\       (if neg (number_of v) then #0 \
   2.214 -\        else if neg (number_of v') then number_of v \
   2.215 -\        else nat (number_of v mod number_of v'))";
   2.216 -by (simp_tac
   2.217 -    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   2.218 -				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   2.219 -				  nat_mod_distrib RS sym]) 1);
   2.220 -qed "mod_nat_number_of";
   2.221 -
   2.222 -Addsimps [mod_nat_number_of];
   2.223 -
   2.224 -
   2.225 -(*** Comparisons ***)
   2.226 -
   2.227 -(** Equals (=) **)
   2.228 -
   2.229 -Goal "[| (#0::int) <= z;  #0 <= z' |] ==> (nat z = nat z') = (z=z')";
   2.230 -by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   2.231 -qed "eq_nat_nat_iff";
   2.232 -
   2.233 -(*"neg" is used in rewrite rules for binary comparisons*)
   2.234 -Goal "((number_of v :: nat) = number_of v') = \
   2.235 -\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
   2.236 -\      else if neg (number_of v') then iszero (number_of v) \
   2.237 -\      else iszero (number_of (bin_add v (bin_minus v'))))";
   2.238 -by (simp_tac
   2.239 -    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   2.240 -				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   2.241 -by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
   2.242 -					   iszero_def]) 1);
   2.243 -by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
   2.244 -qed "eq_nat_number_of";
   2.245 -
   2.246 -Addsimps [eq_nat_number_of];
   2.247 -
   2.248 -(** Less-than (<) **)
   2.249 -
   2.250 -(*"neg" is used in rewrite rules for binary comparisons*)
   2.251 -Goal "((number_of v :: nat) < number_of v') = \
   2.252 -\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   2.253 -\         else neg (number_of (bin_add v (bin_minus v'))))";
   2.254 -by (simp_tac
   2.255 -    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   2.256 -				  nat_less_eq_zless, less_number_of_eq_neg,
   2.257 -				  nat_0]) 1);
   2.258 -by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, 
   2.259 -				number_of_minus, zless_nat_eq_int_zless]) 1);
   2.260 -qed "less_nat_number_of";
   2.261 -
   2.262 -Addsimps [less_nat_number_of];
   2.263 -
   2.264 -
   2.265 -(** Less-than-or-equals (<=) **)
   2.266 -
   2.267 -Goal "(number_of x <= (number_of y::nat)) = \
   2.268 -\     (~ number_of y < (number_of x::nat))";
   2.269 -by (rtac (linorder_not_less RS sym) 1);
   2.270 -qed "le_nat_number_of_eq_not_less"; 
   2.271 -
   2.272 -Addsimps [le_nat_number_of_eq_not_less];
   2.273 -
   2.274 -(*** New versions of existing theorems involving 0, 1, 2 ***)
   2.275 -
   2.276 -(*Maps n to #n for n = 0, 1, 2*)
   2.277 -val numeral_sym_ss = 
   2.278 -    HOL_ss addsimps [numeral_0_eq_0 RS sym, 
   2.279 -		     numeral_1_eq_1 RS sym, 
   2.280 -		     numeral_2_eq_2 RS sym,
   2.281 -		     Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
   2.282 -
   2.283 -fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
   2.284 -
   2.285 -(*Maps #n to n for n = 0, 1, 2*)
   2.286 -val numeral_ss = 
   2.287 -    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
   2.288 -
   2.289 -(** Nat **)
   2.290 -
   2.291 -Goal "#0 < n ==> n = Suc(n - #1)";
   2.292 -by (asm_full_simp_tac numeral_ss 1);
   2.293 -qed "Suc_pred'";
   2.294 -
   2.295 -(*Expresses a natural number constant as the Suc of another one.
   2.296 -  NOT suitable for rewriting because n recurs in the condition.*)
   2.297 -bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   2.298 -
   2.299 -(** NatDef & Nat **)
   2.300 -
   2.301 -Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
   2.302 -
   2.303 -AddIffs (map rename_numerals
   2.304 -	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
   2.305 -	  le0, le_0_eq, 
   2.306 -	  neq0_conv, zero_neq_conv, not_gr0]);
   2.307 -
   2.308 -(** Arith **)
   2.309 -
   2.310 -(*Identity laws for + - * *)	 
   2.311 -val basic_renamed_arith_simps =
   2.312 -    map rename_numerals
   2.313 -        [diff_0, diff_0_eq_0, add_0, add_0_right, 
   2.314 -	 mult_0, mult_0_right, mult_1, mult_1_right];
   2.315 -	 
   2.316 -(*Non-trivial simplifications*)	 
   2.317 -val other_renamed_arith_simps =
   2.318 -    map rename_numerals
   2.319 -	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
   2.320 -	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
   2.321 -
   2.322 -Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
   2.323 -
   2.324 -AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
   2.325 -
   2.326 -Goal "Suc n = n + #1";
   2.327 -by (asm_simp_tac numeral_ss 1);
   2.328 -qed "Suc_eq_add_numeral_1";
   2.329 -
   2.330 -(* These two can be useful when m = number_of... *)
   2.331 -
   2.332 -Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
   2.333 -by (case_tac "m" 1);
   2.334 -by (ALLGOALS (asm_simp_tac numeral_ss));
   2.335 -qed "add_eq_if";
   2.336 -
   2.337 -Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
   2.338 -by (case_tac "m" 1);
   2.339 -by (ALLGOALS (asm_simp_tac numeral_ss));
   2.340 -qed "mult_eq_if";
   2.341 -
   2.342 -Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
   2.343 -by (case_tac "m" 1);
   2.344 -by (ALLGOALS (asm_simp_tac numeral_ss));
   2.345 -qed "power_eq_if";
   2.346 -
   2.347 -Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
   2.348 -by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
   2.349 -qed "diff_less'";
   2.350 -
   2.351 -Addsimps [inst "n" "number_of ?v" diff_less'];
   2.352 -
   2.353 -(*various theorems that aren't in the default simpset*)
   2.354 -bind_thm ("add_is_one'", rename_numerals add_is_1);
   2.355 -bind_thm ("one_is_add'", rename_numerals one_is_add);
   2.356 -bind_thm ("zero_induct'", rename_numerals zero_induct);
   2.357 -bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
   2.358 -bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
   2.359 -bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
   2.360 -bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
   2.361 -
   2.362 -(** Divides **)
   2.363 -
   2.364 -Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]);
   2.365 -AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]);
   2.366 -
   2.367 -(*useful?*)
   2.368 -bind_thm ("mod_self'", rename_numerals mod_self);
   2.369 -bind_thm ("div_self'", rename_numerals div_self);
   2.370 -bind_thm ("div_less'", rename_numerals div_less);
   2.371 -bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0);
   2.372 -
   2.373 -(** Power **)
   2.374 -
   2.375 -Goal "(p::nat) ^ #0 = #1";
   2.376 -by (simp_tac numeral_ss 1);
   2.377 -qed "power_zero";
   2.378 -
   2.379 -Goal "(p::nat) ^ #1 = p";
   2.380 -by (simp_tac numeral_ss 1);
   2.381 -qed "power_one";
   2.382 -Addsimps [power_zero, power_one];
   2.383 -
   2.384 -Goal "(p::nat) ^ #2 = p*p";
   2.385 -by (simp_tac numeral_ss 1);
   2.386 -qed "power_two";
   2.387 -
   2.388 -Goal "#0 < (i::nat) ==> #0 < i^n";
   2.389 -by (asm_simp_tac numeral_ss 1);
   2.390 -qed "zero_less_power'";
   2.391 -Addsimps [zero_less_power'];
   2.392 -
   2.393 -bind_thm ("binomial_zero", rename_numerals binomial_0);
   2.394 -bind_thm ("binomial_Suc'", rename_numerals binomial_Suc);
   2.395 -bind_thm ("binomial_n_n'", rename_numerals binomial_n_n);
   2.396 -
   2.397 -(*binomial_0_Suc doesn't work well on numerals*)
   2.398 -Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]);
   2.399 -
   2.400 -Addsimps [rename_numerals card_Pow];
   2.401 -
   2.402 -(*** Comparisons involving (0::nat) ***)
   2.403 -
   2.404 -Goal "(number_of v = (0::nat)) = \
   2.405 -\     (if neg (number_of v) then True else iszero (number_of v))";
   2.406 -by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   2.407 -qed "eq_number_of_0";
   2.408 -
   2.409 -Goal "((0::nat) = number_of v) = \
   2.410 -\     (if neg (number_of v) then True else iszero (number_of v))";
   2.411 -by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
   2.412 -qed "eq_0_number_of";
   2.413 -
   2.414 -Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
   2.415 -by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   2.416 -qed "less_0_number_of";
   2.417 -
   2.418 -(*Simplification already handles n<0, n<=0 and 0<=n.*)
   2.419 -Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
   2.420 -
   2.421 -Goal "neg (number_of v) ==> number_of v = (0::nat)";
   2.422 -by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   2.423 -qed "neg_imp_number_of_eq_0";
   2.424 -
   2.425 -
   2.426 -
   2.427 -(*** Comparisons involving Suc ***)
   2.428 -
   2.429 -Goal "(number_of v = Suc n) = \
   2.430 -\       (let pv = number_of (bin_pred v) in \
   2.431 -\        if neg pv then False else nat pv = n)";
   2.432 -by (simp_tac
   2.433 -    (simpset_of Int.thy addsimps
   2.434 -      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   2.435 -       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   2.436 -by (res_inst_tac [("x", "number_of v")] spec 1);
   2.437 -by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
   2.438 -qed "eq_number_of_Suc";
   2.439 -
   2.440 -Goal "(Suc n = number_of v) = \
   2.441 -\       (let pv = number_of (bin_pred v) in \
   2.442 -\        if neg pv then False else nat pv = n)";
   2.443 -by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
   2.444 -qed "Suc_eq_number_of";
   2.445 -
   2.446 -Goal "(number_of v < Suc n) = \
   2.447 -\       (let pv = number_of (bin_pred v) in \
   2.448 -\        if neg pv then True else nat pv < n)";
   2.449 -by (simp_tac
   2.450 -    (simpset_of Int.thy addsimps
   2.451 -      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   2.452 -       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   2.453 -by (res_inst_tac [("x", "number_of v")] spec 1);
   2.454 -by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   2.455 -qed "less_number_of_Suc";
   2.456 -
   2.457 -Goal "(Suc n < number_of v) = \
   2.458 -\       (let pv = number_of (bin_pred v) in \
   2.459 -\        if neg pv then False else n < nat pv)";
   2.460 -by (simp_tac
   2.461 -    (simpset_of Int.thy addsimps
   2.462 -      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   2.463 -       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   2.464 -by (res_inst_tac [("x", "number_of v")] spec 1);
   2.465 -by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
   2.466 -qed "less_Suc_number_of";
   2.467 -
   2.468 -Goal "(number_of v <= Suc n) = \
   2.469 -\       (let pv = number_of (bin_pred v) in \
   2.470 -\        if neg pv then True else nat pv <= n)";
   2.471 -by (simp_tac
   2.472 -    (simpset () addsimps
   2.473 -      [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
   2.474 -qed "le_number_of_Suc";
   2.475 -
   2.476 -Goal "(Suc n <= number_of v) = \
   2.477 -\       (let pv = number_of (bin_pred v) in \
   2.478 -\        if neg pv then False else n <= nat pv)";
   2.479 -by (simp_tac
   2.480 -    (simpset () addsimps
   2.481 -      [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
   2.482 -qed "le_Suc_number_of";
   2.483 -
   2.484 -Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
   2.485 -	  less_number_of_Suc, less_Suc_number_of, 
   2.486 -	  le_number_of_Suc, le_Suc_number_of];
   2.487 -
   2.488 -(* Push int(.) inwards: *)
   2.489 -Addsimps [int_Suc,zadd_int RS sym];
   2.490 -
   2.491 -Goal "(m+m = n+n) = (m = (n::int))";
   2.492 -by Auto_tac;
   2.493 -val lemma1 = result();
   2.494 -
   2.495 -Goal "m+m ~= int 1 + n + n";
   2.496 -by Auto_tac;
   2.497 -by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   2.498 -by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   2.499 -val lemma2 = result();
   2.500 -
   2.501 -Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
   2.502 -\     (x=y & (((number_of v) ::int) = number_of w))"; 
   2.503 -by (simp_tac (simpset_of Int.thy addsimps
   2.504 -	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
   2.505 -qed "eq_number_of_BIT_BIT"; 
   2.506 -
   2.507 -Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
   2.508 -\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
   2.509 -by (simp_tac (simpset_of Int.thy addsimps
   2.510 -	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
   2.511 -by (res_inst_tac [("x", "number_of v")] spec 1);
   2.512 -by Safe_tac;
   2.513 -by (ALLGOALS Full_simp_tac);
   2.514 -by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   2.515 -by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   2.516 -qed "eq_number_of_BIT_Pls"; 
   2.517 -
   2.518 -Goal "((number_of (v BIT x) ::int) = number_of Min) = \
   2.519 -\     (x=True & (((number_of v) ::int) = number_of Min))"; 
   2.520 -by (simp_tac (simpset_of Int.thy addsimps
   2.521 -	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
   2.522 -by (res_inst_tac [("x", "number_of v")] spec 1);
   2.523 -by Auto_tac;
   2.524 -by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   2.525 -by Auto_tac;
   2.526 -qed "eq_number_of_BIT_Min"; 
   2.527 -
   2.528 -Goal "(number_of Pls ::int) ~= number_of Min"; 
   2.529 -by Auto_tac;
   2.530 -qed "eq_number_of_Pls_Min"; 
   2.531 -
   2.532 -
   2.533 -(*** Further lemmas about "nat" ***)
   2.534 -
   2.535 -Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
   2.536 -by (case_tac "z=#0 | w=#0" 1);
   2.537 -by Auto_tac;  
   2.538 -by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
   2.539 -                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
   2.540 -by (arith_tac 1);
   2.541 -qed "nat_abs_mult_distrib";
     3.1 --- a/src/HOL/Integ/NatBin.thy	Fri Dec 01 19:44:48 2000 +0100
     3.2 +++ b/src/HOL/Integ/NatBin.thy	Fri Dec 01 19:53:29 2000 +0100
     3.3 @@ -8,14 +8,16 @@
     3.4  This case is simply reduced to that for the non-negative integers
     3.5  *)
     3.6  
     3.7 -NatBin = IntPower +
     3.8 +theory NatBin = IntPower
     3.9 +files ("nat_bin.ML"):
    3.10  
    3.11 -instance
    3.12 -  nat :: number 
    3.13 +instance  nat :: number ..
    3.14  
    3.15  defs
    3.16 -  nat_number_of_def
    3.17 +  nat_number_of_def:
    3.18      "number_of v == nat (number_of v)"
    3.19       (*::bin=>nat        ::bin=>int*)
    3.20  
    3.21 +use "nat_bin.ML"	setup nat_bin_arith_setup
    3.22 +
    3.23  end
     4.1 --- a/src/HOL/Integ/int_arith1.ML	Fri Dec 01 19:44:48 2000 +0100
     4.2 +++ b/src/HOL/Integ/int_arith1.ML	Fri Dec 01 19:53:29 2000 +0100
     4.3 @@ -392,12 +392,13 @@
     4.4  
     4.5  (* reduce contradictory <= to False *)
     4.6  val add_rules = simp_thms @ bin_arith_simps @ bin_rel_simps @
     4.7 -                [int_0, zadd_0, zadd_0_right, zdiff_def,
     4.8 +                [zadd_0, zadd_0_right, zdiff_def,
     4.9  		 zadd_zminus_inverse, zadd_zminus_inverse2, 
    4.10  		 zmult_0, zmult_0_right, 
    4.11  		 zmult_1, zmult_1_right, 
    4.12  		 zmult_minus1, zmult_minus1_right,
    4.13 -		 zminus_zadd_distrib, zminus_zminus];
    4.14 +		 zminus_zadd_distrib, zminus_zminus,
    4.15 +                 int_0, zadd_int RS sym, int_Suc];
    4.16  
    4.17  val simprocs = [Int_Times_Assoc.conv, Int_Numeral_Simprocs.combine_numerals]@
    4.18                 Int_Numeral_Simprocs.cancel_numerals;
    4.19 @@ -415,12 +416,14 @@
    4.20  in
    4.21  
    4.22  val int_arith_setup =
    4.23 - [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
    4.24 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    4.25     {add_mono_thms = add_mono_thms @ add_mono_thms_int,
    4.26 +    inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
    4.27      lessD = lessD @ [add1_zle_eq RS iffD2],
    4.28      simpset = simpset addsimps add_rules
    4.29                        addsimprocs simprocs
    4.30                        addcongs [if_weak_cong]}),
    4.31 +  arith_inj_const ("IntDef.int", HOLogic.natT --> Type("IntDef.int",[])),
    4.32    arith_discrete ("IntDef.int", true)];
    4.33  
    4.34  end;
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Integ/nat_bin.ML	Fri Dec 01 19:53:29 2000 +0100
     5.3 @@ -0,0 +1,548 @@
     5.4 +(*  Title:      HOL/nat_bin.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1999  University of Cambridge
     5.8 +
     5.9 +Binary arithmetic for the natural numbers
    5.10 +*)
    5.11 +
    5.12 +val nat_number_of_def = thm "nat_number_of_def";
    5.13 +
    5.14 +(** nat (coercion from int to nat) **)
    5.15 +
    5.16 +Goal "nat (number_of w) = number_of w";
    5.17 +by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
    5.18 +qed "nat_number_of";
    5.19 +Addsimps [nat_number_of];
    5.20 +
    5.21 +(*These rewrites should one day be re-oriented...*)
    5.22 +
    5.23 +Goal "#0 = (0::nat)";
    5.24 +by (simp_tac (HOL_basic_ss addsimps [nat_0, nat_number_of_def]) 1);
    5.25 +qed "numeral_0_eq_0";
    5.26 +
    5.27 +Goal "#1 = (1::nat)";
    5.28 +by (simp_tac (HOL_basic_ss addsimps [nat_1, nat_number_of_def]) 1);
    5.29 +qed "numeral_1_eq_1";
    5.30 +
    5.31 +Goal "#2 = (2::nat)";
    5.32 +by (simp_tac (HOL_basic_ss addsimps [nat_2, nat_number_of_def]) 1);
    5.33 +qed "numeral_2_eq_2";
    5.34 +
    5.35 +bind_thm ("zero_eq_numeral_0", numeral_0_eq_0 RS sym);
    5.36 +
    5.37 +(** int (coercion from nat to int) **)
    5.38 +
    5.39 +(*"neg" is used in rewrite rules for binary comparisons*)
    5.40 +Goal "int (number_of v :: nat) = \
    5.41 +\        (if neg (number_of v) then #0 \
    5.42 +\         else (number_of v :: int))";
    5.43 +by (simp_tac
    5.44 +    (simpset_of Int.thy addsimps [neg_nat, nat_number_of_def, 
    5.45 +				  not_neg_nat, int_0]) 1);
    5.46 +qed "int_nat_number_of";
    5.47 +Addsimps [int_nat_number_of];
    5.48 +
    5.49 +
    5.50 +val nat_bin_arith_setup =
    5.51 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    5.52 +   {add_mono_thms = add_mono_thms,
    5.53 +    inj_thms = inj_thms,
    5.54 +    lessD = lessD,
    5.55 +    simpset = simpset addsimps [int_nat_number_of,
    5.56 + not_neg_number_of_Pls,neg_number_of_Min,neg_number_of_BIT]})];
    5.57 +
    5.58 +(** Successor **)
    5.59 +
    5.60 +Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)";
    5.61 +by (rtac sym 1);
    5.62 +by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1);
    5.63 +qed "Suc_nat_eq_nat_zadd1";
    5.64 +
    5.65 +Goal "Suc (number_of v) = \
    5.66 +\       (if neg (number_of v) then #1 else number_of (bin_succ v))";
    5.67 +by (simp_tac
    5.68 +    (simpset_of Int.thy addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
    5.69 +				  nat_number_of_def, int_Suc, 
    5.70 +				  Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
    5.71 +qed "Suc_nat_number_of";
    5.72 +Addsimps [Suc_nat_number_of];
    5.73 +
    5.74 +Goal "Suc (number_of v + n) = \
    5.75 +\       (if neg (number_of v) then #1+n else number_of (bin_succ v) + n)";
    5.76 +by (Simp_tac 1);
    5.77 +qed "Suc_nat_number_of_add";
    5.78 +
    5.79 +Goal "Suc #0 = #1";
    5.80 +by (Simp_tac 1);
    5.81 +qed "Suc_numeral_0_eq_1";
    5.82 +
    5.83 +Goal "Suc #1 = #2";
    5.84 +by (Simp_tac 1);
    5.85 +qed "Suc_numeral_1_eq_2";
    5.86 +
    5.87 +(** Addition **)
    5.88 +
    5.89 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z+z') = nat z + nat z'";
    5.90 +by (rtac (inj_int RS injD) 1);
    5.91 +by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
    5.92 +qed "nat_add_distrib";
    5.93 +
    5.94 +(*"neg" is used in rewrite rules for binary comparisons*)
    5.95 +Goal "(number_of v :: nat) + number_of v' = \
    5.96 +\        (if neg (number_of v) then number_of v' \
    5.97 +\         else if neg (number_of v') then number_of v \
    5.98 +\         else number_of (bin_add v v'))";
    5.99 +by (simp_tac
   5.100 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   5.101 +				  nat_add_distrib RS sym, number_of_add]) 1);
   5.102 +qed "add_nat_number_of";
   5.103 +
   5.104 +Addsimps [add_nat_number_of];
   5.105 +
   5.106 +
   5.107 +(** Subtraction **)
   5.108 +
   5.109 +Goal "[| (#0::int) <= z';  z' <= z |] ==> nat (z-z') = nat z - nat z'";
   5.110 +by (rtac (inj_int RS injD) 1);
   5.111 +by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
   5.112 +qed "nat_diff_distrib";
   5.113 +
   5.114 +
   5.115 +Goal "nat z - nat z' = \
   5.116 +\       (if neg z' then nat z  \
   5.117 +\        else let d = z-z' in    \
   5.118 +\             if neg d then 0 else nat d)";
   5.119 +by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
   5.120 +				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   5.121 +by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
   5.122 +qed "diff_nat_eq_if";
   5.123 +
   5.124 +Goalw [nat_number_of_def]
   5.125 +     "(number_of v :: nat) - number_of v' = \
   5.126 +\       (if neg (number_of v') then number_of v \
   5.127 +\        else let d = number_of (bin_add v (bin_minus v')) in    \
   5.128 +\             if neg d then #0 else nat d)";
   5.129 +by (simp_tac
   5.130 +    (simpset_of Int.thy delcongs [if_weak_cong]
   5.131 +			addsimps [not_neg_eq_ge_0, nat_0,
   5.132 +				  diff_nat_eq_if, diff_number_of_eq]) 1);
   5.133 +qed "diff_nat_number_of";
   5.134 +
   5.135 +Addsimps [diff_nat_number_of];
   5.136 +
   5.137 +
   5.138 +(** Multiplication **)
   5.139 +
   5.140 +Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
   5.141 +by (case_tac "#0 <= z'" 1);
   5.142 +by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
   5.143 +by (rtac (inj_int RS injD) 1);
   5.144 +by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
   5.145 +				      int_0_le_mult_iff]) 1);
   5.146 +qed "nat_mult_distrib";
   5.147 +
   5.148 +Goal "z <= (#0::int) ==> nat(z*z') = nat(-z) * nat(-z')"; 
   5.149 +by (rtac trans 1); 
   5.150 +by (rtac nat_mult_distrib 2); 
   5.151 +by Auto_tac;  
   5.152 +qed "nat_mult_distrib_neg";
   5.153 +
   5.154 +Goal "(number_of v :: nat) * number_of v' = \
   5.155 +\      (if neg (number_of v) then #0 else number_of (bin_mult v v'))";
   5.156 +by (simp_tac
   5.157 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   5.158 +				  nat_mult_distrib RS sym, number_of_mult, 
   5.159 +				  nat_0]) 1);
   5.160 +qed "mult_nat_number_of";
   5.161 +
   5.162 +Addsimps [mult_nat_number_of];
   5.163 +
   5.164 +
   5.165 +(** Quotient **)
   5.166 +
   5.167 +Goal "(#0::int) <= z ==> nat (z div z') = nat z div nat z'";
   5.168 +by (case_tac "#0 <= z'" 1);
   5.169 +by (auto_tac (claset(), 
   5.170 +	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
   5.171 +by (zdiv_undefined_case_tac "z' = #0" 1);
   5.172 + by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
   5.173 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   5.174 +by (rename_tac "m m'" 1);
   5.175 +by (subgoal_tac "#0 <= int m div int m'" 1);
   5.176 + by (asm_full_simp_tac 
   5.177 +     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
   5.178 +by (rtac (inj_int RS injD) 1);
   5.179 +by (Asm_simp_tac 1);
   5.180 +by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
   5.181 + by (Force_tac 2);
   5.182 +by (asm_full_simp_tac 
   5.183 +    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   5.184 +	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
   5.185 +by (rtac (mod_div_equality RS sym RS trans) 1);
   5.186 +by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   5.187 +qed "nat_div_distrib";
   5.188 +
   5.189 +Goal "(number_of v :: nat)  div  number_of v' = \
   5.190 +\         (if neg (number_of v) then #0 \
   5.191 +\          else nat (number_of v div number_of v'))";
   5.192 +by (simp_tac
   5.193 +    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   5.194 +				  nat_div_distrib RS sym, nat_0]) 1);
   5.195 +qed "div_nat_number_of";
   5.196 +
   5.197 +Addsimps [div_nat_number_of];
   5.198 +
   5.199 +
   5.200 +(** Remainder **)
   5.201 +
   5.202 +(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
   5.203 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
   5.204 +by (zdiv_undefined_case_tac "z' = #0" 1);
   5.205 + by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
   5.206 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   5.207 +by (rename_tac "m m'" 1);
   5.208 +by (subgoal_tac "#0 <= int m mod int m'" 1);
   5.209 + by (asm_full_simp_tac 
   5.210 +     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
   5.211 +by (rtac (inj_int RS injD) 1);
   5.212 +by (Asm_simp_tac 1);
   5.213 +by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
   5.214 + by (Force_tac 2);
   5.215 +by (asm_full_simp_tac 
   5.216 +     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
   5.217 +		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
   5.218 +by (rtac (mod_div_equality RS sym RS trans) 1);
   5.219 +by (asm_simp_tac (simpset() addsimps add_ac@mult_ac) 1);
   5.220 +qed "nat_mod_distrib";
   5.221 +
   5.222 +Goal "(number_of v :: nat)  mod  number_of v' = \
   5.223 +\       (if neg (number_of v) then #0 \
   5.224 +\        else if neg (number_of v') then number_of v \
   5.225 +\        else nat (number_of v mod number_of v'))";
   5.226 +by (simp_tac
   5.227 +    (simpset_of Int.thy addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   5.228 +				  neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   5.229 +				  nat_mod_distrib RS sym]) 1);
   5.230 +qed "mod_nat_number_of";
   5.231 +
   5.232 +Addsimps [mod_nat_number_of];
   5.233 +
   5.234 +
   5.235 +(*** Comparisons ***)
   5.236 +
   5.237 +(** Equals (=) **)
   5.238 +
   5.239 +Goal "[| (#0::int) <= z;  #0 <= z' |] ==> (nat z = nat z') = (z=z')";
   5.240 +by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   5.241 +qed "eq_nat_nat_iff";
   5.242 +
   5.243 +(*"neg" is used in rewrite rules for binary comparisons*)
   5.244 +Goal "((number_of v :: nat) = number_of v') = \
   5.245 +\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
   5.246 +\      else if neg (number_of v') then iszero (number_of v) \
   5.247 +\      else iszero (number_of (bin_add v (bin_minus v'))))";
   5.248 +by (simp_tac
   5.249 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   5.250 +				  eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   5.251 +by (simp_tac (simpset_of Int.thy addsimps [nat_eq_iff, nat_eq_iff2, 
   5.252 +					   iszero_def]) 1);
   5.253 +by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
   5.254 +qed "eq_nat_number_of";
   5.255 +
   5.256 +Addsimps [eq_nat_number_of];
   5.257 +
   5.258 +(** Less-than (<) **)
   5.259 +
   5.260 +(*"neg" is used in rewrite rules for binary comparisons*)
   5.261 +Goal "((number_of v :: nat) < number_of v') = \
   5.262 +\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   5.263 +\         else neg (number_of (bin_add v (bin_minus v'))))";
   5.264 +by (simp_tac
   5.265 +    (simpset_of Int.thy addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   5.266 +				  nat_less_eq_zless, less_number_of_eq_neg,
   5.267 +				  nat_0]) 1);
   5.268 +by (simp_tac (simpset_of Int.thy addsimps [neg_eq_less_int0, zminus_zless, 
   5.269 +				number_of_minus, zless_nat_eq_int_zless]) 1);
   5.270 +qed "less_nat_number_of";
   5.271 +
   5.272 +Addsimps [less_nat_number_of];
   5.273 +
   5.274 +
   5.275 +(** Less-than-or-equals (<=) **)
   5.276 +
   5.277 +Goal "(number_of x <= (number_of y::nat)) = \
   5.278 +\     (~ number_of y < (number_of x::nat))";
   5.279 +by (rtac (linorder_not_less RS sym) 1);
   5.280 +qed "le_nat_number_of_eq_not_less"; 
   5.281 +
   5.282 +Addsimps [le_nat_number_of_eq_not_less];
   5.283 +
   5.284 +(*** New versions of existing theorems involving 0, 1, 2 ***)
   5.285 +
   5.286 +(*Maps n to #n for n = 0, 1, 2*)
   5.287 +val numeral_sym_ss = 
   5.288 +    HOL_ss addsimps [numeral_0_eq_0 RS sym, 
   5.289 +		     numeral_1_eq_1 RS sym, 
   5.290 +		     numeral_2_eq_2 RS sym,
   5.291 +		     Suc_numeral_1_eq_2, Suc_numeral_0_eq_1];
   5.292 +
   5.293 +fun rename_numerals th = simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
   5.294 +
   5.295 +(*Maps #n to n for n = 0, 1, 2*)
   5.296 +val numeral_ss = 
   5.297 +    simpset() addsimps [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2];
   5.298 +
   5.299 +(** Nat **)
   5.300 +
   5.301 +Goal "#0 < n ==> n = Suc(n - #1)";
   5.302 +by (asm_full_simp_tac numeral_ss 1);
   5.303 +qed "Suc_pred'";
   5.304 +
   5.305 +(*Expresses a natural number constant as the Suc of another one.
   5.306 +  NOT suitable for rewriting because n recurs in the condition.*)
   5.307 +bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   5.308 +
   5.309 +(** NatDef & Nat **)
   5.310 +
   5.311 +Addsimps (map rename_numerals [min_0L, min_0R, max_0L, max_0R]);
   5.312 +
   5.313 +AddIffs (map rename_numerals
   5.314 +	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
   5.315 +	  le0, le_0_eq, 
   5.316 +	  neq0_conv, zero_neq_conv, not_gr0]);
   5.317 +
   5.318 +(** Arith **)
   5.319 +
   5.320 +(*Identity laws for + - * *)	 
   5.321 +val basic_renamed_arith_simps =
   5.322 +    map rename_numerals
   5.323 +        [diff_0, diff_0_eq_0, add_0, add_0_right, 
   5.324 +	 mult_0, mult_0_right, mult_1, mult_1_right];
   5.325 +	 
   5.326 +(*Non-trivial simplifications*)	 
   5.327 +val other_renamed_arith_simps =
   5.328 +    map rename_numerals
   5.329 +	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
   5.330 +	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
   5.331 +
   5.332 +Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
   5.333 +
   5.334 +AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
   5.335 +
   5.336 +Goal "Suc n = n + #1";
   5.337 +by (asm_simp_tac numeral_ss 1);
   5.338 +qed "Suc_eq_add_numeral_1";
   5.339 +
   5.340 +(* These two can be useful when m = number_of... *)
   5.341 +
   5.342 +Goal "(m::nat) + n = (if m=#0 then n else Suc ((m - #1) + n))";
   5.343 +by (case_tac "m" 1);
   5.344 +by (ALLGOALS (asm_simp_tac numeral_ss));
   5.345 +qed "add_eq_if";
   5.346 +
   5.347 +Goal "(m::nat) * n = (if m=#0 then #0 else n + ((m - #1) * n))";
   5.348 +by (case_tac "m" 1);
   5.349 +by (ALLGOALS (asm_simp_tac numeral_ss));
   5.350 +qed "mult_eq_if";
   5.351 +
   5.352 +Goal "(p ^ m :: nat) = (if m=#0 then #1 else p * (p ^ (m - #1)))";
   5.353 +by (case_tac "m" 1);
   5.354 +by (ALLGOALS (asm_simp_tac numeral_ss));
   5.355 +qed "power_eq_if";
   5.356 +
   5.357 +Goal "[| #0<n; #0<m |] ==> m - n < (m::nat)";
   5.358 +by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
   5.359 +qed "diff_less'";
   5.360 +
   5.361 +Addsimps [inst "n" "number_of ?v" diff_less'];
   5.362 +
   5.363 +(*various theorems that aren't in the default simpset*)
   5.364 +bind_thm ("add_is_one'", rename_numerals add_is_1);
   5.365 +bind_thm ("one_is_add'", rename_numerals one_is_add);
   5.366 +bind_thm ("zero_induct'", rename_numerals zero_induct);
   5.367 +bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
   5.368 +bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
   5.369 +bind_thm ("le_pred_eq'", rename_numerals le_pred_eq);
   5.370 +bind_thm ("less_pred_eq'", rename_numerals less_pred_eq);
   5.371 +
   5.372 +(** Divides **)
   5.373 +
   5.374 +Addsimps (map rename_numerals [mod_1, mod_0, div_1, div_0]);
   5.375 +AddIffs (map rename_numerals [dvd_1_left, dvd_0_right]);
   5.376 +
   5.377 +(*useful?*)
   5.378 +bind_thm ("mod_self'", rename_numerals mod_self);
   5.379 +bind_thm ("div_self'", rename_numerals div_self);
   5.380 +bind_thm ("div_less'", rename_numerals div_less);
   5.381 +bind_thm ("mod_mult_self_is_zero'", rename_numerals mod_mult_self_is_0);
   5.382 +
   5.383 +(** Power **)
   5.384 +
   5.385 +Goal "(p::nat) ^ #0 = #1";
   5.386 +by (simp_tac numeral_ss 1);
   5.387 +qed "power_zero";
   5.388 +
   5.389 +Goal "(p::nat) ^ #1 = p";
   5.390 +by (simp_tac numeral_ss 1);
   5.391 +qed "power_one";
   5.392 +Addsimps [power_zero, power_one];
   5.393 +
   5.394 +Goal "(p::nat) ^ #2 = p*p";
   5.395 +by (simp_tac numeral_ss 1);
   5.396 +qed "power_two";
   5.397 +
   5.398 +Goal "#0 < (i::nat) ==> #0 < i^n";
   5.399 +by (asm_simp_tac numeral_ss 1);
   5.400 +qed "zero_less_power'";
   5.401 +Addsimps [zero_less_power'];
   5.402 +
   5.403 +bind_thm ("binomial_zero", rename_numerals binomial_0);
   5.404 +bind_thm ("binomial_Suc'", rename_numerals binomial_Suc);
   5.405 +bind_thm ("binomial_n_n'", rename_numerals binomial_n_n);
   5.406 +
   5.407 +(*binomial_0_Suc doesn't work well on numerals*)
   5.408 +Addsimps (map rename_numerals [binomial_n_0, binomial_zero, binomial_1]);
   5.409 +
   5.410 +Addsimps [rename_numerals card_Pow];
   5.411 +
   5.412 +(*** Comparisons involving (0::nat) ***)
   5.413 +
   5.414 +Goal "(number_of v = (0::nat)) = \
   5.415 +\     (if neg (number_of v) then True else iszero (number_of v))";
   5.416 +by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   5.417 +qed "eq_number_of_0";
   5.418 +
   5.419 +Goal "((0::nat) = number_of v) = \
   5.420 +\     (if neg (number_of v) then True else iszero (number_of v))";
   5.421 +by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
   5.422 +qed "eq_0_number_of";
   5.423 +
   5.424 +Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
   5.425 +by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   5.426 +qed "less_0_number_of";
   5.427 +
   5.428 +(*Simplification already handles n<0, n<=0 and 0<=n.*)
   5.429 +Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
   5.430 +
   5.431 +Goal "neg (number_of v) ==> number_of v = (0::nat)";
   5.432 +by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   5.433 +qed "neg_imp_number_of_eq_0";
   5.434 +
   5.435 +
   5.436 +
   5.437 +(*** Comparisons involving Suc ***)
   5.438 +
   5.439 +Goal "(number_of v = Suc n) = \
   5.440 +\       (let pv = number_of (bin_pred v) in \
   5.441 +\        if neg pv then False else nat pv = n)";
   5.442 +by (simp_tac
   5.443 +    (simpset_of Int.thy addsimps
   5.444 +      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   5.445 +       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   5.446 +by (res_inst_tac [("x", "number_of v")] spec 1);
   5.447 +by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
   5.448 +qed "eq_number_of_Suc";
   5.449 +
   5.450 +Goal "(Suc n = number_of v) = \
   5.451 +\       (let pv = number_of (bin_pred v) in \
   5.452 +\        if neg pv then False else nat pv = n)";
   5.453 +by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
   5.454 +qed "Suc_eq_number_of";
   5.455 +
   5.456 +Goal "(number_of v < Suc n) = \
   5.457 +\       (let pv = number_of (bin_pred v) in \
   5.458 +\        if neg pv then True else nat pv < n)";
   5.459 +by (simp_tac
   5.460 +    (simpset_of Int.thy addsimps
   5.461 +      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   5.462 +       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   5.463 +by (res_inst_tac [("x", "number_of v")] spec 1);
   5.464 +by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   5.465 +qed "less_number_of_Suc";
   5.466 +
   5.467 +Goal "(Suc n < number_of v) = \
   5.468 +\       (let pv = number_of (bin_pred v) in \
   5.469 +\        if neg pv then False else n < nat pv)";
   5.470 +by (simp_tac
   5.471 +    (simpset_of Int.thy addsimps
   5.472 +      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   5.473 +       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   5.474 +by (res_inst_tac [("x", "number_of v")] spec 1);
   5.475 +by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
   5.476 +qed "less_Suc_number_of";
   5.477 +
   5.478 +Goal "(number_of v <= Suc n) = \
   5.479 +\       (let pv = number_of (bin_pred v) in \
   5.480 +\        if neg pv then True else nat pv <= n)";
   5.481 +by (simp_tac
   5.482 +    (simpset () addsimps
   5.483 +      [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
   5.484 +qed "le_number_of_Suc";
   5.485 +
   5.486 +Goal "(Suc n <= number_of v) = \
   5.487 +\       (let pv = number_of (bin_pred v) in \
   5.488 +\        if neg pv then False else n <= nat pv)";
   5.489 +by (simp_tac
   5.490 +    (simpset () addsimps
   5.491 +      [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
   5.492 +qed "le_Suc_number_of";
   5.493 +
   5.494 +Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
   5.495 +	  less_number_of_Suc, less_Suc_number_of, 
   5.496 +	  le_number_of_Suc, le_Suc_number_of];
   5.497 +
   5.498 +(* Push int(.) inwards: *)
   5.499 +Addsimps [int_Suc,zadd_int RS sym];
   5.500 +
   5.501 +Goal "(m+m = n+n) = (m = (n::int))";
   5.502 +by Auto_tac;
   5.503 +val lemma1 = result();
   5.504 +
   5.505 +Goal "m+m ~= int 1 + n + n";
   5.506 +by Auto_tac;
   5.507 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   5.508 +by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   5.509 +val lemma2 = result();
   5.510 +
   5.511 +Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
   5.512 +\     (x=y & (((number_of v) ::int) = number_of w))"; 
   5.513 +by (simp_tac (simpset_of Int.thy addsimps
   5.514 +	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
   5.515 +qed "eq_number_of_BIT_BIT"; 
   5.516 +
   5.517 +Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
   5.518 +\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
   5.519 +by (simp_tac (simpset_of Int.thy addsimps
   5.520 +	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
   5.521 +by (res_inst_tac [("x", "number_of v")] spec 1);
   5.522 +by Safe_tac;
   5.523 +by (ALLGOALS Full_simp_tac);
   5.524 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   5.525 +by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   5.526 +qed "eq_number_of_BIT_Pls"; 
   5.527 +
   5.528 +Goal "((number_of (v BIT x) ::int) = number_of Min) = \
   5.529 +\     (x=True & (((number_of v) ::int) = number_of Min))"; 
   5.530 +by (simp_tac (simpset_of Int.thy addsimps
   5.531 +	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
   5.532 +by (res_inst_tac [("x", "number_of v")] spec 1);
   5.533 +by Auto_tac;
   5.534 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
   5.535 +by Auto_tac;
   5.536 +qed "eq_number_of_BIT_Min"; 
   5.537 +
   5.538 +Goal "(number_of Pls ::int) ~= number_of Min"; 
   5.539 +by Auto_tac;
   5.540 +qed "eq_number_of_Pls_Min"; 
   5.541 +
   5.542 +
   5.543 +(*** Further lemmas about "nat" ***)
   5.544 +
   5.545 +Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
   5.546 +by (case_tac "z=#0 | w=#0" 1);
   5.547 +by Auto_tac;  
   5.548 +by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym, 
   5.549 +                          nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
   5.550 +by (arith_tac 1);
   5.551 +qed "nat_abs_mult_distrib";
     6.1 --- a/src/HOL/Integ/nat_simprocs.ML	Fri Dec 01 19:44:48 2000 +0100
     6.2 +++ b/src/HOL/Integ/nat_simprocs.ML	Fri Dec 01 19:53:29 2000 +0100
     6.3 @@ -466,8 +466,8 @@
     6.4  in
     6.5  
     6.6  val nat_simprocs_setup =
     6.7 - [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
     6.8 -   {add_mono_thms = add_mono_thms, lessD = lessD,
     6.9 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    6.10 +   {add_mono_thms = add_mono_thms, inj_thms = inj_thms, lessD = lessD,
    6.11      simpset = simpset addsimps add_rules
    6.12                        addsimps basic_renamed_arith_simps
    6.13                        addsimprocs simprocs})];
     7.1 --- a/src/HOL/IsaMakefile	Fri Dec 01 19:44:48 2000 +0100
     7.2 +++ b/src/HOL/IsaMakefile	Fri Dec 01 19:53:29 2000 +0100
     7.3 @@ -78,7 +78,7 @@
     7.4    Integ/Equiv.ML Integ/Equiv.thy Integ/Int.ML Integ/Int.thy \
     7.5    Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \
     7.6    Integ/IntDiv.ML Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \
     7.7 -  Integ/NatBin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
     7.8 +  Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
     7.9    Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
    7.10    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
    7.11    Inverse_Image.ML Inverse_Image.thy Lfp.ML \
     8.1 --- a/src/HOL/Real/RealArith.ML	Fri Dec 01 19:44:48 2000 +0100
     8.2 +++ b/src/HOL/Real/RealArith.ML	Fri Dec 01 19:53:29 2000 +0100
     8.3 @@ -1,4 +1,3 @@
     8.4 -
     8.5  (*useful??*)
     8.6  Goal "(z = z + w) = (w = (#0::real))";
     8.7  by Auto_tac;
     9.1 --- a/src/HOL/Real/RealArith.thy	Fri Dec 01 19:44:48 2000 +0100
     9.2 +++ b/src/HOL/Real/RealArith.thy	Fri Dec 01 19:53:29 2000 +0100
     9.3 @@ -1,4 +1,3 @@
     9.4 -
     9.5  theory RealArith = RealBin
     9.6  files "real_arith.ML":
     9.7  
    10.1 --- a/src/HOL/Real/real_arith.ML	Fri Dec 01 19:44:48 2000 +0100
    10.2 +++ b/src/HOL/Real/real_arith.ML	Fri Dec 01 19:53:29 2000 +0100
    10.3 @@ -53,8 +53,9 @@
    10.4    "fast_real_arith" real_arith_simproc_pats Fast_Arith.lin_arith_prover;
    10.5  
    10.6  val real_arith_setup =
    10.7 - [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset} =>
    10.8 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
    10.9     {add_mono_thms = add_mono_thms @ add_mono_thms_real,
   10.10 +    inj_thms = inj_thms, (*FIXME: add real*)
   10.11      lessD = lessD,  (*We don't change LA_Data_Ref.lessD because the real ordering is dense!*)
   10.12      simpset = simpset addsimps simps@add_rules
   10.13                        addsimprocs simprocs
    11.1 --- a/src/HOL/arith_data.ML	Fri Dec 01 19:44:48 2000 +0100
    11.2 +++ b/src/HOL/arith_data.ML	Fri Dec 01 19:53:29 2000 +0100
    11.3 @@ -265,24 +265,29 @@
    11.4  structure ArithTheoryDataArgs =
    11.5  struct
    11.6    val name = "HOL/arith";
    11.7 -  type T = {splits: thm list, discrete: (string * bool) list};
    11.8 +  type T = {splits: thm list, inj_consts: (string * typ)list, discrete: (string * bool) list};
    11.9  
   11.10 -  val empty = {splits = [], discrete = []};
   11.11 +  val empty = {splits = [], inj_consts = [], discrete = []};
   11.12    val copy = I;
   11.13    val prep_ext = I;
   11.14 -  fun merge ({splits = splits1, discrete = discrete1}, {splits = splits2, discrete = discrete2}) =
   11.15 +  fun merge ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
   11.16 +             {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) =
   11.17     {splits = Drule.merge_rules (splits1, splits2),
   11.18 +    inj_consts = merge_lists inj_consts1 inj_consts2,
   11.19      discrete = merge_alists discrete1 discrete2};
   11.20    fun print _ _ = ();
   11.21  end;
   11.22  
   11.23  structure ArithTheoryData = TheoryDataFun(ArithTheoryDataArgs);
   11.24  
   11.25 -fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits, discrete} =>
   11.26 -  {splits = thm :: splits, discrete = discrete}) thy, thm);
   11.27 +fun arith_split_add (thy, thm) = (ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
   11.28 +  {splits= thm::splits, inj_consts= inj_consts, discrete= discrete}) thy, thm);
   11.29  
   11.30 -fun arith_discrete d = ArithTheoryData.map (fn {splits, discrete} =>
   11.31 -  {splits = splits, discrete = d :: discrete});
   11.32 +fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
   11.33 +  {splits = splits, inj_consts = inj_consts, discrete = d :: discrete});
   11.34 +
   11.35 +fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete} =>
   11.36 +  {splits = splits, inj_consts = c :: inj_consts, discrete = discrete});
   11.37  
   11.38  
   11.39  structure LA_Data_Ref: LIN_ARITH_DATA =
   11.40 @@ -296,6 +301,9 @@
   11.41  fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
   11.42                             | Some n => (overwrite(p,(t,n+m:int)), i));
   11.43  
   11.44 +fun decomp2 inj_consts (rel,lhs,rhs) =
   11.45 +
   11.46 +let
   11.47  (* Turn term into list of summand * multiplicity plus a constant *)
   11.48  fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   11.49    | poly(all as Const("op -",T) $ s $ t, m, pi) =
   11.50 @@ -313,10 +321,11 @@
   11.51    | poly(all as Const("Numeral.number_of",_)$t,m,(p,i)) =
   11.52       ((p,i + m*HOLogic.dest_binum t)
   11.53        handle TERM _ => add_atom(all,m,(p,i)))
   11.54 +  | poly(all as Const f $ x, m, pi) =
   11.55 +      if f mem inj_consts then poly(x,m,pi) else add_atom(all,m,pi)
   11.56    | poly x  = add_atom x;
   11.57  
   11.58 -fun decomp2(rel,lhs,rhs) =
   11.59 -  let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
   11.60 +  val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
   11.61    in case rel of
   11.62         "op <"  => Some(p,i,"<",q,j)
   11.63       | "op <=" => Some(p,i,"<=",q,j)
   11.64 @@ -327,22 +336,24 @@
   11.65  fun negate(Some(x,i,rel,y,j,d)) = Some(x,i,"~"^rel,y,j,d)
   11.66    | negate None = None;
   11.67  
   11.68 -fun decomp1 discrete (T,xxx) =
   11.69 +fun decomp1 (discrete,inj_consts) (T,xxx) =
   11.70    (case T of
   11.71       Type("fun",[Type(D,[]),_]) =>
   11.72         (case assoc(discrete,D) of
   11.73            None => None
   11.74 -        | Some d => (case decomp2 xxx of
   11.75 +        | Some d => (case decomp2 inj_consts xxx of
   11.76                         None => None
   11.77                       | Some(p,i,rel,q,j) => Some(p,i,rel,q,j,d)))
   11.78     | _ => None);
   11.79  
   11.80 -fun decomp2 discrete (_$(Const(rel,T)$lhs$rhs)) = decomp1 discrete (T,(rel,lhs,rhs))
   11.81 -  | decomp2 discrete (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   11.82 -      negate(decomp1 discrete (T,(rel,lhs,rhs)))
   11.83 -  | decomp2 discrete _ = None
   11.84 +fun decomp2 data (_$(Const(rel,T)$lhs$rhs)) = decomp1 data (T,(rel,lhs,rhs))
   11.85 +  | decomp2 data (_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   11.86 +      negate(decomp1 data (T,(rel,lhs,rhs)))
   11.87 +  | decomp2 data _ = None
   11.88  
   11.89 -val decomp = decomp2 o #discrete o ArithTheoryData.get_sg;
   11.90 +fun decomp sg =
   11.91 +  let val {discrete, inj_consts, ...} = ArithTheoryData.get_sg sg
   11.92 +  in decomp2 (discrete,inj_consts) end
   11.93  
   11.94  end;
   11.95  
   11.96 @@ -373,8 +384,9 @@
   11.97  
   11.98  val init_lin_arith_data =
   11.99   Fast_Arith.setup @
  11.100 - [Fast_Arith.map_data (fn {add_mono_thms, lessD, simpset = _} =>
  11.101 + [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset = _} =>
  11.102     {add_mono_thms = add_mono_thms @ add_mono_thms_nat,
  11.103 +    inj_thms = inj_thms,
  11.104      lessD = lessD @ [Suc_leI],
  11.105      simpset = HOL_basic_ss addsimps add_rules addsimprocs nat_cancel_sums_add}),
  11.106    ArithTheoryData.init, arith_discrete ("nat", true)];
  11.107 @@ -416,7 +428,7 @@
  11.108  
  11.109  in
  11.110  
  11.111 -val arith_tac = atomize_tac THEN' raw_arith_tac;
  11.112 +val arith_tac = fast_arith_tac ORELSE' (atomize_tac THEN' raw_arith_tac);
  11.113  
  11.114  fun arith_method prems =
  11.115    Method.METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));