equal
deleted
inserted
replaced
855 |
855 |
856 lemma abs_power_minus_one [simp]: |
856 lemma abs_power_minus_one [simp]: |
857 "abs(-1 ^ n) = (1::'a::linordered_idom)" |
857 "abs(-1 ^ n) = (1::'a::linordered_idom)" |
858 by (simp add: power_abs) |
858 by (simp add: power_abs) |
859 |
859 |
860 text{*Lemmas for specialist use, NOT as default simprules*} |
|
861 (* TODO: see if semiring duplication can be removed without breaking proofs *) |
|
862 lemma mult_2: "2 * z = (z+z::'a::semiring_1)" |
|
863 unfolding one_add_one [symmetric] left_distrib by simp |
|
864 |
|
865 lemma mult_2_right: "z * 2 = (z+z::'a::semiring_1)" |
|
866 unfolding one_add_one [symmetric] right_distrib by simp |
|
867 |
|
868 |
860 |
869 subsection{*More Inequality Reasoning*} |
861 subsection{*More Inequality Reasoning*} |
870 |
862 |
871 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)" |
863 lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)" |
872 by arith |
864 by arith |