equal
deleted
inserted
replaced
124 also have "... = - of_int 1" by (simp only: of_int_minus) |
124 also have "... = - of_int 1" by (simp only: of_int_minus) |
125 also have "... = -1" by simp |
125 also have "... = -1" by simp |
126 finally show ?thesis . |
126 finally show ?thesis . |
127 qed |
127 qed |
128 |
128 |
129 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_ring,number_ring})" |
129 lemma abs_minus_one [simp]: "abs (-1) = (1::'a::{ordered_idom,number_ring})" |
130 by (simp add: abs_if) |
130 by (simp add: abs_if) |
131 |
131 |
132 lemma abs_power_minus_one [simp]: |
132 lemma abs_power_minus_one [simp]: |
133 "abs(-1 ^ n) = (1::'a::{ordered_ring,number_ring,ringpower})" |
133 "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,ringpower})" |
134 by (simp add: power_abs) |
134 by (simp add: power_abs) |
135 |
135 |
136 lemma of_int_number_of_eq: |
136 lemma of_int_number_of_eq: |
137 "of_int (number_of v) = (number_of v :: 'a :: number_ring)" |
137 "of_int (number_of v) = (number_of v :: 'a :: number_ring)" |
138 apply (induct v) |
138 apply (induct v) |