--- a/src/HOL/Algebra/abstract/Ring2.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Thu Apr 23 12:17:51 2009 +0200
@@ -12,7 +12,7 @@
subsection {* Ring axioms *}
-class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd +
+class ring = zero + one + plus + minus + uminus + times + inverse + recpower + Ring_and_Field.dvd +
assumes a_assoc: "(a + b) + c = a + (b + c)"
and l_zero: "0 + a = a"
and l_neg: "(-a) + a = 0"
@@ -28,8 +28,6 @@
assumes minus_def: "a - b = a + (-b)"
and inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
and divide_def: "a / b = a * inverse b"
- and power_0 [simp]: "a ^ 0 = 1"
- and power_Suc [simp]: "a ^ Suc n = a ^ n * a"
begin
definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
--- a/src/HOL/Algebra/poly/LongDiv.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Algebra/poly/LongDiv.thy Thu Apr 23 12:17:51 2009 +0200
@@ -1,6 +1,5 @@
(*
Experimental theory: long division of polynomials
- $Id$
Author: Clemens Ballarin, started 23 June 1999
*)
@@ -133,9 +132,9 @@
delsimprocs [ring_simproc]) 1 *})
apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
- thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"]
+ thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc2"]
delsimprocs [ring_simproc]) 1 *})
- apply simp
+ apply (simp add: smult_assoc1 [symmetric])
done
ML {*
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Thu Apr 23 12:17:51 2009 +0200
@@ -155,16 +155,6 @@
end
-instantiation up :: ("{times, one, comm_monoid_add}") power
-begin
-
-primrec power_up where
- "(a \<Colon> 'a up) ^ 0 = 1"
- | "(a \<Colon> 'a up) ^ Suc n = a ^ n * a"
-
-instance ..
-
-end
subsection {* Effect of operations on coefficients *}
@@ -328,8 +318,9 @@
qed
show "(p + q) * r = p * r + q * r"
by (rule up_eqI) simp
- show "p * q = q * p"
+ show "\<And>q. p * q = q * p"
proof (rule up_eqI)
+ fix q
fix n
{
fix k
@@ -354,11 +345,12 @@
by (simp add: up_inverse_def)
show "p / q = p * inverse q"
by (simp add: up_divide_def)
- fix n
- show "p ^ 0 = 1" by simp
- show "p ^ Suc n = p ^ n * p" by simp
+ show "p * 1 = p"
+ unfolding `p * 1 = 1 * p` by (fact `1 * p = p`)
qed
+instance up :: (ring) recpower ..
+
(* Further properties of monom *)
lemma monom_zero [simp]:
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 23 12:17:51 2009 +0200
@@ -97,7 +97,7 @@
"(\<Sum>j=0..<n. (1 / real (f (j' + j))) * (Ifloat x ^ j)) \<le> Ifloat (ub n ((F o^ j') s) (f j') x)" (is "?ub")
proof -
{ fix x y z :: float have "x - y * z = x + - y * z"
- by (cases x, cases y, cases z, simp add: plus_float.simps minus_float.simps uminus_float.simps times_float.simps algebra_simps)
+ by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def uminus_float.simps times_float.simps algebra_simps)
} note diff_mult_minus = this
{ fix x :: float have "- (- x) = x" by (cases x, auto simp add: uminus_float.simps) } note minus_minus = this
@@ -1462,7 +1462,8 @@
finally have "0 < Ifloat ((?horner x) ^ num)" .
}
ultimately show ?thesis
- unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def by (cases "floor_fl x", cases "x < - 1", auto simp add: le_float_def less_float_def normfloat)
+ unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def
+ by (cases "floor_fl x", cases "x < - 1", auto simp add: float_power le_float_def less_float_def)
qed
lemma exp_boundaries': assumes "x \<le> 0"
--- a/src/HOL/NSA/HyperDef.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/NSA/HyperDef.thy Thu Apr 23 12:17:51 2009 +0200
@@ -426,7 +426,7 @@
subsection{*Powers with Hypernatural Exponents*}
-definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+definition pow :: "['a::recpower star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N"
(* hypernatural powers of hyperreals *)
--- a/src/HOL/NSA/StarDef.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/NSA/StarDef.thy Thu Apr 23 12:17:51 2009 +0200
@@ -1,5 +1,4 @@
(* Title : HOL/Hyperreal/StarDef.thy
- ID : $Id$
Author : Jacques D. Fleuriot and Brian Huffman
*)
@@ -546,16 +545,6 @@
end
-instantiation star :: (power) power
-begin
-
-definition
- star_power_def: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
-
-instance ..
-
-end
-
instantiation star :: (ord) ord
begin
@@ -574,7 +563,7 @@
star_add_def star_diff_def star_minus_def
star_mult_def star_divide_def star_inverse_def
star_le_def star_less_def star_abs_def star_sgn_def
- star_div_def star_mod_def star_power_def
+ star_div_def star_mod_def
text {* Class operations preserve standard elements *}
@@ -614,15 +603,11 @@
lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
by (simp add: star_mod_def)
-lemma Standard_power: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
-by (simp add: star_power_def)
-
lemmas Standard_simps [simp] =
Standard_zero Standard_one Standard_number_of
Standard_add Standard_diff Standard_minus
Standard_mult Standard_divide Standard_inverse
Standard_abs Standard_div Standard_mod
- Standard_power
text {* @{term star_of} preserves class operations *}
@@ -650,9 +635,6 @@
lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
by transfer (rule refl)
-lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
-by transfer (rule refl)
-
lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
by transfer (rule refl)
@@ -717,8 +699,7 @@
lemmas star_of_simps [simp] =
star_of_add star_of_diff star_of_minus
star_of_mult star_of_divide star_of_inverse
- star_of_div star_of_mod
- star_of_power star_of_abs
+ star_of_div star_of_mod star_of_abs
star_of_zero star_of_one star_of_number_of
star_of_less star_of_le star_of_eq
star_of_0_less star_of_0_le star_of_0_eq
@@ -970,25 +951,35 @@
instance star :: (ordered_idom) ordered_idom ..
instance star :: (ordered_field) ordered_field ..
-subsection {* Power classes *}
+
+subsection {* Power *}
+
+instance star :: (recpower) recpower ..
-text {*
- Proving the class axiom @{thm [source] power_Suc} for type
- @{typ "'a star"} is a little tricky, because it quantifies
- over values of type @{typ nat}. The transfer principle does
- not handle quantification over non-star types in general,
- but we can work around this by fixing an arbitrary @{typ nat}
- value, and then applying the transfer principle.
-*}
+lemma star_power_def [transfer_unfold]:
+ "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
+proof (rule eq_reflection, rule ext, rule ext)
+ fix n :: nat
+ show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x"
+ proof (induct n)
+ case 0
+ have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
+ by transfer simp
+ then show ?case by simp
+ next
+ case (Suc n)
+ have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x"
+ by transfer simp
+ with Suc show ?case by simp
+ qed
+qed
-instance star :: (recpower) recpower
-proof
- show "\<And>a::'a star. a ^ 0 = 1"
- by transfer (rule power_0)
-next
- fix n show "\<And>a::'a star. a ^ Suc n = a * a ^ n"
- by transfer (rule power_Suc)
-qed
+lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
+ by (simp add: star_power_def)
+
+lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n"
+ by transfer (rule refl)
+
subsection {* Number classes *}
--- a/src/HOL/SizeChange/Graphs.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/SizeChange/Graphs.thy Thu Apr 23 12:17:51 2009 +0200
@@ -228,18 +228,8 @@
qed
qed
-instantiation graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower, star}"
-begin
-
-primrec power_graph :: "('a\<Colon>type, 'b\<Colon>monoid_mult) graph \<Rightarrow> nat => ('a, 'b) graph"
-where
- "(A \<Colon> ('a, 'b) graph) ^ 0 = 1"
-| "(A \<Colon> ('a, 'b) graph) ^ Suc n = A * (A ^ n)"
-
-definition
- graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)"
-
-instance proof
+instance graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower}"
+proof
fix a b c :: "('a, 'b) graph"
show "1 * a = a"
@@ -258,10 +248,16 @@
show "a + a = a" unfolding graph_plus_def by simp
- show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
- by simp_all
qed
+instantiation graph :: (type, monoid_mult) star
+begin
+
+definition
+ graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)"
+
+instance ..
+
end
lemma graph_leqI:
@@ -351,7 +347,7 @@
lemma in_tcl:
"has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
- apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps power_Suc)
+ apply (auto simp: tcl_is_SUP in_SUP simp del: power.simps power_Suc)
apply (rule_tac x = "n - 1" in exI, auto)
done
--- a/src/HOL/Word/WordArith.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Word/WordArith.thy Thu Apr 23 12:17:51 2009 +0200
@@ -778,6 +778,8 @@
apply (simp add: word_mult_1)
done
+instance word :: (len0) recpower ..
+
instance word :: (len0) comm_semiring
by (intro_classes) (simp add : word_left_distrib)
--- a/src/HOL/Word/WordDefinition.thy Thu Apr 23 12:17:51 2009 +0200
+++ b/src/HOL/Word/WordDefinition.thy Thu Apr 23 12:17:51 2009 +0200
@@ -99,7 +99,7 @@
subsection "Arithmetic operations"
-instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
+instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord, bit}"
begin
definition
@@ -126,10 +126,6 @@
definition
word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
-primrec power_word where
- "(a\<Colon>'a word) ^ 0 = 1"
- | "(a\<Colon>'a word) ^ Suc n = a * a ^ n"
-
definition
word_number_of_def: "number_of w = word_of_int w"
@@ -157,7 +153,7 @@
instance ..
-end
+end
definition
word_succ :: "'a :: len0 word => 'a word"