Tidying of the integer development; towards removing the
authorpaulson
Thu Dec 04 10:29:17 2003 +0100 (2003-12-04)
changeset 142725efbb548107d
parent 14271 8ed6989228bb
child 14273 e33ffff0123c
Tidying of the integer development; towards removing the
abel_cancel simproc
src/HOL/Integ/Bin.ML
src/HOL/Integ/Bin.thy
src/HOL/Integ/Int.thy
src/HOL/Integ/IntArith.thy
src/HOL/Integ/NatBin.thy
src/HOL/Integ/NatSimprocs.ML
src/HOL/Integ/int_arith1.ML
src/HOL/Integ/nat_bin.ML
src/HOL/IsaMakefile
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Integ/Bin.ML	Wed Dec 03 10:49:34 2003 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,503 +0,0 @@
     1.4 -(*  Title:      HOL/Integ/Bin.ML
     1.5 -    ID:         $Id$
     1.6 -    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -                David Spelt, University of Twente 
     1.8 -                Tobias Nipkow, Technical University Munich
     1.9 -    Copyright   1994  University of Cambridge
    1.10 -    Copyright   1996  University of Twente
    1.11 -    Copyright   1999  TU Munich
    1.12 -
    1.13 -Arithmetic on binary integers.
    1.14 -*)
    1.15 -
    1.16 -(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
    1.17 -
    1.18 -Goal "NCons bin.Pls False = bin.Pls";
    1.19 -by (Simp_tac 1);
    1.20 -qed "NCons_Pls_0";
    1.21 -
    1.22 -Goal "NCons bin.Pls True = bin.Pls BIT True";
    1.23 -by (Simp_tac 1);
    1.24 -qed "NCons_Pls_1";
    1.25 -
    1.26 -Goal "NCons bin.Min False = bin.Min BIT False";
    1.27 -by (Simp_tac 1);
    1.28 -qed "NCons_Min_0";
    1.29 -
    1.30 -Goal "NCons bin.Min True = bin.Min";
    1.31 -by (Simp_tac 1);
    1.32 -qed "NCons_Min_1";
    1.33 -
    1.34 -Goal "bin_succ(w BIT True) = (bin_succ w) BIT False";
    1.35 -by (Simp_tac 1);
    1.36 -qed "bin_succ_1";
    1.37 -
    1.38 -Goal "bin_succ(w BIT False) =  NCons w True";
    1.39 -by (Simp_tac 1);
    1.40 -qed "bin_succ_0";
    1.41 -
    1.42 -Goal "bin_pred(w BIT True) = NCons w False";
    1.43 -by (Simp_tac 1);
    1.44 -qed "bin_pred_1";
    1.45 -
    1.46 -Goal "bin_pred(w BIT False) = (bin_pred w) BIT True";
    1.47 -by (Simp_tac 1);
    1.48 -qed "bin_pred_0";
    1.49 -
    1.50 -Goal "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)";
    1.51 -by (Simp_tac 1);
    1.52 -qed "bin_minus_1";
    1.53 -
    1.54 -Goal "bin_minus(w BIT False) = (bin_minus w) BIT False";
    1.55 -by (Simp_tac 1);
    1.56 -qed "bin_minus_0";
    1.57 -
    1.58 -
    1.59 -(*** bin_add: binary addition ***)
    1.60 -
    1.61 -Goal "bin_add (v BIT True) (w BIT True) = \
    1.62 -\    NCons (bin_add v (bin_succ w)) False";
    1.63 -by (Simp_tac 1);
    1.64 -qed "bin_add_BIT_11";
    1.65 -
    1.66 -Goal "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True";
    1.67 -by (Simp_tac 1);
    1.68 -qed "bin_add_BIT_10";
    1.69 -
    1.70 -Goal "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y";
    1.71 -by Auto_tac;
    1.72 -qed "bin_add_BIT_0";
    1.73 -
    1.74 -Goal "bin_add w bin.Pls = w";
    1.75 -by (induct_tac "w" 1);
    1.76 -by Auto_tac;
    1.77 -qed "bin_add_Pls_right";
    1.78 -
    1.79 -Goal "bin_add w bin.Min = bin_pred w";
    1.80 -by (induct_tac "w" 1);
    1.81 -by Auto_tac;
    1.82 -qed "bin_add_Min_right";
    1.83 -
    1.84 -Goal "bin_add (v BIT x) (w BIT y) = \
    1.85 -\    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)";
    1.86 -by (Simp_tac 1);
    1.87 -qed "bin_add_BIT_BIT";
    1.88 -
    1.89 -
    1.90 -(*** bin_mult: binary multiplication ***)
    1.91 -
    1.92 -Goal "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w";
    1.93 -by (Simp_tac 1);
    1.94 -qed "bin_mult_1";
    1.95 -
    1.96 -Goal "bin_mult (v BIT False) w = NCons (bin_mult v w) False";
    1.97 -by (Simp_tac 1);
    1.98 -qed "bin_mult_0";
    1.99 -
   1.100 -
   1.101 -(**** The carry/borrow functions, bin_succ and bin_pred ****)
   1.102 -
   1.103 -
   1.104 -(** number_of **)
   1.105 -
   1.106 -Goal "number_of(NCons w b) = (number_of(w BIT b)::int)";
   1.107 -by (induct_tac "w" 1);
   1.108 -by (ALLGOALS Asm_simp_tac);
   1.109 -qed "number_of_NCons";
   1.110 -
   1.111 -Addsimps [number_of_NCons];
   1.112 -
   1.113 -Goal "number_of(bin_succ w) = (1 + number_of w :: int)";
   1.114 -by (induct_tac "w" 1);
   1.115 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   1.116 -qed "number_of_succ";
   1.117 -
   1.118 -Goal "number_of(bin_pred w) = (- 1 + number_of w :: int)";
   1.119 -by (induct_tac "w" 1);
   1.120 -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
   1.121 -qed "number_of_pred";
   1.122 -
   1.123 -Goal "number_of(bin_minus w) = (- (number_of w)::int)";
   1.124 -by (induct_tac "w" 1);
   1.125 -by (Simp_tac 1);
   1.126 -by (Simp_tac 1);
   1.127 -by (asm_simp_tac (simpset()
   1.128 -		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
   1.129 -		  addsimps [number_of_succ,number_of_pred,
   1.130 -			    zadd_assoc]) 1);
   1.131 -qed "number_of_minus";
   1.132 -
   1.133 -(*This proof is complicated by the mutual recursion*)
   1.134 -Goal "! w. number_of(bin_add v w) = (number_of v + number_of w::int)";
   1.135 -by (induct_tac "v" 1); 
   1.136 -by (Simp_tac 1);
   1.137 -by (simp_tac (simpset() addsimps [number_of_pred]) 1);
   1.138 -by (rtac allI 1);
   1.139 -by (induct_tac "w" 1);
   1.140 -by (ALLGOALS (asm_simp_tac (simpset() addsimps 
   1.141 -               [bin_add_BIT_BIT, number_of_succ, number_of_pred] @ zadd_ac)));
   1.142 -qed_spec_mp "number_of_add";
   1.143 -
   1.144 -
   1.145 -(*Subtraction*)
   1.146 -Goalw [zdiff_def]
   1.147 -     "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)";
   1.148 -by (simp_tac (simpset() addsimps [number_of_add, number_of_minus]) 1);
   1.149 -qed "diff_number_of_eq";
   1.150 -
   1.151 -bind_thms ("bin_mult_simps", 
   1.152 -           [int_Suc0_eq_1, zmult_zminus, number_of_minus, number_of_add]);
   1.153 -
   1.154 -Goal "number_of(bin_mult v w) = (number_of v * number_of w::int)";
   1.155 -by (induct_tac "v" 1);
   1.156 -by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   1.157 -by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   1.158 -by (asm_simp_tac
   1.159 -    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
   1.160 -qed "number_of_mult";
   1.161 -
   1.162 -
   1.163 -(*The correctness of shifting.  But it doesn't seem to give a measurable
   1.164 -  speed-up.*)
   1.165 -Goal "(2::int) * number_of w = number_of (w BIT False)";
   1.166 -by (induct_tac "w" 1);
   1.167 -by (ALLGOALS (asm_simp_tac
   1.168 -    (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)));
   1.169 -qed "double_number_of_BIT";
   1.170 -
   1.171 -
   1.172 -(** Converting numerals 0 and 1 to their abstract versions **)
   1.173 -
   1.174 -Goal "Numeral0 = (0::int)";
   1.175 -by (Simp_tac 1);
   1.176 -qed "int_numeral_0_eq_0";
   1.177 -
   1.178 -Goal "Numeral1 = (1::int)";
   1.179 -by (simp_tac (simpset() addsimps [int_1, int_Suc0_eq_1]) 1);
   1.180 -qed "int_numeral_1_eq_1";
   1.181 -
   1.182 -
   1.183 -(** Special simplification, for constants only **)
   1.184 -
   1.185 -(*Distributive laws for literals*)
   1.186 -Addsimps (map (inst "w" "number_of ?v")
   1.187 -	  [zadd_zmult_distrib, zadd_zmult_distrib2,
   1.188 -	   zdiff_zmult_distrib, zdiff_zmult_distrib2]);
   1.189 -
   1.190 -Addsimps (map (inst "x" "number_of ?v") 
   1.191 -	  [zless_zminus, zle_zminus, equation_zminus]);
   1.192 -Addsimps (map (inst "y" "number_of ?v") 
   1.193 -	  [zminus_zless, zminus_zle, zminus_equation]);
   1.194 -
   1.195 -(*Equations and inequations involving 1*)
   1.196 -Addsimps (map (simplify (simpset()) o inst "x" "1") 
   1.197 -	  [zless_zminus, zle_zminus, equation_zminus]);
   1.198 -Addsimps (map (simplify (simpset()) o inst "y" "1") 
   1.199 -	  [zminus_zless, zminus_zle, zminus_equation]);
   1.200 -
   1.201 -(*Moving negation out of products*)
   1.202 -Addsimps [zmult_zminus, zmult_zminus_right];
   1.203 -
   1.204 -(*Cancellation of constant factors in comparisons (< and <=) *)
   1.205 -Addsimps (map (inst "k" "number_of ?v")
   1.206 -	  [zmult_zless_cancel1, zmult_zless_cancel2,
   1.207 -	   zmult_zle_cancel1, zmult_zle_cancel2]);
   1.208 -
   1.209 -
   1.210 -(** Special-case simplification for small constants **)
   1.211 -
   1.212 -Goal "-1 * z = -(z::int)";
   1.213 -by (simp_tac (simpset() addsimps compare_rls@[int_Suc0_eq_1, zmult_zminus]) 1);
   1.214 -qed "zmult_minus1";
   1.215 -
   1.216 -Goal "z * -1 = -(z::int)";
   1.217 -by (stac zmult_commute 1 THEN rtac zmult_minus1 1);
   1.218 -qed "zmult_minus1_right";
   1.219 -
   1.220 -Addsimps [zmult_minus1, zmult_minus1_right];
   1.221 -
   1.222 -(*Negation of a coefficient*)
   1.223 -Goal "- (number_of w) * z = number_of(bin_minus w) * (z::int)";
   1.224 -by (simp_tac (simpset() addsimps [number_of_minus, zmult_zminus]) 1);
   1.225 -qed "zminus_number_of_zmult";
   1.226 -Addsimps [zminus_number_of_zmult];
   1.227 -
   1.228 -(*Integer unary minus for the abstract constant 1. Cannot be inserted
   1.229 -  as a simprule until later: it is number_of_Min re-oriented!*)
   1.230 -Goal "- 1 = (-1::int)";
   1.231 -by (Simp_tac 1);
   1.232 -qed "zminus_1_eq_m1";
   1.233 -
   1.234 -Goal "(0 < nat z) = (0 < z)";
   1.235 -by (cut_inst_tac [("w","0")] zless_nat_conj 1);
   1.236 -by Auto_tac;  
   1.237 -qed "zero_less_nat_eq";
   1.238 -Addsimps [zero_less_nat_eq];
   1.239 -
   1.240 -
   1.241 -(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
   1.242 -
   1.243 -(** Equals (=) **)
   1.244 -
   1.245 -Goalw [iszero_def]
   1.246 -  "((number_of x::int) = number_of y) = \
   1.247 -\  iszero (number_of (bin_add x (bin_minus y)))"; 
   1.248 -by (simp_tac (simpset()
   1.249 -                 addsimps compare_rls @ [number_of_add, number_of_minus]) 1); 
   1.250 -qed "eq_number_of_eq"; 
   1.251 -
   1.252 -Goalw [iszero_def] "iszero ((number_of bin.Pls)::int)"; 
   1.253 -by (Simp_tac 1); 
   1.254 -qed "iszero_number_of_Pls"; 
   1.255 -
   1.256 -Goalw [iszero_def] "~ iszero ((number_of bin.Min)::int)";
   1.257 -by (simp_tac (simpset() addsimps [eq_commute]) 1);
   1.258 -qed "nonzero_number_of_Min"; 
   1.259 -
   1.260 -fun int_case_tac x = res_inst_tac [("z",x)] int_cases;
   1.261 -
   1.262 -Goalw [iszero_def]
   1.263 -     "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"; 
   1.264 -by (int_case_tac "number_of w" 1); 
   1.265 -by (ALLGOALS 
   1.266 -    (asm_simp_tac 
   1.267 -     (simpset() addsimps compare_rls @ 
   1.268 -  	                 [zero_reorient, zminus_zadd_distrib RS sym, 
   1.269 -                          int_Suc0_eq_1 RS sym, zadd_int]))); 
   1.270 -qed "iszero_number_of_BIT"; 
   1.271 -
   1.272 -Goal "iszero (number_of (w BIT False)) = iszero (number_of w::int)"; 
   1.273 -by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
   1.274 -qed "iszero_number_of_0"; 
   1.275 -
   1.276 -Goal "~ iszero (number_of (w BIT True)::int)"; 
   1.277 -by (simp_tac (HOL_ss addsimps [iszero_number_of_BIT]) 1); 
   1.278 -qed "iszero_number_of_1"; 
   1.279 -
   1.280 -
   1.281 -
   1.282 -(** Less-than (<) **)
   1.283 -
   1.284 -Goalw [zless_def,zdiff_def] 
   1.285 -    "((number_of x::int) < number_of y) \
   1.286 -\    = neg (number_of (bin_add x (bin_minus y)))";
   1.287 -by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   1.288 -qed "less_number_of_eq_neg"; 
   1.289 -
   1.290 -(*But if Numeral0 is rewritten to 0 then this rule can't be applied:
   1.291 -  Numeral0 IS (number_of Pls) *)
   1.292 -Goal "~ neg (number_of bin.Pls)";
   1.293 -by (simp_tac (simpset() addsimps [neg_eq_less_0]) 1);  
   1.294 -qed "not_neg_number_of_Pls"; 
   1.295 -
   1.296 -Goal "neg (number_of bin.Min)"; 
   1.297 -by (simp_tac (simpset() addsimps [neg_eq_less_0, int_0_less_1]) 1);
   1.298 -qed "neg_number_of_Min"; 
   1.299 -
   1.300 -Goal "neg (number_of (w BIT x)) = neg (number_of w)"; 
   1.301 -by (Asm_simp_tac 1); 
   1.302 -by (int_case_tac "number_of w" 1); 
   1.303 -by (ALLGOALS (asm_simp_tac 
   1.304 -	      (simpset() addsimps [int_Suc0_eq_1 RS sym, zadd_int, 
   1.305 -                         neg_eq_less_0, symmetric zdiff_def] @ compare_rls)));
   1.306 -qed "neg_number_of_BIT"; 
   1.307 -
   1.308 -
   1.309 -(** Less-than-or-equals (<=) **)
   1.310 -
   1.311 -Goal "(number_of x <= (number_of y::int)) = \
   1.312 -\     (~ number_of y < (number_of x::int))";
   1.313 -by (rtac (linorder_not_less RS sym) 1);
   1.314 -qed "le_number_of_eq_not_less"; 
   1.315 -
   1.316 -(** Absolute value (abs) **)
   1.317 -
   1.318 -Goalw [zabs_def]
   1.319 - "abs(number_of x::int) = \
   1.320 -\ (if number_of x < (0::int) then -number_of x else number_of x)";
   1.321 -by (rtac refl 1);
   1.322 -qed "zabs_number_of";
   1.323 -
   1.324 -(*0 and 1 require special rewrites because they aren't numerals*)
   1.325 -Goal "abs (0::int) = 0";
   1.326 -by (simp_tac (simpset() addsimps [zabs_def]) 1); 
   1.327 -qed "zabs_0";
   1.328 -
   1.329 -Goal "abs (1::int) = 1";
   1.330 -by (simp_tac (simpset() delsimps [int_0, int_1] 
   1.331 -                       addsimps [int_0 RS sym, int_1 RS sym, zabs_def]) 1); 
   1.332 -qed "zabs_1";
   1.333 -
   1.334 -(*Re-orientation of the equation nnn=x*)
   1.335 -Goal "(number_of w = x) = (x = number_of w)";
   1.336 -by Auto_tac;  
   1.337 -qed "number_of_reorient";
   1.338 -
   1.339 -
   1.340 -structure Bin_Simprocs =
   1.341 -  struct
   1.342 -  fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
   1.343 -    if t aconv u then None
   1.344 -    else
   1.345 -      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
   1.346 -      in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
   1.347 -
   1.348 -  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
   1.349 -  fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
   1.350 -
   1.351 -  fun prep_simproc (name, pats, proc) =
   1.352 -    Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
   1.353 -
   1.354 -  fun is_numeral (Const("Numeral.number_of", _) $ w) = true
   1.355 -    | is_numeral _ = false
   1.356 -
   1.357 -  fun simplify_meta_eq f_number_of_eq f_eq =
   1.358 -      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
   1.359 -
   1.360 -  structure IntAbstractNumeralsData =
   1.361 -    struct
   1.362 -    val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   1.363 -    val is_numeral	= is_numeral
   1.364 -    val numeral_0_eq_0    = int_numeral_0_eq_0
   1.365 -    val numeral_1_eq_1    = int_numeral_1_eq_1
   1.366 -    val prove_conv	= prove_conv_nohyps_novars
   1.367 -    fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
   1.368 -    val simplify_meta_eq  = simplify_meta_eq 
   1.369 -    end
   1.370 -
   1.371 -  structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData)
   1.372 -
   1.373 -
   1.374 -  (*For addition, we already have rules for the operand 0.
   1.375 -    Multiplication is omitted because there are already special rules for 
   1.376 -    both 0 and 1 as operands.  Unary minus is trivial, just have - 1 = -1.
   1.377 -    For the others, having three patterns is a compromise between just having
   1.378 -    one (many spurious calls) and having nine (just too many!) *)
   1.379 -  val eval_numerals = 
   1.380 -    map prep_simproc
   1.381 -     [("int_add_eval_numerals",
   1.382 -       ["(m::int) + 1", "(m::int) + number_of v"], 
   1.383 -       IntAbstractNumerals.proc (number_of_add RS sym)),
   1.384 -      ("int_diff_eval_numerals",
   1.385 -       ["(m::int) - 1", "(m::int) - number_of v"], 
   1.386 -       IntAbstractNumerals.proc diff_number_of_eq),
   1.387 -      ("int_eq_eval_numerals",
   1.388 -       ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"], 
   1.389 -       IntAbstractNumerals.proc eq_number_of_eq),
   1.390 -      ("int_less_eval_numerals",
   1.391 -       ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"], 
   1.392 -       IntAbstractNumerals.proc less_number_of_eq_neg),
   1.393 -      ("int_le_eval_numerals",
   1.394 -       ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],
   1.395 -       IntAbstractNumerals.proc le_number_of_eq_not_less)]
   1.396 -
   1.397 -  (*reorientation simprules using ==, for the following simproc*)
   1.398 -  val meta_zero_reorient = zero_reorient RS eq_reflection
   1.399 -  val meta_one_reorient = one_reorient RS eq_reflection
   1.400 -  val meta_number_of_reorient = number_of_reorient RS eq_reflection
   1.401 -
   1.402 -  (*reorientation simplification procedure: reorients (polymorphic) 
   1.403 -    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
   1.404 -  fun reorient_proc sg _ (_ $ t $ u) =
   1.405 -    case u of
   1.406 -	Const("0", _) => None
   1.407 -      | Const("1", _) => None
   1.408 -      | Const("Numeral.number_of", _) $ _ => None
   1.409 -      | _ => Some (case t of
   1.410 -		  Const("0", _) => meta_zero_reorient
   1.411 -		| Const("1", _) => meta_one_reorient
   1.412 -		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
   1.413 -
   1.414 -  val reorient_simproc = 
   1.415 -      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
   1.416 -
   1.417 -  end;
   1.418 -
   1.419 -
   1.420 -Addsimprocs Bin_Simprocs.eval_numerals;
   1.421 -Addsimprocs [Bin_Simprocs.reorient_simproc];
   1.422 -
   1.423 -
   1.424 -(*Delete the original rewrites, with their clumsy conditional expressions*)
   1.425 -Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
   1.426 -          NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
   1.427 -
   1.428 -(*Hide the binary representation of integer constants*)
   1.429 -Delsimps [number_of_Pls, number_of_Min, number_of_BIT];
   1.430 -
   1.431 -
   1.432 -
   1.433 -(*Simplification of arithmetic operations on integer constants.
   1.434 -  Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
   1.435 -
   1.436 -bind_thms ("NCons_simps", 
   1.437 -           [NCons_Pls_0, NCons_Pls_1, NCons_Min_0, NCons_Min_1, NCons_BIT]);
   1.438 -
   1.439 -bind_thms ("bin_arith_extra_simps",
   1.440 -    [number_of_add RS sym,
   1.441 -     number_of_minus RS sym, zminus_1_eq_m1,
   1.442 -     number_of_mult RS sym,
   1.443 -     bin_succ_1, bin_succ_0, 
   1.444 -     bin_pred_1, bin_pred_0, 
   1.445 -     bin_minus_1, bin_minus_0,  
   1.446 -     bin_add_Pls_right, bin_add_Min_right,
   1.447 -     bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   1.448 -     diff_number_of_eq, zabs_number_of, zabs_0, zabs_1,
   1.449 -     bin_mult_1, bin_mult_0] @ NCons_simps);
   1.450 -
   1.451 -(*For making a minimal simpset, one must include these default simprules
   1.452 -  of thy.  Also include simp_thms, or at least (~False)=True*)
   1.453 -bind_thms ("bin_arith_simps",
   1.454 -    [bin_pred_Pls, bin_pred_Min,
   1.455 -     bin_succ_Pls, bin_succ_Min,
   1.456 -     bin_add_Pls, bin_add_Min,
   1.457 -     bin_minus_Pls, bin_minus_Min,
   1.458 -     bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps);
   1.459 -
   1.460 -(*Simplification of relational operations*)
   1.461 -bind_thms ("bin_rel_simps",
   1.462 -    [eq_number_of_eq, iszero_number_of_Pls, nonzero_number_of_Min,
   1.463 -     iszero_number_of_0, iszero_number_of_1,
   1.464 -     less_number_of_eq_neg,
   1.465 -     not_neg_number_of_Pls, not_neg_0, not_neg_1, not_iszero_1, 
   1.466 -     neg_number_of_Min, neg_number_of_BIT,
   1.467 -     le_number_of_eq_not_less]);
   1.468 -
   1.469 -Addsimps bin_arith_extra_simps;
   1.470 -Addsimps bin_rel_simps;
   1.471 -
   1.472 -
   1.473 -(** Simplification of arithmetic when nested to the right **)
   1.474 -
   1.475 -Goal "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)";
   1.476 -by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   1.477 -qed "add_number_of_left";
   1.478 -
   1.479 -Goal "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)";
   1.480 -by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   1.481 -qed "mult_number_of_left";
   1.482 -
   1.483 -Goalw [zdiff_def]
   1.484 -    "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)";
   1.485 -by (rtac add_number_of_left 1);
   1.486 -qed "add_number_of_diff1";
   1.487 -
   1.488 -Goal "number_of v + (c - number_of w) = \
   1.489 -\    number_of (bin_add v (bin_minus w)) + (c::int)";
   1.490 -by (stac (diff_number_of_eq RS sym) 1);
   1.491 -by Auto_tac;
   1.492 -qed "add_number_of_diff2";
   1.493 -
   1.494 -Addsimps [add_number_of_left, mult_number_of_left,
   1.495 -	  add_number_of_diff1, add_number_of_diff2]; 
   1.496 -
   1.497 -
   1.498 -(** Inserting these natural simprules earlier would break many proofs! **) 
   1.499 -
   1.500 -(* int (Suc n) = 1 + int n *)
   1.501 -Addsimps [int_Suc];
   1.502 -
   1.503 -(* Numeral0 -> 0 and Numeral1 -> 1 *)
   1.504 -Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
   1.505 -
   1.506 -
     2.1 --- a/src/HOL/Integ/Bin.thy	Wed Dec 03 10:49:34 2003 +0100
     2.2 +++ b/src/HOL/Integ/Bin.thy	Thu Dec 04 10:29:17 2003 +0100
     2.3 @@ -1,73 +1,78 @@
     2.4  (*  Title:	HOL/Integ/Bin.thy
     2.5      ID:         $Id$
     2.6      Authors:	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -		David Spelt, University of Twente 
     2.8 +		David Spelt, University of Twente
     2.9      Copyright	1994  University of Cambridge
    2.10      Copyright   1996 University of Twente
    2.11 +*)
    2.12  
    2.13 -Arithmetic on binary integers.
    2.14 +header{*Arithmetic on Binary Integers*}
    2.15 +
    2.16 +theory Bin = Int + Numeral:
    2.17  
    2.18 -   The sign Pls stands for an infinite string of leading F's.
    2.19 -   The sign Min stands for an infinite string of leading T's.
    2.20 +text{*The sign @{term Pls} stands for an infinite string of leading Falses.*}
    2.21 +text{*The sign @{term Min} stands for an infinite string of leading Trues.*}
    2.22  
    2.23 -A number can have multiple representations, namely leading F's with sign
    2.24 -Pls and leading T's with sign Min.  See ZF/ex/twos-compl.ML/int_of_binary
    2.25 +text{*A number can have multiple representations, namely leading Falses with
    2.26 +sign @{term Pls} and leading Trues with sign @{term Min}.
    2.27 +See @{text "ZF/Integ/twos-compl.ML"}, function @{text int_of_binary},
    2.28  for the numerical interpretation.
    2.29  
    2.30 -The representation expects that (m mod 2) is 0 or 1, even if m is negative;
    2.31 -For instance, -5 div 2 = -3 and -5 mod 2 = 1; thus -5 = (-3)*2 + 1
    2.32 -*)
    2.33 -
    2.34 -Bin = Int + Numeral +
    2.35 +The representation expects that @{term "(m mod 2)"} is 0 or 1,
    2.36 +even if m is negative;
    2.37 +For instance, @{term "-5 div 2 = -3"} and @{term "-5 mod 2 = 1"}; thus
    2.38 +@{term "-5 = (-3)*2 + 1"}.
    2.39 +*}
    2.40  
    2.41  consts
    2.42 -  NCons            :: [bin,bool]=>bin
    2.43 -  bin_succ         :: bin=>bin
    2.44 -  bin_pred         :: bin=>bin
    2.45 -  bin_minus        :: bin=>bin
    2.46 -  bin_add,bin_mult :: [bin,bin]=>bin
    2.47 +  NCons     :: "[bin,bool]=>bin"
    2.48 +  bin_succ  :: "bin=>bin"
    2.49 +  bin_pred  :: "bin=>bin"
    2.50 +  bin_minus :: "bin=>bin"
    2.51 +  bin_add   :: "[bin,bin]=>bin"
    2.52 +  bin_mult  :: "[bin,bin]=>bin"
    2.53  
    2.54  (*NCons inserts a bit, suppressing leading 0s and 1s*)
    2.55  primrec
    2.56 -  NCons_Pls "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
    2.57 -  NCons_Min "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
    2.58 -  NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
    2.59 +  NCons_Pls:  "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
    2.60 +  NCons_Min:  "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
    2.61 +  NCons_BIT:  "NCons (w BIT x) b = (w BIT x) BIT b"
    2.62  
    2.63  instance
    2.64 -  int :: number
    2.65 +  int :: number ..
    2.66  
    2.67  primrec (*the type constraint is essential!*)
    2.68 -  number_of_Pls  "number_of bin.Pls = 0"
    2.69 -  number_of_Min  "number_of bin.Min = - (1::int)"
    2.70 -  number_of_BIT  "number_of(w BIT x) = (if x then 1 else 0) +
    2.71 -	                               (number_of w) + (number_of w)" 
    2.72 +  number_of_Pls: "number_of bin.Pls = 0"
    2.73 +  number_of_Min: "number_of bin.Min = - (1::int)"
    2.74 +  number_of_BIT: "number_of(w BIT x) = (if x then 1 else 0) +
    2.75 +	                               (number_of w) + (number_of w)"
    2.76  
    2.77  primrec
    2.78 -  bin_succ_Pls  "bin_succ bin.Pls = bin.Pls BIT True" 
    2.79 -  bin_succ_Min  "bin_succ bin.Min = bin.Pls"
    2.80 -  bin_succ_BIT  "bin_succ(w BIT x) =
    2.81 +  bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
    2.82 +  bin_succ_Min: "bin_succ bin.Min = bin.Pls"
    2.83 +  bin_succ_BIT: "bin_succ(w BIT x) =
    2.84    	            (if x then bin_succ w BIT False
    2.85  	                  else NCons w True)"
    2.86  
    2.87  primrec
    2.88 -  bin_pred_Pls  "bin_pred bin.Pls = bin.Min"
    2.89 -  bin_pred_Min  "bin_pred bin.Min = bin.Min BIT False"
    2.90 -  bin_pred_BIT  "bin_pred(w BIT x) =
    2.91 +  bin_pred_Pls: "bin_pred bin.Pls = bin.Min"
    2.92 +  bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False"
    2.93 +  bin_pred_BIT: "bin_pred(w BIT x) =
    2.94  	            (if x then NCons w False
    2.95  		          else (bin_pred w) BIT True)"
    2.96 - 
    2.97 +
    2.98  primrec
    2.99 -  bin_minus_Pls  "bin_minus bin.Pls = bin.Pls"
   2.100 -  bin_minus_Min  "bin_minus bin.Min = bin.Pls BIT True"
   2.101 -  bin_minus_BIT  "bin_minus(w BIT x) =
   2.102 +  bin_minus_Pls: "bin_minus bin.Pls = bin.Pls"
   2.103 +  bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True"
   2.104 +  bin_minus_BIT: "bin_minus(w BIT x) =
   2.105  	             (if x then bin_pred (NCons (bin_minus w) False)
   2.106  		           else bin_minus w BIT False)"
   2.107  
   2.108  primrec
   2.109 -  bin_add_Pls  "bin_add bin.Pls w = w"
   2.110 -  bin_add_Min  "bin_add bin.Min w = bin_pred w"
   2.111 -  bin_add_BIT
   2.112 -    "bin_add (v BIT x) w = 
   2.113 +  bin_add_Pls: "bin_add bin.Pls w = w"
   2.114 +  bin_add_Min: "bin_add bin.Min w = bin_pred w"
   2.115 +  bin_add_BIT:
   2.116 +    "bin_add (v BIT x) w =
   2.117         (case w of Pls => v BIT x
   2.118                  | Min => bin_pred (v BIT x)
   2.119                  | (w BIT y) =>
   2.120 @@ -75,10 +80,384 @@
   2.121  	                  (x~=y))"
   2.122  
   2.123  primrec
   2.124 -  bin_mult_Pls  "bin_mult bin.Pls w = bin.Pls"
   2.125 -  bin_mult_Min  "bin_mult bin.Min w = bin_minus w"
   2.126 -  bin_mult_BIT  "bin_mult (v BIT x) w =
   2.127 +  bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls"
   2.128 +  bin_mult_Min: "bin_mult bin.Min w = bin_minus w"
   2.129 +  bin_mult_BIT: "bin_mult (v BIT x) w =
   2.130  	            (if x then (bin_add (NCons (bin_mult v w) False) w)
   2.131  	                  else (NCons (bin_mult v w) False))"
   2.132  
   2.133 +
   2.134 +(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
   2.135 +
   2.136 +lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls"
   2.137 +by simp
   2.138 +
   2.139 +lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True"
   2.140 +by simp
   2.141 +
   2.142 +lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False"
   2.143 +by simp
   2.144 +
   2.145 +lemma NCons_Min_1: "NCons bin.Min True = bin.Min"
   2.146 +by simp
   2.147 +
   2.148 +lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False"
   2.149 +by simp
   2.150 +
   2.151 +lemma bin_succ_0: "bin_succ(w BIT False) =  NCons w True"
   2.152 +by simp
   2.153 +
   2.154 +lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False"
   2.155 +by simp
   2.156 +
   2.157 +lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True"
   2.158 +by simp
   2.159 +
   2.160 +lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
   2.161 +by simp
   2.162 +
   2.163 +lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False"
   2.164 +by simp
   2.165 +
   2.166 +
   2.167 +(*** bin_add: binary addition ***)
   2.168 +
   2.169 +lemma bin_add_BIT_11: "bin_add (v BIT True) (w BIT True) =
   2.170 +     NCons (bin_add v (bin_succ w)) False"
   2.171 +apply simp
   2.172 +done
   2.173 +
   2.174 +lemma bin_add_BIT_10: "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
   2.175 +by simp
   2.176 +
   2.177 +lemma bin_add_BIT_0: "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
   2.178 +by auto
   2.179 +
   2.180 +lemma bin_add_Pls_right: "bin_add w bin.Pls = w"
   2.181 +by (induct_tac "w", auto)
   2.182 +
   2.183 +lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w"
   2.184 +by (induct_tac "w", auto)
   2.185 +
   2.186 +lemma bin_add_BIT_BIT: "bin_add (v BIT x) (w BIT y) =
   2.187 +     NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
   2.188 +apply simp
   2.189 +done
   2.190 +
   2.191 +
   2.192 +(*** bin_mult: binary multiplication ***)
   2.193 +
   2.194 +lemma bin_mult_1: "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
   2.195 +by simp
   2.196 +
   2.197 +lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
   2.198 +by simp
   2.199 +
   2.200 +
   2.201 +(**** The carry/borrow functions, bin_succ and bin_pred ****)
   2.202 +
   2.203 +
   2.204 +(** number_of **)
   2.205 +
   2.206 +lemma number_of_NCons [simp]:
   2.207 +     "number_of(NCons w b) = (number_of(w BIT b)::int)"
   2.208 +apply (induct_tac "w")
   2.209 +apply (simp_all)
   2.210 +done
   2.211 +
   2.212 +lemma number_of_succ: "number_of(bin_succ w) = (1 + number_of w :: int)"
   2.213 +apply (induct_tac "w")
   2.214 +apply (simp_all add: zadd_ac)
   2.215 +done
   2.216 +
   2.217 +lemma number_of_pred: "number_of(bin_pred w) = (- 1 + number_of w :: int)"
   2.218 +apply (induct_tac "w")
   2.219 +apply (simp_all add: add_assoc [symmetric]) 
   2.220 +apply (simp add: zadd_ac)
   2.221 +done
   2.222 +
   2.223 +lemma number_of_minus: "number_of(bin_minus w) = (- (number_of w)::int)"
   2.224 +apply (induct_tac "w", simp, simp)
   2.225 +apply (simp del: bin_pred_Pls bin_pred_Min bin_pred_BIT add: number_of_succ number_of_pred zadd_assoc)
   2.226 +done
   2.227 +
   2.228 +(*This proof is complicated by the mutual recursion*)
   2.229 +lemma number_of_add [rule_format (no_asm)]: "! w. number_of(bin_add v w) = (number_of v + number_of w::int)"
   2.230 +apply (induct_tac "v", simp)
   2.231 +apply (simp add: number_of_pred)
   2.232 +apply (rule allI)
   2.233 +apply (induct_tac "w")
   2.234 +apply (simp_all add: bin_add_BIT_BIT number_of_succ number_of_pred add_ac)
   2.235 +apply (simp add: add_left_commute [of "1::int"]) 
   2.236 +done
   2.237 +
   2.238 +
   2.239 +(*Subtraction*)
   2.240 +lemma diff_number_of_eq:
   2.241 +     "number_of v - number_of w = (number_of(bin_add v (bin_minus w))::int)"
   2.242 +apply (unfold zdiff_def)
   2.243 +apply (simp add: number_of_add number_of_minus)
   2.244 +done
   2.245 +
   2.246 +lemmas bin_mult_simps = 
   2.247 +       int_Suc0_eq_1 zmult_zminus number_of_minus number_of_add
   2.248 +
   2.249 +lemma number_of_mult: "number_of(bin_mult v w) = (number_of v * number_of w::int)"
   2.250 +apply (induct_tac "v")
   2.251 +apply (simp add: bin_mult_simps)
   2.252 +apply (simp add: bin_mult_simps)
   2.253 +apply (simp add: bin_mult_simps zadd_zmult_distrib zadd_ac)
   2.254 +done
   2.255 +
   2.256 +
   2.257 +(*The correctness of shifting.  But it doesn't seem to give a measurable
   2.258 +  speed-up.*)
   2.259 +lemma double_number_of_BIT: "(2::int) * number_of w = number_of (w BIT False)"
   2.260 +apply (induct_tac "w")
   2.261 +apply (simp_all add: bin_mult_simps zadd_zmult_distrib zadd_ac)
   2.262 +done
   2.263 +
   2.264 +
   2.265 +(** Converting numerals 0 and 1 to their abstract versions **)
   2.266 +
   2.267 +lemma int_numeral_0_eq_0: "Numeral0 = (0::int)"
   2.268 +by simp
   2.269 +
   2.270 +lemma int_numeral_1_eq_1: "Numeral1 = (1::int)"
   2.271 +by (simp add: int_1 int_Suc0_eq_1)
   2.272 +
   2.273 +
   2.274 +subsubsection{*Special Simplification for Constants*}
   2.275 +
   2.276 +text{*These distributive laws move literals inside sums and differences.*}
   2.277 +declare left_distrib [of _ _ "number_of v", standard, simp]
   2.278 +declare right_distrib [of "number_of v", standard, simp]
   2.279 +
   2.280 +declare left_diff_distrib [of _ _ "number_of v", standard, simp]
   2.281 +declare right_diff_distrib [of "number_of v", standard, simp]
   2.282 +
   2.283 +text{*These laws simplify inequalities, moving unary minus from a term
   2.284 +into the literal.*}
   2.285 +declare zless_zminus [of "number_of v", standard, simp]
   2.286 +declare zle_zminus [of "number_of v", standard, simp]
   2.287 +declare equation_zminus [of "number_of v", standard, simp]
   2.288 +
   2.289 +declare zminus_zless [of _ "number_of v", standard, simp]
   2.290 +declare zminus_zle [of _ "number_of v", standard, simp]
   2.291 +declare zminus_equation [of _ "number_of v", standard, simp]
   2.292 +
   2.293 +text{*These simplify inequalities where one side is the constant 1.*}
   2.294 +declare zless_zminus [of 1, simplified, simp]
   2.295 +declare zle_zminus [of 1, simplified, simp]
   2.296 +declare equation_zminus [of 1, simplified, simp]
   2.297 +
   2.298 +declare zminus_zless [of _ 1, simplified, simp]
   2.299 +declare zminus_zle [of _ 1, simplified, simp]
   2.300 +declare zminus_equation [of _ 1, simplified, simp]
   2.301 +
   2.302 +
   2.303 +(*Moving negation out of products*)
   2.304 +declare zmult_zminus [simp] zmult_zminus_right [simp]
   2.305 +
   2.306 +(*Cancellation of constant factors in comparisons (< and \<le>) *)
   2.307 +
   2.308 +declare mult_less_cancel_left [of "number_of v", standard, simp]
   2.309 +declare mult_less_cancel_right [of _ "number_of v", standard, simp]
   2.310 +declare mult_le_cancel_left [of "number_of v", standard, simp]
   2.311 +declare mult_le_cancel_right [of _ "number_of v", standard, simp]
   2.312 +
   2.313 +
   2.314 +(** Special-case simplification for small constants **)
   2.315 +
   2.316 +lemma zmult_minus1 [simp]: "-1 * z = -(z::int)"
   2.317 +by (simp add: compare_rls int_Suc0_eq_1 zmult_zminus)
   2.318 +
   2.319 +lemma zmult_minus1_right [simp]: "z * -1 = -(z::int)"
   2.320 +by (subst zmult_commute, rule zmult_minus1)
   2.321 +
   2.322 +
   2.323 +(*Negation of a coefficient*)
   2.324 +lemma zminus_number_of_zmult [simp]: "- (number_of w) * z = number_of(bin_minus w) * (z::int)"
   2.325 +by (simp add: number_of_minus zmult_zminus)
   2.326 +
   2.327 +(*Integer unary minus for the abstract constant 1. Cannot be inserted
   2.328 +  as a simprule until later: it is number_of_Min re-oriented!*)
   2.329 +lemma zminus_1_eq_m1: "- 1 = (-1::int)"
   2.330 +by simp
   2.331 +
   2.332 +lemma zero_less_nat_eq [simp]: "(0 < nat z) = (0 < z)"
   2.333 +by (cut_tac w = 0 in zless_nat_conj, auto)
   2.334 +
   2.335 +
   2.336 +(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
   2.337 +
   2.338 +(** Equals (=) **)
   2.339 +
   2.340 +lemma eq_number_of_eq:
   2.341 +  "((number_of x::int) = number_of y) =
   2.342 +   iszero (number_of (bin_add x (bin_minus y)))"
   2.343 +apply (unfold iszero_def)
   2.344 +apply (simp add: compare_rls number_of_add number_of_minus)
   2.345 +done
   2.346 +
   2.347 +lemma iszero_number_of_Pls: "iszero ((number_of bin.Pls)::int)"
   2.348 +by (unfold iszero_def, simp)
   2.349 +
   2.350 +lemma nonzero_number_of_Min: "~ iszero ((number_of bin.Min)::int)"
   2.351 +apply (unfold iszero_def)
   2.352 +apply (simp add: eq_commute)
   2.353 +done
   2.354 +
   2.355 +lemma iszero_number_of_BIT:
   2.356 +     "iszero (number_of (w BIT x)) = (~x & iszero (number_of w::int))"
   2.357 +apply (unfold iszero_def)
   2.358 +apply (cases "(number_of w)::int" rule: int_cases) 
   2.359 +apply (simp_all (no_asm_simp) add: compare_rls zero_reorient
   2.360 +         zminus_zadd_distrib [symmetric] int_Suc0_eq_1 [symmetric] zadd_int)
   2.361 +done
   2.362 +
   2.363 +lemma iszero_number_of_0: "iszero (number_of (w BIT False)) = iszero (number_of w::int)"
   2.364 +by (simp only: iszero_number_of_BIT simp_thms)
   2.365 +
   2.366 +lemma iszero_number_of_1: "~ iszero (number_of (w BIT True)::int)"
   2.367 +by (simp only: iszero_number_of_BIT simp_thms)
   2.368 +
   2.369 +
   2.370 +
   2.371 +(** Less-than (<) **)
   2.372 +
   2.373 +lemma less_number_of_eq_neg:
   2.374 +    "((number_of x::int) < number_of y)
   2.375 +     = neg (number_of (bin_add x (bin_minus y)))"
   2.376 +
   2.377 +apply (unfold zless_def zdiff_def)
   2.378 +apply (simp add: bin_mult_simps)
   2.379 +done
   2.380 +
   2.381 +(*But if Numeral0 is rewritten to 0 then this rule can't be applied:
   2.382 +  Numeral0 IS (number_of Pls) *)
   2.383 +lemma not_neg_number_of_Pls: "~ neg (number_of bin.Pls)"
   2.384 +by (simp add: neg_eq_less_0)
   2.385 +
   2.386 +lemma neg_number_of_Min: "neg (number_of bin.Min)"
   2.387 +by (simp add: neg_eq_less_0 int_0_less_1)
   2.388 +
   2.389 +lemma neg_number_of_BIT: "neg (number_of (w BIT x)) = neg (number_of w)"
   2.390 +apply simp
   2.391 +apply (cases "(number_of w)::int" rule: int_cases) 
   2.392 +apply (simp_all (no_asm_simp) add: int_Suc0_eq_1 [symmetric] zadd_int neg_eq_less_0 zdiff_def [symmetric] compare_rls)
   2.393 +done
   2.394 +
   2.395 +
   2.396 +(** Less-than-or-equals (\<le>) **)
   2.397 +
   2.398 +lemma le_number_of_eq_not_less: "(number_of x \<le> (number_of y::int)) =
   2.399 +      (~ number_of y < (number_of x::int))"
   2.400 +apply (rule linorder_not_less [symmetric])
   2.401 +done
   2.402 +
   2.403 +(** Absolute value (abs) **)
   2.404 +
   2.405 +lemma zabs_number_of:
   2.406 + "abs(number_of x::int) =
   2.407 +  (if number_of x < (0::int) then -number_of x else number_of x)"
   2.408 +
   2.409 +apply (unfold zabs_def)
   2.410 +apply (rule refl)
   2.411 +done
   2.412 +
   2.413 +(*0 and 1 require special rewrites because they aren't numerals*)
   2.414 +lemma zabs_0: "abs (0::int) = 0"
   2.415 +by (simp add: zabs_def)
   2.416 +
   2.417 +lemma zabs_1: "abs (1::int) = 1"
   2.418 +by (simp del: int_0 int_1 add: int_0 [symmetric] int_1 [symmetric] zabs_def)
   2.419 +
   2.420 +(*Re-orientation of the equation nnn=x*)
   2.421 +lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
   2.422 +by auto
   2.423 +
   2.424 +
   2.425 +(*Delete the original rewrites, with their clumsy conditional expressions*)
   2.426 +declare bin_succ_BIT [simp del] bin_pred_BIT [simp del]
   2.427 +        bin_minus_BIT [simp del]
   2.428 +
   2.429 +declare bin_add_BIT [simp del] bin_mult_BIT [simp del]
   2.430 +declare NCons_Pls [simp del] NCons_Min [simp del]
   2.431 +
   2.432 +(*Hide the binary representation of integer constants*)
   2.433 +declare number_of_Pls [simp del] number_of_Min [simp del]
   2.434 +        number_of_BIT [simp del]
   2.435 +
   2.436 +
   2.437 +
   2.438 +(*Simplification of arithmetic operations on integer constants.
   2.439 +  Note that bin_pred_Pls, etc. were added to the simpset by primrec.*)
   2.440 +
   2.441 +lemmas NCons_simps = NCons_Pls_0 NCons_Pls_1 NCons_Min_0 NCons_Min_1 NCons_BIT
   2.442 +
   2.443 +lemmas bin_arith_extra_simps = 
   2.444 +       number_of_add [symmetric]
   2.445 +       number_of_minus [symmetric] zminus_1_eq_m1
   2.446 +       number_of_mult [symmetric]
   2.447 +       bin_succ_1 bin_succ_0
   2.448 +       bin_pred_1 bin_pred_0
   2.449 +       bin_minus_1 bin_minus_0
   2.450 +       bin_add_Pls_right bin_add_Min_right
   2.451 +       bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
   2.452 +       diff_number_of_eq zabs_number_of zabs_0 zabs_1
   2.453 +       bin_mult_1 bin_mult_0 NCons_simps
   2.454 +
   2.455 +(*For making a minimal simpset, one must include these default simprules
   2.456 +  of thy.  Also include simp_thms, or at least (~False)=True*)
   2.457 +lemmas bin_arith_simps = 
   2.458 +       bin_pred_Pls bin_pred_Min
   2.459 +       bin_succ_Pls bin_succ_Min
   2.460 +       bin_add_Pls bin_add_Min
   2.461 +       bin_minus_Pls bin_minus_Min
   2.462 +       bin_mult_Pls bin_mult_Min bin_arith_extra_simps
   2.463 +
   2.464 +(*Simplification of relational operations*)
   2.465 +lemmas bin_rel_simps = 
   2.466 +       eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
   2.467 +       iszero_number_of_0 iszero_number_of_1
   2.468 +       less_number_of_eq_neg
   2.469 +       not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
   2.470 +       neg_number_of_Min neg_number_of_BIT
   2.471 +       le_number_of_eq_not_less
   2.472 +
   2.473 +declare bin_arith_extra_simps [simp]
   2.474 +declare bin_rel_simps [simp]
   2.475 +
   2.476 +
   2.477 +(** Simplification of arithmetic when nested to the right **)
   2.478 +
   2.479 +lemma add_number_of_left [simp]: "number_of v + (number_of w + z) = (number_of(bin_add v w) + z::int)"
   2.480 +by (simp add: zadd_assoc [symmetric])
   2.481 +
   2.482 +lemma mult_number_of_left [simp]: "number_of v * (number_of w * z) = (number_of(bin_mult v w) * z::int)"
   2.483 +by (simp add: zmult_assoc [symmetric])
   2.484 +
   2.485 +lemma add_number_of_diff1:
   2.486 +    "number_of v + (number_of w - c) = number_of(bin_add v w) - (c::int)"
   2.487 +apply (unfold zdiff_def)
   2.488 +apply (rule add_number_of_left)
   2.489 +done
   2.490 +
   2.491 +lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
   2.492 +     number_of (bin_add v (bin_minus w)) + (c::int)"
   2.493 +apply (subst diff_number_of_eq [symmetric])
   2.494 +apply (simp only: compare_rls)
   2.495 +done
   2.496 +
   2.497 +
   2.498 +
   2.499 +(** Inserting these natural simprules earlier would break many proofs! **)
   2.500 +
   2.501 +(* int (Suc n) = 1 + int n *)
   2.502 +declare int_Suc [simp]
   2.503 +
   2.504 +(* Numeral0 -> 0 and Numeral1 -> 1 *)
   2.505 +declare int_numeral_0_eq_0 [simp] int_numeral_1_eq_1 [simp]
   2.506 +
   2.507  end
     3.1 --- a/src/HOL/Integ/Int.thy	Wed Dec 03 10:49:34 2003 +0100
     3.2 +++ b/src/HOL/Integ/Int.thy	Thu Dec 04 10:29:17 2003 +0100
     3.3 @@ -56,7 +56,7 @@
     3.4  
     3.5  subsection{*Comparison laws*}
     3.6  
     3.7 -(*ring and field?*)
     3.8 +(*RING AND FIELD????????????????????????????????????????????????????????????*)
     3.9  
    3.10  lemma zminus_zless_zminus [simp]: "(- x < - y) = (y < (x::int))"
    3.11  by (simp add: zless_def zdiff_def zadd_ac)
    3.12 @@ -408,8 +408,6 @@
    3.13  end;
    3.14  
    3.15  structure Int_Cancel = Abel_Cancel (Int_Cancel_Data);
    3.16 -
    3.17 -Addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
    3.18  *}
    3.19  
    3.20  
    3.21 @@ -427,37 +425,11 @@
    3.22  done
    3.23  
    3.24  
    3.25 -subsection{*Inequality reasoning*}
    3.26 -
    3.27 -text{*Are they needed????*}
    3.28 -lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
    3.29 -apply (auto simp add: zless_iff_Suc_zadd int_Suc gr0_conv_Suc zero_reorient)
    3.30 -apply (rule_tac x = "Suc n" in exI)
    3.31 -apply (simp add: int_Suc)
    3.32 -done
    3.33 -
    3.34 -lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
    3.35 -apply (simp add: zle_def zless_add1_eq)
    3.36 -apply (auto intro: zless_asym zle_anti_sym
    3.37 -            simp add: order_less_imp_le symmetric zle_def)
    3.38 -done
    3.39 -
    3.40 -lemma add1_left_zle_eq: "((1::int) + w \<le> z) = (w<z)"
    3.41 -apply (subst zadd_commute)
    3.42 -apply (rule add1_zle_eq)
    3.43 -done
    3.44 -
    3.45 -
    3.46 -
    3.47 -
    3.48  ML
    3.49  {*
    3.50  val zless_eq_neg = thm "zless_eq_neg";
    3.51  val eq_eq_iszero = thm "eq_eq_iszero";
    3.52  val zle_eq_not_neg = thm "zle_eq_not_neg";
    3.53 -val zless_add1_eq = thm "zless_add1_eq";
    3.54 -val add1_zle_eq = thm "add1_zle_eq";
    3.55 -val add1_left_zle_eq = thm "add1_left_zle_eq";
    3.56  val zadd_right_cancel_zless = thm "zadd_right_cancel_zless";
    3.57  val zadd_left_cancel_zless = thm "zadd_left_cancel_zless";
    3.58  val zadd_right_cancel_zle = thm "zadd_right_cancel_zle";
     4.1 --- a/src/HOL/Integ/IntArith.thy	Wed Dec 03 10:49:34 2003 +0100
     4.2 +++ b/src/HOL/Integ/IntArith.thy	Thu Dec 04 10:29:17 2003 +0100
     4.3 @@ -8,13 +8,34 @@
     4.4  theory IntArith = Bin
     4.5  files ("int_arith1.ML"):
     4.6  
     4.7 +subsection{*Inequality Reasoning for the Arithmetic Simproc*}
     4.8 +
     4.9 +lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"
    4.10 +  proof (auto simp add: zle_def zless_iff_Suc_zadd) 
    4.11 +  fix m n
    4.12 +  assume "w + 1 = w + (1 + int m) + (1 + int n)"
    4.13 +  hence "(w + 1) + (1 + int (m + n)) = (w + 1) + 0" 
    4.14 +    by (simp add: add_ac zadd_int [symmetric])
    4.15 +  hence "int (Suc(m+n)) = 0" 
    4.16 +    by (simp only: Ring_and_Field.add_left_cancel int_Suc)
    4.17 +  thus False by (simp only: int_eq_0_conv)
    4.18 +  qed
    4.19 +
    4.20  use "int_arith1.ML"
    4.21  setup int_arith_setup
    4.22  
    4.23 -lemma zle_diff1_eq [simp]: "(w <= z - (1::int)) = (w<(z::int))"
    4.24 +subsection{*More inequality reasoning*}
    4.25 +
    4.26 +lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"
    4.27  by arith
    4.28  
    4.29 -lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w<=(z::int))"
    4.30 +lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"
    4.31 +by arith
    4.32 +
    4.33 +lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<(z::int))"
    4.34 +by arith
    4.35 +
    4.36 +lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\<le>(z::int))"
    4.37  by arith
    4.38  
    4.39  lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
    4.40 @@ -22,22 +43,22 @@
    4.41  
    4.42  subsection{*Results about @{term nat}*}
    4.43  
    4.44 -lemma nonneg_eq_int: "[| 0 <= z;  !!m. z = int m ==> P |] ==> P"
    4.45 +lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"
    4.46  by (blast dest: nat_0_le sym)
    4.47  
    4.48 -lemma nat_eq_iff: "(nat w = m) = (if 0 <= w then w = int m else m=0)"
    4.49 +lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
    4.50  by auto
    4.51  
    4.52 -lemma nat_eq_iff2: "(m = nat w) = (if 0 <= w then w = int m else m=0)"
    4.53 +lemma nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    4.54  by auto
    4.55  
    4.56 -lemma nat_less_iff: "0 <= w ==> (nat w < m) = (w < int m)"
    4.57 +lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"
    4.58  apply (rule iffI)
    4.59  apply (erule nat_0_le [THEN subst])
    4.60  apply (simp_all del: zless_int add: zless_int [symmetric]) 
    4.61  done
    4.62  
    4.63 -lemma int_eq_iff: "(int m = z) = (m = nat z & 0 <= z)"
    4.64 +lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"
    4.65  by (auto simp add: nat_eq_iff2)
    4.66  
    4.67  
    4.68 @@ -57,13 +78,13 @@
    4.69  lemma nat_2: "nat 2 = Suc (Suc 0)"
    4.70  by (subst nat_eq_iff, simp)
    4.71  
    4.72 -lemma nat_less_eq_zless: "0 <= w ==> (nat w < nat z) = (w<z)"
    4.73 +lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"
    4.74  apply (case_tac "neg z")
    4.75  apply (auto simp add: nat_less_iff)
    4.76  apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
    4.77  done
    4.78  
    4.79 -lemma nat_le_eq_zle: "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)"
    4.80 +lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"
    4.81  by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
    4.82  
    4.83  subsection{*@{term abs}: Absolute Value, as an Integer*}
    4.84 @@ -72,10 +93,10 @@
    4.85     but arith_tac is not parameterized by such simp rules
    4.86  *)
    4.87  
    4.88 -lemma zabs_split: "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))"
    4.89 +lemma zabs_split: "P(abs(i::int)) = ((0 \<le> i --> P i) & (i < 0 --> P(-i)))"
    4.90  by (simp add: zabs_def)
    4.91  
    4.92 -lemma zero_le_zabs [iff]: "0 <= abs (z::int)"
    4.93 +lemma zero_le_zabs [iff]: "0 \<le> abs (z::int)"
    4.94  by (simp add: zabs_def)
    4.95  
    4.96  
    4.97 @@ -86,7 +107,7 @@
    4.98  declare zabs_split [arith_split]
    4.99  
   4.100  lemma zabs_eq_iff:
   4.101 -    "(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = -w \<and> z < 0)"
   4.102 +    "(abs (z::int) = w) = (z = w \<and> 0 \<le> z \<or> z = -w \<and> z < 0)"
   4.103    by (auto simp add: zabs_def)
   4.104  
   4.105  lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"
   4.106 @@ -117,7 +138,7 @@
   4.107          step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"
   4.108    shows "P i"
   4.109  proof -
   4.110 -  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k <= i \<Longrightarrow> P i"
   4.111 +  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"
   4.112      proof (induct n)
   4.113        case 0
   4.114        hence "i = k" by arith
   4.115 @@ -153,7 +174,7 @@
   4.116          step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"
   4.117    shows "P i"
   4.118  proof -
   4.119 -  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i <= k \<Longrightarrow> P i"
   4.120 +  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"
   4.121      proof (induct n)
   4.122        case 0
   4.123        hence "i = k" by arith
   4.124 @@ -193,7 +214,7 @@
   4.125  lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
   4.126  by arith
   4.127  
   4.128 -lemma triangle_ineq: "abs(x+y) <= abs(x) + abs(y::int)"
   4.129 +lemma triangle_ineq: "abs(x+y) \<le> abs(x) + abs(y::int)"
   4.130  by arith
   4.131  
   4.132  
     5.1 --- a/src/HOL/Integ/NatBin.thy	Wed Dec 03 10:49:34 2003 +0100
     5.2 +++ b/src/HOL/Integ/NatBin.thy	Thu Dec 04 10:29:17 2003 +0100
     5.3 @@ -6,20 +6,516 @@
     5.4  
     5.5  header {* Binary arithmetic for the natural numbers *}
     5.6  
     5.7 -theory NatBin = IntPower
     5.8 -files ("nat_bin.ML"):
     5.9 +theory NatBin = IntPower:
    5.10  
    5.11  text {*
    5.12    This case is simply reduced to that for the non-negative integers.
    5.13  *}
    5.14  
    5.15 -
    5.16  instance nat :: number ..
    5.17  
    5.18  defs (overloaded)
    5.19    nat_number_of_def: "(number_of::bin => nat) v == nat ((number_of :: bin => int) v)"
    5.20  
    5.21 -use "nat_bin.ML"
    5.22 +
    5.23 +(** nat (coercion from int to nat) **)
    5.24 +
    5.25 +lemma nat_number_of: "nat (number_of w) = number_of w"
    5.26 +apply (simp (no_asm) add: nat_number_of_def)
    5.27 +done
    5.28 +declare nat_number_of [simp] nat_0 [simp] nat_1 [simp]
    5.29 +
    5.30 +lemma numeral_0_eq_0: "Numeral0 = (0::nat)"
    5.31 +apply (simp (no_asm) add: nat_number_of_def)
    5.32 +done
    5.33 +
    5.34 +lemma numeral_1_eq_1: "Numeral1 = (1::nat)"
    5.35 +apply (simp (no_asm) add: nat_1 nat_number_of_def)
    5.36 +done
    5.37 +
    5.38 +lemma numeral_1_eq_Suc_0: "Numeral1 = Suc 0"
    5.39 +apply (simp (no_asm) add: numeral_1_eq_1)
    5.40 +done
    5.41 +
    5.42 +lemma numeral_2_eq_2: "2 = Suc (Suc 0)"
    5.43 +apply (unfold nat_number_of_def)
    5.44 +apply (rule nat_2)
    5.45 +done
    5.46 +
    5.47 +
    5.48 +(** Distributive laws for "nat".  The others are in IntArith.ML, but these
    5.49 +    require div and mod to be defined for type "int".  They also need 
    5.50 +    some of the lemmas proved just above.**)
    5.51 +
    5.52 +lemma nat_div_distrib: "(0::int) <= z ==> nat (z div z') = nat z div nat z'"
    5.53 +apply (case_tac "0 <= z'")
    5.54 +apply (auto simp add: div_nonneg_neg_le0 DIVISION_BY_ZERO_DIV)
    5.55 +apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO)
    5.56 +apply (auto elim!: nonneg_eq_int)
    5.57 +apply (rename_tac m m')
    5.58 +apply (subgoal_tac "0 <= int m div int m'")
    5.59 + prefer 2 apply (simp add: numeral_0_eq_0 pos_imp_zdiv_nonneg_iff) 
    5.60 +apply (rule inj_int [THEN injD])
    5.61 +apply (simp (no_asm_simp))
    5.62 +apply (rule_tac r = "int (m mod m') " in quorem_div)
    5.63 + prefer 2 apply (force)
    5.64 +apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int)
    5.65 +done
    5.66 +
    5.67 +(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
    5.68 +lemma nat_mod_distrib: "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'"
    5.69 +apply (case_tac "z' = 0" , simp (no_asm_simp) add: DIVISION_BY_ZERO)
    5.70 +apply (auto elim!: nonneg_eq_int)
    5.71 +apply (rename_tac m m')
    5.72 +apply (subgoal_tac "0 <= int m mod int m'")
    5.73 + prefer 2 apply (simp add: nat_less_iff numeral_0_eq_0 pos_mod_sign) 
    5.74 +apply (rule inj_int [THEN injD])
    5.75 +apply (simp (no_asm_simp))
    5.76 +apply (rule_tac q = "int (m div m') " in quorem_mod)
    5.77 + prefer 2 apply (force)
    5.78 +apply (simp add: nat_less_iff [symmetric] quorem_def numeral_0_eq_0 zadd_int zmult_int)
    5.79 +done
    5.80 +
    5.81 +
    5.82 +(** int (coercion from nat to int) **)
    5.83 +
    5.84 +(*"neg" is used in rewrite rules for binary comparisons*)
    5.85 +lemma int_nat_number_of: "int (number_of v :: nat) =  
    5.86 +         (if neg (number_of v) then 0  
    5.87 +          else (number_of v :: int))"
    5.88 +by (simp del: nat_number_of
    5.89 +	 add: neg_nat nat_number_of_def not_neg_nat add_assoc)
    5.90 +declare int_nat_number_of [simp]
    5.91 +
    5.92 +
    5.93 +(** Successor **)
    5.94 +
    5.95 +lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
    5.96 +apply (rule sym)
    5.97 +apply (simp (no_asm_simp) add: nat_eq_iff int_Suc)
    5.98 +done
    5.99 +
   5.100 +lemma Suc_nat_number_of_add: "Suc (number_of v + n) =  
   5.101 +        (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)" 
   5.102 +by (simp del: nat_number_of 
   5.103 +         add: nat_number_of_def neg_nat
   5.104 +              Suc_nat_eq_nat_zadd1 number_of_succ) 
   5.105 +
   5.106 +lemma Suc_nat_number_of: "Suc (number_of v) =  
   5.107 +        (if neg (number_of v) then 1 else number_of (bin_succ v))"
   5.108 +apply (cut_tac n = "0" in Suc_nat_number_of_add)
   5.109 +apply (simp cong del: if_weak_cong)
   5.110 +done
   5.111 +declare Suc_nat_number_of [simp]
   5.112 +
   5.113 +
   5.114 +(** Addition **)
   5.115 +
   5.116 +(*"neg" is used in rewrite rules for binary comparisons*)
   5.117 +lemma add_nat_number_of: "(number_of v :: nat) + number_of v' =  
   5.118 +         (if neg (number_of v) then number_of v'  
   5.119 +          else if neg (number_of v') then number_of v  
   5.120 +          else number_of (bin_add v v'))"
   5.121 +by (force dest!: neg_nat
   5.122 +          simp del: nat_number_of
   5.123 +          simp add: nat_number_of_def nat_add_distrib [symmetric]) 
   5.124 +
   5.125 +declare add_nat_number_of [simp]
   5.126 +
   5.127 +
   5.128 +(** Subtraction **)
   5.129 +
   5.130 +lemma diff_nat_eq_if: "nat z - nat z' =  
   5.131 +        (if neg z' then nat z   
   5.132 +         else let d = z-z' in     
   5.133 +              if neg d then 0 else nat d)"
   5.134 +apply (simp (no_asm) add: Let_def nat_diff_distrib [symmetric] neg_eq_less_0 not_neg_eq_ge_0)
   5.135 +apply (simp (no_asm) add: diff_is_0_eq nat_le_eq_zle)
   5.136 +done
   5.137 +
   5.138 +lemma diff_nat_number_of: 
   5.139 +     "(number_of v :: nat) - number_of v' =  
   5.140 +        (if neg (number_of v') then number_of v  
   5.141 +         else let d = number_of (bin_add v (bin_minus v')) in     
   5.142 +              if neg d then 0 else nat d)"
   5.143 +by (simp del: nat_number_of add: diff_nat_eq_if nat_number_of_def) 
   5.144 +
   5.145 +declare diff_nat_number_of [simp]
   5.146 +
   5.147 +
   5.148 +(** Multiplication **)
   5.149 +
   5.150 +lemma mult_nat_number_of: "(number_of v :: nat) * number_of v' =  
   5.151 +       (if neg (number_of v) then 0 else number_of (bin_mult v v'))"
   5.152 +by (force dest!: neg_nat
   5.153 +          simp del: nat_number_of
   5.154 +          simp add: nat_number_of_def nat_mult_distrib [symmetric]) 
   5.155 +
   5.156 +declare mult_nat_number_of [simp]
   5.157 +
   5.158 +
   5.159 +(** Quotient **)
   5.160 +
   5.161 +lemma div_nat_number_of: "(number_of v :: nat)  div  number_of v' =  
   5.162 +          (if neg (number_of v) then 0  
   5.163 +           else nat (number_of v div number_of v'))"
   5.164 +by (force dest!: neg_nat
   5.165 +          simp del: nat_number_of
   5.166 +          simp add: nat_number_of_def nat_div_distrib [symmetric]) 
   5.167 +
   5.168 +declare div_nat_number_of [simp]
   5.169 +
   5.170 +
   5.171 +(** Remainder **)
   5.172 +
   5.173 +lemma mod_nat_number_of: "(number_of v :: nat)  mod  number_of v' =  
   5.174 +        (if neg (number_of v) then 0  
   5.175 +         else if neg (number_of v') then number_of v  
   5.176 +         else nat (number_of v mod number_of v'))"
   5.177 +by (force dest!: neg_nat
   5.178 +          simp del: nat_number_of
   5.179 +          simp add: nat_number_of_def nat_mod_distrib [symmetric]) 
   5.180 +
   5.181 +declare mod_nat_number_of [simp]
   5.182 +
   5.183 +ML
   5.184 +{*
   5.185 +val nat_number_of_def = thm"nat_number_of_def";
   5.186 +
   5.187 +val nat_number_of = thm"nat_number_of";
   5.188 +val numeral_0_eq_0 = thm"numeral_0_eq_0";
   5.189 +val numeral_1_eq_1 = thm"numeral_1_eq_1";
   5.190 +val numeral_1_eq_Suc_0 = thm"numeral_1_eq_Suc_0";
   5.191 +val numeral_2_eq_2 = thm"numeral_2_eq_2";
   5.192 +val nat_div_distrib = thm"nat_div_distrib";
   5.193 +val nat_mod_distrib = thm"nat_mod_distrib";
   5.194 +val int_nat_number_of = thm"int_nat_number_of";
   5.195 +val Suc_nat_eq_nat_zadd1 = thm"Suc_nat_eq_nat_zadd1";
   5.196 +val Suc_nat_number_of_add = thm"Suc_nat_number_of_add";
   5.197 +val Suc_nat_number_of = thm"Suc_nat_number_of";
   5.198 +val add_nat_number_of = thm"add_nat_number_of";
   5.199 +val diff_nat_eq_if = thm"diff_nat_eq_if";
   5.200 +val diff_nat_number_of = thm"diff_nat_number_of";
   5.201 +val mult_nat_number_of = thm"mult_nat_number_of";
   5.202 +val div_nat_number_of = thm"div_nat_number_of";
   5.203 +val mod_nat_number_of = thm"mod_nat_number_of";
   5.204 +*}
   5.205 +
   5.206 +
   5.207 +ML
   5.208 +{*
   5.209 +structure NatAbstractNumeralsData =
   5.210 +  struct
   5.211 +  val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   5.212 +  val is_numeral	= Bin_Simprocs.is_numeral
   5.213 +  val numeral_0_eq_0    = numeral_0_eq_0
   5.214 +  val numeral_1_eq_1    = numeral_1_eq_Suc_0
   5.215 +  val prove_conv        = Bin_Simprocs.prove_conv_nohyps_novars
   5.216 +  fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
   5.217 +  val simplify_meta_eq  = Bin_Simprocs.simplify_meta_eq 
   5.218 +  end;
   5.219 +
   5.220 +structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData);
   5.221 +
   5.222 +val nat_eval_numerals = 
   5.223 +  map Bin_Simprocs.prep_simproc
   5.224 +   [("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of),
   5.225 +    ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)];
   5.226 +
   5.227 +Addsimprocs nat_eval_numerals;
   5.228 +*}
   5.229 +
   5.230 +(*** Comparisons ***)
   5.231 +
   5.232 +(** Equals (=) **)
   5.233 +
   5.234 +lemma eq_nat_nat_iff: "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')"
   5.235 +apply (auto elim!: nonneg_eq_int)
   5.236 +done
   5.237 +
   5.238 +(*"neg" is used in rewrite rules for binary comparisons*)
   5.239 +lemma eq_nat_number_of: "((number_of v :: nat) = number_of v') =  
   5.240 +      (if neg (number_of v) then (iszero (number_of v') | neg (number_of v'))  
   5.241 +       else if neg (number_of v') then iszero (number_of v)  
   5.242 +       else iszero (number_of (bin_add v (bin_minus v'))))"
   5.243 +apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   5.244 +                  eq_nat_nat_iff eq_number_of_eq nat_0 iszero_def
   5.245 +            split add: split_if cong add: imp_cong);
   5.246 +apply (simp only: nat_eq_iff nat_eq_iff2)
   5.247 +apply (simp add: not_neg_eq_ge_0 [symmetric])
   5.248 +done
   5.249 +
   5.250 +declare eq_nat_number_of [simp]
   5.251 +
   5.252 +(** Less-than (<) **)
   5.253 +
   5.254 +(*"neg" is used in rewrite rules for binary comparisons*)
   5.255 +lemma less_nat_number_of: "((number_of v :: nat) < number_of v') =  
   5.256 +         (if neg (number_of v) then neg (number_of (bin_minus v'))  
   5.257 +          else neg (number_of (bin_add v (bin_minus v'))))"
   5.258 +apply (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def
   5.259 +                nat_less_eq_zless less_number_of_eq_neg zless_nat_eq_int_zless
   5.260 +            cong add: imp_cong);
   5.261 +apply (simp add: ); 
   5.262 +done
   5.263 +
   5.264 +declare less_nat_number_of [simp]
   5.265 +
   5.266 +
   5.267 +(** Less-than-or-equals (<=) **)
   5.268 +
   5.269 +lemma le_nat_number_of_eq_not_less: "(number_of x <= (number_of y::nat)) =  
   5.270 +      (~ number_of y < (number_of x::nat))"
   5.271 +apply (rule linorder_not_less [symmetric])
   5.272 +done
   5.273 +
   5.274 +declare le_nat_number_of_eq_not_less [simp]
   5.275 +
   5.276 +
   5.277 +(*Maps #n to n for n = 0, 1, 2*)
   5.278 +lemmas numerals = numeral_0_eq_0 numeral_1_eq_1 numeral_2_eq_2
   5.279 +
   5.280 +
   5.281 +(** Nat **)
   5.282 +
   5.283 +lemma Suc_pred': "0 < n ==> n = Suc(n - 1)"
   5.284 +apply (simp add: numerals)
   5.285 +done
   5.286 +
   5.287 +(*Expresses a natural number constant as the Suc of another one.
   5.288 +  NOT suitable for rewriting because n recurs in the condition.*)
   5.289 +lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
   5.290 +
   5.291 +(** Arith **)
   5.292 +
   5.293 +lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
   5.294 +apply (simp add: numerals)
   5.295 +done
   5.296 +
   5.297 +(* These two can be useful when m = number_of... *)
   5.298 +
   5.299 +lemma add_eq_if: "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))"
   5.300 +apply (case_tac "m")
   5.301 +apply (simp_all add: numerals)
   5.302 +done
   5.303 +
   5.304 +lemma mult_eq_if: "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))"
   5.305 +apply (case_tac "m")
   5.306 +apply (simp_all add: numerals)
   5.307 +done
   5.308 +
   5.309 +lemma power_eq_if: "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))"
   5.310 +apply (case_tac "m")
   5.311 +apply (simp_all add: numerals)
   5.312 +done
   5.313 +
   5.314 +lemma diff_less': "[| 0<n; 0<m |] ==> m - n < (m::nat)"
   5.315 +apply (simp add: diff_less numerals)
   5.316 +done
   5.317 +
   5.318 +declare diff_less' [of "number_of v", standard, simp]
   5.319 +
   5.320 +(** Power **)
   5.321 +
   5.322 +lemma power_two: "(p::nat) ^ 2 = p*p"
   5.323 +apply (simp add: numerals)
   5.324 +done
   5.325 +
   5.326 +
   5.327 +(*** Comparisons involving (0::nat) ***)
   5.328 +
   5.329 +lemma eq_number_of_0: "(number_of v = (0::nat)) =  
   5.330 +      (if neg (number_of v) then True else iszero (number_of v))"
   5.331 +apply (simp (no_asm) add: numeral_0_eq_0 [symmetric] iszero_0)
   5.332 +done
   5.333 +
   5.334 +lemma eq_0_number_of: "((0::nat) = number_of v) =  
   5.335 +      (if neg (number_of v) then True else iszero (number_of v))"
   5.336 +apply (rule trans [OF eq_sym_conv eq_number_of_0])
   5.337 +done
   5.338 +
   5.339 +lemma less_0_number_of: "((0::nat) < number_of v) = neg (number_of (bin_minus v))"
   5.340 +apply (simp (no_asm) add: numeral_0_eq_0 [symmetric])
   5.341 +done
   5.342 +
   5.343 +(*Simplification already handles n<0, n<=0 and 0<=n.*)
   5.344 +declare eq_number_of_0 [simp] eq_0_number_of [simp] less_0_number_of [simp]
   5.345 +
   5.346 +lemma neg_imp_number_of_eq_0: "neg (number_of v) ==> number_of v = (0::nat)"
   5.347 +apply (simp (no_asm_simp) add: numeral_0_eq_0 [symmetric] iszero_0)
   5.348 +done
   5.349 +
   5.350 +
   5.351 +
   5.352 +(*** Comparisons involving Suc ***)
   5.353 +
   5.354 +lemma eq_number_of_Suc [simp]: "(number_of v = Suc n) =  
   5.355 +        (let pv = number_of (bin_pred v) in  
   5.356 +         if neg pv then False else nat pv = n)"
   5.357 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   5.358 +                  number_of_pred nat_number_of_def 
   5.359 +            split add: split_if);
   5.360 +apply (rule_tac x = "number_of v" in spec)
   5.361 +apply (auto simp add: nat_eq_iff)
   5.362 +done
   5.363 +
   5.364 +lemma Suc_eq_number_of [simp]: "(Suc n = number_of v) =  
   5.365 +        (let pv = number_of (bin_pred v) in  
   5.366 +         if neg pv then False else nat pv = n)"
   5.367 +apply (rule trans [OF eq_sym_conv eq_number_of_Suc])
   5.368 +done
   5.369 +
   5.370 +lemma less_number_of_Suc [simp]: "(number_of v < Suc n) =  
   5.371 +        (let pv = number_of (bin_pred v) in  
   5.372 +         if neg pv then True else nat pv < n)"
   5.373 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   5.374 +                  number_of_pred nat_number_of_def  
   5.375 +            split add: split_if);
   5.376 +apply (rule_tac x = "number_of v" in spec)
   5.377 +apply (auto simp add: nat_less_iff)
   5.378 +done
   5.379 +
   5.380 +lemma less_Suc_number_of [simp]: "(Suc n < number_of v) =  
   5.381 +        (let pv = number_of (bin_pred v) in  
   5.382 +         if neg pv then False else n < nat pv)"
   5.383 +apply (simp only: simp_thms Let_def neg_eq_less_0 linorder_not_less 
   5.384 +                  number_of_pred nat_number_of_def
   5.385 +            split add: split_if);
   5.386 +apply (rule_tac x = "number_of v" in spec)
   5.387 +apply (auto simp add: zless_nat_eq_int_zless)
   5.388 +done
   5.389 +
   5.390 +lemma le_number_of_Suc [simp]: "(number_of v <= Suc n) =  
   5.391 +        (let pv = number_of (bin_pred v) in  
   5.392 +         if neg pv then True else nat pv <= n)"
   5.393 +apply (simp (no_asm) add: Let_def less_Suc_number_of linorder_not_less [symmetric])
   5.394 +done
   5.395 +
   5.396 +lemma le_Suc_number_of [simp]: "(Suc n <= number_of v) =  
   5.397 +        (let pv = number_of (bin_pred v) in  
   5.398 +         if neg pv then False else n <= nat pv)"
   5.399 +apply (simp (no_asm) add: Let_def less_number_of_Suc linorder_not_less [symmetric])
   5.400 +done
   5.401 +
   5.402 +
   5.403 +(* Push int(.) inwards: *)
   5.404 +declare zadd_int [symmetric, simp]
   5.405 +
   5.406 +lemma lemma1: "(m+m = n+n) = (m = (n::int))"
   5.407 +apply auto
   5.408 +done
   5.409 +
   5.410 +lemma lemma2: "m+m ~= (1::int) + (n + n)"
   5.411 +apply auto
   5.412 +apply (drule_tac f = "%x. x mod 2" in arg_cong)
   5.413 +apply (simp (no_asm_use) add: zmod_zadd1_eq)
   5.414 +done
   5.415 +
   5.416 +lemma eq_number_of_BIT_BIT: "((number_of (v BIT x) ::int) = number_of (w BIT y)) =  
   5.417 +      (x=y & (((number_of v) ::int) = number_of w))"
   5.418 +by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute
   5.419 +               Ring_and_Field.add_left_cancel add_assoc left_zero
   5.420 +            split add: split_if cong: imp_cong); 
   5.421 +
   5.422 +
   5.423 +lemma eq_number_of_BIT_Pls: "((number_of (v BIT x) ::int) = number_of bin.Pls) =  
   5.424 +      (x=False & (((number_of v) ::int) = number_of bin.Pls))"
   5.425 +apply (simp only: simp_thms  add: number_of_BIT number_of_Pls eq_commute
   5.426 +            split add: split_if cong: imp_cong)
   5.427 +apply (rule_tac x = "number_of v" in spec)
   5.428 +apply safe
   5.429 +apply (simp_all (no_asm_use))
   5.430 +apply (drule_tac f = "%x. x mod 2" in arg_cong)
   5.431 +apply (simp (no_asm_use) add: zmod_zadd1_eq)
   5.432 +done
   5.433 +
   5.434 +lemma eq_number_of_BIT_Min: "((number_of (v BIT x) ::int) = number_of bin.Min) =  
   5.435 +      (x=True & (((number_of v) ::int) = number_of bin.Min))"
   5.436 +apply (simp only: simp_thms  add: number_of_BIT number_of_Min eq_commute
   5.437 +            split add: split_if cong: imp_cong)
   5.438 +apply (rule_tac x = "number_of v" in spec)
   5.439 +apply auto
   5.440 +apply (drule_tac f = "%x. x mod 2" in arg_cong)
   5.441 +apply auto
   5.442 +done
   5.443 +
   5.444 +lemma eq_number_of_Pls_Min: "(number_of bin.Pls ::int) ~= number_of bin.Min"
   5.445 +apply auto
   5.446 +done
   5.447 +
   5.448 +
   5.449 +
   5.450 +(*** Literal arithmetic involving powers, type nat ***)
   5.451 +
   5.452 +lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n"
   5.453 +apply (induct_tac "n")
   5.454 +apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   5.455 +done
   5.456 +
   5.457 +lemma power_nat_number_of: "(number_of v :: nat) ^ n =  
   5.458 +       (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))"
   5.459 +by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq
   5.460 +         split add: split_if cong: imp_cong)
   5.461 +
   5.462 +
   5.463 +declare power_nat_number_of [of _ "number_of w", standard, simp]
   5.464 +
   5.465 +
   5.466 +
   5.467 +(*** Literal arithmetic involving powers, type int ***)
   5.468 +
   5.469 +lemma zpower_even: "(z::int) ^ (2*a) = (z^a)^2"
   5.470 +apply (simp (no_asm) add: zpower_zpower mult_commute)
   5.471 +done
   5.472 +
   5.473 +lemma zpower_two: "(p::int) ^ 2 = p*p"
   5.474 +apply (simp add: numerals)
   5.475 +done
   5.476 +
   5.477 +lemma zpower_odd: "(z::int) ^ (2*a + 1) = z * (z^a)^2"
   5.478 +apply (simp (no_asm) add: zpower_even zpower_zadd_distrib)
   5.479 +done
   5.480 +
   5.481 +lemma zpower_number_of_even: "(z::int) ^ number_of (w BIT False) =  
   5.482 +      (let w = z ^ (number_of w) in  w*w)"
   5.483 +apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
   5.484 +apply (simp only: number_of_add) 
   5.485 +apply (rule_tac x = "number_of w" in spec , clarify)
   5.486 +apply (case_tac " (0::int) <= x")
   5.487 +apply (auto simp add: nat_mult_distrib zpower_even zpower_two)
   5.488 +done
   5.489 +
   5.490 +lemma zpower_number_of_odd: "(z::int) ^ number_of (w BIT True) =  
   5.491 +          (if (0::int) <= number_of w                    
   5.492 +           then (let w = z ^ (number_of w) in  z*w*w)    
   5.493 +           else 1)"
   5.494 +apply (simp del: nat_number_of  add: nat_number_of_def number_of_BIT Let_def)
   5.495 +apply (simp only: number_of_add int_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) 
   5.496 +apply (rule_tac x = "number_of w" in spec , clarify)
   5.497 +apply (auto simp add: nat_add_distrib nat_mult_distrib zpower_even zpower_two neg_nat)
   5.498 +done
   5.499 +
   5.500 +declare zpower_number_of_even [of "number_of v", standard, simp]
   5.501 +declare zpower_number_of_odd  [of "number_of v", standard, simp]
   5.502 +
   5.503 +
   5.504 +
   5.505 +ML
   5.506 +{*
   5.507 +val numerals = thms"numerals";
   5.508 +val numeral_ss = simpset() addsimps numerals;
   5.509 +
   5.510 +val nat_bin_arith_setup =
   5.511 + [Fast_Arith.map_data 
   5.512 +   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
   5.513 +     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   5.514 +      inj_thms = inj_thms,
   5.515 +      lessD = lessD,
   5.516 +      simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
   5.517 +                                  not_neg_number_of_Pls,
   5.518 +                                  neg_number_of_Min,neg_number_of_BIT]})]
   5.519 +*}
   5.520 +
   5.521  setup nat_bin_arith_setup
   5.522  
   5.523  (* Enable arith to deal with div/mod k where k is a numeral: *)
   5.524 @@ -64,6 +560,52 @@
   5.525    by (simp add: Let_def)
   5.526  
   5.527  
   5.528 +subsection {*More ML Bindings*}
   5.529 +
   5.530 +ML
   5.531 +{*
   5.532 +val eq_nat_nat_iff = thm"eq_nat_nat_iff";
   5.533 +val eq_nat_number_of = thm"eq_nat_number_of";
   5.534 +val less_nat_number_of = thm"less_nat_number_of";
   5.535 +val le_nat_number_of_eq_not_less = thm"le_nat_number_of_eq_not_less";
   5.536 +val Suc_pred' = thm"Suc_pred'";
   5.537 +val expand_Suc = thm"expand_Suc";
   5.538 +val Suc_eq_add_numeral_1 = thm"Suc_eq_add_numeral_1";
   5.539 +val add_eq_if = thm"add_eq_if";
   5.540 +val mult_eq_if = thm"mult_eq_if";
   5.541 +val power_eq_if = thm"power_eq_if";
   5.542 +val diff_less' = thm"diff_less'";
   5.543 +val power_two = thm"power_two";
   5.544 +val eq_number_of_0 = thm"eq_number_of_0";
   5.545 +val eq_0_number_of = thm"eq_0_number_of";
   5.546 +val less_0_number_of = thm"less_0_number_of";
   5.547 +val neg_imp_number_of_eq_0 = thm"neg_imp_number_of_eq_0";
   5.548 +val eq_number_of_Suc = thm"eq_number_of_Suc";
   5.549 +val Suc_eq_number_of = thm"Suc_eq_number_of";
   5.550 +val less_number_of_Suc = thm"less_number_of_Suc";
   5.551 +val less_Suc_number_of = thm"less_Suc_number_of";
   5.552 +val le_number_of_Suc = thm"le_number_of_Suc";
   5.553 +val le_Suc_number_of = thm"le_Suc_number_of";
   5.554 +val eq_number_of_BIT_BIT = thm"eq_number_of_BIT_BIT";
   5.555 +val eq_number_of_BIT_Pls = thm"eq_number_of_BIT_Pls";
   5.556 +val eq_number_of_BIT_Min = thm"eq_number_of_BIT_Min";
   5.557 +val eq_number_of_Pls_Min = thm"eq_number_of_Pls_Min";
   5.558 +val nat_power_eq = thm"nat_power_eq";
   5.559 +val power_nat_number_of = thm"power_nat_number_of";
   5.560 +val zpower_even = thm"zpower_even";
   5.561 +val zpower_two = thm"zpower_two";
   5.562 +val zpower_odd = thm"zpower_odd";
   5.563 +val zpower_number_of_even = thm"zpower_number_of_even";
   5.564 +val zpower_number_of_odd = thm"zpower_number_of_odd";
   5.565 +val nat_number_of_Pls = thm"nat_number_of_Pls";
   5.566 +val nat_number_of_Min = thm"nat_number_of_Min";
   5.567 +val nat_number_of_BIT_True = thm"nat_number_of_BIT_True";
   5.568 +val nat_number_of_BIT_False = thm"nat_number_of_BIT_False";
   5.569 +val Let_Suc = thm"Let_Suc";
   5.570 +
   5.571 +val nat_number = thms"nat_number";
   5.572 +*}
   5.573 +
   5.574  subsection {* Configuration of the code generator *}
   5.575  
   5.576  ML {*
     6.1 --- a/src/HOL/Integ/NatSimprocs.ML	Wed Dec 03 10:49:34 2003 +0100
     6.2 +++ b/src/HOL/Integ/NatSimprocs.ML	Thu Dec 04 10:29:17 2003 +0100
     6.3 @@ -6,6 +6,8 @@
     6.4  Simprocs for nat numerals (see also nat_simprocs.ML).
     6.5  *)
     6.6  
     6.7 +val ss_Int = simpset_of Int_thy;
     6.8 +
     6.9  (** For simplifying  Suc m - #n **)
    6.10  
    6.11  Goal "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)";
     7.1 --- a/src/HOL/Integ/int_arith1.ML	Wed Dec 03 10:49:34 2003 +0100
     7.2 +++ b/src/HOL/Integ/int_arith1.ML	Thu Dec 04 10:29:17 2003 +0100
     7.3 @@ -5,74 +5,184 @@
     7.4  Simprocs and decision procedure for linear arithmetic.
     7.5  *)
     7.6  
     7.7 -val zadd_ac = thms "Ring_and_Field.add_ac";
     7.8 -val zmult_ac = thms "Ring_and_Field.mult_ac";
     7.9 -
    7.10 -
    7.11 -Addsimps [int_numeral_0_eq_0, int_numeral_1_eq_1];
    7.12 -
    7.13 -(*** Simprocs for numeric literals ***)
    7.14 -
    7.15 -(** Combining of literal coefficients in sums of products **)
    7.16 -
    7.17 -Goal "(x < y) = (x-y < (0::int))";
    7.18 -by (simp_tac (simpset() addsimps compare_rls) 1);
    7.19 -qed "zless_iff_zdiff_zless_0";
    7.20 +val NCons_Pls = thm"NCons_Pls";
    7.21 +val NCons_Min = thm"NCons_Min";
    7.22 +val NCons_BIT = thm"NCons_BIT";
    7.23 +val number_of_Pls = thm"number_of_Pls";
    7.24 +val number_of_Min = thm"number_of_Min";
    7.25 +val number_of_BIT = thm"number_of_BIT";
    7.26 +val bin_succ_Pls = thm"bin_succ_Pls";
    7.27 +val bin_succ_Min = thm"bin_succ_Min";
    7.28 +val bin_succ_BIT = thm"bin_succ_BIT";
    7.29 +val bin_pred_Pls = thm"bin_pred_Pls";
    7.30 +val bin_pred_Min = thm"bin_pred_Min";
    7.31 +val bin_pred_BIT = thm"bin_pred_BIT";
    7.32 +val bin_minus_Pls = thm"bin_minus_Pls";
    7.33 +val bin_minus_Min = thm"bin_minus_Min";
    7.34 +val bin_minus_BIT = thm"bin_minus_BIT";
    7.35 +val bin_add_Pls = thm"bin_add_Pls";
    7.36 +val bin_add_Min = thm"bin_add_Min";
    7.37 +val bin_mult_Pls = thm"bin_mult_Pls";
    7.38 +val bin_mult_Min = thm"bin_mult_Min";
    7.39 +val bin_mult_BIT = thm"bin_mult_BIT";
    7.40  
    7.41 -Goal "(x = y) = (x-y = (0::int))";
    7.42 -by (simp_tac (simpset() addsimps compare_rls) 1);
    7.43 -qed "eq_iff_zdiff_eq_0";
    7.44 +val zadd_ac = thms "Ring_and_Field.add_ac"
    7.45 +val zmult_ac = thms "Ring_and_Field.mult_ac"
    7.46 +val NCons_Pls_0 = thm"NCons_Pls_0";
    7.47 +val NCons_Pls_1 = thm"NCons_Pls_1";
    7.48 +val NCons_Min_0 = thm"NCons_Min_0";
    7.49 +val NCons_Min_1 = thm"NCons_Min_1";
    7.50 +val bin_succ_1 = thm"bin_succ_1";
    7.51 +val bin_succ_0 = thm"bin_succ_0";
    7.52 +val bin_pred_1 = thm"bin_pred_1";
    7.53 +val bin_pred_0 = thm"bin_pred_0";
    7.54 +val bin_minus_1 = thm"bin_minus_1";
    7.55 +val bin_minus_0 = thm"bin_minus_0";
    7.56 +val bin_add_BIT_11 = thm"bin_add_BIT_11";
    7.57 +val bin_add_BIT_10 = thm"bin_add_BIT_10";
    7.58 +val bin_add_BIT_0 = thm"bin_add_BIT_0";
    7.59 +val bin_add_Pls_right = thm"bin_add_Pls_right";
    7.60 +val bin_add_Min_right = thm"bin_add_Min_right";
    7.61 +val bin_add_BIT_BIT = thm"bin_add_BIT_BIT";
    7.62 +val bin_mult_1 = thm"bin_mult_1";
    7.63 +val bin_mult_0 = thm"bin_mult_0";
    7.64 +val number_of_NCons = thm"number_of_NCons";
    7.65 +val number_of_succ = thm"number_of_succ";
    7.66 +val number_of_pred = thm"number_of_pred";
    7.67 +val number_of_minus = thm"number_of_minus";
    7.68 +val number_of_add = thm"number_of_add";
    7.69 +val diff_number_of_eq = thm"diff_number_of_eq";
    7.70 +val number_of_mult = thm"number_of_mult";
    7.71 +val double_number_of_BIT = thm"double_number_of_BIT";
    7.72 +val int_numeral_0_eq_0 = thm"int_numeral_0_eq_0";
    7.73 +val int_numeral_1_eq_1 = thm"int_numeral_1_eq_1";
    7.74 +val zmult_minus1 = thm"zmult_minus1";
    7.75 +val zmult_minus1_right = thm"zmult_minus1_right";
    7.76 +val zminus_number_of_zmult = thm"zminus_number_of_zmult";
    7.77 +val zminus_1_eq_m1 = thm"zminus_1_eq_m1";
    7.78 +val zero_less_nat_eq = thm"zero_less_nat_eq";
    7.79 +val eq_number_of_eq = thm"eq_number_of_eq";
    7.80 +val iszero_number_of_Pls = thm"iszero_number_of_Pls";
    7.81 +val nonzero_number_of_Min = thm"nonzero_number_of_Min";
    7.82 +val iszero_number_of_BIT = thm"iszero_number_of_BIT";
    7.83 +val iszero_number_of_0 = thm"iszero_number_of_0";
    7.84 +val iszero_number_of_1 = thm"iszero_number_of_1";
    7.85 +val less_number_of_eq_neg = thm"less_number_of_eq_neg";
    7.86 +val not_neg_number_of_Pls = thm"not_neg_number_of_Pls";
    7.87 +val neg_number_of_Min = thm"neg_number_of_Min";
    7.88 +val neg_number_of_BIT = thm"neg_number_of_BIT";
    7.89 +val le_number_of_eq_not_less = thm"le_number_of_eq_not_less";
    7.90 +val zabs_number_of = thm"zabs_number_of";
    7.91 +val zabs_0 = thm"zabs_0";
    7.92 +val zabs_1 = thm"zabs_1";
    7.93 +val number_of_reorient = thm"number_of_reorient";
    7.94 +val add_number_of_left = thm"add_number_of_left";
    7.95 +val mult_number_of_left = thm"mult_number_of_left";
    7.96 +val add_number_of_diff1 = thm"add_number_of_diff1";
    7.97 +val add_number_of_diff2 = thm"add_number_of_diff2";
    7.98 +val less_iff_diff_less_0 = thm"less_iff_diff_less_0";
    7.99 +val eq_iff_diff_eq_0 = thm"eq_iff_diff_eq_0";
   7.100 +val le_iff_diff_le_0 = thm"le_iff_diff_le_0";
   7.101  
   7.102 -Goal "(x <= y) = (x-y <= (0::int))";
   7.103 -by (simp_tac (simpset() addsimps compare_rls) 1);
   7.104 -qed "zle_iff_zdiff_zle_0";
   7.105 +val bin_mult_simps = thms"bin_mult_simps";
   7.106 +val NCons_simps = thms"NCons_simps";
   7.107 +val bin_arith_extra_simps = thms"bin_arith_extra_simps";
   7.108 +val bin_arith_simps = thms"bin_arith_simps";
   7.109 +val bin_rel_simps = thms"bin_rel_simps";
   7.110  
   7.111 +val zless_imp_add1_zle = thm "zless_imp_add1_zle";
   7.112  
   7.113 -(** For combine_numerals **)
   7.114 -
   7.115 -Goal "i*u + (j*u + k) = (i+j)*u + (k::int)";
   7.116 -by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
   7.117 -qed "left_zadd_zmult_distrib";
   7.118 +val combine_common_factor = thm"combine_common_factor";
   7.119 +val eq_add_iff1 = thm"eq_add_iff1";
   7.120 +val eq_add_iff2 = thm"eq_add_iff2";
   7.121 +val less_add_iff1 = thm"less_add_iff1";
   7.122 +val less_add_iff2 = thm"less_add_iff2";
   7.123 +val le_add_iff1 = thm"le_add_iff1";
   7.124 +val le_add_iff2 = thm"le_add_iff2";
   7.125  
   7.126  
   7.127 -(** For cancel_numerals **)
   7.128 +structure Bin_Simprocs =
   7.129 +  struct
   7.130 +  fun prove_conv tacs sg (hyps: thm list) xs (t, u) =
   7.131 +    if t aconv u then None
   7.132 +    else
   7.133 +      let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
   7.134 +      in Some (Tactic.prove sg xs [] eq (K (EVERY tacs))) end
   7.135  
   7.136 -val rel_iff_rel_0_rls = map (inst "y" "?u+?v")
   7.137 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
   7.138 -                           zle_iff_zdiff_zle_0] @
   7.139 -                        map (inst "y" "n")
   7.140 -                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
   7.141 -                           zle_iff_zdiff_zle_0];
   7.142 +  fun prove_conv_nohyps tacs sg = prove_conv tacs sg [];
   7.143 +  fun prove_conv_nohyps_novars tacs sg = prove_conv tacs sg [] [];
   7.144 +
   7.145 +  fun prep_simproc (name, pats, proc) =
   7.146 +    Simplifier.simproc (Theory.sign_of (the_context())) name pats proc;
   7.147 +
   7.148 +  fun is_numeral (Const("Numeral.number_of", _) $ w) = true
   7.149 +    | is_numeral _ = false
   7.150  
   7.151 -Goal "!!i::int. (i*u + m = j*u + n) = ((i-j)*u + m = n)";
   7.152 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   7.153 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   7.154 -qed "eq_add_iff1";
   7.155 +  fun simplify_meta_eq f_number_of_eq f_eq =
   7.156 +      mk_meta_eq ([f_eq, f_number_of_eq] MRS trans)
   7.157  
   7.158 -Goal "!!i::int. (i*u + m = j*u + n) = (m = (j-i)*u + n)";
   7.159 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   7.160 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   7.161 -qed "eq_add_iff2";
   7.162 +  structure IntAbstractNumeralsData =
   7.163 +    struct
   7.164 +    val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   7.165 +    val is_numeral	= is_numeral
   7.166 +    val numeral_0_eq_0    = int_numeral_0_eq_0
   7.167 +    val numeral_1_eq_1    = int_numeral_1_eq_1
   7.168 +    val prove_conv	= prove_conv_nohyps_novars
   7.169 +    fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
   7.170 +    val simplify_meta_eq  = simplify_meta_eq 
   7.171 +    end
   7.172 +
   7.173 +  structure IntAbstractNumerals = AbstractNumeralsFun (IntAbstractNumeralsData)
   7.174 +
   7.175  
   7.176 -Goal "!!i::int. (i*u + m < j*u + n) = ((i-j)*u + m < n)";
   7.177 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   7.178 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   7.179 -qed "less_add_iff1";
   7.180 -
   7.181 -Goal "!!i::int. (i*u + m < j*u + n) = (m < (j-i)*u + n)";
   7.182 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   7.183 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   7.184 -qed "less_add_iff2";
   7.185 +  (*For addition, we already have rules for the operand 0.
   7.186 +    Multiplication is omitted because there are already special rules for 
   7.187 +    both 0 and 1 as operands.  Unary minus is trivial, just have - 1 = -1.
   7.188 +    For the others, having three patterns is a compromise between just having
   7.189 +    one (many spurious calls) and having nine (just too many!) *)
   7.190 +  val eval_numerals = 
   7.191 +    map prep_simproc
   7.192 +     [("int_add_eval_numerals",
   7.193 +       ["(m::int) + 1", "(m::int) + number_of v"], 
   7.194 +       IntAbstractNumerals.proc (number_of_add RS sym)),
   7.195 +      ("int_diff_eval_numerals",
   7.196 +       ["(m::int) - 1", "(m::int) - number_of v"], 
   7.197 +       IntAbstractNumerals.proc diff_number_of_eq),
   7.198 +      ("int_eq_eval_numerals",
   7.199 +       ["(m::int) = 0", "(m::int) = 1", "(m::int) = number_of v"], 
   7.200 +       IntAbstractNumerals.proc eq_number_of_eq),
   7.201 +      ("int_less_eval_numerals",
   7.202 +       ["(m::int) < 0", "(m::int) < 1", "(m::int) < number_of v"], 
   7.203 +       IntAbstractNumerals.proc less_number_of_eq_neg),
   7.204 +      ("int_le_eval_numerals",
   7.205 +       ["(m::int) <= 0", "(m::int) <= 1", "(m::int) <= number_of v"],
   7.206 +       IntAbstractNumerals.proc le_number_of_eq_not_less)]
   7.207  
   7.208 -Goal "!!i::int. (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
   7.209 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
   7.210 -                                     zadd_ac@rel_iff_rel_0_rls) 1);
   7.211 -qed "le_add_iff1";
   7.212 +  (*reorientation simprules using ==, for the following simproc*)
   7.213 +  val meta_zero_reorient = zero_reorient RS eq_reflection
   7.214 +  val meta_one_reorient = one_reorient RS eq_reflection
   7.215 +  val meta_number_of_reorient = number_of_reorient RS eq_reflection
   7.216  
   7.217 -Goal "!!i::int. (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
   7.218 -by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]
   7.219 -                                     @zadd_ac@rel_iff_rel_0_rls) 1);
   7.220 -qed "le_add_iff2";
   7.221 +  (*reorientation simplification procedure: reorients (polymorphic) 
   7.222 +    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
   7.223 +  fun reorient_proc sg _ (_ $ t $ u) =
   7.224 +    case u of
   7.225 +	Const("0", _) => None
   7.226 +      | Const("1", _) => None
   7.227 +      | Const("Numeral.number_of", _) $ _ => None
   7.228 +      | _ => Some (case t of
   7.229 +		  Const("0", _) => meta_zero_reorient
   7.230 +		| Const("1", _) => meta_one_reorient
   7.231 +		| Const("Numeral.number_of", _) $ _ => meta_number_of_reorient)
   7.232 +
   7.233 +  val reorient_simproc = 
   7.234 +      prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc)
   7.235 +
   7.236 +  end;
   7.237 +
   7.238 +
   7.239 +Addsimprocs Bin_Simprocs.eval_numerals;
   7.240 +Addsimprocs [Bin_Simprocs.reorient_simproc];
   7.241  
   7.242  
   7.243  structure Int_Numeral_Simprocs =
   7.244 @@ -285,7 +395,7 @@
   7.245    val dest_sum          = dest_sum
   7.246    val mk_coeff          = mk_coeff
   7.247    val dest_coeff        = dest_coeff 1
   7.248 -  val left_distrib      = left_zadd_zmult_distrib RS trans
   7.249 +  val left_distrib      = combine_common_factor RS trans
   7.250    val prove_conv        = Bin_Simprocs.prove_conv_nohyps
   7.251    val trans_tac          = trans_tac
   7.252    val norm_tac =
   7.253 @@ -436,7 +546,7 @@
   7.254     {add_mono_thms = add_mono_thms @ add_mono_thms_int,
   7.255      mult_mono_thms = mult_mono_thms,
   7.256      inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
   7.257 -    lessD = lessD @ [add1_zle_eq RS iffD2],
   7.258 +    lessD = lessD @ [zless_imp_add1_zle],
   7.259      simpset = simpset addsimps add_rules
   7.260                        addsimprocs simprocs
   7.261                        addcongs [if_weak_cong]}),
     8.1 --- a/src/HOL/Integ/nat_bin.ML	Wed Dec 03 10:49:34 2003 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,500 +0,0 @@
     8.4 -(*  Title:      HOL/nat_bin.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.7 -    Copyright   1999  University of Cambridge
     8.8 -
     8.9 -Binary arithmetic for the natural numbers
    8.10 -*)
    8.11 -
    8.12 -val nat_number_of_def = thm "nat_number_of_def";
    8.13 -
    8.14 -val ss_Int = simpset_of Int_thy;
    8.15 -
    8.16 -(** nat (coercion from int to nat) **)
    8.17 -
    8.18 -Goal "nat (number_of w) = number_of w";
    8.19 -by (simp_tac (simpset() addsimps [nat_number_of_def]) 1);
    8.20 -qed "nat_number_of";
    8.21 -Addsimps [nat_number_of, nat_0, nat_1];
    8.22 -
    8.23 -Goal "Numeral0 = (0::nat)";
    8.24 -by (simp_tac (simpset() addsimps [nat_number_of_def]) 1); 
    8.25 -qed "numeral_0_eq_0";
    8.26 -
    8.27 -Goal "Numeral1 = (1::nat)";
    8.28 -by (simp_tac (simpset() addsimps [nat_1, nat_number_of_def]) 1); 
    8.29 -qed "numeral_1_eq_1";
    8.30 -
    8.31 -Goal "Numeral1 = Suc 0";
    8.32 -by (simp_tac (simpset() addsimps [numeral_1_eq_1]) 1); 
    8.33 -qed "numeral_1_eq_Suc_0";
    8.34 -
    8.35 -Goalw [nat_number_of_def] "2 = Suc (Suc 0)";
    8.36 -by (rtac nat_2 1); 
    8.37 -qed "numeral_2_eq_2";
    8.38 -
    8.39 -
    8.40 -(** Distributive laws for "nat".  The others are in IntArith.ML, but these
    8.41 -    require div and mod to be defined for type "int".  They also need 
    8.42 -    some of the lemmas proved just above.**)
    8.43 -
    8.44 -Goal "(0::int) <= z ==> nat (z div z') = nat z div nat z'";
    8.45 -by (case_tac "0 <= z'" 1);
    8.46 -by (auto_tac (claset(), 
    8.47 -	      simpset() addsimps [div_nonneg_neg_le0, DIVISION_BY_ZERO_DIV]));
    8.48 -by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
    8.49 - by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_DIV]) 1);
    8.50 -by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
    8.51 -by (rename_tac "m m'" 1);
    8.52 -by (subgoal_tac "0 <= int m div int m'" 1);
    8.53 - by (asm_full_simp_tac 
    8.54 -     (simpset() addsimps [numeral_0_eq_0, pos_imp_zdiv_nonneg_iff]) 2);
    8.55 -by (rtac (inj_int RS injD) 1);
    8.56 -by (Asm_simp_tac 1);
    8.57 -by (res_inst_tac [("r", "int (m mod m')")] quorem_div 1);
    8.58 - by (Force_tac 2);
    8.59 -by (asm_full_simp_tac 
    8.60 -    (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
    8.61 -	                 numeral_0_eq_0, zadd_int, zmult_int]) 1);
    8.62 -qed "nat_div_distrib";
    8.63 -
    8.64 -(*Fails if z'<0: the LHS collapses to (nat z) but the RHS doesn't*)
    8.65 -Goal "[| (0::int) <= z;  0 <= z' |] ==> nat (z mod z') = nat z mod nat z'";
    8.66 -by (case_tac "z' = 0" 1 THEN asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1);
    8.67 - by (simp_tac (simpset() addsimps [numeral_0_eq_0, DIVISION_BY_ZERO_MOD]) 1);
    8.68 -by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
    8.69 -by (rename_tac "m m'" 1);
    8.70 -by (subgoal_tac "0 <= int m mod int m'" 1);
    8.71 - by (asm_full_simp_tac 
    8.72 -     (simpset() addsimps [nat_less_iff, numeral_0_eq_0, pos_mod_sign]) 2);
    8.73 -by (rtac (inj_int RS injD) 1);
    8.74 -by (Asm_simp_tac 1);
    8.75 -by (res_inst_tac [("q", "int (m div m')")] quorem_mod 1);
    8.76 - by (Force_tac 2);
    8.77 -by (asm_full_simp_tac 
    8.78 -     (simpset() addsimps [nat_less_iff RS sym, quorem_def, 
    8.79 -		          numeral_0_eq_0, zadd_int, zmult_int]) 1);
    8.80 -qed "nat_mod_distrib";
    8.81 -
    8.82 -
    8.83 -(** int (coercion from nat to int) **)
    8.84 -
    8.85 -(*"neg" is used in rewrite rules for binary comparisons*)
    8.86 -Goal "int (number_of v :: nat) = \
    8.87 -\        (if neg (number_of v) then 0 \
    8.88 -\         else (number_of v :: int))";
    8.89 -by (simp_tac
    8.90 -    (ss_Int addsimps [neg_nat, nat_number_of_def, not_neg_nat, int_0]) 1);
    8.91 -qed "int_nat_number_of";
    8.92 -Addsimps [int_nat_number_of];
    8.93 -
    8.94 -
    8.95 -(** Successor **)
    8.96 -
    8.97 -Goal "(0::int) <= z ==> Suc (nat z) = nat (1 + z)";
    8.98 -by (rtac sym 1);
    8.99 -by (asm_simp_tac (simpset() addsimps [nat_eq_iff, int_Suc]) 1);
   8.100 -qed "Suc_nat_eq_nat_zadd1";
   8.101 -
   8.102 -Goal "Suc (number_of v + n) = \
   8.103 -\       (if neg (number_of v) then 1+n else number_of (bin_succ v) + n)";
   8.104 -by (simp_tac (ss_Int addsimps [neg_nat, nat_1, not_neg_eq_ge_0, 
   8.105 -		               nat_number_of_def, int_Suc, 
   8.106 -		               Suc_nat_eq_nat_zadd1, number_of_succ]) 1);
   8.107 -qed "Suc_nat_number_of_add";
   8.108 -
   8.109 -Goal "Suc (number_of v) = \
   8.110 -\       (if neg (number_of v) then 1 else number_of (bin_succ v))";
   8.111 -by (cut_inst_tac [("n","0")] Suc_nat_number_of_add 1);
   8.112 -by (asm_full_simp_tac (simpset() delcongs [if_weak_cong]) 1); 
   8.113 -qed "Suc_nat_number_of";
   8.114 -Addsimps [Suc_nat_number_of];
   8.115 -
   8.116 -val nat_bin_arith_setup =
   8.117 - [Fast_Arith.map_data 
   8.118 -   (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} =>
   8.119 -     {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   8.120 -      inj_thms = inj_thms,
   8.121 -      lessD = lessD,
   8.122 -      simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
   8.123 -                                  not_neg_number_of_Pls,
   8.124 -                                  neg_number_of_Min,neg_number_of_BIT]})];
   8.125 -
   8.126 -(** Addition **)
   8.127 -
   8.128 -(*"neg" is used in rewrite rules for binary comparisons*)
   8.129 -Goal "(number_of v :: nat) + number_of v' = \
   8.130 -\        (if neg (number_of v) then number_of v' \
   8.131 -\         else if neg (number_of v') then number_of v \
   8.132 -\         else number_of (bin_add v v'))";
   8.133 -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   8.134 -		  	       nat_add_distrib RS sym, number_of_add]) 1);
   8.135 -qed "add_nat_number_of";
   8.136 -
   8.137 -Addsimps [add_nat_number_of];
   8.138 -
   8.139 -
   8.140 -(** Subtraction **)
   8.141 -
   8.142 -Goal "nat z - nat z' = \
   8.143 -\       (if neg z' then nat z  \
   8.144 -\        else let d = z-z' in    \
   8.145 -\             if neg d then 0 else nat d)";
   8.146 -by (simp_tac (simpset() addsimps [Let_def, nat_diff_distrib RS sym,
   8.147 -				  neg_eq_less_0, not_neg_eq_ge_0]) 1);
   8.148 -by (simp_tac (simpset() addsimps [diff_is_0_eq, nat_le_eq_zle]) 1);
   8.149 -qed "diff_nat_eq_if";
   8.150 -
   8.151 -Goalw [nat_number_of_def]
   8.152 -     "(number_of v :: nat) - number_of v' = \
   8.153 -\       (if neg (number_of v') then number_of v \
   8.154 -\        else let d = number_of (bin_add v (bin_minus v')) in    \
   8.155 -\             if neg d then 0 else nat d)";
   8.156 -by (simp_tac (ss_Int delcongs [if_weak_cong]
   8.157 -		     addsimps [not_neg_eq_ge_0, nat_0,
   8.158 -			       diff_nat_eq_if, diff_number_of_eq]) 1);
   8.159 -qed "diff_nat_number_of";
   8.160 -
   8.161 -Addsimps [diff_nat_number_of];
   8.162 -
   8.163 -
   8.164 -(** Multiplication **)
   8.165 -
   8.166 -Goal "(number_of v :: nat) * number_of v' = \
   8.167 -\      (if neg (number_of v) then 0 else number_of (bin_mult v v'))";
   8.168 -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   8.169 -		               nat_mult_distrib RS sym, number_of_mult, 
   8.170 -			       nat_0]) 1);
   8.171 -qed "mult_nat_number_of";
   8.172 -
   8.173 -Addsimps [mult_nat_number_of];
   8.174 -
   8.175 -
   8.176 -(** Quotient **)
   8.177 -
   8.178 -Goal "(number_of v :: nat)  div  number_of v' = \
   8.179 -\         (if neg (number_of v) then 0 \
   8.180 -\          else nat (number_of v div number_of v'))";
   8.181 -by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, neg_nat, 
   8.182 -			       nat_div_distrib RS sym, nat_0]) 1);
   8.183 -qed "div_nat_number_of";
   8.184 -
   8.185 -Addsimps [div_nat_number_of];
   8.186 -
   8.187 -
   8.188 -(** Remainder **)
   8.189 -
   8.190 -Goal "(number_of v :: nat)  mod  number_of v' = \
   8.191 -\       (if neg (number_of v) then 0 \
   8.192 -\        else if neg (number_of v') then number_of v \
   8.193 -\        else nat (number_of v mod number_of v'))";
   8.194 -by (simp_tac (ss_Int addsimps [not_neg_eq_ge_0, nat_number_of_def, 
   8.195 -                               neg_nat, nat_0, DIVISION_BY_ZERO_MOD,
   8.196 -                               nat_mod_distrib RS sym]) 1);
   8.197 -qed "mod_nat_number_of";
   8.198 -
   8.199 -Addsimps [mod_nat_number_of];
   8.200 -
   8.201 -structure NatAbstractNumeralsData =
   8.202 -  struct
   8.203 -  val dest_eq		= HOLogic.dest_eq o HOLogic.dest_Trueprop o concl_of
   8.204 -  val is_numeral	= Bin_Simprocs.is_numeral
   8.205 -  val numeral_0_eq_0    = numeral_0_eq_0
   8.206 -  val numeral_1_eq_1    = numeral_1_eq_Suc_0
   8.207 -  val prove_conv        = Bin_Simprocs.prove_conv_nohyps_novars
   8.208 -  fun norm_tac simps	= ALLGOALS (simp_tac (HOL_ss addsimps simps))
   8.209 -  val simplify_meta_eq  = Bin_Simprocs.simplify_meta_eq 
   8.210 -  end
   8.211 -
   8.212 -structure NatAbstractNumerals = AbstractNumeralsFun (NatAbstractNumeralsData)
   8.213 -
   8.214 -val nat_eval_numerals = 
   8.215 -  map Bin_Simprocs.prep_simproc
   8.216 -   [("nat_div_eval_numerals", ["(Suc 0) div m"], NatAbstractNumerals.proc div_nat_number_of),
   8.217 -    ("nat_mod_eval_numerals", ["(Suc 0) mod m"], NatAbstractNumerals.proc mod_nat_number_of)];
   8.218 -
   8.219 -Addsimprocs nat_eval_numerals;
   8.220 -
   8.221 -
   8.222 -(*** Comparisons ***)
   8.223 -
   8.224 -(** Equals (=) **)
   8.225 -
   8.226 -Goal "[| (0::int) <= z;  0 <= z' |] ==> (nat z = nat z') = (z=z')";
   8.227 -by (auto_tac (claset() addSEs [nonneg_eq_int], simpset()));
   8.228 -qed "eq_nat_nat_iff";
   8.229 -
   8.230 -(*"neg" is used in rewrite rules for binary comparisons*)
   8.231 -Goal "((number_of v :: nat) = number_of v') = \
   8.232 -\     (if neg (number_of v) then (iszero (number_of v') | neg (number_of v')) \
   8.233 -\      else if neg (number_of v') then iszero (number_of v) \
   8.234 -\      else iszero (number_of (bin_add v (bin_minus v'))))";
   8.235 -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   8.236 -                               eq_nat_nat_iff, eq_number_of_eq, nat_0]) 1);
   8.237 -by (simp_tac (ss_Int addsimps [nat_eq_iff, nat_eq_iff2, iszero_def]) 1);
   8.238 -by (simp_tac (simpset () addsimps [not_neg_eq_ge_0 RS sym]) 1);
   8.239 -qed "eq_nat_number_of";
   8.240 -
   8.241 -Addsimps [eq_nat_number_of];
   8.242 -
   8.243 -(** Less-than (<) **)
   8.244 -
   8.245 -(*"neg" is used in rewrite rules for binary comparisons*)
   8.246 -Goal "((number_of v :: nat) < number_of v') = \
   8.247 -\        (if neg (number_of v) then neg (number_of (bin_minus v')) \
   8.248 -\         else neg (number_of (bin_add v (bin_minus v'))))";
   8.249 -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   8.250 -                          nat_less_eq_zless, less_number_of_eq_neg, nat_0]) 1);
   8.251 -by (simp_tac (ss_Int addsimps [neg_eq_less_0, zminus_zless, 
   8.252 -				number_of_minus, zless_nat_eq_int_zless]) 1);
   8.253 -qed "less_nat_number_of";
   8.254 -
   8.255 -Addsimps [less_nat_number_of];
   8.256 -
   8.257 -
   8.258 -(** Less-than-or-equals (<=) **)
   8.259 -
   8.260 -Goal "(number_of x <= (number_of y::nat)) = \
   8.261 -\     (~ number_of y < (number_of x::nat))";
   8.262 -by (rtac (linorder_not_less RS sym) 1);
   8.263 -qed "le_nat_number_of_eq_not_less"; 
   8.264 -
   8.265 -Addsimps [le_nat_number_of_eq_not_less];
   8.266 -
   8.267 -
   8.268 -(*Maps #n to n for n = 0, 1, 2*)
   8.269 -bind_thms ("numerals", [numeral_0_eq_0, numeral_1_eq_1, numeral_2_eq_2]);
   8.270 -val numeral_ss = simpset() addsimps numerals;
   8.271 -
   8.272 -(** Nat **)
   8.273 -
   8.274 -Goal "0 < n ==> n = Suc(n - 1)";
   8.275 -by (asm_full_simp_tac numeral_ss 1);
   8.276 -qed "Suc_pred'";
   8.277 -
   8.278 -(*Expresses a natural number constant as the Suc of another one.
   8.279 -  NOT suitable for rewriting because n recurs in the condition.*)
   8.280 -bind_thm ("expand_Suc", inst "n" "number_of ?v" Suc_pred');
   8.281 -
   8.282 -(** Arith **)
   8.283 -
   8.284 -Goal "Suc n = n + 1";
   8.285 -by (asm_simp_tac numeral_ss 1);
   8.286 -qed "Suc_eq_add_numeral_1";
   8.287 -
   8.288 -(* These two can be useful when m = number_of... *)
   8.289 -
   8.290 -Goal "(m::nat) + n = (if m=0 then n else Suc ((m - 1) + n))";
   8.291 -by (case_tac "m" 1);
   8.292 -by (ALLGOALS (asm_simp_tac numeral_ss));
   8.293 -qed "add_eq_if";
   8.294 -
   8.295 -Goal "(m::nat) * n = (if m=0 then 0 else n + ((m - 1) * n))";
   8.296 -by (case_tac "m" 1);
   8.297 -by (ALLGOALS (asm_simp_tac numeral_ss));
   8.298 -qed "mult_eq_if";
   8.299 -
   8.300 -Goal "(p ^ m :: nat) = (if m=0 then 1 else p * (p ^ (m - 1)))";
   8.301 -by (case_tac "m" 1);
   8.302 -by (ALLGOALS (asm_simp_tac numeral_ss));
   8.303 -qed "power_eq_if";
   8.304 -
   8.305 -Goal "[| 0<n; 0<m |] ==> m - n < (m::nat)";
   8.306 -by (asm_full_simp_tac (numeral_ss addsimps [diff_less]) 1);
   8.307 -qed "diff_less'";
   8.308 -
   8.309 -Addsimps [inst "n" "number_of ?v" diff_less'];
   8.310 -
   8.311 -(** Power **)
   8.312 -
   8.313 -Goal "(p::nat) ^ 2 = p*p";
   8.314 -by (simp_tac numeral_ss 1);
   8.315 -qed "power_two";
   8.316 -
   8.317 -
   8.318 -(*** Comparisons involving (0::nat) ***)
   8.319 -
   8.320 -Goal "(number_of v = (0::nat)) = \
   8.321 -\     (if neg (number_of v) then True else iszero (number_of v))";
   8.322 -by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
   8.323 -qed "eq_number_of_0"; 
   8.324 -
   8.325 -Goal "((0::nat) = number_of v) = \
   8.326 -\     (if neg (number_of v) then True else iszero (number_of v))";
   8.327 -by (rtac ([eq_sym_conv, eq_number_of_0] MRS trans) 1);
   8.328 -qed "eq_0_number_of";
   8.329 -
   8.330 -Goal "((0::nat) < number_of v) = neg (number_of (bin_minus v))";
   8.331 -by (simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym]) 1);
   8.332 -qed "less_0_number_of";
   8.333 -
   8.334 -(*Simplification already handles n<0, n<=0 and 0<=n.*)
   8.335 -Addsimps [eq_number_of_0, eq_0_number_of, less_0_number_of];
   8.336 -
   8.337 -Goal "neg (number_of v) ==> number_of v = (0::nat)";
   8.338 -by (asm_simp_tac (simpset() addsimps [numeral_0_eq_0 RS sym, iszero_0]) 1);
   8.339 -qed "neg_imp_number_of_eq_0";
   8.340 -
   8.341 -
   8.342 -
   8.343 -(*** Comparisons involving Suc ***)
   8.344 -
   8.345 -Goal "(number_of v = Suc n) = \
   8.346 -\       (let pv = number_of (bin_pred v) in \
   8.347 -\        if neg pv then False else nat pv = n)";
   8.348 -by (simp_tac (ss_Int addsimps
   8.349 -	      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   8.350 -	       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   8.351 -by (res_inst_tac [("x", "number_of v")] spec 1);
   8.352 -by (auto_tac (claset(), simpset() addsimps [nat_eq_iff]));
   8.353 -qed "eq_number_of_Suc";
   8.354 -
   8.355 -Goal "(Suc n = number_of v) = \
   8.356 -\       (let pv = number_of (bin_pred v) in \
   8.357 -\        if neg pv then False else nat pv = n)";
   8.358 -by (rtac ([eq_sym_conv, eq_number_of_Suc] MRS trans) 1);
   8.359 -qed "Suc_eq_number_of";
   8.360 -
   8.361 -Goal "(number_of v < Suc n) = \
   8.362 -\       (let pv = number_of (bin_pred v) in \
   8.363 -\        if neg pv then True else nat pv < n)";
   8.364 -by (simp_tac (ss_Int addsimps
   8.365 -	      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   8.366 -	       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   8.367 -by (res_inst_tac [("x", "number_of v")] spec 1);
   8.368 -by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   8.369 -qed "less_number_of_Suc";
   8.370 -
   8.371 -Goal "(Suc n < number_of v) = \
   8.372 -\       (let pv = number_of (bin_pred v) in \
   8.373 -\        if neg pv then False else n < nat pv)";
   8.374 -by (simp_tac (ss_Int addsimps
   8.375 -	      [Let_def, neg_eq_less_0, linorder_not_less, number_of_pred,
   8.376 -	       nat_number_of_def, zadd_0] @ zadd_ac) 1);
   8.377 -by (res_inst_tac [("x", "number_of v")] spec 1);
   8.378 -by (auto_tac (claset(), simpset() addsimps [zless_nat_eq_int_zless]));
   8.379 -qed "less_Suc_number_of";
   8.380 -
   8.381 -Goal "(number_of v <= Suc n) = \
   8.382 -\       (let pv = number_of (bin_pred v) in \
   8.383 -\        if neg pv then True else nat pv <= n)";
   8.384 -by (simp_tac
   8.385 -    (simpset () addsimps
   8.386 -      [Let_def, less_Suc_number_of, linorder_not_less RS sym]) 1);
   8.387 -qed "le_number_of_Suc";
   8.388 -
   8.389 -Goal "(Suc n <= number_of v) = \
   8.390 -\       (let pv = number_of (bin_pred v) in \
   8.391 -\        if neg pv then False else n <= nat pv)";
   8.392 -by (simp_tac
   8.393 -    (simpset () addsimps
   8.394 -      [Let_def, less_number_of_Suc, linorder_not_less RS sym]) 1);
   8.395 -qed "le_Suc_number_of";
   8.396 -
   8.397 -Addsimps [eq_number_of_Suc, Suc_eq_number_of, 
   8.398 -	  less_number_of_Suc, less_Suc_number_of, 
   8.399 -	  le_number_of_Suc, le_Suc_number_of];
   8.400 -
   8.401 -(* Push int(.) inwards: *)
   8.402 -Addsimps [zadd_int RS sym];
   8.403 -
   8.404 -Goal "(m+m = n+n) = (m = (n::int))";
   8.405 -by Auto_tac;
   8.406 -val lemma1 = result();
   8.407 -
   8.408 -Goal "m+m ~= (1::int) + n + n";
   8.409 -by Auto_tac;
   8.410 -by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   8.411 -by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   8.412 -val lemma2 = result();
   8.413 -
   8.414 -Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
   8.415 -\     (x=y & (((number_of v) ::int) = number_of w))"; 
   8.416 -by (simp_tac (ss_Int addsimps [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
   8.417 -qed "eq_number_of_BIT_BIT"; 
   8.418 -
   8.419 -Goal "((number_of (v BIT x) ::int) = number_of bin.Pls) = \
   8.420 -\     (x=False & (((number_of v) ::int) = number_of bin.Pls))"; 
   8.421 -by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Pls, eq_commute]) 1); 
   8.422 -by (res_inst_tac [("x", "number_of v")] spec 1);
   8.423 -by Safe_tac;
   8.424 -by (ALLGOALS Full_simp_tac);
   8.425 -by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   8.426 -by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
   8.427 -qed "eq_number_of_BIT_Pls"; 
   8.428 -
   8.429 -Goal "((number_of (v BIT x) ::int) = number_of bin.Min) = \
   8.430 -\     (x=True & (((number_of v) ::int) = number_of bin.Min))"; 
   8.431 -by (simp_tac (ss_Int addsimps [number_of_BIT, number_of_Min, eq_commute]) 1); 
   8.432 -by (res_inst_tac [("x", "number_of v")] spec 1);
   8.433 -by Auto_tac;
   8.434 -by (dres_inst_tac [("f", "%x. x mod 2")] arg_cong 1);
   8.435 -by Auto_tac;
   8.436 -qed "eq_number_of_BIT_Min"; 
   8.437 -
   8.438 -Goal "(number_of bin.Pls ::int) ~= number_of bin.Min"; 
   8.439 -by Auto_tac;
   8.440 -qed "eq_number_of_Pls_Min"; 
   8.441 -
   8.442 -
   8.443 -(*Distributive laws for literals*)
   8.444 -Addsimps (map (inst "k" "number_of ?v")
   8.445 -	  [add_mult_distrib, add_mult_distrib2,
   8.446 -	   diff_mult_distrib, diff_mult_distrib2]);
   8.447 -
   8.448 -
   8.449 -(*** Literal arithmetic involving powers, type nat ***)
   8.450 -
   8.451 -Goal "(0::int) <= z ==> nat (z^n) = nat z ^ n";
   8.452 -by (induct_tac "n" 1); 
   8.453 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_mult_distrib])));
   8.454 -qed "nat_power_eq";
   8.455 -
   8.456 -Goal "(number_of v :: nat) ^ n = \
   8.457 -\      (if neg (number_of v) then 0^n else nat ((number_of v :: int) ^ n))";
   8.458 -by (simp_tac (ss_Int addsimps [neg_nat, not_neg_eq_ge_0, nat_number_of_def, 
   8.459 -				  nat_power_eq]) 1);
   8.460 -qed "power_nat_number_of";
   8.461 -
   8.462 -Addsimps [inst "n" "number_of ?w" power_nat_number_of];
   8.463 -
   8.464 -
   8.465 -
   8.466 -(*** Literal arithmetic involving powers, type int ***)
   8.467 -
   8.468 -Goal "(z::int) ^ (2*a) = (z^a)^2";
   8.469 -by (simp_tac (simpset() addsimps [zpower_zpower, mult_commute]) 1); 
   8.470 -qed "zpower_even";
   8.471 -
   8.472 -Goal "(p::int) ^ 2 = p*p"; 
   8.473 -by (simp_tac numeral_ss 1);
   8.474 -qed "zpower_two";  
   8.475 -
   8.476 -Goal "(z::int) ^ (2*a + 1) = z * (z^a)^2";
   8.477 -by (simp_tac (simpset() addsimps [zpower_even, zpower_zadd_distrib]) 1); 
   8.478 -qed "zpower_odd";
   8.479 -
   8.480 -Goal "(z::int) ^ number_of (w BIT False) = \
   8.481 -\     (let w = z ^ (number_of w) in  w*w)";
   8.482 -by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1);
   8.483 -by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
   8.484 -by (case_tac "(0::int) <= x" 1);
   8.485 -by (auto_tac (claset(), 
   8.486 -     simpset() addsimps [nat_mult_distrib, zpower_even, zpower_two])); 
   8.487 -qed "zpower_number_of_even";
   8.488 -
   8.489 -Goal "(z::int) ^ number_of (w BIT True) = \
   8.490 -\         (if (0::int) <= number_of w                   \
   8.491 -\          then (let w = z ^ (number_of w) in  z*w*w)   \
   8.492 -\          else 1)";
   8.493 -by (simp_tac (ss_Int addsimps [nat_number_of_def, number_of_BIT, Let_def]) 1);
   8.494 -by (res_inst_tac [("x","number_of w")] spec 1 THEN Clarify_tac 1); 
   8.495 -by (case_tac "(0::int) <= x" 1);
   8.496 -by (auto_tac (claset(), 
   8.497 -              simpset() addsimps [nat_add_distrib, nat_mult_distrib, 
   8.498 -                                  zpower_even, zpower_two])); 
   8.499 -qed "zpower_number_of_odd";
   8.500 -
   8.501 -Addsimps (map (inst "z" "number_of ?v")
   8.502 -              [zpower_number_of_even, zpower_number_of_odd]);
   8.503 -
     9.1 --- a/src/HOL/IsaMakefile	Wed Dec 03 10:49:34 2003 +0100
     9.2 +++ b/src/HOL/IsaMakefile	Thu Dec 04 10:29:17 2003 +0100
     9.3 @@ -84,11 +84,11 @@
     9.4    Divides.thy Extraction.thy Finite_Set.ML Finite_Set.thy \
     9.5    Fun.thy Gfp.ML Gfp.thy \
     9.6    Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
     9.7 -  HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
     9.8 +  HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.thy \
     9.9    Integ/cooper_dec.ML Integ/cooper_proof.ML \
    9.10    Integ/Equiv.thy Integ/Int.thy Integ/IntArith.thy Integ/IntDef.thy \
    9.11    Integ/IntDiv.thy Integ/IntPower.thy \
    9.12 -  Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
    9.13 +  Integ/NatBin.thy Integ/NatSimprocs.ML \
    9.14    Integ/NatSimprocs.thy Integ/int_arith1.ML \
    9.15    Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
    9.16    Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
    10.1 --- a/src/HOL/Ring_and_Field.thy	Wed Dec 03 10:49:34 2003 +0100
    10.2 +++ b/src/HOL/Ring_and_Field.thy	Thu Dec 04 10:29:17 2003 +0100
    10.3 @@ -137,6 +137,20 @@
    10.4  lemma neg_0_equal_iff_equal [simp]: "(0 = -a) = (0 = (a::'a::ring))"
    10.5  by (subst neg_equal_iff_equal [symmetric], simp)
    10.6  
    10.7 +text{*The next two equations can make the simplifier loop!*}
    10.8 +
    10.9 +lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))"
   10.10 +  proof -
   10.11 +  have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal)
   10.12 +  thus ?thesis by (simp add: eq_commute)
   10.13 +  qed
   10.14 +
   10.15 +lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)"
   10.16 +  proof -
   10.17 +  have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal)
   10.18 +  thus ?thesis by (simp add: eq_commute)
   10.19 +  qed
   10.20 +
   10.21  
   10.22  subsection {* Derived rules for multiplication *}
   10.23  
   10.24 @@ -199,6 +213,10 @@
   10.25  
   10.26  theorems ring_distrib = right_distrib left_distrib
   10.27  
   10.28 +text{*For the @{text combine_numerals} simproc*}
   10.29 +lemma combine_common_factor: "a*e + (b*e + c) = (a+b)*e + (c::'a::semiring)"
   10.30 +by (simp add: left_distrib add_ac)
   10.31 +
   10.32  lemma minus_add_distrib [simp]: "- (a + b) = -a + -(b::'a::ring)"
   10.33  apply (rule equals_zero_I)
   10.34  apply (simp add: add_ac) 
   10.35 @@ -221,6 +239,9 @@
   10.36  by (simp add: right_distrib diff_minus 
   10.37                minus_mult_left [symmetric] minus_mult_right [symmetric]) 
   10.38  
   10.39 +lemma left_diff_distrib: "(a - b) * c = a * c - b * (c::'a::ring)"
   10.40 +by (simp add: mult_commute [of _ c] right_diff_distrib) 
   10.41 +
   10.42  lemma minus_diff_eq [simp]: "- (a - b) = b - (a::'a::ring)"
   10.43  by (simp add: diff_minus add_commute) 
   10.44  
   10.45 @@ -330,6 +351,30 @@
   10.46  lemma neg_0_less_iff_less [simp]: "(0 < -a) = (a < (0::'a::ordered_ring))"
   10.47  by (subst neg_less_iff_less [symmetric], simp)
   10.48  
   10.49 +text{*The next several equations can make the simplifier loop!*}
   10.50 +
   10.51 +lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))"
   10.52 +  proof -
   10.53 +  have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less)
   10.54 +  thus ?thesis by simp
   10.55 +  qed
   10.56 +
   10.57 +lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))"
   10.58 +  proof -
   10.59 +  have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less)
   10.60 +  thus ?thesis by simp
   10.61 +  qed
   10.62 +
   10.63 +lemma le_minus_iff: "(a \<le> - b) = (b \<le> - (a::'a::ordered_ring))"
   10.64 +apply (simp add: linorder_not_less [symmetric])
   10.65 +apply (rule minus_less_iff) 
   10.66 +done
   10.67 +
   10.68 +lemma minus_le_iff: "(- a \<le> b) = (- b \<le> (a::'a::ordered_ring))"
   10.69 +apply (simp add: linorder_not_less [symmetric])
   10.70 +apply (rule less_minus_iff) 
   10.71 +done
   10.72 +
   10.73  
   10.74  subsection{*Subtraction Laws*}
   10.75  
   10.76 @@ -353,7 +398,7 @@
   10.77  
   10.78  text{*Further subtraction laws for ordered rings*}
   10.79  
   10.80 -lemma less_eq_diff: "(a < b) = (a - b < (0::'a::ordered_ring))"
   10.81 +lemma less_iff_diff_less_0: "(a < b) = (a - b < (0::'a::ordered_ring))"
   10.82  proof -
   10.83    have  "(a < b) = (a + (- b) < b + (-b))"  
   10.84      by (simp only: add_less_cancel_right)
   10.85 @@ -362,14 +407,14 @@
   10.86  qed
   10.87  
   10.88  lemma diff_less_eq: "(a-b < c) = (a < c + (b::'a::ordered_ring))"
   10.89 -apply (subst less_eq_diff)
   10.90 -apply (rule less_eq_diff [of _ c, THEN ssubst])
   10.91 +apply (subst less_iff_diff_less_0)
   10.92 +apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst])
   10.93  apply (simp add: diff_minus add_ac)
   10.94  done
   10.95  
   10.96  lemma less_diff_eq: "(a < c-b) = (a + (b::'a::ordered_ring) < c)"
   10.97 -apply (subst less_eq_diff)
   10.98 -apply (rule less_eq_diff [of _ "c-b", THEN ssubst])
   10.99 +apply (subst less_iff_diff_less_0)
  10.100 +apply (rule less_iff_diff_less_0 [of _ "c-b", THEN ssubst])
  10.101  apply (simp add: diff_minus add_ac)
  10.102  done
  10.103  
  10.104 @@ -389,6 +434,51 @@
  10.105         diff_eq_eq eq_diff_eq
  10.106  
  10.107  
  10.108 +subsection{*Lemmas for the @{text cancel_numerals} simproc*}
  10.109 +
  10.110 +lemma eq_iff_diff_eq_0: "(a = b) = (a-b = (0::'a::ring))"
  10.111 +by (simp add: compare_rls)
  10.112 +
  10.113 +lemma le_iff_diff_le_0: "(a \<le> b) = (a-b \<le> (0::'a::ordered_ring))"
  10.114 +by (simp add: compare_rls)
  10.115 +
  10.116 +lemma eq_add_iff1:
  10.117 +     "(a*e + c = b*e + d) = ((a-b)*e + c = (d::'a::ring))"
  10.118 +apply (simp add: diff_minus left_distrib add_ac)
  10.119 +apply (simp add: compare_rls minus_mult_left [symmetric]) 
  10.120 +done
  10.121 +
  10.122 +lemma eq_add_iff2:
  10.123 +     "(a*e + c = b*e + d) = (c = (b-a)*e + (d::'a::ring))"
  10.124 +apply (simp add: diff_minus left_distrib add_ac)
  10.125 +apply (simp add: compare_rls minus_mult_left [symmetric]) 
  10.126 +done
  10.127 +
  10.128 +lemma less_add_iff1:
  10.129 +     "(a*e + c < b*e + d) = ((a-b)*e + c < (d::'a::ordered_ring))"
  10.130 +apply (simp add: diff_minus left_distrib add_ac)
  10.131 +apply (simp add: compare_rls minus_mult_left [symmetric]) 
  10.132 +done
  10.133 +
  10.134 +lemma less_add_iff2:
  10.135 +     "(a*e + c < b*e + d) = (c < (b-a)*e + (d::'a::ordered_ring))"
  10.136 +apply (simp add: diff_minus left_distrib add_ac)
  10.137 +apply (simp add: compare_rls minus_mult_left [symmetric]) 
  10.138 +done
  10.139 +
  10.140 +lemma le_add_iff1:
  10.141 +     "(a*e + c \<le> b*e + d) = ((a-b)*e + c \<le> (d::'a::ordered_ring))"
  10.142 +apply (simp add: diff_minus left_distrib add_ac)
  10.143 +apply (simp add: compare_rls minus_mult_left [symmetric]) 
  10.144 +done
  10.145 +
  10.146 +lemma le_add_iff2:
  10.147 +     "(a*e + c \<le> b*e + d) = (c \<le> (b-a)*e + (d::'a::ordered_ring))"
  10.148 +apply (simp add: diff_minus left_distrib add_ac)
  10.149 +apply (simp add: compare_rls minus_mult_left [symmetric]) 
  10.150 +done
  10.151 +
  10.152 +
  10.153  subsection {* Ordering Rules for Multiplication *}
  10.154  
  10.155  lemma mult_strict_right_mono: