author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44647  e4de7750cdeb 
child 50526  899c9c4e4a4c 
permissions  rwrr 
36432  1 
(* Author: John Harrison 
2 
Translation from HOL light: Robert Himmelmann, TU Muenchen *) 

3 

4 
header {* Fashoda meet theorem. *} 

5 

6 
theory Fashoda 

37674
f86de9c00c47
convert theorem path_connected_sphere to euclidean_space class
huffman
parents:
37489
diff
changeset

7 
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space 
36432  8 
begin 
9 

10 
subsection {*Fashoda meet theorem. *} 

11 

12 
lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

13 
unfolding infnorm_cart UNIV_2 apply(rule Sup_eq) by auto 
36432  14 

15 
lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow> 

16 
(abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = 1 \<or> x$1 = 1 \<or> x$2 = 1 \<or> x$2 = 1))" 

17 
unfolding infnorm_2 by auto 

18 

19 
lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1" 

20 
using assms unfolding infnorm_eq_1_2 by auto 

21 

22 
lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2" 

23 
assumes "f ` { 1..1} \<subseteq> { 1..1}" "g ` { 1..1} \<subseteq> { 1..1}" 

24 
"continuous_on { 1..1} f" "continuous_on { 1..1} g" 

25 
"f ( 1)$1 =  1" "f 1$1 = 1" "g ( 1) $2 = 1" "g 1 $2 = 1" 

26 
shows "\<exists>s\<in>{ 1..1}. \<exists>t\<in>{ 1..1}. f s = g t" proof(rule ccontr) 

27 
case goal1 note as = this[unfolded bex_simps,rule_format] 

28 
def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 

29 
def negatex \<equiv> "\<lambda>x::real^2. (vector [(x$1), x$2])::real^2" 

30 
have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z" 

31 
unfolding negatex_def infnorm_2 vector_2 by auto 

32 
have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def 

33 
unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

34 
apply(subst infnorm_eq_0[THEN sym]) by auto 
36432  35 
let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w  (g \<circ> (\<lambda>x. x$2)) w)" 
36 
have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` { 1..1} = { 1..1::real}" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
37674
diff
changeset

37 
apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer 
36432  38 
apply(rule_tac x="vec x" in exI) by auto 
39 
{ fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w  (g \<circ> (\<lambda>x. x $ 2)) w) ` { 1..1::real^2}" 

40 
then guess w unfolding image_iff .. note w = this 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

41 
hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this 
36432  42 
have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

43 
have 1:"{ 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto 
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

44 
have 2:"continuous_on { 1..1} (negatex \<circ> sqprojection \<circ> ?F)" 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

45 
apply(intro continuous_on_intros continuous_on_component) 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

46 
unfolding * apply(rule assms)+ 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

47 
apply(subst sqprojection_def) 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

48 
apply(intro continuous_on_intros) 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

49 
apply(simp add: infnorm_eq_0 x0) 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

50 
apply(rule linear_continuous_on) 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

51 
proof 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

52 
show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real 
36593
fb69c8cd27bd
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents:
36583
diff
changeset

53 
show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" 
41958  54 
applyapply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[12] 21) 
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

55 
unfolding negatex_def by(auto simp add:vector_2 ) qed 
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44531
diff
changeset

56 
qed 
36432  57 
have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` { 1..1} \<subseteq> { 1..1}" unfolding subset_eq apply rule proof 
58 
case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto 

59 
hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply by(rule lem2[rule_format]) 

60 
have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format]) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

61 
thus "x\<in>{ 1..1}" unfolding mem_interval_cart infnorm_2 apply apply rule 
36432  62 
proofcase goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed 
63 
guess x apply(rule brouwer_weak[of "{ 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"]) 

64 
apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval 

65 
apply(rule 1 2 3)+ . note x=this 

66 
have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto 

67 
hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format]) 

68 
have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format]) 

69 
have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)" 

70 
apply apply(rule_tac[!] allI impI)+ proof fix x::"real^2" and i::2 assume x:"x\<noteq>0" 

71 
have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto 

72 
thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)" 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44136
diff
changeset

73 
unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def 
36432  74 
unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed 
75 
note lem3 = this[rule_format] 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

76 
have x1:"x $ 1 \<in> { 1..1::real}" "x $ 2 \<in> { 1..1::real}" using x(1) unfolding mem_interval_cart by auto 
36432  77 
hence nz:"f (x $ 1)  g (x $ 2) \<noteq> 0" unfolding right_minus_eq applyapply(rule as) by auto 
78 
have "x $ 1 = 1 \<or> x $ 1 = 1 \<or> x $ 2 = 1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto 

79 
thus False proof fix P Q R S 

80 
presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto 

81 
next assume as:"x$1 = 1" 

82 
hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto 

83 
have "sqprojection (f (x$1)  g (x$2)) $ 1 < 0" 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

84 
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 
36432  85 
unfolding as negatex_def vector_2 by auto moreover 
86 
from x1 have "g (x $ 2) \<in> { 1..1}" applyapply(rule assms(2)[unfolded subset_eq,rule_format]) by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

87 
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432  88 
apply(erule_tac x=1 in allE) by auto 
89 
next assume as:"x$1 = 1" 

90 
hence *:"f (x $ 1) $ 1 =  1" using assms(5) by auto 

91 
have "sqprojection (f (x$1)  g (x$2)) $ 1 > 0" 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

92 
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 
36432  93 
unfolding as negatex_def vector_2 by auto moreover 
94 
from x1 have "g (x $ 2) \<in> { 1..1}" applyapply(rule assms(2)[unfolded subset_eq,rule_format]) by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

95 
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432  96 
apply(erule_tac x=1 in allE) by auto 
97 
next assume as:"x$2 = 1" 

98 
hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto 

99 
have "sqprojection (f (x$1)  g (x$2)) $ 2 > 0" 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

100 
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 
36432  101 
unfolding as negatex_def vector_2 by auto moreover 
102 
from x1 have "f (x $ 1) \<in> { 1..1}" applyapply(rule assms(1)[unfolded subset_eq,rule_format]) by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

103 
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432  104 
apply(erule_tac x=2 in allE) by auto 
105 
next assume as:"x$2 = 1" 

106 
hence *:"g (x $ 2) $ 2 =  1" using assms(7) by auto 

107 
have "sqprojection (f (x$1)  g (x$2)) $ 2 < 0" 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

108 
using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 
36432  109 
unfolding as negatex_def vector_2 by auto moreover 
110 
from x1 have "f (x $ 1) \<in> { 1..1}" applyapply(rule assms(1)[unfolded subset_eq,rule_format]) by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

111 
ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432  112 
apply(erule_tac x=2 in allE) by auto qed(auto) qed 
113 

114 
lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2" 

115 
assumes "path f" "path g" "path_image f \<subseteq> { 1..1}" "path_image g \<subseteq> { 1..1}" 

116 
"(pathstart f)$1 = 1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = 1" "(pathfinish g)$2 = 1" 

117 
obtains z where "z \<in> path_image f" "z \<in> path_image g" proof 

118 
note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] 

119 
def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)" 

120 
have isc:"iscale ` { 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto) 

121 
have "\<exists>s\<in>{ 1..1}. \<exists>t\<in>{ 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) 

122 
show "(f \<circ> iscale) ` { 1..1} \<subseteq> { 1..1}" "(g \<circ> iscale) ` { 1..1} \<subseteq> { 1..1}" 

123 
using isc and assms(34) unfolding image_compose by auto 

124 
have *:"continuous_on { 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+ 

125 
show "continuous_on { 1..1} (f \<circ> iscale)" "continuous_on { 1..1} (g \<circ> iscale)" 

126 
applyapply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc]) 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

127 
by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto 
36432  128 
show "(f \<circ> iscale) ( 1) $ 1 =  1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) ( 1) $ 2 = 1" "(g \<circ> iscale) 1 $ 2 = 1" 
129 
unfolding o_def iscale_def using assms by(auto simp add:*) qed 

130 
then guess s .. from this(2) guess t .. note st=this 

131 
show thesis apply(rule_tac z="f (iscale s)" in that) 

132 
using st `s\<in>{ 1..1}` unfolding o_def path_image_def image_iff apply 

133 
apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI) 

134 
using isc[unfolded subset_eq, rule_format] by auto qed 

135 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

136 
(* move *) 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

137 
lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

138 
shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

139 
unfolding interval_bij_cart split_conv vec_eq_iff vec_lambda_beta 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

140 
apply(rule,insert assms,erule_tac x=i in allE) by auto 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

141 

36432  142 
lemma fashoda: fixes b::"real^2" 
143 
assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}" 

144 
"(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1" 

145 
"(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2" 

146 
obtains z where "z \<in> path_image f" "z \<in> path_image g" proof 

147 
fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto 

148 
next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

149 
hence "a \<le> b" unfolding interval_eq_empty_cart less_eq_vec_def by(auto simp add: not_less) 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

150 
thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding less_eq_vec_def forall_2 by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

151 
next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component_cart) 
36432  152 
apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image) 
153 
unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"] 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

154 
unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this 
36432  155 
have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

156 
hence "z = f 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

157 
using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

158 
unfolding mem_interval_cart apply(erule_tac x=1 in allE) using as by auto 
36432  159 
thus thesis applyapply(rule that[OF _ z(1)]) unfolding path_image_def by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

160 
next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component_cart) 
36432  161 
apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image) 
162 
unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"] 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

163 
unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this 
36432  164 
have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

165 
hence "z = g 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

166 
using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2] 
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

167 
unfolding mem_interval_cart apply(erule_tac x=2 in allE) using as by auto 
36432  168 
thus thesis applyapply(rule that[OF z(1)]) unfolding path_image_def by auto 
169 
next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

170 
have int_nem:"{ 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto 
36432  171 
guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) ( 1,1) \<circ> f" "interval_bij (a,b) ( 1,1) \<circ> g"]) 
172 
unfolding path_def path_image_def pathstart_def pathfinish_def 

173 
apply(rule_tac[12] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+ 

174 
unfolding subset_eq apply(rule_tac[12] ballI) 

175 
proof fix x assume "x \<in> (interval_bij (a, b) ( 1, 1) \<circ> f) ` {0..1}" 

176 
then guess y unfolding image_iff .. note y=this 

177 
show "x \<in> { 1..1}" unfolding y o_def apply(rule in_interval_interval_bij) 

178 
using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto 

179 
next fix x assume "x \<in> (interval_bij (a, b) ( 1, 1) \<circ> g) ` {0..1}" 

180 
then guess y unfolding image_iff .. note y=this 

181 
show "x \<in> { 1..1}" unfolding y o_def apply(rule in_interval_interval_bij) 

182 
using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto 

183 
next show "(interval_bij (a, b) ( 1, 1) \<circ> f) 0 $ 1 = 1" 

184 
"(interval_bij (a, b) ( 1, 1) \<circ> f) 1 $ 1 = 1" 

185 
"(interval_bij (a, b) ( 1, 1) \<circ> g) 0 $ 2 = 1" 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

186 
"(interval_bij (a, b) ( 1, 1) \<circ> g) 1 $ 2 = 1" 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44282
diff
changeset

187 
unfolding interval_bij_cart vector_component_simps o_def split_conv 
36432  188 
unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this 
189 
from z(1) guess zf unfolding image_iff .. note zf=this 

190 
from z(2) guess zg unfolding image_iff .. note zg=this 

191 
have *:"\<forall>i. ( 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto 

192 
show thesis apply(rule_tac z="interval_bij ( 1,1) (a,b) z" in that) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

193 
apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij_cart[OF *] path_image_def 
36432  194 
using zf(1) zg(1) by auto qed 
195 

196 
subsection {*Some slightly ad hoc lemmas I use below*} 

197 

198 
lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1" 

199 
shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and> 

200 
(a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R") 

201 
proof 

202 
let ?L = "\<exists>u. (x $ 1 = (1  u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1  u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1" 

203 
{ presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

204 
unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } 
36432  205 
{ assume ?L then guess u applyapply(erule exE)apply(erule conjE)+ . note u=this 
206 
{ fix b a assume "b + u * a > a + u * b" 

207 
hence "(1  u) * b > (1  u) * a" by(auto simp add:field_simps) 

208 
hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto 

209 
hence "u * a \<le> u * b" applyapply(rule mult_left_mono[OF _ u(3)]) 

210 
using u(34) by(auto simp add:field_simps) } note * = this 

211 
{ fix a b assume "u * b > u * a" hence "(1  u) * a \<le> (1  u) * b" applyapply(rule mult_left_mono) 

212 
apply(drule mult_less_imp_less_left) using u by auto 

213 
hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this 

214 
thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) } 

215 
{ assume ?R thus ?L proof(cases "x$2 = b$2") 

216 
case True thus ?L apply(rule_tac x="(x$2  a$2) / (b$2  a$2)" in exI) unfolding assms True 

217 
using `?R` by(auto simp add:field_simps) 

218 
next case False thus ?L apply(rule_tac x="1  (x$2  b$2) / (a$2  b$2)" in exI) unfolding assms using `?R` 

219 
by(auto simp add:field_simps) 

220 
qed } qed 

221 

222 
lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2" 

223 
shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and> 

224 
(a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R") 

225 
proof 

226 
let ?L = "\<exists>u. (x $ 1 = (1  u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1  u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1" 

227 
{ presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

228 
unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } 
36432  229 
{ assume ?L then guess u applyapply(erule exE)apply(erule conjE)+ . note u=this 
230 
{ fix b a assume "b + u * a > a + u * b" 

231 
hence "(1  u) * b > (1  u) * a" by(auto simp add:field_simps) 

232 
hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto 

233 
hence "u * a \<le> u * b" applyapply(rule mult_left_mono[OF _ u(3)]) 

234 
using u(34) by(auto simp add:field_simps) } note * = this 

235 
{ fix a b assume "u * b > u * a" hence "(1  u) * a \<le> (1  u) * b" applyapply(rule mult_left_mono) 

236 
apply(drule mult_less_imp_less_left) using u by auto 

237 
hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this 

238 
thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) } 

239 
{ assume ?R thus ?L proof(cases "x$1 = b$1") 

240 
case True thus ?L apply(rule_tac x="(x$1  a$1) / (b$1  a$1)" in exI) unfolding assms True 

241 
using `?R` by(auto simp add:field_simps) 

242 
next case False thus ?L apply(rule_tac x="1  (x$1  b$1) / (a$1  b$1)" in exI) unfolding assms using `?R` 

243 
by(auto simp add:field_simps) 

244 
qed } qed 

245 

246 
subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *} 

247 

248 
lemma fashoda_interlace: fixes a::"real^2" 

249 
assumes "path f" "path g" 

250 
"path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}" 

251 
"(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2" 

252 
"(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2" 

253 
"(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1" 

254 
"(pathfinish f)$1 < (pathfinish g)$1" 

255 
obtains z where "z \<in> path_image f" "z \<in> path_image g" 

256 
proof 

257 
have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

258 
note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less] 
36432  259 
have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}" 
260 
using pathstart_in_path_image pathfinish_in_path_image using assms(34) by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

261 
note startfin = this[unfolded mem_interval_cart forall_2] 
36432  262 
let ?P1 = "linepath (vector[a$1  2, a$2  2]) (vector[(pathstart f)$1,a$2  2]) +++ 
263 
linepath(vector[(pathstart f)$1,a$2  2])(pathstart f) +++ f +++ 

264 
linepath(pathfinish f)(vector[(pathfinish f)$1,a$2  2]) +++ 

265 
linepath(vector[(pathfinish f)$1,a$2  2])(vector[b$1 + 2,a$2  2])" 

266 
let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2  3])(pathstart g) +++ g +++ 

267 
linepath(pathfinish g)(vector[(pathfinish g)$1,a$2  1]) +++ 

268 
linepath(vector[(pathfinish g)$1,a$2  1])(vector[b$1 + 1,a$2  1]) +++ 

269 
linepath(vector[b$1 + 1,a$2  1])(vector[b$1 + 1,b$2 + 3])" 

270 
let ?a = "vector[a$1  2, a$2  3]" 

271 
let ?b = "vector[b$1 + 2, b$2 + 3]" 

272 
have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1  2, a$2  2]) (vector[(pathstart f)$1,a$2  2])) \<union> 

273 
path_image (linepath(vector[(pathstart f)$1,a$2  2])(pathstart f)) \<union> path_image f \<union> 

274 
path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2  2])) \<union> 

275 
path_image (linepath(vector[(pathfinish f)$1,a$2  2])(vector[b$1 + 2,a$2  2]))" 

276 
"path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2  3])(pathstart g)) \<union> path_image g \<union> 

277 
path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2  1])) \<union> 

278 
path_image(linepath(vector[(pathfinish g)$1,a$2  1])(vector[b$1 + 1,a$2  1])) \<union> 

279 
path_image(linepath(vector[b$1 + 1,a$2  1])(vector[b$1 + 1,b$2 + 3]))" using assms(12) 

280 
by(auto simp add: path_image_join path_linepath) 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

281 
have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:less_eq_vec_def forall_2 vector_2) 
36432  282 
guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b]) 
283 
unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof 

284 
show "path ?P1" "path ?P2" using assms by auto 

285 
have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3 

286 
apply(rule_tac[14] convex_interval(1)[unfolded convex_contains_segment,rule_format]) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

287 
unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(3) 
36432  288 
using assms(9) unfolding assms by(auto simp add:field_simps) 
289 
thus "path_image ?P1 \<subseteq> {?a .. ?b}" . 

290 
have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2 

291 
apply(rule_tac[14] convex_interval(1)[unfolded convex_contains_segment,rule_format]) 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

292 
unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(4) 
36432  293 
using assms(9) unfolding assms by(auto simp add:field_simps) 
294 
thus "path_image ?P2 \<subseteq> {?a .. ?b}" . 

295 
show "a $ 1  2 = a $ 1  2" "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2  3 = a $ 2  3" "b $ 2 + 3 = b $ 2 + 3" 

296 
by(auto simp add: assms) 

297 
qed note z=this[unfolded P1P2 path_image_linepath] 

298 
show thesis apply(rule that[of z]) proof 

299 
have "(z \<in> closed_segment (vector [a $ 1  2, a $ 2  2]) (vector [pathstart f $ 1, a $ 2  2]) \<or> 

300 
z \<in> closed_segment (vector [pathstart f $ 1, a $ 2  2]) (pathstart f)) \<or> 

301 
z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2  2]) \<or> 

302 
z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2  2]) (vector [b $ 1 + 2, a $ 2  2]) \<Longrightarrow> 

303 
(((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2  3]) (pathstart g)) \<or> 

304 
z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2  1])) \<or> 

305 
z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2  1]) (vector [b $ 1 + 1, a $ 2  1])) \<or> 

306 
z \<in> closed_segment (vector [b $ 1 + 1, a $ 2  1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False" 

307 
apply(simp only: segment_vertical segment_horizontal vector_2) proof case goal1 note as=this 

308 
have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

309 
hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto 
36432  310 
hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps) 
311 
moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

312 
hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto 
36432  313 
hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps) 
314 
ultimately have *:"z$2 = a$2  2" using goal1(1) by auto 

315 
have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *) 

316 
moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

317 
note this[unfolded mem_interval_cart forall_2] 
36432  318 
hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *) 
319 
ultimately have "a $ 2  1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2  1" 

320 
using as(2) unfolding * assms by(auto simp add:field_simps) 

321 
thus False unfolding * using ab by auto 

322 
qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast 

323 
hence z':"z\<in>{a..b}" using assms(34) by auto 

324 
have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)" 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

325 
unfolding vec_eq_iff forall_2 assms by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

326 
with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval_cart forall_2 apply 
36432  327 
apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto 
328 
have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)" 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
41958
diff
changeset

329 
unfolding vec_eq_iff forall_2 assms by auto 
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

330 
with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval_cart forall_2 apply 
36432  331 
apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto 
332 
qed qed 

333 

334 
(** The Following still needs to be translated. Maybe I will do that later. 

335 

336 
(*  *) 

337 
(* Complement in dimension N >= 2 of set homeomorphic to any interval in *) 

338 
(* any dimension is (path)connected. This naively generalizes the argument *) 

339 
(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer *) 

340 
(* fixed point theorem", American Mathematical Monthly 1984. *) 

341 
(*  *) 

342 

343 
let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove 

344 
(`!p:real^M>real^N a b. 

345 
~(interval[a,b] = {}) /\ 

346 
p continuous_on interval[a,b] /\ 

347 
(!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y) 

348 
==> ?f. f continuous_on (:real^N) /\ 

349 
IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\ 

350 
(!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`, 

351 
REPEAT STRIP_TAC THEN 

352 
FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN 

353 
DISCH_THEN(X_CHOOSE_TAC `q:real^N>real^M`) THEN 

354 
SUBGOAL_THEN `(q:real^N>real^M) continuous_on 

355 
(IMAGE p (interval[a:real^M,b]))` 

356 
ASSUME_TAC THENL 

357 
[MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]; 

358 
ALL_TAC] THEN 

359 
MP_TAC(ISPECL [`q:real^N>real^M`; 

360 
`IMAGE (p:real^M>real^N) 

361 
(interval[a,b])`; 

362 
`a:real^M`; `b:real^M`] 

363 
TIETZE_CLOSED_INTERVAL) THEN 

364 
ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE; 

365 
COMPACT_IMP_CLOSED] THEN 

366 
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN 

367 
DISCH_THEN(X_CHOOSE_THEN `r:real^N>real^M` STRIP_ASSUME_TAC) THEN 

368 
EXISTS_TAC `(p:real^M>real^N) o (r:real^N>real^M)` THEN 

369 
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN 

370 
CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN 

371 
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN 

372 
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ] 

373 
CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);; 

374 

375 
let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove 

376 
(`!s:real^N>bool a b:real^M. 

377 
s homeomorphic (interval[a,b]) 

378 
==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`, 

379 
REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN 

380 
REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN 

381 
MAP_EVERY X_GEN_TAC [`p':real^N>real^M`; `p:real^M>real^N`] THEN 

382 
DISCH_TAC THEN 

383 
SUBGOAL_THEN 

384 
`!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ 

385 
(p:real^M>real^N) x = p y ==> x = y` 

386 
ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN 

387 
FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN 

388 
DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN 

389 
ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN 

390 
ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV; 

391 
NOT_BOUNDED_UNIV] THEN 

392 
ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN 

393 
X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN 

394 
SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN 

395 
SUBGOAL_THEN `bounded((path_component s c) UNION 

396 
(IMAGE (p:real^M>real^N) (interval[a,b])))` 

397 
MP_TAC THENL 

398 
[ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED; 

399 
COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; 

400 
ALL_TAC] THEN 

401 
DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN 

402 
REWRITE_TAC[UNION_SUBSET] THEN 

403 
DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN 

404 
MP_TAC(ISPECL [`p:real^M>real^N`; `a:real^M`; `b:real^M`] 

405 
RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN 

406 
ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN 

407 
DISCH_THEN(X_CHOOSE_THEN `r:real^N>real^N` MP_TAC) THEN 

408 
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC 

409 
(CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN 

410 
REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN 

411 
ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN 

412 
SUBGOAL_THEN 

413 
`(q:real^N>real^N) continuous_on 

414 
(closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))` 

415 
MP_TAC THENL 

416 
[EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN 

417 
REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN 

418 
REPEAT CONJ_TAC THENL 

419 
[MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN 

420 
ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED; 

421 
COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; 

422 
ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; 

423 
ALL_TAC] THEN 

424 
X_GEN_TAC `z:real^N` THEN 

425 
REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN 

426 
STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 

427 
MP_TAC(ISPECL 

428 
[`path_component s (z:real^N)`; `path_component s (c:real^N)`] 

429 
OPEN_INTER_CLOSURE_EQ_EMPTY) THEN 

430 
ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL 

431 
[MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN 

432 
ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED; 

433 
COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL]; 

434 
REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN 

435 
DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN 

436 
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN 

437 
REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]]; 

438 
ALL_TAC] THEN 

439 
SUBGOAL_THEN 

440 
`closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) = 

441 
(:real^N)` 

442 
SUBST1_TAC THENL 

443 
[MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN 

444 
REWRITE_TAC[CLOSURE_SUBSET]; 

445 
DISCH_TAC] THEN 

446 
MP_TAC(ISPECL 

447 
[`(\x. &2 % c  x) o 

448 
(\x. c + B / norm(x  c) % (x  c)) o (q:real^N>real^N)`; 

449 
`cball(c:real^N,B)`] 

450 
BROUWER) THEN 

451 
REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN 

452 
ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN 

453 
SUBGOAL_THEN `!x. ~((q:real^N>real^N) x = c)` ASSUME_TAC THENL 

454 
[X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN 

455 
REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN 

456 
ASM SET_TAC[PATH_COMPONENT_REFL_EQ]; 

457 
ALL_TAC] THEN 

458 
REPEAT CONJ_TAC THENL 

459 
[MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN 

460 
SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN 

461 
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL 

462 
[ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN 

463 
MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN 

464 
MATCH_MP_TAC CONTINUOUS_ON_MUL THEN 

465 
SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN 

466 
REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN 

467 
MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN 

468 
MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN 

469 
ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN 

470 
SUBGOAL_THEN 

471 
`(\x:real^N. lift(norm(x  c))) = (lift o norm) o (\x. x  c)` 

472 
SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN 

473 
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN 

474 
ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST; 

475 
CONTINUOUS_ON_LIFT_NORM]; 

476 
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN 

477 
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN 

478 
REWRITE_TAC[VECTOR_ARITH `c  (&2 % c  (c + x)) = x`] THEN 

479 
REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN 

480 
ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN 

481 
ASM_REAL_ARITH_TAC; 

482 
REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN 

483 
REWRITE_TAC[IN_CBALL; o_THM; dist] THEN 

484 
X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN 

485 
REWRITE_TAC[VECTOR_ARITH `&2 % c  (c + x') = x <=> x' = x  c`] THEN 

486 
ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL 

487 
[MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(x = y)`) THEN 

488 
REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN 

489 
ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN 

490 
ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN 

491 
UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN 

492 
REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB]; 

493 
EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN 

494 
REWRITE_TAC[VECTOR_ARITH `(c % x) = x <=> (&1 + c) % x = vec 0`] THEN 

495 
ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN 

496 
SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL 

497 
[ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN 

498 
ASM_REWRITE_TAC[] THEN 

499 
MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN 

500 
ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);; 

501 

502 
let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove 

503 
(`!s:real^N>bool a b:real^M. 

504 
2 <= dimindex(:N) /\ s homeomorphic interval[a,b] 

505 
==> path_connected((:real^N) DIFF s)`, 

506 
REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN 

507 
FIRST_ASSUM(MP_TAC o MATCH_MP 

508 
UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN 

509 
ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN 

510 
ABBREV_TAC `t = (:real^N) DIFF s` THEN 

511 
DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN 

512 
STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN 

513 
REWRITE_TAC[COMPACT_INTERVAL] THEN 

514 
DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN 

515 
REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN 

516 
X_GEN_TAC `B:real` THEN STRIP_TAC THEN 

517 
SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\ 

518 
(?v:real^N. v IN path_component t y /\ B < norm(v))` 

519 
STRIP_ASSUME_TAC THENL 

520 
[ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN 

521 
MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN 

522 
CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN 

523 
MATCH_MP_TAC PATH_COMPONENT_SYM THEN 

524 
MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN 

525 
CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN 

526 
MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN 

527 
EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL 

528 
[EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE 

529 
`s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN 

530 
ASM_REWRITE_TAC[SUBSET; IN_CBALL_0]; 

531 
MP_TAC(ISPEC `cball(vec 0:real^N,B)` 

532 
PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN 

533 
ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN 

534 
REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN 

535 
DISCH_THEN MATCH_MP_TAC THEN 

536 
ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);; 

537 

538 
(*  *) 

539 
(* In particular, apply all these to the special case of an arc. *) 

540 
(*  *) 

541 

542 
let RETRACTION_ARC = prove 

543 
(`!p. arc p 

544 
==> ?f. f continuous_on (:real^N) /\ 

545 
IMAGE f (:real^N) SUBSET path_image p /\ 

546 
(!x. x IN path_image p ==> f x = x)`, 

547 
REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN 

548 
MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN 

37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36593
diff
changeset

549 
ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);; 
36432  550 

551 
let PATH_CONNECTED_ARC_COMPLEMENT = prove 

552 
(`!p. 2 <= dimindex(:N) /\ arc p 

553 
==> path_connected((:real^N) DIFF path_image p)`, 

554 
REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN 

555 
MP_TAC(ISPECL [`path_image p:real^N>bool`; `vec 0:real^1`; `vec 1:real^1`] 

556 
PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN 

557 
ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN 

558 
ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN 

559 
MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN 

560 
EXISTS_TAC `p:real^1>real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);; 

561 

562 
let CONNECTED_ARC_COMPLEMENT = prove 

563 
(`!p. 2 <= dimindex(:N) /\ arc p 

564 
==> connected((:real^N) DIFF path_image p)`, 

565 
SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *) 

566 

567 
end 