equal
deleted
inserted
replaced
487 qed "Ord_lt_mono_imp_le_mono"; |
487 qed "Ord_lt_mono_imp_le_mono"; |
488 |
488 |
489 (*le monotonicity, 1st argument*) |
489 (*le monotonicity, 1st argument*) |
490 goal Arith.thy |
490 goal Arith.thy |
491 "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; |
491 "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k"; |
492 by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1); |
492 by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1); |
493 by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); |
493 by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1)); |
494 qed "add_le_mono1"; |
494 qed "add_le_mono1"; |
495 |
495 |
496 (* le monotonicity, BOTH arguments*) |
496 (* le monotonicity, BOTH arguments*) |
497 goal Arith.thy |
497 goal Arith.thy |