equal
deleted
inserted
replaced
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); |