better rules for cancellation of common factors across comparisons
authorpaulson
Thu Aug 17 12:02:01 2000 +0200 (2000-08-17)
changeset 963747d39a31eb2f
parent 9636 a0d4d9de9893
child 9638 1f62547edc0e
better rules for cancellation of common factors across comparisons
src/HOL/Divides.ML
src/HOL/Nat.ML
src/HOL/Power.ML
     1.1 --- a/src/HOL/Divides.ML	Thu Aug 17 12:01:09 2000 +0200
     1.2 +++ b/src/HOL/Divides.ML	Thu Aug 17 12:02:01 2000 +0200
     1.3 @@ -424,7 +424,6 @@
     1.4  Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
     1.5  by (etac exE 1);
     1.6  by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
     1.7 -by (Blast_tac 1);
     1.8  qed "dvd_mult_cancel";
     1.9  
    1.10  Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";
     2.1 --- a/src/HOL/Nat.ML	Thu Aug 17 12:01:09 2000 +0200
     2.2 +++ b/src/HOL/Nat.ML	Thu Aug 17 12:02:01 2000 +0200
     2.3 @@ -256,14 +256,6 @@
     2.4  qed "add_gr_0";
     2.5  AddIffs [add_gr_0];
     2.6  
     2.7 -(* Could be generalized, eg to "k<n ==> m+(n-(Suc k)) = (m+n)-(Suc k)" *)
     2.8 -Goal "!!m::nat. 0<n ==> m + (n-1) = (m+n)-1";
     2.9 -by (case_tac "m" 1);
    2.10 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc, Suc_n_not_n]
    2.11 -                                      addsplits [nat.split])));
    2.12 -qed "add_pred";
    2.13 -Addsimps [add_pred];
    2.14 -
    2.15  Goal "!!m::nat. m + n = m ==> n = 0";
    2.16  by (dtac (add_0_right RS ssubst) 1);
    2.17  by (asm_full_simp_tac (simpset() addsimps [add_assoc]
    2.18 @@ -673,54 +665,57 @@
    2.19  qed "mult_eq_1_iff";
    2.20  Addsimps [mult_eq_1_iff];
    2.21  
    2.22 -Goal "!!m::nat. 0<k ==> (m*k < n*k) = (m<n)";
    2.23 +Goal "!!m::nat. (m*k < n*k) = (0<k & m<n)";
    2.24  by (safe_tac (claset() addSIs [mult_less_mono1]));
    2.25 -by (cut_facts_tac [less_linear] 1);
    2.26 -by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
    2.27 +by (case_tac "k" 1);
    2.28 +by Auto_tac;  
    2.29 +by (full_simp_tac (simpset() delsimps [le_0_eq]
    2.30 +			     addsimps [linorder_not_le RS sym]) 1);
    2.31 +by (blast_tac (claset() addIs [mult_le_mono1]) 1); 
    2.32  qed "mult_less_cancel2";
    2.33  
    2.34 -Goal "!!m::nat. 0<k ==> (k*m < k*n) = (m<n)";
    2.35 -by (dtac mult_less_cancel2 1);
    2.36 -by (etac subst 1);
    2.37 -by (simp_tac (simpset() addsimps [mult_commute]) 1);
    2.38 +Goal "!!m::nat. (k*m < k*n) = (0<k & m<n)";
    2.39 +by (simp_tac (simpset() addsimps [mult_less_cancel2, 
    2.40 +                                  inst "m" "k" mult_commute]) 1);
    2.41  qed "mult_less_cancel1";
    2.42  Addsimps [mult_less_cancel1, mult_less_cancel2];
    2.43  
    2.44 -Goal "!!m::nat. 0<k ==> (m*k <= n*k) = (m<=n)";
    2.45 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    2.46 +Goal "!!m::nat. (m*k <= n*k) = (0<k --> m<=n)";
    2.47 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    2.48 +by Auto_tac;  
    2.49  qed "mult_le_cancel2";
    2.50  
    2.51 -Goal "!!m::nat. 0<k ==> (k*m <= k*n) = (m<=n)";
    2.52 -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    2.53 +Goal "!!m::nat. (k*m <= k*n) = (0<k --> m<=n)";
    2.54 +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1);
    2.55 +by Auto_tac;  
    2.56  qed "mult_le_cancel1";
    2.57  Addsimps [mult_le_cancel1, mult_le_cancel2];
    2.58  
    2.59 -Goal "(Suc k * m < Suc k * n) = (m < n)";
    2.60 -by (rtac mult_less_cancel1 1);
    2.61 -by (Simp_tac 1);
    2.62 -qed "Suc_mult_less_cancel1";
    2.63 -
    2.64 -Goalw [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
    2.65 -by (simp_tac (simpset_of HOL.thy) 1);
    2.66 -by (rtac Suc_mult_less_cancel1 1);
    2.67 -qed "Suc_mult_le_cancel1";
    2.68 -
    2.69 -Goal "0 < (k::nat) ==> (m*k = n*k) = (m=n)";
    2.70 +Goal "(m*k = n*k) = (m=n | (k = (0::nat)))";
    2.71  by (cut_facts_tac [less_linear] 1);
    2.72  by Safe_tac;
    2.73 -by (assume_tac 2);
    2.74 +by Auto_tac; 	
    2.75  by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
    2.76  by (ALLGOALS Asm_full_simp_tac);
    2.77  qed "mult_cancel2";
    2.78  
    2.79 -Goal "0 < (k::nat) ==> (k*m = k*n) = (m=n)";
    2.80 -by (dtac mult_cancel2 1);
    2.81 -by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
    2.82 +Goal "(k*m = k*n) = (m=n | (k = (0::nat)))";
    2.83 +by (simp_tac (simpset() addsimps [mult_cancel2, inst "m" "k" mult_commute]) 1);
    2.84  qed "mult_cancel1";
    2.85  Addsimps [mult_cancel1, mult_cancel2];
    2.86  
    2.87 +Goal "(Suc k * m < Suc k * n) = (m < n)";
    2.88 +by (stac mult_less_cancel1 1);
    2.89 +by (Simp_tac 1);
    2.90 +qed "Suc_mult_less_cancel1";
    2.91 +
    2.92 +Goal "(Suc k * m <= Suc k * n) = (m <= n)";
    2.93 +by (stac mult_le_cancel1 1);
    2.94 +by (Simp_tac 1);
    2.95 +qed "Suc_mult_le_cancel1";
    2.96 +
    2.97  Goal "(Suc k * m = Suc k * n) = (m = n)";
    2.98 -by (rtac mult_cancel1 1);
    2.99 +by (stac mult_cancel1 1);
   2.100  by (Simp_tac 1);
   2.101  qed "Suc_mult_cancel1";
   2.102  
     3.1 --- a/src/HOL/Power.ML	Thu Aug 17 12:01:09 2000 +0200
     3.2 +++ b/src/HOL/Power.ML	Thu Aug 17 12:02:01 2000 +0200
     3.3 @@ -34,7 +34,6 @@
     3.4  Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
     3.5  by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
     3.6  by (asm_simp_tac (simpset() addsimps [power_add]) 1);
     3.7 -by (Blast_tac 1);
     3.8  qed "le_imp_power_dvd";
     3.9  
    3.10  Goal "!!i::nat. [| 0 < i; i^m < i^n |] ==> m < n";