author haftmann Thu, 23 Apr 2009 12:17:51 +0200 changeset 30968 10fef94f40fc parent 30967 b5d67f83576e child 30969 fd9c89419358
adaptions due to rearrangment of power operation
 src/HOL/Algebra/abstract/Ring2.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/poly/LongDiv.thy file | annotate | diff | comparison | revisions src/HOL/Algebra/poly/UnivPoly2.thy file | annotate | diff | comparison | revisions src/HOL/Decision_Procs/Approximation.thy file | annotate | diff | comparison | revisions src/HOL/NSA/HyperDef.thy file | annotate | diff | comparison | revisions src/HOL/NSA/StarDef.thy file | annotate | diff | comparison | revisions src/HOL/SizeChange/Graphs.thy file | annotate | diff | comparison | revisions src/HOL/Word/WordArith.thy file | annotate | diff | comparison | revisions src/HOL/Word/WordDefinition.thy file | annotate | diff | comparison | revisions
```--- 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"```