--- a/src/HOL/Limits.thy Wed Jul 11 15:36:12 2018 +0100
+++ b/src/HOL/Limits.thy Wed Jul 11 19:19:00 2018 +0100
@@ -36,7 +36,7 @@
have 3: "\<forall>x. u \<le> \<bar>x\<bar> \<longrightarrow> A x \<Longrightarrow> \<exists>N. \<forall>n\<le>N. A n" for A and u::real
by (metis (full_types) abs_ge_self abs_minus_cancel le_minus_iff order_trans)
show ?thesis
- by (auto simp add: filter_eq_iff eventually_sup eventually_at_infinity
+ by (auto simp: filter_eq_iff eventually_sup eventually_at_infinity
eventually_at_top_linorder eventually_at_bot_linorder intro: 1 2 3)
qed
@@ -136,7 +136,7 @@
by (simp add: Bseq_def)
lemma BseqI: "0 < K \<Longrightarrow> \<forall>n. norm (X n) \<le> K \<Longrightarrow> Bseq X"
- by (auto simp add: Bseq_def)
+ by (auto simp: Bseq_def)
lemma Bseq_bdd_above: "Bseq X \<Longrightarrow> bdd_above (range X)"
for X :: "nat \<Rightarrow> real"
@@ -222,7 +222,7 @@
proof
assume ?P
then obtain K where *: "0 < K" and **: "\<And>n. norm (X n) \<le> K"
- by (auto simp add: Bseq_def)
+ by (auto simp: Bseq_def)
from * have "0 < K + norm (X 0)" by (rule order_less_le_trans) simp
from ** have "\<forall>n. norm (X n - X 0) \<le> K + norm (X 0)"
by (auto intro: order_trans norm_triangle_ineq4)
@@ -231,7 +231,7 @@
with \<open>0 < K + norm (X 0)\<close> show ?Q by blast
next
assume ?Q
- then show ?P by (auto simp add: Bseq_iff2)
+ then show ?P by (auto simp: Bseq_iff2)
qed
@@ -688,7 +688,7 @@
unfolding tendsto_Zfun_iff add_diff_add
using tendsto_fst[OF filterlim_ident, of "(a,b)"] tendsto_snd[OF filterlim_ident, of "(a,b)"]
by (intro Zfun_add)
- (auto simp add: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
+ (auto simp: tendsto_Zfun_iff[symmetric] nhds_prod[symmetric] intro!: tendsto_fst)
show "(uminus \<longlongrightarrow> - a) (nhds a)"
unfolding tendsto_Zfun_iff minus_diff_minus
using filterlim_ident[of "nhds a"]
@@ -826,7 +826,7 @@
lemma continuous_on_mult_const [simp]:
fixes c::"'a::real_normed_algebra"
- shows "continuous_on s (( * ) c)"
+ shows "continuous_on s (( *) c)"
by (intro continuous_on_mult_left continuous_on_id)
lemma tendsto_divide_zero:
@@ -910,14 +910,6 @@
shows "Zfun (\<lambda>x. f x ** g x) F"
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
-lemma Bfun_inverse_lemma:
- fixes x :: "'a::real_normed_div_algebra"
- shows "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
- apply (subst nonzero_norm_inverse)
- apply clarsimp
- apply (erule (1) le_imp_inverse_le)
- done
-
lemma Bfun_inverse:
fixes a :: "'a::real_normed_div_algebra"
assumes f: "(f \<longlongrightarrow> a) F"
@@ -1304,14 +1296,14 @@
lemma at_bot_mirror :
shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
apply (rule filtermap_fun_inverse[of uminus, symmetric])
- subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
+ subgoal unfolding filterlim_at_top filterlim_at_bot eventually_at_bot_linorder using le_minus_iff by auto
subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
by auto
lemma at_top_mirror :
shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
apply (subst at_bot_mirror)
- by (auto simp add: filtermap_filtermap)
+ by (auto simp: filtermap_filtermap)
lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
unfolding filterlim_def at_top_mirror filtermap_filtermap ..
@@ -1355,7 +1347,7 @@
fix Z :: real
assume [arith]: "0 < Z"
then have "eventually (\<lambda>x. x < inverse Z) (nhds 0)"
- by (auto simp add: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
+ by (auto simp: eventually_nhds_metric dist_real_def intro!: exI[of _ "\<bar>inverse Z\<bar>"])
then show "eventually (\<lambda>x. x \<noteq> 0 \<longrightarrow> x \<in> {0<..} \<longrightarrow> Z \<le> inverse x) (nhds 0)"
by (auto elim!: eventually_mono simp: inverse_eq_divide field_simps)
qed
@@ -1563,10 +1555,7 @@
have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
by (fact tendsto_inverse_0)
then show "filtermap inverse at_infinity \<le> at (0::'a)"
- apply (simp add: le_principal eventually_filtermap eventually_at_infinity filterlim_def at_within_def)
- apply (rule_tac x="1" in exI)
- apply auto
- done
+ using filterlim_def filterlim_ident filterlim_inverse_at_iff by fastforce
next
have "filtermap inverse (filtermap inverse (at (0::'a))) \<le> filtermap inverse at_infinity"
using filterlim_inverse_at_infinity unfolding filterlim_def
@@ -1873,16 +1862,6 @@
unfolding tendsto_def eventually_sequentially
by (metis div_le_dividend div_mult_self1_is_m le_trans mult.commute)
-lemma norm_inverse_le_norm: "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
- for x :: "'a::real_normed_div_algebra"
- apply (subst nonzero_norm_inverse, clarsimp)
- apply (erule (1) le_imp_inverse_le)
- done
-
-lemma Bseq_inverse: "X \<longlonglongrightarrow> a \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> Bseq (\<lambda>n. inverse (X n))"
- for a :: "'a::real_normed_div_algebra"
- by (rule Bfun_inverse)
-
text \<open>Transformation of limit.\<close>
@@ -1900,11 +1879,7 @@
lemma Lim_transform_eventually:
"eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> l) net"
- apply (rule topological_tendstoI)
- apply (drule (2) topological_tendstoD)
- apply (erule (1) eventually_elim2)
- apply simp
- done
+ using eventually_elim2 by (fastforce simp add: tendsto_def)
lemma Lim_transform_within:
assumes "(f \<longlongrightarrow> l) (at x within S)"
@@ -1988,9 +1963,7 @@
assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
apply (rule filterlim_compose[OF tendsto_inverse_0])
- apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
- apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le)
- done
+ by (metis assms eventually_at_top_linorderI filterlim_at_top_dense filterlim_at_top_imp_at_infinity)
text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close>
lemma LIMSEQ_inverse_real_of_nat: "(\<lambda>n. inverse (real (Suc n))) \<longlonglongrightarrow> 0"
@@ -2261,18 +2234,11 @@
lemma Bseq_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> Bseq (\<lambda>n. x ^ n)"
for x :: real
- apply (simp add: Bseq_def)
- apply (rule_tac x = 1 in exI)
- apply (simp add: power_abs)
- apply (auto dest: power_mono)
- done
+ by (metis decseq_bounded decseq_def power_decreasing zero_le_power)
lemma monoseq_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> monoseq (\<lambda>n. x ^ n)"
for x :: real
- apply (clarify intro!: mono_SucI2)
- apply (cut_tac n = n and N = "Suc n" and a = x in power_decreasing)
- apply auto
- done
+ using monoseq_def power_decreasing by blast
lemma convergent_realpow: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> convergent (\<lambda>n. x ^ n)"
for x :: real
@@ -2303,9 +2269,7 @@
lemma LIMSEQ_power_zero: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
for x :: "'a::real_normed_algebra_1"
apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
- apply (simp only: tendsto_Zfun_iff, erule Zfun_le)
- apply (simp add: power_abs norm_power_ineq)
- done
+ by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff)
lemma LIMSEQ_divide_realpow_zero: "1 < x \<Longrightarrow> (\<lambda>n. a / (x ^ n) :: real) \<longlonglongrightarrow> 0"
by (rule tendsto_divide_0 [OF tendsto_const filterlim_realpow_sequentially_gt1]) simp
@@ -2327,7 +2291,7 @@
using \<open>filterlim f sequentially F\<close>
by (simp add: filterlim_at_top)
then show "\<forall>\<^sub>F i in F. dist (x ^ f i) 0 < e"
- by (eventually_elim) (auto simp: N)
+ by eventually_elim (auto simp: N)
qed
text \<open>Limit of @{term "c^n"} for @{term"\<bar>c\<bar> < 1"}.\<close>
@@ -2717,14 +2681,14 @@
shows "a \<le> b \<Longrightarrow> \<forall>x::real. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
\<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
using continuous_attains_sup[of "{a..b}" f]
- by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def)
+ by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def)
lemma isCont_eq_Lb:
fixes f :: "real \<Rightarrow> 'a::linorder_topology"
shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
\<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> M \<le> f x) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
using continuous_attains_inf[of "{a..b}" f]
- by (auto simp add: continuous_at_imp_continuous_on Ball_def Bex_def)
+ by (auto simp: continuous_at_imp_continuous_on Ball_def Bex_def)
lemma isCont_bounded:
fixes f :: "real \<Rightarrow> 'a::linorder_topology"
@@ -2760,16 +2724,20 @@
using isCont_eq_Ub[OF assms] by auto
obtain L where L: "a \<le> L" "L \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f L \<le> f x"
using isCont_eq_Lb[OF assms] by auto
- show ?thesis
- using IVT[of f L _ M] IVT2[of f L _ M] M L assms
- apply (rule_tac x="f L" in exI)
- apply (rule_tac x="f M" in exI)
- apply (cases "L \<le> M")
- apply simp
- apply (metis order_trans)
- apply simp
- apply (metis order_trans)
- done
+ have "(\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f L \<le> f x \<and> f x \<le> f M)"
+ using M L by simp
+ moreover
+ have "(\<forall>y. f L \<le> y \<and> y \<le> f M \<longrightarrow> (\<exists>x\<ge>a. x \<le> b \<and> f x = y))"
+ proof (cases "L \<le> M")
+ case True then show ?thesis
+ using IVT[of f L _ M] M L assms by (metis order.trans)
+ next
+ case False then show ?thesis
+ using IVT2[of f L _ M]
+ by (metis L(2) M(1) assms(2) le_cases order.trans)
+qed
+ ultimately show ?thesis
+ by blast
qed
@@ -2800,8 +2768,7 @@
using d inj by (intro continuous_inj_imp_mono[OF _ _ f] inj_on_imageI2[of g, OF inj_onI]) auto
then have "f x \<in> {min ?A ?B <..< max ?A ?B}"
by auto
- ultimately
- show ?thesis
+ ultimately show ?thesis
by (simp add: continuous_on_eq_continuous_at)
qed
@@ -2818,23 +2785,14 @@
text \<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110.\<close>
lemma LIM_fun_gt_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
for f :: "real \<Rightarrow> real"
- apply (drule (1) LIM_D)
- apply clarify
- apply (rule_tac x = s in exI)
- apply (simp add: abs_less_iff)
- done
+ by (force simp: dest: LIM_D)
lemma LIM_fun_less_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l < 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x < 0)"
for f :: "real \<Rightarrow> real"
- apply (drule LIM_D [where r="-l"])
- apply simp
- apply clarify
- apply (rule_tac x = s in exI)
- apply (simp add: abs_less_iff)
- done
+ by (drule LIM_D [where r="-l"]) force+
lemma LIM_fun_not_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> f x \<noteq> 0)"
for f :: "real \<Rightarrow> real"
- using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp add: neq_iff)
+ using LIM_fun_gt_zero[of f l c] LIM_fun_less_zero[of f l c] by (auto simp: neq_iff)
end
--- a/src/HOL/Quotient.thy Wed Jul 11 15:36:12 2018 +0100
+++ b/src/HOL/Quotient.thy Wed Jul 11 19:19:00 2018 +0100
@@ -349,11 +349,8 @@
apply(rule iffI)
apply(simp_all only: babs_rsp[OF q])
apply(auto simp add: Babs_def rel_fun_def)
- apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
- apply(metis Babs_def)
- apply (simp add: in_respects)
- using Quotient3_rel[OF q]
- by metis
+ apply(metis Babs_def in_respects Quotient3_rel[OF q])
+ done
(* If a user proves that a particular functional relation
is an equivalence this may be useful in regularising *)
@@ -401,51 +398,17 @@
lemma bex1_rel_aux:
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
unfolding Bex1_rel_def
- apply (erule conjE)+
- apply (erule bexE)
- apply rule
- apply (rule_tac x="xa" in bexI)
- apply metis
- apply metis
- apply rule+
- apply (erule_tac x="xaa" in ballE)
- prefer 2
- apply (metis)
- apply (erule_tac x="ya" in ballE)
- prefer 2
- apply (metis)
- apply (metis in_respects)
- done
+ by (metis in_respects)
lemma bex1_rel_aux2:
"\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
unfolding Bex1_rel_def
- apply (erule conjE)+
- apply (erule bexE)
- apply rule
- apply (rule_tac x="xa" in bexI)
- apply metis
- apply metis
- apply rule+
- apply (erule_tac x="xaa" in ballE)
- prefer 2
- apply (metis)
- apply (erule_tac x="ya" in ballE)
- prefer 2
- apply (metis)
- apply (metis in_respects)
- done
+ by (metis in_respects)
lemma bex1_rel_rsp:
assumes a: "Quotient3 R absf repf"
shows "((R ===> (=)) ===> (=)) (Bex1_rel R) (Bex1_rel R)"
- apply (simp add: rel_fun_def)
- apply clarify
- apply rule
- apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
- apply (erule bex1_rel_aux2)
- apply assumption
- done
+ unfolding rel_fun_def by (metis bex1_rel_aux bex1_rel_aux2)
lemma ex1_prs:
--- a/src/HOL/Real_Vector_Spaces.thy Wed Jul 11 15:36:12 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Wed Jul 11 19:19:00 2018 +0100
@@ -830,6 +830,11 @@
for a b :: "'a::{real_normed_field,field}"
by (simp add: divide_inverse norm_mult norm_inverse)
+lemma norm_inverse_le_norm:
+ fixes x :: "'a::real_normed_div_algebra"
+ shows "r \<le> norm x \<Longrightarrow> 0 < r \<Longrightarrow> norm (inverse x) \<le> inverse r"
+ by (simp add: le_imp_inverse_le norm_inverse)
+
lemma norm_power_ineq: "norm (x ^ n) \<le> norm x ^ n"
for x :: "'a::real_normed_algebra_1"
proof (induct n)