author  paulson <lp15@cam.ac.uk> 
Mon, 23 May 2016 15:33:24 +0100  
changeset 63114  27afe7af7379 
parent 63099  af0e964aad7b 
child 63171  a0088f1c049d 
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 
55088
57c82e01022b
moved 'bacc' back to 'Enum' (cf. 744934b818c7)  reduces baggage loaded by 'Hilbert_Choice'
blanchet
parents:
55085
diff
changeset

17 
imports Lattices_Big 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 

133 
lemma atLeast_subset_iff [iff]: 

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

134 
"(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

135 
by (blast intro: order_trans) 
13850  136 

137 
lemma atLeast_eq_iff [iff]: 

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

138 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  139 
by (blast intro: order_antisym order_trans) 
140 

141 
lemma greaterThan_subset_iff [iff]: 

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

142 
"(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

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

144 
apply (subst linorder_not_less [symmetric], blast) 
13850  145 
done 
146 

147 
lemma greaterThan_eq_iff [iff]: 

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

148 
"(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

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

150 
apply (erule equalityE) 
29709  151 
apply simp_all 
13850  152 
done 
153 

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

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

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

157 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  158 
by (blast intro: order_antisym order_trans) 
159 

160 
lemma lessThan_subset_iff [iff]: 

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

161 
"(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

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

163 
apply (subst linorder_not_less [symmetric], blast) 
13850  164 
done 
165 

166 
lemma lessThan_eq_iff [iff]: 

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

167 
"(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

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

169 
apply (erule equalityE) 
29709  170 
apply simp_all 
13735  171 
done 
172 

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

173 
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

174 
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

175 
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

176 
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) 
13735  177 

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

178 
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

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

180 

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

181 
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

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

183 

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

186 

60758  187 
subsection \<open>Twosided intervals\<close> 
13735  188 

24691  189 
context ord 
190 
begin 

191 

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

192 
lemma greaterThanLessThan_iff [simp]: 
25062  193 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  194 
by (simp add: greaterThanLessThan_def) 
195 

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

196 
lemma atLeastLessThan_iff [simp]: 
25062  197 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  198 
by (simp add: atLeastLessThan_def) 
199 

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

200 
lemma greaterThanAtMost_iff [simp]: 
25062  201 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  202 
by (simp add: greaterThanAtMost_def) 
203 

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

204 
lemma atLeastAtMost_iff [simp]: 
25062  205 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  206 
by (simp add: atLeastAtMost_def) 
207 

60758  208 
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

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

211 

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

214 

24691  215 
end 
13735  216 

60758  217 
subsubsection\<open>Emptyness, singletons, subset\<close> 
15554  218 

24691  219 
context order 
220 
begin 

15554  221 

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

224 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

225 

226 
lemma atLeastatMost_empty_iff[simp]: 

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

228 
by auto (blast intro: order_trans) 

229 

230 
lemma atLeastatMost_empty_iff2[simp]: 

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

232 
by auto (blast intro: order_trans) 

233 

234 
lemma atLeastLessThan_empty[simp]: 

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

236 
by(auto simp: atLeastLessThan_def) 

24691  237 

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

240 
by auto (blast intro: le_less_trans) 

241 

242 
lemma atLeastLessThan_empty_iff2[simp]: 

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

244 
by auto (blast intro: le_less_trans) 

15554  245 

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

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

251 

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

253 
by auto (blast intro: less_le_trans) 

254 

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

25062  258 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  259 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
260 

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

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

262 

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

265 
unfolding atLeastAtMost_def atLeast_def atMost_def 

266 
by (blast intro: order_trans) 

267 

268 
lemma atLeastatMost_psubset_iff: 

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

270 
((~ 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

271 
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 
32400  272 

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

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

276 

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

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

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

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

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

281 
hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp 
60758  282 
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

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

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

285 

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

288 
by(auto simp: subset_eq intro: order_trans) 

289 

290 
lemma Icc_subset_Iic_iff[simp]: 

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

292 
by(auto simp: subset_eq intro: order_trans) 

293 

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

295 
by(auto simp: set_eq_iff) 

296 

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

298 
by(auto simp: set_eq_iff) 

299 

300 
lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] 

301 
lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] 

302 

24691  303 
end 
14485  304 

51334  305 
context no_top 
306 
begin 

307 

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

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

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

311 

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

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

314 

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

316 
using gt_ex[of h'] 

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

318 

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

320 
using gt_ex[of h'] 

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

322 

323 
end 

324 

325 
context no_bot 

326 
begin 

327 

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

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

330 

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

332 
using lt_ex[of l'] 

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

334 

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

336 
using lt_ex[of l'] 

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

338 

339 
end 

340 

341 

342 
context no_top 

343 
begin 

344 

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

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

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

348 

349 
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] 

350 

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

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

353 

354 
lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] 

355 

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

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

358 

359 
lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] 

360 

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

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

363 
using not_Ici_le_Iic[of l' h] by blast 

364 

365 
lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] 

366 

367 
end 

368 

369 
context no_bot 

370 
begin 

371 

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

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

374 

375 
lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] 

376 

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

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

379 

380 
lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] 

381 

382 
end 

383 

384 

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

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

387 

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

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

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

390 
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

391 

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

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

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

394 
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

395 

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

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

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

400 

401 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

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

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

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

405 

406 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

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

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

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

410 

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

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

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

62369  415 

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

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

417 
"{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

418 
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

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

421 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

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

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

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

425 

426 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

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

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

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

430 

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

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

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

435 

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

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

437 

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

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

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

440 

51334  441 
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

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

443 

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

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

445 

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

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

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

448 

51334  449 
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

450 
using lt_ex[of x] by auto 
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 
end 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

453 

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

456 
apply (auto simp:subset_eq Ball_def) 

457 
apply(frule_tac x=a in spec) 

458 
apply(erule_tac x=d in allE) 

459 
apply (simp add: less_imp_le) 

460 
done 

461 

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

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

463 
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

464 
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

465 
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

466 
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

467 

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

468 
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

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 "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 ..< 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

472 
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

473 

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

474 
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

475 
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

476 

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

477 
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

478 
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

479 

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_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

481 
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

482 

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

483 
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" 
51334  484 
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

485 

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

486 
lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top" 
51334  487 
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

488 

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

491 
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

492 

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

495 

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

497 
by (simp add: Iio_eq_empty_iff bot_nat_def) 

498 

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

501 
shows "f m = m'" 

502 
proof  

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

504 
by (metis atLeastLessThan_empty_iff image_is_empty) 

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

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

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

508 
ultimately show "f m = m'" 

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

510 
qed 

511 

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

512 

60758  513 
subsection \<open>Infinite intervals\<close> 
56328  514 

515 
context dense_linorder 

516 
begin 

517 

518 
lemma infinite_Ioo: 

519 
assumes "a < b" 

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

521 
proof 

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

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

60758  524 
using \<open>a < b\<close> by auto 
56328  525 
ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" 
526 
using Max_in[of "{a <..< b}"] by auto 

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

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

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

60758  530 
using \<open>a < Max {a <..< b}\<close> by auto 
56328  531 
then have "x \<le> Max {a <..< b}" 
532 
using fin by auto 

60758  533 
with \<open>Max {a <..< b} < x\<close> show False by auto 
56328  534 
qed 
535 

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

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

538 
by (auto dest: finite_subset) 

539 

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

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

542 
by (auto dest: finite_subset) 

543 

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

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

546 
by (auto dest: finite_subset) 

547 

548 
end 

549 

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

551 
proof 

552 
assume "finite {..< a}" 

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

554 
by auto 

555 
obtain x where "x < a" 

556 
using lt_ex by auto 

557 

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

559 
using lt_ex by auto 

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

60758  561 
using \<open>x < a\<close> by fact 
562 
also note \<open>x < a\<close> 

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

60758  565 
with \<open>y < Min {..< a}\<close> show False by auto 
56328  566 
qed 
567 

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

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

570 
by (auto simp: subset_eq less_imp_le) 

571 

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

573 
proof 

574 
assume "finite {a <..}" 

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

576 
by auto 

577 

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

579 
using gt_ex by auto 

580 

581 
obtain x where "a < x" 

582 
using gt_ex by auto 

583 
also then have "x \<le> Max {a <..}" 

584 
by fact 

60758  585 
also note \<open>Max {a <..} < y\<close> 
56328  586 
finally have "y \<le> Max { a <..}" 
587 
by fact 

60758  588 
with \<open>Max {a <..} < y\<close> show False by auto 
56328  589 
qed 
590 

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

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

593 
by (auto simp: subset_eq less_imp_le) 

594 

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

596 

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

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

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

599 

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

600 
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

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

602 

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

603 
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

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

605 

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

606 
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

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

608 

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

609 
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

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

611 

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

612 
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

613 
by auto 
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 
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

616 
by auto 
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_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

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_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

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

623 

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

626 

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

627 
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  628 
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

629 

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

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

631 

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

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

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

634 

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

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

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

637 
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

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

639 
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

640 
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

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

642 

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

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

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

645 
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

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

647 
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

648 
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

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

650 

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

651 
end 
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 
53216  654 
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

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

656 
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

657 
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

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

659 
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

660 
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

661 
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

662 

60758  663 
subsection \<open>Intervals of natural numbers\<close> 
14485  664 

60758  665 
subsubsection \<open>The Constant @{term lessThan}\<close> 
15047  666 

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

669 

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

671 
by (simp add: lessThan_def less_Suc_eq, blast) 

672 

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

59000  677 
lemma zero_notin_Suc_image: "0 \<notin> Suc ` A" 
678 
by auto 

679 

39072  680 
lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})" 
59000  681 
by (auto simp: image_iff less_Suc_eq_0_disj) 
39072  682 

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

685 

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

688 

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

691 

60758  692 
subsubsection \<open>The Constant @{term greaterThan}\<close> 
15047  693 

14485  694 
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" 
695 
apply (simp add: greaterThan_def) 

696 
apply (blast dest: gr0_conv_Suc [THEN iffD1]) 

697 
done 

698 

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

700 
apply (simp add: greaterThan_def) 

701 
apply (auto elim: linorder_neqE) 

702 
done 

703 

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

705 
by blast 

706 

60758  707 
subsubsection \<open>The Constant @{term atLeast}\<close> 
15047  708 

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

711 

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

713 
apply (simp add: atLeast_def) 

714 
apply (simp add: Suc_le_eq) 

715 
apply (simp add: order_le_less, blast) 

716 
done 

717 

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

719 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

720 

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

722 
by blast 

723 

60758  724 
subsubsection \<open>The Constant @{term atMost}\<close> 
15047  725 

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

728 

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

730 
apply (simp add: atMost_def) 

731 
apply (simp add: less_Suc_eq order_le_less, blast) 

732 
done 

733 

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

735 
by blast 

736 

60758  737 
subsubsection \<open>The Constant @{term atLeastLessThan}\<close> 
15047  738 

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

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

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

60758  744 
specific concept to a more general one.\<close> 
28068  745 

15047  746 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  747 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  748 

28068  749 
lemma atLeast0AtMost: "{0..n::nat} = {..n}" 
750 
by(simp add:atMost_def atLeastAtMost_def) 

751 

31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset

752 
declare atLeast0LessThan[symmetric, code_unfold] 
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset

753 
atLeast0AtMost[symmetric, code_unfold] 
24449  754 

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

15047  756 
by (simp add: atLeastLessThan_def) 
24449  757 

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

60758  760 
text\<open>Not a simprule because the RHS is too messy.\<close> 
15047  761 
lemma atLeastLessThanSuc: 
762 
"{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

763 
by (auto simp add: atLeastLessThan_def) 
15047  764 

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

765 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  766 
by (auto simp add: atLeastLessThan_def) 
16041  767 
(* 
15047  768 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
769 
by (induct k, simp_all add: atLeastLessThanSuc) 

770 

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

772 
by (auto simp add: atLeastLessThan_def) 

16041  773 
*) 
15045  774 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  775 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
776 

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

777 
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

778 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  779 
greaterThanAtMost_def) 
780 

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

781 
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

782 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  783 
greaterThanLessThan_def) 
784 

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

787 

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

790 

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

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

795 
by (auto intro: set_eqI) 

796 

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

33044  800 
done 
801 

60758  802 
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

803 

61799  804 
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

805 
"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

806 
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

807 

61799  808 
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

809 
"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

810 
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

811 

61799  812 
lemma atLeastLessThan_nat_numeral: \<comment>\<open>Evaluation for specific numerals\<close> 
62369  813 
"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

814 
(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

815 
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

816 
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

817 

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

819 

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

820 
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

821 
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

822 
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

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

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

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

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

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

828 
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

829 
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

830 
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

831 
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

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

833 
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

834 
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

835 
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

836 
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

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

838 
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

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

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

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

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

843 

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

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

845 
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

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

847 
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

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

849 

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

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

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

852 
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

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

854 
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

855 

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

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

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

858 
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

859 
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

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

861 
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

862 
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

863 
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

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

865 

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

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

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

868 
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

869 
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

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

871 
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

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

873 

61204  874 
lemma image_affinity_atLeastAtMost_div: 
875 
fixes c :: "'a::linordered_field" 

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

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

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

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

880 
by (simp add: field_class.field_divide_inverse algebra_simps) 

62369  881 

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

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

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

884 
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

885 
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

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

887 
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

888 
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

889 

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

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

891 
"(%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

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

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

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

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

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

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

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

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

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

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

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

903 

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

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

905 
"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

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

907 

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

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

909 
"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

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

911 

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

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

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

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

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

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

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

918 

37664  919 
lemma image_minus_const_atLeastLessThan_nat: 
920 
fixes c :: nat 

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

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

923 
(is "_ = ?right") 

924 
proof safe 

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

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

927 
proof cases 

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

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

930 
next 

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

62390  932 
by (auto intro!: image_eqI[of _ _ x] split: if_split_asm) 
37664  933 
qed 
934 
qed auto 

935 

51152  936 
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

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

35580  939 
context ordered_ab_group_add 
940 
begin 

941 

942 
lemma 

943 
fixes x :: 'a 

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

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

946 
proof safe 

947 
fix y assume "y < x" 

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

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

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

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

952 
next 

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

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

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

958 

959 
lemma 

960 
fixes x :: 'a 

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

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

963 
proof  

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

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

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

967 
by (simp_all add: image_image 

968 
del: image_uminus_greaterThan image_uminus_atLeast) 

969 
qed 

970 

971 
lemma 

972 
fixes x :: 'a 

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

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

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

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

977 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

978 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

979 
end 

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

980 

60758  981 
subsubsection \<open>Finiteness\<close> 
14485  982 

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

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

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

988 

989 
lemma finite_greaterThanLessThan [iff]: 

15045  990 
fixes l :: nat shows "finite {l<..<u}" 
14485  991 
by (simp add: greaterThanLessThan_def) 
992 

993 
lemma finite_atLeastLessThan [iff]: 

15045  994 
fixes l :: nat shows "finite {l..<u}" 
14485  995 
by (simp add: atLeastLessThan_def) 
996 

997 
lemma finite_greaterThanAtMost [iff]: 

15045  998 
fixes l :: nat shows "finite {l<..u}" 
14485  999 
by (simp add: greaterThanAtMost_def) 
1000 

1001 
lemma finite_atLeastAtMost [iff]: 

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

1003 
by (simp add: atLeastAtMost_def) 

1004 

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

1010 
done 

1011 

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

1015 
proof 

1016 
assume f:?F show ?B 

60758  1017 
using Max_ge[OF \<open>?F\<close>, simplified less_Suc_eq_le[symmetric]] by blast 
31044  1018 
next 
60758  1019 
assume ?B show ?F using \<open>?B\<close> by(blast intro:bounded_nat_set_is_finite) 
31044  1020 
qed 
1021 

1022 
lemma finite_nat_set_iff_bounded_le: 

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

1024 
apply(simp add:finite_nat_set_iff_bounded) 

1025 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

1026 
done 

1027 

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

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

14485  1031 

56328  1032 

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

24853  1035 

1036 
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

1037 
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

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

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

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

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

1042 
proof (induct A rule: finite_linorder_max_induct) 
24853  1043 
case empty thus ?case by auto 
1044 
next 

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

1046 
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

1047 
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

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

1049 
with insert * show ?case by auto 
24853  1050 
qed 
1051 
next 

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

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

1053 
with assms show ?thesis by simp 
24853  1054 
qed 
1055 

1056 

60758  1057 
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

1058 

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

1061 
proof 

1062 
show "?A <= ?B" 

1063 
proof 

1064 
fix x assume "x : ?A" 

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

1066 
show "x : ?B" 

1067 
proof(cases i) 

1068 
case 0 with i show ?thesis by simp 

1069 
next 

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

1071 
qed 

1072 
qed 

1073 
next 

1074 
show "?B <= ?A" by auto 

1075 
qed 

1076 

1077 
lemma UN_le_add_shift: 

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

1079 
proof 

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

1080 
show "?A <= ?B" by fastforce 
36755  1081 
next 
1082 
show "?B <= ?A" 

1083 
proof 

1084 
fix x assume "x : ?B" 

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

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

1087 
thus "x : ?A" by blast 

1088 
qed 

1089 
qed 

1090 

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

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

1093 

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

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

1095 
"(\<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

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

1097 

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

1099 
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

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

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

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

1103 
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

1104 
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

1105 
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

1106 
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

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

1108 

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

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

1110 
"(\<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

1111 
(\<Union>n. A n) = (\<Union>n. B n)" 
33044  1112 
apply (rule subset_antisym) 
1113 
apply (rule UN_finite2_subset, blast) 

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

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

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

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

1117 

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

1118 

60758  1119 
subsubsection \<open>Cardinality\<close> 
14485  1120 

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

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

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

1126 

15045  1127 
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

1128 
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

1129 
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

1130 
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

1131 
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

1132 
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

1133 
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

1134 
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

1135 
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

1136 
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

1137 
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

1138 
qed 
14485  1139 

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

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

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

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

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

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

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

1150 
"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

1151 
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

1152 
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

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

1154 

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

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

1156 
"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

1157 
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

1158 

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

1161 
apply(drule ex_bij_betw_finite_nat) 

1162 
apply(drule ex_bij_betw_nat_finite) 

1163 
apply(auto intro!:bij_betw_trans) 

1164 
done 

1165 

1166 
lemma ex_bij_betw_nat_finite_1: 

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

1168 
by (rule finite_same_card_bij) auto 

1169 

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

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

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

1172 
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

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

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

1175 
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

1176 
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

1177 
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

1178 
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

1179 
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

1180 
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

1181 
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

1182 
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

1183 

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

1184 
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

1185 
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

1186 
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

1187 
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

1188 
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

1189 
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

1190 
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

1191 
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

1192 
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

1193 
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
diff
changeset

1194 
hence "inj_on (g o f) A" using 1 comp_inj_on by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

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

1196 
{have "{0 ..< card A} \<le> {0 ..< card B}" using * by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1197 
with 2 have "f ` A \<le> {0 ..< card B}" by blast 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

1198 
hence "(g o f) ` A \<le> B" unfolding comp_def using 3 by force 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

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

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

1201 
qed (insert assms, auto) 
26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset

1202 

60758  1203 
subsection \<open>Intervals of integers\<close> 
14485  1204 

15045  1205 
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" 
14485  1206 
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) 
1207 

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

1208 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  1209 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
1210 

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

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

1212 
"{l+1..<u} = {l<..<u::int}" 
14485  1213 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
1214 

60758  1215 
subsubsection \<open>Finiteness\<close> 
14485  1216 

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

1217 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  1218 
{(0::int)..<u} = int ` {..<nat u}" 
14485  1219 
apply (unfold image_def lessThan_def) 
1220 
apply auto 

1221 
apply (rule_tac x = "nat x" in exI) 

35216  1222 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  1223 
done 
1224 

15045  1225 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
47988  1226 
apply (cases "0 \<le> u") 
14485  1227 
apply (subst image_atLeastZeroLessThan_int, assumption) 
1228 
apply (rule finite_imageI) 

1229 
apply auto 

1230 
done 

1231 

15045  1232 
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" 
1233 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 

14485  1234 
apply (erule subst) 
1235 
apply (rule finite_imageI) 

1236 
apply (rule finite_atLeastZeroLessThan_int) 

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

1237 
apply (rule image_add_int_atLeastLessThan) 
14485  1238 
done 
1239 

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

1240 
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" 
14485  1241 
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) 
1242 

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

1243 
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" 
14485  1244 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
1245 

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

1246 
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" 
14485  1247 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
1248 

24853  1249 

60758  1250 
subsubsection \<open>Cardinality\<close> 
14485  1251 

15045  1252 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
47988  1253 
apply (cases "0 \<le> u") 
14485  1254 
apply (subst image_atLeastZeroLessThan_int, assumption) 
1255 
apply (subst card_image) 

1256 
apply (auto simp add: inj_on_def) 

1257 
done 

1258 

15045  1259 
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u  l)" 
1260 
apply (subgoal_tac "card {l..<u} = card {0..<ul}") 

14485  1261 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  1262 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  1263 
apply (erule subst) 
1264 
apply (rule card_image) 

1265 
apply (simp add: inj_on_def) 

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

1266 
apply (rule image_add_int_atLeastLessThan) 
14485  1267 
done 
1268 

1269 
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u  l + 1)" 

29667  1270 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
1271 
apply (auto simp add: algebra_simps) 

1272 
done 

14485  1273 

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

1274 
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u  l)" 
29667  1275 
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) 
14485  1276 

15045  1277 
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u  (l + 1))" 
29667  1278 
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) 
14485  1279 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1280 
lemma finite_M_bounded_by_nat: "finite {k. P k \<and> k < (i::nat)}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1281 
proof  
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1282 
have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto 