1.1 --- a/src/HOL/Integ/NatSimprocs.thy	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/Integ/NatSimprocs.thy	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -31,8 +31,10 @@
     1.4  lemma Suc_diff_number_of:
     1.5       "neg (number_of (bin_minus v)::int) ==>  
     1.6        Suc m - (number_of v) = m - (number_of (bin_pred v))"
     1.7 -apply (subst Suc_diff_eq_diff_pred, simp, simp)
     1.8 -apply (force simp only: diff_nat_number_of less_0_number_of [symmetric] 
     1.9 +apply (subst Suc_diff_eq_diff_pred)
    1.10 +apply (simp add: ); 
    1.11 +apply (simp del: nat_numeral_1_eq_1); 
    1.12 +apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] 
    1.13                          neg_number_of_bin_pred_iff_0)
    1.14  done
    1.15  
    1.16 @@ -54,7 +56,8 @@
    1.17           if neg pv then nat_case a f n else f (nat pv + n))"
    1.18  apply (subst add_eq_if)
    1.19  apply (simp split add: nat.split
    1.20 -            add: numeral_1_eq_Suc_0 [symmetric] Let_def 
    1.21 +            del: nat_numeral_1_eq_1
    1.22 +	    add: numeral_1_eq_Suc_0 [symmetric] Let_def 
    1.23                   neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
    1.24  done
    1.25  
    1.26 @@ -74,6 +77,7 @@
    1.27                     else f (nat pv + n) (nat_rec a f (nat pv + n)))"
    1.28  apply (subst add_eq_if)
    1.29  apply (simp split add: nat.split
    1.30 +            del: nat_numeral_1_eq_1
    1.31              add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
    1.32                   neg_number_of_bin_pred_iff_0)
    1.33  done
    1.34 @@ -106,8 +110,6 @@
    1.35  lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
    1.36  by simp
    1.37  
    1.38 -declare numeral_0_eq_0 [simp] numeral_1_eq_1 [simp] 
    1.39 -
    1.40  text{*Can be used to eliminate long strings of Sucs, but not by default*}
    1.41  lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
    1.42  by simp
    1.43 @@ -194,4 +196,20 @@
    1.44  declare divide_eq_eq [of _ "number_of w", standard, simp]
    1.45  
    1.46  
    1.47 +subsubsection{*Division By @{term "-1"}*}
    1.48 +
    1.49 +lemma divide_minus1 [simp]:
    1.50 +     "x/-1 = -(x::'a::{field,division_by_zero,number_ring})" 
    1.51 +by simp
    1.52 +
    1.53 +lemma minus1_divide [simp]:
    1.54 +     "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
    1.55 +by (simp add: divide_inverse_zero inverse_minus_eq)
    1.56 +
    1.57 +ML
    1.58 +{*
    1.59 +val divide_minus1 = thm "divide_minus1";
    1.60 +val minus1_divide = thm "minus1_divide";
    1.61 +*}
    1.62 +
    1.63  end