--- a/src/Doc/Sledgehammer/document/root.tex Wed Sep 30 23:15:50 2015 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Wed Sep 30 23:22:27 2015 +0200
@@ -278,7 +278,7 @@
provers might be missing or present with a \textit{remote\_} prefix.
For each successful prover, Sledgehammer gives a one-line \textit{metis} or
-\textit{smt2} method call. Rough timings are shown in parentheses, indicating how
+\textit{smt} method call. Rough timings are shown in parentheses, indicating how
fast the call is. You can click the proof to insert it into the theory text.
In addition, you can ask Sledgehammer for an Isar text proof by enabling the
@@ -289,7 +289,7 @@
\postw
When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt2} one-line
+readable and also faster than the \textit{metis} or \textit{smt} one-line
proofs. This feature is experimental and is only available for ATPs.
\section{Hints}
@@ -341,7 +341,7 @@
\item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
that Isar proofs should be generated, in addition to one-line \textit{metis} or
-\textit{smt2} proofs. The length of the Isar proofs can be controlled by setting
+\textit{smt} proofs. The length of the Isar proofs can be controlled by setting
\textit{compress} (\S\ref{output-format}).
\item[\labelitemi] \textbf{\textit{timeout}} (\S\ref{timeouts}) controls the
@@ -1277,9 +1277,9 @@
The collection of methods is roughly the same as for the \textbf{try0} command.
\opsmart{smt\_proofs}{no\_smt\_proofs}
-Specifies whether the \textit{smt2} proof method should be tried in addition to
+Specifies whether the \textit{smt} proof method should be tried in addition to
Isabelle's other proof methods. If the option is set to \textit{smart} (the
-default), the \textit{smt2} method is used for one-line proofs but not in Isar
+default), the \textit{smt} method is used for one-line proofs but not in Isar
proofs.
\end{enum}
--- a/src/HOL/MacLaurin.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/MacLaurin.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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/Determinants.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy Wed Sep 30 23:22:27 2015 +0200
@@ -10,74 +10,6 @@
"~~/src/HOL/Library/Permutations"
begin
-subsection\<open>First some facts about products\<close>
-
-lemma setprod_add_split:
- fixes m n :: nat
- assumes mn: "m \<le> n + 1"
- shows "setprod f {m..n+p} = setprod f {m .. n} * setprod f {n+1..n+p}"
-proof -
- let ?A = "{m..n+p}"
- let ?B = "{m..n}"
- let ?C = "{n+1..n+p}"
- from mn have un: "?B \<union> ?C = ?A"
- by auto
- from mn have dj: "?B \<inter> ?C = {}"
- by auto
- have f: "finite ?B" "finite ?C"
- by simp_all
- from setprod.union_disjoint[OF f dj, of f, unfolded un] show ?thesis .
-qed
-
-
-lemma setprod_offset:
- fixes m n :: nat
- shows "setprod f {m + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}"
- by (rule setprod.reindex_bij_witness[where i="op + p" and j="\<lambda>i. i - p"]) auto
-
-lemma setprod_singleton: "setprod f {x} = f x"
- by simp
-
-lemma setprod_singleton_nat_seg:
- fixes n :: "'a::order"
- shows "setprod f {n..n} = f n"
- by simp
-
-lemma setprod_numseg:
- "setprod f {m..0} = (if m = 0 then f 0 else 1)"
- "setprod f {m .. Suc n} =
- (if m \<le> Suc n then f (Suc n) * setprod f {m..n} else setprod f {m..n})"
- by (auto simp add: atLeastAtMostSuc_conv)
-
-lemma setprod_le:
- fixes f g :: "'b \<Rightarrow> 'a::linordered_idom"
- assumes fS: "finite S"
- and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> g x"
- shows "setprod f S \<le> setprod g S"
- using fS fg
- apply (induct S)
- apply simp
- apply auto
- apply (rule mult_mono)
- apply (auto intro: setprod_nonneg)
- done
-
-(* FIXME: In Finite_Set there is a useless further assumption *)
-lemma setprod_inversef:
- "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field)"
- apply (erule finite_induct)
- apply (simp)
- apply simp
- done
-
-lemma setprod_le_1:
- fixes f :: "'b \<Rightarrow> 'a::linordered_idom"
- assumes fS: "finite S"
- and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> 1"
- shows "setprod f S \<le> 1"
- using setprod_le[OF fS f] unfolding setprod.neutral_const .
-
-
subsection \<open>Trace\<close>
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
@@ -1275,16 +1207,16 @@
text \<open>Explicit formulas for low dimensions.\<close>
lemma setprod_neutral_const: "setprod f {(1::nat)..1} = f 1"
- by (fact setprod_singleton_nat_seg)
+ by simp
lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
- by (simp add: eval_nat_numeral setprod_numseg mult.commute)
+ by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
- by (simp add: eval_nat_numeral setprod_numseg mult.commute)
+ by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
- by (simp add: det_def sign_id)
+ by (simp add: det_def of_nat_Suc sign_id)
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
proof -
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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/Multivariate_Analysis/ex/Approximations.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Wed Sep 30 23:22:27 2015 +0200
@@ -27,9 +27,9 @@
lemma pi_approx_32: "abs(pi - 13493037705/4294967296) \<le> inverse(2 ^ 32)"
apply (simp only: abs_diff_le_iff)
apply (rule sin_pi6_straddle, simp_all)
- using Taylor_sin [of "1686629713/3221225472" 11]
+ using Taylor_sin [of "1686629713/3221225472" 11]
apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
- apply (simp only: pos_le_divide_eq [symmetric])
+ apply (simp only: pos_le_divide_eq [symmetric])
using Taylor_sin [of "6746518853/12884901888" 11]
apply (simp add: in_Reals_norm sin_coeff_def Re_sin atMost_nat_numeral fact_numeral)
apply (simp only: pos_le_divide_eq [symmetric] pos_divide_le_eq [symmetric])
--- a/src/HOL/NSA/HSEQ.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/NSA/HSEQ.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/NSA/HyperDef.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/NSA/NSA.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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/Old_Number_Theory/Finite2.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy Wed Sep 30 23:22:27 2015 +0200
@@ -37,15 +37,11 @@
qed
lemma setsum_const: "finite X ==> setsum (%x. (c :: int)) X = c * int(card X)"
- apply (induct set: finite)
- apply (auto simp add: distrib_right distrib_left)
- done
+by (simp add: of_nat_mult)
lemma setsum_const2: "finite X ==> int (setsum (%x. (c :: nat)) X) =
int(c) * int(card X)"
- apply (induct set: finite)
- apply (auto simp add: distrib_left)
- done
+by (simp add: of_nat_mult)
lemma setsum_const_mult: "finite A ==> setsum (%x. c * ((f x)::int)) A =
c * setsum f A"
--- a/src/HOL/Probability/Borel_Space.thy Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Probability/Regularity.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Real.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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 Wed Sep 30 23:15:50 2015 +0200
+++ b/src/HOL/Transcendental.thy Wed Sep 30 23:22:27 2015 +0200
@@ -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