--- a/src/HOL/Deriv.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Deriv.thy Tue Aug 16 09:31:23 2011 -0700
@@ -670,7 +670,7 @@
|] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
apply (drule IVT [where f = "%x. - f x"], assumption)
-apply (auto intro: isCont_minus)
+apply simp_all
done
(*HOL style here: object-level formulations*)
@@ -750,7 +750,7 @@
with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
by (fastsimp simp add: linorder_not_le [symmetric])
hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
- by (auto simp add: isCont_inverse isCont_diff con)
+ by (auto simp add: con)
from isCont_bounded [OF le this]
obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
@@ -1059,8 +1059,8 @@
(f(b) - f(a) = (b-a) * l)"
proof -
let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
- have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
- by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident)
+ have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
+ using con by (fast intro: isCont_intros)
have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
proof (clarify)
fix x::real
@@ -1353,7 +1353,7 @@
==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
apply (insert lemma_isCont_inj
[where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
-apply (simp add: isCont_minus linorder_not_le)
+apply (simp add: linorder_not_le)
done
text{*Show there's an interval surrounding @{term "f(x)"} in
@@ -1509,27 +1509,9 @@
let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
from assms have "a < b" by simp
moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
- proof -
- have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
- with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
- by (auto intro: isCont_mult)
- moreover
- have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
- with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
- by (auto intro: isCont_mult)
- ultimately show ?thesis
- by (fastsimp intro: isCont_diff)
- qed
- moreover
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
- proof -
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
- with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
- moreover
- have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
- with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
- ultimately show ?thesis by simp
- qed
+ using fc gc by simp
+ moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
+ using fd gd by simp
ultimately have "\<exists>l z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" by (rule MVT)
then obtain l where ldef: "\<exists>z. a < z \<and> z < b \<and> DERIV ?h z :> l \<and> ?h b - ?h a = (b - a) * l" ..
then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
--- a/src/HOL/Library/Inner_Product.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Library/Inner_Product.thy Tue Aug 16 09:31:23 2011 -0700
@@ -175,6 +175,8 @@
bounded_linear "\<lambda>y::'a::real_inner. inner x y"
by (rule inner.bounded_linear_right)
+declare inner.isCont [simp]
+
subsection {* Class instances *}
--- a/src/HOL/Library/Product_Vector.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy Tue Aug 16 09:31:23 2011 -0700
@@ -359,6 +359,16 @@
(simp add: subsetD [OF `A \<times> B \<subseteq> S`])
qed
+lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
+ unfolding isCont_def by (rule tendsto_fst)
+
+lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
+ unfolding isCont_def by (rule tendsto_snd)
+
+lemma isCont_Pair [simp]:
+ "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
+ unfolding isCont_def by (rule tendsto_Pair)
+
lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
@@ -381,10 +391,6 @@
then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
qed
-lemma isCont_Pair [simp]:
- "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
- unfolding isCont_def by (rule tendsto_Pair)
-
subsection {* Product is a complete metric space *}
instance prod :: (complete_space, complete_space) complete_space
--- a/src/HOL/Lim.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Lim.thy Tue Aug 16 09:31:23 2011 -0700
@@ -321,9 +321,6 @@
"g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
by (rule tendsto)
-lemma (in bounded_linear) cont: "f -- a --> f a"
-by (rule LIM [OF LIM_ident])
-
lemma (in bounded_linear) LIM_zero:
"g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
by (rule tendsto_zero)
@@ -401,39 +398,46 @@
lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
unfolding isCont_def by (rule LIM_const)
-lemma isCont_norm:
+lemma isCont_norm [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
unfolding isCont_def by (rule LIM_norm)
-lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
+lemma isCont_rabs [simp]:
+ fixes f :: "'a::topological_space \<Rightarrow> real"
+ shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
unfolding isCont_def by (rule LIM_rabs)
-lemma isCont_add:
+lemma isCont_add [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
unfolding isCont_def by (rule LIM_add)
-lemma isCont_minus:
+lemma isCont_minus [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
unfolding isCont_def by (rule LIM_minus)
-lemma isCont_diff:
+lemma isCont_diff [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
unfolding isCont_def by (rule LIM_diff)
-lemma isCont_mult:
+lemma isCont_mult [simp]:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
unfolding isCont_def by (rule LIM_mult)
-lemma isCont_inverse:
+lemma isCont_inverse [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
unfolding isCont_def by (rule LIM_inverse)
+lemma isCont_divide [simp]:
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
+ shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
+ unfolding isCont_def by (rule tendsto_divide)
+
lemma isCont_LIM_compose:
"\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
unfolding isCont_def by (rule LIM_compose)
@@ -459,37 +463,40 @@
lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
unfolding o_def by (rule isCont_o2)
-lemma (in bounded_linear) isCont: "isCont f a"
- unfolding isCont_def by (rule cont)
+lemma (in bounded_linear) isCont:
+ "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
+ unfolding isCont_def by (rule LIM)
lemma (in bounded_bilinear) isCont:
"\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
unfolding isCont_def by (rule LIM)
-lemmas isCont_scaleR = scaleR.isCont
+lemmas isCont_scaleR [simp] = scaleR.isCont
-lemma isCont_of_real:
+lemma isCont_of_real [simp]:
"isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
- unfolding isCont_def by (rule LIM_of_real)
+ by (rule of_real.isCont)
-lemma isCont_power:
+lemma isCont_power [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
unfolding isCont_def by (rule LIM_power)
-lemma isCont_sgn:
+lemma isCont_sgn [simp]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
unfolding isCont_def by (rule LIM_sgn)
-lemma isCont_abs [simp]: "isCont abs (a::real)"
-by (rule isCont_rabs [OF isCont_ident])
+lemma isCont_setsum [simp]:
+ fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
+ fixes A :: "'a set"
+ shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
+ unfolding isCont_def by (simp add: tendsto_setsum)
-lemma isCont_setsum:
- fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
- fixes A :: "'a set" assumes "finite A"
- shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
- unfolding isCont_def by (simp add: tendsto_setsum)
+lemmas isCont_intros =
+ isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
+ isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
+ isCont_of_real isCont_power isCont_sgn isCont_setsum
lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 16 09:31:23 2011 -0700
@@ -1100,8 +1100,7 @@
unfolding continuous_on_def by (intro ballI tendsto_intros)
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
- unfolding Collect_all_eq
- by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
+ by (simp add: Collect_all_eq closed_INT closed_Collect_le)
lemma Lim_component_cart:
fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
@@ -1287,13 +1286,11 @@
lemma closed_interval_left_cart: fixes b::"real^'n"
shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
- unfolding Collect_all_eq
- by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
+ by (simp add: Collect_all_eq closed_INT closed_Collect_le)
lemma closed_interval_right_cart: fixes a::"real^'n"
shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
- unfolding Collect_all_eq
- by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
+ by (simp add: Collect_all_eq closed_INT closed_Collect_le)
lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)"
@@ -1301,19 +1298,19 @@
lemma closed_halfspace_component_le_cart:
shows "closed {x::real^'n. x$i \<le> a}"
- by (intro closed_Collect_le vec_nth.isCont isCont_const)
+ by (simp add: closed_Collect_le)
lemma closed_halfspace_component_ge_cart:
shows "closed {x::real^'n. x$i \<ge> a}"
- by (intro closed_Collect_le vec_nth.isCont isCont_const)
+ by (simp add: closed_Collect_le)
lemma open_halfspace_component_lt_cart:
shows "open {x::real^'n. x$i < a}"
- by (intro open_Collect_less vec_nth.isCont isCont_const)
+ by (simp add: open_Collect_less)
lemma open_halfspace_component_gt_cart:
shows "open {x::real^'n. x$i > a}"
- by (intro open_Collect_less vec_nth.isCont isCont_const)
+ by (simp add: open_Collect_less)
lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f(x)$i \<le> b) net"
@@ -1352,8 +1349,7 @@
proof-
{ fix i::'n
have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
- by (cases "P i", simp_all,
- intro closed_Collect_eq vec_nth.isCont isCont_const) }
+ by (cases "P i", simp_all add: closed_Collect_eq) }
thus ?thesis
unfolding Collect_all_eq by (simp add: closed_INT)
qed
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 16 09:31:23 2011 -0700
@@ -124,6 +124,8 @@
bounded_linear "\<lambda>x. euclidean_component x i"
by (rule bounded_linear_euclidean_component)
+declare euclidean_component.isCont [simp]
+
lemma euclidean_eqI:
fixes x y :: "'a::euclidean_space"
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Tue Aug 16 09:31:23 2011 -0700
@@ -408,6 +408,8 @@
apply (rule_tac x="1" in exI, simp add: norm_nth_le)
done
+declare vec_nth.isCont [simp]
+
instance vec :: (banach, finite) banach ..
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 16 13:07:52 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 16 09:31:23 2011 -0700
@@ -5229,37 +5229,37 @@
unfolding continuous_on by (rule ballI) (intro tendsto_intros)
lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
- by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
+ by (simp add: closed_Collect_le)
lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
- by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
+ by (simp add: closed_Collect_le)
lemma closed_hyperplane: "closed {x. inner a x = b}"
- by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
+ by (simp add: closed_Collect_eq)
lemma closed_halfspace_component_le:
shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
- by (intro closed_Collect_le euclidean_component.isCont isCont_const)
+ by (simp add: closed_Collect_le)
lemma closed_halfspace_component_ge:
shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
- by (intro closed_Collect_le euclidean_component.isCont isCont_const)
+ by (simp add: closed_Collect_le)
text {* Openness of halfspaces. *}
lemma open_halfspace_lt: "open {x. inner a x < b}"
- by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
+ by (simp add: open_Collect_less)
lemma open_halfspace_gt: "open {x. inner a x > b}"
- by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
+ by (simp add: open_Collect_less)
lemma open_halfspace_component_lt:
shows "open {x::'a::euclidean_space. x$$i < a}"
- by (intro open_Collect_less euclidean_component.isCont isCont_const)
+ by (simp add: open_Collect_less)
lemma open_halfspace_component_gt:
shows "open {x::'a::euclidean_space. x$$i > a}"
- by (intro open_Collect_less euclidean_component.isCont isCont_const)
+ by (simp add: open_Collect_less)
text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
@@ -5297,15 +5297,13 @@
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {.. a}"
unfolding eucl_atMost_eq_halfspaces
- by (intro closed_INT ballI closed_Collect_le
- euclidean_component.isCont isCont_const)
+ by (simp add: closed_INT closed_Collect_le)
lemma closed_eucl_atLeast[simp, intro]:
fixes a :: "'a\<Colon>ordered_euclidean_space"
shows "closed {a ..}"
unfolding eucl_atLeast_eq_halfspaces
- by (intro closed_INT ballI closed_Collect_le
- euclidean_component.isCont isCont_const)
+ by (simp add: closed_INT closed_Collect_le)
lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
by (auto intro!: continuous_open_vimage)