src/HOL/Arith.ML
changeset 4389 1865cb8df116
parent 4378 e52f864c5b88
child 4423 a129b817b58a
equal deleted inserted replaced
4388:c54f2e3423f2 4389:1865cb8df116
   542 Addsimps [mult_eq_1_iff];
   542 Addsimps [mult_eq_1_iff];
   543 
   543 
   544 goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
   544 goal Arith.thy "!!k. 0<k ==> (m*k < n*k) = (m<n)";
   545 by (safe_tac (claset() addSIs [mult_less_mono1]));
   545 by (safe_tac (claset() addSIs [mult_less_mono1]));
   546 by (cut_facts_tac [less_linear] 1);
   546 by (cut_facts_tac [less_linear] 1);
   547 by (blast_tac (claset() addDs [mult_less_mono1] addEs [less_asym]) 1);
   547 by (blast_tac (claset() addIs [mult_less_mono1] addEs [less_asym]) 1);
   548 qed "mult_less_cancel2";
   548 qed "mult_less_cancel2";
   549 
   549 
   550 goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
   550 goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
   551 by (dtac mult_less_cancel2 1);
   551 by (dtac mult_less_cancel2 1);
   552 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);
   552 by (asm_full_simp_tac (simpset() addsimps [mult_commute]) 1);