author  hoelzl 
Wed, 20 Feb 2013 12:04:42 +0100  
changeset 51329  4a3c453f99a1 
parent 51328  d63ec23c9125 
child 51334  fd531bd984d8 
permissions  rwrr 
47317
432b29a96f61
modernized obsolete oldstyle theory name with proper newstyle underscore
huffman
parents:
47222
diff
changeset

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

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

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

4 
Author: Jeremy Avigad 
8924  5 

13735  6 
lessThan, greaterThan, atLeast, atMost and twosided intervals 
8924  7 
*) 
8 

14577  9 
header {* Set intervals *} 
10 

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

11 
theory Set_Interval 
33318
ddd97d9dfbfb
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
haftmann
parents:
33044
diff
changeset

12 
imports Int Nat_Transfer 
15131  13 
begin 
8924  14 

24691  15 
context ord 
16 
begin 

44008  17 

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

19 
lessThan :: "'a => 'a set" ("(1{..<_})") where 
25062  20 
"{..<u} == {x. x < u}" 
24691  21 

22 
definition 

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

23 
atMost :: "'a => 'a set" ("(1{.._})") where 
25062  24 
"{..u} == {x. x \<le> u}" 
24691  25 

26 
definition 

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

27 
greaterThan :: "'a => 'a set" ("(1{_<..})") where 
25062  28 
"{l<..} == {x. l<x}" 
24691  29 

30 
definition 

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

31 
atLeast :: "'a => 'a set" ("(1{_..})") where 
25062  32 
"{l..} == {x. l\<le>x}" 
24691  33 

34 
definition 

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

24691  37 

38 
definition 

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

24691  41 

42 
definition 

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

24691  45 

46 
definition 

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

24691  49 

50 
end 

8924  51 

13735  52 

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

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

14418  57 
syntax 
36364
0e2679025aeb
fix syntax precedence declarations for UNION, INTER, SUP, INF
huffman
parents:
36307
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

75 
translations 

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

15045  77 
"UN i<n. A" == "UN i:{..<n}. A" 
14418  78 
"INT i<=n. A" == "INT i:{..n}. A" 
15045  79 
"INT i<n. A" == "INT i:{..<n}. A" 
14418  80 

81 

14485  82 
subsection {* Various equivalences *} 
13735  83 

25062  84 
lemma (in ord) lessThan_iff [iff]: "(i: lessThan k) = (i<k)" 
13850  85 
by (simp add: lessThan_def) 
13735  86 

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

87 
lemma Compl_lessThan [simp]: 
13735  88 
"!!k:: 'a::linorder. lessThan k = atLeast k" 
13850  89 
apply (auto simp add: lessThan_def atLeast_def) 
13735  90 
done 
91 

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

13735  94 

25062  95 
lemma (in ord) greaterThan_iff [iff]: "(i: greaterThan k) = (k<i)" 
13850  96 
by (simp add: greaterThan_def) 
13735  97 

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

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

100 
by (auto simp add: greaterThan_def atMost_def) 
13735  101 

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

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

104 
apply (rule double_complement) 
13735  105 
done 
106 

25062  107 
lemma (in ord) atLeast_iff [iff]: "(i: atLeast k) = (k<=i)" 
13850  108 
by (simp add: atLeast_def) 
13735  109 

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

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

112 
by (auto simp add: lessThan_def atLeast_def) 
13735  113 

25062  114 
lemma (in ord) atMost_iff [iff]: "(i: atMost k) = (i<=k)" 
13850  115 
by (simp add: atMost_def) 
13735  116 

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

13850  119 

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

122 

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

124 
by auto 

13850  125 

14485  126 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  127 

128 
lemma atLeast_subset_iff [iff]: 

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

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

130 
by (blast intro: order_trans) 
13850  131 

132 
lemma atLeast_eq_iff [iff]: 

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

133 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  134 
by (blast intro: order_antisym order_trans) 
135 

136 
lemma greaterThan_subset_iff [iff]: 

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

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

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

139 
apply (subst linorder_not_less [symmetric], blast) 
13850  140 
done 
141 

142 
lemma greaterThan_eq_iff [iff]: 

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

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

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

145 
apply (erule equalityE) 
29709  146 
apply simp_all 
13850  147 
done 
148 

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

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

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

152 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  153 
by (blast intro: order_antisym order_trans) 
154 

155 
lemma lessThan_subset_iff [iff]: 

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

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

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

158 
apply (subst linorder_not_less [symmetric], blast) 
13850  159 
done 
160 

161 
lemma lessThan_eq_iff [iff]: 

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

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

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

164 
apply (erule equalityE) 
29709  165 
apply simp_all 
13735  166 
done 
167 

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

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

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

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

171 
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) 
13735  172 

13850  173 
subsection {*Twosided intervals*} 
13735  174 

24691  175 
context ord 
176 
begin 

177 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

178 
lemma greaterThanLessThan_iff [simp,no_atp]: 
25062  179 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  180 
by (simp add: greaterThanLessThan_def) 
181 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

182 
lemma atLeastLessThan_iff [simp,no_atp]: 
25062  183 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  184 
by (simp add: atLeastLessThan_def) 
185 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

186 
lemma greaterThanAtMost_iff [simp,no_atp]: 
25062  187 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  188 
by (simp add: greaterThanAtMost_def) 
189 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

190 
lemma atLeastAtMost_iff [simp,no_atp]: 
25062  191 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  192 
by (simp add: atLeastAtMost_def) 
193 

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

194 
text {* The above four lemmas could be declared as iffs. Unfortunately this 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

195 
breaks many proofs. Since it only helps blast, it is better to leave well 
10cd49e0c067
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
nipkow
parents:
32408
diff
changeset

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

197 

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

200 

24691  201 
end 
13735  202 

32400  203 
subsubsection{* Emptyness, singletons, subset *} 
15554  204 

24691  205 
context order 
206 
begin 

15554  207 

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

210 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

211 

212 
lemma atLeastatMost_empty_iff[simp]: 

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

214 
by auto (blast intro: order_trans) 

215 

216 
lemma atLeastatMost_empty_iff2[simp]: 

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

218 
by auto (blast intro: order_trans) 

219 

220 
lemma atLeastLessThan_empty[simp]: 

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

222 
by(auto simp: atLeastLessThan_def) 

24691  223 

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

226 
by auto (blast intro: le_less_trans) 

227 

228 
lemma atLeastLessThan_empty_iff2[simp]: 

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

230 
by auto (blast intro: le_less_trans) 

15554  231 

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

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

237 

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

239 
by auto (blast intro: less_le_trans) 

240 

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

25062  244 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  245 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
246 

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

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

248 

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

251 
unfolding atLeastAtMost_def atLeast_def atMost_def 

252 
by (blast intro: order_trans) 

253 

254 
lemma atLeastatMost_psubset_iff: 

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

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

257 
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 
32400  258 

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

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

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

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

262 
assume "{a..b} = {c}" 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

263 
hence "\<not> (\<not> a \<le> b)" unfolding atLeastatMost_empty_iff[symmetric] by simp 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

264 
moreover with `{a..b} = {c}` have "c \<le> a \<and> b \<le> c" by auto 
0f67561ed5a6
Added atLeastAtMost_singleton_iff, atLeastAtMost_singleton'
hoelzl
parents:
36755
diff
changeset

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

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

267 

24691  268 
end 
14485  269 

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

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

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

272 

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

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

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

275 
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

276 

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

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

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

279 
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

280 

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

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

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

285 

286 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

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

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

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

290 

291 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

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

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

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

295 

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

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

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

300 

301 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

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

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

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

305 

306 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

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

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

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

310 

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

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

312 

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

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

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

315 

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

316 
lemma greaterThan_non_empty: "{x <..} \<noteq> {}" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

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

318 

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

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

320 

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

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

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

323 

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

324 
lemma lessThan_non_empty: "{..< x} \<noteq> {}" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

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

326 

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

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

328 

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

331 
apply (auto simp:subset_eq Ball_def) 

332 
apply(frule_tac x=a in spec) 

333 
apply(erule_tac x=d in allE) 

334 
apply (simp add: less_imp_le) 

335 
done 

336 

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

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

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

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

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

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

342 

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

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

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

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

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

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

348 

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

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

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

351 

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

352 
lemma atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot" 
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

353 
by (auto simp: set_eq_iff intro: le_bot) 
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

354 

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

355 
lemma atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top" 
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

356 
by (auto simp: set_eq_iff intro: top_le) 
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

357 

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

358 
lemma atLeastAtMost_eq_UNIV_iff: "{x..y} = UNIV \<longleftrightarrow> (x = bot \<and> y = top)" 
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

359 
by (auto simp: set_eq_iff intro: top_le le_bot) 
d63ec23c9125
move auxiliary lemmas from Library/Extended_Reals to HOL image
hoelzl
parents:
51152
diff
changeset

360 

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

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

362 

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

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

364 

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

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

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

367 

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

368 
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

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

370 

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

371 
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

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

373 

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

374 
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

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

376 

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

377 
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

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

379 

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

380 
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

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

382 

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

383 
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

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

385 

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

386 
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

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

388 

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

389 
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

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

391 

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

394 

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

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

396 

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

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

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

399 

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

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

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

402 
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

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

404 
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

405 
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

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

407 

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

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

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

410 
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

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

412 
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

413 
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

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

415 

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

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

417 

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

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

419 
fixes x y :: "'a :: {complete_lattice, inner_dense_linorder}" 
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
51328
diff
changeset

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

421 
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

422 
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

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

424 
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

425 
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

426 
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

427 

14485  428 
subsection {* Intervals of natural numbers *} 
429 

15047  430 
subsubsection {* The Constant @{term lessThan} *} 
431 

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

434 

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

436 
by (simp add: lessThan_def less_Suc_eq, blast) 

437 

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

441 

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

443 
proof safe 

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

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

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

447 
qed 

448 

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

451 

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

453 
by blast 

454 

15047  455 
subsubsection {* The Constant @{term greaterThan} *} 
456 

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

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

460 
done 

461 

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

463 
apply (simp add: greaterThan_def) 

464 
apply (auto elim: linorder_neqE) 

465 
done 

466 

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

468 
by blast 

469 

15047  470 
subsubsection {* The Constant @{term atLeast} *} 
471 

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

474 

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

476 
apply (simp add: atLeast_def) 

477 
apply (simp add: Suc_le_eq) 

478 
apply (simp add: order_le_less, blast) 

479 
done 

480 

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

482 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

483 

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

485 
by blast 

486 

15047  487 
subsubsection {* The Constant @{term atMost} *} 
488 

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

491 

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

493 
apply (simp add: atMost_def) 

494 
apply (simp add: less_Suc_eq order_le_less, blast) 

495 
done 

496 

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

498 
by blast 

499 

15047  500 
subsubsection {* The Constant @{term atLeastLessThan} *} 
501 

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

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

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

507 
specific concept to a more general one. *} 

28068  508 

15047  509 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  510 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  511 

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

514 

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

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

516 
atLeast0AtMost[symmetric, code_unfold] 
24449  517 

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

15047  519 
by (simp add: atLeastLessThan_def) 
24449  520 

15047  521 
subsubsection {* Intervals of nats with @{term Suc} *} 
522 

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

524 
lemma atLeastLessThanSuc: 

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

526 
by (auto simp add: atLeastLessThan_def) 
15047  527 

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

528 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  529 
by (auto simp add: atLeastLessThan_def) 
16041  530 
(* 
15047  531 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
532 
by (induct k, simp_all add: atLeastLessThanSuc) 

533 

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

535 
by (auto simp add: atLeastLessThan_def) 

16041  536 
*) 
15045  537 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  538 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
539 

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

540 
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

541 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  542 
greaterThanAtMost_def) 
543 

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

544 
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

545 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  546 
greaterThanLessThan_def) 
547 

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

550 

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

553 

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

556 
lemma atLeastAtMostPlus1_int_conv: 

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

558 
by (auto intro: set_eqI) 

559 

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

562 
apply (simp_all add: atLeastLessThanSuc) 

563 
done 

564 

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

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

566 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

580 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

594 

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

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

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

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

598 

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

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

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

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

602 

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

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

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

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

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

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

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

609 

37664  610 
lemma image_minus_const_atLeastLessThan_nat: 
611 
fixes c :: nat 

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

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

614 
(is "_ = ?right") 

615 
proof safe 

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

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

618 
proof cases 

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

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

621 
next 

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

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

624 
qed 

625 
qed auto 

626 

51152  627 
lemma image_int_atLeastLessThan: "int ` {a..<b} = {int a..<int b}" 
628 
by(auto intro!: image_eqI[where x="nat x", standard]) 

629 

35580  630 
context ordered_ab_group_add 
631 
begin 

632 

633 
lemma 

634 
fixes x :: 'a 

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

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

637 
proof safe 

638 
fix y assume "y < x" 

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

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

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

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

643 
next 

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

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

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

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

648 
qed simp_all 

649 

650 
lemma 

651 
fixes x :: 'a 

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

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

654 
proof  

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

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

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

658 
by (simp_all add: image_image 

659 
del: image_uminus_greaterThan image_uminus_atLeast) 

660 
qed 

661 

662 
lemma 

663 
fixes x :: 'a 

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

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

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

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

668 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

669 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

670 
end 

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

671 

14485  672 
subsubsection {* Finiteness *} 
673 

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

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

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

679 

680 
lemma finite_greaterThanLessThan [iff]: 

15045  681 
fixes l :: nat shows "finite {l<..<u}" 
14485  682 
by (simp add: greaterThanLessThan_def) 
683 

684 
lemma finite_atLeastLessThan [iff]: 

15045  685 
fixes l :: nat shows "finite {l..<u}" 
14485  686 
by (simp add: atLeastLessThan_def) 
687 

688 
lemma finite_greaterThanAtMost [iff]: 

15045  689 
fixes l :: nat shows "finite {l<..u}" 
14485  690 
by (simp add: greaterThanAtMost_def) 
691 

692 
lemma finite_atLeastAtMost [iff]: 

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

694 
by (simp add: atLeastAtMost_def) 

695 

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

701 
done 

702 

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

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

706 
proof 

707 
assume f:?F show ?B 

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

709 
next 

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

711 
qed 

712 

713 
lemma finite_nat_set_iff_bounded_le: 

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

715 
apply(simp add:finite_nat_set_iff_bounded) 

716 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

717 
done 

718 

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

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

14485  722 

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

725 

726 
lemma subset_card_intvl_is_intvl: 

727 
"A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P") 

728 
proof cases 

729 
assume "finite A" 

730 
thus "PROP ?P" 

32006  731 
proof(induct A rule:finite_linorder_max_induct) 
24853  732 
case empty thus ?case by auto 
733 
next 

33434  734 
case (insert b A) 
24853  735 
moreover hence "b ~: A" by auto 
736 
moreover have "A <= {k..<k+card A}" and "b = k+card A" 

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

737 
using `b ~: A` insert by fastforce+ 
24853  738 
ultimately show ?case by auto 
739 
qed 

740 
next 

741 
assume "~finite A" thus "PROP ?P" by simp 

742 
qed 

743 

744 

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

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

746 

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

749 
proof 

750 
show "?A <= ?B" 

751 
proof 

752 
fix x assume "x : ?A" 

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

754 
show "x : ?B" 

755 
proof(cases i) 

756 
case 0 with i show ?thesis by simp 

757 
next 

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

759 
qed 

760 
qed 

761 
next 

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

763 
qed 

764 

765 
lemma UN_le_add_shift: 

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

767 
proof 

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

768 
show "?A <= ?B" by fastforce 
36755  769 
next 
770 
show "?B <= ?A" 

771 
proof 

772 
fix x assume "x : ?B" 

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

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

775 
thus "x : ?A" by blast 

776 
qed 

777 
qed 

778 

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

779 
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

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

781 

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

782 
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

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

784 

33044  785 
lemma UN_finite2_subset: 
786 
"(!!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)" 

787 
apply (rule UN_finite_subset) 

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

789 
apply blast 

790 
done 

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

791 

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

792 
lemma UN_finite2_eq: 
33044  793 
"(!!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)" 
794 
apply (rule subset_antisym) 

795 
apply (rule UN_finite2_subset, blast) 

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

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

799 

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

800 

14485  801 
subsubsection {* Cardinality *} 
802 

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

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

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

808 

15045  809 
lemma card_atLeastLessThan [simp]: "card {l..<u} = u  l" 
810 
apply (subgoal_tac "card {l..<u} = card {..<ul}") 

14485  811 
apply (erule ssubst, rule card_lessThan) 
15045  812 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  813 
apply (erule subst) 
814 
apply (rule card_image) 

815 
apply (simp add: inj_on_def) 

816 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

817 
apply (rule_tac x = "x  l" in exI) 

818 
apply arith 

819 
done 

820 

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

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

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

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

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

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

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

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

832 
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

833 
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

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

835 

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

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

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

838 
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

839 

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

842 
apply(drule ex_bij_betw_finite_nat) 

843 
apply(drule ex_bij_betw_nat_finite) 

844 
apply(auto intro!:bij_betw_trans) 

845 
done 

846 

847 
lemma ex_bij_betw_nat_finite_1: 

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

849 
by (rule finite_same_card_bij) auto 

850 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

865 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

884 

14485  885 
subsection {* Intervals of integers *} 
886 

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

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

890 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  891 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
892 

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

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

894 
"{l+1..<u} = {l<..<u::int}" 
14485  895 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
896 

897 
subsubsection {* Finiteness *} 

898 

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

899 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  900 
{(0::int)..<u} = int ` {..<nat u}" 
14485  901 
apply (unfold image_def lessThan_def) 
902 
apply auto 

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

35216  904 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  905 
done 
906 

15045  907 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
47988  908 
apply (cases "0 \<le> u") 
14485  909 
apply (subst image_atLeastZeroLessThan_int, assumption) 
910 
apply (rule finite_imageI) 

911 
apply auto 

912 
done 

913 

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

14485  916 
apply (erule subst) 
917 
apply (rule finite_imageI) 

918 
apply (rule finite_atLeastZeroLessThan_int) 

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

919 
apply (rule image_add_int_atLeastLessThan) 
14485  920 
done 
921 

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

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

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

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

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

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

24853  931 

14485  932 
subsubsection {* Cardinality *} 
933 

15045  934 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
47988  935 
apply (cases "0 \<le> u") 
14485  936 
apply (subst image_atLeastZeroLessThan_int, assumption) 
937 
apply (subst card_image) 

938 
apply (auto simp add: inj_on_def) 

939 
done 

940 

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

14485  943 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  944 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  945 
apply (erule subst) 
946 
apply (rule card_image) 

947 
apply (simp add: inj_on_def) 

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

948 
apply (rule image_add_int_atLeastLessThan) 
14485  949 
done 
950 

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

29667  952 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
953 
apply (auto simp add: algebra_simps) 

954 
done 

14485  955 

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

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

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

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

962 
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

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

964 
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

965 
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

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

967 

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

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

969 
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

970 
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

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

972 
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

973 
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

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

975 

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

976 
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  977 
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

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

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

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

981 
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

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

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

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

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

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

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

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

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

990 

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

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

992 
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

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

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

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

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

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

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

999 
from finite_M_bounded_by_nat[of "\<lambda>x. x \<in> M" "Suc i"] have "Suc (card {k. Suc k \<in> M \<and> k < i}) = card (insert 0 ({k \<in> M. k < Suc i}  {0}))" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

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

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

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

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

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

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

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

1008 

14485  1009 

13850  1010 
subsection {*Lemmas useful with the summation operator setsum*} 
1011 

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

1012 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  1013 

14577  1014 
subsubsection {* Disjoint Unions *} 
13735  1015 

14577  1016 
text {* Singletons and open intervals *} 
13735  1017 

1018 
lemma ivl_disj_un_singleton: 

15045  1019 
"{l::'a::linorder} Un {l<..} = {l..}" 
1020 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

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

1025 
by auto 
13735  1026 

14577  1027 
text {* One and twosided intervals *} 
13735  1028 

1029 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

1038 
by auto 
13735  1039 

14577  1040 
text {* Two and twosided intervals *} 
13735  1041 

1042 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

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

1051 
by auto 
13735  1052 

1053 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

1054 

14577  1055 
subsubsection {* Disjoint Intersections *} 
13735  1056 

14577  1057 
text {* One and twosided intervals *} 
13735  1058 

1059 
lemma ivl_disj_int_one: 

15045  1060 
"{..l::'a::order} Int {l<..<u} = {}" 
1061 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

1068 
by auto 
13735  1069 

14577  1070 
text {* Two and twosided intervals *} 
13735  1071 

1072 
lemma ivl_disj_int_two: 

15045  1073 
"{l::'a::order<..<m} Int {m..<u} = {}" 
1074 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

1081 
by auto 
13735  1082 

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

1083 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  1084 

15542  1085 
subsubsection {* Some Differences *} 
1086 

1087 
lemma ivl_diff[simp]: 

1088 
"i \<le> n \<Longrightarrow> {i..<m}  {i..<n} = {n..<(m::'a::linorder)}" 

1089 
by(auto) 

1090 

1091 

1092 
subsubsection {* Some Subset Conditions *} 

1093 

35828
46cfc4b8112e
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
blanchet
parents:
35644
diff
changeset

1094 
lemma ivl_subset [simp,no_atp]: 
15542  1095 
"({i..<j} \<subseteq> {m..<n}) = (j \<le> i  m \<le> i & j \<le> (n::'a::linorder))" 
1096 
apply(auto simp:linorder_not_le) 

1097 
apply(rule ccontr) 

1098 
apply(insert linorder_le_less_linear[of i n]) 

1099 
apply(clarsimp simp:linorder_not_le) 

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

1100 
apply(fastforce) 
15542  1101 
done 
1102 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1103 

15042  1104 
subsection {* Summation indexed over intervals *} 
1105 

1106 
syntax 

1107 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10) 

15048  1108 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10) 
16052  1109 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10) 
1110 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10) 

15042  1111 
syntax (xsymbols) 
1112 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  1113 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  1114 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
1115 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

15042  1116 
syntax (HTML output) 
1117 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10) 

15048  1118 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10) 
16052  1119 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10) 
1120 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10) 

15056  1121 
syntax (latex_sum output) 
15052  1122 
"_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
1123 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) 

1124 
"_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 

1125 
("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) 

16052  1126 
"_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
1127 
("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) 

15052  1128 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
16052  1129 
("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10) 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1130 

15048  1131 
translations 
28853
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1132 
"\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1133 
"\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1134 
"\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}" 
69eb69659bf3
Added new fold operator and renamed the old oe to fold_image.
nipkow
parents:
28068
diff
changeset

1135 
"\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}" 
15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1136 

15052  1137 
text{* The above introduces some pretty alternative syntaxes for 
15056  1138 
summation over intervals: 
15052  1139 
\begin{center} 
1140 
\begin{tabular}{lll} 

15056  1141 
Old & New & \LaTeX\\ 
1142 
@{term[source]"\<Sum>x\<in>{a..b}. e"} & @{term"\<Sum>x=a..b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..b. e"}\\ 

1143 
@{term[source]"\<Sum>x\<in>{a..<b}. e"} & @{term"\<Sum>x=a..<b. e"} & @{term[mode=latex_sum]"\<Sum>x=a..<b. e"}\\ 

16052  1144 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  1145 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  1146 
\end{tabular} 
1147 
\end{center} 

15056  1148 
The left column shows the term before introduction of the new syntax, 
1149 
the middle column shows the new (default) syntax, and the right column 

1150 
shows a special syntax. The latter is only meaningful for latex output 

1151 
and has to be activated explicitly by setting the print mode to 

21502  1152 
@{text latex_sum} (e.g.\ via @{text "mode = latex_sum"} in 
15056  1153 
antiquotations). It is not the default \LaTeX\ output because it only 
1154 
works well with italicstyle formulae, not ttstyle. 

15052  1155 

1156 
Note that for uniformity on @{typ nat} it is better to use 

1157 
@{term"\<Sum>x::nat=0..<n. e"} rather than @{text"\<Sum>x<n. e"}: @{text setsum} may 

1158 
not provide all lemmas available for @{term"{m..<n}"} also in the 

1159 
special form for @{term"{..<n}"}. *} 

1160 

15542  1161 
text{* This congruence rule should be used for sums over intervals as 
1162 
the standard theorem @{text[source]setsum_cong} does not work well 

1163 
with the simplifier who adds the unsimplified premise @{term"x:B"} to 

1164 
the context. *} 

1165 

1166 
lemma setsum_ivl_cong: 

1167 
"\<lbrakk>a = c; b = d; !!x. \<lbrakk> c \<le> x; x < d \<rbrakk> \<Longrightarrow> f x = g x \<rbrakk> \<Longrightarrow> 

1168 
setsum f {a..<b} = setsum g {c..<d}" 

1169 
by(rule setsum_cong, simp_all) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1170 

16041  1171 
(* FIXME why are the following simp rules but the corresponding eqns 
1172 
on intervals are not? *) 

1173 

16052  1174 
lemma setsum_atMost_Suc[simp]: "(\<Sum>i \<le> Suc n. f i) = (\<Sum>i \<le> n. f i) + f(Suc n)" 
1175 
by (simp add:atMost_Suc add_ac) 

1176 

16041  1177 
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" 
1178 
by (simp add:lessThan_Suc add_ac) 

15041
a6b1f0cef7b3
Got rid of Summation and made it a translation into setsum instead.
nipkow
parents:
14846
diff
changeset

1179 

15911  1180 
lemma setsum_cl_ivl_Suc[simp]: 
15561  1181 
"setsum f {m..Suc n} = (if Suc n < m then 0 else setsum f {m..n} + f(Suc n))" 
1182 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

1183 

15911  1184 
lemma setsum_op_ivl_Suc[simp]: 
15561  1185 
"setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))" 
1186 
by (auto simp:add_ac atLeastLessThanSuc) 

16041  1187 
(* 
15561  1188 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
1189 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

1190 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  1191 
*) 
28068  1192 

1193 
lemma setsum_head: 

1194 
fixes n :: nat 

1195 
assumes mn: "m <= n" 

1196 
shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs") 

1197 
proof  

1198 
from mn 

1199 
have "{m..n} = {m} \<union> {m<..n}" 

1200 
by (auto intro: ivl_disj_un_singleton) 

1201 
hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)" 

1202 
by (simp add: atLeast0LessThan) 

1203 
also have "\<dots> = ?rhs" by simp 

1204 
finally show ?thesis . 

1205 
qed 

1206 

1207 
lemma setsum_head_Suc: 

1208 
"m \<le> n \<Longrightarrow> setsum f {m..n} = f m + setsum f {Suc m..n}" 

1209 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

1210 

1211 
lemma setsum_head_upt_Suc: 

1212 
"m < n \<Longrightarrow> setsum f {m..<n} = f m + setsum f {Suc m..<n}" 

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

1213 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  1214 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  1215 
done 
1216 

31501  1217 
lemma setsum_ub_add_nat: assumes "(m::nat) \<le> n + 1" 
1218 
shows "setsum f {m..n + p} = setsum f {m..n} + setsum f {n + 1..n + p}" 

1219 
proof 

1220 
have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using `m \<le> n+1` by auto 

1221 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

1222 
atLeastSucAtMost_greaterThanAtMost) 

1223 
qed 

28068  1224 

15539  1225 
lemma setsum_add_nat_ivl: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 
1226 
setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}" 

1227 
by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un) 

1228 

1229 
lemma setsum_diff_nat_ivl: 

1230 
fixes f :: "nat \<Rightarrow> 'a::ab_group_add" 

1231 
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> 

1232 
setsum f {m..<p}  setsum f {m..<n} = setsum f {n..<p}" 

1233 
using setsum_add_nat_ivl [of m n p f,symmetric] 

1234 
apply (simp add: add_ac) 

1235 
done 

1236 

31505  1237 
lemma setsum_natinterval_difff: 
1238 
fixes f:: "nat \<Rightarrow> ('a::ab_group_add)" 

1239 
shows "setsum (\<lambda>k. f k  f(k + 1)) {(m::nat) .. n} = 

1240 
(if m <= n then f m  f(n + 1) else 0)" 

1241 
by (induct n, auto simp add: algebra_simps not_le le_Suc_eq) 

1242 

44008  1243 
lemma setsum_restrict_set': 
1244 
"finite A \<Longrightarrow> setsum f {x \<in> A. x \<in> B} = (\<Sum>x\<in>A. if x \<in> B then f x else 0)" 

1245 
by (simp add: setsum_restrict_set [symmetric] Int_def) 

1246 

1247 
lemma setsum_restrict_set'': 

1248 
"finite A \<Longrightarrow> setsum f {x \<in> A. P x} = (\<Sum>x\<in>A. if P x then f x else 0)" 

1249 
by (simp add: setsum_restrict_set' [of A f "{x. P x}", simplified mem_Collect_eq]) 

31509  1250 

1251 
lemma setsum_setsum_restrict: 

44008  1252 
"finite S \<Longrightarrow> finite T \<Longrightarrow> 
1253 
setsum (\<lambda>x. setsum (\<lambda>y. f x y) {y. y \<in> T \<and> R x y}) S = setsum (\<lambda>y. setsum (\<lambda>x. f x y) {x. x \<in> S \<and> R x y}) T" 

1254 
by (simp add: setsum_restrict_set'') (rule setsum_commute) 

31509  1255 

1256 
lemma setsum_image_gen: assumes fS: "finite S" 

1257 
shows "setsum g S = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 

1258 
proof 

1259 
{ fix x assume "x \<in> S" then have "{y. y\<in> f`S \<and> f x = y} = {f x}" by auto } 

1260 
hence "setsum g S = setsum (\<lambda>x. setsum (\<lambda>y. g x) {y. y\<in> f`S \<and> f x = y}) S" 

1261 
by simp 

1262 
also have "\<dots> = setsum (\<lambda>y. setsum g {x. x \<in> S \<and> f x = y}) (f ` S)" 

1263 
by (rule setsum_setsum_restrict[OF fS finite_imageI[OF fS]]) 

1264 
finally show ?thesis . 

1265 
qed 

1266 

35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1267 
lemma setsum_le_included: 
36307
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1268 
fixes f :: "'a \<Rightarrow> 'b::ordered_comm_monoid_add" 
35171
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1269 
assumes "finite s" "finite t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1270 
and "\<forall>y\<in>t. 0 \<le> g y" "(\<forall>x\<in>s. \<exists>y\<in>t. i y = x \<and> f x \<le> g y)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1271 
shows "setsum f s \<le> setsum g t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1272 
proof  
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1273 
have "setsum f s \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) s" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1274 
proof (rule setsum_mono) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1275 
fix y assume "y \<in> s" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1276 
with assms obtain z where z: "z \<in> t" "y = i z" "f y \<le> g z" by auto 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1277 
with assms show "f y \<le> setsum g {x \<in> t. i x = y}" (is "?A y \<le> ?B y") 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1278 
using order_trans[of "?A (i z)" "setsum g {z}" "?B (i z)", intro] 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1279 
by (auto intro!: setsum_mono2) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1280 
qed 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1281 
also have "... \<le> setsum (\<lambda>y. setsum g {x. x\<in>t \<and> i x = y}) (i ` t)" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1282 
using assms(24) by (auto intro!: setsum_mono2 setsum_nonneg) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1283 
also have "... \<le> setsum g t" 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1284 
using assms by (auto simp: setsum_image_gen[symmetric]) 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1285 
finally show ?thesis . 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1286 
qed 
28f824c7addc
Moved setprod_mono, abs_setprod and setsum_le_included to the Main image. Is used in Multivariate_Analysis.
hoelzl
parents:
35115
diff
changeset

1287 

31509  1288 
lemma setsum_multicount_gen: 
1289 
assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)" 

1290 
shows "setsum (\<lambda>i. (card {j\<in>t. R i j})) s = setsum k t" (is "?l = ?r") 

1291 
proof 

1292 
have "?l = setsum (\<lambda>i. setsum (\<lambda>x.1) {j\<in>t. R i j}) s" by auto 

1293 
also have "\<dots> = ?r" unfolding setsum_setsum_restrict[OF assms(12)] 

1294 
using assms(3) by auto 

