src/HOL/Nat.ML
changeset 9637 47d39a31eb2f
parent 9436 62bb04ab4b01
child 9870 2374ba026fc6
     1.1 --- a/src/HOL/Nat.ML	Thu Aug 17 12:01:09 2000 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Aug 17 12:02:01 2000 +0200
     1.3 @@ -256,14 +256,6 @@
     1.4  qed "add_gr_0";
     1.5  AddIffs [add_gr_0];
     1.6  
     1.7 -(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
     1.8 -Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
     1.9 -by (case_tac "m" 1);
    1.10 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
    1.11 -                                      addsplits [nat.split])));
    1.12 -qed "add_pred";
    1.13 -Addsimps [add_pred];
    1.14 -
    1.15  Goal "!!m::nat. m + n = m ==> n = 0";
    1.16  by (dtac (add_0_right RS ssubst) 1);
    1.17  by (asm_full_simp_tac (simpset() addsimps [add_assoc]
    1.18 @@ -673,54 +665,57 @@
    1.19  qed "mult_eq_1_iff";
    1.20  Addsimps [mult_eq_1_iff];
    1.21  
    1.22 -Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
    1.23 +Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
    1.24  by (safe_tac (claset() addSIs [mult_less_mono1]));
    1.25 -by (cut_facts_tac [less_linear] 1);
    1.26 -by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
    1.27 +by (case_tac "k" 1);
    1.28 +by Auto_tac;  
    1.29 +by (full_simp_tac (simpset() delsimps [le_0_eq]
    1.30 +			     addsimps [linorder_not_le RS sym]) 1);
    1.31 +by (blast_tac (claset() addIs [mult_le_mono1]) 1); 
    1.32  qed "mult_less_cancel2";
    1.33  
    1.34 -Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
    1.35 -by (dtac mult_less_cancel2 1);
    1.36 -by (etac subst 1);
    1.37 -by (simp_tac (simpset() addsimps [mult_commute]) 1);
    1.38 +Goal "!!m::nat. (k*m < k*n) = (0<k & m<n)";
    1.39 +by (simp_tac (simpset() addsimps [mult_less_cancel2, 
    1.40 +                                  inst "m" "k" mult_commute]) 1);
    1.41  qed "mult_less_cancel1";
    1.42  Addsimps [mult_less_cancel1, mult_less_cancel2];
    1.43  
    1.44 -Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
    1.45 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    1.46 +Goal "!!m::nat. (m*k <= n*k) = (0<k --> m<=n)";
    1.47 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    1.48 +by Auto_tac;  
    1.49  qed "mult_le_cancel2";
    1.50  
    1.51 -Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
    1.52 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    1.53 +Goal "!!m::nat. (k*m <= k*n) = (0<k --> m<=n)";
    1.54 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    1.55 +by Auto_tac;  
    1.56  qed "mult_le_cancel1";
    1.57  Addsimps [mult_le_cancel1, mult_le_cancel2];
    1.58  
    1.59 -Goal "(Suc k * m < Suc k * n) = (m < n)";
    1.60 -by (rtac mult_less_cancel1 1);
    1.61 -by (Simp_tac 1);
    1.62 -qed "Suc_mult_less_cancel1";
    1.63 -
    1.64 -Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
    1.65 -by (simp_tac (simpset_of HOL.thy) 1);
    1.66 -by (rtac Suc_mult_less_cancel1 1);
    1.67 -qed "Suc_mult_le_cancel1";
    1.68 -
    1.69 -Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
    1.70 +Goal "(m*k = n*k) = (m=n | (k = (0::nat)))";
    1.71  by (cut_facts_tac [less_linear] 1);
    1.72  by Safe_tac;
    1.73 -by (assume_tac 2);
    1.74 +by Auto_tac; 	
    1.75  by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
    1.76  by (ALLGOALS Asm_full_simp_tac);
    1.77  qed "mult_cancel2";
    1.78  
    1.79 -Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
    1.80 -by (dtac mult_cancel2 1);
    1.81 -by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
    1.82 +Goal "(k*m = k*n) = (m=n | (k = (0::nat)))";
    1.83 +by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
    1.84  qed "mult_cancel1";
    1.85  Addsimps [mult_cancel1, mult_cancel2];
    1.86  
    1.87 +Goal "(Suc k * m < Suc k * n) = (m < n)";
    1.88 +by (stac mult_less_cancel1 1);
    1.89 +by (Simp_tac 1);
    1.90 +qed "Suc_mult_less_cancel1";
    1.91 +
    1.92 +Goal "(Suc k * m <= Suc k * n) = (m <= n)";
    1.93 +by (stac mult_le_cancel1 1);
    1.94 +by (Simp_tac 1);
    1.95 +qed "Suc_mult_le_cancel1";
    1.96 +
    1.97  Goal "(Suc k * m = Suc k * n) = (m = n)";
    1.98 -by (rtac mult_cancel1 1);
    1.99 +by (stac mult_cancel1 1);
   1.100  by (Simp_tac 1);
   1.101  qed "Suc_mult_cancel1";
   1.102