254 |
254 |
255 text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}. |
255 text{*We cannot refer to the number @{term 2} in @{text Ring_and_Field.thy}. |
256 We cannot prove general results about the numeral @{term "-1"}, so we have to |
256 We cannot prove general results about the numeral @{term "-1"}, so we have to |
257 use @{term "- 1"} instead.*} |
257 use @{term "- 1"} instead.*} |
258 |
258 |
259 lemma power2_eq_square: "(a::'a::{semiring,ringpower})\<twosuperior> = a * a" |
259 lemma power2_eq_square: "(a::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = a * a" |
260 by (simp add: numeral_2_eq_2 Power.power_Suc) |
260 by (simp add: numeral_2_eq_2 Power.power_Suc) |
261 |
261 |
262 lemma [simp]: "(0::'a::{semiring,ringpower})\<twosuperior> = 0" |
262 lemma [simp]: "(0::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 0" |
263 by (simp add: power2_eq_square) |
263 by (simp add: power2_eq_square) |
264 |
264 |
265 lemma [simp]: "(1::'a::{semiring,ringpower})\<twosuperior> = 1" |
265 lemma [simp]: "(1::'a::{comm_semiring_1_cancel,ringpower})\<twosuperior> = 1" |
266 by (simp add: power2_eq_square) |
266 by (simp add: power2_eq_square) |
267 |
267 |
268 text{*Squares of literal numerals will be evaluated.*} |
268 text{*Squares of literal numerals will be evaluated.*} |
269 declare power2_eq_square [of "number_of w", standard, simp] |
269 declare power2_eq_square [of "number_of w", standard, simp] |
270 |
270 |
271 lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_ring,ringpower})" |
271 lemma zero_le_power2 [simp]: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,ringpower})" |
272 by (simp add: power2_eq_square zero_le_square) |
272 by (simp add: power2_eq_square zero_le_square) |
273 |
273 |
274 lemma zero_less_power2 [simp]: |
274 lemma zero_less_power2 [simp]: |
275 "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_ring,ringpower}))" |
275 "(0 < a\<twosuperior>) = (a \<noteq> (0::'a::{ordered_idom,ringpower}))" |
276 by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) |
276 by (force simp add: power2_eq_square zero_less_mult_iff linorder_neq_iff) |
277 |
277 |
278 lemma zero_eq_power2 [simp]: |
278 lemma zero_eq_power2 [simp]: |
279 "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_ring,ringpower}))" |
279 "(a\<twosuperior> = 0) = (a = (0::'a::{ordered_idom,ringpower}))" |
280 by (force simp add: power2_eq_square mult_eq_0_iff) |
280 by (force simp add: power2_eq_square mult_eq_0_iff) |
281 |
281 |
282 lemma abs_power2 [simp]: |
282 lemma abs_power2 [simp]: |
283 "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_ring,ringpower})" |
283 "abs(a\<twosuperior>) = (a\<twosuperior>::'a::{ordered_idom,ringpower})" |
284 by (simp add: power2_eq_square abs_mult abs_mult_self) |
284 by (simp add: power2_eq_square abs_mult abs_mult_self) |
285 |
285 |
286 lemma power2_abs [simp]: |
286 lemma power2_abs [simp]: |
287 "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_ring,ringpower})" |
287 "(abs a)\<twosuperior> = (a\<twosuperior>::'a::{ordered_idom,ringpower})" |
288 by (simp add: power2_eq_square abs_mult_self) |
288 by (simp add: power2_eq_square abs_mult_self) |
289 |
289 |
290 lemma power2_minus [simp]: |
290 lemma power2_minus [simp]: |
291 "(- a)\<twosuperior> = (a\<twosuperior>::'a::{ring,ringpower})" |
291 "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,ringpower})" |
292 by (simp add: power2_eq_square) |
292 by (simp add: power2_eq_square) |
293 |
293 |
294 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{ring,ringpower})" |
294 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,ringpower})" |
295 apply (induct_tac "n") |
295 apply (induct_tac "n") |
296 apply (auto simp add: power_Suc power_add) |
296 apply (auto simp add: power_Suc power_add) |
297 done |
297 done |
298 |
298 |
299 lemma power_even_eq: "(a::'a::ringpower) ^ (2*n) = (a^n)^2" |
299 lemma power_even_eq: "(a::'a::ringpower) ^ (2*n) = (a^n)^2" |
301 |
301 |
302 lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2" |
302 lemma power_odd_eq: "(a::int) ^ Suc(2*n) = a * (a^n)^2" |
303 by (simp add: power_even_eq) |
303 by (simp add: power_even_eq) |
304 |
304 |
305 lemma power_minus_even [simp]: |
305 lemma power_minus_even [simp]: |
306 "(-a) ^ (2*n) = (a::'a::{ring,ringpower}) ^ (2*n)" |
306 "(-a) ^ (2*n) = (a::'a::{comm_ring_1,ringpower}) ^ (2*n)" |
307 by (simp add: power_minus1_even power_minus [of a]) |
307 by (simp add: power_minus1_even power_minus [of a]) |
308 |
308 |
309 lemma zero_le_even_power: |
309 lemma zero_le_even_power: |
310 "0 \<le> (a::'a::{ordered_ring,ringpower}) ^ (2*n)" |
310 "0 \<le> (a::'a::{ordered_idom,ringpower}) ^ (2*n)" |
311 proof (induct "n") |
311 proof (induct "n") |
312 case 0 |
312 case 0 |
313 show ?case by (simp add: zero_le_one) |
313 show ?case by (simp add: zero_le_one) |
314 next |
314 next |
315 case (Suc n) |
315 case (Suc n) |
471 |
471 |
472 lemma eq_number_of_BIT_BIT: |
472 lemma eq_number_of_BIT_BIT: |
473 "((number_of (v BIT x) ::int) = number_of (w BIT y)) = |
473 "((number_of (v BIT x) ::int) = number_of (w BIT y)) = |
474 (x=y & (((number_of v) ::int) = number_of w))" |
474 (x=y & (((number_of v) ::int) = number_of w))" |
475 by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute |
475 by (simp only: simp_thms number_of_BIT lemma1 lemma2 eq_commute |
476 Ring_and_Field.add_left_cancel add_assoc Ring_and_Field.add_0 |
476 OrderedGroup.add_left_cancel add_assoc OrderedGroup.add_0 |
477 split add: split_if cong: imp_cong) |
477 split add: split_if cong: imp_cong) |
478 |
478 |
479 |
479 |
480 lemma eq_number_of_BIT_Pls: |
480 lemma eq_number_of_BIT_Pls: |
481 "((number_of (v BIT x) ::int) = number_of bin.Pls) = |
481 "((number_of (v BIT x) ::int) = number_of bin.Pls) = |