author  nipkow 
Wed, 23 Aug 2017 18:28:56 +0200  
changeset 66490  cc66ab2373ce 
parent 65578  e4997c181cce 
child 66836  4eb431c3f974 
permissions  rwrr 
47317
432b29a96f61
modernized obsolete oldstyle theory name with proper newstyle underscore
huffman
parents:
47222
diff
changeset

1 
(* Title: HOL/Set_Interval.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

2 
Author: Tobias Nipkow 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

3 
Author: Clemens Ballarin 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

4 
Author: Jeremy Avigad 
8924  5 

13735  6 
lessThan, greaterThan, atLeast, atMost and twosided intervals 
51334  7 

8 
Modern convention: Ixy stands for an interval where x and y 

9 
describe the lower and upper bound and x,y : {c,o,i} 

10 
where c = closed, o = open, i = infinite. 

11 
Examples: Ico = {_ ..< _} and Ici = {_ ..} 

8924  12 
*) 
13 

60758  14 
section \<open>Set intervals\<close> 
14577  15 

47317
432b29a96f61
modernized obsolete oldstyle theory name with proper newstyle underscore
huffman
parents:
47222
diff
changeset

16 
theory Set_Interval 
63365  17 
imports Lattices_Big Divides Nat_Transfer 
15131  18 
begin 
8924  19 

24691  20 
context ord 
21 
begin 

44008  22 

24691  23 
definition 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

24 
lessThan :: "'a => 'a set" ("(1{..<_})") where 
25062  25 
"{..<u} == {x. x < u}" 
24691  26 

27 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

28 
atMost :: "'a => 'a set" ("(1{.._})") where 
25062  29 
"{..u} == {x. x \<le> u}" 
24691  30 

31 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

32 
greaterThan :: "'a => 'a set" ("(1{_<..})") where 
25062  33 
"{l<..} == {x. l<x}" 
24691  34 

35 
definition 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32596
diff
changeset

36 
atLeast :: "'a => 'a set" ("(1{_..})") where 
25062  37 
"{l..} == {x. l\<le>x}" 
24691  38 

39 
definition 

25062  40 
greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where 
41 
"{l<..<u} == {l<..} Int {..<u}" 

24691  42 

43 
definition 

25062  44 
atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where 
45 
"{l..<u} == {l..} Int {..<u}" 

24691  46 

47 
definition 

25062  48 
greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where 
49 
"{l<..u} == {l<..} Int {..u}" 

24691  50 

51 
definition 

25062  52 
atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where 
53 
"{l..u} == {l..} Int {..u}" 

24691  54 

55 
end 

8924  56 

13735  57 

60758  58 
text\<open>A note of warning when using @{term"{..<n}"} on type @{typ 
15048  59 
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving 
60758  60 
@{term"{m..<n}"} may not exist in @{term"{..<n}"}form as well.\<close> 
15048  61 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

62 
syntax (ASCII) 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

63 
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3UN _<=_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

64 
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3UN _<_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

65 
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3INT _<=_./ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

66 
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3INT _<_./ _)" [0, 0, 10] 10) 
14418  67 

30372  68 
syntax (latex output) 
62789  69 
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10) 
70 
"_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10) 

71 
"_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ \<le> _)/ _)" [0, 0, 10] 10) 

72 
"_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(\<open>unbreakable\<close>_ < _)/ _)" [0, 0, 10] 10) 

14418  73 

61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

74 
syntax 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

75 
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

76 
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

77 
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

78 
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_<_./ _)" [0, 0, 10] 10) 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

79 

14418  80 
translations 
61955
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

81 
"\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A" 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

82 
"\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A" 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

83 
"\<Inter>i\<le>n. A" \<rightleftharpoons> "\<Inter>i\<in>{..n}. A" 
e96292f32c3c
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
wenzelm
parents:
61799
diff
changeset

84 
"\<Inter>i<n. A" \<rightleftharpoons> "\<Inter>i\<in>{..<n}. A" 
14418  85 

86 

60758  87 
subsection \<open>Various equivalences\<close> 
13735  88 

25062  89 
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)" 
13850  90 
by (simp add: lessThan_def) 
13735  91 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

92 
lemma Compl_lessThan [simp]: 
13735  93 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  94 
apply (auto simp add: lessThan_def atLeast_def) 
13735  95 
done 
96 

13850  97 
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k}  lessThan k = {k}" 
98 
by auto 

13735  99 

25062  100 
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" 
13850  101 
by (simp add: greaterThan_def) 
13735  102 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

103 
lemma Compl_greaterThan [simp]: 
13735  104 
"!!k:: 'a::linorder. greaterThan k = atMost k" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

105 
by (auto simp add: greaterThan_def atMost_def) 
13735  106 

13850  107 
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. atMost k = greaterThan k" 
108 
apply (subst Compl_greaterThan [symmetric]) 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

109 
apply (rule double_complement) 
13735  110 
done 
111 

25062  112 
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" 
13850  113 
by (simp add: atLeast_def) 
13735  114 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

115 
lemma Compl_atLeast [simp]: 
13735  116 
"!!k:: 'a::linorder. atLeast k = lessThan k" 
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset

117 
by (auto simp add: lessThan_def atLeast_def) 
13735  118 

25062  119 
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" 
13850  120 
by (simp add: atMost_def) 
13735  121 

14485  122 
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" 
123 
by (blast intro: order_antisym) 

13850  124 

50999  125 
lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}" 
126 
by auto 

127 

128 
lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}" 

129 
by auto 

13850  130 

60758  131 
subsection \<open>Logical Equivalences for Set Inclusion and Equality\<close> 
13850  132 

63879
15bbf6360339
simple new lemmas, mostly about sets
paulson <lp15@cam.ac.uk>
parents:
63721
diff
changeset

133 
lemma atLeast_empty_triv [simp]: "{{}..} = UNIV" 
15bbf6360339
simple new lemmas, mostly about sets
paulson <lp15@cam.ac.uk>
parents:
63721
diff
changeset

134 
by auto 
15bbf6360339
simple new lemmas, mostly about sets
paulson <lp15@cam.ac.uk>
parents:
63721
diff
changeset

135 

15bbf6360339
simple new lemmas, mostly about sets
paulson <lp15@cam.ac.uk>
parents:
63721
diff
changeset

136 
lemma atMost_UNIV_triv [simp]: "{..UNIV} = UNIV" 
15bbf6360339
simple new lemmas, mostly about sets
paulson <lp15@cam.ac.uk>
parents:
63721
diff
changeset

137 
by auto 
15bbf6360339
simple new lemmas, mostly about sets
paulson <lp15@cam.ac.uk>
parents:
63721
diff
changeset

138 

13850  139 
lemma atLeast_subset_iff [iff]: 
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

140 
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

141 
by (blast intro: order_trans) 
13850  142 

143 
lemma atLeast_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

144 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  145 
by (blast intro: order_antisym order_trans) 
146 

147 
lemma greaterThan_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

148 
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

149 
apply (auto simp add: greaterThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

150 
apply (subst linorder_not_less [symmetric], blast) 
13850  151 
done 
152 

153 
lemma greaterThan_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

154 
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

155 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

156 
apply (erule equalityE) 
29709  157 
apply simp_all 
13850  158 
done 
159 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

160 
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" 
13850  161 
by (blast intro: order_trans) 
162 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

163 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  164 
by (blast intro: order_antisym order_trans) 
165 

166 
lemma lessThan_subset_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

167 
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

168 
apply (auto simp add: lessThan_def) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

169 
apply (subst linorder_not_less [symmetric], blast) 
13850  170 
done 
171 

172 
lemma lessThan_eq_iff [iff]: 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

173 
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

174 
apply (rule iffI) 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

175 
apply (erule equalityE) 
29709  176 
apply simp_all 
13735  177 
done 
178 

40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

179 
lemma lessThan_strict_subset_iff: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

180 
fixes m n :: "'a::linorder" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

181 
shows "{..<m} < {..<n} \<longleftrightarrow> m < n" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

182 
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) 
13735  183 

57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

184 
lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

185 
by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

186 

159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

187 
lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b" 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

188 
by auto 
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset

189 

62369  190 
lemma (in preorder) Ioi_le_Ico: "{a <..} \<subseteq> {a ..}" 
191 
by (auto intro: less_imp_le) 

192 

60758  193 
subsection \<open>Twosided intervals\<close> 
13735  194 

24691  195 
context ord 
196 
begin 

197 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

198 
lemma greaterThanLessThan_iff [simp]: 
25062  199 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  200 
by (simp add: greaterThanLessThan_def) 
201 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

202 
lemma atLeastLessThan_iff [simp]: 
25062  203 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  204 
by (simp add: atLeastLessThan_def) 
205 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

206 
lemma greaterThanAtMost_iff [simp]: 
25062  207 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  208 
by (simp add: greaterThanAtMost_def) 
209 

54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset

210 
lemma atLeastAtMost_iff [simp]: 
25062  211 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  212 
by (simp add: atLeastAtMost_def) 
213 

60758  214 
text \<open>The above four lemmas could be declared as iffs. Unfortunately this 
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset

215 
breaks many proofs. Since it only helps blast, it is better to leave them 
60758  216 
alone.\<close> 
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

217 

50999  218 
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }" 
219 
by auto 

220 

24691  221 
end 
13735  222 

60758  223 
subsubsection\<open>Emptyness, singletons, subset\<close> 
15554  224 

24691  225 
context order 
226 
begin 

15554  227 

32400  228 
lemma atLeastatMost_empty[simp]: 
229 
"b < a \<Longrightarrow> {a..b} = {}" 

230 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

231 

232 
lemma atLeastatMost_empty_iff[simp]: 

233 
"{a..b} = {} \<longleftrightarrow> (~ a <= b)" 

234 
by auto (blast intro: order_trans) 

235 

236 
lemma atLeastatMost_empty_iff2[simp]: 

237 
"{} = {a..b} \<longleftrightarrow> (~ a <= b)" 

238 
by auto (blast intro: order_trans) 

239 

240 
lemma atLeastLessThan_empty[simp]: 

241 
"b <= a \<Longrightarrow> {a..<b} = {}" 

242 
by(auto simp: atLeastLessThan_def) 

24691  243 

32400  244 
lemma atLeastLessThan_empty_iff[simp]: 
245 
"{a..<b} = {} \<longleftrightarrow> (~ a < b)" 

246 
by auto (blast intro: le_less_trans) 

247 

248 
lemma atLeastLessThan_empty_iff2[simp]: 

249 
"{} = {a..<b} \<longleftrightarrow> (~ a < b)" 

250 
by auto (blast intro: le_less_trans) 

15554  251 

32400  252 
lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}" 
17719  253 
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) 
254 

32400  255 
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l" 
256 
by auto (blast intro: less_le_trans) 

257 

258 
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l" 

259 
by auto (blast intro: less_le_trans) 

260 

29709  261 
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}" 
17719  262 
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) 
263 

25062  264 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  265 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
266 

36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

267 
lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

268 

32400  269 
lemma atLeastatMost_subset_iff[simp]: 
270 
"{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b)  c <= a & b <= d" 

271 
unfolding atLeastAtMost_def atLeast_def atMost_def 

272 
by (blast intro: order_trans) 

273 

274 
lemma atLeastatMost_psubset_iff: 

275 
"{a..b} < {c..d} \<longleftrightarrow> 

276 
((~ a <= b)  c <= a & b <= d & (c < a  b < d)) & c <= d" 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

277 
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 
32400  278 

51334  279 
lemma Icc_eq_Icc[simp]: 
280 
"{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')" 

281 
by(simp add: order_class.eq_iff)(auto intro: order_trans) 

282 

36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

283 
lemma atLeastAtMost_singleton_iff[simp]: 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

284 
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c" 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

285 
proof 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

286 
assume "{a..b} = {c}" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

287 
hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp 
60758  288 
with \<open>{a..b} = {c}\<close> have "c \<le> a \<and> b \<le> c" by auto 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

289 
with * show "a = b \<and> b = c" by auto 
36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

290 
qed simp 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

291 

51334  292 
lemma Icc_subset_Ici_iff[simp]: 
293 
"{l..h} \<subseteq> {l'..} = (~ l\<le>h \<or> l\<ge>l')" 

294 
by(auto simp: subset_eq intro: order_trans) 

295 

296 
lemma Icc_subset_Iic_iff[simp]: 

297 
"{l..h} \<subseteq> {..h'} = (~ l\<le>h \<or> h\<le>h')" 

298 
by(auto simp: subset_eq intro: order_trans) 

299 

300 
lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}" 

301 
by(auto simp: set_eq_iff) 

302 

303 
lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}" 

304 
by(auto simp: set_eq_iff) 

305 

306 
lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] 

307 
lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] 

308 

24691  309 
end 
14485  310 

51334  311 
context no_top 
312 
begin 

313 

314 
(* also holds for no_bot but no_top should suffice *) 

315 
lemma not_UNIV_le_Icc[simp]: "\<not> UNIV \<subseteq> {l..h}" 

316 
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) 

317 

318 
lemma not_UNIV_le_Iic[simp]: "\<not> UNIV \<subseteq> {..h}" 

319 
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) 

320 

321 
lemma not_Ici_le_Icc[simp]: "\<not> {l..} \<subseteq> {l'..h'}" 

322 
using gt_ex[of h'] 

323 
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 

324 

325 
lemma not_Ici_le_Iic[simp]: "\<not> {l..} \<subseteq> {..h'}" 

326 
using gt_ex[of h'] 

327 
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 

328 

329 
end 

330 

331 
context no_bot 

332 
begin 

333 

334 
lemma not_UNIV_le_Ici[simp]: "\<not> UNIV \<subseteq> {l..}" 

335 
using lt_ex[of l] by(auto simp: subset_eq less_le_not_le) 

336 

337 
lemma not_Iic_le_Icc[simp]: "\<not> {..h} \<subseteq> {l'..h'}" 

338 
using lt_ex[of l'] 

339 
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 

340 

341 
lemma not_Iic_le_Ici[simp]: "\<not> {..h} \<subseteq> {l'..}" 

342 
using lt_ex[of l'] 

343 
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) 

344 

345 
end 

346 

347 

348 
context no_top 

349 
begin 

350 

351 
(* also holds for no_bot but no_top should suffice *) 

352 
lemma not_UNIV_eq_Icc[simp]: "\<not> UNIV = {l'..h'}" 

353 
using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) 

354 

355 
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] 

356 

357 
lemma not_UNIV_eq_Iic[simp]: "\<not> UNIV = {..h'}" 

358 
using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) 

359 

360 
lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] 

361 

362 
lemma not_Icc_eq_Ici[simp]: "\<not> {l..h} = {l'..}" 

363 
unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast 

364 

365 
lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] 

366 

367 
(* also holds for no_bot but no_top should suffice *) 

368 
lemma not_Iic_eq_Ici[simp]: "\<not> {..h} = {l'..}" 

369 
using not_Ici_le_Iic[of l' h] by blast 

370 

371 
lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] 

372 

373 
end 

374 

375 
context no_bot 

376 
begin 

377 

378 
lemma not_UNIV_eq_Ici[simp]: "\<not> UNIV = {l'..}" 

379 
using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le) 

380 

381 
lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] 

382 

383 
lemma not_Icc_eq_Iic[simp]: "\<not> {l..h} = {..h'}" 

384 
unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast 

385 

386 
lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] 

387 

388 
end 

389 

390 

53216  391 
context dense_linorder 
42891
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

392 
begin 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

393 

e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

394 
lemma greaterThanLessThan_empty_iff[simp]: 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

395 
"{ a <..< b } = {} \<longleftrightarrow> b \<le> a" 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

396 
using dense[of a b] by (cases "a < b") auto 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

397 

e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

398 
lemma greaterThanLessThan_empty_iff2[simp]: 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

399 
"{} = { a <..< b } \<longleftrightarrow> b \<le> a" 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

400 
using dense[of a b] by (cases "a < b") auto 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

401 

42901  402 
lemma atLeastLessThan_subseteq_atLeastAtMost_iff: 
403 
"{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

404 
using dense[of "max a d" "b"] 

405 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

406 

407 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

408 
"{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

409 
using dense[of "a" "min c b"] 

410 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

411 

412 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

413 
"{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

414 
using dense[of "a" "min c b"] dense[of "max a d" "b"] 

415 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

416 

43657  417 
lemma atLeastAtMost_subseteq_atLeastLessThan_iff: 
418 
"{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)" 

419 
using dense[of "max a d" "b"] 

420 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

62369  421 

61524
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61378
diff
changeset

422 
lemma greaterThanLessThan_subseteq_greaterThanLessThan: 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61378
diff
changeset

423 
"{a <..< b} \<subseteq> {c <..< d} \<longleftrightarrow> (a < b \<longrightarrow> a \<ge> c \<and> b \<le> d)" 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61378
diff
changeset

424 
using dense[of "a" "min c b"] dense[of "max a d" "b"] 
f2e51e704a96
added many small lemmas about setsum/setprod/powr/...
eberlm
parents:
61378
diff
changeset

425 
by (force simp: subset_eq Ball_def not_less[symmetric]) 
43657  426 

427 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

428 
"{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)" 

429 
using dense[of "a" "min c b"] 

430 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

431 

432 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

433 
"{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

434 
using dense[of "a" "min c b"] dense[of "max a d" "b"] 

435 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

436 

56328  437 
lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff: 
438 
"{a <..< b} \<subseteq> { c <.. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" 

439 
using dense[of "a" "min c b"] dense[of "max a d" "b"] 

440 
by (force simp: subset_eq Ball_def not_less[symmetric]) 

441 

42891
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

442 
end 
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset

443 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

444 
context no_top 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

445 
begin 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

446 

51334  447 
lemma greaterThan_non_empty[simp]: "{x <..} \<noteq> {}" 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

448 
using gt_ex[of x] by auto 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

449 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

450 
end 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

451 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

452 
context no_bot 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

453 
begin 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

454 

51334  455 
lemma lessThan_non_empty[simp]: "{..< x} \<noteq> {}" 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

456 
using lt_ex[of x] by auto 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

457 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

458 
end 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

459 

32408  460 
lemma (in linorder) atLeastLessThan_subset_iff: 
461 
"{a..<b} <= {c..<d} \<Longrightarrow> b <= a  c<=a & b<=d" 

462 
apply (auto simp:subset_eq Ball_def) 

463 
apply(frule_tac x=a in spec) 

464 
apply(erule_tac x=d in allE) 

465 
apply (simp add: less_imp_le) 

466 
done 

467 

40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

468 
lemma atLeastLessThan_inj: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

469 
fixes a b c d :: "'a::linorder" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

470 
assumes eq: "{a ..< b} = {c ..< d}" and "a < b" "c < d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

471 
shows "a = c" "b = d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

472 
using assms by (metis atLeastLessThan_subset_iff eq less_le_not_le linorder_antisym_conv2 subset_refl)+ 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

473 

d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

474 
lemma atLeastLessThan_eq_iff: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

475 
fixes a b c d :: "'a::linorder" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

476 
assumes "a < b" "c < d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

477 
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

478 
using atLeastLessThan_inj assms by auto 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

479 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

480 
lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

481 
by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

482 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

483 
lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

484 
by auto 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

485 

87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

486 
lemma (in linorder) Ioc_subset_iff: "{a<..b} \<subseteq> {c<..d} \<longleftrightarrow> (b \<le> a \<or> c \<le> a \<and> b \<le> d)" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

487 
by (auto simp: subset_eq Ball_def) (metis less_le not_less) 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

488 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset

489 
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" 
51334  490 
by (auto simp: set_eq_iff intro: le_bot) 
51328
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

491 

52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset

492 
lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top" 
51334  493 
by (auto simp: set_eq_iff intro: top_le) 
51328
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

494 

51334  495 
lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff: 
496 
"{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)" 

497 
by (auto simp: set_eq_iff intro: top_le le_bot) 

51328
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

498 

56949  499 
lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot" 
500 
by (auto simp: set_eq_iff not_less le_bot) 

501 

502 
lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0" 

503 
by (simp add: Iio_eq_empty_iff bot_nat_def) 

504 

58970  505 
lemma mono_image_least: 
506 
assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n" 

507 
shows "f m = m'" 

508 
proof  

509 
from f_img have "{m' ..< n'} \<noteq> {}" 

510 
by (metis atLeastLessThan_empty_iff image_is_empty) 

511 
with f_img have "m' \<in> f ` {m ..< n}" by auto 

512 
then obtain k where "f k = m'" "m \<le> k" by auto 

513 
moreover have "m' \<le> f m" using f_img by auto 

514 
ultimately show "f m = m'" 

515 
using f_mono by (auto elim: monoE[where x=m and y=k]) 

516 
qed 

517 

51328
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

518 

60758  519 
subsection \<open>Infinite intervals\<close> 
56328  520 

521 
context dense_linorder 

522 
begin 

523 

524 
lemma infinite_Ioo: 

525 
assumes "a < b" 

526 
shows "\<not> finite {a<..<b}" 

527 
proof 

528 
assume fin: "finite {a<..<b}" 

529 
moreover have ne: "{a<..<b} \<noteq> {}" 

60758  530 
using \<open>a < b\<close> by auto 
56328  531 
ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" 
532 
using Max_in[of "{a <..< b}"] by auto 

533 
then obtain x where "Max {a <..< b} < x" "x < b" 

534 
using dense[of "Max {a<..<b}" b] by auto 

535 
then have "x \<in> {a <..< b}" 

60758  536 
using \<open>a < Max {a <..< b}\<close> by auto 
56328  537 
then have "x \<le> Max {a <..< b}" 
538 
using fin by auto 

60758  539 
with \<open>Max {a <..< b} < x\<close> show False by auto 
56328  540 
qed 
541 

542 
lemma infinite_Icc: "a < b \<Longrightarrow> \<not> finite {a .. b}" 

543 
using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b] 

544 
by (auto dest: finite_subset) 

545 

546 
lemma infinite_Ico: "a < b \<Longrightarrow> \<not> finite {a ..< b}" 

547 
using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b] 

548 
by (auto dest: finite_subset) 

549 

550 
lemma infinite_Ioc: "a < b \<Longrightarrow> \<not> finite {a <.. b}" 

551 
using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] 

552 
by (auto dest: finite_subset) 

553 

63967
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

554 
lemma infinite_Ioo_iff [simp]: "infinite {a<..<b} \<longleftrightarrow> a < b" 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

555 
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioo) 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

556 

2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

557 
lemma infinite_Icc_iff [simp]: "infinite {a .. b} \<longleftrightarrow> a < b" 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

558 
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Icc) 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

559 

2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

560 
lemma infinite_Ico_iff [simp]: "infinite {a..<b} \<longleftrightarrow> a < b" 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

561 
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ico) 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

562 

2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

563 
lemma infinite_Ioc_iff [simp]: "infinite {a<..b} \<longleftrightarrow> a < b" 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

564 
using not_less_iff_gr_or_eq by (fastforce simp: infinite_Ioc) 
2aa42596edc3
new material on paths, etc. Also rationalisation
paulson <lp15@cam.ac.uk>
parents:
63935
diff
changeset

565 

56328  566 
end 
567 

568 
lemma infinite_Iio: "\<not> finite {..< a :: 'a :: {no_bot, linorder}}" 

569 
proof 

570 
assume "finite {..< a}" 

571 
then have *: "\<And>x. x < a \<Longrightarrow> Min {..< a} \<le> x" 

572 
by auto 

573 
obtain x where "x < a" 

574 
using lt_ex by auto 

575 

576 
obtain y where "y < Min {..< a}" 

577 
using lt_ex by auto 

578 
also have "Min {..< a} \<le> x" 

60758  579 
using \<open>x < a\<close> by fact 
580 
also note \<open>x < a\<close> 

56328  581 
finally have "Min {..< a} \<le> y" 
582 
by fact 

60758  583 
with \<open>y < Min {..< a}\<close> show False by auto 
56328  584 
qed 
585 

586 
lemma infinite_Iic: "\<not> finite {.. a :: 'a :: {no_bot, linorder}}" 

587 
using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"] 

588 
by (auto simp: subset_eq less_imp_le) 

589 

590 
lemma infinite_Ioi: "\<not> finite {a :: 'a :: {no_top, linorder} <..}" 

591 
proof 

592 
assume "finite {a <..}" 

593 
then have *: "\<And>x. a < x \<Longrightarrow> x \<le> Max {a <..}" 

594 
by auto 

595 

596 
obtain y where "Max {a <..} < y" 

597 
using gt_ex by auto 

598 

63540  599 
obtain x where x: "a < x" 
56328  600 
using gt_ex by auto 
63540  601 
also from x have "x \<le> Max {a <..}" 
56328  602 
by fact 
60758  603 
also note \<open>Max {a <..} < y\<close> 
56328  604 
finally have "y \<le> Max { a <..}" 
605 
by fact 

60758  606 
with \<open>Max {a <..} < y\<close> show False by auto 
56328  607 
qed 
608 

609 
lemma infinite_Ici: "\<not> finite {a :: 'a :: {no_top, linorder} ..}" 

610 
using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] 

611 
by (auto simp: subset_eq less_imp_le) 

612 

60758  613 
subsubsection \<open>Intersection\<close> 
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

614 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

615 
context linorder 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

616 
begin 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

617 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

618 
lemma Int_atLeastAtMost[simp]: "{a..b} Int {c..d} = {max a c .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

619 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

620 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

621 
lemma Int_atLeastAtMostR1[simp]: "{..b} Int {c..d} = {c .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

622 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

623 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

624 
lemma Int_atLeastAtMostR2[simp]: "{a..} Int {c..d} = {max a c .. d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

625 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

626 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

627 
lemma Int_atLeastAtMostL1[simp]: "{a..b} Int {..d} = {a .. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

628 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

629 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

630 
lemma Int_atLeastAtMostL2[simp]: "{a..b} Int {c..} = {max a c .. b}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

631 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

632 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

633 
lemma Int_atLeastLessThan[simp]: "{a..<b} Int {c..<d} = {max a c ..< min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

634 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

635 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

636 
lemma Int_greaterThanAtMost[simp]: "{a<..b} Int {c<..d} = {max a c <.. min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

637 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

638 

341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

639 
lemma Int_greaterThanLessThan[simp]: "{a<..<b} Int {c<..<d} = {max a c <..< min b d}" 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

640 
by auto 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

641 

50417  642 
lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}" 
643 
by (auto simp: min_def) 

644 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

645 
lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a" 
63092  646 
by auto 
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset

647 

32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

648 
end 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

649 

51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

650 
context complete_lattice 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

651 
begin 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

652 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

653 
lemma 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

654 
shows Sup_atLeast[simp]: "Sup {x ..} = top" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

655 
and Sup_greaterThanAtLeast[simp]: "x < top \<Longrightarrow> Sup {x <..} = top" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

656 
and Sup_atMost[simp]: "Sup {.. y} = y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

657 
and Sup_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Sup { x .. y} = y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

658 
and Sup_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Sup { x <.. y} = y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

659 
by (auto intro!: Sup_eqI) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

660 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

661 
lemma 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

662 
shows Inf_atMost[simp]: "Inf {.. x} = bot" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

663 
and Inf_atMostLessThan[simp]: "top < x \<Longrightarrow> Inf {..< x} = bot" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

664 
and Inf_atLeast[simp]: "Inf {x ..} = x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

665 
and Inf_atLeastAtMost[simp]: "x \<le> y \<Longrightarrow> Inf { x .. y} = x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

666 
and Inf_atLeastLessThan[simp]: "x < y \<Longrightarrow> Inf { x ..< y} = x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

667 
by (auto intro!: Inf_eqI) 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

668 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

669 
end 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

670 

4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

671 
lemma 
53216  672 
fixes x y :: "'a :: {complete_lattice, dense_linorder}" 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

673 
shows Sup_lessThan[simp]: "Sup {..< y} = y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

674 
and Sup_atLeastLessThan[simp]: "x < y \<Longrightarrow> Sup { x ..< y} = y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

675 
and Sup_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Sup { x <..< y} = y" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

676 
and Inf_greaterThan[simp]: "Inf {x <..} = x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

677 
and Inf_greaterThanAtMost[simp]: "x < y \<Longrightarrow> Inf { x <.. y} = x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

678 
and Inf_greaterThanLessThan[simp]: "x < y \<Longrightarrow> Inf { x <..< y} = x" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

679 
by (auto intro!: Inf_eqI Sup_eqI intro: dense_le dense_le_bounded dense_ge dense_ge_bounded) 
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

680 

60758  681 
subsection \<open>Intervals of natural numbers\<close> 
14485  682 

60758  683 
subsubsection \<open>The Constant @{term lessThan}\<close> 
15047  684 

14485  685 
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" 
686 
by (simp add: lessThan_def) 

687 

688 
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" 

689 
by (simp add: lessThan_def less_Suc_eq, blast) 

690 

60758  691 
text \<open>The following proof is convenient in induction proofs where 
39072  692 
new elements get indices at the beginning. So it is used to transform 
60758  693 
@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}.\<close> 
39072  694 

59000  695 
lemma zero_notin_Suc_image: "0 \<notin> Suc ` A" 
696 
by auto 

697 

39072  698 
lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})" 
59000  699 
by (auto simp: image_iff less_Suc_eq_0_disj) 
39072  700 

14485  701 
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" 
702 
by (simp add: lessThan_def atMost_def less_Suc_eq_le) 

703 

59000  704 
lemma Iic_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})" 
705 
unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] .. 

706 

14485  707 
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" 
708 
by blast 

709 

60758  710 
subsubsection \<open>The Constant @{term greaterThan}\<close> 
15047  711 

65273
917ae0ba03a2
Removal of [simp] status for greaterThan_0. Moved two theorems into main HOL.
paulson <lp15@cam.ac.uk>
parents:
64773
diff
changeset

712 
lemma greaterThan_0: "greaterThan 0 = range Suc" 
14485  713 
apply (simp add: greaterThan_def) 
714 
apply (blast dest: gr0_conv_Suc [THEN iffD1]) 

715 
done 

716 

717 
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k  {Suc k}" 

718 
apply (simp add: greaterThan_def) 

719 
apply (auto elim: linorder_neqE) 

720 
done 

721 

722 
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" 

723 
by blast 

724 

60758  725 
subsubsection \<open>The Constant @{term atLeast}\<close> 
15047  726 

14485  727 
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" 
728 
by (unfold atLeast_def UNIV_def, simp) 

729 

730 
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k  {k}" 

731 
apply (simp add: atLeast_def) 

732 
apply (simp add: Suc_le_eq) 

733 
apply (simp add: order_le_less, blast) 

734 
done 

735 

736 
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" 

737 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

738 

739 
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" 

740 
by blast 

741 

60758  742 
subsubsection \<open>The Constant @{term atMost}\<close> 
15047  743 

14485  744 
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" 
745 
by (simp add: atMost_def) 

746 

747 
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" 

748 
apply (simp add: atMost_def) 

749 
apply (simp add: less_Suc_eq order_le_less, blast) 

750 
done 

751 

752 
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" 

753 
by blast 

754 

60758  755 
subsubsection \<open>The Constant @{term atLeastLessThan}\<close> 
15047  756 

60758  757 
text\<open>The orientation of the following 2 rules is tricky. The lhs is 
24449  758 
defined in terms of the rhs. Hence the chosen orientation makes sense 
759 
in this theory  the reverse orientation complicates proofs (eg 

760 
nontermination). But outside, when the definition of the lhs is rarely 

761 
used, the opposite orientation seems preferable because it reduces a 

60758  762 
specific concept to a more general one.\<close> 
28068  763 

63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

764 
lemma atLeast0LessThan [code_abbrev]: "{0::nat..<n} = {..<n}" 
15042  765 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  766 

63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

767 
lemma atLeast0AtMost [code_abbrev]: "{0..n::nat} = {..n}" 
28068  768 
by(simp add:atMost_def atLeastAtMost_def) 
769 

63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

770 
lemma lessThan_atLeast0: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

771 
"{..<n} = {0::nat..<n}" 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

772 
by (simp add: atLeast0LessThan) 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

773 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

774 
lemma atMost_atLeast0: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

775 
"{..n} = {0::nat..n}" 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

776 
by (simp add: atLeast0AtMost) 
24449  777 

778 
lemma atLeastLessThan0: "{m..<0::nat} = {}" 

15047  779 
by (simp add: atLeastLessThan_def) 
24449  780 

63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

781 
lemma atLeast0_lessThan_Suc: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

782 
"{0..<Suc n} = insert n {0..<n}" 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

783 
by (simp add: atLeast0LessThan lessThan_Suc) 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

784 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

785 
lemma atLeast0_lessThan_Suc_eq_insert_0: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

786 
"{0..<Suc n} = insert 0 (Suc ` {0..<n})" 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

787 
by (simp add: atLeast0LessThan lessThan_Suc_eq_insert_0) 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

788 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

789 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

790 
subsubsection \<open>The Constant @{term atLeastAtMost}\<close> 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

791 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

792 
lemma atLeast0_atMost_Suc: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

793 
"{0..Suc n} = insert (Suc n) {0..n}" 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

794 
by (simp add: atLeast0AtMost atMost_Suc) 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

795 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

796 
lemma atLeast0_atMost_Suc_eq_insert_0: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

797 
"{0..Suc n} = insert 0 (Suc ` {0..n})" 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

798 
by (simp add: atLeast0AtMost Iic_Suc_eq_insert_0) 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

799 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

800 

60758  801 
subsubsection \<open>Intervals of nats with @{term Suc}\<close> 
15047  802 

60758  803 
text\<open>Not a simprule because the RHS is too messy.\<close> 
15047  804 
lemma atLeastLessThanSuc: 
805 
"{m..<Suc n} = (if m \<le> n then insert n {m..<n} else {})" 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

806 
by (auto simp add: atLeastLessThan_def) 
15047  807 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

808 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  809 
by (auto simp add: atLeastLessThan_def) 
16041  810 
(* 
15047  811 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
812 
by (induct k, simp_all add: atLeastLessThanSuc) 

813 

814 
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" 

815 
by (auto simp add: atLeastLessThan_def) 

16041  816 
*) 
15045  817 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  818 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
819 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

820 
lemma atLeastSucAtMost_greaterThanAtMost: "{Suc l..u} = {l<..u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

821 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  822 
greaterThanAtMost_def) 
823 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

824 
lemma atLeastSucLessThan_greaterThanLessThan: "{Suc l..<u} = {l<..<u}" 
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

825 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  826 
greaterThanLessThan_def) 
827 

15554  828 
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" 
829 
by (auto simp add: atLeastAtMost_def) 

830 

45932  831 
lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}" 
832 
by auto 

833 

60758  834 
text \<open>The analogous result is useful on @{typ int}:\<close> 
43157  835 
(* here, because we don't have an own int section *) 
836 
lemma atLeastAtMostPlus1_int_conv: 

837 
"m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}" 

838 
by (auto intro: set_eqI) 

839 

33044  840 
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}" 
62369  841 
apply (induct k) 
842 
apply (simp_all add: atLeastLessThanSuc) 

33044  843 
done 
844 

60758  845 
subsubsection \<open>Intervals and numerals\<close> 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

846 

61799  847 
lemma lessThan_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close> 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

848 
"lessThan (numeral k :: nat) = insert (pred_numeral k) (lessThan (pred_numeral k))" 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

849 
by (simp add: numeral_eq_Suc lessThan_Suc) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

850 

61799  851 
lemma atMost_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close> 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

852 
"atMost (numeral k :: nat) = insert (numeral k) (atMost (pred_numeral k))" 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

853 
by (simp add: numeral_eq_Suc atMost_Suc) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

854 

61799  855 
lemma atLeastLessThan_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close> 
62369  856 
"atLeastLessThan m (numeral k :: nat) = 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

857 
(if m \<le> (pred_numeral k) then insert (pred_numeral k) (atLeastLessThan m (pred_numeral k)) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

858 
else {})" 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

859 
by (simp add: numeral_eq_Suc atLeastLessThanSuc) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

860 

60758  861 
subsubsection \<open>Image\<close> 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

862 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

863 
lemma image_add_atLeastAtMost [simp]: 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

864 
fixes k ::"'a::linordered_semidom" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

865 
shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

866 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

867 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

868 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

869 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

870 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

871 
fix n assume a: "n : ?B" 
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

872 
hence "n  k : {i..j}" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

873 
by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

874 
moreover have "n = (n  k) + k" using a 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

875 
proof  
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

876 
have "k + i \<le> n" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

877 
by (metis a add.commute atLeastAtMost_iff) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

878 
hence "k + (n  k) = n" 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

879 
by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

880 
thus ?thesis 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

881 
by (simp add: add.commute) 
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset

882 
qed 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

883 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

884 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

885 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

886 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

887 
lemma image_diff_atLeastAtMost [simp]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

888 
fixes d::"'a::linordered_idom" shows "(op  d ` {a..b}) = {db..da}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

889 
apply auto 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

890 
apply (rule_tac x="dx" in rev_image_eqI, auto) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

891 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

892 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

893 
lemma image_mult_atLeastAtMost [simp]: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

894 
fixes d::"'a::linordered_field" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

895 
assumes "d>0" shows "(op * d ` {a..b}) = {d*a..d*b}" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

896 
using assms 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

897 
by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

898 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

899 
lemma image_affinity_atLeastAtMost: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

900 
fixes c :: "'a::linordered_field" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

901 
shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {} 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

902 
else if 0 \<le> m then {m*a + c .. m *b + c} 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

903 
else {m*b + c .. m*a + c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

904 
apply (case_tac "m=0", auto simp: mult_le_cancel_left) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

905 
apply (rule_tac x="inverse m*(xc)" in rev_image_eqI, auto simp: field_simps) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

906 
apply (rule_tac x="inverse m*(xc)" in rev_image_eqI, auto simp: field_simps) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

907 
done 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

908 

457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

909 
lemma image_affinity_atLeastAtMost_diff: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

910 
fixes c :: "'a::linordered_field" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

911 
shows "((\<lambda>x. m*x  c) ` {a..b}) = (if {a..b}={} then {} 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

912 
else if 0 \<le> m then {m*a  c .. m*b  c} 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

913 
else {m*b  c .. m*a  c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

914 
using image_affinity_atLeastAtMost [of m "c" a b] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

915 
by simp 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

916 

61204  917 
lemma image_affinity_atLeastAtMost_div: 
918 
fixes c :: "'a::linordered_field" 

919 
shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {} 

920 
else if 0 \<le> m then {a/m + c .. b/m + c} 

921 
else {b/m + c .. a/m + c})" 

922 
using image_affinity_atLeastAtMost [of "inverse m" c a b] 

923 
by (simp add: field_class.field_divide_inverse algebra_simps) 

62369  924 

60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

925 
lemma image_affinity_atLeastAtMost_div_diff: 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

926 
fixes c :: "'a::linordered_field" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

927 
shows "((\<lambda>x. x/m  c) ` {a..b}) = (if {a..b}={} then {} 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

928 
else if 0 \<le> m then {a/m  c .. b/m  c} 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

929 
else {b/m  c .. a/m  c})" 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

930 
using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

931 
by (simp add: field_class.field_divide_inverse algebra_simps) 
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset

932 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

933 
lemma image_add_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

934 
"(%n::nat. n+k) ` {i..<j} = {i+k..<j+k}" (is "?A = ?B") 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

935 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

936 
show "?A \<subseteq> ?B" by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

937 
next 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

938 
show "?B \<subseteq> ?A" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

939 
proof 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

940 
fix n assume a: "n : ?B" 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset

941 
hence "n  k : {i..<j}" by auto 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

942 
moreover have "n = (n  k) + k" using a by auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

943 
ultimately show "n : ?A" by blast 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

944 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

945 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

946 

63365  947 
corollary image_Suc_lessThan: 
948 
"Suc ` {..<n} = {1..n}" 

949 
using image_add_atLeastLessThan [of 1 0 n] 

950 
by (auto simp add: lessThan_Suc_atMost atLeast0LessThan) 

63915  951 

63365  952 
corollary image_Suc_atMost: 
953 
"Suc ` {..n} = {1..Suc n}" 

954 
using image_add_atLeastLessThan [of 1 0 "Suc n"] 

955 
by (auto simp add: lessThan_Suc_atMost atLeast0LessThan) 

956 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

957 
corollary image_Suc_atLeastAtMost[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

958 
"Suc ` {i..j} = {Suc i..Suc j}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

959 
using image_add_atLeastAtMost[where k="Suc 0"] by simp 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

960 

236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

961 
corollary image_Suc_atLeastLessThan[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

962 
"Suc ` {i..<j} = {Suc i..<Suc j}" 
30079
293b896b9c25
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
huffman
parents:
29960
diff
changeset

963 
using image_add_atLeastLessThan[where k="Suc 0"] by simp 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

964 

63365  965 
lemma atLeast1_lessThan_eq_remove0: 
966 
"{Suc 0..<n} = {..<n}  {0}" 

967 
by auto 

968 

969 
lemma atLeast1_atMost_eq_remove0: 

970 
"{Suc 0..n} = {..n}  {0}" 

971 
by auto 

972 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

973 
lemma image_add_int_atLeastLessThan: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

974 
"(%x. x + (l::int)) ` {0..<ul} = {l..<u}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

975 
apply (auto simp add: image_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

976 
apply (rule_tac x = "x  l" in bexI) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

977 
apply auto 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

978 
done 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

979 

37664  980 
lemma image_minus_const_atLeastLessThan_nat: 
981 
fixes c :: nat 

982 
shows "(\<lambda>i. i  c) ` {x ..< y} = 

983 
(if c < y then {x  c ..< y  c} else if x < y then {0} else {})" 

984 
(is "_ = ?right") 

985 
proof safe 

986 
fix a assume a: "a \<in> ?right" 

987 
show "a \<in> (\<lambda>i. i  c) ` {x ..< y}" 

988 
proof cases 

989 
assume "c < y" with a show ?thesis 

990 
by (auto intro!: image_eqI[of _ _ "a + c"]) 

991 
next 

992 
assume "\<not> c < y" with a show ?thesis 

62390  993 
by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) 
37664  994 
qed 
995 
qed auto 

996 

51152  997 
lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}" 
55143
04448228381d
explicit eigencontext for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55088
diff
changeset

998 
by (auto intro!: image_eqI [where x = "nat x" for x]) 
51152  999 

35580  1000 
context ordered_ab_group_add 
1001 
begin 

1002 

1003 
lemma 

1004 
fixes x :: 'a 

1005 
shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<x}" 

1006 
and image_uminus_atLeast[simp]: "uminus ` {x..} = {..x}" 

1007 
proof safe 

1008 
fix y assume "y < x" 

1009 
hence *: "x < y" using neg_less_iff_less[of "y" x] by simp 

1010 
have " (y) \<in> uminus ` {x<..}" 

1011 
by (rule imageI) (simp add: *) 

1012 
thus "y \<in> uminus ` {x<..}" by simp 

1013 
next 

1014 
fix y assume "y \<le> x" 

1015 
have " (y) \<in> uminus ` {x..}" 

60758  1016 
by (rule imageI) (insert \<open>y \<le> x\<close>[THEN le_imp_neg_le], simp) 
35580  1017 
thus "y \<in> uminus ` {x..}" by simp 
1018 
qed simp_all 

1019 

1020 
lemma 

1021 
fixes x :: 'a 

1022 
shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {x<..}" 

1023 
and image_uminus_atMost[simp]: "uminus ` {..x} = {x..}" 

1024 
proof  

1025 
have "uminus ` {..<x} = uminus ` uminus ` {x<..}" 

1026 
and "uminus ` {..x} = uminus ` uminus ` {x..}" by simp_all 

1027 
thus "uminus ` {..<x} = {x<..}" and "uminus ` {..x} = {x..}" 

1028 
by (simp_all add: image_image 

1029 
del: image_uminus_greaterThan image_uminus_atLeast) 

1030 
qed 

1031 

1032 
lemma 

1033 
fixes x :: 'a 

1034 
shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {y..x}" 

1035 
and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {y..<x}" 

1036 
and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {y<..x}" 

1037 
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {y<..<x}" 

1038 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

1039 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

1040 
end 

16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1041 

60758  1042 
subsubsection \<open>Finiteness\<close> 
14485  1043 

15045  1044 
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" 
14485  1045 
by (induct k) (simp_all add: lessThan_Suc) 
1046 

1047 
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" 

1048 
by (induct k) (simp_all add: atMost_Suc) 

1049 

1050 
lemma finite_greaterThanLessThan [iff]: 

15045  1051 
fixes l :: nat shows "finite {l<..<u}" 
14485  1052 
by (simp add: greaterThanLessThan_def) 
1053 

1054 
lemma finite_atLeastLessThan [iff]: 

15045  1055 
fixes l :: nat shows "finite {l..<u}" 
14485  1056 
by (simp add: atLeastLessThan_def) 
1057 

1058 
lemma finite_greaterThanAtMost [iff]: 

15045  1059 
fixes l :: nat shows "finite {l<..u}" 
14485  1060 
by (simp add: greaterThanAtMost_def) 
1061 

1062 
lemma finite_atLeastAtMost [iff]: 

1063 
fixes l :: nat shows "finite {l..u}" 

1064 
by (simp add: atLeastAtMost_def) 

1065 

60758  1066 
text \<open>A bounded set of natural numbers is finite.\<close> 
14485  1067 
lemma bounded_nat_set_is_finite: 
24853  1068 
"(ALL i:N. i < (n::nat)) ==> finite N" 
28068  1069 
apply (rule finite_subset) 
1070 
apply (rule_tac [2] finite_lessThan, auto) 

1071 
done 

1072 

60758  1073 
text \<open>A set of natural numbers is finite iff it is bounded.\<close> 
31044  1074 
lemma finite_nat_set_iff_bounded: 
1075 
"finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B") 

1076 
proof 

1077 
assume f:?F show ?B 

60758  1078 
using Max_ge[OF \<open>?F\<close>, simplified less_Suc_eq_le[symmetric]] by blast 
31044  1079 
next 
60758  1080 
assume ?B show ?F using \<open>?B\<close> by(blast intro:bounded_nat_set_is_finite) 
31044  1081 
qed 
1082 

1083 
lemma finite_nat_set_iff_bounded_le: 

1084 
"finite(N::nat set) = (EX m. ALL n:N. n<=m)" 

1085 
apply(simp add:finite_nat_set_iff_bounded) 

1086 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

1087 
done 

1088 

28068  1089 
lemma finite_less_ub: 
1090 
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" 

1091 
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) 

14485  1092 

64773
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1093 
lemma bounded_Max_nat: 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1094 
fixes P :: "nat \<Rightarrow> bool" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1095 
assumes x: "P x" and M: "\<And>x. P x \<Longrightarrow> x \<le> M" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1096 
obtains m where "P m" "\<And>x. P x \<Longrightarrow> x \<le> m" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1097 
proof  
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1098 
have "finite {x. P x}" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1099 
using M finite_nat_set_iff_bounded_le by auto 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1100 
then have "Max {x. P x} \<in> {x. P x}" 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1101 
using Max_in x by auto 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1102 
then show ?thesis 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1103 
by (simp add: \<open>finite {x. P x}\<close> that) 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1104 
qed 
223b2ebdda79
Many new theorems, and more tidying
paulson <lp15@cam.ac.uk>
parents:
64272
diff
changeset

1105 

56328  1106 

60758  1107 
text\<open>Any subset of an interval of natural numbers the size of the 
1108 
subset is exactly that interval.\<close> 

24853  1109 

1110 
lemma subset_card_intvl_is_intvl: 

55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54606
diff
changeset

1111 
assumes "A \<subseteq> {k..<k + card A}" 
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54606
diff
changeset

1112 
shows "A = {k..<k + card A}" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1113 
proof (cases "finite A") 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1114 
case True 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1115 
from this and assms show ?thesis 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1116 
proof (induct A rule: finite_linorder_max_induct) 
24853  1117 
case empty thus ?case by auto 
1118 
next 

33434  1119 
case (insert b A) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1120 
hence *: "b \<notin> A" by auto 
55085
0e8e4dc55866
moved 'fundef_cong' attribute (and other basic 'fun' stuff) up the dependency chain
blanchet
parents:
54606
diff
changeset

1121 
with insert have "A <= {k..<k + card A}" and "b = k + card A" 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1122 
by fastforce+ 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1123 
with insert * show ?case by auto 
24853  1124 
qed 
1125 
next 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1126 
case False 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

1127 
with assms show ?thesis by simp 
24853  1128 
qed 
1129 

1130 

60758  1131 
subsubsection \<open>Proving Inclusions and Equalities between Unions\<close> 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1132 

36755  1133 
lemma UN_le_eq_Un0: 
1134 
"(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B") 

1135 
proof 

1136 
show "?A <= ?B" 

1137 
proof 

1138 
fix x assume "x : ?A" 

1139 
then obtain i where i: "i\<le>n" "x : M i" by auto 

1140 
show "x : ?B" 

1141 
proof(cases i) 

1142 
case 0 with i show ?thesis by simp 

1143 
next 

1144 
case (Suc j) with i show ?thesis by auto 

1145 
qed 

1146 
qed 

1147 
next 

63171  1148 
show "?B <= ?A" by fastforce 
36755  1149 
qed 
1150 

1151 
lemma UN_le_add_shift: 

1152 
"(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B") 

1153 
proof 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44008
diff
changeset

1154 
show "?A <= ?B" by fastforce 
36755  1155 
next 
1156 
show "?B <= ?A" 

1157 
proof 

1158 
fix x assume "x : ?B" 

1159 
then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto 

1160 
hence "ik\<le>n & x : M((ik)+k)" by auto 

1161 
thus "x : ?A" by blast 

1162 
qed 

1163 
qed 

1164 

62369  1165 
lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" 
1166 
by (auto simp add: atLeast0LessThan) 

32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1167 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1168 
lemma UN_finite_subset: 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1169 
"(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> C) \<Longrightarrow> (\<Union>n. A n) \<subseteq> C" 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1170 
by (subst UN_UN_finite_eq [symmetric]) blast 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1171 

62369  1172 
lemma UN_finite2_subset: 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1173 
assumes "\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1174 
shows "(\<Union>n. A n) \<subseteq> (\<Union>n. B n)" 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1175 
proof (rule UN_finite_subset, rule) 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1176 
fix n and a 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1177 
from assms have "(\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n + k}. B i)" . 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1178 
moreover assume "a \<in> (\<Union>i\<in>{0..<n}. A i)" 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1179 
ultimately have "a \<in> (\<Union>i\<in>{0..<n + k}. B i)" by blast 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1180 
then show "a \<in> (\<Union>i. B i)" by (auto simp add: UN_UN_finite_eq) 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1181 
qed 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1182 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1183 
lemma UN_finite2_eq: 
62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1184 
"(\<And>n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n + k}. B i)) \<Longrightarrow> 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1185 
(\<Union>n. A n) = (\<Union>n. B n)" 
33044  1186 
apply (rule subset_antisym) 
1187 
apply (rule UN_finite2_subset, blast) 

62343
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1188 
apply (rule UN_finite2_subset [where k=k]) 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1189 
apply (force simp add: atLeastLessThan_add_Un [of 0]) 
24106dc44def
prefer abbreviations for compound operators INFIMUM and SUPREMUM
haftmann
parents:
62128
diff
changeset

1190 
done 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1191 

bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1192 

60758  1193 
subsubsection \<open>Cardinality\<close> 
14485  1194 

15045  1195 
lemma card_lessThan [simp]: "card {..<u} = u" 
15251  1196 
by (induct u, simp_all add: lessThan_Suc) 
14485  1197 

1198 
lemma card_atMost [simp]: "card {..u} = Suc u" 

1199 
by (simp add: lessThan_Suc_atMost [THEN sym]) 

1200 

15045  1201 
lemma card_atLeastLessThan [simp]: "card {l..<u} = u  l" 
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1202 
proof  
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1203 
have "{l..<u} = (%x. x + l) ` {..<ul}" 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1204 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1205 
apply (rule_tac x = "x  l" in exI) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1206 
apply arith 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1207 
done 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1208 
then have "card {l..<u} = card {..<ul}" 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1209 
by (simp add: card_image inj_on_def) 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1210 
then show ?thesis 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1211 
by simp 
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset

1212 
qed 
14485  1213 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

1214 
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u  l" 
14485  1215 
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) 
1216 

15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset

1217 
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u  l" 
14485  1218 
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) 
1219 

15045  1220 
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u  Suc l" 
14485  1221 
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) 
1222 

63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1223 
lemma subset_eq_atLeast0_lessThan_finite: 
63365  1224 
fixes n :: nat 
63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1225 
assumes "N \<subseteq> {0..<n}" 
63915  1226 
shows "finite N" 
63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1227 
using assms finite_atLeastLessThan by (rule finite_subset) 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1228 

c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1229 
lemma subset_eq_atLeast0_atMost_finite: 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1230 
fixes n :: nat 
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1231 
assumes "N \<subseteq> {0..n}" 
63915  1232 
shows "finite N" 
63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63365
diff
changeset

1233 
using assms finite_atLeastAtMost by (rule finite_subset) 
63365  1234 

26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1235 
lemma ex_bij_betw_nat_finite: 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1236 
"finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M" 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1237 
apply(drule finite_imp_nat_seg_image_inj_on) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1238 
apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1239 
done 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1240 

ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1241 
lemma ex_bij_betw_finite_nat: 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1242 
"finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}" 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1243 
by (blast dest: ex_bij_betw_nat_finite bij_betw_inv) 
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1244 

31438  1245 
lemma finite_same_card_bij: 
1246 
"finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B" 

1247 
apply(drule ex_bij_betw_finite_nat) 

1248 
apply(drule ex_bij_betw_nat_finite) 

1249 
apply(auto intro!:bij_betw_trans) 

1250 
done 

1251 

1252 
lemma ex_bij_betw_nat_finite_1: 

1253 
"finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M" 

1254 
by (rule finite_same_card_bij) auto 

1255 

40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1256 
lemma bij_betw_iff_card: 
63114
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1257 
assumes "finite A" "finite B" 
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1258 
shows "(\<exists>f. bij_betw f A B) \<longleftrightarrow> (card A = card B)" 
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1259 
proof 
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1260 
assume "card A = card B" 
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1261 
moreover obtain f where "bij_betw f A {0 ..< card A}" 
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1262 
using assms ex_bij_betw_finite_nat by blast 
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1263 
moreover obtain g where "bij_betw g {0 ..< card B} B" 
63114
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1264 
using assms ex_bij_betw_nat_finite by blast 
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1265 
ultimately have "bij_betw (g o f) A B" 
63114
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1266 
by (auto simp: bij_betw_trans) 
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1267 
thus "(\<exists>f. bij_betw f A B)" by blast 
63114
27afe7af7379
Lots of new material for multivariate analysis
paulson <lp15@cam.ac.uk>
parents:
63099
diff
changeset

1268 
qed (auto simp: bij_betw_same_card) 
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1269 

d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1270 
lemma inj_on_iff_card_le: 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1271 
assumes FIN: "finite A" and FIN': "finite B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1272 
shows "(\<exists>f. inj_on f A \<and> f ` A \<le> B) = (card A \<le> card B)" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1273 
proof (safe intro!: card_inj_on_le) 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1274 
assume *: "card A \<le> card B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1275 
obtain f where 1: "inj_on f A" and 2: "f ` A = {0 ..< card A}" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1276 
using FIN ex_bij_betw_finite_nat unfolding bij_betw_def by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1277 
moreover obtain g where "inj_on g {0 ..< card B}" and 3: "g ` {0 ..< card B} = B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1278 
using FIN' ex_bij_betw_nat_finite unfolding bij_betw_def by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1279 
ultimately have "inj_on g (f ` A)" using subset_inj_on[of g _ "f ` A"] * by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
