author  paulson <lp15@cam.ac.uk> 
Thu, 29 May 2014 14:39:19 +0100  
changeset 57113  7e95523302e6 
parent 56949  d1a937cbf858 
child 57129  7edb7550663e 
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 

14577  14 
header {* Set intervals *} 
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 

15048  58 
text{* A note of warning when using @{term"{..<n}"} on type @{typ 
59 
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving 

15052  60 
@{term"{m..<n}"} may not exist in @{term"{..<n}"}form as well. *} 
15048  61 

14418  62 
syntax 
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 (xsymbols) 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

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

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

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

72 
"_INTER_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter> _<_./ _)" [0, 0, 10] 10) 
14418  73 

30372  74 
syntax (latex output) 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

75 
"_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

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

77 
"_INTER_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10) 
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

78 
"_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10) 
14418  79 

80 
translations 

81 
"UN i<=n. A" == "UN i:{..n}. A" 

15045  82 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  83 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  84 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  85 

86 

14485  87 
subsection {* Various equivalences *} 
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 

14485  131 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
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 

13850  178 
subsection {*Twosided intervals*} 
13735  179 

24691  180 
context ord 
181 
begin 

182 

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

183 
lemma greaterThanLessThan_iff [simp]: 
25062  184 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  185 
by (simp add: greaterThanLessThan_def) 
186 

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

187 
lemma atLeastLessThan_iff [simp]: 
25062  188 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  189 
by (simp add: atLeastLessThan_def) 
190 

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

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

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

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

32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

199 
text {* 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

200 
breaks many proofs. Since it only helps blast, it is better to leave them 
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset

201 
alone. *} 
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

202 

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

205 

24691  206 
end 
13735  207 

32400  208 
subsubsection{* Emptyness, singletons, subset *} 
15554  209 

24691  210 
context order 
211 
begin 

15554  212 

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

215 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

216 

217 
lemma atLeastatMost_empty_iff[simp]: 

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

219 
by auto (blast intro: order_trans) 

220 

221 
lemma atLeastatMost_empty_iff2[simp]: 

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

223 
by auto (blast intro: order_trans) 

224 

225 
lemma atLeastLessThan_empty[simp]: 

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

227 
by(auto simp: atLeastLessThan_def) 

24691  228 

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

231 
by auto (blast intro: le_less_trans) 

232 

233 
lemma atLeastLessThan_empty_iff2[simp]: 

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

235 
by auto (blast intro: le_less_trans) 

15554  236 

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

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

242 

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

244 
by auto (blast intro: less_le_trans) 

245 

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

25062  249 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  250 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
251 

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

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

253 

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

256 
unfolding atLeastAtMost_def atLeast_def atMost_def 

257 
by (blast intro: order_trans) 

258 

259 
lemma atLeastatMost_psubset_iff: 

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

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

262 
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 
32400  263 

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

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

267 

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

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

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

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

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

272 
hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

273 
with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset

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

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

276 

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

279 
by(auto simp: subset_eq intro: order_trans) 

280 

281 
lemma Icc_subset_Iic_iff[simp]: 

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

283 
by(auto simp: subset_eq intro: order_trans) 

284 

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

286 
by(auto simp: set_eq_iff) 

287 

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

289 
by(auto simp: set_eq_iff) 

290 

291 
lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] 

292 
lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] 

293 

24691  294 
end 
14485  295 

51334  296 
context no_top 
297 
begin 

298 

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

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

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

302 

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

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

305 

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

307 
using gt_ex[of h'] 

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

309 

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

311 
using gt_ex[of h'] 

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

313 

314 
end 

315 

316 
context no_bot 

317 
begin 

318 

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

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

321 

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

323 
using lt_ex[of l'] 

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

325 

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

327 
using lt_ex[of l'] 

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

329 

330 
end 

331 

332 

333 
context no_top 

334 
begin 

335 

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

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

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

339 

340 
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] 

341 

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

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

344 

345 
lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] 

346 

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

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

349 

350 
lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] 

351 

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

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

354 
using not_Ici_le_Iic[of l' h] by blast 

355 

356 
lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] 

357 

358 
end 

359 

360 
context no_bot 

361 
begin 

362 

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

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

365 

366 
lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] 

367 

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

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

370 

371 
lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] 

372 

373 
end 

374 

375 

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

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

378 

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

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

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

381 
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

382 

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

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

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

385 
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

386 

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

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

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

391 

392 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

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

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

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

396 

397 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

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

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

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

401 

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

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

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

406 

407 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

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

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

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

411 

412 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

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

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

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

416 

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

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

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

421 

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

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

423 

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

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

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

426 

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

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

429 

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

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

431 

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

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

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

434 

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

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

437 

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

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

439 

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

442 
apply (auto simp:subset_eq Ball_def) 

443 
apply(frule_tac x=a in spec) 

444 
apply(erule_tac x=d in allE) 

445 
apply (simp add: less_imp_le) 

446 
done 

447 

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

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

449 
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

450 
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

451 
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

452 
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

453 

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

454 
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

455 
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

456 
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

457 
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

458 
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

459 

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

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

462 

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

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

465 

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

468 
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

469 

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

472 

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

474 
by (simp add: Iio_eq_empty_iff bot_nat_def) 

475 

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

476 

56328  477 
subsection {* Infinite intervals *} 
478 

479 
context dense_linorder 

480 
begin 

481 

482 
lemma infinite_Ioo: 

483 
assumes "a < b" 

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

485 
proof 

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

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

488 
using `a < b` by auto 

489 
ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" 

490 
using Max_in[of "{a <..< b}"] by auto 

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

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

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

494 
using `a < Max {a <..< b}` by auto 

495 
then have "x \<le> Max {a <..< b}" 

496 
using fin by auto 

497 
with `Max {a <..< b} < x` show False by auto 

498 
qed 

499 

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

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

502 
by (auto dest: finite_subset) 

503 

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

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

506 
by (auto dest: finite_subset) 

507 

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

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

510 
by (auto dest: finite_subset) 

511 

512 
end 

513 

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

515 
proof 

516 
assume "finite {..< a}" 

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

518 
by auto 

519 
obtain x where "x < a" 

520 
using lt_ex by auto 

521 

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

523 
using lt_ex by auto 

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

525 
using `x < a` by fact 

526 
also note `x < a` 

527 
finally have "Min {..< a} \<le> y" 

528 
by fact 

529 
with `y < Min {..< a}` show False by auto 

530 
qed 

531 

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

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

534 
by (auto simp: subset_eq less_imp_le) 

535 

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

537 
proof 

538 
assume "finite {a <..}" 

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

540 
by auto 

541 

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

543 
using gt_ex by auto 

544 

545 
obtain x where "a < x" 

546 
using gt_ex by auto 

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

548 
by fact 

549 
also note `Max {a <..} < y` 

550 
finally have "y \<le> Max { a <..}" 

551 
by fact 

552 
with `Max {a <..} < y` show False by auto 

553 
qed 

554 

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

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

557 
by (auto simp: subset_eq less_imp_le) 

558 

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

559 
subsubsection {* Intersection *} 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

560 

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

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

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

563 

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

564 
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

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

566 

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

567 
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

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

569 

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

570 
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

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

572 

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

573 
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

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

575 

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

576 
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

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

578 

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

579 
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

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

581 

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

582 
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

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

584 

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

585 
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

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

587 

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

590 

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

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

592 

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

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

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

595 

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

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

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

598 
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

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

600 
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

601 
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

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

603 

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

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

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

606 
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

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

608 
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

609 
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

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

611 

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

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

613 

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

614 
lemma 
53216  615 
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

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

617 
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

618 
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

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

620 
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

621 
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

622 
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

623 

14485  624 
subsection {* Intervals of natural numbers *} 
625 

15047  626 
subsubsection {* The Constant @{term lessThan} *} 
627 

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

630 

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

632 
by (simp add: lessThan_def less_Suc_eq, blast) 

633 

43156  634 
text {* The following proof is convenient in induction proofs where 
39072  635 
new elements get indices at the beginning. So it is used to transform 
636 
@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}. *} 

637 

638 
lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})" 

639 
proof safe 

640 
fix x assume "x < Suc n" "x \<notin> Suc ` {..<n}" 

641 
then have "x \<noteq> Suc (x  1)" by auto 

642 
with `x < Suc n` show "x = 0" by auto 

643 
qed 

644 

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

647 

648 
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" 

649 
by blast 

650 

15047  651 
subsubsection {* The Constant @{term greaterThan} *} 
652 

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

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

656 
done 

657 

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

659 
apply (simp add: greaterThan_def) 

660 
apply (auto elim: linorder_neqE) 

661 
done 

662 

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

664 
by blast 

665 

15047  666 
subsubsection {* The Constant @{term atLeast} *} 
667 

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

670 

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

672 
apply (simp add: atLeast_def) 

673 
apply (simp add: Suc_le_eq) 

674 
apply (simp add: order_le_less, blast) 

675 
done 

676 

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

678 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

679 

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

681 
by blast 

682 

15047  683 
subsubsection {* The Constant @{term atMost} *} 
684 

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

687 

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

689 
apply (simp add: atMost_def) 

690 
apply (simp add: less_Suc_eq order_le_less, blast) 

691 
done 

692 

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

694 
by blast 

695 

15047  696 
subsubsection {* The Constant @{term atLeastLessThan} *} 
697 

28068  698 
text{*The orientation of the following 2 rules is tricky. The lhs is 
24449  699 
defined in terms of the rhs. Hence the chosen orientation makes sense 
700 
in this theory  the reverse orientation complicates proofs (eg 

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

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

703 
specific concept to a more general one. *} 

28068  704 

15047  705 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  706 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  707 

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

710 

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

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

712 
atLeast0AtMost[symmetric, code_unfold] 
24449  713 

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

15047  715 
by (simp add: atLeastLessThan_def) 
24449  716 

15047  717 
subsubsection {* Intervals of nats with @{term Suc} *} 
718 

719 
text{*Not a simprule because the RHS is too messy.*} 

720 
lemma atLeastLessThanSuc: 

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

722 
by (auto simp add: atLeastLessThan_def) 
15047  723 

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

724 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  725 
by (auto simp add: atLeastLessThan_def) 
16041  726 
(* 
15047  727 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
728 
by (induct k, simp_all add: atLeastLessThanSuc) 

729 

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

731 
by (auto simp add: atLeastLessThan_def) 

16041  732 
*) 
15045  733 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  734 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
735 

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

736 
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

737 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  738 
greaterThanAtMost_def) 
739 

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

740 
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

741 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  742 
greaterThanLessThan_def) 
743 

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

746 

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

749 

43157  750 
text {* The analogous result is useful on @{typ int}: *} 
751 
(* here, because we don't have an own int section *) 

752 
lemma atLeastAtMostPlus1_int_conv: 

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

754 
by (auto intro: set_eqI) 

755 

33044  756 
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}" 
757 
apply (induct k) 

758 
apply (simp_all add: atLeastLessThanSuc) 

759 
done 

760 

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

761 
subsubsection {* Intervals and numerals *} 
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

762 

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

763 
lemma lessThan_nat_numeral: {*Evaluation for specific numerals*} 
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

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

765 
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

766 

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

767 
lemma atMost_nat_numeral: {*Evaluation for specific numerals*} 
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

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

769 
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

770 

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

771 
lemma atLeastLessThan_nat_numeral: {*Evaluation for specific numerals*} 
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

772 
"atLeastLessThan m (numeral k :: nat) = 
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

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

774 
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

775 
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

776 

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

777 
subsubsection {* Image *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

778 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

792 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

806 

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

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

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

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

810 

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

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

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

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

814 

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

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

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

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

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

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

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

821 

37664  822 
lemma image_minus_const_atLeastLessThan_nat: 
823 
fixes c :: nat 

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

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

826 
(is "_ = ?right") 

827 
proof safe 

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

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

830 
proof cases 

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

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

833 
next 

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

835 
by (auto intro!: image_eqI[of _ _ x] split: split_if_asm) 

836 
qed 

837 
qed auto 

838 

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

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

35580  842 
context ordered_ab_group_add 
843 
begin 

844 

845 
lemma 

846 
fixes x :: 'a 

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

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

849 
proof safe 

850 
fix y assume "y < x" 

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

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

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

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

855 
next 

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

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

858 
by (rule imageI) (insert `y \<le> x`[THEN le_imp_neg_le], simp) 

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

860 
qed simp_all 

861 

862 
lemma 

863 
fixes x :: 'a 

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

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

866 
proof  

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

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

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

870 
by (simp_all add: image_image 

871 
del: image_uminus_greaterThan image_uminus_atLeast) 

872 
qed 

873 

874 
lemma 

875 
fixes x :: 'a 

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

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

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

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

880 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

881 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

882 
end 

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

883 

14485  884 
subsubsection {* Finiteness *} 
885 

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

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

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

891 

892 
lemma finite_greaterThanLessThan [iff]: 

15045  893 
fixes l :: nat shows "finite {l<..<u}" 
14485  894 
by (simp add: greaterThanLessThan_def) 
895 

896 
lemma finite_atLeastLessThan [iff]: 

15045  897 
fixes l :: nat shows "finite {l..<u}" 
14485  898 
by (simp add: atLeastLessThan_def) 
899 

900 
lemma finite_greaterThanAtMost [iff]: 

15045  901 
fixes l :: nat shows "finite {l<..u}" 
14485  902 
by (simp add: greaterThanAtMost_def) 
903 

904 
lemma finite_atLeastAtMost [iff]: 

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

906 
by (simp add: atLeastAtMost_def) 

907 

28068  908 
text {* A bounded set of natural numbers is finite. *} 
14485  909 
lemma bounded_nat_set_is_finite: 
24853  910 
"(ALL i:N. i < (n::nat)) ==> finite N" 
28068  911 
apply (rule finite_subset) 
912 
apply (rule_tac [2] finite_lessThan, auto) 

913 
done 

914 

31044  915 
text {* A set of natural numbers is finite iff it is bounded. *} 
916 
lemma finite_nat_set_iff_bounded: 

917 
"finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B") 

918 
proof 

919 
assume f:?F show ?B 

920 
using Max_ge[OF `?F`, simplified less_Suc_eq_le[symmetric]] by blast 

921 
next 

922 
assume ?B show ?F using `?B` by(blast intro:bounded_nat_set_is_finite) 

923 
qed 

924 

925 
lemma finite_nat_set_iff_bounded_le: 

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

927 
apply(simp add:finite_nat_set_iff_bounded) 

928 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

929 
done 

930 

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

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

14485  934 

56328  935 

24853  936 
text{* Any subset of an interval of natural numbers the size of the 
937 
subset is exactly that interval. *} 

938 

939 
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

940 
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

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

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

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

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

945 
proof (induct A rule: finite_linorder_max_induct) 
24853  946 
case empty thus ?case by auto 
947 
next 

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

949 
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

950 
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

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

952 
with insert * show ?case by auto 
24853  953 
qed 
954 
next 

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

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

956 
with assms show ?thesis by simp 
24853  957 
qed 
958 

959 

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

960 
subsubsection {* Proving Inclusions and Equalities between Unions *} 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

961 

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

964 
proof 

965 
show "?A <= ?B" 

966 
proof 

967 
fix x assume "x : ?A" 

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

969 
show "x : ?B" 

970 
proof(cases i) 

971 
case 0 with i show ?thesis by simp 

972 
next 

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

974 
qed 

975 
qed 

976 
next 

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

978 
qed 

979 

980 
lemma UN_le_add_shift: 

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

982 
proof 

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

983 
show "?A <= ?B" by fastforce 
36755  984 
next 
985 
show "?B <= ?A" 

986 
proof 

987 
fix x assume "x : ?B" 

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

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

990 
thus "x : ?A" by blast 

991 
qed 

992 
qed 

993 

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

994 
lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)" 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

995 
by (auto simp add: atLeast0LessThan) 
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

996 

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

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

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

999 

33044  1000 
lemma UN_finite2_subset: 
1001 
"(!!n::nat. (\<Union>i\<in>{0..<n}. A i) \<subseteq> (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) \<subseteq> (\<Union>n. B n)" 

1002 
apply (rule UN_finite_subset) 

1003 
apply (subst UN_UN_finite_eq [symmetric, of B]) 

1004 
apply blast 

1005 
done 

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

1006 

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

1007 
lemma UN_finite2_eq: 
33044  1008 
"(!!n::nat. (\<Union>i\<in>{0..<n}. A i) = (\<Union>i\<in>{0..<n+k}. B i)) \<Longrightarrow> (\<Union>n. A n) = (\<Union>n. B n)" 
1009 
apply (rule subset_antisym) 

1010 
apply (rule UN_finite2_subset, blast) 

1011 
apply (rule UN_finite2_subset [where k=k]) 

35216  1012 
apply (force simp add: atLeastLessThan_add_Un [of 0]) 
33044  1013 
done 
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset

1014 

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

1015 

14485  1016 
subsubsection {* Cardinality *} 
1017 

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

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

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

1023 

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

1025 
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

1026 
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

1027 
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

1028 
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

1029 
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

1030 
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

1031 
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

1032 
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

1033 
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

1034 
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

1035 
qed 
14485  1036 

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

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

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

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

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

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

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

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

1048 
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

1049 
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

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

1051 

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

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

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

1054 
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

1055 

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

1058 
apply(drule ex_bij_betw_finite_nat) 

1059 
apply(drule ex_bij_betw_nat_finite) 

1060 
apply(auto intro!:bij_betw_trans) 

1061 
done 

1062 

1063 
lemma ex_bij_betw_nat_finite_1: 

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

1065 
by (rule finite_same_card_bij) auto 

1066 

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

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

1068 
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

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

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

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

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

1073 
obtain f where "bij_betw 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

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

1075 
moreover obtain g where "bij_betw 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

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

1077 
ultimately have "bij_betw (g o f) A B" 
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOLimage.
hoelzl
parents:
39302
diff
changeset

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

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

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

1081 

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

1082 
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

1083 
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

1084 
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

1085 
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

1086 
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

1087 
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

1088 
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

1089 
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

1090 
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

1091 
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

1092 
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

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

1094 
{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

1095 
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

1096 
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

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

1098 
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

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

1100 

14485  1101 
subsection {* Intervals of integers *} 
1102 

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

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

1106 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  1107 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
1108 

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

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

1110 
"{l+1..<u} = {l<..<u::int}" 
14485  1111 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
1112 

1113 
subsubsection {* Finiteness *} 

1114 

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

1115 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  1116 
{(0::int)..<u} = int ` {..<nat u}" 
14485  1117 
apply (unfold image_def lessThan_def) 
1118 
apply auto 

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

35216  1120 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  1121 
done 
1122 

15045  1123 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
47988  1124 
apply (cases "0 \<le> u") 
14485  1125 
apply (subst image_atLeastZeroLessThan_int, assumption) 
1126 
apply (rule finite_imageI) 

1127 
apply auto 

1128 
done 

1129 

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

14485  1132 
apply (erule subst) 
1133 
apply (rule finite_imageI) 

1134 
apply (rule finite_atLeastZeroLessThan_int) 

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

1135 
apply (rule image_add_int_atLeastLessThan) 
14485  1136 
done 
1137 

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

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

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

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

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

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

24853  1147 

14485  1148 
subsubsection {* Cardinality *} 
1149 

15045  1150 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
47988  1151 
apply (cases "0 \<le> u") 
14485  1152 
apply (subst image_atLeastZeroLessThan_int, assumption) 
1153 
apply (subst card_image) 

1154 
apply (auto simp add: inj_on_def) 

1155 
done 

1156 

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

14485  1159 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  1160 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  1161 
apply (erule subst) 
1162 
apply (rule card_image) 

1163 
apply (simp add: inj_on_def) 

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

1164 
apply (rule image_add_int_atLeastLessThan) 
14485  1165 
done 
1166 

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

29667  1168 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
1169 
apply (auto simp add: algebra_simps) 

1170 
done 

14485  1171 

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

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

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

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

1178 
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

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

1180 
have "{k. P k \<and> k < i} \<subseteq> {..<i}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1181 
with finite_lessThan[of "i"] show ?thesis by (simp add: finite_subset) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1183 

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

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

1185 
assumes zero_in_M: "0 \<in> M" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1186 
shows "card {k \<in> M. k < Suc i} \<noteq> 0" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1188 
from zero_in_M have "{k \<in> M. k < Suc i} \<noteq> {}" by auto 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1189 
with finite_M_bounded_by_nat show ?thesis by (auto simp add: card_eq_0_iff) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1191 

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

1192 
lemma card_less_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" 
37388  1193 
apply (rule card_bij_eq [of Suc _ _ "\<lambda>x. x  Suc 0"]) 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1195 
apply (rule inj_on_diff_nat) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1197 
apply (case_tac x) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1199 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1201 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

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

1204 

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

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

1206 
assumes zero_in_M: "0 \<in> M" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1207 
shows "Suc (card {k. Suc k \<in> M \<and> k < i}) = card {k \<in> M. k < Suc i}" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1209 
from assms have a: "0 \<in> {k \<in> M. k < Suc i}" by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1210 
hence c: "{k \<in> M. k < Suc i} = insert 0 ({k \<in> M. k < Suc i}  {0})" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1211 
by (auto simp only: insert_Diff) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1212 
have b: "{k \<in> M. k < Suc i}  {0} = {k \<in> M  {0}. k < Suc i}" by auto 
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

1213 
from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] 
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

1214 
have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i}  {0}))" 
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1215 
apply (subst card_insert) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1217 
apply (subst b) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

1218 
apply (subst card_less_Suc2[symmetric]) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

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

1221 
with c show ?thesis by simp 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

1223 

14485  1224 

13850  1225 
subsection {*Lemmas useful with the summation operator setsum*} 
1226 

16102
c5f6726d9bb1
Locale expressions: rename with optional mixfix syntax.
ballarin
parents:
16052
diff
changeset

1227 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  1228 

14577  1229 
subsubsection {* Disjoint Unions *} 
13735  1230 

14577  1231 
text {* Singletons and open intervals *} 
13735  1232 

1233 
lemma ivl_disj_un_singleton: 

15045  1234 
"{l::'a::linorder} Un {l<..} = {l..}" 
1235 
"{..<u} Un {u::'a::linorder} = {..u}" 

1236 
"(l::'a::linorder) < u ==> {l} Un {l<..<u} = {l..<u}" 

1237 
"(l::'a::linorder) < u ==> {l<..<u} Un {u} = {l<..u}" 

1238 
"(l::'a::linorder) <= u ==> {l} Un {l<..u} = {l..u}" 

1239 
"(l::'a::linorder) <= u ==> {l..<u} Un {u} = {l..u}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

1240 
by auto 
13735  1241 

14577  1242 
text {* One and twosided intervals *} 
13735  1243 

1244 
lemma ivl_disj_un_one: 

15045  1245 
"(l::'a::linorder) < u ==> {..l} Un {l<..<u} = {..<u}" 
1246 
"(l::'a::linorder) <= u ==> {..<l} Un {l..<u} = {..<u}" 

1247 
"(l::'a::linorder) <= u ==> {..l} Un {l<..u} = {..u}" 

1248 
"(l::'a::linorder) <= u ==> {..<l} Un {l..u} = {..u}" 

1249 
"(l::'a::linorder) <= u ==> {l<..u} Un {u<..} = {l<..}" 

1250 
"(l::'a::linorder) < u ==> {l<..<u} Un {u..} = {l<..}" 

1251 
"(l::'a::linorder) <= u ==> {l..u} Un {u<..} = {l..}" 

1252 
"(l::'a::linorder) <= u ==> {l..<u} Un {u..} = {l..}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

1253 
by auto 
13735  1254 

14577  1255 
text {* Two and twosided intervals *} 
13735  1256 

1257 
lemma ivl_disj_un_two: 

15045  1258 
"[ (l::'a::linorder) < m; m <= u ] ==> {l<..<m} Un {m..<u} = {l<..<u}" 
1259 
"[ (l::'a::linorder) <= m; m < u ] ==> {l<..m} Un {m<..<u} = {l<..<u}" 

1260 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..<m} Un {m..<u} = {l..<u}" 

1261 
"[ (l::'a::linorder) <= m; m < u ] ==> {l..m} Un {m<..<u} = {l..<u}" 

1262 
"[ (l::'a::linorder) < m; m <= u ] ==> {l<..<m} Un {m..u} = {l<..u}" 

1263 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l<..m} Un {m<..u} = {l<..u}" 

1264 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..<m} Un {m..u} = {l..u}" 

1265 
"[ (l::'a::linorder) <= m; m <= u ] ==> {l..m} Un {m<..u} = {l..u}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

1266 
by auto 
13735  1267 

1268 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

1269 

14577  1270 
subsubsection {* Disjoint Intersections *} 
13735  1271 

14577  1272 
text {* One and twosided intervals *} 
13735  1273 

1274 
lemma ivl_disj_int_one: 

15045  1275 
"{..l::'a::order} Int {l<..<u} = {}" 
1276 
"{..<l} Int {l..<u} = {}" 

1277 
"{..l} Int {l<..u} = {}" 

1278 
"{..<l} Int {l..u} = {}" 

1279 
"{l<..u} Int {u<..} = {}" 

1280 
"{l<..<u} Int {u..} = {}" 

1281 
"{l..u} Int {u<..} = {}" 

1282 
"{l..<u} Int {u..} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

1283 
by auto 
13735  1284 

14577  1285 
text {* Two and twosided intervals *} 
13735  1286 

1287 
lemma ivl_disj_int_two: 

15045  1288 
"{l::'a::order<..<m} Int {m..<u} = {}" 
1289 
"{l<..m} Int {m<..<u} = {}" 

1290 
"{l..<m} Int {m..<u} = {}" 

1291 
"{l..m} Int {m<..<u} = {}" 

1292 
"{l<..<m} Int {m..u} = {}" 

1293 
"{l<..m} Int {m<..u} = {}" 

1294 
"{l..<m} Int {m..u} = {}" 

1295 
"{l..m} Int {m<..u} = {}" 

14398
c5c47703f763
Efficient, graphbased reasoner for linear and partial orders.
ballarin
parents:
13850
diff
changeset

1296 
by auto 
13735  1297 

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