equal
deleted
inserted
replaced
530 by (ALLGOALS Asm_simp_tac); |
530 by (ALLGOALS Asm_simp_tac); |
531 by (nat_ind_tac "x" [] 1); |
531 by (nat_ind_tac "x" [] 1); |
532 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); |
532 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); |
533 qed "mult_lt_mono2"; |
533 qed "mult_lt_mono2"; |
534 |
534 |
|
535 goal thy "!!k. [| i<j; 0<k; i:nat; j:nat; k:nat |] ==> i#*k < j#*k"; |
|
536 by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1); |
|
537 qed "mult_lt_mono1"; |
|
538 |
535 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n"; |
539 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n"; |
536 by (best_tac (claset() addEs [natE] addss (simpset())) 1); |
540 by (best_tac (claset() addEs [natE] addss (simpset())) 1); |
537 qed "zero_lt_mult_iff"; |
541 qed "zero_lt_mult_iff"; |
538 |
542 |
539 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1"; |
543 goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1"; |