src/HOL/Integ/NatBin.thy
changeset 17085 5b57f995a179
parent 16775 c1b87ef4a1c3
child 17550 9bcd6ea262b8
equal deleted inserted replaced
17084:fb0a80aef0be 17085:5b57f995a179
   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 {*