109 |
117 |
110 lemma path_join[simp]: |
118 lemma path_join[simp]: |
111 assumes "pathfinish g1 = pathstart g2" |
119 assumes "pathfinish g1 = pathstart g2" |
112 shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2" |
120 shows "path (g1 +++ g2) \<longleftrightarrow> path g1 \<and> path g2" |
113 unfolding path_def pathfinish_def pathstart_def |
121 unfolding path_def pathfinish_def pathstart_def |
114 apply rule defer |
122 proof safe |
115 apply(erule conjE) |
123 assume cont: "continuous_on {0..1} (g1 +++ g2)" |
116 proof - |
124 have g1: "continuous_on {0..1} g1 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2))" |
117 assume as: "continuous_on {0..1} (g1 +++ g2)" |
125 by (intro continuous_on_cong refl) (auto simp: joinpaths_def) |
118 have *: "g1 = (\<lambda>x. g1 (2 *\<^sub>R x)) \<circ> (\<lambda>x. (1/2) *\<^sub>R x)" |
126 have g2: "continuous_on {0..1} g2 \<longleftrightarrow> continuous_on {0..1} ((g1 +++ g2) \<circ> (\<lambda>x. x / 2 + 1/2))" |
119 "g2 = (\<lambda>x. g2 (2 *\<^sub>R x - 1)) \<circ> (\<lambda>x. (1/2) *\<^sub>R (x + 1))" |
127 using assms by (intro continuous_on_cong refl) (auto simp: joinpaths_def pathfinish_def pathstart_def) |
120 unfolding o_def by (auto simp add: add_divide_distrib) |
128 show "continuous_on {0..1} g1" "continuous_on {0..1} g2" |
121 have "op *\<^sub>R (1 / 2) ` {0::real..1} \<subseteq> {0..1}" |
129 unfolding g1 g2 by (auto intro!: continuous_on_intros continuous_on_subset[OF cont]) |
122 "(\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {(0::real)..1} \<subseteq> {0..1}" |
130 next |
|
131 assume g1g2: "continuous_on {0..1} g1" "continuous_on {0..1} g2" |
|
132 have 01: "{0 .. 1} = {0..1/2} \<union> {1/2 .. 1::real}" |
123 by auto |
133 by auto |
124 then show "continuous_on {0..1} g1 \<and> continuous_on {0..1} g2" |
134 { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2) ` {0..1 / 2}" |
125 apply - |
135 by (intro image_eqI[where x="x/2"]) auto } |
126 apply rule |
136 note 1 = this |
127 apply (subst *) defer |
137 { fix x :: real assume "0 \<le> x" "x \<le> 1" then have "x \<in> (\<lambda>x. x * 2 - 1) ` {1 / 2..1}" |
128 apply (subst *) |
138 by (intro image_eqI[where x="x/2 + 1/2"]) auto } |
129 apply (rule_tac[!] continuous_on_compose) |
139 note 2 = this |
130 apply (intro continuous_on_intros) defer |
|
131 apply (intro continuous_on_intros) |
|
132 apply (rule_tac[!] continuous_on_eq[of _ "g1 +++ g2"]) defer prefer 3 |
|
133 apply (rule_tac[1-2] continuous_on_subset[of "{0 .. 1}"]) |
|
134 apply (rule as, assumption, rule as, assumption) |
|
135 apply rule defer |
|
136 apply rule |
|
137 proof - |
|
138 fix x |
|
139 assume "x \<in> op *\<^sub>R (1 / 2) ` {0::real..1}" |
|
140 then have "x \<le> 1 / 2" unfolding image_iff by auto |
|
141 then show "(g1 +++ g2) x = g1 (2 *\<^sub>R x)" unfolding joinpaths_def by auto |
|
142 next |
|
143 fix x |
|
144 assume "x \<in> (\<lambda>x. (1 / 2) *\<^sub>R (x + 1)) ` {0::real..1}" |
|
145 then have "x \<ge> 1 / 2" unfolding image_iff by auto |
|
146 then show "(g1 +++ g2) x = g2 (2 *\<^sub>R x - 1)" |
|
147 proof (cases "x = 1 / 2") |
|
148 case True |
|
149 then have "x = (1/2) *\<^sub>R 1" by auto |
|
150 then show ?thesis |
|
151 unfolding joinpaths_def |
|
152 using assms[unfolded pathstart_def pathfinish_def] |
|
153 by (auto simp add: mult_ac) |
|
154 qed (auto simp add:le_less joinpaths_def) |
|
155 qed |
|
156 next |
|
157 assume as:"continuous_on {0..1} g1" "continuous_on {0..1} g2" |
|
158 have *: "{0 .. 1::real} = {0.. (1/2)*\<^sub>R 1} \<union> {(1/2) *\<^sub>R 1 .. 1}" by auto |
|
159 have **: "op *\<^sub>R 2 ` {0..(1 / 2) *\<^sub>R 1} = {0..1::real}" |
|
160 apply (rule set_eqI, rule) |
|
161 unfolding image_iff |
|
162 defer |
|
163 apply (rule_tac x="(1/2)*\<^sub>R x" in bexI) |
|
164 apply auto |
|
165 done |
|
166 have ***: "(\<lambda>x. 2 *\<^sub>R x - 1) ` {(1 / 2) *\<^sub>R 1..1} = {0..1::real}" |
|
167 apply (auto simp add: image_def) |
|
168 apply (rule_tac x="(x + 1) / 2" in bexI) |
|
169 apply (auto simp add: add_divide_distrib) |
|
170 done |
|
171 show "continuous_on {0..1} (g1 +++ g2)" |
140 show "continuous_on {0..1} (g1 +++ g2)" |
172 unfolding * |
141 using assms unfolding joinpaths_def 01 |
173 apply (rule continuous_on_union) |
142 by (intro continuous_on_cases closed_atLeastAtMost g1g2[THEN continuous_on_compose2] continuous_on_intros) |
174 apply (rule closed_real_atLeastAtMost)+ |
143 (auto simp: field_simps pathfinish_def pathstart_def intro!: 1 2) |
175 proof - |
|
176 show "continuous_on {0..(1 / 2) *\<^sub>R 1} (g1 +++ g2)" |
|
177 apply (rule continuous_on_eq[of _ "\<lambda>x. g1 (2 *\<^sub>R x)"]) defer |
|
178 unfolding o_def[THEN sym] |
|
179 apply (rule continuous_on_compose) |
|
180 apply (intro continuous_on_intros) |
|
181 unfolding ** |
|
182 apply (rule as(1)) |
|
183 unfolding joinpaths_def |
|
184 apply auto |
|
185 done |
|
186 next |
|
187 show "continuous_on {(1/2)*\<^sub>R1..1} (g1 +++ g2)" |
|
188 apply (rule continuous_on_eq[of _ "g2 \<circ> (\<lambda>x. 2 *\<^sub>R x - 1)"]) defer |
|
189 apply (rule continuous_on_compose) |
|
190 apply (intro continuous_on_intros) |
|
191 unfolding *** o_def joinpaths_def |
|
192 apply (rule as(2)) |
|
193 using assms[unfolded pathstart_def pathfinish_def] |
|
194 apply (auto simp add: mult_ac) |
|
195 done |
|
196 qed |
|
197 qed |
144 qed |
198 |
145 |
199 lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)" |
146 lemma path_image_join_subset: "path_image(g1 +++ g2) \<subseteq> (path_image g1 \<union> path_image g2)" |
200 proof |
147 unfolding path_image_def joinpaths_def by auto |
201 fix x |
|
202 assume "x \<in> path_image (g1 +++ g2)" |
|
203 then obtain y where y:"y\<in>{0..1}" "x = (if y \<le> 1 / 2 then g1 (2 *\<^sub>R y) else g2 (2 *\<^sub>R y - 1))" |
|
204 unfolding path_image_def image_iff joinpaths_def by auto |
|
205 then show "x \<in> path_image g1 \<union> path_image g2" |
|
206 apply (cases "y \<le> 1/2") |
|
207 apply (rule_tac UnI1) defer |
|
208 apply (rule_tac UnI2) |
|
209 unfolding y(2) path_image_def |
|
210 using y(1) |
|
211 apply (auto intro!: imageI) |
|
212 done |
|
213 qed |
|
214 |
148 |
215 lemma subset_path_image_join: |
149 lemma subset_path_image_join: |
216 assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s" |
150 assumes "path_image g1 \<subseteq> s" "path_image g2 \<subseteq> s" |
217 shows "path_image(g1 +++ g2) \<subseteq> s" |
151 shows "path_image(g1 +++ g2) \<subseteq> s" |
218 using path_image_join_subset[of g1 g2] and assms by auto |
152 using path_image_join_subset[of g1 g2] and assms by auto |
219 |
153 |
220 lemma path_image_join: |
154 lemma path_image_join: |
221 assumes "path g1" "path g2" "pathfinish g1 = pathstart g2" |
155 assumes "pathfinish g1 = pathstart g2" |
222 shows "path_image(g1 +++ g2) = (path_image g1) \<union> (path_image g2)" |
156 shows "path_image(g1 +++ g2) = (path_image g1) \<union> (path_image g2)" |
223 apply (rule, rule path_image_join_subset, rule) |
157 apply (rule, rule path_image_join_subset, rule) |
224 unfolding Un_iff |
158 unfolding Un_iff |
225 proof (erule disjE) |
159 proof (erule disjE) |
226 fix x |
160 fix x |