equal
deleted
inserted
replaced
455 finally show ?thesis . |
455 finally show ?thesis . |
456 qed |
456 qed |
457 |
457 |
458 lemma odd_less_0: |
458 lemma odd_less_0: |
459 "(1 + z + z < 0) = (z < (0::int))"; |
459 "(1 + z + z < 0) = (z < (0::int))"; |
460 proof (cases z rule: int_cases) |
460 proof (cases z rule: int_cases') |
461 case (nonneg n) |
461 case (nonneg n) |
462 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
462 thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing |
463 le_imp_0_less [THEN order_less_imp_le]) |
463 le_imp_0_less [THEN order_less_imp_le]) |
464 next |
464 next |
465 case (neg n) |
465 case (neg n) |
466 thus ?thesis by (simp del: int_Suc |
466 thus ?thesis by (simp del: of_nat_Suc of_nat_add |
467 add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls) |
467 add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric]) |
468 qed |
468 qed |
469 |
469 |
470 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} |
470 text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *} |
471 |
471 |
472 lemma Ints_odd_less_0: |
472 lemma Ints_odd_less_0: |