cleaned up theory power further
authorhaftmann
Mon Apr 27 10:11:44 2009 +0200 (2009-04-27)
changeset 310017e6ffd8f51a9
parent 31000 c2524d123528
child 31002 bc4117fe72ab
cleaned up theory power further
NEWS
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Int.thy
src/HOL/NSA/HyperDef.thy
src/HOL/Power.thy
     1.1 --- a/NEWS	Mon Apr 27 08:22:37 2009 +0200
     1.2 +++ b/NEWS	Mon Apr 27 10:11:44 2009 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  * Power operations on relations and functions are now one dedicate constant compow with
     1.6  infix syntax "^^".  Power operations on multiplicative monoids retains syntax "^"
     1.7 -and is now defined generic in class recpower; class power disappeared.  INCOMPATIBILITY.
     1.8 +and is now defined generic in class power.  INCOMPATIBILITY.
     1.9  
    1.10  * ML antiquotation @{code_datatype} inserts definition of a datatype generated
    1.11  by the code generator; see Predicate.thy for an example.
     2.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Apr 27 08:22:37 2009 +0200
     2.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Apr 27 10:11:44 2009 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5  subsection {* Ring axioms *}
     2.6  
     2.7 -class ring = zero + one + plus + minus + uminus + times + inverse + recpower + Ring_and_Field.dvd +
     2.8 +class ring = zero + one + plus + minus + uminus + times + inverse + power + dvd +
     2.9    assumes a_assoc:      "(a + b) + c = a + (b + c)"
    2.10    and l_zero:           "0 + a = a"
    2.11    and l_neg:            "(-a) + a = 0"
     3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 27 08:22:37 2009 +0200
     3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Mon Apr 27 10:11:44 2009 +0200
     3.3 @@ -345,11 +345,10 @@
     3.4      by (simp add: up_inverse_def)
     3.5    show "p / q = p * inverse q"
     3.6      by (simp add: up_divide_def)
     3.7 -  show "p * 1 = p"
     3.8 -    unfolding `p * 1 = 1 * p` by (fact `1 * p = p`)
     3.9  qed
    3.10  
    3.11 -instance up :: (ring) recpower ..
    3.12 +instance up :: (ring) recpower proof
    3.13 +qed simp_all
    3.14  
    3.15  (* Further properties of monom *)
    3.16  
     4.1 --- a/src/HOL/Int.thy	Mon Apr 27 08:22:37 2009 +0200
     4.2 +++ b/src/HOL/Int.thy	Mon Apr 27 10:11:44 2009 +0200
     4.3 @@ -1536,7 +1536,7 @@
     4.4  by (simp add: abs_if)
     4.5  
     4.6  lemma abs_power_minus_one [simp]:
     4.7 -     "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring,recpower})"
     4.8 +  "abs(-1 ^ n) = (1::'a::{ordered_idom,number_ring})"
     4.9  by (simp add: power_abs)
    4.10  
    4.11  lemma of_int_number_of_eq [simp]:
    4.12 @@ -1848,18 +1848,21 @@
    4.13  
    4.14  subsection {* Integer Powers *} 
    4.15  
    4.16 -instance int :: recpower ..
    4.17 +context ring_1
    4.18 +begin
    4.19  
    4.20  lemma of_int_power:
    4.21 -  "of_int (z ^ n) = (of_int z ^ n :: 'a::{recpower, ring_1})"
    4.22 +  "of_int (z ^ n) = of_int z ^ n"
    4.23    by (induct n) simp_all
    4.24  
    4.25 +end
    4.26 +
    4.27  lemma zpower_zpower:
    4.28    "(x ^ y) ^ z = (x ^ (y * z)::int)"
    4.29    by (rule power_mult [symmetric])
    4.30  
    4.31  lemma int_power:
    4.32 -  "int (m^n) = (int m) ^ n"
    4.33 +  "int (m ^ n) = int m ^ n"
    4.34    by (rule of_nat_power)
    4.35  
    4.36  lemmas zpower_int = int_power [symmetric]
    4.37 @@ -2200,6 +2203,8 @@
    4.38  
    4.39  subsection {* Legacy theorems *}
    4.40  
    4.41 +instance int :: recpower ..
    4.42 +
    4.43  lemmas zminus_zminus = minus_minus [of "z::int", standard]
    4.44  lemmas zminus_0 = minus_zero [where 'a=int]
    4.45  lemmas zminus_zadd_distrib = minus_add_distrib [of "z::int" "w", standard]
     5.1 --- a/src/HOL/NSA/HyperDef.thy	Mon Apr 27 08:22:37 2009 +0200
     5.2 +++ b/src/HOL/NSA/HyperDef.thy	Mon Apr 27 10:11:44 2009 +0200
     5.3 @@ -426,7 +426,7 @@
     5.4  
     5.5  subsection{*Powers with Hypernatural Exponents*}
     5.6  
     5.7 -definition pow :: "['a::recpower star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
     5.8 +definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
     5.9    hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
    5.10    (* hypernatural powers of hyperreals *)
    5.11  
    5.12 @@ -459,7 +459,7 @@
    5.13  by transfer (rule power_add)
    5.14  
    5.15  lemma hyperpow_one [simp]:
    5.16 -  "\<And>r. (r::'a::recpower star) pow (1::hypnat) = r"
    5.17 +  "\<And>r. (r::'a::monoid_mult star) pow (1::hypnat) = r"
    5.18  by transfer (rule power_one_right)
    5.19  
    5.20  lemma hyperpow_two:
     6.1 --- a/src/HOL/Power.thy	Mon Apr 27 08:22:37 2009 +0200
     6.2 +++ b/src/HOL/Power.thy	Mon Apr 27 10:11:44 2009 +0200
     6.3 @@ -36,7 +36,7 @@
     6.4    by (induct n) simp_all
     6.5  
     6.6  lemma power_one_right [simp]:
     6.7 -  "a ^ 1 = a * 1"
     6.8 +  "a ^ 1 = a"
     6.9    by simp
    6.10  
    6.11  lemma power_commutes: