equal
deleted
inserted
replaced
297 lemma power2_minus [simp]: |
297 lemma power2_minus [simp]: |
298 "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})" |
298 "(- a)\<twosuperior> = (a\<twosuperior>::'a::{comm_ring_1,recpower})" |
299 by (simp add: power2_eq_square) |
299 by (simp add: power2_eq_square) |
300 |
300 |
301 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})" |
301 lemma power_minus1_even: "(- 1) ^ (2*n) = (1::'a::{comm_ring_1,recpower})" |
302 apply (induct_tac "n") |
302 apply (induct "n") |
303 apply (auto simp add: power_Suc power_add) |
303 apply (auto simp add: power_Suc power_add) |
304 done |
304 done |
305 |
305 |
306 lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2" |
306 lemma power_even_eq: "(a::'a::recpower) ^ (2*n) = (a^n)^2" |
307 by (simp add: power_mult power_mult_distrib power2_eq_square) |
307 by (simp add: power_mult power_mult_distrib power2_eq_square) |
518 |
518 |
519 |
519 |
520 subsection{*Literal arithmetic involving powers*} |
520 subsection{*Literal arithmetic involving powers*} |
521 |
521 |
522 lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n" |
522 lemma nat_power_eq: "(0::int) <= z ==> nat (z^n) = nat z ^ n" |
523 apply (induct_tac "n") |
523 apply (induct "n") |
524 apply (simp_all (no_asm_simp) add: nat_mult_distrib) |
524 apply (simp_all (no_asm_simp) add: nat_mult_distrib) |
525 done |
525 done |
526 |
526 |
527 lemma power_nat_number_of: |
527 lemma power_nat_number_of: |
528 "(number_of v :: nat) ^ n = |
528 "(number_of v :: nat) ^ n = |