Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
--- a/src/HOL/Archimedean_Field.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Archimedean_Field.thy Fri Nov 13 12:27:13 2015 +0000
@@ -152,7 +152,7 @@
shows "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
using floor_correct floor_unique by auto
-lemma of_int_floor_le: "of_int (floor x) \<le> x"
+lemma of_int_floor_le [simp]: "of_int (floor x) \<le> x"
using floor_correct ..
lemma le_floor_iff: "z \<le> floor x \<longleftrightarrow> of_int z \<le> x"
@@ -381,12 +381,12 @@
ceiling ("\<lceil>_\<rceil>")
lemma ceiling_correct: "of_int (ceiling x) - 1 < x \<and> x \<le> of_int (ceiling x)"
- unfolding ceiling_def using floor_correct [of "- x"] by simp
+ unfolding ceiling_def using floor_correct [of "- x"] by (simp add: le_minus_iff)
lemma ceiling_unique: "\<lbrakk>of_int z - 1 < x; x \<le> of_int z\<rbrakk> \<Longrightarrow> ceiling x = z"
unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp
-lemma le_of_int_ceiling: "x \<le> of_int (ceiling x)"
+lemma le_of_int_ceiling [simp]: "x \<le> of_int (ceiling x)"
using ceiling_correct ..
lemma ceiling_le_iff: "ceiling x \<le> z \<longleftrightarrow> x \<le> of_int z"
@@ -494,7 +494,7 @@
text \<open>Addition and subtraction of integers\<close>
lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
- using ceiling_correct [of x] by (simp add: ceiling_unique)
+ using ceiling_correct [of x] by (simp add: ceiling_def)
lemma ceiling_add_numeral [simp]:
"ceiling (x + numeral v) = ceiling x + numeral v"
--- a/src/HOL/Binomial.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Binomial.thy Fri Nov 13 12:27:13 2015 +0000
@@ -67,11 +67,11 @@
proof (induct n)
case (Suc n)
then have *: "fact n \<le> (of_nat (Suc n ^ n) ::'a)"
- by (rule order_trans) (simp add: power_mono)
+ by (rule order_trans) (simp add: power_mono del: of_nat_power)
have "fact (Suc n) = (of_nat (Suc n) * fact n ::'a)"
by (simp add: algebra_simps)
also have "... \<le> (of_nat (Suc n) * of_nat (Suc n ^ n) ::'a)"
- by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono)
+ by (simp add: "*" ordered_comm_semiring_class.comm_mult_left_mono del: of_nat_power)
also have "... \<le> (of_nat (Suc n ^ Suc n) ::'a)"
by (metis of_nat_mult order_refl power_Suc)
finally show ?case .
--- a/src/HOL/Complex.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Complex.thy Fri Nov 13 12:27:13 2015 +0000
@@ -842,7 +842,7 @@
by (simp add: cis_divide [symmetric] cis_2pi_int)
moreover have "- pi < c \<and> c \<le> pi"
using ceiling_correct [of "(b - pi) / (2*pi)"]
- by (simp add: c_def less_divide_eq divide_le_eq algebra_simps)
+ by (simp add: c_def less_divide_eq divide_le_eq algebra_simps del: le_of_int_ceiling)
ultimately show "\<exists>a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi" by fast
qed
--- a/src/HOL/Decision_Procs/Approximation.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri Nov 13 12:27:13 2015 +0000
@@ -808,7 +808,7 @@
also note float_round_up
finally have "pi / 2 - float_round_up prec (?ub_horner ?invx) \<le> arctan x"
using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
- unfolding real_sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto
+ unfolding sgn_pos[OF \<open>0 < 1 / real_of_float x\<close>] le_diff_eq by auto
moreover
have "lb_pi prec * Float 1 (- 1) \<le> pi / 2"
unfolding Float_num times_divide_eq_right mult_1_left using pi_boundaries by simp
@@ -935,7 +935,7 @@
unfolding one_float.rep_eq[symmetric] by (rule arctan_monotone') (rule float_divl)
finally have "arctan x \<le> pi / 2 - (?lb_horner ?invx)"
using \<open>0 \<le> arctan x\<close> arctan_inverse[OF \<open>1 / x \<noteq> 0\<close>]
- unfolding real_sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
+ unfolding sgn_pos[OF \<open>0 < 1 / x\<close>] le_diff_eq by auto
moreover
have "pi / 2 \<le> ub_pi prec * Float 1 (- 1)"
unfolding Float_num times_divide_eq_right mult_1_right
--- a/src/HOL/Decision_Procs/MIR.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Fri Nov 13 12:27:13 2015 +0000
@@ -35,12 +35,12 @@
hence th: "\<exists> k. x=real_of_int (i*k)" by (simp add: rdvd_def)
hence th': "real_of_int (floor x) = x" by (auto simp del: of_int_mult)
with th have "\<exists> k. real_of_int (floor x) = real_of_int (i*k)" by simp
- hence "\<exists> k. floor x = i*k" by blast
+ hence "\<exists> k. floor x = i*k" by presburger
thus ?r using th' by (simp add: dvd_def)
next
assume "?r" hence "(i::int) dvd \<lfloor>x::real\<rfloor>" ..
hence "\<exists> k. real_of_int (floor x) = real_of_int (i*k)"
- using dvd_def by blast
+ by (metis (no_types) dvd_def)
thus ?l using \<open>?r\<close> by (simp add: rdvd_def)
qed
@@ -123,7 +123,7 @@
let ?fe = "floor ?e"
assume be: "isint e bs" hence efe:"real_of_int ?fe = ?e" by (simp add: isint_iff)
have "real_of_int ((floor (Inum bs (Mul c e)))) = real_of_int (floor (real_of_int (c * ?fe)))" using efe by simp
- also have "\<dots> = real_of_int (c* ?fe)" using floor_of_int by blast
+ also have "\<dots> = real_of_int (c* ?fe)" by (metis floor_of_int)
also have "\<dots> = real_of_int c * ?e" using efe by simp
finally show ?thesis using isint_iff by simp
qed
@@ -1053,9 +1053,10 @@
"iff p q \<equiv> (if (p = q) then T else if (p = not q \<or> not p = q) then F else
if p=F then not q else if q=F then not p else if p=T then q else if q=T then p else
Iff p q)"
+
lemma iff[simp]: "Ifm bs (iff p q) = Ifm bs (Iff p q)"
- by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp)
-(cases "not p= q", auto simp add:not)
+ by (unfold iff_def,cases "p=q", simp,cases "p=not q", simp) (cases "not p= q", auto simp add:not)
+
lemma iff_qf[simp]: "\<lbrakk>qfree p ; qfree q\<rbrakk> \<Longrightarrow> qfree (iff p q)"
by (unfold iff_def,cases "p=q", auto)
@@ -2623,7 +2624,7 @@
hence "x + floor ?e +1 \<ge> 1 \<and> x + floor ?e + 1 \<le> d" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. j = x + floor ?e + 1" by simp
hence "\<exists> (j::int) \<in> {1 .. d}. x= - floor ?e - 1 + j" by (simp add: algebra_simps)
- hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by blast
+ hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= real_of_int (- floor ?e - 1 + j)" by presburger
hence "\<exists> (j::int) \<in> {1 .. d}. real_of_int x= - ?e - 1 + real_of_int j"
by (simp add: ie[simplified isint_iff])
with nob have ?case by simp }
--- a/src/HOL/Divides.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Divides.thy Fri Nov 13 12:27:13 2015 +0000
@@ -1696,17 +1696,14 @@
lemma divmod_int_rel:
"divmod_int_rel k l (k div l, k mod l)"
+ unfolding divmod_int_rel_def divide_int_def mod_int_def
apply (cases k rule: int_cases3)
- apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
+ apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
apply (cases l rule: int_cases3)
- apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
- apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
- apply (simp add: of_nat_add [symmetric])
- apply (simp add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
- apply (simp add: of_nat_add [symmetric])
+ apply (simp add: mod_greater_zero_iff_not_dvd not_le algebra_simps)
+ apply (simp_all del: of_nat_add of_nat_mult add: mod_greater_zero_iff_not_dvd not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
apply (cases l rule: int_cases3)
- apply (simp_all add: mod_greater_zero_iff_not_dvd not_le divmod_int_rel_def divide_int_def mod_int_def algebra_simps int_dvd_iff of_nat_mult [symmetric])
- apply (simp_all add: of_nat_add [symmetric])
+ apply (simp_all del: of_nat_add of_nat_mult add: not_le algebra_simps int_dvd_iff of_nat_add [symmetric] of_nat_mult [symmetric])
done
instantiation int :: ring_div
--- a/src/HOL/GCD.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/GCD.thy Fri Nov 13 12:27:13 2015 +0000
@@ -1133,10 +1133,7 @@
apply (erule subst)
apply (rule iffI)
apply force
- apply (drule_tac x = "abs e" for e in exI)
- apply (case_tac "e >= 0" for e :: int)
- apply force
- apply force
+ using abs_dvd_iff abs_ge_zero apply blast
done
lemma gcd_coprime_nat:
--- a/src/HOL/Inequalities.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Inequalities.thy Fri Nov 13 12:27:13 2015 +0000
@@ -34,7 +34,7 @@
by (auto simp: Setsum_Icc_int[transferred, OF assms] zdiv_int int_mult simp del: of_nat_setsum
split: zdiff_int_split)
thus ?thesis
- by blast
+ using int_int_eq by blast
qed
lemma Setsum_Ico_nat: assumes "(m::nat) \<le> n"
--- a/src/HOL/Int.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Int.thy Fri Nov 13 12:27:13 2015 +0000
@@ -319,25 +319,25 @@
text \<open>Comparisons involving @{term of_int}.\<close>
lemma of_int_eq_numeral_iff [iff]:
- "of_int z = (numeral n :: 'a::ring_char_0)
+ "of_int z = (numeral n :: 'a::ring_char_0)
\<longleftrightarrow> z = numeral n"
using of_int_eq_iff by fastforce
-lemma of_int_le_numeral_iff [simp]:
- "of_int z \<le> (numeral n :: 'a::linordered_idom)
+lemma of_int_le_numeral_iff [simp]:
+ "of_int z \<le> (numeral n :: 'a::linordered_idom)
\<longleftrightarrow> z \<le> numeral n"
using of_int_le_iff [of z "numeral n"] by simp
-lemma of_int_numeral_le_iff [simp]:
+lemma of_int_numeral_le_iff [simp]:
"(numeral n :: 'a::linordered_idom) \<le> of_int z \<longleftrightarrow> numeral n \<le> z"
using of_int_le_iff [of "numeral n"] by simp
-lemma of_int_less_numeral_iff [simp]:
- "of_int z < (numeral n :: 'a::linordered_idom)
+lemma of_int_less_numeral_iff [simp]:
+ "of_int z < (numeral n :: 'a::linordered_idom)
\<longleftrightarrow> z < numeral n"
using of_int_less_iff [of z "numeral n"] by simp
-lemma of_int_numeral_less_iff [simp]:
+lemma of_int_numeral_less_iff [simp]:
"(numeral n :: 'a::linordered_idom) < of_int z \<longleftrightarrow> numeral n < z"
using of_int_less_iff [of "numeral n" z] by simp
@@ -815,22 +815,22 @@
subsection \<open>@{term setsum} and @{term setprod}\<close>
-lemma of_nat_setsum: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
+lemma of_nat_setsum [simp]: "of_nat (setsum f A) = (\<Sum>x\<in>A. of_nat(f x))"
apply (cases "finite A")
apply (erule finite_induct, auto)
done
-lemma of_int_setsum: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
+lemma of_int_setsum [simp]: "of_int (setsum f A) = (\<Sum>x\<in>A. of_int(f x))"
apply (cases "finite A")
apply (erule finite_induct, auto)
done
-lemma of_nat_setprod: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
+lemma of_nat_setprod [simp]: "of_nat (setprod f A) = (\<Prod>x\<in>A. of_nat(f x))"
apply (cases "finite A")
apply (erule finite_induct, auto simp add: of_nat_mult)
done
-lemma of_int_setprod: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
+lemma of_int_setprod [simp]: "of_int (setprod f A) = (\<Prod>x\<in>A. of_int(f x))"
apply (cases "finite A")
apply (erule finite_induct, auto)
done
@@ -1401,7 +1401,7 @@
then show "x dvd y"
proof (cases k)
case (nonneg n)
- with A have "y = x * n" by (simp add: of_nat_mult [symmetric])
+ with A have "y = x * n" by (simp del: of_nat_mult add: of_nat_mult [symmetric])
then show ?thesis ..
next
case (neg n)
@@ -1695,16 +1695,6 @@
lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
-lemma zpower_zpower:
- "(x ^ y) ^ z = (x ^ (y * z)::int)"
- by (rule power_mult [symmetric])
-
-lemma int_power:
- "int (m ^ n) = int m ^ n"
- by (fact of_nat_power)
-
-lemmas zpower_int = int_power [symmetric]
-
text \<open>De-register @{text "int"} as a quotient type:\<close>
lifting_update int.lifting
--- a/src/HOL/Library/Float.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Library/Float.thy Fri Nov 13 12:27:13 2015 +0000
@@ -375,7 +375,7 @@
also have "\<dots> = m2 * 2^nat (e2 - e1)"
by (simp add: powr_realpow)
finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
- by blast
+ by linarith
with m1 have "m1 = m2"
by (cases "nat (e2 - e1)") (auto simp add: dvd_def)
then show ?thesis
@@ -526,8 +526,10 @@
ultimately have "real_of_int m = mantissa f * 2^nat (exponent f - e)"
by (simp add: powr_realpow[symmetric])
with \<open>e \<le> exponent f\<close>
- show "m = mantissa f * 2 ^ nat (exponent f - e)" "e = exponent f - nat (exponent f - e)"
- by force+
+ show "m = mantissa f * 2 ^ nat (exponent f - e)"
+ by linarith
+ show "e = exponent f - nat (exponent f - e)"
+ using `e \<le> exponent f` by auto
qed
context
@@ -1258,7 +1260,7 @@
case True
def x' \<equiv> "x * 2 ^ nat l"
have "int x * 2 ^ nat l = x'"
- by (simp add: x'_def int_mult int_power)
+ by (simp add: x'_def int_mult of_nat_power)
moreover have "real x * 2 powr l = real x'"
by (simp add: powr_realpow[symmetric] \<open>0 \<le> l\<close> x'_def)
ultimately show ?thesis
@@ -1271,7 +1273,7 @@
case False
def y' \<equiv> "y * 2 ^ nat (- l)"
from \<open>y \<noteq> 0\<close> have "y' \<noteq> 0" by (simp add: y'_def)
- have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult int_power)
+ have "int y * 2 ^ nat (- l) = y'" by (simp add: y'_def int_mult of_nat_power)
moreover have "real x * real_of_int (2::int) powr real_of_int l / real y = x / real y'"
using \<open>\<not> 0 \<le> l\<close>
by (simp add: powr_realpow[symmetric] powr_minus y'_def field_simps)
@@ -1554,7 +1556,7 @@
using bitlen_bounds[of "\<bar>m2\<bar>"]
by (auto simp: powr_add bitlen_nonneg)
then show ?thesis
- by (metis bitlen_nonneg powr_int real_of_int_abs real_of_int_less_numeral_power_cancel_iff zero_less_numeral)
+ by (metis bitlen_nonneg powr_int of_int_abs real_of_int_less_numeral_power_cancel_iff zero_less_numeral)
qed
lemma floor_sum_times_2_powr_sgn_eq:
@@ -1984,7 +1986,7 @@
by simp
also have "\<dots> \<le> 2 powr (bitlen \<bar>mantissa x\<bar>)"
using bitlen_bounds[of "\<bar>mantissa x\<bar>"] bitlen_nonneg \<open>mantissa x \<noteq> 0\<close>
- by (auto simp del: real_of_int_abs simp add: powr_int)
+ by (auto simp del: of_int_abs simp add: powr_int)
finally show ?thesis by (simp add: powr_add)
qed
--- a/src/HOL/Library/Formal_Power_Series.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy Fri Nov 13 12:27:13 2015 +0000
@@ -3787,10 +3787,8 @@
lemma binomial_Vandermonde:
"setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
- apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
- of_nat_setsum[symmetric] of_nat_add[symmetric])
- apply blast
- done
+ by (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric]
+ of_nat_setsum[symmetric] of_nat_add[symmetric] of_nat_eq_iff)
lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n"
using binomial_Vandermonde[of n n n, symmetric]
--- a/src/HOL/Library/Numeral_Type.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Library/Numeral_Type.thy Fri Nov 13 12:27:13 2015 +0000
@@ -376,7 +376,6 @@
lemma Abs_bit0'_code [code abstract]:
"Rep_bit0 (Abs_bit0' x :: 'a :: finite bit0) = x mod int (CARD('a bit0))"
by(auto simp add: Abs_bit0'_def intro!: Abs_bit0_inverse)
- (metis bit0.Rep_Abs_mod bit0.Rep_less_n card_bit0 of_nat_numeral zmult_int)
lemma inj_on_Abs_bit0:
"inj_on (Abs_bit0 :: int \<Rightarrow> 'a bit0) {0..<2 * int CARD('a :: finite)}"
@@ -389,8 +388,7 @@
lemma Abs_bit1'_code [code abstract]:
"Rep_bit1 (Abs_bit1' x :: 'a :: finite bit1) = x mod int (CARD('a bit1))"
-by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
- (metis of_nat_0_less_iff of_nat_Suc of_nat_mult of_nat_numeral pos_mod_conj zero_less_Suc)
+ by(auto simp add: Abs_bit1'_def intro!: Abs_bit1_inverse)
lemma inj_on_Abs_bit1:
"inj_on (Abs_bit1 :: int \<Rightarrow> 'a bit1) {0..<1 + 2 * int CARD('a :: finite)}"
@@ -414,7 +412,7 @@
instance
proof(intro_classes)
show "distinct (enum_class.enum :: 'a bit0 list)"
- by(auto intro!: inj_onI simp add: Abs_bit0'_def Abs_bit0_inject zmod_int[symmetric] enum_bit0_def distinct_map)
+ by (simp add: enum_bit0_def distinct_map inj_on_def Abs_bit0'_def Abs_bit0_inject mod_pos_pos_trivial)
show univ_eq: "(UNIV :: 'a bit0 set) = set enum_class.enum"
unfolding enum_bit0_def type_definition.Abs_image[OF type_definition_bit0, symmetric]
--- a/src/HOL/Limits.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Limits.thy Fri Nov 13 12:27:13 2015 +0000
@@ -89,7 +89,7 @@
lemma BfunE:
assumes "Bfun f F"
obtains B where "0 < B" and "eventually (\<lambda>x. norm (f x) \<le> B) F"
-using assms unfolding Bfun_def by fast
+using assms unfolding Bfun_def by blast
lemma Cauchy_Bseq: "Cauchy X \<Longrightarrow> Bseq X"
unfolding Cauchy_def Bfun_metric_def eventually_sequentially
@@ -175,7 +175,10 @@
ultimately have "\<forall>m. norm (X m) \<le> real (Suc n)"
by (blast intro: order_trans)
then show "\<exists>N. \<forall>n. norm (X n) \<le> real (Suc N)" ..
-qed (force simp add: of_nat_Suc)
+next
+ show "\<And>N. \<forall>n. norm (X n) \<le> real (Suc N) \<Longrightarrow> \<exists>K>0. \<forall>n. norm (X n) \<le> K"
+ using of_nat_0_less_iff by blast
+qed
text\<open>alternative definition for Bseq\<close>
lemma Bseq_iff: "Bseq X = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
@@ -367,7 +370,7 @@
fix r::real assume "0 < r"
hence "0 < r / K" using K by simp
then have "eventually (\<lambda>x. norm (f x) < r / K) F"
- using ZfunD [OF f] by fast
+ using ZfunD [OF f] by blast
with g show "eventually (\<lambda>x. norm (g x) < r) F"
proof eventually_elim
case (elim x)
@@ -433,7 +436,7 @@
shows "Zfun (\<lambda>x. f (g x)) F"
proof -
obtain K where "\<And>x. norm (f x) \<le> norm x * K"
- using bounded by fast
+ using bounded by blast
then have "eventually (\<lambda>x. norm (f (g x)) \<le> norm (g x) * K) F"
by simp
with g show ?thesis
@@ -448,7 +451,7 @@
fix r::real assume r: "0 < r"
obtain K where K: "0 < K"
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
- using pos_bounded by fast
+ using pos_bounded by blast
from K have K': "0 < inverse K"
by (rule positive_imp_inverse_positive)
have "eventually (\<lambda>x. norm (f x) < r) F"
@@ -787,7 +790,7 @@
proof -
obtain K where K: "0 \<le> K"
and norm_le: "\<And>x y. norm (x ** y) \<le> norm x * norm y * K"
- using nonneg_bounded by fast
+ using nonneg_bounded by blast
obtain B where B: "0 < B"
and norm_g: "eventually (\<lambda>x. norm (g x) \<le> B) F"
using g by (rule BfunE)
@@ -816,7 +819,7 @@
apply (rule scaleR_left)
apply (subst mult.commute)
using bounded
- apply fast
+ apply blast
done
lemma (in bounded_bilinear) Bfun_prod_Zfun:
@@ -840,9 +843,9 @@
proof -
from a have "0 < norm a" by simp
hence "\<exists>r>0. r < norm a" by (rule dense)
- then obtain r where r1: "0 < r" and r2: "r < norm a" by fast
+ then obtain r where r1: "0 < r" and r2: "r < norm a" by blast
have "eventually (\<lambda>x. dist (f x) a < r) F"
- using tendstoD [OF f r1] by fast
+ using tendstoD [OF f r1] by blast
hence "eventually (\<lambda>x. norm (inverse (f x)) \<le> inverse (norm a - r)) F"
proof eventually_elim
case (elim x)
@@ -911,7 +914,7 @@
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
shows "continuous_on s (\<lambda>x. inverse (f x))"
- using assms unfolding continuous_on_def by (fast intro: tendsto_inverse)
+ using assms unfolding continuous_on_def by (blast intro: tendsto_inverse)
lemma tendsto_divide [tendsto_intros]:
fixes a b :: "'a::real_normed_field"
@@ -941,7 +944,7 @@
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. g x \<noteq> 0"
shows "continuous_on s (\<lambda>x. (f x) / (g x))"
- using assms unfolding continuous_on_def by (fast intro: tendsto_divide)
+ using assms unfolding continuous_on_def by (blast intro: tendsto_divide)
lemma tendsto_sgn [tendsto_intros]:
fixes l :: "'a::real_normed_vector"
@@ -970,7 +973,7 @@
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
shows "continuous_on s (\<lambda>x. sgn (f x))"
- using assms unfolding continuous_on_def by (fast intro: tendsto_sgn)
+ using assms unfolding continuous_on_def by (blast intro: tendsto_sgn)
lemma filterlim_at_infinity:
fixes f :: "_ \<Rightarrow> 'a::real_normed_vector"
@@ -1685,7 +1688,7 @@
assumes "convergent (\<lambda>n. X n)"
assumes "convergent (\<lambda>n. Y n)"
shows "convergent (\<lambda>n. X n + Y n)"
- using assms unfolding convergent_def by (fast intro: tendsto_add)
+ using assms unfolding convergent_def by (blast intro: tendsto_add)
lemma convergent_setsum:
fixes X :: "'a \<Rightarrow> nat \<Rightarrow> 'b::real_normed_vector"
@@ -1699,12 +1702,12 @@
lemma (in bounded_linear) convergent:
assumes "convergent (\<lambda>n. X n)"
shows "convergent (\<lambda>n. f (X n))"
- using assms unfolding convergent_def by (fast intro: tendsto)
+ using assms unfolding convergent_def by (blast intro: tendsto)
lemma (in bounded_bilinear) convergent:
assumes "convergent (\<lambda>n. X n)" and "convergent (\<lambda>n. Y n)"
shows "convergent (\<lambda>n. X n ** Y n)"
- using assms unfolding convergent_def by (fast intro: tendsto)
+ using assms unfolding convergent_def by (blast intro: tendsto)
lemma convergent_minus_iff:
fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -1719,7 +1722,7 @@
assumes "convergent (\<lambda>n. X n)"
assumes "convergent (\<lambda>n. Y n)"
shows "convergent (\<lambda>n. X n - Y n)"
- using assms unfolding convergent_def by (fast intro: tendsto_diff)
+ using assms unfolding convergent_def by (blast intro: tendsto_diff)
lemma convergent_norm:
assumes "convergent f"
@@ -1757,7 +1760,7 @@
assumes "convergent (\<lambda>n. X n)"
assumes "convergent (\<lambda>n. Y n)"
shows "convergent (\<lambda>n. X n * Y n)"
- using assms unfolding convergent_def by (fast intro: tendsto_mult)
+ using assms unfolding convergent_def by (blast intro: tendsto_mult)
lemma convergent_mult_const_iff:
assumes "c \<noteq> 0"
@@ -2122,7 +2125,7 @@
proof (intro allI impI)
fix r::real assume r: "0 < r"
obtain K where K: "0 < K" and norm_le: "\<And>x. norm (f x) \<le> norm x * K"
- using pos_bounded by fast
+ using pos_bounded by blast
show "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
proof (rule exI, safe)
from r K show "0 < r / K" by simp
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Fri Nov 13 12:27:13 2015 +0000
@@ -2399,15 +2399,15 @@
by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arccos_body_lemma)
lemma Re_Arccos_bound: "abs(Re(Arccos z)) \<le> pi"
- using Re_Arccos_bounds abs_le_interval_iff less_eq_real_def by blast
+ by (meson Re_Arccos_bounds abs_le_iff less_eq_real_def minus_less_iff)
lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
unfolding Re_Arcsin
by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
lemma Re_Arcsin_bound: "abs(Re(Arcsin z)) \<le> pi"
- using Re_Arcsin_bounds abs_le_interval_iff less_eq_real_def by blast
-
+ by (meson Re_Arcsin_bounds abs_le_iff less_eq_real_def minus_less_iff)
+
subsection\<open>Interrelations between Arcsin and Arccos\<close>
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Fri Nov 13 12:27:13 2015 +0000
@@ -2139,7 +2139,7 @@
have *: "\<forall>n. \<exists>f f'. \<forall>x\<in>s.
(f has_derivative (f' x)) (at x within s) \<and>
(\<forall>h. norm(f' x h - g' x h) \<le> inverse (real (Suc n)) * norm h)"
- by (metis assms(2) inverse_positive_iff_positive real_of_nat_Suc_gt_zero)
+ by (simp add: assms(2))
obtain f where
*: "\<forall>x. \<exists>f'. \<forall>xa\<in>s. (f x has_derivative f' xa) (at xa within s) \<and>
(\<forall>h. norm (f' xa h - g' xa h) \<le> inverse (real (Suc x)) * norm h)"
@@ -2221,7 +2221,7 @@
have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
by (simp add: norm_mult [symmetric] ring_distribs setsum_left_distrib)
also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
- hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h"
+ hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h"
by (intro mult_right_mono) simp_all
finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
}
@@ -2245,9 +2245,9 @@
"\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
"\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
- from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
+ from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)"
by (simp add: at_within_interior[of x s])
- also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
+ also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow>
((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
@@ -2311,7 +2311,7 @@
qed
qed (insert f' f'', auto simp: has_vector_derivative_def)
then show ?thesis
- unfolding fun_eq_iff by auto
+ unfolding fun_eq_iff by (metis scaleR_one)
qed
lemma vector_derivative_unique_at:
@@ -2350,7 +2350,7 @@
intro: someI frechet_derivative_at [symmetric])
lemma has_real_derivative:
- fixes f :: "real \<Rightarrow> real"
+ fixes f :: "real \<Rightarrow> real"
assumes "(f has_derivative f') F"
obtains c where "(f has_real_derivative c) F"
proof -
@@ -2361,7 +2361,7 @@
qed
lemma has_real_derivative_iff:
- fixes f :: "real \<Rightarrow> real"
+ fixes f :: "real \<Rightarrow> real"
shows "(\<exists>c. (f has_real_derivative c) F) = (\<exists>D. (f has_derivative D) F)"
by (metis has_field_derivative_def has_real_derivative)
@@ -2390,7 +2390,7 @@
assumes "open s" and t: "t = closure s" "x \<in> t"
shows "x islimpt t"
proof cases
- assume "x \<in> s"
+ assume "x \<in> s"
{ fix T assume "x \<in> T" "open T"
then have "open (s \<inter> T)"
using \<open>open s\<close> by auto
@@ -2579,7 +2579,7 @@
by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto
hence "f y - f c \<le> (f x - f c) * ((c - y) / (c - x))" by simp
also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps)
- finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc
+ finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc
by (simp add: divide_simps)
qed
hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Fri Nov 13 12:27:13 2015 +0000
@@ -14,7 +14,8 @@
lemma cSup_abs_le: (* TODO: move to Conditionally_Complete_Lattices.thy? *)
fixes S :: "real set"
shows "S \<noteq> {} \<Longrightarrow> (\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a) \<Longrightarrow> \<bar>Sup S\<bar> \<le> a"
- by (auto simp add: abs_le_interval_iff intro: cSup_least) (metis cSup_upper2 bdd_aboveI)
+ apply (auto simp add: abs_le_iff intro: cSup_least)
+ by (metis bdd_aboveI cSup_upper neg_le_iff_le order_trans)
lemma cInf_abs_ge:
fixes S :: "real set"
--- a/src/HOL/NSA/NSA.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/NSA/NSA.thy Fri Nov 13 12:27:13 2015 +0000
@@ -1243,7 +1243,9 @@
apply (frule lemma_st_part1a)
apply (frule_tac [4] lemma_st_part2a, auto)
apply (drule order_le_imp_less_or_eq)+
-apply (auto dest: lemma_st_part_not_eq1 lemma_st_part_not_eq2 simp add: abs_less_iff)
+apply auto
+using lemma_st_part_not_eq2 apply fastforce
+using lemma_st_part_not_eq1 apply fastforce
done
lemma lemma_st_part_major2:
@@ -1252,6 +1254,7 @@
by (blast dest!: lemma_st_part_major)
+
text{*Existence of real and Standard Part Theorem*}
lemma lemma_st_part_Ex:
"(x::hypreal) \<in> HFinite
@@ -1778,7 +1781,7 @@
done
lemma st_SReal_eq: "x \<in> \<real> ==> st x = x"
- by (metis approx_refl st_unique)
+ by (metis approx_refl st_unique)
lemma st_hypreal_of_real [simp]: "st (hypreal_of_real x) = hypreal_of_real x"
by (rule SReal_hypreal_of_real [THEN st_SReal_eq])
@@ -2022,7 +2025,7 @@
lemma lemma_Infinitesimal:
"(\<forall>r. 0 < r --> x < r) = (\<forall>n. x < inverse(real (Suc n)))"
-apply (auto simp add: real_of_nat_Suc_gt_zero simp del: of_nat_Suc)
+apply (auto simp del: of_nat_Suc)
apply (blast dest!: reals_Archimedean intro: order_less_trans)
done
@@ -2031,10 +2034,8 @@
(\<forall>n. x < inverse(hypreal_of_nat (Suc n)))"
apply safe
apply (drule_tac x = "inverse (hypreal_of_real (real (Suc n))) " in bspec)
- apply (simp (no_asm_use))
- apply (rule real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive, THEN star_of_less [THEN iffD2], THEN [2] impE])
- prefer 2 apply assumption
- apply simp
+ apply simp_all
+ using less_imp_of_nat_less apply fastforce
apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: of_nat_Suc)
apply (drule star_of_less [THEN iffD2])
apply simp
@@ -2077,7 +2078,7 @@
by (auto simp add: lemma_real_le_Un_eq lemma_finite_omega_set finite_real_of_nat_less_real)
lemma finite_rabs_real_of_nat_le_real: "finite {n::nat. abs(real n) \<le> u}"
-apply (simp (no_asm) add: real_of_nat_Suc_gt_zero finite_real_of_nat_le_real)
+apply (simp (no_asm) add: finite_real_of_nat_le_real)
done
lemma rabs_real_of_nat_le_real_FreeUltrafilterNat:
@@ -2133,7 +2134,7 @@
apply (simp add: inverse_eq_divide)
apply (subst pos_less_divide_eq, assumption)
apply (subst pos_less_divide_eq)
- apply (simp add: real_of_nat_Suc_gt_zero)
+ apply simp
apply (simp add: mult.commute)
done
@@ -2153,7 +2154,7 @@
lemma finite_inverse_real_of_posnat_ge_real:
"0 < u ==> finite {n. u \<le> inverse(real(Suc n))}"
-by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
+by (auto simp add: lemma_real_le_Un_eq2 lemma_finite_epsilon_set finite_inverse_real_of_posnat_gt_real
simp del: of_nat_Suc)
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
@@ -2181,8 +2182,8 @@
lemma SEQ_Infinitesimal:
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
- real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
+by (simp add: hypnat_omega_def starfun_star_n star_n_inverse Infinitesimal_FreeUltrafilterNat_iff
+ FreeUltrafilterNat_inverse_real_of_posnat del: of_nat_Suc)
text{* Example where we get a hyperreal from a real sequence
for which a particular property holds. The theorem is
@@ -2198,7 +2199,7 @@
"\<forall>n. norm(X n - x) < inverse(real(Suc n))
==> star_n X - star_of x \<in> Infinitesimal"
unfolding star_n_diff star_of_def Infinitesimal_FreeUltrafilterNat_iff star_n_inverse
-by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
+by (auto dest!: FreeUltrafilterNat_inverse_real_of_posnat
intro: order_less_trans elim!: eventually_elim1)
lemma real_seq_to_hypreal_approx:
--- a/src/HOL/Nat.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Nat.thy Fri Nov 13 12:27:13 2015 +0000
@@ -1469,7 +1469,7 @@
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: ac_simps)
-lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
+lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
by (induct m) (simp_all add: ac_simps distrib_right)
lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
--- a/src/HOL/Nat_Transfer.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Nat_Transfer.thy Fri Nov 13 12:27:13 2015 +0000
@@ -203,11 +203,9 @@
lemma transfer_nat_int_sum_prod2:
"setsum f A = nat(setsum (%x. int (f x)) A)"
"setprod f A = nat(setprod (%x. int (f x)) A)"
- apply (subst int_setsum [symmetric])
- apply auto
- apply (subst int_setprod [symmetric])
- apply auto
-done
+ apply (simp only: int_setsum [symmetric] nat_int)
+ apply (simp only: int_setprod [symmetric] nat_int)
+ done
lemma transfer_nat_int_sum_prod_closure:
"nat_set A \<Longrightarrow> (!!x. x >= 0 \<Longrightarrow> f x >= (0::int)) \<Longrightarrow> setsum f A >= 0"
@@ -288,7 +286,7 @@
"(int x) * (int y) = int (x * y)"
"tsub (int x) (int y) = int (x - y)"
"(int x)^n = int (x^n)"
- by (auto simp add: int_mult tsub_def int_power)
+ by (auto simp add: int_mult tsub_def of_nat_power)
lemma transfer_int_nat_function_closures:
"is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
@@ -411,9 +409,7 @@
"(!!x. x:A \<Longrightarrow> is_nat (f x)) \<Longrightarrow>
setprod f A = int(setprod (%x. nat (f x)) A)"
unfolding is_nat_def
- apply (subst int_setsum, auto)
- apply (subst int_setprod, auto simp add: cong: setprod.cong)
-done
+ by (subst int_setsum) auto
declare transfer_morphism_int_nat [transfer add
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
--- a/src/HOL/NthRoot.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/NthRoot.thy Fri Nov 13 12:27:13 2015 +0000
@@ -257,7 +257,7 @@
have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
using n by (intro continuous_on_If continuous_intros) auto
then have "continuous_on UNIV ?f"
- by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
+ by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less sgn_neg le_less n)
then have [simp]: "\<And>x. isCont ?f x"
by (simp add: continuous_on_eq_continuous_at)
@@ -697,7 +697,7 @@
(simp_all add: at_infinity_eq_at_top_bot)
{ fix n :: nat assume "1 < n"
have "1 + x n * n = 1 + of_nat (n choose 1) * x n^1"
- using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp
+ using \<open>1 < n\<close> unfolding gbinomial_def binomial_gbinomial by simp
also have "\<dots> \<le> (\<Sum>k\<in>{0, 1}. of_nat (n choose k) * x n^k)"
by (simp add: x_def)
also have "\<dots> \<le> (\<Sum>k=0..n. of_nat (n choose k) * x n^k)"
@@ -741,8 +741,4 @@
lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
-(* needed for CauchysMeanTheorem.het_base from AFP *)
-lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
-by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
-
end
--- a/src/HOL/Number_Theory/Fib.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Number_Theory/Fib.thy Fri Nov 13 12:27:13 2015 +0000
@@ -51,7 +51,7 @@
lemma fib_Cassini_nat:
"fib (Suc (Suc n)) * fib n =
(if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
- using fib_Cassini_int [of n] by auto
+ using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power)
subsection \<open>Law 6.111 of Concrete Mathematics\<close>
--- a/src/HOL/Old_Number_Theory/Euler.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Old_Number_Theory/Euler.thy Fri Nov 13 12:27:13 2015 +0000
@@ -284,7 +284,7 @@
apply (metis zprime_zOdd_eq_grt_2)
apply (frule aux__1, auto)
apply (drule_tac z = "nat ((p - 1) div 2)" in zcong_zpower)
- apply (auto simp add: zpower_zpower)
+ apply (auto simp add: power_mult [symmetric])
apply (rule zcong_trans)
apply (auto simp add: zcong_sym [of "x ^ nat ((p - 1) div 2)"])
apply (metis Little_Fermat even_div_2_prop2 odd_minus_one_even mult_1 aux__2)
--- a/src/HOL/Old_Number_Theory/EvenOdd.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Old_Number_Theory/EvenOdd.thy Fri Nov 13 12:27:13 2015 +0000
@@ -176,7 +176,7 @@
finally have "(-1::int)^nat x = (-1)^(2 * nat a)"
by simp
also have "... = (-1::int)\<^sup>2 ^ nat a"
- by (simp add: zpower_zpower [symmetric])
+ by (simp add: power_mult)
also have "(-1::int)\<^sup>2 = 1"
by simp
finally show ?thesis
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Fri Nov 13 12:27:13 2015 +0000
@@ -133,7 +133,7 @@
5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a"
apply (unfold inv_def)
apply (subst power_mod)
- apply (subst zpower_zpower)
+ apply (subst power_mult [symmetric])
apply (rule zcong_zless_imp_eq)
prefer 5
apply (subst zcong_zmod)
--- a/src/HOL/Power.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Power.thy Fri Nov 13 12:27:13 2015 +0000
@@ -175,7 +175,7 @@
context semiring_1
begin
-lemma of_nat_power:
+lemma of_nat_power [simp]:
"of_nat (m ^ n) = of_nat m ^ n"
by (induct n) (simp_all add: of_nat_mult)
@@ -310,7 +310,7 @@
lemma power_minus1_odd:
"(- 1) ^ Suc (2*n) = -1"
by simp
-
+
lemma power_minus_even [simp]:
"(-a) ^ (2*n) = a ^ (2*n)"
by (simp add: power_minus [of a])
@@ -320,7 +320,7 @@
context ring_1_no_zero_divisors
begin
-subclass semiring_1_no_zero_divisors ..
+subclass semiring_1_no_zero_divisors ..
lemma power2_eq_1_iff:
"a\<^sup>2 = 1 \<longleftrightarrow> a = 1 \<or> a = - 1"
@@ -377,7 +377,7 @@
"(1 / a) ^ n = 1 / a ^ n"
using power_inverse [of a] by (simp add: divide_inverse)
-end
+end
context field
begin
@@ -463,6 +463,10 @@
qed
qed
+lemma of_nat_zero_less_power_iff [simp]:
+ "of_nat x ^ n > 0 \<longleftrightarrow> x > 0 \<or> n = 0"
+ by (induct n) auto
+
text\<open>Surely we can strengthen this? It holds for @{text "0<a<1"} too.\<close>
lemma power_inject_exp [simp]:
"1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
@@ -491,7 +495,7 @@
proof (induct N)
case 0 then show ?case by simp
next
- case (Suc N) then show ?case
+ case (Suc N) then show ?case
apply (auto simp add: power_Suc_less less_Suc_eq)
apply (subgoal_tac "a * a^N < 1 * a^n")
apply simp
@@ -505,7 +509,7 @@
proof (induct N)
case 0 then show ?case by simp
next
- case (Suc N) then show ?case
+ case (Suc N) then show ?case
apply (auto simp add: le_Suc_eq)
apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp)
apply (rule mult_mono) apply auto
@@ -522,7 +526,7 @@
proof (induct N)
case 0 then show ?case by simp
next
- case (Suc N) then show ?case
+ case (Suc N) then show ?case
apply (auto simp add: le_Suc_eq)
apply (subgoal_tac "1 * a^n \<le> a * a^N", simp)
apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one])
@@ -539,7 +543,7 @@
proof (induct N)
case 0 then show ?case by simp
next
- case (Suc N) then show ?case
+ case (Suc N) then show ?case
apply (auto simp add: power_less_power_Suc less_Suc_eq)
apply (subgoal_tac "1 * a^n < a * a^N", simp)
apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
@@ -552,7 +556,7 @@
lemma power_strict_increasing_iff [simp]:
"1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
-by (blast intro: power_less_imp_less_exp power_strict_increasing)
+by (blast intro: power_less_imp_less_exp power_strict_increasing)
lemma power_le_imp_le_base:
assumes le: "a ^ Suc n \<le> b ^ Suc n"
@@ -680,7 +684,7 @@
lemma odd_0_le_power_imp_0_le:
"0 \<le> a ^ Suc (2*n) \<Longrightarrow> 0 \<le> a"
using odd_power_less_zero [of a n]
- by (force simp add: linorder_not_less [symmetric])
+ by (force simp add: linorder_not_less [symmetric])
lemma zero_le_even_power'[simp]:
"0 \<le> a ^ (2*n)"
@@ -689,7 +693,7 @@
show ?case by simp
next
case (Suc n)
- have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
+ have "a ^ (2 * Suc n) = (a*a) * a ^ (2*n)"
by (simp add: ac_simps power_add power2_eq_square)
thus ?case
by (simp add: Suc zero_le_mult_iff)
@@ -733,7 +737,7 @@
lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
by (auto simp add: abs_if power2_eq_1_iff)
-
+
lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
using abs_square_eq_1 [of x] abs_square_le_1 [of x]
by (auto simp add: le_less)
@@ -768,10 +772,10 @@
lemmas zero_compare_simps =
add_strict_increasing add_strict_increasing2 add_increasing
- zero_le_mult_iff zero_le_divide_iff
- zero_less_mult_iff zero_less_divide_iff
- mult_le_0_iff divide_le_0_iff
- mult_less_0_iff divide_less_0_iff
+ zero_le_mult_iff zero_le_divide_iff
+ zero_less_mult_iff zero_less_divide_iff
+ mult_le_0_iff divide_le_0_iff
+ mult_less_0_iff divide_less_0_iff
zero_le_power2 power2_less_0
@@ -785,7 +789,7 @@
"x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0"
by (induct n) auto
-lemma nat_power_eq_Suc_0_iff [simp]:
+lemma nat_power_eq_Suc_0_iff [simp]:
"x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
by (induct m) auto
@@ -842,13 +846,13 @@
lemma card_Pow: "finite A \<Longrightarrow> card (Pow A) = 2 ^ card A"
proof (induct rule: finite_induct)
- case empty
+ case empty
show ?case by auto
next
case (insert x A)
- then have "inj_on (insert x) (Pow A)"
+ then have "inj_on (insert x) (Pow A)"
unfolding inj_on_def by (blast elim!: equalityE)
- then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
+ then have "card (Pow A) + card (insert x ` Pow A) = 2 * 2 ^ card A"
by (simp add: mult_2 card_image Pow_insert insert.hyps)
then show ?case using insert
apply (simp add: Pow_insert)
@@ -882,11 +886,11 @@
lemma setprod_power_distrib:
fixes f :: "'a \<Rightarrow> 'b::comm_semiring_1"
shows "setprod f A ^ n = setprod (\<lambda>x. (f x) ^ n) A"
-proof (cases "finite A")
- case True then show ?thesis
+proof (cases "finite A")
+ case True then show ?thesis
by (induct A rule: finite_induct) (auto simp add: power_mult_distrib)
next
- case False then show ?thesis
+ case False then show ?thesis
by simp
qed
@@ -902,13 +906,13 @@
{assume a: "a \<notin> S"
hence "\<forall> k\<in> S. ?f k = c" by simp
hence ?thesis using a setprod_constant[OF fS, of c] by simp }
- moreover
+ moreover
{assume a: "a \<in> S"
let ?A = "S - {a}"
let ?B = "{a}"
- have eq: "S = ?A \<union> ?B" using a by blast
+ have eq: "S = ?A \<union> ?B" using a by blast
have dj: "?A \<inter> ?B = {}" by simp
- from fS have fAB: "finite ?A" "finite ?B" by auto
+ from fS have fAB: "finite ?A" "finite ?B" by auto
have fA0:"setprod ?f ?A = setprod (\<lambda>i. c) ?A"
apply (rule setprod.cong) by auto
have cA: "card ?A = card S - 1" using fS a by auto
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Fri Nov 13 12:27:13 2015 +0000
@@ -471,7 +471,7 @@
using entropy_le_card[of "t\<circ>OB", OF simple_distributedI[OF simple_function_finite refl]] by simp
also have "\<dots> \<le> log b (real (n + 1)^card observations)"
using card_T_bound not_empty
- by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: of_nat_power of_nat_Suc)
+ by (auto intro!: log_le simp: card_gt_0_iff of_nat_power [symmetric] simp del: of_nat_power of_nat_Suc)
also have "\<dots> = real (card observations) * log b (real n + 1)"
by (simp add: log_nat_power add.commute)
finally show ?thesis .
--- a/src/HOL/Real.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Real.thy Fri Nov 13 12:27:13 2015 +0000
@@ -114,7 +114,7 @@
proof (rule vanishesI)
fix r :: rat assume r: "0 < r"
obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
- using X by fast
+ using X by blast
obtain b where b: "0 < b" "r = a * b"
proof
show "0 < r / a" using r a by simp
@@ -217,9 +217,9 @@
then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
by (rule obtain_pos_sum)
obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
- using cauchy_imp_bounded [OF X] by fast
+ using cauchy_imp_bounded [OF X] by blast
obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"
- using cauchy_imp_bounded [OF Y] by fast
+ using cauchy_imp_bounded [OF Y] by blast
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
proof
show "0 < v/b" using v b(1) by simp
@@ -259,7 +259,7 @@
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
using cauchyD [OF X s] ..
obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"
- using r by fast
+ using r by blast
have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"
using i \<open>i \<le> k\<close> by auto
have "X k \<le> - r \<or> r \<le> X k"
@@ -285,7 +285,7 @@
proof (rule cauchyI)
fix r :: rat assume "0 < r"
obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
- using cauchy_not_vanishes [OF X nz] by fast
+ using cauchy_not_vanishes [OF X nz] by blast
from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
proof
@@ -317,9 +317,9 @@
proof (rule vanishesI)
fix r :: rat assume r: "0 < r"
obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
- using cauchy_not_vanishes [OF X] by fast
+ using cauchy_not_vanishes [OF X] by blast
obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
- using cauchy_not_vanishes [OF Y] by fast
+ using cauchy_not_vanishes [OF Y] by blast
obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
proof
show "0 < a * r * b"
@@ -372,7 +372,7 @@
done
lemma part_equivp_realrel: "part_equivp realrel"
- by (fast intro: part_equivpI symp_realrel transp_realrel
+ by (blast intro: part_equivpI symp_realrel transp_realrel
realrel_refl cauchy_const)
subsection \<open>The field of real numbers\<close>
@@ -527,7 +527,7 @@
unfolding realrel_def by simp_all
assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
- by fast
+ by blast
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
using \<open>0 < r\<close> by (rule obtain_pos_sum)
obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
@@ -539,7 +539,7 @@
using i j n by simp_all
thus "t < Y n" unfolding r by simp
qed
- hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast
+ hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by blast
} note 1 = this
fix X Y assume "realrel X Y"
hence "realrel X Y" and "realrel Y X"
@@ -579,7 +579,8 @@
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
apply transfer
apply (simp add: realrel_def)
-apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
+apply (drule (1) cauchy_not_vanishes_cases, safe)
+apply blast+
done
instantiation real :: linordered_field
@@ -781,7 +782,7 @@
finally have "of_int (floor (x - 1)) < x" .
hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
then show "\<not> P (of_int (floor (x - 1)))"
- unfolding P_def of_rat_of_int_eq using x by fast
+ unfolding P_def of_rat_of_int_eq using x by blast
qed
obtain b where b: "P b"
proof
@@ -810,7 +811,7 @@
have width: "\<And>n. B n - A n = (b - a) / 2^n"
apply (simp add: eq_divide_eq)
apply (induct_tac n, simp)
- apply (simp add: C_def avg_def power_Suc algebra_simps)
+ apply (simp add: C_def avg_def algebra_simps)
done
have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
@@ -902,7 +903,7 @@
proof (rule vanishesI)
fix r :: rat assume "0 < r"
then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
- using twos by fast
+ using twos by blast
have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
proof (clarify)
fix n assume n: "k \<le> n"
@@ -1022,17 +1023,20 @@
declare [[coercion_map "\<lambda>f g (x,y). (f x, g y)"]]
declare of_int_eq_0_iff [algebra, presburger]
-declare of_int_eq_iff [iff, algebra, presburger] (*FIXME*)
-declare of_int_eq_iff [iff, algebra, presburger] (*FIXME*)
-declare of_int_less_iff [iff, algebra, presburger] (*FIXME*)
-declare of_int_le_iff [iff, algebra, presburger] (*FIXME*)
+declare of_int_eq_1_iff [algebra, presburger]
+declare of_int_eq_iff [algebra, presburger]
+declare of_int_less_0_iff [algebra, presburger]
+declare of_int_less_1_iff [algebra, presburger]
+declare of_int_less_iff [algebra, presburger]
+declare of_int_le_0_iff [algebra, presburger]
+declare of_int_le_1_iff [algebra, presburger]
+declare of_int_le_iff [algebra, presburger]
+declare of_int_0_less_iff [algebra, presburger]
+declare of_int_0_le_iff [algebra, presburger]
+declare of_int_1_less_iff [algebra, presburger]
+declare of_int_1_le_iff [algebra, presburger]
-declare of_int_0_less_iff [presburger]
-declare of_int_0_le_iff [presburger]
-declare of_int_less_0_iff [presburger]
-declare of_int_le_0_iff [presburger]
-
-lemma real_of_int_abs [simp]: "real_of_int (abs x) = abs(real_of_int x)"
+lemma of_int_abs [simp]: "of_int (abs x) = (abs(of_int x) :: 'a::linordered_idom)"
by (auto simp add: abs_if)
lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
@@ -1086,29 +1090,9 @@
subsection\<open>Embedding the Naturals into the Reals\<close>
-declare of_nat_less_iff [iff] (*FIXME*)
-declare of_nat_le_iff [iff] (*FIXME*)
-declare of_nat_0_le_iff [iff] (*FIXME*)
-declare of_nat_less_iff [iff] (*FIXME*)
-declare of_nat_less_iff [iff] (*FIXME*)
-
-lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" (*NEEDED?*)
- using of_nat_0_less_iff by blast
-
-declare of_nat_mult [simp] (*FIXME*)
-declare of_nat_power [simp] (*FIXME*)
-
-lemmas power_real_of_nat = of_nat_power [symmetric]
-
-declare of_nat_setsum [simp] (*FIXME*)
-declare of_nat_setprod [simp] (*FIXME*)
-
lemma real_of_card: "real (card A) = setsum (\<lambda>x.1) A"
by simp
-declare of_nat_eq_iff [iff] (*FIXME*)
-declare of_nat_eq_0_iff [iff] (*FIXME*)
-
lemma nat_less_real_le: "(n < m) = (real n + 1 \<le> real m)"
by (metis discrete of_nat_1 of_nat_add of_nat_le_iff)
@@ -1151,9 +1135,6 @@
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
by (insert real_of_nat_div2 [of n x], simp)
-lemma of_nat_nat [simp]: "0 <= x ==> real(nat x) = real x"
- by force
-
subsection \<open>The Archimedean Property of the Reals\<close>
lemmas reals_Archimedean = ex_inverse_of_nat_Suc_less (*FIXME*)
@@ -1276,7 +1257,7 @@
by (simp add: divide_less_eq diff_less_eq \<open>0 < q\<close>
less_ceiling_iff [symmetric])
moreover from r_def have "r \<in> \<rat>" by simp
- ultimately show ?thesis by fast
+ ultimately show ?thesis by blast
qed
lemma of_rat_dense:
@@ -1294,8 +1275,6 @@
"real_of_int (- numeral k) = - numeral k"
by simp_all
-
- (*FIXME*)
declaration \<open>
K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2]
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *)
@@ -1329,9 +1308,6 @@
subsection \<open>Lemmas about powers\<close>
-text \<open>FIXME: declare this in Rings.thy or not at all\<close>
-declare abs_mult_self [simp]
-
(* used by Import/HOL/real.imp *)
lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
by simp
@@ -1440,10 +1416,6 @@
lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
by (simp add: abs_if)
-(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)
-lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
-by (force simp add: abs_le_iff)
-
lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
by (simp add: abs_if)
--- a/src/HOL/Real_Vector_Spaces.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Nov 13 12:27:13 2015 +0000
@@ -1062,7 +1062,7 @@
subclass topological_space
proof
have "\<exists>e::real. 0 < e"
- by (fast intro: zero_less_one)
+ by (blast intro: zero_less_one)
then show "open UNIV"
unfolding open_dist by simp
next
@@ -1076,7 +1076,7 @@
done
next
fix K assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)"
- unfolding open_dist by fast
+ unfolding open_dist by (meson UnionE UnionI)
qed
lemma open_ball: "open {y. dist x y < d}"
@@ -1260,26 +1260,14 @@
by (simp add: sgn_div_norm norm_mult mult.commute)
lemma real_sgn_eq: "sgn (x::real) = x / \<bar>x\<bar>"
-by (simp add: sgn_div_norm divide_inverse)
-
-lemma real_sgn_pos: "0 < (x::real) \<Longrightarrow> sgn x = 1"
-unfolding real_sgn_eq by simp
-
-lemma real_sgn_neg: "(x::real) < 0 \<Longrightarrow> sgn x = -1"
-unfolding real_sgn_eq by simp
+ by (simp add: sgn_div_norm divide_inverse)
lemma zero_le_sgn_iff [simp]: "0 \<le> sgn x \<longleftrightarrow> 0 \<le> (x::real)"
by (cases "0::real" x rule: linorder_cases) simp_all
-lemma zero_less_sgn_iff [simp]: "0 < sgn x \<longleftrightarrow> 0 < (x::real)"
- by (cases "0::real" x rule: linorder_cases) simp_all
-
lemma sgn_le_0_iff [simp]: "sgn x \<le> 0 \<longleftrightarrow> (x::real) \<le> 0"
by (cases "0::real" x rule: linorder_cases) simp_all
-lemma sgn_less_0_iff [simp]: "sgn x < 0 \<longleftrightarrow> (x::real) < 0"
- by (cases "0::real" x rule: linorder_cases) simp_all
-
lemma norm_conv_dist: "norm x = dist x 0"
unfolding dist_norm by simp
@@ -1321,7 +1309,7 @@
"\<exists>K>0. \<forall>x. norm (f x) \<le> norm x * K"
proof -
obtain K where K: "\<And>x. norm (f x) \<le> norm x * K"
- using bounded by fast
+ using bounded by blast
show ?thesis
proof (intro exI impI conjI allI)
show "0 < max 1 K"
@@ -1351,7 +1339,7 @@
assumes "\<And>r x. f (scaleR r x) = scaleR r (f x)"
assumes "\<And>x. norm (f x) \<le> norm x * K"
shows "bounded_linear f"
- by standard (fast intro: assms)+
+ by standard (blast intro: assms)+
locale bounded_bilinear =
fixes prod :: "['a::real_normed_vector, 'b::real_normed_vector]
@@ -1481,9 +1469,9 @@
by (simp only: f.scaleR g.scaleR)
next
from f.pos_bounded
- obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by fast
+ obtain Kf where f: "\<And>x. norm (f x) \<le> norm x * Kf" and Kf: "0 < Kf" by blast
from g.pos_bounded
- obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by fast
+ obtain Kg where g: "\<And>x. norm (g x) \<le> norm x * Kg" by blast
show "\<exists>K. \<forall>x. norm (f (g x)) \<le> norm x * K"
proof (intro exI allI)
fix x
@@ -1735,7 +1723,7 @@
proof (intro allI impI)
fix e :: real assume e: "e > 0"
with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
- unfolding Cauchy_def by fast
+ unfolding Cauchy_def by blast
thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
qed
qed
@@ -1783,9 +1771,9 @@
show "\<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m) (X n) < e"
proof (intro exI allI impI)
fix m assume "N \<le> m"
- hence m: "dist (X m) a < e/2" using N by fast
+ hence m: "dist (X m) a < e/2" using N by blast
fix n assume "N \<le> n"
- hence n: "dist (X n) a < e/2" using N by fast
+ hence n: "dist (X n) a < e/2" using N by blast
have "dist (X m) (X n) \<le> dist (X m) a + dist (X n) a"
by (rule dist_triangle2)
also from m n have "\<dots> < e" by simp
@@ -1805,7 +1793,7 @@
lemma Cauchy_convergent_iff:
fixes X :: "nat \<Rightarrow> 'a::complete_space"
shows "Cauchy X = convergent X"
-by (fast intro: Cauchy_convergent convergent_Cauchy)
+by (blast intro: Cauchy_convergent convergent_Cauchy)
subsection \<open>The set of real numbers is a complete metric space\<close>
@@ -1881,11 +1869,11 @@
hence N: "\<forall>n\<ge>N. X N - r/2 < X n \<and> X n < X N + r/2"
by (simp only: dist_real_def abs_diff_less_iff)
- from N have "\<forall>n\<ge>N. X N - r/2 < X n" by fast
+ from N have "\<forall>n\<ge>N. X N - r/2 < X n" by blast
hence "X N - r/2 \<in> S" by (rule mem_S)
hence 1: "X N - r/2 \<le> Sup S" by (simp add: cSup_upper)
- from N have "\<forall>n\<ge>N. X n < X N + r/2" by fast
+ from N have "\<forall>n\<ge>N. X n < X N + r/2" by blast
from bound_isUb[OF this]
have 2: "Sup S \<le> X N + r/2"
by (intro cSup_least) simp_all
@@ -1953,7 +1941,7 @@
using ex_le_of_nat[of x] ..
note monoD[OF mono this]
also have "f (real_of_nat n) \<le> y"
- by (rule LIMSEQ_le_const[OF limseq]) (auto intro: exI[of _ n] monoD[OF mono])
+ by (rule LIMSEQ_le_const[OF limseq]) (auto intro!: exI[of _ n] monoD[OF mono])
finally have "f x \<le> y" . }
note le = this
have "eventually (\<lambda>x. real N \<le> x) at_top"
--- a/src/HOL/Rings.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Rings.thy Fri Nov 13 12:27:13 2015 +0000
@@ -1976,7 +1976,7 @@
"\<bar>a * b\<bar> = \<bar>a\<bar> * \<bar>b\<bar>"
by (rule abs_eq_mult) auto
-lemma abs_mult_self:
+lemma abs_mult_self [simp]:
"\<bar>a\<bar> * \<bar>a\<bar> = a * a"
by (simp add: abs_if)
--- a/src/HOL/Transcendental.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Transcendental.thy Fri Nov 13 12:27:13 2015 +0000
@@ -10,13 +10,6 @@
imports Binomial Series Deriv NthRoot
begin
-lemma reals_Archimedean4:
- assumes "0 < y" "0 \<le> x"
- obtains n where "real n * y \<le> x" "x < real (Suc n) * y"
- using floor_correct [of "x/y"] assms
- apply (auto simp: field_simps intro!: that [of "nat (floor (x/y))"])
-by (metis (no_types, hide_lams) divide_inverse divide_self_if floor_correct mult.left_commute mult.right_neutral mult_eq_0_iff order_refl order_trans real_mult_le_cancel_iff2)
-
lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
@@ -3556,6 +3549,14 @@
done
qed
+
+lemma reals_Archimedean4:
+ assumes "0 < y" "0 \<le> x"
+ obtains n where "real n * y \<le> x" "x < real (Suc n) * y"
+ using floor_correct [of "x/y"] assms
+ apply (auto simp: field_simps intro!: that [of "nat (floor (x/y))"])
+by (metis (no_types, hide_lams) divide_inverse divide_self_if floor_correct mult.left_commute mult.right_neutral mult_eq_0_iff order_refl order_trans real_mult_le_cancel_iff2)
+
lemma cos_zero_lemma:
"\<lbrakk>0 \<le> x; cos x = 0\<rbrakk> \<Longrightarrow>
\<exists>n::nat. odd n & x = real n * (pi/2)"
@@ -4399,7 +4400,7 @@
by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
lemma arcsin_eq_iff: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
- by (metis abs_le_interval_iff arcsin)
+ by (metis abs_le_iff arcsin minus_le_iff)
lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
using arcsin_lt_bounded cos_gt_zero_pi by force
--- a/src/HOL/Word/Word.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Word/Word.thy Fri Nov 13 12:27:13 2015 +0000
@@ -960,7 +960,7 @@
apply auto
apply (erule_tac nat_less_iff [THEN iffD2])
apply (rule_tac [2] zless_nat_eq_int_zless [THEN iffD1])
- apply (auto simp add : nat_power_eq int_power)
+ apply (auto simp add : nat_power_eq of_nat_power)
done
lemma unats_uints: "unats n = nat ` uints n"
@@ -1901,7 +1901,7 @@
lemma Abs_fnat_hom_mult:
"of_nat a * of_nat b = (of_nat (a * b) :: 'a :: len word)"
- by (simp add: word_of_nat wi_hom_mult zmult_int)
+ by (simp add: word_of_nat wi_hom_mult)
lemma Abs_fnat_hom_Suc:
"word_succ (of_nat a) = of_nat (Suc a)"
@@ -2125,9 +2125,7 @@
"(i :: 'a :: len word) <= k div x \<Longrightarrow> uint i * uint x < 2 ^ len_of TYPE('a)"
apply (unfold uint_nat)
apply (drule div_lt')
- apply (simp add: zmult_int zless_nat_eq_int_zless [symmetric]
- nat_power_eq)
- done
+ by (metis of_nat_less_iff of_nat_mult of_nat_numeral of_nat_power)
lemmas div_lt_uint'' = order_less_imp_le [THEN div_lt_uint']
@@ -2156,22 +2154,14 @@
lemmas thd = refl [THEN [2] split_div_lemma [THEN iffD2], THEN conjunct1]
-lemma thd1:
- "a div b * b \<le> (a::nat)"
- using gt_or_eq_0 [of b]
- apply (rule disjE)
- apply (erule xtr4 [OF thd mult.commute])
- apply clarsimp
- done
-
-lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend thd1
+lemmas uno_simps [THEN le_unat_uoi] = mod_le_divisor div_le_dividend dtle
lemma word_mod_div_equality:
"(n div b) * b + (n mod b) = (n :: 'a :: len word)"
apply (unfold word_less_nat_alt word_arith_nat_defs)
apply (cut_tac y="unat b" in gt_or_eq_0)
apply (erule disjE)
- apply (simp add: mod_div_equality uno_simps)
+ apply (simp only: mod_div_equality uno_simps Word.word_unat.Rep_inverse)
apply simp
done
@@ -2179,7 +2169,7 @@
apply (unfold word_le_nat_alt word_arith_nat_defs)
apply (cut_tac y="unat b" in gt_or_eq_0)
apply (erule disjE)
- apply (simp add: div_mult_le uno_simps)
+ apply (simp only: div_mult_le uno_simps Word.word_unat.Rep_inverse)
apply simp
done
@@ -3305,7 +3295,7 @@
apply (unfold dvd_def)
apply auto
apply (drule uint_ge_0 [THEN nat_int.Abs_inverse' [simplified], symmetric])
- apply (simp add : int_mult int_power)
+ apply (simp add : int_mult of_nat_power)
apply (simp add : nat_mult_distrib nat_power_eq)
done
@@ -4653,15 +4643,7 @@
"1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
apply (simp add: word_rec_def unat_word_ariths)
apply (subst nat_mod_eq')
- apply (cut_tac x=n in unat_lt2p)
- apply (drule Suc_mono)
- apply (simp add: less_Suc_eq_le)
- apply (simp only: order_less_le, simp)
- apply (erule contrapos_pn, simp)
- apply (drule arg_cong[where f=of_nat])
- apply simp
- apply (subst (asm) word_unat.Rep_inverse[of n])
- apply simp
+ apply (metis Suc_eq_plus1_left Suc_lessI of_nat_2p unat_1 unat_lt2p word_arith_nat_add)
apply simp
done
--- a/src/HOL/ex/Sqrt.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/ex/Sqrt.thy Fri Nov 13 12:27:13 2015 +0000
@@ -26,7 +26,7 @@
by (auto simp add: power2_eq_square)
also have "(sqrt p)\<^sup>2 = p" by simp
also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
- finally show ?thesis ..
+ finally show ?thesis using of_nat_eq_iff by blast
qed
have "p dvd m \<and> p dvd n"
proof
@@ -69,7 +69,7 @@
by (auto simp add: power2_eq_square)
also have "(sqrt p)\<^sup>2 = p" by simp
also have "\<dots> * n\<^sup>2 = p * n\<^sup>2" by simp
- finally have eq: "m\<^sup>2 = p * n\<^sup>2" ..
+ finally have eq: "m\<^sup>2 = p * n\<^sup>2" using of_nat_eq_iff by blast
then have "p dvd m\<^sup>2" ..
with \<open>prime p\<close> have dvd_m: "p dvd m" by (rule prime_dvd_power_nat)
then obtain k where "m = p * k" ..
--- a/src/HOL/ex/Sum_of_Powers.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/ex/Sum_of_Powers.thy Fri Nov 13 12:27:13 2015 +0000
@@ -175,7 +175,7 @@
from sum_of_squares have "real (6 * (\<Sum>k\<le>n. k ^ 2)) = real (2 * n ^ 3 + 3 * n ^ 2 + n)"
by (auto simp add: field_simps)
then have "6 * (\<Sum>k\<le>n. k ^ 2) = 2 * n ^ 3 + 3 * n ^ 2 + n"
- by blast
+ using of_nat_eq_iff by blast
then show ?thesis by auto
qed
@@ -197,7 +197,7 @@
from sum_of_cubes have "real (4 * (\<Sum>k\<le>n. k ^ 3)) = real ((n ^ 2 + n) ^ 2)"
by (auto simp add: field_simps)
then have "4 * (\<Sum>k\<le>n. k ^ 3) = (n ^ 2 + n) ^ 2"
- by blast
+ using of_nat_eq_iff by blast
then show ?thesis by auto
qed
--- a/src/HOL/ex/Transfer_Int_Nat.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/ex/Transfer_Int_Nat.thy Fri Nov 13 12:27:13 2015 +0000
@@ -46,7 +46,7 @@
unfolding rel_fun_def ZN_def tsub_def by (simp add: zdiff_int)
lemma ZN_power [transfer_rule]: "(ZN ===> op = ===> ZN) (op ^) (op ^)"
- unfolding rel_fun_def ZN_def by (simp add: int_power)
+ unfolding rel_fun_def ZN_def by (simp add: of_nat_power)
lemma ZN_nat_id [transfer_rule]: "(ZN ===> op =) nat id"
unfolding rel_fun_def ZN_def by simp