--- a/src/HOL/Divides.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Divides.thy Thu Aug 06 23:56:48 2015 +0200
@@ -30,13 +30,17 @@
using div_mult_self1 [of b 0 a] by (simp add: ac_simps)
qed simp
-lemma power_not_zero: -- \<open>FIXME cf. @{text field_power_not_zero}\<close>
- "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
- by (induct n) (simp_all add: no_zero_divisors)
-
-lemma semiring_div_power_eq_0_iff: -- \<open>FIXME cf. @{text power_eq_0_iff}, @{text power_eq_0_nat_iff}\<close>
- "n \<noteq> 0 \<Longrightarrow> a ^ n = 0 \<longleftrightarrow> a = 0"
- using power_not_zero [of a n] by (auto simp add: zero_power)
+lemma div_by_1:
+ "a div 1 = a"
+ by (fact divide_1)
+
+lemma div_mult_self1_is_id:
+ "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
+ by (fact nonzero_mult_divide_cancel_left)
+
+lemma div_mult_self2_is_id:
+ "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
+ by (fact nonzero_mult_divide_cancel_right)
text \<open>@{const divide} and @{const mod}\<close>
@@ -104,31 +108,24 @@
"(b * c + a) mod b = a mod b"
by (simp add: add.commute)
-lemma div_mult_self1_is_id:
- "b \<noteq> 0 \<Longrightarrow> b * a div b = a"
- by (fact nonzero_mult_divide_cancel_left)
-
-lemma div_mult_self2_is_id:
- "b \<noteq> 0 \<Longrightarrow> a * b div b = a"
- by (fact nonzero_mult_divide_cancel_right)
-
-lemma mod_mult_self1_is_0 [simp]: "b * a mod b = 0"
+lemma mod_mult_self1_is_0 [simp]:
+ "b * a mod b = 0"
using mod_mult_self2 [of 0 b a] by simp
-lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
+lemma mod_mult_self2_is_0 [simp]:
+ "a * b mod b = 0"
using mod_mult_self1 [of 0 a b] by simp
-lemma div_by_1: "a div 1 = a"
- by (fact divide_1)
-
-lemma mod_by_1 [simp]: "a mod 1 = 0"
+lemma mod_by_1 [simp]:
+ "a mod 1 = 0"
proof -
from mod_div_equality [of a one] div_by_1 have "a + a mod 1 = a" by simp
then have "a + a mod 1 = a + 0" by simp
then show ?thesis by (rule add_left_imp_eq)
qed
-lemma mod_self [simp]: "a mod a = 0"
+lemma mod_self [simp]:
+ "a mod a = 0"
using mod_mult_self2_is_0 [of 1] by simp
lemma div_add_self1 [simp]:
@@ -181,7 +178,7 @@
then show "b dvd a" ..
qed
-lemma dvd_eq_mod_eq_0 [code]:
+lemma dvd_eq_mod_eq_0 [nitpick_unfold, code]:
"a dvd b \<longleftrightarrow> b mod a = 0"
by (simp add: mod_eq_0_iff_dvd)
@@ -212,17 +209,6 @@
finally show ?thesis .
qed
-lemma div_dvd_div [simp]:
- assumes "a dvd b" and "a dvd c"
- shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
-using assms apply (cases "a = 0")
-apply auto
-apply (unfold dvd_def)
-apply auto
- apply(blast intro:mult.assoc[symmetric])
-apply(fastforce simp add: mult.assoc)
-done
-
lemma dvd_mod_imp_dvd:
assumes "k dvd m mod n" and "k dvd n"
shows "k dvd m"
@@ -234,7 +220,8 @@
text \<open>Addition respects modular equivalence.\<close>
-lemma mod_add_left_eq: "(a + b) mod c = (a mod c + b) mod c"
+lemma mod_add_left_eq: -- \<open>FIXME reorient\<close>
+ "(a + b) mod c = (a mod c + b) mod c"
proof -
have "(a + b) mod c = (a div c * c + a mod c + b) mod c"
by (simp only: mod_div_equality)
@@ -245,7 +232,8 @@
finally show ?thesis .
qed
-lemma mod_add_right_eq: "(a + b) mod c = (a + b mod c) mod c"
+lemma mod_add_right_eq: -- \<open>FIXME reorient\<close>
+ "(a + b) mod c = (a + b mod c) mod c"
proof -
have "(a + b) mod c = (a + (b div c * c + b mod c)) mod c"
by (simp only: mod_div_equality)
@@ -256,7 +244,8 @@
finally show ?thesis .
qed
-lemma mod_add_eq: "(a + b) mod c = (a mod c + b mod c) mod c"
+lemma mod_add_eq: -- \<open>FIXME reorient\<close>
+ "(a + b) mod c = (a mod c + b mod c) mod c"
by (rule trans [OF mod_add_left_eq mod_add_right_eq])
lemma mod_add_cong:
@@ -270,13 +259,10 @@
by (simp only: mod_add_eq [symmetric])
qed
-lemma div_add [simp]: "z dvd x \<Longrightarrow> z dvd y
- \<Longrightarrow> (x + y) div z = x div z + y div z"
-by (cases "z = 0", simp, unfold dvd_def, auto simp add: algebra_simps)
-
text \<open>Multiplication respects modular equivalence.\<close>
-lemma mod_mult_left_eq: "(a * b) mod c = ((a mod c) * b) mod c"
+lemma mod_mult_left_eq: -- \<open>FIXME reorient\<close>
+ "(a * b) mod c = ((a mod c) * b) mod c"
proof -
have "(a * b) mod c = ((a div c * c + a mod c) * b) mod c"
by (simp only: mod_div_equality)
@@ -287,7 +273,8 @@
finally show ?thesis .
qed
-lemma mod_mult_right_eq: "(a * b) mod c = (a * (b mod c)) mod c"
+lemma mod_mult_right_eq: -- \<open>FIXME reorient\<close>
+ "(a * b) mod c = (a * (b mod c)) mod c"
proof -
have "(a * b) mod c = (a * (b div c * c + b mod c)) mod c"
by (simp only: mod_div_equality)
@@ -298,7 +285,8 @@
finally show ?thesis .
qed
-lemma mod_mult_eq: "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
+lemma mod_mult_eq: -- \<open>FIXME reorient\<close>
+ "(a * b) mod c = ((a mod c) * (b mod c)) mod c"
by (rule trans [OF mod_mult_left_eq mod_mult_right_eq])
lemma mod_mult_cong:
@@ -314,7 +302,7 @@
text \<open>Exponentiation respects modular equivalence.\<close>
-lemma power_mod: "(a mod b)^n mod b = a^n mod b"
+lemma power_mod: "(a mod b) ^ n mod b = a ^ n mod b"
apply (induct n, simp_all)
apply (rule mod_mult_right_eq [THEN trans])
apply (simp (no_asm_simp))
@@ -338,15 +326,6 @@
finally show ?thesis .
qed
-lemma div_mult_div_if_dvd:
- "y dvd x \<Longrightarrow> z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)"
- apply (cases "y = 0", simp)
- apply (cases "z = 0", simp)
- apply (auto elim!: dvdE simp add: algebra_simps)
- apply (subst mult.assoc [symmetric])
- apply (simp add: no_zero_divisors)
- done
-
lemma div_mult_mult2 [simp]:
"c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
by (drule div_mult_mult1) (simp add: mult.commute)
@@ -384,31 +363,6 @@
lemma dvd_mod_iff: "k dvd n \<Longrightarrow> k dvd (m mod n) \<longleftrightarrow> k dvd m"
by (blast intro: dvd_mod_imp_dvd dvd_mod)
-lemma div_power:
- "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
-apply (induct n)
- apply simp
-apply(simp add: div_mult_div_if_dvd dvd_power_same)
-done
-
-lemma dvd_div_eq_mult:
- assumes "a \<noteq> 0" and "a dvd b"
- shows "b div a = c \<longleftrightarrow> b = c * a"
-proof
- assume "b = c * a"
- then show "b div a = c" by (simp add: assms)
-next
- assume "b div a = c"
- then have "b div a * a = c * a" by simp
- moreover from \<open>a dvd b\<close> have "b div a * a = b" by simp
- ultimately show "b = c * a" by simp
-qed
-
-lemma dvd_div_div_eq_mult:
- assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
- shows "b div a = d div c \<longleftrightarrow> b * c = a * d"
- using assms by (auto simp add: mult.commute [of _ a] dvd_div_eq_mult div_mult_swap intro: sym)
-
end
class ring_div = comm_ring_1 + semiring_div
@@ -477,10 +431,9 @@
apply simp
done
-lemma div_diff[simp]:
- "\<lbrakk> z dvd x; z dvd y\<rbrakk> \<Longrightarrow> (x - y) div z = x div z - y div z"
-using div_add[where y = "- z" for z]
-by (simp add: dvd_neg_div)
+lemma div_diff [simp]:
+ "z dvd x \<Longrightarrow> z dvd y \<Longrightarrow> (x - y) div z = x div z - y div z"
+ using div_add [of _ _ "- y"] by (simp add: dvd_neg_div)
lemma div_minus_minus [simp]: "(-a) div (-b) = a div b"
using div_mult_mult1 [of "- 1" a b]
@@ -670,7 +623,7 @@
by (simp add: w_def div_mult2_eq mult_div_cancel ac_simps)
with \<open>w = 1\<close> have div: "2 * (a div (2 * b)) = a div b - 1" by simp
then show ?P and ?Q
- by (simp_all add: div mod add_implies_diff [symmetric] le_add_diff_inverse2)
+ by (simp_all add: div mod add_implies_diff [symmetric])
qed
lemma divmod_digit_0:
@@ -701,11 +654,11 @@
where
"divmod m n = (numeral m div numeral n, numeral m mod numeral n)"
-lemma fst_divmod [simp]:
+lemma fst_divmod:
"fst (divmod m n) = numeral m div numeral n"
by (simp add: divmod_def)
-lemma snd_divmod [simp]:
+lemma snd_divmod:
"snd (divmod m n) = numeral m mod numeral n"
by (simp add: divmod_def)
@@ -722,16 +675,11 @@
and evaluate accordingly.
\<close>
-lemma divmod_step_eq [code]:
+lemma divmod_step_eq [code, simp]:
"divmod_step l (q, r) = (if numeral l \<le> r
then (2 * q + 1, r - numeral l) else (2 * q, r))"
by (simp add: divmod_step_def)
-lemma divmod_step_simps [simp]:
- "r < numeral l \<Longrightarrow> divmod_step l (q, r) = (2 * q, r)"
- "numeral l \<le> r \<Longrightarrow> divmod_step l (q, r) = (2 * q + 1, r - numeral l)"
- by (auto simp add: divmod_step_eq not_le)
-
text \<open>
This is a formulation of school-method division.
If the divisor is smaller than the dividend, terminate.
@@ -740,13 +688,13 @@
opposite direction.
\<close>
-lemma divmod_divmod_step [code]:
+lemma divmod_divmod_step:
"divmod m n = (if m < n then (0, numeral m)
else divmod_step n (divmod m (Num.Bit0 n)))"
proof (cases "m < n")
case True then have "numeral m < numeral n" by simp
then show ?thesis
- by (simp add: prod_eq_iff div_less mod_less)
+ by (simp add: prod_eq_iff div_less mod_less fst_divmod snd_divmod)
next
case False
have "divmod m n =
@@ -754,10 +702,10 @@
numeral m mod (2 * numeral n))"
proof (cases "numeral n \<le> numeral m mod (2 * numeral n)")
case True
- with divmod_step_simps
+ with divmod_step_eq
have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
(2 * (numeral m div (2 * numeral n)) + 1, numeral m mod (2 * numeral n) - numeral n)"
- by blast
+ by simp
moreover from True divmod_digit_1 [of "numeral m" "numeral n"]
have "2 * (numeral m div (2 * numeral n)) + 1 = numeral m div numeral n"
and "numeral m mod (2 * numeral n) - numeral n = numeral m mod numeral n"
@@ -766,10 +714,10 @@
next
case False then have *: "numeral m mod (2 * numeral n) < numeral n"
by (simp add: not_le)
- with divmod_step_simps
+ with divmod_step_eq
have "divmod_step n (numeral m div (2 * numeral n), numeral m mod (2 * numeral n)) =
(2 * (numeral m div (2 * numeral n)), numeral m mod (2 * numeral n))"
- by blast
+ by auto
moreover from * divmod_digit_0 [of "numeral n" "numeral m"]
have "2 * (numeral m div (2 * numeral n)) = numeral m div numeral n"
and "numeral m mod (2 * numeral n) = numeral m mod numeral n"
@@ -785,10 +733,17 @@
with False show ?thesis by simp
qed
-lemma divmod_eq [simp]:
- "m < n \<Longrightarrow> divmod m n = (0, numeral m)"
- "n \<le> m \<Longrightarrow> divmod m n = divmod_step n (divmod m (Num.Bit0 n))"
- by (auto simp add: divmod_divmod_step [of m n])
+text \<open>The division rewrite proper – first, trivial results involving @{text 1}\<close>
+
+lemma divmod_trivial [simp, code]:
+ "divmod Num.One Num.One = (numeral Num.One, 0)"
+ "divmod (Num.Bit0 m) Num.One = (numeral (Num.Bit0 m), 0)"
+ "divmod (Num.Bit1 m) Num.One = (numeral (Num.Bit1 m), 0)"
+ "divmod num.One (num.Bit0 n) = (0, Numeral1)"
+ "divmod num.One (num.Bit1 n) = (0, Numeral1)"
+ using divmod_divmod_step [of "Num.One"] by (simp_all add: divmod_def)
+
+text \<open>Division by an even number is a right-shift\<close>
lemma divmod_cancel [simp, code]:
"divmod (Num.Bit0 m) (Num.Bit0 n) = (case divmod m n of (q, r) \<Rightarrow> (q, 2 * r))" (is ?P)
@@ -799,10 +754,26 @@
by (simp_all only: numeral_mult numeral.simps distrib) simp_all
have "1 div 2 = 0" "1 mod 2 = 1" by (auto intro: div_less mod_less)
then show ?P and ?Q
- by (simp_all add: prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
- div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2] add.commute del: numeral_times_numeral)
+ by (simp_all add: fst_divmod snd_divmod prod_eq_iff split_def * [of m] * [of n] mod_mult_mult1
+ div_mult2_eq [of _ _ 2] mod_mult2_eq [of _ _ 2]
+ add.commute del: numeral_times_numeral)
qed
+text \<open>The really hard work\<close>
+
+lemma divmod_steps [simp, code]:
+ "divmod (num.Bit0 m) (num.Bit1 n) =
+ (if m \<le> n then (0, numeral (num.Bit0 m))
+ else divmod_step (num.Bit1 n)
+ (divmod (num.Bit0 m)
+ (num.Bit0 (num.Bit1 n))))"
+ "divmod (num.Bit1 m) (num.Bit1 n) =
+ (if m < n then (0, numeral (num.Bit1 m))
+ else divmod_step (num.Bit1 n)
+ (divmod (num.Bit1 m)
+ (num.Bit0 (num.Bit1 n))))"
+ by (simp_all add: divmod_divmod_step)
+
text \<open>Special case: divisibility\<close>
definition divides_aux :: "'a \<times> 'a \<Rightarrow> bool"
@@ -817,6 +788,24 @@
"numeral m dvd numeral n \<longleftrightarrow> divides_aux (divmod n m)"
by (simp add: divmod_def mod_eq_0_iff_dvd)
+text \<open>Generic computation of quotient and remainder\<close>
+
+lemma numeral_div_numeral [simp]:
+ "numeral k div numeral l = fst (divmod k l)"
+ by (simp add: fst_divmod)
+
+lemma numeral_mod_numeral [simp]:
+ "numeral k mod numeral l = snd (divmod k l)"
+ by (simp add: snd_divmod)
+
+lemma one_div_numeral [simp]:
+ "1 div numeral n = fst (divmod num.One n)"
+ by (simp add: fst_divmod)
+
+lemma one_mod_numeral [simp]:
+ "1 mod numeral n = snd (divmod num.One n)"
+ by (simp add: snd_divmod)
+
end
@@ -1580,10 +1569,6 @@
by simp
qed
-lemma odd_Suc_minus_one [simp]:
- "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
- by (auto elim: oddE)
-
lemma parity_induct [case_names zero even odd]:
assumes zero: "P 0"
assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
@@ -2789,15 +2774,15 @@
lemma div_nat_numeral [simp]:
"(numeral v :: nat) div numeral v' = nat (numeral v div numeral v')"
- by (simp add: nat_div_distrib)
+ by (subst nat_div_distrib) simp_all
lemma one_div_nat_numeral [simp]:
"Suc 0 div numeral v' = nat (1 div numeral v')"
- by (subst nat_div_distrib, simp_all)
+ by (subst nat_div_distrib) simp_all
lemma mod_nat_numeral [simp]:
"(numeral v :: nat) mod numeral v' = nat (numeral v mod numeral v')"
- by (simp add: nat_mod_distrib)
+ by (subst nat_mod_distrib) simp_all
lemma one_mod_nat_numeral [simp]:
"Suc 0 mod numeral v' = nat (1 mod numeral v')"
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy Thu Aug 06 23:56:48 2015 +0200
@@ -240,6 +240,8 @@
instance fps :: (semiring_0_cancel) semiring_0_cancel ..
+instance fps :: (semiring_1) semiring_1 ..
+
subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close>
@@ -372,8 +374,9 @@
by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1
fps_const_add [symmetric])
-lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)"
- by (simp only: numeral_fps_const fps_const_neg)
+lemma neg_numeral_fps_const:
+ "(- numeral k :: 'a :: ring_1 fps) = fps_const (- numeral k)"
+ by (simp add: numeral_fps_const)
subsection \<open>The eXtractor series X\<close>
@@ -556,7 +559,7 @@
unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
by simp
then have "x > (1 / y)^k" using yp
- by (simp add: field_simps nonzero_power_divide)
+ by (simp add: field_simps)
then show ?thesis
using kp by blast
qed
@@ -2201,7 +2204,7 @@
from a0 b0 have ab0[simp]: "(a/b)$0 = a$0 / b$0"
by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def)
have th0: "r k ((a/b)$0) ^ k = (a/b)$0"
- by (simp add: \<open>?lhs\<close> nonzero_power_divide[OF rb0'] ra0 rb0)
+ by (simp add: \<open>?lhs\<close> power_divide ra0 rb0)
from a0 b0 ra0' rb0' kp \<open>?lhs\<close>
have th1: "r k ((a / b) $ 0) = (fps_radical r k a / fps_radical r k b) $ 0"
by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse)
@@ -2407,7 +2410,7 @@
lemma fps_compose_0[simp]: "0 oo a = 0"
by (simp add: fps_eq_iff fps_compose_nth)
-lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a$0)"
+lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a $ 0)"
by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum.neutral)
lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)"
--- a/src/HOL/Library/Poly_Deriv.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy Thu Aug 06 23:56:48 2015 +0200
@@ -175,7 +175,7 @@
next
show "\<not> [:- a, 1:] ^ Suc n' dvd pderiv ([:- a, 1:] ^ Suc n' * q)"
apply (subst lemma_order_pderiv1)
- by (metis * nd dvd_mult_cancel_right field_power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
+ by (metis * nd dvd_mult_cancel_right power_not_zero pCons_eq_0_iff power_Suc zero_neq_one)
qed
then show ?thesis
by (metis \<open>n = Suc n'\<close> pe)
--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML Thu Aug 06 23:56:48 2015 +0200
@@ -1045,7 +1045,7 @@
let
val simp_ctxt =
ctxt addsimps @{thms field_simps}
- addsimps [@{thm nonzero_power_divide}, @{thm power_divide}]
+ addsimps [@{thm power_divide}]
val th =
Thm.instantiate' [] [SOME d, SOME (Thm.dest_arg P)]
(if ord then @{lemma "(d=0 --> P) & (d>0 --> P) & (d<(0::real) --> P) ==> P" by auto}
--- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Thu Aug 06 23:56:48 2015 +0200
@@ -5257,7 +5257,7 @@
also have "\<dots> < e * inverse 2 * 2"
unfolding divide_inverse setsum_right_distrib[symmetric]
apply (rule mult_strict_left_mono)
- unfolding power_inverse lessThan_Suc_atMost[symmetric]
+ unfolding power_inverse [symmetric] lessThan_Suc_atMost[symmetric]
apply (subst geometric_sum)
using goal1
apply auto
@@ -9892,7 +9892,7 @@
show "(\<Sum>i = 0..s. e / 2 ^ (i + 2)) < e / 2"
unfolding power_add divide_inverse inverse_mult_distrib
unfolding setsum_right_distrib[symmetric] setsum_left_distrib[symmetric]
- unfolding power_inverse sum_gp
+ unfolding power_inverse [symmetric] sum_gp
apply(rule mult_strict_left_mono[OF _ e])
unfolding power2_eq_square
apply auto
--- a/src/HOL/NSA/HyperDef.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy Thu Aug 06 23:56:48 2015 +0200
@@ -441,12 +441,12 @@
lemma hyperpow_not_zero:
"\<And>r n. r \<noteq> (0::'a::{field} star) ==> r pow n \<noteq> 0"
-by transfer (rule field_power_not_zero)
+by transfer (rule power_not_zero)
lemma hyperpow_inverse:
"\<And>r n. r \<noteq> (0::'a::field star)
\<Longrightarrow> inverse (r pow n) = (inverse r) pow n"
-by transfer (rule power_inverse)
+by transfer (rule power_inverse [symmetric])
lemma hyperpow_hrabs:
"\<And>r n. abs (r::'a::{linordered_idom} star) pow n = abs (r pow n)"
--- a/src/HOL/NSA/NSComplex.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/NSComplex.thy Thu Aug 06 23:56:48 2015 +0200
@@ -377,19 +377,20 @@
by transfer simp
lemma hcpow_mult:
- "!!r s n. ((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
+ "((r::hcomplex) * s) pow n = (r pow n) * (s pow n)"
by (fact hyperpow_mult)
lemma hcpow_zero2 [simp]:
- "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
-by transfer (rule power_0_Suc)
+ "\<And>n. 0 pow (hSuc n) = (0::'a::semiring_1 star)"
+ by transfer (rule power_0_Suc)
lemma hcpow_not_zero [simp,intro]:
"!!r n. r \<noteq> 0 ==> r pow n \<noteq> (0::hcomplex)"
-by (rule hyperpow_not_zero)
+ by (fact hyperpow_not_zero)
-lemma hcpow_zero_zero: "r pow n = (0::hcomplex) ==> r = 0"
-by (blast intro: ccontr dest: hcpow_not_zero)
+lemma hcpow_zero_zero:
+ "r pow n = (0::hcomplex) ==> r = 0"
+ by (blast intro: ccontr dest: hcpow_not_zero)
subsection{*The Function @{term hsgn}*}
--- a/src/HOL/NSA/StarDef.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NSA/StarDef.thy Thu Aug 06 23:56:48 2015 +0200
@@ -688,7 +688,7 @@
star_inf_def [transfer_unfold]: "inf \<equiv> *f2* inf"
instance
- by default (transfer, auto)+
+ by (standard; transfer) auto
end
@@ -699,14 +699,14 @@
star_sup_def [transfer_unfold]: "sup \<equiv> *f2* sup"
instance
- by default (transfer, auto)+
+ by (standard; transfer) auto
end
instance star :: (lattice) lattice ..
instance star :: (distrib_lattice) distrib_lattice
- by default (transfer, auto simp add: sup_inf_distrib1)
+ by (standard; transfer) (auto simp add: sup_inf_distrib1)
lemma Standard_inf [simp]:
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> inf x y \<in> Standard"
@@ -775,6 +775,8 @@
apply (transfer, rule mult_1_right)
done
+instance star :: (power) power ..
+
instance star :: (comm_monoid_mult) comm_monoid_mult
by (intro_classes, transfer, rule mult_1)
@@ -843,6 +845,8 @@
instance star :: (semiring_no_zero_divisors) semiring_no_zero_divisors
by (intro_classes; transfer) (fact no_zero_divisors)
+instance star :: (semiring_1_no_zero_divisors) semiring_1_no_zero_divisors ..
+
instance star :: (semiring_no_zero_divisors_cancel) semiring_no_zero_divisors_cancel
by (intro_classes; transfer) simp_all
--- a/src/HOL/NthRoot.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/NthRoot.thy Thu Aug 06 23:56:48 2015 +0200
@@ -112,7 +112,7 @@
have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
using power_less_imp_less_base[of a n b] power_less_imp_less_base[of "-b" n "-a"]
- by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
+ by (simp add: sgn_real_def x [of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
qed
lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
@@ -130,7 +130,7 @@
by (auto simp add: order_le_less real_root_pow_pos)
lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x"
- by (auto split: split_root simp: sgn_real_def power_less_zero_eq)
+ by (auto split: split_root simp: sgn_real_def)
lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
@@ -496,7 +496,7 @@
done
lemma real_inv_sqrt_pow2: "0 < x ==> (inverse (sqrt x))\<^sup>2 = inverse x"
-by (simp add: power_inverse [symmetric])
+by (simp add: power_inverse)
lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
by simp
@@ -525,7 +525,7 @@
apply (cases "x = 0")
apply simp_all
using sqrt_divide_self_eq[of x]
- apply (simp add: inverse_eq_divide field_simps)
+ apply (simp add: field_simps)
done
lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
--- a/src/HOL/Parity.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Parity.thy Thu Aug 06 23:56:48 2015 +0200
@@ -195,6 +195,10 @@
shows "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
using even_abs_add_iff [of l k] by (simp add: ac_simps)
+lemma odd_Suc_minus_one [simp]:
+ "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
+ by (auto elim: oddE)
+
instance int :: ring_parity
proof
show "\<not> 2 dvd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
--- a/src/HOL/Power.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Power.thy Thu Aug 06 23:56:48 2015 +0200
@@ -9,6 +9,19 @@
imports Num Equiv_Relations
begin
+context linordered_ring (* TODO: move *)
+begin
+
+lemma sum_squares_ge_zero:
+ "0 \<le> x * x + y * y"
+ by (intro add_nonneg_nonneg zero_le_square)
+
+lemma not_sum_squares_lt_zero:
+ "\<not> x * x + y * y < 0"
+ by (simp add: not_less sum_squares_ge_zero)
+
+end
+
subsection \<open>Powers for Arbitrary Monoids\<close>
class power = one + times
@@ -186,6 +199,15 @@
lemma one_power2: "1\<^sup>2 = 1" (* delete? *)
by (rule power_one)
+lemma power_0_Suc [simp]:
+ "0 ^ Suc n = 0"
+ by simp
+
+text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
+lemma power_0_left:
+ "0 ^ n = (if n = 0 then 1 else 0)"
+ by (cases n) simp_all
+
end
context comm_semiring_1
@@ -229,6 +251,32 @@
end
+class semiring_1_no_zero_divisors = semiring_1 + semiring_no_zero_divisors
+begin
+
+subclass power .
+
+lemma power_eq_0_iff [simp]:
+ "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
+ by (induct n) auto
+
+lemma power_not_zero:
+ "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
+ by (induct n) auto
+
+lemma zero_eq_power2 [simp]:
+ "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
+ unfolding power2_eq_square by simp
+
+end
+
+context semidom
+begin
+
+subclass semiring_1_no_zero_divisors ..
+
+end
+
context ring_1
begin
@@ -252,7 +300,7 @@
lemma power2_minus [simp]:
"(- a)\<^sup>2 = a\<^sup>2"
- by (rule power_minus_Bit0)
+ by (fact power_minus_Bit0)
lemma power_minus1_even [simp]:
"(- 1) ^ (2*n) = 1"
@@ -272,29 +320,14 @@
end
-lemma power_eq_0_nat_iff [simp]:
- fixes m n :: nat
- shows "m ^ n = 0 \<longleftrightarrow> m = 0 \<and> n > 0"
- by (induct n) auto
-
context ring_1_no_zero_divisors
begin
-lemma power_eq_0_iff [simp]:
- "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
- by (induct n) auto
-
-lemma field_power_not_zero:
- "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
- by (induct n) auto
-
-lemma zero_eq_power2 [simp]:
- "a\<^sup>2 = 0 \<longleftrightarrow> a = 0"
- unfolding power2_eq_square by simp
+subclass semiring_1_no_zero_divisors ..
lemma power2_eq_1_iff:
"a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
- unfolding power2_eq_square by (rule square_eq_1_iff)
+ using square_eq_1_iff [of a] by (simp add: power2_eq_square)
end
@@ -306,6 +339,16 @@
end
+context algebraic_semidom
+begin
+
+lemma div_power:
+ assumes "b dvd a"
+ shows "(a div b) ^ n = a ^ n div b ^ n"
+ using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
+
+end
+
context normalization_semidom
begin
@@ -322,41 +365,42 @@
context division_ring
begin
-text \<open>FIXME reorient or rename to @{text nonzero_inverse_power}\<close>
-lemma nonzero_power_inverse:
- "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
- by (induct n)
- (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
+text\<open>Perhaps these should be simprules.\<close>
+lemma power_inverse [field_simps, divide_simps]:
+ "inverse a ^ n = inverse (a ^ n)"
+proof (cases "a = 0")
+ case True then show ?thesis by (simp add: power_0_left)
+next
+ case False then have "inverse (a ^ n) = inverse a ^ n"
+ by (induct n) (simp_all add: nonzero_inverse_mult_distrib power_commutes)
+ then show ?thesis by simp
+qed
-end
+lemma power_one_over [field_simps, divide_simps]:
+ "(1 / a) ^ n = 1 / a ^ n"
+ using power_inverse [of a] by (simp add: divide_inverse)
+
+end
context field
begin
-lemma nonzero_power_divide:
- "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
- by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
+lemma power_diff:
+ assumes nz: "a \<noteq> 0"
+ shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
+ by (induct m n rule: diff_induct) (simp_all add: nz power_not_zero)
-declare nonzero_power_divide [where b = "numeral w" for w, simp]
+lemma power_divide [field_simps, divide_simps]:
+ "(a / b) ^ n = a ^ n / b ^ n"
+ by (induct n) simp_all
+
+declare power_divide [where b = "numeral w" for w, simp]
end
subsection \<open>Exponentiation on ordered types\<close>
-context linordered_ring (* TODO: move *)
-begin
-
-lemma sum_squares_ge_zero:
- "0 \<le> x * x + y * y"
- by (intro add_nonneg_nonneg zero_le_square)
-
-lemma not_sum_squares_lt_zero:
- "\<not> x * x + y * y < 0"
- by (simp add: not_less sum_squares_ge_zero)
-
-end
-
context linordered_semidom
begin
@@ -702,12 +746,12 @@
subsection \<open>Miscellaneous rules\<close>
-lemma self_le_power:
- fixes x::"'a::linordered_semidom"
- shows "1 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x \<le> x ^ n"
- using power_increasing[of 1 n x] power_one_right[of x] by auto
+lemma (in linordered_semidom) self_le_power:
+ "1 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> a \<le> a ^ n"
+ using power_increasing [of 1 n a] power_one_right [of a] by auto
-lemma power_eq_if: "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
+lemma (in power) power_eq_if:
+ "p ^ m = (if m=0 then 1 else p * (p ^ (m - 1)))"
unfolding One_nat_def by (cases m) simp_all
lemma (in comm_semiring_1) power2_sum:
@@ -718,40 +762,6 @@
"(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
by (simp add: algebra_simps power2_eq_square mult_2_right)
-lemma power_0_Suc [simp]:
- "(0::'a::{power, semiring_0}) ^ Suc n = 0"
- by simp
-
-text\<open>It looks plausible as a simprule, but its effect can be strange.\<close>
-lemma power_0_left:
- "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
- by (induct n) simp_all
-
-lemma (in field) power_diff:
- assumes nz: "a \<noteq> 0"
- shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
- by (induct m n rule: diff_induct) (simp_all add: nz field_power_not_zero)
-
-text\<open>Perhaps these should be simprules.\<close>
-lemma power_inverse:
- fixes a :: "'a::division_ring"
- shows "inverse (a ^ n) = inverse a ^ n"
-apply (cases "a = 0")
-apply (simp add: power_0_left)
-apply (simp add: nonzero_power_inverse)
-done (* TODO: reorient or rename to inverse_power *)
-
-lemma power_one_over:
- "1 / (a::'a::{field, power}) ^ n = (1 / a) ^ n"
- by (simp add: divide_inverse) (rule power_inverse)
-
-lemma power_divide [field_simps, divide_simps]:
- "(a / b) ^ n = (a::'a::field) ^ n / b ^ n"
-apply (cases "b = 0")
-apply (simp add: power_0_left)
-apply (rule nonzero_power_divide)
-apply assumption
-done
text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
@@ -820,7 +830,7 @@
assume "\<not> m \<le> n"
then have "n < m" by simp
with assms Suc show False
- by (auto simp add: algebra_simps) (simp add: power2_eq_square)
+ by (simp add: power2_eq_square)
qed
qed
@@ -916,4 +926,3 @@
code_module Power \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
end
-
--- a/src/HOL/Rings.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Rings.thy Thu Aug 06 23:56:48 2015 +0200
@@ -633,6 +633,20 @@
"a div 1 = a"
using nonzero_mult_divide_cancel_left [of 1 a] by simp
+end
+
+class idom_divide = idom + semidom_divide
+
+class algebraic_semidom = semidom_divide
+begin
+
+text \<open>
+ Class @{class algebraic_semidom} enriches a integral domain
+ by notions from algebra, like units in a ring.
+ It is a separate class to avoid spoiling fields with notions
+ which are degenerated there.
+\<close>
+
lemma dvd_times_left_cancel_iff [simp]:
assumes "a \<noteq> 0"
shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
@@ -667,19 +681,60 @@
with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
qed
-end
+lemma div_dvd_div [simp]:
+ assumes "a dvd b" and "a dvd c"
+ shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
+proof (cases "a = 0")
+ case True with assms show ?thesis by simp
+next
+ case False
+ moreover from assms obtain k l where "b = a * k" and "c = a * l"
+ by (auto elim!: dvdE)
+ ultimately show ?thesis by simp
+qed
-class idom_divide = idom + semidom_divide
-
-class algebraic_semidom = semidom_divide
-begin
+lemma div_add [simp]:
+ assumes "c dvd a" and "c dvd b"
+ shows "(a + b) div c = a div c + b div c"
+proof (cases "c = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ moreover from assms obtain k l where "a = c * k" and "b = c * l"
+ by (auto elim!: dvdE)
+ moreover have "c * k + c * l = c * (k + l)"
+ by (simp add: algebra_simps)
+ ultimately show ?thesis
+ by simp
+qed
-text \<open>
- Class @{class algebraic_semidom} enriches a integral domain
- by notions from algebra, like units in a ring.
- It is a separate class to avoid spoiling fields with notions
- which are degenerated there.
-\<close>
+lemma div_mult_div_if_dvd:
+ assumes "b dvd a" and "d dvd c"
+ shows "(a div b) * (c div d) = (a * c) div (b * d)"
+proof (cases "b = 0 \<or> c = 0")
+ case True with assms show ?thesis by auto
+next
+ case False
+ moreover from assms obtain k l where "a = b * k" and "c = d * l"
+ by (auto elim!: dvdE)
+ moreover have "b * k * (d * l) div (b * d) = (b * d) * (k * l) div (b * d)"
+ by (simp add: ac_simps)
+ ultimately show ?thesis by simp
+qed
+
+lemma dvd_div_eq_mult:
+ assumes "a \<noteq> 0" and "a dvd b"
+ shows "b div a = c \<longleftrightarrow> b = c * a"
+proof
+ assume "b = c * a"
+ then show "b div a = c" by (simp add: assms)
+next
+ assume "b div a = c"
+ then have "b div a * a = c * a" by simp
+ moreover from \<open>a \<noteq> 0\<close> \<open>a dvd b\<close> have "b div a * a = b"
+ by (auto elim!: dvdE simp add: ac_simps)
+ ultimately show "b = c * a" by simp
+qed
lemma dvd_div_mult_self [simp]:
"a dvd b \<Longrightarrow> b div a * a = b"
@@ -716,6 +771,22 @@
by (cases "b = 0 \<or> c = 0") (auto, simp add: ac_simps)
qed
+lemma dvd_div_div_eq_mult:
+ assumes "a \<noteq> 0" "c \<noteq> 0" and "a dvd b" "c dvd d"
+ shows "b div a = d div c \<longleftrightarrow> b * c = a * d" (is "?P \<longleftrightarrow> ?Q")
+proof -
+ from assms have "a * c \<noteq> 0" by simp
+ then have "?P \<longleftrightarrow> b div a * (a * c) = d div c * (a * c)"
+ by simp
+ also have "\<dots> \<longleftrightarrow> (a * (b div a)) * c = (c * (d div c)) * a"
+ by (simp add: ac_simps)
+ also have "\<dots> \<longleftrightarrow> (a * b div a) * c = (c * d div c) * a"
+ using assms by (simp add: div_mult_swap)
+ also have "\<dots> \<longleftrightarrow> ?Q"
+ using assms by (simp add: ac_simps)
+ finally show ?thesis .
+qed
+
text \<open>Units: invertible elements in a ring\<close>
--- a/src/HOL/Series.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Series.thy Thu Aug 06 23:56:48 2015 +0200
@@ -550,7 +550,7 @@
fix n
show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n"
using r r0 M [of n]
- apply (auto simp add: abs_mult field_simps power_divide)
+ apply (auto simp add: abs_mult field_simps)
apply (cases "r=0", simp)
apply (cases n, auto)
done
--- a/src/HOL/Transcendental.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Transcendental.thy Thu Aug 06 23:56:48 2015 +0200
@@ -160,7 +160,7 @@
} note ** = this
show ?thesis using *
apply (rule summable_LIMSEQ_zero [OF summable_ratio_test, where N1="nat N"])
- apply (simp add: N0 norm_mult nat_le_iff field_simps power_Suc **
+ apply (simp add: N0 norm_mult field_simps **
del: of_nat_Suc real_of_int_add)
done
qed
@@ -737,7 +737,7 @@
by simp
then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ n)"
using False summable_mult2 [of "\<lambda>n. (of_nat (Suc n) * c(Suc n) * x ^ n) * x" "inverse x"]
- by (simp add: mult.assoc) (auto simp: power_Suc mult_ac)
+ by (simp add: mult.assoc) (auto simp: ac_simps)
then show ?thesis
by (simp add: diffs_def)
qed
@@ -1289,7 +1289,7 @@
lemma exp_of_nat_mult:
fixes x :: "'a::{real_normed_field,banach}"
shows "exp(of_nat n * x) = exp(x) ^ n"
- by (induct n) (auto simp add: power_Suc distrib_left exp_add mult.commute)
+ by (induct n) (auto simp add: distrib_left exp_add mult.commute)
corollary exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n"
by (simp add: exp_of_nat_mult real_of_nat_def)
@@ -1668,7 +1668,7 @@
hence "inverse (fact (n + 2)) \<le> inverse ((2::real) * 2 ^ n)"
by (rule le_imp_inverse_le) simp
hence "inverse (fact (n + 2)) \<le> 1/(2::real) * (1/2)^n"
- by (simp add: power_inverse)
+ by (simp add: power_inverse [symmetric])
hence "inverse (fact (n + 2)) * (x^n * x\<^sup>2) \<le> 1/2 * (1/2)^n * (1 * x\<^sup>2)"
by (rule mult_mono)
(rule mult_mono, simp_all add: power_le_one a b)
@@ -2309,9 +2309,7 @@
by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
lemma powr_realpow: "0 < x ==> x powr (real n) = x^n"
- apply (induct n)
- apply simp
- by (simp add: add.commute power.simps(2) powr_add real_of_nat_Suc)
+ by (induct n) (simp_all add: ac_simps powr_add real_of_nat_Suc)
lemma powr_realpow_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
unfolding real_of_nat_numeral [symmetric] by (rule powr_realpow)
@@ -3150,7 +3148,7 @@
by (simp add: inverse_eq_divide less_divide_eq)
}
then show ?thesis
- by (force intro!: sumr_pos_lt_pair [OF sm] simp add: power_Suc divide_inverse algebra_simps)
+ by (force intro!: sumr_pos_lt_pair [OF sm] simp add: divide_inverse algebra_simps)
qed
ultimately have "0 < (\<Sum>n. - ((- 1::real) ^ n * 2 ^ (2 * n) / (fact (2 * n))))"
by (rule order_less_trans)
@@ -4403,9 +4401,7 @@
shows "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
apply (rule power_inverse [THEN subst])
apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
- apply (auto dest: field_power_not_zero
- simp add: power_mult_distrib distrib_right power_divide tan_def
- mult.assoc power_inverse [symmetric])
+ apply (auto simp add: tan_def field_simps)
done
lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
@@ -4524,7 +4520,8 @@
apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
apply (rule DERIV_cong [OF DERIV_tan])
apply (rule cos_arctan_not_zero)
- apply (simp add: arctan power_inverse tan_sec [symmetric])
+ apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
+ apply (simp add: arctan power_inverse [symmetric] tan_sec [symmetric])
apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
done
@@ -5426,7 +5423,7 @@
unfolding Set_Interval.setsum_atMost_Suc_shift
by simp
also have "... = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
- by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc)
+ by (simp add: setsum_right_distrib ac_simps)
finally have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" .
}
then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
--- a/src/HOL/Word/Bit_Representation.thy Thu Aug 06 19:12:09 2015 +0200
+++ b/src/HOL/Word/Bit_Representation.thy Thu Aug 06 23:56:48 2015 +0200
@@ -104,7 +104,7 @@
"bin_last (numeral (Num.Bit1 w))"
"\<not> bin_last (- numeral (Num.Bit0 w))"
"bin_last (- numeral (Num.Bit1 w))"
- unfolding expand_BIT bin_last_BIT by (simp_all add: bin_last_def zmod_zminus1_eq_if)
+ by (simp_all add: bin_last_def zmod_zminus1_eq_if) (auto simp add: divmod_def)
lemma bin_rest_numeral_simps [simp]:
"bin_rest 0 = 0"
@@ -115,7 +115,7 @@
"bin_rest (numeral (Num.Bit1 w)) = numeral w"
"bin_rest (- numeral (Num.Bit0 w)) = - numeral w"
"bin_rest (- numeral (Num.Bit1 w)) = - numeral (w + Num.One)"
- unfolding expand_BIT bin_rest_BIT by (simp_all add: bin_rest_def zdiv_zminus1_eq_if)
+ by (simp_all add: bin_rest_def zdiv_zminus1_eq_if) (auto simp add: divmod_def)
lemma less_Bits:
"v BIT b < w BIT c \<longleftrightarrow> v < w \<or> v \<le> w \<and> \<not> b \<and> c"