adaptions due to rearrangment of power operation
authorhaftmann
Thu Apr 23 12:17:51 2009 +0200 (2009-04-23)
changeset 3096810fef94f40fc
parent 30967 b5d67f83576e
child 30969 fd9c89419358
adaptions due to rearrangment of power operation
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/NSA/HyperDef.thy
src/HOL/NSA/StarDef.thy
src/HOL/SizeChange/Graphs.thy
src/HOL/Word/WordArith.thy
src/HOL/Word/WordDefinition.thy
     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,25 +951,35 @@
    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 +subsection {* Power *}
    6.78 +
    6.79 +instance star :: (recpower) recpower ..
    6.80  
    6.81 -text {*
    6.82 -  Proving the class axiom @{thm [source] power_Suc} for type
    6.83 -  @{typ "'a star"} is a little tricky, because it quantifies
    6.84 -  over values of type @{typ nat}. The transfer principle does
    6.85 -  not handle quantification over non-star types in general,
    6.86 -  but we can work around this by fixing an arbitrary @{typ nat}
    6.87 -  value, and then applying the transfer principle.
    6.88 -*}
    6.89 +lemma star_power_def [transfer_unfold]:
    6.90 +  "(op ^) \<equiv> \<lambda>x n. ( *f* (\<lambda>x. x ^ n)) x"
    6.91 +proof (rule eq_reflection, rule ext, rule ext)
    6.92 +  fix n :: nat
    6.93 +  show "\<And>x::'a star. x ^ n = ( *f* (\<lambda>x. x ^ n)) x" 
    6.94 +  proof (induct n)
    6.95 +    case 0
    6.96 +    have "\<And>x::'a star. ( *f* (\<lambda>x. 1)) x = 1"
    6.97 +      by transfer simp
    6.98 +    then show ?case by simp
    6.99 +  next
   6.100 +    case (Suc n)
   6.101 +    have "\<And>x::'a star. x * ( *f* (\<lambda>x\<Colon>'a. x ^ n)) x = ( *f* (\<lambda>x\<Colon>'a. x * x ^ n)) x"
   6.102 +      by transfer simp
   6.103 +    with Suc show ?case by simp
   6.104 +  qed
   6.105 +qed
   6.106  
   6.107 -instance star :: (recpower) recpower
   6.108 -proof
   6.109 -  show "\<And>a::'a star. a ^ 0 = 1"
   6.110 -    by transfer (rule power_0)
   6.111 -next
   6.112 -  fix n show "\<And>a::'a star. a ^ Suc n = a * a ^ n"
   6.113 -    by transfer (rule power_Suc)
   6.114 -qed
   6.115 +lemma Standard_power [simp]: "x \<in> Standard \<Longrightarrow> x ^ n \<in> Standard"
   6.116 +  by (simp add: star_power_def)
   6.117 +
   6.118 +lemma star_of_power [simp]: "star_of (x ^ n) = star_of x ^ n"
   6.119 +  by transfer (rule refl)
   6.120 +
   6.121  
   6.122  subsection {* Number classes *}
   6.123  
     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"