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