src/HOL/Integ/Bin.ML
author nipkow
Wed Jan 27 17:11:39 1999 +0100 (1999-01-27)
changeset 6157 29942d3a1818
parent 6128 2acc5d36610c
child 6301 08245f5a436d
permissions -rw-r--r--
arith_tac for min/max
     1 (*  Title:      HOL/Integ/Bin.ML
     2     Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
     3                 David Spelt, University of Twente 
     4                 Tobias Nipkow, Technical University Munich
     5     Copyright   1994  University of Cambridge
     6     Copyright   1996  University of Twente
     7     Copyright   1999  TU Munich
     8 
     9 Arithmetic on binary integers;
    10 decision procedure for linear arithmetic.
    11 *)
    12 
    13 (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
    14 
    15 qed_goal "NCons_Pls_0" Bin.thy
    16     "NCons Pls False = Pls"
    17  (fn _ => [(Simp_tac 1)]);
    18 
    19 qed_goal "NCons_Pls_1" Bin.thy
    20     "NCons Pls True = Pls BIT True"
    21  (fn _ => [(Simp_tac 1)]);
    22 
    23 qed_goal "NCons_Min_0" Bin.thy
    24     "NCons Min False = Min BIT False"
    25  (fn _ => [(Simp_tac 1)]);
    26 
    27 qed_goal "NCons_Min_1" Bin.thy
    28     "NCons Min True = Min"
    29  (fn _ => [(Simp_tac 1)]);
    30 
    31 qed_goal "bin_succ_1" Bin.thy
    32     "bin_succ(w BIT True) = (bin_succ w) BIT False"
    33  (fn _ => [(Simp_tac 1)]);
    34 
    35 qed_goal "bin_succ_0" Bin.thy
    36     "bin_succ(w BIT False) =  NCons w True"
    37  (fn _ => [(Simp_tac 1)]);
    38 
    39 qed_goal "bin_pred_1" Bin.thy
    40     "bin_pred(w BIT True) = NCons w False"
    41  (fn _ => [(Simp_tac 1)]);
    42 
    43 qed_goal "bin_pred_0" Bin.thy
    44     "bin_pred(w BIT False) = (bin_pred w) BIT True"
    45  (fn _ => [(Simp_tac 1)]);
    46 
    47 qed_goal "bin_minus_1" Bin.thy
    48     "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
    49  (fn _ => [(Simp_tac 1)]);
    50 
    51 qed_goal "bin_minus_0" Bin.thy
    52     "bin_minus(w BIT False) = (bin_minus w) BIT False"
    53  (fn _ => [(Simp_tac 1)]);
    54 
    55 
    56 (*** bin_add: binary addition ***)
    57 
    58 qed_goal "bin_add_BIT_11" Bin.thy
    59     "bin_add (v BIT True) (w BIT True) = \
    60 \    NCons (bin_add v (bin_succ w)) False"
    61  (fn _ => [(Simp_tac 1)]);
    62 
    63 qed_goal "bin_add_BIT_10" Bin.thy
    64     "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
    65  (fn _ => [(Simp_tac 1)]);
    66 
    67 qed_goal "bin_add_BIT_0" Bin.thy
    68     "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
    69  (fn _ => [Auto_tac]);
    70 
    71 Goal "bin_add w Pls = w";
    72 by (induct_tac "w" 1);
    73 by Auto_tac;
    74 qed "bin_add_Pls_right";
    75 
    76 qed_goal "bin_add_BIT_Min" Bin.thy
    77     "bin_add (v BIT x) Min = bin_pred (v BIT x)"
    78  (fn _ => [(Simp_tac 1)]);
    79 
    80 qed_goal "bin_add_BIT_BIT" Bin.thy
    81     "bin_add (v BIT x) (w BIT y) = \
    82 \    NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
    83  (fn _ => [(Simp_tac 1)]);
    84 
    85 
    86 (*** bin_mult: binary multiplication ***)
    87 
    88 qed_goal "bin_mult_1" Bin.thy
    89     "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
    90  (fn _ => [(Simp_tac 1)]);
    91 
    92 qed_goal "bin_mult_0" Bin.thy
    93     "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
    94  (fn _ => [(Simp_tac 1)]);
    95 
    96 
    97 (**** The carry/borrow functions, bin_succ and bin_pred ****)
    98 
    99 
   100 (**** integ_of ****)
   101 
   102 qed_goal "integ_of_NCons" Bin.thy
   103     "integ_of(NCons w b) = integ_of(w BIT b)"
   104  (fn _ =>[(induct_tac "w" 1),
   105           (ALLGOALS Asm_simp_tac) ]);
   106 
   107 Addsimps [integ_of_NCons];
   108 
   109 qed_goal "integ_of_succ" Bin.thy
   110     "integ_of(bin_succ w) = int 1 + integ_of w"
   111  (fn _ =>[(rtac bin.induct 1),
   112           (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
   113 
   114 qed_goal "integ_of_pred" Bin.thy
   115     "integ_of(bin_pred w) = - (int 1) + integ_of w"
   116  (fn _ =>[(rtac bin.induct 1),
   117           (ALLGOALS(asm_simp_tac (simpset() addsimps zadd_ac))) ]);
   118 
   119 Goal "integ_of(bin_minus w) = - (integ_of w)";
   120 by (rtac bin.induct 1);
   121 by (Simp_tac 1);
   122 by (Simp_tac 1);
   123 by (asm_simp_tac (simpset()
   124 		  delsimps [bin_pred_Pls, bin_pred_Min, bin_pred_BIT]
   125 		  addsimps [integ_of_succ,integ_of_pred,
   126 			    zadd_assoc]) 1);
   127 qed "integ_of_minus";
   128 
   129  
   130 val bin_add_simps = [bin_add_BIT_BIT, integ_of_succ, integ_of_pred];
   131 
   132 (*This proof is complicated by the mutual recursion*)
   133 Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w";
   134 by (induct_tac "v" 1);
   135 by (simp_tac (simpset() addsimps bin_add_simps) 1);
   136 by (simp_tac (simpset() addsimps bin_add_simps) 1);
   137 by (rtac allI 1);
   138 by (induct_tac "w" 1);
   139 by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
   140 qed_spec_mp "integ_of_add";
   141 
   142 
   143 (*Subtraction*)
   144 Goalw [zdiff_def]
   145      "integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))";
   146 by (simp_tac (simpset() addsimps [integ_of_add, integ_of_minus]) 1);
   147 qed "diff_integ_of_eq";
   148 
   149 val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add];
   150 
   151 Goal "integ_of(bin_mult v w) = integ_of v * integ_of w";
   152 by (induct_tac "v" 1);
   153 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   154 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   155 by (asm_simp_tac
   156     (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
   157 qed "integ_of_mult";
   158 
   159 
   160 (** Simplification rules with integer constants **)
   161 
   162 Goal "#0 + z = z";
   163 by (Simp_tac 1);
   164 qed "zadd_0";
   165 
   166 Goal "z + #0 = z";
   167 by (Simp_tac 1);
   168 qed "zadd_0_right";
   169 
   170 Addsimps [zadd_0, zadd_0_right];
   171 
   172 
   173 (** Converting simple cases of (int n) to numerals **)
   174 
   175 (*int 0 = #0 *)
   176 bind_thm ("int_0", integ_of_Pls RS sym);
   177 
   178 Goal "int (Suc n) = #1 + int n";
   179 by (simp_tac (simpset() addsimps [zadd_int]) 1);
   180 qed "int_Suc";
   181 
   182 val int_simps = [int_0, int_Suc];
   183 
   184 Goal "- (#0) = #0";
   185 by (Simp_tac 1);
   186 qed "zminus_0";
   187 
   188 Addsimps [zminus_0];
   189 
   190 
   191 Goal "#0 - x = -x";
   192 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   193 qed "zdiff0";
   194 
   195 Goal "x - #0 = x";
   196 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   197 qed "zdiff0_right";
   198 
   199 Goal "x - x = #0";
   200 by (simp_tac (simpset() addsimps [zdiff_def]) 1);
   201 qed "zdiff_self";
   202 
   203 Addsimps [zdiff0, zdiff0_right, zdiff_self];
   204 
   205 Goal "#0 * z = #0";
   206 by (Simp_tac 1);
   207 qed "zmult_0";
   208 
   209 Goal "#1 * z = z";
   210 by (Simp_tac 1);
   211 qed "zmult_1";
   212 
   213 Goal "#2 * z = z+z";
   214 by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1);
   215 qed "zmult_2";
   216 
   217 Goal "z * #0 = #0";
   218 by (Simp_tac 1);
   219 qed "zmult_0_right";
   220 
   221 Goal "z * #1 = z";
   222 by (Simp_tac 1);
   223 qed "zmult_1_right";
   224 
   225 Goal "z * #2 = z+z";
   226 by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1);
   227 qed "zmult_2_right";
   228 
   229 Addsimps [zmult_0, zmult_0_right, 
   230 	  zmult_1, zmult_1_right, 
   231 	  zmult_2, zmult_2_right];
   232 
   233 Goal "(w < z + #1) = (w<z | w=z)";
   234 by (simp_tac (simpset() addsimps [zless_add_int_Suc_eq]) 1);
   235 qed "zless_add1_eq";
   236 
   237 Goal "(w + #1 <= z) = (w<z)";
   238 by (simp_tac (simpset() addsimps [add_int_Suc_zle_eq]) 1);
   239 qed "add1_zle_eq";
   240 Addsimps [add1_zle_eq];
   241 
   242 Goal "neg x = (x < #0)";
   243 by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1); 
   244 qed "neg_eq_less_0"; 
   245 
   246 Goal "(~neg x) = (int 0 <= x)";
   247 by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1); 
   248 qed "not_neg_eq_ge_0"; 
   249 
   250 Goal "#0 <= int m";
   251 by (Simp_tac 1);
   252 qed "zero_zle_int";
   253 AddIffs [zero_zle_int];
   254 
   255 
   256 (** Needed because (int 0) rewrites to #0.
   257     Can these be generalized without evaluating large numbers?**)
   258 
   259 Goal "~ (int k < #0)";
   260 by (Simp_tac 1);
   261 qed "int_less_0_conv";
   262 
   263 Goal "(int k <= #0) = (k=0)";
   264 by (Simp_tac 1);
   265 qed "int_le_0_conv";
   266 
   267 Goal "(int k = #0) = (k=0)";
   268 by (Simp_tac 1);
   269 qed "int_eq_0_conv";
   270 
   271 Goal "(#0 = int k) = (k=0)";
   272 by Auto_tac;
   273 qed "int_eq_0_conv'";
   274 
   275 Addsimps [int_less_0_conv, int_le_0_conv, int_eq_0_conv, int_eq_0_conv'];
   276 
   277 
   278 (** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
   279 
   280 (** Equals (=) **)
   281 
   282 Goalw [iszero_def]
   283   "(integ_of x = integ_of y) = iszero(integ_of (bin_add x (bin_minus y)))"; 
   284 by (simp_tac (simpset() addsimps
   285               (zcompare_rls @ [integ_of_add, integ_of_minus])) 1); 
   286 qed "eq_integ_of_eq"; 
   287 
   288 Goalw [iszero_def] "iszero (integ_of Pls)"; 
   289 by (Simp_tac 1); 
   290 qed "iszero_integ_of_Pls"; 
   291 
   292 Goalw [iszero_def] "~ iszero(integ_of Min)"; 
   293 by (Simp_tac 1);
   294 qed "nonzero_integ_of_Min"; 
   295 
   296 Goalw [iszero_def]
   297      "iszero (integ_of (w BIT x)) = (~x & iszero (integ_of w))"; 
   298 by (Simp_tac 1);
   299 by (int_case_tac "integ_of w" 1); 
   300 by (ALLGOALS (asm_simp_tac 
   301 	      (simpset() addsimps zcompare_rls @ 
   302 				  [zminus_zadd_distrib RS sym, 
   303 				   zadd_int]))); 
   304 qed "iszero_integ_of_BIT"; 
   305 
   306 Goal "iszero (integ_of (w BIT False)) = iszero (integ_of w)"; 
   307 by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); 
   308 qed "iszero_integ_of_0"; 
   309 
   310 Goal "~ iszero (integ_of (w BIT True))"; 
   311 by (simp_tac (HOL_ss addsimps [iszero_integ_of_BIT]) 1); 
   312 qed "iszero_integ_of_1"; 
   313 
   314 
   315 
   316 (** Less-than (<) **)
   317 
   318 Goalw [zless_def,zdiff_def] 
   319     "integ_of x < integ_of y \
   320 \    = neg (integ_of (bin_add x (bin_minus y)))";
   321 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
   322 qed "less_integ_of_eq_neg"; 
   323 
   324 Goal "~ neg (integ_of Pls)"; 
   325 by (Simp_tac 1); 
   326 qed "not_neg_integ_of_Pls"; 
   327 
   328 Goal "neg (integ_of Min)"; 
   329 by (Simp_tac 1);
   330 qed "neg_integ_of_Min"; 
   331 
   332 Goal "neg (integ_of (w BIT x)) = neg (integ_of w)"; 
   333 by (Asm_simp_tac 1); 
   334 by (int_case_tac "integ_of w" 1); 
   335 by (ALLGOALS (asm_simp_tac 
   336 	      (simpset() addsimps [zadd_int, neg_eq_less_nat0, 
   337 				   symmetric zdiff_def] @ zcompare_rls))); 
   338 qed "neg_integ_of_BIT"; 
   339 
   340 
   341 (** Less-than-or-equals (<=) **)
   342 
   343 Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)";
   344 by (simp_tac (simpset() addsimps [zle_def]) 1);
   345 qed "le_integ_of_eq_not_less"; 
   346 
   347 (*Delete the original rewrites, with their clumsy conditional expressions*)
   348 Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT, 
   349           NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
   350 
   351 (*Hide the binary representation of integer constants*)
   352 Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
   353 
   354 (*simplification of arithmetic operations on integer constants*)
   355 val bin_arith_extra_simps =
   356     [integ_of_add RS sym,
   357      integ_of_minus RS sym,
   358      integ_of_mult RS sym,
   359      bin_succ_1, bin_succ_0, 
   360      bin_pred_1, bin_pred_0, 
   361      bin_minus_1, bin_minus_0,  
   362      bin_add_Pls_right, bin_add_BIT_Min,
   363      bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
   364      diff_integ_of_eq, 
   365      bin_mult_1, bin_mult_0, 
   366      NCons_Pls_0, NCons_Pls_1, 
   367      NCons_Min_0, NCons_Min_1, NCons_BIT];
   368 
   369 (*For making a minimal simpset, one must include these default simprules
   370   of Bin.thy.  Also include simp_thms, or at least (~False)=True*)
   371 val bin_arith_simps =
   372     [bin_pred_Pls, bin_pred_Min,
   373      bin_succ_Pls, bin_succ_Min,
   374      bin_add_Pls, bin_add_Min,
   375      bin_minus_Pls, bin_minus_Min,
   376      bin_mult_Pls, bin_mult_Min] @ bin_arith_extra_simps;
   377 
   378 (*Simplification of relational operations*)
   379 val bin_rel_simps =
   380     [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
   381      iszero_integ_of_0, iszero_integ_of_1,
   382      less_integ_of_eq_neg,
   383      not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
   384      le_integ_of_eq_not_less];
   385 
   386 Addsimps bin_arith_extra_simps;
   387 Addsimps bin_rel_simps;
   388 
   389 (*---------------------------------------------------------------------------*)
   390 (* Linear arithmetic                                                         *)
   391 (*---------------------------------------------------------------------------*)
   392 
   393 (*
   394 Instantiation of the generic linear arithmetic package for int.
   395 FIXME: multiplication with constants (eg #2 * i) does not work yet.
   396 Solution: the cancellation simprocs in Int_Cancel should be able to deal with
   397 it (eg simplify #3 * i <= 2 * i to i <= #0) or `add_rules' below should
   398 include rules for turning multiplication with constants into addition.
   399 (The latter option is very inefficient!)
   400 *)
   401 
   402 structure Int_LA_Data(*: LIN_ARITH_DATA*) =
   403 struct
   404 
   405 val lessD = Nat_LA_Data.lessD @ [add1_zle_eq RS iffD2];
   406 
   407 (* borrowed from Bin.thy: *)
   408 fun dest_bit (Const ("False", _)) = 0
   409   | dest_bit (Const ("True", _)) = 1
   410   | dest_bit _ = raise Match;
   411 
   412 fun dest_bin tm =
   413   let
   414     fun bin_of (Const ("Bin.bin.Pls", _)) = []
   415       | bin_of (Const ("Bin.bin.Min", _)) = [~1]
   416       | bin_of (Const ("Bin.bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
   417       | bin_of _ = raise Match;
   418 
   419     fun int_of [] = 0
   420       | int_of (b :: bs) = b + 2 * int_of bs;
   421 
   422   in int_of(bin_of tm) end;
   423 
   424 fun add_atom(t,m,(p,i)) = (case assoc(p,t) of None => ((t,m)::p,i)
   425                            | Some n => (overwrite(p,(t,n+m:int)), i));
   426 
   427 (* Turn term into list of summand * multiplicity plus a constant *)
   428 fun poly(Const("op +",_) $ s $ t, m, pi) = poly(s,m,poly(t,m,pi))
   429   | poly(Const("op -",_) $ s $ t, m, pi) = poly(s,m,poly(t,~1*m,pi))
   430   | poly(Const("uminus",_) $ t, m, pi) =   poly(t,~1*m,pi)
   431   | poly(all as Const("op *",_) $ (Const("Bin.integ_of",_)$c) $ t, m, pi) =
   432       (poly(t,m*dest_bin c,pi) handle Match => add_atom(all,m,pi))
   433   | poly(all as Const("Bin.integ_of",_)$t,m,(p,i)) =
   434      ((p,i + m*dest_bin t) handle Match => add_atom(all,m,(p,i)))
   435   | poly x  = add_atom x;
   436 
   437 fun decomp2(rel,lhs,rhs) =
   438   let val (p,i) = poly(lhs,1,([],0)) and (q,j) = poly(rhs,1,([],0))
   439   in case rel of
   440        "op <"  => Some(p,i,"<",q,j)
   441      | "op <=" => Some(p,i,"<=",q,j)
   442      | "op ="  => Some(p,i,"=",q,j)
   443      | _       => None
   444   end;
   445 
   446 val intT = Type("IntDef.int",[]);
   447 fun iib T = T = ([intT,intT] ---> HOLogic.boolT);
   448 
   449 fun decomp1(T,xxx) =
   450   if iib T then decomp2 xxx else Nat_LA_Data.decomp1(T,xxx);
   451 
   452 fun decomp(_$(Const(rel,T)$lhs$rhs)) = decomp1(T,(rel,lhs,rhs))
   453   | decomp(_$(Const("Not",_)$(Const(rel,T)$lhs$rhs))) =
   454       Nat_LA_Data.negate(decomp1(T,(rel,lhs,rhs)))
   455   | decomp _ = None
   456 
   457 (* reduce contradictory <= to False *)
   458 val add_rules = simp_thms@bin_arith_simps@bin_rel_simps@[int_0];
   459 
   460 val cancel_sums_ss = Nat_LA_Data.cancel_sums_ss addsimps add_rules
   461           addsimprocs [Int_Cancel.sum_conv, Int_Cancel.rel_conv];
   462 
   463 val simp = simplify cancel_sums_ss;
   464 
   465 val add_mono_thms = Nat_LA_Data.add_mono_thms @
   466   map (fn s => prove_goal Int.thy s
   467                  (fn prems => [cut_facts_tac prems 1,
   468                       asm_simp_tac (simpset() addsimps [zadd_zle_mono]) 1]))
   469     ["(i <= j) & (k <= l) ==> i + k <= j + (l::int)",
   470      "(i  = j) & (k <= l) ==> i + k <= j + (l::int)",
   471      "(i <= j) & (k  = l) ==> i + k <= j + (l::int)",
   472      "(i  = j) & (k  = l) ==> i + k  = j + (l::int)"
   473     ];
   474 
   475 end;
   476 
   477 (* Update parameters of arithmetic prover *)
   478 LA_Data_Ref.add_mono_thms := Int_LA_Data.add_mono_thms;
   479 LA_Data_Ref.lessD :=         Int_LA_Data.lessD;
   480 LA_Data_Ref.decomp :=        Int_LA_Data.decomp;
   481 LA_Data_Ref.simp :=          Int_LA_Data.simp;
   482 
   483 
   484 val int_arith_simproc_pats =
   485   map (fn s => Thm.read_cterm (sign_of Int.thy) (s, HOLogic.boolT))
   486       ["(m::int) < n","(m::int) <= n", "(m::int) = n"];
   487 
   488 val fast_int_arith_simproc = mk_simproc "fast_int_arith" int_arith_simproc_pats
   489                                         Fast_Arith.lin_arith_prover;
   490 
   491 Addsimprocs [fast_int_arith_simproc];
   492 
   493 (* FIXME: K true should be replaced by a sensible test to speed things up
   494    in case there are lots of irrelevant terms involved.
   495 
   496 val arith_tac =
   497   refute_tac (K true) (REPEAT o split_tac[nat_diff_split])
   498              ((REPEAT_DETERM o etac linorder_neqE) THEN' fast_arith_tac);
   499 *)
   500 
   501 (* Some test data
   502 Goal "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d";
   503 by(fast_arith_tac 1);
   504 Goal "!!a::int. [| a < b; c < d |] ==> a-d+ #2 <= b+(-c)";
   505 by(fast_arith_tac 1);
   506 Goal "!!a::int. [| a < b; c < d |] ==> a+c+ #1 < b+d";
   507 by(fast_arith_tac 1);
   508 Goal "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c";
   509 by(fast_arith_tac 1);
   510 Goal "!!a::int. [| a+b <= i+j; a<=b; i<=j |] \
   511 \     ==> a+a <= j+j";
   512 by(fast_arith_tac 1);
   513 Goal "!!a::int. [| a+b < i+j; a<b; i<j |] \
   514 \     ==> a+a - - #-1 < j+j - #3";
   515 by(fast_arith_tac 1);
   516 Goal "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k";
   517 by(arith_tac 1);
   518 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   519 \     ==> a <= l";
   520 by(fast_arith_tac 1);
   521 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   522 \     ==> a+a+a+a <= l+l+l+l";
   523 by(fast_arith_tac 1);
   524 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   525 \     ==> a+a+a+a+a <= l+l+l+l+i";
   526 by(fast_arith_tac 1);
   527 Goal "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \
   528 \     ==> a+a+a+a+a+a <= l+l+l+l+i+l";
   529 by(fast_arith_tac 1);
   530 *)
   531 
   532 (*---------------------------------------------------------------------------*)
   533 (* End of linear arithmetic                                                  *)
   534 (*---------------------------------------------------------------------------*)
   535 
   536 (** Simplification of arithmetic when nested to the right **)
   537 
   538 Goal "integ_of v + (integ_of w + z) = integ_of(bin_add v w) + z";
   539 by (simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
   540 qed "add_integ_of_left";
   541 
   542 Goal "integ_of v * (integ_of w * z) = integ_of(bin_mult v w) * z";
   543 by (simp_tac (simpset() addsimps [zmult_assoc RS sym]) 1);
   544 qed "mult_integ_of_left";
   545 
   546 Addsimps [add_integ_of_left, mult_integ_of_left];
   547 
   548 (** Simplification of inequalities involving numerical constants **)
   549 
   550 Goal "(w <= z + #1) = (w<=z | w = z + #1)";
   551 by(arith_tac 1);
   552 qed "zle_add1_eq";
   553 
   554 Goal "(w <= z - #1) = (w<z)";
   555 by(arith_tac 1);
   556 qed "zle_diff1_eq";
   557 Addsimps [zle_diff1_eq];
   558 
   559 (*2nd premise can be proved automatically if v is a literal*)
   560 Goal "[| w <= z; #0 <= v |] ==> w <= z + v";
   561 by(fast_arith_tac 1);
   562 qed "zle_imp_zle_zadd";
   563 
   564 Goal "w <= z ==> w <= z + #1";
   565 by(fast_arith_tac 1);
   566 qed "zle_imp_zle_zadd1";
   567 
   568 (*2nd premise can be proved automatically if v is a literal*)
   569 Goal "[| w < z; #0 <= v |] ==> w < z + v";
   570 by(fast_arith_tac 1);
   571 qed "zless_imp_zless_zadd";
   572 
   573 Goal "w < z ==> w < z + #1";
   574 by(fast_arith_tac 1);
   575 qed "zless_imp_zless_zadd1";
   576 
   577 Goal "(w < z + #1) = (w<=z)";
   578 by(arith_tac 1);
   579 qed "zle_add1_eq_le";
   580 Addsimps [zle_add1_eq_le];
   581 
   582 Goal "(z = z + w) = (w = #0)";
   583 by(arith_tac 1);
   584 qed "zadd_left_cancel0";
   585 Addsimps [zadd_left_cancel0];
   586 
   587 (*LOOPS as a simprule!*)
   588 Goal "[| w + v < z; #0 <= v |] ==> w < z";
   589 by(fast_arith_tac 1);
   590 qed "zless_zadd_imp_zless";
   591 
   592 (*LOOPS as a simprule!  Analogous to Suc_lessD*)
   593 Goal "w + #1 < z ==> w < z";
   594 by(fast_arith_tac 1);
   595 qed "zless_zadd1_imp_zless";
   596 
   597 Goal "w + #-1 = w - #1";
   598 by (Simp_tac 1);
   599 qed "zplus_minus1_conv";
   600 
   601 
   602 (*** nat ***)
   603 
   604 Goal "#0 <= z ==> int (nat z) = z"; 
   605 by (asm_full_simp_tac
   606     (simpset() addsimps [neg_eq_less_0, zle_def, not_neg_nat]) 1); 
   607 qed "nat_0_le"; 
   608 
   609 Goal "z < #0 ==> nat z = 0"; 
   610 by (asm_full_simp_tac
   611     (simpset() addsimps [neg_eq_less_0, zle_def, neg_nat]) 1); 
   612 qed "nat_less_0"; 
   613 
   614 Addsimps [nat_0_le, nat_less_0];
   615 
   616 Goal "#0 <= w ==> (nat w = m) = (w = int m)";
   617 by Auto_tac;
   618 qed "nat_eq_iff";
   619 
   620 Goal "#0 <= w ==> (nat w < m) = (w < int m)";
   621 by (rtac iffI 1);
   622 by (asm_full_simp_tac 
   623     (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
   624 by (etac (nat_0_le RS subst) 1);
   625 by (Simp_tac 1);
   626 qed "nat_less_iff";
   627 
   628 
   629 (*Users don't want to see (int 0) or w + - z*)
   630 Addsimps [int_0, symmetric zdiff_def];
   631 
   632 Goal "#0 <= w ==> (nat w < nat z) = (w<z)";
   633 by (case_tac "neg z" 1);
   634 by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
   635 by (auto_tac (claset() addIs [zless_trans], 
   636 	      simpset() addsimps [neg_eq_less_0, zle_def]));
   637 qed "nat_less_eq_zless";
   638