author | paulson <lp15@cam.ac.uk> |
Tue, 28 Jul 2015 16:16:13 +0100 | |
changeset 60809 | 457abb82fb9e |
parent 60762 | bf0c76ccee8d |
child 61204 | 3e491e34a62e |
permissions | -rw-r--r-- |
47317
432b29a96f61
modernized obsolete old-style theory name with proper new-style underscore
huffman
parents:
47222
diff
changeset
|
1 |
(* Title: HOL/Set_Interval.thy |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32596
diff
changeset
|
2 |
Author: Tobias Nipkow |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32596
diff
changeset
|
3 |
Author: Clemens Ballarin |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32596
diff
changeset
|
4 |
Author: Jeremy Avigad |
8924 | 5 |
|
13735 | 6 |
lessThan, greaterThan, atLeast, atMost and two-sided intervals |
51334 | 7 |
|
8 |
Modern convention: Ixy stands for an interval where x and y |
|
9 |
describe the lower and upper bound and x,y : {c,o,i} |
|
10 |
where c = closed, o = open, i = infinite. |
|
11 |
Examples: Ico = {_ ..< _} and Ici = {_ ..} |
|
8924 | 12 |
*) |
13 |
||
60758 | 14 |
section \<open>Set intervals\<close> |
14577 | 15 |
|
47317
432b29a96f61
modernized obsolete old-style theory name with proper new-style 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 tab-width;
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 tab-width;
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 tab-width;
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 tab-width;
wenzelm
parents:
32596
diff
changeset
|
36 |
atLeast :: "'a => 'a set" ("(1{_..})") where |
25062 | 37 |
"{l..} == {x. l\<le>x}" |
24691 | 38 |
|
39 |
definition |
|
25062 | 40 |
greaterThanLessThan :: "'a => 'a => 'a set" ("(1{_<..<_})") where |
41 |
"{l<..<u} == {l<..} Int {..<u}" |
|
24691 | 42 |
|
43 |
definition |
|
25062 | 44 |
atLeastLessThan :: "'a => 'a => 'a set" ("(1{_..<_})") where |
45 |
"{l..<u} == {l..} Int {..<u}" |
|
24691 | 46 |
|
47 |
definition |
|
25062 | 48 |
greaterThanAtMost :: "'a => 'a => 'a set" ("(1{_<.._})") where |
49 |
"{l<..u} == {l<..} Int {..u}" |
|
24691 | 50 |
|
51 |
definition |
|
25062 | 52 |
atLeastAtMost :: "'a => 'a => 'a set" ("(1{_.._})") where |
53 |
"{l..u} == {l..} Int {..u}" |
|
24691 | 54 |
|
55 |
end |
|
8924 | 56 |
|
13735 | 57 |
|
60758 | 58 |
text\<open>A note of warning when using @{term"{..<n}"} on type @{typ |
15048 | 59 |
nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving |
60758 | 60 |
@{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well.\<close> |
15048 | 61 |
|
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) |
60586
1d31e3a50373
proper spacing, as for other syntax for these symbols;
wenzelm
parents:
60162
diff
changeset
|
69 |
"_UNION_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10) |
1d31e3a50373
proper spacing, as for other syntax for these symbols;
wenzelm
parents:
60162
diff
changeset
|
70 |
"_UNION_less" :: "'a => 'a => 'b set => 'b set" ("(3\<Union>_<_./ _)" [0, 0, 10] 10) |
1d31e3a50373
proper spacing, as for other syntax for these symbols;
wenzelm
parents:
60162
diff
changeset
|
71 |
"_INTER_le" :: "'a => 'a => 'b set => 'b set" ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10) |
1d31e3a50373
proper spacing, as for other syntax for these symbols;
wenzelm
parents:
60162
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 |
||
60758 | 87 |
subsection \<open>Various equivalences\<close> |
13735 | 88 |
|
25062 | 89 |
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)" |
13850 | 90 |
by (simp add: lessThan_def) |
13735 | 91 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
92 |
lemma Compl_lessThan [simp]: |
13735 | 93 |
"!!k:: 'a::linorder. -lessThan k = atLeast k" |
13850 | 94 |
apply (auto simp add: lessThan_def atLeast_def) |
13735 | 95 |
done |
96 |
||
13850 | 97 |
lemma single_Diff_lessThan [simp]: "!!k:: 'a::order. {k} - lessThan k = {k}" |
98 |
by auto |
|
13735 | 99 |
|
25062 | 100 |
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" |
13850 | 101 |
by (simp add: greaterThan_def) |
13735 | 102 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
103 |
lemma Compl_greaterThan [simp]: |
13735 | 104 |
"!!k:: 'a::linorder. -greaterThan k = atMost k" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset
|
105 |
by (auto simp add: greaterThan_def atMost_def) |
13735 | 106 |
|
13850 | 107 |
lemma Compl_atMost [simp]: "!!k:: 'a::linorder. -atMost k = greaterThan k" |
108 |
apply (subst Compl_greaterThan [symmetric]) |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
109 |
apply (rule double_complement) |
13735 | 110 |
done |
111 |
||
25062 | 112 |
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" |
13850 | 113 |
by (simp add: atLeast_def) |
13735 | 114 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
115 |
lemma Compl_atLeast [simp]: |
13735 | 116 |
"!!k:: 'a::linorder. -atLeast k = lessThan k" |
26072
f65a7fa2da6c
<= and < on nat no longer depend on wellfounded relations
haftmann
parents:
25919
diff
changeset
|
117 |
by (auto simp add: lessThan_def atLeast_def) |
13735 | 118 |
|
25062 | 119 |
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" |
13850 | 120 |
by (simp add: atMost_def) |
13735 | 121 |
|
14485 | 122 |
lemma atMost_Int_atLeast: "!!n:: 'a::order. atMost n Int atLeast n = {n}" |
123 |
by (blast intro: order_antisym) |
|
13850 | 124 |
|
50999 | 125 |
lemma (in linorder) lessThan_Int_lessThan: "{ a <..} \<inter> { b <..} = { max a b <..}" |
126 |
by auto |
|
127 |
||
128 |
lemma (in linorder) greaterThan_Int_greaterThan: "{..< a} \<inter> {..< b} = {..< min a b}" |
|
129 |
by auto |
|
13850 | 130 |
|
60758 | 131 |
subsection \<open>Logical Equivalences for Set Inclusion and Equality\<close> |
13850 | 132 |
|
133 |
lemma atLeast_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
134 |
"(atLeast x \<subseteq> atLeast y) = (y \<le> (x::'a::order))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
135 |
by (blast intro: order_trans) |
13850 | 136 |
|
137 |
lemma atLeast_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
138 |
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" |
13850 | 139 |
by (blast intro: order_antisym order_trans) |
140 |
||
141 |
lemma greaterThan_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
142 |
"(greaterThan x \<subseteq> greaterThan y) = (y \<le> (x::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
143 |
apply (auto simp add: greaterThan_def) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
144 |
apply (subst linorder_not_less [symmetric], blast) |
13850 | 145 |
done |
146 |
||
147 |
lemma greaterThan_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
148 |
"(greaterThan x = greaterThan y) = (x = (y::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
149 |
apply (rule iffI) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
150 |
apply (erule equalityE) |
29709 | 151 |
apply simp_all |
13850 | 152 |
done |
153 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
154 |
lemma atMost_subset_iff [iff]: "(atMost x \<subseteq> atMost y) = (x \<le> (y::'a::order))" |
13850 | 155 |
by (blast intro: order_trans) |
156 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
157 |
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" |
13850 | 158 |
by (blast intro: order_antisym order_trans) |
159 |
||
160 |
lemma lessThan_subset_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
161 |
"(lessThan x \<subseteq> lessThan y) = (x \<le> (y::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
162 |
apply (auto simp add: lessThan_def) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
163 |
apply (subst linorder_not_less [symmetric], blast) |
13850 | 164 |
done |
165 |
||
166 |
lemma lessThan_eq_iff [iff]: |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
167 |
"(lessThan x = lessThan y) = (x = (y::'a::linorder))" |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
168 |
apply (rule iffI) |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
169 |
apply (erule equalityE) |
29709 | 170 |
apply simp_all |
13735 | 171 |
done |
172 |
||
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
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 HOL-image.
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 HOL-image.
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
176 |
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) |
13735 | 177 |
|
57448
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset
|
178 |
lemma (in linorder) Ici_subset_Ioi_iff: "{a ..} \<subseteq> {b <..} \<longleftrightarrow> b < a" |
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset
|
179 |
by auto |
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset
|
180 |
|
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset
|
181 |
lemma (in linorder) Iic_subset_Iio_iff: "{.. a} \<subseteq> {..< b} \<longleftrightarrow> a < b" |
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset
|
182 |
by auto |
159e45728ceb
more equalities of topological filters; strengthen dependent_nat_choice; tuned a couple of proofs
hoelzl
parents:
57447
diff
changeset
|
183 |
|
60758 | 184 |
subsection \<open>Two-sided intervals\<close> |
13735 | 185 |
|
24691 | 186 |
context ord |
187 |
begin |
|
188 |
||
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset
|
189 |
lemma greaterThanLessThan_iff [simp]: |
25062 | 190 |
"(i : {l<..<u}) = (l < i & i < u)" |
13735 | 191 |
by (simp add: greaterThanLessThan_def) |
192 |
||
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset
|
193 |
lemma atLeastLessThan_iff [simp]: |
25062 | 194 |
"(i : {l..<u}) = (l <= i & i < u)" |
13735 | 195 |
by (simp add: atLeastLessThan_def) |
196 |
||
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset
|
197 |
lemma greaterThanAtMost_iff [simp]: |
25062 | 198 |
"(i : {l<..u}) = (l < i & i <= u)" |
13735 | 199 |
by (simp add: greaterThanAtMost_def) |
200 |
||
54147
97a8ff4e4ac9
killed most "no_atp", to make Sledgehammer more complete
blanchet
parents:
53374
diff
changeset
|
201 |
lemma atLeastAtMost_iff [simp]: |
25062 | 202 |
"(i : {l..u}) = (l <= i & i <= u)" |
13735 | 203 |
by (simp add: atLeastAtMost_def) |
204 |
||
60758 | 205 |
text \<open>The above four lemmas could be declared as iffs. Unfortunately this |
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset
|
206 |
breaks many proofs. Since it only helps blast, it is better to leave them |
60758 | 207 |
alone.\<close> |
32436
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset
|
208 |
|
50999 | 209 |
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }" |
210 |
by auto |
|
211 |
||
24691 | 212 |
end |
13735 | 213 |
|
60758 | 214 |
subsubsection\<open>Emptyness, singletons, subset\<close> |
15554 | 215 |
|
24691 | 216 |
context order |
217 |
begin |
|
15554 | 218 |
|
32400 | 219 |
lemma atLeastatMost_empty[simp]: |
220 |
"b < a \<Longrightarrow> {a..b} = {}" |
|
221 |
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) |
|
222 |
||
223 |
lemma atLeastatMost_empty_iff[simp]: |
|
224 |
"{a..b} = {} \<longleftrightarrow> (~ a <= b)" |
|
225 |
by auto (blast intro: order_trans) |
|
226 |
||
227 |
lemma atLeastatMost_empty_iff2[simp]: |
|
228 |
"{} = {a..b} \<longleftrightarrow> (~ a <= b)" |
|
229 |
by auto (blast intro: order_trans) |
|
230 |
||
231 |
lemma atLeastLessThan_empty[simp]: |
|
232 |
"b <= a \<Longrightarrow> {a..<b} = {}" |
|
233 |
by(auto simp: atLeastLessThan_def) |
|
24691 | 234 |
|
32400 | 235 |
lemma atLeastLessThan_empty_iff[simp]: |
236 |
"{a..<b} = {} \<longleftrightarrow> (~ a < b)" |
|
237 |
by auto (blast intro: le_less_trans) |
|
238 |
||
239 |
lemma atLeastLessThan_empty_iff2[simp]: |
|
240 |
"{} = {a..<b} \<longleftrightarrow> (~ a < b)" |
|
241 |
by auto (blast intro: le_less_trans) |
|
15554 | 242 |
|
32400 | 243 |
lemma greaterThanAtMost_empty[simp]: "l \<le> k ==> {k<..l} = {}" |
17719 | 244 |
by(auto simp:greaterThanAtMost_def greaterThan_def atMost_def) |
245 |
||
32400 | 246 |
lemma greaterThanAtMost_empty_iff[simp]: "{k<..l} = {} \<longleftrightarrow> ~ k < l" |
247 |
by auto (blast intro: less_le_trans) |
|
248 |
||
249 |
lemma greaterThanAtMost_empty_iff2[simp]: "{} = {k<..l} \<longleftrightarrow> ~ k < l" |
|
250 |
by auto (blast intro: less_le_trans) |
|
251 |
||
29709 | 252 |
lemma greaterThanLessThan_empty[simp]:"l \<le> k ==> {k<..<l} = {}" |
17719 | 253 |
by(auto simp:greaterThanLessThan_def greaterThan_def lessThan_def) |
254 |
||
25062 | 255 |
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" |
24691 | 256 |
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) |
257 |
||
36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
258 |
lemma atLeastAtMost_singleton': "a = b \<Longrightarrow> {a .. b} = {a}" by simp |
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
259 |
|
32400 | 260 |
lemma atLeastatMost_subset_iff[simp]: |
261 |
"{a..b} <= {c..d} \<longleftrightarrow> (~ a <= b) | c <= a & b <= d" |
|
262 |
unfolding atLeastAtMost_def atLeast_def atMost_def |
|
263 |
by (blast intro: order_trans) |
|
264 |
||
265 |
lemma atLeastatMost_psubset_iff: |
|
266 |
"{a..b} < {c..d} \<longleftrightarrow> |
|
267 |
((~ 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
|
268 |
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) |
32400 | 269 |
|
51334 | 270 |
lemma Icc_eq_Icc[simp]: |
271 |
"{l..h} = {l'..h'} = (l=l' \<and> h=h' \<or> \<not> l\<le>h \<and> \<not> l'\<le>h')" |
|
272 |
by(simp add: order_class.eq_iff)(auto intro: order_trans) |
|
273 |
||
36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
274 |
lemma atLeastAtMost_singleton_iff[simp]: |
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
275 |
"{a .. b} = {c} \<longleftrightarrow> a = b \<and> b = c" |
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
276 |
proof |
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
277 |
assume "{a..b} = {c}" |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
278 |
hence *: "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp |
60758 | 279 |
with \<open>{a..b} = {c}\<close> have "c \<le> a \<and> b \<le> c" by auto |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
280 |
with * show "a = b \<and> b = c" by auto |
36846
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
281 |
qed simp |
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset
|
282 |
|
51334 | 283 |
lemma Icc_subset_Ici_iff[simp]: |
284 |
"{l..h} \<subseteq> {l'..} = (~ l\<le>h \<or> l\<ge>l')" |
|
285 |
by(auto simp: subset_eq intro: order_trans) |
|
286 |
||
287 |
lemma Icc_subset_Iic_iff[simp]: |
|
288 |
"{l..h} \<subseteq> {..h'} = (~ l\<le>h \<or> h\<le>h')" |
|
289 |
by(auto simp: subset_eq intro: order_trans) |
|
290 |
||
291 |
lemma not_Ici_eq_empty[simp]: "{l..} \<noteq> {}" |
|
292 |
by(auto simp: set_eq_iff) |
|
293 |
||
294 |
lemma not_Iic_eq_empty[simp]: "{..h} \<noteq> {}" |
|
295 |
by(auto simp: set_eq_iff) |
|
296 |
||
297 |
lemmas not_empty_eq_Ici_eq_empty[simp] = not_Ici_eq_empty[symmetric] |
|
298 |
lemmas not_empty_eq_Iic_eq_empty[simp] = not_Iic_eq_empty[symmetric] |
|
299 |
||
24691 | 300 |
end |
14485 | 301 |
|
51334 | 302 |
context no_top |
303 |
begin |
|
304 |
||
305 |
(* also holds for no_bot but no_top should suffice *) |
|
306 |
lemma not_UNIV_le_Icc[simp]: "\<not> UNIV \<subseteq> {l..h}" |
|
307 |
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) |
|
308 |
||
309 |
lemma not_UNIV_le_Iic[simp]: "\<not> UNIV \<subseteq> {..h}" |
|
310 |
using gt_ex[of h] by(auto simp: subset_eq less_le_not_le) |
|
311 |
||
312 |
lemma not_Ici_le_Icc[simp]: "\<not> {l..} \<subseteq> {l'..h'}" |
|
313 |
using gt_ex[of h'] |
|
314 |
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) |
|
315 |
||
316 |
lemma not_Ici_le_Iic[simp]: "\<not> {l..} \<subseteq> {..h'}" |
|
317 |
using gt_ex[of h'] |
|
318 |
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) |
|
319 |
||
320 |
end |
|
321 |
||
322 |
context no_bot |
|
323 |
begin |
|
324 |
||
325 |
lemma not_UNIV_le_Ici[simp]: "\<not> UNIV \<subseteq> {l..}" |
|
326 |
using lt_ex[of l] by(auto simp: subset_eq less_le_not_le) |
|
327 |
||
328 |
lemma not_Iic_le_Icc[simp]: "\<not> {..h} \<subseteq> {l'..h'}" |
|
329 |
using lt_ex[of l'] |
|
330 |
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) |
|
331 |
||
332 |
lemma not_Iic_le_Ici[simp]: "\<not> {..h} \<subseteq> {l'..}" |
|
333 |
using lt_ex[of l'] |
|
334 |
by(auto simp: subset_eq less_le)(blast dest:antisym_conv intro: order_trans) |
|
335 |
||
336 |
end |
|
337 |
||
338 |
||
339 |
context no_top |
|
340 |
begin |
|
341 |
||
342 |
(* also holds for no_bot but no_top should suffice *) |
|
343 |
lemma not_UNIV_eq_Icc[simp]: "\<not> UNIV = {l'..h'}" |
|
344 |
using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) |
|
345 |
||
346 |
lemmas not_Icc_eq_UNIV[simp] = not_UNIV_eq_Icc[symmetric] |
|
347 |
||
348 |
lemma not_UNIV_eq_Iic[simp]: "\<not> UNIV = {..h'}" |
|
349 |
using gt_ex[of h'] by(auto simp: set_eq_iff less_le_not_le) |
|
350 |
||
351 |
lemmas not_Iic_eq_UNIV[simp] = not_UNIV_eq_Iic[symmetric] |
|
352 |
||
353 |
lemma not_Icc_eq_Ici[simp]: "\<not> {l..h} = {l'..}" |
|
354 |
unfolding atLeastAtMost_def using not_Ici_le_Iic[of l'] by blast |
|
355 |
||
356 |
lemmas not_Ici_eq_Icc[simp] = not_Icc_eq_Ici[symmetric] |
|
357 |
||
358 |
(* also holds for no_bot but no_top should suffice *) |
|
359 |
lemma not_Iic_eq_Ici[simp]: "\<not> {..h} = {l'..}" |
|
360 |
using not_Ici_le_Iic[of l' h] by blast |
|
361 |
||
362 |
lemmas not_Ici_eq_Iic[simp] = not_Iic_eq_Ici[symmetric] |
|
363 |
||
364 |
end |
|
365 |
||
366 |
context no_bot |
|
367 |
begin |
|
368 |
||
369 |
lemma not_UNIV_eq_Ici[simp]: "\<not> UNIV = {l'..}" |
|
370 |
using lt_ex[of l'] by(auto simp: set_eq_iff less_le_not_le) |
|
371 |
||
372 |
lemmas not_Ici_eq_UNIV[simp] = not_UNIV_eq_Ici[symmetric] |
|
373 |
||
374 |
lemma not_Icc_eq_Iic[simp]: "\<not> {l..h} = {..h'}" |
|
375 |
unfolding atLeastAtMost_def using not_Iic_le_Ici[of h'] by blast |
|
376 |
||
377 |
lemmas not_Iic_eq_Icc[simp] = not_Icc_eq_Iic[symmetric] |
|
378 |
||
379 |
end |
|
380 |
||
381 |
||
53216 | 382 |
context dense_linorder |
42891
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
383 |
begin |
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
384 |
|
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
385 |
lemma greaterThanLessThan_empty_iff[simp]: |
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
386 |
"{ a <..< b } = {} \<longleftrightarrow> b \<le> a" |
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
387 |
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
|
388 |
|
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
389 |
lemma greaterThanLessThan_empty_iff2[simp]: |
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
390 |
"{} = { a <..< b } \<longleftrightarrow> b \<le> a" |
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
391 |
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
|
392 |
|
42901 | 393 |
lemma atLeastLessThan_subseteq_atLeastAtMost_iff: |
394 |
"{a ..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" |
|
395 |
using dense[of "max a d" "b"] |
|
396 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
397 |
||
398 |
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: |
|
399 |
"{a <.. b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" |
|
400 |
using dense[of "a" "min c b"] |
|
401 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
402 |
||
403 |
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: |
|
404 |
"{a <..< b} \<subseteq> { c .. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" |
|
405 |
using dense[of "a" "min c b"] dense[of "max a d" "b"] |
|
406 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
407 |
||
43657 | 408 |
lemma atLeastAtMost_subseteq_atLeastLessThan_iff: |
409 |
"{a .. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a \<le> b \<longrightarrow> c \<le> a \<and> b < d)" |
|
410 |
using dense[of "max a d" "b"] |
|
411 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
412 |
||
413 |
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: |
|
414 |
"{a <.. b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b < d)" |
|
415 |
using dense[of "a" "min c b"] |
|
416 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
417 |
||
418 |
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: |
|
419 |
"{a <..< b} \<subseteq> { c ..< d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" |
|
420 |
using dense[of "a" "min c b"] dense[of "max a d" "b"] |
|
421 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
422 |
||
56328 | 423 |
lemma greaterThanLessThan_subseteq_greaterThanAtMost_iff: |
424 |
"{a <..< b} \<subseteq> { c <.. d } \<longleftrightarrow> (a < b \<longrightarrow> c \<le> a \<and> b \<le> d)" |
|
425 |
using dense[of "a" "min c b"] dense[of "max a d" "b"] |
|
426 |
by (force simp: subset_eq Ball_def not_less[symmetric]) |
|
427 |
||
42891
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
428 |
end |
e2f473671937
simp rules for empty intervals on dense linear order
hoelzl
parents:
40703
diff
changeset
|
429 |
|
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
430 |
context no_top |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
431 |
begin |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
432 |
|
51334 | 433 |
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
|
434 |
using gt_ex[of x] by auto |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
435 |
|
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
436 |
end |
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 |
context no_bot |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
439 |
begin |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
440 |
|
51334 | 441 |
lemma lessThan_non_empty[simp]: "{..< x} \<noteq> {}" |
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
442 |
using lt_ex[of x] by auto |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
443 |
|
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
444 |
end |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
445 |
|
32408 | 446 |
lemma (in linorder) atLeastLessThan_subset_iff: |
447 |
"{a..<b} <= {c..<d} \<Longrightarrow> b <= a | c<=a & b<=d" |
|
448 |
apply (auto simp:subset_eq Ball_def) |
|
449 |
apply(frule_tac x=a in spec) |
|
450 |
apply(erule_tac x=d in allE) |
|
451 |
apply (simp add: less_imp_le) |
|
452 |
done |
|
453 |
||
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
454 |
lemma atLeastLessThan_inj: |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
456 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
457 |
shows "a = c" "b = d" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
458 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
459 |
|
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
460 |
lemma atLeastLessThan_eq_iff: |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
461 |
fixes a b c d :: "'a::linorder" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
462 |
assumes "a < b" "c < d" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
463 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
464 |
using atLeastLessThan_inj assms by auto |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
465 |
|
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
466 |
lemma (in linorder) Ioc_inj: "{a <.. b} = {c <.. d} \<longleftrightarrow> (b \<le> a \<and> d \<le> c) \<or> a = c \<and> b = d" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
467 |
by (metis eq_iff greaterThanAtMost_empty_iff2 greaterThanAtMost_iff le_cases not_le) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
468 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
469 |
lemma (in order) Iio_Int_singleton: "{..<k} \<inter> {x} = (if x < k then {x} else {})" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
470 |
by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
471 |
|
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
472 |
lemma (in linorder) Ioc_subset_iff: "{a<..b} \<subseteq> {c<..d} \<longleftrightarrow> (b \<le> a \<or> c \<le> a \<and> b \<le> d)" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
473 |
by (auto simp: subset_eq Ball_def) (metis less_le not_less) |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
474 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset
|
475 |
lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" |
51334 | 476 |
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
|
477 |
|
52729
412c9e0381a1
factored syntactic type classes for bot and top (by Alessandro Coglio)
haftmann
parents:
52380
diff
changeset
|
478 |
lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top" |
51334 | 479 |
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
|
480 |
|
51334 | 481 |
lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff: |
482 |
"{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)" |
|
483 |
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
|
484 |
|
56949 | 485 |
lemma Iio_eq_empty_iff: "{..< n::'a::{linorder, order_bot}} = {} \<longleftrightarrow> n = bot" |
486 |
by (auto simp: set_eq_iff not_less le_bot) |
|
487 |
||
488 |
lemma Iio_eq_empty_iff_nat: "{..< n::nat} = {} \<longleftrightarrow> n = 0" |
|
489 |
by (simp add: Iio_eq_empty_iff bot_nat_def) |
|
490 |
||
58970 | 491 |
lemma mono_image_least: |
492 |
assumes f_mono: "mono f" and f_img: "f ` {m ..< n} = {m' ..< n'}" "m < n" |
|
493 |
shows "f m = m'" |
|
494 |
proof - |
|
495 |
from f_img have "{m' ..< n'} \<noteq> {}" |
|
496 |
by (metis atLeastLessThan_empty_iff image_is_empty) |
|
497 |
with f_img have "m' \<in> f ` {m ..< n}" by auto |
|
498 |
then obtain k where "f k = m'" "m \<le> k" by auto |
|
499 |
moreover have "m' \<le> f m" using f_img by auto |
|
500 |
ultimately show "f m = m'" |
|
501 |
using f_mono by (auto elim: monoE[where x=m and y=k]) |
|
502 |
qed |
|
503 |
||
51328
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset
|
504 |
|
60758 | 505 |
subsection \<open>Infinite intervals\<close> |
56328 | 506 |
|
507 |
context dense_linorder |
|
508 |
begin |
|
509 |
||
510 |
lemma infinite_Ioo: |
|
511 |
assumes "a < b" |
|
512 |
shows "\<not> finite {a<..<b}" |
|
513 |
proof |
|
514 |
assume fin: "finite {a<..<b}" |
|
515 |
moreover have ne: "{a<..<b} \<noteq> {}" |
|
60758 | 516 |
using \<open>a < b\<close> by auto |
56328 | 517 |
ultimately have "a < Max {a <..< b}" "Max {a <..< b} < b" |
518 |
using Max_in[of "{a <..< b}"] by auto |
|
519 |
then obtain x where "Max {a <..< b} < x" "x < b" |
|
520 |
using dense[of "Max {a<..<b}" b] by auto |
|
521 |
then have "x \<in> {a <..< b}" |
|
60758 | 522 |
using \<open>a < Max {a <..< b}\<close> by auto |
56328 | 523 |
then have "x \<le> Max {a <..< b}" |
524 |
using fin by auto |
|
60758 | 525 |
with \<open>Max {a <..< b} < x\<close> show False by auto |
56328 | 526 |
qed |
527 |
||
528 |
lemma infinite_Icc: "a < b \<Longrightarrow> \<not> finite {a .. b}" |
|
529 |
using greaterThanLessThan_subseteq_atLeastAtMost_iff[of a b a b] infinite_Ioo[of a b] |
|
530 |
by (auto dest: finite_subset) |
|
531 |
||
532 |
lemma infinite_Ico: "a < b \<Longrightarrow> \<not> finite {a ..< b}" |
|
533 |
using greaterThanLessThan_subseteq_atLeastLessThan_iff[of a b a b] infinite_Ioo[of a b] |
|
534 |
by (auto dest: finite_subset) |
|
535 |
||
536 |
lemma infinite_Ioc: "a < b \<Longrightarrow> \<not> finite {a <.. b}" |
|
537 |
using greaterThanLessThan_subseteq_greaterThanAtMost_iff[of a b a b] infinite_Ioo[of a b] |
|
538 |
by (auto dest: finite_subset) |
|
539 |
||
540 |
end |
|
541 |
||
542 |
lemma infinite_Iio: "\<not> finite {..< a :: 'a :: {no_bot, linorder}}" |
|
543 |
proof |
|
544 |
assume "finite {..< a}" |
|
545 |
then have *: "\<And>x. x < a \<Longrightarrow> Min {..< a} \<le> x" |
|
546 |
by auto |
|
547 |
obtain x where "x < a" |
|
548 |
using lt_ex by auto |
|
549 |
||
550 |
obtain y where "y < Min {..< a}" |
|
551 |
using lt_ex by auto |
|
552 |
also have "Min {..< a} \<le> x" |
|
60758 | 553 |
using \<open>x < a\<close> by fact |
554 |
also note \<open>x < a\<close> |
|
56328 | 555 |
finally have "Min {..< a} \<le> y" |
556 |
by fact |
|
60758 | 557 |
with \<open>y < Min {..< a}\<close> show False by auto |
56328 | 558 |
qed |
559 |
||
560 |
lemma infinite_Iic: "\<not> finite {.. a :: 'a :: {no_bot, linorder}}" |
|
561 |
using infinite_Iio[of a] finite_subset[of "{..< a}" "{.. a}"] |
|
562 |
by (auto simp: subset_eq less_imp_le) |
|
563 |
||
564 |
lemma infinite_Ioi: "\<not> finite {a :: 'a :: {no_top, linorder} <..}" |
|
565 |
proof |
|
566 |
assume "finite {a <..}" |
|
567 |
then have *: "\<And>x. a < x \<Longrightarrow> x \<le> Max {a <..}" |
|
568 |
by auto |
|
569 |
||
570 |
obtain y where "Max {a <..} < y" |
|
571 |
using gt_ex by auto |
|
572 |
||
573 |
obtain x where "a < x" |
|
574 |
using gt_ex by auto |
|
575 |
also then have "x \<le> Max {a <..}" |
|
576 |
by fact |
|
60758 | 577 |
also note \<open>Max {a <..} < y\<close> |
56328 | 578 |
finally have "y \<le> Max { a <..}" |
579 |
by fact |
|
60758 | 580 |
with \<open>Max {a <..} < y\<close> show False by auto |
56328 | 581 |
qed |
582 |
||
583 |
lemma infinite_Ici: "\<not> finite {a :: 'a :: {no_top, linorder} ..}" |
|
584 |
using infinite_Ioi[of a] finite_subset[of "{a <..}" "{a ..}"] |
|
585 |
by (auto simp: subset_eq less_imp_le) |
|
586 |
||
60758 | 587 |
subsubsection \<open>Intersection\<close> |
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
588 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
589 |
context linorder |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
590 |
begin |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
591 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
592 |
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
|
593 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
594 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
595 |
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
|
596 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
597 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
598 |
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
|
599 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
600 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
601 |
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
|
602 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
603 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
604 |
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
|
605 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
606 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
607 |
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
|
608 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
609 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
610 |
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
|
611 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
612 |
|
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
613 |
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
|
614 |
by auto |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
615 |
|
50417 | 616 |
lemma Int_atMost[simp]: "{..a} \<inter> {..b} = {.. min a b}" |
617 |
by (auto simp: min_def) |
|
618 |
||
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
619 |
lemma Ioc_disjoint: "{a<..b} \<inter> {c<..d} = {} \<longleftrightarrow> b \<le> a \<or> d \<le> c \<or> b \<le> c \<or> d \<le> a" |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
620 |
using assms by auto |
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57418
diff
changeset
|
621 |
|
32456
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
622 |
end |
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset
|
623 |
|
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
624 |
context complete_lattice |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
625 |
begin |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
626 |
|
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
627 |
lemma |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
628 |
shows Sup_atLeast[simp]: "Sup {x ..} = top" |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
629 |
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
|
630 |
and Sup_atMost[simp]: "Sup {.. y} = y" |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
631 |
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
|
632 |
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
|
633 |
by (auto intro!: Sup_eqI) |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
634 |
|
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
635 |
lemma |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
636 |
shows Inf_atMost[simp]: "Inf {.. x} = bot" |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
637 |
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
|
638 |
and Inf_atLeast[simp]: "Inf {x ..} = x" |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
639 |
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
|
640 |
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
|
641 |
by (auto intro!: Inf_eqI) |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
642 |
|
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
643 |
end |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
644 |
|
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
645 |
lemma |
53216 | 646 |
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
|
647 |
shows Sup_lessThan[simp]: "Sup {..< y} = y" |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
648 |
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
|
649 |
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
|
650 |
and Inf_greaterThan[simp]: "Inf {x <..} = x" |
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset
|
651 |
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
|
652 |
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
|
653 |
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
|
654 |
|
60758 | 655 |
subsection \<open>Intervals of natural numbers\<close> |
14485 | 656 |
|
60758 | 657 |
subsubsection \<open>The Constant @{term lessThan}\<close> |
15047 | 658 |
|
14485 | 659 |
lemma lessThan_0 [simp]: "lessThan (0::nat) = {}" |
660 |
by (simp add: lessThan_def) |
|
661 |
||
662 |
lemma lessThan_Suc: "lessThan (Suc k) = insert k (lessThan k)" |
|
663 |
by (simp add: lessThan_def less_Suc_eq, blast) |
|
664 |
||
60758 | 665 |
text \<open>The following proof is convenient in induction proofs where |
39072 | 666 |
new elements get indices at the beginning. So it is used to transform |
60758 | 667 |
@{term "{..<Suc n}"} to @{term "0::nat"} and @{term "{..< n}"}.\<close> |
39072 | 668 |
|
59000 | 669 |
lemma zero_notin_Suc_image: "0 \<notin> Suc ` A" |
670 |
by auto |
|
671 |
||
39072 | 672 |
lemma lessThan_Suc_eq_insert_0: "{..<Suc n} = insert 0 (Suc ` {..<n})" |
59000 | 673 |
by (auto simp: image_iff less_Suc_eq_0_disj) |
39072 | 674 |
|
14485 | 675 |
lemma lessThan_Suc_atMost: "lessThan (Suc k) = atMost k" |
676 |
by (simp add: lessThan_def atMost_def less_Suc_eq_le) |
|
677 |
||
59000 | 678 |
lemma Iic_Suc_eq_insert_0: "{.. Suc n} = insert 0 (Suc ` {.. n})" |
679 |
unfolding lessThan_Suc_atMost[symmetric] lessThan_Suc_eq_insert_0[of "Suc n"] .. |
|
680 |
||
14485 | 681 |
lemma UN_lessThan_UNIV: "(UN m::nat. lessThan m) = UNIV" |
682 |
by blast |
|
683 |
||
60758 | 684 |
subsubsection \<open>The Constant @{term greaterThan}\<close> |
15047 | 685 |
|
14485 | 686 |
lemma greaterThan_0 [simp]: "greaterThan 0 = range Suc" |
687 |
apply (simp add: greaterThan_def) |
|
688 |
apply (blast dest: gr0_conv_Suc [THEN iffD1]) |
|
689 |
done |
|
690 |
||
691 |
lemma greaterThan_Suc: "greaterThan (Suc k) = greaterThan k - {Suc k}" |
|
692 |
apply (simp add: greaterThan_def) |
|
693 |
apply (auto elim: linorder_neqE) |
|
694 |
done |
|
695 |
||
696 |
lemma INT_greaterThan_UNIV: "(INT m::nat. greaterThan m) = {}" |
|
697 |
by blast |
|
698 |
||
60758 | 699 |
subsubsection \<open>The Constant @{term atLeast}\<close> |
15047 | 700 |
|
14485 | 701 |
lemma atLeast_0 [simp]: "atLeast (0::nat) = UNIV" |
702 |
by (unfold atLeast_def UNIV_def, simp) |
|
703 |
||
704 |
lemma atLeast_Suc: "atLeast (Suc k) = atLeast k - {k}" |
|
705 |
apply (simp add: atLeast_def) |
|
706 |
apply (simp add: Suc_le_eq) |
|
707 |
apply (simp add: order_le_less, blast) |
|
708 |
done |
|
709 |
||
710 |
lemma atLeast_Suc_greaterThan: "atLeast (Suc k) = greaterThan k" |
|
711 |
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) |
|
712 |
||
713 |
lemma UN_atLeast_UNIV: "(UN m::nat. atLeast m) = UNIV" |
|
714 |
by blast |
|
715 |
||
60758 | 716 |
subsubsection \<open>The Constant @{term atMost}\<close> |
15047 | 717 |
|
14485 | 718 |
lemma atMost_0 [simp]: "atMost (0::nat) = {0}" |
719 |
by (simp add: atMost_def) |
|
720 |
||
721 |
lemma atMost_Suc: "atMost (Suc k) = insert (Suc k) (atMost k)" |
|
722 |
apply (simp add: atMost_def) |
|
723 |
apply (simp add: less_Suc_eq order_le_less, blast) |
|
724 |
done |
|
725 |
||
726 |
lemma UN_atMost_UNIV: "(UN m::nat. atMost m) = UNIV" |
|
727 |
by blast |
|
728 |
||
60758 | 729 |
subsubsection \<open>The Constant @{term atLeastLessThan}\<close> |
15047 | 730 |
|
60758 | 731 |
text\<open>The orientation of the following 2 rules is tricky. The lhs is |
24449 | 732 |
defined in terms of the rhs. Hence the chosen orientation makes sense |
733 |
in this theory --- the reverse orientation complicates proofs (eg |
|
734 |
nontermination). But outside, when the definition of the lhs is rarely |
|
735 |
used, the opposite orientation seems preferable because it reduces a |
|
60758 | 736 |
specific concept to a more general one.\<close> |
28068 | 737 |
|
15047 | 738 |
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" |
15042 | 739 |
by(simp add:lessThan_def atLeastLessThan_def) |
24449 | 740 |
|
28068 | 741 |
lemma atLeast0AtMost: "{0..n::nat} = {..n}" |
742 |
by(simp add:atMost_def atLeastAtMost_def) |
|
743 |
||
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset
|
744 |
declare atLeast0LessThan[symmetric, code_unfold] |
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31509
diff
changeset
|
745 |
atLeast0AtMost[symmetric, code_unfold] |
24449 | 746 |
|
747 |
lemma atLeastLessThan0: "{m..<0::nat} = {}" |
|
15047 | 748 |
by (simp add: atLeastLessThan_def) |
24449 | 749 |
|
60758 | 750 |
subsubsection \<open>Intervals of nats with @{term Suc}\<close> |
15047 | 751 |
|
60758 | 752 |
text\<open>Not a simprule because the RHS is too messy.\<close> |
15047 | 753 |
lemma atLeastLessThanSuc: |
754 |
"{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
|
755 |
by (auto simp add: atLeastLessThan_def) |
15047 | 756 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
757 |
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" |
15047 | 758 |
by (auto simp add: atLeastLessThan_def) |
16041 | 759 |
(* |
15047 | 760 |
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" |
761 |
by (induct k, simp_all add: atLeastLessThanSuc) |
|
762 |
||
763 |
lemma atLeastSucLessThan [simp]: "{Suc n..<n} = {}" |
|
764 |
by (auto simp add: atLeastLessThan_def) |
|
16041 | 765 |
*) |
15045 | 766 |
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" |
14485 | 767 |
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) |
768 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
769 |
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
|
770 |
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def |
14485 | 771 |
greaterThanAtMost_def) |
772 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
773 |
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
|
774 |
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def |
14485 | 775 |
greaterThanLessThan_def) |
776 |
||
15554 | 777 |
lemma atLeastAtMostSuc_conv: "m \<le> Suc n \<Longrightarrow> {m..Suc n} = insert (Suc n) {m..n}" |
778 |
by (auto simp add: atLeastAtMost_def) |
|
779 |
||
45932 | 780 |
lemma atLeastAtMost_insertL: "m \<le> n \<Longrightarrow> insert m {Suc m..n} = {m ..n}" |
781 |
by auto |
|
782 |
||
60758 | 783 |
text \<open>The analogous result is useful on @{typ int}:\<close> |
43157 | 784 |
(* here, because we don't have an own int section *) |
785 |
lemma atLeastAtMostPlus1_int_conv: |
|
786 |
"m <= 1+n \<Longrightarrow> {m..1+n} = insert (1+n) {m..n::int}" |
|
787 |
by (auto intro: set_eqI) |
|
788 |
||
33044 | 789 |
lemma atLeastLessThan_add_Un: "i \<le> j \<Longrightarrow> {i..<j+k} = {i..<j} \<union> {j..<j+k::nat}" |
790 |
apply (induct k) |
|
791 |
apply (simp_all add: atLeastLessThanSuc) |
|
792 |
done |
|
793 |
||
60758 | 794 |
subsubsection \<open>Intervals and numerals\<close> |
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset
|
795 |
|
60758 | 796 |
lemma lessThan_nat_numeral: --\<open>Evaluation for specific numerals\<close> |
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset
|
797 |
"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
|
798 |
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
|
799 |
|
60758 | 800 |
lemma atMost_nat_numeral: --\<open>Evaluation for specific numerals\<close> |
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset
|
801 |
"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
|
802 |
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
|
803 |
|
60758 | 804 |
lemma atLeastLessThan_nat_numeral: --\<open>Evaluation for specific numerals\<close> |
57113
7e95523302e6
New theorems to enable the simplification of certain functions when applied to specific natural number constants (such as 4)
paulson <lp15@cam.ac.uk>
parents:
56949
diff
changeset
|
805 |
"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
|
806 |
(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
|
807 |
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
|
808 |
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
|
809 |
|
60758 | 810 |
subsubsection \<open>Image\<close> |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
811 |
|
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
812 |
lemma image_add_atLeastAtMost [simp]: |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
813 |
fixes k ::"'a::linordered_semidom" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
814 |
shows "(\<lambda>n. n+k) ` {i..j} = {i+k..j+k}" (is "?A = ?B") |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
815 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
816 |
show "?A \<subseteq> ?B" by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
817 |
next |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
818 |
show "?B \<subseteq> ?A" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
819 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
820 |
fix n assume a: "n : ?B" |
60615
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
821 |
hence "n - k : {i..j}" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
822 |
by (auto simp: add_le_imp_le_diff add_le_add_imp_diff_le) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
823 |
moreover have "n = (n - k) + k" using a |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
824 |
proof - |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
825 |
have "k + i \<le> n" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
826 |
by (metis a add.commute atLeastAtMost_iff) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
827 |
hence "k + (n - k) = n" |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
828 |
by (metis (no_types) ab_semigroup_add_class.add_ac(1) add_diff_cancel_left' le_add_diff_inverse) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
829 |
thus ?thesis |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
830 |
by (simp add: add.commute) |
e5fa1d5d3952
Useful lemmas. The theorem concerning swapping the variables in a double integral.
paulson <lp15@cam.ac.uk>
parents:
60586
diff
changeset
|
831 |
qed |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
832 |
ultimately show "n : ?A" by blast |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
833 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
834 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
835 |
|
60809
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
836 |
lemma image_diff_atLeastAtMost [simp]: |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
837 |
fixes d::"'a::linordered_idom" shows "(op - d ` {a..b}) = {d-b..d-a}" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
838 |
apply auto |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
839 |
apply (rule_tac x="d-x" in rev_image_eqI, auto) |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
840 |
done |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
841 |
|
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
842 |
lemma image_mult_atLeastAtMost [simp]: |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
843 |
fixes d::"'a::linordered_field" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
844 |
assumes "d>0" shows "(op * d ` {a..b}) = {d*a..d*b}" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
845 |
using assms |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
846 |
by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x]) |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
847 |
|
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
848 |
lemma image_affinity_atLeastAtMost: |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
849 |
fixes c :: "'a::linordered_field" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
850 |
shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {} |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
851 |
else if 0 \<le> m then {m*a + c .. m *b + c} |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
852 |
else {m*b + c .. m*a + c})" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
853 |
apply (case_tac "m=0", auto simp: mult_le_cancel_left) |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
854 |
apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps) |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
855 |
apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps) |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
856 |
done |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
857 |
|
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
858 |
lemma image_affinity_atLeastAtMost_diff: |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
859 |
fixes c :: "'a::linordered_field" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
860 |
shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {} |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
861 |
else if 0 \<le> m then {m*a - c .. m*b - c} |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
862 |
else {m*b - c .. m*a - c})" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
863 |
using image_affinity_atLeastAtMost [of m "-c" a b] |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
864 |
by simp |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
865 |
|
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
866 |
lemma image_affinity_atLeastAtMost_div_diff: |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
867 |
fixes c :: "'a::linordered_field" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
868 |
shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {} |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
869 |
else if 0 \<le> m then {a/m - c .. b/m - c} |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
870 |
else {b/m - c .. a/m - c})" |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
871 |
using image_affinity_atLeastAtMost_diff [of "inverse m" c a b] |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
872 |
by (simp add: field_class.field_divide_inverse algebra_simps) |
457abb82fb9e
the Cauchy integral theorem and related material
paulson <lp15@cam.ac.uk>
parents:
60762
diff
changeset
|
873 |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
874 |
lemma image_add_atLeastLessThan: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
875 |
"(%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
|
876 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
877 |
show "?A \<subseteq> ?B" by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
878 |
next |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
879 |
show "?B \<subseteq> ?A" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
880 |
proof |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
881 |
fix n assume a: "n : ?B" |
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19538
diff
changeset
|
882 |
hence "n - k : {i..<j}" by auto |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
883 |
moreover have "n = (n - k) + k" using a by auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
884 |
ultimately show "n : ?A" by blast |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
885 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
886 |
qed |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
887 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
888 |
corollary image_Suc_atLeastAtMost[simp]: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
889 |
"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
|
890 |
using image_add_atLeastAtMost[where k="Suc 0"] by simp |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
891 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
892 |
corollary image_Suc_atLeastLessThan[simp]: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
893 |
"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
|
894 |
using image_add_atLeastLessThan[where k="Suc 0"] by simp |
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
895 |
|
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
896 |
lemma image_add_int_atLeastLessThan: |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
897 |
"(%x. x + (l::int)) ` {0..<u-l} = {l..<u}" |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
898 |
apply (auto simp add: image_def) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
899 |
apply (rule_tac x = "x - l" in bexI) |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
900 |
apply auto |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
901 |
done |
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
902 |
|
37664 | 903 |
lemma image_minus_const_atLeastLessThan_nat: |
904 |
fixes c :: nat |
|
905 |
shows "(\<lambda>i. i - c) ` {x ..< y} = |
|
906 |
(if c < y then {x - c ..< y - c} else if x < y then {0} else {})" |
|
907 |
(is "_ = ?right") |
|
908 |
proof safe |
|
909 |
fix a assume a: "a \<in> ?right" |
|
910 |
show "a \<in> (\<lambda>i. i - c) ` {x ..< y}" |
|
911 |
proof cases |
|
912 |
assume "c < y" with a show ?thesis |
|
913 |
by (auto intro!: image_eqI[of _ _ "a + c"]) |
|
914 |
next |
|
915 |
assume "\<not> c < y" with a show ?thesis |
|
916 |
by (auto intro!: image_eqI[of _ _ x] split: split_if_asm) |
|
917 |
qed |
|
918 |
qed auto |
|
919 |
||
51152 | 920 |
lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}" |
55143
04448228381d
explicit eigen-context for attributes "where", "of", and corresponding read_instantiate, instantiate_tac;
wenzelm
parents:
55088
diff
changeset
|
921 |
by (auto intro!: image_eqI [where x = "nat x" for x]) |
51152 | 922 |
|
35580 | 923 |
context ordered_ab_group_add |
924 |
begin |
|
925 |
||
926 |
lemma |
|
927 |
fixes x :: 'a |
|
928 |
shows image_uminus_greaterThan[simp]: "uminus ` {x<..} = {..<-x}" |
|
929 |
and image_uminus_atLeast[simp]: "uminus ` {x..} = {..-x}" |
|
930 |
proof safe |
|
931 |
fix y assume "y < -x" |
|
932 |
hence *: "x < -y" using neg_less_iff_less[of "-y" x] by simp |
|
933 |
have "- (-y) \<in> uminus ` {x<..}" |
|
934 |
by (rule imageI) (simp add: *) |
|
935 |
thus "y \<in> uminus ` {x<..}" by simp |
|
936 |
next |
|
937 |
fix y assume "y \<le> -x" |
|
938 |
have "- (-y) \<in> uminus ` {x..}" |
|
60758 | 939 |
by (rule imageI) (insert \<open>y \<le> -x\<close>[THEN le_imp_neg_le], simp) |
35580 | 940 |
thus "y \<in> uminus ` {x..}" by simp |
941 |
qed simp_all |
|
942 |
||
943 |
lemma |
|
944 |
fixes x :: 'a |
|
945 |
shows image_uminus_lessThan[simp]: "uminus ` {..<x} = {-x<..}" |
|
946 |
and image_uminus_atMost[simp]: "uminus ` {..x} = {-x..}" |
|
947 |
proof - |
|
948 |
have "uminus ` {..<x} = uminus ` uminus ` {-x<..}" |
|
949 |
and "uminus ` {..x} = uminus ` uminus ` {-x..}" by simp_all |
|
950 |
thus "uminus ` {..<x} = {-x<..}" and "uminus ` {..x} = {-x..}" |
|
951 |
by (simp_all add: image_image |
|
952 |
del: image_uminus_greaterThan image_uminus_atLeast) |
|
953 |
qed |
|
954 |
||
955 |
lemma |
|
956 |
fixes x :: 'a |
|
957 |
shows image_uminus_atLeastAtMost[simp]: "uminus ` {x..y} = {-y..-x}" |
|
958 |
and image_uminus_greaterThanAtMost[simp]: "uminus ` {x<..y} = {-y..<-x}" |
|
959 |
and image_uminus_atLeastLessThan[simp]: "uminus ` {x..<y} = {-y<..-x}" |
|
960 |
and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}" |
|
961 |
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def |
|
962 |
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) |
|
963 |
end |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
964 |
|
60758 | 965 |
subsubsection \<open>Finiteness\<close> |
14485 | 966 |
|
15045 | 967 |
lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}" |
14485 | 968 |
by (induct k) (simp_all add: lessThan_Suc) |
969 |
||
970 |
lemma finite_atMost [iff]: fixes k :: nat shows "finite {..k}" |
|
971 |
by (induct k) (simp_all add: atMost_Suc) |
|
972 |
||
973 |
lemma finite_greaterThanLessThan [iff]: |
|
15045 | 974 |
fixes l :: nat shows "finite {l<..<u}" |
14485 | 975 |
by (simp add: greaterThanLessThan_def) |
976 |
||
977 |
lemma finite_atLeastLessThan [iff]: |
|
15045 | 978 |
fixes l :: nat shows "finite {l..<u}" |
14485 | 979 |
by (simp add: atLeastLessThan_def) |
980 |
||
981 |
lemma finite_greaterThanAtMost [iff]: |
|
15045 | 982 |
fixes l :: nat shows "finite {l<..u}" |
14485 | 983 |
by (simp add: greaterThanAtMost_def) |
984 |
||
985 |
lemma finite_atLeastAtMost [iff]: |
|
986 |
fixes l :: nat shows "finite {l..u}" |
|
987 |
by (simp add: atLeastAtMost_def) |
|
988 |
||
60758 | 989 |
text \<open>A bounded set of natural numbers is finite.\<close> |
14485 | 990 |
lemma bounded_nat_set_is_finite: |
24853 | 991 |
"(ALL i:N. i < (n::nat)) ==> finite N" |
28068 | 992 |
apply (rule finite_subset) |
993 |
apply (rule_tac [2] finite_lessThan, auto) |
|
994 |
done |
|
995 |
||
60758 | 996 |
text \<open>A set of natural numbers is finite iff it is bounded.\<close> |
31044 | 997 |
lemma finite_nat_set_iff_bounded: |
998 |
"finite(N::nat set) = (EX m. ALL n:N. n<m)" (is "?F = ?B") |
|
999 |
proof |
|
1000 |
assume f:?F show ?B |
|
60758 | 1001 |
using Max_ge[OF \<open>?F\<close>, simplified less_Suc_eq_le[symmetric]] by blast |
31044 | 1002 |
next |
60758 | 1003 |
assume ?B show ?F using \<open>?B\<close> by(blast intro:bounded_nat_set_is_finite) |
31044 | 1004 |
qed |
1005 |
||
1006 |
lemma finite_nat_set_iff_bounded_le: |
|
1007 |
"finite(N::nat set) = (EX m. ALL n:N. n<=m)" |
|
1008 |
apply(simp add:finite_nat_set_iff_bounded) |
|
1009 |
apply(blast dest:less_imp_le_nat le_imp_less_Suc) |
|
1010 |
done |
|
1011 |
||
28068 | 1012 |
lemma finite_less_ub: |
1013 |
"!!f::nat=>nat. (!!n. n \<le> f n) ==> finite {n. f n \<le> u}" |
|
1014 |
by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans) |
|
14485 | 1015 |
|
56328 | 1016 |
|
60758 | 1017 |
text\<open>Any subset of an interval of natural numbers the size of the |
1018 |
subset is exactly that interval.\<close> |
|
24853 | 1019 |
|
1020 |
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
|
1021 |
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
|
1022 |
shows "A = {k..<k + card A}" |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1023 |
proof (cases "finite A") |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1024 |
case True |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1025 |
from this and assms show ?thesis |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1026 |
proof (induct A rule: finite_linorder_max_induct) |
24853 | 1027 |
case empty thus ?case by auto |
1028 |
next |
|
33434 | 1029 |
case (insert b A) |
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1030 |
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
|
1031 |
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
|
1032 |
by fastforce+ |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1033 |
with insert * show ?case by auto |
24853 | 1034 |
qed |
1035 |
next |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1036 |
case False |
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
53216
diff
changeset
|
1037 |
with assms show ?thesis by simp |
24853 | 1038 |
qed |
1039 |
||
1040 |
||
60758 | 1041 |
subsubsection \<open>Proving Inclusions and Equalities between Unions\<close> |
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1042 |
|
36755 | 1043 |
lemma UN_le_eq_Un0: |
1044 |
"(\<Union>i\<le>n::nat. M i) = (\<Union>i\<in>{1..n}. M i) \<union> M 0" (is "?A = ?B") |
|
1045 |
proof |
|
1046 |
show "?A <= ?B" |
|
1047 |
proof |
|
1048 |
fix x assume "x : ?A" |
|
1049 |
then obtain i where i: "i\<le>n" "x : M i" by auto |
|
1050 |
show "x : ?B" |
|
1051 |
proof(cases i) |
|
1052 |
case 0 with i show ?thesis by simp |
|
1053 |
next |
|
1054 |
case (Suc j) with i show ?thesis by auto |
|
1055 |
qed |
|
1056 |
qed |
|
1057 |
next |
|
1058 |
show "?B <= ?A" by auto |
|
1059 |
qed |
|
1060 |
||
1061 |
lemma UN_le_add_shift: |
|
1062 |
"(\<Union>i\<le>n::nat. M(i+k)) = (\<Union>i\<in>{k..n+k}. M i)" (is "?A = ?B") |
|
1063 |
proof |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44008
diff
changeset
|
1064 |
show "?A <= ?B" by fastforce |
36755 | 1065 |
next |
1066 |
show "?B <= ?A" |
|
1067 |
proof |
|
1068 |
fix x assume "x : ?B" |
|
1069 |
then obtain i where i: "i : {k..n+k}" "x : M(i)" by auto |
|
1070 |
hence "i-k\<le>n & x : M((i-k)+k)" by auto |
|
1071 |
thus "x : ?A" by blast |
|
1072 |
qed |
|
1073 |
qed |
|
1074 |
||
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1075 |
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
|
1076 |
by (auto simp add: atLeast0LessThan) |
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1077 |
|
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1078 |
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
|
1079 |
by (subst UN_UN_finite_eq [symmetric]) blast |
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1080 |
|
33044 | 1081 |
lemma UN_finite2_subset: |
1082 |
"(!!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)" |
|
1083 |
apply (rule UN_finite_subset) |
|
1084 |
apply (subst UN_UN_finite_eq [symmetric, of B]) |
|
1085 |
apply blast |
|
1086 |
done |
|
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1087 |
|
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1088 |
lemma UN_finite2_eq: |
33044 | 1089 |
"(!!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)" |
1090 |
apply (rule subset_antisym) |
|
1091 |
apply (rule UN_finite2_subset, blast) |
|
1092 |
apply (rule UN_finite2_subset [where k=k]) |
|
35216 | 1093 |
apply (force simp add: atLeastLessThan_add_Un [of 0]) |
33044 | 1094 |
done |
32596
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1095 |
|
bd68c04dace1
New theorems for proving equalities and inclusions involving unions
paulson
parents:
32456
diff
changeset
|
1096 |
|
60758 | 1097 |
subsubsection \<open>Cardinality\<close> |
14485 | 1098 |
|
15045 | 1099 |
lemma card_lessThan [simp]: "card {..<u} = u" |
15251 | 1100 |
by (induct u, simp_all add: lessThan_Suc) |
14485 | 1101 |
|
1102 |
lemma card_atMost [simp]: "card {..u} = Suc u" |
|
1103 |
by (simp add: lessThan_Suc_atMost [THEN sym]) |
|
1104 |
||
15045 | 1105 |
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
|
1106 |
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
|
1107 |
have "{l..<u} = (%x. x + l) ` {..<u-l}" |
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
|
1108 |
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
|
1109 |
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
|
1110 |
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
|
1111 |
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
|
1112 |
then have "card {l..<u} = card {..<u-l}" |
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
|
1113 |
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
|
1114 |
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
|
1115 |
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
|
1116 |
qed |
14485 | 1117 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1118 |
lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l" |
14485 | 1119 |
by (subst atLeastLessThanSuc_atLeastAtMost [THEN sym], simp) |
1120 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1121 |
lemma card_greaterThanAtMost [simp]: "card {l<..u} = u - l" |
14485 | 1122 |
by (subst atLeastSucAtMost_greaterThanAtMost [THEN sym], simp) |
1123 |
||
15045 | 1124 |
lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l" |
14485 | 1125 |
by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp) |
1126 |
||
26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
1127 |
lemma ex_bij_betw_nat_finite: |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
1128 |
"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
|
1129 |
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
|
1130 |
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
|
1131 |
done |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
1132 |
|
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
1133 |
lemma ex_bij_betw_finite_nat: |
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
1134 |
"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
|
1135 |
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
|
1136 |
|
31438 | 1137 |
lemma finite_same_card_bij: |
1138 |
"finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B" |
|
1139 |
apply(drule ex_bij_betw_finite_nat) |
|
1140 |
apply(drule ex_bij_betw_nat_finite) |
|
1141 |
apply(auto intro!:bij_betw_trans) |
|
1142 |
done |
|
1143 |
||
1144 |
lemma ex_bij_betw_nat_finite_1: |
|
1145 |
"finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M" |
|
1146 |
by (rule finite_same_card_bij) auto |
|
1147 |
||
40703
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1148 |
lemma bij_betw_iff_card: |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1149 |
assumes FIN: "finite A" and FIN': "finite B" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1150 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1151 |
using assms |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1152 |
proof(auto simp add: bij_betw_same_card) |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1153 |
assume *: "card A = card B" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1154 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1155 |
using FIN ex_bij_betw_finite_nat by blast |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1156 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1157 |
using FIN' ex_bij_betw_nat_finite by blast |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1158 |
ultimately have "bij_betw (g o f) A B" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1159 |
using * by (auto simp add: bij_betw_trans) |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1160 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1161 |
qed |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1162 |
|
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1163 |
lemma inj_on_iff_card_le: |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1164 |
assumes FIN: "finite A" and FIN': "finite B" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1165 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1166 |
proof (safe intro!: card_inj_on_le) |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1167 |
assume *: "card A \<le> card B" |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1168 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1169 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1170 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1171 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1172 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1173 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1174 |
moreover |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1175 |
{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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1176 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1177 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1178 |
} |
d1fc454d6735
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1179 |
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 HOL-image.
hoelzl
parents:
39302
diff
changeset
|
1180 |
qed (insert assms, auto) |
26105
ae06618225ec
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and
nipkow
parents:
26072
diff
changeset
|
1181 |
|
60758 | 1182 |
subsection \<open>Intervals of integers\<close> |
14485 | 1183 |
|
15045 | 1184 |
lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}" |
14485 | 1185 |
by (auto simp add: atLeastAtMost_def atLeastLessThan_def) |
1186 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1187 |
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" |
14485 | 1188 |
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) |
1189 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1190 |
lemma atLeastPlusOneLessThan_greaterThanLessThan_int: |
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1191 |
"{l+1..<u} = {l<..<u::int}" |
14485 | 1192 |
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) |
1193 |
||
60758 | 1194 |
subsubsection \<open>Finiteness\<close> |
14485 | 1195 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1196 |
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> |
15045 | 1197 |
{(0::int)..<u} = int ` {..<nat u}" |
14485 | 1198 |
apply (unfold image_def lessThan_def) |
1199 |
apply auto |
|
1200 |
apply (rule_tac x = "nat x" in exI) |
|
35216 | 1201 |
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) |
14485 | 1202 |
done |
1203 |
||
15045 | 1204 |
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" |
47988 | 1205 |
apply (cases "0 \<le> u") |
14485 | 1206 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
1207 |
apply (rule finite_imageI) |
|
1208 |
apply auto |
|
1209 |
done |
|
1210 |
||
15045 | 1211 |
lemma finite_atLeastLessThan_int [iff]: "finite {l..<u::int}" |
1212 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
|
14485 | 1213 |
apply (erule subst) |
1214 |
apply (rule finite_imageI) |
|
1215 |
apply (rule finite_atLeastZeroLessThan_int) |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
1216 |
apply (rule image_add_int_atLeastLessThan) |
14485 | 1217 |
done |
1218 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1219 |
lemma finite_atLeastAtMost_int [iff]: "finite {l..(u::int)}" |
14485 | 1220 |
by (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym], simp) |
1221 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1222 |
lemma finite_greaterThanAtMost_int [iff]: "finite {l<..(u::int)}" |
14485 | 1223 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
1224 |
||
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1225 |
lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}" |
14485 | 1226 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
1227 |
||
24853 | 1228 |
|
60758 | 1229 |
subsubsection \<open>Cardinality\<close> |
14485 | 1230 |
|
15045 | 1231 |
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" |
47988 | 1232 |
apply (cases "0 \<le> u") |
14485 | 1233 |
apply (subst image_atLeastZeroLessThan_int, assumption) |
1234 |
apply (subst card_image) |
|
1235 |
apply (auto simp add: inj_on_def) |
|
1236 |
done |
|
1237 |
||
15045 | 1238 |
lemma card_atLeastLessThan_int [simp]: "card {l..<u} = nat (u - l)" |
1239 |
apply (subgoal_tac "card {l..<u} = card {0..<u-l}") |
|
14485 | 1240 |
apply (erule ssubst, rule card_atLeastZeroLessThan_int) |
15045 | 1241 |
apply (subgoal_tac "(%x. x + l) ` {0..<u-l} = {l..<u}") |
14485 | 1242 |
apply (erule subst) |
1243 |
apply (rule card_image) |
|
1244 |
apply (simp add: inj_on_def) |
|
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset
|
1245 |
apply (rule image_add_int_atLeastLessThan) |
14485 | 1246 |
done |
1247 |
||
1248 |
lemma card_atLeastAtMost_int [simp]: "card {l..u} = nat (u - l + 1)" |
|
29667 | 1249 |
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) |
1250 |
apply (auto simp add: algebra_simps) |
|
1251 |
done |
|
14485 | 1252 |
|
15418
e28853da5df5
removed two looping simplifications in SetInterval.thy; deleted the .ML file
paulson
parents:
15402
diff
changeset
|
1253 |
lemma card_greaterThanAtMost_int [simp]: "card {l<..u} = nat (u - l)" |
29667 | 1254 |
by (subst atLeastPlusOneAtMost_greaterThanAtMost_int [THEN sym], simp) |
14485 | 1255 |
|
15045 | 1256 |
lemma card_greaterThanLessThan_int [simp]: "card {l<..<u} = nat (u - (l + 1))" |
29667 | 1257 |
by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp) |
14485 | 1258 |
|
27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1259 |
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
|
1260 |
proof - |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1261 |
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
|
1262 |
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
|
1263 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1264 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1265 |
lemma card_less: |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1266 |
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
|
1267 |
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
|
1268 |
proof - |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1269 |
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
|
1270 |
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
|
1271 |
qed |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1272 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1273 |
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 | 1274 |
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
|
1275 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1276 |
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
|
1277 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1278 |
apply (case_tac x) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1279 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1280 |
apply (case_tac xa) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1281 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1282 |
apply (case_tac xa) |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1283 |
apply auto |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1284 |
done |
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1285 |
|
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset
|
1286 |
lemma card_less_Suc: |