author  kleing 
Mon, 06 Jun 2011 16:29:13 +0200  
changeset 43157  b505be6f029a 
parent 43156  04aaac80183f 
child 43657  537ea3846f64 
permissions  rwrr 
8924  1 
(* Title: HOL/SetInterval.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 

15131  11 
theory SetInterval 
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 

17 
definition 

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

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

21 
definition 

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

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

25 
definition 

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

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

29 
definition 

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

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

33 
definition 

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

24691  36 

37 
definition 

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

24691  40 

41 
definition 

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

24691  44 

45 
definition 

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

24691  48 

49 
end 

8924  50 

13735  51 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

74 
translations 

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

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

80 

14485  81 
subsection {* Various equivalences *} 
13735  82 

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

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

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

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

13735  93 

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

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

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

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

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

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

103 
apply (rule double_complement) 
13735  104 
done 
105 

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

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

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

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

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

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

13850  118 

119 

14485  120 
subsection {* Logical Equivalences for Set Inclusion and Equality *} 
13850  121 

122 
lemma atLeast_subset_iff [iff]: 

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

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

124 
by (blast intro: order_trans) 
13850  125 

126 
lemma atLeast_eq_iff [iff]: 

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

127 
"(atLeast x = atLeast y) = (x = (y::'a::linorder))" 
13850  128 
by (blast intro: order_antisym order_trans) 
129 

130 
lemma greaterThan_subset_iff [iff]: 

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

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

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

133 
apply (subst linorder_not_less [symmetric], blast) 
13850  134 
done 
135 

136 
lemma greaterThan_eq_iff [iff]: 

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

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

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

139 
apply (erule equalityE) 
29709  140 
apply simp_all 
13850  141 
done 
142 

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

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

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

146 
lemma atMost_eq_iff [iff]: "(atMost x = atMost y) = (x = (y::'a::linorder))" 
13850  147 
by (blast intro: order_antisym order_trans) 
148 

149 
lemma lessThan_subset_iff [iff]: 

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

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

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

152 
apply (subst linorder_not_less [symmetric], blast) 
13850  153 
done 
154 

155 
lemma lessThan_eq_iff [iff]: 

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

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

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

158 
apply (erule equalityE) 
29709  159 
apply simp_all 
13735  160 
done 
161 

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

162 
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

163 
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

164 
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

165 
by (metis leD lessThan_subset_iff linorder_linear not_less_iff_gr_or_eq psubset_eq) 
13735  166 

13850  167 
subsection {*Twosided intervals*} 
13735  168 

24691  169 
context ord 
170 
begin 

171 

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

172 
lemma greaterThanLessThan_iff [simp,no_atp]: 
25062  173 
"(i : {l<..<u}) = (l < i & i < u)" 
13735  174 
by (simp add: greaterThanLessThan_def) 
175 

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

176 
lemma atLeastLessThan_iff [simp,no_atp]: 
25062  177 
"(i : {l..<u}) = (l <= i & i < u)" 
13735  178 
by (simp add: atLeastLessThan_def) 
179 

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

180 
lemma greaterThanAtMost_iff [simp,no_atp]: 
25062  181 
"(i : {l<..u}) = (l < i & i <= u)" 
13735  182 
by (simp add: greaterThanAtMost_def) 
183 

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

184 
lemma atLeastAtMost_iff [simp,no_atp]: 
25062  185 
"(i : {l..u}) = (l <= i & i <= u)" 
13735  186 
by (simp add: atLeastAtMost_def) 
187 

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

188 
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

189 
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

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

191 

24691  192 
end 
13735  193 

32400  194 
subsubsection{* Emptyness, singletons, subset *} 
15554  195 

24691  196 
context order 
197 
begin 

15554  198 

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

201 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

202 

203 
lemma atLeastatMost_empty_iff[simp]: 

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

205 
by auto (blast intro: order_trans) 

206 

207 
lemma atLeastatMost_empty_iff2[simp]: 

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

209 
by auto (blast intro: order_trans) 

210 

211 
lemma atLeastLessThan_empty[simp]: 

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

213 
by(auto simp: atLeastLessThan_def) 

24691  214 

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

217 
by auto (blast intro: le_less_trans) 

218 

219 
lemma atLeastLessThan_empty_iff2[simp]: 

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

221 
by auto (blast intro: le_less_trans) 

15554  222 

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

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

228 

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

230 
by auto (blast intro: less_le_trans) 

231 

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

25062  235 
lemma atLeastAtMost_singleton [simp]: "{a..a} = {a}" 
24691  236 
by (auto simp add: atLeastAtMost_def atMost_def atLeast_def) 
237 

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

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

239 

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

242 
unfolding atLeastAtMost_def atLeast_def atMost_def 

243 
by (blast intro: order_trans) 

244 

245 
lemma atLeastatMost_psubset_iff: 

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

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

248 
by(simp add: psubset_eq set_eq_iff less_le_not_le)(blast intro: order_trans) 
32400  249 

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

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

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

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

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

254 
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

255 
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

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

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

258 

24691  259 
end 
14485  260 

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

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

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

263 

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

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

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

266 
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

267 

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

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

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

270 
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

271 

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

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

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

276 

277 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

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

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

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

281 

282 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

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

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

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

286 

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

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

288 

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

291 
apply (auto simp:subset_eq Ball_def) 

292 
apply(frule_tac x=a in spec) 

293 
apply(erule_tac x=d in allE) 

294 
apply (simp add: less_imp_le) 

295 
done 

296 

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

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

298 
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

299 
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

300 
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

301 
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

302 

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

303 
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

304 
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

305 
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

306 
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

307 
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

308 

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

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

310 

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

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

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

313 

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

314 
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

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

316 

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

317 
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

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

319 

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

320 
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

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

322 

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

323 
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

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

325 

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

326 
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

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

328 

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

329 
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

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

331 

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

332 
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

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

334 

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

335 
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

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

337 

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

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

339 

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

340 

14485  341 
subsection {* Intervals of natural numbers *} 
342 

15047  343 
subsubsection {* The Constant @{term lessThan} *} 
344 

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

347 

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

349 
by (simp add: lessThan_def less_Suc_eq, blast) 

350 

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

354 

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

356 
proof safe 

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

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

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

360 
qed 

361 

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

364 

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

366 
by blast 

367 

15047  368 
subsubsection {* The Constant @{term greaterThan} *} 
369 

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

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

373 
done 

374 

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

376 
apply (simp add: greaterThan_def) 

377 
apply (auto elim: linorder_neqE) 

378 
done 

379 

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

381 
by blast 

382 

15047  383 
subsubsection {* The Constant @{term atLeast} *} 
384 

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

387 

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

389 
apply (simp add: atLeast_def) 

390 
apply (simp add: Suc_le_eq) 

391 
apply (simp add: order_le_less, blast) 

392 
done 

393 

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

395 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

396 

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

398 
by blast 

399 

15047  400 
subsubsection {* The Constant @{term atMost} *} 
401 

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

404 

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

406 
apply (simp add: atMost_def) 

407 
apply (simp add: less_Suc_eq order_le_less, blast) 

408 
done 

409 

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

411 
by blast 

412 

15047  413 
subsubsection {* The Constant @{term atLeastLessThan} *} 
414 

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

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

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

420 
specific concept to a more general one. *} 

28068  421 

15047  422 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  423 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  424 

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

427 

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

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

429 
atLeast0AtMost[symmetric, code_unfold] 
24449  430 

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

15047  432 
by (simp add: atLeastLessThan_def) 
24449  433 

15047  434 
subsubsection {* Intervals of nats with @{term Suc} *} 
435 

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

437 
lemma atLeastLessThanSuc: 

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

439 
by (auto simp add: atLeastLessThan_def) 
15047  440 

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

441 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  442 
by (auto simp add: atLeastLessThan_def) 
16041  443 
(* 
15047  444 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
445 
by (induct k, simp_all add: atLeastLessThanSuc) 

446 

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

448 
by (auto simp add: atLeastLessThan_def) 

16041  449 
*) 
15045  450 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  451 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
452 

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

453 
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

454 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  455 
greaterThanAtMost_def) 
456 

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

457 
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

458 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  459 
greaterThanLessThan_def) 
460 

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

463 

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

466 
lemma atLeastAtMostPlus1_int_conv: 

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

468 
by (auto intro: set_eqI) 

469 

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

472 
apply (simp_all add: atLeastLessThanSuc) 

473 
done 

474 

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

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

476 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

490 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

504 

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

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

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

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

508 

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

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

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

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

512 

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

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

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

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

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

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

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

519 

37664  520 
lemma image_minus_const_atLeastLessThan_nat: 
521 
fixes c :: nat 

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

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

524 
(is "_ = ?right") 

525 
proof safe 

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

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

528 
proof cases 

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

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

531 
next 

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

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

534 
qed 

535 
qed auto 

536 

35580  537 
context ordered_ab_group_add 
538 
begin 

539 

540 
lemma 

541 
fixes x :: 'a 

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

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

544 
proof safe 

545 
fix y assume "y < x" 

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

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

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

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

550 
next 

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

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

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

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

555 
qed simp_all 

556 

557 
lemma 

558 
fixes x :: 'a 

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

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

561 
proof  

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

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

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

565 
by (simp_all add: image_image 

566 
del: image_uminus_greaterThan image_uminus_atLeast) 

567 
qed 

568 

569 
lemma 

570 
fixes x :: 'a 

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

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

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

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

575 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

576 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

577 
end 

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

578 

14485  579 
subsubsection {* Finiteness *} 
580 

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

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

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

586 

587 
lemma finite_greaterThanLessThan [iff]: 

15045  588 
fixes l :: nat shows "finite {l<..<u}" 
14485  589 
by (simp add: greaterThanLessThan_def) 
590 

591 
lemma finite_atLeastLessThan [iff]: 

15045  592 
fixes l :: nat shows "finite {l..<u}" 
14485  593 
by (simp add: atLeastLessThan_def) 
594 

595 
lemma finite_greaterThanAtMost [iff]: 

15045  596 
fixes l :: nat shows "finite {l<..u}" 
14485  597 
by (simp add: greaterThanAtMost_def) 
598 

599 
lemma finite_atLeastAtMost [iff]: 

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

601 
by (simp add: atLeastAtMost_def) 

602 

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

608 
done 

609 

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

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

613 
proof 

614 
assume f:?F show ?B 

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

616 
next 

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

618 
qed 

619 

620 
lemma finite_nat_set_iff_bounded_le: 

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

622 
apply(simp add:finite_nat_set_iff_bounded) 

623 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

624 
done 

625 

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

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

14485  629 

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

632 

633 
lemma subset_card_intvl_is_intvl: 

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

635 
proof cases 

636 
assume "finite A" 

637 
thus "PROP ?P" 

32006  638 
proof(induct A rule:finite_linorder_max_induct) 
24853  639 
case empty thus ?case by auto 
640 
next 

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

644 
using `b ~: A` insert by fastsimp+ 

645 
ultimately show ?case by auto 

646 
qed 

647 
next 

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

649 
qed 

650 

651 

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

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

653 

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

656 
proof 

657 
show "?A <= ?B" 

658 
proof 

659 
fix x assume "x : ?A" 

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

661 
show "x : ?B" 

662 
proof(cases i) 

663 
case 0 with i show ?thesis by simp 

664 
next 

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

666 
qed 

667 
qed 

668 
next 

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

670 
qed 

671 

672 
lemma UN_le_add_shift: 

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

674 
proof 

675 
show "?A <= ?B" by fastsimp 

676 
next 

677 
show "?B <= ?A" 

678 
proof 

679 
fix x assume "x : ?B" 

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

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

682 
thus "x : ?A" by blast 

683 
qed 

684 
qed 

685 

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

686 
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

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

688 

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

689 
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

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

691 

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

694 
apply (rule UN_finite_subset) 

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

696 
apply blast 

697 
done 

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

698 

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

699 
lemma UN_finite2_eq: 
33044  700 
"(!!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)" 
701 
apply (rule subset_antisym) 

702 
apply (rule UN_finite2_subset, blast) 

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

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

706 

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

707 

14485  708 
subsubsection {* Cardinality *} 
709 

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

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

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

715 

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

14485  718 
apply (erule ssubst, rule card_lessThan) 
15045  719 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  720 
apply (erule subst) 
721 
apply (rule card_image) 

722 
apply (simp add: inj_on_def) 

723 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

725 
apply arith 

726 
done 

727 

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

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

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

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

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

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

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

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

739 
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

740 
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

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

742 

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

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

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

745 
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

746 

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

749 
apply(drule ex_bij_betw_finite_nat) 

750 
apply(drule ex_bij_betw_nat_finite) 

751 
apply(auto intro!:bij_betw_trans) 

752 
done 

753 

754 
lemma ex_bij_betw_nat_finite_1: 

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

756 
by (rule finite_same_card_bij) auto 

757 

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

758 
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

759 
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

760 
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

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

762 
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

763 
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

764 
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

765 
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

766 
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

767 
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

768 
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

769 
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

770 
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

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

772 

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

773 
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

774 
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

775 
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

776 
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

777 
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

778 
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

779 
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

780 
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

781 
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

782 
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

783 
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

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

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

786 
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

787 
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

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

789 
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

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

791 

14485  792 
subsection {* Intervals of integers *} 
793 

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

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

797 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  798 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
799 

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

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

801 
"{l+1..<u} = {l<..<u::int}" 
14485  802 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
803 

804 
subsubsection {* Finiteness *} 

805 

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

806 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  807 
{(0::int)..<u} = int ` {..<nat u}" 
14485  808 
apply (unfold image_def lessThan_def) 
809 
apply auto 

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

35216  811 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  812 
done 
813 

15045  814 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
14485  815 
apply (case_tac "0 \<le> u") 
816 
apply (subst image_atLeastZeroLessThan_int, assumption) 

817 
apply (rule finite_imageI) 

818 
apply auto 

819 
done 

820 

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

14485  823 
apply (erule subst) 
824 
apply (rule finite_imageI) 

825 
apply (rule finite_atLeastZeroLessThan_int) 

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

826 
apply (rule image_add_int_atLeastLessThan) 
14485  827 
done 
828 

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

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

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

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

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

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

24853  838 

14485  839 
subsubsection {* Cardinality *} 
840 

15045  841 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
14485  842 
apply (case_tac "0 \<le> u") 
843 
apply (subst image_atLeastZeroLessThan_int, assumption) 

844 
apply (subst card_image) 

845 
apply (auto simp add: inj_on_def) 

846 
done 

847 

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

14485  850 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  851 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  852 
apply (erule subst) 
853 
apply (rule card_image) 

854 
apply (simp add: inj_on_def) 

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

855 
apply (rule image_add_int_atLeastLessThan) 
14485  856 
done 
857 

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

29667  859 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
860 
apply (auto simp add: algebra_simps) 

861 
done 

14485  862 

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

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

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

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

869 
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

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

871 
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

872 
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

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

874 

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

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

876 
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

877 
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

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

879 
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

880 
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

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

882 

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

883 
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  884 
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

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

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

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

888 
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

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

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

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

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

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

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

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

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

897 

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

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

899 
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

900 
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

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

902 
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

903 
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

904 
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

905 
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

906 
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

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

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

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

910 
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

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

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

913 
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

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

915 

14485  916 

13850  917 
subsection {*Lemmas useful with the summation operator setsum*} 
918 

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

919 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  920 

14577  921 
subsubsection {* Disjoint Unions *} 
13735  922 

14577  923 
text {* Singletons and open intervals *} 
13735  924 

925 
lemma ivl_disj_un_singleton: 

15045  926 
"{l::'a::linorder} Un {l<..} = {l..}" 
927 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

932 
by auto 
13735  933 

14577  934 
text {* One and twosided intervals *} 
13735  935 

936 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

945 
by auto 
13735  946 

14577  947 
text {* Two and twosided intervals *} 
13735  948 

949 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

957 
"[ (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

958 
by auto 
13735  959 

960 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

961 

14577  962 
subsubsection {* Disjoint Intersections *} 
13735  963 

14577  964 
text {* One and twosided intervals *} 
13735  965 

966 
lemma ivl_disj_int_one: 

15045  967 
"{..l::'a::order} Int {l<..<u} = {}" 
968 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

975 
by auto 
13735  976 

14577  977 
text {* Two and twosided intervals *} 
13735  978 

979 
lemma ivl_disj_int_two: 

15045  980 
"{l::'a::order<..<m} Int {m..<u} = {}" 
981 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

988 
by auto 
13735  989 

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

990 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  991 

15542  992 
subsubsection {* Some Differences *} 
993 

994 
lemma ivl_diff[simp]: 

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

996 
by(auto) 

997 

998 

999 
subsubsection {* Some Subset Conditions *} 

1000 

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

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

1004 
apply(rule ccontr) 

1005 
apply(insert linorder_le_less_linear[of i n]) 

1006 
apply(clarsimp simp:linorder_not_le) 

1007 
apply(fastsimp) 

1008 
done 

1009 

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

1010 

15042  1011 
subsection {* Summation indexed over intervals *} 
1012 

1013 
syntax 

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

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

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

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

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

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

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

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

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

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

15052  1035 
"_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" 
16052  1036 
("(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

1037 

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

1039 
"\<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

1040 
"\<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

1041 
"\<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

1042 
"\<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

1043 

15052  1044 
text{* The above introduces some pretty alternative syntaxes for 
15056  1045 
summation over intervals: 
15052  1046 
\begin{center} 
1047 
\begin{tabular}{lll} 

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

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

16052  1051 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  1052 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  1053 
\end{tabular} 
1054 
\end{center} 

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

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

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

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

15052  1062 

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

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

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

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

1067 

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

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

1071 
the context. *} 

1072 

1073 
lemma setsum_ivl_cong: 

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

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

1076 
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

1077 

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

1080 

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

1083 

16041  1084 
lemma setsum_lessThan_Suc[simp]: "(\<Sum>i < Suc n. f i) = (\<Sum>i < n. f i) + f n" 
1085 
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

1086 

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

1090 

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

16041  1094 
(* 
15561  1095 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
1096 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

1097 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  1098 
*) 
28068  1099 

1100 
lemma setsum_head: 

1101 
fixes n :: nat 

1102 
assumes mn: "m <= n" 

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

1104 
proof  

1105 
from mn 

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

1107 
by (auto intro: ivl_disj_un_singleton) 

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

1109 
by (simp add: atLeast0LessThan) 

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

1111 
finally show ?thesis . 

1112 
qed 

1113 

1114 
lemma setsum_head_Suc: 

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

1116 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

1117 

1118 
lemma setsum_head_upt_Suc: 

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

1120 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  1121 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  1122 
done 
1123 

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

1126 
proof 

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

1128 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

1129 
atLeastSucAtMost_greaterThanAtMost) 

1130 
qed 

28068  1131 

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

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

1135 

1136 
lemma setsum_diff_nat_ivl: 

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

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

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

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

1141 
apply (simp add: add_ac) 

1142 
done 

1143 

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

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

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

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

1149 

31509  1150 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
1151 

1152 
lemma setsum_setsum_restrict: 

1153 
"finite S \<Longrightarrow> finite T \<Longrightarrow> 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" 

1154 
by (simp add: setsum_restrict_set'[unfolded mem_def] mem_def) 

1155 
(rule setsum_commute) 

1156 

1157 
lemma setsum_image_gen: assumes fS: "finite S" 

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

1159 
proof 

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

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

1162 
by simp 

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

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

1165 
finally show ?thesis . 

1166 
qed 

1167 

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

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

1169 
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

1170 
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

1171 
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

1172 
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

1173 
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

1174 
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

1175 
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

1176 
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

1177 
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

1178 
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

1179 
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

1180 
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

1181 
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

1182 
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

1183 
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

1184 
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

1185 
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

1186 
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

1187 
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

1188 

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

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

1192 
proof 

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

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

1195 
using assms(3) by auto 

1196 
finally show ?thesis . 

1197 
qed 

1198 

1199 
lemma setsum_multicount: 

1200 
assumes "finite S" "finite T" "\<forall>j\<in>T. (card {i\<in>S. R i j} = k)" 

1201 
shows "setsum (\<lambda>i. card {j\<in>T. R i j}) S = k * card T" (is "?l = ?r") 

1202 
proof 

1203 
have "?l = setsum (\<lambda>i. k) T" by(rule setsum_multicount_gen)(auto simp:assms) 

35216  1204 
also have "\<dots> = ?r" by(simp add: mult_commute) 
31509  1205 
finally show ?thesis by auto 
1206 
qed 

1207 

28068  1208 

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

1209 
subsection{* Shifting bounds *} 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1210 

15539  1211 
lemma setsum_shift_bounds_nat_ivl: 
1212 
"setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}" 

1213 
by (induct "n", auto simp:atLeastLessThanSuc) 

1214 

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

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

1216 
"setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}" 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1217 
apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"]) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1218 
apply (simp add:image_add_atLeastAtMost o_def) 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

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

1220 

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

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

1222 
"setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){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

1223 
by (simp add:setsum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified]) 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1224 

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

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

1226 
"setsum f {Suc m..<Suc n} = setsum (%i. f(Suc i)){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

1227 
by (simp add:setsum_shift_bounds_nat_ivl[where k="Suc 0", simplified]) 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

1228 

28068  1229 
lemma setsum_shift_lb_Suc0_0: 
1230 
"f(0::nat) = (0::nat) \<Longrightarrow> setsum f {Suc 0..k} = setsum f {0..k}" 

1231 
by(simp add:setsum_head_Suc) 

19106
6e6b5b1fdc06
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
kleing
parents:
19022
diff
changeset

1232 

28068  1233 
lemma setsum_shift_lb_Suc0_0_upt: 
1234 
"f(0::nat) = 0 \<Longrightarrow> setsum f {Suc 0..<k} = setsum f {0..<k}" 

1235 
apply(cases k)apply simp 

1236 
apply(simp add:setsum_head_upt_Suc) 

1237 
done 

19022
0e6ec4fd204c
* moved ThreeDivides from Isar_examples to better suited HOL/ex
kleing
parents:
17719
diff
changeset

1238 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1239 
subsection {* The formula for geometric sums *} 
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1240 

e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

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

1242 
assumes "x \<noteq> 1" 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1243 
shows "(\<Sum>i=0..<n. x ^ i) = (x ^ n  1) / (x  1::'a::field)" 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1244 
proof  
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1245 
from assms obtain y where "y = x  1" and "y \<noteq> 0" by simp_all 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1246 
moreover have "(\<Sum>i=0..<n. (y + 1) ^ i) = ((y + 1) ^ n  1) / y" 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1247 
proof (induct n) 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1248 
case 0 then show ?case by simp 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1249 
next 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1250 
case (Suc n) 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1251 
moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
36350  1252 
ultimately show ?case by (simp add: field_simps divide_inverse) 
36307
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1253 
qed 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1254 
ultimately show ?thesis by simp 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1255 
qed 
1732232f9b27
sharpened constraint (c.f. 4e7f5b22dd7d); explicit is better than implicit
haftmann
parents:
35828
diff
changeset

1256 

17149
e2b19c92ef51
Lemmas on dvd, power and finite summation added or strengthened.
ballarin
parents:
16733
diff
changeset

1257 

19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1258 
subsection {* The formula for arithmetic sums *} 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1259 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1260 
lemma gauss_sum: 
23277  1261 
"((1::'a::comm_semiring_1) + 1)*(\<Sum>i\<in>{1..n}. of_nat i) = 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1262 
of_nat n*((of_nat n)+1)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1263 
proof (induct n) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1264 
case 0 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1265 
show ?case by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1266 
next 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1267 
case (Suc n) 
29667  1268 
then show ?case by (simp add: algebra_simps) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1269 
qed 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1270 

958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1271 
theorem arith_series_general: 
23277  1272 
"((1::'a::comm_semiring_1) + 1) * (\<Sum>i\<in>{..<n}. a + of_nat i * d) = 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1273 
of_nat n * (a + (a + of_nat(n  1)*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1274 
proof cases 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1275 
assume ngt1: "n > 1" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1276 
let ?I = "\<lambda>i. of_nat i" and ?n = "of_nat n" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1277 
have 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1278 
"(\<Sum>i\<in>{..<n}. a+?I i*d) = 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1279 
((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1280 
by (rule setsum_addf) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1281 
also from ngt1 have "\<dots> = ?n*a + (\<Sum>i\<in>{..<n}. ?I i*d)" by simp 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1282 
also from ngt1 have "\<dots> = (?n*a + d*(\<Sum>i\<in>{1..<n}. ?I i))" 
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

1283 
unfolding One_nat_def 
28068  1284 
by (simp add: setsum_right_distrib atLeast0LessThan[symmetric] setsum_shift_lb_Suc0_0_upt mult_ac) 
19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1285 
also have "(1+1)*\<dots> = (1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..<n}. ?I i)" 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1286 
by (simp add: left_distrib right_distrib) 
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1287 
also from ngt1 have "{1..<n} = {1..n  1}" 
28068  1288 
by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost) 
1289 
also from ngt1 

19469
958d2f2dd8d4
moved arithmetic series to geometric series in SetInterval
kleing
parents:
19376
diff
changeset

1290 
have "(1+1)*?n*a + d*(1+1)*(\<Sum>i\<in>{1..n  1}. ?I i) = ((1+1)*?n*a + d*?I (n  1)*?I 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

1291 
by (simp only: mult_ac gauss_sum [of "n  1"], unfold One_nat_def) 
23431
25ca91279a9b
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents:
23413
diff
changeset

1292 
(simp add: mult_ac trans [OF add_commute of_nat_Suc [symmetric]]) 
29667  1293 
finally show ?thesis by (simp add: algebra_simps) 
19469 