changeset 14436 | 77017c49c004 |
parent 14390 | 55fe71faadda |
child 14473 | 846c237bd9b3 |
--- a/src/HOL/Integ/IntArith.thy Fri Mar 05 15:18:59 2004 +0100 +++ b/src/HOL/Integ/IntArith.thy Fri Mar 05 15:19:55 2004 +0100 @@ -140,6 +140,10 @@ lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_ring,number_ring})" by (simp add: abs_if) +lemma abs_power_minus_one [simp]: + "abs(-1 ^ n) = (1::'a::{ordered_ring,number_ring,ringpower})" +by (simp add: power_abs) + lemma of_int_number_of_eq: "of_int (number_of v) = (number_of v :: 'a :: number_ring)" apply (induct v)