src/HOL/Multivariate_Analysis/Fashoda.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 44647 e4de7750cdeb
child 50526 899c9c4e4a4c
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     1
(* Author:                     John Harrison
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     2
   Translation from HOL light: Robert Himmelmann, TU Muenchen *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     3
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     4
header {* Fashoda meet theorem. *}
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     5
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     6
theory Fashoda
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
     7
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     8
begin
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     9
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    10
subsection {*Fashoda meet theorem. *}
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    11
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    12
lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    13
  unfolding infnorm_cart UNIV_2 apply(rule Sup_eq) by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    14
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    15
lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    16
        (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    17
  unfolding infnorm_2 by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    18
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    19
lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    20
  using assms unfolding infnorm_eq_1_2 by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    21
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    22
lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    23
  assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    24
  "continuous_on {- 1..1} f"  "continuous_on {- 1..1} g"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    25
  "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    26
  shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    27
  case goal1 note as = this[unfolded bex_simps,rule_format]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    28
  def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    29
  def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    30
  have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    31
    unfolding negatex_def infnorm_2 vector_2 by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    32
  have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    33
    unfolding infnorm_mul[unfolded smult_conv_scaleR] unfolding abs_inverse real_abs_infnorm
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    34
    apply(subst infnorm_eq_0[THEN sym]) by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    35
  let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    36
  have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 37674
diff changeset
    37
    apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer 
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    38
    apply(rule_tac x="vec x" in exI) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    39
  { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    40
    then guess w unfolding image_iff .. note w = this
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    41
    hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    42
  have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    43
  have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    44
  have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)"
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    45
    apply(intro continuous_on_intros continuous_on_component)
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    46
    unfolding * apply(rule assms)+
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    47
    apply(subst sqprojection_def)
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    48
    apply(intro continuous_on_intros)
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    49
    apply(simp add: infnorm_eq_0 x0)
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    50
    apply(rule linear_continuous_on)
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    51
  proof-
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
    52
    show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real
36593
fb69c8cd27bd define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents: 36583
diff changeset
    53
      show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
41958
5abc60a017e0 eliminated hard tabs;
wenzelm
parents: 39302
diff changeset
    54
        apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) 
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    55
        unfolding negatex_def by(auto simp add:vector_2 ) qed
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
    56
  qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    57
  have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    58
    case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    59
    hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format])
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    60
    have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format])
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    61
    thus "x\<in>{- 1..1}" unfolding mem_interval_cart infnorm_2 apply- apply rule
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    62
    proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    63
  guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"])
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    64
    apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    65
    apply(rule 1 2 3)+ . note x=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    66
  have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    67
  hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format])
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    68
  have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format])
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    69
  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"    "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    70
    apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    71
    have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    72
    thus "(0 < sqprojection x $ i) = (0 < x $ i)"   "(sqprojection x $ i < 0) = (x $ i < 0)"
44282
f0de18b62d63 remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents: 44136
diff changeset
    73
      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    74
      unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    75
  note lem3 = this[rule_format]
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    76
  have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    77
  hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    78
  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    79
  thus False proof- fix P Q R S 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    80
    presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    81
  next assume as:"x$1 = 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    82
    hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    83
    have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
    84
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    85
      unfolding as negatex_def vector_2 by auto moreover
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    86
    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    87
    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    88
      apply(erule_tac x=1 in allE) by auto 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    89
  next assume as:"x$1 = -1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    90
    hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    91
    have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
    92
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    93
      unfolding as negatex_def vector_2 by auto moreover
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    94
    from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
    95
    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    96
      apply(erule_tac x=1 in allE) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    97
  next assume as:"x$2 = 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    98
    hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    99
    have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   100
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   101
      unfolding as negatex_def vector_2 by auto moreover
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   102
    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   103
    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   104
     apply(erule_tac x=2 in allE) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   105
 next assume as:"x$2 = -1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   106
    hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   107
    have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   108
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   109
      unfolding as negatex_def vector_2 by auto moreover
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   110
    from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   111
    ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart 
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   112
      apply(erule_tac x=2 in allE) by auto qed(auto) qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   113
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   114
lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   115
  assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   116
  "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1"  "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   117
  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   118
  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   119
  def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   120
  have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   121
  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   122
    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   123
      using isc and assms(3-4) unfolding image_compose by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   124
    have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   125
    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   126
      apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc])
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   127
      by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   128
    show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   129
      unfolding o_def iscale_def using assms by(auto simp add:*) qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   130
  then guess s .. from this(2) guess t .. note st=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   131
  show thesis apply(rule_tac z="f (iscale s)" in that)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   132
    using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   133
    apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   134
    using isc[unfolded subset_eq, rule_format] by auto qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   135
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   136
(* move *)
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   137
lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" 
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   138
  shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   139
  unfolding interval_bij_cart split_conv vec_eq_iff vec_lambda_beta
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   140
  apply(rule,insert assms,erule_tac x=i in allE) by auto
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   141
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   142
lemma fashoda: fixes b::"real^2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   143
  assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   144
  "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   145
  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   146
  obtains z where "z \<in> path_image f" "z \<in> path_image g" proof-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   147
  fix P Q S presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" "Q \<Longrightarrow> thesis" "S \<Longrightarrow> thesis" thus thesis by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   148
next have "{a..b} \<noteq> {}" using assms(3) using path_image_nonempty by auto
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   149
  hence "a \<le> b" unfolding interval_eq_empty_cart less_eq_vec_def by(auto simp add: not_less)
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   150
  thus "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" unfolding less_eq_vec_def forall_2 by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   151
next assume as:"a$1 = b$1" have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component_cart)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   152
    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   153
    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   154
    unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   155
  have "z \<in> {a..b}" using z(1) assms(4) unfolding path_image_def by blast 
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   156
  hence "z = f 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   157
    using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   158
    unfolding mem_interval_cart apply(erule_tac x=1 in allE) using as by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   159
  thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   160
next assume as:"a$2 = b$2" have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component_cart)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   161
    apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   162
    unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   163
    unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   164
  have "z \<in> {a..b}" using z(1) assms(3) unfolding path_image_def by blast 
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   165
  hence "z = g 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   166
    using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2]
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   167
    unfolding mem_interval_cart apply(erule_tac x=2 in allE) using as by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   168
  thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   169
next assume as:"a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   170
  have int_nem:"{- 1..1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   171
  guess z apply(rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   172
    unfolding path_def path_image_def pathstart_def pathfinish_def
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   173
    apply(rule_tac[1-2] continuous_on_compose) apply(rule assms[unfolded path_def] continuous_on_interval_bij)+
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   174
    unfolding subset_eq apply(rule_tac[1-2] ballI)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   175
  proof- fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   176
    then guess y unfolding image_iff .. note y=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   177
    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   178
      using y(1) using assms(3)[unfolded path_image_def subset_eq] int_nem by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   179
  next fix x assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   180
    then guess y unfolding image_iff .. note y=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   181
    show "x \<in> {- 1..1}" unfolding y o_def apply(rule in_interval_interval_bij)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   182
      using y(1) using assms(4)[unfolded path_image_def subset_eq] int_nem by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   183
  next show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   184
      "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   185
      "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   186
      "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
44457
d366fa5551ef declare euclidean_simps [simp] at the point they are proved;
huffman
parents: 44282
diff changeset
   187
      unfolding interval_bij_cart vector_component_simps o_def split_conv
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   188
      unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   189
  from z(1) guess zf unfolding image_iff .. note zf=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   190
  from z(2) guess zg unfolding image_iff .. note zg=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   191
  have *:"\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" unfolding forall_2 using as by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   192
  show thesis apply(rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   193
    apply(subst zf) defer apply(subst zg) unfolding o_def interval_bij_bij_cart[OF *] path_image_def
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   194
    using zf(1) zg(1) by auto qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   195
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   196
subsection {*Some slightly ad hoc lemmas I use below*}
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   197
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   198
lemma segment_vertical: fixes a::"real^2" assumes "a$1 = b$1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   199
  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$1 = a$1 \<and> x$1 = b$1 \<and>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   200
           (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2))" (is "_ = ?R")
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   201
proof- 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   202
  let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   203
  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   204
      unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   205
  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   206
    { fix b a assume "b + u * a > a + u * b"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   207
      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   208
      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   209
      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   210
        using u(3-4) by(auto simp add:field_simps) } note * = this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   211
    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   212
        apply(drule mult_less_imp_less_left) using u by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   213
      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   214
    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   215
  { assume ?R thus ?L proof(cases "x$2 = b$2")
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   216
      case True thus ?L apply(rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) unfolding assms True
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   217
        using `?R` by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   218
    next case False thus ?L apply(rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) unfolding assms using `?R`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   219
        by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   220
    qed } qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   221
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   222
lemma segment_horizontal: fixes a::"real^2" assumes "a$2 = b$2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   223
  shows "x \<in> closed_segment a b \<longleftrightarrow> (x$2 = a$2 \<and> x$2 = b$2 \<and>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   224
           (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1))" (is "_ = ?R")
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   225
proof- 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   226
  let ?L = "\<exists>u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \<and> x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \<and> 0 \<le> u \<and> u \<le> 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   227
  { presume "?L \<Longrightarrow> ?R" "?R \<Longrightarrow> ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   228
      unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast }
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   229
  { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   230
    { fix b a assume "b + u * a > a + u * b"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   231
      hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   232
      hence "b \<ge> a" apply(drule_tac mult_less_imp_less_left) using u by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   233
      hence "u * a \<le> u * b" apply-apply(rule mult_left_mono[OF _ u(3)]) 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   234
        using u(3-4) by(auto simp add:field_simps) } note * = this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   235
    { fix a b assume "u * b > u * a" hence "(1 - u) * a \<le> (1 - u) * b" apply-apply(rule mult_left_mono)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   236
        apply(drule mult_less_imp_less_left) using u by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   237
      hence "a + u * b \<le> b + u * a" by(auto simp add:field_simps) } note ** = this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   238
    thus ?R unfolding u assms using u by(auto simp add:field_simps not_le intro:* **) }
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   239
  { assume ?R thus ?L proof(cases "x$1 = b$1")
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   240
      case True thus ?L apply(rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) unfolding assms True
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   241
        using `?R` by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   242
    next case False thus ?L apply(rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) unfolding assms using `?R`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   243
        by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   244
    qed } qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   245
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   246
subsection {*useful Fashoda corollary pointed out to me by Tom Hales. *}
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   247
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   248
lemma fashoda_interlace: fixes a::"real^2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   249
  assumes "path f" "path g"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   250
  "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   251
  "(pathstart f)$2 = a$2" "(pathfinish f)$2 = a$2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   252
  "(pathstart g)$2 = a$2" "(pathfinish g)$2 = a$2"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   253
  "(pathstart f)$1 < (pathstart g)$1" "(pathstart g)$1 < (pathfinish f)$1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   254
  "(pathfinish f)$1 < (pathfinish g)$1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   255
  obtains z where "z \<in> path_image f" "z \<in> path_image g"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   256
proof-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   257
  have "{a..b} \<noteq> {}" using path_image_nonempty using assms(3) by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   258
  note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   259
  have "pathstart f \<in> {a..b}" "pathfinish f \<in> {a..b}" "pathstart g \<in> {a..b}" "pathfinish g \<in> {a..b}"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   260
    using pathstart_in_path_image pathfinish_in_path_image using assms(3-4) by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   261
  note startfin = this[unfolded mem_interval_cart forall_2]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   262
  let ?P1 = "linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2]) +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   263
     linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f) +++ f +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   264
     linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   265
     linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])" 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   266
  let ?P2 = "linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g) +++ g +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   267
     linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   268
     linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1]) +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   269
     linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3])"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   270
  let ?a = "vector[a$1 - 2, a$2 - 3]"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   271
  let ?b = "vector[b$1 + 2, b$2 + 3]"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   272
  have P1P2:"path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   273
      path_image (linepath(vector[(pathstart f)$1,a$2 - 2])(pathstart f)) \<union> path_image f \<union>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   274
      path_image (linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2])) \<union>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   275
      path_image (linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2]))"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   276
    "path_image ?P2 = path_image(linepath(vector[(pathstart g)$1, (pathstart g)$2 - 3])(pathstart g)) \<union> path_image g \<union>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   277
      path_image(linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1])) \<union>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   278
      path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \<union>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   279
      path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   280
      by(auto simp add: path_image_join path_linepath)
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   281
  have abab: "{a..b} \<subseteq> {?a..?b}" by(auto simp add:less_eq_vec_def forall_2 vector_2)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   282
  guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b])
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   283
    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   284
    show "path ?P1" "path ?P2" using assms by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   285
    have "path_image ?P1 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 3
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   286
      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   287
      unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(3)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   288
      using assms(9-) unfolding assms by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   289
    thus "path_image ?P1  \<subseteq> {?a .. ?b}" .
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   290
    have "path_image ?P2 \<subseteq> {?a .. ?b}" unfolding P1P2 path_image_linepath apply(rule Un_least)+ defer 2
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   291
      apply(rule_tac[1-4] convex_interval(1)[unfolded convex_contains_segment,rule_format])
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   292
      unfolding mem_interval_cart forall_2 vector_2 using ab startfin abab assms(4)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   293
      using assms(9-) unfolding assms  by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   294
    thus "path_image ?P2  \<subseteq> {?a .. ?b}" . 
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   295
    show "a $ 1 - 2 = a $ 1 - 2"  "b $ 1 + 2 = b $ 1 + 2" "pathstart g $ 2 - 3 = a $ 2 - 3"  "b $ 2 + 3 = b $ 2 + 3"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   296
      by(auto simp add: assms)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   297
  qed note z=this[unfolded P1P2 path_image_linepath]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   298
  show thesis apply(rule that[of z]) proof-
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   299
    have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   300
     z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   301
   z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   302
  z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   303
  (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   304
    z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   305
   z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   306
  z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   307
      apply(simp only: segment_vertical segment_horizontal vector_2) proof- case goal1 note as=this
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   308
      have "pathfinish f \<in> {a..b}" using assms(3) pathfinish_in_path_image[of f] by auto 
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   309
      hence "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   310
      hence "z$1 \<noteq> pathfinish f$1" using as(2) using assms ab by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   311
      moreover have "pathstart f \<in> {a..b}" using assms(3) pathstart_in_path_image[of f] by auto 
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   312
      hence "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False" unfolding mem_interval_cart forall_2 by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   313
      hence "z$1 \<noteq> pathstart f$1" using as(2) using assms ab by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   314
      ultimately have *:"z$2 = a$2 - 2" using goal1(1) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   315
      have "z$1 \<noteq> pathfinish g$1" using as(2) using assms ab by(auto simp add:field_simps *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   316
      moreover have "pathstart g \<in> {a..b}" using assms(4) pathstart_in_path_image[of g] by auto 
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   317
      note this[unfolded mem_interval_cart forall_2]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   318
      hence "z$1 \<noteq> pathstart g$1" using as(1) using assms ab by(auto simp add:field_simps *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   319
      ultimately have "a $ 2 - 1 \<le> z $ 2 \<and> z $ 2 \<le> b $ 2 + 3 \<or> b $ 2 + 3 \<le> z $ 2 \<and> z $ 2 \<le> a $ 2 - 1"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   320
        using as(2) unfolding * assms by(auto simp add:field_simps)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   321
      thus False unfolding * using ab by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   322
    qed hence "z \<in> path_image f \<or> z \<in> path_image g" using z unfolding Un_iff by blast
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   323
    hence z':"z\<in>{a..b}" using assms(3-4) by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   324
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow> (z = pathstart f \<or> z = pathfinish f)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   325
      unfolding vec_eq_iff forall_2 assms by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   326
    with z' show "z\<in>path_image f" using z(1) unfolding Un_iff mem_interval_cart forall_2 apply-
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   327
      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   328
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow> (z = pathstart g \<or> z = pathfinish g)"
44136
e63ad7d5158d more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents: 41958
diff changeset
   329
      unfolding vec_eq_iff forall_2 assms by auto
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   330
    with z' show "z\<in>path_image g" using z(2) unfolding Un_iff mem_interval_cart forall_2 apply-
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   331
      apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   332
  qed qed
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   333
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   334
(** The Following still needs to be translated. Maybe I will do that later.
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   335
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   336
(* ------------------------------------------------------------------------- *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   337
(* Complement in dimension N >= 2 of set homeomorphic to any interval in     *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   338
(* any dimension is (path-)connected. This naively generalizes the argument  *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   339
(* in Ryuji Maehara's paper "The Jordan curve theorem via the Brouwer        *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   340
(* fixed point theorem", American Mathematical Monthly 1984.                 *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   341
(* ------------------------------------------------------------------------- *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   342
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   343
let RETRACTION_INJECTIVE_IMAGE_INTERVAL = prove
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   344
 (`!p:real^M->real^N a b.
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   345
        ~(interval[a,b] = {}) /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   346
        p continuous_on interval[a,b] /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   347
        (!x y. x IN interval[a,b] /\ y IN interval[a,b] /\ p x = p y ==> x = y)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   348
        ==> ?f. f continuous_on (:real^N) /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   349
                IMAGE f (:real^N) SUBSET (IMAGE p (interval[a,b])) /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   350
                (!x. x IN (IMAGE p (interval[a,b])) ==> f x = x)`,
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   351
  REPEAT STRIP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   352
  FIRST_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INJECTIVE_ON_LEFT_INVERSE]) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   353
  DISCH_THEN(X_CHOOSE_TAC `q:real^N->real^M`) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   354
  SUBGOAL_THEN `(q:real^N->real^M) continuous_on
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   355
                (IMAGE p (interval[a:real^M,b]))`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   356
  ASSUME_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   357
   [MATCH_MP_TAC CONTINUOUS_ON_INVERSE THEN ASM_REWRITE_TAC[COMPACT_INTERVAL];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   358
    ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   359
  MP_TAC(ISPECL [`q:real^N->real^M`;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   360
                 `IMAGE (p:real^M->real^N)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   361
                 (interval[a,b])`;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   362
                 `a:real^M`; `b:real^M`]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   363
        TIETZE_CLOSED_INTERVAL) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   364
  ASM_SIMP_TAC[COMPACT_INTERVAL; COMPACT_CONTINUOUS_IMAGE;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   365
               COMPACT_IMP_CLOSED] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   366
  ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   367
  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^M` STRIP_ASSUME_TAC) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   368
  EXISTS_TAC `(p:real^M->real^N) o (r:real^N->real^M)` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   369
  REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_UNIV] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   370
  CONJ_TAC THENL [ALL_TAC; ASM SET_TAC[]] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   371
  MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN ASM_REWRITE_TAC[] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   372
  FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP(REWRITE_RULE[IMP_CONJ]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   373
        CONTINUOUS_ON_SUBSET)) THEN ASM SET_TAC[]);;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   374
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   375
let UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   376
 (`!s:real^N->bool a b:real^M.
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   377
        s homeomorphic (interval[a,b])
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   378
        ==> !x. ~(x IN s) ==> ~bounded(path_component((:real^N) DIFF s) x)`,
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   379
  REPEAT GEN_TAC THEN REWRITE_TAC[homeomorphic; homeomorphism] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   380
  REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   381
  MAP_EVERY X_GEN_TAC [`p':real^N->real^M`; `p:real^M->real^N`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   382
  DISCH_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   383
  SUBGOAL_THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   384
   `!x y. x IN interval[a,b] /\ y IN interval[a,b] /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   385
          (p:real^M->real^N) x = p y ==> x = y`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   386
  ASSUME_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   387
  FIRST_X_ASSUM(MP_TAC o funpow 4 CONJUNCT2) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   388
  DISCH_THEN(CONJUNCTS_THEN2 (SUBST1_TAC o SYM) ASSUME_TAC) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   389
  ASM_CASES_TAC `interval[a:real^M,b] = {}` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   390
  ASM_REWRITE_TAC[IMAGE_CLAUSES; DIFF_EMPTY; PATH_COMPONENT_UNIV;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   391
                  NOT_BOUNDED_UNIV] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   392
  ABBREV_TAC `s = (:real^N) DIFF (IMAGE p (interval[a:real^M,b]))` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   393
  X_GEN_TAC `c:real^N` THEN REPEAT STRIP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   394
  SUBGOAL_THEN `(c:real^N) IN s` ASSUME_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   395
  SUBGOAL_THEN `bounded((path_component s c) UNION
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   396
                        (IMAGE (p:real^M->real^N) (interval[a,b])))`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   397
  MP_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   398
   [ASM_SIMP_TAC[BOUNDED_UNION; COMPACT_IMP_BOUNDED; COMPACT_IMP_BOUNDED;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   399
                 COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   400
    ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   401
  DISCH_THEN(MP_TAC o SPEC `c:real^N` o MATCH_MP BOUNDED_SUBSET_BALL) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   402
  REWRITE_TAC[UNION_SUBSET] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   403
  DISCH_THEN(X_CHOOSE_THEN `B:real` STRIP_ASSUME_TAC) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   404
  MP_TAC(ISPECL [`p:real^M->real^N`; `a:real^M`; `b:real^M`]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   405
    RETRACTION_INJECTIVE_IMAGE_INTERVAL) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   406
  ASM_REWRITE_TAC[SUBSET; IN_UNIV] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   407
  DISCH_THEN(X_CHOOSE_THEN `r:real^N->real^N` MP_TAC) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   408
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   409
   (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   410
  REWRITE_TAC[FORALL_IN_IMAGE; IN_UNIV] THEN DISCH_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   411
  ABBREV_TAC `q = \z:real^N. if z IN path_component s c then r(z) else z` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   412
  SUBGOAL_THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   413
    `(q:real^N->real^N) continuous_on
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   414
     (closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)))`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   415
  MP_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   416
   [EXPAND_TAC "q" THEN MATCH_MP_TAC CONTINUOUS_ON_CASES THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   417
    REWRITE_TAC[CLOSED_CLOSURE; CONTINUOUS_ON_ID; GSYM OPEN_CLOSED] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   418
    REPEAT CONJ_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   419
     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   420
      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   421
                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   422
      ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   423
      ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   424
    X_GEN_TAC `z:real^N` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   425
    REWRITE_TAC[SET_RULE `~(z IN (s DIFF t) /\ z IN t)`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   426
    STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   427
    MP_TAC(ISPECL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   428
     [`path_component s (z:real^N)`; `path_component s (c:real^N)`]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   429
     OPEN_INTER_CLOSURE_EQ_EMPTY) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   430
    ASM_REWRITE_TAC[GSYM DISJOINT; PATH_COMPONENT_DISJOINT] THEN ANTS_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   431
     [MATCH_MP_TAC OPEN_PATH_COMPONENT THEN EXPAND_TAC "s" THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   432
      ASM_SIMP_TAC[GSYM CLOSED_OPEN; COMPACT_IMP_CLOSED;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   433
                   COMPACT_CONTINUOUS_IMAGE; COMPACT_INTERVAL];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   434
      REWRITE_TAC[DISJOINT; EXTENSION; IN_INTER; NOT_IN_EMPTY] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   435
      DISCH_THEN(MP_TAC o SPEC `z:real^N`) THEN ASM_REWRITE_TAC[] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   436
      GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [IN] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   437
      REWRITE_TAC[PATH_COMPONENT_REFL_EQ] THEN ASM SET_TAC[]];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   438
    ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   439
  SUBGOAL_THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   440
   `closure(path_component s c) UNION ((:real^N) DIFF (path_component s c)) =
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   441
    (:real^N)`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   442
  SUBST1_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   443
   [MATCH_MP_TAC(SET_RULE `s SUBSET t ==> t UNION (UNIV DIFF s) = UNIV`) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   444
    REWRITE_TAC[CLOSURE_SUBSET];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   445
    DISCH_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   446
  MP_TAC(ISPECL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   447
   [`(\x. &2 % c - x) o
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   448
     (\x. c + B / norm(x - c) % (x - c)) o (q:real^N->real^N)`;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   449
    `cball(c:real^N,B)`]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   450
    BROUWER) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   451
  REWRITE_TAC[NOT_IMP; GSYM CONJ_ASSOC; COMPACT_CBALL; CONVEX_CBALL] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   452
  ASM_SIMP_TAC[CBALL_EQ_EMPTY; REAL_LT_IMP_LE; REAL_NOT_LT] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   453
  SUBGOAL_THEN `!x. ~((q:real^N->real^N) x = c)` ASSUME_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   454
   [X_GEN_TAC `x:real^N` THEN EXPAND_TAC "q" THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   455
    REWRITE_TAC[NORM_EQ_0; VECTOR_SUB_EQ] THEN COND_CASES_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   456
    ASM SET_TAC[PATH_COMPONENT_REFL_EQ];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   457
    ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   458
  REPEAT CONJ_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   459
   [MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   460
    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   461
    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN CONJ_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   462
     [ASM_MESON_TAC[CONTINUOUS_ON_SUBSET; SUBSET_UNIV]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   463
    MATCH_MP_TAC CONTINUOUS_ON_ADD THEN REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   464
    MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   465
    SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   466
    REWRITE_TAC[o_DEF; real_div; LIFT_CMUL] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   467
    MATCH_MP_TAC CONTINUOUS_ON_CMUL THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   468
    MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_INV) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   469
    ASM_REWRITE_TAC[FORALL_IN_IMAGE; NORM_EQ_0; VECTOR_SUB_EQ] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   470
    SUBGOAL_THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   471
     `(\x:real^N. lift(norm(x - c))) = (lift o norm) o (\x. x - c)`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   472
    SUBST1_TAC THENL [REWRITE_TAC[o_DEF]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   473
    MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   474
    ASM_SIMP_TAC[CONTINUOUS_ON_SUB; CONTINUOUS_ON_ID; CONTINUOUS_ON_CONST;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   475
                 CONTINUOUS_ON_LIFT_NORM];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   476
    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; o_THM; dist] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   477
    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   478
    REWRITE_TAC[VECTOR_ARITH `c - (&2 % c - (c + x)) = x`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   479
    REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   480
    ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   481
    ASM_REAL_ARITH_TAC;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   482
    REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(c /\ b) <=> c ==> ~b`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   483
    REWRITE_TAC[IN_CBALL; o_THM; dist] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   484
    X_GEN_TAC `x:real^N` THEN DISCH_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   485
    REWRITE_TAC[VECTOR_ARITH `&2 % c - (c + x') = x <=> --x' = x - c`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   486
    ASM_CASES_TAC `(x:real^N) IN path_component s c` THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   487
     [MATCH_MP_TAC(NORM_ARITH `norm(y) < B /\ norm(x) = B ==> ~(--x = y)`) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   488
      REWRITE_TAC[NORM_MUL; REAL_ABS_DIV; REAL_ABS_NORM] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   489
      ASM_SIMP_TAC[REAL_DIV_RMUL; NORM_EQ_0; VECTOR_SUB_EQ] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   490
      ASM_SIMP_TAC[REAL_ARITH `&0 < B ==> abs B = B`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   491
      UNDISCH_TAC `path_component s c SUBSET ball(c:real^N,B)` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   492
      REWRITE_TAC[SUBSET; IN_BALL] THEN ASM_MESON_TAC[dist; NORM_SUB];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   493
      EXPAND_TAC "q" THEN REWRITE_TAC[] THEN ASM_REWRITE_TAC[] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   494
      REWRITE_TAC[VECTOR_ARITH `--(c % x) = x <=> (&1 + c) % x = vec 0`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   495
      ASM_REWRITE_TAC[DE_MORGAN_THM; VECTOR_SUB_EQ; VECTOR_MUL_EQ_0] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   496
      SUBGOAL_THEN `~(x:real^N = c)` ASSUME_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   497
       [ASM_MESON_TAC[PATH_COMPONENT_REFL; IN]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   498
      ASM_REWRITE_TAC[] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   499
      MATCH_MP_TAC(REAL_ARITH `&0 < x ==> ~(&1 + x = &0)`) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   500
      ASM_SIMP_TAC[REAL_LT_DIV; NORM_POS_LT; VECTOR_SUB_EQ]]]);;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   501
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   502
let PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL = prove
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   503
 (`!s:real^N->bool a b:real^M.
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   504
        2 <= dimindex(:N) /\ s homeomorphic interval[a,b]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   505
        ==> path_connected((:real^N) DIFF s)`,
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   506
  REPEAT STRIP_TAC THEN REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   507
  FIRST_ASSUM(MP_TAC o MATCH_MP
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   508
    UNBOUNDED_PATH_COMPONENTS_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   509
  ASM_REWRITE_TAC[SET_RULE `~(x IN s) <=> x IN (UNIV DIFF s)`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   510
  ABBREV_TAC `t = (:real^N) DIFF s` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   511
  DISCH_TAC THEN MAP_EVERY X_GEN_TAC [`x:real^N`; `y:real^N`] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   512
  STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP HOMEOMORPHIC_COMPACTNESS) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   513
  REWRITE_TAC[COMPACT_INTERVAL] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   514
  DISCH_THEN(MP_TAC o MATCH_MP COMPACT_IMP_BOUNDED) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   515
  REWRITE_TAC[BOUNDED_POS; LEFT_IMP_EXISTS_THM] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   516
  X_GEN_TAC `B:real` THEN STRIP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   517
  SUBGOAL_THEN `(?u:real^N. u IN path_component t x /\ B < norm(u)) /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   518
                (?v:real^N. v IN path_component t y /\ B < norm(v))`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   519
  STRIP_ASSUME_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   520
   [ASM_MESON_TAC[BOUNDED_POS; REAL_NOT_LE]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   521
  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `u:real^N` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   522
  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   523
  MATCH_MP_TAC PATH_COMPONENT_SYM THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   524
  MATCH_MP_TAC PATH_COMPONENT_TRANS THEN EXISTS_TAC `v:real^N` THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   525
  CONJ_TAC THENL [ASM_MESON_TAC[IN]; ALL_TAC] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   526
  MATCH_MP_TAC PATH_COMPONENT_OF_SUBSET THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   527
  EXISTS_TAC `(:real^N) DIFF cball(vec 0,B)` THEN CONJ_TAC THENL
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   528
   [EXPAND_TAC "t" THEN MATCH_MP_TAC(SET_RULE
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   529
     `s SUBSET t ==> (u DIFF t) SUBSET (u DIFF s)`) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   530
    ASM_REWRITE_TAC[SUBSET; IN_CBALL_0];
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   531
    MP_TAC(ISPEC `cball(vec 0:real^N,B)`
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   532
       PATH_CONNECTED_COMPLEMENT_BOUNDED_CONVEX) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   533
    ASM_REWRITE_TAC[BOUNDED_CBALL; CONVEX_CBALL] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   534
    REWRITE_TAC[PATH_CONNECTED_IFF_PATH_COMPONENT] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   535
    DISCH_THEN MATCH_MP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   536
    ASM_REWRITE_TAC[IN_DIFF; IN_UNIV; IN_CBALL_0; REAL_NOT_LE]]);;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   537
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   538
(* ------------------------------------------------------------------------- *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   539
(* In particular, apply all these to the special case of an arc.             *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   540
(* ------------------------------------------------------------------------- *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   541
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   542
let RETRACTION_ARC = prove
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   543
 (`!p. arc p
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   544
       ==> ?f. f continuous_on (:real^N) /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   545
               IMAGE f (:real^N) SUBSET path_image p /\
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   546
               (!x. x IN path_image p ==> f x = x)`,
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   547
  REWRITE_TAC[arc; path; path_image] THEN REPEAT STRIP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   548
  MATCH_MP_TAC RETRACTION_INJECTIVE_IMAGE_INTERVAL THEN
37489
44e42d392c6e Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents: 36593
diff changeset
   549
  ASM_REWRITE_TAC[INTERVAL_EQ_EMPTY_CART_1; DROP_VEC; REAL_NOT_LT; REAL_POS]);;
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   550
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   551
let PATH_CONNECTED_ARC_COMPLEMENT = prove
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   552
 (`!p. 2 <= dimindex(:N) /\ arc p
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   553
       ==> path_connected((:real^N) DIFF path_image p)`,
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   554
  REWRITE_TAC[arc; path] THEN REPEAT STRIP_TAC THEN SIMP_TAC[path_image] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   555
  MP_TAC(ISPECL [`path_image p:real^N->bool`; `vec 0:real^1`; `vec 1:real^1`]
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   556
    PATH_CONNECTED_COMPLEMENT_HOMEOMORPHIC_INTERVAL) THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   557
  ASM_REWRITE_TAC[path_image] THEN DISCH_THEN MATCH_MP_TAC THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   558
  ONCE_REWRITE_TAC[HOMEOMORPHIC_SYM] THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   559
  MATCH_MP_TAC HOMEOMORPHIC_COMPACT THEN
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   560
  EXISTS_TAC `p:real^1->real^N` THEN ASM_REWRITE_TAC[COMPACT_INTERVAL]);;
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   561
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   562
let CONNECTED_ARC_COMPLEMENT = prove
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   563
 (`!p. 2 <= dimindex(:N) /\ arc p
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   564
       ==> connected((:real^N) DIFF path_image p)`,
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   565
  SIMP_TAC[PATH_CONNECTED_ARC_COMPLEMENT; PATH_CONNECTED_IMP_CONNECTED]);; *)
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   566
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   567
end