src/HOL/Analysis/Fashoda_Theorem.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69722 b5163b2132c5
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
wenzelm@53572
     1
(*  Author:     John Harrison
wenzelm@53572
     2
    Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
wenzelm@53572
     3
*)
huffman@36432
     4
ak2110@69722
     5
section \<open>Fashoda Meet Theorem\<close>
huffman@36432
     6
hoelzl@63594
     7
theory Fashoda_Theorem
huffman@37674
     8
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
huffman@36432
     9
begin
huffman@36432
    10
immler@69683
    11
subsection \<open>Bijections between intervals\<close>
hoelzl@56273
    12
ak2110@69173
    13
definition%important interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
hoelzl@56273
    14
  where "interval_bij =
hoelzl@56273
    15
    (\<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
    16
hoelzl@56273
    17
lemma interval_bij_affine:
hoelzl@56273
    18
  "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
    19
    (\<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))"
nipkow@64267
    20
  by (auto simp: sum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
nipkow@64267
    21
    field_simps inner_simps add_divide_distrib[symmetric] intro!: sum.cong)
hoelzl@56273
    22
hoelzl@56273
    23
lemma continuous_interval_bij:
hoelzl@56273
    24
  fixes a b :: "'a::euclidean_space"
hoelzl@56273
    25
  shows "continuous (at x) (interval_bij (a, b) (u, v))"
nipkow@64267
    26
  by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)
hoelzl@56273
    27
hoelzl@56273
    28
lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
hoelzl@56273
    29
  apply(rule continuous_at_imp_continuous_on)
hoelzl@56273
    30
  apply (rule, rule continuous_interval_bij)
hoelzl@56273
    31
  done
hoelzl@56273
    32
immler@69681
    33
lemma in_interval_interval_bij:
hoelzl@56273
    34
  fixes a b u v x :: "'a::euclidean_space"
hoelzl@56273
    35
  assumes "x \<in> cbox a b"
hoelzl@56273
    36
    and "cbox u v \<noteq> {}"
hoelzl@56273
    37
  shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
nipkow@64267
    38
  apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
hoelzl@56273
    39
  apply safe
immler@69681
    40
proof -
hoelzl@56273
    41
  fix i :: 'a
hoelzl@56273
    42
  assume i: "i \<in> Basis"
hoelzl@56273
    43
  have "cbox a b \<noteq> {}"
hoelzl@56273
    44
    using assms by auto
hoelzl@56273
    45
  with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
hoelzl@56273
    46
    using assms(2) by (auto simp add: box_eq_empty)
hoelzl@56273
    47
  have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
hoelzl@56273
    48
    using assms(1)[unfolded mem_box] using i by auto
hoelzl@56273
    49
  have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
hoelzl@56571
    50
    using * x by auto
hoelzl@56273
    51
  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
    52
    using * by auto
hoelzl@56273
    53
  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
    54
    apply (rule mult_right_mono)
hoelzl@56273
    55
    unfolding divide_le_eq_1
hoelzl@56273
    56
    using * x
hoelzl@56273
    57
    apply auto
hoelzl@56273
    58
    done
hoelzl@56273
    59
  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
    60
    using * by auto
hoelzl@56273
    61
qed
hoelzl@56273
    62
hoelzl@56273
    63
lemma interval_bij_bij:
hoelzl@56273
    64
  "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
hoelzl@56273
    65
    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
hoelzl@56273
    66
  by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
hoelzl@56273
    67
hoelzl@63594
    68
lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i"
hoelzl@56273
    69
  shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
hoelzl@56273
    70
  using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
hoelzl@56273
    71
wenzelm@53572
    72
immler@69683
    73
subsection \<open>Fashoda meet theorem\<close>
huffman@36432
    74
wenzelm@53572
    75
lemma infnorm_2:
wenzelm@53572
    76
  fixes x :: "real^2"
wenzelm@61945
    77
  shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
wenzelm@53572
    78
  unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
huffman@36432
    79
wenzelm@53572
    80
lemma infnorm_eq_1_2:
wenzelm@53572
    81
  fixes x :: "real^2"
wenzelm@53572
    82
  shows "infnorm x = 1 \<longleftrightarrow>
wenzelm@61945
    83
    \<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
    84
  unfolding infnorm_2 by auto
huffman@36432
    85
wenzelm@53572
    86
lemma infnorm_eq_1_imp:
wenzelm@53572
    87
  fixes x :: "real^2"
wenzelm@53572
    88
  assumes "infnorm x = 1"
wenzelm@61945
    89
  shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
huffman@36432
    90
  using assms unfolding infnorm_eq_1_2 by auto
huffman@36432
    91
immler@69681
    92
proposition fashoda_unit:
wenzelm@53572
    93
  fixes f g :: "real \<Rightarrow> real^2"
immler@56188
    94
  assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
immler@56188
    95
    and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
immler@56188
    96
    and "continuous_on {-1 .. 1} f"
immler@56188
    97
    and "continuous_on {-1 .. 1} g"
wenzelm@53572
    98
    and "f (- 1)$1 = - 1"
wenzelm@53572
    99
    and "f 1$1 = 1" "g (- 1) $2 = -1"
wenzelm@53572
   100
    and "g 1 $2 = 1"
immler@56188
   101
  shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
immler@69681
   102
proof (rule ccontr)
wenzelm@53572
   103
  assume "\<not> ?thesis"
wenzelm@53572
   104
  note as = this[unfolded bex_simps,rule_format]
wenzelm@63040
   105
  define sqprojection
wenzelm@63040
   106
    where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
wenzelm@63040
   107
  define negatex :: "real^2 \<Rightarrow> real^2"
wenzelm@63040
   108
    where "negatex x = (vector [-(x$1), x$2])" for x
wenzelm@53572
   109
  have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
huffman@36432
   110
    unfolding negatex_def infnorm_2 vector_2 by auto
wenzelm@53572
   111
  have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
lp15@68054
   112
    unfolding sqprojection_def infnorm_mul[unfolded scalar_mult_eq_scaleR]
lp15@68054
   113
    by (simp add: real_abs_infnorm infnorm_eq_0)
wenzelm@53572
   114
  let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
lp15@68054
   115
  have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1..1}"
lp15@68054
   116
  proof 
lp15@68054
   117
    show "(\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 \<subseteq> {-1..1}" for i
lp15@68054
   118
      by (auto simp: mem_box_cart)
lp15@68054
   119
    show "{-1..1} \<subseteq> (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1" for i
lp15@68054
   120
      by (clarsimp simp: image_iff mem_box_cart Bex_def) (metis (no_types, hide_lams) vec_component)
lp15@68054
   121
  qed
wenzelm@53572
   122
  {
wenzelm@53572
   123
    fix x
immler@56188
   124
    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
   125
    then obtain w :: "real^2" where w:
immler@56188
   126
        "w \<in> cbox (- 1) 1"
wenzelm@55675
   127
        "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
wenzelm@55675
   128
      unfolding image_iff ..
wenzelm@53572
   129
    then have "x \<noteq> 0"
wenzelm@53572
   130
      using as[of "w$1" "w$2"]
lp15@67673
   131
      unfolding mem_box_cart atLeastAtMost_iff
wenzelm@53572
   132
      by auto
wenzelm@53572
   133
  } note x0 = this
immler@54775
   134
  have 1: "box (- 1) (1::real^2) \<noteq> {}"
wenzelm@53572
   135
    unfolding interval_eq_empty_cart by auto
lp15@68054
   136
  have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
lp15@68054
   137
    for i x y c
lp15@68054
   138
    using exhaust_2 [of i] by (auto simp: negatex_def)
lp15@68054
   139
  then have "bounded_linear negatex"
lp15@68054
   140
    by (simp add: bounded_linearI' vec_eq_iff)
lp15@68054
   141
  then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
hoelzl@56371
   142
    apply (intro continuous_intros continuous_on_component)
lp15@68054
   143
    unfolding * sqprojection_def
lp15@68054
   144
    apply (intro assms continuous_intros)+
lp15@68054
   145
     apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on)
lp15@68054
   146
    done
immler@56188
   147
  have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
wenzelm@53572
   148
    unfolding subset_eq
wenzelm@61166
   149
  proof (rule, goal_cases)
wenzelm@61165
   150
    case (1 x)
wenzelm@55675
   151
    then obtain y :: "real^2" where y:
haftmann@58410
   152
        "y \<in> cbox (- 1) 1"
wenzelm@55675
   153
        "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
wenzelm@55675
   154
      unfolding image_iff ..
wenzelm@53572
   155
    have "?F y \<noteq> 0"
lp15@68054
   156
      by (rule x0) (use y in auto)
wenzelm@53572
   157
    then have *: "infnorm (sqprojection (?F y)) = 1"
wenzelm@53628
   158
      unfolding y o_def
wenzelm@53628
   159
      by - (rule lem2[rule_format])
lp15@68054
   160
    have inf1: "infnorm x = 1"
wenzelm@53628
   161
      unfolding *[symmetric] y o_def
wenzelm@53628
   162
      by (rule lem1[rule_format])
lp15@68054
   163
    show "x \<in> cbox (-1) 1"
lp15@67673
   164
      unfolding mem_box_cart interval_cbox_cart infnorm_2
lp15@68054
   165
    proof 
wenzelm@61165
   166
      fix i
lp15@68054
   167
      show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
lp15@68054
   168
        using exhaust_2 [of i] inf1 by (auto simp: infnorm_2)
wenzelm@53572
   169
    qed
wenzelm@53572
   170
  qed
wenzelm@55675
   171
  obtain x :: "real^2" where x:
haftmann@58410
   172
      "x \<in> cbox (- 1) 1"
wenzelm@55675
   173
      "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
haftmann@58410
   174
    apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
immler@56188
   175
    apply (rule compact_cbox convex_box)+
immler@56188
   176
    unfolding interior_cbox
wenzelm@53572
   177
    apply (rule 1 2 3)+
wenzelm@55675
   178
    apply blast
wenzelm@53572
   179
    done
wenzelm@53572
   180
  have "?F x \<noteq> 0"
lp15@68054
   181
    by (rule x0) (use x in auto)
wenzelm@53572
   182
  then have *: "infnorm (sqprojection (?F x)) = 1"
wenzelm@53628
   183
    unfolding o_def
wenzelm@53628
   184
    by (rule lem2[rule_format])
wenzelm@53572
   185
  have nx: "infnorm x = 1"
wenzelm@53628
   186
    apply (subst x(2)[symmetric])
wenzelm@53628
   187
    unfolding *[symmetric] o_def
wenzelm@53572
   188
    apply (rule lem1[rule_format])
wenzelm@53572
   189
    done
lp15@68054
   190
  have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for x i
wenzelm@53572
   191
  proof -
wenzelm@53572
   192
    have "inverse (infnorm x) > 0"
lp15@68054
   193
      by (simp add: infnorm_pos_lt that)
wenzelm@53572
   194
    then show "(0 < sqprojection x $ i) = (0 < x $ i)"
wenzelm@53572
   195
      and "(sqprojection x $ i < 0) = (x $ i < 0)"
huffman@44282
   196
      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
wenzelm@53572
   197
      unfolding zero_less_mult_iff mult_less_0_iff
wenzelm@53572
   198
      by (auto simp add: field_simps)
wenzelm@53572
   199
  qed
wenzelm@53572
   200
  have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
lp15@67673
   201
    using x(1) unfolding mem_box_cart by auto
wenzelm@53572
   202
  then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
lp15@68054
   203
    using as by auto
lp15@68054
   204
  consider "x $ 1 = -1" | "x $ 1 = 1" | "x $ 2 = -1" | "x $ 2 = 1"
hoelzl@63594
   205
    using nx unfolding infnorm_eq_1_2 by auto
wenzelm@53572
   206
  then show False
lp15@68054
   207
  proof cases
lp15@68054
   208
    case 1
wenzelm@53572
   209
    then have *: "f (x $ 1) $ 1 = - 1"
wenzelm@53572
   210
      using assms(5) by auto
huffman@36432
   211
    have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
huffman@44136
   212
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
lp15@68054
   213
      by (auto simp: negatex_def 1)
wenzelm@53572
   214
    moreover
immler@56188
   215
    from x1 have "g (x $ 2) \<in> cbox (-1) 1"
lp15@67982
   216
      using assms(2) by blast
wenzelm@53572
   217
    ultimately show False
lp15@68054
   218
      unfolding iff[OF nz] vector_component_simps * mem_box_cart
lp15@67982
   219
      using not_le by auto
wenzelm@53572
   220
  next
lp15@68054
   221
    case 2
lp15@68054
   222
    then have *: "f (x $ 1) $ 1 = 1"
lp15@68054
   223
      using assms(6) by auto
lp15@68054
   224
    have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
lp15@68054
   225
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2
lp15@68054
   226
      by (auto simp: negatex_def)
lp15@68054
   227
    moreover have "g (x $ 2) \<in> cbox (-1) 1"
lp15@68054
   228
      using assms(2) x1 by blast
lp15@68054
   229
    ultimately show False
lp15@68054
   230
      unfolding iff[OF nz] vector_component_simps * mem_box_cart
lp15@68054
   231
      using not_le by auto
lp15@68054
   232
  next
lp15@68054
   233
    case 3
lp15@68054
   234
    then have *: "g (x $ 2) $ 2 = - 1"
lp15@68054
   235
      using assms(7) by auto
lp15@68054
   236
    have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
lp15@68054
   237
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def)
lp15@68054
   238
    moreover
lp15@68054
   239
    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
lp15@68054
   240
      using assms(1) by blast
lp15@68054
   241
    ultimately show False
lp15@68054
   242
      unfolding iff[OF nz] vector_component_simps * mem_box_cart
lp15@68054
   243
      by (erule_tac x=2 in allE) auto
lp15@68054
   244
  next
lp15@68054
   245
    case 4
wenzelm@53572
   246
    then have *: "g (x $ 2) $ 2 = 1"
wenzelm@53572
   247
      using assms(8) by auto
huffman@36432
   248
    have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
lp15@68054
   249
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def)
wenzelm@53572
   250
    moreover
immler@56188
   251
    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
lp15@68054
   252
      using assms(1) by blast
wenzelm@53572
   253
    ultimately show False
lp15@68054
   254
      unfolding iff[OF nz] vector_component_simps * mem_box_cart
lp15@68054
   255
      by (erule_tac x=2 in allE) auto
lp15@68054
   256
  qed 
wenzelm@53572
   257
qed
huffman@36432
   258
immler@69681
   259
proposition fashoda_unit_path:
wenzelm@53572
   260
  fixes f g :: "real \<Rightarrow> real^2"
wenzelm@53572
   261
  assumes "path f"
wenzelm@53572
   262
    and "path g"
immler@56188
   263
    and "path_image f \<subseteq> cbox (-1) 1"
immler@56188
   264
    and "path_image g \<subseteq> cbox (-1) 1"
wenzelm@53572
   265
    and "(pathstart f)$1 = -1"
wenzelm@53572
   266
    and "(pathfinish f)$1 = 1"
wenzelm@53572
   267
    and "(pathstart g)$2 = -1"
wenzelm@53572
   268
    and "(pathfinish g)$2 = 1"
wenzelm@53572
   269
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
immler@69681
   270
proof -
huffman@36432
   271
  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
wenzelm@63040
   272
  define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
wenzelm@53572
   273
  have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
wenzelm@53572
   274
    unfolding iscale_def by auto
wenzelm@53572
   275
  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
wenzelm@53572
   276
  proof (rule fashoda_unit)
haftmann@58410
   277
    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
haftmann@56154
   278
      using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
wenzelm@53572
   279
    have *: "continuous_on {- 1..1} iscale"
hoelzl@56371
   280
      unfolding iscale_def by (rule continuous_intros)+
huffman@36432
   281
    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
wenzelm@53572
   282
      apply -
wenzelm@53572
   283
      apply (rule_tac[!] continuous_on_compose[OF *])
wenzelm@53572
   284
      apply (rule_tac[!] continuous_on_subset[OF _ isc])
wenzelm@53572
   285
      apply (rule assms)+
wenzelm@53572
   286
      done
wenzelm@53572
   287
    have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
wenzelm@53572
   288
      unfolding vec_eq_iff by auto
wenzelm@53572
   289
    show "(f \<circ> iscale) (- 1) $ 1 = - 1"
wenzelm@53572
   290
      and "(f \<circ> iscale) 1 $ 1 = 1"
wenzelm@53572
   291
      and "(g \<circ> iscale) (- 1) $ 2 = -1"
wenzelm@53572
   292
      and "(g \<circ> iscale) 1 $ 2 = 1"
wenzelm@53572
   293
      unfolding o_def iscale_def
wenzelm@53572
   294
      using assms
wenzelm@53572
   295
      by (auto simp add: *)
wenzelm@53572
   296
  qed
wenzelm@55675
   297
  then obtain s t where st:
wenzelm@55675
   298
      "s \<in> {- 1..1}"
wenzelm@55675
   299
      "t \<in> {- 1..1}"
wenzelm@55675
   300
      "(f \<circ> iscale) s = (g \<circ> iscale) t"
immler@56188
   301
    by auto
wenzelm@53572
   302
  show thesis
wenzelm@53628
   303
    apply (rule_tac z = "f (iscale s)" in that)
wenzelm@55675
   304
    using st
wenzelm@53572
   305
    unfolding o_def path_image_def image_iff
wenzelm@53572
   306
    apply -
wenzelm@53572
   307
    apply (rule_tac x="iscale s" in bexI)
wenzelm@53572
   308
    prefer 3
wenzelm@53572
   309
    apply (rule_tac x="iscale t" in bexI)
wenzelm@53572
   310
    using isc[unfolded subset_eq, rule_format]
wenzelm@53572
   311
    apply auto
wenzelm@53572
   312
    done
wenzelm@53572
   313
qed
huffman@36432
   314
immler@69681
   315
theorem fashoda:
wenzelm@53627
   316
  fixes b :: "real^2"
wenzelm@53627
   317
  assumes "path f"
wenzelm@53627
   318
    and "path g"
immler@56188
   319
    and "path_image f \<subseteq> cbox a b"
immler@56188
   320
    and "path_image g \<subseteq> cbox a b"
wenzelm@53627
   321
    and "(pathstart f)$1 = a$1"
wenzelm@53627
   322
    and "(pathfinish f)$1 = b$1"
wenzelm@53627
   323
    and "(pathstart g)$2 = a$2"
wenzelm@53627
   324
    and "(pathfinish g)$2 = b$2"
wenzelm@53627
   325
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
immler@69681
   326
proof -
wenzelm@53627
   327
  fix P Q S
wenzelm@53627
   328
  presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
wenzelm@53627
   329
  then show thesis
wenzelm@53627
   330
    by auto
wenzelm@53627
   331
next
immler@56188
   332
  have "cbox a b \<noteq> {}"
immler@54775
   333
    using assms(3) using path_image_nonempty[of f] by auto
wenzelm@53627
   334
  then have "a \<le> b"
wenzelm@53627
   335
    unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
wenzelm@53627
   336
  then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
wenzelm@53627
   337
    unfolding less_eq_vec_def forall_2 by auto
wenzelm@53627
   338
next
wenzelm@53627
   339
  assume as: "a$1 = b$1"
wenzelm@53627
   340
  have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
wenzelm@53627
   341
    apply (rule connected_ivt_component_cart)
wenzelm@53627
   342
    apply (rule connected_path_image assms)+
wenzelm@53627
   343
    apply (rule pathstart_in_path_image)
wenzelm@53627
   344
    apply (rule pathfinish_in_path_image)
huffman@36432
   345
    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
wenzelm@53627
   346
    unfolding pathstart_def
lp15@67673
   347
    apply (auto simp add: less_eq_vec_def mem_box_cart)
wenzelm@53627
   348
    done
wenzelm@55675
   349
  then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
immler@56188
   350
  have "z \<in> cbox a b"
wenzelm@53627
   351
    using z(1) assms(4)
wenzelm@53627
   352
    unfolding path_image_def
immler@56188
   353
    by blast
wenzelm@53627
   354
  then have "z = f 0"
wenzelm@53627
   355
    unfolding vec_eq_iff forall_2
wenzelm@53627
   356
    unfolding z(2) pathstart_def
lp15@67673
   357
    using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
lp15@67673
   358
    unfolding mem_box_cart
wenzelm@53627
   359
    apply (erule_tac x=1 in allE)
wenzelm@53627
   360
    using as
wenzelm@53627
   361
    apply auto
wenzelm@53627
   362
    done
wenzelm@53627
   363
  then show thesis
wenzelm@53627
   364
    apply -
wenzelm@53627
   365
    apply (rule that[OF _ z(1)])
wenzelm@53627
   366
    unfolding path_image_def
wenzelm@53627
   367
    apply auto
wenzelm@53627
   368
    done
wenzelm@53627
   369
next
wenzelm@53627
   370
  assume as: "a$2 = b$2"
wenzelm@53627
   371
  have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
wenzelm@53627
   372
    apply (rule connected_ivt_component_cart)
wenzelm@53627
   373
    apply (rule connected_path_image assms)+
wenzelm@53627
   374
    apply (rule pathstart_in_path_image)
wenzelm@53627
   375
    apply (rule pathfinish_in_path_image)
wenzelm@53627
   376
    unfolding assms
wenzelm@53627
   377
    using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
wenzelm@53627
   378
    unfolding pathstart_def
lp15@67673
   379
    apply (auto simp add: less_eq_vec_def mem_box_cart)
wenzelm@53627
   380
    done
wenzelm@55675
   381
  then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
immler@56188
   382
  have "z \<in> cbox a b"
wenzelm@53627
   383
    using z(1) assms(3)
wenzelm@53627
   384
    unfolding path_image_def
immler@56188
   385
    by blast
wenzelm@53627
   386
  then have "z = g 0"
wenzelm@53627
   387
    unfolding vec_eq_iff forall_2
wenzelm@53627
   388
    unfolding z(2) pathstart_def
lp15@67673
   389
    using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
lp15@67673
   390
    unfolding mem_box_cart
wenzelm@53627
   391
    apply (erule_tac x=2 in allE)
wenzelm@53627
   392
    using as
wenzelm@53627
   393
    apply auto
wenzelm@53627
   394
    done
wenzelm@53627
   395
  then show thesis
wenzelm@53627
   396
    apply -
wenzelm@53627
   397
    apply (rule that[OF z(1)])
wenzelm@53627
   398
    unfolding path_image_def
wenzelm@53627
   399
    apply auto
wenzelm@53627
   400
    done
wenzelm@53627
   401
next
wenzelm@53627
   402
  assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
immler@56188
   403
  have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
wenzelm@53627
   404
    unfolding interval_eq_empty_cart by auto
wenzelm@55675
   405
  obtain z :: "real^2" where z:
wenzelm@55675
   406
      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
wenzelm@55675
   407
      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
hoelzl@63594
   408
    apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
huffman@36432
   409
    unfolding path_def path_image_def pathstart_def pathfinish_def
wenzelm@53627
   410
    apply (rule_tac[1-2] continuous_on_compose)
wenzelm@53627
   411
    apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
wenzelm@53627
   412
    unfolding subset_eq
wenzelm@53627
   413
    apply(rule_tac[1-2] ballI)
wenzelm@53627
   414
  proof -
wenzelm@53627
   415
    fix x
wenzelm@53627
   416
    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
wenzelm@55675
   417
    then obtain y where y:
wenzelm@55675
   418
        "y \<in> {0..1}"
wenzelm@55675
   419
        "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
wenzelm@55675
   420
      unfolding image_iff ..
haftmann@58410
   421
    show "x \<in> cbox (- 1) 1"
wenzelm@53627
   422
      unfolding y o_def
wenzelm@53627
   423
      apply (rule in_interval_interval_bij)
wenzelm@53627
   424
      using y(1)
wenzelm@53627
   425
      using assms(3)[unfolded path_image_def subset_eq] int_nem
wenzelm@53627
   426
      apply auto
wenzelm@53627
   427
      done
wenzelm@53627
   428
  next
wenzelm@53627
   429
    fix x
wenzelm@53627
   430
    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
wenzelm@55675
   431
    then obtain y where y:
wenzelm@55675
   432
        "y \<in> {0..1}"
wenzelm@55675
   433
        "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
wenzelm@55675
   434
      unfolding image_iff ..
haftmann@58410
   435
    show "x \<in> cbox (- 1) 1"
wenzelm@53627
   436
      unfolding y o_def
wenzelm@53627
   437
      apply (rule in_interval_interval_bij)
wenzelm@53627
   438
      using y(1)
wenzelm@53627
   439
      using assms(4)[unfolded path_image_def subset_eq] int_nem
wenzelm@53627
   440
      apply auto
wenzelm@53627
   441
      done
wenzelm@53627
   442
  next
wenzelm@53627
   443
    show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
wenzelm@53627
   444
      and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
wenzelm@53627
   445
      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
wenzelm@53627
   446
      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
immler@56188
   447
      using assms as
lp15@67982
   448
      by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
hoelzl@50526
   449
         (simp_all add: inner_axis)
wenzelm@53627
   450
  qed
wenzelm@55675
   451
  from z(1) obtain zf where zf:
wenzelm@55675
   452
      "zf \<in> {0..1}"
wenzelm@55675
   453
      "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
wenzelm@55675
   454
    unfolding image_iff ..
wenzelm@55675
   455
  from z(2) obtain zg where zg:
wenzelm@55675
   456
      "zg \<in> {0..1}"
wenzelm@55675
   457
      "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
wenzelm@55675
   458
    unfolding image_iff ..
wenzelm@53627
   459
  have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
wenzelm@53627
   460
    unfolding forall_2
wenzelm@53627
   461
    using as
wenzelm@53627
   462
    by auto
wenzelm@53627
   463
  show thesis
lp15@68054
   464
  proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
lp15@68054
   465
    show "interval_bij (- 1, 1) (a, b) z \<in> path_image f"
lp15@68054
   466
      using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def)
lp15@68054
   467
    show "interval_bij (- 1, 1) (a, b) z \<in> path_image g"
lp15@68054
   468
      using zg by (simp add: interval_bij_bij_cart[OF *] path_image_def)
lp15@68054
   469
  qed
wenzelm@53627
   470
qed
huffman@36432
   471
wenzelm@53627
   472
ak2110@69173
   473
subsection%unimportant \<open>Some slightly ad hoc lemmas I use below\<close>
huffman@36432
   474
wenzelm@53627
   475
lemma segment_vertical:
wenzelm@53627
   476
  fixes a :: "real^2"
wenzelm@53627
   477
  assumes "a$1 = b$1"
wenzelm@53627
   478
  shows "x \<in> closed_segment a b \<longleftrightarrow>
wenzelm@53627
   479
    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
   480
  (is "_ = ?R")
wenzelm@53627
   481
proof -
huffman@36432
   482
  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
   483
  {
wenzelm@53627
   484
    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
wenzelm@53627
   485
    then show ?thesis
wenzelm@53627
   486
      unfolding closed_segment_def mem_Collect_eq
wenzelm@53628
   487
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
wenzelm@53627
   488
      by blast
wenzelm@53627
   489
  }
wenzelm@53627
   490
  {
wenzelm@53627
   491
    assume ?L
wenzelm@55675
   492
    then obtain u where u:
wenzelm@55675
   493
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
wenzelm@55675
   494
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
wenzelm@55675
   495
        "0 \<le> u"
wenzelm@55675
   496
        "u \<le> 1"
wenzelm@55675
   497
      by blast
wenzelm@53627
   498
    { fix b a
wenzelm@53627
   499
      assume "b + u * a > a + u * b"
wenzelm@53627
   500
      then have "(1 - u) * b > (1 - u) * a"
wenzelm@53627
   501
        by (auto simp add:field_simps)
wenzelm@53627
   502
      then have "b \<ge> a"
haftmann@59555
   503
        apply (drule_tac mult_left_less_imp_less)
wenzelm@53627
   504
        using u
wenzelm@53627
   505
        apply auto
wenzelm@53627
   506
        done
wenzelm@53627
   507
      then have "u * a \<le> u * b"
wenzelm@53627
   508
        apply -
hoelzl@63594
   509
        apply (rule mult_left_mono[OF _ u(3)])
wenzelm@53627
   510
        using u(3-4)
wenzelm@53627
   511
        apply (auto simp add: field_simps)
wenzelm@53627
   512
        done
wenzelm@53627
   513
    } note * = this
wenzelm@53627
   514
    {
wenzelm@53627
   515
      fix a b
wenzelm@53627
   516
      assume "u * b > u * a"
wenzelm@53627
   517
      then have "(1 - u) * a \<le> (1 - u) * b"
wenzelm@53627
   518
        apply -
wenzelm@53627
   519
        apply (rule mult_left_mono)
haftmann@59555
   520
        apply (drule mult_left_less_imp_less)
wenzelm@53627
   521
        using u
wenzelm@53627
   522
        apply auto
wenzelm@53627
   523
        done
wenzelm@53627
   524
      then have "a + u * b \<le> b + u * a"
wenzelm@53627
   525
        by (auto simp add: field_simps)
wenzelm@53627
   526
    } note ** = this
wenzelm@53627
   527
    then show ?R
wenzelm@53627
   528
      unfolding u assms
wenzelm@53627
   529
      using u
wenzelm@53627
   530
      by (auto simp add:field_simps not_le intro: * **)
wenzelm@53627
   531
  }
wenzelm@53627
   532
  {
wenzelm@53627
   533
    assume ?R
wenzelm@53627
   534
    then show ?L
wenzelm@53627
   535
    proof (cases "x$2 = b$2")
wenzelm@53627
   536
      case True
wenzelm@53627
   537
      then show ?L
wenzelm@53627
   538
        apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
lp15@68310
   539
        unfolding assms True using \<open>?R\<close> apply (auto simp add: field_simps)
wenzelm@53627
   540
        done
wenzelm@53627
   541
    next
wenzelm@53627
   542
      case False
wenzelm@53627
   543
      then show ?L
wenzelm@53627
   544
        apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
lp15@68310
   545
        unfolding assms using \<open>?R\<close> apply (auto simp add: field_simps)
wenzelm@53627
   546
        done
wenzelm@53627
   547
    qed
wenzelm@53627
   548
  }
wenzelm@53627
   549
qed
huffman@36432
   550
wenzelm@53627
   551
lemma segment_horizontal:
wenzelm@53627
   552
  fixes a :: "real^2"
wenzelm@53627
   553
  assumes "a$2 = b$2"
wenzelm@53627
   554
  shows "x \<in> closed_segment a b \<longleftrightarrow>
wenzelm@53627
   555
    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
   556
  (is "_ = ?R")
wenzelm@53627
   557
proof -
huffman@36432
   558
  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
   559
  {
wenzelm@53627
   560
    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
wenzelm@53627
   561
    then show ?thesis
wenzelm@53627
   562
      unfolding closed_segment_def mem_Collect_eq
wenzelm@53628
   563
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
wenzelm@53627
   564
      by blast
wenzelm@53627
   565
  }
wenzelm@53627
   566
  {
wenzelm@53627
   567
    assume ?L
wenzelm@55675
   568
    then obtain u where u:
wenzelm@55675
   569
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
wenzelm@55675
   570
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
wenzelm@55675
   571
        "0 \<le> u"
wenzelm@55675
   572
        "u \<le> 1"
wenzelm@55675
   573
      by blast
wenzelm@53627
   574
    {
wenzelm@53627
   575
      fix b a
wenzelm@53627
   576
      assume "b + u * a > a + u * b"
wenzelm@53627
   577
      then have "(1 - u) * b > (1 - u) * a"
wenzelm@53628
   578
        by (auto simp add: field_simps)
wenzelm@53627
   579
      then have "b \<ge> a"
haftmann@59555
   580
        apply (drule_tac mult_left_less_imp_less)
wenzelm@53627
   581
        using u
wenzelm@53627
   582
        apply auto
wenzelm@53627
   583
        done
wenzelm@53627
   584
      then have "u * a \<le> u * b"
wenzelm@53627
   585
        apply -
wenzelm@53627
   586
        apply (rule mult_left_mono[OF _ u(3)])
wenzelm@53627
   587
        using u(3-4)
wenzelm@53627
   588
        apply (auto simp add: field_simps)
wenzelm@53627
   589
        done
wenzelm@53627
   590
    } note * = this
wenzelm@53627
   591
    {
wenzelm@53627
   592
      fix a b
wenzelm@53627
   593
      assume "u * b > u * a"
wenzelm@53627
   594
      then have "(1 - u) * a \<le> (1 - u) * b"
wenzelm@53627
   595
        apply -
wenzelm@53627
   596
        apply (rule mult_left_mono)
haftmann@59555
   597
        apply (drule mult_left_less_imp_less)
wenzelm@53627
   598
        using u
wenzelm@53627
   599
        apply auto
wenzelm@53627
   600
        done
wenzelm@53627
   601
      then have "a + u * b \<le> b + u * a"
wenzelm@53627
   602
        by (auto simp add: field_simps)
wenzelm@53627
   603
    } note ** = this
wenzelm@53627
   604
    then show ?R
wenzelm@53627
   605
      unfolding u assms
wenzelm@53627
   606
      using u
wenzelm@53627
   607
      by (auto simp add: field_simps not_le intro: * **)
wenzelm@53627
   608
  }
wenzelm@53627
   609
  {
wenzelm@53627
   610
    assume ?R
wenzelm@53627
   611
    then show ?L
wenzelm@53627
   612
    proof (cases "x$1 = b$1")
wenzelm@53627
   613
      case True
wenzelm@53627
   614
      then show ?L
wenzelm@53627
   615
        apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
wenzelm@53627
   616
        unfolding assms True
wenzelm@60420
   617
        using \<open>?R\<close>
wenzelm@53627
   618
        apply (auto simp add: field_simps)
wenzelm@53627
   619
        done
wenzelm@53627
   620
    next
wenzelm@53627
   621
      case False
wenzelm@53627
   622
      then show ?L
wenzelm@53627
   623
        apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
wenzelm@53627
   624
        unfolding assms
wenzelm@60420
   625
        using \<open>?R\<close>
wenzelm@53627
   626
        apply (auto simp add: field_simps)
wenzelm@53627
   627
        done
wenzelm@53627
   628
    qed
wenzelm@53627
   629
  }
wenzelm@53627
   630
qed
huffman@36432
   631
wenzelm@53627
   632
immler@69683
   633
subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>(*FIXME change title? *)
huffman@36432
   634
immler@69681
   635
corollary fashoda_interlace:
wenzelm@53627
   636
  fixes a :: "real^2"
wenzelm@53627
   637
  assumes "path f"
wenzelm@53627
   638
    and "path g"
lp15@68054
   639
    and paf: "path_image f \<subseteq> cbox a b"
lp15@68054
   640
    and pag: "path_image g \<subseteq> cbox a b"
wenzelm@53627
   641
    and "(pathstart f)$2 = a$2"
wenzelm@53627
   642
    and "(pathfinish f)$2 = a$2"
wenzelm@53627
   643
    and "(pathstart g)$2 = a$2"
wenzelm@53627
   644
    and "(pathfinish g)$2 = a$2"
wenzelm@53627
   645
    and "(pathstart f)$1 < (pathstart g)$1"
wenzelm@53627
   646
    and "(pathstart g)$1 < (pathfinish f)$1"
wenzelm@53627
   647
    and "(pathfinish f)$1 < (pathfinish g)$1"
wenzelm@53627
   648
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
immler@69681
   649
proof -
immler@56188
   650
  have "cbox a b \<noteq> {}"
immler@54775
   651
    using path_image_nonempty[of f] using assms(3) by auto
hoelzl@37489
   652
  note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
immler@56188
   653
  have "pathstart f \<in> cbox a b"
immler@56188
   654
    and "pathfinish f \<in> cbox a b"
immler@56188
   655
    and "pathstart g \<in> cbox a b"
immler@56188
   656
    and "pathfinish g \<in> cbox a b"
wenzelm@53628
   657
    using pathstart_in_path_image pathfinish_in_path_image
wenzelm@53628
   658
    using assms(3-4)
wenzelm@53628
   659
    by auto
lp15@67673
   660
  note startfin = this[unfolded mem_box_cart forall_2]
huffman@36432
   661
  let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
huffman@36432
   662
     linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
huffman@36432
   663
     linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
hoelzl@63594
   664
     linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])"
huffman@36432
   665
  let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
huffman@36432
   666
     linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
huffman@36432
   667
     linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
huffman@36432
   668
     linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
huffman@36432
   669
  let ?a = "vector[a$1 - 2, a$2 - 3]"
huffman@36432
   670
  let ?b = "vector[b$1 + 2, b$2 + 3]"
wenzelm@53627
   671
  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
   672
      path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
huffman@36432
   673
      path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
huffman@36432
   674
      path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
huffman@36432
   675
    "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
huffman@36432
   676
      path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
huffman@36432
   677
      path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
huffman@36432
   678
      path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
huffman@36432
   679
      by(auto simp add: path_image_join path_linepath)
immler@56188
   680
  have abab: "cbox a b \<subseteq> cbox ?a ?b"
immler@56188
   681
    unfolding interval_cbox_cart[symmetric]
wenzelm@53627
   682
    by (auto simp add:less_eq_vec_def forall_2 vector_2)
wenzelm@55675
   683
  obtain z where
wenzelm@55675
   684
    "z \<in> path_image
wenzelm@55675
   685
          (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
wenzelm@55675
   686
           linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++
wenzelm@55675
   687
           f +++
wenzelm@55675
   688
           linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++
wenzelm@55675
   689
           linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))"
wenzelm@55675
   690
    "z \<in> path_image
wenzelm@55675
   691
          (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++
wenzelm@55675
   692
           g +++
wenzelm@55675
   693
           linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++
wenzelm@55675
   694
           linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++
wenzelm@55675
   695
           linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))"
wenzelm@53627
   696
    apply (rule fashoda[of ?P1 ?P2 ?a ?b])
wenzelm@53627
   697
    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
wenzelm@53627
   698
  proof -
wenzelm@53628
   699
    show "path ?P1" and "path ?P2"
wenzelm@53627
   700
      using assms by auto
lp15@68054
   701
    show "path_image ?P1 \<subseteq> cbox ?a ?b" "path_image ?P2 \<subseteq> cbox ?a ?b"
lp15@68054
   702
      unfolding P1P2 path_image_linepath using startfin paf pag
lp15@68054
   703
      by (auto simp: mem_box_cart segment_horizontal segment_vertical forall_2)
wenzelm@53627
   704
    show "a $ 1 - 2 = a $ 1 - 2"
wenzelm@53627
   705
      and "b $ 1 + 2 = b $ 1 + 2"
wenzelm@53627
   706
      and "pathstart g $ 2 - 3 = a $ 2 - 3"
wenzelm@53627
   707
      and "b $ 2 + 3 = b $ 2 + 3"
wenzelm@53627
   708
      by (auto simp add: assms)
wenzelm@53628
   709
  qed
wenzelm@53628
   710
  note z=this[unfolded P1P2 path_image_linepath]
wenzelm@53627
   711
  show thesis
lp15@68054
   712
  proof (rule that[of z])
huffman@36432
   713
    have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
wenzelm@53627
   714
      z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
wenzelm@53627
   715
      z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
wenzelm@53627
   716
      z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
wenzelm@53627
   717
    (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
wenzelm@53627
   718
      z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
wenzelm@53627
   719
      z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
wenzelm@53627
   720
      z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
wenzelm@61166
   721
    proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
wenzelm@61167
   722
      case prems: 1
immler@56188
   723
      have "pathfinish f \<in> cbox a b"
hoelzl@63594
   724
        using assms(3) pathfinish_in_path_image[of f] by auto
wenzelm@53628
   725
      then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
lp15@67673
   726
        unfolding mem_box_cart forall_2 by auto
wenzelm@53627
   727
      then have "z$1 \<noteq> pathfinish f$1"
wenzelm@61167
   728
        using prems(2)
wenzelm@53628
   729
        using assms ab
wenzelm@53628
   730
        by (auto simp add: field_simps)
immler@56188
   731
      moreover have "pathstart f \<in> cbox a b"
wenzelm@53628
   732
        using assms(3) pathstart_in_path_image[of f]
wenzelm@53628
   733
        by auto
wenzelm@53627
   734
      then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
lp15@67673
   735
        unfolding mem_box_cart forall_2
wenzelm@53628
   736
        by auto
wenzelm@53627
   737
      then have "z$1 \<noteq> pathstart f$1"
wenzelm@61167
   738
        using prems(2) using assms ab
wenzelm@53628
   739
        by (auto simp add: field_simps)
wenzelm@53627
   740
      ultimately have *: "z$2 = a$2 - 2"
lp15@68054
   741
        using prems(1) by auto
wenzelm@53627
   742
      have "z$1 \<noteq> pathfinish g$1"
lp15@68054
   743
        using prems(2) assms ab
wenzelm@53628
   744
        by (auto simp add: field_simps *)
immler@56188
   745
      moreover have "pathstart g \<in> cbox a b"
wenzelm@53628
   746
        using assms(4) pathstart_in_path_image[of g]
hoelzl@63594
   747
        by auto
lp15@67673
   748
      note this[unfolded mem_box_cart forall_2]
wenzelm@53627
   749
      then have "z$1 \<noteq> pathstart g$1"
lp15@68054
   750
        using prems(1) assms ab
wenzelm@53628
   751
        by (auto simp add: field_simps *)
huffman@36432
   752
      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"
lp15@68054
   753
        using prems(2)  unfolding * assms by (auto simp add: field_simps)
wenzelm@53627
   754
      then show False
wenzelm@53627
   755
        unfolding * using ab by auto
wenzelm@53627
   756
    qed
wenzelm@53627
   757
    then have "z \<in> path_image f \<or> z \<in> path_image g"
wenzelm@53627
   758
      using z unfolding Un_iff by blast
immler@56188
   759
    then have z': "z \<in> cbox a b"
lp15@68054
   760
      using assms(3-4) by auto
wenzelm@53627
   761
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
wenzelm@53627
   762
      z = pathstart f \<or> z = pathfinish f"
wenzelm@53628
   763
      unfolding vec_eq_iff forall_2 assms
wenzelm@53628
   764
      by auto
wenzelm@53627
   765
    with z' show "z \<in> path_image f"
wenzelm@53627
   766
      using z(1)
lp15@67673
   767
      unfolding Un_iff mem_box_cart forall_2
lp15@68054
   768
      by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
wenzelm@53627
   769
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
wenzelm@53627
   770
      z = pathstart g \<or> z = pathfinish g"
wenzelm@53628
   771
      unfolding vec_eq_iff forall_2 assms
wenzelm@53628
   772
      by auto
wenzelm@53627
   773
    with z' show "z \<in> path_image g"
wenzelm@53627
   774
      using z(2)
lp15@67673
   775
      unfolding Un_iff mem_box_cart forall_2
lp15@68054
   776
      by (simp only: segment_vertical segment_horizontal vector_2) (auto simp: assms)
wenzelm@53627
   777
  qed
wenzelm@53627
   778
qed
huffman@36432
   779
huffman@36432
   780
end