--- a/src/HOL/Deriv.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Deriv.thy Fri Mar 22 10:41:43 2013 +0100
@@ -831,16 +831,7 @@
lemma lemma_MVT:
"f a - (f b - f a)/(b-a) * a = f b - (f b - f a)/(b-a) * (b::real)"
-proof cases
- assume "a=b" thus ?thesis by simp
-next
- assume "a\<noteq>b"
- hence ba: "b-a \<noteq> 0" by arith
- show ?thesis
- by (rule real_mult_left_cancel [OF ba, THEN iffD1],
- simp add: right_diff_distrib,
- simp add: left_diff_distrib)
-qed
+ by (cases "a = b") (simp_all add: field_simps)
theorem MVT:
assumes lt: "a < b"
@@ -1090,152 +1081,47 @@
by simp
qed
-subsection {* Continuous injective functions *}
-
-text{*Dull lemma: an continuous injection on an interval must have a
-strict maximum at an end point, not in the middle.*}
-
-lemma lemma_isCont_inj:
- fixes f :: "real \<Rightarrow> real"
- assumes d: "0 < d"
- and inj [rule_format]: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
- and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
- shows "\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z"
-proof (rule ccontr)
- assume "~ (\<exists>z. \<bar>z-x\<bar> \<le> d & f x < f z)"
- hence all [rule_format]: "\<forall>z. \<bar>z - x\<bar> \<le> d --> f z \<le> f x" by auto
- show False
- proof (cases rule: linorder_le_cases [of "f(x-d)" "f(x+d)"])
- case le
- from d cont all [of "x+d"]
- have flef: "f(x+d) \<le> f x"
- and xlex: "x - d \<le> x"
- and cont': "\<forall>z. x - d \<le> z \<and> z \<le> x \<longrightarrow> isCont f z"
- by (auto simp add: abs_if)
- from IVT [OF le flef xlex cont']
- obtain x' where "x-d \<le> x'" "x' \<le> x" "f x' = f(x+d)" by blast
- moreover
- hence "g(f x') = g (f(x+d))" by simp
- ultimately show False using d inj [of x'] inj [of "x+d"]
- by (simp add: abs_le_iff)
- next
- case ge
- from d cont all [of "x-d"]
- have flef: "f(x-d) \<le> f x"
- and xlex: "x \<le> x+d"
- and cont': "\<forall>z. x \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z"
- by (auto simp add: abs_if)
- from IVT2 [OF ge flef xlex cont']
- obtain x' where "x \<le> x'" "x' \<le> x+d" "f x' = f(x-d)" by blast
- moreover
- hence "g(f x') = g (f(x-d))" by simp
- ultimately show False using d inj [of x'] inj [of "x-d"]
- by (simp add: abs_le_iff)
- qed
-qed
-
-
-text{*Similar version for lower bound.*}
-
-lemma lemma_isCont_inj2:
- fixes f g :: "real \<Rightarrow> real"
- shows "[|0 < d; \<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z;
- \<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z |]
- ==> \<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: linorder_not_le)
-done
-
-text{*Show there's an interval surrounding @{term "f(x)"} in
-@{text "f[[x - d, x + d]]"} .*}
-
-lemma isCont_inj_range:
- fixes f :: "real \<Rightarrow> real"
- assumes d: "0 < d"
- and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
- and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
- shows "\<exists>e>0. \<forall>y. \<bar>y - f x\<bar> \<le> e --> (\<exists>z. \<bar>z-x\<bar> \<le> d & f z = y)"
-proof -
- have "x-d \<le> x+d" "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> isCont f z" using cont d
- by (auto simp add: abs_le_iff)
- from isCont_Lb_Ub [OF this]
- obtain L M
- where all1 [rule_format]: "\<forall>z. x-d \<le> z \<and> z \<le> x+d \<longrightarrow> L \<le> f z \<and> f z \<le> M"
- and all2 [rule_format]:
- "\<forall>y. L \<le> y \<and> y \<le> M \<longrightarrow> (\<exists>z. x-d \<le> z \<and> z \<le> x+d \<and> f z = y)"
- by auto
- with d have "L \<le> f x & f x \<le> M" by simp
- moreover have "L \<noteq> f x"
- proof -
- from lemma_isCont_inj2 [OF d inj cont]
- obtain u where "\<bar>u - x\<bar> \<le> d" "f u < f x" by auto
- thus ?thesis using all1 [of u] by arith
- qed
- moreover have "f x \<noteq> M"
- proof -
- from lemma_isCont_inj [OF d inj cont]
- obtain u where "\<bar>u - x\<bar> \<le> d" "f x < f u" by auto
- thus ?thesis using all1 [of u] by arith
- qed
- ultimately have "L < f x & f x < M" by arith
- hence "0 < f x - L" "0 < M - f x" by arith+
- from real_lbound_gt_zero [OF this]
- obtain e where e: "0 < e" "e < f x - L" "e < M - f x" by auto
- thus ?thesis
- proof (intro exI conjI)
- show "0<e" using e(1) .
- show "\<forall>y. \<bar>y - f x\<bar> \<le> e \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y)"
- proof (intro strip)
- fix y::real
- assume "\<bar>y - f x\<bar> \<le> e"
- with e have "L \<le> y \<and> y \<le> M" by arith
- from all2 [OF this]
- obtain z where "x - d \<le> z" "z \<le> x + d" "f z = y" by blast
- thus "\<exists>z. \<bar>z - x\<bar> \<le> d \<and> f z = y"
- by (force simp add: abs_le_iff)
- qed
- qed
-qed
-
-
text{*Continuity of inverse function*}
lemma isCont_inverse_function:
fixes f g :: "real \<Rightarrow> real"
assumes d: "0 < d"
- and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d --> g(f z) = z"
- and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d --> isCont f z"
+ and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
+ and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
shows "isCont g (f x)"
-proof (simp add: isCont_iff LIM_eq)
- show "\<forall>r. 0 < r \<longrightarrow>
- (\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r)"
- proof (intro strip)
- fix r::real
- assume r: "0<r"
- from real_lbound_gt_zero [OF r d]
- obtain e where e: "0 < e" and e_lt: "e < r \<and> e < d" by blast
- with inj cont
- have e_simps: "\<forall>z. \<bar>z-x\<bar> \<le> e --> g (f z) = z"
- "\<forall>z. \<bar>z-x\<bar> \<le> e --> isCont f z" by auto
- from isCont_inj_range [OF e this]
- obtain e' where e': "0 < e'"
- and all: "\<forall>y. \<bar>y - f x\<bar> \<le> e' \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)"
- by blast
- show "\<exists>s>0. \<forall>z. z\<noteq>0 \<and> \<bar>z\<bar> < s \<longrightarrow> \<bar>g(f x + z) - g(f x)\<bar> < r"
- proof (intro exI conjI)
- show "0<e'" using e' .
- show "\<forall>z. z \<noteq> 0 \<and> \<bar>z\<bar> < e' \<longrightarrow> \<bar>g (f x + z) - g (f x)\<bar> < r"
- proof (intro strip)
- fix z::real
- assume z: "z \<noteq> 0 \<and> \<bar>z\<bar> < e'"
- with e e_lt e_simps all [rule_format, of "f x + z"]
- show "\<bar>g (f x + z) - g (f x)\<bar> < r" by force
- qed
- qed
- qed
+proof -
+ let ?A = "f (x - d)" and ?B = "f (x + d)" and ?D = "{x - d..x + d}"
+
+ have f: "continuous_on ?D f"
+ using cont by (intro continuous_at_imp_continuous_on ballI) auto
+ then have g: "continuous_on (f`?D) g"
+ using inj by (intro continuous_on_inv) auto
+
+ from d f have "{min ?A ?B <..< max ?A ?B} \<subseteq> f ` ?D"
+ by (intro connected_contains_Ioo connected_continuous_image) (auto split: split_min split_max)
+ with g have "continuous_on {min ?A ?B <..< max ?A ?B} g"
+ by (rule continuous_on_subset)
+ moreover
+ have "(?A < f x \<and> f x < ?B) \<or> (?B < f x \<and> f x < ?A)"
+ 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
+ by (simp add: continuous_on_eq_continuous_at)
qed
+lemma isCont_inverse_function2:
+ fixes f g :: "real \<Rightarrow> real" shows
+ "\<lbrakk>a < x; x < b;
+ \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
+ \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
+ \<Longrightarrow> isCont g (f x)"
+apply (rule isCont_inverse_function
+ [where f=f and d="min (x - a) (b - x)"])
+apply (simp_all add: abs_le_iff)
+done
+
text {* Derivative of inverse function *}
lemma DERIV_inverse_function:
@@ -1285,7 +1171,6 @@
using neq by (rule tendsto_inverse)
qed
-
subsection {* Generalized Mean Value Theorem *}
theorem GMVT:
@@ -1355,21 +1240,6 @@
==> isCont g (f x)"
by (rule isCont_inverse_function)
-lemma isCont_inv_fun_inv:
- fixes f g :: "real \<Rightarrow> real"
- shows "[| 0 < d;
- \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;
- \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]
- ==> \<exists>e. 0 < e &
- (\<forall>y. 0 < \<bar>y - f(x)\<bar> & \<bar>y - f(x)\<bar> < e --> f(g(y)) = y)"
-apply (drule isCont_inj_range)
-prefer 2 apply (assumption, assumption, auto)
-apply (rule_tac x = e in exI, auto)
-apply (rotate_tac 2)
-apply (drule_tac x = y in spec, auto)
-done
-
-
text{*Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110*}
lemma LIM_fun_gt_zero:
"[| f -- c --> (l::real); 0 < l |]
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Fri Mar 22 10:41:43 2013 +0100
@@ -470,7 +470,7 @@
fixes f :: "'a::t2_space => real"
fixes A assumes "open A"
shows "continuous_on A f <-> continuous_on A (ereal o f)"
- using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at)
+ using continuous_at_iff_ereal assms by (auto simp add: continuous_on_eq_continuous_at cong del: continuous_on_cong)
lemma continuous_on_real: "continuous_on (UNIV-{\<infinity>,(-\<infinity>::ereal)}) real"
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Fri Mar 22 10:41:43 2013 +0100
@@ -8,14 +8,6 @@
imports Convex_Euclidean_Space
begin
-lemma continuous_on_cong: (* MOVE to Topological_Spaces *)
- "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
- unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto
-
-lemma continuous_on_compose2:
- shows "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
- using continuous_on_compose[of s f g] by (simp add: comp_def)
-
subsection {* Paths. *}
definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
@@ -126,7 +118,8 @@
have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
show "continuous_on {0..1} g1" "continuous_on {0..1} g2"
- unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont])
+ unfolding g1 g2
+ by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
next
assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
@@ -689,8 +682,8 @@
unfolding xy
apply (rule_tac x="f \<circ> g" in exI)
unfolding path_defs
- using assms(1)
- apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"])
+ apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)])
+ apply auto
done
qed
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Mar 22 10:41:43 2013 +0100
@@ -34,6 +34,24 @@
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (PiE I F)"
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
+lemma Lim_within_open:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
+ shows "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
+ by (fact tendsto_within_open)
+
+lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+ by (fact tendsto_within_subset)
+
+lemma continuous_on_union:
+ "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+ by (fact continuous_on_closed_Un)
+
+lemma continuous_on_cases:
+ "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t g \<Longrightarrow>
+ \<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x \<Longrightarrow>
+ continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
+ by (rule continuous_on_If) auto
+
subsection {* Topological Basis *}
context topological_space
@@ -1301,10 +1319,6 @@
lemma Lim_within_empty: "(f ---> l) (net within {})"
unfolding tendsto_def Limits.eventually_within by simp
-lemma Lim_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
- unfolding tendsto_def Topological_Spaces.eventually_within
- by (auto elim!: eventually_elim1)
-
lemma Lim_Un: assumes "(f ---> l) (net within S)" "(f ---> l) (net within T)"
shows "(f ---> l) (net within (S \<union> T))"
using assms unfolding tendsto_def Limits.eventually_within
@@ -1352,16 +1366,6 @@
"x \<in> interior S \<Longrightarrow> at x within S = at x"
by (simp add: filter_eq_iff eventually_within_interior)
-lemma at_within_open:
- "\<lbrakk>x \<in> S; open S\<rbrakk> \<Longrightarrow> at x within S = at x"
- by (simp only: at_within_interior interior_open)
-
-lemma Lim_within_open:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::topological_space"
- assumes"a \<in> S" "open S"
- shows "(f ---> l)(at a within S) \<longleftrightarrow> (f ---> l)(at a)"
- using assms by (simp only: at_within_open)
-
lemma Lim_within_LIMSEQ:
fixes a :: "'a::metric_space"
assumes "\<forall>S. (\<forall>n. S n \<noteq> a \<and> S n \<in> T) \<and> S ----> a \<longrightarrow> (\<lambda>n. X (S n)) ----> L"
@@ -2552,35 +2556,6 @@
thus ?thesis unfolding closed_sequential_limits by fast
qed
-lemma compact_imp_closed:
- fixes s :: "'a::t2_space set"
- assumes "compact s" shows "closed s"
-unfolding closed_def
-proof (rule openI)
- fix y assume "y \<in> - s"
- let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
- note `compact s`
- moreover have "\<forall>u\<in>?C. open u" by simp
- moreover have "s \<subseteq> \<Union>?C"
- proof
- fix x assume "x \<in> s"
- with `y \<in> - s` have "x \<noteq> y" by clarsimp
- hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
- by (rule hausdorff)
- with `x \<in> s` show "x \<in> \<Union>?C"
- unfolding eventually_nhds by auto
- qed
- ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
- by (rule compactE)
- from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
- with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
- by (simp add: eventually_Ball_finite)
- with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
- by (auto elim!: eventually_mono [rotated])
- thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
- by (simp add: eventually_nhds subset_eq)
-qed
-
lemma compact_imp_bounded:
assumes "compact U" shows "bounded U"
proof -
@@ -2614,20 +2589,6 @@
"finite A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> compact (B x)) \<Longrightarrow> compact (\<Union>x\<in>A. B x)"
unfolding SUP_def by (rule compact_Union) auto
-lemma compact_inter_closed [intro]:
- assumes "compact s" and "closed t"
- shows "compact (s \<inter> t)"
-proof (rule compactI)
- fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
- from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
- moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
- ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
- using `compact s` unfolding compact_eq_heine_borel by auto
- then guess D ..
- then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
- by (intro exI[of _ "D - {-t}"]) auto
-qed
-
lemma closed_inter_compact [intro]:
assumes "closed s" and "compact t"
shows "compact (s \<inter> t)"
@@ -3802,19 +3763,11 @@
lemmas continuous_on = continuous_on_def -- "legacy theorem name"
-lemma continuous_on_eq_continuous_at:
- shows "open s ==> (continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. continuous (at x) f))"
- by (auto simp add: continuous_on continuous_at Lim_within_open)
-
lemma continuous_within_subset:
"continuous (at x within s) f \<Longrightarrow> t \<subseteq> s
==> continuous (at x within t) f"
unfolding continuous_within by(metis Lim_within_subset)
-lemma continuous_on_subset:
- shows "continuous_on s f \<Longrightarrow> t \<subseteq> s ==> continuous_on t f"
- unfolding continuous_on by (metis subset_eq Lim_within_subset)
-
lemma continuous_on_interior:
shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
by (erule interiorE, drule (1) continuous_on_subset,
@@ -4087,70 +4040,18 @@
qed
lemma continuous_on_open:
- shows "continuous_on s f \<longleftrightarrow>
+ "continuous_on s f \<longleftrightarrow>
(\<forall>t. openin (subtopology euclidean (f ` s)) t
--> openin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof (safe)
- fix t :: "'b set"
- assume 1: "continuous_on s f"
- assume 2: "openin (subtopology euclidean (f ` s)) t"
- from 2 obtain B where B: "open B" and t: "t = f ` s \<inter> B"
- unfolding openin_open by auto
- def U == "\<Union>{A. open A \<and> (\<forall>x\<in>s. x \<in> A \<longrightarrow> f x \<in> B)}"
- have "open U" unfolding U_def by (simp add: open_Union)
- moreover have "\<forall>x\<in>s. x \<in> U \<longleftrightarrow> f x \<in> t"
- proof (intro ballI iffI)
- fix x assume "x \<in> s" and "x \<in> U" thus "f x \<in> t"
- unfolding U_def t by auto
- next
- fix x assume "x \<in> s" and "f x \<in> t"
- hence "x \<in> s" and "f x \<in> B"
- unfolding t by auto
- with 1 B obtain A where "open A" "x \<in> A" "\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B"
- unfolding t continuous_on_topological by metis
- then show "x \<in> U"
- unfolding U_def by auto
- qed
- ultimately have "open U \<and> {x \<in> s. f x \<in> t} = s \<inter> U" by auto
- then show "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}"
- unfolding openin_open by fast
-next
- assume "?rhs" show "continuous_on s f"
- unfolding continuous_on_topological
- proof (clarify)
- fix x and B assume "x \<in> s" and "open B" and "f x \<in> B"
- have "openin (subtopology euclidean (f ` s)) (f ` s \<inter> B)"
- unfolding openin_open using `open B` by auto
- then have "openin (subtopology euclidean s) {x \<in> s. f x \<in> f ` s \<inter> B}"
- using `?rhs` by fast
- then show "\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)"
- unfolding openin_open using `x \<in> s` and `f x \<in> B` by auto
- qed
-qed
+ unfolding continuous_on_open_invariant openin_open Int_def vimage_def Int_commute
+ by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
text {* Similarly in terms of closed sets. *}
lemma continuous_on_closed:
shows "continuous_on s f \<longleftrightarrow> (\<forall>t. closedin (subtopology euclidean (f ` s)) t --> closedin (subtopology euclidean s) {x \<in> s. f x \<in> t})" (is "?lhs = ?rhs")
-proof
- assume ?lhs
- { fix t
- have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
- have **:"f ` s - (f ` s - (f ` s - t)) = f ` s - t" by auto
- assume as:"closedin (subtopology euclidean (f ` s)) t"
- hence "closedin (subtopology euclidean (f ` s)) (f ` s - (f ` s - t))" unfolding closedin_def topspace_euclidean_subtopology unfolding ** by auto
- hence "closedin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?lhs`[unfolded continuous_on_open, THEN spec[where x="(f ` s) - t"]]
- unfolding openin_closedin_eq topspace_euclidean_subtopology unfolding * by auto }
- thus ?rhs by auto
-next
- assume ?rhs
- { fix t
- have *:"s - {x \<in> s. f x \<in> f ` s - t} = {x \<in> s. f x \<in> t}" by auto
- assume as:"openin (subtopology euclidean (f ` s)) t"
- hence "openin (subtopology euclidean s) {x \<in> s. f x \<in> t}" using `?rhs`[THEN spec[where x="(f ` s) - t"]]
- unfolding openin_closedin_eq topspace_euclidean_subtopology *[THEN sym] closedin_subtopology by auto }
- thus ?lhs unfolding continuous_on_open by auto
-qed
+ unfolding continuous_on_closed_invariant closedin_closed Int_def vimage_def Int_commute
+ by (simp add: imp_ex imageI conj_commute eq_commute cong: conj_cong)
text {* Half-global and completely global cases. *}
@@ -4544,38 +4445,6 @@
qed (insert D, auto)
qed auto
-text{* Continuity of inverse function on compact domain. *}
-
-lemma continuous_on_inv:
- fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
- assumes "continuous_on s f" "compact s" "\<forall>x \<in> s. g (f x) = x"
- shows "continuous_on (f ` s) g"
-unfolding continuous_on_topological
-proof (clarsimp simp add: assms(3))
- fix x :: 'a and B :: "'a set"
- assume "x \<in> s" and "open B" and "x \<in> B"
- have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
- using assms(3) by (auto, metis)
- have "continuous_on (s - B) f"
- using `continuous_on s f` Diff_subset
- by (rule continuous_on_subset)
- moreover have "compact (s - B)"
- using `open B` and `compact s`
- unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
- ultimately have "compact (f ` (s - B))"
- by (rule compact_continuous_image)
- hence "closed (f ` (s - B))"
- by (rule compact_imp_closed)
- hence "open (- f ` (s - B))"
- by (rule open_Compl)
- moreover have "f x \<in> - f ` (s - B)"
- using `x \<in> s` and `x \<in> B` by (simp add: 1)
- moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
- by (simp add: 1)
- ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
- by fast
-qed
-
text {* A uniformly convergent limit of continuous functions is continuous. *}
lemma continuous_uniform_limit:
@@ -5664,27 +5533,6 @@
(\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net)"
unfolding tendsto_def trivial_limit_eq by auto
-lemma continuous_on_union:
- assumes "closed s" "closed t" "continuous_on s f" "continuous_on t f"
- shows "continuous_on (s \<union> t) f"
- using assms unfolding continuous_on Lim_within_union
- unfolding Lim_topological trivial_limit_within closed_limpt by auto
-
-lemma continuous_on_cases:
- assumes "closed s" "closed t" "continuous_on s f" "continuous_on t g"
- "\<forall>x. (x\<in>s \<and> \<not> P x) \<or> (x \<in> t \<and> P x) \<longrightarrow> f x = g x"
- shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)"
-proof-
- let ?h = "(\<lambda>x. if P x then f x else g x)"
- have "\<forall>x\<in>s. f x = (if P x then f x else g x)" using assms(5) by auto
- hence "continuous_on s ?h" using continuous_on_eq[of s f ?h] using assms(3) by auto
- moreover
- have "\<forall>x\<in>t. g x = (if P x then f x else g x)" using assms(5) by auto
- hence "continuous_on t ?h" using continuous_on_eq[of t g ?h] using assms(4) by auto
- ultimately show ?thesis using continuous_on_union[OF assms(1,2), of ?h] by auto
-qed
-
-
text{* Some more convenient intermediate-value theorem formulations. *}
lemma connected_ivt_hyperplane:
--- a/src/HOL/RealVector.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/RealVector.thy Fri Mar 22 10:41:43 2013 +0100
@@ -950,6 +950,8 @@
end
+instance real :: linear_continuum_topology ..
+
lemma connectedI_interval:
fixes U :: "'a :: linear_continuum_topology set"
assumes *: "\<And>x y z. x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x \<le> z \<Longrightarrow> z \<le> y \<Longrightarrow> z \<in> U"
@@ -1068,6 +1070,27 @@
shows "f b \<le> y \<Longrightarrow> y \<le> f a \<Longrightarrow> a \<le> b \<Longrightarrow> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x) \<Longrightarrow> \<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y"
by (rule IVT2') (auto intro: continuous_at_imp_continuous_on)
-instance real :: linear_continuum_topology ..
+lemma continuous_inj_imp_mono:
+ fixes f :: "'a::linear_continuum_topology \<Rightarrow> 'b :: linorder_topology"
+ assumes x: "a < x" "x < b"
+ assumes cont: "continuous_on {a..b} f"
+ assumes inj: "inj_on f {a..b}"
+ shows "(f a < f x \<and> f x < f b) \<or> (f b < f x \<and> f x < f a)"
+proof -
+ note I = inj_on_iff[OF inj]
+ { assume "f x < f a" "f x < f b"
+ then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f x < f s"
+ using IVT'[of f x "min (f a) (f b)" b] IVT2'[of f x "min (f a) (f b)" a] x
+ by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+ with x I have False by auto }
+ moreover
+ { assume "f a < f x" "f b < f x"
+ then obtain s t where "x \<le> s" "s \<le> b" "a \<le> t" "t \<le> x" "f s = f t" "f s < f x"
+ using IVT'[of f a "max (f a) (f b)" x] IVT2'[of f b "max (f a) (f b)" x] x
+ by (auto simp: continuous_on_subset[OF cont] less_imp_le)
+ with x I have False by auto }
+ ultimately show ?thesis
+ using I[of a x] I[of x b] x less_trans[OF x] by (auto simp add: le_less less_imp_neq neq_iff)
+qed
end
--- a/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Mar 22 10:41:43 2013 +0100
@@ -724,6 +724,9 @@
"eventually P (at a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. x \<noteq> a \<longrightarrow> P x))"
unfolding at_def eventually_within eventually_nhds by simp
+lemma at_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> at a within S = at a"
+ unfolding filter_eq_iff eventually_within eventually_at_topological by (metis open_Int Int_iff)
+
lemma at_eq_bot_iff: "at a = bot \<longleftrightarrow> open {a}"
unfolding trivial_limit_def eventually_at_topological
by (safe, case_tac "S = {a}", simp, fast, fast)
@@ -869,6 +872,9 @@
by (auto elim!: allE[of _ "\<lambda>x. x \<in> S"] eventually_rev_mp)
qed (auto elim!: eventually_rev_mp simp: eventually_nhds eventually_filtermap le_filter_def)
+lemma tendsto_within_subset: "(f ---> l) (net within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f ---> l) (net within T)"
+ by (auto simp: tendsto_def eventually_within elim!: eventually_elim1)
+
lemma filterlim_at:
"(LIM x F. f x :> at b) \<longleftrightarrow> (eventually (\<lambda>x. f x \<noteq> b) F \<and> (f ---> b) F)"
by (simp add: at_def filterlim_within)
@@ -1540,6 +1546,9 @@
("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
"f -- a --> L \<equiv> (f ---> L) (at a)"
+lemma tendsto_within_open: "a \<in> S \<Longrightarrow> open S \<Longrightarrow> (f ---> l) (at a within S) \<longleftrightarrow> (f -- a --> l)"
+ unfolding tendsto_def by (simp add: at_within_open)
+
lemma LIM_const_not_eq[tendsto_intros]:
fixes a :: "'a::perfect_space"
fixes k L :: "'b::t2_space"
@@ -1629,6 +1638,10 @@
definition continuous_on :: "'a set \<Rightarrow> ('a :: topological_space \<Rightarrow> 'b :: topological_space) \<Rightarrow> bool" where
"continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. (f ---> f x) (at x within s))"
+lemma continuous_on_cong [cong]:
+ "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
+ unfolding continuous_on_def by (intro ball_cong filterlim_cong) (auto simp: eventually_within)
+
lemma continuous_on_topological:
"continuous_on s f \<longleftrightarrow>
(\<forall>x\<in>s. \<forall>B. open B \<longrightarrow> f x \<in> B \<longrightarrow> (\<exists>A. open A \<and> x \<in> A \<and> (\<forall>y\<in>s. y \<in> A \<longrightarrow> f y \<in> B)))"
@@ -1655,6 +1668,11 @@
qed
qed
+lemma continuous_on_open_vimage:
+ "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. open B \<longrightarrow> open (f -` B \<inter> s))"
+ unfolding continuous_on_open_invariant
+ by (metis open_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+
lemma continuous_on_closed_invariant:
"continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> (\<exists>A. closed A \<and> A \<inter> s = f -` B \<inter> s))"
proof -
@@ -1664,6 +1682,36 @@
unfolding continuous_on_open_invariant by (intro *) (auto simp: open_closed[symmetric])
qed
+lemma continuous_on_closed_vimage:
+ "closed s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>B. closed B \<longrightarrow> closed (f -` B \<inter> s))"
+ unfolding continuous_on_closed_invariant
+ by (metis closed_Int Int_absorb Int_commute[of s] Int_assoc[of _ _ s])
+
+lemma continuous_on_open_Union:
+ "(\<And>s. s \<in> S \<Longrightarrow> open s) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on s f) \<Longrightarrow> continuous_on (\<Union>S) f"
+ unfolding continuous_on_def by (simp add: tendsto_within_open open_Union)
+
+lemma continuous_on_open_UN:
+ "(\<And>s. s \<in> S \<Longrightarrow> open (A s)) \<Longrightarrow> (\<And>s. s \<in> S \<Longrightarrow> continuous_on (A s) f) \<Longrightarrow> continuous_on (\<Union>s\<in>S. A s) f"
+ unfolding Union_image_eq[symmetric] by (rule continuous_on_open_Union) auto
+
+lemma continuous_on_closed_Un:
+ "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
+ by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
+
+lemma continuous_on_If:
+ assumes closed: "closed s" "closed t" and cont: "continuous_on s f" "continuous_on t g"
+ and P: "\<And>x. x \<in> s \<Longrightarrow> \<not> P x \<Longrightarrow> f x = g x" "\<And>x. x \<in> t \<Longrightarrow> P x \<Longrightarrow> f x = g x"
+ shows "continuous_on (s \<union> t) (\<lambda>x. if P x then f x else g x)" (is "continuous_on _ ?h")
+proof-
+ from P have "\<forall>x\<in>s. f x = ?h x" "\<forall>x\<in>t. g x = ?h x"
+ by auto
+ with cont have "continuous_on s ?h" "continuous_on t ?h"
+ by simp_all
+ with closed show ?thesis
+ by (rule continuous_on_closed_Un)
+qed
+
ML {*
structure Continuous_On_Intros = Named_Thms
@@ -1686,6 +1734,10 @@
"continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
unfolding continuous_on_topological by simp metis
+lemma continuous_on_compose2:
+ "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
+ using continuous_on_compose[of s f g] by (simp add: comp_def)
+
subsubsection {* Continuity at a point *}
definition continuous :: "'a::t2_space filter \<Rightarrow> ('a \<Rightarrow> 'b::topological_space) \<Rightarrow> bool" where
@@ -1749,6 +1801,12 @@
lemma continuous_at_within: "isCont f x \<Longrightarrow> continuous (at x within s) f"
by (auto intro: within_le filterlim_mono simp: continuous_at continuous_within)
+lemma continuous_on_eq_continuous_at: "open s \<Longrightarrow> continuous_on s f \<longleftrightarrow> (\<forall>x\<in>s. isCont f x)"
+ by (simp add: continuous_on_def continuous_at tendsto_within_open)
+
+lemma continuous_on_subset: "continuous_on s f \<Longrightarrow> t \<subseteq> s \<Longrightarrow> continuous_on t f"
+ unfolding continuous_on_def by (metis subset_eq tendsto_within_subset)
+
lemma continuous_at_imp_continuous_on: "\<forall>x\<in>s. isCont f x \<Longrightarrow> continuous_on s f"
by (auto intro: continuous_at_within simp: continuous_on_eq_continuous_within)
@@ -1801,8 +1859,101 @@
using assms unfolding ball_simps[symmetric] SUP_def
by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
+lemma compact_inter_closed [intro]:
+ assumes "compact s" and "closed t"
+ shows "compact (s \<inter> t)"
+proof (rule compactI)
+ fix C assume C: "\<forall>c\<in>C. open c" and cover: "s \<inter> t \<subseteq> \<Union>C"
+ from C `closed t` have "\<forall>c\<in>C \<union> {-t}. open c" by auto
+ moreover from cover have "s \<subseteq> \<Union>(C \<union> {-t})" by auto
+ ultimately have "\<exists>D\<subseteq>C \<union> {-t}. finite D \<and> s \<subseteq> \<Union>D"
+ using `compact s` unfolding compact_eq_heine_borel by auto
+ then guess D ..
+ then show "\<exists>D\<subseteq>C. finite D \<and> s \<inter> t \<subseteq> \<Union>D"
+ by (intro exI[of _ "D - {-t}"]) auto
+qed
+
end
+lemma (in t2_space) compact_imp_closed:
+ assumes "compact s" shows "closed s"
+unfolding closed_def
+proof (rule openI)
+ fix y assume "y \<in> - s"
+ let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
+ note `compact s`
+ moreover have "\<forall>u\<in>?C. open u" by simp
+ moreover have "s \<subseteq> \<Union>?C"
+ proof
+ fix x assume "x \<in> s"
+ with `y \<in> - s` have "x \<noteq> y" by clarsimp
+ hence "\<exists>u v. open u \<and> open v \<and> x \<in> u \<and> y \<in> v \<and> u \<inter> v = {}"
+ by (rule hausdorff)
+ with `x \<in> s` show "x \<in> \<Union>?C"
+ unfolding eventually_nhds by auto
+ qed
+ ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
+ by (rule compactE)
+ from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
+ with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
+ by (simp add: eventually_Ball_finite)
+ with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
+ by (auto elim!: eventually_mono [rotated])
+ thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"
+ by (simp add: eventually_nhds subset_eq)
+qed
+
+lemma compact_continuous_image:
+ assumes f: "continuous_on s f" and s: "compact s"
+ shows "compact (f ` s)"
+proof (rule compactI)
+ fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
+ with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
+ unfolding continuous_on_open_invariant by blast
+ then guess A unfolding bchoice_iff .. note A = this
+ with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
+ by (fastforce simp add: subset_eq set_eq_iff)+
+ from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
+ with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
+ by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
+qed
+
+lemma continuous_on_inv:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+ assumes "continuous_on s f" "compact s" "\<forall>x\<in>s. g (f x) = x"
+ shows "continuous_on (f ` s) g"
+unfolding continuous_on_topological
+proof (clarsimp simp add: assms(3))
+ fix x :: 'a and B :: "'a set"
+ assume "x \<in> s" and "open B" and "x \<in> B"
+ have 1: "\<forall>x\<in>s. f x \<in> f ` (s - B) \<longleftrightarrow> x \<in> s - B"
+ using assms(3) by (auto, metis)
+ have "continuous_on (s - B) f"
+ using `continuous_on s f` Diff_subset
+ by (rule continuous_on_subset)
+ moreover have "compact (s - B)"
+ using `open B` and `compact s`
+ unfolding Diff_eq by (intro compact_inter_closed closed_Compl)
+ ultimately have "compact (f ` (s - B))"
+ by (rule compact_continuous_image)
+ hence "closed (f ` (s - B))"
+ by (rule compact_imp_closed)
+ hence "open (- f ` (s - B))"
+ by (rule open_Compl)
+ moreover have "f x \<in> - f ` (s - B)"
+ using `x \<in> s` and `x \<in> B` by (simp add: 1)
+ moreover have "\<forall>y\<in>s. f y \<in> - f ` (s - B) \<longrightarrow> y \<in> B"
+ by (simp add: 1)
+ ultimately show "\<exists>A. open A \<and> f x \<in> A \<and> (\<forall>y\<in>s. f y \<in> A \<longrightarrow> y \<in> B)"
+ by fast
+qed
+
+lemma continuous_on_inv_into:
+ fixes f :: "'a::topological_space \<Rightarrow> 'b::t2_space"
+ assumes s: "continuous_on s f" "compact s" and f: "inj_on f s"
+ shows "continuous_on (f ` s) (the_inv_into s f)"
+ by (rule continuous_on_inv[OF s]) (auto simp: the_inv_into_f_f[OF f])
+
lemma (in linorder_topology) compact_attains_sup:
assumes "compact S" "S \<noteq> {}"
shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
@@ -1841,21 +1992,6 @@
by fastforce
qed
-lemma compact_continuous_image:
- assumes f: "continuous_on s f" and s: "compact s"
- shows "compact (f ` s)"
-proof (rule compactI)
- fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
- with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
- unfolding continuous_on_open_invariant by blast
- then guess A unfolding bchoice_iff .. note A = this
- with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
- by (fastforce simp add: subset_eq set_eq_iff)+
- from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
- with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
- by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
-qed
-
lemma continuous_attains_sup:
fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f y \<le> f x)"
--- a/src/HOL/Transcendental.thy Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Transcendental.thy Fri Mar 22 10:41:43 2013 +0100
@@ -2457,17 +2457,6 @@
lemma arctan_eq_zero_iff [simp]: "arctan x = 0 \<longleftrightarrow> x = 0"
using arctan_eq_iff [of x 0] by simp
-lemma isCont_inverse_function2: (* generalize with continuous_on *)
- fixes f g :: "real \<Rightarrow> real" shows
- "\<lbrakk>a < x; x < b;
- \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z;
- \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z\<rbrakk>
- \<Longrightarrow> isCont g (f x)"
-apply (rule isCont_inverse_function
- [where f=f and d="min (x - a) (b - x)"])
-apply (simp_all add: abs_le_iff)
-done
-
lemma isCont_arcsin: "\<lbrakk>-1 < x; x < 1\<rbrakk> \<Longrightarrow> isCont arcsin x" (* generalize with continuous_on {-1 .. 1} *)
apply (subgoal_tac "isCont arcsin (sin (arcsin x))", simp)
apply (rule isCont_inverse_function2 [where f=sin])