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.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]