diff -r 3793c3a11378 -r ef949192e5d6 src/HOL/Multivariate_Analysis/Path_Connected.thy --- 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 \ (\x. x \ t \ f x = g x) \ continuous_on s f \ 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 \ continuous_on s f \ t = f ` s \ continuous_on s (\x. g (f x))" - using continuous_on_compose[of s f g] by (simp add: comp_def) - subsection {* Paths. *} definition path :: "(real \ 'a::topological_space) \ bool" @@ -126,7 +118,8 @@ have g2: "continuous_on {0..1} g2 \ continuous_on {0..1} ((g1 +++ g2) \ (\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} \ {1/2 .. 1::real}" @@ -689,8 +682,8 @@ unfolding xy apply (rule_tac x="f \ 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