src/HOL/Analysis/Fashoda_Theorem.thy
author paulson <lp15@cam.ac.uk>
Fri, 27 Apr 2018 12:38:30 +0100
changeset 68050 7eacc812ad1c
parent 68004 a8a20be7053a
child 68054 ebd179b82e20
permissions -rw-r--r--
minor typeclass generalisations and junk removal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
     1
(*  Author:     John Harrison
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
     2
    Author:     Robert Himmelmann, TU Muenchen (translation from HOL light)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
     3
*)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     4
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
     5
section \<open>Fashoda meet theorem\<close>
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     6
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
     7
theory Fashoda_Theorem
37674
f86de9c00c47 convert theorem path_connected_sphere to euclidean_space class
huffman
parents: 37489
diff changeset
     8
imports Brouwer_Fixpoint Path_Connected Cartesian_Euclidean_Space
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
     9
begin
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    10
67968
a5ad4c015d1c removed dots at the end of (sub)titles
nipkow
parents: 67673
diff changeset
    11
subsection \<open>Bijections between intervals\<close>
56273
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    12
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    13
definition interval_bij :: "'a \<times> 'a \<Rightarrow> 'a \<times> 'a \<Rightarrow> 'a \<Rightarrow> 'a::euclidean_space"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    14
  where "interval_bij =
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    15
    (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    16
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    17
lemma interval_bij_affine:
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    18
  "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) +
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    19
    (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63627
diff changeset
    20
  by (auto simp: sum.distrib[symmetric] scaleR_add_left[symmetric] interval_bij_def fun_eq_iff
b9a1486e79be setsum -> sum
nipkow
parents: 63627
diff changeset
    21
    field_simps inner_simps add_divide_distrib[symmetric] intro!: sum.cong)
56273
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    22
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    23
lemma continuous_interval_bij:
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    24
  fixes a b :: "'a::euclidean_space"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    25
  shows "continuous (at x) (interval_bij (a, b) (u, v))"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63627
diff changeset
    26
  by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros)
56273
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    27
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    28
lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    29
  apply(rule continuous_at_imp_continuous_on)
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    30
  apply (rule, rule continuous_interval_bij)
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    31
  done
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    32
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    33
lemma in_interval_interval_bij:
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    34
  fixes a b u v x :: "'a::euclidean_space"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    35
  assumes "x \<in> cbox a b"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    36
    and "cbox u v \<noteq> {}"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    37
  shows "interval_bij (a, b) (u, v) x \<in> cbox u v"
64267
b9a1486e79be setsum -> sum
nipkow
parents: 63627
diff changeset
    38
  apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong)
56273
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    39
  apply safe
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    40
proof -
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    41
  fix i :: 'a
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    42
  assume i: "i \<in> Basis"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    43
  have "cbox a b \<noteq> {}"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    44
    using assms by auto
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    45
  with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    46
    using assms(2) by (auto simp add: box_eq_empty)
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    47
  have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    48
    using assms(1)[unfolded mem_box] using i by auto
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    49
  have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
56571
f4635657d66f added divide_nonneg_nonneg and co; made it a simp rule
hoelzl
parents: 56371
diff changeset
    50
    using * x by auto
56273
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    51
  then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    52
    using * by auto
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    53
  have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    54
    apply (rule mult_right_mono)
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    55
    unfolding divide_le_eq_1
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    56
    using * x
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    57
    apply auto
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    58
    done
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    59
  then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    60
    using * by auto
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    61
qed
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    62
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    63
lemma interval_bij_bij:
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    64
  "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow>
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    65
    interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    66
  by (auto simp: interval_bij_def euclidean_eq_iff[where 'a='a])
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    67
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
    68
lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i"
56273
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    69
  shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x"
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    70
  using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis)
def3bbe6f2a5 cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)
hoelzl
parents: 56189
diff changeset
    71
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    72
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
    73
subsection \<open>Fashoda meet theorem\<close>
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    74
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    75
lemma infnorm_2:
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    76
  fixes x :: "real^2"
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61167
diff changeset
    77
  shows "infnorm x = max \<bar>x$1\<bar> \<bar>x$2\<bar>"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    78
  unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    79
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    80
lemma infnorm_eq_1_2:
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    81
  fixes x :: "real^2"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    82
  shows "infnorm x = 1 \<longleftrightarrow>
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61167
diff changeset
    83
    \<bar>x$1\<bar> \<le> 1 \<and> \<bar>x$2\<bar> \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)"
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    84
  unfolding infnorm_2 by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    85
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    86
lemma infnorm_eq_1_imp:
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    87
  fixes x :: "real^2"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    88
  assumes "infnorm x = 1"
61945
1135b8de26c3 more symbols;
wenzelm
parents: 61167
diff changeset
    89
  shows "\<bar>x$1\<bar> \<le> 1" and "\<bar>x$2\<bar> \<le> 1"
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    90
  using assms unfolding infnorm_eq_1_2 by auto
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
    91
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    92
lemma fashoda_unit:
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    93
  fixes f g :: "real \<Rightarrow> real^2"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
    94
  assumes "f ` {-1 .. 1} \<subseteq> cbox (-1) 1"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
    95
    and "g ` {-1 .. 1} \<subseteq> cbox (-1) 1"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
    96
    and "continuous_on {-1 .. 1} f"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
    97
    and "continuous_on {-1 .. 1} g"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    98
    and "f (- 1)$1 = - 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
    99
    and "f 1$1 = 1" "g (- 1) $2 = -1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   100
    and "g 1 $2 = 1"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   101
  shows "\<exists>s\<in>{-1 .. 1}. \<exists>t\<in>{-1 .. 1}. f s = g t"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   102
proof (rule ccontr)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   103
  assume "\<not> ?thesis"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   104
  note as = this[unfolded bex_simps,rule_format]
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   105
  define sqprojection
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   106
    where [abs_def]: "sqprojection z = (inverse (infnorm z)) *\<^sub>R z" for z :: "real^2"
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   107
  define negatex :: "real^2 \<Rightarrow> real^2"
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   108
    where "negatex x = (vector [-(x$1), x$2])" for x
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   109
  have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z"
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   110
    unfolding negatex_def infnorm_2 vector_2 by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   111
  have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   112
    unfolding sqprojection_def
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   113
    unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR]
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   114
    unfolding abs_inverse real_abs_infnorm
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   115
    apply (subst infnorm_eq_0[symmetric])
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   116
    apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   117
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   118
  let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   119
  have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` cbox (- 1) 1 = {-1 .. 1}"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   120
    apply (rule set_eqI)
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   121
    unfolding image_iff Bex_def mem_box_cart interval_cbox_cart
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   122
    apply rule
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   123
    defer
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   124
    apply (rule_tac x="vec x" in exI)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   125
    apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   126
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   127
  {
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   128
    fix x
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   129
    assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` (cbox (- 1) (1::real^2))"
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   130
    then obtain w :: "real^2" where w:
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   131
        "w \<in> cbox (- 1) 1"
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   132
        "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   133
      unfolding image_iff ..
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   134
    then have "x \<noteq> 0"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   135
      using as[of "w$1" "w$2"]
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   136
      unfolding mem_box_cart atLeastAtMost_iff
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   137
      by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   138
  } note x0 = this
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   139
  have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   140
    using UNIV_2 by auto
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 53628
diff changeset
   141
  have 1: "box (- 1) (1::real^2) \<noteq> {}"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   142
    unfolding interval_eq_empty_cart by auto
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   143
  have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56273
diff changeset
   144
    apply (intro continuous_intros continuous_on_component)
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   145
    unfolding *
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   146
    apply (rule assms)+
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   147
    apply (subst sqprojection_def)
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56273
diff changeset
   148
    apply (intro continuous_intros)
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   149
    apply (simp add: infnorm_eq_0 x0)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   150
    apply (rule linear_continuous_on)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   151
  proof -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   152
    show "bounded_linear negatex"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   153
      apply (rule bounded_linearI')
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   154
      unfolding vec_eq_iff
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   155
    proof (rule_tac[!] allI)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   156
      fix i :: 2
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   157
      fix x y :: "real^2"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   158
      fix c :: real
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   159
      show "negatex (x + y) $ i =
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   160
        (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   161
        apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   162
        apply (case_tac[!] "i\<noteq>1")
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   163
        prefer 3
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   164
        apply (drule_tac[1-2] 21)
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   165
        unfolding negatex_def
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   166
        apply (auto simp add:vector_2)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   167
        done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   168
    qed
44647
e4de7750cdeb modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents: 44531
diff changeset
   169
  qed
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   170
  have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   171
    unfolding subset_eq
61166
5976fe402824 renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents: 61165
diff changeset
   172
  proof (rule, goal_cases)
61165
8020249565fb tuned proofs;
wenzelm
parents: 60420
diff changeset
   173
    case (1 x)
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   174
    then obtain y :: "real^2" where y:
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   175
        "y \<in> cbox (- 1) 1"
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   176
        "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   177
      unfolding image_iff ..
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   178
    have "?F y \<noteq> 0"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   179
      apply (rule x0)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   180
      using y(1)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   181
      apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   182
      done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   183
    then have *: "infnorm (sqprojection (?F y)) = 1"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   184
      unfolding y o_def
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   185
      by - (rule lem2[rule_format])
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   186
    have "infnorm x = 1"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   187
      unfolding *[symmetric] y o_def
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   188
      by (rule lem1[rule_format])
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   189
    then show "x \<in> cbox (-1) 1"
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   190
      unfolding mem_box_cart interval_cbox_cart infnorm_2
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   191
      apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   192
      apply rule
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   193
    proof -
61165
8020249565fb tuned proofs;
wenzelm
parents: 60420
diff changeset
   194
      fix i
8020249565fb tuned proofs;
wenzelm
parents: 60420
diff changeset
   195
      assume "max \<bar>x $ 1\<bar> \<bar>x $ 2\<bar> = 1"
8020249565fb tuned proofs;
wenzelm
parents: 60420
diff changeset
   196
      then show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   197
        apply (cases "i = 1")
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   198
        defer
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   199
        apply (drule 21)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   200
        apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   201
        done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   202
    qed
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   203
  qed
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   204
  obtain x :: "real^2" where x:
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   205
      "x \<in> cbox (- 1) 1"
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   206
      "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x"
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   207
    apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"])
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   208
    apply (rule compact_cbox convex_box)+
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   209
    unfolding interior_cbox
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   210
    apply (rule 1 2 3)+
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   211
    apply blast
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   212
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   213
  have "?F x \<noteq> 0"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   214
    apply (rule x0)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   215
    using x(1)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   216
    apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   217
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   218
  then have *: "infnorm (sqprojection (?F x)) = 1"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   219
    unfolding o_def
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   220
    by (rule lem2[rule_format])
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   221
  have nx: "infnorm x = 1"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   222
    apply (subst x(2)[symmetric])
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   223
    unfolding *[symmetric] o_def
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   224
    apply (rule lem1[rule_format])
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   225
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   226
  have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   227
    and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   228
    apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   229
    apply (rule_tac[!] allI impI)+
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   230
  proof -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   231
    fix x :: "real^2"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   232
    fix i :: 2
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   233
    assume x: "x \<noteq> 0"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   234
    have "inverse (infnorm x) > 0"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   235
      using x[unfolded infnorm_pos_lt[symmetric]] by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   236
    then show "(0 < sqprojection x $ i) = (0 < x $ i)"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   237
      and "(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
   238
      unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   239
      unfolding zero_less_mult_iff mult_less_0_iff
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   240
      by (auto simp add: field_simps)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   241
  qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   242
  note lem3 = this[rule_format]
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   243
  have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}"
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   244
    using x(1) unfolding mem_box_cart by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   245
  then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   246
    unfolding right_minus_eq
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   247
    apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   248
    apply (rule as)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   249
    apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   250
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   251
  have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1"
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   252
    using nx unfolding infnorm_eq_1_2 by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   253
  then show False
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   254
  proof -
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   255
    fix P Q R S
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   256
    presume "P \<or> Q \<or> R \<or> S"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   257
      and "P \<Longrightarrow> False"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   258
      and "Q \<Longrightarrow> False"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   259
      and "R \<Longrightarrow> False"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   260
      and "S \<Longrightarrow> False"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   261
    then show False by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   262
  next
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   263
    assume as: "x$1 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   264
    then have *: "f (x $ 1) $ 1 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   265
      using assms(6) by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   266
    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
   267
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   268
      unfolding as negatex_def vector_2
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   269
      by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   270
    moreover
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   271
    from x1 have "g (x $ 2) \<in> cbox (-1) 1"
67982
7643b005b29a various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
   272
      using assms(2) by blast
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   273
    ultimately show False
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   274
      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
67982
7643b005b29a various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
   275
      using not_le by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   276
  next
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   277
    assume as: "x$1 = -1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   278
    then have *: "f (x $ 1) $ 1 = - 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   279
      using assms(5) by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   280
    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
   281
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]]
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   282
      unfolding as negatex_def vector_2
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   283
      by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   284
    moreover
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   285
    from x1 have "g (x $ 2) \<in> cbox (-1) 1"
67982
7643b005b29a various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
   286
      using assms(2) by blast
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   287
    ultimately show False
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   288
      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
67982
7643b005b29a various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
   289
      using not_le by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   290
  next
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   291
    assume as: "x$2 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   292
    then have *: "g (x $ 2) $ 2 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   293
      using assms(8) by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   294
    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
   295
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   296
      unfolding as negatex_def vector_2
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   297
      by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   298
    moreover
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   299
    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   300
      apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   301
      apply (rule assms(1)[unfolded subset_eq,rule_format])
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   302
      apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   303
      done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   304
    ultimately show False
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   305
      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   306
      apply (erule_tac x=2 in allE)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   307
      apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   308
      done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   309
  next
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   310
    assume as: "x$2 = -1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   311
    then have *: "g (x $ 2) $ 2 = - 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   312
      using assms(7) by auto
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   313
    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
   314
      using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]]
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   315
      unfolding as negatex_def vector_2
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   316
      by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   317
    moreover
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   318
    from x1 have "f (x $ 1) \<in> cbox (-1) 1"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   319
      apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   320
      apply (rule assms(1)[unfolded subset_eq,rule_format])
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   321
      apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   322
      done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   323
    ultimately show False
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   324
      unfolding lem3[OF nz] vector_component_simps * mem_box_cart
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   325
      apply (erule_tac x=2 in allE)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   326
      apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   327
      done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   328
  qed auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   329
qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   330
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   331
lemma fashoda_unit_path:
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   332
  fixes f g :: "real \<Rightarrow> real^2"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   333
  assumes "path f"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   334
    and "path g"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   335
    and "path_image f \<subseteq> cbox (-1) 1"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   336
    and "path_image g \<subseteq> cbox (-1) 1"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   337
    and "(pathstart f)$1 = -1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   338
    and "(pathfinish f)$1 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   339
    and "(pathstart g)$2 = -1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   340
    and "(pathfinish g)$2 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   341
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   342
proof -
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   343
  note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def]
63040
eb4ddd18d635 eliminated old 'def';
wenzelm
parents: 62397
diff changeset
   344
  define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   345
  have isc: "iscale ` {- 1..1} \<subseteq> {0..1}"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   346
    unfolding iscale_def by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   347
  have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   348
  proof (rule fashoda_unit)
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   349
    show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1"
56154
f0a927235162 more complete set of lemmas wrt. image and composition
haftmann
parents: 55675
diff changeset
   350
      using isc and assms(3-4) by (auto simp add: image_comp [symmetric])
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   351
    have *: "continuous_on {- 1..1} iscale"
56371
fb9ae0727548 extend continuous_intros; remove continuous_on_intros and isCont_intros
hoelzl
parents: 56273
diff changeset
   352
      unfolding iscale_def by (rule continuous_intros)+
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   353
    show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)"
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   354
      apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   355
      apply (rule_tac[!] continuous_on_compose[OF *])
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   356
      apply (rule_tac[!] continuous_on_subset[OF _ isc])
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   357
      apply (rule assms)+
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   358
      done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   359
    have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   360
      unfolding vec_eq_iff by auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   361
    show "(f \<circ> iscale) (- 1) $ 1 = - 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   362
      and "(f \<circ> iscale) 1 $ 1 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   363
      and "(g \<circ> iscale) (- 1) $ 2 = -1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   364
      and "(g \<circ> iscale) 1 $ 2 = 1"
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   365
      unfolding o_def iscale_def
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   366
      using assms
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   367
      by (auto simp add: *)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   368
  qed
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   369
  then obtain s t where st:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   370
      "s \<in> {- 1..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   371
      "t \<in> {- 1..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   372
      "(f \<circ> iscale) s = (g \<circ> iscale) t"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   373
    by auto
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   374
  show thesis
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   375
    apply (rule_tac z = "f (iscale s)" in that)
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   376
    using st
53572
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   377
    unfolding o_def path_image_def image_iff
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   378
    apply -
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   379
    apply (rule_tac x="iscale s" in bexI)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   380
    prefer 3
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   381
    apply (rule_tac x="iscale t" in bexI)
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   382
    using isc[unfolded subset_eq, rule_format]
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   383
    apply auto
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   384
    done
e7b77b217491 tuned proofs;
wenzelm
parents: 51475
diff changeset
   385
qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   386
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   387
lemma fashoda:
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   388
  fixes b :: "real^2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   389
  assumes "path f"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   390
    and "path g"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   391
    and "path_image f \<subseteq> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   392
    and "path_image g \<subseteq> cbox a b"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   393
    and "(pathstart f)$1 = a$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   394
    and "(pathfinish f)$1 = b$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   395
    and "(pathstart g)$2 = a$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   396
    and "(pathfinish g)$2 = b$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   397
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   398
proof -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   399
  fix P Q S
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   400
  presume "P \<or> Q \<or> S" "P \<Longrightarrow> thesis" and "Q \<Longrightarrow> thesis" and "S \<Longrightarrow> thesis"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   401
  then show thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   402
    by auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   403
next
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   404
  have "cbox a b \<noteq> {}"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 53628
diff changeset
   405
    using assms(3) using path_image_nonempty[of f] by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   406
  then have "a \<le> b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   407
    unfolding interval_eq_empty_cart less_eq_vec_def by (auto simp add: not_less)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   408
  then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   409
    unfolding less_eq_vec_def forall_2 by auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   410
next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   411
  assume as: "a$1 = b$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   412
  have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   413
    apply (rule connected_ivt_component_cart)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   414
    apply (rule connected_path_image assms)+
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   415
    apply (rule pathstart_in_path_image)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   416
    apply (rule pathfinish_in_path_image)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   417
    unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"]
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   418
    unfolding pathstart_def
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   419
    apply (auto simp add: less_eq_vec_def mem_box_cart)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   420
    done
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   421
  then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" ..
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   422
  have "z \<in> cbox a b"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   423
    using z(1) assms(4)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   424
    unfolding path_image_def
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   425
    by blast
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   426
  then have "z = f 0"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   427
    unfolding vec_eq_iff forall_2
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   428
    unfolding z(2) pathstart_def
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   429
    using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1]
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   430
    unfolding mem_box_cart
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   431
    apply (erule_tac x=1 in allE)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   432
    using as
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   433
    apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   434
    done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   435
  then show thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   436
    apply -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   437
    apply (rule that[OF _ z(1)])
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   438
    unfolding path_image_def
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   439
    apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   440
    done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   441
next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   442
  assume as: "a$2 = b$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   443
  have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   444
    apply (rule connected_ivt_component_cart)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   445
    apply (rule connected_path_image assms)+
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   446
    apply (rule pathstart_in_path_image)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   447
    apply (rule pathfinish_in_path_image)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   448
    unfolding assms
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   449
    using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"]
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   450
    unfolding pathstart_def
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   451
    apply (auto simp add: less_eq_vec_def mem_box_cart)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   452
    done
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   453
  then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" ..
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   454
  have "z \<in> cbox a b"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   455
    using z(1) assms(3)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   456
    unfolding path_image_def
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   457
    by blast
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   458
  then have "z = g 0"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   459
    unfolding vec_eq_iff forall_2
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   460
    unfolding z(2) pathstart_def
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   461
    using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2]
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   462
    unfolding mem_box_cart
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   463
    apply (erule_tac x=2 in allE)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   464
    using as
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   465
    apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   466
    done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   467
  then show thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   468
    apply -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   469
    apply (rule that[OF z(1)])
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   470
    unfolding path_image_def
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   471
    apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   472
    done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   473
next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   474
  assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   475
  have int_nem: "cbox (-1) (1::real^2) \<noteq> {}"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   476
    unfolding interval_eq_empty_cart by auto
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   477
  obtain z :: "real^2" where z:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   478
      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   479
      "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   480
    apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"])
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   481
    unfolding path_def path_image_def pathstart_def pathfinish_def
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   482
    apply (rule_tac[1-2] continuous_on_compose)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   483
    apply (rule assms[unfolded path_def] continuous_on_interval_bij)+
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   484
    unfolding subset_eq
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   485
    apply(rule_tac[1-2] ballI)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   486
  proof -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   487
    fix x
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   488
    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}"
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   489
    then obtain y where y:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   490
        "y \<in> {0..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   491
        "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   492
      unfolding image_iff ..
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   493
    show "x \<in> cbox (- 1) 1"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   494
      unfolding y o_def
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   495
      apply (rule in_interval_interval_bij)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   496
      using y(1)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   497
      using assms(3)[unfolded path_image_def subset_eq] int_nem
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   498
      apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   499
      done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   500
  next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   501
    fix x
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   502
    assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}"
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   503
    then obtain y where y:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   504
        "y \<in> {0..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   505
        "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   506
      unfolding image_iff ..
58410
6d46ad54a2ab explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
haftmann
parents: 57418
diff changeset
   507
    show "x \<in> cbox (- 1) 1"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   508
      unfolding y o_def
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   509
      apply (rule in_interval_interval_bij)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   510
      using y(1)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   511
      using assms(4)[unfolded path_image_def subset_eq] int_nem
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   512
      apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   513
      done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   514
  next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   515
    show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   516
      and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   517
      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   518
      and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   519
      using assms as
67982
7643b005b29a various new results on measures, integrals, etc., and some simplified proofs
paulson <lp15@cam.ac.uk>
parents: 67968
diff changeset
   520
      by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
50526
899c9c4e4a4c Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents: 44647
diff changeset
   521
         (simp_all add: inner_axis)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   522
  qed
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   523
  from z(1) obtain zf where zf:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   524
      "zf \<in> {0..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   525
      "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   526
    unfolding image_iff ..
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   527
  from z(2) obtain zg where zg:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   528
      "zg \<in> {0..1}"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   529
      "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   530
    unfolding image_iff ..
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   531
  have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   532
    unfolding forall_2
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   533
    using as
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   534
    by auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   535
  show thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   536
    apply (rule_tac z="interval_bij (- 1,1) (a,b) z" in that)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   537
    apply (subst zf)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   538
    defer
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   539
    apply (subst zg)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   540
    unfolding o_def interval_bij_bij_cart[OF *] path_image_def
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   541
    using zf(1) zg(1)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   542
    apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   543
    done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   544
qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   545
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   546
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
   547
subsection \<open>Some slightly ad hoc lemmas I use below\<close>
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   548
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   549
lemma segment_vertical:
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   550
  fixes a :: "real^2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   551
  assumes "a$1 = b$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   552
  shows "x \<in> closed_segment a b \<longleftrightarrow>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   553
    x$1 = a$1 \<and> x$1 = b$1 \<and> (a$2 \<le> x$2 \<and> x$2 \<le> b$2 \<or> b$2 \<le> x$2 \<and> x$2 \<le> a$2)"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   554
  (is "_ = ?R")
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   555
proof -
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   556
  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"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   557
  {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   558
    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   559
    then show ?thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   560
      unfolding closed_segment_def mem_Collect_eq
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   561
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   562
      by blast
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   563
  }
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   564
  {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   565
    assume ?L
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   566
    then obtain u where u:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   567
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   568
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   569
        "0 \<le> u"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   570
        "u \<le> 1"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   571
      by blast
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   572
    { fix b a
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   573
      assume "b + u * a > a + u * b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   574
      then have "(1 - u) * b > (1 - u) * a"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   575
        by (auto simp add:field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   576
      then have "b \<ge> a"
59555
05573e5504a9 eliminated fact duplicates
haftmann
parents: 58877
diff changeset
   577
        apply (drule_tac mult_left_less_imp_less)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   578
        using u
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   579
        apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   580
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   581
      then have "u * a \<le> u * b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   582
        apply -
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   583
        apply (rule mult_left_mono[OF _ u(3)])
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   584
        using u(3-4)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   585
        apply (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   586
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   587
    } note * = this
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   588
    {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   589
      fix a b
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   590
      assume "u * b > u * a"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   591
      then have "(1 - u) * a \<le> (1 - u) * b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   592
        apply -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   593
        apply (rule mult_left_mono)
59555
05573e5504a9 eliminated fact duplicates
haftmann
parents: 58877
diff changeset
   594
        apply (drule mult_left_less_imp_less)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   595
        using u
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   596
        apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   597
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   598
      then have "a + u * b \<le> b + u * a"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   599
        by (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   600
    } note ** = this
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   601
    then show ?R
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   602
      unfolding u assms
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   603
      using u
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   604
      by (auto simp add:field_simps not_le intro: * **)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   605
  }
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   606
  {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   607
    assume ?R
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   608
    then show ?L
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   609
    proof (cases "x$2 = b$2")
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   610
      case True
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   611
      then show ?L
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   612
        apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   613
        unfolding assms True
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
   614
        using \<open>?R\<close>
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   615
        apply (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   616
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   617
    next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   618
      case False
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   619
      then show ?L
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   620
        apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   621
        unfolding assms
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
   622
        using \<open>?R\<close>
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   623
        apply (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   624
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   625
    qed
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   626
  }
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   627
qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   628
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   629
lemma segment_horizontal:
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   630
  fixes a :: "real^2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   631
  assumes "a$2 = b$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   632
  shows "x \<in> closed_segment a b \<longleftrightarrow>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   633
    x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   634
  (is "_ = ?R")
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   635
proof -
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   636
  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"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   637
  {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   638
    presume "?L \<Longrightarrow> ?R" and "?R \<Longrightarrow> ?L"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   639
    then show ?thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   640
      unfolding closed_segment_def mem_Collect_eq
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   641
      unfolding vec_eq_iff forall_2 scalar_mult_eq_scaleR[symmetric] vector_component_simps
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   642
      by blast
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   643
  }
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   644
  {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   645
    assume ?L
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   646
    then obtain u where u:
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   647
        "x $ 1 = (1 - u) * a $ 1 + u * b $ 1"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   648
        "x $ 2 = (1 - u) * a $ 2 + u * b $ 2"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   649
        "0 \<le> u"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   650
        "u \<le> 1"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   651
      by blast
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   652
    {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   653
      fix b a
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   654
      assume "b + u * a > a + u * b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   655
      then have "(1 - u) * b > (1 - u) * a"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   656
        by (auto simp add: field_simps)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   657
      then have "b \<ge> a"
59555
05573e5504a9 eliminated fact duplicates
haftmann
parents: 58877
diff changeset
   658
        apply (drule_tac mult_left_less_imp_less)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   659
        using u
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   660
        apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   661
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   662
      then have "u * a \<le> u * b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   663
        apply -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   664
        apply (rule mult_left_mono[OF _ u(3)])
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   665
        using u(3-4)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   666
        apply (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   667
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   668
    } note * = this
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   669
    {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   670
      fix a b
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   671
      assume "u * b > u * a"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   672
      then have "(1 - u) * a \<le> (1 - u) * b"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   673
        apply -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   674
        apply (rule mult_left_mono)
59555
05573e5504a9 eliminated fact duplicates
haftmann
parents: 58877
diff changeset
   675
        apply (drule mult_left_less_imp_less)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   676
        using u
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   677
        apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   678
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   679
      then have "a + u * b \<le> b + u * a"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   680
        by (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   681
    } note ** = this
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   682
    then show ?R
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   683
      unfolding u assms
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   684
      using u
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   685
      by (auto simp add: field_simps not_le intro: * **)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   686
  }
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   687
  {
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   688
    assume ?R
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   689
    then show ?L
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   690
    proof (cases "x$1 = b$1")
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   691
      case True
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   692
      then show ?L
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   693
        apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   694
        unfolding assms True
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
   695
        using \<open>?R\<close>
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   696
        apply (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   697
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   698
    next
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   699
      case False
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   700
      then show ?L
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   701
        apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   702
        unfolding assms
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
   703
        using \<open>?R\<close>
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   704
        apply (auto simp add: field_simps)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   705
        done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   706
    qed
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   707
  }
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   708
qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   709
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   710
60420
884f54e01427 isabelle update_cartouches;
wenzelm
parents: 59555
diff changeset
   711
subsection \<open>Useful Fashoda corollary pointed out to me by Tom Hales\<close>
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   712
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   713
lemma fashoda_interlace:
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   714
  fixes a :: "real^2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   715
  assumes "path f"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   716
    and "path g"
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   717
    and "path_image f \<subseteq> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   718
    and "path_image g \<subseteq> cbox a b"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   719
    and "(pathstart f)$2 = a$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   720
    and "(pathfinish f)$2 = a$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   721
    and "(pathstart g)$2 = a$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   722
    and "(pathfinish g)$2 = a$2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   723
    and "(pathstart f)$1 < (pathstart g)$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   724
    and "(pathstart g)$1 < (pathfinish f)$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   725
    and "(pathfinish f)$1 < (pathfinish g)$1"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   726
  obtains z where "z \<in> path_image f" and "z \<in> path_image g"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   727
proof -
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   728
  have "cbox a b \<noteq> {}"
54775
2d3df8633dad prefer box over greaterThanLessThan on euclidean_space
immler
parents: 53628
diff changeset
   729
    using path_image_nonempty[of f] 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
   730
  note ab=this[unfolded interval_eq_empty_cart not_ex forall_2 not_less]
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   731
  have "pathstart f \<in> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   732
    and "pathfinish f \<in> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   733
    and "pathstart g \<in> cbox a b"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   734
    and "pathfinish g \<in> cbox a b"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   735
    using pathstart_in_path_image pathfinish_in_path_image
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   736
    using assms(3-4)
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   737
    by auto
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   738
  note startfin = this[unfolded mem_box_cart forall_2]
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   739
  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
   740
     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
   741
     linepath(pathfinish f)(vector[(pathfinish f)$1,a$2 - 2]) +++
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   742
     linepath(vector[(pathfinish f)$1,a$2 - 2])(vector[b$1 + 2,a$2 - 2])"
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   743
  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
   744
     linepath(pathfinish g)(vector[(pathfinish g)$1,a$2 - 1]) +++
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   745
     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
   746
     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
   747
  let ?a = "vector[a$1 - 2, a$2 - 3]"
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   748
  let ?b = "vector[b$1 + 2, b$2 + 3]"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   749
  have P1P2: "path_image ?P1 = path_image (linepath (vector[a$1 - 2, a$2 - 2]) (vector[(pathstart f)$1,a$2 - 2])) \<union>
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   750
      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
   751
      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
   752
      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
   753
    "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
   754
      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
   755
      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
   756
      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
   757
      by(auto simp add: path_image_join path_linepath)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   758
  have abab: "cbox a b \<subseteq> cbox ?a ?b"
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   759
    unfolding interval_cbox_cart[symmetric]
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   760
    by (auto simp add:less_eq_vec_def forall_2 vector_2)
55675
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   761
  obtain z where
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   762
    "z \<in> path_image
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   763
          (linepath (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   764
           linepath (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f) +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   765
           f +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   766
           linepath (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   767
           linepath (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]))"
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   768
    "z \<in> path_image
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   769
          (linepath (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g) +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   770
           g +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   771
           linepath (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1]) +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   772
           linepath (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1]) +++
ccbf1722ae32 tuned proofs;
wenzelm
parents: 54775
diff changeset
   773
           linepath (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]))"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   774
    apply (rule fashoda[of ?P1 ?P2 ?a ?b])
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   775
    unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   776
  proof -
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   777
    show "path ?P1" and "path ?P2"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   778
      using assms by auto
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   779
    have "path_image ?P1 \<subseteq> cbox ?a ?b"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   780
      unfolding P1P2 path_image_linepath
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   781
      apply (rule Un_least)+
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   782
      defer 3
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   783
      apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   784
      unfolding mem_box_cart forall_2 vector_2
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   785
      using ab startfin abab assms(3)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   786
      using assms(9-)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   787
      unfolding assms
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   788
      apply (auto simp add: field_simps box_def)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   789
      done
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   790
    then show "path_image ?P1 \<subseteq> cbox ?a ?b" .
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   791
    have "path_image ?P2 \<subseteq> cbox ?a ?b"
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   792
      unfolding P1P2 path_image_linepath
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   793
      apply (rule Un_least)+
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   794
      defer 2
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   795
      apply (rule_tac[1-4] convex_box(1)[unfolded convex_contains_segment,rule_format])
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   796
      unfolding mem_box_cart forall_2 vector_2
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   797
      using ab startfin abab assms(4)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   798
      using assms(9-)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   799
      unfolding assms
56189
c4daa97ac57a removed dependencies on theory Ordered_Euclidean_Space
immler
parents: 56188
diff changeset
   800
      apply (auto simp add: field_simps box_def)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   801
      done
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   802
    then show "path_image ?P2 \<subseteq> cbox ?a ?b" .
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   803
    show "a $ 1 - 2 = a $ 1 - 2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   804
      and "b $ 1 + 2 = b $ 1 + 2"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   805
      and "pathstart g $ 2 - 3 = a $ 2 - 3"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   806
      and "b $ 2 + 3 = b $ 2 + 3"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   807
      by (auto simp add: assms)
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   808
  qed
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   809
  note z=this[unfolded P1P2 path_image_linepath]
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   810
  show thesis
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   811
    apply (rule that[of z])
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   812
  proof -
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   813
    have "(z \<in> closed_segment (vector [a $ 1 - 2, a $ 2 - 2]) (vector [pathstart f $ 1, a $ 2 - 2]) \<or>
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   814
      z \<in> closed_segment (vector [pathstart f $ 1, a $ 2 - 2]) (pathstart f)) \<or>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   815
      z \<in> closed_segment (pathfinish f) (vector [pathfinish f $ 1, a $ 2 - 2]) \<or>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   816
      z \<in> closed_segment (vector [pathfinish f $ 1, a $ 2 - 2]) (vector [b $ 1 + 2, a $ 2 - 2]) \<Longrightarrow>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   817
    (((z \<in> closed_segment (vector [pathstart g $ 1, pathstart g $ 2 - 3]) (pathstart g)) \<or>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   818
      z \<in> closed_segment (pathfinish g) (vector [pathfinish g $ 1, a $ 2 - 1])) \<or>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   819
      z \<in> closed_segment (vector [pathfinish g $ 1, a $ 2 - 1]) (vector [b $ 1 + 1, a $ 2 - 1])) \<or>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   820
      z \<in> closed_segment (vector [b $ 1 + 1, a $ 2 - 1]) (vector [b $ 1 + 1, b $ 2 + 3]) \<Longrightarrow> False"
61166
5976fe402824 renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents: 61165
diff changeset
   821
    proof (simp only: segment_vertical segment_horizontal vector_2, goal_cases)
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   822
      case prems: 1
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   823
      have "pathfinish f \<in> cbox a b"
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   824
        using assms(3) pathfinish_in_path_image[of f] by auto
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   825
      then have "1 + b $ 1 \<le> pathfinish f $ 1 \<Longrightarrow> False"
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   826
        unfolding mem_box_cart forall_2 by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   827
      then have "z$1 \<noteq> pathfinish f$1"
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   828
        using prems(2)
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   829
        using assms ab
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   830
        by (auto simp add: field_simps)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   831
      moreover have "pathstart f \<in> cbox a b"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   832
        using assms(3) pathstart_in_path_image[of f]
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   833
        by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   834
      then have "1 + b $ 1 \<le> pathstart f $ 1 \<Longrightarrow> False"
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   835
        unfolding mem_box_cart forall_2
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   836
        by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   837
      then have "z$1 \<noteq> pathstart f$1"
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   838
        using prems(2) using assms ab
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   839
        by (auto simp add: field_simps)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   840
      ultimately have *: "z$2 = a$2 - 2"
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   841
        using prems(1)
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   842
        by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   843
      have "z$1 \<noteq> pathfinish g$1"
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   844
        using prems(2)
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   845
        using assms ab
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   846
        by (auto simp add: field_simps *)
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   847
      moreover have "pathstart g \<in> cbox a b"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   848
        using assms(4) pathstart_in_path_image[of g]
63594
bd218a9320b5 HOL-Multivariate_Analysis: rename theories for more descriptive names
hoelzl
parents: 63040
diff changeset
   849
        by auto
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   850
      note this[unfolded mem_box_cart forall_2]
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   851
      then have "z$1 \<noteq> pathstart g$1"
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   852
        using prems(1)
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   853
        using assms ab
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   854
        by (auto simp add: field_simps *)
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   855
      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"
61167
34f782641caa tuned proofs;
wenzelm
parents: 61166
diff changeset
   856
        using prems(2)
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   857
        unfolding * assms
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   858
        by (auto simp add: field_simps)
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   859
      then show False
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   860
        unfolding * using ab by auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   861
    qed
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   862
    then have "z \<in> path_image f \<or> z \<in> path_image g"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   863
      using z unfolding Un_iff by blast
56188
0268784f60da use cbox to relax class constraints
immler
parents: 56154
diff changeset
   864
    then have z': "z \<in> cbox a b"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   865
      using assms(3-4)
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   866
      by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   867
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart f $ 1 \<or> z $ 1 = pathfinish f $ 1) \<Longrightarrow>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   868
      z = pathstart f \<or> z = pathfinish f"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   869
      unfolding vec_eq_iff forall_2 assms
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   870
      by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   871
    with z' show "z \<in> path_image f"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   872
      using z(1)
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   873
      unfolding Un_iff mem_box_cart forall_2
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   874
      apply -
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   875
      apply (simp only: segment_vertical segment_horizontal vector_2)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   876
      unfolding assms
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   877
      apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   878
      done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   879
    have "a $ 2 = z $ 2 \<Longrightarrow> (z $ 1 = pathstart g $ 1 \<or> z $ 1 = pathfinish g $ 1) \<Longrightarrow>
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   880
      z = pathstart g \<or> z = pathfinish g"
53628
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   881
      unfolding vec_eq_iff forall_2 assms
15405540288e tuned proofs;
wenzelm
parents: 53627
diff changeset
   882
      by auto
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   883
    with z' show "z \<in> path_image g"
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   884
      using z(2)
67673
c8caefb20564 lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents: 64267
diff changeset
   885
      unfolding Un_iff mem_box_cart forall_2
53627
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   886
      apply (simp only: segment_vertical segment_horizontal vector_2)
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   887
      unfolding assms
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   888
      apply auto
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   889
      done
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   890
  qed
f3fd9168911c tuned proofs;
wenzelm
parents: 53572
diff changeset
   891
qed
36432
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   892
1ad1cfeaec2d move proof of Fashoda meet theorem into separate file
huffman
parents:
diff changeset
   893
end