--- a/src/HOL/MacLaurin.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/MacLaurin.thy Wed Sep 30 16:36:42 2015 +0100
@@ -430,16 +430,16 @@
apply (cut_tac f = sin and n = n and x = x
and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
apply safe
-apply (simp (no_asm))
-apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: derivative_eq_intros)
-apply (subst (asm) setsum.neutral, auto)[1]
-apply (rule ccontr, simp)
-apply (drule_tac x = x in spec, simp)
+ apply (simp)
+ apply (simp add: sin_expansion_lemma del: real_of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ apply (subst (asm) setsum.neutral, auto)[1]
+ apply (rule ccontr, simp)
+ apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
+apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: real_of_nat_Suc)
done
lemma Maclaurin_sin_expansion:
@@ -458,13 +458,13 @@
+ ((sin(t + 1/2 * real(n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: derivative_eq_intros)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
+ apply simp
+ apply (simp (no_asm) add: sin_expansion_lemma del: real_of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ apply (erule ssubst)
+ apply (rule_tac x = t in exI, simp)
+ apply (rule setsum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: real_of_nat_Suc)
done
lemma Maclaurin_sin_expansion4:
@@ -475,13 +475,13 @@
+ ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: sin_expansion_lemma)
-apply (force intro!: derivative_eq_intros)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
-apply (rule setsum.cong[OF refl])
-apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE)
+ apply simp
+ apply (simp (no_asm) add: sin_expansion_lemma del: real_of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ apply (erule ssubst)
+ apply (rule_tac x = t in exI, simp)
+ apply (rule setsum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: real_of_nat_Suc)
done
@@ -502,10 +502,10 @@
+ ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
apply safe
-apply (simp (no_asm))
-apply (simp (no_asm) add: cos_expansion_lemma)
-apply (case_tac "n", simp)
-apply (simp del: setsum_lessThan_Suc)
+ apply (simp (no_asm))
+ apply (simp (no_asm) add: cos_expansion_lemma del: real_of_nat_Suc)
+ apply (case_tac "n", simp)
+ apply (simp del: setsum_lessThan_Suc)
apply (rule ccontr, simp)
apply (drule_tac x = x in spec, simp)
apply (erule ssubst)
@@ -522,10 +522,10 @@
+ ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: cos_expansion_lemma)
-apply (erule ssubst)
-apply (rule_tac x = t in exI, simp)
+ apply simp
+ apply (simp (no_asm) add: cos_expansion_lemma del: real_of_nat_Suc)
+ apply (erule ssubst)
+ apply (rule_tac x = t in exI, simp)
apply (rule setsum.cong[OF refl])
apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
done
@@ -538,8 +538,8 @@
+ ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
apply safe
-apply simp
-apply (simp (no_asm) add: cos_expansion_lemma)
+ apply simp
+ apply (simp (no_asm) add: cos_expansion_lemma del: real_of_nat_Suc)
apply (erule ssubst)
apply (rule_tac x = t in exI, simp)
apply (rule setsum.cong[OF refl])
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Sep 30 16:36:42 2015 +0100
@@ -1742,7 +1742,7 @@
have "(\<Sum>i\<in>Basis. \<bar>real (r (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(1)[OF b'_im]
- apply (auto simp add:* field_simps)
+ apply (auto simp add:* field_simps simp del: real_of_nat_Suc)
done
also have "\<dots> < e * real p"
using p \<open>e > 0\<close> \<open>p > 0\<close>
@@ -1754,7 +1754,7 @@
have "(\<Sum>i\<in>Basis. \<bar>real (s (b' i)) - real (q (b' i))\<bar>) \<le> (\<Sum>(i::'a)\<in>Basis. 1)"
apply (rule setsum_mono)
using rs(2)[OF b'_im]
- apply (auto simp add:* field_simps)
+ apply (auto simp add:* field_simps simp del: real_of_nat_Suc)
done
also have "\<dots> < e * real p"
using p \<open>e > 0\<close> \<open>p > 0\<close>
--- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Sep 30 16:36:42 2015 +0100
@@ -3030,7 +3030,7 @@
path_integral (linepath (h (n/N)) (g (n/N))) f = 0"
using path_integral_unique [OF pi0] Suc.prems
by (simp add: g h fpa valid_path_subpath path_integrable_subpath
- fpa1 fpa2 fpa3 algebra_simps)
+ fpa1 fpa2 fpa3 algebra_simps del: real_of_nat_Suc)
have *: "\<And>hn he hn' gn gd gn' hgn ghn gh0 ghn'.
\<lbrakk>hn - gn = ghn - gh0;
gd + ghn' + he + hgn = (0::complex);
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 30 16:36:42 2015 +0100
@@ -560,7 +560,7 @@
lemma real_arch_inv: "0 < e \<longleftrightarrow> (\<exists>n::nat. n \<noteq> 0 \<and> 0 < inverse (real n) \<and> inverse (real n) < e)"
using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
- by (auto simp add: field_simps cong: conj_cong)
+ by (auto simp add: field_simps cong: conj_cong simp del: real_of_nat_Suc)
text\<open>Bernoulli's inequality\<close>
lemma Bernoulli_inequality:
@@ -654,9 +654,7 @@
(\<And>n. P (inverse (real (Suc n)))) \<Longrightarrow> 0 < e \<Longrightarrow> P e"
apply (rule forall_pos_mono)
apply auto
- apply (atomize)
- apply (erule_tac x="n - 1" in allE)
- apply auto
+ apply (metis Suc_pred real_of_nat_Suc)
done
lemma real_archimedian_rdiv_eq_0:
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Sep 30 16:36:42 2015 +0100
@@ -6597,8 +6597,7 @@
then have "\<exists>N::nat. inverse (real (N + 1)) < e"
using real_arch_inv[of e]
apply (auto simp add: Suc_pred')
- apply (rule_tac x="n - 1" in exI)
- apply auto
+ apply (metis Suc_pred' real_of_nat_Suc)
done
then obtain N :: nat where "inverse (real (N + 1)) < e"
by auto
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Wed Sep 30 16:36:42 2015 +0100
@@ -664,9 +664,9 @@
apply simp
done
also have "... \<le> j*e + e*(n - j + 1)*e/n "
- using \<open>1 \<le> n\<close> e by (simp add: field_simps)
+ using \<open>1 \<le> n\<close> e by (simp add: field_simps del: real_of_nat_Suc)
also have "... \<le> j*e + e*e"
- using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps)
+ using \<open>1 \<le> n\<close> e j1 by (simp add: field_simps del: real_of_nat_Suc)
also have "... < (j + 1/3)*e"
using e by (auto simp: field_simps)
finally have gj1: "g t < (j + 1 / 3) * e" .
--- a/src/HOL/NSA/HSEQ.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/NSA/HSEQ.thy Wed Sep 30 16:36:42 2015 +0100
@@ -225,11 +225,11 @@
by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_zero)
lemma NSLIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----NS> 0"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat)
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat del: real_of_nat_Suc)
lemma NSLIMSEQ_inverse_real_of_nat_add:
"(%n. r + inverse(real(Suc n))) ----NS> r"
-by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add)
+by (simp add: LIMSEQ_NSLIMSEQ_iff [symmetric] LIMSEQ_inverse_real_of_nat_add del: real_of_nat_Suc)
lemma NSLIMSEQ_inverse_real_of_nat_add_minus:
"(%n. r + -inverse(real(Suc n))) ----NS> r"
--- a/src/HOL/NSA/HyperDef.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy Wed Sep 30 16:36:42 2015 +0100
@@ -266,7 +266,7 @@
lemma not_ex_hypreal_of_real_eq_epsilon: "~ (\<exists>x. hypreal_of_real x = epsilon)"
by (auto simp add: epsilon_def star_of_def star_n_eq_iff
- lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite])
+ lemma_finite_epsilon_set [THEN FreeUltrafilterNat.finite] simp del: real_of_nat_Suc)
lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
by (insert not_ex_hypreal_of_real_eq_epsilon, auto)
--- a/src/HOL/NSA/NSA.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/NSA/NSA.thy Wed Sep 30 16:36:42 2015 +0100
@@ -2025,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)
+apply (auto simp add: real_of_nat_Suc_gt_zero simp del: real_of_nat_Suc)
apply (blast dest!: reals_Archimedean intro: order_less_trans)
done
@@ -2033,12 +2033,12 @@
"(\<forall>r \<in> Reals. 0 < r --> x < r) =
(\<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 add: real_of_nat_def)
-apply (auto dest!: reals_Archimedean simp add: SReal_iff)
+ 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 add: real_of_nat_def)
+apply (auto dest!: reals_Archimedean simp add: SReal_iff simp del: real_of_nat_Suc)
apply (drule star_of_less [THEN iffD2])
apply (simp add: real_of_nat_def)
apply (blast intro: order_less_trans)
@@ -2148,7 +2148,7 @@
lemma finite_inverse_real_of_posnat_gt_real:
"0 < u ==> finite {n. u < inverse(real(Suc n))}"
-apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff)
+apply (simp (no_asm_simp) add: real_of_nat_less_inverse_iff del: real_of_nat_Suc)
apply (simp (no_asm_simp) add: real_of_nat_Suc less_diff_eq [symmetric])
apply (rule finite_real_of_nat_less_real)
done
@@ -2161,7 +2161,8 @@
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: real_of_nat_Suc)
lemma inverse_real_of_posnat_ge_real_FreeUltrafilterNat:
"0 < u ==> \<not> eventually (\<lambda>n. u \<le> inverse(real(Suc n))) FreeUltrafilterNat"
@@ -2188,10 +2189,8 @@
lemma SEQ_Infinitesimal:
"( *f* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"
-apply (simp add: hypnat_omega_def starfun_star_n star_n_inverse)
-apply (simp add: Infinitesimal_FreeUltrafilterNat_iff)
-apply (simp add: real_of_nat_Suc_gt_zero FreeUltrafilterNat_inverse_real_of_posnat)
-done
+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: real_of_nat_Suc)
text{* Example where we get a hyperreal from a real sequence
for which a particular property holds. The theorem is
--- a/src/HOL/Probability/Borel_Space.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Wed Sep 30 16:36:42 2015 +0100
@@ -618,7 +618,7 @@
interpret sigma_algebra UNIV ?SIGMA
by (intro sigma_algebra_sigma_sets) simp_all
have *: "?set = (\<Union>n. UNIV - {x::'a. x \<bullet> i < a + 1 / real (Suc n)})"
- proof (safe, simp_all add: not_less)
+ proof (safe, simp_all add: not_less del: real_of_nat_Suc)
fix x :: 'a assume "a < x \<bullet> i"
with reals_Archimedean[of "x \<bullet> i - a"]
obtain n where "a + 1 / real (Suc n) < x \<bullet> i"
@@ -655,7 +655,7 @@
fix a :: real and i :: 'a assume "(a, i) \<in> UNIV \<times> Basis"
then have i: "i \<in> Basis" by auto
have *: "{x::'a. x\<bullet>i < a} = (\<Union>n. {x. x\<bullet>i \<le> a - 1/real (Suc n)})"
- proof (safe, simp_all)
+ proof (safe, simp_all del: real_of_nat_Suc)
fix x::'a assume *: "x\<bullet>i < a"
with reals_Archimedean[of "a - x\<bullet>i"]
obtain n where "x \<bullet> i < a - 1 / (real (Suc n))"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Sep 30 16:36:42 2015 +0100
@@ -1298,7 +1298,7 @@
proof (subst integral_FTC_Icc_real)
fix x show "DERIV (\<lambda>x. x^Suc k / Suc k) x :> x^k"
by (intro derivative_eq_intros) auto
-qed (auto simp: field_simps)
+qed (auto simp: field_simps simp del: real_of_nat_Suc)
subsection {* Integration by parts *}
--- a/src/HOL/Probability/Regularity.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Probability/Regularity.thy Wed Sep 30 16:36:42 2015 +0100
@@ -192,7 +192,7 @@
also have "\<dots> \<le> (\<Sum>n. ereal (e*2 powr - real (Suc n)))"
using B_compl_le by (intro suminf_le_pos) (simp_all add: measure_nonneg emeasure_eq_measure)
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
- by (simp add: Transcendental.powr_minus powr_realpow field_simps)
+ by (simp add: Transcendental.powr_minus powr_realpow field_simps del: real_of_nat_Suc)
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
by simp
@@ -254,7 +254,7 @@
from in_closed_iff_infdist_zero[OF `closed A` `A \<noteq> {}`]
have "A = {x. infdist x A = 0}" by auto
also have "\<dots> = (\<Inter>i. ?G (1/real (Suc i)))"
- proof (auto, rule ccontr)
+ proof (auto simp del: real_of_nat_Suc, rule ccontr)
fix x
assume "infdist x A \<noteq> 0"
hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
@@ -262,7 +262,7 @@
moreover
assume "\<forall>i. infdist x A < 1 / real (Suc i)"
hence "infdist x A < 1 / real (Suc n)" by auto
- ultimately show False by simp
+ ultimately show False by simp
qed
also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
proof (rule INF_emeasure_decseq[symmetric], safe)
@@ -439,7 +439,7 @@
by (intro suminf_le_pos, subst emeasure_Diff)
(auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg intro: less_imp_le)
also have "\<dots> \<le> (\<Sum>n. ereal (e * (1 / 2) ^ Suc n))"
- by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide)
+ by (simp add: powr_minus inverse_eq_divide powr_realpow field_simps power_divide del: real_of_nat_Suc)
also have "\<dots> = (\<Sum>n. ereal e * ((1 / 2) ^ Suc n))"
unfolding times_ereal.simps[symmetric] ereal_power[symmetric] one_ereal_def numeral_eq_ereal
by simp
--- a/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Sep 30 16:36:42 2015 +0100
@@ -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: real_of_nat_power)
+ by (auto intro!: log_le simp: card_gt_0_iff power_real_of_nat simp del: real_of_nat_power real_of_nat_Suc)
also have "\<dots> = real (card observations) * log b (real n + 1)"
by (simp add: log_nat_power real_of_nat_Suc)
finally show ?thesis .
--- a/src/HOL/Real.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Real.thy Wed Sep 30 16:36:42 2015 +0100
@@ -22,7 +22,7 @@
subsection \<open>Preliminary lemmas\<close>
-lemma inj_add_left [simp]:
+lemma inj_add_left [simp]:
fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)"
by (meson add_left_imp_eq injI)
@@ -945,7 +945,7 @@
then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z"
using complete_real[of X] by blast
then have "Sup X = s"
- unfolding Sup_real_def by (best intro: Least_equality)
+ unfolding Sup_real_def by (best intro: Least_equality)
also from s z have "... \<le> z"
by blast
finally show "Sup X \<le> z" . }
@@ -971,7 +971,7 @@
lifting_update real.lifting
lifting_forget real.lifting
-
+
subsection\<open>More Lemmas\<close>
text \<open>BH: These lemmas should not be necessary; they should be
@@ -1010,7 +1010,7 @@
instantiation nat :: real_of
begin
-definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat"
+definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat"
instance ..
end
@@ -1018,7 +1018,7 @@
instantiation int :: real_of
begin
-definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int"
+definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int"
instance ..
end
@@ -1042,23 +1042,23 @@
lemma real_eq_of_int: "real = of_int"
unfolding real_of_int_def ..
-lemma real_of_int_zero [simp]: "real (0::int) = 0"
-by (simp add: real_of_int_def)
+lemma real_of_int_zero [simp]: "real (0::int) = 0"
+by (simp add: real_of_int_def)
lemma real_of_one [simp]: "real (1::int) = (1::real)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
by (simp add: real_of_int_def of_int_power)
@@ -1070,31 +1070,31 @@
apply (rule of_int_setsum)
done
-lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
+lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =
(PROD x:A. real(f x))"
apply (subst real_eq_of_int)+
apply (rule of_int_setprod)
done
lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
-by (simp add: real_of_int_def)
+by (simp add: real_of_int_def)
-lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
+lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)"
by (simp add: real_of_int_def)
lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
@@ -1127,7 +1127,7 @@
apply simp
done
-lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
+lemma real_of_int_div_aux: "(real (x::int)) / (real d) =
real (x div d) + (real (x mod d)) / (real d)"
proof -
have "x = (x div d) * d + x mod d"
@@ -1167,7 +1167,7 @@
apply (auto simp add: divide_le_eq intro: order_less_imp_le)
done
-lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
+lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x"
by (insert real_of_int_div2 [of n x], simp)
lemma Ints_real_of_int [simp]: "real (x::int) \<in> \<int>"
@@ -1188,11 +1188,10 @@
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
by (simp add: real_of_nat_def)
-(*Not for addsimps: often the LHS is used to represent a positive natural*)
-lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
+lemma real_of_nat_Suc [simp]: "real (Suc n) = real n + (1::real)"
by (simp add: real_of_nat_def)
-lemma real_of_nat_less_iff [iff]:
+lemma real_of_nat_less_iff [iff]:
"(real (n::nat) < real m) = (n < m)"
by (simp add: real_of_nat_def)
@@ -1213,13 +1212,13 @@
lemmas power_real_of_nat = real_of_nat_power [symmetric]
-lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
+lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =
(SUM x:A. real(f x))"
apply (subst real_eq_of_nat)+
apply (rule of_nat_setsum)
done
-lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
+lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =
(PROD x:A. real(f x))"
apply (subst real_eq_of_nat)+
apply (rule of_nat_setprod)
@@ -1250,18 +1249,12 @@
by (simp add: add: real_of_nat_def)
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"
- apply (subgoal_tac "real n + 1 = real (Suc n)")
- apply simp
- apply (auto simp add: real_of_nat_Suc)
-done
+by (metis discrete real_of_nat_1 real_of_nat_add real_of_nat_le_iff)
lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"
- apply (subgoal_tac "real m + 1 = real (Suc m)")
- apply (simp add: less_Suc_eq_le)
- apply (simp add: real_of_nat_Suc)
-done
+ by (meson nat_less_real_le not_le)
-lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
+lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =
real (x div d) + (real (x mod d)) / (real d)"
proof -
have "x = (x div d) * d + x mod d"
@@ -1295,7 +1288,7 @@
apply simp
done
-lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x"
+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 real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"
@@ -1399,7 +1392,7 @@
by (rule dvd_mult_div_cancel)
from \<open>n \<noteq> 0\<close> and gcd_l
have "?gcd * ?l \<noteq> 0" by simp
- then have "?l \<noteq> 0" by (blast dest!: mult_not_zero)
+ then have "?l \<noteq> 0" by (blast dest!: mult_not_zero)
moreover
have "\<bar>x\<bar> = real ?k / real ?l"
proof -
@@ -1432,8 +1425,8 @@
assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
proof -
from \<open>x<y\<close> have "0 < y-x" by simp
- with reals_Archimedean obtain q::nat
- where q: "inverse (real q) < y-x" and "0 < q" by auto
+ with reals_Archimedean obtain q::nat
+ where q: "inverse (real q) < y-x" and "0 < q" by blast
def p \<equiv> "ceiling (y * real q) - 1"
def r \<equiv> "of_int p / real q"
from q have "x < y - inverse (real q)" by simp
@@ -1493,7 +1486,7 @@
subsection\<open>Simprules combining x+y and 0: ARE THEY NEEDED?\<close>
-lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
+lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)"
by arith
text \<open>FIXME: redundant with @{text add_eq_0_iff} below\<close>
@@ -1649,7 +1642,7 @@
lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
by simp
-
+
lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
by simp
@@ -2017,7 +2010,7 @@
lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"
by (simp add: of_rat_inverse)
-
+
lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
by (simp add: of_rat_divide)
--- a/src/HOL/Transcendental.thy Tue Sep 29 23:43:35 2015 +0200
+++ b/src/HOL/Transcendental.thy Wed Sep 30 16:36:42 2015 +0100
@@ -870,7 +870,7 @@
from DERIV_D[OF DERIV_f[where n=n], THEN LIM_D, OF \<open>0 < ?r\<close>, unfolded real_norm_def]
obtain s where s_bound: "0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> \<bar>x\<bar> < s \<longrightarrow> \<bar>?diff n x - f' x0 n\<bar> < ?r)"
by auto
- have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound)
+ have "0 < ?s n" by (rule someI2[where a=s]) (auto simp add: s_bound simp del: real_of_nat_Suc)
thus "0 < x" unfolding \<open>x = ?s n\<close> .
qed
qed auto
@@ -930,7 +930,7 @@
by (rule setsum_constant)
also have "\<dots> = real ?N * ?r"
unfolding real_eq_of_nat by auto
- also have "\<dots> = r/3" by auto
+ also have "\<dots> = r/3" by (auto simp del: real_of_nat_Suc)
finally have "\<bar>\<Sum>n<?N. ?diff n x - f' x0 n \<bar> < r / 3" (is "?diff_part < r / 3") .
from suminf_diff[OF allf_summable[OF x_in_I] allf_summable[OF x0_in_I]]
@@ -1042,7 +1042,7 @@
by (rule mult_left_mono) auto
show "norm (f n * x^n) \<le> norm (f n * real (Suc n) * x^n)"
unfolding real_norm_def abs_mult
- by (rule mult_right_mono) (auto simp add: le[unfolded mult_1_right])
+ using le mult_right_mono by fastforce
qed (rule powser_insidea[OF converges[OF \<open>R' \<in> {-R <..< R}\<close>] \<open>norm x < norm R'\<close>])
from this[THEN summable_mult2[where c=x], unfolded mult.assoc, unfolded mult.commute]
show "summable (?f x)" by auto
@@ -5110,7 +5110,7 @@
}
have "?a 1 ----> 0"
unfolding tendsto_rabs_zero_iff power_one divide_inverse One_nat_def
- by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat)
+ by (auto intro!: tendsto_mult LIMSEQ_linear LIMSEQ_inverse_real_of_nat simp del: real_of_nat_Suc)
have "?diff 1 ----> 0"
proof (rule LIMSEQ_I)
fix r :: real