1.1 --- a/src/HOL/Algebra/abstract/Ring2.thy Thu Apr 23 12:17:51 2009 +0200
1.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy Thu Apr 23 12:17:51 2009 +0200
1.3 @@ -12,7 +12,7 @@
1.4
1.5 subsection {* Ring axioms *}
1.6
1.7 -class ring = zero + one + plus + minus + uminus + times + inverse + power + Ring_and_Field.dvd +
1.8 +class ring = zero + one + plus + minus + uminus + times + inverse + recpower + Ring_and_Field.dvd +
1.9 assumes a_assoc: "(a + b) + c = a + (b + c)"
1.10 and l_zero: "0 + a = a"
1.11 and l_neg: "(-a) + a = 0"
1.12 @@ -28,8 +28,6 @@
1.13 assumes minus_def: "a - b = a + (-b)"
1.14 and inverse_def: "inverse a = (if a dvd 1 then THE x. a*x = 1 else 0)"
1.15 and divide_def: "a / b = a * inverse b"
1.16 - and power_0 [simp]: "a ^ 0 = 1"
1.17 - and power_Suc [simp]: "a ^ Suc n = a ^ n * a"
1.18 begin
1.19
1.20 definition assoc :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "assoc" 50) where
2.1 --- a/src/HOL/Algebra/poly/LongDiv.thy Thu Apr 23 12:17:51 2009 +0200
2.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy Thu Apr 23 12:17:51 2009 +0200
2.3 @@ -1,6 +1,5 @@
2.4 (*
2.5 Experimental theory: long division of polynomials
2.6 - $Id$
2.7 Author: Clemens Ballarin, started 23 June 1999
2.8 *)
2.9
2.10 @@ -133,9 +132,9 @@
2.11 delsimprocs [ring_simproc]) 1 *})
2.12 apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
2.13 apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
2.14 - thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc1", thm "smult_assoc2"]
2.15 + thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc2"]
2.16 delsimprocs [ring_simproc]) 1 *})
2.17 - apply simp
2.18 + apply (simp add: smult_assoc1 [symmetric])
2.19 done
2.20
2.21 ML {*
3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu Apr 23 12:17:51 2009 +0200
3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy Thu Apr 23 12:17:51 2009 +0200
3.3 @@ -155,16 +155,6 @@
3.4
3.5 end
3.6
3.7 -instantiation up :: ("{times, one, comm_monoid_add}") power
3.8 -begin
3.9 -
3.10 -primrec power_up where
3.11 - "(a \<Colon> 'a up) ^ 0 = 1"
3.12 - | "(a \<Colon> 'a up) ^ Suc n = a ^ n * a"
3.13 -
3.14 -instance ..
3.15 -
3.16 -end
3.17
3.18 subsection {* Effect of operations on coefficients *}
3.19
3.20 @@ -328,8 +318,9 @@
3.21 qed
3.22 show "(p + q) * r = p * r + q * r"
3.23 by (rule up_eqI) simp
3.24 - show "p * q = q * p"
3.25 + show "\<And>q. p * q = q * p"
3.26 proof (rule up_eqI)
3.27 + fix q
3.28 fix n
3.29 {
3.30 fix k
3.31 @@ -354,11 +345,12 @@
3.32 by (simp add: up_inverse_def)
3.33 show "p / q = p * inverse q"
3.34 by (simp add: up_divide_def)
3.35 - fix n
3.36 - show "p ^ 0 = 1" by simp
3.37 - show "p ^ Suc n = p ^ n * p" by simp
3.38 + show "p * 1 = p"
3.39 + unfolding `p * 1 = 1 * p` by (fact `1 * p = p`)
3.40 qed
3.41
3.42 +instance up :: (ring) recpower ..
3.43 +
3.44 (* Further properties of monom *)
3.45
3.46 lemma monom_zero [simp]:
4.1 --- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 23 12:17:51 2009 +0200
4.2 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Apr 23 12:17:51 2009 +0200
4.3 @@ -97,7 +97,7 @@
4.4 "(\<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")
4.5 proof -
4.6 { fix x y z :: float have "x - y * z = x + - y * z"
4.7 - by (cases x, cases y, cases z, simp add: plus_float.simps minus_float.simps uminus_float.simps times_float.simps algebra_simps)
4.8 + by (cases x, cases y, cases z, simp add: plus_float.simps minus_float_def uminus_float.simps times_float.simps algebra_simps)
4.9 } note diff_mult_minus = this
4.10
4.11 { fix x :: float have "- (- x) = x" by (cases x, auto simp add: uminus_float.simps) } note minus_minus = this
4.12 @@ -1462,7 +1462,8 @@
4.13 finally have "0 < Ifloat ((?horner x) ^ num)" .
4.14 }
4.15 ultimately show ?thesis
4.16 - 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)
4.17 + unfolding lb_exp.simps if_not_P[OF `\<not> 0 < x`] Let_def
4.18 + by (cases "floor_fl x", cases "x < - 1", auto simp add: float_power le_float_def less_float_def)
4.19 qed
4.20
4.21 lemma exp_boundaries': assumes "x \<le> 0"
5.1 --- a/src/HOL/NSA/HyperDef.thy Thu Apr 23 12:17:51 2009 +0200
5.2 +++ b/src/HOL/NSA/HyperDef.thy Thu Apr 23 12:17:51 2009 +0200
5.3 @@ -426,7 +426,7 @@
5.4
5.5 subsection{*Powers with Hypernatural Exponents*}
5.6
5.7 -definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
5.8 +definition pow :: "['a::recpower 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
6.1 --- a/src/HOL/NSA/StarDef.thy Thu Apr 23 12:17:51 2009 +0200
6.2 +++ b/src/HOL/NSA/StarDef.thy Thu Apr 23 12:17:51 2009 +0200
6.3 @@ -1,5 +1,4 @@
6.4 (* Title : HOL/Hyperreal/StarDef.thy
6.5 - ID : $Id$
6.6 Author : Jacques D. Fleuriot and Brian Huffman
6.7 *)
6.8
6.9 @@ -546,16 +545,6 @@
6.10
6.11 end
6.12
6.13 -instantiation star :: (power) power
6.14 -begin
6.15 -
6.16 -definition
6.17 - star_power_def: "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
6.18 -
6.19 -instance ..
6.20 -
6.21 -end
6.22 -
6.23 instantiation star :: (ord) ord
6.24 begin
6.25
6.26 @@ -574,7 +563,7 @@
6.27 star_add_def star_diff_def star_minus_def
6.28 star_mult_def star_divide_def star_inverse_def
6.29 star_le_def star_less_def star_abs_def star_sgn_def
6.30 - star_div_def star_mod_def star_power_def
6.31 + star_div_def star_mod_def
6.32
6.33 text {* Class operations preserve standard elements *}
6.34
6.35 @@ -614,15 +603,11 @@
6.36 lemma Standard_mod: "\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> x mod y \<in> Standard"
6.37 by (simp add: star_mod_def)
6.38
6.39 -lemma Standard_power: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
6.40 -by (simp add: star_power_def)
6.41 -
6.42 lemmas Standard_simps [simp] =
6.43 Standard_zero Standard_one Standard_number_of
6.44 Standard_add Standard_diff Standard_minus
6.45 Standard_mult Standard_divide Standard_inverse
6.46 Standard_abs Standard_div Standard_mod
6.47 - Standard_power
6.48
6.49 text {* @{term star_of} preserves class operations *}
6.50
6.51 @@ -650,9 +635,6 @@
6.52 lemma star_of_mod: "star_of (x mod y) = star_of x mod star_of y"
6.53 by transfer (rule refl)
6.54
6.55 -lemma star_of_power: "star_of (x ^ n) = star_of x ^ n"
6.56 -by transfer (rule refl)
6.57 -
6.58 lemma star_of_abs: "star_of (abs x) = abs (star_of x)"
6.59 by transfer (rule refl)
6.60
6.61 @@ -717,8 +699,7 @@
6.62 lemmas star_of_simps [simp] =
6.63 star_of_add star_of_diff star_of_minus
6.64 star_of_mult star_of_divide star_of_inverse
6.65 - star_of_div star_of_mod
6.66 - star_of_power star_of_abs
6.67 + star_of_div star_of_mod star_of_abs
6.68 star_of_zero star_of_one star_of_number_of
6.69 star_of_less star_of_le star_of_eq
6.70 star_of_0_less star_of_0_le star_of_0_eq
6.71 @@ -970,26 +951,36 @@
6.72 instance star :: (ordered_idom) ordered_idom ..
6.73 instance star :: (ordered_field) ordered_field ..
6.74
6.75 -subsection {* Power classes *}
6.76
6.77 -text {*
6.78 - Proving the class axiom @{thm [source] power_Suc} for type
6.79 - @{typ "'a star"} is a little tricky, because it quantifies
6.80 - over values of type @{typ nat}. The transfer principle does
6.81 - not handle quantification over non-star types in general,
6.82 - but we can work around this by fixing an arbitrary @{typ nat}
6.83 - value, and then applying the transfer principle.
6.84 -*}
6.85 +subsection {* Power *}
6.86
6.87 -instance star :: (recpower) recpower
6.88 -proof
6.89 - show "\<And>a::'a star. a ^ 0 = 1"
6.90 - by transfer (rule power_0)
6.91 -next
6.92 - fix n show "\<And>a::'a star. a ^ Suc n = a * a ^ n"
6.93 - by transfer (rule power_Suc)
6.94 +instance star :: (recpower) recpower ..
6.95 +
6.96 +lemma star_power_def [transfer_unfold]:
6.97 + "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
6.98 +proof (rule eq_reflection, rule ext, rule ext)
6.99 + fix n :: nat
6.100 + show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x"
6.101 + proof (induct n)
6.102 + case 0
6.103 + have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
6.104 + by transfer simp
6.105 + then show ?case by simp
6.106 + next
6.107 + case (Suc n)
6.108 + have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x"
6.109 + by transfer simp
6.110 + with Suc show ?case by simp
6.111 + qed
6.112 qed
6.113
6.114 +lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
6.115 + by (simp add: star_power_def)
6.116 +
6.117 +lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n"
6.118 + by transfer (rule refl)
6.119 +
6.120 +
6.121 subsection {* Number classes *}
6.122
6.123 lemma star_of_nat_def [transfer_unfold]: "of_nat n = star_of (of_nat n)"
7.1 --- a/src/HOL/SizeChange/Graphs.thy Thu Apr 23 12:17:51 2009 +0200
7.2 +++ b/src/HOL/SizeChange/Graphs.thy Thu Apr 23 12:17:51 2009 +0200
7.3 @@ -228,18 +228,8 @@
7.4 qed
7.5 qed
7.6
7.7 -instantiation graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower, star}"
7.8 -begin
7.9 -
7.10 -primrec power_graph :: "('a\<Colon>type, 'b\<Colon>monoid_mult) graph \<Rightarrow> nat => ('a, 'b) graph"
7.11 -where
7.12 - "(A \<Colon> ('a, 'b) graph) ^ 0 = 1"
7.13 -| "(A \<Colon> ('a, 'b) graph) ^ Suc n = A * (A ^ n)"
7.14 -
7.15 -definition
7.16 - graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)"
7.17 -
7.18 -instance proof
7.19 +instance graph :: (type, monoid_mult) "{semiring_1, idem_add, recpower}"
7.20 +proof
7.21 fix a b c :: "('a, 'b) graph"
7.22
7.23 show "1 * a = a"
7.24 @@ -258,10 +248,16 @@
7.25
7.26 show "a + a = a" unfolding graph_plus_def by simp
7.27
7.28 - show "a ^ 0 = 1" "\<And>n. a ^ (Suc n) = a * a ^ n"
7.29 - by simp_all
7.30 qed
7.31
7.32 +instantiation graph :: (type, monoid_mult) star
7.33 +begin
7.34 +
7.35 +definition
7.36 + graph_star_def: "star (G \<Colon> ('a, 'b) graph) = (SUP n. G ^ n)"
7.37 +
7.38 +instance ..
7.39 +
7.40 end
7.41
7.42 lemma graph_leqI:
7.43 @@ -351,7 +347,7 @@
7.44
7.45 lemma in_tcl:
7.46 "has_edge (tcl G) a x b = (\<exists>n>0. has_edge (G ^ n) a x b)"
7.47 - apply (auto simp: tcl_is_SUP in_SUP simp del: power_graph.simps power_Suc)
7.48 + apply (auto simp: tcl_is_SUP in_SUP simp del: power.simps power_Suc)
7.49 apply (rule_tac x = "n - 1" in exI, auto)
7.50 done
7.51
8.1 --- a/src/HOL/Word/WordArith.thy Thu Apr 23 12:17:51 2009 +0200
8.2 +++ b/src/HOL/Word/WordArith.thy Thu Apr 23 12:17:51 2009 +0200
8.3 @@ -778,6 +778,8 @@
8.4 apply (simp add: word_mult_1)
8.5 done
8.6
8.7 +instance word :: (len0) recpower ..
8.8 +
8.9 instance word :: (len0) comm_semiring
8.10 by (intro_classes) (simp add : word_left_distrib)
8.11
9.1 --- a/src/HOL/Word/WordDefinition.thy Thu Apr 23 12:17:51 2009 +0200
9.2 +++ b/src/HOL/Word/WordDefinition.thy Thu Apr 23 12:17:51 2009 +0200
9.3 @@ -99,7 +99,7 @@
9.4
9.5 subsection "Arithmetic operations"
9.6
9.7 -instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, power, ord, bit}"
9.8 +instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord, bit}"
9.9 begin
9.10
9.11 definition
9.12 @@ -126,10 +126,6 @@
9.13 definition
9.14 word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
9.15
9.16 -primrec power_word where
9.17 - "(a\<Colon>'a word) ^ 0 = 1"
9.18 - | "(a\<Colon>'a word) ^ Suc n = a * a ^ n"
9.19 -
9.20 definition
9.21 word_number_of_def: "number_of w = word_of_int w"
9.22
9.23 @@ -157,7 +153,7 @@
9.24
9.25 instance ..
9.26
9.27 -end
9.28 +end
9.29
9.30 definition
9.31 word_succ :: "'a :: len0 word => 'a word"