add simp rules for isCont
authorhuffman
Tue Aug 16 09:31:23 2011 -0700 (2011-08-16)
changeset 44233aa74ce315bae
parent 44229 7e3a026f014f
child 44234 17ae4af434aa
add simp rules for isCont
src/HOL/Deriv.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Lim.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Deriv.thy	Tue Aug 16 13:07:52 2011 -0700
     1.2 +++ b/src/HOL/Deriv.thy	Tue Aug 16 09:31:23 2011 -0700
     1.3 @@ -670,7 +670,7 @@
     1.4        |] ==> \<exists>x. a \<le> x & x \<le> b & f(x) = y"
     1.5  apply (subgoal_tac "- f a \<le> -y & -y \<le> - f b", clarify)
     1.6  apply (drule IVT [where f = "%x. - f x"], assumption)
     1.7 -apply (auto intro: isCont_minus)
     1.8 +apply simp_all
     1.9  done
    1.10  
    1.11  (*HOL style here: object-level formulations*)
    1.12 @@ -750,7 +750,7 @@
    1.13        with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
    1.14          by (fastsimp simp add: linorder_not_le [symmetric])
    1.15        hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
    1.16 -        by (auto simp add: isCont_inverse isCont_diff con)
    1.17 +        by (auto simp add: con)
    1.18        from isCont_bounded [OF le this]
    1.19        obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
    1.20        have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
    1.21 @@ -1059,8 +1059,8 @@
    1.22                     (f(b) - f(a) = (b-a) * l)"
    1.23  proof -
    1.24    let ?F = "%x. f x - ((f b - f a) / (b-a)) * x"
    1.25 -  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x" using con
    1.26 -    by (fast intro: isCont_diff isCont_const isCont_mult isCont_ident)
    1.27 +  have contF: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?F x"
    1.28 +    using con by (fast intro: isCont_intros)
    1.29    have difF: "\<forall>x. a < x \<and> x < b \<longrightarrow> ?F differentiable x"
    1.30    proof (clarify)
    1.31      fix x::real
    1.32 @@ -1353,7 +1353,7 @@
    1.33        ==> \<exists>z. \<bar>z-x\<bar> \<le> d & f z < f x"
    1.34  apply (insert lemma_isCont_inj
    1.35            [where f = "%x. - f x" and g = "%y. g(-y)" and x = x and d = d])
    1.36 -apply (simp add: isCont_minus linorder_not_le)
    1.37 +apply (simp add: linorder_not_le)
    1.38  done
    1.39  
    1.40  text{*Show there's an interval surrounding @{term "f(x)"} in
    1.41 @@ -1509,27 +1509,9 @@
    1.42    let ?h = "\<lambda>x. (f b - f a)*(g x) - (g b - g a)*(f x)"
    1.43    from assms have "a < b" by simp
    1.44    moreover have "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont ?h x"
    1.45 -  proof -
    1.46 -    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. f b - f a) x" by simp
    1.47 -    with gc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (f b - f a) * g x) x"
    1.48 -      by (auto intro: isCont_mult)
    1.49 -    moreover
    1.50 -    have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. g b - g a) x" by simp
    1.51 -    with fc have "\<forall>x. a <= x \<and> x <= b \<longrightarrow> isCont (\<lambda>x. (g b - g a) * f x) x"
    1.52 -      by (auto intro: isCont_mult)
    1.53 -    ultimately show ?thesis
    1.54 -      by (fastsimp intro: isCont_diff)
    1.55 -  qed
    1.56 -  moreover
    1.57 -  have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
    1.58 -  proof -
    1.59 -    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. f b - f a) differentiable x" by simp
    1.60 -    with gd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (f b - f a) * g x) differentiable x" by simp
    1.61 -    moreover
    1.62 -    have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. g b - g a) differentiable x" by simp
    1.63 -    with fd have "\<forall>x. a < x \<and> x < b \<longrightarrow> (\<lambda>x. (g b - g a) * f x) differentiable x" by simp
    1.64 -    ultimately show ?thesis by simp
    1.65 -  qed
    1.66 +    using fc gc by simp
    1.67 +  moreover have "\<forall>x. a < x \<and> x < b \<longrightarrow> ?h differentiable x"
    1.68 +    using fd gd by simp
    1.69    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)
    1.70    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" ..
    1.71    then obtain c where cdef: "a < c \<and> c < b \<and> DERIV ?h c :> l \<and> ?h b - ?h a = (b - a) * l" ..
     2.1 --- a/src/HOL/Library/Inner_Product.thy	Tue Aug 16 13:07:52 2011 -0700
     2.2 +++ b/src/HOL/Library/Inner_Product.thy	Tue Aug 16 09:31:23 2011 -0700
     2.3 @@ -175,6 +175,8 @@
     2.4    bounded_linear "\<lambda>y::'a::real_inner. inner x y"
     2.5    by (rule inner.bounded_linear_right)
     2.6  
     2.7 +declare inner.isCont [simp]
     2.8 +
     2.9  
    2.10  subsection {* Class instances *}
    2.11  
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 16 13:07:52 2011 -0700
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 16 09:31:23 2011 -0700
     3.3 @@ -359,6 +359,16 @@
     3.4         (simp add: subsetD [OF `A \<times> B \<subseteq> S`])
     3.5  qed
     3.6  
     3.7 +lemma isCont_fst [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. fst (f x)) a"
     3.8 +  unfolding isCont_def by (rule tendsto_fst)
     3.9 +
    3.10 +lemma isCont_snd [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. snd (f x)) a"
    3.11 +  unfolding isCont_def by (rule tendsto_snd)
    3.12 +
    3.13 +lemma isCont_Pair [simp]:
    3.14 +  "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
    3.15 +  unfolding isCont_def by (rule tendsto_Pair)
    3.16 +
    3.17  lemma Cauchy_fst: "Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. fst (X n))"
    3.18  unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le])
    3.19  
    3.20 @@ -381,10 +391,6 @@
    3.21    then show "\<exists>n0. \<forall>m\<ge>n0. \<forall>n\<ge>n0. dist (X m, Y m) (X n, Y n) < r" ..
    3.22  qed
    3.23  
    3.24 -lemma isCont_Pair [simp]:
    3.25 -  "\<lbrakk>isCont f x; isCont g x\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) x"
    3.26 -  unfolding isCont_def by (rule tendsto_Pair)
    3.27 -
    3.28  subsection {* Product is a complete metric space *}
    3.29  
    3.30  instance prod :: (complete_space, complete_space) complete_space
     4.1 --- a/src/HOL/Lim.thy	Tue Aug 16 13:07:52 2011 -0700
     4.2 +++ b/src/HOL/Lim.thy	Tue Aug 16 09:31:23 2011 -0700
     4.3 @@ -321,9 +321,6 @@
     4.4    "g -- a --> l \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> f l"
     4.5  by (rule tendsto)
     4.6  
     4.7 -lemma (in bounded_linear) cont: "f -- a --> f a"
     4.8 -by (rule LIM [OF LIM_ident])
     4.9 -
    4.10  lemma (in bounded_linear) LIM_zero:
    4.11    "g -- a --> 0 \<Longrightarrow> (\<lambda>x. f (g x)) -- a --> 0"
    4.12    by (rule tendsto_zero)
    4.13 @@ -401,39 +398,46 @@
    4.14  lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
    4.15    unfolding isCont_def by (rule LIM_const)
    4.16  
    4.17 -lemma isCont_norm:
    4.18 +lemma isCont_norm [simp]:
    4.19    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    4.20    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
    4.21    unfolding isCont_def by (rule LIM_norm)
    4.22  
    4.23 -lemma isCont_rabs: "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x :: real\<bar>) a"
    4.24 +lemma isCont_rabs [simp]:
    4.25 +  fixes f :: "'a::topological_space \<Rightarrow> real"
    4.26 +  shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. \<bar>f x\<bar>) a"
    4.27    unfolding isCont_def by (rule LIM_rabs)
    4.28  
    4.29 -lemma isCont_add:
    4.30 +lemma isCont_add [simp]:
    4.31    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    4.32    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"
    4.33    unfolding isCont_def by (rule LIM_add)
    4.34  
    4.35 -lemma isCont_minus:
    4.36 +lemma isCont_minus [simp]:
    4.37    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    4.38    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. - f x) a"
    4.39    unfolding isCont_def by (rule LIM_minus)
    4.40  
    4.41 -lemma isCont_diff:
    4.42 +lemma isCont_diff [simp]:
    4.43    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    4.44    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x - g x) a"
    4.45    unfolding isCont_def by (rule LIM_diff)
    4.46  
    4.47 -lemma isCont_mult:
    4.48 +lemma isCont_mult [simp]:
    4.49    fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_algebra"
    4.50    shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
    4.51    unfolding isCont_def by (rule LIM_mult)
    4.52  
    4.53 -lemma isCont_inverse:
    4.54 +lemma isCont_inverse [simp]:
    4.55    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
    4.56    shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
    4.57    unfolding isCont_def by (rule LIM_inverse)
    4.58  
    4.59 +lemma isCont_divide [simp]:
    4.60 +  fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_field"
    4.61 +  shows "\<lbrakk>isCont f a; isCont g a; g a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x / g x) a"
    4.62 +  unfolding isCont_def by (rule tendsto_divide)
    4.63 +
    4.64  lemma isCont_LIM_compose:
    4.65    "\<lbrakk>isCont g l; f -- a --> l\<rbrakk> \<Longrightarrow> (\<lambda>x. g (f x)) -- a --> g l"
    4.66    unfolding isCont_def by (rule LIM_compose)
    4.67 @@ -459,37 +463,40 @@
    4.68  lemma isCont_o: "\<lbrakk>isCont f a; isCont g (f a)\<rbrakk> \<Longrightarrow> isCont (g o f) a"
    4.69    unfolding o_def by (rule isCont_o2)
    4.70  
    4.71 -lemma (in bounded_linear) isCont: "isCont f a"
    4.72 -  unfolding isCont_def by (rule cont)
    4.73 +lemma (in bounded_linear) isCont:
    4.74 +  "isCont g a \<Longrightarrow> isCont (\<lambda>x. f (g x)) a"
    4.75 +  unfolding isCont_def by (rule LIM)
    4.76  
    4.77  lemma (in bounded_bilinear) isCont:
    4.78    "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x ** g x) a"
    4.79    unfolding isCont_def by (rule LIM)
    4.80  
    4.81 -lemmas isCont_scaleR = scaleR.isCont
    4.82 +lemmas isCont_scaleR [simp] = scaleR.isCont
    4.83  
    4.84 -lemma isCont_of_real:
    4.85 +lemma isCont_of_real [simp]:
    4.86    "isCont f a \<Longrightarrow> isCont (\<lambda>x. of_real (f x)::'b::real_normed_algebra_1) a"
    4.87 -  unfolding isCont_def by (rule LIM_of_real)
    4.88 +  by (rule of_real.isCont)
    4.89  
    4.90 -lemma isCont_power:
    4.91 +lemma isCont_power [simp]:
    4.92    fixes f :: "'a::topological_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    4.93    shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
    4.94    unfolding isCont_def by (rule LIM_power)
    4.95  
    4.96 -lemma isCont_sgn:
    4.97 +lemma isCont_sgn [simp]:
    4.98    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
    4.99    shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. sgn (f x)) a"
   4.100    unfolding isCont_def by (rule LIM_sgn)
   4.101  
   4.102 -lemma isCont_abs [simp]: "isCont abs (a::real)"
   4.103 -by (rule isCont_rabs [OF isCont_ident])
   4.104 +lemma isCont_setsum [simp]:
   4.105 +  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   4.106 +  fixes A :: "'a set"
   4.107 +  shows "\<forall>i\<in>A. isCont (f i) a \<Longrightarrow> isCont (\<lambda>x. \<Sum>i\<in>A. f i x) a"
   4.108 +  unfolding isCont_def by (simp add: tendsto_setsum)
   4.109  
   4.110 -lemma isCont_setsum:
   4.111 -  fixes f :: "'a \<Rightarrow> 'b::topological_space \<Rightarrow> 'c::real_normed_vector"
   4.112 -  fixes A :: "'a set" assumes "finite A"
   4.113 -  shows "\<forall> i \<in> A. isCont (f i) x \<Longrightarrow> isCont (\<lambda> x. \<Sum> i \<in> A. f i x) x"
   4.114 -  unfolding isCont_def by (simp add: tendsto_setsum)
   4.115 +lemmas isCont_intros =
   4.116 +  isCont_ident isCont_const isCont_norm isCont_rabs isCont_add isCont_minus
   4.117 +  isCont_diff isCont_mult isCont_inverse isCont_divide isCont_scaleR
   4.118 +  isCont_of_real isCont_power isCont_sgn isCont_setsum
   4.119  
   4.120  lemma LIM_less_bound: fixes f :: "real \<Rightarrow> real" assumes "b < x"
   4.121    and all_le: "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and isCont: "isCont f x"
     5.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
     5.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
     5.3 @@ -1100,8 +1100,7 @@
     5.4  unfolding continuous_on_def by (intro ballI tendsto_intros)
     5.5  
     5.6  lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}"
     5.7 -  unfolding Collect_all_eq
     5.8 -  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
     5.9 +  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
    5.10  
    5.11  lemma Lim_component_cart:
    5.12    fixes f :: "'a \<Rightarrow> 'b::metric_space ^ 'n"
    5.13 @@ -1287,13 +1286,11 @@
    5.14  
    5.15  lemma closed_interval_left_cart: fixes b::"real^'n"
    5.16    shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}"
    5.17 -  unfolding Collect_all_eq
    5.18 -  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    5.19 +  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
    5.20  
    5.21  lemma closed_interval_right_cart: fixes a::"real^'n"
    5.22    shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}"
    5.23 -  unfolding Collect_all_eq
    5.24 -  by (intro closed_INT ballI closed_Collect_le isCont_const vec_nth.isCont)
    5.25 +  by (simp add: Collect_all_eq closed_INT closed_Collect_le)
    5.26  
    5.27  lemma is_interval_cart:"is_interval (s::(real^'n) set) \<longleftrightarrow>
    5.28    (\<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)"
    5.29 @@ -1301,19 +1298,19 @@
    5.30  
    5.31  lemma closed_halfspace_component_le_cart:
    5.32    shows "closed {x::real^'n. x$i \<le> a}"
    5.33 -  by (intro closed_Collect_le vec_nth.isCont isCont_const)
    5.34 +  by (simp add: closed_Collect_le)
    5.35  
    5.36  lemma closed_halfspace_component_ge_cart:
    5.37    shows "closed {x::real^'n. x$i \<ge> a}"
    5.38 -  by (intro closed_Collect_le vec_nth.isCont isCont_const)
    5.39 +  by (simp add: closed_Collect_le)
    5.40  
    5.41  lemma open_halfspace_component_lt_cart:
    5.42    shows "open {x::real^'n. x$i < a}"
    5.43 -  by (intro open_Collect_less vec_nth.isCont isCont_const)
    5.44 +  by (simp add: open_Collect_less)
    5.45  
    5.46  lemma open_halfspace_component_gt_cart:
    5.47    shows "open {x::real^'n. x$i  > a}"
    5.48 -  by (intro open_Collect_less vec_nth.isCont isCont_const)
    5.49 +  by (simp add: open_Collect_less)
    5.50  
    5.51  lemma Lim_component_le_cart: fixes f :: "'a \<Rightarrow> real^'n"
    5.52    assumes "(f ---> l) net" "\<not> (trivial_limit net)"  "eventually (\<lambda>x. f(x)$i \<le> b) net"
    5.53 @@ -1352,8 +1349,7 @@
    5.54  proof-
    5.55    { fix i::'n
    5.56      have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}"
    5.57 -      by (cases "P i", simp_all,
    5.58 -        intro closed_Collect_eq vec_nth.isCont isCont_const) }
    5.59 +      by (cases "P i", simp_all add: closed_Collect_eq) }
    5.60    thus ?thesis
    5.61      unfolding Collect_all_eq by (simp add: closed_INT)
    5.62  qed
     6.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
     6.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
     6.3 @@ -124,6 +124,8 @@
     6.4    bounded_linear "\<lambda>x. euclidean_component x i"
     6.5    by (rule bounded_linear_euclidean_component)
     6.6  
     6.7 +declare euclidean_component.isCont [simp]
     6.8 +
     6.9  lemma euclidean_eqI:
    6.10    fixes x y :: "'a::euclidean_space"
    6.11    assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
     7.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Aug 16 13:07:52 2011 -0700
     7.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Tue Aug 16 09:31:23 2011 -0700
     7.3 @@ -408,6 +408,8 @@
     7.4  apply (rule_tac x="1" in exI, simp add: norm_nth_le)
     7.5  done
     7.6  
     7.7 +declare vec_nth.isCont [simp]
     7.8 +
     7.9  instance vec :: (banach, finite) banach ..
    7.10  
    7.11  
     8.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 16 13:07:52 2011 -0700
     8.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 16 09:31:23 2011 -0700
     8.3 @@ -5229,37 +5229,37 @@
     8.4    unfolding continuous_on by (rule ballI) (intro tendsto_intros)
     8.5  
     8.6  lemma closed_halfspace_le: "closed {x. inner a x \<le> b}"
     8.7 -  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
     8.8 +  by (simp add: closed_Collect_le)
     8.9  
    8.10  lemma closed_halfspace_ge: "closed {x. inner a x \<ge> b}"
    8.11 -  by (intro closed_Collect_le inner.isCont isCont_const isCont_ident)
    8.12 +  by (simp add: closed_Collect_le)
    8.13  
    8.14  lemma closed_hyperplane: "closed {x. inner a x = b}"
    8.15 -  by (intro closed_Collect_eq inner.isCont isCont_const isCont_ident)
    8.16 +  by (simp add: closed_Collect_eq)
    8.17  
    8.18  lemma closed_halfspace_component_le:
    8.19    shows "closed {x::'a::euclidean_space. x$$i \<le> a}"
    8.20 -  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
    8.21 +  by (simp add: closed_Collect_le)
    8.22  
    8.23  lemma closed_halfspace_component_ge:
    8.24    shows "closed {x::'a::euclidean_space. x$$i \<ge> a}"
    8.25 -  by (intro closed_Collect_le euclidean_component.isCont isCont_const)
    8.26 +  by (simp add: closed_Collect_le)
    8.27  
    8.28  text {* Openness of halfspaces. *}
    8.29  
    8.30  lemma open_halfspace_lt: "open {x. inner a x < b}"
    8.31 -  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
    8.32 +  by (simp add: open_Collect_less)
    8.33  
    8.34  lemma open_halfspace_gt: "open {x. inner a x > b}"
    8.35 -  by (intro open_Collect_less inner.isCont isCont_const isCont_ident)
    8.36 +  by (simp add: open_Collect_less)
    8.37  
    8.38  lemma open_halfspace_component_lt:
    8.39    shows "open {x::'a::euclidean_space. x$$i < a}"
    8.40 -  by (intro open_Collect_less euclidean_component.isCont isCont_const)
    8.41 +  by (simp add: open_Collect_less)
    8.42  
    8.43  lemma open_halfspace_component_gt:
    8.44    shows "open {x::'a::euclidean_space. x$$i > a}"
    8.45 -  by (intro open_Collect_less euclidean_component.isCont isCont_const)
    8.46 +  by (simp add: open_Collect_less)
    8.47  
    8.48  text{* Instantiation for intervals on @{text ordered_euclidean_space} *}
    8.49  
    8.50 @@ -5297,15 +5297,13 @@
    8.51    fixes a :: "'a\<Colon>ordered_euclidean_space"
    8.52    shows "closed {.. a}"
    8.53    unfolding eucl_atMost_eq_halfspaces
    8.54 -  by (intro closed_INT ballI closed_Collect_le
    8.55 -    euclidean_component.isCont isCont_const)
    8.56 +  by (simp add: closed_INT closed_Collect_le)
    8.57  
    8.58  lemma closed_eucl_atLeast[simp, intro]:
    8.59    fixes a :: "'a\<Colon>ordered_euclidean_space"
    8.60    shows "closed {a ..}"
    8.61    unfolding eucl_atLeast_eq_halfspaces
    8.62 -  by (intro closed_INT ballI closed_Collect_le
    8.63 -    euclidean_component.isCont isCont_const)
    8.64 +  by (simp add: closed_INT closed_Collect_le)
    8.65  
    8.66  lemma open_vimage_euclidean_component: "open S \<Longrightarrow> open ((\<lambda>x. x $$ i) -` S)"
    8.67    by (auto intro!: continuous_open_vimage)