equal
deleted
inserted
replaced
528 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono]))); |
528 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono]))); |
529 qed "mult_le_mono1"; |
529 qed "mult_le_mono1"; |
530 |
530 |
531 (*<=monotonicity, BOTH arguments*) |
531 (*<=monotonicity, BOTH arguments*) |
532 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l"; |
532 goal Arith.thy "!!i::nat. [| i<=j; k<=l |] ==> i*k<=j*l"; |
|
533 by (etac (mult_le_mono1 RS le_trans) 1); |
533 by (rtac le_trans 1); |
534 by (rtac le_trans 1); |
534 by (ALLGOALS |
535 by (stac mult_commute 2); |
535 (deepen_tac (!claset addIs [mult_commute RS ssubst, mult_le_mono1]) 0)); |
536 by (etac mult_le_mono1 2); |
|
537 by (simp_tac (!simpset addsimps [mult_commute]) 1); |
536 qed "mult_le_mono"; |
538 qed "mult_le_mono"; |
537 |
539 |
538 (*strict, in 1st argument; proof is by induction on k>0*) |
540 (*strict, in 1st argument; proof is by induction on k>0*) |
539 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
541 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j"; |
540 be zero_less_natE 1; |
542 be zero_less_natE 1; |