equal
deleted
inserted
replaced
282 apply (subst nat_eq_iff) |
282 apply (subst nat_eq_iff) |
283 apply simp |
283 apply simp |
284 done |
284 done |
285 |
285 |
286 text{*Squares of literal numerals will be evaluated.*} |
286 text{*Squares of literal numerals will be evaluated.*} |
287 declare power2_eq_square [of "number_of w", standard, simp] |
287 lemmas power2_eq_square_number_of = |
|
288 power2_eq_square [of "number_of w", standard] |
|
289 declare power2_eq_square_number_of [simp] |
|
290 |
288 |
291 |
289 lemma zero_le_power2: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})" |
292 lemma zero_le_power2: "0 \<le> (a\<twosuperior>::'a::{ordered_idom,recpower})" |
290 by (simp add: power2_eq_square zero_le_square) |
293 by (simp add: power2_eq_square zero_le_square) |
291 |
294 |
292 lemma zero_less_power2: |
295 lemma zero_less_power2: |
541 (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))" |
544 (if neg (number_of v :: int) then 0^n else nat ((number_of v :: int) ^ n))" |
542 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq |
545 by (simp only: simp_thms neg_nat not_neg_eq_ge_0 nat_number_of_def nat_power_eq |
543 split add: split_if cong: imp_cong) |
546 split add: split_if cong: imp_cong) |
544 |
547 |
545 |
548 |
546 declare power_nat_number_of [of _ "number_of w", standard, simp] |
549 lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard] |
|
550 declare power_nat_number_of_number_of [simp] |
|
551 |
547 |
552 |
548 |
553 |
549 text{*For the integers*} |
554 text{*For the integers*} |
550 |
555 |
551 lemma zpower_number_of_even: |
556 lemma zpower_number_of_even: |
567 apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) |
572 apply (simp only: number_of_add nat_numeral_1_eq_1 not_neg_eq_ge_0 neg_eq_less_0) |
568 apply (rule_tac x = "number_of w" in spec, clarify) |
573 apply (rule_tac x = "number_of w" in spec, clarify) |
569 apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat) |
574 apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat) |
570 done |
575 done |
571 |
576 |
572 declare zpower_number_of_even [of "number_of v", standard, simp] |
577 lemmas zpower_number_of_even_number_of = |
573 declare zpower_number_of_odd [of "number_of v", standard, simp] |
578 zpower_number_of_even [of "number_of v", standard] |
|
579 declare zpower_number_of_even_number_of [simp] |
|
580 |
|
581 lemmas zpower_number_of_odd_number_of = |
|
582 zpower_number_of_odd [of "number_of v", standard] |
|
583 declare zpower_number_of_odd_number_of [simp] |
|
584 |
574 |
585 |
575 |
586 |
576 |
587 |
577 ML |
588 ML |
578 {* |
589 {* |