author  webertj 
Fri, 19 Oct 2012 15:12:52 +0200  
changeset 49962  a8cc904a6820 
parent 47988  e4b69e10b990 
child 50417  f18b92f91818 
permissions  rwrr 
47317
432b29a96f61
modernized obsolete oldstyle theory name with proper newstyle underscore
huffman
parents:
47222
diff
changeset

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

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

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

4 
Author: Jeremy Avigad 
8924  5 

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

14577  9 
header {* Set intervals *} 
10 

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

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

12 
imports Int Nat_Transfer 
15131  13 
begin 
8924  14 

24691  15 
context ord 
16 
begin 

44008  17 

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

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

22 
definition 

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

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

26 
definition 

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

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

30 
definition 

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

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

34 
definition 

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

24691  37 

38 
definition 

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

24691  41 

42 
definition 

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

24691  45 

46 
definition 

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

24691  49 

50 
end 

8924  51 

13735  52 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

75 
translations 

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

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

81 

14485  82 
subsection {* Various equivalences *} 
13735  83 

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

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

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

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

13735  94 

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

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

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

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

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

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

104 
apply (rule double_complement) 
13735  105 
done 
106 

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

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

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

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

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

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

13850  119 

120 

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

123 
lemma atLeast_subset_iff [iff]: 

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

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

125 
by (blast intro: order_trans) 
13850  126 

127 
lemma atLeast_eq_iff [iff]: 

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

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

131 
lemma greaterThan_subset_iff [iff]: 

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

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

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

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

137 
lemma greaterThan_eq_iff [iff]: 

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

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

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

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

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

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

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

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

150 
lemma lessThan_subset_iff [iff]: 

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

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

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

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

156 
lemma lessThan_eq_iff [iff]: 

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

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

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

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

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

163 
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

164 
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

165 
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

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

13850  168 
subsection {*Twosided intervals*} 
13735  169 

24691  170 
context ord 
171 
begin 

172 

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

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

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

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

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

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

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

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

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

189 
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

190 
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

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

192 

24691  193 
end 
13735  194 

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

24691  197 
context order 
198 
begin 

15554  199 

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

202 
by(auto simp: atLeastAtMost_def atLeast_def atMost_def) 

203 

204 
lemma atLeastatMost_empty_iff[simp]: 

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

206 
by auto (blast intro: order_trans) 

207 

208 
lemma atLeastatMost_empty_iff2[simp]: 

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

210 
by auto (blast intro: order_trans) 

211 

212 
lemma atLeastLessThan_empty[simp]: 

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

214 
by(auto simp: atLeastLessThan_def) 

24691  215 

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

218 
by auto (blast intro: le_less_trans) 

219 

220 
lemma atLeastLessThan_empty_iff2[simp]: 

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

222 
by auto (blast intro: le_less_trans) 

15554  223 

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

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

229 

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

231 
by auto (blast intro: less_le_trans) 

232 

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

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

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

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

240 

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

243 
unfolding atLeastAtMost_def atLeast_def atMost_def 

244 
by (blast intro: order_trans) 

245 

246 
lemma atLeastatMost_psubset_iff: 

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

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

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

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

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

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

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

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

255 
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

256 
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

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

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

259 

24691  260 
end 
14485  261 

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

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

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

264 

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

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

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

267 
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

268 

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

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

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

271 
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

272 

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

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

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

277 

278 
lemma greaterThanAtMost_subseteq_atLeastAtMost_iff: 

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

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

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

282 

283 
lemma greaterThanLessThan_subseteq_atLeastAtMost_iff: 

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

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

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

287 

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

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

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

292 

293 
lemma greaterThanAtMost_subseteq_atLeastLessThan_iff: 

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

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

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

297 

298 
lemma greaterThanLessThan_subseteq_atLeastLessThan_iff: 

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

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

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

302 

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

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

304 

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

307 
apply (auto simp:subset_eq Ball_def) 

308 
apply(frule_tac x=a in spec) 

309 
apply(erule_tac x=d in allE) 

310 
apply (simp add: less_imp_le) 

311 
done 

312 

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

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

314 
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

315 
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

316 
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

317 
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

318 

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

319 
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

320 
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

321 
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

322 
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

323 
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

324 

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

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

326 

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

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

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

329 

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

330 
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

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

332 

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

333 
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

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

335 

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

336 
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

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

338 

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

339 
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

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

341 

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

342 
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

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

344 

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

345 
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

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

347 

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

348 
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

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

350 

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

351 
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

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

353 

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

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

355 

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

356 

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

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

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

363 

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

365 
by (simp add: lessThan_def less_Suc_eq, blast) 

366 

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

370 

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

372 
proof safe 

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

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

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

376 
qed 

377 

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

380 

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

382 
by blast 

383 

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

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

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

389 
done 

390 

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

392 
apply (simp add: greaterThan_def) 

393 
apply (auto elim: linorder_neqE) 

394 
done 

395 

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

397 
by blast 

398 

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

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

403 

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

405 
apply (simp add: atLeast_def) 

406 
apply (simp add: Suc_le_eq) 

407 
apply (simp add: order_le_less, blast) 

408 
done 

409 

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

411 
by (auto simp add: greaterThan_def atLeast_def less_Suc_eq_le) 

412 

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

414 
by blast 

415 

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

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

420 

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

422 
apply (simp add: atMost_def) 

423 
apply (simp add: less_Suc_eq order_le_less, blast) 

424 
done 

425 

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

427 
by blast 

428 

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

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

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

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

436 
specific concept to a more general one. *} 

28068  437 

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

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

443 

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

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

445 
atLeast0AtMost[symmetric, code_unfold] 
24449  446 

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

15047  448 
by (simp add: atLeastLessThan_def) 
24449  449 

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

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

453 
lemma atLeastLessThanSuc: 

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

455 
by (auto simp add: atLeastLessThan_def) 
15047  456 

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

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

462 

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

464 
by (auto simp add: atLeastLessThan_def) 

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

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

469 
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

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

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

473 
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

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

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

479 

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

482 

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

485 
lemma atLeastAtMostPlus1_int_conv: 

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

487 
by (auto intro: set_eqI) 

488 

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

491 
apply (simp_all add: atLeastLessThanSuc) 

492 
done 

493 

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

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

495 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

509 

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

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

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

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

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

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

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

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

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

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

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

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

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

522 
qed 
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_atLeastAtMost[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_atLeastAtMost[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 
corollary image_Suc_atLeastLessThan[simp]: 
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16102
diff
changeset

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

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

531 

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

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

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

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

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

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

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

538 

37664  539 
lemma image_minus_const_atLeastLessThan_nat: 
540 
fixes c :: nat 

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

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

543 
(is "_ = ?right") 

544 
proof safe 

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

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

547 
proof cases 

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

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

550 
next 

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

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

553 
qed 

554 
qed auto 

555 

35580  556 
context ordered_ab_group_add 
557 
begin 

558 

559 
lemma 

560 
fixes x :: 'a 

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

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

563 
proof safe 

564 
fix y assume "y < x" 

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

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

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

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

569 
next 

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

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

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

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

574 
qed simp_all 

575 

576 
lemma 

577 
fixes x :: 'a 

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

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

580 
proof  

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

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

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

584 
by (simp_all add: image_image 

585 
del: image_uminus_greaterThan image_uminus_atLeast) 

586 
qed 

587 

588 
lemma 

589 
fixes x :: 'a 

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

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

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

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

594 
by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def 

595 
greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute) 

596 
end 

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

597 

14485  598 
subsubsection {* Finiteness *} 
599 

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

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

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

605 

606 
lemma finite_greaterThanLessThan [iff]: 

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

610 
lemma finite_atLeastLessThan [iff]: 

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

614 
lemma finite_greaterThanAtMost [iff]: 

15045  615 
fixes l :: nat shows "finite {l<..u}" 
14485  616 
by (simp add: greaterThanAtMost_def) 
617 

618 
lemma finite_atLeastAtMost [iff]: 

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

620 
by (simp add: atLeastAtMost_def) 

621 

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

627 
done 

628 

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

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

632 
proof 

633 
assume f:?F show ?B 

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

635 
next 

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

637 
qed 

638 

639 
lemma finite_nat_set_iff_bounded_le: 

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

641 
apply(simp add:finite_nat_set_iff_bounded) 

642 
apply(blast dest:less_imp_le_nat le_imp_less_Suc) 

643 
done 

644 

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

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

14485  648 

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

651 

652 
lemma subset_card_intvl_is_intvl: 

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

654 
proof cases 

655 
assume "finite A" 

656 
thus "PROP ?P" 

32006  657 
proof(induct A rule:finite_linorder_max_induct) 
24853  658 
case empty thus ?case by auto 
659 
next 

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

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

663 
using `b ~: A` insert by fastforce+ 
24853  664 
ultimately show ?case by auto 
665 
qed 

666 
next 

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

668 
qed 

669 

670 

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

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

672 

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

675 
proof 

676 
show "?A <= ?B" 

677 
proof 

678 
fix x assume "x : ?A" 

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

680 
show "x : ?B" 

681 
proof(cases i) 

682 
case 0 with i show ?thesis by simp 

683 
next 

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

685 
qed 

686 
qed 

687 
next 

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

689 
qed 

690 

691 
lemma UN_le_add_shift: 

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

693 
proof 

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

694 
show "?A <= ?B" by fastforce 
36755  695 
next 
696 
show "?B <= ?A" 

697 
proof 

698 
fix x assume "x : ?B" 

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

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

701 
thus "x : ?A" by blast 

702 
qed 

703 
qed 

704 

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

705 
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

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

707 

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

708 
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

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

710 

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

713 
apply (rule UN_finite_subset) 

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

715 
apply blast 

716 
done 

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

717 

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

718 
lemma UN_finite2_eq: 
33044  719 
"(!!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)" 
720 
apply (rule subset_antisym) 

721 
apply (rule UN_finite2_subset, blast) 

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

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

725 

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

726 

14485  727 
subsubsection {* Cardinality *} 
728 

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

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

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

734 

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

14485  737 
apply (erule ssubst, rule card_lessThan) 
15045  738 
apply (subgoal_tac "(%x. x + l) ` {..<ul} = {l..<u}") 
14485  739 
apply (erule subst) 
740 
apply (rule card_image) 

741 
apply (simp add: inj_on_def) 

742 
apply (auto simp add: image_def atLeastLessThan_def lessThan_def) 

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

744 
apply arith 

745 
done 

746 

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

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

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

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

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

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

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

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

758 
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

759 
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

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

761 

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

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

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

764 
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

765 

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

768 
apply(drule ex_bij_betw_finite_nat) 

769 
apply(drule ex_bij_betw_nat_finite) 

770 
apply(auto intro!:bij_betw_trans) 

771 
done 

772 

773 
lemma ex_bij_betw_nat_finite_1: 

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

775 
by (rule finite_same_card_bij) auto 

776 

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

777 
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

778 
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

779 
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

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

781 
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

782 
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

783 
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

784 
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

785 
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

786 
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

787 
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

788 
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

789 
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

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

791 

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

792 
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

793 
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

794 
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

795 
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

796 
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

797 
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

798 
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

799 
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

800 
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

801 
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

802 
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

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

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

805 
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

806 
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

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

808 
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

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

810 

14485  811 
subsection {* Intervals of integers *} 
812 

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

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

816 
lemma atLeastPlusOneAtMost_greaterThanAtMost_int: "{l+1..u} = {l<..(u::int)}" 
14485  817 
by (auto simp add: atLeastAtMost_def greaterThanAtMost_def) 
818 

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

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

820 
"{l+1..<u} = {l<..<u::int}" 
14485  821 
by (auto simp add: atLeastLessThan_def greaterThanLessThan_def) 
822 

823 
subsubsection {* Finiteness *} 

824 

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

825 
lemma image_atLeastZeroLessThan_int: "0 \<le> u ==> 
15045  826 
{(0::int)..<u} = int ` {..<nat u}" 
14485  827 
apply (unfold image_def lessThan_def) 
828 
apply auto 

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

35216  830 
apply (auto simp add: zless_nat_eq_int_zless [THEN sym]) 
14485  831 
done 
832 

15045  833 
lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}" 
47988  834 
apply (cases "0 \<le> u") 
14485  835 
apply (subst image_atLeastZeroLessThan_int, assumption) 
836 
apply (rule finite_imageI) 

837 
apply auto 

838 
done 

839 

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

14485  842 
apply (erule subst) 
843 
apply (rule finite_imageI) 

844 
apply (rule finite_atLeastZeroLessThan_int) 

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

845 
apply (rule image_add_int_atLeastLessThan) 
14485  846 
done 
847 

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

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

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

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

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

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

24853  857 

14485  858 
subsubsection {* Cardinality *} 
859 

15045  860 
lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u" 
47988  861 
apply (cases "0 \<le> u") 
14485  862 
apply (subst image_atLeastZeroLessThan_int, assumption) 
863 
apply (subst card_image) 

864 
apply (auto simp add: inj_on_def) 

865 
done 

866 

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

14485  869 
apply (erule ssubst, rule card_atLeastZeroLessThan_int) 
15045  870 
apply (subgoal_tac "(%x. x + l) ` {0..<ul} = {l..<u}") 
14485  871 
apply (erule subst) 
872 
apply (rule card_image) 

873 
apply (simp add: inj_on_def) 

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

874 
apply (rule image_add_int_atLeastLessThan) 
14485  875 
done 
876 

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

29667  878 
apply (subst atLeastLessThanPlusOne_atLeastAtMost_int [THEN sym]) 
879 
apply (auto simp add: algebra_simps) 

880 
done 

14485  881 

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

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

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

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

888 
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

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

890 
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

891 
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

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

893 

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

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

895 
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

896 
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

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

898 
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

899 
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

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

901 

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

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

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

905 
apply fastforce 
27656
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 (rule inj_on_diff_nat) 
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 x) 
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 
apply (case_tac xa) 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
26105
diff
changeset

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

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

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

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

916 

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

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

918 
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

919 
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

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

921 
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

922 
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

923 
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

924 
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

925 
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

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

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

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

929 
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

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

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

932 
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

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

934 

14485  935 

13850  936 
subsection {*Lemmas useful with the summation operator setsum*} 
937 

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

938 
text {* For examples, see Algebra/poly/UnivPoly2.thy *} 
13735  939 

14577  940 
subsubsection {* Disjoint Unions *} 
13735  941 

14577  942 
text {* Singletons and open intervals *} 
13735  943 

944 
lemma ivl_disj_un_singleton: 

15045  945 
"{l::'a::linorder} Un {l<..} = {l..}" 
946 
"{..<u} Un {u::'a::linorder} = {..u}" 

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

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

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

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

951 
by auto 
13735  952 

14577  953 
text {* One and twosided intervals *} 
13735  954 

955 
lemma ivl_disj_un_one: 

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

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

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

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

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

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

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

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

964 
by auto 
13735  965 

14577  966 
text {* Two and twosided intervals *} 
13735  967 

968 
lemma ivl_disj_un_two: 

15045  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}" 

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

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

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

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

977 
by auto 
13735  978 

979 
lemmas ivl_disj_un = ivl_disj_un_singleton ivl_disj_un_one ivl_disj_un_two 

980 

14577  981 
subsubsection {* Disjoint Intersections *} 
13735  982 

14577  983 
text {* One and twosided intervals *} 
13735  984 

985 
lemma ivl_disj_int_one: 

15045  986 
"{..l::'a::order} Int {l<..<u} = {}" 
987 
"{..<l} Int {l..<u} = {}" 

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

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

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

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

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

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

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

994 
by auto 
13735  995 

14577  996 
text {* Two and twosided intervals *} 
13735  997 

998 
lemma ivl_disj_int_two: 

15045  999 
"{l::'a::order<..<m} Int {m..<u} = {}" 
1000 
"{l<..m} Int {m<..<u} = {}" 

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

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

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

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

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

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

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

1007 
by auto 
13735  1008 

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

1009 
lemmas ivl_disj_int = ivl_disj_int_one ivl_disj_int_two 
13735  1010 

15542  1011 
subsubsection {* Some Differences *} 
1012 

1013 
lemma ivl_diff[simp]: 

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

1015 
by(auto) 

1016 

1017 

1018 
subsubsection {* Some Subset Conditions *} 

1019 

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

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

1023 
apply(rule ccontr) 

1024 
apply(insert linorder_le_less_linear[of i n]) 

1025 
apply(clarsimp simp:linorder_not_le) 

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

1026 
apply(fastforce) 
15542  1027 
done 
1028 

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

1029 

15042  1030 
subsection {* Summation indexed over intervals *} 
1031 

1032 
syntax 

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

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

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

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

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

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

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

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

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

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

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

1056 

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

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

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

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

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

1062 

15052  1063 
text{* The above introduces some pretty alternative syntaxes for 
15056  1064 
summation over intervals: 
15052  1065 
\begin{center} 
1066 
\begin{tabular}{lll} 

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

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

16052  1070 
@{term[source]"\<Sum>x\<in>{..b}. e"} & @{term"\<Sum>x\<le>b. e"} & @{term[mode=latex_sum]"\<Sum>x\<le>b. e"}\\ 
15056  1071 
@{term[source]"\<Sum>x\<in>{..<b}. e"} & @{term"\<Sum>x<b. e"} & @{term[mode=latex_sum]"\<Sum>x<b. e"} 
15052  1072 
\end{tabular} 
1073 
\end{center} 

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

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

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

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

15052  1081 

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

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

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

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

1086 

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

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

1090 
the context. *} 

1091 

1092 
lemma setsum_ivl_cong: 

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

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

1095 
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

1096 

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

1099 

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

1102 

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

1105 

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

1109 

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

16041  1113 
(* 
15561  1114 
lemma setsum_cl_ivl_add_one_nat: "(n::nat) <= m + 1 ==> 
1115 
(\<Sum>i=n..m+1. f i) = (\<Sum>i=n..m. f i) + f(m + 1)" 

1116 
by (auto simp:add_ac atLeastAtMostSuc_conv) 

16041  1117 
*) 
28068  1118 

1119 
lemma setsum_head: 

1120 
fixes n :: nat 

1121 
assumes mn: "m <= n" 

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

1123 
proof  

1124 
from mn 

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

1126 
by (auto intro: ivl_disj_un_singleton) 

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

1128 
by (simp add: atLeast0LessThan) 

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

1130 
finally show ?thesis . 

1131 
qed 

1132 

1133 
lemma setsum_head_Suc: 

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

1135 
by (simp add: setsum_head atLeastSucAtMost_greaterThanAtMost) 

1136 

1137 
lemma setsum_head_upt_Suc: 

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

1139 
apply(insert setsum_head_Suc[of m "n  Suc 0" f]) 
29667  1140 
apply (simp add: atLeastLessThanSuc_atLeastAtMost[symmetric] algebra_simps) 
28068  1141 
done 
1142 

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

1145 
proof 

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

1147 
thus ?thesis by (auto simp: ivl_disj_int setsum_Un_disjoint 

1148 
atLeastSucAtMost_greaterThanAtMost) 

1149 
qed 

28068  1150 

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

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

1154 

1155 
lemma setsum_diff_nat_ivl: 

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

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

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

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

1160 
apply (simp add: add_ac) 

1161 
done 

1162 

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

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

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

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

1168 

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

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

1172 

1173 
lemma setsum_restrict_set'': 

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

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

31509  1176 

1177 
lemma setsum_setsum_restrict: 

44008  1178 
"finite S \<Longrightarrow> finite T \<Longrightarrow> 
1179 
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" 

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

31509  1181 

1182 
lemma setsum_image_gen: assumes fS: "finite S" 

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

1184 
proof 

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

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

1187 
by simp 

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

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

1190 
finally show ?thesis . 

1191 
qed 

1192 

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

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

1194 
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

1195 
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

1196 
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

1197 
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

1198 
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

1199 
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

1200 
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

1201 
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

1202 
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

1203 
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

1204 
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

1205 
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

1206 
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

1207 
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

1208 
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

1209 
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

1210 
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

1211 
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

1212 
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

1213 

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

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

1217 
proof 

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

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

1220 
using assms(3) by auto 

1221 
finally show ?thesis . 

1222 
qed 

1223 

1224 
lemma setsum_multicount: 

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

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

1227 
proof 

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

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

1232 

28068  1233 

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

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

1235 

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

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

1239 

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

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

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

1242 
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

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

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

1245 

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

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

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

1248 
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

1249 

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

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

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

1252 
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

1253 

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

1256 
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

1257 

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

1260 
apply(cases k)apply simp 

1261 
apply(simp add:setsum_head_upt_Suc) 

1262 
done 

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

1263 

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

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

1265 

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

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

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

1268 
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

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

1270 
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

1271 
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

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

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

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

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

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

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

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

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

1281 

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

1282 

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

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

1284 

47222
1b7c909a6fad
rephrase lemmas about arithmetic series using numeral '2'
huffman
parents:
47108
diff
changeset

1285 
lemma gauss_sum: 
1b7c909a6fad
rephrase lemmas about arithmetic series using numeral '2'
huffman
parents:
47108
diff
changeset

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

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

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

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

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

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

1292 
case (Suc n) 
47222
1b7c909a6fad
rephrase lemmas about arithmetic series using numeral '2'
huffman
parents:
47108
diff
changeset

1293 
then show ?case 
