src/HOL/Multivariate_Analysis/Path_Connected.thy
 changeset 51481 ef949192e5d6 parent 51478 270b21f3ae0a child 53593 a7bcbb5a17d8
```     1.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
1.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri Mar 22 10:41:43 2013 +0100
1.3 @@ -8,14 +8,6 @@
1.4  imports Convex_Euclidean_Space
1.5  begin
1.6
1.7 -lemma continuous_on_cong: (* MOVE to Topological_Spaces *)
1.8 -  "s = t \<Longrightarrow> (\<And>x. x \<in> t \<Longrightarrow> f x = g x) \<Longrightarrow> continuous_on s f \<longleftrightarrow> continuous_on t g"
1.9 -  unfolding continuous_on_def by (intro ball_cong Lim_cong_within) auto
1.10 -
1.11 -lemma continuous_on_compose2:
1.12 -  shows "continuous_on t g \<Longrightarrow> continuous_on s f \<Longrightarrow> t = f ` s \<Longrightarrow> continuous_on s (\<lambda>x. g (f x))"
1.13 -  using continuous_on_compose[of s f g] by (simp add: comp_def)
1.14 -
1.15  subsection {* Paths. *}
1.16
1.17  definition path :: "(real \<Rightarrow> 'a::topological_space) \<Rightarrow> bool"
1.18 @@ -126,7 +118,8 @@
1.19    have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))"
1.20      using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def)
1.21    show "continuous_on {0..1} g1" "continuous_on {0..1} g2"
1.22 -    unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont])
1.23 +    unfolding g1 g2
1.24 +    by (auto intro!: continuous_on_intros continuous_on_subset[OF cont] simp del: o_apply)
1.25  next
1.26    assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2"
1.27    have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}"
1.28 @@ -689,8 +682,8 @@
1.29      unfolding xy
1.30      apply (rule_tac x="f \<circ> g" in exI)
1.31      unfolding path_defs
1.32 -    using assms(1)
1.33 -    apply (auto intro!: continuous_on_compose continuous_on_subset[of _ _ "g ` {0..1}"])
1.34 +    apply (intro conjI continuous_on_compose continuous_on_subset[OF assms(1)])
1.35 +    apply auto
1.36      done
1.37  qed
1.38
```