# HG changeset patch # User haftmann # Date 1240481871 -7200 # Node ID 10fef94f40fc8d5457b552f8d46f2200c54b8bc0 # Parent b5d67f83576e0261d7aed214b71e3175ce1c6712 adaptions due to rearrangment of power operation diff -r b5d67f83576e -r 10fef94f40fc src/HOL/Algebra/abstract/Ring2.thy --- 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 \ 'a \ bool" (infixl "assoc" 50) where diff -r b5d67f83576e -r 10fef94f40fc src/HOL/Algebra/poly/LongDiv.thy --- 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 {* diff -r b5d67f83576e -r 10fef94f40fc src/HOL/Algebra/poly/UnivPoly2.thy --- 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 \ 'a up) ^ 0 = 1" - | "(a \ '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 "\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]: diff -r b5d67f83576e -r 10fef94f40fc src/HOL/Decision_Procs/Approximation.thy --- 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 @@ "(\j=0.. 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 `\ 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 `\ 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 \ 0" diff -r b5d67f83576e -r 10fef94f40fc src/HOL/NSA/HyperDef.thy --- 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] \ 'a star" (infixr "pow" 80) where +definition pow :: "['a::recpower star, nat star] \ 'a star" (infixr "pow" 80) where hyperpow_def [transfer_unfold, code del]: "R pow N = ( *f2* op ^) R N" (* hypernatural powers of hyperreals *) diff -r b5d67f83576e -r 10fef94f40fc src/HOL/NSA/StarDef.thy --- 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 ^) \ \x n. ( *f* (\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: "\x \ Standard; y \ Standard\ \ x mod y \ Standard" by (simp add: star_mod_def) -lemma Standard_power: "x \ Standard \ x ^ n \ 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 ^) \ \x n. ( *f* (\x. x ^ n)) x" +proof (rule eq_reflection, rule ext, rule ext) + fix n :: nat + show "\x::'a star. x ^ n = ( *f* (\x. x ^ n)) x" + proof (induct n) + case 0 + have "\x::'a star. ( *f* (\x. 1)) x = 1" + by transfer simp + then show ?case by simp + next + case (Suc n) + have "\x::'a star. x * ( *f* (\x\'a. x ^ n)) x = ( *f* (\x\'a. x * x ^ n)) x" + by transfer simp + with Suc show ?case by simp + qed +qed -instance star :: (recpower) recpower -proof - show "\a::'a star. a ^ 0 = 1" - by transfer (rule power_0) -next - fix n show "\a::'a star. a ^ Suc n = a * a ^ n" - by transfer (rule power_Suc) -qed +lemma Standard_power [simp]: "x \ Standard \ x ^ n \ 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 *} diff -r b5d67f83576e -r 10fef94f40fc src/HOL/SizeChange/Graphs.thy --- 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\type, 'b\monoid_mult) graph \ nat => ('a, 'b) graph" -where - "(A \ ('a, 'b) graph) ^ 0 = 1" -| "(A \ ('a, 'b) graph) ^ Suc n = A * (A ^ n)" - -definition - graph_star_def: "star (G \ ('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" "\n. a ^ (Suc n) = a * a ^ n" - by simp_all qed +instantiation graph :: (type, monoid_mult) star +begin + +definition + graph_star_def: "star (G \ ('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 = (\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 diff -r b5d67f83576e -r 10fef94f40fc src/HOL/Word/WordArith.thy --- 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) diff -r b5d67f83576e -r 10fef94f40fc src/HOL/Word/WordDefinition.thy --- 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\'a word) ^ 0 = 1" - | "(a\'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"