author  hoelzl 
Mon, 04 Jul 2011 10:15:49 +0200  
changeset 43657  537ea3846f64 
parent 43157  b505be6f029a 
child 44008  2e09299ce807 
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 

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

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

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

291 

292 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

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

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

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

296 

297 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

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

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

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

301 

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

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

303 

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

306 
apply (auto simp:subset_eq Ball_def) 

307 
apply(frule_tac x=a in spec) 

308 
apply(erule_tac x=d in allE) 

309 
apply (simp add: less_imp_le) 

310 
done 

311 

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

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

313 
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

314 
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

315 
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

316 
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

317 

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

318 
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

319 
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

320 
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

321 
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

322 
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

323 

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

324 
subsubsection {* Intersection *} 
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 
context linorder 
341c83339aeb
tuned the simp rules for Int involving insert and intervals.
nipkow
parents:
32436
diff
changeset

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

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

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

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

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

340 

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

341 
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

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

343 

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

344 
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

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

346 

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

347 
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

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

349 

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

350 
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

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

352 

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

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

354 

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

355 

14485  356 
subsection {* Intervals of natural numbers *} 
357 

15047  358 
subsubsection {* The Constant @{term lessThan} *} 
359 

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

362 

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

364 
by (simp add: lessThan_def less_Suc_eq, blast) 

365 

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

369 

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

371 
proof safe 

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

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

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

375 
qed 

376 

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

379 

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

381 
by blast 

382 

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

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

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

388 
done 

389 

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

391 
apply (simp add: greaterThan_def) 

392 
apply (auto elim: linorder_neqE) 

393 
done 

394 

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

396 
by blast 

397 

15047  398 
subsubsection {* The Constant @{term atLeast} *} 
399 

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

402 

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

404 
apply (simp add: atLeast_def) 

405 
apply (simp add: Suc_le_eq) 

406 
apply (simp add: order_le_less, blast) 

407 
done 

408 

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

410 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

411 

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

413 
by blast 

414 

15047  415 
subsubsection {* The Constant @{term atMost} *} 
416 

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

419 

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

421 
apply (simp add: atMost_def) 

422 
apply (simp add: less_Suc_eq order_le_less, blast) 

423 
done 

424 

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

426 
by blast 

427 

15047  428 
subsubsection {* The Constant @{term atLeastLessThan} *} 
429 

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

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

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

435 
specific concept to a more general one. *} 

28068  436 

15047  437 
lemma atLeast0LessThan: "{0::nat..<n} = {..<n}" 
15042  438 
by(simp add:lessThan_def atLeastLessThan_def) 
24449  439 

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

442 

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

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

444 
atLeast0AtMost[symmetric, code_unfold] 
24449  445 

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

15047  447 
by (simp add: atLeastLessThan_def) 
24449  448 

15047  449 
subsubsection {* Intervals of nats with @{term Suc} *} 
450 

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

452 
lemma atLeastLessThanSuc: 

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

454 
by (auto simp add: atLeastLessThan_def) 
15047  455 

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

456 
lemma atLeastLessThan_singleton [simp]: "{m..<Suc m} = {m}" 
15047  457 
by (auto simp add: atLeastLessThan_def) 
16041  458 
(* 
15047  459 
lemma atLeast_sum_LessThan [simp]: "{m + k..<k::nat} = {}" 
460 
by (induct k, simp_all add: atLeastLessThanSuc) 

461 

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

463 
by (auto simp add: atLeastLessThan_def) 

16041  464 
*) 
15045  465 
lemma atLeastLessThanSuc_atLeastAtMost: "{l..<Suc u} = {l..u}" 
14485  466 
by (simp add: lessThan_Suc_atMost atLeastAtMost_def atLeastLessThan_def) 
467 

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

468 
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

469 
by (simp add: atLeast_Suc_greaterThan atLeastAtMost_def 
14485  470 
greaterThanAtMost_def) 
471 

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

472 
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

473 
by (simp add: atLeast_Suc_greaterThan atLeastLessThan_def 
14485  474 
greaterThanLessThan_def) 
475 

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

478 

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

481 
lemma atLeastAtMostPlus1_int_conv: 

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

483 
by (auto intro: set_eqI) 

484 

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

487 
apply (simp_all add: atLeastLessThanSuc) 

488 
done 

489 

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

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

491 

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

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

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

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

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

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

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

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

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

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

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

502 
ultimately show "n : ?A" by blast 
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 
qed 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

505 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

519 

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

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

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

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

523 

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

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

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

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

527 

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

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

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

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

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

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

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

534 

37664  535 
lemma image_minus_const_atLeastLessThan_nat: 
536 
fixes c :: nat 

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

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

539 
(is "_ = ?right") 

540 
proof safe 

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

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

543 
proof cases 

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

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

546 
next 

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

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

549 
qed 

550 
qed auto 

551 

35580  552 
context ordered_ab_group_add 
553 
begin 

554 

555 
lemma 

556 
fixes x :: 'a 

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

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

559 
proof safe 

560 
fix y assume "y < x" 

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

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

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

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

565 
next 

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

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

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

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

570 
qed simp_all 

571 

572 
lemma 

573 
fixes x :: 'a 

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

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

576 
proof  

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

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

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

580 
by (simp_all add: image_image 

581 
del: image_uminus_greaterThan image_uminus_atLeast) 

582 
qed 

583 

584 
lemma 

585 
fixes x :: 'a 

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

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

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

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

590 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

591 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

592 
end 

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

593 

14485  594 
subsubsection {* Finiteness *} 
595 

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

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

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

601 

602 
lemma finite_greaterThanLessThan [iff]: 

15045  603 
fixes l :: nat shows "finite {l<..<u}" 
14485  604 
by (simp add: greaterThanLessThan_def) 
605 

606 
lemma finite_atLeastLessThan [iff]: 

15045  607 
fixes l :: nat shows "finite {l..<u}" 
14485  608 
by (simp add: atLeastLessThan_def) 
609 

610 
lemma finite_greaterThanAtMost [iff]: 

15045  611 
fixes l :: nat shows "finite {l<..u}" 
14485  612 
by (simp add: greaterThanAtMost_def) 
613 

614 
lemma finite_atLeastAtMost [iff]: 

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

616 
by (simp add: atLeastAtMost_def) 

617 

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

623 
done 

624 

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

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

628 
proof 

629 
assume f:?F show ?B 

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

631 
next 

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

633 
qed 

634 

635 
lemma finite_nat_set_iff_bounded_le: 

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

637 
apply(simp add:finite_nat_set_iff_bounded) 

638 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

639 
done 

640 

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

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

14485  644 

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

647 

648 
lemma subset_card_intvl_is_intvl: 

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

650 
proof cases 

651 
assume "finite A" 

652 
thus "PROP ?P" 

32006  653 
proof(induct A rule:finite_linorder_max_induct) 
24853  654 
case empty thus ?case by auto 
655 
next 

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

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

660 
ultimately show ?case by auto 

661 
qed 

662 
next 

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

664 
qed 

665 

666 

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

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

668 

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

671 
proof 

672 
show "?A <= ?B" 

673 
proof 

674 
fix x assume "x : ?A" 

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

676 
show "x : ?B" 

677 
proof(cases i) 

678 
case 0 with i show ?thesis by simp 

679 
next 

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

681 
qed 

682 
qed 

683 
next 

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

685 
qed 

686 

687 
lemma UN_le_add_shift: 

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

689 
proof 

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

691 
next 

692 
show "?B <= ?A" 

693 
proof 

694 
fix x assume "x : ?B" 

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

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

697 
thus "x : ?A" by blast 

698 
qed 

699 
qed 

700 

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

701 
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

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

703 

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

704 
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

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

706 

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

709 
apply (rule UN_finite_subset) 

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

711 
apply blast 

712 
done 

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

713 

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

714 
lemma UN_finite2_eq: 
33044  715 
"(!!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)" 
716 
apply (rule subset_antisym) 

717 
apply (rule UN_finite2_subset, blast) 

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

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

721 

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

722 

14485  723 
subsubsection {* Cardinality *} 
724 

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

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

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

730 

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

14485  733 
apply (erule ssubst, rule card_lessThan) 
15045  734 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  735 
apply (erule subst) 
736 
apply (rule card_image) 

737 
apply (simp add: inj_on_def) 

738 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

740 
apply arith 

741 
done 

742 

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

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

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

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

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

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

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

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

754 
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

755 
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

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

757 

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

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

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

760 
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

761 

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

764 
apply(drule ex_bij_betw_finite_nat) 

765 
apply(drule ex_bij_betw_nat_finite) 

766 
apply(auto intro!:bij_betw_trans) 

767 
done 

768 

769 
lemma ex_bij_betw_nat_finite_1: 

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

771 
by (rule finite_same_card_bij) auto 

772 

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

773 
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

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

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

777 
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

778 
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

779 
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

780 
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

781 
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

782 
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

783 
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

784 
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

785 
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

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

787 

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

788 
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

789 
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

790 
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

791 
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

792 
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

793 
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

794 
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

795 
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

796 
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

797 
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

798 
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

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

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

801 
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

802 
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

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

804 
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

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

806 

14485  807 
subsection {* Intervals of integers *} 
808 

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

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

812 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  813 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
814 

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

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

816 
"{l+1..<u} = {l<..<u::int}" 
14485  817 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
818 

819 
subsubsection {* Finiteness *} 

820 

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

821 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  822 
{(0::int)..<u} = int ` {..<nat u}" 
14485  823 
apply (unfold image_def lessThan_def) 
824 
apply auto 

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

35216  826 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  827 
done 
828 

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

832 
apply (rule finite_imageI) 

833 
apply auto 

834 
done 

835 

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

14485  838 
apply (erule subst) 
839 
apply (rule finite_imageI) 

840 
apply (rule finite_atLeastZeroLessThan_int) 

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

841 
apply (rule image_add_int_atLeastLessThan) 
14485  842 
done 
843 

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

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

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

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

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

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

24853  853 

14485  854 
subsubsection {* Cardinality *} 
855 

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

859 
apply (subst card_image) 

860 
apply (auto simp add: inj_on_def) 

861 
done 

862 

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

14485  865 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  866 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  867 
apply (erule subst) 
868 
apply (rule card_image) 

869 
apply (simp add: inj_on_def) 

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

870 
apply (rule image_add_int_atLeastLessThan) 
14485  871 
done 
872 

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

29667  874 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
875 
apply (auto simp add: algebra_simps) 

876 
done 

14485  877 

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

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

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

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

884 
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

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

886 
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

887 
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

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

889 

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

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

891 
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

892 
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

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

894 
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

895 
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

896 
qed 
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_Suc2: "0 \<notin> M \<Longrightarrow> card {k. Suc k \<in> M \<and> k < i} = card {k \<in> M. k < Suc i}" 
37388  899 
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

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

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

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

903 
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

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

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

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

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

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

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

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

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

912 

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

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

914 
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

915 
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

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

917 
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

918 
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

919 
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

920 
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

921 
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

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

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

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

925 
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

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

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

928 
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

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

930 

14485  931 

13850  932 
subsection {*Lemmas useful with the summation operator setsum*} 
933 

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

934 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  935 

14577  936 
subsubsection {* Disjoint Unions *} 
13735  937 

14577  938 
text {* Singletons and open intervals *} 
13735  939 

940 
lemma ivl_disj_un_singleton: 

15045  941 
"{l::'a::linorder} Un {l<..} = {l..}" 
942 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

947 
by auto 
13735  948 

14577  949 
text {* One and twosided intervals *} 
13735  950 

951 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

960 
by auto 
13735  961 

14577  962 
text {* Two and twosided intervals *} 
13735  963 

964 
lemma ivl_disj_un_two: 

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

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

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

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

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

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

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

973 
by auto 
13735  974 

975 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

976 

14577  977 
subsubsection {* Disjoint Intersections *} 
13735  978 

14577  979 
text {* One and twosided intervals *} 
13735  980 

981 
lemma ivl_disj_int_one: 

15045  982 
"{..l::'a::order} Int {l<..<u} = {}" 
983 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

990 
by auto 
13735  991 

14577  992 
text {* Two and twosided intervals *} 
13735  993 

994 
lemma ivl_disj_int_two: 

15045  995 
"{l::'a::order<..<m} Int {m..<u} = {}" 
996 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

1003 
by auto 
13735  1004 

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

1005 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  1006 

15542  1007 
subsubsection {* Some Differences *} 
1008 

1009 
lemma ivl_diff[simp]: 

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

1011 
by(auto) 

1012 

1013 

1014 
subsubsection {* Some Subset Conditions *} 

1015 

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

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

1019 
apply(rule ccontr) 

1020 
apply(insert linorder_le_less_linear[of i n]) 

1021 
apply(clarsimp simp:linorder_not_le) 

1022 
apply(fastsimp) 

1023 
done 

1024 

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

1025 

15042  1026 
subsection {* Summation indexed over intervals *} 
1027 

1028 
syntax 

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

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

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

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

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

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

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

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

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

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

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

1052 

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

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

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

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

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

1058 

15052  1059 
text{* The above introduces some pretty alternative syntaxes for 
15056  1060 
summation over intervals: 
15052  1061 
\begin{center} 
1062 
\begin{tabular}{lll} 

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

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

16052  1066 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  1067 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  1068 
\end{tabular} 
1069 
\end{center} 

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

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

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

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

15052  1077 

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

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

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

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

1082 

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

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

1086 
the context. *} 

1087 

1088 
lemma setsum_ivl_cong: 

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

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

1091 
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

1092 

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

1095 

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

1098 

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

1101 

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

1105 

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

16041  1109 
(* 
15561  1110 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
1111 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

1112 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  1113 
*) 
28068  1114 

1115 
lemma setsum_head: 

1116 
fixes n :: nat 

1117 
assumes mn: "m <= n" 

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

1119 
proof  

1120 
from mn 

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

1122 
by (auto intro: ivl_disj_un_singleton) 

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

1124 
by (simp add: atLeast0LessThan) 

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

1126 
finally show ?thesis . 

1127 
qed 

1128 

1129 
lemma setsum_head_Suc: 

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

1131 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

1132 

1133 
lemma setsum_head_upt_Suc: 

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

1135 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  1136 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  1137 
done 
1138 

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

1141 
proof 

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

1143 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

1144 
atLeastSucAtMost_greaterThanAtMost) 

1145 
qed 

28068  1146 

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

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

1150 

1151 
lemma setsum_diff_nat_ivl: 

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

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

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

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

1156 
apply (simp add: add_ac) 

1157 
done 

1158 

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

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

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

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

1164 

31509  1165 
lemmas setsum_restrict_set' = setsum_restrict_set[unfolded Int_def] 
1166 

1167 
lemma setsum_setsum_restrict: 

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

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

1170 
(rule setsum_commute) 

1171 

1172 
lemma setsum_image_gen: assumes fS: "finite S" 

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

1174 
proof 

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

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

1177 
by simp 

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

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

1180 
finally show ?thesis . 

1181 
qed 

1182 

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

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

1184 
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

1185 
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

1186 
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

1187 
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

1188 
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

1189 
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

1190 
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

1191 
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

1192 
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

1193 
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

1194 
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

1195 
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

1196 
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

1197 
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

1198 
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

1199 
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

1200 
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

1201 
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

1202 
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

1203 

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

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

1207 
proof 

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

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

1210 
using assms(3) by auto 

1211 
finally show ?thesis . 

1212 
qed 

1213 

1214 
lemma setsum_multicount: 

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

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

1217 
proof 

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

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

1222 

28068  1223 

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

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

1225 

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

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

1229 

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

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

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

1232 
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

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

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

1235 

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

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

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

1238 
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

1239 

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

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

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

1242 
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

1243 

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

1246 
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

1247 

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

1250 
apply(cases k)apply simp 

1251 
apply(simp add:setsum_head_upt_Suc) 

1252 
done 

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

1253 

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

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

1255 

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

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

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

1258 
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

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

1260 
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

1261 
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

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

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

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

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

1266 
moreover with `y \<noteq> 0` have "(1 + y) ^ n = (y * inverse y) * (1 + y) ^ n" by simp 
36350  1267 
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

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

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

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

1271 

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

1272 

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

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

1274 

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

1275 
lemma gauss_sum: 
23277  1276 
"((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

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

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

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

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

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

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

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

1285 

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

1286 
theorem arith_series_general: 
23277  1287 
"((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

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

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

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

1291 
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

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

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

1294 
((\<Sum>i\<in>{..<n}. a) + (\<Sum>i\<in>{..<n}. ?I i*d))" 