src/HOL/Arith.ML
changeset 7622 dcb93b295683
parent 7582 2650c9c2ab7f
child 7945 3aca6352f063
equal deleted inserted replaced
7621:4074bc1e380d 7622:dcb93b295683
   334 Goal "(m*n = 0) = (m=0 | n=0)";
   334 Goal "(m*n = 0) = (m=0 | n=0)";
   335 by (induct_tac "m" 1);
   335 by (induct_tac "m" 1);
   336 by (induct_tac "n" 2);
   336 by (induct_tac "n" 2);
   337 by (ALLGOALS Asm_simp_tac);
   337 by (ALLGOALS Asm_simp_tac);
   338 qed "mult_is_0";
   338 qed "mult_is_0";
   339 Addsimps [mult_is_0];
   339 
       
   340 Goal "(0 = m*n) = (0=m | 0=n)";
       
   341 by (cut_facts_tac [mult_is_0] 1);
       
   342 by (full_simp_tac (simpset() addsimps [eq_commute]) 1);
       
   343 qed "zero_is_mult";
       
   344 
       
   345 Addsimps [mult_is_0, zero_is_mult];
   340 
   346 
   341 Goal "m <= m*(m::nat)";
   347 Goal "m <= m*(m::nat)";
   342 by (induct_tac "m" 1);
   348 by (induct_tac "m" 1);
   343 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
   349 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_assoc RS sym])));
   344 by (etac (le_add2 RSN (2,le_trans)) 1);
   350 by (etac (le_add2 RSN (2,le_trans)) 1);