# HG changeset patch
# User huffman
# Date 1313512283 25200
# Node ID aa74ce315bae6d57a9bd673606711d81f95c0d5f
# Parent  7e3a026f014f9ffee882a05359ea1608179e2f8d
add simp rules for isCont

diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Deriv.thy
--- 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" ..
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Library/Inner_Product.thy
--- 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 *}
 
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Library/Product_Vector.thy
--- 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
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Lim.thy
--- 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"
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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"
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- 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 ..
 
 
diff -r 7e3a026f014f -r aa74ce315bae src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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)