1.1 --- a/src/HOL/Arith.ML	Wed Oct 27 11:15:35 1999 +0200
     1.2 +++ b/src/HOL/Arith.ML	Wed Oct 27 12:50:48 1999 +0200
     1.3 @@ -132,13 +132,6 @@
     1.4  qed "add_gr_0";
     1.5  AddIffs [add_gr_0];
     1.6  
     1.7 -(* FIXME: really needed?? *)
     1.8 -Goal "((m+n)-1 = 0) = (m=0 & n-1 = 0 | m-1 = 0 & n=0)";
     1.9 -by (exhaust_tac "m" 1);
    1.10 -by (ALLGOALS (fast_tac (claset() addss (simpset()))));
    1.11 -qed "pred_add_is_0";
    1.12 -(*Addsimps [pred_add_is_0];*)
    1.13 -
    1.14  (* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
    1.15  Goal "0<n ==> m + (n-1) = (m+n)-1";
    1.16  by (exhaust_tac "m" 1);
    1.17 @@ -1013,14 +1006,16 @@
    1.18  simpset_ref () := (simpset() addSolver
    1.19     (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac));
    1.20  
    1.21 -(* Elimination of `-' on nat due to John Harrison *)
    1.22 -Goal "P(a - b::nat) = (!d. (b = a + d --> P 0) & (a = b + d --> P d))";
    1.23 +(*Elimination of `-' on nat due to John Harrison.  An alternative is to
    1.24 +  replace b=a+d by a<b; not clear that it makes much difference. *)
    1.25 +Goal "P(a - b::nat) = (ALL d. (b = a + d --> P 0) & (a = b + d --> P d))";
    1.26  by (case_tac "a <= b" 1);
    1.27  by Auto_tac;
    1.28  by (eres_inst_tac [("x","b-a")] allE 1);
    1.29  by (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]) 1);
    1.30  qed "nat_diff_split";
    1.31  
    1.32 +
    1.33  (* FIXME: K true should be replaced by a sensible test to speed things up
    1.34     in case there are lots of irrelevant terms involved;
    1.35     elimination of min/max can be optimized:
    1.36 @@ -1120,38 +1115,24 @@
    1.37  
    1.38  (*** Reducting subtraction to addition ***)
    1.39  
    1.40 -(*Intended for use with linear arithmetic, but useful in its own right*)
    1.41 -Goal "P (x-y) = (ALL z. (x<y --> P 0) & (x = y+z --> P z))";
    1.42 -by (case_tac "x<y" 1);
    1.43 -by (auto_tac (claset(),  simpset() addsimps [diff_is_0_eq RS iffD2]));
    1.44 -qed "split_diff";
    1.45 -
    1.46 -val remove_diff_ss = 
    1.47 -    simpset()
    1.48 -      delsimps ex_simps@all_simps
    1.49 -      addsimps [le_diff_conv2, le_diff_conv, le_imp_diff_is_add, 
    1.50 -		diff_diff_right] 
    1.51 -      addcongs [conj_cong]
    1.52 -      addsplits [split_diff];
    1.53 -
    1.54  Goal "n<=(l::nat) --> Suc l - n + m = Suc (l - n + m)";
    1.55 -by (simp_tac remove_diff_ss 1);
    1.56 +by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.57  qed_spec_mp "Suc_diff_add_le";
    1.58  
    1.59  Goal "i<n ==> n - Suc i < n - i";
    1.60 -by (asm_simp_tac remove_diff_ss 1);
    1.61 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.62  qed "diff_Suc_less_diff";
    1.63  
    1.64  Goal "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.65 -by (simp_tac remove_diff_ss 1);
    1.66 +by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.67  qed "if_Suc_diff_le";
    1.68  
    1.69  Goal "Suc(m)-n <= Suc(m-n)";
    1.70 -by (simp_tac remove_diff_ss 1);
    1.71 +by (simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.72  qed "diff_Suc_le_Suc_diff";
    1.73  
    1.74  Goal "[| k<=n; n<=m |] ==> (m-k) - (n-k) = m-(n::nat)";
    1.75 -by (asm_simp_tac remove_diff_ss 1);
    1.76 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.77  qed "diff_right_cancel";
    1.78  
    1.79  
    1.80 @@ -1159,18 +1140,17 @@
    1.81  
    1.82  (* Monotonicity of subtraction in first argument *)
    1.83  Goal "m <= (n::nat) ==> (m-l) <= (n-l)";
    1.84 -by (asm_simp_tac remove_diff_ss 1);
    1.85 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.86  qed "diff_le_mono";
    1.87  
    1.88  Goal "m <= (n::nat) ==> (l-n) <= (l-m)";
    1.89 -by (asm_simp_tac remove_diff_ss 1);
    1.90 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.91  qed "diff_le_mono2";
    1.92  
    1.93 -(*This proof requires natdiff_cancel_sums*)
    1.94  Goal "[| m < (n::nat); m<l |] ==> (l-n) < (l-m)";
    1.95 -by (asm_simp_tac remove_diff_ss 1);
    1.96 +by (asm_simp_tac (simpset() addsplits [nat_diff_split]) 1);
    1.97  qed "diff_less_mono2";
    1.98  
    1.99  Goal "[| m-n = 0; n-m = 0 |] ==>  m=n";
   1.100 -by (asm_full_simp_tac remove_diff_ss 1);
   1.101 +by (asm_full_simp_tac (simpset() addsplits [nat_diff_split]) 1);
   1.102  qed "diffs0_imp_equal";