src/HOL/Int.thy
changeset 31001 7e6ffd8f51a9
parent 30960 fec1a04b7220
child 31010 aabad7789183
     1.1 --- a/src/HOL/Int.thy	Mon Apr 27 08:22:37 2009 +0200
     1.2 +++ b/src/HOL/Int.thy	Mon Apr 27 10:11:44 2009 +0200
     1.3 @@ -1536,7 +1536,7 @@
     1.4  by (simp add: abs_if)
     1.5  
     1.6  lemma abs_power_minus_one [simp]:
     1.7 -     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
     1.8 +  "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring})"
     1.9  by (simp add: power_abs)
    1.10  
    1.11  lemma of_int_number_of_eq [simp]:
    1.12 @@ -1848,18 +1848,21 @@
    1.13  
    1.14  subsection {* Integer Powers *} 
    1.15  
    1.16 -instance int :: recpower ..
    1.17 +context ring_1
    1.18 +begin
    1.19  
    1.20  lemma of_int_power:
    1.21 -  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
    1.22 +  "of_int (z ^ n) = of_int z ^ n"
    1.23    by (induct n) simp_all
    1.24  
    1.25 +end
    1.26 +
    1.27  lemma zpower_zpower:
    1.28    "(x ^ y) ^ z = (x ^ (y * z)::int)"
    1.29    by (rule power_mult [symmetric])
    1.30  
    1.31  lemma int_power:
    1.32 -  "int (m^n) = (int m) ^ n"
    1.33 +  "int (m ^ n) = int m ^ n"
    1.34    by (rule of_nat_power)
    1.35  
    1.36  lemmas zpower_int = int_power [symmetric]
    1.37 @@ -2200,6 +2203,8 @@
    1.38  
    1.39  subsection {* Legacy theorems *}
    1.40  
    1.41 +instance int :: recpower ..
    1.42 +
    1.43  lemmas zminus_zminus = minus_minus [of "z::int", standard]
    1.44  lemmas zminus_0 = minus_zero [where 'a=int]
    1.45  lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]