author huffman Tue, 16 Aug 2011 09:31:23 -0700 changeset 44233 aa74ce315bae parent 44229 7e3a026f014f child 44234 17ae4af434aa
```--- 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])
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)

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"

-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)

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)

lemma open_halfspace_component_lt_cart:
shows "open {x::real^'n. x\$i < a}"
-  by (intro open_Collect_less vec_nth.isCont isCont_const)

lemma open_halfspace_component_gt_cart:
shows "open {x::real^'n. x\$i  > a}"
-  by (intro open_Collect_less vec_nth.isCont isCont_const)

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)

lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
-  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)

lemma closed_hyperplane: "closed {x. inner a x = b}"
-  by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)

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)

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)

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)

lemma open_halfspace_gt: "open {x. inner a x > b}"
-  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)

lemma open_halfspace_component_lt:
shows "open {x::'a::euclidean_space. x\$\$i < a}"
-  by (intro open_Collect_less euclidean_component.isCont isCont_const)

lemma open_halfspace_component_gt:
shows "open {x::'a::euclidean_space. x\$\$i > a}"
-  by (intro open_Collect_less euclidean_component.isCont isCont_const)

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)```