tidied a proof using new lemmas for signs of products
authorpaulson
Wed Jun 14 17:46:10 2000 +0200 (2000-06-14)
changeset 9064eacebbcafe57
parent 9063 0d7628966069
child 9065 15f82c9aa331
tidied a proof using new lemmas for signs of products
src/HOL/Integ/NatBin.ML
     1.1 --- a/src/HOL/Integ/NatBin.ML	Wed Jun 14 17:45:01 2000 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.ML	Wed Jun 14 17:46:10 2000 +0200
     1.3 @@ -126,14 +126,10 @@
     1.4  
     1.5  Goal "(#0::int) <= z ==> nat (z*z') = nat z * nat z'";
     1.6  by (case_tac "#0 <= z'" 1);
     1.7 -by (subgoal_tac "z'*z <= #0" 2);
     1.8 -by (rtac (neg_imp_zmult_nonpos_iff RS iffD2) 3);
     1.9 -by (auto_tac (claset(),
    1.10 -	      simpset() addsimps [zmult_commute]));
    1.11 -by (subgoal_tac "#0 <= z*z'" 1);
    1.12 -by (force_tac (claset() addDs [zmult_zle_mono1], simpset()) 2);
    1.13 +by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
    1.14  by (rtac (inj_int RS injD) 1);
    1.15 -by (asm_simp_tac (simpset() addsimps [zmult_int RS sym]) 1);
    1.16 +by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
    1.17 +				      int_0_le_mult_iff]) 1);
    1.18  qed "nat_mult_distrib";
    1.19  
    1.20  Goal "(number_of v :: nat) * number_of v' = \