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