--- a/src/HOL/MacLaurin.thy Fri Jul 20 09:05:34 2018 +0200
+++ b/src/HOL/MacLaurin.thy Sat Jul 21 13:30:43 2018 +0200
@@ -146,13 +146,6 @@
qed
qed
-lemma Maclaurin_objl:
- "0 < h \<and> n > 0 \<and> diff 0 = f \<and>
- (\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
- (\<exists>t. 0 < t \<and> t < h \<and> f h = (\<Sum>m<n. diff m 0 / (fact m) * h ^ m) + diff n t / fact n * h ^ n)"
- for n :: nat and h :: real
- by (blast intro: Maclaurin)
-
lemma Maclaurin2:
fixes n :: nat
and h :: real
@@ -172,13 +165,6 @@
then show ?thesis by fastforce
qed
-lemma Maclaurin2_objl:
- "0 < h \<and> diff 0 = f \<and>
- (\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
- (\<exists>t. 0 < t \<and> t \<le> h \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n)"
- for n :: nat and h :: real
- by (blast intro: Maclaurin2)
-
lemma Maclaurin_minus:
fixes n :: nat and h :: real
assumes "h < 0" "0 < n" "diff 0 = f"
@@ -205,24 +191,9 @@
then show ?thesis ..
qed
-lemma Maclaurin_minus_objl:
- fixes n :: nat and h :: real
- shows
- "h < 0 \<and> n > 0 \<and> diff 0 = f \<and>
- (\<forall>m t. m < n \<and> h \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t) \<longrightarrow>
- (\<exists>t. h < t \<and> t < 0 \<and> f h = (\<Sum>m<n. diff m 0 / fact m * h ^ m) + diff n t / fact n * h ^ n)"
- by (blast intro: Maclaurin_minus)
-
subsection \<open>More Convenient "Bidirectional" Version.\<close>
-(* not good for PVS sin_approx, cos_approx *)
-
-lemma Maclaurin_bi_le_lemma:
- "n > 0 \<Longrightarrow>
- diff 0 0 = (\<Sum>m<n. diff m 0 * 0 ^ m / (fact m)) + diff n 0 * 0 ^ n / (fact n :: real)"
- by (induct n) auto
-
lemma Maclaurin_bi_le:
fixes n :: nat and x :: real
assumes "diff 0 = f"
@@ -238,7 +209,7 @@
proof (cases rule: linorder_cases)
assume "x = 0"
with \<open>n \<noteq> 0\<close> \<open>diff 0 = f\<close> DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and> f x = ?f x 0"
- by (auto simp add: Maclaurin_bi_le_lemma)
+ by auto
then show ?thesis ..
next
assume "x < 0"
@@ -294,18 +265,9 @@
then show ?thesis ..
qed
-
-lemma Maclaurin_all_lt_objl:
- fixes x :: real
- shows
- "diff 0 = f \<and> (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x) \<and> x \<noteq> 0 \<and> n > 0 \<longrightarrow>
- (\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and>
- f x = (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) + (diff n t / fact n) * x ^ n)"
- by (blast intro: Maclaurin_all_lt)
-
lemma Maclaurin_zero: "x = 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> (\<Sum>m<n. (diff m 0 / fact m) * x ^ m) = diff 0 0"
for x :: real and n :: nat
- by (induct n) auto
+ by simp
lemma Maclaurin_all_le:
@@ -352,7 +314,7 @@
shows
"x \<noteq> 0 \<Longrightarrow> n > 0 \<Longrightarrow>
(\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> exp x = (\<Sum>m<n. (x ^ m) / fact m) + (exp t / fact n) * x ^ n)"
- using Maclaurin_all_lt_objl [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
+ using Maclaurin_all_lt [where diff = "\<lambda>n. exp" and f = exp and x = x and n = n] by auto
lemma Maclaurin_exp_le:
fixes x :: real and n :: nat
@@ -377,15 +339,6 @@
for m :: nat
by auto
-lemma Suc_Suc_mult_two_diff_two [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (Suc (2 * n - 2)) = 2 * n"
- by (induct n) auto
-
-lemma lemma_Suc_Suc_4n_diff_2 [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (Suc (4 * n - 2)) = 4 * n"
- by (induct n) auto
-
-lemma Suc_mult_two_diff_one [simp]: "n \<noteq> 0 \<Longrightarrow> Suc (2 * n - 1) = 2 * n"
- by (induct n) auto
-
text \<open>It is unclear why so many variant results are needed.\<close>
@@ -395,61 +348,72 @@
lemma Maclaurin_sin_expansion2:
"\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
- using Maclaurin_all_lt_objl
- [where f = sin and n = n and x = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
- apply safe
- apply simp
- apply (simp add: sin_expansion_lemma del: of_nat_Suc)
- apply (force intro!: derivative_eq_intros)
- apply (subst (asm) sum.neutral; auto)
- apply (rule ccontr)
- apply simp
- apply (drule_tac x = x in spec)
- apply simp
- apply (erule ssubst)
- apply (rule_tac x = t in exI)
- apply simp
- apply (rule sum.cong[OF refl])
- apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
- done
+proof (cases "n = 0 \<or> x = 0")
+ case False
+ let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
+ have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> sin x =
+ (\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n"
+ proof (rule Maclaurin_all_lt)
+ show "\<forall>m x. ((\<lambda>t. sin (t + 1/2 * real m * pi)) has_real_derivative
+ sin (x + 1/2 * real (Suc m) * pi)) (at x)"
+ by (rule allI derivative_eq_intros | use sin_expansion_lemma in force)+
+ qed (use False in auto)
+ then show ?thesis
+ apply (rule ex_forward)
+ apply simp
+ apply (rule sum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
+ done
+qed auto
lemma Maclaurin_sin_expansion:
"\<exists>t. sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
using Maclaurin_sin_expansion2 [of x n] by blast
lemma Maclaurin_sin_expansion3:
- "n > 0 \<Longrightarrow> 0 < x \<Longrightarrow>
- \<exists>t. 0 < t \<and> t < x \<and>
- sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
- using Maclaurin_objl
- [where f = sin and n = n and h = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
- apply safe
+ assumes "n > 0" "x > 0"
+ shows "\<exists>t. 0 < t \<and> t < x \<and>
+ sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+proof -
+ let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
+ have "\<exists>t. 0 < t \<and> t < x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
+ proof (rule Maclaurin)
+ show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
+ ((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative
+ sin (t + 1/2 * real (Suc m) * pi)) (at t)"
+ apply (simp add: sin_expansion_lemma del: of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ done
+ qed (use assms in auto)
+ then show ?thesis
+ apply (rule ex_forward)
apply simp
- apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
- apply (force intro!: derivative_eq_intros)
- apply (erule ssubst)
- apply (rule_tac x = t in exI)
- apply simp
- apply (rule sum.cong[OF refl])
- apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
- done
+ apply (rule sum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
+ done
+qed
lemma Maclaurin_sin_expansion4:
- "0 < x \<Longrightarrow>
- \<exists>t. 0 < t \<and> t \<le> x \<and>
- sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
- using Maclaurin2_objl
- [where f = sin and n = n and h = x and diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"]
- apply safe
+ assumes "0 < x"
+ shows "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. sin_coeff m * x ^ m) + (sin (t + 1/2 * real n * pi) / fact n) * x ^ n"
+proof -
+ let ?diff = "\<lambda>n x. sin (x + 1/2 * real n * pi)"
+ have "\<exists>t. 0 < t \<and> t \<le> x \<and> sin x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
+ proof (rule Maclaurin2)
+ show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
+ ((\<lambda>u. sin (u + 1/2 * real m * pi)) has_real_derivative
+ sin (t + 1/2 * real (Suc m) * pi)) (at t)"
+ apply (simp add: sin_expansion_lemma del: of_nat_Suc)
+ apply (force intro!: derivative_eq_intros)
+ done
+ qed (use assms in auto)
+ then show ?thesis
+ apply (rule ex_forward)
apply simp
- apply (simp (no_asm) add: sin_expansion_lemma del: of_nat_Suc)
- apply (force intro!: derivative_eq_intros)
- apply (erule ssubst)
- apply (rule_tac x = t in exI)
- apply simp
- apply (rule sum.cong[OF refl])
- apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
- done
+ apply (rule sum.cong[OF refl])
+ apply (auto simp add: sin_coeff_def sin_zero_iff elim: oddE simp del: of_nat_Suc)
+ done
+qed
subsection \<open>Maclaurin Expansion for Cosine Function\<close>
@@ -463,56 +427,66 @@
lemma Maclaurin_cos_expansion:
"\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos(t + 1/2 * real n * pi) / fact n) * x ^ n"
- using Maclaurin_all_lt_objl
- [where f = cos and n = n and x = x and diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"]
- apply safe
- apply simp
- apply (simp add: cos_expansion_lemma del: of_nat_Suc)
- apply (cases n)
- apply simp
- apply (simp del: sum_lessThan_Suc)
- apply (rule ccontr)
- apply simp
- apply (drule_tac x = x in spec)
- apply simp
- apply (erule ssubst)
- apply (rule_tac x = t in exI)
- apply simp
- apply (rule sum.cong[OF refl])
- apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
- done
+proof (cases "n = 0 \<or> x = 0")
+ case False
+ let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
+ have "\<exists>t. 0 < \<bar>t\<bar> \<and> \<bar>t\<bar> < \<bar>x\<bar> \<and> cos x =
+ (\<Sum>m<n. (?diff m 0 / fact m) * x ^ m) + (?diff n t / fact n) * x ^ n"
+ proof (rule Maclaurin_all_lt)
+ show "\<forall>m x. ((\<lambda>t. cos (t + 1/2 * real m * pi)) has_real_derivative
+ cos (x + 1/2 * real (Suc m) * pi)) (at x)"
+ apply (rule allI derivative_eq_intros | simp)+
+ using cos_expansion_lemma by force
+ qed (use False in auto)
+ then show ?thesis
+ apply (rule ex_forward)
+ apply simp
+ apply (rule sum.cong[OF refl])
+ apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE simp del: of_nat_Suc)
+ done
+qed auto
lemma Maclaurin_cos_expansion2:
- "0 < x \<Longrightarrow> n > 0 \<Longrightarrow>
- \<exists>t. 0 < t \<and> t < x \<and>
+ assumes "n > 0" "x > 0"
+ shows "\<exists>t. 0 < t \<and> t < x \<and>
cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + (cos (t + 1/2 * real n * pi) / fact n) * x ^ n"
- using Maclaurin_objl
- [where f = cos and n = n and h = x and diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"]
- apply safe
+proof -
+ let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
+ have "\<exists>t. 0 < t \<and> t < x \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
+ proof (rule Maclaurin)
+ show "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow>
+ ((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative
+ cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
+ by (simp add: cos_expansion_lemma del: of_nat_Suc)
+ qed (use assms in auto)
+ then show ?thesis
+ apply (rule ex_forward)
apply simp
- apply (simp add: cos_expansion_lemma del: of_nat_Suc)
- apply (erule ssubst)
- apply (rule_tac x = t in exI)
- apply simp
- apply (rule sum.cong[OF refl])
- apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
- done
+ apply (rule sum.cong[OF refl])
+ apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
+ done
+qed
lemma Maclaurin_minus_cos_expansion:
- "x < 0 \<Longrightarrow> n > 0 \<Longrightarrow>
- \<exists>t. x < t \<and> t < 0 \<and>
- cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)"
- using Maclaurin_minus_objl
- [where f = cos and n = n and h = x and diff = "\<lambda>n x. cos (x + 1/2 * real n *pi)"]
- apply safe
+ assumes "n > 0" "x < 0"
+ shows "\<exists>t. x < t \<and> t < 0 \<and>
+ cos x = (\<Sum>m<n. cos_coeff m * x ^ m) + ((cos (t + 1/2 * real n * pi) / fact n) * x ^ n)"
+proof -
+ let ?diff = "\<lambda>n x. cos (x + 1/2 * real n * pi)"
+ have "\<exists>t. x < t \<and> t < 0 \<and> cos x = (\<Sum>m<n. ?diff m 0 / (fact m) * x ^ m) + ?diff n t / fact n * x ^ n"
+ proof (rule Maclaurin_minus)
+ show "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow>
+ ((\<lambda>u. cos (u + 1 / 2 * real m * pi)) has_real_derivative
+ cos (t + 1 / 2 * real (Suc m) * pi)) (at t)"
+ by (simp add: cos_expansion_lemma del: of_nat_Suc)
+ qed (use assms in auto)
+ then show ?thesis
+ apply (rule ex_forward)
apply simp
- apply (simp add: cos_expansion_lemma del: of_nat_Suc)
- apply (erule ssubst)
- apply (rule_tac x = t in exI)
- apply simp
- apply (rule sum.cong[OF refl])
- apply (auto simp: cos_coeff_def cos_zero_iff elim: evenE)
- done
+ apply (rule sum.cong[OF refl])
+ apply (auto simp add: cos_coeff_def cos_zero_iff elim: evenE)
+ done
+qed
(* Version for ln(1 +/- x). Where is it?? *)
--- a/src/HOL/Real.thy Fri Jul 20 09:05:34 2018 +0200
+++ b/src/HOL/Real.thy Sat Jul 21 13:30:43 2018 +0200
@@ -381,11 +381,7 @@
lemma transp_realrel: "transp realrel"
unfolding realrel_def
- apply (rule transpI)
- apply clarify
- apply (drule (1) vanishes_add)
- apply (simp add: algebra_simps)
- done
+ by (rule transpI) (force simp add: dest: vanishes_add)
lemma part_equivp_realrel: "part_equivp realrel"
by (blast intro: part_equivpI symp_realrel transp_realrel realrel_refl cauchy_const)
@@ -567,33 +563,32 @@
lemma positive_zero: "\<not> positive 0"
by transfer auto
-lemma positive_add: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
- apply transfer
- apply clarify
- apply (rename_tac a b i j)
- apply (rule_tac x = "a + b" in exI)
- apply simp
- apply (rule_tac x = "max i j" in exI)
- apply clarsimp
- apply (simp add: add_strict_mono)
- done
+lemma positive_add:
+ assumes "positive x" "positive y" shows "positive (x + y)"
+proof -
+ have *: "\<lbrakk>\<forall>n\<ge>i. a < x n; \<forall>n\<ge>j. b < y n; 0 < a; 0 < b; n \<ge> max i j\<rbrakk>
+ \<Longrightarrow> a+b < x n + y n" for x y and a b::rat and i j n::nat
+ by (simp add: add_strict_mono)
+ show ?thesis
+ using assms
+ by transfer (blast intro: * pos_add_strict)
+qed
-lemma positive_mult: "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
- apply transfer
- apply clarify
- apply (rename_tac a b i j)
- apply (rule_tac x = "a * b" in exI)
- apply simp
- apply (rule_tac x = "max i j" in exI)
- apply clarsimp
- apply (rule mult_strict_mono)
- apply auto
- done
+lemma positive_mult:
+ assumes "positive x" "positive y" shows "positive (x * y)"
+proof -
+ have *: "\<lbrakk>\<forall>n\<ge>i. a < x n; \<forall>n\<ge>j. b < y n; 0 < a; 0 < b; n \<ge> max i j\<rbrakk>
+ \<Longrightarrow> a*b < x n * y n" for x y and a b::rat and i j n::nat
+ by (simp add: mult_strict_mono')
+ show ?thesis
+ using assms
+ by transfer (blast intro: * mult_pos_pos)
+qed
lemma positive_minus: "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
apply transfer
apply (simp add: realrel_def)
- apply (blast intro: dest: cauchy_not_vanishes_cases)
+ apply (blast dest: cauchy_not_vanishes_cases)
done
instantiation real :: linordered_field
@@ -690,18 +685,24 @@
subsection \<open>Completeness\<close>
-lemma not_positive_Real: "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" (is "?lhs = ?rhs")
- if "cauchy X"
- unfolding positive_Real [OF that]
- apply auto
- apply (unfold not_less)
- apply (erule obtain_pos_sum)
- apply (drule_tac x=s in spec)
- apply simp
- apply (drule_tac r=t in cauchyD [OF that])
- apply fastforce
- apply (meson le_cases)
- done
+lemma not_positive_Real:
+ assumes "cauchy X" shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" (is "?lhs = ?rhs")
+ unfolding positive_Real [OF assms]
+proof (intro iffI allI notI impI)
+ show "\<exists>k. \<forall>n\<ge>k. X n \<le> r" if r: "\<not> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)" and "0 < r" for r
+ proof -
+ obtain s t where "s > 0" "t > 0" "r = s+t"
+ using \<open>r > 0\<close> obtain_pos_sum by blast
+ obtain k where k: "\<And>m n. \<lbrakk>m\<ge>k; n\<ge>k\<rbrakk> \<Longrightarrow> \<bar>X m - X n\<bar> < t"
+ using cauchyD [OF assms \<open>t > 0\<close>] by blast
+ obtain n where "n \<ge> k" "X n \<le> s"
+ by (meson r \<open>0 < s\<close> not_less)
+ then have "X l \<le> r" if "l \<ge> n" for l
+ using k [OF \<open>n \<ge> k\<close>, of l] that \<open>r = s+t\<close> by linarith
+ then show ?thesis
+ by blast
+ qed
+qed (meson le_cases not_le)
lemma le_Real:
assumes "cauchy X" "cauchy Y"
@@ -811,70 +812,62 @@
unfolding A_def B_def C_def bisect_def split_def by simp
have width: "B n - A n = (b - a) / 2^n" for n
- apply (induct n)
- apply (simp_all add: eq_divide_eq)
- apply (simp_all add: C_def avg_def algebra_simps)
- done
-
- have twos: "0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r" for y r :: rat
- apply (simp add: divide_less_eq)
- apply (subst mult.commute)
- apply (frule_tac y=y in ex_less_of_nat_mult)
- apply clarify
- apply (rule_tac x=n in exI)
- by (metis less_trans mult.commute mult_less_cancel_left_pos of_nat_less_two_power)
-
+ proof (induct n)
+ case (Suc n)
+ then show ?case
+ by (simp add: C_def eq_divide_eq avg_def algebra_simps)
+ qed simp
+ have twos: "\<exists>n. y / 2 ^ n < r" if "0 < r" for y r :: rat
+ proof -
+ obtain n where "y / r < rat_of_nat n"
+ using \<open>0 < r\<close> reals_Archimedean2 by blast
+ then have "\<exists>n. y < r * 2 ^ n"
+ by (metis divide_less_eq less_trans mult.commute of_nat_less_two_power that)
+ then show ?thesis
+ by (simp add: divide_simps)
+ qed
have PA: "\<not> P (A n)" for n
by (induct n) (simp_all add: a)
have PB: "P (B n)" for n
by (induct n) (simp_all add: b)
have ab: "a < b"
using a b unfolding P_def
- apply (clarsimp simp add: not_le)
- using less_le_trans of_rat_less by blast
+ by (meson leI less_le_trans of_rat_less)
have AB: "A n < B n" for n
by (induct n) (simp_all add: ab C_def avg_def)
- have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
- apply (auto simp add: le_less [where 'a=nat])
- apply (erule less_Suc_induct)
- apply (clarsimp simp add: C_def avg_def)
- apply (simp add: add_divide_distrib [symmetric])
- apply (rule AB [THEN less_imp_le])
- apply simp
- done
- have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"
- apply (auto simp add: le_less [where 'a=nat])
- apply (erule less_Suc_induct)
- apply (clarsimp simp add: C_def avg_def)
- apply (simp add: add_divide_distrib [symmetric])
- apply (rule AB [THEN less_imp_le])
- apply simp
- done
- have cauchy_lemma: "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
- apply (rule cauchyI)
- apply (drule twos [where y="b - a"])
- apply (erule exE)
- apply (rule_tac x=n in exI, clarify, rename_tac i j)
- apply (rule_tac y="B n - A n" in le_less_trans) defer
- apply (simp add: width)
- apply (drule_tac x=n in spec)
- apply (frule_tac x=i in spec, drule (1) mp)
- apply (frule_tac x=j in spec, drule (1) mp)
- apply (frule A_mono, drule B_mono)
- apply (frule A_mono, drule B_mono)
- apply arith
- done
+ have "A i \<le> A j \<and> B j \<le> B i" if "i < j" for i j
+ using that
+ proof (induction rule: less_Suc_induct)
+ case (1 i)
+ then show ?case
+ apply (clarsimp simp add: C_def avg_def add_divide_distrib [symmetric])
+ apply (rule AB [THEN less_imp_le])
+ done
+ qed simp
+ then have A_mono: "A i \<le> A j" and B_mono: "B j \<le> B i" if "i \<le> j" for i j
+ by (metis eq_refl le_neq_implies_less that)+
+ have cauchy_lemma: "cauchy X" if *: "\<And>n i. i\<ge>n \<Longrightarrow> A n \<le> X i \<and> X i \<le> B n" for X
+ proof (rule cauchyI)
+ fix r::rat
+ assume "0 < r"
+ then obtain k where k: "(b - a) / 2 ^ k < r"
+ using twos by blast
+ have "\<bar>X m - X n\<bar> < r" if "m\<ge>k" "n\<ge>k" for m n
+ proof -
+ have "\<bar>X m - X n\<bar> \<le> B k - A k"
+ by (simp add: * abs_rat_def diff_mono that)
+ also have "... < r"
+ by (simp add: k width)
+ finally show ?thesis .
+ qed
+ then show "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
+ by blast
+ qed
have "cauchy A"
- apply (rule cauchy_lemma [rule_format])
- apply (simp add: A_mono)
- apply (erule order_trans [OF less_imp_le [OF AB] B_mono])
- done
+ by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order less_le_trans)
have "cauchy B"
- apply (rule cauchy_lemma [rule_format])
- apply (simp add: B_mono)
- apply (erule order_trans [OF A_mono less_imp_le [OF AB]])
- done
- have 1: "\<forall>x\<in>S. x \<le> Real B"
+ by (rule cauchy_lemma) (meson AB A_mono B_mono dual_order.strict_implies_order le_less_trans)
+ have "\<forall>x\<in>S. x \<le> Real B"
proof
fix x
assume "x \<in> S"
@@ -882,20 +875,9 @@
using PB [unfolded P_def] \<open>cauchy B\<close>
by (simp add: le_RealI)
qed
- have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"
- apply clarify
- apply (erule contrapos_pp)
- apply (simp add: not_le)
- apply (drule less_RealD [OF \<open>cauchy A\<close>])
- apply clarify
- apply (subgoal_tac "\<not> P (A n)")
- apply (simp add: P_def not_le)
- apply clarify
- apply (erule rev_bexI)
- apply (erule (1) less_trans)
- apply (simp add: PA)
- done
- have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
+ moreover have "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"
+ by (meson PA Real_leI P_def \<open>cauchy A\<close> le_cases order.trans)
+ moreover have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
proof (rule vanishesI)
fix r :: rat
assume "0 < r"
@@ -914,13 +896,10 @@
qed
then show "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
qed
- then have 3: "Real B = Real A"
+ then have "Real B = Real A"
by (simp add: eq_Real \<open>cauchy A\<close> \<open>cauchy B\<close> width)
- show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
- apply (rule exI [where x = "Real B"])
- using 1 2 3
- apply simp
- done
+ ultimately show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
+ by force
qed
instantiation real :: linear_continuum
@@ -1068,18 +1047,15 @@
by (simp add: real_of_int_div_aux)
lemma real_of_int_div2: "0 \<le> real_of_int n / real_of_int x - real_of_int (n div x)"
- apply (cases "x = 0")
- apply simp
- apply (cases "0 < x")
- apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq)
- apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq)
- done
+proof (cases "x = 0")
+ case False
+ then show ?thesis
+ by (metis diff_ge_0_iff_ge floor_divide_of_int_eq of_int_floor_le)
+qed simp
lemma real_of_int_div3: "real_of_int n / real_of_int x - real_of_int (n div x) \<le> 1"
apply (simp add: algebra_simps)
- apply (subst real_of_int_div_aux)
- apply (auto simp add: divide_le_eq intro: order_less_imp_le)
- done
+ by (metis add.commute floor_correct floor_divide_of_int_eq less_eq_real_def of_int_1 of_int_add)
lemma real_of_int_div4: "real_of_int (n div x) \<le> real_of_int n / real_of_int x"
using real_of_int_div2 [of n x] by simp
@@ -1114,17 +1090,14 @@
lemma real_of_nat_div2: "0 \<le> real n / real x - real (n div x)" for n x :: nat
apply (simp add: algebra_simps)
- apply (subst real_of_nat_div_aux)
- apply simp
- done
+ by (metis floor_divide_of_nat_eq of_int_floor_le of_int_of_nat_eq)
lemma real_of_nat_div3: "real n / real x - real (n div x) \<le> 1" for n x :: nat
- apply (cases "x = 0")
- apply simp
- apply (simp add: algebra_simps)
- apply (subst real_of_nat_div_aux)
- apply simp
- done
+proof (cases "x = 0")
+ case False
+ then show ?thesis
+ by (metis of_int_of_nat_eq real_of_int_div3 zdiv_int)
+qed auto
lemma real_of_nat_div4: "real (n div x) \<le> real n / real x" for n x :: nat
using real_of_nat_div2 [of n x] by simp
@@ -1502,10 +1475,7 @@
by (auto intro!: bexI[of _ "of_nat (nat \<lceil>x\<rceil>)"]) linarith
lemma Rats_no_bot_less: "\<exists>q \<in> \<rat>. q < x" for x :: real
- apply (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"])
- apply (rule less_le_trans[OF _ of_int_floor_le])
- apply simp
- done
+ by (auto intro!: bexI[of _ "of_int (\<lfloor>x\<rfloor> - 1)"]) linarith
subsection \<open>Exponentiation with floor\<close>
--- a/src/HOL/Real_Vector_Spaces.thy Fri Jul 20 09:05:34 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Sat Jul 21 13:30:43 2018 +0200
@@ -512,13 +512,11 @@
lemma scaleR_left_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> c *\<^sub>R a \<le> c *\<^sub>R b"
for a b :: "'a::ordered_real_vector"
- apply (drule scaleR_left_mono [of _ _ "- c"], simp_all)
- done
+ by (drule scaleR_left_mono [of _ _ "- c"], simp_all)
lemma scaleR_right_mono_neg: "b \<le> a \<Longrightarrow> c \<le> 0 \<Longrightarrow> a *\<^sub>R c \<le> b *\<^sub>R c"
for c :: "'a::ordered_real_vector"
- apply (drule scaleR_right_mono [of _ _ "- c"], simp_all)
- done
+ by (drule scaleR_right_mono [of _ _ "- c"], simp_all)
lemma scaleR_nonpos_nonpos: "a \<le> 0 \<Longrightarrow> b \<le> 0 \<Longrightarrow> 0 \<le> a *\<^sub>R b"
for b :: "'a::ordered_real_vector"
@@ -1433,10 +1431,7 @@
lemma flip: "bounded_bilinear (\<lambda>x y. y ** x)"
apply standard
- apply (rule add_right)
- apply (rule add_left)
- apply (rule scaleR_right)
- apply (rule scaleR_left)
+ apply (simp_all add: add_right add_left scaleR_right scaleR_left)
by (metis bounded mult.commute)
lemma comp1:
@@ -1496,11 +1491,7 @@
proof -
interpret f: bounded_linear f by fact
show ?thesis
- apply unfold_locales
- apply (simp add: f.add)
- apply (simp add: f.scaleR)
- apply (simp add: f.bounded)
- done
+ by unfold_locales (simp_all add: f.add f.scaleR f.bounded)
qed
lemma bounded_linear_sub: "bounded_linear f \<Longrightarrow> bounded_linear g \<Longrightarrow> bounded_linear (\<lambda>x. f x - g x)"