author | blanchet |
Wed, 12 Feb 2014 08:35:56 +0100 | |
changeset 55413 | a8e96847523c |
parent 54781 | fe462aa28c3d |
child 56166 | 9a241bc276cd |
permissions | -rw-r--r-- |
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
1 |
theory Ordered_Euclidean_Space |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
2 |
imports |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
3 |
Topology_Euclidean_Space |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
4 |
"~~/src/HOL/Library/Product_Order" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
5 |
begin |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
6 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
7 |
subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
8 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
9 |
class ordered_euclidean_space = ord + inf + sup + abs + Inf + Sup + euclidean_space + |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
10 |
assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i\<in>Basis. x \<bullet> i \<le> y \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
11 |
assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
12 |
assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
13 |
assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
14 |
assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
15 |
assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
16 |
assumes eucl_abs: "abs x = (\<Sum>i\<in>Basis. abs (x \<bullet> i) *\<^sub>R i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
17 |
begin |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
18 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
19 |
subclass order |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
20 |
by default |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
21 |
(auto simp: eucl_le eucl_less_le_not_le intro!: euclidean_eqI antisym intro: order.trans) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
22 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
23 |
subclass ordered_ab_group_add_abs |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
24 |
by default (auto simp: eucl_le inner_add_left eucl_abs abs_leI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
25 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
26 |
subclass ordered_real_vector |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
27 |
by default (auto simp: eucl_le intro!: mult_left_mono mult_right_mono) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
28 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
29 |
subclass lattice |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
30 |
by default (auto simp: eucl_inf eucl_sup eucl_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
31 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
32 |
subclass distrib_lattice |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
33 |
by default (auto simp: eucl_inf eucl_sup sup_inf_distrib1 intro!: euclidean_eqI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
34 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
35 |
subclass conditionally_complete_lattice |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
36 |
proof |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
37 |
fix z::'a and X::"'a set" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
38 |
assume "X \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
39 |
hence "\<And>i. (\<lambda>x. x \<bullet> i) ` X \<noteq> {}" by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
40 |
thus "(\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" "(\<And>x. x \<in> X \<Longrightarrow> x \<le> z) \<Longrightarrow> Sup X \<le> z" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
41 |
by (auto simp: eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
42 |
intro!: cInf_greatest cSup_least) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
43 |
qed (force intro!: cInf_lower cSup_upper |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
44 |
simp: bdd_below_def bdd_above_def preorder_class.bdd_below_def preorder_class.bdd_above_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
45 |
eucl_Inf eucl_Sup eucl_le Inf_class.INF_def Sup_class.SUP_def)+ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
46 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
47 |
lemma inner_Basis_inf_left: "i \<in> Basis \<Longrightarrow> inf x y \<bullet> i = inf (x \<bullet> i) (y \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
48 |
and inner_Basis_sup_left: "i \<in> Basis \<Longrightarrow> sup x y \<bullet> i = sup (x \<bullet> i) (y \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
49 |
by (simp_all add: eucl_inf eucl_sup inner_setsum_left inner_Basis if_distrib setsum_delta |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
50 |
cong: if_cong) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
51 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
52 |
lemma inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
53 |
and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
54 |
by (simp_all add: INF_def SUP_def eucl_Sup eucl_Inf) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
55 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
56 |
lemma abs_inner: "i \<in> Basis \<Longrightarrow> abs x \<bullet> i = abs (x \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
57 |
by (auto simp: eucl_abs) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
58 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
59 |
lemma |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
60 |
abs_scaleR: "\<bar>a *\<^sub>R b\<bar> = \<bar>a\<bar> *\<^sub>R \<bar>b\<bar>" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
61 |
by (auto simp: eucl_abs abs_mult intro!: euclidean_eqI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
62 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
63 |
lemma interval_inner_leI: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
64 |
assumes "x \<in> {a .. b}" "0 \<le> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
65 |
shows "a\<bullet>i \<le> x\<bullet>i" "x\<bullet>i \<le> b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
66 |
using assms |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
67 |
unfolding euclidean_inner[of a i] euclidean_inner[of x i] euclidean_inner[of b i] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
68 |
by (auto intro!: setsum_mono mult_right_mono simp: eucl_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
69 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
70 |
lemma inner_nonneg_nonneg: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
71 |
shows "0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 \<le> a \<bullet> b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
72 |
using interval_inner_leI[of a 0 a b] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
73 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
74 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
75 |
lemma inner_Basis_mono: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
76 |
shows "a \<le> b \<Longrightarrow> c \<in> Basis \<Longrightarrow> a \<bullet> c \<le> b \<bullet> c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
77 |
by (simp add: eucl_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
78 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
79 |
lemma Basis_nonneg[intro, simp]: "i \<in> Basis \<Longrightarrow> 0 \<le> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
80 |
by (auto simp: eucl_le inner_Basis) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
81 |
|
54781 | 82 |
lemma Sup_eq_maximum_componentwise: |
83 |
fixes s::"'a set" |
|
84 |
assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b" |
|
85 |
assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> x \<bullet> b \<le> X \<bullet> b" |
|
86 |
assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s" |
|
87 |
shows "Sup s = X" |
|
88 |
using assms |
|
89 |
unfolding eucl_Sup euclidean_representation_setsum |
|
90 |
by (auto simp: Sup_class.SUP_def intro!: conditionally_complete_lattice_class.cSup_eq_maximum) |
|
91 |
||
92 |
lemma Inf_eq_minimum_componentwise: |
|
93 |
assumes i: "\<And>b. b \<in> Basis \<Longrightarrow> X \<bullet> b = i b \<bullet> b" |
|
94 |
assumes sup: "\<And>b x. b \<in> Basis \<Longrightarrow> x \<in> s \<Longrightarrow> X \<bullet> b \<le> x \<bullet> b" |
|
95 |
assumes i_s: "\<And>b. b \<in> Basis \<Longrightarrow> (i b \<bullet> b) \<in> (\<lambda>x. x \<bullet> b) ` s" |
|
96 |
shows "Inf s = X" |
|
97 |
using assms |
|
98 |
unfolding eucl_Inf euclidean_representation_setsum |
|
99 |
by (auto simp: Inf_class.INF_def intro!: conditionally_complete_lattice_class.cInf_eq_minimum) |
|
100 |
||
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
101 |
end |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
102 |
|
54781 | 103 |
lemma |
104 |
compact_attains_Inf_componentwise: |
|
105 |
fixes b::"'a::ordered_euclidean_space" |
|
106 |
assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X" |
|
107 |
obtains x where "x \<in> X" "x \<bullet> b = Inf X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
|
108 |
proof atomize_elim |
|
109 |
let ?proj = "(\<lambda>x. x \<bullet> b) ` X" |
|
110 |
from assms have "compact ?proj" "?proj \<noteq> {}" |
|
111 |
by (auto intro!: compact_continuous_image continuous_on_intros) |
|
112 |
from compact_attains_inf[OF this] |
|
113 |
obtain s x |
|
114 |
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> s \<le> t" |
|
115 |
and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> x \<bullet> b \<le> y \<bullet> b" |
|
116 |
by auto |
|
117 |
hence "Inf ?proj = x \<bullet> b" |
|
118 |
by (auto intro!: conditionally_complete_lattice_class.cInf_eq_minimum) |
|
119 |
hence "x \<bullet> b = Inf X \<bullet> b" |
|
120 |
by (auto simp: eucl_Inf Inf_class.INF_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` |
|
121 |
setsum_delta cong: if_cong) |
|
122 |
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Inf X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> x \<bullet> b \<le> y \<bullet> b)" by blast |
|
123 |
qed |
|
124 |
||
125 |
lemma |
|
126 |
compact_attains_Sup_componentwise: |
|
127 |
fixes b::"'a::ordered_euclidean_space" |
|
128 |
assumes "b \<in> Basis" assumes "X \<noteq> {}" "compact X" |
|
129 |
obtains x where "x \<in> X" "x \<bullet> b = Sup X \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
|
130 |
proof atomize_elim |
|
131 |
let ?proj = "(\<lambda>x. x \<bullet> b) ` X" |
|
132 |
from assms have "compact ?proj" "?proj \<noteq> {}" |
|
133 |
by (auto intro!: compact_continuous_image continuous_on_intros) |
|
134 |
from compact_attains_sup[OF this] |
|
135 |
obtain s x |
|
136 |
where s: "s\<in>(\<lambda>x. x \<bullet> b) ` X" "\<And>t. t\<in>(\<lambda>x. x \<bullet> b) ` X \<Longrightarrow> t \<le> s" |
|
137 |
and x: "x \<in> X" "s = x \<bullet> b" "\<And>y. y \<in> X \<Longrightarrow> y \<bullet> b \<le> x \<bullet> b" |
|
138 |
by auto |
|
139 |
hence "Sup ?proj = x \<bullet> b" |
|
140 |
by (auto intro!: cSup_eq_maximum) |
|
141 |
hence "x \<bullet> b = Sup X \<bullet> b" |
|
142 |
by (auto simp: eucl_Sup[where 'a='a] SUP_def inner_setsum_left inner_Basis if_distrib `b \<in> Basis` |
|
143 |
setsum_delta cong: if_cong) |
|
144 |
with x show "\<exists>x. x \<in> X \<and> x \<bullet> b = Sup X \<bullet> b \<and> (\<forall>y. y \<in> X \<longrightarrow> y \<bullet> b \<le> x \<bullet> b)" by blast |
|
145 |
qed |
|
146 |
||
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
147 |
lemma (in order) atLeastatMost_empty'[simp]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
148 |
"(~ a <= b) \<Longrightarrow> {a..b} = {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
149 |
by (auto) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
150 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
151 |
instance real :: ordered_euclidean_space |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
152 |
by default (auto simp: INF_def SUP_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
153 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
154 |
lemma in_Basis_prod_iff: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
155 |
fixes i::"'a::euclidean_space*'b::euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
156 |
shows "i \<in> Basis \<longleftrightarrow> fst i = 0 \<and> snd i \<in> Basis \<or> snd i = 0 \<and> fst i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
157 |
by (cases i) (auto simp: Basis_prod_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
158 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
159 |
instantiation prod::(abs, abs) abs |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
160 |
begin |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
161 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
162 |
definition "abs x = (abs (fst x), abs (snd x))" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
163 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
164 |
instance proof qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
165 |
end |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
166 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
167 |
instance prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
168 |
by default |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
169 |
(auto intro!: add_mono simp add: euclidean_representation_setsum' Ball_def inner_prod_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
170 |
in_Basis_prod_iff inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left Inf_prod_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
171 |
inner_Basis_SUP_left Sup_prod_def less_prod_def less_eq_prod_def eucl_le[where 'a='a] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
172 |
eucl_le[where 'a='b] abs_prod_def abs_inner) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
173 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
174 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
175 |
subsection {* Intervals *} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
176 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
177 |
lemma interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
178 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
179 |
shows "box a b = {x::'a. \<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
180 |
and "{a .. b} = {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
181 |
by (auto simp add:set_eq_iff eucl_le[where 'a='a] box_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
182 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
183 |
lemma mem_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
184 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
185 |
shows "x \<in> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < x\<bullet>i \<and> x\<bullet>i < b\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
186 |
and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
187 |
using interval[of a b] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
188 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
189 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
190 |
lemma interval_eq_empty: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
191 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
192 |
shows "(box a b = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i \<le> a\<bullet>i))" (is ?th1) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
193 |
and "({a .. b} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. b\<bullet>i < a\<bullet>i))" (is ?th2) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
194 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
195 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
196 |
fix i x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
197 |
assume i: "i\<in>Basis" and as:"b\<bullet>i \<le> a\<bullet>i" and x:"x\<in>box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
198 |
then have "a \<bullet> i < x \<bullet> i \<and> x \<bullet> i < b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
199 |
unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
200 |
then have "a\<bullet>i < b\<bullet>i" by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
201 |
then have False using as by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
202 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
203 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
204 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
205 |
assume as: "\<forall>i\<in>Basis. \<not> (b\<bullet>i \<le> a\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
206 |
let ?x = "(1/2) *\<^sub>R (a + b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
207 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
208 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
209 |
assume i: "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
210 |
have "a\<bullet>i < b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
211 |
using as[THEN bspec[where x=i]] i by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
212 |
then have "a\<bullet>i < ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i < b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
213 |
by (auto simp: inner_add_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
214 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
215 |
then have "box a b \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
216 |
using mem_interval(1)[of "?x" a b] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
217 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
218 |
ultimately show ?th1 by blast |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
219 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
220 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
221 |
fix i x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
222 |
assume i: "i \<in> Basis" and as:"b\<bullet>i < a\<bullet>i" and x:"x\<in>{a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
223 |
then have "a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
224 |
unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
225 |
then have "a\<bullet>i \<le> b\<bullet>i" by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
226 |
then have False using as by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
227 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
228 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
229 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
230 |
assume as:"\<forall>i\<in>Basis. \<not> (b\<bullet>i < a\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
231 |
let ?x = "(1/2) *\<^sub>R (a + b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
232 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
233 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
234 |
assume i:"i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
235 |
have "a\<bullet>i \<le> b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
236 |
using as[THEN bspec[where x=i]] i by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
237 |
then have "a\<bullet>i \<le> ((1/2) *\<^sub>R (a+b)) \<bullet> i" "((1/2) *\<^sub>R (a+b)) \<bullet> i \<le> b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
238 |
by (auto simp: inner_add_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
239 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
240 |
then have "{a .. b} \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
241 |
using mem_interval(2)[of "?x" a b] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
242 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
243 |
ultimately show ?th2 by blast |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
244 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
245 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
246 |
lemma interval_ne_empty: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
247 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
248 |
shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
249 |
and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i\<in>Basis. a\<bullet>i < b\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
250 |
unfolding interval_eq_empty[of a b] by fastforce+ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
251 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
252 |
lemma interval_sing: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
253 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
254 |
shows "{a .. a} = {a}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
255 |
and "box a a = {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
256 |
unfolding set_eq_iff mem_interval eq_iff [symmetric] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
257 |
by (auto intro: euclidean_eqI simp: ex_in_conv) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
258 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
259 |
lemma subset_interval_imp: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
260 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
261 |
shows "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
262 |
and "(\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i) \<Longrightarrow> {c .. d} \<subseteq> box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
263 |
and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
264 |
and "(\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i) \<Longrightarrow> box c d \<subseteq> box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
265 |
unfolding subset_eq[unfolded Ball_def] unfolding mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
266 |
by (best intro: order_trans less_le_trans le_less_trans less_imp_le)+ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
267 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
268 |
lemma interval_open_subset_closed: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
269 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
270 |
shows "box a b \<subseteq> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
271 |
unfolding subset_eq [unfolded Ball_def] mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
272 |
by (fast intro: less_imp_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
273 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
274 |
lemma subset_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
275 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
276 |
shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th1) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
277 |
and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i \<le> d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i < c\<bullet>i \<and> d\<bullet>i < b\<bullet>i)" (is ?th2) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
278 |
and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th3) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
279 |
and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i) --> (\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i)" (is ?th4) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
280 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
281 |
show ?th1 |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
282 |
unfolding subset_eq and Ball_def and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
283 |
by (auto intro: order_trans) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
284 |
show ?th2 |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
285 |
unfolding subset_eq and Ball_def and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
286 |
by (auto intro: le_less_trans less_le_trans order_trans less_imp_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
287 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
288 |
assume as: "box c d \<subseteq> {a .. b}" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
289 |
then have "box c d \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
290 |
unfolding interval_eq_empty by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
291 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
292 |
assume i: "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
293 |
(** TODO combine the following two parts as done in the HOL_light version. **) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
294 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
295 |
let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((min (a\<bullet>j) (d\<bullet>j))+c\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
296 |
assume as2: "a\<bullet>i > c\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
297 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
298 |
fix j :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
299 |
assume j: "j \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
300 |
then have "c \<bullet> j < ?x \<bullet> j \<and> ?x \<bullet> j < d \<bullet> j" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
301 |
apply (cases "j = i") |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
302 |
using as(2)[THEN bspec[where x=j]] i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
303 |
apply (auto simp add: as2) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
304 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
305 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
306 |
then have "?x\<in>box c d" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
307 |
using i unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
308 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
309 |
have "?x \<notin> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
310 |
unfolding mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
311 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
312 |
apply (rule_tac x=i in bexI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
313 |
using as(2)[THEN bspec[where x=i]] and as2 i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
314 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
315 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
316 |
ultimately have False using as by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
317 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
318 |
then have "a\<bullet>i \<le> c\<bullet>i" by (rule ccontr) auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
319 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
320 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
321 |
let ?x = "(\<Sum>j\<in>Basis. (if j=i then ((max (b\<bullet>j) (c\<bullet>j))+d\<bullet>j)/2 else (c\<bullet>j+d\<bullet>j)/2) *\<^sub>R j)::'a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
322 |
assume as2: "b\<bullet>i < d\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
323 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
324 |
fix j :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
325 |
assume "j\<in>Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
326 |
then have "d \<bullet> j > ?x \<bullet> j \<and> ?x \<bullet> j > c \<bullet> j" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
327 |
apply (cases "j = i") |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
328 |
using as(2)[THEN bspec[where x=j]] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
329 |
apply (auto simp add: as2) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
330 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
331 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
332 |
then have "?x\<in>box c d" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
333 |
unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
334 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
335 |
have "?x\<notin>{a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
336 |
unfolding mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
337 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
338 |
apply (rule_tac x=i in bexI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
339 |
using as(2)[THEN bspec[where x=i]] and as2 using i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
340 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
341 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
342 |
ultimately have False using as by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
343 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
344 |
then have "b\<bullet>i \<ge> d\<bullet>i" by (rule ccontr) auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
345 |
ultimately |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
346 |
have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
347 |
} note part1 = this |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
348 |
show ?th3 |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
349 |
unfolding subset_eq and Ball_def and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
350 |
apply (rule, rule, rule, rule) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
351 |
apply (rule part1) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
352 |
unfolding subset_eq and Ball_def and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
353 |
prefer 4 |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
354 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
355 |
apply (erule_tac x=xa in allE, erule_tac x=xa in allE, fastforce)+ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
356 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
357 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
358 |
assume as: "box c d \<subseteq> box a b" "\<forall>i\<in>Basis. c\<bullet>i < d\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
359 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
360 |
assume i:"i\<in>Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
361 |
from as(1) have "box c d \<subseteq> {a..b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
362 |
using interval_open_subset_closed[of a b] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
363 |
then have "a\<bullet>i \<le> c\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
364 |
using part1 and as(2) using i by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
365 |
} note * = this |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
366 |
show ?th4 |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
367 |
unfolding subset_eq and Ball_def and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
368 |
apply (rule, rule, rule, rule) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
369 |
apply (rule *) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
370 |
unfolding subset_eq and Ball_def and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
371 |
prefer 4 |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
372 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
373 |
apply (erule_tac x=xa in allE, simp)+ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
374 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
375 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
376 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
377 |
lemma inter_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
378 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
379 |
shows "{a .. b} \<inter> {c .. d} = |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
380 |
{(\<Sum>i\<in>Basis. max (a\<bullet>i) (c\<bullet>i) *\<^sub>R i) .. (\<Sum>i\<in>Basis. min (b\<bullet>i) (d\<bullet>i) *\<^sub>R i)}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
381 |
unfolding set_eq_iff and Int_iff and mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
382 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
383 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
384 |
lemma disjoint_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
385 |
fixes a::"'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
386 |
shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i < c\<bullet>i \<or> d\<bullet>i < a\<bullet>i))" (is ?th1) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
387 |
and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i < a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th2) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
388 |
and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i < c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th3) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
389 |
and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i\<in>Basis. (b\<bullet>i \<le> a\<bullet>i \<or> d\<bullet>i \<le> c\<bullet>i \<or> b\<bullet>i \<le> c\<bullet>i \<or> d\<bullet>i \<le> a\<bullet>i))" (is ?th4) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
390 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
391 |
let ?z = "(\<Sum>i\<in>Basis. (((max (a\<bullet>i) (c\<bullet>i)) + (min (b\<bullet>i) (d\<bullet>i))) / 2) *\<^sub>R i)::'a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
392 |
have **: "\<And>P Q. (\<And>i :: 'a. i \<in> Basis \<Longrightarrow> Q ?z i \<Longrightarrow> P i) \<Longrightarrow> |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
393 |
(\<And>i x :: 'a. i \<in> Basis \<Longrightarrow> P i \<Longrightarrow> Q x i) \<Longrightarrow> (\<forall>x. \<exists>i\<in>Basis. Q x i) \<longleftrightarrow> (\<exists>i\<in>Basis. P i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
394 |
by blast |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
395 |
note * = set_eq_iff Int_iff empty_iff mem_interval ball_conj_distrib[symmetric] eq_False ball_simps(10) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
396 |
show ?th1 unfolding * by (intro **) auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
397 |
show ?th2 unfolding * by (intro **) auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
398 |
show ?th3 unfolding * by (intro **) auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
399 |
show ?th4 unfolding * by (intro **) auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
400 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
401 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
402 |
(* Moved interval_open_subset_closed a bit upwards *) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
403 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
404 |
lemma open_interval[intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
405 |
fixes a b :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
406 |
shows "open (box a b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
407 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
408 |
have "open (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
409 |
by (intro open_INT finite_lessThan ballI continuous_open_vimage allI |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
410 |
linear_continuous_at open_real_greaterThanLessThan finite_Basis bounded_linear_inner_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
411 |
also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i<..<b\<bullet>i}) = box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
412 |
by (auto simp add: interval) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
413 |
finally show "open (box a b)" . |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
414 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
415 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
416 |
lemma closed_interval[intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
417 |
fixes a b :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
418 |
shows "closed {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
419 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
420 |
have "closed (\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
421 |
by (intro closed_INT ballI continuous_closed_vimage allI |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
422 |
linear_continuous_at closed_real_atLeastAtMost finite_Basis bounded_linear_inner_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
423 |
also have "(\<Inter>i\<in>Basis. (\<lambda>x. x\<bullet>i) -` {a\<bullet>i .. b\<bullet>i}) = {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
424 |
by (auto simp add: eucl_le [where 'a='a]) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
425 |
finally show "closed {a .. b}" . |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
426 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
427 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
428 |
lemma interior_closed_interval [intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
429 |
fixes a b :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
430 |
shows "interior {a..b} = box a b" (is "?L = ?R") |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
431 |
proof(rule subset_antisym) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
432 |
show "?R \<subseteq> ?L" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
433 |
using interval_open_subset_closed open_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
434 |
by (rule interior_maximal) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
435 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
436 |
fix x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
437 |
assume "x \<in> interior {a..b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
438 |
then obtain s where s: "open s" "x \<in> s" "s \<subseteq> {a..b}" .. |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
439 |
then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
440 |
unfolding open_dist and subset_eq by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
441 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
442 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
443 |
assume i: "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
444 |
have "dist (x - (e / 2) *\<^sub>R i) x < e" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
445 |
and "dist (x + (e / 2) *\<^sub>R i) x < e" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
446 |
unfolding dist_norm |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
447 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
448 |
unfolding norm_minus_cancel |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
449 |
using norm_Basis[OF i] `e>0` |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
450 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
451 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
452 |
then have "a \<bullet> i \<le> (x - (e / 2) *\<^sub>R i) \<bullet> i" and "(x + (e / 2) *\<^sub>R i) \<bullet> i \<le> b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
453 |
using e[THEN spec[where x="x - (e/2) *\<^sub>R i"]] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
454 |
and e[THEN spec[where x="x + (e/2) *\<^sub>R i"]] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
455 |
unfolding mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
456 |
using i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
457 |
by blast+ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
458 |
then have "a \<bullet> i < x \<bullet> i" and "x \<bullet> i < b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
459 |
using `e>0` i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
460 |
by (auto simp: inner_diff_left inner_Basis inner_add_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
461 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
462 |
then have "x \<in> box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
463 |
unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
464 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
465 |
then show "?L \<subseteq> ?R" .. |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
466 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
467 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
468 |
lemma bounded_closed_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
469 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
470 |
shows "bounded {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
471 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
472 |
let ?b = "\<Sum>i\<in>Basis. \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
473 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
474 |
fix x :: "'a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
475 |
assume x: "\<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
476 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
477 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
478 |
assume "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
479 |
then have "\<bar>x\<bullet>i\<bar> \<le> \<bar>a\<bullet>i\<bar> + \<bar>b\<bullet>i\<bar>" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
480 |
using x[THEN bspec[where x=i]] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
481 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
482 |
then have "(\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar>) \<le> ?b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
483 |
apply - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
484 |
apply (rule setsum_mono) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
485 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
486 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
487 |
then have "norm x \<le> ?b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
488 |
using norm_le_l1[of x] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
489 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
490 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
491 |
unfolding interval and bounded_iff by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
492 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
493 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
494 |
lemma bounded_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
495 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
496 |
shows "bounded {a .. b} \<and> bounded (box a b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
497 |
using bounded_closed_interval[of a b] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
498 |
using interval_open_subset_closed[of a b] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
499 |
using bounded_subset[of "{a..b}" "box a b"] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
500 |
by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
501 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
502 |
lemma not_interval_univ: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
503 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
504 |
shows "{a .. b} \<noteq> UNIV \<and> box a b \<noteq> UNIV" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
505 |
using bounded_interval[of a b] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
506 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
507 |
lemma compact_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
508 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
509 |
shows "compact {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
510 |
using bounded_closed_imp_seq_compact[of "{a..b}"] using bounded_interval[of a b] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
511 |
by (auto simp: compact_eq_seq_compact_metric) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
512 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
513 |
lemma open_interval_midpoint: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
514 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
515 |
assumes "box a b \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
516 |
shows "((1/2) *\<^sub>R (a + b)) \<in> box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
517 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
518 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
519 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
520 |
assume "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
521 |
then have "a \<bullet> i < ((1 / 2) *\<^sub>R (a + b)) \<bullet> i \<and> ((1 / 2) *\<^sub>R (a + b)) \<bullet> i < b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
522 |
using assms[unfolded interval_ne_empty, THEN bspec[where x=i]] by (auto simp: inner_add_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
523 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
524 |
then show ?thesis unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
525 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
526 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
527 |
lemma open_closed_interval_convex: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
528 |
fixes x :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
529 |
assumes x: "x \<in> box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
530 |
and y: "y \<in> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
531 |
and e: "0 < e" "e \<le> 1" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
532 |
shows "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<in> box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
533 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
534 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
535 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
536 |
assume i: "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
537 |
have "a \<bullet> i = e * (a \<bullet> i) + (1 - e) * (a \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
538 |
unfolding left_diff_distrib by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
539 |
also have "\<dots> < e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
540 |
apply (rule add_less_le_mono) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
541 |
using e unfolding mult_less_cancel_left and mult_le_cancel_left |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
542 |
apply simp_all |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
543 |
using x unfolding mem_interval using i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
544 |
apply simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
545 |
using y unfolding mem_interval using i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
546 |
apply simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
547 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
548 |
finally have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
549 |
unfolding inner_simps by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
550 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
551 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
552 |
have "b \<bullet> i = e * (b\<bullet>i) + (1 - e) * (b\<bullet>i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
553 |
unfolding left_diff_distrib by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
554 |
also have "\<dots> > e * (x \<bullet> i) + (1 - e) * (y \<bullet> i)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
555 |
apply (rule add_less_le_mono) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
556 |
using e unfolding mult_less_cancel_left and mult_le_cancel_left |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
557 |
apply simp_all |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
558 |
using x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
559 |
unfolding mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
560 |
using i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
561 |
apply simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
562 |
using y |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
563 |
unfolding mem_interval |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
564 |
using i |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
565 |
apply simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
566 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
567 |
finally have "(e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
568 |
unfolding inner_simps by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
569 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
570 |
ultimately have "a \<bullet> i < (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i \<and> (e *\<^sub>R x + (1 - e) *\<^sub>R y) \<bullet> i < b \<bullet> i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
571 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
572 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
573 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
574 |
unfolding mem_interval by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
575 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
576 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
577 |
notation |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
578 |
eucl_less (infix "<e" 50) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
579 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
580 |
lemma closure_open_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
581 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
582 |
assumes "box a b \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
583 |
shows "closure (box a b) = {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
584 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
585 |
have ab: "a <e b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
586 |
using assms by (simp add: eucl_less_def interval_ne_empty) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
587 |
let ?c = "(1 / 2) *\<^sub>R (a + b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
588 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
589 |
fix x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
590 |
assume as:"x \<in> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
591 |
def f \<equiv> "\<lambda>n::nat. x + (inverse (real n + 1)) *\<^sub>R (?c - x)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
592 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
593 |
fix n |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
594 |
assume fn: "f n <e b \<longrightarrow> a <e f n \<longrightarrow> f n = x" and xc: "x \<noteq> ?c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
595 |
have *: "0 < inverse (real n + 1)" "inverse (real n + 1) \<le> 1" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
596 |
unfolding inverse_le_1_iff by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
597 |
have "(inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b)) + (1 - inverse (real n + 1)) *\<^sub>R x = |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
598 |
x + (inverse (real n + 1)) *\<^sub>R (((1 / 2) *\<^sub>R (a + b)) - x)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
599 |
by (auto simp add: algebra_simps) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
600 |
then have "f n <e b" and "a <e f n" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
601 |
using open_closed_interval_convex[OF open_interval_midpoint[OF assms] as *] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
602 |
unfolding f_def by (auto simp: interval eucl_less_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
603 |
then have False |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
604 |
using fn unfolding f_def using xc by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
605 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
606 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
607 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
608 |
assume "\<not> (f ---> x) sequentially" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
609 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
610 |
fix e :: real |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
611 |
assume "e > 0" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
612 |
then have "\<exists>N::nat. inverse (real (N + 1)) < e" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
613 |
using real_arch_inv[of e] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
614 |
apply (auto simp add: Suc_pred') |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
615 |
apply (rule_tac x="n - 1" in exI) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
616 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
617 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
618 |
then obtain N :: nat where "inverse (real (N + 1)) < e" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
619 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
620 |
then have "\<forall>n\<ge>N. inverse (real n + 1) < e" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
621 |
apply auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
622 |
apply (metis Suc_le_mono le_SucE less_imp_inverse_less nat_le_real_less order_less_trans |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
623 |
real_of_nat_Suc real_of_nat_Suc_gt_zero) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
624 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
625 |
then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
626 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
627 |
then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
628 |
unfolding LIMSEQ_def by(auto simp add: dist_norm) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
629 |
then have "(f ---> x) sequentially" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
630 |
unfolding f_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
631 |
using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
632 |
using tendsto_scaleR [OF _ tendsto_const, of "\<lambda>n::nat. inverse (real n + 1)" 0 sequentially "((1 / 2) *\<^sub>R (a + b) - x)"] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
633 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
634 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
635 |
ultimately have "x \<in> closure (box a b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
636 |
using as and open_interval_midpoint[OF assms] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
637 |
unfolding closure_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
638 |
unfolding islimpt_sequential |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
639 |
by (cases "x=?c") (auto simp: in_box_eucl_less) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
640 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
641 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
642 |
using closure_minimal[OF interval_open_subset_closed closed_interval, of a b] by blast |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
643 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
644 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
645 |
lemma bounded_subset_open_interval_symmetric: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
646 |
fixes s::"('a::ordered_euclidean_space) set" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
647 |
assumes "bounded s" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
648 |
shows "\<exists>a. s \<subseteq> box (-a) a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
649 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
650 |
obtain b where "b>0" and b: "\<forall>x\<in>s. norm x \<le> b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
651 |
using assms[unfolded bounded_pos] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
652 |
def a \<equiv> "(\<Sum>i\<in>Basis. (b + 1) *\<^sub>R i)::'a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
653 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
654 |
fix x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
655 |
assume "x \<in> s" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
656 |
fix i :: 'a |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
657 |
assume i: "i \<in> Basis" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
658 |
then have "(-a)\<bullet>i < x\<bullet>i" and "x\<bullet>i < a\<bullet>i" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
659 |
using b[THEN bspec[where x=x], OF `x\<in>s`] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
660 |
using Basis_le_norm[OF i, of x] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
661 |
unfolding inner_simps and a_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
662 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
663 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
664 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
665 |
by (auto intro: exI[where x=a] simp add: interval) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
666 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
667 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
668 |
lemma bounded_subset_open_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
669 |
fixes s :: "('a::ordered_euclidean_space) set" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
670 |
shows "bounded s \<Longrightarrow> (\<exists>a b. s \<subseteq> box a b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
671 |
by (auto dest!: bounded_subset_open_interval_symmetric) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
672 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
673 |
lemma bounded_subset_closed_interval_symmetric: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
674 |
fixes s :: "('a::ordered_euclidean_space) set" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
675 |
assumes "bounded s" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
676 |
shows "\<exists>a. s \<subseteq> {-a .. a}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
677 |
proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
678 |
obtain a where "s \<subseteq> box (-a) a" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
679 |
using bounded_subset_open_interval_symmetric[OF assms] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
680 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
681 |
using interval_open_subset_closed[of "-a" a] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
682 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
683 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
684 |
lemma bounded_subset_closed_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
685 |
fixes s :: "('a::ordered_euclidean_space) set" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
686 |
shows "bounded s \<Longrightarrow> \<exists>a b. s \<subseteq> {a .. b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
687 |
using bounded_subset_closed_interval_symmetric[of s] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
688 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
689 |
lemma frontier_closed_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
690 |
fixes a b :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
691 |
shows "frontier {a .. b} = {a .. b} - box a b" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
692 |
unfolding frontier_def unfolding interior_closed_interval and closure_closed[OF closed_interval] .. |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
693 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
694 |
lemma frontier_open_interval: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
695 |
fixes a b :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
696 |
shows "frontier (box a b) = (if box a b = {} then {} else {a .. b} - box a b)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
697 |
proof (cases "box a b = {}") |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
698 |
case True |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
699 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
700 |
using frontier_empty by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
701 |
next |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
702 |
case False |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
703 |
then show ?thesis |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
704 |
unfolding frontier_def and closure_open_interval[OF False] and interior_open[OF open_interval] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
705 |
by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
706 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
707 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
708 |
lemma inter_interval_mixed_eq_empty: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
709 |
fixes a :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
710 |
assumes "box c d \<noteq> {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
711 |
shows "box a b \<inter> {c .. d} = {} \<longleftrightarrow> box a b \<inter> box c d = {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
712 |
unfolding closure_open_interval[OF assms, symmetric] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
713 |
unfolding open_inter_closure_eq_empty[OF open_interval] .. |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
714 |
|
54781 | 715 |
lemma diameter_closed_interval: |
716 |
fixes a b::"'a::ordered_euclidean_space" |
|
717 |
shows "a \<le> b \<Longrightarrow> diameter {a..b} = dist a b" |
|
718 |
by (force simp add: diameter_def SUP_def intro!: cSup_eq_maximum setL2_mono |
|
719 |
simp: euclidean_dist_l2[where 'a='a] eucl_le[where 'a='a] dist_norm) |
|
720 |
||
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
721 |
text {* Intervals in general, including infinite and mixtures of open and closed. *} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
722 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
723 |
definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow> |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
724 |
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
725 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
726 |
lemma is_interval_interval: "is_interval {a .. b::'a::ordered_euclidean_space}" (is ?th1) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
727 |
"is_interval (box a b)" (is ?th2) proof - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
728 |
show ?th1 ?th2 unfolding is_interval_def mem_interval Ball_def atLeastAtMost_iff |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
729 |
by(meson order_trans le_less_trans less_le_trans less_trans)+ qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
730 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
731 |
lemma is_interval_empty: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
732 |
"is_interval {}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
733 |
unfolding is_interval_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
734 |
by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
735 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
736 |
lemma is_interval_univ: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
737 |
"is_interval UNIV" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
738 |
unfolding is_interval_def |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
739 |
by simp |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
740 |
|
54781 | 741 |
lemma mem_is_intervalI: |
742 |
assumes "is_interval s" |
|
743 |
assumes "a \<in> s" "b \<in> s" |
|
744 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> b \<bullet> i \<or> b \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> a \<bullet> i" |
|
745 |
shows "x \<in> s" |
|
746 |
by (rule assms(1)[simplified is_interval_def, rule_format, OF assms(2,3,4)]) |
|
747 |
||
748 |
lemma interval_subst: |
|
749 |
fixes S::"'a::ordered_euclidean_space set" |
|
750 |
assumes "is_interval S" |
|
751 |
assumes "x \<in> S" "y j \<in> S" |
|
752 |
assumes "j \<in> Basis" |
|
753 |
shows "(\<Sum>i\<in>Basis. (if i = j then y i \<bullet> i else x \<bullet> i) *\<^sub>R i) \<in> S" |
|
754 |
by (rule mem_is_intervalI[OF assms(1,2)]) (auto simp: assms) |
|
755 |
||
756 |
lemma mem_interval_componentwiseI: |
|
757 |
fixes S::"'a::ordered_euclidean_space set" |
|
758 |
assumes "is_interval S" |
|
759 |
assumes "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<in> ((\<lambda>x. x \<bullet> i) ` S)" |
|
760 |
shows "x \<in> S" |
|
761 |
proof - |
|
762 |
from assms have "\<forall>i \<in> Basis. \<exists>s \<in> S. x \<bullet> i = s \<bullet> i" |
|
763 |
by auto |
|
764 |
with finite_Basis obtain s and bs::"'a list" where |
|
765 |
s: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i = s i \<bullet> i" "\<And>i. i \<in> Basis \<Longrightarrow> s i \<in> S" and |
|
766 |
bs: "set bs = Basis" "distinct bs" |
|
767 |
by (metis finite_distinct_list) |
|
768 |
from nonempty_Basis s obtain j where j: "j \<in> Basis" "s j \<in> S" by blast |
|
55413
a8e96847523c
adapted theories to '{case,rec}_{list,option}' names
blanchet
parents:
54781
diff
changeset
|
769 |
def y \<equiv> "rec_list |
54781 | 770 |
(s j) |
771 |
(\<lambda>j _ Y. (\<Sum>i\<in>Basis. (if i = j then s i \<bullet> i else Y \<bullet> i) *\<^sub>R i))" |
|
772 |
have "x = (\<Sum>i\<in>Basis. (if i \<in> set bs then s i \<bullet> i else s j \<bullet> i) *\<^sub>R i)" |
|
773 |
using bs by (auto simp add: s(1)[symmetric] euclidean_representation) |
|
774 |
also have [symmetric]: "y bs = \<dots>" |
|
775 |
using bs(2) bs(1)[THEN equalityD1] |
|
776 |
by (induct bs) (auto simp: y_def euclidean_representation intro!: euclidean_eqI[where 'a='a]) |
|
777 |
also have "y bs \<in> S" |
|
778 |
using bs(1)[THEN equalityD1] |
|
779 |
apply (induct bs) |
|
780 |
apply (auto simp: y_def j) |
|
781 |
apply (rule interval_subst[OF assms(1)]) |
|
782 |
apply (auto simp: s) |
|
783 |
done |
|
784 |
finally show ?thesis . |
|
785 |
qed |
|
786 |
||
54780
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
787 |
text{* Instantiation for intervals on @{text ordered_euclidean_space} *} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
788 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
789 |
lemma eucl_lessThan_eq_halfspaces: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
790 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
791 |
shows "{x. x <e a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i < a \<bullet> i})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
792 |
by (auto simp: eucl_less_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
793 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
794 |
lemma eucl_greaterThan_eq_halfspaces: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
795 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
796 |
shows "{x. a <e x} = (\<Inter>i\<in>Basis. {x. a \<bullet> i < x \<bullet> i})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
797 |
by (auto simp: eucl_less_def) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
798 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
799 |
lemma eucl_atMost_eq_halfspaces: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
800 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
801 |
shows "{.. a} = (\<Inter>i\<in>Basis. {x. x \<bullet> i \<le> a \<bullet> i})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
802 |
by (auto simp: eucl_le[where 'a='a]) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
803 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
804 |
lemma eucl_atLeast_eq_halfspaces: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
805 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
806 |
shows "{a ..} = (\<Inter>i\<in>Basis. {x. a \<bullet> i \<le> x \<bullet> i})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
807 |
by (auto simp: eucl_le[where 'a='a]) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
808 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
809 |
lemma open_eucl_lessThan[simp, intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
810 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
811 |
shows "open {x. x <e a}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
812 |
by (auto simp: eucl_lessThan_eq_halfspaces open_halfspace_component_lt) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
813 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
814 |
lemma open_eucl_greaterThan[simp, intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
815 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
816 |
shows "open {x. a <e x}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
817 |
by (auto simp: eucl_greaterThan_eq_halfspaces open_halfspace_component_gt) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
818 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
819 |
lemma closed_eucl_atMost[simp, intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
820 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
821 |
shows "closed {.. a}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
822 |
unfolding eucl_atMost_eq_halfspaces |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
823 |
by (simp add: closed_INT closed_Collect_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
824 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
825 |
lemma closed_eucl_atLeast[simp, intro]: |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
826 |
fixes a :: "'a\<Colon>ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
827 |
shows "closed {a ..}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
828 |
unfolding eucl_atLeast_eq_halfspaces |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
829 |
by (simp add: closed_INT closed_Collect_le) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
830 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
831 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
832 |
lemma image_affinity_interval: fixes m::real |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
833 |
fixes a b c :: "'a::ordered_euclidean_space" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
834 |
shows "(\<lambda>x. m *\<^sub>R x + c) ` {a .. b} = |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
835 |
(if {a .. b} = {} then {} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
836 |
else (if 0 \<le> m then {m *\<^sub>R a + c .. m *\<^sub>R b + c} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
837 |
else {m *\<^sub>R b + c .. m *\<^sub>R a + c}))" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
838 |
proof (cases "m = 0") |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
839 |
case True |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
840 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
841 |
fix x |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
842 |
assume "x \<le> c" "c \<le> x" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
843 |
then have "x = c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
844 |
unfolding eucl_le[where 'a='a] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
845 |
apply - |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
846 |
apply (subst euclidean_eq_iff) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
847 |
apply (auto intro: order_antisym) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
848 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
849 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
850 |
moreover have "c \<in> {m *\<^sub>R a + c..m *\<^sub>R b + c}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
851 |
unfolding True by (auto simp add: eucl_le[where 'a='a]) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
852 |
ultimately show ?thesis using True by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
853 |
next |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
854 |
case False |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
855 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
856 |
fix y |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
857 |
assume "a \<le> y" "y \<le> b" "m > 0" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
858 |
then have "m *\<^sub>R a + c \<le> m *\<^sub>R y + c" and "m *\<^sub>R y + c \<le> m *\<^sub>R b + c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
859 |
unfolding eucl_le[where 'a='a] by (auto simp: inner_distrib) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
860 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
861 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
862 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
863 |
fix y |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
864 |
assume "a \<le> y" "y \<le> b" "m < 0" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
865 |
then have "m *\<^sub>R b + c \<le> m *\<^sub>R y + c" and "m *\<^sub>R y + c \<le> m *\<^sub>R a + c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
866 |
unfolding eucl_le[where 'a='a] by (auto simp add: mult_left_mono_neg inner_distrib) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
867 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
868 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
869 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
870 |
fix y |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
871 |
assume "m > 0" and "m *\<^sub>R a + c \<le> y" and "y \<le> m *\<^sub>R b + c" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
872 |
then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
873 |
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
874 |
apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
875 |
apply (auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
876 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
877 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
878 |
moreover |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
879 |
{ |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
880 |
fix y |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
881 |
assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
882 |
then have "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
883 |
unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a] |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
884 |
apply (intro exI[where x="(1 / m) *\<^sub>R (y - c)"]) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
885 |
apply (auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff inner_distrib inner_diff_left) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
886 |
done |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
887 |
} |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
888 |
ultimately show ?thesis using False by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
889 |
qed |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
890 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
891 |
lemma image_smult_interval:"(\<lambda>x. m *\<^sub>R (x::_::ordered_euclidean_space)) ` {a..b} = |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
892 |
(if {a..b} = {} then {} else if 0 \<le> m then {m *\<^sub>R a..m *\<^sub>R b} else {m *\<^sub>R b..m *\<^sub>R a})" |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
893 |
using image_affinity_interval[of m 0 a b] by auto |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
894 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
895 |
no_notation |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
896 |
eucl_less (infix "<e" 50) |
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
897 |
|
6fae499e0827
summarized notions related to ordered_euclidean_space and intervals in separate theory
immler
parents:
diff
changeset
|
898 |
end |