src/HOL/Nat_Numeral.thy
changeset 30960 fec1a04b7220
parent 30925 c38cbc0ac8d1
child 31002 bc4117fe72ab
     1.1 --- a/src/HOL/Nat_Numeral.thy	Wed Apr 22 19:09:19 2009 +0200
     1.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Apr 22 19:09:21 2009 +0200
     1.3 @@ -28,9 +28,12 @@
     1.4    "nat (number_of v) = number_of v"
     1.5    unfolding nat_number_of_def ..
     1.6  
     1.7 +context recpower
     1.8 +begin
     1.9 +
    1.10  abbreviation (xsymbols)
    1.11 -  power2 :: "'a::power => 'a"  ("(_\<twosuperior>)" [1000] 999) where
    1.12 -  "x\<twosuperior> == x^2"
    1.13 +  power2 :: "'a \<Rightarrow> 'a"  ("(_\<twosuperior>)" [1000] 999) where
    1.14 +  "x\<twosuperior> \<equiv> x ^ 2"
    1.15  
    1.16  notation (latex output)
    1.17    power2  ("(_\<twosuperior>)" [1000] 999)
    1.18 @@ -38,6 +41,8 @@
    1.19  notation (HTML output)
    1.20    power2  ("(_\<twosuperior>)" [1000] 999)
    1.21  
    1.22 +end
    1.23 +
    1.24  
    1.25  subsection {* Predicate for negative binary numbers *}
    1.26  
    1.27 @@ -397,8 +402,8 @@
    1.28  by (simp add: power_even_eq) 
    1.29  
    1.30  lemma power_minus_even [simp]:
    1.31 -     "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
    1.32 -by (simp add: power_minus1_even power_minus [of a]) 
    1.33 +  "(-a) ^ (2*n) = (a::'a::{comm_ring_1,recpower}) ^ (2*n)"
    1.34 +  by (simp add: power_minus [of a]) 
    1.35  
    1.36  lemma zero_le_even_power'[simp]:
    1.37       "0 \<le> (a::'a::{ordered_idom,recpower}) ^ (2*n)"
    1.38 @@ -972,4 +977,4 @@
    1.39      Suc_mod_eq_add3_mod [of _ "number_of v", standard]
    1.40  declare Suc_mod_eq_add3_mod_number_of [simp]
    1.41  
    1.42 -end
    1.43 +end
    1.44 \ No newline at end of file