src/HOL/Multivariate_Analysis/Fashoda.thy
author hoelzl
Fri Feb 19 13:40:50 2016 +0100 (2016-02-19)
changeset 62378 85ed00c1fe7c
parent 61945 1135b8de26c3
child 62397 5ae24f33d343
permissions -rw-r--r--
generalize more theorems to support enat and ennreal
wenzelm@53572
     1
(*  Author:     John Harrison
wenzelm@53572
     2
    Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
wenzelm@53572
     3
*)
huffman@36432
     4
wenzelm@60420
     5
section \<open>Fashoda meet theorem\<close>
huffman@36432
     6
huffman@36432
     7
theory Fashoda
huffman@37674
     8
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
huffman@36432
     9
begin
huffman@36432
    10
hoelzl@50526
    11
(* move *)
hoelzl@50526
    12
hoelzl@50526
    13
lemma cart_eq_inner_axis: "a $ i = a \<bullet> axis i 1"
hoelzl@50526
    14
  by (simp add: inner_axis)
hoelzl@50526
    15
hoelzl@50526
    16
lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
hoelzl@50526
    17
  by (auto simp add: Basis_vec_def axis_eq_axis)
hoelzl@50526
    18
wenzelm@60420
    19
subsection \<open>Bijections between intervals.\<close>
hoelzl@56273
    20
hoelzl@56273
    21
definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
hoelzl@56273
    22
  where "interval_bij =
hoelzl@56273
    23
    (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
hoelzl@56273
    24
hoelzl@56273
    25
lemma interval_bij_affine:
hoelzl@56273
    26
  "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
hoelzl@56273
    27
    (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
haftmann@57418
    28
  by (auto simp: setsum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
haftmann@57418
    29
    field_simps inner_simps add_divide_distrib[symmetric] intro!: setsum.cong)
hoelzl@56273
    30
hoelzl@56273
    31
lemma continuous_interval_bij:
hoelzl@56273
    32
  fixes a b :: "'a::euclidean_space"
hoelzl@56273
    33
  shows "continuous (at x) (interval_bij (a, b) (u, v))"
hoelzl@56273
    34
  by (auto simp add: divide_inverse interval_bij_def intro!: continuous_setsum continuous_intros)
hoelzl@56273
    35
hoelzl@56273
    36
lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
hoelzl@56273
    37
  apply(rule continuous_at_imp_continuous_on)
hoelzl@56273
    38
  apply (rule, rule continuous_interval_bij)
hoelzl@56273
    39
  done
hoelzl@56273
    40
hoelzl@56273
    41
lemma in_interval_interval_bij:
hoelzl@56273
    42
  fixes a b u v x :: "'a::euclidean_space"
hoelzl@56273
    43
  assumes "x \<in> cbox a b"
hoelzl@56273
    44
    and "cbox u v \<noteq> {}"
hoelzl@56273
    45
  shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
hoelzl@56273
    46
  apply (simp only: interval_bij_def split_conv mem_box inner_setsum_left_Basis cong: ball_cong)
hoelzl@56273
    47
  apply safe
hoelzl@56273
    48
proof -
hoelzl@56273
    49
  fix i :: 'a
hoelzl@56273
    50
  assume i: "i \<in> Basis"
hoelzl@56273
    51
  have "cbox a b \<noteq> {}"
hoelzl@56273
    52
    using assms by auto
hoelzl@56273
    53
  with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
hoelzl@56273
    54
    using assms(2) by (auto simp add: box_eq_empty)
hoelzl@56273
    55
  have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
hoelzl@56273
    56
    using assms(1)[unfolded mem_box] using i by auto
hoelzl@56273
    57
  have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
hoelzl@56571
    58
    using * x by auto
hoelzl@56273
    59
  then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
hoelzl@56273
    60
    using * by auto
hoelzl@56273
    61
  have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
hoelzl@56273
    62
    apply (rule mult_right_mono)
hoelzl@56273
    63
    unfolding divide_le_eq_1
hoelzl@56273
    64
    using * x
hoelzl@56273
    65
    apply auto
hoelzl@56273
    66
    done
hoelzl@56273
    67
  then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
hoelzl@56273
    68
    using * by auto
hoelzl@56273
    69
qed
hoelzl@56273
    70
hoelzl@56273
    71
lemma interval_bij_bij:
hoelzl@56273
    72
  "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
hoelzl@56273
    73
    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
hoelzl@56273
    74
  by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
hoelzl@56273
    75
hoelzl@56273
    76
lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" 
hoelzl@56273
    77
  shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
hoelzl@56273
    78
  using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
hoelzl@56273
    79
wenzelm@53572
    80
wenzelm@60420
    81
subsection \<open>Fashoda meet theorem\<close>
huffman@36432
    82
wenzelm@53572
    83
lemma infnorm_2:
wenzelm@53572
    84
  fixes x :: "real^2"
wenzelm@61945
    85
  shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
wenzelm@53572
    86
  unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
huffman@36432
    87
wenzelm@53572
    88
lemma infnorm_eq_1_2:
wenzelm@53572
    89
  fixes x :: "real^2"
wenzelm@53572
    90
  shows "infnorm x = 1 \<longleftrightarrow>
wenzelm@61945
    91
    \<bar>x$1\<bar> \<le> 1 \<and> \<bar>x$2\<bar> \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
huffman@36432
    92
  unfolding infnorm_2 by auto
huffman@36432
    93
wenzelm@53572
    94
lemma infnorm_eq_1_imp:
wenzelm@53572
    95
  fixes x :: "real^2"
wenzelm@53572
    96
  assumes "infnorm x = 1"
wenzelm@61945
    97
  shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
huffman@36432
    98
  using assms unfolding infnorm_eq_1_2 by auto
huffman@36432
    99
wenzelm@53572
   100
lemma fashoda_unit:
wenzelm@53572
   101
  fixes f g :: "real \<Rightarrow> real^2"
immler@56188
   102
  assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
immler@56188
   103
    and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
immler@56188
   104
    and "continuous_on {-1 .. 1} f"
immler@56188
   105
    and "continuous_on {-1 .. 1} g"
wenzelm@53572
   106
    and "f (- 1)$1 = - 1"
wenzelm@53572
   107
    and "f 1$1 = 1" "g (- 1) $2 = -1"
wenzelm@53572
   108
    and "g 1 $2 = 1"
immler@56188
   109
  shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
wenzelm@53572
   110
proof (rule ccontr)
wenzelm@53572
   111
  assume "\<not> ?thesis"
wenzelm@53572
   112
  note as = this[unfolded bex_simps,rule_format]
huffman@36432
   113
  def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
wenzelm@53572
   114
  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2"
wenzelm@53572
   115
  have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
huffman@36432
   116
    unfolding negatex_def infnorm_2 vector_2 by auto
wenzelm@53572
   117
  have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
wenzelm@53572
   118
    unfolding sqprojection_def
wenzelm@53572
   119
    unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
wenzelm@53572
   120
    unfolding abs_inverse real_abs_infnorm
wenzelm@53628
   121
    apply (subst infnorm_eq_0[symmetric])
wenzelm@53572
   122
    apply auto
wenzelm@53572
   123
    done
wenzelm@53572
   124
  let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
immler@56188
   125
  have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}"
wenzelm@53572
   126
    apply (rule set_eqI)
immler@56188
   127
    unfolding image_iff Bex_def mem_interval_cart interval_cbox_cart
wenzelm@53572
   128
    apply rule
wenzelm@53572
   129
    defer
wenzelm@53572
   130
    apply (rule_tac x="vec x" in exI)
wenzelm@53572
   131
    apply auto
wenzelm@53572
   132
    done
wenzelm@53572
   133
  {
wenzelm@53572
   134
    fix x
immler@56188
   135
    assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` (cbox (- 1) (1::real^2))"
wenzelm@55675
   136
    then obtain w :: "real^2" where w:
immler@56188
   137
        "w \<in> cbox (- 1) 1"
wenzelm@55675
   138
        "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
wenzelm@55675
   139
      unfolding image_iff ..
wenzelm@53572
   140
    then have "x \<noteq> 0"
wenzelm@53572
   141
      using as[of "w$1" "w$2"]
immler@56188
   142
      unfolding mem_interval_cart atLeastAtMost_iff
wenzelm@53572
   143
      by auto
wenzelm@53572
   144
  } note x0 = this
wenzelm@53572
   145
  have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
wenzelm@53572
   146
    using UNIV_2 by auto
immler@54775
   147
  have 1: "box (- 1) (1::real^2) \<noteq> {}"
wenzelm@53572
   148
    unfolding interval_eq_empty_cart by auto
haftmann@58410
   149
  have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
hoelzl@56371
   150
    apply (intro continuous_intros continuous_on_component)
wenzelm@53572
   151
    unfolding *
wenzelm@53572
   152
    apply (rule assms)+
wenzelm@53572
   153
    apply (subst sqprojection_def)
hoelzl@56371
   154
    apply (intro continuous_intros)
wenzelm@53572
   155
    apply (simp add: infnorm_eq_0 x0)
wenzelm@53572
   156
    apply (rule linear_continuous_on)
wenzelm@53572
   157
  proof -
wenzelm@53572
   158
    show "bounded_linear negatex"
wenzelm@53572
   159
      apply (rule bounded_linearI')
wenzelm@53572
   160
      unfolding vec_eq_iff
wenzelm@53572
   161
    proof (rule_tac[!] allI)
wenzelm@53572
   162
      fix i :: 2
wenzelm@53572
   163
      fix x y :: "real^2"
wenzelm@53572
   164
      fix c :: real
wenzelm@53572
   165
      show "negatex (x + y) $ i =
wenzelm@53572
   166
        (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
wenzelm@53572
   167
        apply -
wenzelm@53572
   168
        apply (case_tac[!] "i\<noteq>1")
wenzelm@53572
   169
        prefer 3
wenzelm@53572
   170
        apply (drule_tac[1-2] 21) 
wenzelm@53572
   171
        unfolding negatex_def
wenzelm@53572
   172
        apply (auto simp add:vector_2)
wenzelm@53572
   173
        done
wenzelm@53572
   174
    qed
huffman@44647
   175
  qed
immler@56188
   176
  have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
wenzelm@53572
   177
    unfolding subset_eq
wenzelm@61166
   178
  proof (rule, goal_cases)
wenzelm@61165
   179
    case (1 x)
wenzelm@55675
   180
    then obtain y :: "real^2" where y:
haftmann@58410
   181
        "y \<in> cbox (- 1) 1"
wenzelm@55675
   182
        "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
wenzelm@55675
   183
      unfolding image_iff ..
wenzelm@53572
   184
    have "?F y \<noteq> 0"
wenzelm@53572
   185
      apply (rule x0)
wenzelm@53572
   186
      using y(1)
wenzelm@53572
   187
      apply auto
wenzelm@53572
   188
      done
wenzelm@53572
   189
    then have *: "infnorm (sqprojection (?F y)) = 1"
wenzelm@53628
   190
      unfolding y o_def
wenzelm@53628
   191
      by - (rule lem2[rule_format])
wenzelm@53572
   192
    have "infnorm x = 1"
wenzelm@53628
   193
      unfolding *[symmetric] y o_def
wenzelm@53628
   194
      by (rule lem1[rule_format])
immler@56188
   195
    then show "x \<in> cbox (-1) 1"
immler@56188
   196
      unfolding mem_interval_cart interval_cbox_cart infnorm_2
wenzelm@53572
   197
      apply -
wenzelm@53572
   198
      apply rule
wenzelm@53572
   199
    proof -
wenzelm@61165
   200
      fix i
wenzelm@61165
   201
      assume "max \<bar>x $ 1\<bar> \<bar>x $ 2\<bar> = 1"
wenzelm@61165
   202
      then show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
wenzelm@53572
   203
        apply (cases "i = 1")
wenzelm@53572
   204
        defer
wenzelm@53572
   205
        apply (drule 21)
wenzelm@53572
   206
        apply auto
wenzelm@53572
   207
        done
wenzelm@53572
   208
    qed
wenzelm@53572
   209
  qed
wenzelm@55675
   210
  obtain x :: "real^2" where x:
haftmann@58410
   211
      "x \<in> cbox (- 1) 1"
wenzelm@55675
   212
      "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
haftmann@58410
   213
    apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
immler@56188
   214
    apply (rule compact_cbox convex_box)+
immler@56188
   215
    unfolding interior_cbox
wenzelm@53572
   216
    apply (rule 1 2 3)+
wenzelm@55675
   217
    apply blast
wenzelm@53572
   218
    done
wenzelm@53572
   219
  have "?F x \<noteq> 0"
wenzelm@53572
   220
    apply (rule x0)
wenzelm@53572
   221
    using x(1)
wenzelm@53572
   222
    apply auto
wenzelm@53572
   223
    done
wenzelm@53572
   224
  then have *: "infnorm (sqprojection (?F x)) = 1"
wenzelm@53628
   225
    unfolding o_def
wenzelm@53628
   226
    by (rule lem2[rule_format])
wenzelm@53572
   227
  have nx: "infnorm x = 1"
wenzelm@53628
   228
    apply (subst x(2)[symmetric])
wenzelm@53628
   229
    unfolding *[symmetric] o_def
wenzelm@53572
   230
    apply (rule lem1[rule_format])
wenzelm@53572
   231
    done
wenzelm@53572
   232
  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
wenzelm@53572
   233
    and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
wenzelm@53572
   234
    apply -
wenzelm@53572
   235
    apply (rule_tac[!] allI impI)+
wenzelm@53572
   236
  proof -
wenzelm@53572
   237
    fix x :: "real^2"
wenzelm@53572
   238
    fix i :: 2
wenzelm@53572
   239
    assume x: "x \<noteq> 0"
wenzelm@53572
   240
    have "inverse (infnorm x) > 0"
wenzelm@53628
   241
      using x[unfolded infnorm_pos_lt[symmetric]] by auto
wenzelm@53572
   242
    then show "(0 < sqprojection x $ i) = (0 < x $ i)"
wenzelm@53572
   243
      and "(sqprojection x $ i < 0) = (x $ i < 0)"
huffman@44282
   244
      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
wenzelm@53572
   245
      unfolding zero_less_mult_iff mult_less_0_iff
wenzelm@53572
   246
      by (auto simp add: field_simps)
wenzelm@53572
   247
  qed
huffman@36432
   248
  note lem3 = this[rule_format]
wenzelm@53572
   249
  have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
wenzelm@53572
   250
    using x(1) unfolding mem_interval_cart by auto
wenzelm@53572
   251
  then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
wenzelm@53572
   252
    unfolding right_minus_eq
wenzelm@53572
   253
    apply -
wenzelm@53572
   254
    apply (rule as)
wenzelm@53572
   255
    apply auto
wenzelm@53572
   256
    done
wenzelm@53572
   257
  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1"
wenzelm@53572
   258
    using nx unfolding infnorm_eq_1_2 by auto 
wenzelm@53572
   259
  then show False
wenzelm@53572
   260
  proof -
wenzelm@53572
   261
    fix P Q R S 
wenzelm@53572
   262
    presume "P \<or> Q \<or> R \<or> S"
wenzelm@53572
   263
      and "P \<Longrightarrow> False"
wenzelm@53572
   264
      and "Q \<Longrightarrow> False"
wenzelm@53572
   265
      and "R \<Longrightarrow> False"
wenzelm@53572
   266
      and "S \<Longrightarrow> False"
wenzelm@53572
   267
    then show False by auto
wenzelm@53572
   268
  next
wenzelm@53572
   269
    assume as: "x$1 = 1"
wenzelm@53572
   270
    then have *: "f (x $ 1) $ 1 = 1"
wenzelm@53572
   271
      using assms(6) by auto
huffman@36432
   272
    have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
huffman@44136
   273
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
wenzelm@53572
   274
      unfolding as negatex_def vector_2
wenzelm@53572
   275
      by auto
wenzelm@53572
   276
    moreover
immler@56188
   277
    from x1 have "g (x $ 2) \<in> cbox (-1) 1"
wenzelm@53572
   278
      apply -
wenzelm@53572
   279
      apply (rule assms(2)[unfolded subset_eq,rule_format])
wenzelm@53572
   280
      apply auto
wenzelm@53572
   281
      done
wenzelm@53572
   282
    ultimately show False
wenzelm@53572
   283
      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
wenzelm@53572
   284
      apply (erule_tac x=1 in allE)
wenzelm@53572
   285
      apply auto
wenzelm@53572
   286
      done
wenzelm@53572
   287
  next
wenzelm@53572
   288
    assume as: "x$1 = -1"
wenzelm@53572
   289
    then have *: "f (x $ 1) $ 1 = - 1"
wenzelm@53572
   290
      using assms(5) by auto
huffman@36432
   291
    have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
huffman@44136
   292
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
wenzelm@53572
   293
      unfolding as negatex_def vector_2
wenzelm@53572
   294
      by auto
wenzelm@53572
   295
    moreover
immler@56188
   296
    from x1 have "g (x $ 2) \<in> cbox (-1) 1"
wenzelm@53572
   297
      apply -
wenzelm@53572
   298
      apply (rule assms(2)[unfolded subset_eq,rule_format])
wenzelm@53572
   299
      apply auto
wenzelm@53572
   300
      done
wenzelm@53572
   301
    ultimately show False
wenzelm@53572
   302
      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
wenzelm@53572
   303
      apply (erule_tac x=1 in allE)
wenzelm@53572
   304
      apply auto
wenzelm@53572
   305
      done
wenzelm@53572
   306
  next
wenzelm@53572
   307
    assume as: "x$2 = 1"
wenzelm@53572
   308
    then have *: "g (x $ 2) $ 2 = 1"
wenzelm@53572
   309
      using assms(8) by auto
huffman@36432
   310
    have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
huffman@44136
   311
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
wenzelm@53572
   312
      unfolding as negatex_def vector_2
wenzelm@53572
   313
      by auto
wenzelm@53572
   314
    moreover
immler@56188
   315
    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
wenzelm@53572
   316
      apply -
wenzelm@53572
   317
      apply (rule assms(1)[unfolded subset_eq,rule_format])
wenzelm@53572
   318
      apply auto
wenzelm@53572
   319
      done
wenzelm@53572
   320
    ultimately show False
wenzelm@53572
   321
      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
wenzelm@53572
   322
      apply (erule_tac x=2 in allE)
wenzelm@53572
   323
      apply auto
wenzelm@53572
   324
      done
wenzelm@53572
   325
  next
wenzelm@53572
   326
    assume as: "x$2 = -1"
wenzelm@53572
   327
    then have *: "g (x $ 2) $ 2 = - 1"
wenzelm@53572
   328
      using assms(7) by auto
huffman@36432
   329
    have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
huffman@44136
   330
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
wenzelm@53572
   331
      unfolding as negatex_def vector_2
wenzelm@53572
   332
      by auto
wenzelm@53572
   333
    moreover
immler@56188
   334
    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
wenzelm@53572
   335
      apply -
wenzelm@53572
   336
      apply (rule assms(1)[unfolded subset_eq,rule_format])
wenzelm@53572
   337
      apply auto
wenzelm@53572
   338
      done
wenzelm@53572
   339
    ultimately show False
wenzelm@53572
   340
      unfolding lem3[OF nz] vector_component_simps * mem_interval_cart
wenzelm@53572
   341
      apply (erule_tac x=2 in allE)
wenzelm@53572
   342
      apply auto
wenzelm@53572
   343
      done
wenzelm@53572
   344
  qed auto
wenzelm@53572
   345
qed
huffman@36432
   346
wenzelm@53572
   347
lemma fashoda_unit_path:
wenzelm@53572
   348
  fixes f g :: "real \<Rightarrow> real^2"
wenzelm@53572
   349
  assumes "path f"
wenzelm@53572
   350
    and "path g"
immler@56188
   351
    and "path_image f \<subseteq> cbox (-1) 1"
immler@56188
   352
    and "path_image g \<subseteq> cbox (-1) 1"
wenzelm@53572
   353
    and "(pathstart f)$1 = -1"
wenzelm@53572
   354
    and "(pathfinish f)$1 = 1"
wenzelm@53572
   355
    and "(pathstart g)$2 = -1"
wenzelm@53572
   356
    and "(pathfinish g)$2 = 1"
wenzelm@53572
   357
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
wenzelm@53572
   358
proof -
huffman@36432
   359
  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
huffman@36432
   360
  def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
wenzelm@53572
   361
  have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
wenzelm@53572
   362
    unfolding iscale_def by auto
wenzelm@53572
   363
  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
wenzelm@53572
   364
  proof (rule fashoda_unit)
haftmann@58410
   365
    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
haftmann@56154
   366
      using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
wenzelm@53572
   367
    have *: "continuous_on {- 1..1} iscale"
hoelzl@56371
   368
      unfolding iscale_def by (rule continuous_intros)+
huffman@36432
   369
    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
wenzelm@53572
   370
      apply -
wenzelm@53572
   371
      apply (rule_tac[!] continuous_on_compose[OF *])
wenzelm@53572
   372
      apply (rule_tac[!] continuous_on_subset[OF _ isc])
wenzelm@53572
   373
      apply (rule assms)+
wenzelm@53572
   374
      done
wenzelm@53572
   375
    have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
wenzelm@53572
   376
      unfolding vec_eq_iff by auto
wenzelm@53572
   377
    show "(f \<circ> iscale) (- 1) $ 1 = - 1"
wenzelm@53572
   378
      and "(f \<circ> iscale) 1 $ 1 = 1"
wenzelm@53572
   379
      and "(g \<circ> iscale) (- 1) $ 2 = -1"
wenzelm@53572
   380
      and "(g \<circ> iscale) 1 $ 2 = 1"
wenzelm@53572
   381
      unfolding o_def iscale_def
wenzelm@53572
   382
      using assms
wenzelm@53572
   383
      by (auto simp add: *)
wenzelm@53572
   384
  qed
wenzelm@55675
   385
  then obtain s t where st:
wenzelm@55675
   386
      "s \<in> {- 1..1}"
wenzelm@55675
   387
      "t \<in> {- 1..1}"
wenzelm@55675
   388
      "(f \<circ> iscale) s = (g \<circ> iscale) t"
immler@56188
   389
    by auto
wenzelm@53572
   390
  show thesis
wenzelm@53628
   391
    apply (rule_tac z = "f (iscale s)" in that)
wenzelm@55675
   392
    using st
wenzelm@53572
   393
    unfolding o_def path_image_def image_iff
wenzelm@53572
   394
    apply -
wenzelm@53572
   395
    apply (rule_tac x="iscale s" in bexI)
wenzelm@53572
   396
    prefer 3
wenzelm@53572
   397
    apply (rule_tac x="iscale t" in bexI)
wenzelm@53572
   398
    using isc[unfolded subset_eq, rule_format]
wenzelm@53572
   399
    apply auto
wenzelm@53572
   400
    done
wenzelm@53572
   401
qed
huffman@36432
   402
wenzelm@53627
   403
lemma fashoda:
wenzelm@53627
   404
  fixes b :: "real^2"
wenzelm@53627
   405
  assumes "path f"
wenzelm@53627
   406
    and "path g"
immler@56188
   407
    and "path_image f \<subseteq> cbox a b"
immler@56188
   408
    and "path_image g \<subseteq> cbox a b"
wenzelm@53627
   409
    and "(pathstart f)$1 = a$1"
wenzelm@53627
   410
    and "(pathfinish f)$1 = b$1"
wenzelm@53627
   411
    and "(pathstart g)$2 = a$2"
wenzelm@53627
   412
    and "(pathfinish g)$2 = b$2"
wenzelm@53627
   413
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
wenzelm@53627
   414
proof -
wenzelm@53627
   415
  fix P Q S
wenzelm@53627
   416
  presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
wenzelm@53627
   417
  then show thesis
wenzelm@53627
   418
    by auto
wenzelm@53627
   419
next
immler@56188
   420
  have "cbox a b \<noteq> {}"
immler@54775
   421
    using assms(3) using path_image_nonempty[of f] by auto
wenzelm@53627
   422
  then have "a \<le> b"
wenzelm@53627
   423
    unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
wenzelm@53627
   424
  then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
wenzelm@53627
   425
    unfolding less_eq_vec_def forall_2 by auto
wenzelm@53627
   426
next
wenzelm@53627
   427
  assume as: "a$1 = b$1"
wenzelm@53627
   428
  have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
wenzelm@53627
   429
    apply (rule connected_ivt_component_cart)
wenzelm@53627
   430
    apply (rule connected_path_image assms)+
wenzelm@53627
   431
    apply (rule pathstart_in_path_image)
wenzelm@53627
   432
    apply (rule pathfinish_in_path_image)
huffman@36432
   433
    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
wenzelm@53627
   434
    unfolding pathstart_def
immler@56188
   435
    apply (auto simp add: less_eq_vec_def mem_interval_cart)
wenzelm@53627
   436
    done
wenzelm@55675
   437
  then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
immler@56188
   438
  have "z \<in> cbox a b"
wenzelm@53627
   439
    using z(1) assms(4)
wenzelm@53627
   440
    unfolding path_image_def
immler@56188
   441
    by blast
wenzelm@53627
   442
  then have "z = f 0"
wenzelm@53627
   443
    unfolding vec_eq_iff forall_2
wenzelm@53627
   444
    unfolding z(2) pathstart_def
hoelzl@37489
   445
    using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
wenzelm@53627
   446
    unfolding mem_interval_cart
wenzelm@53627
   447
    apply (erule_tac x=1 in allE)
wenzelm@53627
   448
    using as
wenzelm@53627
   449
    apply auto
wenzelm@53627
   450
    done
wenzelm@53627
   451
  then show thesis
wenzelm@53627
   452
    apply -
wenzelm@53627
   453
    apply (rule that[OF _ z(1)])
wenzelm@53627
   454
    unfolding path_image_def
wenzelm@53627
   455
    apply auto
wenzelm@53627
   456
    done
wenzelm@53627
   457
next
wenzelm@53627
   458
  assume as: "a$2 = b$2"
wenzelm@53627
   459
  have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
wenzelm@53627
   460
    apply (rule connected_ivt_component_cart)
wenzelm@53627
   461
    apply (rule connected_path_image assms)+
wenzelm@53627
   462
    apply (rule pathstart_in_path_image)
wenzelm@53627
   463
    apply (rule pathfinish_in_path_image)
wenzelm@53627
   464
    unfolding assms
wenzelm@53627
   465
    using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
wenzelm@53627
   466
    unfolding pathstart_def
immler@56188
   467
    apply (auto simp add: less_eq_vec_def mem_interval_cart)
wenzelm@53627
   468
    done
wenzelm@55675
   469
  then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
immler@56188
   470
  have "z \<in> cbox a b"
wenzelm@53627
   471
    using z(1) assms(3)
wenzelm@53627
   472
    unfolding path_image_def
immler@56188
   473
    by blast
wenzelm@53627
   474
  then have "z = g 0"
wenzelm@53627
   475
    unfolding vec_eq_iff forall_2
wenzelm@53627
   476
    unfolding z(2) pathstart_def
hoelzl@37489
   477
    using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
wenzelm@53627
   478
    unfolding mem_interval_cart
wenzelm@53627
   479
    apply (erule_tac x=2 in allE)
wenzelm@53627
   480
    using as
wenzelm@53627
   481
    apply auto
wenzelm@53627
   482
    done
wenzelm@53627
   483
  then show thesis
wenzelm@53627
   484
    apply -
wenzelm@53627
   485
    apply (rule that[OF z(1)])
wenzelm@53627
   486
    unfolding path_image_def
wenzelm@53627
   487
    apply auto
wenzelm@53627
   488
    done
wenzelm@53627
   489
next
wenzelm@53627
   490
  assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
immler@56188
   491
  have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
wenzelm@53627
   492
    unfolding interval_eq_empty_cart by auto
wenzelm@55675
   493
  obtain z :: "real^2" where z:
wenzelm@55675
   494
      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
wenzelm@55675
   495
      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
wenzelm@53627
   496
    apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
huffman@36432
   497
    unfolding path_def path_image_def pathstart_def pathfinish_def
wenzelm@53627
   498
    apply (rule_tac[1-2] continuous_on_compose)
wenzelm@53627
   499
    apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
wenzelm@53627
   500
    unfolding subset_eq
wenzelm@53627
   501
    apply(rule_tac[1-2] ballI)
wenzelm@53627
   502
  proof -
wenzelm@53627
   503
    fix x
wenzelm@53627
   504
    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
wenzelm@55675
   505
    then obtain y where y:
wenzelm@55675
   506
        "y \<in> {0..1}"
wenzelm@55675
   507
        "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
wenzelm@55675
   508
      unfolding image_iff ..
haftmann@58410
   509
    show "x \<in> cbox (- 1) 1"
wenzelm@53627
   510
      unfolding y o_def
wenzelm@53627
   511
      apply (rule in_interval_interval_bij)
wenzelm@53627
   512
      using y(1)
wenzelm@53627
   513
      using assms(3)[unfolded path_image_def subset_eq] int_nem
wenzelm@53627
   514
      apply auto
wenzelm@53627
   515
      done
wenzelm@53627
   516
  next
wenzelm@53627
   517
    fix x
wenzelm@53627
   518
    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
wenzelm@55675
   519
    then obtain y where y:
wenzelm@55675
   520
        "y \<in> {0..1}"
wenzelm@55675
   521
        "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
wenzelm@55675
   522
      unfolding image_iff ..
haftmann@58410
   523
    show "x \<in> cbox (- 1) 1"
wenzelm@53627
   524
      unfolding y o_def
wenzelm@53627
   525
      apply (rule in_interval_interval_bij)
wenzelm@53627
   526
      using y(1)
wenzelm@53627
   527
      using assms(4)[unfolded path_image_def subset_eq] int_nem
wenzelm@53627
   528
      apply auto
wenzelm@53627
   529
      done
wenzelm@53627
   530
  next
wenzelm@53627
   531
    show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
wenzelm@53627
   532
      and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
wenzelm@53627
   533
      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
wenzelm@53627
   534
      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
immler@56188
   535
      using assms as
hoelzl@50526
   536
      by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
hoelzl@50526
   537
         (simp_all add: inner_axis)
wenzelm@53627
   538
  qed
wenzelm@55675
   539
  from z(1) obtain zf where zf:
wenzelm@55675
   540
      "zf \<in> {0..1}"
wenzelm@55675
   541
      "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
wenzelm@55675
   542
    unfolding image_iff ..
wenzelm@55675
   543
  from z(2) obtain zg where zg:
wenzelm@55675
   544
      "zg \<in> {0..1}"
wenzelm@55675
   545
      "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
wenzelm@55675
   546
    unfolding image_iff ..
wenzelm@53627
   547
  have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
wenzelm@53627
   548
    unfolding forall_2
wenzelm@53627
   549
    using as
wenzelm@53627
   550
    by auto
wenzelm@53627
   551
  show thesis
wenzelm@53627
   552
    apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
wenzelm@53627
   553
    apply (subst zf)
wenzelm@53627
   554
    defer
wenzelm@53627
   555
    apply (subst zg)
wenzelm@53627
   556
    unfolding o_def interval_bij_bij_cart[OF *] path_image_def
wenzelm@53627
   557
    using zf(1) zg(1)
wenzelm@53627
   558
    apply auto
wenzelm@53627
   559
    done
wenzelm@53627
   560
qed
huffman@36432
   561
wenzelm@53627
   562
wenzelm@60420
   563
subsection \<open>Some slightly ad hoc lemmas I use below\<close>
huffman@36432
   564
wenzelm@53627
   565
lemma segment_vertical:
wenzelm@53627
   566
  fixes a :: "real^2"
wenzelm@53627
   567
  assumes "a$1 = b$1"
wenzelm@53627
   568
  shows "x \<in> closed_segment a b \<longleftrightarrow>
wenzelm@53627
   569
    x$1 = a$1 \<and> x$1 = b$1 \<and> (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2)"
wenzelm@53627
   570
  (is "_ = ?R")
wenzelm@53627
   571
proof -
huffman@36432
   572
  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"
wenzelm@53627
   573
  {
wenzelm@53627
   574
    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
wenzelm@53627
   575
    then show ?thesis
wenzelm@53627
   576
      unfolding closed_segment_def mem_Collect_eq
wenzelm@53628
   577
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
wenzelm@53627
   578
      by blast
wenzelm@53627
   579
  }
wenzelm@53627
   580
  {
wenzelm@53627
   581
    assume ?L
wenzelm@55675
   582
    then obtain u where u:
wenzelm@55675
   583
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
wenzelm@55675
   584
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
wenzelm@55675
   585
        "0 \<le> u"
wenzelm@55675
   586
        "u \<le> 1"
wenzelm@55675
   587
      by blast
wenzelm@53627
   588
    { fix b a
wenzelm@53627
   589
      assume "b + u * a > a + u * b"
wenzelm@53627
   590
      then have "(1 - u) * b > (1 - u) * a"
wenzelm@53627
   591
        by (auto simp add:field_simps)
wenzelm@53627
   592
      then have "b \<ge> a"
haftmann@59555
   593
        apply (drule_tac mult_left_less_imp_less)
wenzelm@53627
   594
        using u
wenzelm@53627
   595
        apply auto
wenzelm@53627
   596
        done
wenzelm@53627
   597
      then have "u * a \<le> u * b"
wenzelm@53627
   598
        apply -
wenzelm@53627
   599
        apply (rule mult_left_mono[OF _ u(3)]) 
wenzelm@53627
   600
        using u(3-4)
wenzelm@53627
   601
        apply (auto simp add: field_simps)
wenzelm@53627
   602
        done
wenzelm@53627
   603
    } note * = this
wenzelm@53627
   604
    {
wenzelm@53627
   605
      fix a b
wenzelm@53627
   606
      assume "u * b > u * a"
wenzelm@53627
   607
      then have "(1 - u) * a \<le> (1 - u) * b"
wenzelm@53627
   608
        apply -
wenzelm@53627
   609
        apply (rule mult_left_mono)
haftmann@59555
   610
        apply (drule mult_left_less_imp_less)
wenzelm@53627
   611
        using u
wenzelm@53627
   612
        apply auto
wenzelm@53627
   613
        done
wenzelm@53627
   614
      then have "a + u * b \<le> b + u * a"
wenzelm@53627
   615
        by (auto simp add: field_simps)
wenzelm@53627
   616
    } note ** = this
wenzelm@53627
   617
    then show ?R
wenzelm@53627
   618
      unfolding u assms
wenzelm@53627
   619
      using u
wenzelm@53627
   620
      by (auto simp add:field_simps not_le intro: * **)
wenzelm@53627
   621
  }
wenzelm@53627
   622
  {
wenzelm@53627
   623
    assume ?R
wenzelm@53627
   624
    then show ?L
wenzelm@53627
   625
    proof (cases "x$2 = b$2")
wenzelm@53627
   626
      case True
wenzelm@53627
   627
      then show ?L
wenzelm@53627
   628
        apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
wenzelm@53627
   629
        unfolding assms True
wenzelm@60420
   630
        using \<open>?R\<close>
wenzelm@53627
   631
        apply (auto simp add: field_simps)
wenzelm@53627
   632
        done
wenzelm@53627
   633
    next
wenzelm@53627
   634
      case False
wenzelm@53627
   635
      then show ?L
wenzelm@53627
   636
        apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
wenzelm@53627
   637
        unfolding assms
wenzelm@60420
   638
        using \<open>?R\<close>
wenzelm@53627
   639
        apply (auto simp add: field_simps)
wenzelm@53627
   640
        done
wenzelm@53627
   641
    qed
wenzelm@53627
   642
  }
wenzelm@53627
   643
qed
huffman@36432
   644
wenzelm@53627
   645
lemma segment_horizontal:
wenzelm@53627
   646
  fixes a :: "real^2"
wenzelm@53627
   647
  assumes "a$2 = b$2"
wenzelm@53627
   648
  shows "x \<in> closed_segment a b \<longleftrightarrow>
wenzelm@53627
   649
    x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)"
wenzelm@53627
   650
  (is "_ = ?R")
wenzelm@53627
   651
proof -
huffman@36432
   652
  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"
wenzelm@53627
   653
  {
wenzelm@53627
   654
    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
wenzelm@53627
   655
    then show ?thesis
wenzelm@53627
   656
      unfolding closed_segment_def mem_Collect_eq
wenzelm@53628
   657
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
wenzelm@53627
   658
      by blast
wenzelm@53627
   659
  }
wenzelm@53627
   660
  {
wenzelm@53627
   661
    assume ?L
wenzelm@55675
   662
    then obtain u where u:
wenzelm@55675
   663
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
wenzelm@55675
   664
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
wenzelm@55675
   665
        "0 \<le> u"
wenzelm@55675
   666
        "u \<le> 1"
wenzelm@55675
   667
      by blast
wenzelm@53627
   668
    {
wenzelm@53627
   669
      fix b a
wenzelm@53627
   670
      assume "b + u * a > a + u * b"
wenzelm@53627
   671
      then have "(1 - u) * b > (1 - u) * a"
wenzelm@53628
   672
        by (auto simp add: field_simps)
wenzelm@53627
   673
      then have "b \<ge> a"
haftmann@59555
   674
        apply (drule_tac mult_left_less_imp_less)
wenzelm@53627
   675
        using u
wenzelm@53627
   676
        apply auto
wenzelm@53627
   677
        done
wenzelm@53627
   678
      then have "u * a \<le> u * b"
wenzelm@53627
   679
        apply -
wenzelm@53627
   680
        apply (rule mult_left_mono[OF _ u(3)])
wenzelm@53627
   681
        using u(3-4)
wenzelm@53627
   682
        apply (auto simp add: field_simps)
wenzelm@53627
   683
        done
wenzelm@53627
   684
    } note * = this
wenzelm@53627
   685
    {
wenzelm@53627
   686
      fix a b
wenzelm@53627
   687
      assume "u * b > u * a"
wenzelm@53627
   688
      then have "(1 - u) * a \<le> (1 - u) * b"
wenzelm@53627
   689
        apply -
wenzelm@53627
   690
        apply (rule mult_left_mono)
haftmann@59555
   691
        apply (drule mult_left_less_imp_less)
wenzelm@53627
   692
        using u
wenzelm@53627
   693
        apply auto
wenzelm@53627
   694
        done
wenzelm@53627
   695
      then have "a + u * b \<le> b + u * a"
wenzelm@53627
   696
        by (auto simp add: field_simps)
wenzelm@53627
   697
    } note ** = this
wenzelm@53627
   698
    then show ?R
wenzelm@53627
   699
      unfolding u assms
wenzelm@53627
   700
      using u
wenzelm@53627
   701
      by (auto simp add: field_simps not_le intro: * **)
wenzelm@53627
   702
  }
wenzelm@53627
   703
  {
wenzelm@53627
   704
    assume ?R
wenzelm@53627
   705
    then show ?L
wenzelm@53627
   706
    proof (cases "x$1 = b$1")
wenzelm@53627
   707
      case True
wenzelm@53627
   708
      then show ?L
wenzelm@53627
   709
        apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
wenzelm@53627
   710
        unfolding assms True
wenzelm@60420
   711
        using \<open>?R\<close>
wenzelm@53627
   712
        apply (auto simp add: field_simps)
wenzelm@53627
   713
        done
wenzelm@53627
   714
    next
wenzelm@53627
   715
      case False
wenzelm@53627
   716
      then show ?L
wenzelm@53627
   717
        apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
wenzelm@53627
   718
        unfolding assms
wenzelm@60420
   719
        using \<open>?R\<close>
wenzelm@53627
   720
        apply (auto simp add: field_simps)
wenzelm@53627
   721
        done
wenzelm@53627
   722
    qed
wenzelm@53627
   723
  }
wenzelm@53627
   724
qed
huffman@36432
   725
wenzelm@53627
   726
wenzelm@60420
   727
subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>
huffman@36432
   728
wenzelm@53627
   729
lemma fashoda_interlace:
wenzelm@53627
   730
  fixes a :: "real^2"
wenzelm@53627
   731
  assumes "path f"
wenzelm@53627
   732
    and "path g"
immler@56188
   733
    and "path_image f \<subseteq> cbox a b"
immler@56188
   734
    and "path_image g \<subseteq> cbox a b"
wenzelm@53627
   735
    and "(pathstart f)$2 = a$2"
wenzelm@53627
   736
    and "(pathfinish f)$2 = a$2"
wenzelm@53627
   737
    and "(pathstart g)$2 = a$2"
wenzelm@53627
   738
    and "(pathfinish g)$2 = a$2"
wenzelm@53627
   739
    and "(pathstart f)$1 < (pathstart g)$1"
wenzelm@53627
   740
    and "(pathstart g)$1 < (pathfinish f)$1"
wenzelm@53627
   741
    and "(pathfinish f)$1 < (pathfinish g)$1"
wenzelm@53627
   742
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
wenzelm@53627
   743
proof -
immler@56188
   744
  have "cbox a b \<noteq> {}"
immler@54775
   745
    using path_image_nonempty[of f] using assms(3) by auto
hoelzl@37489
   746
  note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
immler@56188
   747
  have "pathstart f \<in> cbox a b"
immler@56188
   748
    and "pathfinish f \<in> cbox a b"
immler@56188
   749
    and "pathstart g \<in> cbox a b"
immler@56188
   750
    and "pathfinish g \<in> cbox a b"
wenzelm@53628
   751
    using pathstart_in_path_image pathfinish_in_path_image
wenzelm@53628
   752
    using assms(3-4)
wenzelm@53628
   753
    by auto
hoelzl@37489
   754
  note startfin = this[unfolded mem_interval_cart forall_2]
huffman@36432
   755
  let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
huffman@36432
   756
     linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
huffman@36432
   757
     linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
huffman@36432
   758
     linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" 
huffman@36432
   759
  let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
huffman@36432
   760
     linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
huffman@36432
   761
     linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
huffman@36432
   762
     linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
huffman@36432
   763
  let ?a = "vector[a$1 - 2, a$2 - 3]"
huffman@36432
   764
  let ?b = "vector[b$1 + 2, b$2 + 3]"
wenzelm@53627
   765
  have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
huffman@36432
   766
      path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
huffman@36432
   767
      path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
huffman@36432
   768
      path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
huffman@36432
   769
    "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
huffman@36432
   770
      path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
huffman@36432
   771
      path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
huffman@36432
   772
      path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
huffman@36432
   773
      by(auto simp add: path_image_join path_linepath)
immler@56188
   774
  have abab: "cbox a b \<subseteq> cbox ?a ?b"
immler@56188
   775
    unfolding interval_cbox_cart[symmetric]
wenzelm@53627
   776
    by (auto simp add:less_eq_vec_def forall_2 vector_2)
wenzelm@55675
   777
  obtain z where
wenzelm@55675
   778
    "z \<in> path_image
wenzelm@55675
   779
          (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
wenzelm@55675
   780
           linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++
wenzelm@55675
   781
           f +++
wenzelm@55675
   782
           linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++
wenzelm@55675
   783
           linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))"
wenzelm@55675
   784
    "z \<in> path_image
wenzelm@55675
   785
          (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++
wenzelm@55675
   786
           g +++
wenzelm@55675
   787
           linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++
wenzelm@55675
   788
           linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++
wenzelm@55675
   789
           linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))"
wenzelm@53627
   790
    apply (rule fashoda[of ?P1 ?P2 ?a ?b])
wenzelm@53627
   791
    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
wenzelm@53627
   792
  proof -
wenzelm@53628
   793
    show "path ?P1" and "path ?P2"
wenzelm@53627
   794
      using assms by auto
immler@56188
   795
    have "path_image ?P1 \<subseteq> cbox ?a ?b"
wenzelm@53627
   796
      unfolding P1P2 path_image_linepath
wenzelm@53627
   797
      apply (rule Un_least)+
wenzelm@53627
   798
      defer 3
immler@56188
   799
      apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
wenzelm@53627
   800
      unfolding mem_interval_cart forall_2 vector_2
wenzelm@53627
   801
      using ab startfin abab assms(3)
wenzelm@53627
   802
      using assms(9-)
wenzelm@53627
   803
      unfolding assms
immler@56189
   804
      apply (auto simp add: field_simps box_def)
wenzelm@53627
   805
      done
immler@56188
   806
    then show "path_image ?P1 \<subseteq> cbox ?a ?b" .
immler@56188
   807
    have "path_image ?P2 \<subseteq> cbox ?a ?b"
wenzelm@53627
   808
      unfolding P1P2 path_image_linepath
wenzelm@53627
   809
      apply (rule Un_least)+
wenzelm@53627
   810
      defer 2
immler@56188
   811
      apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
wenzelm@53627
   812
      unfolding mem_interval_cart forall_2 vector_2
wenzelm@53627
   813
      using ab startfin abab assms(4)
wenzelm@53627
   814
      using assms(9-)
wenzelm@53627
   815
      unfolding assms
immler@56189
   816
      apply (auto simp add: field_simps box_def)
wenzelm@53627
   817
      done
immler@56188
   818
    then show "path_image ?P2 \<subseteq> cbox ?a ?b" .
wenzelm@53627
   819
    show "a $ 1 - 2 = a $ 1 - 2"
wenzelm@53627
   820
      and "b $ 1 + 2 = b $ 1 + 2"
wenzelm@53627
   821
      and "pathstart g $ 2 - 3 = a $ 2 - 3"
wenzelm@53627
   822
      and "b $ 2 + 3 = b $ 2 + 3"
wenzelm@53627
   823
      by (auto simp add: assms)
wenzelm@53628
   824
  qed
wenzelm@53628
   825
  note z=this[unfolded P1P2 path_image_linepath]
wenzelm@53627
   826
  show thesis
wenzelm@53627
   827
    apply (rule that[of z])
wenzelm@53627
   828
  proof -
huffman@36432
   829
    have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
wenzelm@53627
   830
      z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
wenzelm@53627
   831
      z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
wenzelm@53627
   832
      z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
wenzelm@53627
   833
    (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
wenzelm@53627
   834
      z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
wenzelm@53627
   835
      z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
wenzelm@53627
   836
      z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
wenzelm@61166
   837
    proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
wenzelm@61167
   838
      case prems: 1
immler@56188
   839
      have "pathfinish f \<in> cbox a b"
wenzelm@53627
   840
        using assms(3) pathfinish_in_path_image[of f] by auto 
wenzelm@53628
   841
      then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
wenzelm@53627
   842
        unfolding mem_interval_cart forall_2 by auto
wenzelm@53627
   843
      then have "z$1 \<noteq> pathfinish f$1"
wenzelm@61167
   844
        using prems(2)
wenzelm@53628
   845
        using assms ab
wenzelm@53628
   846
        by (auto simp add: field_simps)
immler@56188
   847
      moreover have "pathstart f \<in> cbox a b"
wenzelm@53628
   848
        using assms(3) pathstart_in_path_image[of f]
wenzelm@53628
   849
        by auto
wenzelm@53627
   850
      then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
wenzelm@53628
   851
        unfolding mem_interval_cart forall_2
wenzelm@53628
   852
        by auto
wenzelm@53627
   853
      then have "z$1 \<noteq> pathstart f$1"
wenzelm@61167
   854
        using prems(2) using assms ab
wenzelm@53628
   855
        by (auto simp add: field_simps)
wenzelm@53627
   856
      ultimately have *: "z$2 = a$2 - 2"
wenzelm@61167
   857
        using prems(1)
wenzelm@53628
   858
        by auto
wenzelm@53627
   859
      have "z$1 \<noteq> pathfinish g$1"
wenzelm@61167
   860
        using prems(2)
wenzelm@53628
   861
        using assms ab
wenzelm@53628
   862
        by (auto simp add: field_simps *)
immler@56188
   863
      moreover have "pathstart g \<in> cbox a b"
wenzelm@53628
   864
        using assms(4) pathstart_in_path_image[of g]
wenzelm@53628
   865
        by auto 
hoelzl@37489
   866
      note this[unfolded mem_interval_cart forall_2]
wenzelm@53627
   867
      then have "z$1 \<noteq> pathstart g$1"
wenzelm@61167
   868
        using prems(1)
wenzelm@53628
   869
        using assms ab
wenzelm@53628
   870
        by (auto simp add: field_simps *)
huffman@36432
   871
      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"
wenzelm@61167
   872
        using prems(2)
wenzelm@53628
   873
        unfolding * assms
wenzelm@53628
   874
        by (auto simp add: field_simps)
wenzelm@53627
   875
      then show False
wenzelm@53627
   876
        unfolding * using ab by auto
wenzelm@53627
   877
    qed
wenzelm@53627
   878
    then have "z \<in> path_image f \<or> z \<in> path_image g"
wenzelm@53627
   879
      using z unfolding Un_iff by blast
immler@56188
   880
    then have z': "z \<in> cbox a b"
wenzelm@53628
   881
      using assms(3-4)
wenzelm@53628
   882
      by auto
wenzelm@53627
   883
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
wenzelm@53627
   884
      z = pathstart f \<or> z = pathfinish f"
wenzelm@53628
   885
      unfolding vec_eq_iff forall_2 assms
wenzelm@53628
   886
      by auto
wenzelm@53627
   887
    with z' show "z \<in> path_image f"
wenzelm@53627
   888
      using z(1)
wenzelm@53627
   889
      unfolding Un_iff mem_interval_cart forall_2
wenzelm@53627
   890
      apply -
wenzelm@53627
   891
      apply (simp only: segment_vertical segment_horizontal vector_2)
wenzelm@53627
   892
      unfolding assms
wenzelm@53627
   893
      apply auto
wenzelm@53627
   894
      done
wenzelm@53627
   895
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
wenzelm@53627
   896
      z = pathstart g \<or> z = pathfinish g"
wenzelm@53628
   897
      unfolding vec_eq_iff forall_2 assms
wenzelm@53628
   898
      by auto
wenzelm@53627
   899
    with z' show "z \<in> path_image g"
wenzelm@53627
   900
      using z(2)
wenzelm@53627
   901
      unfolding Un_iff mem_interval_cart forall_2
wenzelm@53627
   902
      apply (simp only: segment_vertical segment_horizontal vector_2)
wenzelm@53627
   903
      unfolding assms
wenzelm@53627
   904
      apply auto
wenzelm@53627
   905
      done
wenzelm@53627
   906
  qed
wenzelm@53627
   907
qed
huffman@36432
   908
huffman@36432
   909
(** The Following still needs to be translated. Maybe I will do that later.
huffman@36432
   910
huffman@36432
   911
(* ------------------------------------------------------------------------- *)
huffman@36432
   912
(* Complement in dimension N >= 2 of set homeomorphic to any interval in     *)
huffman@36432
   913
(* any dimension is (path-)connected. This naively generalizes the argument  *)
huffman@36432
   914
(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer        *)
huffman@36432
   915
(* fixed point theorem", American Mathematical Monthly 1984.                 *)
huffman@36432
   916
(* ------------------------------------------------------------------------- *)
huffman@36432
   917
huffman@36432
   918
let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
huffman@36432
   919
 (`!p:real^M->real^N a b.
huffman@36432
   920
        ~(interval[a,b] = {}) /\
huffman@36432
   921
        p continuous_on interval[a,b] /\
huffman@36432
   922
        (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
huffman@36432
   923
        ==> ?f. f continuous_on (:real^N) /\
huffman@36432
   924
                IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
huffman@36432
   925
                (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
huffman@36432
   926
  REPEAT STRIP_TAC THEN
huffman@36432
   927
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
huffman@36432
   928
  DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
huffman@36432
   929
  SUBGOAL_THEN `(q:real^N->real^M) continuous_on
huffman@36432
   930
                (IMAGE p (interval[a:real^M,b]))`
huffman@36432
   931
  ASSUME_TAC THENL
huffman@36432
   932
   [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
huffman@36432
   933
    ALL_TAC] THEN
huffman@36432
   934
  MP_TAC(ISPECL [`q:real^N->real^M`;
huffman@36432
   935
                 `IMAGE (p:real^M->real^N)
huffman@36432
   936
                 (interval[a,b])`;
huffman@36432
   937
                 `a:real^M`; `b:real^M`]
huffman@36432
   938
        TIETZE_CLOSED_INTERVAL) THEN
huffman@36432
   939
  ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
huffman@36432
   940
               COMPACT_IMP_CLOSED] THEN
huffman@36432
   941
  ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
huffman@36432
   942
  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
huffman@36432
   943
  EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
huffman@36432
   944
  REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
huffman@36432
   945
  CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
huffman@36432
   946
  MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
huffman@36432
   947
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
huffman@36432
   948
        CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
huffman@36432
   949
huffman@36432
   950
let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
huffman@36432
   951
 (`!s:real^N->bool a b:real^M.
huffman@36432
   952
        s homeomorphic (interval[a,b])
huffman@36432
   953
        ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
huffman@36432
   954
  REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
huffman@36432
   955
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
huffman@36432
   956
  MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
huffman@36432
   957
  DISCH_TAC THEN
huffman@36432
   958
  SUBGOAL_THEN
huffman@36432
   959
   `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
huffman@36432
   960
          (p:real^M->real^N) x = p y ==> x = y`
huffman@36432
   961
  ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
huffman@36432
   962
  FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
huffman@36432
   963
  DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
huffman@36432
   964
  ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
huffman@36432
   965
  ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
huffman@36432
   966
                  NOT_BOUNDED_UNIV] THEN
huffman@36432
   967
  ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
huffman@36432
   968
  X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
huffman@36432
   969
  SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
huffman@36432
   970
  SUBGOAL_THEN `bounded((path_component s c) UNION
huffman@36432
   971
                        (IMAGE (p:real^M->real^N) (interval[a,b])))`
huffman@36432
   972
  MP_TAC THENL
huffman@36432
   973
   [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
huffman@36432
   974
                 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
huffman@36432
   975
    ALL_TAC] THEN
huffman@36432
   976
  DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
huffman@36432
   977
  REWRITE_TAC[UNION_SUBSET] THEN
huffman@36432
   978
  DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
huffman@36432
   979
  MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
huffman@36432
   980
    RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
huffman@36432
   981
  ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
huffman@36432
   982
  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
huffman@36432
   983
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
huffman@36432
   984
   (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
huffman@36432
   985
  REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
huffman@36432
   986
  ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
huffman@36432
   987
  SUBGOAL_THEN
huffman@36432
   988
    `(q:real^N->real^N) continuous_on
huffman@36432
   989
     (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
huffman@36432
   990
  MP_TAC THENL
huffman@36432
   991
   [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
huffman@36432
   992
    REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
huffman@36432
   993
    REPEAT CONJ_TAC THENL
huffman@36432
   994
     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
huffman@36432
   995
      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
huffman@36432
   996
                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
huffman@36432
   997
      ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
huffman@36432
   998
      ALL_TAC] THEN
huffman@36432
   999
    X_GEN_TAC `z:real^N` THEN
huffman@36432
  1000
    REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
huffman@36432
  1001
    STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
huffman@36432
  1002
    MP_TAC(ISPECL
huffman@36432
  1003
     [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
huffman@36432
  1004
     OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
huffman@36432
  1005
    ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
huffman@36432
  1006
     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
huffman@36432
  1007
      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
huffman@36432
  1008
                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
huffman@36432
  1009
      REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
huffman@36432
  1010
      DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
huffman@36432
  1011
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
huffman@36432
  1012
      REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
huffman@36432
  1013
    ALL_TAC] THEN
huffman@36432
  1014
  SUBGOAL_THEN
huffman@36432
  1015
   `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
huffman@36432
  1016
    (:real^N)`
huffman@36432
  1017
  SUBST1_TAC THENL
huffman@36432
  1018
   [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
huffman@36432
  1019
    REWRITE_TAC[CLOSURE_SUBSET];
huffman@36432
  1020
    DISCH_TAC] THEN
huffman@36432
  1021
  MP_TAC(ISPECL
huffman@36432
  1022
   [`(\x. &2 % c - x) o
huffman@36432
  1023
     (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
huffman@36432
  1024
    `cball(c:real^N,B)`]
huffman@36432
  1025
    BROUWER) THEN
huffman@36432
  1026
  REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
huffman@36432
  1027
  ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
huffman@36432
  1028
  SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
huffman@36432
  1029
   [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
huffman@36432
  1030
    REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
huffman@36432
  1031
    ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
huffman@36432
  1032
    ALL_TAC] THEN
huffman@36432
  1033
  REPEAT CONJ_TAC THENL
huffman@36432
  1034
   [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
huffman@36432
  1035
    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
huffman@36432
  1036
    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
huffman@36432
  1037
     [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
huffman@36432
  1038
    MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
huffman@36432
  1039
    MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
huffman@36432
  1040
    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
huffman@36432
  1041
    REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
huffman@36432
  1042
    MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
huffman@36432
  1043
    MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
huffman@36432
  1044
    ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
huffman@36432
  1045
    SUBGOAL_THEN
huffman@36432
  1046
     `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
huffman@36432
  1047
    SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
huffman@36432
  1048
    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
huffman@36432
  1049
    ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
huffman@36432
  1050
                 CONTINUOUS_ON_LIFT_NORM];
huffman@36432
  1051
    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
huffman@36432
  1052
    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
huffman@36432
  1053
    REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
huffman@36432
  1054
    REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
huffman@36432
  1055
    ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
huffman@36432
  1056
    ASM_REAL_ARITH_TAC;
huffman@36432
  1057
    REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
huffman@36432
  1058
    REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
huffman@36432
  1059
    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
huffman@36432
  1060
    REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
huffman@36432
  1061
    ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
huffman@36432
  1062
     [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
huffman@36432
  1063
      REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
huffman@36432
  1064
      ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
huffman@36432
  1065
      ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
huffman@36432
  1066
      UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
huffman@36432
  1067
      REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
huffman@36432
  1068
      EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
huffman@36432
  1069
      REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
huffman@36432
  1070
      ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
huffman@36432
  1071
      SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
huffman@36432
  1072
       [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
huffman@36432
  1073
      ASM_REWRITE_TAC[] THEN
huffman@36432
  1074
      MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
huffman@36432
  1075
      ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
huffman@36432
  1076
huffman@36432
  1077
let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
huffman@36432
  1078
 (`!s:real^N->bool a b:real^M.
huffman@36432
  1079
        2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
huffman@36432
  1080
        ==> path_connected((:real^N) DIFF s)`,
huffman@36432
  1081
  REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
huffman@36432
  1082
  FIRST_ASSUM(MP_TAC o MATCH_MP
huffman@36432
  1083
    UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
huffman@36432
  1084
  ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
huffman@36432
  1085
  ABBREV_TAC `t = (:real^N) DIFF s` THEN
huffman@36432
  1086
  DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
huffman@36432
  1087
  STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
huffman@36432
  1088
  REWRITE_TAC[COMPACT_INTERVAL] THEN
huffman@36432
  1089
  DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
huffman@36432
  1090
  REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
huffman@36432
  1091
  X_GEN_TAC `B:real` THEN STRIP_TAC THEN
huffman@36432
  1092
  SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
huffman@36432
  1093
                (?v:real^N. v IN path_component t y /\ B < norm(v))`
huffman@36432
  1094
  STRIP_ASSUME_TAC THENL
huffman@36432
  1095
   [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
huffman@36432
  1096
  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
huffman@36432
  1097
  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
huffman@36432
  1098
  MATCH_MP_TAC PATH_COMPONENT_SYM THEN
huffman@36432
  1099
  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
huffman@36432
  1100
  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
huffman@36432
  1101
  MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
huffman@36432
  1102
  EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
huffman@36432
  1103
   [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
huffman@36432
  1104
     `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
huffman@36432
  1105
    ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
huffman@36432
  1106
    MP_TAC(ISPEC `cball(vec 0:real^N,B)`
huffman@36432
  1107
       PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
huffman@36432
  1108
    ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
huffman@36432
  1109
    REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
huffman@36432
  1110
    DISCH_THEN MATCH_MP_TAC THEN
huffman@36432
  1111
    ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
huffman@36432
  1112
huffman@36432
  1113
(* ------------------------------------------------------------------------- *)
huffman@36432
  1114
(* In particular, apply all these to the special case of an arc.             *)
huffman@36432
  1115
(* ------------------------------------------------------------------------- *)
huffman@36432
  1116
huffman@36432
  1117
let RETRACTION_ARC = prove
huffman@36432
  1118
 (`!p. arc p
huffman@36432
  1119
       ==> ?f. f continuous_on (:real^N) /\
huffman@36432
  1120
               IMAGE f (:real^N) SUBSET path_image p /\
huffman@36432
  1121
               (!x. x IN path_image p ==> f x = x)`,
huffman@36432
  1122
  REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
huffman@36432
  1123
  MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
hoelzl@37489
  1124
  ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
huffman@36432
  1125
huffman@36432
  1126
let PATH_CONNECTED_ARC_COMPLEMENT = prove
huffman@36432
  1127
 (`!p. 2 <= dimindex(:N) /\ arc p
huffman@36432
  1128
       ==> path_connected((:real^N) DIFF path_image p)`,
huffman@36432
  1129
  REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
huffman@36432
  1130
  MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
huffman@36432
  1131
    PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
huffman@36432
  1132
  ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
huffman@36432
  1133
  ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
huffman@36432
  1134
  MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
huffman@36432
  1135
  EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
huffman@36432
  1136
huffman@36432
  1137
let CONNECTED_ARC_COMPLEMENT = prove
huffman@36432
  1138
 (`!p. 2 <= dimindex(:N) /\ arc p
huffman@36432
  1139
       ==> connected((:real^N) DIFF path_image p)`,
huffman@36432
  1140
  SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
huffman@36432
  1141
huffman@36432
  1142
end